shared_data.cpp \
rewriter.h \
rewriter_attributes.h \
- rewriter.cpp
+ rewriter.cpp \
+ valuation.h \
+ valuation.cpp
+
nodist_libtheory_la_SOURCES = \
rewriter_tables.h \
theory_traits.h
CLEANFILES = \
rewriter_tables.h \
- theory_traits.h
+ theory_traits.h
include @top_srcdir@/src/theory/Makefile.subdirs
$< \
`cat @top_builddir@/src/theory/.subdirs` \
> $@) || (rm -f $@ && exit 1)
-
\ No newline at end of file
#include "expr/metakind.h"
#include "expr/node_builder.h"
-#include "theory/theory_engine.h"
+#include "theory/valuation.h"
#include "util/rational.h"
#include "util/integer.h"
// }
}
-Node TheoryArith::getValue(TNode n, TheoryEngine* engine) {
+Node TheoryArith::getValue(TNode n, Valuation* valuation) {
NodeManager* nodeManager = NodeManager::currentNM();
switch(n.getKind()) {
Node eq = d_removedRows.find(var)->second;
Assert(n == eq[0]);
Node rhs = eq[1];
- return getValue(rhs, engine);
+ return getValue(rhs, valuation);
}
DeltaRational drat = d_partialModel.getAssignment(var);
case kind::EQUAL: // 2 args
return nodeManager->
- mkConst( engine->getValue(n[0]) == engine->getValue(n[1]) );
+ mkConst( valuation->getValue(n[0]) == valuation->getValue(n[1]) );
case kind::PLUS: { // 2+ args
Rational value = d_constants.d_ZERO;
iend = n.end();
i != iend;
++i) {
- value += engine->getValue(*i).getConst<Rational>();
+ value += valuation->getValue(*i).getConst<Rational>();
}
return nodeManager->mkConst(value);
}
iend = n.end();
i != iend;
++i) {
- value *= engine->getValue(*i).getConst<Rational>();
+ value *= valuation->getValue(*i).getConst<Rational>();
}
return nodeManager->mkConst(value);
}
Unreachable();
case kind::DIVISION: // 2 args
- return nodeManager->mkConst( engine->getValue(n[0]).getConst<Rational>() /
- engine->getValue(n[1]).getConst<Rational>() );
+ return nodeManager->mkConst( valuation->getValue(n[0]).getConst<Rational>() /
+ valuation->getValue(n[1]).getConst<Rational>() );
case kind::LT: // 2 args
- return nodeManager->mkConst( engine->getValue(n[0]).getConst<Rational>() <
- engine->getValue(n[1]).getConst<Rational>() );
+ return nodeManager->mkConst( valuation->getValue(n[0]).getConst<Rational>() <
+ valuation->getValue(n[1]).getConst<Rational>() );
case kind::LEQ: // 2 args
- return nodeManager->mkConst( engine->getValue(n[0]).getConst<Rational>() <=
- engine->getValue(n[1]).getConst<Rational>() );
+ return nodeManager->mkConst( valuation->getValue(n[0]).getConst<Rational>() <=
+ valuation->getValue(n[1]).getConst<Rational>() );
case kind::GT: // 2 args
- return nodeManager->mkConst( engine->getValue(n[0]).getConst<Rational>() >
- engine->getValue(n[1]).getConst<Rational>() );
+ return nodeManager->mkConst( valuation->getValue(n[0]).getConst<Rational>() >
+ valuation->getValue(n[1]).getConst<Rational>() );
case kind::GEQ: // 2 args
- return nodeManager->mkConst( engine->getValue(n[0]).getConst<Rational>() >=
- engine->getValue(n[1]).getConst<Rational>() );
+ return nodeManager->mkConst( valuation->getValue(n[0]).getConst<Rational>() >=
+ valuation->getValue(n[1]).getConst<Rational>() );
default:
Unhandled(n.getKind());
void notifyEq(TNode lhs, TNode rhs);
- Node getValue(TNode n, TheoryEngine* engine);
+ Node getValue(TNode n, Valuation* valuation);
void shutdown(){ }
#include "theory/arrays/theory_arrays.h"
-#include "theory/theory_engine.h"
+#include "theory/valuation.h"
#include "expr/kind.h"
Debug("arrays") << "TheoryArrays::check(): done" << endl;
}
-Node TheoryArrays::getValue(TNode n, TheoryEngine* engine) {
+Node TheoryArrays::getValue(TNode n, Valuation* valuation) {
NodeManager* nodeManager = NodeManager::currentNM();
switch(n.getKind()) {
case kind::EQUAL: // 2 args
return nodeManager->
- mkConst( engine->getValue(n[0]) == engine->getValue(n[1]) );
+ mkConst( valuation->getValue(n[0]) == valuation->getValue(n[1]) );
default:
Unhandled(n.getKind());
void check(Effort e);
void propagate(Effort e) { }
void explain(TNode n) { }
- Node getValue(TNode n, TheoryEngine* engine);
+ Node getValue(TNode n, Valuation* valuation);
void shutdown() { }
std::string identify() const { return std::string("TheoryArrays"); }
};/* class TheoryArrays */
#include "theory/theory.h"
#include "theory/booleans/theory_bool.h"
-#include "theory/theory_engine.h"
+#include "theory/valuation.h"
namespace CVC4 {
namespace theory {
namespace booleans {
-Node TheoryBool::getValue(TNode n, TheoryEngine* engine) {
+Node TheoryBool::getValue(TNode n, Valuation* valuation) {
NodeManager* nodeManager = NodeManager::currentNM();
switch(n.getKind()) {
Unreachable();
case kind::NOT: // 1 arg
- return nodeManager->mkConst(! engine->getValue(n[0]).getConst<bool>());
+ return nodeManager->mkConst(! valuation->getValue(n[0]).getConst<bool>());
case kind::AND: { // 2+ args
for(TNode::iterator i = n.begin(),
iend = n.end();
i != iend;
++i) {
- if(! engine->getValue(*i).getConst<bool>()) {
+ if(! valuation->getValue(*i).getConst<bool>()) {
return nodeManager->mkConst(false);
}
}
}
case kind::IFF: // 2 args
- return nodeManager->mkConst( engine->getValue(n[0]).getConst<bool>() ==
- engine->getValue(n[1]).getConst<bool>() );
+ return nodeManager->mkConst( valuation->getValue(n[0]).getConst<bool>() ==
+ valuation->getValue(n[1]).getConst<bool>() );
case kind::IMPLIES: // 2 args
- return nodeManager->mkConst( (! engine->getValue(n[0]).getConst<bool>()) ||
- engine->getValue(n[1]).getConst<bool>() );
+ return nodeManager->mkConst( (! valuation->getValue(n[0]).getConst<bool>()) ||
+ valuation->getValue(n[1]).getConst<bool>() );
case kind::OR: { // 2+ args
for(TNode::iterator i = n.begin(),
iend = n.end();
i != iend;
++i) {
- if(engine->getValue(*i).getConst<bool>()) {
+ if(valuation->getValue(*i).getConst<bool>()) {
return nodeManager->mkConst(true);
}
}
}
case kind::XOR: // 2 args
- return nodeManager->mkConst( engine->getValue(n[0]).getConst<bool>() !=
- engine->getValue(n[1]).getConst<bool>() );
+ return nodeManager->mkConst( valuation->getValue(n[0]).getConst<bool>() !=
+ valuation->getValue(n[1]).getConst<bool>() );
case kind::ITE: // 3 args
// all ITEs should be gone except (bool,bool,bool) ones
Assert( n[1].getType() == nodeManager->booleanType() &&
n[2].getType() == nodeManager->booleanType() );
- return nodeManager->mkConst( engine->getValue(n[0]).getConst<bool>() ?
- engine->getValue(n[1]).getConst<bool>() :
- engine->getValue(n[2]).getConst<bool>() );
+ return nodeManager->mkConst( valuation->getValue(n[0]).getConst<bool>() ?
+ valuation->getValue(n[1]).getConst<bool>() :
+ valuation->getValue(n[2]).getConst<bool>() );
default:
Unhandled(n.getKind());
Debug("bool") << "bool: end preRegisterTerm(" << n << ")" << std::endl;
}
- Node getValue(TNode n, TheoryEngine* engine);
+ Node getValue(TNode n, Valuation* valuation);
std::string identify() const { return std::string("TheoryBool"); }
};
**/
#include "theory/builtin/theory_builtin.h"
-#include "theory/theory_engine.h"
+#include "theory/valuation.h"
#include "expr/kind.h"
using namespace std;
namespace theory {
namespace builtin {
-Node TheoryBuiltin::getValue(TNode n, TheoryEngine* engine) {
+Node TheoryBuiltin::getValue(TNode n, Valuation* valuation) {
switch(n.getKind()) {
case kind::VARIABLE:
Assert(n[0].getKind() == kind::TUPLE &&
n[1].getKind() == kind::TUPLE);
return NodeManager::currentNM()->
- mkConst( getValue(n[0], engine) == getValue(n[1], engine) );
+ mkConst( getValue(n[0], valuation) == getValue(n[1], valuation) );
}
case kind::TUPLE: { // 2+ args
iend = n.end();
i != iend;
++i) {
- nb << engine->getValue(*i);
+ nb << valuation->getValue(*i);
}
return Node(nb);
}
default:
// all other "builtins" should have been rewritten away or handled
- // by theory engine, or handled elsewhere.
+ // by the valuation, or handled elsewhere.
Unhandled(n.getKind());
}
}
public:
TheoryBuiltin(context::Context* c, OutputChannel& out) :
Theory(THEORY_BUILTIN, c, out) {}
- Node getValue(TNode n, TheoryEngine* engine);
+ Node getValue(TNode n, Valuation* valuation);
std::string identify() const { return std::string("TheoryBuiltin"); }
};/* class TheoryBuiltin */
#include "theory/bv/theory_bv.h"
#include "theory/bv/theory_bv_utils.h"
-#include "theory/theory_engine.h"
+#include "theory/valuation.h"
using namespace CVC4;
using namespace CVC4::theory;
return true;
}
-Node TheoryBV::getValue(TNode n, TheoryEngine* engine) {
+Node TheoryBV::getValue(TNode n, Valuation* valuation) {
NodeManager* nodeManager = NodeManager::currentNM();
switch(n.getKind()) {
case kind::EQUAL: // 2 args
return nodeManager->
- mkConst( engine->getValue(n[0]) == engine->getValue(n[1]) );
+ mkConst( valuation->getValue(n[0]) == valuation->getValue(n[1]) );
default:
Unhandled(n.getKind());
void explain(TNode n) { }
- Node getValue(TNode n, TheoryEngine* engine);
+ Node getValue(TNode n, Valuation* valuation);
std::string identify() const { return std::string("TheoryBV"); }
};/* class TheoryBV */
class TheoryEngine;
+namespace theory {
+ class Valuation;
+}/* CVC4::theory namespace */
+
namespace theory {
/**
* if you *know* that you are responsible handle the Node you're
* asking for; other theories can use your types, so be careful
* here! To be safe, it's best to delegate back to the
- * TheoryEngine.
+ * TheoryEngine (by way of the Valuation proxy object, which avoids
+ * direct dependence on TheoryEngine).
*
* Usually, you need to handle at least the two cases of EQUAL and
* VARIABLE---EQUAL in case a value of yours is on the LHS of an
* and suspect this situation is the case, return Node::null()
* rather than throwing an exception.
*/
- virtual Node getValue(TNode n, TheoryEngine* engine) = 0;
+ virtual Node getValue(TNode n, Valuation* valuation) = 0;
/**
* The theory should only add (via .operator<< or .append()) to the
d_theoryRegistration(opts.theoryRegistration),
d_hasShutDown(false),
d_incomplete(ctxt, false),
+ d_valuation(this),
d_statistics() {
Rewriter::init();
return preprocessed;
}
+/**
+ * Check all (currently-active) theories for conflicts.
+ * @param effort the effort level to use
+ */
+bool TheoryEngine::check(theory::Theory::Effort effort) {
+ d_theoryOut.d_conflictNode = Node::null();
+ d_theoryOut.d_propagatedLiterals.clear();
+
+#ifdef CVC4_FOR_EACH_THEORY_STATEMENT
+#undef CVC4_FOR_EACH_THEORY_STATEMENT
+#endif
+#define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \
+ if (theory::TheoryTraits<THEORY>::hasCheck) { \
+ reinterpret_cast<theory::TheoryTraits<THEORY>::theory_class*>(d_theoryTable[THEORY])->check(effort); \
+ if (!d_theoryOut.d_conflictNode.get().isNull()) { \
+ return false; \
+ } \
+ }
+
+ // Do the checking
+ try {
+ CVC4_FOR_EACH_THEORY
+ } catch(const theory::Interrupted&) {
+ Debug("theory") << "TheoryEngine::check() => conflict" << std::endl;
+ }
+
+ return true;
+}
+
+void TheoryEngine::propagate() {
+ // Definition of the statement that is to be run by every theory
+#ifdef CVC4_FOR_EACH_THEORY_STATEMENT
+#undef CVC4_FOR_EACH_THEORY_STATEMENT
+#endif
+#define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \
+ if (theory::TheoryTraits<THEORY>::hasPropagate) { \
+ reinterpret_cast<theory::TheoryTraits<THEORY>::theory_class*>(d_theoryTable[THEORY])->propagate(theory::Theory::FULL_EFFORT); \
+ }
+
+ // Propagate for each theory using the statement above
+ CVC4_FOR_EACH_THEORY
+}
+
/* Our goal is to tease out any ITE's sitting under a theory operator. */
Node TheoryEngine::removeITEs(TNode node) {
Debug("ite") << "removeITEs(" << node << ")" << endl;
}
// otherwise ask the theory-in-charge
- return theoryOf(node)->getValue(node, this);
+ return theoryOf(node)->getValue(node, &d_valuation);
}/* TheoryEngine::getValue(TNode node) */
bool TheoryEngine::presolve() {
#include "prop/prop_engine.h"
#include "theory/shared_term_manager.h"
#include "theory/theory.h"
-#include "theory/theory_traits.h"
#include "theory/rewriter.h"
+#include "theory/valuation.h"
#include "util/options.h"
#include "util/stats.h"
*/
context::CDO<bool> d_incomplete;
+ /**
+ * A "valuation proxy" for this TheoryEngine. Used only in getValue()
+ * for decoupled Theory-to-TheoryEngine communication.
+ */
+ theory::Valuation d_valuation;
+
/**
* Replace ITE forms in a node.
*/
* Check all (currently-active) theories for conflicts.
* @param effort the effort level to use
*/
- inline bool check(theory::Theory::Effort effort)
- {
- d_theoryOut.d_conflictNode = Node::null();
- d_theoryOut.d_propagatedLiterals.clear();
-
-#ifdef CVC4_FOR_EACH_THEORY_STATEMENT
-#undef CVC4_FOR_EACH_THEORY_STATEMENT
-#endif
-#define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \
- if (theory::TheoryTraits<THEORY>::hasCheck) { \
- reinterpret_cast<theory::TheoryTraits<THEORY>::theory_class*>(d_theoryTable[THEORY])->check(effort); \
- if (!d_theoryOut.d_conflictNode.get().isNull()) { \
- return false; \
- } \
- }
-
- // Do the checking
- try {
- CVC4_FOR_EACH_THEORY
- } catch(const theory::Interrupted&) {
- Debug("theory") << "TheoryEngine::check() => conflict" << std::endl;
- }
-
- return true;
- }
+ bool check(theory::Theory::Effort effort);
/**
* Calls staticLearning() on all active theories, accumulating their
return d_theoryOut.d_conflictNode;
}
- inline void propagate() {
-
- // Definition of the statement that is to be run by every theory
-#ifdef CVC4_FOR_EACH_THEORY_STATEMENT
-#undef CVC4_FOR_EACH_THEORY_STATEMENT
-#endif
-#define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \
- if (theory::TheoryTraits<THEORY>::hasPropagate) { \
- reinterpret_cast<theory::TheoryTraits<THEORY>::theory_class*>(d_theoryTable[THEORY])->propagate(theory::Theory::FULL_EFFORT); \
- }
-
- // Propagate for each theory using the statement above
- CVC4_FOR_EACH_THEORY
- }
+ void propagate();
inline Node getExplanation(TNode node, theory::Theory* theory) {
theory->explain(node);
**/
#include "theory/uf/morgan/theory_uf_morgan.h"
-#include "theory/theory_engine.h"
+#include "theory/valuation.h"
#include "expr/kind.h"
#include "util/congruence_closure.h"
Debug("uf") << "uf: end notifyDecisionLevelZero()" << endl;
}
-Node TheoryUFMorgan::getValue(TNode n, TheoryEngine* engine) {
+Node TheoryUFMorgan::getValue(TNode n, Valuation* valuation) {
NodeManager* nodeManager = NodeManager::currentNM();
switch(n.getKind()) {
case kind::EQUAL: // 2 args
return nodeManager->
- mkConst( engine->getValue(n[0]) == engine->getValue(n[1]) );
+ mkConst( valuation->getValue(n[0]) == valuation->getValue(n[1]) );
default:
Unhandled(n.getKind());
* Overloads Node getValue(TNode n); from theory.h.
* See theory/theory.h for more information about this method.
*/
- Node getValue(TNode n, TheoryEngine* engine);
+ Node getValue(TNode n, Valuation* valuation);
std::string identify() const { return std::string("TheoryUFMorgan"); }
** (http://portal.acm.org/ft_gateway.cfm?id=322198&type=pdf)
** This has been extended to work in a context-dependent way.
** This interacts heavily with the data-structures given in ecdata.h .
- **
**/
#include "cvc4_private.h"
* Overloads Node getValue(TNode n); from theory.h.
* See theory/theory.h for more information about this method.
*/
- Node getValue(TNode n, TheoryEngine* engine) {
+ Node getValue(TNode n, Valuation* valuation) {
Unimplemented("TheoryUFTim doesn't support model generation");
}
--- /dev/null
+/********************* */
+/*! \file valuation.cpp
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief A "valuation" proxy for TheoryEngine
+ **
+ ** Implementation of Valuation class.
+ **/
+
+#include "expr/node.h"
+#include "theory/valuation.h"
+#include "theory/theory_engine.h"
+
+namespace CVC4 {
+namespace theory {
+
+Node Valuation::getValue(TNode n) {
+ return d_engine->getValue(n);
+}
+
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
--- /dev/null
+/********************* */
+/*! \file valuation.h
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief A "valuation" proxy for TheoryEngine
+ **
+ ** A "valuation" proxy for TheoryEngine. This class breaks the dependence
+ ** of theories' getValue() implementations on TheoryEngine. getValue()
+ ** takes a Valuation, which delegates to TheoryEngine.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__VALUATION_H
+#define __CVC4__THEORY__VALUATION_H
+
+#include "expr/node.h"
+
+namespace CVC4 {
+
+class TheoryEngine;
+
+namespace theory {
+
+class Valuation {
+ TheoryEngine* d_engine;
+public:
+ Valuation(TheoryEngine* engine) :
+ d_engine(engine) {
+ }
+
+ Node getValue(TNode n);
+
+};/* class Valuation */
+
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__VALUATION_H */
void preRegisterTerm(TNode n) {}
void propagate(Effort level) {}
void explain(TNode n, Effort level) {}
- Node getValue(TNode n, TheoryEngine* engine) { return Node::null(); }
+ Node getValue(TNode n, Valuation* valuation) { return Node::null(); }
string identify() const { return "DummyTheory"; }
};
#include "theory/theory.h"
#include "theory/theory_engine.h"
+#include "theory/valuation.h"
#include "theory/rewriter.h"
#include "expr/node.h"
#include "expr/node_manager.h"
void check(Theory::Effort) { Unimplemented(); }
void propagate(Theory::Effort) { Unimplemented(); }
void explain(TNode, Theory::Effort) { Unimplemented(); }
- Node getValue(TNode n, TheoryEngine* engine) { return Node::null(); }
+ Node getValue(TNode n, Valuation* valuation) { return Node::null(); }
};/* class FakeTheory */
projects / cvc5.git / commitdiff