diff options
Diffstat (limited to 'src/theory/idl/theory_idl.cpp')
-rw-r--r-- | src/theory/idl/theory_idl.cpp | 126 |
1 files changed, 126 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..bf2297d3d --- /dev/null +++ b/src/theory/idl/theory_idl.cpp @@ -0,0 +1,126 @@ +#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; +} |