projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 5f7eee9) | patch
Move bv arith conversions to arith (#8945)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Mon, 11 Jul 2022 20:02:59 +0000 (15:02 -0500)
committerGitHub <noreply@github.com>
Mon, 11 Jul 2022 20:02:59 +0000 (15:02 -0500)
commit3c3a730c70623001c93751759aee3ab2b3d6fb07
treee389e242b97e419625a36573b578e53229bd21c7tree
parent5f7eee9f639496ce4959206999f4576a7da32663commit | diff
Move bv arith conversions to arith (#8945)

This is in preparation for lazier handling of bv2nat and int2bv. Our infrastructure in arithmetic is better equipped for doing this.

There are no behavior changes in this PR.
17 files changed:
src/theory/arith/arith_rewriter.cpp diff | blob | history
src/theory/arith/arith_rewriter.h diff | blob | history
src/theory/arith/arith_utilities.cpp diff | blob | history
src/theory/arith/arith_utilities.h diff | blob | history
src/theory/arith/kinds 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/operator_elim.cpp diff | blob | history
src/theory/arith/theory_arith_type_rules.cpp diff | blob | history
src/theory/arith/theory_arith_type_rules.h diff | blob | history
src/theory/bv/kinds diff | blob | history
src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h diff | blob | history
src/theory/bv/theory_bv_rewriter.cpp diff | blob | history
src/theory/bv/theory_bv_type_rules.cpp diff | blob | history
src/theory/bv/theory_bv_type_rules.h diff | blob | history
src/theory/bv/theory_bv_utils.cpp diff | blob | history
src/theory/bv/theory_bv_utils.h diff | blob | history