From 607ec3f043b5d82106881710a936c1ad77a77c29 Mon Sep 17 00:00:00 2001 From: Guillaume Bury Date: Mon, 7 Aug 2017 18:09:25 +0200 Subject: [PATCH] Added Coq backend (not tested yet) --- src/backend/coq.ml | 173 +++++++++++++++++++++++++++++++++++++++++++ src/backend/coq.mli | 50 +++++++++++++ src/core/res_intf.ml | 17 ++++- src/doc.txt | 1 + src/msat.mlpack | 1 + src/msat.odocl | 1 + 6 files changed, 239 insertions(+), 4 deletions(-) create mode 100644 src/backend/coq.ml create mode 100644 src/backend/coq.mli diff --git a/src/backend/coq.ml b/src/backend/coq.ml new file mode 100644 index 00000000..39009c2a --- /dev/null +++ b/src/backend/coq.ml @@ -0,0 +1,173 @@ +(* +MSAT is free software, using the Apache license, see file LICENSE +Copyright 2015 Guillaume Bury +*) + +module type S = Backend_intf.S + +module type Arg = sig + + type atom + + type hyp + type lemma + type assumption + + val print_atom : Format.formatter -> atom -> unit + + val prove_hyp : Format.formatter -> string -> hyp -> unit + val prove_lemma : Format.formatter -> string -> lemma -> unit + val prove_assumption : Format.formatter -> string -> assumption -> unit + +end + +module Make(S : Res.S)(A : Arg with type atom := S.atom + and type hyp := S.clause + and type lemma := S.clause + and type assumption := S.clause) = struct + + module M = Map.Make(struct + type t = S.St.atom + let compare a b = compare a.S.St.aid b.S.St.aid + end) + + let name c = c.S.St.name + + let pp_atom fmt a = + if a == S.St.(a.var.pa) then + Format.fprintf fmt "~ %a" A.print_atom a + else + Format.fprintf fmt "~ ~ %a" A.print_atom a.S.St.neg + + let pp_clause fmt c = + let rec aux fmt (a, i) = + if i < Array.length a then + Format.fprintf fmt "@[%a ->@ @]%a" + pp_atom a.(i) aux (a, i + 1) + else + Format.fprintf fmt "False" + in + Format.fprintf fmt "@[(%a)@]" aux (c.S.St.atoms, 0) + + let pp_clause_intro fmt c = + let rec aux fmt acc a i = + if i >= Array.length a then acc + else begin + let name = Format.sprintf "A%d" i in + Format.fprintf fmt "%s@ " name; + aux fmt (M.add a.(i) name acc) a (i + 1) + end + in + Format.fprintf fmt "intros @["; + let m = aux fmt M.empty c.S.St.atoms 0 in + Format.fprintf fmt "@].@\n"; + m + + let clausify + + let elim_duplicate fmt goal hyp _ = + (** Printing info comment in coq *) + Format.fprintf fmt "(* Eliminating doublons.@\n"; + Format.fprintf fmt " Goal : %s ; Hyp : %s *)@\n" (name goal) (name hyp); + (** Use 'assert' to introduce the clause we want to prove *) + Format.fprintf fmt "assert (%s: %a).@\n" (name goal) pp_clause goal; + (** Prove the goal: intro the atoms, then use them with the hyp *) + let m = pp_clause_intro fmt goal in + Format.fprintf fmt "exact (%s%a).@\n" + (name hyp) (fun fmt -> Array.iter (fun atom -> + Format.fprintf fmt " %s" (M.find atom m))) hyp.S.St.atoms + + let resolution fmt goal hyp1 hyp2 atom = + let a = S.St.(atom.var.pa) in + let h1, h2 = + if Array.memq a hyp1.S.St.atoms then hyp1, hyp2 + else (assert (Array.memq a hyp2.S.St.atoms); hyp2, hyp1) + in + (** Print some debug info *) + Format.fprintf fmt "(* Clausal resolution.@\n"; + Format.fprintf fmt " Goal : %s ; Hyps : %s, %s *)@\n" + (name goal) (name h1) (name h2); + (** use a cut to introduce the clause we want to prove *) + Format.fprintf fmt "assert (%s: %a).@\n" (name goal) pp_clause goal; + (** Prove the goal: intro the axioms, then perform resolution *) + let m = pp_clause_intro fmt goal in + Format.fprintf fmt "exact (%s%a).@\n" + (name h1) (fun fmt -> Array.iter (fun b -> + if b == a then begin + Format.fprintf fmt " (fun p => %s%a" + (name h2) (fun fmt -> (Array.iter (fun c -> + if c == a.S.St.neg then + Format.fprintf fmt " (fun np => np p)" + else + Format.fprintf fmt " %s" (M.find c m))) + ) h2.S.St.atoms + end else + Format.fprintf fmt " %s" (M.find b m)) + ) h1.S.St.atoms + + + let prove_node t fmt node = + let clause = node.S.conclusion in + match node.S.step with + | S.Hypothesis -> + A.prove_hyp fmt (name clause) clause + | S.Assumption -> + A.prove_assumption fmt (name clause) clause + | S.Lemma _ -> + A.prove_lemma fmt (name clause) clause + | S.Duplicate (p, l) -> + let c = (S.expand p).S.conclusion in + elim_duplicate fmt clause c l + | S.Resolution (p1, p2, a) -> + let c1 = (S.expand p1).S.conclusion in + let c2 = (S.expand p2).S.conclusion in + resolution fmt clause c1 c2 a + + (* Here the main idea is to always try and have exactly + one goal to prove, i.e False. So each *) + let print fmt p = + let h = S.H.create 4013 in + let aux () node = + Format.fprintf fmt "%a@\n@\n" (prove_node h) node + in + Format.fprintf fmt "(* Coq proof generated by mSAT*)@\n"; + S.fold aux () p + +end + + +module Simple(S : Res.S) + (A : Arg with type atom := S.St.formula + and type hyp = S.St.formula list + and type lemma := S.lemma + and type assumption := S.St.formula) = + Make(S)(struct + + (* Some helpers *) + let lit a = a.S.St.lit + + let get_assumption c = + match S.to_list c with + | [ x ] -> x + | _ -> assert false + + let get_lemma c = + match c.S.St.cpremise with + | S.St.Lemma p -> p + | _ -> assert false + + (* Actual functions *) + let print_atom fmt a = + A.print_atom fmt a.S.St.lit + + let prove_hyp fmt name c = + A.prove_hyp fmt name (List.map lit (S.to_list c)) + + let prove_lemma fmt name c = + A.prove_lemma fmt name (get_lemma c) + + let prove_assumption fmt name c = + A.prove_assumption fmt name (lit (get_assumption c)) + + end) + diff --git a/src/backend/coq.mli b/src/backend/coq.mli new file mode 100644 index 00000000..76faabfc --- /dev/null +++ b/src/backend/coq.mli @@ -0,0 +1,50 @@ +(* +MSAT is free software, using the Apache license, see file LICENSE +Copyright 2015 Guillaume Bury +*) + +(** Coq Backend + + This module provides an easy way to produce coq scripts + corresponding to the resolution proofs output by the + sat solver. *) + +module type S = Backend_intf.S +(** Interface for exporting proofs. *) + +module type Arg = sig + (** Term printing for Coq *) + + type atom + (** The type of atomic formulas *) + + type hyp + type lemma + type assumption + (** The types of hypotheses, lemmas, and assumptions *) + + val print_atom : Format.formatter -> atom -> unit + (** Print the given atomic formula *) + + val prove_hyp : Format.formatter -> string -> hyp -> unit + val prove_lemma : Format.formatter -> string -> lemma -> unit + val prove_assumption : Format.formatter -> string -> assumption -> unit + (** Proving function for hypotheses, lemmas and assumptions. + [prove_x fmt name x] should prove [x], and be such that after + executing it, [x] is among the coq hypotheses under the name [name]. *) + +end + +module Make(S : Res.S)(A : Arg with type atom := S.atom + and type hyp := S.clause + and type lemma := S.clause + and type assumption := S.clause) : S with type t := S.proof +(** Base functor to output Coq proofs *) + + +module Simple(S : Res.S)(A : Arg with type atom := S.St.formula + and type hyp = S.St.formula list + and type lemma := S.lemma + and type assumption := S.St.formula) : S with type t := S.proof +(** Simple functo to output Coq proofs *) + diff --git a/src/core/res_intf.ml b/src/core/res_intf.ml index a9d02b6c..3ac445dd 100644 --- a/src/core/res_intf.ml +++ b/src/core/res_intf.ml @@ -83,8 +83,8 @@ module type S = sig val expl : step -> string (** Returns a short string description for the proof step; for instance - ["hypothesis"] for a [Hypothesis] (generally, it currently is the - variant name in lowercase). *) + ["hypothesis"] for a [Hypothesis] + (it currently returns the variant name in lowercase). *) val parents : step -> proof list (** Returns the parents of a proof node. *) @@ -97,8 +97,8 @@ module type S = sig val fold : ('a -> proof_node -> 'a) -> 'a -> proof -> '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 ndoe in the tree, and that the execution of - [f] on a proof node happens after the execution on the children of the nodes. *) + [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. *) val unsat_core : proof -> clause list (** Returns the unsat_core of the given proof, i.e the lists of conclusions of all leafs of the proof. @@ -113,4 +113,13 @@ module type S = sig val print_clause : Format.formatter -> clause -> unit (** A nice looking printer for clauses, which sort the atoms before printing. *) + + (** {3 Unsafe} *) + + module H : Hashtbl.S with type key = clause + (** Hashtable over clauses. Uses the details of the internal representation + to achieve the best performances, however hashtables from this module + become invalid when solving is restarted, so they should only be live + during inspection of a single proof. *) + end diff --git a/src/doc.txt b/src/doc.txt index 66503fb5..da9f38a9 100644 --- a/src/doc.txt +++ b/src/doc.txt @@ -74,6 +74,7 @@ Backends for exporting proofs to different formats: {!modules: Dot +Coq Dedukti Backend_intf } diff --git a/src/msat.mlpack b/src/msat.mlpack index 87487681..088df142 100644 --- a/src/msat.mlpack +++ b/src/msat.mlpack @@ -22,6 +22,7 @@ Solver_types Res Backend_intf Dot +Coq Dimacs Dedukti diff --git a/src/msat.odocl b/src/msat.odocl index 60c485dc..4e17798f 100644 --- a/src/msat.odocl +++ b/src/msat.odocl @@ -23,6 +23,7 @@ solver/Tseitin # Backends backend/Dot +backend/Coq backend/Dedukti backend/Backend_intf