diff options
Diffstat (limited to 'src/preprocessing/util/ite_utilities.h')
| -rw-r--r-- | src/preprocessing/util/ite_utilities.h | 420 |
1 files changed, 420 insertions, 0 deletions
diff --git a/src/preprocessing/util/ite_utilities.h b/src/preprocessing/util/ite_utilities.h new file mode 100644 index 000000000..e137749db --- /dev/null +++ b/src/preprocessing/util/ite_utilities.h @@ -0,0 +1,420 @@ +/********************* */ +/*! \file ite_utilities.h + ** \verbatim + ** Top contributors (to current version): + ** Tim King, Aina Niemetz, Paul Meng + ** 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 for ITE expressions + ** + ** This module implements preprocessing phases designed to simplify ITE + ** expressions. Based on: + ** Kim, Somenzi, Jin. Efficient Term-ITE Conversion for SMT. FMCAD 2009. + ** Burch, Jerry. Techniques for Verifying Superscalar Microprocessors. DAC + *'96 + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__ITE_UTILITIES_H +#define __CVC4__ITE_UTILITIES_H + +#include <unordered_map> +#include <vector> + +#include "expr/node.h" +#include "util/hash.h" +#include "util/statistics_registry.h" + +namespace CVC4 { +namespace preprocessing { +namespace util { + +class IncomingArcCounter; +class TermITEHeightCounter; +class ITECompressor; +class ITESimplifier; +class ITECareSimplifier; + +/** + * A caching visitor that computes whether a node contains a term ite. + */ +class ContainsTermITEVisitor +{ + public: + ContainsTermITEVisitor(); + ~ContainsTermITEVisitor(); + + /** returns true if a node contains a term ite. */ + bool containsTermITE(TNode n); + + /** Garbage collects the cache. */ + void garbageCollect(); + + /** returns the size of the cache. */ + size_t cache_size() const { return d_cache.size(); } + + private: + typedef std::unordered_map<Node, bool, NodeHashFunction> NodeBoolMap; + NodeBoolMap d_cache; +}; + +class ITEUtilities +{ + public: + ITEUtilities(); + ~ITEUtilities(); + + Node simpITE(TNode assertion); + + bool simpIteDidALotOfWorkHeuristic() const; + + /* returns false if an assertion is discovered to be equal to false. */ + bool compress(std::vector<Node>& assertions); + + Node simplifyWithCare(TNode e); + + void clear(); + + ContainsTermITEVisitor* getContainsVisitor() + { + return d_containsVisitor.get(); + } + + bool containsTermITE(TNode n) + { + return d_containsVisitor->containsTermITE(n); + } + + private: + std::unique_ptr<ContainsTermITEVisitor> d_containsVisitor; + ITECompressor* d_compressor; + ITESimplifier* d_simplifier; + ITECareSimplifier* d_careSimp; +}; + +class IncomingArcCounter +{ + public: + IncomingArcCounter(bool skipVars = false, bool skipConstants = false); + ~IncomingArcCounter(); + void computeReachability(const std::vector<Node>& assertions); + + inline uint32_t lookupIncoming(Node n) const + { + NodeCountMap::const_iterator it = d_reachCount.find(n); + if (it == d_reachCount.end()) + { + return 0; + } + else + { + return (*it).second; + } + } + void clear(); + + private: + typedef std::unordered_map<Node, uint32_t, NodeHashFunction> NodeCountMap; + NodeCountMap d_reachCount; + + bool d_skipVariables; + bool d_skipConstants; +}; + +class TermITEHeightCounter +{ + public: + TermITEHeightCounter(); + ~TermITEHeightCounter(); + + /** + * Compute and [potentially] cache the termITEHeight() of e. + * The term ite height equals the maximum number of term ites + * encountered on any path from e to a leaf. + * Inductively: + * - termITEHeight(leaves) = 0 + * - termITEHeight(e: term-ite(c, t, e) ) = + * 1 + max(termITEHeight(t), termITEHeight(e)) ; Don't include c + * - termITEHeight(e not term ite) = max_{c in children(e)) + * (termITEHeight(c)) + */ + uint32_t termITEHeight(TNode e); + + /** Clear the cache. */ + void clear(); + + /** Size of the cache. */ + size_t cache_size() const; + + private: + typedef std::unordered_map<Node, uint32_t, NodeHashFunction> NodeCountMap; + NodeCountMap d_termITEHeight; +}; /* class TermITEHeightCounter */ + +/** + * A routine designed to undo the potentially large blow up + * due to expansion caused by the ite simplifier. + */ +class ITECompressor +{ + public: + ITECompressor(ContainsTermITEVisitor* contains); + ~ITECompressor(); + + /* returns false if an assertion is discovered to be equal to false. */ + bool compress(std::vector<Node>& assertions); + + /* garbage Collects the compressor. */ + void garbageCollect(); + + private: + Node d_true; /* Copy of true. */ + Node d_false; /* Copy of false. */ + ContainsTermITEVisitor* d_contains; + std::vector<Node>* d_assertions; + IncomingArcCounter d_incoming; + + typedef std::unordered_map<Node, Node, NodeHashFunction> NodeMap; + NodeMap d_compressed; + + void reset(); + + Node push_back_boolean(Node original, Node compressed); + bool multipleParents(TNode c); + Node compressBooleanITEs(Node toCompress); + Node compressTerm(Node toCompress); + Node compressBoolean(Node toCompress); + + class Statistics + { + public: + IntStat d_compressCalls; + IntStat d_skolemsAdded; + Statistics(); + ~Statistics(); + }; + Statistics d_statistics; +}; /* class ITECompressor */ + +class ITESimplifier +{ + public: + ITESimplifier(ContainsTermITEVisitor* d_containsVisitor); + ~ITESimplifier(); + + Node simpITE(TNode assertion); + + bool doneALotOfWorkHeuristic() const; + void clearSimpITECaches(); + + private: + Node d_true; + Node d_false; + + ContainsTermITEVisitor* d_containsVisitor; + inline bool containsTermITE(TNode n) + { + return d_containsVisitor->containsTermITE(n); + } + TermITEHeightCounter d_termITEHeight; + inline uint32_t termITEHeight(TNode e) + { + return d_termITEHeight.termITEHeight(e); + } + + // ConstantIte is a small inductive sublanguage: + // constant + // or termITE(cnd, ConstantIte, ConstantIte) + typedef std::vector<Node> NodeVec; + typedef std::unordered_map<Node, NodeVec*, NodeHashFunction> + ConstantLeavesMap; + ConstantLeavesMap d_constantLeaves; + + // d_constantLeaves satisfies the following invariants: + // not containsTermITE(x) then !isKey(x) + // containsTermITE(x): + // - not isKey(x) then this value is uncomputed + // - d_constantLeaves[x] == NULL, then this contains a non-constant leaf + // - d_constantLeaves[x] != NULL, then this contains a sorted list of constant + // leaf + bool isConstantIte(TNode e); + + /** If its not a constant and containsTermITE(ite), + * returns a sorted NodeVec of the leaves. */ + NodeVec* computeConstantLeaves(TNode ite); + + // Lists all of the vectors in d_constantLeaves for fast deletion. + std::vector<NodeVec*> d_allocatedConstantLeaves; + + /* transforms */ + Node transformAtom(TNode atom); + Node attemptConstantRemoval(TNode atom); + Node attemptLiftEquality(TNode atom); + Node attemptEagerRemoval(TNode atom); + + // Given ConstantIte trees lcite and rcite, + // return a boolean expression equivalent to (= lcite rcite) + Node intersectConstantIte(TNode lcite, TNode rcite); + + // Given ConstantIte tree cite and a constant c, + // return a boolean expression equivalent to (= lcite c) + Node constantIteEqualsConstant(TNode cite, TNode c); + uint32_t d_citeEqConstApplications; + + typedef std::pair<Node, Node> NodePair; + using NodePairHashFunction = + PairHashFunction<Node, Node, NodeHashFunction, NodeHashFunction>; + typedef std::unordered_map<NodePair, Node, NodePairHashFunction> NodePairMap; + NodePairMap d_constantIteEqualsConstantCache; + NodePairMap d_replaceOverCache; + NodePairMap d_replaceOverTermIteCache; + Node replaceOver(Node n, Node replaceWith, Node simpVar); + Node replaceOverTermIte(Node term, Node simpAtom, Node simpVar); + + std::unordered_map<Node, bool, NodeHashFunction> d_leavesConstCache; + bool leavesAreConst(TNode e, theory::TheoryId tid); + bool leavesAreConst(TNode e); + + NodePairMap d_simpConstCache; + Node simpConstants(TNode simpContext, TNode iteNode, TNode simpVar); + std::unordered_map<TypeNode, Node, TypeNode::HashFunction> d_simpVars; + Node getSimpVar(TypeNode t); + + typedef std::unordered_map<Node, Node, NodeHashFunction> NodeMap; + NodeMap d_simpContextCache; + Node createSimpContext(TNode c, Node& iteNode, Node& simpVar); + + NodeMap d_simpITECache; + Node simpITEAtom(TNode atom); + + private: + class Statistics + { + public: + IntStat d_maxNonConstantsFolded; + IntStat d_unexpected; + IntStat d_unsimplified; + IntStat d_exactMatchFold; + IntStat d_binaryPredFold; + IntStat d_specialEqualityFolds; + IntStat d_simpITEVisits; + + HistogramStat<uint32_t> d_inSmaller; + + Statistics(); + ~Statistics(); + }; + + Statistics d_statistics; +}; + +class ITECareSimplifier +{ + public: + ITECareSimplifier(); + ~ITECareSimplifier(); + + Node simplifyWithCare(TNode e); + + void clear(); + + private: + /** + * This should always equal the number of care sets allocated by + * this object - the number of these that have been deleted. This is + * initially 0 and should always be 0 at the *start* of + * ~ITECareSimplifier(). + */ + unsigned d_careSetsOutstanding; + + Node d_true; + Node d_false; + + typedef std::unordered_map<TNode, Node, TNodeHashFunction> TNodeMap; + + class CareSetPtr; + class CareSetPtrVal + { + public: + bool safeToGarbageCollect() const { return d_refCount == 0; } + + private: + friend class ITECareSimplifier::CareSetPtr; + ITECareSimplifier& d_iteSimplifier; + unsigned d_refCount; + std::set<Node> d_careSet; + CareSetPtrVal(ITECareSimplifier& simp) + : d_iteSimplifier(simp), d_refCount(1) + { + } + }; /* class ITECareSimplifier::CareSetPtrVal */ + + std::vector<CareSetPtrVal*> d_usedSets; + void careSetPtrGC(CareSetPtrVal* val) { d_usedSets.push_back(val); } + + class CareSetPtr + { + CareSetPtrVal* d_val; + CareSetPtr(CareSetPtrVal* val) : d_val(val) {} + + public: + CareSetPtr() : d_val(NULL) {} + CareSetPtr(const CareSetPtr& cs) + { + d_val = cs.d_val; + if (d_val != NULL) + { + ++(d_val->d_refCount); + } + } + ~CareSetPtr() + { + if (d_val != NULL && (--(d_val->d_refCount) == 0)) + { + d_val->d_iteSimplifier.careSetPtrGC(d_val); + } + } + CareSetPtr& operator=(const CareSetPtr& cs) + { + if (d_val != cs.d_val) + { + if (d_val != NULL && (--(d_val->d_refCount) == 0)) + { + d_val->d_iteSimplifier.careSetPtrGC(d_val); + } + d_val = cs.d_val; + if (d_val != NULL) + { + ++(d_val->d_refCount); + } + } + return *this; + } + std::set<Node>& getCareSet() { return d_val->d_careSet; } + + static CareSetPtr mkNew(ITECareSimplifier& simp); + static CareSetPtr recycle(CareSetPtrVal* val) + { + Assert(val != NULL && val->d_refCount == 0); + val->d_refCount = 1; + return CareSetPtr(val); + } + }; /* class ITECareSimplifier::CareSetPtr */ + + CareSetPtr getNewSet(); + + typedef std::map<TNode, CareSetPtr> CareMap; + void updateQueue(CareMap& queue, TNode e, CareSetPtr& careSet); + Node substitute(TNode e, TNodeMap& substTable, TNodeMap& cache); +}; + +} // namespace util +} // namespace preprocessing +} // namespace CVC4 + +#endif |