From 7722319b0a41cb9d92398b3c8c61347da3e2fa3e Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Thu, 28 Dec 2017 16:01:36 +0100 Subject: [PATCH] move tseitin transformation into its own lib --- Makefile | 4 ++-- src/core/Res.ml | 2 +- src/core/msat.mld | 15 ++++----------- src/sat/jbuild | 2 +- src/sat/type_sat.ml | 2 +- src/smt/expr_smt.ml | 2 +- src/smt/expr_smt.mli | 2 +- src/smt/jbuild | 2 +- .../tseitin.ml => tseitin/Msat_tseitin.ml} | 0 .../tseitin.mli => tseitin/Msat_tseitin.mli} | 0 .../tseitin_intf.ml => tseitin/Tseitin_intf.ml} | 0 src/tseitin/jbuild | 12 ++++++++++++ tests/test_api.ml | 2 +- 13 files changed, 25 insertions(+), 20 deletions(-) rename src/{solver/tseitin.ml => tseitin/Msat_tseitin.ml} (100%) rename src/{solver/tseitin.mli => tseitin/Msat_tseitin.mli} (100%) rename src/{solver/tseitin_intf.ml => tseitin/Tseitin_intf.ml} (100%) create mode 100644 src/tseitin/jbuild diff --git a/Makefile b/Makefile index 3995e022..171013cd 100644 --- a/Makefile +++ b/Makefile @@ -12,7 +12,7 @@ OPTS= -j $(J) LIB=$(addprefix $(NAME), .cma .cmxa .cmxs) -all: build test +all: build-dev test build: jbuilder build $(OPTS) @install @@ -58,7 +58,7 @@ reindent: ocp-indent @find src '(' -name '*.ml' -or -name '*.mli' ')' -print0 | xargs -0 echo "reindenting: " @find src '(' -name '*.ml' -or -name '*.mli' ')' -print0 | xargs -0 ocp-indent -i -WATCH=build-dev +WATCH=all watch: while find src/ -print0 | xargs -0 inotifywait -e delete_self -e modify ; do \ echo "============ at `date` ==========" ; \ diff --git a/src/core/Res.ml b/src/core/Res.ml index f29dc568..5d9f5e26 100644 --- a/src/core/Res.ml +++ b/src/core/Res.ml @@ -201,7 +201,7 @@ module Make(St : Solver_types.S) = struct let duplicates, res = analyze (list c) in assert (cmp_cl res (list conclusion) = 0); { conclusion; step = Duplicate (c, List.concat duplicates) } - | St.History ( c :: ([d] as r)) -> + | St.History ( c :: ([_] as r)) -> let (l, c', d', a) = chain_res (c, to_list c) r in assert (cmp_cl l (to_list conclusion) = 0); { conclusion; step = Resolution (c', d', a); } diff --git a/src/core/msat.mld b/src/core/msat.mld index da9f38a9..622fc9c6 100644 --- a/src/core/msat.mld +++ b/src/core/msat.mld @@ -21,19 +21,13 @@ The following modules allow to easily create a SAT or SMT solver (remark: a SAT simply an SMT solver with an empty theory). {!modules: -Solver -Solver_intf -Formula_intf -Theory_intf +Msat_solver } The following modules allow the creation of a McSat solver (Model Constructing solver): {!modules: -Mcsolver -Solver_intf -Expr_intf -Plugin_intf +Msat_mcsolver } {4 Useful tools} @@ -41,14 +35,13 @@ Plugin_intf An instanciation of a pure sat solver is also provided: {!modules: -Sat +Msat_sat } Lastly, mSAT also provides an implementation of Tseitin's CNF conversion: {!modules: -Tseitin -Tseitin_intf +Msat_tseitin } {4 Proof Management} diff --git a/src/sat/jbuild b/src/sat/jbuild index 7ee505a7..86386d7a 100644 --- a/src/sat/jbuild +++ b/src/sat/jbuild @@ -3,7 +3,7 @@ (library ((name msat_sat) (public_name msat.sat) - (libraries (msat msat.solver)) + (libraries (msat msat.tseitin msat.solver)) (synopsis "sat interface") (flags (:standard -w +a-4-42-44-48-50-58-32-60@8 -color always -safe-string -open Msat)) (ocamlopt_flags (:standard -O3 -bin-annot diff --git a/src/sat/type_sat.ml b/src/sat/type_sat.ml index 1b846e44..426b16d7 100644 --- a/src/sat/type_sat.ml +++ b/src/sat/type_sat.ml @@ -10,7 +10,7 @@ Copyright 2014 Simon Cruanes module Id = Dolmen.Id module Ast = Dolmen.Term module H = Hashtbl.Make(Id) -module Formula = Msat_solver.Tseitin.Make(Sat.Expr) +module Formula = Msat_tseitin.Make(Sat.Expr) (* Exceptions *) (* ************************************************************************ *) diff --git a/src/smt/expr_smt.ml b/src/smt/expr_smt.ml index 51d87cd2..f3b8961f 100644 --- a/src/smt/expr_smt.ml +++ b/src/smt/expr_smt.ml @@ -521,5 +521,5 @@ module Atom = struct end -module Formula = Msat_solver.Tseitin.Make(Atom) +module Formula = Msat_tseitin.Make(Atom) diff --git a/src/smt/expr_smt.mli b/src/smt/expr_smt.mli index 7e410e8d..03f0b07c 100644 --- a/src/smt/expr_smt.mli +++ b/src/smt/expr_smt.mli @@ -322,5 +322,5 @@ module Atom : sig end -module Formula : Msat_solver.Tseitin.S with type atom = atom +module Formula : Msat_tseitin.S with type atom = atom diff --git a/src/smt/jbuild b/src/smt/jbuild index f8d694fe..843fa9c3 100644 --- a/src/smt/jbuild +++ b/src/smt/jbuild @@ -3,7 +3,7 @@ (library ((name msat_smt) (public_name msat.smt) - (libraries (msat msat.solver dolmen)) + (libraries (msat msat.solver msat.tseitin dolmen)) (synopsis "smt interface") (flags (:standard -w +a-4-42-44-48-50-58-32-60@8 -color always -safe-string -open Msat)) (ocamlopt_flags (:standard -O3 -bin-annot diff --git a/src/solver/tseitin.ml b/src/tseitin/Msat_tseitin.ml similarity index 100% rename from src/solver/tseitin.ml rename to src/tseitin/Msat_tseitin.ml diff --git a/src/solver/tseitin.mli b/src/tseitin/Msat_tseitin.mli similarity index 100% rename from src/solver/tseitin.mli rename to src/tseitin/Msat_tseitin.mli diff --git a/src/solver/tseitin_intf.ml b/src/tseitin/Tseitin_intf.ml similarity index 100% rename from src/solver/tseitin_intf.ml rename to src/tseitin/Tseitin_intf.ml diff --git a/src/tseitin/jbuild b/src/tseitin/jbuild new file mode 100644 index 00000000..e70bd0e7 --- /dev/null +++ b/src/tseitin/jbuild @@ -0,0 +1,12 @@ +; vim:ft=lisp: + +(library + ((name msat_tseitin) + (public_name msat.tseitin) + (synopsis "Tseitin transformation for msat") + (libraries ()) + (flags (:standard -w +a-4-42-44-48-50-58-32-60@8 -color always -safe-string)) + (ocamlopt_flags (:standard -O3 -bin-annot + -unbox-closures -unbox-closures-factor 20)) + )) + diff --git a/tests/test_api.ml b/tests/test_api.ml index 158dc30b..8984c12d 100644 --- a/tests/test_api.ml +++ b/tests/test_api.ml @@ -10,7 +10,7 @@ open Msat open Msat_sat module F = Sat.Expr -module T = Msat_solver.Tseitin.Make(F) +module T = Msat_tseitin.Make(F) let (|>) x f = f x