diff --git a/dev/sidekick-base/Sidekick_base/Solver/Unknown/index.html b/dev/sidekick-base/Sidekick_base/Solver/Unknown/index.html deleted file mode 100644 index 4024fc30..00000000 --- a/dev/sidekick-base/Sidekick_base/Solver/Unknown/index.html +++ /dev/null @@ -1,2 +0,0 @@ - -Unknown (sidekick-base.Sidekick_base.Solver.Unknown)

Module Solver.Unknown

type t
val pp : t CCFormat.printer
\ No newline at end of file diff --git a/dev/sidekick-base/Sidekick_base/Solver/index.html b/dev/sidekick-base/Sidekick_base/Solver/index.html index 28788237..a2f7ffda 100644 --- a/dev/sidekick-base/Sidekick_base/Solver/index.html +++ b/dev/sidekick-base/Sidekick_base/Solver/index.html @@ -1,5 +1,5 @@ -Solver (sidekick-base.Sidekick_base.Solver)

Module Sidekick_base.Solver

include module type of struct include Sidekick_smt_solver.Solver end
type t

The solver's state.

A solver contains a registry so that theories can share data

val mk_theory : +Solver (sidekick-base.Sidekick_base.Solver)

Module Sidekick_base.Solver

include module type of struct include Sidekick_smt_solver.Solver end
type t

The solver's state.

A solver contains a registry so that theories can share data

val mk_theory : name:string -> create_and_setup: ( id:Sidekick_smt_solver.Theory_id.t -> @@ -8,7 +8,7 @@ ?push_level:( 'th -> unit ) -> ?pop_levels:( 'th -> int -> unit ) -> unit -> - Sidekick_smt_solver.Theory.t

Helper to create a theory.

module Unknown : sig ... end

Main API

val stats : t -> Sidekick_util.Stat.t

Helper to create a theory.

Main API

val stats : t -> Sidekick_util.Stat.t
val create : (module Sidekick_smt_solver.Sigs.ARG) -> ?stat:Sidekick_util.Stat.t -> ?size:[ `Big | `Tiny | `Small ] -> @@ -29,14 +29,13 @@ t -> Sidekick_smt_solver.Sigs.lit list -> Sidekick_smt_solver.Sigs.step_id -> - unit

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

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

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

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

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

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

Satisfiable

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

Unsat core (subset of assumptions), or empty

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

Proof step for the empty clause

*)
}		(*

Unsatisfiable

*)
| Unknown of Unknown.t(*

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

*)

Result of solving for the current set of clauses

val solve : + unit

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

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

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

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

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

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

Satisfiable

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

Unsat core (subset of assumptions), or empty

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

Proof step for the empty clause

*)
}		(*

Unsatisfiable

*)
| Unknown of Unknown.t(*

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

*)

Result of solving for the current set of clauses

val solve : ?on_exit:( unit -> unit ) list -> - ?check:bool -> - ?on_progress:( t -> unit ) -> - ?should_stop:( t -> int -> bool ) -> + ?on_progress:( unit -> unit ) -> + ?should_stop:( int -> bool ) -> assumptions:Sidekick_smt_solver.Sigs.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 last_res : t -> res option

Last result, if any. Some operations will erase this (e.g. assert_term).

val push_assumption : t -> Sidekick_smt_solver.Sigs.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 -> Sidekick_smt_solver.Sigs.lit Iter.t;
}
val check_sat_propagations_only : + res

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

  • 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 from within the solver. It is given 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

Comply to the abstract solver interface

val last_res : t -> res option

Last result, if any. Some operations will erase this (e.g. assert_term).

val push_assumption : t -> Sidekick_smt_solver.Sigs.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 -> Sidekick_smt_solver.Sigs.lit Iter.t;
}
val check_sat_propagations_only : assumptions:Sidekick_smt_solver.Sigs.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.

  • returns

    one of:

    • PR_sat if the current state seems satisfiable
    • PR_conflict {backtracked=n} if a conflict was found and resolved, leading to backtracking n levels of assumptions
    • PR_unsat … if the assumptions were found to be unsatisfiable, with the given core.
val pp_stats : t CCFormat.printer

Print some statistics. What it prints exactly is unspecified.

val default_arg : (module Sidekick_smt_solver.Sigs.ARG)
val create_default : diff --git a/dev/sidekick-bin/Sidekick_smtlib/.dummy b/dev/sidekick-base/Sidekick_smtlib/.dummy similarity index 100% rename from dev/sidekick-bin/Sidekick_smtlib/.dummy rename to dev/sidekick-base/Sidekick_smtlib/.dummy diff --git a/dev/sidekick-base/Sidekick_smtlib/Check_cc/index.html b/dev/sidekick-base/Sidekick_smtlib/Check_cc/index.html new file mode 100644 index 00000000..dbe08262 --- /dev/null +++ b/dev/sidekick-base/Sidekick_smtlib/Check_cc/index.html @@ -0,0 +1,2 @@ + +Check_cc (sidekick-base.Sidekick_smtlib.Check_cc)

Module Sidekick_smtlib.Check_cc

val theory : Solver.cdcl_theory

theory that check validity of EUF conflicts, on the fly

\ No newline at end of file diff --git a/dev/sidekick-base/Sidekick_smtlib/Driver/index.html b/dev/sidekick-base/Sidekick_smtlib/Driver/index.html new file mode 100644 index 00000000..b1b7f887 --- /dev/null +++ b/dev/sidekick-base/Sidekick_smtlib/Driver/index.html @@ -0,0 +1,12 @@ + +Driver (sidekick-base.Sidekick_smtlib.Driver)

Module Sidekick_smtlib.Driver

Driver.

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

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

The SMTLIB driver

val create : + ?restarts:bool -> + ?pp_cnf:bool -> + ?proof_file:string -> + ?pp_model:bool -> + ?check:bool -> + ?time:float -> + ?memory:float -> + ?progress:bool -> + Asolver.t -> + t
val process_stmt : t -> Sidekick_base.Statement.t -> unit or_error
\ No newline at end of file diff --git a/dev/sidekick-base/Sidekick_smtlib/Solver/index.html b/dev/sidekick-base/Sidekick_smtlib/Solver/index.html new file mode 100644 index 00000000..1a185697 --- /dev/null +++ b/dev/sidekick-base/Sidekick_smtlib/Solver/index.html @@ -0,0 +1,2 @@ + +Solver (sidekick-base.Sidekick_smtlib.Solver)

Module Sidekick_smtlib.Solver

module Smt_solver = Sidekick_smt_solver
type t = Asolver.t
type cdcl_theory = Smt_solver.theory
\ No newline at end of file diff --git a/dev/sidekick-base/Sidekick_smtlib/index.html b/dev/sidekick-base/Sidekick_smtlib/index.html new file mode 100644 index 00000000..ee291fe1 --- /dev/null +++ b/dev/sidekick-base/Sidekick_smtlib/index.html @@ -0,0 +1,2 @@ + +Sidekick_smtlib (sidekick-base.Sidekick_smtlib)

Module Sidekick_smtlib

SMTLib-2.6 Driver

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

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

Driver.

module Solver : sig ... end
module Proof_trace = Sidekick_core.Proof_trace
module Check_cc : sig ... end
val parse : Term.store -> string -> Stmt.t list or_error
val parse_stdin : Term.store -> Stmt.t list or_error
\ No newline at end of file diff --git a/dev/sidekick-base/index.html b/dev/sidekick-base/index.html index ba47675a..cb51efa1 100644 --- a/dev/sidekick-base/index.html +++ b/dev/sidekick-base/index.html @@ -1,2 +1,2 @@ -index (sidekick-base.index)

sidekick-base index

Library sidekick-base

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

Library sidekick-base.proof-trace

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

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

sidekick-base index

Library sidekick-base

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

Library sidekick-base.proof-trace

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

Library sidekick-base.smtlib

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

\ No newline at end of file diff --git a/dev/sidekick-bin/Sidekick_smtlib/Process/Check_cc/index.html b/dev/sidekick-bin/Sidekick_smtlib/Process/Check_cc/index.html deleted file mode 100644 index 79c96e84..00000000 --- a/dev/sidekick-bin/Sidekick_smtlib/Process/Check_cc/index.html +++ /dev/null @@ -1,2 +0,0 @@ - -Check_cc (sidekick-bin.Sidekick_smtlib.Process.Check_cc)

Module Process.Check_cc

val theory : Solver.theory

theory that check validity of conflicts

\ No newline at end of file diff --git a/dev/sidekick-bin/Sidekick_smtlib/Process/index.html b/dev/sidekick-bin/Sidekick_smtlib/Process/index.html deleted file mode 100644 index 5c197c2b..00000000 --- a/dev/sidekick-bin/Sidekick_smtlib/Process/index.html +++ /dev/null @@ -1,14 +0,0 @@ - -Process (sidekick-bin.Sidekick_smtlib.Process)

Module Sidekick_smtlib.Process

Process Statements

module Solver = Sidekick_base.Solver
val th_bool_dyn : Solver.theory
val th_bool_static : Solver.theory
val th_data : Solver.theory
val th_lra : Solver.theory
val th_ty_unin : Solver.theory
type 'a or_error = ( 'a, string ) CCResult.t
module Check_cc : sig ... end
val process_stmt : - ?gc:bool -> - ?restarts:bool -> - ?pp_cnf:bool -> - ?proof_file:string -> - ?pp_model:bool -> - ?check:bool -> - ?time:float -> - ?memory:float -> - ?progress:bool -> - Solver.t -> - Sidekick_base.Statement.t -> - unit or_error
\ No newline at end of file diff --git a/dev/sidekick-bin/Sidekick_smtlib/index.html b/dev/sidekick-bin/Sidekick_smtlib/index.html deleted file mode 100644 index 078f9597..00000000 --- a/dev/sidekick-bin/Sidekick_smtlib/index.html +++ /dev/null @@ -1,2 +0,0 @@ - -Sidekick_smtlib (sidekick-bin.Sidekick_smtlib)

Module Sidekick_smtlib

SMTLib-2 Interface

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

type 'a or_error = ( 'a, string ) CCResult.t
module Term = Sidekick_base.Term
module Process : sig ... end
module Solver = Process.Solver
module Proof_trace = Sidekick_core.Proof_trace
val parse : Term.store -> string -> Stmt.t list or_error
val parse_stdin : Term.store -> Stmt.t list or_error
\ No newline at end of file diff --git a/dev/sidekick-bin/index.html b/dev/sidekick-bin/index.html index fb86a6dc..24e673c6 100644 --- a/dev/sidekick-bin/index.html +++ b/dev/sidekick-bin/index.html @@ -1,2 +1,2 @@ -index (sidekick-bin.index)

sidekick-bin index

Library sidekick-bin.lib

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

Library sidekick-bin.smtlib

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

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

sidekick-bin index

Library sidekick-bin.lib

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

\ No newline at end of file diff --git a/dev/sidekick/Sidekick_abstract_solver/.dummy b/dev/sidekick/Sidekick_abstract_solver/.dummy new file mode 100644 index 00000000..e69de29b diff --git a/dev/sidekick/Sidekick_abstract_solver/Asolver/class-type-t/index.html b/dev/sidekick/Sidekick_abstract_solver/Asolver/class-type-t/index.html new file mode 100644 index 00000000..adf78554 --- /dev/null +++ b/dev/sidekick/Sidekick_abstract_solver/Asolver/class-type-t/index.html @@ -0,0 +1,11 @@ + +t (sidekick.Sidekick_abstract_solver.Asolver.t)

Class type Asolver.t

method assert_term : Sidekick_core.Term.t -> unit

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

This uses Proof_sat.sat_input_clause to justify the assertion.

method assert_clause : Sidekick_core.Lit.t array -> + Sidekick_core.Proof_step.id -> + unit

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

method assert_clause_l : Sidekick_core.Lit.t list -> + Sidekick_core.Proof_step.id -> + unit

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

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

Add a new sort/atomic type.

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

Convert a term into a simplified literal.

method solve : ?on_exit:( unit -> unit ) list -> + ?on_progress:( unit -> unit ) -> + ?should_stop:( int -> bool ) -> + assumptions:Sidekick_core.Lit.t list -> + unit -> + Check_res.t

Checks the satisfiability of the clauses added so far to the solver.

  • parameter assumptions

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

  • parameter on_progress

    called regularly during solving.

  • parameter should_stop

    a callback regularly called from within the solver. It is given 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

method last_res : Check_res.t option

Returns the result of the last call to solve, if the logic statee has not changed (mostly by asserting new clauses).

TODO: remove, use Tracer instead

\ No newline at end of file diff --git a/dev/sidekick/Sidekick_abstract_solver/Asolver/index.html b/dev/sidekick/Sidekick_abstract_solver/Asolver/index.html new file mode 100644 index 00000000..408bddec --- /dev/null +++ b/dev/sidekick/Sidekick_abstract_solver/Asolver/index.html @@ -0,0 +1,21 @@ + +Asolver (sidekick.Sidekick_abstract_solver.Asolver)

Module Sidekick_abstract_solver.Asolver

Abstract interface for a solver

module Unknown = Unknown
module Check_res = Check_res
class type t = object ... end
val assert_term : t -> Sidekick_core.Term.t -> unit
val assert_clause : + t -> + Sidekick_core.Lit.t array -> + Sidekick_core.Proof_step.id -> + unit
val assert_clause_l : + t -> + Sidekick_core.Lit.t list -> + Sidekick_core.Proof_step.id -> + unit
val add_ty : t -> ty:Sidekick_core.Term.t -> unit
val lit_of_term : + t -> + ?sign:bool -> + Sidekick_core.Term.t -> + Sidekick_core.Lit.t
val solve : + t -> + ?on_exit:( unit -> unit ) list -> + ?on_progress:( unit -> unit ) -> + ?should_stop:( int -> bool ) -> + assumptions:Sidekick_core.Lit.t list -> + unit -> + Check_res.t
val last_res : t -> Check_res.t option
\ No newline at end of file diff --git a/dev/sidekick/Sidekick_abstract_solver/Check_res/index.html b/dev/sidekick/Sidekick_abstract_solver/Check_res/index.html new file mode 100644 index 00000000..445e990e --- /dev/null +++ b/dev/sidekick/Sidekick_abstract_solver/Check_res/index.html @@ -0,0 +1,2 @@ + +Check_res (sidekick.Sidekick_abstract_solver.Check_res)

Module Sidekick_abstract_solver.Check_res

Result of solving for the current set of clauses

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

Satisfiable

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

Unsat core (subset of assumptions), or empty

*)
unsat_step_id : unit -> Sidekick_core.Proof_trace.step_id option;(*

Proof step for the empty clause

*)
}		(*

Unsatisfiable

*)
| Unknown of Unknown.t(*

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

*)

Result of calling "check"

val pp : Sidekick_core.Fmt.t -> t -> unit
\ No newline at end of file diff --git a/dev/sidekick/Sidekick_abstract_solver/Unknown/index.html b/dev/sidekick/Sidekick_abstract_solver/Unknown/index.html new file mode 100644 index 00000000..ed150143 --- /dev/null +++ b/dev/sidekick/Sidekick_abstract_solver/Unknown/index.html @@ -0,0 +1,2 @@ + +Unknown (sidekick.Sidekick_abstract_solver.Unknown)

Module Sidekick_abstract_solver.Unknown

type t =
| U_timeout
| U_max_depth
| U_incomplete
| U_asked_to_stop
val pp : t Sidekick_core.Fmt.printer
\ No newline at end of file diff --git a/dev/sidekick/Sidekick_abstract_solver/class-type-t/index.html b/dev/sidekick/Sidekick_abstract_solver/class-type-t/index.html new file mode 100644 index 00000000..e4b37f32 --- /dev/null +++ b/dev/sidekick/Sidekick_abstract_solver/class-type-t/index.html @@ -0,0 +1,11 @@ + +t (sidekick.Sidekick_abstract_solver.t)

Class type Sidekick_abstract_solver.t

Main abstract solver type

method assert_term : Sidekick_core.Term.t -> unit

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

This uses Proof_sat.sat_input_clause to justify the assertion.

method assert_clause : Sidekick_core.Lit.t array -> + Sidekick_core.Proof_step.id -> + unit

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

method assert_clause_l : Sidekick_core.Lit.t list -> + Sidekick_core.Proof_step.id -> + unit

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

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

Add a new sort/atomic type.

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

Convert a term into a simplified literal.

method solve : ?on_exit:( unit -> unit ) list -> + ?on_progress:( unit -> unit ) -> + ?should_stop:( int -> bool ) -> + assumptions:Sidekick_core.Lit.t list -> + unit -> + Asolver.Check_res.t

Checks the satisfiability of the clauses added so far to the solver.

  • parameter assumptions

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

  • parameter on_progress

    called regularly during solving.

  • parameter should_stop

    a callback regularly called from within the solver. It is given 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

method last_res : Asolver.Check_res.t option

Returns the result of the last call to solve, if the logic statee has not changed (mostly by asserting new clauses).

TODO: remove, use Tracer instead

\ No newline at end of file diff --git a/dev/sidekick/Sidekick_abstract_solver/index.html b/dev/sidekick/Sidekick_abstract_solver/index.html new file mode 100644 index 00000000..c9d16554 --- /dev/null +++ b/dev/sidekick/Sidekick_abstract_solver/index.html @@ -0,0 +1,2 @@ + +Sidekick_abstract_solver (sidekick.Sidekick_abstract_solver)

Module Sidekick_abstract_solver

Abstract interface for a solver

module Unknown : sig ... end
module Check_res : sig ... end

Result of solving for the current set of clauses

module Asolver : sig ... end

Abstract interface for a solver

class type t = Asolver.t

Main abstract solver type

\ No newline at end of file diff --git a/dev/sidekick/Sidekick_smt_solver/Solver/Unknown/index.html b/dev/sidekick/Sidekick_smt_solver/Solver/Unknown/index.html deleted file mode 100644 index af576ecb..00000000 --- a/dev/sidekick/Sidekick_smt_solver/Solver/Unknown/index.html +++ /dev/null @@ -1,2 +0,0 @@ - -Unknown (sidekick.Sidekick_smt_solver.Solver.Unknown)

Module Solver.Unknown

type t
val pp : t CCFormat.printer
\ No newline at end of file diff --git a/dev/sidekick/Sidekick_smt_solver/Solver/index.html b/dev/sidekick/Sidekick_smt_solver/Solver/index.html index e6995bcc..1eeba185 100644 --- a/dev/sidekick/Sidekick_smt_solver/Solver/index.html +++ b/dev/sidekick/Sidekick_smt_solver/Solver/index.html @@ -1,11 +1,11 @@ -Solver (sidekick.Sidekick_smt_solver.Solver)

Module Sidekick_smt_solver.Solver

Main solver type, user facing.

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.

type t

The solver's state.

val registry : t -> Registry.t

A solver contains a registry so that theories can share data

type theory = Theory.t
val mk_theory : +Solver (sidekick.Sidekick_smt_solver.Solver)

Module Sidekick_smt_solver.Solver

Main solver type, user facing.

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.

type t

The solver's state.

val registry : t -> Registry.t

A solver contains a registry so that theories can share data

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

Helper to create a theory.

module Unknown : sig ... end

Main API

val stats : t -> Sidekick_util.Stat.t
val tst : t -> Sigs.Term.store
val proof : t -> Sigs.proof_trace
val create : + Theory.t

Helper to create a theory.

Main API

val stats : t -> Sidekick_util.Stat.t
val tst : t -> Sigs.Term.store
val proof : t -> Sigs.proof_trace
val create : (module Sigs.ARG) -> ?stat:Sidekick_util.Stat.t -> ?size:[ `Big | `Tiny | `Small ] -> @@ -22,14 +22,13 @@ theories:Theory.t list -> Sigs.Term.store -> unit -> - t

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

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

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

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

Add the given theory and obtain its state

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

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

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

val add_clause : t -> Sigs.lit array -> Sigs.step_id -> unit

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

val add_clause_l : t -> Sigs.lit list -> Sigs.step_id -> unit

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

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

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

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

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

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

Satisfiable

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

Unsat core (subset of assumptions), or empty

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

Proof step for the empty clause

*)
}		(*

Unsatisfiable

*)
| Unknown of Unknown.t(*

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

*)

Result of solving for the current set of clauses

val solve : + t

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

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

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

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

Add the given theory and obtain its state

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

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

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

val add_clause : t -> Sigs.lit array -> Sigs.step_id -> unit

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

val add_clause_l : t -> Sigs.lit list -> Sigs.step_id -> unit

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

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

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

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

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

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

Satisfiable

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

Unsat core (subset of assumptions), or empty

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

Proof step for the empty clause

*)
}		(*

Unsatisfiable

*)
| Unknown of Unknown.t(*

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

*)

Result of solving for the current set of clauses

val solve : ?on_exit:( unit -> unit ) list -> - ?check:bool -> - ?on_progress:( t -> unit ) -> - ?should_stop:( t -> int -> bool ) -> + ?on_progress:( unit -> unit ) -> + ?should_stop:( int -> bool ) -> assumptions:Sigs.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 last_res : t -> res option

Last result, if any. Some operations will erase this (e.g. assert_term).

val push_assumption : t -> Sigs.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 -> Sigs.lit Iter.t;
}
val check_sat_propagations_only : + res

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

  • 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 from within the solver. It is given 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

Comply to the abstract solver interface

val last_res : t -> res option

Last result, if any. Some operations will erase this (e.g. assert_term).

val push_assumption : t -> Sigs.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 -> Sigs.lit Iter.t;
}
val check_sat_propagations_only : assumptions:Sigs.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.

  • returns

    one of:

    • PR_sat if the current state seems satisfiable
    • PR_conflict {backtracked=n} if a conflict was found and resolved, leading to backtracking n levels of assumptions
    • PR_unsat … if the assumptions were found to be unsatisfiable, with the given core.
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/index.html b/dev/sidekick/index.html index 9bcd3ef2..a10b30d4 100644 --- a/dev/sidekick/index.html +++ b/dev/sidekick/index.html @@ -1,2 +1,2 @@ -index (sidekick.index)

sidekick index

Library sidekick.arith

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

Library sidekick.bencode

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

Library sidekick.cc

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

Library sidekick.cc.plugin

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

Library sidekick.core

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

Library sidekick.core-logic

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

Library sidekick.drup

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

Library sidekick.memtrace

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

Library sidekick.mini-cc

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

Library sidekick.model

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

Library sidekick.quip

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

Library sidekick.sat

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

Library sidekick.sigs

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

Library sidekick.simplex

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

Library sidekick.simplify

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

Library sidekick.smt-solver

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

Library sidekick.tef

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

Library sidekick.th-bool-dyn

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

Library sidekick.th-bool-static

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

Library sidekick.th-cstor

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

Library sidekick.th-data

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

Library sidekick.th-lra

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

Library sidekick.th-ty-unin

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

Library sidekick.trace

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

Library sidekick.util

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

Library sidekick.zarith

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

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

sidekick index

Library sidekick.abstract-solver

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

Library sidekick.arith

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

Library sidekick.bencode

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

Library sidekick.cc

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

Library sidekick.cc.plugin

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

Library sidekick.core

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

Library sidekick.core-logic

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

Library sidekick.drup

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

Library sidekick.memtrace

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

Library sidekick.mini-cc

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

Library sidekick.model

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

Library sidekick.quip

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

Library sidekick.sat

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

Library sidekick.sigs

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

Library sidekick.simplex

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

Library sidekick.simplify

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

Library sidekick.smt-solver

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

Library sidekick.tef

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

Library sidekick.th-bool-dyn

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

Library sidekick.th-bool-static

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

Library sidekick.th-cstor

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

Library sidekick.th-data

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

Library sidekick.th-lra

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

Library sidekick.th-ty-unin

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

Library sidekick.trace

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

Library sidekick.util

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

Library sidekick.zarith

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

\ No newline at end of file