From 17a2f5a1e83f26a4bd19931c6c188a80344947df Mon Sep 17 00:00:00 2001
From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Mon, 24 Aug 2009 04:52:52 +0000
Subject: [PATCH] * 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
---
 scripts/config.info   | 1 -
 src/AST/Makefile      | 2 +-
 src/AST/ToCNF.cpp     | 2 ++
 src/parser/smtlib.lex | 2 +-
 src/parser/smtlib.y   | 4 +++-
 src/sat/Makefile      | 2 +-
 6 files changed, 8 insertions(+), 5 deletions(-)
 delete mode 100644 scripts/config.info

diff --git a/scripts/config.info b/scripts/config.info
deleted file mode 100644
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 3358471..c25326d 100644
--- 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 3291d7e..822541e 100644
--- 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 9490bf0..80af712 100644
--- 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 67f82a8..36f84f5 100644
--- 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 9d98fc8..a6aa9e6 100644
--- 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
-- 
2.47.3