From 54f90282b9966f85fd63812b8c7dbd1785ce22ee Mon Sep 17 00:00:00 2001 From: c-cube Date: Fri, 11 Jun 2021 23:00:26 +0000 Subject: [PATCH] deploy: dcbc4d4a593c2fed35807b6c0f687ab315eb8345 --- dev/sidekick/Sidekick_msat_solver/Make/index.html | 2 +- dev/sidekick/Sidekick_msat_solver/index.html | 2 +- dev/sidekick/Sidekick_msat_solver/module-type-ARG/index.html | 2 +- .../Sidekick_th_bool_static/Make/argument-1-A/Gensym/index.html | 2 +- .../Sidekick_th_bool_static/Make/argument-1-A/index.html | 2 +- dev/sidekick/Sidekick_th_bool_static/Make/index.html | 2 +- dev/sidekick/Sidekick_th_bool_static/index.html | 2 +- .../Sidekick_th_bool_static/module-type-ARG/Gensym/index.html | 2 +- dev/sidekick/Sidekick_th_bool_static/module-type-ARG/index.html | 2 +- .../Sidekick_th_bool_static/module-type-S/A/Gensym/index.html | 2 +- dev/sidekick/Sidekick_th_bool_static/module-type-S/A/index.html | 2 +- dev/sidekick/Sidekick_th_bool_static/module-type-S/index.html | 2 +- .../Sidekick_th_data/Make/argument-1-A/Cstor/index.html | 2 +- dev/sidekick/Sidekick_th_data/Make/argument-1-A/index.html | 2 +- dev/sidekick/Sidekick_th_data/Make/index.html | 2 +- dev/sidekick/Sidekick_th_data/index.html | 2 +- dev/sidekick/Sidekick_th_data/module-type-ARG/Cstor/index.html | 2 +- dev/sidekick/Sidekick_th_data/module-type-ARG/index.html | 2 +- dev/sidekick/Sidekick_th_data/module-type-S/A/Cstor/index.html | 2 +- dev/sidekick/Sidekick_th_data/module-type-S/A/index.html | 2 +- dev/sidekick/Sidekick_th_data/module-type-S/index.html | 2 +- 21 files changed, 21 insertions(+), 21 deletions(-) diff --git a/dev/sidekick/Sidekick_msat_solver/Make/index.html b/dev/sidekick/Sidekick_msat_solver/Make/index.html index 8249c1e2..1ba63c41 100644 --- a/dev/sidekick/Sidekick_msat_solver/Make/index.html +++ b/dev/sidekick/Sidekick_msat_solver/Make/index.html @@ -1,2 +1,2 @@ -Make (sidekick.Sidekick_msat_solver.Make)

Module Sidekick_msat_solver.Make

Parameters

Signature

module T = A.T
module P = A.P
module Lit : Sidekick_core.LIT with module T = T
module Solver_internal : Sidekick_core.SOLVER_INTERNAL with module T = T and module P = P and module Lit = Lit

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
type lemma = P.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 Atom : sig ... end
module Model : sig ... end

Models

module Unknown : sig ... end
module Proof : sig ... end
type proof = Proof.t

Main API

val stats : t -> Sidekick_util.Stat.t
val tst : t -> T.Term.state
val ty_st : t -> T.Ty.state
val create : ?⁠stat:Sidekick_util.Stat.t -> ?⁠size:[ `Big | `Tiny | `Small ] -> ?⁠store_proof:bool -> theories:theory list -> T.Term.state -> T.Ty.state -> 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_atom_lit : t -> lit -> Atom.t

Turn a literal into a SAT solver literal.

val mk_atom_t : t -> ?⁠sign:bool -> term -> Atom.t

Turn a boolean term, with a sign, into a SAT solver's literal.

val add_clause : t -> Atom.t Sidekick_util.IArray.t -> 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 -> Atom.t list -> unit

Same as add_clause but with a list of atoms.

type res =
| Sat of Model.t

Satisfiable

| Unsat of {
proof : proof option lazy_t;

proof of unsat

unsat_core : Atom.t list lazy_t;

subset of assumptions responsible for unsat

}

Unsatisfiable

| Unknown of Unknown.t

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

Result of solving for the current set of clauses

val solve : ?⁠on_exit:(unit -> unit) list -> ?⁠check:bool -> ?⁠on_progress:(t -> unit) -> assumptions:Atom.t list -> t -> res

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

parameter check

if true, the model is checked before returning.

parameter on_progress

called regularly during solving.

parameter assumptions

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

parameter on_exit

functions to be run before this returns

val pp_stats : t CCFormat.printer

Print some statistics. What it prints exactly is unspecified.

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

Module Sidekick_msat_solver.Make

Main functor to get a solver.

Parameters

Signature

module T = A.T
module P = A.P
module Lit : Sidekick_core.LIT with module T = T
module Solver_internal : Sidekick_core.SOLVER_INTERNAL with module T = T and module P = P and module Lit = Lit

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
type lemma = P.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 Atom : sig ... end
module Model : sig ... end

Models

module Unknown : sig ... end
module Proof : sig ... end
type proof = Proof.t

Main API

val stats : t -> Sidekick_util.Stat.t
val tst : t -> T.Term.state
val ty_st : t -> T.Ty.state
val create : ?⁠stat:Sidekick_util.Stat.t -> ?⁠size:[ `Big | `Tiny | `Small ] -> ?⁠store_proof:bool -> theories:theory list -> T.Term.state -> T.Ty.state -> 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_atom_lit : t -> lit -> Atom.t

Turn a literal into a SAT solver literal.

val mk_atom_t : t -> ?⁠sign:bool -> term -> Atom.t

Turn a boolean term, with a sign, into a SAT solver's literal.

val add_clause : t -> Atom.t Sidekick_util.IArray.t -> 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 -> Atom.t list -> unit

Same as add_clause but with a list of atoms.

type res =
| Sat of Model.t

Satisfiable

| Unsat of {
proof : proof option lazy_t;

proof of unsat

unsat_core : Atom.t list lazy_t;

subset of assumptions responsible for unsat

}

Unsatisfiable

| Unknown of Unknown.t

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

Result of solving for the current set of clauses

val solve : ?⁠on_exit:(unit -> unit) list -> ?⁠check:bool -> ?⁠on_progress:(t -> unit) -> assumptions:Atom.t list -> t -> res

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

parameter check

if true, the model is checked before returning.

parameter on_progress

called regularly during solving.

parameter assumptions

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

parameter on_exit

functions to be run before this returns

val pp_stats : t CCFormat.printer

Print some statistics. What it prints exactly is unspecified.

\ No newline at end of file diff --git a/dev/sidekick/Sidekick_msat_solver/index.html b/dev/sidekick/Sidekick_msat_solver/index.html index b4bed888..791da306 100644 --- a/dev/sidekick/Sidekick_msat_solver/index.html +++ b/dev/sidekick/Sidekick_msat_solver/index.html @@ -1,2 +1,2 @@ -Sidekick_msat_solver (sidekick.Sidekick_msat_solver)

Module Sidekick_msat_solver

Implementation of a Solver using Msat

module Log = Msat.Log
module type ARG = sig ... end
module type S = Sidekick_core.SOLVER
module Make : functor (A : ARG) -> S with module T = A.T and module P = A.P
\ No newline at end of file +Sidekick_msat_solver (sidekick.Sidekick_msat_solver)

Module Sidekick_msat_solver

Implementation of a Solver using Msat

module Log = Msat.Log

A logging module

module type ARG = sig ... end

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

module type S = Sidekick_core.SOLVER
module Make : functor (A : ARG) -> S with module T = A.T and module P = A.P

Main functor to get a solver.

\ No newline at end of file diff --git a/dev/sidekick/Sidekick_msat_solver/module-type-ARG/index.html b/dev/sidekick/Sidekick_msat_solver/module-type-ARG/index.html index 6e5cf069..b80c94ce 100644 --- a/dev/sidekick/Sidekick_msat_solver/module-type-ARG/index.html +++ b/dev/sidekick/Sidekick_msat_solver/module-type-ARG/index.html @@ -1,2 +1,2 @@ -ARG (sidekick.Sidekick_msat_solver.ARG)

Module type Sidekick_msat_solver.ARG

val cc_view : T.Term.t -> (T.Fun.t, T.Term.t, T.Term.t Iter.t) Sidekick_core.CC_view.t
val is_valid_literal : T.Term.t -> bool

Is this a valid boolean literal? (e.g. is it a closed term, not inside a quantifier)

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

Module type Sidekick_msat_solver.ARG

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

val cc_view : T.Term.t -> (T.Fun.t, T.Term.t, T.Term.t Iter.t) Sidekick_core.CC_view.t
val is_valid_literal : T.Term.t -> bool

Is this a valid boolean literal? (e.g. is it a closed term, not inside a quantifier)

\ No newline at end of file diff --git a/dev/sidekick/Sidekick_th_bool_static/Make/argument-1-A/Gensym/index.html b/dev/sidekick/Sidekick_th_bool_static/Make/argument-1-A/Gensym/index.html index bafbefc4..565722d1 100644 --- a/dev/sidekick/Sidekick_th_bool_static/Make/argument-1-A/Gensym/index.html +++ b/dev/sidekick/Sidekick_th_bool_static/Make/argument-1-A/Gensym/index.html @@ -1,2 +1,2 @@ -Gensym (sidekick.Sidekick_th_bool_static.Make.1-A.Gensym)

Module 1-A.Gensym

type t
val create : S.T.Term.state -> t
val fresh_term : t -> pre:string -> S.T.Ty.t -> term

Make a fresh term of the given type

\ No newline at end of file +Gensym (sidekick.Sidekick_th_bool_static.Make.1-A.Gensym)

Module 1-A.Gensym

Fresh symbol generator.

The theory needs to be able to create new terms with fresh names, to be used as placeholders for complex formulas during Tseitin encoding.

type t
val create : S.T.Term.state -> t

New (stateful) generator instance.

val fresh_term : t -> pre:string -> S.T.Ty.t -> term

Make a fresh term of the given type

\ No newline at end of file diff --git a/dev/sidekick/Sidekick_th_bool_static/Make/argument-1-A/index.html b/dev/sidekick/Sidekick_th_bool_static/Make/argument-1-A/index.html index 85a8f1ea..43fdc5b1 100644 --- a/dev/sidekick/Sidekick_th_bool_static/Make/argument-1-A/index.html +++ b/dev/sidekick/Sidekick_th_bool_static/Make/argument-1-A/index.html @@ -1,2 +1,2 @@ -1-A (sidekick.Sidekick_th_bool_static.Make.1-A)

Parameter Make.1-A

type term = S.T.Term.t
val view_as_bool : term -> (term, term Iter.t) bool_view

Project the term into the boolean view

val mk_bool : S.T.Term.state -> (term, term Sidekick_util.IArray.t) bool_view -> term

Make a term from the given boolean view

val check_congruence_classes : bool

Configuration: add final-check handler to verify if new boolean formulas are present in the congruence closure. Only enable if some theories are susceptible to create boolean formulas during the proof search.

module Gensym : sig ... end
\ No newline at end of file +1-A (sidekick.Sidekick_th_bool_static.Make.1-A)

Parameter Make.1-A

type term = S.T.Term.t
val view_as_bool : term -> (term, term Iter.t) bool_view

Project the term into the boolean view.

val mk_bool : S.T.Term.state -> (term, term Sidekick_util.IArray.t) bool_view -> term

Make a term from the given boolean view.

val check_congruence_classes : bool

Configuration: add final-check handler to verify if new boolean formulas are present in the congruence closure. Only enable if some theories are susceptible to create boolean formulas during the proof search.

module Gensym : sig ... end

Fresh symbol generator.

\ No newline at end of file diff --git a/dev/sidekick/Sidekick_th_bool_static/Make/index.html b/dev/sidekick/Sidekick_th_bool_static/Make/index.html index 27d7c40b..81e7019e 100644 --- a/dev/sidekick/Sidekick_th_bool_static/Make/index.html +++ b/dev/sidekick/Sidekick_th_bool_static/Make/index.html @@ -1,2 +1,2 @@ -Make (sidekick.Sidekick_th_bool_static.Make)

Module Sidekick_th_bool_static.Make

Parameters

Signature

module A = A
type state
val create : A.S.T.Term.state -> A.S.T.Ty.state -> state
val simplify : state -> A.S.Solver_internal.simplify_hook

Simplify given term

val cnf : state -> A.S.Solver_internal.preprocess_hook

add clauses for the booleans within the term.

val theory : A.S.theory
\ No newline at end of file +Make (sidekick.Sidekick_th_bool_static.Make)

Module Sidekick_th_bool_static.Make

Parameters

Signature

module A = A
type state
val create : A.S.T.Term.state -> A.S.T.Ty.state -> state
val simplify : state -> A.S.Solver_internal.simplify_hook

Simplify given term

val cnf : state -> A.S.Solver_internal.preprocess_hook

preprocesses formulas by giving them names and adding clauses to equate the name with the boolean formula.

val theory : A.S.theory

A theory that can be added to the solver A.S.

This theory does most of its work during preprocessing, turning boolean formulas into SAT clauses via the Tseitin encoding .

\ No newline at end of file diff --git a/dev/sidekick/Sidekick_th_bool_static/index.html b/dev/sidekick/Sidekick_th_bool_static/index.html index c410d494..f22b15be 100644 --- a/dev/sidekick/Sidekick_th_bool_static/index.html +++ b/dev/sidekick/Sidekick_th_bool_static/index.html @@ -1,2 +1,2 @@ -Sidekick_th_bool_static (sidekick.Sidekick_th_bool_static)

Module Sidekick_th_bool_static

Signatures for booleans

type ('a, 'args) bool_view =
| B_bool of bool
| B_not of 'a
| B_and of 'args
| B_or of 'args
| B_imply of 'args * 'a
| B_equiv of 'a * 'a
| B_xor of 'a * 'a
| B_eq of 'a * 'a
| B_neq of 'a * 'a
| B_ite of 'a * 'a * 'a
| B_opaque_bool of 'a
| B_atom of 'a
module type ARG = sig ... end
module type S = sig ... end
module Make : functor (A : ARG) -> S with module A = A
\ No newline at end of file +Sidekick_th_bool_static (sidekick.Sidekick_th_bool_static)

Module Sidekick_th_bool_static

Theory of boolean formulas.

This handles formulas containing "and", "or", "=>", "if-then-else", etc.

type ('a, 'args) bool_view =
| B_bool of bool
| B_not of 'a
| B_and of 'args
| B_or of 'args
| B_imply of 'args * 'a
| B_equiv of 'a * 'a
| B_xor of 'a * 'a
| B_eq of 'a * 'a
| B_neq of 'a * 'a
| B_ite of 'a * 'a * 'a
| B_opaque_bool of 'a
| B_atom of 'a

Boolean-oriented view of terms

module type ARG = sig ... end

Argument to the theory

module type S = sig ... end

Signature

module Make : functor (A : ARG) -> S with module A = A
\ No newline at end of file diff --git a/dev/sidekick/Sidekick_th_bool_static/module-type-ARG/Gensym/index.html b/dev/sidekick/Sidekick_th_bool_static/module-type-ARG/Gensym/index.html index 8288d7f9..d263511f 100644 --- a/dev/sidekick/Sidekick_th_bool_static/module-type-ARG/Gensym/index.html +++ b/dev/sidekick/Sidekick_th_bool_static/module-type-ARG/Gensym/index.html @@ -1,2 +1,2 @@ -Gensym (sidekick.Sidekick_th_bool_static.ARG.Gensym)

Module ARG.Gensym

type t
val create : S.T.Term.state -> t
val fresh_term : t -> pre:string -> S.T.Ty.t -> term

Make a fresh term of the given type

\ No newline at end of file +Gensym (sidekick.Sidekick_th_bool_static.ARG.Gensym)

Module ARG.Gensym

Fresh symbol generator.

The theory needs to be able to create new terms with fresh names, to be used as placeholders for complex formulas during Tseitin encoding.

type t
val create : S.T.Term.state -> t

New (stateful) generator instance.

val fresh_term : t -> pre:string -> S.T.Ty.t -> term

Make a fresh term of the given type

\ No newline at end of file diff --git a/dev/sidekick/Sidekick_th_bool_static/module-type-ARG/index.html b/dev/sidekick/Sidekick_th_bool_static/module-type-ARG/index.html index b6b6aefb..876923b3 100644 --- a/dev/sidekick/Sidekick_th_bool_static/module-type-ARG/index.html +++ b/dev/sidekick/Sidekick_th_bool_static/module-type-ARG/index.html @@ -1,2 +1,2 @@ -ARG (sidekick.Sidekick_th_bool_static.ARG)

Module type Sidekick_th_bool_static.ARG

type term = S.T.Term.t
val view_as_bool : term -> (term, term Iter.t) bool_view

Project the term into the boolean view

val mk_bool : S.T.Term.state -> (term, term Sidekick_util.IArray.t) bool_view -> term

Make a term from the given boolean view

val check_congruence_classes : bool

Configuration: add final-check handler to verify if new boolean formulas are present in the congruence closure. Only enable if some theories are susceptible to create boolean formulas during the proof search.

module Gensym : sig ... end
\ No newline at end of file +ARG (sidekick.Sidekick_th_bool_static.ARG)

Module type Sidekick_th_bool_static.ARG

Argument to the theory

type term = S.T.Term.t
val view_as_bool : term -> (term, term Iter.t) bool_view

Project the term into the boolean view.

val mk_bool : S.T.Term.state -> (term, term Sidekick_util.IArray.t) bool_view -> term

Make a term from the given boolean view.

val check_congruence_classes : bool

Configuration: add final-check handler to verify if new boolean formulas are present in the congruence closure. Only enable if some theories are susceptible to create boolean formulas during the proof search.

module Gensym : sig ... end

Fresh symbol generator.

\ No newline at end of file diff --git a/dev/sidekick/Sidekick_th_bool_static/module-type-S/A/Gensym/index.html b/dev/sidekick/Sidekick_th_bool_static/module-type-S/A/Gensym/index.html index d0970f74..ec791035 100644 --- a/dev/sidekick/Sidekick_th_bool_static/module-type-S/A/Gensym/index.html +++ b/dev/sidekick/Sidekick_th_bool_static/module-type-S/A/Gensym/index.html @@ -1,2 +1,2 @@ -Gensym (sidekick.Sidekick_th_bool_static.S.A.Gensym)

Module A.Gensym

type t
val create : S.T.Term.state -> t
val fresh_term : t -> pre:string -> S.T.Ty.t -> term

Make a fresh term of the given type

\ No newline at end of file +Gensym (sidekick.Sidekick_th_bool_static.S.A.Gensym)

Module A.Gensym

Fresh symbol generator.

The theory needs to be able to create new terms with fresh names, to be used as placeholders for complex formulas during Tseitin encoding.

type t
val create : S.T.Term.state -> t

New (stateful) generator instance.

val fresh_term : t -> pre:string -> S.T.Ty.t -> term

Make a fresh term of the given type

\ No newline at end of file diff --git a/dev/sidekick/Sidekick_th_bool_static/module-type-S/A/index.html b/dev/sidekick/Sidekick_th_bool_static/module-type-S/A/index.html index 05a137f9..b838cead 100644 --- a/dev/sidekick/Sidekick_th_bool_static/module-type-S/A/index.html +++ b/dev/sidekick/Sidekick_th_bool_static/module-type-S/A/index.html @@ -1,2 +1,2 @@ -A (sidekick.Sidekick_th_bool_static.S.A)

Module S.A

type term = S.T.Term.t
val view_as_bool : term -> (term, term Iter.t) bool_view

Project the term into the boolean view

val mk_bool : S.T.Term.state -> (term, term Sidekick_util.IArray.t) bool_view -> term

Make a term from the given boolean view

val check_congruence_classes : bool

Configuration: add final-check handler to verify if new boolean formulas are present in the congruence closure. Only enable if some theories are susceptible to create boolean formulas during the proof search.

module Gensym : sig ... end
\ No newline at end of file +A (sidekick.Sidekick_th_bool_static.S.A)

Module S.A

type term = S.T.Term.t
val view_as_bool : term -> (term, term Iter.t) bool_view

Project the term into the boolean view.

val mk_bool : S.T.Term.state -> (term, term Sidekick_util.IArray.t) bool_view -> term

Make a term from the given boolean view.

val check_congruence_classes : bool

Configuration: add final-check handler to verify if new boolean formulas are present in the congruence closure. Only enable if some theories are susceptible to create boolean formulas during the proof search.

module Gensym : sig ... end

Fresh symbol generator.

\ No newline at end of file diff --git a/dev/sidekick/Sidekick_th_bool_static/module-type-S/index.html b/dev/sidekick/Sidekick_th_bool_static/module-type-S/index.html index 099a49cd..553cebed 100644 --- a/dev/sidekick/Sidekick_th_bool_static/module-type-S/index.html +++ b/dev/sidekick/Sidekick_th_bool_static/module-type-S/index.html @@ -1,2 +1,2 @@ -S (sidekick.Sidekick_th_bool_static.S)

Module type Sidekick_th_bool_static.S

module A : ARG
type state
val create : A.S.T.Term.state -> A.S.T.Ty.state -> state
val simplify : state -> A.S.Solver_internal.simplify_hook

Simplify given term

val cnf : state -> A.S.Solver_internal.preprocess_hook

add clauses for the booleans within the term.

val theory : A.S.theory
\ No newline at end of file +S (sidekick.Sidekick_th_bool_static.S)

Module type Sidekick_th_bool_static.S

Signature

module A : ARG
type state
val create : A.S.T.Term.state -> A.S.T.Ty.state -> state
val simplify : state -> A.S.Solver_internal.simplify_hook

Simplify given term

val cnf : state -> A.S.Solver_internal.preprocess_hook

preprocesses formulas by giving them names and adding clauses to equate the name with the boolean formula.

val theory : A.S.theory

A theory that can be added to the solver A.S.

This theory does most of its work during preprocessing, turning boolean formulas into SAT clauses via the Tseitin encoding .

\ No newline at end of file diff --git a/dev/sidekick/Sidekick_th_data/Make/argument-1-A/Cstor/index.html b/dev/sidekick/Sidekick_th_data/Make/argument-1-A/Cstor/index.html index 72d96c2f..fcb9db83 100644 --- a/dev/sidekick/Sidekick_th_data/Make/argument-1-A/Cstor/index.html +++ b/dev/sidekick/Sidekick_th_data/Make/argument-1-A/Cstor/index.html @@ -1,2 +1,2 @@ -Cstor (sidekick.Sidekick_th_data.Make.1-A.Cstor)

Module 1-A.Cstor

type t
val ty_args : t -> S.T.Ty.t Iter.t
val pp : t Sidekick_util.Fmt.printer
val equal : t -> t -> bool
\ No newline at end of file +Cstor (sidekick.Sidekick_th_data.Make.1-A.Cstor)

Module 1-A.Cstor

Constructor symbols.

A constructor is an injective symbol, part of a datatype (or "sum type"). For example, in type option a = Some a | None, the constructors are Some and None.

type t

Constructor

val ty_args : t -> S.T.Ty.t Iter.t

Type arguments, for a polymorphic constructor

val pp : t Sidekick_util.Fmt.printer
val equal : t -> t -> bool

Comparison

\ No newline at end of file diff --git a/dev/sidekick/Sidekick_th_data/Make/argument-1-A/index.html b/dev/sidekick/Sidekick_th_data/Make/argument-1-A/index.html index 2592be9e..7fdf6a54 100644 --- a/dev/sidekick/Sidekick_th_data/Make/argument-1-A/index.html +++ b/dev/sidekick/Sidekick_th_data/Make/argument-1-A/index.html @@ -1,2 +1,2 @@ -1-A (sidekick.Sidekick_th_data.Make.1-A)

Parameter Make.1-A

module Cstor : sig ... end
val as_datatype : S.T.Ty.t -> (Cstor.t Iter.t, S.T.Ty.t) data_ty_view

Try to view type as a datatype (with its constructors)

val view_as_data : S.T.Term.t -> (Cstor.t, S.T.Term.t) data_view

Try to view term as a datatype term

val mk_cstor : S.T.Term.state -> Cstor.t -> S.T.Term.t Sidekick_util.IArray.t -> S.T.Term.t

Make a constructor application term

val mk_is_a : S.T.Term.state -> Cstor.t -> S.T.Term.t -> S.T.Term.t

Make a is-a term

val mk_sel : S.T.Term.state -> Cstor.t -> int -> S.T.Term.t -> S.T.Term.t

Make a selector term

val mk_eq : S.T.Term.state -> S.T.Term.t -> S.T.Term.t -> S.T.Term.t

Make a term equality

val ty_is_finite : S.T.Ty.t -> bool

Is the given type known to be finite?

val ty_set_is_finite : S.T.Ty.t -> bool -> unit

Modify the "finite" field (see ty_is_finite)

\ No newline at end of file +1-A (sidekick.Sidekick_th_data.Make.1-A)

Parameter Make.1-A

module Cstor : sig ... end

Constructor symbols.

val as_datatype : S.T.Ty.t -> (Cstor.t Iter.t, S.T.Ty.t) data_ty_view

Try to view type as a datatype (with its constructors)

val view_as_data : S.T.Term.t -> (Cstor.t, S.T.Term.t) data_view

Try to view term as a datatype term

val mk_cstor : S.T.Term.state -> Cstor.t -> S.T.Term.t Sidekick_util.IArray.t -> S.T.Term.t

Make a constructor application term

val mk_is_a : S.T.Term.state -> Cstor.t -> S.T.Term.t -> S.T.Term.t

Make a is-a term

val mk_sel : S.T.Term.state -> Cstor.t -> int -> S.T.Term.t -> S.T.Term.t

Make a selector term

val mk_eq : S.T.Term.state -> S.T.Term.t -> S.T.Term.t -> S.T.Term.t

Make a term equality

val ty_is_finite : S.T.Ty.t -> bool

Is the given type known to be finite? For example a finite datatype (an "enum" in C parlance), or Bool, or Array Bool Bool.

val ty_set_is_finite : S.T.Ty.t -> bool -> unit

Modify the "finite" field (see ty_is_finite)

\ No newline at end of file diff --git a/dev/sidekick/Sidekick_th_data/Make/index.html b/dev/sidekick/Sidekick_th_data/Make/index.html index cdc2a6b4..fa88b574 100644 --- a/dev/sidekick/Sidekick_th_data/Make/index.html +++ b/dev/sidekick/Sidekick_th_data/Make/index.html @@ -1,2 +1,2 @@ -Make (sidekick.Sidekick_th_data.Make)

Module Sidekick_th_data.Make

Parameters

Signature

module A = A
val theory : A.S.theory
\ No newline at end of file +Make (sidekick.Sidekick_th_data.Make)

Module Sidekick_th_data.Make

Parameters

Signature

module A = A
val theory : A.S.theory

A theory that can be added to A.S to perform datatype reasoning.

\ No newline at end of file diff --git a/dev/sidekick/Sidekick_th_data/index.html b/dev/sidekick/Sidekick_th_data/index.html index 99374d43..12e5bb5b 100644 --- a/dev/sidekick/Sidekick_th_data/index.html +++ b/dev/sidekick/Sidekick_th_data/index.html @@ -1,2 +1,2 @@ -Sidekick_th_data (sidekick.Sidekick_th_data)

Module Sidekick_th_data

type ('c, 't) data_view =
| T_cstor of 'c * 't Sidekick_util.IArray.t
| T_select of 'c * int * 't
| T_is_a of 'c * 't
| T_other of 't

Datatype-oriented view of terms. 'c is the representation of constructors 't is the representation of terms

type ('c, 'ty) data_ty_view =
| Ty_arrow of 'ty Iter.t * 'ty
| Ty_app of {
args : 'ty Iter.t;
}
| Ty_data of {
cstors : 'c;
}
| Ty_other

View of types in a way that is directly useful for the theory of datatypes

module type ARG = sig ... end
module type S = sig ... end
module Make : functor (A : ARG) -> S with module A = A
\ No newline at end of file +Sidekick_th_data (sidekick.Sidekick_th_data)

Module Sidekick_th_data

Theory for datatypes.

type ('c, 't) data_view =
| T_cstor of 'c * 't Sidekick_util.IArray.t
| T_select of 'c * int * 't
| T_is_a of 'c * 't
| T_other of 't

Datatype-oriented view of terms. 'c is the representation of constructors 't is the representation of terms

type ('c, 'ty) data_ty_view =
| Ty_arrow of 'ty Iter.t * 'ty
| Ty_app of {
args : 'ty Iter.t;
}
| Ty_data of {
cstors : 'c;
}
| Ty_other

View of types in a way that is directly useful for the theory of datatypes

module type ARG = sig ... end

Argument to the functor

module type S = sig ... end
module Make : functor (A : ARG) -> S with module A = A
\ No newline at end of file diff --git a/dev/sidekick/Sidekick_th_data/module-type-ARG/Cstor/index.html b/dev/sidekick/Sidekick_th_data/module-type-ARG/Cstor/index.html index 1b6e49e7..1cb15355 100644 --- a/dev/sidekick/Sidekick_th_data/module-type-ARG/Cstor/index.html +++ b/dev/sidekick/Sidekick_th_data/module-type-ARG/Cstor/index.html @@ -1,2 +1,2 @@ -Cstor (sidekick.Sidekick_th_data.ARG.Cstor)

Module ARG.Cstor

type t
val ty_args : t -> S.T.Ty.t Iter.t
val pp : t Sidekick_util.Fmt.printer
val equal : t -> t -> bool
\ No newline at end of file +Cstor (sidekick.Sidekick_th_data.ARG.Cstor)

Module ARG.Cstor

Constructor symbols.

A constructor is an injective symbol, part of a datatype (or "sum type"). For example, in type option a = Some a | None, the constructors are Some and None.

type t

Constructor

val ty_args : t -> S.T.Ty.t Iter.t

Type arguments, for a polymorphic constructor

val pp : t Sidekick_util.Fmt.printer
val equal : t -> t -> bool

Comparison

\ No newline at end of file diff --git a/dev/sidekick/Sidekick_th_data/module-type-ARG/index.html b/dev/sidekick/Sidekick_th_data/module-type-ARG/index.html index 8bf5f6b8..1c4369b9 100644 --- a/dev/sidekick/Sidekick_th_data/module-type-ARG/index.html +++ b/dev/sidekick/Sidekick_th_data/module-type-ARG/index.html @@ -1,2 +1,2 @@ -ARG (sidekick.Sidekick_th_data.ARG)

Module type Sidekick_th_data.ARG

module Cstor : sig ... end
val as_datatype : S.T.Ty.t -> (Cstor.t Iter.t, S.T.Ty.t) data_ty_view

Try to view type as a datatype (with its constructors)

val view_as_data : S.T.Term.t -> (Cstor.t, S.T.Term.t) data_view

Try to view term as a datatype term

val mk_cstor : S.T.Term.state -> Cstor.t -> S.T.Term.t Sidekick_util.IArray.t -> S.T.Term.t

Make a constructor application term

val mk_is_a : S.T.Term.state -> Cstor.t -> S.T.Term.t -> S.T.Term.t

Make a is-a term

val mk_sel : S.T.Term.state -> Cstor.t -> int -> S.T.Term.t -> S.T.Term.t

Make a selector term

val mk_eq : S.T.Term.state -> S.T.Term.t -> S.T.Term.t -> S.T.Term.t

Make a term equality

val ty_is_finite : S.T.Ty.t -> bool

Is the given type known to be finite?

val ty_set_is_finite : S.T.Ty.t -> bool -> unit

Modify the "finite" field (see ty_is_finite)

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

Module type Sidekick_th_data.ARG

Argument to the functor

module Cstor : sig ... end

Constructor symbols.

val as_datatype : S.T.Ty.t -> (Cstor.t Iter.t, S.T.Ty.t) data_ty_view

Try to view type as a datatype (with its constructors)

val view_as_data : S.T.Term.t -> (Cstor.t, S.T.Term.t) data_view

Try to view term as a datatype term

val mk_cstor : S.T.Term.state -> Cstor.t -> S.T.Term.t Sidekick_util.IArray.t -> S.T.Term.t

Make a constructor application term

val mk_is_a : S.T.Term.state -> Cstor.t -> S.T.Term.t -> S.T.Term.t

Make a is-a term

val mk_sel : S.T.Term.state -> Cstor.t -> int -> S.T.Term.t -> S.T.Term.t

Make a selector term

val mk_eq : S.T.Term.state -> S.T.Term.t -> S.T.Term.t -> S.T.Term.t

Make a term equality

val ty_is_finite : S.T.Ty.t -> bool

Is the given type known to be finite? For example a finite datatype (an "enum" in C parlance), or Bool, or Array Bool Bool.

val ty_set_is_finite : S.T.Ty.t -> bool -> unit

Modify the "finite" field (see ty_is_finite)

\ No newline at end of file diff --git a/dev/sidekick/Sidekick_th_data/module-type-S/A/Cstor/index.html b/dev/sidekick/Sidekick_th_data/module-type-S/A/Cstor/index.html index 582a1246..2d6719de 100644 --- a/dev/sidekick/Sidekick_th_data/module-type-S/A/Cstor/index.html +++ b/dev/sidekick/Sidekick_th_data/module-type-S/A/Cstor/index.html @@ -1,2 +1,2 @@ -Cstor (sidekick.Sidekick_th_data.S.A.Cstor)

Module A.Cstor

type t
val ty_args : t -> S.T.Ty.t Iter.t
val pp : t Sidekick_util.Fmt.printer
val equal : t -> t -> bool
\ No newline at end of file +Cstor (sidekick.Sidekick_th_data.S.A.Cstor)

Module A.Cstor

Constructor symbols.

A constructor is an injective symbol, part of a datatype (or "sum type"). For example, in type option a = Some a | None, the constructors are Some and None.

type t

Constructor

val ty_args : t -> S.T.Ty.t Iter.t

Type arguments, for a polymorphic constructor

val pp : t Sidekick_util.Fmt.printer
val equal : t -> t -> bool

Comparison

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

Module S.A

module Cstor : sig ... end
val as_datatype : S.T.Ty.t -> (Cstor.t Iter.t, S.T.Ty.t) data_ty_view

Try to view type as a datatype (with its constructors)

val view_as_data : S.T.Term.t -> (Cstor.t, S.T.Term.t) data_view

Try to view term as a datatype term

val mk_cstor : S.T.Term.state -> Cstor.t -> S.T.Term.t Sidekick_util.IArray.t -> S.T.Term.t

Make a constructor application term

val mk_is_a : S.T.Term.state -> Cstor.t -> S.T.Term.t -> S.T.Term.t

Make a is-a term

val mk_sel : S.T.Term.state -> Cstor.t -> int -> S.T.Term.t -> S.T.Term.t

Make a selector term

val mk_eq : S.T.Term.state -> S.T.Term.t -> S.T.Term.t -> S.T.Term.t

Make a term equality

val ty_is_finite : S.T.Ty.t -> bool

Is the given type known to be finite?

val ty_set_is_finite : S.T.Ty.t -> bool -> unit

Modify the "finite" field (see ty_is_finite)

\ No newline at end of file +A (sidekick.Sidekick_th_data.S.A)

Module S.A

module Cstor : sig ... end

Constructor symbols.

val as_datatype : S.T.Ty.t -> (Cstor.t Iter.t, S.T.Ty.t) data_ty_view

Try to view type as a datatype (with its constructors)

val view_as_data : S.T.Term.t -> (Cstor.t, S.T.Term.t) data_view

Try to view term as a datatype term

val mk_cstor : S.T.Term.state -> Cstor.t -> S.T.Term.t Sidekick_util.IArray.t -> S.T.Term.t

Make a constructor application term

val mk_is_a : S.T.Term.state -> Cstor.t -> S.T.Term.t -> S.T.Term.t

Make a is-a term

val mk_sel : S.T.Term.state -> Cstor.t -> int -> S.T.Term.t -> S.T.Term.t

Make a selector term

val mk_eq : S.T.Term.state -> S.T.Term.t -> S.T.Term.t -> S.T.Term.t

Make a term equality

val ty_is_finite : S.T.Ty.t -> bool

Is the given type known to be finite? For example a finite datatype (an "enum" in C parlance), or Bool, or Array Bool Bool.

val ty_set_is_finite : S.T.Ty.t -> bool -> unit

Modify the "finite" field (see ty_is_finite)

\ No newline at end of file diff --git a/dev/sidekick/Sidekick_th_data/module-type-S/index.html b/dev/sidekick/Sidekick_th_data/module-type-S/index.html index 7750fb35..28126c50 100644 --- a/dev/sidekick/Sidekick_th_data/module-type-S/index.html +++ b/dev/sidekick/Sidekick_th_data/module-type-S/index.html @@ -1,2 +1,2 @@ -S (sidekick.Sidekick_th_data.S)

Module type Sidekick_th_data.S

module A : ARG
val theory : A.S.theory
\ No newline at end of file +S (sidekick.Sidekick_th_data.S)

Module type Sidekick_th_data.S

module A : ARG
val theory : A.S.theory

A theory that can be added to A.S to perform datatype reasoning.

\ No newline at end of file