Module Mc2_core.ActionsSource

Actions for Plugins

Plugins are given a set of possible actions at certain times, such as propagation or first-time addition of watches to a term.

Sourcetype t

Actions available to terms/plugins when doing propagation/model building, including adding clauses, registering actions to do upon backtracking, etc.

Sourceval 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.

Sourceval level : t -> int

access current decision level

Sourceval 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 literal t assigned to boolean value b, explained by evaluation with relevant (sub)terms l

  • parameter subs

    subterms used for the propagation

Sourceval 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 literal t assigned to boolean value b, explained by a valid theory lemma c. Precondition: c is a tautology such that c == (c' ∨ t=b), where c' is composed of atoms false in current model.

Sourceval 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

Sourceval on_backtrack : t -> (unit -> unit) -> unit

on_backtrack f will call f when the solver backtracks