projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: da087b4) | patch
Eliminating some uses of const rational in arithmetic (#7846)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Mon, 20 Dec 2021 19:10:30 +0000 (13:10 -0600)
committerGitHub <noreply@github.com>
Mon, 20 Dec 2021 19:10:30 +0000 (19:10 +0000)
commit32347c2043d60dc83cd2a5675d3f7796a42022a2
treeef985386260522210ac524ddd410c5f834b56d87tree
parentda087b4f6cc677261961f5ea8a7c5b08b02060c7commit | diff
Eliminating some uses of const rational in arithmetic (#7846)

Note that there are several nested dependencies in arithmetic for constructing constants Constant::mkConstant ---> mkRationalNode ---> mkConst(CONST_RATIONAL, r)

This starts to disambiguate these calls.
src/preprocessing/passes/pseudo_boolean_processor.cpp diff | blob | history
src/theory/arith/arith_rewriter.cpp diff | blob | history
src/theory/arith/branch_and_bound.cpp diff | blob | history
src/theory/arith/dio_solver.cpp diff | blob | history
src/theory/arith/nl/transcendental/sine_solver.cpp diff | blob | history
src/theory/arith/operator_elim.cpp diff | blob | history