Add option for timeout for rewrite candidate check (#2156)

diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml
index be4c66b27398071f1632c258ebe68e41cc7f9d22..ecd4182821b937823cb6f07d2a62b89296080d32 100644 (file)
--- 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 a5a35f89d8863b533a36999ca7077749424c1d24..f9c63f4da056123c1e581f7f62bfda7f00cbf8c2 100644 (file)
--- 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);