From: Morgan Deters <mdeters@gmail.com>
Date: Sun, 4 Jul 2010 04:38:58 +0000 (+0000)
Subject: enable arrays
X-Git-Tag: cvc5-1.0.0~8953
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=78f7f12f981982bc54435828aea224f785ec3f87;p=cvc5.git

enable arrays
---

diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h
index 17d0779ca..4d2f502fd 100644
--- a/src/theory/bv/theory_bv.h
+++ b/src/theory/bv/theory_bv.h
@@ -36,8 +36,8 @@ public:
 
   void preRegisterTerm(TNode n) { Unimplemented(); }
   void registerTerm(TNode n) { Unimplemented(); }
-  void check(Effort e) { Unimplemented(); }
-  void propagate(Effort e) { Unimplemented(); }
+  void check(Effort e) {}
+  void propagate(Effort e) {}
   void explain(TNode n, Effort e) { Unimplemented(); }
   std::string identify() const { return std::string("TheoryBV"); }
 };/* class TheoryBV */
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 92008cc99..24d1f4790 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -265,7 +265,7 @@ public:
       //d_bool.check(effort);
       d_uf.check(effort);
       d_arith.check(effort);
-      //d_arrays.check(effort);
+      d_arrays.check(effort);
       //d_bv.check(effort);
     } catch(const theory::Interrupted&) {
       Debug("theory") << "TheoryEngine::check() => conflict" << std::endl;
@@ -301,8 +301,12 @@ public:
   inline void propagate() {
     d_theoryOut.d_propagatedLiterals.clear();
     // Do the propagation
+    //d_builtin.propagate(theory::Theory::FULL_EFFORT);
+    //d_bool.propagate(theory::Theory::FULL_EFFORT);
     d_uf.propagate(theory::Theory::FULL_EFFORT);
     d_arith.propagate(theory::Theory::FULL_EFFORT);
+    d_arrays.propagate(theory::Theory::FULL_EFFORT);
+    //d_bv.propagate(theory::Theory::FULL_EFFORT);
   }
 
   inline Node getExplanation(TNode node){