src/theory/arith/attempt_solution_simplex.cpp

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