diff options
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); } |