From ac396e8cf5f52fe9418181e65f6b41aee4a5bbe9 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Mon, 22 Jan 2018 22:09:47 -0600 Subject: [PATCH] rename to `cdcl` --- Makefile | 5 +++-- msat.opam => cdcl.opam | 8 ++++---- main.exe | 1 + msat.exe | 1 - src/backend/Coq.ml | 1 - src/backend/Coq.mli | 1 - src/backend/Dedukti.ml | 2 -- src/backend/Dedukti.mli | 2 -- src/backend/Dimacs.ml | 2 -- src/backend/Dimacs.mli | 2 -- src/backend/Dot.ml | 2 -- src/backend/Dot.mli | 1 - src/backend/jbuild | 10 +++++----- src/core/{Msat.ml => CDCL.ml} | 0 src/core/jbuild | 6 +++--- src/main_test/jbuild | 6 +++--- src/main_test/{msat_test.ml => main_test.ml} | 14 +++++++------- src/main_test/type_sat.ml | 4 ++-- src/main_test/type_sat.mli | 4 ++-- src/sat/{Msat_sat.ml => CDCL_sat.ml} | 2 +- src/sat/{Msat_sat.mli => CDCL_sat.mli} | 2 +- src/sat/Th_sat.ml | 10 +++++----- src/sat/Th_sat.mli | 2 +- src/sat/jbuild | 8 ++++---- src/tseitin/{Msat_tseitin.ml => CDCL_tseitin.ml} | 0 src/tseitin/{Msat_tseitin.mli => CDCL_tseitin.mli} | 0 src/tseitin/jbuild | 6 +++--- tests/jbuild | 2 +- tests/run | 6 ++++-- tests/test_api.ml | 8 ++++---- 30 files changed, 54 insertions(+), 64 deletions(-) rename msat.opam => cdcl.opam (77%) create mode 120000 main.exe delete mode 120000 msat.exe rename src/core/{Msat.ml => CDCL.ml} (100%) rename src/main_test/{msat_test.ml => main_test.ml} (95%) rename src/sat/{Msat_sat.ml => CDCL_sat.ml} (84%) rename src/sat/{Msat_sat.mli => CDCL_sat.mli} (89%) rename src/tseitin/{Msat_tseitin.ml => CDCL_tseitin.ml} (100%) rename src/tseitin/{Msat_tseitin.mli => CDCL_tseitin.mli} (100%) diff --git a/Makefile b/Makefile index c6bf8a2f..ad91e0a6 100644 --- a/Makefile +++ b/Makefile @@ -22,13 +22,14 @@ build-dev: jbuilder build $(OPTS) @install --dev build-test: build - jbuilder build $(OPTS) src/main_test/msat_test.exe + jbuilder build $(OPTS) src/main_test/main_test.exe test: build-test @echo "run API tests…" jbuilder runtest @echo "run benchmarks…" - @/usr/bin/time -f "%e" ./tests/run smt + @/usr/bin/time -f "%e" ./tests/run sat + #@/usr/bin/time -f "%e" ./tests/run smt # @/usr/bin/time -f "%e" ./tests/run mcsat enable_log: diff --git a/msat.opam b/cdcl.opam similarity index 77% rename from msat.opam rename to cdcl.opam index e5d45a09..7510703c 100644 --- a/msat.opam +++ b/cdcl.opam @@ -1,5 +1,5 @@ opam-version: "1.2" -name: "msat" +name: "cdcl" license: "Apache" version: "dev" author: ["Sylvain Conchon" "Alain Mebsout" "Stephane Lecuyer" "Simon Cruanes" "Guillaume Bury"] @@ -19,7 +19,7 @@ available: [ ocaml-version >= "4.03.0" ] tags: [ "sat" "smt" ] -homepage: "https://github.com/Gbury/mSAT" -dev-repo: "https://github.com/Gbury/mSAT.git" -bug-reports: "https://github.com/Gbury/mSAT/issues/" +homepage: "https://github.com/c-cube/cdcl" +dev-repo: "https://github.com/c-cube/cdcl.git" +bug-reports: "https://github.com/c-cube/cdcl/issues/" diff --git a/main.exe b/main.exe new file mode 120000 index 00000000..25e5011f --- /dev/null +++ b/main.exe @@ -0,0 +1 @@ +_build/default/src/main_test/main_test.exe \ No newline at end of file diff --git a/msat.exe b/msat.exe deleted file mode 120000 index 2d015b30..00000000 --- a/msat.exe +++ /dev/null @@ -1 +0,0 @@ -_build/default/src/main_test/msat_test.exe \ No newline at end of file diff --git a/src/backend/Coq.ml b/src/backend/Coq.ml index bba56ac7..aefcfa6f 100644 --- a/src/backend/Coq.ml +++ b/src/backend/Coq.ml @@ -2,7 +2,6 @@ MSAT is free software, using the Apache license, see file LICENSE Copyright 2015 Guillaume Bury *) -open Msat module type S = Backend_intf.S diff --git a/src/backend/Coq.mli b/src/backend/Coq.mli index ec743ff2..4e4828dc 100644 --- a/src/backend/Coq.mli +++ b/src/backend/Coq.mli @@ -8,7 +8,6 @@ Copyright 2015 Guillaume Bury This module provides an easy way to produce coq scripts corresponding to the resolution proofs output by the sat solver. *) -open Msat module type S = Backend_intf.S (** Interface for exporting proofs. *) diff --git a/src/backend/Dedukti.ml b/src/backend/Dedukti.ml index 76c9db7f..742f5886 100644 --- a/src/backend/Dedukti.ml +++ b/src/backend/Dedukti.ml @@ -3,8 +3,6 @@ MSAT is free software, using the Apache license, see file LICENSE Copyright 2015 Guillaume Bury *) -open Msat - module type S = Backend_intf.S module type Arg = sig diff --git a/src/backend/Dedukti.mli b/src/backend/Dedukti.mli index 826c8031..5e14c075 100644 --- a/src/backend/Dedukti.mli +++ b/src/backend/Dedukti.mli @@ -9,8 +9,6 @@ Copyright 2014 Simon Cruanes Work in progress... *) -open Msat - module type S = Backend_intf.S module type Arg = sig diff --git a/src/backend/Dimacs.ml b/src/backend/Dimacs.ml index 07b1ee02..d4ac3dcb 100644 --- a/src/backend/Dimacs.ml +++ b/src/backend/Dimacs.ml @@ -4,8 +4,6 @@ Copyright 2014 Guillaume Bury Copyright 2014 Simon Cruanes *) -open Msat - module type S = sig type st diff --git a/src/backend/Dimacs.mli b/src/backend/Dimacs.mli index e829bebd..927f88a9 100644 --- a/src/backend/Dimacs.mli +++ b/src/backend/Dimacs.mli @@ -10,8 +10,6 @@ Copyright 2014 Simon Cruanes iCNF formats. *) -open Msat - module type S = sig type st diff --git a/src/backend/Dot.ml b/src/backend/Dot.ml index d25f1a09..1087f084 100644 --- a/src/backend/Dot.ml +++ b/src/backend/Dot.ml @@ -4,8 +4,6 @@ Copyright 2014 Guillaume Bury Copyright 2014 Simon Cruanes *) -open Msat - (** Output interface for the backend *) module type S = Backend_intf.S diff --git a/src/backend/Dot.mli b/src/backend/Dot.mli index a3c9c787..5e76cc33 100644 --- a/src/backend/Dot.mli +++ b/src/backend/Dot.mli @@ -9,7 +9,6 @@ Copyright 2014 Simon Cruanes 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. *) -open Msat module type S = Backend_intf.S (** Interface for exporting proofs. *) diff --git a/src/backend/jbuild b/src/backend/jbuild index aa2609ff..f0d1cae6 100644 --- a/src/backend/jbuild +++ b/src/backend/jbuild @@ -2,11 +2,11 @@ ; main binary (library - ((name msat_backend) - (public_name msat.backend) - (synopsis "proof backends for msat") - (libraries (msat)) - (flags (:standard -w +a-4-42-44-48-50-58-32-60@8 -color always -safe-string)) + ((name CDCL_backend) + (public_name cdcl.backend) + (synopsis "proof backends for cdcl") + (libraries (cdcl)) + (flags (:standard -w +a-4-42-44-48-50-58-32-60@8 -color always -safe-string -open CDCL)) (ocamlopt_flags (:standard -O3 -bin-annot -unbox-closures -unbox-closures-factor 20)) )) diff --git a/src/core/Msat.ml b/src/core/CDCL.ml similarity index 100% rename from src/core/Msat.ml rename to src/core/CDCL.ml diff --git a/src/core/jbuild b/src/core/jbuild index 22ef52fb..d8abd569 100644 --- a/src/core/jbuild +++ b/src/core/jbuild @@ -1,9 +1,9 @@ ; vim:ft=lisp: (library - ((name msat) - (public_name msat) - (synopsis "core data structures and algorithms for msat") + ((name CDCL) + (public_name cdcl) + (synopsis "core data structures and algorithms for cdcl") (libraries ()) (flags (:standard -w +a-4-42-44-48-50-58-32-60@8 -color always -safe-string)) (ocamlopt_flags (:standard -O3 -bin-annot diff --git a/src/main_test/jbuild b/src/main_test/jbuild index cc91b1f2..11b6586f 100644 --- a/src/main_test/jbuild +++ b/src/main_test/jbuild @@ -1,9 +1,9 @@ ; vim:ft=lisp: (executable - ((name msat_test) - (libraries (msat msat.backend msat.tseitin msat.sat dolmen)) - (flags (:standard -w +a-4-42-44-48-50-58-32-60@8 -color always -safe-string -open Msat)) + ((name main_test) + (libraries (cdcl cdcl.backend cdcl.tseitin cdcl.sat dolmen)) + (flags (:standard -w +a-4-42-44-48-50-58-32-60@8 -color always -safe-string -open CDCL)) (ocamlopt_flags (:standard -O3 -bin-annot -unbox-closures -unbox-closures-factor 20)) )) diff --git a/src/main_test/msat_test.ml b/src/main_test/main_test.ml similarity index 95% rename from src/main_test/msat_test.ml rename to src/main_test/main_test.ml index 6f6228ff..b82891f8 100644 --- a/src/main_test/msat_test.ml +++ b/src/main_test/main_test.ml @@ -25,9 +25,9 @@ module type S = sig end module Make - (S : Msat.S) + (S : CDCL.S) (Th : sig - include Msat.Theory_intf.S with type t = S.theory + include CDCL.Theory_intf.S with type t = S.theory end) (T : sig include Type.S with type atom := S.atom @@ -37,7 +37,7 @@ module Make val do_task : Dolmen.Statement.t -> unit end = struct - module D = Msat_backend.Dot.Make(S.Proof)(Msat_backend.Dot.Default(S.Proof)) + module D = CDCL_backend.Dot.Make(S.Proof)(CDCL_backend.Dot.Default(S.Proof)) let hyps = ref [] @@ -45,7 +45,7 @@ module Make let th = S.theory st let t_st = T.create th - let check_model (Msat.Sat_state sat) = + let check_model (CDCL.Sat_state sat) = let check_clause c = let l = List.map (function a -> Log.debugf 99 @@ -66,7 +66,7 @@ module Make raise Incorrect_model; let t' = Sys.time () -. t in Format.printf "Sat (%f/%f)@." t t' - | S.Unsat (Msat.Unsat_state us) -> + | S.Unsat (CDCL.Unsat_state us) -> if !p_check then begin let p = us.get_proof () in S.Proof.check p; @@ -113,9 +113,9 @@ module Make Dolmen.Statement.print s end -module Sat = Make(Msat_sat)(Msat_sat.Th)(Type_sat) +module Sat = Make(CDCL_sat)(CDCL_sat.Th)(Type_sat) (* -module Smt = Make(Minismt_smt)(Msat_sat.Th)(Minismt_smt.Type) +module Smt = Make(Minismt_smt)(CDCL_sat.Th)(Minismt_smt.Type) *) let solver = ref (module Sat : S) diff --git a/src/main_test/type_sat.ml b/src/main_test/type_sat.ml index b733d31e..e6124421 100644 --- a/src/main_test/type_sat.ml +++ b/src/main_test/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_tseitin.Make(Msat_sat.Th) +module Formula = CDCL_tseitin.Make(CDCL_sat.Th) (* Exceptions *) (* ************************************************************************ *) @@ -36,7 +36,7 @@ let find_id st id = try H.find st.symbols id with Not_found -> - let res = Msat_sat.Th.fresh st.fresh in + let res = CDCL_sat.Th.fresh st.fresh in H.add st.symbols id res; res diff --git a/src/main_test/type_sat.mli b/src/main_test/type_sat.mli index 01011b17..5f081f16 100644 --- a/src/main_test/type_sat.mli +++ b/src/main_test/type_sat.mli @@ -8,7 +8,7 @@ Copyright 2014 Simon Cruanes This module provides functions to parse terms from the untyped syntax tree defined in Dolmen, and generate formulas as defined in the Expr_sat module. *) -include Type.S with type atom := Msat_sat.Th.formula +include Type.S with type atom := CDCL_sat.Th.formula -val create : Msat_sat.Th.t -> t +val create : CDCL_sat.Th.t -> t diff --git a/src/sat/Msat_sat.ml b/src/sat/CDCL_sat.ml similarity index 84% rename from src/sat/Msat_sat.ml rename to src/sat/CDCL_sat.ml index 016fa3b2..c418ae5d 100644 --- a/src/sat/Msat_sat.ml +++ b/src/sat/CDCL_sat.ml @@ -5,5 +5,5 @@ Copyright 2016 Guillaume Bury module Th = Th_sat -include Msat.Make(Th) +include CDCL.Make(Th) diff --git a/src/sat/Msat_sat.mli b/src/sat/CDCL_sat.mli similarity index 89% rename from src/sat/Msat_sat.mli rename to src/sat/CDCL_sat.mli index d0201e41..231b1cb3 100644 --- a/src/sat/Msat_sat.mli +++ b/src/sat/CDCL_sat.mli @@ -11,6 +11,6 @@ Copyright 2016 Guillaume Bury module Th = Th_sat -include module type of Msat.Make(Th) +include module type of CDCL.Make(Th) (** A functor that can generate as many solvers as needed. *) diff --git a/src/sat/Th_sat.ml b/src/sat/Th_sat.ml index 07b484d9..0916cf97 100644 --- a/src/sat/Th_sat.ml +++ b/src/sat/Th_sat.ml @@ -8,7 +8,7 @@ type proof = unit type formula = int type t = { - actions: (formula, proof) Msat.actions; + actions: (formula, proof) CDCL.actions; mutable max_index: int; mutable max_fresh: int; } @@ -49,9 +49,9 @@ module Form = struct let norm a = abs a, if a < 0 then - Msat.Negated + CDCL.Negated else - Msat.Same_sign + CDCL.Same_sign let print fmt a = Format.fprintf fmt "%s%s%d" @@ -82,6 +82,6 @@ let iter: (t -> unit) -> unit = fun f -> done *) -let assume _ _ = Msat.Theory_intf.Sat +let assume _ _ = CDCL.Theory_intf.Sat -let if_sat _ _ = Msat.Theory_intf.Sat +let if_sat _ _ = CDCL.Theory_intf.Sat diff --git a/src/sat/Th_sat.mli b/src/sat/Th_sat.mli index 1e30c2e3..2121adb6 100644 --- a/src/sat/Th_sat.mli +++ b/src/sat/Th_sat.mli @@ -8,7 +8,7 @@ near optimal efficiency (both in terms of space and time). *) -open Msat +open CDCL include Theory_intf.S with type formula = int and type proof = unit (** This modules implements the requirements for implementing an SAT Solver. *) diff --git a/src/sat/jbuild b/src/sat/jbuild index cc2424e4..7d2cf448 100644 --- a/src/sat/jbuild +++ b/src/sat/jbuild @@ -1,11 +1,11 @@ ; vim:ft=lisp: (library - ((name msat_sat) - (public_name msat.sat) - (libraries (msat msat.tseitin)) + ((name CDCL_sat) + (public_name cdcl.sat) + (libraries (cdcl cdcl.tseitin)) (synopsis "sat interface") - (flags (:standard -w +a-4-42-44-48-50-58-32-60@8 -color always -safe-string -open Msat)) + (flags (:standard -w +a-4-42-44-48-50-58-32-60@8 -color always -safe-string -open CDCL)) (ocamlopt_flags (:standard -O3 -bin-annot -unbox-closures -unbox-closures-factor 20)) )) diff --git a/src/tseitin/Msat_tseitin.ml b/src/tseitin/CDCL_tseitin.ml similarity index 100% rename from src/tseitin/Msat_tseitin.ml rename to src/tseitin/CDCL_tseitin.ml diff --git a/src/tseitin/Msat_tseitin.mli b/src/tseitin/CDCL_tseitin.mli similarity index 100% rename from src/tseitin/Msat_tseitin.mli rename to src/tseitin/CDCL_tseitin.mli diff --git a/src/tseitin/jbuild b/src/tseitin/jbuild index e70bd0e7..de0d8941 100644 --- a/src/tseitin/jbuild +++ b/src/tseitin/jbuild @@ -1,9 +1,9 @@ ; vim:ft=lisp: (library - ((name msat_tseitin) - (public_name msat.tseitin) - (synopsis "Tseitin transformation for msat") + ((name CDCL_tseitin) + (public_name cdcl.tseitin) + (synopsis "Tseitin transformation for CDCL") (libraries ()) (flags (:standard -w +a-4-42-44-48-50-58-32-60@8 -color always -safe-string)) (ocamlopt_flags (:standard -O3 -bin-annot diff --git a/tests/jbuild b/tests/jbuild index 879d27cf..e9fae11e 100644 --- a/tests/jbuild +++ b/tests/jbuild @@ -2,7 +2,7 @@ (executable ((name test_api) - (libraries (msat msat.tseitin msat.backend msat.sat)) + (libraries (cdcl cdcl.tseitin cdcl.backend cdcl.sat)) (flags (:standard -w +a-4-42-44-48-50-58-32-60@8 -color always -safe-string)) (ocamlopt_flags (:standard -O3 -color always -unbox-closures -unbox-closures-factor 20)) diff --git a/tests/run b/tests/run index 463ab373..235a9159 100755 --- a/tests/run +++ b/tests/run @@ -1,10 +1,12 @@ #!/bin/bash CURDIR=`dirname $0` -SOLVER="$CURDIR/../msat.exe" +SOLVER="$CURDIR/../main.exe" solvertest () { - for f in `find -L $1 -type f -name '*.cnf' -o -name '*.smt2'` + # FIXME + #for f in `find -L $1 -type f -name '*.cnf' -o -name '*.smt2'` + for f in `find -L $1 -type f -name '*.cnf'` do echo -ne "\r\033[KTesting $f..." "$SOLVER" -s $3 -time 30s -size 1G -check $f | grep $2 diff --git a/tests/test_api.ml b/tests/test_api.ml index be0bba02..566e3755 100644 --- a/tests/test_api.ml +++ b/tests/test_api.ml @@ -6,10 +6,10 @@ Copyright 2014 Simon Cruanes (* Tests that require the API *) -open Msat +open CDCL -module Th = Msat_sat.Th -module F = Msat_tseitin.Make(Th) +module Th = CDCL_sat.Th +module F = CDCL_tseitin.Make(Th) let (|>) x f = f x @@ -48,7 +48,7 @@ end let mk_solver (): (module BASIC_SOLVER) = let module S = struct - include Msat_sat + include CDCL_sat let create() = create() let solve st ?assumptions () = match solve st ?assumptions() with