projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 83af1ef) | patch
Simplify sygus solver and sygus stream (#5389)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Thu, 12 Nov 2020 23:34:22 +0000 (17:34 -0600)
committerGitHub <noreply@github.com>
Thu, 12 Nov 2020 23:34:22 +0000 (17:34 -0600)
commitcf7c2ce97615990388bb6c37b151c0e2b2fe8f9a
tree8ed1f346c4b736eb17683e8f0727d3118b98ed13tree
parent83af1ef582a7ff3749126a5d91d5ef0ac34c1516commit | diff
Simplify sygus solver and sygus stream (#5389)

This simplifies the sygus solver based on the fact that verification lemmas are always processed in a separate subsolver.

In particular, this means that the implementation of --sygus-stream can be simplified signficantly.
src/theory/decision_manager.h diff | blob | history
src/theory/quantifiers/sygus/synth_conjecture.cpp diff | blob | history
src/theory/quantifiers/sygus/synth_conjecture.h diff | blob | history
src/theory/quantifiers/sygus/synth_engine.cpp diff | blob | history