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

author	mudathirmahgoub <mudathirmahgoub@gmail.com>
	Tue, 22 Sep 2020 21:59:41 +0000 (16:59 -0500)
committer	GitHub <noreply@github.com>
	Tue, 22 Sep 2020 21:59:41 +0000 (16:59 -0500)
commit	e4a29a6033ecc7ba5ec266f37e8f151f09ead020
tree	26dff55bd5121dc311185dcd3071a6e8751f9f5e	tree
parent	524c879720779abc3bc529459da8734f2eb3e3ad	commit \| diff

Add skeleton for theory of bags (multisets) (#5100)

This PR adds initial headers and mostly empty source files for the theory of bags (multisets).
It acts as a basis for future commits.
It includes straightforward implementation for typing rules an enumerator for bags.

42 files changed:

src/CMakeLists.txt		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/expr/CMakeLists.txt		diff \| blob \| history
src/expr/emptybag.cpp	[new file with mode: 0644]	blob
src/expr/emptybag.h	[new file with mode: 0644]	blob
src/expr/node_manager.cpp		diff \| blob \| history
src/expr/node_manager.h		diff \| blob \| history
src/expr/type_node.cpp		diff \| blob \| history
src/expr/type_node.h		diff \| blob \| history
src/parser/parser.cpp		diff \| blob \| history
src/parser/parser.h		diff \| blob \| history
src/parser/smt2/Smt2.g		diff \| blob \| history
src/parser/smt2/smt2.cpp		diff \| blob \| history
src/printer/smt2/smt2_printer.cpp		diff \| blob \| history
src/smt/set_defaults.cpp		diff \| blob \| history
src/theory/bags/inference_manager.cpp	[new file with mode: 0644]	blob
src/theory/bags/inference_manager.h	[new file with mode: 0644]	blob
src/theory/bags/kinds	[new file with mode: 0644]	blob
src/theory/bags/normal_form.cpp	[new file with mode: 0644]	blob
src/theory/bags/normal_form.h	[new file with mode: 0644]	blob
src/theory/bags/solver_state.cpp	[new file with mode: 0644]	blob
src/theory/bags/solver_state.h	[new file with mode: 0644]	blob
src/theory/bags/term_registry.cpp	[new file with mode: 0644]	blob
src/theory/bags/term_registry.h	[new file with mode: 0644]	blob
src/theory/bags/theory_bags.cpp	[new file with mode: 0644]	blob
src/theory/bags/theory_bags.h	[new file with mode: 0644]	blob
src/theory/bags/theory_bags_rewriter.cpp	[new file with mode: 0644]	blob
src/theory/bags/theory_bags_rewriter.h	[new file with mode: 0644]	blob
src/theory/bags/theory_bags_type_enumerator.cpp	[new file with mode: 0644]	blob
src/theory/bags/theory_bags_type_enumerator.h	[new file with mode: 0644]	blob
src/theory/bags/theory_bags_type_rules.h	[new file with mode: 0644]	blob
src/theory/logic_info.cpp		diff \| blob \| history
src/theory/theory_engine.cpp		diff \| blob \| history
src/theory/theory_id.cpp		diff \| blob \| history
src/theory/theory_id.h		diff \| blob \| history
test/unit/api/solver_black.h		diff \| blob \| history
test/unit/api/sort_black.h		diff \| blob \| history
test/unit/theory/CMakeLists.txt		diff \| blob \| history
test/unit/theory/logic_info_white.h		diff \| blob \| history
test/unit/theory/theory_bags_type_rules_black.h	[new file with mode: 0644]	blob

RSS Atom