diff options
Diffstat (limited to 'src/smt/smt_engine.cpp')
-rw-r--r-- | src/smt/smt_engine.cpp | 55 |
1 files changed, 34 insertions, 21 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 6e90ab152..74d6c1b10 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -298,7 +298,8 @@ struct SmtEngineStatistics { class SoftResourceOutListener : public Listener { public: SoftResourceOutListener(SmtEngine& smt) : d_smt(&smt) {} - virtual void notify() { + void notify() override + { SmtScope scope(d_smt); Assert(smt::smtEngineInScope()); d_smt->interrupt(); @@ -311,7 +312,8 @@ class SoftResourceOutListener : public Listener { class HardResourceOutListener : public Listener { public: HardResourceOutListener(SmtEngine& smt) : d_smt(&smt) {} - virtual void notify() { + void notify() override + { SmtScope scope(d_smt); theory::Rewriter::clearCaches(); } @@ -322,7 +324,8 @@ class HardResourceOutListener : public Listener { class SetLogicListener : public Listener { public: SetLogicListener(SmtEngine& smt) : d_smt(&smt) {} - virtual void notify() { + void notify() override + { LogicInfo inOptions(options::forceLogicString()); d_smt->setLogic(inOptions); } @@ -333,9 +336,8 @@ class SetLogicListener : public Listener { class BeforeSearchListener : public Listener { public: BeforeSearchListener(SmtEngine& smt) : d_smt(&smt) {} - virtual void notify() { - d_smt->beforeSearch(); - } + void notify() override { d_smt->beforeSearch(); } + private: SmtEngine* d_smt; }; /* class BeforeSearchListener */ @@ -346,7 +348,8 @@ class UseTheoryListListener : public Listener { : d_theoryEngine(theoryEngine) {} - void notify() { + void notify() override + { std::stringstream commaList(options::useTheoryList()); std::string token; @@ -375,7 +378,8 @@ class UseTheoryListListener : public Listener { class SetDefaultExprDepthListener : public Listener { public: - virtual void notify() { + void notify() override + { int depth = options::defaultExprDepth(); Debug.getStream() << expr::ExprSetDepth(depth); Trace.getStream() << expr::ExprSetDepth(depth); @@ -389,7 +393,8 @@ class SetDefaultExprDepthListener : public Listener { class SetDefaultExprDagListener : public Listener { public: - virtual void notify() { + void notify() override + { int dag = options::defaultDagThresh(); Debug.getStream() << expr::ExprDag(dag); Trace.getStream() << expr::ExprDag(dag); @@ -403,7 +408,8 @@ class SetDefaultExprDagListener : public Listener { class SetPrintExprTypesListener : public Listener { public: - virtual void notify() { + void notify() override + { bool value = options::printExprTypes(); Debug.getStream() << expr::ExprPrintTypes(value); Trace.getStream() << expr::ExprPrintTypes(value); @@ -417,7 +423,8 @@ class SetPrintExprTypesListener : public Listener { class DumpModeListener : public Listener { public: - virtual void notify() { + void notify() override + { const std::string& value = options::dumpModeString(); Dump.setDumpFromString(value); } @@ -425,7 +432,8 @@ class DumpModeListener : public Listener { class PrintSuccessListener : public Listener { public: - virtual void notify() { + void notify() override + { bool value = options::printSuccess(); Debug.getStream() << Command::printsuccess(value); Trace.getStream() << Command::printsuccess(value); @@ -748,7 +756,8 @@ public: d_resourceManager->spendResource(amount); } - void nmNotifyNewSort(TypeNode tn, uint32_t flags) { + void nmNotifyNewSort(TypeNode tn, uint32_t flags) override + { DeclareTypeCommand c(tn.getAttribute(expr::VarNameAttr()), 0, tn.toType()); @@ -757,19 +766,22 @@ public: } } - void nmNotifyNewSortConstructor(TypeNode tn) { + void nmNotifyNewSortConstructor(TypeNode tn) override + { DeclareTypeCommand c(tn.getAttribute(expr::VarNameAttr()), tn.getAttribute(expr::SortArityAttr()), tn.toType()); d_smt.addToModelCommandAndDump(c); } - void nmNotifyNewDatatypes(const std::vector<DatatypeType>& dtts) { + void nmNotifyNewDatatypes(const std::vector<DatatypeType>& dtts) override + { DatatypeDeclarationCommand c(dtts); d_smt.addToModelCommandAndDump(c); } - void nmNotifyNewVar(TNode n, uint32_t flags) { + void nmNotifyNewVar(TNode n, uint32_t flags) override + { DeclareFunctionCommand c(n.getAttribute(expr::VarNameAttr()), n.toExpr(), n.getType().toType()); @@ -781,11 +793,12 @@ public: } } - void nmNotifyNewSkolem(TNode n, const std::string& comment, uint32_t flags) { + void nmNotifyNewSkolem(TNode n, + const std::string& comment, + uint32_t flags) override + { string id = n.getAttribute(expr::VarNameAttr()); - DeclareFunctionCommand c(id, - n.toExpr(), - n.getType().toType()); + DeclareFunctionCommand c(id, n.toExpr(), n.getType().toType()); if(Dump.isOn("skolems") && comment != "") { Dump("skolems") << CommentCommand(id + " is " + comment); } @@ -797,7 +810,7 @@ public: } } - void nmNotifyDeleteNode(TNode n) {} + void nmNotifyDeleteNode(TNode n) override {} Node applySubstitutions(TNode node) const { return Rewriter::rewrite(d_topLevelSubstitutions.apply(node)); |