Made eager lemmas an option, enabled for QF_AX

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 8d13b5cc6f2a9f48360b6da4fea0350e5ac4a31c..10a74ea5b97eabfdf32b395cb69f4f5d809b19d4 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -875,6 +875,15 @@ void SmtEngine::setLogicInternal() throw() {
       options::arraysEagerIndexSplitting.set(false);
     }
   }
+  // Turn on array eager lemmas for QF_AX
+  if(! options::arraysEagerLemmas.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);
+    }
+  }
   // Turn on multiple-pass non-clausal simplification for QF_AUFBV
   if(! options::repeatSimp.wasSetByUser()) {
     bool repeatSimp = !d_logic.isQuantified() &&

diff --git a/src/theory/arrays/options b/src/theory/arrays/options
index 8a971cfe8e5aac5b12363afe944702f16a51f505..15220fbc218e63184f5e2060fd1ca9c3ca7752e1 100644 (file)
--- 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 02f4152e9a9c141769876586c3f24f4a73af89a7..9c28b3a42698e5544cc1b61f05a8b233b983cedf 100644 (file)
--- 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);