1 /********************* */
2 /*! \file sort_infer.cpp
3 ** \verbatim
4 ** Top contributors (to current version):
5 ** Andrew Reynolds, Andres Noetzli
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
8 ** in the top-level source directory) and their institutional affiliations.
9 ** All rights reserved. See the file COPYING in the top-level source
10 ** directory for licensing information.\endverbatim
11 **
12 ** \brief Sort inference preprocessing pass
13 **/
14
15 #include "preprocessing/passes/sort_infer.h"
16
17 #include "options/smt_options.h"
18 #include "options/uf_options.h"
19 #include "theory/rewriter.h"
20 #include "theory/sort_inference.h"
21
22 using namespace std;
23
24 namespace CVC4 {
25 namespace preprocessing {
26 namespace passes {
27
SortInferencePass(PreprocessingPassContext * preprocContext)28 SortInferencePass::SortInferencePass(PreprocessingPassContext* preprocContext)
29 : PreprocessingPass(preprocContext, "sort-inference")
30 {
31 }
32
applyInternal(AssertionPipeline * assertionsToPreprocess)33 PreprocessingPassResult SortInferencePass::applyInternal(
34 AssertionPipeline* assertionsToPreprocess)
35 {
36 SortInference* si = d_preprocContext->getTheoryEngine()->getSortInference();
37
38 if (options::sortInference())
39 {
40 si->initialize(assertionsToPreprocess->ref());
41 std::map<Node, Node> model_replace_f;
42 std::map<Node, std::map<TypeNode, Node> > visited;
43 for (unsigned i = 0, size = assertionsToPreprocess->size(); i < size; i++)
44 {
45 Node prev = (*assertionsToPreprocess)[i];
46 Node next = si->simplify(prev, model_replace_f, visited);
47 if (next != prev)
48 {
49 next = theory::Rewriter::rewrite(next);
50 assertionsToPreprocess->replace(i, next);
51 Trace("sort-infer-preprocess")
52 << "*** Preprocess SortInferencePass " << prev << endl;
53 Trace("sort-infer-preprocess")
54 << " ...got " << (*assertionsToPreprocess)[i] << endl;
55 }
56 }
57 std::vector<Node> newAsserts;
58 si->getNewAssertions(newAsserts);
59 for (const Node& na : newAsserts)
60 {
61 Node nar = theory::Rewriter::rewrite(na);
62 Trace("sort-infer-preprocess")
63 << "*** Preprocess SortInferencePass : new constraint " << nar
64 << endl;
65 assertionsToPreprocess->push_back(nar);
66 }
67 // indicate correspondence between the functions
68 // TODO (#2308): move this to a better place
69 SmtEngine* smt = smt::currentSmtEngine();
70 for (const std::pair<const Node, Node>& mrf : model_replace_f)
71 {
72 smt->setPrintFuncInModel(mrf.first.toExpr(), false);
73 smt->setPrintFuncInModel(mrf.second.toExpr(), true);
74 }
75 }
76 // only need to compute monotonicity on the resulting formula if we are
77 // using this option
78 if (options::ufssFairnessMonotone())
79 {
80 si->computeMonotonicity(assertionsToPreprocess->ref());
81 }
82 return PreprocessingPassResult::NO_CONFLICT;
83 }
84
85
86 } // namespace passes
87 } // namespace preprocessing
88 } // namespace CVC4
89