projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: fc0a5dc) | patch
Make Sygus conjectures higher-order (#1244)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Fri, 20 Oct 2017 19:52:31 +0000 (14:52 -0500)
committerGitHub <noreply@github.com>
Fri, 20 Oct 2017 19:52:31 +0000 (14:52 -0500)
commit78373c7f5fe93b7e8bbea10e3924f24d25a618ac
treeb3bd84e3d2154a4835679c71c028e87dbe1e2665tree
parentfc0a5dcc002b12f075681d53e87cca1ddfbd479dcommit | diff
Make Sygus conjectures higher-order (#1244)

* Represent sygus synthesis conjectures using higher-order quantification, remove associated hacks.

* Minor fix

* Fix bug in Node::hasBoundVar for non-ground operators.

* Add regression.

* Address review.

* Apply clang format.
12 files changed:
src/expr/node.cpp diff | blob | history
src/parser/smt2/Smt2.g diff | blob | history
src/parser/smt2/smt2.cpp diff | blob | history
src/smt/smt_engine.cpp diff | blob | history
src/theory/quantifiers/ce_guided_conjecture.cpp diff | blob | history
src/theory/quantifiers/ce_guided_single_inv.cpp diff | blob | history
src/theory/quantifiers/quantifiers_attributes.cpp diff | blob | history
src/theory/quantifiers/sygus_grammar_cons.cpp diff | blob | history
src/theory/quantifiers/term_util.h diff | blob | history
src/theory/quantifiers/theory_quantifiers.cpp diff | blob | history
test/regress/regress1/sygus/MPwL_d1s3.sy [new file with mode: 0644] blob
test/regress/regress1/sygus/Makefile.am diff | blob | history