SMTSatSolver

(类来自 pyomo.contrib.satsolver.satsolver)

class pyomo.contrib.satsolver.satsolver.SMTSatSolver(model=None, logger=None)

基础类：object

可满足性求解器，通过使用z3 Sat求解器检查约束的可行性。对象以与SMT-LIB标准一致的形式存储表达式和变量。 有关SMT-LIB标准的文档，请参见 http://smtlib.cs.uiowa.edu/

__init__(model=None, logger=None)

方法

__init__([model, logger])
add_expr(expression)
add_var(var)
check()
get_SMT_string()
get_var_dict()

成员文档