diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2018-08-25 21:09:22 -0700 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-08-25 23:09:22 -0500 |
commit | b70ccff4de0a23bdf11c70002d10a2cc0795a91c (patch) | |
tree | 9898234cdf62e2e58941ba1dd9bed2dca5de8e50 /src/theory/unconstrained_simplifier.h | |
parent | c66033a67511b10b5ee22b7072b9ceab45552a79 (diff) |
Refactor unconstrained simplification pass (#2374)
Diffstat (limited to 'src/theory/unconstrained_simplifier.h')
-rw-r--r-- | src/theory/unconstrained_simplifier.h | 67 |
1 files changed, 0 insertions, 67 deletions
diff --git a/src/theory/unconstrained_simplifier.h b/src/theory/unconstrained_simplifier.h deleted file mode 100644 index b13311e2a..000000000 --- a/src/theory/unconstrained_simplifier.h +++ /dev/null @@ -1,67 +0,0 @@ -/********************* */ -/*! \file unconstrained_simplifier.h - ** \verbatim - ** Top contributors (to current version): - ** Clark Barrett, Tim King - ** 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 Simplifications based on unconstrained variables - ** - ** This module implements a preprocessing phase which replaces certain "unconstrained" expressions - ** by variables. Based on Roberto Bruttomesso's PhD thesis. - **/ - -#include "cvc4_private.h" - -#ifndef __CVC4__UNCONSTRAINED_SIMPLIFIER_H -#define __CVC4__UNCONSTRAINED_SIMPLIFIER_H - -#include <unordered_map> -#include <unordered_set> -#include <utility> -#include <vector> - -#include "expr/node.h" -#include "theory/substitutions.h" -#include "util/statistics_registry.h" - -namespace CVC4 { - -/* Forward Declarations */ -class LogicInfo; - -class UnconstrainedSimplifier { - - /** number of expressions eliminated due to unconstrained simplification */ - IntStat d_numUnconstrainedElim; - - typedef std::unordered_map<TNode, unsigned, TNodeHashFunction> TNodeCountMap; - typedef std::unordered_map<TNode, TNode, TNodeHashFunction> TNodeMap; - typedef std::unordered_set<TNode, TNodeHashFunction> TNodeSet; - - TNodeCountMap d_visited; - TNodeMap d_visitedOnce; - TNodeSet d_unconstrained; - - context::Context* d_context; - theory::SubstitutionMap d_substitutions; - - const LogicInfo& d_logicInfo; - - void visitAll(TNode assertion); - Node newUnconstrainedVar(TypeNode t, TNode var); - void processUnconstrained(); - -public: - UnconstrainedSimplifier(context::Context* context, const LogicInfo& logicInfo); - ~UnconstrainedSimplifier(); - void processAssertions(std::vector<Node>& assertions); -}; - -} - -#endif |