projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 1cd3c3c) | patch
Use TypeNode in EmptySet (#4740)
authorAndres Noetzli <andres.noetzli@gmail.com>
Tue, 14 Jul 2020 14:33:01 +0000 (07:33 -0700)
committerGitHub <noreply@github.com>
Tue, 14 Jul 2020 14:33:01 +0000 (09:33 -0500)
commitc13527bfa6b47ff4675b429b5e7bb7c6f43ff595
treef182e942b3bc4ad99a8fdf765959781f1a2570ddtree
parent1cd3c3c5dad84093aa6b2db164798c8fff473feccommit | diff
Use TypeNode in EmptySet (#4740)

This commit changes EmptySet to use TypeNode instead of Type.
14 files changed:
src/api/cvc4cpp.cpp diff | blob | history
src/expr/emptyset.cpp diff | blob | history
src/expr/emptyset.h diff | blob | history
src/expr/expr_template.cpp diff | blob | history
src/expr/node_manager.h diff | blob | history
src/theory/sep/theory_sep.cpp diff | blob | history
src/theory/sep/theory_sep_rewriter.cpp diff | blob | history
src/theory/sets/normal_form.h diff | blob | history
src/theory/sets/solver_state.cpp diff | blob | history
src/theory/sets/theory_sets_private.cpp diff | blob | history
src/theory/sets/theory_sets_rewriter.cpp diff | blob | history
src/theory/sets/theory_sets_type_enumerator.cpp diff | blob | history
src/theory/sets/theory_sets_type_rules.h diff | blob | history
test/unit/theory/theory_sets_type_enumerator_white.h diff | blob | history