diff options
Diffstat (limited to 'src/theory/arith/nl/transcendental/sine_solver.cpp')
| -rw-r--r-- | src/theory/arith/nl/transcendental/sine_solver.cpp | 23 |
1 files changed, 13 insertions, 10 deletions
diff --git a/src/theory/arith/nl/transcendental/sine_solver.cpp b/src/theory/arith/nl/transcendental/sine_solver.cpp index ed37ee91c..b6b5c92c1 100644 --- a/src/theory/arith/nl/transcendental/sine_solver.cpp +++ b/src/theory/arith/nl/transcendental/sine_solver.cpp @@ -30,6 +30,8 @@ #include "theory/arith/nl/transcendental/transcendental_state.h" #include "theory/rewriter.h" +using namespace cvc5::kind; + namespace cvc5 { namespace theory { namespace arith { @@ -73,12 +75,13 @@ void SineSolver::doPhaseShift(TNode a, TNode new_a, TNode y) nm->mkNode(Kind::ITE, mkValidPhase(a[0], d_data->d_pi), a[0].eqNode(y), - a[0].eqNode(nm->mkNode(Kind::PLUS, - y, - nm->mkNode(Kind::MULT, - nm->mkConst(Rational(2)), - shift, - d_data->d_pi)))), + a[0].eqNode(nm->mkNode( + Kind::PLUS, + y, + nm->mkNode(Kind::MULT, + nm->mkConst(CONST_RATIONAL, Rational(2)), + shift, + d_data->d_pi)))), new_a.eqNode(a)); CDProof* proof = nullptr; if (d_data->isProofEnabled()) @@ -399,7 +402,7 @@ void SineSolver::doTangentLemma( proof->addStep(lem, PfRule::ARITH_TRANS_SINE_APPROX_BELOW_NEG, {}, - {nm->mkConst<Rational>(2 * d), + {nm->mkConst(CONST_RATIONAL, Rational(2 * d)), e[0], c, regionToLowerBound(region), @@ -410,7 +413,7 @@ void SineSolver::doTangentLemma( proof->addStep(lem, PfRule::ARITH_TRANS_SINE_APPROX_BELOW_NEG, {}, - {nm->mkConst<Rational>(2 * d), + {nm->mkConst(CONST_RATIONAL, Rational(2 * d)), e[0], c, c, @@ -424,7 +427,7 @@ void SineSolver::doTangentLemma( proof->addStep(lem, PfRule::ARITH_TRANS_SINE_APPROX_ABOVE_POS, {}, - {nm->mkConst<Rational>(2 * d), + {nm->mkConst(CONST_RATIONAL, Rational(2 * d)), e[0], c, regionToLowerBound(region), @@ -435,7 +438,7 @@ void SineSolver::doTangentLemma( proof->addStep(lem, PfRule::ARITH_TRANS_SINE_APPROX_ABOVE_POS, {}, - {nm->mkConst<Rational>(2 * d), + {nm->mkConst(CONST_RATIONAL, Rational(2 * d)), e[0], c, c, |