1 /*********************                                                        */
2 /*! \file bv_subtheory_algebraic.h
3  ** \verbatim
4  ** Top contributors (to current version):
5  **   Liana Hadarean, Mathias Preiner, Tim King
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 Algebraic solver.
13  **
14  ** Algebraic solver.
15  **/
16 
17 #include "cvc4_private.h"
18 
19 #pragma once
20 
21 #include <unordered_map>
22 #include <unordered_set>
23 
24 #include "theory/bv/bv_subtheory.h"
25 #include "theory/bv/slicer.h"
26 #include "theory/substitutions.h"
27 
28 namespace CVC4 {
29 namespace theory {
30 namespace bv {
31 
32 class AlgebraicSolver;
33 
34 
35 Node mergeExplanations(TNode expl1, TNode expl2);
36 Node mergeExplanations(const std::vector<Node>& expls);
37 
38 
39 /**
40  * Non-context dependent substitution with explanations.
41  *
42  */
43 class SubstitutionEx {
44   struct SubstitutionElement {
45     Node to;
46     Node reason;
SubstitutionElementSubstitutionElement47     SubstitutionElement()
48       : to()
49       , reason()
50     {}
51 
SubstitutionElementSubstitutionElement52     SubstitutionElement(TNode t, TNode r)
53       : to(t)
54       , reason(r)
55     {}
56   };
57 
58   struct SubstitutionStackElement {
59     TNode node;
60     bool childrenAdded;
61     SubstitutionStackElement(TNode n, bool ca = false)
nodeSubstitutionStackElement62       : node(n)
63       , childrenAdded(ca)
64     {}
65   };
66 
67   typedef std::unordered_map<Node, SubstitutionElement, NodeHashFunction> Substitutions;
68   typedef std::unordered_map<Node, SubstitutionElement, NodeHashFunction> SubstitutionsCache;
69 
70   Substitutions d_substitutions;
71   SubstitutionsCache d_cache;
72   bool d_cacheInvalid;
73   theory::SubstitutionMap* d_modelMap;
74 
75 
76   Node getReason(TNode node) const;
77   bool hasCache(TNode node) const;
78   Node getCache(TNode node) const;
79   void storeCache(TNode from, TNode to, Node rason);
80   Node internalApply(TNode node);
81 
82 public:
83   SubstitutionEx(theory::SubstitutionMap* modelMap);
84   /**
85    * Returnst true if the substitution map did not contain from.
86    *
87    * @param from
88    * @param to
89    * @param reason
90    *
91    * @return
92    */
93   bool addSubstitution(TNode from, TNode to, TNode reason);
94   Node apply(TNode node);
95   Node explain(TNode node) const;
96 };
97 
98 /**
99  * In-processing worklist element, id keeps track of
100  * original assertion.
101  *
102  */
103 struct WorklistElement {
104   Node node;
105   unsigned id;
WorklistElementWorklistElement106   WorklistElement(Node n, unsigned i) : node(n), id(i) {}
WorklistElementWorklistElement107   WorklistElement() : node(), id(-1) {}
108 };
109 
110 
111 typedef std::unordered_map<Node, Node, NodeHashFunction> NodeNodeMap;
112 typedef std::unordered_map<Node, unsigned, NodeHashFunction> NodeIdMap;
113 typedef std::unordered_set<TNode, TNodeHashFunction> TNodeSet;
114 
115 
116 class ExtractSkolemizer {
117   struct Extract {
118     unsigned high;
119     unsigned low;
ExtractExtract120     Extract(unsigned h, unsigned l) : high(h), low(l) {}
121   };
122 
123   struct ExtractList {
124     Base base;
125     std::vector<Extract> extracts;
ExtractListExtractList126     ExtractList(unsigned bitwidth) : base(bitwidth), extracts() {}
ExtractListExtractList127     ExtractList() : base(1), extracts() {}
128     void addExtract(Extract& e);
129   };
130   typedef   std::unordered_map<Node, ExtractList, NodeHashFunction> VarExtractMap;
131   context::Context d_emptyContext;
132   VarExtractMap d_varToExtract;
133   theory::SubstitutionMap* d_modelMap;
134   theory::SubstitutionMap d_skolemSubst;
135   theory::SubstitutionMap d_skolemSubstRev;
136 
137   void storeSkolem(TNode node, TNode skolem);
138   void storeExtract(TNode var, unsigned high, unsigned low);
139   void collectExtracts(TNode node, TNodeSet& seen);
140   Node skolemize(TNode);
141   Node unSkolemize(TNode);
142 
143   Node mkSkolem(Node node);
144 public:
145   ExtractSkolemizer(theory::SubstitutionMap* modelMap);
146   void skolemize(std::vector<WorklistElement>&);
147   void unSkolemize(std::vector<WorklistElement>&);
148   ~ExtractSkolemizer();
149 };
150 
151 class BVQuickCheck;
152 class QuickXPlain;
153 
154 /**
155  * AlgebraicSolver
156  */
157 class AlgebraicSolver : public SubtheorySolver {
158 
159   struct Statistics {
160     IntStat d_numCallstoCheck;
161     IntStat d_numSimplifiesToTrue;
162     IntStat d_numSimplifiesToFalse;
163     IntStat d_numUnsat;
164     IntStat d_numSat;
165     IntStat d_numUnknown;
166     TimerStat d_solveTime;
167     BackedStat<double> d_useHeuristic;
168     Statistics();
169     ~Statistics();
170   };
171 
172   std::unique_ptr<SubstitutionMap> d_modelMap;
173   std::unique_ptr<BVQuickCheck> d_quickSolver;
174   context::CDO<bool> d_isComplete;
175   context::CDO<bool> d_isDifficult; /**< flag to indicate whether the current assertions contain expensive BV operators */
176 
177   unsigned long d_budget;
178   std::vector<Node> d_explanations; /**< explanations for assertions indexed by assertion id */
179   TNodeSet d_inputAssertions;   /**< assertions in current context (for debugging purposes only) */
180   NodeIdMap d_ids;              /**< map from assertions to ids */
181   uint64_t d_numSolved;
182   uint64_t d_numCalls;
183 
184   /** separate quickXplain module as it can reuse the current SAT solver */
185   std::unique_ptr<QuickXPlain> d_quickXplain;
186 
187   Statistics d_statistics;
188   bool useHeuristic();
189   void setConflict(TNode conflict);
190   bool isSubstitutableIn(TNode node, TNode in);
191   bool checkExplanation(TNode expl);
192   void storeExplanation(TNode expl);
193   void storeExplanation(unsigned id, TNode expl);
194   /**
195    * Apply substitutions and rewriting to the worklist assertions to a fixpoint.
196    * Subsitutions learned store in subst.
197    *
198    * @param worklist
199    * @param subst
200    */
201   void processAssertions(std::vector<WorklistElement>& worklist, SubstitutionEx& subst);
202   /**
203    * Attempt to solve the equation in fact, and if successful
204    * add a substitution to subst.
205    *
206    * @param fact equation we are trying to solve
207    * @param reason the reason in terms of original assertions
208    * @param subst substitution map
209    *
210    * @return true if added a substitution to subst
211    */
212   bool solve(TNode fact, TNode reason, SubstitutionEx& subst);
213   /**
214    * Run a SAT solver on the given facts with the given budget.
215    * Sets the isComplete flag and conflict accordingly.
216    *
217    * @param facts
218    *
219    * @return true if no conflict was detected.
220    */
221   bool quickCheck(std::vector<Node>& facts);
222 
223 public:
224   AlgebraicSolver(context::Context* c, TheoryBV* bv);
225   ~AlgebraicSolver();
226 
preRegister(TNode node)227   void preRegister(TNode node) override {}
228   bool check(Theory::Effort e) override;
explain(TNode literal,std::vector<TNode> & assumptions)229   void explain(TNode literal, std::vector<TNode>& assumptions) override
230   {
231     Unreachable("AlgebraicSolver does not propagate.\n");
232   }
233   EqualityStatus getEqualityStatus(TNode a, TNode b) override;
234   bool collectModelInfo(TheoryModel* m, bool fullModel) override;
235   Node getModelValue(TNode node) override;
236   bool isComplete() override;
237   void assertFact(TNode fact) override;
238 };
239 
240 }  // namespace bv
241 }  // namespace theory
242 }  // namespace CVC4
243