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

refactor: eager proofs; stronger preprocessing

Browse source 
proofs are now directly emitted (almost) everywhere, which simplifies
a lot of things. preprocessing is more recursive (a bit too much
really).
This commit is contained in:
Simon Cruanes 2021-08-22 01:13:41 -04:00
parent 0668f28ac7
commit e93e084eac
No known key found for this signature in database
GPG key ID: 4AC01D0849AA62B6
13 changed files with 456 additions and 478 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/base/Proof_stub.ml
View file

@ -8,7 +8,7 @@ type t = unit
type dproof = t -> unit
let create () : t = ()
let enabled _ = false
let with_proof _ _ = ()
let begin_subproof _ = ()
let end_subproof _ = ()
@ -26,5 +26,5 @@ let lemma_isa_split _ _ = ()
let lemma_bool_tauto _ _ = ()
let lemma_bool_c _ _ _ = ()
let lemma_bool_equiv _ _ _ = ()
let lemma_ite_true _ ~a:_ ~ite:_ = ()
let lemma_ite_false _ ~a:_ ~ite:_ = ()
let lemma_ite_true ~a:_ ~ite:_ _ = ()
let lemma_ite_false ~a:_ ~ite:_ _ = ()

18
src/base/Proof_stub.mli
View file

@ -9,14 +9,14 @@ include Sidekick_core.PROOF
val create : unit -> t
val lemma_bool_tauto : t -> Lit.t Iter.t -> unit
val lemma_bool_c : t -> string -> term list -> unit
val lemma_bool_equiv : t -> term -> term -> unit
val lemma_ite_true : t -> a:term -> ite:term -> unit
val lemma_ite_false : t -> a:term -> ite:term -> unit
val lemma_bool_tauto : Lit.t Iter.t -> t -> unit
val lemma_bool_c : string -> term list -> t -> unit
val lemma_bool_equiv : term -> term -> t -> unit
val lemma_ite_true : a:term -> ite:term -> t -> unit
val lemma_ite_false : a:term -> ite:term -> t -> unit
val lemma_lra : t -> Lit.t Iter.t -> unit
val lemma_lra : Lit.t Iter.t -> t -> unit
val lemma_isa_split : t -> Lit.t Iter.t -> unit
val lemma_isa_disj : t -> Lit.t Iter.t -> unit
val lemma_cstor_inj : t -> Lit.t Iter.t -> unit
val lemma_isa_split : Lit.t Iter.t -> t -> unit
val lemma_isa_disj : Lit.t Iter.t -> t -> unit
val lemma_cstor_inj : Lit.t Iter.t -> t -> unit

6
src/cc/Sidekick_cc.ml
View file

@ -660,7 +660,7 @@ module Make (A: CC_ARG)
let lits = explain_equal cc ~th lits b rb in
let emit_proof p =
let p_lits = Iter.of_list lits |> Iter.map Lit.neg in
P.lemma_cc p p_lits in
P.lemma_cc p_lits p in
raise_conflict_ cc ~th:!th acts (List.rev_map Lit.neg lits) emit_proof
);
(* We will merge [r_from] into [r_into].
@ -779,7 +779,7 @@ module Make (A: CC_ARG)
let emit_proof p =
(* make a tautology, not a true guard *)
let p_lits = Iter.cons lit (Iter.of_list lits |> Iter.map Lit.neg) in
P.lemma_cc p p_lits
P.lemma_cc p_lits p
in
lits, emit_proof
) in
@ -850,7 +850,7 @@ module Make (A: CC_ARG)
let lits = List.rev_map Lit.neg lits in
let emit_proof p =
let p_lits = Iter.of_list lits in
P.lemma_cc p p_lits
P.lemma_cc p_lits p
in
raise_conflict_ cc ~th:!th acts lits emit_proof

161
src/core/Sidekick_core.ml
View file

@ -150,7 +150,7 @@ module type CC_PROOF = sig
type t
type lit
val lemma_cc : t -> lit Iter.t -> unit
val lemma_cc : lit Iter.t -> t -> unit
(** [lemma_cc proof lits] asserts that [lits] form a tautology for the theory
of uninterpreted functions. *)
end
@ -169,17 +169,18 @@ module type SAT_PROOF = sig
type dproof = t -> unit
(** A delayed proof, used to produce proofs on demand from theories. *)
val enabled : t -> bool
(** Do we emit proofs at all? *)
val with_proof : t -> (t -> unit) -> unit
(** If proof is enabled, call [f] on it to emit steps.
if proof is disabled, the callback won't even be called. *)
val emit_input_clause : t -> lit Iter.t -> unit
val emit_input_clause : lit Iter.t -> t -> unit
(** Emit an input clause. *)
val emit_redundant_clause : t -> lit Iter.t -> unit
val emit_redundant_clause : lit Iter.t -> t -> unit
(** Emit a clause deduced by the SAT solver, redundant wrt axioms.
The clause must be RUP wrt previous clauses. *)
val del_clause : t -> lit Iter.t -> unit
val del_clause : lit Iter.t -> t -> unit
(** Forget a clause. Only useful for performance considerations. *)
(* TODO: replace with something index-based? *)
end
@ -215,20 +216,17 @@ module type PROOF = sig
(** [end_subproof p] ends the current active subproof, the last result
of which is kept. *)
val define_term : t -> term -> term -> unit
val define_term : term -> term -> t -> unit
(** [define_term p cst u] defines the new constant [cst] as being equal
to [u]. *)
val lemma_true : t -> term -> unit
val lemma_true : term -> t -> unit
(** [lemma_true p (true)] asserts the clause [(true)] *)
val lemma_preprocess : t -> term -> term -> unit
val lemma_preprocess : term -> term -> t -> 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
(** Is proof production enabled? *)
end
(** Literals
@ -662,9 +660,11 @@ module type SOLVER_INTERNAL = sig
val ty_st : t -> ty_store
val stats : t -> Stat.t
val with_proof : t -> (proof -> unit) -> unit
(** {3 Actions for the theories} *)
type actions
type theory_actions
(** Handle that the theories can use to perform actions. *)
type lit = Lit.t
@ -685,7 +685,7 @@ module type SOLVER_INTERNAL = sig
and type proof = proof
and type P.t = proof
and type P.lit = lit
and type Actions.t = actions
and type Actions.t = theory_actions
val cc : t -> CC.t
(** Congruence closure for this solver *)
@ -702,19 +702,21 @@ module type SOLVER_INTERNAL = sig
val clear : t -> unit
(** Reset internal cache, etc. *)
type hook = t -> term -> (term * dproof) option
val with_proof : t -> (proof -> unit) -> unit
type hook = t -> term -> term option
(** 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],
and if [t] is [app "+" (const x) (const y)] where [x] and [y] are number,
returns [Some (const (x+y))], and [None] otherwise. *)
val normalize : t -> term -> (term * dproof) option
val normalize : t -> term -> term option
(** Normalize a term using all the hooks. This performs
a fixpoint, i.e. it only stops when no hook applies anywhere inside
the term. *)
val normalize_t : t -> term -> term * dproof
val normalize_t : t -> term -> term
(** Normalize a term using all the hooks, along with a proof that the
simplification is correct.
returns [t, refl t] if no simplification occurred. *)
@ -727,58 +729,99 @@ module type SOLVER_INTERNAL = sig
val simplifier : t -> Simplify.t
val simplify_t : t -> term -> (term * dproof) option
(** Simplify input term, returns [Some (u, |- t=u)] if some
val simplify_t : t -> term -> term option
(** Simplify input term, returns [Some u] if some
simplification occurred. *)
val simp_t : t -> term -> term * dproof
(** [simp_t si t] returns [u, |- t=u] even if no simplification occurred
val simp_t : t -> term -> term
(** [simp_t si t] returns [u] even if no simplification occurred
(in which case [t == u] syntactically).
It emits [|- t=u].
(see {!simplifier}) *)
(** {3 Preprocessors}
These preprocessors turn mixed, raw literals (possibly simplified) into
literals suitable for reasoning.
Typically some clauses are also added to the solver. *)
module type PREPROCESS_ACTS = sig
val mk_lit : ?sign:bool -> term -> lit
(** creates a new literal for a boolean term. *)
val add_clause : lit list -> dproof -> unit
(** pushes a new clause into the SAT solver. *)
val add_lit : ?default_pol:bool -> lit -> unit
(** Ensure the literal will be decided/handled by the SAT solver. *)
end
type preprocess_actions = (module PREPROCESS_ACTS)
(** Actions available to the preprocessor *)
type preprocess_hook =
t ->
preprocess_actions ->
term -> term option
(** Given a term, try to preprocess it. Return [None] if it didn't change,
or [Some (u)] if [t=u].
Can also add clauses to define new terms.
Preprocessing might transform terms to make them more amenable
to reasoning, e.g. by removing boolean formulas via Tseitin encoding,
adding clauses that encode their meaning in the same move.
@param preprocess_actions actions available during preprocessing.
*)
val on_preprocess : t -> preprocess_hook -> unit
(** 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} *)
val raise_conflict : t -> actions -> lit list -> dproof -> 'a
val raise_conflict : t -> theory_actions -> lit list -> dproof -> 'a
(** Give a conflict clause to the solver *)
val push_decision : t -> actions -> lit -> unit
val push_decision : t -> theory_actions -> lit -> unit
(** Ask the SAT solver to decide the given literal in an extension of the
current trail. This is useful for theory combination.
If the SAT solver backtracks, this (potential) decision is removed
and forgotten. *)
val propagate: t -> actions -> lit -> reason:(unit -> lit list * dproof) -> unit
val propagate: t -> theory_actions -> lit -> reason:(unit -> lit list * dproof) -> unit
(** Propagate a boolean using a unit clause.
[expl => lit] must be a theory lemma, that is, a T-tautology *)
val propagate_l: t -> actions -> lit -> lit list -> dproof -> unit
val propagate_l: t -> theory_actions -> lit -> lit list -> dproof -> unit
(** Propagate a boolean using a unit clause.
[expl => lit] must be a theory lemma, that is, a T-tautology *)
val add_clause_temp : t -> actions -> lit list -> dproof -> unit
val add_clause_temp : t -> theory_actions -> lit list -> dproof -> unit
(** Add local clause to the SAT solver. This clause will be
removed when the solver backtracks. *)
val add_clause_permanent : t -> actions -> lit list -> dproof -> unit
val add_clause_permanent : t -> theory_actions -> lit list -> dproof -> unit
(** Add toplevel clause to the SAT solver. This clause will
not be backtracked. *)
val mk_lit : t -> actions -> ?sign:bool -> term -> lit
val mk_lit : t -> theory_actions -> ?sign:bool -> term -> lit
(** Create a literal. This automatically preprocesses the term. *)
val preprocess_term :
t -> add_clause:(Lit.t list -> dproof -> unit) -> term -> term * dproof
(** Preprocess a term. *)
val preprocess_term : t -> preprocess_actions -> term -> term
(** Preprocess a term. The preprocessing proof is automatically emitted. *)
val add_lit : t -> actions -> 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
a boolean value *)
a boolean value.
@param default_pol default polarity for the corresponding atom *)
val add_lit_t : t -> actions -> ?sign:bool -> term -> unit
val add_lit_t : t -> theory_actions -> ?sign:bool -> term -> unit
(** Add the given (signed) bool term to the SAT solver, so it gets assigned
a boolean value *)
val cc_raise_conflict_expl : t -> actions -> CC.Expl.t -> 'a
val cc_raise_conflict_expl : t -> theory_actions -> CC.Expl.t -> 'a
(** Raise a conflict with the given congruence closure explanation.
it must be a theory tautology that [expl ==> absurd].
To be used in theories. *)
@ -789,12 +832,12 @@ module type SOLVER_INTERNAL = sig
val cc_are_equal : t -> term -> term -> bool
(** Are these two terms equal in the congruence closure? *)
val cc_merge : t -> actions -> CC.N.t -> CC.N.t -> CC.Expl.t -> unit
val cc_merge : t -> theory_actions -> CC.N.t -> CC.N.t -> CC.Expl.t -> unit
(** Merge these two nodes in the congruence closure, given this explanation.
It must be a theory tautology that [expl ==> n1 = n2].
To be used in theories. *)
val cc_merge_t : t -> actions -> term -> term -> CC.Expl.t -> unit
val cc_merge_t : t -> theory_actions -> term -> term -> CC.Expl.t -> unit
(** Merge these two terms in the congruence closure, given this explanation.
See {!cc_merge} *)
@ -806,10 +849,10 @@ module type SOLVER_INTERNAL = sig
(** Return [true] if the term is explicitly in the congruence closure.
To be used in theories *)
val on_cc_pre_merge : t -> (CC.t -> actions -> CC.N.t -> CC.N.t -> CC.Expl.t -> unit) -> unit
val on_cc_pre_merge : t -> (CC.t -> theory_actions -> CC.N.t -> CC.N.t -> CC.Expl.t -> unit) -> unit
(** Callback for when two classes containing data for this key are merged (called before) *)
val on_cc_post_merge : t -> (CC.t -> actions -> CC.N.t -> CC.N.t -> unit) -> unit
val on_cc_post_merge : t -> (CC.t -> theory_actions -> CC.N.t -> CC.N.t -> unit) -> unit
(** Callback for when two classes containing data for this key are merged (called after)*)
val on_cc_new_term : t -> (CC.t -> CC.N.t -> term -> unit) -> unit
@ -826,7 +869,7 @@ module type SOLVER_INTERNAL = sig
val on_cc_propagate : t -> (CC.t -> lit -> (unit -> lit list * dproof) -> unit) -> unit
(** Callback called on every CC propagation *)
val on_partial_check : t -> (t -> actions -> lit Iter.t -> unit) -> unit
val on_partial_check : t -> (t -> theory_actions -> lit Iter.t -> unit) -> unit
(** Register callbacked to be called with the slice of literals
newly added on the trail.
@ -834,7 +877,7 @@ module type SOLVER_INTERNAL = sig
to be complete, only correct. It's given only the slice of
the trail consisting in new literals. *)
val on_final_check: t -> (t -> actions -> lit Iter.t -> unit) -> unit
val on_final_check: t -> (t -> theory_actions -> lit Iter.t -> unit) -> unit
(** Register callback to be called during the final check.
Must be complete (i.e. must raise a conflict if the set of literals is
@ -842,31 +885,6 @@ module type SOLVER_INTERNAL = sig
is given the whole trail.
*)
(** {3 Preprocessors}
These preprocessors turn mixed, raw literals (possibly simplified) into
literals suitable for reasoning.
Typically some clauses are also added to the solver. *)
type preprocess_hook =
t ->
mk_lit:(term -> lit) ->
add_clause:(lit list -> dproof -> unit) ->
term -> (term * dproof) option
(** 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].
Can also add clauses to define new terms.
Preprocessing might transform terms to make them more amenable
to reasoning, e.g. by removing boolean formulas via Tseitin encoding,
adding clauses that encode their meaning in the same move.
@param mk_lit creates a new literal for a boolean term.
@param add_clause pushes a new clause into the SAT solver.
*)
val on_preprocess : t -> preprocess_hook -> unit
(** Add a hook that will be called when terms are preprocessed *)
(** {3 Model production} *)
type model_hook =
@ -1041,13 +1059,12 @@ module type SOLVER = sig
val add_theory_l : t -> theory list -> unit
val mk_lit_t : t -> ?sign:bool -> term -> lit * dproof
(** [mk_lit_t _ ~sign t] returns [lit, pr]
where [lit] is a internal representation of [± t],
and [pr] is a proof of [|- lit = (± t)] *)
val mk_lit_t : t -> ?sign:bool -> term -> lit
(** [mk_lit_t _ ~sign t] returns [lit'],
where [lit'] is [preprocess(lit)] and [lit] is
an internal representation of [± t].
val mk_lit_t' : t -> ?sign:bool -> term -> lit
(** Like {!mk_lit_t} but skips the proof *)
The proof of [|- lit = lit'] is directly added to the solver's proof. *)
val add_clause : t -> lit IArray.t -> dproof -> unit
(** [add_clause solver cs] adds a boolean clause to the solver.

87
src/lra/sidekick_arith_lra.ml
View file

@ -60,7 +60,7 @@ module type ARG = sig
val has_ty_real : term -> bool
(** Does this term have the type [Real] *)
val lemma_lra : S.proof -> S.Lit.t Iter.t -> unit
val lemma_lra : S.Lit.t Iter.t -> S.proof -> unit
module Gensym : sig
type t
@ -233,29 +233,18 @@ module Make(A : ARG) : S with module A = A = struct
);
proxy
let add_clause_lra_ ~add_clause lits =
let emit_proof p =
A.lemma_lra p (Iter.of_list lits)
in
add_clause lits emit_proof
let add_clause_lra_ (module PA:SI.PREPROCESS_ACTS) lits =
let pr = A.lemma_lra (Iter.of_list lits) in
PA.add_clause lits pr
(* preprocess linear expressions away *)
let preproc_lra (self:state) si ~mk_lit ~add_clause
(t:T.t) : (T.t * _) option =
Log.debugf 50 (fun k->k "lra.preprocess %a" T.pp t);
let preproc_lra (self:state) si (module PA:SI.PREPROCESS_ACTS)
(t:T.t) : T.t option =
Log.debugf 50 (fun k->k "(@[lra.preprocess@ %a@])" T.pp t);
let tst = SI.tst si in
let sub_proofs_ = ref [] in
(* preprocess subterm *)
let preproc_t t =
let u, p_t_eq_u = SI.preprocess_term ~add_clause si t in
if t != u then (
(* add [|- t=u] to hyps *)
sub_proofs_ := (t,u,p_t_eq_u) :: !sub_proofs_;
);
u
in
let preproc_t t = SI.preprocess_term si (module PA) t in
(* tell the CC this term exists *)
let declare_term_to_cc t =
@ -274,12 +263,12 @@ module Make(A : ARG) : S with module A = A = struct
T.Tbl.add self.encoded_eqs t ();
(* encode [t <=> (u1 /\ u2)] *)
let lit_t = mk_lit t in
let lit_u1 = mk_lit u1 in
let lit_u2 = mk_lit u2 in
add_clause_lra_ ~add_clause [SI.Lit.neg lit_t; lit_u1];
add_clause_lra_ ~add_clause [SI.Lit.neg lit_t; lit_u2];
add_clause_lra_ ~add_clause
let lit_t = PA.mk_lit t in
let lit_u1 = PA.mk_lit u1 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_u2];
add_clause_lra_ (module PA)
[SI.Lit.neg lit_u1; SI.Lit.neg lit_u2; lit_t];
);
None
@ -309,14 +298,14 @@ module Make(A : ARG) : S with module A = A = struct
let new_t = A.mk_lra tst (LRA_simplex_pred (proxy, op, le_const)) in
begin
let lit = mk_lit new_t in
let lit = PA.mk_lit new_t in
let constr = SimpSolver.Constraint.mk proxy op le_const in
SimpSolver.declare_bound self.simplex constr (Tag.Lit lit);
end;
Log.debugf 10 (fun k->k "lra.preprocess:@ %a@ :into %a" T.pp t T.pp new_t);
(* FIXME: by def proxy + LRA *)
Some (new_t, (fun _ -> ()))
(* FIXME: emit proof: by def proxy + LRA *)
Some new_t
| Some (coeff, v), pred ->
(* [c . v <= const] becomes a direct simplex constraint [v <= const/c] *)
@ -335,15 +324,14 @@ module Make(A : ARG) : S with module A = A = struct
let new_t = A.mk_lra tst (LRA_simplex_pred (v, op, q)) in
begin
let lit = mk_lit new_t in
let lit = PA.mk_lit new_t in
let constr = SimpSolver.Constraint.mk v op q in
SimpSolver.declare_bound self.simplex constr (Tag.Lit lit);
end;
Log.debugf 10 (fun k->k "lra.preprocess@ :%a@ :into %a" T.pp t T.pp new_t);
(* FIXME: preprocess proof *)
let emit_proof _ = () in
Some (new_t, emit_proof)
Some new_t
end
| LRA_op _ | LRA_mult _ ->
@ -357,9 +345,7 @@ module Make(A : ARG) : S with module A = A = struct
declare_term_to_cc proxy;
(* FIXME: proof by def of proxy *)
let emit_proof _ = () in
Some (proxy, emit_proof)
Some proxy
) else (
(* a bit more complicated: we cannot just define [proxy := le_comb]
because of the coefficient.
@ -382,29 +368,30 @@ module Make(A : ARG) : S with module A = A = struct
declare_term_to_cc proxy;
declare_term_to_cc proxy2;
add_clause [
mk_lit (A.mk_lra tst (LRA_simplex_pred (proxy2, Leq, A.Q.neg le_const)))
PA.add_clause [
PA.mk_lit (A.mk_lra tst (LRA_simplex_pred (proxy2, Leq, A.Q.neg le_const)))
] (fun _ -> ()); (* TODO: by-def proxy2 + LRA *)
add_clause [
mk_lit (A.mk_lra tst (LRA_simplex_pred (proxy2, Geq, A.Q.neg le_const)))
PA.add_clause [
PA.mk_lit (A.mk_lra tst (LRA_simplex_pred (proxy2, Geq, A.Q.neg le_const)))
] (fun _ -> ()); (* TODO: by-def proxy2 + LRA *)
(* FIXME: actual proof *)
let emit_proof _ = () in
Some (proxy, emit_proof)
Some proxy
)
| LRA_other t when A.has_ty_real t -> None
| LRA_const _ | LRA_simplex_pred _ | LRA_simplex_var _ | LRA_other _ -> None
| LRA_const _ | LRA_simplex_pred _ | LRA_simplex_var _ | LRA_other _ ->
Log.debug 0 "LRA NONE";
None
let simplify (self:state) (_recurse:_) (t:T.t) : (T.t * SI.dproof) option =
let simplify (self:state) (_recurse:_) (t:T.t) : T.t option =
match A.view_as_lra t with
| LRA_op _ | LRA_mult _ ->
let le = as_linexp_id t in
if LE.is_const le then (
let c = LE.const le in
(* FIXME: proof *)
Some (A.mk_lra self.tst (LRA_const c), (fun _ -> ()))
Some (A.mk_lra self.tst (LRA_const c))
) else None
| LRA_pred (pred, l1, l2) ->
let le = LE.(as_linexp_id l1 - as_linexp_id l2) in
@ -419,7 +406,7 @@ module Make(A : ARG) : S with module A = A = struct
| Neq -> A.Q.(c <> zero)
in
(* FIXME: proof *)
Some (A.mk_bool self.tst is_true, (fun _ -> ()))
Some (A.mk_bool self.tst is_true)
) else None
| _ -> None
@ -433,8 +420,8 @@ module Make(A : ARG) : S with module A = A = struct
|> CCList.flat_map (Tag.to_lits si)
|> List.rev_map SI.Lit.neg
in
let emit_proof p = A.lemma_lra p (Iter.of_list confl) in
SI.raise_conflict si acts confl emit_proof
let pr = A.lemma_lra (Iter.of_list confl) in
SI.raise_conflict si acts confl pr
let on_propagate_ si acts lit ~reason =
match lit with
@ -443,10 +430,8 @@ module Make(A : ARG) : S with module A = A = struct
SI.propagate si acts lit
~reason:(fun() ->
let lits = CCList.flat_map (Tag.to_lits si) reason in
let emit_proof p =
A.lemma_lra p Iter.(cons lit (of_list lits))
in
CCList.flat_map (Tag.to_lits si) reason, emit_proof)
let pr = A.lemma_lra Iter.(cons lit (of_list lits)) in
CCList.flat_map (Tag.to_lits si) reason, pr)
| _ -> ()
let check_simplex_ self si acts : SimpSolver.Subst.t =
@ -594,7 +579,7 @@ module Make(A : ARG) : S with module A = A = struct
);
()
let final_check_ (self:state) si (acts:SI.actions) (_trail:_ Iter.t) : unit =
let final_check_ (self:state) si (acts:SI.theory_actions) (_trail:_ Iter.t) : unit =
Log.debug 5 "(th-lra.final-check)";
Profile.with_ "lra.final-check" @@ fun () ->

12
src/main/pure_sat_solver.ml
View file

@ -38,26 +38,26 @@ end = struct
}
type dproof = t -> unit
let[@inline] enabled = function
| Dummy -> false
| Inner _ -> true
let[@inline] with_proof pr f = match pr with
| Dummy -> ()
| Inner _ -> f pr
let emit_lits_ buf lits =
lits (fun i -> bpf buf "%d " i)
let emit_input_clause self lits =
let emit_input_clause lits self =
match self with
| Dummy -> ()
| Inner {buf} ->
bpf buf "i "; emit_lits_ buf lits; bpf buf "0\n"
let emit_redundant_clause self lits =
let emit_redundant_clause lits self =
match self with
| Dummy -> ()
| Inner {buf} ->
bpf buf "r "; emit_lits_ buf lits; bpf buf "0\n"
let del_clause self lits =
let del_clause lits self =
match self with
| Dummy -> ()
| Inner {buf} ->

32
src/sat/Solver.ml
View file

@ -1402,7 +1402,7 @@ module Make(Plugin : PLUGIN)
let atoms = List.rev_map (make_atom_ self) l in
let removable = not keep in
let c = Clause.make_l self.store ~removable atoms in
if Proof.enabled self.proof then dp self.proof;
Proof.with_proof self.proof dp;
Log.debugf 5 (fun k->k "(@[sat.th.add-clause@ %a@])" (Clause.debug self.store) c);
Vec.push self.clauses_to_add c
@ -1415,11 +1415,11 @@ module Make(Plugin : PLUGIN)
self.next_decisions <- a :: self.next_decisions
)
let acts_raise self (l:lit list) (pr:dproof) : 'a =
let acts_raise self (l:lit list) (dp:dproof) : 'a =
let atoms = List.rev_map (make_atom_ self) l in
(* conflicts can be removed *)
let c = Clause.make_l self.store ~removable:true atoms in
if Proof.enabled self.proof then pr self.proof;
Proof.with_proof self.proof dp;
Log.debugf 5 (fun k->k "(@[@{<yellow>sat.th.raise-conflict@}@ %a@])"
(Clause.debug self.store) c);
raise_notrace (Th_conflict c)
@ -1444,7 +1444,7 @@ module Make(Plugin : PLUGIN)
let l = List.rev_map (fun f -> Atom.neg @@ make_atom_ self f) lits in
check_consequence_lits_false_ self l;
let c = Clause.make_l store ~removable:true (p :: l) in
if Proof.enabled self.proof then dp self.proof;
Proof.with_proof self.proof dp;
raise_notrace (Th_conflict c)
) else (
insert_var_order self (Atom.var p);
@ -1458,7 +1458,7 @@ module Make(Plugin : PLUGIN)
(otherwise the propagated lit would have been backtracked and
discarded already.) *)
check_consequence_lits_false_ self l;
if Proof.enabled self.proof then dp self.proof;
Proof.with_proof self.proof dp;
Clause.make_l store ~removable:true (p :: l)
) in
let level = decision_level self in
@ -1481,7 +1481,7 @@ module Make(Plugin : PLUGIN)
let a = make_atom_ self f in
eval_atom_ self a
let[@inline] acts_mk_lit self ?default_pol f : unit =
let[@inline] acts_add_lit self ?default_pol f : unit =
ignore (make_atom_ ?default_pol self f : atom)
let[@inline] current_slice st : _ Solver_intf.acts =
@ -1491,7 +1491,7 @@ module Make(Plugin : PLUGIN)
type nonrec lit = lit
let iter_assumptions=acts_iter st ~full:false st.th_head
let eval_lit= acts_eval_lit st
let mk_lit=acts_mk_lit st
let add_lit=acts_add_lit st
let add_clause = acts_add_clause st
let propagate = acts_propagate st
let raise_conflict c pr=acts_raise st c pr
@ -1507,7 +1507,7 @@ module Make(Plugin : PLUGIN)
type nonrec lit = lit
let iter_assumptions=acts_iter st ~full:true st.th_head
let eval_lit= acts_eval_lit st
let mk_lit=acts_mk_lit st
let add_lit=acts_add_lit st
let add_clause = acts_add_clause st
let propagate = acts_propagate st
let raise_conflict c pr=acts_raise st c pr
@ -1830,9 +1830,8 @@ module Make(Plugin : PLUGIN)
(fun l ->
let atoms = Util.array_of_list_map (make_atom_ self) l in
let c = Clause.make_a self.store ~removable:false atoms in
if Proof.enabled self.proof then (
Proof.emit_input_clause self.proof (Iter.of_list l)
);
Proof.with_proof self.proof
(Proof.emit_input_clause (Iter.of_list l));
Log.debugf 10 (fun k -> k "(@[sat.assume-clause@ @[<hov 2>%a@]@])"
(Clause.debug self.store) c);
Vec.push self.clauses_to_add c)
@ -1843,6 +1842,7 @@ module Make(Plugin : PLUGIN)
let[@inline] proof st = st.proof
let[@inline] add_lit self ?default_pol lit =
Log.debugf 0 (fun k->k"add lit %a" Lit.pp lit); (* XXX *)
ignore (make_atom_ self lit ?default_pol : atom)
let[@inline] set_default_pol (self:t) (lit:lit) (pol:bool) : unit =
let a = make_atom_ self lit ~default_pol:pol in
@ -1906,7 +1906,7 @@ module Make(Plugin : PLUGIN)
let add_clause_atoms_ self (c:atom array) dp : unit =
try
let c = Clause.make_a self.store ~removable:false c in
if Proof.enabled self.proof then dp self.proof;
Proof.with_proof self.proof dp;
add_clause_ self c
with
| E_unsat (US_false c) ->
@ -1921,12 +1921,12 @@ module Make(Plugin : PLUGIN)
add_clause_atoms_ self c dp
let add_input_clause self (c:lit list) =
let emit_proof p = Proof.emit_input_clause p (Iter.of_list c) in
add_clause self c emit_proof
let dp = Proof.emit_input_clause (Iter.of_list c) in
add_clause self c dp
let add_input_clause_a self c =
let emit_proof p = Proof.emit_input_clause p (Iter.of_array c) in
add_clause_a self c emit_proof
let dp = Proof.emit_input_clause (Iter.of_array c) in
add_clause_a self c dp
let solve ?(assumptions=[]) (self:t) : res =
cancel_until self 0;

4
src/sat/Solver_intf.ml
View file

@ -93,8 +93,8 @@ module type ACTS = sig
val eval_lit: lit -> lbool
(** Obtain current value of the given literal *)
val mk_lit: ?default_pol:bool -> lit -> unit
(** Map the given lit to a literal, which will be decided by the
val add_lit: ?default_pol:bool -> lit -> unit
(** Map the given lit to an internal atom, which will be decided by the
SAT solver. *)
val add_clause: ?keep:bool -> lit list -> dproof -> unit

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

@ -103,27 +103,28 @@ module Make(A : ARG)
next: th_states;
} -> th_states
type actions = sat_acts
type theory_actions = sat_acts
module Simplify = struct
type t = {
tst: term_store;
ty_st: ty_store;
proof: proof;
mutable hooks: hook list;
cache: Term.t Term.Tbl.t;
}
and hook = t -> term -> (term * dproof) option
and hook = t -> term -> term option
let create tst ty_st ~proof : t =
{tst; ty_st; proof; hooks=[]; cache=Term.Tbl.create 32;}
let create tst ty_st : t =
{tst; ty_st; hooks=[]; cache=Term.Tbl.create 32;}
let[@inline] tst self = self.tst
let[@inline] ty_st self = self.ty_st
let[@inline] with_proof self f = P.with_proof self.proof f
let add_hook self f = self.hooks <- f :: self.hooks
let clear self = Term.Tbl.clear self.cache
let normalize (self:t) (t:Term.t) : (Term.t * dproof) option =
let sub_proofs_: dproof list ref = ref [] in
let normalize (self:t) (t:Term.t) : Term.t option =
(* compute and cache normal form of [t] *)
let rec aux t : Term.t =
match Term.Tbl.find self.cache t with
@ -140,33 +141,31 @@ module Make(A : ARG)
| h :: hooks_tl ->
match h self t with
| None -> aux_rec t hooks_tl
| Some (u, _) when Term.equal t u -> aux_rec t hooks_tl
| Some (u, pr_t_u) ->
sub_proofs_ := pr_t_u :: !sub_proofs_;
aux u
| Some u when Term.equal t u -> aux_rec t hooks_tl
| Some u -> aux u (* fixpoint *)
in
let u = aux t in
if Term.equal t u then None
else (
(* proof: [sub_proofs |- t=u] by CC + subproof *)
let emit_proof p =
if not (T.Term.equal t u) then (
P.begin_subproof p;
List.iter (fun dp -> dp p) !sub_proofs_;
P.lemma_preprocess p t u;
P.end_subproof p;
)
in
Some (u, emit_proof)
P.with_proof self.proof (P.lemma_preprocess t u);
Some u
)
let normalize_t self t =
match normalize self t with
| Some (u,pr) -> u, pr
| None -> t, (fun _ -> ())
| Some u -> u
| None -> t
end
type simplify_hook = Simplify.hook
module type PREPROCESS_ACTS = sig
val mk_lit : ?sign:bool -> term -> lit
val add_clause : lit list -> dproof -> unit
val add_lit : ?default_pol:bool -> lit -> unit
end
type preprocess_actions = (module PREPROCESS_ACTS)
type t = {
tst: Term.store; (** state for managing terms *)
ty_st: Ty.store;
@ -181,19 +180,18 @@ module Make(A : ARG)
simp: Simplify.t;
mutable preprocess: preprocess_hook list;
mutable mk_model: model_hook list;
preprocess_cache: (Term.t * dproof list) Term.Tbl.t;
preprocess_cache: Term.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 -> actions -> lit Iter.t -> unit) list;
mutable on_final_check: (t -> actions -> lit Iter.t -> unit) list;
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;
}
and preprocess_hook =
t ->
mk_lit:(term -> lit) ->
add_clause:(lit list -> dproof -> unit) ->
term -> (term * dproof) option
preprocess_actions ->
term -> term option
and model_hook =
recurse:(t -> CC.N.t -> term) ->
@ -208,6 +206,7 @@ module Make(A : ARG)
let[@inline] cc (t:t) = Lazy.force t.cc
let[@inline] tst t = t.tst
let[@inline] ty_st t = t.ty_st
let[@inline] with_proof self f = Proof.with_proof self.proof f
let stats t = t.stat
let define_const (self:t) ~const ~rhs : unit =
@ -215,24 +214,24 @@ module Make(A : ARG)
let simplifier self = self.simp
let simplify_t self (t:Term.t) : _ option = Simplify.normalize self.simp t
let simp_t self (t:Term.t) : Term.t * dproof = Simplify.normalize_t self.simp t
let simp_t self (t:Term.t) : Term.t = Simplify.normalize_t self.simp t
let add_simplifier (self:t) f : unit = Simplify.add_hook self.simp f
let on_preprocess self f = self.preprocess <- f :: self.preprocess
let on_model_gen self f = self.mk_model <- f :: self.mk_model
let push_decision (_self:t) (acts:actions) (lit:lit) : unit =
let push_decision (_self:t) (acts:theory_actions) (lit:lit) : unit =
let (module A) = acts in
let sign = Lit.sign lit in
A.add_decision_lit (Lit.abs lit) sign
let[@inline] raise_conflict self (acts:actions) c proof : 'a =
let[@inline] raise_conflict self (acts:theory_actions) c proof : 'a =
let (module A) = acts in
Stat.incr self.count_conflict;
A.raise_conflict c proof
let[@inline] propagate self (acts:actions) p ~reason : unit =
let[@inline] propagate self (acts:theory_actions) p ~reason : unit =
let (module A) = acts in
Stat.incr self.count_propagate;
A.propagate p (Sidekick_sat.Consequence reason)
@ -240,139 +239,176 @@ module Make(A : ARG)
let[@inline] propagate_l self acts p cs proof : unit =
propagate self acts p ~reason:(fun()->cs,proof)
let add_sat_clause_ self (acts:actions) ~keep lits (proof:dproof) : unit =
let add_sat_clause_ self (acts:theory_actions) ~keep lits (proof:dproof) : unit =
let (module A) = acts in
Stat.incr self.count_axiom;
A.add_clause ~keep lits proof
let preprocess_term_ (self:t) ~add_clause (t:term) : term * dproof =
let mk_lit t = Lit.atom self.tst t in (* no further simplification *)
let add_sat_lit self ?default_pol (acts:theory_actions) (lit:Lit.t) : unit =
let (module A) = acts in
A.add_lit ?default_pol lit
(* actual preprocessing logic, acting on terms.
this calls all the preprocessing hooks on subterms, ensuring
a fixpoint. *)
let preprocess_term_ (self:t) (module A:PREPROCESS_ACTS) (t:term) : term =
let mk_lit_nopreproc t = Lit.atom self.tst t in (* no further simplification *)
(* compute and cache normal form [u] of [t].
Also cache a list of proofs [ps] such
that [ps |- t=u] by CC. *)
let rec aux t : term * dproof list =
match Term.Tbl.find self.preprocess_cache t with
| u, ps ->
u, ps
| exception Not_found ->
let sub_p: _ list ref = ref [] in
Also cache a list of proofs [ps] such that [ps |- t=u] by CC.
It is important that we cache the proofs here, because
next time we preprocess [t], we will have to re-emit the same
proofs, even though we will not do any actual preprocessing work.
*)
let rec aux t : term =
match Term.Tbl.find self.preprocess_cache t with
| u -> u
| exception Not_found ->
(* try rewrite at root *)
let t1 = aux_rec ~sub_p t self.preprocess in
let t1 = aux_rec t self.preprocess in
(* map subterms *)
let t2 =
Term.map_shallow self.tst
(fun t_sub ->
let u_sub, ps_t = aux t_sub in
if not (Term.equal t_sub u_sub) then (
sub_p := List.rev_append ps_t !sub_p;
);
u_sub)
t1
in
let t2 = Term.map_shallow self.tst aux t1 in
let u =
if not (Term.equal t t2) then (
(* fixpoint *)
let v, ps_t2_v = aux t2 in
if not (Term.equal t2 v) then (
sub_p := List.rev_append ps_t2_v !sub_p
);
v
aux t2 (* fixpoint *)
) else (
t2
)
in
(* signal boolean subterms, so as to decide them
in the SAT solver *)
if Ty.is_bool (Term.ty u) then (
Log.debugf 5
(fun k->k "(@[solver.map-bool-subterm-to-lit@ :subterm %a@])" Term.pp u);
(* make a literal (already preprocessed) *)
let lit = mk_lit_nopreproc u in
(* ensure that SAT solver has a boolean atom for [u] *)
A.add_lit lit;
(* also map [sub] to this atom in the congruence closure, for propagation *)
let cc = cc self in
CC.set_as_lit cc (CC.add_term cc u) lit;
);
if t != u then (
Log.debugf 5
(fun k->k "(@[smt-solver.preprocess.term@ :from %a@ :to %a@])"
Term.pp t Term.pp u);
);
Term.Tbl.add self.preprocess_cache t (u,!sub_p);
u, !sub_p
Term.Tbl.add self.preprocess_cache t u;
u
(* try each function in [hooks] successively *)
and aux_rec ~sub_p t hooks : term =
and aux_rec t hooks : term =
match hooks with
| [] -> t
| h :: hooks_tl ->
match h self ~mk_lit ~add_clause t with
| None -> aux_rec ~sub_p t hooks_tl
| Some (u, ps_t_u) ->
sub_p := ps_t_u :: !sub_p;
let v, ps_u_v = aux u in
if t != v then (
sub_p := List.rev_append ps_u_v !sub_p;
);
v
match h self (module A) t with
| None -> aux_rec t hooks_tl
| Some u -> aux u
in
let t1, p_t_t1 = simp_t self t in
P.begin_subproof self.proof;
let u, ps_t1_u = aux t1 in
(* simplify the term *)
let t1 = simp_t self t in
let emit_proof_t_eq_u =
if t != u then (
let hyps =
if t == t1 then ps_t1_u
else p_t_t1 :: ps_t1_u in
let emit_proof p =
P.begin_subproof p;
List.iter (fun dp -> dp p) hyps;
P.lemma_preprocess p t u;
P.end_subproof p;
in
emit_proof
) else (fun _->())
in
u, emit_proof_t_eq_u
(* return preprocessed lit + proof they are equal *)
let preprocess_lit_ (self:t) ~add_clause (lit:lit) : lit * dproof =
let t, p = Lit.term lit |> preprocess_term_ self ~add_clause in
let lit' = Lit.atom self.tst ~sign:(Lit.sign lit) t in
if not (Lit.equal lit lit') then (
Log.debugf 10
(fun k->k "(@[smt-solver.preprocess.lit@ :lit %a@ :into %a@])"
Lit.pp lit Lit.pp lit');
(* preprocess *)
let u = aux t1 in
(* emit [|- t=u] *)
if not (Term.equal t u) then (
P.with_proof self.proof (P.lemma_preprocess t u);
);
lit', p
P.end_subproof self.proof;
u
(* return preprocessed lit + proof they are equal *)
let preprocess_lit_ (self:t) (module A0:PREPROCESS_ACTS) (lit:lit) : lit =
(* create literal and preprocess it with [pacts], which uses [A0]
for the base operations, and preprocesses new literals and clauses
recursively. *)
let rec mk_lit ?sign t =
Log.debug 0 "A.MK_LIT";
let u = preprocess_term_ self (Lazy.force pacts) t in
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);
);
Lit.atom self.tst ?sign u
and preprocess_lit (lit:lit) : lit =
let t = Lit.term lit in
let sign = Lit.sign lit in
mk_lit ~sign t
(* wrap [A0] so that all operations go throught preprocessing *)
and pacts = lazy (
(module struct
let add_lit ?default_pol lit =
let lit = preprocess_lit lit in
A0.add_lit lit
let add_clause c pr =
Stat.incr self.count_preprocess_clause;
let c = CCList.map preprocess_lit c in
A0.add_clause c pr
let mk_lit = mk_lit
end : PREPROCESS_ACTS)
) in
preprocess_lit lit
(* add a clause using [acts] *)
let add_clause_ self acts lits (proof:dproof) : unit =
Stat.incr self.count_preprocess_clause;
add_sat_clause_ self acts ~keep:true lits proof
(* FIXME: should we store the proof somewhere? *)
let mk_lit self acts ?sign t : Lit.t =
let add_clause = add_clause_ self acts in
let lit, _p =
preprocess_lit_ self ~add_clause @@ Lit.atom self.tst ?sign t
in
lit
let[@inline] preprocess_term self ~add_clause (t:term) : term * dproof =
preprocess_term_ self ~add_clause t
let[@inline] add_clause_temp self acts lits (proof:dproof) : unit =
add_sat_clause_ self acts ~keep:false lits proof
let[@inline] add_clause_permanent self acts lits (proof:dproof) : unit =
add_sat_clause_ self acts ~keep:true lits proof
let[@inline] add_lit _self (acts:actions) lit : unit =
let[@inline] add_lit _self (acts:theory_actions) ?default_pol lit : unit =
let (module A) = acts in
A.mk_lit lit
A.add_lit ?default_pol lit
let preprocess_acts_of_acts (self:t) (acts:theory_actions) : preprocess_actions =
(module struct
let mk_lit ?sign t = Lit.atom self.tst ?sign t
let add_clause = add_clause_ self acts
let add_lit = add_lit self acts
end)
let preprocess_clause_ (self:t) (acts:theory_actions) (c:lit list) : lit list =
let pacts = preprocess_acts_of_acts self acts in
let c = CCList.map (preprocess_lit_ self pacts) c in
c
(* make literal and preprocess it *)
let[@inline] mk_plit (self:t) (pacts:preprocess_actions) ?sign (t:term) : lit =
let lit = Lit.atom self.tst ?sign t in
preprocess_lit_ self pacts lit
let[@inline] preprocess_term self (pacts:preprocess_actions) (t:term) : term =
preprocess_term_ self pacts t
let[@inline] add_clause_temp self acts c (proof:dproof) : unit =
let c = preprocess_clause_ self acts c in
add_sat_clause_ self acts ~keep:false c proof
let[@inline] add_clause_permanent self acts c (proof:dproof) : unit =
let c = preprocess_clause_ self acts c 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 lit = mk_lit self acts ?sign t in
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
@ -420,7 +456,7 @@ module Make(A : ARG)
exception E_loop_exit
(* handle a literal assumed by the SAT solver *)
let assert_lits_ ~final (self:t) (acts:actions) (lits:Lit.t Iter.t) : unit =
let assert_lits_ ~final (self:t) (acts:theory_actions) (lits:Lit.t Iter.t) : unit =
Log.debugf 2
(fun k->k "(@[<hv1>@{<green>smt-solver.assume_lits@}%s[lvl=%d]@ %a@])"
(if final then "[final]" else "") self.level (Util.pp_iter ~sep:"; " Lit.pp) lits);
@ -448,7 +484,7 @@ module Make(A : ARG)
);
()
let[@inline] iter_atoms_ (acts:actions) : _ Iter.t =
let[@inline] iter_atoms_ (acts:theory_actions) : _ Iter.t =
fun f ->
let (module A) = acts in
A.iter_assumptions f
@ -481,7 +517,7 @@ module Make(A : ARG)
proof;
th_states=Ths_nil;
stat;
simp=Simplify.create tst ty_st;
simp=Simplify.create tst ty_st ~proof;
on_progress=(fun () -> ());
preprocess=[];
mk_model=[];
@ -507,6 +543,7 @@ module Make(A : ARG)
si: Solver_internal.t;
solver: Sat_solver.t;
stat: Stat.t;
proof: P.t;
count_clause: int Stat.counter;
count_solve: int Stat.counter;
(* config: Config.t *)
@ -554,7 +591,7 @@ module Make(A : ARG)
Log.debug 5 "smt-solver.create";
let si = Solver_internal.create ~stat ~proof tst ty_st () in
let self = {
si;
si; proof;
solver=Sat_solver.create ~proof ?size si;
stat;
count_clause=Stat.mk_int stat "solver.add-clause";
@ -567,7 +604,7 @@ module Make(A : ARG)
let t_true = Term.bool tst true in
Sat_solver.add_clause self.solver
[Lit.atom tst t_true]
(fun p -> P.lemma_true p t_true)
(P.lemma_true t_true)
end;
self
@ -577,65 +614,25 @@ module Make(A : ARG)
let[@inline] tst self = Solver_internal.tst self.si
let[@inline] ty_st self = Solver_internal.ty_st self.si
(* map boolean subterms to literals *)
let add_bool_subterms_ (self:t) (t:Term.t) : unit =
Term.iter_dag t
|> Iter.filter (fun t -> Ty.is_bool @@ Term.ty t)
|> Iter.filter
(fun t -> match A.cc_view t with
| Sidekick_core.CC_view.Not _ -> false (* will process the subterm just later *)
| _ -> true)
|> Iter.filter (fun t -> A.is_valid_literal t)
|> Iter.iter
(fun sub ->
Log.debugf 5 (fun k->k "(@[solver.map-bool-subterm-to-lit@ :subterm %a@])" Term.pp sub);
(* ensure that SAT solver has a boolean atom for [sub] *)
let lit = Lit.atom self.si.tst sub in
Sat_solver.add_lit self.solver lit;
(* also map [sub] to this atom in the congruence closure, for propagation *)
let cc = cc self in
CC.set_as_lit cc (CC.add_term cc sub) lit;
())
let preprocess_acts_of_solver_
(self:t) : (module Solver_internal.PREPROCESS_ACTS) =
(module struct
let mk_lit ?sign t = Lit.atom ?sign self.si.tst t
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 literals, making them ready for being added to the solver *)
let rec preprocess_lit_ self lit : Lit.t * dproof =
let lit, proof =
Solver_internal.preprocess_lit_
~add_clause:(fun lits proof ->
(* recursively add these sub-literals, so they're also properly processed *)
Stat.incr self.si.count_preprocess_clause;
let pr_l = ref [] in
let lits =
CCList.map
(fun lit ->
let a, pr = preprocess_lit_ self lit in
(* FIXME if not (P.is_trivial_refl pr) then ( *)
pr_l := pr :: !pr_l;
(* ); *)
a)
lits
in
let emit_proof p = List.iter (fun dp -> dp p) !pr_l; in
Sat_solver.add_clause self.solver lits emit_proof)
self.si lit
in
Sat_solver.add_lit self.solver lit;
lit, proof
(* preprocess literal *)
let preprocess_lit_ (self:t) (lit:lit) : lit =
let pacts = preprocess_acts_of_solver_ self in
Solver_internal.preprocess_lit_ self.si pacts lit
(* FIXME: should we just add the proof instead? *)
let[@inline] preprocess_lit' self lit : Lit.t =
fst (preprocess_lit_ self lit)
(* FIXME: should we just assert the proof instead? or do we wait because
we're most likely in a subproof? *)
let rec mk_lit_t (self:t) ?sign (t:term) : lit * dproof =
let lit = Lit.atom ?sign self.si.tst t in
let lit, proof = preprocess_lit_ self lit in
Sat_solver.add_lit self.solver lit;
add_bool_subterms_ self (Lit.term lit);
lit, proof
let[@inline] mk_lit_t' self ?sign lit = mk_lit_t self ?sign lit |> fst
(* make a literal from a term, ensuring it is properly preprocessed *)
let mk_lit_t (self:t) ?sign (t:term) : lit =
let pacts = preprocess_acts_of_solver_ self in
Solver_internal.mk_plit self.si pacts ?sign t
(** {2 Result} *)
@ -699,12 +696,11 @@ module Make(A : ARG)
let assert_terms self c =
let c = CCList.map (fun t -> Lit.atom (tst self) t) c in
let emit_proof p =
P.emit_input_clause p (Iter.of_list c)
in
(* FIXME: just emit proofs on the fly? *)
let c = CCList.map (preprocess_lit' self) c in
add_clause_l self c emit_proof
let c = CCList.map (preprocess_lit_ self) c in
(* TODO: if c != c0 then P.emit_redundant_clause c
because we jsut preprocessed it away? *)
let dp = P.emit_input_clause (Iter.of_list c) in
add_clause_l self c dp
let assert_term self t = assert_terms self [t]

23
src/smtlib/Process.ml
View file

@ -233,7 +233,7 @@ let process_stmt
(* FIXME: how to map [l] to [assumptions] in proof? *)
let assumptions =
List.map
(fun (sign,t) -> Solver.mk_lit_t' solver ~sign t)
(fun (sign,t) -> Solver.mk_lit_t solver ~sign t)
l
in
solve
@ -253,33 +253,24 @@ let process_stmt
if pp_cnf then (
Format.printf "(@[<hv1>assert@ %a@])@." Term.pp t
);
let lit = Solver.mk_lit_t' solver t in
let lit = Solver.mk_lit_t solver t in
Solver.add_clause solver (IArray.singleton lit)
(fun p -> Solver.P.emit_input_clause p (Iter.singleton lit));
(Solver.P.emit_input_clause (Iter.singleton lit));
E.return()
| Statement.Stmt_assert_clause c_ts ->
if pp_cnf then (
Format.printf "(@[<hv1>assert-clause@ %a@])@." (Util.pp_list Term.pp) c_ts
);
let pr_l = ref [] in
let c =
List.map
(fun t ->
let lit, pr = Solver.mk_lit_t solver t in
pr_l := pr :: !pr_l;
lit)
c_ts in
let c = CCList.map (fun t -> Solver.mk_lit_t solver t) c_ts in
(* proof of assert-input + preprocessing *)
let emit_proof p =
let module P = Solver.P in
P.begin_subproof p;
let tst = Solver.tst solver in
P.emit_input_clause p (Iter.of_list c_ts |> Iter.map (Lit.atom tst));
List.iter (fun dp -> dp p) !pr_l;
P.emit_redundant_clause p (Iter.of_list c);
P.end_subproof p;
P.emit_input_clause (Iter.of_list c_ts |> Iter.map (Lit.atom tst)) p;
P.emit_redundant_clause (Iter.of_list c) p;
in
Solver.add_clause solver (IArray.of_list c) emit_proof;

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

@ -36,20 +36,20 @@ module type ARG = sig
Only enable if some theories are susceptible to
create boolean formulas during the proof search. *)
val lemma_bool_tauto : S.P.t -> S.Lit.t Iter.t -> unit
val lemma_bool_tauto : S.Lit.t Iter.t -> S.P.t -> unit
(** Boolean tautology lemma (clause) *)
val lemma_bool_c : S.P.t -> string -> term list -> unit
val lemma_bool_c : string -> term list -> S.P.t -> 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
val lemma_bool_equiv : term -> term -> S.P.t -> unit
(** Boolean tautology lemma (equivalence) *)
val lemma_ite_true : S.P.t -> a:term -> ite:term -> unit
val lemma_ite_true : a:term -> ite:term -> S.P.t -> unit
(** lemma [a => ite a b c = b] *)
val lemma_ite_false : S.P.t -> a:term -> ite:term -> unit
val lemma_ite_false : a:term -> ite:term -> S.P.t -> unit
(** lemma [¬a => ite a b c = c] *)
(** Fresh symbol generator.
@ -102,7 +102,7 @@ module Make(A : ARG) : S with module A = A = struct
type state = {
tst: T.store;
ty_st: Ty.store;
cnf: (Lit.t * SI.dproof) T.Tbl.t; (* tseitin CNF *)
cnf: Lit.t T.Tbl.t; (* tseitin CNF *)
gensym: A.Gensym.t;
}
@ -118,14 +118,16 @@ 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_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.dproof) option =
let simplify (self:state) (simp:SI.Simplify.t) (t:T.t) : T.t option =
let tst = self.tst 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)
if not (T.equal t u) then (
SI.Simplify.with_proof simp (fun p ->
A.lemma_bool_equiv t u p;
A.S.P.lemma_preprocess t u p;
);
);
Some u
in
match A.view_as_bool t with
| B_bool _ -> None
@ -148,14 +150,14 @@ module Make(A : ARG) : S with module A = A = struct
| B_ite (a,b,c) ->
(* directly simplify [a] so that maybe we never will simplify one
of the branches *)
let a, pr_a = SI.Simplify.normalize_t simp a in
let a = SI.Simplify.normalize_t simp a in
begin match A.view_as_bool a with
| B_bool true ->
let emit_proof p = pr_a p; A.lemma_ite_true p ~a ~ite:t in
Some (b, emit_proof)
SI.Simplify.with_proof simp (A.lemma_ite_true ~a ~ite:t);
Some b
| B_bool false ->
let emit_proof p = pr_a p; A.lemma_ite_false p ~a ~ite:t in
Some (c, emit_proof)
SI.Simplify.with_proof simp (A.lemma_ite_false ~a ~ite:t);
Some c
| _ ->
None
end
@ -186,136 +188,124 @@ module Make(A : ARG) : S with module A = A = struct
proxy, mk_lit proxy
(* preprocess "ite" away *)
let preproc_ite self si ~mk_lit ~add_clause (t:T.t) : (T.t * SI.dproof) option =
let preproc_ite self si (module PA:SI.PREPROCESS_ACTS) (t:T.t) : T.t option =
match A.view_as_bool t with
| B_ite (a,b,c) ->
let a, pr_a = SI.simp_t si a in
let a = SI.simp_t si a in
begin match A.view_as_bool a with
| B_bool true ->
(* [a=true |- ite a b c=b], [|- a=true] ==> [|- t=b] *)
let emit_proof p = pr_a p; A.lemma_ite_true p ~a ~ite:t in
Some (b, emit_proof)
SI.with_proof si (A.lemma_ite_true ~a ~ite:t);
Some b
| B_bool false ->
(* [a=false |- ite a b c=c], [|- a=false] ==> [|- t=c] *)
let emit_proof p = pr_a p; A.lemma_ite_false p ~a ~ite:t in
Some (c, emit_proof)
SI.with_proof si (A.lemma_ite_false ~a ~ite:t);
Some 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 lit_a = mk_lit a in
add_clause [Lit.neg lit_a; mk_lit (eq self.tst t_ite b)]
(fun p -> A.lemma_ite_true p ~a ~ite:t);
add_clause [lit_a; mk_lit (eq self.tst t_ite c)]
SI.with_proof si (SI.P.define_term t_ite t);
let lit_a = PA.mk_lit a in
PA.add_clause [Lit.neg lit_a; PA.mk_lit (eq self.tst t_ite b)]
(fun p -> A.lemma_ite_true ~a ~ite:t p);
PA.add_clause [lit_a; PA.mk_lit (eq self.tst t_ite c)]
(fun p -> A.lemma_ite_false p ~a ~ite:t);
Some (t_ite, fun p -> SI.P.define_term p t_ite t)
Some t_ite
end
| _ -> None
(* TODO: polarity? *)
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 * _ =
let cnf (self:state) (si:SI.t) (module PA:SI.PREPROCESS_ACTS) (t:T.t) : T.t option =
let rec get_lit (t:T.t) : Lit.t =
let t_abs, t_sign = T.abs self.tst t in
let lit_abs, pr =
let lit_abs =
match T.Tbl.find self.cnf t_abs with
| lit_pr -> lit_pr (* cached *)
| lit -> lit (* cached *)
| exception Not_found ->
(* compute and cache *)
let lit, pr = get_lit_uncached si t_abs in
let lit = get_lit_uncached si t_abs in
if not (T.equal (Lit.term lit) t_abs) then (
T.Tbl.add self.cnf t_abs (lit, pr);
T.Tbl.add self.cnf t_abs lit;
Log.debugf 20
(fun k->k "(@[sidekick.bool.add-lit@ :lit %a@ :for-t %a@])"
Lit.pp lit T.pp t_abs);
);
lit, pr
lit
in
let lit = if t_sign then lit_abs else Lit.neg lit_abs in
lit, pr
lit
and equiv_ si ~get_lit ~is_xor ~for_t t_a t_b : Lit.t * SI.dproof =
and equiv_ si ~get_lit ~is_xor ~for_t t_a t_b : Lit.t =
let a = get_lit t_a 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 t_proxy, proxy = fresh_lit ~for_t ~mk_lit ~pre:"equiv_" self in
let t_proxy, proxy = fresh_lit ~for_t ~mk_lit:PA.mk_lit ~pre:"equiv_" self in
SI.define_const si ~const:t_proxy ~rhs:for_t;
SI.with_proof si (SI.P.define_term t_proxy for_t);
let add_clause c pr =
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]
(fun p ->
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]);
(if is_xor then A.lemma_bool_c "xor-e+" [t_proxy]
else A.lemma_bool_c "eq-e" [t_proxy; t_a]);
add_clause [Lit.neg proxy; Lit.neg b; a]
(fun p ->
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]);
(if is_xor then A.lemma_bool_c "xor-e-" [t_proxy]
else A.lemma_bool_c "eq-e" [t_proxy; t_b]);
add_clause [proxy; a; b]
(fun p -> if is_xor then A.lemma_bool_c p "xor-i" [t_proxy; t_a]
else A.lemma_bool_c p "eq-i+" [t_proxy]);
(if is_xor then A.lemma_bool_c "xor-i" [t_proxy; t_a]
else A.lemma_bool_c "eq-i+" [t_proxy]);
add_clause [proxy; Lit.neg a; Lit.neg b]
(fun p ->
if is_xor then A.lemma_bool_c p "xor-i" [t_proxy; t_b]
else A.lemma_bool_c p "eq-i-" [t_proxy]);
proxy, (fun p->SI.P.define_term p t_proxy for_t)
(if is_xor then A.lemma_bool_c "xor-i" [t_proxy; t_b]
else A.lemma_bool_c "eq-i-" [t_proxy]);
proxy
(* make a literal for [t], with a proof of [|- abs(t) = abs(lit)] *)
and get_lit_uncached si t : Lit.t * SI.dproof =
let sub_p = ref [] in
let get_lit t =
let lit, pr = get_lit_and_proof_ t in
if Lit.term lit != t then (
sub_p := pr :: !sub_p;
);
lit
in
and get_lit_uncached si t : Lit.t =
match A.view_as_bool t with
| B_bool b -> mk_lit (T.bool self.tst b), (fun _->())
| B_opaque_bool t -> mk_lit t, (fun _->())
| B_bool b -> PA.mk_lit (T.bool self.tst b)
| B_opaque_bool t -> PA.mk_lit t
| B_not u ->
let lit, pr = get_lit_and_proof_ u in
Lit.neg lit, pr
let lit = get_lit u in
Lit.neg lit
| B_and l ->
let t_subs = Iter.to_list l in
let subs = List.map get_lit t_subs in
let t_proxy, proxy = fresh_lit ~for_t:t ~mk_lit ~pre:"and_" self in
let t_proxy, proxy = fresh_lit ~for_t:t ~mk_lit:PA.mk_lit ~pre:"and_" self in
SI.define_const si ~const:t_proxy ~rhs:t;
SI.with_proof si (SI.P.define_term t_proxy t);
(* add clauses *)
List.iter2
(fun t_u u ->
add_clause
PA.add_clause
[Lit.neg proxy; u]
(fun p -> A.lemma_bool_c p "and-e" [t_proxy; t_u]))
(A.lemma_bool_c "and-e" [t_proxy; t_u]))
t_subs subs;
add_clause (proxy :: List.map Lit.neg subs)
(fun p -> A.lemma_bool_c p "and-i" [t_proxy]);
let emit_proof p =
SI.P.define_term p t_proxy t;
in
proxy, emit_proof
PA.add_clause (proxy :: List.map Lit.neg subs)
(A.lemma_bool_c "and-i" [t_proxy]);
proxy
| B_or l ->
let t_subs = Iter.to_list l in
let subs = List.map get_lit t_subs in
let t_proxy, proxy = fresh_lit ~for_t:t ~mk_lit ~pre:"or_" self in
let t_proxy, proxy = fresh_lit ~for_t:t ~mk_lit:PA.mk_lit ~pre:"or_" self in
SI.define_const si ~const:t_proxy ~rhs:t;
SI.with_proof si (SI.P.define_term t_proxy t);
(* add clauses *)
List.iter2
(fun t_u u ->
add_clause [Lit.neg u; proxy]
(fun p -> A.lemma_bool_c p "or-i" [t_proxy; t_u]))
PA.add_clause [Lit.neg u; proxy]
(A.lemma_bool_c "or-i" [t_proxy; t_u]))
t_subs subs;
add_clause (Lit.neg proxy :: subs)
(fun p -> A.lemma_bool_c p "or-e" [t_proxy]);
let emit_proof p = SI.P.define_term p t_proxy t in
proxy, emit_proof
PA.add_clause (Lit.neg proxy :: subs)
(A.lemma_bool_c "or-e" [t_proxy]);
proxy
| B_imply (t_args, t_u) ->
(* transform into [¬args \/ u] on the fly *)
@ -325,35 +315,35 @@ module Make(A : ARG) : S with module A = A = struct
let subs = u :: args in
(* now the or-encoding *)
let t_proxy, proxy = fresh_lit ~for_t:t ~mk_lit ~pre:"implies_" self in
let t_proxy, proxy = fresh_lit ~for_t:t ~mk_lit:PA.mk_lit ~pre:"implies_" self in
SI.define_const si ~const:t_proxy ~rhs:t;
SI.with_proof si (SI.P.define_term t_proxy t);
(* add clauses *)
List.iter2
(fun t_u u ->
add_clause [Lit.neg u; proxy]
(fun p -> A.lemma_bool_c p "imp-i" [t_proxy; t_u]))
PA.add_clause [Lit.neg u; proxy]
(A.lemma_bool_c "imp-i" [t_proxy; t_u]))
(t_u::t_args) subs;
add_clause (Lit.neg proxy :: subs)
(fun p -> A.lemma_bool_c p "imp-e" [t_proxy]);
let emit_proof p = SI.P.define_term p t_proxy t in
proxy, emit_proof
PA.add_clause (Lit.neg proxy :: subs)
(A.lemma_bool_c "imp-e" [t_proxy]);
proxy
| B_ite _ | B_eq _ | B_neq _ -> mk_lit t, (fun _ ->())
| B_ite _ | B_eq _ | B_neq _ -> PA.mk_lit t
| 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:t ~is_xor:true a b
| B_atom u -> mk_lit u, (fun _->())
| B_atom u -> PA.mk_lit u
in
let lit, pr = get_lit_and_proof_ t in
let lit = get_lit t in
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, pr)
if T.equal u t then None else Some u
(* 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.actions) (_trail:_ Iter.t) : unit =
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
@ -362,15 +352,14 @@ module Make(A : ARG) : S with module A = A = struct
|> Iter.map CC.N.term
in
let cnf_of t =
cnf self si t
~mk_lit:(SI.mk_lit si acts) ~add_clause:(SI.add_clause_permanent si acts)
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) ->
(* FIXME: what to do with pr_t_u? emit it? *)
| Some u ->
Log.debugf 5
(fun k->k "(@[th-bool-static.final-check.cnf@ %a@ :yields %a@])"
T.pp t T.pp u);

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

@ -74,9 +74,9 @@ module type ARG = sig
val ty_is_finite : S.T.Ty.t -> bool
val ty_set_is_finite : S.T.Ty.t -> bool -> unit
val lemma_isa_split : S.proof -> S.Lit.t Iter.t -> unit
val lemma_isa_disj : S.proof -> S.Lit.t Iter.t -> unit
val lemma_cstor_inj : S.proof -> S.Lit.t Iter.t -> unit
val lemma_isa_split : S.Lit.t Iter.t -> S.proof -> unit
val lemma_isa_disj : S.Lit.t Iter.t -> S.proof -> unit
val lemma_cstor_inj : S.Lit.t Iter.t -> S.proof -> unit
end
(** Helper to compute the cardinality of types *)
@ -496,7 +496,7 @@ module Make(A : ARG) : S with module A = A = struct
end;
g
let check (self:t) (solver:SI.t) (acts:SI.actions) : unit =
let check (self:t) (solver:SI.t) (acts:SI.theory_actions) : unit =
let cc = SI.cc solver in
(* create graph *)
let g = mk_graph self cc in
@ -574,19 +574,19 @@ module Make(A : ARG) : S with module A = A = struct
|> Iter.to_rev_list
in
SI.add_clause_permanent solver acts c
(fun p -> A.lemma_isa_split p (Iter.of_list c));
(A.lemma_isa_split (Iter.of_list c));
Iter.diagonal_l c
(fun (c1,c2) ->
let emit_proof p =
A.lemma_isa_disj p (Iter.of_list [SI.Lit.neg c1; SI.Lit.neg c2]) in
let pr =
A.lemma_isa_disj (Iter.of_list [SI.Lit.neg c1; SI.Lit.neg c2]) in
SI.add_clause_permanent solver acts
[SI.Lit.neg c1; SI.Lit.neg c2] emit_proof);
[SI.Lit.neg c1; SI.Lit.neg c2] pr);
)
(* on final check, check acyclicity,
then make sure we have done case split on all terms that
need it. *)
let on_final_check (self:t) (solver:SI.t) (acts:SI.actions) trail =
let on_final_check (self:t) (solver:SI.t) (acts:SI.theory_actions) trail =
Profile.with_ "data.final-check" @@ fun () ->
check_is_a self solver acts trail;

6
src/th-data/Sidekick_th_data.mli
View file

@ -74,9 +74,9 @@ module type ARG = sig
(* TODO: should we store this ourself? would be simpler… *)
val lemma_isa_split : S.proof -> S.Lit.t Iter.t -> unit
val lemma_isa_disj : S.proof -> S.Lit.t Iter.t -> unit
val lemma_cstor_inj : S.proof -> S.Lit.t Iter.t -> unit
val lemma_isa_split : S.Lit.t Iter.t -> S.proof -> unit
val lemma_isa_disj : S.Lit.t Iter.t -> S.proof -> unit
val lemma_cstor_inj : S.Lit.t Iter.t -> S.proof -> unit
end
module type S = sig