projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 102b5b2) | patch
Make IAND solver use inference manager. (#5126)
authorGereon Kremer <gereon.kremer@cs.rwth-aachen.de>
Wed, 23 Sep 2020 18:05:06 +0000 (20:05 +0200)
committerGitHub <noreply@github.com>
Wed, 23 Sep 2020 18:05:06 +0000 (20:05 +0200)
commit770d9ae622ec04bc2fbea8356ce11329ed06fa5b
tree0c1fe354fa4b1b7514520d265c9012521c00e4fftree
parent102b5b2ebeea5c0e4e13583c9f8e8ac8b811e264commit | diff
Make IAND solver use inference manager. (#5126)

This PR moves the iand solver (within the nonlinear extension) to use the new inference manager to send lemmas.
src/theory/arith/nl/iand_solver.cpp diff | blob | history
src/theory/arith/nl/iand_solver.h diff | blob | history
src/theory/arith/nl/nonlinear_extension.cpp diff | blob | history
src/theory/arith/nl/nonlinear_extension.h diff | blob | history
src/theory/arith/theory_arith.cpp diff | blob | history