This double checks that TheoryArithPrivate generates a model that does not assign real values to integer variables.
This is done outside of TheoryArithPrivate intentionally, so that it can be checked independently.
This code should very rarely be applied but would have caught the incorrect model which led to wrong results in the UFNIA division of smtcomp 2021.
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
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
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;
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
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)
{
// 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)
{
#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 {
* 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,
}
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
ArithPreprocess d_arithPreproc;
/** The theory rewriter for this theory. */
ArithRewriter d_rewriter;
-
};/* class TheoryArith */
} // namespace arith
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)),
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();
#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"
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;
TheoryArithPrivate(TheoryArith& containing,
context::Context* c,
context::UserContext* u,
- OutputChannel& out,
- Valuation valuation,
- const LogicInfo& logicInfo,
+ BranchAndBound& bab,
ProofNodeManager* pnm);
~TheoryArithPrivate();
projects / cvc5.git / commitdiff