diff options
| author | Clark Barrett <barrett@cs.nyu.edu> | 2013-04-01 22:27:17 -0400 |
|---|---|---|
| committer | Clark Barrett <barrett@cs.nyu.edu> | 2013-04-01 22:27:17 -0400 |
| commit | a5d0a2bf74fd0af30914b63798c4832e65d44964 (patch) | |
| tree | 05ecb0bcea0d7c4afbb58c4c54b5fab36a735a61 /src/theory/arrays/theory_arrays.cpp | |
| parent | 1898e8aa441a83f83a7603a7e157284accbd019b (diff) | |
Made eager lemmas an option, enabled for QF_AX
Diffstat (limited to 'src/theory/arrays/theory_arrays.cpp')
| -rw-r--r-- | src/theory/arrays/theory_arrays.cpp | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index 02f4152e9..9c28b3a42 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -40,7 +40,7 @@ namespace arrays { // Use static configuration of options for now const bool d_ccStore = false; const bool d_useArrTable = false; -const bool d_eagerLemmas = false; + //const bool d_eagerLemmas = false; const bool d_propagateLemmas = true; const bool d_preprocess = true; const bool d_solveWrite = true; @@ -964,7 +964,7 @@ void TheoryArrays::check(Effort e) { checkModel(e); } - if(!d_eagerLemmas && fullEffort(e) && !d_conflict && !options::arraysModelBased()) { + 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(); @@ -2281,7 +2281,7 @@ void TheoryArrays::queueRowLemma(RowLemmaType lem) // TODO: maybe add triggers here - if (d_eagerLemmas || bothExist) { + if (options::arraysEagerLemmas() || bothExist) { // Make sure that any terms introduced by rewriting are appropriately stored in the equality database Node aj2 = Rewriter::rewrite(aj); |