summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/expr/node_manager.cpp3
-rw-r--r--src/prop/cnf_stream.cpp50
-rw-r--r--src/prop/cnf_stream.h3
-rw-r--r--src/theory/theory_engine.cpp94
-rw-r--r--src/theory/theory_engine.h15
-rw-r--r--src/theory/uf/theory_uf.cpp12
-rw-r--r--src/theory/uf/theory_uf.h8
7 files changed, 112 insertions, 73 deletions
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index 7c8fb229a..a1b5b771f 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -229,6 +229,9 @@ TypeNode NodeManager::getType(TNode n) throw (TypeCheckingExceptionPrivate) {
case kind::UMINUS:
typeNode = CVC4::theory::arith::ArithOperatorTypeRule::computeType(this, n);
break;
+ case kind::DIVISION:
+ typeNode = CVC4::theory::arith::ArithOperatorTypeRule::computeType(this, n);
+ break;
case kind::CONST_RATIONAL:
typeNode = CVC4::theory::arith::ArithConstantTypeRule::computeType(this, n);
break;
diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp
index 219c25399..350b6f5cf 100644
--- a/src/prop/cnf_stream.cpp
+++ b/src/prop/cnf_stream.cpp
@@ -325,49 +325,6 @@ SatLiteral TseitinCnfStream::handleIte(TNode iteNode) {
return iteLit;
}
-Node TseitinCnfStream::handleNonAtomicNode(TNode node) {
- Debug("cnf") << "handleNonAtomicNode(" << node << ")" << endl;
-
- /* Our main goal here is to tease out any ITE's sitting under a theory operator. */
- Node rewrite;
- NodeManager *nodeManager = NodeManager::currentNM();
- if(nodeManager->getAttribute(node, IteRewriteAttr(), rewrite)) {
- return rewrite.isNull() ? Node(node) : rewrite;
- }
-
- if(node.getKind() == ITE) {
- Assert( node.getNumChildren() == 3 );
- //TODO should this be a skolem?
- Node skolem = nodeManager->mkVar(node.getType());
- Node newAssertion =
- nodeManager->mkNode(
- ITE,
- node[0],
- nodeManager->mkNode(EQUAL, skolem, node[1]),
- nodeManager->mkNode(EQUAL, skolem, node[2]));
- nodeManager->setAttribute(node, IteRewriteAttr(), skolem);
- convertAndAssert(newAssertion, d_assertingLemma);
- return skolem;
- } else {
- std::vector<Node> newChildren;
- bool somethingChanged = false;
- for(TNode::const_iterator it = node.begin(), end = node.end(); it != end; ++it) {
- Node newChild = handleNonAtomicNode(*it);
- somethingChanged |= (newChild != *it);
- newChildren.push_back(newChild);
- }
-
- if(somethingChanged) {
-
- rewrite = nodeManager->mkNode(node.getKind(), newChildren);
- nodeManager->setAttribute(node, IteRewriteAttr(), rewrite);
- return rewrite;
- } else {
- nodeManager->setAttribute(node, IteRewriteAttr(), Node::null());
- return node;
- }
- }
-}
SatLiteral TseitinCnfStream::toCNF(TNode node) {
Debug("cnf") << "toCNF(" << node << ")" << endl;
@@ -395,8 +352,11 @@ SatLiteral TseitinCnfStream::toCNF(TNode node) {
return handleAnd(node);
default:
{
- Node atomic = handleNonAtomicNode(node);
- return isCached(atomic) ? lookupInCache(atomic) : handleAtom(atomic);
+ //TODO make sure this does not contain any boolean substructure
+ return handleAtom(node);
+ //Unreachable();
+ //Node atomic = handleNonAtomicNode(node);
+ //return isCached(atomic) ? lookupInCache(atomic) : handleAtom(atomic);
}
}
}
diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h
index 1ea600322..a574adf23 100644
--- a/src/prop/cnf_stream.h
+++ b/src/prop/cnf_stream.h
@@ -215,9 +215,6 @@ private:
SatLiteral handleAnd(TNode node);
SatLiteral handleOr(TNode node);
- struct IteRewriteTag {};
- typedef expr::Attribute<IteRewriteTag, Node> IteRewriteAttr;
- Node handleNonAtomicNode(TNode node);
/**
* Transforms the node into CNF recursively.
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 5af64c5dd..22b2b2b22 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -28,6 +28,9 @@ namespace theory {
struct PreRegisteredTag {};
typedef expr::Attribute<PreRegisteredTag, bool> PreRegistered;
+struct IteRewriteTag {};
+typedef expr::Attribute<IteRewriteTag, Node> IteRewriteAttr;
+
}/* CVC4::theory namespace */
Node TheoryEngine::preprocess(TNode t) {
@@ -83,6 +86,57 @@ Node TheoryEngine::preprocess(TNode t) {
return top;
}
+ /* Our goal is to tease out any ITE's sitting under a theory operator. */
+Node TheoryEngine::removeITEs(TNode node) {
+ Debug("ite") << "handleNonAtomicNode(" << node << ")" << endl;
+
+ /* The result may be cached already */
+ Node rewrite;
+ NodeManager *nodeManager = NodeManager::currentNM();
+ if(nodeManager->getAttribute(node, theory::IteRewriteAttr(), rewrite)) {
+ return rewrite.isNull() ? Node(node) : rewrite;
+ }
+
+ if(node.getKind() == kind::ITE){
+ if(theoryOf(node[1]) != &d_bool && node[1].getKind() != kind::EQUAL) {
+ Assert( node.getNumChildren() == 3 );
+
+ Debug("ite") << theoryOf(node[1]) << " " << &d_bool <<endl;
+
+ Node skolem = nodeManager->mkVar(node.getType());
+ Node newAssertion =
+ nodeManager->mkNode(
+ kind::ITE,
+ node[0],
+ nodeManager->mkNode(kind::EQUAL, skolem, node[1]),
+ nodeManager->mkNode(kind::EQUAL, skolem, node[2]));
+ nodeManager->setAttribute(node, theory::IteRewriteAttr(), skolem);
+
+ Node preprocessed = preprocess(newAssertion);
+ d_propEngine->assertFormula(preprocessed);
+
+ return skolem;
+ }
+ }
+ std::vector<Node> newChildren;
+ bool somethingChanged = false;
+ for(TNode::const_iterator it = node.begin(), end = node.end(); it != end; ++it) {
+ Node newChild = removeITEs(*it);
+ somethingChanged |= (newChild != *it);
+ newChildren.push_back(newChild);
+ }
+
+ if(somethingChanged) {
+
+ rewrite = nodeManager->mkNode(node.getKind(), newChildren);
+ nodeManager->setAttribute(node, theory::IteRewriteAttr(), rewrite);
+ return rewrite;
+ } else {
+ nodeManager->setAttribute(node, theory::IteRewriteAttr(), Node::null());
+ return node;
+ }
+
+}
Node TheoryEngine::rewrite(TNode in) {
if(inRewriteCache(in)) {
@@ -93,28 +147,10 @@ Node TheoryEngine::rewrite(TNode in) {
return in;
}
- /*
- theory::Theory* thy = theoryOf(in);
- if(thy == NULL) {
- Node out = rewriteBuiltins(in);
- setRewriteCache(in, out);
- return in;
- } else {
- Node out = thy->rewrite(in);
- setRewriteCache(in, out);
- return out;
- }
- */
+ in = removeITEs(in);
// these special cases should go away when theory rewriting comes online
- if(in.getKind() == kind::EQUAL) {
- Assert(in.getNumChildren() == 2);
- if(in[0] == in[1]) {
- Node out = NodeManager::currentNM()->mkConst(true);
- //setRewriteCache(in, out);
- return out;
- }
- } else if(in.getKind() == kind::DISTINCT) {
+ if(in.getKind() == kind::DISTINCT) {
vector<Node> diseqs;
for(TNode::iterator i = in.begin(); i != in.end(); ++i) {
TNode::iterator j = i;
@@ -130,14 +166,24 @@ Node TheoryEngine::rewrite(TNode in) {
: NodeManager::currentNM()->mkNode(CVC4::kind::AND, diseqs);
//setRewriteCache(in, out);
return out;
- } else {
- Node out = rewriteChildren(in);
+ }
+
+ theory::Theory* thy = theoryOf(in);
+ if(thy == NULL) {
+ Node out = rewriteBuiltins(in);
+ //setRewriteCache(in, out);
+ return in;
+ } else if(thy != &d_bool){
+ Node out = thy->rewrite(in);
//setRewriteCache(in, out);
return out;
+ }else{
+ Node out = rewriteChildren(in);
+ setRewriteCache(in, out);
+ return out;
}
- //setRewriteCache(in, in);
- return in;
+ Unreachable();
}
}/* CVC4 namespace */
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 00336a1e3..e9cb56b88 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -136,6 +136,10 @@ class TheoryEngine {
}
NodeBuilder<> b(in.getKind());
+ if(in.getMetaKind() == kind::metakind::PARAMETERIZED){
+ Assert(in.hasOperator());
+ b << in.getOperator();
+ }
for(TNode::iterator c = in.begin(); c != in.end(); ++c) {
b << rewrite(*c);
}
@@ -168,6 +172,8 @@ class TheoryEngine {
}
}
+ Node removeITEs(TNode t);
+
public:
/**
@@ -220,7 +226,14 @@ public:
Assert(k >= 0 && k < kind::LAST_KIND);
if(k == kind::VARIABLE) {
- return &d_uf;
+ TypeNode t = n.getType();
+ if(t.isBoolean()){
+ return &d_bool;
+ }else if(t.isReal()){
+ return &d_arith;
+ }else{
+ return &d_uf;
+ }
//Unimplemented();
} else if(k == kind::EQUAL) {
// if LHS is a VARIABLE, use theoryOf(LHS.getType())
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index 2d7d4e91f..1f09ce81d 100644
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -35,6 +35,18 @@ TheoryUF::TheoryUF(Context* c, OutputChannel& out) :
TheoryUF::~TheoryUF() {
}
+Node TheoryUF::rewrite(TNode n){
+ Debug("uf") << "uf: begin rewrite(" << n << ")" << std::endl;
+ Node ret(n);
+ if(n.getKind() == EQUAL){
+ Assert(n.getNumChildren() == 2);
+ if(n[0] == n[1]) {
+ ret = NodeManager::currentNM()->mkConst(true);
+ }
+ }
+ Debug("uf") << "uf: end rewrite(" << n << ") : " << ret << std::endl;
+ return ret;
+}
void TheoryUF::preRegisterTerm(TNode n) {
Debug("uf") << "uf: begin preRegisterTerm(" << n << ")" << std::endl;
Debug("uf") << "uf: end preRegisterTerm(" << n << ")" << std::endl;
diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h
index 5863a31fc..be08cfee7 100644
--- a/src/theory/uf/theory_uf.h
+++ b/src/theory/uf/theory_uf.h
@@ -119,6 +119,14 @@ public:
*/
void check(Effort level);
+
+ /**
+ * Rewrites a node in the theory of uninterpreted functions.
+ * This is fairly basic and only ensures that atoms that are
+ * unsatisfiable or a valid are rewritten to false or true respectively.
+ */
+ Node rewrite(TNode n);
+
/**
* Propagates theory literals. Currently does nothing.
*
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback