projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: be1f030) | patch
Connect the equality solver to theory arith (#6894)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Thu, 15 Jul 2021 15:53:05 +0000 (10:53 -0500)
committerGitHub <noreply@github.com>
Thu, 15 Jul 2021 15:53:05 +0000 (10:53 -0500)
commit31b053a52258bd4697409b92d042a8bebb64f7b2
tree94fb8f70b22c57332ba54b24af5f036cae723654tree
parentbe1f03037110e8334bb2e73e9b6afb76eee959e2commit | diff
Connect the equality solver to theory arith (#6894)

--arith-eq-solver is a new option to enable the equality solver in arithmetic, disabled by default.

This PR connects the equality solver to TheoryArith when this option is enabled.

This is in preparation for the central equality engine.
src/CMakeLists.txt diff | blob | history
src/options/arith_options.toml diff | blob | history
src/theory/arith/theory_arith.cpp diff | blob | history
src/theory/arith/theory_arith.h diff | blob | history