From: trevor_hansen Date: Mon, 28 Jun 2010 15:12:43 +0000 (+0000) Subject: Change how the counter example is built. Previously the counter example relied on... X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=dd29d5f74fe9bcd68b49f81f7fe7904cd165b38a;p=francis%2Fstp.git Change how the counter example is built. Previously the counter example relied on specific nodes existing that wont be created when we bitblast via AIGs. 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 da96c91..576a64e 100644 --- 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& 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 * 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 (symbolWidth); + _ASTNode_to_BitvectorMap[symbol] = new HASHMAP (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 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 81eac9f..c150636 100644 --- 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 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 4a44dd4..53d860b 100644 --- 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, + 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 _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()