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 3be0a607bb8319c19a01a267a41102a1949a75bd..878ee0ac1420d114aec4db1cb9b0604f228c18f6 100644 (file)
--- 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 a1470c3056997cc3ab1fd5fecd47be469bce8c53..1308c7d64423bfa59f0b0432393e3e16b32c0b59 100644 (file)
--- 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)
   {