Disable some array optimizations when models are on

diff --git a/src/theory/arrays/options b/src/theory/arrays/options
index bf8afc589062c4f6fe48cf178d1ca24ac8eb60fc..755cf239c2574252180dffc77fa34390db5efd0d 100644 (file)
--- a/src/theory/arrays/options
+++ b/src/theory/arrays/options
@@ -5,4 +5,10 @@
 
 module ARRAYS "theory/arrays/options.h" Arrays theory
 
+option arraysOptimizeLinear --arrays-optimize-linear bool :default true :read-write
+ turn on optimization for linear array terms (see de Moura FMCAD 09 arrays paper)
+
+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)
+
 endmodule

diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index 7aa6d8597833b6a5532f67b59bfa6a46a9195373..c0777f79fe368861dd27b7e1fb3b51c5ddb654a1 100644 (file)
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -24,6 +24,8 @@
 #include "theory/arrays/theory_arrays_instantiator.h"
 #include "theory/arrays/theory_arrays_model.h"
 #include "theory/model.h"
+#include "theory/arrays/options.h"
+
 
 using namespace std;
 
@@ -43,7 +45,9 @@ const bool d_propagateLemmas = true;
 const bool d_preprocess = true;
 const bool d_solveWrite = true;
 const bool d_solveWrite2 = false;
-const bool d_useNonLinearOpt = true;
+  // These are now options
+  //bool d_useNonLinearOpt = true;
+  //bool d_lazyRIntro1 = true;
 const bool d_eagerIndexSplitting = true;
 
 TheoryArrays::TheoryArrays(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, QuantifiersEngine* qe) :
@@ -382,21 +386,23 @@ void TheoryArrays::preRegisterTerm(TNode node)
     // The may equal needs the store
     d_mayEqualEqualityEngine.addTerm(store);
 
-    // Apply RIntro1 rule to any stores equal to store if not done already
-    const CTNodeList* stores = d_infoMap.getStores(store);
-    CTNodeList::const_iterator it = stores->begin();
-    if (it != stores->end()) {
-      NodeManager* nm = NodeManager::currentNM();
-      TNode s = *it;
-      if (!d_infoMap.rIntro1Applied(s)) {
-        d_infoMap.setRIntro1Applied(s);
-        Assert(s.getKind()==kind::STORE);
-        Node ni = nm->mkNode(kind::SELECT, s, s[1]);
-        if (ni != node) {
-          preRegisterTerm(ni);
+    if (options::arraysLazyRIntro1()) {
+      // Apply RIntro1 rule to any stores equal to store if not done already
+      const CTNodeList* stores = d_infoMap.getStores(store);
+      CTNodeList::const_iterator it = stores->begin();
+      if (it != stores->end()) {
+        NodeManager* nm = NodeManager::currentNM();
+        TNode s = *it;
+        if (!d_infoMap.rIntro1Applied(s)) {
+          d_infoMap.setRIntro1Applied(s);
+          Assert(s.getKind()==kind::STORE);
+          Node ni = nm->mkNode(kind::SELECT, s, s[1]);
+          if (ni != node) {
+            preRegisterTerm(ni);
+          }
+          d_equalityEngine.assertEquality(ni.eqNode(s[2]), true, d_true);
+          Assert(++it == stores->end());
         }
-        d_equalityEngine.assertEquality(ni.eqNode(s[2]), true, d_true);
-        Assert(++it == stores->end());
       }
     }
 
@@ -426,19 +432,21 @@ void TheoryArrays::preRegisterTerm(TNode node)
     d_equalityEngine.addTriggerTerm(node, THEORY_ARRAY);
 
     TNode a = d_equalityEngine.getRepresentative(node[0]);
-    //    TNode i = node[1];
-    //    TNode v = node[2];
 
     d_mayEqualEqualityEngine.assertEquality(node.eqNode(a), true, d_true);
 
-    // NodeManager* nm = NodeManager::currentNM();
-    // Node ni = nm->mkNode(kind::SELECT, node, i);
-    // if (!d_equalityEngine.hasTerm(ni)) {
-    //   preRegisterTerm(ni);
-    // }
+    if (!options::arraysLazyRIntro1()) {
+      TNode i = node[1];
+      TNode v = node[2];
+      NodeManager* nm = NodeManager::currentNM();
+      Node ni = nm->mkNode(kind::SELECT, node, i);
+      if (!d_equalityEngine.hasTerm(ni)) {
+        preRegisterTerm(ni);
+      }
 
-    // // Apply RIntro1 Rule
-    // d_equalityEngine.addEquality(ni, v, d_true);
+      // Apply RIntro1 Rule
+      d_equalityEngine.assertEquality(ni.eqNode(v), true, d_true);
+    }
 
     d_infoMap.addStore(node, node);
     d_infoMap.addInStore(a, node);
@@ -982,10 +990,12 @@ void TheoryArrays::mergeArrays(TNode a, TNode b)
   while (true) {
     Trace("arrays-merge") << spaces(getSatContext()->getLevel()) << "Arrays::merge: " << a << "," << b << ")\n";
 
-    checkRIntro1(a, b);
-    checkRIntro1(b, a);
+    if (options::arraysLazyRIntro1()) {
+      checkRIntro1(a, b);
+      checkRIntro1(b, a);
+    }
 
-    if (d_useNonLinearOpt) {
+    if (options::arraysOptimizeLinear()) {
       bool aNL = d_infoMap.isNonLinear(a);
       bool bNL = d_infoMap.isNonLinear(b);
       if (aNL) {
@@ -1051,7 +1061,7 @@ void TheoryArrays::checkStore(TNode a) {
 
   TNode brep = d_equalityEngine.getRepresentative(b);
 
-  if (!d_useNonLinearOpt || d_infoMap.isNonLinear(brep)) {
+  if (!options::arraysOptimizeLinear() || d_infoMap.isNonLinear(brep)) {
     const CTNodeList* js = d_infoMap.getIndices(brep);
     size_t it = 0;
     RowLemmaType lem;
@@ -1092,7 +1102,7 @@ void TheoryArrays::checkRowForIndex(TNode i, TNode a)
     queueRowLemma(lem);
   }
 
-  if (!d_useNonLinearOpt || d_infoMap.isNonLinear(a)) {
+  if (!options::arraysOptimizeLinear() || d_infoMap.isNonLinear(a)) {
     it = 0;
     for(; it < instores->size(); ++it) {
       TNode instore = (*instores)[it];
@@ -1141,7 +1151,7 @@ void TheoryArrays::checkRowLemmas(TNode a, TNode b)
     }
   }
 
-  if (!d_useNonLinearOpt || d_infoMap.isNonLinear(b)) {
+  if (!options::arraysOptimizeLinear() || d_infoMap.isNonLinear(b)) {
     for(it = 0 ; it < i_a->size(); ++it ) {
       TNode i = (*i_a)[it];
       its = 0;

diff --git a/src/theory/model.cpp b/src/theory/model.cpp
index 957491d37c424336f3f0bfcde2843be8daaec103..2b819d6bd314ed7a82802904760c4c8ededc0bb7 100644 (file)
--- a/src/theory/model.cpp
+++ b/src/theory/model.cpp
@@ -226,8 +226,8 @@ void TheoryModel::assertEquality( Node a, Node b, bool polarity ){
   if (a == b && polarity) {
     return;
   }
-  d_equalityEngine.assertEquality( a.eqNode(b), polarity, Node::null() );
   Trace("model-builder-assertions") << "(assert " << (polarity ? "(= " : "(not (= ") << a << " " << b << (polarity ? "));" : ")));") << endl;
+  d_equalityEngine.assertEquality( a.eqNode(b), polarity, Node::null() );
   Assert(d_equalityEngine.consistent());
 }
 
@@ -240,8 +240,8 @@ void TheoryModel::assertPredicate( Node a, bool polarity ){
   if( a.getKind()==EQUAL ){
     d_equalityEngine.assertEquality( a, polarity, Node::null() );
   }else{
-    d_equalityEngine.assertPredicate( a, polarity, Node::null() );
     Trace("model-builder-assertions") << "(assert " << (polarity ? "" : "(not ") << a << (polarity ? ");" : "));") << endl;
+    d_equalityEngine.assertPredicate( a, polarity, Node::null() );
     Assert(d_equalityEngine.consistent());
   }
 }
@@ -269,7 +269,7 @@ void TheoryModel::assertEqualityEngine( const eq::EqualityEngine* ee ){
           assertPredicate(*eqc_i, false);
         }
         else if (eqc != (*eqc_i)) {
-          Trace("model-builder-assertions") << "(assert (iff " << *eqc_i << " " << eqc << "));" << endl;
+          Trace("model-builder-assertions") << "(assert (= " << *eqc_i << " " << eqc << "));" << endl;
           d_equalityEngine.mergePredicates(*eqc_i, eqc, Node::null());
           Assert(d_equalityEngine.consistent());
         }
@@ -451,9 +451,6 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel)
       for (it = typeNoRepSet.begin(); it != typeNoRepSet.end(); ++it) {
         TypeNode t = TypeSet::getType(it);
         Trace("model-builder") << "  Working on type: " << t << endl;
-        // This assertion may be too strong, but hopefully not: we expect that for every type, either all of its EC's have asserted reps (or constants)
-        // or none of its EC's have asserted reps.
-        Assert(!fullModel || typeRepSet.getSet(t) == NULL);
         set<Node>& noRepSet = TypeSet::getSet(it);
         if (noRepSet.empty()) {
           continue;

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index d5c4998d4915c5be670b03b5a47554ab59c506a2..a952c9ee62c914dfe5391d0e4b716b5f07ccd367 100644 (file)
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -563,7 +563,11 @@ void TheoryEngine::collectModelInfo( theory::TheoryModel* m, bool fullModel ){
     TNode var = *it;
     hasValue = d_propEngine->hasValue(var, value);
     // TODO: Assert that hasValue is true?
-    m->assertPredicate(var, hasValue ? value : false);
+    if (!hasValue) {
+      value = false;
+    }
+    Trace("model-builder-assertions") << "(assert" << (value ? " " : " (not ") << var << (value ? ");" : "));") << endl;
+    m->assertPredicate(var, value);
   }
 }