diff options
author | Gereon Kremer <gereon.kremer@cs.rwth-aachen.de> | 2020-12-21 18:16:53 +0100 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-12-21 11:16:53 -0600 |
commit | 0c2a43ab616c3670f3077758defcaa1f61cbe291 (patch) | |
tree | 83cf86aa5cdd2ea0af07a980ebca0cd4af072f83 /src | |
parent | 708c5a14bca031100b05000ddae65a9828d76da0 (diff) |
Add proof for sine shift lemmas. (#5710)
This PR adds proofs for the sine shift lemmas that add equivalent instances of the sine function where the argument is in its "main phase" between minus pi and pi.
Diffstat (limited to 'src')
-rw-r--r-- | src/expr/proof_rule.cpp | 1 | ||||
-rw-r--r-- | src/expr/proof_rule.h | 14 | ||||
-rw-r--r-- | src/theory/arith/nl/transcendental/proof_checker.cpp | 25 | ||||
-rw-r--r-- | src/theory/arith/nl/transcendental/sine_solver.cpp | 8 |
4 files changed, 47 insertions, 1 deletions
diff --git a/src/expr/proof_rule.cpp b/src/expr/proof_rule.cpp index 22459edd4..24cfa0091 100644 --- a/src/expr/proof_rule.cpp +++ b/src/expr/proof_rule.cpp @@ -160,6 +160,7 @@ const char* toString(PfRule id) case PfRule::INT_TRUST: return "INT_TRUST"; case PfRule::ARITH_MULT_TANGENT: return "ARITH_MULT_TANGENT"; case PfRule::ARITH_OP_ELIM_AXIOM: return "ARITH_OP_ELIM_AXIOM"; + case PfRule::ARITH_TRANS_SINE_SHIFT: return "ARITH_TRANS_SINE_SHIFT"; //================================================= Unknown rule case PfRule::UNKNOWN: return "UNKNOWN"; default: return "?"; diff --git a/src/expr/proof_rule.h b/src/expr/proof_rule.h index b5899af66..e92e09a9b 100644 --- a/src/expr/proof_rule.h +++ b/src/expr/proof_rule.h @@ -1104,6 +1104,20 @@ enum class PfRule : uint32_t // or 1. tplane is the tangent plane of x*y at (a,b): b*x + a*y - a*b ARITH_MULT_TANGENT, + //======== Sine arg shifted to -pi..pi + // Children: none + // Arguments: (x, y, s) + // --------------------- + // Conclusion: (and + // (<= -pi y pi) + // (= (sin y) (sin x)) + // (ite (<= -pi x pi) (= x y) (= x (+ y (* 2 pi s)))) + // ) + // Where x is the argument to sine, y is a new real skolem that is x shifted + // into -pi..pi and s is a new integer skolem that is the number of phases y + // is shifted. + ARITH_TRANS_SINE_SHIFT, + //================================================= Unknown rule UNKNOWN, }; diff --git a/src/theory/arith/nl/transcendental/proof_checker.cpp b/src/theory/arith/nl/transcendental/proof_checker.cpp index d407621e9..c4f06a136 100644 --- a/src/theory/arith/nl/transcendental/proof_checker.cpp +++ b/src/theory/arith/nl/transcendental/proof_checker.cpp @@ -29,6 +29,7 @@ namespace transcendental { void TranscendentalProofRuleChecker::registerTo(ProofChecker* pc) { + pc->registerChecker(PfRule::ARITH_TRANS_SINE_SHIFT, this); } Node TranscendentalProofRuleChecker::checkInternal( @@ -45,6 +46,30 @@ Node TranscendentalProofRuleChecker::checkInternal( { Trace("nl-trans-checker") << "\t" << c << std::endl; } + if (id == PfRule::ARITH_TRANS_SINE_SHIFT) + { + Assert(children.empty()); + Assert(args.size() == 3); + 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::PLUS, + y, + nm->mkNode(Kind::MULT, nm->mkConst<Rational>(2), s, pi)))), + nm->mkNode(Kind::SINE, y).eqNode(nm->mkNode(Kind::SINE, x))}); + } return Node::null(); } diff --git a/src/theory/arith/nl/transcendental/sine_solver.cpp b/src/theory/arith/nl/transcendental/sine_solver.cpp index 1747077bd..40137095c 100644 --- a/src/theory/arith/nl/transcendental/sine_solver.cpp +++ b/src/theory/arith/nl/transcendental/sine_solver.cpp @@ -70,11 +70,17 @@ void SineSolver::doPhaseShift(TNode a, TNode new_a, TNode y) shift, d_data->d_pi)))), new_a.eqNode(a)); + CDProof* proof = nullptr; + if (d_data->isProofEnabled()) + { + proof = d_data->getProof(); + proof->addStep(lem, PfRule::ARITH_TRANS_SINE_SHIFT, {}, {a[0], y, shift}); + } // note we must do preprocess on this lemma Trace("nl-ext-lemma") << "NonlinearExtension::Lemma : purify : " << lem << std::endl; NlLemma nlem( - lem, LemmaProperty::PREPROCESS, nullptr, InferenceId::NL_T_PURIFY_ARG); + lem, LemmaProperty::PREPROCESS, proof, InferenceId::NL_T_PURIFY_ARG); d_data->d_im.addPendingArithLemma(nlem); } |