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

author	Mathias Preiner <mathias.preiner@gmail.com>
	Sat, 6 Mar 2021 03:28:19 +0000 (19:28 -0800)
committer	GitHub <noreply@github.com>
	Sat, 6 Mar 2021 03:28:19 +0000 (21:28 -0600)
commit	59d9aad4839e64e0f6d6b57ff112c418ffbbe9fb
tree	d0df100653994157bc631e9ca7fe422dd78e29ff	tree
parent	c6fffe4fd328401f7f7e0757303e8dea5f6c14a4	commit \| diff

Remove partial UDIV/UREM operators. (#6069)

This commit removes the partial UDIV/UREM operator handling. BITVECTOR_UDIV and BITVECTOR_UREM are now total.

28 files changed:

src/api/cvc4cpp.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/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/theory/bv/bitblast/bitblast_strategies_template.h		diff \| blob \| history
src/theory/bv/bitblast/bitblaster.h		diff \| blob \| history
src/theory/bv/bv_solver_lazy.cpp		diff \| blob \| history
src/theory/bv/bv_subtheory_algebraic.cpp		diff \| blob \| history
src/theory/bv/kinds		diff \| blob \| history
src/theory/bv/theory_bv.cpp		diff \| blob \| history
src/theory/bv/theory_bv.h		diff \| blob \| history
src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.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/datatypes/sygus_datatype_utils.cpp		diff \| blob \| history
src/theory/datatypes/sygus_extension.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/sygus/sygus_grammar_cons.cpp		diff \| blob \| history
src/theory/quantifiers/term_util.cpp		diff \| blob \| history
src/theory/subs_minimize.cpp		diff \| blob \| history
test/unit/preprocessing/pass_bv_gauss_white.cpp		diff \| blob \| history
test/unit/theory/theory_quantifiers_bv_inverter_white.cpp		diff \| blob \| history

RSS Atom