diff options
| author | Clark Barrett <barrett@cs.nyu.edu> | 2014-09-17 15:01:19 -0700 |
|---|---|---|
| committer | Clark Barrett <barrett@cs.nyu.edu> | 2014-10-02 13:28:22 -0700 |
| commit | 4c32421fee453d82e6c1d7d3dc1605da11db1a09 (patch) | |
| tree | b0e4689aac85a856db5e75513610d53475fc4f7d /src/theory | |
| parent | 3df8013300486129fc06f3a20d43def1f34a221a (diff) | |
More model-based combination for arrays
Diffstat (limited to 'src/theory')
| -rw-r--r-- | src/theory/arrays/options | 2 | ||||
| -rw-r--r-- | src/theory/arrays/theory_arrays.cpp | 4 | ||||
| -rw-r--r-- | src/theory/theory_engine.cpp | 4 |
3 files changed, 6 insertions, 4 deletions
diff --git a/src/theory/arrays/options b/src/theory/arrays/options index 15220fbc2..baf0962bf 100644 --- a/src/theory/arrays/options +++ b/src/theory/arrays/options @@ -12,7 +12,7 @@ option arraysLazyRIntro1 --arrays-lazy-rintro1 bool :default true :read-write turn on optimization to only perform RIntro1 rule lazily (see Jovanovic/Barrett 2012: Being Careful with Theory Combination) option arraysModelBased --arrays-model-based bool :default false :read-write - turn on model-based arrray solver + turn on model-based array solver option arraysEagerIndexSplitting --arrays-eager-index bool :default true :read-write turn on eager index splitting for generated array lemmas diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index 6b91400e8..bfbf046c3 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -990,7 +990,9 @@ void TheoryArrays::check(Effort e) { if(!options::arraysEagerLemmas() && fullEffort(e) && !d_conflict && !options::arraysModelBased()) { // generate the lemmas on the worklist Trace("arrays-lem")<<"Arrays::discharging lemmas: "<<d_RowQueue.size()<<"\n"; - dischargeLemmas(); + while (d_RowQueue.size() > 0 && !d_conflict) { + dischargeLemmas(); + } } Trace("arrays") << spaces(getSatContext()->getLevel()) << "Arrays::check(): done" << endl; diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index ffe4258cd..b943a7ee5 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -501,8 +501,8 @@ void TheoryEngine::combineTheories() { // We need to split on it Debug("combineTheories") << "TheoryEngine::combineTheories(): requesting a split " << endl; lemma(equality.orNode(equality.notNode()), false, false, false, carePair.theory); - if (false) { - if (es == EQUALITY_TRUE_IN_MODEL) { + if (true) { + if (es == EQUALITY_TRUE || es == EQUALITY_TRUE_IN_MODEL) { Node e = ensureLiteral(equality); d_propEngine->requirePhase(e, true); } |