<?xml version="1.0" encoding="UTF-8"?>
<projectDescription>
- <name>cvc4-bvprop</name>
+ <name>cvc4-idl</name>
<comment></comment>
<projects>
</projects>
../main/options.cpp \
../main/options.h \
../parser/options.cpp \
- ../parser/options.h
+ ../parser/options.h \
+ ../theory/idl/options.cpp \
+ ../theory/idl/options.h
OPTIONS_FILES = \
$(patsubst %.cpp,%,$(filter %.cpp,$(OPTIONS_FILES_SRCS)))
../main/options.cpp \
../main/options.h \
../parser/options.cpp \
- ../parser/options.h
+ ../parser/options.h \
+ ../theory/idl/options.cpp \
+ ../theory/idl/options.h
BUILT_SOURCES = \
exprs-builts \
-I@builddir@/.. -I@srcdir@/../include -I@srcdir@/..
AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN)
-SUBDIRS = builtin booleans uf arith bv arrays datatypes quantifiers rewriterules
+SUBDIRS = builtin booleans uf arith bv arrays datatypes quantifiers rewriterules idl
DIST_SUBDIRS = $(SUBDIRS) example
noinst_LTLIBRARIES = libtheory.la
@builddir@/bv/libbv.la \
@builddir@/datatypes/libdatatypes.la \
@builddir@/quantifiers/libquantifiers.la \
- @builddir@/rewriterules/librewriterules.la
+ @builddir@/rewriterules/librewriterules.la \
+ @builddir@/idl/libidl.la
EXTRA_DIST = \
logic_info.i \
--- /dev/null
+topdir = ../../..
+srcdir = src/theory/rdl
+
+include $(topdir)/Makefile.subdir
--- /dev/null
+AM_CPPFLAGS = \
+ -D__BUILDING_CVC4LIB \
+ -I@builddir@/../.. -I@srcdir@/../../include -I@srcdir@/../..
+AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN)
+
+noinst_LTLIBRARIES = libidl.la
+
+libidl_la_SOURCES = \
+ idl_model.h \
+ idl_model.cpp \
+ idl_assertion.h \
+ idl_assertion.cpp \
+ idl_assertion_db.h \
+ idl_assertion_db.cpp \
+ theory_idl.h \
+ theory_idl.cpp
+
+EXTRA_DIST = \
+ kinds
--- /dev/null
+#include "theory/idl/idl_assertion.h"
+
+using namespace CVC4;
+using namespace theory;
+using namespace idl;
+
+IDLAssertion::IDLAssertion()
+: d_op(kind::LAST_KIND)
+{}
+
+IDLAssertion::IDLAssertion(TNode node) {
+ bool ok = parse(node, 1, false);
+ if (!ok) {
+ d_x = d_y = TNode::null();
+ } else {
+ if (d_op == kind::GT) {
+ // Turn GT into LT x - y > c is the same as y - x < -c
+ std::swap(d_x, d_y);
+ d_c = -d_c;
+ d_op = kind::LT;
+ }
+ if (d_op == kind::GEQ) {
+ // Turn GT into LT x - y >= c is the same as y - x <= -c
+ std::swap(d_x, d_y);
+ d_c = -d_c;
+ d_op = kind::LEQ;
+ }
+ if (d_op == kind::LT) {
+ // Turn strict into non-strict x - y < c is the same as x - y <= c-1
+ d_c = d_c - 1;
+ d_op = kind::LEQ;
+ }
+ }
+ d_original = node;
+}
+
+IDLAssertion::IDLAssertion(const IDLAssertion& other)
+: d_x(other.d_x)
+, d_y(other.d_y)
+, d_op(other.d_op)
+, d_c(other.d_c)
+, d_original(other.d_original)
+{}
+
+bool IDLAssertion::propagate(IDLModel& model) const {
+ Debug("theory::idl::model") << model << std::endl;
+ Assert(ok());
+ // Should be d_x - d_y <= d_c, or d_x - d_c <= d_y
+ Integer x_value = model.getValue(d_x);
+ Integer y_value = model.getValue(d_y);
+ if (x_value - y_value > d_c) {
+ model.setValue(d_y, x_value - d_c, IDLReason(d_x, d_original));
+ Debug("theory::idl::model") << model << std::endl;
+ return true;
+ } else {
+ return false;
+ }
+}
+
+void IDLAssertion::toStream(std::ostream& out) const {
+ out << "IDL[" << d_x << " - " << d_y << " " << d_op << " " << d_c << "]";
+}
+
+/** Negates the given arithmetic kind */
+static Kind negateOp(Kind op) {
+ switch (op) {
+ case kind::LT:
+ // not (a < b) = (a >= b)
+ return kind::GEQ;
+ case kind::LEQ:
+ // not (a <= b) = (a > b)
+ return kind::GT;
+ case kind::GT:
+ // not (a > b) = (a <= b)
+ return kind::LEQ;
+ case kind::GEQ:
+ // not (a >= b) = (a < b)
+ return kind::LT;
+ case kind::EQUAL:
+ // not (a = b) = (a != b)
+ return kind::DISTINCT;
+ case kind::DISTINCT:
+ // not (a != b) = (a = b)
+ return kind::EQUAL;
+ default:
+ Unreachable();
+ break;
+ }
+ return kind::LAST_KIND;
+}
+
+bool IDLAssertion::parse(TNode node, int c, bool negated) {
+
+ // Only unit coefficients allowed
+ if (c != 1 && c != -1) {
+ return false;
+ }
+
+ // Assume we're ok
+ bool ok = true;
+
+ // The kind of the node
+ switch(node.getKind()) {
+
+ case kind::NOT:
+ // We parse the negation
+ ok = parse(node[0], c, true);
+ // Setup the kind
+ if(ok) {
+ d_op = negateOp(d_op);
+ }
+ break;
+
+ case kind::EQUAL:
+ case kind::LT:
+ case kind::LEQ:
+ case kind::GT:
+ case kind::GEQ: {
+ // All relation operators are parsed on both sides
+ d_op = node.getKind();
+ ok = parse(node[0], c, negated);
+ if(ok) {
+ ok = parse(node[1],-c, negated);
+ }
+ break;
+ }
+
+ case kind::CONST_RATIONAL: {
+ // Constants
+ Rational m = node.getConst<Rational>();
+ if (m.isIntegral()) {
+ d_c += m.getNumerator() * (-c);
+ } else {
+ ok = false;
+ }
+ break;
+ }
+ case kind::MULT: {
+ // Only unit multiplication of variables
+ if(node.getNumChildren() == 2 && node[0].isConst()) {
+ Rational a = node[0].getConst<Rational>();
+ if(a == 1 || a == -1) {
+ return parse(node[1], c * a.sgn(), negated);
+ } else {
+ ok = false;
+ }
+ } else {
+ ok = false;
+ }
+ break;
+ }
+
+ case kind::PLUS: {
+ for(unsigned i = 0; i < node.getNumChildren(); ++i) {
+ bool ok = parse(node[i], c, negated);
+ if(!ok) {
+ break;
+ }
+ }
+ break;
+ }
+
+ case kind::MINUS: {
+ ok = parse(node[0], c, negated);
+ if(ok) {
+ ok = parse(node[1], -c, negated);
+ }
+ break;
+ }
+
+ case kind::UMINUS: {
+ ok = parse(node[0], -c, negated);
+ break;
+ }
+
+ default: {
+ if(c > 0) {
+ if(d_x.isNull()) {
+ d_x = node;
+ } else {
+ ok = false;
+ }
+ } else {
+ if(d_y.isNull()) {
+ d_y = node;
+ } else {
+ ok = false;
+ }
+ }
+ break;
+ }
+ } // End case
+
+ // Difference logic OK
+ return ok;
+}
--- /dev/null
+#pragma once
+
+#include "theory/idl/idl_model.h"
+
+namespace CVC4 {
+namespace theory {
+namespace idl {
+
+/**
+ * An internal representation of the IDL assertions. Each IDL assertions is
+ * of the form (x - y op c) where op is one of (<=, =, !=). IDL assertion
+ * can be constructed from an expression.
+ */
+class IDLAssertion {
+
+ /** The positive variable */
+ TNode d_x;
+ /** The negative variable */
+ TNode d_y;
+ /** The relation */
+ Kind d_op;
+ /** The RHS constant */
+ Integer d_c;
+
+ /** Original assertion we got this one from */
+ TNode d_original;
+
+ /** Parses the given node into an assertion, and return true if OK. */
+ bool parse(TNode node, int c = 1, bool negated = false);
+
+public:
+
+ /** Null assertion */
+ IDLAssertion();
+ /** Create the assertion from given node */
+ IDLAssertion(TNode node);
+ /** Copy constructor */
+ IDLAssertion(const IDLAssertion& other);
+
+ TNode getX() const { return d_x; }
+ TNode getY() const { return d_y; }
+ Kind getOp() const { return d_op;}
+ Integer getC() const { return d_c; }
+
+ /**
+ * Propagate the constraint using the model. For example, if the constraint
+ * is of the form x - y <= -1, and the value of x in the model is 0, then
+ *
+ * (x - y <= -1) and (x = 0) implies y >= x + 1 = 1
+ *
+ * If the value of y is less then 1, is is set to 1 and true is returned. If
+ * the value of y is 1 or more, than false is return.
+ *
+ * @return true if value of y was updated
+ */
+ bool propagate(IDLModel& model) const;
+
+ /** Is this constraint proper */
+ bool ok() const {
+ return !d_x.isNull() || !d_y.isNull();
+ }
+
+ /** Output to the stream */
+ void toStream(std::ostream& out) const;
+};
+
+inline std::ostream& operator << (std::ostream& out, const IDLAssertion& assertion) {
+ assertion.toStream(out);
+ return out;
+}
+
+}
+}
+}
--- /dev/null
+#include "theory/idl/idl_assertion_db.h"
+
+using namespace CVC4;
+using namespace theory;
+using namespace idl;
+
+IDLAssertionDB::IDLAssertionDB(context::Context* c)
+: d_assertions(c)
+, d_variableLists(c)
+{}
+
+void IDLAssertionDB::add(const IDLAssertion& assertion, TNode var) {
+ // Is there a list for the variable already?
+ unsigned previous = -1;
+ var_to_unsigned_map::iterator find = d_variableLists.find(var);
+ if (find != d_variableLists.end()) {
+ previous = (*find).second;
+ }
+ // Add to the DB
+ d_variableLists[var] = d_assertions.size();
+ d_assertions.push_back(IDLAssertionListElement(assertion, previous));
+}
+
+IDLAssertionDB::iterator::iterator(IDLAssertionDB& db, TNode var)
+: d_db(db)
+, d_current(-1)
+{
+ var_to_unsigned_map::const_iterator find = d_db.d_variableLists.find(var);
+ if (find != d_db.d_variableLists.end()) {
+ d_current = (*find).second;
+ }
+}
+
+void IDLAssertionDB::iterator::next() {
+ if (d_current != (unsigned)(-1)) {
+ d_current = d_db.d_assertions[d_current].d_previous;
+ }
+}
+
+IDLAssertion IDLAssertionDB::iterator::get() const {
+ return d_db.d_assertions[d_current].d_assertion;
+}
--- /dev/null
+#pragma once
+
+#include "theory/idl/idl_assertion.h"
+#include "context/cdlist.h"
+
+namespace CVC4 {
+namespace theory {
+namespace idl {
+
+/**
+ * Context-dependent database assertions, organized by variable. Each variable
+ * can be associated a list of IDL assertions. The list of assertions can
+ * be iterated over using the provided iterator class.
+ */
+class IDLAssertionDB {
+
+ /** Elements of the assertion lists */
+ struct IDLAssertionListElement {
+ /** The assertion itself */
+ IDLAssertion d_assertion;
+ /** The inndex of the previous element (-1 for null) */
+ unsigned d_previous;
+
+ IDLAssertionListElement(const IDLAssertion& assertion, unsigned previous)
+ : d_assertion(assertion), d_previous(previous)
+ {}
+ };
+
+ /** All assertions in a context dependent stack */
+ context::CDList<IDLAssertionListElement> d_assertions;
+
+ typedef context::CDHashMap<TNode, unsigned, TNodeHashFunction> var_to_unsigned_map;
+
+ /** Map from variables to the first element of their list */
+ var_to_unsigned_map d_variableLists;
+
+public:
+
+ /** Create a new assertion database */
+ IDLAssertionDB(context::Context* c);
+
+ /** Add a new assertion, attach to the list of the given variable */
+ void add(const IDLAssertion& assertion, TNode var);
+
+ /** Iteration over the constraints of a variable */
+ class iterator {
+ /** The database */
+ const IDLAssertionDB& d_db;
+ /** Index of the current constraint */
+ unsigned d_current;
+ public:
+ /** Construct the iterator for the variable */
+ iterator(IDLAssertionDB& db, TNode var);
+ /** Is this iterator done */
+ bool done() const { return d_current == (unsigned)(-1); }
+ /** Next element */
+ void next();
+ /** Get the assertion */
+ IDLAssertion get() const;
+ };
+};
+
+}
+}
+}
+
+
+
+
--- /dev/null
+#include "theory/idl/idl_model.h"
+
+using namespace CVC4;
+using namespace theory;
+using namespace idl;
+
+IDLModel::IDLModel(context::Context* context)
+: d_model(context)
+, d_reason(context)
+{}
+
+Integer IDLModel::getValue(TNode var) const {
+ model_value_map::const_iterator find = d_model.find(var);
+ if (find != d_model.end()) {
+ return (*find).second;
+ } else {
+ return 0;
+ }
+}
+
+void IDLModel::setValue(TNode var, Integer value, IDLReason reason) {
+ Assert(!reason.constraint.isNull());
+ d_model[var] = value;
+ d_reason[var] = reason;
+}
+
+void IDLModel::getReasonCycle(TNode var, std::vector<TNode>& reasons) {
+ TNode current = var;
+ do {
+ Debug("theory::idl::model") << "processing: " << var << std::endl;
+ Assert(d_reason.find(current) != d_reason.end());
+ IDLReason reason = d_reason[current];
+ Debug("theory::idl::model") << "adding reason: " << reason.constraint << std::endl;
+ reasons.push_back(reason.constraint);
+ current = reason.x;
+ } while (current != var);
+}
+
+void IDLModel::toStream(std::ostream& out) const {
+ model_value_map::const_iterator it = d_model.begin();
+ model_value_map::const_iterator it_end = d_model.end();
+ out << "Model[" << std::endl;
+ for (; it != it_end; ++ it) {
+ out << (*it).first << " -> " << (*it).second << std::endl;
+ }
+ out << "]";
+}
--- /dev/null
+#pragma once
+
+#include "expr/node.h"
+#include "context/cdhashmap.h"
+
+namespace CVC4 {
+namespace theory {
+namespace idl {
+
+/**
+ * A reason for a value of a variable in the model is a constraint that implies
+ * this value by means of the value of another variable. For example, if the
+ * value of x is 0, then the variable x and the constraint (y > 0) are a reason
+ * for the y taking the value 1.
+ */
+struct IDLReason {
+ /** The variable of the reason */
+ TNode x;
+ /** The constraint of the reaason */
+ TNode constraint;
+
+ IDLReason(TNode x, TNode constraint)
+ : x(x), constraint(constraint) {}
+ IDLReason() {}
+};
+
+/**
+ * A model maps variables to integer values and backs them up with reasons.
+ * Default values (if not set with setValue) for all variables are 0.
+ */
+class IDLModel {
+
+ typedef context::CDHashMap<TNode, Integer, TNodeHashFunction> model_value_map;
+ typedef context::CDHashMap<TNode, IDLReason, TNodeHashFunction> model_reason_map;
+
+ /** Values assigned to individual variables */
+ model_value_map d_model;
+
+ /** Reasons constraining the individual variables */
+ model_reason_map d_reason;
+
+public:
+
+ IDLModel(context::Context* context);
+
+ /** Get the model value of the variable */
+ Integer getValue(TNode var) const;
+
+ /** Set the value of the variable */
+ void setValue(TNode var, Integer value, IDLReason reason);
+
+ /** Get the cycle of reasons behind the variable var */
+ void getReasonCycle(TNode var, std::vector<TNode>& reasons);
+
+ /** Output to the given stream */
+ void toStream(std::ostream& out) const;
+
+};
+
+inline std::ostream& operator << (std::ostream& out, const IDLModel& model) {
+ model.toStream(out);
+ return out;
+}
+
+}
+}
+}
--- /dev/null
+# kinds -*- sh -*-
+#
+# For documentation on this file format, please refer to
+# src/theory/builtin/kinds.
+#
+
+alternate THEORY_ARITH "idl" ::CVC4::theory::idl::TheoryIdl "theory/idl/theory_idl.h"
+
--- /dev/null
+#
+# Option specification file for CVC4
+# See src/options/base_options for a description of this file format
+#
+
+module IDL "theory/idl/options.h" Idl
+
+option idlRewriteEq --enable-idl-rewrite-equalities/--disable-idl-rewrite-equalities bool :default false :read-write
+
+endmodule
--- /dev/null
+#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;
+}
--- /dev/null
+#pragma once
+
+#include "cvc4_private.h"
+
+#include "theory/theory.h"
+#include "theory/idl/idl_model.h"
+#include "theory/idl/idl_assertion_db.h"
+
+namespace CVC4 {
+namespace theory {
+namespace idl {
+
+/**
+ * Handles integer difference logic (IDL) constraints.
+ */
+class TheoryIdl : public Theory {
+
+ /** The current model */
+ IDLModel d_model;
+
+ /** The asserted constraints, organized by variable */
+ IDLAssertionDB d_assertionsDB;
+
+ /** Process a new assertion, returns false if in conflict */
+ bool processAssertion(const IDLAssertion& assertion);
+
+public:
+
+ /** Theory constructor. */
+ TheoryIdl(context::Context* c, context::UserContext* u, OutputChannel& out,
+ Valuation valuation, const LogicInfo& logicInfo, QuantifiersEngine* qe);
+
+ /** Pre-processing of input atoms */
+ Node ppRewrite(TNode atom);
+
+ /** Check the assertions for satisfiability */
+ void check(Effort effort);
+
+ /** Identity string */
+ std::string identify() const { return "THEORY_IDL"; }
+
+};/* class TheoryIdl */
+
+}/* CVC4::theory::idl namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
projects / cvc5.git / commitdiff