projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: bc37256) | patch
Move libpoly <-> CoCoA conversion to new utility (#8199)
authorGereon Kremer <gereon.kremer@cs.rwth-aachen.de>
Wed, 2 Mar 2022 17:21:32 +0000 (18:21 +0100)
committerGitHub <noreply@github.com>
Wed, 2 Mar 2022 17:21:32 +0000 (17:21 +0000)
commit0ac85165d7550f5206593b0ea6440979050fa736
tree7f1b38db13835f07c8f6503ddfe3525eb23ebe61tree
parentbc37256a1a23ade3ebecc74247d0e69f02abc844commit | diff
Move libpoly <-> CoCoA conversion to new utility (#8199)

This PR factors the conversion between libpoly and CoCoA out of the LazardEvaluation class into a new utility. The goal is to make it reusable for other applications of CoCoA within cvc5, for example to replace the (rather naive) equality substitution utility by a new simplification technique based on CoCoAs Gröbner bases. This PR merely moves code around and should not actually change anything.
src/CMakeLists.txt diff | blob | history
src/theory/arith/nl/coverings/cocoa_converter.cpp [new file with mode: 0644] blob
src/theory/arith/nl/coverings/cocoa_converter.h [new file with mode: 0644] blob
src/theory/arith/nl/coverings/lazard_evaluation.cpp diff | blob | history