Change how the counter example is built. Previously the counter example relied on...

I needed to reimplement the code to print the sat model too. I didn't preserve the format. I suspect though no one is parsing it.

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

diff --git a/src/absrefine_counterexample/CounterExample.cpp b/src/absrefine_counterexample/CounterExample.cpp
index da96c91e57602b0e0c30fe704e28bdea31ad7dd4..576a64ebebddf71c51812cc22bd80286acaed964 100644 (file)
--- a/src/absrefine_counterexample/CounterExample.cpp
+++ b/src/absrefine_counterexample/CounterExample.cpp
@@ -24,7 +24,7 @@ namespace BEEV
    * step2: Iterate over the map from ASTNodes->Vector-of-Bools and
    * populate the CounterExampleMap data structure (ASTNode -> BVConst)
    */
-  void 
+  void
   AbsRefine_CounterExample::ConstructCounterExample(MINISAT::Solver& newS)
   {
     //iterate over MINISAT counterexample and construct a map from AST
@@ -41,71 +41,63 @@ namespace BEEV
     assert(CounterExampleMap.size() == 0);
 
     CopySolverMap_To_CounterExample();
-    for (int i = 0; i < newS.nVars(); i++)
+
+    ToSAT::ASTNodeToVar m = tosat->SATVar_to_SymbolIndexMap();
+
+    for (ToSAT::ASTNodeToVar::const_iterator it = m.begin(); it != m.end(); it++)
       {
-        //Make sure that the MINISAT::Var is defined
-        if (newS.model[i] != MINISAT::l_Undef)
+        const ASTNode& symbol = it->first;
+        const vector<unsigned>& v = it->second;
+
+        for (int index = 0; index < v.size(); index++)
           {
+            const unsigned sat_variable_index = v[index];
+
+            if (sat_variable_index == ~((unsigned) 0)) // not sent to the sat solver.
+              continue;
 
-            //mapping from MINISAT::Vars to ASTNodes. We do not need to
-            //print MINISAT vars or CNF vars.
-            ASTNode s = tosat->SATVar_to_ASTMap(i);
+            if (newS.model[sat_variable_index] == MINISAT::l_Undef)
+              continue;
 
             //assemble the counterexample here
-            if (!s.IsNull() && s.GetKind() == BVGETBIT && s[0].GetKind() == SYMBOL)
+            if (symbol.GetType() == BITVECTOR_TYPE)
               {
-                const ASTNode& symbol = s[0];
                 const unsigned int symbolWidth = symbol.GetValueWidth();
 
                 //'v' is the map from bit-index to bit-value
                 HASHMAP<unsigned, bool> * v;
-                if (_ASTNode_to_BitvectorMap.find(symbol) == 
-                    _ASTNode_to_BitvectorMap.end())
+                if (_ASTNode_to_BitvectorMap.find(symbol)
+                    == _ASTNode_to_BitvectorMap.end())
                   {
-                    _ASTNode_to_BitvectorMap[symbol] = 
-                      new HASHMAP<unsigned, bool> (symbolWidth);
+                    _ASTNode_to_BitvectorMap[symbol] = new HASHMAP<unsigned,
+                        bool> (symbolWidth);
                   }
 
                 //v holds the map from bit-index to bit-value
                 v = _ASTNode_to_BitvectorMap[symbol];
 
-                //kk is the index of BVGETBIT
-                const unsigned int kk = s[1].GetUnsignedConst();
-
                 //Collect the bits of 'symbol' and store in v. Store
                 //in reverse order.
-                if (newS.model[i] == MINISAT::l_True)
-                  (*v)[(symbolWidth - 1) - kk] = true;
+                if (newS.model[sat_variable_index] == MINISAT::l_True)
+                  (*v)[(symbolWidth - 1) - index] = true;
                 else
-                  (*v)[(symbolWidth - 1) - kk] = false;
+                  (*v)[(symbolWidth - 1) - index] = false;
               }
             else
               {
-                if (!s.IsNull() && s.GetKind() == SYMBOL && s.GetType() == BOOLEAN_TYPE)
+                assert (symbol.GetType() == BOOLEAN_TYPE);
+                const char * zz = symbol.GetName();
+                //if the variables are not cnf variables then add
+                //them to the counterexample
+                if (0 != strncmp("cnf", zz, 3) && 0
+                    != strcmp("*TrueDummy*", zz))
                   {
-                    const char * zz = s.GetName();
-                    //if the variables are not cnf variables then add
-                    //them to the counterexample
-                    if (0 != strncmp("cnf", zz, 3) 
-                        && 0 != strcmp("*TrueDummy*", zz))
-                      {
-                        if (newS.model[i] == MINISAT::l_True)
-                          CounterExampleMap[s] = ASTTrue;
-                        else if (newS.model[i] == MINISAT::l_False)
-                          CounterExampleMap[s] = ASTFalse;
-                        else
-                          {
-                           if(bm->UserFlags.random_seed_flag)
-                             {
-                               int seed = bm->UserFlags.random_seed;
-                               srand(seed);
-                               CounterExampleMap[s] = 
-                                 (rand() > seed) ? ASTFalse : ASTTrue;
-                             }
-                           else
-                             CounterExampleMap[s] = ASTFalse;
-                          }
-                      }
+                    if (newS.model[sat_variable_index] == MINISAT::l_True)
+                      CounterExampleMap[symbol] = ASTTrue;
+                    else if (newS.model[sat_variable_index] == MINISAT::l_False)
+                      CounterExampleMap[symbol] = ASTFalse;
+                    else
+                      FatalError("never heres.");
                   }
               }
           }
@@ -890,30 +882,36 @@ namespace BEEV
   {
     if (!newS.okay())
       FatalError("PrintSATModel: NO COUNTEREXAMPLE TO PRINT", ASTUndefined);
-    // FIXME: Don't put tests like this in the print functions.  The
-    // print functions should print unconditionally.  Put a
-    // conditional around the call if you don't want them to print
-    if (!(bm->UserFlags.stats_flag 
+    if (!(bm->UserFlags.stats_flag
           && bm->UserFlags.print_nodes_flag))
       return;
 
-    int num_vars = newS.nVars();
+    ToSAT::ASTNodeToVar m = tosat->SATVar_to_SymbolIndexMap();
+
     cout << "Satisfying assignment: " << endl;
-    for (int i = 0; i < num_vars; i++)
-      {
-        ASTNode s = tosat->SATVar_to_ASTMap(i);
-        if (s.IsNull())
-               continue;
+    for (ToSAT::ASTNodeToVar::const_iterator it= m.begin(); it != m.end();it++)
+    {
+      ASTNode symbol = it->first;
+      vector<unsigned> v = it->second;
+
+      for (int i =0 ; i < v.size();i++)
+        {
+        if (v[i] == ~((unsigned)0)) // nb. special value.
+          continue;
 
-       if (newS.model[i] == MINISAT::l_True)
+        if (newS.model[v[i]] == MINISAT::l_True)
           {
-            cout << s << endl;
+            it->first.nodeprint(cout);
+            cout << " {" << i << "}"  << endl;
           }
-        else if (newS.model[i] == MINISAT::l_False)
+        else if (newS.model[v[i]] == MINISAT::l_False)
           {
-            cout << bm->CreateNode(NOT, s) << endl;
+          cout << "NOT ";
+          it->first.nodeprint(cout);
+          cout << " {" << i << "}"  << endl;
           }
-      }
+        }
+    }
   } //end of PrintSATModel()
 
   //FUNCTION: this function accepts a boolvector and returns a BVConst

diff --git a/src/to-sat/ToSAT.cpp b/src/to-sat/ToSAT.cpp
index 81eac9fe0bafa5b86a2c8e982a0846c294687f40..c1506368d299d839b98968878f49528de671eed0 100644 (file)
--- a/src/to-sat/ToSAT.cpp
+++ b/src/to-sat/ToSAT.cpp
@@ -48,7 +48,26 @@ namespace BEEV
         //ASSUMPTION: I am assuming that the newSolver.newVar() call increments v
         //by 1 each time it is called, and the initial value of a
         //MINISAT::Var is 0.
-        _SATVar_to_AST_Vector.push_back(n);
+
+        // Copies the symbol into the map that is used to build the counter example.
+        // For boolean we create a vector of size 1.
+        if (n.GetKind() == BVGETBIT && n[0].GetKind() == SYMBOL || (n.GetKind() == SYMBOL && !isTseitinVariable(n)))
+          {
+            const ASTNode& symbol = n.GetKind() == BVGETBIT ? n[0] : n;
+            const unsigned index = n.GetKind() == BVGETBIT ? n[1].GetUnsignedConst() : 0;
+            const unsigned width = n.GetKind() == BVGETBIT ? symbol.GetValueWidth(): 1;
+
+            if (SATVar_to_SymbolIndex.find(symbol) == SATVar_to_SymbolIndex.end())
+              {
+                // In the SAT solver these are signed...
+                vector<unsigned> vec(width,~((unsigned)0));
+                SATVar_to_SymbolIndex.insert(make_pair(symbol, vec));
+              }
+            assert(index < width);
+            assert(SATVar_to_SymbolIndex[symbol].size() > index);
+
+            SATVar_to_SymbolIndex[symbol][index] = v;
+          }
 
         // experimental. Don't add Tseitin variables as decision variables.
         if (!bm->UserFlags.tseitin_are_decision_variables_flag && isTseitinVariable(n))
@@ -224,17 +243,21 @@ namespace BEEV
     // Delete the cnf generator.
     if (final)
     {
-       for (int i =0; i < _SATVar_to_AST_Vector.size();i++)
-       {
-               ASTNode n = _SATVar_to_AST_Vector[i];
-               if (!n.IsNull() && isTseitinVariable(n))
-               {
-                       _ASTNode_to_SATVar_Map.erase(n);
-                       _SATVar_to_AST_Vector[i] = ASTNode();
-               }
-       }
-       delete cm;
-       cm = NULL;
+      ASTVec toDelete;
+
+      ASTtoSATMap::const_iterator it =_ASTNode_to_SATVar_Map.begin();
+      for (;it!=_ASTNode_to_SATVar_Map.end();it++)
+        {
+        ASTNode n = it->first;
+        if (!n.IsNull() && isTseitinVariable(n))
+          toDelete.push_back(n);
+        }
+
+      for (ASTVec::iterator it = toDelete.begin(); it!= toDelete.end();it++)
+        _ASTNode_to_SATVar_Map.erase(*it);
+
+      delete cm;
+      cm = NULL;
     }
 
 

diff --git a/src/to-sat/ToSAT.h b/src/to-sat/ToSAT.h
index 4a44dd4eba09e62e4411305a4ca22e907a2e78b5..53d860b8e4d861dc7e35ce4dbdda454d19f90f55 100644 (file)
--- a/src/to-sat/ToSAT.h
+++ b/src/to-sat/ToSAT.h
@@ -23,6 +23,14 @@
 namespace BEEV
 {
   class ToSAT {
+
+  public:
+    typedef HASHMAP<
+    ASTNode,
+    vector<unsigned>,
+    ASTNode::ASTNodeHasher,
+    ASTNode::ASTNodeEqual> ASTNodeToVar;
+
   private:
     /****************************************************************
      * Private Typedefs and Data                                    *
@@ -41,12 +49,12 @@ namespace BEEV
     ASTNode::ASTNodeEqual> ASTtoSATMap;
     ASTtoSATMap _ASTNode_to_SATVar_Map;
 
-    // MAP: This is a map from MINISAT::Vars to ASTNodes
+    // MAP: This is a map from  ASTNodes to MINISAT::Vars for SYMBOLS>
     //
     // Reverse map used in building counterexamples. MINISAT returns a
     // model in terms of MINISAT Vars, and this map helps us convert
     // it to a model over ASTNode variables.
-    vector<ASTNode> _SATVar_to_AST_Vector;
+    ASTNodeToVar SATVar_to_SymbolIndex;
 
     // Ptr to STPManager
     STPMgr * bm;
@@ -130,15 +138,15 @@ namespace BEEV
     //print the STP solver output
     void PrintOutput(SOLVER_RETURN_TYPE ret);
 
-    ASTNode SATVar_to_ASTMap(int i)
+    ASTNodeToVar& SATVar_to_SymbolIndexMap()
     {
-      return _SATVar_to_AST_Vector[i];
+      return SATVar_to_SymbolIndex;
     }
 
     void ClearAllTables(void)
     {
       _ASTNode_to_SATVar_Map.clear();
-      _SATVar_to_AST_Vector.clear();
+      SATVar_to_SymbolIndex.clear();
     }
 
     ~ToSAT()