zoukankan      html  css  js  c++  java
  • z3约束器学习笔记

    • 安装方法

    pip install z3-solver

    或者也可以去github

    https://github.com/Z3Prover/z3
    • 使用方法

    • 申明变量

    一,申请 Int对象 语法 “ Int(name) ”   name即对象名字

    x = Int('x')

      似乎只能进行加减乘除的约束

    二,申请 位向量 语法“ Bitvex(name,size) ” name为对象名字,size为大小 2^size  (这里似乎可以看作是一个约束)

    x = BitVec('x',16)

      位向量还可以一次性申请多个,类似这样

    x,y,z = BitVecs('x y z',16)

      等价于

    x = BitVec('x',16)
    y = BitVec('y',16)
    z = BitVec('z',16)
    • 创建解的对象

    sol = Solver()
    • 添加约束条件

    sol.add(约束式子)
    • 求解

    sol.check() # 如果返回 sat 则存在解
    • 输出解

    print sol.model()

      sol.model() 其实是一个list,可以用我们变量名称作为下标取出里面的值,比如

    x = Int('x')
    y = Int('y')
    s = Solver()
    s.add(x+y == 4)
    s.add(x > 0)
    s.add(y > 0)
    if s.check() == sat:
        m = s.model()
        print m[x]
    • 多解情况

      很清晰的思路,直接吧每一次计算出来的解add进入条件,使其不成立

    while s.check() == sat:
        m = s.model()
        print m
        s.add(Or(x!=m[x],y!=m[y],z!=m[z]))

      注意这里的Or(),可以理解为不能让里面的式子同时不成立。少了它就相当于

    x!=m[x] and y!=m[y] and z!=m[z]

      明显就会漏解

  • 相关阅读:
    linux中服务器定时程序设定
    Linux中java项目环境部署,简单记录一下
    四则运算使用栈和后缀表达式
    PAT乙1003
    L7,too late
    PAT乙1002
    L6,Percy Buttons
    如何计算递归算法的时间复杂度
    c#打印(转)
    C中数组与指针【转】
  • 原文地址:https://www.cnblogs.com/lxy8584099/p/12924357.html
Copyright © 2011-2022 走看看