void ExponentialSolver::doPurification(TNode a, TNode new_a)
{
+ Assert(TranscendentalState::isSimplePurify(a));
NodeManager* nm = NodeManager::currentNM();
// do both equalities to ensure that new_a becomes a preregistered term
Node lem = nm->mkNode(Kind::AND, a.eqNode(new_a), a[0].eqNode(new_a[0]));
// note we must do preprocess on this lemma
Trace("nl-ext-lemma") << "NonlinearExtension::Lemma : purify : " << lem
<< std::endl;
- d_data->d_im.addPendingLemma(lem, InferenceId::ARITH_NL_T_PURIFY_ARG);
+ CDProof* proof = nullptr;
+ if (d_data->isProofEnabled())
+ {
+ // simple to justify
+ proof = d_data->getProof();
+ proof->addStep(lem, PfRule::MACRO_SR_PRED_INTRO, {}, {lem});
+ }
+ d_data->d_im.addPendingLemma(lem, InferenceId::ARITH_NL_T_PURIFY_ARG, proof);
}
void ExponentialSolver::checkInitialRefine()
#include "expr/sequence.h"
#include "theory/arith/arith_utilities.h"
+#include "theory/arith/nl/transcendental/sine_solver.h"
#include "theory/arith/nl/transcendental/taylor_generator.h"
#include "theory/evaluator.h"
const auto& x = args[0];
const auto& y = args[1];
const auto& s = args[2];
- return nm->mkAnd(std::vector<Node>{
- nm->mkAnd(std::vector<Node>{
- nm->mkNode(Kind::GEQ, y, nm->mkNode(Kind::MULT, mone, pi)),
- nm->mkNode(Kind::LEQ, y, pi)}),
- nm->mkNode(
- Kind::ITE,
- nm->mkAnd(std::vector<Node>{
- nm->mkNode(Kind::GEQ, x, nm->mkNode(Kind::MULT, mone, pi)),
- nm->mkNode(Kind::LEQ, x, pi),
- }),
- x.eqNode(y),
- x.eqNode(nm->mkNode(
- Kind::ADD,
- y,
- nm->mkNode(Kind::MULT, nm->mkConstReal(2), s, pi)))),
- nm->mkNode(Kind::SINE, y).eqNode(nm->mkNode(Kind::SINE, x))});
+ return SineSolver::getPhaseShiftLemma(x, y, s);
}
else if (id == PfRule::ARITH_TRANS_SINE_SYMMETRY)
{
namespace arith {
namespace nl {
namespace transcendental {
-namespace {
-
-/**
- * Ensure a is in the main phase:
- * -pi <= a <= pi
- */
-inline Node mkValidPhase(TNode a, TNode pi)
-{
- NodeManager* nm = NodeManager::currentNM();
- return mkBounded(
- nm->mkNode(Kind::MULT, nm->mkConstReal(Rational(-1)), pi), a, pi);
-}
-} // namespace
SineSolver::SineSolver(Env& env, TranscendentalState* tstate)
: EnvObj(env), d_data(tstate)
}
}
+Node SineSolver::getPhaseShiftLemma(const Node& x, const Node& y, const Node& s)
+{
+ NodeManager* nm = NodeManager::currentNM();
+ Node mone = nm->mkConstReal(Rational(-1));
+ Node pi = nm->mkNullaryOperator(nm->realType(), PI);
+ return nm->mkAnd(std::vector<Node>{
+ nm->mkNode(GEQ, y, nm->mkNode(MULT, mone, pi)),
+ nm->mkNode(LEQ, y, pi),
+ nm->mkNode(IS_INTEGER, s),
+ nm->mkNode(ITE,
+ nm->mkAnd(std::vector<Node>{
+ nm->mkNode(GEQ, x, nm->mkNode(MULT, mone, pi)),
+ nm->mkNode(LEQ, x, pi),
+ }),
+ x.eqNode(y),
+ x.eqNode(nm->mkNode(
+ ADD, y, nm->mkNode(MULT, nm->mkConstReal(2), s, pi)))),
+ nm->mkNode(SINE, y).eqNode(nm->mkNode(SINE, x))});
+}
+
void SineSolver::doPhaseShift(TNode a, TNode new_a)
{
- TNode y = new_a[0];
NodeManager* nm = NodeManager::currentNM();
SkolemManager* sm = nm->getSkolemManager();
Assert(a.getKind() == Kind::SINE);
- Trace("nl-ext-tf") << "Basis sine : " << new_a << " for " << a << std::endl;
- Node shift = sm->mkDummySkolem("s", nm->integerType(), "number of shifts");
- // TODO (cvc4-projects #47) : do not introduce shift here, instead needs model-based
- // refinement for constant shifts (cvc4-projects #1284)
- Node lem = nm->mkNode(
- Kind::AND,
- mkValidPhase(y, d_pi),
- nm->mkNode(
- Kind::ITE,
- mkValidPhase(a[0], d_pi),
- a[0].eqNode(y),
- a[0].eqNode(nm->mkNode(
- Kind::ADD,
- y,
- nm->mkNode(
- Kind::MULT, nm->mkConstReal(Rational(2)), shift, d_pi)))),
- new_a.eqNode(a));
CDProof* proof = nullptr;
- if (d_data->isProofEnabled())
+ Node lem;
+ Trace("nl-ext-tf") << "Basis sine : " << new_a << " for " << a << std::endl;
+ InferenceId iid;
+ if (TranscendentalState::isSimplePurify(a))
{
- proof = d_data->getProof();
- proof->addStep(lem, PfRule::ARITH_TRANS_SINE_SHIFT, {}, {a[0], y, shift});
+ lem = nm->mkNode(Kind::AND, a.eqNode(new_a), a[0].eqNode(new_a[0]));
+ if (d_data->isProofEnabled())
+ {
+ // simple to justify
+ proof = d_data->getProof();
+ proof->addStep(lem, PfRule::MACRO_SR_PRED_INTRO, {}, {lem});
+ }
+ iid = InferenceId::ARITH_NL_T_PURIFY_ARG;
+ }
+ else
+ {
+ Node shift = sm->mkDummySkolem("s", nm->realType(), "number of shifts");
+ // TODO (cvc4-projects #47) : do not introduce shift here, instead needs
+ // model-based refinement for constant shifts (cvc4-projects #1284)
+ lem = getPhaseShiftLemma(a[0], new_a[0], shift);
+ if (d_data->isProofEnabled())
+ {
+ proof = d_data->getProof();
+ proof->addStep(
+ lem, PfRule::ARITH_TRANS_SINE_SHIFT, {}, {a[0], new_a[0], shift});
+ }
+ iid = InferenceId::ARITH_NL_T_PURIFY_ARG_PHASE_SHIFT;
}
// note we must do preprocess on this lemma
Trace("nl-ext-lemma") << "NonlinearExtension::Lemma : purify : " << lem
<< std::endl;
- d_data->d_im.addPendingLemma(lem, InferenceId::ARITH_NL_T_PURIFY_ARG, proof);
+ d_data->d_im.addPendingLemma(lem, iid, proof);
}
void SineSolver::checkInitialRefine()
*/
bool hasExactModelValue(TNode n) const;
+ /**
+ * Make the lemma for the phase shift of arguments to SINE x and y, where
+ * s is the (integral) shift. The lemma conceptually says that y is
+ * in the bounds [-pi, pi] and y is offset from x by an integral factor of
+ * 2*pi.
+ */
+ static Node getPhaseShiftLemma(const Node& x, const Node& y, const Node& s);
+
private:
std::pair<Node, Node> getSecantBounds(TNode e,
TNode c,
{
d_pi = nm->mkNullaryOperator(nm->realType(), Kind::PI);
// initialize bounds
- d_pi_bound[0] = nm->mkConstReal(Rational(103993) / Rational(33102));
- d_pi_bound[1] = nm->mkConstReal(Rational(104348) / Rational(33215));
+ d_pi_bound[0] = nm->mkConstReal(getPiInitialLowerBound());
+ d_pi_bound[1] = nm->mkConstReal(getPiInitialUpperBound());
}
}
}
Kind k = n.getKind();
Assert(k == Kind::SINE || k == Kind::EXPONENTIAL);
- Node y = sm->mkSkolemFunction(
- SkolemFunId::TRANSCENDENTAL_PURIFY_ARG, nm->realType(), n);
+ Node y;
+ if (isSimplePurify(n))
+ {
+ y = sm->mkPurifySkolem(n[0], "transk");
+ }
+ else
+ {
+ y = sm->mkSkolemFunction(
+ SkolemFunId::TRANSCENDENTAL_PURIFY_ARG, nm->realType(), n);
+ }
Node new_n = nm->mkNode(k, y);
d_trPurify[n] = new_n;
d_trPurify[new_n] = new_n;
return new_n;
}
+bool TranscendentalState::isSimplePurify(TNode n)
+{
+ if (n.getKind() != kind::SINE)
+ {
+ return true;
+ }
+ if (!n[0].isConst())
+ {
+ return false;
+ }
+ Rational r = n[0].getConst<Rational>();
+ // use a fixed value of pi
+ Rational piLower = getPiInitialLowerBound();
+ return -piLower <= r && r <= piLower;
+}
+
bool TranscendentalState::addModelBoundForPurifyTerm(TNode n, TNode l, TNode u)
{
Assert(d_funcCongClass.find(n) != d_funcCongClass.end());
return true;
}
+Rational TranscendentalState::getPiInitialLowerBound()
+{
+ return Rational(103993) / Rational(33102);
+}
+
+Rational TranscendentalState::getPiInitialUpperBound()
+{
+ return Rational(104348) / Rational(33215);
+}
+
} // namespace transcendental
} // namespace nl
} // namespace arith
bool isPurified(TNode n) const;
/** get the purified form of node n */
Node getPurifiedForm(TNode n);
+ /**
+ * Can we do "simple" purification for n? If this is the case, then
+ * f(x) is purified by f(k) where k is the purification variable for x.
+ *
+ * This is true for sin(x) where x is guaranteed to be a constant in the
+ * bound [-pi, pi] (note that there may be some x in [-pi, pi] for which
+ * this function returns false, because the check is not precise).
+ */
+ static bool isSimplePurify(TNode n);
/**
* Add bound for n, and for what (if anything) it purifies
*/
bool addModelBoundForPurifyTerm(TNode n, TNode l, TNode u);
+ /** initial lower and upper bounds for PI */
+ static Rational getPiInitialLowerBound();
+ static Rational getPiInitialUpperBound();
Node d_true;
Node d_false;
case InferenceId::ARITH_NL_T_SINE_BOUNDARY_REDUCE:
return "ARITH_NL_T_SINE_BOUNDARY_REDUCE";
case InferenceId::ARITH_NL_T_PURIFY_ARG: return "ARITH_NL_T_PURIFY_ARG";
+ case InferenceId::ARITH_NL_T_PURIFY_ARG_PHASE_SHIFT:
+ return "ARITH_NL_T_PURIFY_ARG_PHASE_SHIFT";
case InferenceId::ARITH_NL_T_INIT_REFINE: return "ARITH_NL_T_INIT_REFINE";
case InferenceId::ARITH_NL_T_PI_BOUND: return "ARITH_NL_T_PI_BOUND";
case InferenceId::ARITH_NL_T_MONOTONICITY: return "ARITH_NL_T_MONOTONICITY";
ARITH_NL_T_SINE_BOUNDARY_REDUCE,
// purification of arguments to transcendental functions
ARITH_NL_T_PURIFY_ARG,
+ // purification of arguments to transcendental functions with phase shifting
+ ARITH_NL_T_PURIFY_ARG_PHASE_SHIFT,
// initial refinement (TranscendentalSolver::checkTranscendentalInitialRefine)
ARITH_NL_T_INIT_REFINE,
// pi bounds
projects / cvc5.git / commitdiff