33 if (isLeaf(e))
return reflexivityRule(e);
36 vector<Theorem> newChildrenThm;
37 vector<unsigned> changed;
38 for(
int k = 0; k < ar; ++k) {
42 newChildrenThm.push_back(thm);
46 if(changed.size() > 0) {
47 return canonThm(substitutivityRule(e, changed, newChildrenThm));
61 os <<
"-" << (-r).toString();
62 if (printAsReal) os <<
".0";
71 os <<
space << (-r).toString();
72 if (printAsReal) os <<
".0";
78 if (printAsReal) os <<
".0";
82 os <<
"(" <<
push <<
"/ ";
86 os <<
"-" << (-tmp).toString();
87 if (printAsReal) os <<
".0";
96 os <<
space << (-tmp).toString();
97 if (printAsReal) os <<
".0";
103 if (printAsReal) os <<
".0";
109 if (printAsReal) os <<
".0";
115 bool TheoryArith::isAtomicArithTerm(
const Expr& e)
130 int i=0, iend=e.
arity();
131 for(; i!=iend; ++i) {
132 if (!isAtomicArithTerm(e[i]))
return false;
143 bool TheoryArith::isAtomicArithFormula(
const Expr& e)
151 return isAtomicArithTerm(e[0]) && isAtomicArithTerm(e[1]);
168 if (isSyntacticRational(e[0], r)) {
175 if (isSyntacticRational(e[0], num)) {
177 if (isSyntacticRational(e[1], den)) {
191 Expr tmp = e[0] - e[1];
192 tmp = canonRec(tmp).getRHS();
196 switch (e.getKind()) {
198 if (r < 0)
return trueExpr();
199 else return falseExpr();
201 if (r <= 0)
return trueExpr();
202 else return falseExpr();
204 if (r > 0)
return trueExpr();
205 else return falseExpr();
207 if (r >= 0)
return trueExpr();
208 else return falseExpr();
210 if (r == 0)
return trueExpr();
211 else return falseExpr();
216 if (tmp[0].getRational() != -1)
return e;
217 return Expr(e.getOp(), theoryCore()->getTranslator()->zeroVar() - tmp[1], rat(0));
222 if (tmp.
arity() == 2) {
223 if (tmp[1].getKind() ==
MULT) {
224 x = theoryCore()->getTranslator()->zeroVar();
229 y = rat(-1) * theoryCore()->getTranslator()->zeroVar();
232 else if (tmp.
arity() == 3) {
233 if (tmp[1].getKind() ==
MULT) {
237 else if (tmp[2].getKind() ==
MULT) {
246 if (y[0].getRational() != -1)
return e;
247 return Expr(e.getOp(), x - y[1], getEM()->newRatExpr(-c));
250 return Expr(e.getOp(), tmp - theoryCore()->getTranslator()->zeroVar(), rat(0));
259 DebugAssert(canonRec(e).getRHS() == e,
"canonSimp expects input to be canonized");
261 if (isLeaf(e))
return find(e);
263 vector<Theorem> newChildrenThm;
264 vector<unsigned> changed;
266 for (
int k = 0; k < ar; ++k) {
267 thm = canonSimp(e[k]);
269 newChildrenThm.push_back(thm);
270 changed.push_back(k);
273 if(changed.size() > 0) {
274 thm = canonThm(substitutivityRule(e, changed, newChildrenThm));
275 return transitivityRule(thm, find(thm.
getRHS()));
283 bool TheoryArith::recursiveCanonSimpCheck(
const Expr& e)
286 if (e != canonSimp(e).getRHS())
return false;
288 for (; i != iend; ++i)
289 if (!recursiveCanonSimpCheck(*i))
return false;
294 bool TheoryArith::leavesAreNumConst(
const Expr& e)
298 "Expected term or arith prop atom");
321 for (; k < e.
arity(); ++k) {
322 if (!leavesAreNumConst(e[k])) {