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

author	Morgan Deters <mdeters@gmail.com>
	Fri, 3 Aug 2012 20:39:25 +0000 (20:39 +0000)
committer	Morgan Deters <mdeters@gmail.com>
	Fri, 3 Aug 2012 20:39:25 +0000 (20:39 +0000)
commit	3daaecd22fe5f6147cb08e5a4e08177b33a2daa2
tree	46cb65c3673a5678a7779ff970aea9460233f1f1	tree
parent	e26a44d5f98a9953dffeb07b29a21e7efd501684	commit \| diff

fix uses of getMetaKind() from outside the expr package. (they now use isConst() and isVar() as appropriate)

also some base infrastructure for the new ::isConst().

32 files changed:

src/expr/expr_template.cpp		diff \| blob \| history
src/expr/mkexpr		diff \| blob \| history
src/expr/mkkind		diff \| blob \| history
src/expr/mkmetakind		diff \| blob \| history
src/expr/node.h		diff \| blob \| history
src/expr/node_manager.h		diff \| blob \| history
src/expr/type_checker.h		diff \| blob \| history
src/expr/type_checker_template.cpp		diff \| blob \| history
src/printer/cvc/cvc_printer.cpp		diff \| blob \| history
src/printer/dagification_visitor.cpp		diff \| blob \| history
src/printer/smt2/smt2_printer.cpp		diff \| blob \| history
src/prop/cnf_stream.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/normal_form.h		diff \| blob \| history
src/theory/arith/theory_arith.cpp		diff \| blob \| history
src/theory/arrays/theory_arrays.cpp		diff \| blob \| history
src/theory/booleans/circuit_propagator.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/mkinstantiator		diff \| blob \| history
src/theory/mkrewriter		diff \| blob \| history
src/theory/mktheorytraits		diff \| blob \| history
src/theory/model.cpp		diff \| blob \| history
src/theory/quantifiers/first_order_model.cpp		diff \| blob \| history
src/theory/quantifiers/rep_set_iterator.cpp		diff \| blob \| history
src/theory/theory.cpp		diff \| blob \| history
src/theory/theory.h		diff \| blob \| history
src/theory/uf/symmetry_breaker.cpp		diff \| blob \| history
src/util/boolean_simplification.cpp		diff \| blob \| history
src/util/boolean_simplification.h		diff \| blob \| history

RSS Atom