Module `A.Solver`

module Lit = Libzipperposition.BBox.Lit

exception UndecidedLit

type clause = Lit.t list

val add_clause : 
  proof:Libzipperposition.Sat_solver.proof_step ->
  Lit.t list ->
  unit

add_clause ~tag ~proof c adds the constraint c to the SAT solver, annotated with proof. tag is a unique identifier for this constraint and must not have been already used.

val add_clauses : 
  proof:Libzipperposition.Sat_solver.proof_step ->
  Lit.t list list ->
  unit

val add_clause_seq : 
  proof:Libzipperposition.Sat_solver.proof_step ->
  Lit.t list Iter.t ->
  unit

val check : full:bool -> unit -> Libzipperposition.Sat_solver.result

Is the current problem satisfiable?

parameter full
if true, check unconditionally

val last_result : unit -> Libzipperposition.Sat_solver.result

Last computed result. This does not compute a new result

val valuation : Lit.t -> bool

Assuming the last call to check returned Sat, get the boolean valuation for this (positive) literal in the current model.

raises WrongState
if the last result wasn't Sat

val valuation_level : Lit.t -> bool * int

Gives the value of a literal in the model, as well as its decision level. If decision level is 0, the literal has been proved, rather than decided/propagated

raises WrongState
if the last result wasn't Sat

val proved_at_0 : Lit.t -> bool option

If the literal has been propagated at decision level 0, return its value (which does not depend on the model). Otherwise return None

val all_proved : unit -> Lit.Set.t

Set of (signed) proved literals

val set_printer : Lit.t CCFormat.printer -> unit

How to print literals?

val get_proof : unit -> Libzipperposition.Sat_solver.proof

Return a proof of false, assuming check returned Unsat. The leaves of the proof are input clauses' proofs, the internal nodes are clauses deduced by the SAT solver.

raises WrongState
if the last result isn't Unsat

val get_proof_opt : unit -> Libzipperposition.Sat_solver.proof option

Obtain the proof, if any

val get_proof_of_lit : Lit.t -> Libzipperposition.Sat_solver.proof

get_proof_of_lit lit returns the proof of lit, assuming it has been proved true at level 0 (see valuation_level)

raises Invalid_argument
if the literal is not at level 0

val setup : unit -> unit

val clear : ?size:[ `Big | `Small | `Tiny ] -> unit -> unit

Reset the SAT solver state

Install

Dune Dependency

Authors

Maintainers

Sources

doc/libzipperposition.induction/Libzipperposition_induction/Make/argument-2-A/Solver/index.html

Module `A.Solver`

package libzipperposition

Install

Dune Dependency

Authors

Maintainers

Sources

doc/libzipperposition.induction/Libzipperposition_induction/Make/argument-2-A/Solver/index.html

Module A.Solver

Module `A.Solver`