git.libre-soc.org Git - cvc5.git/commit

author	Aina Niemetz <aina.niemetz@gmail.com>
	Fri, 21 May 2021 00:41:50 +0000 (17:41 -0700)
committer	GitHub <noreply@github.com>
	Fri, 21 May 2021 00:41:50 +0000 (00:41 +0000)
commit	9670dd43576cd21de82e22e76c57e783aa143d21
tree	7a5157afa203bbe0a8755bdb0e178fb993d7e262	tree
parent	9e5f2385b73d55f675fa3996a2dd6df0e8d7652b	commit \| diff

BV: Rename BITVECTOR_PLUS to BITVECTOR_ADD. (#6589)

50 files changed:

examples/api/bitvectors.cpp		diff \| blob \| history
examples/api/java/BitVectors.java		diff \| blob \| history
examples/api/python/bitvectors.py		diff \| blob \| history
src/api/cpp/cvc5.cpp		diff \| blob \| history
src/api/cpp/cvc5_kind.h		diff \| blob \| history
src/api/parsekinds.py		diff \| blob \| history
src/expr/proof_rule.cpp		diff \| blob \| history
src/expr/proof_rule.h		diff \| blob \| history
src/parser/cvc/Cvc.g		diff \| blob \| history
src/parser/smt2/smt2.cpp		diff \| blob \| history
src/preprocessing/passes/bv_gauss.cpp		diff \| blob \| history
src/preprocessing/passes/bv_to_int.cpp		diff \| blob \| history
src/preprocessing/passes/int_to_bv.cpp		diff \| blob \| history
src/preprocessing/passes/unconstrained_simplifier.cpp		diff \| blob \| history
src/printer/cvc/cvc_printer.cpp		diff \| blob \| history
src/printer/smt2/smt2_printer.cpp		diff \| blob \| history
src/smt_util/nary_builder.cpp		diff \| blob \| history
src/theory/bv/bitblast/bitblast_strategies_template.h		diff \| blob \| history
src/theory/bv/bitblast/bitblaster.h		diff \| blob \| history
src/theory/bv/bitblast/proof_bitblaster.cpp		diff \| blob \| history
src/theory/bv/bv_solver_lazy.cpp		diff \| blob \| history
src/theory/bv/bv_subtheory_core.cpp		diff \| blob \| history
src/theory/bv/bv_subtheory_inequality.cpp		diff \| blob \| history
src/theory/bv/kinds		diff \| blob \| history
src/theory/bv/proof_checker.cpp		diff \| blob \| history
src/theory/bv/theory_bv.cpp		diff \| blob \| history
src/theory/bv/theory_bv_rewrite_rules.h		diff \| blob \| history
src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h		diff \| blob \| history
src/theory/bv/theory_bv_rewrite_rules_normalization.h		diff \| blob \| history
src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h		diff \| blob \| history
src/theory/bv/theory_bv_rewrite_rules_simplification.h		diff \| blob \| history
src/theory/bv/theory_bv_rewriter.cpp		diff \| blob \| history
src/theory/bv/theory_bv_rewriter.h		diff \| blob \| history
src/theory/bv/theory_bv_utils.cpp		diff \| blob \| history
src/theory/bv/theory_bv_utils.h		diff \| blob \| history
src/theory/datatypes/sygus_simple_sym.cpp		diff \| blob \| history
src/theory/evaluator.cpp		diff \| blob \| history
src/theory/fp/fp_converter.cpp		diff \| blob \| history
src/theory/quantifiers/bv_inverter.cpp		diff \| blob \| history
src/theory/quantifiers/bv_inverter_utils.cpp		diff \| blob \| history
src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp		diff \| blob \| history
src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.cpp		diff \| blob \| history
src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.h		diff \| blob \| history
src/theory/quantifiers/extended_rewrite.h		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_grammar_cons.cpp		diff \| blob \| history
src/theory/quantifiers/term_util.cpp		diff \| blob \| history
test/unit/preprocessing/pass_bv_gauss_white.cpp		diff \| blob \| history
test/unit/theory/theory_bv_white.cpp		diff \| blob \| history
test/unit/theory/theory_quantifiers_bv_instantiator_white.cpp		diff \| blob \| history
test/unit/theory/theory_quantifiers_bv_inverter_white.cpp		diff \| blob \| history

RSS Atom