From 1e331468c0bc5ad20f5b3e0e74e6482670c6227a Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Fri, 6 Jul 2018 04:03:58 -0700 Subject: [PATCH] Add option for timeout for rewrite candidate check (#2156) --- src/options/quantifiers_options.toml | 7 +++++++ .../quantifiers/candidate_rewrite_database.cpp | 14 +++++++++++--- 2 files changed, 18 insertions(+), 3 deletions(-) diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml index be4c66b27..ecd418282 100644 --- a/src/options/quantifiers_options.toml +++ b/src/options/quantifiers_options.toml @@ -1218,6 +1218,13 @@ header = "options/quantifiers_options.h" default = "false" help = "use satisfiability check to verify correctness of candidate rewrites" +[[option]] + name = "sygusRewSynthCheckTimeout" + category = "regular" + long = "sygus-rr-synth-check-timeout" + type = "unsigned long" + help = "timeout (in milliseconds) for the satisfiability check to verify correctness of candidate rewrites" + # CEGQI applied to general quantified formulas [[option]] diff --git a/src/theory/quantifiers/candidate_rewrite_database.cpp b/src/theory/quantifiers/candidate_rewrite_database.cpp index a5a35f89d..f9c63f4da 100644 --- a/src/theory/quantifiers/candidate_rewrite_database.cpp +++ b/src/theory/quantifiers/candidate_rewrite_database.cpp @@ -116,8 +116,13 @@ bool CandidateRewriteDatabase::addTerm(Node sol, // options as the SmtEngine we belong to, where we ensure that // produce-models is set. NodeManager* nm = NodeManager::currentNM(); - SmtEngine rrChecker(nm->toExprManager()); + 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; // quantify over the free variables in crr @@ -146,7 +151,8 @@ bool CandidateRewriteDatabase::addTerm(Node sol, } crr = crr.substitute(fvs.begin(), fvs.end(), sks.begin(), sks.end()); } - rrChecker.assertFormula(crr.toExpr()); + Expr eccr = crr.toExpr().exportTo(&em, varMap); + rrChecker.assertFormula(eccr); Result r = rrChecker.checkSat(); Trace("rr-check") << "...result : " << r << std::endl; if (r.asSatisfiabilityResult().isSat() == Result::SAT) @@ -179,7 +185,9 @@ bool CandidateRewriteDatabase::addTerm(Node sol, if (val.isNull()) { Assert(!refv.isNull() && refv.getKind() != BOUND_VARIABLE); - val = Node::fromExpr(rrChecker.getValue(refv.toExpr())); + Expr erefv = refv.toExpr().exportTo(&em, varMap); + val = Node::fromExpr(rrChecker.getValue(erefv).exportTo( + nm->toExprManager(), varMap)); } Trace("rr-check") << " " << v << " -> " << val << std::endl; pt.push_back(val); -- 2.30.2