projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: c6a7138) | patch
Fix BagsRewriter::rewriteUnionDisjoint (#5840)
authormudathirmahgoub <mudathirmahgoub@gmail.com>
Mon, 1 Feb 2021 14:42:39 +0000 (08:42 -0600)
committerGitHub <noreply@github.com>
Mon, 1 Feb 2021 14:42:39 +0000 (08:42 -0600)
commitc0937f742479d8a5054e42597da9447d55e876c0
tree386fa3a7a46be381ba61ce132a538fe811cf16f9tree
parentc6a71382bad8bae30b8278055995279c36433811commit | diff
Fix BagsRewriter::rewriteUnionDisjoint (#5840)

This PR fixes the implementation of (union_disjoint (union_max A B) (intersection_min A B)) =(union_disjoint A B).
It also skips processed bags during model building.
src/theory/bags/bags_rewriter.cpp diff | blob | history
src/theory/bags/theory_bags.cpp diff | blob | history
test/unit/theory/theory_bags_rewriter_white.h diff | blob | history