\ No newline at end of file
diff --git a/dev/sidekick-base/Sidekick_base_solver/Th_bool/A/S/Solver_internal/index.html b/dev/sidekick-base/Sidekick_base_solver/Th_bool/A/S/Solver_internal/index.html
index 05709ab0..50d54b10 100644
--- a/dev/sidekick-base/Sidekick_base_solver/Th_bool/A/S/Solver_internal/index.html
+++ b/dev/sidekick-base/Sidekick_base_solver/Th_bool/A/S/Solver_internal/index.html
@@ -1,2 +1,2 @@
-Solver_internal (sidekick-base.Sidekick_base_solver.Th_bool.A.S.Solver_internal)
\ No newline at end of file
diff --git a/dev/sidekick-base/Sidekick_base_solver/Th_data/A/S/Solver_internal/index.html b/dev/sidekick-base/Sidekick_base_solver/Th_data/A/S/Solver_internal/index.html
index 3a5c1885..e6936948 100644
--- a/dev/sidekick-base/Sidekick_base_solver/Th_data/A/S/Solver_internal/index.html
+++ b/dev/sidekick-base/Sidekick_base_solver/Th_data/A/S/Solver_internal/index.html
@@ -1,2 +1,2 @@
-Solver_internal (sidekick-base.Sidekick_base_solver.Th_data.A.S.Solver_internal)
\ No newline at end of file
diff --git a/dev/sidekick-base/Sidekick_base_solver/Th_lra/A/S/Solver_internal/index.html b/dev/sidekick-base/Sidekick_base_solver/Th_lra/A/S/Solver_internal/index.html
index 645fee92..bf10ebdc 100644
--- a/dev/sidekick-base/Sidekick_base_solver/Th_lra/A/S/Solver_internal/index.html
+++ b/dev/sidekick-base/Sidekick_base_solver/Th_lra/A/S/Solver_internal/index.html
@@ -1,2 +1,2 @@
-Solver_internal (sidekick-base.Sidekick_base_solver.Th_lra.A.S.Solver_internal)
\ No newline at end of file
diff --git a/dev/sidekick-bin/Sidekick_smtlib/Process/Solver/Solver_internal/index.html b/dev/sidekick-bin/Sidekick_smtlib/Process/Solver/Solver_internal/index.html
index f610f43d..09adcaf0 100644
--- a/dev/sidekick-bin/Sidekick_smtlib/Process/Solver/Solver_internal/index.html
+++ b/dev/sidekick-bin/Sidekick_smtlib/Process/Solver/Solver_internal/index.html
@@ -1,2 +1,2 @@
-Solver_internal (sidekick-bin.Sidekick_smtlib.Process.Solver.Solver_internal)
define_const si ~const ~rhs adds the definition const := rhs to the (future) proof. const should be a fresh constant that occurs nowhere else, and rhs a term defined without const.
simp_t si t returns u even if no simplification occurred (in which case t == u syntactically). It emits |- t=u. (see simplifier)
Preprocessors
These preprocessors turn mixed, raw literals (possibly simplified) into literals suitable for reasoning. Typically some clauses are also added to the solver.
Given a term, try to preprocess it. Return None if it didn't change, or Some (u) if t=u. Can also add clauses to define new terms.
Preprocessing might transform terms to make them more amenable to reasoning, e.g. by removing boolean formulas via Tseitin encoding, adding clauses that encode their meaning in the same move.
Ask the SAT solver to decide the given literal in an extension of the current trail. This is useful for theory combination. If the SAT solver backtracks, this (potential) decision is removed and forgotten.
Register callbacked to be called with the slice of literals newly added on the trail.
This is called very often and should be efficient. It doesn't have to be complete, only correct. It's given only the slice of the trail consisting in new literals.
A model-production hook. It takes the solver, a class, and returns a term for this class. For example, an arithmetic theory might detect that a class contains a numeric constant, and return this constant as a model value.
If no hook assigns a value to a class, a fake value is created for it.
define_const si ~const ~rhs adds the definition const := rhs to the (future) proof. const should be a fresh constant that occurs nowhere else, and rhs a term defined without const.
simp_t si t returns u even if no simplification occurred (in which case t == u syntactically). It emits |- t=u. (see simplifier)
Preprocessors
These preprocessors turn mixed, raw literals (possibly simplified) into literals suitable for reasoning. Typically some clauses are also added to the solver.
Given a term, try to preprocess it. Return None if it didn't change, or Some (u) if t=u. Can also add clauses to define new terms.
Preprocessing might transform terms to make them more amenable to reasoning, e.g. by removing boolean formulas via Tseitin encoding, adding clauses that encode their meaning in the same move.
Ask the SAT solver to decide the given literal in an extension of the current trail. This is useful for theory combination. If the SAT solver backtracks, this (potential) decision is removed and forgotten.
Register callbacked to be called with the slice of literals newly added on the trail.
This is called very often and should be efficient. It doesn't have to be complete, only correct. It's given only the slice of the trail consisting in new literals.
A model-production hook. It takes the solver, a class, and returns a term for this class. For example, an arithmetic theory might detect that a class contains a numeric constant, and return this constant as a model value.
If no hook assigns a value to a class, a fake value is created for it.
Add a hook that will be called when a model is being produced
\ No newline at end of file
diff --git a/dev/sidekick-bin/Sidekick_smtlib__/Process/Solver/Solver_internal/index.html b/dev/sidekick-bin/Sidekick_smtlib__/Process/Solver/Solver_internal/index.html
index 22cd5034..3f134af0 100644
--- a/dev/sidekick-bin/Sidekick_smtlib__/Process/Solver/Solver_internal/index.html
+++ b/dev/sidekick-bin/Sidekick_smtlib__/Process/Solver/Solver_internal/index.html
@@ -1,2 +1,2 @@
-Solver_internal (sidekick-bin.Sidekick_smtlib__.Process.Solver.Solver_internal)
define_const si ~const ~rhs adds the definition const := rhs to the (future) proof. const should be a fresh constant that occurs nowhere else, and rhs a term defined without const.
simp_t si t returns u even if no simplification occurred (in which case t == u syntactically). It emits |- t=u. (see simplifier)
Preprocessors
These preprocessors turn mixed, raw literals (possibly simplified) into literals suitable for reasoning. Typically some clauses are also added to the solver.
Given a term, try to preprocess it. Return None if it didn't change, or Some (u) if t=u. Can also add clauses to define new terms.
Preprocessing might transform terms to make them more amenable to reasoning, e.g. by removing boolean formulas via Tseitin encoding, adding clauses that encode their meaning in the same move.
Ask the SAT solver to decide the given literal in an extension of the current trail. This is useful for theory combination. If the SAT solver backtracks, this (potential) decision is removed and forgotten.
Register callbacked to be called with the slice of literals newly added on the trail.
This is called very often and should be efficient. It doesn't have to be complete, only correct. It's given only the slice of the trail consisting in new literals.
A model-production hook. It takes the solver, a class, and returns a term for this class. For example, an arithmetic theory might detect that a class contains a numeric constant, and return this constant as a model value.
If no hook assigns a value to a class, a fake value is created for it.
define_const si ~const ~rhs adds the definition const := rhs to the (future) proof. const should be a fresh constant that occurs nowhere else, and rhs a term defined without const.
simp_t si t returns u even if no simplification occurred (in which case t == u syntactically). It emits |- t=u. (see simplifier)
Preprocessors
These preprocessors turn mixed, raw literals (possibly simplified) into literals suitable for reasoning. Typically some clauses are also added to the solver.
Given a term, try to preprocess it. Return None if it didn't change, or Some (u) if t=u. Can also add clauses to define new terms.
Preprocessing might transform terms to make them more amenable to reasoning, e.g. by removing boolean formulas via Tseitin encoding, adding clauses that encode their meaning in the same move.
Ask the SAT solver to decide the given literal in an extension of the current trail. This is useful for theory combination. If the SAT solver backtracks, this (potential) decision is removed and forgotten.
Register callbacked to be called with the slice of literals newly added on the trail.
This is called very often and should be efficient. It doesn't have to be complete, only correct. It's given only the slice of the trail consisting in new literals.
A model-production hook. It takes the solver, a class, and returns a term for this class. For example, an arithmetic theory might detect that a class contains a numeric constant, and return this constant as a model value.
If no hook assigns a value to a class, a fake value is created for it.
Add a hook that will be called when a model is being produced
\ No newline at end of file
diff --git a/dev/sidekick-bin/Sidekick_smtlib__Process/Solver/Solver_internal/index.html b/dev/sidekick-bin/Sidekick_smtlib__Process/Solver/Solver_internal/index.html
index d0b0b5ed..2db6a5bd 100644
--- a/dev/sidekick-bin/Sidekick_smtlib__Process/Solver/Solver_internal/index.html
+++ b/dev/sidekick-bin/Sidekick_smtlib__Process/Solver/Solver_internal/index.html
@@ -1,2 +1,2 @@
-Solver_internal (sidekick-bin.Sidekick_smtlib__Process.Solver.Solver_internal)
define_const si ~const ~rhs adds the definition const := rhs to the (future) proof. const should be a fresh constant that occurs nowhere else, and rhs a term defined without const.
simp_t si t returns u even if no simplification occurred (in which case t == u syntactically). It emits |- t=u. (see simplifier)
Preprocessors
These preprocessors turn mixed, raw literals (possibly simplified) into literals suitable for reasoning. Typically some clauses are also added to the solver.
Given a term, try to preprocess it. Return None if it didn't change, or Some (u) if t=u. Can also add clauses to define new terms.
Preprocessing might transform terms to make them more amenable to reasoning, e.g. by removing boolean formulas via Tseitin encoding, adding clauses that encode their meaning in the same move.
Ask the SAT solver to decide the given literal in an extension of the current trail. This is useful for theory combination. If the SAT solver backtracks, this (potential) decision is removed and forgotten.
Register callbacked to be called with the slice of literals newly added on the trail.
This is called very often and should be efficient. It doesn't have to be complete, only correct. It's given only the slice of the trail consisting in new literals.
A model-production hook. It takes the solver, a class, and returns a term for this class. For example, an arithmetic theory might detect that a class contains a numeric constant, and return this constant as a model value.
If no hook assigns a value to a class, a fake value is created for it.
define_const si ~const ~rhs adds the definition const := rhs to the (future) proof. const should be a fresh constant that occurs nowhere else, and rhs a term defined without const.
simp_t si t returns u even if no simplification occurred (in which case t == u syntactically). It emits |- t=u. (see simplifier)
Preprocessors
These preprocessors turn mixed, raw literals (possibly simplified) into literals suitable for reasoning. Typically some clauses are also added to the solver.
Given a term, try to preprocess it. Return None if it didn't change, or Some (u) if t=u. Can also add clauses to define new terms.
Preprocessing might transform terms to make them more amenable to reasoning, e.g. by removing boolean formulas via Tseitin encoding, adding clauses that encode their meaning in the same move.
Ask the SAT solver to decide the given literal in an extension of the current trail. This is useful for theory combination. If the SAT solver backtracks, this (potential) decision is removed and forgotten.
Register callbacked to be called with the slice of literals newly added on the trail.
This is called very often and should be efficient. It doesn't have to be complete, only correct. It's given only the slice of the trail consisting in new literals.
A model-production hook. It takes the solver, a class, and returns a term for this class. For example, an arithmetic theory might detect that a class contains a numeric constant, and return this constant as a model value.
If no hook assigns a value to a class, a fake value is created for it.
Add a hook that will be called when a model is being produced
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_arith_lra/Make/argument-1-A/S/Solver_internal/index.html b/dev/sidekick/Sidekick_arith_lra/Make/argument-1-A/S/Solver_internal/index.html
index 4759c608..ab80050b 100644
--- a/dev/sidekick/Sidekick_arith_lra/Make/argument-1-A/S/Solver_internal/index.html
+++ b/dev/sidekick/Sidekick_arith_lra/Make/argument-1-A/S/Solver_internal/index.html
@@ -1,2 +1,2 @@
-Solver_internal (sidekick.Sidekick_arith_lra.Make.1-A.S.Solver_internal)
define_const si ~const ~rhs adds the definition const := rhs to the (future) proof. const should be a fresh constant that occurs nowhere else, and rhs a term defined without const.
simp_t si t returns u even if no simplification occurred (in which case t == u syntactically). It emits |- t=u. (see simplifier)
Preprocessors
These preprocessors turn mixed, raw literals (possibly simplified) into literals suitable for reasoning. Typically some clauses are also added to the solver.
Given a term, try to preprocess it. Return None if it didn't change, or Some (u) if t=u. Can also add clauses to define new terms.
Preprocessing might transform terms to make them more amenable to reasoning, e.g. by removing boolean formulas via Tseitin encoding, adding clauses that encode their meaning in the same move.
Ask the SAT solver to decide the given literal in an extension of the current trail. This is useful for theory combination. If the SAT solver backtracks, this (potential) decision is removed and forgotten.
Register callbacked to be called with the slice of literals newly added on the trail.
This is called very often and should be efficient. It doesn't have to be complete, only correct. It's given only the slice of the trail consisting in new literals.
A model-production hook. It takes the solver, a class, and returns a term for this class. For example, an arithmetic theory might detect that a class contains a numeric constant, and return this constant as a model value.
If no hook assigns a value to a class, a fake value is created for it.
define_const si ~const ~rhs adds the definition const := rhs to the (future) proof. const should be a fresh constant that occurs nowhere else, and rhs a term defined without const.
simp_t si t returns u even if no simplification occurred (in which case t == u syntactically). It emits |- t=u. (see simplifier)
Preprocessors
These preprocessors turn mixed, raw literals (possibly simplified) into literals suitable for reasoning. Typically some clauses are also added to the solver.
Given a term, try to preprocess it. Return None if it didn't change, or Some (u) if t=u. Can also add clauses to define new terms.
Preprocessing might transform terms to make them more amenable to reasoning, e.g. by removing boolean formulas via Tseitin encoding, adding clauses that encode their meaning in the same move.
Ask the SAT solver to decide the given literal in an extension of the current trail. This is useful for theory combination. If the SAT solver backtracks, this (potential) decision is removed and forgotten.
Register callbacked to be called with the slice of literals newly added on the trail.
This is called very often and should be efficient. It doesn't have to be complete, only correct. It's given only the slice of the trail consisting in new literals.
A model-production hook. It takes the solver, a class, and returns a term for this class. For example, an arithmetic theory might detect that a class contains a numeric constant, and return this constant as a model value.
If no hook assigns a value to a class, a fake value is created for it.
Add a hook that will be called when a model is being produced
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_arith_lra/module-type-ARG/S/Solver_internal/index.html b/dev/sidekick/Sidekick_arith_lra/module-type-ARG/S/Solver_internal/index.html
index 3d26600c..5dc181e3 100644
--- a/dev/sidekick/Sidekick_arith_lra/module-type-ARG/S/Solver_internal/index.html
+++ b/dev/sidekick/Sidekick_arith_lra/module-type-ARG/S/Solver_internal/index.html
@@ -1,2 +1,2 @@
-Solver_internal (sidekick.Sidekick_arith_lra.ARG.S.Solver_internal)
define_const si ~const ~rhs adds the definition const := rhs to the (future) proof. const should be a fresh constant that occurs nowhere else, and rhs a term defined without const.
simp_t si t returns u even if no simplification occurred (in which case t == u syntactically). It emits |- t=u. (see simplifier)
Preprocessors
These preprocessors turn mixed, raw literals (possibly simplified) into literals suitable for reasoning. Typically some clauses are also added to the solver.
Given a term, try to preprocess it. Return None if it didn't change, or Some (u) if t=u. Can also add clauses to define new terms.
Preprocessing might transform terms to make them more amenable to reasoning, e.g. by removing boolean formulas via Tseitin encoding, adding clauses that encode their meaning in the same move.
Ask the SAT solver to decide the given literal in an extension of the current trail. This is useful for theory combination. If the SAT solver backtracks, this (potential) decision is removed and forgotten.
Register callbacked to be called with the slice of literals newly added on the trail.
This is called very often and should be efficient. It doesn't have to be complete, only correct. It's given only the slice of the trail consisting in new literals.
A model-production hook. It takes the solver, a class, and returns a term for this class. For example, an arithmetic theory might detect that a class contains a numeric constant, and return this constant as a model value.
If no hook assigns a value to a class, a fake value is created for it.
define_const si ~const ~rhs adds the definition const := rhs to the (future) proof. const should be a fresh constant that occurs nowhere else, and rhs a term defined without const.
simp_t si t returns u even if no simplification occurred (in which case t == u syntactically). It emits |- t=u. (see simplifier)
Preprocessors
These preprocessors turn mixed, raw literals (possibly simplified) into literals suitable for reasoning. Typically some clauses are also added to the solver.
Given a term, try to preprocess it. Return None if it didn't change, or Some (u) if t=u. Can also add clauses to define new terms.
Preprocessing might transform terms to make them more amenable to reasoning, e.g. by removing boolean formulas via Tseitin encoding, adding clauses that encode their meaning in the same move.
Ask the SAT solver to decide the given literal in an extension of the current trail. This is useful for theory combination. If the SAT solver backtracks, this (potential) decision is removed and forgotten.
Register callbacked to be called with the slice of literals newly added on the trail.
This is called very often and should be efficient. It doesn't have to be complete, only correct. It's given only the slice of the trail consisting in new literals.
A model-production hook. It takes the solver, a class, and returns a term for this class. For example, an arithmetic theory might detect that a class contains a numeric constant, and return this constant as a model value.
If no hook assigns a value to a class, a fake value is created for it.
Add a hook that will be called when a model is being produced
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_arith_lra/module-type-S/A/S/Solver_internal/index.html b/dev/sidekick/Sidekick_arith_lra/module-type-S/A/S/Solver_internal/index.html
index c387f7f3..e5043282 100644
--- a/dev/sidekick/Sidekick_arith_lra/module-type-S/A/S/Solver_internal/index.html
+++ b/dev/sidekick/Sidekick_arith_lra/module-type-S/A/S/Solver_internal/index.html
@@ -1,2 +1,2 @@
-Solver_internal (sidekick.Sidekick_arith_lra.S.A.S.Solver_internal)
define_const si ~const ~rhs adds the definition const := rhs to the (future) proof. const should be a fresh constant that occurs nowhere else, and rhs a term defined without const.
simp_t si t returns u even if no simplification occurred (in which case t == u syntactically). It emits |- t=u. (see simplifier)
Preprocessors
These preprocessors turn mixed, raw literals (possibly simplified) into literals suitable for reasoning. Typically some clauses are also added to the solver.
Given a term, try to preprocess it. Return None if it didn't change, or Some (u) if t=u. Can also add clauses to define new terms.
Preprocessing might transform terms to make them more amenable to reasoning, e.g. by removing boolean formulas via Tseitin encoding, adding clauses that encode their meaning in the same move.
Ask the SAT solver to decide the given literal in an extension of the current trail. This is useful for theory combination. If the SAT solver backtracks, this (potential) decision is removed and forgotten.
Register callbacked to be called with the slice of literals newly added on the trail.
This is called very often and should be efficient. It doesn't have to be complete, only correct. It's given only the slice of the trail consisting in new literals.
A model-production hook. It takes the solver, a class, and returns a term for this class. For example, an arithmetic theory might detect that a class contains a numeric constant, and return this constant as a model value.
If no hook assigns a value to a class, a fake value is created for it.
define_const si ~const ~rhs adds the definition const := rhs to the (future) proof. const should be a fresh constant that occurs nowhere else, and rhs a term defined without const.
simp_t si t returns u even if no simplification occurred (in which case t == u syntactically). It emits |- t=u. (see simplifier)
Preprocessors
These preprocessors turn mixed, raw literals (possibly simplified) into literals suitable for reasoning. Typically some clauses are also added to the solver.
Given a term, try to preprocess it. Return None if it didn't change, or Some (u) if t=u. Can also add clauses to define new terms.
Preprocessing might transform terms to make them more amenable to reasoning, e.g. by removing boolean formulas via Tseitin encoding, adding clauses that encode their meaning in the same move.
Ask the SAT solver to decide the given literal in an extension of the current trail. This is useful for theory combination. If the SAT solver backtracks, this (potential) decision is removed and forgotten.
Register callbacked to be called with the slice of literals newly added on the trail.
This is called very often and should be efficient. It doesn't have to be complete, only correct. It's given only the slice of the trail consisting in new literals.
A model-production hook. It takes the solver, a class, and returns a term for this class. For example, an arithmetic theory might detect that a class contains a numeric constant, and return this constant as a model value.
If no hook assigns a value to a class, a fake value is created for it.
Add a hook that will be called when a model is being produced
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_core/Monoid_of_repr/argument-1-M/SI/index.html b/dev/sidekick/Sidekick_core/Monoid_of_repr/argument-1-M/SI/index.html
index 64390e80..83d5cd2c 100644
--- a/dev/sidekick/Sidekick_core/Monoid_of_repr/argument-1-M/SI/index.html
+++ b/dev/sidekick/Sidekick_core/Monoid_of_repr/argument-1-M/SI/index.html
@@ -1,2 +1,2 @@
-SI (sidekick.Sidekick_core.Monoid_of_repr.1-M.SI)
define_const si ~const ~rhs adds the definition const := rhs to the (future) proof. const should be a fresh constant that occurs nowhere else, and rhs a term defined without const.
simp_t si t returns u even if no simplification occurred (in which case t == u syntactically). It emits |- t=u. (see simplifier)
Preprocessors
These preprocessors turn mixed, raw literals (possibly simplified) into literals suitable for reasoning. Typically some clauses are also added to the solver.
Given a term, try to preprocess it. Return None if it didn't change, or Some (u) if t=u. Can also add clauses to define new terms.
Preprocessing might transform terms to make them more amenable to reasoning, e.g. by removing boolean formulas via Tseitin encoding, adding clauses that encode their meaning in the same move.
Ask the SAT solver to decide the given literal in an extension of the current trail. This is useful for theory combination. If the SAT solver backtracks, this (potential) decision is removed and forgotten.
Register callbacked to be called with the slice of literals newly added on the trail.
This is called very often and should be efficient. It doesn't have to be complete, only correct. It's given only the slice of the trail consisting in new literals.
A model-production hook. It takes the solver, a class, and returns a term for this class. For example, an arithmetic theory might detect that a class contains a numeric constant, and return this constant as a model value.
If no hook assigns a value to a class, a fake value is created for it.
define_const si ~const ~rhs adds the definition const := rhs to the (future) proof. const should be a fresh constant that occurs nowhere else, and rhs a term defined without const.
simp_t si t returns u even if no simplification occurred (in which case t == u syntactically). It emits |- t=u. (see simplifier)
Preprocessors
These preprocessors turn mixed, raw literals (possibly simplified) into literals suitable for reasoning. Typically some clauses are also added to the solver.
Given a term, try to preprocess it. Return None if it didn't change, or Some (u) if t=u. Can also add clauses to define new terms.
Preprocessing might transform terms to make them more amenable to reasoning, e.g. by removing boolean formulas via Tseitin encoding, adding clauses that encode their meaning in the same move.
Ask the SAT solver to decide the given literal in an extension of the current trail. This is useful for theory combination. If the SAT solver backtracks, this (potential) decision is removed and forgotten.
Register callbacked to be called with the slice of literals newly added on the trail.
This is called very often and should be efficient. It doesn't have to be complete, only correct. It's given only the slice of the trail consisting in new literals.
A model-production hook. It takes the solver, a class, and returns a term for this class. For example, an arithmetic theory might detect that a class contains a numeric constant, and return this constant as a model value.
If no hook assigns a value to a class, a fake value is created for it.
Add a hook that will be called when a model is being produced
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_core/module-type-MONOID_ARG/SI/index.html b/dev/sidekick/Sidekick_core/module-type-MONOID_ARG/SI/index.html
index 747f829c..4d2c87d0 100644
--- a/dev/sidekick/Sidekick_core/module-type-MONOID_ARG/SI/index.html
+++ b/dev/sidekick/Sidekick_core/module-type-MONOID_ARG/SI/index.html
@@ -1,2 +1,2 @@
-SI (sidekick.Sidekick_core.MONOID_ARG.SI)
define_const si ~const ~rhs adds the definition const := rhs to the (future) proof. const should be a fresh constant that occurs nowhere else, and rhs a term defined without const.
simp_t si t returns u even if no simplification occurred (in which case t == u syntactically). It emits |- t=u. (see simplifier)
Preprocessors
These preprocessors turn mixed, raw literals (possibly simplified) into literals suitable for reasoning. Typically some clauses are also added to the solver.
Given a term, try to preprocess it. Return None if it didn't change, or Some (u) if t=u. Can also add clauses to define new terms.
Preprocessing might transform terms to make them more amenable to reasoning, e.g. by removing boolean formulas via Tseitin encoding, adding clauses that encode their meaning in the same move.
Ask the SAT solver to decide the given literal in an extension of the current trail. This is useful for theory combination. If the SAT solver backtracks, this (potential) decision is removed and forgotten.
Register callbacked to be called with the slice of literals newly added on the trail.
This is called very often and should be efficient. It doesn't have to be complete, only correct. It's given only the slice of the trail consisting in new literals.
A model-production hook. It takes the solver, a class, and returns a term for this class. For example, an arithmetic theory might detect that a class contains a numeric constant, and return this constant as a model value.
If no hook assigns a value to a class, a fake value is created for it.
define_const si ~const ~rhs adds the definition const := rhs to the (future) proof. const should be a fresh constant that occurs nowhere else, and rhs a term defined without const.
simp_t si t returns u even if no simplification occurred (in which case t == u syntactically). It emits |- t=u. (see simplifier)
Preprocessors
These preprocessors turn mixed, raw literals (possibly simplified) into literals suitable for reasoning. Typically some clauses are also added to the solver.
Given a term, try to preprocess it. Return None if it didn't change, or Some (u) if t=u. Can also add clauses to define new terms.
Preprocessing might transform terms to make them more amenable to reasoning, e.g. by removing boolean formulas via Tseitin encoding, adding clauses that encode their meaning in the same move.
Ask the SAT solver to decide the given literal in an extension of the current trail. This is useful for theory combination. If the SAT solver backtracks, this (potential) decision is removed and forgotten.
Register callbacked to be called with the slice of literals newly added on the trail.
This is called very often and should be efficient. It doesn't have to be complete, only correct. It's given only the slice of the trail consisting in new literals.
A model-production hook. It takes the solver, a class, and returns a term for this class. For example, an arithmetic theory might detect that a class contains a numeric constant, and return this constant as a model value.
If no hook assigns a value to a class, a fake value is created for it.
Add a hook that will be called when a model is being produced
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_core/module-type-SOLVER/Solver_internal/index.html b/dev/sidekick/Sidekick_core/module-type-SOLVER/Solver_internal/index.html
index e9185b5e..81631897 100644
--- a/dev/sidekick/Sidekick_core/module-type-SOLVER/Solver_internal/index.html
+++ b/dev/sidekick/Sidekick_core/module-type-SOLVER/Solver_internal/index.html
@@ -1,2 +1,2 @@
-Solver_internal (sidekick.Sidekick_core.SOLVER.Solver_internal)
define_const si ~const ~rhs adds the definition const := rhs to the (future) proof. const should be a fresh constant that occurs nowhere else, and rhs a term defined without const.
simp_t si t returns u even if no simplification occurred (in which case t == u syntactically). It emits |- t=u. (see simplifier)
Preprocessors
These preprocessors turn mixed, raw literals (possibly simplified) into literals suitable for reasoning. Typically some clauses are also added to the solver.
Given a term, try to preprocess it. Return None if it didn't change, or Some (u) if t=u. Can also add clauses to define new terms.
Preprocessing might transform terms to make them more amenable to reasoning, e.g. by removing boolean formulas via Tseitin encoding, adding clauses that encode their meaning in the same move.
Ask the SAT solver to decide the given literal in an extension of the current trail. This is useful for theory combination. If the SAT solver backtracks, this (potential) decision is removed and forgotten.
Register callbacked to be called with the slice of literals newly added on the trail.
This is called very often and should be efficient. It doesn't have to be complete, only correct. It's given only the slice of the trail consisting in new literals.
A model-production hook. It takes the solver, a class, and returns a term for this class. For example, an arithmetic theory might detect that a class contains a numeric constant, and return this constant as a model value.
If no hook assigns a value to a class, a fake value is created for it.
define_const si ~const ~rhs adds the definition const := rhs to the (future) proof. const should be a fresh constant that occurs nowhere else, and rhs a term defined without const.
simp_t si t returns u even if no simplification occurred (in which case t == u syntactically). It emits |- t=u. (see simplifier)
Preprocessors
These preprocessors turn mixed, raw literals (possibly simplified) into literals suitable for reasoning. Typically some clauses are also added to the solver.
Given a term, try to preprocess it. Return None if it didn't change, or Some (u) if t=u. Can also add clauses to define new terms.
Preprocessing might transform terms to make them more amenable to reasoning, e.g. by removing boolean formulas via Tseitin encoding, adding clauses that encode their meaning in the same move.
Ask the SAT solver to decide the given literal in an extension of the current trail. This is useful for theory combination. If the SAT solver backtracks, this (potential) decision is removed and forgotten.
Register callbacked to be called with the slice of literals newly added on the trail.
This is called very often and should be efficient. It doesn't have to be complete, only correct. It's given only the slice of the trail consisting in new literals.
A model-production hook. It takes the solver, a class, and returns a term for this class. For example, an arithmetic theory might detect that a class contains a numeric constant, and return this constant as a model value.
If no hook assigns a value to a class, a fake value is created for it.
Add a hook that will be called when a model is being produced
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_core/module-type-SOLVER_INTERNAL/index.html b/dev/sidekick/Sidekick_core/module-type-SOLVER_INTERNAL/index.html
index 6ac50467..924c735e 100644
--- a/dev/sidekick/Sidekick_core/module-type-SOLVER_INTERNAL/index.html
+++ b/dev/sidekick/Sidekick_core/module-type-SOLVER_INTERNAL/index.html
@@ -1,2 +1,2 @@
-SOLVER_INTERNAL (sidekick.Sidekick_core.SOLVER_INTERNAL)
Module type Sidekick_core.SOLVER_INTERNAL
A view of the solver from a theory's point of view.
Theories should interact with the solver via this module, to assert new lemmas, propagate literals, access the congruence closure, etc.
define_const si ~const ~rhs adds the definition const := rhs to the (future) proof. const should be a fresh constant that occurs nowhere else, and rhs a term defined without const.
simp_t si t returns u even if no simplification occurred (in which case t == u syntactically). It emits |- t=u. (see simplifier)
Preprocessors
These preprocessors turn mixed, raw literals (possibly simplified) into literals suitable for reasoning. Typically some clauses are also added to the solver.
Given a term, try to preprocess it. Return None if it didn't change, or Some (u) if t=u. Can also add clauses to define new terms.
Preprocessing might transform terms to make them more amenable to reasoning, e.g. by removing boolean formulas via Tseitin encoding, adding clauses that encode their meaning in the same move.
Ask the SAT solver to decide the given literal in an extension of the current trail. This is useful for theory combination. If the SAT solver backtracks, this (potential) decision is removed and forgotten.
Register callbacked to be called with the slice of literals newly added on the trail.
This is called very often and should be efficient. It doesn't have to be complete, only correct. It's given only the slice of the trail consisting in new literals.
A model-production hook. It takes the solver, a class, and returns a term for this class. For example, an arithmetic theory might detect that a class contains a numeric constant, and return this constant as a model value.
If no hook assigns a value to a class, a fake value is created for it.
define_const si ~const ~rhs adds the definition const := rhs to the (future) proof. const should be a fresh constant that occurs nowhere else, and rhs a term defined without const.
simp_t si t returns u even if no simplification occurred (in which case t == u syntactically). It emits |- t=u. (see simplifier)
Preprocessors
These preprocessors turn mixed, raw literals (possibly simplified) into literals suitable for reasoning. Typically some clauses are also added to the solver.
Given a term, try to preprocess it. Return None if it didn't change, or Some (u) if t=u. Can also add clauses to define new terms.
Preprocessing might transform terms to make them more amenable to reasoning, e.g. by removing boolean formulas via Tseitin encoding, adding clauses that encode their meaning in the same move.
Ask the SAT solver to decide the given literal in an extension of the current trail. This is useful for theory combination. If the SAT solver backtracks, this (potential) decision is removed and forgotten.
Register callbacked to be called with the slice of literals newly added on the trail.
This is called very often and should be efficient. It doesn't have to be complete, only correct. It's given only the slice of the trail consisting in new literals.
A model-production hook. It takes the solver, a class, and returns a term for this class. For example, an arithmetic theory might detect that a class contains a numeric constant, and return this constant as a model value.
If no hook assigns a value to a class, a fake value is created for it.
Add a hook that will be called when a model is being produced
\ 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 ff6ddcb8..db9b7488 100644
--- a/dev/sidekick/Sidekick_sat/Solver/Make_cdcl_t/index.html
+++ b/dev/sidekick/Sidekick_sat/Solver/Make_cdcl_t/index.html
@@ -1,2 +1,2 @@
-Make_cdcl_t (sidekick.Sidekick_sat.Solver.Make_cdcl_t)
\ 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 7749b079..022dbbcc 100644
--- a/dev/sidekick/Sidekick_sat/Solver/Make_pure_sat/index.html
+++ b/dev/sidekick/Sidekick_sat/Solver/Make_pure_sat/index.html
@@ -1,2 +1,2 @@
-Make_pure_sat (sidekick.Sidekick_sat.Solver.Make_pure_sat)
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_sat/Solver/module-type-S/index.html b/dev/sidekick/Sidekick_sat/Solver/module-type-S/index.html
index c19fc2ec..e29ea201 100644
--- a/dev/sidekick/Sidekick_sat/Solver/module-type-S/index.html
+++ b/dev/sidekick/Sidekick_sat/Solver/module-type-S/index.html
@@ -1,2 +1,2 @@
-S (sidekick.Sidekick_sat.Solver.S)
Module type Solver.S
Safe external interface of solvers.
Internal modules
These are the internal modules used, you should probably not use them if you're not familiar with the internals of mSAT.
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_sat/Solver_intf/Clause_pool_id/index.html b/dev/sidekick/Sidekick_sat/Solver_intf/Clause_pool_id/index.html
new file mode 100644
index 00000000..758a5fea
--- /dev/null
+++ b/dev/sidekick/Sidekick_sat/Solver_intf/Clause_pool_id/index.html
@@ -0,0 +1,2 @@
+
+Clause_pool_id (sidekick.Sidekick_sat.Solver_intf.Clause_pool_id)
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_sat/Solver_intf/index.html b/dev/sidekick/Sidekick_sat/Solver_intf/index.html
index ee2acfeb..d60556c7 100644
--- a/dev/sidekick/Sidekick_sat/Solver_intf/index.html
+++ b/dev/sidekick/Sidekick_sat/Solver_intf/index.html
@@ -1,2 +1,2 @@
-Solver_intf (sidekick.Sidekick_sat.Solver_intf)
Module Sidekick_sat.Solver_intf
Interface for Solvers
This modules defines the safe external interface for solvers. Solvers that implements this interface can be obtained using the Make functor in Solver or Mcsolver.
type'a printer = Stdlib.Format.formatter ->'a-> unit
The type of values returned when the solver reaches an UNSAT state.
type same_sign = bool
This type is used during the normalisation of lits. true means the literal stayed the same, false that its sign was flipped.
type('lit, 'proof) reason =
| Consequenceof unit ->'lit list * 'proof
The type of reasons for propagations of a lit f.
Consequence (l, p) means that the lits in l imply the propagated lit f. The proof should be a proof of the clause "l implies f".
invariant: in Consequence (fun () -> l,p), all elements of l must be true in the current trail.
note on lazyiness: the justification is suspended (using unit -> …) to avoid potentially costly computations that might never be used if this literal is backtracked without participating in a conflict. Therefore the function that produces (l,p) needs only be safe in trails (partial models) that are conservative extensions of the current trail. If the theory isn't robust w.r.t. extensions of the trail (e.g. if its internal state undergoes significant changes), it can be easier to produce the explanation eagerly when propagating, and then use Consequence (fun () -> expl, proof) with the already produced (expl,proof) tuple.
The external interface implemented by safe solvers, such as the one created by the Solver.Make and Mcsolver.Make functors.
\ No newline at end of file
+Solver_intf (sidekick.Sidekick_sat.Solver_intf)
Module Sidekick_sat.Solver_intf
Interface for Solvers
This modules defines the safe external interface for solvers. Solvers that implements this interface can be obtained using the Make functor in Solver or Mcsolver.
type'a printer = Stdlib.Format.formatter ->'a-> unit
The type of values returned when the solver reaches an UNSAT state.
type same_sign = bool
This type is used during the normalisation of lits. true means the literal stayed the same, false that its sign was flipped.
type('lit, 'proof) reason =
| Consequenceof unit ->'lit list * 'proof
The type of reasons for propagations of a lit f.
Consequence (l, p) means that the lits in l imply the propagated lit f. The proof should be a proof of the clause "l implies f".
invariant: in Consequence (fun () -> l,p), all elements of l must be true in the current trail.
note on lazyiness: the justification is suspended (using unit -> …) to avoid potentially costly computations that might never be used if this literal is backtracked without participating in a conflict. Therefore the function that produces (l,p) needs only be safe in trails (partial models) that are conservative extensions of the current trail. If the theory isn't robust w.r.t. extensions of the trail (e.g. if its internal state undergoes significant changes), it can be easier to produce the explanation eagerly when propagating, and then use Consequence (fun () -> expl, proof) with the already produced (expl,proof) tuple.
The external interface implemented by safe solvers, such as the one created by the Solver.Make and Mcsolver.Make functors.
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_sat/Solver_intf/module-type-ACTS/index.html b/dev/sidekick/Sidekick_sat/Solver_intf/module-type-ACTS/index.html
index 4c3ffd1b..7df8541b 100644
--- a/dev/sidekick/Sidekick_sat/Solver_intf/module-type-ACTS/index.html
+++ b/dev/sidekick/Sidekick_sat/Solver_intf/module-type-ACTS/index.html
@@ -1,2 +1,2 @@
-ACTS (sidekick.Sidekick_sat.Solver_intf.ACTS)
Ask the SAT solver to decide on the given lit with given sign before it can answer SAT. The order of decisions is still unspecified. Useful for theory combination. This will be undone on backtracking.
\ No newline at end of file
+ACTS (sidekick.Sidekick_sat.Solver_intf.ACTS)
Module type Solver_intf.ACTS
Actions available to the Plugin
The plugin provides callbacks for the SAT solver to use. These callbacks are provided with a (module ACTS) so they can modify the SAT solver by adding new lemmas, raise conflicts, etc.
Ask the SAT solver to decide on the given lit with given sign before it can answer SAT. The order of decisions is still unspecified. Useful for theory combination. This will be undone on backtracking.
\ 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 0d6a56d1..609f6b66 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,2 +1,2 @@
-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.
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_sat/module-type-ACTS/index.html b/dev/sidekick/Sidekick_sat/module-type-ACTS/index.html
index d12d6474..caf9884b 100644
--- a/dev/sidekick/Sidekick_sat/module-type-ACTS/index.html
+++ b/dev/sidekick/Sidekick_sat/module-type-ACTS/index.html
@@ -1,2 +1,2 @@
-ACTS (sidekick.Sidekick_sat.ACTS)
Ask the SAT solver to decide on the given lit with given sign before it can answer SAT. The order of decisions is still unspecified. Useful for theory combination. This will be undone on backtracking.
\ No newline at end of file
+ACTS (sidekick.Sidekick_sat.ACTS)
Ask the SAT solver to decide on the given lit with given sign before it can answer SAT. The order of decisions is still unspecified. Useful for theory combination. This will be undone on backtracking.
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_sat/module-type-S/index.html b/dev/sidekick/Sidekick_sat/module-type-S/index.html
index 8e5c5cc8..4bfbd7fc 100644
--- a/dev/sidekick/Sidekick_sat/module-type-S/index.html
+++ b/dev/sidekick/Sidekick_sat/module-type-S/index.html
@@ -1,2 +1,2 @@
-S (sidekick.Sidekick_sat.S)
Module type Sidekick_sat.S
Internal modules
These are the internal modules used, you should probably not use them if you're not familiar with the internals of mSAT.
\ 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 8c6a6ef7..20148429 100644
--- a/dev/sidekick/Sidekick_sat__/Solver/Make_cdcl_t/index.html
+++ b/dev/sidekick/Sidekick_sat__/Solver/Make_cdcl_t/index.html
@@ -1,2 +1,2 @@
-Make_cdcl_t (sidekick.Sidekick_sat__.Solver.Make_cdcl_t)
\ 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 41c327e5..37fd2d60 100644
--- a/dev/sidekick/Sidekick_sat__/Solver/Make_pure_sat/index.html
+++ b/dev/sidekick/Sidekick_sat__/Solver/Make_pure_sat/index.html
@@ -1,2 +1,2 @@
-Make_pure_sat (sidekick.Sidekick_sat__.Solver.Make_pure_sat)
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_sat__/Solver/module-type-S/index.html b/dev/sidekick/Sidekick_sat__/Solver/module-type-S/index.html
index 82becb3c..3fee137d 100644
--- a/dev/sidekick/Sidekick_sat__/Solver/module-type-S/index.html
+++ b/dev/sidekick/Sidekick_sat__/Solver/module-type-S/index.html
@@ -1,2 +1,2 @@
-S (sidekick.Sidekick_sat__.Solver.S)
Module type Solver.S
Safe external interface of solvers.
Internal modules
These are the internal modules used, you should probably not use them if you're not familiar with the internals of mSAT.
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_sat__/Solver_intf/Clause_pool_id/index.html b/dev/sidekick/Sidekick_sat__/Solver_intf/Clause_pool_id/index.html
new file mode 100644
index 00000000..c1143265
--- /dev/null
+++ b/dev/sidekick/Sidekick_sat__/Solver_intf/Clause_pool_id/index.html
@@ -0,0 +1,2 @@
+
+Clause_pool_id (sidekick.Sidekick_sat__.Solver_intf.Clause_pool_id)
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_sat__/Solver_intf/index.html b/dev/sidekick/Sidekick_sat__/Solver_intf/index.html
index ff36f25f..f9028bd2 100644
--- a/dev/sidekick/Sidekick_sat__/Solver_intf/index.html
+++ b/dev/sidekick/Sidekick_sat__/Solver_intf/index.html
@@ -1,2 +1,2 @@
-Solver_intf (sidekick.Sidekick_sat__.Solver_intf)
Module Sidekick_sat__.Solver_intf
type'a printer = Stdlib.Format.formatter ->'a-> unit
The type of values returned when the solver reaches an UNSAT state.
type same_sign = bool
This type is used during the normalisation of lits. true means the literal stayed the same, false that its sign was flipped.
type('lit, 'proof) reason =
| Consequenceof unit ->'lit list * 'proof
The type of reasons for propagations of a lit f.
Consequence (l, p) means that the lits in l imply the propagated lit f. The proof should be a proof of the clause "l implies f".
invariant: in Consequence (fun () -> l,p), all elements of l must be true in the current trail.
note on lazyiness: the justification is suspended (using unit -> …) to avoid potentially costly computations that might never be used if this literal is backtracked without participating in a conflict. Therefore the function that produces (l,p) needs only be safe in trails (partial models) that are conservative extensions of the current trail. If the theory isn't robust w.r.t. extensions of the trail (e.g. if its internal state undergoes significant changes), it can be easier to produce the explanation eagerly when propagating, and then use Consequence (fun () -> expl, proof) with the already produced (expl,proof) tuple.
The type of values returned when the solver reaches an UNSAT state.
type same_sign = bool
This type is used during the normalisation of lits. true means the literal stayed the same, false that its sign was flipped.
type('lit, 'proof) reason =
| Consequenceof unit ->'lit list * 'proof
The type of reasons for propagations of a lit f.
Consequence (l, p) means that the lits in l imply the propagated lit f. The proof should be a proof of the clause "l implies f".
invariant: in Consequence (fun () -> l,p), all elements of l must be true in the current trail.
note on lazyiness: the justification is suspended (using unit -> …) to avoid potentially costly computations that might never be used if this literal is backtracked without participating in a conflict. Therefore the function that produces (l,p) needs only be safe in trails (partial models) that are conservative extensions of the current trail. If the theory isn't robust w.r.t. extensions of the trail (e.g. if its internal state undergoes significant changes), it can be easier to produce the explanation eagerly when propagating, and then use Consequence (fun () -> expl, proof) with the already produced (expl,proof) tuple.
The external interface implemented by safe solvers, such as the one created by the Solver.Make and Mcsolver.Make functors.
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_sat__/Solver_intf/module-type-ACTS/index.html b/dev/sidekick/Sidekick_sat__/Solver_intf/module-type-ACTS/index.html
index fb7a92cc..47198a66 100644
--- a/dev/sidekick/Sidekick_sat__/Solver_intf/module-type-ACTS/index.html
+++ b/dev/sidekick/Sidekick_sat__/Solver_intf/module-type-ACTS/index.html
@@ -1,2 +1,2 @@
-ACTS (sidekick.Sidekick_sat__.Solver_intf.ACTS)
Ask the SAT solver to decide on the given lit with given sign before it can answer SAT. The order of decisions is still unspecified. Useful for theory combination. This will be undone on backtracking.
\ No newline at end of file
+ACTS (sidekick.Sidekick_sat__.Solver_intf.ACTS)
Module type Solver_intf.ACTS
Actions available to the Plugin
The plugin provides callbacks for the SAT solver to use. These callbacks are provided with a (module ACTS) so they can modify the SAT solver by adding new lemmas, raise conflicts, etc.
Ask the SAT solver to decide on the given lit with given sign before it can answer SAT. The order of decisions is still unspecified. Useful for theory combination. This will be undone on backtracking.
\ 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 c718aee8..a74c9f82 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,2 +1,2 @@
-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.
\ 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 6e3f47d4..30334b1c 100644
--- a/dev/sidekick/Sidekick_sat__Solver/Make_cdcl_t/index.html
+++ b/dev/sidekick/Sidekick_sat__Solver/Make_cdcl_t/index.html
@@ -1,2 +1,2 @@
-Make_cdcl_t (sidekick.Sidekick_sat__Solver.Make_cdcl_t)
\ 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 6622c9f3..662d6352 100644
--- a/dev/sidekick/Sidekick_sat__Solver/Make_pure_sat/index.html
+++ b/dev/sidekick/Sidekick_sat__Solver/Make_pure_sat/index.html
@@ -1,2 +1,2 @@
-Make_pure_sat (sidekick.Sidekick_sat__Solver.Make_pure_sat)
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_sat__Solver/module-type-S/index.html b/dev/sidekick/Sidekick_sat__Solver/module-type-S/index.html
index b55aa306..c66a79c5 100644
--- a/dev/sidekick/Sidekick_sat__Solver/module-type-S/index.html
+++ b/dev/sidekick/Sidekick_sat__Solver/module-type-S/index.html
@@ -1,2 +1,2 @@
-S (sidekick.Sidekick_sat__Solver.S)
Module type Sidekick_sat__Solver.S
Safe external interface of solvers.
Internal modules
These are the internal modules used, you should probably not use them if you're not familiar with the internals of mSAT.
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_sat__Solver_intf/Clause_pool_id/index.html b/dev/sidekick/Sidekick_sat__Solver_intf/Clause_pool_id/index.html
new file mode 100644
index 00000000..cd57b2c4
--- /dev/null
+++ b/dev/sidekick/Sidekick_sat__Solver_intf/Clause_pool_id/index.html
@@ -0,0 +1,2 @@
+
+Clause_pool_id (sidekick.Sidekick_sat__Solver_intf.Clause_pool_id)
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_sat__Solver_intf/index.html b/dev/sidekick/Sidekick_sat__Solver_intf/index.html
index f79f99ed..2f635919 100644
--- a/dev/sidekick/Sidekick_sat__Solver_intf/index.html
+++ b/dev/sidekick/Sidekick_sat__Solver_intf/index.html
@@ -1,2 +1,2 @@
-Sidekick_sat__Solver_intf (sidekick.Sidekick_sat__Solver_intf)
Module Sidekick_sat__Solver_intf
Interface for Solvers
This modules defines the safe external interface for solvers. Solvers that implements this interface can be obtained using the Make functor in Solver or Mcsolver.
type'a printer = Stdlib.Format.formatter ->'a-> unit
The type of values returned when the solver reaches an UNSAT state.
type same_sign = bool
This type is used during the normalisation of lits. true means the literal stayed the same, false that its sign was flipped.
type('lit, 'proof) reason =
| Consequenceof unit ->'lit list * 'proof
The type of reasons for propagations of a lit f.
Consequence (l, p) means that the lits in l imply the propagated lit f. The proof should be a proof of the clause "l implies f".
invariant: in Consequence (fun () -> l,p), all elements of l must be true in the current trail.
note on lazyiness: the justification is suspended (using unit -> …) to avoid potentially costly computations that might never be used if this literal is backtracked without participating in a conflict. Therefore the function that produces (l,p) needs only be safe in trails (partial models) that are conservative extensions of the current trail. If the theory isn't robust w.r.t. extensions of the trail (e.g. if its internal state undergoes significant changes), it can be easier to produce the explanation eagerly when propagating, and then use Consequence (fun () -> expl, proof) with the already produced (expl,proof) tuple.
The external interface implemented by safe solvers, such as the one created by the Solver.Make and Mcsolver.Make functors.
\ No newline at end of file
+Sidekick_sat__Solver_intf (sidekick.Sidekick_sat__Solver_intf)
Module Sidekick_sat__Solver_intf
Interface for Solvers
This modules defines the safe external interface for solvers. Solvers that implements this interface can be obtained using the Make functor in Solver or Mcsolver.
type'a printer = Stdlib.Format.formatter ->'a-> unit
The type of values returned when the solver reaches an UNSAT state.
type same_sign = bool
This type is used during the normalisation of lits. true means the literal stayed the same, false that its sign was flipped.
type('lit, 'proof) reason =
| Consequenceof unit ->'lit list * 'proof
The type of reasons for propagations of a lit f.
Consequence (l, p) means that the lits in l imply the propagated lit f. The proof should be a proof of the clause "l implies f".
invariant: in Consequence (fun () -> l,p), all elements of l must be true in the current trail.
note on lazyiness: the justification is suspended (using unit -> …) to avoid potentially costly computations that might never be used if this literal is backtracked without participating in a conflict. Therefore the function that produces (l,p) needs only be safe in trails (partial models) that are conservative extensions of the current trail. If the theory isn't robust w.r.t. extensions of the trail (e.g. if its internal state undergoes significant changes), it can be easier to produce the explanation eagerly when propagating, and then use Consequence (fun () -> expl, proof) with the already produced (expl,proof) tuple.
The external interface implemented by safe solvers, such as the one created by the Solver.Make and Mcsolver.Make functors.
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_sat__Solver_intf/module-type-ACTS/index.html b/dev/sidekick/Sidekick_sat__Solver_intf/module-type-ACTS/index.html
index 022b493d..22969300 100644
--- a/dev/sidekick/Sidekick_sat__Solver_intf/module-type-ACTS/index.html
+++ b/dev/sidekick/Sidekick_sat__Solver_intf/module-type-ACTS/index.html
@@ -1,2 +1,2 @@
-ACTS (sidekick.Sidekick_sat__Solver_intf.ACTS)
Ask the SAT solver to decide on the given lit with given sign before it can answer SAT. The order of decisions is still unspecified. Useful for theory combination. This will be undone on backtracking.
\ No newline at end of file
+ACTS (sidekick.Sidekick_sat__Solver_intf.ACTS)
Module type Sidekick_sat__Solver_intf.ACTS
Actions available to the Plugin
The plugin provides callbacks for the SAT solver to use. These callbacks are provided with a (module ACTS) so they can modify the SAT solver by adding new lemmas, raise conflicts, etc.
Ask the SAT solver to decide on the given lit with given sign before it can answer SAT. The order of decisions is still unspecified. Useful for theory combination. This will be undone on backtracking.
\ 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 dc5f92a9..6b870346 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,2 +1,2 @@
-S (sidekick.Sidekick_sat__Solver_intf.S)
Module type Sidekick_sat__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.
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_smt_solver/Make/Solver_internal/index.html b/dev/sidekick/Sidekick_smt_solver/Make/Solver_internal/index.html
index df96b67f..31cc289a 100644
--- a/dev/sidekick/Sidekick_smt_solver/Make/Solver_internal/index.html
+++ b/dev/sidekick/Sidekick_smt_solver/Make/Solver_internal/index.html
@@ -1,2 +1,2 @@
-Solver_internal (sidekick.Sidekick_smt_solver.Make.Solver_internal)
define_const si ~const ~rhs adds the definition const := rhs to the (future) proof. const should be a fresh constant that occurs nowhere else, and rhs a term defined without const.
simp_t si t returns u even if no simplification occurred (in which case t == u syntactically). It emits |- t=u. (see simplifier)
Preprocessors
These preprocessors turn mixed, raw literals (possibly simplified) into literals suitable for reasoning. Typically some clauses are also added to the solver.
Given a term, try to preprocess it. Return None if it didn't change, or Some (u) if t=u. Can also add clauses to define new terms.
Preprocessing might transform terms to make them more amenable to reasoning, e.g. by removing boolean formulas via Tseitin encoding, adding clauses that encode their meaning in the same move.
Ask the SAT solver to decide the given literal in an extension of the current trail. This is useful for theory combination. If the SAT solver backtracks, this (potential) decision is removed and forgotten.
Register callbacked to be called with the slice of literals newly added on the trail.
This is called very often and should be efficient. It doesn't have to be complete, only correct. It's given only the slice of the trail consisting in new literals.
A model-production hook. It takes the solver, a class, and returns a term for this class. For example, an arithmetic theory might detect that a class contains a numeric constant, and return this constant as a model value.
If no hook assigns a value to a class, a fake value is created for it.
define_const si ~const ~rhs adds the definition const := rhs to the (future) proof. const should be a fresh constant that occurs nowhere else, and rhs a term defined without const.
simp_t si t returns u even if no simplification occurred (in which case t == u syntactically). It emits |- t=u. (see simplifier)
Preprocessors
These preprocessors turn mixed, raw literals (possibly simplified) into literals suitable for reasoning. Typically some clauses are also added to the solver.
Given a term, try to preprocess it. Return None if it didn't change, or Some (u) if t=u. Can also add clauses to define new terms.
Preprocessing might transform terms to make them more amenable to reasoning, e.g. by removing boolean formulas via Tseitin encoding, adding clauses that encode their meaning in the same move.
Ask the SAT solver to decide the given literal in an extension of the current trail. This is useful for theory combination. If the SAT solver backtracks, this (potential) decision is removed and forgotten.
Register callbacked to be called with the slice of literals newly added on the trail.
This is called very often and should be efficient. It doesn't have to be complete, only correct. It's given only the slice of the trail consisting in new literals.
A model-production hook. It takes the solver, a class, and returns a term for this class. For example, an arithmetic theory might detect that a class contains a numeric constant, and return this constant as a model value.
If no hook assigns a value to a class, a fake value is created for it.
Add a hook that will be called when a model is being produced
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_smt_solver/module-type-S/Solver_internal/index.html b/dev/sidekick/Sidekick_smt_solver/module-type-S/Solver_internal/index.html
index 0aeba74b..2c12b5cd 100644
--- a/dev/sidekick/Sidekick_smt_solver/module-type-S/Solver_internal/index.html
+++ b/dev/sidekick/Sidekick_smt_solver/module-type-S/Solver_internal/index.html
@@ -1,2 +1,2 @@
-Solver_internal (sidekick.Sidekick_smt_solver.S.Solver_internal)
define_const si ~const ~rhs adds the definition const := rhs to the (future) proof. const should be a fresh constant that occurs nowhere else, and rhs a term defined without const.
simp_t si t returns u even if no simplification occurred (in which case t == u syntactically). It emits |- t=u. (see simplifier)
Preprocessors
These preprocessors turn mixed, raw literals (possibly simplified) into literals suitable for reasoning. Typically some clauses are also added to the solver.
Given a term, try to preprocess it. Return None if it didn't change, or Some (u) if t=u. Can also add clauses to define new terms.
Preprocessing might transform terms to make them more amenable to reasoning, e.g. by removing boolean formulas via Tseitin encoding, adding clauses that encode their meaning in the same move.
Ask the SAT solver to decide the given literal in an extension of the current trail. This is useful for theory combination. If the SAT solver backtracks, this (potential) decision is removed and forgotten.
Register callbacked to be called with the slice of literals newly added on the trail.
This is called very often and should be efficient. It doesn't have to be complete, only correct. It's given only the slice of the trail consisting in new literals.
A model-production hook. It takes the solver, a class, and returns a term for this class. For example, an arithmetic theory might detect that a class contains a numeric constant, and return this constant as a model value.
If no hook assigns a value to a class, a fake value is created for it.
define_const si ~const ~rhs adds the definition const := rhs to the (future) proof. const should be a fresh constant that occurs nowhere else, and rhs a term defined without const.
simp_t si t returns u even if no simplification occurred (in which case t == u syntactically). It emits |- t=u. (see simplifier)
Preprocessors
These preprocessors turn mixed, raw literals (possibly simplified) into literals suitable for reasoning. Typically some clauses are also added to the solver.
Given a term, try to preprocess it. Return None if it didn't change, or Some (u) if t=u. Can also add clauses to define new terms.
Preprocessing might transform terms to make them more amenable to reasoning, e.g. by removing boolean formulas via Tseitin encoding, adding clauses that encode their meaning in the same move.
Ask the SAT solver to decide the given literal in an extension of the current trail. This is useful for theory combination. If the SAT solver backtracks, this (potential) decision is removed and forgotten.
Register callbacked to be called with the slice of literals newly added on the trail.
This is called very often and should be efficient. It doesn't have to be complete, only correct. It's given only the slice of the trail consisting in new literals.
A model-production hook. It takes the solver, a class, and returns a term for this class. For example, an arithmetic theory might detect that a class contains a numeric constant, and return this constant as a model value.
If no hook assigns a value to a class, a fake value is created for it.
Add a hook that will be called when a model is being produced
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_th_bool_static/Make/argument-1-A/S/Solver_internal/index.html b/dev/sidekick/Sidekick_th_bool_static/Make/argument-1-A/S/Solver_internal/index.html
index 99354121..9909c3ab 100644
--- a/dev/sidekick/Sidekick_th_bool_static/Make/argument-1-A/S/Solver_internal/index.html
+++ b/dev/sidekick/Sidekick_th_bool_static/Make/argument-1-A/S/Solver_internal/index.html
@@ -1,2 +1,2 @@
-Solver_internal (sidekick.Sidekick_th_bool_static.Make.1-A.S.Solver_internal)
define_const si ~const ~rhs adds the definition const := rhs to the (future) proof. const should be a fresh constant that occurs nowhere else, and rhs a term defined without const.
simp_t si t returns u even if no simplification occurred (in which case t == u syntactically). It emits |- t=u. (see simplifier)
Preprocessors
These preprocessors turn mixed, raw literals (possibly simplified) into literals suitable for reasoning. Typically some clauses are also added to the solver.
Given a term, try to preprocess it. Return None if it didn't change, or Some (u) if t=u. Can also add clauses to define new terms.
Preprocessing might transform terms to make them more amenable to reasoning, e.g. by removing boolean formulas via Tseitin encoding, adding clauses that encode their meaning in the same move.
Ask the SAT solver to decide the given literal in an extension of the current trail. This is useful for theory combination. If the SAT solver backtracks, this (potential) decision is removed and forgotten.
Register callbacked to be called with the slice of literals newly added on the trail.
This is called very often and should be efficient. It doesn't have to be complete, only correct. It's given only the slice of the trail consisting in new literals.
A model-production hook. It takes the solver, a class, and returns a term for this class. For example, an arithmetic theory might detect that a class contains a numeric constant, and return this constant as a model value.
If no hook assigns a value to a class, a fake value is created for it.
define_const si ~const ~rhs adds the definition const := rhs to the (future) proof. const should be a fresh constant that occurs nowhere else, and rhs a term defined without const.
simp_t si t returns u even if no simplification occurred (in which case t == u syntactically). It emits |- t=u. (see simplifier)
Preprocessors
These preprocessors turn mixed, raw literals (possibly simplified) into literals suitable for reasoning. Typically some clauses are also added to the solver.
Given a term, try to preprocess it. Return None if it didn't change, or Some (u) if t=u. Can also add clauses to define new terms.
Preprocessing might transform terms to make them more amenable to reasoning, e.g. by removing boolean formulas via Tseitin encoding, adding clauses that encode their meaning in the same move.
Ask the SAT solver to decide the given literal in an extension of the current trail. This is useful for theory combination. If the SAT solver backtracks, this (potential) decision is removed and forgotten.
Register callbacked to be called with the slice of literals newly added on the trail.
This is called very often and should be efficient. It doesn't have to be complete, only correct. It's given only the slice of the trail consisting in new literals.
A model-production hook. It takes the solver, a class, and returns a term for this class. For example, an arithmetic theory might detect that a class contains a numeric constant, and return this constant as a model value.
If no hook assigns a value to a class, a fake value is created for it.
Add a hook that will be called when a model is being produced
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_th_bool_static/module-type-ARG/S/Solver_internal/index.html b/dev/sidekick/Sidekick_th_bool_static/module-type-ARG/S/Solver_internal/index.html
index 28b5eafc..357ac46e 100644
--- a/dev/sidekick/Sidekick_th_bool_static/module-type-ARG/S/Solver_internal/index.html
+++ b/dev/sidekick/Sidekick_th_bool_static/module-type-ARG/S/Solver_internal/index.html
@@ -1,2 +1,2 @@
-Solver_internal (sidekick.Sidekick_th_bool_static.ARG.S.Solver_internal)
define_const si ~const ~rhs adds the definition const := rhs to the (future) proof. const should be a fresh constant that occurs nowhere else, and rhs a term defined without const.
simp_t si t returns u even if no simplification occurred (in which case t == u syntactically). It emits |- t=u. (see simplifier)
Preprocessors
These preprocessors turn mixed, raw literals (possibly simplified) into literals suitable for reasoning. Typically some clauses are also added to the solver.
Given a term, try to preprocess it. Return None if it didn't change, or Some (u) if t=u. Can also add clauses to define new terms.
Preprocessing might transform terms to make them more amenable to reasoning, e.g. by removing boolean formulas via Tseitin encoding, adding clauses that encode their meaning in the same move.
Ask the SAT solver to decide the given literal in an extension of the current trail. This is useful for theory combination. If the SAT solver backtracks, this (potential) decision is removed and forgotten.
Register callbacked to be called with the slice of literals newly added on the trail.
This is called very often and should be efficient. It doesn't have to be complete, only correct. It's given only the slice of the trail consisting in new literals.
A model-production hook. It takes the solver, a class, and returns a term for this class. For example, an arithmetic theory might detect that a class contains a numeric constant, and return this constant as a model value.
If no hook assigns a value to a class, a fake value is created for it.
define_const si ~const ~rhs adds the definition const := rhs to the (future) proof. const should be a fresh constant that occurs nowhere else, and rhs a term defined without const.
simp_t si t returns u even if no simplification occurred (in which case t == u syntactically). It emits |- t=u. (see simplifier)
Preprocessors
These preprocessors turn mixed, raw literals (possibly simplified) into literals suitable for reasoning. Typically some clauses are also added to the solver.
Given a term, try to preprocess it. Return None if it didn't change, or Some (u) if t=u. Can also add clauses to define new terms.
Preprocessing might transform terms to make them more amenable to reasoning, e.g. by removing boolean formulas via Tseitin encoding, adding clauses that encode their meaning in the same move.
Ask the SAT solver to decide the given literal in an extension of the current trail. This is useful for theory combination. If the SAT solver backtracks, this (potential) decision is removed and forgotten.
Register callbacked to be called with the slice of literals newly added on the trail.
This is called very often and should be efficient. It doesn't have to be complete, only correct. It's given only the slice of the trail consisting in new literals.
A model-production hook. It takes the solver, a class, and returns a term for this class. For example, an arithmetic theory might detect that a class contains a numeric constant, and return this constant as a model value.
If no hook assigns a value to a class, a fake value is created for it.
Add a hook that will be called when a model is being produced
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_th_bool_static/module-type-S/A/S/Solver_internal/index.html b/dev/sidekick/Sidekick_th_bool_static/module-type-S/A/S/Solver_internal/index.html
index b74fe7db..235f8676 100644
--- a/dev/sidekick/Sidekick_th_bool_static/module-type-S/A/S/Solver_internal/index.html
+++ b/dev/sidekick/Sidekick_th_bool_static/module-type-S/A/S/Solver_internal/index.html
@@ -1,2 +1,2 @@
-Solver_internal (sidekick.Sidekick_th_bool_static.S.A.S.Solver_internal)
define_const si ~const ~rhs adds the definition const := rhs to the (future) proof. const should be a fresh constant that occurs nowhere else, and rhs a term defined without const.
simp_t si t returns u even if no simplification occurred (in which case t == u syntactically). It emits |- t=u. (see simplifier)
Preprocessors
These preprocessors turn mixed, raw literals (possibly simplified) into literals suitable for reasoning. Typically some clauses are also added to the solver.
Given a term, try to preprocess it. Return None if it didn't change, or Some (u) if t=u. Can also add clauses to define new terms.
Preprocessing might transform terms to make them more amenable to reasoning, e.g. by removing boolean formulas via Tseitin encoding, adding clauses that encode their meaning in the same move.
Ask the SAT solver to decide the given literal in an extension of the current trail. This is useful for theory combination. If the SAT solver backtracks, this (potential) decision is removed and forgotten.
Register callbacked to be called with the slice of literals newly added on the trail.
This is called very often and should be efficient. It doesn't have to be complete, only correct. It's given only the slice of the trail consisting in new literals.
A model-production hook. It takes the solver, a class, and returns a term for this class. For example, an arithmetic theory might detect that a class contains a numeric constant, and return this constant as a model value.
If no hook assigns a value to a class, a fake value is created for it.
define_const si ~const ~rhs adds the definition const := rhs to the (future) proof. const should be a fresh constant that occurs nowhere else, and rhs a term defined without const.
simp_t si t returns u even if no simplification occurred (in which case t == u syntactically). It emits |- t=u. (see simplifier)
Preprocessors
These preprocessors turn mixed, raw literals (possibly simplified) into literals suitable for reasoning. Typically some clauses are also added to the solver.
Given a term, try to preprocess it. Return None if it didn't change, or Some (u) if t=u. Can also add clauses to define new terms.
Preprocessing might transform terms to make them more amenable to reasoning, e.g. by removing boolean formulas via Tseitin encoding, adding clauses that encode their meaning in the same move.
Ask the SAT solver to decide the given literal in an extension of the current trail. This is useful for theory combination. If the SAT solver backtracks, this (potential) decision is removed and forgotten.
Register callbacked to be called with the slice of literals newly added on the trail.
This is called very often and should be efficient. It doesn't have to be complete, only correct. It's given only the slice of the trail consisting in new literals.
A model-production hook. It takes the solver, a class, and returns a term for this class. For example, an arithmetic theory might detect that a class contains a numeric constant, and return this constant as a model value.
If no hook assigns a value to a class, a fake value is created for it.
Add a hook that will be called when a model is being produced
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_th_cstor/Make/argument-1-A/S/Solver_internal/index.html b/dev/sidekick/Sidekick_th_cstor/Make/argument-1-A/S/Solver_internal/index.html
index 91c72672..a14ff705 100644
--- a/dev/sidekick/Sidekick_th_cstor/Make/argument-1-A/S/Solver_internal/index.html
+++ b/dev/sidekick/Sidekick_th_cstor/Make/argument-1-A/S/Solver_internal/index.html
@@ -1,2 +1,2 @@
-Solver_internal (sidekick.Sidekick_th_cstor.Make.1-A.S.Solver_internal)
define_const si ~const ~rhs adds the definition const := rhs to the (future) proof. const should be a fresh constant that occurs nowhere else, and rhs a term defined without const.
simp_t si t returns u even if no simplification occurred (in which case t == u syntactically). It emits |- t=u. (see simplifier)
Preprocessors
These preprocessors turn mixed, raw literals (possibly simplified) into literals suitable for reasoning. Typically some clauses are also added to the solver.
Given a term, try to preprocess it. Return None if it didn't change, or Some (u) if t=u. Can also add clauses to define new terms.
Preprocessing might transform terms to make them more amenable to reasoning, e.g. by removing boolean formulas via Tseitin encoding, adding clauses that encode their meaning in the same move.
Ask the SAT solver to decide the given literal in an extension of the current trail. This is useful for theory combination. If the SAT solver backtracks, this (potential) decision is removed and forgotten.
Register callbacked to be called with the slice of literals newly added on the trail.
This is called very often and should be efficient. It doesn't have to be complete, only correct. It's given only the slice of the trail consisting in new literals.
A model-production hook. It takes the solver, a class, and returns a term for this class. For example, an arithmetic theory might detect that a class contains a numeric constant, and return this constant as a model value.
If no hook assigns a value to a class, a fake value is created for it.
define_const si ~const ~rhs adds the definition const := rhs to the (future) proof. const should be a fresh constant that occurs nowhere else, and rhs a term defined without const.
simp_t si t returns u even if no simplification occurred (in which case t == u syntactically). It emits |- t=u. (see simplifier)
Preprocessors
These preprocessors turn mixed, raw literals (possibly simplified) into literals suitable for reasoning. Typically some clauses are also added to the solver.
Given a term, try to preprocess it. Return None if it didn't change, or Some (u) if t=u. Can also add clauses to define new terms.
Preprocessing might transform terms to make them more amenable to reasoning, e.g. by removing boolean formulas via Tseitin encoding, adding clauses that encode their meaning in the same move.
Ask the SAT solver to decide the given literal in an extension of the current trail. This is useful for theory combination. If the SAT solver backtracks, this (potential) decision is removed and forgotten.
Register callbacked to be called with the slice of literals newly added on the trail.
This is called very often and should be efficient. It doesn't have to be complete, only correct. It's given only the slice of the trail consisting in new literals.
A model-production hook. It takes the solver, a class, and returns a term for this class. For example, an arithmetic theory might detect that a class contains a numeric constant, and return this constant as a model value.
If no hook assigns a value to a class, a fake value is created for it.
Add a hook that will be called when a model is being produced
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_th_cstor/module-type-ARG/S/Solver_internal/index.html b/dev/sidekick/Sidekick_th_cstor/module-type-ARG/S/Solver_internal/index.html
index 740c91e3..83e68f2d 100644
--- a/dev/sidekick/Sidekick_th_cstor/module-type-ARG/S/Solver_internal/index.html
+++ b/dev/sidekick/Sidekick_th_cstor/module-type-ARG/S/Solver_internal/index.html
@@ -1,2 +1,2 @@
-Solver_internal (sidekick.Sidekick_th_cstor.ARG.S.Solver_internal)
define_const si ~const ~rhs adds the definition const := rhs to the (future) proof. const should be a fresh constant that occurs nowhere else, and rhs a term defined without const.
simp_t si t returns u even if no simplification occurred (in which case t == u syntactically). It emits |- t=u. (see simplifier)
Preprocessors
These preprocessors turn mixed, raw literals (possibly simplified) into literals suitable for reasoning. Typically some clauses are also added to the solver.
Given a term, try to preprocess it. Return None if it didn't change, or Some (u) if t=u. Can also add clauses to define new terms.
Preprocessing might transform terms to make them more amenable to reasoning, e.g. by removing boolean formulas via Tseitin encoding, adding clauses that encode their meaning in the same move.
Ask the SAT solver to decide the given literal in an extension of the current trail. This is useful for theory combination. If the SAT solver backtracks, this (potential) decision is removed and forgotten.
Register callbacked to be called with the slice of literals newly added on the trail.
This is called very often and should be efficient. It doesn't have to be complete, only correct. It's given only the slice of the trail consisting in new literals.
A model-production hook. It takes the solver, a class, and returns a term for this class. For example, an arithmetic theory might detect that a class contains a numeric constant, and return this constant as a model value.
If no hook assigns a value to a class, a fake value is created for it.
define_const si ~const ~rhs adds the definition const := rhs to the (future) proof. const should be a fresh constant that occurs nowhere else, and rhs a term defined without const.
simp_t si t returns u even if no simplification occurred (in which case t == u syntactically). It emits |- t=u. (see simplifier)
Preprocessors
These preprocessors turn mixed, raw literals (possibly simplified) into literals suitable for reasoning. Typically some clauses are also added to the solver.
Given a term, try to preprocess it. Return None if it didn't change, or Some (u) if t=u. Can also add clauses to define new terms.
Preprocessing might transform terms to make them more amenable to reasoning, e.g. by removing boolean formulas via Tseitin encoding, adding clauses that encode their meaning in the same move.
Ask the SAT solver to decide the given literal in an extension of the current trail. This is useful for theory combination. If the SAT solver backtracks, this (potential) decision is removed and forgotten.
Register callbacked to be called with the slice of literals newly added on the trail.
This is called very often and should be efficient. It doesn't have to be complete, only correct. It's given only the slice of the trail consisting in new literals.
A model-production hook. It takes the solver, a class, and returns a term for this class. For example, an arithmetic theory might detect that a class contains a numeric constant, and return this constant as a model value.
If no hook assigns a value to a class, a fake value is created for it.
Add a hook that will be called when a model is being produced
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_th_cstor/module-type-S/A/S/Solver_internal/index.html b/dev/sidekick/Sidekick_th_cstor/module-type-S/A/S/Solver_internal/index.html
index 8beadb95..3ca37e3c 100644
--- a/dev/sidekick/Sidekick_th_cstor/module-type-S/A/S/Solver_internal/index.html
+++ b/dev/sidekick/Sidekick_th_cstor/module-type-S/A/S/Solver_internal/index.html
@@ -1,2 +1,2 @@
-Solver_internal (sidekick.Sidekick_th_cstor.S.A.S.Solver_internal)
define_const si ~const ~rhs adds the definition const := rhs to the (future) proof. const should be a fresh constant that occurs nowhere else, and rhs a term defined without const.
simp_t si t returns u even if no simplification occurred (in which case t == u syntactically). It emits |- t=u. (see simplifier)
Preprocessors
These preprocessors turn mixed, raw literals (possibly simplified) into literals suitable for reasoning. Typically some clauses are also added to the solver.
Given a term, try to preprocess it. Return None if it didn't change, or Some (u) if t=u. Can also add clauses to define new terms.
Preprocessing might transform terms to make them more amenable to reasoning, e.g. by removing boolean formulas via Tseitin encoding, adding clauses that encode their meaning in the same move.
Ask the SAT solver to decide the given literal in an extension of the current trail. This is useful for theory combination. If the SAT solver backtracks, this (potential) decision is removed and forgotten.
Register callbacked to be called with the slice of literals newly added on the trail.
This is called very often and should be efficient. It doesn't have to be complete, only correct. It's given only the slice of the trail consisting in new literals.
A model-production hook. It takes the solver, a class, and returns a term for this class. For example, an arithmetic theory might detect that a class contains a numeric constant, and return this constant as a model value.
If no hook assigns a value to a class, a fake value is created for it.
define_const si ~const ~rhs adds the definition const := rhs to the (future) proof. const should be a fresh constant that occurs nowhere else, and rhs a term defined without const.
simp_t si t returns u even if no simplification occurred (in which case t == u syntactically). It emits |- t=u. (see simplifier)
Preprocessors
These preprocessors turn mixed, raw literals (possibly simplified) into literals suitable for reasoning. Typically some clauses are also added to the solver.
Given a term, try to preprocess it. Return None if it didn't change, or Some (u) if t=u. Can also add clauses to define new terms.
Preprocessing might transform terms to make them more amenable to reasoning, e.g. by removing boolean formulas via Tseitin encoding, adding clauses that encode their meaning in the same move.
Ask the SAT solver to decide the given literal in an extension of the current trail. This is useful for theory combination. If the SAT solver backtracks, this (potential) decision is removed and forgotten.
Register callbacked to be called with the slice of literals newly added on the trail.
This is called very often and should be efficient. It doesn't have to be complete, only correct. It's given only the slice of the trail consisting in new literals.
A model-production hook. It takes the solver, a class, and returns a term for this class. For example, an arithmetic theory might detect that a class contains a numeric constant, and return this constant as a model value.
If no hook assigns a value to a class, a fake value is created for it.
Add a hook that will be called when a model is being produced
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_th_data/Make/argument-1-A/S/Solver_internal/index.html b/dev/sidekick/Sidekick_th_data/Make/argument-1-A/S/Solver_internal/index.html
index 6aad92b5..8a1950fb 100644
--- a/dev/sidekick/Sidekick_th_data/Make/argument-1-A/S/Solver_internal/index.html
+++ b/dev/sidekick/Sidekick_th_data/Make/argument-1-A/S/Solver_internal/index.html
@@ -1,2 +1,2 @@
-Solver_internal (sidekick.Sidekick_th_data.Make.1-A.S.Solver_internal)
define_const si ~const ~rhs adds the definition const := rhs to the (future) proof. const should be a fresh constant that occurs nowhere else, and rhs a term defined without const.
simp_t si t returns u even if no simplification occurred (in which case t == u syntactically). It emits |- t=u. (see simplifier)
Preprocessors
These preprocessors turn mixed, raw literals (possibly simplified) into literals suitable for reasoning. Typically some clauses are also added to the solver.
Given a term, try to preprocess it. Return None if it didn't change, or Some (u) if t=u. Can also add clauses to define new terms.
Preprocessing might transform terms to make them more amenable to reasoning, e.g. by removing boolean formulas via Tseitin encoding, adding clauses that encode their meaning in the same move.
Ask the SAT solver to decide the given literal in an extension of the current trail. This is useful for theory combination. If the SAT solver backtracks, this (potential) decision is removed and forgotten.
Register callbacked to be called with the slice of literals newly added on the trail.
This is called very often and should be efficient. It doesn't have to be complete, only correct. It's given only the slice of the trail consisting in new literals.
A model-production hook. It takes the solver, a class, and returns a term for this class. For example, an arithmetic theory might detect that a class contains a numeric constant, and return this constant as a model value.
If no hook assigns a value to a class, a fake value is created for it.
define_const si ~const ~rhs adds the definition const := rhs to the (future) proof. const should be a fresh constant that occurs nowhere else, and rhs a term defined without const.
simp_t si t returns u even if no simplification occurred (in which case t == u syntactically). It emits |- t=u. (see simplifier)
Preprocessors
These preprocessors turn mixed, raw literals (possibly simplified) into literals suitable for reasoning. Typically some clauses are also added to the solver.
Given a term, try to preprocess it. Return None if it didn't change, or Some (u) if t=u. Can also add clauses to define new terms.
Preprocessing might transform terms to make them more amenable to reasoning, e.g. by removing boolean formulas via Tseitin encoding, adding clauses that encode their meaning in the same move.
Ask the SAT solver to decide the given literal in an extension of the current trail. This is useful for theory combination. If the SAT solver backtracks, this (potential) decision is removed and forgotten.
Register callbacked to be called with the slice of literals newly added on the trail.
This is called very often and should be efficient. It doesn't have to be complete, only correct. It's given only the slice of the trail consisting in new literals.
A model-production hook. It takes the solver, a class, and returns a term for this class. For example, an arithmetic theory might detect that a class contains a numeric constant, and return this constant as a model value.
If no hook assigns a value to a class, a fake value is created for it.
Add a hook that will be called when a model is being produced
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_th_data/module-type-ARG/S/Solver_internal/index.html b/dev/sidekick/Sidekick_th_data/module-type-ARG/S/Solver_internal/index.html
index 55e63633..85863de2 100644
--- a/dev/sidekick/Sidekick_th_data/module-type-ARG/S/Solver_internal/index.html
+++ b/dev/sidekick/Sidekick_th_data/module-type-ARG/S/Solver_internal/index.html
@@ -1,2 +1,2 @@
-Solver_internal (sidekick.Sidekick_th_data.ARG.S.Solver_internal)
define_const si ~const ~rhs adds the definition const := rhs to the (future) proof. const should be a fresh constant that occurs nowhere else, and rhs a term defined without const.
simp_t si t returns u even if no simplification occurred (in which case t == u syntactically). It emits |- t=u. (see simplifier)
Preprocessors
These preprocessors turn mixed, raw literals (possibly simplified) into literals suitable for reasoning. Typically some clauses are also added to the solver.
Given a term, try to preprocess it. Return None if it didn't change, or Some (u) if t=u. Can also add clauses to define new terms.
Preprocessing might transform terms to make them more amenable to reasoning, e.g. by removing boolean formulas via Tseitin encoding, adding clauses that encode their meaning in the same move.
Ask the SAT solver to decide the given literal in an extension of the current trail. This is useful for theory combination. If the SAT solver backtracks, this (potential) decision is removed and forgotten.
Register callbacked to be called with the slice of literals newly added on the trail.
This is called very often and should be efficient. It doesn't have to be complete, only correct. It's given only the slice of the trail consisting in new literals.
A model-production hook. It takes the solver, a class, and returns a term for this class. For example, an arithmetic theory might detect that a class contains a numeric constant, and return this constant as a model value.
If no hook assigns a value to a class, a fake value is created for it.
define_const si ~const ~rhs adds the definition const := rhs to the (future) proof. const should be a fresh constant that occurs nowhere else, and rhs a term defined without const.
simp_t si t returns u even if no simplification occurred (in which case t == u syntactically). It emits |- t=u. (see simplifier)
Preprocessors
These preprocessors turn mixed, raw literals (possibly simplified) into literals suitable for reasoning. Typically some clauses are also added to the solver.
Given a term, try to preprocess it. Return None if it didn't change, or Some (u) if t=u. Can also add clauses to define new terms.
Preprocessing might transform terms to make them more amenable to reasoning, e.g. by removing boolean formulas via Tseitin encoding, adding clauses that encode their meaning in the same move.
Ask the SAT solver to decide the given literal in an extension of the current trail. This is useful for theory combination. If the SAT solver backtracks, this (potential) decision is removed and forgotten.
Register callbacked to be called with the slice of literals newly added on the trail.
This is called very often and should be efficient. It doesn't have to be complete, only correct. It's given only the slice of the trail consisting in new literals.
A model-production hook. It takes the solver, a class, and returns a term for this class. For example, an arithmetic theory might detect that a class contains a numeric constant, and return this constant as a model value.
If no hook assigns a value to a class, a fake value is created for it.
Add a hook that will be called when a model is being produced
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_th_data/module-type-S/A/S/Solver_internal/index.html b/dev/sidekick/Sidekick_th_data/module-type-S/A/S/Solver_internal/index.html
index cc42c133..cc1ffe06 100644
--- a/dev/sidekick/Sidekick_th_data/module-type-S/A/S/Solver_internal/index.html
+++ b/dev/sidekick/Sidekick_th_data/module-type-S/A/S/Solver_internal/index.html
@@ -1,2 +1,2 @@
-Solver_internal (sidekick.Sidekick_th_data.S.A.S.Solver_internal)
define_const si ~const ~rhs adds the definition const := rhs to the (future) proof. const should be a fresh constant that occurs nowhere else, and rhs a term defined without const.
simp_t si t returns u even if no simplification occurred (in which case t == u syntactically). It emits |- t=u. (see simplifier)
Preprocessors
These preprocessors turn mixed, raw literals (possibly simplified) into literals suitable for reasoning. Typically some clauses are also added to the solver.
Given a term, try to preprocess it. Return None if it didn't change, or Some (u) if t=u. Can also add clauses to define new terms.
Preprocessing might transform terms to make them more amenable to reasoning, e.g. by removing boolean formulas via Tseitin encoding, adding clauses that encode their meaning in the same move.
Ask the SAT solver to decide the given literal in an extension of the current trail. This is useful for theory combination. If the SAT solver backtracks, this (potential) decision is removed and forgotten.
Register callbacked to be called with the slice of literals newly added on the trail.
This is called very often and should be efficient. It doesn't have to be complete, only correct. It's given only the slice of the trail consisting in new literals.
A model-production hook. It takes the solver, a class, and returns a term for this class. For example, an arithmetic theory might detect that a class contains a numeric constant, and return this constant as a model value.
If no hook assigns a value to a class, a fake value is created for it.
define_const si ~const ~rhs adds the definition const := rhs to the (future) proof. const should be a fresh constant that occurs nowhere else, and rhs a term defined without const.
simp_t si t returns u even if no simplification occurred (in which case t == u syntactically). It emits |- t=u. (see simplifier)
Preprocessors
These preprocessors turn mixed, raw literals (possibly simplified) into literals suitable for reasoning. Typically some clauses are also added to the solver.
Given a term, try to preprocess it. Return None if it didn't change, or Some (u) if t=u. Can also add clauses to define new terms.
Preprocessing might transform terms to make them more amenable to reasoning, e.g. by removing boolean formulas via Tseitin encoding, adding clauses that encode their meaning in the same move.
Ask the SAT solver to decide the given literal in an extension of the current trail. This is useful for theory combination. If the SAT solver backtracks, this (potential) decision is removed and forgotten.
Register callbacked to be called with the slice of literals newly added on the trail.
This is called very often and should be efficient. It doesn't have to be complete, only correct. It's given only the slice of the trail consisting in new literals.
A model-production hook. It takes the solver, a class, and returns a term for this class. For example, an arithmetic theory might detect that a class contains a numeric constant, and return this constant as a model value.
If no hook assigns a value to a class, a fake value is created for it.
Add a hook that will be called when a model is being produced
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_util/VecI32/index.html b/dev/sidekick/Sidekick_util/VecI32/index.html
index 1918dfd8..2354b224 100644
--- a/dev/sidekick/Sidekick_util/VecI32/index.html
+++ b/dev/sidekick/Sidekick_util/VecI32/index.html
@@ -1,2 +1,2 @@
-VecI32 (sidekick.Sidekick_util.VecI32)
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_util/Vec_float/index.html b/dev/sidekick/Sidekick_util/Vec_float/index.html
index cabd9d5d..3570d805 100644
--- a/dev/sidekick/Sidekick_util/Vec_float/index.html
+++ b/dev/sidekick/Sidekick_util/Vec_float/index.html
@@ -1,2 +1,2 @@
-Vec_float (sidekick.Sidekick_util.Vec_float)
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_util/Vec_sig/module-type-S/index.html b/dev/sidekick/Sidekick_util/Vec_sig/module-type-S/index.html
index 505cd1a6..168bbb6c 100644
--- a/dev/sidekick/Sidekick_util/Vec_sig/module-type-S/index.html
+++ b/dev/sidekick/Sidekick_util/Vec_sig/module-type-S/index.html
@@ -1,2 +1,2 @@
-S (sidekick.Sidekick_util.Vec_sig.S)
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_util__/VecI32/index.html b/dev/sidekick/Sidekick_util__/VecI32/index.html
index 7eaa908d..ea584e12 100644
--- a/dev/sidekick/Sidekick_util__/VecI32/index.html
+++ b/dev/sidekick/Sidekick_util__/VecI32/index.html
@@ -1,2 +1,2 @@
-VecI32 (sidekick.Sidekick_util__.VecI32)
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_util__/Vec_float/index.html b/dev/sidekick/Sidekick_util__/Vec_float/index.html
index 01ce5901..c833d6fe 100644
--- a/dev/sidekick/Sidekick_util__/Vec_float/index.html
+++ b/dev/sidekick/Sidekick_util__/Vec_float/index.html
@@ -1,2 +1,2 @@
-Vec_float (sidekick.Sidekick_util__.Vec_float)
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_util__/Vec_sig/module-type-S/index.html b/dev/sidekick/Sidekick_util__/Vec_sig/module-type-S/index.html
index 8b6cadf2..d6b4cc14 100644
--- a/dev/sidekick/Sidekick_util__/Vec_sig/module-type-S/index.html
+++ b/dev/sidekick/Sidekick_util__/Vec_sig/module-type-S/index.html
@@ -1,2 +1,2 @@
-S (sidekick.Sidekick_util__.Vec_sig.S)
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_util__VecI32/index.html b/dev/sidekick/Sidekick_util__VecI32/index.html
index a296365b..ab8956eb 100644
--- a/dev/sidekick/Sidekick_util__VecI32/index.html
+++ b/dev/sidekick/Sidekick_util__VecI32/index.html
@@ -1,2 +1,2 @@
-Sidekick_util__VecI32 (sidekick.Sidekick_util__VecI32)
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_util__Vec_float/index.html b/dev/sidekick/Sidekick_util__Vec_float/index.html
index e9e93f60..27067541 100644
--- a/dev/sidekick/Sidekick_util__Vec_float/index.html
+++ b/dev/sidekick/Sidekick_util__Vec_float/index.html
@@ -1,2 +1,2 @@
-Sidekick_util__Vec_float (sidekick.Sidekick_util__Vec_float)
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_util__Vec_sig/module-type-S/index.html b/dev/sidekick/Sidekick_util__Vec_sig/module-type-S/index.html
index 17a8feea..24a582b1 100644
--- a/dev/sidekick/Sidekick_util__Vec_sig/module-type-S/index.html
+++ b/dev/sidekick/Sidekick_util__Vec_sig/module-type-S/index.html
@@ -1,2 +1,2 @@
-S (sidekick.Sidekick_util__Vec_sig.S)