module M: sig .. end
Interface to the solver.
val check : ?tnf:bool -> Structure.structure -> Formula.formula -> bool
Check the formula on the structure.
val evaluate : ?tnf:bool ->
Structure.structure -> Formula.formula -> Assignments.assignment_set
Evaluate the formula on the structure.
val evaluate_partial : ?tnf:bool ->
Structure.structure ->
Assignments.assignment_set -> Formula.formula -> Assignments.assignment_set
Evaluate the formula on the structure and join with given assignment.
val evaluate_real : string ->
Formula.real_expr -> Structure.structure -> Assignments.assignment_set
Evaluate real expressions. Result is represented as assignments with
real-valued polynomials using variable rvar to represent expr.
We assume that rvar does not occur in expr.
val get_real_val : ?asg:Assignments.assignment_set ->
Formula.real_expr -> Structure.structure -> float
Get the value of a real expression without free variables.
val set_timeout : (unit -> bool) -> unit
Set timeout function.
val clear_timeout : unit -> unit
Clear timeout function.