diff options
| -rw-r--r-- | src/theory/arith/Makefile.am | 3 | ||||
| -rw-r--r-- | src/theory/arith/bound_counts.cpp | 16 | ||||
| -rw-r--r-- | src/theory/arith/bound_counts.h | 17 | ||||
| -rw-r--r-- | src/theory/arith/callbacks.cpp | 4 | ||||
| -rw-r--r-- | src/theory/arith/callbacks.h | 16 | ||||
| -rw-r--r-- | src/theory/arith/error_set.h | 2 | ||||
| -rw-r--r-- | src/theory/arith/fc_simplex.cpp | 9 | ||||
| -rw-r--r-- | src/theory/arith/linear_equality.cpp | 208 | ||||
| -rw-r--r-- | src/theory/arith/linear_equality.h | 12 | ||||
| -rw-r--r-- | src/theory/arith/pure_update_simplex.cpp | 261 | ||||
| -rw-r--r-- | src/theory/arith/pure_update_simplex.h | 118 | ||||
| -rw-r--r-- | src/theory/arith/simplex-converge.cpp | 1674 | ||||
| -rw-r--r-- | src/theory/arith/simplex-converge.h | 531 | ||||
| -rw-r--r-- | src/theory/arith/soi_simplex.cpp | 1 | ||||
| -rw-r--r-- | src/theory/arith/theory_arith_private.cpp | 8 | ||||
| -rw-r--r-- | src/theory/arith/theory_arith_private.h | 6 |
16 files changed, 33 insertions, 2853 deletions
diff --git a/src/theory/arith/Makefile.am b/src/theory/arith/Makefile.am index e6ef6fdc2..ed14e972b 100644 --- a/src/theory/arith/Makefile.am +++ b/src/theory/arith/Makefile.am @@ -11,7 +11,6 @@ libarith_la_SOURCES = \ arithvar.h \ arithvar.cpp \ bound_counts.h \ - bound_counts.cpp \ arith_rewriter.h \ arith_rewriter.cpp \ arith_static_learner.h \ @@ -52,8 +51,6 @@ libarith_la_SOURCES = \ soi_simplex.cpp \ approx_simplex.h \ approx_simplex.cpp \ - pure_update_simplex.h \ - pure_update_simplex.cpp \ theory_arith.h \ theory_arith.cpp \ theory_arith_private_forward.h \ diff --git a/src/theory/arith/bound_counts.cpp b/src/theory/arith/bound_counts.cpp deleted file mode 100644 index 27e9a35dc..000000000 --- a/src/theory/arith/bound_counts.cpp +++ /dev/null @@ -1,16 +0,0 @@ -#include "theory/arith/bound_counts.h" -#include "theory/arith/tableau.h" - -namespace CVC4 { -namespace theory { -namespace arith { - -const BoundsInfo& BoundCountingLookup::boundsInfo(ArithVar basic) const { - RowIndex ridx = d_tab->basicToRowIndex(basic); - Assert(d_bc->isKey(ridx)); - return (*d_bc)[ridx]; -} - -}/* CVC4::theory::arith namespace */ -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ diff --git a/src/theory/arith/bound_counts.h b/src/theory/arith/bound_counts.h index d82fff3eb..1ee6ada06 100644 --- a/src/theory/arith/bound_counts.h +++ b/src/theory/arith/bound_counts.h @@ -198,23 +198,6 @@ public: /** This is intended to map each row to its relevant bound information. */ typedef DenseMap<BoundsInfo> BoundInfoMap; -class Tableau; - -class BoundCountingLookup { -private: - BoundInfoMap* d_bc; - Tableau* d_tab; -public: - BoundCountingLookup(BoundInfoMap* bc, Tableau* tab) : d_bc(bc), d_tab(tab) {} - const BoundsInfo& boundsInfo(ArithVar basic) const; - BoundCounts atBounds(ArithVar basic) const{ - return boundsInfo(basic).atBounds(); - } - BoundCounts hasBounds(ArithVar basic) const { - return boundsInfo(basic).hasBounds(); - } -}; - inline std::ostream& operator<<(std::ostream& os, const BoundCounts& bc){ os << "[bc " << bc.lowerBoundCount() << ", " << bc.upperBoundCount() << "]"; return os; diff --git a/src/theory/arith/callbacks.cpp b/src/theory/arith/callbacks.cpp index 6b6170b20..1e827d316 100644 --- a/src/theory/arith/callbacks.cpp +++ b/src/theory/arith/callbacks.cpp @@ -32,6 +32,10 @@ void RaiseConflict::operator()(Node n){ d_ta.raiseConflict(n); } +const BoundsInfo& BoundCountingLookup::boundsInfo(ArithVar basic) const{ + return d_ta.boundsInfo(basic); +} + }/* CVC4::theory::arith namespace */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ diff --git a/src/theory/arith/callbacks.h b/src/theory/arith/callbacks.h index 0d754d159..718799e9f 100644 --- a/src/theory/arith/callbacks.h +++ b/src/theory/arith/callbacks.h @@ -3,10 +3,10 @@ #include "expr/node.h" #include "util/rational.h" -#include "context/cdlist.h" #include "theory/arith/theory_arith_private_forward.h" #include "theory/arith/arithvar.h" +#include "theory/arith/bound_counts.h" namespace CVC4 { namespace theory { @@ -87,6 +87,20 @@ public: void operator()(Node n); }; +class BoundCountingLookup { +private: + TheoryArithPrivate& d_ta; +public: + BoundCountingLookup(TheoryArithPrivate& ta) : d_ta(ta) {} + const BoundsInfo& boundsInfo(ArithVar basic) const; + BoundCounts atBounds(ArithVar basic) const{ + return boundsInfo(basic).atBounds(); + } + BoundCounts hasBounds(ArithVar basic) const { + return boundsInfo(basic).hasBounds(); + } +}; + }/* CVC4::theory::arith namespace */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ diff --git a/src/theory/arith/error_set.h b/src/theory/arith/error_set.h index 27ac6ccd2..c5174a86a 100644 --- a/src/theory/arith/error_set.h +++ b/src/theory/arith/error_set.h @@ -26,9 +26,9 @@ #include "theory/arith/partial_model.h" #include "theory/arith/arith_heuristic_pivot_rule.h" #include "theory/arith/tableau_sizes.h" +#include "theory/arith/callbacks.h" #include "util/statistics_registry.h" -//#include <boost/heap/d_ary_heap.hpp> #if CVC4_GCC_HAS_PB_DS_BUG // Unfortunate bug in some older GCCs (e.g., v4.2): diff --git a/src/theory/arith/fc_simplex.cpp b/src/theory/arith/fc_simplex.cpp index d264be978..e99e62505 100644 --- a/src/theory/arith/fc_simplex.cpp +++ b/src/theory/arith/fc_simplex.cpp @@ -358,18 +358,9 @@ UpdateInfo FCSimplexDecisionProcedure::selectPrimalUpdate(ArithVar basic, Linear ArithVar curr = cand.d_nb; const Rational& coeff = *cand.d_coeff; -#warning "Who is using computeSafeUpdate?" LinearEqualityModule::UpdatePreferenceFunction leavingPrefFunc = selectLeavingFunction(curr); UpdateInfo currProposal = d_linEq.speculativeUpdate(curr, coeff, leavingPrefFunc); - //int curr_movement = cand.d_sgn; - // if(isFocus){ - // currProposal = d_linEq.speculativeUpdate(curr, coeff, upf); - // }else{ - // currProposal = UpdateInfo(curr, curr_movement); - // d_linEq.computeSafeUpdate(currProposal, bpf); - // } - Debug("arith::selectPrimalUpdate") << "selected " << selected << endl << "currProp " << currProposal << endl diff --git a/src/theory/arith/linear_equality.cpp b/src/theory/arith/linear_equality.cpp index b1dfa8705..1c32f80e4 100644 --- a/src/theory/arith/linear_equality.cpp +++ b/src/theory/arith/linear_equality.cpp @@ -55,7 +55,6 @@ LinearEqualityModule::LinearEqualityModule(ArithVariables& vars, Tableau& t, Bou d_basicVariableUpdates(f), d_increasing(1), d_decreasing(-1), - d_relevantErrorBuffer(), d_btracking(boundsTracking), d_areTracking(false), d_trackCallback(this) @@ -851,213 +850,6 @@ void LinearEqualityModule::trackingCoefficientChange(RowIndex ridx, ArithVar nb, row_bi.addInSgn(nb_inf, oldSgn, currSgn); } -void LinearEqualityModule::computeSafeUpdate(UpdateInfo& inf, VarPreferenceFunction pref){ - ArithVar nb = inf.nonbasic(); - int sgn = inf.nonbasicDirection(); - Assert(sgn != 0); - Assert(!d_tableau.isBasic(nb)); - - - // Error variables moving in the correct direction - Assert(d_relevantErrorBuffer.empty()); - - // phases : - enum ComputeSafePhase { - NoBoundSelected, - NbsBoundSelected, - BasicBoundSelected, - DegenerateBoundSelected - } phase; - - phase = NoBoundSelected; - - static int instance = 0; - Debug("computeSafeUpdate") << "computeSafeUpdate " << (++instance) << endl; - - if(sgn > 0 && d_variables.hasUpperBound(nb)){ - Constraint ub = d_variables.getUpperBoundConstraint(nb); - inf.updatePureFocus(ub->getValue() - d_variables.getAssignment(nb), ub); - - Assert(inf.nonbasicDelta().sgn() == sgn); - Debug("computeSafeUpdate") << "computeSafeUpdate " << inf.limiting() << endl; - phase = NbsBoundSelected; - }else if(sgn < 0 && d_variables.hasLowerBound(nb)){ - Constraint lb = d_variables.getLowerBoundConstraint(nb); - inf.updatePureFocus(lb->getValue() - d_variables.getAssignment(nb), lb); - - Assert(inf.nonbasicDelta().sgn() == sgn); - - Debug("computeSafeUpdate") << "computeSafeUpdate " << inf.limiting() << endl; - phase = NbsBoundSelected; - } - - Tableau::ColIterator basicIter = d_tableau.colIterator(nb); - for(; !basicIter.atEnd(); ++basicIter){ - const Tableau::Entry& entry = *basicIter; - Assert(entry.getColVar() == nb); - - ArithVar basic = d_tableau.rowIndexToBasic(entry.getRowIndex()); - const Rational& a_ji = entry.getCoefficient(); - int basic_movement = sgn * a_ji.sgn(); - - Debug("computeSafeUpdate") - << "computeSafeUpdate: " - << basic << ", " - << basic_movement << ", " - << d_variables.cmpAssignmentUpperBound(basic) << ", " - << d_variables.cmpAssignmentLowerBound(basic) << ", " - << a_ji << ", " - << d_variables.getAssignment(basic) << endl; - - Constraint proposal = NullConstraint; - - if(basic_movement > 0){ - if(d_variables.cmpAssignmentLowerBound(basic) < 0){ - d_relevantErrorBuffer.push_back(&entry); - } - if(d_variables.hasUpperBound(basic) && - d_variables.cmpAssignmentUpperBound(basic) <= 0){ - proposal = d_variables.getUpperBoundConstraint(basic); - } - }else if(basic_movement < 0){ - if(d_variables.cmpAssignmentUpperBound(basic) > 0){ - d_relevantErrorBuffer.push_back(&entry); - } - if(d_variables.hasLowerBound(basic) && - d_variables.cmpAssignmentLowerBound(basic) >= 0){ - proposal = d_variables.getLowerBoundConstraint(basic); - } - } - if(proposal != NullConstraint){ - const Rational& coeff = entry.getCoefficient(); - DeltaRational diff = proposal->getValue() - d_variables.getAssignment(basic); - diff /= coeff; - int cmp = phase == NoBoundSelected ? 0 : diff.cmp(inf.nonbasicDelta()); - Assert(diff.sgn() == sgn || diff.sgn() == 0); - bool prefer = false; - switch(phase){ - case NoBoundSelected: - prefer = true; - break; - case NbsBoundSelected: - prefer = (sgn > 0 && cmp < 0 ) || (sgn < 0 && cmp > 0); - break; - case BasicBoundSelected: - prefer = - (sgn > 0 && cmp < 0 ) || - (sgn < 0 && cmp > 0) || - (cmp == 0 && basic == (this->*pref)(basic, inf.leaving())); - break; - case DegenerateBoundSelected: - prefer = cmp == 0 && basic == (this->*pref)(basic, inf.leaving()); - break; - } - if(prefer){ - inf.updatePivot(diff, coeff, proposal); - - phase = (diff.sgn() != 0) ? BasicBoundSelected : DegenerateBoundSelected; - } - } - } - - if(phase == DegenerateBoundSelected){ - inf.setErrorsChange(0); - }else{ - computedFixed(inf); - } - inf.determineFocusDirection(); - - d_relevantErrorBuffer.clear(); -} - -void LinearEqualityModule::computedFixed(UpdateInfo& proposal){ - Assert(proposal.nonbasicDirection() != 0); - Assert(!d_tableau.isBasic(proposal.nonbasic())); - - //bool unconstrained = (proposal.d_limiting == NullConstraint); - - Assert(!proposal.unbounded() || !d_relevantErrorBuffer.empty()); - - Assert(proposal.unbounded() || - proposal.nonbasicDelta().sgn() == proposal.nonbasicDirection()); - - // proposal.d_value is the max - - UpdateInfo max; - int dropped = 0; - //Constraint maxFix = NullConstraint; - //DeltaRational maxAmount; - - EntryPointerVector::const_iterator i = d_relevantErrorBuffer.begin(); - EntryPointerVector::const_iterator i_end = d_relevantErrorBuffer.end(); - for(; i != i_end; ++i){ - const Tableau::Entry& entry = *(*i); - Assert(entry.getColVar() == proposal.nonbasic()); - - ArithVar basic = d_tableau.rowIndexToBasic(entry.getRowIndex()); - const Rational& a_ji = entry.getCoefficient(); - int basic_movement = proposal.nonbasicDirection() * a_ji.sgn(); - - DeltaRational theta; - DeltaRational proposedValue; - if(!proposal.unbounded()){ - theta = proposal.nonbasicDelta() * a_ji; - proposedValue = theta + d_variables.getAssignment(basic); - } - - Constraint fixed = NullConstraint; - - if(basic_movement < 0){ - Assert(d_variables.cmpAssignmentUpperBound(basic) > 0); - - if(proposal.unbounded() || d_variables.cmpToUpperBound(basic, proposedValue) <= 0){ - --dropped; - fixed = d_variables.getUpperBoundConstraint(basic); - } - }else if(basic_movement > 0){ - Assert(d_variables.cmpAssignmentLowerBound(basic) < 0); - - if(proposal.unbounded() || d_variables.cmpToLowerBound(basic, proposedValue) >= 0){ - --dropped; - fixed = d_variables.getLowerBoundConstraint(basic); - } - } - if(fixed != NullConstraint){ - DeltaRational amount = fixed->getValue() - d_variables.getAssignment(basic); - amount /= a_ji; - Assert(amount.sgn() == proposal.nonbasicDirection()); - - if(max.uninitialized()){ - max = UpdateInfo(proposal.nonbasic(), proposal.nonbasicDirection()); - max.updatePivot(amount, a_ji, fixed, dropped); - }else{ - int cmp = amount.cmp(max.nonbasicDelta()); - bool prefer = - (proposal.nonbasicDirection() < 0 && cmp < 0) || - (proposal.nonbasicDirection() > 0 && cmp > 0) || - (cmp == 0 && fixed->getVariable() < max.limiting()->getVariable()); - - if(prefer){ - max.updatePivot(amount, a_ji, fixed, dropped); - }else{ - max.setErrorsChange(dropped); - } - } - } - } - Assert(dropped < 0 || !proposal.unbounded()); - - if(dropped < 0){ - proposal = max; - }else{ - Assert(dropped == 0); - Assert(proposal.nonbasicDelta().sgn() != 0); - Assert(proposal.nonbasicDirection() != 0); - proposal.setErrorsChange(0); - } - Assert(proposal.errorsChange() == dropped); -} - ArithVar LinearEqualityModule::minBy(const ArithVarVec& vec, VarPreferenceFunction pf) const{ if(vec.empty()) { return ARITHVAR_SENTINEL; diff --git a/src/theory/arith/linear_equality.h b/src/theory/arith/linear_equality.h index 4d18d5c81..607ee6244 100644 --- a/src/theory/arith/linear_equality.h +++ b/src/theory/arith/linear_equality.h @@ -277,8 +277,6 @@ public: void includeBoundUpdate(ArithVar nb, const BoundsInfo& prev); - void computeSafeUpdate(UpdateInfo& inf, VarPreferenceFunction basic); - uint32_t updateProduct(const UpdateInfo& inf) const; @@ -400,16 +398,12 @@ public: } private: - typedef std::vector<const Tableau::Entry*> EntryPointerVector; - EntryPointerVector d_relevantErrorBuffer; - - //uint32_t computeUnconstrainedUpdate(ArithVar nb, int sgn, DeltaRational& am); - //uint32_t computedFixed(ArithVar nb, int sgn, const DeltaRational& am); - void computedFixed(UpdateInfo&); /** * This maps each row index to its relevant bounds info. - * This tracks the */ + * This tracks the count for how many variables on a row have bounds + * and how many are assigned at their bounds. + */ BoundInfoMap& d_btracking; bool d_areTracking; diff --git a/src/theory/arith/pure_update_simplex.cpp b/src/theory/arith/pure_update_simplex.cpp deleted file mode 100644 index 233fc292f..000000000 --- a/src/theory/arith/pure_update_simplex.cpp +++ /dev/null @@ -1,261 +0,0 @@ -/********************* */ -/*! \file simplex.cpp - ** \verbatim - ** Original author: taking - ** Major contributors: none - ** Minor contributors (to current version): mdeters - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief [[ Add one-line brief description here ]] - ** - ** [[ Add lengthier description here ]] - ** \todo document this file - **/ - - -#include "theory/arith/pure_update_simplex.h" -#include "theory/arith/options.h" -#include "theory/arith/constraint.h" - -using namespace std; - -namespace CVC4 { -namespace theory { -namespace arith { - -PureUpdateSimplexDecisionProcedure::PureUpdateSimplexDecisionProcedure(LinearEqualityModule& linEq, ErrorSet& errors, RaiseConflict conflictChannel, TempVarMalloc tvmalloc) - : SimplexDecisionProcedure(linEq, errors, conflictChannel, tvmalloc) -{ } - -Result::Sat PureUpdateSimplexDecisionProcedure::findModel(bool exactResult){ - Assert(d_conflictVariables.empty()); - - static CVC4_THREADLOCAL(unsigned int) instance = 0; - instance = instance + 1; - - if(d_errorSet.errorEmpty() && !d_errorSet.moreSignals()){ - Debug("arith::findModel") << "puFindModel("<< instance <<") " - << "trivial" << endl; - return Result::SAT; - } - - // We need to reduce this because of - d_errorSet.reduceToSignals(); - d_errorSet.setSelectionRule(VAR_ORDER); - - if(processSignals()){ - d_conflictVariables.purge(); - - Debug("arith::findModel") << "puFindModel("<< instance <<") " - << "early conflict" << endl; - return Result::UNSAT; - }else if(d_errorSet.errorEmpty()){ - Debug("arith::findModel") << "puFindModel("<< instance <<") " - << "fixed itself" << endl; - Assert(!d_errorSet.moreSignals()); - return Result::SAT; - } - - Debug("arith::findModel") << "puFindModel(" << instance <<") " - << "start non-trivial" << endl; - - static const bool verbose = false; - Result::Sat result = Result::SAT_UNKNOWN; - - if(result == Result::SAT_UNKNOWN){ - if(attemptPureUpdates()){ - result = Result::UNSAT; - } - if(result == Result::UNSAT){ - ++(d_statistics.d_pureUpdateFoundUnsat); - if(verbose){ Message() << "pure updates found unsat" << endl; } - }else if(d_errorSet.errorEmpty()){ - ++(d_statistics.d_pureUpdateFoundSat); - if(verbose){ Message() << "pure updates found model" << endl; } - }else{ - ++(d_statistics.d_pureUpdateMissed); - if(verbose){ Message() << "pure updates missed" << endl; } - } - } - - Assert(!d_errorSet.moreSignals()); - if(result == Result::SAT_UNKNOWN && d_errorSet.errorEmpty()){ - result = Result::SAT; - } - - // ensure that the conflict variable is still in the queue. - d_conflictVariables.purge(); - - Assert(d_focusErrorVar == ARITHVAR_SENTINEL); - Debug("arith::findModel") << "end findModel() " << instance << " " - << result << endl; - - return result; -} - - - -PureUpdateSimplexDecisionProcedure::Statistics::Statistics(): - d_pureUpdateFoundUnsat("theory::arith::PureUpdate::FoundUnsat", 0), - d_pureUpdateFoundSat("theory::arith::PureUpdate::FoundSat", 0), - d_pureUpdateMissed("theory::arith::PureUpdate::Missed", 0), - d_pureUpdates("theory::arith::PureUpdate::updates", 0), - d_pureUpdateDropped("theory::arith::PureUpdate::dropped", 0), - d_pureUpdateConflicts("theory::arith::PureUpdate::conflicts", 0), - d_foundConflicts("theory::arith::PureUpdate::foundConflicts", 0), - d_attemptPureUpdatesTimer("theory::arith::PureUpdate::timer"), - d_processSignalsTime("theory::arith::PureUpdate::process::timer"), - d_constructionTimer("theory::arith::PureUpdate::construction::timer") -{ - StatisticsRegistry::registerStat(&d_pureUpdateFoundUnsat); - StatisticsRegistry::registerStat(&d_pureUpdateFoundSat); - StatisticsRegistry::registerStat(&d_pureUpdateMissed); - StatisticsRegistry::registerStat(&d_pureUpdates); - StatisticsRegistry::registerStat(&d_pureUpdateDropped); - StatisticsRegistry::registerStat(&d_pureUpdateConflicts); - - StatisticsRegistry::registerStat(&d_foundConflicts); - - StatisticsRegistry::registerStat(&d_attemptPureUpdatesTimer); - StatisticsRegistry::registerStat(&d_processSignalsTime); - StatisticsRegistry::registerStat(&d_constructionTimer); -} - -PureUpdateSimplexDecisionProcedure::Statistics::~Statistics(){ - StatisticsRegistry::unregisterStat(&d_pureUpdateFoundUnsat); - StatisticsRegistry::unregisterStat(&d_pureUpdateFoundSat); - StatisticsRegistry::unregisterStat(&d_pureUpdateMissed); - StatisticsRegistry::unregisterStat(&d_pureUpdates); - StatisticsRegistry::unregisterStat(&d_pureUpdateDropped); - StatisticsRegistry::unregisterStat(&d_pureUpdateConflicts); - - StatisticsRegistry::unregisterStat(&d_foundConflicts); - - StatisticsRegistry::unregisterStat(&d_attemptPureUpdatesTimer); - StatisticsRegistry::unregisterStat(&d_processSignalsTime); - StatisticsRegistry::unregisterStat(&d_constructionTimer); -} - -bool PureUpdateSimplexDecisionProcedure::attemptPureUpdates(){ - TimerStat::CodeTimer codeTimer(d_statistics.d_attemptPureUpdatesTimer); - - Assert(!d_errorSet.focusEmpty()); - Assert(d_errorSet.noSignals()); - - d_focusErrorVar = constructInfeasiblityFunction(d_statistics.d_constructionTimer); - - UpdateInfo proposal; - int boundImprovements = 0; - int dropped = 0; - int computations = 0; - - for( Tableau::RowIterator ri = d_tableau.basicRowIterator(d_focusErrorVar); !ri.atEnd(); ++ri){ - const Tableau::Entry& e = *ri; - - ArithVar curr = e.getColVar(); - if(curr == d_focusErrorVar){ continue; } - - int dir = e.getCoefficient().sgn(); - Assert(dir != 0); - - bool worthwhile = false; - - if( (dir > 0 && d_variables.cmpAssignmentUpperBound(curr) < 0) || - (dir < 0 && d_variables.cmpAssignmentLowerBound(curr) > 0) ){ - - ++computations; - proposal = UpdateInfo(curr, dir); - d_linEq.computeSafeUpdate(proposal, &LinearEqualityModule::noPreference); - - Assert(proposal.errorsChange() <= 0); - Assert(proposal.focusDirection() >= 0); - - worthwhile = proposal.errorsChange() < 0 || - (proposal.focusDirection() > 0 && - d_variables.atBoundCounts(curr).isZero() && - !proposal.describesPivot()); - - Debug("pu::refined") - << "pure update proposal " - << curr << " " - << worthwhile << " " - << proposal - << endl; - } - if(worthwhile){ - Debug("pu") << d_variables.getAssignment(d_focusErrorVar) << endl; - - BoundCounts before = d_variables.atBoundCounts(curr); - DeltaRational newAssignment = - d_variables.getAssignment(curr) + proposal.nonbasicDelta(); - d_linEq.updateTracked(curr, newAssignment); - BoundCounts after = d_variables.atBoundCounts(curr); - - ++d_statistics.d_pureUpdates; - ++boundImprovements; - Debug("pu") << boundImprovements << ": " << curr - << " before: " << before - << " after: " << after - << e.getCoefficient() - << d_variables.getAssignment(d_focusErrorVar) << endl; - - uint32_t prevSize = d_errorSet.errorSize(); - Assert(d_errorSet.moreSignals()); - if(Debug.isOn("pu")){ d_errorSet.debugPrint(Debug("pu")); } - while(d_errorSet.moreSignals()){ - ArithVar updated = d_errorSet.topSignal(); - bool wasInError = d_errorSet.inError(updated); - d_errorSet.popSignal(); - if(updated == curr){ continue; } - Assert(d_tableau.isBasic(updated)); - if(!d_linEq.basicIsTracked(updated)){continue;} - - - Assert(d_linEq.basicIsTracked(updated)); - Assert(wasInError || d_variables.assignmentIsConsistent(updated)); - - if(!d_variables.assignmentIsConsistent(updated) - && checkBasicForConflict(updated)){ - Assert(!d_conflictVariables.isMember(updated) ); - Debug("pu") - << "It worked? " - << d_statistics.d_pureUpdateConflicts.getData() - << " " << curr - << " " << checkBasicForConflict(updated) << endl; - reportConflict(updated); - ++(d_statistics.d_foundConflicts); - ++(d_statistics.d_pureUpdateConflicts); - } - } - if(d_conflictVariables.empty()){ - if(Debug.isOn("pu")){ d_errorSet.debugPrint(Debug("pu")); } - uint32_t currSize = d_errorSet.errorSize(); - Assert(currSize <= prevSize); - if(currSize < prevSize){ - dropped+= prevSize - currSize; - if(currSize == 0){ - break; - } - } - }else{ - break; - } - } - } - - tearDownInfeasiblityFunction(d_statistics.d_constructionTimer, d_focusErrorVar); - d_focusErrorVar = ARITHVAR_SENTINEL; - - (d_statistics.d_pureUpdateDropped) += dropped; - - Assert(d_errorSet.noSignals()); - return !d_conflictVariables.empty(); -} - - -}/* CVC4::theory::arith namespace */ -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ diff --git a/src/theory/arith/pure_update_simplex.h b/src/theory/arith/pure_update_simplex.h deleted file mode 100644 index 50b751d7b..000000000 --- a/src/theory/arith/pure_update_simplex.h +++ /dev/null @@ -1,118 +0,0 @@ -/********************* */ -/*! \file simplex.h - ** \verbatim - ** Original author: taking - ** Major contributors: none - ** Minor contributors (to current version): kshitij, mdeters - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief This is an implementation of the Simplex Module for the Simplex for DPLL(T) - ** decision procedure. - ** - ** This implements the Simplex module for the Simpelx for DPLL(T) decision procedure. - ** See the Simplex for DPLL(T) technical report for more background.(citation?) - ** This shares with the theory a Tableau, and a PartialModel that: - ** - satisfies the equalities in the Tableau, and - ** - the assignment for the non-basic variables satisfies their bounds. - ** This is required to either produce a conflict or satisifying PartialModel. - ** Further, we require being told when a basic variable updates its value. - ** - ** During the Simplex search we maintain a queue of variables. - ** The queue is required to contain all of the basic variables that voilate their bounds. - ** As elimination from the queue is more efficient to be done lazily, - ** we do not maintain that the queue of variables needs to be only basic variables or only - ** variables that satisfy their bounds. - ** - ** The simplex procedure roughly follows Alberto's thesis. (citation?) - ** There is one round of selecting using a heuristic pivoting rule. (See PreferenceFunction - ** Documentation for the available options.) - ** The non-basic variable is the one that appears in the fewest pivots. (Bruno says that - ** Leonardo invented this first.) - ** After this, Bland's pivot rule is invoked. - ** - ** During this proccess, we periodically inspect the queue of variables to - ** 1) remove now extraneous extries, - ** 2) detect conflicts that are "waiting" on the queue but may not be detected by the - ** current queue heuristics, and - ** 3) detect multiple conflicts. - ** - ** Conflicts are greedily slackened to use the weakest bounds that still produce the - ** conflict. - ** - ** Extra things tracked atm: (Subject to change at Tim's whims) - ** - A superset of all of the newly pivoted variables. - ** - A queue of additional conflicts that were discovered by Simplex. - ** These are theory valid and are currently turned into lemmas - **/ - - -#include "cvc4_private.h" - -#pragma once - -#include "theory/arith/simplex.h" -#include "util/dense_map.h" -#include "util/statistics_registry.h" -#include <stdint.h> -#include "theory/arith/arithvar.h" -#include "theory/arith/delta_rational.h" - -namespace CVC4 { -namespace theory { -namespace arith { - -class PureUpdateSimplexDecisionProcedure : public SimplexDecisionProcedure{ -public: - PureUpdateSimplexDecisionProcedure(LinearEqualityModule& linEq, ErrorSet& errors, RaiseConflict conflictChannel, TempVarMalloc tvmalloc); - - Result::Sat findModel(bool exactResult); - -private: - ArithVar d_focusErrorVar; - - bool attemptPureUpdates(); - - /** - * This is the main simplex for DPLL(T) loop. - * It runs for at most maxIterations. - * - * Returns true iff it has found a conflict. - * d_conflictVariable will be set and the conflict for this row is reported. - */ - bool searchForFeasibleSolution(uint32_t maxIterations); - - bool processSignals(){ - TimerStat &timer = d_statistics.d_processSignalsTime; - IntStat& conflictStat = d_statistics.d_foundConflicts; - return standardProcessSignals(timer, conflictStat); - } - - /** These fields are designed to be accessible to TheoryArith methods. */ - class Statistics { - public: - IntStat d_pureUpdateFoundUnsat; - IntStat d_pureUpdateFoundSat; - IntStat d_pureUpdateMissed; - IntStat d_pureUpdates; - IntStat d_pureUpdateDropped; - IntStat d_pureUpdateConflicts; - - IntStat d_foundConflicts; - - TimerStat d_attemptPureUpdatesTimer; - TimerStat d_processSignalsTime; - - TimerStat d_constructionTimer; - - Statistics(); - ~Statistics(); - } d_statistics; -};/* class PureUpdateSimplexDecisionProcedure */ - -}/* CVC4::theory::arith namespace */ -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ - diff --git a/src/theory/arith/simplex-converge.cpp b/src/theory/arith/simplex-converge.cpp deleted file mode 100644 index decce3882..000000000 --- a/src/theory/arith/simplex-converge.cpp +++ /dev/null @@ -1,1674 +0,0 @@ -/********************* */ -/*! \file simplex.cpp - ** \verbatim - ** Original author: taking - ** Major contributors: none - ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief [[ Add one-line brief description here ]] - ** - ** [[ Add lengthier description here ]] - ** \todo document this file - **/ - - -#include "theory/arith/simplex.h" -#include "theory/arith/options.h" - -using namespace std; - -using namespace CVC4; -using namespace CVC4::kind; - -using namespace CVC4::theory; -using namespace CVC4::theory::arith; - -static const bool CHECK_AFTER_PIVOT = true; - -SimplexDecisionProcedure::SimplexDecisionProcedure(LinearEqualityModule& linEq, NodeCallBack& conflictChannel, ArithVarMalloc& malloc, ConstraintDatabase& cd) : - d_conflictVariable(ARITHVAR_SENTINEL), - d_linEq(linEq), - d_partialModel(d_linEq.getPartialModel()), - d_tableau(d_linEq.getTableau()), - d_queue(d_partialModel, d_tableau), - d_numVariables(0), - d_conflictChannel(conflictChannel), - d_pivotsInRound(), - d_DELTA_ZERO(0,0), - d_arithVarMalloc(malloc), - d_constraintDatabase(cd), - d_optRow(ARITHVAR_SENTINEL), - d_negOptConstant(d_DELTA_ZERO) -{ - switch(ArithHeuristicPivotRule rule = options::arithHeuristicPivotRule()) { - case MINIMUM: - d_queue.setPivotRule(ArithPriorityQueue::MINIMUM); - break; - case BREAK_TIES: - d_queue.setPivotRule(ArithPriorityQueue::BREAK_TIES); - break; - case MAXIMUM: - d_queue.setPivotRule(ArithPriorityQueue::MAXIMUM); - break; - default: - Unhandled(rule); - } - - srand(62047); -} - -SimplexDecisionProcedure::Statistics::Statistics(): - d_statUpdateConflicts("theory::arith::UpdateConflicts", 0), - d_findConflictOnTheQueueTime("theory::arith::findConflictOnTheQueueTime"), - d_attemptBeforeDiffSearch("theory::arith::qi::BeforeDiffSearch::attempt",0), - d_successBeforeDiffSearch("theory::arith::qi::BeforeDiffSearch::success",0), - d_attemptAfterDiffSearch("theory::arith::qi::AfterDiffSearch::attempt",0), - d_successAfterDiffSearch("theory::arith::qi::AfterDiffSearch::success",0), - d_attemptDuringDiffSearch("theory::arith::qi::DuringDiffSearch::attempt",0), - d_successDuringDiffSearch("theory::arith::qi::DuringDiffSearch::success",0), - d_attemptDuringVarOrderSearch("theory::arith::qi::DuringVarOrderSearch::attempt",0), - d_successDuringVarOrderSearch("theory::arith::qi::DuringVarOrderSearch::success",0), - d_attemptAfterVarOrderSearch("theory::arith::qi::AfterVarOrderSearch::attempt",0), - d_successAfterVarOrderSearch("theory::arith::qi::AfterVarOrderSearch::success",0), - d_weakeningAttempts("theory::arith::weakening::attempts",0), - d_weakeningSuccesses("theory::arith::weakening::success",0), - d_weakenings("theory::arith::weakening::total",0), - d_weakenTime("theory::arith::weakening::time"), - d_simplexConflicts("theory::arith::simplexConflicts",0), - // primal - d_primalTimer("theory::arith::primal::overall::timer"), - d_internalTimer("theory::arith::primal::internal::timer"), - d_primalCalls("theory::arith::primal::calls",0), - d_primalSatCalls("theory::arith::primal::calls::sat",0), - d_primalUnsatCalls("theory::arith::primal::calls::unsat",0), - d_primalPivots("theory::arith::primal::pivots",0), - d_primalImprovingPivots("theory::arith::primal::pivots::improving",0), - d_primalThresholdReachedPivot("theory::arith::primal::thresholds",0), - d_primalThresholdReachedPivot_dropped("theory::arith::primal::thresholds::dropped",0), - d_primalReachedMaxPivots("theory::arith::primal::maxpivots",0), - d_primalReachedMaxPivots_contractMadeProgress("theory::arith::primal::maxpivots::contract",0), - d_primalReachedMaxPivots_checkForConflictWorked("theory::arith::primal::maxpivots::checkworked",0), - d_primalGlobalMinimum("theory::arith::primal::minimum",0), - d_primalGlobalMinimum_rowConflictWorked("theory::arith::primal::minimum::checkworked",0), - d_primalGlobalMinimum_firstHalfWasSat("theory::arith::primal::minimum::firsthalf::sat",0), - d_primalGlobalMinimum_firstHalfWasUnsat("theory::arith::primal::minimum::firsthalf::unsat",0), - d_primalGlobalMinimum_contractMadeProgress("theory::arith::primal::minimum::progress",0), - d_unboundedFound("theory::arith::primal::unbounded",0), - d_unboundedFound_drive("theory::arith::primal::unbounded::drive",0), - d_unboundedFound_dropped("theory::arith::primal::unbounded::dropped",0) -{ - StatisticsRegistry::registerStat(&d_statUpdateConflicts); - - StatisticsRegistry::registerStat(&d_findConflictOnTheQueueTime); - - StatisticsRegistry::registerStat(&d_attemptBeforeDiffSearch); - StatisticsRegistry::registerStat(&d_successBeforeDiffSearch); - StatisticsRegistry::registerStat(&d_attemptAfterDiffSearch); - StatisticsRegistry::registerStat(&d_successAfterDiffSearch); - StatisticsRegistry::registerStat(&d_attemptDuringDiffSearch); - StatisticsRegistry::registerStat(&d_successDuringDiffSearch); - StatisticsRegistry::registerStat(&d_attemptDuringVarOrderSearch); - StatisticsRegistry::registerStat(&d_successDuringVarOrderSearch); - StatisticsRegistry::registerStat(&d_attemptAfterVarOrderSearch); - StatisticsRegistry::registerStat(&d_successAfterVarOrderSearch); - - StatisticsRegistry::registerStat(&d_weakeningAttempts); - StatisticsRegistry::registerStat(&d_weakeningSuccesses); - StatisticsRegistry::registerStat(&d_weakenings); - StatisticsRegistry::registerStat(&d_weakenTime); - - StatisticsRegistry::registerStat(&d_simplexConflicts); - - //primal - StatisticsRegistry::registerStat(&d_primalTimer); - StatisticsRegistry::registerStat(&d_internalTimer); - - StatisticsRegistry::registerStat(&d_primalCalls); - StatisticsRegistry::registerStat(&d_primalSatCalls); - StatisticsRegistry::registerStat(&d_primalUnsatCalls); - - StatisticsRegistry::registerStat(&d_primalPivots); - StatisticsRegistry::registerStat(&d_primalImprovingPivots); - - StatisticsRegistry::registerStat(&d_primalThresholdReachedPivot); - StatisticsRegistry::registerStat(&d_primalThresholdReachedPivot_dropped); - - StatisticsRegistry::registerStat(&d_primalReachedMaxPivots); - StatisticsRegistry::registerStat(&d_primalReachedMaxPivots_contractMadeProgress); - StatisticsRegistry::registerStat(&d_primalReachedMaxPivots_checkForConflictWorked); - - - StatisticsRegistry::registerStat(&d_primalGlobalMinimum); - StatisticsRegistry::registerStat(&d_primalGlobalMinimum_rowConflictWorked); - StatisticsRegistry::registerStat(&d_primalGlobalMinimum_firstHalfWasSat); - StatisticsRegistry::registerStat(&d_primalGlobalMinimum_firstHalfWasUnsat); - StatisticsRegistry::registerStat(&d_primalGlobalMinimum_contractMadeProgress); - - - StatisticsRegistry::registerStat(&d_unboundedFound); - StatisticsRegistry::registerStat(&d_unboundedFound_drive); - StatisticsRegistry::registerStat(&d_unboundedFound_dropped); - -} - -SimplexDecisionProcedure::Statistics::~Statistics(){ - StatisticsRegistry::unregisterStat(&d_statUpdateConflicts); - - StatisticsRegistry::unregisterStat(&d_findConflictOnTheQueueTime); - - StatisticsRegistry::unregisterStat(&d_attemptBeforeDiffSearch); - StatisticsRegistry::unregisterStat(&d_successBeforeDiffSearch); - StatisticsRegistry::unregisterStat(&d_attemptAfterDiffSearch); - StatisticsRegistry::unregisterStat(&d_successAfterDiffSearch); - StatisticsRegistry::unregisterStat(&d_attemptDuringDiffSearch); - StatisticsRegistry::unregisterStat(&d_successDuringDiffSearch); - StatisticsRegistry::unregisterStat(&d_attemptDuringVarOrderSearch); - StatisticsRegistry::unregisterStat(&d_successDuringVarOrderSearch); - StatisticsRegistry::unregisterStat(&d_attemptAfterVarOrderSearch); - StatisticsRegistry::unregisterStat(&d_successAfterVarOrderSearch); - - StatisticsRegistry::unregisterStat(&d_weakeningAttempts); - StatisticsRegistry::unregisterStat(&d_weakeningSuccesses); - StatisticsRegistry::unregisterStat(&d_weakenings); - StatisticsRegistry::unregisterStat(&d_weakenTime); - - StatisticsRegistry::unregisterStat(&d_simplexConflicts); - - //primal - StatisticsRegistry::unregisterStat(&d_primalTimer); - StatisticsRegistry::unregisterStat(&d_internalTimer); - - StatisticsRegistry::unregisterStat(&d_primalCalls); - StatisticsRegistry::unregisterStat(&d_primalSatCalls); - StatisticsRegistry::unregisterStat(&d_primalUnsatCalls); - - StatisticsRegistry::unregisterStat(&d_primalPivots); - StatisticsRegistry::unregisterStat(&d_primalImprovingPivots); - - StatisticsRegistry::unregisterStat(&d_primalThresholdReachedPivot); - StatisticsRegistry::unregisterStat(&d_primalThresholdReachedPivot_dropped); - - StatisticsRegistry::unregisterStat(&d_primalReachedMaxPivots); - StatisticsRegistry::unregisterStat(&d_primalReachedMaxPivots_contractMadeProgress); - StatisticsRegistry::unregisterStat(&d_primalReachedMaxPivots_checkForConflictWorked); - - - StatisticsRegistry::unregisterStat(&d_primalGlobalMinimum); - StatisticsRegistry::unregisterStat(&d_primalGlobalMinimum_rowConflictWorked); - StatisticsRegistry::unregisterStat(&d_primalGlobalMinimum_firstHalfWasSat); - StatisticsRegistry::unregisterStat(&d_primalGlobalMinimum_firstHalfWasUnsat); - StatisticsRegistry::unregisterStat(&d_primalGlobalMinimum_contractMadeProgress); - - StatisticsRegistry::unregisterStat(&d_unboundedFound); - StatisticsRegistry::unregisterStat(&d_unboundedFound_drive); - StatisticsRegistry::unregisterStat(&d_unboundedFound_dropped); -} - - - - -ArithVar SimplexDecisionProcedure::minVarOrder(const SimplexDecisionProcedure& simp, ArithVar x, ArithVar y){ - Assert(x != ARITHVAR_SENTINEL); - Assert(y != ARITHVAR_SENTINEL); - // Assert(!simp.d_tableau.isBasic(x)); - // Assert(!simp.d_tableau.isBasic(y)); - if(x <= y){ - return x; - } else { - return y; - } -} - -ArithVar SimplexDecisionProcedure::minColLength(const SimplexDecisionProcedure& simp, ArithVar x, ArithVar y){ - Assert(x != ARITHVAR_SENTINEL); - Assert(y != ARITHVAR_SENTINEL); - Assert(!simp.d_tableau.isBasic(x)); - Assert(!simp.d_tableau.isBasic(y)); - uint32_t xLen = simp.d_tableau.getColLength(x); - uint32_t yLen = simp.d_tableau.getColLength(y); - if( xLen > yLen){ - return y; - } else if( xLen== yLen ){ - return minVarOrder(simp,x,y); - }else{ - return x; - } -} - -ArithVar SimplexDecisionProcedure::minRowLength(const SimplexDecisionProcedure& simp, ArithVar x, ArithVar y){ - Assert(x != ARITHVAR_SENTINEL); - Assert(y != ARITHVAR_SENTINEL); - Assert(simp.d_tableau.isBasic(x)); - Assert(simp.d_tableau.isBasic(y)); - uint32_t xLen = simp.d_tableau.getRowLength(simp.d_tableau.basicToRowIndex(x)); - uint32_t yLen = simp.d_tableau.getRowLength(simp.d_tableau.basicToRowIndex(y)); - if( xLen > yLen){ - return y; - } else if( xLen == yLen ){ - return minVarOrder(simp,x,y); - }else{ - return x; - } -} -ArithVar SimplexDecisionProcedure::minBoundAndRowCount(const SimplexDecisionProcedure& simp, ArithVar x, ArithVar y){ - Assert(x != ARITHVAR_SENTINEL); - Assert(y != ARITHVAR_SENTINEL); - Assert(!simp.d_tableau.isBasic(x)); - Assert(!simp.d_tableau.isBasic(y)); - if(simp.d_partialModel.hasEitherBound(x) && !simp.d_partialModel.hasEitherBound(y)){ - return y; - }else if(!simp.d_partialModel.hasEitherBound(x) && simp.d_partialModel.hasEitherBound(y)){ - return x; - }else { - return minColLength(simp, x, y); - } -} - -template <bool above> -ArithVar SimplexDecisionProcedure::selectSlack(ArithVar x_i, SimplexDecisionProcedure::PreferenceFunction pref){ - ArithVar slack = ARITHVAR_SENTINEL; - - for(Tableau::RowIterator iter = d_tableau.basicRowIterator(x_i); !iter.atEnd(); ++iter){ - const Tableau::Entry& entry = *iter; - ArithVar nonbasic = entry.getColVar(); - if(nonbasic == x_i) continue; - - const Rational& a_ij = entry.getCoefficient(); - int sgn = a_ij.sgn(); - if(isAcceptableSlack<above>(sgn, nonbasic)){ - //If one of the above conditions is met, we have found an acceptable - //nonbasic variable to pivot x_i with. We can now choose which one we - //prefer the most. - slack = (slack == ARITHVAR_SENTINEL) ? nonbasic : pref(*this, slack, nonbasic); - } - } - - return slack; -} - -Node betterConflict(TNode x, TNode y){ - if(x.isNull()) return y; - else if(y.isNull()) return x; - else if(x.getNumChildren() <= y.getNumChildren()) return x; - else return y; -} - -bool SimplexDecisionProcedure::findConflictOnTheQueue(SearchPeriod type) { - TimerStat::CodeTimer codeTimer(d_statistics.d_findConflictOnTheQueueTime); - Assert(d_successes.empty()); - - switch(type){ - case BeforeDiffSearch: ++(d_statistics.d_attemptBeforeDiffSearch); break; - case DuringDiffSearch: ++(d_statistics.d_attemptDuringDiffSearch); break; - case AfterDiffSearch: ++(d_statistics.d_attemptAfterDiffSearch); break; - case DuringVarOrderSearch: ++(d_statistics.d_attemptDuringVarOrderSearch); break; - case AfterVarOrderSearch: ++(d_statistics.d_attemptAfterVarOrderSearch); break; - } - - ArithPriorityQueue::const_iterator i = d_queue.begin(); - ArithPriorityQueue::const_iterator end = d_queue.end(); - for(; i != end; ++i){ - ArithVar x_i = *i; - - if(x_i != d_conflictVariable && d_tableau.isBasic(x_i) && !d_successes.isMember(x_i)){ - Node possibleConflict = checkBasicForConflict(x_i); - if(!possibleConflict.isNull()){ - d_successes.add(x_i); - reportConflict(possibleConflict); - } - } - } - if(!d_successes.empty()){ - switch(type){ - case BeforeDiffSearch: ++(d_statistics.d_successBeforeDiffSearch); break; - case DuringDiffSearch: ++(d_statistics.d_successDuringDiffSearch); break; - case AfterDiffSearch: ++(d_statistics.d_successAfterDiffSearch); break; - case DuringVarOrderSearch: ++(d_statistics.d_successDuringVarOrderSearch); break; - case AfterVarOrderSearch: ++(d_statistics.d_successAfterVarOrderSearch); break; - } - d_successes.purge(); - return true; - }else{ - return false; - } -} - -Result::Sat SimplexDecisionProcedure::dualFindModel(bool exactResult){ - Assert(d_conflictVariable == ARITHVAR_SENTINEL); - Assert(d_queue.inCollectionMode()); - - if(d_queue.empty()){ - return Result::SAT; - } - static CVC4_THREADLOCAL(unsigned int) instance = 0; - instance = instance + 1; - Debug("arith::findModel") << "begin findModel()" << instance << endl; - - d_queue.transitionToDifferenceMode(); - - Result::Sat result = Result::SAT_UNKNOWN; - - if(d_queue.empty()){ - result = Result::SAT; - }else if(d_queue.size() > 1){ - if(findConflictOnTheQueue(BeforeDiffSearch)){ - result = Result::UNSAT; - } - } - static const bool verbose = false; - exactResult |= options::arithStandardCheckVarOrderPivots() < 0; - const uint32_t inexactResultsVarOrderPivots = exactResult ? 0 : options::arithStandardCheckVarOrderPivots(); - - uint32_t checkPeriod = options::arithSimplexCheckPeriod(); - if(result == Result::SAT_UNKNOWN){ - uint32_t numDifferencePivots = options::arithHeuristicPivots() < 0 ? - d_numVariables + 1 : options::arithHeuristicPivots(); - // The signed to unsigned conversion is safe. - uint32_t pivotsRemaining = numDifferencePivots; - while(!d_queue.empty() && - result != Result::UNSAT && - pivotsRemaining > 0){ - uint32_t pivotsToDo = min(checkPeriod, pivotsRemaining); - pivotsRemaining -= pivotsToDo; - if(searchForFeasibleSolution(pivotsToDo)){ - result = Result::UNSAT; - }//Once every CHECK_PERIOD examine the entire queue for conflicts - if(result != Result::UNSAT){ - if(findConflictOnTheQueue(DuringDiffSearch)) { result = Result::UNSAT; } - }else{ - findConflictOnTheQueue(AfterDiffSearch); // already unsat - } - } - - if(verbose && numDifferencePivots > 0){ - if(result == Result::UNSAT){ - Message() << "diff order found unsat" << endl; - }else if(d_queue.empty()){ - Message() << "diff order found model" << endl; - }else{ - Message() << "diff order missed" << endl; - } - } - } - - if(!d_queue.empty() && result != Result::UNSAT){ - if(exactResult){ - d_queue.transitionToVariableOrderMode(); - - while(!d_queue.empty() && result != Result::UNSAT){ - if(searchForFeasibleSolution(checkPeriod)){ - result = Result::UNSAT; - } - - //Once every CHECK_PERIOD examine the entire queue for conflicts - if(result != Result::UNSAT){ - if(findConflictOnTheQueue(DuringVarOrderSearch)){ - result = Result::UNSAT; - } - } else{ - findConflictOnTheQueue(AfterVarOrderSearch); - } - } - if(verbose){ - if(result == Result::UNSAT){ - Message() << "bland found unsat" << endl; - }else if(d_queue.empty()){ - Message() << "bland found model" << endl; - }else{ - Message() << "bland order missed" << endl; - } - } - }else{ - d_queue.transitionToVariableOrderMode(); - - if(searchForFeasibleSolution(inexactResultsVarOrderPivots)){ - result = Result::UNSAT; - findConflictOnTheQueue(AfterVarOrderSearch); // already unsat - }else{ - if(findConflictOnTheQueue(AfterVarOrderSearch)) { result = Result::UNSAT; } - } - - if(verbose){ - if(result == Result::UNSAT){ - Message() << "restricted var order found unsat" << endl; - }else if(d_queue.empty()){ - Message() << "restricted var order found model" << endl; - }else{ - Message() << "restricted var order missed" << endl; - } - } - } - } - - if(result == Result::SAT_UNKNOWN && d_queue.empty()){ - result = Result::SAT; - } - - - - d_pivotsInRound.purge(); - // ensure that the conflict variable is still in the queue. - if(d_conflictVariable != ARITHVAR_SENTINEL){ - d_queue.enqueueIfInconsistent(d_conflictVariable); - } - d_conflictVariable = ARITHVAR_SENTINEL; - - d_queue.transitionToCollectionMode(); - Assert(d_queue.inCollectionMode()); - Debug("arith::findModel") << "end findModel() " << instance << " " << result << endl; - return result; - - - // Assert(foundConflict || d_queue.empty()); - - // // Curiously the invariant that we always do a full check - // // means that the assignment we can always empty these queues. - // d_queue.clear(); - // d_pivotsInRound.purge(); - // d_conflictVariable = ARITHVAR_SENTINEL; - - // Assert(!d_queue.inCollectionMode()); - // d_queue.transitionToCollectionMode(); - - - // Assert(d_queue.inCollectionMode()); - - // Debug("arith::findModel") << "end findModel() " << instance << endl; - - // return foundConflict; -} - - - -Node SimplexDecisionProcedure::checkBasicForConflict(ArithVar basic){ - - Assert(d_tableau.isBasic(basic)); - const DeltaRational& beta = d_partialModel.getAssignment(basic); - - if(d_partialModel.strictlyLessThanLowerBound(basic, beta)){ - ArithVar x_j = selectSlackUpperBound(basic); - if(x_j == ARITHVAR_SENTINEL ){ - return generateConflictBelowLowerBound(basic); - } - }else if(d_partialModel.strictlyGreaterThanUpperBound(basic, beta)){ - ArithVar x_j = selectSlackLowerBound(basic); - if(x_j == ARITHVAR_SENTINEL ){ - return generateConflictAboveUpperBound(basic); - } - } - return Node::null(); -} - -//corresponds to Check() in dM06 -//template <SimplexDecisionProcedure::PreferenceFunction pf> -bool SimplexDecisionProcedure::searchForFeasibleSolution(uint32_t remainingIterations){ - Debug("arith") << "searchForFeasibleSolution" << endl; - Assert(remainingIterations > 0); - - while(remainingIterations > 0){ - if(Debug.isOn("paranoid:check_tableau")){ d_linEq.debugCheckTableau(); } - - ArithVar x_i = d_queue.dequeueInconsistentBasicVariable(); - Debug("arith::update::select") << "selectSmallestInconsistentVar()=" << x_i << endl; - if(x_i == ARITHVAR_SENTINEL){ - Debug("arith_update") << "No inconsistent variables" << endl; - return false; //sat - } - - --remainingIterations; - - bool useVarOrderPivot = d_pivotsInRound.count(x_i) >= options::arithPivotThreshold(); - if(!useVarOrderPivot){ - d_pivotsInRound.add(x_i); - } - - - Debug("playground") << "pivots in rounds: " << d_pivotsInRound.count(x_i) - << " use " << useVarOrderPivot - << " threshold " << options::arithPivotThreshold() - << endl; - - PreferenceFunction pf = useVarOrderPivot ? minVarOrder : minBoundAndRowCount; - - DeltaRational beta_i = d_partialModel.getAssignment(x_i); - ArithVar x_j = ARITHVAR_SENTINEL; - - if(d_partialModel.strictlyLessThanLowerBound(x_i, beta_i)){ - x_j = selectSlackUpperBound(x_i, pf); - if(x_j == ARITHVAR_SENTINEL ){ - ++(d_statistics.d_statUpdateConflicts); - Node conflict = generateConflictBelowLowerBound(x_i); //unsat - d_conflictVariable = x_i; - reportConflict(conflict); - return true; - } - DeltaRational l_i = d_partialModel.getLowerBound(x_i); - d_linEq.pivotAndUpdate(x_i, x_j, l_i); - - }else if(d_partialModel.strictlyGreaterThanUpperBound(x_i, beta_i)){ - x_j = selectSlackLowerBound(x_i, pf); - if(x_j == ARITHVAR_SENTINEL ){ - ++(d_statistics.d_statUpdateConflicts); - Node conflict = generateConflictAboveUpperBound(x_i); //unsat - - d_conflictVariable = x_i; - reportConflict(conflict); - return true; - } - DeltaRational u_i = d_partialModel.getUpperBound(x_i); - d_linEq.pivotAndUpdate(x_i, x_j, u_i); - } - Assert(x_j != ARITHVAR_SENTINEL); - - //Check to see if we already have a conflict with x_j to prevent wasteful work - if(CHECK_AFTER_PIVOT){ - Node possibleConflict = checkBasicForConflict(x_j); - if(!possibleConflict.isNull()){ - d_conflictVariable = x_j; - reportConflict(possibleConflict); - return true; // unsat - } - } - } - Assert(remainingIterations == 0); - - return false; -} - - - -Constraint SimplexDecisionProcedure::weakestExplanation(bool aboveUpper, DeltaRational& surplus, ArithVar v, const Rational& coeff, bool& anyWeakening, ArithVar basic){ - - int sgn = coeff.sgn(); - bool ub = aboveUpper?(sgn < 0) : (sgn > 0); - - Constraint c = ub ? - d_partialModel.getUpperBoundConstraint(v) : - d_partialModel.getLowerBoundConstraint(v); - -// #warning "revisit" -// Node exp = ub ? -// d_partialModel.explainUpperBound(v) : -// d_partialModel.explainLowerBound(v); - - bool weakened; - do{ - const DeltaRational& bound = c->getValue(); - - weakened = false; - - Constraint weaker = ub? - c->getStrictlyWeakerUpperBound(true, true): - c->getStrictlyWeakerLowerBound(true, true); - - // Node weaker = ub? - // d_propManager.strictlyWeakerAssertedUpperBound(v, bound): - // d_propManager.strictlyWeakerAssertedLowerBound(v, bound); - - if(weaker != NullConstraint){ - //if(!weaker.isNull()){ - const DeltaRational& weakerBound = weaker->getValue(); - //DeltaRational weakerBound = asDeltaRational(weaker); - - DeltaRational diff = aboveUpper ? bound - weakerBound : weakerBound - bound; - //if var == basic, - // if aboveUpper, weakerBound > bound, multiply by -1 - // if !aboveUpper, weakerBound < bound, multiply by -1 - diff = diff * coeff; - if(surplus > diff){ - ++d_statistics.d_weakenings; - weakened = true; - anyWeakening = true; - surplus = surplus - diff; - - Debug("weak") << "found:" << endl; - if(v == basic){ - Debug("weak") << " basic: "; - } - Debug("weak") << " " << surplus << " "<< diff << endl - << " " << bound << c << endl - << " " << weakerBound << weaker << endl; - - Assert(diff > d_DELTA_ZERO); - c = weaker; - } - } - }while(weakened); - - return c; -} - -Node SimplexDecisionProcedure::weakenConflict(bool aboveUpper, ArithVar basicVar){ - TimerStat::CodeTimer codeTimer(d_statistics.d_weakenTime); - - const DeltaRational& assignment = d_partialModel.getAssignment(basicVar); - DeltaRational surplus; - if(aboveUpper){ - Assert(d_partialModel.hasUpperBound(basicVar)); - Assert(assignment > d_partialModel.getUpperBound(basicVar)); - surplus = assignment - d_partialModel.getUpperBound(basicVar); - }else{ - Assert(d_partialModel.hasLowerBound(basicVar)); - Assert(assignment < d_partialModel.getLowerBound(basicVar)); - surplus = d_partialModel.getLowerBound(basicVar) - assignment; - } - - NodeBuilder<> conflict(kind::AND); - bool anyWeakenings = false; - for(Tableau::RowIterator i = d_tableau.basicRowIterator(basicVar); !i.atEnd(); ++i){ - const Tableau::Entry& entry = *i; - ArithVar v = entry.getColVar(); - const Rational& coeff = entry.getCoefficient(); - bool weakening = false; - Constraint c = weakestExplanation(aboveUpper, surplus, v, coeff, weakening, basicVar); - Debug("weak") << "weak : " << weakening << " " - << c->assertedToTheTheory() << " " - << d_partialModel.getAssignment(v) << " " - << c << endl - << c->explainForConflict() << endl; - anyWeakenings = anyWeakenings || weakening; - - Debug("weak") << "weak : " << c->explainForConflict() << endl; - c->explainForConflict(conflict); - } - ++d_statistics.d_weakeningAttempts; - if(anyWeakenings){ - ++d_statistics.d_weakeningSuccesses; - } - return conflict; -} - - -Node SimplexDecisionProcedure::generateConflictAboveUpperBound(ArithVar conflictVar){ - return weakenConflict(true, conflictVar); -} - -Node SimplexDecisionProcedure::generateConflictBelowLowerBound(ArithVar conflictVar){ - return weakenConflict(false, conflictVar); -} - - -// responses -// unbounded below(arithvar) -// reached threshold -// reached maxpivots -// reached GlobalMinimumd -// -SimplexDecisionProcedure::PrimalResponse SimplexDecisionProcedure::primal(uint32_t maxIterations) -{ - Assert(d_optRow != ARITHVAR_SENTINEL); - - for(uint32_t iteration = 0; iteration < maxIterations; iteration++){ - if(belowThreshold()){ - return ReachedThresholdValue; - } - - PrimalResponse res = primalCheck(); - switch(res){ - case GlobalMinimum: - case FoundUnboundedVariable: - return res; - case NoProgressOnLeaving: - ++d_statistics.d_primalPivots; - ++d_pivotsSinceOptProgress; - ++d_pivotsSinceLastCheck; - ++d_pivotsSinceErrorProgress; - - d_linEq.pivotAndUpdate(d_primalCarry.d_entering, d_primalCarry.d_leaving, d_partialModel.getAssignment(d_primalCarry.d_entering)); - - if(Debug.isOn("primal::tableau")){ - d_linEq.debugCheckTableau(); - } - if(Debug.isOn("primal::consistent")){ Assert(d_linEq.debugEntireLinEqIsConsistent("MakeProgressOnLeaving")); } - - break; - case MakeProgressOnLeaving: - { - ++d_statistics.d_primalPivots; - ++d_statistics.d_primalImprovingPivots; - - d_pivotsSinceOptProgress = 0; - ++d_pivotsSinceErrorProgress; - ++d_pivotsSinceLastCheck; - - d_linEq.pivotAndUpdate(d_primalCarry.d_entering, d_primalCarry.d_leaving, d_primalCarry.d_nextEnteringValue); - - static int helpful = 0; - static int hurtful = 0; - static int penguin = 0; - if(d_currentErrorVariables.isKey(d_primalCarry.d_entering)){ - cout << "entering is error " << d_primalCarry.d_entering; - if(d_currentErrorVariables[d_primalCarry.d_entering].errorIsLeqZero(d_partialModel)){ - cout << " now below threshold (" << (++helpful) << ") " << d_pivotsSinceErrorProgress << endl; - }else{ - cout << "ouch (" << (++hurtful) << ")"<< d_pivotsSinceErrorProgress << endl; - } - }else if(d_currentErrorVariables.isKey(d_primalCarry.d_leaving)){ - cout << "leaving is error " << d_primalCarry.d_leaving; - if(d_currentErrorVariables[d_primalCarry.d_leaving].errorIsLeqZero(d_partialModel)){ - cout << " now below threshold(" << (++helpful) << ")" << d_pivotsSinceErrorProgress << endl; - }else{ - cout << "ouch (" << (++hurtful) << ")" << d_pivotsSinceErrorProgress<< endl; - } - }else{ - cout << " penguin (" << (++penguin) << ")" << d_pivotsSinceErrorProgress<< endl; - } - - if(Debug.isOn("primal::tableau")){ - d_linEq.debugCheckTableau(); - } - if(Debug.isOn("primal::consistent")){ Assert(d_linEq.debugEntireLinEqIsConsistent("MakeProgressOnLeaving")); } - } - break; - default: - Unreachable(); - } - } - return UsedMaxPivots; -} - - -/** - * Error set - * ErrorVariable |-> {ErrorVariable, InputVariable, InputConstraint} - */ - -/** - * Returns SAT if it was able to satisfy all of the constraints in the error set - * Returns UNSAT if it was able to able to find an error - */ -Result::Sat SimplexDecisionProcedure::primalConverge(int depth){ - d_pivotsSinceLastCheck = 0; - - while(!d_currentErrorVariables.empty()){ - PrimalResponse res = primal(MAX_ITERATIONS - d_pivotsSinceLastCheck); - - switch(res){ - case FoundUnboundedVariable: - - // Drive the variable to at least 0 - // TODO This variable should be driven to a value that makes all of the error functions including it 0 - // It'll or another unbounded will be selected in the next round anyways so ignore for now. - ++d_statistics.d_unboundedFound; - if( !belowThreshold() ){ - driveOptToZero(d_primalCarry.d_unbounded); - d_linEq.debugCheckTableau(); - if(Debug.isOn("primal::consistent")){ Assert(d_linEq.debugEntireLinEqIsConsistent("primalConverge")); } - - ++d_statistics.d_unboundedFound_drive; - } - Assert(belowThreshold()); - { - uint32_t dropped = contractErrorVariables(true); - Debug("primal::converge") << "primalConverge -> FoundUnboundedVariable -> dropped " << dropped << " to " << d_currentErrorVariables.size() << endl; - d_statistics.d_unboundedFound_dropped += dropped; - } - break; - case ReachedThresholdValue: - ++d_statistics.d_primalThresholdReachedPivot; - - Assert(belowThreshold()); - { - uint32_t dropped = contractErrorVariables(true); - Debug("primal::converge") << "primalConverge -> ReachedThresholdValue -> dropped " << dropped << " to " << d_currentErrorVariables.size() << endl; - d_statistics.d_primalThresholdReachedPivot_dropped += dropped; - } - break; - case UsedMaxPivots: - { - d_pivotsSinceLastCheck = 0; - ++d_statistics.d_primalReachedMaxPivots; - - // periodically attempt to do the following : - // contract the error variable - // check for a conflict on an error variable - uint32_t dropped = contractErrorVariables(false); - - if( checkForRowConflicts() ){ // try to periodically look for a row - Debug("primal::converge") << "primalConverge -> UsedMaxPivots -> unsat " << endl; - - ++d_statistics.d_primalReachedMaxPivots_checkForConflictWorked; - return Result::UNSAT; // row conflicts are minimal so stop. - } - - if(dropped > 0){ - Debug("primal::converge") << "primalConverge -> UsedMaxPivots -> dropped " << dropped << " to " << d_currentErrorVariables.size() << endl; - ++d_statistics.d_primalReachedMaxPivots_contractMadeProgress; - }else{ - Debug("primal::converge") << "primalConverge -> UsedMaxPivots -> nothing " << endl; - } - } - break; - case GlobalMinimum: - ++d_statistics.d_primalGlobalMinimum; - - // If the minimum is positive, this is unsat. - // However, the optimization row is not necessarily a minimal conflict - if(!belowThreshold()){ - - if(d_currentErrorVariables.size() == 1){ - // The optimization function is exactly the same as the last remaining variable - // The conflict for the row is the same as the conflict for the optimization function. - bool foundConflict = checkForRowConflicts(); - Assert(foundConflict); - Debug("primal::converge") << "primalConverge -> GlobalMinimum -> one variable" << endl; - - return Result::UNSAT; - }else{ - // There are at least 2 error variables. - // Look for a minimal conflict - - - if(checkForRowConflicts() ){ - Debug("primal::converge") << "primalConverge -> GlobalMinimum -> postitive -> rowconflict " << endl; - - ++d_statistics.d_primalGlobalMinimum_rowConflictWorked; - return Result::UNSAT; - } - - uint32_t dropped = contractErrorVariables(false); - - Debug("primal::converge") << "primalConverge -> GlobalMinimum -> postitive -> dropped " << dropped << " to " << d_currentErrorVariables.size() << endl; - if(dropped > 0){ - ++d_statistics.d_primalGlobalMinimum_contractMadeProgress; - } - - ErrorMap half; - d_currentErrorVariables.splitInto(half); - - Debug("primal::converge") << "primalConverge -> GlobalMinimum -> recursion " << depth << endl; - - - reconstructOptimizationFunction(); - Result::Sat resultOnRemaining = primalConverge(depth + 1); - - if(resultOnRemaining == Result::UNSAT){ - Debug("primal::converge") << "primalConverge -> GlobalMinimum -> recursion " << depth << " was unsat " << endl; - ++d_statistics.d_primalGlobalMinimum_firstHalfWasUnsat; - restoreErrorVariables(half); - return Result::UNSAT; - }else{ - ++d_statistics.d_primalGlobalMinimum_firstHalfWasSat; - Debug("primal::converge") << "primalConverge -> GlobalMinimum -> recursion " << depth << " was sat " << endl; - - Assert(resultOnRemaining == Result::SAT); - Assert(d_currentErrorVariables.empty()); - d_currentErrorVariables.addAll(half); - reconstructOptimizationFunction(); - return primalConverge(depth + 1); - } - } - - }else{ - - // if the optimum is <= 0 - // drop all of the satisfied variables and continue; - uint32_t dropped = contractErrorVariables(true); - Debug("primal::converge") << "primalConverge -> GlobalMinimum -> negative -> dropped "<< dropped << " to " << d_currentErrorVariables.size() << endl; - - ++d_statistics.d_primalGlobalMinimum_contractMadeProgress; - } - break; - default: - Unreachable(); - } - } - - return Result::SAT; -} - - -Result::Sat SimplexDecisionProcedure::primalFindModel(){ - Assert(d_primalCarry.isClear()); - - // Reduce the queue to only contain violations - reduceQueue(); - - if(d_queue.empty()){ - return Result::SAT; - } - TimerStat::CodeTimer codeTimer(d_statistics.d_primalTimer); - - ++d_statistics.d_primalCalls; - - Debug("primalFindModel") << "primalFindModel() begin" << endl; - - const int PAUSE_RATE = 100; - if(Debug.isOn("primal::pause") && d_statistics.d_primalCalls.getData() % PAUSE_RATE == 0){ - Debug("primal::pause") << "waiting for input: "; - std::string dummy; - std::getline(std::cin, dummy); - } - - // TODO restore the tableau by ejecting variables - // Tableau copy(d_tableau); - - Result::Sat answer; - { - TimerStat::CodeTimer codeTimer(d_statistics.d_internalTimer); - - // This is needed because of the fiddling with the partial model - //context::Context::ScopedPush speculativePush(satContext); - - constructErrorVariables(); - constructOptimizationFunction(); - if(Debug.isOn("primal::tableau")){ d_linEq.debugCheckTableau(); } - if(Debug.isOn("primal::consistent")){ d_linEq.debugEntireLinEqIsConsistent("primalFindModel 1"); } - answer = primalConverge(0); - } - removeOptimizationFunction(); - - - // exit - uint32_t nc = d_tableau.getNumColumns(); - //d_tableau = copy; - while(d_tableau.getNumColumns() < nc){ - d_tableau.increaseSize(); - } - restoreErrorVariables(d_currentErrorVariables); - - reduceQueue(); - - if(Debug.isOn("primal::tableau")){ d_linEq.debugCheckTableau(); } - - if(Debug.isOn("primal::consistent")){ d_linEq.debugEntireLinEqIsConsistent("primalFindModel2"); } - Debug("primalFindModel") << "primalFindModel() end " << answer << endl; - - // The set of variables in conflict with their bounds will still be a subset of the - // variables that are in conflict with their bounds in the beginning. - // The basic variables are the same because of the copy. - // Thus it is safe to not try to not recompute the queue of violating variables - - if(answer == Result::UNSAT){ - // This needs to be done in a different context level than the push - ++d_statistics.d_primalUnsatCalls; - }else{ - ++d_statistics.d_primalSatCalls; - } - - d_primalCarry.clear(); - - return answer; -} - -/** Clears the ErrorMap and relase the resources associated with it. - * There are a couple of error maps around - */ -void SimplexDecisionProcedure::restoreErrorVariables(SimplexDecisionProcedure::ErrorMap& es){ - while(!es.empty()){ - ArithVar e = es.back(); - - reassertErrorConstraint(e, es, false, false); - es.pop_back(); - } -} - -void SimplexDecisionProcedure::constructErrorVariables(){ - Assert(d_currentErrorVariables.empty()); - Assert(!d_queue.empty()); - - for(ArithPriorityQueue::const_iterator iter = d_queue.begin(), end = d_queue.end(); iter != end; ++iter){ - ArithVar input = *iter; - - Assert(d_tableau.isBasic(input)); - Assert(!d_partialModel.assignmentIsConsistent(input)); - - Assert(!d_currentErrorVariables.isKey(input)); - - bool ub = d_partialModel.strictlyGreaterThanUpperBound(input, d_partialModel.getAssignment(input)); - - Constraint original = ub ? d_partialModel.getUpperBoundConstraint(input) - : d_partialModel.getLowerBoundConstraint(input); - - d_currentErrorVariables.set(input, ErrorInfo(input, ub, original)); - - if(ub){ - d_partialModel.forceRelaxUpperBound(input); - }else{ - d_partialModel.forceRelaxLowerBound(input); - } - Debug("primal") << "adding error variable (" << input << ", " << ", " << original <<") "; - Debug("primal") << "ub "<< ub << " " << d_partialModel.getAssignment(input) << " " << original->getValue() <<")" << endl; - d_currentErrorVariables.set(input, ErrorInfo(input, ub, original)); - - // Constraint boundIsValue = d_constraintDatabase.getConstraint(bound, Equality, original->getValue()); - // boundIsValue->setPsuedoConstraint(); - - // d_partialModel.setAssignment(bound, boundIsValue->getValue()); - // d_partialModel.setUpperBoundConstraint(boundIsValue); - // d_partialModel.setLowerBoundConstraint(boundIsValue); - - // // if ub - // // then error = x - boundIsValue - // // else error = boundIsValue - x - - // ArithVar error = requestVariable(); - - // DeltaRational diff = ub ? - // d_partialModel.getAssignment(input) - boundIsValue->getValue() : - // boundIsValue->getValue() - d_partialModel.getAssignment(input); - - // d_partialModel.setAssignment(error, diff); - - // vector<Rational> coeffs; - // vector<ArithVar> variables; - // variables.push_back(input); - // coeffs.push_back(ub ? Rational(1) : Rational(-1)); - // variables.push_back(bound); - // coeffs.push_back(ub ? Rational(-1) : Rational(1)); - - // d_tableau.addRow(error, coeffs, variables); - - - } - - if(Debug.isOn("primal::tableau")){ d_linEq.debugCheckTableau(); } - if(Debug.isOn("primal::consistent")){ d_linEq.debugEntireLinEqIsConsistent("constructErrorVariables");} - Assert(!d_currentErrorVariables.empty()); -} - - - -/** Returns true if it has found a row conflict for any of the error variables. */ -bool SimplexDecisionProcedure::checkForRowConflicts(){ - vector<ArithVar> inConflict; - for(ErrorMap::const_iterator iter = d_currentErrorVariables.begin(), end = d_currentErrorVariables.end(); iter != end; ++iter){ - ArithVar error = *iter; - const ErrorInfo& info = d_currentErrorVariables[error]; - if(d_tableau.isBasic(error) && !info.errorIsLeqZero(d_partialModel)){ - - ArithVar x_j = info.isUpperbound() ? - selectSlackLowerBound(error) : - selectSlackUpperBound(error); - - if(x_j == ARITHVAR_SENTINEL ){ - inConflict.push_back(error); - } - } - } - - if(!inConflict.empty()){ - while(!inConflict.empty()){ - ArithVar error = inConflict.back(); - inConflict.pop_back(); - - reassertErrorConstraint(error, d_currentErrorVariables, false, true); - - Node conflict = d_currentErrorVariables[error].isUpperbound() ? - generateConflictAboveUpperBound(error) : - generateConflictBelowLowerBound(error); - Assert(!conflict.isNull()); - - d_currentErrorVariables.remove(error); - - reportConflict(conflict); - } - reconstructOptimizationFunction(); - return true; - }else{ - return false; - } -} - -void SimplexDecisionProcedure::reassertErrorConstraint(ArithVar e, SimplexDecisionProcedure::ErrorMap& es, bool definitelyTrue, bool definitelyFalse){ - Assert(es.isKey(e)); - const ErrorInfo& info = es.get(e); - Constraint original = info.getConstraint(); - - if(info.isUpperbound()){ - d_partialModel.setUpperBoundConstraint(original); - }else if(original->isLowerBound()){ - d_partialModel.setLowerBoundConstraint(original); - } - - Assert(!definitelyTrue || d_partialModel.assignmentIsConsistent(e)); - Assert(!definitelyFalse || !d_partialModel.assignmentIsConsistent(e)); -} - -uint32_t SimplexDecisionProcedure::contractErrorVariables(bool guaranteedSuccess){ - uint32_t entrySize = d_currentErrorVariables.size(); - Debug("primal::contract") << "contractErrorVariables() begin : " << d_currentErrorVariables.size() << endl; - - std::vector<ArithVar> toRemove; - for(ErrorMap::const_iterator iter = d_currentErrorVariables.begin(), end = d_currentErrorVariables.end(); iter != end; ++iter){ - ArithVar e = *iter; - if(d_currentErrorVariables[e].errorIsLeqZero(d_partialModel)){ - toRemove.push_back(e); - } - } - - Assert(!guaranteedSuccess || !toRemove.empty()); - - if(!toRemove.empty()){ - while(!toRemove.empty()){ - ArithVar e = toRemove.back(); - toRemove.pop_back(); - reassertErrorConstraint(e, d_currentErrorVariables, true, false); - d_currentErrorVariables.remove(e); - } - - reconstructOptimizationFunction(); - } - - Debug("primal::contract") << "contractErrorVariables() end : " << d_currentErrorVariables.size() << endl; - - uint32_t exitSize = d_currentErrorVariables.size(); - - Assert(exitSize <= entrySize); - Assert(!guaranteedSuccess|| exitSize < entrySize); - return entrySize - exitSize; -} - -void SimplexDecisionProcedure::removeOptimizationFunction(){ - Assert(d_optRow != ARITHVAR_SENTINEL); - Assert(d_tableau.isBasic(d_optRow)); - - d_tableau.removeBasicRow(d_optRow); - releaseVariable(d_optRow); - - d_optRow = ARITHVAR_SENTINEL; - d_negOptConstant = d_DELTA_ZERO; - - Assert(d_optRow == ARITHVAR_SENTINEL); -} - -void SimplexDecisionProcedure::constructOptimizationFunction(){ - Assert(d_optRow == ARITHVAR_SENTINEL); - Assert(d_negOptConstant == d_DELTA_ZERO); - - d_optRow = requestVariable(); - - - std::vector<Rational> coeffs; - std::vector<ArithVar> variables; - for(ErrorMap::const_iterator iter = d_currentErrorVariables.begin(), end = d_currentErrorVariables.end(); iter != end; ++iter){ - ArithVar e = *iter; - - if(d_currentErrorVariables[e].isUpperbound()){ - coeffs.push_back(Rational(1)); - variables.push_back(e); - d_negOptConstant = d_negOptConstant + (d_currentErrorVariables[e].getConstraint()->getValue()); - }else{ - coeffs.push_back(Rational(-1)); - variables.push_back(e); - d_negOptConstant = d_negOptConstant - (d_currentErrorVariables[e].getConstraint()->getValue()); - } - } - d_tableau.addRow(d_optRow, coeffs, variables); - - DeltaRational newAssignment = d_linEq.computeRowValue(d_optRow, false); - d_partialModel.setAssignment(d_optRow, newAssignment); - - if(Debug.isOn("primal::tableau")){ d_linEq.debugCheckTableau(); } - - - if(Debug.isOn("primal::consistent")){ - d_linEq.debugEntireLinEqIsConsistent("constructOptimizationFunction"); - } - - d_pivotsSinceOptProgress = 0; - d_pivotsSinceErrorProgress = 0; - - Assert(d_optRow != ARITHVAR_SENTINEL); -} - -void SimplexDecisionProcedure::reconstructOptimizationFunction(){ - removeOptimizationFunction(); - constructOptimizationFunction(); -} - - - -/* TODO: - * Very naive implementation. Recomputes everything every time. - * Currently looks for the variable that can decrease the optimization function the most. - * - */ -SimplexDecisionProcedure::PrimalResponse SimplexDecisionProcedure::primalCheck() -{ - Debug("primal") << "primalCheck() begin" << endl; - - ArithVar leaving = ARITHVAR_SENTINEL; - ArithVar entering = ARITHVAR_SENTINEL; - DeltaRational leavingShift = d_DELTA_ZERO; // The amount the leaving variable can change by without making the tableau inconsistent - DeltaRational leavingDelta = d_DELTA_ZERO; // The amount the optimization function changes by selecting leaving - - Assert(d_improvementCandidates.empty()); - - for( Tableau::RowIterator ri = d_tableau.basicRowIterator(d_optRow); !ri.atEnd(); ++ri){ - const Tableau::Entry& e = *ri; - - ArithVar curr = e.getColVar(); - if(curr == d_optRow){ continue; } - - - int sgn = e.getCoefficient().sgn(); - Assert(sgn != 0); - if( (sgn < 0 && d_partialModel.strictlyBelowUpperBound(curr)) || - (sgn > 0 && d_partialModel.strictlyAboveLowerBound(curr)) ){ - - d_improvementCandidates.push_back(&e); - } - } - - if(d_improvementCandidates.empty()){ - Debug("primal") << "primalCheck() end : global" << endl; - return GlobalMinimum; // No variable in the optimization function can be improved - } - - DeltaRational minimumShift; - DeltaRational currShift; - for(EntryVector::const_iterator ci = d_improvementCandidates.begin(), end_ci = d_improvementCandidates.end(); ci != end_ci; ++ci){ - const Tableau::Entry& e = *(*ci); - ArithVar curr = e.getColVar(); - - ArithVar currEntering; - bool progress; - - minimumShift = (leaving == ARITHVAR_SENTINEL ) ? leavingDelta/(e.getCoefficient().abs()) : d_DELTA_ZERO; - int sgn = e.getCoefficient().sgn(); - computeShift(curr, sgn < 0, progress, currEntering, currShift, minimumShift); - - if(currEntering == ARITHVAR_SENTINEL){ - d_improvementCandidates.clear(); - - Debug("primal") << "primalCheck() end : unbounded" << endl; - d_primalCarry.d_unbounded = curr; - return FoundUnboundedVariable; - }else if(progress) { - leaving = curr; - leavingShift = currShift; - leavingDelta = currShift * e.getCoefficient(); - entering = currEntering; - - Assert(leavingDelta < d_DELTA_ZERO); - - const int RECHECK_PERIOD = 10; - if(d_pivotsSinceErrorProgress % RECHECK_PERIOD != 0){ - // we can make progress, stop - break; - } - } - } - - if(leaving == ARITHVAR_SENTINEL){ - cout << "Nothing can make progress " << endl; - - const uint32_t THRESHOLD = 20; - if(d_pivotsSinceOptProgress <= THRESHOLD){ - - int index = rand() % d_improvementCandidates.size(); - leaving = (*d_improvementCandidates[index]).getColVar(); - entering = selectFirstValid(leaving, (*d_improvementCandidates[index]).getCoefficient().sgn() < 0); - }else{ // Bland's rule - bool increasing; - for(EntryVector::const_iterator ci = d_improvementCandidates.begin(), end_ci = d_improvementCandidates.end(); ci != end_ci; ++ci){ - const Tableau::Entry& e = *(*ci); - ArithVar curr = e.getColVar(); - leaving = (leaving == ARITHVAR_SENTINEL) ? curr : minVarOrder(*this, curr, leaving); - if(leaving == curr){ - increasing = (e.getCoefficient().sgn() < 0); - } - } - - entering = selectMinimumValid(leaving, increasing); - } - Assert(leaving != ARITHVAR_SENTINEL); - Assert(entering != ARITHVAR_SENTINEL); - - d_primalCarry.d_leaving = leaving; - d_primalCarry.d_entering = entering; - - d_primalCarry.d_nextEnteringValue = d_partialModel.getAssignment(entering); - - Debug("primal") << "primalCheck() end : no progress made " << leaving << " to " << entering << " (" << d_pivotsSinceOptProgress << ")"<< endl; - d_improvementCandidates.clear(); - return NoProgressOnLeaving; - }else{ - const Tableau::Entry& enterLeavingEntry = d_tableau.findEntry(d_tableau.basicToRowIndex(entering), leaving); - Assert(!enterLeavingEntry.blank()); - - d_primalCarry.d_leaving = leaving; - d_primalCarry.d_entering = entering; - d_primalCarry.d_nextEnteringValue = d_partialModel.getAssignment(entering) - + leavingShift * enterLeavingEntry.getCoefficient(); - - Debug("primal") << "primalCheck() end : progress" << endl - << leaving << " to " << entering << " ~ " - << d_partialModel.getAssignment(leaving) << " ~ " << leavingShift - << " ~ " << enterLeavingEntry.getCoefficient() - << " ~ " << d_primalCarry.d_nextEnteringValue << endl; - - d_improvementCandidates.clear(); - return MakeProgressOnLeaving; - } - - // anyProgress = true; - - // DeltaRational currDelta = currShift * e.getCoefficient(); - - // int cmp = currDelta.cmp(leavingDelta); - - // // Cases: - // // 1) No candidate yet, - // // 2) there is a candidate with a strictly better update, or - // // 3) there is a candidate with the same update value that has a smaller value in the variable ordering. - // // - // // Case 3 covers Bland's rule. - // if(entering == ARITHVAR_SENTINEL || cmp < 0){ - // leaving = curr; - // }else if( cmp == 0 ){ - // leaving = minVarOrder(*this, curr, leaving); - // } - - // if(leaving == curr){ - // leavingShift = currShift; - // leavingDelta = currDelta; - // entering = currEntering; - // } - // } - // } - - // if(leaving == ARITHVAR_SENTINEL){ - // Debug("primal") << "primalCheck() end : global" << endl; - // return GlobalMinimum; // No variable in the optimization function can be improved - // }else{ - // const Tableau::Entry& enterLeavingEntry = d_tableau.findEntry(d_tableau.basicToRowIndex(entering), leaving); - // Assert(!enterLeavingEntry.blank()); - - // d_primalCarry.d_leaving = leaving; - // d_primalCarry.d_entering = entering; - // d_primalCarry.d_nextEnteringValue = d_partialModel.getAssignment(entering) - // + leavingShift * enterLeavingEntry.getCoefficient(); - - // Debug("primal") << "primalCheck() end : progress" << endl - // << leaving << " to " << entering << " ~ " - // << d_partialModel.getAssignment(leaving) << " ~ " << leavingShift - // << " ~ " << enterLeavingEntry.getCoefficient() - // << " ~ " << d_primalCarry.d_nextEnteringValue << endl; - // return MakeProgressOnLeaving; - // } -} - -ArithVar SimplexDecisionProcedure::selectMinimumValid(ArithVar v, bool increasing){ - ArithVar minimum = ARITHVAR_SENTINEL; - for(Tableau::ColIterator colIter = d_tableau.colIterator(v);!colIter.atEnd(); ++colIter){ - const Tableau::Entry& e = *colIter; - ArithVar basic = d_tableau.rowIndexToBasic(e.getRowIndex()); - if(basic == d_optRow) continue; - - - int esgn = e.getCoefficient().sgn(); - bool basicInc = (increasing == (esgn > 0)); - - if(!(basicInc ? d_partialModel.strictlyBelowUpperBound(basic) : - d_partialModel.strictlyAboveLowerBound(basic))){ - if(minimum == ARITHVAR_SENTINEL){ - minimum = basic; - }else{ - minimum = minVarOrder(*this, basic, minimum); - } - } - } - return minimum; -} - -ArithVar SimplexDecisionProcedure::selectFirstValid(ArithVar v, bool increasing){ - ArithVar minimum = ARITHVAR_SENTINEL; - - for(Tableau::ColIterator colIter = d_tableau.colIterator(v);!colIter.atEnd(); ++colIter){ - const Tableau::Entry& e = *colIter; - ArithVar basic = d_tableau.rowIndexToBasic(e.getRowIndex()); - if(basic == d_optRow) continue; - - int esgn = e.getCoefficient().sgn(); - bool basicInc = (increasing == (esgn > 0)); - - if(!(basicInc ? d_partialModel.strictlyBelowUpperBound(basic) : - d_partialModel.strictlyAboveLowerBound(basic))){ - if(minimum == ARITHVAR_SENTINEL){ - minimum = basic; - }else{ - minimum = minRowLength(*this, basic, minimum); - } - } - } - return minimum; -} - - - -void SimplexDecisionProcedure::computeShift(ArithVar leaving, bool increasing, bool& progress, ArithVar& entering, DeltaRational& shift, const DeltaRational& minimumShift){ - Assert(increasing ? (minimumShift >= d_DELTA_ZERO) : (minimumShift <= d_DELTA_ZERO) ); - - static int instance = 0; - Debug("primal") << "computeshift " << ++instance << " " << leaving << endl; - - // The selection for the leaving variable - entering = ARITHVAR_SENTINEL; - - // no progress is initially made - progress = false; - - bool bounded = false; - - if(increasing ? d_partialModel.hasUpperBound(leaving) : d_partialModel.hasLowerBound(leaving)){ - const DeltaRational& assignment = d_partialModel.getAssignment(leaving); - - bounded = true; - - DeltaRational diff = increasing ? d_partialModel.getUpperBound(leaving) - assignment : d_partialModel.getLowerBound(leaving) - assignment; - Assert(increasing ? diff.sgn() >=0 : diff.sgn() <= 0); - if((increasing) ? (diff < minimumShift) : ( diff > minimumShift)){ - Assert(!progress); - entering = leaving; // My my my, what an ugly hack - return; // no progress is possible stop - } - } - - // shift has a meaningful value once entering has a meaningful value - // if increasing, - // then shift > minimumShift >= 0 - // else shift < minimumShift <= 0 - // - // Maintain the following invariant: - // - // if increasing, - // if e_ij > 0, diff >= shift > minimumShift >= 0 - // if e_ij < 0, diff >= shift > minimumShift >= 0 - // if !increasing, - // if e_ij > 0, diff <= shift < minimumShift <= 0 - // if e_ij < 0, diff <= shift < minimumShift <= 0 - // if increasing == (e_ij > 0), diff = (d_partialModel.getUpperBound(basic) - d_partialModel.getAssignment(basic)) / e.getCoefficient() - // if increasing != (e_ij > 0), diff = (d_partialModel.getLowerBound(basic) - d_partialModel.getAssignment(basic)) / e.getCoefficient() - - for(Tableau::ColIterator colIter = d_tableau.colIterator(leaving);!colIter.atEnd(); ++colIter){ - const Tableau::Entry& e = *colIter; - - ArithVar basic = d_tableau.rowIndexToBasic(e.getRowIndex()); - if(basic == d_optRow) continue; - - int esgn = e.getCoefficient().sgn(); - bool basicInc = (increasing == (esgn > 0)); - // If both are true, increasing the variable entering increases the basic variable - // If both are false, the entering variable is decreasing, but the coefficient is negative and the basic variable is increasing - // If exactly one is false, the basic variable is decreasing. - - Debug("primal::shift") << basic << " " << d_partialModel.hasUpperBound(basic) << " " - << d_partialModel.hasLowerBound(basic) << " " - << e.getCoefficient() << endl; - - if( (basicInc && d_partialModel.hasUpperBound(basic))|| - (!basicInc && d_partialModel.hasLowerBound(basic))){ - - if(!(basicInc ? d_partialModel.strictlyBelowUpperBound(basic) : - d_partialModel.strictlyAboveLowerBound(basic))){ - // diff == 0, as diff > minimumShift >= 0 or diff < minimumShift <= 0 - Assert(!progress); - entering = basic; - return; - }else{ - DeltaRational diff = basicInc ? - (d_partialModel.getUpperBound(basic) - d_partialModel.getAssignment(basic)) / e.getCoefficient() : - (d_partialModel.getLowerBound(basic) - d_partialModel.getAssignment(basic)) / e.getCoefficient(); - - if( entering == ARITHVAR_SENTINEL ){ - if(increasing ? (diff <= minimumShift) : (diff >= minimumShift)){ - Assert(!progress); - entering = basic; - return; - }else{ - Assert(increasing ? (diff > minimumShift) : (diff < minimumShift)); - shift = diff; - entering = basic; - bounded = true; - } - }else{ - if( increasing ? (diff < shift) : diff > shift){ - // a new min for increasing - // a new max for decreasing - - if(increasing ? (diff <= minimumShift) : (diff >= minimumShift)){ - Assert(!progress); - entering = basic; - return; - }else{ - Assert(increasing ? (diff > minimumShift) : (diff < minimumShift)); - shift = diff; - entering = basic; - } - } - } - } - } - } - - if(!bounded){ - // A totally unbounded variable - Assert(entering == ARITHVAR_SENTINEL); - progress = true; - return; - }else if(entering == ARITHVAR_SENTINEL){ - // We have a variable that is bounded only by its maximum - for(Tableau::ColIterator colIter = d_tableau.colIterator(leaving);!colIter.atEnd(); ++colIter){ - const Tableau::Entry& e = *colIter; - - ArithVar basic = d_tableau.rowIndexToBasic(e.getRowIndex()); - if(basic == d_optRow){ - continue; - } else{ - entering = basic; - break; - } - } - Assert(entering != ARITHVAR_SENTINEL); - - Assert(increasing ? d_partialModel.hasUpperBound(leaving) : d_partialModel.hasLowerBound(leaving)); - - const DeltaRational& assignment = d_partialModel.getAssignment(leaving); - DeltaRational diff = increasing ? d_partialModel.getUpperBound(leaving) - assignment : d_partialModel.getLowerBound(leaving) - assignment; - - shift = diff; - - Assert(increasing ? shift.sgn() >=0 : shift.sgn() <= 0); - Assert(increasing ? shift > minimumShift : shift < minimumShift); - - progress = true; - return; - }else{ - Assert(bounded); - progress = true; - - if((increasing ? d_partialModel.hasUpperBound(leaving) : d_partialModel.hasLowerBound(leaving) )){ - Assert(entering != ARITHVAR_SENTINEL); - const DeltaRational& assignment = d_partialModel.getAssignment(leaving); - DeltaRational diff = increasing ? d_partialModel.getUpperBound(leaving) - assignment : d_partialModel.getLowerBound(leaving) - assignment; - if((increasing) ? (diff < shift) : ( diff > shift)){ - shift = diff; - } - } - - Assert(increasing ? shift.sgn() >=0 : shift.sgn() <= 0); - Assert(increasing ? shift > minimumShift : shift < minimumShift); - return; - } - - - // if(! bounded || - // (increasing && diff < shift) || // a new min for increasing - // (!increasing && diff > shift)){ // a new max for decreasing - // bounded = true; - // shift = diff; - // entering = basic; - // } - // } - - // if(notAtTheBound && !blandMode){ - // DeltaRational diff = basicInc ? - // (d_partialModel.getUpperBound(basic) - d_partialModel.getAssignment(basic)) / e.getCoefficient() : - // (d_partialModel.getLowerBound(basic) - d_partialModel.getAssignment(basic)) / e.getCoefficient(); - - // if(! bounded || - // (increasing && diff < shift) || // a new min for increasing - // (!increasing && diff > shift)){ // a new max for decreasing - // bounded = true; - // shift = diff; - // entering = basic; - // } - // }else if (!notAtTheBound) { // basic is already exactly at the bound - // if(!blandMode){ // Enter into using Bland's rule - // blandMode = true; - // bounded = true; - // shift = d_DELTA_ZERO; - // entering = basic; - // }else{ - // entering = minVarOrder(*this, entering, basic); // Bland's rule. - // } - // } - // else this basic variable cannot be violated by increasing/decreasing entering - - - - - // if(!blandMode && (increasing ? d_partialModel.hasUpperBound(leaving) : d_partialModel.hasLowerBound(leaving) )){ - // Assert(entering != ARITHVAR_SENTINEL); - // bounded = true; - // DeltaRational diff = increasing ? d_partialModel.getUpperBound(leaving) - assignment : d_partialModel.getLowerBound(leaving) - assignment; - // if((increasing) ? (diff < shift) : ( diff > shift)){ - // shift = diff; - // } - // } - - // Assert(increasing ? shift.sgn() >=0 : shift.sgn() <= 0); - - // return shift; -} - - -/** - * Given an variable on the optimization row that can be used to decrease the value of the optimization function - * arbitrarily and an optimization function that is strictly positive in the current model, - * driveOptToZero updates the value of unbounded s.t. the value of d_opt is exactly 0. - */ -void SimplexDecisionProcedure::driveOptToZero(ArithVar unbounded){ - Assert(!belowThreshold()); - - const Tableau::Entry& e = d_tableau.findEntry(d_tableau.basicToRowIndex(d_optRow), unbounded); - Assert(!e.blank()); - - DeltaRational theta = (d_negOptConstant-d_partialModel.getAssignment(d_optRow))/ (e.getCoefficient()); - Assert((e.getCoefficient().sgn() > 0) ? (theta.sgn() < 0) : (theta.sgn() > 0)); - - DeltaRational newAssignment = d_partialModel.getAssignment(unbounded) + theta; - d_linEq.update(unbounded, newAssignment); - - if(Debug.isOn("primal::consistent")){ Assert(d_linEq.debugEntireLinEqIsConsistent("driveOptToZero")); } - - Assert(belowThreshold()); -} diff --git a/src/theory/arith/simplex-converge.h b/src/theory/arith/simplex-converge.h deleted file mode 100644 index dac3a9b49..000000000 --- a/src/theory/arith/simplex-converge.h +++ /dev/null @@ -1,531 +0,0 @@ -/********************* */ -/*! \file simplex.h - ** \verbatim - ** Original author: taking - ** Major contributors: none - ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief This is an implementation of the Simplex Module for the Simplex for DPLL(T) decision procedure. - ** - ** This implements the Simplex module for the Simpelx for DPLL(T) decision procedure. - ** See the Simplex for DPLL(T) technical report for more background.(citation?) - ** This shares with the theory a Tableau, and a PartialModel that: - ** - satisfies the equalities in the Tableau, and - ** - the assignment for the non-basic variables satisfies their bounds. - ** This is required to either produce a conflict or satisifying PartialModel. - ** Further, we require being told when a basic variable updates its value. - ** - ** During the Simplex search we maintain a queue of variables. - ** The queue is required to contain all of the basic variables that voilate their bounds. - ** As elimination from the queue is more efficient to be done lazily, - ** we do not maintain that the queue of variables needs to be only basic variables or only variables that satisfy their bounds. - ** - ** The simplex procedure roughly follows Alberto's thesis. (citation?) - ** There is one round of selecting using a heuristic pivoting rule. (See PreferenceFunction Documentation for the available options.) - ** The non-basic variable is the one that appears in the fewest pivots. (Bruno says that Leonardo invented this first.) - ** After this, Bland's pivot rule is invoked. - ** - ** During this proccess, we periodically inspect the queue of variables to - ** 1) remove now extraneous extries, - ** 2) detect conflicts that are "waiting" on the queue but may not be detected by the current queue heuristics, and - ** 3) detect multiple conflicts. - ** - ** Conflicts are greedily slackened to use the weakest bounds that still produce the conflict. - ** - ** Extra things tracked atm: (Subject to change at Tim's whims) - ** - A superset of all of the newly pivoted variables. - ** - A queue of additional conflicts that were discovered by Simplex. - ** These are theory valid and are currently turned into lemmas - **/ - - -#include "cvc4_private.h" - -#ifndef __CVC4__THEORY__ARITH__SIMPLEX_H -#define __CVC4__THEORY__ARITH__SIMPLEX_H - -#include "theory/arith/arithvar.h" -#include "theory/arith/arith_priority_queue.h" -#include "theory/arith/delta_rational.h" -#include "theory/arith/matrix.h" -#include "theory/arith/partial_model.h" -#include "theory/arith/linear_equality.h" - -#include "context/cdlist.h" - -#include "util/dense_map.h" -#include "options/options.h" -#include "util/stats.h" -#include "util/result.h" - -#include <queue> - -namespace CVC4 { -namespace theory { -namespace arith { - -class SimplexDecisionProcedure { -private: - ArithVar d_conflictVariable; - DenseSet d_successes; - - /** Linear equality module. */ - LinearEqualityModule& d_linEq; - - /** - * Manages information about the assignment and upper and lower bounds on - * variables. - * Partial model matches that in LinearEqualityModule. - */ - ArithPartialModel& d_partialModel; - - /** - * Stores the linear equalities used by Simplex. - * Tableau from the LinearEquality module. - */ - Tableau& d_tableau; - - /** Contains a superset of the basic variables in violation of their bounds. */ - ArithPriorityQueue d_queue; - - /** Number of variables in the system. This is used for tuning heuristics. */ - ArithVar d_numVariables; - - /** This is the call back channel for Simplex to report conflicts. */ - NodeCallBack& d_conflictChannel; - - /** Maps a variable to how many times they have been used as a pivot in the simplex search. */ - DenseMultiset d_pivotsInRound; - - /** Stores to the DeltaRational constant 0. */ - DeltaRational d_DELTA_ZERO; - - //TODO make an option - const static uint32_t MAX_ITERATIONS = 20; - - - /** Used for requesting d_opt, bound and error variables for primal.*/ - ArithVarMalloc& d_arithVarMalloc; - - /** Used for constructing temporary variables, bound and error variables for primal.*/ - ConstraintDatabase& d_constraintDatabase; - -public: - SimplexDecisionProcedure(LinearEqualityModule& linEq, - NodeCallBack& conflictChannel, - ArithVarMalloc& variables, - ConstraintDatabase& constraintDatabase); - - /** - * This must be called when the value of a basic variable may now voilate one - * of its bounds. - */ - void updateBasic(ArithVar x){ - d_queue.enqueueIfInconsistent(x); - } - - /** - * Tries to update the assignments of variables such that all of the - * assignments are consistent with their bounds. - * This is done by a simplex search through the possible bases of the tableau. - * - * If all of the variables can be made consistent with their bounds - * SAT is returned. Otherwise UNSAT is returned, and at least 1 conflict - * was reported on the conflictCallback passed to the Module. - * - * Tableau pivoting is performed so variables may switch from being basic to - * nonbasic and vice versa. - * - * Corresponds to the "check()" procedure in [Cav06]. - */ - Result::Sat dualFindModel(bool exactResult); - - - /** - * Tries to update the assignments of the variables s.t. all of the assignments - * are consistent with their bounds. - * - * This is a REALLY heavy hammer consider calling dualFindModel(false) first. - * - * !!!!!!!!!!!!!IMPORTANT!!!!!!!!!!!!!! - * This procedure needs to temporarily relax contraints to contruct a satisfiable system. - * To do this, it is going to do a sat push. - */ - Result::Sat primalFindModel(); - -private: - - - /** - * A PreferenceFunction takes a const ref to the SimplexDecisionProcedure, - * and 2 ArithVar variables and returns one of the ArithVar variables potentially - * using the internals of the SimplexDecisionProcedure. - * - * Both ArithVar must be non-basic in d_tableau. - */ - typedef ArithVar (*PreferenceFunction)(const SimplexDecisionProcedure&, ArithVar, ArithVar); - - /** - * minVarOrder is a PreferenceFunction for selecting the smaller of the 2 ArithVars. - * This PreferenceFunction is used during the VarOrder stage of - * findModel. - */ - static ArithVar minVarOrder(const SimplexDecisionProcedure& simp, ArithVar x, ArithVar y); - - /** - * minRowCount is a PreferenceFunction for selecting the variable with the smaller - * row count in the tableau. - * - * This is a heuristic rule and should not be used - * during the VarOrder stage of findModel. - */ - static ArithVar minColLength(const SimplexDecisionProcedure& simp, ArithVar x, ArithVar y); - static ArithVar minRowLength(const SimplexDecisionProcedure& simp, ArithVar x, ArithVar y); - - /** - * minBoundAndRowCount is a PreferenceFunction for preferring a variable - * without an asserted bound over variables with an asserted bound. - * If both have bounds or both do not have bounds, - * the rule falls back to minRowCount(...). - * - * This is a heuristic rule and should not be used - * during the VarOrder stage of findModel. - */ - static ArithVar minBoundAndRowCount(const SimplexDecisionProcedure& simp, ArithVar x, ArithVar y); - - - /** - * This is the main simplex for DPLL(T) loop. - * It runs for at most maxIterations. - * - * Returns true iff it has found a conflict. - * d_conflictVariable will be set and the conflict for this row is reported. - */ - bool searchForFeasibleSolution(uint32_t maxIterations); - - enum SearchPeriod {BeforeDiffSearch, DuringDiffSearch, AfterDiffSearch, DuringVarOrderSearch, AfterVarOrderSearch}; - - bool findConflictOnTheQueue(SearchPeriod period); - - - /** - * Given the basic variable x_i, - * this function finds the smallest nonbasic variable x_j in the row of x_i - * in the tableau that can "take up the slack" to let x_i satisfy its bounds. - * This returns ARITHVAR_SENTINEL if none exists. - * - * More formally one of the following conditions must be satisfied: - * - lowerBound && a_ij < 0 && assignment(x_j) < upperbound(x_j) - * - lowerBound && a_ij > 0 && assignment(x_j) > lowerbound(x_j) - * - !lowerBound && a_ij > 0 && assignment(x_j) < upperbound(x_j) - * - !lowerBound && a_ij < 0 && assignment(x_j) > lowerbound(x_j) - * - */ - template <bool lowerBound> ArithVar selectSlack(ArithVar x_i, PreferenceFunction pf); - ArithVar selectSlackLowerBound(ArithVar x_i, PreferenceFunction pf = minVarOrder) { - return selectSlack<true>(x_i, pf); - } - ArithVar selectSlackUpperBound(ArithVar x_i, PreferenceFunction pf = minVarOrder) { - return selectSlack<false>(x_i, pf); - } - /** - * Returns the smallest basic variable whose assignment is not consistent - * with its upper and lower bounds. - */ - ArithVar selectSmallestInconsistentVar(); - - /** - * Given a non-basic variable that is know to not be updatable - * to a consistent value, construct and return a conflict. - * Follows section 4.2 in the CAV06 paper. - */ - Node generateConflictAboveUpperBound(ArithVar conflictVar); - Node generateConflictBelowLowerBound(ArithVar conflictVar); - -public: - void increaseMax() {d_numVariables++;} - - - void clearQueue() { - d_queue.clear(); - } - - - bool debugIsInCollectionQueue(ArithVar var) const{ - Assert(d_queue.inCollectionMode()); - return d_queue.collectionModeContains(var); - } - - void reduceQueue(){ - d_queue.reduce(); - } - - ArithPriorityQueue::const_iterator queueBegin() const{ - return d_queue.begin(); - } - - ArithPriorityQueue::const_iterator queueEnd() const{ - return d_queue.end(); - } - -private: - - /** Reports a conflict to on the output channel. */ - void reportConflict(Node conflict){ - d_conflictChannel(conflict); - ++(d_statistics.d_simplexConflicts); - } - - template <bool above> - inline bool isAcceptableSlack(int sgn, ArithVar nonbasic){ - return - ( above && sgn < 0 && d_partialModel.strictlyBelowUpperBound(nonbasic)) || - ( above && sgn > 0 && d_partialModel.strictlyAboveLowerBound(nonbasic)) || - (!above && sgn > 0 && d_partialModel.strictlyBelowUpperBound(nonbasic)) || - (!above && sgn < 0 && d_partialModel.strictlyAboveLowerBound(nonbasic)); - } - - /** - * Checks a basic variable, b, to see if it is in conflict. - * If a conflict is discovered a node summarizing the conflict is returned. - * Otherwise, Node::null() is returned. - */ - Node checkBasicForConflict(ArithVar b); - - Node weakenConflict(bool aboveUpper, ArithVar basicVar); - Constraint weakestExplanation(bool aboveUpper, DeltaRational& surplus, ArithVar v, const Rational& coeff, bool& anyWeakening, ArithVar basic); - - /** Gets a fresh variable from TheoryArith. */ - ArithVar requestVariable(){ - return d_arithVarMalloc.request(); - } - - /** Releases a requested variable from TheoryArith.*/ - void releaseVariable(ArithVar v){ - d_arithVarMalloc.release(v); - } - - - /** An error info keeps the information associated with the construction of an ErrorVariable. */ - class ErrorInfo { - private: - /** The variable for which the error variable was constructed.*/ - ArithVar d_variable; - - // If false -> lowerbound - bool d_upperbound; - - /** The violated constraint this was constructed to try to satisfy.*/ - Constraint d_violated; - - public: - ErrorInfo(ArithVar error, bool ub, const Constraint original) - : d_variable(error), d_upperbound(ub), d_violated(original) {} - - ErrorInfo() : - d_variable(ARITHVAR_SENTINEL), d_upperbound(false), d_violated(NullConstraint){} - - inline ArithVar getVariable() const { - return d_variable; - } - - inline bool isUpperbound() const { - return d_upperbound; - } - - inline bool errorIsLeqZero(const ArithPartialModel& d_pm) const{ - return isUpperbound() ? - (d_pm.getAssignment(d_variable) <= d_violated->getValue()) : - (d_pm.getAssignment(d_variable) >= d_violated->getValue()); - } - - inline Constraint getConstraint() const { - return d_violated; - } - - inline DeltaRational getErrorAmount(const ArithPartialModel& d_pm) const { - return isUpperbound() ? - (d_pm.getAssignment(d_variable) - d_violated->getValue()) : - (d_violated->getValue() - d_pm.getAssignment(d_variable)); - } - }; - - typedef DenseMap<ErrorInfo> ErrorMap; - - /** A map from the error variables to the associated ErrorInfo.*/ - ErrorMap d_currentErrorVariables; - - /** The optimization function is implicitly defined as - * f_i = d_optRow - d_negOptConstant - * - * d_optRow is a basic variable in the tableau. - * The tableau maintains that it is equal to the sum of -1^{!ub} * the error variables in - * d_currentErrorVariables. - * - * d_negOptConstant is explicitly the negation of the sum of the bounds that were violated - * - * assignment(f_i) <= 0 iff assignment(d_optRow) <= d_negOptConstant - */ - /** The variable for the variable part of the optimization function.*/ - ArithVar d_optRow; - - /** The constant part of the optimization function.*/ - DeltaRational d_negOptConstant; - - inline bool belowThreshold() const { - return d_partialModel.getAssignment(d_optRow) <= d_negOptConstant; - } - - /** - * A PrimalResponse represents the state that the primal simplex solver is in. - */ - enum PrimalResponse { - // The optimization can decrease arbitrarily on some variable in the function - FoundUnboundedVariable, - - // The optimization function has reached a threshold value and is checking back in - ReachedThresholdValue, - - // Simplex has used up its pivot bound and is checking back in with its caller - UsedMaxPivots, - - //Simplex can make progress on the pair of entering and leaving variables - MakeProgressOnLeaving, - - //Simplex is not at a minimum but no leaving variable can be changed to help - NoProgressOnLeaving, - - // Simplex has reached a minimum for its optimization function - GlobalMinimum - }; - - /** - * These fields are for sticking information for passing information back with the PrimalRespones. - * These fields should be ignored as unsafe/unknown unless you have a PrimalResponse that states - * the field makes sense. - */ - struct PrimalPassBack { - public: - /** - * A variable s.t. its value can be increased/decreased arbitrarily to change the optimization function - * arbitrarily low. - */ - ArithVar d_unbounded; - - /** The leaving variable selection for primal simplex. */ - ArithVar d_leaving; - - /** The entering variable selection for primal simplex. */ - ArithVar d_entering; - - /** The new value for the leaving variable value for primal simplex.*/ - DeltaRational d_nextEnteringValue; - - PrimalPassBack() { clear(); } - void clear(){ - d_unbounded = (d_leaving = (d_entering = ARITHVAR_SENTINEL)); - d_nextEnteringValue = DeltaRational(); - } - - bool isClear() const { - return d_unbounded == ARITHVAR_SENTINEL && - d_leaving == ARITHVAR_SENTINEL && - d_entering == ARITHVAR_SENTINEL && - d_nextEnteringValue.sgn() == 0; - } - } d_primalCarry; - - uint32_t d_pivotsSinceErrorProgress; - uint32_t d_pivotsSinceOptProgress; - uint32_t d_pivotsSinceLastCheck; - - typedef std::vector< const Tableau::Entry* > EntryVector; - EntryVector d_improvementCandidates; - - PrimalResponse primal(uint32_t maxIterations); - PrimalResponse primalCheck(); - Result::Sat primalConverge(int depth); - void driveOptToZero(ArithVar unbounded); - uint32_t contractErrorVariables(bool guaranteedSuccess); - bool checkForRowConflicts(); - void restoreErrorVariables(ErrorMap& es); - void constructErrorVariables(); - void constructOptimizationFunction(); - void removeOptimizationFunction(); - void reconstructOptimizationFunction(); - ArithVar selectMinimumValid(ArithVar v, bool increasing); - ArithVar selectFirstValid(ArithVar v, bool increasing); - - void reassertErrorConstraint(ArithVar e, ErrorMap& es, bool definitelyTrue, bool definitelyFalse); - void computeShift(ArithVar leaving, bool increasing, bool& progress, ArithVar& entering, DeltaRational& shift, const DeltaRational& minimumShift); - - /** These fields are designed to be accessible to TheoryArith methods. */ - class Statistics { - public: - IntStat d_statUpdateConflicts; - - TimerStat d_findConflictOnTheQueueTime; - - IntStat d_attemptBeforeDiffSearch, d_successBeforeDiffSearch; - IntStat d_attemptAfterDiffSearch, d_successAfterDiffSearch; - IntStat d_attemptDuringDiffSearch, d_successDuringDiffSearch; - IntStat d_attemptDuringVarOrderSearch, d_successDuringVarOrderSearch; - IntStat d_attemptAfterVarOrderSearch, d_successAfterVarOrderSearch; - - IntStat d_weakeningAttempts, d_weakeningSuccesses, d_weakenings; - TimerStat d_weakenTime; - - - IntStat d_simplexConflicts; - - // Primal stuffs - TimerStat d_primalTimer; - TimerStat d_internalTimer; - - IntStat d_primalCalls; - IntStat d_primalSatCalls; - IntStat d_primalUnsatCalls; - - IntStat d_primalPivots; - IntStat d_primalImprovingPivots; - - IntStat d_primalThresholdReachedPivot; - IntStat d_primalThresholdReachedPivot_dropped; - - IntStat d_primalReachedMaxPivots; - IntStat d_primalReachedMaxPivots_contractMadeProgress; - IntStat d_primalReachedMaxPivots_checkForConflictWorked; - - - IntStat d_primalGlobalMinimum; - IntStat d_primalGlobalMinimum_rowConflictWorked; - IntStat d_primalGlobalMinimum_firstHalfWasSat; - IntStat d_primalGlobalMinimum_firstHalfWasUnsat; - IntStat d_primalGlobalMinimum_contractMadeProgress; - - - IntStat d_unboundedFound; - IntStat d_unboundedFound_drive; - IntStat d_unboundedFound_dropped; - - - Statistics(); - ~Statistics(); - }; - - Statistics d_statistics; - -};/* class SimplexDecisionProcedure */ - -}/* CVC4::theory::arith namespace */ -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ - -#endif /* __CVC4__THEORY__ARITH__SIMPLEX_H */ - diff --git a/src/theory/arith/soi_simplex.cpp b/src/theory/arith/soi_simplex.cpp index d0595321c..6095727a3 100644 --- a/src/theory/arith/soi_simplex.cpp +++ b/src/theory/arith/soi_simplex.cpp @@ -286,7 +286,6 @@ UpdateInfo SumOfInfeasibilitiesSPD::selectUpdate(LinearEqualityModule::UpdatePre ArithVar curr = cand.d_nb; const Rational& coeff = *cand.d_coeff; -#warning "Who is using computeSafeUpdate?" LinearEqualityModule::UpdatePreferenceFunction leavingPrefFunc = selectLeavingFunction(curr); UpdateInfo currProposal = d_linEq.speculativeUpdate(curr, coeff, leavingPrefFunc); diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp index 7eae2606c..e4b19a683 100644 --- a/src/theory/arith/theory_arith_private.cpp +++ b/src/theory/arith/theory_arith_private.cpp @@ -96,7 +96,7 @@ TheoryArithPrivate::TheoryArithPrivate(TheoryArith& containing, context::Context d_currentPropagationList(), d_learnedBounds(c), d_partialModel(c, DeltaComputeCallback(*this)), - d_errorSet(d_partialModel, TableauSizes(&d_tableau), BoundCountingLookup(&d_rowTracking, &d_tableau)), + d_errorSet(d_partialModel, TableauSizes(&d_tableau), BoundCountingLookup(*this)), d_tableau(), d_linEq(d_partialModel, d_tableau, d_rowTracking, BasicVarModelUpdateCallBack(*this)), d_diosolver(c), @@ -107,7 +107,6 @@ TheoryArithPrivate::TheoryArithPrivate(TheoryArith& containing, context::Context d_conflicts(c), d_congruenceManager(c, d_constraintDatabase, SetupLiteralCallBack(*this), d_partialModel, RaiseConflict(*this)), d_dualSimplex(d_linEq, d_errorSet, RaiseConflict(*this), TempVarMalloc(*this)), - d_pureUpdate(d_linEq, d_errorSet, RaiseConflict(*this), TempVarMalloc(*this)), d_fcSimplex(d_linEq, d_errorSet, RaiseConflict(*this), TempVarMalloc(*this)), d_soiSimplex(d_linEq, d_errorSet, RaiseConflict(*this), TempVarMalloc(*this)), d_DELTA_ZERO(0), @@ -2882,6 +2881,11 @@ void TheoryArithPrivate::dumpUpdatedBoundsToRows(){ d_updatedBounds.purge(); } +const BoundsInfo& TheoryArithPrivate::boundsInfo(ArithVar basic) const{ + RowIndex ridx = d_tableau.basicToRowIndex(basic); + return d_rowTracking[ridx]; +} + }/* CVC4::theory::arith namespace */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ diff --git a/src/theory/arith/theory_arith_private.h b/src/theory/arith/theory_arith_private.h index e522bb8c8..b97ab3468 100644 --- a/src/theory/arith/theory_arith_private.h +++ b/src/theory/arith/theory_arith_private.h @@ -58,7 +58,6 @@ #include "theory/arith/dual_simplex.h" #include "theory/arith/fc_simplex.h" #include "theory/arith/soi_simplex.h" -#include "theory/arith/pure_update_simplex.h" #include "theory/arith/constraint.h" @@ -316,7 +315,6 @@ private: /** This implements the Simplex decision procedure. */ DualSimplexDecisionProcedure d_dualSimplex; - PureUpdateSimplexDecisionProcedure d_pureUpdate; FCSimplexDecisionProcedure d_fcSimplex; SumOfInfeasibilitiesSPD d_soiSimplex; @@ -430,6 +428,10 @@ public: */ ArithVar requestArithVar(TNode x, bool slack); +public: + const BoundsInfo& boundsInfo(ArithVar basic) const; + + private: /** Initial (not context dependent) sets up for a variable.*/ void setupBasicValue(ArithVar x); |