From: Tim King Date: Sat, 23 Oct 2010 21:47:47 +0000 (+0000) Subject: Removed slack.h, and arith_activity.h. Replaced IsBasicManager with the more general... X-Git-Tag: cvc5-1.0.0~8783 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=237995ce0e7f47b826e26c0afb317cf5e3174879;p=cvc5.git Removed slack.h, and arith_activity.h. Replaced IsBasicManager with the more general ArithVarDenseSet. Renamed NextArithRewriter to ArithRewriter. --- diff --git a/src/theory/arith/Makefile.am b/src/theory/arith/Makefile.am index 665b9be4b..21ec99390 100644 --- a/src/theory/arith/Makefile.am +++ b/src/theory/arith/Makefile.am @@ -7,20 +7,18 @@ noinst_LTLIBRARIES = libarith.la libarith_la_SOURCES = \ theory_arith_type_rules.h \ - next_arith_rewriter.h \ - next_arith_rewriter.cpp \ + arith_rewriter.h \ + arith_rewriter.cpp \ normal_form.h\ normal_form.cpp \ arith_utilities.h \ arith_constants.h \ - arith_activity.h \ delta_rational.h \ delta_rational.cpp \ partial_model.h \ partial_model.cpp \ ordered_bounds_list.h \ - basic.h \ - slack.h \ + arithvar_dense_set.h \ tableau.h \ tableau.cpp \ arith_propagator.h \ diff --git a/src/theory/arith/arith_activity.h b/src/theory/arith/arith_activity.h deleted file mode 100644 index 7db3d7d8f..000000000 --- a/src/theory/arith/arith_activity.h +++ /dev/null @@ -1,67 +0,0 @@ -/********************* */ -/*! \file arith_activity.h - ** \verbatim - ** Original author: taking - ** Major contributors: mdeters - ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 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 [[ Add one-line brief description here ]] - ** - ** [[ Add lengthier description here ]] - ** \todo document this file - **/ - -#include "cvc4_private.h" - -#ifndef __CVC4__THEORY__ARITH__ARITH_ACTIVITY_H -#define __CVC4__THEORY__ARITH__ARITH_ACTIVITY_H - -#include "expr/node.h" -#include "expr/attribute.h" - -namespace CVC4 { -namespace theory { -namespace arith { - - -class ActivityMonitor { -private: - std::vector d_activities; - -public: - const static uint64_t ACTIVITY_THRESHOLD = 100; - - ActivityMonitor() : d_activities() {} - - void resetActivity(ArithVar var){ - d_activities[var] = 0; - } - - void initActivity(ArithVar var){ - Assert(var == d_activities.size()); - d_activities.push_back(0); - } - - uint64_t getActivity(ArithVar var) const{ - return d_activities[var]; - } - - inline void increaseActivity(ArithVar var, uint64_t x){ - d_activities[var] += x; - } - -}; - - -}; /* namesapce arith */ -}; /* namespace theory */ -}; /* namespace CVC4 */ - - -#endif diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp new file mode 100644 index 000000000..9f4388b54 --- /dev/null +++ b/src/theory/arith/arith_rewriter.cpp @@ -0,0 +1,326 @@ +/********************* */ +/*! \file arith_rewriter.cpp + ** \verbatim + ** Original author: taking + ** Major contributors: none + ** Minor contributors (to current version): mdeters + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010 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 [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ + + +#include "theory/theory.h" +#include "theory/arith/normal_form.h" +#include "theory/arith/arith_rewriter.h" +#include "theory/arith/arith_utilities.h" + +#include +#include +#include + + +using namespace CVC4; +using namespace CVC4::theory; +using namespace CVC4::theory::arith; + +bool isVariable(TNode t){ + return t.getMetaKind() == kind::metakind::VARIABLE; +} + +RewriteResponse ArithRewriter::rewriteConstant(TNode t){ + Assert(t.getMetaKind() == kind::metakind::CONSTANT); + Node val = coerceToRationalNode(t); + + return RewriteComplete(val); +} + +RewriteResponse ArithRewriter::rewriteVariable(TNode t){ + Assert(isVariable(t)); + + return RewriteComplete(t); +} + +RewriteResponse ArithRewriter::rewriteMinus(TNode t, bool pre){ + Assert(t.getKind()== kind::MINUS); + + if(t[0] == t[1]) return RewriteComplete(d_constants->d_ZERO_NODE); + + Node noMinus = makeSubtractionNode(t[0],t[1]); + if(pre){ + return RewriteComplete(noMinus); + }else{ + return FullRewriteNeeded(noMinus); + } +} + +RewriteResponse ArithRewriter::rewriteUMinus(TNode t, bool pre){ + Assert(t.getKind()== kind::UMINUS); + + Node noUminus = makeUnaryMinusNode(t[0]); + if(pre) + return RewriteComplete(noUminus); + else + return RewriteAgain(noUminus); +} + +RewriteResponse ArithRewriter::preRewriteTerm(TNode t){ + if(t.getMetaKind() == kind::metakind::CONSTANT){ + return rewriteConstant(t); + }else if(isVariable(t)){ + return rewriteVariable(t); + }else if(t.getKind() == kind::MINUS){ + return rewriteMinus(t, true); + }else if(t.getKind() == kind::UMINUS){ + return rewriteUMinus(t, true); + }else if(t.getKind() == kind::DIVISION){ + if(t[0].getKind()== kind::CONST_RATIONAL){ + return rewriteDivByConstant(t, true); + }else{ + return RewriteComplete(t); + } + }else if(t.getKind() == kind::PLUS){ + return preRewritePlus(t); + }else if(t.getKind() == kind::MULT){ + return preRewriteMult(t); + }else{ + Unreachable(); + } +} +RewriteResponse ArithRewriter::postRewriteTerm(TNode t){ + if(t.getMetaKind() == kind::metakind::CONSTANT){ + return rewriteConstant(t); + }else if(isVariable(t)){ + return rewriteVariable(t); + }else if(t.getKind() == kind::MINUS){ + return rewriteMinus(t, false); + }else if(t.getKind() == kind::UMINUS){ + return rewriteUMinus(t, false); + }else if(t.getKind() == kind::DIVISION){ + return rewriteDivByConstant(t, false); + }else if(t.getKind() == kind::PLUS){ + return postRewritePlus(t); + }else if(t.getKind() == kind::MULT){ + return postRewriteMult(t); + }else{ + Unreachable(); + } +} + +RewriteResponse ArithRewriter::preRewriteMult(TNode t){ + Assert(t.getKind()== kind::MULT); + + // Rewrite multiplications with a 0 argument and to 0 + Integer intZero; + + for(TNode::iterator i = t.begin(); i != t.end(); ++i) { + if((*i).getKind() == kind::CONST_RATIONAL) { + if((*i).getConst() == d_constants->d_ZERO) { + return RewriteComplete(d_constants->d_ZERO_NODE); + } + } else if((*i).getKind() == kind::CONST_INTEGER) { + if((*i).getConst() == intZero) { + if(t.getType().isInteger()) { + return RewriteComplete(NodeManager::currentNM()->mkConst(intZero)); + } else { + return RewriteComplete(d_constants->d_ZERO_NODE); + } + } + } + } + return RewriteComplete(t); +} +RewriteResponse ArithRewriter::preRewritePlus(TNode t){ + Assert(t.getKind()== kind::PLUS); + + return RewriteComplete(t); +} + +RewriteResponse ArithRewriter::postRewritePlus(TNode t){ + Assert(t.getKind()== kind::PLUS); + + Polynomial res = Polynomial::mkZero(); + + for(TNode::iterator i = t.begin(), end = t.end(); i != end; ++i){ + Node curr = *i; + Polynomial currPoly = Polynomial::parsePolynomial(curr); + + res = res + currPoly; + } + + return RewriteComplete(res.getNode()); +} + +RewriteResponse ArithRewriter::postRewriteMult(TNode t){ + Assert(t.getKind()== kind::MULT); + + Polynomial res = Polynomial::mkOne(); + + for(TNode::iterator i = t.begin(), end = t.end(); i != end; ++i){ + Node curr = *i; + Polynomial currPoly = Polynomial::parsePolynomial(curr); + + res = res * currPoly; + } + + return RewriteComplete(res.getNode()); +} + +RewriteResponse ArithRewriter::postRewriteAtomConstantRHS(TNode t){ + TNode left = t[0]; + TNode right = t[1]; + + + Comparison cmp = Comparison::mkComparison(t.getKind(), Polynomial::parsePolynomial(left), Constant(right)); + + if(cmp.isBoolean()){ + return RewriteComplete(cmp.getNode()); + } + + if(cmp.getLeft().containsConstant()){ + Monomial constantHead = cmp.getLeft().getHead(); + Assert(constantHead.isConstant()); + + Constant constant = constantHead.getConstant(); + + Constant negativeConstantHead = -constant; + + cmp = cmp.addConstant(negativeConstantHead); + } + Assert(!cmp.getLeft().containsConstant()); + + if(!cmp.getLeft().getHead().coefficientIsOne()){ + Monomial constantHead = cmp.getLeft().getHead(); + Assert(!constantHead.isConstant()); + Constant constant = constantHead.getConstant(); + + Constant inverse = Constant::mkConstant(constant.getValue().inverse()); + + cmp = cmp.multiplyConstant(inverse); + } + Assert(cmp.getLeft().getHead().coefficientIsOne()); + + Assert(cmp.isBoolean() || cmp.isNormalForm()); + return RewriteComplete(cmp.getNode()); +} + +RewriteResponse ArithRewriter::postRewriteAtom(TNode atom){ + // left |><| right + TNode left = atom[0]; + TNode right = atom[1]; + + if(right.getMetaKind() == kind::metakind::CONSTANT){ + return postRewriteAtomConstantRHS(atom); + }else{ + //Transform this to: (left - right) |><| 0 + Node diff = makeSubtractionNode(left, right); + Node reduction = NodeManager::currentNM()->mkNode(atom.getKind(), diff, d_constants->d_ZERO_NODE); + return FullRewriteNeeded(reduction); + } +} + +RewriteResponse ArithRewriter::preRewriteAtom(TNode atom){ + Assert(isAtom(atom)); + NodeManager* currNM = NodeManager::currentNM(); + + if(atom.getKind() == kind::EQUAL) { + if(atom[0] == atom[1]) { + return RewriteComplete(currNM->mkConst(true)); + } + } + + Node reduction = atom; + + if(atom[1].getMetaKind() != kind::metakind::CONSTANT){ + // left |><| right + TNode left = atom[0]; + TNode right = atom[1]; + + //Transform this to: (left - right) |><| 0 + Node diff = makeSubtractionNode(left, right); + reduction = currNM->mkNode(atom.getKind(), diff, d_constants->d_ZERO_NODE); + } + + if(reduction.getKind() == kind::GT){ + Node leq = currNM->mkNode(kind::LEQ, reduction[0], reduction[1]); + reduction = currNM->mkNode(kind::NOT, leq); + }else if(reduction.getKind() == kind::LT){ + Node geq = currNM->mkNode(kind::GEQ, reduction[0], reduction[1]); + reduction = currNM->mkNode(kind::NOT, geq); + } + + return RewriteComplete(reduction); +} + +RewriteResponse ArithRewriter::postRewrite(TNode t){ + if(isTerm(t)){ + RewriteResponse response = postRewriteTerm(t); + if(Debug.isOn("arith::rewriter") && response.isDone()) { + Polynomial::parsePolynomial(response.getNode()); + } + return response; + }else if(isAtom(t)){ + RewriteResponse response = postRewriteAtom(t); + if(Debug.isOn("arith::rewriter") && response.isDone()) { + Comparison::parseNormalForm(response.getNode()); + } + return response; + }else{ + Unreachable(); + return RewriteComplete(Node::null()); + } +} + +RewriteResponse ArithRewriter::preRewrite(TNode t){ + if(isTerm(t)){ + return preRewriteTerm(t); + }else if(isAtom(t)){ + return preRewriteAtom(t); + }else{ + Unreachable(); + return RewriteComplete(Node::null()); + } +} + +Node ArithRewriter::makeUnaryMinusNode(TNode n){ + return NodeManager::currentNM()->mkNode(kind::MULT,d_constants->d_NEGATIVE_ONE_NODE,n); +} + +Node ArithRewriter::makeSubtractionNode(TNode l, TNode r){ + Node negR = makeUnaryMinusNode(r); + Node diff = NodeManager::currentNM()->mkNode(kind::PLUS, l, negR); + + return diff; +} + +RewriteResponse ArithRewriter::rewriteDivByConstant(TNode t, bool pre){ + Assert(t.getKind()== kind::DIVISION); + + Node left = t[0]; + Node right = t[1]; + Assert(right.getKind()== kind::CONST_RATIONAL); + + + const Rational& den = right.getConst(); + + Assert(den != d_constants->d_ZERO); + + Rational div = den.inverse(); + + Node result = mkRationalNode(div); + + Node mult = NodeManager::currentNM()->mkNode(kind::MULT,left,result); + if(pre){ + return RewriteComplete(mult); + }else{ + return RewriteAgain(mult); + } +} diff --git a/src/theory/arith/arith_rewriter.h b/src/theory/arith/arith_rewriter.h new file mode 100644 index 000000000..f7ef8c0c7 --- /dev/null +++ b/src/theory/arith/arith_rewriter.h @@ -0,0 +1,74 @@ +/********************* */ +/*! \file arith_rewriter.h + ** \verbatim + ** Original author: taking + ** Major contributors: mdeters + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010 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 [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ + +#include "theory/arith/arith_constants.h" +#include "theory/theory.h" +#include "theory/arith/normal_form.h" + +#ifndef __CVC4__THEORY__ARITH__REWRITER_H +#define __CVC4__THEORY__ARITH__REWRITER_H + +namespace CVC4 { +namespace theory { +namespace arith { + +class ArithRewriter{ +private: + ArithConstants* d_constants; + + Node makeSubtractionNode(TNode l, TNode r); + Node makeUnaryMinusNode(TNode n); + + RewriteResponse preRewriteTerm(TNode t); + RewriteResponse postRewriteTerm(TNode t); + + RewriteResponse rewriteVariable(TNode t); + RewriteResponse rewriteConstant(TNode t); + RewriteResponse rewriteMinus(TNode t, bool pre); + RewriteResponse rewriteUMinus(TNode t, bool pre); + RewriteResponse rewriteDivByConstant(TNode t, bool pre); + + RewriteResponse preRewritePlus(TNode t); + RewriteResponse postRewritePlus(TNode t); + + RewriteResponse preRewriteMult(TNode t); + RewriteResponse postRewriteMult(TNode t); + + + RewriteResponse preRewriteAtom(TNode t); + RewriteResponse postRewriteAtom(TNode t); + RewriteResponse postRewriteAtomConstantRHS(TNode t); + +public: + ArithRewriter(ArithConstants* ac) : d_constants(ac) {} + + RewriteResponse preRewrite(TNode n); + RewriteResponse postRewrite(TNode n); + +private: + bool isAtom(TNode n) const { return isRelationOperator(n.getKind()); } + bool isTerm(TNode n) const { return !isAtom(n); } +}; + + +}; /* namesapce arith */ +}; /* namespace theory */ +}; /* namespace CVC4 */ + +#endif /* __CVC4__THEORY__ARITH__REWRITER_H */ diff --git a/src/theory/arith/arith_utilities.h b/src/theory/arith/arith_utilities.h index c764d0d2e..d50c48552 100644 --- a/src/theory/arith/arith_utilities.h +++ b/src/theory/arith/arith_utilities.h @@ -25,6 +25,7 @@ #include "util/rational.h" #include "expr/node.h" #include "expr/attribute.h" +#include #include #include @@ -55,6 +56,9 @@ inline void setArithVar(TNode x, ArithVar a){ return x.setAttribute(ArithVarAttr(), (uint64_t)a); } +typedef std::vector ActivityMonitor; + + inline Node mkRationalNode(const Rational& q){ return NodeManager::currentNM()->mkConst(q); } diff --git a/src/theory/arith/arithvar_dense_set.h b/src/theory/arith/arithvar_dense_set.h new file mode 100644 index 000000000..274246fbe --- /dev/null +++ b/src/theory/arith/arithvar_dense_set.h @@ -0,0 +1,72 @@ +/********************* */ +/*! \file arithvar_dense_set.h + ** \verbatim + ** Original author: taking + ** Major contributors: mdeters + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010 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 [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ + +#include +#include "theory/arith/arith_utilities.h" + + +#ifndef __CVC4__THEORY__ARITH__ARTIHVAR_DENSE_SET_H +#define __CVC4__THEORY__ARITH__ARTIHVAR_DENSE_SET_H + +namespace CVC4 { +namespace theory { +namespace arith { + +class ArithVarDenseSet { +private: + std::vector d_set; + +public: + ArithVarDenseSet() : d_set() {} + + size_t size() const { + return d_set.size(); + } + + void increaseSize(ArithVar max){ + Assert(max >= size()); + d_set.resize(max+1, false); + } + + bool isMember(ArithVar x) const{ + return d_set[x]; + } + + void init(ArithVar x, bool val) { + Assert(x >= size()); + increaseSize(x); + d_set[x] = val; + } + + void add(ArithVar x){ + Assert(!isMember(x)); + d_set[x] = true; + } + + void remove(ArithVar x){ + Assert(isMember(x)); + d_set[x] = false; + } +}; + +}; /* namespace arith */ +}; /* namespace theory */ +}; /* namespace CVC4 */ + +#endif /* __CVC4__THEORY__ARITH__ARTIHVAR_DENSE_SET_H */ diff --git a/src/theory/arith/basic.h b/src/theory/arith/basic.h deleted file mode 100644 index c52e0881d..000000000 --- a/src/theory/arith/basic.h +++ /dev/null @@ -1,63 +0,0 @@ -/********************* */ -/*! \file basic.h - ** \verbatim - ** Original author: taking - ** Major contributors: mdeters - ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 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 [[ Add one-line brief description here ]] - ** - ** [[ Add lengthier description here ]] - ** \todo document this file - **/ - - -#include "expr/node.h" -#include "expr/attribute.h" - - -#ifndef __CVC4__THEORY__ARITH__BASIC_H -#define __CVC4__THEORY__ARITH__BASIC_H - -namespace CVC4 { -namespace theory { -namespace arith { - -class IsBasicManager { -private: - std::vector d_basic; - -public: - IsBasicManager() : d_basic() {} - - void init(ArithVar var, bool value){ - Assert(var == d_basic.size()); - d_basic.push_back(value); - } - - bool isBasic(ArithVar x) const{ - return d_basic[x]; - } - - void makeBasic(ArithVar x){ - Assert(!isBasic(x)); - d_basic[x] = true; - } - - void makeNonbasic(ArithVar x){ - Assert(isBasic(x)); - d_basic[x] = false; - } -}; - -}; /* namespace arith */ -}; /* namespace theory */ -}; /* namespace CVC4 */ - -#endif /* __CVC4__THEORY__ARITH__BASIC_H */ diff --git a/src/theory/arith/next_arith_rewriter.cpp b/src/theory/arith/next_arith_rewriter.cpp deleted file mode 100644 index 29fae233b..000000000 --- a/src/theory/arith/next_arith_rewriter.cpp +++ /dev/null @@ -1,326 +0,0 @@ -/********************* */ -/*! \file next_arith_rewriter.cpp - ** \verbatim - ** Original author: taking - ** Major contributors: none - ** Minor contributors (to current version): mdeters - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 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 [[ Add one-line brief description here ]] - ** - ** [[ Add lengthier description here ]] - ** \todo document this file - **/ - - -#include "theory/theory.h" -#include "theory/arith/normal_form.h" -#include "theory/arith/next_arith_rewriter.h" -#include "theory/arith/arith_utilities.h" - -#include -#include -#include - - -using namespace CVC4; -using namespace CVC4::theory; -using namespace CVC4::theory::arith; - -bool isVariable(TNode t){ - return t.getMetaKind() == kind::metakind::VARIABLE; -} - -RewriteResponse NextArithRewriter::rewriteConstant(TNode t){ - Assert(t.getMetaKind() == kind::metakind::CONSTANT); - Node val = coerceToRationalNode(t); - - return RewriteComplete(val); -} - -RewriteResponse NextArithRewriter::rewriteVariable(TNode t){ - Assert(isVariable(t)); - - return RewriteComplete(t); -} - -RewriteResponse NextArithRewriter::rewriteMinus(TNode t, bool pre){ - Assert(t.getKind()== kind::MINUS); - - if(t[0] == t[1]) return RewriteComplete(d_constants->d_ZERO_NODE); - - Node noMinus = makeSubtractionNode(t[0],t[1]); - if(pre){ - return RewriteComplete(noMinus); - }else{ - return FullRewriteNeeded(noMinus); - } -} - -RewriteResponse NextArithRewriter::rewriteUMinus(TNode t, bool pre){ - Assert(t.getKind()== kind::UMINUS); - - Node noUminus = makeUnaryMinusNode(t[0]); - if(pre) - return RewriteComplete(noUminus); - else - return RewriteAgain(noUminus); -} - -RewriteResponse NextArithRewriter::preRewriteTerm(TNode t){ - if(t.getMetaKind() == kind::metakind::CONSTANT){ - return rewriteConstant(t); - }else if(isVariable(t)){ - return rewriteVariable(t); - }else if(t.getKind() == kind::MINUS){ - return rewriteMinus(t, true); - }else if(t.getKind() == kind::UMINUS){ - return rewriteUMinus(t, true); - }else if(t.getKind() == kind::DIVISION){ - if(t[0].getKind()== kind::CONST_RATIONAL){ - return rewriteDivByConstant(t, true); - }else{ - return RewriteComplete(t); - } - }else if(t.getKind() == kind::PLUS){ - return preRewritePlus(t); - }else if(t.getKind() == kind::MULT){ - return preRewriteMult(t); - }else{ - Unreachable(); - } -} -RewriteResponse NextArithRewriter::postRewriteTerm(TNode t){ - if(t.getMetaKind() == kind::metakind::CONSTANT){ - return rewriteConstant(t); - }else if(isVariable(t)){ - return rewriteVariable(t); - }else if(t.getKind() == kind::MINUS){ - return rewriteMinus(t, false); - }else if(t.getKind() == kind::UMINUS){ - return rewriteUMinus(t, false); - }else if(t.getKind() == kind::DIVISION){ - return rewriteDivByConstant(t, false); - }else if(t.getKind() == kind::PLUS){ - return postRewritePlus(t); - }else if(t.getKind() == kind::MULT){ - return postRewriteMult(t); - }else{ - Unreachable(); - } -} - -RewriteResponse NextArithRewriter::preRewriteMult(TNode t){ - Assert(t.getKind()== kind::MULT); - - // Rewrite multiplications with a 0 argument and to 0 - Integer intZero; - - for(TNode::iterator i = t.begin(); i != t.end(); ++i) { - if((*i).getKind() == kind::CONST_RATIONAL) { - if((*i).getConst() == d_constants->d_ZERO) { - return RewriteComplete(d_constants->d_ZERO_NODE); - } - } else if((*i).getKind() == kind::CONST_INTEGER) { - if((*i).getConst() == intZero) { - if(t.getType().isInteger()) { - return RewriteComplete(NodeManager::currentNM()->mkConst(intZero)); - } else { - return RewriteComplete(d_constants->d_ZERO_NODE); - } - } - } - } - return RewriteComplete(t); -} -RewriteResponse NextArithRewriter::preRewritePlus(TNode t){ - Assert(t.getKind()== kind::PLUS); - - return RewriteComplete(t); -} - -RewriteResponse NextArithRewriter::postRewritePlus(TNode t){ - Assert(t.getKind()== kind::PLUS); - - Polynomial res = Polynomial::mkZero(); - - for(TNode::iterator i = t.begin(), end = t.end(); i != end; ++i){ - Node curr = *i; - Polynomial currPoly = Polynomial::parsePolynomial(curr); - - res = res + currPoly; - } - - return RewriteComplete(res.getNode()); -} - -RewriteResponse NextArithRewriter::postRewriteMult(TNode t){ - Assert(t.getKind()== kind::MULT); - - Polynomial res = Polynomial::mkOne(); - - for(TNode::iterator i = t.begin(), end = t.end(); i != end; ++i){ - Node curr = *i; - Polynomial currPoly = Polynomial::parsePolynomial(curr); - - res = res * currPoly; - } - - return RewriteComplete(res.getNode()); -} - -RewriteResponse NextArithRewriter::postRewriteAtomConstantRHS(TNode t){ - TNode left = t[0]; - TNode right = t[1]; - - - Comparison cmp = Comparison::mkComparison(t.getKind(), Polynomial::parsePolynomial(left), Constant(right)); - - if(cmp.isBoolean()){ - return RewriteComplete(cmp.getNode()); - } - - if(cmp.getLeft().containsConstant()){ - Monomial constantHead = cmp.getLeft().getHead(); - Assert(constantHead.isConstant()); - - Constant constant = constantHead.getConstant(); - - Constant negativeConstantHead = -constant; - - cmp = cmp.addConstant(negativeConstantHead); - } - Assert(!cmp.getLeft().containsConstant()); - - if(!cmp.getLeft().getHead().coefficientIsOne()){ - Monomial constantHead = cmp.getLeft().getHead(); - Assert(!constantHead.isConstant()); - Constant constant = constantHead.getConstant(); - - Constant inverse = Constant::mkConstant(constant.getValue().inverse()); - - cmp = cmp.multiplyConstant(inverse); - } - Assert(cmp.getLeft().getHead().coefficientIsOne()); - - Assert(cmp.isBoolean() || cmp.isNormalForm()); - return RewriteComplete(cmp.getNode()); -} - -RewriteResponse NextArithRewriter::postRewriteAtom(TNode atom){ - // left |><| right - TNode left = atom[0]; - TNode right = atom[1]; - - if(right.getMetaKind() == kind::metakind::CONSTANT){ - return postRewriteAtomConstantRHS(atom); - }else{ - //Transform this to: (left - right) |><| 0 - Node diff = makeSubtractionNode(left, right); - Node reduction = NodeManager::currentNM()->mkNode(atom.getKind(), diff, d_constants->d_ZERO_NODE); - return FullRewriteNeeded(reduction); - } -} - -RewriteResponse NextArithRewriter::preRewriteAtom(TNode atom){ - Assert(isAtom(atom)); - NodeManager* currNM = NodeManager::currentNM(); - - if(atom.getKind() == kind::EQUAL) { - if(atom[0] == atom[1]) { - return RewriteComplete(currNM->mkConst(true)); - } - } - - Node reduction = atom; - - if(atom[1].getMetaKind() != kind::metakind::CONSTANT){ - // left |><| right - TNode left = atom[0]; - TNode right = atom[1]; - - //Transform this to: (left - right) |><| 0 - Node diff = makeSubtractionNode(left, right); - reduction = currNM->mkNode(atom.getKind(), diff, d_constants->d_ZERO_NODE); - } - - if(reduction.getKind() == kind::GT){ - Node leq = currNM->mkNode(kind::LEQ, reduction[0], reduction[1]); - reduction = currNM->mkNode(kind::NOT, leq); - }else if(reduction.getKind() == kind::LT){ - Node geq = currNM->mkNode(kind::GEQ, reduction[0], reduction[1]); - reduction = currNM->mkNode(kind::NOT, geq); - } - - return RewriteComplete(reduction); -} - -RewriteResponse NextArithRewriter::postRewrite(TNode t){ - if(isTerm(t)){ - RewriteResponse response = postRewriteTerm(t); - if(Debug.isOn("arith::rewriter") && response.isDone()) { - Polynomial::parsePolynomial(response.getNode()); - } - return response; - }else if(isAtom(t)){ - RewriteResponse response = postRewriteAtom(t); - if(Debug.isOn("arith::rewriter") && response.isDone()) { - Comparison::parseNormalForm(response.getNode()); - } - return response; - }else{ - Unreachable(); - return RewriteComplete(Node::null()); - } -} - -RewriteResponse NextArithRewriter::preRewrite(TNode t){ - if(isTerm(t)){ - return preRewriteTerm(t); - }else if(isAtom(t)){ - return preRewriteAtom(t); - }else{ - Unreachable(); - return RewriteComplete(Node::null()); - } -} - -Node NextArithRewriter::makeUnaryMinusNode(TNode n){ - return NodeManager::currentNM()->mkNode(kind::MULT,d_constants->d_NEGATIVE_ONE_NODE,n); -} - -Node NextArithRewriter::makeSubtractionNode(TNode l, TNode r){ - Node negR = makeUnaryMinusNode(r); - Node diff = NodeManager::currentNM()->mkNode(kind::PLUS, l, negR); - - return diff; -} - -RewriteResponse NextArithRewriter::rewriteDivByConstant(TNode t, bool pre){ - Assert(t.getKind()== kind::DIVISION); - - Node left = t[0]; - Node right = t[1]; - Assert(right.getKind()== kind::CONST_RATIONAL); - - - const Rational& den = right.getConst(); - - Assert(den != d_constants->d_ZERO); - - Rational div = den.inverse(); - - Node result = mkRationalNode(div); - - Node mult = NodeManager::currentNM()->mkNode(kind::MULT,left,result); - if(pre){ - return RewriteComplete(mult); - }else{ - return RewriteAgain(mult); - } -} diff --git a/src/theory/arith/next_arith_rewriter.h b/src/theory/arith/next_arith_rewriter.h deleted file mode 100644 index 1fb743f71..000000000 --- a/src/theory/arith/next_arith_rewriter.h +++ /dev/null @@ -1,74 +0,0 @@ -/********************* */ -/*! \file next_arith_rewriter.h - ** \verbatim - ** Original author: taking - ** Major contributors: mdeters - ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 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 [[ Add one-line brief description here ]] - ** - ** [[ Add lengthier description here ]] - ** \todo document this file - **/ - -#include "theory/arith/arith_constants.h" -#include "theory/theory.h" -#include "theory/arith/normal_form.h" - -#ifndef __CVC4__THEORY__ARITH__REWRITER_NEXT_H -#define __CVC4__THEORY__ARITH__REWRITER_NEXT_H - -namespace CVC4 { -namespace theory { -namespace arith { - -class NextArithRewriter{ -private: - ArithConstants* d_constants; - - Node makeSubtractionNode(TNode l, TNode r); - Node makeUnaryMinusNode(TNode n); - - RewriteResponse preRewriteTerm(TNode t); - RewriteResponse postRewriteTerm(TNode t); - - RewriteResponse rewriteVariable(TNode t); - RewriteResponse rewriteConstant(TNode t); - RewriteResponse rewriteMinus(TNode t, bool pre); - RewriteResponse rewriteUMinus(TNode t, bool pre); - RewriteResponse rewriteDivByConstant(TNode t, bool pre); - - RewriteResponse preRewritePlus(TNode t); - RewriteResponse postRewritePlus(TNode t); - - RewriteResponse preRewriteMult(TNode t); - RewriteResponse postRewriteMult(TNode t); - - - RewriteResponse preRewriteAtom(TNode t); - RewriteResponse postRewriteAtom(TNode t); - RewriteResponse postRewriteAtomConstantRHS(TNode t); - -public: - NextArithRewriter(ArithConstants* ac) : d_constants(ac) {} - - RewriteResponse preRewrite(TNode n); - RewriteResponse postRewrite(TNode n); - -private: - bool isAtom(TNode n) const { return isRelationOperator(n.getKind()); } - bool isTerm(TNode n) const { return !isAtom(n); } -}; - - -}; /* namesapce arith */ -}; /* namespace theory */ -}; /* namespace CVC4 */ - -#endif /* __CVC4__THEORY__ARITH__REWRITER_NEXT_H */ diff --git a/src/theory/arith/slack.h b/src/theory/arith/slack.h deleted file mode 100644 index 87bf83e32..000000000 --- a/src/theory/arith/slack.h +++ /dev/null @@ -1,33 +0,0 @@ -/********************* */ -/*! \file slack.h - ** \verbatim - ** Original author: taking - ** Major contributors: mdeters - ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 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 [[ Add one-line brief description here ]] - ** - ** [[ Add lengthier description here ]] - ** \todo document this file - **/ - - -namespace CVC4 { -namespace theory { -namespace arith { - -struct SlackAttrID; - -typedef expr::Attribute Slack; - - -}; /* namespace arith */ -}; /* namespace theory */ -}; /* namespace CVC4 */ - diff --git a/src/theory/arith/tableau.cpp b/src/theory/arith/tableau.cpp index d6a30ac91..2490ed51b 100644 --- a/src/theory/arith/tableau.cpp +++ b/src/theory/arith/tableau.cpp @@ -108,7 +108,7 @@ void Tableau::addRow(ArithVar basicVar, const std::vector& variables){ Assert(coeffs.size() == variables.size()); - Assert(d_basicManager.isBasic(basicVar)); + Assert(d_basicManager.isMember(basicVar)); //The new basic variable cannot already be a basic variable Assert(!isActiveBasicVariable(basicVar)); @@ -126,7 +126,7 @@ void Tableau::addRow(ArithVar basicVar, for( ; coeffsIter != coeffsEnd; ++coeffsIter, ++ varsIter){ ArithVar var = *varsIter; - if(d_basicManager.isBasic(var)){ + if(d_basicManager.isMember(var)){ if(!isActiveBasicVariable(var)){ reinjectBasic(var); } @@ -139,8 +139,8 @@ void Tableau::addRow(ArithVar basicVar, } void Tableau::pivot(ArithVar x_r, ArithVar x_s){ - Assert(d_basicManager.isBasic(x_r)); - Assert(!d_basicManager.isBasic(x_s)); + Assert(d_basicManager.isMember(x_r)); + Assert(!d_basicManager.isMember(x_s)); Row* row_s = lookup(x_r); Assert(row_s->has(x_s)); @@ -150,10 +150,10 @@ void Tableau::pivot(ArithVar x_r, ArithVar x_s){ d_rowsTable[x_r] = NULL; d_activeBasicVars.erase(x_r); - d_basicManager.makeNonbasic(x_r); + d_basicManager.remove(x_r); d_activeBasicVars.insert(x_s); - d_basicManager.makeBasic(x_s); + d_basicManager.add(x_s); row_s->pivot(x_s); @@ -162,7 +162,7 @@ void Tableau::pivot(ArithVar x_r, ArithVar x_s){ ArithVar basic = *basicIter; Row* row_k = lookup(basic); if(row_k->has(x_s)){ - d_activityMonitor.increaseActivity(basic, 30); + d_activityMonitor[basic] += 30; row_k->substitute(*row_s); } } @@ -185,7 +185,7 @@ void Tableau::updateRow(Row* row){ for(Row::iterator i=row->begin(), endIter = row->end(); i != endIter; ){ ArithVar var = i->first; ++i; - if(d_basicManager.isBasic(var)){ + if(d_basicManager.isMember(var)){ Row* row_var = isActiveBasicVariable(var) ? lookup(var) : lookupEjected(var); Assert(row_var != row); diff --git a/src/theory/arith/tableau.h b/src/theory/arith/tableau.h index 88a5c2317..588b521b1 100644 --- a/src/theory/arith/tableau.h +++ b/src/theory/arith/tableau.h @@ -22,8 +22,7 @@ #include "expr/attribute.h" #include "theory/arith/arith_utilities.h" -#include "theory/arith/arith_activity.h" -#include "theory/arith/basic.h" +#include "theory/arith/arithvar_dense_set.h" #include "theory/arith/normal_form.h" #include @@ -144,14 +143,15 @@ private: ArithVarSet d_activeBasicVars; RowsTable d_rowsTable; + ActivityMonitor& d_activityMonitor; - IsBasicManager& d_basicManager; + ArithVarDenseSet& d_basicManager; public: /** * Constructs an empty tableau. */ - Tableau(ActivityMonitor &am, IsBasicManager& bm) : + Tableau(ActivityMonitor &am, ArithVarDenseSet& bm) : d_activeBasicVars(), d_rowsTable(), d_activityMonitor(am), @@ -196,18 +196,18 @@ public: void printTableau(); bool isEjected(ArithVar var){ - return d_basicManager.isBasic(var) && !isActiveBasicVariable(var); + return d_basicManager.isMember(var) && !isActiveBasicVariable(var); } void ejectBasic(ArithVar basic){ - Assert(d_basicManager.isBasic(basic)); + Assert(d_basicManager.isMember(basic)); Assert(isActiveBasicVariable(basic)); d_activeBasicVars.erase(basic); } void reinjectBasic(ArithVar basic){ - Assert(d_basicManager.isBasic(basic)); + Assert(d_basicManager.isMember(basic)); Assert(isEjected(basic)); Row* row = lookupEjected(basic); diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index f913eda93..bd686737a 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -31,11 +31,9 @@ #include "theory/arith/delta_rational.h" #include "theory/arith/partial_model.h" #include "theory/arith/tableau.h" -#include "theory/arith/slack.h" -#include "theory/arith/basic.h" -#include "theory/arith/arith_activity.h" +#include "theory/arith/arithvar_dense_set.h" -#include "theory/arith/next_arith_rewriter.h" +#include "theory/arith/arith_rewriter.h" #include "theory/arith/arith_propagator.h" #include "theory/arith/theory_arith.h" @@ -52,7 +50,10 @@ using namespace CVC4::kind; using namespace CVC4::theory; using namespace CVC4::theory::arith; +struct SlackAttrID; +typedef expr::Attribute Slack; +const static uint64_t ACTIVITY_THRESHOLD = 100; TheoryArith::TheoryArith(int id, context::Context* c, OutputChannel& out) : Theory(id, c, out), @@ -62,7 +63,7 @@ TheoryArith::TheoryArith(int id, context::Context* c, OutputChannel& out) : d_activityMonitor(), d_diseq(c), d_tableau(d_activityMonitor, d_basicManager), - d_nextRewriter(&d_constants), + d_rewriter(&d_constants), d_propagator(c), d_statistics() {} @@ -133,7 +134,7 @@ bool TheoryArith::shouldEject(ArithVar var){ return false; }else if(!d_partialModel.hasEverHadABound(var)){ return true; - }else if(d_activityMonitor.getActivity(var) >= ActivityMonitor::ACTIVITY_THRESHOLD){ + }else if(d_activityMonitor[var] >= ACTIVITY_THRESHOLD){ return true; } return false; @@ -159,7 +160,7 @@ void TheoryArith::ejectInactiveVariables(){ //TNode var = *i; //ArithVar variable = asArithVar(var); if(shouldEject(variable)){ - if(d_basicManager.isBasic(variable)){ + if(d_basicManager.isMember(variable)){ Debug("decay") << "ejecting basic " << variable << endl;; d_tableau.ejectBasic(variable); } @@ -228,7 +229,7 @@ void TheoryArith::preRegisterTerm(TNode n) { void TheoryArith::checkBasicVariable(ArithVar basic){ - Assert(d_basicManager.isBasic(basic)); + Assert(d_basicManager.isMember(basic)); if(!d_partialModel.assignmentIsConsistent(basic)){ d_possiblyInconsistent.push(basic); } @@ -247,8 +248,10 @@ ArithVar TheoryArith::requestArithVar(TNode x, bool basic){ setArithVar(x,varX); - d_activityMonitor.initActivity(varX); - d_basicManager.init(varX, basic); + Assert(varX == d_activityMonitor.size()); + d_activityMonitor.push_back(0); + + d_basicManager.init(varX,basic); d_tableau.increaseSize(); Debug("arith::arithvar") << x << " |-> " << varX << endl; @@ -299,7 +302,7 @@ void TheoryArith::setupSlack(TNode left){ */ void TheoryArith::setupInitialValue(ArithVar x){ - if(!d_basicManager.isBasic(x)){ + if(!d_basicManager.isMember(x)){ d_partialModel.initialize(x,d_constants.d_ZERO_DELTA); }else{ //If the variable is basic, assertions may have already happened and updates @@ -325,7 +328,7 @@ void TheoryArith::setupInitialValue(ArithVar x){ * Computes the value of a basic variable using the current assignment. */ DeltaRational TheoryArith::computeRowValue(ArithVar x, bool useSafe){ - Assert(d_basicManager.isBasic(x)); + Assert(d_basicManager.isMember(x)); DeltaRational sum = d_constants.d_ZERO_DELTA; Row* row = d_tableau.lookup(x); @@ -341,7 +344,7 @@ DeltaRational TheoryArith::computeRowValue(ArithVar x, bool useSafe){ RewriteResponse TheoryArith::preRewrite(TNode n, bool topLevel) { - return d_nextRewriter.preRewrite(n); + return d_rewriter.preRewrite(n); } void TheoryArith::registerTerm(TNode tn){ @@ -352,7 +355,7 @@ void TheoryArith::registerTerm(TNode tn){ bool TheoryArith::AssertUpper(ArithVar x_i, const DeltaRational& c_i, TNode original){ Debug("arith") << "AssertUpper(" << x_i << " " << c_i << ")"<< std::endl; - if(d_basicManager.isBasic(x_i) && d_tableau.isEjected(x_i)){ + if(d_basicManager.isMember(x_i) && d_tableau.isEjected(x_i)){ reinjectVariable(x_i); } @@ -371,9 +374,9 @@ bool TheoryArith::AssertUpper(ArithVar x_i, const DeltaRational& c_i, TNode orig d_partialModel.setUpperConstraint(x_i,original); d_partialModel.setUpperBound(x_i, c_i); - d_activityMonitor.resetActivity(x_i); + d_activityMonitor[x_i] = 0; - if(!d_basicManager.isBasic(x_i)){ + if(!d_basicManager.isMember(x_i)){ if(d_partialModel.getAssignment(x_i) > c_i){ update(x_i, c_i); } @@ -388,7 +391,7 @@ bool TheoryArith::AssertUpper(ArithVar x_i, const DeltaRational& c_i, TNode orig bool TheoryArith::AssertLower(ArithVar x_i, const DeltaRational& c_i, TNode original){ Debug("arith") << "AssertLower(" << x_i << " " << c_i << ")"<< std::endl; - if(d_basicManager.isBasic(x_i) && d_tableau.isEjected(x_i)){ + if(d_basicManager.isMember(x_i) && d_tableau.isEjected(x_i)){ reinjectVariable(x_i); } @@ -406,9 +409,9 @@ bool TheoryArith::AssertLower(ArithVar x_i, const DeltaRational& c_i, TNode orig d_partialModel.setLowerConstraint(x_i,original); d_partialModel.setLowerBound(x_i, c_i); - d_activityMonitor.resetActivity(x_i); + d_activityMonitor[x_i] = 0; - if(!d_basicManager.isBasic(x_i)){ + if(!d_basicManager.isMember(x_i)){ if(d_partialModel.getAssignment(x_i) < c_i){ update(x_i, c_i); } @@ -424,7 +427,7 @@ bool TheoryArith::AssertEquality(ArithVar x_i, const DeltaRational& c_i, TNode o Debug("arith") << "AssertEquality(" << x_i << " " << c_i << ")"<< std::endl; - if(d_basicManager.isBasic(x_i) && d_tableau.isEjected(x_i)){ + if(d_basicManager.isMember(x_i) && d_tableau.isEjected(x_i)){ reinjectVariable(x_i); } @@ -456,9 +459,9 @@ bool TheoryArith::AssertEquality(ArithVar x_i, const DeltaRational& c_i, TNode o d_partialModel.setUpperConstraint(x_i,original); d_partialModel.setUpperBound(x_i, c_i); - d_activityMonitor.resetActivity(x_i); + d_activityMonitor[x_i] = 0; - if(!d_basicManager.isBasic(x_i)){ + if(!d_basicManager.isMember(x_i)){ if(!(d_partialModel.getAssignment(x_i) == c_i)){ update(x_i, c_i); } @@ -469,7 +472,7 @@ bool TheoryArith::AssertEquality(ArithVar x_i, const DeltaRational& c_i, TNode o return false; } void TheoryArith::update(ArithVar x_i, const DeltaRational& v){ - Assert(!d_basicManager.isBasic(x_i)); + Assert(!d_basicManager.isMember(x_i)); DeltaRational assignment_x_i = d_partialModel.getAssignment(x_i); ++(d_statistics.d_statUpdates); @@ -490,7 +493,7 @@ void TheoryArith::update(ArithVar x_i, const DeltaRational& v){ DeltaRational nAssignment = assignment+(diff * a_ji); d_partialModel.setAssignment(x_j, nAssignment); - d_activityMonitor.increaseActivity(x_j, 1); + d_activityMonitor[x_j] += 1; checkBasicVariable(x_j); } @@ -532,7 +535,7 @@ void TheoryArith::pivotAndUpdate(ArithVar x_i, ArithVar x_j, DeltaRational& v){ DeltaRational nextAssignment = d_partialModel.getAssignment(x_k) + (theta * a_kj); d_partialModel.setAssignment(x_k, nextAssignment); - d_activityMonitor.increaseActivity(x_j, 1); + d_activityMonitor[x_j] += 1; checkBasicVariable(x_k); } @@ -556,7 +559,7 @@ ArithVar TheoryArith::selectSmallestInconsistentVar(){ while(!d_possiblyInconsistent.empty()){ ArithVar var = d_possiblyInconsistent.top(); Debug("arith_update") << "possiblyInconsistent var" << var << endl; - if(d_basicManager.isBasic(var)){ + if(d_basicManager.isMember(var)){ if(!d_partialModel.assignmentIsConsistent(var)){ return var; } @@ -834,7 +837,7 @@ void TheoryArith::check(Effort level){ for (ArithVar i = 0; i < d_variables.size(); ++ i) { Debug("arith::print_model") << d_variables[i] << " : " << d_partialModel.getAssignment(i); - if(d_basicManager.isBasic(i)) + if(d_basicManager.isMember(i)) Debug("arith::print_model") << " (basic)"; Debug("arith::print_model") << endl; } diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h index 5d00c4cc8..5395327c0 100644 --- a/src/theory/arith/theory_arith.h +++ b/src/theory/arith/theory_arith.h @@ -27,11 +27,10 @@ #include "expr/node.h" #include "theory/arith/arith_utilities.h" -#include "theory/arith/basic.h" -#include "theory/arith/arith_activity.h" +#include "theory/arith/arithvar_dense_set.h" #include "theory/arith/delta_rational.h" #include "theory/arith/tableau.h" -#include "theory/arith/next_arith_rewriter.h" +#include "theory/arith/arith_rewriter.h" #include "theory/arith/partial_model.h" #include "theory/arith/arith_propagator.h" @@ -80,7 +79,7 @@ private: */ ArithPartialModel d_partialModel; - IsBasicManager d_basicManager; + ArithVarDenseSet d_basicManager; ActivityMonitor d_activityMonitor; /** @@ -96,7 +95,7 @@ private: /** * The rewriter module for arithmetic. */ - NextArithRewriter d_nextRewriter; + ArithRewriter d_rewriter; ArithUnatePropagator d_propagator; @@ -113,7 +112,7 @@ public: * Plug in old rewrite to the new (pre,post)rewrite interface. */ RewriteResponse postRewrite(TNode n, bool topLevel) { - return d_nextRewriter.postRewrite(n); + return d_rewriter.postRewrite(n); } /**