projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: bfb744a) | patch
Use arith::InferenceManager for CAD lemmas (#5015)
authorGereon Kremer <gereon.kremer@cs.rwth-aachen.de>
Fri, 4 Sep 2020 14:59:49 +0000 (16:59 +0200)
committerGitHub <noreply@github.com>
Fri, 4 Sep 2020 14:59:49 +0000 (09:59 -0500)
commit0d0c1cdbce4fb46ad5c7d4bc620b712ea014722e
tree5fa7c5d06cbf0a67541c5bdbc82bf692f5d1dd48tree
parentbfb744af4f932f095640d97be8f0bfa9ff60e981commit | diff
Use arith::InferenceManager for CAD lemmas (#5015)

This makes the CAD solver use the new arith::InferenceManager instead of the previously used lemma collection scheme.
src/theory/arith/inference_manager.cpp diff | blob | history
src/theory/arith/inference_manager.h diff | blob | history
src/theory/arith/nl/cad_solver.cpp diff | blob | history
src/theory/arith/nl/cad_solver.h diff | blob | history
src/theory/arith/nl/nonlinear_extension.cpp diff | blob | history
src/theory/sets/cardinality_extension.cpp diff | blob | history
src/theory/sets/theory_sets_private.cpp diff | blob | history
src/theory/theory_inference_manager.cpp diff | blob | history
src/theory/theory_inference_manager.h diff | blob | history