1 /********************* */
4 ** Original author: taking
5 ** Major contributors: none
6 ** Minor contributors (to current version): kshitij, mdeters
7 ** This file is part of the CVC4 prototype.
8 ** Copyright (c) 2009-2012 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 This is an implementation of the Simplex Module for the Simplex for DPLL(T)
13 ** decision procedure.
15 ** This implements the Simplex module for the Simpelx for DPLL(T) decision procedure.
16 ** See the Simplex for DPLL(T) technical report for more background.(citation?)
17 ** This shares with the theory a Tableau, and a PartialModel that:
18 ** - satisfies the equalities in the Tableau, and
19 ** - the assignment for the non-basic variables satisfies their bounds.
20 ** This is required to either produce a conflict or satisifying PartialModel.
21 ** Further, we require being told when a basic variable updates its value.
23 ** During the Simplex search we maintain a queue of variables.
24 ** The queue is required to contain all of the basic variables that voilate their bounds.
25 ** As elimination from the queue is more efficient to be done lazily,
26 ** we do not maintain that the queue of variables needs to be only basic variables or only
27 ** variables that satisfy their bounds.
29 ** The simplex procedure roughly follows Alberto's thesis. (citation?)
30 ** There is one round of selecting using a heuristic pivoting rule. (See PreferenceFunction
31 ** Documentation for the available options.)
32 ** The non-basic variable is the one that appears in the fewest pivots. (Bruno says that
33 ** Leonardo invented this first.)
34 ** After this, Bland's pivot rule is invoked.
36 ** During this proccess, we periodically inspect the queue of variables to
37 ** 1) remove now extraneous extries,
38 ** 2) detect conflicts that are "waiting" on the queue but may not be detected by the
39 ** current queue heuristics, and
40 ** 3) detect multiple conflicts.
42 ** Conflicts are greedily slackened to use the weakest bounds that still produce the
45 ** Extra things tracked atm: (Subject to change at Tim's whims)
46 ** - A superset of all of the newly pivoted variables.
47 ** - A queue of additional conflicts that were discovered by Simplex.
48 ** These are theory valid and are currently turned into lemmas
52 #include "cvc4_private.h"
56 #include "util/statistics_registry.h"
57 #include "theory/arith/simplex.h"
58 #include "theory/arith/approx_simplex.h"
64 class AttemptSolutionSDP
: public SimplexDecisionProcedure
{
66 AttemptSolutionSDP(LinearEqualityModule
& linEq
, ErrorSet
& errors
, RaiseConflict conflictChannel
, TempVarMalloc tvmalloc
);
68 Result::Sat
attempt(const ApproximateSimplex::Solution
& sol
);
70 Result::Sat
findModel(bool exactResult
){
75 bool matchesNewValue(const DenseMap
<DeltaRational
>& nv
, ArithVar v
) const;
77 bool processSignals(){
78 TimerStat
&timer
= d_statistics
.d_queueTime
;
79 IntStat
& conflictStat
= d_statistics
.d_conflicts
;
80 return standardProcessSignals(timer
, conflictStat
);
82 /** These fields are designed to be accessible to TheoryArith methods. */
85 TimerStat d_searchTime
;
86 TimerStat d_queueTime
;
92 };/* class AttemptSolutionSDP */
94 }/* CVC4::theory::arith namespace */
95 }/* CVC4::theory namespace */