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

diff --git a/README b/README
index 3bc7485d89e4a9721e45c7f6ac847509470e4ed6..7b33ae5cd17534f58065d59c1a72c23676de9076 100644 (file)
--- 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 56c7f6904b74399521a050fce13b7cd60a71e29c..9260e4206a8e439842065c13e78be42f16852b87 100644 (file)
--- 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 04651b120b86f314215136cec74049d260b0ecee..23aea2cd73daaac7980fec0006fcc5f7ac66afe6 100644 (file)
--- 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 fb446addb1bfc5b267c5a3ad0c8832d319c2b1d8..c28efaf9a776c03f18362a3df47c7c5252c37be0 100644 (file)
--- 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 52a1c8bc939912b045071cb06c6f46be3ee80962..d71fd9bdfba76413d65e7f220142f1f2448211c3 100644 (file)
--- 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 <stdlib.h>
@@ -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 d6e9ea9be8f4966a89b37894f292a247f621f56a..b6e34d9ded57e6f796f39bc68be01324b12f1b2b 100644 (file)
--- 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)