From 2d090a0db0945dbca4128ad5a8a739e366fd70a3 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 2 Feb 2022 13:32:48 -0600 Subject: [PATCH] Add missing null terminators for regexp (#8027) Led to some LFSC proof checking failures on strings benchmarks. --- src/expr/nary_term_util.cpp | 8 ++++++++ src/proof/lfsc/lfsc_node_converter.cpp | 2 ++ test/regress/CMakeLists.txt | 1 + test/regress/regress1/strings/instance2984-null-term.smt2 | 5 +++++ 4 files changed, 16 insertions(+) create mode 100644 test/regress/regress1/strings/instance2984-null-term.smt2 diff --git a/src/expr/nary_term_util.cpp b/src/expr/nary_term_util.cpp index 03ce637e4..500b45a81 100644 --- a/src/expr/nary_term_util.cpp +++ b/src/expr/nary_term_util.cpp @@ -132,6 +132,14 @@ Node getNullTerminator(Kind k, TypeNode tn) // the language containing only the empty string nullTerm = nm->mkNode(STRING_TO_REGEXP, nm->mkConst(String(""))); break; + case REGEXP_UNION: + // empty language + nullTerm = nm->mkNode(REGEXP_NONE); + break; + case REGEXP_INTER: + // universal language + nullTerm = nm->mkNode(REGEXP_STAR, nm->mkNode(REGEXP_ALLCHAR)); + break; case BITVECTOR_AND: nullTerm = theory::bv::utils::mkOnes(tn.getBitVectorSize()); break; diff --git a/src/proof/lfsc/lfsc_node_converter.cpp b/src/proof/lfsc/lfsc_node_converter.cpp index 148c5d9e7..8d1273dd2 100644 --- a/src/proof/lfsc/lfsc_node_converter.cpp +++ b/src/proof/lfsc/lfsc_node_converter.cpp @@ -450,6 +450,8 @@ Node LfscNodeConverter::postConvert(Node n) ret = nm->mkNode(ck, children[i], ret); } } + Trace("lfsc-term-process-debug") + << "...return n-ary conv " << ret << std::endl; return ret; } return n; diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 83cc6f1c8..aded275b6 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -2326,6 +2326,7 @@ set(regress_1_tests regress1/strings/idof-neg-index.smt2 regress1/strings/idof-triv.smt2 regress1/strings/ilc-l-nt.smt2 + regress1/strings/instance2984-null-term.smt2 regress1/strings/instance3303-delta.smt2 regress1/strings/instance7075-delta.smt2 regress1/strings/issue1105.smt2 diff --git a/test/regress/regress1/strings/instance2984-null-term.smt2 b/test/regress/regress1/strings/instance2984-null-term.smt2 new file mode 100644 index 000000000..da9389095 --- /dev/null +++ b/test/regress/regress1/strings/instance2984-null-term.smt2 @@ -0,0 +1,5 @@ +(set-logic ALL) +(set-info :status unsat) +(declare-const X String) +(assert (not (str.in_re X (re.union (str.to_re "") (re.comp (str.to_re "")) (re.* (str.to_re "")))))) +(check-sat) -- 2.30.2