00001
00002
00003
00004
00005
00006
00007
00008
00009
00010
00011
00012
00013
00014
00015
00016
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;
00030 CDO<size_t> d_diseqIdx;
00031 ArithProofRules* d_rules;
00032 CDO<bool> d_inModelCreation;
00033
00034
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
00046 friend std::ostream& operator<<(std::ostream& os, const FreeConst& fc);
00047
00048 class Ineq {
00049 private:
00050 Theorem d_ineq;
00051 bool d_rhs;
00052 const FreeConst* d_const;
00053
00054 Ineq() { }
00055 public:
00056
00057 Ineq(const Theorem& ineq, bool varOnRHS, const FreeConst& c):
00058 d_ineq(ineq), d_rhs(varOnRHS), d_const(&c) { }
00059
00060 const Theorem& ineq() const { return d_ineq; }
00061
00062 const FreeConst& getConst() const { return *d_const; }
00063
00064 bool varOnRHS() const { return d_rhs; }
00065
00066 bool varOnLHS() const { return !d_rhs; }
00067
00068 operator Theorem() const { return d_ineq; }
00069 };
00070
00071 friend std::ostream& operator<<(std::ostream& os, const Ineq& ineq);
00072
00073 ExprMap<CDList<Ineq> *> d_inequalitiesRightDB;
00074
00075 ExprMap<CDList<Ineq> *> d_inequalitiesLeftDB;
00076
00077
00078
00079
00080
00081
00082
00083
00084 CDMap<Expr, FreeConst> d_freeConstDB;
00085
00086 CDList<Theorem> d_buffer;
00087 CDO<size_t> d_bufferIdx;
00088 const int* d_bufferThres;
00089
00090
00091
00092 CDMap<Expr, int> d_countRight;
00093
00094
00095 CDMap<Expr, int> d_countLeft;
00096
00097 CDMap<Expr, bool> d_sharedTerms;
00098
00099 CDMap<Expr, bool> d_sharedVars;
00100
00101
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
00109 bool lessThan(const Expr& e1, const Expr& e2);
00110
00111
00112 void selectLargest(const std::vector<Expr>& v1, std::vector<Expr>& v2);
00113
00114
00115 void selectSmallest( std::vector<Expr>& v1, std::vector<Expr>& v2);
00116
00117 };
00118
00119 VarOrderGraph d_graph;
00120
00121
00122
00123
00124 Theorem isIntegerThm(const Expr& e);
00125
00126
00127 Theorem isIntegerDerive(const Expr& isIntE, const Theorem& thm);
00128
00129 bool isInteger(const Expr& e) { return !(isIntegerThm(e).isNull()); }
00130
00131 const Rational& freeConstIneq(const Expr& ineq, bool varOnRHS);
00132
00133
00134
00135
00136
00137
00138 const FreeConst& updateSubsumptionDB(const Expr& ineq, bool varOnRHS,
00139 bool& subsumed);
00140
00141 bool kidsCanonical(const Expr& e);
00142
00143 Theorem canon(const Expr& e);
00144
00145
00146 Theorem canonSimplify(const Expr& e);
00147
00148
00149
00150 Theorem canonSimplify(const Theorem& thm) {
00151 return transitivityRule(thm, canonSimplify(thm.getRHS()));
00152 }
00153
00154 Theorem canonPred(const Theorem& thm);
00155
00156
00157 Theorem canonPredEquiv(const Theorem& thm);
00158
00159 Theorem doSolve(const Theorem& e);
00160
00161 Theorem canonConjunctionEquiv(const Theorem& thm);
00162
00163
00164 Expr pickIntEqMonomial(const Expr& right);
00165
00166 Theorem processRealEq(const Theorem& eqn);
00167
00168 Theorem processIntEq(const Theorem& eqn);
00169
00170 Theorem processSimpleIntEq(const Theorem& eqn);
00171
00172 void processBuffer();
00173
00174 Theorem isolateVariable(const Theorem& inputThm, bool& e1);
00175
00176 void updateStats(const Rational& c, const Expr& var);
00177
00178 void updateStats(const Expr& monomial);
00179
00180 void addToBuffer(const Theorem& thm);
00181
00182
00183 Expr computeNormalFactor(const Expr& rhs);
00184
00185 Theorem normalize(const Expr& e);
00186
00187
00188
00189
00190 Theorem normalize(const Theorem& thm);
00191 Expr pickMonomial(const Expr& right);
00192 public:
00193
00194 void separateMonomial(const Expr& e, Expr& c, Expr& var);
00195 private:
00196 bool lessThanVar(const Expr& isolatedVar, const Expr& var2);
00197
00198 bool isStale(const Expr& e);
00199
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
00211 Theorem solvedForm(const std::vector<Theorem>& solvedEqs);
00212
00213
00214
00215 Theorem substAndCanonize(const Expr& t, ExprMap<Theorem>& subst);
00216
00217
00218
00219
00220 Theorem substAndCanonize(const Theorem& eq, ExprMap<Theorem>& subst);
00221
00222 void collectVars(const Expr& e, std::vector<Expr>& vars,
00223 std::set<Expr>& cache);
00224
00225
00226
00227 void processFiniteInterval(const Theorem& alphaLEax,
00228 const Theorem& bxLEbeta);
00229
00230 void processFiniteIntervals(const Expr& x);
00231
00232 void setupRec(const Expr& e);
00233
00234 public:
00235 TheoryArithOld(TheoryCore* core);
00236 ~TheoryArithOld();
00237
00238
00239
00240 ArithProofRules* createProofRulesOld();
00241
00242
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