From 1fcd04a0ca0f15a54e8349e6df9c30be4c937950 Mon Sep 17 00:00:00 2001 From: vijay_ganesh Date: Mon, 31 Aug 2009 18:00:05 +0000 Subject: [PATCH] removed SMTLIB C-flag git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@163 e59a4935-1847-0410-ae03-e826735625c1 --- README | 10 +++++-- scripts/Makefile.common | 3 +- src/AST/AST.cpp | 16 +++++----- src/AST/AST.h | 56 ++++------------------------------- src/AST/Transform.cpp | 10 +++++-- src/simplifier/simplifier.cpp | 10 ++++++- 6 files changed, 37 insertions(+), 68 deletions(-) diff --git a/README b/README index 3bc7485..7b33ae5 100644 --- a/README +++ b/README @@ -8,24 +8,28 @@ * LICENSE: Please view LICENSE file in the home dir of this Program ********************************************************************/ + INSTALL ------- See INSTALL file in the home dir of this program + LICENSE ------- See LICENSE file in the home dir of this program + WEBSITE ------- -http://sourceforge.net/projects/stp-fast-prover/ +http://sourceforge.net/projects/stp-fast-prover -http://people.csail.mit.edu/vganesh/stp.html DOCUMENTATION ------------- http://people.csail.mit.edu/vganesh/STP_files/stp-docs.html -cd papers +PAPERS +----- +http://people.csail.mit.edu/vganesh/STP_files/stp-papers.html diff --git a/scripts/Makefile.common b/scripts/Makefile.common index 56c7f69..9260e42 100644 --- a/scripts/Makefile.common +++ b/scripts/Makefile.common @@ -5,13 +5,12 @@ #do not edit #OPTIONS1 = -DNATIVE_C_ARITH -#OPTIONS2 = -DSMTLIB #OPTIMIZE = -g -pg # Debugging and gprof-style profiling #OPTIMIZE = -g # Debugging OPTIMIZE = -O3 -DNDEBUG # Maximum optimization -CFLAGS_BASE = $(OPTIMIZE) $(OPTIONS1) $(OPTIONS2) +CFLAGS_BASE = $(OPTIMIZE) $(OPTIONS1) # You can compile using make STATIC=true to compile a statically linked executable # Note that you should execute liblinks.sh first. ifdef STATIC diff --git a/src/AST/AST.cpp b/src/AST/AST.cpp index 04651b1..23aea2c 100644 --- a/src/AST/AST.cpp +++ b/src/AST/AST.cpp @@ -626,10 +626,11 @@ ASTNode BeevMgr::CreateBVConst(const char* strval, int base) else { //this is an ugly hack to accomodate SMTLIB format - //restrictions. SMTLIB format represents bitvector constants in - //base 10 (what a terrible idea, but i have no choice but to - //support it), and make an implicit assumption that the length - //is 32 (another terrible idea). + //restrictions. SMTLIB format represents bitvector + //constants in base 10 (what a terrible idea, but i + //have no choice but to support it), and make an + //implicit assumption that the length is 32 (another + //terrible idea). unsigned width = 32; unsigned long long int val = strtoull(strval, NULL, base); ASTNode bvcon = CreateBVConst(width, val); @@ -809,16 +810,15 @@ void lpvec(const ASTVec &vec) ASTNode::ASTNode(const ASTNode &n) : _int_node_ptr(n._int_node_ptr) { -#ifndef SMTLIB if (n._int_node_ptr) { n._int_node_ptr->IncRef(); } -#endif } -// If there is a lot of sharing in the graph, this will take a long time. -// it doesn't mark subgraphs as already having been typechecked. +// If there is a lot of sharing in the graph, this will take a long +// time. it doesn't mark subgraphs as already having been +// typechecked. bool BeevMgr::BVTypeCheckRecursive(const ASTNode& n) { const ASTVec& c = n.GetChildren(); diff --git a/src/AST/AST.h b/src/AST/AST.h index fb446ad..c28efaf 100644 --- a/src/AST/AST.h +++ b/src/AST/AST.h @@ -423,15 +423,10 @@ protected: unsigned int _value_width; // Increment refcount. -#ifndef SMTLIB void IncRef() { ++_ref_count; } -#else - void IncRef() - {} -#endif // DecRef is a potentially expensive, because it has to delete // the node from the unique table, in addition to freeing it. @@ -1177,25 +1172,19 @@ inline types ASTNode::GetType() const // Constructor; creates a new pointer, increments refcount of // pointed-to object. -#ifndef SMTLIB inline ASTNode::ASTNode(ASTInternal *in) : _int_node_ptr(in) { if (in) in->IncRef(); } -#else -inline ASTNode::ASTNode(ASTInternal *in) : _int_node_ptr(in) -{}; -#endif -// Assignment. Increment refcount of new value, decrement refcount -// of old value and destroy if this was the last pointer. FIXME: +// Assignment. Increment refcount of new value, decrement refcount of +// old value and destroy if this was the last pointer. FIXME: // accelerate this by creating an intnode with a ref counter instead -// of pointing to NULL. Need a special check in CleanUp to make -// sure the null node never gets freed. +// of pointing to NULL. Need a special check in CleanUp to make sure +// the null node never gets freed. -#ifndef SMTLIB inline ASTNode& ASTNode::operator=(const ASTNode& n) { if (n._int_node_ptr) @@ -1209,15 +1198,7 @@ inline ASTNode& ASTNode::operator=(const ASTNode& n) _int_node_ptr = n._int_node_ptr; return *this; } -#else -inline ASTNode& ASTNode::operator=(const ASTNode& n) -{ - _int_node_ptr = n._int_node_ptr; - return *this; -} -#endif -#ifndef SMTLIB inline void ASTInternal::DecRef() { if (--_ref_count == 0) @@ -1235,18 +1216,6 @@ inline ASTNode::~ASTNode() _int_node_ptr->DecRef(); } } -; -#else -// No refcounting -inline void ASTInternal::DecRef() -{ -} - -// Destructor -inline ASTNode::~ASTNode() -{ -}; -#endif inline BeevMgr& ASTNode::GetBeevMgr() const { @@ -1265,9 +1234,6 @@ class BeevMgr friend class ASTBVConst; friend class ASTSymbol; - // FIXME: The values appear to be the same regardless of the value of SMTLIB - // initial hash table sizes, to save time on resizing. -#ifdef SMTLIB static const int INITIAL_INTERIOR_UNIQUE_TABLE_SIZE = 100; static const int INITIAL_SYMBOL_UNIQUE_TABLE_SIZE = 100; static const int INITIAL_BVCONST_UNIQUE_TABLE_SIZE = 100; @@ -1278,19 +1244,6 @@ class BeevMgr static const int INITIAL_SOLVER_MAP_SIZE = 100; static const int INITIAL_ARRAYREAD_SYMBOL_SIZE = 100; static const int INITIAL_INTRODUCED_SYMBOLS_SIZE = 100; -#else - // these are the STL defaults - static const int INITIAL_INTERIOR_UNIQUE_TABLE_SIZE = 100; - static const int INITIAL_SYMBOL_UNIQUE_TABLE_SIZE = 100; - static const int INITIAL_BVCONST_UNIQUE_TABLE_SIZE = 100; - static const int INITIAL_BBTERM_MEMO_TABLE_SIZE = 100; - static const int INITIAL_BBFORM_MEMO_TABLE_SIZE = 100; - - static const int INITIAL_SIMPLIFY_MAP_SIZE = 100; - static const int INITIAL_SOLVER_MAP_SIZE = 100; - static const int INITIAL_ARRAYREAD_SYMBOL_SIZE = 100; - static const int INITIAL_INTRODUCED_SYMBOLS_SIZE = 100; -#endif private: // Typedef for unique Interior node table. @@ -1604,6 +1557,7 @@ public: ASTNode SimplifyImpliesFormula(const ASTNode& a, bool pushNeg); ASTNode SimplifyIffFormula(const ASTNode& a, bool pushNeg); ASTNode SimplifyIteFormula(const ASTNode& a, bool pushNeg); + ASTNode SimplifyForFormula(const ASTNode& a, bool pushNeg); ASTNode FlattenOneLevel(const ASTNode& a); ASTNode FlattenAndOr(const ASTNode& a); ASTNode CombineLikeTerms(const ASTNode& a); diff --git a/src/AST/Transform.cpp b/src/AST/Transform.cpp index 52a1c8b..d71fd9b 100644 --- a/src/AST/Transform.cpp +++ b/src/AST/Transform.cpp @@ -7,9 +7,13 @@ ********************************************************************/ // -*- c++ -*- -// Transform: * Converts signed Div/ signed remainder/ signed modulus into unsigned. -// * Removes array selects and stores from formula. +/* Transform: + * + * Converts signed Div/signed remainder/signed modulus into their + * unsigned counterparts. Removes array selects and stores from + * formula. Arrays are replaced by equivalent bit-vector variables + */ #include "AST.h" #include @@ -437,7 +441,7 @@ ASTNode BeevMgr::TransformArray(const ASTNode& term) } else { - // Full Seshia transform if we're not doing read refinement. + // Full Array transform if we're not doing read refinement. ASTVec::const_reverse_iterator it2 = readIndices.rbegin(); ASTVec::const_reverse_iterator it2end = readIndices.rend(); for (; it2 != it2end; it2++) diff --git a/src/simplifier/simplifier.cpp b/src/simplifier/simplifier.cpp index d6e9ea9..b6e34d9 100644 --- a/src/simplifier/simplifier.cpp +++ b/src/simplifier/simplifier.cpp @@ -220,7 +220,7 @@ ASTNode BeevMgr::SimplifyFormula(const ASTNode& b, bool pushNeg) ASTNode a = b; ASTVec ca = a.GetChildren(); - if (!(IMPLIES == kind || ITE == kind || isAtomic(kind))) + if (!(IMPLIES == kind || ITE == kind || FOR == kind || isAtomic(kind))) { SortByArith(ca); a = CreateNode(kind, ca); @@ -260,6 +260,9 @@ ASTNode BeevMgr::SimplifyFormula(const ASTNode& b, bool pushNeg) case ITE: output = SimplifyIteFormula(a, pushNeg); break; + case FOR: + output = SimplifyForFormula(a, pushNeg); + break; default: //kind can be EQ,NEQ,BVLT,BVLE,... or a propositional variable output = SimplifyAtomicFormula(a, pushNeg); @@ -272,6 +275,11 @@ ASTNode BeevMgr::SimplifyFormula(const ASTNode& b, bool pushNeg) return output; } +ASTNode BeevMgr::SimplifyForFormula(const ASTNode& a, bool pushNeg) { + //Code this up properly later. Mainly pushing the negation down + return a; +} + ASTNode BeevMgr::SimplifyAtomicFormula(const ASTNode& a, bool pushNeg) { if (!optimize_flag) -- 2.47.3