diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-06-27 14:12:17 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-06-27 14:12:17 -0500 |
commit | d6c7967cfc7a9f8530f0de50f12f99bfc5f93da7 (patch) | |
tree | 2741c23c2cc42c065dc2aa573e0983e8f10823c1 /src/theory/quantifiers/dynamic_rewrite.cpp | |
parent | a236ade3242599d4916fd9ee676c2c68c7c004b1 (diff) |
Synthesize candidate-rewrites from standard inputs (#1918)
Diffstat (limited to 'src/theory/quantifiers/dynamic_rewrite.cpp')
-rw-r--r-- | src/theory/quantifiers/dynamic_rewrite.cpp | 30 |
1 files changed, 27 insertions, 3 deletions
diff --git a/src/theory/quantifiers/dynamic_rewrite.cpp b/src/theory/quantifiers/dynamic_rewrite.cpp index 352d6892f..ef1cb3a9d 100644 --- a/src/theory/quantifiers/dynamic_rewrite.cpp +++ b/src/theory/quantifiers/dynamic_rewrite.cpp @@ -23,9 +23,9 @@ namespace CVC4 { namespace theory { namespace quantifiers { -DynamicRewriter::DynamicRewriter(const std::string& name, QuantifiersEngine* qe) - : d_equalityEngine(qe->getUserContext(), "DynamicRewriter::" + name, true), - d_rewrites(qe->getUserContext()) +DynamicRewriter::DynamicRewriter(const std::string& name, + context::UserContext* u) + : d_equalityEngine(u, "DynamicRewriter::" + name, true), d_rewrites(u) { d_equalityEngine.addFunctionKind(kind::APPLY_UF); } @@ -42,6 +42,11 @@ void DynamicRewriter::addRewrite(Node a, Node b) // add to the equality engine Node ai = toInternal(a); Node bi = toInternal(b); + if (ai.isNull() || bi.isNull()) + { + Trace("dyn-rewrite") << "...not internalizable." << std::endl; + return; + } Trace("dyn-rewrite-debug") << "Internal : " << ai << " " << bi << std::endl; Trace("dyn-rewrite-debug") << "assert eq..." << std::endl; @@ -58,11 +63,19 @@ bool DynamicRewriter::areEqual(Node a, Node b) { return true; } + Trace("dyn-rewrite-debug") << "areEqual? : " << a << " " << b << std::endl; // add to the equality engine Node ai = toInternal(a); Node bi = toInternal(b); + if (ai.isNull() || bi.isNull()) + { + Trace("dyn-rewrite") << "...not internalizable." << std::endl; + return false; + } + Trace("dyn-rewrite-debug") << "internal : " << ai << " " << bi << std::endl; d_equalityEngine.addTerm(ai); d_equalityEngine.addTerm(bi); + Trace("dyn-rewrite-debug") << "...added terms" << std::endl; return d_equalityEngine.areEqual(ai, bi); } @@ -84,6 +97,12 @@ Node DynamicRewriter::toInternal(Node a) if (a.getKind() != APPLY_UF) { op = d_ois_trie[op].getSymbol(a); + // if this term involves an argument that is not of first class type, + // we cannot reason about it. This includes operators like str.in-re. + if (op.isNull()) + { + return Node::null(); + } } children.push_back(op); } @@ -120,6 +139,11 @@ Node DynamicRewriter::OpInternalSymTrie::getSymbol(Node n) OpInternalSymTrie* curr = this; for (unsigned i = 0, size = ctypes.size(); i < size; i++) { + // cannot handle certain types (e.g. regular expressions or functions) + if (!ctypes[i].isFirstClass()) + { + return Node::null(); + } curr = &(curr->d_children[ctypes[i]]); } if (!curr->d_sym.isNull()) |