Warn about infeasible SyGuS conjectures (#6345)

diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
index 47ddaa0d296f0556851d0e609636464c23bef1bb..f96e1e5793b15ad049d008bcc1032157497e4654 100644 (file)
--- a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
+++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
@@ -233,8 +233,13 @@ bool CegSingleInv::solve()
   siSmt->assertFormula(siq);
   Result r = siSmt->checkSat();
   Trace("sygus-si") << "Result: " << r << std::endl;
-  if (r.asSatisfiabilityResult().isSat() != Result::UNSAT)
+  Result::Sat res = r.asSatisfiabilityResult().isSat();
+  if (res != Result::UNSAT)
   {
+    Warning() << "Warning : the single invocation solver determined the SyGuS "
+                 "conjecture"
+              << (res == Result::SAT ? " is" : " may be") << " infeasible"
+              << std::endl;
     // conjecture is infeasible or unknown
     return false;
   }

diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp
index e5dadcb7cb49975a7aa89b72f69e024c162ffcda..0eb96e2775aff64f25a90333d168dc8b012b4b33 100644 (file)
--- a/src/theory/quantifiers/sygus/synth_conjecture.cpp
+++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp
@@ -284,6 +284,8 @@ bool SynthConjecture::needsCheck()
     if (!value)
     {
       Trace("sygus-engine-debug") << "Conjecture is infeasible." << std::endl;
+      Warning() << "Warning : the SyGuS conjecture may be infeasible"
+                << std::endl;
       return false;
     }
     else

diff --git a/test/regress/regress0/sygus/pbe-pred-contra.sy b/test/regress/regress0/sygus/pbe-pred-contra.sy
index 5bd6ebae4b05de3492a5554af5cb910e9a154272..927d1bf0ef998fae31d4d5e3932cbabf454254d8 100644 (file)
--- a/test/regress/regress0/sygus/pbe-pred-contra.sy
+++ b/test/regress/regress0/sygus/pbe-pred-contra.sy
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --lang=sygus2 --sygus-si=none --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --sygus-si=none --sygus-out=status -q
 ; EXPECT: unknown
 (set-logic LIA)
 (synth-fun P ((x Int)) Bool)

diff --git a/test/regress/regress0/sygus/univ_3-long-repeat-conflict.sy b/test/regress/regress0/sygus/univ_3-long-repeat-conflict.sy
index b9bd8e8157424c8402349b01c980412de2713c6c..abcccd2ab22f500c0d0db9a50aaacb7d84a2e5bb 100644 (file)
--- a/test/regress/regress0/sygus/univ_3-long-repeat-conflict.sy
+++ b/test/regress/regress0/sygus/univ_3-long-repeat-conflict.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unknown
-; COMMAND-LINE: --lang=sygus2 --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --sygus-out=status -q
 (set-logic SLIA)
 
 (synth-fun f ((col1 String) (col2 String)) String

diff --git a/test/regress/regress1/issue3970-nl-ext-purify.smt2 b/test/regress/regress1/issue3970-nl-ext-purify.smt2
index 5fbddf13d15f56134877919ee3a40d59262b7a9f..c19884a632b4c13566ddce3558de0f0d2d9afce0 100644 (file)
--- a/test/regress/regress1/issue3970-nl-ext-purify.smt2
+++ b/test/regress/regress1/issue3970-nl-ext-purify.smt2
@@ -1,3 +1,5 @@
+; COMMAND-LINE: -q
+; EXPECT: unsat
 (set-logic QF_UFNRA)
 (set-option :nl-ext-purify true)
 (set-option :sygus-inference true)

diff --git a/test/regress/regress1/sygus/issue3201.smt2 b/test/regress/regress1/sygus/issue3201.smt2
index 99a555010f960315628f0f0c3f3a4574a20e2348..f9df0e78203c2fbf17d47dd6472387b34ad7f09e 100644 (file)
--- a/test/regress/regress1/sygus/issue3201.smt2
+++ b/test/regress/regress1/sygus/issue3201.smt2
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --sygus-inference
+; COMMAND-LINE: --sygus-inference -q
 (set-logic ALL)
 (declare-fun v () Bool)
 (assert false)

diff --git a/test/regress/regress1/sygus/issue3247.smt2 b/test/regress/regress1/sygus/issue3247.smt2
index 6784b8797423136eea0c623db438505a7b58fe04..a02fbc5ce0e4efb6d1634e0007122f7b92855162 100644 (file)
--- a/test/regress/regress1/sygus/issue3247.smt2
+++ b/test/regress/regress1/sygus/issue3247.smt2
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --sygus-inference --strings-exp
+; COMMAND-LINE: --sygus-inference --strings-exp -q
 (set-logic ALL)
 (declare-fun a () String) 
 (declare-fun b () String) 

diff --git a/test/regress/regress1/sygus/issue3649.sy b/test/regress/regress1/sygus/issue3649.sy
index b650c4ca6e463fd014361a1208869236964b7d21..0f7fc668caab91f6d1227ce337904c6584c2ea7e 100644 (file)
--- a/test/regress/regress1/sygus/issue3649.sy
+++ b/test/regress/regress1/sygus/issue3649.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unknown
-; COMMAND-LINE: --lang=sygus2 --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --sygus-out=status -q
 (set-logic ALL)
 (synth-fun inv-fn ((i Int) (x (Array Int Int)) (c Int)) Bool)
 

diff --git a/test/regress/regress1/sygus/issue4009-qep.smt2 b/test/regress/regress1/sygus/issue4009-qep.smt2
index cc79954c4feb0fdc4e576bcd33696e742a35262a..c2cae2ca2c8420e47f912a00b9fb3334bc8c1cb7 100644 (file)
--- a/test/regress/regress1/sygus/issue4009-qep.smt2
+++ b/test/regress/regress1/sygus/issue4009-qep.smt2
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --sygus-inference --sygus-qe-preproc --no-check-unsat-cores
+; COMMAND-LINE: --sygus-inference --sygus-qe-preproc --no-check-unsat-cores -q
 (set-logic ALL)
 (declare-fun a () Real)
 (declare-fun b () Real)

diff --git a/test/regress/regress1/sygus/issue4083-var-shadow.smt2 b/test/regress/regress1/sygus/issue4083-var-shadow.smt2
index bb943486054f70b480a88a49e45abf9b6db09f7f..91b77bfaaa473ea54498768d9aa016af26a4cdb7 100644 (file)
--- a/test/regress/regress1/sygus/issue4083-var-shadow.smt2
+++ b/test/regress/regress1/sygus/issue4083-var-shadow.smt2
@@ -1,3 +1,5 @@
+; COMMAND-LINE: -q
+; EXPECT: unsat
 (set-logic ALL)
 (set-option :miniscope-quant true)
 (set-option :sygus-inference true)