CVC3  2.4.1
theory_arith.h
Go to the documentation of this file.
1 /*****************************************************************************/
2 /*!
3  * \file theory_arith.h
4  *
5  * Author: Clark Barrett
6  *
7  * Created: Fri Jan 17 18:34:55 2003
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_arith_h_
22 #define _cvc3__include__theory_arith_h_
23 
24 #include "theory.h"
25 #include "cdmap.h"
26 
27 namespace CVC3 {
28 
29  class ArithProofRules;
30 
31  typedef enum {
32  // New constants
33  REAL_CONST = 30, // wrapper around constants to indicate that they should be real
34  NEGINF = 31,
35  POSINF = 32,
36 
37  REAL = 3000,
38  INT,
40 
46  POW,
48  MOD,
49  LT,
50  LE,
51  GT,
52  GE,
56 
57  } ArithKinds;
58 
59 /*****************************************************************************/
60 /*!
61  *\class TheoryArith
62  *\ingroup Theories
63  *\brief This theory handles basic linear arithmetic.
64  *
65  * Author: Clark Barrett
66  *
67  * Created: Sat Feb 8 14:44:32 2003
68  */
69 /*****************************************************************************/
70 class TheoryArith :public Theory {
71  protected:
74  std::vector<int> d_kinds;
75 
76  protected:
77 
78  //! Canonize the expression e, assuming all children are canonical
79  virtual Theorem canon(const Expr& e) = 0;
80 
81  //! Canonize the expression e recursively
82  Theorem canonRec(const Expr& e);
83 
84  //! Print a rational in SMT-LIB format
85  void printRational(ExprStream& os, const Rational& r,
86  bool printAsReal = false);
87 
88  //! Whether any ite's appear in the arithmetic part of the term e
89  bool isAtomicArithTerm(const Expr& e);
90 
91  //! simplify leaves and then canonize
92  Theorem canonSimp(const Expr& e);
93 
94  //! helper for checkAssertEqInvariant
95  bool recursiveCanonSimpCheck(const Expr& e);
96 
97  public:
98  TheoryArith(TheoryCore* core, const std::string& name)
99  : Theory(core, name) {}
101 
102  virtual void addMultiplicativeSignSplit(const Theorem& case_split_thm) {};
103 
104  /**
105  * Record that smaller should be smaller than bigger in the variable order.
106  * Should be implemented in decision procedures that support it.
107  */
108  virtual bool addPairToArithOrder(const Expr& smaller, const Expr& bigger) { return true; };
109 
110  // Used by translator
111  //! Return whether e is syntactically identical to a rational constant
112  bool isSyntacticRational(const Expr& e, Rational& r);
113  //! Whether any ite's appear in the arithmetic part of the formula e
114  bool isAtomicArithFormula(const Expr& e);
115  //! Rewrite an atom to look like x - y op c if possible--for smtlib translation
116  Expr rewriteToDiff(const Expr& e);
117 
118  /*! @brief Composition of canon(const Expr&) by transitivity: take e0 = e1,
119  * canonize e1 to e2, return e0 = e2. */
120  Theorem canonThm(const Theorem& thm) {
121  return transitivityRule(thm, canon(thm.getRHS()));
122  }
123 
124  // ArithTheoremProducer needs this function, so make it public
125  //! Separate monomial e = c*p1*...*pn into c and 1*p1*...*pn
126  virtual void separateMonomial(const Expr& e, Expr& c, Expr& var) = 0;
127 
128  // Theory interface
129  virtual void addSharedTerm(const Expr& e) = 0;
130  virtual void assertFact(const Theorem& e) = 0;
131  virtual void refineCounterExample() = 0;
132  virtual void computeModelBasic(const std::vector<Expr>& v) = 0;
133  virtual void computeModel(const Expr& e, std::vector<Expr>& vars) = 0;
134  virtual void checkSat(bool fullEffort) = 0;
135  virtual Theorem rewrite(const Expr& e) = 0;
136  virtual void setup(const Expr& e) = 0;
137  virtual void update(const Theorem& e, const Expr& d) = 0;
138  virtual Theorem solve(const Theorem& e) = 0;
139  virtual void checkAssertEqInvariant(const Theorem& e) = 0;
140  virtual void checkType(const Expr& e) = 0;
141  virtual Cardinality finiteTypeInfo(Expr& e, Unsigned& n,
142  bool enumerate, bool computeSize) = 0;
143  virtual void computeType(const Expr& e) = 0;
144  virtual Type computeBaseType(const Type& t) = 0;
145  virtual void computeModelTerm(const Expr& e, std::vector<Expr>& v) = 0;
146  virtual Expr computeTypePred(const Type& t, const Expr& e) = 0;
147  virtual Expr computeTCC(const Expr& e) = 0;
148  virtual ExprStream& print(ExprStream& os, const Expr& e) = 0;
149  virtual Expr parseExprOp(const Expr& e) = 0;
150 
151  // Arith constructors
152  Type realType() { return d_realType; }
153  Type intType() { return d_intType;}
154  Type subrangeType(const Expr& l, const Expr& r)
155  { return Type(Expr(SUBRANGE, l, r)); }
156  Expr rat(Rational r) { return getEM()->newRatExpr(r); }
157  // Dark and Gray shadows (for internal use only)
158  //! Construct the dark shadow expression representing lhs <= rhs
159  Expr darkShadow(const Expr& lhs, const Expr& rhs) {
160  return Expr(DARK_SHADOW, lhs, rhs);
161  }
162  //! Construct the gray shadow expression representing c1 <= v - e <= c2
163  /*! Alternatively, v = e + i for some i s.t. c1 <= i <= c2
164  */
165  Expr grayShadow(const Expr& v, const Expr& e,
166  const Rational& c1, const Rational& c2) {
167  return Expr(GRAY_SHADOW, v, e, rat(c1), rat(c2));
168  }
169  bool leavesAreNumConst(const Expr& e);
170 };
171 
172 // Arith testers
173 inline bool isReal(Type t) { return t.getExpr().getKind() == REAL; }
174 inline bool isInt(Type t) { return t.getExpr().getKind() == INT; }
175 
176 // Static arith testers
177 inline bool isRational(const Expr& e) { return e.isRational(); }
178 inline bool isIntegerConst(const Expr& e)
179  { return e.isRational() && e.getRational().isInteger(); }
180 inline bool isUMinus(const Expr& e) { return e.getKind() == UMINUS; }
181 inline bool isPlus(const Expr& e) { return e.getKind() == PLUS; }
182 inline bool isMinus(const Expr& e) { return e.getKind() == MINUS; }
183 inline bool isMult(const Expr& e) { return e.getKind() == MULT; }
184 inline bool isDivide(const Expr& e) { return e.getKind() == DIVIDE; }
185 inline bool isPow(const Expr& e) { return e.getKind() == POW; }
186 inline bool isLT(const Expr& e) { return e.getKind() == LT; }
187 inline bool isLE(const Expr& e) { return e.getKind() == LE; }
188 inline bool isGT(const Expr& e) { return e.getKind() == GT; }
189 inline bool isGE(const Expr& e) { return e.getKind() == GE; }
190 inline bool isDarkShadow(const Expr& e) { return e.getKind() == DARK_SHADOW;}
191 inline bool isGrayShadow(const Expr& e) { return e.getKind() == GRAY_SHADOW;}
192 inline bool isIneq(const Expr& e)
193  { return isLT(e) || isLE(e) || isGT(e) || isGE(e); }
194 inline bool isIntPred(const Expr& e) { return e.getKind() == IS_INTEGER; }
195 
196 // Static arith constructors
197 inline Expr uminusExpr(const Expr& child)
198  { return Expr(UMINUS, child); }
199 inline Expr plusExpr(const Expr& left, const Expr& right)
200  { return Expr(PLUS, left, right); }
201 inline Expr plusExpr(const std::vector<Expr>& children) {
202  DebugAssert(children.size() > 0, "plusExpr()");
203  return Expr(PLUS, children);
204 }
205 inline Expr minusExpr(const Expr& left, const Expr& right)
206  { return Expr(MINUS, left, right); }
207 inline Expr multExpr(const Expr& left, const Expr& right)
208  { return Expr(MULT, left, right); }
209 // Begin Deepak:
210 //! a Mult expr with two or more children
211 inline Expr multExpr(const std::vector<Expr>& children) {
212  DebugAssert(children.size() > 0, "multExpr()");
213  return Expr(MULT, children);
214 }
215 //! Power (x^n, or base^{pow}) expressions
216 inline Expr powExpr(const Expr& pow, const Expr & base)
217  { return Expr(POW, pow, base);}
218 // End Deepak
219 inline Expr divideExpr(const Expr& left, const Expr& right)
220  { return Expr(DIVIDE, left, right); }
221 inline Expr ltExpr(const Expr& left, const Expr& right)
222  { return Expr(LT, left, right); }
223 inline Expr leExpr(const Expr& left, const Expr& right)
224  { return Expr(LE, left, right); }
225 inline Expr gtExpr(const Expr& left, const Expr& right)
226  { return Expr(GT, left, right); }
227 inline Expr geExpr(const Expr& left, const Expr& right)
228  { return Expr(GE, left, right); }
229 
230 inline Expr operator-(const Expr& child)
231  { return uminusExpr(child); }
232 inline Expr operator+(const Expr& left, const Expr& right)
233  { return plusExpr(left, right); }
234 inline Expr operator-(const Expr& left, const Expr& right)
235  { return minusExpr(left, right); }
236 inline Expr operator*(const Expr& left, const Expr& right)
237  { return multExpr(left, right); }
238 inline Expr operator/(const Expr& left, const Expr& right)
239  { return divideExpr(left, right); }
240 
241 }
242 
243 #endif
Expr minusExpr(const Expr &left, const Expr &right)
Definition: theory_arith.h:205
bool isInt(Type t)
Definition: theory_arith.h:174
virtual void assertFact(const Theorem &e)=0
Assert a new fact to the decision procedure.
Expr ltExpr(const Expr &left, const Expr &right)
Definition: theory_arith.h:221
Data structure of expressions in CVC3.
Definition: expr.h:133
virtual void computeModel(const Expr &e, std::vector< Expr > &vars)=0
Compute the value of a compound variable from the more primitive ones.
This theory handles the built-in logical connectives plus equality. It also handles the registration ...
Definition: theory_core.h:53
virtual Theorem rewrite(const Expr &e)=0
Theory-specific rewrite rules.
virtual void update(const Theorem &e, const Expr &d)=0
Notify a theory of a new equality.
bool isRational() const
Definition: expr.h:431
bool isIntPred(const Expr &e)
Definition: theory_arith.h:194
Expr grayShadow(const Expr &v, const Expr &e, const Rational &c1, const Rational &c2)
Construct the gray shadow expression representing c1 <= v - e <= c2.
Definition: theory_arith.h:165
const Rational & getRational() const
Get the Rational value out of RATIONAL_EXPR.
Definition: expr.h:1135
Expr operator+(const Expr &left, const Expr &right)
Definition: theory_arith.h:232
virtual Type computeBaseType(const Type &t)=0
Compute the base type of the top-level operator of an arbitrary type.
This theory handles basic linear arithmetic.
Definition: theory_arith.h:70
virtual Theorem canon(const Expr &e)=0
Canonize the expression e, assuming all children are canonical.
bool isLE(const Expr &e)
Definition: theory_arith.h:187
bool isAtomicArithTerm(const Expr &e)
Whether any ite's appear in the arithmetic part of the term e.
MS C++ specific settings.
Definition: type.h:42
Base class for theories.
Definition: theory.h:64
bool isGE(const Expr &e)
Definition: theory_arith.h:189
void printRational(ExprStream &os, const Rational &r, bool printAsReal=false)
Print a rational in SMT-LIB format.
Expr operator/(const Expr &left, const Expr &right)
Definition: theory_arith.h:238
virtual void checkType(const Expr &e)=0
Check that e is a valid Type expr.
Expr gtExpr(const Expr &left, const Expr &right)
Definition: theory_arith.h:225
#define DebugAssert(cond, str)
Definition: debug.h:408
virtual void refineCounterExample()=0
Process disequalities from the arrangement for model generation.
virtual void addMultiplicativeSignSplit(const Theorem &case_split_thm)
Definition: theory_arith.h:102
virtual Expr computeTypePred(const Type &t, const Expr &e)=0
Theory specific computation of the subtyping predicate for type t applied to the expression e...
bool isAtomicArithFormula(const Expr &e)
Whether any ite's appear in the arithmetic part of the formula e.
bool isGT(const Expr &e)
Definition: theory_arith.h:188
Expr operator-(const Expr &child)
Definition: theory_arith.h:230
bool isPlus(const Expr &e)
Definition: theory_arith.h:181
bool isMinus(const Expr &e)
Definition: theory_arith.h:182
bool isRational(const Expr &e)
Definition: theory_arith.h:177
virtual void separateMonomial(const Expr &e, Expr &c, Expr &var)=0
Separate monomial e = c*p1*...*pn into c and 1*p1*...*pn.
ArithKinds
Definition: theory_arith.h:31
virtual Cardinality finiteTypeInfo(Expr &e, Unsigned &n, bool enumerate, bool computeSize)=0
Compute information related to finiteness of types.
virtual void computeModelBasic(const std::vector< Expr > &v)=0
Assign concrete values to basic-type variables in v.
const Expr & getExpr() const
Definition: type.h:52
TheoryArith(TheoryCore *core, const std::string &name)
Definition: theory_arith.h:98
virtual bool addPairToArithOrder(const Expr &smaller, const Expr &bigger)
Definition: theory_arith.h:108
Expr operator*(const Expr &left, const Expr &right)
Definition: theory_arith.h:236
bool isInteger() const
bool isSyntacticRational(const Expr &e, Rational &r)
Return whether e is syntactically identical to a rational constant.
static int left(int i)
Definition: minisat_heap.h:53
virtual Expr parseExprOp(const Expr &e)=0
Theory-specific parsing implemented by the DP.
int getKind() const
Definition: expr.h:1168
Pretty-printing output stream for Expr. READ THE DOCS BEFORE USING!
Definition: expr_stream.h:110
virtual void computeType(const Expr &e)=0
Compute and store the type of e.
const Expr & getRHS() const
Definition: theorem.cpp:246
Expr powExpr(const Expr &pow, const Expr &base)
Power (x^n, or base^{pow}) expressions.
Definition: theory_arith.h:216
bool isIntegerConst(const Expr &e)
Definition: theory_arith.h:178
Expr newRatExpr(const Rational &r)
Definition: expr_manager.h:471
bool isIneq(const Expr &e)
Definition: theory_arith.h:192
ExprManager * getEM()
Access to ExprManager.
Definition: theory.h:90
Expr rewriteToDiff(const Expr &e)
Rewrite an atom to look like x - y op c if possible–for smtlib translation.
bool leavesAreNumConst(const Expr &e)
virtual void addSharedTerm(const Expr &e)=0
Notify theory of a new shared term.
bool isDarkShadow(const Expr &e)
Definition: theory_arith.h:190
virtual void computeModelTerm(const Expr &e, std::vector< Expr > &v)=0
Add variables from 'e' to 'v' for constructing a concrete model.
Expr darkShadow(const Expr &lhs, const Expr &rhs)
Construct the dark shadow expression representing lhs <= rhs.
Definition: theory_arith.h:159
Generic API for Theories plus methods commonly used by theories.
static int right(int i)
Definition: minisat_heap.h:54
Theorem canonRec(const Expr &e)
Canonize the expression e recursively.
bool isDivide(const Expr &e)
Definition: theory_arith.h:184
virtual ExprStream & print(ExprStream &os, const Expr &e)=0
Theory-specific pretty-printing.
virtual void checkAssertEqInvariant(const Theorem &e)=0
A debug check used by the primary solver.
Expr rat(Rational r)
Definition: theory_arith.h:156
bool isUMinus(const Expr &e)
Definition: theory_arith.h:180
bool isLT(const Expr &e)
Definition: theory_arith.h:186
Expr plusExpr(const Expr &left, const Expr &right)
Definition: theory_arith.h:199
bool isGrayShadow(const Expr &e)
Definition: theory_arith.h:191
Expr geExpr(const Expr &left, const Expr &right)
Definition: theory_arith.h:227
std::vector< int > d_kinds
Definition: theory_arith.h:74
bool recursiveCanonSimpCheck(const Expr &e)
helper for checkAssertEqInvariant
Cardinality
Enum for cardinality of types.
Definition: expr.h:80
Theorem canonThm(const Theorem &thm)
Composition of canon(const Expr&) by transitivity: take e0 = e1, canonize e1 to e2, return e0 = e2.
Definition: theory_arith.h:120
bool isReal(Type t)
Definition: theory_arith.h:173
Rational pow(Rational pow, const Rational &base)
Raise 'base' into the power of 'pow' (pow must be an integer)
Definition: rational.h:159
bool isPow(const Expr &e)
Definition: theory_arith.h:185
Definition: expr.cpp:35
Expr uminusExpr(const Expr &child)
Definition: theory_arith.h:197
virtual void setup(const Expr &e)=0
Set up the term e for call-backs when e or its children change.
Expr leExpr(const Expr &left, const Expr &right)
Definition: theory_arith.h:223
bool isMult(const Expr &e)
Definition: theory_arith.h:183
Expr divideExpr(const Expr &left, const Expr &right)
Definition: theory_arith.h:219
Theorem canonSimp(const Expr &e)
simplify leaves and then canonize
virtual Theorem solve(const Theorem &e)=0
An optional solver.
Type subrangeType(const Expr &l, const Expr &r)
Definition: theory_arith.h:154
virtual Expr computeTCC(const Expr &e)=0
Compute and cache the TCC of e.
Expr multExpr(const Expr &left, const Expr &right)
Definition: theory_arith.h:207
Theorem transitivityRule(const Theorem &a1_eq_a2, const Theorem &a2_eq_a3)
(a1 == a2) & (a2 == a3) ==> (a1 == a3)
Definition: theory.h:681
virtual void checkSat(bool fullEffort)=0
Check for satisfiability in the theory.