1 /********************* */
2 /*! \file unconstrained_simplifier.h
4 ** Top contributors (to current version):
5 ** Clark Barrett, Andres Noetzli, Andrew Reynolds
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2020 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
12 ** \brief Simplifications based on unconstrained variables
14 ** This module implements a preprocessing phase which replaces certain
15 ** "unconstrained" expressions by variables. Based on Roberto
16 ** Bruttomesso's PhD thesis.
19 #include "cvc4_private.h"
21 #ifndef CVC4__PREPROCESSING_PASSES_UNCONSTRAINED_SIMPLIFIER_H
22 #define CVC4__PREPROCESSING_PASSES_UNCONSTRAINED_SIMPLIFIER_H
24 #include <unordered_map>
25 #include <unordered_set>
28 #include "context/context.h"
29 #include "expr/node.h"
30 #include "preprocessing/preprocessing_pass.h"
31 #include "preprocessing/preprocessing_pass_context.h"
32 #include "theory/logic_info.h"
33 #include "theory/substitutions.h"
34 #include "util/statistics_registry.h"
37 namespace preprocessing
{
40 class UnconstrainedSimplifier
: public PreprocessingPass
43 UnconstrainedSimplifier(PreprocessingPassContext
* preprocContext
);
44 ~UnconstrainedSimplifier() override
;
46 PreprocessingPassResult
applyInternal(
47 AssertionPipeline
* assertionsToPreprocess
) override
;
50 /** number of expressions eliminated due to unconstrained simplification */
51 IntStat d_numUnconstrainedElim
;
53 using TNodeCountMap
= std::unordered_map
<TNode
, unsigned, TNodeHashFunction
>;
54 using TNodeMap
= std::unordered_map
<TNode
, TNode
, TNodeHashFunction
>;
55 using TNodeSet
= std::unordered_set
<TNode
, TNodeHashFunction
>;
57 TNodeCountMap d_visited
;
58 TNodeMap d_visitedOnce
;
59 TNodeSet d_unconstrained
;
61 context::Context
* d_context
;
62 theory::SubstitutionMap d_substitutions
;
65 * Visit all subterms in assertion. This method throws a LogicException if
66 * there is a subterm that is unhandled by this preprocessing pass (e.g. a
67 * quantified formula).
69 void visitAll(TNode assertion
);
70 Node
newUnconstrainedVar(TypeNode t
, TNode var
);
71 void processUnconstrained();
75 } // namespace preprocessing