projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 61b9dad) | patch
Replace old sygus term reconstruction algorithm with a new one. (#5779)
authorAbdalrhman Mohamed <32971963+abdoo8080@users.noreply.github.com>
Tue, 23 Mar 2021 14:44:39 +0000 (09:44 -0500)
committerGitHub <noreply@github.com>
Tue, 23 Mar 2021 14:44:39 +0000 (14:44 +0000)
commit6beb70fcedd18e965ad82949090365cb44a43692
tree0b66d7599fed75e39257a0d29e88483c59c6b03etree
parent61b9dadc88de3bf7d52538f9e914cfb61cbb7bb6commit | diff
Replace old sygus term reconstruction algorithm with a new one. (#5779)

This PR replaces the old algorithm for reconstructing sygus terms with a new "proper" implementation.
24 files changed:
src/CMakeLists.txt diff | blob | history
src/expr/node.h diff | blob | history
src/theory/quantifiers/candidate_rewrite_database.h diff | blob | history
src/theory/quantifiers/sygus/ce_guided_single_inv.cpp diff | blob | history
src/theory/quantifiers/sygus/ce_guided_single_inv.h diff | blob | history
src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp [deleted file] blob | history
src/theory/quantifiers/sygus/ce_guided_single_inv_sol.h [deleted file] blob | history
src/theory/quantifiers/sygus/rcons_obligation_info.cpp [new file with mode: 0644] blob
src/theory/quantifiers/sygus/rcons_obligation_info.h [new file with mode: 0644] blob
src/theory/quantifiers/sygus/rcons_type_info.cpp [new file with mode: 0644] blob
src/theory/quantifiers/sygus/rcons_type_info.h [new file with mode: 0644] blob
src/theory/quantifiers/sygus/sygus_reconstruct.cpp [new file with mode: 0644] blob
src/theory/quantifiers/sygus/sygus_reconstruct.h [new file with mode: 0644] blob
src/theory/quantifiers/sygus/synth_conjecture.cpp diff | blob | history
src/theory/quantifiers/sygus/synth_conjecture.h diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress1/sygus/array_search_2.sy diff | blob | history
test/regress/regress1/sygus/complex-no-rewrite.sy [new file with mode: 0644] blob
test/regress/regress1/sygus/complex-rewrite-in-db.sy [new file with mode: 0644] blob
test/regress/regress1/sygus/no-var-in-sol.sy [new file with mode: 0644] blob
test/regress/regress1/sygus/simple-no-rewrite.sy [new file with mode: 0644] blob
test/regress/regress1/sygus/simple-not-in-grammar.sy [new file with mode: 0644] blob
test/regress/regress1/sygus/simple-rewrite-in-db.sy [new file with mode: 0644] blob
test/regress/regress1/sygus/simple-rewrite-not-in-db.sy [new file with mode: 0644] blob