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 #include "theory/arith/arith_prop_manager.h"
  40 #include "theory/arith/arithvar_node_map.h"
  41
  42 #include "util/stats.h"
  43
  44 #include <vector>
  45 #include <map>
  46 #include <queue>
  47
  48 namespace CVC4 {
  49 namespace theory {
  50 namespace arith {
  51
  52 /**
  53  * Implementation of QF_LRA.
  54  * Based upon:
  55  * http://research.microsoft.com/en-us/um/people/leonardo/cav06.pdf
  56  */
  57 class TheoryArith : public Theory {
  58 private:
  59
  60   /** Static learner. */
  61   ArithStaticLearner learner;
  62
  63   /**
  64    * List of the variables in the system.
  65    * This is needed to keep a positive ref count on slack variables.
  66    */
  67   std::vector<Node> d_variables;
  68
  69   ArithVarNodeMap d_arithvarNodeMap;
  70
  71   /**
  72    * If ArithVar v maps to the node n in d_removednode,
  73    * then n = (= asNode(v) rhs) where rhs is a term that
  74    * can be used to determine the value of n using getValue().
  75    */
  76   std::map<ArithVar, Node> d_removedRows;
  77
  78   /**
  79    * Manages information about the assignment and upper and lower bounds on
  80    * variables.
  81    */
  82   ArithPartialModel d_partialModel;
  83
  84   /**
  85    * Set of ArithVars that were introduced via preregisteration.
  86    */
  87   ArithVarSet d_userVariables;
  88
  89
  90
  91   /**
  92    * List of all of the inequalities asserted in the current context.
  93    */
  94   context::CDSet<Node, NodeHashFunction> d_diseq;
  95
  96   /**
  97    * The tableau for all of the constraints seen thus far in the system.
  98    */
  99   Tableau d_tableau;
 100
 101
 102   /** Counts the number of notifyRestart() calls to the theory. */
 103   uint32_t d_restartsCounter;
 104
 105   /**
 106    * Every number of restarts equal to s_TABLEAU_RESET_PERIOD,
 107    * the density of the tableau, d, is computed.
 108    * If d >= s_TABLEAU_RESET_DENSITY * d_initialDensity, the tableau
 109    * is set to d_initialTableau.
 110    */
 111   bool d_presolveHasBeenCalled;
 112   double d_tableauResetDensity;
 113   uint32_t d_tableauResetPeriod;
 114   static const uint32_t s_TABLEAU_RESET_INCREMENT = 5;
 115
 116   /**
 117    * A copy of the tableau immediately after removing variables
 118    * without bounds in presolve().
 119    */
 120   Tableau d_smallTableauCopy;
 121
 122   ArithUnatePropagator d_propagator;
 123
 124   ArithPropManager d_propManager;
 125
 126   SimplexDecisionProcedure d_simplex;
 127
 128 public:
 129   TheoryArith(context::Context* c, OutputChannel& out, Valuation valuation);
 130   ~TheoryArith();
 131
 132   /**
 133    * Does non-context dependent setup for a node connected to a theory.
 134    */
 135   void preRegisterTerm(TNode n);
 136
 137   /** CD setup for a node. Currently does nothing. */
 138   void registerTerm(TNode n);
 139
 140   void check(Effort e);
 141   void propagate(Effort e);
 142   void explain(TNode n);
 143
 144   void notifyEq(TNode lhs, TNode rhs);
 145
 146   Node getValue(TNode n);
 147
 148   void shutdown(){ }
 149
 150   void presolve();
 151   void notifyRestart();
 152   void staticLearning(TNode in, NodeBuilder<>& learned);
 153
 154   std::string identify() const { return std::string("TheoryArith"); }
 155
 156 private:
 157   /** The constant zero. */
 158   DeltaRational d_DELTA_ZERO;
 159
 160   /** propagates an arithvar */
 161   void propagateArithVar(bool upperbound, ArithVar var );
 162
 163   /**
 164    * Using the simpleKind return the ArithVar associated with the
 165    * left hand side of assertion.
 166    */
 167   ArithVar determineLeftVariable(TNode assertion, Kind simpleKind);
 168
 169   /** Splits the disequalities in d_diseq that are violated using lemmas on demand. */
 170   void splitDisequalities();
 171
 172   /**
 173    * This requests a new unique ArithVar value for x.
 174    * This also does initial (not context dependent) set up for a variable,
 175    * except for setting up the initial.
 176    */
 177   ArithVar requestArithVar(TNode x, bool basic);
 178
 179   /** Initial (not context dependent) sets up for a variable.*/
 180   void setupInitialValue(ArithVar x);
 181
 182   /** Initial (not context dependent) sets up for a new slack variable.*/
 183   void setupSlack(TNode left);
 184
 185
 186   /**
 187    * Handles the case splitting for check() for a new assertion.
 188    * Returns a conflict if one was found.
 189    * Returns Node::null if no conflict was found.
 190    */
 191   Node assertionCases(TNode assertion);
 192
 193   /**
 194    * This is used for reporting conflicts caused by disequalities during assertionCases.
 195    */
 196   Node disequalityConflict(TNode eq, TNode lb, TNode ub);
 197
 198   /**
 199    * Returns the basic variable with the shorted row containg a non-basic variable.
 200    * If no such row exists, return ARITHVAR_SENTINEL.
 201    */
 202   ArithVar findShortestBasicRow(ArithVar variable);
 203
 204   /**
 205    * Debugging only routine!
 206    * Returns true iff every variable is consistent in the partial model.
 207    */
 208   bool entireStateIsConsistent();
 209
 210   /**
 211    * Permanently removes a variable from the problem.
 212    * The caller guarentees the saftey of this removal!
 213    */
 214   void permanentlyRemoveVariable(ArithVar v);
 215
 216   bool isImpliedUpperBound(ArithVar var, Node exp);
 217   bool isImpliedLowerBound(ArithVar var, Node exp);
 218
 219   void internalExplain(TNode n, NodeBuilder<>& explainBuilder);
 220
 221
 222   void asVectors(Polynomial& p,
 223                  std::vector<Rational>& coeffs,
 224                  std::vector<ArithVar>& variables) const;
 225
 226   /** Routine for debugging. Print the assertions the theory is aware of. */
 227   void debugPrintAssertions();
 228   /** Debugging only routine. Prints the model. */
 229   void debugPrintModel();
 230
 231   /** These fields are designed to be accessable to TheoryArith methods. */
 232   class Statistics {
 233   public:
 234     IntStat d_statUserVariables, d_statSlackVariables;
 235     IntStat d_statDisequalitySplits;
 236     IntStat d_statDisequalityConflicts;
 237     TimerStat d_staticLearningTimer;
 238
 239     IntStat d_permanentlyRemovedVariables;
 240     TimerStat d_presolveTime;
 241
 242     IntStat d_initialTableauSize;
 243     //ListStat<uint32_t> d_tableauSizeHistory;
 244     IntStat d_currSetToSmaller;
 245     IntStat d_smallerSetToCurr;
 246     TimerStat d_restartTimer;
 247
 248     Statistics();
 249     ~Statistics();
 250   };
 251
 252   Statistics d_statistics;
 253
 254
 255 };/* class TheoryArith */
 256
 257 }/* CVC4::theory::arith namespace */
 258 }/* CVC4::theory namespace */
 259 }/* CVC4 namespace */
 260
 261 #endif /* __CVC4__THEORY__ARITH__THEORY_ARITH_H */