From 7d9d562bb560cb4b83ffaaf94918f834916dad2f Mon Sep 17 00:00:00 2001 From: Tim King Date: Fri, 28 May 2010 20:17:48 +0000 Subject: [PATCH] Moving the ITE removal from CnfStream to TheoryEngine, which is a bit closer to its final destination. Added a basic rewriter to TheoryUF. (x=x rewrites to true.) Added DIVISION to src/expr/node_manager.cpp's getType. Fixed the theory returned for variables in theoryOf() for bool and arith. Fixed TheoryEngine rewrite children to properly handle APPLY_UFs. Removed the special case for equality in TheoryEngine rewrite. A few tests are currently broken due to deallocation errors. Morgan and I will try to commit a fix to this in a little bit. --- src/expr/node_manager.cpp | 3 ++ src/prop/cnf_stream.cpp | 50 ++----------------- src/prop/cnf_stream.h | 3 -- src/theory/theory_engine.cpp | 94 +++++++++++++++++++++++++++--------- src/theory/theory_engine.h | 15 +++++- src/theory/uf/theory_uf.cpp | 12 +++++ src/theory/uf/theory_uf.h | 8 +++ 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 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 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 PreRegistered; +struct IteRewriteTag {}; +typedef expr::Attribute IteRewriteAttr; + }/* CVC4::theory namespace */ Node TheoryEngine::preprocess(TNode t) { @@ -82,6 +85,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 <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 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) { @@ -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 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. * -- 2.30.2