* Add -m32 flag to c-api-tests to get it compiling

* -t now tracks the bvsolver, and the substitution mapper (which sometimes takes a freakishly large amount of time).
* SimplifyCaches are no longer cleared at the start of topLevel simplify. Sometimes there is good stuff in there.

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

diff --git a/src/AST/AST.cpp b/src/AST/AST.cpp
index 72d7d03d0addcc4cfebe0442aea31d8be20bae01..c6f9ad071e94d1e9b80f3e7a6a6cf0f5561a4a0e 100644 (file)
--- a/src/AST/AST.cpp
+++ b/src/AST/AST.cpp
@@ -794,6 +794,8 @@ namespace BEEV
               FatalError("BVTypeCheck: indices should be BVCONST\n", n);
             if (n.GetValueWidth() != GetUnsignedConst(n[1]) - GetUnsignedConst(n[2]) + 1)
               FatalError("BVTypeCheck: length mismatch\n", n);
+                       if (GetUnsignedConst(n[1]) >= n[0].GetValueWidth())
+                               FatalError("BVTypeCheck: Top index of select is greater or equal to the bitwidth.\n", n);
             break;
           case BVLEFTSHIFT:
           case BVRIGHTSHIFT:

diff --git a/src/AST/RunTimes.cpp b/src/AST/RunTimes.cpp
index 80e0d7e98bb8281d9b1964fd8a240361c186a785..4c30ceb8e5df08a0744d237817b9b86773a12730 100644 (file)
--- a/src/AST/RunTimes.cpp
+++ b/src/AST/RunTimes.cpp
@@ -15,7 +15,7 @@
 #include <utility>
 
 // BE VERY CAREFUL> Update the Category Names to match.
-std::string RunTimes::CategoryNames[] = { "Transforming", "Simplifying", "Parsing", "CNF Conversion", "Bit Blasting", "Solving"};
+std::string RunTimes::CategoryNames[] = { "Transforming", "Simplifying", "Parsing", "CNF Conversion", "Bit Blasting", "SAT Solving", "Bitvector Solving","Create SubstitutionMap"};
 
 namespace BEEV
 {

diff --git a/src/AST/RunTimes.h b/src/AST/RunTimes.h
index f4288236a78fa616908a0f52e875f2c128555f8f..a7c9fd65bef33b25f442dabf4024eecd84e317c6 100644 (file)
--- a/src/AST/RunTimes.h
+++ b/src/AST/RunTimes.h
@@ -10,7 +10,7 @@ class RunTimes
 public:
        enum Category
                {
-                       Transforming = 0, SimplifyTopLevel, Parsing, CNFConversion, BitBlasting, Solving
+                       Transforming = 0, SimplifyTopLevel, Parsing, CNFConversion, BitBlasting, Solving, BVSolver, CreateSubstitutionMap
        };
 
        static std::string CategoryNames[];

diff --git a/src/simplifier/bvsolver.cpp b/src/simplifier/bvsolver.cpp
index a51549d59f083b7cdff37babfb4cc5fac1ec140e..89413cc4420792347404e5826599d839c2342d5b 100644 (file)
--- a/src/simplifier/bvsolver.cpp
+++ b/src/simplifier/bvsolver.cpp
@@ -541,6 +541,8 @@ namespace BEEV
         //output is TRUE. The formula is thus dropped
         return output;
       }
+
+    _bm->runTimes.start(RunTimes::BVSolver);
     ASTVec o;
     ASTVec c;
     if (EQ == k)
@@ -589,6 +591,7 @@ namespace BEEV
     output = _bm->CreateNode(AND, output, evens);
 
     UpdateAlreadySolvedMap(input, output);
+    _bm->runTimes.stop(RunTimes::BVSolver);
     return output;
   } //end of TopLevelBVSolve()
 

diff --git a/src/simplifier/simplifier.cpp b/src/simplifier/simplifier.cpp
index 9db64188b6e7fd040c26d5b0d640de8dc5bd5264..7c4813985f5c294f458e47334b324b25d8fef79f 100644 (file)
--- a/src/simplifier/simplifier.cpp
+++ b/src/simplifier/simplifier.cpp
@@ -308,12 +308,11 @@ ASTNode Flatten(const ASTNode& a)
       }
   }
 
-  ASTNode 
-  BeevMgr::SimplifyFormula_TopLevel(const ASTNode& b, 
-                                   bool pushNeg, ASTNodeMap* VarConstMap)
+  // The SimplifyMaps on entry to the topLevel functions may contain useful entries.
+  // E.g. The BVSolver calls SimplifyTerm()
+  ASTNode BeevMgr::SimplifyFormula_TopLevel(const ASTNode& b, bool pushNeg, ASTNodeMap* VarConstMap)
   {
        runTimes.start(RunTimes::SimplifyTopLevel);
-    ResetSimplifyMaps();
     if (smtlib_parser_flag)
     BuildReferenceCountMap(b);
     ASTNode out = SimplifyFormula(b, pushNeg, VarConstMap);
@@ -322,6 +321,16 @@ ASTNode Flatten(const ASTNode& a)
     return out;
   }
 
+ASTNode BeevMgr::SimplifyTerm_TopLevel(const ASTNode& b)
+{
+       runTimes.start(RunTimes::SimplifyTopLevel);
+       ASTNode out = SimplifyTerm(b);
+       ResetSimplifyMaps();
+       runTimes.stop(RunTimes::SimplifyTopLevel);
+       return out;
+}
+
+
   ASTNode 
   BeevMgr::SimplifyFormula(const ASTNode& b, 
                           bool pushNeg, ASTNodeMap* VarConstMap)
@@ -1393,14 +1402,6 @@ ASTNode Flatten(const ASTNode& a)
     //memoize
   } //end of flattenonelevel()
 
-  ASTNode BeevMgr::SimplifyTerm_TopLevel(const ASTNode& b)
-  {
-    ResetSimplifyMaps();
-    ASTNode out = SimplifyTerm(b);
-    ResetSimplifyMaps();
-    return out;
-  }
-
   //This function simplifies terms based on their kind
   ASTNode 
   BeevMgr::SimplifyTerm(const ASTNode& actualInputterm, ASTNodeMap* VarConstMap)
@@ -3220,15 +3221,20 @@ ASTNode Flatten(const ASTNode& a)
   // clears() in particular.
   void BeevMgr::ResetSimplifyMaps()
   {
-    SimplifyMap->clear();
+    // clear() is extremely expensive for hash_maps with a lot of buckets,
+    // in the EXT_MAP implementation it visits every bucket, checking whether
+    // each bucket is empty or not, if non-empty it deletes the contents. 
+    // The destructor seems to clear everything anyway. 
+
+    //SimplifyMap->clear();
     delete SimplifyMap;
     SimplifyMap = new ASTNodeMap(INITIAL_SIMPLIFY_MAP_SIZE);
 
-    SimplifyNegMap->clear();
+    //SimplifyNegMap->clear();
     delete SimplifyNegMap;
     SimplifyNegMap = new ASTNodeMap(INITIAL_SIMPLIFY_MAP_SIZE);
 
-    ReferenceCount->clear();
+    //ReferenceCount->clear();
     delete ReferenceCount;
     ReferenceCount = new ASTNodeCountMap(INITIAL_SIMPLIFY_MAP_SIZE);
   }

diff --git a/src/to-sat/ToSAT.cpp b/src/to-sat/ToSAT.cpp
index e02340b1a3ebcee806723648949f8297ccc4df7c..55582e31758a740614ea96a21e9627afafbdc535 100644 (file)
--- a/src/to-sat/ToSAT.cpp
+++ b/src/to-sat/ToSAT.cpp
@@ -953,8 +953,10 @@ namespace BEEV
        if(optimize_flag) 
          {
 
+          runTimes.start(RunTimes::CreateSubstitutionMap);
            simplified_solved_InputToSAT = 
              CreateSubstitutionMap(simplified_solved_InputToSAT);
+          runTimes.stop(RunTimes::CreateSubstitutionMap);
            //printf("##################################################\n");
            ASTNodeStats("after pure substitution: ", simplified_solved_InputToSAT);
 
@@ -988,8 +990,10 @@ namespace BEEV
 
        if(optimize_flag) 
          {
+               runTimes.start(RunTimes::CreateSubstitutionMap);
            simplified_solved_InputToSAT = 
              CreateSubstitutionMap(simplified_solved_InputToSAT);
+           runTimes.stop(RunTimes::CreateSubstitutionMap);
            ASTNodeStats("after pure substitution: ", simplified_solved_InputToSAT);
 
            simplified_solved_InputToSAT = 

diff --git a/tests/c-api-tests/Makefile b/tests/c-api-tests/Makefile
index 427e68156ce6038a0f5340be20fbd78e3c61f4e5..33c63802b4adafbcaf8b3ade42ecc69be0ce5a19 100644 (file)
--- a/tests/c-api-tests/Makefile
+++ b/tests/c-api-tests/Makefile
@@ -1,64 +1,66 @@
+CXXFLAGS=-DEXT_HASH_MAP -m32 -I../../src/c_interface -L../../lib
+
 
 all: 0 1 2 3 4 5 6 7 8 9 10 11 11 12 13 14 15 16 17 18
        rm -rf *.out
 
 0:     
-       g++ -DEXT_HASH_MAP array-cvcl-02.c -I../../src/c_interface -L../../lib -lstp -o a0.out
+       g++ $(CXXFLAGS) array-cvcl-02.c -o a0.out -lstp
        ./a0.out
 
 1:     
-       g++ -DEXT_HASH_MAP b4-c.c -I../../src/c_interface -L../../lib -lstp -o a1.out
+       g++  $(CXXFLAGS) b4-c.c -lstp -o a1.out
        ./a1.out
 2:
-       g++ -DEXT_HASH_MAP b4-c2.c -I../../src/c_interface -L../../lib -lstp -o a2.out
+       g++  $(CXXFLAGS) b4-c2.c -lstp -o a2.out
        ./a2.out
 3:
-       g++ -DEXT_HASH_MAP getbvunsignedlonglong-check.c -I../../src/c_interface -L../../lib -lstp -o a3.out
+       g++  $(CXXFLAGS) getbvunsignedlonglong-check.c -lstp -o a3.out
        ./a3.out
 4:
-       g++ -DEXT_HASH_MAP multiple-queries.c -I../../src/c_interface -L../../lib -lstp -o a4.out
+       g++  $(CXXFLAGS) multiple-queries.c  -lstp -o a4.out
        ./a4.out
 5:
-       g++ -DEXT_HASH_MAP parsefile-using-cinterface.c -I../../src/c_interface -L../../lib -lstp -o a5.out
+       g++  $(CXXFLAGS) parsefile-using-cinterface.c -lstp -o a5.out
        ./a5.out
 6:
-       g++ -DEXT_HASH_MAP print.c -I../../src/c_interface -L../../lib -lstp -o a6.out
+       g++  $(CXXFLAGS) print.c -lstp -o a6.out
        ./a6.out
 7:
-       g++ -DEXT_HASH_MAP push-pop-1.c -I../../src/c_interface -L../../lib -lstp -o a7.out
+       g++  $(CXXFLAGS) push-pop-1.c -lstp -o a7.out
        ./a7.out
 8:
-       g++ -DEXT_HASH_MAP sbvmod.c -I../../src/c_interface -L../../lib -lstp -o a8.out
+       g++  $(CXXFLAGS)  sbvmod.c -lstp -o a8.out
        ./a8.out
 9:
-       g++ -DEXT_HASH_MAP simplify.c -I../../src/c_interface -L../../lib -lstp -o a9.out
+       g++  $(CXXFLAGS)  simplify.c -o a9.out -lstp
        ./a9.out
 10:
-       g++ -DEXT_HASH_MAP simplify1.c -I../../src/c_interface -L../../lib -lstp -o a10.out
+       g++  $(CXXFLAGS)  simplify1.c -lstp -o a10.out
        ./a10.out
 11:
-       g++ -DEXT_HASH_MAP squares-leak.c -I../../src/c_interface -L../../lib -lstp -o a11.out
+       g++  $(CXXFLAGS)  squares-leak.c -lstp -o a11.out
        ./a11.out
 12:
-       g++ -DEXT_HASH_MAP stp-counterex.c -I../../src/c_interface -L../../lib -lstp -o a12.out
+       g++  $(CXXFLAGS)  stp-counterex.c -lstp -o a12.out
        ./a12.out
 13:
-       g++ -DEXT_HASH_MAP stp-div-001.c -I../../src/c_interface -L../../lib -lstp -o a13.out
+       g++  $(CXXFLAGS)  stp-div-001.c  -lstp -o a13.out
        ./a13.out
 14:
-       g++ -DEXT_HASH_MAP stpcheck.c -I../../src/c_interface -L../../lib -lstp -o a14.out
+       g++  $(CXXFLAGS)  stpcheck.c -o a14.out -lstp
        ./a14.out
 15:
-       g++ -DEXT_HASH_MAP x.c -I../../src/c_interface -L../../lib -lstp -o a15.out
+       g++  $(CXXFLAGS)  x.c  -lstp -o a15.out
        ./a15.out
 16:
-       g++ -DEXT_HASH_MAP y.c -I../../src/c_interface -L../../lib -lstp -o a16.out
+       g++ $(CXXFLAGS)  y.c -lstp -o a16.out
        ./a16.out
 17:
-       g++ -DEXT_HASH_MAP push-pop.c -I../../src/c_interface -L../../lib -lstp -o a17.out
+       g++  $(CXXFLAGS)  push-pop.c -lstp -o a17.out
        ./a17.out
 18:
-       g++ -DEXT_HASH_MAP cvc-to-c.cpp -I../../src/c_interface -L../../lib -lstp -o a18.out
+       g++  $(CXXFLAGS)  cvc-to-c.cpp  -lstp -o a18.out
        ./a18.out ./t.cvc