wip: make SMT great again

Gbury · Aug 16, 2016 · 41557a1 · Gbury · Aug 16, 2016 · 41557a1
1 parent 7d57b3f
commit 41557a1
Show file tree

Hide file tree

Showing 42 changed files with 1,968 additions and 198 deletions.
diff --git a/.merlin b/.merlin
@@ -1,6 +1,7 @@
 S src/core
 S src/solver
-S src/example
+S src/sat
+S src/smt
 S src/backend
 S src/util
 S src/util/smtlib
@@ -9,7 +10,8 @@ S tests
 B _build/src/
 B _build/src/core
 B _build/src/solver
-B _build/src/example
+B _build/src/sat
+B _build/src/smt
 B _build/src/util
 B _build/src/util/smtlib
 B _build/src/backend

diff --git a/META b/META
@@ -1,3 +1,4 @@
+# meta
 name="msat"
 version="dev"
 description="MSAT is a modular SAT solver, plus extensions"
@@ -6,3 +7,25 @@ archive(byte) = "msat.cma"
 archive(byte, plugin) = "msat.cma"
 archive(native) = "msat.cmxa"
 archive(native, plugin) = "msat.cmxs"
+
+package "sat" (
+ version = "dev"
+ description = "SAT solver instance"
+ requires = "msat"
+ archive(byte) = "msat_sat.cma"
+ archive(byte, plugin) = "msat_sat.cma"
+ archive(native) = "msat_sat.cmxa"
+ archive(native, plugin) = "msat_sat.cmxs"
+ exists_if = "msat_sat.cma"
+)
+
+package "smt" (
+ version = "dev"
+ description = "SMT solver instance"
+ requires = "msat"
+ archive(byte) = "msat_smt.cma"
+ archive(byte, plugin) = "msat_smt.cma"
+ archive(native) = "msat_smt.cmxa"
+ archive(native, plugin) = "msat_smt.cmxs"
+ exists_if = "msat_smt.cma"
+)
diff --git a/Makefile b/Makefile
@@ -3,12 +3,20 @@
 LOG=build.log
 COMP=ocamlbuild -log $(LOG) -use-ocamlfind
 FLAGS=
-DOC=msat.docdir/index.html
+DOC=msat.docdir/index.html msat_smt.docdir/index.html
 BIN=main.native
 TEST_BIN=tests/test_api.native
-NAME=msat
 
-LIB=$(addprefix $(NAME), .cma .cmxa .cmxs)
+NAME_OCAMLFIND=msat
+NAME_BIN=msat
+NAME_CORE=msat
+NAME_SAT=msat_sat
+NAME_SMT=msat_smt
+
+LIB_CORE=$(addprefix $(NAME_CORE), .cma .cmxa .cmxs)
+LIB_SAT=$(addprefix $(NAME_SAT), .cma .cmxa .cmxs)
+LIB_SMT=$(addprefix $(NAME_SMT), .cma .cmxa .cmxs)
+LIB=$(LIB_CORE) $(LIB_SAT) $(LIB_SMT)
 
 all: lib test
 
@@ -20,7 +28,7 @@ doc:
 
 bin:
 	$(COMP) $(FLAGS) $(BIN)
-	cp $(BIN) $(NAME) && rm $(BIN)
+	cp $(BIN) $(NAME_BIN) && rm $(BIN)
 
 test_bin:
 	$(COMP) $(FLAGS) $(TEST_BIN)
@@ -44,16 +52,26 @@ log:
 clean:
 	$(COMP) -clean
 
-TO_INSTALL=META $(addprefix _build/src/,$(LIB) $(NAME).a $(NAME).cmi)
+ALL_NAMES = $(NAME_CORE) $(NAME_SAT) $(NAME_SMT)
+TO_INSTALL_LIB=$(addsuffix .a, $(ALL_NAMES)) \
+	       $(addsuffix .cmi, $(ALL_NAMES))
+TO_INSTALL=META $(addprefix _build/src/,$(LIB) $(TO_INSTALL_LIB))
 
 install: lib
-	ocamlfind install msat $(TO_INSTALL)
+	ocamlfind install $(NAME_OCAMLFIND) $(TO_INSTALL)
 
 uninstall:
-	ocamlfind remove msat
+	ocamlfind remove $(NAME_OCAMLFIND)
 
 reinstall: all
-	ocamlfind remove msat || true
-	ocamlfind install msat $(TO_INSTALL)
+	ocamlfind remove $(NAME_OCAMLFIND) || true
+	ocamlfind install $(NAME_OCAMLFIND) $(TO_INSTALL)
+
+watch:
+	while find src/ -print0 | xargs -0 inotifywait -e delete_self -e modify ; do \
+		echo "============ at `date` ==========" ; \
+		sleep 0.1; \
+		make all; \
+	done
 
 .PHONY: clean doc all bench install uninstall reinstall enable_log disable_log bin test
diff --git a/_tags b/_tags
@@ -9,7 +9,8 @@ true: inline(100), optimize(3), unbox_closures, unbox_closures_factor(20)
 <src/core>: include
 <src/solver>: include
 <src/backend>: include
-<src/example>: include
+<src/smt>: include
+<src/sat>: include
 <src/util>: include
 <src/util/smtlib>: include
 
@@ -18,7 +19,8 @@ true: inline(100), optimize(3), unbox_closures, unbox_closures_factor(20)
 <src/solver/*.cmx>: for-pack(Msat)
 <src/backend/*.cmx>: for-pack(Msat)
 <src/util/*.cmx>: for-pack(Msat)
-<src/example/*.cmx>: for-pack(Msat)
+<src/sat/*.cmx>: for-pack(Msat_sat)
+<src/smt/*.cmx>: for-pack(Msat_smt)
 
 # more warnings
 <src/**/*.ml>: warn_K, warn_Y, warn_X

diff --git a/src/example/cc.ml b/src/example/cc.ml
diff --git a/src/example/cc.mli b/src/example/cc.mli
diff --git a/src/example/sig.mli b/src/example/sig.mli
diff --git a/src/main.ml b/src/main.ml
@@ -5,9 +5,10 @@ Copyright 2014 Simon Cruanes
 *)
 
 module F = Expr
-module T = Cnf.S
-module Smt = Smt.Make(struct end)
-module Mcsat = Mcsat.Make(struct end)
+module T = Msat_smt.Cnf.S
+module Sat = Msat_sat.Sat.Make(struct end)
+module Smt = Msat_smt.Smt.Make(struct end)
+module Mcsat = Msat_smt.Mcsat.Make(struct end)
 
 exception Incorrect_model
 exception Out_of_time
@@ -26,6 +27,7 @@ type sat_output =
   | Dot
 
 type solver =
+  | Sat
   | Smt
   | Mcsat
 
@@ -43,6 +45,7 @@ let output_list = [
   "dk", Dedukti;
 ]
 let solver_list = [
+  "sat", Sat;
   "smt", Smt;
   "mcsat", Mcsat;
 ]

diff --git a/src/msat.mlpack b/src/msat.mlpack
@@ -19,20 +19,11 @@ Mcsolver
 Solver_types
 
 # Backends
+Backend_intf
 Dot
 Dedukti
 
 # Auxiliary modules
 Res
 Tseitin
-
-# Sat/Smt modules
-Expr
-Cnf
-Sat
-Mcsat
-Cc
-Sig
-Smt
-Unionfind
-
+Hashcons
diff --git a/src/msat.odocl b/src/msat.odocl
@@ -13,20 +13,20 @@ solver/Tseitin_intf
 
 # Main modules
 core/Res
+core/Res_intf
 core/Internal
 core/External
 core/Solver_types
 
 solver/Solver
 solver/Mcsolver
 solver/Tseitin
+solver/Tseitin_intf
 
 # Backends
 backend/Dot
 backend/Dedukti
 backend/Backend_intf
 
-# Examples
-example/Sat
-example/Smt
-
+# Auxiliary
+util/Hashcons
diff --git a/src/msat_sat.mlpack b/src/msat_sat.mlpack
@@ -0,0 +1,2 @@
+Sat
+
diff --git a/src/msat_sat.odocl b/src/msat_sat.odocl
@@ -0,0 +1,3 @@
+
+smt/Sat
+
diff --git a/src/msat_smt.mlpack b/src/msat_smt.mlpack
@@ -0,0 +1,12 @@
+Cc
+Cnf
+Explanation
+Expr
+ID
+Literal
+Mcsat
+Smt
+Symbols
+Term
+Ty
+Unionfind
diff --git a/src/msat_smt.odocl b/src/msat_smt.odocl
@@ -0,0 +1,17 @@
+
+smt/Smt
+
+# support
+smt/Cc
+smt/Cnf
+smt/Explanation
+smt/Expr
+smt/ID
+smt/Sat
+smt/Literal
+smt/Mcsat
+smt/Symbols
+smt/Term
+smt/Ty
+smt/Unionfind
+
diff --git a/src/example/sat.ml → src/sat/sat.ml b/src/example/sat.ml → src/sat/sat.ml
@@ -4,6 +4,8 @@ Copyright 2014 Guillaume Bury
 Copyright 2014 Simon Cruanes
 *)
 
+open Msat
+
 module FI = Formula_intf
 
 module Fsat = struct