src/theory/arith/congruence_manager.h

   1 /*********************                                                        */
   2 /*! \file congruence_manager.h
   3  ** \verbatim
   4  ** Original author: Tim King
   5  ** Major contributors: Dejan Jovanovic
   6  ** Minor contributors (to current version): Morgan Deters
   7  ** This file is part of the CVC4 project.
   8  ** Copyright (c) 2009-2013  New York University and The University of Iowa
   9  ** See the file COPYING in the top-level source directory for licensing
  10  ** information.\endverbatim
  11  **
  12  ** \brief [[ Add one-line brief description here ]]
  13  **
  14  ** [[ Add lengthier description here ]]
  15  ** \todo document this file
  16  **/
  17
  18 #include "cvc4_private.h"
  19
  20 #pragma once
  21
  22 #include "theory/arith/arithvar.h"
  23 #include "theory/arith/constraint_forward.h"
  24 #include "theory/arith/partial_model.h"
  25
  26 #include "theory/uf/equality_engine.h"
  27
  28 #include "context/cdo.h"
  29 #include "context/cdlist.h"
  30 #include "context/context.h"
  31 #include "context/cdtrail_queue.h"
  32 #include "context/cdmaybe.h"
  33
  34 #include "util/statistics_registry.h"
  35 #include "util/dense_map.h"
  36
  37 namespace CVC4 {
  38 namespace theory {
  39 namespace arith {
  40
  41 class ArithCongruenceManager {
  42 private:
  43   context::CDRaised d_inConflict;
  44   RaiseConflict d_raiseConflict;
  45
  46   /**
  47    * The set of ArithVars equivalent to a pair of terms.
  48    * If this is 0 or cannot be 0, this can be signalled.
  49    * The pair of terms for the congruence is stored in watched equalities.
  50    */
  51   DenseSet d_watchedVariables;
  52   /** d_watchedVariables |-> (= x y) */
  53   ArithVarToNodeMap d_watchedEqualities;
  54
  55
  56   class ArithCongruenceNotify : public eq::EqualityEngineNotify {
  57   private:
  58     ArithCongruenceManager& d_acm;
  59   public:
  60     ArithCongruenceNotify(ArithCongruenceManager& acm): d_acm(acm) {}
  61
  62     bool eqNotifyTriggerEquality(TNode equality, bool value) {
  63       Debug("arith::congruences") << "ArithCongruenceNotify::eqNotifyTriggerEquality(" << equality << ", " << (value ? "true" : "false") << ")" << std::endl;
  64       if (value) {
  65         return d_acm.propagate(equality);
  66       } else {
  67         return d_acm.propagate(equality.notNode());
  68       }
  69     }
  70
  71     bool eqNotifyTriggerPredicate(TNode predicate, bool value) {
  72       Unreachable();
  73     }
  74
  75     bool eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value) {
  76       Debug("arith::congruences") << "ArithCongruenceNotify::eqNotifyTriggerTermEquality(" << t1 << ", " << t2 << ", " << (value ? "true" : "false") << ")" << std::endl;
  77       if (value) {
  78         return d_acm.propagate(t1.eqNode(t2));
  79       } else {
  80         return d_acm.propagate(t1.eqNode(t2).notNode());
  81       }
  82     }
  83
  84     void eqNotifyConstantTermMerge(TNode t1, TNode t2) {
  85       Debug("arith::congruences") << "ArithCongruenceNotify::eqNotifyConstantTermMerge(" << t1 << ", " << t2 << std::endl;
  86       if (t1.getKind() == kind::CONST_BOOLEAN) {
  87         d_acm.propagate(t1.iffNode(t2));
  88       } else {
  89         d_acm.propagate(t1.eqNode(t2));
  90       }
  91     }
  92
  93     void eqNotifyNewClass(TNode t) { }
  94     void eqNotifyPreMerge(TNode t1, TNode t2) { }
  95     void eqNotifyPostMerge(TNode t1, TNode t2) { }
  96     void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) { }
  97   };
  98   ArithCongruenceNotify d_notify;
  99
 100   context::CDList<Node> d_keepAlive;
 101
 102   /** Store the propagations. */
 103   context::CDTrailQueue<Node> d_propagatations;
 104
 105   /* This maps the node a theory engine will request on an explain call to
 106    * to its corresponding PropUnit.
 107    * This is node is potentially both the propagation or
 108    * Rewriter::rewrite(propagation).
 109    */
 110   typedef context::CDHashMap<Node, size_t, NodeHashFunction> ExplainMap;
 111   ExplainMap d_explanationMap;
 112
 113   ConstraintDatabase& d_constraintDatabase;
 114   SetupLiteralCallBack d_setupLiteral;
 115
 116   const ArithVariables& d_avariables;
 117
 118   eq::EqualityEngine d_ee;
 119
 120   void raiseConflict(Node conflict){
 121     Assert(!inConflict());
 122     Debug("arith::conflict") << "difference manager conflict   " << conflict << std::endl;
 123     d_inConflict.raise();
 124     d_raiseConflict(conflict);
 125   }
 126 public:
 127
 128   bool inConflict() const{
 129     return d_inConflict.isRaised();
 130   };
 131
 132   bool hasMorePropagations() const {
 133     return !d_propagatations.empty();
 134   }
 135
 136   const Node getNextPropagation() {
 137     Assert(hasMorePropagations());
 138     Node prop = d_propagatations.front();
 139     d_propagatations.dequeue();
 140     return prop;
 141   }
 142
 143   bool canExplain(TNode n) const {
 144     return d_explanationMap.find(n) != d_explanationMap.end();
 145   }
 146
 147   void setMasterEqualityEngine(eq::EqualityEngine* eq);
 148
 149 private:
 150   Node externalToInternal(TNode n) const{
 151     Assert(canExplain(n));
 152     ExplainMap::const_iterator iter = d_explanationMap.find(n);
 153     size_t pos = (*iter).second;
 154     return d_propagatations[pos];
 155   }
 156
 157   void pushBack(TNode n){
 158     d_explanationMap.insert(n, d_propagatations.size());
 159     d_propagatations.enqueue(n);
 160
 161     ++(d_statistics.d_propagations);
 162   }
 163
 164   void pushBack(TNode n, TNode r){
 165     d_explanationMap.insert(r, d_propagatations.size());
 166     d_explanationMap.insert(n, d_propagatations.size());
 167     d_propagatations.enqueue(n);
 168
 169     ++(d_statistics.d_propagations);
 170   }
 171
 172   void pushBack(TNode n, TNode r, TNode w){
 173     d_explanationMap.insert(w, d_propagatations.size());
 174     d_explanationMap.insert(r, d_propagatations.size());
 175     d_explanationMap.insert(n, d_propagatations.size());
 176     d_propagatations.enqueue(n);
 177
 178     ++(d_statistics.d_propagations);
 179   }
 180
 181   bool propagate(TNode x);
 182   void explain(TNode literal, std::vector<TNode>& assumptions);
 183
 184
 185   /** This sends a shared term to the uninterpreted equality engine. */
 186   void assertionToEqualityEngine(bool eq, ArithVar s, TNode reason);
 187
 188   /** Dequeues the delay queue and asserts these equalities.*/
 189   void enableSharedTerms();
 190   void dequeueLiterals();
 191
 192   void enqueueIntoNB(const std::set<TNode> all, NodeBuilder<>& nb);
 193
 194   Node explainInternal(TNode internal);
 195
 196 public:
 197
 198   ArithCongruenceManager(context::Context* satContext, ConstraintDatabase&, SetupLiteralCallBack, const ArithVariables&, RaiseConflict raiseConflict);
 199
 200   Node explain(TNode literal);
 201   void explain(TNode lit, NodeBuilder<>& out);
 202
 203   void addWatchedPair(ArithVar s, TNode x, TNode y);
 204
 205   inline bool isWatchedVariable(ArithVar s) const {
 206     return d_watchedVariables.isMember(s);
 207   }
 208
 209   /** Assert an equality. */
 210   void watchedVariableIsZero(Constraint eq);
 211
 212   /** Assert a conjunction from lb and ub. */
 213   void watchedVariableIsZero(Constraint lb, Constraint ub);
 214
 215   /** Assert that the value cannot be zero. */
 216   void watchedVariableCannotBeZero(Constraint c);
 217
 218   /** Assert that the value cannot be zero. */
 219   void watchedVariableCannotBeZero(Constraint c, Constraint d);
 220
 221
 222   /** Assert that the value is congruent to a constant. */
 223   void equalsConstant(Constraint eq);
 224   void equalsConstant(Constraint lb, Constraint ub);
 225
 226
 227   void addSharedTerm(Node x);
 228
 229 private:
 230   class Statistics {
 231   public:
 232     IntStat d_watchedVariables;
 233     IntStat d_watchedVariableIsZero;
 234     IntStat d_watchedVariableIsNotZero;
 235
 236     IntStat d_equalsConstantCalls;
 237
 238     IntStat d_propagations;
 239     IntStat d_propagateConstraints;
 240     IntStat d_conflicts;
 241
 242     Statistics();
 243     ~Statistics();
 244   } d_statistics;
 245
 246 };/* class ArithCongruenceManager */
 247
 248 }/* CVC4::theory::arith namespace */
 249 }/* CVC4::theory namespace */
 250 }/* CVC4 namespace */