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

refactor(smt): preprocessing is now using a queue of delayed actions

Browse source 
- preprocessing doesn't simplify anymore, it assumes terms are already
  simplified. It only adds clauses/adds literals, it does not return
  new terms.
- adding clauses/literals to SAT is done as delayed actions, to avoid
  issues of reentrancy.
  These actions are performed after preprocessing, in a loop that has
  access to the SAT solver.
This commit is contained in:
Simon Cruanes 2022-02-04 16:08:01 -05:00
parent f9036fa33b
commit cbc9c5ac6f
No known key found for this signature in database
GPG key ID: EBFFF6F283F3A2B4
9 changed files with 298 additions and 531 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/base-solver/sidekick_base_solver.ml
View file

@ -119,7 +119,6 @@ module Th_lra = Sidekick_arith_lra.Make(struct
let rec view_as_lra t = match T.view t with let rec view_as_lra t = match T.view t with
| T.LIA (Const i) -> LRA.LRA_const (Q.of_bigint i) | T.LIA (Const i) -> LRA.LRA_const (Q.of_bigint i)
| T.LRA l -> | T.LRA l ->
let open Base_types in
let module LRA = Sidekick_arith_lra in let module LRA = Sidekick_arith_lra in
begin match l with begin match l with
| Const c -> LRA.LRA_const c | Const c -> LRA.LRA_const c
@ -165,7 +164,6 @@ module Th_lia = Sidekick_arith_lia.Make(struct
let view_as_lia t = match T.view t with let view_as_lia t = match T.view t with
| T.LIA l -> | T.LIA l ->
let open Base_types in
let module LIA = Sidekick_arith_lia in let module LIA = Sidekick_arith_lia in
begin match l with begin match l with
| Const c -> LIA.LIA_const c | Const c -> LIA.LIA_const c
@ -183,7 +181,6 @@ module Th_lia = Sidekick_arith_lia.Make(struct
let lemma_lia = Proof.lemma_lia let lemma_lia = Proof.lemma_lia
let lemma_relax_to_lra = Proof.lemma_relax_to_lra let lemma_relax_to_lra = Proof.lemma_relax_to_lra
module Gensym = Gensym
end) end)
let th_bool : Solver.theory = Th_bool.theory let th_bool : Solver.theory = Th_bool.theory

4
src/base/Base_types.ml
View file

@ -992,6 +992,7 @@ module Term : sig
val iter_dag : t -> t Iter.t val iter_dag : t -> t Iter.t
val map_shallow : store -> (t -> t) -> t -> t val map_shallow : store -> (t -> t) -> t -> t
val iter_shallow : store -> (t -> unit) -> t -> unit
val pp : t Fmt.printer val pp : t Fmt.printer
@ -1210,6 +1211,9 @@ end = struct
let pp = pp_term let pp = pp_term
let[@inline] iter_shallow _tst f (t:t) : unit =
Term_cell.iter f (view t)
module Iter_dag = struct module Iter_dag = struct
type t = unit Tbl.t type t = unit Tbl.t
type order = Pre | Post type order = Pre | Post

3
src/base/Form.ml
View file

@ -188,6 +188,3 @@ module Gensym = struct
let id = ID.make name in let id = ID.make name in
T.const self.tst @@ Fun.mk_undef_const id ty T.const self.tst @@ Fun.mk_undef_const id ty
end end
(* NOTE: no plugin produces new boolean formulas *)
let check_congruence_classes = false

35
src/core/Sidekick_core.ml
View file

@ -119,6 +119,9 @@ module type TERM = sig
val map_shallow : store -> (t -> t) -> t -> t val map_shallow : store -> (t -> t) -> t -> t
(** Map function on immediate subterms. This should not be recursive. *) (** Map function on immediate subterms. This should not be recursive. *)
val iter_shallow : store -> (t -> unit) -> t -> unit
(** Iterate function on immediate subterms. This should not be recursive. *)
val iter_dag : t -> (t -> unit) -> unit val iter_dag : t -> (t -> unit) -> unit
(** [iter_dag t f] calls [f] once on each subterm of [t], [t] included. (** [iter_dag t f] calls [f] once on each subterm of [t], [t] included.
It must {b not} traverse [t] as a tree, but rather as a It must {b not} traverse [t] as a tree, but rather as a
@ -809,7 +812,11 @@ module type SOLVER_INTERNAL = sig
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.
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) option val normalize : t -> term -> (term * proof_step) option
(** Normalize a term using all the hooks. This performs (** Normalize a term using all the hooks. This performs
@ -845,14 +852,9 @@ module type SOLVER_INTERNAL = sig
module type PREPROCESS_ACTS = sig module type PREPROCESS_ACTS = sig
val proof : proof val proof : proof
val mk_lit_nopreproc : ?sign:bool -> term -> lit val mk_lit : ?sign:bool -> term -> lit
(** [mk_lit t] creates a new literal for a boolean term [t]. *) (** [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
is the proof of [|- t = lit] with [lit] the result. *)
val add_clause : lit list -> proof_step -> unit val add_clause : lit list -> proof_step -> unit
(** pushes a new clause into the SAT solver. *) (** pushes a new clause into the SAT solver. *)
@ -866,14 +868,13 @@ module type SOLVER_INTERNAL = sig
type preprocess_hook = type preprocess_hook =
t -> t ->
preprocess_actions -> preprocess_actions ->
term -> (term * proof_step Iter.t) option term -> unit
(** Given a term, try to preprocess it. Return [None] if it didn't change, (** Given a term, preprocess it.
or [Some (u)] if [t=u].
Can also add clauses to define new terms.
Preprocessing might transform terms to make them more amenable The idea is to add literals and clauses to help define the meaning of
to reasoning, e.g. by removing boolean formulas via Tseitin encoding, the term, if needed. For example for boolean formulas, clauses
adding clauses that encode their meaning in the same move. for their Tseitin encoding can be added, with the formula acting
as its own proxy symbol.
@param preprocess_actions actions available during preprocessing. @param preprocess_actions actions available during preprocessing.
*) *)
@ -881,9 +882,6 @@ module type SOLVER_INTERNAL = sig
val on_preprocess : t -> preprocess_hook -> unit val on_preprocess : t -> preprocess_hook -> unit
(** Add a hook that will be called when terms are preprocessed *) (** Add a hook that will be called when terms are preprocessed *)
val preprocess_acts_of_acts : t -> theory_actions -> preprocess_actions
(** Obtain preprocessor actions, from theory actions *)
(** {3 hooks for the theory} *) (** {3 hooks for the theory} *)
val raise_conflict : t -> theory_actions -> lit list -> proof_step -> 'a val raise_conflict : t -> theory_actions -> lit list -> proof_step -> 'a
@ -914,9 +912,6 @@ module type SOLVER_INTERNAL = sig
val mk_lit : t -> theory_actions -> ?sign:bool -> term -> lit val mk_lit : t -> theory_actions -> ?sign:bool -> term -> lit
(** Create a literal. This automatically preprocesses the term. *) (** Create a literal. This automatically preprocesses the term. *)
val preprocess_term : t -> preprocess_actions -> term -> term * proof_step option
(** Preprocess a term. *)
val add_lit : t -> theory_actions -> ?default_pol:bool -> lit -> unit val add_lit : t -> theory_actions -> ?default_pol:bool -> lit -> unit
(** Add the given literal to the SAT solver, so it gets assigned (** Add the given literal to the SAT solver, so it gets assigned
a boolean value. a boolean value.

13
src/lia/Sidekick_arith_lia.ml
View file

@ -74,7 +74,7 @@ module Make(A : ARG) : S with module A = A = struct
(* preprocess linear expressions away *) (* preprocess linear expressions away *)
let preproc_lia (self:state) si (module PA:SI.PREPROCESS_ACTS) let preproc_lia (self:state) si (module PA:SI.PREPROCESS_ACTS)
(t:T.t) : (T.t * SI.proof_step Iter.t) option = (t:T.t) : unit =
Log.debugf 50 (fun k->k "(@[lia.preprocess@ %a@])" T.pp t); Log.debugf 50 (fun k->k "(@[lia.preprocess@ %a@])" T.pp t);
match A.view_as_lia t with match A.view_as_lia t with
@ -85,16 +85,17 @@ module Make(A : ARG) : S with module A = A = struct
let lits = [Lit.atom ~sign:false self.tst t; Lit.atom self.tst u] in let lits = [Lit.atom ~sign:false self.tst t; Lit.atom self.tst u] in
A.lemma_relax_to_lra Iter.(of_list lits) self.proof A.lemma_relax_to_lra Iter.(of_list lits) self.proof
in in
Some (u, Iter.return pr)
(* add [t => u] *)
let cl = [PA.mk_lit ~sign:false t; PA.mk_lit u] in
PA.add_clause cl pr;
| LIA_other t when A.has_ty_int t -> | LIA_other t when A.has_ty_int t ->
SI.declare_pb_is_incomplete si; SI.declare_pb_is_incomplete si;
None
| LIA_op _ | LIA_mult _ -> | LIA_op _ | LIA_mult _ ->
(* TODO: theory combination?*)
SI.declare_pb_is_incomplete si; SI.declare_pb_is_incomplete si;
None (* TODO: theory combination?*) | LIA_const _ | LIA_other _ -> ()
| LIA_const _ | LIA_other _ ->
None
let create_and_setup si = let create_and_setup si =
Log.debug 2 "(th-lia.setup)"; Log.debug 2 "(th-lia.setup)";

99
src/lra/sidekick_arith_lra.ml
View file

@ -218,27 +218,25 @@ module Make(A : ARG) : S with module A = A = struct
Fmt.fprintf out "(@[%a@ :l1 %a@ :l2 %a@])" Predicate.pp p LE.pp l1 LE.pp l2 Fmt.fprintf out "(@[%a@ :l1 %a@ :l2 %a@])" Predicate.pp p LE.pp l1 LE.pp l2
(* turn the term into a linear expression. Apply [f] on leaves. *) (* turn the term into a linear expression. Apply [f] on leaves. *)
let rec as_linexp ~f (t:T.t) : LE.t = let rec as_linexp (t:T.t) : LE.t =
let open LE.Infix in let open LE.Infix in
match A.view_as_lra t with match A.view_as_lra t with
| LRA_other _ -> LE.monomial1 (f t) | LRA_other _ -> LE.monomial1 t
| LRA_pred _ | LRA_simplex_pred _ -> | LRA_pred _ | LRA_simplex_pred _ ->
Error.errorf "type error: in linexp, LRA predicate %a" T.pp t Error.errorf "type error: in linexp, LRA predicate %a" T.pp t
| LRA_op (op, t1, t2) -> | LRA_op (op, t1, t2) ->
let t1 = as_linexp ~f t1 in let t1 = as_linexp t1 in
let t2 = as_linexp ~f t2 in let t2 = as_linexp t2 in
begin match op with begin match op with
| Plus -> t1 + t2 | Plus -> t1 + t2
| Minus -> t1 - t2 | Minus -> t1 - t2
end end
| LRA_mult (n, x) -> | LRA_mult (n, x) ->
let t = as_linexp ~f x in let t = as_linexp x in
LE.( n * t ) LE.( n * t )
| LRA_simplex_var v -> LE.monomial1 v | LRA_simplex_var v -> LE.monomial1 v
| LRA_const q -> LE.of_const q | LRA_const q -> LE.of_const q
let as_linexp_id = as_linexp ~f:CCFun.id
(* return a variable that is equal to [le_comb] in the simplex. *) (* return a variable that is equal to [le_comb] in the simplex. *)
let var_encoding_comb ~pre self (le_comb:LE_.Comb.t) : T.t = let var_encoding_comb ~pre self (le_comb:LE_.Comb.t) : T.t =
match LE_.Comb.as_singleton le_comb with match LE_.Comb.as_singleton le_comb with
@ -277,19 +275,11 @@ module Make(A : ARG) : S with module A = A = struct
PA.add_clause lits pr PA.add_clause lits pr
(* preprocess linear expressions away *) (* preprocess linear expressions away *)
let preproc_lra (self:state) si (module PA:SI.PREPROCESS_ACTS) let preproc_lra (self:state) si
(t:T.t) : (T.t * SI.proof_step Iter.t) option = (module PA:SI.PREPROCESS_ACTS) (t:T.t) : unit =
Log.debugf 50 (fun k->k "(@[lra.preprocess@ %a@])" T.pp t); Log.debugf 50 (fun k->k "(@[lra.preprocess@ %a@])" T.pp t);
let tst = SI.tst si in let tst = SI.tst si in
(* preprocess subterm *)
let preproc_t ~steps t =
let u, pr = SI.preprocess_term si (module PA) t in
T.Tbl.replace self.in_model t ();
CCOpt.iter (fun s -> steps := s :: !steps) pr;
u
in
(* tell the CC this term exists *) (* tell the CC this term exists *)
let declare_term_to_cc t = let declare_term_to_cc t =
Log.debugf 50 (fun k->k "(@[simplex2.declare-term-to-cc@ %a@])" T.pp t); Log.debugf 50 (fun k->k "(@[simplex2.declare-term-to-cc@ %a@])" T.pp t);
@ -307,20 +297,18 @@ module Make(A : ARG) : S with module A = A = struct
T.Tbl.add self.encoded_eqs t (); T.Tbl.add self.encoded_eqs t ();
(* encode [t <=> (u1 /\ u2)] *) (* encode [t <=> (u1 /\ u2)] *)
let lit_t = PA.mk_lit_nopreproc t in let lit_t = PA.mk_lit t in
let lit_u1 = PA.mk_lit_nopreproc u1 in let lit_u1 = PA.mk_lit u1 in
let lit_u2 = PA.mk_lit_nopreproc u2 in let lit_u2 = PA.mk_lit u2 in
add_clause_lra_ (module PA) [SI.Lit.neg lit_t; lit_u1]; add_clause_lra_ (module PA) [SI.Lit.neg lit_t; lit_u1];
add_clause_lra_ (module PA) [SI.Lit.neg lit_t; lit_u2]; add_clause_lra_ (module PA) [SI.Lit.neg lit_t; lit_u2];
add_clause_lra_ (module PA) add_clause_lra_ (module PA)
[SI.Lit.neg lit_u1; SI.Lit.neg lit_u2; lit_t]; [SI.Lit.neg lit_u1; SI.Lit.neg lit_u2; lit_t];
); );
None
| LRA_pred (pred, t1, t2) -> | LRA_pred (pred, t1, t2) ->
let steps = ref [] in let l1 = as_linexp t1 in
let l1 = as_linexp ~f:(preproc_t ~steps) t1 in let l2 = as_linexp t2 in
let l2 = as_linexp ~f:(preproc_t ~steps) t2 in
let le = LE.(l1 - l2) in let le = LE.(l1 - l2) in
let le_comb, le_const = LE.comb le, LE.const le in let le_comb, le_const = LE.comb le, LE.const le in
let le_const = A.Q.neg le_const in let le_const = A.Q.neg le_const in
@ -329,10 +317,7 @@ module Make(A : ARG) : S with module A = A = struct
begin match LE_.Comb.as_singleton le_comb, pred with begin match LE_.Comb.as_singleton le_comb, pred with
| None, _ -> | None, _ ->
(* non trivial linexp, give it a fresh name in the simplex *) (* non trivial linexp, give it a fresh name in the simplex *)
let proxy = var_encoding_comb self ~pre:"_le" le_comb in declare_term_to_cc t;
let pr_def = SI.P.define_term proxy t PA.proof in
steps := pr_def :: !steps;
declare_term_to_cc proxy;
let op = let op =
match pred with match pred with
@ -343,15 +328,14 @@ module Make(A : ARG) : S with module A = A = struct
| Gt -> S_op.Gt | Gt -> S_op.Gt
in in
let new_t = A.mk_lra tst (LRA_simplex_pred (proxy, op, le_const)) in let new_t = A.mk_lra tst (LRA_simplex_pred (t, op, le_const)) in
begin begin
let lit = PA.mk_lit_nopreproc new_t in let lit = PA.mk_lit new_t in
let constr = SimpSolver.Constraint.mk proxy op le_const in let constr = SimpSolver.Constraint.mk t op le_const in
SimpSolver.declare_bound self.simplex constr (Tag.Lit lit); SimpSolver.declare_bound self.simplex constr (Tag.Lit lit);
end; end;
Log.debugf 10 (fun k->k "(@[lra.preprocess:@ %a@ :into %a@])" T.pp t T.pp new_t); Log.debugf 10 (fun k->k "(@[lra.preprocess:@ %a@ :into %a@])" T.pp t T.pp new_t);
Some (new_t, Iter.of_list !steps)
| Some (coeff, v), pred -> | Some (coeff, v), pred ->
(* [c . v <= const] becomes a direct simplex constraint [v <= const/c] *) (* [c . v <= const] becomes a direct simplex constraint [v <= const/c] *)
@ -370,45 +354,33 @@ module Make(A : ARG) : S with module A = A = struct
let new_t = A.mk_lra tst (LRA_simplex_pred (v, op, q)) in let new_t = A.mk_lra tst (LRA_simplex_pred (v, op, q)) in
begin begin
let lit = PA.mk_lit_nopreproc new_t in let lit = PA.mk_lit new_t in
let constr = SimpSolver.Constraint.mk v op q in let constr = SimpSolver.Constraint.mk v op q in
SimpSolver.declare_bound self.simplex constr (Tag.Lit lit); SimpSolver.declare_bound self.simplex constr (Tag.Lit lit);
end; end;
Log.debugf 10 (fun k->k "lra.preprocess@ :%a@ :into %a" T.pp t T.pp new_t); Log.debugf 10 (fun k->k "lra.preprocess@ :%a@ :into %a" T.pp t T.pp new_t);
Some (new_t, Iter.of_list !steps)
end end
| LRA_op _ | LRA_mult _ -> | LRA_op _ | LRA_mult _ ->
let steps = ref [] in let steps = ref [] in
let le = as_linexp ~f:(preproc_t ~steps) t in let le = as_linexp t in
let le_comb, le_const = LE.comb le, LE.const le in let le_comb, le_const = LE.comb le, LE.const le in
if A.Q.(le_const = zero) then ( if A.Q.(le_const = zero) then (
(* if there is no constant, define [proxy] as [proxy := le_comb] and (* if there is no constant, define [t] as [t := le_comb] *)
return [proxy] *) declare_term_to_cc t;
let proxy = var_encoding_comb self ~pre:"_le" le_comb in
begin
let pr_def = SI.P.define_term proxy t PA.proof in
steps := pr_def :: !steps;
end;
declare_term_to_cc proxy;
Some (proxy, Iter.of_list !steps)
) else ( ) else (
(* a bit more complicated: we cannot just define [proxy := le_comb] (* a bit more complicated: we cannot just define [t := le_comb]
because of the coefficient. because of the coefficient.
Instead we assert [proxy - le_comb = le_const] using a secondary Instead we assert [t - le_comb = le_const] using a secondary
variable [proxy2 := le_comb - proxy] variable [proxy2 := t - le_comb]
and asserting [proxy2 = -le_const] *) and asserting [proxy2 = le_const] *)
let proxy = fresh_term self ~pre:"_le" (T.ty t) in
begin
let pr_def = SI.P.define_term proxy t PA.proof in
steps := pr_def :: !steps;
end;
let proxy2 = fresh_term self ~pre:"_le_diff" (T.ty t) in let proxy2 = fresh_term self ~pre:"_le_diff" (T.ty t) in
(* TODO
let pr_def2 = let pr_def2 =
SI.P.define_term proxy (A.mk_lra tst (LRA_op (Minus, t, proxy))) PA.proof SI.P.define_term proxy2
(A.mk_lra tst (LRA_op (Minus, t, A.mk_lra tst (LRA_const le_const)))) PA.proof
in in
SimpSolver.add_var self.simplex proxy; SimpSolver.add_var self.simplex proxy;
@ -425,21 +397,22 @@ module Make(A : ARG) : S with module A = A = struct
declare_term_to_cc proxy2; declare_term_to_cc proxy2;
add_clause_lra_ ~using:Iter.(return pr_def2) (module PA) [ add_clause_lra_ ~using:Iter.(return pr_def2) (module PA) [
PA.mk_lit_nopreproc (A.mk_lra tst (LRA_simplex_pred (proxy2, Leq, A.Q.neg le_const))) PA.mk_lit (A.mk_lra tst (LRA_simplex_pred (proxy2, Leq, A.Q.neg le_const)))
]; ];
add_clause_lra_ ~using:Iter.(return pr_def2) (module PA) [ add_clause_lra_ ~using:Iter.(return pr_def2) (module PA) [
PA.mk_lit_nopreproc (A.mk_lra tst (LRA_simplex_pred (proxy2, Geq, A.Q.neg le_const))) PA.mk_lit (A.mk_lra tst (LRA_simplex_pred (proxy2, Geq, A.Q.neg le_const)))
]; ];
Some (proxy, Iter.of_list !steps) Some (proxy, Iter.of_list !steps)
*)
()
) )
| LRA_other t when A.has_ty_real t -> None | LRA_other t when A.has_ty_real t -> ()
| LRA_const _ | LRA_simplex_pred _ | LRA_simplex_var _ | LRA_other _ -> | LRA_const _ | LRA_simplex_pred _ | LRA_simplex_var _ | LRA_other _ ->
None ()
let simplify (self:state) (_recurse:_) (t:T.t) : (T.t * SI.proof_step Iter.t) option = let simplify (self:state) (_recurse:_) (t:T.t) : (T.t * SI.proof_step Iter.t) option =
let proof_eq t u = let proof_eq t u =
A.lemma_lra A.lemma_lra
(Iter.return (SI.Lit.atom self.tst (A.mk_eq self.tst t u))) self.proof (Iter.return (SI.Lit.atom self.tst (A.mk_eq self.tst t u))) self.proof
@ -451,7 +424,7 @@ module Make(A : ARG) : S with module A = A = struct
match A.view_as_lra t with match A.view_as_lra t with
| LRA_op _ | LRA_mult _ -> | LRA_op _ | LRA_mult _ ->
let le = as_linexp_id t in let le = as_linexp t in
if LE.is_const le then ( if LE.is_const le then (
let c = LE.const le in let c = LE.const le in
let u = A.mk_lra self.tst (LRA_const c) in let u = A.mk_lra self.tst (LRA_const c) in
@ -459,7 +432,7 @@ module Make(A : ARG) : S with module A = A = struct
Some (u, Iter.return pr) Some (u, Iter.return pr)
) else None ) else None
| LRA_pred (pred, l1, l2) -> | LRA_pred (pred, l1, l2) ->
let le = LE.(as_linexp_id l1 - as_linexp_id l2) in let le = LE.(as_linexp l1 - as_linexp l2) in
if LE.is_const le then ( if LE.is_const le then (
let c = LE.const le in let c = LE.const le in
let is_true = match pred with let is_true = match pred with
@ -527,7 +500,7 @@ module Make(A : ARG) : S with module A = A = struct
let t2 = N.term n2 in let t2 = N.term n2 in
let t1, t2 = if T.compare t1 t2 > 0 then t2, t1 else t1, t2 in let t1, t2 = if T.compare t1 t2 > 0 then t2, t1 else t1, t2 in
let le = LE.(as_linexp_id t1 - as_linexp_id t2) in let le = LE.(as_linexp t1 - as_linexp t2) in
let le_comb, le_const = LE.comb le, LE.const le in let le_comb, le_const = LE.comb le, LE.const le in
let le_const = A.Q.neg le_const in let le_const = A.Q.neg le_const in

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

@ -129,6 +129,19 @@ module Make(A : ARG)
module CC = Sidekick_cc.Make(CC_actions) module CC = Sidekick_cc.Make(CC_actions)
module N = CC.N module N = CC.N
(* delayed actions. We avoid doing them on the spot because, when
triggered by a theory, they might go back to the theory "too early". *)
type delayed_action =
| DA_add_clause of {
c: lit list;
pr: proof_step;
keep: bool;
}
| DA_add_lit of {
default_pol: bool option;
lit: lit;
}
(** Internal solver, given to theories and to Msat *) (** Internal solver, given to theories and to Msat *)
module Solver_internal = struct module Solver_internal = struct
module T = T module T = T
@ -232,8 +245,7 @@ module Make(A : ARG)
module type PREPROCESS_ACTS = sig module type PREPROCESS_ACTS = sig
val proof : proof val proof : proof
val mk_lit_nopreproc : ?sign:bool -> term -> lit val mk_lit : ?sign:bool -> term -> lit
val mk_lit : ?sign:bool -> term -> lit * proof_step option
val add_clause : lit list -> proof_step -> unit val add_clause : lit list -> proof_step -> unit
val add_lit : ?default_pol:bool -> lit -> unit val add_lit : ?default_pol:bool -> lit -> unit
end end
@ -246,30 +258,35 @@ module Make(A : ARG)
ty_st: Ty.store; ty_st: Ty.store;
cc: CC.t lazy_t; (** congruence closure *) cc: CC.t lazy_t; (** congruence closure *)
proof: proof; (** proof logger *) proof: proof; (** proof logger *)
registry: Registry.t;
mutable on_progress: unit -> unit;
mutable on_partial_check: (t -> theory_actions -> lit Iter.t -> unit) list;
mutable on_final_check: (t -> theory_actions -> lit Iter.t -> unit) list;
mutable preprocess: preprocess_hook list;
mutable model_ask: model_ask_hook list;
mutable model_complete: model_completion_hook list;
simp: Simplify.t;
preprocessed: unit Term.Tbl.t;
delayed_actions: delayed_action Queue.t;
mutable t_defs : (term*term) list; (* term definitions *)
mutable th_states : th_states; (** Set of theories *)
mutable level: int;
mutable complete: bool;
stat: Stat.t; stat: Stat.t;
count_axiom: int Stat.counter; count_axiom: int Stat.counter;
count_preprocess_clause: int Stat.counter; count_preprocess_clause: int Stat.counter;
count_conflict: int Stat.counter; count_conflict: int Stat.counter;
count_propagate: int Stat.counter; count_propagate: int Stat.counter;
registry: Registry.t;
mutable on_progress: unit -> unit;
simp: Simplify.t;
mutable preprocess: preprocess_hook list;
mutable model_ask: model_ask_hook list;
mutable model_complete: model_completion_hook list;
preprocess_cache: (Term.t * proof_step Bag.t) Term.Tbl.t;
mutable t_defs : (term*term) list; (* term definitions *)
mutable th_states : th_states; (** Set of theories *)
mutable on_partial_check: (t -> theory_actions -> lit Iter.t -> unit) list;
mutable on_final_check: (t -> theory_actions -> lit Iter.t -> unit) list;
mutable level: int;
mutable complete: bool;
} }
and preprocess_hook = and preprocess_hook =
t -> t ->
preprocess_actions -> preprocess_actions ->
term -> (term * proof_step Iter.t) option term -> unit
and model_ask_hook = and model_ask_hook =
recurse:(t -> CC.N.t -> term) -> recurse:(t -> CC.N.t -> term) ->
@ -329,222 +346,160 @@ module Make(A : ARG)
Stat.incr self.count_axiom; Stat.incr self.count_axiom;
A.add_clause_in_pool ~pool lits proof A.add_clause_in_pool ~pool lits proof
let add_sat_lit _self ?default_pol (acts:theory_actions) (lit:Lit.t) : unit = let add_sat_lit_ _self ?default_pol (acts:theory_actions) (lit:Lit.t) : unit =
let (module A) = acts in let (module A) = acts in
A.add_lit ?default_pol lit A.add_lit ?default_pol lit
(* actual preprocessing logic, acting on terms. let delayed_add_lit (self:t) ?default_pol (lit:Lit.t) : unit =
this calls all the preprocessing hooks on subterms, ensuring Queue.push (DA_add_lit {default_pol; lit}) self.delayed_actions
a fixpoint. *)
let preprocess_term_ (self:t) (module A0:PREPROCESS_ACTS) (t:term) : term * proof_step option =
let mk_lit_nopreproc ?sign t = Lit.atom ?sign self.tst t in (* no further simplification *)
(* compute and cache normal form [u] of [t]. let delayed_add_clause (self:t) ~keep (c:Lit.t list) (pr:proof_step) : unit =
Queue.push (DA_add_clause {c;pr;keep}) self.delayed_actions
Also cache a list of proofs [ps] such that [ps |- t=u] by CC. (* preprocess a term. We assume the term has been simplified already. *)
It is important that we cache the proofs here, because let preprocess_term_ (self:t) (t0:term) : unit =
next time we preprocess [t], we will have to re-emit the same let module A = struct
proofs, even though we will not do any actual preprocessing work. let proof = self.proof
*) let mk_lit ?sign t : Lit.t = Lit.atom self.tst ?sign t
let rec preproc_rec ~steps t : term = let add_lit ?default_pol lit : unit = delayed_add_lit self ?default_pol lit
match Term.Tbl.find self.preprocess_cache t with let add_clause c pr : unit = delayed_add_clause self ~keep:true c pr
| u, pr_u -> end in
steps := Bag.append pr_u !steps; let acts = (module A:PREPROCESS_ACTS) in
u
| exception Not_found -> (* how to preprocess a term and its subterms *)
(* try rewrite at root *) let rec preproc_rec_ t =
let steps = ref Bag.empty in if not (Term.Tbl.mem self.preprocessed t) then (
let t1 = preproc_with_hooks ~steps t self.preprocess in Term.Tbl.add self.preprocessed t ();
Log.debugf 50 (fun k->k "(@[smt.preprocess@ %a@])" Term.pp t);
(* map subterms *)
let t2 = Term.map_shallow self.tst (preproc_rec ~steps) t1 in
let u =
if not (Term.equal t t2) then (
preproc_rec ~steps t2 (* fixpoint *)
) else (
t2
)
in
(* signal boolean subterms, so as to decide them (* signal boolean subterms, so as to decide them
in the SAT solver *) in the SAT solver *)
if Ty.is_bool (Term.ty u) then ( if Ty.is_bool (Term.ty t) then (
Log.debugf 5 Log.debugf 5
(fun k->k "(@[solver.map-bool-subterm-to-lit@ :subterm %a@])" Term.pp u); (fun k->k "(@[solver.map-bool-subterm-to-lit@ :subterm %a@])" Term.pp t);
(* make a literal (already preprocessed) *) (* make a literal *)
let lit = mk_lit_nopreproc u in let lit = Lit.atom self.tst t in
(* ensure that SAT solver has a boolean atom for [u] *) (* ensure that SAT solver has a boolean atom for [u] *)
A0.add_lit lit; delayed_add_lit self lit;
(* also map [sub] to this atom in the congruence closure, for propagation *) (* also map [sub] to this atom in the congruence closure, for propagation *)
let cc = cc self in let cc = cc self in
CC.set_as_lit cc (CC.add_term cc u) lit; CC.set_as_lit cc (CC.add_term cc t) lit;
); );
if t != u then ( List.iter
Log.debugf 5 (fun f -> f self acts t) self.preprocess;
(fun k->k "(@[smt-solver.preprocess.term@ :from %a@ :to %a@])"
Term.pp t Term.pp u);
);
let pr_t_u = !steps in (* process sub-terms *)
Term.Tbl.add self.preprocess_cache t (u, pr_t_u); Term.iter_shallow self.tst preproc_rec_ t;
u )
(* try each function in [hooks] successively *)
and preproc_with_hooks ~steps t hooks : term =
let[@inline] add_step s = steps := Bag.cons s !steps in
match hooks with
| [] -> t
| h :: hooks_tl ->
(* call hook, using [pacts] which will ensure all new
literals and clauses are also preprocessed *)
match h self (Lazy.force pacts) t with
| None -> preproc_with_hooks ~steps t hooks_tl
| Some (u, pr_u) ->
Iter.iter add_step pr_u;
preproc_rec ~steps u
(* create literal and preprocess it with [pacts], which uses [A0]
for the base operations, and preprocesses new literals and clauses
recursively. *)
and mk_lit ?sign t : _ * proof_step option =
let steps = ref Bag.empty in
let u = preproc_rec ~steps t in
let pr_t_u =
if not (Term.equal t u) then (
Log.debugf 10
(fun k->k "(@[smt-solver.preprocess.t@ :t %a@ :into %a@])"
Term.pp t Term.pp u);
let p =
A.P.lemma_preprocess t u ~using:(Bag.to_iter !steps) self.proof
in in
Some p preproc_rec_ t0
) else None
in
Lit.atom self.tst ?sign u, pr_t_u
and preprocess_lit ~steps (lit:lit) : lit = let simplify_lit_ (self:t) (lit:Lit.t) : Lit.t * proof_step option =
let t = Lit.term lit in let t = Lit.term lit in
let sign = Lit.sign lit in let sign = Lit.sign lit in
let lit, pr = mk_lit ~sign t in let u, pr = match simplify_t self t with
CCOpt.iter (fun s -> steps := s :: !steps) pr; | None -> t, None
lit | Some (u, pr_t_u) ->
Log.debugf 30
(fun k->k "(@[smt-solver.simplify@ :t %a@ :into %a@])"
Term.pp t Term.pp u);
u, Some pr_t_u
in
preprocess_term_ self u;
Lit.atom self.tst ~sign u, pr
(* wrap [A0] so that all operations go throught preprocessing *) module type ARR = sig
and pacts = lazy ( type 'a t
(module struct val map : ('a -> 'b) -> 'a t -> 'b t
let proof = A0.proof val to_iter : 'a t -> 'a Iter.t
end
let add_lit ?default_pol lit = module Preprocess_clause(A: ARR) = struct
(* just drop the proof *) (* preprocess a clause's literals, possibly emitting a proof
(* TODO: add a clause instead [lit => preprocess(lit)]? *) for the preprocessing. *)
let lit = preprocess_lit ~steps:(ref []) lit in let top (self:t)
A0.add_lit ?default_pol lit (c:lit A.t) (pr_c:proof_step) : lit A.t * proof_step =
let add_clause c pr_c =
Stat.incr self.count_preprocess_clause;
let steps = ref [] in let steps = ref [] in
let c' = CCList.map (preprocess_lit ~steps) c in
(* simplify a literal, then preprocess it *)
let[@inline] simp_lit lit =
let lit, pr = simplify_lit_ self lit in
CCOpt.iter (fun pr -> steps := pr :: !steps) pr;
lit
in
let c' = A.map simp_lit c in
let pr_c' = let pr_c' =
A.P.lemma_rw_clause pr_c if !steps=[] then pr_c
~res:(Iter.of_list c') else (
~using:(Iter.of_list !steps) proof Stat.incr self.count_preprocess_clause;
P.lemma_rw_clause pr_c
~res:(A.to_iter c')
~using:(Iter.of_list !steps) self.proof
)
in in
A0.add_clause c' pr_c' c', pr_c'
end[@@inline]
let mk_lit_nopreproc = mk_lit_nopreproc module PC_list = Preprocess_clause(CCList)
module PC_arr = Preprocess_clause(IArray)
let mk_lit = mk_lit let preprocess_clause_ = PC_list.top
end : PREPROCESS_ACTS) let preprocess_clause_iarray_ = PC_arr.top
) in
let steps = ref Bag.empty in module type PERFORM_ACTS = sig
let[@inline] add_step s = steps := Bag.cons s !steps in type t
val add_clause : solver -> t -> keep:bool -> lit list -> proof_step -> unit
val add_lit : solver -> t -> ?default_pol:bool -> lit -> unit
end
(* simplify the term *) module Perform_delayed(A : PERFORM_ACTS) = struct
let t1, pr_1 = simp_t self t in (* perform actions that were delayed *)
CCOpt.iter add_step pr_1; let top (self:t) (acts:A.t) : unit =
while not (Queue.is_empty self.delayed_actions) do
let act = Queue.pop self.delayed_actions in
begin match act with
| DA_add_clause {c; pr=pr_c; keep} ->
let c', pr_c' = preprocess_clause_ self c pr_c in
A.add_clause self acts ~keep c' pr_c'
(* preprocess *) | DA_add_lit {default_pol; lit} ->
let u = preproc_rec ~steps t1 in preprocess_term_ self (Lit.term lit);
A.add_lit self acts ?default_pol lit
end
done
end[@@inline]
(* emit [|- t=u] *) module Perform_delayed_th = Perform_delayed(struct
let pr_u = type t = theory_actions
if not (Term.equal t u) then ( let add_clause self acts ~keep c pr : unit =
let p = P.lemma_preprocess t u ~using:(Bag.to_iter !steps) self.proof in add_sat_clause_ self acts ~keep c pr
Some p let add_lit self acts ?default_pol lit : unit =
) else None add_sat_lit_ self acts ?default_pol lit
in
u, pr_u
(* return preprocessed lit *)
let preprocess_lit_ ~steps (self:t) (pacts:preprocess_actions) (lit:lit) : lit =
let t = Lit.term lit in
let sign = Lit.sign lit in
let u, pr_u = preprocess_term_ self pacts t in
CCOpt.iter (fun s -> steps := s :: !steps) pr_u;
Lit.atom self.tst ~sign u
(* add a clause using [acts] *)
let add_clause_ self acts lits (proof:proof_step) : unit =
add_sat_clause_ self acts ~keep:true lits proof
let[@inline] add_lit _self (acts:theory_actions) ?default_pol lit : unit =
let (module A) = acts in
A.add_lit ?default_pol lit
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
end) end)
let preprocess_clause_ (self:t) (acts:theory_actions) let[@inline] add_clause_temp self _acts c (proof:proof_step) : unit =
(c:lit list) (proof:proof_step) : lit list * proof_step = let c, proof = preprocess_clause_ self c proof in
let steps = ref [] in delayed_add_clause self ~keep:false c proof
let pacts = preprocess_acts_of_acts self acts in
let c = CCList.map (preprocess_lit_ ~steps self pacts) c in
let pr =
P.lemma_rw_clause proof
~res:(Iter.of_list c) ~using:(Iter.of_list !steps) self.proof
in
c, pr
(* make literal and preprocess it *) let[@inline] add_clause_permanent self _acts c (proof:proof_step) : unit =
let[@inline] mk_plit (self:t) (pacts:preprocess_actions) ?sign (t:term) : lit = let c, proof = preprocess_clause_ self c proof in
delayed_add_clause self ~keep:true c proof
let[@inline] mk_lit (self:t) (_acts:theory_actions) ?sign t : lit =
Lit.atom self.tst ?sign t
let[@inline] add_lit self _acts ?default_pol lit =
delayed_add_lit self ?default_pol lit
let add_lit_t self _acts ?sign t =
let lit = Lit.atom self.tst ?sign t in let lit = Lit.atom self.tst ?sign t in
let steps = ref [] in let lit, _ = simplify_lit_ self lit in
preprocess_lit_ ~steps self pacts lit delayed_add_lit self lit
let[@inline] preprocess_term self
(pacts:preprocess_actions) (t:term) : term * _ option =
preprocess_term_ self pacts t
let[@inline] add_clause_temp self acts c (proof:proof_step) : unit =
let c, proof = preprocess_clause_ self acts c proof in
add_sat_clause_ self acts ~keep:false c proof
let[@inline] add_clause_permanent self acts c (proof:proof_step) : unit =
let c, proof = preprocess_clause_ self acts c proof in
add_sat_clause_ self acts ~keep:true c proof
let[@inline] mk_lit (self:t) (acts:theory_actions) ?sign t : lit =
let pacts = preprocess_acts_of_acts self acts in
mk_plit self pacts ?sign t
let add_lit_t self acts ?sign t =
let pacts = preprocess_acts_of_acts self acts in
let lit = mk_plit self pacts ?sign t in
add_lit self acts lit
let on_final_check self f = self.on_final_check <- f :: self.on_final_check let on_final_check self f = self.on_final_check <- f :: self.on_final_check
let on_partial_check self f = self.on_partial_check <- f :: self.on_partial_check let on_partial_check self f = self.on_partial_check <- f :: self.on_partial_check
@ -607,7 +562,9 @@ module Make(A : ARG)
while true do while true do
(* TODO: theory combination *) (* TODO: theory combination *)
List.iter (fun f -> f self acts lits) self.on_final_check; List.iter (fun f -> f self acts lits) self.on_final_check;
Perform_delayed_th.top self acts;
CC.check cc acts; CC.check cc acts;
Perform_delayed_th.top self acts;
if not @@ CC.new_merges cc then ( if not @@ CC.new_merges cc then (
raise_notrace E_loop_exit raise_notrace E_loop_exit
); );
@ -616,6 +573,7 @@ module Make(A : ARG)
() ()
) else ( ) else (
List.iter (fun f -> f self acts lits) self.on_partial_check; List.iter (fun f -> f self acts lits) self.on_partial_check;
Perform_delayed_th.top self acts;
); );
() ()
@ -664,7 +622,8 @@ module Make(A : ARG)
model_ask=[]; model_ask=[];
model_complete=[]; model_complete=[];
registry=Registry.create(); registry=Registry.create();
preprocess_cache=Term.Tbl.create 32; preprocessed=Term.Tbl.create 32;
delayed_actions=Queue.create();
count_axiom = Stat.mk_int stat "solver.th-axioms"; count_axiom = Stat.mk_int stat "solver.th-axioms";
count_preprocess_clause = Stat.mk_int stat "solver.preprocess-clause"; count_preprocess_clause = Stat.mk_int stat "solver.preprocess-clause";
count_propagate = Stat.mk_int stat "solver.th-propagations"; count_propagate = Stat.mk_int stat "solver.th-propagations";
@ -816,38 +775,13 @@ module Make(A : ARG)
let reset_last_res_ self = self.last_res <- None let reset_last_res_ self = self.last_res <- None
let preprocess_acts_of_solver_
(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
let add_clause c pr =
Sat_solver.add_clause self.solver c pr
end)
(* preprocess literal *)
let preprocess_lit_ ~steps (self:t) (lit:lit) : lit =
let pacts = preprocess_acts_of_solver_ self in
Solver_internal.preprocess_lit_ ~steps self.si pacts lit
(* preprocess clause, return new proof *) (* preprocess clause, return new proof *)
let preprocess_clause_ (self:t) let preprocess_clause_ (self:t)
(c:lit IArray.t) (pr:proof_step) : lit IArray.t * proof_step = (c:lit IArray.t) (pr:proof_step) : lit IArray.t * proof_step =
let steps = ref [] in Solver_internal.preprocess_clause_iarray_ self.si c pr
let c = IArray.map (preprocess_lit_ self ~steps) c in
let pr =
P.lemma_rw_clause pr
~res:(IArray.to_iter c) ~using:(Iter.of_list !steps) self.proof
in
c, pr
(* make a literal from a term, ensuring it is properly preprocessed *) let[@inline] mk_lit_t (self:t) ?sign (t:term) : lit =
let mk_lit_t (self:t) ?sign (t:term) : lit = Lit.atom self.si.tst ?sign t
let pacts = preprocess_acts_of_solver_ self in
Solver_internal.mk_plit self.si pacts ?sign t
(** {2 Main} *) (** {2 Main} *)
@ -867,22 +801,26 @@ module Make(A : ARG)
let add_clause_nopreproc_l_ self c p = add_clause_nopreproc_ self (IArray.of_list c) p let add_clause_nopreproc_l_ self c p = add_clause_nopreproc_ self (IArray.of_list c) p
module Perform_delayed_ = Solver_internal.Perform_delayed(struct
type nonrec t = t
let add_clause _si solver ~keep:_ c pr : unit =
add_clause_nopreproc_l_ solver c pr
let add_lit _si solver ?default_pol lit : unit =
Sat_solver.add_lit solver.solver ?default_pol lit
end)
let add_clause (self:t) (c:lit IArray.t) (proof:proof_step) : unit = let add_clause (self:t) (c:lit IArray.t) (proof:proof_step) : unit =
let c, proof = preprocess_clause_ self c proof in let c, proof = preprocess_clause_ self c proof in
add_clause_nopreproc_ self c proof add_clause_nopreproc_ self c proof;
Perform_delayed_.top self.si self; (* finish preproc *)
()
let add_clause_l self c p = add_clause self (IArray.of_list c) p let add_clause_l self c p = add_clause self (IArray.of_list c) p
let assert_terms self c = let assert_terms self c =
let steps = ref [] in
let c = CCList.map (fun t -> Lit.atom (tst self) t) c in let c = CCList.map (fun t -> Lit.atom (tst self) t) c in
let c = CCList.map (preprocess_lit_ ~steps self) c in let pr_c = P.emit_input_clause (Iter.of_list c) self.proof in
(* TODO: if c != c0 then P.emit_redundant_clause c add_clause_l self c pr_c
because we jsut preprocessed it away? *)
let pr = P.emit_input_clause (Iter.of_list c) self.proof in
let pr = P.lemma_rw_clause pr
~res:(Iter.of_list c) ~using:(Iter.of_list !steps) self.proof in
add_clause_l self c pr
let assert_term self t = assert_terms self [t] let assert_term self t = assert_terms self [t]

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

@ -53,12 +53,6 @@ module type ARG = sig
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. *)
val check_congruence_classes : bool
(** Configuration: add final-check handler to verify if new boolean formulas
are present in the congruence closure.
Only enable if some theories are susceptible to
create boolean formulas during the proof search. *)
include PROOF include PROOF
with type proof := S.P.t with type proof := S.P.t
and type proof_step := S.P.proof_step and type proof_step := S.P.proof_step
@ -115,13 +109,11 @@ 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;
preprocessed: (T.t * SI.proof_step Iter.t) option T.Tbl.t;
gensym: A.Gensym.t; gensym: A.Gensym.t;
} }
let create tst ty_st : state = let create tst ty_st : state =
{ tst; ty_st; { tst; ty_st;
preprocessed=T.Tbl.create 64;
gensym=A.Gensym.create tst; gensym=A.Gensym.create tst;
} }
@ -216,223 +208,99 @@ module Make(A : ARG) : S with module A = A = struct
let proxy = fresh_term ~for_t ~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
let pr_p1 p s1 s2 = SI.P.proof_p1 s1 s2 p
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 preprocess_uncached_ self si (module PA:SI.PREPROCESS_ACTS)
(t:T.t) : (T.t * SI.proof_step Iter.t) option =
let steps = ref [] in
let add_step_ s = steps := s :: !steps in
let ret u =
if t==u then None
else Some (u, Iter.of_list !steps)
in
(* FIXME: make sure add-clause is delayed… perhaps return a vector of actions
or something like that *)
let add_clause_rw lits ~using ~c0 : unit =
PA.add_clause lits @@
SI.P.lemma_rw_clause c0 ~res:(Iter.of_list lits) ~using PA.proof
in
match A.view_as_bool t with
| B_ite (a,b,c) ->
let a', pr_a = SI.simp_t si a in
CCOpt.iter add_step_ pr_a;
begin match A.view_as_bool a' with
| B_bool true ->
(* [a |- ite a b c=b], [a=true] implies [ite a b c=b] *)
add_step_
(pr_p1_opt PA.proof pr_a @@ A.lemma_ite_true ~ite:t PA.proof);
ret b
| B_bool false ->
(* [¬a |- ite a b c=c], [a=false] implies [ite a b c=c] *)
add_step_
(pr_p1_opt PA.proof pr_a @@ A.lemma_ite_false ~ite:t PA.proof);
ret c
| _ ->
let b', pr_b = SI.simp_t si b in
CCOpt.iter add_step_ pr_b;
let c', pr_c = SI.simp_t si c in
CCOpt.iter add_step_ pr_c;
let t_ite = A.mk_bool self.tst (B_ite (a', b', c')) in
let lit_a = PA.mk_lit_nopreproc a' in
add_clause_rw [Lit.neg lit_a; PA.mk_lit_nopreproc (eq self.tst t_ite b')]
~using:Iter.(of_opt pr_a)
~c0:(A.lemma_ite_true ~ite:t PA.proof);
add_clause_rw [lit_a; PA.mk_lit_nopreproc (eq self.tst t_ite c')]
~using:Iter.(of_opt pr_a)
~c0:(A.lemma_ite_false ~ite:t PA.proof);
ret t_ite
end
| _ -> None
let preprocess self si pa t =
match T.Tbl.find_opt self.preprocessed t with
| None ->
let res = preprocess_uncached_ self si pa t in
T.Tbl.add self.preprocessed t res;
res
| Some r -> r
(* TODO: polarity? *) (* TODO: polarity? *)
let cnf (self:state) (si:SI.t) (module PA:SI.PREPROCESS_ACTS) let cnf (self:state) (si:SI.t)
(t:T.t) : (T.t * _ Iter.t) option = (module PA:SI.PREPROCESS_ACTS) (t:T.t) : unit =
Log.debugf 50 (fun k->k"(@[th-bool.cnf@ %a@])" T.pp t); Log.debugf 50 (fun k->k"(@[th-bool.cnf@ %a@])" T.pp t);
let steps = ref [] in
let[@inline] add_step s = steps := s :: !steps in
(* handle boolean equality *) (* handle boolean equality *)
let equiv_ _si ~is_xor ~for_t t_a t_b : Lit.t = let equiv_ _si ~is_xor ~t t_a t_b : unit =
let a = PA.mk_lit_nopreproc t_a in let a = PA.mk_lit t_a in
let b = PA.mk_lit_nopreproc t_b in let b = PA.mk_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_t ~mk_lit:PA.mk_lit_nopreproc ~pre:"equiv_" self in let lit = PA.mk_lit t in
let pr_def = SI.P.define_term t_proxy for_t PA.proof in
add_step pr_def;
let[@inline] add_clause c pr = PA.add_clause c pr in
(* proxy => a<=> b, (* proxy => a<=> b,
¬proxy => a xor b *) ¬proxy => a xor b *)
add_clause [Lit.neg proxy; Lit.neg a; b] PA.add_clause [Lit.neg lit; Lit.neg a; b]
(pr_p1 PA.proof pr_def @@ (if is_xor then A.lemma_bool_c "xor-e+" [t] PA.proof
if is_xor then A.lemma_bool_c "xor-e+" [for_t] PA.proof else A.lemma_bool_c "eq-e" [t; t_a] PA.proof);
else A.lemma_bool_c "eq-e" [for_t; t_a] PA.proof); PA.add_clause [Lit.neg lit; Lit.neg b; a]
add_clause [Lit.neg proxy; Lit.neg b; a] (if is_xor then A.lemma_bool_c "xor-e-" [t] PA.proof
(pr_p1 PA.proof pr_def @@ else A.lemma_bool_c "eq-e" [t; t_b] PA.proof);
if is_xor then A.lemma_bool_c "xor-e-" [for_t] PA.proof PA.add_clause [lit; a; b]
else A.lemma_bool_c "eq-e" [for_t; t_b] PA.proof); (if is_xor then A.lemma_bool_c "xor-i" [t; t_a] PA.proof
add_clause [proxy; a; b] else A.lemma_bool_c "eq-i+" [t] PA.proof);
(pr_p1 PA.proof pr_def @@ PA.add_clause [lit; Lit.neg a; Lit.neg b]
if is_xor then A.lemma_bool_c "xor-i" [for_t; t_a] PA.proof (if is_xor then A.lemma_bool_c "xor-i" [t; t_b] PA.proof
else A.lemma_bool_c "eq-i+" [for_t] PA.proof); else A.lemma_bool_c "eq-i-" [t] PA.proof);
add_clause [proxy; Lit.neg a; Lit.neg b]
(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 in
(* 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)] *)
let rec get_lit_for_term_ t : Lit.t option = begin match A.view_as_bool t with
match A.view_as_bool t with | B_opaque_bool _ -> ()
| B_opaque_bool _ -> None | B_bool _ -> ()
| B_bool _ -> None | B_not _ -> ()
| B_not u ->
let lit = get_lit_for_term_ u in
CCOpt.map Lit.neg lit
| 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 PA.mk_lit_nopreproc t_subs in let lit = PA.mk_lit t in
let t_proxy, proxy = fresh_lit ~for_t:t ~mk_lit:PA.mk_lit_nopreproc ~pre:"and_" self in let subs = List.map PA.mk_lit t_subs in
let pr_def = SI.P.define_term t_proxy t PA.proof in
add_step pr_def;
(* add clauses *) (* add clauses *)
List.iter2 List.iter2
(fun t_u u -> (fun t_u u ->
PA.add_clause PA.add_clause
[Lit.neg proxy; u] [Lit.neg lit; u]
(pr_p1 PA.proof pr_def @@ A.lemma_bool_c "and-e" [t; t_u] PA.proof)) (A.lemma_bool_c "and-e" [t; t_u] PA.proof))
t_subs subs; t_subs subs;
PA.add_clause (proxy :: List.map Lit.neg subs) PA.add_clause (lit :: List.map Lit.neg subs)
(pr_p1 PA.proof pr_def @@ A.lemma_bool_c "and-i" [t] PA.proof); (A.lemma_bool_c "and-i" [t] PA.proof);
Some proxy
| 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 PA.mk_lit_nopreproc t_subs in let subs = List.map PA.mk_lit t_subs in
let t_proxy, proxy = fresh_lit ~for_t:t ~mk_lit:PA.mk_lit_nopreproc ~pre:"or_" self in let lit = PA.mk_lit t in
let pr_def = SI.P.define_term t_proxy t PA.proof in
add_step pr_def;
(* add clauses *) (* add clauses *)
List.iter2 List.iter2
(fun t_u u -> (fun t_u u ->
PA.add_clause [Lit.neg u; proxy] PA.add_clause [Lit.neg u; lit]
(pr_p1 PA.proof pr_def @@ (A.lemma_bool_c "or-i" [t; t_u] PA.proof))
A.lemma_bool_c "or-i" [t; t_u] PA.proof))
t_subs subs; t_subs subs;
PA.add_clause (Lit.neg proxy :: subs) PA.add_clause (Lit.neg lit :: subs)
(pr_p1 PA.proof pr_def @@ A.lemma_bool_c "or-e" [t] PA.proof); (A.lemma_bool_c "or-e" [t] PA.proof);
Some proxy
| 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 *)
let t_args = Iter.to_list t_args in let t_args = Iter.to_list t_args in
let args = List.map (fun t -> Lit.neg (PA.mk_lit_nopreproc t)) t_args in let args = List.map (fun t -> Lit.neg (PA.mk_lit t)) t_args in
let u = PA.mk_lit_nopreproc t_u in let u = PA.mk_lit t_u in
let subs = u :: args in let subs = u :: args in
(* now the or-encoding *) (* now the or-encoding *)
let t_proxy, proxy = let lit = PA.mk_lit t in
fresh_lit ~for_t:t ~mk_lit:PA.mk_lit_nopreproc ~pre:"implies_" self in
let pr_def = SI.P.define_term t_proxy t PA.proof in
add_step pr_def;
(* add clauses *) (* add clauses *)
List.iter2 List.iter2
(fun t_u u -> (fun t_u u ->
PA.add_clause [Lit.neg u; proxy] PA.add_clause [Lit.neg u; lit]
(pr_p1 PA.proof pr_def @@ (A.lemma_bool_c "imp-i" [t; t_u] PA.proof))
A.lemma_bool_c "imp-i" [t_proxy; t_u] PA.proof))
(t_u::t_args) subs; (t_u::t_args) subs;
PA.add_clause (Lit.neg proxy :: subs) PA.add_clause (Lit.neg lit :: subs)
(pr_p1 PA.proof pr_def @@ (A.lemma_bool_c "imp-e" [t] PA.proof);
A.lemma_bool_c "imp-e" [t_proxy] PA.proof);
Some proxy
| B_ite _ | B_eq _ | B_neq _ -> None | B_ite (a,b,c) ->
| B_equiv (a,b) -> Some (equiv_ si ~for_t:t ~is_xor:false a b) let lit_a = PA.mk_lit a in
| B_xor (a,b) -> Some (equiv_ si ~for_t:t ~is_xor:true a b) PA.add_clause [Lit.neg lit_a; PA.mk_lit (eq self.tst t b)]
| B_atom _ -> None (A.lemma_ite_true ~ite:t PA.proof);
in PA.add_clause [lit_a; PA.mk_lit (eq self.tst t c)]
(A.lemma_ite_false ~ite:t PA.proof);
begin match get_lit_for_term_ t with | B_eq _ | B_neq _ -> ()
| None -> None | B_equiv (a,b) -> equiv_ si ~t ~is_xor:false a b
| Some lit -> | B_xor (a,b) -> equiv_ si ~t ~is_xor:true a b
let u = Lit.term lit in | B_atom _ -> ()
(* 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, Iter.of_list !steps)
end
(* check if new terms were added to the congruence closure, that can be turned
into clauses *)
let check_new_terms (self:state) si (acts:SI.theory_actions) (_trail:_ Iter.t) : unit =
let cc_ = SI.cc si in
let all_terms =
let open SI in
CC.all_classes cc_
|> Iter.flat_map CC.N.iter_class
|> Iter.map CC.N.term
in
let cnf_of t =
let pacts = SI.preprocess_acts_of_acts si acts in
cnf self si pacts t
in
begin
all_terms
(fun t -> match cnf_of t with
| None -> ()
| Some (u, pr_t_u) ->
Log.debugf 5
(fun k->k "(@[th-bool-static.final-check.cnf@ %a@ :yields %a@])"
T.pp t T.pp u);
(* produce a single step proof of [|- t=u] *)
let proof = SI.proof si in
let pr = SI.P.lemma_preprocess t u ~using:pr_t_u proof in
SI.CC.merge_t cc_ t u
(SI.CC.Expl.mk_theory t u [] pr);
());
end; end;
() ()
@ -440,12 +308,7 @@ module Make(A : ARG) : S with module A = A = struct
Log.debug 2 "(th-bool.setup)"; Log.debug 2 "(th-bool.setup)";
let st = create (SI.tst si) (SI.ty_st si) in let st = create (SI.tst si) (SI.ty_st si) in
SI.add_simplifier si (simplify st); SI.add_simplifier si (simplify st);
SI.on_preprocess si (preprocess st);
SI.on_preprocess si (cnf st); SI.on_preprocess si (cnf st);
if A.check_congruence_classes then (
Log.debug 5 "(th-bool.add-final-check)";
SI.on_final_check si (check_new_terms st);
);
st st
let theory = let theory =

13
src/th-data/Sidekick_th_data.ml
View file

@ -309,10 +309,10 @@ module Make(A : ARG) : S with module A = A = struct
N_tbl.pop_levels self.to_decide n; N_tbl.pop_levels self.to_decide n;
() ()
let preprocess (self:t) si (acts:SI.preprocess_actions) (t:T.t) : _ option = let preprocess (self:t) si (acts:SI.preprocess_actions) (t:T.t) : unit =
let ty = T.ty t in let ty = T.ty t in
match A.view_as_data t, A.as_datatype ty with match A.view_as_data t, A.as_datatype ty with
| T_cstor _, _ -> None | T_cstor _, _ -> ()
| _, Ty_data {cstors; _} -> | _, Ty_data {cstors; _} ->
begin match Iter.take 2 cstors |> Iter.to_rev_list with begin match Iter.take 2 cstors |> Iter.to_rev_list with
| [cstor] when not (T.Tbl.mem self.single_cstor_preproc_done t) -> | [cstor] when not (T.Tbl.mem self.single_cstor_preproc_done t) ->
@ -338,7 +338,7 @@ module Make(A : ARG) : S with module A = A = struct
let proof = let proof =
let pr_isa = let pr_isa =
A.P.lemma_isa_split t A.P.lemma_isa_split t
(Iter.return @@ Act.mk_lit_nopreproc (A.mk_is_a self.tst cstor t)) (Iter.return @@ Act.mk_lit (A.mk_is_a self.tst cstor t))
self.proof self.proof
and pr_eq_sel = and pr_eq_sel =
A.P.lemma_select_cstor ~cstor_t:u t self.proof A.P.lemma_select_cstor ~cstor_t:u t self.proof
@ -349,12 +349,11 @@ module Make(A : ARG) : S with module A = A = struct
T.Tbl.add self.single_cstor_preproc_done t (); (* avoid loops *) T.Tbl.add self.single_cstor_preproc_done t (); (* avoid loops *)
T.Tbl.add self.case_split_done t (); (* no need to decide *) T.Tbl.add self.case_split_done t (); (* no need to decide *)
Act.add_clause [Act.mk_lit_nopreproc (A.mk_eq self.tst t u)] proof; Act.add_clause [Act.mk_lit (A.mk_eq self.tst t u)] proof;
None
| _ -> None | _ -> ()
end end
| _ -> None | _ -> ()
(* remember terms of a datatype *) (* remember terms of a datatype *)
let on_new_term_look_at_ty (self:t) n (t:T.t) : unit = let on_new_term_look_at_ty (self:t) n (t:T.t) : unit =