GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/arith/attempt_solution_simplex.cpp Lines: 15 80 18.8 %
Date: 2021-03-22 Branches: 16 298 5.4 %

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