CVC3  2.4.1
theory_arith3.h
Go to the documentation of this file.
1 /*****************************************************************************/
2 /*!
3  * \file theory_arith3.h
4  *
5  * Author: Clark Barrett
6  *
7  * Created: Thu Jun 14 13:22:11 2007
8  *
9  * <hr>
10  *
11  * License to use, copy, modify, sell and/or distribute this software
12  * and its documentation for any purpose is hereby granted without
13  * royalty, subject to the terms and conditions defined in the \ref
14  * LICENSE file provided with this distribution.
15  *
16  * <hr>
17  *
18  */
19 /*****************************************************************************/
20 
21 #ifndef _cvc3__include__theory_arith3_h_
22 #define _cvc3__include__theory_arith3_h_
23 
24 #include "theory_arith.h"
25 
26 namespace CVC3 {
27 
28 class TheoryArith3 :public TheoryArith {
29  CDList<Theorem> d_diseq; // For concrete model generation
30  CDO<size_t> d_diseqIdx; // Index to the next unprocessed disequality
33 
34  //! Data class for the strongest free constant in separation inqualities
35  class FreeConst {
36  private:
38  bool d_strict;
39  public:
40  FreeConst() { }
41  FreeConst(const Rational& r, bool strict): d_r(r), d_strict(strict) { }
42  const Rational& getConst() const { return d_r; }
43  bool strict() const { return d_strict; }
44  };
45  //! Printing
46  friend std::ostream& operator<<(std::ostream& os, const FreeConst& fc);
47 
48  //! Private class for an inequality in the Fourier-Motzkin database
49  class Ineq {
50  private:
51  Theorem d_ineq; //!< The inequality
52  bool d_rhs; //!< Var is isolated on the RHS
53  const FreeConst* d_const; //!< The max/min const for subsumption check
54  //! Default constructor is disabled
55  Ineq() { }
56  public:
57  //! Initial constructor. 'r' is taken from the subsumption database.
58  Ineq(const Theorem& ineq, bool varOnRHS, const FreeConst& c):
59  d_ineq(ineq), d_rhs(varOnRHS), d_const(&c) { }
60  //! Get the inequality
61  const Theorem& ineq() const { return d_ineq; }
62  //! Get the max/min constant
63  const FreeConst& getConst() const { return *d_const; }
64  //! Flag whether var is isolated on the RHS
65  bool varOnRHS() const { return d_rhs; }
66  //! Flag whether var is isolated on the LHS
67  bool varOnLHS() const { return !d_rhs; }
68  //! Auto-cast to Theorem
69  operator Theorem() const { return d_ineq; }
70  };
71  //! Printing
72  friend std::ostream& operator<<(std::ostream& os, const Ineq& ineq);
73 
74  //! Database of inequalities with a variable isolated on the right
76 
77  //! Database of inequalities with a variable isolated on the left
79 
80  //! Mapping of inequalities to the largest/smallest free constant
81  /*! The Expr is the original inequality with the free constant
82  * removed and inequality converted to non-strict (for indexing
83  * purposes). I.e. ax<c+t becomes ax<=t. This inequality is mapped
84  * to a pair<c,strict>, the smallest (largest for c+t<ax) constant
85  * among inequalities with the same 'a', 'x', and 't', and a boolean
86  * flag indicating whether the strongest inequality is strict.
87  */
89 
90  // Input buffer to store the incoming inequalities
91  CDList<Theorem> d_buffer; //!< Buffer of input inequalities
92 
93  CDO<size_t> d_bufferIdx; //!< Buffer index of the next unprocessed inequality
94 
95  const int* d_bufferThres; //!< Threshold when the buffer must be processed
96 
97  // Statistics for the variables
98 
99  /*! @brief Mapping of a variable to the number of inequalities where
100  the variable would be isolated on the right */
102 
103  /*! @brief Mapping of a variable to the number of inequalities where
104  the variable would be isolated on the left */
106 
107  //! Set of shared terms (for counterexample generation)
109 
110  //! Set of shared integer variables (i-leaves)
112 
113  //Directed Acyclic Graph representing partial variable ordering for
114  //variable projection over inequalities.
118  bool dfs(const Expr& e1, const Expr& e2);
119  public:
120  void addEdge(const Expr& e1, const Expr& e2);
121  //returns true if e1 < e2, false otherwise.
122  bool lessThan(const Expr& e1, const Expr& e2);
123  //selects those variables which are largest and incomparable among
124  //v1 and puts it into v2
125  void selectLargest(const std::vector<Expr>& v1, std::vector<Expr>& v2);
126  //selects those variables which are smallest and incomparable among
127  //v1, removes them from v1 and puts them into v2.
128  void selectSmallest( std::vector<Expr>& v1, std::vector<Expr>& v2);
129  };
130 
132 
133  // Private methods
134 
135  //! Check the term t for integrality.
136  /*! \return a theorem of IS_INTEGER(t) or Null. */
137  Theorem isIntegerThm(const Expr& e);
138 
139  //! A helper method for isIntegerThm()
140  /*! Check if IS_INTEGER(e) is easily derivable from the given 'thm' */
141  Theorem isIntegerDerive(const Expr& isIntE, const Theorem& thm);
142 
143  //! Extract the free constant from an inequality
144  const Rational& freeConstIneq(const Expr& ineq, bool varOnRHS);
145 
146  //! Update the free constant subsumption database with new inequality
147  /*! \return a reference to the max/min constant.
148  *
149  * Also, sets 'subsumed' argument to true if the inequality is
150  * subsumed by an existing inequality.
151  */
152  const FreeConst& updateSubsumptionDB(const Expr& ineq, bool varOnRHS,
153  bool& subsumed);
154  //! Check if the kids of e are fully simplified and canonized (for debugging)
155  bool kidsCanonical(const Expr& e);
156 
157  //! Canonize the expression e, assuming all children are canonical
158  Theorem canon(const Expr& e);
159 
160  /*! @brief Canonize and reduce e w.r.t. union-find database; assume
161  * all children are canonical */
162  Theorem canonSimplify(const Expr& e);
163 
164  /*! @brief Composition of canonSimplify(const Expr&) by
165  * transitivity: take e0 = e1, canonize and simplify e1 to e2,
166  * return e0 = e2. */
168  return transitivityRule(thm, canonSimplify(thm.getRHS()));
169  }
170 
171  //! Canonize predicate (x = y, x < y, etc.)
172  Theorem canonPred(const Theorem& thm);
173 
174  //! Canonize predicate like canonPred except that the input theorem
175  //! is an equivalent transformation.
176  Theorem canonPredEquiv(const Theorem& thm);
177 
178  //! Solve an equation and return an equivalent Theorem in the solved form
179  Theorem doSolve(const Theorem& e);
180 
181  //! takes in a conjunction equivalence Thm and canonizes it.
183 
184  //! picks the monomial with the smallest abs(coeff) from the input
185  //integer equation.
186  bool pickIntEqMonomial(const Expr& right, Expr& isolated, bool& nonlin);
187 
188  //! processes equalities with 1 or more vars of type REAL
189  Theorem processRealEq(const Theorem& eqn);
190 
191  //! processes equalities whose vars are all of type INT
192  Theorem processIntEq(const Theorem& eqn);
193 
194  //! One step of INT equality processing (aux. method for processIntEq())
195  Theorem processSimpleIntEq(const Theorem& eqn);
196 
197  //! Process inequalities in the buffer
198  void processBuffer();
199 
200  //! Take an inequality and isolate a variable
201  Theorem isolateVariable(const Theorem& inputThm, bool& e1);
202 
203  //! Update the statistics counters for the variable with a coeff. c
204  void updateStats(const Rational& c, const Expr& var);
205 
206  //! Update the statistics counters for the monomial
207  void updateStats(const Expr& monomial);
208 
209  //! Add an inequality to the input buffer. See also d_buffer
210  void addToBuffer(const Theorem& thm);
211 
212  /*! @brief Given a canonized term, compute a factor to make all
213  coefficients integer and relatively prime */
214  Expr computeNormalFactor(const Expr& rhs);
215 
216  //! Normalize an equation (make all coefficients rel. prime integers)
217  Theorem normalize(const Expr& e);
218 
219  //! Normalize an equation (make all coefficients rel. prime integers)
220  /*! accepts a rewrite theorem over eqn|ineqn and normalizes it
221  * and returns a theorem to that effect.
222  */
223  Theorem normalize(const Theorem& thm);
224 
225  Expr pickMonomial(const Expr& right);
226 
227  void getFactors(const Expr& e, std::set<Expr>& factors);
228 
229  public: // ArithTheoremProducer needs this function, so make it public
230  //! Separate monomial e = c*p1*...*pn into c and 1*p1*...*pn
231  void separateMonomial(const Expr& e, Expr& c, Expr& var);
232  //! Check the term t for integrality (return bool)
233  bool isInteger(const Expr& e) { return !(isIntegerThm(e).isNull()); }
234 
235 
236  private:
237 
238  bool lessThanVar(const Expr& isolatedVar, const Expr& var2);
239 
240  //! Check if the term expression is "stale"
241  bool isStale(const Expr& e);
242 
243  //! Check if the inequality is "stale" or subsumed
244  bool isStale(const Ineq& ineq);
245 
246  void projectInequalities(const Theorem& theInequality,bool isolatedVarOnRHS);
247 
248  void assignVariables(std::vector<Expr>&v);
249 
250  void findRationalBound(const Expr& varSide, const Expr& ratSide,
251  const Expr& var,
252  Rational &r);
253 
254  bool findBounds(const Expr& e, Rational& lub, Rational& glb);
255 
256  Theorem normalizeProjectIneqs(const Theorem& ineqThm1,
257  const Theorem& ineqThm2);
258 
259  //! Take a system of equations and turn it into a solved form
260  Theorem solvedForm(const std::vector<Theorem>& solvedEqs);
261 
262  /*! @brief Substitute all vars in term 't' according to the
263  * substitution 'subst' and canonize the result.
264  */
265  Theorem substAndCanonize(const Expr& t, ExprMap<Theorem>& subst);
266 
267  /*! @brief Substitute all vars in the RHS of the equation 'eq' of
268  * the form (x = t) according to the substitution 'subst', and
269  * canonize the result.
270  */
272 
273  //! Traverse 'e' and push all the i-leaves into 'vars' vector
274  void collectVars(const Expr& e, std::vector<Expr>& vars,
275  std::set<Expr>& cache);
276 
277  /*! @brief Check if alpha <= ax & bx <= beta is a finite interval
278  * for integer var 'x', and assert the corresponding constraint
279  */
280  void processFiniteInterval(const Theorem& alphaLEax,
281  const Theorem& bxLEbeta);
282 
283  //! For an integer var 'x', find and process all constraints A <= ax <= A+c
284  void processFiniteIntervals(const Expr& x);
285 
286  //! Recursive setup for isolated inequalities (and other new expressions)
287  void setupRec(const Expr& e);
288 
289 public:
290  TheoryArith3(TheoryCore* core);
291  ~TheoryArith3();
292 
293  // Trusted method that creates the proof rules class (used in constructor).
294  // Implemented in arith_theorem_producer.cpp
296 
297  // Theory interface
298  void addSharedTerm(const Expr& e);
299  void assertFact(const Theorem& e);
300  void refineCounterExample();
301  void computeModelBasic(const std::vector<Expr>& v);
302  void computeModel(const Expr& e, std::vector<Expr>& vars);
303  void checkSat(bool fullEffort);
304  Theorem rewrite(const Expr& e);
305  void setup(const Expr& e);
306  void update(const Theorem& e, const Expr& d);
307  Theorem solve(const Theorem& e);
308  void checkAssertEqInvariant(const Theorem& e);
309  void checkType(const Expr& e);
311  bool enumerate, bool computeSize);
312  void computeType(const Expr& e);
313  Type computeBaseType(const Type& t);
314  void computeModelTerm(const Expr& e, std::vector<Expr>& v);
315  Expr computeTypePred(const Type& t, const Expr& e);
316  Expr computeTCC(const Expr& e);
317  ExprStream& print(ExprStream& os, const Expr& e);
318  Expr parseExprOp(const Expr& e);
319 
320 private:
321 
322  /** Map from variables to the maximal (by absolute value) of one of it's coefficients */
325 
326  /** Map from variables to the fixed value of one of it's coefficients */
328 
329  /**
330  * Returns the current maximal coefficient of the variable.
331  *
332  * @param var the variable.
333  */
335 
336  /**
337  * Fixes the current max coefficient to be used in the ordering. If the maximal coefficient
338  * changes in the future, it will not be used in the ordering.
339  *
340  * @param variable the variable
341  * @param max the value to set it to
342  */
343  void fixCurrentMaxCoefficient(Expr variable, Rational max);
344 
345  /**
346  * Among given input variables, select the smallest ones with respect to the coefficients.
347  */
348  void selectSmallestByCoefficient(std::vector<Expr> input, std::vector<Expr>& output);
349 };
350 
351 }
352 
353 #endif