src/theory/arith/attempt_solution_simplex.cpp

   1 /*********************                                                        */
   2 /*! \file attempt_solution_simplex.cpp
   3  ** \verbatim
   4  ** Original author: Tim King
   5  ** Major contributors: none
   6  ** Minor contributors (to current version): none
   7  ** This file is part of the CVC4 project.
   8  ** Copyright (c) 2009-2013  New York University and The University of Iowa
   9  ** See the file COPYING in the top-level source directory for licensing
  10  ** information.\endverbatim
  11  **
  12  ** \brief [[ Add one-line brief description here ]]
  13  **
  14  ** [[ Add lengthier description here ]]
  15  ** \todo document this file
  16  **/
  17
  18
  19 #include "theory/arith/attempt_solution_simplex.h"
  20 #include "theory/arith/options.h"
  21 #include "theory/arith/constraint.h"
  22
  23 using namespace std;
  24
  25 namespace CVC4 {
  26 namespace theory {
  27 namespace arith {
  28
  29 AttemptSolutionSDP::AttemptSolutionSDP(LinearEqualityModule& linEq, ErrorSet& errors, RaiseConflict conflictChannel, TempVarMalloc tvmalloc)
  30   : SimplexDecisionProcedure(linEq, errors, conflictChannel, tvmalloc)
  31   , d_statistics()
  32 { }
  33
  34 AttemptSolutionSDP::Statistics::Statistics():
  35   d_searchTime("theory::arith::attempt::searchTime"),
  36   d_queueTime("theory::arith::attempt::queueTime"),
  37   d_conflicts("theory::arith::attempt::conflicts", 0)
  38 {
  39   StatisticsRegistry::registerStat(&d_searchTime);
  40   StatisticsRegistry::registerStat(&d_queueTime);
  41   StatisticsRegistry::registerStat(&d_conflicts);
  42 }
  43
  44 AttemptSolutionSDP::Statistics::~Statistics(){
  45   StatisticsRegistry::unregisterStat(&d_searchTime);
  46   StatisticsRegistry::unregisterStat(&d_queueTime);
  47   StatisticsRegistry::unregisterStat(&d_conflicts);
  48 }
  49
  50 bool AttemptSolutionSDP::matchesNewValue(const DenseMap<DeltaRational>& nv, ArithVar v) const{
  51   return nv[v] == d_variables.getAssignment(v);
  52 }
  53
  54 Result::Sat AttemptSolutionSDP::attempt(const ApproximateSimplex::Solution& sol){
  55   const DenseSet& newBasis = sol.newBasis;
  56   const DenseMap<DeltaRational>& newValues = sol.newValues;
  57
  58   DenseSet needsToBeAdded;
  59   for(DenseSet::const_iterator i = newBasis.begin(), i_end = newBasis.end(); i != i_end; ++i){
  60     ArithVar b = *i;
  61     if(!d_tableau.isBasic(b)){
  62       needsToBeAdded.add(b);
  63     }
  64   }
  65   DenseMap<DeltaRational>::const_iterator nvi = newValues.begin(), nvi_end = newValues.end();
  66   for(; nvi != nvi_end; ++nvi){
  67     ArithVar currentlyNb = *nvi;
  68     if(!d_tableau.isBasic(currentlyNb)){
  69       if(!matchesNewValue(newValues, currentlyNb)){
  70         const DeltaRational& newValue = newValues[currentlyNb];
  71         Trace("arith::updateMany")
  72           << "updateMany:" << currentlyNb << " "
  73           << d_variables.getAssignment(currentlyNb) << " to "<< newValue << endl;
  74         d_linEq.update(currentlyNb, newValue);
  75         Assert(d_variables.assignmentIsConsistent(currentlyNb));
  76       }
  77     }
  78   }
  79   d_errorSet.reduceToSignals();
  80   d_errorSet.setSelectionRule(VAR_ORDER);
  81
  82   static int instance = 0;
  83   ++instance;
  84
  85   if(processSignals()){
  86     Debug("arith::findModel") << "attemptSolution("<< instance <<") early conflict" << endl;
  87     d_conflictVariables.purge();
  88     return Result::UNSAT;
  89   }else if(d_errorSet.errorEmpty()){
  90     Debug("arith::findModel") << "attemptSolution("<< instance <<") fixed itself" << endl;
  91     return Result::SAT;
  92   }
  93
  94   while(!needsToBeAdded.empty() && !d_errorSet.errorEmpty()){
  95     ArithVar toRemove = ARITHVAR_SENTINEL;
  96     ArithVar toAdd = ARITHVAR_SENTINEL;
  97     DenseSet::const_iterator i = needsToBeAdded.begin(), i_end = needsToBeAdded.end();
  98     for(; toAdd == ARITHVAR_SENTINEL && i != i_end; ++i){
  99       ArithVar v = *i;
 100
 101       Tableau::ColIterator colIter = d_tableau.colIterator(v);
 102       for(; !colIter.atEnd(); ++colIter){
 103         const Tableau::Entry& entry = *colIter;
 104         Assert(entry.getColVar() == v);
 105         ArithVar b = d_tableau.rowIndexToBasic(entry.getRowIndex());
 106         if(!newBasis.isMember(b)){
 107           toAdd = v;
 108
 109           bool favorBOverToRemove =
 110             (toRemove == ARITHVAR_SENTINEL) ||
 111             (matchesNewValue(newValues, toRemove) && !matchesNewValue(newValues, b)) ||
 112             (d_tableau.basicRowLength(toRemove) > d_tableau.basicRowLength(b));
 113
 114           if(favorBOverToRemove){
 115             toRemove = b;
 116           }
 117         }
 118       }
 119     }
 120     Assert(toRemove != ARITHVAR_SENTINEL);
 121     Assert(toAdd != ARITHVAR_SENTINEL);
 122
 123     Trace("arith::forceNewBasis") << toRemove << " " << toAdd << endl;
 124     //Message() << toRemove << " " << toAdd << endl;
 125
 126     d_linEq.pivotAndUpdate(toRemove, toAdd, newValues[toRemove]);
 127
 128     Trace("arith::forceNewBasis") << needsToBeAdded.size() << "to go" << endl;
 129     //Message() << needsToBeAdded.size() << "to go" << endl;
 130     needsToBeAdded.remove(toAdd);
 131
 132     bool conflict = processSignals();
 133     if(conflict){
 134       d_errorSet.reduceToSignals();
 135       d_conflictVariables.purge();
 136
 137       return Result::UNSAT;
 138     }
 139   }
 140   Assert( d_conflictVariables.empty() );
 141
 142   if(d_errorSet.errorEmpty()){
 143     return Result::SAT;
 144   }else{
 145     d_errorSet.reduceToSignals();
 146     return Result::SAT_UNKNOWN;
 147   }
 148 }
 149
 150 }/* CVC4::theory::arith namespace */
 151 }/* CVC4::theory namespace */
 152 }/* CVC4 namespace */