diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-08-03 09:40:52 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-08-03 09:40:52 -0500 |
| commit | 5a3569cbeba6c53c157f4fb8e88016c5a501cafb (patch) | |
| tree | 8ed6fac7663c7ba722236f4b9e8c0d4cefbb4736 /src/preprocessing/passes | |
| parent | 4caca6f74cc23b185757648bbf6f20daa6e78303 (diff) | |
Split dump manager from SmtEngine (#4824)
Towards splitting SmtEngine.
This moves utilities related to managing information for dumping to its own utility, DumpManager.
Its current responsibilities are to track information about how to print a model, and the implementation of some dumping traces, although its responsibilities should be extended further so that SmtEngine is not responsible for any command dumping. This is future work.
Diffstat (limited to 'src/preprocessing/passes')
| -rw-r--r-- | src/preprocessing/passes/sort_infer.cpp | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/src/preprocessing/passes/sort_infer.cpp b/src/preprocessing/passes/sort_infer.cpp index 92c2e55b1..03f0469bf 100644 --- a/src/preprocessing/passes/sort_infer.cpp +++ b/src/preprocessing/passes/sort_infer.cpp @@ -16,6 +16,7 @@ #include "options/smt_options.h" #include "options/uf_options.h" +#include "smt/dump_manager.h" #include "theory/rewriter.h" #include "theory/sort_inference.h" @@ -65,12 +66,12 @@ PreprocessingPassResult SortInferencePass::applyInternal( assertionsToPreprocess->push_back(nar); } // indicate correspondence between the functions - // TODO (#2308): move this to a better place SmtEngine* smt = smt::currentSmtEngine(); + smt::DumpManager* dm = smt->getDumpManager(); for (const std::pair<const Node, Node>& mrf : model_replace_f) { - smt->setPrintFuncInModel(mrf.first.toExpr(), false); - smt->setPrintFuncInModel(mrf.second.toExpr(), true); + dm->setPrintFuncInModel(mrf.first, false); + dm->setPrintFuncInModel(mrf.second, true); } } // only need to compute monotonicity on the resulting formula if we are |