summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/expr/kind_template.h2
-rw-r--r--src/expr/node_builder.h20
-rw-r--r--src/expr/node_manager.h5
-rw-r--r--src/theory/arith/theory_arith.cpp5
-rw-r--r--src/theory/arith/theory_arith.h3
-rwxr-xr-xsrc/theory/mktheorytraits2
-rw-r--r--src/theory/theory_engine.cpp31
-rw-r--r--src/theory/theory_engine.h22
-rw-r--r--src/theory/uf/tim/theory_uf_tim.cpp5
-rw-r--r--test/regress/regress0/uf/Makefile.am4
10 files changed, 78 insertions, 21 deletions
diff --git a/src/expr/kind_template.h b/src/expr/kind_template.h
index 724f7413f..fe1e31a7b 100644
--- a/src/expr/kind_template.h
+++ b/src/expr/kind_template.h
@@ -62,6 +62,8 @@ ${kind_printers}
return out;
}
+#line 66 "${template}"
+
/** Returns true if the given kind is associative. This is used by ExprManager to
* decide whether it's safe to modify big expressions by changing the grouping of
* the arguments. */
diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h
index 252cba43e..156d14299 100644
--- a/src/expr/node_builder.h
+++ b/src/expr/node_builder.h
@@ -946,6 +946,16 @@ expr::NodeValue* NodeBuilder<nchild_thresh>::constructNV() {
kind::metakind::getUpperBoundForKind(getKind()),
getNumChildren());
+#if 0
+ // if the kind is PARAMETERIZED, check that the operator is correctly-kinded
+ Assert(kind::metaKindOf(getKind()) != kind::metakind::PARAMETERIZED ||
+ kind::operatorKindToKind(getOperator().getKind()) == getKind(),
+ "Attempted to construct a parameterized kind `%s' with "
+ "incorrectly-kinded operator `%s'",
+ kind::kindToString(getKind()).c_str(),
+ kind::kindToString(getOperator().getKind()).c_str());
+#endif /* 0 */
+
// Implementation differs depending on whether the NodeValue was
// malloc'ed or not and whether or not it's in the already-been-seen
// NodeManager pool of Nodes. See implementation notes at the top
@@ -1121,6 +1131,16 @@ expr::NodeValue* NodeBuilder<nchild_thresh>::constructNV() const {
kind::metakind::getUpperBoundForKind(getKind()),
getNumChildren());
+#if 0
+ // if the kind is PARAMETERIZED, check that the operator is correctly-kinded
+ Assert(kind::metaKindOf(getKind()) != kind::metakind::PARAMETERIZED ||
+ kind::operatorKindToKind(getOperator().getKind()) == getKind(),
+ "Attempted to construct a parameterized kind `%s' with "
+ "incorrectly-kinded operator `%s'",
+ kind::kindToString(getKind()).c_str(),
+ kind::kindToString(getOperator().getKind()).c_str());
+#endif /* 0 */
+
// Implementation differs depending on whether the NodeValue was
// malloc'ed or not and whether or not it's in the already-been-seen
// NodeManager pool of Nodes. See implementation notes at the top
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 54266db13..5c3e4731b 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -826,10 +826,11 @@ inline TypeNode NodeManager::mkTupleType(const std::vector<TypeNode>& types) {
Assert(types.size() >= 2);
std::vector<TypeNode> typeNodes;
for (unsigned i = 0; i < types.size(); ++ i) {
- /* FIXME when congruence closure no longer abuses tuples
+ /* FIXME when congruence closure no longer abuses tuples */
+#if 0
CheckArgument(!types[i].isFunctionLike(), types,
"cannot put function-like types in tuples");
- */
+#endif /* 0 */
typeNodes.push_back(types[i]);
}
return mkTypeNode(kind::TUPLE_TYPE, typeNodes);
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 8e8064b7f..a4c9f3ce0 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -292,13 +292,8 @@ void TheoryArith::setupInitialValue(ArithVar x){
d_partialModel.setAssignment(x,assignment);
}
Debug("arithgc") << "setupVariable("<<x<<")"<<std::endl;
-};
-
-void TheoryArith::registerTerm(TNode tn){
- Debug("arith") << "registerTerm(" << tn << ")" << endl;
}
-
ArithVar TheoryArith::determineLeftVariable(TNode assertion, Kind simpleKind){
TNode left = getSide<true>(assertion, simpleKind);
diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h
index dc5cd2050..241ef8075 100644
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -140,9 +140,6 @@ public:
*/
void preRegisterTerm(TNode n);
- /** CD setup for a node. Currently does nothing. */
- void registerTerm(TNode n);
-
void check(Effort e);
void propagate(Effort e);
void explain(TNode n);
diff --git a/src/theory/mktheorytraits b/src/theory/mktheorytraits
index 45c108b72..538ffb25f 100755
--- a/src/theory/mktheorytraits
+++ b/src/theory/mktheorytraits
@@ -133,7 +133,7 @@ struct TheoryTraits<${theory_id}> {
static const bool hasRegisterTerm = ${theory_has_registerTerm};
static const bool hasNotifyRestart = ${theory_has_notifyRestart};
static const bool hasPresolve = ${theory_has_presolve};
-};
+};/* struct TheoryTraits<${theory_id}> */
"
# warnings about theory content and properties
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index cf105803c..db22d8981 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -68,7 +68,9 @@ void TheoryEngine::EngineOutputChannel::newFact(TNode fact) {
d_engine->getSharedTermManager()->addEq(fact);
}
- if(Options::current()->theoryRegistration && !fact.getAttribute(RegisteredAttr())) {
+ if(Options::current()->theoryRegistration &&
+ !fact.getAttribute(RegisteredAttr()) &&
+ d_engine->d_needRegistration) {
list<TNode> toReg;
toReg.push_back(fact);
@@ -137,6 +139,7 @@ TheoryEngine::TheoryEngine(context::Context* ctxt) :
d_propEngine(NULL),
d_context(ctxt),
d_activeTheories(0),
+ d_needRegistration(false),
d_theoryOut(this, ctxt),
d_hasShutDown(false),
d_incomplete(ctxt, false),
@@ -272,7 +275,7 @@ bool TheoryEngine::check(theory::Theory::Effort effort) {
// Do the checking
try {
- CVC4_FOR_EACH_THEORY
+ CVC4_FOR_EACH_THEORY;
} catch(const theory::Interrupted&) {
Debug("theory") << "TheoryEngine::check() => conflict" << std::endl;
}
@@ -291,7 +294,7 @@ void TheoryEngine::propagate() {
}
// Propagate for each theory using the statement above
- CVC4_FOR_EACH_THEORY
+ CVC4_FOR_EACH_THEORY;
}
/* Our goal is to tease out any ITE's sitting under a theory operator. */
@@ -389,7 +392,7 @@ bool TheoryEngine::presolve() {
}
// Presolve for each theory using the statement above
- CVC4_FOR_EACH_THEORY
+ CVC4_FOR_EACH_THEORY;
} catch(const theory::Interrupted&) {
Debug("theory") << "TheoryEngine::presolve() => interrupted" << endl;
}
@@ -409,7 +412,7 @@ void TheoryEngine::notifyRestart() {
}
// notify each theory using the statement above
- CVC4_FOR_EACH_THEORY
+ CVC4_FOR_EACH_THEORY;
}
void TheoryEngine::staticLearning(TNode in, NodeBuilder<>& learned) {
@@ -429,7 +432,23 @@ void TheoryEngine::staticLearning(TNode in, NodeBuilder<>& learned) {
}
// static learning for each theory using the statement above
- CVC4_FOR_EACH_THEORY
+ CVC4_FOR_EACH_THEORY;
+}
+
+bool TheoryEngine::hasRegisterTerm(TheoryId th) const {
+ switch(th) {
+ // 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) \
+ case THEORY: \
+ return theory::TheoryTraits<THEORY>::hasRegisterTerm;
+
+ CVC4_FOR_EACH_THEORY
+ default:
+ Unhandled(th);
+ }
}
Node TheoryEngine::simplify(TNode in, theory::Substitutions& outSubstitutions) {
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 2dd3db863..852eea0c4 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -74,6 +74,13 @@ class TheoryEngine {
size_t d_activeTheories;
/**
+ * Need the registration infrastructure when theory sharing is on
+ * (>=2 active theories) or when the sole active theory has
+ * requested it.
+ */
+ bool d_needRegistration;
+
+ /**
* The type of the simplification cache.
*/
typedef Cache<Node, std::pair<Node, theory::Substitutions>, NodeHashFunction> SimplifyCache;
@@ -194,11 +201,22 @@ class TheoryEngine {
void markActive(theory::TheoryId th) {
if(!d_theoryIsActive[th]) {
d_theoryIsActive[th] = true;
- ++d_activeTheories;
- Notice() << "Theory " << th << " has been activated." << std::endl;
+ if(th != theory::THEORY_BUILTIN && th != theory::THEORY_BOOL) {
+ if(++d_activeTheories == 1) {
+ // theory requests registration
+ d_needRegistration = hasRegisterTerm(th);
+ } else {
+ // need it for sharing
+ d_needRegistration = true;
+ }
+ }
+ Notice() << "Theory " << th << " has been activated (registration is "
+ << (d_needRegistration ? "on" : "off") << ")." << std::endl;
}
}
+ bool hasRegisterTerm(theory::TheoryId th) const;
+
public:
/** The logic of the problem */
std::string d_logic;
diff --git a/src/theory/uf/tim/theory_uf_tim.cpp b/src/theory/uf/tim/theory_uf_tim.cpp
index ef1704426..ae37dfe99 100644
--- a/src/theory/uf/tim/theory_uf_tim.cpp
+++ b/src/theory/uf/tim/theory_uf_tim.cpp
@@ -34,6 +34,11 @@ TheoryUFTim::TheoryUFTim(Context* c, OutputChannel& out, Valuation valuation) :
d_currentPendingIdx(c,0),
d_disequality(c),
d_registered(c) {
+ Warning() << "NOTE:" << std::endl
+ << "NOTE: currently the 'Tim' UF solver is broken," << std::endl
+ << "NOTE: since its registerTerm() function is never" << std::endl
+ << "NOTE: called." << std::endl
+ << "NOTE:" << std::endl;
}
TheoryUFTim::~TheoryUFTim() {
diff --git a/test/regress/regress0/uf/Makefile.am b/test/regress/regress0/uf/Makefile.am
index e288a01d2..01eaee999 100644
--- a/test/regress/regress0/uf/Makefile.am
+++ b/test/regress/regress0/uf/Makefile.am
@@ -12,7 +12,6 @@ TESTS = \
euf_simp06.smt \
euf_simp08.smt \
euf_simp09.smt \
- euf_simp09.tim.smt \
euf_simp10.smt \
euf_simp11.smt \
euf_simp12.smt \
@@ -30,7 +29,8 @@ TESTS = \
simple.03.cvc \
simple.04.cvc
-EXTRA_DIST = $(TESTS)
+EXTRA_DIST = $(TESTS) \
+ euf_simp09.tim.smt
#if CVC4_BUILD_PROFILE_COMPETITION
#else
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback