From dd31916953ecc29514499e5c1cb96e3ae33ff3b8 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 29 Nov 2017 16:11:09 -0600 Subject: [PATCH] Improve caching in term formula removal (#1398) --- src/smt/term_formula_removal.cpp | 194 +++++++++++-------- src/smt/term_formula_removal.h | 47 ++++- test/regress/regress0/arrays/incorrect10.smt | 2 + 3 files changed, 161 insertions(+), 82 deletions(-) diff --git a/src/smt/term_formula_removal.cpp b/src/smt/term_formula_removal.cpp index c2f9facce..250c21202 100644 --- a/src/smt/term_formula_removal.cpp +++ b/src/smt/term_formula_removal.cpp @@ -26,7 +26,7 @@ using namespace std; namespace CVC4 { RemoveTermFormulas::RemoveTermFormulas(context::UserContext* u) - : d_iteCache(u) + : d_tfCache(u), d_skolem_cache(u) { d_containsVisitor = new theory::ContainsTermITEVisitor(); } @@ -43,10 +43,6 @@ theory::ContainsTermITEVisitor* RemoveTermFormulas::getContainsVisitor() { return d_containsVisitor; } -size_t RemoveTermFormulas::collectedCacheSizes() const{ - return d_containsVisitor->cache_size() + d_iteCache.size(); -} - void RemoveTermFormulas::run(std::vector& output, IteSkolemMap& iteSkolemMap, bool reportDeps) { size_t n = output.size(); @@ -91,91 +87,130 @@ Node RemoveTermFormulas::run(TNode node, std::vector& output, int cv = cacheVal( inQuant, inTerm ); std::pair cacheKey(node, cv); NodeManager *nodeManager = NodeManager::currentNM(); - ITECache::const_iterator i = d_iteCache.find(cacheKey); - if(i != d_iteCache.end()) { + TermFormulaCache::const_iterator i = d_tfCache.find(cacheKey); + if (i != d_tfCache.end()) + { Node cached = (*i).second; Debug("ite") << "removeITEs: in-cache: " << cached << endl; return cached.isNull() ? Node(node) : cached; } - // If an ITE, replace it TypeNode nodeType = node.getType(); Node skolem; Node newAssertion; if(node.getKind() == kind::ITE) { - if(!nodeType.isBoolean() && (!inQuant || !node.hasBoundVar())) { - // Make the skolem to represent the ITE - skolem = nodeManager->mkSkolem("termITE", nodeType, "a variable introduced due to term-level ITE removal"); - - // The new assertion - newAssertion = - nodeManager->mkNode(kind::ITE, node[0], skolem.eqNode(node[1]), - skolem.eqNode(node[2])); + // If an ITE, replace it + if (!nodeType.isBoolean() && (!inQuant || !node.hasBoundVar())) + { + skolem = getSkolemForNode(node); + if (skolem.isNull()) + { + // Make the skolem to represent the ITE + skolem = nodeManager->mkSkolem( + "termITE", + nodeType, + "a variable introduced due to term-level ITE removal"); + d_skolem_cache.insert(node, skolem); + + // The new assertion + newAssertion = nodeManager->mkNode( + kind::ITE, node[0], skolem.eqNode(node[1]), skolem.eqNode(node[2])); + } } } - //if a lambda, do lambda-lifting - if( node.getKind() == kind::LAMBDA && !inQuant ){ - // Make the skolem to represent the lambda - skolem = nodeManager->mkSkolem("lambdaF", nodeType, "a function introduced due to term-level lambda removal"); - - // The new assertion - std::vector< Node > children; - // bound variable list - children.push_back( node[0] ); - // body - std::vector< Node > skolem_app_c; - skolem_app_c.push_back( skolem ); - for( unsigned i=0; imkSkolem( + "lambdaF", + nodeType, + "a function introduced due to term-level lambda removal"); + d_skolem_cache.insert(node, skolem); + + // The new assertion + std::vector children; + // bound variable list + children.push_back(node[0]); + // body + std::vector skolem_app_c; + skolem_app_c.push_back(skolem); + skolem_app_c.insert(skolem_app_c.end(), node[0].begin(), node[0].end()); + Node skolem_app = nodeManager->mkNode(kind::APPLY_UF, skolem_app_c); + children.push_back(skolem_app.eqNode(node[1])); + // axiom defining skolem + newAssertion = nodeManager->mkNode(kind::FORALL, children); + } } - Node skolem_app = nodeManager->mkNode( kind::APPLY_UF, skolem_app_c ); - children.push_back( skolem_app.eqNode( node[1] ) ); - // axiom defining skolem - newAssertion = nodeManager->mkNode( kind::FORALL, children ); } - - // If a Hilbert choice function, witness the choice. - // For details on this operator, see - // http://planetmath.org/hilbertsvarepsilonoperator. - if (node.getKind() == kind::CHOICE && !inQuant) + else if (node.getKind() == kind::CHOICE) { - // Make the skolem to witness the choice - skolem = nodeManager->mkSkolem( - "choiceK", - nodeType, - "a skolem introduced due to term-level Hilbert choice removal"); - - Assert(node[0].getNumChildren() == 1); - - // The new assertion is the assumption that the body - // of the choice operator holds for the Skolem - newAssertion = node[1].substitute(node[0][0], skolem); + // If a Hilbert choice function, witness the choice. + // For details on this operator, see + // http://planetmath.org/hilbertsvarepsilonoperator. + if (!inQuant) + { + skolem = getSkolemForNode(node); + if (skolem.isNull()) + { + // Make the skolem to witness the choice + skolem = nodeManager->mkSkolem( + "choiceK", + nodeType, + "a skolem introduced due to term-level Hilbert choice removal"); + d_skolem_cache.insert(node, skolem); + + Assert(node[0].getNumChildren() == 1); + + // The new assertion is the assumption that the body + // of the choice operator holds for the Skolem + newAssertion = node[1].substitute(node[0][0], skolem); + } + } } + else if (node.getKind() != kind::BOOLEAN_TERM_VARIABLE && nodeType.isBoolean() + && inTerm + && !inQuant) + { + // if a non-variable Boolean term, replace it + skolem = getSkolemForNode(node); + if (skolem.isNull()) + { + // Make the skolem to represent the Boolean term + // skolem = nodeManager->mkSkolem("termBT", nodeType, "a variable + // introduced due to Boolean term removal"); + skolem = nodeManager->mkBooleanTermVariable(); + d_skolem_cache.insert(node, skolem); - //if a non-variable Boolean term, replace it - if(node.getKind()!=kind::BOOLEAN_TERM_VARIABLE && nodeType.isBoolean() && inTerm && !inQuant ){//(!inQuant || !node.hasBoundVar())){ - - // Make the skolem to represent the Boolean term - //skolem = nodeManager->mkSkolem("termBT", nodeType, "a variable introduced due to Boolean term removal"); - skolem = nodeManager->mkBooleanTermVariable(); - - // The new assertion - newAssertion = skolem.eqNode( node ); + // The new assertion + newAssertion = skolem.eqNode(node); + } } - // if we introduced a skolem + // if the term should be replaced by a skolem if( !skolem.isNull() ){ - Debug("ite") << "removeITEs(" << node << ") => " << newAssertion << endl; - // Attach the skolem - d_iteCache.insert(cacheKey, skolem); + d_tfCache.insert(cacheKey, skolem); + + // if the skolem was introduced in this call + if (!newAssertion.isNull()) + { + Debug("ite") << "*** term formula removal introduced " << skolem + << " for " << node << std::endl; - // Remove ITEs from the new assertion, rewrite it and push it to the output - newAssertion = run(newAssertion, output, iteSkolemMap, false, false); + // Remove ITEs from the new assertion, rewrite it and push it to the + // output + newAssertion = run(newAssertion, output, iteSkolemMap, false, false); - iteSkolemMap[skolem] = output.size(); - output.push_back(newAssertion); + iteSkolemMap[skolem] = output.size(); + output.push_back(newAssertion); + } // The representation is now the skolem return skolem; @@ -206,20 +241,26 @@ Node RemoveTermFormulas::run(TNode node, std::vector& output, // If changes, we rewrite if(somethingChanged) { Node cached = nodeManager->mkNode(node.getKind(), newChildren); - d_iteCache.insert(cacheKey, cached); + d_tfCache.insert(cacheKey, cached); return cached; } else { - d_iteCache.insert(cacheKey, Node::null()); + d_tfCache.insert(cacheKey, Node::null()); return node; } } +Node RemoveTermFormulas::getSkolemForNode(Node node) const +{ + context::CDInsertHashMap::const_iterator itk = + d_skolem_cache.find(node); + if (itk != d_skolem_cache.end()) + { + return itk->second; + } + return Node::null(); +} + Node RemoveTermFormulas::replace(TNode node, bool inQuant, bool inTerm) const { - //if(node.isVar() || node.isConst()){ - // (options::biasedITERemoval() && !containsTermITE(node))){ - //if(node.isVar()){ - // return Node(node); - //} if( node.getKind()==kind::INST_PATTERN_LIST ){ return Node(node); } @@ -227,8 +268,9 @@ Node RemoveTermFormulas::replace(TNode node, bool inQuant, bool inTerm) const { // Check the cache NodeManager *nodeManager = NodeManager::currentNM(); int cv = cacheVal( inQuant, inTerm ); - ITECache::const_iterator i = d_iteCache.find(make_pair(node, cv)); - if(i != d_iteCache.end()) { + TermFormulaCache::const_iterator i = d_tfCache.find(make_pair(node, cv)); + if (i != d_tfCache.end()) + { Node cached = (*i).second; return cached.isNull() ? Node(node) : cached; } diff --git a/src/smt/term_formula_removal.h b/src/smt/term_formula_removal.h index 371ca1f58..63a74a332 100644 --- a/src/smt/term_formula_removal.h +++ b/src/smt/term_formula_removal.h @@ -37,11 +37,49 @@ namespace theory { typedef std::unordered_map IteSkolemMap; class RemoveTermFormulas { - typedef context::CDInsertHashMap< std::pair, Node, PairHashFunction > ITECache; - ITECache d_iteCache; + typedef context:: + CDInsertHashMap, + Node, + PairHashFunction > + TermFormulaCache; + /** term formula removal cache + * + * This stores the results of term formula removal for inputs to the run(...) + * function below, where the integer in the pair we hash on is the + * result of cacheVal below. + */ + TermFormulaCache d_tfCache; + /** return the integer cache value for the input flags to run(...) */ static inline int cacheVal( bool inQuant, bool inTerm ) { return (inQuant ? 1 : 0) + 2*(inTerm ? 1 : 0); } - + + /** skolem cache + * + * This is a cache that maps terms to the skolem we use to replace them. + * + * Notice that this cache is necessary in addition to d_tfCache, since + * we should use the same skolem to replace terms, regardless of the input + * arguments to run(...). For example: + * + * ite( G, a, b ) = c ^ forall x. P( ite( G, a, b ), x ) + * + * should be processed to: + * + * k = c ^ forall x. P( k, x ) ^ ite( G, k=a, k=b ) + * + * where notice + * d_skolem_cache[ite( G, a, b )] = k, and + * d_tfCache[] = d_tfCache[] = k. + */ + context::CDInsertHashMap d_skolem_cache; + + /** gets the skolem for node + * + * This returns the d_skolem_cache value for node, if it exists as a key + * in the above map, or the null node otherwise. + */ + inline Node getSkolemForNode(Node node) const; + static bool hasNestedTermChildren( TNode node ); public: @@ -111,9 +149,6 @@ public: /** Returns true if e contains a term ite. */ bool containsTermITE(TNode e) const; - /** Returns the collected size of the caches. */ - size_t collectedCacheSizes() const; - /** Garbage collects non-context dependent data-structures. */ void garbageCollect(); diff --git a/test/regress/regress0/arrays/incorrect10.smt b/test/regress/regress0/arrays/incorrect10.smt index 402fcc128..6fbdb7ee9 100644 --- a/test/regress/regress0/arrays/incorrect10.smt +++ b/test/regress/regress0/arrays/incorrect10.smt @@ -1,3 +1,5 @@ +% COMMAND-LINE: --no-check-proofs +% EXPECT: unsat (benchmark fuzzsmt :logic QF_AX :status unsat -- 2.30.2