1 /******************************************************************** 2 * AUTHORS: Vijay Ganesh 3 * 4 * BEGIN DATE: November, 2005 5 * 6 Permission is hereby granted, free of charge, to any person obtaining a copy 7 of this software and associated documentation files (the "Software"), to deal 8 in the Software without restriction, including without limitation the rights 9 to use, copy, modify, merge, publish, distribute, sublicense, and/or sell 10 copies of the Software, and to permit persons to whom the Software is 11 furnished to do so, subject to the following conditions: 12 13 The above copyright notice and this permission notice shall be included in 14 all copies or substantial portions of the Software. 15 16 THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR 17 IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, 18 FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE 19 AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER 20 LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, 21 OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN 22 THE SOFTWARE. 23 ********************************************************************/ 24 25 #ifndef CTREXAMPLE_H 26 #define CTREXAMPLE_H 27 28 #include "stp/AST/AST.h" 29 #include "stp/AbsRefineCounterExample/ArrayTransformer.h" 30 #include "stp/STPManager/STPManager.h" 31 #include "stp/Simplifier/Simplifier.h" 32 #include "stp/ToSat/ToSATBase.h" 33 34 namespace stp 35 { 36 class AbsRefine_CounterExample // not copyable 37 { 38 private: 39 // Handy defs 40 ASTNode ASTTrue, ASTFalse, ASTUndefined; 41 42 // Data structure that holds the counterexample 43 ASTNodeMap CounterExampleMap; 44 45 // This memo map is used by the ComputeFormulaUsingModel() 46 ASTNodeMap ComputeFormulaMap; 47 48 // Ptr to STPManager 49 STPMgr* bm; 50 51 // Ptr to Simplifier 52 Simplifier* simp; 53 54 // Ptr to ArrayTransformer 55 ArrayTransformer* ArrayTransform; 56 57 // Checks if the counterexample is good. In order for the 58 // counterexample to be ok, every assert must evaluate to true 59 // w.r.t couner_example, and the query must evaluate to 60 // false. Otherwise we know that the counter_example is bogus. 61 void CheckCounterExample(bool t); 62 63 // Accepts a term and turns it into a constant-term w.r.t 64 // counter_example 65 ASTNode TermToConstTermUsingModel(const ASTNode& term, 66 bool ArrayReadFlag = true); 67 68 ASTNode Expand_ReadOverWrite_UsingModel(const ASTNode& term, 69 bool ArrayReadFlag = true); 70 71 void CopySolverMap_To_CounterExample(void); 72 73 // Converts a vector of bools to a BVConst 74 ASTNode BoolVectoBVConst(const vector<bool>* w, const unsigned int l); 75 76 // Converts MINISAT counterexample into an AST memotable (i.e. the 77 // function populates the datastructure CounterExampleMap) 78 void ConstructCounterExample(SATSolver& newS, 79 ToSATBase::ASTNodeToSATVar& satVarToSymbol); 80 81 // Prints MINISAT assigment one bit at a time, for debugging. 82 void PrintSATModel(SATSolver& S, ToSATBase::ASTNodeToSATVar& satVarToSymbol); 83 84 public: AbsRefine_CounterExample(STPMgr * b,Simplifier * s,ArrayTransformer * at)85 AbsRefine_CounterExample(STPMgr* b, Simplifier* s, ArrayTransformer* at) 86 : bm(b), simp(s), ArrayTransform(at) 87 { 88 ASTTrue = bm->CreateNode(TRUE); 89 ASTFalse = bm->CreateNode(FALSE); 90 ASTUndefined = bm->CreateNode(UNDEFINED); 91 } 92 93 // Prints the counterexample to stdout 94 void PrintCounterExample(bool t, std::ostream& os = std::cout); 95 void PrintCounterExampleSMTLIB2(std::ostream& os); 96 void PrintSMTLIB2(std::ostream& os, const ASTNode& n); 97 ClearCounterExampleMap(void)98 void ClearCounterExampleMap(void) { CounterExampleMap.clear(); } 99 ClearComputeFormulaMap(void)100 void ClearComputeFormulaMap(void) { ComputeFormulaMap.clear(); } 101 102 // Prints the counterexample to stdout 103 void PrintCounterExample_InOrder(bool t); 104 105 // queries the counterexample, and returns the value corresponding 106 // to e 107 ASTNode GetCounterExample(const ASTNode& e); 108 109 // queries the counterexample, and returns a vector of index-value pairs for e 110 vector<std::pair<ASTNode, ASTNode>> GetCounterExampleArray(bool t, 111 const ASTNode& e); 112 CounterExampleSize(void)113 int CounterExampleSize(void) const { return CounterExampleMap.size(); } 114 115 // FIXME: This is bloody dangerous function. Hack attack to take 116 // care of requests from users who want to store complete 117 // counter-examples in their own data structures. GetCompleteCounterExample()118 ASTNodeMap GetCompleteCounterExample() { return CounterExampleMap; } 119 120 // Computes the truth value of a formula w.r.t counter_example 121 ASTNode ComputeFormulaUsingModel(const ASTNode& form); 122 123 /**************************************************************** 124 * Array Refinement functions * 125 ****************************************************************/ 126 SOLVER_RETURN_TYPE 127 CallSAT_ResultCheck(SATSolver& SatSolver, const ASTNode& modified_input, 128 const ASTNode& original_input, ToSATBase* tosat, 129 bool refinement); 130 131 SOLVER_RETURN_TYPE 132 SATBased_ArrayReadRefinement(SATSolver& newS, const ASTNode& original_input, 133 ToSATBase* tosat); 134 135 void applyAllCongruenceConstraints(SATSolver& SatSolver, ToSATBase* tosat); 136 137 #if 0 138 SOLVER_RETURN_TYPE 139 SATBased_ArrayWriteRefinement(SATSolver& newS, 140 const ASTNode& orig_input, 141 ToSATBase *tosat); 142 143 //creates array write axiom only for the input term or formula, if 144 //necessary. If there are no axioms to produce then it simply 145 //generates TRUE 146 ASTNode 147 Create_ArrayWriteAxioms(const ASTNode& array_readoverwrite_term, 148 const ASTNode& array_newname); 149 150 #endif 151 ClearAllTables(void)152 void ClearAllTables(void) 153 { 154 CounterExampleMap.clear(); 155 ComputeFormulaMap.clear(); 156 } 157 ~AbsRefine_CounterExample()158 ~AbsRefine_CounterExample() { ClearAllTables(); } 159 }; 160 161 class CompleteCounterExample // not copyable 162 { 163 ASTNodeMap counterexample; 164 STPMgr* bv; 165 166 public: CompleteCounterExample(ASTNodeMap a,STPMgr * beev)167 CompleteCounterExample(ASTNodeMap a, STPMgr* beev) 168 : counterexample(a), bv(beev) 169 { 170 } GetCounterExample(ASTNode e)171 ASTNode GetCounterExample(ASTNode e) 172 { 173 if (BOOLEAN_TYPE == e.GetType() && SYMBOL != e.GetKind()) 174 { 175 FatalError("You must input a term or propositional variables\n", e); 176 } 177 if (counterexample.find(e) != counterexample.end()) 178 { 179 return counterexample[e]; 180 } 181 else 182 { 183 if (SYMBOL == e.GetKind() && BOOLEAN_TYPE == e.GetType()) 184 { 185 return bv->CreateNode(stp::FALSE); 186 } 187 188 if (SYMBOL == e.GetKind()) 189 { 190 ASTNode z = bv->CreateZeroConst(e.GetValueWidth()); 191 return z; 192 } 193 194 return e; 195 } 196 } 197 }; 198 } // end of namespace 199 #endif 200