From b3f0087c07dd183748d063f0581a711f781e2d42 Mon Sep 17 00:00:00 2001
From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Wed, 27 Oct 2021 12:46:24 -0700
Subject: [PATCH] Require ITE branches to be first class types (#7508)

Fixes cvc5/cvc5-projects#316.
---
 src/theory/booleans/theory_bool.cpp           | 20 +++++++++++++++++++
 src/theory/booleans/theory_bool.h             |  2 ++
 test/regress/CMakeLists.txt                   |  1 +
 .../strings/proj-issue316-regexp-ite.smt2     | 10 ++++++++++
 4 files changed, 33 insertions(+)
 create mode 100644 test/regress/regress0/strings/proj-issue316-regexp-ite.smt2

diff --git a/src/theory/booleans/theory_bool.cpp b/src/theory/booleans/theory_bool.cpp
index 33bb820b4..1327d1131 100644
--- 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 e0b7e6511..6c197d797 100644
--- 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 197c22196..a3fd70683 100644
--- 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
index 000000000..e19accd36
--- /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)
-- 
2.30.2