diff options
Diffstat (limited to 'src/theory/idl')
| -rw-r--r-- | src/theory/idl/idl_assertion.cpp | 213 | ||||
| -rw-r--r-- | src/theory/idl/idl_assertion.h | 91 | ||||
| -rw-r--r-- | src/theory/idl/idl_assertion_db.cpp | 59 | ||||
| -rw-r--r-- | src/theory/idl/idl_assertion_db.h | 86 | ||||
| -rw-r--r-- | src/theory/idl/idl_model.cpp | 74 | ||||
| -rw-r--r-- | src/theory/idl/idl_model.h | 84 | ||||
| -rw-r--r-- | src/theory/idl/kinds | 8 | ||||
| -rw-r--r-- | src/theory/idl/theory_idl.cpp | 156 | ||||
| -rw-r--r-- | src/theory/idl/theory_idl.h | 63 |
9 files changed, 0 insertions, 834 deletions
diff --git a/src/theory/idl/idl_assertion.cpp b/src/theory/idl/idl_assertion.cpp deleted file mode 100644 index 1e3905537..000000000 --- a/src/theory/idl/idl_assertion.cpp +++ /dev/null @@ -1,213 +0,0 @@ -/********************* */ -/*! \file idl_assertion.cpp - ** \verbatim - ** Top contributors (to current version): - ** Dejan Jovanovic - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. - ** All rights reserved. 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/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) { - ok = 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) { - 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 deleted file mode 100644 index e24fbfc67..000000000 --- a/src/theory/idl/idl_assertion.h +++ /dev/null @@ -1,91 +0,0 @@ -/********************* */ -/*! \file idl_assertion.h - ** \verbatim - ** Top contributors (to current version): - ** Dejan Jovanovic - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. - ** All rights reserved. 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 - **/ - -#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 deleted file mode 100644 index 865d8b4f5..000000000 --- a/src/theory/idl/idl_assertion_db.cpp +++ /dev/null @@ -1,59 +0,0 @@ -/********************* */ -/*! \file idl_assertion_db.cpp - ** \verbatim - ** Top contributors (to current version): - ** Dejan Jovanovic - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. - ** All rights reserved. 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/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 deleted file mode 100644 index ac87282d9..000000000 --- a/src/theory/idl/idl_assertion_db.h +++ /dev/null @@ -1,86 +0,0 @@ -/********************* */ -/*! \file idl_assertion_db.h - ** \verbatim - ** Top contributors (to current version): - ** Dejan Jovanovic, Morgan Deters - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. - ** All rights reserved. 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 - **/ - -#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 index 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; - }; -}; - -} -} -} - - - - diff --git a/src/theory/idl/idl_model.cpp b/src/theory/idl/idl_model.cpp deleted file mode 100644 index 4a3426222..000000000 --- a/src/theory/idl/idl_model.cpp +++ /dev/null @@ -1,74 +0,0 @@ -/********************* */ -/*! \file idl_model.cpp - ** \verbatim - ** Top contributors (to current version): - ** Dejan Jovanovic - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. - ** All rights reserved. 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/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.d_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.d_constraint << std::endl; - reasons.push_back(reason.d_constraint); - current = reason.d_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 deleted file mode 100644 index 610b90695..000000000 --- a/src/theory/idl/idl_model.h +++ /dev/null @@ -1,84 +0,0 @@ -/********************* */ -/*! \file idl_model.h - ** \verbatim - ** Top contributors (to current version): - ** Dejan Jovanovic, Morgan Deters - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. - ** All rights reserved. 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 - **/ - -#pragma once - -#include "context/cdhashmap.h" -#include "expr/node.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 d_x; - /** The constraint of the reason */ - TNode d_constraint; - - IDLReason(TNode x, TNode constraint) : d_x(x), d_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; -} - -} // namespace idl -} // namespace theory -} // namespace CVC4 diff --git a/src/theory/idl/kinds b/src/theory/idl/kinds deleted file mode 100644 index 6bf0218b0..000000000 --- a/src/theory/idl/kinds +++ /dev/null @@ -1,8 +0,0 @@ -# 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/theory_idl.cpp b/src/theory/idl/theory_idl.cpp deleted file mode 100644 index f92738bcb..000000000 --- a/src/theory/idl/theory_idl.cpp +++ /dev/null @@ -1,156 +0,0 @@ -/********************* */ -/*! \file theory_idl.cpp - ** \verbatim - ** Top contributors (to current version): - ** Dejan Jovanovic, Tim King, Morgan Deters - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. - ** All rights reserved. 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 <set> -#include <queue> - -#include "options/idl_options.h" -#include "theory/rewriter.h" - - -using namespace std; - -namespace CVC4 { -namespace theory { -namespace idl { - -TheoryIdl::TheoryIdl(context::Context* c, context::UserContext* u, - OutputChannel& out, Valuation valuation, - const LogicInfo& logicInfo) - : Theory(THEORY_ARITH, c, u, out, valuation, logicInfo) - , 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) { - if (done() && !fullEffort(level)) { - return; - } - - TimerStat::CodeTimer checkTimer(d_checkTime); - - while(!done()) { - - // Get the next assertion - Assertion assertion = get(); - Debug("theory::idl") << "TheoryIdl::check(): processing " - << assertion.d_assertion << std::endl; - - // Convert the assertion into the internal representation - IDLAssertion idlAssertion(assertion.d_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; -} - -} /* namepsace CVC4::theory::idl */ -} /* namepsace CVC4::theory */ -} /* namepsace CVC4 */ diff --git a/src/theory/idl/theory_idl.h b/src/theory/idl/theory_idl.h deleted file mode 100644 index 1d48d0785..000000000 --- a/src/theory/idl/theory_idl.h +++ /dev/null @@ -1,63 +0,0 @@ -/********************* */ -/*! \file theory_idl.h - ** \verbatim - ** Top contributors (to current version): - ** Dejan Jovanovic, Mathias Preiner, Tim King - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. - ** All rights reserved. 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 - **/ - -#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); - - /** Pre-processing of input atoms */ - Node ppRewrite(TNode atom) override; - - /** Check the assertions for satisfiability */ - void check(Effort effort) override; - - /** Identity string */ - std::string identify() const override { return "THEORY_IDL"; } - -};/* class TheoryIdl */ - -}/* CVC4::theory::idl namespace */ -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ |