diff options
author | Alex Ozdemir <aozdemir@hmc.edu> | 2020-02-10 13:53:54 -0800 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-02-10 13:53:54 -0800 |
commit | 499f1c70dbc869e2b1dd5f8a7b98d45bee2d29cc (patch) | |
tree | 7693c792269cafb3267897346ad52b18c7cc16a7 /src/proof | |
parent | 779f9cd3c0f9a3620a52c30a853bde9e7b911494 (diff) |
Add function for tightening literals (#3732)
* Add function for tightening literals
The function tightens a literal if it can be tightened, and prints a
proof of the result.
* Include a #include
Co-authored-by: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Diffstat (limited to 'src/proof')
-rw-r--r-- | src/proof/arith_proof.cpp | 75 | ||||
-rw-r--r-- | src/proof/arith_proof.h | 13 |
2 files changed, 88 insertions, 0 deletions
diff --git a/src/proof/arith_proof.cpp b/src/proof/arith_proof.cpp index 3ff0ff539..f1d7c0e43 100644 --- a/src/proof/arith_proof.cpp +++ b/src/proof/arith_proof.cpp @@ -23,6 +23,7 @@ #include "proof/proof_manager.h" #include "proof/theory_proof.h" #include "theory/arith/constraint_forward.h" +#include "theory/arith/normal_form.h" #include "theory/arith/theory_arith.h" #define CVC4_ARITH_VAR_TERM_PREFIX "term." @@ -1055,6 +1056,80 @@ void LFSCArithProof::printLinearPolynomialPredicateNormalizer(std::ostream& o, o << ")))"; } +std::pair<Node, std::string> LFSCArithProof::printProofAndMaybeTighten( + const Node& bound) +{ + const Node & nonNegBound = bound.getKind() == kind::NOT ? bound[0] : bound; + std::ostringstream pfOfPossiblyTightenedPredicate; + if (nonNegBound[0].getType().isInteger()) { + switch(bound.getKind()) + { + case kind::NOT: + { + // Tighten ~[i >= r] to [i < r] to [i <= {r}] to [-i >= -{r}] + // where + // * i is an integer + // * r is a real + // * {r} denotes the greatest int less than r + // it is equivalent to (ceil(r) - 1) + Assert(nonNegBound[1].getKind() == kind::CONST_RATIONAL); + Rational oldBound = nonNegBound[1].getConst<Rational>(); + Integer newBound = -(oldBound.ceiling() - 1); + pfOfPossiblyTightenedPredicate + << "(" + << (oldBound.isIntegral() ? "tighten_not_>=_IntInt" + : "tighten_not_>=_IntReal") + << " _ _ _ _ (" + << (oldBound.isIntegral() + ? "check_neg_of_greatest_integer_below_int " + : "check_neg_of_greatest_integer_below "); + printInteger(pfOfPossiblyTightenedPredicate, newBound); + pfOfPossiblyTightenedPredicate << " "; + if (oldBound.isIntegral()) + { + printInteger(pfOfPossiblyTightenedPredicate, oldBound.ceiling()); + } + else + { + printRational(pfOfPossiblyTightenedPredicate, oldBound); + } + pfOfPossiblyTightenedPredicate << ") " << ProofManager::getLitName(bound.negate(), "") << ")"; + Node newLeft = (theory::arith::Polynomial::parsePolynomial(nonNegBound[0]) * -1).getNode(); + Node newRight = NodeManager::currentNM()->mkConst(Rational(newBound)); + Node newTerm = NodeManager::currentNM()->mkNode(kind::GEQ, newLeft, newRight); + return std::make_pair(newTerm, pfOfPossiblyTightenedPredicate.str()); + } + case kind::GEQ: + { + // Tighten [i >= r] to [i >= ceil(r)] + // where + // * i is an integer + // * r is a real + Assert(nonNegBound[1].getKind() == kind::CONST_RATIONAL); + + Rational oldBound = nonNegBound[1].getConst<Rational>(); + if (oldBound.isIntegral()) { + pfOfPossiblyTightenedPredicate << ProofManager::getLitName(bound.negate(), ""); + return std::make_pair(bound, pfOfPossiblyTightenedPredicate.str()); + } else { + Integer newBound = oldBound.ceiling(); + pfOfPossiblyTightenedPredicate << "(tighten_>=_IntReal _ _ " << + newBound << " " << ProofManager::getLitName(bound.negate(), "") << ")"; + Node newRight = NodeManager::currentNM()->mkConst(Rational(newBound)); + Node newTerm = NodeManager::currentNM()->mkNode(kind::GEQ, nonNegBound[0], newRight); + return std::make_pair(newTerm, pfOfPossiblyTightenedPredicate.str()); + } + break; + } + default: Unreachable(); + } + } else { + return std::make_pair(bound, ProofManager::getLitName(bound.negate(), "")); + } + // Silence compiler warnings about missing a return. + Unreachable(); +} + void LFSCArithProof::printTheoryLemmaProof(std::vector<Expr>& lemma, std::ostream& os, std::ostream& paren, diff --git a/src/proof/arith_proof.h b/src/proof/arith_proof.h index 5522b4eb4..44e99cb76 100644 --- a/src/proof/arith_proof.h +++ b/src/proof/arith_proof.h @@ -192,6 +192,19 @@ public: const ProofLetMap& globalLetMap) override; /** + * Given a node that is an arith literal (an arith comparison or negation + * thereof), prints a proof of that literal. + * + * If the node represents a tightenable bound (e.g. [Int] < 3) then it prints + * a proof of the tightening instead. (e.g. [Int] <= 2). + * + * @return a pair comprising: + * * the new node (after tightening) and + * * a string proving it. + */ + std::pair<Node, std::string> printProofAndMaybeTighten(const Node& bound); + + /** * Return whether this node, when serialized to LFSC, has sort `Bool`. Otherwise, the sort is `formula`. */ bool printsAsBool(const Node& n) override; |