Enable the simplifying node factory when parsing smt-lib format file.

BVConstEvaluator now does the logical operations too. I moved them over from CounterExample. I realise they no longer short-cut nicely, but don't believe it matters.

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

diff --git a/src/absrefine_counterexample/CounterExample.cpp b/src/absrefine_counterexample/CounterExample.cpp
index 35796be187ff1aeda197c42eea458a6957d2332a..4241a424c2d0b61ac76b64cc8d868248489eb291 100644 (file)
--- a/src/absrefine_counterexample/CounterExample.cpp
+++ b/src/absrefine_counterexample/CounterExample.cpp
@@ -404,9 +404,10 @@ namespace BEEV
         }
       default:
         {
-          ASTVec c = term.GetChildren();
+          const ASTVec& c = term.GetChildren();
           ASTVec o;
-          for (ASTVec::iterator
+                  o.reserve(c.size());
+          for (ASTVec::const_iterator
                  it = c.begin(), itend = c.end(); it != itend; it++)
             {
               ASTNode ff = TermToConstTermUsingModel(*it, ArrayReadFlag);
@@ -508,8 +509,8 @@ namespace BEEV
   ASTNode 
   AbsRefine_CounterExample::ComputeFormulaUsingModel(const ASTNode& form)
   {
-    ASTNode in = form;
-    Kind k = form.GetKind();
+    const ASTNode& in = form;
+    const Kind k = form.GetKind();
     if (!(is_Form_kind(k) && BOOLEAN_TYPE == form.GetType()))
       {
         FatalError(" ComputeConstFormUsingModel: "\
@@ -532,8 +533,7 @@ namespace BEEV
           }
       }
 
-    ASTNode t0, t1;
-    ASTNode output = ASTFalse;
+    ASTNode output = ASTUndefined;
     switch (k)
       {
       case TRUE:
@@ -570,106 +570,60 @@ namespace BEEV
       case BVSLT:
       case BVSLE:
       case BVSGT:
-      case BVSGE:
-        //convert form[0] into a constant term
-        t0 = TermToConstTermUsingModel(form[0], false);
-        //convert form[0] into a constant term
-        t1 = TermToConstTermUsingModel(form[1], false);
-        output = simp->BVConstEvaluator(bm->CreateNode(k, t0, t1));
-
-        //evaluate formula to false if bvdiv execption occurs while
-        //counterexample is being checked during refinement.
-        if (bm->bvdiv_exception_occured 
-            && bm->counterexample_checking_during_refinement)
-          {
-            output = ASTFalse;
-          }
-        break;
+      case BVSGE: {
+               ASTVec children;
+               children.reserve(form.Degree());
+
+               for (ASTVec::const_iterator it = form.begin(), itend = form.end(); it
+                               != itend; it++) {
+                       children.push_back(TermToConstTermUsingModel(*it, false));
+               }
+
+               output = simp->BVConstEvaluator(bm->CreateNode(k, children));
+
+               //evaluate formula to false if bvdiv execption occurs while
+               //counterexample is being checked during refinement.
+               if (bm->bvdiv_exception_occured
+                               && bm->counterexample_checking_during_refinement) {
+                       output = ASTFalse;
+               }
+
+       }
+      break;
+
       case NAND:
-        {
-          ASTNode o = ASTTrue;
-          for (ASTVec::const_iterator
-                 it = form.begin(), itend = form.end(); it != itend; it++)
-            if (ASTFalse == ComputeFormulaUsingModel(*it))
-              {
-                o = ASTFalse;
-                break;
-              }
-          if (o == ASTTrue)
-            output = ASTFalse;
-          else
-            output = ASTTrue;
-          break;
-        }
       case NOR:
-        {
-          ASTNode o = ASTFalse;
-          for (ASTVec::const_iterator
-                 it = form.begin(), itend = form.end(); it != itend; it++)
-            if (ASTTrue == ComputeFormulaUsingModel(*it))
-              {
-                o = ASTTrue;
-                break;
-              }
-          if (o == ASTTrue)
-            output = ASTFalse;
-          else
-            output = ASTTrue;
-          break;
-        }
       case NOT:
-        if (ASTTrue == ComputeFormulaUsingModel(form[0]))
-          output = ASTFalse;
-        else
-          output = ASTTrue;
-        break;
-      case OR:
-        for (ASTVec::const_iterator
-               it = form.begin(), itend = form.end(); it != itend; it++)
-          if (ASTTrue == ComputeFormulaUsingModel(*it))
-            output = ASTTrue;
-        break;
       case AND:
-        output = ASTTrue;
-        for (ASTVec::const_iterator
-               it = form.begin(), itend = form.end(); it != itend; it++)
-          {
-            if (ASTFalse == ComputeFormulaUsingModel(*it))
-              {
-                output = ASTFalse;
-                break;
-              }
-          }
-        break;
       case XOR:
-        t0 = ComputeFormulaUsingModel(form[0]);
-        t1 = ComputeFormulaUsingModel(form[1]);
-        if ((ASTTrue == t0 
-             && ASTTrue == t1) 
-            || (ASTFalse == t0 && ASTFalse == t1))
-          output = ASTFalse;
-        else
-          output = ASTTrue;
-        break;
       case IFF:
-        t0 = ComputeFormulaUsingModel(form[0]);
-        t1 = ComputeFormulaUsingModel(form[1]);
-        if ((ASTTrue == t0 && ASTTrue == t1) 
-            || (ASTFalse == t0 && ASTFalse == t1))
-          output = ASTTrue;
-        else
-          output = ASTFalse;
-        break;
       case IMPLIES:
-        t0 = ComputeFormulaUsingModel(form[0]);
-        t1 = ComputeFormulaUsingModel(form[1]);
-        if ((ASTFalse == t0) || (ASTTrue == t0 && ASTTrue == t1))
-          output = ASTTrue;
-        else
-          output = ASTFalse;
+      case OR:
+       {
+               ASTVec children;
+               children.reserve(form.Degree());
+
+               for (ASTVec::const_iterator it = form.begin(), itend = form.end(); it != itend; it++)
+               {
+                       children.push_back( ComputeFormulaUsingModel(*it));
+               }
+
+            output = simp->BVConstEvaluator(bm->CreateNode(k, children));
+
+            //evaluate formula to false if bvdiv execption occurs while
+            //counterexample is being checked during refinement.
+            if (bm->bvdiv_exception_occured
+                && bm->counterexample_checking_during_refinement)
+              {
+                output = ASTFalse;
+              }
+
+       }
         break;
+
       case ITE:
-        t0 = ComputeFormulaUsingModel(form[0]);
+      {
+         ASTNode t0 = ComputeFormulaUsingModel(form[0]);
         if (ASTTrue == t0)
           output = ComputeFormulaUsingModel(form[1]);
         else if (ASTFalse == t0)
@@ -677,6 +631,7 @@ namespace BEEV
         else
           FatalError("ComputeFormulaUsingModel: ITE: "\
                      "something is wrong with the formula: ", form);
+      }
         break;
       case PARAMBOOL:
         output = bm->NewParameterized_BooleanVar(form[0],form[1]);
@@ -687,12 +642,15 @@ namespace BEEV
         output = ASTTrue;
         break;
       default:
+         cerr << _kind_names[k];
         FatalError(" ComputeFormulaUsingModel: "\
                    "the kind has not been implemented", ASTUndefined);
         break;
       }
 
     //cout << "ComputeFormulaUsingModel output is:" << output << endl;
+    assert(ASTUndefined != output);
+    assert(output.isConstant());
     ComputeFormulaMap[form] = output;
     return output;
   }

diff --git a/src/main/main.cpp b/src/main/main.cpp
index b7f5f84918956d485ea65f603b1cdb7e60700aa4..bc70f3cae3b5a81e7e562869665d3823532cc4b7 100644 (file)
--- a/src/main/main.cpp
+++ b/src/main/main.cpp
@@ -336,10 +336,11 @@ int main(int argc, char ** argv) {
     {
          // Wrap a typchecking node factory around the default node factory.
          // every node created is typechecked.
-         TypeChecker nf(*bm->defaultNodeFactory,*bm);
+         SimplifyingNodeFactory simpNF(*bm->defaultNodeFactory,*bm);
+         TypeChecker nf(simpNF,*bm);
 
          // Changes need to be made to the constant evaluator to get this working.
-         //SimplifyingNodeFactory nf3(nf,*bm);
+
          ParserInterface pi(*bm, &nf);
          parserInterface = π
 

diff --git a/src/simplifier/consteval.cpp b/src/simplifier/consteval.cpp
index d809785e6a58be31cfd59fd146395e0c6bb61fff..58d2c2f810e4f0c55f5080d95904a13037729e82 100644 (file)
--- a/src/simplifier/consteval.cpp
+++ b/src/simplifier/consteval.cpp
@@ -1,6 +1,6 @@
 // -*- c++ -*-
 /********************************************************************
- * AUTHORS: Vijay Ganesh
+ * AUTHORS: Vijay Ganesh, Trevor Hansen
  *
  * BEGIN DATE: November, 2005
  *
@@ -21,6 +21,7 @@ namespace BEEV
     FatalError(ss.c_str(), t);
   }
 
+// Const evaluator logical and arithmetic operations.
   ASTNode Simplifier::BVConstEvaluator(const ASTNode& t)
   {
     ASTNode OutputNode;
@@ -37,18 +38,31 @@ namespace BEEV
     CBV tmp0 = NULL;
     CBV tmp1 = NULL;
 
+    ASTVec children;
+    children.reserve(t.Degree());
+    for (int i =0; i < t.Degree(); i++)
+    {
+       if (t[i].isConstant())
+               children.push_back(t[i]);
+       else
+               children.push_back(BVConstEvaluator(t[i]));
+    }
+
+    if ((t.Degree() ==2 || t.Degree() == 1) && t[0].GetType() == BITVECTOR_TYPE)
+    {
     //saving some typing. BVPLUS does not use these variables. if the
     //input BVPLUS has two nodes, then we want to avoid setting these
     //variables.
     if (1 == t.Degree())
       {
-        tmp0 = BVConstEvaluator(t[0]).GetBVConst();
+        tmp0 = children[0].GetBVConst();
       }
     else if (2 == t.Degree() && k != BVPLUS)
       {
-        tmp0 = BVConstEvaluator(t[0]).GetBVConst();
-        tmp1 = BVConstEvaluator(t[1]).GetBVConst();
+        tmp0 = children[0].GetBVConst();
+        tmp1 = children[1].GetBVConst();
       }
+       }
 
     switch (k)
       {
@@ -56,10 +70,9 @@ namespace BEEV
       case READ:
       case WRITE:
       case SYMBOL:
-        FatalError("BVConstEvaluator: term is not a constant-term", t);
+           FatalError("BVConstEvaluator: term is not a constant-term", t);
         break;
       case BVCONST:
-        //FIXME Handle this special case better
         OutputNode = t;
         break;
       case BVNEG:
@@ -72,7 +85,6 @@ namespace BEEV
       case BVSX:
         {
           output = CONSTANTBV::BitVector_Create(inputwidth, true);
-          //unsigned * out0 = BVConstEvaluator(t[0]).GetBVConst();
           unsigned t0_width = t[0].GetValueWidth();
           if (inputwidth == t0_width)
             {
@@ -106,7 +118,7 @@ namespace BEEV
           output = CONSTANTBV::BitVector_Create(inputwidth, true);
 
           // Number of bits to shift it.
-          ASTNode shiftNode = BVConstEvaluator(t[1]);
+          ASTNode shiftNode = children[1];
 
           bool msb = CONSTANTBV::BitVector_msb_(tmp0);
 
@@ -186,9 +198,9 @@ namespace BEEV
       case BVEXTRACT:
         {
           output = CONSTANTBV::BitVector_Create(inputwidth, true);
-          tmp0 = BVConstEvaluator(t[0]).GetBVConst();
-          unsigned int hi = GetUnsignedConst(BVConstEvaluator(t[1]));
-          unsigned int low = GetUnsignedConst(BVConstEvaluator(t[2]));
+          tmp0 = children[0].GetBVConst();
+          unsigned int hi = GetUnsignedConst(children[1]);
+          unsigned int low = GetUnsignedConst(children[2]);
           unsigned int len = hi - low + 1;
 
           CONSTANTBV::BitVector_Destroy(output);
@@ -203,8 +215,8 @@ namespace BEEV
         {
           assert(2==t.Degree());
           output = CONSTANTBV::BitVector_Create(inputwidth, true);
-          unsigned t0_width = t[0].GetValueWidth();
-          unsigned t1_width = t[1].GetValueWidth();
+          unsigned t0_width = children[0].GetValueWidth();
+          unsigned t1_width = children[1].GetValueWidth();
           CONSTANTBV::BitVector_Destroy(output);
 
           output = CONSTANTBV::BitVector_Concat(tmp0, tmp1);
@@ -234,10 +246,9 @@ namespace BEEV
         {
           output = CONSTANTBV::BitVector_Create(inputwidth, true);
           bool carry = false;
-          ASTVec c = t.GetChildren();
-          for (ASTVec::iterator it = c.begin(), itend = c.end(); it != itend; it++)
+          for (ASTVec::iterator it = children.begin(), itend = children.end(); it != itend; it++)
             {
-              CBV kk = BVConstEvaluator(*it).GetBVConst();
+              CBV kk = (*it).GetBVConst();
               CONSTANTBV::BitVector_add(output, output, kk, &carry);
               carry = false;
               //CONSTANTBV::BitVector_Destroy(kk);
@@ -468,12 +479,10 @@ namespace BEEV
         }
       case ITE:
         {
-          ASTNode tmp0 = t[0]; // Should this run BVConstEvaluator??
-
-          if (ASTTrue == tmp0)
-            OutputNode = BVConstEvaluator(t[1]);
-          else if (ASTFalse == tmp0)
-            OutputNode = BVConstEvaluator(t[2]);
+          if (ASTTrue == t[0])
+            OutputNode = children[1];
+          else if (ASTFalse == t[0])
+            OutputNode = children[2];
           else
             {
               cerr << tmp0;
@@ -547,6 +556,121 @@ namespace BEEV
             OutputNode = ASTFalse;
           break;
         }
+        
+              case TRUE:
+         OutputNode = ASTTrue;
+         break;
+      case FALSE:
+         OutputNode = ASTFalse;
+          break;
+      case NOT:
+                         if (ASTTrue == t[0])
+                                 return ASTFalse;
+                         else if (ASTFalse == t[0])
+                                 return ASTTrue;
+                         else
+                                 {
+                                 cerr << ASTFalse;
+                                 cerr << t[0];
+                                 FatalError("BVConstEvaluator: unexpected not input", t);
+                                 }
+
+      case OR:
+         OutputNode = ASTFalse;
+        for (ASTVec::const_iterator it = children.begin(), itend = children.end(); it != itend; it++)
+          if (ASTTrue == *it)
+                 OutputNode = ASTTrue;
+
+
+        break;
+
+      case NOR:
+       {
+               ASTNode o = ASTFalse;
+               for (ASTVec::const_iterator it = children.begin(), itend =
+                               children.end(); it != itend; it++)
+                       if (ASTTrue == (*it)) {
+                               o = ASTTrue;
+                               break;
+                       }
+               if (o == ASTTrue)
+                       OutputNode = ASTFalse;
+               else
+                       OutputNode = ASTTrue;
+               break;
+       }
+
+
+      case XOR:
+      {
+       bool output = false;
+               for (ASTVec::const_iterator it = children.begin(), itend =
+                               children.end(); it != itend; it++)
+               {
+                       if (ASTTrue == *it)
+                               output = !output; //parity.
+               }
+
+               if (output)
+                       OutputNode = ASTTrue;
+               else
+                       OutputNode = ASTFalse;
+
+               break;
+
+
+      }
+
+      case AND:
+      {
+         OutputNode = ASTTrue;
+      for (ASTVec::const_iterator it = children.begin(), itend = children.end(); it != itend; it++)
+              {
+                if (ASTFalse == (*it))
+                  {
+                    OutputNode = ASTFalse;
+                    break;
+                  }
+              }
+            break;
+      }
+
+      case NAND:
+      { OutputNode = ASTFalse;
+      for (ASTVec::const_iterator it = children.begin(), itend = children.end(); it != itend; it++)
+              {
+                if (ASTFalse == (*it))
+                  {
+                    OutputNode = ASTTrue;
+                    break;
+                  }
+              }
+            break;
+      }
+
+
+      case IFF:
+      {
+         const ASTNode&  t0 = children[0];
+         const ASTNode&  t1 = children[1];
+             if ((ASTTrue == t0 && ASTTrue == t1) || (ASTFalse == t0 && ASTFalse == t1))
+               OutputNode = ASTTrue;
+             else
+               OutputNode = ASTFalse;
+             break;
+      }
+
+      case IMPLIES:
+      {
+               const ASTNode& t0 = children[0];
+               const ASTNode& t1 = children[1];
+               if ((ASTFalse == t0) || (ASTTrue == t0 && ASTTrue == t1))
+                       OutputNode = ASTTrue;
+               else
+                       OutputNode = ASTFalse;
+               break;
+       }
+        
       default:
         FatalError("BVConstEvaluator: The input kind is not supported yet:", t);
         break;
@@ -561,6 +685,7 @@ namespace BEEV
       cerr<<endl<<"------------------------"<<endl;
       }
     */
+    assert(OutputNode.isConstant());
     UpdateSolverMap(t, OutputNode);
     //UpdateSimplifyMap(t,OutputNode,false);
     return OutputNode;

diff --git a/src/simplifier/simplifier.h b/src/simplifier/simplifier.h
index 6404342b16dcce06b78bb71016f78b0d938d769d..0a8a876a14f43c2d2fc7539556c67940020f991f 100644 (file)
--- a/src/simplifier/simplifier.h
+++ b/src/simplifier/simplifier.h
@@ -213,10 +213,8 @@ namespace BEEV
 
     ASTNode ConvertBVSXToITE(const ASTNode& a);
 
-    //accepts constant term and simplifies it to a bvconst
     ASTNode BVConstEvaluator(const ASTNode& t);
 
-
     //checks if the input constant is odd or not
     bool BVConstIsOdd(const ASTNode& c);