From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Sat, 14 Jul 2018 08:45:58 +0000 (-0700)
Subject: exportTo only if needed for --sygus-rr-synth-check (#2168)
X-Git-Tag: cvc5-1.0.0~4894
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=292b2c5712ce31282ac3ec564f268ee7f0aa3506;p=cvc5.git

exportTo only if needed for --sygus-rr-synth-check (#2168)
---

diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index 33b06ead4..457e54d9b 100644
--- a/src/expr/expr_manager_template.cpp
+++ b/src/expr/expr_manager_template.cpp
@@ -1023,6 +1023,16 @@ TypeNode exportTypeInternal(TypeNode n, NodeManager* from, NodeManager* to, Expr
   } else if(n.getKind() == kind::BITVECTOR_TYPE) {
     return to->mkBitVectorType(n.getConst<BitVectorSize>());
   }
+  else if (n.getKind() == kind::FLOATINGPOINT_TYPE)
+  {
+    return to->mkFloatingPointType(n.getConst<FloatingPointSize>());
+  }
+  else if (n.getNumChildren() == 0)
+  {
+    std::stringstream msg;
+    msg << "export of type " << n << " not supported";
+    throw ExportUnsupportedException(msg.str().c_str());
+  }
   Type from_t = from->toType(n);
   Type& to_t = vmap.d_typeMap[from_t];
   if(! to_t.isNull()) {
diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp
index 1344935af..3a0d31b2d 100644
--- a/src/expr/expr_template.cpp
+++ b/src/expr/expr_template.cpp
@@ -248,8 +248,11 @@ public:
         children.push_back(exportInternal(*i));
       }
       if(Debug.isOn("export")) {
-        ExprManagerScope ems(*to);
         Debug("export") << "children for export from " << n << std::endl;
+
+        // `n` belongs to the `from` ExprManager, so begin ExprManagerScope
+        // after printing `n`
+        ExprManagerScope ems(*to);
         for(std::vector<Node>::iterator i = children.begin(), i_end = children.end(); i != i_end; ++i) {
           Debug("export") << "  child: " << *i << std::endl;
         }
diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp
index b3e5c5a83..d6cf12d41 100644
--- a/src/expr/type_node.cpp
+++ b/src/expr/type_node.cpp
@@ -342,6 +342,7 @@ TypeNode TypeNode::commonTypeNode(TypeNode t0, TypeNode t1, bool isLeast) {
   // t1.getKind() == kind::TYPE_CONSTANT
   switch(t0.getKind()) {
   case kind::BITVECTOR_TYPE:
+  case kind::FLOATINGPOINT_TYPE:
   case kind::SORT_TYPE:
   case kind::CONSTRUCTOR_TYPE:
   case kind::SELECTOR_TYPE:
diff --git a/src/theory/quantifiers/candidate_rewrite_database.cpp b/src/theory/quantifiers/candidate_rewrite_database.cpp
index f9c63f4da..3df3717c3 100644
--- a/src/theory/quantifiers/candidate_rewrite_database.cpp
+++ b/src/theory/quantifiers/candidate_rewrite_database.cpp
@@ -112,16 +112,7 @@ bool CandidateRewriteDatabase::addTerm(Node sol,
       // verify it if applicable
       if (options::sygusRewSynthCheck())
       {
-        // Notice we don't set produce-models. rrChecker takes the same
-        // options as the SmtEngine we belong to, where we ensure that
-        // produce-models is set.
         NodeManager* nm = NodeManager::currentNM();
-        Options opts;
-        ExprManager em(nm->getOptions());
-        ExprManagerMapCollection varMap;
-        SmtEngine rrChecker(&em);
-        rrChecker.setTimeLimit(options::sygusRewSynthCheckTimeout(), true);
-        rrChecker.setLogic(smt::currentSmtEngine()->getLogicInfo());
 
         Node crr = solbr.eqNode(eq_solr).negate();
         Trace("rr-check") << "Check candidate rewrite : " << crr << std::endl;
@@ -151,9 +142,48 @@ bool CandidateRewriteDatabase::addTerm(Node sol,
           }
           crr = crr.substitute(fvs.begin(), fvs.end(), sks.begin(), sks.end());
         }
-        Expr eccr = crr.toExpr().exportTo(&em, varMap);
-        rrChecker.assertFormula(eccr);
-        Result r = rrChecker.checkSat();
+
+        // Notice we don't set produce-models. rrChecker takes the same
+        // options as the SmtEngine we belong to, where we ensure that
+        // produce-models is set.
+        bool needExport = true;
+        ExprManagerMapCollection varMap;
+        ExprManager em(nm->getOptions());
+        std::unique_ptr<SmtEngine> rrChecker;
+        Result r;
+        if (options::sygusRewSynthCheckTimeout.wasSetByUser())
+        {
+          // To support a separate timeout for the subsolver, we need to create
+          // a separate ExprManager with its own options. This requires that
+          // the expressions sent to the subsolver can be exported from on
+          // ExprManager to another. If the export fails, we throw an
+          // OptionException.
+          try
+          {
+            rrChecker.reset(new SmtEngine(&em));
+            rrChecker->setTimeLimit(options::sygusRewSynthCheckTimeout(), true);
+            rrChecker->setLogic(smt::currentSmtEngine()->getLogicInfo());
+            Expr eccr = crr.toExpr().exportTo(&em, varMap);
+            rrChecker->assertFormula(eccr);
+            r = rrChecker->checkSat();
+          }
+          catch (const CVC4::ExportUnsupportedException& e)
+          {
+            std::stringstream msg;
+            msg << "Unable to export " << crr
+                << " but exporting expressions is required for "
+                   "--sygus-rr-synth-check-timeout.";
+            throw OptionException(msg.str());
+          }
+        }
+        else
+        {
+          needExport = false;
+          rrChecker.reset(new SmtEngine(nm->toExprManager()));
+          rrChecker->assertFormula(crr.toExpr());
+          r = rrChecker->checkSat();
+        }
+
         Trace("rr-check") << "...result : " << r << std::endl;
         if (r.asSatisfiabilityResult().isSat() == Result::SAT)
         {
@@ -185,9 +215,16 @@ bool CandidateRewriteDatabase::addTerm(Node sol,
             if (val.isNull())
             {
               Assert(!refv.isNull() && refv.getKind() != BOUND_VARIABLE);
-              Expr erefv = refv.toExpr().exportTo(&em, varMap);
-              val = Node::fromExpr(rrChecker.getValue(erefv).exportTo(
-                  nm->toExprManager(), varMap));
+              if (needExport)
+              {
+                Expr erefv = refv.toExpr().exportTo(&em, varMap);
+                val = Node::fromExpr(rrChecker->getValue(erefv).exportTo(
+                    nm->toExprManager(), varMap));
+              }
+              else
+              {
+                val = Node::fromExpr(rrChecker->getValue(refv.toExpr()));
+              }
             }
             Trace("rr-check") << "  " << v << " -> " << val << std::endl;
             pt.push_back(val);