Synthesize candidate-rewrites from standard inputs (#1918)

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())