Introduced a C API regression option 'make regress_c_api'. Only one test fails: due...

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@153 e59a4935-1847-0410-ae03-e826735625c1

diff --git a/Makefile b/Makefile
index 24ddc7c22f2a16cdd9b433bef436f8a1837c31c9..7294e80460f19eaf4bb13e5b8c6a274d1c150ff8 100644 (file)
--- a/Makefile
+++ b/Makefile
@@ -77,8 +77,8 @@ REGRESS_LOG = `date +%Y-%m-%d`"-regress.log"
 PROGNAME=bin/stp
 ALL_OPTIONS= -l $(REGRESS_LEVEL) $(PROGNAME) $(REGRESS_TESTS)
 
-.PHONY: regress
-regress:
+.PHONY: regressall
+regressall:
        @echo "*********************************************************" \
           | tee -a $(REGRESS_LOG)
        @echo "Starting tests at" `date` | tee -a $(REGRESS_LOG)
@@ -126,18 +126,25 @@ regress_smt:
        @echo "*********************************************************" \
           | tee -a $(REGRESS_LOG)
 
-
-.PHONY: regressall
-regressall:
-       $(MAKE) regress
+.PHONY: regress_c_api
+regress_c_api:
+       @echo "*********************************************************" \
+          | tee -a $(REGRESS_LOG)
+       @echo "Starting tests at" `date` | tee -a $(REGRESS_LOG)
+       @echo "*********************************************************" \
+          | tee -a $(REGRESS_LOG)
+       $(MAKE) -C tests/c-api-tests 2>&1 | tee -a $(REGRESS_LOG); [ $${PIPESTATUS[0]} -eq 0 ]
+       @echo "*********************************************************" \
+          | tee -a $(REGRESS_LOG)
+       @echo "Output is saved in $(REGRESS_LOG)" | tee -a $(REGRESS_LOG)
+       @echo "*********************************************************" \
+          | tee -a $(REGRESS_LOG)
 
 GRIND_LOG = `date +%Y-%m-%d`"-grind.log"
 GRINDPROG = valgrind --leak-check=full --undef-value-errors=no
 GRIND_TAR  = $(BIN_DIR)/stp -d
 GRIND_CALL = -vc "$(GRINDPROG) $(GRIND_TAR)" 
 GRIND_OPTIONS = -l $(REGRESS_LEVEL) -rt $(GRIND_CALL) $(REGRESS_TESTS)
-
-
 .PHONY: grind
 grind:
 

diff --git a/scripts/Makefile.in b/scripts/Makefile.in
index 24ddc7c22f2a16cdd9b433bef436f8a1837c31c9..7294e80460f19eaf4bb13e5b8c6a274d1c150ff8 100644 (file)
--- a/scripts/Makefile.in
+++ b/scripts/Makefile.in
@@ -77,8 +77,8 @@ REGRESS_LOG = `date +%Y-%m-%d`"-regress.log"
 PROGNAME=bin/stp
 ALL_OPTIONS= -l $(REGRESS_LEVEL) $(PROGNAME) $(REGRESS_TESTS)
 
-.PHONY: regress
-regress:
+.PHONY: regressall
+regressall:
        @echo "*********************************************************" \
           | tee -a $(REGRESS_LOG)
        @echo "Starting tests at" `date` | tee -a $(REGRESS_LOG)
@@ -126,18 +126,25 @@ regress_smt:
        @echo "*********************************************************" \
           | tee -a $(REGRESS_LOG)
 
-
-.PHONY: regressall
-regressall:
-       $(MAKE) regress
+.PHONY: regress_c_api
+regress_c_api:
+       @echo "*********************************************************" \
+          | tee -a $(REGRESS_LOG)
+       @echo "Starting tests at" `date` | tee -a $(REGRESS_LOG)
+       @echo "*********************************************************" \
+          | tee -a $(REGRESS_LOG)
+       $(MAKE) -C tests/c-api-tests 2>&1 | tee -a $(REGRESS_LOG); [ $${PIPESTATUS[0]} -eq 0 ]
+       @echo "*********************************************************" \
+          | tee -a $(REGRESS_LOG)
+       @echo "Output is saved in $(REGRESS_LOG)" | tee -a $(REGRESS_LOG)
+       @echo "*********************************************************" \
+          | tee -a $(REGRESS_LOG)
 
 GRIND_LOG = `date +%Y-%m-%d`"-grind.log"
 GRINDPROG = valgrind --leak-check=full --undef-value-errors=no
 GRIND_TAR  = $(BIN_DIR)/stp -d
 GRIND_CALL = -vc "$(GRINDPROG) $(GRIND_TAR)" 
 GRIND_OPTIONS = -l $(REGRESS_LEVEL) -rt $(GRIND_CALL) $(REGRESS_TESTS)
-
-
 .PHONY: grind
 grind:
 

diff --git a/src/c_interface/c_interface.h b/src/c_interface/c_interface.h
index 04f2837ac59fbb5f177eedbee8968a18e85b1157..78ebf4a220a2c55372047d5020e168e23518b7ed 100644 (file)
--- a/src/c_interface/c_interface.h
+++ b/src/c_interface/c_interface.h
@@ -144,7 +144,7 @@ extern "C" {
   //! Prints asserts to stdout. The flag simplify_print must be set to
   //"1" if you wish simplification to occur dring printing. It must be
   //set to "0" otherwise
-  void vc_printAsserts(VC vc, int simplify_print);
+  void vc_printAsserts(VC vc, int simplify_print=0);
 
   //! Prints the state of the query to malloc'd buffer '*buf' and
   //stores ! the length of the buffer to '*len'.  It is the

diff --git a/tests/c-api-tests/Makefile b/tests/c-api-tests/Makefile
new file mode 100644 (file)
index 0000000..a5d7040
--- /dev/null
+++ b/tests/c-api-tests/Makefile
@@ -0,0 +1,44 @@
+
+all:
+       g++ -DEXT_HASH_MAP array-cvcl-02.c -I../../src/c_interface -L../../lib -lstp -o a0.out
+       ./a0.out
+       g++ -DEXT_HASH_MAP b4-c.c -I../../src/c_interface -L../../lib -lstp -o a1.out
+       ./a1.out
+       g++ -DEXT_HASH_MAP b4-c2.c -I../../src/c_interface -L../../lib -lstp -o a2.out
+       ./a2.out
+       g++ -DEXT_HASH_MAP getbvunsignedlonglong-check.c -I../../src/c_interface -L../../lib -lstp -o a3.out
+       ./a3.out
+       g++ -DEXT_HASH_MAP multiple-queries.c -I../../src/c_interface -L../../lib -lstp -o a4.out
+       ./a4.out
+       g++ -DEXT_HASH_MAP parsefile-using-cinterface.c -I../../src/c_interface -L../../lib -lstp -o a5.out
+       ./a5.out
+       g++ -DEXT_HASH_MAP print.c -I../../src/c_interface -L../../lib -lstp -o a6.out
+       ./a6.out
+       g++ -DEXT_HASH_MAP push-pop-1.c -I../../src/c_interface -L../../lib -lstp -o a7.out
+       ./a7.out
+       g++ -DEXT_HASH_MAP sbvmod.c -I../../src/c_interface -L../../lib -lstp -o a8.out
+       ./a8.out
+       g++ -DEXT_HASH_MAP simplify.c -I../../src/c_interface -L../../lib -lstp -o a9.out
+       ./a9.out
+       g++ -DEXT_HASH_MAP simplify1.c -I../../src/c_interface -L../../lib -lstp -o a10.out
+       ./a10.out
+       g++ -DEXT_HASH_MAP squares-leak.c -I../../src/c_interface -L../../lib -lstp -o a11.out
+       ./a11.out
+       g++ -DEXT_HASH_MAP stp-counterex.c -I../../src/c_interface -L../../lib -lstp -o a12.out
+       ./a12.out
+       g++ -DEXT_HASH_MAP stp-div-001.c -I../../src/c_interface -L../../lib -lstp -o a13.out
+       ./a13.out
+       g++ -DEXT_HASH_MAP stpcheck.c -I../../src/c_interface -L../../lib -lstp -o a14.out
+       ./a14.out
+       g++ -DEXT_HASH_MAP x.c -I../../src/c_interface -L../../lib -lstp -o a15.out
+       ./a15.out
+       g++ -DEXT_HASH_MAP y.c -I../../src/c_interface -L../../lib -lstp -o a16.out
+       ./a16.out
+       g++ -DEXT_HASH_MAP push-pop.c -I../../src/c_interface -L../../lib -lstp -o a17.out
+       ./a17.out
+       g++ -DEXT_HASH_MAP cvc-to-c.cpp -I../../src/c_interface -L../../lib -lstp -o a18.out
+       ./a18.out ./t.cvc
+
+
+clean:
+       rm -rf *~ *.out
\ No newline at end of file

diff --git a/tests/c-api-tests/t.cvc b/tests/c-api-tests/t.cvc
index 0a6f9f4f0979bf740254a159564c34d98d872142..0736f426393cdf611312bac38e777ba387b00b43 100644 (file)
--- a/tests/c-api-tests/t.cvc
+++ b/tests/c-api-tests/t.cvc
@@ -130,3 +130,4 @@ ASSERT( NOT(0hex00 = arr666[0hex00000003]
  );
 ASSERT( 0hex00 = arr666[0hex00000004]
  );
+QUERY FALSE;
\ No newline at end of file