projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 2e2424a) | patch
Fix compilation without LibPoly (#5118)
authorAndres Noetzli <andres.noetzli@gmail.com>
Tue, 22 Sep 2020 19:13:33 +0000 (12:13 -0700)
committerGitHub <noreply@github.com>
Tue, 22 Sep 2020 19:13:33 +0000 (14:13 -0500)
commit524c879720779abc3bc529459da8734f2eb3e3ad
tree5a14c2502159a646adb7d9be1169110357129b07tree
parent2e2424a1a8ce19a3c4e357cf491ca027a5d1b4cccommit | diff
Fix compilation without LibPoly (#5118)

Commit e969318 introduced the ICP-based
solver for nonlinear arithmetic. That code, however, depends on LibPoly.
When configuring CVC4 without LibPoly, the code doesn't compile because
the class ICPSolver is missing. This commit adds a dummy version if
ICPSolver to remedy the issue.
.github/workflows/ci.yml diff | blob | history
src/theory/arith/nl/icp/icp_solver.cpp diff | blob | history
src/theory/arith/nl/icp/icp_solver.h diff | blob | history