* lhsminusrhs(..) does not perform its simplification if it will increase the number...

* The Transform functions are now mostly non-member. The cache is created on entry to TopLevel and deleted on exit.
* regress_smt only checks the smt-test folder, not its subfolders! These regression tests take under a minute to run.

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

diff --git a/scripts/run_smt_tests.pl b/scripts/run_smt_tests.pl
index c686c9100a1799d4229ed351224dc6092d43a2c6..69fd71bba438d9961b9623b21db534d7f012893e 100755 (executable)
--- a/scripts/run_smt_tests.pl
+++ b/scripts/run_smt_tests.pl
@@ -90,9 +90,9 @@ my %options = ();
 # The list of testcases to run
 #
 my @testcases = "../../stp-tests/smt-test";
-my @testcases1 = "../../stp-tests/smt-test/QF_AUFBV/brummayerbiere2";
-my @testcases2 = "../../stp-tests/smt-test/QF_AUFBV/brummayerbiere2";
-my @testcases3 = "../../stp-tests/smt-test/QF_AUFBV/platania";
+#my @testcases1 = "../../stp-tests/smt-test/QF_AUFBV/brummayerbiere2";
+#my @testcases2 = "../../stp-tests/smt-test/QF_AUFBV/brummayerbiere2";
+#my @testcases3 = "../../stp-tests/smt-test/QF_AUFBV/platania";
 # Temporary array for STP options
 my @stpOptions = ();
 
@@ -250,7 +250,7 @@ my $totalTime = time;
 my $defaultDir = `pwd`;
 $defaultDir =~ s/\n//;
 
-foreach my $testcase ((@testcases,@testcases1,@testcases2,@testcases3)) {
+foreach my $testcase ((@testcases)) {
     chdir $defaultDir or die "Cannot chdir to $defaultDir: $?";
     my @testcasesTmp = ();
     if(-f $testcase) { push @testcasesTmp, $testcase; }

diff --git a/src/AST/AST.cpp b/src/AST/AST.cpp
index f67589a21133bb2cece93842efea95df96dc1326..ec02c4fdf7506a9b05bd21a6b8abe879e75eb971 100644 (file)
--- a/src/AST/AST.cpp
+++ b/src/AST/AST.cpp
@@ -1265,12 +1265,13 @@ void BeevMgr::ClearAllTables(void)
        AlreadyPrintedSet.clear();
        SimplifyMap->clear();
        SimplifyNegMap->clear();
+       ReferenceCount->clear();
        SolverMap.clear();
        AlwaysTrueFormMap.clear();
        _arrayread_ite.clear();
        _arrayread_symbol.clear();
        _introduced_symbols.clear();
-       TransformMap.clear();
+       //TransformMap.clear();
        _letid_expr_map->clear();
        CounterExampleMap.clear();
        ComputeFormulaMap.clear();
@@ -1324,12 +1325,12 @@ void BeevMgr::ClearAllCaches(void)
        AlreadyPrintedSet.clear();
        SimplifyMap->clear();
        SimplifyNegMap->clear();
+       ReferenceCount->clear();
        SolverMap.clear();
        AlwaysTrueFormMap.clear();
        _arrayread_ite.clear();
        _arrayread_symbol.clear();
        _introduced_symbols.clear();
-       TransformMap.clear();
        _letid_expr_map->clear();
        CounterExampleMap.clear();
        ComputeFormulaMap.clear();
@@ -1421,6 +1422,7 @@ BeevMgr::~BeevMgr()
        delete SimplifyMap;
        delete SimplifyNegMap;
        delete _letid_expr_map;
+       delete ReferenceCount;
 }
 
 }

diff --git a/src/AST/AST.h b/src/AST/AST.h
index bdcbdc6aaf85a2f1bf86a5a60b463003793a7a39..58602abd0491eb365b7512d7830b6f338b942dba 100644 (file)
--- a/src/AST/AST.h
+++ b/src/AST/AST.h
@@ -32,6 +32,7 @@
 #include <algorithm>
 #include "ASTUtil.h"
 #include "ASTKind.h"
+#include <stdint.h>
 #include "../sat/core/Solver.h"
 //#include "../sat/simp/SimpSolver.h"
 //#include "../sat/unsound/UnsoundSimpSolver.h"
@@ -1027,6 +1028,9 @@ inline unsigned int GetUnsignedConst(const ASTNode n)
 // Hash table from ASTNodes to ASTNodes
 typedef hash_map<ASTNode, ASTNode, ASTNode::ASTNodeHasher, ASTNode::ASTNodeEqual> ASTNodeMap;
 
+typedef hash_map<ASTNode, int32_t, ASTNode::ASTNodeHasher, ASTNode::ASTNodeEqual> ASTNodeCountMap;
+
+
 // Function to dump contents of ASTNodeMap
 ostream &operator<<(ostream &os, const ASTNodeMap &nmap);
 
@@ -1532,6 +1536,8 @@ public:
        ASTNode SimplifyTerm(const ASTNode& a);
        ASTNode SimplifyTermAux(const ASTNode& a);
        void CheckSimplifyInvariant(const ASTNode& a, const ASTNode& output);
+       void BuildReferenceCountMap(const ASTNode& b);
+
 private:
        //memo table for simplifcation
        ASTNodeMap *SimplifyMap;
@@ -1540,6 +1546,15 @@ private:
        ASTNodeSet AlwaysTrueFormMap;
        ASTNodeMap MultInverseMap;
 
+
+       // The number of direct parents of each node. i.e. the number of times the pointer is in "children".
+       // When we simplify we want to be careful sometimes about using the context of a node. For example,
+       // given ((x + 23) = 2), the obvious simplification is to join the constants. However, if there are
+       // lots of references to the plus node. Then each time we simplify, we'll create an additional plus.
+       // nextpoweroftwo064.smt is the motivating benchmark. The splitting increased the number of pluses
+       // from 1 to 65.
+       ASTNodeCountMap *ReferenceCount;
+
 public:
        ASTNode SimplifyAtomicFormula(const ASTNode& a, bool pushNeg);
        ASTNode CreateSimplifiedEQ(const ASTNode& t1, const ASTNode& t2);
@@ -1610,6 +1625,8 @@ public:
        ///print SAT solver statistics
        void PrintStats(MINISAT::Solver& stats);
 
+       void printCacheStatus();
+
        //from v8
        int TopLevelSATAux(const ASTNode& query);
 
@@ -1678,23 +1695,18 @@ private:
 
        ASTNodeSet _introduced_symbols;
 
-       /*Memoization map for TransformFormula/TransformTerm/TransformArray function
-        */
-       ASTNodeMap TransformMap;
-
        //count to keep track of new symbolic constants introduced
        //corresponding to Array Reads
        unsigned int _symbol_count;
 
        //Formula/Term Transformers. Let Expr Manager, Type Checker
 public:
-       //Functions that Transform ASTNodes
-       ASTNode TransformFormula(const ASTNode& query);
-       ASTNode TransformTerm(const ASTNode& term);
+       //Functions that Transform ASTNodes. TransformArray should be a non-member function,
+       // but it accesses private elements. Move it later.
+       ASTNode TransformFormula_TopLevel(const ASTNode& form);
        ASTNode TransformArray(const ASTNode& term);
        ASTNode TransformFiniteFor(const ASTNode& form);
-       ASTNode TranslateSignedDivModRem(const ASTNode& term);
-       void    assertTransformPostConditions(const ASTNode & term);
+
 
        //LET Management
 private:
@@ -1931,6 +1943,7 @@ public:
                SimplifyMap = new ASTNodeMap(INITIAL_SIMPLIFY_MAP_SIZE);
                SimplifyNegMap = new ASTNodeMap(INITIAL_SIMPLIFY_MAP_SIZE);
                _letid_expr_map = new ASTNodeMap(INITIAL_INTRODUCED_SYMBOLS_SIZE);
+               ReferenceCount = new ASTNodeCountMap(INITIAL_SIMPLIFY_MAP_SIZE);
        }
        ;
 

diff --git a/src/AST/ToSAT.cpp b/src/AST/ToSAT.cpp
index 5d1d0bc80b2be725f5522bbc3f2b0fdc8ff9dc57..84bdde3d74afd827424880ff333a8d6f51cae78e 100644 (file)
--- a/src/AST/ToSAT.cpp
+++ b/src/AST/ToSAT.cpp
@@ -1101,6 +1101,23 @@ ASTNode BeevMgr::GetCounterExample(bool t, const ASTNode& expr)
 //##################################################
 //##################################################
 
+
+void BeevMgr::printCacheStatus()
+{
+       cerr << SimplifyMap->size() << endl;
+       cerr << SimplifyNegMap->size() << endl;
+       cerr << ReferenceCount->size() << endl;
+       cerr << TermsAlreadySeenMap.size() << endl;
+
+       cerr << SimplifyMap->bucket_count() << endl;
+       cerr << SimplifyNegMap->bucket_count() << endl;
+       cerr << ReferenceCount->bucket_count() << endl;
+       cerr << TermsAlreadySeenMap.bucket_count() << endl;
+
+
+
+}
+
 // FIXME:  Don't use numeric codes.  Use an enum type!
 //Acceps a query, calls the SAT solver and generates Valid/InValid.
 //if returned 0 then input is INVALID
@@ -1179,12 +1196,13 @@ int BeevMgr::TopLevelSATAux(const ASTNode& inputasserts)
        SimplifyWrites_InPlace_Flag = false;
        Begin_RemoveWrites = false;
 
-       newq = TransformFormula(newq);
-       if (false)
-               assertTransformPostConditions(newq);
+       newq = TransformFormula_TopLevel(newq);
        ASTNodeStats("after transformation: ", newq);
        TermsAlreadySeenMap.clear();
 
+       //if(stats_flag)
+       //      printCacheStatus();
+
        int res;
        //solver instantiated here
        MINISAT::Solver newS;
@@ -1369,12 +1387,12 @@ int BeevMgr::SATBased_ArrayWriteRefinement(MINISAT::Solver& newS, const ASTNode&
                writeAxiom = Create_ArrayWriteAxioms(it->first, it->second);
                if (ASTFalse == ComputeFormulaUsingModel(writeAxiom))
                {
-                       writeAxiom = TransformFormula(writeAxiom);
+                       writeAxiom = TransformFormula_TopLevel(writeAxiom);
                        FalseAxioms.push_back(writeAxiom);
                }
                else
                {
-                       writeAxiom = TransformFormula(writeAxiom);
+                       writeAxiom = TransformFormula_TopLevel(writeAxiom);
                        RemainingAxioms.push_back(writeAxiom);
                }
        }

diff --git a/src/AST/Transform.cpp b/src/AST/Transform.cpp
index 459f0ed2ed97e53028c9dc832644f34427a91791..84b3988cb235719a9872743f4821d505cc9afb2a 100644 (file)
--- a/src/AST/Transform.cpp
+++ b/src/AST/Transform.cpp
@@ -8,52 +8,78 @@
 // -*- c++ -*-
 
 
-/* Transform: 
+/* 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>
 #include <stdio.h>
 namespace BEEV
 {
 
+ASTNode TransformFormula(const ASTNode& form);
+ASTNode TranslateSignedDivModRem(const ASTNode& in);
+ASTNode TransformTerm(const ASTNode& inputterm);
+void assertTransformPostConditions(const ASTNode & term);
+
+ASTNodeMap* TransformMap;
+
+const bool debug_transform = false;
+
+// NB: This is the only function that should be called externally. It sets
+// up the cache that the others use.
+ASTNode BeevMgr::TransformFormula_TopLevel(const ASTNode& form)
+{
+       assert(TransformMap == NULL);
+       TransformMap = new ASTNodeMap(100);
+       ASTNode result = TransformFormula(form);
+       if (debug_transform)
+               assertTransformPostConditions(result);
+       TransformMap->clear();
+       delete TransformMap;
+       TransformMap = NULL;
+       return result;
+}
+
 //Translates signed BVDIV,BVMOD and BVREM into unsigned variety
-ASTNode BeevMgr::TranslateSignedDivModRem(const ASTNode& in)
+ASTNode TranslateSignedDivModRem(const ASTNode& in)
 {
+       BeevMgr& bm = in.GetBeevMgr();
        assert(in.GetChildren().size() ==2);
 
        ASTNode dividend = in[0];
        ASTNode divisor = in[1];
        unsigned len = in.GetValueWidth();
 
-       ASTNode hi1 = CreateBVConst(32, len - 1);
-       ASTNode one = CreateOneConst(1);
-       ASTNode zero = CreateZeroConst(1);
+       ASTNode hi1 = bm.CreateBVConst(32, len - 1);
+       ASTNode one = bm.CreateOneConst(1);
+       ASTNode zero = bm.CreateZeroConst(1);
        // create the condition for the dividend
-       ASTNode cond_dividend = CreateNode(EQ, one, CreateTerm(BVEXTRACT, 1, dividend, hi1, hi1));
+       ASTNode cond_dividend = bm.CreateNode(EQ, one, bm.CreateTerm(BVEXTRACT, 1, dividend, hi1, hi1));
        // create the condition for the divisor
-       ASTNode cond_divisor = CreateNode(EQ, one, CreateTerm(BVEXTRACT, 1, divisor, hi1, hi1));
+       ASTNode cond_divisor = bm.CreateNode(EQ, one, bm.CreateTerm(BVEXTRACT, 1, divisor, hi1, hi1));
 
        if (SBVREM == in.GetKind())
        {
                //BVMOD is an expensive operation. So have the fewest bvmods possible. Just one.
 
                //Take absolute value.
-               ASTNode pos_dividend = CreateTerm(ITE, len, cond_dividend, CreateTerm(BVUMINUS, len, dividend), dividend);
-               ASTNode pos_divisor = CreateTerm(ITE, len, cond_divisor, CreateTerm(BVUMINUS, len, divisor), divisor);
+               ASTNode pos_dividend = bm.CreateTerm(ITE, len, cond_dividend, bm.CreateTerm(BVUMINUS, len, dividend), dividend);
+               ASTNode pos_divisor = bm.CreateTerm(ITE, len, cond_divisor, bm.CreateTerm(BVUMINUS, len, divisor), divisor);
 
                //create the modulus term
-               ASTNode modnode = CreateTerm(BVMOD, len, pos_dividend, pos_divisor);
+               ASTNode modnode = bm.CreateTerm(BVMOD, len, pos_dividend, pos_divisor);
 
                //If the dividend is <0 take the unary minus.
-               ASTNode n = CreateTerm(ITE, len, cond_dividend, CreateTerm(BVUMINUS, len, modnode), modnode);
+               ASTNode n = bm.CreateTerm(ITE, len, cond_dividend, bm.CreateTerm(BVUMINUS, len, modnode), modnode);
 
                //put everything together, simplify, and return
-               return SimplifyTerm_TopLevel(n);
+               return bm.SimplifyTerm_TopLevel(n);
        }
 
        // This is the modulus of dividing rounding to -infinity.
@@ -72,19 +98,19 @@ ASTNode BeevMgr::TranslateSignedDivModRem(const ASTNode& in)
                //      (bvneg (bvurem (bvneg s) (bvneg t)))))))
 
                //Take absolute value.
-               ASTNode pos_dividend = CreateTerm(ITE, len, cond_dividend, CreateTerm(BVUMINUS, len, dividend), dividend);
-               ASTNode pos_divisor = CreateTerm(ITE, len, cond_divisor, CreateTerm(BVUMINUS, len, divisor), divisor);
+               ASTNode pos_dividend = bm.CreateTerm(ITE, len, cond_dividend, bm.CreateTerm(BVUMINUS, len, dividend), dividend);
+               ASTNode pos_divisor = bm.CreateTerm(ITE, len, cond_divisor, bm.CreateTerm(BVUMINUS, len, divisor), divisor);
 
-               ASTNode urem_node = CreateTerm(BVMOD, len, pos_dividend, pos_divisor);
+               ASTNode urem_node = bm.CreateTerm(BVMOD, len, pos_dividend, pos_divisor);
 
                // If the dividend is <0, then we negate the whole thing.
-               ASTNode rev_node = CreateTerm(ITE, len, cond_dividend, CreateTerm(BVUMINUS, len, urem_node), urem_node);
+               ASTNode rev_node = bm.CreateTerm(ITE, len, cond_dividend, bm.CreateTerm(BVUMINUS, len, urem_node), urem_node);
 
                // if It's XOR <0 then add t (not its absolute value).
-               ASTNode xor_node = CreateNode(XOR, cond_dividend, cond_divisor);
-               ASTNode n = CreateTerm(ITE, len, xor_node, CreateTerm(BVPLUS, len, rev_node, divisor), rev_node);
+               ASTNode xor_node = bm.CreateNode(XOR, cond_dividend, cond_divisor);
+               ASTNode n = bm.CreateTerm(ITE, len, xor_node, bm.CreateTerm(BVPLUS, len, rev_node, divisor), rev_node);
 
-               return SimplifyTerm_TopLevel(n);
+               return bm.SimplifyTerm_TopLevel(n);
        }
        else if (SBVDIV == in.GetKind())
        {
@@ -104,25 +130,25 @@ ASTNode BeevMgr::TranslateSignedDivModRem(const ASTNode& in)
                //else simply output BVDIV(dividend,divisor)
 
                //Take absolute value.
-               ASTNode pos_dividend = CreateTerm(ITE, len, cond_dividend, CreateTerm(BVUMINUS, len, dividend), dividend);
-               ASTNode pos_divisor = CreateTerm(ITE, len, cond_divisor, CreateTerm(BVUMINUS, len, divisor), divisor);
+               ASTNode pos_dividend = bm.CreateTerm(ITE, len, cond_dividend, bm.CreateTerm(BVUMINUS, len, dividend), dividend);
+               ASTNode pos_divisor = bm.CreateTerm(ITE, len, cond_divisor, bm.CreateTerm(BVUMINUS, len, divisor), divisor);
 
-               ASTNode divnode = CreateTerm(BVDIV, len, pos_dividend, pos_divisor);
+               ASTNode divnode = bm.CreateTerm(BVDIV, len, pos_dividend, pos_divisor);
 
                // A little confusing. Only negate the result if they are XOR <0.
-               ASTNode xor_node = CreateNode(XOR, cond_dividend, cond_divisor);
-               ASTNode n = CreateTerm(ITE, len, xor_node, CreateTerm(BVUMINUS, len, divnode), divnode);
+               ASTNode xor_node = bm.CreateNode(XOR, cond_dividend, cond_divisor);
+               ASTNode n = bm.CreateTerm(ITE, len, xor_node, bm.CreateTerm(BVUMINUS, len, divnode), divnode);
 
-               return SimplifyTerm_TopLevel(n);
+               return bm.SimplifyTerm_TopLevel(n);
        }
 
        FatalError("TranslateSignedDivModRem: input must be signed DIV/MOD/REM", in);
-       return ASTUndefined;
+       return bm.CreateNode(UNDEFINED);
 
 }//end of TranslateSignedDivModRem()
 
 // Check that the transformations have occurred.
-void BeevMgr::assertTransformPostConditions(const ASTNode & term)
+void assertTransformPostConditions(const ASTNode & term)
 {
        const Kind k = term.GetKind();
 
@@ -148,8 +174,12 @@ void BeevMgr::assertTransformPostConditions(const ASTNode & term)
        }
 }
 
-ASTNode BeevMgr::TransformFormula(const ASTNode& form)
+ASTNode TransformFormula(const ASTNode& form)
 {
+       BeevMgr& bm = form.GetBeevMgr();
+
+       assert(TransformMap != null);
+
        ASTNode result;
 
        ASTNode simpleForm = form;
@@ -161,7 +191,7 @@ ASTNode BeevMgr::TransformFormula(const ASTNode& form)
        }
 
        ASTNodeMap::iterator iter;
-       if ((iter = TransformMap.find(simpleForm)) != TransformMap.end())
+       if ((iter = TransformMap->find(simpleForm)) != TransformMap->end())
                return iter->second;
 
        switch (k)
@@ -176,7 +206,7 @@ ASTNode BeevMgr::TransformFormula(const ASTNode& form)
                {
                        ASTVec c;
                        c.push_back(TransformFormula(simpleForm[0]));
-                       result = CreateNode(NOT, c);
+                       result = bm.CreateNode(NOT, c);
                        break;
                }
                case BVLT:
@@ -192,14 +222,14 @@ ASTNode BeevMgr::TransformFormula(const ASTNode& form)
                        ASTVec c;
                        c.push_back(TransformTerm(simpleForm[0]));
                        c.push_back(TransformTerm(simpleForm[1]));
-                       result = CreateNode(k, c);
+                       result = bm.CreateNode(k, c);
                        break;
                }
                case EQ:
                {
                        ASTNode term1 = TransformTerm(simpleForm[0]);
                        ASTNode term2 = TransformTerm(simpleForm[1]);
-                       result = CreateSimplifiedEQ(term1, term2);
+                       result = bm.CreateSimplifiedEQ(term1, term2);
                        break;
                }
                case AND:
@@ -219,7 +249,7 @@ ASTNode BeevMgr::TransformFormula(const ASTNode& form)
                                vec.push_back(o);
                        }
 
-                       result = CreateNode(k, vec);
+                       result = bm.CreateNode(k, vec);
                        break;
                }
                default:
@@ -229,17 +259,22 @@ ASTNode BeevMgr::TransformFormula(const ASTNode& form)
                        {
                                cerr << "The input is: " << simpleForm << endl;
                                cerr << "The valuewidth of input is : " << simpleForm.GetValueWidth() << endl;
-                               FatalError("TransformFormula: Illegal kind: ", ASTUndefined, k);
+                               FatalError("TransformFormula: Illegal kind: ", bm.CreateNode(UNDEFINED), k);
                        }
                        break;
        }
-       //assert(BVTypeCheckRecursive(result));
-       TransformMap[simpleForm] = result;
+
+       if (simpleForm.GetChildren().size() > 0)
+               (*TransformMap)[simpleForm] = result;
        return result;
 } //End of TransformFormula
 
-ASTNode BeevMgr::TransformTerm(const ASTNode& inputterm)
+ASTNode TransformTerm(const ASTNode& inputterm)
 {
+       assert(TransformMap != null);
+
+       BeevMgr& bm = inputterm.GetBeevMgr();
+
        ASTNode result;
        ASTNode term = inputterm;
 
@@ -247,7 +282,7 @@ ASTNode BeevMgr::TransformTerm(const ASTNode& inputterm)
        if (!is_Term_kind(k))
                FatalError("TransformTerm: Illegal kind: You have input a nonterm:", inputterm, k);
        ASTNodeMap::iterator iter;
-       if ((iter = TransformMap.find(term)) != TransformMap.end())
+       if ((iter = TransformMap->find(term)) != TransformMap->end())
                return iter->second;
        switch (k)
        {
@@ -267,7 +302,7 @@ ASTNode BeevMgr::TransformTerm(const ASTNode& inputterm)
                        FatalError("TransformTerm: this kind is not supported", term);
                        break;
                case READ:
-                       result = TransformArray(term);
+                       result = bm.TransformArray(term);
                        break;
                case ITE:
                {
@@ -278,7 +313,7 @@ ASTNode BeevMgr::TransformTerm(const ASTNode& inputterm)
                        thn = TransformTerm(thn);
                        els = TransformTerm(els);
                        //result = CreateTerm(ITE,term.GetValueWidth(),cond,thn,els);
-                       result = CreateSimplifiedTermITE(cond, thn, els);
+                       result = bm.CreateSimplifiedTermITE(cond, thn, els);
                        result.SetIndexWidth(term.GetIndexWidth());
                        break;
                }
@@ -295,7 +330,7 @@ ASTNode BeevMgr::TransformTerm(const ASTNode& inputterm)
                                o.push_back(TransformTerm(*it));
                        }
 
-                       result = CreateTerm(k, width, o);
+                       result = bm.CreateTerm(k, width, o);
                        result.SetIndexWidth(indexwidth);
 
                        Kind k = result.GetKind();
@@ -315,9 +350,9 @@ ASTNode BeevMgr::TransformTerm(const ASTNode& inputterm)
                                        // result is embedded unchanged inside the result.
 
                                        unsigned inputValueWidth = result.GetValueWidth();
-                                       ASTNode zero = CreateZeroConst(inputValueWidth);
-                                       ASTNode one = CreateOneConst(inputValueWidth);
-                                       result = CreateTerm(ITE, inputValueWidth, CreateNode(EQ, zero, bottom), one, result);
+                                       ASTNode zero = bm.CreateZeroConst(inputValueWidth);
+                                       ASTNode one = bm.CreateOneConst(inputValueWidth);
+                                       result = bm.CreateTerm(ITE, inputValueWidth, bm.CreateNode(EQ, zero, bottom), one, result);
                                }
                        }
                }
@@ -327,7 +362,8 @@ ASTNode BeevMgr::TransformTerm(const ASTNode& inputterm)
                        break;
        }
 
-       TransformMap[term] = result;
+       if (term.GetChildren().size() > 0)
+               (*TransformMap)[term] = result;
        if (term.GetValueWidth() != result.GetValueWidth())
                FatalError("TransformTerm: result and input terms are of different length", result);
        if (term.GetIndexWidth() != result.GetIndexWidth())
@@ -351,6 +387,8 @@ ASTNode BeevMgr::TransformTerm(const ASTNode& inputterm)
  */
 ASTNode BeevMgr::TransformArray(const ASTNode& term)
 {
+       assert(TransformMap != null);
+
        ASTNode result = term;
 
        const unsigned int width = term.GetValueWidth();
@@ -359,7 +397,7 @@ ASTNode BeevMgr::TransformArray(const ASTNode& term)
                FatalError("TransformArray: input term is of wrong kind: ", ASTUndefined);
 
        ASTNodeMap::iterator iter;
-       if ((iter = TransformMap.find(term)) != TransformMap.end())
+       if ((iter = TransformMap->find(term)) != TransformMap->end())
                return iter->second;
 
        //'term' is of the form READ(arrName, readIndex)
@@ -574,7 +612,7 @@ ASTNode BeevMgr::TransformArray(const ASTNode& term)
                        break;
        }
 
-       TransformMap[term] = result;
+       (*TransformMap)[term] = result;
        return result;
 } //end of TransformArray()
 

diff --git a/src/parser/smtlib.y b/src/parser/smtlib.y
index 36f84f5341699eb7a355e264bb8c156e32b85b36..c8b335926d8c8dbc4a1be7679e3fad2939c31470 100644 (file)
--- a/src/parser/smtlib.y
+++ b/src/parser/smtlib.y
@@ -776,7 +776,7 @@ an_nonbvconst_term:
       BEEV::ASTNode hi  =  BEEV::globalBeevMgr_for_parser->CreateBVConst(32, $3);
       BEEV::ASTNode low =  BEEV::globalBeevMgr_for_parser->CreateBVConst(32, $5);
       BEEV::ASTNode output = BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::BVEXTRACT, width, *$7,hi,low);
-      BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->SimplifyTerm(output));
+      BEEV::ASTNode * n = new BEEV::ASTNode(output);
       BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n);
       $$ = n;
       delete $7;

diff --git a/src/simplifier/simplifier.cpp b/src/simplifier/simplifier.cpp
index ba813035ba3362050ca9a52e7e1c17a00f4338ac..6e73afc04ccb794043e518e9ab8d8eae449a440c 100644 (file)
--- a/src/simplifier/simplifier.cpp
+++ b/src/simplifier/simplifier.cpp
@@ -1,4 +1,4 @@
-/********************************************************************
+                                       /********************************************************************
  * AUTHORS: Vijay Ganesh
  *
  * BEGIN DATE: November, 2005
@@ -35,8 +35,22 @@ bool BeevMgr::CheckSimplifyMap(const ASTNode& key, ASTNode& output, bool pushNeg
        return false;
 }
 
+// Push any reference count used by the key to the value.
 void BeevMgr::UpdateSimplifyMap(const ASTNode& key, const ASTNode& value, bool pushNeg)
 {
+       // If there are references to the key, add them to the references of the value.
+       ASTNodeCountMap::const_iterator itKey, itValue;
+       itKey = ReferenceCount->find(key);
+       if (itKey != ReferenceCount->end())
+       {
+               itValue = ReferenceCount->find(value);
+               if (itValue != ReferenceCount->end())
+                       (*ReferenceCount)[value] = itValue->second + itKey->second;
+               else
+                       (*ReferenceCount)[value] = itKey->second;
+       }
+
+
        if (pushNeg)
                (*SimplifyNegMap)[key] = value;
        else
@@ -138,10 +152,9 @@ int BeevMgr::TermOrder(const ASTNode& a, const ASTNode& b)
 
        //a is of the form READ(Arr,const), and b is const, or
        //a is of the form var, and b is const
-       if ((k1 == READ && a[0].GetKind() == SYMBOL && a[1].GetKind() == BVCONST && 
-            (k2 == BVCONST)))
-             // || 
-//           k2 == READ && b[0].GetKind() == SYMBOL && b[1].GetKind() == BVCONST)))
+       if ((k1 == READ && a[0].GetKind() == SYMBOL && a[1].GetKind() == BVCONST && (k2 == BVCONST)))
+               // ||
+               //            k2 == READ && b[0].GetKind() == SYMBOL && b[1].GetKind() == BVCONST)))
                return 1;
 
        if (SYMBOL == k1 && (BVCONST == k2 || TRUE == k2 || FALSE == k2))
@@ -199,9 +212,37 @@ ASTNode BeevMgr::SimplifyFormula_NoRemoveWrites(const ASTNode& b, bool pushNeg)
        return out;
 }
 
+void BeevMgr::BuildReferenceCountMap(const ASTNode& b)
+{
+       if (b.GetChildren().size() == 0)
+               return;
+
+       ASTNodeCountMap::iterator it, itend;
+
+       it = ReferenceCount->find(b);
+       if (it == ReferenceCount->end())
+       {
+               (*ReferenceCount)[b] = 1;
+       }
+       else
+       {
+               (*ReferenceCount)[b] = it->second + 1;
+               return;
+       }
+
+       const ASTVec& c = b.GetChildren();
+       ASTVec::const_iterator itC = c.begin();
+       ASTVec::const_iterator itendC = c.end();
+       for (; itC != itendC; itC++)
+       {
+               BuildReferenceCountMap(*itC);
+       }
+}
+
 ASTNode BeevMgr::SimplifyFormula_TopLevel(const ASTNode& b, bool pushNeg)
 {
        ResetSimplifyMaps();
+       BuildReferenceCountMap(b);
        ASTNode out = SimplifyFormula(b, pushNeg);
        ResetSimplifyMaps();
        return out;
@@ -209,8 +250,8 @@ ASTNode BeevMgr::SimplifyFormula_TopLevel(const ASTNode& b, bool pushNeg)
 
 ASTNode BeevMgr::SimplifyFormula(const ASTNode& b, bool pushNeg)
 {
-  if (!optimize_flag)
-    return b;
+       if (!optimize_flag)
+               return b;
 
        Kind kind = b.GetKind();
        if (BOOLEAN_TYPE != b.GetType())
@@ -283,8 +324,7 @@ ASTNode BeevMgr::SimplifyForFormula(const ASTNode& a, bool pushNeg) {
 ASTNode BeevMgr::SimplifyAtomicFormula(const ASTNode& a, bool pushNeg)
 {
        if (!optimize_flag)
-         return a;
-
+               return a;
 
        ASTNode output;
        if (CheckSimplifyMap(a, output, pushNeg))
@@ -554,7 +594,6 @@ ASTNode BeevMgr::PullUpITE(const ASTNode& in)
        return result;
 }
 
-
 //takes care of some simple ITE Optimizations in the context of equations
 ASTNode BeevMgr::ITEOpt_InEqs(const ASTNode& in)
 {
@@ -653,9 +692,9 @@ ASTNode BeevMgr::CreateSimplifiedEQ(const ASTNode& in1, const ASTNode& in2)
        Kind k2 = in2.GetKind();
 
        // if (!optimize_flag)
-//     {
-//             return CreateNode(EQ, in1, in2);
-//     }
+       //      {
+       //              return CreateNode(EQ, in1, in2);
+       //      }
 
        if (in1 == in2)
                //terms are syntactically the same
@@ -1117,7 +1156,7 @@ ASTNode BeevMgr::SimplifyIffFormula(const ASTNode& a, bool pushNeg)
 ASTNode BeevMgr::SimplifyIteFormula(const ASTNode& b, bool pushNeg)
 {
        if (!optimize_flag)
-         return b;
+               return b;
 
        ASTNode output;
        if (CheckSimplifyMap(b, output, pushNeg))
@@ -1253,10 +1292,9 @@ ASTNode BeevMgr::SimplifyTerm(const ASTNode& actualInputterm)
        //cout << "SimplifyTerm: input: " << a << endl;
        if (!optimize_flag)
        {
-         return inputterm;
+               return inputterm;
        }
 
-       
        ASTNode output;
        assert(BVTypeCheck(inputterm));
        //########################################
@@ -2921,6 +2959,14 @@ ASTNode BeevMgr::LhsMinusRhs(const ASTNode& eq)
                swap_flag = true;
        }
 
+       ASTNodeCountMap::const_iterator it;
+       it = ReferenceCount->find(lhs);
+       if (it != ReferenceCount->end())
+       {
+               if (it->second > 1)
+                       return eq;
+       }
+
        unsigned int len = lhs.GetValueWidth();
        ASTNode zero = CreateZeroConst(len);
        //right is -1*(rhs): Simplify(-1*rhs)
@@ -3518,8 +3564,8 @@ bool BeevMgr::BVConstIsOdd(const ASTNode& c)
 //The big substitution function
 ASTNode BeevMgr::CreateSubstitutionMap(const ASTNode& a)
 {
-        if (!wordlevel_solve_flag)
-         return a;
+       if (!wordlevel_solve_flag)
+               return a;
 
        ASTNode output = a;
        //if the variable has been solved for, then simply return it
@@ -3656,11 +3702,17 @@ bool BeevMgr::VarSeenInTerm(const ASTNode& var, const ASTNode& term)
 // clears() in particular.
 void BeevMgr::ResetSimplifyMaps()
 {
+       SimplifyMap->clear();
        delete SimplifyMap;
        SimplifyMap = new ASTNodeMap(INITIAL_SIMPLIFY_MAP_SIZE);
 
+       SimplifyNegMap->clear();
        delete SimplifyNegMap;
        SimplifyNegMap = new ASTNodeMap(INITIAL_SIMPLIFY_MAP_SIZE);
+
+       ReferenceCount->clear();
+       delete ReferenceCount;
+       ReferenceCount = new ASTNodeCountMap(INITIAL_SIMPLIFY_MAP_SIZE);
 }
 
 }