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

author	mudathirmahgoub <mudathirmahgoub@gmail.com>
	Tue, 19 May 2020 21:24:59 +0000 (16:24 -0500)
committer	GitHub <noreply@github.com>
	Tue, 19 May 2020 21:24:59 +0000 (16:24 -0500)
commit	c8f149fa83fa16f821f37687fedfa778808809bd
tree	8808ec522b58c0d8273280923b984a72e0b7bb29	tree
parent	6bb98062a5578d126db6a3e8cdca083881893b32	commit \| diff

Renamed operator CHOICE to WITNESS (#4207)

Renamed operator CHOICE to WITNESS, and removed it from the front end

33 files changed:

src/api/cvc4cpp.cpp		diff \| blob \| history
src/api/cvc4cppkind.h		diff \| blob \| history
src/expr/expr_manager_template.h		diff \| blob \| history
src/expr/node.h		diff \| blob \| history
src/expr/node_algorithm.h		diff \| blob \| history
src/options/smt_options.toml		diff \| blob \| history
src/parser/cvc/Cvc.g		diff \| blob \| history
src/parser/smt2/Smt2.g		diff \| blob \| history
src/parser/tptp/Tptp.g		diff \| blob \| history
src/printer/smt2/smt2_printer.cpp		diff \| blob \| history
src/smt/term_formula_removal.cpp		diff \| blob \| history
src/smt/term_formula_removal.h		diff \| blob \| history
src/theory/arith/nl_model.cpp		diff \| blob \| history
src/theory/arith/theory_arith_private.cpp		diff \| blob \| history
src/theory/builtin/kinds		diff \| blob \| history
src/theory/builtin/theory_builtin.cpp		diff \| blob \| history
src/theory/builtin/theory_builtin_rewriter.cpp		diff \| blob \| history
src/theory/builtin/theory_builtin_type_rules.h		diff \| blob \| history
src/theory/quantifiers/bv_inverter.cpp		diff \| blob \| history
src/theory/quantifiers/bv_inverter.h		diff \| blob \| history
src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp		diff \| blob \| history
src/theory/quantifiers/cegqi/ceg_instantiator.cpp		diff \| blob \| history
src/theory/quantifiers/cegqi/ceg_instantiator.h		diff \| blob \| history
src/theory/quantifiers/fmf/bounded_integers.cpp		diff \| blob \| history
src/theory/quantifiers/fmf/bounded_integers.h		diff \| blob \| history
src/theory/sets/theory_sets_private.cpp		diff \| blob \| history
src/theory/strings/theory_strings.cpp		diff \| blob \| history
src/theory/theory_model.cpp		diff \| blob \| history
test/regress/CMakeLists.txt		diff \| blob \| history
test/regress/regress0/nl/sqrt2-value.smt2		diff \| blob \| history
test/regress/regress0/parser/choice.cvc	[deleted file]	blob \| history
test/regress/regress0/parser/choice.smt2	[deleted file]	blob \| history
test/regress/regress1/nl/issue3300-approx-sqrt-witness.smt2		diff \| blob \| history

RSS Atom