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

author	Andres Noetzli <andres.noetzli@gmail.com>
	Thu, 16 Aug 2018 23:46:05 +0000 (16:46 -0700)
committer	Andrew Reynolds <andrew.j.reynolds@gmail.com>
	Thu, 16 Aug 2018 23:46:05 +0000 (18:46 -0500)
commit	7fc04bf78c6c20f3711d14425469eef2e0c2cd60
tree	d9f2e91a52406edf66967faccad550631cd9e4a5	tree
parent	4e62cdade61514f268b96e78e2f82ad12dfcad07	commit \| diff

Move node algorithms to separate file (#2311)

32 files changed:

src/expr/Makefile.am		diff \| blob \| history
src/expr/expr_template.cpp		diff \| blob \| history
src/expr/node.cpp		diff \| blob \| history
src/expr/node.h		diff \| blob \| history
src/expr/node_algorithm.cpp	[new file with mode: 0644]	blob
src/expr/node_algorithm.h	[new file with mode: 0644]	blob
src/smt/term_formula_removal.cpp		diff \| blob \| history
src/theory/arith/arith_static_learner.cpp		diff \| blob \| history
src/theory/arith/nonlinear_extension.cpp		diff \| blob \| history
src/theory/arith/theory_arith_private.cpp		diff \| blob \| history
src/theory/arrays/theory_arrays.cpp		diff \| blob \| history
src/theory/booleans/circuit_propagator.cpp		diff \| blob \| history
src/theory/builtin/theory_builtin_rewriter.cpp		diff \| blob \| history
src/theory/bv/bv_subtheory_algebraic.cpp		diff \| blob \| history
src/theory/bv/theory_bv.cpp		diff \| blob \| history
src/theory/bv/theory_bv_rewrite_rules_normalization.h		diff \| blob \| history
src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp		diff \| blob \| history
src/theory/quantifiers/cegqi/ceg_dt_instantiator.cpp		diff \| blob \| history
src/theory/quantifiers/cegqi/ceg_epr_instantiator.cpp		diff \| blob \| history
src/theory/quantifiers/cegqi/ceg_instantiator.cpp		diff \| blob \| history
src/theory/quantifiers/cegqi/inst_strategy_cbqi.cpp		diff \| blob \| history
src/theory/quantifiers/ematching/trigger.cpp		diff \| blob \| history
src/theory/quantifiers/fmf/bounded_integers.cpp		diff \| blob \| history
src/theory/quantifiers/quant_conflict_find.cpp		diff \| blob \| history
src/theory/quantifiers/quantifiers_rewriter.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/ce_guided_single_inv.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp		diff \| blob \| history
src/theory/quantifiers/term_util.cpp		diff \| blob \| history
src/theory/sets/theory_sets_private.cpp		diff \| blob \| history
src/theory/substitutions.cpp		diff \| blob \| history
src/theory/theory.cpp		diff \| blob \| history
src/theory/theory_engine.cpp		diff \| blob \| history

RSS Atom