diff options
| -rw-r--r-- | src/theory/arith/arith_state.cpp | 9 | ||||
| -rw-r--r-- | src/theory/arith/arith_state.h | 9 | ||||
| -rw-r--r-- | src/theory/arith/theory_arith.cpp | 70 | ||||
| -rw-r--r-- | src/theory/arith/theory_arith.h | 25 | ||||
| -rw-r--r-- | src/theory/arith/theory_arith_private.cpp | 100 | ||||
| -rw-r--r-- | src/theory/arith/theory_arith_private.h | 8 |
6 files changed, 67 insertions, 154 deletions
diff --git a/src/theory/arith/arith_state.cpp b/src/theory/arith/arith_state.cpp index 4af7b8b8d..93d410bf8 100644 --- a/src/theory/arith/arith_state.cpp +++ b/src/theory/arith/arith_state.cpp @@ -21,19 +21,20 @@ namespace cvc5 { namespace theory { namespace arith { -ArithState::ArithState(TheoryArithPrivate& parent, - context::Context* c, +ArithState::ArithState(context::Context* c, context::UserContext* u, Valuation val) - : TheoryState(c, u, val), d_parent(parent) + : TheoryState(c, u, val), d_parent(nullptr) { } bool ArithState::isInConflict() const { - return d_parent.anyConflict() || d_conflict; + return d_parent->anyConflict() || d_conflict; } +void ArithState::setParent(TheoryArithPrivate* p) { d_parent = p; } + } // namespace arith } // namespace theory } // namespace cvc5 diff --git a/src/theory/arith/arith_state.h b/src/theory/arith/arith_state.h index 0aa848f46..a54ae6bf0 100644 --- a/src/theory/arith/arith_state.h +++ b/src/theory/arith/arith_state.h @@ -38,17 +38,16 @@ class TheoryArithPrivate; class ArithState : public TheoryState { public: - ArithState(TheoryArithPrivate& parent, - context::Context* c, - context::UserContext* u, - Valuation val); + ArithState(context::Context* c, context::UserContext* u, Valuation val); ~ArithState() {} /** Are we currently in conflict? */ bool isInConflict() const override; + /** Set parent */ + void setParent(TheoryArithPrivate* p); private: /** reference to parent */ - TheoryArithPrivate& d_parent; + TheoryArithPrivate* d_parent; }; } // namespace arith diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index 5c4678cb4..980714d53 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -41,18 +41,20 @@ TheoryArith::TheoryArith(context::Context* c, const LogicInfo& logicInfo, ProofNodeManager* pnm) : Theory(THEORY_ARITH, c, u, out, valuation, logicInfo, pnm), - d_internal( - new TheoryArithPrivate(*this, c, u, out, valuation, logicInfo, pnm)), d_ppRewriteTimer(smtStatisticsRegistry().registerTimer( "theory::arith::ppRewriteTimer")), - d_ppPfGen(pnm, c, "Arith::ppRewrite"), - d_astate(*d_internal, c, u, valuation), + d_astate(c, u, valuation), d_im(*this, d_astate, pnm), + d_ppre(c, pnm), + d_bab(d_astate, d_im, d_ppre, pnm), + d_internal(new TheoryArithPrivate(*this, c, u, d_bab, pnm)), d_nonlinearExtension(nullptr), d_opElim(pnm, logicInfo), d_arithPreproc(d_astate, d_im, pnm, d_opElim), d_rewriter(d_opElim) { + // currently a cyclic dependency to TheoryArithPrivate + d_astate.setParent(d_internal); // indicate we are using the theory state object and inference manager d_theoryState = &d_astate; d_inferManager = &d_im; @@ -114,7 +116,7 @@ TrustNode TheoryArith::ppRewrite(TNode atom, std::vector<SkolemLemma>& lems) if (atom.getKind() == kind::EQUAL) { - return ppRewriteEq(atom); + return d_ppre.ppRewriteEq(atom); } Assert(Theory::theoryOf(atom) == THEORY_ARITH); // Eliminate operators. Notice we must do this here since other @@ -126,30 +128,6 @@ TrustNode TheoryArith::ppRewrite(TNode atom, std::vector<SkolemLemma>& lems) return d_arithPreproc.eliminate(atom, lems, false); } -TrustNode TheoryArith::ppRewriteEq(TNode atom) -{ - Assert(atom.getKind() == kind::EQUAL); - if (!options::arithRewriteEq()) - { - return TrustNode::null(); - } - Assert(atom[0].getType().isReal()); - Node leq = NodeBuilder(kind::LEQ) << atom[0] << atom[1]; - Node geq = NodeBuilder(kind::GEQ) << atom[0] << atom[1]; - Node rewritten = Rewriter::rewrite(leq.andNode(geq)); - Debug("arith::preprocess") - << "arith::preprocess() : returning " << rewritten << endl; - // don't need to rewrite terms since rewritten is not a non-standard op - if (proofsEnabled()) - { - return d_ppPfGen.mkTrustedRewrite( - atom, - rewritten, - d_pnm->mkNode(PfRule::INT_TRUST, {}, {atom.eqNode(rewritten)})); - } - return TrustNode::mkTrustRewrite(atom, rewritten, nullptr); -} - Theory::PPAssertStatus TheoryArith::ppAssert( TrustNode tin, TrustSubstitutionMap& outSubstitutions) { @@ -239,6 +217,40 @@ bool TheoryArith::collectModelValues(TheoryModel* m, // get the model from the linear solver std::map<Node, Node> arithModel; d_internal->collectModelValues(termSet, arithModel); + // Double check that the model from the linear solver respects integer types, + // if it does not, add a branch and bound lemma. This typically should never + // be necessary, but is needed in rare cases. + bool addedLemma = false; + bool badAssignment = false; + for (const std::pair<const Node, Node>& p : arithModel) + { + if (p.first.getType().isInteger() && !p.second.getType().isInteger()) + { + Assert(false) << "TheoryArithPrivate generated a bad model value for " + "integer variable " + << p.first << " : " << p.second; + // must branch and bound + TrustNode lem = + d_bab.branchIntegerVariable(p.first, p.second.getConst<Rational>()); + if (d_im.trustedLemma(lem, InferenceId::ARITH_BB_LEMMA)) + { + addedLemma = true; + } + badAssignment = true; + } + } + if (addedLemma) + { + // we had to add a branch and bound lemma since the linear solver assigned + // a non-integer value to an integer variable. + return false; + } + // this would imply that linear arithmetic's model failed to satisfy a branch + // and bound lemma + AlwaysAssert(!badAssignment) + << "Bad assignment from TheoryArithPrivate::collectModelValues, and no " + "branching lemma was sent"; + // if non-linear is enabled, intercept the model, which may repair its values if (d_nonlinearExtension != nullptr) { diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h index 43c962e30..decbf93bd 100644 --- a/src/theory/arith/theory_arith.h +++ b/src/theory/arith/theory_arith.h @@ -21,7 +21,9 @@ #include "theory/arith/arith_preprocess.h" #include "theory/arith/arith_rewriter.h" #include "theory/arith/arith_state.h" +#include "theory/arith/branch_and_bound.h" #include "theory/arith/inference_manager.h" +#include "theory/arith/pp_rewrite_eq.h" #include "theory/theory.h" namespace cvc5 { @@ -39,16 +41,7 @@ class TheoryArithPrivate; * http://research.microsoft.com/en-us/um/people/leonardo/cav06.pdf */ class TheoryArith : public Theory { - private: friend class TheoryArithPrivate; - - TheoryArithPrivate* d_internal; - - TimerStat d_ppRewriteTimer; - - /** Used to prove pp-rewrites */ - EagerProofGenerator d_ppPfGen; - public: TheoryArith(context::Context* c, context::UserContext* u, @@ -136,17 +129,20 @@ class TheoryArith : public Theory { } private: - /** - * Preprocess equality, applies ppRewrite for equalities. This method is - * distinct from ppRewrite since it is not allowed to construct lemmas. - */ - TrustNode ppRewriteEq(TNode eq); /** Get the proof equality engine */ eq::ProofEqEngine* getProofEqEngine(); + /** Timer for ppRewrite */ + TimerStat d_ppRewriteTimer; /** The state object wrapping TheoryArithPrivate */ ArithState d_astate; /** The arith::InferenceManager. */ InferenceManager d_im; + /** The preprocess rewriter for equality */ + PreprocessRewriteEq d_ppre; + /** The branch and bound utility */ + BranchAndBound d_bab; + /** The (old) linear arithmetic solver */ + TheoryArithPrivate* d_internal; /** * The non-linear extension, responsible for all approaches for non-linear @@ -159,7 +155,6 @@ class TheoryArith : public Theory { ArithPreprocess d_arithPreproc; /** The theory rewriter for this theory. */ ArithRewriter d_rewriter; - };/* class TheoryArith */ } // namespace arith diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp index 98de1eeee..fb9de9641 100644 --- a/src/theory/arith/theory_arith_private.cpp +++ b/src/theory/arith/theory_arith_private.cpp @@ -87,13 +87,12 @@ static bool complexityBelow(const DenseMap<Rational>& row, uint32_t cap); TheoryArithPrivate::TheoryArithPrivate(TheoryArith& containing, context::Context* c, context::UserContext* u, - OutputChannel& out, - Valuation valuation, - const LogicInfo& logicInfo, + BranchAndBound& bab, ProofNodeManager* pnm) : d_containing(containing), d_foundNl(false), d_rowTracking(), + d_bab(bab), d_pnm(pnm), d_checker(), d_pfGen(new EagerProofGenerator(d_pnm, u)), @@ -3455,102 +3454,9 @@ TrustNode TheoryArithPrivate::branchIntegerVariable(ArithVar x) const const Rational& r = d.getNoninfinitesimalPart(); const Rational& i = d.getInfinitesimalPart(); Trace("integers") << "integers: assignment to [[" << d_partialModel.asNode(x) << "]] is " << r << "[" << i << "]" << endl; - Assert(!(r.getDenominator() == 1 && i.getNumerator() == 0)); - Assert(!d.isIntegral()); TNode var = d_partialModel.asNode(x); - Integer floor_d = d.floor(); - - TrustNode lem = TrustNode::null(); - NodeManager* nm = NodeManager::currentNM(); - if (options::brabTest()) - { - Trace("integers") << "branch-round-and-bound enabled" << endl; - Integer ceil_d = d.ceiling(); - Rational f = r - floor_d; - // Multiply by -1 to get abs value. - Rational c = (r - ceil_d) * (-1); - Integer nearest = (c > f) ? floor_d : ceil_d; - - // Prioritize trying a simple rounding of the real solution first, - // it that fails, fall back on original branch and bound strategy. - Node ub = Rewriter::rewrite( - nm->mkNode(kind::LEQ, var, mkRationalNode(nearest - 1))); - Node lb = Rewriter::rewrite( - nm->mkNode(kind::GEQ, var, mkRationalNode(nearest + 1))); - Node right = nm->mkNode(kind::OR, ub, lb); - Node rawEq = nm->mkNode(kind::EQUAL, var, mkRationalNode(nearest)); - Node eq = Rewriter::rewrite(rawEq); - // Also preprocess it before we send it out. This is important since - // arithmetic may prefer eliminating equalities. - TrustNode teq; - if (Theory::theoryOf(eq) == THEORY_ARITH) - { - teq = d_containing.ppRewriteEq(eq); - eq = teq.isNull() ? eq : teq.getNode(); - } - Node literal = d_containing.getValuation().ensureLiteral(eq); - Trace("integers") << "eq: " << eq << "\nto: " << literal << endl; - d_containing.getOutputChannel().requirePhase(literal, true); - Node l = nm->mkNode(kind::OR, literal, right); - Trace("integers") << "l: " << l << endl; - if (proofsEnabled()) - { - Node less = nm->mkNode(kind::LT, var, mkRationalNode(nearest)); - Node greater = nm->mkNode(kind::GT, var, mkRationalNode(nearest)); - // TODO (project #37): justify. Thread proofs through *ensureLiteral*. - Debug("integers::pf") << "less: " << less << endl; - Debug("integers::pf") << "greater: " << greater << endl; - Debug("integers::pf") << "literal: " << literal << endl; - Debug("integers::pf") << "eq: " << eq << endl; - Debug("integers::pf") << "rawEq: " << rawEq << endl; - Pf pfNotLit = d_pnm->mkAssume(literal.negate()); - // rewrite notLiteral to notRawEq, using teq. - Pf pfNotRawEq = - literal == rawEq - ? pfNotLit - : d_pnm->mkNode( - PfRule::MACRO_SR_PRED_TRANSFORM, - {pfNotLit, teq.getGenerator()->getProofFor(teq.getProven())}, - {rawEq.negate()}); - Pf pfBot = - d_pnm->mkNode(PfRule::CONTRA, - {d_pnm->mkNode(PfRule::ARITH_TRICHOTOMY, - {d_pnm->mkAssume(less.negate()), pfNotRawEq}, - {greater}), - d_pnm->mkAssume(greater.negate())}, - {}); - std::vector<Node> assumptions = { - literal.negate(), less.negate(), greater.negate()}; - // Proof of (not (and (not (= v i)) (not (< v i)) (not (> v i)))) - Pf pfNotAnd = d_pnm->mkScope(pfBot, assumptions); - Pf pfL = d_pnm->mkNode(PfRule::MACRO_SR_PRED_TRANSFORM, - {d_pnm->mkNode(PfRule::NOT_AND, {pfNotAnd}, {})}, - {l}); - lem = d_pfGen->mkTrustNode(l, pfL); - } - else - { - lem = TrustNode::mkTrustLemma(l, nullptr); - } - } - else - { - Node ub = - Rewriter::rewrite(nm->mkNode(kind::LEQ, var, mkRationalNode(floor_d))); - Node lb = ub.notNode(); - if (proofsEnabled()) - { - lem = d_pfGen->mkTrustNode( - nm->mkNode(kind::OR, ub, lb), PfRule::SPLIT, {}, {ub}); - } - else - { - lem = TrustNode::mkTrustLemma(nm->mkNode(kind::OR, ub, lb), nullptr); - } - } - - Trace("integers") << "integers: branch & bound: " << lem << endl; + TrustNode lem = d_bab.branchIntegerVariable(var, r); if (Debug.isOn("integers")) { Node l = lem.getNode(); diff --git a/src/theory/arith/theory_arith_private.h b/src/theory/arith/theory_arith_private.h index dc3c8bbb8..4afe121b9 100644 --- a/src/theory/arith/theory_arith_private.h +++ b/src/theory/arith/theory_arith_private.h @@ -33,6 +33,7 @@ #include "theory/arith/arith_utilities.h" #include "theory/arith/arithvar.h" #include "theory/arith/attempt_solution_simplex.h" +#include "theory/arith/branch_and_bound.h" #include "theory/arith/congruence_manager.h" #include "theory/arith/constraint.h" #include "theory/arith/delta_rational.h" @@ -94,7 +95,8 @@ private: bool d_foundNl; BoundInfoMap d_rowTracking; - + /** Branch and bound utility */ + BranchAndBound& d_bab; // For proofs /** Manages the proof nodes of this theory. */ ProofNodeManager* d_pnm; @@ -424,9 +426,7 @@ private: TheoryArithPrivate(TheoryArith& containing, context::Context* c, context::UserContext* u, - OutputChannel& out, - Valuation valuation, - const LogicInfo& logicInfo, + BranchAndBound& bab, ProofNodeManager* pnm); ~TheoryArithPrivate(); |