From 2a38d482462fdf30376c984e7a82c99d08e75f92 Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Wed, 22 Apr 2020 04:32:06 -0700 Subject: [PATCH] Reinstantiate support for conjunctions in facts (#4377) Fixes #4376. Commit 6255c0356bd78140a9cf075491c1d4608ac27704 removed support for conjunctions in the conclusion of facts. However, `F_ENDPOINT_EMP` generates a conjunction in the conclusion of the inference if multiple components are inferred to be empty. This commit reinstantiates support for conjunctions in the conclusion of facts. --- src/theory/strings/inference_manager.cpp | 32 ++++++++++++++------ test/regress/CMakeLists.txt | 1 + test/regress/regress0/strings/issue4376.smt2 | 11 +++++++ 3 files changed, 35 insertions(+), 9 deletions(-) create mode 100644 test/regress/regress0/strings/issue4376.smt2 diff --git a/src/theory/strings/inference_manager.cpp b/src/theory/strings/inference_manager.cpp index 8e68913ac..42dc975fa 100644 --- a/src/theory/strings/inference_manager.cpp +++ b/src/theory/strings/inference_manager.cpp @@ -279,24 +279,38 @@ void InferenceManager::doPendingFacts() // should be added as a normal equality or predicate to the equality engine // with no new external assumptions (ii.d_antn). Assert(ii.isFact()); - Node fact = ii.d_conc; + Node facts = ii.d_conc; Node exp = utils::mkAnd(ii.d_ant); - Trace("strings-assert") << "(assert (=> " << exp << " " << fact + Trace("strings-assert") << "(assert (=> " << exp << " " << facts << ")) ; fact " << ii.d_id << std::endl; // only keep stats if we process it here - Trace("strings-lemma") << "Strings::Fact: " << fact << " from " << exp + Trace("strings-lemma") << "Strings::Fact: " << facts << " from " << exp << " by " << ii.d_id << std::endl; d_statistics.d_inferences << ii.d_id; // assert it as a pending fact - bool polarity = fact.getKind() != NOT; - TNode atom = polarity ? fact : fact[0]; - // no double negation or double (conjunctive) conclusions - Assert(atom.getKind() != NOT && atom.getKind() != AND); - assertPendingFact(atom, polarity, exp); + if (facts.getKind() == AND) + { + for (const Node& fact : facts) + { + bool polarity = fact.getKind() != NOT; + TNode atom = polarity ? fact : fact[0]; + // no double negation or double (conjunctive) conclusions + Assert(atom.getKind() != NOT && atom.getKind() != AND); + assertPendingFact(atom, polarity, exp); + } + } + else + { + bool polarity = facts.getKind() != NOT; + TNode atom = polarity ? facts : facts[0]; + // no double negation or double (conjunctive) conclusions + Assert(atom.getKind() != NOT && atom.getKind() != AND); + assertPendingFact(atom, polarity, exp); + } // Must reference count the equality and its explanation, which is not done // by the equality engine. Notice that we do not need to do this for // external assertions, which enter as facts through sendAssumption. - d_keep.insert(fact); + d_keep.insert(facts); d_keep.insert(exp); i++; } diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 2b24767d6..ac96110ce 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -947,6 +947,7 @@ set(regress_0_tests regress0/strings/issue3497.smt2 regress0/strings/issue3657-evalLeq.smt2 regress0/strings/issue4070.smt2 + regress0/strings/issue4376.smt2 regress0/strings/itos-entail.smt2 regress0/strings/large-model.smt2 regress0/strings/leadingzero001.smt2 diff --git a/test/regress/regress0/strings/issue4376.smt2 b/test/regress/regress0/strings/issue4376.smt2 new file mode 100644 index 000000000..f6dd88059 --- /dev/null +++ b/test/regress/regress0/strings/issue4376.smt2 @@ -0,0 +1,11 @@ +; COMMAND-LINE: --strings-exp --strings-eager +(set-info :status sat) +(set-logic QF_SLIA) +(declare-const i0 Int) +(declare-const Str1 String) +(declare-const Str9 String) +(declare-const Str11 String) +(declare-const Str15 String) +(assert (= (str.++ Str1 "ijruldtzyp") Str15)) +(assert (= (str.++ (str.++ Str1 "ijruldtzyp") Str11 (int.to.str i0)) Str15 Str9)) +(check-sat) -- 2.30.2