diff --git a/dev/sidekick-base/Sidekick_base_solver/Th_lia/A/LRA_solver/A/Gensym/index.html b/dev/sidekick-base/Sidekick_base_solver/Th_lia/A/LRA_solver/A/Gensym/index.html deleted file mode 100644 index d995757c..00000000 --- a/dev/sidekick-base/Sidekick_base_solver/Th_lia/A/LRA_solver/A/Gensym/index.html +++ /dev/null @@ -1,2 +0,0 @@ - -
A.GensymA.Qtype t = Q.tval zero : tval one : tval minus_one : tval sign : t -> intval of_int : int -> tval hash : t -> intval pp : t CCFormat.printertype bigint = Z.tval infinity : tval minus_infinity : tval is_real : t -> boolval is_int : t -> boolval pp_approx : int -> Stdlib.Format.formatter -> t -> unitT.FunTerm.Tbltype key = ttype !'a t = 'a T.Term.Tbl.tval create : int -> 'a tval clear : 'a t -> unitval reset : 'a t -> unitval length : 'a t -> intval stats : 'a t -> Stdlib.Hashtbl.statisticsval to_seq_values : 'a t -> 'a Stdlib.Seq.tval values : 'a t -> 'a CCHashtbl.iterval values_list : 'a t -> 'a listT.Termtype t = T.Term.tval hash : t -> intval pp : t Sidekick_core.Fmt.printertype store = T.Term.storeval as_bool : t -> bool optionmodule Tbl : sig ... endT.Tytype t = T.Ty.tval hash : t -> intval pp : t Sidekick_core.Fmt.printertype store = T.Ty.storeval is_bool : t -> boolLit.TS.Litmodule T : sig ... endtype t = S.Lit.tval sign : t -> boolval atom : ?sign:bool -> T.Term.store -> T.Term.t -> tval hash : t -> intval pp : t Sidekick_core.Fmt.printerS.ModelP.Step_vectype elt = proof_steptype t = S.P.Step_vec.tval size : t -> intval create : ?cap:int -> unit -> tval clear : t -> unitval is_empty : t -> boolval fast_remove : t -> int -> unitval ensure_size : t -> int -> unitval shrink : t -> int -> unitS.Ptype t = prooftype proof_step = proof_steptype term = T.Term.ttype lit = Lit.ttype proof_rule = t -> proof_stepmodule Step_vec : sig ... endval enabled : t -> boolval emit_input_clause : lit Iter.t -> proof_ruleval emit_redundant_clause : lit Iter.t -> hyps:proof_step Iter.t -> proof_ruleval emit_unsat_core : lit Iter.t -> proof_ruleval emit_unsat : proof_step -> t -> unitval del_clause : proof_step -> lit Iter.t -> t -> unitval lemma_cc : lit Iter.t -> proof_ruleval define_term : term -> term -> proof_ruleval proof_p1 : proof_step -> proof_step -> proof_ruleval proof_r1 : proof_step -> proof_step -> proof_ruleval proof_res : pivot:term -> proof_step -> proof_step -> proof_ruleval with_defs : proof_step -> proof_step Iter.t -> proof_ruleval lemma_true : term -> proof_ruleval lemma_preprocess : term -> term -> using:proof_step Iter.t -> proof_ruleval lemma_rw_clause :
- proof_step ->
- res:lit Iter.t ->
- using:proof_step Iter.t ->
- proof_ruleS.Registrytype t = S.Registry.ttype 'a key = 'a S.Registry.keyval create_key : unit -> 'a keyval create : unit -> tT.FunTerm.Tbltype key = ttype !'a t = 'a T.Term.Tbl.tval create : int -> 'a tval clear : 'a t -> unitval reset : 'a t -> unitval length : 'a t -> intval stats : 'a t -> Stdlib.Hashtbl.statisticsval to_seq_values : 'a t -> 'a Stdlib.Seq.tval values : 'a t -> 'a CCHashtbl.iterval values_list : 'a t -> 'a listT.Termtype t = T.Term.tval hash : t -> intval pp : t Sidekick_core.Fmt.printertype store = T.Term.storeval as_bool : t -> bool optionmodule Tbl : sig ... endT.Tytype t = T.Ty.tval hash : t -> intval pp : t Sidekick_core.Fmt.printertype store = T.Ty.storeval is_bool : t -> boolLit.TActions.Litmodule T : sig ... endtype t = Lit.tval sign : t -> boolval atom : ?sign:bool -> T.Term.store -> T.Term.t -> tval hash : t -> intval pp : t Sidekick_core.Fmt.printerP.Step_vectype elt = proof_stepval size : t -> intval create : ?cap:int -> unit -> tval clear : t -> unitval is_empty : t -> boolval fast_remove : t -> int -> unitval ensure_size : t -> int -> unitval shrink : t -> int -> unitActions.Ptype t = prooftype proof_step = proof_steptype term = T.Term.ttype lit = Lit.ttype proof_rule = t -> proof_stepmodule Step_vec : sig ... endval enabled : t -> boolval emit_input_clause : lit Iter.t -> proof_ruleval emit_redundant_clause : lit Iter.t -> hyps:proof_step Iter.t -> proof_ruleval emit_unsat_core : lit Iter.t -> proof_ruleval emit_unsat : proof_step -> t -> unitval del_clause : proof_step -> lit Iter.t -> t -> unitval lemma_cc : lit Iter.t -> proof_ruleval define_term : term -> term -> proof_ruleval proof_p1 : proof_step -> proof_step -> proof_ruleval proof_r1 : proof_step -> proof_step -> proof_ruleval proof_res : pivot:term -> proof_step -> proof_step -> proof_ruleval with_defs : proof_step -> proof_step Iter.t -> proof_ruleval lemma_true : term -> proof_ruleval lemma_preprocess : term -> term -> using:proof_step Iter.t -> proof_ruleval lemma_rw_clause :
- proof_step ->
- res:lit Iter.t ->
- using:proof_step Iter.t ->
- proof_ruleT.FunTerm.Tbltype key = ttype !'a t = 'a T.Term.Tbl.tval create : int -> 'a tval clear : 'a t -> unitval reset : 'a t -> unitval length : 'a t -> intval stats : 'a t -> Stdlib.Hashtbl.statisticsval to_seq_values : 'a t -> 'a Stdlib.Seq.tval values : 'a t -> 'a CCHashtbl.iterval values_list : 'a t -> 'a listT.Termtype t = T.Term.tval hash : t -> intval pp : t Sidekick_core.Fmt.printertype store = T.Term.storeval as_bool : t -> bool optionmodule Tbl : sig ... endT.Tytype t = T.Ty.tval hash : t -> intval pp : t Sidekick_core.Fmt.printertype store = T.Ty.storeval is_bool : t -> boolActions.TCC.Actionsmodule T : sig ... endmodule Lit : sig ... endtype proof = prooftype proof_step = proof_stepmodule P : sig ... endtype t = theory_actionsval raise_conflict : t -> Lit.t list -> proof_step -> 'aval propagate :
- t ->
- Lit.t ->
- reason:( unit -> Lit.t list * proof_step ) ->
- unitCC.Debug_val pp : t Sidekick_core.Fmt.printerCC.Expltype t = S.Solver_internal.CC.Expl.tval pp : t Sidekick_core.Fmt.printerT.FunTerm.Tbltype key = ttype !'a t = 'a T.Term.Tbl.tval create : int -> 'a tval clear : 'a t -> unitval reset : 'a t -> unitval length : 'a t -> intval stats : 'a t -> Stdlib.Hashtbl.statisticsval to_seq_values : 'a t -> 'a Stdlib.Seq.tval values : 'a t -> 'a CCHashtbl.iterval values_list : 'a t -> 'a listT.Termtype t = T.Term.tval hash : t -> intval pp : t Sidekick_core.Fmt.printertype store = T.Term.storeval as_bool : t -> bool optionmodule Tbl : sig ... endT.Tytype t = T.Ty.tval hash : t -> intval pp : t Sidekick_core.Fmt.printertype store = T.Ty.storeval is_bool : t -> boolLit.TCC.Litmodule T : sig ... endtype t = Lit.tval sign : t -> boolval atom : ?sign:bool -> T.Term.store -> T.Term.t -> tval hash : t -> intval pp : t Sidekick_core.Fmt.printerCC.Ntype t = S.Solver_internal.CC.N.tval hash : t -> intval pp : t Sidekick_core.Fmt.printerval is_root : t -> booltype bitfield = S.Solver_internal.CC.N.bitfieldP.Step_vectype elt = proof_steptype t = S.Solver_internal.CC.P.Step_vec.tval size : t -> intval create : ?cap:int -> unit -> tval clear : t -> unitval is_empty : t -> boolval fast_remove : t -> int -> unitval ensure_size : t -> int -> unitval shrink : t -> int -> unitCC.Ptype t = prooftype proof_step = proof_steptype term = S.Solver_internal.CC.P.termtype lit = littype proof_rule = t -> proof_stepmodule Step_vec : sig ... endval enabled : t -> boolval emit_input_clause : lit Iter.t -> proof_ruleval emit_redundant_clause : lit Iter.t -> hyps:proof_step Iter.t -> proof_ruleval emit_unsat_core : lit Iter.t -> proof_ruleval emit_unsat : proof_step -> t -> unitval del_clause : proof_step -> lit Iter.t -> t -> unitval lemma_cc : lit Iter.t -> proof_ruleval define_term : term -> term -> proof_ruleval proof_p1 : proof_step -> proof_step -> proof_ruleval proof_r1 : proof_step -> proof_step -> proof_ruleval proof_res : pivot:term -> proof_step -> proof_step -> proof_ruleval with_defs : proof_step -> proof_step Iter.t -> proof_ruleval lemma_true : term -> proof_ruleval lemma_preprocess : term -> term -> using:proof_step Iter.t -> proof_ruleval lemma_rw_clause :
- proof_step ->
- res:lit Iter.t ->
- using:proof_step Iter.t ->
- proof_ruleCC.Resolved_expltype t = S.Solver_internal.CC.Resolved_expl.t = {lits : lit list; |
same_value : (N.t * N.t) list; |
pr : proof -> proof_step; |
}val is_semantic : t -> boolval pp : t Sidekick_core.Fmt.printerT.FunTerm.Tbltype key = ttype !'a t = 'a T.Term.Tbl.tval create : int -> 'a tval clear : 'a t -> unitval reset : 'a t -> unitval length : 'a t -> intval stats : 'a t -> Stdlib.Hashtbl.statisticsval to_seq_values : 'a t -> 'a Stdlib.Seq.tval values : 'a t -> 'a CCHashtbl.iterval values_list : 'a t -> 'a listT.Termtype t = T.Term.tval hash : t -> intval pp : t Sidekick_core.Fmt.printertype store = T.Term.storeval as_bool : t -> bool optionmodule Tbl : sig ... endT.Tytype t = T.Ty.tval hash : t -> intval pp : t Sidekick_core.Fmt.printertype store = T.Ty.storeval is_bool : t -> boolCC.TSolver_internal.CCmodule T : sig ... endmodule Lit : sig ... endtype proof = prooftype proof_step = proof_stepmodule P : sig ... endmodule Actions : sig ... endtype term_store = T.Term.storetype term = T.Term.ttype value = termtype fun_ = T.Fun.ttype lit = Lit.ttype actions = Actions.ttype t = S.Solver_internal.CC.tmodule N : sig ... endmodule Expl : sig ... endmodule Resolved_expl : sig ... endtype node = N.ttype repr = N.ttype explanation = Expl.tval term_store : t -> term_storetype ev_on_propagate = t -> lit -> ( unit -> lit list * proof_step ) -> unitval create :
- ?stat:Sidekick_util.Stat.t ->
- ?on_pre_merge:ev_on_pre_merge list ->
- ?on_post_merge:ev_on_post_merge list ->
- ?on_new_term:ev_on_new_term list ->
- ?on_conflict:ev_on_conflict list ->
- ?on_propagate:ev_on_propagate list ->
- ?on_is_subterm:ev_on_is_subterm list ->
- ?size:[ `Big | `Small ] ->
- term_store ->
- proof ->
- tval allocate_bitfield : descr:string -> t -> N.bitfieldval get_bitfield : t -> N.bitfield -> N.t -> boolval set_bitfield : t -> N.bitfield -> bool -> N.t -> unitval on_pre_merge : t -> ev_on_pre_merge -> unitval on_post_merge : t -> ev_on_post_merge -> unitval on_new_term : t -> ev_on_new_term -> unitval on_conflict : t -> ev_on_conflict -> unitval on_propagate : t -> ev_on_propagate -> unitval on_is_subterm : t -> ev_on_is_subterm -> unitval explain_eq : t -> N.t -> N.t -> Resolved_expl.tval with_model_mode : t -> ( unit -> 'a ) -> 'aval push_level : t -> unitval pop_levels : t -> int -> unitmodule Debug_ : sig ... endT.FunTerm.Tbltype key = ttype !'a t = 'a T.Term.Tbl.tval create : int -> 'a tval clear : 'a t -> unitval reset : 'a t -> unitval length : 'a t -> intval stats : 'a t -> Stdlib.Hashtbl.statisticsval to_seq_values : 'a t -> 'a Stdlib.Seq.tval values : 'a t -> 'a CCHashtbl.iterval values_list : 'a t -> 'a listT.Termtype t = T.Term.tval hash : t -> intval pp : t Sidekick_core.Fmt.printertype store = T.Term.storeval as_bool : t -> bool optionmodule Tbl : sig ... endT.Tytype t = T.Ty.tval hash : t -> intval pp : t Sidekick_core.Fmt.printertype store = T.Ty.storeval is_bool : t -> boolLit.TSolver_internal.Litmodule T : sig ... endtype t = Lit.tval sign : t -> boolval atom : ?sign:bool -> T.Term.store -> T.Term.t -> tval hash : t -> intval pp : t Sidekick_core.Fmt.printerP.Step_vectype elt = proof_steptype t = P.Step_vec.tval size : t -> intval create : ?cap:int -> unit -> tval clear : t -> unitval is_empty : t -> boolval fast_remove : t -> int -> unitval ensure_size : t -> int -> unitval shrink : t -> int -> unitSolver_internal.Ptype t = prooftype proof_step = proof_steptype term = T.Term.ttype lit = Lit.ttype proof_rule = t -> proof_stepmodule Step_vec : sig ... endval enabled : t -> boolval emit_input_clause : lit Iter.t -> proof_ruleval emit_redundant_clause : lit Iter.t -> hyps:proof_step Iter.t -> proof_ruleval emit_unsat_core : lit Iter.t -> proof_ruleval emit_unsat : proof_step -> t -> unitval del_clause : proof_step -> lit Iter.t -> t -> unitval lemma_cc : lit Iter.t -> proof_ruleval define_term : term -> term -> proof_ruleval proof_p1 : proof_step -> proof_step -> proof_ruleval proof_r1 : proof_step -> proof_step -> proof_ruleval proof_res : pivot:term -> proof_step -> proof_step -> proof_ruleval with_defs : proof_step -> proof_step Iter.t -> proof_ruleval lemma_true : term -> proof_ruleval lemma_preprocess : term -> term -> using:proof_step Iter.t -> proof_ruleval lemma_rw_clause :
- proof_step ->
- res:lit Iter.t ->
- using:proof_step Iter.t ->
- proof_ruleSolver_internal.Registrytype t = S.Solver_internal.Registry.ttype 'a key = 'a S.Solver_internal.Registry.keyval create_key : unit -> 'a keyval create : unit -> tSolver_internal.Simplifytype t = S.Solver_internal.Simplify.tval tst : t -> term_storeval clear : t -> unittype hook = t -> term -> (term * proof_step Iter.t) optionval normalize : t -> term -> (term * proof_step) optionval normalize_t : t -> term -> term * proof_step optionT.FunTerm.Tbltype key = ttype !'a t = 'a T.Term.Tbl.tval create : int -> 'a tval clear : 'a t -> unitval reset : 'a t -> unitval length : 'a t -> intval stats : 'a t -> Stdlib.Hashtbl.statisticsval to_seq_values : 'a t -> 'a Stdlib.Seq.tval values : 'a t -> 'a CCHashtbl.iterval values_list : 'a t -> 'a listT.Termtype t = T.Term.tval hash : t -> intval pp : t Sidekick_core.Fmt.printertype store = T.Term.storeval as_bool : t -> bool optionmodule Tbl : sig ... endT.Tytype t = T.Ty.tval hash : t -> intval pp : t Sidekick_core.Fmt.printertype store = T.Ty.storeval is_bool : t -> boolSolver_internal.TS.Solver_internalmodule T : sig ... endmodule Lit : sig ... endtype ty = T.Ty.ttype term = T.Term.ttype value = T.Term.ttype term_store = T.Term.storetype ty_store = T.Ty.storetype clause_pool = S.Solver_internal.clause_pooltype proof = prooftype proof_step = proof_stepmodule P : sig ... endtype t = S.Solver_internal.ttype solver = tval tst : t -> term_storeval stats : t -> Sidekick_util.Stat.tmodule Registry : sig ... endval registry : t -> Registry.ttype theory_actions = S.Solver_internal.theory_actionstype lit = Lit.tmodule CC : sig ... endmodule Simplify : sig ... endtype simplify_hook = Simplify.hookval add_simplifier : t -> Simplify.hook -> unitval simplify_t : t -> term -> (term * proof_step) optionval simp_t : t -> term -> term * proof_step optionmodule type PREPROCESS_ACTS = sig ... endtype preprocess_actions = (module PREPROCESS_ACTS)type preprocess_hook = t -> preprocess_actions -> term -> unitval on_preprocess : t -> preprocess_hook -> unitval raise_conflict : t -> theory_actions -> lit list -> proof_step -> 'aval push_decision : t -> theory_actions -> lit -> unitval propagate :
- t ->
- theory_actions ->
- lit ->
- reason:( unit -> lit list * proof_step ) ->
- unitval propagate_l : t -> theory_actions -> lit -> lit list -> proof_step -> unitval add_clause_temp : t -> theory_actions -> lit list -> proof_step -> unitval add_clause_permanent :
- t ->
- theory_actions ->
- lit list ->
- proof_step ->
- unitval mk_lit : t -> theory_actions -> ?sign:bool -> term -> litval add_lit : t -> theory_actions -> ?default_pol:bool -> lit -> unitval add_lit_t : t -> theory_actions -> ?sign:bool -> term -> unitval cc_raise_conflict_expl : t -> theory_actions -> CC.Expl.t -> 'aval cc_merge : t -> theory_actions -> CC.N.t -> CC.N.t -> CC.Expl.t -> unitval cc_merge_t : t -> theory_actions -> term -> term -> CC.Expl.t -> unitval on_cc_post_merge :
- t ->
- ( CC.t -> theory_actions -> CC.N.t -> CC.N.t -> unit ) ->
- unitval on_cc_propagate :
- t ->
- ( CC.t -> lit -> ( unit -> lit list * proof_step ) -> unit ) ->
- unitval on_partial_check :
- t ->
- ( t -> theory_actions -> lit Iter.t -> unit ) ->
- unitval on_final_check : t -> ( t -> theory_actions -> lit Iter.t -> unit ) -> unitval on_th_combination :
- t ->
- ( t -> theory_actions -> (term * value) Iter.t ) ->
- unitval declare_pb_is_incomplete : t -> unitval on_model :
- ?ask:model_ask_hook ->
- ?complete:model_completion_hook ->
- t ->
- unitSolver_internal.PREPROCESS_ACTSval proof : proofval add_clause : lit list -> proof_step -> unitval add_lit : ?default_pol:bool -> lit -> unitT.FunTerm.Tbltype key = ttype !'a t = 'a S.T.Term.Tbl.tval create : int -> 'a tval clear : 'a t -> unitval reset : 'a t -> unitval length : 'a t -> intval stats : 'a t -> Stdlib.Hashtbl.statisticsval to_seq_values : 'a t -> 'a Stdlib.Seq.tval values : 'a t -> 'a CCHashtbl.iterval values_list : 'a t -> 'a listT.Termtype t = S.T.Term.tval hash : t -> intval pp : t Sidekick_core.Fmt.printertype store = S.T.Term.storeval as_bool : t -> bool optionmodule Tbl : sig ... endT.Tytype t = S.T.Ty.tval hash : t -> intval pp : t Sidekick_core.Fmt.printertype store = S.T.Ty.storeval is_bool : t -> boolS.TS.Unknowntype t = S.Unknown.tval pp : t CCFormat.printerA.Smodule T : sig ... endmodule Lit : sig ... endtype proof = S.prooftype proof_step = S.proof_stepmodule P : sig ... endmodule Solver_internal : sig ... endtype t = S.ttype solver = ttype term = T.Term.ttype ty = T.Ty.ttype lit = Lit.tmodule Registry : sig ... endval registry : t -> Registry.tmodule type THEORY = sig ... endtype theory = (module THEORY)val mk_theory :
- name:string ->
- create_and_setup:( Solver_internal.t -> 'th ) ->
- ?push_level:( 'th -> unit ) ->
- ?pop_levels:( 'th -> int -> unit ) ->
- unit ->
- theorymodule Model : sig ... endmodule Unknown : sig ... endval stats : t -> Sidekick_util.Stat.tval tst : t -> T.Term.storeval ty_st : t -> T.Ty.storeval create :
- ?stat:Sidekick_util.Stat.t ->
- ?size:[ `Big | `Small | `Tiny ] ->
- proof:proof ->
- theories:theory list ->
- T.Term.store ->
- T.Ty.store ->
- unit ->
- tval add_clause : t -> lit Sidekick_util.IArray.t -> proof_step -> unitval add_clause_l : t -> lit list -> proof_step -> unittype res = S.res = | Sat of Model.t | ||
| Unsat of {
} | ||
| Unknown of Unknown.t |
val pop_assumptions : t -> int -> unittype propagation_result = S.propagation_result = | PR_sat | |
| PR_conflict of {
} | |
| PR_unsat of {
} |
val check_sat_propagations_only :
- assumptions:lit list ->
- t ->
- propagation_resultval pp_stats : t CCFormat.printerS.THEORYval create_and_setup : Solver_internal.t -> tval push_level : t -> unitval pop_levels : t -> int -> unitA.Zval zero : tval one : tval minus_one : tval sign : t -> intval of_int : int -> tval hash : t -> intval pp : t CCFormat.printerLRA_solver.Amodule S : sig ... endmodule Z : sig ... endmodule Q : sig ... endtype term = S.T.Term.ttype ty = S.T.Ty.tval view_as_lra : term -> ( Q.t, term ) Sidekick_arith_lra.lra_viewval mk_bool : S.T.Term.store -> bool -> termval mk_lra :
- S.T.Term.store ->
- ( Q.t, term ) Sidekick_arith_lra.lra_view ->
- termval ty_lra : S.T.Term.store -> tyval mk_eq : S.T.Term.store -> term -> term -> termval has_ty_real : term -> boolval lemma_lra : S.Lit.t Iter.t -> S.P.proof_rulemodule Gensym : sig ... endSimpSolver.ConstraintSimpSolver.Qtype t = Th_lra.SimpSolver.Q.tval zero : tval one : tval minus_one : tval sign : t -> intval of_int : int -> tval hash : t -> intval pp : t CCFormat.printertype bigint = Z.tval infinity : tval minus_infinity : tval is_real : t -> boolval is_int : t -> boolval pp_approx : int -> Stdlib.Format.formatter -> t -> unitSimpSolver.SubstSimpSolver.Unsat_certSimpSolver.Vtype t = Th_lra.SimpSolver.V.tval pp : t Sidekick_util.Fmt.printertype lit = Th_lra.SimpSolver.V.litval pp_lit : lit Sidekick_util.Fmt.printerSimpSolver.V_maptype key = V.tval empty : 'a tval is_empty : 'a t -> boolval cardinal : 'a t -> intval values : 'a t -> 'a CCMap.iterSimpSolver.Ztype t = Th_lra.SimpSolver.Z.tval zero : tval one : tval minus_one : tval sign : t -> intval of_int : int -> tval hash : t -> intval pp : t CCFormat.printerLRA_solver.SimpSolvermodule V : sig ... endmodule V_map : sig ... endmodule Z : sig ... endmodule Q : sig ... endtype num = Q.tmodule Constraint : sig ... endmodule Subst : sig ... endtype t = Th_lra.SimpSolver.tval create : ?stat:Sidekick_util.Stat.t -> unit -> tval push_level : t -> unitval pop_levels : t -> int -> unittype unsat_cert = Th_lra.SimpSolver.unsat_certmodule Unsat_cert : sig ... endexception E_unsat of Unsat_cert.tval add_constraint :
- ?keep_on_backtracking:bool ->
- ?is_int:bool ->
- on_propagate:ev_on_propagate ->
- t ->
- Constraint.t ->
- V.lit ->
- unitval declare_bound : ?is_int:bool -> t -> Constraint.t -> V.lit -> unitval n_vars : t -> intval n_rows : t -> intval _check_invariants : t -> unitval _check_cert : unsat_cert -> unitA.LRA_solvermodule A : sig ... endmodule SimpSolver : sig ... endtype state = Th_lra.stateval create : ?stat:Sidekick_util.Stat.t -> A.S.Solver_internal.t -> stateval k_state : state A.S.Solver_internal.Registry.keyval theory : A.S.theoryA.Qval zero : tval one : tval minus_one : tval sign : t -> intval of_int : int -> tval hash : t -> intval pp : t CCFormat.printertype bigint = Z.tval infinity : tval minus_infinity : tval is_real : t -> boolval is_int : t -> boolval pp_approx : int -> Stdlib.Format.formatter -> t -> unitT.FunTerm.Tbltype key = ttype !'a t = 'a T.Term.Tbl.tval create : int -> 'a tval clear : 'a t -> unitval reset : 'a t -> unitval length : 'a t -> intval stats : 'a t -> Stdlib.Hashtbl.statisticsval to_seq_values : 'a t -> 'a Stdlib.Seq.tval values : 'a t -> 'a CCHashtbl.iterval values_list : 'a t -> 'a listT.Termtype t = T.Term.tval hash : t -> intval pp : t Sidekick_core.Fmt.printertype store = T.Term.storeval as_bool : t -> bool optionmodule Tbl : sig ... endT.Tytype t = T.Ty.tval hash : t -> intval pp : t Sidekick_core.Fmt.printertype store = T.Ty.storeval is_bool : t -> boolLit.TS.Litmodule T : sig ... endtype t = Solver_arg.Lit.tval sign : t -> boolval atom : ?sign:bool -> T.Term.store -> T.Term.t -> tval hash : t -> intval pp : t Sidekick_core.Fmt.printerS.ModelP.Step_vectype elt = proof_steptype t = Solver_arg.P.Step_vec.tval size : t -> intval create : ?cap:int -> unit -> tval clear : t -> unitval is_empty : t -> boolval fast_remove : t -> int -> unitval ensure_size : t -> int -> unitval shrink : t -> int -> unitS.Ptype t = prooftype proof_step = proof_steptype term = T.Term.ttype lit = Lit.ttype proof_rule = t -> proof_stepmodule Step_vec : sig ... endval enabled : t -> boolval emit_input_clause : lit Iter.t -> proof_ruleval emit_redundant_clause : lit Iter.t -> hyps:proof_step Iter.t -> proof_ruleval emit_unsat_core : lit Iter.t -> proof_ruleval emit_unsat : proof_step -> t -> unitval del_clause : proof_step -> lit Iter.t -> t -> unitval lemma_cc : lit Iter.t -> proof_ruleval define_term : term -> term -> proof_ruleval proof_p1 : proof_step -> proof_step -> proof_ruleval proof_r1 : proof_step -> proof_step -> proof_ruleval proof_res : pivot:term -> proof_step -> proof_step -> proof_ruleval with_defs : proof_step -> proof_step Iter.t -> proof_ruleval lemma_true : term -> proof_ruleval lemma_preprocess : term -> term -> using:proof_step Iter.t -> proof_ruleval lemma_rw_clause :
- proof_step ->
- res:lit Iter.t ->
- using:proof_step Iter.t ->
- proof_ruleS.Registrytype 'a key = 'a Sidekick_smt_solver.Make(Solver_arg).Registry.keyval create_key : unit -> 'a keyval create : unit -> tT.FunTerm.Tbltype key = ttype !'a t = 'a T.Term.Tbl.tval create : int -> 'a tval clear : 'a t -> unitval reset : 'a t -> unitval length : 'a t -> intval stats : 'a t -> Stdlib.Hashtbl.statisticsval to_seq_values : 'a t -> 'a Stdlib.Seq.tval values : 'a t -> 'a CCHashtbl.iterval values_list : 'a t -> 'a listT.Termtype t = T.Term.tval hash : t -> intval pp : t Sidekick_core.Fmt.printertype store = T.Term.storeval as_bool : t -> bool optionmodule Tbl : sig ... endT.Tytype t = T.Ty.tval hash : t -> intval pp : t Sidekick_core.Fmt.printertype store = T.Ty.storeval is_bool : t -> boolLit.TActions.Litmodule T : sig ... endtype t = Lit.tval sign : t -> boolval atom : ?sign:bool -> T.Term.store -> T.Term.t -> tval hash : t -> intval pp : t Sidekick_core.Fmt.printerP.Step_vectype elt = proof_stepval size : t -> intval create : ?cap:int -> unit -> tval clear : t -> unitval is_empty : t -> boolval fast_remove : t -> int -> unitval ensure_size : t -> int -> unitval shrink : t -> int -> unitActions.Ptype t = prooftype proof_step = proof_steptype term = T.Term.ttype lit = Lit.ttype proof_rule = t -> proof_stepmodule Step_vec : sig ... endval enabled : t -> boolval emit_input_clause : lit Iter.t -> proof_ruleval emit_redundant_clause : lit Iter.t -> hyps:proof_step Iter.t -> proof_ruleval emit_unsat_core : lit Iter.t -> proof_ruleval emit_unsat : proof_step -> t -> unitval del_clause : proof_step -> lit Iter.t -> t -> unitval lemma_cc : lit Iter.t -> proof_ruleval define_term : term -> term -> proof_ruleval proof_p1 : proof_step -> proof_step -> proof_ruleval proof_r1 : proof_step -> proof_step -> proof_ruleval proof_res : pivot:term -> proof_step -> proof_step -> proof_ruleval with_defs : proof_step -> proof_step Iter.t -> proof_ruleval lemma_true : term -> proof_ruleval lemma_preprocess : term -> term -> using:proof_step Iter.t -> proof_ruleval lemma_rw_clause :
- proof_step ->
- res:lit Iter.t ->
- using:proof_step Iter.t ->
- proof_ruleT.FunTerm.Tbltype key = ttype !'a t = 'a T.Term.Tbl.tval create : int -> 'a tval clear : 'a t -> unitval reset : 'a t -> unitval length : 'a t -> intval stats : 'a t -> Stdlib.Hashtbl.statisticsval to_seq_values : 'a t -> 'a Stdlib.Seq.tval values : 'a t -> 'a CCHashtbl.iterval values_list : 'a t -> 'a listT.Termtype t = T.Term.tval hash : t -> intval pp : t Sidekick_core.Fmt.printertype store = T.Term.storeval as_bool : t -> bool optionmodule Tbl : sig ... endT.Tytype t = T.Ty.tval hash : t -> intval pp : t Sidekick_core.Fmt.printertype store = T.Ty.storeval is_bool : t -> boolActions.TCC.Actionsmodule T : sig ... endmodule Lit : sig ... endtype proof = prooftype proof_step = proof_stepmodule P : sig ... endtype t = theory_actionsval raise_conflict : t -> Lit.t list -> proof_step -> 'aval propagate :
- t ->
- Lit.t ->
- reason:( unit -> Lit.t list * proof_step ) ->
- unitCC.Debug_val pp : t Sidekick_core.Fmt.printerCC.Explval pp : t Sidekick_core.Fmt.printerT.FunTerm.Tbltype key = ttype !'a t = 'a T.Term.Tbl.tval create : int -> 'a tval clear : 'a t -> unitval reset : 'a t -> unitval length : 'a t -> intval stats : 'a t -> Stdlib.Hashtbl.statisticsval to_seq_values : 'a t -> 'a Stdlib.Seq.tval values : 'a t -> 'a CCHashtbl.iterval values_list : 'a t -> 'a listT.Termtype t = T.Term.tval hash : t -> intval pp : t Sidekick_core.Fmt.printertype store = T.Term.storeval as_bool : t -> bool optionmodule Tbl : sig ... endT.Tytype t = T.Ty.tval hash : t -> intval pp : t Sidekick_core.Fmt.printertype store = T.Ty.storeval is_bool : t -> boolLit.TCC.Litmodule T : sig ... endtype t = Lit.tval sign : t -> boolval atom : ?sign:bool -> T.Term.store -> T.Term.t -> tval hash : t -> intval pp : t Sidekick_core.Fmt.printerCC.Nval hash : t -> intval pp : t Sidekick_core.Fmt.printerval is_root : t -> booltype bitfield =
- Sidekick_smt_solver.Make(Solver_arg).Solver_internal.CC.N.bitfieldP.Step_vectype elt = proof_stepval size : t -> intval create : ?cap:int -> unit -> tval clear : t -> unitval is_empty : t -> boolval fast_remove : t -> int -> unitval ensure_size : t -> int -> unitval shrink : t -> int -> unitCC.Ptype t = prooftype proof_step = proof_steptype lit = littype proof_rule = t -> proof_stepmodule Step_vec : sig ... endval enabled : t -> boolval emit_input_clause : lit Iter.t -> proof_ruleval emit_redundant_clause : lit Iter.t -> hyps:proof_step Iter.t -> proof_ruleval emit_unsat_core : lit Iter.t -> proof_ruleval emit_unsat : proof_step -> t -> unitval del_clause : proof_step -> lit Iter.t -> t -> unitval lemma_cc : lit Iter.t -> proof_ruleval define_term : term -> term -> proof_ruleval proof_p1 : proof_step -> proof_step -> proof_ruleval proof_r1 : proof_step -> proof_step -> proof_ruleval proof_res : pivot:term -> proof_step -> proof_step -> proof_ruleval with_defs : proof_step -> proof_step Iter.t -> proof_ruleval lemma_true : term -> proof_ruleval lemma_preprocess : term -> term -> using:proof_step Iter.t -> proof_ruleval lemma_rw_clause :
- proof_step ->
- res:lit Iter.t ->
- using:proof_step Iter.t ->
- proof_ruleCC.Resolved_expltype t =
- Sidekick_smt_solver.Make(Solver_arg).Solver_internal.CC.Resolved_expl.t =
- {lits : lit list; |
same_value : (N.t * N.t) list; |
pr : proof -> proof_step; |
}val is_semantic : t -> boolval pp : t Sidekick_core.Fmt.printerT.FunTerm.Tbltype key = ttype !'a t = 'a T.Term.Tbl.tval create : int -> 'a tval clear : 'a t -> unitval reset : 'a t -> unitval length : 'a t -> intval stats : 'a t -> Stdlib.Hashtbl.statisticsval to_seq_values : 'a t -> 'a Stdlib.Seq.tval values : 'a t -> 'a CCHashtbl.iterval values_list : 'a t -> 'a listT.Termtype t = T.Term.tval hash : t -> intval pp : t Sidekick_core.Fmt.printertype store = T.Term.storeval as_bool : t -> bool optionmodule Tbl : sig ... endT.Tytype t = T.Ty.tval hash : t -> intval pp : t Sidekick_core.Fmt.printertype store = T.Ty.storeval is_bool : t -> boolCC.TSolver_internal.CCmodule T : sig ... endmodule Lit : sig ... endtype proof = prooftype proof_step = proof_stepmodule P : sig ... endmodule Actions : sig ... endtype term_store = T.Term.storetype term = T.Term.ttype value = termtype fun_ = T.Fun.ttype lit = Lit.ttype actions = Actions.tmodule N : sig ... endmodule Expl : sig ... endmodule Resolved_expl : sig ... endtype node = N.ttype repr = N.ttype explanation = Expl.tval term_store : t -> term_storetype ev_on_propagate = t -> lit -> ( unit -> lit list * proof_step ) -> unitval create :
- ?stat:Sidekick_util.Stat.t ->
- ?on_pre_merge:ev_on_pre_merge list ->
- ?on_post_merge:ev_on_post_merge list ->
- ?on_new_term:ev_on_new_term list ->
- ?on_conflict:ev_on_conflict list ->
- ?on_propagate:ev_on_propagate list ->
- ?on_is_subterm:ev_on_is_subterm list ->
- ?size:[ `Big | `Small ] ->
- term_store ->
- proof ->
- tval allocate_bitfield : descr:string -> t -> N.bitfieldval get_bitfield : t -> N.bitfield -> N.t -> boolval set_bitfield : t -> N.bitfield -> bool -> N.t -> unitval on_pre_merge : t -> ev_on_pre_merge -> unitval on_post_merge : t -> ev_on_post_merge -> unitval on_new_term : t -> ev_on_new_term -> unitval on_conflict : t -> ev_on_conflict -> unitval on_propagate : t -> ev_on_propagate -> unitval on_is_subterm : t -> ev_on_is_subterm -> unitval explain_eq : t -> N.t -> N.t -> Resolved_expl.tval with_model_mode : t -> ( unit -> 'a ) -> 'aval push_level : t -> unitval pop_levels : t -> int -> unitmodule Debug_ : sig ... endT.FunTerm.Tbltype key = ttype !'a t = 'a T.Term.Tbl.tval create : int -> 'a tval clear : 'a t -> unitval reset : 'a t -> unitval length : 'a t -> intval stats : 'a t -> Stdlib.Hashtbl.statisticsval to_seq_values : 'a t -> 'a Stdlib.Seq.tval values : 'a t -> 'a CCHashtbl.iterval values_list : 'a t -> 'a listT.Termtype t = T.Term.tval hash : t -> intval pp : t Sidekick_core.Fmt.printertype store = T.Term.storeval as_bool : t -> bool optionmodule Tbl : sig ... endT.Tytype t = T.Ty.tval hash : t -> intval pp : t Sidekick_core.Fmt.printertype store = T.Ty.storeval is_bool : t -> boolLit.TSolver_internal.Litmodule T : sig ... endtype t = Lit.tval sign : t -> boolval atom : ?sign:bool -> T.Term.store -> T.Term.t -> tval hash : t -> intval pp : t Sidekick_core.Fmt.printerP.Step_vectype elt = proof_steptype t = P.Step_vec.tval size : t -> intval create : ?cap:int -> unit -> tval clear : t -> unitval is_empty : t -> boolval fast_remove : t -> int -> unitval ensure_size : t -> int -> unitval shrink : t -> int -> unitSolver_internal.Ptype t = prooftype proof_step = proof_steptype term = T.Term.ttype lit = Lit.ttype proof_rule = t -> proof_stepmodule Step_vec : sig ... endval enabled : t -> boolval emit_input_clause : lit Iter.t -> proof_ruleval emit_redundant_clause : lit Iter.t -> hyps:proof_step Iter.t -> proof_ruleval emit_unsat_core : lit Iter.t -> proof_ruleval emit_unsat : proof_step -> t -> unitval del_clause : proof_step -> lit Iter.t -> t -> unitval lemma_cc : lit Iter.t -> proof_ruleval define_term : term -> term -> proof_ruleval proof_p1 : proof_step -> proof_step -> proof_ruleval proof_r1 : proof_step -> proof_step -> proof_ruleval proof_res : pivot:term -> proof_step -> proof_step -> proof_ruleval with_defs : proof_step -> proof_step Iter.t -> proof_ruleval lemma_true : term -> proof_ruleval lemma_preprocess : term -> term -> using:proof_step Iter.t -> proof_ruleval lemma_rw_clause :
- proof_step ->
- res:lit Iter.t ->
- using:proof_step Iter.t ->
- proof_ruleSolver_internal.Registrytype 'a key =
- 'a Sidekick_smt_solver.Make(Solver_arg).Solver_internal.Registry.keyval create_key : unit -> 'a keyval create : unit -> tSolver_internal.Simplifyval tst : t -> term_storeval clear : t -> unittype hook = t -> term -> (term * proof_step Iter.t) optionval normalize : t -> term -> (term * proof_step) optionval normalize_t : t -> term -> term * proof_step optionT.FunTerm.Tbltype key = ttype !'a t = 'a T.Term.Tbl.tval create : int -> 'a tval clear : 'a t -> unitval reset : 'a t -> unitval length : 'a t -> intval stats : 'a t -> Stdlib.Hashtbl.statisticsval to_seq_values : 'a t -> 'a Stdlib.Seq.tval values : 'a t -> 'a CCHashtbl.iterval values_list : 'a t -> 'a listT.Termtype t = T.Term.tval hash : t -> intval pp : t Sidekick_core.Fmt.printertype store = T.Term.storeval as_bool : t -> bool optionmodule Tbl : sig ... endT.Tytype t = T.Ty.tval hash : t -> intval pp : t Sidekick_core.Fmt.printertype store = T.Ty.storeval is_bool : t -> boolSolver_internal.TS.Solver_internalmodule T : sig ... endmodule Lit : sig ... endtype ty = T.Ty.ttype term = T.Term.ttype value = T.Term.ttype term_store = T.Term.storetype ty_store = T.Ty.storetype clause_pool =
- Sidekick_smt_solver.Make(Solver_arg).Solver_internal.clause_pooltype proof = prooftype proof_step = proof_stepmodule P : sig ... endtype solver = tval tst : t -> term_storeval stats : t -> Sidekick_util.Stat.tmodule Registry : sig ... endval registry : t -> Registry.ttype theory_actions =
- Sidekick_smt_solver.Make(Solver_arg).Solver_internal.theory_actionstype lit = Lit.tmodule CC : sig ... endmodule Simplify : sig ... endtype simplify_hook = Simplify.hookval add_simplifier : t -> Simplify.hook -> unitval simplify_t : t -> term -> (term * proof_step) optionval simp_t : t -> term -> term * proof_step optionmodule type PREPROCESS_ACTS = sig ... endtype preprocess_actions = (module PREPROCESS_ACTS)type preprocess_hook = t -> preprocess_actions -> term -> unitval on_preprocess : t -> preprocess_hook -> unitval raise_conflict : t -> theory_actions -> lit list -> proof_step -> 'aval push_decision : t -> theory_actions -> lit -> unitval propagate :
- t ->
- theory_actions ->
- lit ->
- reason:( unit -> lit list * proof_step ) ->
- unitval propagate_l : t -> theory_actions -> lit -> lit list -> proof_step -> unitval add_clause_temp : t -> theory_actions -> lit list -> proof_step -> unitval add_clause_permanent :
- t ->
- theory_actions ->
- lit list ->
- proof_step ->
- unitval mk_lit : t -> theory_actions -> ?sign:bool -> term -> litval add_lit : t -> theory_actions -> ?default_pol:bool -> lit -> unitval add_lit_t : t -> theory_actions -> ?sign:bool -> term -> unitval cc_raise_conflict_expl : t -> theory_actions -> CC.Expl.t -> 'aval cc_merge : t -> theory_actions -> CC.N.t -> CC.N.t -> CC.Expl.t -> unitval cc_merge_t : t -> theory_actions -> term -> term -> CC.Expl.t -> unitval on_cc_post_merge :
- t ->
- ( CC.t -> theory_actions -> CC.N.t -> CC.N.t -> unit ) ->
- unitval on_cc_propagate :
- t ->
- ( CC.t -> lit -> ( unit -> lit list * proof_step ) -> unit ) ->
- unitval on_partial_check :
- t ->
- ( t -> theory_actions -> lit Iter.t -> unit ) ->
- unitval on_final_check : t -> ( t -> theory_actions -> lit Iter.t -> unit ) -> unitval on_th_combination :
- t ->
- ( t -> theory_actions -> (term * value) Iter.t ) ->
- unitval declare_pb_is_incomplete : t -> unitval on_model :
- ?ask:model_ask_hook ->
- ?complete:model_completion_hook ->
- t ->
- unitSolver_internal.PREPROCESS_ACTSval proof : proofval add_clause : lit list -> proof_step -> unitval add_lit : ?default_pol:bool -> lit -> unitT.FunTerm.Tbltype key = tval create : int -> 'a tval clear : 'a t -> unitval reset : 'a t -> unitval length : 'a t -> intval stats : 'a t -> Stdlib.Hashtbl.statisticsval to_seq_values : 'a t -> 'a Stdlib.Seq.tval values : 'a t -> 'a CCHashtbl.iterval values_list : 'a t -> 'a listT.Termtype t = Solver_arg.T.Term.tval hash : t -> intval pp : t Sidekick_core.Fmt.printertype store = Solver_arg.T.Term.storeval as_bool : t -> bool optionmodule Tbl : sig ... endT.Tytype t = Solver_arg.T.Ty.tval hash : t -> intval pp : t Sidekick_core.Fmt.printertype store = Solver_arg.T.Ty.storeval is_bool : t -> boolS.TS.Unknownval pp : t CCFormat.printerA.Smodule T : sig ... endmodule Lit : sig ... endtype proof = Solver_arg.prooftype proof_step = Solver_arg.proof_stepmodule P : sig ... endmodule Solver_internal : sig ... endtype solver = ttype term = T.Term.ttype ty = T.Ty.ttype lit = Lit.tmodule Registry : sig ... endval registry : t -> Registry.tmodule type THEORY = sig ... endtype theory = (module THEORY)val mk_theory :
- name:string ->
- create_and_setup:( Solver_internal.t -> 'th ) ->
- ?push_level:( 'th -> unit ) ->
- ?pop_levels:( 'th -> int -> unit ) ->
- unit ->
- theorymodule Model : sig ... endmodule Unknown : sig ... endval stats : t -> Sidekick_util.Stat.tval tst : t -> T.Term.storeval ty_st : t -> T.Ty.storeval create :
- ?stat:Sidekick_util.Stat.t ->
- ?size:[ `Big | `Small | `Tiny ] ->
- proof:proof ->
- theories:theory list ->
- T.Term.store ->
- T.Ty.store ->
- unit ->
- tval add_clause : t -> lit Sidekick_util.IArray.t -> proof_step -> unitval add_clause_l : t -> lit list -> proof_step -> unittype res = Sidekick_smt_solver.Make(Solver_arg).res = | Sat of Model.t | ||
| Unsat of {
} | ||
| Unknown of Unknown.t |
val pop_assumptions : t -> int -> unittype propagation_result =
- Sidekick_smt_solver.Make(Solver_arg).propagation_result =
- | PR_sat | |
| PR_conflict of {
} | |
| PR_unsat of {
} |
val check_sat_propagations_only :
- assumptions:lit list ->
- t ->
- propagation_resultval pp_stats : t CCFormat.printerS.THEORYval create_and_setup : Solver_internal.t -> tval push_level : t -> unitval pop_levels : t -> int -> unitA.Zval zero : tval one : tval minus_one : tval sign : t -> intval of_int : int -> tval hash : t -> intval pp : t CCFormat.printerTh_lia.Amodule S : sig ... endmodule Z : sig ... endmodule Q : sig ... endmodule LRA_solver : sig ... endtype term = S.T.Term.ttype ty = S.T.Ty.tval view_as_lia : term -> ( Z.t, Q.t, term ) Sidekick_arith_lia.lia_viewval mk_bool : S.T.Term.store -> bool -> termval mk_to_real : S.T.Term.store -> term -> termval mk_lia :
- S.T.Term.store ->
- ( Z.t, Q.t, term ) Sidekick_arith_lia.lia_view ->
- termval ty_int : S.T.Term.store -> tyval mk_eq : S.T.Term.store -> term -> term -> termval has_ty_int : term -> boolval lemma_lia : S.Lit.t Iter.t -> S.P.proof_ruleval lemma_relax_to_lra : S.Lit.t Iter.t -> S.P.proof_ruleSidekick_base_solver.Th_liamodule A : sig ... endval theory : A.S.theoryTh_lra.SimpSolvermodule V : Sidekick_simplex.VARmodule Z : Sidekick_simplex.INTmodule Q : Sidekick_simplex.RATIONAL with type bigint = Z.ttype num = Q.tNumbers
module Constraint : sig ... endmodule Subst : sig ... endval create : ?stat:Sidekick_util.Stat.t -> unit -> tCreate a new simplex.
val push_level : t -> unitval pop_levels : t -> int -> unitDefine a basic variable in terms of other variables. This is useful to "name" a linear expression and get back a variable that can be used in a Constraint.t
module Unsat_cert : sig ... endexception E_unsat of Unsat_cert.tval add_constraint :
- ?keep_on_backtracking:bool ->
?is_int:bool ->
on_propagate:ev_on_propagate ->
t ->
Constraint.t ->
V.lit ->
- unitAdd a constraint to the simplex.
This is removed upon backtracking by default.
val declare_bound : ?is_int:bool -> t -> Constraint.t -> V.lit -> unitDeclare that this constraint exists and map it to a literal, so we can possibly propagate it later. Unlike add_constraint this does NOT assert that the constraint is true
val declare_bound : ?is_int:bool -> t -> Constraint.t -> V.lit -> unitDeclare that this constraint exists and map it to a literal, so we can possibly propagate it later. Unlike add_constraint this does NOT assert that the constraint is true
Check the whole simplex for satisfiability.
Call check_exn and return a model or a proof of unsat. This does NOT enforce that integer variables map to integer values.
val check_branch_and_bound :
diff --git a/dev/sidekick-base/Sidekick_base_solver/index.html b/dev/sidekick-base/Sidekick_base_solver/index.html
index d1523ffb..c1fc4506 100644
--- a/dev/sidekick-base/Sidekick_base_solver/index.html
+++ b/dev/sidekick-base/Sidekick_base_solver/index.html
@@ -1,2 +1,2 @@
-Sidekick_base_solver (sidekick-base.Sidekick_base_solver) Module Sidekick_base_solver
SMT Solver and Theories for Sidekick_base.
This contains instances of the SMT solver, and theories, from Sidekick_core, using data structures from Sidekick_base.
module Solver_arg : sig ... endArgument to the SMT solver
module Solver : sig ... endSMT solver, obtained from Sidekick_smt_solver
module Th_data : sig ... endTheory of datatypes
module Th_bool : sig ... endReducing boolean formulas to clauses
module Gensym : sig ... endmodule Th_lra : sig ... endTheory of Linear Rational Arithmetic
module Th_lia : sig ... endval th_bool : Solver.theoryval th_data : Solver.theoryval th_lra : Solver.theoryval th_lia : Solver.theory
\ No newline at end of file
+Sidekick_base_solver (sidekick-base.Sidekick_base_solver) Module Sidekick_base_solver
SMT Solver and Theories for Sidekick_base.
This contains instances of the SMT solver, and theories, from Sidekick_core, using data structures from Sidekick_base.
module Solver_arg : sig ... endArgument to the SMT solver
module Solver : sig ... endSMT solver, obtained from Sidekick_smt_solver
module Th_data : sig ... endTheory of datatypes
module Th_bool : sig ... endReducing boolean formulas to clauses
module Gensym : sig ... endmodule Th_lra : sig ... endTheory of Linear Rational Arithmetic
val th_bool : Solver.theoryval th_data : Solver.theoryval th_lra : Solver.theory
\ No newline at end of file
diff --git a/dev/sidekick-bin/Sidekick_smtlib/Process/index.html b/dev/sidekick-bin/Sidekick_smtlib/Process/index.html
index 49b3746d..162a5b19 100644
--- a/dev/sidekick-bin/Sidekick_smtlib/Process/index.html
+++ b/dev/sidekick-bin/Sidekick_smtlib/Process/index.html
@@ -5,7 +5,7 @@
and type T.Term.store = Sidekick_base.Term.store
and type T.Ty.t = Sidekick_base.Ty.t
and type T.Ty.store = Sidekick_base.Ty.store
- and type proof = Sidekick_base.Proof.tval th_bool : Solver.theoryval th_data : Solver.theoryval th_lra : Solver.theoryval th_lia : Solver.theorymodule Check_cc : sig ... endval process_stmt :
+ and type proof = Sidekick_base.Proof.tval th_bool : Solver.theoryval th_data : Solver.theoryval th_lra : Solver.theorymodule Check_cc : sig ... endval process_stmt :
?gc:bool ->
?restarts:bool ->
?pp_cnf:bool ->
diff --git a/dev/sidekick/Sidekick_arith_lia/.dummy b/dev/sidekick/Sidekick_arith_lia/.dummy
deleted file mode 100644
index e69de29b..00000000
diff --git a/dev/sidekick/Sidekick_arith_lia/Make/argument-1-A/LRA_solver/A/Gensym/index.html b/dev/sidekick/Sidekick_arith_lia/Make/argument-1-A/LRA_solver/A/Gensym/index.html
deleted file mode 100644
index a831aaac..00000000
--- a/dev/sidekick/Sidekick_arith_lia/Make/argument-1-A/LRA_solver/A/Gensym/index.html
+++ /dev/null
@@ -1,2 +0,0 @@
-
-Gensym (sidekick.Sidekick_arith_lia.Make.1-A.LRA_solver.A.Gensym) Module A.Gensym
val create : S.T.Term.store -> tval tst : t -> S.T.Term.store
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_arith_lia/Make/argument-1-A/LRA_solver/A/Q/index.html b/dev/sidekick/Sidekick_arith_lia/Make/argument-1-A/LRA_solver/A/Q/index.html
deleted file mode 100644
index 6b344216..00000000
--- a/dev/sidekick/Sidekick_arith_lia/Make/argument-1-A/LRA_solver/A/Q/index.html
+++ /dev/null
@@ -1,2 +0,0 @@
-
-Q (sidekick.Sidekick_arith_lia.Make.1-A.LRA_solver.A.Q) Module A.Q
include Sidekick_arith.NUM with type t = Q.t
type t = Q.tval zero : tval one : tval minus_one : tval sign : t -> intval of_int : int -> tinclude Sidekick_sigs.EQ with type t := t
include Sidekick_sigs.ORD with type t := t
include Sidekick_sigs.HASH with type t := t
val hash : t -> intinclude Sidekick_sigs.PRINT with type t := t
val pp : t CCFormat.printertype bigint = Z.tval infinity : t+infinity
val minus_infinity : tval is_real : t -> boolA proper real, not nan/infinity
val is_int : t -> boolIs this a proper integer?
val pp_approx : int -> Stdlib.Format.formatter -> t -> unitPretty print rational with given amount of precision (for example as a floating point number)
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_arith_lia/Make/argument-1-A/LRA_solver/A/Z/index.html b/dev/sidekick/Sidekick_arith_lia/Make/argument-1-A/LRA_solver/A/Z/index.html
deleted file mode 100644
index b6f5cb02..00000000
--- a/dev/sidekick/Sidekick_arith_lia/Make/argument-1-A/LRA_solver/A/Z/index.html
+++ /dev/null
@@ -1,2 +0,0 @@
-
-Z (sidekick.Sidekick_arith_lia.Make.1-A.LRA_solver.A.Z) Module A.Z
include Sidekick_arith.NUM
val zero : tval one : tval minus_one : tval sign : t -> intval of_int : int -> tinclude Sidekick_sigs.EQ with type t := t
include Sidekick_sigs.ORD with type t := t
include Sidekick_sigs.HASH with type t := t
val hash : t -> intinclude Sidekick_sigs.PRINT with type t := t
val pp : t CCFormat.printer
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_arith_lia/Make/argument-1-A/LRA_solver/A/index.html b/dev/sidekick/Sidekick_arith_lia/Make/argument-1-A/LRA_solver/A/index.html
deleted file mode 100644
index f7c51918..00000000
--- a/dev/sidekick/Sidekick_arith_lia/Make/argument-1-A/LRA_solver/A/index.html
+++ /dev/null
@@ -1,5 +0,0 @@
-
-A (sidekick.Sidekick_arith_lia.Make.1-A.LRA_solver.A) Module LRA_solver.A
module S = Smodule Z : Sidekick_arith_lra.INTtype term = S.T.Term.ttype ty = S.T.Ty.tval view_as_lra : term -> ( Q.t, term ) Sidekick_arith_lra.lra_viewProject the term into the theory view
val mk_bool : S.T.Term.store -> bool -> termval mk_lra :
- S.T.Term.store ->
- ( Q.t, term ) Sidekick_arith_lra.lra_view ->
- termMake a term from the given theory view
val ty_lra : S.T.Term.store -> tyval mk_eq : S.T.Term.store -> term -> term -> termsyntactic equality
val has_ty_real : term -> boolDoes this term have the type Real
val lemma_lra : S.Lit.t Iter.t -> S.P.proof_rulemodule Gensym : sig ... end
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_arith_lia/Make/argument-1-A/LRA_solver/SimpSolver/Constraint/index.html b/dev/sidekick/Sidekick_arith_lia/Make/argument-1-A/LRA_solver/SimpSolver/Constraint/index.html
deleted file mode 100644
index ee7f2c2f..00000000
--- a/dev/sidekick/Sidekick_arith_lia/Make/argument-1-A/LRA_solver/SimpSolver/Constraint/index.html
+++ /dev/null
@@ -1,2 +0,0 @@
-
-Constraint (sidekick.Sidekick_arith_lia.Make.1-A.LRA_solver.SimpSolver.Constraint) Module SimpSolver.Constraint
type op = Sidekick_simplex.Op.tval pp : t Sidekick_util.Fmt.printer
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_arith_lia/Make/argument-1-A/LRA_solver/SimpSolver/Q/index.html b/dev/sidekick/Sidekick_arith_lia/Make/argument-1-A/LRA_solver/SimpSolver/Q/index.html
deleted file mode 100644
index 3fd92f4a..00000000
--- a/dev/sidekick/Sidekick_arith_lia/Make/argument-1-A/LRA_solver/SimpSolver/Q/index.html
+++ /dev/null
@@ -1,2 +0,0 @@
-
-Q (sidekick.Sidekick_arith_lia.Make.1-A.LRA_solver.SimpSolver.Q) Module SimpSolver.Q
include Sidekick_arith.NUM
val zero : tval one : tval minus_one : tval sign : t -> intval of_int : int -> tinclude Sidekick_sigs.EQ with type t := t
include Sidekick_sigs.ORD with type t := t
include Sidekick_sigs.HASH with type t := t
val hash : t -> intinclude Sidekick_sigs.PRINT with type t := t
val pp : t CCFormat.printertype bigint = Z.tval infinity : t+infinity
val minus_infinity : tval is_real : t -> boolA proper real, not nan/infinity
val is_int : t -> boolIs this a proper integer?
val pp_approx : int -> Stdlib.Format.formatter -> t -> unitPretty print rational with given amount of precision (for example as a floating point number)
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_arith_lia/Make/argument-1-A/LRA_solver/SimpSolver/Subst/index.html b/dev/sidekick/Sidekick_arith_lia/Make/argument-1-A/LRA_solver/SimpSolver/Subst/index.html
deleted file mode 100644
index fb9880b0..00000000
--- a/dev/sidekick/Sidekick_arith_lia/Make/argument-1-A/LRA_solver/SimpSolver/Subst/index.html
+++ /dev/null
@@ -1,2 +0,0 @@
-
-Subst (sidekick.Sidekick_arith_lia.Make.1-A.LRA_solver.SimpSolver.Subst) Module SimpSolver.Subst
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_arith_lia/Make/argument-1-A/LRA_solver/SimpSolver/Unsat_cert/index.html b/dev/sidekick/Sidekick_arith_lia/Make/argument-1-A/LRA_solver/SimpSolver/Unsat_cert/index.html
deleted file mode 100644
index 77e1ff9f..00000000
--- a/dev/sidekick/Sidekick_arith_lia/Make/argument-1-A/LRA_solver/SimpSolver/Unsat_cert/index.html
+++ /dev/null
@@ -1,2 +0,0 @@
-
-Unsat_cert (sidekick.Sidekick_arith_lia.Make.1-A.LRA_solver.SimpSolver.Unsat_cert) Module SimpSolver.Unsat_cert
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_arith_lia/Make/argument-1-A/LRA_solver/SimpSolver/V/index.html b/dev/sidekick/Sidekick_arith_lia/Make/argument-1-A/LRA_solver/SimpSolver/V/index.html
deleted file mode 100644
index 571d7c57..00000000
--- a/dev/sidekick/Sidekick_arith_lia/Make/argument-1-A/LRA_solver/SimpSolver/V/index.html
+++ /dev/null
@@ -1,2 +0,0 @@
-
-V (sidekick.Sidekick_arith_lia.Make.1-A.LRA_solver.SimpSolver.V) Module SimpSolver.V
val pp : t Sidekick_util.Fmt.printerPrinter for variables.
val pp_lit : lit Sidekick_util.Fmt.printer
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_arith_lia/Make/argument-1-A/LRA_solver/SimpSolver/Z/index.html b/dev/sidekick/Sidekick_arith_lia/Make/argument-1-A/LRA_solver/SimpSolver/Z/index.html
deleted file mode 100644
index 17640f1e..00000000
--- a/dev/sidekick/Sidekick_arith_lia/Make/argument-1-A/LRA_solver/SimpSolver/Z/index.html
+++ /dev/null
@@ -1,2 +0,0 @@
-
-Z (sidekick.Sidekick_arith_lia.Make.1-A.LRA_solver.SimpSolver.Z) Module SimpSolver.Z
include Sidekick_arith.NUM
val zero : tval one : tval minus_one : tval sign : t -> intval of_int : int -> tinclude Sidekick_sigs.EQ with type t := t
include Sidekick_sigs.ORD with type t := t
include Sidekick_sigs.HASH with type t := t
val hash : t -> intinclude Sidekick_sigs.PRINT with type t := t
val pp : t CCFormat.printer
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_arith_lia/Make/argument-1-A/LRA_solver/SimpSolver/index.html b/dev/sidekick/Sidekick_arith_lia/Make/argument-1-A/LRA_solver/SimpSolver/index.html
deleted file mode 100644
index 34096e4e..00000000
--- a/dev/sidekick/Sidekick_arith_lia/Make/argument-1-A/LRA_solver/SimpSolver/index.html
+++ /dev/null
@@ -1,16 +0,0 @@
-
-SimpSolver (sidekick.Sidekick_arith_lia.Make.1-A.LRA_solver.SimpSolver) Module LRA_solver.SimpSolver
Simplexe
module V : Sidekick_simplex.VARmodule Z : Sidekick_simplex.INTmodule Q : Sidekick_simplex.RATIONAL with type bigint = Z.ttype num = Q.tNumbers
module Constraint : sig ... endmodule Subst : sig ... endval create : ?stat:Sidekick_util.Stat.t -> unit -> tCreate a new simplex.
val push_level : t -> unitval pop_levels : t -> int -> unitDefine a basic variable in terms of other variables. This is useful to "name" a linear expression and get back a variable that can be used in a Constraint.t
module Unsat_cert : sig ... endexception E_unsat of Unsat_cert.tval add_constraint :
- ?keep_on_backtracking:bool ->
- ?is_int:bool ->
- on_propagate:ev_on_propagate ->
- t ->
- Constraint.t ->
- V.lit ->
- unitAdd a constraint to the simplex.
This is removed upon backtracking by default.
val declare_bound : ?is_int:bool -> t -> Constraint.t -> V.lit -> unitDeclare that this constraint exists and map it to a literal, so we can possibly propagate it later. Unlike add_constraint this does NOT assert that the constraint is true
Check the whole simplex for satisfiability.
Call check_exn and return a model or a proof of unsat. This does NOT enforce that integer variables map to integer values.
val check_branch_and_bound :
- on_propagate:( V.lit -> reason:V.lit list -> unit ) ->
- max_tree_nodes:int ->
- t ->
- result optionTry to solve and respect the integer constraints.
val n_vars : t -> intval n_rows : t -> int
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_arith_lia/Make/argument-1-A/LRA_solver/index.html b/dev/sidekick/Sidekick_arith_lia/Make/argument-1-A/LRA_solver/index.html
deleted file mode 100644
index 13f3f8c0..00000000
--- a/dev/sidekick/Sidekick_arith_lia/Make/argument-1-A/LRA_solver/index.html
+++ /dev/null
@@ -1,2 +0,0 @@
-
-LRA_solver (sidekick.Sidekick_arith_lia.Make.1-A.LRA_solver) Module 1-A.LRA_solver
module SimpSolver : Sidekick_simplex.SSimplexe
val create : ?stat:Sidekick_util.Stat.t -> A.S.Solver_internal.t -> stateval k_state : state A.S.Solver_internal.Registry.keyKey to access the state from outside, available when the theory has been setup
val theory : A.S.theory
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_arith_lia/Make/argument-1-A/Q/index.html b/dev/sidekick/Sidekick_arith_lia/Make/argument-1-A/Q/index.html
deleted file mode 100644
index 9bede7fd..00000000
--- a/dev/sidekick/Sidekick_arith_lia/Make/argument-1-A/Q/index.html
+++ /dev/null
@@ -1,2 +0,0 @@
-
-Q (sidekick.Sidekick_arith_lia.Make.1-A.Q) Module 1-A.Q
include Sidekick_arith.NUM
val zero : tval one : tval minus_one : tval sign : t -> intval of_int : int -> tinclude Sidekick_sigs.EQ with type t := t
include Sidekick_sigs.ORD with type t := t
include Sidekick_sigs.HASH with type t := t
val hash : t -> intinclude Sidekick_sigs.PRINT with type t := t
val pp : t CCFormat.printertype bigint = Z.tval infinity : t+infinity
val minus_infinity : tval is_real : t -> boolA proper real, not nan/infinity
val is_int : t -> boolIs this a proper integer?
val pp_approx : int -> Stdlib.Format.formatter -> t -> unitPretty print rational with given amount of precision (for example as a floating point number)
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_arith_lia/Make/argument-1-A/S/Lit/index.html b/dev/sidekick/Sidekick_arith_lia/Make/argument-1-A/S/Lit/index.html
deleted file mode 100644
index c78df551..00000000
--- a/dev/sidekick/Sidekick_arith_lia/Make/argument-1-A/S/Lit/index.html
+++ /dev/null
@@ -1,2 +0,0 @@
-
-Lit (sidekick.Sidekick_arith_lia.Make.1-A.S.Lit) Module S.Lit
module T = TLiterals depend on terms
val sign : t -> boolGet the sign. A negated literal has sign false.
val atom : ?sign:bool -> T.Term.store -> T.Term.t -> tatom store t makes a literal out of a term, possibly normalizing its sign in the process.
norm_sign (+t) is +t, true, and norm_sign (-t) is +t, false. In both cases the term is positive, and the boolean reflects the initial sign.
val hash : t -> intval pp : t Sidekick_core.Fmt.printer
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_arith_lia/Make/argument-1-A/S/Model/index.html b/dev/sidekick/Sidekick_arith_lia/Make/argument-1-A/S/Model/index.html
deleted file mode 100644
index e5f431cb..00000000
--- a/dev/sidekick/Sidekick_arith_lia/Make/argument-1-A/S/Model/index.html
+++ /dev/null
@@ -1,2 +0,0 @@
-
-Model (sidekick.Sidekick_arith_lia.Make.1-A.S.Model) Module S.Model
Models
A model can be produced when the solver is found to be in a satisfiable state after a call to solve.
val empty : tval pp : t Sidekick_core.Fmt.printer
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_arith_lia/Make/argument-1-A/S/P/Step_vec/index.html b/dev/sidekick/Sidekick_arith_lia/Make/argument-1-A/S/P/Step_vec/index.html
deleted file mode 100644
index 94050bd2..00000000
--- a/dev/sidekick/Sidekick_arith_lia/Make/argument-1-A/S/P/Step_vec/index.html
+++ /dev/null
@@ -1,2 +0,0 @@
-
-Step_vec (sidekick.Sidekick_arith_lia.Make.1-A.S.P.Step_vec) Module P.Step_vec
A vector of steps
include Sidekick_util.Vec_sig.BASE with type elt = proof_step
include Sidekick_util.Vec_sig.BASE_RO with type elt = proof_step
type elt = proof_stepval size : t -> intval create : ?cap:int -> unit -> tval clear : t -> unitval is_empty : t -> boolval fast_remove : t -> int -> unitRemove element at index i without preserving order (swap with last element)
val ensure_size : t -> int -> unitval shrink : t -> int -> unit
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_arith_lia/Make/argument-1-A/S/P/index.html b/dev/sidekick/Sidekick_arith_lia/Make/argument-1-A/S/P/index.html
deleted file mode 100644
index 5acbe804..00000000
--- a/dev/sidekick/Sidekick_arith_lia/Make/argument-1-A/S/P/index.html
+++ /dev/null
@@ -1,10 +0,0 @@
-
-P (sidekick.Sidekick_arith_lia.Make.1-A.S.P) Module S.P
type t = proofThe abstract representation of a proof. A proof always proves a clause to be valid (true in every possible interpretation of the problem's assertions, and the theories)
type proof_step = proof_stepIdentifier for a proof proof_rule (like a unique ID for a clause previously added/proved)
type term = T.Term.ttype lit = Lit.ttype proof_rule = t -> proof_stepinclude Sidekick_core.SAT_PROOF
- with type t := t
- and type lit := lit
- and type proof_step := proof_step
- and type proof_rule := proof_rule
module Step_vec : Sidekick_util.Vec_sig.S with type elt = proof_stepA vector of steps
val enabled : t -> boolReturns true if proof production is enabled
val emit_input_clause : lit Iter.t -> proof_ruleEmit an input clause.
val emit_redundant_clause : lit Iter.t -> hyps:proof_step Iter.t -> proof_ruleEmit a clause deduced by the SAT solver, redundant wrt previous clauses. The clause must be RUP wrt hyps.
val emit_unsat_core : lit Iter.t -> proof_ruleProduce a proof of the empty clause given this subset of the assumptions. FIXME: probably needs the list of proof_step that disprove the lits?
val emit_unsat : proof_step -> t -> unitSignal "unsat" result at the given proof
val del_clause : proof_step -> lit Iter.t -> t -> unitForget a clause. Only useful for performance considerations.
val lemma_cc : lit Iter.t -> proof_rulelemma_cc proof lits asserts that lits form a tautology for the theory of uninterpreted functions.
val define_term : term -> term -> proof_ruledefine_term cst u proof defines the new constant cst as being equal to u. The result is a proof of the clause cst = u
val proof_p1 : proof_step -> proof_step -> proof_ruleproof_p1 p1 p2, where p1 proves the unit clause t=u (t:bool) and p2 proves C \/ t, is the rule that produces C \/ u, i.e unit paramodulation.
val proof_r1 : proof_step -> proof_step -> proof_ruleproof_r1 p1 p2, where p1 proves the unit clause |- t (t:bool) and p2 proves C \/ ¬t, is the rule that produces C \/ u, i.e unit resolution.
val proof_res : pivot:term -> proof_step -> proof_step -> proof_ruleproof_res ~pivot p1 p2, where p1 proves the clause |- C \/ l and p2 proves D \/ ¬l, where l is either pivot or ¬pivot, is the rule that produces C \/ D, i.e boolean resolution.
val with_defs : proof_step -> proof_step Iter.t -> proof_rulewith_defs pr defs specifies that pr is valid only in a context where the definitions defs are present.
val lemma_true : term -> proof_rulelemma_true (true) p asserts the clause (true)
val lemma_preprocess : term -> term -> using:proof_step Iter.t -> proof_rulelemma_preprocess t u ~using p asserts that t = u is a tautology and that t has been preprocessed into u.
The theorem /\_{eqn in using} eqn |- t=u is proved using congruence closure, and then resolved against the clauses using to obtain a unit equality.
From now on, t and u will be used interchangeably.
val lemma_rw_clause :
- proof_step ->
- res:lit Iter.t ->
- using:proof_step Iter.t ->
- proof_rulelemma_rw_clause prc ~res ~using, where prc is the proof of |- c, uses the equations |- p_i = q_i from using to rewrite some literals of c into res. This is used to preprocess literals of a clause (using lemma_preprocess individually).
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_arith_lia/Make/argument-1-A/S/Registry/index.html b/dev/sidekick/Sidekick_arith_lia/Make/argument-1-A/S/Registry/index.html
deleted file mode 100644
index ee528a4e..00000000
--- a/dev/sidekick/Sidekick_arith_lia/Make/argument-1-A/S/Registry/index.html
+++ /dev/null
@@ -1,2 +0,0 @@
-
-Registry (sidekick.Sidekick_arith_lia.Make.1-A.S.Registry) Module S.Registry
val create_key : unit -> 'a keyCall this statically, typically at program initialization, for each distinct key.
val create : unit -> t
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_arith_lia/Make/argument-1-A/S/Solver_internal/CC/Actions/P/Step_vec/index.html b/dev/sidekick/Sidekick_arith_lia/Make/argument-1-A/S/Solver_internal/CC/Actions/P/Step_vec/index.html
deleted file mode 100644
index fe9945a9..00000000
--- a/dev/sidekick/Sidekick_arith_lia/Make/argument-1-A/S/Solver_internal/CC/Actions/P/Step_vec/index.html
+++ /dev/null
@@ -1,2 +0,0 @@
-
-Step_vec (sidekick.Sidekick_arith_lia.Make.1-A.S.Solver_internal.CC.Actions.P.Step_vec) Module P.Step_vec
A vector of steps
include Sidekick_util.Vec_sig.BASE with type elt = proof_step
include Sidekick_util.Vec_sig.BASE_RO with type elt = proof_step
type elt = proof_stepval size : t -> intval create : ?cap:int -> unit -> tval clear : t -> unitval is_empty : t -> boolval fast_remove : t -> int -> unitRemove element at index i without preserving order (swap with last element)
val ensure_size : t -> int -> unitval shrink : t -> int -> unit
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_arith_lia/Make/argument-1-A/S/Solver_internal/CC/Actions/P/index.html b/dev/sidekick/Sidekick_arith_lia/Make/argument-1-A/S/Solver_internal/CC/Actions/P/index.html
deleted file mode 100644
index 5b69903c..00000000
--- a/dev/sidekick/Sidekick_arith_lia/Make/argument-1-A/S/Solver_internal/CC/Actions/P/index.html
+++ /dev/null
@@ -1,10 +0,0 @@
-
-P (sidekick.Sidekick_arith_lia.Make.1-A.S.Solver_internal.CC.Actions.P) Module Actions.P
type t = proofThe abstract representation of a proof. A proof always proves a clause to be valid (true in every possible interpretation of the problem's assertions, and the theories)
type proof_step = proof_stepIdentifier for a proof proof_rule (like a unique ID for a clause previously added/proved)
type term = T.Term.ttype lit = Lit.ttype proof_rule = t -> proof_stepinclude Sidekick_core.SAT_PROOF
- with type t := t
- and type lit := lit
- and type proof_step := proof_step
- and type proof_rule := proof_rule
module Step_vec : Sidekick_util.Vec_sig.S with type elt = proof_stepA vector of steps
val enabled : t -> boolReturns true if proof production is enabled
val emit_input_clause : lit Iter.t -> proof_ruleEmit an input clause.
val emit_redundant_clause : lit Iter.t -> hyps:proof_step Iter.t -> proof_ruleEmit a clause deduced by the SAT solver, redundant wrt previous clauses. The clause must be RUP wrt hyps.
val emit_unsat_core : lit Iter.t -> proof_ruleProduce a proof of the empty clause given this subset of the assumptions. FIXME: probably needs the list of proof_step that disprove the lits?
val emit_unsat : proof_step -> t -> unitSignal "unsat" result at the given proof
val del_clause : proof_step -> lit Iter.t -> t -> unitForget a clause. Only useful for performance considerations.
val lemma_cc : lit Iter.t -> proof_rulelemma_cc proof lits asserts that lits form a tautology for the theory of uninterpreted functions.
val define_term : term -> term -> proof_ruledefine_term cst u proof defines the new constant cst as being equal to u. The result is a proof of the clause cst = u
val proof_p1 : proof_step -> proof_step -> proof_ruleproof_p1 p1 p2, where p1 proves the unit clause t=u (t:bool) and p2 proves C \/ t, is the rule that produces C \/ u, i.e unit paramodulation.
val proof_r1 : proof_step -> proof_step -> proof_ruleproof_r1 p1 p2, where p1 proves the unit clause |- t (t:bool) and p2 proves C \/ ¬t, is the rule that produces C \/ u, i.e unit resolution.
val proof_res : pivot:term -> proof_step -> proof_step -> proof_ruleproof_res ~pivot p1 p2, where p1 proves the clause |- C \/ l and p2 proves D \/ ¬l, where l is either pivot or ¬pivot, is the rule that produces C \/ D, i.e boolean resolution.
val with_defs : proof_step -> proof_step Iter.t -> proof_rulewith_defs pr defs specifies that pr is valid only in a context where the definitions defs are present.
val lemma_true : term -> proof_rulelemma_true (true) p asserts the clause (true)
val lemma_preprocess : term -> term -> using:proof_step Iter.t -> proof_rulelemma_preprocess t u ~using p asserts that t = u is a tautology and that t has been preprocessed into u.
The theorem /\_{eqn in using} eqn |- t=u is proved using congruence closure, and then resolved against the clauses using to obtain a unit equality.
From now on, t and u will be used interchangeably.
val lemma_rw_clause :
- proof_step ->
- res:lit Iter.t ->
- using:proof_step Iter.t ->
- proof_rulelemma_rw_clause prc ~res ~using, where prc is the proof of |- c, uses the equations |- p_i = q_i from using to rewrite some literals of c into res. This is used to preprocess literals of a clause (using lemma_preprocess individually).
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_arith_lia/Make/argument-1-A/S/Solver_internal/CC/Actions/index.html b/dev/sidekick/Sidekick_arith_lia/Make/argument-1-A/S/Solver_internal/CC/Actions/index.html
deleted file mode 100644
index 1cdac9aa..00000000
--- a/dev/sidekick/Sidekick_arith_lia/Make/argument-1-A/S/Solver_internal/CC/Actions/index.html
+++ /dev/null
@@ -1,15 +0,0 @@
-
-Actions (sidekick.Sidekick_arith_lia.Make.1-A.S.Solver_internal.CC.Actions) Module CC.Actions
module T = Tmodule Lit = Littype proof = prooftype proof_step = proof_stepmodule P :
- Sidekick_core.PROOF
- with type lit = Lit.t
- and type t = proof
- and type term = T.Term.t
- and type proof_step = proof_steptype t = theory_actionsAn action handle. It is used by the congruence closure to perform the actions below. How it performs the actions is not specified and is solver-specific.
val raise_conflict : t -> Lit.t list -> proof_step -> 'araise_conflict acts c pr declares that c is a tautology of the theory of congruence. This does not return (it should raise an exception).
raise_semantic_conflict acts lits same_val declares that the conjunction of all lits (literals true in current trail) and tuples {=,≠}, t_i, u_i implies false.
The {=,≠}, t_i, u_i are pairs of terms with the same value (if = / true) or distinct value (if ≠ / false)) in the current model.
This does not return. It should raise an exception.
val propagate :
- t ->
- Lit.t ->
- reason:( unit -> Lit.t list * proof_step ) ->
- unitpropagate acts lit ~reason pr declares that reason() => lit is a tautology.
reason() should return a list of literals that are currently true.lit should be a literal of interest (see CC_S.set_as_lit).
This function might never be called, a congruence closure has the right to not propagate and only trigger conflicts.
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_arith_lia/Make/argument-1-A/S/Solver_internal/CC/Expl/index.html b/dev/sidekick/Sidekick_arith_lia/Make/argument-1-A/S/Solver_internal/CC/Expl/index.html
deleted file mode 100644
index 5622b259..00000000
--- a/dev/sidekick/Sidekick_arith_lia/Make/argument-1-A/S/Solver_internal/CC/Expl/index.html
+++ /dev/null
@@ -1,2 +0,0 @@
-
-Expl (sidekick.Sidekick_arith_lia.Make.1-A.S.Solver_internal.CC.Expl) Module CC.Expl
Explanations
Explanations are specialized proofs, created by the congruence closure when asked to justify why 2 terms are equal.
val pp : t Sidekick_core.Fmt.printerExplanation: we merged t and u because of literal t=u, or we merged t and true because of literal t, or t and false because of literal ¬t
mk_theory t u expl_sets pr builds a theory explanation for why |- t=u. It depends on sub-explanations expl_sets which are tuples (t_i, u_i, expls_i) where expls_i are explanations that justify t_i = u_i in the current congruence closure.
The proof pr is the theory lemma, of the form (t_i = u_i)_i |- t=u . It is resolved against each expls_i |- t_i=u_i obtained from expl_sets, on pivot t_i=u_i, to obtain a proof of Gamma |- t=u where Gamma is a subset of the literals asserted into the congruence closure.
For example for the lemma a=b deduced by injectivity from Some a=Some b in the theory of datatypes, the arguments would be a, b, [Some a, Some b, mk_merge_t (Some a)(Some b)], pr where pr is the injectivity lemma Some a=Some b |- a=b.
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_arith_lia/Make/argument-1-A/S/Solver_internal/CC/N/index.html b/dev/sidekick/Sidekick_arith_lia/Make/argument-1-A/S/Solver_internal/CC/N/index.html
deleted file mode 100644
index b02107b0..00000000
--- a/dev/sidekick/Sidekick_arith_lia/Make/argument-1-A/S/Solver_internal/CC/N/index.html
+++ /dev/null
@@ -1,2 +0,0 @@
-
-N (sidekick.Sidekick_arith_lia.Make.1-A.S.Solver_internal.CC.N) Module CC.N
Equivalence classes.
An equivalence class is a set of terms that are currently equal in the partial model built by the solver. The class is represented by a collection of nodes, one of which is distinguished and is called the "representative".
All information pertaining to the whole equivalence class is stored in this representative's node.
When two classes become equal (are "merged"), one of the two representatives is picked as the representative of the new class. The new class contains the union of the two old classes' nodes.
We also allow theories to store additional information in the representative. This information can be used when two classes are merged, to detect conflicts and solve equations à la Shostak.
An equivalent class, containing terms that are proved to be equal.
A value of type t points to a particular term, but see find to get the representative of the class.
Term contained in this equivalence class. If is_root n, then term n is the class' representative term.
Are two classes physically equal? To check for logical equality, use CC.N.equal (CC.find cc n1) (CC.find cc n2) which checks for equality of representatives.
val hash : t -> intAn opaque hash of this node.
val pp : t Sidekick_core.Fmt.printerUnspecified printing of the node, for example its term, a unique ID, etc.
val is_root : t -> boolIs the node a root (ie the representative of its class)? See find to get the root.
Traverse the congruence class. Precondition: is_root n (see find below)
Traverse the parents of the class. Precondition: is_root n (see find below)
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_arith_lia/Make/argument-1-A/S/Solver_internal/CC/P/Step_vec/index.html b/dev/sidekick/Sidekick_arith_lia/Make/argument-1-A/S/Solver_internal/CC/P/Step_vec/index.html
deleted file mode 100644
index 954f6ea7..00000000
--- a/dev/sidekick/Sidekick_arith_lia/Make/argument-1-A/S/Solver_internal/CC/P/Step_vec/index.html
+++ /dev/null
@@ -1,2 +0,0 @@
-
-Step_vec (sidekick.Sidekick_arith_lia.Make.1-A.S.Solver_internal.CC.P.Step_vec) Module P.Step_vec
A vector of steps
include Sidekick_util.Vec_sig.BASE with type elt = proof_step
include Sidekick_util.Vec_sig.BASE_RO with type elt = proof_step
type elt = proof_stepval size : t -> intval create : ?cap:int -> unit -> tval clear : t -> unitval is_empty : t -> boolval fast_remove : t -> int -> unitRemove element at index i without preserving order (swap with last element)
val ensure_size : t -> int -> unitval shrink : t -> int -> unit
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_arith_lia/Make/argument-1-A/S/Solver_internal/CC/P/index.html b/dev/sidekick/Sidekick_arith_lia/Make/argument-1-A/S/Solver_internal/CC/P/index.html
deleted file mode 100644
index 1ac0e9f7..00000000
--- a/dev/sidekick/Sidekick_arith_lia/Make/argument-1-A/S/Solver_internal/CC/P/index.html
+++ /dev/null
@@ -1,10 +0,0 @@
-
-P (sidekick.Sidekick_arith_lia.Make.1-A.S.Solver_internal.CC.P) Module CC.P
type t = proofThe abstract representation of a proof. A proof always proves a clause to be valid (true in every possible interpretation of the problem's assertions, and the theories)
type proof_step = proof_stepIdentifier for a proof proof_rule (like a unique ID for a clause previously added/proved)
type lit = littype proof_rule = t -> proof_stepinclude Sidekick_core.SAT_PROOF
- with type t := t
- and type lit := lit
- and type proof_step := proof_step
- and type proof_rule := proof_rule
module Step_vec : Sidekick_util.Vec_sig.S with type elt = proof_stepA vector of steps
val enabled : t -> boolReturns true if proof production is enabled
val emit_input_clause : lit Iter.t -> proof_ruleEmit an input clause.
val emit_redundant_clause : lit Iter.t -> hyps:proof_step Iter.t -> proof_ruleEmit a clause deduced by the SAT solver, redundant wrt previous clauses. The clause must be RUP wrt hyps.
val emit_unsat_core : lit Iter.t -> proof_ruleProduce a proof of the empty clause given this subset of the assumptions. FIXME: probably needs the list of proof_step that disprove the lits?
val emit_unsat : proof_step -> t -> unitSignal "unsat" result at the given proof
val del_clause : proof_step -> lit Iter.t -> t -> unitForget a clause. Only useful for performance considerations.
val lemma_cc : lit Iter.t -> proof_rulelemma_cc proof lits asserts that lits form a tautology for the theory of uninterpreted functions.
val define_term : term -> term -> proof_ruledefine_term cst u proof defines the new constant cst as being equal to u. The result is a proof of the clause cst = u
val proof_p1 : proof_step -> proof_step -> proof_ruleproof_p1 p1 p2, where p1 proves the unit clause t=u (t:bool) and p2 proves C \/ t, is the rule that produces C \/ u, i.e unit paramodulation.
val proof_r1 : proof_step -> proof_step -> proof_ruleproof_r1 p1 p2, where p1 proves the unit clause |- t (t:bool) and p2 proves C \/ ¬t, is the rule that produces C \/ u, i.e unit resolution.
val proof_res : pivot:term -> proof_step -> proof_step -> proof_ruleproof_res ~pivot p1 p2, where p1 proves the clause |- C \/ l and p2 proves D \/ ¬l, where l is either pivot or ¬pivot, is the rule that produces C \/ D, i.e boolean resolution.
val with_defs : proof_step -> proof_step Iter.t -> proof_rulewith_defs pr defs specifies that pr is valid only in a context where the definitions defs are present.
val lemma_true : term -> proof_rulelemma_true (true) p asserts the clause (true)
val lemma_preprocess : term -> term -> using:proof_step Iter.t -> proof_rulelemma_preprocess t u ~using p asserts that t = u is a tautology and that t has been preprocessed into u.
The theorem /\_{eqn in using} eqn |- t=u is proved using congruence closure, and then resolved against the clauses using to obtain a unit equality.
From now on, t and u will be used interchangeably.
val lemma_rw_clause :
- proof_step ->
- res:lit Iter.t ->
- using:proof_step Iter.t ->
- proof_rulelemma_rw_clause prc ~res ~using, where prc is the proof of |- c, uses the equations |- p_i = q_i from using to rewrite some literals of c into res. This is used to preprocess literals of a clause (using lemma_preprocess individually).
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_arith_lia/Make/argument-1-A/S/Solver_internal/CC/Resolved_expl/index.html b/dev/sidekick/Sidekick_arith_lia/Make/argument-1-A/S/Solver_internal/CC/Resolved_expl/index.html
deleted file mode 100644
index 68298a0f..00000000
--- a/dev/sidekick/Sidekick_arith_lia/Make/argument-1-A/S/Solver_internal/CC/Resolved_expl/index.html
+++ /dev/null
@@ -1,2 +0,0 @@
-
-Resolved_expl (sidekick.Sidekick_arith_lia.Make.1-A.S.Solver_internal.CC.Resolved_expl) Module CC.Resolved_expl
Resolved explanations.
The congruence closure keeps explanations for why terms are in the same class. However these are represented in a compact, cheap form. To use these explanations we need to resolve them into a resolved explanation, typically a list of literals that are true in the current trail and are responsible for merges.
However, we can also have merged classes because they have the same value in the current model.
val is_semantic : t -> boolis_semantic expl is true if there's at least one pair in expl.same_value.
val pp : t Sidekick_core.Fmt.printer
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_arith_lia/Make/argument-1-A/S/Solver_internal/CC/index.html b/dev/sidekick/Sidekick_arith_lia/Make/argument-1-A/S/Solver_internal/CC/index.html
deleted file mode 100644
index dcb649f7..00000000
--- a/dev/sidekick/Sidekick_arith_lia/Make/argument-1-A/S/Solver_internal/CC/index.html
+++ /dev/null
@@ -1,25 +0,0 @@
-
-CC (sidekick.Sidekick_arith_lia.Make.1-A.S.Solver_internal.CC) Module Solver_internal.CC
Congruence closure instance
first, some aliases.
module T = Tmodule Lit = Littype proof = prooftype proof_step = proof_stepmodule P :
- Sidekick_core.PROOF
- with type lit = Lit.t
- and type t = proof
- and type proof_step = proof_step
- with type t = proof
- with type lit = litmodule Actions :
- Sidekick_core.CC_ACTIONS
- with module T = T
- and module Lit = Lit
- and type proof = proof
- and type proof_step = proof_step
- with type t = theory_actionstype term_store = T.Term.storetype term = T.Term.ttype value = termtype fun_ = T.Fun.ttype lit = Lit.ttype actions = Actions.tThe congruence closure object. It contains a fair amount of state and is mutable and backtrackable.
module N : sig ... endEquivalence classes.
module Expl : sig ... endExplanations
module Resolved_expl : sig ... endResolved explanations.
type node = N.tA node of the congruence closure
type repr = N.tNode that is currently a representative
type explanation = Expl.tAccessors
val term_store : t -> term_storeAdd the term to the congruence closure, if not present already. Will be backtracked.
Returns true if the term is explicitly present in the congruence closure
Events
Events triggered by the congruence closure, to which other plugins can subscribe.
ev_on_pre_merge cc acts n1 n2 expl is called right before n1 and n2 are merged with explanation expl.
ev_on_post_merge cc acts n1 n2 is called right after n1 and n2 were merged. find cc n1 and find cc n2 will return the same node.
ev_on_new_term cc n t is called whenever a new term t is added to the congruence closure. Its node is n.
ev_on_conflict acts ~th c is called when the congruence closure triggers a conflict by asserting the tautology c.
type ev_on_propagate = t -> lit -> ( unit -> lit list * proof_step ) -> unitev_on_propagate cc lit reason is called whenever reason() => lit is a propagated lemma. See CC_ACTIONS.propagate.
ev_on_is_subterm n t is called when n is a subterm of another node for the first time. t is the term corresponding to the node n. This can be useful for theory combination.
val create :
- ?stat:Sidekick_util.Stat.t ->
- ?on_pre_merge:ev_on_pre_merge list ->
- ?on_post_merge:ev_on_post_merge list ->
- ?on_new_term:ev_on_new_term list ->
- ?on_conflict:ev_on_conflict list ->
- ?on_propagate:ev_on_propagate list ->
- ?on_is_subterm:ev_on_is_subterm list ->
- ?size:[ `Small | `Big ] ->
- term_store ->
- proof ->
- tCreate a new congruence closure.
val allocate_bitfield : descr:string -> t -> N.bitfieldAllocate a new node field (see N.bitfield).
This field descriptor is henceforth reserved for all nodes in this congruence closure, and can be set using set_bitfield for each node individually. This can be used to efficiently store some metadata on nodes (e.g. "is there a numeric value in the class" or "is there a constructor term in the class").
There may be restrictions on how many distinct fields are allocated for a given congruence closure (e.g. at most Sys.int_size fields).
val get_bitfield : t -> N.bitfield -> N.t -> boolAccess the bit field of the given node
val set_bitfield : t -> N.bitfield -> bool -> N.t -> unitSet the bitfield for the node. This will be backtracked. See N.bitfield.
val on_pre_merge : t -> ev_on_pre_merge -> unitAdd a function to be called when two classes are merged
val on_post_merge : t -> ev_on_post_merge -> unitAdd a function to be called when two classes are merged
val on_new_term : t -> ev_on_new_term -> unitAdd a function to be called when a new node is created
val on_conflict : t -> ev_on_conflict -> unitCalled when the congruence closure finds a conflict
val on_propagate : t -> ev_on_propagate -> unitCalled when the congruence closure propagates a literal
val on_is_subterm : t -> ev_on_is_subterm -> unitCalled on terms that are subterms of function symbols
All current classes. This is costly, only use if there is no other solution
Given a literal, assume it in the congruence closure and propagate its consequences. Will be backtracked.
Useful for the theory combination or the SAT solver's functor
val explain_eq : t -> N.t -> N.t -> Resolved_expl.tExplain why the two nodes are equal. Fails if they are not, in an unspecified way.
Raise a conflict with the given explanation. It must be a theory tautology that expl ==> absurd. To be used in theories.
This fails in an unspecified way if the explanation, once resolved, satisfies Resolved_expl.is_semantic.
Merge these two nodes given this explanation. It must be a theory tautology that expl ==> n1 = n2. To be used in theories.
val with_model_mode : t -> ( unit -> 'a ) -> 'aEnter model combination mode.
In model combination mode, obtain classes with their values.
Perform all pending operations done via assert_eq, assert_lit, etc. Will use the actions to propagate literals, declare conflicts, etc.
val push_level : t -> unitPush backtracking level
val pop_levels : t -> int -> unitRestore to state n calls to push_level earlier. Used during backtracking.
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_arith_lia/Make/argument-1-A/S/Solver_internal/Registry/index.html b/dev/sidekick/Sidekick_arith_lia/Make/argument-1-A/S/Solver_internal/Registry/index.html
deleted file mode 100644
index 1550abe5..00000000
--- a/dev/sidekick/Sidekick_arith_lia/Make/argument-1-A/S/Solver_internal/Registry/index.html
+++ /dev/null
@@ -1,2 +0,0 @@
-
-Registry (sidekick.Sidekick_arith_lia.Make.1-A.S.Solver_internal.Registry) Module Solver_internal.Registry
val create_key : unit -> 'a keyCall this statically, typically at program initialization, for each distinct key.
val create : unit -> t
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_arith_lia/Make/argument-1-A/S/Solver_internal/Simplify/index.html b/dev/sidekick/Sidekick_arith_lia/Make/argument-1-A/S/Solver_internal/Simplify/index.html
deleted file mode 100644
index 6707bdbc..00000000
--- a/dev/sidekick/Sidekick_arith_lia/Make/argument-1-A/S/Solver_internal/Simplify/index.html
+++ /dev/null
@@ -1,2 +0,0 @@
-
-Simplify (sidekick.Sidekick_arith_lia.Make.1-A.S.Solver_internal.Simplify) Module Solver_internal.Simplify
Simplify terms
val tst : t -> term_storeval clear : t -> unitReset internal cache, etc.
type hook = t -> term -> (term * proof_step Iter.t) optionGiven a term, try to simplify it. Return None if it didn't change.
A simple example could be a hook that takes a term t, and if t is app "+" (const x) (const y) where x and y are number, returns Some (const (x+y)), and None otherwise.
The simplifier will take care of simplifying the resulting term further, caching (so that work is not duplicated in subterms), etc.
val normalize : t -> term -> (term * proof_step) optionNormalize a term using all the hooks. This performs a fixpoint, i.e. it only stops when no hook applies anywhere inside the term.
val normalize_t : t -> term -> term * proof_step optionNormalize a term using all the hooks, along with a proof that the simplification is correct. returns t, ø if no simplification occurred.
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_arith_lia/Make/argument-1-A/S/Solver_internal/index.html b/dev/sidekick/Sidekick_arith_lia/Make/argument-1-A/S/Solver_internal/index.html
deleted file mode 100644
index 904b61cb..00000000
--- a/dev/sidekick/Sidekick_arith_lia/Make/argument-1-A/S/Solver_internal/index.html
+++ /dev/null
@@ -1,43 +0,0 @@
-
-Solver_internal (sidekick.Sidekick_arith_lia.Make.1-A.S.Solver_internal) Module S.Solver_internal
Internal solver, available to theories.
module T = Tmodule Lit = Littype ty = T.Ty.ttype term = T.Term.ttype value = T.Term.ttype term_store = T.Term.storetype ty_store = T.Ty.storetype proof = prooftype proof_step = proof_stepmodule P = Ptype solver = tval tst : t -> term_storeval stats : t -> Sidekick_util.Stat.tRegistry
module Registry : Sidekick_core.REGISTRYval registry : t -> Registry.tA solver contains a registry so that theories can share data
Actions for the theories
type lit = Lit.tCongruence Closure
module CC :
- Sidekick_core.CC_S
- with module T = T
- and module Lit = Lit
- and type proof = proof
- and type proof_step = proof_step
- and type P.t = proof
- and type P.lit = lit
- and type Actions.t = theory_actionsCongruence closure instance
Simplifiers
module Simplify : sig ... endSimplify terms
type simplify_hook = Simplify.hookval add_simplifier : t -> Simplify.hook -> unitAdd a simplifier hook for preprocessing.
val simplify_t : t -> term -> (term * proof_step) optionSimplify input term, returns Some u if some simplification occurred.
val simp_t : t -> term -> term * proof_step optionsimp_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.
module type PREPROCESS_ACTS = sig ... endtype preprocess_actions = (module PREPROCESS_ACTS)Actions available to the preprocessor
type preprocess_hook = t -> preprocess_actions -> term -> unitGiven a term, preprocess it.
The idea is to add literals and clauses to help define the meaning of the term, if needed. For example for boolean formulas, clauses for their Tseitin encoding can be added, with the formula acting as its own proxy symbol.
val on_preprocess : t -> preprocess_hook -> unitAdd a hook that will be called when terms are preprocessed
hooks for the theory
val raise_conflict : t -> theory_actions -> lit list -> proof_step -> 'aGive a conflict clause to the solver
val push_decision : t -> theory_actions -> lit -> unitAsk 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.
val propagate :
- t ->
- theory_actions ->
- lit ->
- reason:( unit -> lit list * proof_step ) ->
- unitPropagate a boolean using a unit clause. expl => lit must be a theory lemma, that is, a T-tautology
val propagate_l : t -> theory_actions -> lit -> lit list -> proof_step -> unitPropagate a boolean using a unit clause. expl => lit must be a theory lemma, that is, a T-tautology
val add_clause_temp : t -> theory_actions -> lit list -> proof_step -> unitAdd local clause to the SAT solver. This clause will be removed when the solver backtracks.
val add_clause_permanent :
- t ->
- theory_actions ->
- lit list ->
- proof_step ->
- unitAdd toplevel clause to the SAT solver. This clause will not be backtracked.
val mk_lit : t -> theory_actions -> ?sign:bool -> term -> litCreate a literal. This automatically preprocesses the term.
val add_lit : t -> theory_actions -> ?default_pol:bool -> lit -> unitAdd the given literal to the SAT solver, so it gets assigned a boolean value.
val add_lit_t : t -> theory_actions -> ?sign:bool -> term -> unitAdd the given (signed) bool term to the SAT solver, so it gets assigned a boolean value
val cc_raise_conflict_expl : t -> theory_actions -> CC.Expl.t -> 'aRaise a conflict with the given congruence closure explanation. it must be a theory tautology that expl ==> absurd. To be used in theories.
val cc_merge : t -> theory_actions -> CC.N.t -> CC.N.t -> CC.Expl.t -> unitMerge these two nodes in the congruence closure, given this explanation. It must be a theory tautology that expl ==> n1 = n2. To be used in theories.
val cc_merge_t : t -> theory_actions -> term -> term -> CC.Expl.t -> unitMerge these two terms in the congruence closure, given this explanation. See cc_merge
Add/retrieve congruence closure node for this term. To be used in theories
Return true if the term is explicitly in the congruence closure. To be used in theories
val on_cc_pre_merge :
- t ->
- ( CC.t -> theory_actions -> CC.N.t -> CC.N.t -> CC.Expl.t -> unit ) ->
- unitCallback for when two classes containing data for this key are merged (called before)
val on_cc_post_merge :
- t ->
- ( CC.t -> theory_actions -> CC.N.t -> CC.N.t -> unit ) ->
- unitCallback for when two classes containing data for this key are merged (called after)
Callback to add data on terms when they are added to the congruence closure
Callback for when a term is a subterm of another term in the congruence closure
Callback called on every CC conflict
val on_cc_propagate :
- t ->
- ( CC.t -> lit -> ( unit -> lit list * proof_step ) -> unit ) ->
- unitCallback called on every CC propagation
val on_partial_check :
- t ->
- ( t -> theory_actions -> lit Iter.t -> unit ) ->
- unitRegister 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.
val on_final_check : t -> ( t -> theory_actions -> lit Iter.t -> unit ) -> unitRegister callback to be called during the final check.
Must be complete (i.e. must raise a conflict if the set of literals is not satisfiable) and can be expensive. The function is given the whole trail.
val on_th_combination :
- t ->
- ( t -> theory_actions -> (term * value) Iter.t ) ->
- unitAdd a hook called during theory combination. The hook must return an iterator of pairs (t, v) which mean that term t has value v in the model.
Terms with the same value (according to Term.equal) will be merged in the CC; if two terms with different values are merged, we get a semantic conflict and must pick another model.
val declare_pb_is_incomplete : t -> unitDeclare that, in some theory, the problem is outside the logic fragment that is decidable (e.g. if we meet proper NIA formulas). The solver will not reply "SAT" from now on.
Model production
A model-production hook to query values from a theory.
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.
A model production hook, for the theory to add values. The hook is given a add function to add bindings to the model.
val on_model :
- ?ask:model_ask_hook ->
- ?complete:model_completion_hook ->
- t ->
- unitAdd model production/completion hooks.
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_arith_lia/Make/argument-1-A/S/Solver_internal/module-type-PREPROCESS_ACTS/index.html b/dev/sidekick/Sidekick_arith_lia/Make/argument-1-A/S/Solver_internal/module-type-PREPROCESS_ACTS/index.html
deleted file mode 100644
index 3b442f06..00000000
--- a/dev/sidekick/Sidekick_arith_lia/Make/argument-1-A/S/Solver_internal/module-type-PREPROCESS_ACTS/index.html
+++ /dev/null
@@ -1,2 +0,0 @@
-
-PREPROCESS_ACTS (sidekick.Sidekick_arith_lia.Make.1-A.S.Solver_internal.PREPROCESS_ACTS) Module type Solver_internal.PREPROCESS_ACTS
val proof : proofval add_clause : lit list -> proof_step -> unitpushes a new clause into the SAT solver.
val add_lit : ?default_pol:bool -> lit -> unitEnsure the literal will be decided/handled by the SAT solver.
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_arith_lia/Make/argument-1-A/S/T/Fun/index.html b/dev/sidekick/Sidekick_arith_lia/Make/argument-1-A/S/T/Fun/index.html
deleted file mode 100644
index fd073028..00000000
--- a/dev/sidekick/Sidekick_arith_lia/Make/argument-1-A/S/T/Fun/index.html
+++ /dev/null
@@ -1,2 +0,0 @@
-
-Fun (sidekick.Sidekick_arith_lia.Make.1-A.S.T.Fun) Module T.Fun
A function symbol, like "f" or "plus" or "is_human" or "socrates"
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_arith_lia/Make/argument-1-A/S/T/Term/index.html b/dev/sidekick/Sidekick_arith_lia/Make/argument-1-A/S/T/Term/index.html
deleted file mode 100644
index d13968eb..00000000
--- a/dev/sidekick/Sidekick_arith_lia/Make/argument-1-A/S/T/Term/index.html
+++ /dev/null
@@ -1,8 +0,0 @@
-
-Term (sidekick.Sidekick_arith_lia.Make.1-A.S.T.Term) Module T.Term
Term structure.
Terms should be hashconsed, with perfect sharing. This allows, for example, Term.Tbl and Term.iter_dag to be efficient.
val hash : t -> intval pp : t Sidekick_core.Fmt.printerA store used to create new terms. It is where the hashconsing table should live, along with other all-terms related store.
val as_bool : t -> bool optionas_bool t is Some true if t is the term true, and similarly for false. For other terms it is None.
abs t returns an "absolute value" for the term, along with the sign of t.
The idea is that we want to turn not a into (a, false), or (a != b) into (a=b, false). For terms without a negation this should return (t, true).
The store is passed in case a new term needs to be created.
Map function on immediate subterms. This should not be recursive.
Iterate function on immediate subterms. This should not be recursive.
iter_dag t f calls f once on each subterm of t, t included. It must not traverse t as a tree, but rather as a perfectly shared DAG.
For example, in:
let x = 2 in
-let y = f x x in
-let z = g y x in
-z = z
the DAG has the following nodes:
n1: 2
-n2: f n1 n1
-n3: g n2 n1
-n4: = n3 n3
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_arith_lia/Make/argument-1-A/S/T/Ty/index.html b/dev/sidekick/Sidekick_arith_lia/Make/argument-1-A/S/T/Ty/index.html
deleted file mode 100644
index 5cde388d..00000000
--- a/dev/sidekick/Sidekick_arith_lia/Make/argument-1-A/S/T/Ty/index.html
+++ /dev/null
@@ -1,2 +0,0 @@
-
-Ty (sidekick.Sidekick_arith_lia.Make.1-A.S.T.Ty) Module T.Ty
Types
Types should be comparable (ideally, in O(1)), and have at least a boolean type available.
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_arith_lia/Make/argument-1-A/S/T/index.html b/dev/sidekick/Sidekick_arith_lia/Make/argument-1-A/S/T/index.html
deleted file mode 100644
index 53794bbf..00000000
--- a/dev/sidekick/Sidekick_arith_lia/Make/argument-1-A/S/T/index.html
+++ /dev/null
@@ -1,2 +0,0 @@
-
-T (sidekick.Sidekick_arith_lia.Make.1-A.S.T) Module S.T
module Fun : sig ... endA function symbol, like "f" or "plus" or "is_human" or "socrates"
module Ty : sig ... endTypes
module Term : sig ... endTerm structure.
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_arith_lia/Make/argument-1-A/S/Unknown/index.html b/dev/sidekick/Sidekick_arith_lia/Make/argument-1-A/S/Unknown/index.html
deleted file mode 100644
index adc95a82..00000000
--- a/dev/sidekick/Sidekick_arith_lia/Make/argument-1-A/S/Unknown/index.html
+++ /dev/null
@@ -1,2 +0,0 @@
-
-Unknown (sidekick.Sidekick_arith_lia.Make.1-A.S.Unknown) Module S.Unknown
val pp : t CCFormat.printer
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_arith_lia/Make/argument-1-A/S/index.html b/dev/sidekick/Sidekick_arith_lia/Make/argument-1-A/S/index.html
deleted file mode 100644
index 86d698f8..00000000
--- a/dev/sidekick/Sidekick_arith_lia/Make/argument-1-A/S/index.html
+++ /dev/null
@@ -1,37 +0,0 @@
-
-S (sidekick.Sidekick_arith_lia.Make.1-A.S) Module 1-A.S
module T : Sidekick_core.TERMmodule Lit : Sidekick_core.LIT with module T = Tmodule P :
- Sidekick_core.PROOF
- with type lit = Lit.t
- and type t = proof
- and type proof_step = proof_step
- and type term = T.Term.tmodule Solver_internal :
- Sidekick_core.SOLVER_INTERNAL
- with module T = T
- and module Lit = Lit
- and type proof = proof
- and type proof_step = proof_step
- and module P = PInternal solver, available to theories.
type solver = ttype term = T.Term.ttype ty = T.Ty.ttype lit = Lit.tValue registry
module Registry : Sidekick_core.REGISTRYval registry : t -> Registry.tA solver contains a registry so that theories can share data
module type THEORY = sig ... endtype theory = (module THEORY)A theory that can be used for this particular solver.
A theory that can be used for this particular solver, with state of type 'a.
val mk_theory :
- name:string ->
- create_and_setup:( Solver_internal.t -> 'th ) ->
- ?push_level:( 'th -> unit ) ->
- ?pop_levels:( 'th -> int -> unit ) ->
- unit ->
- theoryHelper to create a theory.
module Model : sig ... endModels
module Unknown : sig ... endMain API
val stats : t -> Sidekick_util.Stat.tval tst : t -> T.Term.storeval ty_st : t -> T.Ty.storeval create :
- ?stat:Sidekick_util.Stat.t ->
- ?size:[ `Big | `Tiny | `Small ] ->
- proof:proof ->
- theories:theory list ->
- T.Term.store ->
- T.Ty.store ->
- unit ->
- tCreate a new solver.
It needs a term state and a type state to manipulate terms and types. All terms and types interacting with this solver will need to come from these exact states.
Add a theory to the solver. This should be called before any call to solve or to add_clause and the likes (otherwise the theory will have a partial view of the problem).
mk_lit_t _ ~sign t returns lit', where lit' is preprocess(lit) and lit is an internal representation of ± t.
The proof of |- lit = lit' is directly added to the solver's proof.
val add_clause : t -> lit Sidekick_util.IArray.t -> proof_step -> unitadd_clause solver cs adds a boolean clause to the solver. Subsequent calls to solve will need to satisfy this clause.
val add_clause_l : t -> lit list -> proof_step -> unitAdd a clause to the solver, given as a list.
Helper that turns each term into an atom, before adding the result to the solver as an assertion
Helper that turns the term into an atom, before adding the result to the solver as a unit clause assertion
type res = | Sat of Model.t(*Satisfiable
*) | Unsat of {unsat_core : unit -> lit Iter.t;(*Unsat core (subset of assumptions), or empty
*) unsat_proof_step : unit -> proof_step option;(*Proof step for the empty clause
*)
}(*Unsatisfiable
*) | Unknown of Unknown.t(*Unknown, obtained after a timeout, memory limit, etc.
*)
Result of solving for the current set of clauses
val solve :
- ?on_exit:( unit -> unit ) list ->
- ?check:bool ->
- ?on_progress:( t -> unit ) ->
- ?should_stop:( t -> int -> bool ) ->
- assumptions:lit list ->
- t ->
- ressolve s checks the satisfiability of the clauses added so far to s.
Last result, if any. Some operations will erase this (e.g. assert_term).
Pushes an assumption onto the assumption stack. It will remain there until it's pop'd by pop_assumptions.
val pop_assumptions : t -> int -> unitpop_assumptions solver n removes n assumptions from the stack. It removes the assumptions that were the most recently added via push_assumptions. Note that check_sat_propagations_only can call this if it meets a conflict.
type propagation_result = | PR_sat| PR_conflict of {backtracked : int;
}| PR_unsat of {unsat_core : unit -> lit Iter.t;
}
val check_sat_propagations_only :
- assumptions:lit list ->
- t ->
- propagation_resultcheck_sat_propagations_only solver uses assumptions (including the assumptions parameter, and atoms previously added via push_assumptions) and boolean+theory propagation to quickly assess satisfiability. It is not complete; calling solve is required to get an accurate result.
val pp_stats : t CCFormat.printerPrint some statistics. What it prints exactly is unspecified.
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_arith_lia/Make/argument-1-A/S/module-type-THEORY/index.html b/dev/sidekick/Sidekick_arith_lia/Make/argument-1-A/S/module-type-THEORY/index.html
deleted file mode 100644
index be4e9169..00000000
--- a/dev/sidekick/Sidekick_arith_lia/Make/argument-1-A/S/module-type-THEORY/index.html
+++ /dev/null
@@ -1,2 +0,0 @@
-
-THEORY (sidekick.Sidekick_arith_lia.Make.1-A.S.THEORY) Module type S.THEORY
A theory
Theories are abstracted over the concrete implementation of the solver, so they can work with any implementation.
Typically a theory should be a functor taking an argument containing a SOLVER_INTERNAL or even a full SOLVER, and some additional views on terms, literals, etc. that are specific to the theory (e.g. to map terms to linear expressions). The theory can then be instantiated on any kind of solver for any term representation that also satisfies the additional theory-specific requirements. Instantiated theories (ie values of type SOLVER.theory) can be added to the solver.
val create_and_setup : Solver_internal.t -> tInstantiate the theory's state for the given (internal) solver, register callbacks, create keys, etc.
Called once for every solver this theory is added to.
val push_level : t -> unitPush backtracking level. When the corresponding pop is called, the theory's state should be restored to a state equivalent to what it was just before push_level.
it does not have to be exactly the same state, it just needs to be equivalent.
val pop_levels : t -> int -> unitpop_levels theory n pops n backtracking levels, restoring theory to its state before calling push_level n times.
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_arith_lia/Make/argument-1-A/Z/index.html b/dev/sidekick/Sidekick_arith_lia/Make/argument-1-A/Z/index.html
deleted file mode 100644
index a5bc0274..00000000
--- a/dev/sidekick/Sidekick_arith_lia/Make/argument-1-A/Z/index.html
+++ /dev/null
@@ -1,2 +0,0 @@
-
-Z (sidekick.Sidekick_arith_lia.Make.1-A.Z) Module 1-A.Z
include Sidekick_arith.NUM
val zero : tval one : tval minus_one : tval sign : t -> intval of_int : int -> tinclude Sidekick_sigs.EQ with type t := t
include Sidekick_sigs.ORD with type t := t
include Sidekick_sigs.HASH with type t := t
val hash : t -> intinclude Sidekick_sigs.PRINT with type t := t
val pp : t CCFormat.printer
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_arith_lia/Make/argument-1-A/index.html b/dev/sidekick/Sidekick_arith_lia/Make/argument-1-A/index.html
deleted file mode 100644
index 4667c930..00000000
--- a/dev/sidekick/Sidekick_arith_lia/Make/argument-1-A/index.html
+++ /dev/null
@@ -1,3 +0,0 @@
-
-A (sidekick.Sidekick_arith_lia.Make.1-A) Parameter Make.1-A
module S : Sidekick_core.SOLVERmodule LRA_solver :
- Sidekick_arith_lra.S with type A.Q.t = Q.t and module A.S = Stype term = S.T.Term.ttype ty = S.T.Ty.tval mk_bool : S.T.Term.store -> bool -> termval mk_to_real : S.T.Term.store -> term -> termWrap term into a to_real projector to rationals
Make a term from the given theory view
val ty_int : S.T.Term.store -> tyval mk_eq : S.T.Term.store -> term -> term -> termsyntactic equality
val has_ty_int : term -> boolDoes this term have the type Int
val lemma_lia : S.Lit.t Iter.t -> S.P.proof_ruleval lemma_relax_to_lra : S.Lit.t Iter.t -> S.P.proof_rule
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_arith_lia/Make/index.html b/dev/sidekick/Sidekick_arith_lia/Make/index.html
deleted file mode 100644
index f49d76dd..00000000
--- a/dev/sidekick/Sidekick_arith_lia/Make/index.html
+++ /dev/null
@@ -1,2 +0,0 @@
-
-Make (sidekick.Sidekick_arith_lia.Make) Module Sidekick_arith_lia.Make
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_arith_lia/index.html b/dev/sidekick/Sidekick_arith_lia/index.html
deleted file mode 100644
index 4974676f..00000000
--- a/dev/sidekick/Sidekick_arith_lia/index.html
+++ /dev/null
@@ -1,5 +0,0 @@
-
-Sidekick_arith_lia (sidekick.Sidekick_arith_lia) Module Sidekick_arith_lia
Linear Rational Arithmetic
module type RATIONAL = Sidekick_arith.RATIONALmodule type INT = Sidekick_arith.INTmodule S_op = Sidekick_simplex.Opmodule type ARG = sig ... endmodule type S = sig ... end
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_arith_lia/module-type-ARG/LRA_solver/A/Gensym/index.html b/dev/sidekick/Sidekick_arith_lia/module-type-ARG/LRA_solver/A/Gensym/index.html
deleted file mode 100644
index 4533fdeb..00000000
--- a/dev/sidekick/Sidekick_arith_lia/module-type-ARG/LRA_solver/A/Gensym/index.html
+++ /dev/null
@@ -1,2 +0,0 @@
-
-Gensym (sidekick.Sidekick_arith_lia.ARG.LRA_solver.A.Gensym) Module A.Gensym
val create : S.T.Term.store -> tval tst : t -> S.T.Term.store
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_arith_lia/module-type-ARG/LRA_solver/A/Q/index.html b/dev/sidekick/Sidekick_arith_lia/module-type-ARG/LRA_solver/A/Q/index.html
deleted file mode 100644
index 67f4fc5e..00000000
--- a/dev/sidekick/Sidekick_arith_lia/module-type-ARG/LRA_solver/A/Q/index.html
+++ /dev/null
@@ -1,2 +0,0 @@
-
-Q (sidekick.Sidekick_arith_lia.ARG.LRA_solver.A.Q) Module A.Q
include Sidekick_arith.NUM with type t = Q.t
type t = Q.tval zero : tval one : tval minus_one : tval sign : t -> intval of_int : int -> tinclude Sidekick_sigs.EQ with type t := t
include Sidekick_sigs.ORD with type t := t
include Sidekick_sigs.HASH with type t := t
val hash : t -> intinclude Sidekick_sigs.PRINT with type t := t
val pp : t CCFormat.printertype bigint = Z.tval infinity : t+infinity
val minus_infinity : tval is_real : t -> boolA proper real, not nan/infinity
val is_int : t -> boolIs this a proper integer?
val pp_approx : int -> Stdlib.Format.formatter -> t -> unitPretty print rational with given amount of precision (for example as a floating point number)
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_arith_lia/module-type-ARG/LRA_solver/A/Z/index.html b/dev/sidekick/Sidekick_arith_lia/module-type-ARG/LRA_solver/A/Z/index.html
deleted file mode 100644
index 20cf01cb..00000000
--- a/dev/sidekick/Sidekick_arith_lia/module-type-ARG/LRA_solver/A/Z/index.html
+++ /dev/null
@@ -1,2 +0,0 @@
-
-Z (sidekick.Sidekick_arith_lia.ARG.LRA_solver.A.Z) Module A.Z
include Sidekick_arith.NUM
val zero : tval one : tval minus_one : tval sign : t -> intval of_int : int -> tinclude Sidekick_sigs.EQ with type t := t
include Sidekick_sigs.ORD with type t := t
include Sidekick_sigs.HASH with type t := t
val hash : t -> intinclude Sidekick_sigs.PRINT with type t := t
val pp : t CCFormat.printer
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_arith_lia/module-type-ARG/LRA_solver/A/index.html b/dev/sidekick/Sidekick_arith_lia/module-type-ARG/LRA_solver/A/index.html
deleted file mode 100644
index a0720fe3..00000000
--- a/dev/sidekick/Sidekick_arith_lia/module-type-ARG/LRA_solver/A/index.html
+++ /dev/null
@@ -1,5 +0,0 @@
-
-A (sidekick.Sidekick_arith_lia.ARG.LRA_solver.A) Module LRA_solver.A
module S = Smodule Z : Sidekick_arith_lra.INTtype term = S.T.Term.ttype ty = S.T.Ty.tval view_as_lra : term -> ( Q.t, term ) Sidekick_arith_lra.lra_viewProject the term into the theory view
val mk_bool : S.T.Term.store -> bool -> termval mk_lra :
- S.T.Term.store ->
- ( Q.t, term ) Sidekick_arith_lra.lra_view ->
- termMake a term from the given theory view
val ty_lra : S.T.Term.store -> tyval mk_eq : S.T.Term.store -> term -> term -> termsyntactic equality
val has_ty_real : term -> boolDoes this term have the type Real
val lemma_lra : S.Lit.t Iter.t -> S.P.proof_rulemodule Gensym : sig ... end
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_arith_lia/module-type-ARG/LRA_solver/SimpSolver/Constraint/index.html b/dev/sidekick/Sidekick_arith_lia/module-type-ARG/LRA_solver/SimpSolver/Constraint/index.html
deleted file mode 100644
index 8f473670..00000000
--- a/dev/sidekick/Sidekick_arith_lia/module-type-ARG/LRA_solver/SimpSolver/Constraint/index.html
+++ /dev/null
@@ -1,2 +0,0 @@
-
-Constraint (sidekick.Sidekick_arith_lia.ARG.LRA_solver.SimpSolver.Constraint) Module SimpSolver.Constraint
type op = Sidekick_simplex.Op.tval pp : t Sidekick_util.Fmt.printer
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_arith_lia/module-type-ARG/LRA_solver/SimpSolver/Q/index.html b/dev/sidekick/Sidekick_arith_lia/module-type-ARG/LRA_solver/SimpSolver/Q/index.html
deleted file mode 100644
index 55e8eb18..00000000
--- a/dev/sidekick/Sidekick_arith_lia/module-type-ARG/LRA_solver/SimpSolver/Q/index.html
+++ /dev/null
@@ -1,2 +0,0 @@
-
-Q (sidekick.Sidekick_arith_lia.ARG.LRA_solver.SimpSolver.Q) Module SimpSolver.Q
include Sidekick_arith.NUM
val zero : tval one : tval minus_one : tval sign : t -> intval of_int : int -> tinclude Sidekick_sigs.EQ with type t := t
include Sidekick_sigs.ORD with type t := t
include Sidekick_sigs.HASH with type t := t
val hash : t -> intinclude Sidekick_sigs.PRINT with type t := t
val pp : t CCFormat.printertype bigint = Z.tval infinity : t+infinity
val minus_infinity : tval is_real : t -> boolA proper real, not nan/infinity
val is_int : t -> boolIs this a proper integer?
val pp_approx : int -> Stdlib.Format.formatter -> t -> unitPretty print rational with given amount of precision (for example as a floating point number)
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_arith_lia/module-type-ARG/LRA_solver/SimpSolver/Subst/index.html b/dev/sidekick/Sidekick_arith_lia/module-type-ARG/LRA_solver/SimpSolver/Subst/index.html
deleted file mode 100644
index c5e3d9a3..00000000
--- a/dev/sidekick/Sidekick_arith_lia/module-type-ARG/LRA_solver/SimpSolver/Subst/index.html
+++ /dev/null
@@ -1,2 +0,0 @@
-
-Subst (sidekick.Sidekick_arith_lia.ARG.LRA_solver.SimpSolver.Subst) Module SimpSolver.Subst
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_arith_lia/module-type-ARG/LRA_solver/SimpSolver/Unsat_cert/index.html b/dev/sidekick/Sidekick_arith_lia/module-type-ARG/LRA_solver/SimpSolver/Unsat_cert/index.html
deleted file mode 100644
index adb47df2..00000000
--- a/dev/sidekick/Sidekick_arith_lia/module-type-ARG/LRA_solver/SimpSolver/Unsat_cert/index.html
+++ /dev/null
@@ -1,2 +0,0 @@
-
-Unsat_cert (sidekick.Sidekick_arith_lia.ARG.LRA_solver.SimpSolver.Unsat_cert) Module SimpSolver.Unsat_cert
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_arith_lia/module-type-ARG/LRA_solver/SimpSolver/V/index.html b/dev/sidekick/Sidekick_arith_lia/module-type-ARG/LRA_solver/SimpSolver/V/index.html
deleted file mode 100644
index d26e96f1..00000000
--- a/dev/sidekick/Sidekick_arith_lia/module-type-ARG/LRA_solver/SimpSolver/V/index.html
+++ /dev/null
@@ -1,2 +0,0 @@
-
-V (sidekick.Sidekick_arith_lia.ARG.LRA_solver.SimpSolver.V) Module SimpSolver.V
val pp : t Sidekick_util.Fmt.printerPrinter for variables.
val pp_lit : lit Sidekick_util.Fmt.printer
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_arith_lia/module-type-ARG/LRA_solver/SimpSolver/Z/index.html b/dev/sidekick/Sidekick_arith_lia/module-type-ARG/LRA_solver/SimpSolver/Z/index.html
deleted file mode 100644
index ce6236b9..00000000
--- a/dev/sidekick/Sidekick_arith_lia/module-type-ARG/LRA_solver/SimpSolver/Z/index.html
+++ /dev/null
@@ -1,2 +0,0 @@
-
-Z (sidekick.Sidekick_arith_lia.ARG.LRA_solver.SimpSolver.Z) Module SimpSolver.Z
include Sidekick_arith.NUM
val zero : tval one : tval minus_one : tval sign : t -> intval of_int : int -> tinclude Sidekick_sigs.EQ with type t := t
include Sidekick_sigs.ORD with type t := t
include Sidekick_sigs.HASH with type t := t
val hash : t -> intinclude Sidekick_sigs.PRINT with type t := t
val pp : t CCFormat.printer
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_arith_lia/module-type-ARG/LRA_solver/SimpSolver/index.html b/dev/sidekick/Sidekick_arith_lia/module-type-ARG/LRA_solver/SimpSolver/index.html
deleted file mode 100644
index 810fd60f..00000000
--- a/dev/sidekick/Sidekick_arith_lia/module-type-ARG/LRA_solver/SimpSolver/index.html
+++ /dev/null
@@ -1,16 +0,0 @@
-
-SimpSolver (sidekick.Sidekick_arith_lia.ARG.LRA_solver.SimpSolver) Module LRA_solver.SimpSolver
Simplexe
module V : Sidekick_simplex.VARmodule Z : Sidekick_simplex.INTmodule Q : Sidekick_simplex.RATIONAL with type bigint = Z.ttype num = Q.tNumbers
module Constraint : sig ... endmodule Subst : sig ... endval create : ?stat:Sidekick_util.Stat.t -> unit -> tCreate a new simplex.
val push_level : t -> unitval pop_levels : t -> int -> unitDefine a basic variable in terms of other variables. This is useful to "name" a linear expression and get back a variable that can be used in a Constraint.t
module Unsat_cert : sig ... endexception E_unsat of Unsat_cert.tval add_constraint :
- ?keep_on_backtracking:bool ->
- ?is_int:bool ->
- on_propagate:ev_on_propagate ->
- t ->
- Constraint.t ->
- V.lit ->
- unitAdd a constraint to the simplex.
This is removed upon backtracking by default.
val declare_bound : ?is_int:bool -> t -> Constraint.t -> V.lit -> unitDeclare that this constraint exists and map it to a literal, so we can possibly propagate it later. Unlike add_constraint this does NOT assert that the constraint is true
Check the whole simplex for satisfiability.
Call check_exn and return a model or a proof of unsat. This does NOT enforce that integer variables map to integer values.
val check_branch_and_bound :
- on_propagate:( V.lit -> reason:V.lit list -> unit ) ->
- max_tree_nodes:int ->
- t ->
- result optionTry to solve and respect the integer constraints.
val n_vars : t -> intval n_rows : t -> int
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_arith_lia/module-type-ARG/LRA_solver/index.html b/dev/sidekick/Sidekick_arith_lia/module-type-ARG/LRA_solver/index.html
deleted file mode 100644
index 59dae44f..00000000
--- a/dev/sidekick/Sidekick_arith_lia/module-type-ARG/LRA_solver/index.html
+++ /dev/null
@@ -1,2 +0,0 @@
-
-LRA_solver (sidekick.Sidekick_arith_lia.ARG.LRA_solver) Module ARG.LRA_solver
module SimpSolver : Sidekick_simplex.SSimplexe
val create : ?stat:Sidekick_util.Stat.t -> A.S.Solver_internal.t -> stateval k_state : state A.S.Solver_internal.Registry.keyKey to access the state from outside, available when the theory has been setup
val theory : A.S.theory
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_arith_lia/module-type-ARG/Q/index.html b/dev/sidekick/Sidekick_arith_lia/module-type-ARG/Q/index.html
deleted file mode 100644
index 4cd14844..00000000
--- a/dev/sidekick/Sidekick_arith_lia/module-type-ARG/Q/index.html
+++ /dev/null
@@ -1,2 +0,0 @@
-
-Q (sidekick.Sidekick_arith_lia.ARG.Q) Module ARG.Q
include Sidekick_arith.NUM
val zero : tval one : tval minus_one : tval sign : t -> intval of_int : int -> tinclude Sidekick_sigs.EQ with type t := t
include Sidekick_sigs.ORD with type t := t
include Sidekick_sigs.HASH with type t := t
val hash : t -> intinclude Sidekick_sigs.PRINT with type t := t
val pp : t CCFormat.printertype bigint = Z.tval infinity : t+infinity
val minus_infinity : tval is_real : t -> boolA proper real, not nan/infinity
val is_int : t -> boolIs this a proper integer?
val pp_approx : int -> Stdlib.Format.formatter -> t -> unitPretty print rational with given amount of precision (for example as a floating point number)
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_arith_lia/module-type-ARG/S/Lit/index.html b/dev/sidekick/Sidekick_arith_lia/module-type-ARG/S/Lit/index.html
deleted file mode 100644
index bbefc4c4..00000000
--- a/dev/sidekick/Sidekick_arith_lia/module-type-ARG/S/Lit/index.html
+++ /dev/null
@@ -1,2 +0,0 @@
-
-Lit (sidekick.Sidekick_arith_lia.ARG.S.Lit) Module S.Lit
module T = TLiterals depend on terms
val sign : t -> boolGet the sign. A negated literal has sign false.
val atom : ?sign:bool -> T.Term.store -> T.Term.t -> tatom store t makes a literal out of a term, possibly normalizing its sign in the process.
norm_sign (+t) is +t, true, and norm_sign (-t) is +t, false. In both cases the term is positive, and the boolean reflects the initial sign.
val hash : t -> intval pp : t Sidekick_core.Fmt.printer
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_arith_lia/module-type-ARG/S/Model/index.html b/dev/sidekick/Sidekick_arith_lia/module-type-ARG/S/Model/index.html
deleted file mode 100644
index 637e2668..00000000
--- a/dev/sidekick/Sidekick_arith_lia/module-type-ARG/S/Model/index.html
+++ /dev/null
@@ -1,2 +0,0 @@
-
-Model (sidekick.Sidekick_arith_lia.ARG.S.Model) Module S.Model
Models
A model can be produced when the solver is found to be in a satisfiable state after a call to solve.
val empty : tval pp : t Sidekick_core.Fmt.printer
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_arith_lia/module-type-ARG/S/P/Step_vec/index.html b/dev/sidekick/Sidekick_arith_lia/module-type-ARG/S/P/Step_vec/index.html
deleted file mode 100644
index 6b508426..00000000
--- a/dev/sidekick/Sidekick_arith_lia/module-type-ARG/S/P/Step_vec/index.html
+++ /dev/null
@@ -1,2 +0,0 @@
-
-Step_vec (sidekick.Sidekick_arith_lia.ARG.S.P.Step_vec) Module P.Step_vec
A vector of steps
include Sidekick_util.Vec_sig.BASE with type elt = proof_step
include Sidekick_util.Vec_sig.BASE_RO with type elt = proof_step
type elt = proof_stepval size : t -> intval create : ?cap:int -> unit -> tval clear : t -> unitval is_empty : t -> boolval fast_remove : t -> int -> unitRemove element at index i without preserving order (swap with last element)
val ensure_size : t -> int -> unitval shrink : t -> int -> unit
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_arith_lia/module-type-ARG/S/P/index.html b/dev/sidekick/Sidekick_arith_lia/module-type-ARG/S/P/index.html
deleted file mode 100644
index 169a1307..00000000
--- a/dev/sidekick/Sidekick_arith_lia/module-type-ARG/S/P/index.html
+++ /dev/null
@@ -1,10 +0,0 @@
-
-P (sidekick.Sidekick_arith_lia.ARG.S.P) Module S.P
type t = proofThe abstract representation of a proof. A proof always proves a clause to be valid (true in every possible interpretation of the problem's assertions, and the theories)
type proof_step = proof_stepIdentifier for a proof proof_rule (like a unique ID for a clause previously added/proved)
type term = T.Term.ttype lit = Lit.ttype proof_rule = t -> proof_stepinclude Sidekick_core.SAT_PROOF
- with type t := t
- and type lit := lit
- and type proof_step := proof_step
- and type proof_rule := proof_rule
module Step_vec : Sidekick_util.Vec_sig.S with type elt = proof_stepA vector of steps
val enabled : t -> boolReturns true if proof production is enabled
val emit_input_clause : lit Iter.t -> proof_ruleEmit an input clause.
val emit_redundant_clause : lit Iter.t -> hyps:proof_step Iter.t -> proof_ruleEmit a clause deduced by the SAT solver, redundant wrt previous clauses. The clause must be RUP wrt hyps.
val emit_unsat_core : lit Iter.t -> proof_ruleProduce a proof of the empty clause given this subset of the assumptions. FIXME: probably needs the list of proof_step that disprove the lits?
val emit_unsat : proof_step -> t -> unitSignal "unsat" result at the given proof
val del_clause : proof_step -> lit Iter.t -> t -> unitForget a clause. Only useful for performance considerations.
val lemma_cc : lit Iter.t -> proof_rulelemma_cc proof lits asserts that lits form a tautology for the theory of uninterpreted functions.
val define_term : term -> term -> proof_ruledefine_term cst u proof defines the new constant cst as being equal to u. The result is a proof of the clause cst = u
val proof_p1 : proof_step -> proof_step -> proof_ruleproof_p1 p1 p2, where p1 proves the unit clause t=u (t:bool) and p2 proves C \/ t, is the rule that produces C \/ u, i.e unit paramodulation.
val proof_r1 : proof_step -> proof_step -> proof_ruleproof_r1 p1 p2, where p1 proves the unit clause |- t (t:bool) and p2 proves C \/ ¬t, is the rule that produces C \/ u, i.e unit resolution.
val proof_res : pivot:term -> proof_step -> proof_step -> proof_ruleproof_res ~pivot p1 p2, where p1 proves the clause |- C \/ l and p2 proves D \/ ¬l, where l is either pivot or ¬pivot, is the rule that produces C \/ D, i.e boolean resolution.
val with_defs : proof_step -> proof_step Iter.t -> proof_rulewith_defs pr defs specifies that pr is valid only in a context where the definitions defs are present.
val lemma_true : term -> proof_rulelemma_true (true) p asserts the clause (true)
val lemma_preprocess : term -> term -> using:proof_step Iter.t -> proof_rulelemma_preprocess t u ~using p asserts that t = u is a tautology and that t has been preprocessed into u.
The theorem /\_{eqn in using} eqn |- t=u is proved using congruence closure, and then resolved against the clauses using to obtain a unit equality.
From now on, t and u will be used interchangeably.
val lemma_rw_clause :
- proof_step ->
- res:lit Iter.t ->
- using:proof_step Iter.t ->
- proof_rulelemma_rw_clause prc ~res ~using, where prc is the proof of |- c, uses the equations |- p_i = q_i from using to rewrite some literals of c into res. This is used to preprocess literals of a clause (using lemma_preprocess individually).
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_arith_lia/module-type-ARG/S/Registry/index.html b/dev/sidekick/Sidekick_arith_lia/module-type-ARG/S/Registry/index.html
deleted file mode 100644
index 521b758c..00000000
--- a/dev/sidekick/Sidekick_arith_lia/module-type-ARG/S/Registry/index.html
+++ /dev/null
@@ -1,2 +0,0 @@
-
-Registry (sidekick.Sidekick_arith_lia.ARG.S.Registry) Module S.Registry
val create_key : unit -> 'a keyCall this statically, typically at program initialization, for each distinct key.
val create : unit -> t
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_arith_lia/module-type-ARG/S/Solver_internal/CC/Actions/P/Step_vec/index.html b/dev/sidekick/Sidekick_arith_lia/module-type-ARG/S/Solver_internal/CC/Actions/P/Step_vec/index.html
deleted file mode 100644
index c16c8bfb..00000000
--- a/dev/sidekick/Sidekick_arith_lia/module-type-ARG/S/Solver_internal/CC/Actions/P/Step_vec/index.html
+++ /dev/null
@@ -1,2 +0,0 @@
-
-Step_vec (sidekick.Sidekick_arith_lia.ARG.S.Solver_internal.CC.Actions.P.Step_vec) Module P.Step_vec
A vector of steps
include Sidekick_util.Vec_sig.BASE with type elt = proof_step
include Sidekick_util.Vec_sig.BASE_RO with type elt = proof_step
type elt = proof_stepval size : t -> intval create : ?cap:int -> unit -> tval clear : t -> unitval is_empty : t -> boolval fast_remove : t -> int -> unitRemove element at index i without preserving order (swap with last element)
val ensure_size : t -> int -> unitval shrink : t -> int -> unit
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_arith_lia/module-type-ARG/S/Solver_internal/CC/Actions/P/index.html b/dev/sidekick/Sidekick_arith_lia/module-type-ARG/S/Solver_internal/CC/Actions/P/index.html
deleted file mode 100644
index 26c1f875..00000000
--- a/dev/sidekick/Sidekick_arith_lia/module-type-ARG/S/Solver_internal/CC/Actions/P/index.html
+++ /dev/null
@@ -1,10 +0,0 @@
-
-P (sidekick.Sidekick_arith_lia.ARG.S.Solver_internal.CC.Actions.P) Module Actions.P
type t = proofThe abstract representation of a proof. A proof always proves a clause to be valid (true in every possible interpretation of the problem's assertions, and the theories)
type proof_step = proof_stepIdentifier for a proof proof_rule (like a unique ID for a clause previously added/proved)
type term = T.Term.ttype lit = Lit.ttype proof_rule = t -> proof_stepinclude Sidekick_core.SAT_PROOF
- with type t := t
- and type lit := lit
- and type proof_step := proof_step
- and type proof_rule := proof_rule
module Step_vec : Sidekick_util.Vec_sig.S with type elt = proof_stepA vector of steps
val enabled : t -> boolReturns true if proof production is enabled
val emit_input_clause : lit Iter.t -> proof_ruleEmit an input clause.
val emit_redundant_clause : lit Iter.t -> hyps:proof_step Iter.t -> proof_ruleEmit a clause deduced by the SAT solver, redundant wrt previous clauses. The clause must be RUP wrt hyps.
val emit_unsat_core : lit Iter.t -> proof_ruleProduce a proof of the empty clause given this subset of the assumptions. FIXME: probably needs the list of proof_step that disprove the lits?
val emit_unsat : proof_step -> t -> unitSignal "unsat" result at the given proof
val del_clause : proof_step -> lit Iter.t -> t -> unitForget a clause. Only useful for performance considerations.
val lemma_cc : lit Iter.t -> proof_rulelemma_cc proof lits asserts that lits form a tautology for the theory of uninterpreted functions.
val define_term : term -> term -> proof_ruledefine_term cst u proof defines the new constant cst as being equal to u. The result is a proof of the clause cst = u
val proof_p1 : proof_step -> proof_step -> proof_ruleproof_p1 p1 p2, where p1 proves the unit clause t=u (t:bool) and p2 proves C \/ t, is the rule that produces C \/ u, i.e unit paramodulation.
val proof_r1 : proof_step -> proof_step -> proof_ruleproof_r1 p1 p2, where p1 proves the unit clause |- t (t:bool) and p2 proves C \/ ¬t, is the rule that produces C \/ u, i.e unit resolution.
val proof_res : pivot:term -> proof_step -> proof_step -> proof_ruleproof_res ~pivot p1 p2, where p1 proves the clause |- C \/ l and p2 proves D \/ ¬l, where l is either pivot or ¬pivot, is the rule that produces C \/ D, i.e boolean resolution.
val with_defs : proof_step -> proof_step Iter.t -> proof_rulewith_defs pr defs specifies that pr is valid only in a context where the definitions defs are present.
val lemma_true : term -> proof_rulelemma_true (true) p asserts the clause (true)
val lemma_preprocess : term -> term -> using:proof_step Iter.t -> proof_rulelemma_preprocess t u ~using p asserts that t = u is a tautology and that t has been preprocessed into u.
The theorem /\_{eqn in using} eqn |- t=u is proved using congruence closure, and then resolved against the clauses using to obtain a unit equality.
From now on, t and u will be used interchangeably.
val lemma_rw_clause :
- proof_step ->
- res:lit Iter.t ->
- using:proof_step Iter.t ->
- proof_rulelemma_rw_clause prc ~res ~using, where prc is the proof of |- c, uses the equations |- p_i = q_i from using to rewrite some literals of c into res. This is used to preprocess literals of a clause (using lemma_preprocess individually).
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_arith_lia/module-type-ARG/S/Solver_internal/CC/Actions/index.html b/dev/sidekick/Sidekick_arith_lia/module-type-ARG/S/Solver_internal/CC/Actions/index.html
deleted file mode 100644
index 2e6bf03e..00000000
--- a/dev/sidekick/Sidekick_arith_lia/module-type-ARG/S/Solver_internal/CC/Actions/index.html
+++ /dev/null
@@ -1,15 +0,0 @@
-
-Actions (sidekick.Sidekick_arith_lia.ARG.S.Solver_internal.CC.Actions) Module CC.Actions
module T = Tmodule Lit = Littype proof = prooftype proof_step = proof_stepmodule P :
- Sidekick_core.PROOF
- with type lit = Lit.t
- and type t = proof
- and type term = T.Term.t
- and type proof_step = proof_steptype t = theory_actionsAn action handle. It is used by the congruence closure to perform the actions below. How it performs the actions is not specified and is solver-specific.
val raise_conflict : t -> Lit.t list -> proof_step -> 'araise_conflict acts c pr declares that c is a tautology of the theory of congruence. This does not return (it should raise an exception).
raise_semantic_conflict acts lits same_val declares that the conjunction of all lits (literals true in current trail) and tuples {=,≠}, t_i, u_i implies false.
The {=,≠}, t_i, u_i are pairs of terms with the same value (if = / true) or distinct value (if ≠ / false)) in the current model.
This does not return. It should raise an exception.
val propagate :
- t ->
- Lit.t ->
- reason:( unit -> Lit.t list * proof_step ) ->
- unitpropagate acts lit ~reason pr declares that reason() => lit is a tautology.
reason() should return a list of literals that are currently true.lit should be a literal of interest (see CC_S.set_as_lit).
This function might never be called, a congruence closure has the right to not propagate and only trigger conflicts.
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_arith_lia/module-type-ARG/S/Solver_internal/CC/Expl/index.html b/dev/sidekick/Sidekick_arith_lia/module-type-ARG/S/Solver_internal/CC/Expl/index.html
deleted file mode 100644
index 1e2025bf..00000000
--- a/dev/sidekick/Sidekick_arith_lia/module-type-ARG/S/Solver_internal/CC/Expl/index.html
+++ /dev/null
@@ -1,2 +0,0 @@
-
-Expl (sidekick.Sidekick_arith_lia.ARG.S.Solver_internal.CC.Expl) Module CC.Expl
Explanations
Explanations are specialized proofs, created by the congruence closure when asked to justify why 2 terms are equal.
val pp : t Sidekick_core.Fmt.printerExplanation: we merged t and u because of literal t=u, or we merged t and true because of literal t, or t and false because of literal ¬t
mk_theory t u expl_sets pr builds a theory explanation for why |- t=u. It depends on sub-explanations expl_sets which are tuples (t_i, u_i, expls_i) where expls_i are explanations that justify t_i = u_i in the current congruence closure.
The proof pr is the theory lemma, of the form (t_i = u_i)_i |- t=u . It is resolved against each expls_i |- t_i=u_i obtained from expl_sets, on pivot t_i=u_i, to obtain a proof of Gamma |- t=u where Gamma is a subset of the literals asserted into the congruence closure.
For example for the lemma a=b deduced by injectivity from Some a=Some b in the theory of datatypes, the arguments would be a, b, [Some a, Some b, mk_merge_t (Some a)(Some b)], pr where pr is the injectivity lemma Some a=Some b |- a=b.
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_arith_lia/module-type-ARG/S/Solver_internal/CC/N/index.html b/dev/sidekick/Sidekick_arith_lia/module-type-ARG/S/Solver_internal/CC/N/index.html
deleted file mode 100644
index e58d05af..00000000
--- a/dev/sidekick/Sidekick_arith_lia/module-type-ARG/S/Solver_internal/CC/N/index.html
+++ /dev/null
@@ -1,2 +0,0 @@
-
-N (sidekick.Sidekick_arith_lia.ARG.S.Solver_internal.CC.N) Module CC.N
Equivalence classes.
An equivalence class is a set of terms that are currently equal in the partial model built by the solver. The class is represented by a collection of nodes, one of which is distinguished and is called the "representative".
All information pertaining to the whole equivalence class is stored in this representative's node.
When two classes become equal (are "merged"), one of the two representatives is picked as the representative of the new class. The new class contains the union of the two old classes' nodes.
We also allow theories to store additional information in the representative. This information can be used when two classes are merged, to detect conflicts and solve equations à la Shostak.
An equivalent class, containing terms that are proved to be equal.
A value of type t points to a particular term, but see find to get the representative of the class.
Term contained in this equivalence class. If is_root n, then term n is the class' representative term.
Are two classes physically equal? To check for logical equality, use CC.N.equal (CC.find cc n1) (CC.find cc n2) which checks for equality of representatives.
val hash : t -> intAn opaque hash of this node.
val pp : t Sidekick_core.Fmt.printerUnspecified printing of the node, for example its term, a unique ID, etc.
val is_root : t -> boolIs the node a root (ie the representative of its class)? See find to get the root.
Traverse the congruence class. Precondition: is_root n (see find below)
Traverse the parents of the class. Precondition: is_root n (see find below)
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_arith_lia/module-type-ARG/S/Solver_internal/CC/P/Step_vec/index.html b/dev/sidekick/Sidekick_arith_lia/module-type-ARG/S/Solver_internal/CC/P/Step_vec/index.html
deleted file mode 100644
index 4782a0c6..00000000
--- a/dev/sidekick/Sidekick_arith_lia/module-type-ARG/S/Solver_internal/CC/P/Step_vec/index.html
+++ /dev/null
@@ -1,2 +0,0 @@
-
-Step_vec (sidekick.Sidekick_arith_lia.ARG.S.Solver_internal.CC.P.Step_vec) Module P.Step_vec
A vector of steps
include Sidekick_util.Vec_sig.BASE with type elt = proof_step
include Sidekick_util.Vec_sig.BASE_RO with type elt = proof_step
type elt = proof_stepval size : t -> intval create : ?cap:int -> unit -> tval clear : t -> unitval is_empty : t -> boolval fast_remove : t -> int -> unitRemove element at index i without preserving order (swap with last element)
val ensure_size : t -> int -> unitval shrink : t -> int -> unit
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_arith_lia/module-type-ARG/S/Solver_internal/CC/P/index.html b/dev/sidekick/Sidekick_arith_lia/module-type-ARG/S/Solver_internal/CC/P/index.html
deleted file mode 100644
index 7263856e..00000000
--- a/dev/sidekick/Sidekick_arith_lia/module-type-ARG/S/Solver_internal/CC/P/index.html
+++ /dev/null
@@ -1,10 +0,0 @@
-
-P (sidekick.Sidekick_arith_lia.ARG.S.Solver_internal.CC.P) Module CC.P
type t = proofThe abstract representation of a proof. A proof always proves a clause to be valid (true in every possible interpretation of the problem's assertions, and the theories)
type proof_step = proof_stepIdentifier for a proof proof_rule (like a unique ID for a clause previously added/proved)
type lit = littype proof_rule = t -> proof_stepinclude Sidekick_core.SAT_PROOF
- with type t := t
- and type lit := lit
- and type proof_step := proof_step
- and type proof_rule := proof_rule
module Step_vec : Sidekick_util.Vec_sig.S with type elt = proof_stepA vector of steps
val enabled : t -> boolReturns true if proof production is enabled
val emit_input_clause : lit Iter.t -> proof_ruleEmit an input clause.
val emit_redundant_clause : lit Iter.t -> hyps:proof_step Iter.t -> proof_ruleEmit a clause deduced by the SAT solver, redundant wrt previous clauses. The clause must be RUP wrt hyps.
val emit_unsat_core : lit Iter.t -> proof_ruleProduce a proof of the empty clause given this subset of the assumptions. FIXME: probably needs the list of proof_step that disprove the lits?
val emit_unsat : proof_step -> t -> unitSignal "unsat" result at the given proof
val del_clause : proof_step -> lit Iter.t -> t -> unitForget a clause. Only useful for performance considerations.
val lemma_cc : lit Iter.t -> proof_rulelemma_cc proof lits asserts that lits form a tautology for the theory of uninterpreted functions.
val define_term : term -> term -> proof_ruledefine_term cst u proof defines the new constant cst as being equal to u. The result is a proof of the clause cst = u
val proof_p1 : proof_step -> proof_step -> proof_ruleproof_p1 p1 p2, where p1 proves the unit clause t=u (t:bool) and p2 proves C \/ t, is the rule that produces C \/ u, i.e unit paramodulation.
val proof_r1 : proof_step -> proof_step -> proof_ruleproof_r1 p1 p2, where p1 proves the unit clause |- t (t:bool) and p2 proves C \/ ¬t, is the rule that produces C \/ u, i.e unit resolution.
val proof_res : pivot:term -> proof_step -> proof_step -> proof_ruleproof_res ~pivot p1 p2, where p1 proves the clause |- C \/ l and p2 proves D \/ ¬l, where l is either pivot or ¬pivot, is the rule that produces C \/ D, i.e boolean resolution.
val with_defs : proof_step -> proof_step Iter.t -> proof_rulewith_defs pr defs specifies that pr is valid only in a context where the definitions defs are present.
val lemma_true : term -> proof_rulelemma_true (true) p asserts the clause (true)
val lemma_preprocess : term -> term -> using:proof_step Iter.t -> proof_rulelemma_preprocess t u ~using p asserts that t = u is a tautology and that t has been preprocessed into u.
The theorem /\_{eqn in using} eqn |- t=u is proved using congruence closure, and then resolved against the clauses using to obtain a unit equality.
From now on, t and u will be used interchangeably.
val lemma_rw_clause :
- proof_step ->
- res:lit Iter.t ->
- using:proof_step Iter.t ->
- proof_rulelemma_rw_clause prc ~res ~using, where prc is the proof of |- c, uses the equations |- p_i = q_i from using to rewrite some literals of c into res. This is used to preprocess literals of a clause (using lemma_preprocess individually).
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_arith_lia/module-type-ARG/S/Solver_internal/CC/Resolved_expl/index.html b/dev/sidekick/Sidekick_arith_lia/module-type-ARG/S/Solver_internal/CC/Resolved_expl/index.html
deleted file mode 100644
index 8cbfd93f..00000000
--- a/dev/sidekick/Sidekick_arith_lia/module-type-ARG/S/Solver_internal/CC/Resolved_expl/index.html
+++ /dev/null
@@ -1,2 +0,0 @@
-
-Resolved_expl (sidekick.Sidekick_arith_lia.ARG.S.Solver_internal.CC.Resolved_expl) Module CC.Resolved_expl
Resolved explanations.
The congruence closure keeps explanations for why terms are in the same class. However these are represented in a compact, cheap form. To use these explanations we need to resolve them into a resolved explanation, typically a list of literals that are true in the current trail and are responsible for merges.
However, we can also have merged classes because they have the same value in the current model.
val is_semantic : t -> boolis_semantic expl is true if there's at least one pair in expl.same_value.
val pp : t Sidekick_core.Fmt.printer
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_arith_lia/module-type-ARG/S/Solver_internal/CC/index.html b/dev/sidekick/Sidekick_arith_lia/module-type-ARG/S/Solver_internal/CC/index.html
deleted file mode 100644
index 76515caf..00000000
--- a/dev/sidekick/Sidekick_arith_lia/module-type-ARG/S/Solver_internal/CC/index.html
+++ /dev/null
@@ -1,25 +0,0 @@
-
-CC (sidekick.Sidekick_arith_lia.ARG.S.Solver_internal.CC) Module Solver_internal.CC
Congruence closure instance
first, some aliases.
module T = Tmodule Lit = Littype proof = prooftype proof_step = proof_stepmodule P :
- Sidekick_core.PROOF
- with type lit = Lit.t
- and type t = proof
- and type proof_step = proof_step
- with type t = proof
- with type lit = litmodule Actions :
- Sidekick_core.CC_ACTIONS
- with module T = T
- and module Lit = Lit
- and type proof = proof
- and type proof_step = proof_step
- with type t = theory_actionstype term_store = T.Term.storetype term = T.Term.ttype value = termtype fun_ = T.Fun.ttype lit = Lit.ttype actions = Actions.tThe congruence closure object. It contains a fair amount of state and is mutable and backtrackable.
module N : sig ... endEquivalence classes.
module Expl : sig ... endExplanations
module Resolved_expl : sig ... endResolved explanations.
type node = N.tA node of the congruence closure
type repr = N.tNode that is currently a representative
type explanation = Expl.tAccessors
val term_store : t -> term_storeAdd the term to the congruence closure, if not present already. Will be backtracked.
Returns true if the term is explicitly present in the congruence closure
Events
Events triggered by the congruence closure, to which other plugins can subscribe.
ev_on_pre_merge cc acts n1 n2 expl is called right before n1 and n2 are merged with explanation expl.
ev_on_post_merge cc acts n1 n2 is called right after n1 and n2 were merged. find cc n1 and find cc n2 will return the same node.
ev_on_new_term cc n t is called whenever a new term t is added to the congruence closure. Its node is n.
ev_on_conflict acts ~th c is called when the congruence closure triggers a conflict by asserting the tautology c.
type ev_on_propagate = t -> lit -> ( unit -> lit list * proof_step ) -> unitev_on_propagate cc lit reason is called whenever reason() => lit is a propagated lemma. See CC_ACTIONS.propagate.
ev_on_is_subterm n t is called when n is a subterm of another node for the first time. t is the term corresponding to the node n. This can be useful for theory combination.
val create :
- ?stat:Sidekick_util.Stat.t ->
- ?on_pre_merge:ev_on_pre_merge list ->
- ?on_post_merge:ev_on_post_merge list ->
- ?on_new_term:ev_on_new_term list ->
- ?on_conflict:ev_on_conflict list ->
- ?on_propagate:ev_on_propagate list ->
- ?on_is_subterm:ev_on_is_subterm list ->
- ?size:[ `Small | `Big ] ->
- term_store ->
- proof ->
- tCreate a new congruence closure.
val allocate_bitfield : descr:string -> t -> N.bitfieldAllocate a new node field (see N.bitfield).
This field descriptor is henceforth reserved for all nodes in this congruence closure, and can be set using set_bitfield for each node individually. This can be used to efficiently store some metadata on nodes (e.g. "is there a numeric value in the class" or "is there a constructor term in the class").
There may be restrictions on how many distinct fields are allocated for a given congruence closure (e.g. at most Sys.int_size fields).
val get_bitfield : t -> N.bitfield -> N.t -> boolAccess the bit field of the given node
val set_bitfield : t -> N.bitfield -> bool -> N.t -> unitSet the bitfield for the node. This will be backtracked. See N.bitfield.
val on_pre_merge : t -> ev_on_pre_merge -> unitAdd a function to be called when two classes are merged
val on_post_merge : t -> ev_on_post_merge -> unitAdd a function to be called when two classes are merged
val on_new_term : t -> ev_on_new_term -> unitAdd a function to be called when a new node is created
val on_conflict : t -> ev_on_conflict -> unitCalled when the congruence closure finds a conflict
val on_propagate : t -> ev_on_propagate -> unitCalled when the congruence closure propagates a literal
val on_is_subterm : t -> ev_on_is_subterm -> unitCalled on terms that are subterms of function symbols
All current classes. This is costly, only use if there is no other solution
Given a literal, assume it in the congruence closure and propagate its consequences. Will be backtracked.
Useful for the theory combination or the SAT solver's functor
val explain_eq : t -> N.t -> N.t -> Resolved_expl.tExplain why the two nodes are equal. Fails if they are not, in an unspecified way.
Raise a conflict with the given explanation. It must be a theory tautology that expl ==> absurd. To be used in theories.
This fails in an unspecified way if the explanation, once resolved, satisfies Resolved_expl.is_semantic.
Merge these two nodes given this explanation. It must be a theory tautology that expl ==> n1 = n2. To be used in theories.
val with_model_mode : t -> ( unit -> 'a ) -> 'aEnter model combination mode.
In model combination mode, obtain classes with their values.
Perform all pending operations done via assert_eq, assert_lit, etc. Will use the actions to propagate literals, declare conflicts, etc.
val push_level : t -> unitPush backtracking level
val pop_levels : t -> int -> unitRestore to state n calls to push_level earlier. Used during backtracking.
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_arith_lia/module-type-ARG/S/Solver_internal/Registry/index.html b/dev/sidekick/Sidekick_arith_lia/module-type-ARG/S/Solver_internal/Registry/index.html
deleted file mode 100644
index f927ccf9..00000000
--- a/dev/sidekick/Sidekick_arith_lia/module-type-ARG/S/Solver_internal/Registry/index.html
+++ /dev/null
@@ -1,2 +0,0 @@
-
-Registry (sidekick.Sidekick_arith_lia.ARG.S.Solver_internal.Registry) Module Solver_internal.Registry
val create_key : unit -> 'a keyCall this statically, typically at program initialization, for each distinct key.
val create : unit -> t
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_arith_lia/module-type-ARG/S/Solver_internal/Simplify/index.html b/dev/sidekick/Sidekick_arith_lia/module-type-ARG/S/Solver_internal/Simplify/index.html
deleted file mode 100644
index 857a4a60..00000000
--- a/dev/sidekick/Sidekick_arith_lia/module-type-ARG/S/Solver_internal/Simplify/index.html
+++ /dev/null
@@ -1,2 +0,0 @@
-
-Simplify (sidekick.Sidekick_arith_lia.ARG.S.Solver_internal.Simplify) Module Solver_internal.Simplify
Simplify terms
val tst : t -> term_storeval clear : t -> unitReset internal cache, etc.
type hook = t -> term -> (term * proof_step Iter.t) optionGiven a term, try to simplify it. Return None if it didn't change.
A simple example could be a hook that takes a term t, and if t is app "+" (const x) (const y) where x and y are number, returns Some (const (x+y)), and None otherwise.
The simplifier will take care of simplifying the resulting term further, caching (so that work is not duplicated in subterms), etc.
val normalize : t -> term -> (term * proof_step) optionNormalize a term using all the hooks. This performs a fixpoint, i.e. it only stops when no hook applies anywhere inside the term.
val normalize_t : t -> term -> term * proof_step optionNormalize a term using all the hooks, along with a proof that the simplification is correct. returns t, ø if no simplification occurred.
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_arith_lia/module-type-ARG/S/Solver_internal/index.html b/dev/sidekick/Sidekick_arith_lia/module-type-ARG/S/Solver_internal/index.html
deleted file mode 100644
index 2b0eaf3b..00000000
--- a/dev/sidekick/Sidekick_arith_lia/module-type-ARG/S/Solver_internal/index.html
+++ /dev/null
@@ -1,43 +0,0 @@
-
-Solver_internal (sidekick.Sidekick_arith_lia.ARG.S.Solver_internal) Module S.Solver_internal
Internal solver, available to theories.
module T = Tmodule Lit = Littype ty = T.Ty.ttype term = T.Term.ttype value = T.Term.ttype term_store = T.Term.storetype ty_store = T.Ty.storetype proof = prooftype proof_step = proof_stepmodule P = Ptype solver = tval tst : t -> term_storeval stats : t -> Sidekick_util.Stat.tRegistry
module Registry : Sidekick_core.REGISTRYval registry : t -> Registry.tA solver contains a registry so that theories can share data
Actions for the theories
type lit = Lit.tCongruence Closure
module CC :
- Sidekick_core.CC_S
- with module T = T
- and module Lit = Lit
- and type proof = proof
- and type proof_step = proof_step
- and type P.t = proof
- and type P.lit = lit
- and type Actions.t = theory_actionsCongruence closure instance
Simplifiers
module Simplify : sig ... endSimplify terms
type simplify_hook = Simplify.hookval add_simplifier : t -> Simplify.hook -> unitAdd a simplifier hook for preprocessing.
val simplify_t : t -> term -> (term * proof_step) optionSimplify input term, returns Some u if some simplification occurred.
val simp_t : t -> term -> term * proof_step optionsimp_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.
module type PREPROCESS_ACTS = sig ... endtype preprocess_actions = (module PREPROCESS_ACTS)Actions available to the preprocessor
type preprocess_hook = t -> preprocess_actions -> term -> unitGiven a term, preprocess it.
The idea is to add literals and clauses to help define the meaning of the term, if needed. For example for boolean formulas, clauses for their Tseitin encoding can be added, with the formula acting as its own proxy symbol.
val on_preprocess : t -> preprocess_hook -> unitAdd a hook that will be called when terms are preprocessed
hooks for the theory
val raise_conflict : t -> theory_actions -> lit list -> proof_step -> 'aGive a conflict clause to the solver
val push_decision : t -> theory_actions -> lit -> unitAsk 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.
val propagate :
- t ->
- theory_actions ->
- lit ->
- reason:( unit -> lit list * proof_step ) ->
- unitPropagate a boolean using a unit clause. expl => lit must be a theory lemma, that is, a T-tautology
val propagate_l : t -> theory_actions -> lit -> lit list -> proof_step -> unitPropagate a boolean using a unit clause. expl => lit must be a theory lemma, that is, a T-tautology
val add_clause_temp : t -> theory_actions -> lit list -> proof_step -> unitAdd local clause to the SAT solver. This clause will be removed when the solver backtracks.
val add_clause_permanent :
- t ->
- theory_actions ->
- lit list ->
- proof_step ->
- unitAdd toplevel clause to the SAT solver. This clause will not be backtracked.
val mk_lit : t -> theory_actions -> ?sign:bool -> term -> litCreate a literal. This automatically preprocesses the term.
val add_lit : t -> theory_actions -> ?default_pol:bool -> lit -> unitAdd the given literal to the SAT solver, so it gets assigned a boolean value.
val add_lit_t : t -> theory_actions -> ?sign:bool -> term -> unitAdd the given (signed) bool term to the SAT solver, so it gets assigned a boolean value
val cc_raise_conflict_expl : t -> theory_actions -> CC.Expl.t -> 'aRaise a conflict with the given congruence closure explanation. it must be a theory tautology that expl ==> absurd. To be used in theories.
val cc_merge : t -> theory_actions -> CC.N.t -> CC.N.t -> CC.Expl.t -> unitMerge these two nodes in the congruence closure, given this explanation. It must be a theory tautology that expl ==> n1 = n2. To be used in theories.
val cc_merge_t : t -> theory_actions -> term -> term -> CC.Expl.t -> unitMerge these two terms in the congruence closure, given this explanation. See cc_merge
Add/retrieve congruence closure node for this term. To be used in theories
Return true if the term is explicitly in the congruence closure. To be used in theories
val on_cc_pre_merge :
- t ->
- ( CC.t -> theory_actions -> CC.N.t -> CC.N.t -> CC.Expl.t -> unit ) ->
- unitCallback for when two classes containing data for this key are merged (called before)
val on_cc_post_merge :
- t ->
- ( CC.t -> theory_actions -> CC.N.t -> CC.N.t -> unit ) ->
- unitCallback for when two classes containing data for this key are merged (called after)
Callback to add data on terms when they are added to the congruence closure
Callback for when a term is a subterm of another term in the congruence closure
Callback called on every CC conflict
val on_cc_propagate :
- t ->
- ( CC.t -> lit -> ( unit -> lit list * proof_step ) -> unit ) ->
- unitCallback called on every CC propagation
val on_partial_check :
- t ->
- ( t -> theory_actions -> lit Iter.t -> unit ) ->
- unitRegister 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.
val on_final_check : t -> ( t -> theory_actions -> lit Iter.t -> unit ) -> unitRegister callback to be called during the final check.
Must be complete (i.e. must raise a conflict if the set of literals is not satisfiable) and can be expensive. The function is given the whole trail.
val on_th_combination :
- t ->
- ( t -> theory_actions -> (term * value) Iter.t ) ->
- unitAdd a hook called during theory combination. The hook must return an iterator of pairs (t, v) which mean that term t has value v in the model.
Terms with the same value (according to Term.equal) will be merged in the CC; if two terms with different values are merged, we get a semantic conflict and must pick another model.
val declare_pb_is_incomplete : t -> unitDeclare that, in some theory, the problem is outside the logic fragment that is decidable (e.g. if we meet proper NIA formulas). The solver will not reply "SAT" from now on.
Model production
A model-production hook to query values from a theory.
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.
A model production hook, for the theory to add values. The hook is given a add function to add bindings to the model.
val on_model :
- ?ask:model_ask_hook ->
- ?complete:model_completion_hook ->
- t ->
- unitAdd model production/completion hooks.
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_arith_lia/module-type-ARG/S/Solver_internal/module-type-PREPROCESS_ACTS/index.html b/dev/sidekick/Sidekick_arith_lia/module-type-ARG/S/Solver_internal/module-type-PREPROCESS_ACTS/index.html
deleted file mode 100644
index 826ea7eb..00000000
--- a/dev/sidekick/Sidekick_arith_lia/module-type-ARG/S/Solver_internal/module-type-PREPROCESS_ACTS/index.html
+++ /dev/null
@@ -1,2 +0,0 @@
-
-PREPROCESS_ACTS (sidekick.Sidekick_arith_lia.ARG.S.Solver_internal.PREPROCESS_ACTS) Module type Solver_internal.PREPROCESS_ACTS
val proof : proofval add_clause : lit list -> proof_step -> unitpushes a new clause into the SAT solver.
val add_lit : ?default_pol:bool -> lit -> unitEnsure the literal will be decided/handled by the SAT solver.
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_arith_lia/module-type-ARG/S/T/Fun/index.html b/dev/sidekick/Sidekick_arith_lia/module-type-ARG/S/T/Fun/index.html
deleted file mode 100644
index 39e813a2..00000000
--- a/dev/sidekick/Sidekick_arith_lia/module-type-ARG/S/T/Fun/index.html
+++ /dev/null
@@ -1,2 +0,0 @@
-
-Fun (sidekick.Sidekick_arith_lia.ARG.S.T.Fun) Module T.Fun
A function symbol, like "f" or "plus" or "is_human" or "socrates"
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_arith_lia/module-type-ARG/S/T/Term/index.html b/dev/sidekick/Sidekick_arith_lia/module-type-ARG/S/T/Term/index.html
deleted file mode 100644
index 0609e004..00000000
--- a/dev/sidekick/Sidekick_arith_lia/module-type-ARG/S/T/Term/index.html
+++ /dev/null
@@ -1,8 +0,0 @@
-
-Term (sidekick.Sidekick_arith_lia.ARG.S.T.Term) Module T.Term
Term structure.
Terms should be hashconsed, with perfect sharing. This allows, for example, Term.Tbl and Term.iter_dag to be efficient.
val hash : t -> intval pp : t Sidekick_core.Fmt.printerA store used to create new terms. It is where the hashconsing table should live, along with other all-terms related store.
val as_bool : t -> bool optionas_bool t is Some true if t is the term true, and similarly for false. For other terms it is None.
abs t returns an "absolute value" for the term, along with the sign of t.
The idea is that we want to turn not a into (a, false), or (a != b) into (a=b, false). For terms without a negation this should return (t, true).
The store is passed in case a new term needs to be created.
Map function on immediate subterms. This should not be recursive.
Iterate function on immediate subterms. This should not be recursive.
iter_dag t f calls f once on each subterm of t, t included. It must not traverse t as a tree, but rather as a perfectly shared DAG.
For example, in:
let x = 2 in
-let y = f x x in
-let z = g y x in
-z = z
the DAG has the following nodes:
n1: 2
-n2: f n1 n1
-n3: g n2 n1
-n4: = n3 n3
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_arith_lia/module-type-ARG/S/T/Ty/index.html b/dev/sidekick/Sidekick_arith_lia/module-type-ARG/S/T/Ty/index.html
deleted file mode 100644
index 174b3ea7..00000000
--- a/dev/sidekick/Sidekick_arith_lia/module-type-ARG/S/T/Ty/index.html
+++ /dev/null
@@ -1,2 +0,0 @@
-
-Ty (sidekick.Sidekick_arith_lia.ARG.S.T.Ty) Module T.Ty
Types
Types should be comparable (ideally, in O(1)), and have at least a boolean type available.
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_arith_lia/module-type-ARG/S/T/index.html b/dev/sidekick/Sidekick_arith_lia/module-type-ARG/S/T/index.html
deleted file mode 100644
index 835f0198..00000000
--- a/dev/sidekick/Sidekick_arith_lia/module-type-ARG/S/T/index.html
+++ /dev/null
@@ -1,2 +0,0 @@
-
-T (sidekick.Sidekick_arith_lia.ARG.S.T) Module S.T
module Fun : sig ... endA function symbol, like "f" or "plus" or "is_human" or "socrates"
module Ty : sig ... endTypes
module Term : sig ... endTerm structure.
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_arith_lia/module-type-ARG/S/Unknown/index.html b/dev/sidekick/Sidekick_arith_lia/module-type-ARG/S/Unknown/index.html
deleted file mode 100644
index 38191872..00000000
--- a/dev/sidekick/Sidekick_arith_lia/module-type-ARG/S/Unknown/index.html
+++ /dev/null
@@ -1,2 +0,0 @@
-
-Unknown (sidekick.Sidekick_arith_lia.ARG.S.Unknown) Module S.Unknown
val pp : t CCFormat.printer
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_arith_lia/module-type-ARG/S/index.html b/dev/sidekick/Sidekick_arith_lia/module-type-ARG/S/index.html
deleted file mode 100644
index 1b165886..00000000
--- a/dev/sidekick/Sidekick_arith_lia/module-type-ARG/S/index.html
+++ /dev/null
@@ -1,37 +0,0 @@
-
-S (sidekick.Sidekick_arith_lia.ARG.S) Module ARG.S
module T : Sidekick_core.TERMmodule Lit : Sidekick_core.LIT with module T = Tmodule P :
- Sidekick_core.PROOF
- with type lit = Lit.t
- and type t = proof
- and type proof_step = proof_step
- and type term = T.Term.tmodule Solver_internal :
- Sidekick_core.SOLVER_INTERNAL
- with module T = T
- and module Lit = Lit
- and type proof = proof
- and type proof_step = proof_step
- and module P = PInternal solver, available to theories.
type solver = ttype term = T.Term.ttype ty = T.Ty.ttype lit = Lit.tValue registry
module Registry : Sidekick_core.REGISTRYval registry : t -> Registry.tA solver contains a registry so that theories can share data
module type THEORY = sig ... endtype theory = (module THEORY)A theory that can be used for this particular solver.
A theory that can be used for this particular solver, with state of type 'a.
val mk_theory :
- name:string ->
- create_and_setup:( Solver_internal.t -> 'th ) ->
- ?push_level:( 'th -> unit ) ->
- ?pop_levels:( 'th -> int -> unit ) ->
- unit ->
- theoryHelper to create a theory.
module Model : sig ... endModels
module Unknown : sig ... endMain API
val stats : t -> Sidekick_util.Stat.tval tst : t -> T.Term.storeval ty_st : t -> T.Ty.storeval create :
- ?stat:Sidekick_util.Stat.t ->
- ?size:[ `Big | `Tiny | `Small ] ->
- proof:proof ->
- theories:theory list ->
- T.Term.store ->
- T.Ty.store ->
- unit ->
- tCreate a new solver.
It needs a term state and a type state to manipulate terms and types. All terms and types interacting with this solver will need to come from these exact states.
Add a theory to the solver. This should be called before any call to solve or to add_clause and the likes (otherwise the theory will have a partial view of the problem).
mk_lit_t _ ~sign t returns lit', where lit' is preprocess(lit) and lit is an internal representation of ± t.
The proof of |- lit = lit' is directly added to the solver's proof.
val add_clause : t -> lit Sidekick_util.IArray.t -> proof_step -> unitadd_clause solver cs adds a boolean clause to the solver. Subsequent calls to solve will need to satisfy this clause.
val add_clause_l : t -> lit list -> proof_step -> unitAdd a clause to the solver, given as a list.
Helper that turns each term into an atom, before adding the result to the solver as an assertion
Helper that turns the term into an atom, before adding the result to the solver as a unit clause assertion
type res = | Sat of Model.t(*Satisfiable
*) | Unsat of {unsat_core : unit -> lit Iter.t;(*Unsat core (subset of assumptions), or empty
*) unsat_proof_step : unit -> proof_step option;(*Proof step for the empty clause
*)
}(*Unsatisfiable
*) | Unknown of Unknown.t(*Unknown, obtained after a timeout, memory limit, etc.
*)
Result of solving for the current set of clauses
val solve :
- ?on_exit:( unit -> unit ) list ->
- ?check:bool ->
- ?on_progress:( t -> unit ) ->
- ?should_stop:( t -> int -> bool ) ->
- assumptions:lit list ->
- t ->
- ressolve s checks the satisfiability of the clauses added so far to s.
Last result, if any. Some operations will erase this (e.g. assert_term).
Pushes an assumption onto the assumption stack. It will remain there until it's pop'd by pop_assumptions.
val pop_assumptions : t -> int -> unitpop_assumptions solver n removes n assumptions from the stack. It removes the assumptions that were the most recently added via push_assumptions. Note that check_sat_propagations_only can call this if it meets a conflict.
type propagation_result = | PR_sat| PR_conflict of {backtracked : int;
}| PR_unsat of {unsat_core : unit -> lit Iter.t;
}
val check_sat_propagations_only :
- assumptions:lit list ->
- t ->
- propagation_resultcheck_sat_propagations_only solver uses assumptions (including the assumptions parameter, and atoms previously added via push_assumptions) and boolean+theory propagation to quickly assess satisfiability. It is not complete; calling solve is required to get an accurate result.
val pp_stats : t CCFormat.printerPrint some statistics. What it prints exactly is unspecified.
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_arith_lia/module-type-ARG/S/module-type-THEORY/index.html b/dev/sidekick/Sidekick_arith_lia/module-type-ARG/S/module-type-THEORY/index.html
deleted file mode 100644
index 951fbc29..00000000
--- a/dev/sidekick/Sidekick_arith_lia/module-type-ARG/S/module-type-THEORY/index.html
+++ /dev/null
@@ -1,2 +0,0 @@
-
-THEORY (sidekick.Sidekick_arith_lia.ARG.S.THEORY) Module type S.THEORY
A theory
Theories are abstracted over the concrete implementation of the solver, so they can work with any implementation.
Typically a theory should be a functor taking an argument containing a SOLVER_INTERNAL or even a full SOLVER, and some additional views on terms, literals, etc. that are specific to the theory (e.g. to map terms to linear expressions). The theory can then be instantiated on any kind of solver for any term representation that also satisfies the additional theory-specific requirements. Instantiated theories (ie values of type SOLVER.theory) can be added to the solver.
val create_and_setup : Solver_internal.t -> tInstantiate the theory's state for the given (internal) solver, register callbacks, create keys, etc.
Called once for every solver this theory is added to.
val push_level : t -> unitPush backtracking level. When the corresponding pop is called, the theory's state should be restored to a state equivalent to what it was just before push_level.
it does not have to be exactly the same state, it just needs to be equivalent.
val pop_levels : t -> int -> unitpop_levels theory n pops n backtracking levels, restoring theory to its state before calling push_level n times.
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_arith_lia/module-type-ARG/Z/index.html b/dev/sidekick/Sidekick_arith_lia/module-type-ARG/Z/index.html
deleted file mode 100644
index c570658e..00000000
--- a/dev/sidekick/Sidekick_arith_lia/module-type-ARG/Z/index.html
+++ /dev/null
@@ -1,2 +0,0 @@
-
-Z (sidekick.Sidekick_arith_lia.ARG.Z) Module ARG.Z
include Sidekick_arith.NUM
val zero : tval one : tval minus_one : tval sign : t -> intval of_int : int -> tinclude Sidekick_sigs.EQ with type t := t
include Sidekick_sigs.ORD with type t := t
include Sidekick_sigs.HASH with type t := t
val hash : t -> intinclude Sidekick_sigs.PRINT with type t := t
val pp : t CCFormat.printer
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_arith_lia/module-type-ARG/index.html b/dev/sidekick/Sidekick_arith_lia/module-type-ARG/index.html
deleted file mode 100644
index d87b7ab9..00000000
--- a/dev/sidekick/Sidekick_arith_lia/module-type-ARG/index.html
+++ /dev/null
@@ -1,3 +0,0 @@
-
-ARG (sidekick.Sidekick_arith_lia.ARG) Module type Sidekick_arith_lia.ARG
module S : Sidekick_core.SOLVERmodule LRA_solver :
- Sidekick_arith_lra.S with type A.Q.t = Q.t and module A.S = Stype term = S.T.Term.ttype ty = S.T.Ty.tval mk_bool : S.T.Term.store -> bool -> termval mk_to_real : S.T.Term.store -> term -> termWrap term into a to_real projector to rationals
Make a term from the given theory view
val ty_int : S.T.Term.store -> tyval mk_eq : S.T.Term.store -> term -> term -> termsyntactic equality
val has_ty_int : term -> boolDoes this term have the type Int
val lemma_lia : S.Lit.t Iter.t -> S.P.proof_ruleval lemma_relax_to_lra : S.Lit.t Iter.t -> S.P.proof_rule
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_arith_lia/module-type-S/A/LRA_solver/A/Gensym/index.html b/dev/sidekick/Sidekick_arith_lia/module-type-S/A/LRA_solver/A/Gensym/index.html
deleted file mode 100644
index 20302cb8..00000000
--- a/dev/sidekick/Sidekick_arith_lia/module-type-S/A/LRA_solver/A/Gensym/index.html
+++ /dev/null
@@ -1,2 +0,0 @@
-
-Gensym (sidekick.Sidekick_arith_lia.S.A.LRA_solver.A.Gensym) Module A.Gensym
val create : S.T.Term.store -> tval tst : t -> S.T.Term.store
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_arith_lia/module-type-S/A/LRA_solver/A/Q/index.html b/dev/sidekick/Sidekick_arith_lia/module-type-S/A/LRA_solver/A/Q/index.html
deleted file mode 100644
index 4567ea0d..00000000
--- a/dev/sidekick/Sidekick_arith_lia/module-type-S/A/LRA_solver/A/Q/index.html
+++ /dev/null
@@ -1,2 +0,0 @@
-
-Q (sidekick.Sidekick_arith_lia.S.A.LRA_solver.A.Q) Module A.Q
include Sidekick_arith.NUM with type t = Q.t
type t = Q.tval zero : tval one : tval minus_one : tval sign : t -> intval of_int : int -> tinclude Sidekick_sigs.EQ with type t := t
include Sidekick_sigs.ORD with type t := t
include Sidekick_sigs.HASH with type t := t
val hash : t -> intinclude Sidekick_sigs.PRINT with type t := t
val pp : t CCFormat.printertype bigint = Z.tval infinity : t+infinity
val minus_infinity : tval is_real : t -> boolA proper real, not nan/infinity
val is_int : t -> boolIs this a proper integer?
val pp_approx : int -> Stdlib.Format.formatter -> t -> unitPretty print rational with given amount of precision (for example as a floating point number)
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_arith_lia/module-type-S/A/LRA_solver/A/Z/index.html b/dev/sidekick/Sidekick_arith_lia/module-type-S/A/LRA_solver/A/Z/index.html
deleted file mode 100644
index d54b7b5f..00000000
--- a/dev/sidekick/Sidekick_arith_lia/module-type-S/A/LRA_solver/A/Z/index.html
+++ /dev/null
@@ -1,2 +0,0 @@
-
-Z (sidekick.Sidekick_arith_lia.S.A.LRA_solver.A.Z) Module A.Z
include Sidekick_arith.NUM
val zero : tval one : tval minus_one : tval sign : t -> intval of_int : int -> tinclude Sidekick_sigs.EQ with type t := t
include Sidekick_sigs.ORD with type t := t
include Sidekick_sigs.HASH with type t := t
val hash : t -> intinclude Sidekick_sigs.PRINT with type t := t
val pp : t CCFormat.printer
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_arith_lia/module-type-S/A/LRA_solver/A/index.html b/dev/sidekick/Sidekick_arith_lia/module-type-S/A/LRA_solver/A/index.html
deleted file mode 100644
index e7c6dc7f..00000000
--- a/dev/sidekick/Sidekick_arith_lia/module-type-S/A/LRA_solver/A/index.html
+++ /dev/null
@@ -1,5 +0,0 @@
-
-A (sidekick.Sidekick_arith_lia.S.A.LRA_solver.A) Module LRA_solver.A
module S = Smodule Z : Sidekick_arith_lra.INTtype term = S.T.Term.ttype ty = S.T.Ty.tval view_as_lra : term -> ( Q.t, term ) Sidekick_arith_lra.lra_viewProject the term into the theory view
val mk_bool : S.T.Term.store -> bool -> termval mk_lra :
- S.T.Term.store ->
- ( Q.t, term ) Sidekick_arith_lra.lra_view ->
- termMake a term from the given theory view
val ty_lra : S.T.Term.store -> tyval mk_eq : S.T.Term.store -> term -> term -> termsyntactic equality
val has_ty_real : term -> boolDoes this term have the type Real
val lemma_lra : S.Lit.t Iter.t -> S.P.proof_rulemodule Gensym : sig ... end
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_arith_lia/module-type-S/A/LRA_solver/SimpSolver/Constraint/index.html b/dev/sidekick/Sidekick_arith_lia/module-type-S/A/LRA_solver/SimpSolver/Constraint/index.html
deleted file mode 100644
index f6514d39..00000000
--- a/dev/sidekick/Sidekick_arith_lia/module-type-S/A/LRA_solver/SimpSolver/Constraint/index.html
+++ /dev/null
@@ -1,2 +0,0 @@
-
-Constraint (sidekick.Sidekick_arith_lia.S.A.LRA_solver.SimpSolver.Constraint) Module SimpSolver.Constraint
type op = Sidekick_simplex.Op.tval pp : t Sidekick_util.Fmt.printer
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_arith_lia/module-type-S/A/LRA_solver/SimpSolver/Q/index.html b/dev/sidekick/Sidekick_arith_lia/module-type-S/A/LRA_solver/SimpSolver/Q/index.html
deleted file mode 100644
index eabd8975..00000000
--- a/dev/sidekick/Sidekick_arith_lia/module-type-S/A/LRA_solver/SimpSolver/Q/index.html
+++ /dev/null
@@ -1,2 +0,0 @@
-
-Q (sidekick.Sidekick_arith_lia.S.A.LRA_solver.SimpSolver.Q) Module SimpSolver.Q
include Sidekick_arith.NUM
val zero : tval one : tval minus_one : tval sign : t -> intval of_int : int -> tinclude Sidekick_sigs.EQ with type t := t
include Sidekick_sigs.ORD with type t := t
include Sidekick_sigs.HASH with type t := t
val hash : t -> intinclude Sidekick_sigs.PRINT with type t := t
val pp : t CCFormat.printertype bigint = Z.tval infinity : t+infinity
val minus_infinity : tval is_real : t -> boolA proper real, not nan/infinity
val is_int : t -> boolIs this a proper integer?
val pp_approx : int -> Stdlib.Format.formatter -> t -> unitPretty print rational with given amount of precision (for example as a floating point number)
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_arith_lia/module-type-S/A/LRA_solver/SimpSolver/Subst/index.html b/dev/sidekick/Sidekick_arith_lia/module-type-S/A/LRA_solver/SimpSolver/Subst/index.html
deleted file mode 100644
index d91e0bbf..00000000
--- a/dev/sidekick/Sidekick_arith_lia/module-type-S/A/LRA_solver/SimpSolver/Subst/index.html
+++ /dev/null
@@ -1,2 +0,0 @@
-
-Subst (sidekick.Sidekick_arith_lia.S.A.LRA_solver.SimpSolver.Subst) Module SimpSolver.Subst
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_arith_lia/module-type-S/A/LRA_solver/SimpSolver/Unsat_cert/index.html b/dev/sidekick/Sidekick_arith_lia/module-type-S/A/LRA_solver/SimpSolver/Unsat_cert/index.html
deleted file mode 100644
index 0c1b0811..00000000
--- a/dev/sidekick/Sidekick_arith_lia/module-type-S/A/LRA_solver/SimpSolver/Unsat_cert/index.html
+++ /dev/null
@@ -1,2 +0,0 @@
-
-Unsat_cert (sidekick.Sidekick_arith_lia.S.A.LRA_solver.SimpSolver.Unsat_cert) Module SimpSolver.Unsat_cert
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_arith_lia/module-type-S/A/LRA_solver/SimpSolver/V/index.html b/dev/sidekick/Sidekick_arith_lia/module-type-S/A/LRA_solver/SimpSolver/V/index.html
deleted file mode 100644
index c49b8bd0..00000000
--- a/dev/sidekick/Sidekick_arith_lia/module-type-S/A/LRA_solver/SimpSolver/V/index.html
+++ /dev/null
@@ -1,2 +0,0 @@
-
-V (sidekick.Sidekick_arith_lia.S.A.LRA_solver.SimpSolver.V) Module SimpSolver.V
val pp : t Sidekick_util.Fmt.printerPrinter for variables.
val pp_lit : lit Sidekick_util.Fmt.printer
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_arith_lia/module-type-S/A/LRA_solver/SimpSolver/Z/index.html b/dev/sidekick/Sidekick_arith_lia/module-type-S/A/LRA_solver/SimpSolver/Z/index.html
deleted file mode 100644
index 0df2694f..00000000
--- a/dev/sidekick/Sidekick_arith_lia/module-type-S/A/LRA_solver/SimpSolver/Z/index.html
+++ /dev/null
@@ -1,2 +0,0 @@
-
-Z (sidekick.Sidekick_arith_lia.S.A.LRA_solver.SimpSolver.Z) Module SimpSolver.Z
include Sidekick_arith.NUM
val zero : tval one : tval minus_one : tval sign : t -> intval of_int : int -> tinclude Sidekick_sigs.EQ with type t := t
include Sidekick_sigs.ORD with type t := t
include Sidekick_sigs.HASH with type t := t
val hash : t -> intinclude Sidekick_sigs.PRINT with type t := t
val pp : t CCFormat.printer
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_arith_lia/module-type-S/A/LRA_solver/SimpSolver/index.html b/dev/sidekick/Sidekick_arith_lia/module-type-S/A/LRA_solver/SimpSolver/index.html
deleted file mode 100644
index da506670..00000000
--- a/dev/sidekick/Sidekick_arith_lia/module-type-S/A/LRA_solver/SimpSolver/index.html
+++ /dev/null
@@ -1,16 +0,0 @@
-
-SimpSolver (sidekick.Sidekick_arith_lia.S.A.LRA_solver.SimpSolver) Module LRA_solver.SimpSolver
Simplexe
module V : Sidekick_simplex.VARmodule Z : Sidekick_simplex.INTmodule Q : Sidekick_simplex.RATIONAL with type bigint = Z.ttype num = Q.tNumbers
module Constraint : sig ... endmodule Subst : sig ... endval create : ?stat:Sidekick_util.Stat.t -> unit -> tCreate a new simplex.
val push_level : t -> unitval pop_levels : t -> int -> unitDefine a basic variable in terms of other variables. This is useful to "name" a linear expression and get back a variable that can be used in a Constraint.t
module Unsat_cert : sig ... endexception E_unsat of Unsat_cert.tval add_constraint :
- ?keep_on_backtracking:bool ->
- ?is_int:bool ->
- on_propagate:ev_on_propagate ->
- t ->
- Constraint.t ->
- V.lit ->
- unitAdd a constraint to the simplex.
This is removed upon backtracking by default.
val declare_bound : ?is_int:bool -> t -> Constraint.t -> V.lit -> unitDeclare that this constraint exists and map it to a literal, so we can possibly propagate it later. Unlike add_constraint this does NOT assert that the constraint is true
Check the whole simplex for satisfiability.
Call check_exn and return a model or a proof of unsat. This does NOT enforce that integer variables map to integer values.
val check_branch_and_bound :
- on_propagate:( V.lit -> reason:V.lit list -> unit ) ->
- max_tree_nodes:int ->
- t ->
- result optionTry to solve and respect the integer constraints.
val n_vars : t -> intval n_rows : t -> int
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_arith_lia/module-type-S/A/LRA_solver/index.html b/dev/sidekick/Sidekick_arith_lia/module-type-S/A/LRA_solver/index.html
deleted file mode 100644
index 7c0c32a4..00000000
--- a/dev/sidekick/Sidekick_arith_lia/module-type-S/A/LRA_solver/index.html
+++ /dev/null
@@ -1,2 +0,0 @@
-
-LRA_solver (sidekick.Sidekick_arith_lia.S.A.LRA_solver) Module A.LRA_solver
module SimpSolver : Sidekick_simplex.SSimplexe
val create : ?stat:Sidekick_util.Stat.t -> A.S.Solver_internal.t -> stateval k_state : state A.S.Solver_internal.Registry.keyKey to access the state from outside, available when the theory has been setup
val theory : A.S.theory
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_arith_lia/module-type-S/A/Q/index.html b/dev/sidekick/Sidekick_arith_lia/module-type-S/A/Q/index.html
deleted file mode 100644
index cd35b1a4..00000000
--- a/dev/sidekick/Sidekick_arith_lia/module-type-S/A/Q/index.html
+++ /dev/null
@@ -1,2 +0,0 @@
-
-Q (sidekick.Sidekick_arith_lia.S.A.Q) Module A.Q
include Sidekick_arith.NUM
val zero : tval one : tval minus_one : tval sign : t -> intval of_int : int -> tinclude Sidekick_sigs.EQ with type t := t
include Sidekick_sigs.ORD with type t := t
include Sidekick_sigs.HASH with type t := t
val hash : t -> intinclude Sidekick_sigs.PRINT with type t := t
val pp : t CCFormat.printertype bigint = Z.tval infinity : t+infinity
val minus_infinity : tval is_real : t -> boolA proper real, not nan/infinity
val is_int : t -> boolIs this a proper integer?
val pp_approx : int -> Stdlib.Format.formatter -> t -> unitPretty print rational with given amount of precision (for example as a floating point number)
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_arith_lia/module-type-S/A/S/Lit/index.html b/dev/sidekick/Sidekick_arith_lia/module-type-S/A/S/Lit/index.html
deleted file mode 100644
index be9a24dd..00000000
--- a/dev/sidekick/Sidekick_arith_lia/module-type-S/A/S/Lit/index.html
+++ /dev/null
@@ -1,2 +0,0 @@
-
-Lit (sidekick.Sidekick_arith_lia.S.A.S.Lit) Module S.Lit
module T = TLiterals depend on terms
val sign : t -> boolGet the sign. A negated literal has sign false.
val atom : ?sign:bool -> T.Term.store -> T.Term.t -> tatom store t makes a literal out of a term, possibly normalizing its sign in the process.
norm_sign (+t) is +t, true, and norm_sign (-t) is +t, false. In both cases the term is positive, and the boolean reflects the initial sign.
val hash : t -> intval pp : t Sidekick_core.Fmt.printer
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_arith_lia/module-type-S/A/S/Model/index.html b/dev/sidekick/Sidekick_arith_lia/module-type-S/A/S/Model/index.html
deleted file mode 100644
index 34b43f7b..00000000
--- a/dev/sidekick/Sidekick_arith_lia/module-type-S/A/S/Model/index.html
+++ /dev/null
@@ -1,2 +0,0 @@
-
-Model (sidekick.Sidekick_arith_lia.S.A.S.Model) Module S.Model
Models
A model can be produced when the solver is found to be in a satisfiable state after a call to solve.
val empty : tval pp : t Sidekick_core.Fmt.printer
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_arith_lia/module-type-S/A/S/P/Step_vec/index.html b/dev/sidekick/Sidekick_arith_lia/module-type-S/A/S/P/Step_vec/index.html
deleted file mode 100644
index 615eb808..00000000
--- a/dev/sidekick/Sidekick_arith_lia/module-type-S/A/S/P/Step_vec/index.html
+++ /dev/null
@@ -1,2 +0,0 @@
-
-Step_vec (sidekick.Sidekick_arith_lia.S.A.S.P.Step_vec) Module P.Step_vec
A vector of steps
include Sidekick_util.Vec_sig.BASE with type elt = proof_step
include Sidekick_util.Vec_sig.BASE_RO with type elt = proof_step
type elt = proof_stepval size : t -> intval create : ?cap:int -> unit -> tval clear : t -> unitval is_empty : t -> boolval fast_remove : t -> int -> unitRemove element at index i without preserving order (swap with last element)
val ensure_size : t -> int -> unitval shrink : t -> int -> unit
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_arith_lia/module-type-S/A/S/P/index.html b/dev/sidekick/Sidekick_arith_lia/module-type-S/A/S/P/index.html
deleted file mode 100644
index 6c0e8438..00000000
--- a/dev/sidekick/Sidekick_arith_lia/module-type-S/A/S/P/index.html
+++ /dev/null
@@ -1,10 +0,0 @@
-
-P (sidekick.Sidekick_arith_lia.S.A.S.P) Module S.P
type t = proofThe abstract representation of a proof. A proof always proves a clause to be valid (true in every possible interpretation of the problem's assertions, and the theories)
type proof_step = proof_stepIdentifier for a proof proof_rule (like a unique ID for a clause previously added/proved)
type term = T.Term.ttype lit = Lit.ttype proof_rule = t -> proof_stepinclude Sidekick_core.SAT_PROOF
- with type t := t
- and type lit := lit
- and type proof_step := proof_step
- and type proof_rule := proof_rule
module Step_vec : Sidekick_util.Vec_sig.S with type elt = proof_stepA vector of steps
val enabled : t -> boolReturns true if proof production is enabled
val emit_input_clause : lit Iter.t -> proof_ruleEmit an input clause.
val emit_redundant_clause : lit Iter.t -> hyps:proof_step Iter.t -> proof_ruleEmit a clause deduced by the SAT solver, redundant wrt previous clauses. The clause must be RUP wrt hyps.
val emit_unsat_core : lit Iter.t -> proof_ruleProduce a proof of the empty clause given this subset of the assumptions. FIXME: probably needs the list of proof_step that disprove the lits?
val emit_unsat : proof_step -> t -> unitSignal "unsat" result at the given proof
val del_clause : proof_step -> lit Iter.t -> t -> unitForget a clause. Only useful for performance considerations.
val lemma_cc : lit Iter.t -> proof_rulelemma_cc proof lits asserts that lits form a tautology for the theory of uninterpreted functions.
val define_term : term -> term -> proof_ruledefine_term cst u proof defines the new constant cst as being equal to u. The result is a proof of the clause cst = u
val proof_p1 : proof_step -> proof_step -> proof_ruleproof_p1 p1 p2, where p1 proves the unit clause t=u (t:bool) and p2 proves C \/ t, is the rule that produces C \/ u, i.e unit paramodulation.
val proof_r1 : proof_step -> proof_step -> proof_ruleproof_r1 p1 p2, where p1 proves the unit clause |- t (t:bool) and p2 proves C \/ ¬t, is the rule that produces C \/ u, i.e unit resolution.
val proof_res : pivot:term -> proof_step -> proof_step -> proof_ruleproof_res ~pivot p1 p2, where p1 proves the clause |- C \/ l and p2 proves D \/ ¬l, where l is either pivot or ¬pivot, is the rule that produces C \/ D, i.e boolean resolution.
val with_defs : proof_step -> proof_step Iter.t -> proof_rulewith_defs pr defs specifies that pr is valid only in a context where the definitions defs are present.
val lemma_true : term -> proof_rulelemma_true (true) p asserts the clause (true)
val lemma_preprocess : term -> term -> using:proof_step Iter.t -> proof_rulelemma_preprocess t u ~using p asserts that t = u is a tautology and that t has been preprocessed into u.
The theorem /\_{eqn in using} eqn |- t=u is proved using congruence closure, and then resolved against the clauses using to obtain a unit equality.
From now on, t and u will be used interchangeably.
val lemma_rw_clause :
- proof_step ->
- res:lit Iter.t ->
- using:proof_step Iter.t ->
- proof_rulelemma_rw_clause prc ~res ~using, where prc is the proof of |- c, uses the equations |- p_i = q_i from using to rewrite some literals of c into res. This is used to preprocess literals of a clause (using lemma_preprocess individually).
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_arith_lia/module-type-S/A/S/Registry/index.html b/dev/sidekick/Sidekick_arith_lia/module-type-S/A/S/Registry/index.html
deleted file mode 100644
index 75144380..00000000
--- a/dev/sidekick/Sidekick_arith_lia/module-type-S/A/S/Registry/index.html
+++ /dev/null
@@ -1,2 +0,0 @@
-
-Registry (sidekick.Sidekick_arith_lia.S.A.S.Registry) Module S.Registry
val create_key : unit -> 'a keyCall this statically, typically at program initialization, for each distinct key.
val create : unit -> t
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_arith_lia/module-type-S/A/S/Solver_internal/CC/Actions/P/Step_vec/index.html b/dev/sidekick/Sidekick_arith_lia/module-type-S/A/S/Solver_internal/CC/Actions/P/Step_vec/index.html
deleted file mode 100644
index 0fbfaf63..00000000
--- a/dev/sidekick/Sidekick_arith_lia/module-type-S/A/S/Solver_internal/CC/Actions/P/Step_vec/index.html
+++ /dev/null
@@ -1,2 +0,0 @@
-
-Step_vec (sidekick.Sidekick_arith_lia.S.A.S.Solver_internal.CC.Actions.P.Step_vec) Module P.Step_vec
A vector of steps
include Sidekick_util.Vec_sig.BASE with type elt = proof_step
include Sidekick_util.Vec_sig.BASE_RO with type elt = proof_step
type elt = proof_stepval size : t -> intval create : ?cap:int -> unit -> tval clear : t -> unitval is_empty : t -> boolval fast_remove : t -> int -> unitRemove element at index i without preserving order (swap with last element)
val ensure_size : t -> int -> unitval shrink : t -> int -> unit
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_arith_lia/module-type-S/A/S/Solver_internal/CC/Actions/P/index.html b/dev/sidekick/Sidekick_arith_lia/module-type-S/A/S/Solver_internal/CC/Actions/P/index.html
deleted file mode 100644
index b1916fc7..00000000
--- a/dev/sidekick/Sidekick_arith_lia/module-type-S/A/S/Solver_internal/CC/Actions/P/index.html
+++ /dev/null
@@ -1,10 +0,0 @@
-
-P (sidekick.Sidekick_arith_lia.S.A.S.Solver_internal.CC.Actions.P) Module Actions.P
type t = proofThe abstract representation of a proof. A proof always proves a clause to be valid (true in every possible interpretation of the problem's assertions, and the theories)
type proof_step = proof_stepIdentifier for a proof proof_rule (like a unique ID for a clause previously added/proved)
type term = T.Term.ttype lit = Lit.ttype proof_rule = t -> proof_stepinclude Sidekick_core.SAT_PROOF
- with type t := t
- and type lit := lit
- and type proof_step := proof_step
- and type proof_rule := proof_rule
module Step_vec : Sidekick_util.Vec_sig.S with type elt = proof_stepA vector of steps
val enabled : t -> boolReturns true if proof production is enabled
val emit_input_clause : lit Iter.t -> proof_ruleEmit an input clause.
val emit_redundant_clause : lit Iter.t -> hyps:proof_step Iter.t -> proof_ruleEmit a clause deduced by the SAT solver, redundant wrt previous clauses. The clause must be RUP wrt hyps.
val emit_unsat_core : lit Iter.t -> proof_ruleProduce a proof of the empty clause given this subset of the assumptions. FIXME: probably needs the list of proof_step that disprove the lits?
val emit_unsat : proof_step -> t -> unitSignal "unsat" result at the given proof
val del_clause : proof_step -> lit Iter.t -> t -> unitForget a clause. Only useful for performance considerations.
val lemma_cc : lit Iter.t -> proof_rulelemma_cc proof lits asserts that lits form a tautology for the theory of uninterpreted functions.
val define_term : term -> term -> proof_ruledefine_term cst u proof defines the new constant cst as being equal to u. The result is a proof of the clause cst = u
val proof_p1 : proof_step -> proof_step -> proof_ruleproof_p1 p1 p2, where p1 proves the unit clause t=u (t:bool) and p2 proves C \/ t, is the rule that produces C \/ u, i.e unit paramodulation.
val proof_r1 : proof_step -> proof_step -> proof_ruleproof_r1 p1 p2, where p1 proves the unit clause |- t (t:bool) and p2 proves C \/ ¬t, is the rule that produces C \/ u, i.e unit resolution.
val proof_res : pivot:term -> proof_step -> proof_step -> proof_ruleproof_res ~pivot p1 p2, where p1 proves the clause |- C \/ l and p2 proves D \/ ¬l, where l is either pivot or ¬pivot, is the rule that produces C \/ D, i.e boolean resolution.
val with_defs : proof_step -> proof_step Iter.t -> proof_rulewith_defs pr defs specifies that pr is valid only in a context where the definitions defs are present.
val lemma_true : term -> proof_rulelemma_true (true) p asserts the clause (true)
val lemma_preprocess : term -> term -> using:proof_step Iter.t -> proof_rulelemma_preprocess t u ~using p asserts that t = u is a tautology and that t has been preprocessed into u.
The theorem /\_{eqn in using} eqn |- t=u is proved using congruence closure, and then resolved against the clauses using to obtain a unit equality.
From now on, t and u will be used interchangeably.
val lemma_rw_clause :
- proof_step ->
- res:lit Iter.t ->
- using:proof_step Iter.t ->
- proof_rulelemma_rw_clause prc ~res ~using, where prc is the proof of |- c, uses the equations |- p_i = q_i from using to rewrite some literals of c into res. This is used to preprocess literals of a clause (using lemma_preprocess individually).
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_arith_lia/module-type-S/A/S/Solver_internal/CC/Actions/index.html b/dev/sidekick/Sidekick_arith_lia/module-type-S/A/S/Solver_internal/CC/Actions/index.html
deleted file mode 100644
index aa152101..00000000
--- a/dev/sidekick/Sidekick_arith_lia/module-type-S/A/S/Solver_internal/CC/Actions/index.html
+++ /dev/null
@@ -1,15 +0,0 @@
-
-Actions (sidekick.Sidekick_arith_lia.S.A.S.Solver_internal.CC.Actions) Module CC.Actions
module T = Tmodule Lit = Littype proof = prooftype proof_step = proof_stepmodule P :
- Sidekick_core.PROOF
- with type lit = Lit.t
- and type t = proof
- and type term = T.Term.t
- and type proof_step = proof_steptype t = theory_actionsAn action handle. It is used by the congruence closure to perform the actions below. How it performs the actions is not specified and is solver-specific.
val raise_conflict : t -> Lit.t list -> proof_step -> 'araise_conflict acts c pr declares that c is a tautology of the theory of congruence. This does not return (it should raise an exception).
raise_semantic_conflict acts lits same_val declares that the conjunction of all lits (literals true in current trail) and tuples {=,≠}, t_i, u_i implies false.
The {=,≠}, t_i, u_i are pairs of terms with the same value (if = / true) or distinct value (if ≠ / false)) in the current model.
This does not return. It should raise an exception.
val propagate :
- t ->
- Lit.t ->
- reason:( unit -> Lit.t list * proof_step ) ->
- unitpropagate acts lit ~reason pr declares that reason() => lit is a tautology.
reason() should return a list of literals that are currently true.lit should be a literal of interest (see CC_S.set_as_lit).
This function might never be called, a congruence closure has the right to not propagate and only trigger conflicts.
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_arith_lia/module-type-S/A/S/Solver_internal/CC/Expl/index.html b/dev/sidekick/Sidekick_arith_lia/module-type-S/A/S/Solver_internal/CC/Expl/index.html
deleted file mode 100644
index 63005105..00000000
--- a/dev/sidekick/Sidekick_arith_lia/module-type-S/A/S/Solver_internal/CC/Expl/index.html
+++ /dev/null
@@ -1,2 +0,0 @@
-
-Expl (sidekick.Sidekick_arith_lia.S.A.S.Solver_internal.CC.Expl) Module CC.Expl
Explanations
Explanations are specialized proofs, created by the congruence closure when asked to justify why 2 terms are equal.
val pp : t Sidekick_core.Fmt.printerExplanation: we merged t and u because of literal t=u, or we merged t and true because of literal t, or t and false because of literal ¬t
mk_theory t u expl_sets pr builds a theory explanation for why |- t=u. It depends on sub-explanations expl_sets which are tuples (t_i, u_i, expls_i) where expls_i are explanations that justify t_i = u_i in the current congruence closure.
The proof pr is the theory lemma, of the form (t_i = u_i)_i |- t=u . It is resolved against each expls_i |- t_i=u_i obtained from expl_sets, on pivot t_i=u_i, to obtain a proof of Gamma |- t=u where Gamma is a subset of the literals asserted into the congruence closure.
For example for the lemma a=b deduced by injectivity from Some a=Some b in the theory of datatypes, the arguments would be a, b, [Some a, Some b, mk_merge_t (Some a)(Some b)], pr where pr is the injectivity lemma Some a=Some b |- a=b.
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_arith_lia/module-type-S/A/S/Solver_internal/CC/N/index.html b/dev/sidekick/Sidekick_arith_lia/module-type-S/A/S/Solver_internal/CC/N/index.html
deleted file mode 100644
index cdf3860e..00000000
--- a/dev/sidekick/Sidekick_arith_lia/module-type-S/A/S/Solver_internal/CC/N/index.html
+++ /dev/null
@@ -1,2 +0,0 @@
-
-N (sidekick.Sidekick_arith_lia.S.A.S.Solver_internal.CC.N) Module CC.N
Equivalence classes.
An equivalence class is a set of terms that are currently equal in the partial model built by the solver. The class is represented by a collection of nodes, one of which is distinguished and is called the "representative".
All information pertaining to the whole equivalence class is stored in this representative's node.
When two classes become equal (are "merged"), one of the two representatives is picked as the representative of the new class. The new class contains the union of the two old classes' nodes.
We also allow theories to store additional information in the representative. This information can be used when two classes are merged, to detect conflicts and solve equations à la Shostak.
An equivalent class, containing terms that are proved to be equal.
A value of type t points to a particular term, but see find to get the representative of the class.
Term contained in this equivalence class. If is_root n, then term n is the class' representative term.
Are two classes physically equal? To check for logical equality, use CC.N.equal (CC.find cc n1) (CC.find cc n2) which checks for equality of representatives.
val hash : t -> intAn opaque hash of this node.
val pp : t Sidekick_core.Fmt.printerUnspecified printing of the node, for example its term, a unique ID, etc.
val is_root : t -> boolIs the node a root (ie the representative of its class)? See find to get the root.
Traverse the congruence class. Precondition: is_root n (see find below)
Traverse the parents of the class. Precondition: is_root n (see find below)
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_arith_lia/module-type-S/A/S/Solver_internal/CC/P/Step_vec/index.html b/dev/sidekick/Sidekick_arith_lia/module-type-S/A/S/Solver_internal/CC/P/Step_vec/index.html
deleted file mode 100644
index ec479c03..00000000
--- a/dev/sidekick/Sidekick_arith_lia/module-type-S/A/S/Solver_internal/CC/P/Step_vec/index.html
+++ /dev/null
@@ -1,2 +0,0 @@
-
-Step_vec (sidekick.Sidekick_arith_lia.S.A.S.Solver_internal.CC.P.Step_vec) Module P.Step_vec
A vector of steps
include Sidekick_util.Vec_sig.BASE with type elt = proof_step
include Sidekick_util.Vec_sig.BASE_RO with type elt = proof_step
type elt = proof_stepval size : t -> intval create : ?cap:int -> unit -> tval clear : t -> unitval is_empty : t -> boolval fast_remove : t -> int -> unitRemove element at index i without preserving order (swap with last element)
val ensure_size : t -> int -> unitval shrink : t -> int -> unit
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_arith_lia/module-type-S/A/S/Solver_internal/CC/P/index.html b/dev/sidekick/Sidekick_arith_lia/module-type-S/A/S/Solver_internal/CC/P/index.html
deleted file mode 100644
index dbda9244..00000000
--- a/dev/sidekick/Sidekick_arith_lia/module-type-S/A/S/Solver_internal/CC/P/index.html
+++ /dev/null
@@ -1,10 +0,0 @@
-
-P (sidekick.Sidekick_arith_lia.S.A.S.Solver_internal.CC.P) Module CC.P
type t = proofThe abstract representation of a proof. A proof always proves a clause to be valid (true in every possible interpretation of the problem's assertions, and the theories)
type proof_step = proof_stepIdentifier for a proof proof_rule (like a unique ID for a clause previously added/proved)
type lit = littype proof_rule = t -> proof_stepinclude Sidekick_core.SAT_PROOF
- with type t := t
- and type lit := lit
- and type proof_step := proof_step
- and type proof_rule := proof_rule
module Step_vec : Sidekick_util.Vec_sig.S with type elt = proof_stepA vector of steps
val enabled : t -> boolReturns true if proof production is enabled
val emit_input_clause : lit Iter.t -> proof_ruleEmit an input clause.
val emit_redundant_clause : lit Iter.t -> hyps:proof_step Iter.t -> proof_ruleEmit a clause deduced by the SAT solver, redundant wrt previous clauses. The clause must be RUP wrt hyps.
val emit_unsat_core : lit Iter.t -> proof_ruleProduce a proof of the empty clause given this subset of the assumptions. FIXME: probably needs the list of proof_step that disprove the lits?
val emit_unsat : proof_step -> t -> unitSignal "unsat" result at the given proof
val del_clause : proof_step -> lit Iter.t -> t -> unitForget a clause. Only useful for performance considerations.
val lemma_cc : lit Iter.t -> proof_rulelemma_cc proof lits asserts that lits form a tautology for the theory of uninterpreted functions.
val define_term : term -> term -> proof_ruledefine_term cst u proof defines the new constant cst as being equal to u. The result is a proof of the clause cst = u
val proof_p1 : proof_step -> proof_step -> proof_ruleproof_p1 p1 p2, where p1 proves the unit clause t=u (t:bool) and p2 proves C \/ t, is the rule that produces C \/ u, i.e unit paramodulation.
val proof_r1 : proof_step -> proof_step -> proof_ruleproof_r1 p1 p2, where p1 proves the unit clause |- t (t:bool) and p2 proves C \/ ¬t, is the rule that produces C \/ u, i.e unit resolution.
val proof_res : pivot:term -> proof_step -> proof_step -> proof_ruleproof_res ~pivot p1 p2, where p1 proves the clause |- C \/ l and p2 proves D \/ ¬l, where l is either pivot or ¬pivot, is the rule that produces C \/ D, i.e boolean resolution.
val with_defs : proof_step -> proof_step Iter.t -> proof_rulewith_defs pr defs specifies that pr is valid only in a context where the definitions defs are present.
val lemma_true : term -> proof_rulelemma_true (true) p asserts the clause (true)
val lemma_preprocess : term -> term -> using:proof_step Iter.t -> proof_rulelemma_preprocess t u ~using p asserts that t = u is a tautology and that t has been preprocessed into u.
The theorem /\_{eqn in using} eqn |- t=u is proved using congruence closure, and then resolved against the clauses using to obtain a unit equality.
From now on, t and u will be used interchangeably.
val lemma_rw_clause :
- proof_step ->
- res:lit Iter.t ->
- using:proof_step Iter.t ->
- proof_rulelemma_rw_clause prc ~res ~using, where prc is the proof of |- c, uses the equations |- p_i = q_i from using to rewrite some literals of c into res. This is used to preprocess literals of a clause (using lemma_preprocess individually).
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_arith_lia/module-type-S/A/S/Solver_internal/CC/Resolved_expl/index.html b/dev/sidekick/Sidekick_arith_lia/module-type-S/A/S/Solver_internal/CC/Resolved_expl/index.html
deleted file mode 100644
index 756cb973..00000000
--- a/dev/sidekick/Sidekick_arith_lia/module-type-S/A/S/Solver_internal/CC/Resolved_expl/index.html
+++ /dev/null
@@ -1,2 +0,0 @@
-
-Resolved_expl (sidekick.Sidekick_arith_lia.S.A.S.Solver_internal.CC.Resolved_expl) Module CC.Resolved_expl
Resolved explanations.
The congruence closure keeps explanations for why terms are in the same class. However these are represented in a compact, cheap form. To use these explanations we need to resolve them into a resolved explanation, typically a list of literals that are true in the current trail and are responsible for merges.
However, we can also have merged classes because they have the same value in the current model.
val is_semantic : t -> boolis_semantic expl is true if there's at least one pair in expl.same_value.
val pp : t Sidekick_core.Fmt.printer
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_arith_lia/module-type-S/A/S/Solver_internal/CC/index.html b/dev/sidekick/Sidekick_arith_lia/module-type-S/A/S/Solver_internal/CC/index.html
deleted file mode 100644
index 3c7b2aa7..00000000
--- a/dev/sidekick/Sidekick_arith_lia/module-type-S/A/S/Solver_internal/CC/index.html
+++ /dev/null
@@ -1,25 +0,0 @@
-
-CC (sidekick.Sidekick_arith_lia.S.A.S.Solver_internal.CC) Module Solver_internal.CC
Congruence closure instance
first, some aliases.
module T = Tmodule Lit = Littype proof = prooftype proof_step = proof_stepmodule P :
- Sidekick_core.PROOF
- with type lit = Lit.t
- and type t = proof
- and type proof_step = proof_step
- with type t = proof
- with type lit = litmodule Actions :
- Sidekick_core.CC_ACTIONS
- with module T = T
- and module Lit = Lit
- and type proof = proof
- and type proof_step = proof_step
- with type t = theory_actionstype term_store = T.Term.storetype term = T.Term.ttype value = termtype fun_ = T.Fun.ttype lit = Lit.ttype actions = Actions.tThe congruence closure object. It contains a fair amount of state and is mutable and backtrackable.
module N : sig ... endEquivalence classes.
module Expl : sig ... endExplanations
module Resolved_expl : sig ... endResolved explanations.
type node = N.tA node of the congruence closure
type repr = N.tNode that is currently a representative
type explanation = Expl.tAccessors
val term_store : t -> term_storeAdd the term to the congruence closure, if not present already. Will be backtracked.
Returns true if the term is explicitly present in the congruence closure
Events
Events triggered by the congruence closure, to which other plugins can subscribe.
ev_on_pre_merge cc acts n1 n2 expl is called right before n1 and n2 are merged with explanation expl.
ev_on_post_merge cc acts n1 n2 is called right after n1 and n2 were merged. find cc n1 and find cc n2 will return the same node.
ev_on_new_term cc n t is called whenever a new term t is added to the congruence closure. Its node is n.
ev_on_conflict acts ~th c is called when the congruence closure triggers a conflict by asserting the tautology c.
type ev_on_propagate = t -> lit -> ( unit -> lit list * proof_step ) -> unitev_on_propagate cc lit reason is called whenever reason() => lit is a propagated lemma. See CC_ACTIONS.propagate.
ev_on_is_subterm n t is called when n is a subterm of another node for the first time. t is the term corresponding to the node n. This can be useful for theory combination.
val create :
- ?stat:Sidekick_util.Stat.t ->
- ?on_pre_merge:ev_on_pre_merge list ->
- ?on_post_merge:ev_on_post_merge list ->
- ?on_new_term:ev_on_new_term list ->
- ?on_conflict:ev_on_conflict list ->
- ?on_propagate:ev_on_propagate list ->
- ?on_is_subterm:ev_on_is_subterm list ->
- ?size:[ `Small | `Big ] ->
- term_store ->
- proof ->
- tCreate a new congruence closure.
val allocate_bitfield : descr:string -> t -> N.bitfieldAllocate a new node field (see N.bitfield).
This field descriptor is henceforth reserved for all nodes in this congruence closure, and can be set using set_bitfield for each node individually. This can be used to efficiently store some metadata on nodes (e.g. "is there a numeric value in the class" or "is there a constructor term in the class").
There may be restrictions on how many distinct fields are allocated for a given congruence closure (e.g. at most Sys.int_size fields).
val get_bitfield : t -> N.bitfield -> N.t -> boolAccess the bit field of the given node
val set_bitfield : t -> N.bitfield -> bool -> N.t -> unitSet the bitfield for the node. This will be backtracked. See N.bitfield.
val on_pre_merge : t -> ev_on_pre_merge -> unitAdd a function to be called when two classes are merged
val on_post_merge : t -> ev_on_post_merge -> unitAdd a function to be called when two classes are merged
val on_new_term : t -> ev_on_new_term -> unitAdd a function to be called when a new node is created
val on_conflict : t -> ev_on_conflict -> unitCalled when the congruence closure finds a conflict
val on_propagate : t -> ev_on_propagate -> unitCalled when the congruence closure propagates a literal
val on_is_subterm : t -> ev_on_is_subterm -> unitCalled on terms that are subterms of function symbols
All current classes. This is costly, only use if there is no other solution
Given a literal, assume it in the congruence closure and propagate its consequences. Will be backtracked.
Useful for the theory combination or the SAT solver's functor
val explain_eq : t -> N.t -> N.t -> Resolved_expl.tExplain why the two nodes are equal. Fails if they are not, in an unspecified way.
Raise a conflict with the given explanation. It must be a theory tautology that expl ==> absurd. To be used in theories.
This fails in an unspecified way if the explanation, once resolved, satisfies Resolved_expl.is_semantic.
Merge these two nodes given this explanation. It must be a theory tautology that expl ==> n1 = n2. To be used in theories.
val with_model_mode : t -> ( unit -> 'a ) -> 'aEnter model combination mode.
In model combination mode, obtain classes with their values.
Perform all pending operations done via assert_eq, assert_lit, etc. Will use the actions to propagate literals, declare conflicts, etc.
val push_level : t -> unitPush backtracking level
val pop_levels : t -> int -> unitRestore to state n calls to push_level earlier. Used during backtracking.
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_arith_lia/module-type-S/A/S/Solver_internal/Registry/index.html b/dev/sidekick/Sidekick_arith_lia/module-type-S/A/S/Solver_internal/Registry/index.html
deleted file mode 100644
index 545672c8..00000000
--- a/dev/sidekick/Sidekick_arith_lia/module-type-S/A/S/Solver_internal/Registry/index.html
+++ /dev/null
@@ -1,2 +0,0 @@
-
-Registry (sidekick.Sidekick_arith_lia.S.A.S.Solver_internal.Registry) Module Solver_internal.Registry
val create_key : unit -> 'a keyCall this statically, typically at program initialization, for each distinct key.
val create : unit -> t
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_arith_lia/module-type-S/A/S/Solver_internal/Simplify/index.html b/dev/sidekick/Sidekick_arith_lia/module-type-S/A/S/Solver_internal/Simplify/index.html
deleted file mode 100644
index af4fbf1e..00000000
--- a/dev/sidekick/Sidekick_arith_lia/module-type-S/A/S/Solver_internal/Simplify/index.html
+++ /dev/null
@@ -1,2 +0,0 @@
-
-Simplify (sidekick.Sidekick_arith_lia.S.A.S.Solver_internal.Simplify) Module Solver_internal.Simplify
Simplify terms
val tst : t -> term_storeval clear : t -> unitReset internal cache, etc.
type hook = t -> term -> (term * proof_step Iter.t) optionGiven a term, try to simplify it. Return None if it didn't change.
A simple example could be a hook that takes a term t, and if t is app "+" (const x) (const y) where x and y are number, returns Some (const (x+y)), and None otherwise.
The simplifier will take care of simplifying the resulting term further, caching (so that work is not duplicated in subterms), etc.
val normalize : t -> term -> (term * proof_step) optionNormalize a term using all the hooks. This performs a fixpoint, i.e. it only stops when no hook applies anywhere inside the term.
val normalize_t : t -> term -> term * proof_step optionNormalize a term using all the hooks, along with a proof that the simplification is correct. returns t, ø if no simplification occurred.
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_arith_lia/module-type-S/A/S/Solver_internal/index.html b/dev/sidekick/Sidekick_arith_lia/module-type-S/A/S/Solver_internal/index.html
deleted file mode 100644
index f0dae0dc..00000000
--- a/dev/sidekick/Sidekick_arith_lia/module-type-S/A/S/Solver_internal/index.html
+++ /dev/null
@@ -1,43 +0,0 @@
-
-Solver_internal (sidekick.Sidekick_arith_lia.S.A.S.Solver_internal) Module S.Solver_internal
Internal solver, available to theories.
module T = Tmodule Lit = Littype ty = T.Ty.ttype term = T.Term.ttype value = T.Term.ttype term_store = T.Term.storetype ty_store = T.Ty.storetype proof = prooftype proof_step = proof_stepmodule P = Ptype solver = tval tst : t -> term_storeval stats : t -> Sidekick_util.Stat.tRegistry
module Registry : Sidekick_core.REGISTRYval registry : t -> Registry.tA solver contains a registry so that theories can share data
Actions for the theories
type lit = Lit.tCongruence Closure
module CC :
- Sidekick_core.CC_S
- with module T = T
- and module Lit = Lit
- and type proof = proof
- and type proof_step = proof_step
- and type P.t = proof
- and type P.lit = lit
- and type Actions.t = theory_actionsCongruence closure instance
Simplifiers
module Simplify : sig ... endSimplify terms
type simplify_hook = Simplify.hookval add_simplifier : t -> Simplify.hook -> unitAdd a simplifier hook for preprocessing.
val simplify_t : t -> term -> (term * proof_step) optionSimplify input term, returns Some u if some simplification occurred.
val simp_t : t -> term -> term * proof_step optionsimp_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.
module type PREPROCESS_ACTS = sig ... endtype preprocess_actions = (module PREPROCESS_ACTS)Actions available to the preprocessor
type preprocess_hook = t -> preprocess_actions -> term -> unitGiven a term, preprocess it.
The idea is to add literals and clauses to help define the meaning of the term, if needed. For example for boolean formulas, clauses for their Tseitin encoding can be added, with the formula acting as its own proxy symbol.
val on_preprocess : t -> preprocess_hook -> unitAdd a hook that will be called when terms are preprocessed
hooks for the theory
val raise_conflict : t -> theory_actions -> lit list -> proof_step -> 'aGive a conflict clause to the solver
val push_decision : t -> theory_actions -> lit -> unitAsk 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.
val propagate :
- t ->
- theory_actions ->
- lit ->
- reason:( unit -> lit list * proof_step ) ->
- unitPropagate a boolean using a unit clause. expl => lit must be a theory lemma, that is, a T-tautology
val propagate_l : t -> theory_actions -> lit -> lit list -> proof_step -> unitPropagate a boolean using a unit clause. expl => lit must be a theory lemma, that is, a T-tautology
val add_clause_temp : t -> theory_actions -> lit list -> proof_step -> unitAdd local clause to the SAT solver. This clause will be removed when the solver backtracks.
val add_clause_permanent :
- t ->
- theory_actions ->
- lit list ->
- proof_step ->
- unitAdd toplevel clause to the SAT solver. This clause will not be backtracked.
val mk_lit : t -> theory_actions -> ?sign:bool -> term -> litCreate a literal. This automatically preprocesses the term.
val add_lit : t -> theory_actions -> ?default_pol:bool -> lit -> unitAdd the given literal to the SAT solver, so it gets assigned a boolean value.
val add_lit_t : t -> theory_actions -> ?sign:bool -> term -> unitAdd the given (signed) bool term to the SAT solver, so it gets assigned a boolean value
val cc_raise_conflict_expl : t -> theory_actions -> CC.Expl.t -> 'aRaise a conflict with the given congruence closure explanation. it must be a theory tautology that expl ==> absurd. To be used in theories.
val cc_merge : t -> theory_actions -> CC.N.t -> CC.N.t -> CC.Expl.t -> unitMerge these two nodes in the congruence closure, given this explanation. It must be a theory tautology that expl ==> n1 = n2. To be used in theories.
val cc_merge_t : t -> theory_actions -> term -> term -> CC.Expl.t -> unitMerge these two terms in the congruence closure, given this explanation. See cc_merge
Add/retrieve congruence closure node for this term. To be used in theories
Return true if the term is explicitly in the congruence closure. To be used in theories
val on_cc_pre_merge :
- t ->
- ( CC.t -> theory_actions -> CC.N.t -> CC.N.t -> CC.Expl.t -> unit ) ->
- unitCallback for when two classes containing data for this key are merged (called before)
val on_cc_post_merge :
- t ->
- ( CC.t -> theory_actions -> CC.N.t -> CC.N.t -> unit ) ->
- unitCallback for when two classes containing data for this key are merged (called after)
Callback to add data on terms when they are added to the congruence closure
Callback for when a term is a subterm of another term in the congruence closure
Callback called on every CC conflict
val on_cc_propagate :
- t ->
- ( CC.t -> lit -> ( unit -> lit list * proof_step ) -> unit ) ->
- unitCallback called on every CC propagation
val on_partial_check :
- t ->
- ( t -> theory_actions -> lit Iter.t -> unit ) ->
- unitRegister 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.
val on_final_check : t -> ( t -> theory_actions -> lit Iter.t -> unit ) -> unitRegister callback to be called during the final check.
Must be complete (i.e. must raise a conflict if the set of literals is not satisfiable) and can be expensive. The function is given the whole trail.
val on_th_combination :
- t ->
- ( t -> theory_actions -> (term * value) Iter.t ) ->
- unitAdd a hook called during theory combination. The hook must return an iterator of pairs (t, v) which mean that term t has value v in the model.
Terms with the same value (according to Term.equal) will be merged in the CC; if two terms with different values are merged, we get a semantic conflict and must pick another model.
val declare_pb_is_incomplete : t -> unitDeclare that, in some theory, the problem is outside the logic fragment that is decidable (e.g. if we meet proper NIA formulas). The solver will not reply "SAT" from now on.
Model production
A model-production hook to query values from a theory.
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.
A model production hook, for the theory to add values. The hook is given a add function to add bindings to the model.
val on_model :
- ?ask:model_ask_hook ->
- ?complete:model_completion_hook ->
- t ->
- unitAdd model production/completion hooks.
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_arith_lia/module-type-S/A/S/Solver_internal/module-type-PREPROCESS_ACTS/index.html b/dev/sidekick/Sidekick_arith_lia/module-type-S/A/S/Solver_internal/module-type-PREPROCESS_ACTS/index.html
deleted file mode 100644
index 75c1098c..00000000
--- a/dev/sidekick/Sidekick_arith_lia/module-type-S/A/S/Solver_internal/module-type-PREPROCESS_ACTS/index.html
+++ /dev/null
@@ -1,2 +0,0 @@
-
-PREPROCESS_ACTS (sidekick.Sidekick_arith_lia.S.A.S.Solver_internal.PREPROCESS_ACTS) Module type Solver_internal.PREPROCESS_ACTS
val proof : proofval add_clause : lit list -> proof_step -> unitpushes a new clause into the SAT solver.
val add_lit : ?default_pol:bool -> lit -> unitEnsure the literal will be decided/handled by the SAT solver.
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_arith_lia/module-type-S/A/S/T/Fun/index.html b/dev/sidekick/Sidekick_arith_lia/module-type-S/A/S/T/Fun/index.html
deleted file mode 100644
index 5b0e668a..00000000
--- a/dev/sidekick/Sidekick_arith_lia/module-type-S/A/S/T/Fun/index.html
+++ /dev/null
@@ -1,2 +0,0 @@
-
-Fun (sidekick.Sidekick_arith_lia.S.A.S.T.Fun) Module T.Fun
A function symbol, like "f" or "plus" or "is_human" or "socrates"
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_arith_lia/module-type-S/A/S/T/Term/index.html b/dev/sidekick/Sidekick_arith_lia/module-type-S/A/S/T/Term/index.html
deleted file mode 100644
index becdb62b..00000000
--- a/dev/sidekick/Sidekick_arith_lia/module-type-S/A/S/T/Term/index.html
+++ /dev/null
@@ -1,8 +0,0 @@
-
-Term (sidekick.Sidekick_arith_lia.S.A.S.T.Term) Module T.Term
Term structure.
Terms should be hashconsed, with perfect sharing. This allows, for example, Term.Tbl and Term.iter_dag to be efficient.
val hash : t -> intval pp : t Sidekick_core.Fmt.printerA store used to create new terms. It is where the hashconsing table should live, along with other all-terms related store.
val as_bool : t -> bool optionas_bool t is Some true if t is the term true, and similarly for false. For other terms it is None.
abs t returns an "absolute value" for the term, along with the sign of t.
The idea is that we want to turn not a into (a, false), or (a != b) into (a=b, false). For terms without a negation this should return (t, true).
The store is passed in case a new term needs to be created.
Map function on immediate subterms. This should not be recursive.
Iterate function on immediate subterms. This should not be recursive.
iter_dag t f calls f once on each subterm of t, t included. It must not traverse t as a tree, but rather as a perfectly shared DAG.
For example, in:
let x = 2 in
-let y = f x x in
-let z = g y x in
-z = z
the DAG has the following nodes:
n1: 2
-n2: f n1 n1
-n3: g n2 n1
-n4: = n3 n3
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_arith_lia/module-type-S/A/S/T/Ty/index.html b/dev/sidekick/Sidekick_arith_lia/module-type-S/A/S/T/Ty/index.html
deleted file mode 100644
index 44d37ef0..00000000
--- a/dev/sidekick/Sidekick_arith_lia/module-type-S/A/S/T/Ty/index.html
+++ /dev/null
@@ -1,2 +0,0 @@
-
-Ty (sidekick.Sidekick_arith_lia.S.A.S.T.Ty) Module T.Ty
Types
Types should be comparable (ideally, in O(1)), and have at least a boolean type available.
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_arith_lia/module-type-S/A/S/T/index.html b/dev/sidekick/Sidekick_arith_lia/module-type-S/A/S/T/index.html
deleted file mode 100644
index 24c51303..00000000
--- a/dev/sidekick/Sidekick_arith_lia/module-type-S/A/S/T/index.html
+++ /dev/null
@@ -1,2 +0,0 @@
-
-T (sidekick.Sidekick_arith_lia.S.A.S.T) Module S.T
module Fun : sig ... endA function symbol, like "f" or "plus" or "is_human" or "socrates"
module Ty : sig ... endTypes
module Term : sig ... endTerm structure.
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_arith_lia/module-type-S/A/S/Unknown/index.html b/dev/sidekick/Sidekick_arith_lia/module-type-S/A/S/Unknown/index.html
deleted file mode 100644
index 7b546ec1..00000000
--- a/dev/sidekick/Sidekick_arith_lia/module-type-S/A/S/Unknown/index.html
+++ /dev/null
@@ -1,2 +0,0 @@
-
-Unknown (sidekick.Sidekick_arith_lia.S.A.S.Unknown) Module S.Unknown
val pp : t CCFormat.printer
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_arith_lia/module-type-S/A/S/index.html b/dev/sidekick/Sidekick_arith_lia/module-type-S/A/S/index.html
deleted file mode 100644
index 61214000..00000000
--- a/dev/sidekick/Sidekick_arith_lia/module-type-S/A/S/index.html
+++ /dev/null
@@ -1,37 +0,0 @@
-
-S (sidekick.Sidekick_arith_lia.S.A.S) Module A.S
module T : Sidekick_core.TERMmodule Lit : Sidekick_core.LIT with module T = Tmodule P :
- Sidekick_core.PROOF
- with type lit = Lit.t
- and type t = proof
- and type proof_step = proof_step
- and type term = T.Term.tmodule Solver_internal :
- Sidekick_core.SOLVER_INTERNAL
- with module T = T
- and module Lit = Lit
- and type proof = proof
- and type proof_step = proof_step
- and module P = PInternal solver, available to theories.
type solver = ttype term = T.Term.ttype ty = T.Ty.ttype lit = Lit.tValue registry
module Registry : Sidekick_core.REGISTRYval registry : t -> Registry.tA solver contains a registry so that theories can share data
module type THEORY = sig ... endtype theory = (module THEORY)A theory that can be used for this particular solver.
A theory that can be used for this particular solver, with state of type 'a.
val mk_theory :
- name:string ->
- create_and_setup:( Solver_internal.t -> 'th ) ->
- ?push_level:( 'th -> unit ) ->
- ?pop_levels:( 'th -> int -> unit ) ->
- unit ->
- theoryHelper to create a theory.
module Model : sig ... endModels
module Unknown : sig ... endMain API
val stats : t -> Sidekick_util.Stat.tval tst : t -> T.Term.storeval ty_st : t -> T.Ty.storeval create :
- ?stat:Sidekick_util.Stat.t ->
- ?size:[ `Big | `Tiny | `Small ] ->
- proof:proof ->
- theories:theory list ->
- T.Term.store ->
- T.Ty.store ->
- unit ->
- tCreate a new solver.
It needs a term state and a type state to manipulate terms and types. All terms and types interacting with this solver will need to come from these exact states.
Add a theory to the solver. This should be called before any call to solve or to add_clause and the likes (otherwise the theory will have a partial view of the problem).
mk_lit_t _ ~sign t returns lit', where lit' is preprocess(lit) and lit is an internal representation of ± t.
The proof of |- lit = lit' is directly added to the solver's proof.
val add_clause : t -> lit Sidekick_util.IArray.t -> proof_step -> unitadd_clause solver cs adds a boolean clause to the solver. Subsequent calls to solve will need to satisfy this clause.
val add_clause_l : t -> lit list -> proof_step -> unitAdd a clause to the solver, given as a list.
Helper that turns each term into an atom, before adding the result to the solver as an assertion
Helper that turns the term into an atom, before adding the result to the solver as a unit clause assertion
type res = | Sat of Model.t(*Satisfiable
*) | Unsat of {unsat_core : unit -> lit Iter.t;(*Unsat core (subset of assumptions), or empty
*) unsat_proof_step : unit -> proof_step option;(*Proof step for the empty clause
*)
}(*Unsatisfiable
*) | Unknown of Unknown.t(*Unknown, obtained after a timeout, memory limit, etc.
*)
Result of solving for the current set of clauses
val solve :
- ?on_exit:( unit -> unit ) list ->
- ?check:bool ->
- ?on_progress:( t -> unit ) ->
- ?should_stop:( t -> int -> bool ) ->
- assumptions:lit list ->
- t ->
- ressolve s checks the satisfiability of the clauses added so far to s.
Last result, if any. Some operations will erase this (e.g. assert_term).
Pushes an assumption onto the assumption stack. It will remain there until it's pop'd by pop_assumptions.
val pop_assumptions : t -> int -> unitpop_assumptions solver n removes n assumptions from the stack. It removes the assumptions that were the most recently added via push_assumptions. Note that check_sat_propagations_only can call this if it meets a conflict.
type propagation_result = | PR_sat| PR_conflict of {backtracked : int;
}| PR_unsat of {unsat_core : unit -> lit Iter.t;
}
val check_sat_propagations_only :
- assumptions:lit list ->
- t ->
- propagation_resultcheck_sat_propagations_only solver uses assumptions (including the assumptions parameter, and atoms previously added via push_assumptions) and boolean+theory propagation to quickly assess satisfiability. It is not complete; calling solve is required to get an accurate result.
val pp_stats : t CCFormat.printerPrint some statistics. What it prints exactly is unspecified.
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_arith_lia/module-type-S/A/S/module-type-THEORY/index.html b/dev/sidekick/Sidekick_arith_lia/module-type-S/A/S/module-type-THEORY/index.html
deleted file mode 100644
index fb4017fc..00000000
--- a/dev/sidekick/Sidekick_arith_lia/module-type-S/A/S/module-type-THEORY/index.html
+++ /dev/null
@@ -1,2 +0,0 @@
-
-THEORY (sidekick.Sidekick_arith_lia.S.A.S.THEORY) Module type S.THEORY
A theory
Theories are abstracted over the concrete implementation of the solver, so they can work with any implementation.
Typically a theory should be a functor taking an argument containing a SOLVER_INTERNAL or even a full SOLVER, and some additional views on terms, literals, etc. that are specific to the theory (e.g. to map terms to linear expressions). The theory can then be instantiated on any kind of solver for any term representation that also satisfies the additional theory-specific requirements. Instantiated theories (ie values of type SOLVER.theory) can be added to the solver.
val create_and_setup : Solver_internal.t -> tInstantiate the theory's state for the given (internal) solver, register callbacks, create keys, etc.
Called once for every solver this theory is added to.
val push_level : t -> unitPush backtracking level. When the corresponding pop is called, the theory's state should be restored to a state equivalent to what it was just before push_level.
it does not have to be exactly the same state, it just needs to be equivalent.
val pop_levels : t -> int -> unitpop_levels theory n pops n backtracking levels, restoring theory to its state before calling push_level n times.
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_arith_lia/module-type-S/A/Z/index.html b/dev/sidekick/Sidekick_arith_lia/module-type-S/A/Z/index.html
deleted file mode 100644
index ff1a4430..00000000
--- a/dev/sidekick/Sidekick_arith_lia/module-type-S/A/Z/index.html
+++ /dev/null
@@ -1,2 +0,0 @@
-
-Z (sidekick.Sidekick_arith_lia.S.A.Z) Module A.Z
include Sidekick_arith.NUM
val zero : tval one : tval minus_one : tval sign : t -> intval of_int : int -> tinclude Sidekick_sigs.EQ with type t := t
include Sidekick_sigs.ORD with type t := t
include Sidekick_sigs.HASH with type t := t
val hash : t -> intinclude Sidekick_sigs.PRINT with type t := t
val pp : t CCFormat.printer
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_arith_lia/module-type-S/A/index.html b/dev/sidekick/Sidekick_arith_lia/module-type-S/A/index.html
deleted file mode 100644
index 29faecf7..00000000
--- a/dev/sidekick/Sidekick_arith_lia/module-type-S/A/index.html
+++ /dev/null
@@ -1,3 +0,0 @@
-
-A (sidekick.Sidekick_arith_lia.S.A) Module S.A
module S : Sidekick_core.SOLVERmodule LRA_solver :
- Sidekick_arith_lra.S with type A.Q.t = Q.t and module A.S = Stype term = S.T.Term.ttype ty = S.T.Ty.tval mk_bool : S.T.Term.store -> bool -> termval mk_to_real : S.T.Term.store -> term -> termWrap term into a to_real projector to rationals
Make a term from the given theory view
val ty_int : S.T.Term.store -> tyval mk_eq : S.T.Term.store -> term -> term -> termsyntactic equality
val has_ty_int : term -> boolDoes this term have the type Int
val lemma_lia : S.Lit.t Iter.t -> S.P.proof_ruleval lemma_relax_to_lra : S.Lit.t Iter.t -> S.P.proof_rule
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_arith_lia/module-type-S/index.html b/dev/sidekick/Sidekick_arith_lia/module-type-S/index.html
deleted file mode 100644
index 001875d5..00000000
--- a/dev/sidekick/Sidekick_arith_lia/module-type-S/index.html
+++ /dev/null
@@ -1,2 +0,0 @@
-
-S (sidekick.Sidekick_arith_lia.S) Module type Sidekick_arith_lia.S
val theory : A.S.theory
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_arith_lra/Make/SimpSolver/index.html b/dev/sidekick/Sidekick_arith_lra/Make/SimpSolver/index.html
index 35bde8e2..c1950beb 100644
--- a/dev/sidekick/Sidekick_arith_lra/Make/SimpSolver/index.html
+++ b/dev/sidekick/Sidekick_arith_lra/Make/SimpSolver/index.html
@@ -1,12 +1,11 @@
SimpSolver (sidekick.Sidekick_arith_lra.Make.SimpSolver) Module Make.SimpSolver
Simplexe
module V : Sidekick_simplex.VARmodule Z : Sidekick_simplex.INTmodule Q : Sidekick_simplex.RATIONAL with type bigint = Z.ttype num = Q.tNumbers
module Constraint : sig ... endmodule Subst : sig ... endval create : ?stat:Sidekick_util.Stat.t -> unit -> tCreate a new simplex.
val push_level : t -> unitval pop_levels : t -> int -> unitDefine a basic variable in terms of other variables. This is useful to "name" a linear expression and get back a variable that can be used in a Constraint.t
module Unsat_cert : sig ... endexception E_unsat of Unsat_cert.tval add_constraint :
- ?keep_on_backtracking:bool ->
?is_int:bool ->
on_propagate:ev_on_propagate ->
t ->
Constraint.t ->
V.lit ->
- unitAdd a constraint to the simplex.
This is removed upon backtracking by default.
val declare_bound : ?is_int:bool -> t -> Constraint.t -> V.lit -> unitDeclare that this constraint exists and map it to a literal, so we can possibly propagate it later. Unlike add_constraint this does NOT assert that the constraint is true
val declare_bound : ?is_int:bool -> t -> Constraint.t -> V.lit -> unitDeclare that this constraint exists and map it to a literal, so we can possibly propagate it later. Unlike add_constraint this does NOT assert that the constraint is true
Check the whole simplex for satisfiability.
Call check_exn and return a model or a proof of unsat. This does NOT enforce that integer variables map to integer values.
val check_branch_and_bound :
diff --git a/dev/sidekick/Sidekick_arith_lra/module-type-S/SimpSolver/index.html b/dev/sidekick/Sidekick_arith_lra/module-type-S/SimpSolver/index.html
index 6f2a1acc..07f1d200 100644
--- a/dev/sidekick/Sidekick_arith_lra/module-type-S/SimpSolver/index.html
+++ b/dev/sidekick/Sidekick_arith_lra/module-type-S/SimpSolver/index.html
@@ -1,12 +1,11 @@
SimpSolver (sidekick.Sidekick_arith_lra.S.SimpSolver) Module S.SimpSolver
Simplexe
module V : Sidekick_simplex.VARmodule Z : Sidekick_simplex.INTmodule Q : Sidekick_simplex.RATIONAL with type bigint = Z.ttype num = Q.tNumbers
module Constraint : sig ... endmodule Subst : sig ... endval create : ?stat:Sidekick_util.Stat.t -> unit -> tCreate a new simplex.
val push_level : t -> unitval pop_levels : t -> int -> unitDefine a basic variable in terms of other variables. This is useful to "name" a linear expression and get back a variable that can be used in a Constraint.t
module Unsat_cert : sig ... endexception E_unsat of Unsat_cert.tval add_constraint :
- ?keep_on_backtracking:bool ->
?is_int:bool ->
on_propagate:ev_on_propagate ->
t ->
Constraint.t ->
V.lit ->
- unitAdd a constraint to the simplex.
This is removed upon backtracking by default.
val declare_bound : ?is_int:bool -> t -> Constraint.t -> V.lit -> unitDeclare that this constraint exists and map it to a literal, so we can possibly propagate it later. Unlike add_constraint this does NOT assert that the constraint is true
val declare_bound : ?is_int:bool -> t -> Constraint.t -> V.lit -> unitDeclare that this constraint exists and map it to a literal, so we can possibly propagate it later. Unlike add_constraint this does NOT assert that the constraint is true
Check the whole simplex for satisfiability.
Call check_exn and return a model or a proof of unsat. This does NOT enforce that integer variables map to integer values.
val check_branch_and_bound :
diff --git a/dev/sidekick/Sidekick_intsolver/.dummy b/dev/sidekick/Sidekick_intsolver/.dummy
deleted file mode 100644
index e69de29b..00000000
diff --git a/dev/sidekick/Sidekick_intsolver/Make/Cert/index.html b/dev/sidekick/Sidekick_intsolver/Make/Cert/index.html
deleted file mode 100644
index b6a5393d..00000000
--- a/dev/sidekick/Sidekick_intsolver/Make/Cert/index.html
+++ /dev/null
@@ -1,2 +0,0 @@
-
-Cert (sidekick.Sidekick_intsolver.Make.Cert) Module Make.Cert
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_intsolver/Make/Model/index.html b/dev/sidekick/Sidekick_intsolver/Make/Model/index.html
deleted file mode 100644
index e9dbebe0..00000000
--- a/dev/sidekick/Sidekick_intsolver/Make/Model/index.html
+++ /dev/null
@@ -1,2 +0,0 @@
-
-Model (sidekick.Sidekick_intsolver.Make.Model) Module Make.Model
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_intsolver/Make/Op/index.html b/dev/sidekick/Sidekick_intsolver/Make/Op/index.html
deleted file mode 100644
index c40eacc6..00000000
--- a/dev/sidekick/Sidekick_intsolver/Make/Op/index.html
+++ /dev/null
@@ -1,2 +0,0 @@
-
-Op (sidekick.Sidekick_intsolver.Make.Op) Module Make.Op
val pp : t Sidekick_util.Fmt.printer
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_intsolver/Make/argument-1-A/Z/index.html b/dev/sidekick/Sidekick_intsolver/Make/argument-1-A/Z/index.html
deleted file mode 100644
index 597cdfb5..00000000
--- a/dev/sidekick/Sidekick_intsolver/Make/argument-1-A/Z/index.html
+++ /dev/null
@@ -1,2 +0,0 @@
-
-Z (sidekick.Sidekick_intsolver.Make.1-A.Z) Module 1-A.Z
include Sidekick_arith.INT
include Sidekick_arith.NUM
val zero : tval one : tval minus_one : tval sign : t -> intval of_int : int -> tinclude Sidekick_sigs.EQ with type t := t
include Sidekick_sigs.ORD with type t := t
include Sidekick_sigs.HASH with type t := t
val hash : t -> intinclude Sidekick_sigs.PRINT with type t := t
val pp : t CCFormat.printerval probab_prime : t -> bool
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_intsolver/Make/argument-1-A/index.html b/dev/sidekick/Sidekick_intsolver/Make/argument-1-A/index.html
deleted file mode 100644
index 4d5bb5ff..00000000
--- a/dev/sidekick/Sidekick_intsolver/Make/argument-1-A/index.html
+++ /dev/null
@@ -1,2 +0,0 @@
-
-A (sidekick.Sidekick_intsolver.Make.1-A) Parameter Make.1-A
module Z : Sidekick_arith.INT_FULLval pp_term : term Sidekick_util.Fmt.printerval pp_lit : lit Sidekick_util.Fmt.printer
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_intsolver/Make/index.html b/dev/sidekick/Sidekick_intsolver/Make/index.html
deleted file mode 100644
index 5c05728f..00000000
--- a/dev/sidekick/Sidekick_intsolver/Make/index.html
+++ /dev/null
@@ -1,2 +0,0 @@
-
-Make (sidekick.Sidekick_intsolver.Make) Module Sidekick_intsolver.Make
Parameters
Signature
module A = Amodule Op : sig ... endval create : unit -> tval push_level : t -> unitval pop_levels : t -> int -> unitmodule Cert : sig ... endmodule Model : sig ... endval pp_result : result Sidekick_util.Fmt.printer
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_intsolver/index.html b/dev/sidekick/Sidekick_intsolver/index.html
deleted file mode 100644
index bc80ca56..00000000
--- a/dev/sidekick/Sidekick_intsolver/index.html
+++ /dev/null
@@ -1,2 +0,0 @@
-
-Sidekick_intsolver (sidekick.Sidekick_intsolver) Module Sidekick_intsolver
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_intsolver/module-type-ARG/Z/index.html b/dev/sidekick/Sidekick_intsolver/module-type-ARG/Z/index.html
deleted file mode 100644
index 524feb0b..00000000
--- a/dev/sidekick/Sidekick_intsolver/module-type-ARG/Z/index.html
+++ /dev/null
@@ -1,2 +0,0 @@
-
-Z (sidekick.Sidekick_intsolver.ARG.Z) Module ARG.Z
include Sidekick_arith.INT
include Sidekick_arith.NUM
val zero : tval one : tval minus_one : tval sign : t -> intval of_int : int -> tinclude Sidekick_sigs.EQ with type t := t
include Sidekick_sigs.ORD with type t := t
include Sidekick_sigs.HASH with type t := t
val hash : t -> intinclude Sidekick_sigs.PRINT with type t := t
val pp : t CCFormat.printerval probab_prime : t -> bool
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_intsolver/module-type-ARG/index.html b/dev/sidekick/Sidekick_intsolver/module-type-ARG/index.html
deleted file mode 100644
index 81bddd6e..00000000
--- a/dev/sidekick/Sidekick_intsolver/module-type-ARG/index.html
+++ /dev/null
@@ -1,2 +0,0 @@
-
-ARG (sidekick.Sidekick_intsolver.ARG) Module type Sidekick_intsolver.ARG
module Z : Sidekick_arith.INT_FULLval pp_term : term Sidekick_util.Fmt.printerval pp_lit : lit Sidekick_util.Fmt.printer
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_intsolver/module-type-S/A/Z/index.html b/dev/sidekick/Sidekick_intsolver/module-type-S/A/Z/index.html
deleted file mode 100644
index 1c759435..00000000
--- a/dev/sidekick/Sidekick_intsolver/module-type-S/A/Z/index.html
+++ /dev/null
@@ -1,2 +0,0 @@
-
-Z (sidekick.Sidekick_intsolver.S.A.Z) Module A.Z
include Sidekick_arith.INT
include Sidekick_arith.NUM
val zero : tval one : tval minus_one : tval sign : t -> intval of_int : int -> tinclude Sidekick_sigs.EQ with type t := t
include Sidekick_sigs.ORD with type t := t
include Sidekick_sigs.HASH with type t := t
val hash : t -> intinclude Sidekick_sigs.PRINT with type t := t
val pp : t CCFormat.printerval probab_prime : t -> bool
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_intsolver/module-type-S/A/index.html b/dev/sidekick/Sidekick_intsolver/module-type-S/A/index.html
deleted file mode 100644
index f5583407..00000000
--- a/dev/sidekick/Sidekick_intsolver/module-type-S/A/index.html
+++ /dev/null
@@ -1,2 +0,0 @@
-
-A (sidekick.Sidekick_intsolver.S.A) Module S.A
module Z : Sidekick_arith.INT_FULLval pp_term : term Sidekick_util.Fmt.printerval pp_lit : lit Sidekick_util.Fmt.printer
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_intsolver/module-type-S/Cert/index.html b/dev/sidekick/Sidekick_intsolver/module-type-S/Cert/index.html
deleted file mode 100644
index e052f156..00000000
--- a/dev/sidekick/Sidekick_intsolver/module-type-S/Cert/index.html
+++ /dev/null
@@ -1,2 +0,0 @@
-
-Cert (sidekick.Sidekick_intsolver.S.Cert) Module S.Cert
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_intsolver/module-type-S/Model/index.html b/dev/sidekick/Sidekick_intsolver/module-type-S/Model/index.html
deleted file mode 100644
index 7c394701..00000000
--- a/dev/sidekick/Sidekick_intsolver/module-type-S/Model/index.html
+++ /dev/null
@@ -1,2 +0,0 @@
-
-Model (sidekick.Sidekick_intsolver.S.Model) Module S.Model
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_intsolver/module-type-S/Op/index.html b/dev/sidekick/Sidekick_intsolver/module-type-S/Op/index.html
deleted file mode 100644
index 0777b82f..00000000
--- a/dev/sidekick/Sidekick_intsolver/module-type-S/Op/index.html
+++ /dev/null
@@ -1,2 +0,0 @@
-
-Op (sidekick.Sidekick_intsolver.S.Op) Module S.Op
val pp : t Sidekick_util.Fmt.printer
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_intsolver/module-type-S/index.html b/dev/sidekick/Sidekick_intsolver/module-type-S/index.html
deleted file mode 100644
index e5a149e8..00000000
--- a/dev/sidekick/Sidekick_intsolver/module-type-S/index.html
+++ /dev/null
@@ -1,2 +0,0 @@
-
-S (sidekick.Sidekick_intsolver.S) Module type Sidekick_intsolver.S
module Op : sig ... endval create : unit -> tval push_level : t -> unitval pop_levels : t -> int -> unitmodule Cert : sig ... endmodule Model : sig ... endval pp_result : result Sidekick_util.Fmt.printer
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_simplex/Make/index.html b/dev/sidekick/Sidekick_simplex/Make/index.html
index d2b922f1..e5e11f79 100644
--- a/dev/sidekick/Sidekick_simplex/Make/index.html
+++ b/dev/sidekick/Sidekick_simplex/Make/index.html
@@ -1,12 +1,11 @@
Make (sidekick.Sidekick_simplex.Make) Module Sidekick_simplex.Make
Parameters
Signature
module V = Arg.Varmodule Z = Arg.Zmodule Q = Arg.Qtype num = Q.tNumbers
module Constraint : sig ... endmodule Subst : sig ... endval create : ?stat:Sidekick_util.Stat.t -> unit -> tCreate a new simplex.
val push_level : t -> unitval pop_levels : t -> int -> unitDefine a basic variable in terms of other variables. This is useful to "name" a linear expression and get back a variable that can be used in a Constraint.t
module Unsat_cert : sig ... endexception E_unsat of Unsat_cert.tval add_constraint :
- ?keep_on_backtracking:bool ->
?is_int:bool ->
on_propagate:ev_on_propagate ->
t ->
Constraint.t ->
V.lit ->
- unitAdd a constraint to the simplex.
This is removed upon backtracking by default.
val declare_bound : ?is_int:bool -> t -> Constraint.t -> V.lit -> unitDeclare that this constraint exists and map it to a literal, so we can possibly propagate it later. Unlike add_constraint this does NOT assert that the constraint is true
val declare_bound : ?is_int:bool -> t -> Constraint.t -> V.lit -> unitDeclare that this constraint exists and map it to a literal, so we can possibly propagate it later. Unlike add_constraint this does NOT assert that the constraint is true
Check the whole simplex for satisfiability.
Call check_exn and return a model or a proof of unsat. This does NOT enforce that integer variables map to integer values.
val check_branch_and_bound :
diff --git a/dev/sidekick/Sidekick_simplex/module-type-S/index.html b/dev/sidekick/Sidekick_simplex/module-type-S/index.html
index 6baf8091..2db7cea2 100644
--- a/dev/sidekick/Sidekick_simplex/module-type-S/index.html
+++ b/dev/sidekick/Sidekick_simplex/module-type-S/index.html
@@ -1,12 +1,11 @@
S (sidekick.Sidekick_simplex.S) Module type Sidekick_simplex.S
type num = Q.tNumbers
module Constraint : sig ... endmodule Subst : sig ... endval create : ?stat:Sidekick_util.Stat.t -> unit -> tCreate a new simplex.
val push_level : t -> unitval pop_levels : t -> int -> unitDefine a basic variable in terms of other variables. This is useful to "name" a linear expression and get back a variable that can be used in a Constraint.t
module Unsat_cert : sig ... endexception E_unsat of Unsat_cert.tval add_constraint :
- ?keep_on_backtracking:bool ->
?is_int:bool ->
on_propagate:ev_on_propagate ->
t ->
Constraint.t ->
V.lit ->
- unitAdd a constraint to the simplex.
This is removed upon backtracking by default.
val declare_bound : ?is_int:bool -> t -> Constraint.t -> V.lit -> unitDeclare that this constraint exists and map it to a literal, so we can possibly propagate it later. Unlike add_constraint this does NOT assert that the constraint is true
val declare_bound : ?is_int:bool -> t -> Constraint.t -> V.lit -> unitDeclare that this constraint exists and map it to a literal, so we can possibly propagate it later. Unlike add_constraint this does NOT assert that the constraint is true
Check the whole simplex for satisfiability.
Call check_exn and return a model or a proof of unsat. This does NOT enforce that integer variables map to integer values.
val check_branch_and_bound :
diff --git a/dev/sidekick/index.html b/dev/sidekick/index.html
index 77a01c96..288be79f 100644
--- a/dev/sidekick/index.html
+++ b/dev/sidekick/index.html
@@ -1,2 +1,2 @@
-index (sidekick.index) sidekick index
Library sidekick.arith
The entry point of this library is the module: Sidekick_arith.
Library sidekick.arith-lia
The entry point of this library is the module: Sidekick_arith_lia.
Library sidekick.arith-lra
The entry point of this library is the module: Sidekick_arith_lra.
Library sidekick.cc
The entry point of this library is the module: Sidekick_cc.
Library sidekick.core
The entry point of this library is the module: Sidekick_core.
Library sidekick.drup
The entry point of this library is the module: Sidekick_drup.
Library sidekick.intsolver
The entry point of this library is the module: Sidekick_intsolver.
Library sidekick.lit
The entry point of this library is the module: Sidekick_lit.
Library sidekick.memtrace
The entry point of this library is the module: Sidekick_memtrace.
Library sidekick.mini-cc
The entry point of this library is the module: Sidekick_mini_cc.
Library sidekick.quip
The entry point of this library is the module: Sidekick_quip.
Library sidekick.sat
The entry point of this library is the module: Sidekick_sat.
Library sidekick.sigs
The entry point of this library is the module: Sidekick_sigs.
Library sidekick.simplex
The entry point of this library is the module: Sidekick_simplex.
Library sidekick.smt-solver
The entry point of this library is the module: Sidekick_smt_solver.
Library sidekick.tef
The entry point of this library is the module: Sidekick_tef.
Library sidekick.th-bool-static
The entry point of this library is the module: Sidekick_th_bool_static.
Library sidekick.th-cstor
The entry point of this library is the module: Sidekick_th_cstor.
Library sidekick.th-data
The entry point of this library is the module: Sidekick_th_data.
Library sidekick.util
The entry point of this library is the module: Sidekick_util.
Library sidekick.zarith
The entry point of this library is the module: Sidekick_zarith.
\ No newline at end of file
+index (sidekick.index) sidekick index
Library sidekick.arith
The entry point of this library is the module: Sidekick_arith.
Library sidekick.arith-lra
The entry point of this library is the module: Sidekick_arith_lra.
Library sidekick.cc
The entry point of this library is the module: Sidekick_cc.
Library sidekick.core
The entry point of this library is the module: Sidekick_core.
Library sidekick.drup
The entry point of this library is the module: Sidekick_drup.
Library sidekick.lit
The entry point of this library is the module: Sidekick_lit.
Library sidekick.memtrace
The entry point of this library is the module: Sidekick_memtrace.
Library sidekick.mini-cc
The entry point of this library is the module: Sidekick_mini_cc.
Library sidekick.quip
The entry point of this library is the module: Sidekick_quip.
Library sidekick.sat
The entry point of this library is the module: Sidekick_sat.
Library sidekick.sigs
The entry point of this library is the module: Sidekick_sigs.
Library sidekick.simplex
The entry point of this library is the module: Sidekick_simplex.
Library sidekick.smt-solver
The entry point of this library is the module: Sidekick_smt_solver.
Library sidekick.tef
The entry point of this library is the module: Sidekick_tef.
Library sidekick.th-bool-static
The entry point of this library is the module: Sidekick_th_bool_static.
Library sidekick.th-cstor
The entry point of this library is the module: Sidekick_th_cstor.
Library sidekick.th-data
The entry point of this library is the module: Sidekick_th_data.
Library sidekick.util
The entry point of this library is the module: Sidekick_util.
Library sidekick.zarith
The entry point of this library is the module: Sidekick_zarith.
\ No newline at end of file