projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 74acadc) | patch
More updates to arithmetic in preparation for central equality engine (#6927)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Mon, 26 Jul 2021 18:26:55 +0000 (13:26 -0500)
committerGitHub <noreply@github.com>
Mon, 26 Jul 2021 18:26:55 +0000 (13:26 -0500)
commite4e19cd62b3eebed2de5b9b627509df0ffec23e1
treea1f56cfa02319fa724acb07490ac2f9ed8fabdedtree
parent74acadc8e7aebd9cd7d41bed64d67e42f45de640commit | diff
More updates to arithmetic in preparation for central equality engine (#6927)

Makes arithEqSolver more robust to propagations from multiple sources, changes the default relationship to congruence manager based on preliminary results on SMT-LIB.
src/options/arith_options.toml diff | blob | history
src/smt/set_defaults.cpp diff | blob | history
src/theory/arith/equality_solver.cpp diff | blob | history
src/theory/arith/inference_manager.cpp diff | blob | history
src/theory/arith/inference_manager.h diff | blob | history
src/theory/arith/theory_arith_private.cpp diff | blob | history
src/theory/theory_inference_manager.h diff | blob | history