src/theory/arith/theory_arith.h

   1 /*********************                                                        */
   2 /*! \file theory_arith.h
   3  ** \verbatim
   4  ** Original author: mdeters
   5  ** Major contributors: taking
   6  ** Minor contributors (to current version): barrett
   7  ** This file is part of the CVC4 prototype.
   8  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
   9  ** Courant Institute of Mathematical Sciences
  10  ** New York University
  11  ** See the file COPYING in the top-level source directory for licensing
  12  ** information.\endverbatim
  13  **
  14  ** \brief Arithmetic theory.
  15  **
  16  ** Arithmetic theory.
  17  **/
  18
  19 #include "cvc4_private.h"
  20
  21 #ifndef __CVC4__THEORY__ARITH__THEORY_ARITH_H
  22 #define __CVC4__THEORY__ARITH__THEORY_ARITH_H
  23
  24 #include "theory/theory.h"
  25 #include "context/context.h"
  26 #include "context/cdlist.h"
  27 #include "context/cdset.h"
  28 #include "expr/node.h"
  29
  30 #include "theory/arith/arith_utilities.h"
  31 #include "theory/arith/arithvar_set.h"
  32 #include "theory/arith/delta_rational.h"
  33 #include "theory/arith/tableau.h"
  34 #include "theory/arith/arith_rewriter.h"
  35 #include "theory/arith/partial_model.h"
  36 #include "theory/arith/unate_propagator.h"
  37 #include "theory/arith/simplex.h"
  38 #include "theory/arith/arith_static_learner.h"
  39
  40 #include "util/stats.h"
  41
  42 #include <vector>
  43 #include <map>
  44 #include <queue>
  45
  46 namespace CVC4 {
  47 namespace theory {
  48 namespace arith {
  49
  50 /**
  51  * Implementation of QF_LRA.
  52  * Based upon:
  53  * http://research.microsoft.com/en-us/um/people/leonardo/cav06.pdf
  54  */
  55 class TheoryArith : public Theory {
  56 private:
  57
  58   /** Static learner. */
  59   ArithStaticLearner learner;
  60
  61   /**
  62    * List of the variables in the system.
  63    * This is needed to keep a positive ref count on slack variables.
  64    */
  65   std::vector<Node> d_variables;
  66
  67   /**
  68    * If ArithVar v maps to the node n in d_removednode,
  69    * then n = (= asNode(v) rhs) where rhs is a term that
  70    * can be used to determine the value of n using getValue().
  71    */
  72   std::map<ArithVar, Node> d_removedRows;
  73
  74   /**
  75    * Manages information about the assignment and upper and lower bounds on
  76    * variables.
  77    */
  78   ArithPartialModel d_partialModel;
  79
  80   /**
  81    * Set of ArithVars that were introduced via preregisteration.
  82    */
  83   ArithVarSet d_userVariables;
  84
  85   /**
  86    * Bidirectional map between Nodes and ArithVars.
  87    */
  88   NodeToArithVarMap d_nodeToArithVarMap;
  89   ArithVarToNodeMap d_arithVarToNodeMap;
  90
  91   inline bool hasArithVar(TNode x) const {
  92     return d_nodeToArithVarMap.find(x) != d_nodeToArithVarMap.end();
  93   }
  94
  95   inline ArithVar asArithVar(TNode x) const{
  96     Assert(hasArithVar(x));
  97     Assert((d_nodeToArithVarMap.find(x))->second <= ARITHVAR_SENTINEL);
  98     return (d_nodeToArithVarMap.find(x))->second;
  99   }
 100   inline Node asNode(ArithVar a) const{
 101     Assert(d_arithVarToNodeMap.find(a) != d_arithVarToNodeMap.end());
 102     return (d_arithVarToNodeMap.find(a))->second;
 103   }
 104
 105   inline void setArithVar(TNode x, ArithVar a){
 106     Assert(!hasArithVar(x));
 107     Assert(d_arithVarToNodeMap.find(a) == d_arithVarToNodeMap.end());
 108     d_arithVarToNodeMap[a] = x;
 109     d_nodeToArithVarMap[x] = a;
 110   }
 111
 112   /**
 113    * List of all of the inequalities asserted in the current context.
 114    */
 115   context::CDSet<Node, NodeHashFunction> d_diseq;
 116
 117   /**
 118    * The tableau for all of the constraints seen thus far in the system.
 119    */
 120   Tableau d_tableau;
 121
 122
 123   /** Counts the number of notifyRestart() calls to the theory. */
 124   uint32_t d_restartsCounter;
 125
 126   /**
 127    * Every number of restarts equal to s_TABLEAU_RESET_PERIOD,
 128    * the density of the tableau, d, is computed.
 129    * If d >= s_TABLEAU_RESET_DENSITY * d_initialDensity, the tableau
 130    * is set to d_initialTableau.
 131    */
 132   bool d_presolveHasBeenCalled;
 133   double d_tableauResetDensity;
 134   uint32_t d_tableauResetPeriod;
 135   static const uint32_t s_TABLEAU_RESET_INCREMENT = 5;
 136
 137   /**
 138    * A copy of the tableau immediately after removing variables
 139    * without bounds in presolve().
 140    */
 141   Tableau d_smallTableauCopy;
 142
 143   ArithUnatePropagator d_propagator;
 144   SimplexDecisionProcedure d_simplex;
 145
 146 public:
 147   TheoryArith(context::Context* c, OutputChannel& out, Valuation valuation);
 148   ~TheoryArith();
 149
 150   /**
 151    * Does non-context dependent setup for a node connected to a theory.
 152    */
 153   void preRegisterTerm(TNode n);
 154
 155   /** CD setup for a node. Currently does nothing. */
 156   void registerTerm(TNode n);
 157
 158   void check(Effort e);
 159   void propagate(Effort e);
 160   void explain(TNode n);
 161
 162   void notifyEq(TNode lhs, TNode rhs);
 163
 164   Node getValue(TNode n);
 165
 166   void shutdown(){ }
 167
 168   void presolve();
 169   void notifyRestart();
 170   void staticLearning(TNode in, NodeBuilder<>& learned);
 171
 172   std::string identify() const { return std::string("TheoryArith"); }
 173
 174 private:
 175   /** The constant zero. */
 176   DeltaRational d_DELTA_ZERO;
 177
 178   /**
 179    * Using the simpleKind return the ArithVar associated with the
 180    * left hand side of assertion.
 181    */
 182   ArithVar determineLeftVariable(TNode assertion, Kind simpleKind);
 183
 184   /** Splits the disequalities in d_diseq that are violated using lemmas on demand. */
 185   void splitDisequalities();
 186
 187   /**
 188    * This requests a new unique ArithVar value for x.
 189    * This also does initial (not context dependent) set up for a variable,
 190    * except for setting up the initial.
 191    */
 192   ArithVar requestArithVar(TNode x, bool basic);
 193
 194   /** Initial (not context dependent) sets up for a variable.*/
 195   void setupInitialValue(ArithVar x);
 196
 197   /** Initial (not context dependent) sets up for a new slack variable.*/
 198   void setupSlack(TNode left);
 199
 200
 201   /**
 202    * Handles the case splitting for check() for a new assertion.
 203    * Returns a conflict if one was found.
 204    * Returns Node::null if no conflict was found.
 205    */
 206   Node assertionCases(TNode assertion);
 207
 208   /**
 209    * This is used for reporting conflicts caused by disequalities during assertionCases.
 210    */
 211   Node disequalityConflict(TNode eq, TNode lb, TNode ub);
 212
 213   /**
 214    * Returns the basic variable with the shorted row containg a non-basic variable.
 215    * If no such row exists, return ARITHVAR_SENTINEL.
 216    */
 217   ArithVar findShortestBasicRow(ArithVar variable);
 218
 219   /**
 220    * Debugging only routine!
 221    * Returns true iff every variable is consistent in the partial model.
 222    */
 223   bool entireStateIsConsistent();
 224
 225   /**
 226    * Permanently removes a variable from the problem.
 227    * The caller guarentees the saftey of this removal!
 228    */
 229   void permanentlyRemoveVariable(ArithVar v);
 230
 231
 232   void asVectors(Polynomial& p,
 233                  std::vector<Rational>& coeffs,
 234                  std::vector<ArithVar>& variables) const;
 235
 236   /** Routine for debugging. Print the assertions the theory is aware of. */
 237   void debugPrintAssertions();
 238   /** Debugging only routine. Prints the model. */
 239   void debugPrintModel();
 240
 241   /** These fields are designed to be accessable to TheoryArith methods. */
 242   class Statistics {
 243   public:
 244     IntStat d_statUserVariables, d_statSlackVariables;
 245     IntStat d_statDisequalitySplits;
 246     IntStat d_statDisequalityConflicts;
 247     TimerStat d_staticLearningTimer;
 248
 249     IntStat d_permanentlyRemovedVariables;
 250     TimerStat d_presolveTime;
 251
 252     IntStat d_initialTableauSize;
 253     //ListStat<uint32_t> d_tableauSizeHistory;
 254     IntStat d_currSetToSmaller;
 255     IntStat d_smallerSetToCurr;
 256     TimerStat d_restartTimer;
 257
 258     Statistics();
 259     ~Statistics();
 260   };
 261
 262   Statistics d_statistics;
 263
 264
 265 };/* class TheoryArith */
 266
 267 }/* CVC4::theory::arith namespace */
 268 }/* CVC4::theory namespace */
 269 }/* CVC4 namespace */
 270
 271 #endif /* __CVC4__THEORY__ARITH__THEORY_ARITH_H */