namespace CVC4 {
RemoveTermFormulas::RemoveTermFormulas(context::UserContext* u)
- : d_iteCache(u)
+ : d_tfCache(u), d_skolem_cache(u)
{
d_containsVisitor = new theory::ContainsTermITEVisitor();
}
return d_containsVisitor;
}
-size_t RemoveTermFormulas::collectedCacheSizes() const{
- return d_containsVisitor->cache_size() + d_iteCache.size();
-}
-
void RemoveTermFormulas::run(std::vector<Node>& output, IteSkolemMap& iteSkolemMap, bool reportDeps)
{
size_t n = output.size();
int cv = cacheVal( inQuant, inTerm );
std::pair<Node, int> 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; i<node[0].getNumChildren(); i++ ){
- skolem_app_c.push_back( node[0][i] );
+ else if (node.getKind() == kind::LAMBDA)
+ {
+ // if a lambda, do lambda-lifting
+ if (!inQuant)
+ {
+ skolem = getSkolemForNode(node);
+ if (skolem.isNull())
+ {
+ // Make the skolem to represent the lambda
+ skolem = nodeManager->mkSkolem(
+ "lambdaF",
+ nodeType,
+ "a function introduced due to term-level lambda removal");
+ d_skolem_cache.insert(node, skolem);
+
+ // 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);
+ 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;
// 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<Node, Node, NodeHashFunction>::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);
}
// 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;
}
typedef std::unordered_map<Node, unsigned, NodeHashFunction> IteSkolemMap;
class RemoveTermFormulas {
- typedef context::CDInsertHashMap< std::pair<Node, int>, Node, PairHashFunction<Node, int, NodeHashFunction, BoolHashFunction> > ITECache;
- ITECache d_iteCache;
+ typedef context::
+ CDInsertHashMap<std::pair<Node, int>,
+ Node,
+ PairHashFunction<Node, int, NodeHashFunction> >
+ 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[<ite( G, a, b ),0>] = d_tfCache[<ite( G, a, b ),1>] = k.
+ */
+ context::CDInsertHashMap<Node, Node, NodeHashFunction> 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:
/** 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();
projects / cvc5.git / commitdiff