projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 8590025) | patch
Fix to consider leafs of theory sets to be variables (#8305)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Tue, 15 Mar 2022 03:16:41 +0000 (22:16 -0500)
committerGitHub <noreply@github.com>
Tue, 15 Mar 2022 03:16:41 +0000 (03:16 +0000)
commit1ee275804ae31dbd13b67aaab01e757ec115c177
treef51de04655c8bf96c2b531a252133467175d9a56tree
parent85900254c193c7205afc6f67158459d0940b7426commit | diff
Fix to consider leafs of theory sets to be variables (#8305)

Fixes cvc5/cvc5-projects#494.

With this fix, we now properly consider terms that belong to other theories that are of set type, e.g. (select x (as set.universe (Set RoundingMode)) in this example to be "variables" according to the theory of sets procedure.

The benchmark is unsat because there are 5 rounding modes and we are selecting an index in a sequence storing "false" at the first 6 indices.
src/theory/sets/solver_state.cpp diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress1/sets/proj-issue494-finite-leafof.smt2 [new file with mode: 0644] blob