diff options
Diffstat (limited to 'src/theory/arith/operator_elim.cpp')
| -rw-r--r-- | src/theory/arith/operator_elim.cpp | 92 |
1 files changed, 54 insertions, 38 deletions
diff --git a/src/theory/arith/operator_elim.cpp b/src/theory/arith/operator_elim.cpp index 5c43189ea..17efa53a5 100644 --- a/src/theory/arith/operator_elim.cpp +++ b/src/theory/arith/operator_elim.cpp @@ -170,21 +170,25 @@ Node OperatorElim::eliminateOperators(Node node, nm->mkNode( LT, num, - nm->mkNode(MULT, - den, - nm->mkNode(PLUS, v, nm->mkConst(Rational(1)))))); + nm->mkNode( + MULT, + den, + nm->mkNode( + PLUS, v, nm->mkConst(CONST_RATIONAL, Rational(1)))))); } else { lem = nm->mkNode( AND, leqNum, - nm->mkNode( - LT, - num, - nm->mkNode(MULT, - den, - nm->mkNode(PLUS, v, nm->mkConst(Rational(-1)))))); + nm->mkNode(LT, + num, + nm->mkNode(MULT, + den, + nm->mkNode(PLUS, + v, + nm->mkConst(CONST_RATIONAL, + Rational(-1)))))); } } else @@ -194,30 +198,34 @@ Node OperatorElim::eliminateOperators(Node node, AND, nm->mkNode( IMPLIES, - nm->mkNode(GT, den, nm->mkConst(Rational(0))), + nm->mkNode(GT, den, nm->mkConst(CONST_RATIONAL, Rational(0))), nm->mkNode( AND, leqNum, nm->mkNode( LT, num, - nm->mkNode( - MULT, - den, - nm->mkNode(PLUS, v, nm->mkConst(Rational(1))))))), + nm->mkNode(MULT, + den, + nm->mkNode(PLUS, + v, + nm->mkConst(CONST_RATIONAL, + Rational(1))))))), nm->mkNode( IMPLIES, - nm->mkNode(LT, den, nm->mkConst(Rational(0))), + nm->mkNode(LT, den, nm->mkConst(CONST_RATIONAL, Rational(0))), nm->mkNode( AND, leqNum, nm->mkNode( LT, num, - nm->mkNode( - MULT, - den, - nm->mkNode(PLUS, v, nm->mkConst(Rational(-1)))))))); + nm->mkNode(MULT, + den, + nm->mkNode(PLUS, + v, + nm->mkConst(CONST_RATIONAL, + Rational(-1)))))))); } Node intVar = mkWitnessTerm( v, lem, "linearIntDiv", "the result of an intdiv-by-k term", lems); @@ -251,9 +259,10 @@ 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(Rational(0))).negate(), - nm->mkNode(MULT, den, v).eqNode(num)); + Node lem = nm->mkNode( + IMPLIES, + den.eqNode(nm->mkConst(CONST_RATIONAL, 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; @@ -267,7 +276,8 @@ Node OperatorElim::eliminateOperators(Node node, { checkNonLinearLogic(node); Node divByZeroNum = getArithSkolemApp(num, SkolemFunId::DIV_BY_ZERO); - Node denEq0 = nm->mkNode(EQUAL, den, nm->mkConst(Rational(0))); + Node denEq0 = + nm->mkNode(EQUAL, den, nm->mkConst(CONST_RATIONAL, Rational(0))); ret = nm->mkNode(ITE, denEq0, divByZeroNum, ret); } return ret; @@ -285,7 +295,8 @@ Node OperatorElim::eliminateOperators(Node node, checkNonLinearLogic(node); Node intDivByZeroNum = getArithSkolemApp(num, SkolemFunId::INT_DIV_BY_ZERO); - Node denEq0 = nm->mkNode(EQUAL, den, nm->mkConst(Rational(0))); + Node denEq0 = + nm->mkNode(EQUAL, den, nm->mkConst(CONST_RATIONAL, Rational(0))); ret = nm->mkNode(ITE, denEq0, intDivByZeroNum, ret); } return ret; @@ -302,7 +313,8 @@ Node OperatorElim::eliminateOperators(Node node, { checkNonLinearLogic(node); Node modZeroNum = getArithSkolemApp(num, SkolemFunId::MOD_BY_ZERO); - Node denEq0 = nm->mkNode(EQUAL, den, nm->mkConst(Rational(0))); + Node denEq0 = + nm->mkNode(EQUAL, den, nm->mkConst(CONST_RATIONAL, Rational(0))); ret = nm->mkNode(ITE, denEq0, modZeroNum, ret); } return ret; @@ -311,10 +323,11 @@ Node OperatorElim::eliminateOperators(Node node, case ABS: { - return nm->mkNode(ITE, - nm->mkNode(LT, node[0], nm->mkConst(Rational(0))), - nm->mkNode(UMINUS, node[0]), - node[0]); + return nm->mkNode( + ITE, + nm->mkNode(LT, node[0], nm->mkConst(CONST_RATIONAL, Rational(0))), + nm->mkNode(UMINUS, node[0]), + node[0]); break; } case SQRT: @@ -350,10 +363,11 @@ 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(Rational(0))), - nonNeg, - uf); + lem = nm->mkNode( + ITE, + nm->mkNode(GEQ, node[0], nm->mkConst(CONST_RATIONAL, Rational(0))), + nonNeg, + uf); } else { @@ -363,9 +377,10 @@ Node OperatorElim::eliminateOperators(Node node, Node rlem; if (k == ARCSINE || k == ARCTANGENT || k == ARCCOSECANT) { - Node half = nm->mkConst(Rational(1) / Rational(2)); + Node half = nm->mkConst(CONST_RATIONAL, Rational(1) / Rational(2)); Node pi2 = nm->mkNode(MULT, half, pi); - Node npi2 = nm->mkNode(MULT, nm->mkConst(Rational(-1)), pi2); + Node npi2 = + nm->mkNode(MULT, nm->mkConst(CONST_RATIONAL, Rational(-1)), pi2); // -pi/2 < var <= pi/2 rlem = nm->mkNode( AND, nm->mkNode(LT, npi2, var), nm->mkNode(LEQ, var, pi2)); @@ -373,9 +388,10 @@ Node OperatorElim::eliminateOperators(Node node, else { // 0 <= var < pi - rlem = nm->mkNode(AND, - nm->mkNode(LEQ, nm->mkConst(Rational(0)), var), - nm->mkNode(LT, var, pi)); + rlem = nm->mkNode( + AND, + nm->mkNode(LEQ, nm->mkConst(CONST_RATIONAL, Rational(0)), var), + nm->mkNode(LT, var, pi)); } Kind rk = |