From: Dejan Jovanović Date: Wed, 5 Jun 2013 20:35:37 +0000 (-0400) Subject: IDL example theory (to be used with --use-theory=idl). X-Git-Tag: cvc5-1.0.0~7287^2~107 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=482167cc10c5df25e107e0b44a24c125f7b18bd2;p=cvc5.git IDL example theory (to be used with --use-theory=idl). --- diff --git a/.project b/.project index 252288336..b1fd9f133 100644 --- a/.project +++ b/.project @@ -1,6 +1,6 @@ - cvc4-bvprop + cvc4-idl diff --git a/src/options/Makefile.am b/src/options/Makefile.am index 21988df56..670718e4e 100644 --- a/src/options/Makefile.am +++ b/src/options/Makefile.am @@ -36,7 +36,9 @@ 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 OPTIONS_FILES = \ $(patsubst %.cpp,%,$(filter %.cpp,$(OPTIONS_FILES_SRCS))) @@ -93,7 +95,9 @@ nodist_liboptions_la_SOURCES = \ ../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 \ diff --git a/src/theory/Makefile.am b/src/theory/Makefile.am index 70962e6ed..2df698da4 100644 --- a/src/theory/Makefile.am +++ b/src/theory/Makefile.am @@ -3,7 +3,7 @@ AM_CPPFLAGS = \ -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 @@ -60,7 +60,8 @@ libtheory_la_LIBADD = \ @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 \ diff --git a/src/theory/idl/Makefile b/src/theory/idl/Makefile new file mode 100644 index 000000000..7c57f81ef --- /dev/null +++ b/src/theory/idl/Makefile @@ -0,0 +1,4 @@ +topdir = ../../.. +srcdir = src/theory/rdl + +include $(topdir)/Makefile.subdir diff --git a/src/theory/idl/Makefile.am b/src/theory/idl/Makefile.am new file mode 100644 index 000000000..4297e3bdb --- /dev/null +++ b/src/theory/idl/Makefile.am @@ -0,0 +1,19 @@ +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 diff --git a/src/theory/idl/idl_assertion.cpp b/src/theory/idl/idl_assertion.cpp new file mode 100644 index 000000000..c84989d4f --- /dev/null +++ b/src/theory/idl/idl_assertion.cpp @@ -0,0 +1,196 @@ +#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(); + 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(); + 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; +} diff --git a/src/theory/idl/idl_assertion.h b/src/theory/idl/idl_assertion.h new file mode 100644 index 000000000..2ed5a6bef --- /dev/null +++ b/src/theory/idl/idl_assertion.h @@ -0,0 +1,74 @@ +#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; +} + +} +} +} diff --git a/src/theory/idl/idl_assertion_db.cpp b/src/theory/idl/idl_assertion_db.cpp new file mode 100644 index 000000000..7c27e9d0d --- /dev/null +++ b/src/theory/idl/idl_assertion_db.cpp @@ -0,0 +1,42 @@ +#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; +} diff --git a/src/theory/idl/idl_assertion_db.h b/src/theory/idl/idl_assertion_db.h new file mode 100644 index 000000000..3972819da --- /dev/null +++ b/src/theory/idl/idl_assertion_db.h @@ -0,0 +1,69 @@ +#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 d_assertions; + + typedef context::CDHashMap 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; + }; +}; + +} +} +} + + + + diff --git a/src/theory/idl/idl_model.cpp b/src/theory/idl/idl_model.cpp new file mode 100644 index 000000000..2feabd700 --- /dev/null +++ b/src/theory/idl/idl_model.cpp @@ -0,0 +1,47 @@ +#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& 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 << "]"; +} diff --git a/src/theory/idl/idl_model.h b/src/theory/idl/idl_model.h new file mode 100644 index 000000000..a1840a35a --- /dev/null +++ b/src/theory/idl/idl_model.h @@ -0,0 +1,67 @@ +#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 model_value_map; + typedef context::CDHashMap 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& 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; +} + +} +} +} diff --git a/src/theory/idl/kinds b/src/theory/idl/kinds new file mode 100644 index 000000000..6bf0218b0 --- /dev/null +++ b/src/theory/idl/kinds @@ -0,0 +1,8 @@ +# 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" + diff --git a/src/theory/idl/options b/src/theory/idl/options new file mode 100644 index 000000000..0048353b9 --- /dev/null +++ b/src/theory/idl/options @@ -0,0 +1,10 @@ +# +# 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 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 +#include + +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 queue; // Queue of variables to consider + std::set 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 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; +} diff --git a/src/theory/idl/theory_idl.h b/src/theory/idl/theory_idl.h new file mode 100644 index 000000000..25b992981 --- /dev/null +++ b/src/theory/idl/theory_idl.h @@ -0,0 +1,46 @@ +#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 */