projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: c38f351) | patch
Interpolation: Add interface for SyGuS interpolation module (step3) (#4726)
authorYing Sheng <sqy1415@gmail.com>
Tue, 28 Jul 2020 16:55:52 +0000 (09:55 -0700)
committerGitHub <noreply@github.com>
Tue, 28 Jul 2020 16:55:52 +0000 (11:55 -0500)
commite63544462eb850a27f7b416f2f0613efb96eef1d
tree824a3e8d61a44a84a31c3eac651ccd2405c2fdfbtree
parentc38f35164adc5ab255803765a568ef820fa8f3b2commit | diff
Interpolation: Add interface for SyGuS interpolation module (step3) (#4726)

This is the 3rd step of adding interface for SyGuS Interpolation module. The whole change will be adding the API for (get-interpol s B), which is aim for computes an I that A->I and I->B. Here A is the assertions in the stack.

The 3rd step partially implemented the interpolation module.
src/theory/quantifiers/sygus/sygus_interpol.cpp diff | blob | history
src/theory/quantifiers/sygus/sygus_interpol.h diff | blob | history