projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: a276c52) | patch
Add arithmetic-specific, runtime, proof-macros. (#4992)
authorAlex Ozdemir <aozdemir@hmc.edu>
Tue, 1 Sep 2020 17:57:51 +0000 (10:57 -0700)
committerGitHub <noreply@github.com>
Tue, 1 Sep 2020 17:57:51 +0000 (14:57 -0300)
commit58f059a967ccb968f127b2d56f69c20700a943fb
tree86dc604488e7faa371020b59283339ee8bce3714tree
parenta276c5259782f867584bdd5e6e5cd50adc3c5daecommit | diff
Add arithmetic-specific, runtime, proof-macros. (#4992)

We'll use this to gate farkas-coefficient machinery after we remove the
old proof-macros.

I've changed the macros slightly from the proof-new branch: I removed the dependence on options::proof() (no longer wanted) and options::unsatCores() (I had copied this from the original proof macros, but it's not needed either, since we're in a theory).
src/theory/arith/proof_macros.h [new file with mode: 0644] blob