From 1f07775e9205b3f9e172a1ad218a9015b7265b58 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Mon, 8 Nov 2010 23:37:36 +0000 Subject: [PATCH] command-line flag to disable theory registration, also SMT-LIBv2 compliance (per SMT-LIB mailing list this afternoon) --- src/smt/smt_engine.cpp | 30 ++++++++++++++++++------------ src/theory/theory_engine.cpp | 6 ++++-- src/theory/theory_engine.h | 6 ++++++ src/util/options.cpp | 7 +++++++ src/util/options.h | 4 ++++ 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 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 @@ -135,6 +135,12 @@ class TheoryEngine { theory::Theory* d_arrays; 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), -- 2.30.2