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

wip: refactor proofs for SMT

Browse source
This commit is contained in:
Simon Cruanes 2021-08-12 22:05:49 -04:00
parent 9975a471f7
commit 27e775ee04
13 changed files with 152 additions and 794 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

29
src/backend/Backend_intf.ml
View file

@ -1,29 +0,0 @@
(*
MSAT is free software, using the Apache license, see file LICENSE
Copyright 2014 Guillaume Bury
Copyright 2014 Simon Cruanes
*)
(** Backend interface
This modules defines the interface of the modules providing
export of proofs.
*)
module type S = sig
(** Proof exporting
Currently, exporting a proof means printing it into a file
according to the conventions of a given format.
*)
type store
type t
(** The type of proofs. *)
val pp : store -> Format.formatter -> t -> unit
(** A function for printing proofs in the desired format. *)
end

156
src/backend/Dot.ml
View file

@ -1,156 +0,0 @@
(*
MSAT is free software, using the Apache license, see file LICENSE
Copyright 2014 Guillaume Bury
Copyright 2014 Simon Cruanes
*)
(** Output interface for the backend *)
module type S = Backend_intf.S
(** Input module for the backend *)
module type Arg = sig
type atom
(* Type of atoms *)
type store
type hyp
type lemma
type assumption
(** Types for hypotheses, lemmas, and assumptions. *)
val print_atom : store -> Format.formatter -> atom -> unit
(** Printing function for atoms *)
val hyp_info : store -> hyp -> string * string option * (Format.formatter -> unit -> unit) list
val lemma_info : store -> lemma -> string * string option * (Format.formatter -> unit -> unit) list
val assumption_info : store -> assumption -> string * string option * (Format.formatter -> unit -> unit) list
(** Functions to return information about hypotheses and lemmas *)
end
module Default(S : Sidekick_sat.S) = struct
module Atom = S.Atom
module Clause = S.Clause
type store = S.solver
let print_atom = S.Atom.pp
let hyp_info store c =
"hypothesis", Some "LIGHTBLUE",
[ fun fmt () -> Format.fprintf fmt "%s" @@ S.Clause.short_name store c]
let lemma_info store c =
"lemma", Some "BLUE",
[ fun fmt () -> Format.fprintf fmt "%s" @@ S.Clause.short_name store c]
let assumption_info store c =
"assumption", Some "PURPLE",
[ fun fmt () -> Format.fprintf fmt "%s" @@ S.Clause.short_name store c]
end
(** Functor to provide dot printing *)
module Make(S : Sidekick_sat.S)(A : Arg with type atom := S.atom
and type hyp := S.clause
and type lemma := S.clause
and type store := S.store
and type assumption := S.clause) = struct
module Atom = S.Atom
module Clause = S.Clause
module P = S.Proof
let node_id store n = S.Clause.short_name store n.P.conclusion
let proof_id store p = node_id store (P.expand store p)
let res_nn_id store n1 n2 = node_id store n1 ^ "_" ^ node_id store n2 ^ "_res"
let res_np_id store n1 n2 = node_id store n1 ^ "_" ^ proof_id store n2 ^ "_res"
let print_clause store fmt c =
let v = S.Clause.atoms_a store c in
if Array.length v = 0 then
Format.fprintf fmt "⊥"
else
let n = Array.length v in
for i = 0 to n - 1 do
Format.fprintf fmt "%a" (A.print_atom store) v.(i);
if i < n - 1 then
Format.fprintf fmt ", "
done
let print_edge fmt i j =
Format.fprintf fmt "%s -> %s;@\n" j i
let print_edges store fmt n =
match P.(n.step) with
| P.Hyper_res {P.hr_steps=[];_} -> assert false (* NOTE: should never happen *)
| P.Hyper_res {P.hr_init; hr_steps=((_,p0)::_) as l} ->
print_edge fmt (res_np_id store n p0) (proof_id store hr_init);
List.iter
(fun (_,p2) -> print_edge fmt (res_np_id store n p2) (proof_id store p2))
l;
| _ -> ()
let table_options fmt color =
Format.fprintf fmt "BORDER=\"0\" CELLBORDER=\"1\" CELLSPACING=\"0\" BGCOLOR=\"%s\"" color
let table store fmt (c, rule, color, l) =
Format.fprintf fmt "<TR><TD colspan=\"2\">%a</TD></TR>" (print_clause store) c;
match l with
| [] ->
Format.fprintf fmt "<TR><TD BGCOLOR=\"%s\" colspan=\"2\">%s</TD></TR>" color rule
| f :: r ->
Format.fprintf fmt "<TR><TD BGCOLOR=\"%s\" rowspan=\"%d\">%s</TD><TD>%a</TD></TR>"
color (List.length l) rule f ();
List.iter (fun f -> Format.fprintf fmt "<TR><TD>%a</TD></TR>" f ()) r
let print_dot_node store fmt id color c rule rule_color l =
Format.fprintf fmt "%s [shape=plaintext, label=<<TABLE %a>%a</TABLE>>];@\n"
id table_options color (table store) (c, rule, rule_color, l)
let print_dot_res_node store fmt id a =
Format.fprintf fmt "%s [label=<%a>];@\n" id (A.print_atom store) a
let ttify f c = fun fmt () -> f fmt c
let print_contents store fmt n =
match P.(n.step) with
(* Leafs of the proof tree *)
| P.Hypothesis _ ->
let rule, color, l = A.hyp_info store P.(n.conclusion) in
let color = match color with None -> "LIGHTBLUE" | Some c -> c in
print_dot_node store fmt (node_id store n) "LIGHTBLUE" P.(n.conclusion) rule color l
| P.Assumption ->
let rule, color, l = A.assumption_info store P.(n.conclusion) in
let color = match color with None -> "LIGHTBLUE" | Some c -> c in
print_dot_node store fmt (node_id store n) "LIGHTBLUE" P.(n.conclusion) rule color l
| P.Lemma _ ->
let rule, color, l = A.lemma_info store P.(n.conclusion) in
let color = match color with None -> "YELLOW" | Some c -> c in
print_dot_node store fmt (node_id store n) "LIGHTBLUE" P.(n.conclusion) rule color l
(* Tree nodes *)
| P.Duplicate (p, l) ->
print_dot_node store fmt (node_id store n) "GREY" P.(n.conclusion) "Duplicate" "GREY"
((fun fmt () -> (Format.fprintf fmt "%s" (node_id store n))) ::
List.map (ttify @@ A.print_atom store) l);
print_edge fmt (node_id store n) (node_id store (P.expand store p))
| P.Hyper_res {P.hr_steps=l; _} ->
print_dot_node store fmt (node_id store n) "GREY" P.(n.conclusion) "Resolution" "GREY"
[(fun fmt () -> (Format.fprintf fmt "%s" (node_id store n)))];
List.iter
(fun (a,p2) ->
print_dot_res_node store fmt (res_np_id store n p2) a;
print_edge fmt (node_id store n) (res_np_id store n p2))
l
let print_node store fmt n =
print_contents store fmt n;
print_edges store fmt n
let pp store fmt p =
Format.fprintf fmt "digraph proof {@\n";
P.fold store (fun () -> print_node store fmt) () p;
Format.fprintf fmt "}@."
end

67
src/backend/Dot.mli
View file

@ -1,67 +0,0 @@
(*
MSAT is free software, using the Apache license, see file LICENSE
Copyright 2014 Guillaume Bury
Copyright 2014 Simon Cruanes
*)
(** Dot backend for proofs
This module provides functions to export proofs into the dot graph format.
Graphs in dot format can be used to generates images using the graphviz tool.
*)
module type S = Backend_intf.S
(** Interface for exporting proofs. *)
module type Arg = sig
(** Term printing for DOT
This module defines what functions are required in order to export
a proof to the DOT format.
*)
type atom
(** The type of atomic formuals *)
type hyp
type lemma
type assumption
(** The type of theory-specifi proofs (also called lemmas). *)
type store
val print_atom : store -> Format.formatter -> atom -> unit
(** Print the contents of the given atomic formulas.
WARNING: this function should take care to escape and/or not output special
reserved characters for the dot format (such as quotes and so on). *)
val hyp_info : store -> hyp -> string * string option * (Format.formatter -> unit -> unit) list
val lemma_info : store -> lemma -> string * string option * (Format.formatter -> unit -> unit) list
val assumption_info : store -> assumption -> string * string option * (Format.formatter -> unit -> unit) list
(** Generate some information about the leafs of the proof tree. Currently this backend
print each lemma/assumption/hypothesis as a single leaf of the proof tree.
These function should return a triplet [(rule, color, l)], such that:
- [rule] is a name for the proof (arbitrary, does not need to be unique, but
should rather be descriptive)
- [color] is a color name (optional) understood by DOT
- [l] is a list of printers that will be called to print some additional information
*)
end
module Default(S : Sidekick_sat.S) : Arg with type atom := S.atom
and type hyp := S.clause
and type lemma := S.clause
and type store := S.store
and type assumption := S.clause
(** Provides a reasonnable default to instantiate the [Make] functor, assuming
the original printing functions are compatible with DOT html labels. *)
module Make(S : Sidekick_sat.S)
(A : Arg with type atom := S.atom
and type hyp := S.clause
and type lemma := S.clause
and type store := S.store
and type assumption := S.clause)
: S with type t := S.Proof.t and type store := S.store
(** Functor for making a module to export proofs to the DOT format. *)

7
src/backend/dune
View file

@ -1,7 +0,0 @@
(library
(name sidekick_backend)
(public_name sidekick.backend)
(synopsis "Proof backends for sidekick")
(flags :standard -warn-error -a+8)
(libraries sidekick.sat))

47
src/cc/Sidekick_cc.ml
View file

@ -15,18 +15,18 @@ module type S = Sidekick_core.CC_S
module Make (A: CC_ARG)
: S with module T = A.T
and module Lit = A.Lit
and module P = A.P
and type lemma = A.lemma
and module Actions = A.Actions
= struct
module T = A.T
module P = A.P
module Lit = A.Lit
module Actions = A.Actions
module P = Actions.P
type term = T.Term.t
type term_store = T.Term.store
type lit = Lit.t
type fun_ = T.Fun.t
type proof = P.t
type lemma = A.lemma
type actions = Actions.t
module Term = T.Term
@ -95,7 +95,6 @@ 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
@ -169,7 +168,6 @@ 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_debug ~sharing:false) p
| E_and (a,b) ->
Format.fprintf out "(@[<hv1>and@ %a@ %a@])" pp a pp b
@ -179,7 +177,6 @@ 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
@ -283,7 +280,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 * P.t) -> unit
and ev_on_propagate = t -> lit -> (unit -> lit list * P.lemma) -> unit
and ev_on_is_subterm = N.t -> term -> unit
let[@inline] size_ (r:repr) = r.n_size
@ -310,16 +307,8 @@ module Make (A: CC_ARG)
Invariant: [in_cc t ∧ do_cc t => forall u subterm t, in_cc u] *)
let[@inline] mem (cc:t) (t:term): bool = T_tbl.mem cc.tbl t
let ret_cc_lemma _what _lits p_lits =
let p = P.cc_lemma p_lits in
(* useful to debug bad lemmas
let n_pos = Iter.of_list p_lits |> Iter.filter P.lit_sign |> Iter.length in
if n_pos <> 1 then (
Log.debugf 0 (fun k->k"emit (n-pos=%d) :from %s@ %a@ :lits %a"
n_pos what
(P.pp_debug ~sharing:false) p Fmt.(Dump.list Lit.pp) lits);
);
*)
let ret_cc_lemma _what (_lits:lit list) (p_lits:lit Iter.t) =
let p = P.lemma_cc p_lits in
p
(* print full state *)
@ -473,9 +462,6 @@ module Make (A: CC_ARG)
| E_lit lit -> lit :: acc
| E_theory e' ->
th := true; explain_decompose_expl 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_equal cc ~th acc a b
| E_merge_t (a,b) ->
(* find nodes for [a] and [b] on the fly *)
@ -676,14 +662,8 @@ module Make (A: CC_ARG)
let lits = explain_equal cc ~th lits a ra in
let lits = explain_equal cc ~th lits b rb in
let proof =
let p_lits =
lits
|> List.rev_map (fun lit ->
let t, sign = Lit.signed_term lit in
P.lit_mk (not sign) t)
in
ret_cc_lemma "true-eq-false" lits p_lits
in
let p_lits = Iter.of_list lits |> Iter.map Lit.neg in
ret_cc_lemma "true-eq-false" lits p_lits in
raise_conflict_ cc ~th:!th acts (List.rev_map Lit.neg lits) proof
);
(* We will merge [r_from] into [r_into].
@ -801,10 +781,7 @@ module Make (A: CC_ARG)
let lits = explain_equal cc ~th acc u1 t1 in
let p_lits =
(* make a tautology, not a true guard *)
let tauto = lit :: List.rev_map Lit.neg lits in
tauto |> List.rev_map (fun lit ->
let t, sign = Lit.signed_term lit in
A.P.(lit_mk sign t))
Iter.cons lit (Iter.of_list lits |> Iter.map Lit.neg)
in
let p = ret_cc_lemma "bool-parent" lits p_lits in
lits, p
@ -875,11 +852,7 @@ module Make (A: CC_ARG)
let lits = explain_decompose_expl cc ~th [] expl in
let lits = List.rev_map Lit.neg lits in
let proof =
let p_lits =
lits |> List.rev_map (fun lit ->
let t, sign = Lit.signed_term lit in
P.lit_mk sign t)
in
let p_lits = Iter.of_list lits in
ret_cc_lemma "from-expl" lits p_lits
in
raise_conflict_ cc ~th:!th acts lits proof

4
src/cc/Sidekick_cc.mli
View file

@ -4,7 +4,7 @@ open Sidekick_core
module type S = Sidekick_core.CC_S
module Make (A: CC_ARG)
: S with module T = A.T
: S with module T = A.T
and module Lit = A.Lit
and module P = A.P
and type lemma = A.lemma
and module Actions = A.Actions

153
src/core/Sidekick_core.ml
View file

@ -145,89 +145,37 @@ module type TERM = sig
end
end
(** Proofs of unsatisfiability *)
(** Proofs for the congruence closure *)
module type CC_PROOF = sig
type lit
type lemma
val lemma_cc : lit Iter.t -> lemma
end
(* TODO: use same proofs as Sidekick_sat?
but give more precise type to [lemma]? *)
(** Proofs of unsatisfiability.
We use DRUP(T)-style traces where we simply emit clauses as we go,
annotating enough for the checker to reconstruct them.
This allows for low overhead proof production. *)
module type PROOF = sig
type t
(** The abstract representation of a proof. A proof always proves
a clause to be {b valid} (true in every possible interpretation
of the problem's assertions, and the theories) *)
type term
type ty
type hres_step
(** hyper-resolution steps: resolution, unit resolution;
bool paramodulation, unit bool paramodulation *)
val r : t -> pivot:term -> hres_step
(** Resolution step on given pivot term *)
val r1 : t -> hres_step
(** Unit resolution; pivot is obvious *)
val p : t -> lhs:term -> rhs:term -> hres_step
(** Paramodulation using proof whose conclusion has a literal [lhs=rhs] *)
val p1 : t -> hres_step
(** Unit paramodulation *)
type lemma
type lit
(** Proof representation of literals *)
val pp_lit : lit Fmt.printer
val lit_a : term -> lit
val lit_na : term -> lit
val lit_mk : bool -> term -> lit
val lit_eq : term -> term -> lit
val lit_neq : term -> term -> lit
val lit_not : lit -> lit
val lit_sign : lit -> bool
include CC_PROOF
with type lemma := lemma
and type lit := lit
type composite_step
val stepc : name:string -> lit list -> t -> composite_step
val deft : term -> term -> composite_step (** define a (new) atomic term *)
val is_trivial_refl : t -> bool
(** is this a proof of [|- t=t]? This can be used to remove
some trivial steps that would build on the proof (e.g. rewriting
using [refl t] is useless). *)
val assertion : term -> t
val assertion_c : lit Iter.t -> t
val ref_by_name : string -> t (* named clause, see {!defc} *)
val assertion_c_l : lit list -> t
val drup_res : lit list -> t (* assert clause and let DRUP take care of it *)
val hres_iter : t -> hres_step Iter.t -> t (* hyper-res *)
val hres_l : t -> hres_step list -> t (* hyper-res *)
val res : pivot:term -> t -> t -> t (* resolution with pivot *)
val res1 : t -> t -> t (* unit resolution *)
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 nn : t -> t (* negation normalization *)
val cc_lemma : lit list -> 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 composite_iter : ?assms:(string * lit) list -> composite_step Iter.t -> t
val composite_l : ?assms:(string * lit) list -> composite_step list -> t
val sorry : t [@@alert cstor "sorry used"] (* proof hole when we don't know how to produce a proof *)
val sorry_c : lit Iter.t -> t
[@@alert cstor "sorry used"] (* proof hole when we don't know how to produce a proof *)
val sorry_c_l : lit list -> t
val default : t [@@alert cstor "do not use default constructor"]
val pp_debug : sharing:bool -> t Fmt.printer
(** Pretty print a proof.
@param sharing if true, try to compact the proof by introducing
definitions for common terms, clauses, and steps as needed. Safe to ignore. *)
module Quip : sig
val output : out_channel -> t -> unit
(** Printer in Quip format (experimental) *)
end
val enabled : t -> bool
end
(** Literals
@ -274,20 +222,21 @@ module type CC_ACTIONS = sig
module T : TERM
module Lit : LIT with module T = T
module P : PROOF with type term = T.Term.t
type lemma
module P : CC_PROOF with type lit = Lit.t and type lemma = lemma
type t
(** An action handle. It is used by the congruence closure
to perform the actions below. How it performs the actions
is not specified and is solver-specific. *)
val raise_conflict : t -> Lit.t list -> P.t -> 'a
val raise_conflict : t -> Lit.t list -> lemma -> 'a
(** [raise_conflict acts c pr] declares that [c] is a tautology of
the theory of congruence. This does not return (it should raise an
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 * lemma) -> unit
(** [propagate acts lit ~reason pr] declares that [reason() => lit]
is a tautology.
@ -301,15 +250,19 @@ end
(** Arguments to a congruence closure's implementation *)
module type CC_ARG = sig
module T : TERM
module P : PROOF with type term = T.Term.t
module Lit : LIT with module T = T
module Actions : CC_ACTIONS with module T=T and module P = P and module Lit = Lit
type lemma
module P : CC_PROOF with type lit = Lit.t and type lemma = lemma
module Actions : CC_ACTIONS
with module T=T
and module Lit = Lit
and type lemma = lemma
val cc_view : T.Term.t -> (T.Fun.t, T.Term.t, T.Term.t Iter.t) CC_view.t
(** View the term through the lens of the congruence closure *)
end
(** Main congruence closure.
(** Main congruence closure signature.
The congruence closure handles the theory QF_UF (uninterpreted
function symbols).
@ -329,14 +282,17 @@ module type CC_S = sig
(** first, some aliases. *)
module T : TERM
module P : PROOF with type term = T.Term.t
module Lit : LIT with module T = T
module Actions : CC_ACTIONS with module T = T and module Lit = Lit and module P = P
type lemma
module P : CC_PROOF with type lit = Lit.t and type lemma = lemma
module Actions : CC_ACTIONS
with module T = T
and module Lit = Lit
and type lemma = lemma
type term_store = T.Term.store
type term = T.Term.t
type fun_ = T.Fun.t
type lit = Lit.t
type proof = P.t
type actions = Actions.t
type t
@ -421,7 +377,6 @@ 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
@ -474,7 +429,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 * P.t) -> unit
type ev_on_propagate = t -> lit -> (unit -> lit list * P.lemma) -> unit
(** [ev_on_propagate cc lit reason] is called whenever [reason() => lit]
is a propagated lemma. See {!CC_ACTIONS.propagate}. *)
@ -620,12 +575,22 @@ end
new lemmas, propagate literals, access the congruence closure, etc. *)
module type SOLVER_INTERNAL = sig
module T : TERM
module P : PROOF with type term = T.Term.t
type ty = T.Ty.t
type term = T.Term.t
type term_store = T.Term.store
type ty_store = T.Ty.store
(** {3 Literals}
A literal is a (preprocessed) term along with its sign.
It is directly manipulated by the SAT solver.
*)
module Lit : LIT with module T = T
(** {3 Proofs} *)
type lemma
module P : PROOF with type lit = Lit.t and type lemma = lemma
type proof = P.t
(** {3 Main type for a solver} *)
@ -641,13 +606,6 @@ module type SOLVER_INTERNAL = sig
type actions
(** Handle that the theories can use to perform actions. *)
(** {3 Literals}
A literal is a (preprocessed) term along with its sign.
It is directly manipulated by the SAT solver.
*)
module Lit : LIT with module T = T
type lit = Lit.t
(** {3 Proof helpers} *)
@ -662,8 +620,10 @@ module type SOLVER_INTERNAL = sig
(** Congruence closure instance *)
module CC : CC_S
with module T = T
and module P = P
and module Lit = Lit
and type lemma = lemma
and type P.lemma = lemma
and type P.lit = lit
and type Actions.t = actions
val cc : t -> CC.t
@ -872,15 +832,16 @@ end
Theory implementors will mostly interact with {!SOLVER_INTERNAL}. *)
module type SOLVER = sig
module T : TERM
module P : PROOF with type term = T.Term.t
module Lit : LIT with module T = T
type lemma
module P : PROOF with type lit = Lit.t and type lemma = lemma
module Solver_internal
: SOLVER_INTERNAL
with module T = T
and module P = P
and module Lit = Lit
and type lemma = lemma
and module P = P
(** Internal solver, available to theories. *)
type t

2
src/msat-solver/dune
View file

@ -2,5 +2,5 @@
(name Sidekick_msat_solver)
(public_name sidekick.msat-solver)
(libraries containers iter sidekick.core sidekick.util
sidekick.cc sidekick.sat sidekick.backend)
sidekick.cc sidekick.sat)
(flags :standard -open Sidekick_util))

283
src/sat/Solver.ml
View file

@ -34,10 +34,12 @@ end
module Make(Plugin : PLUGIN)
= struct
module Formula = Plugin.Formula
module Proof = Plugin.Proof
type formula = Formula.t
type theory = Plugin.t
type lemma = Plugin.proof
type lemma = Plugin.lemma
type proof = Plugin.proof
(* ### types ### *)
@ -511,279 +513,6 @@ module Make(Plugin : PLUGIN)
module Var = Store.Var
module Clause = Store.Clause
(* TODO: mostly, move into a functor outside that works on integers *)
module Proof = struct
exception Resolution_error of string
type atom = Atom.t
type clause = Clause.t
type formula = Formula.t
type lemma = Plugin.proof
type nonrec store = store
let error_res_f msg = Format.kasprintf (fun s -> raise (Resolution_error s)) msg
let[@inline] clear_var_of_ store (a:atom) = Store.clear_var store (Atom.var a)
(* Compute resolution of 2 clauses.
returns [pivots, resulting_atoms] *)
let resolve store (c1:clause) (c2:clause) : atom list * atom list =
(* invariants: only atoms in [c2] are marked, and the pivot is
cleared when traversing [c1] *)
Clause.iter store c2 ~f:(Atom.mark store);
let pivots = ref [] in
let l =
Clause.fold store [] c1
~f:(fun l a ->
if Atom.marked store a then l
else if Atom.marked store (Atom.neg a) then (
pivots := (Atom.abs a) :: !pivots;
clear_var_of_ store a;
l
) else a::l)
in
let l =
Clause.fold store l c2
~f:(fun l a -> if Atom.marked store a then a::l else l)
in
Clause.iter store c2 ~f:(clear_var_of_ store);
!pivots, l
(* [find_dups c] returns a list of duplicate atoms, and the deduplicated list *)
let find_dups (store:store) (c:clause) : atom list * atom list =
let res =
Clause.fold store ([], []) c
~f:(fun (dups,l) a ->
if Atom.marked store a then (
a::dups, l
) else (
Atom.mark store a;
dups, a::l
))
in
Clause.iter store c ~f:(clear_var_of_ store);
res
(* do [c1] and [c2] have the same lits, modulo reordering and duplicates? *)
let same_lits store (c1:atom Iter.t) (c2:atom Iter.t): bool =
let subset a b =
Iter.iter (Atom.mark store) b;
let res = Iter.for_all (Atom.marked store) a in
Iter.iter (clear_var_of_ store) b;
res
in
subset c1 c2 && subset c2 c1
let prove (store:store) conclusion =
match Clause.premise store conclusion with
| History [] -> assert false
| Empty_premise -> raise Solver_intf.No_proof
| _ -> conclusion
let rec set_atom_proof store a =
let aux acc b =
if Atom.equal (Atom.neg a) b then acc
else set_atom_proof store b :: acc
in
assert (Var.level store (Atom.var a) >= 0);
match Var.reason store (Atom.var a) with
| Some (Bcp c | Bcp_lazy (lazy c)) ->
Log.debugf 5 (fun k->k "(@[proof.analyze.clause@ :atom %a@ :c %a@])"
(Atom.debug store) a (Clause.debug store) c);
if Clause.n_atoms store c = 1 then (
Log.debugf 5 (fun k -> k "(@[proof.analyze.old-reason@ %a@])"
(Atom.debug store) a);
c
) else (
assert (Atom.is_false store a);
let r = History (c :: (Clause.fold store [] c ~f:aux)) in
let c' = Clause.make_l store ~removable:false [Atom.neg a] r in
Var.set_reason store (Atom.var a) (Some (Bcp c'));
Log.debugf 5
(fun k -> k "(@[proof.analyze.new-reason@ :atom %a@ :c %a@])"
(Atom.debug store) a (Clause.debug store) c');
c'
)
| _ ->
error_res_f "cannot prove atom %a" (Atom.debug store) a
let prove_unsat store conflict =
if Clause.n_atoms store conflict = 0 then (
conflict
) else (
Log.debugf 1 (fun k -> k "(@[sat.prove-unsat@ :from %a@])" (Clause.debug store) conflict);
let l = Clause.fold store [] conflict
~f:(fun acc a -> set_atom_proof store a :: acc) in
let res = Clause.make_l store ~removable:false [] (History (conflict :: l)) in
Log.debugf 1 (fun k -> k "(@[sat.proof-found@ %a@])" (Clause.debug store) res);
res
)
let prove_atom self a =
if Atom.is_true self a &&
Var.level self (Atom.var a) = 0 then
Some (set_atom_proof self a)
else
None
type t = clause
and proof_node = {
conclusion : clause;
step : step;
}
and step =
| Hypothesis of lemma
| Assumption
| Lemma of lemma
| Duplicate of t * atom list
| Hyper_res of hyper_res_step
and hyper_res_step = {
hr_init: t;
hr_steps: (atom * t) list; (* list of pivot+clause to resolve against [init] *)
}
let[@inline] conclusion (p:t) : clause = p
(* find pivots for resolving [l] with [init], and also return
the atoms of the conclusion *)
let find_pivots store (init:clause) (l:clause list) : _ * (atom * t) list =
Log.debugf 15
(fun k->k "(@[proof.find-pivots@ :init %a@ :l %a@])"
(Clause.debug store) init (Format.pp_print_list (Clause.debug store)) l);
Clause.iter store init ~f:(Atom.mark store);
let steps =
List.map
(fun c ->
let pivot =
match
Clause.atoms_iter store c
|> Iter.filter (fun a -> Atom.marked store (Atom.neg a))
|> Iter.to_list
with
| [a] -> a
| [] ->
error_res_f "(@[proof.expand.pivot_missing@ %a@])" (Clause.debug store) c
| pivots ->
error_res_f "(@[proof.expand.multiple_pivots@ %a@ :pivots %a@])"
(Clause.debug store) c (Atom.debug_l store) pivots
in
Clause.iter store c ~f:(Atom.mark store); (* add atoms to result *)
clear_var_of_ store pivot;
Atom.abs pivot, c)
l
in
(* cleanup *)
let res = ref [] in
let cleanup_a_ a =
if Atom.marked store a then (
res := a :: !res;
clear_var_of_ store a
)
in
Clause.iter store init ~f:cleanup_a_;
List.iter (fun c -> Clause.iter store c ~f:cleanup_a_) l;
!res, steps
let expand store conclusion =
Log.debugf 5 (fun k -> k "(@[sat.proof.expand@ @[%a@]@])" (Clause.debug store) conclusion);
match Clause.premise store conclusion with
| Lemma l ->
{ conclusion; step = Lemma l; }
| Local ->
{ conclusion; step = Assumption; }
| Hyp l ->
{ conclusion; step = Hypothesis l; }
| History [] ->
error_res_f "@[empty history for clause@ %a@]" (Clause.debug store) conclusion
| History [c] ->
let duplicates, res = find_dups store c in
assert (same_lits store (Iter.of_list res) (Clause.atoms_iter store conclusion));
{ conclusion; step = Duplicate (c, duplicates) }
| History (c :: r) ->
let res, steps = find_pivots store c r in
assert (same_lits store (Iter.of_list res) (Clause.atoms_iter store conclusion));
{ conclusion; step = Hyper_res {hr_init=c; hr_steps=steps}; }
| Empty_premise -> raise Solver_intf.No_proof
let rec res_of_hyper_res store (hr: hyper_res_step) : _ * _ * atom =
let {hr_init=c1; hr_steps=l} = hr in
match l with
| [] -> assert false
| [a, c2] -> c1, c2, a (* done *)
| (a,c2) :: steps' ->
(* resolve [c1] with [c2], then resolve that against [steps] *)
let pivots, l = resolve store c1 c2 in
assert (match pivots with [a'] -> Atom.equal a a' | _ -> false);
let c_1_2 = Clause.make_l store ~removable:true l (History [c1; c2]) in
res_of_hyper_res store {hr_init=c_1_2; hr_steps=steps'}
(* Proof nodes manipulation *)
let is_leaf = function
| Hypothesis _
| Assumption
| Lemma _ -> true
| Duplicate _
| Hyper_res _ -> false
let parents = function
| Hypothesis _
| Assumption
| Lemma _ -> []
| Duplicate (p, _) -> [p]
| Hyper_res {hr_init; hr_steps} -> hr_init :: List.map snd hr_steps
let expl = function
| Hypothesis _ -> "hypothesis"
| Assumption -> "assumption"
| Lemma _ -> "lemma"
| Duplicate _ -> "duplicate"
| Hyper_res _ -> "hyper-resolution"
module Tbl = Clause.Tbl
type task =
| Enter of t
| Leaving of t
let spop s = try Some (Stack.pop s) with Stack.Empty -> None
let rec fold_aux self s h f acc =
match spop s with
| None -> acc
| Some (Leaving c) ->
Tbl.add h c true;
fold_aux self s h f (f acc (expand self c))
| Some (Enter c) ->
if not (Tbl.mem h c) then begin
Stack.push (Leaving c) s;
let node = expand self c in
begin match node.step with
| Duplicate (p1, _) ->
Stack.push (Enter p1) s
| Hyper_res {hr_init=p1; hr_steps=l} ->
List.iter (fun (_,p2) -> Stack.push (Enter p2) s) l;
Stack.push (Enter p1) s;
| Hypothesis _ | Assumption | Lemma _ -> ()
end
end;
fold_aux self s h f acc
let fold self f acc p =
let h = Tbl.create 42 in
let s = Stack.create () in
Stack.push (Enter p) s;
fold_aux self s h f acc
let check_empty_conclusion store (p:t) =
if Clause.n_atoms store p > 0 then (
error_res_f "@[<2>Proof.check: non empty conclusion for clause@ %a@]"
(Clause.debug store) p;
)
let check self (p:t) = fold self (fun () _ -> ()) () p
end
module H = (Heap.Make [@specialise]) (struct
type store = Store.t
type t = var
@ -1775,7 +1504,8 @@ module Make(Plugin : PLUGIN)
let[@inline] current_slice st : _ Solver_intf.acts =
let module M = struct
type nonrec proof = lemma
type nonrec proof = proof
type nonrec lemma = lemma
type nonrec formula = formula
let iter_assumptions=acts_iter st ~full:false st.th_head
let eval_lit= acts_eval_lit st
@ -1790,7 +1520,8 @@ module Make(Plugin : PLUGIN)
(* full slice, for [if_sat] final check *)
let[@inline] full_slice st : _ Solver_intf.acts =
let module M = struct
type nonrec proof = lemma
type nonrec proof = proof
type nonrec lemma = lemma
type nonrec formula = formula
let iter_assumptions=acts_iter st ~full:true st.th_head
let eval_lit= acts_eval_lit st

6
src/sat/Solver.mli
View file

@ -4,10 +4,12 @@ module type S = Solver_intf.S
module Make_pure_sat(Th: Solver_intf.PLUGIN_SAT)
: S with module Formula = Th.Formula
and type lemma = Th.proof
and type lemma = Th.lemma
and type proof = Th.proof
and type theory = unit
module Make_cdcl_t(Th : Solver_intf.PLUGIN_CDCL_T)
: S with module Formula = Th.Formula
and type lemma = Th.proof
and type lemma = Th.lemma
and type proof = Th.proof
and type theory = Th.t

188
src/sat/Solver_intf.ml
View file

@ -64,8 +64,8 @@ type negated =
See {!val:Expr_intf.S.norm} for more details. *)
(** The type of reasons for propagations of a formula [f]. *)
type ('formula, 'proof) reason =
| Consequence of (unit -> 'formula list * 'proof) [@@unboxed]
type ('formula, 'lemma) reason =
| Consequence of (unit -> 'formula list * 'lemma) [@@unboxed]
(** [Consequence (l, p)] means that the formulas in [l] imply the propagated
formula [f]. The proof should be a proof of the clause "[l] implies [f]".
@ -90,7 +90,7 @@ type lbool = L_true | L_false | L_undefined
module type ACTS = sig
type formula
type proof
type lemma
val iter_assumptions: (formula -> unit) -> unit
(** Traverse the new assumptions on the boolean trail. *)
@ -102,19 +102,19 @@ module type ACTS = sig
(** Map the given formula to a literal, which will be decided by the
SAT solver. *)
val add_clause: ?keep:bool -> formula list -> proof -> unit
val add_clause: ?keep:bool -> formula list -> lemma -> unit
(** Add a clause to the solver.
@param keep if true, the clause will be kept by the solver.
Otherwise the solver is allowed to GC the clause and propose this
partial model again.
*)
val raise_conflict: formula list -> proof -> 'b
val raise_conflict: formula list -> lemma -> 'b
(** Raise a conflict, yielding control back to the solver.
The list of atoms must be a valid theory lemma that is false in the
current trail. *)
val propagate: formula -> (formula, proof) reason -> unit
val propagate: formula -> (formula, lemma) reason -> unit
(** Propagate a formula, i.e. the theory can evaluate the formula to be true
(see the definition of {!type:eval_res} *)
@ -124,10 +124,9 @@ module type ACTS = sig
Useful for theory combination. This will be undone on backtracking. *)
end
(* TODO: find a way to use atoms instead of formulas here *)
type ('formula, 'proof) acts =
type ('formula, 'lemma) acts =
(module ACTS with type formula = 'formula
and type proof = 'proof)
and type lemma = 'lemma)
(** The type for a slice of assertions to assume/propagate in the theory. *)
exception No_proof
@ -158,6 +157,45 @@ module type FORMULA = sig
but one returns [Negated] and the other [Same_sign]. *)
end
(** Signature for proof emission, using DRUP.
We do not store the resolution steps, just the stream of clauses deduced.
See {!Sidekick_drup} for checking these proofs. *)
module type PROOF = sig
type t
(** The stored proof (possibly nil, possibly on disk, possibly in memory) *)
type atom
(** A boolean atom for the proof trace *)
type lemma
(** A theory lemma *)
module Atom : sig
type t = atom
val sign : t -> bool
val var_int : t -> int
val make : sign:bool -> int -> t
val pp : t Fmt.printer
end
val enabled : t -> bool
(** Do we emit proofs at all? *)
val emit_input_clause : t -> atom Iter.t -> unit
(** Emit an input clause. *)
val emit_lemma : t -> atom Iter.t -> lemma -> unit
(** Emit a theory lemma *)
val emit_redundant_clause : t -> atom Iter.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 -> atom Iter.t -> unit
(** Forget a clause. Only useful for performance considerations. *)
end
(** Signature for theories to be given to the CDCL(T) solver *)
module type PLUGIN_CDCL_T = sig
type t
@ -166,6 +204,14 @@ module type PLUGIN_CDCL_T = sig
module Formula : FORMULA
type proof
(** Proof storage/recording *)
type lemma
(* Theory lemmas *)
module Proof : PROOF
with type t = proof
and type lemma = lemma
val push_level : t -> unit
(** Create a new backtrack level *)
@ -173,12 +219,12 @@ module type PLUGIN_CDCL_T = sig
val pop_levels : t -> int -> unit
(** Pop [n] levels of the theory *)
val partial_check : t -> (Formula.t, proof) acts -> unit
val partial_check : t -> (Formula.t, lemma) acts -> unit
(** Assume the formulas in the slice, possibly using the [slice]
to push new formulas to be propagated or to raising a conflict or to add
new lemmas. *)
val final_check : t -> (Formula.t, proof) acts -> unit
val final_check : t -> (Formula.t, lemma) acts -> unit
(** Called at the end of the search in case a model has been found.
If no new clause is pushed, then proof search ends and "sat" is returned;
if lemmas are added, search is resumed;
@ -189,111 +235,12 @@ end
module type PLUGIN_SAT = sig
module Formula : FORMULA
type lemma = unit
type proof
end
module type PROOF = sig
(** Signature for a module handling proof by resolution from sat solving traces *)
(** {3 Type declarations} *)
exception Resolution_error of string
(** Raised when resolution failed. *)
type formula
type atom
type lemma
type clause
(** Abstract types for atoms, clauses and theory-specific lemmas *)
type store
type t
(** Lazy type for proof trees. Proofs are persistent objects, and can be
extended to proof nodes using functions defined later. *)
and proof_node = {
conclusion : clause; (** The conclusion of the proof *)
step : step; (** The reasoning step used to prove the conclusion *)
}
(** A proof can be expanded into a proof node, which show the first step of the proof. *)
(** The type of reasoning steps allowed in a proof. *)
and step =
| Hypothesis of lemma
(** The conclusion is a user-provided hypothesis *)
| Assumption
(** The conclusion has been locally assumed by the user *)
| Lemma of lemma
(** The conclusion is a tautology provided by the theory, with associated proof *)
| Duplicate of t * atom list
(** The conclusion is obtained by eliminating multiple occurences of the atom in
the conclusion of the provided proof. *)
| Hyper_res of hyper_res_step
and hyper_res_step = {
hr_init: t;
hr_steps: (atom * t) list; (* list of pivot+clause to resolve against [init] *)
}
(** {3 Proof building functions} *)
val prove : store -> clause -> t
(** Given a clause, return a proof of that clause.
@raise Resolution_error if it does not succeed. *)
val prove_unsat : store -> clause -> t
(** Given a conflict clause [c], returns a proof of the empty clause.
@raise Resolution_error if it does not succeed. *)
val prove_atom : store -> atom -> t option
(** Given an atom [a], returns a proof of the clause [[a]] if [a] is true at level 0 *)
val res_of_hyper_res : store -> hyper_res_step -> t * t * atom
(** Turn an hyper resolution step into a resolution step.
The conclusion can be deduced by performing a resolution between the conclusions
of the two given proofs.
The atom on which to perform the resolution is also given. *)
(** {3 Proof Nodes} *)
val parents : step -> t list
(** Returns the parents of a proof node. *)
val is_leaf : step -> bool
(** Returns wether the the proof node is a leaf, i.e. an hypothesis,
an assumption, or a lemma.
[true] if and only if {!parents} returns the empty list. *)
val expl : step -> string
(** Returns a short string description for the proof step; for instance
["hypothesis"] for a [Hypothesis]
(it currently returns the variant name in lowercase). *)
(** {3 Proof Manipulation} *)
val expand : store -> t -> proof_node
(** Return the proof step at the root of a given proof. *)
val conclusion : t -> clause
(** What is proved at the root of the clause *)
val fold : store -> ('a -> proof_node -> 'a) -> 'a -> t -> 'a
(** [fold f acc p], fold [f] over the proof [p] and all its node. It is guaranteed that
[f] is executed exactly once on each proof node in the tree, and that the execution of
[f] on a proof node happens after the execution on the parents of the nodes. *)
(** {3 Misc} *)
val check_empty_conclusion : store -> t -> unit
(** Check that the proof's conclusion is the empty clause,
@raise Resolution_error otherwise *)
val check : store -> t -> unit
(** Check the contents of a proof. Mainly for internal use. *)
module Tbl : Hashtbl.S with type key = t
module Proof : PROOF
with type t = proof
and type lemma = lemma
end
(** The external interface implemented by safe solvers, such as the one
@ -317,11 +264,16 @@ module type S = sig
type theory
type lemma
(** A theory lemma or an input axiom *)
(** A theory lemma or an input axiom. *)
type proof
(** A representation of a full proof *)
type solver
(** The main solver type. *)
type store
(** Stores atoms, clauses, etc. *)
(* TODO: keep this internal *)
module Atom : sig
@ -365,11 +317,9 @@ module type S = sig
end
module Proof : PROOF
with type clause = clause
and type atom = atom
and type formula = formula
with type atom = atom
and type lemma = lemma
and type store = store
and type t = proof
(** A module to manipulate proofs. *)
type t = solver

3
src/smtlib/dune
View file

@ -3,6 +3,5 @@
(public_name sidekick-bin.smtlib)
(libraries containers zarith sidekick.core sidekick.util
sidekick-base sidekick-base.solver
sidekick.backend smtlib-utils
sidekick.tef)
smtlib-utils sidekick.tef)
(flags :standard -warn-error -a+8 -open Sidekick_util))

1
src/th-cstor/Sidekick_th_cstor.ml
View file

@ -9,6 +9,7 @@ let name = "th-cstor"
module type ARG = sig
module S : Sidekick_core.SOLVER
val view_as_cstor : S.T.Term.t -> (S.T.Fun.t, S.T.Term.t) cstor_view
val lemma_cstor : S.Lit.t Iter.t -> S.lemma
end
module type S = sig