Module Mc2_core.Actions
Actions for Plugins
type t
= Mc2_core__.Solver_types.actions
Actions available to terms/plugins when doing propagation/model building, including adding clauses, registering actions to do upon backtracking, etc.
val push_clause : t -> Mc2_core__.Solver_types.clause -> unit
push a new clause. This clause is added to the solver and will not be backtracked.
val level : t -> Mc2_core__.Solver_types.level
access current decision level
val propagate_bool_eval : t -> Mc2_core__.Solver_types.term -> bool -> subs:Mc2_core__.Solver_types.term list -> unit
propagate_bool_eval t b l
propagates the boolean literalt
assigned to boolean valueb
, explained by evaluation with relevant (sub)termsl
- parameter subs
subterms used for the propagation
val propagate_bool_lemma : t -> Mc2_core__.Solver_types.term -> bool -> Mc2_core__.Solver_types.atom list -> Mc2_core__.Solver_types.lemma -> unit
propagate_bool_lemma t b c
propagates the boolean literalt
assigned to boolean valueb
, explained by a valid theory lemmac
. Precondition:c
is a tautology such thatc == (c' ∨ t=b)
, wherec'
is composed of atoms false in current model.
val raise_conflict : t -> Mc2_core__.Solver_types.atom list -> Mc2_core__.Solver_types.lemma -> 'a
Raise a conflict with the given clause, which must be false in the current trail, and with a lemma to explain
val on_backtrack : t -> (unit -> unit) -> unit
on_backtrack f
will callf
when the solver backtracks