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,
39 SUBRANGE,
40
41 UMINUS,
42 PLUS,
43 MINUS,
44 MULT,
45 DIVIDE,
46 POW,
47 INTDIV,
48 MOD,
49 LT,
50 LE,
51 GT,
52 GE,
53 IS_INTEGER,
54 DARK_SHADOW,
55 GRAY_SHADOW
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:
72 Type d_realType;
73 Type d_intType;
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:
TheoryArith(TheoryCore * core,const std::string & name)98 TheoryArith(TheoryCore* core, const std::string& name)
99 : Theory(core, name) {}
~TheoryArith()100 ~TheoryArith() {}
101
addMultiplicativeSignSplit(const Theorem & case_split_thm)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 */
addPairToArithOrder(const Expr & smaller,const Expr & bigger)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. */
canonThm(const Theorem & thm)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
realType()152 Type realType() { return d_realType; }
intType()153 Type intType() { return d_intType;}
subrangeType(const Expr & l,const Expr & r)154 Type subrangeType(const Expr& l, const Expr& r)
155 { return Type(Expr(SUBRANGE, l, r)); }
rat(Rational 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
darkShadow(const Expr & lhs,const Expr & 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 */
grayShadow(const Expr & v,const Expr & e,const Rational & c1,const Rational & c2)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
isReal(Type t)173 inline bool isReal(Type t) { return t.getExpr().getKind() == REAL; }
isInt(Type t)174 inline bool isInt(Type t) { return t.getExpr().getKind() == INT; }
175
176 // Static arith testers
isRational(const Expr & e)177 inline bool isRational(const Expr& e) { return e.isRational(); }
isIntegerConst(const Expr & e)178 inline bool isIntegerConst(const Expr& e)
179 { return e.isRational() && e.getRational().isInteger(); }
isUMinus(const Expr & e)180 inline bool isUMinus(const Expr& e) { return e.getKind() == UMINUS; }
isPlus(const Expr & e)181 inline bool isPlus(const Expr& e) { return e.getKind() == PLUS; }
isMinus(const Expr & e)182 inline bool isMinus(const Expr& e) { return e.getKind() == MINUS; }
isMult(const Expr & e)183 inline bool isMult(const Expr& e) { return e.getKind() == MULT; }
isDivide(const Expr & e)184 inline bool isDivide(const Expr& e) { return e.getKind() == DIVIDE; }
isPow(const Expr & e)185 inline bool isPow(const Expr& e) { return e.getKind() == POW; }
isLT(const Expr & e)186 inline bool isLT(const Expr& e) { return e.getKind() == LT; }
isLE(const Expr & e)187 inline bool isLE(const Expr& e) { return e.getKind() == LE; }
isGT(const Expr & e)188 inline bool isGT(const Expr& e) { return e.getKind() == GT; }
isGE(const Expr & e)189 inline bool isGE(const Expr& e) { return e.getKind() == GE; }
isDarkShadow(const Expr & e)190 inline bool isDarkShadow(const Expr& e) { return e.getKind() == DARK_SHADOW;}
isGrayShadow(const Expr & e)191 inline bool isGrayShadow(const Expr& e) { return e.getKind() == GRAY_SHADOW;}
isIneq(const Expr & e)192 inline bool isIneq(const Expr& e)
193 { return isLT(e) || isLE(e) || isGT(e) || isGE(e); }
isIntPred(const Expr & e)194 inline bool isIntPred(const Expr& e) { return e.getKind() == IS_INTEGER; }
195
196 // Static arith constructors
uminusExpr(const Expr & child)197 inline Expr uminusExpr(const Expr& child)
198 { return Expr(UMINUS, child); }
plusExpr(const Expr & left,const Expr & right)199 inline Expr plusExpr(const Expr& left, const Expr& right)
200 { return Expr(PLUS, left, right); }
plusExpr(const std::vector<Expr> & children)201 inline Expr plusExpr(const std::vector<Expr>& children) {
202 DebugAssert(children.size() > 0, "plusExpr()");
203 return Expr(PLUS, children);
204 }
minusExpr(const Expr & left,const Expr & right)205 inline Expr minusExpr(const Expr& left, const Expr& right)
206 { return Expr(MINUS, left, right); }
multExpr(const Expr & left,const Expr & 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
multExpr(const std::vector<Expr> & 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
powExpr(const Expr & pow,const Expr & base)216 inline Expr powExpr(const Expr& pow, const Expr & base)
217 { return Expr(POW, pow, base);}
218 // End Deepak
divideExpr(const Expr & left,const Expr & right)219 inline Expr divideExpr(const Expr& left, const Expr& right)
220 { return Expr(DIVIDE, left, right); }
ltExpr(const Expr & left,const Expr & right)221 inline Expr ltExpr(const Expr& left, const Expr& right)
222 { return Expr(LT, left, right); }
leExpr(const Expr & left,const Expr & right)223 inline Expr leExpr(const Expr& left, const Expr& right)
224 { return Expr(LE, left, right); }
gtExpr(const Expr & left,const Expr & right)225 inline Expr gtExpr(const Expr& left, const Expr& right)
226 { return Expr(GT, left, right); }
geExpr(const Expr & left,const Expr & 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
244