diff options
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/bv/bitblaster_template.h | 19 | ||||
-rw-r--r-- | src/theory/bv/lazy_bitblaster.cpp | 10 | ||||
-rw-r--r-- | src/theory/bv/theory_bv.cpp | 5 | ||||
-rw-r--r-- | src/theory/bv/theory_bv.h | 2 | ||||
-rw-r--r-- | src/theory/bv/theory_bv_rewrite_rules_normalization.h | 20 | ||||
-rw-r--r-- | src/theory/bv/theory_bv_rewrite_rules_simplification.h | 23 | ||||
-rw-r--r-- | src/theory/bv/theory_bv_utils.h | 9 | ||||
-rw-r--r-- | src/theory/logic_info.cpp | 7 | ||||
-rw-r--r-- | src/theory/logic_info.h | 6 | ||||
-rw-r--r-- | src/theory/rewriter_attributes.h | 12 | ||||
-rw-r--r-- | src/theory/theory.cpp | 46 | ||||
-rw-r--r-- | src/theory/theory.h | 20 | ||||
-rw-r--r-- | src/theory/theory_engine.cpp | 10 | ||||
-rw-r--r-- | src/theory/theory_engine.h | 7 | ||||
-rw-r--r-- | src/theory/theory_model.cpp | 3 |
15 files changed, 104 insertions, 95 deletions
diff --git a/src/theory/bv/bitblaster_template.h b/src/theory/bv/bitblaster_template.h index 33dd4387e..1dc2d8b1e 100644 --- a/src/theory/bv/bitblaster_template.h +++ b/src/theory/bv/bitblaster_template.h @@ -137,10 +137,10 @@ class TLazyBitblaster : public TBitblaster<Node> { , d_lazyBB(lbv) {} - bool notify(prop::SatLiteral lit); - void notify(prop::SatClause& clause); - void spendResource(unsigned ammount); - void safePoint(unsigned ammount); + bool notify(prop::SatLiteral lit) override; + void notify(prop::SatClause& clause) override; + void spendResource(unsigned amount) override; + void safePoint(unsigned amount) override; }; TheoryBV *d_bv; @@ -249,12 +249,13 @@ public: class MinisatEmptyNotify : public prop::BVSatSolverInterface::Notify { public: MinisatEmptyNotify() {} - bool notify(prop::SatLiteral lit) { return true; } - void notify(prop::SatClause& clause) { } - void spendResource(unsigned ammount) { - NodeManager::currentResourceManager()->spendResource(ammount); + bool notify(prop::SatLiteral lit) override { return true; } + void notify(prop::SatClause& clause) override {} + void spendResource(unsigned amount) override + { + NodeManager::currentResourceManager()->spendResource(amount); } - void safePoint(unsigned ammount) {} + void safePoint(unsigned amount) override {} }; diff --git a/src/theory/bv/lazy_bitblaster.cpp b/src/theory/bv/lazy_bitblaster.cpp index d108a37f0..33342dc2e 100644 --- a/src/theory/bv/lazy_bitblaster.cpp +++ b/src/theory/bv/lazy_bitblaster.cpp @@ -384,12 +384,14 @@ void TLazyBitblaster::MinisatNotify::notify(prop::SatClause& clause) { } } -void TLazyBitblaster::MinisatNotify::spendResource(unsigned ammount) { - d_bv->spendResource(ammount); +void TLazyBitblaster::MinisatNotify::spendResource(unsigned amount) +{ + d_bv->spendResource(amount); } -void TLazyBitblaster::MinisatNotify::safePoint(unsigned ammount) { - d_bv->d_out->safePoint(ammount); +void TLazyBitblaster::MinisatNotify::safePoint(unsigned amount) +{ + d_bv->d_out->safePoint(amount); } diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index af1dd5331..c6f2ec74b 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -125,8 +125,9 @@ void TheoryBV::setMasterEqualityEngine(eq::EqualityEngine* eq) { } } -void TheoryBV::spendResource(unsigned ammount) throw(UnsafeInterruptException) { - getOutputChannel().spendResource(ammount); +void TheoryBV::spendResource(unsigned amount) +{ + getOutputChannel().spendResource(amount); } TheoryBV::Statistics::Statistics(const std::string &name): diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h index a425cbdc8..8cefe03b2 100644 --- a/src/theory/bv/theory_bv.h +++ b/src/theory/bv/theory_bv.h @@ -120,7 +120,7 @@ private: Statistics d_statistics; - void spendResource(unsigned ammount) throw(UnsafeInterruptException); + void spendResource(unsigned amount); /** * Return the uninterpreted function symbol corresponding to division-by-zero diff --git a/src/theory/bv/theory_bv_rewrite_rules_normalization.h b/src/theory/bv/theory_bv_rewrite_rules_normalization.h index 07688a8bb..d17f20152 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_normalization.h +++ b/src/theory/bv/theory_bv_rewrite_rules_normalization.h @@ -109,8 +109,8 @@ Node RewriteRule<ExtractSignExtend>::apply(TNode node) { } else if (low < extendee_size && high >= extendee_size) { // if extract overlaps sign extend and extendee Node low_extract = utils::mkExtract(extendee, extendee_size - 1, low); - unsigned new_ammount = high - extendee_size + 1; - resultNode = utils::mkSignExtend(low_extract, new_ammount); + unsigned new_amount = high - extendee_size + 1; + resultNode = utils::mkSignExtend(low_extract, new_amount); } else { // extract only over sign extend Assert (low >= extendee_size); @@ -529,15 +529,15 @@ bool RewriteRule<ConcatToMult>::applies(TNode node) { if (!node[1].isConst()) return false; TNode extract = node[0]; TNode c = node[1]; - unsigned ammount = utils::getSize(c); - - if (utils::getSize(node) != utils::getSize(extract[0])) return false; - if (c != utils::mkConst(ammount, 0)) return false; + unsigned amount = utils::getSize(c); + + if (utils::getSize(node) != utils::getSize(extract[0])) return false; + if (c != utils::mkZero(amount)) return false; unsigned low = utils::getExtractLow(extract); if (low != 0) return false; unsigned high = utils::getExtractHigh(extract); - if (high + ammount + 1 != utils::getSize(node)) return false; + if (high + amount + 1 != utils::getSize(node)) return false; return true; } @@ -546,9 +546,9 @@ Node RewriteRule<ConcatToMult>::apply(TNode node) { Debug("bv-rewrite") << "RewriteRule<ConcatToMult>(" << node << ")" << std::endl; unsigned size = utils::getSize(node); Node factor = node[0][0]; - Assert(utils::getSize(factor) == utils::getSize(node)); - BitVector ammount = BitVector(size, utils::getSize(node[1])); - Node coef = utils::mkConst(BitVector(size, 1u).leftShift(ammount)); + Assert(utils::getSize(factor) == utils::getSize(node)); + BitVector amount = BitVector(size, utils::getSize(node[1])); + Node coef = utils::mkConst(BitVector(size, 1u).leftShift(amount)); return utils::mkNode(kind::BITVECTOR_MULT, factor, coef); } diff --git a/src/theory/bv/theory_bv_rewrite_rules_simplification.h b/src/theory/bv/theory_bv_rewrite_rules_simplification.h index 5956ced7e..067440ee2 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_simplification.h +++ b/src/theory/bv/theory_bv_rewrite_rules_simplification.h @@ -1127,31 +1127,32 @@ bool RewriteRule<MergeSignExtend>::applies(TNode node) { template<> inline Node RewriteRule<MergeSignExtend>::apply(TNode node) { Debug("bv-rewrite") << "RewriteRule<MergeSignExtend>(" << node << ")" << std::endl; - unsigned ammount1 = node.getOperator().getConst<BitVectorSignExtend>().signExtendAmount; + unsigned amount1 = + node.getOperator().getConst<BitVectorSignExtend>().signExtendAmount; NodeManager* nm = NodeManager::currentNM(); if (node[0].getKind() == kind::BITVECTOR_ZERO_EXTEND) { - unsigned ammount2 = node[0].getOperator().getConst<BitVectorZeroExtend>().zeroExtendAmount; - if (ammount2 == 0) { + unsigned amount2 = + node[0].getOperator().getConst<BitVectorZeroExtend>().zeroExtendAmount; + if (amount2 == 0) + { NodeBuilder<> nb(kind::BITVECTOR_SIGN_EXTEND); - Node op = nm->mkConst<BitVectorSignExtend>(BitVectorSignExtend(ammount1)); + Node op = nm->mkConst<BitVectorSignExtend>(BitVectorSignExtend(amount1)); nb << op << node[0][0]; Node res = nb; return res; } NodeBuilder<> nb(kind::BITVECTOR_ZERO_EXTEND); - Node op = nm->mkConst<BitVectorZeroExtend>(BitVectorZeroExtend(ammount1 + ammount2)); + Node op = nm->mkConst<BitVectorZeroExtend>( + BitVectorZeroExtend(amount1 + amount2)); nb << op << node[0][0]; Node res = nb; return res; } Assert (node[0].getKind() == kind::BITVECTOR_SIGN_EXTEND); - unsigned ammount2 = node[0].getOperator().getConst<BitVectorSignExtend>().signExtendAmount; - NodeBuilder<> nb(kind::BITVECTOR_SIGN_EXTEND); - Node op = nm->mkConst<BitVectorSignExtend>(BitVectorSignExtend(ammount1+ ammount2)); - nb << op << node[0][0]; - Node res = nb; - return res; + unsigned amount2 = + node[0].getOperator().getConst<BitVectorSignExtend>().signExtendAmount; + return utils::mkSignExtend(node[0][0], amount1 + amount2); } /** diff --git a/src/theory/bv/theory_bv_utils.h b/src/theory/bv/theory_bv_utils.h index ecd93cd2c..e304e4801 100644 --- a/src/theory/bv/theory_bv_utils.h +++ b/src/theory/bv/theory_bv_utils.h @@ -144,10 +144,11 @@ inline Node mkXor(TNode node1, TNode node2) { return NodeManager::currentNM()->mkNode(kind::XOR, node1, node2); } - -inline Node mkSignExtend(TNode node, unsigned ammount) { - NodeManager* nm = NodeManager::currentNM(); - Node signExtendOp = nm->mkConst<BitVectorSignExtend>(BitVectorSignExtend(ammount)); +inline Node mkSignExtend(TNode node, unsigned amount) +{ + NodeManager* nm = NodeManager::currentNM(); + Node signExtendOp = + nm->mkConst<BitVectorSignExtend>(BitVectorSignExtend(amount)); return nm->mkNode(signExtendOp, node); } diff --git a/src/theory/logic_info.cpp b/src/theory/logic_info.cpp index bf1a9bf65..a458eec30 100644 --- a/src/theory/logic_info.cpp +++ b/src/theory/logic_info.cpp @@ -47,7 +47,7 @@ LogicInfo::LogicInfo() } } -LogicInfo::LogicInfo(std::string logicString) throw(IllegalArgumentException) +LogicInfo::LogicInfo(std::string logicString) : d_logicString(""), d_theories(THEORY_LAST, false), d_sharingTheories(0), @@ -63,7 +63,7 @@ LogicInfo::LogicInfo(std::string logicString) throw(IllegalArgumentException) lock(); } -LogicInfo::LogicInfo(const char* logicString) throw(IllegalArgumentException) +LogicInfo::LogicInfo(const char* logicString) : d_logicString(""), d_theories(THEORY_LAST, false), d_sharingTheories(0), @@ -327,7 +327,8 @@ std::string LogicInfo::getLogicString() const { return d_logicString; } -void LogicInfo::setLogicString(std::string logicString) throw(IllegalArgumentException) { +void LogicInfo::setLogicString(std::string logicString) +{ PrettyCheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified"); for(TheoryId id = THEORY_FIRST; id < THEORY_LAST; ++id) { diff --git a/src/theory/logic_info.h b/src/theory/logic_info.h index dc88cc9f4..cbb04604e 100644 --- a/src/theory/logic_info.h +++ b/src/theory/logic_info.h @@ -90,14 +90,14 @@ public: * Throws an IllegalArgumentException if the logic string cannot * be interpreted. */ - LogicInfo(std::string logicString) throw(IllegalArgumentException); + LogicInfo(std::string logicString); /** * Construct a LogicInfo from an SMT-LIB-like logic string. * Throws an IllegalArgumentException if the logic string cannot * be interpreted. */ - LogicInfo(const char* logicString) throw(IllegalArgumentException); + LogicInfo(const char* logicString); // ACCESSORS @@ -157,7 +157,7 @@ public: * Throws an IllegalArgumentException if the string can't be * interpreted. */ - void setLogicString(std::string logicString) throw(IllegalArgumentException); + void setLogicString(std::string logicString); /** * Enable all functionality. All theories, plus quantifiers, will be diff --git a/src/theory/rewriter_attributes.h b/src/theory/rewriter_attributes.h index ec120ff0c..60fa3a417 100644 --- a/src/theory/rewriter_attributes.h +++ b/src/theory/rewriter_attributes.h @@ -35,7 +35,8 @@ struct RewriteAttibute { /** * Get the value of the pre-rewrite cache. */ - static Node getPreRewriteCache(TNode node) throw() { + static Node getPreRewriteCache(TNode node) + { Node cache; if (node.hasAttribute(pre_rewrite())) { node.getAttribute(pre_rewrite(), cache); @@ -52,7 +53,8 @@ struct RewriteAttibute { /** * Set the value of the pre-rewrite cache. */ - static void setPreRewriteCache(TNode node, TNode cache) throw() { + static void setPreRewriteCache(TNode node, TNode cache) + { Trace("rewriter") << "setting pre-rewrite of " << node << " to " << cache << std::endl; Assert(!cache.isNull()); if (node == cache) { @@ -66,7 +68,8 @@ struct RewriteAttibute { * Get the value of the post-rewrite cache. * none). */ - static Node getPostRewriteCache(TNode node) throw() { + static Node getPostRewriteCache(TNode node) + { Node cache; if (node.hasAttribute(post_rewrite())) { node.getAttribute(post_rewrite(), cache); @@ -83,7 +86,8 @@ struct RewriteAttibute { /** * Set the value of the post-rewrite cache. v cannot be a null Node. */ - static void setPostRewriteCache(TNode node, TNode cache) throw() { + static void setPostRewriteCache(TNode node, TNode cache) + { Assert(!cache.isNull()); Trace("rewriter") << "setting rewrite of " << node << " to " << cache << std::endl; if (node == cache) { diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp index 8509e84ab..069767968 100644 --- a/src/theory/theory.cpp +++ b/src/theory/theory.cpp @@ -51,28 +51,30 @@ std::ostream& operator<<(std::ostream& os, Theory::Effort level){ return os; }/* ostream& operator<<(ostream&, Theory::Effort) */ - -Theory::Theory(TheoryId id, context::Context* satContext, - context::UserContext* userContext, OutputChannel& out, - Valuation valuation, const LogicInfo& logicInfo, - std::string name) throw() - : d_id(id) - , d_instanceName(name) - , d_satContext(satContext) - , d_userContext(userContext) - , d_logicInfo(logicInfo) - , d_facts(satContext) - , d_factsHead(satContext, 0) - , d_sharedTermsIndex(satContext, 0) - , d_careGraph(NULL) - , d_quantEngine(NULL) - , d_extTheory(NULL) - , d_checkTime(getFullInstanceName() + "::checkTime") - , d_computeCareGraphTime(getFullInstanceName() + "::computeCareGraphTime") - , d_sharedTerms(satContext) - , d_out(&out) - , d_valuation(valuation) - , d_proofsEnabled(false) +Theory::Theory(TheoryId id, + context::Context* satContext, + context::UserContext* userContext, + OutputChannel& out, + Valuation valuation, + const LogicInfo& logicInfo, + std::string name) + : d_id(id), + d_instanceName(name), + d_satContext(satContext), + d_userContext(userContext), + d_logicInfo(logicInfo), + d_facts(satContext), + d_factsHead(satContext, 0), + d_sharedTermsIndex(satContext, 0), + d_careGraph(NULL), + d_quantEngine(NULL), + d_extTheory(NULL), + d_checkTime(getFullInstanceName() + "::checkTime"), + d_computeCareGraphTime(getFullInstanceName() + "::computeCareGraphTime"), + d_sharedTerms(satContext), + d_out(&out), + d_valuation(valuation), + d_proofsEnabled(false) { smtStatisticsRegistry()->registerStat(&d_checkTime); smtStatisticsRegistry()->registerStat(&d_computeCareGraphTime); diff --git a/src/theory/theory.h b/src/theory/theory.h index 204c514a9..0571a67b7 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -177,10 +177,13 @@ private: * The pair <id, instance> is assumed to uniquely identify this Theory * w.r.t. the SmtEngine. */ - Theory(TheoryId id, context::Context* satContext, - context::UserContext* userContext, OutputChannel& out, - Valuation valuation, const LogicInfo& logicInfo, - std::string instance = "") throw(); // taking : No default. + Theory(TheoryId id, + context::Context* satContext, + context::UserContext* userContext, + OutputChannel& out, + Valuation valuation, + const LogicInfo& logicInfo, + std::string instance = ""); // taking : No default. /** * This is called at shutdown time by the TheoryEngine, just before @@ -289,13 +292,8 @@ public: return node.getNumChildren() == 0 || theoryOf(node) != theoryId; } - /** - * Returns true if the assertFact queue is empty - */ - bool done() const throw() { - return d_factsHead == d_facts.size(); - } - + /** Returns true if the assertFact queue is empty*/ + bool done() const { return d_factsHead == d_facts.size(); } /** * Destructs a Theory. */ diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 4e2062c43..435dadce7 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -370,10 +370,7 @@ TheoryEngine::~TheoryEngine() { smtStatisticsRegistry()->unregisterStat(&d_arithSubstitutionsAdded); } -void TheoryEngine::interrupt() throw(ModalException) { - d_interrupted = true; -} - +void TheoryEngine::interrupt() { d_interrupted = true; } void TheoryEngine::preRegister(TNode preprocessed) { Debug("theory") << "TheoryEngine::preRegister( " << preprocessed << ")" << std::endl; @@ -2320,8 +2317,9 @@ std::pair<bool, Node> TheoryEngine::entailmentCheck(theory::TheoryOfMode mode, T } } -void TheoryEngine::spendResource(unsigned ammount) { - d_resourceManager->spendResource(ammount); +void TheoryEngine::spendResource(unsigned amount) +{ + d_resourceManager->spendResource(amount); } void TheoryEngine::enableTheoryAlternative(const std::string& name){ diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index f380e86aa..22e269409 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -461,10 +461,9 @@ public: /** Destroys a theory engine */ ~TheoryEngine(); - void interrupt() throw(ModalException); - /** - * "Spend" a resource during a search or preprocessing. - */ + void interrupt(); + + /** "Spend" a resource during a search or preprocessing.*/ void spendResource(unsigned amount); /** diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp index 5555e29e2..739925f4f 100644 --- a/src/theory/theory_model.cpp +++ b/src/theory/theory_model.cpp @@ -50,7 +50,8 @@ TheoryModel::TheoryModel(context::Context* c, d_eeContext->push(); } -TheoryModel::~TheoryModel() throw() { +TheoryModel::~TheoryModel() +{ d_eeContext->pop(); delete d_equalityEngine; delete d_eeContext; |