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

author	Morgan Deters <mdeters@gmail.com>
	Fri, 24 Aug 2012 23:23:34 +0000 (23:23 +0000)
committer	Morgan Deters <mdeters@gmail.com>
	Fri, 24 Aug 2012 23:23:34 +0000 (23:23 +0000)
commit	80afd586eb0865efcc38aa14833d682f1b7cc27f
tree	aac37b28e0330bf3b72083e979ae94ee71918771	tree
parent	3619c784bd5dd4b91ab0a2ad429ea145636d3424	commit \| diff

* disallow internal uses of mkVar() (you have to mkSkolem())
* add support for mkBoundVar() (BOUND_VAR_LISTs in quantifiers must be bound vars)

28 files changed:

src/compat/cvc3_compat.cpp		diff \| blob \| history
src/expr/expr_manager_template.cpp		diff \| blob \| history
src/expr/expr_manager_template.h		diff \| blob \| history
src/expr/node_manager.h		diff \| blob \| history
src/parser/cvc/Cvc.g		diff \| blob \| history
src/parser/parser.cpp		diff \| blob \| history
src/parser/parser.h		diff \| blob \| history
src/parser/smt/Smt.g		diff \| blob \| history
src/parser/smt2/Smt2.g		diff \| blob \| history
src/parser/tptp/Tptp.g		diff \| blob \| history
src/printer/dagification_visitor.cpp		diff \| blob \| history
src/theory/arith/dio_solver.cpp		diff \| blob \| history
src/theory/arith/theory_arith_instantiator.cpp		diff \| blob \| history
src/theory/arrays/theory_arrays.cpp		diff \| blob \| history
src/theory/arrays/theory_arrays_model.cpp		diff \| blob \| history
src/theory/builtin/kinds		diff \| blob \| history
src/theory/builtin/theory_builtin_type_rules.h		diff \| blob \| history
src/theory/bv/theory_bv_utils.h		diff \| blob \| history
src/theory/ite_simplifier.cpp		diff \| blob \| history
src/theory/model.cpp		diff \| blob \| history
src/theory/quantifiers/quantifiers_rewriter.cpp		diff \| blob \| history
src/theory/quantifiers/term_database.cpp		diff \| blob \| history
src/theory/quantifiers/theory_quantifiers_type_rules.h		diff \| blob \| history
src/theory/uf/theory_uf_strong_solver.cpp		diff \| blob \| history
src/theory/unconstrained_simplifier.cpp		diff \| blob \| history
src/util/datatype.cpp		diff \| blob \| history
src/util/datatype.h		diff \| blob \| history
src/util/ite_removal.cpp		diff \| blob \| history