projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: fad0df0) | patch
Internal representation of oracle interface quantifiers (#8585)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Thu, 7 Apr 2022 21:32:07 +0000 (16:32 -0500)
committerGitHub <noreply@github.com>
Thu, 7 Apr 2022 21:32:07 +0000 (21:32 +0000)
commit134c3bf441564f32c7978ba17d581751bc457a97
treeaa6bc81ff8da6af9656e4bd127cbbbdaf63cd790tree
parentfad0df02d9d56c717c37269b50497ec5c58749f3commit | diff
Internal representation of oracle interface quantifiers (#8585)

This is the first step towards supporting SMT and synthesis modulo oracles.

It adds the kind required for specifying "oracle interface quantifiers", or, quantified formulas that specify constraints that depend on an external binary.
src/theory/quantifiers/kinds diff | blob | history
src/theory/quantifiers/quantifiers_attributes.cpp diff | blob | history
src/theory/quantifiers/quantifiers_attributes.h diff | blob | history
src/theory/quantifiers/theory_quantifiers_type_rules.cpp diff | blob | history
src/theory/quantifiers/theory_quantifiers_type_rules.h diff | blob | history