CVC3

theory_arith3.h

Go to the documentation of this file.
00001 /*****************************************************************************/
00002 /*!
00003  * \file theory_arith3.h
00004  * 
00005  * Author: Clark Barrett
00006  * 
00007  * Created: Thu Jun 14 13:22:11 2007
00008  *
00009  * <hr>
00010  *
00011  * License to use, copy, modify, sell and/or distribute this software
00012  * and its documentation for any purpose is hereby granted without
00013  * royalty, subject to the terms and conditions defined in the \ref
00014  * LICENSE file provided with this distribution.
00015  * 
00016  * <hr>
00017  * 
00018  */
00019 /*****************************************************************************/
00020 
00021 #ifndef _cvc3__include__theory_arith3_h_
00022 #define _cvc3__include__theory_arith3_h_
00023 
00024 #include "theory_arith.h"
00025 
00026 namespace CVC3 {
00027 
00028 class TheoryArith3 :public TheoryArith {
00029   CDList<Theorem> d_diseq;  // For concrete model generation
00030   CDO<size_t> d_diseqIdx; // Index to the next unprocessed disequality
00031   ArithProofRules* d_rules;
00032   CDO<bool> d_inModelCreation;
00033 
00034   //! Data class for the strongest free constant in separation inqualities
00035   class FreeConst {
00036   private:
00037     Rational d_r;
00038     bool d_strict;
00039   public:
00040     FreeConst() { }
00041     FreeConst(const Rational& r, bool strict): d_r(r), d_strict(strict) { }
00042     const Rational& getConst() const { return d_r; }
00043     bool strict() const { return d_strict; }
00044   };
00045   //! Printing
00046   friend std::ostream& operator<<(std::ostream& os, const FreeConst& fc);
00047 
00048   //! Private class for an inequality in the Fourier-Motzkin database
00049   class Ineq {
00050   private:
00051     Theorem d_ineq; //!< The inequality
00052     bool d_rhs; //!< Var is isolated on the RHS
00053     const FreeConst* d_const; //!< The max/min const for subsumption check
00054     //! Default constructor is disabled
00055     Ineq() { }
00056   public:
00057     //! Initial constructor.  'r' is taken from the subsumption database.
00058     Ineq(const Theorem& ineq, bool varOnRHS, const FreeConst& c):
00059       d_ineq(ineq), d_rhs(varOnRHS), d_const(&c) { }
00060     //! Get the inequality
00061     const Theorem& ineq() const { return d_ineq; }
00062     //! Get the max/min constant
00063     const FreeConst& getConst() const { return *d_const; }
00064     //! Flag whether var is isolated on the RHS
00065     bool varOnRHS() const { return d_rhs; }
00066     //! Flag whether var is isolated on the LHS
00067     bool varOnLHS() const { return !d_rhs; }
00068     //! Auto-cast to Theorem
00069     operator Theorem() const { return d_ineq; }
00070   };
00071   //! Printing
00072   friend std::ostream& operator<<(std::ostream& os, const Ineq& ineq);
00073 
00074   //! Database of inequalities with a variable isolated on the right
00075   ExprMap<CDList<Ineq> *> d_inequalitiesRightDB;
00076 
00077   //! Database of inequalities with a variable isolated on the left
00078   ExprMap<CDList<Ineq> *> d_inequalitiesLeftDB;
00079 
00080   //! Mapping of inequalities to the largest/smallest free constant
00081   /*! The Expr is the original inequality with the free constant
00082    * removed and inequality converted to non-strict (for indexing
00083    * purposes).  I.e. ax<c+t becomes ax<=t.  This inequality is mapped
00084    * to a pair<c,strict>, the smallest (largest for c+t<ax) constant
00085    * among inequalities with the same 'a', 'x', and 't', and a boolean
00086    * flag indicating whether the strongest inequality is strict.
00087    */
00088   CDMap<Expr, FreeConst> d_freeConstDB;
00089 
00090   // Input buffer to store the incoming inequalities
00091   CDList<Theorem> d_buffer; //!< Buffer of input inequalities
00092 
00093   CDO<size_t> d_bufferIdx; //!< Buffer index of the next unprocessed inequality
00094 
00095   const int* d_bufferThres; //!< Threshold when the buffer must be processed
00096 
00097   // Statistics for the variables
00098 
00099   /*! @brief Mapping of a variable to the number of inequalities where
00100     the variable would be isolated on the right */
00101   CDMap<Expr, int> d_countRight;
00102 
00103   /*! @brief Mapping of a variable to the number of inequalities where
00104     the variable would be isolated on the left */
00105   CDMap<Expr, int> d_countLeft;
00106 
00107   //! Set of shared terms (for counterexample generation)
00108   CDMap<Expr, bool> d_sharedTerms;
00109 
00110   //! Set of shared integer variables (i-leaves)
00111   CDMap<Expr, bool> d_sharedVars;
00112 
00113   //Directed Acyclic Graph representing partial variable ordering for
00114   //variable projection over inequalities.
00115   class VarOrderGraph {
00116     ExprMap<std::vector<Expr> > d_edges;
00117     ExprMap<bool> d_cache;
00118     bool dfs(const Expr& e1, const Expr& e2);
00119   public:
00120     void addEdge(const Expr& e1, const Expr& e2);
00121     //returns true if e1 < e2, false otherwise.
00122     bool lessThan(const Expr& e1, const Expr& e2);
00123     //selects those variables which are largest and incomparable among
00124     //v1 and puts it into v2
00125     void selectLargest(const std::vector<Expr>& v1, std::vector<Expr>& v2);
00126     //selects those variables which are smallest and incomparable among
00127     //v1, removes them from v1 and  puts them into v2. 
00128     void selectSmallest( std::vector<Expr>& v1, std::vector<Expr>& v2);
00129   };
00130   
00131   VarOrderGraph d_graph;
00132 
00133   // Private methods
00134 
00135   //! Check the term t for integrality.  
00136   /*! \return a theorem of IS_INTEGER(t) or Null. */
00137   Theorem isIntegerThm(const Expr& e);
00138 
00139   //! A helper method for isIntegerThm()
00140   /*! Check if IS_INTEGER(e) is easily derivable from the given 'thm' */
00141   Theorem isIntegerDerive(const Expr& isIntE, const Theorem& thm);
00142 
00143   //! Extract the free constant from an inequality
00144   const Rational& freeConstIneq(const Expr& ineq, bool varOnRHS);
00145 
00146   //! Update the free constant subsumption database with new inequality
00147   /*! \return a reference to the max/min constant.
00148    *
00149    * Also, sets 'subsumed' argument to true if the inequality is
00150    * subsumed by an existing inequality.
00151    */
00152   const FreeConst& updateSubsumptionDB(const Expr& ineq, bool varOnRHS,
00153               bool& subsumed);
00154   //! Check if the kids of e are fully simplified and canonized (for debugging)
00155   bool kidsCanonical(const Expr& e);
00156 
00157   //! Canonize the expression e, assuming all children are canonical
00158   Theorem canon(const Expr& e);
00159 
00160   /*! @brief Canonize and reduce e w.r.t. union-find database; assume
00161    * all children are canonical */
00162   Theorem canonSimplify(const Expr& e);
00163 
00164   /*! @brief Composition of canonSimplify(const Expr&) by
00165    * transitivity: take e0 = e1, canonize and simplify e1 to e2,
00166    * return e0 = e2. */
00167   Theorem canonSimplify(const Theorem& thm) {
00168     return transitivityRule(thm, canonSimplify(thm.getRHS()));
00169   }
00170 
00171   //! Canonize predicate (x = y, x < y, etc.)
00172   Theorem canonPred(const Theorem& thm);
00173 
00174   //! Canonize predicate like canonPred except that the input theorem
00175   //! is an equivalent transformation.
00176   Theorem canonPredEquiv(const Theorem& thm);
00177 
00178   //! Solve an equation and return an equivalent Theorem in the solved form
00179   Theorem doSolve(const Theorem& e);
00180 
00181   //! takes in a conjunction equivalence Thm and canonizes it.
00182   Theorem canonConjunctionEquiv(const Theorem& thm);
00183 
00184   //! picks the monomial with the smallest abs(coeff) from the input
00185   //integer equation.
00186   bool pickIntEqMonomial(const Expr& right, Expr& isolated, bool& nonlin);
00187 
00188   //! processes equalities with 1 or more vars of type REAL
00189   Theorem processRealEq(const Theorem& eqn);
00190 
00191   //! processes equalities whose vars are all of type INT
00192   Theorem processIntEq(const Theorem& eqn);
00193 
00194   //! One step of INT equality processing (aux. method for processIntEq())
00195   Theorem processSimpleIntEq(const Theorem& eqn);
00196 
00197   //! Process inequalities in the buffer
00198   void processBuffer();
00199 
00200   //! Take an inequality and isolate a variable
00201   Theorem isolateVariable(const Theorem& inputThm, bool& e1);
00202 
00203   //! Update the statistics counters for the variable with a coeff. c
00204   void updateStats(const Rational& c, const Expr& var);
00205 
00206   //! Update the statistics counters for the monomial
00207   void updateStats(const Expr& monomial);
00208 
00209   //! Add an inequality to the input buffer.  See also d_buffer
00210   void addToBuffer(const Theorem& thm);
00211 
00212   /*! @brief Given a canonized term, compute a factor to make all
00213     coefficients integer and relatively prime */
00214   Expr computeNormalFactor(const Expr& rhs);
00215 
00216   //! Normalize an equation (make all coefficients rel. prime integers)
00217   Theorem normalize(const Expr& e);
00218 
00219   //! Normalize an equation (make all coefficients rel. prime integers)
00220   /*! accepts a rewrite theorem over eqn|ineqn and normalizes it
00221    *  and returns a theorem to that effect.
00222    */
00223   Theorem normalize(const Theorem& thm);
00224 
00225   Expr pickMonomial(const Expr& right);
00226 
00227   void getFactors(const Expr& e, std::set<Expr>& factors);
00228 
00229  public: // ArithTheoremProducer needs this function, so make it public
00230   //! Separate monomial e = c*p1*...*pn into c and 1*p1*...*pn
00231   void separateMonomial(const Expr& e, Expr& c, Expr& var);
00232   //! Check the term t for integrality (return bool)
00233   bool isInteger(const Expr& e) { return !(isIntegerThm(e).isNull()); }
00234 
00235 
00236  private:
00237 
00238   bool lessThanVar(const Expr& isolatedVar, const Expr& var2);
00239 
00240   //! Check if the term expression is "stale"
00241   bool isStale(const Expr& e);
00242 
00243   //! Check if the inequality is "stale" or subsumed
00244   bool isStale(const Ineq& ineq);
00245 
00246   void projectInequalities(const Theorem& theInequality,bool isolatedVarOnRHS);
00247 
00248   void assignVariables(std::vector<Expr>&v);
00249 
00250   void findRationalBound(const Expr& varSide, const Expr& ratSide, 
00251        const Expr& var,
00252        Rational &r);
00253 
00254   bool findBounds(const Expr& e, Rational& lub, Rational&  glb);
00255 
00256   Theorem normalizeProjectIneqs(const Theorem& ineqThm1,
00257         const Theorem& ineqThm2);
00258 
00259   //! Take a system of equations and turn it into a solved form
00260   Theorem solvedForm(const std::vector<Theorem>& solvedEqs);
00261 
00262   /*! @brief Substitute all vars in term 't' according to the
00263    * substitution 'subst' and canonize the result.
00264    */
00265   Theorem substAndCanonize(const Expr& t, ExprMap<Theorem>& subst);
00266 
00267   /*! @brief Substitute all vars in the RHS of the equation 'eq' of
00268    * the form (x = t) according to the substitution 'subst', and
00269    * canonize the result.
00270    */
00271   Theorem substAndCanonize(const Theorem& eq, ExprMap<Theorem>& subst);
00272 
00273   //! Traverse 'e' and push all the i-leaves into 'vars' vector
00274   void collectVars(const Expr& e, std::vector<Expr>& vars,
00275        std::set<Expr>& cache);
00276 
00277   /*! @brief Check if alpha <= ax & bx <= beta is a finite interval
00278    *  for integer var 'x', and assert the corresponding constraint
00279    */
00280   void processFiniteInterval(const Theorem& alphaLEax,
00281            const Theorem& bxLEbeta);
00282 
00283   //! For an integer var 'x', find and process all constraints A <= ax <= A+c 
00284   void processFiniteIntervals(const Expr& x);
00285 
00286   //! Recursive setup for isolated inequalities (and other new expressions)
00287   void setupRec(const Expr& e);
00288 
00289 public:
00290   TheoryArith3(TheoryCore* core);
00291   ~TheoryArith3();
00292 
00293   // Trusted method that creates the proof rules class (used in constructor).
00294   // Implemented in arith_theorem_producer.cpp
00295   ArithProofRules* createProofRules3();
00296 
00297   // Theory interface
00298   void addSharedTerm(const Expr& e);
00299   void assertFact(const Theorem& e);
00300   void refineCounterExample();
00301   void computeModelBasic(const std::vector<Expr>& v);
00302   void computeModel(const Expr& e, std::vector<Expr>& vars);
00303   void checkSat(bool fullEffort);
00304   Theorem rewrite(const Expr& e);
00305   void setup(const Expr& e);
00306   void update(const Theorem& e, const Expr& d);
00307   Theorem solve(const Theorem& e);
00308   void checkAssertEqInvariant(const Theorem& e);
00309   void checkType(const Expr& e);
00310   Cardinality finiteTypeInfo(Expr& e, Unsigned& n,
00311                              bool enumerate, bool computeSize);
00312   void computeType(const Expr& e);
00313   Type computeBaseType(const Type& t);
00314   void computeModelTerm(const Expr& e, std::vector<Expr>& v);
00315   Expr computeTypePred(const Type& t, const Expr& e);
00316   Expr computeTCC(const Expr& e);
00317   ExprStream& print(ExprStream& os, const Expr& e);
00318   Expr parseExprOp(const Expr& e);
00319 
00320 private:
00321   
00322   /** Map from variables to the maximal (by absolute value) of one of it's coefficients */  
00323   CDMap<Expr, Rational> maxCoefficientLeft;
00324   CDMap<Expr, Rational> maxCoefficientRight;
00325   
00326   /** Map from variables to the fixed value of one of it's coefficients */
00327   CDMap<Expr, Rational> fixedMaxCoefficient;  
00328   
00329   /** 
00330    * Returns the current maximal coefficient of the variable.
00331    * 
00332    * @param var the variable.
00333    */
00334   Rational currentMaxCoefficient(Expr var);
00335   
00336   /**
00337    * Fixes the current max coefficient to be used in the ordering. If the maximal coefficient
00338    * changes in the future, it will not be used in the ordering.
00339    * 
00340    * @param variable the variable
00341    * @param max the value to set it to
00342    */ 
00343   void fixCurrentMaxCoefficient(Expr variable, Rational max);
00344   
00345   /**
00346    * Among given input variables, select the smallest ones with respect to the coefficients.
00347    */
00348   void selectSmallestByCoefficient(std::vector<Expr> input, std::vector<Expr>& output);
00349 };
00350 
00351 }
00352 
00353 #endif