summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/smt/smt_engine.cpp30
-rw-r--r--src/theory/theory_engine.cpp6
-rw-r--r--src/theory/theory_engine.h6
-rw-r--r--src/util/options.cpp7
-rw-r--r--src/util/options.h4
5 files changed, 39 insertions, 14 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 296abe0e1..151f7237b 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -253,23 +253,13 @@ SExpr SmtEngine::getInfo(const std::string& key) const
void SmtEngine::setOption(const std::string& key, const SExpr& value)
throw(BadOptionException, ModalException) {
Debug("smt") << "SMT setOption(" << key << ", " << value << ")" << endl;
- if(d_logic != "") {
- throw ModalException("logic already set; cannot set options");
- }
+
if(key == ":print-success") {
throw BadOptionException();
} else if(key == ":expand-definitions") {
throw BadOptionException();
} else if(key == ":interactive-mode") {
throw BadOptionException();
- } else if(key == ":produce-proofs") {
- throw BadOptionException();
- } else if(key == ":produce-unsat-cores") {
- throw BadOptionException();
- } else if(key == ":produce-models") {
- throw BadOptionException();
- } else if(key == ":produce-assignments") {
- throw BadOptionException();
} else if(key == ":regular-output-channel") {
throw BadOptionException();
} else if(key == ":diagnostic-output-channel") {
@@ -279,7 +269,23 @@ void SmtEngine::setOption(const std::string& key, const SExpr& value)
} else if(key == ":verbosity") {
throw BadOptionException();
} else {
- throw BadOptionException();
+ // The following options can only be set at the beginning; we throw
+ // a ModalException if someone tries.
+ if(d_logic != "") {
+ throw ModalException("logic already set; cannot set options");
+ }
+
+ if(key == ":produce-proofs") {
+ throw BadOptionException();
+ } else if(key == ":produce-unsat-cores") {
+ throw BadOptionException();
+ } else if(key == ":produce-models") {
+ throw BadOptionException();
+ } else if(key == ":produce-assignments") {
+ throw BadOptionException();
+ } else {
+ throw BadOptionException();
+ }
}
}
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 40debc7c7..eb4c18161 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -65,7 +65,8 @@ void TheoryEngine::EngineOutputChannel::newFact(TNode fact) {
// Automatically track all asserted equalities in the shared term manager
d_engine->getSharedTermManager()->addEq(fact);
}
- if(! fact.getAttribute(RegisteredAttr())) {
+
+ if(d_engine->d_theoryRegistration && !fact.getAttribute(RegisteredAttr())) {
list<TNode> toReg;
toReg.push_back(fact);
@@ -123,12 +124,13 @@ void TheoryEngine::EngineOutputChannel::newFact(TNode fact) {
d_engine->theoryOf(n)->registerTerm(n);
}
}
- }
+ }/* d_engine->d_theoryRegistration && !fact.getAttribute(RegisteredAttr()) */
}
TheoryEngine::TheoryEngine(context::Context* ctxt, const Options& opts) :
d_propEngine(NULL),
d_theoryOut(this, ctxt),
+ d_theoryRegistration(opts.theoryRegistration),
d_hasShutDown(false),
d_incomplete(ctxt, false),
d_statistics() {
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 7e08a29d5..b2f047824 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -136,6 +136,12 @@ class TheoryEngine {
theory::Theory* d_bv;
/**
+ * Whether or not theory registration is on. May not be safe to
+ * turn off with some theories.
+ */
+ bool d_theoryRegistration;
+
+ /**
* Debugging flag to ensure that shutdown() is called before the
* destructor.
*/
diff --git a/src/util/options.cpp b/src/util/options.cpp
index 6d3a06b4b..dbfed887d 100644
--- a/src/util/options.cpp
+++ b/src/util/options.cpp
@@ -52,6 +52,7 @@ static const string optionsDescription = "\
--eager-type-checking type check expressions immediately on creation\n\
--no-type-checking never type check expressions\n\
--no-checking disable ALL semantic checks, including type checks \n\
+ --no-theory-registration disable theory reg (not safe for some theories)\n\
--strict-parsing fail on non-conformant inputs (SMT2 only)\n\
--verbose | -v increase verbosity (repeatable)\n\
--quiet | -q decrease verbosity (repeatable)\n\
@@ -103,6 +104,7 @@ enum OptionValue {
SEGV_NOSPIN,
PARSE_ONLY,
NO_CHECKING,
+ NO_THEORY_REGISTRATION,
USE_MMAP,
SHOW_CONFIG,
STRICT_PARSING,
@@ -151,6 +153,7 @@ static struct option cmdlineOptions[] = {
{ "trace" , required_argument, NULL, 't' },
{ "stats" , no_argument , NULL, STATS },
{ "no-checking", no_argument , NULL, NO_CHECKING },
+ { "no-theory-registration", no_argument, NULL, NO_THEORY_REGISTRATION },
{ "show-config", no_argument , NULL, SHOW_CONFIG },
{ "segv-nospin", no_argument , NULL, SEGV_NOSPIN },
{ "help" , no_argument , NULL, 'h' },
@@ -268,6 +271,10 @@ throw(OptionException) {
parseOnly = true;
break;
+ case NO_THEORY_REGISTRATION:
+ theoryRegistration = false;
+ break;
+
case NO_CHECKING:
semanticChecks = false;
typeChecking = false;
diff --git a/src/util/options.h b/src/util/options.h
index 8cf0b8446..60c8f2a1a 100644
--- a/src/util/options.h
+++ b/src/util/options.h
@@ -90,6 +90,9 @@ struct CVC4_PUBLIC Options {
/** Should the parser do semantic checks? */
bool semanticChecks;
+ /** Should the TheoryEngine do theory registration? */
+ bool theoryRegistration;
+
/** Should the parser memory-map file input? */
bool memoryMap;
@@ -134,6 +137,7 @@ struct CVC4_PUBLIC Options {
uf_implementation(MORGAN),
parseOnly(false),
semanticChecks(DO_SEMANTIC_CHECKS_BY_DEFAULT),
+ theoryRegistration(true),
memoryMap(false),
strictParsing(false),
lazyDefinitionExpansion(false),
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback