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: proof production

Browse source
This commit is contained in:
Simon Cruanes 2021-10-09 00:51:15 -04:00
parent d3537f2c3f
commit 0550f6fcfa
No known key found for this signature in database
GPG key ID: 4AC01D0849AA62B6
3 changed files with 76 additions and 53 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/core/Sidekick_core.ml
View file

@ -786,6 +786,9 @@ module type SOLVER_INTERNAL = sig
module type PREPROCESS_ACTS = sig
val proof : proof
val mk_lit_nopreproc : ?sign:bool -> term -> lit
(** [mk_lit t] creates a new literal for a boolean term [t]. *)
val mk_lit : ?sign:bool -> term -> lit * proof_step option
(** [mk_lit t] creates a new literal for a boolean term [t].
Also returns an optional proof of preprocessing, which if present

10
src/smt-solver/Sidekick_smt_solver.ml
View file

@ -187,6 +187,7 @@ module Make(A : ARG)
module type PREPROCESS_ACTS = sig
val proof : proof
val mk_lit_nopreproc : ?sign:bool -> term -> lit
val mk_lit : ?sign:bool -> term -> lit * proof_step option
val add_clause : lit list -> proof_step -> unit
val add_lit : ?default_pol:bool -> lit -> unit
@ -282,7 +283,7 @@ module Make(A : ARG)
this calls all the preprocessing hooks on subterms, ensuring
a fixpoint. *)
let preprocess_term_ (self:t) (module A0:PREPROCESS_ACTS) (t:term) : term * proof_step option =
let mk_lit_nopreproc t = Lit.atom self.tst t in (* no further simplification *)
let mk_lit_nopreproc ?sign t = Lit.atom ?sign self.tst t in (* no further simplification *)
(* compute and cache normal form [u] of [t].
@ -384,10 +385,13 @@ module Make(A : ARG)
and pacts = lazy (
(module struct
let proof = A0.proof
let add_lit ?default_pol lit =
(* just drop the proof *)
(* TODO: add a clause instead [lit => preprocess(lit)]? *)
let lit = preprocess_lit ~steps:(ref []) lit in
A0.add_lit ?default_pol lit
let add_clause c pr_c =
Stat.incr self.count_preprocess_clause;
let steps = ref [] in
@ -398,6 +402,8 @@ module Make(A : ARG)
in
A0.add_clause c' pr_c'
let mk_lit_nopreproc = mk_lit_nopreproc
let mk_lit = mk_lit
end : PREPROCESS_ACTS)
) in
@ -441,6 +447,7 @@ module Make(A : ARG)
let preprocess_acts_of_acts (self:t) (acts:theory_actions) : preprocess_actions =
(module struct
let proof = self.proof
let mk_lit_nopreproc ?sign t = Lit.atom self.tst ?sign t
let mk_lit ?sign t = Lit.atom self.tst ?sign t, None
let add_clause = add_clause_ self acts
let add_lit = add_lit self acts
@ -693,6 +700,7 @@ module Make(A : ARG)
(self:t) : (module Solver_internal.PREPROCESS_ACTS) =
(module struct
let proof = self.proof
let mk_lit_nopreproc ?sign t = Lit.atom ?sign self.si.tst t
let mk_lit ?sign t = Lit.atom ?sign self.si.tst t, None
let add_lit ?default_pol lit =
Sat_solver.add_lit self.solver ?default_pol lit

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

@ -126,7 +126,7 @@ module Make(A : ARG) : S with module A = A = struct
in
(* proof is [t <=> u] *)
let ret_bequiv t1 u =
add_step_ @@ SI.Simplify.with_proof simp (A.lemma_bool_equiv t1 u);
add_step_ @@ A.lemma_bool_equiv t1 u @@ SI.Simplify.proof simp;
ret u
in
@ -152,13 +152,13 @@ module Make(A : ARG) : S with module A = A = struct
(* directly simplify [a] so that maybe we never will simplify one
of the branches *)
let a, prf_a = SI.Simplify.normalize_t simp a in
Iter.iter add_step_ prf_a;
CCOpt.iter add_step_ prf_a;
begin match A.view_as_bool a with
| B_bool true ->
add_step_ @@ SI.Simplify.with_proof simp (A.lemma_ite_true ~a ~ite:t);
add_step_ @@ A.lemma_ite_true ~a ~ite:t @@ SI.Simplify.proof simp;
ret b
| B_bool false ->
add_step_ @@ SI.Simplify.with_proof simp (A.lemma_ite_false ~a ~ite:t);
add_step_ @@ A.lemma_ite_false ~a ~ite:t @@ SI.Simplify.proof simp;
ret c
| _ ->
None
@ -189,13 +189,10 @@ module Make(A : ARG) : S with module A = A = struct
let proxy = fresh_term ~for_t ~pre self (Ty.bool self.ty_st) in
proxy, mk_lit proxy
let p1_opt s1 s2 p : SI.proof_step =
let s2 = s2 p in
let pr_p1_opt p s1 s2 : SI.proof_step =
CCOpt.map_or ~default:s2 (fun s1 -> SI.P.proof_p1 s1 s2 p) s1
let p1_map s1 s2 p =
let s2 = s2 p in
SI.P.proof_p1 s1 s2 p
let pr_p1 p s1 s2 = SI.P.proof_p1 s1 s2 p
(* preprocess "ite" away *)
let preproc_ite self si (module PA:SI.PREPROCESS_ACTS) (t:T.t) : (T.t * SI.proof_step Iter.t) option =
@ -211,60 +208,66 @@ module Make(A : ARG) : S with module A = A = struct
begin match A.view_as_bool a' with
| B_bool true ->
(* [a=true |- ite a b c=b], [|- a=true] ==> [|- t=b] *)
add_step_ @@ SI.with_proof si (A.lemma_ite_true ~a:a' ~ite:t);
add_step_ @@ A.lemma_ite_true ~a:a' ~ite:t PA.proof;
ret b
| B_bool false ->
(* [a=false |- ite a b c=c], [|- a=false] ==> [|- t=c] *)
add_step_ @@ SI.with_proof si (A.lemma_ite_false ~a:a' ~ite:t);
add_step_ @@ A.lemma_ite_false ~a:a' ~ite:t PA.proof;
ret c
| _ ->
let t_ite = fresh_term self ~for_t:t ~pre:"ite" (T.ty b) in
SI.define_const si ~const:t_ite ~rhs:t;
let pr_def = SI.with_proof si (SI.P.define_term t_ite t) in
let lit_a = PA.mk_lit a' in
let pr_def = SI.P.define_term t_ite t PA.proof in
let lit_a = PA.mk_lit_nopreproc a' in
(* TODO: use unit paramod on each clause with side t=t_ite and on a=a' *)
PA.add_clause [Lit.neg lit_a; PA.mk_lit (eq self.tst t_ite b)]
(p1_map pr_def @@ p1_opt pr_a (A.lemma_ite_true ~a:a' ~ite:t));
PA.add_clause [lit_a; PA.mk_lit (eq self.tst t_ite c)]
(p1_map pr_def @@ p1_opt pr_a (A.lemma_ite_false ~a:a' ~ite:t));
PA.add_clause [Lit.neg lit_a; PA.mk_lit_nopreproc (eq self.tst t_ite b)]
(pr_p1 PA.proof pr_def @@ pr_p1_opt PA.proof pr_a @@
A.lemma_ite_true ~a:a' ~ite:t PA.proof);
PA.add_clause [lit_a; PA.mk_lit_nopreproc (eq self.tst t_ite c)]
(pr_p1 PA.proof pr_def @@ pr_p1_opt PA.proof pr_a @@
A.lemma_ite_false ~a:a' ~ite:t PA.proof);
ret t_ite
end
| _ -> None
(* TODO: polarity? *)
let cnf (self:state) (si:SI.t) (module PA:SI.PREPROCESS_ACTS) (t:T.t) : T.t option =
let cnf (self:state) (si:SI.t) (module PA:SI.PREPROCESS_ACTS)
(t:T.t) : (T.t * _ Iter.t) option =
Log.debugf 50 (fun k->k"(@[th-bool.cnf@ %a@])" T.pp t);
let mk_lit = PA.mk_lit in
let steps = ref [] in
let[@inline] add_step s = steps := s :: !steps in
(* handle boolean equality *)
let equiv_ si ~is_xor ~for_t t_a t_b : Lit.t =
let a = mk_lit t_a in
let b = mk_lit t_b in
let a = PA.mk_lit_nopreproc t_a in
let b = PA.mk_lit_nopreproc t_b in
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_t ~mk_lit:PA.mk_lit ~pre:"equiv_" self in
let t_proxy, proxy = fresh_lit ~for_t ~mk_lit:PA.mk_lit_nopreproc ~pre:"equiv_" self in
SI.define_const si ~const:t_proxy ~rhs:for_t;
let pr_def = SI.with_proof si (SI.P.define_term t_proxy for_t) in
let pr_def = SI.P.define_term t_proxy for_t PA.proof in
add_step pr_def;
let add_clause c pr =
PA.add_clause c pr
in
let[@inline] add_clause c pr = PA.add_clause c pr in
(* proxy => a<=> b,
¬proxy => a xor b *)
add_clause [Lit.neg proxy; Lit.neg a; b]
(if is_xor then A.lemma_bool_c "xor-e+" [t_proxy]
else A.lemma_bool_c "eq-e" [t_proxy; t_a]);
(pr_p1 PA.proof pr_def @@
if is_xor then A.lemma_bool_c "xor-e+" [for_t] PA.proof
else A.lemma_bool_c "eq-e" [for_t; t_a] PA.proof);
add_clause [Lit.neg proxy; Lit.neg b; a]
(if is_xor then A.lemma_bool_c "xor-e-" [t_proxy]
else A.lemma_bool_c "eq-e" [t_proxy; t_b]);
(pr_p1 PA.proof pr_def @@
if is_xor then A.lemma_bool_c "xor-e-" [for_t] PA.proof
else A.lemma_bool_c "eq-e" [for_t; t_b] PA.proof);
add_clause [proxy; a; b]
(if is_xor then A.lemma_bool_c "xor-i" [t_proxy; t_a]
else A.lemma_bool_c "eq-i+" [t_proxy]);
(pr_p1 PA.proof pr_def @@
if is_xor then A.lemma_bool_c "xor-i" [for_t; t_a] PA.proof
else A.lemma_bool_c "eq-i+" [for_t] PA.proof);
add_clause [proxy; Lit.neg a; Lit.neg b]
(if is_xor then A.lemma_bool_c "xor-i" [t_proxy; t_b]
else A.lemma_bool_c "eq-i-" [t_proxy]);
(pr_p1 PA.proof pr_def @@
if is_xor then A.lemma_bool_c "xor-i" [for_t; t_b] PA.proof
else A.lemma_bool_c "eq-i-" [for_t] PA.proof);
proxy
in
@ -279,57 +282,66 @@ module Make(A : ARG) : S with module A = A = struct
| B_and l ->
let t_subs = Iter.to_list l in
let subs = List.map mk_lit t_subs in
let t_proxy, proxy = fresh_lit ~for_t:t ~mk_lit:PA.mk_lit ~pre:"and_" self in
let subs = List.map PA.mk_lit_nopreproc t_subs in
let t_proxy, proxy = fresh_lit ~for_t:t ~mk_lit:PA.mk_lit_nopreproc ~pre:"and_" self in
SI.define_const si ~const:t_proxy ~rhs:t;
SI.with_proof si (SI.P.define_term t_proxy t);
let pr_def = SI.P.define_term t_proxy t PA.proof in
add_step pr_def;
(* add clauses *)
List.iter2
(fun t_u u ->
PA.add_clause
[Lit.neg proxy; u]
(A.lemma_bool_c "and-e" [t_proxy; t_u]))
(pr_p1 PA.proof pr_def @@ A.lemma_bool_c "and-e" [t; t_u] PA.proof))
t_subs subs;
PA.add_clause (proxy :: List.map Lit.neg subs)
(A.lemma_bool_c "and-i" [t_proxy]);
(pr_p1 PA.proof pr_def @@ A.lemma_bool_c "and-i" [t] PA.proof);
Some proxy
| B_or l ->
let t_subs = Iter.to_list l in
let subs = List.map mk_lit t_subs in
let t_proxy, proxy = fresh_lit ~for_t:t ~mk_lit:PA.mk_lit ~pre:"or_" self in
let subs = List.map PA.mk_lit_nopreproc t_subs in
let t_proxy, proxy = fresh_lit ~for_t:t ~mk_lit:PA.mk_lit_nopreproc ~pre:"or_" self in
SI.define_const si ~const:t_proxy ~rhs:t;
SI.with_proof si (SI.P.define_term t_proxy t);
let pr_def = SI.P.define_term t_proxy t PA.proof in
add_step pr_def;
(* add clauses *)
List.iter2
(fun t_u u ->
PA.add_clause [Lit.neg u; proxy]
(A.lemma_bool_c "or-i" [t_proxy; t_u]))
(pr_p1 PA.proof pr_def @@
A.lemma_bool_c "or-i" [t; t_u] PA.proof))
t_subs subs;
PA.add_clause (Lit.neg proxy :: subs)
(A.lemma_bool_c "or-e" [t_proxy]);
(pr_p1 PA.proof pr_def @@ A.lemma_bool_c "or-e" [t] PA.proof);
Some proxy
| B_imply (t_args, t_u) ->
(* transform into [¬args \/ u] on the fly *)
let t_args = Iter.to_list t_args in
let args = List.map (fun t -> Lit.neg (mk_lit t)) t_args in
let u = mk_lit t_u in
let args = List.map (fun t -> Lit.neg (PA.mk_lit_nopreproc t)) t_args in
let u = PA.mk_lit_nopreproc t_u in
let subs = u :: args in
(* now the or-encoding *)
let t_proxy, proxy = fresh_lit ~for_t:t ~mk_lit:PA.mk_lit ~pre:"implies_" self in
let t_proxy, proxy =
fresh_lit ~for_t:t ~mk_lit:PA.mk_lit_nopreproc ~pre:"implies_" self in
SI.define_const si ~const:t_proxy ~rhs:t;
SI.with_proof si (SI.P.define_term t_proxy t);
let pr_def = SI.P.define_term t_proxy t PA.proof in
add_step pr_def;
(* add clauses *)
List.iter2
(fun t_u u ->
PA.add_clause [Lit.neg u; proxy]
(A.lemma_bool_c "imp-i" [t_proxy; t_u]))
(pr_p1 PA.proof pr_def @@
A.lemma_bool_c "imp-i" [t_proxy; t_u] PA.proof))
(t_u::t_args) subs;
PA.add_clause (Lit.neg proxy :: subs)
(A.lemma_bool_c "imp-e" [t_proxy]);
(pr_p1 PA.proof pr_def @@
A.lemma_bool_c "imp-e" [t_proxy] PA.proof);
Some proxy
| B_ite _ | B_eq _ | B_neq _ -> None
@ -344,7 +356,7 @@ module Make(A : ARG) : S with module A = A = struct
let u = Lit.term lit in
(* put sign back as a "not" *)
let u = if Lit.sign lit then u else A.mk_bool self.tst (B_not u) in
if T.equal u t then None else Some u
if T.equal u t then None else Some (u, Iter.of_list !steps)
end
(* check if new terms were added to the congruence closure, that can be turned