projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 35f58d8) | patch
Consolidate basic sygus utilities regarding sygus conjectures (#5421)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Tue, 15 Dec 2020 21:19:08 +0000 (15:19 -0600)
committerGitHub <noreply@github.com>
Tue, 15 Dec 2020 21:19:08 +0000 (15:19 -0600)
commit8c4598683e4edd217ed524d47c68a053b6881f4c
tree5fe19c4d5e0fba6800ba2b3f853617f2b6e390ectree
parent35f58d81fb57608d52884f560ff281fe52c7b18fcommit | diff
Consolidate basic sygus utilities regarding sygus conjectures (#5421)

This is required for new work on generalizing CAV 2015 single invocation techniques.

It adds a new system of marking solutions for synthesis conjectures as attributes, which will be used as a way of eliminating functions from a conjecture while still preserving their solution in a response to check-synth.
src/CMakeLists.txt diff | blob | history
src/preprocessing/passes/sygus_inference.cpp diff | blob | history
src/preprocessing/passes/synth_rew_rules.cpp diff | blob | history
src/theory/quantifiers/sygus/sygus_abduct.cpp diff | blob | history
src/theory/quantifiers/sygus/sygus_grammar_cons.cpp diff | blob | history
src/theory/quantifiers/sygus/sygus_grammar_cons.h diff | blob | history
src/theory/quantifiers/sygus/sygus_utils.cpp [new file with mode: 0644] blob
src/theory/quantifiers/sygus/sygus_utils.h [new file with mode: 0644] blob
src/theory/quantifiers/sygus/template_infer.cpp diff | blob | history