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