projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 2f46d30) | patch
Types & side-conditions for linear and affine fns (#3627)
authorAlex Ozdemir <aozdemir@hmc.edu>
Tue, 21 Jan 2020 20:15:10 +0000 (12:15 -0800)
committerGitHub <noreply@github.com>
Tue, 21 Jan 2020 20:15:10 +0000 (12:15 -0800)
commitf90660bac410b8790d460be2ebd248e543a587e1
tree8dbcbc95b17769b23f9656d989bd27ea7f1bfe80tree
parent2f46d30ea76158dec2118e35086290ae7ddceedfcommit | diff
Types & side-conditions for linear and affine fns (#3627)

This commit introduces types for linear combinations of arith variables
along with side conditions for their arithmetic.

It does the same for affine functions.

These primitives are ultimately used in our machinery for Farkas proofs.
proofs/signatures/th_lira.plf diff | blob | history