projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 2fb5ff6) | patch
Add implementation for SyGuS interpolation module (step4) (#4811)
authorYing Sheng <sqy1415@gmail.com>
Mon, 3 Aug 2020 23:26:08 +0000 (16:26 -0700)
committerGitHub <noreply@github.com>
Mon, 3 Aug 2020 23:26:08 +0000 (16:26 -0700)
commit3dad390f4216a9d279197a52b40b8e93696d4019
tree5b0ad70f88b9e36be2afb920b6535cd32fbd869dtree
parent2fb5ff63e8e80b06450a8a2a33d7d61cc0a0e2accommit | diff
Add implementation for SyGuS interpolation module (step4) (#4811)

This is the 4th 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 4th step finished the implementation of the interpolation module.
src/theory/quantifiers/sygus/sygus_interpol.cpp diff | blob | history
src/theory/quantifiers/sygus/sygus_interpol.h diff | blob | history