From a5d0a2bf74fd0af30914b63798c4832e65d44964 Mon Sep 17 00:00:00 2001
From: Clark Barrett <barrett@cs.nyu.edu>
Date: Mon, 1 Apr 2013 22:27:17 -0400
Subject: Made eager lemmas an option, enabled for QF_AX

---
 src/theory/arrays/options           | 3 +++
 src/theory/arrays/theory_arrays.cpp | 6 +++---
 2 files changed, 6 insertions(+), 3 deletions(-)

(limited to 'src/theory/arrays')

diff --git a/src/theory/arrays/options b/src/theory/arrays/options
index 8a971cfe8..15220fbc2 100644
--- a/src/theory/arrays/options
+++ b/src/theory/arrays/options
@@ -17,4 +17,7 @@ option arraysModelBased --arrays-model-based bool :default false :read-write
 option arraysEagerIndexSplitting --arrays-eager-index bool :default true :read-write
  turn on eager index splitting for generated array lemmas
 
+option arraysEagerLemmas --arrays-eager-lemmas bool :default false :read-write
+ turn on eager lemma generation for arrays
+
 endmodule
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);
-- 
cgit v1.2.3