diff options
| author | Gereon Kremer <gereon.kremer@cs.rwth-aachen.de> | 2020-07-30 18:16:25 +0200 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-07-30 09:16:25 -0700 |
| commit | 9f57f4613dd273b0ef1a531cc72fc418cf4b1af0 (patch) | |
| tree | 3f7ab1a2b1f2a59927de109c51b4d146d2610a45 /src/CMakeLists.txt | |
| parent | e142a47195faba468d523660710bedc05f6591dd (diff) | |
Adds the interface for the CAD-based arithmetic solver. (#4773)
This PR adds some utilities and, most importantly, the interface of the new
CAD-based solver.
The approach is based on https://arxiv.org/pdf/2003.05633.pdf and the code
structure follows the paper rather closely.
Diffstat (limited to 'src/CMakeLists.txt')
| -rw-r--r-- | src/CMakeLists.txt | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 992da9a85..59b559cb2 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -306,6 +306,10 @@ libcvc4_add_sources( theory/arith/linear_equality.h theory/arith/matrix.cpp theory/arith/matrix.h + theory/arith/nl/cad/cdcac.cpp + theory/arith/nl/cad/cdcac.h + theory/arith/nl/cad/cdcac_utils.cpp + theory/arith/nl/cad/cdcac_utils.h theory/arith/nl/cad/constraints.cpp theory/arith/nl/cad/constraints.h theory/arith/nl/cad/projections.cpp |