From bbbd40763152b054182a72b8679d10f9270b5989 Mon Sep 17 00:00:00 2001 From: Guillaume Bury Date: Fri, 2 Oct 2015 13:30:32 +0200 Subject: [PATCH] Res now includes solver type --- _tags | 1 + backend/dedukti.ml | 43 +++++++++++++++++++++++++++++++----------- backend/dedukti.mli | 9 ++++++--- backend/dot.ml | 11 +++++------ backend/dot.mli | 4 +--- smt/mcsat.ml | 1 - solver/internal.mli | 5 +---- solver/mcsolver.mli | 5 ++--- solver/res.ml | 2 ++ solver/res.mli | 3 +-- solver/res_intf.ml | 9 ++++++--- solver/solver.mli | 5 +---- solver/solver_types.ml | 1 - tests/run | 2 +- util/log.ml | 2 +- 15 files changed, 60 insertions(+), 43 deletions(-) diff --git a/_tags b/_tags index 044a9402..acfe0b21 100644 --- a/_tags +++ b/_tags @@ -13,5 +13,6 @@ # more warnings <**/*.ml>: warn_K, warn_Y, warn_X +<**/*.ml>: keep_locks, short_paths, safe_string, strict_sequence <**/*.cm*>: debug diff --git a/backend/dedukti.ml b/backend/dedukti.ml index 6b219c15..2bd18c80 100644 --- a/backend/dedukti.ml +++ b/backend/dedukti.ml @@ -1,26 +1,44 @@ (* MSAT is free software, using the Apache license, see file LICENSE -Copyright 2014 Guillaume Bury -Copyright 2014 Simon Cruanes +Copyright 2015 Guillaume Bury *) module type S = Backend_intf.S module type Arg = sig + type proof + type lemma type formula - val prove : Format.formatter -> formula list -> unit + + val print : Format.formatter -> formula -> unit + val prove : Format.formatter -> lemma -> unit val context : Format.formatter -> proof -> unit - val translate : Format.formatter -> formula -> unit end -module Make(S : Res.S)(A : Arg with type formula := S.atom and type proof := S.proof) = struct +module Make(S : Res.S)(A : Arg with type formula := S.St.formula and type proof := S.proof) = struct - let print_aux fmt = Format.fprintf fmt "@\n" + let pp_nl fmt = Format.fprintf fmt "@\n" + let fprintf fmt format = Format.kfprintf pp_nl fmt format - let fprintf fmt format = Format.kfprintf print_aux fmt format + let clause_name c = S.St.(c.name) - let context fmt () = + let pp_clause fmt c = + let rec aux fmt = function + | [] -> () + | a :: r -> + let f, pos = + if S.St.(a.var.pa == a) then + S.St.(a.lit), true + else + S.St.(a.neg.lit), false + in + fprintf fmt "%s _b %a ->@ %a" + (if pos then "_pos" else "_neg") A.print f aux r + in + fprintf fmt "_b : Prop ->@ %a ->@ _proof _b" aux (S.to_list c) + + let context fmt p = fprintf fmt "(; Embedding ;)"; fprintf fmt "Prop : Type."; fprintf fmt "_proof : Prop -> Type."; @@ -28,10 +46,13 @@ module Make(S : Res.S)(A : Arg with type formula := S.atom and type proof := S.p fprintf fmt "_pos : Prop -> Prop -> Type."; fprintf fmt "_neg : Prop -> Prop -> Type."; fprintf fmt "[b: Prop, p: Prop] _pos b p --> _proof p -> _proof b."; - fprintf fmt "[b: Prop, p: Prop] _neg b p --> _pos b p -> _proof b." + fprintf fmt "[b: Prop, p: Prop] _neg b p --> _pos b p -> _proof b."; + A.context fmt p - let print fmt _ = - context fmt (); + let print fmt p = + fprintf fmt "#NAME Proof."; + fprintf fmt "(; Dedukti file automatically generated by mSAT ;)"; + context fmt p; () end diff --git a/backend/dedukti.mli b/backend/dedukti.mli index 3a14b23e..b39aa26a 100644 --- a/backend/dedukti.mli +++ b/backend/dedukti.mli @@ -2,15 +2,18 @@ module type S = Backend_intf.S module type Arg = sig + + type lemma type proof type formula - val prove : Format.formatter -> formula list -> unit + + val print : Format.formatter -> formula -> unit + val prove : Format.formatter -> lemma -> unit val context : Format.formatter -> proof -> unit - val translate : Format.formatter -> formula -> unit end module Make : functor(S : Res.S) -> - functor(A : Arg with type formula := S.atom and type proof := S.proof) -> + functor(A : Arg with type formula := S.St.formula and type proof := S.proof) -> S with type t := S.proof (** Functor to generate a backend to output proofs for the dedukti type checker. *) diff --git a/backend/dot.ml b/backend/dot.ml index 894449a5..cc04791a 100644 --- a/backend/dot.ml +++ b/backend/dot.ml @@ -2,18 +2,17 @@ module type S = Backend_intf.S module type Arg = sig + type atom - type clause type lemma - val clause_name : clause -> string val print_atom : Format.formatter -> atom -> unit val lemma_info : lemma -> string * string option * (Format.formatter -> unit -> unit) list end -module Make(S : Res.S)(A : Arg with type atom := S.atom and type clause := S.clause and type lemma := S.lemma) = struct +module Make(S : Res.S)(A : Arg with type atom := S.atom and type lemma := S.lemma) = struct - let node_id n = A.clause_name S.(n.conclusion) + let node_id n = n.S.conclusion.S.St.name let res_node_id n = (node_id n) ^ "_res" @@ -55,14 +54,14 @@ module Make(S : Res.S)(A : Arg with type atom := S.atom and type clause := S.cla match S.(n.step) with | S.Hypothesis -> print_dot_node fmt (node_id n) "LIGHTBLUE" S.(n.conclusion) "Hypothesis" "LIGHTBLUE" - [(fun fmt () -> (Format.fprintf fmt "%s" (A.clause_name n.S.conclusion)))]; + [(fun fmt () -> (Format.fprintf fmt "%s" (node_id n)))]; | S.Lemma lemma -> let rule, color, l = A.lemma_info lemma in let color = match color with None -> "YELLOW" | Some c -> c in print_dot_node fmt (node_id n) "LIGHTBLUE" S.(n.conclusion) rule color l | S.Resolution (_, _, a) -> print_dot_node fmt (node_id n) "GREY" S.(n.conclusion) "Resolution" "GREY" - [(fun fmt () -> (Format.fprintf fmt "%s" (A.clause_name n.S.conclusion)))]; + [(fun fmt () -> (Format.fprintf fmt "%s" (node_id n)))]; print_dot_res_node fmt (res_node_id n) a; print_edge fmt (node_id n) (res_node_id n) diff --git a/backend/dot.mli b/backend/dot.mli index 2520aef4..aa86092d 100644 --- a/backend/dot.mli +++ b/backend/dot.mli @@ -3,14 +3,12 @@ module type S = Backend_intf.S module type Arg = sig type atom - type clause type lemma - val clause_name : clause -> string val print_atom : Format.formatter -> atom -> unit val lemma_info : lemma -> string * string option * (Format.formatter -> unit -> unit) list end -module Make(S : Res.S)(A : Arg with type atom := S.atom and type clause := S.clause and type lemma := S.lemma) : +module Make(S : Res.S)(A : Arg with type atom := S.atom and type lemma := S.lemma) : S with type t := S.proof diff --git a/smt/mcsat.ml b/smt/mcsat.ml index 257682ea..47edf2c5 100644 --- a/smt/mcsat.ml +++ b/smt/mcsat.ml @@ -112,7 +112,6 @@ module Make(Dummy:sig end) = struct module SmtSolver = Mcsolver.Make(Log)(Fsmt)(Tsmt) module Dot = Dot.Make(SmtSolver.Proof)(struct - let clause_name c = SmtSolver.St.(c.name) let print_atom = SmtSolver.St.print_atom let lemma_info () = "Proof", Some "PURPLE", [] end) diff --git a/solver/internal.mli b/solver/internal.mli index 6e640f8a..89e94f4b 100644 --- a/solver/internal.mli +++ b/solver/internal.mli @@ -10,10 +10,7 @@ module Make (L : Log_intf.S)(St : Solver_types.S) exception Unsat - module Proof : Res.S - with type atom = St.atom - and type clause = St.clause - and type lemma = Th.proof + module Proof : Res.S with module St = St val solve : unit -> unit (** Try and solves the current set of assumptions. diff --git a/solver/mcsolver.mli b/solver/mcsolver.mli index 33672b3d..2af323b5 100644 --- a/solver/mcsolver.mli +++ b/solver/mcsolver.mli @@ -13,11 +13,10 @@ module Make (L : Log_intf.S)(E : Expr_intf.S) module St : Solver_types.S with type term = E.Term.t and type formula = E.Formula.t + and type proof = E.proof module Proof : Res.S - with type atom = St.atom - and type clause = St.clause - and type lemma = Th.proof + with module St = St val solve : unit -> unit (** Try and solves the current set of assumptions. diff --git a/solver/res.ml b/solver/res.ml index 0d0f6d61..6688a81e 100644 --- a/solver/res.ml +++ b/solver/res.ml @@ -8,6 +8,8 @@ module type S = Res_intf.S module Make(L : Log_intf.S)(St : Solver_types.S) = struct + module St = St + (* Type definitions *) type lemma = St.proof type clause = St.clause diff --git a/solver/res.mli b/solver/res.mli index 657937e7..fef361ca 100644 --- a/solver/res.mli +++ b/solver/res.mli @@ -8,6 +8,5 @@ module type S = Res_intf.S module Make : functor (L : Log_intf.S) -> - functor (St : Solver_types.S) -> - S with type atom = St.atom and type clause = St.clause and type lemma = St.proof + functor (St : Solver_types.S) -> S with module St = St (** Functor to create a module building proofs from a sat-solver unsat trace. *) diff --git a/solver/res_intf.ml b/solver/res_intf.ml index d81628be..419c433e 100644 --- a/solver/res_intf.ml +++ b/solver/res_intf.ml @@ -7,14 +7,17 @@ Copyright 2014 Simon Cruanes module type S = sig (** Signature for a module handling proof by resolution from sat solving traces *) + module St : Solver_types.S + (** Module defining atom and clauses *) + (** {3 Type declarations} *) exception Insuficient_hyps (** Raised when a complete resolution derivation cannot be found using the current hypotheses. *) - type atom - type clause - type lemma + type atom = St.atom + type clause = St.clause + type lemma = St.proof (** Abstract types for atoms, clauses and theory-specific lemmas *) type proof diff --git a/solver/solver.mli b/solver/solver.mli index 6777f73e..6d668d89 100644 --- a/solver/solver.mli +++ b/solver/solver.mli @@ -22,10 +22,7 @@ module Make (L : Log_intf.S)(F : Formula_intf.S) with type formula = F.t and type proof = F.proof - module Proof : Res.S - with type atom = St.atom - and type clause = St.clause - and type lemma = Th.proof + module Proof : Res.S with module St = St val solve : unit -> unit (** Try and solves the current set of assumptions. diff --git a/solver/solver_types.ml b/solver/solver_types.ml index 9d363ed8..a7062309 100644 --- a/solver/solver_types.ml +++ b/solver/solver_types.ml @@ -349,7 +349,6 @@ module SatMake (L : Log_intf.S)(E : Formula_intf.S) = struct | Lemma of proof | History of clause list - (* Flag for Mcsat v.s Pure Sat *) (* Flag for Mcsat v.s Pure Sat *) let mcsat = false diff --git a/tests/run b/tests/run index 882ff2a2..18241eb1 100755 --- a/tests/run +++ b/tests/run @@ -7,7 +7,7 @@ solvertest () { for f in `find -L $1 -type f -name '*.cnf' -o -name '*.smt2'` do echo -ne "\r\033[KTesting $f..." - "$SOLVER" -s $3 -check -time 30s -size 1G $f | grep $2 + "$SOLVER" -s $3 -time 30s -size 1G $f | grep $2 RET=$? if [ $RET -ne 0 ]; then diff --git a/util/log.ml b/util/log.ml index cd5cfc95..6162952d 100644 --- a/util/log.ml +++ b/util/log.ml @@ -44,5 +44,5 @@ let on_buffer pp x = Buffer.contents buf let on_fmt pp x = - pp Format.str_formatter x; + let _ = pp Format.str_formatter x in Format.flush_str_formatter ()