1 /********************* */
2 /*! \file attempt_solution_simplex.cpp
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
12 ** \brief [[ Add one-line brief description here ]]
14 ** [[ Add lengthier description here ]]
15 ** \todo document this file
19 #include "theory/arith/attempt_solution_simplex.h"
20 #include "theory/arith/options.h"
21 #include "theory/arith/constraint.h"
29 AttemptSolutionSDP::AttemptSolutionSDP(LinearEqualityModule
& linEq
, ErrorSet
& errors
, RaiseConflict conflictChannel
, TempVarMalloc tvmalloc
)
30 : SimplexDecisionProcedure(linEq
, errors
, conflictChannel
, tvmalloc
)
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)
39 StatisticsRegistry::registerStat(&d_searchTime
);
40 StatisticsRegistry::registerStat(&d_queueTime
);
41 StatisticsRegistry::registerStat(&d_conflicts
);
44 AttemptSolutionSDP::Statistics::~Statistics(){
45 StatisticsRegistry::unregisterStat(&d_searchTime
);
46 StatisticsRegistry::unregisterStat(&d_queueTime
);
47 StatisticsRegistry::unregisterStat(&d_conflicts
);
50 bool AttemptSolutionSDP::matchesNewValue(const DenseMap
<DeltaRational
>& nv
, ArithVar v
) const{
51 return nv
[v
] == d_variables
.getAssignment(v
);
54 Result::Sat
AttemptSolutionSDP::attempt(const ApproximateSimplex::Solution
& sol
){
55 const DenseSet
& newBasis
= sol
.newBasis
;
56 const DenseMap
<DeltaRational
>& newValues
= sol
.newValues
;
58 DenseSet needsToBeAdded
;
59 for(DenseSet::const_iterator i
= newBasis
.begin(), i_end
= newBasis
.end(); i
!= i_end
; ++i
){
61 if(!d_tableau
.isBasic(b
)){
62 needsToBeAdded
.add(b
);
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
));
79 d_errorSet
.reduceToSignals();
80 d_errorSet
.setSelectionRule(VAR_ORDER
);
82 static int instance
= 0;
86 Debug("arith::findModel") << "attemptSolution("<< instance
<<") early conflict" << endl
;
87 d_conflictVariables
.purge();
89 }else if(d_errorSet
.errorEmpty()){
90 Debug("arith::findModel") << "attemptSolution("<< instance
<<") fixed itself" << endl
;
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
){
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
)){
109 bool favorBOverToRemove
=
110 (toRemove
== ARITHVAR_SENTINEL
) ||
111 (matchesNewValue(newValues
, toRemove
) && !matchesNewValue(newValues
, b
)) ||
112 (d_tableau
.basicRowLength(toRemove
) > d_tableau
.basicRowLength(b
));
114 if(favorBOverToRemove
){
120 Assert(toRemove
!= ARITHVAR_SENTINEL
);
121 Assert(toAdd
!= ARITHVAR_SENTINEL
);
123 Trace("arith::forceNewBasis") << toRemove
<< " " << toAdd
<< endl
;
124 //Message() << toRemove << " " << toAdd << endl;
126 d_linEq
.pivotAndUpdate(toRemove
, toAdd
, newValues
[toRemove
]);
128 Trace("arith::forceNewBasis") << needsToBeAdded
.size() << "to go" << endl
;
129 //Message() << needsToBeAdded.size() << "to go" << endl;
130 needsToBeAdded
.remove(toAdd
);
132 bool conflict
= processSignals();
134 d_errorSet
.reduceToSignals();
135 d_conflictVariables
.purge();
137 return Result::UNSAT
;
140 Assert( d_conflictVariables
.empty() );
142 if(d_errorSet
.errorEmpty()){
145 d_errorSet
.reduceToSignals();
146 return Result::SAT_UNKNOWN
;
150 }/* CVC4::theory::arith namespace */
151 }/* CVC4::theory namespace */
152 }/* CVC4 namespace */