#!/usr/bin/env python # -*- coding: utf-8 -*- from z3 import * # 創建約束決議器 solver = Solver() # 定義變數 m1 = Int('m1') m2 = Int('m2') m3 = Int('m3') m4 = Int('m4') m5 = Int('m5') m6 = Int('m6') m7 = Int('m7') # 添加約束條件 # 引數前7個ascii等于0x321 solver.add(m1+m2+m3+m4+m5+m6+m7==0x321) # 約束每個解的范圍都是在可見字串 solver.add(32<=m1) solver.add(m1<127) solver.add(32<=m2) solver.add(m2<127) solver.add(32<=m3) solver.add(m3<127) solver.add(32<=m4) solver.add(m4<127) solver.add(32<=m5) solver.add(m5<127) solver.add(32<=m6) solver.add(m6<127) solver.add(32<=m7) solver.add(m7<127) if solver.check() == sat: flag = solver.model() print(flag) else: print("no answer")
轉載請註明出處，本文鏈接：https://www.uj5u.com/houduan/5076.html
標籤：Python