From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Fri, 4 Mar 2022 19:12:52 +0000 (-0600)
Subject: Logic exception when using solution filtering for non-Boolean grammars (#8225)
X-Git-Tag: cvc5-1.0.0~324
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=ddf2ec6fbf35c8174c6d63a6de3a4993872019c9;p=cvc5.git

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 aead6784f..364a3c812 100644
--- 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 6b941c63d..07883f373 100644
--- 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
index 000000000..e8a61fdf4
--- /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)