Option currently disabled. To not use Tseitin variables as decision variables. On...

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

diff --git a/src/STPManager/UserDefinedFlags.h b/src/STPManager/UserDefinedFlags.h
index 8755b1ec2badde07d254ba792ee9d2c38743f337..b9beb3aac7c589c588d961ee79c960f4566a2f3b 100644 (file)
--- a/src/STPManager/UserDefinedFlags.h
+++ b/src/STPManager/UserDefinedFlags.h
@@ -86,6 +86,8 @@ namespace BEEV
     
     bool quick_statistics_flag;
   
+    bool tseitin_are_decision_variables_flag;
+
     //CONSTRUCTOR    
     UserDefinedFlags()
     {  
@@ -152,6 +154,8 @@ namespace BEEV
       division_by_zero_returns_one_flag = false;
       
       quick_statistics_flag=false;
+
+      tseitin_are_decision_variables_flag=true;
     } //End of constructor for UserDefinedFlags
 
   }; //End of struct UserDefinedFlags

diff --git a/src/to-sat/BitBlast.cpp b/src/to-sat/BitBlast.cpp
index 78d156adf9ddf40eaadf73995e7660523c392060..4193e4b5f953932bcc02f41fa4d6623adc422a55 100644 (file)
--- a/src/to-sat/BitBlast.cpp
+++ b/src/to-sat/BitBlast.cpp
@@ -748,9 +748,9 @@ namespace BEEV
   {
     // For some unexplained reason, XORs are faster than converting
     // them to cluases at this point
-    ASTNode S0 = _bm->CreateSimpForm(XOR, 
-                                     _bm->CreateSimpForm(XOR, xi, yi), 
-                                     cin);    
+    ASTNode S0 = _bm->CreateSimpForm(XOR,
+                                     _bm->CreateSimpForm(XOR, xi, yi),
+                                     cin);
     return S0;
     // ASTNode S1 = _bm->CreateSimpForm(OR,xi,yi,cin);
     //     ASTNode S2 = _bm->CreateSimpForm(OR,

diff --git a/src/to-sat/ToSAT.cpp b/src/to-sat/ToSAT.cpp
index 949d0648bc619785f515e86bf663f92087ca208e..1f774d59e2cbb529d3fc08b71164e141ee35dc86 100644 (file)
--- a/src/to-sat/ToSAT.cpp
+++ b/src/to-sat/ToSAT.cpp
@@ -10,10 +10,25 @@
 
 namespace BEEV
 {
-  /* FUNCTION: lookup or create a new MINISAT literal
-   * lookup or create new MINISAT Vars from the global MAP
-   * _ASTNode_to_SATVar.
-   */
+
+bool isTseitinVariable(const ASTNode& n) {
+       if (n.GetKind() == SYMBOL && n.GetType() == BOOLEAN_TYPE) {
+               const char * zz = n.GetName();
+               //if the variables ARE cnf variables then dont make them
+               // decision variables.
+               if (0 == strncmp("cnf", zz, 3))
+               {
+                       return true;
+               }
+       }
+       return false;
+}
+
+       /* FUNCTION: lookup or create a new MINISAT literal
+          * lookup or create new MINISAT Vars from the global MAP
+          * _ASTNode_to_SATVar.
+          */
+
   MINISAT::Var 
   ToSAT::LookupOrCreateSATVar(MINISAT::Solver& newS, const ASTNode& n)
   {
@@ -31,7 +46,14 @@ namespace BEEV
         //by 1 each time it is called, and the initial value of a
         //MINISAT::Var is 0.
         _SATVar_to_AST_Vector.push_back(n);
-      }
+
+        // experimental. Don't add Tseitin variables as decision variables.
+        if (!bm->UserFlags.tseitin_are_decision_variables_flag && isTseitinVariable(n))
+        {
+               newS.setDecisionVar(v,false);
+        }
+
+       }
     else
       v = it->second;
     return v;
@@ -103,7 +125,7 @@ namespace BEEV
         float percentage=CLAUSAL_ABSTRACTION_CUTOFF;
         if(count++ >= input_clauselist_size*percentage)
           {
-            //Arbitrary adding only 60% of the clauses in the hopes of
+               //Arbitrary adding only 60% of the clauses in the hopes of
             //terminating early 
             //      cout << "Percentage clauses added: " 
             //           << percentage << endl;
@@ -132,7 +154,6 @@ namespace BEEV
       } // End of For-loop adding the clauses 
 
     bm->GetRunTimes()->stop(RunTimes::SendingToSAT);
-    //cout << "Added remaining clauses\n";
     bm->GetRunTimes()->start(RunTimes::Solving);
     newS.solve();
     bm->GetRunTimes()->stop(RunTimes::Solving);

diff --git a/src/to-sat/ToSAT.h b/src/to-sat/ToSAT.h
index 4e10b6af198ef3ade618c8512ee35950fb44f569..c80f9c7dd26179ca2061da69d9e01701091c48d2 100644 (file)
--- a/src/to-sat/ToSAT.h
+++ b/src/to-sat/ToSAT.h
@@ -23,7 +23,7 @@
 
 namespace BEEV
 {
-  #define CLAUSAL_ABSTRACTION_CUTOFF 0.6
+  #define CLAUSAL_ABSTRACTION_CUTOFF 1.1
 
   class ToSAT {
   private: