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

author	Aina Niemetz <aina.niemetz@gmail.com>
	Thu, 11 Mar 2021 19:05:58 +0000 (11:05 -0800)
committer	GitHub <noreply@github.com>
	Thu, 11 Mar 2021 19:05:58 +0000 (19:05 +0000)
commit	dc679ed380aabc62aadfbb4033c02c5a27ae903c
tree	eae38a0bcbd56104c4e381e84d7f8c724104d365	tree
parent	c314b0162c7fa089c400e11bd72c4ca24a26c9d0	commit \| diff

Delete Expr layer. (#6117)

56 files changed:

src/CMakeLists.txt		diff \| blob \| history
src/api/cvc4cpp.cpp		diff \| blob \| history
src/api/cvc4cpp.h		diff \| blob \| history
src/expr/CMakeLists.txt		diff \| blob \| history
src/expr/expr_manager_scope.h	[deleted file]	blob \| history
src/expr/expr_manager_template.cpp	[deleted file]	blob \| history
src/expr/expr_manager_template.h	[deleted file]	blob \| history
src/expr/expr_template.cpp	[deleted file]	blob \| history
src/expr/expr_template.h	[deleted file]	blob \| history
src/expr/node.h		diff \| blob \| history
src/expr/node_manager.cpp		diff \| blob \| history
src/expr/node_manager.h		diff \| blob \| history
src/expr/type.cpp	[deleted file]	blob \| history
src/expr/type.h	[deleted file]	blob \| history
src/expr/type_node.h		diff \| blob \| history
src/expr/variable_type_map.h	[deleted file]	blob \| history
src/include/cvc4.h		diff \| blob \| history
src/preprocessing/passes/bv_to_int.cpp		diff \| blob \| history
src/preprocessing/passes/int_to_bv.cpp		diff \| blob \| history
src/preprocessing/passes/real_to_int.cpp		diff \| blob \| history
src/printer/cvc/cvc_printer.cpp		diff \| blob \| history
src/printer/smt2/smt2_printer.cpp		diff \| blob \| history
src/proof/cnf_proof.h		diff \| blob \| history
src/prop/prop_engine.h		diff \| blob \| history
src/smt/assertions.cpp		diff \| blob \| history
src/smt/expand_definitions.cpp		diff \| blob \| history
src/smt/interpolation_solver.cpp		diff \| blob \| history
src/smt/optimization_solver.h		diff \| blob \| history
src/smt/smt_engine.cpp		diff \| blob \| history
src/theory/datatypes/theory_datatypes_type_rules.h		diff \| blob \| history
src/theory/quantifiers/cegqi/ceg_dt_instantiator.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/cegis_core_connective.h		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_grammar_cons.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_grammar_norm.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_process_conj.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/synth_conjecture.cpp		diff \| blob \| history
src/theory/sets/theory_sets_type_rules.h		diff \| blob \| history
src/theory/strings/type_enumerator.cpp		diff \| blob \| history
src/theory/strings/type_enumerator.h		diff \| blob \| history
src/theory/uf/equality_engine.cpp		diff \| blob \| history
src/theory/uf/theory_uf_type_rules.h		diff \| blob \| history
test/api/ouroborous.cpp		diff \| blob \| history
test/api/smt2_compliance.cpp		diff \| blob \| history
test/unit/expr/node_black.cpp		diff \| blob \| history
test/unit/expr/node_traversal_black.cpp		diff \| blob \| history
test/unit/expr/symbol_table_black.cpp		diff \| blob \| history
test/unit/expr/type_cardinality_black.cpp		diff \| blob \| history
test/unit/expr/type_node_white.cpp		diff \| blob \| history
test/unit/main/interactive_shell_black.cpp		diff \| blob \| history
test/unit/parser/parser_black.cpp		diff \| blob \| history
test/unit/test_node.h		diff \| blob \| history
test/unit/test_smt.h		diff \| blob \| history
test/unit/theory/theory_bv_white.cpp		diff \| blob \| history
test/unit/theory/theory_quantifiers_bv_inverter_white.cpp		diff \| blob \| history
test/unit/util/array_store_all_white.cpp		diff \| blob \| history
test/unit/util/datatype_black.cpp		diff \| blob \| history

RSS Atom