diff options
| author | Clark Barrett <barrett@cs.nyu.edu> | 2013-04-01 22:38:52 -0400 |
|---|---|---|
| committer | Clark Barrett <barrett@cs.nyu.edu> | 2013-04-01 22:38:52 -0400 |
| commit | 1f1f24f3c8618cb601b2ef95991792c7e3232a71 (patch) | |
| tree | 2de5a2e54218bc13af22d48b10b66c7e776e94e9 /src | |
| parent | a5d0a2bf74fd0af30914b63798c4832e65d44964 (diff) | |
Turning on model based array solver for QF_AX
Diffstat (limited to 'src')
| -rw-r--r-- | src/smt/smt_engine.cpp | 15 |
1 files changed, 7 insertions, 8 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 10a74ea5b..7bbc12551 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -864,24 +864,23 @@ void SmtEngine::setLogicInternal() throw() { Trace("smt") << "setting ite simplification to " << iteSimp << endl; options::doITESimp.set(iteSimp); } - // Turn off array eager index splitting for QF_AUFLIA and QF_AX + // Turn off array eager index splitting for QF_AUFLIA if(! options::arraysEagerIndexSplitting.wasSetByUser()) { if (not d_logic.isQuantified() && d_logic.isTheoryEnabled(THEORY_ARRAY) && - (d_logic.isPure(THEORY_ARRAY) || - (d_logic.isTheoryEnabled(THEORY_UF) && - d_logic.isTheoryEnabled(THEORY_ARITH)))) { + d_logic.isTheoryEnabled(THEORY_UF) && + d_logic.isTheoryEnabled(THEORY_ARITH)) { Trace("smt") << "setting array eager index splitting to false" << endl; options::arraysEagerIndexSplitting.set(false); } } - // Turn on array eager lemmas for QF_AX - if(! options::arraysEagerLemmas.wasSetByUser()) { + // Turn on model-based arrays for QF_AX + if(! options::arraysModelBased.wasSetByUser()) { if (not d_logic.isQuantified() && d_logic.isTheoryEnabled(THEORY_ARRAY) && d_logic.isPure(THEORY_ARRAY)) { - Trace("smt") << "setting array eager lemmas to true" << endl; - options::arraysEagerIndexSplitting.set(true); + Trace("smt") << "turning on model-based array solver" << endl; + options::arraysModelBased.set(true); } } // Turn on multiple-pass non-clausal simplification for QF_AUFBV |