diff --git a/dev/sidekick-base/Sidekick_base_solver/Solver/index.html b/dev/sidekick-base/Sidekick_base_solver/Solver/index.html index 39fa9e37..c2a1e5bb 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) -> -?should_stop:(t -> int -> bool) -> 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 push_assumption : t -> lit -> unit
val pop_assumptions : t -> int -> unit
type propagation_result = Sidekick_smt_solver.Make(Solver_arg).propagation_result =
| PR_sat
| PR_conflict of {
backtracked : int;
}
| PR_unsat of {
unsat_core : unit -> lit Iter.t;
}
val check_sat_propagations_only : assumptions:lit list -> t -> propagation_result
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 3fbbaede..d22e2032 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) -> -?should_stop:(t -> int -> bool) -> 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 push_assumption : t -> lit -> unit
val pop_assumptions : t -> int -> unit
type propagation_result = Sidekick_smt_solver.Make(Solver_arg).propagation_result =
| PR_sat
| PR_conflict of {
backtracked : int;
}
| PR_unsat of {
unsat_core : unit -> lit Iter.t;
}
val check_sat_propagations_only : assumptions:lit list -> t -> propagation_result
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 f4fd1be0..6e9c9e1d 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) -> -?should_stop:(t -> int -> bool) -> 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 push_assumption : t -> lit -> unit
val pop_assumptions : t -> int -> unit
type propagation_result = Sidekick_smt_solver.Make(Solver_arg).propagation_result =
| PR_sat
| PR_conflict of {
backtracked : int;
}
| PR_unsat of {
unsat_core : unit -> lit Iter.t;
}
val check_sat_propagations_only : assumptions:lit list -> t -> propagation_result
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 e2ca1b04..45f89e99 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) -> -?should_stop:(t -> int -> bool) -> 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 push_assumption : t -> lit -> unit
val pop_assumptions : t -> int -> unit
type propagation_result = Sidekick_smt_solver.Make(Solver_arg).propagation_result =
| PR_sat
| PR_conflict of {
backtracked : int;
}
| PR_unsat of {
unsat_core : unit -> lit Iter.t;
}
val check_sat_propagations_only : assumptions:lit list -> t -> propagation_result
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 6628ae2b..cbec5d68 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) -> -?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 +?should_stop:(t -> int -> bool) -> assumptions:lit list -> t -> res

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

val push_assumption : t -> lit -> unit

Pushes an assumption onto the assumption stack. It will remain there until it's pop'd by pop_assumptions.

val pop_assumptions : t -> int -> unit

pop_assumptions solver n removes n assumptions from the stack. It removes the assumptions that were the most recently added via push_assumptions. Note that check_sat_propagations_only can call this if it meets a conflict.

type propagation_result =
| PR_sat
| PR_conflict of {
backtracked : int;
}
| PR_unsat of {
unsat_core : unit -> lit Iter.t;
}
val check_sat_propagations_only : assumptions:lit list -> t -> propagation_result

check_sat_propagations_only solver uses assumptions (including the assumptions parameter, and atoms previously added via push_assumptions) and boolean+theory propagation to quickly assess satisfiability. It is not complete; calling solve is required to get an accurate result.

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 b89ae274..bd8918af 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) -> -?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 +?should_stop:(t -> int -> bool) -> assumptions:lit list -> t -> res

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

val push_assumption : t -> lit -> unit

Pushes an assumption onto the assumption stack. It will remain there until it's pop'd by pop_assumptions.

val pop_assumptions : t -> int -> unit

pop_assumptions solver n removes n assumptions from the stack. It removes the assumptions that were the most recently added via push_assumptions. Note that check_sat_propagations_only can call this if it meets a conflict.

type propagation_result =
| PR_sat
| PR_conflict of {
backtracked : int;
}
| PR_unsat of {
unsat_core : unit -> lit Iter.t;
}
val check_sat_propagations_only : assumptions:lit list -> t -> propagation_result

check_sat_propagations_only solver uses assumptions (including the assumptions parameter, and atoms previously added via push_assumptions) and boolean+theory propagation to quickly assess satisfiability. It is not complete; calling solve is required to get an accurate result.

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 12876fed..3819d9a3 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) -> -?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 +?should_stop:(t -> int -> bool) -> assumptions:lit list -> t -> res

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

val push_assumption : t -> lit -> unit

Pushes an assumption onto the assumption stack. It will remain there until it's pop'd by pop_assumptions.

val pop_assumptions : t -> int -> unit

pop_assumptions solver n removes n assumptions from the stack. It removes the assumptions that were the most recently added via push_assumptions. Note that check_sat_propagations_only can call this if it meets a conflict.

type propagation_result =
| PR_sat
| PR_conflict of {
backtracked : int;
}
| PR_unsat of {
unsat_core : unit -> lit Iter.t;
}
val check_sat_propagations_only : assumptions:lit list -> t -> propagation_result

check_sat_propagations_only solver uses assumptions (including the assumptions parameter, and atoms previously added via push_assumptions) and boolean+theory propagation to quickly assess satisfiability. It is not complete; calling solve is required to get an accurate result.

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 0fe07c71..462be9e5 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) -> -?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 +?should_stop:(t -> int -> bool) -> assumptions:lit list -> t -> res

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

val push_assumption : t -> lit -> unit

Pushes an assumption onto the assumption stack. It will remain there until it's pop'd by pop_assumptions.

val pop_assumptions : t -> int -> unit

pop_assumptions solver n removes n assumptions from the stack. It removes the assumptions that were the most recently added via push_assumptions. Note that check_sat_propagations_only can call this if it meets a conflict.

type propagation_result =
| PR_sat
| PR_conflict of {
backtracked : int;
}
| PR_unsat of {
unsat_core : unit -> lit Iter.t;
}
val check_sat_propagations_only : assumptions:lit list -> t -> propagation_result

check_sat_propagations_only solver uses assumptions (including the assumptions parameter, and atoms previously added via push_assumptions) and boolean+theory propagation to quickly assess satisfiability. It is not complete; calling solve is required to get an accurate result.

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/module-type-SOLVER/index.html b/dev/sidekick/Sidekick_core/module-type-SOLVER/index.html index 0c8ec80a..8f2158b9 100644 --- a/dev/sidekick/Sidekick_core/module-type-SOLVER/index.html +++ b/dev/sidekick/Sidekick_core/module-type-SOLVER/index.html @@ -2,4 +2,4 @@ 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) -> -?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 +?should_stop:(t -> int -> bool) -> assumptions:lit list -> t -> res

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

val push_assumption : t -> lit -> unit

Pushes an assumption onto the assumption stack. It will remain there until it's pop'd by pop_assumptions.

val pop_assumptions : t -> int -> unit

pop_assumptions solver n removes n assumptions from the stack. It removes the assumptions that were the most recently added via push_assumptions. Note that check_sat_propagations_only can call this if it meets a conflict.

type propagation_result =
| PR_sat
| PR_conflict of {
backtracked : int;
}
| PR_unsat of {
unsat_core : unit -> lit Iter.t;
}
val check_sat_propagations_only : assumptions:lit list -> t -> propagation_result

check_sat_propagations_only solver uses assumptions (including the assumptions parameter, and atoms previously added via push_assumptions) and boolean+theory propagation to quickly assess satisfiability. It is not complete; calling solve is required to get an accurate result.

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 26afe508..543a3a95 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) -> +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.

Main Solver Type

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 : ?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 +?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

Solving

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

Evaluating and adding literals

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

Assumption stack

val push_assumption : t -> lit -> unit

Pushes an assumption onto the assumption stack. It will remain there until it's pop'd by pop_assumptions.

val pop_assumptions : t -> int -> unit

pop_assumptions solver n removes n assumptions from the stack. It removes the assumptions that were the most recently added via push_assumptions.

type propagation_result =
| PR_sat
| PR_conflict of {
backtracked : int;
}
| PR_unsat of (lit, clause, proof_step) Solver_intf.unsat_state

Result returned by check_sat_propagations_only

val check_sat_propagations_only : ?assumptions:lit list -> t -> propagation_result

check_sat_propagations_only solver uses the added clauses and local assumptions (using push_assumptions and assumptions) to quickly assess whether the context is satisfiable. It is not complete; calling solve is required to get an accurate result.

  • returns

    either Ok() if propagation yielded no conflict, or Error c if a conflict clause c was found.

\ 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 8d71fde7..5ee44b17 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) -> +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.

Main Solver Type

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 : ?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 +?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

Solving

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

Evaluating and adding literals

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

Assumption stack

val push_assumption : t -> lit -> unit

Pushes an assumption onto the assumption stack. It will remain there until it's pop'd by pop_assumptions.

val pop_assumptions : t -> int -> unit

pop_assumptions solver n removes n assumptions from the stack. It removes the assumptions that were the most recently added via push_assumptions.

type propagation_result =
| PR_sat
| PR_conflict of {
backtracked : int;
}
| PR_unsat of (lit, clause, proof_step) Solver_intf.unsat_state

Result returned by check_sat_propagations_only

val check_sat_propagations_only : ?assumptions:lit list -> t -> propagation_result

check_sat_propagations_only solver uses the added clauses and local assumptions (using push_assumptions and assumptions) to quickly assess whether the context is satisfiable. It is not complete; calling solve is required to get an accurate result.

  • returns

    either Ok() if propagation yielded no conflict, or Error c if a conflict clause c was found.

\ 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 37b66a30..841af84f 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) -> +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.

Main Solver Type

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 : ?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 +?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

Solving

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

Evaluating and adding literals

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

Assumption stack

val push_assumption : t -> lit -> unit

Pushes an assumption onto the assumption stack. It will remain there until it's pop'd by pop_assumptions.

val pop_assumptions : t -> int -> unit

pop_assumptions solver n removes n assumptions from the stack. It removes the assumptions that were the most recently added via push_assumptions.

type propagation_result =
| PR_sat
| PR_conflict of {
backtracked : int;
}
| PR_unsat of (lit, clause, proof_step) unsat_state

Result returned by check_sat_propagations_only

val check_sat_propagations_only : ?assumptions:lit list -> t -> propagation_result

check_sat_propagations_only solver uses the added clauses and local assumptions (using push_assumptions and assumptions) to quickly assess whether the context is satisfiable. It is not complete; calling solve is required to get an accurate result.

  • returns

    either Ok() if propagation yielded no conflict, or Error c if a conflict clause c was found.

\ 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 4a44a600..e64c6e37 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) -> -?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 +?should_stop:(t -> int -> bool) -> assumptions:lit list -> t -> res

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

val push_assumption : t -> lit -> unit

Pushes an assumption onto the assumption stack. It will remain there until it's pop'd by pop_assumptions.

val pop_assumptions : t -> int -> unit

pop_assumptions solver n removes n assumptions from the stack. It removes the assumptions that were the most recently added via push_assumptions. Note that check_sat_propagations_only can call this if it meets a conflict.

type propagation_result =
| PR_sat
| PR_conflict of {
backtracked : int;
}
| PR_unsat of {
unsat_core : unit -> lit Iter.t;
}
val check_sat_propagations_only : assumptions:lit list -> t -> propagation_result

check_sat_propagations_only solver uses assumptions (including the assumptions parameter, and atoms previously added via push_assumptions) and boolean+theory propagation to quickly assess satisfiability. It is not complete; calling solve is required to get an accurate result.

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 f718dbc8..eaaac09e 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) -> -?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 +?should_stop:(t -> int -> bool) -> assumptions:lit list -> t -> res

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

val push_assumption : t -> lit -> unit

Pushes an assumption onto the assumption stack. It will remain there until it's pop'd by pop_assumptions.

val pop_assumptions : t -> int -> unit

pop_assumptions solver n removes n assumptions from the stack. It removes the assumptions that were the most recently added via push_assumptions. Note that check_sat_propagations_only can call this if it meets a conflict.

type propagation_result =
| PR_sat
| PR_conflict of {
backtracked : int;
}
| PR_unsat of {
unsat_core : unit -> lit Iter.t;
}
val check_sat_propagations_only : assumptions:lit list -> t -> propagation_result

check_sat_propagations_only solver uses assumptions (including the assumptions parameter, and atoms previously added via push_assumptions) and boolean+theory propagation to quickly assess satisfiability. It is not complete; calling solve is required to get an accurate result.

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 a779b5aa..e059c89f 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) -> -?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 +?should_stop:(t -> int -> bool) -> assumptions:lit list -> t -> res

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

val push_assumption : t -> lit -> unit

Pushes an assumption onto the assumption stack. It will remain there until it's pop'd by pop_assumptions.

val pop_assumptions : t -> int -> unit

pop_assumptions solver n removes n assumptions from the stack. It removes the assumptions that were the most recently added via push_assumptions. Note that check_sat_propagations_only can call this if it meets a conflict.

type propagation_result =
| PR_sat
| PR_conflict of {
backtracked : int;
}
| PR_unsat of {
unsat_core : unit -> lit Iter.t;
}
val check_sat_propagations_only : assumptions:lit list -> t -> propagation_result

check_sat_propagations_only solver uses assumptions (including the assumptions parameter, and atoms previously added via push_assumptions) and boolean+theory propagation to quickly assess satisfiability. It is not complete; calling solve is required to get an accurate result.

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 3061e0cb..f7f2d0fe 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) -> -?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 +?should_stop:(t -> int -> bool) -> assumptions:lit list -> t -> res

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

val push_assumption : t -> lit -> unit

Pushes an assumption onto the assumption stack. It will remain there until it's pop'd by pop_assumptions.

val pop_assumptions : t -> int -> unit

pop_assumptions solver n removes n assumptions from the stack. It removes the assumptions that were the most recently added via push_assumptions. Note that check_sat_propagations_only can call this if it meets a conflict.

type propagation_result =
| PR_sat
| PR_conflict of {
backtracked : int;
}
| PR_unsat of {
unsat_core : unit -> lit Iter.t;
}
val check_sat_propagations_only : assumptions:lit list -> t -> propagation_result

check_sat_propagations_only solver uses assumptions (including the assumptions parameter, and atoms previously added via push_assumptions) and boolean+theory propagation to quickly assess satisfiability. It is not complete; calling solve is required to get an accurate result.

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 20b0873c..994fe367 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) -> -?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 +?should_stop:(t -> int -> bool) -> assumptions:lit list -> t -> res

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

val push_assumption : t -> lit -> unit

Pushes an assumption onto the assumption stack. It will remain there until it's pop'd by pop_assumptions.

val pop_assumptions : t -> int -> unit

pop_assumptions solver n removes n assumptions from the stack. It removes the assumptions that were the most recently added via push_assumptions. Note that check_sat_propagations_only can call this if it meets a conflict.

type propagation_result =
| PR_sat
| PR_conflict of {
backtracked : int;
}
| PR_unsat of {
unsat_core : unit -> lit Iter.t;
}
val check_sat_propagations_only : assumptions:lit list -> t -> propagation_result

check_sat_propagations_only solver uses assumptions (including the assumptions parameter, and atoms previously added via push_assumptions) and boolean+theory propagation to quickly assess satisfiability. It is not complete; calling solve is required to get an accurate result.

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 0bb56dc4..430e38c1 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) -> -?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 +?should_stop:(t -> int -> bool) -> assumptions:lit list -> t -> res

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

val push_assumption : t -> lit -> unit

Pushes an assumption onto the assumption stack. It will remain there until it's pop'd by pop_assumptions.

val pop_assumptions : t -> int -> unit

pop_assumptions solver n removes n assumptions from the stack. It removes the assumptions that were the most recently added via push_assumptions. Note that check_sat_propagations_only can call this if it meets a conflict.

type propagation_result =
| PR_sat
| PR_conflict of {
backtracked : int;
}
| PR_unsat of {
unsat_core : unit -> lit Iter.t;
}
val check_sat_propagations_only : assumptions:lit list -> t -> propagation_result

check_sat_propagations_only solver uses assumptions (including the assumptions parameter, and atoms previously added via push_assumptions) and boolean+theory propagation to quickly assess satisfiability. It is not complete; calling solve is required to get an accurate result.

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 7ee43978..2af66162 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) -> -?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 +?should_stop:(t -> int -> bool) -> assumptions:lit list -> t -> res

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

val push_assumption : t -> lit -> unit

Pushes an assumption onto the assumption stack. It will remain there until it's pop'd by pop_assumptions.

val pop_assumptions : t -> int -> unit

pop_assumptions solver n removes n assumptions from the stack. It removes the assumptions that were the most recently added via push_assumptions. Note that check_sat_propagations_only can call this if it meets a conflict.

type propagation_result =
| PR_sat
| PR_conflict of {
backtracked : int;
}
| PR_unsat of {
unsat_core : unit -> lit Iter.t;
}
val check_sat_propagations_only : assumptions:lit list -> t -> propagation_result

check_sat_propagations_only solver uses assumptions (including the assumptions parameter, and atoms previously added via push_assumptions) and boolean+theory propagation to quickly assess satisfiability. It is not complete; calling solve is required to get an accurate result.

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 b8fb0fb8..57b8eb21 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) -> -?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 +?should_stop:(t -> int -> bool) -> assumptions:lit list -> t -> res

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

val push_assumption : t -> lit -> unit

Pushes an assumption onto the assumption stack. It will remain there until it's pop'd by pop_assumptions.

val pop_assumptions : t -> int -> unit

pop_assumptions solver n removes n assumptions from the stack. It removes the assumptions that were the most recently added via push_assumptions. Note that check_sat_propagations_only can call this if it meets a conflict.

type propagation_result =
| PR_sat
| PR_conflict of {
backtracked : int;
}
| PR_unsat of {
unsat_core : unit -> lit Iter.t;
}
val check_sat_propagations_only : assumptions:lit list -> t -> propagation_result

check_sat_propagations_only solver uses assumptions (including the assumptions parameter, and atoms previously added via push_assumptions) and boolean+theory propagation to quickly assess satisfiability. It is not complete; calling solve is required to get an accurate result.

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 a136a7a6..a7a4f5e5 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) -> -?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 +?should_stop:(t -> int -> bool) -> assumptions:lit list -> t -> res

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

val push_assumption : t -> lit -> unit

Pushes an assumption onto the assumption stack. It will remain there until it's pop'd by pop_assumptions.

val pop_assumptions : t -> int -> unit

pop_assumptions solver n removes n assumptions from the stack. It removes the assumptions that were the most recently added via push_assumptions. Note that check_sat_propagations_only can call this if it meets a conflict.

type propagation_result =
| PR_sat
| PR_conflict of {
backtracked : int;
}
| PR_unsat of {
unsat_core : unit -> lit Iter.t;
}
val check_sat_propagations_only : assumptions:lit list -> t -> propagation_result

check_sat_propagations_only solver uses assumptions (including the assumptions parameter, and atoms previously added via push_assumptions) and boolean+theory propagation to quickly assess satisfiability. It is not complete; calling solve is required to get an accurate result.

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 8e80d430..2ef8b738 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) -> -?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 +?should_stop:(t -> int -> bool) -> assumptions:lit list -> t -> res

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

val push_assumption : t -> lit -> unit

Pushes an assumption onto the assumption stack. It will remain there until it's pop'd by pop_assumptions.

val pop_assumptions : t -> int -> unit

pop_assumptions solver n removes n assumptions from the stack. It removes the assumptions that were the most recently added via push_assumptions. Note that check_sat_propagations_only can call this if it meets a conflict.

type propagation_result =
| PR_sat
| PR_conflict of {
backtracked : int;
}
| PR_unsat of {
unsat_core : unit -> lit Iter.t;
}
val check_sat_propagations_only : assumptions:lit list -> t -> propagation_result

check_sat_propagations_only solver uses assumptions (including the assumptions parameter, and atoms previously added via push_assumptions) and boolean+theory propagation to quickly assess satisfiability. It is not complete; calling solve is required to get an accurate result.

val pp_stats : t CCFormat.printer

Print some statistics. What it prints exactly is unspecified.

\ No newline at end of file