projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: ebf4ff6) | patch
Eliminate use of subtyping from results of quantifier elimination (#7885)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Wed, 12 Jan 2022 15:58:14 +0000 (09:58 -0600)
committerGitHub <noreply@github.com>
Wed, 12 Jan 2022 15:58:14 +0000 (15:58 +0000)
commit141c8f592c31422cc07b0d8965750db235195251
treef6838fd6afbe8650704d2a527f78a9f8047f80actree
parentebf4ff6cc2d93c59ef347f6db515bf3e44c036f3commit | diff
Eliminate use of subtyping from results of quantifier elimination (#7885)

Fixes #7870.

Notice this node converter is potentially unnecessary if we ever get rid of arithmetic subtyping.
src/expr/CMakeLists.txt diff | blob | history
src/expr/subtype_elim_node_converter.cpp [new file with mode: 0644] blob
src/expr/subtype_elim_node_converter.h [new file with mode: 0644] blob
src/smt/quant_elim_solver.cpp diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress1/quantifiers/qe-subtypes.smt2 [new file with mode: 0644] blob