* Stop compiler warnings from the smtlib parser.

* Fix "make clean" to not try to delete a non-existant path.
* Fix "make clean" to remove all the .o files.
* Delete config.info from svn.
* Pre-size some vectors during CNF generation. When solving a single 64-bit multiply, this reduces total runtime by about 5%.

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

diff --git a/scripts/config.info b/scripts/config.info
deleted file mode 100644 (file)
index 6befdf2..0000000
--- a/scripts/config.info
+++ /dev/null
@@ -1 +0,0 @@
-PREFIX=/Users/katelman

diff --git a/src/AST/Makefile b/src/AST/Makefile
index 3358471c4d3ccfd4cf71b14e79489e10f1aed587..c25326d03ec1868147d30458f7e728fe8fbdd20f 100644 (file)
--- a/src/AST/Makefile
+++ b/src/AST/Makefile
@@ -29,7 +29,7 @@ ASTKind.h ASTKind.cpp:        ASTKind.kinds genkinds.pl
 
 clean:
        rm -rf *.o *~ bbtest asttest cnftest *.a  ASTKind.h ASTKind.cpp .#*
-       rm -rf outputer/*.o
+       rm -rf printer/*.o
 
 depend:
        makedepend -Y -- $(CFLAGS) -- $(SRCS)

diff --git a/src/AST/ToCNF.cpp b/src/AST/ToCNF.cpp
index 3291d7e0f6241bda2da2adb09a308a698836a046..822541e0cf3df1f90d1daeefe89485192dcdc00e 100644 (file)
--- a/src/AST/ToCNF.cpp
+++ b/src/AST/ToCNF.cpp
@@ -508,6 +508,7 @@ private:
        {
 
                BeevMgr::ClauseList* psi = new BeevMgr::ClauseList();
+               psi->reserve(varphi1.size() * varphi2.size());
 
                BeevMgr::ClauseList::const_iterator it1 = varphi1.begin();
                for (; it1 != varphi1.end(); it1++)
@@ -518,6 +519,7 @@ private:
                        {
                                BeevMgr::ClausePtr clause2 = *it2;
                                BeevMgr::ClausePtr clause = new vector<const ASTNode*> ();
+                               clause->reserve(clause1->size() + clause2->size());
                                clause->insert(clause->end(), clause1->begin(), clause1->end());
                                clause->insert(clause->end(), clause2->begin(), clause2->end());
                                psi->push_back(clause);

diff --git a/src/parser/smtlib.lex b/src/parser/smtlib.lex
index 9490bf098afcfc7f2342900f5b68ab47144b393c..80af712c632014ac495a26613065a196fe351bca 100644 (file)
--- a/src/parser/smtlib.lex
+++ b/src/parser/smtlib.lex
@@ -38,7 +38,7 @@
 #include "parseSMT_defs.h"
   
   extern char *smttext;
-  extern int smterror (char *msg);
+  extern int smterror (const char *msg);
   
   // File-static (local to this file) variables and functions
   static std::string _string_lit;

diff --git a/src/parser/smtlib.y b/src/parser/smtlib.y
index 67f82a8b48d4cb87a1104cca98de5c5b9ee74eef..36f84f5341699eb7a355e264bb8c156e32b85b36 100644 (file)
--- a/src/parser/smtlib.y
+++ b/src/parser/smtlib.y
@@ -47,7 +47,7 @@
   
   extern int smtlex(void);
 
-  int yyerror(char *s) {
+  int yyerror(const char *s) {
     cout << "syntax error: line " << smtlineno << "\n" << s << endl;
     cout << "  token: " << smttext << endl;
     BEEV::FatalError("");
@@ -1088,6 +1088,7 @@ an_nonbvconst_term:
       }
       else
       {
+       n = NULL; // remove gcc warning.
        yyerror("Rotate must be strictly less than the width.");
       }
       
@@ -1120,6 +1121,7 @@ an_nonbvconst_term:
       }
       else
       {
+               n = NULL; // remove gcc warning.
        yyerror("Rotate must be strictly less than the width.");
       }
       

diff --git a/src/sat/Makefile b/src/sat/Makefile
index 9d98fc867cc4d8eca4a72d87c624c6490fc09bea..a6aa9e6dbd301d794d5710275a947a6814b2d87f 100644 (file)
--- a/src/sat/Makefile
+++ b/src/sat/Makefile
@@ -14,4 +14,4 @@ clean:
        rm -rf *~ libminisat.a
        $(MAKE) -C core clean
        $(MAKE) -C simp clean
-       $(MAKE) -C unsound clean
\ No newline at end of file
+       #$(MAKE) -C unsound clean