diff --git a/dev/sidekick-base/Sidekick_base/Solver/index.html b/dev/sidekick-base/Sidekick_base/Solver/index.html index 36ea3665..6ac4a3d0 100644 --- a/dev/sidekick-base/Sidekick_base/Solver/index.html +++ b/dev/sidekick-base/Sidekick_base/Solver/index.html @@ -28,7 +28,7 @@ t -> Sidekick_smt_solver.Sigs.lit list -> Sidekick_smt_solver.Sigs.Proof.Pterm.delayed -> - unit

Add a clause to the solver, given as a list.

val assert_terms : t -> Sidekick_smt_solver.Sigs.term list -> unit

Helper that turns each term into an atom, before adding disjunction of the resulting atoms to the solver as a clause assertion

val assert_term : t -> Sidekick_smt_solver.Sigs.term -> unit

Helper that turns the term into an atom, before adding the result to the solver as a unit clause assertion

val add_ty : t -> Sidekick_smt_solver.Sigs.ty -> unit
type res = Check_res.t =
| Sat of Sidekick_smt_solver.Sigs.Model.t(*

Satisfiable

*)
| Unsat of {
unsat_core : unit -> Sidekick_smt_solver.Sigs.lit Iter.t;(*

Unsat core (subset of assumptions), or empty

*)
unsat_proof : unit -> Sidekick_smt_solver.Sigs.step_id option;(*

Proof step for the empty clause

*)
}		(*

Unsatisfiable

*)
| Unknown of Unknown.t(*

Unknown, obtained after a timeout, memory limit, etc.

*)

Result of solving for the current set of clauses

val solve : + unit

Add a clause to the solver, given as a list.

val assert_terms : t -> Sidekick_smt_solver.Sigs.term list -> unit

Helper that turns each term into an atom, before adding disjunction of the resulting atoms to the solver as a clause assertion

val assert_term : t -> Sidekick_smt_solver.Sigs.term -> unit

Helper that turns the term into an atom, before adding the result to the solver as a unit clause assertion

val add_ty : t -> Sidekick_smt_solver.Sigs.ty -> unit
type value = Sidekick_smt_solver.Sigs.Term.t
type sat_result = Check_res.sat_result = {
get_value : Sidekick_smt_solver.Sigs.Term.t -> value option;(*

Value for this term

*)
iter_classes : (Sidekick_smt_solver.Sigs.Term.t Iter.t * value) Iter.t;(*

All equivalence classes in the congruence closure

*)
eval_lit : Sidekick_smt_solver.Sigs.Lit.t -> bool option;(*

Evaluate literal

*)
iter_true_lits : Sidekick_smt_solver.Sigs.Lit.t Iter.t;(*

Iterate on literals that are true in the trail

*)
}

Satisfiable

type unsat_result = Check_res.unsat_result = {
unsat_core : unit -> Sidekick_smt_solver.Sigs.Lit.t Iter.t;(*

Unsat core (subset of assumptions), or empty

*)
unsat_proof : unit -> Sidekick_proof.Step.id option;(*

Proof step for the empty clause

*)
}

Unsatisfiable

type res = Check_res.t =
| Sat of sat_result
| Unsat of unsat_result
| Unknown of Unknown.t(*

Unknown, obtained after a timeout, memory limit, etc.

*)

Result of solving for the current set of clauses

val solve : ?on_exit:( unit -> unit ) list -> ?on_progress:( unit -> unit ) -> ?should_stop:( int -> bool ) -> diff --git a/dev/sidekick-base/Sidekick_base/Statement/index.html b/dev/sidekick-base/Sidekick_base/Statement/index.html index d302ba82..27f01bf8 100644 --- a/dev/sidekick-base/Sidekick_base/Statement/index.html +++ b/dev/sidekick-base/Sidekick_base/Statement/index.html @@ -1,2 +1,2 @@ -Statement (sidekick-base.Sidekick_base.Statement)

Module Sidekick_base.Statement

Statements.

A statement is an instruction for the SMT solver to do something, like asserting that a formula is true, declaring a new constant, or checking satisfiabilty of the current set of assertions.

type t = Types_.statement =
| Stmt_set_logic of string
| Stmt_set_option of string list
| Stmt_set_info of string * string
| Stmt_data of Types_.data list
| Stmt_ty_decl of ID.t * int
| Stmt_decl of ID.t * Types_.ty list * Types_.ty
| Stmt_define of Types_.definition list
| Stmt_assert of Types_.term
| Stmt_assert_clause of Types_.term list
| Stmt_check_sat of (bool * Types_.term) list
| Stmt_get_model
| Stmt_get_value of Types_.term list
| Stmt_exit
include Sidekick_sigs.PRINT with type t := t
\ No newline at end of file +Statement (sidekick-base.Sidekick_base.Statement)

Module Sidekick_base.Statement

Statements.

A statement is an instruction for the SMT solver to do something, like asserting that a formula is true, declaring a new constant, or checking satisfiabilty of the current set of assertions.

type t = Types_.statement =
| Stmt_set_logic of string
| Stmt_set_option of string list
| Stmt_set_info of string * string
| Stmt_data of Types_.data list
| Stmt_ty_decl of {
name : ID.t;
arity : int;
ty_const : Types_.ty;
}		(*

new atomic cstor

*)
| Stmt_decl of {
name : ID.t;
ty_args : Types_.ty list;
ty_ret : Types_.ty;
const : Types_.term;
}
| Stmt_define of Types_.definition list
| Stmt_assert of Types_.term
| Stmt_assert_clause of Types_.term list
| Stmt_check_sat of (bool * Types_.term) list
| Stmt_get_model
| Stmt_get_value of Types_.term list
| Stmt_exit
include Sidekick_sigs.PRINT with type t := t
\ No newline at end of file diff --git a/dev/sidekick-base/Sidekick_base/Types_/index.html b/dev/sidekick-base/Sidekick_base/Types_/index.html index dda6913c..e55f4499 100644 --- a/dev/sidekick-base/Sidekick_base/Types_/index.html +++ b/dev/sidekick-base/Sidekick_base/Types_/index.html @@ -4,4 +4,4 @@ * Sidekick_core_logic.Const.Ops.t * ( Sidekick_core_logic__Types_.term Sidekick_util.Ser_decode.t -> Sidekick_core_logic.Const.view Sidekick_util.Ser_decode.t )) - list
type term = Term.t
type ty = Term.t
type value = Term.t
type uconst = {
uc_id : ID.t;
uc_ty : ty;
}

Uninterpreted constant.

type ty_view =
| Ty_int
| Ty_real
| Ty_uninterpreted of {
id : ID.t;
mutable finite : bool;
}
and data = {
data_id : ID.t;
data_cstors : cstor Sidekick_base__.ID.Map.t lazy_t;
data_as_ty : ty lazy_t;
}
and cstor = {
cstor_id : ID.t;
cstor_is_a : ID.t;
mutable cstor_arity : int;
cstor_args : select list lazy_t;
cstor_ty_as_data : data;
cstor_ty : ty lazy_t;
}
and select = {
select_id : ID.t;
select_cstor : cstor;
select_ty : ty lazy_t;
select_i : int;
}
type definition = ID.t * ty * term
type statement =
| Stmt_set_logic of string
| Stmt_set_option of string list
| Stmt_set_info of string * string
| Stmt_data of data list
| Stmt_ty_decl of ID.t * int
| Stmt_decl of ID.t * ty list * ty
| Stmt_define of definition list
| Stmt_assert of term
| Stmt_assert_clause of term list
| Stmt_check_sat of (bool * term) list
| Stmt_get_model
| Stmt_get_value of term list
| Stmt_exit
\ No newline at end of file + list
type term = Term.t
type ty = Term.t
type value = Term.t
type uconst = {
uc_id : ID.t;
uc_ty : ty;
}

Uninterpreted constant.

type ty_view =
| Ty_int
| Ty_real
| Ty_uninterpreted of {
id : ID.t;
mutable finite : bool;
}
and data = {
data_id : ID.t;
data_cstors : cstor Sidekick_base__.ID.Map.t lazy_t;
data_as_ty : ty lazy_t;
}
and cstor = {
cstor_id : ID.t;
cstor_is_a : ID.t;
mutable cstor_arity : int;
cstor_args : select list lazy_t;
cstor_ty_as_data : data;
cstor_ty : ty lazy_t;
}
and select = {
select_id : ID.t;
select_cstor : cstor;
select_ty : ty lazy_t;
select_i : int;
}
type definition = ID.t * ty * term
type statement =
| Stmt_set_logic of string
| Stmt_set_option of string list
| Stmt_set_info of string * string
| Stmt_data of data list
| Stmt_ty_decl of {
name : ID.t;
arity : int;
ty_const : ty;
}		(*

new atomic cstor

*)
| Stmt_decl of {
name : ID.t;
ty_args : ty list;
ty_ret : ty;
const : term;
}
| Stmt_define of definition list
| Stmt_assert of term
| Stmt_assert_clause of term list
| Stmt_check_sat of (bool * term) list
| Stmt_get_model
| Stmt_get_value of term list
| Stmt_exit
\ No newline at end of file diff --git a/dev/sidekick-base/Sidekick_smtlib/Driver/index.html b/dev/sidekick-base/Sidekick_smtlib/Driver/index.html index b1b7f887..356c42ac 100644 --- a/dev/sidekick-base/Sidekick_smtlib/Driver/index.html +++ b/dev/sidekick-base/Sidekick_smtlib/Driver/index.html @@ -1,6 +1,5 @@ Driver (sidekick-base.Sidekick_smtlib.Driver)

Module Sidekick_smtlib.Driver

Driver.

The driver is responsible for processing statements from a SMTLIB file, and interacting with the solver based on the statement (asserting formulas, calling "solve", etc.)

module Asolver = Solver.Asolver
val th_bool_dyn : Sidekick_base.Solver.theory
val th_bool_static : Sidekick_base.Solver.theory
type 'a or_error = ( 'a, string ) CCResult.t
type t

The SMTLIB driver

val create : - ?restarts:bool -> ?pp_cnf:bool -> ?proof_file:string -> ?pp_model:bool -> diff --git a/dev/sidekick-base/Sidekick_smtlib/Model/index.html b/dev/sidekick-base/Sidekick_smtlib/Model/index.html new file mode 100644 index 00000000..948d4eb7 --- /dev/null +++ b/dev/sidekick-base/Sidekick_smtlib/Model/index.html @@ -0,0 +1,2 @@ + +Model (sidekick-base.Sidekick_smtlib.Model)

Module Sidekick_smtlib.Model

Models

A model can be produced when the solver is found to be in a satisfiable state after a call to solve.

type t
type fun_ = Sidekick_core.Term.t
module TL_map : CCMap.S with type key = value list
val empty : t
val is_empty : t -> bool
val add_fun_entry : fun_ -> value list -> value -> t -> t
val get_fun_entry : fun_ -> value list -> t -> value option
val get_fun_entries : fun_ -> t -> value TL_map.t option
val iter_fun_entries : t -> (fun_ * value TL_map.t) Iter.t
val eval : Sidekick_core.Term.t -> t -> value option
include Sidekick_sigs.PRINT with type t := t
\ No newline at end of file diff --git a/dev/sidekick-base/Sidekick_smtlib/index.html b/dev/sidekick-base/Sidekick_smtlib/index.html index ef84c85d..e54945d4 100644 --- a/dev/sidekick-base/Sidekick_smtlib/index.html +++ b/dev/sidekick-base/Sidekick_smtlib/index.html @@ -1,2 +1,2 @@ -Sidekick_smtlib (sidekick-base.Sidekick_smtlib)

Module Sidekick_smtlib

SMTLib-2.6 Driver

This library provides a parser, a type-checker, and a driver for processing SMTLib-2 problems.

type 'a or_error = ( 'a, string ) CCResult.t
module Term = Sidekick_base.Term
module Driver : sig ... end

Driver.

module Solver : sig ... end
module Check_cc : sig ... end
val parse : Term.store -> string -> Stmt.t list or_error
val parse_stdin : Term.store -> Stmt.t list or_error
\ No newline at end of file +Sidekick_smtlib (sidekick-base.Sidekick_smtlib)

Module Sidekick_smtlib

SMTLib-2.6 Driver

This library provides a parser, a type-checker, and a driver for processing SMTLib-2 problems.

type 'a or_error = ( 'a, string ) CCResult.t
module Term = Sidekick_base.Term
module Driver : sig ... end

Driver.

module Solver : sig ... end
module Check_cc : sig ... end
module Model : sig ... end

Models

val parse : Term.store -> string -> Stmt.t list or_error
val parse_stdin : Term.store -> Stmt.t list or_error
\ No newline at end of file diff --git a/dev/sidekick/Sidekick_abstract_solver/Asolver/class-type-t/index.html b/dev/sidekick/Sidekick_abstract_solver/Asolver/class-type-t/index.html index 5ffefa8f..a636e75f 100644 --- a/dev/sidekick/Sidekick_abstract_solver/Asolver/class-type-t/index.html +++ b/dev/sidekick/Sidekick_abstract_solver/Asolver/class-type-t/index.html @@ -1,7 +1,7 @@ t (sidekick.Sidekick_abstract_solver.Asolver.t)

Class type Asolver.t

method assert_term : Sidekick_core.Term.t -> unit

Helper that turns the term into an atom, before adding the result to the solver as a unit clause assertion.

This uses Proof_sat.sat_input_clause to justify the assertion.

method assert_clause : Sidekick_core.Lit.t array -> Proof.Pterm.delayed -> unit

add_clause solver cs adds a boolean clause to the solver. Subsequent calls to solve will need to satisfy this clause.

method assert_clause_l : Sidekick_core.Lit.t list -> Proof.Pterm.delayed -> - unit

Add a clause to the solver, given as a list.

method add_ty : ty:Sidekick_core.Term.t -> unit

Add a new sort/atomic type.

method lit_of_term : ?sign:bool -> Sidekick_core.Term.t -> Sidekick_core.Lit.t

Convert a term into a simplified literal.

method solve : ?on_exit:( unit -> unit ) list -> + unit

Add a clause to the solver, given as a list.

method add_ty : ty:Sidekick_core.Term.t -> unit

Add a new sort/atomic type.

method lit_of_term : ?sign:bool -> Sidekick_core.Term.t -> Sidekick_core.Lit.t

Convert a term into a simplified literal.

method solve : ?on_exit:( unit -> unit ) list -> ?on_progress:( unit -> unit ) -> ?should_stop:( int -> bool ) -> assumptions:Sidekick_core.Lit.t list -> diff --git a/dev/sidekick/Sidekick_abstract_solver/Asolver/index.html b/dev/sidekick/Sidekick_abstract_solver/Asolver/index.html index 51b556fc..b3f0f315 100644 --- a/dev/sidekick/Sidekick_abstract_solver/Asolver/index.html +++ b/dev/sidekick/Sidekick_abstract_solver/Asolver/index.html @@ -1,5 +1,5 @@ -Asolver (sidekick.Sidekick_abstract_solver.Asolver)

Module Sidekick_abstract_solver.Asolver

Abstract interface for a solver

module Unknown = Unknown
module Check_res = Check_res
module Proof = Sidekick_proof
class type t = object ... end
val assert_term : t -> Sidekick_core.Term.t -> unit
val assert_clause : +Asolver (sidekick.Sidekick_abstract_solver.Asolver)

Module Sidekick_abstract_solver.Asolver

Abstract interface for a solver

module Unknown = Unknown
module Check_res = Check_res
module Proof = Sidekick_proof
class type t = object ... end
val assert_term : t -> Sidekick_core.Term.t -> unit
val assert_clause : t -> Sidekick_core.Lit.t array -> Proof.Pterm.delayed -> diff --git a/dev/sidekick/Sidekick_abstract_solver/Check_res/index.html b/dev/sidekick/Sidekick_abstract_solver/Check_res/index.html index 37f7a5d2..6dee6b34 100644 --- a/dev/sidekick/Sidekick_abstract_solver/Check_res/index.html +++ b/dev/sidekick/Sidekick_abstract_solver/Check_res/index.html @@ -1,2 +1,2 @@ -Check_res (sidekick.Sidekick_abstract_solver.Check_res)

Module Sidekick_abstract_solver.Check_res

Result of solving for the current set of clauses

module Model = Sidekick_model
type t =
| Sat of Model.t(*

Satisfiable

*)
| Unsat of {
unsat_core : unit -> Sidekick_core.Lit.t Iter.t;(*

Unsat core (subset of assumptions), or empty

*)
unsat_proof : unit -> Sidekick_proof.Step.id option;(*

Proof step for the empty clause

*)
}		(*

Unsatisfiable

*)
| Unknown of Unknown.t(*

Unknown, obtained after a timeout, memory limit, etc.

*)

Result of calling "check"

val pp : Sidekick_core.Fmt.t -> t -> unit
\ No newline at end of file +Check_res (sidekick.Sidekick_abstract_solver.Check_res)

Module Sidekick_abstract_solver.Check_res

Result of solving for the current set of clauses

type sat_result = {
get_value : Sidekick_core.Term.t -> value option;(*

Value for this term

*)
iter_classes : (Sidekick_core.Term.t Iter.t * value) Iter.t;(*

All equivalence classes in the congruence closure

*)
eval_lit : Sidekick_core.Lit.t -> bool option;(*

Evaluate literal

*)
iter_true_lits : Sidekick_core.Lit.t Iter.t;(*

Iterate on literals that are true in the trail

*)
}

Satisfiable

type unsat_result = {
unsat_core : unit -> Sidekick_core.Lit.t Iter.t;(*

Unsat core (subset of assumptions), or empty

*)
unsat_proof : unit -> Sidekick_proof.Step.id option;(*

Proof step for the empty clause

*)
}

Unsatisfiable

type t =
| Sat of sat_result
| Unsat of unsat_result
| Unknown of Unknown.t(*

Unknown, obtained after a timeout, memory limit, etc.

*)

Result of calling "check"

val pp : Sidekick_core.Fmt.t -> t -> unit
\ No newline at end of file diff --git a/dev/sidekick/Sidekick_abstract_solver/class-type-t/index.html b/dev/sidekick/Sidekick_abstract_solver/class-type-t/index.html index 88dc667f..689a964d 100644 --- a/dev/sidekick/Sidekick_abstract_solver/class-type-t/index.html +++ b/dev/sidekick/Sidekick_abstract_solver/class-type-t/index.html @@ -3,7 +3,7 @@ Asolver.Proof.Pterm.delayed -> unit

add_clause solver cs adds a boolean clause to the solver. Subsequent calls to solve will need to satisfy this clause.

method assert_clause_l : Sidekick_core.Lit.t list -> Asolver.Proof.Pterm.delayed -> - unit

Add a clause to the solver, given as a list.

method add_ty : ty:Sidekick_core.Term.t -> unit

Add a new sort/atomic type.

method lit_of_term : ?sign:bool -> Sidekick_core.Term.t -> Sidekick_core.Lit.t

Convert a term into a simplified literal.

method solve : ?on_exit:( unit -> unit ) list -> + unit

Add a clause to the solver, given as a list.

method add_ty : ty:Sidekick_core.Term.t -> unit

Add a new sort/atomic type.

method lit_of_term : ?sign:bool -> Sidekick_core.Term.t -> Sidekick_core.Lit.t

Convert a term into a simplified literal.

method solve : ?on_exit:( unit -> unit ) list -> ?on_progress:( unit -> unit ) -> ?should_stop:( int -> bool ) -> assumptions:Sidekick_core.Lit.t list -> diff --git a/dev/sidekick/Sidekick_model/.dummy b/dev/sidekick/Sidekick_model/.dummy deleted file mode 100644 index e69de29b..00000000 diff --git a/dev/sidekick/Sidekick_model/index.html b/dev/sidekick/Sidekick_model/index.html deleted file mode 100644 index 97dddfd6..00000000 --- a/dev/sidekick/Sidekick_model/index.html +++ /dev/null @@ -1,2 +0,0 @@ - -Sidekick_model (sidekick.Sidekick_model)

Module Sidekick_model

Models

A model can be produced when the solver is found to be in a satisfiable state after a call to solve.

type t
val empty : t
val is_empty : t -> bool
val mem : t -> Sidekick_core.Term.t -> bool
val keys : t -> Sidekick_core.Term.t Iter.t
val to_iter : t -> (Sidekick_core.Term.t * Sidekick_core.Term.t) Iter.t
include Sidekick_sigs.PRINT with type t := t
\ No newline at end of file diff --git a/dev/sidekick/Sidekick_sat/index.html b/dev/sidekick/Sidekick_sat/index.html index 90f0811e..223892f7 100644 --- a/dev/sidekick/Sidekick_sat/index.html +++ b/dev/sidekick/Sidekick_sat/index.html @@ -1,5 +1,5 @@ -Sidekick_sat (sidekick.Sidekick_sat)

Module Sidekick_sat

Main API

module Proof = Sidekick_proof
module type SAT_STATE = sig ... end

Solver in a "SATISFIABLE" state

type sat_state = (module SAT_STATE)

The type of values returned when the solver reaches a SAT state.

module type UNSAT_STATE = sig ... end

Solver in an "UNSATISFIABLE" state

type 'clause unsat_state = (module UNSAT_STATE with type clause = 'clause)

The type of values returned when the solver reaches an UNSAT state.

type same_sign = bool

This type is used during the normalisation of lits. true means the literal stayed the same, false that its sign was flipped.

type reason =
| Consequence of unit -> Sidekick_core.Lit.t list * Sidekick_proof.Pterm.delayed

The type of reasons for propagations of a lit f.

Consequence (l, p) means that the lits in l imply the propagated lit f. The proof should be a proof of the clause "l implies f".

invariant: in Consequence (fun () -> l,p), all elements of l must be true in the current trail.

note on lazyiness: the justification is suspended (using unit -> …) to avoid potentially costly computations that might never be used if this literal is backtracked without participating in a conflict. Therefore the function that produces (l,p) needs only be safe in trails (partial models) that are conservative extensions of the current trail. If the theory isn't robust w.r.t. extensions of the trail (e.g. if its internal state undergoes significant changes), it can be easier to produce the explanation eagerly when propagating, and then use Consequence (fun () -> expl, proof) with the already produced (expl,proof) tuple.

type lbool =
| L_true
| L_false
| L_undefined(*

Valuation of an atom

*)
val pp_lbool : Sidekick_core.Fmt.t -> lbool -> unit
module type ACTS = sig ... end

Actions available to the Plugin.

type acts = (module ACTS)

The type for a slice of assertions to assume/propagate in the theory.

module type THEORY_CDCL_T = sig ... end

Signature for theories to be given to the CDCL(T) solver

module type PLUGIN = sig ... end
module Solver : sig ... end

The external interface implemented by SAT solvers.

module Tracer : sig ... end

Tracer for clauses and literals

include module type of struct include Solver end
type clause
type plugin = (module Sidekick_sat__Sigs.PLUGIN)
type solver

The main solver type.

type store

Stores atoms, clauses, etc.

module Clause : sig ... end

Main Solver Type

type t = solver

Main solver type, containing all state for solving.

val store : t -> store

Store for the solver

val stat : t -> Sidekick_util.Stat.t

Statistics

val tracer : t -> Tracer.t

Access the inner proof

val on_conflict : t -> ( Clause.t, unit ) Sidekick_util.Event.t
val on_decision : t -> ( Sidekick_core.Lit.t, unit ) Sidekick_util.Event.t
val on_learnt : t -> ( Clause.t, unit ) Sidekick_util.Event.t
val on_gc : t -> ( Sidekick_core.Lit.t array, unit ) Sidekick_util.Event.t

Types

type res =
| Sat of (module Sidekick_sat__Sigs.SAT_STATE)(*

Returned when the solver reaches SAT, with a model

*)
| Unsat of (module Sidekick_sat__Sigs.UNSAT_STATE with type clause = clause)(*

Returned when the solver reaches UNSAT, with a proof

*)

Result type for the solver

exception UndecidedLit

Exception raised by the evaluating functions when a literal has not yet been assigned a value.

Base operations

val assume : t -> Sidekick_core.Lit.t list list -> unit

Add the list of clauses to the current set of assumptions. Modifies the sat solver state in place.

val add_clause : +Sidekick_sat (sidekick.Sidekick_sat)

Module Sidekick_sat

Main API

module Proof = Sidekick_proof
exception UndecidedLit
module type SAT_STATE = sig ... end

Solver in a "SATISFIABLE" state

type sat_state = (module SAT_STATE)

The type of values returned when the solver reaches a SAT state.

module type UNSAT_STATE = sig ... end

Solver in an "UNSATISFIABLE" state

type 'clause unsat_state = (module UNSAT_STATE with type clause = 'clause)

The type of values returned when the solver reaches an UNSAT state.

type same_sign = bool

This type is used during the normalisation of lits. true means the literal stayed the same, false that its sign was flipped.

type reason =
| Consequence of unit -> Sidekick_core.Lit.t list * Sidekick_proof.Pterm.delayed

The type of reasons for propagations of a lit f.

Consequence (l, p) means that the lits in l imply the propagated lit f. The proof should be a proof of the clause "l implies f".

invariant: in Consequence (fun () -> l,p), all elements of l must be true in the current trail.

note on lazyiness: the justification is suspended (using unit -> …) to avoid potentially costly computations that might never be used if this literal is backtracked without participating in a conflict. Therefore the function that produces (l,p) needs only be safe in trails (partial models) that are conservative extensions of the current trail. If the theory isn't robust w.r.t. extensions of the trail (e.g. if its internal state undergoes significant changes), it can be easier to produce the explanation eagerly when propagating, and then use Consequence (fun () -> expl, proof) with the already produced (expl,proof) tuple.

type lbool =
| L_true
| L_false
| L_undefined(*

Valuation of an atom

*)
val pp_lbool : Sidekick_core.Fmt.t -> lbool -> unit
module type ACTS = sig ... end

Actions available to the Plugin.

type acts = (module ACTS)

The type for a slice of assertions to assume/propagate in the theory.

module type THEORY_CDCL_T = sig ... end

Signature for theories to be given to the CDCL(T) solver

module type PLUGIN = sig ... end
module Solver : sig ... end

The external interface implemented by SAT solvers.

module Tracer : sig ... end

Tracer for clauses and literals

include module type of struct include Solver end
type clause
type plugin = (module Sidekick_sat__Sigs.PLUGIN)
type solver

The main solver type.

type store

Stores atoms, clauses, etc.

module Clause : sig ... end

Main Solver Type

type t = solver

Main solver type, containing all state for solving.

val store : t -> store

Store for the solver

val stat : t -> Sidekick_util.Stat.t

Statistics

val tracer : t -> Tracer.t

Access the inner proof

val on_conflict : t -> ( Clause.t, unit ) Sidekick_util.Event.t
val on_decision : t -> ( Sidekick_core.Lit.t, unit ) Sidekick_util.Event.t
val on_learnt : t -> ( Clause.t, unit ) Sidekick_util.Event.t
val on_gc : t -> ( Sidekick_core.Lit.t array, unit ) Sidekick_util.Event.t

Types

type res =
| Sat of (module Sidekick_sat__Sigs.SAT_STATE)(*

Returned when the solver reaches SAT, with a model

*)
| Unsat of (module Sidekick_sat__Sigs.UNSAT_STATE with type clause = clause)(*

Returned when the solver reaches UNSAT, with a proof

*)

Result type for the solver

exception UndecidedLit

Exception raised by the evaluating functions when a literal has not yet been assigned a value.

Base operations

val assume : t -> Sidekick_core.Lit.t list list -> unit

Add the list of clauses to the current set of assumptions. Modifies the sat solver state in place.

val add_clause : t -> Sidekick_core.Lit.t list -> Sidekick_proof.Pterm.delayed -> diff --git a/dev/sidekick/Sidekick_smt_solver/Model/index.html b/dev/sidekick/Sidekick_smt_solver/Model/index.html new file mode 100644 index 00000000..d3ce7a44 --- /dev/null +++ b/dev/sidekick/Sidekick_smt_solver/Model/index.html @@ -0,0 +1,2 @@ + +Model (sidekick.Sidekick_smt_solver.Model)

Module Sidekick_smt_solver.Model

SMT models.

The solver models are partially evaluated; the frontend might ask for values for terms not explicitly present in them.

type t = {
eval : Sigs.Term.t -> Sigs.value option;
map : Sigs.value Sidekick_smt_solver__.Sigs.Term.Map.t;
}
val is_empty : t -> bool
val eval : t -> Sigs.Term.t -> Sigs.value option
val pp : Sidekick_smt_solver__.Sigs.Fmt.t -> t -> unit
\ No newline at end of file diff --git a/dev/sidekick/Sidekick_smt_solver/Model_builder/index.html b/dev/sidekick/Sidekick_smt_solver/Model_builder/index.html index 1ae90707..c07fab9c 100644 --- a/dev/sidekick/Sidekick_smt_solver/Model_builder/index.html +++ b/dev/sidekick/Sidekick_smt_solver/Model_builder/index.html @@ -1,2 +1,5 @@ -Model_builder (sidekick.Sidekick_smt_solver.Model_builder)

Module Sidekick_smt_solver.Model_builder

Model Builder.

This contains a partial model, in construction. It is accessible to every theory, so they can contribute partial values.

TODO: seen values?

type t
include Sidekick_sigs.PRINT with type t := t
val create : Sigs.Term.store -> t
val mem : t -> Sigs.Term.t -> bool
val require_eval : t -> Sigs.Term.t -> unit

Require that this term gets a value.

val add : t -> ?subs:Sigs.Term.t list -> Sigs.Term.t -> Sigs.value -> unit

Add a value to the model.

  • parameter subs

    if provided, these terms will be passed to require_eval to ensure they map to a value.

val gensym : t -> pre:string -> ty:Sigs.Term.t -> Sigs.Term.t

New fresh constant

type eval_cache = Sidekick_smt_solver__.Sigs.Term.Internal_.cache
val eval : ?cache:eval_cache -> t -> Sigs.Term.t -> Sigs.value
val pop_required : t -> Sigs.Term.t option

gives the next subterm that is required but has no value yet

val to_model : t -> Sigs.Model.t
\ No newline at end of file +Model_builder (sidekick.Sidekick_smt_solver.Model_builder)

Module Sidekick_smt_solver.Model_builder

Model Builder.

This contains a partial model, in construction. It is accessible to every theory, so they can contribute partial values.

TODO: seen values?

type t
include Sidekick_sigs.PRINT with type t := t
val create : Sigs.Term.store -> t
val mem : t -> Sigs.Term.t -> bool
val require_eval : t -> Sigs.Term.t -> unit

Require that this term gets a value, and assign it to all terms in the given class.

val add : t -> ?subs:Sigs.Term.t list -> Sigs.Term.t -> Sigs.value -> unit

Add a value to the model.

  • parameter subs

    if provided, these terms will be passed to require_eval to ensure they map to a value.

val gensym : t -> pre:string -> ty:Sigs.Term.t -> Sigs.Term.t

New fresh constant

type eval_cache = Sidekick_smt_solver__.Sigs.Term.Internal_.cache
val create_cache : int -> eval_cache
val eval : ?cache:eval_cache -> t -> Sigs.Term.t -> Sigs.value
val eval_opt : ?cache:eval_cache -> t -> Sigs.Term.t -> Sigs.value option
val pop_required : t -> Sigs.Term.t option

gives the next subterm that is required but has no value yet

val to_map : + ?cache:eval_cache -> + t -> + Sigs.value Sidekick_smt_solver__.Sigs.Term.Map.t
\ No newline at end of file diff --git a/dev/sidekick/Sidekick_smt_solver/Sigs/index.html b/dev/sidekick/Sidekick_smt_solver/Sigs/index.html index bec6b3a4..8081949f 100644 --- a/dev/sidekick/Sidekick_smt_solver/Sigs/index.html +++ b/dev/sidekick/Sidekick_smt_solver/Sigs/index.html @@ -4,4 +4,4 @@ * Sidekick_core_logic.Const.Ops.t * ( Sidekick_core_logic__Types_.term Sidekick_util.Ser_decode.t -> Sidekick_core_logic.Const.view Sidekick_util.Ser_decode.t )) - list
module Model = Sidekick_model
module Simplify = Sidekick_simplify
module CC = Sidekick_cc.CC
module E_node = Sidekick_cc.E_node
module CC_expl = Sidekick_cc.Expl
module Proof = Sidekick_proof
type term = Term.t
type ty = term
type value = Term.t
type lit = Lit.t
type term_store = Term.store
type step_id = Sidekick_proof.Step.id
type sat_acts = Sidekick_sat.acts
type th_combination_conflict = {
lits : lit list;
semantic : (bool * term * term) list;
}

Conflict obtained during theory combination. It involves equalities merged because of the current model so it's not a "true" conflict and doesn't need to kill the current trail.

module type ARG = sig ... end

Argument to pass to the functor Make in order to create a new Msat-based SMT solver.

\ No newline at end of file + list
module Simplify = Sidekick_simplify
module CC = Sidekick_cc.CC
module E_node = Sidekick_cc.E_node
module CC_expl = Sidekick_cc.Expl
module Proof = Sidekick_proof
type term = Term.t
type ty = term
type value = Term.t
type lit = Lit.t
type term_store = Term.store
type step_id = Sidekick_proof.Step.id
type sat_acts = Sidekick_sat.acts
type th_combination_conflict = {
lits : lit list;
semantic : (bool * term * term) list;
}

Conflict obtained during theory combination. It involves equalities merged because of the current model so it's not a "true" conflict and doesn't need to kill the current trail.

module type ARG = sig ... end

Argument to pass to the functor Make in order to create a new Msat-based SMT solver.

\ No newline at end of file diff --git a/dev/sidekick/Sidekick_smt_solver/Solver/index.html b/dev/sidekick/Sidekick_smt_solver/Solver/index.html index 76760d6d..6e902085 100644 --- a/dev/sidekick/Sidekick_smt_solver/Solver/index.html +++ b/dev/sidekick/Sidekick_smt_solver/Solver/index.html @@ -20,7 +20,7 @@ theories:Theory.t list -> Sigs.Term.store -> unit -> - t

Create a new solver with the default CC view, and where all boolean subterms are mapped to boolean atoms.

val add_theory : t -> Theory.t -> unit

Add a theory to the solver. This should be called before any call to solve or to add_clause and the likes (otherwise the theory will have a partial view of the problem).

val add_theory_p : t -> 'a Theory.p -> 'a

Add the given theory and obtain its state

val add_theory_l : t -> Theory.t list -> unit
val mk_lit_t : t -> ?sign:bool -> Sigs.term -> Sigs.lit

mk_lit_t _ ~sign t returns lit', where lit' is preprocess(lit) and lit is an internal representation of ± t.

The proof of |- lit = lit' is directly added to the solver's proof.

val add_clause : t -> Sigs.lit array -> Sigs.Proof.Pterm.delayed -> unit

add_clause solver cs adds a boolean clause to the solver. Subsequent calls to solve will need to satisfy this clause.

val add_clause_l : t -> Sigs.lit list -> Sigs.Proof.Pterm.delayed -> unit

Add a clause to the solver, given as a list.

val assert_terms : t -> Sigs.term list -> unit

Helper that turns each term into an atom, before adding disjunction of the resulting atoms to the solver as a clause assertion

val assert_term : t -> Sigs.term -> unit

Helper that turns the term into an atom, before adding the result to the solver as a unit clause assertion

val add_ty : t -> Sigs.ty -> unit
type res = Check_res.t =
| Sat of Sigs.Model.t(*

Satisfiable

*)
| Unsat of {
unsat_core : unit -> Sigs.lit Iter.t;(*

Unsat core (subset of assumptions), or empty

*)
unsat_proof : unit -> Sigs.step_id option;(*

Proof step for the empty clause

*)
}		(*

Unsatisfiable

*)
| Unknown of Unknown.t(*

Unknown, obtained after a timeout, memory limit, etc.

*)

Result of solving for the current set of clauses

val solve : + t

Create a new solver with the default CC view, and where all boolean subterms are mapped to boolean atoms.

val add_theory : t -> Theory.t -> unit

Add a theory to the solver. This should be called before any call to solve or to add_clause and the likes (otherwise the theory will have a partial view of the problem).

val add_theory_p : t -> 'a Theory.p -> 'a

Add the given theory and obtain its state

val add_theory_l : t -> Theory.t list -> unit
val mk_lit_t : t -> ?sign:bool -> Sigs.term -> Sigs.lit

mk_lit_t _ ~sign t returns lit', where lit' is preprocess(lit) and lit is an internal representation of ± t.

The proof of |- lit = lit' is directly added to the solver's proof.

val add_clause : t -> Sigs.lit array -> Sigs.Proof.Pterm.delayed -> unit

add_clause solver cs adds a boolean clause to the solver. Subsequent calls to solve will need to satisfy this clause.

val add_clause_l : t -> Sigs.lit list -> Sigs.Proof.Pterm.delayed -> unit

Add a clause to the solver, given as a list.

val assert_terms : t -> Sigs.term list -> unit

Helper that turns each term into an atom, before adding disjunction of the resulting atoms to the solver as a clause assertion

val assert_term : t -> Sigs.term -> unit

Helper that turns the term into an atom, before adding the result to the solver as a unit clause assertion

val add_ty : t -> Sigs.ty -> unit
type value = Sigs.Term.t
type sat_result = Check_res.sat_result = {
get_value : Sigs.Term.t -> value option;(*

Value for this term

*)
iter_classes : (Sigs.Term.t Iter.t * value) Iter.t;(*

All equivalence classes in the congruence closure

*)
eval_lit : Sigs.Lit.t -> bool option;(*

Evaluate literal

*)
iter_true_lits : Sigs.Lit.t Iter.t;(*

Iterate on literals that are true in the trail

*)
}

Satisfiable

type unsat_result = Check_res.unsat_result = {
unsat_core : unit -> Sigs.Lit.t Iter.t;(*

Unsat core (subset of assumptions), or empty

*)
unsat_proof : unit -> Sidekick_proof.Step.id option;(*

Proof step for the empty clause

*)
}

Unsatisfiable

type res = Check_res.t =
| Sat of sat_result
| Unsat of unsat_result
| Unknown of Unknown.t(*

Unknown, obtained after a timeout, memory limit, etc.

*)

Result of solving for the current set of clauses

val solve : ?on_exit:( unit -> unit ) list -> ?on_progress:( unit -> unit ) -> ?should_stop:( int -> bool ) -> diff --git a/dev/sidekick/Sidekick_smt_solver/Solver_internal/index.html b/dev/sidekick/Sidekick_smt_solver/Solver_internal/index.html index 8013fa83..65530814 100644 --- a/dev/sidekick/Sidekick_smt_solver/Solver_internal/index.html +++ b/dev/sidekick/Sidekick_smt_solver/Solver_internal/index.html @@ -80,7 +80,7 @@ ?ask:model_ask_hook -> ?complete:model_completion_hook -> t -> - unit

Add model production/completion hooks.

val on_progress : t -> ( unit, unit ) Sidekick_util.Event.t
val is_complete : t -> bool

Are we still in a complete logic fragment?

val last_model : t -> Sigs.Model.t option

Delayed actions

module type PERFORM_ACTS = sig ... end
module Perform_delayed (A : PERFORM_ACTS) : sig ... end
val add_theory_state : + unit

Add model production/completion hooks.

val on_progress : t -> ( unit, unit ) Sidekick_util.Event.t
val is_complete : t -> bool

Are we still in a complete logic fragment?

val last_model : t -> Model.t option

Delayed actions

module type PERFORM_ACTS = sig ... end
module Perform_delayed (A : PERFORM_ACTS) : sig ... end
val add_theory_state : st:'a -> push_level:( 'a -> unit ) -> pop_levels:( 'a -> int -> unit ) -> diff --git a/dev/sidekick/Sidekick_smt_solver/index.html b/dev/sidekick/Sidekick_smt_solver/index.html index bdca990b..71e14cb9 100644 --- a/dev/sidekick/Sidekick_smt_solver/index.html +++ b/dev/sidekick/Sidekick_smt_solver/index.html @@ -1,2 +1,2 @@ -Sidekick_smt_solver (sidekick.Sidekick_smt_solver)

Module Sidekick_smt_solver

Core of the SMT solver using Sidekick_sat

Sidekick_sat (in src/sat/) is a modular SAT solver in pure OCaml.

This builds a SMT solver on top of it.

module Sigs : sig ... end

Signature for the main SMT solver types.

module Model = Sidekick_model
module Model_builder : sig ... end

Model Builder.

module Registry : sig ... end

Registry to extract values

module Solver_internal : sig ... end

A view of the solver from a theory's point of view.

module Solver : sig ... end

Main solver type, user facing.

module Theory : sig ... end

Signatures for theory plugins

module Theory_id : sig ... end
module Preprocess : sig ... end

Preprocessor

module Find_foreign : sig ... end

Find foreign variables.

module Tracer : sig ... end

Tracer for SMT solvers.

module Trace_reader : sig ... end

Read trace

type theory = Theory.t
type solver = Solver.t
\ No newline at end of file +Sidekick_smt_solver (sidekick.Sidekick_smt_solver)

Module Sidekick_smt_solver

Core of the SMT solver using Sidekick_sat

Sidekick_sat (in src/sat/) is a modular SAT solver in pure OCaml.

This builds a SMT solver on top of it.

module Sigs : sig ... end

Signature for the main SMT solver types.

module Model_builder : sig ... end

Model Builder.

module Registry : sig ... end

Registry to extract values

module Solver_internal : sig ... end

A view of the solver from a theory's point of view.

module Solver : sig ... end

Main solver type, user facing.

module Model : sig ... end

SMT models.

module Theory : sig ... end

Signatures for theory plugins

module Theory_id : sig ... end
module Preprocess : sig ... end

Preprocessor

module Find_foreign : sig ... end

Find foreign variables.

module Tracer : sig ... end

Tracer for SMT solvers.

module Trace_reader : sig ... end

Read trace

type theory = Theory.t
type solver = Solver.t
\ No newline at end of file diff --git a/dev/sidekick/index.html b/dev/sidekick/index.html index eeaffcff..85d7622e 100644 --- a/dev/sidekick/index.html +++ b/dev/sidekick/index.html @@ -1,2 +1,2 @@ -index (sidekick.index)

sidekick index

Library sidekick.abstract-solver

The entry point of this library is the module: Sidekick_abstract_solver.

Library sidekick.arith

The entry point of this library is the module: Sidekick_arith.

Library sidekick.bencode

The entry point of this library is the module: Sidekick_bencode.

Library sidekick.cc

The entry point of this library is the module: Sidekick_cc.

Library sidekick.cc.plugin

The entry point of this library is the module: Sidekick_cc_plugin.

Library sidekick.core

The entry point of this library is the module: Sidekick_core.

Library sidekick.core-logic

The entry point of this library is the module: Sidekick_core_logic.

Library sidekick.drup

The entry point of this library is the module: Sidekick_drup.

Library sidekick.memtrace

The entry point of this library is the module: Sidekick_memtrace.

Library sidekick.mini-cc

The entry point of this library is the module: Sidekick_mini_cc.

Library sidekick.model

The entry point of this library is the module: Sidekick_model.

Library sidekick.proof

The entry point of this library is the module: Sidekick_proof.

Library sidekick.quip

The entry point of this library is the module: Sidekick_quip.

Library sidekick.sat

The entry point of this library is the module: Sidekick_sat.

Library sidekick.sigs

The entry point of this library is the module: Sidekick_sigs.

Library sidekick.simplex

The entry point of this library is the module: Sidekick_simplex.

Library sidekick.simplify

The entry point of this library is the module: Sidekick_simplify.

Library sidekick.smt-solver

The entry point of this library is the module: Sidekick_smt_solver.

Library sidekick.tef

The entry point of this library is the module: Sidekick_tef.

Library sidekick.th-bool-dyn

The entry point of this library is the module: Sidekick_th_bool_dyn.

Library sidekick.th-bool-static

The entry point of this library is the module: Sidekick_th_bool_static.

Library sidekick.th-cstor

The entry point of this library is the module: Sidekick_th_cstor.

Library sidekick.th-data

The entry point of this library is the module: Sidekick_th_data.

Library sidekick.th-lra

The entry point of this library is the module: Sidekick_th_lra.

Library sidekick.th-ty-unin

The entry point of this library is the module: Sidekick_th_ty_unin.

Library sidekick.trace

The entry point of this library is the module: Sidekick_trace.

Library sidekick.util

The entry point of this library is the module: Sidekick_util.

Library sidekick.zarith

The entry point of this library is the module: Sidekick_zarith.

\ No newline at end of file +index (sidekick.index)

sidekick index

Library sidekick.abstract-solver

The entry point of this library is the module: Sidekick_abstract_solver.

Library sidekick.arith

The entry point of this library is the module: Sidekick_arith.

Library sidekick.bencode

The entry point of this library is the module: Sidekick_bencode.

Library sidekick.cc

The entry point of this library is the module: Sidekick_cc.

Library sidekick.cc.plugin

The entry point of this library is the module: Sidekick_cc_plugin.

Library sidekick.core

The entry point of this library is the module: Sidekick_core.

Library sidekick.core-logic

The entry point of this library is the module: Sidekick_core_logic.

Library sidekick.drup

The entry point of this library is the module: Sidekick_drup.

Library sidekick.memtrace

The entry point of this library is the module: Sidekick_memtrace.

Library sidekick.mini-cc

The entry point of this library is the module: Sidekick_mini_cc.

Library sidekick.proof

The entry point of this library is the module: Sidekick_proof.

Library sidekick.quip

The entry point of this library is the module: Sidekick_quip.

Library sidekick.sat

The entry point of this library is the module: Sidekick_sat.

Library sidekick.sigs

The entry point of this library is the module: Sidekick_sigs.

Library sidekick.simplex

The entry point of this library is the module: Sidekick_simplex.

Library sidekick.simplify

The entry point of this library is the module: Sidekick_simplify.

Library sidekick.smt-solver

The entry point of this library is the module: Sidekick_smt_solver.

Library sidekick.tef

The entry point of this library is the module: Sidekick_tef.

Library sidekick.th-bool-dyn

The entry point of this library is the module: Sidekick_th_bool_dyn.

Library sidekick.th-bool-static

The entry point of this library is the module: Sidekick_th_bool_static.

Library sidekick.th-cstor

The entry point of this library is the module: Sidekick_th_cstor.

Library sidekick.th-data

The entry point of this library is the module: Sidekick_th_data.

Library sidekick.th-lra

The entry point of this library is the module: Sidekick_th_lra.

Library sidekick.th-ty-unin

The entry point of this library is the module: Sidekick_th_ty_unin.

Library sidekick.trace

The entry point of this library is the module: Sidekick_trace.

Library sidekick.util

The entry point of this library is the module: Sidekick_util.

Library sidekick.zarith

The entry point of this library is the module: Sidekick_zarith.

\ No newline at end of file