projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: f7d88b4) | patch
Improve finite model finding for recursive predicates (#1150)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Thu, 28 Sep 2017 12:23:33 +0000 (07:23 -0500)
committerGitHub <noreply@github.com>
Thu, 28 Sep 2017 12:23:33 +0000 (07:23 -0500)
commit42e970e822ec3d0adaacbff40e0aee02a32372cc
tree148cd56de0600e87338787c686c96650f7440996tree
parentf7d88b42cefcaa6bb48c2709bfd32cf52d35d5accommit | diff
Improve finite model finding for recursive predicates (#1150)

* Optimization for model finding for recursive functions involving branching positions. Update documentation, add regressions.

* Simplifications, update comments.
src/theory/quantifiers/fun_def_process.cpp diff | blob | history
src/theory/quantifiers/fun_def_process.h diff | blob | history
test/regress/regress0/fmf/Makefile.am diff | blob | history
test/regress/regress0/fmf/issue916-fmf-or.smt2 [new file with mode: 0644] blob
test/regress/regress0/fmf/pow2-bool.smt2 [new file with mode: 0644] blob