SMTSatSolver

(class from pyomo.contrib.satsolver.satsolver)

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

Bases: object

Satisfiability solver that checks constraint feasibility through use of z3 Sat Solver. Object stores expressions and variables in form consistent with SMT-LIB standard. For documentation on SMT-LIB standard see http://smtlib.cs.uiowa.edu/

__init__(model=None, logger=None)

Methods

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

Member Documentation