Struct batsat::core::TheoryArg

pub struct TheoryArg<'a> { /* fields omitted */ }

The temporary theory argument, passed to the theory.

This is where the theory can perform actions such as adding clauses. When the theory is called (on a partial model that is satisfiable on the boolean level), it can use this object to trigger conflicts, add lemmas, and propagate literals.

Implementations

impl<'a> TheoryArg<'a>

pub fn is_ok(&self) -> bool

Is the state of the solver still potentially satisfiable?

is_ok() == false means UNSAT was found.

pub fn value(&self, v: Var) -> lbool

Value of given var in current model.

pub fn model(&self) -> &[Lit]

Current (possibly partial) model, as a slice of true literals.

pub fn mk_new_lit(&mut self) -> Lit

Allocate a new literal.

pub fn add_theory_lemma(&mut self, c: &[Lit])

Push a theory lemma into the solver.

This is useful for lemma-on-demand or theory splitting, but can be relatively costly.

NOTE: This is not fully supported yet.

pub fn propagate(&mut self, p: Lit) -> bool

Propagate the literal p, which is theory-implied by the current trail.

This will add p on the trail. The theory must be ready to provide an explanation via Theory::explain_prop(p) if asked to during conflict resolution.

Returns true if propagation succeeded (or did nothing), false if the propagation results in an immediate conflict. If this returns false, the theory should avoid doing more work and return as early as reasonably possible.

pub fn raise_conflict(&mut self, lits: &[Lit], costly: bool)

Add a conflict clause.

This should be used in the theory when the current partial model is unsatisfiable. It will force the SAT solver to backtrack. All propagations added with propagate during this session will be discarded.

Params

• lits a clause that is a tautology of the theory (ie a lemma) and that is false in the current (partial) model.
• costly if true, indicates that the conflict c was costly to produce. This is a hint for the SAT solver to keep the theory lemma that corresponds to c along with the actual learnt clause.