1 

/********************* */ 
2 

/*! \file attempt_solution_simplex.h 
3 

** \verbatim 
4 

** Top contributors (to current version): 
5 

** Tim King, Morgan Deters, Mathias Preiner 
6 

** This file is part of the CVC4 project. 
7 

** Copyright (c) 20092021 by the authors listed in the file AUTHORS 
8 

** in the toplevel source directory and their institutional affiliations. 
9 

** All rights reserved. See the file COPYING in the toplevel source 
10 

** directory for licensing information.\endverbatim 
11 

** 
12 

** \brief This is an implementation of the Simplex Module for the Simplex for 
13 

** DPLL(T) decision procedure. 
14 

** 
15 

** This implements the Simplex module for the Simpelx for DPLL(T) decision 
16 

** procedure. 
17 

** See the Simplex for DPLL(T) technical report for more background.(citation?) 
18 

** This shares with the theory a Tableau, and a PartialModel that: 
19 

**  satisfies the equalities in the Tableau, and 
20 

**  the assignment for the nonbasic variables satisfies their bounds. 
21 

** This is required to either produce a conflict or satisifying PartialModel. 
22 

** Further, we require being told when a basic variable updates its value. 
23 

** 
24 

** During the Simplex search we maintain a queue of variables. 
25 

** The queue is required to contain all of the basic variables that voilate 
26 

** their bounds. 
27 

** As elimination from the queue is more efficient to be done lazily, 
28 

** we do not maintain that the queue of variables needs to be only basic 
29 

** variables or only variables that satisfy their bounds. 
30 

** 
31 

** The simplex procedure roughly follows Alberto's thesis. (citation?) 
32 

** There is one round of selecting using a heuristic pivoting rule. 
33 

** (See PreferenceFunction Documentation for the available options.) 
34 

** The nonbasic variable is the one that appears in the fewest pivots. 
35 

** (Bruno says that Leonardo invented this first.) 
36 

** After this, Bland's pivot rule is invoked. 
37 

** 
38 

** During this proccess, we periodically inspect the queue of variables to 
39 

** 1) remove now extraneous extries, 
40 

** 2) detect conflicts that are "waiting" on the queue but may not be detected 
41 

** by the current queue heuristics, and 
42 

** 3) detect multiple conflicts. 
43 

** 
44 

** Conflicts are greedily slackened to use the weakest bounds that still 
45 

** produce the conflict. 
46 

** 
47 

** Extra things tracked atm: (Subject to change at Tim's whims) 
48 

**  A superset of all of the newly pivoted variables. 
49 

**  A queue of additional conflicts that were discovered by Simplex. 
50 

** These are theory valid and are currently turned into lemmas 
51 

**/ 
52 


53 

#include "cvc4_private.h" 
54 


55 

#pragma once 
56 


57 

#include "theory/arith/simplex.h" 
58 

#include "theory/arith/approx_simplex.h" 
59 

#include "util/statistics_registry.h" 
60 


61 

namespace CVC4 { 
62 

namespace theory { 
63 

namespace arith { 
64 


65 
8992 
class AttemptSolutionSDP : public SimplexDecisionProcedure { 
66 

public: 
67 

AttemptSolutionSDP(LinearEqualityModule& linEq, ErrorSet& errors, RaiseConflict conflictChannel, TempVarMalloc tvmalloc); 
68 


69 

Result::Sat attempt(const ApproximateSimplex::Solution& sol); 
70 


71 

Result::Sat findModel(bool exactResult) override { Unreachable(); } 
72 


73 

private: 
74 

bool matchesNewValue(const DenseMap<DeltaRational>& nv, ArithVar v) const; 
75 


76 

bool processSignals(){ 
77 

TimerStat &timer = d_statistics.d_queueTime; 
78 

IntStat& conflictStat = d_statistics.d_conflicts; 
79 

return standardProcessSignals(timer, conflictStat); 
80 

} 
81 

/** These fields are designed to be accessible to TheoryArith methods. */ 
82 

class Statistics { 
83 

public: 
84 

TimerStat d_searchTime; 
85 

TimerStat d_queueTime; 
86 

IntStat d_conflicts; 
87 


88 

Statistics(); 
89 

~Statistics(); 
90 

} d_statistics; 
91 

};/* class AttemptSolutionSDP */ 
92 


93 

}/* CVC4::theory::arith namespace */ 
94 

}/* CVC4::theory namespace */ 
95 

}/* CVC4 namespace */ 