3rdparty

2 files changed, 30 insertions, 26 deletions

diff --git a/src/versions/native/Make b/src/versions/native/Make
index f45eb72..f28d1c9 100644
--- a/src/versions/native/Make
+++ b/src/versions/native/Make
@@ -17,7 +17,7 @@
 ##    change CMXSFILES into CMXS and add the same block for CMXA and VCMXS. ##
 ## 4) Change the "install" target: change CMOFILES into CMXFILES.     ##
 ## 5) Add to the "clean" target:                                      ##
-##    - rm -f NSMTCoq* cnf/NSMTCoq* euf/NSMTCoq* lia/NSMTCoq* spl/NSMTCoq* ../unit-tests/NSMTCoq* ../unit-tests/*.vo ../unit-tests/*.zlog ../unit-tests/*.vtlog verit/veritParser.mli verit/veritParser.ml verit/veritLexer.ml smtlib2/smtlib2_parse.mli smtlib2/smtlib2_parse.ml smtlib2/smtlib2_lex.ml smtlib2/sExprParser.mli smtlib2/sExprParser.ml smtlib2/sExprLexer.ml lfsc/lfscLexer.ml lfsc/lfscParser.ml lfsc/lfscParser.mli trace/smtcoq.a ##
+##    - rm -f NSMTCoq* cnf/NSMTCoq* euf/NSMTCoq* lia/NSMTCoq* spl/NSMTCoq* ../unit-tests/NSMTCoq* ../unit-tests/*.vo ../unit-tests/*.zlog ../unit-tests/*.vtlog verit/veritParser.mli verit/veritParser.ml verit/veritLexer.ml ../3rdparty/alt-ergo/smtlib2_parse.mli ../3rdparty/alt-ergo/smtlib2_parse.ml ../3rdparty/alt-ergo/smtlib2_lex.ml smtlib2/sExprParser.mli smtlib2/sExprParser.ml smtlib2/sExprLexer.ml lfsc/lfscLexer.ml lfsc/lfscParser.ml lfsc/lfscParser.mli trace/smtcoq.a ##
 ########################################################################
 
 
@@ -35,6 +35,7 @@
 -I verit
 -I zchaff
 -I versions/native
+-I ../3rdparty/alt-ergo
 
 
 -custom "cd ../unit-tests; make vernac" "" "test"
@@ -43,9 +44,9 @@
 
 -custom "$(CAMLLEX) $<" "%.mll" "%.ml"
 -custom "$(CAMLYACC) $<" "%.mly" "%.ml %.mli"
--custom "" "verit/veritParser.ml verit/veritLexer.ml smtlib2/smtlib2_parse.ml smtlib2/smtlib2_lex.ml smtlib2/sExprParser.ml smtlib2/sExprLexer.ml lfsc/lfscParser.ml lfsc/lfscLexer.ml" "ml"
+-custom "" "verit/veritParser.ml verit/veritLexer.ml ../3rdparty/alt-ergo/smtlib2_parse.ml ../3rdparty/alt-ergo/smtlib2_lex.ml smtlib2/sExprParser.ml smtlib2/sExprLexer.ml lfsc/lfscParser.ml lfsc/lfscLexer.ml" "ml"
 
--custom "$(CAMLOPTLINK) $(ZFLAGS) -a -o $@ $^" "versions/native/structures.cmx trace/smtMisc.cmx trace/coqTerms.cmx trace/smtBtype.cmx trace/smtForm.cmx trace/smtCertif.cmx trace/smtTrace.cmx trace/smtCnf.cmx trace/satAtom.cmx trace/smtAtom.cmx zchaff/satParser.cmx zchaff/zchaffParser.cmx zchaff/cnfParser.cmx zchaff/zchaff.cmx smtlib2/smtlib2_util.cmx smtlib2/smtlib2_ast.cmx smtlib2/smtlib2_parse.cmx smtlib2/smtlib2_lex.cmx smtlib2/sExpr.cmx smtlib2/sExprParser.cmx smtlib2/sExprLexer.cmx smtlib2/smtlib2_solver.cmx lia/lia.cmx verit/veritSyntax.cmx verit/veritParser.cmx verit/veritLexer.cmx lfsc/shashcons.cmx lfsc/hstring.cmx lfsc/type.cmx lfsc/ast.cmx lfsc/builtin.cmx lfsc/tosmtcoq.cmx lfsc/converter.cmx lfsc/lfscParser.cmx lfsc/lfscLexer.cmx smtlib2/smtlib2_genConstr.cmx trace/smtCommands.cmx verit/verit.cmx lfsc/lfsc.cmx smtcoq_plugin.cmx" "$(CMXA)"
+-custom "$(CAMLOPTLINK) $(ZFLAGS) -a -o $@ $^" "versions/native/structures.cmx trace/smtMisc.cmx trace/coqTerms.cmx trace/smtBtype.cmx trace/smtForm.cmx trace/smtCertif.cmx trace/smtTrace.cmx trace/smtCnf.cmx trace/satAtom.cmx trace/smtAtom.cmx zchaff/satParser.cmx zchaff/zchaffParser.cmx zchaff/cnfParser.cmx zchaff/zchaff.cmx ../3rdparty/alt-ergo/smtlib2_util.cmx ../3rdparty/alt-ergo/smtlib2_ast.cmx ../3rdparty/alt-ergo/smtlib2_parse.cmx ../3rdparty/alt-ergo/smtlib2_lex.cmx smtlib2/sExpr.cmx smtlib2/sExprParser.cmx smtlib2/sExprLexer.cmx smtlib2/smtlib2_solver.cmx lia/lia.cmx verit/veritSyntax.cmx verit/veritParser.cmx verit/veritLexer.cmx lfsc/shashcons.cmx lfsc/hstring.cmx lfsc/type.cmx lfsc/ast.cmx lfsc/builtin.cmx lfsc/tosmtcoq.cmx lfsc/converter.cmx lfsc/lfscParser.cmx lfsc/lfscLexer.cmx smtlib2/smtlib2_genConstr.cmx trace/smtCommands.cmx verit/verit.cmx lfsc/lfsc.cmx smtcoq_plugin.cmx" "$(CMXA)"
 -custom "$(CAMLOPTLINK) $(ZFLAGS) -o $@ -linkall -shared $^" "$(CMXA)" "$(CMXS)"
 
 CMXA = smtcoq.cmxa
@@ -88,16 +89,17 @@ trace/smtMisc.mli
 trace/smtTrace.ml
 trace/smtTrace.mli
 
-smtlib2/smtlib2_parse.ml
-smtlib2/smtlib2_parse.mli
-smtlib2/smtlib2_lex.ml
-smtlib2/smtlib2_lex.mli
-smtlib2/smtlib2_ast.ml
-smtlib2/smtlib2_ast.mli
+../3rdparty/alt-ergo/smtlib2_parse.ml
+../3rdparty/alt-ergo/smtlib2_parse.mli
+../3rdparty/alt-ergo/smtlib2_lex.ml
+../3rdparty/alt-ergo/smtlib2_lex.mli
+../3rdparty/alt-ergo/smtlib2_ast.ml
+../3rdparty/alt-ergo/smtlib2_ast.mli
+../3rdparty/alt-ergo/smtlib2_util.ml
+../3rdparty/alt-ergo/smtlib2_util.mli
+
 smtlib2/smtlib2_genConstr.ml
 smtlib2/smtlib2_genConstr.mli
-smtlib2/smtlib2_util.ml
-smtlib2/smtlib2_util.mli
 smtlib2/sExprParser.ml
 smtlib2/sExprParser.mli
 smtlib2/sExprLexer.ml
diff --git a/src/versions/native/Makefile b/src/versions/native/Makefile
index 3c6bf30..3f0d0f6 100644
--- a/src/versions/native/Makefile
+++ b/src/versions/native/Makefile
@@ -39,7 +39,8 @@ $(call includecmdwithout@,$(COQBIN)coqtop -config)
 #                        #
 ##########################
 
-OCAMLLIBS?=-I versions/native\
+OCAMLLIBS?=-I ../3rdparty/alt-ergo\
+  -I versions/native\
   -I zchaff\
   -I verit\
   -I trace\
@@ -51,7 +52,8 @@ OCAMLLIBS?=-I versions/native\
   -I array\
   -I classes\
   -I bva
-COQLIBS?=-I versions/native\
+COQLIBS?=-I ../3rdparty/alt-ergo\
+  -I versions/native\
   -I zchaff\
   -I verit\
   -I trace\
@@ -206,11 +208,11 @@ MLFILES:=lia/lia.ml\
   smtlib2/sExpr.ml\
   smtlib2/sExprLexer.ml\
   smtlib2/sExprParser.ml\
-  smtlib2/smtlib2_util.ml\
   smtlib2/smtlib2_genConstr.ml\
-  smtlib2/smtlib2_ast.ml\
-  smtlib2/smtlib2_lex.ml\
-  smtlib2/smtlib2_parse.ml\
+  ../3rdparty/alt-ergo/smtlib2_util.ml\
+  ../3rdparty/alt-ergo/smtlib2_ast.ml\
+  ../3rdparty/alt-ergo/smtlib2_lex.ml\
+  ../3rdparty/alt-ergo/smtlib2_parse.ml\
   trace/smtTrace.ml\
   trace/smtMisc.ml\
   trace/smtForm.ml\
@@ -243,11 +245,11 @@ MLIFILES:=lia/lia.mli\
   smtlib2/smtlib2_solver.mli\
   smtlib2/sExpr.mli\
   smtlib2/sExprParser.mli\
-  smtlib2/smtlib2_util.mli\
   smtlib2/smtlib2_genConstr.mli\
-  smtlib2/smtlib2_ast.mli\
-  smtlib2/smtlib2_lex.mli\
-  smtlib2/smtlib2_parse.mli\
+  ../3rdparty/alt-ergo/smtlib2_util.mli\
+  ../3rdparty/alt-ergo/smtlib2_ast.mli\
+  ../3rdparty/alt-ergo/smtlib2_lex.mli\
+  ../3rdparty/alt-ergo/smtlib2_parse.mli\
   trace/smtTrace.mli\
   trace/smtMisc.mli\
   trace/smtForm.mli\
@@ -327,10 +329,10 @@ beautify: $(VFILES:=.beautified)
 $(CMXS): $(CMXA)
 	$(CAMLOPTLINK) $(ZFLAGS) -o $@ -linkall -shared $^
 
-$(CMXA): versions/native/structures.cmx trace/smtMisc.cmx trace/coqTerms.cmx trace/smtBtype.cmx trace/smtForm.cmx trace/smtCertif.cmx trace/smtTrace.cmx trace/smtCnf.cmx trace/satAtom.cmx trace/smtAtom.cmx zchaff/satParser.cmx zchaff/zchaffParser.cmx zchaff/cnfParser.cmx zchaff/zchaff.cmx smtlib2/smtlib2_util.cmx smtlib2/smtlib2_ast.cmx smtlib2/smtlib2_parse.cmx smtlib2/smtlib2_lex.cmx smtlib2/sExpr.cmx smtlib2/sExprParser.cmx smtlib2/sExprLexer.cmx smtlib2/smtlib2_solver.cmx lia/lia.cmx verit/veritSyntax.cmx verit/veritParser.cmx verit/veritLexer.cmx lfsc/shashcons.cmx lfsc/hstring.cmx lfsc/type.cmx lfsc/ast.cmx lfsc/builtin.cmx lfsc/tosmtcoq.cmx lfsc/converter.cmx lfsc/lfscParser.cmx lfsc/lfscLexer.cmx smtlib2/smtlib2_genConstr.cmx trace/smtCommands.cmx verit/verit.cmx lfsc/lfsc.cmx smtcoq_plugin.cmx
+$(CMXA): versions/native/structures.cmx trace/smtMisc.cmx trace/coqTerms.cmx trace/smtBtype.cmx trace/smtForm.cmx trace/smtCertif.cmx trace/smtTrace.cmx trace/smtCnf.cmx trace/satAtom.cmx trace/smtAtom.cmx zchaff/satParser.cmx zchaff/zchaffParser.cmx zchaff/cnfParser.cmx zchaff/zchaff.cmx ../3rdparty/alt-ergo/smtlib2_util.cmx ../3rdparty/alt-ergo/smtlib2_ast.cmx ../3rdparty/alt-ergo/smtlib2_parse.cmx ../3rdparty/alt-ergo/smtlib2_lex.cmx smtlib2/sExpr.cmx smtlib2/sExprParser.cmx smtlib2/sExprLexer.cmx smtlib2/smtlib2_solver.cmx lia/lia.cmx verit/veritSyntax.cmx verit/veritParser.cmx verit/veritLexer.cmx lfsc/shashcons.cmx lfsc/hstring.cmx lfsc/type.cmx lfsc/ast.cmx lfsc/builtin.cmx lfsc/tosmtcoq.cmx lfsc/converter.cmx lfsc/lfscParser.cmx lfsc/lfscLexer.cmx smtlib2/smtlib2_genConstr.cmx trace/smtCommands.cmx verit/verit.cmx lfsc/lfsc.cmx smtcoq_plugin.cmx
 	$(CAMLOPTLINK) $(ZFLAGS) -a -o $@ $^
 
-ml: verit/veritParser.ml verit/veritLexer.ml smtlib2/smtlib2_parse.ml smtlib2/smtlib2_lex.ml smtlib2/sExprParser.ml smtlib2/sExprLexer.ml lfsc/lfscParser.ml lfsc/lfscLexer.ml
+ml: verit/veritParser.ml verit/veritLexer.ml ../3rdparty/alt-ergo/smtlib2_parse.ml ../3rdparty/alt-ergo/smtlib2_lex.ml smtlib2/sExprParser.ml smtlib2/sExprLexer.ml lfsc/lfscParser.ml lfsc/lfscLexer.ml
 
 
 %.ml %.mli: %.mly
@@ -368,11 +370,11 @@ install-natdynlink:
 	 install -d `dirname $(DSTROOT)$(COQLIBINSTALL)/SMTCoq/$$i`; \
 	 install -m 0644 $$i $(DSTROOT)$(COQLIBINSTALL)/SMTCoq/$$i; \
 	done
-	for i in $(CMXA); do \
+	for i in $(VCMXS); do \
 	 install -d `dirname $(DSTROOT)$(COQLIBINSTALL)/SMTCoq/$$i`; \
 	 install -m 0644 $$i $(DSTROOT)$(COQLIBINSTALL)/SMTCoq/$$i; \
 	done
-	for i in $(VCMXS); do \
+	for i in $(CMXA); do \
 	 install -d `dirname $(DSTROOT)$(COQLIBINSTALL)/SMTCoq/$$i`; \
 	 install -m 0644 $$i $(DSTROOT)$(COQLIBINSTALL)/SMTCoq/$$i; \
 	done
@@ -417,7 +419,7 @@ clean:
 	- rm -rf vtest
 	- rm -rf ztest
 	- rm -rf test
-	- rm -f NSMTCoq* cnf/NSMTCoq* euf/NSMTCoq* lia/NSMTCoq* spl/NSMTCoq* ../unit-tests/NSMTCoq* ../unit-tests/*.vo ../unit-tests/*.zlog ../unit-tests/*.vtlog verit/veritParser.mli verit/veritParser.ml verit/veritLexer.ml smtlib2/smtlib2_parse.mli smtlib2/smtlib2_parse.ml smtlib2/smtlib2_lex.ml smtlib2/sExprParser.mli smtlib2/sExprParser.ml smtlib2/sExprLexer.ml lfsc/lfscLexer.ml lfsc/lfscParser.ml lfsc/lfscParser.mli trace/smtcoq.a
+	- rm -f NSMTCoq* cnf/NSMTCoq* euf/NSMTCoq* lia/NSMTCoq* spl/NSMTCoq* ../unit-tests/NSMTCoq* ../unit-tests/*.vo ../unit-tests/*.zlog ../unit-tests/*.vtlog verit/veritParser.mli verit/veritParser.ml verit/veritLexer.ml ../3rdparty/alt-ergo/smtlib2_parse.mli ../3rdparty/alt-ergo/smtlib2_parse.ml ../3rdparty/alt-ergo/smtlib2_lex.ml smtlib2/sExprParser.mli smtlib2/sExprParser.ml smtlib2/sExprLexer.ml lfsc/lfscLexer.ml lfsc/lfscParser.ml lfsc/lfscParser.mli trace/smtcoq.a
 
 archclean:
 	rm -f *.cmx *.o