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
Theorem substAndCanonize(const Expr &t, ExprMap< Theorem > &subst)
Substitute all vars in term 't' according to the substitution 'subst' and canonize the result...
Theorem processRealEq(const Theorem &eqn)
processes equalities with 1 or more vars of type REAL
void refineCounterExample()
Process disequalities from the arrangement for model generation.
Expr computeTypePred(const Type &t, const Expr &e)
Theory specific computation of the subtyping predicate for type t applied to the expression e...
CDMap< Expr, Rational > fixedMaxCoefficient
void checkType(const Expr &e)
Check that e is a valid Type expr.
Theorem isolateVariable(const Theorem &inputThm, bool &e1)
Take an inequality and isolate a variable.
Theorem d_ineq
The inequality.
Definition: theory_arith3.h:51
ArithProofRules * d_rules
Definition: theory_arith3.h:31
Data structure of expressions in CVC3.
Definition: expr.h:133
Theorem isIntegerDerive(const Expr &isIntE, const Theorem &thm)
A helper method for isIntegerThm()
This theory handles the built-in logical connectives plus equality. It also handles the registration ...
Definition: theory_core.h:53
TheoryArith3(TheoryCore *core)
void addSharedTerm(const Expr &e)
Notify theory of a new shared term.
Theorem processSimpleIntEq(const Theorem &eqn)
One step of INT equality processing (aux. method for processIntEq())
void computeType(const Expr &e)
Compute and store the type of e.
void setupRec(const Expr &e)
Recursive setup for isolated inequalities (and other new expressions)
bool varOnLHS() const
Flag whether var is isolated on the LHS.
Definition: theory_arith3.h:67
Data class for the strongest free constant in separation inqualities.
Definition: theory_arith3.h:35
This theory handles basic linear arithmetic.
Definition: theory_arith.h:70
Theorem doSolve(const Theorem &e)
Solve an equation and return an equivalent Theorem in the solved form.
Theorem rewrite(const Expr &e)
Theory-specific rewrite rules.
T max(T a, T b)
Definition: cvc_util.h:56
Theorem canon(const Expr &e)
Canonize the expression e, assuming all children are canonical.
MS C++ specific settings.
Definition: type.h:42
CDO< size_t > d_bufferIdx
Buffer index of the next unprocessed inequality.
Definition: theory_arith3.h:93
bool lessThan(const Expr &e1, const Expr &e2)
bool varOnRHS() const
Flag whether var is isolated on the RHS.
Definition: theory_arith3.h:65
void processFiniteIntervals(const Expr &x)
For an integer var 'x', find and process all constraints A <= ax <= A+c.
const FreeConst * d_const
Definition: theory_arith3.h:53
ExprMap< CDList< Ineq > * > d_inequalitiesLeftDB
Database of inequalities with a variable isolated on the left.
Definition: theory_arith3.h:78
CDO< size_t > d_diseqIdx
Definition: theory_arith3.h:30
void selectLargest(const std::vector< Expr > &v1, std::vector< Expr > &v2)
void assignVariables(std::vector< Expr > &v)
Theorem canonPredEquiv(const Theorem &thm)
Theorem canonConjunctionEquiv(const Theorem &thm)
takes in a conjunction equivalence Thm and canonizes it.
void update(const Theorem &e, const Expr &d)
Notify a theory of a new equality.
void separateMonomial(const Expr &e, Expr &c, Expr &var)
Separate monomial e = c*p1*...*pn into c and 1*p1*...*pn.
void projectInequalities(const Theorem &theInequality, bool isolatedVarOnRHS)
ExprMap< CDList< Ineq > * > d_inequalitiesRightDB
Database of inequalities with a variable isolated on the right.
Definition: theory_arith3.h:75
void computeModel(const Expr &e, std::vector< Expr > &vars)
Compute the value of a compound variable from the more primitive ones.
const Theorem & ineq() const
Get the inequality.
Definition: theory_arith3.h:61
Ineq(const Theorem &ineq, bool varOnRHS, const FreeConst &c)
Initial constructor. 'r' is taken from the subsumption database.
Definition: theory_arith3.h:58
void selectSmallest(std::vector< Expr > &v1, std::vector< Expr > &v2)
Expr parseExprOp(const Expr &e)
Theory-specific parsing implemented by the DP.
void getFactors(const Expr &e, std::set< Expr > &factors)
Type computeBaseType(const Type &t)
Compute the base type of the top-level operator of an arbitrary type.
bool findBounds(const Expr &e, Rational &lub, Rational &glb)
CDList< Theorem > d_buffer
Buffer of input inequalities.
Definition: theory_arith3.h:91
CDMap< Expr, Rational > maxCoefficientRight
ArithProofRules * createProofRules3()
bool kidsCanonical(const Expr &e)
Check if the kids of e are fully simplified and canonized (for debugging)
void computeModelTerm(const Expr &e, std::vector< Expr > &v)
Add variables from 'e' to 'v' for constructing a concrete model.
Theorem processIntEq(const Theorem &eqn)
processes equalities whose vars are all of type INT
Rational currentMaxCoefficient(Expr var)
bool isInteger(const Expr &e)
Check the term t for integrality (return bool)
ExprStream & print(ExprStream &os, const Expr &e)
Theory-specific pretty-printing.
Pretty-printing output stream for Expr. READ THE DOCS BEFORE USING!
Definition: expr_stream.h:110
void updateStats(const Rational &c, const Expr &var)
Update the statistics counters for the variable with a coeff. c.
const Rational & getConst() const
Definition: theory_arith3.h:42
const Expr & getRHS() const
Definition: theorem.cpp:246
CDList< Theorem > d_diseq
Definition: theory_arith3.h:29
CDMap< Expr, bool > d_sharedTerms
Set of shared terms (for counterexample generation)
const int * d_bufferThres
Threshold when the buffer must be processed.
Definition: theory_arith3.h:95
Ineq()
Default constructor is disabled.
Definition: theory_arith3.h:55
void assertFact(const Theorem &e)
Assert a new fact to the decision procedure.
bool isNull() const
Definition: theorem.h:164
Theorem normalizeProjectIneqs(const Theorem &ineqThm1, const Theorem &ineqThm2)
const Rational & freeConstIneq(const Expr &ineq, bool varOnRHS)
Extract the free constant from an inequality.
CDMap< Expr, int > d_countRight
Mapping of a variable to the number of inequalities where the variable would be isolated on the right...
CDMap< Expr, FreeConst > d_freeConstDB
Mapping of inequalities to the largest/smallest free constant.
Definition: theory_arith3.h:88
bool lessThanVar(const Expr &isolatedVar, const Expr &var2)
bool pickIntEqMonomial(const Expr &right, Expr &isolated, bool &nonlin)
picks the monomial with the smallest abs(coeff) from the input
void collectVars(const Expr &e, std::vector< Expr > &vars, std::set< Expr > &cache)
Traverse 'e' and push all the i-leaves into 'vars' vector.
static int right(int i)
Definition: minisat_heap.h:54
void findRationalBound(const Expr &varSide, const Expr &ratSide, const Expr &var, Rational &r)
Cardinality finiteTypeInfo(Expr &e, Unsigned &n, bool enumerate, bool computeSize)
Compute information related to finiteness of types.
bool isStale(const Expr &e)
Check if the term expression is "stale".
Private class for an inequality in the Fourier-Motzkin database.
Definition: theory_arith3.h:49
const FreeConst & getConst() const
Get the max/min constant.
Definition: theory_arith3.h:63
Expr computeNormalFactor(const Expr &rhs)
Given a canonized term, compute a factor to make all coefficients integer and relatively prime...
void selectSmallestByCoefficient(std::vector< Expr > input, std::vector< Expr > &output)
friend std::ostream & operator<<(std::ostream &os, const FreeConst &fc)
Printing.
Theorem canonSimplify(const Theorem &thm)
Composition of canonSimplify(const Expr&) by transitivity: take e0 = e1, canonize and simplify e1 to ...
void checkAssertEqInvariant(const Theorem &e)
A debug check used by the primary solver.
void addEdge(const Expr &e1, const Expr &e2)
void processBuffer()
Process inequalities in the buffer.
void processFiniteInterval(const Theorem &alphaLEax, const Theorem &bxLEbeta)
Check if alpha <= ax & bx <= beta is a finite interval for integer var 'x', and assert the corresponding ...
bool d_rhs
Var is isolated on the RHS.
Definition: theory_arith3.h:52
CDMap< Expr, Rational > maxCoefficientLeft
Theorem normalize(const Expr &e)
Normalize an equation (make all coefficients rel. prime integers)
Cardinality
Enum for cardinality of types.
Definition: expr.h:80
void computeModelBasic(const std::vector< Expr > &v)
Assign concrete values to basic-type variables in v.
Theorem solve(const Theorem &e)
An optional solver.
CDO< bool > d_inModelCreation
Definition: theory_arith3.h:32
Theorem isIntegerThm(const Expr &e)
Check the term t for integrality.
void fixCurrentMaxCoefficient(Expr variable, Rational max)
Expr pickMonomial(const Expr &right)
Expr computeTCC(const Expr &e)
Compute and cache the TCC of e.
Theorem canonPred(const Theorem &thm)
Canonize predicate (x = y, x < y, etc.)
void addToBuffer(const Theorem &thm)
Add an inequality to the input buffer. See also d_buffer.
VarOrderGraph d_graph
void setup(const Expr &e)
Set up the term e for call-backs when e or its children change.
Theorem solvedForm(const std::vector< Theorem > &solvedEqs)
Take a system of equations and turn it into a solved form.
ExprMap< std::vector< Expr > > d_edges
bool dfs(const Expr &e1, const Expr &e2)
Theorem canonSimplify(const Expr &e)
Canonize and reduce e w.r.t. union-find database; assume all children are canonical.
const FreeConst & updateSubsumptionDB(const Expr &ineq, bool varOnRHS, bool &subsumed)
Update the free constant subsumption database with new inequality.
FreeConst(const Rational &r, bool strict)
Definition: theory_arith3.h:41
void checkSat(bool fullEffort)
Check for satisfiability in the theory.
Theorem transitivityRule(const Theorem &a1_eq_a2, const Theorem &a2_eq_a3)
(a1 == a2) & (a2 == a3) ==> (a1 == a3)
Definition: theory.h:681
CDMap< Expr, int > d_countLeft
Mapping of a variable to the number of inequalities where the variable would be isolated on the left...
CDMap< Expr, bool > d_sharedVars
Set of shared integer variables (i-leaves)