Logic exception when using solution filtering for non-Boolean grammars (#8225)

Fixes cvc5/cvc5-projects#464.

diff --git a/src/theory/quantifiers/solution_filter.cpp b/src/theory/quantifiers/solution_filter.cpp
index aead6784f8760d3342083aace9b4477829d3d322..364a3c812057e2e8c8d812f38addf737e016dda1 100644 (file)
--- a/src/theory/quantifiers/solution_filter.cpp
+++ b/src/theory/quantifiers/solution_filter.cpp
@@ -20,6 +20,7 @@
 #include "options/base_options.h"
 #include "options/quantifiers_options.h"
 #include "smt/env.h"
+#include "smt/logic_exception.h"
 #include "util/random.h"
 
 using namespace cvc5::kind;
@@ -48,7 +49,10 @@ bool SolutionFilterStrength::addTerm(Node n, std::ostream& out)
   if (!n.getType().isBoolean())
   {
     // currently, should not register non-Boolean terms here
-    Assert(false);
+    std::stringstream ss;
+    ss << "SyGuS solution filtering requires the grammar to "
+          "generate Boolean terms only";
+    throw LogicException(ss.str());
     return true;
   }
   Node basen = d_isStrong ? n : n.negate();

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 6b941c63d8dfcdada9772eaf27ac9631cb7c1513..07883f373e6b6fe058a47e5c37ff7b8de5e86c0b 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1420,6 +1420,7 @@ set(regress_0_tests
   regress0/sygus/print-debug.sy
   regress0/sygus/print-define-fun.sy
   regress0/sygus/print-grammar.sy
+  regress0/sygus/proj-issue464-rr-option.smt2
   regress0/sygus/real-si-all.sy
   regress0/sygus/setFeature.sy
   regress0/sygus/strings-unconstrained.sy

diff --git a/test/regress/regress0/sygus/proj-issue464-rr-option.smt2 b/test/regress/regress0/sygus/proj-issue464-rr-option.smt2
new file mode 100644 (file)
index 0000000..e8a61fd
--- /dev/null
+++ b/test/regress/regress0/sygus/proj-issue464-rr-option.smt2
@@ -0,0 +1,13 @@
+; SCRUBBER: grep -v -E '\(define-fun'
+; EXPECT: (error "SyGuS solution filtering requires the grammar to generate Boolean terms only")
+; EXIT: 1
+(set-logic ALL)
+(set-option :global-declarations true)
+(set-option :sygus-rr-synth-input true)
+(set-option :sygus-filter-sol weak)
+(declare-sort _u0 0)
+(declare-const _x6 Bool)
+(declare-const _x10 _u0)
+(declare-const _x12 _u0)
+(assert (= (distinct _x12 _x10) _x6))
+(check-sat)