diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-05-20 00:05:58 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-05-20 00:05:58 -0500 |
commit | 927066eaecfc2c6f00aa1aca695b68e70164aae3 (patch) | |
tree | 7456a1ec973f80aa806b66a8a2c6b6a8dfc3b4ba /src | |
parent | 7b4084440bd9dde894ff46c2ba0197fed41d91d1 (diff) |
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.
Diffstat (limited to 'src')
-rw-r--r-- | src/options/smt_options.toml | 9 | ||||
-rw-r--r-- | src/smt/set_defaults.cpp | 5 | ||||
-rw-r--r-- | src/smt/smt_engine.cpp | 7 | ||||
-rw-r--r-- | src/theory/theory_model_builder.cpp | 2 |
4 files changed, 19 insertions, 4 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,10 +80,17 @@ 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" long = "dump-models" 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<TheoryModel*>(m); Assert(tm != nullptr); // debug-check the model if the checkModels() is enabled. - if (options::checkModels()) + if (options::debugCheckModels()) { debugCheckModel(tm); } |