From 237995ce0e7f47b826e26c0afb317cf5e3174879 Mon Sep 17 00:00:00 2001 From: Tim King Date: Sat, 23 Oct 2010 21:47:47 +0000 Subject: [PATCH] Removed slack.h, and arith_activity.h. Replaced IsBasicManager with the more general ArithVarDenseSet. Renamed NextArithRewriter to ArithRewriter. --- src/theory/arith/Makefile.am | 8 +-- src/theory/arith/arith_activity.h | 67 ------------------- ..._arith_rewriter.cpp => arith_rewriter.cpp} | 40 +++++------ ...next_arith_rewriter.h => arith_rewriter.h} | 12 ++-- src/theory/arith/arith_utilities.h | 4 ++ .../arith/{basic.h => arithvar_dense_set.h} | 51 ++++++++------ src/theory/arith/slack.h | 33 --------- src/theory/arith/tableau.cpp | 16 ++--- src/theory/arith/tableau.h | 14 ++-- src/theory/arith/theory_arith.cpp | 57 ++++++++-------- src/theory/arith/theory_arith.h | 11 ++- 11 files changed, 113 insertions(+), 200 deletions(-) delete mode 100644 src/theory/arith/arith_activity.h rename src/theory/arith/{next_arith_rewriter.cpp => arith_rewriter.cpp} (86%) rename src/theory/arith/{next_arith_rewriter.h => arith_rewriter.h} (87%) rename src/theory/arith/{basic.h => arithvar_dense_set.h} (50%) delete mode 100644 src/theory/arith/slack.h 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/next_arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp similarity index 86% rename from src/theory/arith/next_arith_rewriter.cpp rename to src/theory/arith/arith_rewriter.cpp index 29fae233b..9f4388b54 100644 --- a/src/theory/arith/next_arith_rewriter.cpp +++ b/src/theory/arith/arith_rewriter.cpp @@ -1,5 +1,5 @@ /********************* */ -/*! \file next_arith_rewriter.cpp +/*! \file arith_rewriter.cpp ** \verbatim ** Original author: taking ** Major contributors: none @@ -20,7 +20,7 @@ #include "theory/theory.h" #include "theory/arith/normal_form.h" -#include "theory/arith/next_arith_rewriter.h" +#include "theory/arith/arith_rewriter.h" #include "theory/arith/arith_utilities.h" #include @@ -36,20 +36,20 @@ bool isVariable(TNode t){ return t.getMetaKind() == kind::metakind::VARIABLE; } -RewriteResponse NextArithRewriter::rewriteConstant(TNode t){ +RewriteResponse ArithRewriter::rewriteConstant(TNode t){ Assert(t.getMetaKind() == kind::metakind::CONSTANT); Node val = coerceToRationalNode(t); return RewriteComplete(val); } -RewriteResponse NextArithRewriter::rewriteVariable(TNode t){ +RewriteResponse ArithRewriter::rewriteVariable(TNode t){ Assert(isVariable(t)); return RewriteComplete(t); } -RewriteResponse NextArithRewriter::rewriteMinus(TNode t, bool pre){ +RewriteResponse ArithRewriter::rewriteMinus(TNode t, bool pre){ Assert(t.getKind()== kind::MINUS); if(t[0] == t[1]) return RewriteComplete(d_constants->d_ZERO_NODE); @@ -62,7 +62,7 @@ RewriteResponse NextArithRewriter::rewriteMinus(TNode t, bool pre){ } } -RewriteResponse NextArithRewriter::rewriteUMinus(TNode t, bool pre){ +RewriteResponse ArithRewriter::rewriteUMinus(TNode t, bool pre){ Assert(t.getKind()== kind::UMINUS); Node noUminus = makeUnaryMinusNode(t[0]); @@ -72,7 +72,7 @@ RewriteResponse NextArithRewriter::rewriteUMinus(TNode t, bool pre){ return RewriteAgain(noUminus); } -RewriteResponse NextArithRewriter::preRewriteTerm(TNode t){ +RewriteResponse ArithRewriter::preRewriteTerm(TNode t){ if(t.getMetaKind() == kind::metakind::CONSTANT){ return rewriteConstant(t); }else if(isVariable(t)){ @@ -95,7 +95,7 @@ RewriteResponse NextArithRewriter::preRewriteTerm(TNode t){ Unreachable(); } } -RewriteResponse NextArithRewriter::postRewriteTerm(TNode t){ +RewriteResponse ArithRewriter::postRewriteTerm(TNode t){ if(t.getMetaKind() == kind::metakind::CONSTANT){ return rewriteConstant(t); }else if(isVariable(t)){ @@ -115,7 +115,7 @@ RewriteResponse NextArithRewriter::postRewriteTerm(TNode t){ } } -RewriteResponse NextArithRewriter::preRewriteMult(TNode t){ +RewriteResponse ArithRewriter::preRewriteMult(TNode t){ Assert(t.getKind()== kind::MULT); // Rewrite multiplications with a 0 argument and to 0 @@ -138,13 +138,13 @@ RewriteResponse NextArithRewriter::preRewriteMult(TNode t){ } return RewriteComplete(t); } -RewriteResponse NextArithRewriter::preRewritePlus(TNode t){ +RewriteResponse ArithRewriter::preRewritePlus(TNode t){ Assert(t.getKind()== kind::PLUS); return RewriteComplete(t); } -RewriteResponse NextArithRewriter::postRewritePlus(TNode t){ +RewriteResponse ArithRewriter::postRewritePlus(TNode t){ Assert(t.getKind()== kind::PLUS); Polynomial res = Polynomial::mkZero(); @@ -159,7 +159,7 @@ RewriteResponse NextArithRewriter::postRewritePlus(TNode t){ return RewriteComplete(res.getNode()); } -RewriteResponse NextArithRewriter::postRewriteMult(TNode t){ +RewriteResponse ArithRewriter::postRewriteMult(TNode t){ Assert(t.getKind()== kind::MULT); Polynomial res = Polynomial::mkOne(); @@ -174,7 +174,7 @@ RewriteResponse NextArithRewriter::postRewriteMult(TNode t){ return RewriteComplete(res.getNode()); } -RewriteResponse NextArithRewriter::postRewriteAtomConstantRHS(TNode t){ +RewriteResponse ArithRewriter::postRewriteAtomConstantRHS(TNode t){ TNode left = t[0]; TNode right = t[1]; @@ -212,7 +212,7 @@ RewriteResponse NextArithRewriter::postRewriteAtomConstantRHS(TNode t){ return RewriteComplete(cmp.getNode()); } -RewriteResponse NextArithRewriter::postRewriteAtom(TNode atom){ +RewriteResponse ArithRewriter::postRewriteAtom(TNode atom){ // left |><| right TNode left = atom[0]; TNode right = atom[1]; @@ -227,7 +227,7 @@ RewriteResponse NextArithRewriter::postRewriteAtom(TNode atom){ } } -RewriteResponse NextArithRewriter::preRewriteAtom(TNode atom){ +RewriteResponse ArithRewriter::preRewriteAtom(TNode atom){ Assert(isAtom(atom)); NodeManager* currNM = NodeManager::currentNM(); @@ -260,7 +260,7 @@ RewriteResponse NextArithRewriter::preRewriteAtom(TNode atom){ return RewriteComplete(reduction); } -RewriteResponse NextArithRewriter::postRewrite(TNode t){ +RewriteResponse ArithRewriter::postRewrite(TNode t){ if(isTerm(t)){ RewriteResponse response = postRewriteTerm(t); if(Debug.isOn("arith::rewriter") && response.isDone()) { @@ -279,7 +279,7 @@ RewriteResponse NextArithRewriter::postRewrite(TNode t){ } } -RewriteResponse NextArithRewriter::preRewrite(TNode t){ +RewriteResponse ArithRewriter::preRewrite(TNode t){ if(isTerm(t)){ return preRewriteTerm(t); }else if(isAtom(t)){ @@ -290,18 +290,18 @@ RewriteResponse NextArithRewriter::preRewrite(TNode t){ } } -Node NextArithRewriter::makeUnaryMinusNode(TNode n){ +Node ArithRewriter::makeUnaryMinusNode(TNode n){ return NodeManager::currentNM()->mkNode(kind::MULT,d_constants->d_NEGATIVE_ONE_NODE,n); } -Node NextArithRewriter::makeSubtractionNode(TNode l, TNode r){ +Node ArithRewriter::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){ +RewriteResponse ArithRewriter::rewriteDivByConstant(TNode t, bool pre){ Assert(t.getKind()== kind::DIVISION); Node left = t[0]; diff --git a/src/theory/arith/next_arith_rewriter.h b/src/theory/arith/arith_rewriter.h similarity index 87% rename from src/theory/arith/next_arith_rewriter.h rename to src/theory/arith/arith_rewriter.h index 1fb743f71..f7ef8c0c7 100644 --- a/src/theory/arith/next_arith_rewriter.h +++ b/src/theory/arith/arith_rewriter.h @@ -1,5 +1,5 @@ /********************* */ -/*! \file next_arith_rewriter.h +/*! \file arith_rewriter.h ** \verbatim ** Original author: taking ** Major contributors: mdeters @@ -21,14 +21,14 @@ #include "theory/theory.h" #include "theory/arith/normal_form.h" -#ifndef __CVC4__THEORY__ARITH__REWRITER_NEXT_H -#define __CVC4__THEORY__ARITH__REWRITER_NEXT_H +#ifndef __CVC4__THEORY__ARITH__REWRITER_H +#define __CVC4__THEORY__ARITH__REWRITER_H namespace CVC4 { namespace theory { namespace arith { -class NextArithRewriter{ +class ArithRewriter{ private: ArithConstants* d_constants; @@ -56,7 +56,7 @@ private: RewriteResponse postRewriteAtomConstantRHS(TNode t); public: - NextArithRewriter(ArithConstants* ac) : d_constants(ac) {} + ArithRewriter(ArithConstants* ac) : d_constants(ac) {} RewriteResponse preRewrite(TNode n); RewriteResponse postRewrite(TNode n); @@ -71,4 +71,4 @@ private: }; /* namespace theory */ }; /* namespace CVC4 */ -#endif /* __CVC4__THEORY__ARITH__REWRITER_NEXT_H */ +#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/basic.h b/src/theory/arith/arithvar_dense_set.h similarity index 50% rename from src/theory/arith/basic.h rename to src/theory/arith/arithvar_dense_set.h index c52e0881d..274246fbe 100644 --- a/src/theory/arith/basic.h +++ b/src/theory/arith/arithvar_dense_set.h @@ -1,5 +1,5 @@ /********************* */ -/*! \file basic.h +/*! \file arithvar_dense_set.h ** \verbatim ** Original author: taking ** Major contributors: mdeters @@ -17,42 +17,51 @@ ** \todo document this file **/ +#include +#include "theory/arith/arith_utilities.h" -#include "expr/node.h" -#include "expr/attribute.h" - -#ifndef __CVC4__THEORY__ARITH__BASIC_H -#define __CVC4__THEORY__ARITH__BASIC_H +#ifndef __CVC4__THEORY__ARITH__ARTIHVAR_DENSE_SET_H +#define __CVC4__THEORY__ARITH__ARTIHVAR_DENSE_SET_H namespace CVC4 { namespace theory { namespace arith { -class IsBasicManager { +class ArithVarDenseSet { private: - std::vector d_basic; + std::vector d_set; public: - IsBasicManager() : d_basic() {} + ArithVarDenseSet() : d_set() {} + + size_t size() const { + return d_set.size(); + } + + void increaseSize(ArithVar max){ + Assert(max >= size()); + d_set.resize(max+1, false); + } - void init(ArithVar var, bool value){ - Assert(var == d_basic.size()); - d_basic.push_back(value); + bool isMember(ArithVar x) const{ + return d_set[x]; } - bool isBasic(ArithVar x) const{ - return d_basic[x]; + void init(ArithVar x, bool val) { + Assert(x >= size()); + increaseSize(x); + d_set[x] = val; } - void makeBasic(ArithVar x){ - Assert(!isBasic(x)); - d_basic[x] = true; + void add(ArithVar x){ + Assert(!isMember(x)); + d_set[x] = true; } - void makeNonbasic(ArithVar x){ - Assert(isBasic(x)); - d_basic[x] = false; + void remove(ArithVar x){ + Assert(isMember(x)); + d_set[x] = false; } }; @@ -60,4 +69,4 @@ public: }; /* namespace theory */ }; /* namespace CVC4 */ -#endif /* __CVC4__THEORY__ARITH__BASIC_H */ +#endif /* __CVC4__THEORY__ARITH__ARTIHVAR_DENSE_SET_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); } /** -- 2.30.2