Minor changes to make scripts. Since files got moved around, the libstp.a was broken...

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

diff --git a/Makefile b/Makefile
index 9b84ae47f1c04c304af5a284f772a6dcb51e826c..8f9931e873629c187b20cc061da2ba204a8b781b 100644 (file)
--- a/Makefile
+++ b/Makefile
@@ -18,13 +18,15 @@ HEADERS=$(SRC)/c_interface/*.h
 .PHONY: all
 all:
        $(MAKE) -C $(SRC)/AST
-       $(MAKE) -C $(SRC)/sat simp
+       $(MAKE) -C $(SRC)/sat core
+#      $(MAKE) -C $(SRC)/sat simp
+#      $(MAKE) -C $(SRC)/sat unsound
        $(MAKE) -C $(SRC)/simplifier
        $(MAKE) -C $(SRC)/bitvec
        $(MAKE) -C $(SRC)/c_interface
        $(MAKE) -C $(SRC)/constantbv
        $(MAKE) -C $(SRC)/parser
-       $(AR) rc libstp.a  $(SRC)/AST/*.o $(SRC)/sat/*.a $(SRC)/simplifier/*.o $(SRC)/bitvec/*.o $(SRC)/constantbv/*.o \
+       $(AR) rc libstp.a  $(SRC)/AST/*.o $(SRC)/AST/printer/*.o $(SRC)/sat/*.or $(SRC)/simplifier/*.o $(SRC)/bitvec/*.o $(SRC)/constantbv/*.o \
                           $(SRC)/c_interface/*.o $(SRC)/parser/let-funcs.o $(SRC)/parser/parseCVC.o $(SRC)/parser/lexCVC.o
        $(RANLIB) libstp.a
        @mkdir -p lib

diff --git a/scripts/Makefile.in b/scripts/Makefile.in
index 9b84ae47f1c04c304af5a284f772a6dcb51e826c..8f9931e873629c187b20cc061da2ba204a8b781b 100644 (file)
--- a/scripts/Makefile.in
+++ b/scripts/Makefile.in
@@ -18,13 +18,15 @@ HEADERS=$(SRC)/c_interface/*.h
 .PHONY: all
 all:
        $(MAKE) -C $(SRC)/AST
-       $(MAKE) -C $(SRC)/sat simp
+       $(MAKE) -C $(SRC)/sat core
+#      $(MAKE) -C $(SRC)/sat simp
+#      $(MAKE) -C $(SRC)/sat unsound
        $(MAKE) -C $(SRC)/simplifier
        $(MAKE) -C $(SRC)/bitvec
        $(MAKE) -C $(SRC)/c_interface
        $(MAKE) -C $(SRC)/constantbv
        $(MAKE) -C $(SRC)/parser
-       $(AR) rc libstp.a  $(SRC)/AST/*.o $(SRC)/sat/*.a $(SRC)/simplifier/*.o $(SRC)/bitvec/*.o $(SRC)/constantbv/*.o \
+       $(AR) rc libstp.a  $(SRC)/AST/*.o $(SRC)/AST/printer/*.o $(SRC)/sat/*.or $(SRC)/simplifier/*.o $(SRC)/bitvec/*.o $(SRC)/constantbv/*.o \
                           $(SRC)/c_interface/*.o $(SRC)/parser/let-funcs.o $(SRC)/parser/parseCVC.o $(SRC)/parser/lexCVC.o
        $(RANLIB) libstp.a
        @mkdir -p lib

diff --git a/src/AST/AST.h b/src/AST/AST.h
index 32746578ebc2f2e459a5b4150f8111f4c936f1e4..fb446addb1bfc5b267c5a3ad0c8832d319c2b1d8 100644 (file)
--- a/src/AST/AST.h
+++ b/src/AST/AST.h
@@ -32,8 +32,9 @@
 #include <algorithm>
 #include "ASTUtil.h"
 #include "ASTKind.h"
-//#include "../sat/core/Solver.h"
-#include "../sat/simp/SimpSolver.h"
+#include "../sat/core/Solver.h"
+//#include "../sat/simp/SimpSolver.h"
+//#include "../sat/unsound/UnsoundSimpSolver.h"
 #include "../sat/core/SolverTypes.h"
 #include <stdlib.h>
 #ifndef NATIVE_C_ARITH

diff --git a/src/AST/ASTKind.kinds b/src/AST/ASTKind.kinds
index 985ee6224c912c987605dbaaa63c05b2f11f1146..0257e96bf5ba6ea01f10636a9bbb5cb2f450cf1c 100644 (file)
--- a/src/AST/ASTKind.kinds
+++ b/src/AST/ASTKind.kinds
@@ -1,5 +1,5 @@
 #Please refer LICENSE FILE in the home directory for licensing information
-# name minkids maxkids cat1 cat2 ...
+# name minkids maxkids category1 category2
 Categories:    Term    Form
 
 # Leaf nodes.
@@ -60,6 +60,7 @@ NOR           1       -       Form
 XOR            1       -       Form
 IFF            1       -       Form
 IMPLIES                2       2       Form
+FOR            4       4       Form
 
 # array operations
 READ           2       2       Term

diff --git a/src/AST/ToSAT.cpp b/src/AST/ToSAT.cpp
index 94eaa5838f8459cf41c5079bee20986797f689d1..5d1d0bc80b2be725f5522bbc3f2b0fdc8ff9dc57 100644 (file)
--- a/src/AST/ToSAT.cpp
+++ b/src/AST/ToSAT.cpp
@@ -121,6 +121,7 @@ bool BeevMgr::toSATandSolve(MINISAT::Solver& newS, BeevMgr::ClauseList& cll)
        //PrintActivityLevels_Of_SATVars("Before SAT:",newS);
        //ChangeActivityLevels_Of_SATVars(newS);
        //PrintActivityLevels_Of_SATVars("Before SAT and after initial bias:",newS);
+       //newS.solve();
        newS.solve();
        //PrintActivityLevels_Of_SATVars("After SAT",newS);
 
@@ -1186,7 +1187,9 @@ int BeevMgr::TopLevelSATAux(const ASTNode& inputasserts)
 
        int res;
        //solver instantiated here
-       MINISAT::SimpSolver newS;
+       MINISAT::Solver newS;
+       //MINISAT::SimpSolver newS;
+       //MINISAT::UnsoundSimpSolver newS;
        if (arrayread_refinement_flag)
        {
                counterexample_checking_during_refinement = true;

diff --git a/src/parser/CVC.lex b/src/parser/CVC.lex
index de7f851db1a720927c81a2678c4ff273debab2f9..c515708897f9a7229b822a678468cc1dc80ff4e5 100644 (file)
--- a/src/parser/CVC.lex
+++ b/src/parser/CVC.lex
@@ -50,6 +50,7 @@ ANYTHING ({LETTER}|{DIGIT}|{OPCHAR})
 "NAND"          { return NAND_TOK;}
 "NOR"           { return NOR_TOK;}
 "NOT"           { return NOT_TOK; }
+"FOR"           { return FOR_TOK; }
 "OR"            { return OR_TOK; }
 "/="            { return NEQ_TOK; }
  ":="            { return ASSIGN_TOK;}

diff --git a/src/parser/CVC.y b/src/parser/CVC.y
index c58e17506a21a5e41f64c722b93a5ca1ad7eed61..c5801a319f73732d92bbe01c2453a49648a0efba 100644 (file)
--- a/src/parser/CVC.y
+++ b/src/parser/CVC.y
@@ -56,6 +56,7 @@ using namespace std;
 %token AND_TOK                 "AND"
 %token OR_TOK                  "OR"
 %token NOT_TOK                 "NOT"
+%token FOR_TOK                 "FOR"
 %token XOR_TOK                 "XOR"
 %token NAND_TOK                "NAND"
 %token NOR_TOK                 "NOR"
@@ -440,6 +441,22 @@ Formula            :     '(' Formula ')' { $$ = $2; }
                         delete $1;
                         delete $3;
                       }
+                |      FOR_TOK '(' Formula ';' Formula ';' Formula ')' '{' Formula '}'
+                       {
+                        //Allows a compact representation of
+                        //parameterized set of formulas
+                        //
+                        //$1 is the initialization (this is an AND of
+                        //formulas of the form var = constant)
+                        //
+                        //$2 is the constant bounding (this is an AND
+                        //of formulas of the form var < constant).
+                        //
+                        //$3 is the increment (this is an AND of
+                        //formulas of the form var = var + constant).
+                        //
+                        //$4 is the parameterized formula
+                      }
                |      NOT_TOK Formula 
                        {
                         $$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateNode(BEEV::NOT, *$2));

diff --git a/src/parser/Makefile b/src/parser/Makefile
index 43d99eec888bbac4d6b047954411bd9a8fec46a9..e3e086a184b66e2ddd448ea3421cc6d0c7869d4f 100644 (file)
--- a/src/parser/Makefile
+++ b/src/parser/Makefile
@@ -5,8 +5,9 @@ YACC=bison -d -y --debug -v
 
 SRCS = lexCVC.cpp parseCVC.cpp parseSMT.cpp lexSMT.cpp let-funcs.cpp main.cpp
 OBJS = $(SRCS:.cpp=.o)
-LIBS = -L../AST -last -L../sat/core -L../sat/simp -lminisat -L../simplifier -lsimplifier -L../bitvec -lconsteval -L../constantbv -lconstantbv
-CFLAGS += -I../sat/mtl -I../sat/core -I../sat/simp
+LIBS = -L../AST -last -L../sat -lminisat -L../simplifier -lsimplifier -L../bitvec -lconsteval -L../constantbv -lconstantbv
+#CFLAGS += -I../sat/mtl -I../sat/core -I../sat/simp
+CFLAGS += -I../sat/mtl -I../sat/core  -I../sat/unsound
 
 all: parseSMT.cpp lexSMT.cpp parseCVC.cpp lexCVC.cpp let-funcs.cpp parser parseCVC.o lexCVC.o let-funcs.o 
 

diff --git a/src/sat/Makefile b/src/sat/Makefile
index a6aa9e6dbd301d794d5710275a947a6814b2d87f..d270dc86e28d5927715821a4bb58a171e80442a0 100644 (file)
--- a/src/sat/Makefile
+++ b/src/sat/Makefile
@@ -4,7 +4,6 @@ core:
 .PHONY: simp
 simp:
        $(MAKE) -C simp lib all
-
 .PHONY: unsound
 unsound:
        $(MAKE) -C unsound lib all
@@ -14,4 +13,4 @@ clean:
        rm -rf *~ libminisat.a
        $(MAKE) -C core clean
        $(MAKE) -C simp clean
-       #$(MAKE) -C unsound clean
+       $(MAKE) -C unsound clean

diff --git a/src/sat/core/Makefile b/src/sat/core/Makefile
index ea850508b7002e981a57bca4c8585a38c8178f3a..aa1500255fbb503ec8263c3fb57277561b83c135 100644 (file)
--- a/src/sat/core/Makefile
+++ b/src/sat/core/Makefile
@@ -7,4 +7,6 @@ LFLAGS    = -lz
 
 include ../mtl/template.mk
 all:
+       ranlib libminisat.a
+       cp *.or ../
        cp libminisat.a ../
\ No newline at end of file

diff --git a/src/sat/mtl/template.mk b/src/sat/mtl/template.mk
index e60f2fbfa919f8b963f527f624038bf86bdcb5db..4c27893b2ab18b55b8b6d4893fda393d2d8d5235 100644 (file)
--- a/src/sat/mtl/template.mk
+++ b/src/sat/mtl/template.mk
@@ -72,7 +72,7 @@ $(EXEC) $(EXEC)_profile $(EXEC)_debug $(EXEC)_release $(EXEC)_static:
 lib$(LIB).a lib$(LIB)d.a lib$(LIB)p.a:
        @echo Library: "$@ ( $^ )"
        @rm -f $@
-       @ar cq $@ $^
+       @ar cq $@ $^    
 
 ## Clean rule
 clean:

diff --git a/src/sat/simp/Makefile b/src/sat/simp/Makefile
index 26974d1ec4c68958345861b1f105c513f7a1efff..78c93ecb252598721fe26c115d2a47e3816713c3 100644 (file)
--- a/src/sat/simp/Makefile
+++ b/src/sat/simp/Makefile
@@ -10,4 +10,6 @@ COBJS     = $(addsuffix .o, $(basename $(CSRCS))) $(CORE)/Solver.o
 
 include ../mtl/template.mk
 all:
-       cp libminisat.a ../
\ No newline at end of file
+       ranlib libminisat.a
+       cp *.o ../
+       cp libminisat.a ../

diff --git a/src/simplifier/simplifier.cpp b/src/simplifier/simplifier.cpp
index 5d7570801b6a44163450ad2fc21f54a1eaa96833..d6e9ea9be8f4966a89b37894f292a247f621f56a 100644 (file)
--- a/src/simplifier/simplifier.cpp
+++ b/src/simplifier/simplifier.cpp
@@ -140,7 +140,7 @@ int BeevMgr::TermOrder(const ASTNode& a, const ASTNode& b)
        //a is of the form var, and b is const
        if ((k1 == READ && a[0].GetKind() == SYMBOL && a[1].GetKind() == BVCONST && 
             (k2 == BVCONST)))
-//           || 
+             // || 
 //           k2 == READ && b[0].GetKind() == SYMBOL && b[1].GetKind() == BVCONST)))
                return 1;
 

diff --git a/tests/c-api-tests/array-cvcl-02.c b/tests/c-api-tests/array-cvcl-02.c
index 2855671e5071bd93d6d677da4a692dfa28ef6533..18d4d2435a6f84c5a53e56b527b8dac6245a244f 100644 (file)
--- a/tests/c-api-tests/array-cvcl-02.c
+++ b/tests/c-api-tests/array-cvcl-02.c
@@ -27,8 +27,9 @@ int main() {
   Expr a_of_i = vc_bvSignExtend(vc,
                                vc_readExpr(vc,cvcl_array,i32),
                                32);  
-  Expr a_of_i_eq_11 = vc_eqExpr(vc, a_of_i,
-                               vc_bvConstExprFromInt(vc, 32, 11));
+  Expr a_of_i_eq_11 = vc_eqExpr(vc, 
+                               vc_bvConcatExpr(vc,i32,a_of_i),
+                               vc_bvConstExprFromInt(vc, 64, 11));
  
   vc_assertFormula(vc, in_bounds);
   vc_assertFormula(vc, a_of_i_eq_11);