projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 0e79ea9) | patch
Minor improvements to substitutions (#6380)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Thu, 22 Apr 2021 22:36:02 +0000 (17:36 -0500)
committerGitHub <noreply@github.com>
Thu, 22 Apr 2021 22:36:02 +0000 (22:36 +0000)
commitcd7432f10ca15585df81e3ef2d49fcddbfa9c3c8
tree0bdb3f081a7c878f4b3c0a9440551f7eb1e95b8dtree
parent0e79ea91e254a716b94bc74dc9e5aef13d4a8cbacommit | diff
Minor improvements to substitutions (#6380)

In preparation for using this class as part of our proof checker.

This removes an option that was previously used as a hack to try to make check-models work for quantifiers. It also makes supplying a context optional.
src/theory/substitutions.cpp diff | blob | history
src/theory/substitutions.h diff | blob | history
src/theory/theory_model.cpp diff | blob | history