projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 2b7a016) | patch
Move finite model minimization to UF last call effort (#5050)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Fri, 11 Sep 2020 21:01:11 +0000 (16:01 -0500)
committerGitHub <noreply@github.com>
Fri, 11 Sep 2020 21:01:11 +0000 (16:01 -0500)
commitb7bbe9a3bc30f41d1775a187ccc732aaeb41eaa1
tree8f4d23e04f93aef397c2adafe2e671e2907671cetree
parent2b7a0168bddfd2b840171aa8b9681f16d606c0b8commit | diff
Move finite model minimization to UF last call effort (#5050)

This moves model minimization happen in TheoryUF's last call effort check instead of being a custom call in quantifiers finite model finding. This is both a better design and avoids bugs when quantifiers are not enabled (for QF_UF+cardinality constraints).

Fixes #4850.
src/theory/quantifiers/fmf/model_engine.cpp diff | blob | history
src/theory/theory_state.cpp diff | blob | history
src/theory/theory_state.h diff | blob | history
src/theory/uf/cardinality_extension.cpp diff | blob | history
src/theory/uf/cardinality_extension.h diff | blob | history
src/theory/uf/theory_uf.cpp diff | blob | history
src/theory/uf/theory_uf.h diff | blob | history
src/theory/valuation.h diff | blob | history
test/regress/regress0/fmf/issue4850-force-card.smt2 [new file with mode: 0644] blob