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"
39 #include "theory/arith/arith_prop_manager.h"
40 #include "theory/arith/arithvar_node_map.h"
42 #include "util/stats.h"
53 * Implementation of QF_LRA.
55 * http://research.microsoft.com/en-us/um/people/leonardo/cav06.pdf
57 class TheoryArith
: public Theory
{
60 /** Static learner. */
61 ArithStaticLearner learner
;
64 * List of the variables in the system.
65 * This is needed to keep a positive ref count on slack variables.
67 std::vector
<Node
> d_variables
;
69 ArithVarNodeMap d_arithvarNodeMap
;
72 * If ArithVar v maps to the node n in d_removednode,
73 * then n = (= asNode(v) rhs) where rhs is a term that
74 * can be used to determine the value of n using getValue().
76 std::map
<ArithVar
, Node
> d_removedRows
;
79 * Manages information about the assignment and upper and lower bounds on
82 ArithPartialModel d_partialModel
;
85 * Set of ArithVars that were introduced via preregisteration.
87 ArithVarSet d_userVariables
;
92 * List of all of the inequalities asserted in the current context.
94 context::CDSet
<Node
, NodeHashFunction
> d_diseq
;
97 * The tableau for all of the constraints seen thus far in the system.
102 /** Counts the number of notifyRestart() calls to the theory. */
103 uint32_t d_restartsCounter
;
106 * Every number of restarts equal to s_TABLEAU_RESET_PERIOD,
107 * the density of the tableau, d, is computed.
108 * If d >= s_TABLEAU_RESET_DENSITY * d_initialDensity, the tableau
109 * is set to d_initialTableau.
111 bool d_presolveHasBeenCalled
;
112 double d_tableauResetDensity
;
113 uint32_t d_tableauResetPeriod
;
114 static const uint32_t s_TABLEAU_RESET_INCREMENT
= 5;
117 * A copy of the tableau immediately after removing variables
118 * without bounds in presolve().
120 Tableau d_smallTableauCopy
;
122 ArithUnatePropagator d_propagator
;
124 ArithPropManager d_propManager
;
126 SimplexDecisionProcedure d_simplex
;
129 TheoryArith(context::Context
* c
, OutputChannel
& out
, Valuation valuation
);
133 * Does non-context dependent setup for a node connected to a theory.
135 void preRegisterTerm(TNode n
);
137 /** CD setup for a node. Currently does nothing. */
138 void registerTerm(TNode n
);
140 void check(Effort e
);
141 void propagate(Effort e
);
142 void explain(TNode n
);
144 void notifyEq(TNode lhs
, TNode rhs
);
146 Node
getValue(TNode n
);
151 void notifyRestart();
152 void staticLearning(TNode in
, NodeBuilder
<>& learned
);
154 std::string
identify() const { return std::string("TheoryArith"); }
157 /** The constant zero. */
158 DeltaRational d_DELTA_ZERO
;
160 /** propagates an arithvar */
161 void propagateArithVar(bool upperbound
, ArithVar var
);
164 * Using the simpleKind return the ArithVar associated with the
165 * left hand side of assertion.
167 ArithVar
determineLeftVariable(TNode assertion
, Kind simpleKind
);
169 /** Splits the disequalities in d_diseq that are violated using lemmas on demand. */
170 void splitDisequalities();
173 * This requests a new unique ArithVar value for x.
174 * This also does initial (not context dependent) set up for a variable,
175 * except for setting up the initial.
177 ArithVar
requestArithVar(TNode x
, bool basic
);
179 /** Initial (not context dependent) sets up for a variable.*/
180 void setupInitialValue(ArithVar x
);
182 /** Initial (not context dependent) sets up for a new slack variable.*/
183 void setupSlack(TNode left
);
187 * Handles the case splitting for check() for a new assertion.
188 * Returns a conflict if one was found.
189 * Returns Node::null if no conflict was found.
191 Node
assertionCases(TNode assertion
);
194 * This is used for reporting conflicts caused by disequalities during assertionCases.
196 Node
disequalityConflict(TNode eq
, TNode lb
, TNode ub
);
199 * Returns the basic variable with the shorted row containg a non-basic variable.
200 * If no such row exists, return ARITHVAR_SENTINEL.
202 ArithVar
findShortestBasicRow(ArithVar variable
);
205 * Debugging only routine!
206 * Returns true iff every variable is consistent in the partial model.
208 bool entireStateIsConsistent();
211 * Permanently removes a variable from the problem.
212 * The caller guarentees the saftey of this removal!
214 void permanentlyRemoveVariable(ArithVar v
);
216 bool isImpliedUpperBound(ArithVar var
, Node exp
);
217 bool isImpliedLowerBound(ArithVar var
, Node exp
);
219 void internalExplain(TNode n
, NodeBuilder
<>& explainBuilder
);
222 void asVectors(Polynomial
& p
,
223 std::vector
<Rational
>& coeffs
,
224 std::vector
<ArithVar
>& variables
) const;
226 /** Routine for debugging. Print the assertions the theory is aware of. */
227 void debugPrintAssertions();
228 /** Debugging only routine. Prints the model. */
229 void debugPrintModel();
231 /** These fields are designed to be accessable to TheoryArith methods. */
234 IntStat d_statUserVariables
, d_statSlackVariables
;
235 IntStat d_statDisequalitySplits
;
236 IntStat d_statDisequalityConflicts
;
237 TimerStat d_staticLearningTimer
;
239 IntStat d_permanentlyRemovedVariables
;
240 TimerStat d_presolveTime
;
242 IntStat d_initialTableauSize
;
243 //ListStat<uint32_t> d_tableauSizeHistory;
244 IntStat d_currSetToSmaller
;
245 IntStat d_smallerSetToCurr
;
246 TimerStat d_restartTimer
;
252 Statistics d_statistics
;
255 };/* class TheoryArith */
257 }/* CVC4::theory::arith namespace */
258 }/* CVC4::theory namespace */
259 }/* CVC4 namespace */
261 #endif /* __CVC4__THEORY__ARITH__THEORY_ARITH_H */