1 /*********************                                                        */
2 /*! \file theory_bv.h
3  ** \verbatim
4  ** Top contributors (to current version):
5  **   Liana Hadarean, Tim King, Andrew Reynolds
6  ** This file is part of the CVC4 project.
7  ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
8  ** in the top-level source directory) and their institutional affiliations.
9  ** All rights reserved.  See the file COPYING in the top-level source
10  ** directory for licensing information.\endverbatim
11  **
12  ** \brief Bitvector theory.
13  **
14  ** Bitvector theory.
15  **/
16 
17 #include "cvc4_private.h"
18 
19 #ifndef __CVC4__THEORY__BV__THEORY_BV_H
20 #define __CVC4__THEORY__BV__THEORY_BV_H
21 
22 #include <unordered_map>
23 #include <unordered_set>
24 
25 #include "context/cdhashset.h"
26 #include "context/cdlist.h"
27 #include "context/context.h"
28 #include "theory/bv/bv_subtheory.h"
29 #include "theory/bv/theory_bv_utils.h"
30 #include "theory/theory.h"
31 #include "util/hash.h"
32 #include "util/statistics_registry.h"
33 
34 // Forward declarations, needed because the BV theory and the BV Proof classes
35 // are cyclically dependent
36 namespace CVC4 {
37 namespace proof {
38 class BitVectorProof;
39 }
40 }  // namespace CVC4
41 
42 namespace CVC4 {
43 namespace theory {
44 namespace bv {
45 
46 class CoreSolver;
47 class InequalitySolver;
48 class AlgebraicSolver;
49 class BitblastSolver;
50 
51 class EagerBitblastSolver;
52 
53 class AbstractionModule;
54 
55 class TheoryBV : public Theory {
56 
57   /** The context we are using */
58   context::Context* d_context;
59 
60   /** Context dependent set of atoms we already propagated */
61   context::CDHashSet<Node, NodeHashFunction> d_alreadyPropagatedSet;
62   context::CDHashSet<Node, NodeHashFunction> d_sharedTermsSet;
63 
64   std::vector<std::unique_ptr<SubtheorySolver>> d_subtheories;
65   std::unordered_map<SubTheory, SubtheorySolver*, std::hash<int> > d_subtheoryMap;
66 
67 public:
68 
69   TheoryBV(context::Context* c, context::UserContext* u, OutputChannel& out,
70            Valuation valuation, const LogicInfo& logicInfo,
71            std::string name = "");
72 
73   ~TheoryBV();
74 
75   void setMasterEqualityEngine(eq::EqualityEngine* eq) override;
76 
77   void finishInit() override;
78 
79   Node expandDefinition(LogicRequest& logicRequest, Node node) override;
80 
81   void preRegisterTerm(TNode n) override;
82 
83   void check(Effort e) override;
84 
85   bool needsCheckLastEffort() override;
86 
87   void propagate(Effort e) override;
88 
89   Node explain(TNode n) override;
90 
91   bool collectModelInfo(TheoryModel* m) override;
92 
identify()93   std::string identify() const override { return std::string("TheoryBV"); }
94 
95   /** equality engine */
96   eq::EqualityEngine* getEqualityEngine() override;
97   bool getCurrentSubstitution(int effort,
98                               std::vector<Node>& vars,
99                               std::vector<Node>& subs,
100                               std::map<Node, std::vector<Node> >& exp) override;
101   int getReduction(int effort, Node n, Node& nr) override;
102 
103   PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions) override;
104 
105   void enableCoreTheorySlicer();
106 
107   Node ppRewrite(TNode t) override;
108 
109   void ppStaticLearn(TNode in, NodeBuilder<>& learned) override;
110 
111   void presolve() override;
112 
113   bool applyAbstraction(const std::vector<Node>& assertions, std::vector<Node>& new_assertions);
114 
115   void setProofLog(proof::BitVectorProof* bvp);
116 
117  private:
118 
119   class Statistics {
120   public:
121     AverageStat d_avgConflictSize;
122     IntStat     d_solveSubstitutions;
123     TimerStat   d_solveTimer;
124     IntStat     d_numCallsToCheckFullEffort;
125     IntStat     d_numCallsToCheckStandardEffort;
126     TimerStat   d_weightComputationTimer;
127     IntStat     d_numMultSlice;
128     Statistics();
129     ~Statistics();
130   };
131 
132   Statistics d_statistics;
133 
134   void spendResource(unsigned amount);
135 
136   /**
137    * Return the uninterpreted function symbol corresponding to division-by-zero
138    * for this particular bit-width
139    * @param k should be UREM or UDIV
140    * @param width
141    *
142    * @return
143    */
144   Node getBVDivByZero(Kind k, unsigned width);
145 
146   typedef std::unordered_set<TNode, TNodeHashFunction> TNodeSet;
147   typedef std::unordered_set<Node, NodeHashFunction> NodeSet;
148   NodeSet d_staticLearnCache;
149 
150   /**
151    * Maps from bit-vector width to division-by-zero uninterpreted
152    * function symbols.
153    */
154   std::unordered_map<unsigned, Node> d_BVDivByZero;
155   std::unordered_map<unsigned, Node> d_BVRemByZero;
156 
157   typedef std::unordered_map<Node, Node, NodeHashFunction>  NodeToNode;
158 
159   context::CDO<bool> d_lemmasAdded;
160 
161   // Are we in conflict?
162   context::CDO<bool> d_conflict;
163 
164   // Invalidate the model cache if check was called
165   context::CDO<bool> d_invalidateModelCache;
166 
167   /** The conflict node */
168   Node d_conflictNode;
169 
170   /** Literals to propagate */
171   context::CDList<Node> d_literalsToPropagate;
172 
173   /** Index of the next literal to propagate */
174   context::CDO<unsigned> d_literalsToPropagateIndex;
175 
176   /**
177    * Keeps a map from nodes to the subtheory that propagated it so that we can explain it
178    * properly.
179    */
180   typedef context::CDHashMap<Node, SubTheory, NodeHashFunction> PropagatedMap;
181   PropagatedMap d_propagatedBy;
182 
183   std::unique_ptr<EagerBitblastSolver> d_eagerSolver;
184   std::unique_ptr<AbstractionModule> d_abstractionModule;
185   bool d_isCoreTheory;
186   bool d_calledPreregister;
187 
188   //for extended functions
189   bool d_needsLastCallCheck;
190   context::CDHashSet<Node, NodeHashFunction> d_extf_range_infer;
191   context::CDHashSet<Node, NodeHashFunction> d_extf_collapse_infer;
192   /** do extended function inferences
193    *
194    * This method adds lemmas on the output channel of TheoryBV based on
195    * reasoning about extended functions, such as bv2nat and int2bv. Examples
196    * of lemmas added by this method include:
197    *   0 <= ((_ int2bv w) x) < 2^w
198    *   ((_ int2bv w) (bv2nat x)) = x
199    *   (bv2nat ((_ int2bv w) x)) == x + k*2^w
200    * The purpose of these lemmas is to recognize easy conflicts before fully
201    * reducing extended functions based on their full semantics.
202    */
203   bool doExtfInferences( std::vector< Node >& terms );
204   /** do extended function reductions
205    *
206    * This method adds lemmas on the output channel of TheoryBV based on
207    * reducing all extended function applications that are preregistered to
208    * this theory and have not already been reduced by context-dependent
209    * simplification (see theory/ext_theory.h). Examples of lemmas added by
210    * this method include:
211    *   (bv2nat x) = (ite ((_ extract w w-1) x) 2^{w-1} 0) + ... +
212    *                (ite ((_ extract 1 0) x) 1 0)
213    */
214   bool doExtfReductions( std::vector< Node >& terms );
215 
wasPropagatedBySubtheory(TNode literal)216   bool wasPropagatedBySubtheory(TNode literal) const {
217     return d_propagatedBy.find(literal) != d_propagatedBy.end();
218   }
219 
getPropagatingSubtheory(TNode literal)220   SubTheory getPropagatingSubtheory(TNode literal) const {
221     Assert(wasPropagatedBySubtheory(literal));
222     PropagatedMap::const_iterator find = d_propagatedBy.find(literal);
223     return (*find).second;
224   }
225 
226   /** Should be called to propagate the literal.  */
227   bool storePropagation(TNode literal, SubTheory subtheory);
228 
229   /**
230    * Explains why this literal (propagated by subtheory) is true by adding assumptions.
231    */
232   void explain(TNode literal, std::vector<TNode>& assumptions);
233 
234   void addSharedTerm(TNode t) override;
235 
isSharedTerm(TNode t)236   bool isSharedTerm(TNode t) { return d_sharedTermsSet.contains(t); }
237 
238   EqualityStatus getEqualityStatus(TNode a, TNode b) override;
239 
240   Node getModelValue(TNode var) override;
241 
indent()242   inline std::string indent()
243   {
244     std::string indentStr(getSatContext()->getLevel(), ' ');
245     return indentStr;
246   }
247 
248   void setConflict(Node conflict = Node::null());
249 
inConflict()250   bool inConflict() {
251     return d_conflict;
252   }
253 
254   void sendConflict();
255 
lemma(TNode node)256   void lemma(TNode node) { d_out->lemma(node, RULE_CONFLICT); d_lemmasAdded = true; }
257 
258   void checkForLemma(TNode node);
259 
260   friend class LazyBitblaster;
261   friend class TLazyBitblaster;
262   friend class EagerBitblaster;
263   friend class BitblastSolver;
264   friend class EqualitySolver;
265   friend class CoreSolver;
266   friend class InequalitySolver;
267   friend class AlgebraicSolver;
268   friend class EagerBitblastSolver;
269 };/* class TheoryBV */
270 
271 }/* CVC4::theory::bv namespace */
272 }/* CVC4::theory namespace */
273 
274 }/* CVC4 namespace */
275 
276 #endif /* __CVC4__THEORY__BV__THEORY_BV_H */
277