From: Abdalrhman Mohamed <32971963+abdoo8080@users.noreply.github.com>
Date: Tue, 22 Mar 2022 17:01:13 +0000 (-0500)
Subject: Add a timeout option for verification of synthesized terms. (#8359)
X-Git-Tag: cvc5-1.0.0~211
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=edc8091c268eb67eac1f963383de309d581e4951;p=cvc5.git

Add a timeout option for verification of synthesized terms. (#8359)

This PR adds an option to timeout on the verification check for the terms enumerated by the Sygus solver.
---

diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml
index 3be0a607b..878ee0ac1 100644
--- a/src/options/quantifiers_options.toml
+++ b/src/options/quantifiers_options.toml
@@ -1319,6 +1319,14 @@ name   = "Quantifiers"
   default    = "3"
   help       = "maximum number of instantiation rounds for sygus verification calls (-1 == no limit, default is 3)"
 
+[[option]]
+  name       = "sygusVerifyTimeout"
+  category   = "regular"
+  long       = "sygus-verify-timeout=N"
+  type       = "uint64_t"
+  default    = "0"
+  help       = "timeout (in milliseconds) for verifying satisfiability of synthesized terms"
+
 # Internal uses of sygus
 
 [[option]]
diff --git a/src/theory/quantifiers/sygus/synth_verify.cpp b/src/theory/quantifiers/sygus/synth_verify.cpp
index a1470c305..1308c7d64 100644
--- a/src/theory/quantifiers/sygus/synth_verify.cpp
+++ b/src/theory/quantifiers/sygus/synth_verify.cpp
@@ -110,7 +110,13 @@ Result SynthVerify::verify(Node query,
   }
   Trace("sygus-engine") << "  *** Verify with subcall..." << std::endl;
   query = rewrite(query);
-  Result r = checkWithSubsolver(query, vars, mvs, d_subOptions, d_subLogicInfo);
+  Result r = checkWithSubsolver(query,
+                                vars,
+                                mvs,
+                                d_subOptions,
+                                d_subLogicInfo,
+                                options().quantifiers.sygusVerifyTimeout != 0,
+                                options().quantifiers.sygusVerifyTimeout);
   Trace("sygus-engine") << "  ...got " << r << std::endl;
   if (r.getStatus() == Result::SAT)
   {