projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 2fcaf83) | patch
Sygus enumerators to conjecture (#1237)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Tue, 17 Oct 2017 00:21:25 +0000 (19:21 -0500)
committerGitHub <noreply@github.com>
Tue, 17 Oct 2017 00:21:25 +0000 (19:21 -0500)
commitcec475c392e7082406629a51d0da5aea7a6da151
tree3b6a81db5ea48dd055b4be71697b7758d6d62a17tree
parent2fcaf83bd8d93399cb1fb4bbfe3a252398d314c6commit | diff
Sygus enumerators to conjecture (#1237)

* Initial revision of mapping sygus enumeration terms to CegConjectures. This will allow us to generalize conjecture-specific symmetry breaking.

* Change function names, simplify.

* Fix assertion, minor optimization

* Cleanup, documentation, simplification.

* Address review.

* Apply clang format.
src/theory/datatypes/datatypes_sygus.cpp diff | blob | history
src/theory/datatypes/datatypes_sygus.h diff | blob | history
src/theory/quantifiers/ce_guided_conjecture.cpp diff | blob | history
src/theory/quantifiers/ce_guided_conjecture.h diff | blob | history
src/theory/quantifiers/ce_guided_pbe.cpp diff | blob | history
src/theory/quantifiers/ce_guided_pbe.h diff | blob | history
src/theory/quantifiers/term_database_sygus.cpp diff | blob | history
src/theory/quantifiers/term_database_sygus.h diff | blob | history