summaryrefslogtreecommitdiff
path: root/src/theory
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory')
-rw-r--r--src/theory/bv/bitblaster_template.h19
-rw-r--r--src/theory/bv/lazy_bitblaster.cpp10
-rw-r--r--src/theory/bv/theory_bv.cpp5
-rw-r--r--src/theory/bv/theory_bv.h2
-rw-r--r--src/theory/bv/theory_bv_rewrite_rules_normalization.h20
-rw-r--r--src/theory/bv/theory_bv_rewrite_rules_simplification.h23
-rw-r--r--src/theory/bv/theory_bv_utils.h9
-rw-r--r--src/theory/logic_info.cpp7
-rw-r--r--src/theory/logic_info.h6
-rw-r--r--src/theory/rewriter_attributes.h12
-rw-r--r--src/theory/theory.cpp46
-rw-r--r--src/theory/theory.h20
-rw-r--r--src/theory/theory_engine.cpp10
-rw-r--r--src/theory/theory_engine.h7
-rw-r--r--src/theory/theory_model.cpp3
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;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback