projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: ffbf4a8) | patch
Allow sygus in incremental mode (#7756)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Tue, 7 Dec 2021 19:01:11 +0000 (13:01 -0600)
committerGitHub <noreply@github.com>
Tue, 7 Dec 2021 19:01:11 +0000 (19:01 +0000)
commit3f7bd4478ff43359f4de09294226abdc453a7c58
tree4e2af283b8a4f237f8302ae66d9cdc09f7cbd257tree
parentffbf4a88580c72d7db41a807d3b39008a82b51f4commit | diff
Allow sygus in incremental mode (#7756)

This allows the basic use of SyGuS in incremental mode, where constraints can be pushed/popped.

It does not yet support getting multiple solutions for the same set of constraints, which will require more significant changes.
src/parser/smt2/Smt2.g diff | blob | history
src/smt/sygus_solver.cpp diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress0/sygus/incremental-modify-ex.sy [new file with mode: 0644] blob