projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: c099abe) | patch
Handle `expectedType` in TheoryProofEngine (#3691)
authorAlex Ozdemir <aozdemir@hmc.edu>
Sat, 1 Feb 2020 07:44:24 +0000 (23:44 -0800)
committerGitHub <noreply@github.com>
Sat, 1 Feb 2020 07:44:24 +0000 (23:44 -0800)
commit7583e034bbd991877b634d50249bbccfd9e3c763
tree9c4034b7eaa5a10663347f945dfb3362bcd913e9tree
parentc099abeb9c3a45019b18daac19c4b4cd43b4c6f0commit | diff
Handle `expectedType` in TheoryProofEngine (#3691)

`TheoryProofEngine` now uses the `expectedType` optional argument.
  * When printing terms, it sets this for theories that it dispatches too
  * It occasionally asks theories for help determining the `expectedType` using `equalityType`, which has a sensible default implementation.
  * It is mindful of `expectedType` when using the let map.

I also moved to hpp function implementations into the cpp.
src/proof/theory_proof.cpp diff | blob | history
src/proof/theory_proof.h diff | blob | history