diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-04-07 13:36:15 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-04-07 18:36:15 +0000 |
commit | 04a494e251a8cc2c90bb429e2858f1c4eb8f88ff (patch) | |
tree | 03b1a5792f2f6ca5537353b86682f427090668da /src/theory/arith | |
parent | 5059658ee0d6fc65e4cb1652c605895d016cd274 (diff) |
Replace calls to NodeManager::mkSkolem with SkolemManager::mkDummySkolem (#6291)
This is in preparation for refactoring skolem creation throughout the code base to improve proofs and migrate Theory::expandDefinitions to Rewriter::expandDefinitions.
This PR also eliminates some unused code in TheoryArithPrivate.
Followup PRs will start formalizing/eliminating calls to mkDummySkolem.
Diffstat (limited to 'src/theory/arith')
-rw-r--r-- | src/theory/arith/arith_ite_utils.cpp | 4 | ||||
-rw-r--r-- | src/theory/arith/arith_utilities.h | 14 | ||||
-rw-r--r-- | src/theory/arith/callbacks.cpp | 5 | ||||
-rw-r--r-- | src/theory/arith/dio_solver.cpp | 8 | ||||
-rw-r--r-- | src/theory/arith/nl/cad_solver.cpp | 12 | ||||
-rw-r--r-- | src/theory/arith/nl/transcendental/sine_solver.cpp | 4 | ||||
-rw-r--r-- | src/theory/arith/nl/transcendental/transcendental_solver.cpp | 6 | ||||
-rw-r--r-- | src/theory/arith/theory_arith_private.cpp | 418 | ||||
-rw-r--r-- | src/theory/arith/theory_arith_private.h | 6 |
9 files changed, 26 insertions, 451 deletions
diff --git a/src/theory/arith/arith_ite_utils.cpp b/src/theory/arith/arith_ite_utils.cpp index 218fdf179..64309ad16 100644 --- a/src/theory/arith/arith_ite_utils.cpp +++ b/src/theory/arith/arith_ite_utils.cpp @@ -20,6 +20,7 @@ #include <ostream> #include "base/output.h" +#include "expr/skolem_manager.h" #include "options/smt_options.h" #include "preprocessing/util/ite_utilities.h" #include "theory/arith/arith_utilities.h" @@ -441,10 +442,11 @@ bool ArithIteUtils::solveBinOr(TNode binor){ // a: (sel = otherL) or (sel = otherR), otherL-otherR = c NodeManager* nm = NodeManager::currentNM(); + SkolemManager* sm = nm->getSkolemManager(); Node cnd = findIteCnd(binor[0], binor[1]); - Node sk = nm->mkSkolem("deor", nm->booleanType()); + Node sk = sm->mkDummySkolem("deor", nm->booleanType()); Node ite = sk.iteNode(otherL, otherR); d_skolems.insert(sk, cnd); addSubstitution(sel, ite); diff --git a/src/theory/arith/arith_utilities.h b/src/theory/arith/arith_utilities.h index bc35c6941..c9f572364 100644 --- a/src/theory/arith/arith_utilities.h +++ b/src/theory/arith/arith_utilities.h @@ -49,20 +49,6 @@ inline Node mkBoolNode(bool b){ return NodeManager::currentNM()->mkConst<bool>(b); } -inline Node mkIntSkolem(const std::string& name){ - return NodeManager::currentNM()->mkSkolem(name, NodeManager::currentNM()->integerType()); -} - -inline Node mkRealSkolem(const std::string& name){ - return NodeManager::currentNM()->mkSkolem(name, NodeManager::currentNM()->realType()); -} - -inline Node skolemFunction(const std::string& name, TypeNode dom, TypeNode range){ - NodeManager* currNM = NodeManager::currentNM(); - TypeNode functionType = currNM->mkFunctionType(dom, range); - return currNM->mkSkolem(name, functionType); -} - /** \f$ k \in {LT, LEQ, EQ, GEQ, GT} \f$ */ inline bool isRelationOperator(Kind k){ using namespace kind; diff --git a/src/theory/arith/callbacks.cpp b/src/theory/arith/callbacks.cpp index b2c48163f..0043ccae6 100644 --- a/src/theory/arith/callbacks.cpp +++ b/src/theory/arith/callbacks.cpp @@ -18,6 +18,7 @@ #include "theory/arith/callbacks.h" #include "expr/proof_node.h" +#include "expr/skolem_manager.h" #include "theory/arith/proof_macros.h" #include "theory/arith/theory_arith_private.h" @@ -46,7 +47,9 @@ TempVarMalloc::TempVarMalloc(TheoryArithPrivate& ta) : d_ta(ta) {} ArithVar TempVarMalloc::request(){ - Node skolem = mkRealSkolem("tmpVar"); + NodeManager* nm = NodeManager::currentNM(); + SkolemManager* sm = nm->getSkolemManager(); + Node skolem = sm->mkDummySkolem("tmpVar", nm->realType()); return d_ta.requestArithVar(skolem, false, true); } void TempVarMalloc::release(ArithVar v){ diff --git a/src/theory/arith/dio_solver.cpp b/src/theory/arith/dio_solver.cpp index 3825a3a42..6ceab1933 100644 --- a/src/theory/arith/dio_solver.cpp +++ b/src/theory/arith/dio_solver.cpp @@ -18,6 +18,7 @@ #include <iostream> #include "base/output.h" +#include "expr/skolem_manager.h" #include "options/arith_options.h" #include "smt/smt_statistics_registry.h" #include "theory/arith/partial_model.h" @@ -29,8 +30,11 @@ namespace theory { namespace arith { inline Node makeIntegerVariable(){ - NodeManager* curr = NodeManager::currentNM(); - return curr->mkSkolem("intvar", curr->integerType(), "is an integer variable created by the dio solver"); + NodeManager* nm = NodeManager::currentNM(); + SkolemManager* sm = nm->getSkolemManager(); + return sm->mkDummySkolem("intvar", + nm->integerType(), + "is an integer variable created by the dio solver"); } DioSolver::DioSolver(context::Context* ctxt) diff --git a/src/theory/arith/nl/cad_solver.cpp b/src/theory/arith/nl/cad_solver.cpp index 1cf9cbc54..aa9bce776 100644 --- a/src/theory/arith/nl/cad_solver.cpp +++ b/src/theory/arith/nl/cad_solver.cpp @@ -14,11 +14,12 @@ #include "theory/arith/nl/cad_solver.h" -#include "theory/inference_id.h" +#include "expr/skolem_manager.h" #include "theory/arith/inference_manager.h" #include "theory/arith/nl/cad/cdcac.h" #include "theory/arith/nl/nl_model.h" #include "theory/arith/nl/poly_conversion.h" +#include "theory/inference_id.h" namespace cvc5 { namespace theory { @@ -37,11 +38,10 @@ CadSolver::CadSolver(InferenceManager& im, d_im(im), d_model(model) { - d_ranVariable = - NodeManager::currentNM()->mkSkolem("__z", - NodeManager::currentNM()->realType(), - "", - NodeManager::SKOLEM_EXACT_NAME); + NodeManager* nm = NodeManager::currentNM(); + SkolemManager* sm = nm->getSkolemManager(); + d_ranVariable = sm->mkDummySkolem( + "__z", nm->realType(), "", NodeManager::SKOLEM_EXACT_NAME); #ifdef CVC4_POLY_IMP ProofChecker* pc = pnm != nullptr ? pnm->getChecker() : nullptr; if (pc != nullptr) diff --git a/src/theory/arith/nl/transcendental/sine_solver.cpp b/src/theory/arith/nl/transcendental/sine_solver.cpp index c8c375096..2a1f2ad91 100644 --- a/src/theory/arith/nl/transcendental/sine_solver.cpp +++ b/src/theory/arith/nl/transcendental/sine_solver.cpp @@ -20,6 +20,7 @@ #include "expr/node_algorithm.h" #include "expr/node_builder.h" #include "expr/proof.h" +#include "expr/skolem_manager.h" #include "options/arith_options.h" #include "theory/arith/arith_msum.h" #include "theory/arith/arith_utilities.h" @@ -55,10 +56,11 @@ SineSolver::~SineSolver() {} void SineSolver::doPhaseShift(TNode a, TNode new_a, TNode y) { NodeManager* nm = NodeManager::currentNM(); + SkolemManager* sm = nm->getSkolemManager(); Assert(a.getKind() == Kind::SINE); Trace("nl-ext-tf") << "Basis sine : " << new_a << " for " << a << std::endl; Assert(!d_data->d_pi.isNull()); - Node shift = nm->mkSkolem("s", nm->integerType(), "number of shifts"); + Node shift = sm->mkDummySkolem("s", nm->integerType(), "number of shifts"); // TODO (cvc4-projects #47) : do not introduce shift here, instead needs model-based // refinement for constant shifts (cvc4-projects #1284) Node lem = nm->mkNode( diff --git a/src/theory/arith/nl/transcendental/transcendental_solver.cpp b/src/theory/arith/nl/transcendental/transcendental_solver.cpp index ed5ab4255..b3fd40ce7 100644 --- a/src/theory/arith/nl/transcendental/transcendental_solver.cpp +++ b/src/theory/arith/nl/transcendental/transcendental_solver.cpp @@ -19,6 +19,7 @@ #include "expr/node_algorithm.h" #include "expr/node_builder.h" +#include "expr/skolem_manager.h" #include "options/arith_options.h" #include "theory/arith/arith_msum.h" #include "theory/arith/arith_utilities.h" @@ -56,14 +57,15 @@ void TranscendentalSolver::initLastCall(const std::vector<Node>& xts) } NodeManager* nm = NodeManager::currentNM(); + SkolemManager* sm = nm->getSkolemManager(); for (const Node& a : needsMaster) { // should not have processed this already Assert(d_tstate.d_trMaster.find(a) == d_tstate.d_trMaster.end()); Kind k = a.getKind(); Assert(k == Kind::SINE || k == Kind::EXPONENTIAL); - Node y = - nm->mkSkolem("y", nm->realType(), "phase shifted trigonometric arg"); + Node y = sm->mkDummySkolem( + "y", nm->realType(), "phase shifted trigonometric arg"); Node new_a = nm->mkNode(k, y); d_tstate.d_trSlaves[new_a].insert(new_a); d_tstate.d_trSlaves[new_a].insert(a); diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp index 0a64a4e63..7ad0bbfbb 100644 --- a/src/theory/arith/theory_arith_private.cpp +++ b/src/theory/arith/theory_arith_private.cpp @@ -4958,16 +4958,6 @@ std::pair<bool, Node> TheoryArithPrivate::entailmentCheck(TNode lit, const Arith setToMin(secDir * dm.sgn(), bestSecDiff, tmp); } break; - case inferbounds::Simplex: - { - // primDir * diffm * diff < c or primDir * diffm * diff > c - tmp = entailmentCheckSimplex(primDir * dm.sgn(), dp, ibalg, out.getSimplexSideEffects()); - setToMin(primDir * dm.sgn(), bestPrimDiff, tmp); - - tmp = entailmentCheckSimplex(secDir * dm.sgn(), dp, ibalg, out.getSimplexSideEffects()); - setToMin(secDir * dm.sgn(), bestSecDiff, tmp); - } - break; default: Unhandled(); } @@ -5298,419 +5288,11 @@ void TheoryArithPrivate::entailmentCheckRowSum(std::pair<Node, DeltaRational>& t tmp.first = nb; } -std::pair<Node, DeltaRational> TheoryArithPrivate::entailmentCheckSimplex(int sgn, TNode tp, const inferbounds::InferBoundAlgorithm& param, InferBoundsResult& result){ - - if((sgn == 0) || !(d_qflraStatus == Result::SAT && d_errorSet.noSignals()) || tp.getKind() == CONST_RATIONAL){ - return make_pair(Node::null(), DeltaRational()); - } - - Assert(d_qflraStatus == Result::SAT); - Assert(d_errorSet.noSignals()); - Assert(param.getAlgorithm() == inferbounds::Simplex); - - // TODO Move me into a new file - - enum ResultState {Unset, Inferred, NoBound, ReachedThreshold, ExhaustedRounds}; - ResultState finalState = Unset; - - const int maxRounds = - param.getSimplexRounds().just() ? param.getSimplexRounds().value() : -1; - - Maybe<DeltaRational> threshold; - // TODO: get this from the parameters - - // setup term - Polynomial p = Polynomial::parsePolynomial(tp); - vector<ArithVar> variables; - vector<Rational> coefficients; - asVectors(p, coefficients, variables); - if(sgn < 0){ - for(size_t i=0, N=coefficients.size(); i < N; ++i){ - coefficients[i] = -coefficients[i]; - } - } - // implicitly an upperbound - Node skolem = mkRealSkolem("tmpVar$$"); - ArithVar optVar = requestArithVar(skolem, false, true); - d_tableau.addRow(optVar, coefficients, variables); - RowIndex ridx = d_tableau.basicToRowIndex(optVar); - - DeltaRational newAssignment = d_linEq.computeRowValue(optVar, false); - d_partialModel.setAssignment(optVar, newAssignment); - d_linEq.trackRowIndex(d_tableau.basicToRowIndex(optVar)); - - // Setup simplex - d_partialModel.stopQueueingBoundCounts(); - UpdateTrackingCallback utcb(&d_linEq); - d_partialModel.processBoundsQueue(utcb); - d_linEq.startTrackingBoundCounts(); - - // maximize optVar via primal Simplex - int rounds = 0; - while(finalState == Unset){ - ++rounds; - if(maxRounds >= 0 && rounds > maxRounds){ - finalState = ExhaustedRounds; - break; - } - - // select entering by bland's rule - // TODO improve upon bland's - ArithVar entering = ARITHVAR_SENTINEL; - const Tableau::Entry* enteringEntry = NULL; - for(Tableau::RowIterator ri = d_tableau.ridRowIterator(ridx); !ri.atEnd(); ++ri){ - const Tableau::Entry& entry = *ri; - ArithVar v = entry.getColVar(); - if(v != optVar){ - int sgn1 = entry.getCoefficient().sgn(); - Assert(sgn1 != 0); - bool candidate = (sgn1 > 0) - ? (d_partialModel.cmpAssignmentUpperBound(v) != 0) - : (d_partialModel.cmpAssignmentLowerBound(v) != 0); - if(candidate && (entering == ARITHVAR_SENTINEL || entering > v)){ - entering = v; - enteringEntry = &entry; - } - } - } - if(entering == ARITHVAR_SENTINEL){ - finalState = Inferred; - break; - } - Assert(entering != ARITHVAR_SENTINEL); - Assert(enteringEntry != NULL); - - int esgn = enteringEntry->getCoefficient().sgn(); - Assert(esgn != 0); - - // select leaving and ratio - ArithVar leaving = ARITHVAR_SENTINEL; - DeltaRational minRatio; - const Tableau::Entry* pivotEntry = NULL; - - // Special case check the upper/lowerbound on entering - ConstraintP cOnEntering = (esgn > 0) - ? d_partialModel.getUpperBoundConstraint(entering) - : d_partialModel.getLowerBoundConstraint(entering); - if(cOnEntering != NullConstraint){ - leaving = entering; - minRatio = d_partialModel.getAssignment(entering) - cOnEntering->getValue(); - } - for(Tableau::ColIterator ci = d_tableau.colIterator(entering); !ci.atEnd(); ++ci){ - const Tableau::Entry& centry = *ci; - ArithVar basic = d_tableau.rowIndexToBasic(centry.getRowIndex()); - int csgn = centry.getCoefficient().sgn(); - int basicDir = csgn * esgn; - - ConstraintP bound = (basicDir > 0) - ? d_partialModel.getUpperBoundConstraint(basic) - : d_partialModel.getLowerBoundConstraint(basic); - if(bound != NullConstraint){ - DeltaRational diff = d_partialModel.getAssignment(basic) - bound->getValue(); - DeltaRational ratio = diff/(centry.getCoefficient()); - bool selected = false; - if(leaving == ARITHVAR_SENTINEL){ - selected = true; - }else{ - int cmp = ratio.compare(minRatio); - if((csgn > 0) ? (cmp <= 0) : (cmp >= 0)){ - selected = (cmp != 0) || - ((leaving != entering) && (basic < leaving)); - } - } - if(selected){ - leaving = basic; - minRatio = ratio; - pivotEntry = ¢ry; - } - } - } - - - if(leaving == ARITHVAR_SENTINEL){ - finalState = NoBound; - break; - }else if(leaving == entering){ - d_linEq.update(entering, minRatio); - }else{ - DeltaRational newLeaving = minRatio * (pivotEntry->getCoefficient()); - d_linEq.pivotAndUpdate(leaving, entering, newLeaving); - // no conflicts clear signals - Assert(d_errorSet.noSignals()); - } - - if(threshold.just()){ - if (d_partialModel.getAssignment(optVar) >= threshold.value()) - { - finalState = ReachedThreshold; - break; - } - } - }; - - result = InferBoundsResult(tp, sgn > 0); - - // tear down term - switch(finalState){ - case Inferred: - { - NodeBuilder nb(kind::AND); - for(Tableau::RowIterator ri = d_tableau.ridRowIterator(ridx); !ri.atEnd(); ++ri){ - const Tableau::Entry& e =*ri; - ArithVar colVar = e.getColVar(); - if(colVar != optVar){ - const Rational& q = e.getCoefficient(); - Assert(q.sgn() != 0); - ConstraintP c = (q.sgn() > 0) - ? d_partialModel.getUpperBoundConstraint(colVar) - : d_partialModel.getLowerBoundConstraint(colVar); - c->externalExplainByAssertions(nb); - } - } - Assert(nb.getNumChildren() >= 1); - Node exp = (nb.getNumChildren() >= 2) ? (Node) nb : nb[0]; - result.setBound(d_partialModel.getAssignment(optVar), exp); - result.setIsOptimal(); - break; - } - case NoBound: - break; - case ReachedThreshold: - result.setReachedThreshold(); - break; - case ExhaustedRounds: - result.setBudgetExhausted(); - break; - case Unset: - default: - Unreachable(); - break; - }; - - d_linEq.stopTrackingRowIndex(ridx); - d_tableau.removeBasicRow(optVar); - releaseArithVar(optVar); - - d_linEq.stopTrackingBoundCounts(); - d_partialModel.startQueueingBoundCounts(); - - if(result.foundBound()){ - return make_pair(result.getExplanation(), result.getValue()); - }else{ - return make_pair(Node::null(), DeltaRational()); - } -} - ArithProofRuleChecker* TheoryArithPrivate::getProofChecker() { return &d_checker; } -// InferBoundsResult TheoryArithPrivate::inferUpperBoundSimplex(TNode t, const -// inferbounds::InferBoundAlgorithm& param){ -// Assert(param.findUpperBound()); - -// if(!(d_qflraStatus == Result::SAT && d_errorSet.noSignals())){ -// InferBoundsResult inconsistent; -// inconsistent.setInconsistent(); -// return inconsistent; -// } - -// Assert(d_qflraStatus == Result::SAT); -// Assert(d_errorSet.noSignals()); - -// // TODO Move me into a new file - -// enum ResultState {Unset, Inferred, NoBound, ReachedThreshold, ExhaustedRounds}; -// ResultState finalState = Unset; - -// int maxRounds = 0; -// switch(param.getParamKind()){ -// case InferBoundsParameters::Unbounded: -// maxRounds = -1; -// break; -// case InferBoundsParameters::NumVars: -// maxRounds = d_partialModel.getNumberOfVariables() * param.getSimplexRoundParameter(); -// break; -// case InferBoundsParameters::Direct: -// maxRounds = param.getSimplexRoundParameter(); -// break; -// default: maxRounds = 0; break; -// } - -// // setup term -// Polynomial p = Polynomial::parsePolynomial(t); -// vector<ArithVar> variables; -// vector<Rational> coefficients; -// asVectors(p, coefficients, variables); - -// Node skolem = mkRealSkolem("tmpVar$$"); -// ArithVar optVar = requestArithVar(skolem, false, true); -// d_tableau.addRow(optVar, coefficients, variables); -// RowIndex ridx = d_tableau.basicToRowIndex(optVar); - -// DeltaRational newAssignment = d_linEq.computeRowValue(optVar, false); -// d_partialModel.setAssignment(optVar, newAssignment); -// d_linEq.trackRowIndex(d_tableau.basicToRowIndex(optVar)); - -// // Setup simplex -// d_partialModel.stopQueueingBoundCounts(); -// UpdateTrackingCallback utcb(&d_linEq); -// d_partialModel.processBoundsQueue(utcb); -// d_linEq.startTrackingBoundCounts(); - -// // maximize optVar via primal Simplex -// int rounds = 0; -// while(finalState == Unset){ -// ++rounds; -// if(maxRounds >= 0 && rounds > maxRounds){ -// finalState = ExhaustedRounds; -// break; -// } - -// // select entering by bland's rule -// // TODO improve upon bland's -// ArithVar entering = ARITHVAR_SENTINEL; -// const Tableau::Entry* enteringEntry = NULL; -// for(Tableau::RowIterator ri = d_tableau.ridRowIterator(ridx); -// !ri.atEnd(); ++ri){ -// const Tableau::Entry& entry = *ri; -// ArithVar v = entry.getColVar(); -// if(v != optVar){ -// int sgn = entry.getCoefficient().sgn(); -// Assert(sgn != 0); -// bool candidate = (sgn > 0) -// ? (d_partialModel.cmpAssignmentUpperBound(v) != 0) -// : (d_partialModel.cmpAssignmentLowerBound(v) != 0); -// if(candidate && (entering == ARITHVAR_SENTINEL || entering > v)){ -// entering = v; -// enteringEntry = &entry; -// } -// } -// } -// if(entering == ARITHVAR_SENTINEL){ -// finalState = Inferred; -// break; -// } -// Assert(entering != ARITHVAR_SENTINEL); -// Assert(enteringEntry != NULL); - -// int esgn = enteringEntry->getCoefficient().sgn(); -// Assert(esgn != 0); - -// // select leaving and ratio -// ArithVar leaving = ARITHVAR_SENTINEL; -// DeltaRational minRatio; -// const Tableau::Entry* pivotEntry = NULL; - -// // Special case check the upper/lowerbound on entering -// ConstraintP cOnEntering = (esgn > 0) -// ? d_partialModel.getUpperBoundConstraint(entering) -// : d_partialModel.getLowerBoundConstraint(entering); -// if(cOnEntering != NullConstraint){ -// leaving = entering; -// minRatio = d_partialModel.getAssignment(entering) - cOnEntering->getValue(); -// } -// for(Tableau::ColIterator ci = d_tableau.colIterator(entering); !ci.atEnd(); ++ci){ -// const Tableau::Entry& centry = *ci; -// ArithVar basic = d_tableau.rowIndexToBasic(centry.getRowIndex()); -// int csgn = centry.getCoefficient().sgn(); -// int basicDir = csgn * esgn; - -// ConstraintP bound = (basicDir > 0) -// ? d_partialModel.getUpperBoundConstraint(basic) -// : d_partialModel.getLowerBoundConstraint(basic); -// if(bound != NullConstraint){ -// DeltaRational diff = d_partialModel.getAssignment(basic) - bound->getValue(); -// DeltaRational ratio = diff/(centry.getCoefficient()); -// bool selected = false; -// if(leaving == ARITHVAR_SENTINEL){ -// selected = true; -// }else{ -// int cmp = ratio.compare(minRatio); -// if((csgn > 0) ? (cmp <= 0) : (cmp >= 0)){ -// selected = (cmp != 0) || -// ((leaving != entering) && (basic < leaving)); -// } -// } -// if(selected){ -// leaving = basic; -// minRatio = ratio; -// pivotEntry = ¢ry; -// } -// } -// } - -// if(leaving == ARITHVAR_SENTINEL){ -// finalState = NoBound; -// break; -// }else if(leaving == entering){ -// d_linEq.update(entering, minRatio); -// }else{ -// DeltaRational newLeaving = minRatio * (pivotEntry->getCoefficient()); -// d_linEq.pivotAndUpdate(leaving, entering, newLeaving); -// // no conflicts clear signals -// Assert(d_errorSet.noSignals()); -// } - -// if(param.useThreshold()){ -// if(d_partialModel.getAssignment(optVar) >= param.getThreshold()){ -// finalState = ReachedThreshold; -// break; -// } -// } -// }; - -// InferBoundsResult result(t, param.findUpperBound()); - -// // tear down term -// switch(finalState){ -// case Inferred: -// { -// NodeBuilder nb(kind::AND); -// for(Tableau::RowIterator ri = d_tableau.ridRowIterator(ridx); -// !ri.atEnd(); ++ri){ -// const Tableau::Entry& e =*ri; -// ArithVar colVar = e.getColVar(); -// if(colVar != optVar){ -// const Rational& q = e.getCoefficient(); -// Assert(q.sgn() != 0); -// ConstraintP c = (q.sgn() > 0) -// ? d_partialModel.getUpperBoundConstraint(colVar) -// : d_partialModel.getLowerBoundConstraint(colVar); -// c->externalExplainByAssertions(nb); -// } -// } -// Assert(nb.getNumChildren() >= 1); -// Node exp = (nb.getNumChildren() >= 2) ? (Node) nb : nb[0]; -// result.setBound(d_partialModel.getAssignment(optVar), exp); -// result.setIsOptimal(); -// break; -// } -// case NoBound: -// break; -// case ReachedThreshold: -// result.setReachedThreshold(); -// break; -// case ExhaustedRounds: -// result.setBudgetExhausted(); -// break; -// case Unset: -// default: -// Unreachable(); -// break; -// }; - -// d_linEq.stopTrackingRowIndex(ridx); -// d_tableau.removeBasicRow(optVar); -// releaseArithVar(optVar); - -// d_linEq.stopTrackingBoundCounts(); -// d_partialModel.startQueueingBoundCounts(); - -// return result; -// } - } // namespace arith } // namespace theory } // namespace cvc5 diff --git a/src/theory/arith/theory_arith_private.h b/src/theory/arith/theory_arith_private.h index ba3fdfaf5..50fb89808 100644 --- a/src/theory/arith/theory_arith_private.h +++ b/src/theory/arith/theory_arith_private.h @@ -137,12 +137,6 @@ private: void entailmentCheckBoundLookup(std::pair<Node, DeltaRational>& tmp, int sgn, TNode tp) const; void entailmentCheckRowSum(std::pair<Node, DeltaRational>& tmp, int sgn, TNode tp) const; - std::pair<Node, DeltaRational> entailmentCheckSimplex(int sgn, TNode tp, const inferbounds::InferBoundAlgorithm& p, InferBoundsResult& out); - - //InferBoundsResult inferBound(TNode term, const InferBoundsParameters& p); - //InferBoundsResult inferUpperBoundLookup(TNode t, const InferBoundsParameters& p); - //InferBoundsResult inferUpperBoundSimplex(TNode t, const SimplexInferBoundsParameters& p); - /** * Infers either a new upper/lower bound on term in the real relaxation. * Either: |