case SkolemFunId::BAGS_FOLD_ELEMENTS: return "BAGS_FOLD_ELEMENTS";
case SkolemFunId::BAGS_FOLD_UNION_DISJOINT: return "BAGS_FOLD_UNION_DISJOINT";
case SkolemFunId::BAGS_MAP_PREIMAGE: return "BAGS_MAP_PREIMAGE";
+ case SkolemFunId::BAGS_MAP_PREIMAGE_INDEX: return "BAGS_MAP_PREIMAGE_INDEX";
case SkolemFunId::BAGS_MAP_SUM: return "BAGS_MAP_SUM";
case SkolemFunId::HO_TYPE_MATCH_PRED: return "HO_TYPE_MATCH_PRED";
default: return "?";
* where uf: Int -> E is a skolem function, and E is the type of elements of A
*/
BAGS_MAP_PREIMAGE,
+ /**
+ * A skolem variable for the index that is unique per terms
+ * (map f A), y, preImageSize, y, e which might be an element in A.
+ * (see the documentation for BAGS_MAP_PREIMAGE)
+ */
+ BAGS_MAP_PREIMAGE_INDEX,
/** An uninterpreted function for bag.map operator:
* If the preimage of {y} in A is {uf(1), ..., uf(n)} (see BAGS_MAP_PREIMAGE},
* then the multiplicity of an element y in a bag (map f A) is sum(n),
for (const Node& z : downwards)
{
Node y = d_state.getRepresentative(z);
- if (d_mapCache.count(n) && d_mapCache[n].get()->contains(y))
+ if (!d_mapCache.count(n))
{
- continue;
+ std::shared_ptr<context::CDHashMap<Node, std::pair<Node, Node>>> nMap =
+ std::make_shared<context::CDHashMap<Node, std::pair<Node, Node>>>(
+ userContext());
+ d_mapCache[n] = nMap;
}
- auto [downInference, uf, preImageSize] = d_ig.mapDownwards(n, y);
- d_im.lemmaTheoryInference(&downInference);
- for (const Node& x : upwards)
+ if (!d_mapCache[n].get()->count(y))
{
- InferInfo upInference = d_ig.mapUpwards(n, uf, preImageSize, y, x);
- d_im.lemmaTheoryInference(&upInference);
+ auto [downInference, uf, preImageSize] = d_ig.mapDown(n, y);
+ d_im.lemmaTheoryInference(&downInference);
+ std::pair<Node, Node> yPair = std::make_pair(uf, preImageSize);
+ d_mapCache[n].get()->insert(y, yPair);
}
- if (!d_mapCache.count(n))
+
+ context::CDHashMap<Node, std::pair<Node, Node>>::iterator it =
+ d_mapCache[n].get()->find(y);
+
+ auto [uf, preImageSize] = it->second;
+
+ for (const Node& x : upwards)
{
- std::shared_ptr<context::CDHashSet<Node> > set =
- std::make_shared<context::CDHashSet<Node> >(userContext());
- d_mapCache.insert(n, set);
+ InferInfo upInference = d_ig.mapUp(n, uf, preImageSize, y, x);
+ d_im.lemmaTheoryInference(&upInference);
}
- d_mapCache[n].get()->insert(y);
}
}
/** Reference to the term registry of theory of bags */
TermRegistry& d_termReg;
- /** a cache that stores bags of kind BAG_MAP and those element representatives
- * which we generated their inferences.
+ /**
+ * a map where the keys are nodes of the form (bag.map f A)
+ * where f is a function (-> E T), A a bag of type (Bag E),
+ * and values are maps where keys are elements y's of (bag.map f A)
+ * and values are pairs <uf, preImageSize> such that
+ * uf is an uninterpreted function Int -> E represents the and
+ * preImageSize is the cardinality of the distinct elements in A that are
+ * mapped to each y
+ *
*/
- using BagElementsMap =
- context::CDHashMap<Node, std::shared_ptr<context::CDHashSet<Node> > >;
+ using BagElementsMap = context::CDHashMap<
+ Node,
+ std::shared_ptr<context::CDHashMap<Node, std::pair<Node, Node> > > >;
BagElementsMap d_mapCache;
/** Commonly used constants */
std::ostream& operator<<(std::ostream& out, const InferInfo& ii)
{
- out << "(infer :id " << ii.getId() << std::endl;
- out << ":conclusion " << ii.d_conclusion << std::endl;
+ out << "(infer ;id " << std::endl << ii.getId() << std::endl;
+ out << ";conclusion " << std::endl << ii.d_conclusion << std::endl;
if (!ii.d_premises.empty())
{
- out << " :premise (" << ii.d_premises << ")" << std::endl;
+ out << " ;premise" << std::endl << ii.d_premises << std::endl;
}
- out << ":skolems " << ii.d_skolems << std::endl;
+ out << ";skolems " << ii.d_skolems << std::endl;
out << ")";
return out;
}
return count;
}
-std::tuple<InferInfo, Node, Node> InferenceGenerator::mapDownwards(Node n,
- Node e)
+std::tuple<InferInfo, Node, Node> InferenceGenerator::mapDown(Node n, Node e)
{
Assert(n.getKind() == BAG_MAP && n[1].getType().isBag());
Assert(n[0].getType().isFunction()
&& n[0].getType().getArgTypes().size() == 1);
Assert(e.getType() == n[0].getType().getRangeType());
- InferInfo inferInfo(d_im, InferenceId::BAGS_MAP);
+ InferInfo inferInfo(d_im, InferenceId::BAGS_MAP_DOWN);
Node f = n[0];
Node A = n[1];
std::map<Node, Node> m;
m[e] = conclusion;
- Trace("bags::InferenceGenerator::mapDownwards")
+ Trace("bags::InferenceGenerator::mapDown")
<< "conclusion: " << inferInfo.d_conclusion << std::endl;
return std::tuple(inferInfo, uf, preImageSize);
}
-InferInfo InferenceGenerator::mapUpwards(
+InferInfo InferenceGenerator::mapUp(
Node n, Node uf, Node preImageSize, Node y, Node x)
{
Assert(n.getKind() == BAG_MAP && n[1].getType().isBag());
Assert(n[0].getType().isFunction()
&& n[0].getType().getArgTypes().size() == 1);
- InferInfo inferInfo(d_im, InferenceId::BAGS_MAP);
+ InferInfo inferInfo(d_im, InferenceId::BAGS_MAP_UP);
Node f = n[0];
Node A = n[1];
Node xInA = d_nm->mkNode(GEQ, countA, d_one);
Node notEqual = d_nm->mkNode(EQUAL, d_nm->mkNode(APPLY_UF, f, x), y).negate();
- Node k = d_sm->mkDummySkolem("k", d_nm->integerType());
+ Node k = d_sm->mkSkolemFunction(SkolemFunId::BAGS_MAP_PREIMAGE_INDEX,
+ d_nm->integerType(),
+ {n, uf, preImageSize, y, x});
Node inRange = d_nm->mkNode(
AND, d_nm->mkNode(GEQ, k, d_one), d_nm->mkNode(LEQ, k, preImageSize));
Node equal = d_nm->mkNode(EQUAL, d_nm->mkNode(APPLY_UF, uf, k), x);
* preimage of e,
* and skolem is a fresh variable equals (bag.map f A))
*/
- std::tuple<InferInfo, Node, Node> mapDownwards(Node n, Node e);
+ std::tuple<InferInfo, Node, Node> mapDown(Node n, Node e);
/**
* @param n is (bag.map f A) where f is a function (-> E T), A a bag of type
* @param e is an element of type E
* @return an inference that represents the following implication
* (=>
- * (>= (bag.count x A) 1)
+ * (bag.member x A)
* (or
* (not (= (f x) y)
* (and
* (= (uf skolem) x)))))
* where skolem is a fresh variable
*/
- InferInfo mapUpwards(Node n, Node uf, Node preImageSize, Node y, Node x);
+ InferInfo mapUp(Node n, Node uf, Node preImageSize, Node y, Node x);
/**
* @param n is (bag.filter p A) where p is a function (-> E Bool),
while (!repIt.isFinished())
{
Node eqc = (*repIt);
- Trace("bags-eqc") << "Eqc [ " << eqc << " ] = { ";
+ Trace("bags-eqc") << "(eqc " << eqc << std::endl << "";
if (eqc.getType().isBag())
{
}
++it;
}
- Trace("bags-eqc") << " } " << std::endl;
+ Trace("bags-eqc") << std::endl << " ) " << std::endl;
++repIt;
}
- Trace("bags-eqc") << "bag representatives: " << d_bags << endl;
+ Trace("bags-eqc") << "(bagRepresentatives " << d_bags << ")" << std::endl;
return lemmas;
}
Node n = (*it);
if (n.getKind() == EQUAL && n[0].getType().isBag())
{
- Trace("bags-eqc") << "Disequal terms: " << n << std::endl;
+ Trace("bags-eqc") << "(disequalTerms " << n << " )" << std::endl;
d_deq.insert(n);
}
++it;
return "BAGS_DIFFERENCE_SUBTRACT";
case InferenceId::BAGS_DIFFERENCE_REMOVE: return "BAGS_DIFFERENCE_REMOVE";
case InferenceId::BAGS_DUPLICATE_REMOVAL: return "BAGS_DUPLICATE_REMOVAL";
- case InferenceId::BAGS_MAP: return "BAGS_MAP";
+ case InferenceId::BAGS_MAP_DOWN: return "BAGS_MAP_DOWN";
+ case InferenceId::BAGS_MAP_UP: return "BAGS_MAP_UP";
case InferenceId::BAGS_FILTER_DOWN: return "BAGS_FILTER_DOWN";
case InferenceId::BAGS_FILTER_UP: return "BAGS_FILTER_UP";
case InferenceId::BAGS_FOLD: return "BAGS_FOLD";
BAGS_DIFFERENCE_SUBTRACT,
BAGS_DIFFERENCE_REMOVE,
BAGS_DUPLICATE_REMOVAL,
- BAGS_MAP,
+ BAGS_MAP_DOWN,
+ BAGS_MAP_UP,
BAGS_FILTER_DOWN,
BAGS_FILTER_UP,
BAGS_FOLD,
projects / cvc5.git / commitdiff