src/theory/bv/bv_subtheory_algebraic.h

   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-2020 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 Node mergeExplanations(TNode expl1, TNode expl2);
  35 Node mergeExplanations(const std::vector<Node>& expls);
  36
  37 /**
  38  * Non-context dependent substitution with explanations.
  39  *
  40  */
  41 class SubstitutionEx
  42 {
  43   struct SubstitutionElement
  44   {
  45     Node to;
  46     Node reason;
  47     SubstitutionElement() : to(), reason() {}
  48
  49     SubstitutionElement(TNode t, TNode r) : to(t), reason(r) {}
  50   };
  51
  52   struct SubstitutionStackElement
  53   {
  54     TNode node;
  55     bool childrenAdded;
  56     SubstitutionStackElement(TNode n, bool ca = false)
  57         : node(n), childrenAdded(ca)
  58     {
  59     }
  60   };
  61
  62   typedef std::unordered_map<Node, SubstitutionElement, NodeHashFunction>
  63       Substitutions;
  64   typedef std::unordered_map<Node, SubstitutionElement, NodeHashFunction>
  65       SubstitutionsCache;
  66
  67   Substitutions d_substitutions;
  68   SubstitutionsCache d_cache;
  69   bool d_cacheInvalid;
  70   theory::SubstitutionMap* d_modelMap;
  71
  72   Node getReason(TNode node) const;
  73   bool hasCache(TNode node) const;
  74   Node getCache(TNode node) const;
  75   void storeCache(TNode from, TNode to, Node rason);
  76   Node internalApply(TNode node);
  77
  78  public:
  79   SubstitutionEx(theory::SubstitutionMap* modelMap);
  80   /**
  81    * Returnst true if the substitution map did not contain from.
  82    *
  83    * @param from
  84    * @param to
  85    * @param reason
  86    *
  87    * @return
  88    */
  89   bool addSubstitution(TNode from, TNode to, TNode reason);
  90   Node apply(TNode node);
  91   Node explain(TNode node) const;
  92 };
  93
  94 /**
  95  * In-processing worklist element, id keeps track of
  96  * original assertion.
  97  *
  98  */
  99 struct WorklistElement
 100 {
 101   Node node;
 102   unsigned id;
 103   WorklistElement(Node n, unsigned i) : node(n), id(i) {}
 104   WorklistElement() : node(), id(-1) {}
 105 };
 106
 107 typedef std::unordered_map<Node, Node, NodeHashFunction> NodeNodeMap;
 108 typedef std::unordered_map<Node, unsigned, NodeHashFunction> NodeIdMap;
 109 typedef std::unordered_set<TNode, TNodeHashFunction> TNodeSet;
 110
 111 class ExtractSkolemizer
 112 {
 113   struct Extract
 114   {
 115     unsigned high;
 116     unsigned low;
 117     Extract(unsigned h, unsigned l) : high(h), low(l) {}
 118   };
 119
 120   struct ExtractList
 121   {
 122     Base base;
 123     std::vector<Extract> extracts;
 124     ExtractList(unsigned bitwidth) : base(bitwidth), extracts() {}
 125     ExtractList() : base(1), extracts() {}
 126     void addExtract(Extract& e);
 127   };
 128   typedef std::unordered_map<Node, ExtractList, NodeHashFunction> VarExtractMap;
 129   context::Context d_emptyContext;
 130   VarExtractMap d_varToExtract;
 131   theory::SubstitutionMap* d_modelMap;
 132   theory::SubstitutionMap d_skolemSubst;
 133   theory::SubstitutionMap d_skolemSubstRev;
 134
 135   void storeSkolem(TNode node, TNode skolem);
 136   void storeExtract(TNode var, unsigned high, unsigned low);
 137   void collectExtracts(TNode node, TNodeSet& seen);
 138   Node skolemize(TNode);
 139   Node unSkolemize(TNode);
 140
 141   Node mkSkolem(Node node);
 142
 143  public:
 144   ExtractSkolemizer(theory::SubstitutionMap* modelMap);
 145   void skolemize(std::vector<WorklistElement>&);
 146   void unSkolemize(std::vector<WorklistElement>&);
 147   ~ExtractSkolemizer();
 148 };
 149
 150 class BVQuickCheck;
 151 class QuickXPlain;
 152
 153 /**
 154  * AlgebraicSolver
 155  */
 156 class AlgebraicSolver : public SubtheorySolver
 157 {
 158   struct Statistics
 159   {
 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>
 176       d_isDifficult; /**< flag to indicate whether the current assertions
 177                         contain expensive BV operators */
 178
 179   unsigned long d_budget;
 180   std::vector<Node> d_explanations; /**< explanations for assertions indexed by
 181                                        assertion id */
 182   TNodeSet d_inputAssertions; /**< assertions in current context (for debugging
 183                                  purposes only) */
 184   NodeIdMap d_ids;            /**< map from assertions to ids */
 185   uint64_t d_numSolved;
 186   uint64_t d_numCalls;
 187
 188   /** separate quickXplain module as it can reuse the current SAT solver */
 189   std::unique_ptr<QuickXPlain> d_quickXplain;
 190
 191   Statistics d_statistics;
 192   bool useHeuristic();
 193   void setConflict(TNode conflict);
 194   bool isSubstitutableIn(TNode node, TNode in);
 195   bool checkExplanation(TNode expl);
 196   void storeExplanation(TNode expl);
 197   void storeExplanation(unsigned id, TNode expl);
 198   /**
 199    * Apply substitutions and rewriting to the worklist assertions to a fixpoint.
 200    * Subsitutions learned store in subst.
 201    *
 202    * @param worklist
 203    * @param subst
 204    */
 205   void processAssertions(std::vector<WorklistElement>& worklist,
 206                          SubstitutionEx& subst);
 207   /**
 208    * Attempt to solve the equation in fact, and if successful
 209    * add a substitution to subst.
 210    *
 211    * @param fact equation we are trying to solve
 212    * @param reason the reason in terms of original assertions
 213    * @param subst substitution map
 214    *
 215    * @return true if added a substitution to subst
 216    */
 217   bool solve(TNode fact, TNode reason, SubstitutionEx& subst);
 218   /**
 219    * Run a SAT solver on the given facts with the given budget.
 220    * Sets the isComplete flag and conflict accordingly.
 221    *
 222    * @param facts
 223    *
 224    * @return true if no conflict was detected.
 225    */
 226   bool quickCheck(std::vector<Node>& facts);
 227
 228  public:
 229   AlgebraicSolver(context::Context* c, BVSolverLazy* bv);
 230   ~AlgebraicSolver();
 231
 232   void preRegister(TNode node) override {}
 233   bool check(Theory::Effort e) override;
 234   void explain(TNode literal, std::vector<TNode>& assumptions) override
 235   {
 236     Unreachable() << "AlgebraicSolver does not propagate.\n";
 237   }
 238   EqualityStatus getEqualityStatus(TNode a, TNode b) override;
 239   bool collectModelValues(TheoryModel* m,
 240                           const std::set<Node>& termSet) override;
 241   Node getModelValue(TNode node) override;
 242   bool isComplete() override;
 243   void assertFact(TNode fact) override;
 244 };
 245
 246 }  // namespace bv
 247 }  // namespace theory
 248 }  // namespace CVC4