Add the --config_full_bvsolve=1 option. With this option enabled, I know of no other...

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

diff --git a/src/STPManager/UserDefinedFlags.h b/src/STPManager/UserDefinedFlags.h
index db38a4a68b22f6f5e6f41373fa1e654fe3e46b9a..7350eecec28fb09b837bbcf323745cc62e90f129 100644 (file)
--- a/src/STPManager/UserDefinedFlags.h
+++ b/src/STPManager/UserDefinedFlags.h
@@ -153,6 +153,12 @@ namespace BEEV
        return get(n,"");
     }
 
+    // "1" is set.
+    bool isSet(string n, string def)
+    {
+       return (get(n,def) == string("1"));
+    }
+
     string get(string n, string def)
     {
        if (config_options.empty())

diff --git a/src/simplifier/bvsolver.cpp b/src/simplifier/bvsolver.cpp
index c98e2983b6db407b9ccef99c287f61cb3f8f007b..a5509bd9f7a890109aa06de6eb7a07ecc39ff45a 100644 (file)
--- a/src/simplifier/bvsolver.cpp
+++ b/src/simplifier/bvsolver.cpp
@@ -643,7 +643,8 @@ namespace BEEV
         != and_end; and_child++)
       {
 
-      ASTNode r = solveForXOR(!changed?*and_child:_simp->SimplifyFormula(_simp->applySubstitutionMapUntilArrays(*and_child),false,NULL));
+      ASTNode r = solveForXOR(!changed?*and_child:_simp->SimplifyFormula(completelySubstitute? _simp->applySubstitutionMap(*and_child)
+                 : _simp->applySubstitutionMapUntilArrays(*and_child),false,NULL));
       if (r!=*and_child)
         changed=true;
       output_children.push_back(r);
@@ -659,14 +660,10 @@ namespace BEEV
   //the formula
   ASTNode BVSolver::TopLevelBVSolve(const ASTNode& _input)
   {
-    //    if (!wordlevel_solve_flag)
-    //       {
-    //         return input;
-    //       }
+      completelySubstitute = _bm->UserFlags.isSet("full_bvsolve","0");
+      assert (_bm->UserFlags.wordlevel_solve_flag);
          ASTNode input = _input;
 
-
-
     ASTNode output = input;
     if (CheckAlreadySolvedMap(input, output))
       {
@@ -674,6 +671,10 @@ namespace BEEV
         return output;
       }
 
+    if (completelySubstitute)
+       input = _simp->applySubstitutionMap(input);
+
+
     Kind k = input.GetKind();
     if (XOR ==k && _bm->UserFlags.solve_for_XORS_flag)
     {
@@ -737,7 +738,10 @@ namespace BEEV
         b = write(A,b,b),
         which shouldn't be simplified.
           */
-        ASTNode aaa = (any_solved && EQ == it->GetKind()) ? _simp->SimplifyFormula(_simp->applySubstitutionMapUntilArrays(*it),false,NULL) : *it;
+
+       ASTNode aaa = (any_solved && EQ == it->GetKind()) ? _simp->SimplifyFormula
+                       (completelySubstitute ? _simp->applySubstitutionMap(*it):
+                       _simp->applySubstitutionMapUntilArrays(*it),false,NULL) : *it;
 
         if (ASTFalse == aaa)
         {
@@ -795,7 +799,11 @@ namespace BEEV
 
     // Imagine in the last conjunct A is replaced by B. But there could
     // be variable A's in the first conjunct. This gets rid of 'em.
-    output = _simp->applySubstitutionMapUntilArrays(output);
+    if (completelySubstitute)
+       output = _simp->applySubstitutionMap(output);
+    else
+       output = _simp->applySubstitutionMapUntilArrays(output);
+
 
     UpdateAlreadySolvedMap(_input, output);
     _bm->GetRunTimes()->stop(RunTimes::BVSolver);

diff --git a/src/simplifier/bvsolver.h b/src/simplifier/bvsolver.h
index 7e65615e8481c7ff48d7480a7646efb5f209fdda..981126fc34381f1073f436555d3eb33d17ece478 100644 (file)
--- a/src/simplifier/bvsolver.h
+++ b/src/simplifier/bvsolver.h
@@ -144,6 +144,10 @@ namespace BEEV
     //else returns FALSE
     bool CheckAlreadySolvedMap(const ASTNode& key, ASTNode& output);
 
+    // If array terms contain variables that have been substituted for, then , it breaks.
+    // However, completely substituting is extremely expensive to do. And only rarely necessary.
+    // With this option enabled, it will do it properly. And slowly!!
+    bool completelySubstitute;
 
   public:
     //constructor