From 054fd84a0c25e399ce49713adc5acd9c7992426b Mon Sep 17 00:00:00 2001 From: c-cube Date: Mon, 20 Dec 2021 18:53:21 +0000 Subject: [PATCH] deploy: 5d2f8a1d3d668cb6b1f42c4c2c8132571ebe086a --- dev/sidekick-base/Sidekick_base_solver/Solver/index.html | 2 +- dev/sidekick-base/Sidekick_base_solver/Th_bool/A/S/index.html | 2 +- dev/sidekick-base/Sidekick_base_solver/Th_data/A/S/index.html | 2 +- dev/sidekick-base/Sidekick_base_solver/Th_lra/A/S/index.html | 2 +- dev/sidekick-bin/Sidekick_smtlib/Process/Solver/index.html | 2 +- .../Sidekick_arith_lra/Make/argument-1-A/S/index.html | 2 +- dev/sidekick/Sidekick_arith_lra/module-type-ARG/S/index.html | 2 +- dev/sidekick/Sidekick_arith_lra/module-type-S/A/S/index.html | 2 +- dev/sidekick/Sidekick_core/index.html | 2 +- dev/sidekick/Sidekick_core/module-type-SOLVER/index.html | 4 ++-- dev/sidekick/Sidekick_sat/Solver/Make_cdcl_t/index.html | 2 +- dev/sidekick/Sidekick_sat/Solver/Make_pure_sat/index.html | 2 +- .../Sidekick_sat/Solver_intf/module-type-S/index.html | 2 +- dev/sidekick/Sidekick_smt_solver/Make/index.html | 2 +- .../Sidekick_th_bool_static/Make/argument-1-A/S/index.html | 2 +- .../Sidekick_th_bool_static/module-type-ARG/S/index.html | 2 +- .../Sidekick_th_bool_static/module-type-S/A/S/index.html | 2 +- dev/sidekick/Sidekick_th_cstor/Make/argument-1-A/S/index.html | 2 +- dev/sidekick/Sidekick_th_cstor/module-type-ARG/S/index.html | 2 +- dev/sidekick/Sidekick_th_cstor/module-type-S/A/S/index.html | 2 +- dev/sidekick/Sidekick_th_data/Make/argument-1-A/S/index.html | 2 +- dev/sidekick/Sidekick_th_data/module-type-ARG/S/index.html | 2 +- dev/sidekick/Sidekick_th_data/module-type-S/A/S/index.html | 2 +- 23 files changed, 24 insertions(+), 24 deletions(-) diff --git a/dev/sidekick-base/Sidekick_base_solver/Solver/index.html b/dev/sidekick-base/Sidekick_base_solver/Solver/index.html index d2773e51..39fa9e37 100644 --- a/dev/sidekick-base/Sidekick_base_solver/Solver/index.html +++ b/dev/sidekick-base/Sidekick_base_solver/Solver/index.html @@ -2,4 +2,4 @@ Solver (sidekick-base.Sidekick_base_solver.Solver)

Module Sidekick_base_solver.Solver

SMT solver, obtained from Sidekick_smt_solver

module T : sig ... end
module Lit : sig ... end
type proof = Solver_arg.proof
type proof_step = Solver_arg.proof_step
module P : sig ... end
module Solver_internal : sig ... end
type solver = t
type term = T.Term.t
type ty = T.Ty.t
type lit = Lit.t
module type THEORY = sig ... end
type theory = (module THEORY)
type !'a theory_p = (module THEORY with type t = 'a)
val mk_theory : name:string -> create_and_setup:(Solver_internal.t -> 'th) -> ?push_level:('th -> unit) -> ?pop_levels:('th -> int -> unit) -> unit -> theory
module Model : sig ... end
module Unknown : sig ... end
val stats : t -> Sidekick_util.Stat.t
val tst : t -> T.Term.store
val ty_st : t -> T.Ty.store
val proof : t -> proof
val create : ?stat:Sidekick_util.Stat.t -> ?size:[ `Big | `Small | `Tiny ] -> proof:proof -> theories:theory list -> T.Term.store -> T.Ty.store -> unit -> t
val add_theory : t -> theory -> unit
val add_theory_p : t -> 'a theory_p -> 'a
val add_theory_l : t -> theory list -> unit
val mk_lit_t : t -> ?sign:bool -> term -> lit
val add_clause : t -> lit Sidekick_util.IArray.t -> proof_step -> unit
val add_clause_l : t -> lit list -> proof_step -> unit
val assert_terms : t -> term list -> unit
val assert_term : t -> term -> unit
type res = Sidekick_smt_solver.Make(Solver_arg).res =
| Sat of Model.t
| Unsat of {
unsat_core : unit -> lit Iter.t;
unsat_proof_step : unit -> proof_step option;
}
| Unknown of Unknown.t
val solve : ?on_exit:(unit -> unit) list -> ?check:bool -> ?on_progress:(t -> unit) -> -assumptions:lit list -> t -> res
val pp_stats : t CCFormat.printer
\ No newline at end of file +?should_stop:(t -> int -> bool) -> assumptions:lit list -> t -> res
val pp_stats : t CCFormat.printer
\ No newline at end of file diff --git a/dev/sidekick-base/Sidekick_base_solver/Th_bool/A/S/index.html b/dev/sidekick-base/Sidekick_base_solver/Th_bool/A/S/index.html index 578b4661..3fbbaede 100644 --- a/dev/sidekick-base/Sidekick_base_solver/Th_bool/A/S/index.html +++ b/dev/sidekick-base/Sidekick_base_solver/Th_bool/A/S/index.html @@ -2,4 +2,4 @@ S (sidekick-base.Sidekick_base_solver.Th_bool.A.S)

Module A.S

module T : sig ... end
module Lit : sig ... end
type proof = Solver_arg.proof
type proof_step = Solver_arg.proof_step
module P : sig ... end
module Solver_internal : sig ... end
type solver = t
type term = T.Term.t
type ty = T.Ty.t
type lit = Lit.t
module type THEORY = sig ... end
type theory = (module THEORY)
type !'a theory_p = (module THEORY with type t = 'a)
val mk_theory : name:string -> create_and_setup:(Solver_internal.t -> 'th) -> ?push_level:('th -> unit) -> ?pop_levels:('th -> int -> unit) -> unit -> theory
module Model : sig ... end
module Unknown : sig ... end
val stats : t -> Sidekick_util.Stat.t
val tst : t -> T.Term.store
val ty_st : t -> T.Ty.store
val proof : t -> proof
val create : ?stat:Sidekick_util.Stat.t -> ?size:[ `Big | `Small | `Tiny ] -> proof:proof -> theories:theory list -> T.Term.store -> T.Ty.store -> unit -> t
val add_theory : t -> theory -> unit
val add_theory_p : t -> 'a theory_p -> 'a
val add_theory_l : t -> theory list -> unit
val mk_lit_t : t -> ?sign:bool -> term -> lit
val add_clause : t -> lit Sidekick_util.IArray.t -> proof_step -> unit
val add_clause_l : t -> lit list -> proof_step -> unit
val assert_terms : t -> term list -> unit
val assert_term : t -> term -> unit
type res = Sidekick_smt_solver.Make(Solver_arg).res =
| Sat of Model.t
| Unsat of {
unsat_core : unit -> lit Iter.t;
unsat_proof_step : unit -> proof_step option;
}
| Unknown of Unknown.t
val solve : ?on_exit:(unit -> unit) list -> ?check:bool -> ?on_progress:(t -> unit) -> -assumptions:lit list -> t -> res
val pp_stats : t CCFormat.printer
\ No newline at end of file +?should_stop:(t -> int -> bool) -> assumptions:lit list -> t -> res
val pp_stats : t CCFormat.printer
\ No newline at end of file diff --git a/dev/sidekick-base/Sidekick_base_solver/Th_data/A/S/index.html b/dev/sidekick-base/Sidekick_base_solver/Th_data/A/S/index.html index 4287e604..f4fd1be0 100644 --- a/dev/sidekick-base/Sidekick_base_solver/Th_data/A/S/index.html +++ b/dev/sidekick-base/Sidekick_base_solver/Th_data/A/S/index.html @@ -2,4 +2,4 @@ S (sidekick-base.Sidekick_base_solver.Th_data.A.S)

Module A.S

module T : sig ... end
module Lit : sig ... end
type proof = Solver_arg.proof
type proof_step = Solver_arg.proof_step
module P : sig ... end
module Solver_internal : sig ... end
type solver = t
type term = T.Term.t
type ty = T.Ty.t
type lit = Lit.t
module type THEORY = sig ... end
type theory = (module THEORY)
type !'a theory_p = (module THEORY with type t = 'a)
val mk_theory : name:string -> create_and_setup:(Solver_internal.t -> 'th) -> ?push_level:('th -> unit) -> ?pop_levels:('th -> int -> unit) -> unit -> theory
module Model : sig ... end
module Unknown : sig ... end
val stats : t -> Sidekick_util.Stat.t
val tst : t -> T.Term.store
val ty_st : t -> T.Ty.store
val proof : t -> proof
val create : ?stat:Sidekick_util.Stat.t -> ?size:[ `Big | `Small | `Tiny ] -> proof:proof -> theories:theory list -> T.Term.store -> T.Ty.store -> unit -> t
val add_theory : t -> theory -> unit
val add_theory_p : t -> 'a theory_p -> 'a
val add_theory_l : t -> theory list -> unit
val mk_lit_t : t -> ?sign:bool -> term -> lit
val add_clause : t -> lit Sidekick_util.IArray.t -> proof_step -> unit
val add_clause_l : t -> lit list -> proof_step -> unit
val assert_terms : t -> term list -> unit
val assert_term : t -> term -> unit
type res = Sidekick_smt_solver.Make(Solver_arg).res =
| Sat of Model.t
| Unsat of {
unsat_core : unit -> lit Iter.t;
unsat_proof_step : unit -> proof_step option;
}
| Unknown of Unknown.t
val solve : ?on_exit:(unit -> unit) list -> ?check:bool -> ?on_progress:(t -> unit) -> -assumptions:lit list -> t -> res
val pp_stats : t CCFormat.printer
\ No newline at end of file +?should_stop:(t -> int -> bool) -> assumptions:lit list -> t -> res
val pp_stats : t CCFormat.printer
\ No newline at end of file diff --git a/dev/sidekick-base/Sidekick_base_solver/Th_lra/A/S/index.html b/dev/sidekick-base/Sidekick_base_solver/Th_lra/A/S/index.html index 611e7c17..e2ca1b04 100644 --- a/dev/sidekick-base/Sidekick_base_solver/Th_lra/A/S/index.html +++ b/dev/sidekick-base/Sidekick_base_solver/Th_lra/A/S/index.html @@ -2,4 +2,4 @@ S (sidekick-base.Sidekick_base_solver.Th_lra.A.S)

Module A.S

module T : sig ... end
module Lit : sig ... end
type proof = Solver_arg.proof
type proof_step = Solver_arg.proof_step
module P : sig ... end
module Solver_internal : sig ... end
type solver = t
type term = T.Term.t
type ty = T.Ty.t
type lit = Lit.t
module type THEORY = sig ... end
type theory = (module THEORY)
type !'a theory_p = (module THEORY with type t = 'a)
val mk_theory : name:string -> create_and_setup:(Solver_internal.t -> 'th) -> ?push_level:('th -> unit) -> ?pop_levels:('th -> int -> unit) -> unit -> theory
module Model : sig ... end
module Unknown : sig ... end
val stats : t -> Sidekick_util.Stat.t
val tst : t -> T.Term.store
val ty_st : t -> T.Ty.store
val proof : t -> proof
val create : ?stat:Sidekick_util.Stat.t -> ?size:[ `Big | `Small | `Tiny ] -> proof:proof -> theories:theory list -> T.Term.store -> T.Ty.store -> unit -> t
val add_theory : t -> theory -> unit
val add_theory_p : t -> 'a theory_p -> 'a
val add_theory_l : t -> theory list -> unit
val mk_lit_t : t -> ?sign:bool -> term -> lit
val add_clause : t -> lit Sidekick_util.IArray.t -> proof_step -> unit
val add_clause_l : t -> lit list -> proof_step -> unit
val assert_terms : t -> term list -> unit
val assert_term : t -> term -> unit
type res = Sidekick_smt_solver.Make(Solver_arg).res =
| Sat of Model.t
| Unsat of {
unsat_core : unit -> lit Iter.t;
unsat_proof_step : unit -> proof_step option;
}
| Unknown of Unknown.t
val solve : ?on_exit:(unit -> unit) list -> ?check:bool -> ?on_progress:(t -> unit) -> -assumptions:lit list -> t -> res
val pp_stats : t CCFormat.printer
\ No newline at end of file +?should_stop:(t -> int -> bool) -> assumptions:lit list -> t -> res
val pp_stats : t CCFormat.printer
\ No newline at end of file diff --git a/dev/sidekick-bin/Sidekick_smtlib/Process/Solver/index.html b/dev/sidekick-bin/Sidekick_smtlib/Process/Solver/index.html index 80de242b..6628ae2b 100644 --- a/dev/sidekick-bin/Sidekick_smtlib/Process/Solver/index.html +++ b/dev/sidekick-bin/Sidekick_smtlib/Process/Solver/index.html @@ -2,4 +2,4 @@ Solver (sidekick-bin.Sidekick_smtlib.Process.Solver)

Module Process.Solver

module Lit : Sidekick_core.LIT with module T = T
type proof_step
module P : Sidekick_core.PROOF with type lit = Lit.t and type t = proof and type proof_step = proof_step and type term = T.Term.t
module Solver_internal : Sidekick_core.SOLVER_INTERNAL with module T = T and module Lit = Lit and type proof = proof and type proof_step = proof_step and module P = P

Internal solver, available to theories.

type t

The solver's state.

type solver = t
type term = T.Term.t
type ty = T.Ty.t
type lit = Lit.t
module type THEORY = sig ... end
type theory = (module THEORY)

A theory that can be used for this particular solver.

type 'a theory_p = (module THEORY with type t = 'a)

A theory that can be used for this particular solver, with state of type 'a.

val mk_theory : name:string -> create_and_setup:(Solver_internal.t -> 'th) -> ?push_level:('th -> unit) -> ?pop_levels:('th -> int -> unit) -> unit -> theory

Helper to create a theory.

module Model : sig ... end

Models

module Unknown : sig ... end

Main API

val stats : t -> Sidekick_util.Stat.t
val tst : t -> T.Term.store
val ty_st : t -> T.Ty.store
val proof : t -> proof
val create : ?stat:Sidekick_util.Stat.t -> ?size:[ `Big | `Tiny | `Small ] -> proof:proof -> theories:theory list -> T.Term.store -> T.Ty.store -> unit -> t

Create a new solver.

It needs a term state and a type state to manipulate terms and types. All terms and types interacting with this solver will need to come from these exact states.

  • parameter store_proof

    if true, proofs from the SAT solver and theories are retained and potentially accessible after solve returns UNSAT.

  • parameter size

    influences the size of initial allocations.

  • parameter theories

    theories to load from the start. Other theories can be added using add_theory.

val add_theory : t -> theory -> 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 list -> unit
val mk_lit_t : t -> ?sign:bool -> term -> 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 -> lit Sidekick_util.IArray.t -> proof_step -> 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 -> lit list -> proof_step -> unit

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

val assert_terms : t -> term list -> unit

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

val assert_term : t -> term -> unit

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

type res =
| Sat of Model.t(*

Satisfiable

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

Unsat core (subset of assumptions), or empty

*)
unsat_proof_step : unit -> proof_step 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 : ?on_exit:(unit -> unit) list -> ?check:bool -> ?on_progress:(t -> unit) -> -assumptions:lit list -> t -> res

solve s checks the satisfiability of the clauses added so far to s.

  • parameter check

    if true, the model is checked before returning.

  • parameter on_progress

    called regularly during solving.

  • parameter assumptions

    a set of atoms held to be true. The unsat core, if any, will be a subset of assumptions.

  • parameter on_exit

    functions to be run before this returns

val pp_stats : t CCFormat.printer

Print some statistics. What it prints exactly is unspecified.

\ No newline at end of file +?should_stop:(t -> int -> bool) -> assumptions:lit list -> t -> res

solve s checks the satisfiability of the clauses added so far to s.

val pp_stats : t CCFormat.printer

Print some statistics. What it prints exactly is unspecified.

\ No newline at end of file diff --git a/dev/sidekick/Sidekick_arith_lra/Make/argument-1-A/S/index.html b/dev/sidekick/Sidekick_arith_lra/Make/argument-1-A/S/index.html index c23d0808..b89ae274 100644 --- a/dev/sidekick/Sidekick_arith_lra/Make/argument-1-A/S/index.html +++ b/dev/sidekick/Sidekick_arith_lra/Make/argument-1-A/S/index.html @@ -2,4 +2,4 @@ S (sidekick.Sidekick_arith_lra.Make.1-A.S)

Module 1-A.S

module Lit : Sidekick_core.LIT with module T = T
type proof
type proof_step
module P : Sidekick_core.PROOF with type lit = Lit.t and type t = proof and type proof_step = proof_step and type term = T.Term.t
module Solver_internal : Sidekick_core.SOLVER_INTERNAL with module T = T and module Lit = Lit and type proof = proof and type proof_step = proof_step and module P = P

Internal solver, available to theories.

type t

The solver's state.

type solver = t
type term = T.Term.t
type ty = T.Ty.t
type lit = Lit.t
module type THEORY = sig ... end
type theory = (module THEORY)

A theory that can be used for this particular solver.

type 'a theory_p = (module THEORY with type t = 'a)

A theory that can be used for this particular solver, with state of type 'a.

val mk_theory : name:string -> create_and_setup:(Solver_internal.t -> 'th) -> ?push_level:('th -> unit) -> ?pop_levels:('th -> int -> unit) -> unit -> theory

Helper to create a theory.

module Model : sig ... end

Models

module Unknown : sig ... end

Main API

val stats : t -> Sidekick_util.Stat.t
val tst : t -> T.Term.store
val ty_st : t -> T.Ty.store
val proof : t -> proof
val create : ?stat:Sidekick_util.Stat.t -> ?size:[ `Big | `Tiny | `Small ] -> proof:proof -> theories:theory list -> T.Term.store -> T.Ty.store -> unit -> t

Create a new solver.

It needs a term state and a type state to manipulate terms and types. All terms and types interacting with this solver will need to come from these exact states.

  • parameter store_proof

    if true, proofs from the SAT solver and theories are retained and potentially accessible after solve returns UNSAT.

  • parameter size

    influences the size of initial allocations.

  • parameter theories

    theories to load from the start. Other theories can be added using add_theory.

val add_theory : t -> theory -> 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 list -> unit
val mk_lit_t : t -> ?sign:bool -> term -> 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 -> lit Sidekick_util.IArray.t -> proof_step -> 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 -> lit list -> proof_step -> unit

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

val assert_terms : t -> term list -> unit

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

val assert_term : t -> term -> unit

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

type res =
| Sat of Model.t(*

Satisfiable

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

Unsat core (subset of assumptions), or empty

*)
unsat_proof_step : unit -> proof_step 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 : ?on_exit:(unit -> unit) list -> ?check:bool -> ?on_progress:(t -> unit) -> -assumptions:lit list -> t -> res

solve s checks the satisfiability of the clauses added so far to s.

  • parameter check

    if true, the model is checked before returning.

  • parameter on_progress

    called regularly during solving.

  • parameter assumptions

    a set of atoms held to be true. The unsat core, if any, will be a subset of assumptions.

  • parameter on_exit

    functions to be run before this returns

val pp_stats : t CCFormat.printer

Print some statistics. What it prints exactly is unspecified.

\ No newline at end of file +?should_stop:(t -> int -> bool) -> assumptions:lit list -> t -> res

solve s checks the satisfiability of the clauses added so far to s.

val pp_stats : t CCFormat.printer

Print some statistics. What it prints exactly is unspecified.

\ No newline at end of file diff --git a/dev/sidekick/Sidekick_arith_lra/module-type-ARG/S/index.html b/dev/sidekick/Sidekick_arith_lra/module-type-ARG/S/index.html index 3a3a3336..12876fed 100644 --- a/dev/sidekick/Sidekick_arith_lra/module-type-ARG/S/index.html +++ b/dev/sidekick/Sidekick_arith_lra/module-type-ARG/S/index.html @@ -2,4 +2,4 @@ S (sidekick.Sidekick_arith_lra.ARG.S)

Module ARG.S

module Lit : Sidekick_core.LIT with module T = T
type proof
type proof_step
module P : Sidekick_core.PROOF with type lit = Lit.t and type t = proof and type proof_step = proof_step and type term = T.Term.t
module Solver_internal : Sidekick_core.SOLVER_INTERNAL with module T = T and module Lit = Lit and type proof = proof and type proof_step = proof_step and module P = P

Internal solver, available to theories.

type t

The solver's state.

type solver = t
type term = T.Term.t
type ty = T.Ty.t
type lit = Lit.t
module type THEORY = sig ... end
type theory = (module THEORY)

A theory that can be used for this particular solver.

type 'a theory_p = (module THEORY with type t = 'a)

A theory that can be used for this particular solver, with state of type 'a.

val mk_theory : name:string -> create_and_setup:(Solver_internal.t -> 'th) -> ?push_level:('th -> unit) -> ?pop_levels:('th -> int -> unit) -> unit -> theory

Helper to create a theory.

module Model : sig ... end

Models

module Unknown : sig ... end

Main API

val stats : t -> Sidekick_util.Stat.t
val tst : t -> T.Term.store
val ty_st : t -> T.Ty.store
val proof : t -> proof
val create : ?stat:Sidekick_util.Stat.t -> ?size:[ `Big | `Tiny | `Small ] -> proof:proof -> theories:theory list -> T.Term.store -> T.Ty.store -> unit -> t

Create a new solver.

It needs a term state and a type state to manipulate terms and types. All terms and types interacting with this solver will need to come from these exact states.

  • parameter store_proof

    if true, proofs from the SAT solver and theories are retained and potentially accessible after solve returns UNSAT.

  • parameter size

    influences the size of initial allocations.

  • parameter theories

    theories to load from the start. Other theories can be added using add_theory.

val add_theory : t -> theory -> 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 list -> unit
val mk_lit_t : t -> ?sign:bool -> term -> 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 -> lit Sidekick_util.IArray.t -> proof_step -> 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 -> lit list -> proof_step -> unit

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

val assert_terms : t -> term list -> unit

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

val assert_term : t -> term -> unit

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

type res =
| Sat of Model.t(*

Satisfiable

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

Unsat core (subset of assumptions), or empty

*)
unsat_proof_step : unit -> proof_step 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 : ?on_exit:(unit -> unit) list -> ?check:bool -> ?on_progress:(t -> unit) -> -assumptions:lit list -> t -> res

solve s checks the satisfiability of the clauses added so far to s.

  • parameter check

    if true, the model is checked before returning.

  • parameter on_progress

    called regularly during solving.

  • parameter assumptions

    a set of atoms held to be true. The unsat core, if any, will be a subset of assumptions.

  • parameter on_exit

    functions to be run before this returns

val pp_stats : t CCFormat.printer

Print some statistics. What it prints exactly is unspecified.

\ No newline at end of file +?should_stop:(t -> int -> bool) -> assumptions:lit list -> t -> res

solve s checks the satisfiability of the clauses added so far to s.

val pp_stats : t CCFormat.printer

Print some statistics. What it prints exactly is unspecified.

\ No newline at end of file diff --git a/dev/sidekick/Sidekick_arith_lra/module-type-S/A/S/index.html b/dev/sidekick/Sidekick_arith_lra/module-type-S/A/S/index.html index 72739a74..0fe07c71 100644 --- a/dev/sidekick/Sidekick_arith_lra/module-type-S/A/S/index.html +++ b/dev/sidekick/Sidekick_arith_lra/module-type-S/A/S/index.html @@ -2,4 +2,4 @@ S (sidekick.Sidekick_arith_lra.S.A.S)

Module A.S

module Lit : Sidekick_core.LIT with module T = T
type proof
type proof_step
module P : Sidekick_core.PROOF with type lit = Lit.t and type t = proof and type proof_step = proof_step and type term = T.Term.t
module Solver_internal : Sidekick_core.SOLVER_INTERNAL with module T = T and module Lit = Lit and type proof = proof and type proof_step = proof_step and module P = P

Internal solver, available to theories.

type t

The solver's state.

type solver = t
type term = T.Term.t
type ty = T.Ty.t
type lit = Lit.t
module type THEORY = sig ... end
type theory = (module THEORY)

A theory that can be used for this particular solver.

type 'a theory_p = (module THEORY with type t = 'a)

A theory that can be used for this particular solver, with state of type 'a.

val mk_theory : name:string -> create_and_setup:(Solver_internal.t -> 'th) -> ?push_level:('th -> unit) -> ?pop_levels:('th -> int -> unit) -> unit -> theory

Helper to create a theory.

module Model : sig ... end

Models

module Unknown : sig ... end

Main API

val stats : t -> Sidekick_util.Stat.t
val tst : t -> T.Term.store
val ty_st : t -> T.Ty.store
val proof : t -> proof
val create : ?stat:Sidekick_util.Stat.t -> ?size:[ `Big | `Tiny | `Small ] -> proof:proof -> theories:theory list -> T.Term.store -> T.Ty.store -> unit -> t

Create a new solver.

It needs a term state and a type state to manipulate terms and types. All terms and types interacting with this solver will need to come from these exact states.

  • parameter store_proof

    if true, proofs from the SAT solver and theories are retained and potentially accessible after solve returns UNSAT.

  • parameter size

    influences the size of initial allocations.

  • parameter theories

    theories to load from the start. Other theories can be added using add_theory.

val add_theory : t -> theory -> 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 list -> unit
val mk_lit_t : t -> ?sign:bool -> term -> 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 -> lit Sidekick_util.IArray.t -> proof_step -> 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 -> lit list -> proof_step -> unit

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

val assert_terms : t -> term list -> unit

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

val assert_term : t -> term -> unit

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

type res =
| Sat of Model.t(*

Satisfiable

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

Unsat core (subset of assumptions), or empty

*)
unsat_proof_step : unit -> proof_step 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 : ?on_exit:(unit -> unit) list -> ?check:bool -> ?on_progress:(t -> unit) -> -assumptions:lit list -> t -> res

solve s checks the satisfiability of the clauses added so far to s.

  • parameter check

    if true, the model is checked before returning.

  • parameter on_progress

    called regularly during solving.

  • parameter assumptions

    a set of atoms held to be true. The unsat core, if any, will be a subset of assumptions.

  • parameter on_exit

    functions to be run before this returns

val pp_stats : t CCFormat.printer

Print some statistics. What it prints exactly is unspecified.

\ No newline at end of file +?should_stop:(t -> int -> bool) -> assumptions:lit list -> t -> res

solve s checks the satisfiability of the clauses added so far to s.

val pp_stats : t CCFormat.printer

Print some statistics. What it prints exactly is unspecified.

\ No newline at end of file diff --git a/dev/sidekick/Sidekick_core/index.html b/dev/sidekick/Sidekick_core/index.html index 9159dc67..74a067a9 100644 --- a/dev/sidekick/Sidekick_core/index.html +++ b/dev/sidekick/Sidekick_core/index.html @@ -1,2 +1,2 @@ -Sidekick_core (sidekick.Sidekick_core)

Module Sidekick_core

Main Signatures

Theories and concrete solvers rely on an environment that defines several important types:

In this module we define most of the main signatures used throughout Sidekick.

module Fmt = CCFormat
module CC_view : sig ... end

View terms through the lens of the Congruence Closure

module type TERM = sig ... end

Main representation of Terms and Types

module type CC_PROOF = sig ... end

Proofs for the congruence closure

module type SAT_PROOF = sig ... end

Signature for SAT-solver proof emission.

module type PROOF = sig ... end

Proofs of unsatisfiability.

module type LIT = sig ... end

Literals

module type CC_ACTIONS = sig ... end

Actions provided to the congruence closure.

module type CC_ARG = sig ... end

Arguments to a congruence closure's implementation

module type CC_S = sig ... end

Main congruence closure signature.

module type SOLVER_INTERNAL = sig ... end

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

module type SOLVER = sig ... end

User facing view of the solver

module type MONOID_ARG = sig ... end

Helper for the congruence closure

module Monoid_of_repr (M : MONOID_ARG) : sig ... end

State for a per-equivalence-class monoid.

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

Module Sidekick_core

Main Signatures

Theories and concrete solvers rely on an environment that defines several important types:

In this module we define most of the main signatures used throughout Sidekick.

module Fmt = CCFormat
module CC_view : sig ... end

View terms through the lens of the Congruence Closure

module type TERM = sig ... end

Main representation of Terms and Types

module type CC_PROOF = sig ... end

Proofs for the congruence closure

module type SAT_PROOF = sig ... end

Signature for SAT-solver proof emission.

module type PROOF = sig ... end

Proofs of unsatisfiability.

module type LIT = sig ... end

Literals

module type CC_ACTIONS = sig ... end

Actions provided to the congruence closure.

module type CC_ARG = sig ... end

Arguments to a congruence closure's implementation

module type CC_S = sig ... end

Main congruence closure signature.

module type SOLVER_INTERNAL = sig ... end

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

module type SOLVER = sig ... end

User facing view of the solver.

module type MONOID_ARG = sig ... end

Helper for the congruence closure

module Monoid_of_repr (M : MONOID_ARG) : sig ... end

State for a per-equivalence-class monoid.

\ No newline at end of file diff --git a/dev/sidekick/Sidekick_core/module-type-SOLVER/index.html b/dev/sidekick/Sidekick_core/module-type-SOLVER/index.html index 3606146a..0c8ec80a 100644 --- a/dev/sidekick/Sidekick_core/module-type-SOLVER/index.html +++ b/dev/sidekick/Sidekick_core/module-type-SOLVER/index.html @@ -1,5 +1,5 @@ -SOLVER (sidekick.Sidekick_core.SOLVER)

Module type Sidekick_core.SOLVER

User facing view of the solver

This is the solver a user of sidekick can see, after instantiating everything. The user can add some theories, clauses, etc. and asks the solver to check satisfiability.

Theory implementors will mostly interact with SOLVER_INTERNAL.

module T : TERM
module Lit : LIT with module T = T
type proof
type proof_step
module P : PROOF with type lit = Lit.t and type t = proof and type proof_step = proof_step and type term = T.Term.t
module Solver_internal : SOLVER_INTERNAL with module T = T and module Lit = Lit and type proof = proof and type proof_step = proof_step and module P = P

Internal solver, available to theories.

type t

The solver's state.

type solver = t
type term = T.Term.t
type ty = T.Ty.t
type lit = Lit.t
module type THEORY = sig ... end
type theory = (module THEORY)

A theory that can be used for this particular solver.

type 'a theory_p = (module THEORY with type t = 'a)

A theory that can be used for this particular solver, with state of type 'a.

val mk_theory : name:string -> create_and_setup:(Solver_internal.t -> 'th) -> +SOLVER (sidekick.Sidekick_core.SOLVER)

Module type Sidekick_core.SOLVER

User facing view of the solver.

This is the solver a user of sidekick can see, after instantiating everything. The user can add some theories, clauses, etc. and asks the solver to check satisfiability.

Theory implementors will mostly interact with SOLVER_INTERNAL.

module T : TERM
module Lit : LIT with module T = T
type proof
type proof_step
module P : PROOF with type lit = Lit.t and type t = proof and type proof_step = proof_step and type term = T.Term.t
module Solver_internal : SOLVER_INTERNAL with module T = T and module Lit = Lit and type proof = proof and type proof_step = proof_step and module P = P

Internal solver, available to theories.

type t

The solver's state.

type solver = t
type term = T.Term.t
type ty = T.Ty.t
type lit = Lit.t
module type THEORY = sig ... end
type theory = (module THEORY)

A theory that can be used for this particular solver.

type 'a theory_p = (module THEORY with type t = 'a)

A theory that can be used for this particular solver, with state of type 'a.

val mk_theory : name:string -> create_and_setup:(Solver_internal.t -> 'th) -> ?push_level:('th -> unit) -> ?pop_levels:('th -> int -> unit) -> unit -> theory

Helper to create a theory.

module Model : sig ... end

Models

module Unknown : sig ... end

Main API

val stats : t -> Sidekick_util.Stat.t
val tst : t -> T.Term.store
val ty_st : t -> T.Ty.store
val proof : t -> proof
val create : ?stat:Sidekick_util.Stat.t -> ?size:[ `Big | `Tiny | `Small ] -> proof:proof -> theories:theory list -> T.Term.store -> T.Ty.store -> unit -> t

Create a new solver.

It needs a term state and a type state to manipulate terms and types. All terms and types interacting with this solver will need to come from these exact states.

  • parameter store_proof

    if true, proofs from the SAT solver and theories are retained and potentially accessible after solve returns UNSAT.

  • parameter size

    influences the size of initial allocations.

  • parameter theories

    theories to load from the start. Other theories can be added using add_theory.

val add_theory : t -> theory -> 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 list -> unit
val mk_lit_t : t -> ?sign:bool -> term -> 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 -> lit Sidekick_util.IArray.t -> proof_step -> 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 -> lit list -> proof_step -> unit

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

val assert_terms : t -> term list -> unit

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

val assert_term : t -> term -> unit

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

type res =
| Sat of Model.t(*

Satisfiable

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

Unsat core (subset of assumptions), or empty

*)
unsat_proof_step : unit -> proof_step 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 : ?on_exit:(unit -> unit) list -> ?check:bool -> ?on_progress:(t -> unit) -> -assumptions:lit list -> t -> res

solve s checks the satisfiability of the clauses added so far to s.

  • parameter check

    if true, the model is checked before returning.

  • parameter on_progress

    called regularly during solving.

  • parameter assumptions

    a set of atoms held to be true. The unsat core, if any, will be a subset of assumptions.

  • parameter on_exit

    functions to be run before this returns

val pp_stats : t CCFormat.printer

Print some statistics. What it prints exactly is unspecified.

\ No newline at end of file +?should_stop:(t -> int -> bool) -> assumptions:lit list -> t -> res

solve s checks the satisfiability of the clauses added so far to s.

  • parameter check

    if true, the model is checked before returning.

  • parameter on_progress

    called regularly during solving.

  • parameter assumptions

    a set of atoms held to be true. The unsat core, if any, will be a subset of assumptions.

  • parameter should_stop

    a callback regularly called with the solver, and with a number of "steps" done since last call. The exact notion of step is not defined, but is guaranteed to increase regularly. The function should return true if it judges solving must stop (returning Unknown), false if solving can proceed.

  • parameter on_exit

    functions to be run before this returns

val pp_stats : t CCFormat.printer

Print some statistics. What it prints exactly is unspecified.

\ No newline at end of file diff --git a/dev/sidekick/Sidekick_sat/Solver/Make_cdcl_t/index.html b/dev/sidekick/Sidekick_sat/Solver/Make_cdcl_t/index.html index b5fac6a5..26afe508 100644 --- a/dev/sidekick/Sidekick_sat/Solver/Make_cdcl_t/index.html +++ b/dev/sidekick/Sidekick_sat/Solver/Make_cdcl_t/index.html @@ -1,4 +1,4 @@ Make_cdcl_t (sidekick.Sidekick_sat.Solver.Make_cdcl_t)

Module Solver.Make_cdcl_t

Parameters

Signature

Internal modules

These are the internal modules used, you should probably not use them if you're not familiar with the internals of mSAT.

type lit = Th.lit

literals

module Lit = Th.Lit
type clause
type clause_pool_id

Pool of clauses, with its own lifetime management

type theory = Th.t
type proof = Th.proof

A representation of a full proof

type proof_step = Th.proof_step
type solver

The main solver type.

type store

Stores atoms, clauses, etc.

module Clause : sig ... end
module Proof = Th.Proof

A module to manipulate proofs.

type t = solver

Main solver type, containing all state for solving.

val create : ?on_conflict:(t -> Clause.t -> unit) -> ?on_decision:(t -> lit -> unit) -> ?on_learnt:(t -> Clause.t -> unit) -> ?on_gc:(t -> lit array -> unit) -> ?stat:Sidekick_util.Stat.t -> -?size:[ `Tiny | `Small | `Big ] -> proof:Proof.t -> theory -> t

Create new solver

  • parameter theory

    the theory

  • parameter the

    proof

  • parameter size

    the initial size of internal data structures. The bigger, the faster, but also the more RAM it uses.

val theory : t -> theory

Access the theory state

val store : t -> store

Store for the solver

val stat : t -> Sidekick_util.Stat.t

Statistics

val proof : t -> proof

Access the inner proof

Clause Pools

Clause pools.

A clause pool holds/owns a set of clauses, and is responsible for managing their lifetime. We only expose an id, not a private type.

val clause_pool_descr : t -> clause_pool_id -> string
val new_clause_pool_gc_fixed_size : descr:string -> size:int -> t -> clause_pool_id

Allocate a new clause pool that GC's its clauses when its size goes above size. It keeps half of the clauses.

Types

type res =
| Sat of lit Solver_intf.sat_state(*

Returned when the solver reaches SAT, with a model

*)
| Unsat of (lit, clause, proof_step) Solver_intf.unsat_state(*

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 -> lit 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 -> lit list -> proof_step -> unit

Lower level addition of clauses

val add_clause_a : t -> lit array -> proof_step -> unit

Lower level addition of clauses

val add_input_clause : t -> lit list -> unit

Like add_clause but with the justification of being an input clause

val add_input_clause_a : t -> lit array -> unit

Like add_clause_a but with justification of being an input clause

val add_clause_in_pool : t -> pool:clause_pool_id -> lit list -> proof_step -> unit

Like add_clause but using a specific clause pool

val add_clause_a_in_pool : t -> pool:clause_pool_id -> lit array -> proof_step -> unit

Like add_clause_a but using a specific clause pool

val solve : ?assumptions:lit list -> t -> res

Try and solves the current set of clauses.

  • parameter assumptions

    additional atomic assumptions to be temporarily added. The assumptions are just used for this call to solve, they are not saved in the solver's state.

val add_lit : t -> ?default_pol:bool -> lit -> unit

Ensure the SAT solver handles this particular literal, ie add a boolean variable for it if it's not already there.

val set_default_pol : t -> lit -> bool -> unit

Set default polarity for the given boolean variable. Sign of the literal is ignored.

val true_at_level0 : t -> lit -> bool

true_at_level0 a returns true if a was proved at level0, i.e. it must hold in all models

val eval_lit : t -> lit -> Solver_intf.lbool

Evaluate atom in current state

\ No newline at end of file +?size:[ `Tiny | `Small | `Big ] -> proof:Proof.t -> theory -> t

Create new solver

val theory : t -> theory

Access the theory state

val store : t -> store

Store for the solver

val stat : t -> Sidekick_util.Stat.t

Statistics

val proof : t -> proof

Access the inner proof

Clause Pools

Clause pools.

A clause pool holds/owns a set of clauses, and is responsible for managing their lifetime. We only expose an id, not a private type.

val clause_pool_descr : t -> clause_pool_id -> string
val new_clause_pool_gc_fixed_size : descr:string -> size:int -> t -> clause_pool_id

Allocate a new clause pool that GC's its clauses when its size goes above size. It keeps half of the clauses.

Types

type res =
| Sat of lit Solver_intf.sat_state(*

Returned when the solver reaches SAT, with a model

*)
| Unsat of (lit, clause, proof_step) Solver_intf.unsat_state(*

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 -> lit 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 -> lit list -> proof_step -> unit

Lower level addition of clauses

val add_clause_a : t -> lit array -> proof_step -> unit

Lower level addition of clauses

val add_input_clause : t -> lit list -> unit

Like add_clause but with the justification of being an input clause

val add_input_clause_a : t -> lit array -> unit

Like add_clause_a but with justification of being an input clause

val add_clause_in_pool : t -> pool:clause_pool_id -> lit list -> proof_step -> unit

Like add_clause but using a specific clause pool

val add_clause_a_in_pool : t -> pool:clause_pool_id -> lit array -> proof_step -> unit

Like add_clause_a but using a specific clause pool

val solve : ?on_progress:(unit -> unit) -> ?assumptions:lit list -> t -> res

Try and solves the current set of clauses.

  • parameter assumptions

    additional atomic assumptions to be temporarily added. The assumptions are just used for this call to solve, they are not saved in the solver's state.

  • parameter on_progress

    regularly called during solving

val add_lit : t -> ?default_pol:bool -> lit -> unit

Ensure the SAT solver handles this particular literal, ie add a boolean variable for it if it's not already there.

val set_default_pol : t -> lit -> bool -> unit

Set default polarity for the given boolean variable. Sign of the literal is ignored.

val true_at_level0 : t -> lit -> bool

true_at_level0 a returns true if a was proved at level0, i.e. it must hold in all models

val eval_lit : t -> lit -> Solver_intf.lbool

Evaluate atom in current state

\ No newline at end of file diff --git a/dev/sidekick/Sidekick_sat/Solver/Make_pure_sat/index.html b/dev/sidekick/Sidekick_sat/Solver/Make_pure_sat/index.html index b31b6078..8d71fde7 100644 --- a/dev/sidekick/Sidekick_sat/Solver/Make_pure_sat/index.html +++ b/dev/sidekick/Sidekick_sat/Solver/Make_pure_sat/index.html @@ -1,4 +1,4 @@ Make_pure_sat (sidekick.Sidekick_sat.Solver.Make_pure_sat)

Module Solver.Make_pure_sat

Parameters

Signature

Internal modules

These are the internal modules used, you should probably not use them if you're not familiar with the internals of mSAT.

type lit = Th.lit

literals

module Lit = Th.Lit
type clause
type clause_pool_id

Pool of clauses, with its own lifetime management

type theory = unit
type proof = Th.proof

A representation of a full proof

type proof_step = Th.proof_step
type solver

The main solver type.

type store

Stores atoms, clauses, etc.

module Clause : sig ... end
module Proof = Th.Proof

A module to manipulate proofs.

type t = solver

Main solver type, containing all state for solving.

val create : ?on_conflict:(t -> Clause.t -> unit) -> ?on_decision:(t -> lit -> unit) -> ?on_learnt:(t -> Clause.t -> unit) -> ?on_gc:(t -> lit array -> unit) -> ?stat:Sidekick_util.Stat.t -> -?size:[ `Tiny | `Small | `Big ] -> proof:Proof.t -> theory -> t

Create new solver

  • parameter theory

    the theory

  • parameter the

    proof

  • parameter size

    the initial size of internal data structures. The bigger, the faster, but also the more RAM it uses.

val theory : t -> theory

Access the theory state

val store : t -> store

Store for the solver

val stat : t -> Sidekick_util.Stat.t

Statistics

val proof : t -> proof

Access the inner proof

Clause Pools

Clause pools.

A clause pool holds/owns a set of clauses, and is responsible for managing their lifetime. We only expose an id, not a private type.

val clause_pool_descr : t -> clause_pool_id -> string
val new_clause_pool_gc_fixed_size : descr:string -> size:int -> t -> clause_pool_id

Allocate a new clause pool that GC's its clauses when its size goes above size. It keeps half of the clauses.

Types

type res =
| Sat of lit Solver_intf.sat_state(*

Returned when the solver reaches SAT, with a model

*)
| Unsat of (lit, clause, proof_step) Solver_intf.unsat_state(*

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 -> lit 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 -> lit list -> proof_step -> unit

Lower level addition of clauses

val add_clause_a : t -> lit array -> proof_step -> unit

Lower level addition of clauses

val add_input_clause : t -> lit list -> unit

Like add_clause but with the justification of being an input clause

val add_input_clause_a : t -> lit array -> unit

Like add_clause_a but with justification of being an input clause

val add_clause_in_pool : t -> pool:clause_pool_id -> lit list -> proof_step -> unit

Like add_clause but using a specific clause pool

val add_clause_a_in_pool : t -> pool:clause_pool_id -> lit array -> proof_step -> unit

Like add_clause_a but using a specific clause pool

val solve : ?assumptions:lit list -> t -> res

Try and solves the current set of clauses.

  • parameter assumptions

    additional atomic assumptions to be temporarily added. The assumptions are just used for this call to solve, they are not saved in the solver's state.

val add_lit : t -> ?default_pol:bool -> lit -> unit

Ensure the SAT solver handles this particular literal, ie add a boolean variable for it if it's not already there.

val set_default_pol : t -> lit -> bool -> unit

Set default polarity for the given boolean variable. Sign of the literal is ignored.

val true_at_level0 : t -> lit -> bool

true_at_level0 a returns true if a was proved at level0, i.e. it must hold in all models

val eval_lit : t -> lit -> Solver_intf.lbool

Evaluate atom in current state

\ No newline at end of file +?size:[ `Tiny | `Small | `Big ] -> proof:Proof.t -> theory -> t

Create new solver

val theory : t -> theory

Access the theory state

val store : t -> store

Store for the solver

val stat : t -> Sidekick_util.Stat.t

Statistics

val proof : t -> proof

Access the inner proof

Clause Pools

Clause pools.

A clause pool holds/owns a set of clauses, and is responsible for managing their lifetime. We only expose an id, not a private type.

val clause_pool_descr : t -> clause_pool_id -> string
val new_clause_pool_gc_fixed_size : descr:string -> size:int -> t -> clause_pool_id

Allocate a new clause pool that GC's its clauses when its size goes above size. It keeps half of the clauses.

Types

type res =
| Sat of lit Solver_intf.sat_state(*

Returned when the solver reaches SAT, with a model

*)
| Unsat of (lit, clause, proof_step) Solver_intf.unsat_state(*

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 -> lit 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 -> lit list -> proof_step -> unit

Lower level addition of clauses

val add_clause_a : t -> lit array -> proof_step -> unit

Lower level addition of clauses

val add_input_clause : t -> lit list -> unit

Like add_clause but with the justification of being an input clause

val add_input_clause_a : t -> lit array -> unit

Like add_clause_a but with justification of being an input clause

val add_clause_in_pool : t -> pool:clause_pool_id -> lit list -> proof_step -> unit

Like add_clause but using a specific clause pool

val add_clause_a_in_pool : t -> pool:clause_pool_id -> lit array -> proof_step -> unit

Like add_clause_a but using a specific clause pool

val solve : ?on_progress:(unit -> unit) -> ?assumptions:lit list -> t -> res

Try and solves the current set of clauses.

  • parameter assumptions

    additional atomic assumptions to be temporarily added. The assumptions are just used for this call to solve, they are not saved in the solver's state.

  • parameter on_progress

    regularly called during solving

val add_lit : t -> ?default_pol:bool -> lit -> unit

Ensure the SAT solver handles this particular literal, ie add a boolean variable for it if it's not already there.

val set_default_pol : t -> lit -> bool -> unit

Set default polarity for the given boolean variable. Sign of the literal is ignored.

val true_at_level0 : t -> lit -> bool

true_at_level0 a returns true if a was proved at level0, i.e. it must hold in all models

val eval_lit : t -> lit -> Solver_intf.lbool

Evaluate atom in current state

\ No newline at end of file diff --git a/dev/sidekick/Sidekick_sat/Solver_intf/module-type-S/index.html b/dev/sidekick/Sidekick_sat/Solver_intf/module-type-S/index.html index 8d8bd545..37b66a30 100644 --- a/dev/sidekick/Sidekick_sat/Solver_intf/module-type-S/index.html +++ b/dev/sidekick/Sidekick_sat/Solver_intf/module-type-S/index.html @@ -1,4 +1,4 @@ S (sidekick.Sidekick_sat.Solver_intf.S)

Module type Solver_intf.S

The external interface implemented by safe solvers, such as the one created by the Solver.Make and Mcsolver.Make functors.

Internal modules

These are the internal modules used, you should probably not use them if you're not familiar with the internals of mSAT.

type lit

literals

module Lit : LIT with type t = lit

lits

type clause
type clause_pool_id

Pool of clauses, with its own lifetime management

type theory
type proof

A representation of a full proof

type proof_step
type solver

The main solver type.

type store

Stores atoms, clauses, etc.

module Clause : sig ... end
module Proof : PROOF with type lit = lit and type t = proof

A module to manipulate proofs.

type t = solver

Main solver type, containing all state for solving.

val create : ?on_conflict:(t -> Clause.t -> unit) -> ?on_decision:(t -> lit -> unit) -> ?on_learnt:(t -> Clause.t -> unit) -> ?on_gc:(t -> lit array -> unit) -> ?stat:Sidekick_util.Stat.t -> -?size:[ `Tiny | `Small | `Big ] -> proof:Proof.t -> theory -> t

Create new solver

  • parameter theory

    the theory

  • parameter the

    proof

  • parameter size

    the initial size of internal data structures. The bigger, the faster, but also the more RAM it uses.

val theory : t -> theory

Access the theory state

val store : t -> store

Store for the solver

val stat : t -> Sidekick_util.Stat.t

Statistics

val proof : t -> proof

Access the inner proof

Clause Pools

Clause pools.

A clause pool holds/owns a set of clauses, and is responsible for managing their lifetime. We only expose an id, not a private type.

val clause_pool_descr : t -> clause_pool_id -> string
val new_clause_pool_gc_fixed_size : descr:string -> size:int -> t -> clause_pool_id

Allocate a new clause pool that GC's its clauses when its size goes above size. It keeps half of the clauses.

Types

type res =
| Sat of lit sat_state(*

Returned when the solver reaches SAT, with a model

*)
| Unsat of (lit, clause, proof_step) unsat_state(*

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 -> lit 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 -> lit list -> proof_step -> unit

Lower level addition of clauses

val add_clause_a : t -> lit array -> proof_step -> unit

Lower level addition of clauses

val add_input_clause : t -> lit list -> unit

Like add_clause but with the justification of being an input clause

val add_input_clause_a : t -> lit array -> unit

Like add_clause_a but with justification of being an input clause

val add_clause_in_pool : t -> pool:clause_pool_id -> lit list -> proof_step -> unit

Like add_clause but using a specific clause pool

val add_clause_a_in_pool : t -> pool:clause_pool_id -> lit array -> proof_step -> unit

Like add_clause_a but using a specific clause pool

val solve : ?assumptions:lit list -> t -> res

Try and solves the current set of clauses.

  • parameter assumptions

    additional atomic assumptions to be temporarily added. The assumptions are just used for this call to solve, they are not saved in the solver's state.

val add_lit : t -> ?default_pol:bool -> lit -> unit

Ensure the SAT solver handles this particular literal, ie add a boolean variable for it if it's not already there.

val set_default_pol : t -> lit -> bool -> unit

Set default polarity for the given boolean variable. Sign of the literal is ignored.

val true_at_level0 : t -> lit -> bool

true_at_level0 a returns true if a was proved at level0, i.e. it must hold in all models

val eval_lit : t -> lit -> lbool

Evaluate atom in current state

\ No newline at end of file +?size:[ `Tiny | `Small | `Big ] -> proof:Proof.t -> theory -> t

Create new solver

val theory : t -> theory

Access the theory state

val store : t -> store

Store for the solver

val stat : t -> Sidekick_util.Stat.t

Statistics

val proof : t -> proof

Access the inner proof

Clause Pools

Clause pools.

A clause pool holds/owns a set of clauses, and is responsible for managing their lifetime. We only expose an id, not a private type.

val clause_pool_descr : t -> clause_pool_id -> string
val new_clause_pool_gc_fixed_size : descr:string -> size:int -> t -> clause_pool_id

Allocate a new clause pool that GC's its clauses when its size goes above size. It keeps half of the clauses.

Types

type res =
| Sat of lit sat_state(*

Returned when the solver reaches SAT, with a model

*)
| Unsat of (lit, clause, proof_step) unsat_state(*

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 -> lit 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 -> lit list -> proof_step -> unit

Lower level addition of clauses

val add_clause_a : t -> lit array -> proof_step -> unit

Lower level addition of clauses

val add_input_clause : t -> lit list -> unit

Like add_clause but with the justification of being an input clause

val add_input_clause_a : t -> lit array -> unit

Like add_clause_a but with justification of being an input clause

val add_clause_in_pool : t -> pool:clause_pool_id -> lit list -> proof_step -> unit

Like add_clause but using a specific clause pool

val add_clause_a_in_pool : t -> pool:clause_pool_id -> lit array -> proof_step -> unit

Like add_clause_a but using a specific clause pool

val solve : ?on_progress:(unit -> unit) -> ?assumptions:lit list -> t -> res

Try and solves the current set of clauses.

  • parameter assumptions

    additional atomic assumptions to be temporarily added. The assumptions are just used for this call to solve, they are not saved in the solver's state.

  • parameter on_progress

    regularly called during solving

val add_lit : t -> ?default_pol:bool -> lit -> unit

Ensure the SAT solver handles this particular literal, ie add a boolean variable for it if it's not already there.

val set_default_pol : t -> lit -> bool -> unit

Set default polarity for the given boolean variable. Sign of the literal is ignored.

val true_at_level0 : t -> lit -> bool

true_at_level0 a returns true if a was proved at level0, i.e. it must hold in all models

val eval_lit : t -> lit -> lbool

Evaluate atom in current state

\ No newline at end of file diff --git a/dev/sidekick/Sidekick_smt_solver/Make/index.html b/dev/sidekick/Sidekick_smt_solver/Make/index.html index 76dc931d..4a44a600 100644 --- a/dev/sidekick/Sidekick_smt_solver/Make/index.html +++ b/dev/sidekick/Sidekick_smt_solver/Make/index.html @@ -2,4 +2,4 @@ Make (sidekick.Sidekick_smt_solver.Make)

Module Sidekick_smt_solver.Make

Main functor to get a solver.

Parameters

module A : ARG

Signature

module T = A.T
module Lit = A.Lit
type proof = A.proof
type proof_step = A.proof_step
module P = A.P
module Solver_internal : Sidekick_core.SOLVER_INTERNAL with module T = T and module Lit = Lit and type proof = proof and type proof_step = proof_step and module P = P

Internal solver, available to theories.

type t

The solver's state.

type solver = t
type term = T.Term.t
type ty = T.Ty.t
type lit = Lit.t
module type THEORY = sig ... end
type theory = (module THEORY)

A theory that can be used for this particular solver.

type 'a theory_p = (module THEORY with type t = 'a)

A theory that can be used for this particular solver, with state of type 'a.

val mk_theory : name:string -> create_and_setup:(Solver_internal.t -> 'th) -> ?push_level:('th -> unit) -> ?pop_levels:('th -> int -> unit) -> unit -> theory

Helper to create a theory.

module Model : sig ... end

Models

module Unknown : sig ... end

Main API

val stats : t -> Sidekick_util.Stat.t
val tst : t -> T.Term.store
val ty_st : t -> T.Ty.store
val proof : t -> proof
val create : ?stat:Sidekick_util.Stat.t -> ?size:[ `Big | `Tiny | `Small ] -> proof:proof -> theories:theory list -> T.Term.store -> T.Ty.store -> unit -> t

Create a new solver.

It needs a term state and a type state to manipulate terms and types. All terms and types interacting with this solver will need to come from these exact states.

  • parameter store_proof

    if true, proofs from the SAT solver and theories are retained and potentially accessible after solve returns UNSAT.

  • parameter size

    influences the size of initial allocations.

  • parameter theories

    theories to load from the start. Other theories can be added using add_theory.

val add_theory : t -> theory -> 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 list -> unit
val mk_lit_t : t -> ?sign:bool -> term -> 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 -> lit Sidekick_util.IArray.t -> proof_step -> 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 -> lit list -> proof_step -> unit

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

val assert_terms : t -> term list -> unit

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

val assert_term : t -> term -> unit

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

type res =
| Sat of Model.t(*

Satisfiable

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

Unsat core (subset of assumptions), or empty

*)
unsat_proof_step : unit -> proof_step 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 : ?on_exit:(unit -> unit) list -> ?check:bool -> ?on_progress:(t -> unit) -> -assumptions:lit list -> t -> res

solve s checks the satisfiability of the clauses added so far to s.

  • parameter check

    if true, the model is checked before returning.

  • parameter on_progress

    called regularly during solving.

  • parameter assumptions

    a set of atoms held to be true. The unsat core, if any, will be a subset of assumptions.

  • parameter on_exit

    functions to be run before this returns

val pp_stats : t CCFormat.printer

Print some statistics. What it prints exactly is unspecified.

\ No newline at end of file +?should_stop:(t -> int -> bool) -> assumptions:lit list -> t -> res

solve s checks the satisfiability of the clauses added so far to s.

val pp_stats : t CCFormat.printer

Print some statistics. What it prints exactly is unspecified.

\ No newline at end of file diff --git a/dev/sidekick/Sidekick_th_bool_static/Make/argument-1-A/S/index.html b/dev/sidekick/Sidekick_th_bool_static/Make/argument-1-A/S/index.html index e2536070..f718dbc8 100644 --- a/dev/sidekick/Sidekick_th_bool_static/Make/argument-1-A/S/index.html +++ b/dev/sidekick/Sidekick_th_bool_static/Make/argument-1-A/S/index.html @@ -2,4 +2,4 @@ S (sidekick.Sidekick_th_bool_static.Make.1-A.S)

Module 1-A.S

module Lit : Sidekick_core.LIT with module T = T
type proof
type proof_step
module P : Sidekick_core.PROOF with type lit = Lit.t and type t = proof and type proof_step = proof_step and type term = T.Term.t
module Solver_internal : Sidekick_core.SOLVER_INTERNAL with module T = T and module Lit = Lit and type proof = proof and type proof_step = proof_step and module P = P

Internal solver, available to theories.

type t

The solver's state.

type solver = t
type term = T.Term.t
type ty = T.Ty.t
type lit = Lit.t
module type THEORY = sig ... end
type theory = (module THEORY)

A theory that can be used for this particular solver.

type 'a theory_p = (module THEORY with type t = 'a)

A theory that can be used for this particular solver, with state of type 'a.

val mk_theory : name:string -> create_and_setup:(Solver_internal.t -> 'th) -> ?push_level:('th -> unit) -> ?pop_levels:('th -> int -> unit) -> unit -> theory

Helper to create a theory.

module Model : sig ... end

Models

module Unknown : sig ... end

Main API

val stats : t -> Sidekick_util.Stat.t
val tst : t -> T.Term.store
val ty_st : t -> T.Ty.store
val proof : t -> proof
val create : ?stat:Sidekick_util.Stat.t -> ?size:[ `Big | `Tiny | `Small ] -> proof:proof -> theories:theory list -> T.Term.store -> T.Ty.store -> unit -> t

Create a new solver.

It needs a term state and a type state to manipulate terms and types. All terms and types interacting with this solver will need to come from these exact states.

  • parameter store_proof

    if true, proofs from the SAT solver and theories are retained and potentially accessible after solve returns UNSAT.

  • parameter size

    influences the size of initial allocations.

  • parameter theories

    theories to load from the start. Other theories can be added using add_theory.

val add_theory : t -> theory -> 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 list -> unit
val mk_lit_t : t -> ?sign:bool -> term -> 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 -> lit Sidekick_util.IArray.t -> proof_step -> 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 -> lit list -> proof_step -> unit

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

val assert_terms : t -> term list -> unit

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

val assert_term : t -> term -> unit

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

type res =
| Sat of Model.t(*

Satisfiable

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

Unsat core (subset of assumptions), or empty

*)
unsat_proof_step : unit -> proof_step 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 : ?on_exit:(unit -> unit) list -> ?check:bool -> ?on_progress:(t -> unit) -> -assumptions:lit list -> t -> res

solve s checks the satisfiability of the clauses added so far to s.

  • parameter check

    if true, the model is checked before returning.

  • parameter on_progress

    called regularly during solving.

  • parameter assumptions

    a set of atoms held to be true. The unsat core, if any, will be a subset of assumptions.

  • parameter on_exit

    functions to be run before this returns

val pp_stats : t CCFormat.printer

Print some statistics. What it prints exactly is unspecified.

\ No newline at end of file +?should_stop:(t -> int -> bool) -> assumptions:lit list -> t -> res

solve s checks the satisfiability of the clauses added so far to s.

val pp_stats : t CCFormat.printer

Print some statistics. What it prints exactly is unspecified.

\ No newline at end of file diff --git a/dev/sidekick/Sidekick_th_bool_static/module-type-ARG/S/index.html b/dev/sidekick/Sidekick_th_bool_static/module-type-ARG/S/index.html index fe1a7641..a779b5aa 100644 --- a/dev/sidekick/Sidekick_th_bool_static/module-type-ARG/S/index.html +++ b/dev/sidekick/Sidekick_th_bool_static/module-type-ARG/S/index.html @@ -2,4 +2,4 @@ S (sidekick.Sidekick_th_bool_static.ARG.S)

Module ARG.S

module Lit : Sidekick_core.LIT with module T = T
type proof
type proof_step
module P : Sidekick_core.PROOF with type lit = Lit.t and type t = proof and type proof_step = proof_step and type term = T.Term.t
module Solver_internal : Sidekick_core.SOLVER_INTERNAL with module T = T and module Lit = Lit and type proof = proof and type proof_step = proof_step and module P = P

Internal solver, available to theories.

type t

The solver's state.

type solver = t
type term = T.Term.t
type ty = T.Ty.t
type lit = Lit.t
module type THEORY = sig ... end
type theory = (module THEORY)

A theory that can be used for this particular solver.

type 'a theory_p = (module THEORY with type t = 'a)

A theory that can be used for this particular solver, with state of type 'a.

val mk_theory : name:string -> create_and_setup:(Solver_internal.t -> 'th) -> ?push_level:('th -> unit) -> ?pop_levels:('th -> int -> unit) -> unit -> theory

Helper to create a theory.

module Model : sig ... end

Models

module Unknown : sig ... end

Main API

val stats : t -> Sidekick_util.Stat.t
val tst : t -> T.Term.store
val ty_st : t -> T.Ty.store
val proof : t -> proof
val create : ?stat:Sidekick_util.Stat.t -> ?size:[ `Big | `Tiny | `Small ] -> proof:proof -> theories:theory list -> T.Term.store -> T.Ty.store -> unit -> t

Create a new solver.

It needs a term state and a type state to manipulate terms and types. All terms and types interacting with this solver will need to come from these exact states.

  • parameter store_proof

    if true, proofs from the SAT solver and theories are retained and potentially accessible after solve returns UNSAT.

  • parameter size

    influences the size of initial allocations.

  • parameter theories

    theories to load from the start. Other theories can be added using add_theory.

val add_theory : t -> theory -> 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 list -> unit
val mk_lit_t : t -> ?sign:bool -> term -> 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 -> lit Sidekick_util.IArray.t -> proof_step -> 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 -> lit list -> proof_step -> unit

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

val assert_terms : t -> term list -> unit

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

val assert_term : t -> term -> unit

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

type res =
| Sat of Model.t(*

Satisfiable

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

Unsat core (subset of assumptions), or empty

*)
unsat_proof_step : unit -> proof_step 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 : ?on_exit:(unit -> unit) list -> ?check:bool -> ?on_progress:(t -> unit) -> -assumptions:lit list -> t -> res

solve s checks the satisfiability of the clauses added so far to s.

  • parameter check

    if true, the model is checked before returning.

  • parameter on_progress

    called regularly during solving.

  • parameter assumptions

    a set of atoms held to be true. The unsat core, if any, will be a subset of assumptions.

  • parameter on_exit

    functions to be run before this returns

val pp_stats : t CCFormat.printer

Print some statistics. What it prints exactly is unspecified.

\ No newline at end of file +?should_stop:(t -> int -> bool) -> assumptions:lit list -> t -> res

solve s checks the satisfiability of the clauses added so far to s.

val pp_stats : t CCFormat.printer

Print some statistics. What it prints exactly is unspecified.

\ No newline at end of file diff --git a/dev/sidekick/Sidekick_th_bool_static/module-type-S/A/S/index.html b/dev/sidekick/Sidekick_th_bool_static/module-type-S/A/S/index.html index aa32182b..3061e0cb 100644 --- a/dev/sidekick/Sidekick_th_bool_static/module-type-S/A/S/index.html +++ b/dev/sidekick/Sidekick_th_bool_static/module-type-S/A/S/index.html @@ -2,4 +2,4 @@ S (sidekick.Sidekick_th_bool_static.S.A.S)

Module A.S

module Lit : Sidekick_core.LIT with module T = T
type proof
type proof_step
module P : Sidekick_core.PROOF with type lit = Lit.t and type t = proof and type proof_step = proof_step and type term = T.Term.t
module Solver_internal : Sidekick_core.SOLVER_INTERNAL with module T = T and module Lit = Lit and type proof = proof and type proof_step = proof_step and module P = P

Internal solver, available to theories.

type t

The solver's state.

type solver = t
type term = T.Term.t
type ty = T.Ty.t
type lit = Lit.t
module type THEORY = sig ... end
type theory = (module THEORY)

A theory that can be used for this particular solver.

type 'a theory_p = (module THEORY with type t = 'a)

A theory that can be used for this particular solver, with state of type 'a.

val mk_theory : name:string -> create_and_setup:(Solver_internal.t -> 'th) -> ?push_level:('th -> unit) -> ?pop_levels:('th -> int -> unit) -> unit -> theory

Helper to create a theory.

module Model : sig ... end

Models

module Unknown : sig ... end

Main API

val stats : t -> Sidekick_util.Stat.t
val tst : t -> T.Term.store
val ty_st : t -> T.Ty.store
val proof : t -> proof
val create : ?stat:Sidekick_util.Stat.t -> ?size:[ `Big | `Tiny | `Small ] -> proof:proof -> theories:theory list -> T.Term.store -> T.Ty.store -> unit -> t

Create a new solver.

It needs a term state and a type state to manipulate terms and types. All terms and types interacting with this solver will need to come from these exact states.

  • parameter store_proof

    if true, proofs from the SAT solver and theories are retained and potentially accessible after solve returns UNSAT.

  • parameter size

    influences the size of initial allocations.

  • parameter theories

    theories to load from the start. Other theories can be added using add_theory.

val add_theory : t -> theory -> 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 list -> unit
val mk_lit_t : t -> ?sign:bool -> term -> 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 -> lit Sidekick_util.IArray.t -> proof_step -> 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 -> lit list -> proof_step -> unit

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

val assert_terms : t -> term list -> unit

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

val assert_term : t -> term -> unit

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

type res =
| Sat of Model.t(*

Satisfiable

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

Unsat core (subset of assumptions), or empty

*)
unsat_proof_step : unit -> proof_step 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 : ?on_exit:(unit -> unit) list -> ?check:bool -> ?on_progress:(t -> unit) -> -assumptions:lit list -> t -> res

solve s checks the satisfiability of the clauses added so far to s.

  • parameter check

    if true, the model is checked before returning.

  • parameter on_progress

    called regularly during solving.

  • parameter assumptions

    a set of atoms held to be true. The unsat core, if any, will be a subset of assumptions.

  • parameter on_exit

    functions to be run before this returns

val pp_stats : t CCFormat.printer

Print some statistics. What it prints exactly is unspecified.

\ No newline at end of file +?should_stop:(t -> int -> bool) -> assumptions:lit list -> t -> res

solve s checks the satisfiability of the clauses added so far to s.

val pp_stats : t CCFormat.printer

Print some statistics. What it prints exactly is unspecified.

\ No newline at end of file diff --git a/dev/sidekick/Sidekick_th_cstor/Make/argument-1-A/S/index.html b/dev/sidekick/Sidekick_th_cstor/Make/argument-1-A/S/index.html index 32957f50..20b0873c 100644 --- a/dev/sidekick/Sidekick_th_cstor/Make/argument-1-A/S/index.html +++ b/dev/sidekick/Sidekick_th_cstor/Make/argument-1-A/S/index.html @@ -2,4 +2,4 @@ S (sidekick.Sidekick_th_cstor.Make.1-A.S)

Module 1-A.S

module Lit : Sidekick_core.LIT with module T = T
type proof
type proof_step
module P : Sidekick_core.PROOF with type lit = Lit.t and type t = proof and type proof_step = proof_step and type term = T.Term.t
module Solver_internal : Sidekick_core.SOLVER_INTERNAL with module T = T and module Lit = Lit and type proof = proof and type proof_step = proof_step and module P = P

Internal solver, available to theories.

type t

The solver's state.

type solver = t
type term = T.Term.t
type ty = T.Ty.t
type lit = Lit.t
module type THEORY = sig ... end
type theory = (module THEORY)

A theory that can be used for this particular solver.

type 'a theory_p = (module THEORY with type t = 'a)

A theory that can be used for this particular solver, with state of type 'a.

val mk_theory : name:string -> create_and_setup:(Solver_internal.t -> 'th) -> ?push_level:('th -> unit) -> ?pop_levels:('th -> int -> unit) -> unit -> theory

Helper to create a theory.

module Model : sig ... end

Models

module Unknown : sig ... end

Main API

val stats : t -> Sidekick_util.Stat.t
val tst : t -> T.Term.store
val ty_st : t -> T.Ty.store
val proof : t -> proof
val create : ?stat:Sidekick_util.Stat.t -> ?size:[ `Big | `Tiny | `Small ] -> proof:proof -> theories:theory list -> T.Term.store -> T.Ty.store -> unit -> t

Create a new solver.

It needs a term state and a type state to manipulate terms and types. All terms and types interacting with this solver will need to come from these exact states.

  • parameter store_proof

    if true, proofs from the SAT solver and theories are retained and potentially accessible after solve returns UNSAT.

  • parameter size

    influences the size of initial allocations.

  • parameter theories

    theories to load from the start. Other theories can be added using add_theory.

val add_theory : t -> theory -> 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 list -> unit
val mk_lit_t : t -> ?sign:bool -> term -> 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 -> lit Sidekick_util.IArray.t -> proof_step -> 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 -> lit list -> proof_step -> unit

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

val assert_terms : t -> term list -> unit

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

val assert_term : t -> term -> unit

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

type res =
| Sat of Model.t(*

Satisfiable

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

Unsat core (subset of assumptions), or empty

*)
unsat_proof_step : unit -> proof_step 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 : ?on_exit:(unit -> unit) list -> ?check:bool -> ?on_progress:(t -> unit) -> -assumptions:lit list -> t -> res

solve s checks the satisfiability of the clauses added so far to s.

  • parameter check

    if true, the model is checked before returning.

  • parameter on_progress

    called regularly during solving.

  • parameter assumptions

    a set of atoms held to be true. The unsat core, if any, will be a subset of assumptions.

  • parameter on_exit

    functions to be run before this returns

val pp_stats : t CCFormat.printer

Print some statistics. What it prints exactly is unspecified.

\ No newline at end of file +?should_stop:(t -> int -> bool) -> assumptions:lit list -> t -> res

solve s checks the satisfiability of the clauses added so far to s.

val pp_stats : t CCFormat.printer

Print some statistics. What it prints exactly is unspecified.

\ No newline at end of file diff --git a/dev/sidekick/Sidekick_th_cstor/module-type-ARG/S/index.html b/dev/sidekick/Sidekick_th_cstor/module-type-ARG/S/index.html index 36388c19..0bb56dc4 100644 --- a/dev/sidekick/Sidekick_th_cstor/module-type-ARG/S/index.html +++ b/dev/sidekick/Sidekick_th_cstor/module-type-ARG/S/index.html @@ -2,4 +2,4 @@ S (sidekick.Sidekick_th_cstor.ARG.S)

Module ARG.S

module Lit : Sidekick_core.LIT with module T = T
type proof
type proof_step
module P : Sidekick_core.PROOF with type lit = Lit.t and type t = proof and type proof_step = proof_step and type term = T.Term.t
module Solver_internal : Sidekick_core.SOLVER_INTERNAL with module T = T and module Lit = Lit and type proof = proof and type proof_step = proof_step and module P = P

Internal solver, available to theories.

type t

The solver's state.

type solver = t
type term = T.Term.t
type ty = T.Ty.t
type lit = Lit.t
module type THEORY = sig ... end
type theory = (module THEORY)

A theory that can be used for this particular solver.

type 'a theory_p = (module THEORY with type t = 'a)

A theory that can be used for this particular solver, with state of type 'a.

val mk_theory : name:string -> create_and_setup:(Solver_internal.t -> 'th) -> ?push_level:('th -> unit) -> ?pop_levels:('th -> int -> unit) -> unit -> theory

Helper to create a theory.

module Model : sig ... end

Models

module Unknown : sig ... end

Main API

val stats : t -> Sidekick_util.Stat.t
val tst : t -> T.Term.store
val ty_st : t -> T.Ty.store
val proof : t -> proof
val create : ?stat:Sidekick_util.Stat.t -> ?size:[ `Big | `Tiny | `Small ] -> proof:proof -> theories:theory list -> T.Term.store -> T.Ty.store -> unit -> t

Create a new solver.

It needs a term state and a type state to manipulate terms and types. All terms and types interacting with this solver will need to come from these exact states.

  • parameter store_proof

    if true, proofs from the SAT solver and theories are retained and potentially accessible after solve returns UNSAT.

  • parameter size

    influences the size of initial allocations.

  • parameter theories

    theories to load from the start. Other theories can be added using add_theory.

val add_theory : t -> theory -> 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 list -> unit
val mk_lit_t : t -> ?sign:bool -> term -> 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 -> lit Sidekick_util.IArray.t -> proof_step -> 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 -> lit list -> proof_step -> unit

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

val assert_terms : t -> term list -> unit

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

val assert_term : t -> term -> unit

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

type res =
| Sat of Model.t(*

Satisfiable

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

Unsat core (subset of assumptions), or empty

*)
unsat_proof_step : unit -> proof_step 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 : ?on_exit:(unit -> unit) list -> ?check:bool -> ?on_progress:(t -> unit) -> -assumptions:lit list -> t -> res

solve s checks the satisfiability of the clauses added so far to s.

  • parameter check

    if true, the model is checked before returning.

  • parameter on_progress

    called regularly during solving.

  • parameter assumptions

    a set of atoms held to be true. The unsat core, if any, will be a subset of assumptions.

  • parameter on_exit

    functions to be run before this returns

val pp_stats : t CCFormat.printer

Print some statistics. What it prints exactly is unspecified.

\ No newline at end of file +?should_stop:(t -> int -> bool) -> assumptions:lit list -> t -> res

solve s checks the satisfiability of the clauses added so far to s.

val pp_stats : t CCFormat.printer

Print some statistics. What it prints exactly is unspecified.

\ No newline at end of file diff --git a/dev/sidekick/Sidekick_th_cstor/module-type-S/A/S/index.html b/dev/sidekick/Sidekick_th_cstor/module-type-S/A/S/index.html index 22c4d837..7ee43978 100644 --- a/dev/sidekick/Sidekick_th_cstor/module-type-S/A/S/index.html +++ b/dev/sidekick/Sidekick_th_cstor/module-type-S/A/S/index.html @@ -2,4 +2,4 @@ S (sidekick.Sidekick_th_cstor.S.A.S)

Module A.S

module Lit : Sidekick_core.LIT with module T = T
type proof
type proof_step
module P : Sidekick_core.PROOF with type lit = Lit.t and type t = proof and type proof_step = proof_step and type term = T.Term.t
module Solver_internal : Sidekick_core.SOLVER_INTERNAL with module T = T and module Lit = Lit and type proof = proof and type proof_step = proof_step and module P = P

Internal solver, available to theories.

type t

The solver's state.

type solver = t
type term = T.Term.t
type ty = T.Ty.t
type lit = Lit.t
module type THEORY = sig ... end
type theory = (module THEORY)

A theory that can be used for this particular solver.

type 'a theory_p = (module THEORY with type t = 'a)

A theory that can be used for this particular solver, with state of type 'a.

val mk_theory : name:string -> create_and_setup:(Solver_internal.t -> 'th) -> ?push_level:('th -> unit) -> ?pop_levels:('th -> int -> unit) -> unit -> theory

Helper to create a theory.

module Model : sig ... end

Models

module Unknown : sig ... end

Main API

val stats : t -> Sidekick_util.Stat.t
val tst : t -> T.Term.store
val ty_st : t -> T.Ty.store
val proof : t -> proof
val create : ?stat:Sidekick_util.Stat.t -> ?size:[ `Big | `Tiny | `Small ] -> proof:proof -> theories:theory list -> T.Term.store -> T.Ty.store -> unit -> t

Create a new solver.

It needs a term state and a type state to manipulate terms and types. All terms and types interacting with this solver will need to come from these exact states.

  • parameter store_proof

    if true, proofs from the SAT solver and theories are retained and potentially accessible after solve returns UNSAT.

  • parameter size

    influences the size of initial allocations.

  • parameter theories

    theories to load from the start. Other theories can be added using add_theory.

val add_theory : t -> theory -> 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 list -> unit
val mk_lit_t : t -> ?sign:bool -> term -> 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 -> lit Sidekick_util.IArray.t -> proof_step -> 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 -> lit list -> proof_step -> unit

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

val assert_terms : t -> term list -> unit

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

val assert_term : t -> term -> unit

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

type res =
| Sat of Model.t(*

Satisfiable

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

Unsat core (subset of assumptions), or empty

*)
unsat_proof_step : unit -> proof_step 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 : ?on_exit:(unit -> unit) list -> ?check:bool -> ?on_progress:(t -> unit) -> -assumptions:lit list -> t -> res

solve s checks the satisfiability of the clauses added so far to s.

  • parameter check

    if true, the model is checked before returning.

  • parameter on_progress

    called regularly during solving.

  • parameter assumptions

    a set of atoms held to be true. The unsat core, if any, will be a subset of assumptions.

  • parameter on_exit

    functions to be run before this returns

val pp_stats : t CCFormat.printer

Print some statistics. What it prints exactly is unspecified.

\ No newline at end of file +?should_stop:(t -> int -> bool) -> assumptions:lit list -> t -> res

solve s checks the satisfiability of the clauses added so far to s.

val pp_stats : t CCFormat.printer

Print some statistics. What it prints exactly is unspecified.

\ No newline at end of file diff --git a/dev/sidekick/Sidekick_th_data/Make/argument-1-A/S/index.html b/dev/sidekick/Sidekick_th_data/Make/argument-1-A/S/index.html index d0f1de1d..b8fb0fb8 100644 --- a/dev/sidekick/Sidekick_th_data/Make/argument-1-A/S/index.html +++ b/dev/sidekick/Sidekick_th_data/Make/argument-1-A/S/index.html @@ -2,4 +2,4 @@ S (sidekick.Sidekick_th_data.Make.1-A.S)

Module 1-A.S

module Lit : Sidekick_core.LIT with module T = T
type proof
type proof_step
module P : Sidekick_core.PROOF with type lit = Lit.t and type t = proof and type proof_step = proof_step and type term = T.Term.t
module Solver_internal : Sidekick_core.SOLVER_INTERNAL with module T = T and module Lit = Lit and type proof = proof and type proof_step = proof_step and module P = P

Internal solver, available to theories.

type t

The solver's state.

type solver = t
type term = T.Term.t
type ty = T.Ty.t
type lit = Lit.t
module type THEORY = sig ... end
type theory = (module THEORY)

A theory that can be used for this particular solver.

type 'a theory_p = (module THEORY with type t = 'a)

A theory that can be used for this particular solver, with state of type 'a.

val mk_theory : name:string -> create_and_setup:(Solver_internal.t -> 'th) -> ?push_level:('th -> unit) -> ?pop_levels:('th -> int -> unit) -> unit -> theory

Helper to create a theory.

module Model : sig ... end

Models

module Unknown : sig ... end

Main API

val stats : t -> Sidekick_util.Stat.t
val tst : t -> T.Term.store
val ty_st : t -> T.Ty.store
val proof : t -> proof
val create : ?stat:Sidekick_util.Stat.t -> ?size:[ `Big | `Tiny | `Small ] -> proof:proof -> theories:theory list -> T.Term.store -> T.Ty.store -> unit -> t

Create a new solver.

It needs a term state and a type state to manipulate terms and types. All terms and types interacting with this solver will need to come from these exact states.

  • parameter store_proof

    if true, proofs from the SAT solver and theories are retained and potentially accessible after solve returns UNSAT.

  • parameter size

    influences the size of initial allocations.

  • parameter theories

    theories to load from the start. Other theories can be added using add_theory.

val add_theory : t -> theory -> 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 list -> unit
val mk_lit_t : t -> ?sign:bool -> term -> 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 -> lit Sidekick_util.IArray.t -> proof_step -> 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 -> lit list -> proof_step -> unit

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

val assert_terms : t -> term list -> unit

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

val assert_term : t -> term -> unit

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

type res =
| Sat of Model.t(*

Satisfiable

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

Unsat core (subset of assumptions), or empty

*)
unsat_proof_step : unit -> proof_step 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 : ?on_exit:(unit -> unit) list -> ?check:bool -> ?on_progress:(t -> unit) -> -assumptions:lit list -> t -> res

solve s checks the satisfiability of the clauses added so far to s.

  • parameter check

    if true, the model is checked before returning.

  • parameter on_progress

    called regularly during solving.

  • parameter assumptions

    a set of atoms held to be true. The unsat core, if any, will be a subset of assumptions.

  • parameter on_exit

    functions to be run before this returns

val pp_stats : t CCFormat.printer

Print some statistics. What it prints exactly is unspecified.

\ No newline at end of file +?should_stop:(t -> int -> bool) -> assumptions:lit list -> t -> res

solve s checks the satisfiability of the clauses added so far to s.

val pp_stats : t CCFormat.printer

Print some statistics. What it prints exactly is unspecified.

\ No newline at end of file diff --git a/dev/sidekick/Sidekick_th_data/module-type-ARG/S/index.html b/dev/sidekick/Sidekick_th_data/module-type-ARG/S/index.html index bec57266..a136a7a6 100644 --- a/dev/sidekick/Sidekick_th_data/module-type-ARG/S/index.html +++ b/dev/sidekick/Sidekick_th_data/module-type-ARG/S/index.html @@ -2,4 +2,4 @@ S (sidekick.Sidekick_th_data.ARG.S)

Module ARG.S

module Lit : Sidekick_core.LIT with module T = T
type proof
type proof_step
module P : Sidekick_core.PROOF with type lit = Lit.t and type t = proof and type proof_step = proof_step and type term = T.Term.t
module Solver_internal : Sidekick_core.SOLVER_INTERNAL with module T = T and module Lit = Lit and type proof = proof and type proof_step = proof_step and module P = P

Internal solver, available to theories.

type t

The solver's state.

type solver = t
type term = T.Term.t
type ty = T.Ty.t
type lit = Lit.t
module type THEORY = sig ... end
type theory = (module THEORY)

A theory that can be used for this particular solver.

type 'a theory_p = (module THEORY with type t = 'a)

A theory that can be used for this particular solver, with state of type 'a.

val mk_theory : name:string -> create_and_setup:(Solver_internal.t -> 'th) -> ?push_level:('th -> unit) -> ?pop_levels:('th -> int -> unit) -> unit -> theory

Helper to create a theory.

module Model : sig ... end

Models

module Unknown : sig ... end

Main API

val stats : t -> Sidekick_util.Stat.t
val tst : t -> T.Term.store
val ty_st : t -> T.Ty.store
val proof : t -> proof
val create : ?stat:Sidekick_util.Stat.t -> ?size:[ `Big | `Tiny | `Small ] -> proof:proof -> theories:theory list -> T.Term.store -> T.Ty.store -> unit -> t

Create a new solver.

It needs a term state and a type state to manipulate terms and types. All terms and types interacting with this solver will need to come from these exact states.

  • parameter store_proof

    if true, proofs from the SAT solver and theories are retained and potentially accessible after solve returns UNSAT.

  • parameter size

    influences the size of initial allocations.

  • parameter theories

    theories to load from the start. Other theories can be added using add_theory.

val add_theory : t -> theory -> 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 list -> unit
val mk_lit_t : t -> ?sign:bool -> term -> 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 -> lit Sidekick_util.IArray.t -> proof_step -> 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 -> lit list -> proof_step -> unit

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

val assert_terms : t -> term list -> unit

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

val assert_term : t -> term -> unit

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

type res =
| Sat of Model.t(*

Satisfiable

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

Unsat core (subset of assumptions), or empty

*)
unsat_proof_step : unit -> proof_step 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 : ?on_exit:(unit -> unit) list -> ?check:bool -> ?on_progress:(t -> unit) -> -assumptions:lit list -> t -> res

solve s checks the satisfiability of the clauses added so far to s.

  • parameter check

    if true, the model is checked before returning.

  • parameter on_progress

    called regularly during solving.

  • parameter assumptions

    a set of atoms held to be true. The unsat core, if any, will be a subset of assumptions.

  • parameter on_exit

    functions to be run before this returns

val pp_stats : t CCFormat.printer

Print some statistics. What it prints exactly is unspecified.

\ No newline at end of file +?should_stop:(t -> int -> bool) -> assumptions:lit list -> t -> res

solve s checks the satisfiability of the clauses added so far to s.

val pp_stats : t CCFormat.printer

Print some statistics. What it prints exactly is unspecified.

\ No newline at end of file diff --git a/dev/sidekick/Sidekick_th_data/module-type-S/A/S/index.html b/dev/sidekick/Sidekick_th_data/module-type-S/A/S/index.html index faaaad70..8e80d430 100644 --- a/dev/sidekick/Sidekick_th_data/module-type-S/A/S/index.html +++ b/dev/sidekick/Sidekick_th_data/module-type-S/A/S/index.html @@ -2,4 +2,4 @@ S (sidekick.Sidekick_th_data.S.A.S)

Module A.S

module Lit : Sidekick_core.LIT with module T = T
type proof
type proof_step
module P : Sidekick_core.PROOF with type lit = Lit.t and type t = proof and type proof_step = proof_step and type term = T.Term.t
module Solver_internal : Sidekick_core.SOLVER_INTERNAL with module T = T and module Lit = Lit and type proof = proof and type proof_step = proof_step and module P = P

Internal solver, available to theories.

type t

The solver's state.

type solver = t
type term = T.Term.t
type ty = T.Ty.t
type lit = Lit.t
module type THEORY = sig ... end
type theory = (module THEORY)

A theory that can be used for this particular solver.

type 'a theory_p = (module THEORY with type t = 'a)

A theory that can be used for this particular solver, with state of type 'a.

val mk_theory : name:string -> create_and_setup:(Solver_internal.t -> 'th) -> ?push_level:('th -> unit) -> ?pop_levels:('th -> int -> unit) -> unit -> theory

Helper to create a theory.

module Model : sig ... end

Models

module Unknown : sig ... end

Main API

val stats : t -> Sidekick_util.Stat.t
val tst : t -> T.Term.store
val ty_st : t -> T.Ty.store
val proof : t -> proof
val create : ?stat:Sidekick_util.Stat.t -> ?size:[ `Big | `Tiny | `Small ] -> proof:proof -> theories:theory list -> T.Term.store -> T.Ty.store -> unit -> t

Create a new solver.

It needs a term state and a type state to manipulate terms and types. All terms and types interacting with this solver will need to come from these exact states.

  • parameter store_proof

    if true, proofs from the SAT solver and theories are retained and potentially accessible after solve returns UNSAT.

  • parameter size

    influences the size of initial allocations.

  • parameter theories

    theories to load from the start. Other theories can be added using add_theory.

val add_theory : t -> theory -> 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 list -> unit
val mk_lit_t : t -> ?sign:bool -> term -> 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 -> lit Sidekick_util.IArray.t -> proof_step -> 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 -> lit list -> proof_step -> unit

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

val assert_terms : t -> term list -> unit

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

val assert_term : t -> term -> unit

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

type res =
| Sat of Model.t(*

Satisfiable

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

Unsat core (subset of assumptions), or empty

*)
unsat_proof_step : unit -> proof_step 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 : ?on_exit:(unit -> unit) list -> ?check:bool -> ?on_progress:(t -> unit) -> -assumptions:lit list -> t -> res

solve s checks the satisfiability of the clauses added so far to s.

  • parameter check

    if true, the model is checked before returning.

  • parameter on_progress

    called regularly during solving.

  • parameter assumptions

    a set of atoms held to be true. The unsat core, if any, will be a subset of assumptions.

  • parameter on_exit

    functions to be run before this returns

val pp_stats : t CCFormat.printer

Print some statistics. What it prints exactly is unspecified.

\ No newline at end of file +?should_stop:(t -> int -> bool) -> assumptions:lit list -> t -> res

solve s checks the satisfiability of the clauses added so far to s.

val pp_stats : t CCFormat.printer

Print some statistics. What it prints exactly is unspecified.

\ No newline at end of file