Solver and Model API for SMT solving
Context methods (receiver omitted for clarity)
NewSolver creates a new solver for the given context.
NewSolverForLogic creates a solver for a specific logic.
FuncInterp represents a function interpretation in a model.
GetArity returns the arity of the function interpretation.
GetElse returns the else value of the function interpretation.
NumEntries returns the number of entries in the function interpretation.
Model represents a Z3 model (satisfying assignment).
Eval evaluates an expression in the model. If modelCompletion is true, Z3 will assign an interpretation for uninterpreted constants.
GetConstDecl returns the i-th constant declaration in the model.
GetConstInterp returns the interpretation of a constant.
GetFuncDecl returns the i-th function declaration in the model.
GetFuncInterp returns the interpretation of a function.
NumConsts returns the number of constants in the model.
NumFuncs returns the number of function interpretations in the model.
SortUniverse returns the universe of values for an uninterpreted sort in the model. The universe is represented as a list of distinct expressions. Returns nil if the sort is not an uninterpreted sort in this model.
String returns the string representation of the model.
Solver represents a Z3 solver.
Assert adds a constraint to the solver.
AssertAndTrack adds a constraint with a tracking literal.
Assertions returns the assertions in the solver.
Check checks the satisfiability of the constraints.
CheckAssumptions checks satisfiability under assumptions.
CongruenceExplain returns an explanation for why two expressions are congruent. The result is an expression that justifies the congruence between a and b. Note: This function works primarily with SimpleSolver. Terms and variables that are eliminated during pre-processing are not visible to the congruence closure.
CongruenceNext returns the next element in the congruence class of the given expression. This allows iteration through all elements in a congruence class. Note: This function works primarily with SimpleSolver. Terms and variables that are eliminated during pre-processing are not visible to the congruence closure.
CongruenceRoot returns the congruence class representative of the given expression. This returns the root element in the congruence closure for the term. Note: This function works primarily with SimpleSolver. Terms and variables that are eliminated during pre-processing are not visible to the congruence closure.
FromFile parses and asserts SMT-LIB2 formulas from a file. The solver will contain the assertions from the file after this call.
FromString parses and asserts SMT-LIB2 formulas from a string. The solver will contain the assertions from the string after this call.
GetHelp returns a string describing all available solver parameters.
GetParamDescrs returns parameter descriptions for the solver.
GetStatistics returns the statistics for the solver. Statistics include performance metrics, memory usage, and decision statistics.
Interrupt interrupts the solver execution. This is useful for stopping long-running solver operations gracefully.
Model returns the model if the constraints are satisfiable.
NonUnits returns the non-unit clauses in the solver's current state. These are clauses that have not been reduced to unit clauses. This is useful for debugging and understanding solver behavior.
NumScopes returns the number of backtracking points.
Pop removes backtracking points.
Push creates a backtracking point.
ReasonUnknown returns the reason why the result is unknown.
Reset removes all assertions from the solver.
SetInitialValue provides an initial value hint for a variable to the solver. This can help guide the solver to find solutions more efficiently. The variable must be a constant or function application, and the value must be compatible with the variable's sort.
SetParams sets solver parameters. Parameters control solver behavior such as timeout, proof generation, etc.
String returns the string representation of the solver.
Trail returns the decision trail of the solver. The trail contains the sequence of literals assigned during search. This is useful for understanding the solver's decision history. Note: This function works primarily with SimpleSolver. For solvers created using tactics (e.g., NewSolver()), it may return an error.
TrailLevels returns the decision levels for each literal in the trail. The returned slice has the same length as the trail, where each element indicates the decision level at which the corresponding trail literal was assigned. This is useful for understanding the structure of the search tree. Note: This function works primarily with SimpleSolver. For solvers created using tactics (e.g., NewSolver()), it may return an error.
Units returns the unit clauses (literals) learned by the solver. Unit clauses are assertions that have been simplified to single literals. This is useful for debugging and understanding solver behavior.
UnsatCore returns the unsat core if the constraints are unsatisfiable.