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

This commit removes the CONST_INTEGER kind from nodes. This code comes from the branch arithmetic/remove_const_int.

18 files changed:

src/compat/cvc3_compat.cpp		diff \| blob \| history
src/expr/pickler.cpp		diff \| blob \| history
src/parser/antlr_input.h		diff \| blob \| history
src/parser/cvc/Cvc.g		diff \| blob \| history
src/printer/cvc/cvc_printer.cpp		diff \| blob \| history
src/printer/smt2/smt2_printer.cpp		diff \| blob \| history
src/smt/smt_engine.cpp		diff \| blob \| history
src/theory/arith/arith_rewriter.cpp		diff \| blob \| history
src/theory/arith/arith_static_learner.cpp		diff \| blob \| history
src/theory/arith/arith_utilities.h		diff \| blob \| history
src/theory/arith/kinds		diff \| blob \| history
src/theory/arith/normal_form.h		diff \| blob \| history
src/theory/arith/theory_arith.cpp		diff \| blob \| history
src/theory/arith/theory_arith_type_rules.h		diff \| blob \| history
test/unit/expr/expr_public.h		diff \| blob \| history
test/unit/expr/node_manager_black.h		diff \| blob \| history
test/unit/expr/node_manager_white.h		diff \| blob \| history
test/unit/expr/node_white.h		diff \| blob \| history