diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-08-15 13:02:46 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-08-15 13:02:46 -0500 |
commit | 4748af3ee298ce5aae36a8ab8cad4426d1398c17 (patch) | |
tree | 94ce5eb140a1f5898b9145a9ecc1ebe92b0ced0e /src/preprocessing/passes | |
parent | e09be1045fc6cc8c5373f9eb96137add66b8d5d5 (diff) |
Make sort inference a preprocessing pass (#2309)
Diffstat (limited to 'src/preprocessing/passes')
-rw-r--r-- | src/preprocessing/passes/sort_infer.cpp | 85 | ||||
-rw-r--r-- | src/preprocessing/passes/sort_infer.h | 58 |
2 files changed, 143 insertions, 0 deletions
diff --git a/src/preprocessing/passes/sort_infer.cpp b/src/preprocessing/passes/sort_infer.cpp new file mode 100644 index 000000000..e2b0bfb59 --- /dev/null +++ b/src/preprocessing/passes/sort_infer.cpp @@ -0,0 +1,85 @@ +/********************* */ +/*! \file sort_infer.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Sort inference preprocessing pass + **/ + +#include "preprocessing/passes/sort_infer.h" + +#include "options/smt_options.h" +#include "options/uf_options.h" +#include "theory/rewriter.h" + +using namespace std; + +namespace CVC4 { +namespace preprocessing { +namespace passes { + +SortInferencePass::SortInferencePass(PreprocessingPassContext* preprocContext, + SortInference* si) + : PreprocessingPass(preprocContext, "sort-inference"), d_si(si) +{ +} + +PreprocessingPassResult SortInferencePass::applyInternal( + AssertionPipeline* assertionsToPreprocess) +{ + if (options::sortInference()) + { + d_si->initialize(assertionsToPreprocess->ref()); + std::map<Node, Node> model_replace_f; + std::map<Node, std::map<TypeNode, Node> > visited; + for (unsigned i = 0, size = assertionsToPreprocess->size(); i < size; i++) + { + Node prev = (*assertionsToPreprocess)[i]; + Node next = d_si->simplify(prev, model_replace_f, visited); + if (next != prev) + { + next = theory::Rewriter::rewrite(next); + assertionsToPreprocess->replace(i, next); + Trace("sort-infer-preprocess") + << "*** Preprocess SortInferencePass " << prev << endl; + Trace("sort-infer-preprocess") + << " ...got " << (*assertionsToPreprocess)[i] << endl; + } + } + std::vector<Node> newAsserts; + d_si->getNewAssertions(newAsserts); + for (const Node& na : newAsserts) + { + Node nar = theory::Rewriter::rewrite(na); + Trace("sort-infer-preprocess") + << "*** Preprocess SortInferencePass : new constraint " << nar + << endl; + assertionsToPreprocess->push_back(nar); + } + // indicate correspondence between the functions + // TODO (#2308): move this to a better place + SmtEngine* smt = smt::currentSmtEngine(); + for (const std::pair<const Node, Node>& mrf : model_replace_f) + { + smt->setPrintFuncInModel(mrf.first.toExpr(), false); + smt->setPrintFuncInModel(mrf.second.toExpr(), true); + } + } + // only need to compute monotonicity on the resulting formula if we are + // using this option + if (options::ufssFairnessMonotone()) + { + d_si->computeMonotonicity(assertionsToPreprocess->ref()); + } + return PreprocessingPassResult::NO_CONFLICT; +} + +} // namespace passes +} // namespace preprocessing +} // namespace CVC4 diff --git a/src/preprocessing/passes/sort_infer.h b/src/preprocessing/passes/sort_infer.h new file mode 100644 index 000000000..e56d7ab60 --- /dev/null +++ b/src/preprocessing/passes/sort_infer.h @@ -0,0 +1,58 @@ +/********************* */ +/*! \file sort_infer.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Sort inference preprocessing pass + **/ + +#ifndef __CVC4__PREPROCESSING__PASSES__SORT_INFERENCE_PASS_H_ +#define __CVC4__PREPROCESSING__PASSES__SORT_INFERENCE_PASS_H_ + +#include <map> +#include <string> +#include <vector> +#include "expr/node.h" + +#include "preprocessing/preprocessing_pass.h" +#include "preprocessing/preprocessing_pass_context.h" +#include "theory/sort_inference.h" + +namespace CVC4 { +namespace preprocessing { +namespace passes { + +/** SortInferencePass + * + * This preprocessing pass runs sort inference techniques on the input formula. + * For details on these techniques, see theory/sort_inference.h. + */ +class SortInferencePass : public PreprocessingPass +{ + public: + SortInferencePass(PreprocessingPassContext* preprocContext, + SortInference* si); + + protected: + PreprocessingPassResult applyInternal( + AssertionPipeline* assertionsToPreprocess) override; + + private: + /** + * Pointer to the sort inference module. This should be the sort inference + * belonging to the theory engine of the current SMT engine. + */ + SortInference* d_si; +}; + +} // namespace passes +} // namespace preprocessing +} // namespace CVC4 + +#endif /* __CVC4__PREPROCESSING__PASSES__SORT_INFERENCE_PASS_H_ */ |