From 0cbe98937285acbca1c6dcef5a4bc78d790f2a90 Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Sun, 2 Jan 2011 03:57:50 +0000 Subject: [PATCH] Cleanup / Speedup. Unnecessary work was done when building the counter example. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1047 e59a4935-1847-0410-ae03-e826735625c1 --- .../AbsRefine_CounterExample.h | 22 +----- .../CounterExample.cpp | 77 ++++--------------- 2 files changed, 17 insertions(+), 82 deletions(-) diff --git a/src/absrefine_counterexample/AbsRefine_CounterExample.h b/src/absrefine_counterexample/AbsRefine_CounterExample.h index c8839c7..a1a8f8f 100644 --- a/src/absrefine_counterexample/AbsRefine_CounterExample.h +++ b/src/absrefine_counterexample/AbsRefine_CounterExample.h @@ -28,17 +28,6 @@ namespace BEEV // Data structure that holds the counterexample ASTNodeMap CounterExampleMap; - // This map for building/printing counterexamples. MINISAT - // returns values for each bit (a BVGETBIT Node), and this maps - // allows us to assemble the bits into bitvectors. - typedef HASHMAP< - ASTNode, - HASHMAP *, - ASTNode::ASTNodeHasher, - ASTNode::ASTNodeEqual> ASTtoBitvectorMap; - - ASTtoBitvectorMap _ASTNode_to_BitvectorMap; - // This memo map is used by the ComputeFormulaUsingModel() ASTNodeMap ComputeFormulaMap; @@ -71,7 +60,7 @@ namespace BEEV void CopySolverMap_To_CounterExample(void); //Converts a vector of bools to a BVConst - ASTNode BoolVectoBVConst(HASHMAP * w, unsigned int l); + ASTNode BoolVectoBVConst(const vector * w, const unsigned int l); //Converts MINISAT counterexample into an AST memotable (i.e. the //function populates the datastructure CounterExampleMap) @@ -179,15 +168,6 @@ namespace BEEV void ClearAllTables(void) { CounterExampleMap.clear(); - for (ASTtoBitvectorMap::iterator - it = _ASTNode_to_BitvectorMap.begin(), - itend = _ASTNode_to_BitvectorMap.end(); - it != itend; it++) - { - (it->second)->clear(); - delete (it->second); - } - _ASTNode_to_BitvectorMap.clear(); ComputeFormulaMap.clear(); } //End of ClearAllTables() diff --git a/src/absrefine_counterexample/CounterExample.cpp b/src/absrefine_counterexample/CounterExample.cpp index dfdf03f..6ca710f 100644 --- a/src/absrefine_counterexample/CounterExample.cpp +++ b/src/absrefine_counterexample/CounterExample.cpp @@ -30,13 +30,7 @@ namespace BEEV AbsRefine_CounterExample::ConstructCounterExample(SATSolver& newS, ToSATBase::ASTNodeToSATVar& satVarToSymbol) { - //iterate over MINISAT counterexample and construct a map from AST - //terms to vector of bools. We need this iteration step because - //MINISAT might return the various bits of a term out of - //order. Therfore, we need to collect all the bits and assemble - //them properly - - if (!newS.okay()) + if (!newS.okay()) return; if (!bm->UserFlags.construct_counterexample_flag) return; @@ -51,6 +45,10 @@ namespace BEEV const ASTNode& symbol = it->first; const vector& v = it->second; + const unsigned int symbolWidth = symbol.GetValueWidth(); + assert(symbol.GetKind() == SYMBOL); + vector bitVector_array(symbolWidth,false); + for (int index = 0; index < v.size(); index++) { const unsigned sat_variable_index = v[index]; @@ -64,35 +62,18 @@ namespace BEEV //assemble the counterexample here if (symbol.GetType() == BITVECTOR_TYPE) { - 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()) - { - _ASTNode_to_BitvectorMap[symbol] = new HASHMAP (symbolWidth); - } - - //v holds the map from bit-index to bit-value - v = _ASTNode_to_BitvectorMap[symbol]; - //Collect the bits of 'symbol' and store in v. Store //in reverse order. - if (newS.modelValue(sat_variable_index) == newS.true_literal() ) - (*v)[(symbolWidth - 1) - index] = true; - else - (*v)[(symbolWidth - 1) - index] = false; + bitVector_array[(symbolWidth - 1) - index] = (newS.modelValue(sat_variable_index) == newS.true_literal() ); } else { assert (symbol.GetType() == BOOLEAN_TYPE); - const char * zz = symbol.GetName(); + //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)) + //if (0 != strncmp("cnf", zz, 3) && 0 + // != strcmp("*TrueDummy*", zz)) { if (newS.modelValue(sat_variable_index) == newS.true_literal()) CounterExampleMap[symbol] = ASTTrue; @@ -103,33 +84,11 @@ namespace BEEV } } } - } - //iterate over the ASTNode_to_Bitvector data-struct and construct - //the the aggregate value of the bitvector, and populate the - //CounterExampleMap datastructure - for (ASTtoBitvectorMap::iterator it = _ASTNode_to_BitvectorMap.begin(), - itend = _ASTNode_to_BitvectorMap.end(); it != itend; it++) - { - ASTNode var = it->first; - //debugging - //cerr << var; - if (SYMBOL != var.GetKind()) - { - FatalError("ConstructCounterExample:" - "error while constructing counterexample: " - "not a variable: ", var); - } - //construct the bitvector value - HASHMAP * w = it->second; - ASTNode value = BoolVectoBVConst(w, var.GetValueWidth()); - //debugging - //cerr << value; - - //populate the counterexample datastructure. add only scalars - //variables which were declared in the input and newly - //introduced variables for array reads - CounterExampleMap[var] = value; + if (symbol.GetType() == BITVECTOR_TYPE) + { + CounterExampleMap[symbol] = BoolVectoBVConst(&bitVector_array, symbol.GetValueWidth()); + } } //In this loop, we compute the value of each array read, the @@ -902,20 +861,16 @@ namespace BEEV //FUNCTION: this function accepts a boolvector and returns a BVConst ASTNode - AbsRefine_CounterExample::BoolVectoBVConst(HASHMAP * w, - unsigned int l) + AbsRefine_CounterExample::BoolVectoBVConst(const vector * w, + const unsigned int l) { - if (l < (unsigned)w->size()) - FatalError("BoolVectorBVConst : " - "length of bitvector does not match HASHMAP size:", ASTUndefined, l); + assert (l == (unsigned)w->size()); CBV cc = CONSTANTBV::BitVector_Create(l,true); for (unsigned int jj = 0; jj < l; jj++) { if ((*w)[jj] == true) CONSTANTBV::BitVector_Bit_On(cc,l-1-jj); - else - CONSTANTBV::BitVector_Bit_Off(cc,l-1-jj); } return bm->CreateBVConst(cc,l); -- 2.47.3