diff options
author | Tim King <taking@cs.nyu.edu> | 2013-11-25 18:36:06 -0500 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2013-11-25 18:36:06 -0500 |
commit | 22df6e9e8618614e8c33700c55705266912500ae (patch) | |
tree | 20d78676c1e819517f371e8bc5e6363008fc9154 /src/theory/ite_utilities.h | |
parent | 91424455840a7365a328cbcc3d02ec453fe9d0ea (diff) |
Substantial Changes:
-ITE Simplification
-- Moved the utilities in src/theory/ite_simplifier.{h,cpp} to ite_utilities.
-- Separated simpWithCare from simpITE.
-- Disabled ite simplification on repeat simplification by default. Currently, ite simplification cannot help unless we internally make new constant leaf ites equal to constants.
-- simplifyWithCare() is now only run on QF_AUFBV by default. Speeds up nec benchmarks dramatically.
-- Added a new compress ites pass that is only run on QF_LIA by default. This targets the perverse structure of ites generated during ite simplification on nec benchmarks.
-- After ite simplification, if the ite simplifier was used many times and the NodeManager's node pool is large enough, this garbage collects: zombies from the NodeManager repeatedly, the ite simplification caches, and the theory rewrite caches.
- TheoryEngine
-- Added TheoryEngine::donePPSimpITE() which orchestrates a number of ite simplifications above.
-- Switched UnconstrainedSimplifier to a pointer.
- RemoveITEs
-- Added a heuristic for checking whether or not a node contains term ites and if not, not bothering to invoke the rest of RemoveITE::run(). This safely changes the type of the cache used on misses of run. This cache can be cleared in the future. Currently disabled pending additional testing.
- TypeChecker
-- added a neverIsConst() rule to the typechecker. Operators that cannot be used in constructing constant expressions by computeIsConst() can now avoid caching on Node::isConst() calls.
- Theory Bool Rewriter
-- Added additional simplifications for boolean ites.
Minor Changes:
- TheoryModel
-- Removed vestigial copy of the ITESimplifier.
- AttributeManager
-- Fixed a garbage collection bug when deleting the node table caused the NodeManager to reclaimZombies() which caused memory corruption by deleting from the attributeManager.
- TypeChecker
-- added a neverIsConst() rule to the typechecker. Operators that cannot be used in constructing constant expressions by computeIsConst() can now avoid caching on Node::isConst() calls.
-NodeManager
-- Added additional functions for reclaiming zombies.
-- Exposed the size of the node pool for heuristics that worry about memory consumption.
- NaryBuilder
-- Added convenience classes for constructing associative and commutative n-ary operators.
-- Added a pass that turns associative and commutative n-ary operators into binary operators. (Mostly for printing expressions for strict parsers.)
Diffstat (limited to 'src/theory/ite_utilities.h')
-rw-r--r-- | src/theory/ite_utilities.h | 373 |
1 files changed, 373 insertions, 0 deletions
diff --git a/src/theory/ite_utilities.h b/src/theory/ite_utilities.h new file mode 100644 index 000000000..73f0386d2 --- /dev/null +++ b/src/theory/ite_utilities.h @@ -0,0 +1,373 @@ +/********************* */ +/*! \file ite_simplifier.h + ** \verbatim + ** Original author: Clark Barrett + ** Major contributors: none + ** Minor contributors (to current version): Morgan Deters + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** 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 <vector> +#include <ext/hash_map> +#include <ext/hash_set> +#include "expr/node.h" +#include "util/statistics_registry.h" + +namespace CVC4 { +namespace theory { + +class ContainsTermITEVistor; +class IncomingArcCounter; +class TermITEHeightCounter; +class ITECompressor; +class ITESimplifier; +class ITECareSimplifier; + +class ITEUtilities { +public: + ITEUtilities(ContainsTermITEVistor* containsVisitor); + ~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(); + +private: + ContainsTermITEVistor* d_containsVisitor; + ITECompressor* d_compressor; + ITESimplifier* d_simplifier; + ITECareSimplifier* d_careSimp; +}; + +/** + * A caching visitor that computes whether a node contains a term ite. + */ +class ContainsTermITEVistor { +public: + ContainsTermITEVistor(); + ~ContainsTermITEVistor(); + + /** 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::hash_map<Node, bool, NodeHashFunction> NodeBoolMap; + NodeBoolMap d_cache; +}; + +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::hash_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::hash_map<Node, uint32_t, NodeHashFunction> NodeCountMap; + NodeCountMap d_termITEHeight; +}; + +/** + * A routine designed to undo the potentially large blow up + * due to expansion caused by the ite simplifier. + */ +class ITECompressor { +public: + ITECompressor(ContainsTermITEVistor* 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. */ + ContainsTermITEVistor* d_contains; + std::vector<Node>* d_assertions; + IncomingArcCounter d_incoming; + + typedef std::hash_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 ITESimplifier { +public: + ITESimplifier(ContainsTermITEVistor* d_containsVisitor); + ~ITESimplifier(); + + Node simpITE(TNode assertion); + + bool doneALotOfWorkHeuristic() const; + void clearSimpITECaches(); + +private: + Node d_true; + Node d_false; + + ContainsTermITEVistor* 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::hash_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; + struct NodePairHashFunction { + size_t operator () (const NodePair& pair) const { + size_t hash = 0; + hash = 0x9e3779b9 + NodeHashFunction().operator()(pair.first); + hash ^= 0x9e3779b9 + NodeHashFunction().operator()(pair.second) + (hash << 6) + (hash >> 2); + return hash; + } + };/* struct ITESimplifier::NodePairHashFunction */ + typedef std::hash_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::hash_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::hash_map<TypeNode, Node, TypeNode::HashFunction> d_simpVars; + Node getSimpVar(TypeNode t); + + typedef std::hash_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: + Node d_true; + Node d_false; + + typedef std::hash_map<TNode, Node, TNodeHashFunction> TNodeMap; + + class CareSetPtr; + class CareSetPtrVal { + friend class ITECareSimplifier::CareSetPtr; + ITECareSimplifier& d_iteSimplifier; + unsigned d_refCount; + std::set<Node> d_careSet; + CareSetPtrVal(ITECareSimplifier& simp) : d_iteSimplifier(simp), d_refCount(1) {} + }; + + 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) { + CareSetPtrVal* val = new CareSetPtrVal(simp); + return CareSetPtr(val); + } + static CareSetPtr recycle(CareSetPtrVal* val) { + Assert(val != NULL && val->d_refCount == 0); + val->d_refCount = 1; + return CareSetPtr(val); + } + }; + + CareSetPtr getNewSet(); + + typedef std::map<TNode, CareSetPtr> CareMap; + void updateQueue(CareMap& queue, TNode e, CareSetPtr& careSet); + Node substitute(TNode e, TNodeMap& substTable, TNodeMap& cache); +}; + +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ + +#endif |