Module Prover (.ml)

module Prover: sig .. end
Interface with the SMT solver


Interface with the SMT solver
module SMT: Smt.Solver 
Instance of the SMT solver
val unsafe : Ast.t_system -> Node.t -> unit
Checks if the node is directly reachable on init of the system
val reached : Hstring.t list -> Types.SAtom.t -> Types.SAtom.t -> unit
reached vars s1 s2 raises Unsat if s2 has not been reached
val assume_goal : Node.t -> unit
Clears the context and assumes a goal formula
val assume_node : Node.t -> Types.ArrayAtom.t -> unit
assume_node n a assumes the negation of a node n given in the form of a renaming a; raises Unsat if the context becomes unsatisfiable
val check_guard : Hstring.t list -> Types.SAtom.t -> Types.SAtom.t -> unit
check_guard vars s g checks if the guard g is feasible in state s; raises Unsat if it is not the case
val make_literal : Types.Atom.t -> Smt.Formula.t
val make_formula : Types.ArrayAtom.t -> Smt.Formula.t
val make_formula_set : Types.SAtom.t -> Smt.Formula.t
val run : unit -> unit
Runs the SMT solver on its current context
val assume_goal_nodes : Node.t -> (Node.t * Types.ArrayAtom.t) list -> unit