Preparations for a CAD-based arithmetic solver (#4762)
authorGereon Kremer <nafur42@gmail.com>
Tue, 21 Jul 2020 13:28:38 +0000 (15:28 +0200)
committerGitHub <noreply@github.com>
Tue, 21 Jul 2020 13:28:38 +0000 (08:28 -0500)
commit45a546f63d40d8ef0e0fac53854930836da2c0ea
tree6495c1ea9059cdc88d6533c945223690f16304b7
parent614ad602bc1f895dad8eaa001a69a4211c5459d2
Preparations for a CAD-based arithmetic solver (#4762)

Based on #4679, this PR contains further preparations for a CAD-based arithmetic solver that extends the current NonlinearExtension.
In detail, it provides:

a Constraints class that manages all (polynomial) constraints visible to the cad solver,
a collection of methods used for cad projections,
a VariableOrdering class that provides different variable ordering heuristics tailored to cad,
an extension to the NlModel class, allowing for witness terms,
further conversion methods, in particular between Node and poly::Polynomial, poly::Value and RealAlgebraicNumber.
15 files changed:
src/CMakeLists.txt
src/theory/arith/nl/cad/constraints.cpp [new file with mode: 0644]
src/theory/arith/nl/cad/constraints.h [new file with mode: 0644]
src/theory/arith/nl/cad/projections.cpp [new file with mode: 0644]
src/theory/arith/nl/cad/projections.h [new file with mode: 0644]
src/theory/arith/nl/cad/variable_ordering.cpp [new file with mode: 0644]
src/theory/arith/nl/cad/variable_ordering.h [new file with mode: 0644]
src/theory/arith/nl/nl_model.cpp
src/theory/arith/nl/nl_model.h
src/theory/arith/nl/nonlinear_extension.cpp
src/theory/arith/nl/nonlinear_extension.h
src/theory/arith/nl/poly_conversion.cpp [new file with mode: 0644]
src/theory/arith/nl/poly_conversion.h [new file with mode: 0644]
src/util/poly_util.cpp
src/util/poly_util.h