theory_arith_old.h

Go to the documentation of this file.
00001 /*****************************************************************************/
00002 /*!
00003  * \file theory_arith_old.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_arith_old_h_
00022 #define _cvc3__include__theory_arith_old_h_
00023 
00024 #include "theory_arith.h"
00025 
00026 namespace CVC3 {
00027 
00028 class TheoryArithOld :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   //! Private class for an inequality in the Fourier-Motzkin database
00048   class Ineq {
00049   private:
00050     Theorem d_ineq; //!< The inequality
00051     bool d_rhs; //!< Var is isolated on the RHS
00052     const FreeConst* d_const; //!< The max/min const for subsumption check
00053     //! Default constructor is disabled
00054     Ineq() { }
00055   public:
00056     //! Initial constructor.  'r' is taken from the subsumption database.
00057     Ineq(const Theorem& ineq, bool varOnRHS, const FreeConst& c):
00058       d_ineq(ineq), d_rhs(varOnRHS), d_const(&c) { }
00059     //! Get the inequality
00060     const Theorem& ineq() const { return d_ineq; }
00061     //! Get the max/min constant
00062     const FreeConst& getConst() const { return *d_const; }
00063     //! Flag whether var is isolated on the RHS
00064     bool varOnRHS() const { return d_rhs; }
00065     //! Flag whether var is isolated on the LHS
00066     bool varOnLHS() const { return !d_rhs; }
00067     //! Auto-cast to Theorem
00068     operator Theorem() const { return d_ineq; }
00069   };
00070   //! Printing
00071   friend std::ostream& operator<<(std::ostream& os, const Ineq& ineq);
00072   //! Database of inequalities with a variable isolated on the right
00073   ExprMap<CDList<Ineq> *> d_inequalitiesRightDB;
00074   //! Database of inequalities with a variable isolated on the left
00075   ExprMap<CDList<Ineq> *> d_inequalitiesLeftDB;
00076   //! Mapping of inequalities to the largest/smallest free constant
00077   /*! The Expr is the original inequality with the free constant
00078    * removed and inequality converted to non-strict (for indexing
00079    * purposes).  I.e. ax<c+t becomes ax<=t.  This inequality is mapped
00080    * to a pair<c,strict>, the smallest (largest for c+t<ax) constant
00081    * among inequalities with the same 'a', 'x', and 't', and a boolean
00082    * flag indicating whether the strongest inequality is strict.
00083    */
00084   CDMap<Expr, FreeConst> d_freeConstDB;
00085   // Input buffer to store the incoming inequalities
00086   CDList<Theorem> d_buffer; //!< Buffer of input inequalities
00087   CDO<size_t> d_bufferIdx; //!< Buffer index of the next unprocessed inequality
00088   const int* d_bufferThres; //!< Threshold when the buffer must be processed
00089   // Statistics for the variables
00090   /*! @brief Mapping of a variable to the number of inequalities where
00091     the variable would be isolated on the right */
00092   CDMap<Expr, int> d_countRight;
00093   /*! @brief Mapping of a variable to the number of inequalities where
00094     the variable would be isolated on the left */
00095   CDMap<Expr, int> d_countLeft;
00096   //! Set of shared terms (for counterexample generation)
00097   CDMap<Expr, bool> d_sharedTerms;
00098   //! Set of shared integer variables (i-leaves)
00099   CDMap<Expr, bool> d_sharedVars;
00100   //Directed Acyclic Graph representing partial variable ordering for
00101   //variable projection over inequalities.
00102   class VarOrderGraph {
00103     ExprMap<std::vector<Expr> > d_edges;
00104     ExprMap<bool> d_cache;
00105     bool dfs(const Expr& e1, const Expr& e2);
00106   public:
00107     void addEdge(const Expr& e1, const Expr& e2);
00108     //returns true if e1 < e2, false otherwise.
00109     bool lessThan(const Expr& e1, const Expr& e2);
00110     //selects those variables which are largest and incomparable among
00111     //v1 and puts it into v2
00112     void selectLargest(const std::vector<Expr>& v1, std::vector<Expr>& v2);
00113     //selects those variables which are smallest and incomparable among
00114     //v1, removes them from v1 and  puts them into v2. 
00115     void selectSmallest( std::vector<Expr>& v1, std::vector<Expr>& v2);
00116 
00117   };
00118   
00119   VarOrderGraph d_graph;
00120 
00121   // Private methods
00122   //! Check the term t for integrality.  
00123   /*! \return a theorem of IS_INTEGER(t) or Null. */
00124   Theorem isIntegerThm(const Expr& e);
00125   //! A helper method for isIntegerThm()
00126   /*! Check if IS_INTEGER(e) is easily derivable from the given 'thm' */
00127   Theorem isIntegerDerive(const Expr& isIntE, const Theorem& thm);
00128   //! Check the term t for integrality (return bool)
00129   bool isInteger(const Expr& e) { return !(isIntegerThm(e).isNull()); }
00130   //! Extract the free constant from an inequality
00131   const Rational& freeConstIneq(const Expr& ineq, bool varOnRHS);
00132   //! Update the free constant subsumption database with new inequality
00133   /*! \return a reference to the max/min constant.
00134    *
00135    * Also, sets 'subsumed' argument to true if the inequality is
00136    * subsumed by an existing inequality.
00137    */
00138   const FreeConst& updateSubsumptionDB(const Expr& ineq, bool varOnRHS,
00139               bool& subsumed);
00140   //! Check if the kids of e are fully simplified and canonized (for debugging)
00141   bool kidsCanonical(const Expr& e);
00142   //! Canonize the expression e, assuming all children are canonical
00143   Theorem canon(const Expr& e);
00144   /*! @brief Canonize and reduce e w.r.t. union-find database; assume
00145    * all children are canonical */
00146   Theorem canonSimplify(const Expr& e);
00147   /*! @brief Composition of canonSimplify(const Expr&) by
00148    * transitivity: take e0 = e1, canonize and simplify e1 to e2,
00149    * return e0 = e2. */
00150   Theorem canonSimplify(const Theorem& thm) {
00151     return transitivityRule(thm, canonSimplify(thm.getRHS()));
00152   }
00153   //! Canonize predicate (x = y, x < y, etc.)
00154   Theorem canonPred(const Theorem& thm);
00155   //! Canonize predicate like canonPred except that the input theorem
00156   //! is an equivalent transformation.
00157   Theorem canonPredEquiv(const Theorem& thm);
00158   //! Solve an equation and return an equivalent Theorem in the solved form
00159   Theorem doSolve(const Theorem& e);
00160   //! takes in a conjunction equivalence Thm and canonizes it.
00161   Theorem canonConjunctionEquiv(const Theorem& thm);
00162   //! picks the monomial with the smallest abs(coeff) from the input
00163   //integer equation.
00164   Expr pickIntEqMonomial(const Expr& right);
00165   //! processes equalities with 1 or more vars of type REAL
00166   Theorem processRealEq(const Theorem& eqn);
00167   //! processes equalities whose vars are all of type INT
00168   Theorem processIntEq(const Theorem& eqn);
00169   //! One step of INT equality processing (aux. method for processIntEq())
00170   Theorem processSimpleIntEq(const Theorem& eqn);
00171   //! Process inequalities in the buffer
00172   void processBuffer();
00173   //! Take an inequality and isolate a variable
00174   Theorem isolateVariable(const Theorem& inputThm, bool& e1);
00175   //! Update the statistics counters for the variable with a coeff. c
00176   void updateStats(const Rational& c, const Expr& var);
00177   //! Update the statistics counters for the monomial
00178   void updateStats(const Expr& monomial);
00179   //! Add an inequality to the input buffer.  See also d_buffer
00180   void addToBuffer(const Theorem& thm);
00181   /*! @brief Given a canonized term, compute a factor to make all
00182     coefficients integer and relatively prime */
00183   Expr computeNormalFactor(const Expr& rhs);
00184   //! Normalize an equation (make all coefficients rel. prime integers)
00185   Theorem normalize(const Expr& e);
00186   //! Normalize an equation (make all coefficients rel. prime integers)
00187   /*! accepts a rewrite theorem over eqn|ineqn and normalizes it
00188    *  and returns a theorem to that effect.
00189    */
00190   Theorem normalize(const Theorem& thm);
00191   Expr pickMonomial(const Expr& right);
00192  public: // ArithTheoremProducer needs this function, so make it public
00193   //! Separate monomial e = c*p1*...*pn into c and 1*p1*...*pn
00194   void separateMonomial(const Expr& e, Expr& c, Expr& var);
00195  private:
00196   bool lessThanVar(const Expr& isolatedVar, const Expr& var2);
00197   //! Check if the term expression is "stale"
00198   bool isStale(const Expr& e);
00199   //! Check if the inequality is "stale" or subsumed
00200   bool isStale(const Ineq& ineq);
00201   void projectInequalities(const Theorem& theInequality,bool isolatedVarOnRHS);
00202   void assignVariables(std::vector<Expr>&v);
00203   void findRationalBound(const Expr& varSide, const Expr& ratSide, 
00204        const Expr& var,
00205        Rational &r);
00206   bool findBounds(const Expr& e, Rational& lub, Rational&  glb);
00207 
00208   Theorem normalizeProjectIneqs(const Theorem& ineqThm1,
00209         const Theorem& ineqThm2);
00210   //! Take a system of equations and turn it into a solved form
00211   Theorem solvedForm(const std::vector<Theorem>& solvedEqs);
00212   /*! @brief Substitute all vars in term 't' according to the
00213    * substitution 'subst' and canonize the result.
00214    */
00215   Theorem substAndCanonize(const Expr& t, ExprMap<Theorem>& subst);
00216   /*! @brief Substitute all vars in the RHS of the equation 'eq' of
00217    * the form (x = t) according to the substitution 'subst', and
00218    * canonize the result.
00219    */
00220   Theorem substAndCanonize(const Theorem& eq, ExprMap<Theorem>& subst);
00221   //! Traverse 'e' and push all the i-leaves into 'vars' vector
00222   void collectVars(const Expr& e, std::vector<Expr>& vars,
00223        std::set<Expr>& cache);
00224   /*! @brief Check if alpha <= ax & bx <= beta is a finite interval
00225    *  for integer var 'x', and assert the corresponding constraint
00226    */
00227   void processFiniteInterval(const Theorem& alphaLEax,
00228            const Theorem& bxLEbeta);
00229   //! For an integer var 'x', find and process all constraints A <= ax <= A+c 
00230   void processFiniteIntervals(const Expr& x);
00231   //! Recursive setup for isolated inequalities (and other new expressions)
00232   void setupRec(const Expr& e);
00233 
00234 public:
00235   TheoryArithOld(TheoryCore* core);
00236   ~TheoryArithOld();
00237 
00238   // Trusted method that creates the proof rules class (used in constructor).
00239   // Implemented in arith_theorem_producer.cpp
00240   ArithProofRules* createProofRulesOld();
00241 
00242   // Theory interface
00243   void addSharedTerm(const Expr& e);
00244   void assertFact(const Theorem& e);
00245   void refineCounterExample();
00246   void computeModelBasic(const std::vector<Expr>& v);
00247   void computeModel(const Expr& e, std::vector<Expr>& vars);
00248   void checkSat(bool fullEffort);
00249   Theorem rewrite(const Expr& e);
00250   void setup(const Expr& e);
00251   void update(const Theorem& e, const Expr& d);
00252   Theorem solve(const Theorem& e);
00253   void checkAssertEqInvariant(const Theorem& e);
00254   void checkType(const Expr& e);
00255   void computeType(const Expr& e);
00256   Type computeBaseType(const Type& t);
00257   void computeModelTerm(const Expr& e, std::vector<Expr>& v);
00258   Expr computeTypePred(const Type& t, const Expr& e);
00259   Expr computeTCC(const Expr& e);
00260   ExprStream& print(ExprStream& os, const Expr& e);
00261   Expr parseExprOp(const Expr& e);
00262 
00263 };
00264 
00265 }
00266 
00267 #endif

Generated on Tue Jul 3 14:33:40 2007 for CVC3 by  doxygen 1.5.1