projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: c214051) | patch
Loop over terms to reconstruct instead of obligations. (#6504)
authorAbdalrhman Mohamed <32971963+abdoo8080@users.noreply.github.com>
Tue, 18 May 2021 22:32:21 +0000 (17:32 -0500)
committerGitHub <noreply@github.com>
Tue, 18 May 2021 22:32:21 +0000 (22:32 +0000)
commit47f71a6d94b600cf7c132569fa05ad1666edc408
tree3c4b244cd467f1ca888edfcf6edd5df358ce2aactree
parentc214051068aefdf831bf67e6b7d72591e5a91ececommit | diff
Loop over terms to reconstruct instead of obligations. (#6504)

This PR modifies the rcons algorithm to loop over terms to reconstruct instead of obligations. It also modifies the Obs data structure to reflect this change. The rest of the PR is mostly updating documentation and refactoring the affected code.
src/CMakeLists.txt diff | blob | history
src/theory/quantifiers/sygus/rcons_obligation.cpp [new file with mode: 0644] blob
src/theory/quantifiers/sygus/rcons_obligation.h [new file with mode: 0644] blob
src/theory/quantifiers/sygus/rcons_obligation_info.cpp [deleted file] blob | history
src/theory/quantifiers/sygus/rcons_obligation_info.h [deleted file] blob | history
src/theory/quantifiers/sygus/rcons_type_info.cpp diff | blob | history
src/theory/quantifiers/sygus/rcons_type_info.h diff | blob | history
src/theory/quantifiers/sygus/sygus_reconstruct.cpp diff | blob | history
src/theory/quantifiers/sygus/sygus_reconstruct.h diff | blob | history
test/regress/regress1/sygus/eq-sub-obs.sy diff | blob | history