src/theory/arith/partial_model.h

   1 /*********************                                                        */
   2 /*! \file partial_model.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Tim King, Morgan Deters, Mathias Preiner
   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 Datastructures that track variable by variable information.
  13  **
  14  ** This is a datastructure that tracks variable specific information.
  15  ** This is partially context dependent to back track upper/lower bounds
  16  ** and information derived from these.
  17  **/
  18
  19 #include "cvc4_private.h"
  20
  21 #ifndef CVC4__THEORY__ARITH__PARTIAL_MODEL_H
  22 #define CVC4__THEORY__ARITH__PARTIAL_MODEL_H
  23
  24 #include <list>
  25 #include <vector>
  26
  27 #include "context/cdlist.h"
  28 #include "context/context.h"
  29 #include "expr/node.h"
  30 #include "theory/arith/arith_utilities.h"
  31 #include "theory/arith/arithvar.h"
  32 #include "theory/arith/bound_counts.h"
  33 #include "theory/arith/callbacks.h"
  34 #include "theory/arith/constraint_forward.h"
  35 #include "theory/arith/delta_rational.h"
  36
  37 namespace CVC4 {
  38 namespace theory {
  39 namespace arith {
  40
  41 /**
  42  * (For the moment) the type hierarchy goes as:
  43  * Integer <: Real
  44  * The type number of a variable is an integer representing the most specific
  45  * type of the variable. The possible values of type number are:
  46  */
  47 enum class ArithType {
  48   Unset,
  49   Real,
  50   Integer,
  51 };
  52
  53 class ArithVariables {
  54 private:
  55
  56   class VarInfo {
  57     friend class ArithVariables;
  58     ArithVar d_var;
  59
  60     DeltaRational d_assignment;
  61     ConstraintP d_lb;
  62     ConstraintP d_ub;
  63     int d_cmpAssignmentLB;
  64     int d_cmpAssignmentUB;
  65
  66     unsigned d_pushCount;
  67     ArithType d_type;
  68     Node d_node;
  69     bool d_auxiliary;
  70
  71   public:
  72     VarInfo();
  73
  74     bool setAssignment(const DeltaRational& r, BoundsInfo& prev);
  75     bool setLowerBound(ConstraintP c, BoundsInfo& prev);
  76     bool setUpperBound(ConstraintP c, BoundsInfo& prev);
  77
  78     /** Returns true if this VarInfo has been initialized. */
  79     bool initialized() const;
  80
  81     /**
  82      * Initializes the VarInfo with the ArithVar index it is associated with,
  83      * the node that the variable represents, and whether it is an auxillary
  84      * variable.
  85      */
  86     void initialize(ArithVar v, Node n, bool aux);
  87
  88     /** Uninitializes the VarInfo. */
  89     void uninitialize();
  90
  91     bool canBeReclaimed() const;
  92
  93     /** Indicator variables for if the assignment is equal to the upper
  94      * and lower bounds. */
  95     BoundCounts atBoundCounts() const;
  96
  97     /** Combination of indicator variables for whether it has upper and
  98      * lower bounds.  */
  99     BoundCounts hasBoundCounts() const;
 100
 101     /** Stores both atBoundCounts() and hasBoundCounts().  */
 102     BoundsInfo boundsInfo() const;
 103   };
 104
 105   /**Maps from ArithVar -> VarInfo */
 106   typedef DenseMap<VarInfo> VarInfoVec;
 107
 108   /** This maps an ArithVar to its Variable information.*/
 109   VarInfoVec d_vars;
 110
 111   /** Partial Map from Arithvar -> PreviousAssignment */
 112   DenseMap<DeltaRational> d_safeAssignment;
 113
 114   /** if d_vars.isKey(x), then x < d_numberOfVariables */
 115   ArithVar d_numberOfVariables;
 116
 117   /** [0, d_numberOfVariables) \intersect d_vars.keys == d_pool */
 118   // Everything in the pool is fair game.
 119   // There must be NO outstanding assertions
 120   std::vector<ArithVar> d_pool;
 121   std::vector<ArithVar> d_released;
 122   //std::list<ArithVar>::iterator d_releasedIterator;
 123
 124   // Reverse Map from Node to ArithVar
 125   // Inverse of d_vars[x].d_node
 126   NodeToArithVarMap d_nodeToArithVarMap;
 127
 128
 129   /** The queue of constraints where the assignment is at the bound.*/
 130   DenseMap<BoundsInfo> d_boundsQueue;
 131
 132   /**
 133    * If this is true, record the incoming changes to the bound information.
 134    * If this is false, the responsibility of recording the changes is
 135    * LinearEqualities's.
 136    */
 137   bool d_enqueueingBoundCounts;
 138
 139  public:
 140
 141   /** Returns the number of variables. */
 142   ArithVar getNumberOfVariables() const;
 143
 144   /** Returns true if the node has an associated variables. */
 145   bool hasArithVar(TNode x) const;
 146
 147   /** Returns true if the variable has a defining node. */
 148   bool hasNode(ArithVar a) const;
 149
 150   /** Returns the ArithVar associated with a node. */
 151   ArithVar asArithVar(TNode x) const;
 152
 153   /** Returns the node associated with an ArithVar. */
 154   Node asNode(ArithVar a) const;
 155
 156   /** Allocates a freshly allocated variables. */
 157   ArithVar allocateVariable();
 158
 159   class var_iterator {
 160   private:
 161     const VarInfoVec* d_vars;
 162     VarInfoVec::const_iterator d_wrapped;
 163   public:
 164     var_iterator();
 165     var_iterator(const VarInfoVec* vars, VarInfoVec::const_iterator ci);
 166     var_iterator& operator++();
 167
 168     bool operator==(const var_iterator& other) const;
 169     bool operator!=(const var_iterator& other) const;
 170     ArithVar operator*() const;
 171
 172   private:
 173     void nextInitialized();
 174   };
 175
 176   var_iterator var_begin() const;
 177   var_iterator var_end() const;
 178
 179
 180   bool canBeReleased(ArithVar v) const;
 181   void releaseArithVar(ArithVar v);
 182   void attemptToReclaimReleased();
 183
 184   /** Is this variable guaranteed to have an integer assignment?
 185    * (Should agree with the type system.) */
 186   bool isInteger(ArithVar x) const;
 187
 188   /** Is the assignment to x integral? */
 189   bool integralAssignment(ArithVar x) const;
 190
 191   /* Is this variable defined as a linear sum of other variables? */
 192   bool isAuxiliary(ArithVar x) const;
 193
 194   /* Is the variable both input and not auxiliary? */
 195   bool isIntegerInput(ArithVar x) const;
 196
 197  private:
 198
 199   typedef std::pair<ArithVar, ConstraintP> AVCPair;
 200   class LowerBoundCleanUp {
 201   private:
 202     ArithVariables* d_pm;
 203   public:
 204     LowerBoundCleanUp(ArithVariables* pm);
 205     void operator()(AVCPair* restore);
 206   };
 207
 208   class UpperBoundCleanUp {
 209   private:
 210     ArithVariables* d_pm;
 211   public:
 212     UpperBoundCleanUp(ArithVariables* pm);
 213     void operator()(AVCPair* restore);
 214   };
 215
 216   typedef context::CDList<AVCPair, LowerBoundCleanUp> LBReverts;
 217   LBReverts d_lbRevertHistory;
 218
 219   typedef context::CDList<AVCPair, UpperBoundCleanUp> UBReverts;
 220   UBReverts d_ubRevertHistory;
 221
 222   void pushUpperBound(VarInfo&);
 223   void popUpperBound(AVCPair*);
 224   void pushLowerBound(VarInfo&);
 225   void popLowerBound(AVCPair*);
 226
 227   // This is true when setDelta() is called, until invalidateDelta is called
 228   bool d_deltaIsSafe;
 229   // Cache of a value of delta to ensure a total order.
 230   Rational d_delta;
 231   // Function to call if the value of delta needs to be recomputed.
 232   DeltaComputeCallback d_deltaComputingFunc;
 233
 234
 235 public:
 236
 237   ArithVariables(context::Context* c, DeltaComputeCallback deltaComputation);
 238
 239   /**
 240    * This sets the lower bound for a variable in the current context.
 241    * This must be stronger the previous constraint.
 242    */
 243   void setLowerBoundConstraint(ConstraintP lb);
 244
 245   /**
 246    * This sets the upper bound for a variable in the current context.
 247    * This must be stronger the previous constraint.
 248    */
 249   void setUpperBoundConstraint(ConstraintP ub);
 250
 251   /** Returns the constraint for the upper bound of a variable. */
 252   inline ConstraintP getUpperBoundConstraint(ArithVar x) const{
 253     return d_vars[x].d_ub;
 254   }
 255   /** Returns the constraint for the lower bound of a variable. */
 256   inline ConstraintP getLowerBoundConstraint(ArithVar x) const{
 257     return d_vars[x].d_lb;
 258   }
 259
 260   /* Initializes a variable to a safe value.*/
 261   void initialize(ArithVar x, Node n, bool aux);
 262
 263   ArithVar allocate(Node n, bool aux = false);
 264
 265   /* Gets the last assignment to a variable that is known to be consistent. */
 266   const DeltaRational& getSafeAssignment(ArithVar x) const;
 267   const DeltaRational& getAssignment(ArithVar x, bool safe) const;
 268
 269   /* Reverts all variable assignments to their safe values. */
 270   void revertAssignmentChanges();
 271
 272   /* Commits all variables assignments as safe.*/
 273   void commitAssignmentChanges();
 274
 275
 276   bool lowerBoundIsZero(ArithVar x);
 277   bool upperBoundIsZero(ArithVar x);
 278
 279   bool boundsAreEqual(ArithVar x) const;
 280
 281   /* Sets an unsafe variable assignment */
 282   void setAssignment(ArithVar x, const DeltaRational& r);
 283   void setAssignment(ArithVar x, const DeltaRational& safe, const DeltaRational& r);
 284
 285
 286   /** Must know that the bound exists before calling this! */
 287   const DeltaRational& getUpperBound(ArithVar x) const;
 288   const DeltaRational& getLowerBound(ArithVar x) const;
 289   const DeltaRational& getAssignment(ArithVar x) const;
 290
 291
 292   bool equalsLowerBound(ArithVar x, const DeltaRational& c);
 293   bool equalsUpperBound(ArithVar x, const DeltaRational& c);
 294
 295   /**
 296    * If lowerbound > - \infty:
 297    *   return getAssignment(x).cmp(getLowerBound(x))
 298    * If lowerbound = - \infty:
 299    *   return 1
 300    */
 301   int cmpToLowerBound(ArithVar x, const DeltaRational& c) const;
 302
 303   inline bool strictlyLessThanLowerBound(ArithVar x, const DeltaRational& c) const{
 304     return cmpToLowerBound(x, c) < 0;
 305   }
 306   inline bool lessThanLowerBound(ArithVar x, const DeltaRational& c) const{
 307     return cmpToLowerBound(x, c) <= 0;
 308   }
 309
 310   inline bool strictlyGreaterThanLowerBound(ArithVar x, const DeltaRational& c) const{
 311     return cmpToLowerBound(x, c) > 0;
 312   }
 313
 314   inline bool greaterThanLowerBound(ArithVar x, const DeltaRational& c) const{
 315     return cmpToLowerBound(x, c) >= 0;
 316   }
 317   /**
 318    * If upperbound < \infty:
 319    *   return getAssignment(x).cmp(getUpperBound(x))
 320    * If upperbound = \infty:
 321    *   return -1
 322    */
 323   int cmpToUpperBound(ArithVar x, const DeltaRational& c) const;
 324
 325   inline bool strictlyLessThanUpperBound(ArithVar x, const DeltaRational& c) const{
 326     return cmpToUpperBound(x, c) < 0;
 327   }
 328
 329   inline bool lessThanUpperBound(ArithVar x, const DeltaRational& c) const{
 330     return cmpToUpperBound(x, c) <= 0;
 331   }
 332
 333   inline bool strictlyGreaterThanUpperBound(ArithVar x, const DeltaRational& c) const{
 334     return cmpToUpperBound(x, c) > 0;
 335   }
 336
 337   inline bool greaterThanUpperBound(ArithVar x, const DeltaRational& c) const{
 338     return cmpToUpperBound(x, c) >= 0;
 339   }
 340
 341   inline int cmpAssignmentLowerBound(ArithVar x) const{
 342     return d_vars[x].d_cmpAssignmentLB;
 343   }
 344   inline int cmpAssignmentUpperBound(ArithVar x) const{
 345     return d_vars[x].d_cmpAssignmentUB;
 346   }
 347
 348   inline BoundCounts atBoundCounts(ArithVar x) const {
 349     return d_vars[x].atBoundCounts();
 350   }
 351   inline BoundCounts hasBoundCounts(ArithVar x) const {
 352     return d_vars[x].hasBoundCounts();
 353   }
 354   inline BoundsInfo boundsInfo(ArithVar x) const{
 355     return d_vars[x].boundsInfo();
 356   }
 357
 358   bool strictlyBelowUpperBound(ArithVar x) const;
 359   bool strictlyAboveLowerBound(ArithVar x) const;
 360   bool assignmentIsConsistent(ArithVar x) const;
 361
 362   void printModel(ArithVar x, std::ostream& out) const;
 363   void printModel(ArithVar x) const;
 364
 365   /** returns true iff x has both a lower and upper bound. */
 366   bool hasEitherBound(ArithVar x) const;
 367   inline bool hasLowerBound(ArithVar x) const{
 368     return d_vars[x].d_lb != NullConstraint;
 369   }
 370   inline bool hasUpperBound(ArithVar x) const{
 371     return d_vars[x].d_ub != NullConstraint;
 372   }
 373
 374   const Rational& getDelta();
 375
 376   void invalidateDelta();
 377
 378   void setDelta(const Rational& d);
 379
 380   void startQueueingBoundCounts();
 381   void stopQueueingBoundCounts();
 382   void addToBoundQueue(ArithVar v, const BoundsInfo& prev);
 383
 384   BoundsInfo selectBoundsInfo(ArithVar v, bool old) const;
 385
 386   bool boundsQueueEmpty() const;
 387   void processBoundsQueue(BoundUpdateCallback& changed);
 388
 389   void printEntireModel(std::ostream& out) const;
 390
 391
 392   /**
 393    * Precondition: assumes boundsAreEqual(x).
 394    * If the either the lower/ upper bound is an equality, eq,
 395    * this returns make_pair(eq, NullConstraint).
 396    * Otherwise, this returns make_pair(lb, ub).
 397    */
 398   std::pair<ConstraintP, ConstraintP> explainEqualBounds(ArithVar x) const;
 399
 400 private:
 401
 402   /**
 403    * This function implements the mostly identical:
 404    * revertAssignmentChanges() and commitAssignmentChanges().
 405    */
 406   void clearSafeAssignments(bool revert);
 407
 408   bool debugEqualSizes();
 409
 410   bool inMaps(ArithVar x) const;
 411
 412 };/* class ArithVariables */
 413
 414
 415 }/* CVC4::theory::arith namespace */
 416 }/* CVC4::theory namespace */
 417 }/* CVC4 namespace */
 418
 419 #endif /* CVC4__THEORY__ARITH__PARTIAL_MODEL_H */