merged golden

1 files changed, 143 insertions, 0 deletions

diff --git a/src/theory/idl/theory_idl.cpp b/src/theory/idl/theory_idl.cpp
new file mode 100644
index 000000000..e5100fc71
--- /dev/null
+++ b/src/theory/idl/theory_idl.cpp
@@ -0,0 +1,143 @@
+/*********************                                                        */
+/*! \file theory_idl.cpp
+ ** \verbatim
+ ** Original author: Dejan Jovanovic
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2013  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief [[ Add one-line brief description here ]]
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
+ **/
+
+#include "theory/idl/theory_idl.h"
+#include "theory/idl/options.h"
+#include "theory/rewriter.h"
+
+#include <set>
+#include <queue>
+
+using namespace std;
+
+using namespace CVC4;
+using namespace theory;
+using namespace idl;
+
+TheoryIdl::TheoryIdl(context::Context* c, context::UserContext* u, OutputChannel& out,
+                     Valuation valuation, const LogicInfo& logicInfo, QuantifiersEngine* qe)
+: Theory(THEORY_ARITH, c, u, out, valuation, logicInfo, qe)
+, d_model(c)
+, d_assertionsDB(c)
+{}
+
+Node TheoryIdl::ppRewrite(TNode atom) {
+  if (atom.getKind() == kind::EQUAL  && options::idlRewriteEq()) {
+    // If the option is turned on, each equality into two inequalities. This in
+    // effect removes equalities, and theorefore dis-equalities too.
+    Node leq = NodeBuilder<2>(kind::LEQ) << atom[0] << atom[1];
+    Node geq = NodeBuilder<2>(kind::GEQ) << atom[0] << atom[1];
+    Node rewritten = Rewriter::rewrite(leq.andNode(geq));
+    return rewritten;
+  } else {
+    return atom;
+  }
+}
+
+void TheoryIdl::check(Effort level) {
+
+  while(!done()) {
+
+    // Get the next assertion
+    Assertion assertion = get();
+    Debug("theory::idl") << "TheoryIdl::check(): processing " << assertion.assertion << std::endl;
+
+    // Convert the assertion into the internal representation
+    IDLAssertion idlAssertion(assertion.assertion);
+    Debug("theory::idl") << "TheoryIdl::check(): got " << idlAssertion << std::endl;
+
+    if (idlAssertion.ok()) {
+      if (idlAssertion.getOp() == kind::DISTINCT) {
+        // We don't handle dis-equalities
+        d_out->setIncomplete();
+      } else {
+        // Process the convex assertions immediately
+        bool ok = processAssertion(idlAssertion);
+        if (!ok) {
+          // In conflict, we're done
+          return;
+        }
+      }
+    } else {
+      // Not an IDL assertion, set incomplete
+      d_out->setIncomplete();
+    }
+  }
+
+}
+
+bool TheoryIdl::processAssertion(const IDLAssertion& assertion) {
+
+  Debug("theory::idl") << "TheoryIdl::processAssertion(" << assertion << ")" << std::endl;
+
+  // Add the constraint (x - y op c) to the list assertions of x
+  d_assertionsDB.add(assertion, assertion.getX());
+
+  // Update the model, if forced by the assertion
+  bool y_updated = assertion.propagate(d_model);
+
+  // If the value of y was updated, we might need to update further
+  if (y_updated) {
+
+    std::queue<TNode> queue; // Queue of variables to consider
+    std::set<TNode> inQueue; // Current elements of the queue
+
+    // Add the first updated variable to the queue
+    queue.push(assertion.getY());
+    inQueue.insert(assertion.getY());
+
+    while (!queue.empty()) {
+      // Pop a new variable x off the queue
+      TNode x = queue.front();
+      queue.pop();
+      inQueue.erase(x);
+
+      // Go through the constraint (x - y op c), and update values of y
+      IDLAssertionDB::iterator it(d_assertionsDB, x);
+      while (!it.done()) {
+        // Get the assertion and update y
+        IDLAssertion x_y_assertion = it.get();
+        y_updated = x_y_assertion.propagate(d_model);
+        // If updated add to the queue
+        if (y_updated) {
+          // If the variable that we updated is the same as the first
+          // variable that we updated, it's a cycle of updates => conflict
+          if (x_y_assertion.getY() == assertion.getX()) {
+            std::vector<TNode> reasons;
+            d_model.getReasonCycle(x_y_assertion.getY(), reasons);
+            // Construct the reason of the conflict
+            Node conflict = NodeManager::currentNM()->mkNode(kind::AND, reasons);
+            d_out->conflict(conflict);
+            return false;
+          } else {
+            // No cycle, just a model update, so we add to the queue
+            TNode y = x_y_assertion.getY();
+            if (inQueue.count(y) == 0) {
+              queue.push(y);
+              inQueue.insert(x_y_assertion.getY());
+            }
+          }
+        }
+        // Go to the next constraint
+        it.next();
+      }
+    }
+  }
+
+  // Everything fine, no conflict
+  return true;
+}