projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 3fb45e0) | patch
pow2: adding a kind, inference rules, and some implementations in the pow2 solver...
authoryoni206 <yoni206@users.noreply.github.com>
Tue, 15 Jun 2021 22:44:52 +0000 (15:44 -0700)
committerGitHub <noreply@github.com>
Tue, 15 Jun 2021 22:44:52 +0000 (22:44 +0000)
commit4ca14e808d788ef9570dda1188645783c6a11e70
treeda87ecaf3a9aa5d789eebda94923829652fff935tree
parent3fb45e059eff665ed5aaf23915f3434db1e60299commit | diff
pow2: adding a kind, inference rules, and some implementations in the pow2 solver (#6736)

This PR is the sequel of #6676 .
It adds the `POW2` kind, inference rules that will be used in the `pow2` solver, an implementation of one function of the solver, as well as stubs for the others. The next PR will include more implementations.
src/CMakeLists.txt diff | blob | history
src/api/cpp/cvc5_kind.h diff | blob | history
src/theory/arith/kinds diff | blob | history
src/theory/arith/nl/pow2_solver.cpp [new file with mode: 0644] blob
src/theory/inference_id.cpp diff | blob | history
src/theory/inference_id.h diff | blob | history