diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-08-16 12:44:11 +0200 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-08-16 12:44:11 +0200 |
commit | 7c798a5a2085754b26a0720d162b2ee45a705c4e (patch) | |
tree | 1d9d8614b69389b11eb0737989f4db2299e59269 /src/smt | |
parent | a582fa3ea1de3b6419797bbebdcb415ff4d0c0d0 (diff) |
More optimizations to --macros-quant, add --macros-quant-mode=ground-uf. Cleanup varContains caches in term db. Fix bug related to macros in non-tracing builds.
Diffstat (limited to 'src/smt')
-rw-r--r-- | src/smt/smt_engine.cpp | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 87cd815e9..192485dcc 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1427,6 +1427,10 @@ void SmtEngine::setDefaults() { if( !options::rewriteDivk.wasSetByUser()) { options::rewriteDivk.set( true ); } + //do not do macros + if( !options::macrosQuant.wasSetByUser()) { + options::macrosQuant.set( false ); + } } //cbqi options @@ -3309,7 +3313,7 @@ void SmtEnginePrivate::processAssertions() { dumpAssertions("post-skolem-quant", d_assertions); if( options::macrosQuant() ){ //quantifiers macro expansion - quantifiers::QuantifierMacros qm; + quantifiers::QuantifierMacros qm( d_smt.d_theoryEngine->getQuantifiersEngine() ); bool success; do{ success = qm.simplify( d_assertions.ref(), true ); |