use jbuilder

arjunguha · Oct 25, 2017 · aa9a3e2 · aa9a3e2
1 parent b94d1b0
commit aa9a3e2
Show file tree

Hide file tree

Showing 21 changed files with 53 additions and 7,845 deletions.
diff --git a/.gitignore b/.gitignore
@@ -1,4 +1,6 @@
 *.native
 _build
 /setup.data
-/setup.log
+/setup.log
+.merlin
+smtlib.install
diff --git a/Makefile b/Makefile
@@ -1,41 +1,19 @@
-# OASIS_START
-# DO NOT EDIT (digest: a3c674b4239234cbbe53afe090018954)
-
-SETUP = ocaml setup.ml
-
-build: setup.data
-	$(SETUP) -build $(BUILDFLAGS)
-
-doc: setup.data build
-	$(SETUP) -doc $(DOCFLAGS)
-
-test: setup.data build
-	$(SETUP) -test $(TESTFLAGS)
-
 all:
-	$(SETUP) -all $(ALLFLAGS)
+	@jbuilder build @install @DEFAULT
 
-install: setup.data
-	$(SETUP) -install $(INSTALLFLAGS)
+install:
+	@jbuilder install
 
-uninstall: setup.data
-	$(SETUP) -uninstall $(UNINSTALLFLAGS)
+doc:
+	@jbuilder build @doc
 
-reinstall: setup.data
-	$(SETUP) -reinstall $(REINSTALLFLAGS)
+test:
+	@jbuilder runtest
 
 clean:
-	$(SETUP) -clean $(CLEANFLAGS)
-
-distclean:
-	$(SETUP) -distclean $(DISTCLEANFLAGS)
-
-setup.data:
-	$(SETUP) -configure $(CONFIGUREFLAGS)
-
-configure:
-	$(SETUP) -configure $(CONFIGUREFLAGS)
+	@jbuilder clean
 
-.PHONY: build doc test all install uninstall reinstall clean distclean configure
+uninstall:
+	@jbuilder uninstall
 
-# OASIS_STOP
+.PHONY: all install test clean uninstall
diff --git a/README.md b/README.md
diff --git a/_oasis b/_oasis
diff --git a/_tags b/_tags
diff --git a/configure b/configure
diff --git a/lib/META b/lib/META
diff --git a/lib/Smtlib.ml b/lib/Smtlib.ml
@@ -1,6 +1,6 @@
 open Sexplib.Std
 
-include Smtlib_syntax
+include Syntax
 
 type solver = { stdin : out_channel; stdout : in_channel; stdout_lexbuf : Lexing.lexbuf }
 
@@ -35,7 +35,7 @@ let write (solver : solver) (e : sexp) : unit =
   flush solver.stdin
 
 let read (solver : solver) : sexp =
-  Smtlib_parser.sexp Smtlib_lexer.token solver.stdout_lexbuf
+  Parser.sexp Lexer.token solver.stdout_lexbuf
 
 let command (solver : solver) (sexp : sexp) = write solver sexp; read solver
 
@@ -248,6 +248,11 @@ let maximize (solver : solver) (term : term) : unit =
 let minimize (solver : solver) (term : term) : unit =
   silent_command solver (SList ([SSymbol "minimize"; term_to_sexp term]))
 
+let read_objectives (solver : solver) : unit =
+  match read solver with
+  | SList [SSymbol "objectives"; SList l] -> ()
+  | s -> failwith ("unexpected result in optimized objective, got " ^ sexp_to_string s)
+
 let rec check_sat (solver : solver) : check_sat_result =
   let fail sexp  = failwith ("unexpected result from (check-sat), got " ^
                        sexp_to_string sexp) in

diff --git a/lib/Smtlib.mli b/lib/Smtlib.mli
@@ -77,6 +77,9 @@ val maximize : solver -> term -> unit
 (** [minimize solver e] runs the command [(minimize e)] *)
 val minimize : solver -> term -> unit
 
+(** [read_objectives solver] reads output of objective function printed after calls to [check_sat solver]  *)
+val read_objectives : solver -> unit
+
 (** [check_sat solver] runs the command [(check-sat)] *)
 val check_sat : solver -> check_sat_result
 
@@ -194,7 +197,7 @@ val bvnot : term -> term
 (** {1 Low-level interface} *)
 
 (** The variant of s-expressions used by SMT-LIB. *)
-type sexp = Smtlib_syntax.sexp =
+type sexp = Syntax.sexp =
   | SList of sexp list
   | SSymbol of string
   | SString of string

diff --git a/lib/doc.odocl b/lib/doc.odocl
diff --git a/lib/jbuild b/lib/jbuild
@@ -0,0 +1,12 @@
+(jbuild_version 1)
+
+(ocamllex
+  (lexer))
+
+(menhir
+  ((modules (parser))))
+
+(library
+  ((name smtlib)
+   (public_name smtlib)
+   (libraries (menhirLib ppx_deriving ppx_jane))))
diff --git a/lib/Smtlib_lexer.mll → lib/lexer.mll b/lib/Smtlib_lexer.mll → lib/lexer.mll
@@ -1,6 +1,6 @@
 {
   open Lexing
-  open Smtlib_parser
+  open Parser
 
   let parse_hex (str : string) : (int * int) =
     let len = (String.length str) - 2 in

diff --git a/lib/Smtlib_parser.mly → lib/parser.mly b/lib/Smtlib_parser.mly → lib/parser.mly
@@ -1,5 +1,5 @@
 %{
-open Smtlib_syntax
+open Syntax
 %}
 
 %token LPAREN RPAREN
@@ -11,7 +11,7 @@ open Smtlib_syntax
 %token EOF
 
 %start sexp
-%type <Smtlib_syntax.sexp> sexp
+%type <Syntax.sexp> sexp
 
 %%
 

diff --git a/lib/Smtlib_syntax.ml → lib/syntax.ml b/lib/Smtlib_syntax.ml → lib/syntax.ml
diff --git a/lib/Smtlib_syntax.mli → lib/syntax.mli b/lib/Smtlib_syntax.mli → lib/syntax.mli
diff --git a/lib/z3.mldylib b/lib/z3.mldylib
diff --git a/lib/z3.mllib b/lib/z3.mllib