Add identifiers for sources of incompleteness (#6311)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Thu, 8 Apr 2021 14:15:31 +0000 (09:15 -0500)
committerGitHub <noreply@github.com>
Thu, 8 Apr 2021 14:15:31 +0000 (14:15 +0000)
commitcd8fd2e4909513b4253ce8f9aa272eb87ae6bf83
tree713ef362a026a676363894277219a54658a9e05e
parent889daf13112f71b6f5dd98444af99ec7656195be
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
src/theory/arith/nl/nonlinear_extension.cpp
src/theory/arith/theory_arith.cpp
src/theory/engine_output_channel.cpp
src/theory/engine_output_channel.h
src/theory/incomplete_id.cpp [new file with mode: 0644]
src/theory/incomplete_id.h [new file with mode: 0644]
src/theory/inference_id.h
src/theory/output_channel.h
src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
src/theory/quantifiers/cegqi/inst_strategy_cegqi.h
src/theory/quantifiers/fmf/model_engine.cpp
src/theory/quantifiers/fmf/model_engine.h
src/theory/quantifiers/instantiate.cpp
src/theory/quantifiers/instantiate.h
src/theory/quantifiers/quant_module.h
src/theory/quantifiers/quant_util.h
src/theory/quantifiers/sygus/synth_conjecture.cpp
src/theory/quantifiers_engine.cpp
src/theory/sep/theory_sep.cpp
src/theory/sets/theory_sets_private.cpp
src/theory/sets/theory_sets_private.h
src/theory/strings/core_solver.cpp
src/theory/strings/inference_manager.cpp
src/theory/strings/inference_manager.h
src/theory/strings/regexp_solver.cpp
src/theory/theory_engine.cpp
src/theory/theory_engine.h
src/theory/theory_inference_manager.cpp
src/theory/theory_inference_manager.h
src/theory/uf/cardinality_extension.cpp
src/theory/uf/ho_extension.cpp
src/theory/uf/theory_uf.cpp
test/unit/test_smt.h