projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 376d72f) | patch
(Refactor) Split sygus term db (#1335)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Tue, 14 Nov 2017 23:04:14 +0000 (17:04 -0600)
committerGitHub <noreply@github.com>
Tue, 14 Nov 2017 23:04:14 +0000 (17:04 -0600)
commit748e20967ae7698f6b545a5128633865701aeb2d
tree3413586dbdeff2ddfbb604db5c1e6045b1a749a7tree
parent376d72fd02d7f8822188055355452449b718481fcommit | diff
(Refactor) Split sygus term db (#1335)

* Split explain utility, invariance tests.

* Split extended rewriter.

* Remove unused function.

* Minor

* Move generic term utilities to term_util.

* Documentation, minor.

* Make arguments private in eval invariance.

* Document

* More documentation.

* Clang format.

* Fix, improve.

* Format

* Address review.

* Address missed comment.

* Add line breaks

* Format
16 files changed:
src/Makefile.am diff | blob | history
src/theory/datatypes/datatypes_sygus.cpp diff | blob | history
src/theory/quantifiers/ce_guided_conjecture.cpp diff | blob | history
src/theory/quantifiers/ce_guided_instantiation.cpp 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/extended_rewrite.cpp [new file with mode: 0644] blob
src/theory/quantifiers/extended_rewrite.h [new file with mode: 0644] blob
src/theory/quantifiers/sygus_explain.cpp diff | blob | history
src/theory/quantifiers/sygus_explain.h diff | blob | history
src/theory/quantifiers/sygus_invariance.cpp [new file with mode: 0644] blob
src/theory/quantifiers/sygus_invariance.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
src/theory/quantifiers/term_util.cpp diff | blob | history
src/theory/quantifiers/term_util.h diff | blob | history