projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 069fde2) | patch
Simplify skolemization in sygus solver (#7331)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Tue, 12 Oct 2021 14:03:29 +0000 (09:03 -0500)
committerGitHub <noreply@github.com>
Tue, 12 Oct 2021 14:03:29 +0000 (14:03 +0000)
commit049203b5060dfb452429318bcb408c6db640a7a6
tree00ceda4601e575e5e015da2c7ceac6e642c1d6c3tree
parent069fde2aac69f741bc7679f64bbdc9aed4874b73commit | diff
Simplify skolemization in sygus solver (#7331)

The core sygus solver predates the use of subsolvers. When doing verification checks in the CEGIS loop, we previously added unique lemmas to the main solver with fresh skolem variables. We now call subsolvers only, meaning that the set of skolem variables used in verification calls can be fixed.
src/theory/quantifiers/sygus/synth_conjecture.cpp diff | blob | history
src/theory/quantifiers/sygus/synth_conjecture.h diff | blob | history