diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-09-18 15:03:12 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-09-18 15:03:12 -0500 |
commit | a9c40f60e4b36494e10520dcc3a3985b4700342f (patch) | |
tree | 70dc9c73b5ce2007850ab40e623a55d205ba62e4 /src | |
parent | 40b83fd9205a7eb772a2ac413f8a3641db1fb02c (diff) |
Decouple fmf-bound and finite-model-find (#3297)
Diffstat (limited to 'src')
-rw-r--r-- | src/smt/smt_engine.cpp | 50 | ||||
-rw-r--r-- | src/theory/quantifiers_engine.cpp | 12 |
2 files changed, 28 insertions, 34 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 6d80207a6..fa318aaf1 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1215,43 +1215,39 @@ void SmtEngine::setDefaults() { d_logic = LogicInfo("QF_BV"); } - // set strings-exp - /* - disabled for 1.4 release [MGD 2014.06.25] - if(!d_logic.hasEverything() && d_logic.isTheoryEnabled(THEORY_STRINGS) ) { - if(! options::stringExp.wasSetByUser()) { - options::stringExp.set( true ); - Trace("smt") << "turning on strings-exp, for the theory of strings" << std::endl; - } - } - */ - // for strings - if(options::stringExp()) { - if( !d_logic.isQuantified() ) { + // set default options associated with strings-exp + if (options::stringExp()) + { + // We require quantifiers since extended functions reduce using them + if (!d_logic.isQuantified()) + { d_logic = d_logic.getUnlockedCopy(); d_logic.enableQuantifiers(); d_logic.lock(); Trace("smt") << "turning on quantifier logic, for strings-exp" << std::endl; } - if(! options::fmfBound.wasSetByUser()) { + // We require bounded quantifier handling. + if (!options::fmfBound.wasSetByUser()) + { options::fmfBound.set( true ); Trace("smt") << "turning on fmf-bound-int, for strings-exp" << std::endl; } - if(! options::fmfInstEngine.wasSetByUser()) { - options::fmfInstEngine.set( true ); - Trace("smt") << "turning on fmf-inst-engine, for strings-exp" << std::endl; + // Turn off E-matching, since some bounded quantifiers introduced by strings + // (e.g. for replaceall) admit matching loops. + if (!options::eMatching.wasSetByUser()) + { + options::eMatching.set(false); + Trace("smt") << "turning off E-matching, for strings-exp" << std::endl; } - /* - if(! options::rewriteDivk.wasSetByUser()) { - options::rewriteDivk.set( true ); - Trace("smt") << "turning on rewrite-divk, for strings-exp" << std::endl; - }*/ - /* - if(! options::stringFMF.wasSetByUser()) { - options::stringFMF.set( true ); - Trace("smt") << "turning on strings-fmf, for strings-exp" << std::endl; + // Do not eliminate extended arithmetic symbols from quantified formulas, + // since some strategies, e.g. --re-elim-agg, introduce them. + if (!options::elimExtArithQuant.wasSetByUser()) + { + options::elimExtArithQuant.set(false); + Trace("smt") << "turning off elim-ext-arith-quant, for strings-exp" + << std::endl; } - */ } // sygus inference may require datatypes @@ -1808,8 +1804,6 @@ void SmtEngine::setDefaults() { //now have determined whether fmfBoundInt is on/off //apply fmfBoundInt options if( options::fmfBound() ){ - //must have finite model finding on - options::finiteModelFind.set( true ); if (!options::mbqiMode.wasSetByUser() || (options::mbqiMode() != quantifiers::MBQI_NONE && options::mbqiMode() != quantifiers::MBQI_FMC)) diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 1eb62945b..e399af71d 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -138,13 +138,13 @@ class QuantifiersEnginePrivate modules.push_back(d_synth_e.get()); } // finite model finding - if (options::finiteModelFind()) + if (options::fmfBound()) + { + d_bint.reset(new quantifiers::BoundedIntegers(c, qe)); + modules.push_back(d_bint.get()); + } + if (options::finiteModelFind() || options::fmfBound()) { - if (options::fmfBound()) - { - d_bint.reset(new quantifiers::BoundedIntegers(c, qe)); - modules.push_back(d_bint.get()); - } d_model_engine.reset(new quantifiers::ModelEngine(c, qe)); modules.push_back(d_model_engine.get()); // finite model finder has special ways of building the model |