From 228d35b578404b4931c6b4b9c9a0a199a0a9236e Mon Sep 17 00:00:00 2001 From: yoni206 Date: Wed, 23 Jun 2021 15:16:58 -0700 Subject: pow2: more implementations (#6756) This PR adds implementations of functions from the pow2 solver, rewriter and type checker. --- src/theory/arith/arith_rewriter.cpp | 19 +++++++ src/theory/arith/arith_rewriter.h | 1 + src/theory/arith/nl/pow2_solver.cpp | 76 ++++++++++++++++++++++++++-- src/theory/arith/theory_arith_type_rules.cpp | 19 +++++++ src/theory/arith/theory_arith_type_rules.h | 6 +++ 5 files changed, 118 insertions(+), 3 deletions(-) diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp index 4d632e043..b0453fad4 100644 --- a/src/theory/arith/arith_rewriter.cpp +++ b/src/theory/arith/arith_rewriter.cpp @@ -112,6 +112,7 @@ RewriteResponse ArithRewriter::preRewriteTerm(TNode t){ case kind::MULT: case kind::NONLINEAR_MULT: return preRewriteMult(t); case kind::IAND: return RewriteResponse(REWRITE_DONE, t); + case kind::POW2: return RewriteResponse(REWRITE_DONE, t); case kind::EXPONENTIAL: case kind::SINE: case kind::COSINE: @@ -175,6 +176,7 @@ RewriteResponse ArithRewriter::postRewriteTerm(TNode t){ case kind::MULT: case kind::NONLINEAR_MULT: return postRewriteMult(t); case kind::IAND: return postRewriteIAnd(t); + case kind::POW2: return postRewritePow2(t); case kind::EXPONENTIAL: case kind::SINE: case kind::COSINE: @@ -381,6 +383,23 @@ RewriteResponse ArithRewriter::postRewriteMult(TNode t){ return RewriteResponse(REWRITE_DONE, res.getNode()); } +RewriteResponse ArithRewriter::postRewritePow2(TNode t) +{ + Assert(t.getKind() == kind::POW2); + NodeManager* nm = NodeManager::currentNM(); + // if constant, we eliminate + if (t[0].isConst()) + { + // pow2 is only supported for integers + Assert(t[0].getType().isInteger()); + Integer i = t[0].getConst().getNumerator(); + unsigned long k = i.getUnsignedLong(); + Node ret = nm->mkConst(Rational(Integer(2).pow(k), Integer(1))); + return RewriteResponse(REWRITE_DONE, ret); + } + return RewriteResponse(REWRITE_DONE, t); +} + RewriteResponse ArithRewriter::postRewriteIAnd(TNode t) { Assert(t.getKind() == kind::IAND); diff --git a/src/theory/arith/arith_rewriter.h b/src/theory/arith/arith_rewriter.h index 6a92ba1cc..813f2b1bb 100644 --- a/src/theory/arith/arith_rewriter.h +++ b/src/theory/arith/arith_rewriter.h @@ -64,6 +64,7 @@ class ArithRewriter : public TheoryRewriter static RewriteResponse postRewriteMult(TNode t); static RewriteResponse postRewriteIAnd(TNode t); + static RewriteResponse postRewritePow2(TNode t); static RewriteResponse preRewriteTranscendental(TNode t); static RewriteResponse postRewriteTranscendental(TNode t); diff --git a/src/theory/arith/nl/pow2_solver.cpp b/src/theory/arith/nl/pow2_solver.cpp index 534895c7f..9864fc709 100644 --- a/src/theory/arith/nl/pow2_solver.cpp +++ b/src/theory/arith/nl/pow2_solver.cpp @@ -61,11 +61,81 @@ void Pow2Solver::initLastCall(const std::vector& assertions, Trace("pow2") << "We have " << d_pow2s.size() << " pow2 terms." << std::endl; } -void Pow2Solver::checkInitialRefine() {} +void Pow2Solver::checkInitialRefine() +{ + Trace("pow2-check") << "Pow2Solver::checkInitialRefine" << std::endl; + NodeManager* nm = NodeManager::currentNM(); + for (const Node& i : d_pow2s) + { + if (d_initRefine.find(i) != d_initRefine.end()) + { + // already sent initial axioms for i in this user context + continue; + } + d_initRefine.insert(i); + // initial refinement lemmas + std::vector conj; + // x>=0 -> x < pow2(x) + Node xgeq0 = nm->mkNode(LEQ, d_zero, i[0]); + Node xltpow2x = nm->mkNode(LT, i[0], i); + conj.push_back(nm->mkNode(IMPLIES, xgeq0, xltpow2x)); + Node lem = nm->mkAnd(conj); + Trace("pow2-lemma") << "Pow2Solver::Lemma: " << lem << " ; INIT_REFINE" + << std::endl; + d_im.addPendingLemma(lem, InferenceId::ARITH_NL_POW2_INIT_REFINE); + } +} -void Pow2Solver::checkFullRefine() {} +void Pow2Solver::checkFullRefine() +{ + Trace("pow2-check") << "Pow2Solver::checkFullRefine"; + Trace("pow2-check") << "pow2 terms: " << std::endl; + for (const Node& i : d_pow2s) + { + Node valPow2x = d_model.computeAbstractModelValue(i); + Node valPow2xC = d_model.computeConcreteModelValue(i); + if (Trace.isOn("pow2-check")) + { + Node x = i[0]; + Node valX = d_model.computeConcreteModelValue(x); -Node Pow2Solver::valueBasedLemma(Node i) { return Node(); } + Trace("pow2-check") << "* " << i << ", value = " << valPow2x << std::endl; + Trace("pow2-check") << " actual (" << valX << ", " + << ") = " << valPow2xC << std::endl; + } + if (valPow2x == valPow2xC) + { + Trace("pow2-check") << "...already correct" << std::endl; + continue; + } + + // Place holder for additional lemma schemas + // + // End of additional lemma schemas + + // this is the most naive model-based schema based on model values + Node lem = valueBasedLemma(i); + Trace("pow2-lemma") << "Pow2Solver::Lemma: " << lem << " ; VALUE_REFINE" + << std::endl; + // send the value lemma + d_im.addPendingLemma( + lem, InferenceId::ARITH_NL_POW2_VALUE_REFINE, nullptr, true); + } +} +Node Pow2Solver::valueBasedLemma(Node i) +{ + Assert(i.getKind() == POW2); + Node x = i[0]; + + Node valX = d_model.computeConcreteModelValue(x); + + NodeManager* nm = NodeManager::currentNM(); + Node valC = nm->mkNode(POW2, valX); + valC = Rewriter::rewrite(valC); + + Node lem = nm->mkNode(IMPLIES, x.eqNode(valX), i.eqNode(valC)); + return lem; +} } // namespace nl } // namespace arith diff --git a/src/theory/arith/theory_arith_type_rules.cpp b/src/theory/arith/theory_arith_type_rules.cpp index 1ba501f90..c9309a3d4 100644 --- a/src/theory/arith/theory_arith_type_rules.cpp +++ b/src/theory/arith/theory_arith_type_rules.cpp @@ -133,6 +133,25 @@ TypeNode IAndTypeRule::computeType(NodeManager* nodeManager, return nodeManager->integerType(); } +TypeNode Pow2TypeRule::computeType(NodeManager* nodeManager, + TNode n, + bool check) +{ + if (n.getKind() != kind::POW2) + { + InternalError() << "POW2 typerule invoked for POW2 kind"; + } + if (check) + { + TypeNode arg1 = n[0].getType(check); + if (!arg1.isInteger()) + { + throw TypeCheckingExceptionPrivate(n, "expecting integer terms"); + } + } + return nodeManager->integerType(); +} + TypeNode IndexedRootPredicateTypeRule::computeType(NodeManager* nodeManager, TNode n, bool check) diff --git a/src/theory/arith/theory_arith_type_rules.h b/src/theory/arith/theory_arith_type_rules.h index f7ef64e2d..7bb623ad2 100644 --- a/src/theory/arith/theory_arith_type_rules.h +++ b/src/theory/arith/theory_arith_type_rules.h @@ -55,6 +55,12 @@ class IAndTypeRule static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); }; +class Pow2TypeRule +{ + public: + static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); +}; + class IndexedRootPredicateTypeRule { public: -- cgit v1.2.3