package mc2

You can search for identifiers within the package.

in-package search v0.2.0

On This Page

Actions for Plugins

mc2.backend
- Mc2_backend
  - Backend_intf
    
    S
  - Dot
    
    Arg
    
    Default
    
    Make
    
    A
mc2.core
- Mc2_core
  - Actions
  - Atom
  - Bound_var
  - Builtins
  - Clause
  - Error
  - ID
    
    Smtlib
  - Lemma
    
    TC
  - Plugin
    
    Factory
    
    S
  - Proof
  - Service
    
    Key
    
    Registry
  - Solver
    
    Sat_state
    
    Unsat_state
  - Statement
  - Term
    
    Bool
    
    TC
    
    TERM_ALLOC
    
    TERM_ALLOC_OPS
    
    Term_allocator
    
    T
    
    Watch1
    
    Watch2
  - Tseitin
    
    Arg
    
    Make
    
    F
    
    S
  - Type
    
    Alloc
    
    T
    
    TC
    
    TY_ALLOC_OPS
  - Value
    
    TC
mc2.dimacs
- Mc2_dimacs
  - Plugin_sat
mc2.lra
- Mc2_lra
  - LE
    
    Infix
mc2.propositional
- Mc2_propositional
  - F
mc2.smtlib
- Mc2_smtlib
  - Make
    
    ARG
  - Typecheck
    
    Make
    
    ARG
mc2.uf
- Mc2_uf
mc2.unin_sort
- Mc2_unin_sort

Legend:
Library
Module
Module type
Parameter
Class
Class type

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.

type t

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 -> int

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

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

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 call f when the solver backtracks