From 927066eaecfc2c6f00aa1aca695b68e70164aae3 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 20 May 2020 00:05:58 -0500 Subject: [PATCH] Use debug-check-model to enable internal debugging in check-model (#4480) Notice this also updates our regression script to use --debug-check-model, preserving previous behavior. Fixes #4461, fixes #4470, fixes #4471, fixes #4475, fixes #4448, fixes #4466, fixes #4460, fixes #4458, fixes #4455, fixes #4456, fixes #4386, fixes #4385, fixes #4478, fixes #4474. --- src/options/smt_options.toml | 9 ++++++++- src/smt/set_defaults.cpp | 5 +++++ src/smt/smt_engine.cpp | 7 +++++-- src/theory/theory_model_builder.cpp | 2 +- test/regress/run_regression.py | 5 +++-- 5 files changed, 22 insertions(+), 6 deletions(-) diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml index 6ac5b0289..08e6f317c 100644 --- a/src/options/smt_options.toml +++ b/src/options/smt_options.toml @@ -80,9 +80,16 @@ header = "options/smt_options.h" long = "check-models" type = "bool" notifies = ["notifyBeforeSearch"] - read_only = true help = "after SAT/INVALID/UNKNOWN, check that the generated model satisfies user assertions" +[[option]] + name = "debugCheckModels" + category = "regular" + long = "debug-check-models" + type = "bool" + notifies = ["notifyBeforeSearch"] + help = "after SAT/INVALID/UNKNOWN, check that the generated model satisfies user and internal assertions" + [[option]] name = "dumpModels" category = "regular" diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp index 8236486dd..899da4d4a 100644 --- a/src/smt/set_defaults.cpp +++ b/src/smt/set_defaults.cpp @@ -46,6 +46,11 @@ namespace smt { void setDefaults(SmtEngine& smte, LogicInfo& logic) { // implied options + if (options::debugCheckModels()) + { + Notice() << "SmtEngine: setting checkModel" << std::endl; + options::checkModels.set(true); + } if (options::checkModels() || options::dumpModels()) { Notice() << "SmtEngine: setting produceModels" << std::endl; diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index d4e83c672..3c0a2cd8f 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -2514,8 +2514,11 @@ void SmtEngine::checkModel(bool hardFailure) { } // Check individual theory assertions - d_theoryEngine->checkTheoryAssertionsWithModel(hardFailure); - + if (options::debugCheckModels()) + { + d_theoryEngine->checkTheoryAssertionsWithModel(hardFailure); + } + // Output the model Notice() << *m; diff --git a/src/theory/theory_model_builder.cpp b/src/theory/theory_model_builder.cpp index 68ad25490..e829c1db4 100644 --- a/src/theory/theory_model_builder.cpp +++ b/src/theory/theory_model_builder.cpp @@ -1115,7 +1115,7 @@ void TheoryEngineModelBuilder::postProcessModel(bool incomplete, Model* m) TheoryModel* tm = static_cast(m); Assert(tm != nullptr); // debug-check the model if the checkModels() is enabled. - if (options::checkModels()) + if (options::debugCheckModels()) { debugCheckModel(tm); } diff --git a/test/regress/run_regression.py b/test/regress/run_regression.py index 78b4db656..83b9a872e 100755 --- a/test/regress/run_regression.py +++ b/test/regress/run_regression.py @@ -343,9 +343,10 @@ def run_regression(unsat_cores, proofs, dump, use_skip_return_code, wrapper, '--check-synth-sol' not in all_args: extra_command_line_args = ['--check-synth-sol'] if re.search(r'^(sat|invalid|unknown)$', expected_output) and \ + '--no-debug-check-models' not in all_args and \ '--no-check-models' not in all_args and \ - '--check-models' not in all_args: - extra_command_line_args = ['--check-models'] + '--debug-check-models' not in all_args: + extra_command_line_args = ['--debug-check-models'] if proofs and re.search(r'^(unsat|valid)$', expected_output): if '--no-check-proofs' not in all_args and \ '--check-proofs' not in all_args and \ -- 2.30.2