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

wip: feat(proof): insert proof constructs in most of sidekick

Browse source
This commit is contained in:
Simon Cruanes 2021-04-15 00:03:15 -04:00
parent 683909c6ef
commit ff7a87f3fb
8 changed files with 385 additions and 180 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

21
src/cc/Sidekick_cc.ml
View file

@ -95,6 +95,7 @@ module Make (A: CC_ARG)
| E_congruence of node * node (* caused by normal congruence *)
| E_and of explanation * explanation
| E_theory of explanation
| E_proof of P.t
type repr = node
@ -168,6 +169,7 @@ module Make (A: CC_ARG)
| E_merge (a,b) -> Fmt.fprintf out "(@[merge@ %a@ %a@])" N.pp a N.pp b
| E_merge_t (a,b) -> Fmt.fprintf out "(@[<hv>merge@ @[:n1 %a@]@ @[:n2 %a@]@])" Term.pp a Term.pp b
| E_theory e -> Fmt.fprintf out "(@[th@ %a@])" pp e
| E_proof p -> Fmt.fprintf out "(@[proof@ %a@])" P.pp p
| E_and (a,b) ->
Format.fprintf out "(@[<hv1>and@ %a@ %a@])" pp a pp b
@ -177,6 +179,7 @@ module Make (A: CC_ARG)
let[@inline] mk_merge_t a b : t = if Term.equal a b then mk_reduction else E_merge_t (a,b)
let[@inline] mk_lit l : t = E_lit l
let mk_theory e = E_theory e
let mk_proof p = E_proof p
let rec mk_list l =
match l with
@ -280,7 +283,7 @@ module Make (A: CC_ARG)
and ev_on_post_merge = t -> actions -> N.t -> N.t -> unit
and ev_on_new_term = t -> N.t -> term -> unit
and ev_on_conflict = t -> th:bool -> lit list -> unit
and ev_on_propagate = t -> lit -> (unit -> lit list) -> unit
and ev_on_propagate = t -> lit -> (unit -> lit list * P.t) -> unit
and ev_on_is_subterm = N.t -> term -> unit
let[@inline] size_ (r:repr) = r.n_size
@ -458,6 +461,9 @@ module Make (A: CC_ARG)
| E_lit lit -> lit :: acc
| E_theory e' ->
th := true; explain_decompose cc ~th acc e'
| E_proof _p ->
(* FIXME: need to also return pairs of [t, u, |-t=u] as part of explanation *)
assert false
| E_merge (a,b) -> explain_pair cc ~th acc a b
| E_merge_t (a,b) ->
(* find nodes for [a] and [b] on the fly *)
@ -657,7 +663,7 @@ module Make (A: CC_ARG)
Iter.of_list lits
|> Iter.map (fun lit -> Lit.term lit, Lit.sign lit)
in
P.make_cc lits
P.cc_lemma lits
in
raise_conflict_ cc ~th:!th acts (List.rev_map Lit.neg lits) proof
);
@ -773,13 +779,18 @@ module Make (A: CC_ARG)
let reason =
let e = lazy (
let lazy (th, acc) = half_expl in
explain_pair cc ~th acc u1 t1
let lits = explain_pair cc ~th acc u1 t1 in
let p =
A.P.cc_lemma
(Iter.of_list lits |> Iter.map (fun l -> Lit.term l, Lit.sign l))
in
lits, p
) in
fun () -> Lazy.force e
in
List.iter (fun f -> f cc lit reason) cc.on_propagate;
Stat.incr cc.count_props;
Actions.propagate acts lit ~reason P.default
Actions.propagate acts lit ~reason
| _ -> ())
module Debug_ = struct
@ -845,7 +856,7 @@ module Make (A: CC_ARG)
Iter.of_list lits
|> Iter.map (fun lit -> Lit.term lit, Lit.sign lit)
in
P.make_cc lits
P.cc_lemma lits
in
raise_conflict_ cc ~th:!th acts lits proof

72
src/core/Sidekick_core.ml
View file

@ -147,10 +147,24 @@ end
module type PROOF = sig
type term
type clause
type t
val pp : t Fmt.printer
val default : t
val make_cc : (term*bool) Iter.t -> t
(** hyper-resolution steps: resolution, unit resolution; bool paramodulation, unit bool paramodulation *)
type hres_step = | R | R1 | P | P1
val hres_iter : t -> (hres_step * t) Iter.t -> t (* hyper-res *)
val hres_l : t -> (hres_step * t) list -> t (* hyper-res *)
val refl : term -> t (* proof of [| t=t] *)
val true_is_true : t (* proof of [|- true] *)
val true_neq_false : t (* proof of [|- not (true=false)] *)
val cc_lemma : (term*bool) Iter.t -> t (* equality tautology, unsigned *)
val cc_imply2 : t -> t -> term -> term -> t (* tautology [p1, p2 |- t=u] *)
val cc_imply_l : t list -> term -> term -> t (* tautology [hyps |- t=u] *)
val sorry : t [@@alert cstor "sorry used"] (* proof hole when we don't know how to produce a proof *)
val default : t [@@alert cstor "do not use default constructor"]
end
(** Literals
@ -208,7 +222,7 @@ module type CC_ACTIONS = sig
exception).
@param pr the proof of [c] being a tautology *)
val propagate : t -> Lit.t -> reason:(unit -> Lit.t list) -> P.t -> unit
val propagate : t -> Lit.t -> reason:(unit -> Lit.t list * P.t) -> unit
(** [propagate acts lit ~reason pr] declares that [reason() => lit]
is a tautology.
@ -310,6 +324,7 @@ module type CC_S = sig
val mk_merge_t : term -> term -> t
val mk_lit : lit -> t
val mk_list : t list -> t
val mk_proof : P.t -> t
val mk_theory : t -> t (* TODO: indicate what theory, or even provide a lemma *)
end
@ -362,7 +377,7 @@ module type CC_S = sig
participating in the conflict are purely syntactic theories
like injectivity of constructors. *)
type ev_on_propagate = t -> lit -> (unit -> lit list) -> unit
type ev_on_propagate = t -> lit -> (unit -> lit list * P.t) -> unit
(** [ev_on_propagate cc lit reason] is called whenever [reason() => lit]
is a propagated lemma. See {!CC_ACTIONS.propagate}. *)
@ -437,6 +452,8 @@ module type CC_S = sig
val assert_lits : t -> lit Iter.t -> unit
(** Addition of many literals *)
(* FIXME: this needs to return [lit list * (term*term*P.t) list].
the explanation is [/\_i lit_i /\ /\_j (|- t_j=u_j) |- n1=n2] *)
val explain_eq : t -> N.t -> N.t -> lit list
(** Explain why the two nodes are equal.
Fails if they are not, in an unspecified way *)
@ -546,7 +563,7 @@ module type SOLVER_INTERNAL = sig
val clear : t -> unit
(** Reset internal cache, etc. *)
type hook = t -> term -> term option
type hook = t -> term -> (term * proof) 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],
@ -557,6 +574,11 @@ module type SOLVER_INTERNAL = sig
(** 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 * P.t
(** Normalize a term using all the hooks, along with a proof that the
simplification is correct.
returns [t, refl t] if no simplification occurred. *)
end
type simplify_hook = Simplify.hook
@ -566,12 +588,18 @@ module type SOLVER_INTERNAL = sig
val simplifier : t -> Simplify.t
val simp_t : t -> term -> term
(** Simplify the term using the solver's simplifier (see {!simplifier}) *)
val simplify_t : t -> term -> (term * proof) option
(** Simplify input term, returns [Some (u, |- t=u)] if some
simplification occurred. *)
val simp_t : t -> term -> term * proof
(** [simp_t si t] returns [u, |- t=u] even if no simplification occurred
(in which case [t == u] syntactically).
(see {!simplifier}) *)
(** {3 hooks for the theory} *)
val propagate : t -> actions -> lit -> reason:(unit -> lit list) -> proof -> unit
val propagate : t -> actions -> lit -> reason:(unit -> lit list * proof) -> unit
(** Propagate a literal for a reason. This is similar to asserting
the clause [reason => lit], but more lightweight, and in a way
that is backtrackable. *)
@ -585,19 +613,19 @@ module type SOLVER_INTERNAL = sig
If the SAT solver backtracks, this (potential) decision is removed
and forgotten. *)
val propagate: t -> actions -> lit -> (unit -> lit list) -> unit
val propagate: t -> actions -> lit -> (unit -> lit list * proof) -> 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 -> unit
val propagate_l: t -> actions -> lit -> lit list -> proof -> 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 -> unit
val add_clause_temp : t -> actions -> lit list -> proof -> 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 -> unit
val add_clause_permanent : t -> actions -> lit list -> proof -> unit
(** Add toplevel clause to the SAT solver. This clause will
not be backtracked. *)
@ -605,7 +633,7 @@ module type SOLVER_INTERNAL = sig
(** Create a literal. This automatically preprocesses the term. *)
val preprocess_term :
t -> add_clause:(Lit.t list -> unit) -> term -> term
t -> add_clause:(Lit.t list -> proof -> unit) -> term -> term * proof
(** Preprocess a term. *)
val add_lit : t -> actions -> lit -> unit
@ -661,7 +689,7 @@ module type SOLVER_INTERNAL = sig
val on_cc_conflict : t -> (CC.t -> th:bool -> lit list -> unit) -> unit
(** Callback called on every CC conflict *)
val on_cc_propagate : t -> (CC.t -> lit -> (unit -> lit list) -> unit) -> unit
val on_cc_propagate : t -> (CC.t -> lit -> (unit -> lit list * proof) -> unit) -> unit
(** Callback called on every CC propagation *)
val on_partial_check : t -> (t -> actions -> lit Iter.t -> unit) -> unit
@ -688,9 +716,10 @@ module type SOLVER_INTERNAL = sig
type preprocess_hook =
t ->
mk_lit:(term -> lit) ->
add_clause:(lit list -> unit) ->
term -> term option
(** Given a term, try to preprocess it. Return [None] if it didn't change.
add_clause:(lit list -> proof -> unit) ->
term -> (term * proof) 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
@ -853,6 +882,11 @@ module type SOLVER = sig
*)
end
(** {3 Proof type}
The representation of a full proof, including toplevel steps
with intermediate, named, clauses. Each clause is justified by
a {!P.t} lemma. *)
module Proof : sig
type t
val check : t -> unit
@ -906,11 +940,11 @@ module type SOLVER = sig
val mk_atom_t : t -> ?sign:bool -> term -> Atom.t
(** Turn a boolean term, with a sign, into a SAT solver's literal. *)
val add_clause : t -> Atom.t IArray.t -> unit
val add_clause : t -> Atom.t IArray.t -> P.t -> unit
(** [add_clause solver cs] adds a boolean clause to the solver.
Subsequent calls to {!solve} will need to satisfy this clause. *)
val add_clause_l : t -> Atom.t list -> unit
val add_clause_l : t -> Atom.t list -> P.t -> unit
(** Same as {!add_clause} but with a list of atoms. *)
(** Result of solving for the current set of clauses *)

55
src/lra/sidekick_arith_lra.ml
View file

@ -57,6 +57,9 @@ module type ARG = sig
val has_ty_real : term -> bool
(** Does this term have the type [Real] *)
(** TODO: actual proof *)
val proof_lra : S.lemma
module Gensym : sig
type t
@ -228,12 +231,22 @@ module Make(A : ARG) : S with module A = A = struct
proxy
(* preprocess linear expressions away *)
let preproc_lra (self:state) si ~mk_lit ~add_clause (t:T.t) : T.t option =
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 tst = SI.tst si in
let sub_proofs_ = ref [] in
(* preprocess subterm *)
let preproc_t = SI.preprocess_term ~add_clause si in
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
(* tell the CC this term exists *)
let declare_term_to_cc t =
@ -255,9 +268,9 @@ module Make(A : ARG) : S with module A = A = struct
let lit_t = mk_lit t in
let lit_u1 = mk_lit u1 in
let lit_u2 = mk_lit u2 in
add_clause [SI.Lit.neg lit_t; lit_u1];
add_clause [SI.Lit.neg lit_t; lit_u2];
add_clause [SI.Lit.neg lit_u1; SI.Lit.neg lit_u2; lit_t];
add_clause [SI.Lit.neg lit_t; lit_u1] A.proof_lra;
add_clause [SI.Lit.neg lit_t; lit_u2] A.proof_lra;
add_clause [SI.Lit.neg lit_u1; SI.Lit.neg lit_u2; lit_t] A.proof_lra;
);
None
@ -292,7 +305,9 @@ module Make(A : ARG) : S with module A = A = struct
end;
Log.debugf 10 (fun k->k "lra.preprocess:@ %a@ :into %a" T.pp t T.pp new_t);
Some new_t
(* FIXME: by def proxy + LRA *)
let proof = A.S.P.sorry in
Some (new_t, proof)
| Some (coeff, v), pred ->
(* [c . v <= const] becomes a direct simplex constraint [v <= const/c] *)
@ -317,7 +332,8 @@ module Make(A : ARG) : S with module A = A = struct
end;
Log.debugf 10 (fun k->k "lra.preprocess@ :%a@ :into %a" T.pp t T.pp new_t);
Some new_t
let proof = A.proof_lra in
Some (new_t, proof)
end
| LRA_op _ | LRA_mult _ ->
@ -330,7 +346,10 @@ module Make(A : ARG) : S with module A = A = struct
let proxy = var_encoding_comb self ~pre:"_le" le_comb in
declare_term_to_cc proxy;
Some proxy
(* TODO: proof by def of proxy *)
let proof = A.S.P.sorry in
Some (proxy, proof)
) else (
(* a bit more complicated: we cannot just define [proxy := le_comb]
because of the coefficient.
@ -355,24 +374,26 @@ module Make(A : ARG) : S with module A = A = struct
add_clause [
mk_lit (A.mk_lra tst (LRA_simplex_pred (proxy2, Leq, Q.neg le_const)))
];
] A.S.P.sorry; (* TODO: by-def proxy2 + LRA *)
add_clause [
mk_lit (A.mk_lra tst (LRA_simplex_pred (proxy2, Geq, Q.neg le_const)))
];
] A.S.P.sorry; (* TODO: by-def proxy2 + LRA *)
Some proxy
(* FIXME: actual proof *)
let proof = A.S.P.sorry in
Some (proxy, proof)
)
| LRA_other t when A.has_ty_real t -> None
| LRA_const _ | LRA_simplex_pred _ | LRA_simplex_var _ | LRA_other _ -> None
let simplify (self:state) (_recurse:_) (t:T.t) : T.t option =
let simplify (self:state) (_recurse:_) (t:T.t) : (T.t * SI.proof) 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
Some (A.mk_lra self.tst (LRA_const c))
Some (A.mk_lra self.tst (LRA_const c), A.proof_lra)
) else None
| LRA_pred (pred, l1, l2) ->
let le = LE.(as_linexp_id l1 - as_linexp_id l2) in
@ -386,7 +407,7 @@ module Make(A : ARG) : S with module A = A = struct
| Eq -> Q.(c = zero)
| Neq -> Q.(c <> zero)
in
Some (A.mk_bool self.tst is_true)
Some (A.mk_bool self.tst is_true, A.proof_lra)
) else None
| _ -> None
@ -400,13 +421,15 @@ module Make(A : ARG) : S with module A = A = struct
|> CCList.flat_map (Tag.to_lits si)
|> List.rev_map SI.Lit.neg
in
SI.raise_conflict si acts confl SI.P.default
(* TODO: more detailed proof certificate *)
SI.raise_conflict si acts confl A.proof_lra
let on_propagate_ si acts lit ~reason =
match lit with
| Tag.Lit lit ->
(* TODO: more detailed proof certificate *)
SI.propagate si acts lit
(fun() -> CCList.flat_map (Tag.to_lits si) reason)
(fun() -> CCList.flat_map (Tag.to_lits si) reason, A.proof_lra)
| _ -> ()
let check_simplex_ self si acts : SimpSolver.Subst.t =

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

@ -93,8 +93,8 @@ module Make(A : ARG)
type t = msat_acts
let[@inline] raise_conflict a lits pr =
a.Msat.acts_raise_conflict lits pr
let[@inline] propagate a lit ~reason pr =
let reason = Msat.Consequence (fun () -> reason(), pr) in
let[@inline] propagate a lit ~reason =
let reason = Msat.Consequence reason in
a.Msat.acts_propagate lit reason
end
end
@ -134,7 +134,7 @@ module Make(A : ARG)
mutable hooks: hook list;
cache: Term.t Term.Tbl.t;
}
and hook = t -> term -> term option
and hook = t -> term -> (term * P.t) option
let create tst ty_st : t =
{tst; ty_st; hooks=[]; cache=Term.Tbl.create 32;}
@ -143,9 +143,11 @@ module Make(A : ARG)
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 =
let normalize (self:t) (t:Term.t) : (Term.t * P.t) option =
let sub_proofs_ = ref [] in
(* compute and cache normal form of [t] *)
let rec aux t =
let rec aux t : Term.t =
match Term.Tbl.find self.cache t with
| u -> u
| exception Not_found ->
@ -160,10 +162,23 @@ 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 -> aux u
| 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
in
aux t
let u = aux t in
if Term.equal t u then None
else (
(* proof: [sub_proofs |- t=u] by CC *)
let pr = P.cc_imply_l !sub_proofs_ t u in
Some (u, pr)
)
let normalize_t self t =
match normalize self t with
| None -> t, P.refl t
| Some (u,pr) -> u, pr
end
type simplify_hook = Simplify.hook
@ -180,7 +195,7 @@ module Make(A : ARG)
simp: Simplify.t;
mutable preprocess: preprocess_hook list;
mutable mk_model: model_hook list;
preprocess_cache: Term.t Term.Tbl.t;
preprocess_cache: (Term.t * P.t) Term.Tbl.t;
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;
@ -190,8 +205,8 @@ module Make(A : ARG)
and preprocess_hook =
t ->
mk_lit:(term -> lit) ->
add_clause:(lit list -> unit) ->
term -> term option
add_clause:(lit list -> P.t -> unit) ->
term -> (term * P.t) option
and model_hook =
recurse:(t -> CC.N.t -> term) ->
@ -216,7 +231,9 @@ module Make(A : ARG)
let stats t = t.stat
let simplifier self = self.simp
let simp_t self (t:Term.t) : Term.t = Simplify.normalize self.simp t
let simplify_t self (t:Term.t) : _ option = Simplify.normalize self.simp t
let simp_t self (t:Term.t) : Term.t * P.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
@ -226,34 +243,58 @@ module Make(A : ARG)
let sign = Lit.sign lit in
acts.Msat.acts_add_decision_lit (Lit.abs lit) sign
let[@inline] raise_conflict self acts c : 'a =
let[@inline] raise_conflict self acts c proof : 'a =
Stat.incr self.count_conflict;
acts.Msat.acts_raise_conflict c P.default
acts.Msat.acts_raise_conflict c proof
let[@inline] propagate self acts p cs : unit =
let[@inline] propagate self acts p reason : unit =
Stat.incr self.count_propagate;
acts.Msat.acts_propagate p (Msat.Consequence (fun () -> cs(), P.default))
acts.Msat.acts_propagate p (Msat.Consequence reason)
let[@inline] propagate_l self acts p cs : unit =
propagate self acts p (fun()->cs)
let[@inline] propagate_l self acts p cs proof : unit =
propagate self acts p (fun()->cs,proof)
let add_sat_clause_ self acts ~keep lits : unit =
let add_sat_clause_ self acts ~keep lits (proof:P.t) : unit =
Stat.incr self.count_axiom;
acts.Msat.acts_add_clause ~keep lits P.default
acts.Msat.acts_add_clause ~keep lits proof
let preprocess_term_ (self:t) ~add_clause (t:term) : term =
let preprocess_term_ (self:t) ~add_clause (t:term) : term * proof =
let mk_lit t = Lit.atom self.tst t in (* no further simplification *)
(* compute and cache normal form of [t] *)
let rec aux t =
let rec aux t : term * proof =
match Term.Tbl.find self.preprocess_cache t with
| u -> u
| up -> up
| exception Not_found ->
let sub_p = ref [] in
(* try rewrite at root *)
let t1 = aux_rec t self.preprocess in
(* then map subterms *)
let t2 = Term.map_shallow self.tst aux t1 in (* map subterms *)
let u = if t != t2 then aux t2 (* fixpoint *) else t2 in
let t1 = aux_rec ~sub_p t self.preprocess in
(* map subterms *)
let t2 =
Term.map_shallow self.tst
(fun t_sub ->
let u_sub, p_t = aux t_sub in
if not (Term.equal t_sub u_sub) then (
sub_p := p_t :: !sub_p;
);
u_sub)
t1
in
let u =
if not (Term.equal t t2) then (
(* fixpoint *)
let v, p_t2_v = aux t2 in
if not (Term.equal t2 v) then (
sub_p := p_t2_v :: !sub_p
);
v
) else (
t2
)
in
if t != u then (
Log.debugf 5
@ -261,46 +302,77 @@ module Make(A : ARG)
:from %a@ :to %a@])" Term.pp t Term.pp u);
);
Term.Tbl.add self.preprocess_cache t u;
u
let p_t_u =
if t != u then (
P.cc_imply_l !sub_p t u (* proof: [sub_p |- t=u] *)
) else P.refl t
in
Term.Tbl.add self.preprocess_cache t (u,p_t_u);
u, p_t_u
(* try each function in [hooks] successively *)
and aux_rec t hooks = match hooks with
and aux_rec ~sub_p t hooks : term =
match hooks with
| [] -> t
| h :: hooks_tl ->
match h self ~mk_lit ~add_clause t with
| None -> aux_rec t hooks_tl
| Some u -> aux u
| None -> aux_rec ~sub_p t hooks_tl
| Some (u, p_t_u) ->
sub_p := p_t_u :: !sub_p;
let v, p_u_v = aux u in
if t != v then (
sub_p := p_u_v :: !sub_p;
);
v
in
t |> simp_t self |> aux
let preprocess_lit_ (self:t) ~add_clause (lit:lit) : lit =
let t = Lit.term lit |> preprocess_term_ self ~add_clause in
let t1, p_t_t1 = simp_t self t in
let u, p_t1_u = aux t1 in
if t != u then (
let pr = P.cc_imply2 p_t_t1 p_t1_u t u in
u, pr
) else (
u, P.refl u
)
(* return preprocessed lit + proof they are equal *)
let preprocess_lit_ (self:t) ~add_clause (lit:lit) : lit * proof =
let t, p = Lit.term lit |> preprocess_term_ self ~add_clause in
let lit' = Lit.atom self.tst ~sign:(Lit.sign lit) t in
Log.debugf 10
(fun k->k "(@[msat-solver.preprocess.lit@ :lit %a@ :into %a@])" Lit.pp lit Lit.pp lit');
lit'
(fun k->k "(@[msat-solver.preprocess.lit@ :lit %a@ :into %a@ :proof %a@])"
Lit.pp lit Lit.pp lit' P.pp p);
lit', p
(* add a clause using [acts] *)
let add_clause_ self acts lits : unit =
let add_clause_ self acts lits (proof:P.t) : unit =
Stat.incr self.count_preprocess_clause;
add_sat_clause_ self acts ~keep:true lits
add_sat_clause_ self acts ~keep:true lits proof
let mk_lit self acts ?sign t =
(* 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 =
let[@inline] preprocess_term self ~add_clause (t:term) : term * proof =
preprocess_term_ self ~add_clause t
let[@inline] add_clause_temp self acts lits : unit =
add_sat_clause_ self acts ~keep:false lits
let[@inline] add_clause_temp self acts lits (proof:P.t) : unit =
add_sat_clause_ self acts ~keep:false lits proof
let[@inline] add_clause_permanent self acts lits : unit =
add_sat_clause_ self acts ~keep:true lits
let[@inline] add_clause_permanent self acts lits (proof:P.t) : unit =
add_sat_clause_ self acts ~keep:true lits proof
let add_lit _self acts lit : unit = acts.Msat.acts_mk_lit lit
let add_lit_t self acts ?sign t = add_lit self acts (mk_lit self acts ?sign t)
let add_lit_t self acts ?sign t =
let lit = mk_lit self acts ?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_partial_check self f = self.on_partial_check <- f :: self.on_partial_check
@ -475,24 +547,29 @@ module Make(A : ARG)
| Lemma l -> Fmt.fprintf out "(@[lemma@ %a@])" P.pp l
| Duplicate (c, _) ->
let n = find_idx_of_proof_ c in
Fmt.fprintf out "(@[dedup@ %d@])" n
Fmt.fprintf out "(@[dedup@ c%d@])" n
| Hyper_res { hr_init=init; hr_steps=steps } ->
let n_init = find_idx_of_proof_ init in
let pp_step out (pivot,p') =
let unit_res =
Array.length (SC.atoms (conclusion p')) = 1 in
let n_p' = find_idx_of_proof_ p' in
Fmt.fprintf out "(@[%d@ :pivot %a@])" n_p' pp_atom pivot
if unit_res then (
Fmt.fprintf out "(@[r1 c%d@])" n_p'
) else (
Fmt.fprintf out "(@[r c%d@ :pivot %a@])" n_p' pp_atom pivot
)
in
Fmt.fprintf out "(@[hres@ %d@ (@[%a@])@])"
n_init Fmt.(list ~sep:(return "@ ") pp_step) steps
in
Fmt.fprintf out "(@[step %d@ (@[cl %a@])@ (@[<1>src@ %a@])@])@ "
Fmt.fprintf out "(@[defc c%d@ (@[cl %a@])@ (@[<1>src@ %a@])@])@ "
idx Fmt.(list ~sep:(return "@ ") pp_atom) atoms
pp_step step;
)
in
Fmt.fprintf out "(@[<v>proof@ ";
Fmt.fprintf out "(@[<v>quip 1@ ";
Sat_solver.Proof.fold pp_node () self;
Fmt.fprintf out "@])@.";
()
@ -564,7 +641,7 @@ module Make(A : ARG)
let tst = Solver_internal.tst self.si in
Sat_solver.assume self.solver [
[Lit.atom tst @@ Term.bool tst true];
] P.default;
] P.true_is_true
end;
self
@ -600,17 +677,17 @@ module Make(A : ARG)
())
let rec mk_atom_lit self lit : Atom.t =
let lit = preprocess_lit_ self lit in
let lit, _proof = preprocess_lit_ self lit in
add_bool_subterms_ self (Lit.term lit);
Sat_solver.make_atom self.solver lit
and preprocess_lit_ self lit : Lit.t =
and preprocess_lit_ self lit : Lit.t * P.t =
Solver_internal.preprocess_lit_
~add_clause:(fun lits ->
~add_clause:(fun lits proof ->
(* recursively add these sub-literals, so they're also properly processed *)
Stat.incr self.si.count_preprocess_clause;
let atoms = List.map (mk_atom_lit self) lits in
Sat_solver.add_clause self.solver atoms P.default)
Sat_solver.add_clause self.solver atoms proof)
self.si lit
let[@inline] mk_atom_t self ?sign t : Atom.t =
@ -667,11 +744,12 @@ module Make(A : ARG)
let pp_stats out (self:t) : unit =
Stat.pp_all out (Stat.all @@ stats self)
let add_clause (self:t) (c:Atom.t IArray.t) : unit =
let add_clause (self:t) (c:Atom.t IArray.t) (proof:P.t) : unit =
Stat.incr self.count_clause;
Log.debugf 50 (fun k->k "(@[solver.add-clause@ %a@])" (Util.pp_iarray Atom.pp) c);
Log.debugf 50 (fun k->k "(@[solver.add-clause@ %a@ :proof %a@])"
(Util.pp_iarray Atom.pp) c P.pp proof);
let pb = Profile.begin_ "add-clause" in
Sat_solver.add_clause_a self.solver (c:> Atom.t array) P.default;
Sat_solver.add_clause_a self.solver (c:> Atom.t array) proof;
Profile.exit pb
let add_clause_l self c = add_clause self (IArray.of_list c)

2
src/smtlib/Process.ml
View file

@ -271,7 +271,7 @@ let process_stmt
);
let atom = Solver.mk_atom_t solver t in
CCOpt.iter (fun h -> Vec.push h [atom]) hyps;
Solver.add_clause solver (IArray.singleton atom);
Solver.add_clause solver (IArray.singleton atom) (Proof.assertion t);
E.return()
| Statement.Stmt_assert_clause c ->
if pp_cnf then (

20
src/smtlib/Proof.ml
View file

@ -4,14 +4,26 @@ type term = T.t
type t =
| Unspecified
| Sorry of term
| CC_lemma_imply of t list * term * term
| CC_lemma of (term * bool) list
| Assertion of term
let default=Unspecified
let sorry t = Sorry t
let make_cc iter : t = CC_lemma (Iter.to_rev_list iter)
let pp out = function
| Unspecified -> Fmt.string out "<unspecified>"
| CC_lemma l ->
let pp_lit out (t,b) =
let assertion t = Assertion t
let rec pp out (self:t) : unit =
let pp_signed_t_ out (t,b) =
if b then T.pp out t else Fmt.fprintf out "(@[not@ %a@])" T.pp t
in
match self with
| Unspecified -> Fmt.string out "<unspecified>"
| CC_lemma_imply (l,t,u) ->
Fmt.fprintf out "(@[cc-lemma@ (@[%a@])@])"
| CC_lemma l ->
Fmt.fprintf out "(@[cc-lemma@ (@[%a@])@])"
Fmt.(list ~sep:(return "@ ") pp_lit) l

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

@ -27,6 +27,15 @@ module type ARG = sig
val view_as_bool : term -> (term, term Iter.t) bool_view
(** Project the term into the boolean view. *)
(** [proof_ite_true (ite a b c)] is [a=true |- ite a b c = b] *)
val proof_ite_true : S.T.Term.t -> S.P.t
(** [proof_ite_false (ite a b c)] is [a=false |- ite a b c = c] *)
val proof_ite_false : S.T.Term.t -> S.P.t
(** By basic boolean logic to prove [a=b] *)
val proof_bool : S.T.Term.t -> S.T.Term.t -> S.P.t
val mk_bool : S.T.Term.state -> (term, term IArray.t) bool_view -> term
(** Make a term from the given boolean view. *)
@ -86,13 +95,12 @@ module Make(A : ARG) : S with module A = A = struct
type state = {
tst: T.state;
ty_st: Ty.state;
simps: T.t T.Tbl.t; (* cache *)
cnf: Lit.t T.Tbl.t; (* tseitin CNF *)
cnf: (Lit.t * SI.P.t) T.Tbl.t; (* tseitin CNF *)
gensym: A.Gensym.t;
}
let create tst ty_st : state =
{ tst; ty_st; simps=T.Tbl.create 128;
{ tst; ty_st;
cnf=T.Tbl.create 128;
gensym=A.Gensym.create tst;
}
@ -107,47 +115,52 @@ 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 option =
let simplify (self:state) (simp:SI.Simplify.t) (t:T.t) : (T.t * SI.P.t) option =
let tst = self.tst in
let ret u = Some (u, A.proof_bool t u) in
match A.view_as_bool t with
| B_bool _ -> None
| B_not u when is_true u -> Some (T.bool tst false)
| B_not u when is_false u -> Some (T.bool tst true)
| B_not u when is_true u -> ret (T.bool tst false)
| B_not u when is_false u -> ret (T.bool tst true)
| B_not _ -> None
| B_opaque_bool _ -> None
| B_and a ->
if Iter.exists is_false a then Some (T.bool tst false)
else if Iter.for_all is_true a then Some (T.bool tst true)
if Iter.exists is_false a then ret (T.bool tst false)
else if Iter.for_all is_true a then ret (T.bool tst true)
else None
| B_or a ->
if Iter.exists is_true a then Some (T.bool tst true)
else if Iter.for_all is_false a then Some (T.bool tst false)
if Iter.exists is_true a then ret (T.bool tst true)
else if Iter.for_all is_false a then ret (T.bool tst false)
else None
| B_imply (args, u) ->
if Iter.exists is_false args then Some (T.bool tst true)
else if is_true u then Some (T.bool tst true)
if Iter.exists is_false args then ret (T.bool tst true)
else if is_true u then ret (T.bool tst true)
else None
| B_ite (a,b,c) ->
(* directly simplify [a] so that maybe we never will simplify one
of the branches *)
let a = SI.Simplify.normalize simp a in
let a, pr_a = SI.Simplify.normalize_t simp a in
begin match A.view_as_bool a with
| B_bool true -> Some b
| B_bool false -> Some c
| B_bool true ->
let pr = SI.P.(hres_l (A.proof_ite_true t) [R1, pr_a]) in
Some (b, pr)
| B_bool false ->
let pr = SI.P.(hres_l (A.proof_ite_false t) [R1, pr_a]) in
Some (c, pr)
| _ ->
None
end
| B_equiv (a,b) when is_true a -> Some b
| B_equiv (a,b) when is_false a -> Some (not_ tst b)
| B_equiv (a,b) when is_true b -> Some a
| B_equiv (a,b) when is_false b -> Some (not_ tst a)
| B_xor (a,b) when is_false a -> Some b
| B_xor (a,b) when is_true a -> Some (not_ tst b)
| B_xor (a,b) when is_false b -> Some a
| B_xor (a,b) when is_true b -> Some (not_ tst a)
| B_equiv (a,b) when is_true a -> ret b
| B_equiv (a,b) when is_false a -> ret (not_ tst b)
| B_equiv (a,b) when is_true b -> ret a
| B_equiv (a,b) when is_false b -> ret (not_ tst a)
| B_xor (a,b) when is_false a -> ret b
| B_xor (a,b) when is_true a -> ret (not_ tst b)
| B_xor (a,b) when is_false b -> ret a
| B_xor (a,b) when is_true b -> ret (not_ tst a)
| B_equiv _ | B_xor _ -> None
| B_eq (a,b) when T.equal a b -> Some (T.bool tst true)
| B_neq (a,b) when T.equal a b -> Some (T.bool tst true)
| B_eq (a,b) when T.equal a b -> ret (T.bool tst true)
| B_neq (a,b) when T.equal a b -> ret (T.bool tst true)
| B_eq _ | B_neq _ -> None
| B_atom _ -> None
@ -164,76 +177,101 @@ module Make(A : ARG) : S with module A = A = struct
mk_lit proxy
(* preprocess "ite" away *)
let preproc_ite self si ~mk_lit ~add_clause (t:T.t) : T.t option =
let preproc_ite self si ~mk_lit ~add_clause (t:T.t) : (T.t * SI.P.t) option =
match A.view_as_bool t with
| B_ite (a,b,c) ->
let a = SI.simp_t si a in
let a, pr_a = SI.simp_t si a in
begin match A.view_as_bool a with
| B_bool true -> Some b
| B_bool false -> Some c
| B_bool true ->
(* [a=true |- ite a b c=b], [|- a=true] ==> [|- t=b] *)
let proof = SI.P.(hres_l (A.proof_ite_true t) [P1, pr_a]) in
Some (b, proof)
| B_bool false ->
(* [a=false |- ite a b c=c], [|- a=false] ==> [|- t=c] *)
let proof = SI.P.(hres_l (A.proof_ite_false t) [P1, pr_a]) in
Some (c, proof)
| _ ->
let t_ite = fresh_term self ~for_:t ~pre:"ite" (T.ty b) in
let lit_a = mk_lit a in
add_clause [Lit.neg lit_a; mk_lit (eq self.tst t_ite b)];
add_clause [lit_a; mk_lit (eq self.tst t_ite c)];
Some t_ite
let pr = SI.P.sorry in (* FIXME: proper proof by-def(t_ite) + bool *)
add_clause [Lit.neg lit_a; mk_lit (eq self.tst t_ite b)] pr;
add_clause [lit_a; mk_lit (eq self.tst t_ite c)] pr;
(* TODO: by def t_ite + ite-true + ite-false
+ case split [a=true \/ a=false] *)
Some (t_ite, SI.P.sorry)
end
| _ -> None
(* TODO: polarity? *)
let cnf (self:state) (_si:SI.t) ~mk_lit ~add_clause (t:T.t) : T.t option =
let rec get_lit (t:T.t) : Lit.t =
let cnf (self:state) (_si:SI.t) ~mk_lit ~add_clause (t:T.t) : (T.t * SI.P.t) option =
let rec get_lit_and_proof_ (t:T.t) : Lit.t * SI.P.t =
let t_abs, t_sign = T.abs self.tst t in
let lit =
let lit_abs, pr =
match T.Tbl.find self.cnf t_abs with
| lit -> lit (* cached *)
| lit_pr -> lit_pr (* cached *)
| exception Not_found ->
(* compute and cache *)
let lit = get_lit_uncached t_abs in
let lit, pr = get_lit_uncached t_abs in
if not (T.equal (Lit.term lit) t_abs) then (
T.Tbl.add self.cnf t_abs lit;
T.Tbl.add self.cnf t_abs (lit, pr);
Log.debugf 20
(fun k->k "(@[sidekick.bool.add-lit@ :lit %a@ :for-t %a@])"
Lit.pp lit T.pp t_abs);
);
lit
lit, pr
in
if t_sign then lit else Lit.neg lit
and equiv_ ~is_xor ~for_ a b : Lit.t =
let lit = if t_sign then lit_abs else Lit.neg lit_abs in
lit, pr
and equiv_ ~get_lit ~is_xor ~for_ a b : Lit.t =
let a = get_lit a in
let b = get_lit b in
let a = if is_xor then Lit.neg a else a in (* [a xor b] is [(¬a) = b] *)
let proxy = fresh_lit ~for_ ~mk_lit ~pre:"equiv_" self in
(* proxy => a<=> b,
¬proxy => a xor b *)
add_clause [Lit.neg proxy; Lit.neg a; b];
add_clause [Lit.neg proxy; Lit.neg b; a];
add_clause [proxy; a; b];
add_clause [proxy; Lit.neg a; Lit.neg b];
let proof = SI.P.sorry in (* FIXME: by_def(proxy) + bool *)
add_clause [Lit.neg proxy; Lit.neg a; b] proof;
add_clause [Lit.neg proxy; Lit.neg b; a] proof;
add_clause [proxy; a; b] proof;
add_clause [proxy; Lit.neg a; Lit.neg b] proof;
proxy
and get_lit_uncached t : Lit.t =
(* make a literal for [t], with a proof of [|- abs(t) = abs(lit)] *)
and get_lit_uncached t : Lit.t * SI.P.t =
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
match A.view_as_bool t with
| B_bool b -> mk_lit (T.bool self.tst b)
| B_opaque_bool t -> mk_lit t
| B_bool b -> mk_lit (T.bool self.tst b), SI.P.refl t
| B_opaque_bool t -> mk_lit t, SI.P.refl t
| B_not u ->
let lit = get_lit u in
Lit.neg lit
let lit, pr = get_lit_and_proof_ u in
Lit.neg lit, pr
| B_and l ->
let subs = l |> Iter.map get_lit |> Iter.to_list in
let proxy = fresh_lit ~for_:t ~mk_lit ~pre:"and_" self in
(* add clauses *)
List.iter (fun u -> add_clause [Lit.neg proxy; u]) subs;
add_clause (proxy :: List.map Lit.neg subs);
proxy
let proof = SI.P.sorry in (* FIXME: by_def(proxy) + bool *)
List.iter (fun u -> add_clause [Lit.neg proxy; u] proof) subs;
add_clause (proxy :: List.map Lit.neg subs) proof;
proxy, proof (* FIXME: use sub_p, by-def(proxy), A.proof_bool *)
| B_or l ->
let subs = l |> Iter.map get_lit |> Iter.to_list in
let proxy = fresh_lit ~for_:t ~mk_lit ~pre:"or_" self in
(* add clauses *)
List.iter (fun u -> add_clause [Lit.neg u; proxy]) subs;
add_clause (Lit.neg proxy :: subs);
proxy
let proof = SI.P.sorry in (* FIXME: by_def(proxy) + bool *)
List.iter (fun u -> add_clause [Lit.neg u; proxy] proof) subs;
add_clause (Lit.neg proxy :: subs) proof;
proxy, proof (* FIXME: use sub_p, by-def(proxy), A.proof_bool *)
| B_imply (args, u) ->
(* transform into [¬args \/ u] on the fly *)
let args = args |> Iter.map get_lit |> Iter.map Lit.neg |> Iter.to_list in
@ -242,19 +280,21 @@ module Make(A : ARG) : S with module A = A = struct
(* now the or-encoding *)
let proxy = fresh_lit ~for_:t ~mk_lit ~pre:"implies_" self in
(* add clauses *)
List.iter (fun u -> add_clause [Lit.neg u; proxy]) subs;
add_clause (Lit.neg proxy :: subs);
proxy
| B_ite _ | B_eq _ | B_neq _ -> mk_lit t
| B_equiv (a,b) -> equiv_ ~for_:t ~is_xor:false a b
| B_xor (a,b) -> equiv_ ~for_:t ~is_xor:true a b
| B_atom u -> mk_lit u
let proof = SI.P.sorry in (* FIXME: by_def(proxy) + bool *)
List.iter (fun u -> add_clause [Lit.neg u; proxy] proof) subs;
add_clause (Lit.neg proxy :: subs) proof;
proxy, proof (* FIXME: by_def(proxy) + sub_p + A.proof_bool *)
| B_ite _ | B_eq _ | B_neq _ -> mk_lit t, SI.P.refl t
| B_equiv (a,b) -> equiv_ ~get_lit ~for_:t ~is_xor:false a b, SI.P.sorry (* FIXME *)
| B_xor (a,b) -> equiv_ ~get_lit ~for_:t ~is_xor:true a b, SI.P.sorry (* FIXME *)
| B_atom u -> mk_lit u, SI.P.refl u
in
let lit = get_lit t in
let lit, pr = get_lit_and_proof_ 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
if T.equal u t then None else Some (u, pr)
(* check if new terms were added to the congruence closure, that can be turned
into clauses *)
@ -274,10 +314,10 @@ module Make(A : ARG) : S with module A = A = struct
all_terms
(fun t -> match cnf_of t with
| None -> ()
| Some u ->
| 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);
(fun k->k "(@[th-bool-static.final-check.cnf@ %a@ :yields %a@ :pr %a@])"
T.pp t T.pp u SI.P.pp pr_t_u);
SI.CC.merge_t cc_ t u (SI.CC.Expl.mk_list []);
());
end;

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

@ -24,6 +24,7 @@ let name = "th-data"
module type DATA_TY = sig
type t
type cstor
type proof
val equal : t -> t -> bool
@ -73,6 +74,10 @@ module type ARG = sig
val mk_eq : S.T.Term.state -> S.T.Term.t -> S.T.Term.t -> S.T.Term.t
val ty_is_finite : S.T.Ty.t -> bool
val ty_set_is_finite : S.T.Ty.t -> bool -> unit
val proof_isa_split : S.T.Term.t Iter.t -> S.P.t
val proof_isa_disj : S.T.Term.t -> S.T.Term.t -> S.P.t
val proof_cstor_inj : Cstor.t -> S.T.Term.t list -> S.T.Term.t list -> S.P.t
end
(** Helper to compute the cardinality of types *)
@ -565,11 +570,13 @@ module Make(A : ARG) : S with module A = A = struct
lit)
|> Iter.to_rev_list
in
SI.add_clause_permanent solver acts c;
SI.add_clause_permanent solver acts c
(A.proof_isa_split @@ (Iter.of_list c|>Iter.map SI.Lit.term));
Iter.diagonal_l c
(fun (c1,c2) ->
let proof = A.proof_isa_disj (SI.Lit.term c1) (SI.Lit.term c2) in
SI.add_clause_permanent solver acts
[SI.Lit.neg c1; SI.Lit.neg c2]);
[SI.Lit.neg c1; SI.Lit.neg c2] proof);
)
(* on final check, check acyclicity,