diff options
Diffstat (limited to 'src/theory/arith/operator_elim.cpp')
-rw-r--r-- | src/theory/arith/operator_elim.cpp | 85 |
1 files changed, 38 insertions, 47 deletions
diff --git a/src/theory/arith/operator_elim.cpp b/src/theory/arith/operator_elim.cpp index 17efa53a5..99f5621d6 100644 --- a/src/theory/arith/operator_elim.cpp +++ b/src/theory/arith/operator_elim.cpp @@ -173,22 +173,20 @@ Node OperatorElim::eliminateOperators(Node node, nm->mkNode( MULT, den, - nm->mkNode( - PLUS, v, nm->mkConst(CONST_RATIONAL, Rational(1)))))); + nm->mkNode(PLUS, v, nm->mkConstInt(Rational(1)))))); } else { lem = nm->mkNode( AND, leqNum, - nm->mkNode(LT, - num, - nm->mkNode(MULT, - den, - nm->mkNode(PLUS, - v, - nm->mkConst(CONST_RATIONAL, - Rational(-1)))))); + nm->mkNode( + LT, + num, + nm->mkNode( + MULT, + den, + nm->mkNode(PLUS, v, nm->mkConstInt(Rational(-1)))))); } } else @@ -198,34 +196,32 @@ Node OperatorElim::eliminateOperators(Node node, AND, nm->mkNode( IMPLIES, - nm->mkNode(GT, den, nm->mkConst(CONST_RATIONAL, Rational(0))), + nm->mkNode(GT, den, nm->mkConstInt(Rational(0))), nm->mkNode( AND, leqNum, nm->mkNode( LT, num, - nm->mkNode(MULT, - den, - nm->mkNode(PLUS, - v, - nm->mkConst(CONST_RATIONAL, - Rational(1))))))), + nm->mkNode( + MULT, + den, + nm->mkNode( + PLUS, v, nm->mkConstInt(Rational(1))))))), nm->mkNode( IMPLIES, - nm->mkNode(LT, den, nm->mkConst(CONST_RATIONAL, Rational(0))), + nm->mkNode(LT, den, nm->mkConstInt(Rational(0))), nm->mkNode( AND, leqNum, nm->mkNode( LT, num, - nm->mkNode(MULT, - den, - nm->mkNode(PLUS, - v, - nm->mkConst(CONST_RATIONAL, - Rational(-1)))))))); + nm->mkNode( + MULT, + den, + nm->mkNode( + PLUS, v, nm->mkConstInt(Rational(-1)))))))); } Node intVar = mkWitnessTerm( v, lem, "linearIntDiv", "the result of an intdiv-by-k term", lems); @@ -259,10 +255,9 @@ Node OperatorElim::eliminateOperators(Node node, checkNonLinearLogic(node); Node rw = nm->mkNode(k, num, den); Node v = bvm->mkBoundVar<ArithWitnessVarAttribute>(rw, nm->realType()); - Node lem = nm->mkNode( - IMPLIES, - den.eqNode(nm->mkConst(CONST_RATIONAL, Rational(0))).negate(), - nm->mkNode(MULT, den, v).eqNode(num)); + Node lem = nm->mkNode(IMPLIES, + den.eqNode(nm->mkConstReal(Rational(0))).negate(), + nm->mkNode(MULT, den, v).eqNode(num)); return mkWitnessTerm( v, lem, "nonlinearDiv", "the result of a non-linear div term", lems); break; @@ -276,8 +271,7 @@ Node OperatorElim::eliminateOperators(Node node, { checkNonLinearLogic(node); Node divByZeroNum = getArithSkolemApp(num, SkolemFunId::DIV_BY_ZERO); - Node denEq0 = - nm->mkNode(EQUAL, den, nm->mkConst(CONST_RATIONAL, Rational(0))); + Node denEq0 = nm->mkNode(EQUAL, den, nm->mkConstReal(Rational(0))); ret = nm->mkNode(ITE, denEq0, divByZeroNum, ret); } return ret; @@ -295,8 +289,7 @@ Node OperatorElim::eliminateOperators(Node node, checkNonLinearLogic(node); Node intDivByZeroNum = getArithSkolemApp(num, SkolemFunId::INT_DIV_BY_ZERO); - Node denEq0 = - nm->mkNode(EQUAL, den, nm->mkConst(CONST_RATIONAL, Rational(0))); + Node denEq0 = nm->mkNode(EQUAL, den, nm->mkConstInt(Rational(0))); ret = nm->mkNode(ITE, denEq0, intDivByZeroNum, ret); } return ret; @@ -313,8 +306,7 @@ Node OperatorElim::eliminateOperators(Node node, { checkNonLinearLogic(node); Node modZeroNum = getArithSkolemApp(num, SkolemFunId::MOD_BY_ZERO); - Node denEq0 = - nm->mkNode(EQUAL, den, nm->mkConst(CONST_RATIONAL, Rational(0))); + Node denEq0 = nm->mkNode(EQUAL, den, nm->mkConstInt(Rational(0))); ret = nm->mkNode(ITE, denEq0, modZeroNum, ret); } return ret; @@ -325,7 +317,9 @@ Node OperatorElim::eliminateOperators(Node node, { return nm->mkNode( ITE, - nm->mkNode(LT, node[0], nm->mkConst(CONST_RATIONAL, Rational(0))), + nm->mkNode(LT, + node[0], + nm->mkConstRealOrInt(node[0].getType(), Rational(0))), nm->mkNode(UMINUS, node[0]), node[0]); break; @@ -363,11 +357,10 @@ Node OperatorElim::eliminateOperators(Node node, // satisfiable. On the original formula, this would require that we // simultaneously interpret sqrt(1) as 1 and -1, which is not a valid // model. - lem = nm->mkNode( - ITE, - nm->mkNode(GEQ, node[0], nm->mkConst(CONST_RATIONAL, Rational(0))), - nonNeg, - uf); + lem = nm->mkNode(ITE, + nm->mkNode(GEQ, node[0], nm->mkConstReal(Rational(0))), + nonNeg, + uf); } else { @@ -377,10 +370,9 @@ Node OperatorElim::eliminateOperators(Node node, Node rlem; if (k == ARCSINE || k == ARCTANGENT || k == ARCCOSECANT) { - Node half = nm->mkConst(CONST_RATIONAL, Rational(1) / Rational(2)); + Node half = nm->mkConstReal(Rational(1) / Rational(2)); Node pi2 = nm->mkNode(MULT, half, pi); - Node npi2 = - nm->mkNode(MULT, nm->mkConst(CONST_RATIONAL, Rational(-1)), pi2); + Node npi2 = nm->mkNode(MULT, nm->mkConstReal(Rational(-1)), pi2); // -pi/2 < var <= pi/2 rlem = nm->mkNode( AND, nm->mkNode(LT, npi2, var), nm->mkNode(LEQ, var, pi2)); @@ -388,10 +380,9 @@ Node OperatorElim::eliminateOperators(Node node, else { // 0 <= var < pi - rlem = nm->mkNode( - AND, - nm->mkNode(LEQ, nm->mkConst(CONST_RATIONAL, Rational(0)), var), - nm->mkNode(LT, var, pi)); + rlem = nm->mkNode(AND, + nm->mkNode(LEQ, nm->mkConstReal(Rational(0)), var), + nm->mkNode(LT, var, pi)); } Kind rk = |