projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 4e6eb0a) | patch
(proof-new) Support proofs of quantifier instantiation (#5001)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Thu, 3 Sep 2020 00:47:52 +0000 (19:47 -0500)
committerGitHub <noreply@github.com>
Thu, 3 Sep 2020 00:47:52 +0000 (19:47 -0500)
commit5f3d21a7402538af837eaf943b5252b1db90080b
tree0f8a791a8b9fcd03545f720df1110516ada7689etree
parent4e6eb0a191ec78cbebd842f9c732ef9bd76bd724commit | diff
(proof-new) Support proofs of quantifier instantiation (#5001)

This adds basic support for proofs of quantifier instantiation, which is the main method for sending lemmas from TheoryQuantifiers. Quantifier instantiation is also heavily used for solving extended string functions.
src/preprocessing/passes/quantifiers_preprocess.cpp diff | blob | history
src/preprocessing/passes/sygus_inference.cpp diff | blob | history
src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp diff | blob | history
src/theory/quantifiers/cegqi/inst_strategy_cegqi.h diff | blob | history
src/theory/quantifiers/instantiate.cpp diff | blob | history
src/theory/quantifiers/instantiate.h diff | blob | history
src/theory/quantifiers/quantifiers_rewriter.cpp diff | blob | history
src/theory/quantifiers/quantifiers_rewriter.h diff | blob | history
src/theory/quantifiers_engine.cpp diff | blob | history
src/theory/quantifiers_engine.h diff | blob | history
src/theory/theory_engine.cpp diff | blob | history