1 
2 /*
3  * File InterpolantMinimizer.hpp.
4  *
5  * This file is part of the source code of the software program
6  * Vampire. It is protected by applicable
7  * copyright laws.
8  *
9  * This source code is distributed under the licence found here
10  * https://vprover.github.io/license.html
11  * and in the source directory
12  *
13  * In summary, you are allowed to use Vampire for non-commercial
14  * purposes but not allowed to distribute, modify, copy, create derivatives,
15  * or use in competitions.
16  * For other uses of Vampire please contact developers for a different
17  * licence, which we will make an effort to provide.
18  */
19 /**
20  * @file InterpolantMinimizer.hpp
21  * Defines class InterpolantMinimizer.
22  */
23 
24 #ifndef __InterpolantMinimizer__
25 #define __InterpolantMinimizer__
26 
27 #include "Lib/DHSet.hpp"
28 #include "Lib/Int.hpp"
29 #include "Lib/MapToLIFO.hpp"
30 #include "Lib/Stack.hpp"
31 
32 #include "Kernel/InferenceStore.hpp"
33 
34 #include "SMTFormula.hpp"
35 
36 namespace Shell {
37 
38 using namespace Lib;
39 using namespace Kernel;
40 
41 class InterpolantMinimizer
42 {
43 public:
44   enum OptimizationTarget
45   {
46     OT_WEIGHT,
47     OT_COUNT,
48     OT_QUANTIFIERS
49   };
50 
51   InterpolantMinimizer(OptimizationTarget target=OT_WEIGHT, bool noSlicing=false,
52       bool showStats=false, vstring statsPrefix="");
53   ~InterpolantMinimizer();
54 
55   typedef List<Unit*> UList;
56 
57   Formula* getInterpolant(Unit* refutation);
58 
59   typedef Signature::Symbol Symbol;
60 
61   void prettyPrint(Term* t, ostream& out);
62   void prettyPrint(Symbol* symb, ostream& out);
63   void prettyPrint(Formula* formula, ostream& out);
64 
65 
66 
67 private:
68   //proof tree traversing
69 
70   void traverse(Unit* refutationUnit);
71 
72   struct TraverseStackEntry;
73 
74   enum UnitState {
75     TRANSPARENT_PARENTS,
76     HAS_LEFT_PARENT,
77     HAS_RIGHT_PARENT
78   };
79 
80   struct UnitInfo
81   {
UnitInfoShell::InterpolantMinimizer::UnitInfo82     UnitInfo() : state(TRANSPARENT_PARENTS), isRefutation(false),
83 	isParentOfLeft(false), isParentOfRight(false), leadsToColor(false),
84 	leftSuccessors(0), rightSuccessors(0), transparentSuccessors(0) {}
85 
86     Color color;
87     Color inputInheritedColor;
88 
89     UnitState state;
90 
91     bool isRefutation;
92     bool isParentOfLeft;
93     bool isParentOfRight;
94 
95     /** True if unit has some non-transparent ancestor (doesn't need to be immediate) */
96     bool leadsToColor;
97 
98     //TODO: fix memory leak caused by these lists
99     List<Unit*>* leftSuccessors;
100     List<Unit*>* rightSuccessors;
101     List<Unit*>* transparentSuccessors;
102   };
103 
104   typedef DHMap<Unit*,UnitInfo> InfoMap;
105 
106   InfoMap _infos;
107 
108 private:
109   //here is the code related to generating the SMT problem
110 
111   struct ParentSummary
112   {
resetShell::InterpolantMinimizer::ParentSummary113     void reset() {
114       rParents.reset();
115       bParents.reset();
116       gParents.reset();
117     }
118 
119     Stack<vstring> rParents;
120     Stack<vstring> bParents;
121     Stack<vstring> gParents;
122   };
123 
124   enum PredType
125   {
126     /** Formula has red (i.e. left) color in its trace */
127     R,
128     /** Formula has blue (i.e. right) color in its trace */
129     B,
130     /** The trace of a formula is gray (i.e. transparent) */
131     G,
132     /** Formula is sliced off */
133     S,
134     /** Formula is a consequence of red symbol elimination */
135     RC,
136     /** Formula is a consequence of blue symbol elimination */
137     BC,
138     /** Red fringe */
139     RF,
140     /** Blue fringe */
141     BF,
142     /** Formula is in the digest */
143     D,
144     /** Atom appears is in the digest */
145     V
146   };
147 
148   SMTConstant pred(PredType t, vstring node);
149   SMTConstant costFunction();
150 
151   void addDistinctColorsFormula(vstring n);
152 
153   void addLeafNodePropertiesFormula(vstring n);
154   void addGreyNodePropertiesFormula(vstring n, ParentSummary& parents);
155   void addColoredParentPropertiesFormulas(vstring n, ParentSummary& parents);
156   void addNodeFormulas(vstring n, ParentSummary& parents);
157 
158   void addFringeFormulas(Unit* u);
159 
160 private:
161   //generating the weight-minimizing part of the problem
162 
163   void addAtomImplicationFormula(Unit* u);
164   void addCostFormula();
165 
166   void collectAtoms(FormulaUnit* f, Stack<vstring>& atoms);
167   vstring getComponentId(Clause* cl);
168   void collectAtoms(Unit* u, Stack<vstring>& atoms);
169 
170   class ClauseSplitter;
171 
172   DHMap<Clause*, vstring> _atomIds;
173   DHMap<vstring, vstring> _formulaAtomIds;
174 
175   typedef DHMap<vstring, unsigned> WeightMap;
176   WeightMap _atomWeights;
177 
178   DHMap<vstring,Unit*> _unitsById;
179 
180   ClauseSplitter* _splitter;
181 private:
182   //and here is the glue
183 
184   void collectSlicedOffNodes(SMTSolverResult& solverResult, DHSet<Unit*>& acc);
185 
186   vstring getUnitId(Unit* u);
187 
188   void addNodeFormulas(Unit* u);
189 
190   void addAllFormulas();
191 
192   OptimizationTarget _optTarget;
193   bool _noSlicing;
194   bool _showStats;
195   vstring _statsPrefix;
196   SMTBenchmark _resBenchmark;
197 };
198 
199 }
200 
201 #endif // __InterpolantMinimizer__
202