projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: c69f492) | patch
Add addition utilities for the arithmetic rewriter (#8013)
authorGereon Kremer <gkremer@cs.stanford.edu>
Tue, 8 Feb 2022 21:26:21 +0000 (13:26 -0800)
committerGitHub <noreply@github.com>
Tue, 8 Feb 2022 21:26:21 +0000 (21:26 +0000)
commitc93eccb4706804ffc139548f9d2f2145fda820a9
tree46ccbd9ab34e3683eb8d415d6faddcedda83f83ctree
parentc69f49277837aa3d4e79e07f1b8170dec03bf287commit | diff
Add addition utilities for the arithmetic rewriter (#8013)

This PR adds methods to deal with sums in the arithmetic rewriter. Sums are stored as std::map<Node,RealAlgebraicNumber> (see the code for some reasoning), and we implement adding terms to sums, collecting sums into nodes and distributing a multiplication over nested sums.
src/CMakeLists.txt diff | blob | history
src/theory/arith/rewriter/addition.cpp [new file with mode: 0644] blob
src/theory/arith/rewriter/addition.h [new file with mode: 0644] blob