projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: e348f20) | patch
Direct lemmas and inference ids for sygus extension (#5960)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Thu, 11 Mar 2021 08:44:30 +0000 (02:44 -0600)
committerGitHub <noreply@github.com>
Thu, 11 Mar 2021 08:44:30 +0000 (08:44 +0000)
commit223155cfb300458f534f4be6b88e5fdc17b0ff14
treeea6eb835057de2c1705020ef5e4f8b1c18a1b6e8tree
parente348f20c62bd55993d675ba4994d7aa6322b7b2fcommit | diff
Direct lemmas and inference ids for sygus extension (#5960)

This adds inference ID for the datatypes sygus solver, and changes its style to send lemmas instead of passing them to the caller.
src/theory/datatypes/inference_manager.cpp diff | blob | history
src/theory/datatypes/inference_manager.h diff | blob | history
src/theory/datatypes/sygus_extension.cpp diff | blob | history
src/theory/datatypes/sygus_extension.h diff | blob | history
src/theory/datatypes/theory_datatypes.cpp diff | blob | history
src/theory/inference_id.cpp diff | blob | history
src/theory/inference_id.h diff | blob | history