Added EXCEPT construct for the FOR-construct

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

diff --git a/scripts/Makefile.common b/scripts/Makefile.common
index efd7c2028a7bb1eb3f09a7c4d854c65ee5493bec..ec455186b16e4b37749d5ea1a9a852b4d233e6cb 100644 (file)
--- a/scripts/Makefile.common
+++ b/scripts/Makefile.common
@@ -4,8 +4,8 @@
 #information always use full screen mode to view/edit this file in
 #emacs
 
-#OPTIMIZE = -g -pg # Debugging and gprof-style profiling
-OPTIMIZE = -g     # Debugging
+#OPTIMIZE = -g -pg           # Debugging and gprof-style profiling
+OPTIMIZE = -g                # Debugging
 OPTIMIZE = -O3 -DNDEBUG     # Maximum optimization
 
 CFLAGS_BASE = $(OPTIMIZE)

diff --git a/src/AST/AST.h b/src/AST/AST.h
index 7bbc83cce5b41bb68e2fd59aaebe6b4a3a5ee2c0..26ece48d6b63dbb6a9528a0e3a536aa9ac8dd59a 100644 (file)
--- a/src/AST/AST.h
+++ b/src/AST/AST.h
@@ -1288,7 +1288,7 @@ namespace BEEV
     void printCacheStatus();
 
     //from v8
-    int TopLevelSATAux(const ASTNode& query);
+    SOLVER_RETURN_TYPE TopLevelSATAux(const ASTNode& query);
 
     //##################################################
     //##################################################
@@ -1296,7 +1296,7 @@ namespace BEEV
     //accepts query and returns the answer. if query is valid, return
     //true, else return false. Automatically constructs counterexample
     //for invalid queries, and prints them upon request.
-    int TopLevelSAT(const ASTNode& query, const ASTNode& asserts);
+    SOLVER_RETURN_TYPE TopLevelSAT(const ASTNode& query, const ASTNode& asserts);
 
     // Debugging function to find problems in BitBlast and ToCNF.
     // See body in ToSAT.cpp for more explanation.
@@ -1446,7 +1446,7 @@ namespace BEEV
 
   public:
     //print the STP solver output
-    void PrintOutput(bool true_iff_valid);
+    void PrintOutput(SOLVER_RETURN_TYPE ret);
 
     //Converts MINISAT counterexample into an AST memotable (i.e. the
     //function populates the datastructure CounterExampleMap)

diff --git a/src/AST/printer/AssortedPrinters.cpp b/src/AST/printer/AssortedPrinters.cpp
index b6455de0adf38d0264106367c7b0bb48c691103c..c4a5879557cc2656dde2562f38283659fb29e066 100644 (file)
--- a/src/AST/printer/AssortedPrinters.cpp
+++ b/src/AST/printer/AssortedPrinters.cpp
@@ -287,8 +287,10 @@ namespace BEEV
   } //printCacheStatus()
 
   //This function prints the output of the STP solver
-  void BeevMgr::PrintOutput(bool true_iff_valid)
+  void BeevMgr::PrintOutput(SOLVER_RETURN_TYPE ret)
   {
+    bool true_iff_valid = (SOLVER_VALID == ret);
+
     if (print_output_flag)
       {
         if (smtlib_parser_flag)

diff --git a/src/AST/printer/PLPrinter.cpp b/src/AST/printer/PLPrinter.cpp
index c00271ab941d203e6639ee9114457e2c8c1f551f..de2587848e2138acd1d0a93966cb1a3331cb69fd 100644 (file)
--- a/src/AST/printer/PLPrinter.cpp
+++ b/src/AST/printer/PLPrinter.cpp
@@ -189,8 +189,11 @@ namespace printer
            PL_Print1(os, c[2], indentation, letize);
            os << ";";
            PL_Print1(os, c[3], indentation, letize);
-           os << "){ \n";
+           os << ";";
+           os << "EXCEPT ";
            PL_Print1(os, c[4], indentation, letize);
+           os << "){ \n";
+           PL_Print1(os, c[5], indentation, letize);
            os << "} \n";
          }
        break;

diff --git a/src/abstraction-refinement/AbstractionRefinement.cpp b/src/abstraction-refinement/AbstractionRefinement.cpp
index e830bf6b92ee9c533107abe6a0fda2d465e4404d..852a076ff12784b91c3bb63c8c423a1986686e44 100644 (file)
--- a/src/abstraction-refinement/AbstractionRefinement.cpp
+++ b/src/abstraction-refinement/AbstractionRefinement.cpp
@@ -281,7 +281,8 @@ namespace BEEV
       }
 
     //All for loops are true in the model
-    return CallSAT_ResultCheck(SatSolver, ASTTrue, original_input);
+    //return CallSAT_ResultCheck(SatSolver, ASTTrue, original_input);
+    return ret;
   } //end of SATBased_AllFiniteLoops_Refinement()
   
   
@@ -319,7 +320,8 @@ namespace BEEV
     int paramInit         = GetUnsignedConst(finiteloop[1]);
     int paramLimit        = GetUnsignedConst(finiteloop[2]);
     int paramIncrement    = GetUnsignedConst(finiteloop[3]);
-    ASTNode formulabody   = finiteloop[4];
+    ASTNode exceptFormula = finiteloop[4];
+    ASTNode formulabody   = finiteloop[5];
     int paramCurrentValue = paramInit;
 
     //Update ParamToCurrentValMap with parameter and its current
@@ -327,7 +329,7 @@ namespace BEEV
     (*ParamToCurrentValMap)[parameter] = 
       CreateBVConst(finiteloop[1].GetValueWidth(),paramCurrentValue);
     
-    SOLVER_RETURN_TYPE ret;
+    SOLVER_RETURN_TYPE ret = SOLVER_UNDECIDED;
     //Go recursively thru' all the FOR-constructs.
     if(FOR == formulabody.GetKind()) 
       { 
@@ -344,11 +346,9 @@ namespace BEEV
              }
 
 
-            //Update ParamToCurrentValMap with parameter and its current
-            //value
-            //
-            //FIXME: Possible leak since I am not freeing the previous
-            //'value' for the same 'key'
+            //Update ParamToCurrentValMap with parameter and its
+            //current value. FIXME: Possible leak since I am not
+            //freeing the previous 'value' for the same 'key'
             paramCurrentValue = paramCurrentValue + paramIncrement;
             (*ParamToCurrentValMap)[parameter] = 
              CreateBVConst(finiteloop[1].GetValueWidth(),paramCurrentValue);
@@ -361,27 +361,28 @@ namespace BEEV
        return ret;
       } //end of recursion FORs
 
-    //ASTVec forloopFormulaVector;
     //Expand the leaf level FOR-construct completely
+    //increment of paramCurrentValue done inside loop
     int ThisForLoopAllTrue = 0;
-    for(;paramCurrentValue < paramLimit;
-       //increment of paramCurrentValue done inside loop
-       ) 
+    for(;paramCurrentValue < paramLimit;) 
       {
         ASTNode currentFormula;
-        currentFormula = 
-         SimplifyFormula(formulabody, false, ParamToCurrentValMap);
-        
+       ASTNode currentExceptFormula =
+         SimplifyFormula(exceptFormula, false, ParamToCurrentValMap);
+       if(ASTTrue ==  currentExceptFormula)
+         {         
+           currentFormula = ASTTrue;
+         }
+       else 
+         {
+           currentFormula = 
+             SimplifyFormula(formulabody, false, ParamToCurrentValMap);
+         }
+
         //Check the currentformula against the model, and add it to the
         //SAT solver if it is false against the model
         if(ASTFalse == ComputeFormulaUsingModel(currentFormula)) 
           {
-            // forloopFormulaVector.push_back(currentFormula); ASTNode
-           //             forloopFormulas =
-           //             (forloopFormulaVector.size() != 1) ?
-           //             CreateNode(AND, forloopFormulaVector) :
-           //             forloopFormulaVector[0];
-            
             currentFormula = TransformFormula_TopLevel(currentFormula);
            SOLVER_RETURN_TYPE result = 
               CallSAT_ResultCheck(SatSolver, currentFormula, original_input);
@@ -446,7 +447,8 @@ namespace BEEV
     int paramInit         = GetUnsignedConst(finiteloop[1]);
     int paramLimit        = GetUnsignedConst(finiteloop[2]);
     int paramIncrement    = GetUnsignedConst(finiteloop[3]);
-    ASTNode formulabody   = finiteloop[4];
+    ASTNode exceptFormula = finiteloop[4];
+    ASTNode formulabody   = finiteloop[5];
     int paramCurrentValue = paramInit;
 
     //Update ParamToCurrentValMap with parameter and its current
@@ -474,11 +476,9 @@ namespace BEEV
                returnVec.push_back(ret);
              }
 
-            //Update ParamToCurrentValMap with parameter and its current
-            //value
-            //
-            //FIXME: Possible leak since I am not freeing the previous
-            //'value' for the same 'key'
+            //Update ParamToCurrentValMap with parameter and its
+            //current value. FIXME: Possible leak since I am not
+            //freeing the previous 'value' for the same 'key'
             paramCurrentValue = paramCurrentValue + paramIncrement;
             (*ParamToCurrentValMap)[parameter] = 
              CreateBVConst(finiteloop[1].GetValueWidth(),paramCurrentValue);
@@ -492,20 +492,35 @@ namespace BEEV
 
     ASTVec forloopFormulaVector;
     //Expand the leaf level FOR-construct completely
-    for(;paramCurrentValue < paramLimit;
-       //incrementing of paramCurrentValue is done inside loop
-       )
+    //incrementing of paramCurrentValue is done inside loop
+    for(;paramCurrentValue < paramLimit;)
       {
-        ASTNode currentFormula;
-        currentFormula = 
-         SimplifyFormula(formulabody, false, ParamToCurrentValMap);
-        
+       ASTNode currentFormula;
+
+       ASTNode currentExceptFormula =
+         SimplifyFormula(exceptFormula, false, ParamToCurrentValMap);
+       if(ASTTrue ==  currentExceptFormula)
+         {
+           currentFormula = ASTTrue;
+           //continue;
+         }
+       else 
+         {
+           currentFormula = 
+             SimplifyFormula(formulabody, false, ParamToCurrentValMap);
+         }
+
         if(checkusingmodel_flag) 
           {
-            //Check the currentformula against the model, and add it to the
-            //SAT solver if it is false against the model
-            if(ASTFalse == ComputeFormulaUsingModel(currentFormula)) 
-              return ASTFalse;
+            //Check the currentformula against the model, and return
+            //immediately
+           //cout << "Printing current Formula: " << currentFormula << "\n"; 
+           ASTNode computedForm = ComputeFormulaUsingModel(currentFormula);
+           //cout << "Printing computed Formula: " << computedForm << "\n"; 
+            if(ASTFalse == computedForm)
+             {
+               return ASTFalse;
+             }
           }
         else 
           {

diff --git a/src/main/main.cpp b/src/main/main.cpp
index 5a99df4802fa3750a2ff61c65500ffa527a20b0a..16cc0eb85823fd5d6d2b0ec2a21a24ccb96155c2 100644 (file)
--- a/src/main/main.cpp
+++ b/src/main/main.cpp
@@ -200,6 +200,7 @@ int main(int argc, char ** argv) {
       return 0;
     } //end of PrintBack if
 
-  GlobalBeevMgr->TopLevelSAT(asserts, query);
+  SOLVER_RETURN_TYPE ret = GlobalBeevMgr->TopLevelSAT(asserts, query);
+  GlobalBeevMgr->PrintOutput(ret);
   return 0;
 }//end of Main

diff --git a/src/parser/CVC.lex b/src/parser/CVC.lex
index 548bb6dc4e4e6721a191720c8f83136ecdca5ae6..30954d79ec2616002005656596d63b440e7d56ce 100644 (file)
--- a/src/parser/CVC.lex
+++ b/src/parser/CVC.lex
@@ -56,6 +56,7 @@ ANYTHING ({LETTER}|{DIGIT}|{OPCHAR})
 "NOR"           { return NOR_TOK;}
 "NOT"           { return NOT_TOK; }
 "FOR"           { return FOR_TOK; }
+"EXCEPT"        { return EXCEPT_TOK; }
 "OR"            { return OR_TOK; }
 "/="            { return NEQ_TOK; }
  ":="            { return ASSIGN_TOK;}

diff --git a/src/parser/CVC.y b/src/parser/CVC.y
index fc35e6d0e26e84a93a17b3fcb730b404b5478314..c163668079fd1598a159dc40f5fdced16a906d28 100644 (file)
--- a/src/parser/CVC.y
+++ b/src/parser/CVC.y
@@ -29,7 +29,7 @@
   int yyerror(const char *s) {
     cout << "syntax error: line " << cvclineno << "\n" << s << endl;    
     FatalError("");
-    return YY_EXIT_FAILURE;                    /* Dill: don't know what it should return */
+    return YY_EXIT_FAILURE;
   };
 %}
 
@@ -60,6 +60,7 @@
 %token OR_TOK                  "OR"
 %token NOT_TOK                 "NOT"
 %token FOR_TOK                 "FOR"
+%token EXCEPT_TOK              "EXCEPT"
 %token XOR_TOK                 "XOR"
 %token NAND_TOK                "NAND"
 %token NOR_TOK                 "NOR"
@@ -451,7 +452,7 @@ Formula             :     '(' Formula ')' { $$ = $2; }
                         delete $1;
                         delete $3;
                       }
-                |      FOR_TOK '(' ForDecl ';' BVCONST_TOK ';' BVCONST_TOK ';' BVCONST_TOK ')' '{' Formula '}'
+                |      FOR_TOK '(' ForDecl ';' BVCONST_TOK ';' BVCONST_TOK ';' BVCONST_TOK ';' EXCEPT_TOK Formula ')' '{' Formula '}'
                        {
                         //Allows a compact representation of
                         //parameterized set of formulas (bounded
@@ -473,6 +474,40 @@ Formula            :     '(' Formula ')' { $$ = $2; }
                         vec.push_back(*$7);
                         vec.push_back(*$9);
                         vec.push_back(*$12);
+                        vec.push_back(*$15);
+                        ASTNode * n = new ASTNode(GlobalBeevMgr->CreateNode(FOR,vec));
+                        GlobalBeevMgr->BVTypeCheck(*n);
+                        $$ = n;
+                        delete $3;
+                        delete $5;
+                        delete $7;
+                        delete $9;
+                        delete $12;                   
+                        delete $15;
+                       }
+               |      FOR_TOK '(' ForDecl ';' BVCONST_TOK ';' BVCONST_TOK ';' BVCONST_TOK ')' '{' Formula '}'
+                       {
+                        //Allows a compact representation of
+                        //parameterized set of formulas (bounded
+                        //universal quantification)
+                        //
+                        //parameter name (a variable)
+                        //
+                        //initial value (BVCONST)
+                        //
+                        //limit value (BVCONST)
+                        //
+                        //increment value (BVCONST)
+                        //
+                        //formula (it can be a nested forloop)                  
+                          
+                        ASTVec vec;
+                        vec.push_back(*$3);
+                        vec.push_back(*$5);
+                        vec.push_back(*$7);
+                        vec.push_back(*$9);
+                        vec.push_back(GlobalBeevMgr->CreateNode(FALSE));
+                        vec.push_back(*$12);
                         ASTNode * n = new ASTNode(GlobalBeevMgr->CreateNode(FOR,vec));
                         GlobalBeevMgr->BVTypeCheck(*n);
                         $$ = n;

diff --git a/src/simplifier/simplifier.cpp b/src/simplifier/simplifier.cpp
index d538f11083ae7ca83f45940b9e0729c7c747dec4..5e8f8647307660cc9cefa631632ed60490dac0d2 100644 (file)
--- a/src/simplifier/simplifier.cpp
+++ b/src/simplifier/simplifier.cpp
@@ -1322,7 +1322,8 @@ ASTNode Flatten(const ASTNode& a)
       {
         output = t1;
       }
-    else if (CheckAlwaysTrueFormMap(CreateNode(NOT, t0)) || (NOT == t0.GetKind() && CheckAlwaysTrueFormMap(t0[0])))
+    else if (CheckAlwaysTrueFormMap(CreateNode(NOT, t0)) || 
+            (NOT == t0.GetKind() && CheckAlwaysTrueFormMap(t0[0])))
       {
         output = t2;
       }
@@ -1408,7 +1409,7 @@ ASTNode Flatten(const ASTNode& a)
     if (CheckSubstitutionMap(inputterm, output))
       {
         //cout << "SolverMap:" << inputterm << " output: " << output << endl;
-        return SimplifyTerm(output);
+        return SimplifyTerm(output, VarConstMap);
       }
 
     if (CheckSimplifyMap(inputterm, output, false, VarConstMap))
@@ -1442,7 +1443,7 @@ ASTNode Flatten(const ASTNode& a)
           }
         if (CheckSolverMap(inputterm, output))
           {
-            return SimplifyTerm(output);
+            return SimplifyTerm(output, VarConstMap);
           }
         output = inputterm;
         break;
@@ -1523,7 +1524,7 @@ ASTNode Flatten(const ASTNode& a)
           //sort, and create BVPLUS/BVMULT and return
           for (ASTVec::iterator it = c.begin(), itend = c.end(); it != itend; it++)
             {
-              ASTNode aaa = SimplifyTerm(*it);
+              ASTNode aaa = SimplifyTerm(*it, VarConstMap);
               if (BVCONST == aaa.GetKind())
                 {
                   constkids.push_back(aaa);
@@ -1644,8 +1645,8 @@ ASTNode Flatten(const ASTNode& a)
       case BVSUB:
         {
           ASTVec c = inputterm.GetChildren();
-          ASTNode a0 = SimplifyTerm(inputterm[0]);
-          ASTNode a1 = SimplifyTerm(inputterm[1]);
+          ASTNode a0 = SimplifyTerm(inputterm[0], VarConstMap);
+          ASTNode a1 = SimplifyTerm(inputterm[1], VarConstMap);
           unsigned int l = inputValueWidth;
           if (a0 == a1)
             output = CreateZeroConst(l);
@@ -1654,8 +1655,8 @@ ASTNode Flatten(const ASTNode& a)
               //covert x-y into x+(-y) and simplify. this transformation
               //triggers more simplifications
               //
-              a1 = SimplifyTerm(CreateTerm(BVUMINUS, l, a1));
-              output = SimplifyTerm(CreateTerm(BVPLUS, l, a0, a1));
+              a1 = SimplifyTerm(CreateTerm(BVUMINUS, l, a1), VarConstMap);
+              output = SimplifyTerm(CreateTerm(BVPLUS, l, a0, a1), VarConstMap);
             }
           break;
         }
@@ -1666,7 +1667,7 @@ ASTNode Flatten(const ASTNode& a)
           //actually 0. One way to reveal this fact is to strip bvuminus
           //out, and replace with something else so that combineliketerms
           //can catch this fact.
-          ASTNode a0 = SimplifyTerm(inputterm[0]);
+          ASTNode a0 = SimplifyTerm(inputterm[0], VarConstMap);
           Kind k1 = a0.GetKind();
           unsigned int l = a0.GetValueWidth();
           ASTNode one = CreateOneConst(l);
@@ -1682,7 +1683,7 @@ ASTNode Flatten(const ASTNode& a)
               }
             case BVNEG:
               {
-                output = SimplifyTerm(CreateTerm(BVPLUS, l, a0[0], one));
+                output = SimplifyTerm(CreateTerm(BVPLUS, l, a0[0], one), VarConstMap);
                 break;
               }
             case BVMULT:
@@ -1703,7 +1704,7 @@ ASTNode Flatten(const ASTNode& a)
                        // not -(3*x).
                        if (BVCONST == a0[0].GetKind())
                        {
-                    ASTNode a00 = SimplifyTerm(CreateTerm(BVUMINUS, l, a0[0]));
+                    ASTNode a00 = SimplifyTerm(CreateTerm(BVUMINUS, l, a0[0]), VarConstMap);
                     output = CreateTerm(BVMULT, l, a00, a0[1]);
                   }
                        else
@@ -1723,25 +1724,25 @@ ASTNode Flatten(const ASTNode& a)
                 for (ASTVec::iterator it = c.begin(), itend = c.end(); it != itend; it++)
                   {
                     //Simplify(BVUMINUS(a1x1))
-                    ASTNode aaa = SimplifyTerm(CreateTerm(BVUMINUS, l, *it));
+                    ASTNode aaa = SimplifyTerm(CreateTerm(BVUMINUS, l, *it), VarConstMap);
                     o.push_back(aaa);
                   }
                 //simplify the bvplus
-                output = SimplifyTerm(CreateTerm(BVPLUS, l, o));
+                output = SimplifyTerm(CreateTerm(BVPLUS, l, o), VarConstMap);
                 break;
               }
             case BVSUB:
               {
                 //BVUMINUS(BVSUB(x,y)) <=> BVSUB(y,x)
-                output = SimplifyTerm(CreateTerm(BVSUB, l, a0[1], a0[0]));
+                output = SimplifyTerm(CreateTerm(BVSUB, l, a0[1], a0[0]), VarConstMap);
                 break;
               }
             case ITE:
               {
                 //BVUMINUS(ITE(c,t1,t2)) <==> ITE(c,BVUMINUS(t1),BVUMINUS(t2))
                 ASTNode c = a0[0];
-                ASTNode t1 = SimplifyTerm(CreateTerm(BVUMINUS, l, a0[1]));
-                ASTNode t2 = SimplifyTerm(CreateTerm(BVUMINUS, l, a0[2]));
+                ASTNode t1 = SimplifyTerm(CreateTerm(BVUMINUS, l, a0[1]), VarConstMap);
+                ASTNode t2 = SimplifyTerm(CreateTerm(BVUMINUS, l, a0[2]), VarConstMap);
                 output = CreateSimplifiedTermITE(c, t1, t2);
                 break;
               }
@@ -1758,7 +1759,7 @@ ASTNode Flatten(const ASTNode& a)
           //it is important to take care of wordlevel transformation in
           //BVEXTRACT. it exposes oppurtunities for later simplification
           //and solving (variable elimination)
-          ASTNode a0 = SimplifyTerm(inputterm[0]);
+          ASTNode a0 = SimplifyTerm(inputterm[0], VarConstMap);
           Kind k1 = a0.GetKind();
           unsigned int a_len = inputValueWidth;
 
@@ -1800,7 +1801,7 @@ ASTNode Flatten(const ASTNode& a)
                     //Apply the following rule:
                     // (t@u)[i:j] <==> u[i:j], if len(u) > i
                     //
-                    output = SimplifyTerm(CreateTerm(BVEXTRACT, a_len, u, i, j));
+                    output = SimplifyTerm(CreateTerm(BVEXTRACT, a_len, u, i, j), VarConstMap);
                   }
                 else if (len_a0 > i_val && j_val >= len_u)
                   {
@@ -1808,7 +1809,7 @@ ASTNode Flatten(const ASTNode& a)
                     // (t@u)[i:j] <==> t[i-len_u:j-len_u], if len(t@u) > i >= j >= len(u)
                     i = CreateBVConst(32, i_val - len_u);
                     j = CreateBVConst(32, j_val - len_u);
-                    output = SimplifyTerm(CreateTerm(BVEXTRACT, a_len, t, i, j));
+                    output = SimplifyTerm(CreateTerm(BVEXTRACT, a_len, t, i, j), VarConstMap);
                   }
                 else
                   {
@@ -1816,8 +1817,8 @@ ASTNode Flatten(const ASTNode& a)
                     // (t@u)[i:j] <==> t[i-len_u:0] @ u[len_u-1:j]
                     i = CreateBVConst(32, i_val - len_u);
                     ASTNode m = CreateBVConst(32, len_u - 1);
-                    t = SimplifyTerm(CreateTerm(BVEXTRACT, i_val - len_u + 1, t, i, zero));
-                    u = SimplifyTerm(CreateTerm(BVEXTRACT, len_u - j_val, u, m, j));
+                    t = SimplifyTerm(CreateTerm(BVEXTRACT, i_val - len_u + 1, t, i, zero), VarConstMap);
+                    u = SimplifyTerm(CreateTerm(BVEXTRACT, len_u - j_val, u, m, j), VarConstMap);
                     output = CreateTerm(BVCONCAT, a_len, t, u);
                   }
                 break;
@@ -1832,7 +1833,7 @@ ASTNode Flatten(const ASTNode& a)
                 for (ASTVec::iterator jt = c.begin(), jtend = c.end(); jt != jtend; jt++)
                   {
                     ASTNode aaa = *jt;
-                    aaa = SimplifyTerm(CreateTerm(BVEXTRACT, i_val + 1, aaa, i, zero));
+                    aaa = SimplifyTerm(CreateTerm(BVEXTRACT, i_val + 1, aaa, i, zero), VarConstMap);
                     o.push_back(aaa);
                   }
                 output = CreateTerm(a0.GetKind(), i_val + 1, o);
@@ -1852,8 +1853,8 @@ ASTNode Flatten(const ASTNode& a)
                 // (t op u)[i:j] <==> t[i:j] op u[i:j]
                 ASTNode t = a0[0];
                 ASTNode u = a0[1];
-                t = SimplifyTerm(CreateTerm(BVEXTRACT, a_len, t, i, j));
-                u = SimplifyTerm(CreateTerm(BVEXTRACT, a_len, u, i, j));
+                t = SimplifyTerm(CreateTerm(BVEXTRACT, a_len, t, i, j), VarConstMap);
+                u = SimplifyTerm(CreateTerm(BVEXTRACT, a_len, u, i, j), VarConstMap);
                 BVTypeCheck(t);
                 BVTypeCheck(u);
                 output = CreateTerm(k1, a_len, t, u);
@@ -1863,7 +1864,7 @@ ASTNode Flatten(const ASTNode& a)
               {
                 // (~t)[i:j] <==> ~(t[i:j])
                 ASTNode t = a0[0];
-                t = SimplifyTerm(CreateTerm(BVEXTRACT, a_len, t, i, j));
+                t = SimplifyTerm(CreateTerm(BVEXTRACT, a_len, t, i, j), VarConstMap);
                 output = CreateTerm(BVNEG, a_len, t);
                 break;
               }
@@ -1886,8 +1887,8 @@ ASTNode Flatten(const ASTNode& a)
             case ITE:
               {
                 ASTNode t0 = a0[0];
-                ASTNode t1 = SimplifyTerm(CreateTerm(BVEXTRACT, a_len, a0[1], i, j));
-                ASTNode t2 = SimplifyTerm(CreateTerm(BVEXTRACT, a_len, a0[2], i, j));
+                ASTNode t1 = SimplifyTerm(CreateTerm(BVEXTRACT, a_len, a0[1], i, j), VarConstMap);
+                ASTNode t2 = SimplifyTerm(CreateTerm(BVEXTRACT, a_len, a0[2], i, j), VarConstMap);
                 output = CreateSimplifiedTermITE(t0, t1, t2);
                 break;
               }
@@ -1901,7 +1902,7 @@ ASTNode Flatten(const ASTNode& a)
         }
       case BVNEG:
         {
-          ASTNode a0 = SimplifyTerm(inputterm[0]);
+          ASTNode a0 = SimplifyTerm(inputterm[0], VarConstMap);
           unsigned len = inputValueWidth;
           switch (a0.GetKind())
             {
@@ -1913,8 +1914,8 @@ ASTNode Flatten(const ASTNode& a)
               break;
               // case ITE: {
               //        ASTNode cond = a0[0];
-              //        ASTNode thenpart = SimplifyTerm(CreateTerm(BVNEG,len,a0[1]));
-              //        ASTNode elsepart = SimplifyTerm(CreateTerm(BVNEG,len,a0[2]));
+              //        ASTNode thenpart = SimplifyTerm(CreateTerm(BVNEG,len,a0[1]), VarConstMap);
+              //        ASTNode elsepart = SimplifyTerm(CreateTerm(BVNEG,len,a0[2]), VarConstMap);
               //        output = CreateSimplifiedTermITE(cond,thenpart,elsepart);
               //        break;
               //       }
@@ -1927,7 +1928,7 @@ ASTNode Flatten(const ASTNode& a)
 
       case BVZX:
         {
-          ASTNode a0 = SimplifyTerm(inputterm[0]);
+          ASTNode a0 = SimplifyTerm(inputterm[0], VarConstMap);
           if (a0.GetKind() == BVCONST)
             output = BVConstEvaluator(CreateTerm(BVZX, inputValueWidth, a0, inputterm[1]));
           else
@@ -1938,7 +1939,7 @@ ASTNode Flatten(const ASTNode& a)
       case BVSX:
         {
           //a0 is the expr which is being sign extended
-          ASTNode a0 = SimplifyTerm(inputterm[0]);
+          ASTNode a0 = SimplifyTerm(inputterm[0], VarConstMap);
           //a1 represents the length of the term BVSX(a0)
           ASTNode a1 = inputterm[1];
           //output length of the BVSX term
@@ -1985,7 +1986,7 @@ ASTNode Flatten(const ASTNode& a)
                     ASTVec o;
                     for (ASTVec::iterator it = c.begin(), itend = c.end(); it != itend; it++)
                       {
-                        ASTNode aaa = SimplifyTerm(CreateTerm(BVSX, len, *it, a1));
+                        ASTNode aaa = SimplifyTerm(CreateTerm(BVSX, len, *it, a1), VarConstMap);
                         o.push_back(aaa);
                       }
                     output = CreateTerm(a0.GetKind(), len, o);
@@ -1996,15 +1997,15 @@ ASTNode Flatten(const ASTNode& a)
               {
                 //if you have BVSX(m,BVSX(n,a)) then you can drop the inner
                 //BVSX provided m is greater than n.
-                a0 = SimplifyTerm(a0[0]);
+                a0 = SimplifyTerm(a0[0], VarConstMap);
                 output = CreateTerm(BVSX, len, a0, a1);
                 break;
               }
             case ITE:
               {
                 ASTNode cond = a0[0];
-                ASTNode thenpart = SimplifyTerm(CreateTerm(BVSX, len, a0[1], a1));
-                ASTNode elsepart = SimplifyTerm(CreateTerm(BVSX, len, a0[2], a1));
+                ASTNode thenpart = SimplifyTerm(CreateTerm(BVSX, len, a0[1], a1), VarConstMap);
+                ASTNode elsepart = SimplifyTerm(CreateTerm(BVSX, len, a0[2], a1), VarConstMap);
                 output = CreateSimplifiedTermITE(cond, thenpart, elsepart);
                 break;
               }
@@ -2028,7 +2029,7 @@ ASTNode Flatten(const ASTNode& a)
           bool constant = true;
           for (ASTVec::iterator it = c.begin(), itend = c.end(); it != itend; it++)
             {
-              ASTNode aaa = SimplifyTerm(*it);
+              ASTNode aaa = SimplifyTerm(*it, VarConstMap);
               if (BVCONST != aaa.GetKind())
                 {
                   constant = false;
@@ -2070,8 +2071,8 @@ ASTNode Flatten(const ASTNode& a)
         }
       case BVCONCAT:
         {
-          ASTNode t = SimplifyTerm(inputterm[0]);
-          ASTNode u = SimplifyTerm(inputterm[1]);
+          ASTNode t = SimplifyTerm(inputterm[0], VarConstMap);
+          ASTNode u = SimplifyTerm(inputterm[1], VarConstMap);
           Kind tkind = t.GetKind();
           Kind ukind = u.GetKind();
 
@@ -2118,7 +2119,7 @@ ASTNode Flatten(const ASTNode& a)
           bool constant = true;
           for (ASTVec::iterator it = c.begin(), itend = c.end(); it != itend; it++)
             {
-              ASTNode aaa = SimplifyTerm(*it);
+              ASTNode aaa = SimplifyTerm(*it, VarConstMap);
               if (BVCONST != aaa.GetKind())
                 {
                   constant = false;
@@ -2146,13 +2147,13 @@ ASTNode Flatten(const ASTNode& a)
               else if (ITE == inputterm[0].GetKind())
                 {
                   ASTNode cond = SimplifyFormula(inputterm[0][0], false, VarConstMap);
-                  ASTNode index = SimplifyTerm(inputterm[1]);
+                  ASTNode index = SimplifyTerm(inputterm[1], VarConstMap);
 
                   ASTNode read1 = CreateTerm(READ, inputValueWidth, inputterm[0][1], index);
                   ASTNode read2 = CreateTerm(READ, inputValueWidth, inputterm[0][2], index);
 
-                  read1 = SimplifyTerm(read1);
-                  read2 = SimplifyTerm(read2);
+                  read1 = SimplifyTerm(read1, VarConstMap);
+                  read2 = SimplifyTerm(read2, VarConstMap);
                   out1 = CreateSimplifiedTermITE(cond, read1, read2);
                 }
               else
@@ -2173,8 +2174,8 @@ ASTNode Flatten(const ASTNode& a)
       case ITE:
         {
           ASTNode t0 = SimplifyFormula(inputterm[0], false, VarConstMap);
-          ASTNode t1 = SimplifyTerm(inputterm[1]);
-          ASTNode t2 = SimplifyTerm(inputterm[2]);
+          ASTNode t1 = SimplifyTerm(inputterm[1], VarConstMap);
+          ASTNode t2 = SimplifyTerm(inputterm[2], VarConstMap);
           output = CreateSimplifiedTermITE(t0, t1, t2);
           break;
         }
@@ -2186,7 +2187,7 @@ ASTNode Flatten(const ASTNode& a)
           ASTVec o;
           for (ASTVec::iterator it = c.begin(), itend = c.end(); it != itend; it++)
             {
-              ASTNode aaa = SimplifyTerm(*it);
+              ASTNode aaa = SimplifyTerm(*it, VarConstMap);
               o.push_back(aaa);
             }
           output = CreateTerm(k, inputValueWidth, o);

diff --git a/src/to-sat/ToCNF.cpp b/src/to-sat/ToCNF.cpp
index 9e67212dbfc8195c8f09d6082a74eee1bcc32a53..3e5b3c9f6a3150597f5eaf4237c2a25ff2afbb53 100644 (file)
--- a/src/to-sat/ToCNF.cpp
+++ b/src/to-sat/ToCNF.cpp
@@ -1752,7 +1752,8 @@ namespace BEEV
 
   }; // end of CNFMgr class
 
-  int BeevMgr::TopLevelSAT(const ASTNode& inputasserts, const ASTNode& query)
+  SOLVER_RETURN_TYPE BeevMgr::TopLevelSAT(const ASTNode& inputasserts, 
+                                         const ASTNode& query)
   {
 
     ASTNode q = CreateNode(AND, inputasserts, CreateNode(NOT, query));
@@ -1793,7 +1794,7 @@ namespace BEEV
 
     if (!sat)
       {
-        PrintOutput(true);
+        //PrintOutput(true);
         return SOLVER_VALID;
       }
     else if (SatSolver.okay())
@@ -1818,7 +1819,7 @@ namespace BEEV
         if (ASTTrue == orig_result)
           {
             //CheckCounterExample(SatSolver.okay());
-            PrintOutput(false);
+            //PrintOutput(false);
             PrintCounterExample(SatSolver.okay());
             PrintCounterExample_InOrder(SatSolver.okay());
             return SOLVER_INVALID;
@@ -1841,7 +1842,7 @@ namespace BEEV
     else
       {
         //Control should never reach here
-        PrintOutput(true);
+        //PrintOutput(true);
         return SOLVER_ERROR;
       }
   } //end of CALLSAT_ResultCheck

diff --git a/src/to-sat/ToSAT.cpp b/src/to-sat/ToSAT.cpp
index ac85291541e16232f0d3de317c80f677329f2869..76232f011b83d39ebe14c1184d38d03c07783ad9 100644 (file)
--- a/src/to-sat/ToSAT.cpp
+++ b/src/to-sat/ToSAT.cpp
@@ -919,7 +919,7 @@ namespace BEEV
   //Acceps a query, calls the SAT solver and generates Valid/InValid.
   //if returned 0 then input is INVALID if returned 1 then input is
   //VALID if returned 2 then UNDECIDED
-  int BeevMgr::TopLevelSATAux(const ASTNode& inputasserts)
+  SOLVER_RETURN_TYPE BeevMgr::TopLevelSATAux(const ASTNode& inputasserts)
   {
     ASTNode inputToSAT = inputasserts;
     ASTNode orig_input = inputToSAT;