1 /********************* */
2 /*! \file theory_arith.h
4 ** Original author: mdeters
5 ** Major contributors: taking
6 ** Minor contributors (to current version): barrett
7 ** This file is part of the CVC4 prototype.
8 ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys)
9 ** Courant Institute of Mathematical Sciences
10 ** New York University
11 ** See the file COPYING in the top-level source directory for licensing
12 ** information.\endverbatim
14 ** \brief Arithmetic theory.
19 #include "cvc4_private.h"
21 #ifndef __CVC4__THEORY__ARITH__THEORY_ARITH_H
22 #define __CVC4__THEORY__ARITH__THEORY_ARITH_H
24 #include "theory/theory.h"
25 #include "context/context.h"
26 #include "context/cdlist.h"
27 #include "context/cdset.h"
28 #include "expr/node.h"
30 #include "theory/arith/arith_utilities.h"
31 #include "theory/arith/arithvar_set.h"
32 #include "theory/arith/delta_rational.h"
33 #include "theory/arith/tableau.h"
34 #include "theory/arith/arith_rewriter.h"
35 #include "theory/arith/partial_model.h"
36 #include "theory/arith/unate_propagator.h"
37 #include "theory/arith/simplex.h"
38 #include "theory/arith/arith_static_learner.h"
40 #include "util/stats.h"
51 * Implementation of QF_LRA.
53 * http://research.microsoft.com/en-us/um/people/leonardo/cav06.pdf
55 class TheoryArith
: public Theory
{
58 /** Static learner. */
59 ArithStaticLearner learner
;
62 * List of the variables in the system.
63 * This is needed to keep a positive ref count on slack variables.
65 std::vector
<Node
> d_variables
;
68 * If ArithVar v maps to the node n in d_removednode,
69 * then n = (= asNode(v) rhs) where rhs is a term that
70 * can be used to determine the value of n using getValue().
72 std::map
<ArithVar
, Node
> d_removedRows
;
75 * Manages information about the assignment and upper and lower bounds on
78 ArithPartialModel d_partialModel
;
81 * Set of ArithVars that were introduced via preregisteration.
83 ArithVarSet d_userVariables
;
86 * Bidirectional map between Nodes and ArithVars.
88 NodeToArithVarMap d_nodeToArithVarMap
;
89 ArithVarToNodeMap d_arithVarToNodeMap
;
91 inline bool hasArithVar(TNode x
) const {
92 return d_nodeToArithVarMap
.find(x
) != d_nodeToArithVarMap
.end();
95 inline ArithVar
asArithVar(TNode x
) const{
96 Assert(hasArithVar(x
));
97 Assert((d_nodeToArithVarMap
.find(x
))->second
<= ARITHVAR_SENTINEL
);
98 return (d_nodeToArithVarMap
.find(x
))->second
;
100 inline Node
asNode(ArithVar a
) const{
101 Assert(d_arithVarToNodeMap
.find(a
) != d_arithVarToNodeMap
.end());
102 return (d_arithVarToNodeMap
.find(a
))->second
;
105 inline void setArithVar(TNode x
, ArithVar a
){
106 Assert(!hasArithVar(x
));
107 Assert(d_arithVarToNodeMap
.find(a
) == d_arithVarToNodeMap
.end());
108 d_arithVarToNodeMap
[a
] = x
;
109 d_nodeToArithVarMap
[x
] = a
;
113 * List of all of the inequalities asserted in the current context.
115 context::CDSet
<Node
, NodeHashFunction
> d_diseq
;
118 * The tableau for all of the constraints seen thus far in the system.
123 /** Counts the number of notifyRestart() calls to the theory. */
124 uint32_t d_restartsCounter
;
127 * Every number of restarts equal to s_TABLEAU_RESET_PERIOD,
128 * the density of the tableau, d, is computed.
129 * If d >= s_TABLEAU_RESET_DENSITY * d_initialDensity, the tableau
130 * is set to d_initialTableau.
132 bool d_presolveHasBeenCalled
;
133 double d_tableauResetDensity
;
134 uint32_t d_tableauResetPeriod
;
135 static const uint32_t s_TABLEAU_RESET_INCREMENT
= 5;
138 * A copy of the tableau immediately after removing variables
139 * without bounds in presolve().
141 Tableau d_smallTableauCopy
;
143 ArithUnatePropagator d_propagator
;
144 SimplexDecisionProcedure d_simplex
;
147 TheoryArith(context::Context
* c
, OutputChannel
& out
, Valuation valuation
);
151 * Does non-context dependent setup for a node connected to a theory.
153 void preRegisterTerm(TNode n
);
155 /** CD setup for a node. Currently does nothing. */
156 void registerTerm(TNode n
);
158 void check(Effort e
);
159 void propagate(Effort e
);
160 void explain(TNode n
);
162 void notifyEq(TNode lhs
, TNode rhs
);
164 Node
getValue(TNode n
);
169 void notifyRestart();
170 void staticLearning(TNode in
, NodeBuilder
<>& learned
);
172 std::string
identify() const { return std::string("TheoryArith"); }
175 /** The constant zero. */
176 DeltaRational d_DELTA_ZERO
;
179 * Using the simpleKind return the ArithVar associated with the
180 * left hand side of assertion.
182 ArithVar
determineLeftVariable(TNode assertion
, Kind simpleKind
);
184 /** Splits the disequalities in d_diseq that are violated using lemmas on demand. */
185 void splitDisequalities();
188 * This requests a new unique ArithVar value for x.
189 * This also does initial (not context dependent) set up for a variable,
190 * except for setting up the initial.
192 ArithVar
requestArithVar(TNode x
, bool basic
);
194 /** Initial (not context dependent) sets up for a variable.*/
195 void setupInitialValue(ArithVar x
);
197 /** Initial (not context dependent) sets up for a new slack variable.*/
198 void setupSlack(TNode left
);
202 * Handles the case splitting for check() for a new assertion.
203 * Returns a conflict if one was found.
204 * Returns Node::null if no conflict was found.
206 Node
assertionCases(TNode assertion
);
209 * This is used for reporting conflicts caused by disequalities during assertionCases.
211 Node
disequalityConflict(TNode eq
, TNode lb
, TNode ub
);
214 * Returns the basic variable with the shorted row containg a non-basic variable.
215 * If no such row exists, return ARITHVAR_SENTINEL.
217 ArithVar
findShortestBasicRow(ArithVar variable
);
220 * Debugging only routine!
221 * Returns true iff every variable is consistent in the partial model.
223 bool entireStateIsConsistent();
226 * Permanently removes a variable from the problem.
227 * The caller guarentees the saftey of this removal!
229 void permanentlyRemoveVariable(ArithVar v
);
232 void asVectors(Polynomial
& p
,
233 std::vector
<Rational
>& coeffs
,
234 std::vector
<ArithVar
>& variables
) const;
236 /** Routine for debugging. Print the assertions the theory is aware of. */
237 void debugPrintAssertions();
238 /** Debugging only routine. Prints the model. */
239 void debugPrintModel();
241 /** These fields are designed to be accessable to TheoryArith methods. */
244 IntStat d_statUserVariables
, d_statSlackVariables
;
245 IntStat d_statDisequalitySplits
;
246 IntStat d_statDisequalityConflicts
;
247 TimerStat d_staticLearningTimer
;
249 IntStat d_permanentlyRemovedVariables
;
250 TimerStat d_presolveTime
;
252 IntStat d_initialTableauSize
;
253 //ListStat<uint32_t> d_tableauSizeHistory;
254 IntStat d_currSetToSmaller
;
255 IntStat d_smallerSetToCurr
;
256 TimerStat d_restartTimer
;
262 Statistics d_statistics
;
265 };/* class TheoryArith */
267 }/* CVC4::theory::arith namespace */
268 }/* CVC4::theory namespace */
269 }/* CVC4 namespace */
271 #endif /* __CVC4__THEORY__ARITH__THEORY_ARITH_H */