projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 83a18f9) | patch
Do not make models for quantified function variables (#4039)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Thu, 12 Mar 2020 19:42:45 +0000 (14:42 -0500)
committerGitHub <noreply@github.com>
Thu, 12 Mar 2020 19:42:45 +0000 (14:42 -0500)
commit9803bedfdfe42bf472654ed8e11bcc888de5df67
tree606a8ab6c334656d3268426521a8724e0101483dtree
parent83a18f98dddbd635db3823dd18b7bdf22b020869commit | diff
Do not make models for quantified function variables (#4039)

If we combine finite model finding and higher-order, then we could try to find a model find operators whose kind was BOUND_VARIABLE.
src/theory/quantifiers/first_order_model.cpp diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress1/sygus/issue3995-fmf-var-op.smt2 [new file with mode: 0644] blob