Probably a refactor. This comments out the write-refinement loop that I broke >1...

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

diff --git a/src/STPManager/STP.cpp b/src/STPManager/STP.cpp
index 9c712225df5320852fd14a84c8b3c20fd8a0ecf9..13fbad617f273d35f2bbe45c97c5ce2bb4a3ab22 100644 (file)
--- a/src/STPManager/STP.cpp
+++ b/src/STPManager/STP.cpp
@@ -353,6 +353,7 @@ namespace BEEV {
         bm->ASTNodeStats("After AIG Core: ", simplified_solved_InputToSAT);
       }
 
+#if 0
     bm->ASTNodeStats("Before SimplifyWrites_Inplace begins: ", simplified_solved_InputToSAT);
 
     bm->SimplifyWrites_InPlace_Flag = true;
@@ -401,6 +402,7 @@ namespace BEEV {
     while (inputToSAT != simplified_solved_InputToSAT);
 
     bm->ASTNodeStats("After SimplifyWrites_Inplace: ", simplified_solved_InputToSAT);
+#endif
 
     if (bm->UserFlags.isSet("enable-unconstrained", "1"))
       {
@@ -534,6 +536,7 @@ namespace BEEV {
         return res;
       }
 
+    #if 0
     res = Ctr_Example->SATBased_ArrayWriteRefinement(NewSolver, original_input, satBase);
     if (SOLVER_UNDECIDED != res)
       {
@@ -553,18 +556,14 @@ namespace BEEV {
         CountersAndStats("print_func_stats", bm);
         return res;
       }
+    #endif
+
+    FatalError("TopLevelSTPAux: reached the end without proper conclusion:"
+      "either a divide by zero in the input or a bug in STP");
+    //bogus return to make the compiler shut up
+    return SOLVER_ERROR;
+
 
-//    if (!bm->UserFlags.num_absrefine_flag)
-      {
-        FatalError("TopLevelSTPAux: reached the end without proper conclusion:"
-          "either a divide by zero in the input or a bug in STP");
-        //bogus return to make the compiler shut up
-        return SOLVER_ERROR;
-      }
-  //  else
-      {
-       // return res;
-      }
   } //End of TopLevelSTPAux
 
 #if 0

diff --git a/src/absrefine_counterexample/AbsRefine_CounterExample.h b/src/absrefine_counterexample/AbsRefine_CounterExample.h
index 0fc69425e7a19cbda560d111373acda279129a02..c7437fc31836e15e9f2e26e326dd3321a5ddfc3e 100644 (file)
--- a/src/absrefine_counterexample/AbsRefine_CounterExample.h
+++ b/src/absrefine_counterexample/AbsRefine_CounterExample.h
@@ -130,12 +130,6 @@ namespace BEEV
                         ToSATBase* tosat,
                         bool refinement);
 
-    //creates array write axiom only for the input term or formula, if
-    //necessary. If there are no axioms to produce then it simply
-    //generates TRUE
-    ASTNode 
-    Create_ArrayWriteAxioms(const ASTNode& array_readoverwrite_term, 
-                            const ASTNode& array_newname);
     
     SOLVER_RETURN_TYPE 
     SATBased_ArrayReadRefinement(SATSolver& newS,
@@ -143,11 +137,21 @@ namespace BEEV
                                  const ASTNode& original_input,
                                  ToSATBase* tosat);
 
+#if 0
     SOLVER_RETURN_TYPE 
     SATBased_ArrayWriteRefinement(SATSolver& newS,
                                   const ASTNode& orig_input,
                                   ToSATBase *tosat);
 
+    //creates array write axiom only for the input term or formula, if
+    //necessary. If there are no axioms to produce then it simply
+    //generates TRUE
+    ASTNode
+    Create_ArrayWriteAxioms(const ASTNode& array_readoverwrite_term,
+                            const ASTNode& array_newname);
+
+#endif
+
     void ClearAllTables(void)
     {
       CounterExampleMap.clear();

diff --git a/src/absrefine_counterexample/AbstractionRefinement.cpp b/src/absrefine_counterexample/AbstractionRefinement.cpp
index 4de675602018cdd58630563fcd70ffc0277bd3a7..3209b6e4fa4fc93606a21903c31da9c6a2879ad4 100644 (file)
--- a/src/absrefine_counterexample/AbstractionRefinement.cpp
+++ b/src/absrefine_counterexample/AbstractionRefinement.cpp
@@ -418,6 +418,9 @@ namespace BEEV
     } //end of SATBased_ArrayReadRefinement
 
 
+#if 0
+    // This isn't currently wired up.
+
   /******************************************************************
    * ARRAY WRITE ABSTRACTION REFINEMENT
    *
@@ -497,5 +500,5 @@ namespace BEEV
     ASTNode arraywrite_axiom = simp->CreateSimplifiedEQ(lhs, rhs);
     return arraywrite_axiom;
   }//end of Create_ArrayWriteAxioms()
-
+#endif
 };// end of namespace BEEV

diff --git a/src/simplifier/simplifier.cpp b/src/simplifier/simplifier.cpp
index 5a883689dfdd24c46acfb836c672099c9fed1f74..fa3c59b80c66e042c230f08739f5b18bbaeea3e7 100644 (file)
--- a/src/simplifier/simplifier.cpp
+++ b/src/simplifier/simplifier.cpp
@@ -2872,8 +2872,10 @@ namespace BEEV
 
         //process only if not  in the substitution map. simplifymap
         //has been checked already
+#if 0
         if (!CheckSubstitutionMap(out1, out1) && out1.GetKind() == READ && WRITE == out1[0].GetKind())
           out1 = RemoveWrites_TopLevel(out1);
+#endif
 
         //it is possible that after all the procesing the READ term
         //reduces to READ(Symbol,const) and hence we should check the
@@ -3325,6 +3327,7 @@ namespace BEEV
     return output;
   } //end of distributemultoverplus()
 
+#if 0
   //converts the BVSX(len, a0) operator into ITE( check top bit,
   //extend a0 by 1, extend a0 by 0)
   ASTNode
@@ -3389,7 +3392,9 @@ namespace BEEV
     UpdateSimplifyMap(a, output, false);
     return output;
   } //end of ConvertBVSXToITE()
+#endif
 
+#if 0
   ASTNode
   Simplifier::RemoveWrites_TopLevel(const ASTNode& term)
   {
@@ -3412,6 +3417,7 @@ namespace BEEV
         return RemoveWrites(term);
       }
   } //end of RemoveWrites_TopLevel()
+#endif
 
   // recursively simplify things that are of type array.
 
@@ -3459,6 +3465,7 @@ namespace BEEV
     return output;
   }
 
+#if 0
   ASTNode
   Simplifier::SimplifyWrites_InPlace(const ASTNode& term, ASTNodeMap* VarConstMap)
   {
@@ -3605,6 +3612,7 @@ namespace BEEV
     return output;
   } //end of RemoveWrites()
 
+
   ASTNode
   Simplifier::ReadOverWrite_To_ITE(const ASTNode& term, ASTNodeMap* VarConstMap)
   {
@@ -3692,6 +3700,7 @@ namespace BEEV
     //UpdateSimplifyMap(term,output,false);
     return output;
   } //ReadOverWrite_To_ITE()
+#endif
 
   //compute the multiplicative inverse of the input
   ASTNode
@@ -3834,10 +3843,13 @@ namespace BEEV
     cerr << "SimplifyNegMap:" << SimplifyNegMap->size() << ":" << SimplifyNegMap->bucket_count() << endl;
     cerr << "AlwaysTrueFormSet" << AlwaysTrueHashSet.size() << ":" << AlwaysTrueHashSet.bucket_count() << endl;
     cerr << "MultInverseMap" << MultInverseMap.size() << ":" << MultInverseMap.bucket_count() << endl;
+
+#if 0
     cerr << "ReadOverWrite_NewName_Map" << ReadOverWrite_NewName_Map->size() << ":"
         << ReadOverWrite_NewName_Map->bucket_count() << endl;
     cerr << "NewName_ReadOverWrite_Map" << NewName_ReadOverWrite_Map.size() << ":"
         << NewName_ReadOverWrite_Map.bucket_count() << endl;
+#endif
     cerr << "substn_map" << substitutionMap.Return_SolverMap()->size() << ":"
         << substitutionMap.Return_SolverMap()->bucket_count() << endl;
 

diff --git a/src/simplifier/simplifier.h b/src/simplifier/simplifier.h
index 2aebf64c238b96bc3564dc59bb4e49cbd3004238..f3e938efc93744002fd18d0d2c82e2506d1dc455 100644 (file)
--- a/src/simplifier/simplifier.h
+++ b/src/simplifier/simplifier.h
@@ -41,11 +41,11 @@ namespace BEEV
 
     // For ArrayWrite Abstraction: map from read-over-write term to
     // newname.
-    ASTNodeMap * ReadOverWrite_NewName_Map;
+    //ASTNodeMap * ReadOverWrite_NewName_Map;
       
     // For ArrayWrite Refinement: Map new arraynames to
     // Read-Over-Write terms
-    ASTNodeMap NewName_ReadOverWrite_Map;
+    //ASTNodeMap NewName_ReadOverWrite_Map;
 
     //Ptr to STP Manager
     STPMgr * _bm;
@@ -73,7 +73,7 @@ namespace BEEV
     {
       SimplifyMap    = new ASTNodeMap(INITIAL_TABLE_SIZE);
       SimplifyNegMap = new ASTNodeMap(INITIAL_TABLE_SIZE);
-      ReadOverWrite_NewName_Map = new ASTNodeMap();
+      //ReadOverWrite_NewName_Map = new ASTNodeMap();
 
       ASTTrue  = bm->CreateNode(TRUE);
       ASTFalse = bm->CreateNode(FALSE);
@@ -86,7 +86,7 @@ namespace BEEV
     {
       delete SimplifyMap;
       delete SimplifyNegMap;
-      delete ReadOverWrite_NewName_Map;
+      //delete ReadOverWrite_NewName_Map;
       delete nf;
     }
 
@@ -213,7 +213,7 @@ namespace BEEV
     ASTNode DistributeMultOverPlus(const ASTNode& a,
                                    bool startdistribution = false);
 
-    ASTNode ConvertBVSXToITE(const ASTNode& a);
+    //ASTNode ConvertBVSXToITE(const ASTNode& a);
 
     ASTNode BVConstEvaluator(const ASTNode& t);
 
@@ -231,17 +231,19 @@ namespace BEEV
 
     ASTNode SimplifyArrayTerm(const ASTNode& term,ASTNodeMap* VarConstMap);
 
-    ASTNode ReadOverWrite_To_ITE(const ASTNode& term, 
-                                 ASTNodeMap* VarConstMap=NULL);
+    //ASTNode ReadOverWrite_To_ITE(const ASTNode& term,
+    //                              ASTNodeMap* VarConstMap=NULL);
 
     void printCacheStatus();
 
+#if 0
     //FIXME: Get rid of this horrible function
     const ASTNodeMap * ReadOverWriteMap()
     {
       return ReadOverWrite_NewName_Map;
     } // End of ReadOverWriteMap()
-      
+#endif
+
     bool hasUnappliedSubstitutions()
     {
       return substitutionMap.hasUnappliedSubstitutions();
@@ -262,8 +264,8 @@ namespace BEEV
     {
       SimplifyMap->clear();
       SimplifyNegMap->clear();
-      ReadOverWrite_NewName_Map->clear();
-      NewName_ReadOverWrite_Map.clear();
+      //ReadOverWrite_NewName_Map->clear();
+      //NewName_ReadOverWrite_Map.clear();
       AlwaysTrueHashSet.clear();
       MultInverseMap.clear();
       substitutionMap.clear();