diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2020-04-22 04:32:06 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-04-22 06:32:06 -0500 |
commit | 2a38d482462fdf30376c984e7a82c99d08e75f92 (patch) | |
tree | db3f24fbdc7bd097091dfced40f9d8a6c29c1e39 /src/theory/strings | |
parent | 6e1ac7281d5986f3636254988979e9048e5267c4 (diff) |
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.
Diffstat (limited to 'src/theory/strings')
-rw-r--r-- | src/theory/strings/inference_manager.cpp | 32 |
1 files changed, 23 insertions, 9 deletions
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++; } |