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

author	Andrew Reynolds <andrew.j.reynolds@gmail.com>
	Mon, 12 Apr 2021 21:55:44 +0000 (16:55 -0500)
committer	GitHub <noreply@github.com>
	Mon, 12 Apr 2021 21:55:44 +0000 (21:55 +0000)
commit	76f495646c0e3a95f2474c5d746bc61ece18f89f
tree	5390007f4be229dfb18e641f34b9d9df6a9dea92	tree
parent	af398235ef9f3a909991fddbb71d43434d6cf3a1	commit \| diff

Fix computation of whether a type is finite (#6312)

This PR generalizes TypeNode::isFinite / TypeNode::isInterpretedFinite with TypeNode::getCardinalityClass. It then uses this method to fix our computation of when a type should be treated as finite.

Fixes #4260, fixes #6100 (that benchmark now says unknown without an error).

31 files changed:

src/api/cpp/cvc5.cpp		diff \| blob \| history
src/expr/dtype.cpp		diff \| blob \| history
src/expr/dtype.h		diff \| blob \| history
src/expr/dtype_cons.cpp		diff \| blob \| history
src/expr/dtype_cons.h		diff \| blob \| history
src/expr/type_node.cpp		diff \| blob \| history
src/expr/type_node.h		diff \| blob \| history
src/theory/datatypes/sygus_extension.cpp		diff \| blob \| history
src/theory/datatypes/theory_datatypes.cpp		diff \| blob \| history
src/theory/datatypes/type_enumerator.cpp		diff \| blob \| history
src/theory/datatypes/type_enumerator.h		diff \| blob \| history
src/theory/quantifiers/fmf/bounded_integers.cpp		diff \| blob \| history
src/theory/quantifiers/fmf/model_engine.cpp		diff \| blob \| history
src/theory/quantifiers/quant_bound_inference.cpp		diff \| blob \| history
src/theory/quantifiers/quant_split.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_enumerator.cpp		diff \| blob \| history
src/theory/sep/theory_sep.cpp		diff \| blob \| history
src/theory/sets/cardinality_extension.cpp		diff \| blob \| history
src/theory/strings/base_solver.cpp		diff \| blob \| history
src/theory/term_registration_visitor.cpp		diff \| blob \| history
src/theory/theory_engine.cpp		diff \| blob \| history
src/theory/theory_engine.h		diff \| blob \| history
src/theory/theory_model_builder.cpp		diff \| blob \| history
src/theory/theory_model_builder.h		diff \| blob \| history
src/theory/theory_state.cpp		diff \| blob \| history
src/theory/theory_state.h		diff \| blob \| history
src/theory/uf/ho_extension.cpp		diff \| blob \| history
src/theory/valuation.cpp		diff \| blob \| history
src/theory/valuation.h		diff \| blob \| history
src/util/CMakeLists.txt		diff \| blob \| history
test/regress/regress0/fmf/issue4260-arrays-card-one.smt2	[new file with mode: 0644]	blob

RSS Atom