minor changes

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

diff --git a/Makefile.common b/Makefile.common
index fcc665a35d37745106769a0c2f9a5db07d0ae652..56c7f6904b74399521a050fce13b7cd60a71e29c 100644 (file)
--- a/Makefile.common
+++ b/Makefile.common
@@ -43,7 +43,8 @@ else
   CFLAGS = $(CFLAGS_BASE)
 endif
 
-CXXFLAGS = $(CFLAGS) -Wall -Wextra -DEXT_HASH_MAP -Wno-deprecated
+#CXXFLAGS = $(CFLAGS) -Wall -Wextra -DEXT_HASH_MAP -Wno-deprecated
+CXXFLAGS = $(CFLAGS) -Wextra -DEXT_HASH_MAP -Wno-deprecated
 #CXXFLAGS = $(CFLAGS) -Wall -DTR1_UNORDERED_MAP
 #CXXFLAGS = $(CFLAGS) -Wall 
 #LDFLAGS= -lstdc++

diff --git a/configure b/configure
index f794a86691cb2b168bfa0fa30f6fbf6fdf4affee..016a02d1831215f230b4d31cdfef0e0b1ec84b66 100755 (executable)
--- a/configure
+++ b/configure
@@ -32,20 +32,20 @@ while [ $# -gt 0 ]; do
 done
 
 
-echo "PREFIX=$PREFIX" > config.info
+echo "PREFIX=$PREFIX" > make-scripts/config.info
 echo "Setting prefix to... $PREFIX"
 if [ $CXX ]
-then echo "CXX=$CXX" >> config.info
+then echo "CXX=$CXX" >> make-scripts/config.info
 export CXX="$CXX"
 echo "Setting CXX to... $CXX"
 fi
 
 if [ ! -d $PREFIX/include ]
-then mkdir $PREFIX/include
+then mkdir -p $PREFIX/include
 fi
 
 if [ ! -d $PREFIX/bin ]
-then mkdir $PREFIX/bin
+then mkdir -p $PREFIX/bin
 fi
 
 if [ ! -d $PREFIX/lib ]
@@ -57,7 +57,7 @@ then mkdir $PREFIX/include/stp
 fi
 
 echo "STP is configured successfully."
-cp Makefile.in Makefile
+cp make-scripts/Makefile.in Makefile
 
 echo
 echo "Type 'make' to compile STP."

diff --git a/Makefile.in b/make-scripts/Makefile.in
similarity index 99%
rename from Makefile.in
rename to make-scripts/Makefile.in
index e154e344f306ebd32fc2b6cbb07231c2ad97872a..9be6b1d2ccc23d2a173c1ea868c24efab7b8ff8c 100644 (file)
--- a/Makefile.in
+++ b/make-scripts/Makefile.in
@@ -4,7 +4,7 @@
  # To make in optimized mode, type 'make "OPTIMIZE=-O3" 
 
 
-include Makefile.common config.info
+include Makefile.common make-scripts/config.info
 
 BIN_DIR=$(PREFIX)/bin
 LIB_DIR=$(PREFIX)/lib

diff --git a/make-scripts/config.info b/make-scripts/config.info
new file mode 100644 (file)
index 0000000..a67a797
--- /dev/null
+++ b/make-scripts/config.info
@@ -0,0 +1 @@
+PREFIX=/usr/local

diff --git a/src/AST/ToSAT.cpp b/src/AST/ToSAT.cpp
index 06f6e763b54c760a72854be2c4c1090be8156e48..81858f5f71b1c58ee7cbf9476c0957f7c09cb417 100644 (file)
--- a/src/AST/ToSAT.cpp
+++ b/src/AST/ToSAT.cpp
@@ -1316,6 +1316,7 @@ int BeevMgr::SATBased_ArrayReadRefinement(MINISAT::Solver& newS, const ASTNode&
                        ASTNodeStats("adding false readaxioms to SAT: ", FalseAxioms);
                        //printf("spot 01\n");
                        int res2 = 2;
+                       //if (FalseAxiomsVec.size() > 0)
                        if (FalseAxiomsVec.size() > oldFalseAxiomsSize)
                        {
                                res2 = CallSAT_ResultCheck(newS, FalseAxioms, orig_input);
@@ -1328,7 +1329,6 @@ int BeevMgr::SATBased_ArrayReadRefinement(MINISAT::Solver& newS, const ASTNode&
                        }
                }
        }
-       //ASTNode RemainingAxioms = RemainingAxiomsVec[0];
        ASTNode RemainingAxioms = (RemainingAxiomsVec.size() > 1) ? CreateNode(AND, RemainingAxiomsVec) : RemainingAxiomsVec[0];
        ASTNodeStats("adding remaining readaxioms to SAT: ", RemainingAxioms);
        return CallSAT_ResultCheck(newS, RemainingAxioms, orig_input);

diff --git a/src/bitvec/consteval.cpp b/src/bitvec/consteval.cpp
index 8e96db69010938e12e35bafd70a744adc16fedbb..daa42724c45223997fc983ca997021d6dd241076 100644 (file)
--- a/src/bitvec/consteval.cpp
+++ b/src/bitvec/consteval.cpp
@@ -1,5 +1,5 @@
 /********************************************************************
- * AUTHORS: Vijay Ganesh, David L. Dill
+ * AUTHORS: Vijay Ganesh
  *
  * BEGIN DATE: November, 2005
  *
@@ -143,7 +143,7 @@ ASTNode BeevMgr::BVConstEvaluator(const ASTNode& t)
                        {
                                // signed shift, and the number was originally negative.
                                // Shift may be larger than the inputwidth.
-                               for (int i =0; i < min(shift,inputwidth);i++)
+                               for (unsigned int i =0; i < min(shift,inputwidth);i++)
                                {
                                        CONSTANTBV::BitVector_Bit_On(output,(inputwidth-1 -i));
                                }

diff --git a/src/c_interface/c_interface.cpp b/src/c_interface/c_interface.cpp
index 75292ea98a113bf7b886aa53e3eb90b8a258cf8c..87627d0bce68d46d5e09c8d45c8103338c5bdae8 100644 (file)
--- a/src/c_interface/c_interface.cpp
+++ b/src/c_interface/c_interface.cpp
@@ -1507,7 +1507,7 @@ Expr getChild(Expr e, int i){
   nodestar a = (nodestar)e;
 
   BEEV::ASTVec c = a->GetChildren();
-  if(0 <=  (unsigned)i && (unsigned)i < c.size()) {
+  if(0 <=  i && i < c.size()) {
     BEEV::ASTNode o = c[i];
     nodestar output = new node(o);
     //if(cinterface_exprdelete_on) created_exprs.push_back(output);

diff --git a/src/parser/CVC.y b/src/parser/CVC.y
index d391d77a402d0836862a530d1eb25296f44677e9..6f8dae4450e7a7d4afb3cff99018c6b3931c3e7a 100644 (file)
--- a/src/parser/CVC.y
+++ b/src/parser/CVC.y
@@ -410,7 +410,7 @@ Formula             :     '(' Formula ')' { $$ = $2; }
                 |      BOOLEXTRACT_TOK '(' Expr ',' NUMERAL_TOK ')'
                        {
                         unsigned int width = $3->GetValueWidth();
-                        if(0 > (unsigned)$5 || width <= (unsigned)$5)
+                        if(width <= (unsigned)$5)
                           yyerror("Fatal Error: BOOLEXTRACT: trying to boolextract a bit which beyond range");
                         
                         BEEV::ASTNode hi  =  BEEV::globalBeevMgr_for_parser->CreateBVConst(32, $5);
@@ -652,7 +652,7 @@ Expr                :      TERMID_TOK { $$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser-
                         if (width < 0)
                           yyerror("Negative width in extract");
                         
-                        if((unsigned)$3 >= $1->GetValueWidth() || (unsigned)$5 < 0)
+                        if((unsigned)$3 >= $1->GetValueWidth())
                           yyerror("Parsing: Wrong width in BVEXTRACT\n");                       
 
                         BEEV::ASTNode hi  =  BEEV::globalBeevMgr_for_parser->CreateBVConst(32, $3);

diff --git a/src/parser/smtlib.y b/src/parser/smtlib.y
index b5be9d16028f58d4da68153d1803507f4d3a37ce..541e763fed0d7c81485f8a57a0e91bfa72390e7d 100644 (file)
--- a/src/parser/smtlib.y
+++ b/src/parser/smtlib.y
@@ -770,7 +770,7 @@ an_nonbvconst_term:
       if (width < 0)
        yyerror("Negative width in extract");
       
-      if((unsigned)$3 >= $7->GetValueWidth() || (unsigned)$5 < 0)
+      if((unsigned)$3 >= $7->GetValueWidth())
        yyerror("Parsing: Wrong width in BVEXTRACT\n");                  
       
       BEEV::ASTNode hi  =  BEEV::globalBeevMgr_for_parser->CreateBVConst(32, $3);

diff --git a/tests/bio-tests/4-alpha-helices-3-rungs-macros.cvc b/tests/bio-tests/4-alpha-helices-3-rungs-macros.cvc
index 460c84a942aee15c21030dab8df5094ad43361b6..533b656f151465efcf92bca277cb8c5dd5357c1a 100644 (file)
--- a/tests/bio-tests/4-alpha-helices-3-rungs-macros.cvc
+++ b/tests/bio-tests/4-alpha-helices-3-rungs-macros.cvc
@@ -66,8 +66,8 @@ ASSERT (BITS12_ONE_MACRO          = 0hex001);
 ASSERT (BITS16_ONE_MACRO          = 0hex0001);
 ASSERT (BITS16_TWO_MACRO          = 0hex0002);
 
-ASSERT (HIGH_ENERGY_MACRO         = 0hex0001);
-ASSERT (LOW_ENERGY_MACRO          = 0hex0000);
+ASSERT (HIGH_ENERGY_MACRO         = 0hex0FFF);
+ASSERT (LOW_ENERGY_MACRO          = 0hex007F);
  
 ASSERT (FACE_LEN1_MACRO           = 0hex1);
 ASSERT (FACE_LEN2_MACRO           = 0hex2);
@@ -530,5 +530,5 @@ ASSERT (inner_energy = BVPLUS(16,  contact_energy12_zero, contact_energy12_one,
 
 
 % final query
-ASSERT (BVGE(inner_energy, 0hex0FF0));
+ASSERT (BVGE(inner_energy, 0hexEFFF));
 QUERY FALSE;
\ No newline at end of file