simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2025-12-06 03:05:31 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

wip: refactor proofs into traces

Browse source
This commit is contained in:
Simon Cruanes 2021-08-17 09:29:46 -04:00
parent 27e775ee04
commit d40ce304ae
5 changed files with 174 additions and 133 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

31
src/cc/Sidekick_cc.ml
View file

@ -15,7 +15,7 @@ module type S = Sidekick_core.CC_S
module Make (A: CC_ARG) module Make (A: CC_ARG)
: S with module T = A.T : S with module T = A.T
and module Lit = A.Lit and module Lit = A.Lit
and type lemma = A.lemma and type proof = A.proof
and module Actions = A.Actions and module Actions = A.Actions
= struct = struct
module T = A.T module T = A.T
@ -26,7 +26,8 @@ module Make (A: CC_ARG)
type term_store = T.Term.store type term_store = T.Term.store
type lit = Lit.t type lit = Lit.t
type fun_ = T.Fun.t type fun_ = T.Fun.t
type lemma = A.lemma type proof = A.proof
type dproof = proof -> unit
type actions = Actions.t type actions = Actions.t
module Term = T.Term module Term = T.Term
@ -280,7 +281,7 @@ module Make (A: CC_ARG)
and ev_on_post_merge = t -> actions -> N.t -> N.t -> unit and ev_on_post_merge = t -> actions -> N.t -> N.t -> unit
and ev_on_new_term = t -> N.t -> term -> unit and ev_on_new_term = t -> N.t -> term -> unit
and ev_on_conflict = t -> th:bool -> lit list -> unit and ev_on_conflict = t -> th:bool -> lit list -> unit
and ev_on_propagate = t -> lit -> (unit -> lit list * P.lemma) -> unit and ev_on_propagate = t -> lit -> (unit -> lit list * (proof -> unit)) -> unit
and ev_on_is_subterm = N.t -> term -> unit and ev_on_is_subterm = N.t -> term -> unit
let[@inline] size_ (r:repr) = r.n_size let[@inline] size_ (r:repr) = r.n_size
@ -307,10 +308,6 @@ module Make (A: CC_ARG)
Invariant: [in_cc t ∧ do_cc t => forall u subterm t, in_cc u] *) Invariant: [in_cc t ∧ do_cc t => forall u subterm t, in_cc u] *)
let[@inline] mem (cc:t) (t:term): bool = T_tbl.mem cc.tbl t let[@inline] mem (cc:t) (t:term): bool = T_tbl.mem cc.tbl t
let ret_cc_lemma _what (_lits:lit list) (p_lits:lit Iter.t) =
let p = P.lemma_cc p_lits in
p
(* print full state *) (* print full state *)
let pp_full out (cc:t) : unit = let pp_full out (cc:t) : unit =
let pp_next out n = let pp_next out n =
@ -661,10 +658,10 @@ module Make (A: CC_ARG)
let lits = explain_decompose_expl cc ~th [] e_ab in let lits = explain_decompose_expl cc ~th [] e_ab in
let lits = explain_equal cc ~th lits a ra in let lits = explain_equal cc ~th lits a ra in
let lits = explain_equal cc ~th lits b rb in let lits = explain_equal cc ~th lits b rb in
let proof = let emit_proof p =
let p_lits = Iter.of_list lits |> Iter.map Lit.neg in let p_lits = Iter.of_list lits |> Iter.map Lit.neg in
ret_cc_lemma "true-eq-false" lits p_lits in P.lemma_cc p p_lits in
raise_conflict_ cc ~th:!th acts (List.rev_map Lit.neg lits) proof raise_conflict_ cc ~th:!th acts (List.rev_map Lit.neg lits) emit_proof
); );
(* We will merge [r_from] into [r_into]. (* We will merge [r_from] into [r_into].
we try to ensure that [size ra <= size rb] in general, but always we try to ensure that [size ra <= size rb] in general, but always
@ -779,12 +776,12 @@ module Make (A: CC_ARG)
let e = lazy ( let e = lazy (
let lazy (th, acc) = half_expl in let lazy (th, acc) = half_expl in
let lits = explain_equal cc ~th acc u1 t1 in let lits = explain_equal cc ~th acc u1 t1 in
let p_lits = let emit_proof p =
(* make a tautology, not a true guard *) (* make a tautology, not a true guard *)
Iter.cons lit (Iter.of_list lits |> Iter.map Lit.neg) let p_lits = Iter.cons lit (Iter.of_list lits |> Iter.map Lit.neg) in
P.lemma_cc p p_lits
in in
let p = ret_cc_lemma "bool-parent" lits p_lits in lits, emit_proof
lits, p
) in ) in
fun () -> Lazy.force e fun () -> Lazy.force e
in in
@ -851,11 +848,11 @@ module Make (A: CC_ARG)
let th = ref true in let th = ref true in
let lits = explain_decompose_expl cc ~th [] expl in let lits = explain_decompose_expl cc ~th [] expl in
let lits = List.rev_map Lit.neg lits in let lits = List.rev_map Lit.neg lits in
let proof = let emit_proof p =
let p_lits = Iter.of_list lits in let p_lits = Iter.of_list lits in
ret_cc_lemma "from-expl" lits p_lits P.lemma_cc p p_lits
in in
raise_conflict_ cc ~th:!th acts lits proof raise_conflict_ cc ~th:!th acts lits emit_proof
let merge cc n1 n2 expl = let merge cc n1 n2 expl =
Log.debugf 5 Log.debugf 5

2
src/cc/Sidekick_cc.mli
View file

@ -6,5 +6,5 @@ module type S = Sidekick_core.CC_S
module Make (A: CC_ARG) module Make (A: CC_ARG)
: S with module T = A.T : S with module T = A.T
and module Lit = A.Lit and module Lit = A.Lit
and type lemma = A.lemma and type proof = A.proof
and module Actions = A.Actions and module Actions = A.Actions

109
src/core/Sidekick_core.ml
View file

@ -147,15 +147,14 @@ end
(** Proofs for the congruence closure *) (** Proofs for the congruence closure *)
module type CC_PROOF = sig module type CC_PROOF = sig
type t
type lit type lit
type lemma
val lemma_cc : lit Iter.t -> lemma val lemma_cc : t -> lit Iter.t -> unit
(** [lemma_cc proof lits] asserts that [lits] form a tautology for the theory
of uninterpreted functions. *)
end end
(* TODO: use same proofs as Sidekick_sat?
but give more precise type to [lemma]? *)
(** Proofs of unsatisfiability. (** Proofs of unsatisfiability.
We use DRUP(T)-style traces where we simply emit clauses as we go, We use DRUP(T)-style traces where we simply emit clauses as we go,
@ -167,15 +166,33 @@ module type PROOF = sig
a clause to be {b valid} (true in every possible interpretation a clause to be {b valid} (true in every possible interpretation
of the problem's assertions, and the theories) *) of the problem's assertions, and the theories) *)
type lemma type term
type lit type lit
include CC_PROOF include CC_PROOF
with type lemma := lemma with type t := t
and type lit := lit and type lit := lit
val begin_subproof : t -> unit
(** Begins a subproof. The result of this will only be the
clause with which {!end_subproof} is called; all other intermediate
steps will be discarded. *)
val end_subproof : t -> lit Iter.t -> unit
(** [end_subproof p lits] ends the current active subproof, which {b must}
prove the clause [lits] by RUP. *)
val define_term : t -> term -> term -> unit
(** [define_term p cst u] defines the new constant [cst] as being equal
to [u]. *)
val lemma_preprocess : t -> term -> term -> unit
(** [lemma_preprocess p t u] asserts that [t = u] is a tautology
and that [t] has been preprocessed into [u].
From now on, [t] and [u] will be used interchangeably. *)
val enabled : t -> bool val enabled : t -> bool
(** Is proof production enabled? *)
end end
(** Literals (** Literals
@ -222,21 +239,22 @@ module type CC_ACTIONS = sig
module T : TERM module T : TERM
module Lit : LIT with module T = T module Lit : LIT with module T = T
type lemma type proof
module P : CC_PROOF with type lit = Lit.t and type lemma = lemma type dproof = proof -> unit
module P : CC_PROOF with type lit = Lit.t and type t = proof
type t type t
(** An action handle. It is used by the congruence closure (** An action handle. It is used by the congruence closure
to perform the actions below. How it performs the actions to perform the actions below. How it performs the actions
is not specified and is solver-specific. *) is not specified and is solver-specific. *)
val raise_conflict : t -> Lit.t list -> lemma -> 'a val raise_conflict : t -> Lit.t list -> dproof -> 'a
(** [raise_conflict acts c pr] declares that [c] is a tautology of (** [raise_conflict acts c pr] declares that [c] is a tautology of
the theory of congruence. This does not return (it should raise an the theory of congruence. This does not return (it should raise an
exception). exception).
@param pr the proof of [c] being a tautology *) @param pr the proof of [c] being a tautology *)
val propagate : t -> Lit.t -> reason:(unit -> Lit.t list * lemma) -> unit val propagate : t -> Lit.t -> reason:(unit -> Lit.t list * dproof) -> unit
(** [propagate acts lit ~reason pr] declares that [reason() => lit] (** [propagate acts lit ~reason pr] declares that [reason() => lit]
is a tautology. is a tautology.
@ -251,12 +269,12 @@ end
module type CC_ARG = sig module type CC_ARG = sig
module T : TERM module T : TERM
module Lit : LIT with module T = T module Lit : LIT with module T = T
type lemma type proof
module P : CC_PROOF with type lit = Lit.t and type lemma = lemma module P : CC_PROOF with type lit = Lit.t and type t = proof
module Actions : CC_ACTIONS module Actions : CC_ACTIONS
with module T=T with module T=T
and module Lit = Lit and module Lit = Lit
and type lemma = lemma and type proof = proof
val cc_view : T.Term.t -> (T.Fun.t, T.Term.t, T.Term.t Iter.t) CC_view.t val cc_view : T.Term.t -> (T.Fun.t, T.Term.t, T.Term.t Iter.t) CC_view.t
(** View the term through the lens of the congruence closure *) (** View the term through the lens of the congruence closure *)
@ -283,12 +301,13 @@ module type CC_S = sig
module T : TERM module T : TERM
module Lit : LIT with module T = T module Lit : LIT with module T = T
type lemma type proof
module P : CC_PROOF with type lit = Lit.t and type lemma = lemma type dproof = proof -> unit
module P : CC_PROOF with type lit = Lit.t and type t = proof
module Actions : CC_ACTIONS module Actions : CC_ACTIONS
with module T = T with module T = T
and module Lit = Lit and module Lit = Lit
and type lemma = lemma and type proof = proof
type term_store = T.Term.store type term_store = T.Term.store
type term = T.Term.t type term = T.Term.t
type fun_ = T.Fun.t type fun_ = T.Fun.t
@ -429,7 +448,7 @@ module type CC_S = sig
participating in the conflict are purely syntactic theories participating in the conflict are purely syntactic theories
like injectivity of constructors. *) like injectivity of constructors. *)
type ev_on_propagate = t -> lit -> (unit -> lit list * P.lemma) -> unit type ev_on_propagate = t -> lit -> (unit -> lit list * dproof) -> unit
(** [ev_on_propagate cc lit reason] is called whenever [reason() => lit] (** [ev_on_propagate cc lit reason] is called whenever [reason() => lit]
is a propagated lemma. See {!CC_ACTIONS.propagate}. *) is a propagated lemma. See {!CC_ACTIONS.propagate}. *)
@ -580,6 +599,9 @@ module type SOLVER_INTERNAL = sig
type term = T.Term.t type term = T.Term.t
type term_store = T.Term.store type term_store = T.Term.store
type ty_store = T.Ty.store type ty_store = T.Ty.store
type proof
type dproof = proof -> unit
(** Delayed proof. This is used to build a proof step on demand. *)
(** {3 Literals} (** {3 Literals}
@ -589,9 +611,7 @@ module type SOLVER_INTERNAL = sig
module Lit : LIT with module T = T module Lit : LIT with module T = T
(** {3 Proofs} *) (** {3 Proofs} *)
type lemma module P : PROOF with type lit = Lit.t and type term = term and type t = proof
module P : PROOF with type lit = Lit.t and type lemma = lemma
type proof = P.t
(** {3 Main type for a solver} *) (** {3 Main type for a solver} *)
type t type t
@ -621,8 +641,8 @@ module type SOLVER_INTERNAL = sig
module CC : CC_S module CC : CC_S
with module T = T with module T = T
and module Lit = Lit and module Lit = Lit
and type lemma = lemma and type proof = proof
and type P.lemma = lemma and type P.t = proof
and type P.lit = lit and type P.lit = lit
and type Actions.t = actions and type Actions.t = actions
@ -641,19 +661,19 @@ module type SOLVER_INTERNAL = sig
val clear : t -> unit val clear : t -> unit
(** Reset internal cache, etc. *) (** Reset internal cache, etc. *)
type hook = t -> term -> (term * proof) option type hook = t -> term -> (term * dproof) option
(** Given a term, try to simplify it. Return [None] if it didn't change. (** Given 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], 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, and if [t] is [app "+" (const x) (const y)] where [x] and [y] are number,
returns [Some (const (x+y))], and [None] otherwise. *) returns [Some (const (x+y))], and [None] otherwise. *)
val normalize : t -> term -> (term * P.t) option val normalize : t -> term -> (term * dproof) option
(** Normalize a term using all the hooks. This performs (** Normalize a term using all the hooks. This performs
a fixpoint, i.e. it only stops when no hook applies anywhere inside a fixpoint, i.e. it only stops when no hook applies anywhere inside
the term. *) the term. *)
val normalize_t : t -> term -> term * P.t val normalize_t : t -> term -> term * dproof
(** Normalize a term using all the hooks, along with a proof that the (** Normalize a term using all the hooks, along with a proof that the
simplification is correct. simplification is correct.
returns [t, refl t] if no simplification occurred. *) returns [t, refl t] if no simplification occurred. *)
@ -666,18 +686,18 @@ module type SOLVER_INTERNAL = sig
val simplifier : t -> Simplify.t val simplifier : t -> Simplify.t
val simplify_t : t -> term -> (term * proof) option val simplify_t : t -> term -> (term * dproof) option
(** Simplify input term, returns [Some (u, |- t=u)] if some (** Simplify input term, returns [Some (u, |- t=u)] if some
simplification occurred. *) simplification occurred. *)
val simp_t : t -> term -> term * proof val simp_t : t -> term -> term * dproof
(** [simp_t si t] returns [u, |- t=u] even if no simplification occurred (** [simp_t si t] returns [u, |- t=u] even if no simplification occurred
(in which case [t == u] syntactically). (in which case [t == u] syntactically).
(see {!simplifier}) *) (see {!simplifier}) *)
(** {3 hooks for the theory} *) (** {3 hooks for the theory} *)
val raise_conflict : t -> actions -> lit list -> proof -> 'a val raise_conflict : t -> actions -> lit list -> dproof -> 'a
(** Give a conflict clause to the solver *) (** Give a conflict clause to the solver *)
val push_decision : t -> actions -> lit -> unit val push_decision : t -> actions -> lit -> unit
@ -686,19 +706,19 @@ module type SOLVER_INTERNAL = sig
If the SAT solver backtracks, this (potential) decision is removed If the SAT solver backtracks, this (potential) decision is removed
and forgotten. *) and forgotten. *)
val propagate: t -> actions -> lit -> reason:(unit -> lit list * proof) -> unit val propagate: t -> actions -> lit -> reason:(unit -> lit list * dproof) -> unit
(** Propagate a boolean using a unit clause. (** Propagate a boolean using a unit clause.
[expl => lit] must be a theory lemma, that is, a T-tautology *) [expl => lit] must be a theory lemma, that is, a T-tautology *)
val propagate_l: t -> actions -> lit -> lit list -> proof -> unit val propagate_l: t -> actions -> lit -> lit list -> dproof -> unit
(** Propagate a boolean using a unit clause. (** Propagate a boolean using a unit clause.
[expl => lit] must be a theory lemma, that is, a T-tautology *) [expl => lit] must be a theory lemma, that is, a T-tautology *)
val add_clause_temp : t -> actions -> lit list -> proof -> unit val add_clause_temp : t -> actions -> lit list -> dproof -> unit
(** Add local clause to the SAT solver. This clause will be (** Add local clause to the SAT solver. This clause will be
removed when the solver backtracks. *) removed when the solver backtracks. *)
val add_clause_permanent : t -> actions -> lit list -> proof -> unit val add_clause_permanent : t -> actions -> lit list -> dproof -> unit
(** Add toplevel clause to the SAT solver. This clause will (** Add toplevel clause to the SAT solver. This clause will
not be backtracked. *) not be backtracked. *)
@ -706,7 +726,7 @@ module type SOLVER_INTERNAL = sig
(** Create a literal. This automatically preprocesses the term. *) (** Create a literal. This automatically preprocesses the term. *)
val preprocess_term : val preprocess_term :
t -> add_clause:(Lit.t list -> proof -> unit) -> term -> term * proof t -> add_clause:(Lit.t list -> proof -> unit) -> term -> term * dproof
(** Preprocess a term. *) (** Preprocess a term. *)
val add_lit : t -> actions -> lit -> unit val add_lit : t -> actions -> lit -> unit
@ -762,7 +782,7 @@ module type SOLVER_INTERNAL = sig
val on_cc_conflict : t -> (CC.t -> th:bool -> lit list -> unit) -> unit val on_cc_conflict : t -> (CC.t -> th:bool -> lit list -> unit) -> unit
(** Callback called on every CC conflict *) (** Callback called on every CC conflict *)
val on_cc_propagate : t -> (CC.t -> lit -> (unit -> lit list * proof) -> unit) -> unit val on_cc_propagate : t -> (CC.t -> lit -> (unit -> lit list * dproof) -> unit) -> unit
(** Callback called on every CC propagation *) (** Callback called on every CC propagation *)
val on_partial_check : t -> (t -> actions -> lit Iter.t -> unit) -> unit val on_partial_check : t -> (t -> actions -> lit Iter.t -> unit) -> unit
@ -789,8 +809,8 @@ module type SOLVER_INTERNAL = sig
type preprocess_hook = type preprocess_hook =
t -> t ->
mk_lit:(term -> lit) -> mk_lit:(term -> lit) ->
add_clause:(lit list -> proof -> unit) -> add_clause:(lit list -> dproof -> unit) ->
term -> (term * proof) option term -> (term * dproof) option
(** Given a term, try to preprocess it. Return [None] if it didn't change, (** Given a term, try to preprocess it. Return [None] if it didn't change,
or [Some (u,p)] if [t=u] and [p] is a proof of [t=u]. or [Some (u,p)] if [t=u] and [p] is a proof of [t=u].
Can also add clauses to define new terms. Can also add clauses to define new terms.
@ -833,14 +853,14 @@ end
module type SOLVER = sig module type SOLVER = sig
module T : TERM module T : TERM
module Lit : LIT with module T = T module Lit : LIT with module T = T
type lemma type proof
module P : PROOF with type lit = Lit.t and type lemma = lemma module P : PROOF with type lit = Lit.t and type t = proof and type term = T.Term.t
module Solver_internal module Solver_internal
: SOLVER_INTERNAL : SOLVER_INTERNAL
with module T = T with module T = T
and module Lit = Lit and module Lit = Lit
and type lemma = lemma and type proof = proof
and module P = P and module P = P
(** Internal solver, available to theories. *) (** Internal solver, available to theories. *)
@ -851,7 +871,8 @@ module type SOLVER = sig
type term = T.Term.t type term = T.Term.t
type ty = T.Ty.t type ty = T.Ty.t
type lit = Lit.t type lit = Lit.t
type proof = P.t type dproof = proof -> unit
(** Delayed proof. This is used to build a proof step on demand. *)
(** {3 A theory} (** {3 A theory}
@ -997,7 +1018,7 @@ module type SOLVER = sig
val add_theory_l : t -> theory list -> unit val add_theory_l : t -> theory list -> unit
val mk_atom_lit : t -> lit -> Atom.t * P.t val mk_atom_lit : t -> lit -> Atom.t
(** [mk_atom_lit _ lit] returns [atom, pr] (** [mk_atom_lit _ lit] returns [atom, pr]
where [atom] is an internal atom for the solver, where [atom] is an internal atom for the solver,
and [pr] is a proof of [|- lit = atom] *) and [pr] is a proof of [|- lit = atom] *)
@ -1005,7 +1026,7 @@ module type SOLVER = sig
val mk_atom_lit' : t -> lit -> Atom.t val mk_atom_lit' : t -> lit -> Atom.t
(** Like {!mk_atom_t} but skips the proof *) (** Like {!mk_atom_t} but skips the proof *)
val mk_atom_t : t -> ?sign:bool -> term -> Atom.t * P.t val mk_atom_t : t -> ?sign:bool -> term -> Atom.t
(** [mk_atom_t _ ~sign t] returns [atom, pr] (** [mk_atom_t _ ~sign t] returns [atom, pr]
where [atom] is an internal representation of [± t], where [atom] is an internal representation of [± t],
and [pr] is a proof of [|- atom = (± t)] *) and [pr] is a proof of [|- atom = (± t)] *)

8
src/msat-solver/Sidekick_msat_solver.ml
View file

@ -11,7 +11,8 @@
module type ARG = sig module type ARG = sig
open Sidekick_core open Sidekick_core
module T : TERM module T : TERM
module P : PROOF with type term = T.Term.t type proof
module P : PROOF with type term = T.Term.t and type t = proof
val cc_view : T.Term.t -> (T.Fun.t, T.Term.t, T.Term.t Iter.t) CC_view.t val cc_view : T.Term.t -> (T.Fun.t, T.Term.t, T.Term.t Iter.t) CC_view.t
@ -26,6 +27,7 @@ module type S = Sidekick_core.SOLVER
module Make(A : ARG) module Make(A : ARG)
: S : S
with module T = A.T with module T = A.T
and type proof = A.proof
and module P = A.P and module P = A.P
= struct = struct
module T = A.T module T = A.T
@ -81,6 +83,7 @@ module Make(A : ARG)
module T = T module T = T
module P = P module P = P
module Lit = Lit_ module Lit = Lit_
type nonrec proof = proof
let cc_view = A.cc_view let cc_view = A.cc_view
module Actions = struct module Actions = struct
@ -516,6 +519,8 @@ module Make(A : ARG)
(** the parametrized SAT Solver *) (** the parametrized SAT Solver *)
module Sat_solver = Sidekick_sat.Make_cdcl_t(Solver_internal) module Sat_solver = Sidekick_sat.Make_cdcl_t(Solver_internal)
(* TODO: move somewhere else? where it can be used to implement the new
proof module?
module Pre_proof = struct module Pre_proof = struct
module SP = Sat_solver.Proof module SP = Sat_solver.Proof
module SC = Sat_solver.Clause module SC = Sat_solver.Clause
@ -643,6 +648,7 @@ module Make(A : ARG)
let pp_debug out self = P.pp_debug ~sharing:false out (to_proof self) let pp_debug out self = P.pp_debug ~sharing:false out (to_proof self)
let output oc (self:t) = P.Quip.output oc (to_proof self) let output oc (self:t) = P.Quip.output oc (to_proof self)
end end
*)
(* main solver state *) (* main solver state *)
type t = { type t = {

157
src/th-bool-static/Sidekick_th_bool_static.ml
View file

@ -27,18 +27,6 @@ module type ARG = sig
val view_as_bool : term -> (term, term Iter.t) bool_view val view_as_bool : term -> (term, term Iter.t) bool_view
(** Project the term into the boolean view. *) (** Project the term into the boolean view. *)
(** [proof_ite_true (ite a b c)] is [a=true |- ite a b c = b] *)
val proof_ite_true : S.T.Term.t -> S.P.t
(** [proof_ite_false (ite a b c)] is [a=false |- ite a b c = c] *)
val proof_ite_false : S.T.Term.t -> S.P.t
(** Basic boolean logic for [|- a=b] *)
val proof_bool_eq : S.T.Term.t -> S.T.Term.t -> S.P.t
(** Basic boolean logic for a clause [|- c] *)
val proof_bool_c : string -> term list -> S.P.t
val mk_bool : S.T.Term.store -> (term, term IArray.t) bool_view -> term val mk_bool : S.T.Term.store -> (term, term IArray.t) bool_view -> term
(** Make a term from the given boolean view. *) (** Make a term from the given boolean view. *)
@ -48,6 +36,22 @@ module type ARG = sig
Only enable if some theories are susceptible to Only enable if some theories are susceptible to
create boolean formulas during the proof search. *) create boolean formulas during the proof search. *)
val lemma_bool_tauto : S.P.t -> S.Lit.t Iter.t -> unit
(** Boolean tautology lemma (clause) *)
val lemma_bool_c : S.P.t -> string -> term list -> unit
(** Basic boolean logic lemma for a clause [|- c].
[proof_bool_c b name cs] is the rule designated by [name]. *)
val lemma_bool_equiv : S.P.t -> term -> term -> unit
(** Boolean tautology lemma (equivalence) *)
val lemma_ite_true : S.P.t -> a:term -> ite:term -> unit
(** lemma [a => ite a b c = b] *)
val lemma_ite_false : S.P.t -> a:term -> ite:term -> unit
(** lemma [¬a => ite a b c = c] *)
(** Fresh symbol generator. (** Fresh symbol generator.
The theory needs to be able to create new terms with fresh names, The theory needs to be able to create new terms with fresh names,
@ -98,7 +102,7 @@ module Make(A : ARG) : S with module A = A = struct
type state = { type state = {
tst: T.store; tst: T.store;
ty_st: Ty.store; ty_st: Ty.store;
cnf: (Lit.t * SI.P.t) T.Tbl.t; (* tseitin CNF *) cnf: (Lit.t * SI.dproof) T.Tbl.t; (* tseitin CNF *)
gensym: A.Gensym.t; gensym: A.Gensym.t;
} }
@ -114,9 +118,15 @@ module Make(A : ARG) : S with module A = A = struct
let is_true t = match T.as_bool t with Some true -> true | _ -> false let is_true t = match T.as_bool t with Some true -> true | _ -> false
let is_false t = match T.as_bool t with Some false -> true | _ -> false let is_false t = match T.as_bool t with Some false -> true | _ -> false
let simplify (self:state) (simp:SI.Simplify.t) (t:T.t) : (T.t * SI.P.t) option = let simplify (self:state) (simp:SI.Simplify.t) (t:T.t) : (T.t * SI.dproof) option =
let tst = self.tst in let tst = self.tst in
let ret u = Some (u, A.proof_bool_eq t u) in let ret u =
let emit_proof p =
A.lemma_bool_equiv p t u;
A.S.P.lemma_preprocess p t u;
in
Some (u, emit_proof)
in
match A.view_as_bool t with match A.view_as_bool t with
| B_bool _ -> None | B_bool _ -> None
| B_not u when is_true u -> ret (T.bool tst false) | B_not u when is_true u -> ret (T.bool tst false)
@ -141,11 +151,11 @@ module Make(A : ARG) : S with module A = A = struct
let a, pr_a = SI.Simplify.normalize_t simp a in let a, pr_a = SI.Simplify.normalize_t simp a in
begin match A.view_as_bool a with begin match A.view_as_bool a with
| B_bool true -> | B_bool true ->
let pr = SI.P.(hres_l (A.proof_ite_true t) [r1 pr_a]) in let emit_proof p = pr_a p; A.lemma_ite_true p ~a ~ite:t in
Some (b, pr) Some (b, emit_proof)
| B_bool false -> | B_bool false ->
let pr = SI.P.(hres_l (A.proof_ite_false t) [r1 pr_a]) in let emit_proof p = pr_a p; A.lemma_ite_false p ~a ~ite:t in
Some (c, pr) Some (c, emit_proof)
| _ -> | _ ->
None None
end end
@ -163,49 +173,47 @@ module Make(A : ARG) : S with module A = A = struct
| B_eq _ | B_neq _ -> None | B_eq _ | B_neq _ -> None
| B_atom _ -> None | B_atom _ -> None
let fresh_term self ~for_ ~pre ty = let fresh_term self ~for_t ~pre ty =
let u = A.Gensym.fresh_term self.gensym ~pre ty in let u = A.Gensym.fresh_term self.gensym ~pre ty in
Log.debugf 20 Log.debugf 20
(fun k->k "(@[sidekick.bool.proxy@ :t %a@ :for %a@])" (fun k->k "(@[sidekick.bool.proxy@ :t %a@ :for %a@])"
T.pp u T.pp for_); T.pp u T.pp for_t);
assert (Ty.equal ty (T.ty u)); assert (Ty.equal ty (T.ty u));
u u
let fresh_lit (self:state) ~for_ ~mk_lit ~pre : T.t * Lit.t = let fresh_lit (self:state) ~for_t ~mk_lit ~pre : T.t * Lit.t =
let proxy = fresh_term ~for_ ~pre self (Ty.bool self.ty_st) in let proxy = fresh_term ~for_t ~pre self (Ty.bool self.ty_st) in
proxy, mk_lit proxy proxy, mk_lit proxy
(* preprocess "ite" away *) (* preprocess "ite" away *)
let preproc_ite self si ~mk_lit ~add_clause (t:T.t) : (T.t * SI.P.t) option = let preproc_ite self si ~mk_lit ~add_clause (t:T.t) : (T.t * SI.dproof) option =
match A.view_as_bool t with match A.view_as_bool t with
| B_ite (a,b,c) -> | B_ite (a,b,c) ->
let a, pr_a = SI.simp_t si a in let a, pr_a = SI.simp_t si a in
begin match A.view_as_bool a with begin match A.view_as_bool a with
| B_bool true -> | B_bool true ->
(* [a=true |- ite a b c=b], [|- a=true] ==> [|- t=b] *) (* [a=true |- ite a b c=b], [|- a=true] ==> [|- t=b] *)
let proof = SI.P.(hres_l (A.proof_ite_true t) [p1 pr_a]) in let emit_proof p = pr_a p; A.lemma_ite_true p ~a ~ite:t in
Some (b, proof) Some (b, emit_proof)
| B_bool false -> | B_bool false ->
(* [a=false |- ite a b c=c], [|- a=false] ==> [|- t=c] *) (* [a=false |- ite a b c=c], [|- a=false] ==> [|- t=c] *)
let proof = SI.P.(hres_l (A.proof_ite_false t) [p1 pr_a]) in let emit_proof p = pr_a p; A.lemma_ite_false p ~a ~ite:t in
Some (c, proof) Some (c, emit_proof)
| _ -> | _ ->
let t_ite = fresh_term self ~for_:t ~pre:"ite" (T.ty b) in let t_ite = fresh_term self ~for_t:t ~pre:"ite" (T.ty b) in
SI.define_const si ~const:t_ite ~rhs:t; SI.define_const si ~const:t_ite ~rhs:t;
let lit_a = mk_lit a in let lit_a = mk_lit a in
add_clause [Lit.neg lit_a; mk_lit (eq self.tst t_ite b)] add_clause [Lit.neg lit_a; mk_lit (eq self.tst t_ite b)]
(A.proof_ite_true t); (fun p -> A.lemma_ite_true p ~a ~ite:t);
add_clause [lit_a; mk_lit (eq self.tst t_ite c)] add_clause [lit_a; mk_lit (eq self.tst t_ite c)]
(A.proof_ite_false t); (fun p -> A.lemma_ite_false p ~a ~ite:t);
Some (t_ite, SI.P.(refl t)) Some (t_ite, fun p -> SI.P.define_term p t_ite t)
end end
| _ -> None | _ -> None
let[@inline] pr_def_refl _proxy t = SI.P.(refl t)
(* TODO: polarity? *) (* TODO: polarity? *)
let cnf (self:state) (si:SI.t) ~mk_lit ~add_clause (t:T.t) : (T.t * SI.P.t) option = let cnf (self:state) (si:SI.t) ~mk_lit ~add_clause (t:T.t) : (T.t * SI.dproof) option =
let rec get_lit_and_proof_ (t:T.t) : Lit.t * SI.P.t = let rec get_lit_and_proof_ (t:T.t) : Lit.t * _ =
let t_abs, t_sign = T.abs self.tst t in let t_abs, t_sign = T.abs self.tst t in
let lit_abs, pr = let lit_abs, pr =
match T.Tbl.find self.cnf t_abs with match T.Tbl.find self.cnf t_abs with
@ -225,13 +233,13 @@ module Make(A : ARG) : S with module A = A = struct
let lit = if t_sign then lit_abs else Lit.neg lit_abs in let lit = if t_sign then lit_abs else Lit.neg lit_abs in
lit, pr lit, pr
and equiv_ si ~get_lit ~is_xor ~for_ t_a t_b : Lit.t * SI.P.t = and equiv_ si ~get_lit ~is_xor ~for_t t_a t_b : Lit.t * SI.dproof =
let a = get_lit t_a in let a = get_lit t_a in
let b = get_lit t_b in let b = get_lit t_b in
let a = if is_xor then Lit.neg a else a in (* [a xor b] is [(¬a) = b] *) let a = if is_xor then Lit.neg a else a in (* [a xor b] is [(¬a) = b] *)
let t_proxy, proxy = fresh_lit ~for_ ~mk_lit ~pre:"equiv_" self in let t_proxy, proxy = fresh_lit ~for_t ~mk_lit ~pre:"equiv_" self in
SI.define_const si ~const:t_proxy ~rhs:for_; SI.define_const si ~const:t_proxy ~rhs:for_t;
let add_clause c pr = let add_clause c pr =
add_clause c pr add_clause c pr
in in
@ -239,21 +247,24 @@ module Make(A : ARG) : S with module A = A = struct
(* proxy => a<=> b, (* proxy => a<=> b,
¬proxy => a xor b *) ¬proxy => a xor b *)
add_clause [Lit.neg proxy; Lit.neg a; b] add_clause [Lit.neg proxy; Lit.neg a; b]
(if is_xor then A.proof_bool_c "xor-e+" [t_proxy] (fun p ->
else A.proof_bool_c "eq-e" [t_proxy; t_a]); if is_xor then A.lemma_bool_c p "xor-e+" [t_proxy]
else A.lemma_bool_c p "eq-e" [t_proxy; t_a]);
add_clause [Lit.neg proxy; Lit.neg b; a] add_clause [Lit.neg proxy; Lit.neg b; a]
(if is_xor then A.proof_bool_c "xor-e-" [t_proxy] (fun p ->
else A.proof_bool_c "eq-e" [t_proxy; t_b]); if is_xor then A.lemma_bool_c p "xor-e-" [t_proxy]
else A.lemma_bool_c p "eq-e" [t_proxy; t_b]);
add_clause [proxy; a; b] add_clause [proxy; a; b]
(if is_xor then A.proof_bool_c "xor-i" [t_proxy; t_a] (fun p -> if is_xor then A.lemma_bool_c p "xor-i" [t_proxy; t_a]
else A.proof_bool_c "eq-i+" [t_proxy]); else A.lemma_bool_c p "eq-i+" [t_proxy]);
add_clause [proxy; Lit.neg a; Lit.neg b] add_clause [proxy; Lit.neg a; Lit.neg b]
(if is_xor then A.proof_bool_c "xor-i" [t_proxy; t_b] (fun p ->
else A.proof_bool_c "eq-i-" [t_proxy]); if is_xor then A.lemma_bool_c p "xor-i" [t_proxy; t_b]
proxy, pr_def_refl t_proxy for_ else A.lemma_bool_c p "eq-i-" [t_proxy]);
proxy, (fun p->SI.P.define_term p t_proxy for_t)
(* make a literal for [t], with a proof of [|- abs(t) = abs(lit)] *) (* make a literal for [t], with a proof of [|- abs(t) = abs(lit)] *)
and get_lit_uncached si t : Lit.t * SI.P.t = and get_lit_uncached si t : Lit.t * SI.dproof =
let sub_p = ref [] in let sub_p = ref [] in
let get_lit t = let get_lit t =
@ -265,8 +276,8 @@ module Make(A : ARG) : S with module A = A = struct
in in
match A.view_as_bool t with match A.view_as_bool t with
| B_bool b -> mk_lit (T.bool self.tst b), SI.P.refl t | B_bool b -> mk_lit (T.bool self.tst b), (fun _->())
| B_opaque_bool t -> mk_lit t, SI.P.refl t | B_opaque_bool t -> mk_lit t, (fun _->())
| B_not u -> | B_not u ->
let lit, pr = get_lit_and_proof_ u in let lit, pr = get_lit_and_proof_ u in
Lit.neg lit, pr Lit.neg lit, pr
@ -274,33 +285,37 @@ module Make(A : ARG) : S with module A = A = struct
| B_and l -> | B_and l ->
let t_subs = Iter.to_list l in let t_subs = Iter.to_list l in
let subs = List.map get_lit t_subs in let subs = List.map get_lit t_subs in
let t_proxy, proxy = fresh_lit ~for_:t ~mk_lit ~pre:"and_" self in let t_proxy, proxy = fresh_lit ~for_t:t ~mk_lit ~pre:"and_" self in
SI.define_const si ~const:t_proxy ~rhs:t; SI.define_const si ~const:t_proxy ~rhs:t;
(* add clauses *) (* add clauses *)
List.iter2 List.iter2
(fun t_u u -> (fun t_u u ->
add_clause add_clause
[Lit.neg proxy; u] [Lit.neg proxy; u]
(A.proof_bool_c "and-e" [t_proxy; t_u])) (fun p -> A.lemma_bool_c p "and-e" [t_proxy; t_u]))
t_subs subs; t_subs subs;
add_clause (proxy :: List.map Lit.neg subs) add_clause (proxy :: List.map Lit.neg subs)
(A.proof_bool_c "and-i" [t_proxy]); (fun p -> A.lemma_bool_c p "and-i" [t_proxy]);
proxy, pr_def_refl t_proxy t let emit_proof p =
SI.P.define_term p t_proxy t;
in
proxy, emit_proof
| B_or l -> | B_or l ->
let t_subs = Iter.to_list l in let t_subs = Iter.to_list l in
let subs = List.map get_lit t_subs in let subs = List.map get_lit t_subs in
let t_proxy, proxy = fresh_lit ~for_:t ~mk_lit ~pre:"or_" self in let t_proxy, proxy = fresh_lit ~for_t:t ~mk_lit ~pre:"or_" self in
SI.define_const si ~const:t_proxy ~rhs:t; SI.define_const si ~const:t_proxy ~rhs:t;
(* add clauses *) (* add clauses *)
List.iter2 List.iter2
(fun t_u u -> (fun t_u u ->
add_clause [Lit.neg u; proxy] add_clause [Lit.neg u; proxy]
(A.proof_bool_c "or-i" [t_proxy; t_u])) (fun p -> A.lemma_bool_c p "or-i" [t_proxy; t_u]))
t_subs subs; t_subs subs;
add_clause (Lit.neg proxy :: subs) add_clause (Lit.neg proxy :: subs)
(A.proof_bool_c "or-e" [t_proxy]); (fun p -> A.lemma_bool_c p "or-e" [t_proxy]);
proxy, pr_def_refl t_proxy t let emit_proof p = SI.P.define_term p t_proxy t in
proxy, emit_proof
| B_imply (t_args, t_u) -> | B_imply (t_args, t_u) ->
(* transform into [¬args \/ u] on the fly *) (* transform into [¬args \/ u] on the fly *)
@ -310,23 +325,24 @@ module Make(A : ARG) : S with module A = A = struct
let subs = u :: args in let subs = u :: args in
(* now the or-encoding *) (* now the or-encoding *)
let t_proxy, proxy = fresh_lit ~for_:t ~mk_lit ~pre:"implies_" self in let t_proxy, proxy = fresh_lit ~for_t:t ~mk_lit ~pre:"implies_" self in
SI.define_const si ~const:t_proxy ~rhs:t; SI.define_const si ~const:t_proxy ~rhs:t;
(* add clauses *) (* add clauses *)
List.iter2 List.iter2
(fun t_u u -> (fun t_u u ->
add_clause [Lit.neg u; proxy] add_clause [Lit.neg u; proxy]
(A.proof_bool_c "imp-i" [t_proxy; t_u])) (fun p -> A.lemma_bool_c p "imp-i" [t_proxy; t_u]))
(t_u::t_args) subs; (t_u::t_args) subs;
add_clause (Lit.neg proxy :: subs) add_clause (Lit.neg proxy :: subs)
(A.proof_bool_c "imp-e" [t_proxy]); (fun p -> A.lemma_bool_c p "imp-e" [t_proxy]);
proxy, pr_def_refl t_proxy t let emit_proof p = SI.P.define_term p t_proxy t in
proxy, emit_proof
| B_ite _ | B_eq _ | B_neq _ -> mk_lit t, SI.P.refl t | B_ite _ | B_eq _ | B_neq _ -> mk_lit t, (fun _ ->())
| B_equiv (a,b) -> equiv_ si ~get_lit ~for_:t ~is_xor:false a b | B_equiv (a,b) -> equiv_ si ~get_lit ~for_t:t ~is_xor:false a b
| B_xor (a,b) -> equiv_ si ~get_lit ~for_:t ~is_xor:true a b | B_xor (a,b) -> equiv_ si ~get_lit ~for_t:t ~is_xor:true a b
| B_atom u -> mk_lit u, SI.P.refl u | B_atom u -> mk_lit u, (fun _->())
in in
let lit, pr = get_lit_and_proof_ t in let lit, pr = get_lit_and_proof_ t in
@ -353,10 +369,11 @@ module Make(A : ARG) : S with module A = A = struct
all_terms all_terms
(fun t -> match cnf_of t with (fun t -> match cnf_of t with
| None -> () | None -> ()
| Some (u, pr_t_u) -> | Some (u, _pr_t_u) ->
(* FIXME: what to do with pr_t_u? emit it? *)
Log.debugf 5 Log.debugf 5
(fun k->k "(@[th-bool-static.final-check.cnf@ %a@ :yields %a@ :pr %a@])" (fun k->k "(@[th-bool-static.final-check.cnf@ %a@ :yields %a@])"
T.pp t T.pp u (SI.P.pp_debug ~sharing:false) pr_t_u); T.pp t T.pp u);
SI.CC.merge_t cc_ t u (SI.CC.Expl.mk_list []); SI.CC.merge_t cc_ t u (SI.CC.Expl.mk_list []);
()); ());
end; end;