Strings: Strengthen multiset reasoning (#2817)
authorAndres Noetzli <andres.noetzli@gmail.com>
Wed, 23 Jan 2019 02:47:08 +0000 (18:47 -0800)
committerGitHub <noreply@github.com>
Wed, 23 Jan 2019 02:47:08 +0000 (18:47 -0800)
commit03e5936c2e265a85d5a98d8cd4c4015da3b508f2
tree82d6fc62daa0627bcd04cfea73c063294d50d2cb
parente5f4e2c0c1dc79f9940ddb4fcdbf04d6cffe98f5
Strings: Strengthen multiset reasoning (#2817)

This commit introduces three helper methods for performing multiset
reasoning: an entailment check whether a term is always a strict subset
of another term in the multiset domain (`checkEntailMultisetSubset()`),
a check whether a string term is always homogeneous
(`checkEntailHomogeneousString()`), and an overapproximation for the
multiset domain (`getMultisetApproximation()`). It also adds unit tests
related to multiset reasoning.
src/theory/strings/theory_strings_rewriter.cpp
src/theory/strings/theory_strings_rewriter.h
test/unit/theory/theory_strings_rewriter_white.h