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

author	Andrew Reynolds <andrew.j.reynolds@gmail.com>
	Thu, 8 Apr 2021 14:15:31 +0000 (09:15 -0500)
committer	GitHub <noreply@github.com>
	Thu, 8 Apr 2021 14:15:31 +0000 (14:15 +0000)
commit	cd8fd2e4909513b4253ce8f9aa272eb87ae6bf83
tree	713ef362a026a676363894277219a54658a9e05e	tree
parent	889daf13112f71b6f5dd98444af99ec7656195be	commit \| diff

Add identifiers for sources of incompleteness (#6311)

This PR classifies all internal kinds of incompleteness as identifiers.

It makes it so TheoryEngine records an identifier when its incomplete flag is set.

The next step will be to possibly communicate this value to the user.

34 files changed:

src/CMakeLists.txt		diff \| blob \| history
src/theory/arith/nl/nonlinear_extension.cpp		diff \| blob \| history
src/theory/arith/theory_arith.cpp		diff \| blob \| history
src/theory/engine_output_channel.cpp		diff \| blob \| history
src/theory/engine_output_channel.h		diff \| blob \| history
src/theory/incomplete_id.cpp	[new file with mode: 0644]	blob
src/theory/incomplete_id.h	[new file with mode: 0644]	blob
src/theory/inference_id.h		diff \| blob \| history
src/theory/output_channel.h		diff \| blob \| history
src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp		diff \| blob \| history
src/theory/quantifiers/cegqi/inst_strategy_cegqi.h		diff \| blob \| history
src/theory/quantifiers/fmf/model_engine.cpp		diff \| blob \| history
src/theory/quantifiers/fmf/model_engine.h		diff \| blob \| history
src/theory/quantifiers/instantiate.cpp		diff \| blob \| history
src/theory/quantifiers/instantiate.h		diff \| blob \| history
src/theory/quantifiers/quant_module.h		diff \| blob \| history
src/theory/quantifiers/quant_util.h		diff \| blob \| history
src/theory/quantifiers/sygus/synth_conjecture.cpp		diff \| blob \| history
src/theory/quantifiers_engine.cpp		diff \| blob \| history
src/theory/sep/theory_sep.cpp		diff \| blob \| history
src/theory/sets/theory_sets_private.cpp		diff \| blob \| history
src/theory/sets/theory_sets_private.h		diff \| blob \| history
src/theory/strings/core_solver.cpp		diff \| blob \| history
src/theory/strings/inference_manager.cpp		diff \| blob \| history
src/theory/strings/inference_manager.h		diff \| blob \| history
src/theory/strings/regexp_solver.cpp		diff \| blob \| history
src/theory/theory_engine.cpp		diff \| blob \| history
src/theory/theory_engine.h		diff \| blob \| history
src/theory/theory_inference_manager.cpp		diff \| blob \| history
src/theory/theory_inference_manager.h		diff \| blob \| history
src/theory/uf/cardinality_extension.cpp		diff \| blob \| history
src/theory/uf/ho_extension.cpp		diff \| blob \| history
src/theory/uf/theory_uf.cpp		diff \| blob \| history
test/unit/test_smt.h		diff \| blob \| history

RSS Atom