projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: af71076) | patch
Refactoring the single invocation solver (#5706)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Wed, 20 Jan 2021 23:32:06 +0000 (17:32 -0600)
committerGitHub <noreply@github.com>
Wed, 20 Jan 2021 23:32:06 +0000 (17:32 -0600)
commit75cd4fe254f1f4de846b5cf9489b591dffbca333
tree463beb7e0d6cb191eb6bcf671150d30d1cfbca92tree
parentaf7107611a37d45d495d0d40c50b67c08fc7de9ccommit | diff
Refactoring the single invocation solver (#5706)

This does an intermediate refactoring of the single invocation solver to make a few things clearer and to add preliminary support for functions that have been marked as solved by external techniques.

This is in preparation for generalizing the CAV 2015 single invocation techniques.
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 diff | blob | history
src/theory/quantifiers/sygus/ce_guided_single_inv_sol.h diff | blob | history