diff options
| -rw-r--r-- | src/expr/expr_manager_template.cpp | 10 | ||||
| -rw-r--r-- | src/expr/expr_template.cpp | 5 | ||||
| -rw-r--r-- | src/expr/type_node.cpp | 1 | ||||
| -rw-r--r-- | src/theory/quantifiers/candidate_rewrite_database.cpp | 67 |
4 files changed, 67 insertions, 16 deletions
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); |