Require ITE branches to be first class types (#7508)

Fixes cvc5/cvc5-projects#316.

diff --git a/src/theory/booleans/theory_bool.cpp b/src/theory/booleans/theory_bool.cpp
index 33bb820b4ef10a3985591ee4db8eb52cc4cece01..1327d1131bad89d0855ba841e454575b9686648b 100644 (file)
--- a/src/theory/booleans/theory_bool.cpp
+++ b/src/theory/booleans/theory_bool.cpp
@@ -19,6 +19,7 @@
 #include <vector>
 
 #include "proof/proof_node_manager.h"
+#include "smt/logic_exception.h"
 #include "smt_util/boolean_simplification.h"
 #include "theory/booleans/circuit_propagator.h"
 #include "theory/booleans/theory_bool_rewriter.h"
@@ -28,6 +29,8 @@
 #include "theory/valuation.h"
 #include "util/hash.h"
 
+using namespace cvc5::kind;
+
 namespace cvc5 {
 namespace theory {
 namespace booleans {
@@ -66,6 +69,23 @@ Theory::PPAssertStatus TheoryBool::ppAssert(
   return Theory::ppAssert(tin, outSubstitutions);
 }
 
+TrustNode TheoryBool::ppRewrite(TNode n, std::vector<SkolemLemma>& lems)
+{
+  Trace("bool-ppr") << "TheoryBool::ppRewrite " << n << std::endl;
+  if (n.getKind() == ITE)
+  {
+    TypeNode tn = n.getType();
+    if (!tn.isFirstClass())
+    {
+      std::stringstream ss;
+      ss << "ITE branches of type " << tn << " are currently not supported."
+         << std::endl;
+      throw LogicException(ss.str());
+    }
+  }
+  return TrustNode::null();
+}
+
 TheoryRewriter* TheoryBool::getTheoryRewriter() { return &d_rewriter; }
 
 ProofRuleChecker* TheoryBool::getProofChecker() { return &d_checker; }

diff --git a/src/theory/booleans/theory_bool.h b/src/theory/booleans/theory_bool.h
index e0b7e6511b5ac8c94cab4c93e958e2d4b1b7fff4..6c197d7975fc0931845578b96bd0b13849543893 100644 (file)
--- a/src/theory/booleans/theory_bool.h
+++ b/src/theory/booleans/theory_bool.h
@@ -39,6 +39,8 @@ class TheoryBool : public Theory {
   PPAssertStatus ppAssert(TrustNode tin,
                           TrustSubstitutionMap& outSubstitutions) override;
 
+  TrustNode ppRewrite(TNode n, std::vector<SkolemLemma>& lems) override;
+
   std::string identify() const override;
 
  private:

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 197c221966db9e49de16eb1354dae923989b2446..a3fd70683bf58cfbeb479fc515ef2273cbc5b12c 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1246,6 +1246,7 @@ set(regress_0_tests
   regress0/strings/norn-31.smt2
   regress0/strings/norn-simp-rew.smt2
   regress0/strings/parser-syms.cvc.smt2
+  regress0/strings/proj-issue316-regexp-ite.smt2
   regress0/strings/re_diff.smt2
   regress0/strings/re-in-rewrite.smt2
   regress0/strings/re-syntax.smt2

diff --git a/test/regress/regress0/strings/proj-issue316-regexp-ite.smt2 b/test/regress/regress0/strings/proj-issue316-regexp-ite.smt2
new file mode 100644 (file)
index 0000000..e19accd
--- /dev/null
+++ b/test/regress/regress0/strings/proj-issue316-regexp-ite.smt2
@@ -0,0 +1,10 @@
+; COMMAND-LINE: --theoryof-mode=type
+; COMMAND-LINE: --theoryof-mode=term
+; SCRUBBER: grep -o "ITE branches of type RegLan are currently not supported"
+; EXPECT: ITE branches of type RegLan are currently not supported
+; EXIT: 1 
+(set-logic QF_SLIA)
+(declare-const b Bool)
+(declare-const x String)
+(assert (str.in_re x (ite b re.none re.allchar)))
+(check-sat)