aigs和sat解算器之间的pythonic接口。
py-aiger-sat的Python项目详细描述
py aiger sat
aigs和sat解算器之间的pythonic接口。
目录
安装
如果您只需要使用aiger_sat，您可以运行：
$ pip install py-aiger-sat
对于开发人员，请注意此项目使用 poetrypython包/依赖项 管理工具。请熟悉它，然后 运行：
$ poetry install
用法
aiger_sat有两个独立的api。第一个称为对象api，
围绕SolverWrapper对象-围绕
pysat解算器。第二个是函数api，它公开了4个函数
solve、is_sat、is_valid和are_equiv。函数api是
主要用于简单的一次性SAT实例，其中
当需要增量解决方案或
必须公开底层的pysat解算器。
对象API
fromaiger_satimportSolverWrappersolver=SolverWrapper()# defaults to Glucose4frompysat.solverimportGlucose3solver2=SolverWrapper(solver=Glucose3)
solver以aiger的形式操作布尔表达式
单输出电路。例如，
importaigerx,y,z=map(aiger.atom,['x','y','z'])expr=(x&y)|~zsolver.add_expr(expr)assertsolver.is_sat()model=solver.get_model()print(model)# {'x': True, 'y': False, 'z': False}assertexpr(model)
此外，aiger_sat支持进行假设和计算
不安全内核。
# Make invalid assumption.assertnotsolver.is_sat(assumptions={'x':False,'z':True,})assertnotsolver.unsolvedcore=solver.get_unsat_core()assertcore=={'x':False,'z':True}
函数api
importaigerimportaiger_satx,y,z=map(aiger.atom,['x','y','z'])assertaiger_sat.is_sat(x&y&z)model=aiger_sat.solve(x&y&z)assertmodel=={'x':True,'y':True,'z':True}assertaiger_sat.is_valid(aiger.atom(True))expr1=x&yexpr2=x&y&(z|~z)assertaiger_sat.are_equiv(expr1,expr2)
欢迎加入QQ群-->： 979659372
