From f66e1fc33ee7549c90eabc808be5a6ef6196aaa0 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 23 Oct 2020 13:03:17 -0500 Subject: [PATCH] Fix related to preregistering boolean term variables in strings (#5331) We should only add trigger predicates for string predicates, and not arbitrary Boolean terms (which can now occur since we are handling parametric sequences). This avoids a debug assertion failure reported on as a followup to #4370. In that benchmark BOOLEAN_TERM_VARIABLE was being added as a trigger predicate. --- src/theory/strings/term_registry.cpp | 8 ++++++-- src/theory/uf/equality_engine.cpp | 2 +- test/regress/CMakeLists.txt | 1 + .../regress0/seq/issue4370-bool-terms.smt2 | 18 ++++++++++++++++++ 4 files changed, 26 insertions(+), 3 deletions(-) create mode 100644 test/regress/regress0/seq/issue4370-bool-terms.smt2 diff --git a/src/theory/strings/term_registry.cpp b/src/theory/strings/term_registry.cpp index b5b2a5a13..2b5daa476 100644 --- a/src/theory/strings/term_registry.cpp +++ b/src/theory/strings/term_registry.cpp @@ -203,8 +203,12 @@ void TermRegistry::preRegisterTerm(TNode n) } else if (tn.isBoolean()) { - // Get triggered for both equal and dis-equal - ee->addTriggerPredicate(n); + // All kinds that we do congruence over that may return a Boolean go here + if (k==STRING_STRCTN || k == STRING_LEQ || k == SEQ_NTH) + { + // Get triggered for both equal and dis-equal + ee->addTriggerPredicate(n); + } } else { diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp index e48e91cd0..fdb80e878 100644 --- a/src/theory/uf/equality_engine.cpp +++ b/src/theory/uf/equality_engine.cpp @@ -1739,7 +1739,7 @@ void EqualityEngine::addTriggerPredicate(TNode predicate) { return addTriggerEquality(predicate); } Assert(d_congruenceKinds.tst(predicate.getKind())) - << "No point in adding non-congruence predicates"; + << "No point in adding non-congruence predicates, kind is " << predicate.getKind(); if (d_done) { return; diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 6c2c51dfb..4653f1c3e 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -883,6 +883,7 @@ set(regress_0_tests regress0/sep/wand-crash.smt2 regress0/seq/intseq.smt2 regress0/seq/intseq_dt.smt2 + regress0/seq/issue4370-bool-terms.smt2 regress0/seq/seq-2var.smt2 regress0/seq/seq-ex1.smt2 regress0/seq/seq-ex2.smt2 diff --git a/test/regress/regress0/seq/issue4370-bool-terms.smt2 b/test/regress/regress0/seq/issue4370-bool-terms.smt2 new file mode 100644 index 000000000..8f6a16b45 --- /dev/null +++ b/test/regress/regress0/seq/issue4370-bool-terms.smt2 @@ -0,0 +1,18 @@ +; COMMAND-LINE: --strings-exp --no-check-models +(set-logic ALL) +(set-info :status sat) +(declare-datatypes ((a 0)) (((b)))) +(define-fun v () (Seq Bool) (as seq.empty (Seq Bool))) +(declare-fun e () (Seq a)) +(define-fun w () Int (seq.len e)) +(define-fun x () (Seq a) (seq.extract e 1 (- w 1))) +(define-fun i () (Seq a) (seq.extract x 1 (- (seq.len x) 1))) +(define-fun y () (Seq Bool) (ite (= 0 (seq.len i)) v (seq.unit true))) +(define-fun m () (Seq Bool) (seq.++ (seq.unit false) y)) +(define-fun n () (Seq Bool) (ite (= 0 (seq.len x)) v m)) +(define-fun o () (Seq Bool) (seq.++ (seq.unit false) n)) +(define-fun p () (Seq Bool) (ite (= 0 w) v o)) +(define-fun s () (Seq Bool) (seq.extract p 1 (- (seq.len p) 1))) +(define-fun u () (Seq Bool) (seq.extract s 1 (- (seq.len s) 1))) +(assert (not (seq.nth u 0))) +(check-sat) -- 2.30.2