From: vijay_ganesh Date: Wed, 12 Aug 2009 23:24:32 +0000 (+0000) Subject: minor changes X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=f8c45bded1f943290b8ca693233053b0e404757b;p=francis%2Fstp.git 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 fcc665a..56c7f69 100644 --- 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 f794a86..016a02d 100755 --- 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 e154e34..9be6b1d 100644 --- 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 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 06f6e76..81858f5 100644 --- 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 8e96db6..daa4272 100644 --- 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 75292ea..87627d0 100644 --- 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 d391d77..6f8dae4 100644 --- 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 b5be9d1..541e763 100644 --- 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 460c84a..533b656 100644 --- 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