projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: c1e90ce) | patch
Add PfRule ARITH_POLY_NORM (#7501)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Fri, 29 Oct 2021 16:36:26 +0000 (11:36 -0500)
committerGitHub <noreply@github.com>
Fri, 29 Oct 2021 16:36:26 +0000 (16:36 +0000)
commitf12af39c6ac5f19913b9e9996eb9453eb7b30034
treec24ae7368a4de4a2064162c237865b69ab5d9758tree
parentc1e90ce118705dc3d572300fd8c922973864df91commit | diff
Add PfRule ARITH_POLY_NORM (#7501)

This is a coarse grained proof rule for showing that two terms are equivalent up to polynomial normalization. It will be used as a hard coded case in proof reconstruction with DSL granularity.
src/CMakeLists.txt diff | blob | history
src/proof/proof_rule.cpp diff | blob | history
src/proof/proof_rule.h diff | blob | history
src/theory/arith/arith_poly_norm.cpp [new file with mode: 0644] blob
src/theory/arith/arith_poly_norm.h [new file with mode: 0644] blob
src/theory/arith/proof_checker.cpp diff | blob | history
test/unit/theory/CMakeLists.txt diff | blob | history
test/unit/theory/arith_poly_white.cpp [new file with mode: 0644] blob