projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 18aef11) | patch
Add skeleton for new Lazard evaluation (#6732)
authorGereon Kremer <nafur42@gmail.com>
Fri, 11 Jun 2021 14:18:45 +0000 (16:18 +0200)
committerGitHub <noreply@github.com>
Fri, 11 Jun 2021 14:18:45 +0000 (14:18 +0000)
commitf10087c3b347da6ef625a2ad92846551ad324d73
treebcdc7d40e2b00761720950bcb4df3e90bb94370ftree
parent18aef1113bbdb5ce8e007d115f032e425ad10797commit | diff
Add skeleton for new Lazard evaluation (#6732)

This PR add the interface and a dummy implementation for the new Lazard evaluation. The dummy implementation is used when CoCoALib is not available and simply falls back to poly::infeasible_regions. The proper implementation that actually does that the comment says will be added with subsequent PRs.
src/CMakeLists.txt diff | blob | history
src/theory/arith/nl/cad/lazard_evaluation.cpp [new file with mode: 0644] blob
src/theory/arith/nl/cad/lazard_evaluation.h [new file with mode: 0644] blob