diff options
| author | Tim King <taking@cs.nyu.edu> | 2013-04-26 17:10:21 -0400 |
|---|---|---|
| committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-04-26 17:10:21 -0400 |
| commit | 9098391fe334d829ec4101f190b8f1fa21c30752 (patch) | |
| tree | b134fc1fe1c767a50013e1449330ca6a7ee18a3d /src/theory/arith/congruence_manager.cpp | |
| parent | a9174ce4dc3939bbe14c9aa1fd11c79c7877eb16 (diff) | |
FCSimplex branch merge
Diffstat (limited to 'src/theory/arith/congruence_manager.cpp')
| -rw-r--r-- | src/theory/arith/congruence_manager.cpp | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/src/theory/arith/congruence_manager.cpp b/src/theory/arith/congruence_manager.cpp index c10d59234..e3e9055a7 100644 --- a/src/theory/arith/congruence_manager.cpp +++ b/src/theory/arith/congruence_manager.cpp @@ -24,7 +24,7 @@ namespace CVC4 { namespace theory { namespace arith { -ArithCongruenceManager::ArithCongruenceManager(context::Context* c, ConstraintDatabase& cd, TNodeCallBack& setup, const ArithVarNodeMap& av2Node, NodeCallBack& raiseConflict) +ArithCongruenceManager::ArithCongruenceManager(context::Context* c, ConstraintDatabase& cd, SetupLiteralCallBack setup, const ArithVariables& avars, RaiseConflict raiseConflict) : d_inConflict(c), d_raiseConflict(raiseConflict), d_notify(*this), @@ -33,7 +33,7 @@ ArithCongruenceManager::ArithCongruenceManager(context::Context* c, ConstraintDa d_explanationMap(c), d_constraintDatabase(cd), d_setupLiteral(setup), - d_av2Node(av2Node), + d_avariables(avars), d_ee(d_notify, c, "theory::arith::ArithCongruenceManager") {} @@ -295,7 +295,7 @@ void ArithCongruenceManager::equalsConstant(Constraint c){ Debug("equalsConstant") << "equals constant " << c << std::endl; ArithVar x = c->getVariable(); - Node xAsNode = d_av2Node.asNode(x); + Node xAsNode = d_avariables.asNode(x); Node asRational = mkRationalNode(c->getValue().getNoninfinitesimalPart()); @@ -321,7 +321,7 @@ void ArithCongruenceManager::equalsConstant(Constraint lb, Constraint ub){ ArithVar x = lb->getVariable(); Node reason = ConstraintValue::explainConflict(lb,ub); - Node xAsNode = d_av2Node.asNode(x); + Node xAsNode = d_avariables.asNode(x); Node asRational = mkRationalNode(lb->getValue().getNoninfinitesimalPart()); //No guarentee this is in normal form! |