Module Prover (.ml)

module Prover: sig .. end

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 assume_goal_no_check : Node.t -> unit

Same as assume_goal but without the solver check

val assume_node_no_check : Node.t -> Types.ArrayAtom.t -> unit

Same as assume_node but without the solver check

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