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

author	Aina Niemetz <aina.niemetz@gmail.com>
	Fri, 26 Apr 2019 01:02:57 +0000 (18:02 -0700)
committer	GitHub <noreply@github.com>
	Fri, 26 Apr 2019 01:02:57 +0000 (18:02 -0700)
commit	78ae0a579b91af102b48f7ac1db60afc09ccf727
tree	148a067616aa4168047859e331c70f39f0ba91fc	tree
parent	caf32b8e9940e90cd0bfe2e029b4a55c6e601f31	commit \| diff

New C++ API: Clean up API: mkVar vs mkConst vs mkBoundVar. (#2977)

This cleans up naming of API functions to create first-order constants and variables.

mkVar -> mkConst
mkBoundVar -> mkVar
declareConst is redundant (= mkConst) and thus, in an effort to avoid redundancy, removed.

Note that we want to avoid redundancy in order to reduce code duplication and maintenance
overhead (we do not allow nested API calls, since this is problematic when tracing API calls).

13 files changed:

RSS Atom

examples/api/bitvectors-new.cpp		diff \| blob \| history
examples/api/bitvectors_and_arrays-new.cpp		diff \| blob \| history
examples/api/combination-new.cpp		diff \| blob \| history
examples/api/datatypes-new.cpp		diff \| blob \| history
examples/api/extract-new.cpp		diff \| blob \| history
examples/api/linear_arith-new.cpp		diff \| blob \| history
examples/api/sets-new.cpp		diff \| blob \| history
examples/api/strings-new.cpp		diff \| blob \| history
src/api/cvc4cpp.cpp		diff \| blob \| history
src/api/cvc4cpp.h		diff \| blob \| history
src/api/cvc4cppkind.h		diff \| blob \| history
src/parser/smt2/Smt2.g		diff \| blob \| history
test/unit/api/solver_black.h		diff \| blob \| history