projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 34e84a2) | patch
Sygus process conjecture (#1286)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Sat, 28 Oct 2017 18:01:49 +0000 (13:01 -0500)
committerGitHub <noreply@github.com>
Sat, 28 Oct 2017 18:01:49 +0000 (13:01 -0500)
commit49912baa48d87e6d8c38f9bc3e1739b8fbe4e8b3
treeab9fd7aa2485871712bd9fd1e12d82a5275bf4c5tree
parent34e84a25a044e3af192bb69089467c2125911900commit | diff
Sygus process conjecture (#1286)

* Initial infrastructure for static preprocessing for sygus conjectures.

* Initial infrastructure.

* Minor change in terminology, move enumerator to synth-fun mapping to sygus term database, minor fix and add documentation to NegContainsInvarianceTest.

* Clang format

* Fixing comments, more initial infrastructure.

* More

* Minor

* New clang format.

* Address review.
src/Makefile.am diff | blob | history
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/sygus_process_conj.cpp [new file with mode: 0644] blob
src/theory/quantifiers/sygus_process_conj.h [new file with mode: 0644] blob
src/theory/quantifiers/term_database_sygus.cpp diff | blob | history
src/theory/quantifiers/term_database_sygus.h diff | blob | history