projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 3f02c93) | patch
Preparation for making equality strictly typed (#8728)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Thu, 5 May 2022 19:13:41 +0000 (14:13 -0500)
committerGitHub <noreply@github.com>
Thu, 5 May 2022 19:13:41 +0000 (19:13 +0000)
commit3266c58ad0ad1c1e3b04a69ceb1caf2a468597db
tree40ac13212fd8c943f196a8b5625b786253f65e7btree
parent3f02c9363244ea92754dc72b8b7c6f5523ce0279commit | diff
Preparation for making equality strictly typed (#8728)

This changes several places in arithmetic so that it never generates equalities between and an Int and a Real.

It also changes several uses of mkConstReal on integer values with mkConstInt whenever their type does not matter.

Since we do not construct CONST_INTEGER yet, this PR has no behavior change yet.
19 files changed:
src/smt/proof_post_processor.cpp diff | blob | history
src/theory/arith/arith_msum.cpp diff | blob | history
src/theory/arith/arith_utilities.cpp diff | blob | history
src/theory/arith/arith_utilities.h diff | blob | history
src/theory/arith/bound_inference.cpp diff | blob | history
src/theory/arith/linear/normal_form.cpp diff | blob | history
src/theory/arith/linear/normal_form.h diff | blob | history
src/theory/arith/nl/ext/ext_state.cpp diff | blob | history
src/theory/arith/nl/ext/factoring_check.cpp diff | blob | history
src/theory/arith/nl/ext/monomial_check.cpp 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/nl/pow2_solver.cpp diff | blob | history
src/theory/arith/nl/transcendental/exponential_solver.cpp diff | blob | history
src/theory/arith/nl/transcendental/proof_checker.cpp diff | blob | history
src/theory/arith/nl/transcendental/transcendental_state.cpp diff | blob | history
src/theory/arith/operator_elim.cpp diff | blob | history
src/theory/arith/proof_checker.cpp diff | blob | history
src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp diff | blob | history