projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 5dd102d) | patch
Sygus logics (#1226)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Thu, 12 Oct 2017 18:00:12 +0000 (13:00 -0500)
committerGitHub <noreply@github.com>
Thu, 12 Oct 2017 18:00:12 +0000 (13:00 -0500)
commitebd9c958a0c20e37cc0e1a79be26afd525dd8fb9
treef53a09d9f8cba99173683ae6c43b386b6b057478tree
parent5dd102d4cb7fc8413d6e8f68b0c32c9ef06b1b17commit | diff
Sygus logics (#1226)

* Allow any smt2 logic to be a sygus logic. Add non-linear SyGuS regressions.

* Minor

* Add case for reals, comment.

* Fix regress1.
src/parser/smt2/smt2.cpp diff | blob | history
test/regress/regress0/sygus/Makefile.am diff | blob | history
test/regress/regress0/sygus/nia-max-square-ns.sy [new file with mode: 0644] blob
test/regress/regress1/sygus/Makefile.am diff | blob | history
test/regress/regress1/sygus/nia-max-square.sy [new file with mode: 0644] blob