From 98b2fe2c6fefb15b57d2eae6bda505e1f41da451 Mon Sep 17 00:00:00 2001 From: Tim King Date: Fri, 2 Mar 2012 23:37:06 +0000 Subject: [PATCH] This commit merges in the changes from branches/arithmetic/refactor0 - Improved the checks in AssertLower and AssertUpper so that redundant bounds cause less work. - Because of the above change, d_constantIntegerVariables now cannot have duplicate elements enqueued. This allows removing d_varsInDioSolver. - Fix to an assertion in CDQueue. - Implements a CDArithVarSet using a vector of booleans and CDList. - Refactored ArithVar out of arith_utilities.h. Miscellaneous cleanup of arithmetic. --- src/context/cdqueue.h | 2 +- src/theory/arith/Makefile.am | 1 + src/theory/arith/arith_priority_queue.h | 2 +- src/theory/arith/arith_prop_manager.cpp | 11 +++- src/theory/arith/arith_prop_manager.h | 2 +- src/theory/arith/arith_rewriter.cpp | 14 ++++- src/theory/arith/arith_rewriter.h | 40 +++++------- src/theory/arith/arith_static_learner.cpp | 12 ++-- src/theory/arith/arith_utilities.h | 31 ++------- src/theory/arith/arithvar.h | 57 +++++++++++++++++ src/theory/arith/arithvar_node_map.h | 2 +- src/theory/arith/arithvar_set.h | 76 ++++++++++++++++++++--- src/theory/arith/atom_database.cpp | 13 ++-- src/theory/arith/difference_manager.h | 2 +- src/theory/arith/dio_solver.h | 1 - src/theory/arith/linear_equality.h | 2 +- src/theory/arith/ordered_set.h | 7 --- src/theory/arith/partial_model.cpp | 11 +++- src/theory/arith/partial_model.h | 2 +- src/theory/arith/simplex.h | 2 +- src/theory/arith/tableau.h | 2 +- src/theory/arith/theory_arith.cpp | 31 ++++----- src/theory/arith/theory_arith.h | 10 +-- 23 files changed, 213 insertions(+), 120 deletions(-) create mode 100644 src/theory/arith/arithvar.h diff --git a/src/context/cdqueue.h b/src/context/cdqueue.h index f84b66349..d733e0b1c 100644 --- a/src/context/cdqueue.h +++ b/src/context/cdqueue.h @@ -122,7 +122,7 @@ public: // Some elements have been enqueued and dequeued in the same // context and now the queue is empty we can destruct them. CDList::truncateList(d_lastsave); - Assert(d_size == d_lastsave); + Assert(CDList::d_size == d_lastsave); d_iter = d_lastsave; } } diff --git a/src/theory/arith/Makefile.am b/src/theory/arith/Makefile.am index 7934140a0..4cff4a782 100644 --- a/src/theory/arith/Makefile.am +++ b/src/theory/arith/Makefile.am @@ -7,6 +7,7 @@ noinst_LTLIBRARIES = libarith.la libarith_la_SOURCES = \ theory_arith_type_rules.h \ + arithvar.h \ arith_rewriter.h \ arith_rewriter.cpp \ arith_static_learner.h \ diff --git a/src/theory/arith/arith_priority_queue.h b/src/theory/arith/arith_priority_queue.h index 1e7e3460b..8c7069975 100644 --- a/src/theory/arith/arith_priority_queue.h +++ b/src/theory/arith/arith_priority_queue.h @@ -23,7 +23,7 @@ #ifndef __CVC4__THEORY__ARITH__ARITH_PRIORITY_QUEUE_H #define __CVC4__THEORY__ARITH__ARITH_PRIORITY_QUEUE_H -#include "theory/arith/arith_utilities.h" +#include "theory/arith/arithvar.h" #include "theory/arith/delta_rational.h" #include "theory/arith/tableau.h" #include "theory/arith/partial_model.h" diff --git a/src/theory/arith/arith_prop_manager.cpp b/src/theory/arith/arith_prop_manager.cpp index 4b52133da..dc9b0ddb9 100644 --- a/src/theory/arith/arith_prop_manager.cpp +++ b/src/theory/arith/arith_prop_manager.cpp @@ -26,13 +26,14 @@ #include "context/cdhashmap.h" #include "context/cdo.h" -using namespace CVC4; -using namespace CVC4::theory; -using namespace CVC4::theory::arith; using namespace CVC4::kind; using namespace std; +namespace CVC4 { +namespace theory { +namespace arith { + bool ArithPropManager::isAsserted(TNode n) const{ Node satValue = d_valuation.getSatValue(n); if(satValue.isNull()){ @@ -166,3 +167,7 @@ ArithPropManager::Statistics::~Statistics() StatisticsRegistry::unregisterStat(&d_alreadyPropagatedNode); StatisticsRegistry::unregisterStat(&d_addedPropagation); } + +}; /* namesapce arith */ +}; /* namespace theory */ +}; /* namespace CVC4 */ diff --git a/src/theory/arith/arith_prop_manager.h b/src/theory/arith/arith_prop_manager.h index 2bac21437..900a0ed58 100644 --- a/src/theory/arith/arith_prop_manager.h +++ b/src/theory/arith/arith_prop_manager.h @@ -23,7 +23,7 @@ #define __CVC4__THEORY__ARITH__ARITH_PROP_MANAGER_H #include "theory/valuation.h" -#include "theory/arith/arith_utilities.h" +#include "theory/arith/arithvar.h" #include "theory/arith/arithvar_node_map.h" #include "theory/arith/atom_database.h" #include "theory/arith/delta_rational.h" diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp index c0ef02ec4..ca0aa4d14 100644 --- a/src/theory/arith/arith_rewriter.cpp +++ b/src/theory/arith/arith_rewriter.cpp @@ -26,14 +26,18 @@ #include #include -using namespace CVC4; -using namespace CVC4::theory; -using namespace CVC4::theory::arith; +namespace CVC4 { +namespace theory { +namespace arith { bool isVariable(TNode t){ return t.getMetaKind() == kind::metakind::VARIABLE; } +bool ArithRewriter::isAtom(TNode n) { + return arith::isRelationOperator(n.getKind()); +} + RewriteResponse ArithRewriter::rewriteConstant(TNode t){ Assert(t.getMetaKind() == kind::metakind::CONSTANT); Node val = coerceToRationalNode(t); @@ -364,3 +368,7 @@ RewriteResponse ArithRewriter::rewriteDivByConstant(TNode t, bool pre){ return RewriteResponse(REWRITE_AGAIN, mult); } } + +}/* CVC4::theory::arith namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ diff --git a/src/theory/arith/arith_rewriter.h b/src/theory/arith/arith_rewriter.h index 822514f38..07c009b2e 100644 --- a/src/theory/arith/arith_rewriter.h +++ b/src/theory/arith/arith_rewriter.h @@ -11,10 +11,10 @@ ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** - ** \brief [[ Add one-line brief description here ]] + ** \brief Rewriter for arithmetic. ** - ** [[ Add lengthier description here ]] - ** \todo document this file + ** Rewriter for the theory of arithmetic. This rewrites to the normal form for + ** arithmetic. See theory/arith/normal_form.h for more information. **/ #include "cvc4_private.h" @@ -23,9 +23,6 @@ #define __CVC4__THEORY__ARITH__ARITH_REWRITER_H #include "theory/theory.h" -#include "theory/arith/arith_utilities.h" -#include "theory/arith/normal_form.h" - #include "theory/rewriter.h" namespace CVC4 { @@ -33,6 +30,18 @@ namespace theory { namespace arith { class ArithRewriter { +public: + + static RewriteResponse preRewrite(TNode n); + static RewriteResponse postRewrite(TNode n); + static Node rewriteEquality(TNode equality) { + // Arithmetic owns the domain, so this is totally ok + return Rewriter::rewrite(equality); + } + + static void init() { } + + static void shutdown() { } private: @@ -59,24 +68,7 @@ private: static RewriteResponse postRewriteAtom(TNode t); static RewriteResponse postRewriteAtomConstantRHS(TNode t); -public: - - static RewriteResponse preRewrite(TNode n); - static RewriteResponse postRewrite(TNode n); - static Node rewriteEquality(TNode equality) { - // Arithmetic owns the domain, so this is totally ok - return Rewriter::rewrite(equality); - } - - static void init() { } - - static void shutdown() { } - -private: - - static inline bool isAtom(TNode n) { - return arith::isRelationOperator(n.getKind()); - } + static bool isAtom(TNode n); static inline bool isTerm(TNode n) { return !isAtom(n); diff --git a/src/theory/arith/arith_static_learner.cpp b/src/theory/arith/arith_static_learner.cpp index d4d495486..2f4f6e32b 100644 --- a/src/theory/arith/arith_static_learner.cpp +++ b/src/theory/arith/arith_static_learner.cpp @@ -30,11 +30,11 @@ #include using namespace std; - -using namespace CVC4; using namespace CVC4::kind; -using namespace CVC4::theory; -using namespace CVC4::theory::arith; + +namespace CVC4 { +namespace theory { +namespace arith { ArithStaticLearner::ArithStaticLearner(SubstitutionMap& pbSubstitutions) : @@ -495,3 +495,7 @@ void ArithStaticLearner::addBound(TNode n) { break; } } + +}; /* namesapce arith */ +}; /* namespace theory */ +}; /* namespace CVC4 */ diff --git a/src/theory/arith/arith_utilities.h b/src/theory/arith/arith_utilities.h index 44b55440e..a5d94ec40 100644 --- a/src/theory/arith/arith_utilities.h +++ b/src/theory/arith/arith_utilities.h @@ -11,10 +11,9 @@ ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** - ** \brief [[ Add one-line brief description here ]] + ** \brief Arith utilities are common inline functions for dealing with nodes. ** - ** [[ Add lengthier description here ]] - ** \todo document this file + ** Arith utilities are common functions for dealing with nodes. **/ #include "cvc4_private.h" @@ -23,41 +22,21 @@ #define __CVC4__THEORY__ARITH__ARITH_UTILITIES_H #include "util/rational.h" +#include "util/integer.h" #include "expr/node.h" -#include "expr/attribute.h" #include "theory/arith/delta_rational.h" #include "context/cdhashset.h" -#include -#include -#include #include +#include namespace CVC4 { namespace theory { namespace arith { - -typedef uint32_t ArithVar; -//static const ArithVar ARITHVAR_SENTINEL = std::numeric_limits::max(); -#define ARITHVAR_SENTINEL std::numeric_limits::max() - -//Maps from Nodes -> ArithVars, and vice versa -typedef __gnu_cxx::hash_map NodeToArithVarMap; -typedef __gnu_cxx::hash_map ArithVarToNodeMap; - //Sets of Nodes typedef __gnu_cxx::hash_set NodeSet; typedef context::CDHashSet CDNodeSet; -typedef context::CDHashSet CDArithVarSet; - -class ArithVarCallBack { -public: - virtual void callback(ArithVar x) = 0; -}; - - - inline Node mkRationalNode(const Rational& q){ return NodeManager::currentNM()->mkConst(q); } @@ -126,7 +105,7 @@ inline bool isRelationOperator(Kind k){ * Given a relational kind, k, return the kind k' s.t. * swapping the lefthand and righthand side is equivalent. * - * The following equivalence should hold, + * The following equivalence should hold, * (k l r) <=> (k' r l) */ inline Kind reverseRelationKind(Kind k){ diff --git a/src/theory/arith/arithvar.h b/src/theory/arith/arithvar.h new file mode 100644 index 000000000..52dc9fd6a --- /dev/null +++ b/src/theory/arith/arithvar.h @@ -0,0 +1,57 @@ +/********************* */ +/*! \file arithvar.h + ** \verbatim + ** Original author: taking + ** Major contributors: none + ** Minor contributors (to current version): dejan, mdeters + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Defines ArithVar which is the internal representation of variables in arithmetic + ** + ** This defines ArithVar which is the internal representation of variables in + ** arithmetic. This is a typedef from uint32_t to ArithVar. + ** This file also provides utilities for ArithVars. + **/ + + +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY__ARITH__ARITHVAR_H +#define __CVC4__THEORY__ARITH__ARITHVAR_H + +#include +#include +#include +#include "expr/node.h" +#include "context/cdhashset.h" + +namespace CVC4 { +namespace theory { +namespace arith { + +typedef uint32_t ArithVar; +const ArithVar ARITHVAR_SENTINEL = std::numeric_limits::max(); + +//Maps from Nodes -> ArithVars, and vice versa +typedef __gnu_cxx::hash_map NodeToArithVarMap; +typedef __gnu_cxx::hash_map ArithVarToNodeMap; + +/** + * ArithVarCallBack provides a mechanism for agreeing on callbacks while + * breaking mutual recursion inclusion order problems. + */ +class ArithVarCallBack { +public: + virtual void callback(ArithVar x) = 0; +}; + +}; /* namesapce arith */ +}; /* namespace theory */ +}; /* namespace CVC4 */ + +#endif /* __CVC4__THEORY__ARITH__ARITHVAR_H */ diff --git a/src/theory/arith/arithvar_node_map.h b/src/theory/arith/arithvar_node_map.h index 1dc8ddf38..e8428850d 100644 --- a/src/theory/arith/arithvar_node_map.h +++ b/src/theory/arith/arithvar_node_map.h @@ -23,7 +23,7 @@ #define __CVC4__THEORY__ARITH__ARITHVAR_NODE_MAP_H -#include "theory/arith/arith_utilities.h" +#include "theory/arith/arithvar.h" #include "context/context.h" #include "context/cdlist.h" #include "context/cdhashmap.h" diff --git a/src/theory/arith/arithvar_set.h b/src/theory/arith/arithvar_set.h index 68937acc4..b502849fd 100644 --- a/src/theory/arith/arithvar_set.h +++ b/src/theory/arith/arithvar_set.h @@ -23,7 +23,10 @@ #define __CVC4__THEORY__ARITH__ARTIHVAR_SET_H #include -#include "theory/arith/arith_utilities.h" +#include "theory/arith/arithvar.h" +#include "context/context.h" +#include "context/cdlist.h" + namespace CVC4 { namespace theory { @@ -244,15 +247,6 @@ public: } } - /** Invalidates iterators */ - /* void init(ArithVar x, bool val) { */ - /* Assert(x >= allocated()); */ - /* increaseSize(x); */ - /* if(val){ */ - /* add(x); */ - /* } */ - /* } */ - /** * Invalidates iterators. */ @@ -325,6 +319,68 @@ public: } }; +class CDArithVarSet { +private: + + class RemoveIntWrapper{ + private: + ArithVar d_var; + ArithVarCallBack& d_onDestruction; + + public: + RemoveIntWrapper(ArithVar v, ArithVarCallBack& onDestruction): + d_var(v), d_onDestruction(onDestruction) + {} + + ~RemoveIntWrapper(){ + d_onDestruction.callback(d_var); + } + }; + + std::vector d_set; + context::CDList d_list; + + class OnDestruction : public ArithVarCallBack { + private: + std::vector& d_set; + public: + OnDestruction(std::vector& set): + d_set(set) + {} + + void callback(ArithVar x){ + Assert(x < d_set.size()); + d_set[x] = false; + } + }; + + OnDestruction d_callback; + +public: + CDArithVarSet(context::Context* c) : + d_list(c), d_callback(d_set) + { } + + /** This cannot be const as garbage collection is done lazily. */ + bool contains(ArithVar x) const{ + if(x < d_set.size()){ + return d_set[x]; + }else{ + return false; + } + } + + void insert(ArithVar x){ + Assert(!contains(x)); + if(x >= d_set.size()){ + d_set.resize(x+1, false); + } + d_list.push_back(RemoveIntWrapper(x, d_callback)); + d_set[x] = true; + } +}; + + }/* CVC4::theory::arith namespace */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ diff --git a/src/theory/arith/atom_database.cpp b/src/theory/arith/atom_database.cpp index 774d0eb22..3476eb8f5 100644 --- a/src/theory/arith/atom_database.cpp +++ b/src/theory/arith/atom_database.cpp @@ -22,13 +22,12 @@ #include -using namespace CVC4; -using namespace CVC4::theory; -using namespace CVC4::theory::arith; - +using namespace std; using namespace CVC4::kind; -using namespace std; +namespace CVC4 { +namespace theory { +namespace arith { ArithAtomDatabase::ArithAtomDatabase(context::Context* cxt, OutputChannel& out) : d_arithOut(out), d_setsMap() @@ -537,3 +536,7 @@ Node ArithAtomDatabase::getWeakerImpliedLowerBound(TNode lowerBound) const { Debug("arith::unate") << lowerBound <<" -> " << result << std::endl; return result; } + +}; /* namesapce arith */ +}; /* namespace theory */ +}; /* namespace CVC4 */ diff --git a/src/theory/arith/difference_manager.h b/src/theory/arith/difference_manager.h index 46b070651..c6e7f314d 100644 --- a/src/theory/arith/difference_manager.h +++ b/src/theory/arith/difference_manager.h @@ -5,7 +5,7 @@ #ifndef __CVC4__THEORY__ARITH__DIFFERENCE_MANAGER_H #define __CVC4__THEORY__ARITH__DIFFERENCE_MANAGER_H -#include "theory/arith/arith_utilities.h" +#include "theory/arith/arithvar.h" #include "theory/uf/equality_engine.h" #include "context/cdo.h" #include "context/cdlist.h" diff --git a/src/theory/arith/dio_solver.h b/src/theory/arith/dio_solver.h index da41d94cd..677040615 100644 --- a/src/theory/arith/dio_solver.h +++ b/src/theory/arith/dio_solver.h @@ -25,7 +25,6 @@ #include "theory/arith/tableau.h" #include "theory/arith/partial_model.h" -#include "theory/arith/arith_utilities.h" #include "util/rational.h" #include "util/stats.h" diff --git a/src/theory/arith/linear_equality.h b/src/theory/arith/linear_equality.h index aa8a49238..4d1d917b3 100644 --- a/src/theory/arith/linear_equality.h +++ b/src/theory/arith/linear_equality.h @@ -33,7 +33,7 @@ #define __CVC4__THEORY__ARITH__LINEAR_EQUALITY_H #include "theory/arith/delta_rational.h" -#include "theory/arith/arith_utilities.h" +#include "theory/arith/arithvar.h" #include "theory/arith/partial_model.h" #include "theory/arith/tableau.h" diff --git a/src/theory/arith/ordered_set.h b/src/theory/arith/ordered_set.h index e3eebae5c..8887daa8d 100644 --- a/src/theory/arith/ordered_set.h +++ b/src/theory/arith/ordered_set.h @@ -109,13 +109,6 @@ typedef std::map BoundValueSet; typedef std::set EqualValueSet; -// struct SetCleanupStrategy{ -// static void cleanup(OrderedSet* l){ -// Debug("arithgc") << "cleaning up " << l << "\n"; -// delete l; -// } -// }; - }/* CVC4::theory::arith namespace */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ diff --git a/src/theory/arith/partial_model.cpp b/src/theory/arith/partial_model.cpp index f113c4d34..65b0083d9 100644 --- a/src/theory/arith/partial_model.cpp +++ b/src/theory/arith/partial_model.cpp @@ -23,9 +23,10 @@ using namespace std; -using namespace CVC4; -using namespace CVC4::theory; -using namespace CVC4::theory::arith; +namespace CVC4 { +namespace theory { +namespace arith { + bool ArithPartialModel::boundsAreEqual(ArithVar x){ @@ -395,3 +396,7 @@ void ArithPartialModel::computeDelta(){ } d_deltaIsSafe = true; } + +}; /* namesapce arith */ +}; /* namespace theory */ +}; /* namespace CVC4 */ diff --git a/src/theory/arith/partial_model.h b/src/theory/arith/partial_model.h index d9fa51d8d..7a2a97726 100644 --- a/src/theory/arith/partial_model.h +++ b/src/theory/arith/partial_model.h @@ -21,7 +21,7 @@ #include "context/context.h" #include "context/cdvector.h" -#include "theory/arith/arith_utilities.h" +#include "theory/arith/arithvar.h" #include "theory/arith/delta_rational.h" #include "expr/attribute.h" #include "expr/node.h" diff --git a/src/theory/arith/simplex.h b/src/theory/arith/simplex.h index d69de3756..39c0bc20b 100644 --- a/src/theory/arith/simplex.h +++ b/src/theory/arith/simplex.h @@ -50,7 +50,7 @@ #ifndef __CVC4__THEORY__ARITH__SIMPLEX_H #define __CVC4__THEORY__ARITH__SIMPLEX_H -#include "theory/arith/arith_utilities.h" +#include "theory/arith/arithvar.h" #include "theory/arith/arith_priority_queue.h" #include "theory/arith/arithvar_set.h" #include "theory/arith/delta_rational.h" diff --git a/src/theory/arith/tableau.h b/src/theory/arith/tableau.h index 321f66c5f..1fcbdf13d 100644 --- a/src/theory/arith/tableau.h +++ b/src/theory/arith/tableau.h @@ -22,7 +22,7 @@ #include "expr/node.h" #include "expr/attribute.h" -#include "theory/arith/arith_utilities.h" +#include "theory/arith/arithvar.h" #include "theory/arith/arithvar_set.h" #include "theory/arith/normal_form.h" diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index bea87fdde..a1d57af66 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -47,14 +47,13 @@ #include using namespace std; - -using namespace CVC4; using namespace CVC4::kind; -using namespace CVC4::theory; -using namespace CVC4::theory::arith; +namespace CVC4 { +namespace theory { +namespace arith { -static const uint32_t RESET_START = 2; +const uint32_t RESET_START = 2; TheoryArith::TheoryArith(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation) : @@ -64,8 +63,6 @@ TheoryArith::TheoryArith(context::Context* c, context::UserContext* u, OutputCha d_learner(d_pbSubstitutions), d_nextIntegerCheckVar(0), d_constantIntegerVariables(c), - d_CivIterator(c,0), - d_varsInDioSolver(c), d_diseq(c), d_partialModel(c, d_differenceManager), d_tableau(), @@ -167,7 +164,7 @@ Node TheoryArith::AssertLower(ArithVar x_i, DeltaRational& c_i, TNode original){ } //TODO Relax to less than? - if(d_partialModel.strictlyLessThanLowerBound(x_i, c_i)){ + if(d_partialModel.lessThanLowerBound(x_i, c_i)){ return Node::null(); } @@ -225,7 +222,7 @@ Node TheoryArith::AssertUpper(ArithVar x_i, DeltaRational& c_i, TNode original){ Debug("arith") << "AssertUpper(" << x_i << " " << c_i << ")"<< std::endl; - if(d_partialModel.strictlyGreaterThanUpperBound(x_i, c_i) ){ // \upperbound(x_i) <= c_i + if(d_partialModel.greaterThanUpperBound(x_i, c_i) ){ // \upperbound(x_i) <= c_i return Node::null(); //sat } @@ -763,21 +760,15 @@ Node TheoryArith::dioCutting(){ } Node TheoryArith::callDioSolver(){ - while(d_CivIterator < d_constantIntegerVariables.size()){ - ArithVar v = d_constantIntegerVariables[d_CivIterator]; - d_CivIterator = d_CivIterator + 1; + while(!d_constantIntegerVariables.empty()){ + ArithVar v = d_constantIntegerVariables.front(); + d_constantIntegerVariables.pop(); Debug("arith::dio") << v << endl; Assert(isInteger(v)); Assert(d_partialModel.boundsAreEqual(v)); - if(d_varsInDioSolver.find(v) != d_varsInDioSolver.end()){ - continue; - }else{ - d_varsInDioSolver.insert(v); - } - TNode lb = d_partialModel.getLowerConstraint(v); TNode ub = d_partialModel.getUpperConstraint(v); @@ -1491,3 +1482,7 @@ void TheoryArith::propagateCandidates(){ propagateCandidate(candidate); } } + +}; /* namesapce arith */ +}; /* namespace theory */ +}; /* namespace CVC4 */ diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h index e6bdbfba0..929ef1173 100644 --- a/src/theory/arith/theory_arith.h +++ b/src/theory/arith/theory_arith.h @@ -24,9 +24,10 @@ #include "context/context.h" #include "context/cdlist.h" #include "context/cdhashset.h" +#include "context/cdqueue.h" #include "expr/node.h" -#include "theory/arith/arith_utilities.h" +#include "theory/arith/arithvar.h" #include "theory/arith/arithvar_set.h" #include "theory/arith/delta_rational.h" #include "theory/arith/tableau.h" @@ -161,18 +162,13 @@ private: /** * Queue of Integer variables that are known to be equal to a constant. */ - context::CDList d_constantIntegerVariables; - /** Iterator over d_constantIntegerVariables. */ - context::CDO d_CivIterator; + context::CDQueue d_constantIntegerVariables; Node callDioSolver(); Node dioCutting(); Comparison mkIntegerEqualityFromAssignment(ArithVar v); - //TODO Replace with a more efficient check - CDArithVarSet d_varsInDioSolver; - /** * If ArithVar v maps to the node n in d_removednode, * then n = (= asNode(v) rhs) where rhs is a term that -- 2.30.2