satsolver

Classes

SMTSatSolver([model, logger])	通过使用z3 Sat Solver检查约束可行性的可满足性求解器。
SMT_visitor(varmap)	从相应的Pyomo表达式创建一个SMT表达式。

Functions

satisfiable(model[, logger])

检查模型是否可满足。