Eliminates NodeHashFunction, TNodeHashFunction and TypeNodeHashFunction.
bool Grammar::containsFreeVariables(const Term& rule) const
{
- std::unordered_set<TNode, TNodeHashFunction> scope;
+ std::unordered_set<TNode> scope;
for (const Term& sygusVar : d_sygusVars)
{
scope.emplace(*ntsymbol.d_node);
}
- std::unordered_set<Node, NodeHashFunction> fvs;
+ std::unordered_set<Node> fvs;
return expr::getFreeVariablesScope(*rule.d_node, fvs, scope, false);
}
{
if (t.isIndexedHelper())
{
- return cvc5::NodeHashFunction()(*t.d_node);
+ return std::hash<cvc5::Node>()(*t.d_node);
}
else
{
size_t std::hash<cvc5::api::Sort>::operator()(const cvc5::api::Sort& s) const
{
- return cvc5::TypeNodeHashFunction()(*s.d_type);
+ return std::hash<cvc5::TypeNode>()(*s.d_type);
}
size_t std::hash<cvc5::api::Term>::operator()(const cvc5::api::Term& t) const
{
- return cvc5::NodeHashFunction()(*t.d_node);
+ return std::hash<cvc5::Node>()(*t.d_node);
}
} // namespace std
namespace cvc5 {
namespace context {
-template <class V, class HashFcn>
-class CDHashSet : protected CDInsertHashMap<V, bool, HashFcn> {
+template <class V, class HashFcn = std::hash<V>>
+class CDHashSet : protected CDInsertHashMap<V, bool, HashFcn>
+{
typedef CDInsertHashMap<V, bool, HashFcn> super;
// no copy or assignment
return super::insertAtContextLevelZero(v, true);
}
-};/* class CDHashSet */
+}; /* class CDHashSet */
} // namespace context
} // namespace cvc5
// no decision does not impact the decision order
return;
}
- std::unordered_set<TNode, TNodeHashFunction>::iterator it =
- d_dlistSet.find(n);
+ std::unordered_set<TNode>::iterator it = d_dlistSet.find(n);
if (s == DecisionStatus::DECISION)
{
if (it == d_dlistSet.end())
/** The list of assertions */
std::vector<TNode> d_dlist;
/** The set of assertions for fast membership testing in the above vector */
- std::unordered_set<TNode, TNodeHashFunction> d_dlistSet;
+ std::unordered_set<TNode> d_dlistSet;
/** The index of the next assertion to satify */
context::CDO<size_t> d_dindex;
};
enum SearchResult {FOUND_SPLITTER, NO_SPLITTER, DONT_KNOW};
typedef std::vector<std::pair<Node, Node> > SkolemList;
- typedef context::CDHashMap<Node, SkolemList, NodeHashFunction> SkolemCache;
+ typedef context::CDHashMap<Node, SkolemList> SkolemCache;
typedef std::vector<Node> ChildList;
- typedef context::
- CDHashMap<Node, std::pair<ChildList, ChildList>, NodeHashFunction>
- ChildCache;
- typedef context::CDHashMap<Node,Node,NodeHashFunction> SkolemMap;
- typedef context::CDHashMap<Node,
- std::pair<DecisionWeight, DecisionWeight>,
- NodeHashFunction>
+ typedef context::CDHashMap<Node, std::pair<ChildList, ChildList>> ChildCache;
+ typedef context::CDHashMap<Node, Node> SkolemMap;
+ typedef context::CDHashMap<Node, std::pair<DecisionWeight, DecisionWeight>>
WeightCache;
// being 'justified' is monotonic with respect to decisions
- typedef context::CDHashSet<Node,NodeHashFunction> JustifiedSet;
+ typedef context::CDHashSet<Node> JustifiedSet;
JustifiedSet d_justified;
- typedef context::CDHashMap<Node,DecisionWeight,NodeHashFunction> ExploredThreshold;
+ typedef context::CDHashMap<Node, DecisionWeight> ExploredThreshold;
ExploredThreshold d_exploredThreshold;
context::CDO<unsigned> d_prvsIndex;
context::CDO<unsigned> d_threshPrvsIndex;
* splitter. Can happen when exploring assertion corresponding to a
* term-ITE.
*/
- std::unordered_set<Node,NodeHashFunction> d_visited;
+ std::unordered_set<Node> d_visited;
/**
* Set to track visited nodes in a dfs search done in computeSkolems
* function
*/
- std::unordered_set<Node, NodeHashFunction> d_visitedComputeSkolems;
+ std::unordered_set<Node> d_visitedComputeSkolems;
/** current decision for the recursive call */
prop::SatLiteral d_curDecision;
* For big and/or nodes, a cache to save starting index into children
* for efficiently.
*/
- typedef context::CDHashMap<Node, int, NodeHashFunction> StartIndexCache;
+ typedef context::CDHashMap<Node, int> StartIndexCache;
StartIndexCache d_startIndexCache;
int getStartIndex(TNode node);
void saveStartIndex(TNode node, int val);
}
size_t ArrayStoreAllHashFunction::operator()(const ArrayStoreAll& asa) const {
- return TypeNodeHashFunction()(asa.getType())
- * NodeHashFunction()(asa.getValue());
+ return std::hash<TypeNode>()(asa.getType())
+ * std::hash<Node>()(asa.getValue());
}
} // namespace cvc5
size_t AscriptionTypeHashFunction::operator()(const AscriptionType& at) const
{
- return TypeNodeHashFunction()(at.getType());
+ return std::hash<TypeNode>()(at.getType());
}
std::ostream& operator<<(std::ostream& out, AscriptionType at)
/** Whether we keep cache values */
bool d_keepCacheVals;
/** The set of cache values we have used */
- std::unordered_set<Node, NodeHashFunction> d_cacheVals;
+ std::unordered_set<Node> d_cacheVals;
};
} // namespace cvc5
*/
class BufferedProofGenerator : public ProofGenerator
{
- typedef context::CDHashMap<Node, std::shared_ptr<ProofStep>, NodeHashFunction>
- NodeProofStepMap;
+ typedef context::CDHashMap<Node, std::shared_ptr<ProofStep>> NodeProofStepMap;
public:
BufferedProofGenerator(context::Context* c, ProofNodeManager* pnm);
{
// all datatype constructors should be sygus and have sygus operators whose
// free variables are subsets of sygus bound var list.
- std::unordered_set<Node, NodeHashFunction> svs;
+ std::unordered_set<Node> svs;
for (const Node& sv : d_sygusBvl)
{
svs.insert(sv);
Node sop = d_constructors[i]->getSygusOp();
Assert(!sop.isNull())
<< "Sygus datatype contains a non-sygus constructor";
- std::unordered_set<Node, NodeHashFunction> fvs;
+ std::unordered_set<Node> fvs;
expr::getFreeVariables(sop, fvs);
for (const Node& v : fvs)
{
return groundTerm;
}
-void DType::getAlienSubfieldTypes(
- std::unordered_set<TypeNode, TypeNodeHashFunction>& types,
- std::map<TypeNode, bool>& processed,
- bool isAlienPos) const
+void DType::getAlienSubfieldTypes(std::unordered_set<TypeNode>& types,
+ std::map<TypeNode, bool>& processed,
+ bool isAlienPos) const
{
std::map<TypeNode, bool>::iterator it = processed.find(d_self);
if (it != processed.end())
Trace("datatypes-init") << "Compute simply recursive for " << getName()
<< std::endl;
// get the alien subfield types of this datatype
- std::unordered_set<TypeNode, TypeNodeHashFunction> types;
+ std::unordered_set<TypeNode> types;
std::map<TypeNode, bool> processed;
getAlienSubfieldTypes(types, processed, false);
if (Trace.isOn("datatypes-init"))
* @param isAlienPos Whether we are in an alien subfield type position. This
* flag is true if we have traversed beneath a non-datatype type constructor.
*/
- void getAlienSubfieldTypes(
- std::unordered_set<TypeNode, TypeNodeHashFunction>& types,
- std::map<TypeNode, bool>& processed,
- bool isAlienPos) const;
+ void getAlienSubfieldTypes(std::unordered_set<TypeNode>& types,
+ std::map<TypeNode, bool>& processed,
+ bool isAlienPos) const;
/** name of this datatype */
std::string d_name;
/** the type parameters of this datatype (if this is a parametric datatype)
size_t EmptyBagHashFunction::operator()(const EmptyBag& es) const
{
- return TypeNodeHashFunction()(es.getType());
+ return std::hash<TypeNode>()(es.getType());
}
/**
}
size_t EmptySetHashFunction::operator()(const EmptySet& es) const {
- return TypeNodeHashFunction()(es.getType());
+ return std::hash<TypeNode>()(es.getType());
}
/**
bool hasGenerator(Node fact) const;
protected:
- typedef context::CDHashMap<Node, ProofGenerator*, NodeHashFunction>
- NodeProofGeneratorMap;
+ typedef context::CDHashMap<Node, ProofGenerator*> NodeProofGeneratorMap;
/** Maps facts that can be proven to generators */
NodeProofGeneratorMap d_gens;
/** The default proof generator */
<< "LazyCDProofChain::getProofFor " << fact << "\n";
// which facts have had proofs retrieved for. This is maintained to avoid
// cycles. It also saves the proof node of the fact
- std::unordered_map<Node, std::shared_ptr<ProofNode>, NodeHashFunction>
- toConnect;
+ std::unordered_map<Node, std::shared_ptr<ProofNode>> toConnect;
// leaves of proof node links in the chain, i.e. assumptions, yet to be
// expanded
- std::unordered_map<Node,
- std::vector<std::shared_ptr<ProofNode>>,
- NodeHashFunction>
+ std::unordered_map<Node, std::vector<std::shared_ptr<ProofNode>>>
assumptionsToExpand;
// invariant of the loop below, the first iteration notwithstanding:
// visit = domain(assumptionsToExpand) \ domain(toConnect)
std::vector<Node> visit{fact};
- std::unordered_map<Node, bool, NodeHashFunction> visited;
+ std::unordered_map<Node, bool> visited;
Node cur;
do
{
/** A dummy context used by this class if none is provided */
context::Context d_context;
/** Maps facts that can be proven to generators */
- context::CDHashMap<Node, ProofGenerator*, NodeHashFunction> d_gens;
+ context::CDHashMap<Node, ProofGenerator*> d_gens;
/** The default proof generator (if one exists) */
ProofGenerator* d_defGen;
};
template bool NodeTemplate<false>::isConst() const;
} // namespace cvc5
+
+namespace std {
+
+size_t hash<cvc5::Node>::operator()(const cvc5::Node& node) const
+{
+ return node.getId();
+}
+
+size_t hash<cvc5::TNode>::operator()(const cvc5::TNode& node) const
+{
+ return node.getId();
+}
+
+} // namespace std
*/
typedef NodeTemplate<false> TNode;
+} // namespace cvc5
+
+namespace std {
+
+template <>
+struct hash<cvc5::Node>
+{
+ size_t operator()(const cvc5::Node& node) const;
+};
+
+template <>
+struct hash<cvc5::TNode>
+{
+ size_t operator()(const cvc5::TNode& node) const;
+};
+
+} // namespace std
+
+namespace cvc5 {
namespace expr {
class NodeValue;
} // namespace metakind
} // namespace kind
-// for hash_maps, hash_sets..
-struct NodeHashFunction {
- inline size_t operator()(Node node) const;
-};/* struct NodeHashFunction */
-struct TNodeHashFunction {
- inline size_t operator()(TNode node) const;
-};/* struct TNodeHashFunction */
-
/**
* Encapsulation of an NodeValue pointer. The reference count is
* maintained in the NodeValue if ref_count is true.
* Cache-aware, recursive version of substitute() used by the public
* member function with a similar signature.
*/
- Node substitute(TNode node, TNode replacement,
- std::unordered_map<TNode, TNode, TNodeHashFunction>& cache) const;
-
- /**
- * Cache-aware, recursive version of substitute() used by the public
- * member function with a similar signature.
- */
- template <class Iterator1, class Iterator2>
- Node substitute(Iterator1 nodesBegin, Iterator1 nodesEnd,
- Iterator2 replacementsBegin, Iterator2 replacementsEnd,
- std::unordered_map<TNode, TNode, TNodeHashFunction>& cache) const;
-
- /**
- * Cache-aware, recursive version of substitute() used by the public
- * member function with a similar signature.
- */
- template <class Iterator>
- Node substitute(Iterator substitutionsBegin, Iterator substitutionsEnd,
- std::unordered_map<TNode, TNode, TNodeHashFunction>& cache) const;
-
- /** Default constructor, makes a null expression. */
- NodeTemplate() : d_nv(&expr::NodeValue::null()) { }
-
- /**
- * Conversion between nodes that are reference-counted and those that are
- * not.
- * @param node the node to make copy of
- */
- NodeTemplate(const NodeTemplate<!ref_count>& node);
-
- /**
- * Copy constructor. Note that GCC does NOT recognize an instantiation of
- * the above template as a copy constructor and problems ensue. So we
- * provide an explicit one here.
- * @param node the node to make copy of
- */
- NodeTemplate(const NodeTemplate& node);
-
- /**
- * Assignment operator for nodes, copies the relevant information from node
- * to this node.
- * @param node the node to copy
- * @return reference to this node
- */
- NodeTemplate& operator=(const NodeTemplate& node);
-
- /**
- * Assignment operator for nodes, copies the relevant information from node
- * to this node.
- * @param node the node to copy
- * @return reference to this node
- */
- NodeTemplate& operator=(const NodeTemplate<!ref_count>& node);
-
- /**
- * Destructor. If ref_count is true it will decrement the reference count
- * and, if zero, collect the NodeValue.
- */
- ~NodeTemplate();
-
- /**
- * Return the null node.
- * @return the null node
- */
- static NodeTemplate null() {
- return s_null;
- }
-
- /**
- * Returns true if this expression is a null expression.
- * @return true if null
- */
- bool isNull() const {
- assertTNodeNotExpired();
- return d_nv == &expr::NodeValue::null();
- }
+ Node substitute(TNode node,
+ TNode replacement,
+ std::unordered_map<TNode, TNode>& cache) const;
+
+ /**
+ * Cache-aware, recursive version of substitute() used by the public
+ * member function with a similar signature.
+ */
+ template <class Iterator1, class Iterator2>
+ Node substitute(Iterator1 nodesBegin,
+ Iterator1 nodesEnd,
+ Iterator2 replacementsBegin,
+ Iterator2 replacementsEnd,
+ std::unordered_map<TNode, TNode>& cache) const;
+
+ /**
+ * Cache-aware, recursive version of substitute() used by the public
+ * member function with a similar signature.
+ */
+ template <class Iterator>
+ Node substitute(Iterator substitutionsBegin,
+ Iterator substitutionsEnd,
+ std::unordered_map<TNode, TNode>& cache) const;
+
+ /** Default constructor, makes a null expression. */
+ NodeTemplate() : d_nv(&expr::NodeValue::null()) {}
+
+ /**
+ * Conversion between nodes that are reference-counted and those that are
+ * not.
+ * @param node the node to make copy of
+ */
+ NodeTemplate(const NodeTemplate<!ref_count>& node);
+
+ /**
+ * Copy constructor. Note that GCC does NOT recognize an instantiation of
+ * the above template as a copy constructor and problems ensue. So we
+ * provide an explicit one here.
+ * @param node the node to make copy of
+ */
+ NodeTemplate(const NodeTemplate& node);
+
+ /**
+ * Assignment operator for nodes, copies the relevant information from node
+ * to this node.
+ * @param node the node to copy
+ * @return reference to this node
+ */
+ NodeTemplate& operator=(const NodeTemplate& node);
+
+ /**
+ * Assignment operator for nodes, copies the relevant information from node
+ * to this node.
+ * @param node the node to copy
+ * @return reference to this node
+ */
+ NodeTemplate& operator=(const NodeTemplate<!ref_count>& node);
+
+ /**
+ * Destructor. If ref_count is true it will decrement the reference count
+ * and, if zero, collect the NodeValue.
+ */
+ ~NodeTemplate();
+
+ /**
+ * Return the null node.
+ * @return the null node
+ */
+ static NodeTemplate null() { return s_null; }
+
+ /**
+ * Returns true if this expression is a null expression.
+ * @return true if null
+ */
+ bool isNull() const
+ {
+ assertTNodeNotExpired();
+ return d_nv == &expr::NodeValue::null();
+ }
/**
* Structural comparison operator for expressions.
/**
* Simultaneous substitution of Nodes in cache.
*/
- Node substitute(
- std::unordered_map<TNode, TNode, TNodeHashFunction>& cache) const;
+ Node substitute(std::unordered_map<TNode, TNode>& cache) const;
/**
* Returns the kind of this node.
namespace cvc5 {
-inline size_t NodeHashFunction::operator()(Node node) const {
- return node.getId();
-}
-inline size_t TNodeHashFunction::operator()(TNode node) const {
- return node.getId();
-}
-
using TNodePairHashFunction =
- PairHashFunction<TNode, TNode, TNodeHashFunction, TNodeHashFunction>;
+ PairHashFunction<TNode, TNode, std::hash<TNode>, std::hash<TNode>>;
template <bool ref_count>
inline size_t NodeTemplate<ref_count>::getNumChildren() const {
if (node == *this) {
return replacement;
}
- std::unordered_map<TNode, TNode, TNodeHashFunction> cache;
+ std::unordered_map<TNode, TNode> cache;
return substitute(node, replacement, cache);
}
template <bool ref_count>
-Node
-NodeTemplate<ref_count>::substitute(TNode node, TNode replacement,
- std::unordered_map<TNode, TNode, TNodeHashFunction>& cache) const {
+Node NodeTemplate<ref_count>::substitute(
+ TNode node,
+ TNode replacement,
+ std::unordered_map<TNode, TNode>& cache) const
+{
Assert(node != *this);
if (getNumChildren() == 0 || node == replacement)
}
// in cache?
- typename std::unordered_map<TNode, TNode, TNodeHashFunction>::const_iterator i = cache.find(*this);
+ typename std::unordered_map<TNode, TNode>::const_iterator i =
+ cache.find(*this);
if(i != cache.end()) {
return (*i).second;
}
Iterator1 nodesEnd,
Iterator2 replacementsBegin,
Iterator2 replacementsEnd) const {
- std::unordered_map<TNode, TNode, TNodeHashFunction> cache;
+ std::unordered_map<TNode, TNode> cache;
return substitute(nodesBegin, nodesEnd,
replacementsBegin, replacementsEnd, cache);
}
template <bool ref_count>
template <class Iterator1, class Iterator2>
-Node
-NodeTemplate<ref_count>::substitute(Iterator1 nodesBegin,
- Iterator1 nodesEnd,
- Iterator2 replacementsBegin,
- Iterator2 replacementsEnd,
- std::unordered_map<TNode, TNode, TNodeHashFunction>& cache) const {
+Node NodeTemplate<ref_count>::substitute(
+ Iterator1 nodesBegin,
+ Iterator1 nodesEnd,
+ Iterator2 replacementsBegin,
+ Iterator2 replacementsEnd,
+ std::unordered_map<TNode, TNode>& cache) const
+{
// in cache?
- typename std::unordered_map<TNode, TNode, TNodeHashFunction>::const_iterator i = cache.find(*this);
+ typename std::unordered_map<TNode, TNode>::const_iterator i =
+ cache.find(*this);
if(i != cache.end()) {
return (*i).second;
}
inline Node
NodeTemplate<ref_count>::substitute(Iterator substitutionsBegin,
Iterator substitutionsEnd) const {
- std::unordered_map<TNode, TNode, TNodeHashFunction> cache;
+ std::unordered_map<TNode, TNode> cache;
return substitute(substitutionsBegin, substitutionsEnd, cache);
}
template <bool ref_count>
inline Node NodeTemplate<ref_count>::substitute(
- std::unordered_map<TNode, TNode, TNodeHashFunction>& cache) const
+ std::unordered_map<TNode, TNode>& cache) const
{
// Since no substitution is given (other than what may already be in the
// cache), we pass dummy iterators to conform to the main substitute method,
template <bool ref_count>
template <class Iterator>
-Node
-NodeTemplate<ref_count>::substitute(Iterator substitutionsBegin,
- Iterator substitutionsEnd,
- std::unordered_map<TNode, TNode, TNodeHashFunction>& cache) const {
+Node NodeTemplate<ref_count>::substitute(
+ Iterator substitutionsBegin,
+ Iterator substitutionsEnd,
+ std::unordered_map<TNode, TNode>& cache) const
+{
// in cache?
- typename std::unordered_map<TNode, TNode, TNodeHashFunction>::const_iterator i = cache.find(*this);
+ typename std::unordered_map<TNode, TNode>::const_iterator i =
+ cache.find(*this);
if(i != cache.end()) {
return (*i).second;
}
return true;
}
- std::unordered_set<TNode, TNodeHashFunction> visited;
+ std::unordered_set<TNode> visited;
std::vector<TNode> toProcess;
toProcess.push_back(n);
bool hasSubtermMulti(TNode n, TNode t)
{
- std::unordered_map<TNode, bool, TNodeHashFunction> visited;
- std::unordered_map<TNode, bool, TNodeHashFunction> contains;
- std::unordered_map<TNode, bool, TNodeHashFunction>::iterator it;
+ std::unordered_map<TNode, bool> visited;
+ std::unordered_map<TNode, bool> contains;
+ std::unordered_map<TNode, bool>::iterator it;
std::vector<TNode> visit;
TNode cur;
visit.push_back(n);
bool hasSubtermKind(Kind k, Node n)
{
- std::unordered_set<TNode, TNodeHashFunction> visited;
+ std::unordered_set<TNode> visited;
std::vector<TNode> visit;
TNode cur;
visit.push_back(n);
{
return false;
}
- std::unordered_set<TNode, TNodeHashFunction> visited;
+ std::unordered_set<TNode> visited;
std::vector<TNode> visit;
TNode cur;
visit.push_back(n);
return true;
}
- std::unordered_set<TNode, TNodeHashFunction> visited;
+ std::unordered_set<TNode> visited;
std::vector<TNode> toProcess;
toProcess.push_back(n);
bool hasFreeVar(TNode n)
{
- std::unordered_set<Node, NodeHashFunction> fvs;
+ std::unordered_set<Node> fvs;
return getFreeVariables(n, fvs, false);
}
return n.getAttribute(HasClosureAttr());
}
-bool getFreeVariables(TNode n,
- std::unordered_set<Node, NodeHashFunction>& fvs,
- bool computeFv)
+bool getFreeVariables(TNode n, std::unordered_set<Node>& fvs, bool computeFv)
{
- std::unordered_set<TNode, TNodeHashFunction> scope;
+ std::unordered_set<TNode> scope;
return getFreeVariablesScope(n, fvs, scope, computeFv);
}
bool getFreeVariablesScope(TNode n,
- std::unordered_set<Node, NodeHashFunction>& fvs,
- std::unordered_set<TNode, TNodeHashFunction>& scope,
+ std::unordered_set<Node>& fvs,
+ std::unordered_set<TNode>& scope,
bool computeFv)
{
- std::unordered_set<TNode, TNodeHashFunction> visited;
+ std::unordered_set<TNode> visited;
std::vector<TNode> visit;
TNode cur;
visit.push_back(n);
{
continue;
}
- std::unordered_set<TNode, TNodeHashFunction>::iterator itv =
- visited.find(cur);
+ std::unordered_set<TNode>::iterator itv = visited.find(cur);
if (itv == visited.end())
{
visited.insert(cur);
return !fvs.empty();
}
-bool getVariables(TNode n, std::unordered_set<TNode, TNodeHashFunction>& vs)
+bool getVariables(TNode n, std::unordered_set<TNode>& vs)
{
- std::unordered_set<TNode, TNodeHashFunction> visited;
+ std::unordered_set<TNode> visited;
std::vector<TNode> visit;
TNode cur;
visit.push_back(n);
{
cur = visit.back();
visit.pop_back();
- std::unordered_set<TNode, TNodeHashFunction>::iterator itv =
- visited.find(cur);
+ std::unordered_set<TNode>::iterator itv = visited.find(cur);
if (itv == visited.end())
{
if (cur.isVar())
return !vs.empty();
}
-void getSymbols(TNode n, std::unordered_set<Node, NodeHashFunction>& syms)
+void getSymbols(TNode n, std::unordered_set<Node>& syms)
{
- std::unordered_set<TNode, TNodeHashFunction> visited;
+ std::unordered_set<TNode> visited;
getSymbols(n, syms, visited);
}
void getSymbols(TNode n,
- std::unordered_set<Node, NodeHashFunction>& syms,
- std::unordered_set<TNode, TNodeHashFunction>& visited)
+ std::unordered_set<Node>& syms,
+ std::unordered_set<TNode>& visited)
{
std::vector<TNode> visit;
TNode cur;
void getKindSubterms(TNode n,
Kind k,
bool topLevel,
- std::unordered_set<Node, NodeHashFunction>& ts)
+ std::unordered_set<Node>& ts)
{
- std::unordered_set<TNode, TNodeHashFunction> visited;
+ std::unordered_set<TNode> visited;
std::vector<TNode> visit;
TNode cur;
visit.push_back(n);
} while (!visit.empty());
}
-void getOperatorsMap(
- TNode n,
- std::map<TypeNode, std::unordered_set<Node, NodeHashFunction>>& ops)
+void getOperatorsMap(TNode n, std::map<TypeNode, std::unordered_set<Node>>& ops)
{
- std::unordered_set<TNode, TNodeHashFunction> visited;
+ std::unordered_set<TNode> visited;
getOperatorsMap(n, ops, visited);
}
-void getOperatorsMap(
- TNode n,
- std::map<TypeNode, std::unordered_set<Node, NodeHashFunction>>& ops,
- std::unordered_set<TNode, TNodeHashFunction>& visited)
+void getOperatorsMap(TNode n,
+ std::map<TypeNode, std::unordered_set<Node>>& ops,
+ std::unordered_set<TNode>& visited)
{
// nodes that we still need to visit
std::vector<TNode> visit;
std::vector<Node>& src,
std::vector<Node>& dest)
{
- std::unordered_map<TNode, Node, TNodeHashFunction> visited;
- std::unordered_map<TNode, Node, TNodeHashFunction>::iterator it;
+ std::unordered_map<TNode, Node> visited;
+ std::unordered_map<TNode, Node>::iterator it;
std::vector<TNode> visit;
TNode curr;
visit.push_back(n);
return visited[n];
}
-void getComponentTypes(
- TypeNode t, std::unordered_set<TypeNode, TypeNodeHashFunction>& types)
+void getComponentTypes(TypeNode t, std::unordered_set<TypeNode>& types)
{
std::vector<TypeNode> toProcess;
toProcess.push_back(t);
} while (!toProcess.empty());
}
-bool match(Node x,
- Node y,
- std::unordered_map<Node, Node, NodeHashFunction>& subs)
+bool match(Node x, Node y, std::unordered_map<Node, Node>& subs)
{
std::unordered_set<std::pair<TNode, TNode>, TNodePairHashFunction> visited;
std::unordered_set<std::pair<TNode, TNode>, TNodePairHashFunction>::iterator
it;
- std::unordered_map<Node, Node, NodeHashFunction>::iterator subsIt;
+ std::unordered_map<Node, Node>::iterator subsIt;
std::vector<std::pair<TNode, TNode>> stack;
stack.emplace_back(x, y);
* @return true iff this node contains a free variable.
*/
bool getFreeVariables(TNode n,
- std::unordered_set<Node, NodeHashFunction>& fvs,
+ std::unordered_set<Node>& fvs,
bool computeFv = true);
/**
* Get the free variables in n, that is, the subterms of n of kind
* @return true iff this node contains a free variable.
*/
bool getFreeVariablesScope(TNode n,
- std::unordered_set<Node, NodeHashFunction>& fvs,
- std::unordered_set<TNode, TNodeHashFunction>& scope,
+ std::unordered_set<Node>& fvs,
+ std::unordered_set<TNode>& scope,
bool computeFv = true);
/**
* @param vs The set which free variables are added to
* @return true iff this node contains a free variable.
*/
-bool getVariables(TNode n, std::unordered_set<TNode, TNodeHashFunction>& vs);
+bool getVariables(TNode n, std::unordered_set<TNode>& vs);
/**
* For term n, this function collects the symbols that occur as a subterms
* @param n The node under investigation
* @param syms The set which the symbols of n are added to
*/
-void getSymbols(TNode n, std::unordered_set<Node, NodeHashFunction>& syms);
+void getSymbols(TNode n, std::unordered_set<Node>& syms);
/**
* For term n, this function collects the symbols that occur as a subterms
* @param visited A cache to be used for visited nodes.
*/
void getSymbols(TNode n,
- std::unordered_set<Node, NodeHashFunction>& syms,
- std::unordered_set<TNode, TNodeHashFunction>& visited);
+ std::unordered_set<Node>& syms,
+ std::unordered_set<TNode>& visited);
/**
* For term n, this function collects the subterms of n whose kind is k.
void getKindSubterms(TNode n,
Kind k,
bool topLevel,
- std::unordered_set<Node, NodeHashFunction>& ts);
+ std::unordered_set<Node>& ts);
/**
* For term n, this function collects the operators that occur in n.
* @param ops The map (from each type to operators of that type) which the
* operators of n are added to
*/
-void getOperatorsMap(
- TNode n,
- std::map<TypeNode, std::unordered_set<Node, NodeHashFunction>>& ops);
+void getOperatorsMap(TNode n,
+ std::map<TypeNode, std::unordered_set<Node>>& ops);
/**
* For term n, this function collects the operators that occur in n.
* operators of n are added to
* @param visited A cache to be used for visited nodes.
*/
-void getOperatorsMap(
- TNode n,
- std::map<TypeNode, std::unordered_set<Node, NodeHashFunction>>& ops,
- std::unordered_set<TNode, TNodeHashFunction>& visited);
+void getOperatorsMap(TNode n,
+ std::map<TypeNode, std::unordered_set<Node>>& ops,
+ std::unordered_set<TNode>& visited);
/*
* Substitution of Nodes in a capture avoiding way.
* @param t The type node under investigation
* @param types The set which component types are added to.
*/
-void getComponentTypes(
- TypeNode t, std::unordered_set<TypeNode, TypeNodeHashFunction>& types);
+void getComponentTypes(TypeNode t, std::unordered_set<TypeNode>& types);
/** match
*
* @param subs the mapping from free vars in `n1` to terms in `n2`
* @return whether or not `n2` is an instance of `n1`
*/
-bool match(Node n1,
- Node n2,
- std::unordered_map<Node, Node, NodeHashFunction>& subs);
+bool match(Node n1, Node n2, std::unordered_map<Node, Node>& subs);
} // namespace expr
} // namespace cvc5
// Absent if we haven't visited it.
// Set to `false` if we've already pre-visited it (enqueued its children).
// Set to `true` if we've also already post-visited it.
- std::unordered_map<TNode, bool, TNodeHashFunction> d_visited;
+ std::unordered_map<TNode, bool> d_visited;
// The visit order that this iterator is using
VisitOrder d_order;
std::string identify() const override;
protected:
- typedef context::CDHashMap<Node, std::shared_ptr<ProofNode>, NodeHashFunction>
- NodeProofNodeMap;
+ typedef context::CDHashMap<Node, std::shared_ptr<ProofNode>> NodeProofNodeMap;
/** The proof manager, used for allocating new ProofNode objects */
ProofNodeManager* d_manager;
/** A dummy context used by this class if none is provided */
// after postvisiting SCOPE1: { y: 1 }
// after postvisiting SCOPE2: {}
//
- std::unordered_map<Node, uint32_t, NodeHashFunction> scopeDepth;
+ std::unordered_map<Node, uint32_t> scopeDepth;
std::shared_ptr<ProofNode> cur;
visit.push_back(pn);
do
}
Trace("pnm-scope") << "ProofNodeManager::mkScope " << assumps << std::endl;
// we first ensure the assumptions are flattened
- std::unordered_set<Node, NodeHashFunction> ac{assumps.begin(), assumps.end()};
+ std::unordered_set<Node> ac{assumps.begin(), assumps.end()};
// map from the rewritten form of assumptions to the original. This is only
// computed in the rare case when we need rewriting to match the
// assumptions. An example of this is for Boolean constant equalities in
// scoped proofs from the proof equality engine.
- std::unordered_map<Node, Node, NodeHashFunction> acr;
+ std::unordered_map<Node, Node> acr;
// whether we have compute the map above
bool computedAcr = false;
// The free assumptions of the proof
std::map<Node, std::vector<std::shared_ptr<ProofNode>>> famap;
expr::getFreeAssumptionsMap(pf, famap);
- std::unordered_set<Node, NodeHashFunction> acu;
+ std::unordered_set<Node> acu;
for (const std::pair<const Node, std::vector<std::shared_ptr<ProofNode>>>&
fa : famap)
{
}
}
Node ar = theory::Rewriter::rewrite(a);
- std::unordered_map<Node, Node, NodeHashFunction>::iterator itr =
- acr.find(ar);
+ std::unordered_map<Node, Node>::iterator itr = acr.find(ar);
if (itr != acr.end())
{
aMatch = itr->second;
const std::vector<Node>& vec = s.getVec();
for (const Node& n : vec)
{
- ret = fnv1a::fnv1a_64(ret, NodeHashFunction()(n));
+ ret = fnv1a::fnv1a_64(ret, std::hash<Node>()(n));
}
return ret;
}
<< "SkolemManager::getOriginalForm " << n << std::endl;
OriginalFormAttribute ofa;
NodeManager* nm = NodeManager::currentNM();
- std::unordered_map<TNode, Node, TNodeHashFunction> visited;
- std::unordered_map<TNode, Node, TNodeHashFunction>::iterator it;
+ std::unordered_map<TNode, Node> visited;
+ std::unordered_map<TNode, Node>::iterator it;
std::vector<TNode> visit;
TNode cur;
visit.push_back(n);
protected:
using NodeIndexPairHashFunction =
- PairHashFunction<Node, size_t, NodeHashFunction>;
+ PairHashFunction<Node, size_t, std::hash<Node>>;
typedef context::
CDHashMap<std::pair<Node, size_t>, Node, NodeIndexPairHashFunction>
NodeIndexNodeMap;
// nodes.
// the final rewritten form of terms
- std::unordered_map<Node, Node, TNodeHashFunction> visited;
+ std::unordered_map<Node, Node> visited;
// the rewritten form of terms we have processed so far
- std::unordered_map<Node, Node, TNodeHashFunction> rewritten;
- std::unordered_map<Node, Node, TNodeHashFunction>::iterator it;
- std::unordered_map<Node, Node, TNodeHashFunction>::iterator itr;
+ std::unordered_map<Node, Node> rewritten;
+ std::unordered_map<Node, Node>::iterator it;
+ std::unordered_map<Node, Node>::iterator itr;
std::map<Node, std::shared_ptr<ProofNode> >::iterator itc;
Trace("tconv-pf-gen-rewrite")
<< "TConvProofGenerator::getProofForRewriting: " << toStringDebug()
std::shared_ptr<ProofNode> getProofForRewriting(Node n);
protected:
- typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeNodeMap;
+ typedef context::CDHashMap<Node, Node> NodeNodeMap;
/** A dummy context used by this class if none is provided */
context::Context d_context;
/** The (lazy) context dependent proof object. */
TypeNode TypeNode::s_null( &expr::NodeValue::null() );
-TypeNode TypeNode::substitute(const TypeNode& type,
- const TypeNode& replacement,
- std::unordered_map<TypeNode, TypeNode, HashFunction>& cache) const {
+TypeNode TypeNode::substitute(
+ const TypeNode& type,
+ const TypeNode& replacement,
+ std::unordered_map<TypeNode, TypeNode>& cache) const
+{
// in cache?
- std::unordered_map<TypeNode, TypeNode, HashFunction>::const_iterator i = cache.find(*this);
+ std::unordered_map<TypeNode, TypeNode>::const_iterator i = cache.find(*this);
if(i != cache.end()) {
return (*i).second;
}
}
} // namespace cvc5
+
+namespace std {
+
+size_t hash<cvc5::TypeNode>::operator()(const cvc5::TypeNode& tn) const
+{
+ return tn.getId();
+}
+
+} // namespace std
*/
class TypeNode {
-public:
-
- // for hash_maps, hash_sets..
- struct HashFunction {
- size_t operator()(TypeNode node) const {
- return (size_t) node.getId();
- }
- };/* struct HashFunction */
-
private:
/**
* Cache-aware, recursive version of substitute() used by the public
* member function with a similar signature.
*/
- TypeNode substitute(const TypeNode& type, const TypeNode& replacement,
- std::unordered_map<TypeNode, TypeNode, HashFunction>& cache) const;
+ TypeNode substitute(const TypeNode& type,
+ const TypeNode& replacement,
+ std::unordered_map<TypeNode, TypeNode>& cache) const;
/**
* Cache-aware, recursive version of substitute() used by the public
* member function with a similar signature.
*/
template <class Iterator1, class Iterator2>
- TypeNode substitute(Iterator1 typesBegin, Iterator1 typesEnd,
- Iterator2 replacementsBegin, Iterator2 replacementsEnd,
- std::unordered_map<TypeNode, TypeNode, HashFunction>& cache) const;
-
-public:
+ TypeNode substitute(Iterator1 typesBegin,
+ Iterator1 typesEnd,
+ Iterator2 replacementsBegin,
+ Iterator2 replacementsEnd,
+ std::unordered_map<TypeNode, TypeNode>& cache) const;
+ public:
/** Default constructor, makes a null expression. */
TypeNode() : d_nv(&expr::NodeValue::null()) { }
return out;
}
-typedef TypeNode::HashFunction TypeNodeHashFunction;
-
} // namespace cvc5
+namespace std {
+
+template <>
+struct hash<cvc5::TypeNode>
+{
+ size_t operator()(const cvc5::TypeNode& tn) const;
+};
+
+} // namespace std
+
#include "expr/node_manager.h"
namespace cvc5 {
inline TypeNode
TypeNode::substitute(const TypeNode& type,
const TypeNode& replacement) const {
- std::unordered_map<TypeNode, TypeNode, HashFunction> cache;
+ std::unordered_map<TypeNode, TypeNode> cache;
return substitute(type, replacement, cache);
}
Iterator1 typesEnd,
Iterator2 replacementsBegin,
Iterator2 replacementsEnd) const {
- std::unordered_map<TypeNode, TypeNode, HashFunction> cache;
+ std::unordered_map<TypeNode, TypeNode> cache;
return substitute(typesBegin, typesEnd,
replacementsBegin, replacementsEnd, cache);
}
template <class Iterator1, class Iterator2>
-TypeNode TypeNode::substitute(Iterator1 typesBegin,
- Iterator1 typesEnd,
- Iterator2 replacementsBegin,
- Iterator2 replacementsEnd,
- std::unordered_map<TypeNode, TypeNode, HashFunction>& cache) const {
+TypeNode TypeNode::substitute(
+ Iterator1 typesBegin,
+ Iterator1 typesEnd,
+ Iterator2 replacementsBegin,
+ Iterator2 replacementsEnd,
+ std::unordered_map<TypeNode, TypeNode>& cache) const
+{
// in cache?
- std::unordered_map<TypeNode, TypeNode, HashFunction>::const_iterator i = cache.find(*this);
+ std::unordered_map<TypeNode, TypeNode>::const_iterator i = cache.find(*this);
if(i != cache.end()) {
return (*i).second;
}
size_t UninterpretedConstantHashFunction::operator()(
const UninterpretedConstant& uc) const
{
- return TypeNodeHashFunction()(uc.getType())
+ return std::hash<TypeNode>()(uc.getType())
* IntegerHashFunction()(uc.getIndex());
}
* a sufficient bit-vector size.
* Populate usVarsToBVVars so that it maps variables with uninterpreted sort to
* the fresh skolem BV variables. variables */
-void collectUSortsToBV(const std::unordered_set<TNode, TNodeHashFunction>& vars,
+void collectUSortsToBV(const std::unordered_set<TNode>& vars,
const USortToBVSizeMap& usortCardinality,
SubstitutionMap& usVarsToBVVars)
{
/* This function returns the list of terms with uninterpreted sort in the
* formula represented by assertions. */
-std::unordered_set<TNode, TNodeHashFunction> getVarsWithUSorts(
- AssertionPipeline* assertions)
+std::unordered_set<TNode> getVarsWithUSorts(AssertionPipeline* assertions)
{
- std::unordered_set<TNode, TNodeHashFunction> res;
+ std::unordered_set<TNode> res;
for (const Node& assertion : assertions->ref())
{
- std::unordered_set<TNode, TNodeHashFunction> vars;
+ std::unordered_set<TNode> vars;
expr::getVariables(assertion, vars);
for (const TNode& var : vars)
USortToBVSizeMap& usortCardinality,
SubstitutionMap& usVarsToBVVars)
{
- std::unordered_set<TNode, TNodeHashFunction> toProcess =
- getVarsWithUSorts(assertions);
+ std::unordered_set<TNode> toProcess = getVarsWithUSorts(assertions);
if (toProcess.size() > 0)
{
namespace preprocessing {
namespace passes {
-using TNodeSet = std::unordered_set<TNode, TNodeHashFunction>;
-using FunctionToArgsMap =
- std::unordered_map<TNode, TNodeSet, TNodeHashFunction>;
-using USortToBVSizeMap =
- std::unordered_map<TypeNode, size_t, TypeNode::HashFunction>;
+using TNodeSet = std::unordered_set<TNode>;
+using FunctionToArgsMap = std::unordered_map<TNode, TNodeSet>;
+using USortToBVSizeMap = std::unordered_map<TypeNode, size_t>;
class Ackermann : public PreprocessingPass
{
{
std::vector<TNode> to_visit;
to_visit.push_back(node);
- std::unordered_set<TNode, TNodeHashFunction> visited;
+ std::unordered_set<TNode> visited;
while (!to_visit.empty())
{
{
std::vector<TNode> visit;
visit.push_back(node);
- std::unordered_set<TNode, TNodeHashFunction> visited;
+ std::unordered_set<TNode> visited;
while (!visit.empty())
{
Note: it only keeps mappings for ITEs of type bit-vector.
Other ITEs will be in the d_lowerCache
*/
- std::unordered_map<Node, Node, NodeHashFunction> d_iteBVLowerCache;
+ std::unordered_map<Node, Node> d_iteBVLowerCache;
/** Keeps track of other lowered nodes
-- will be cleared periodically in ITE mode
*/
- std::unordered_map<Node, Node, NodeHashFunction> d_lowerCache;
+ std::unordered_map<Node, Node> d_lowerCache;
/** Stores the bool-to-bv mode option */
options::BoolToBVMode d_boolToBVMode;
{
std::vector<Node> visit;
/* Maps visited nodes to the determined minimum bit-width required. */
- std::unordered_map<Node, unsigned, NodeHashFunction> visited;
- std::unordered_map<Node, unsigned, NodeHashFunction>::iterator it;
+ std::unordered_map<Node, unsigned> visited;
+ std::unordered_map<Node, unsigned>::iterator it;
visit.push_back(expr);
while (!visit.empty())
* of the form 'unknown = mapped result' in applyInternal.
*/
BVGauss::Result BVGauss::gaussElimRewriteForUrem(
- const std::vector<Node>& equations,
- std::unordered_map<Node, Node, NodeHashFunction>& res)
+ const std::vector<Node>& equations, std::unordered_map<Node, Node>& res)
{
Assert(res.empty());
Node prime;
Integer iprime;
- std::unordered_map<Node, std::vector<Integer>, NodeHashFunction> vars;
+ std::unordered_map<Node, std::vector<Integer>> vars;
size_t neqs = equations.size();
std::vector<Integer> rhs;
std::vector<std::vector<Integer>> lhs =
std::vector<std::vector<Integer>>(neqs, std::vector<Integer>());
- res = std::unordered_map<Node, Node, NodeHashFunction>();
+ res = std::unordered_map<Node, Node>();
for (size_t i = 0; i < neqs; ++i)
{
iprime = get_bv_const_value(prime);
}
- std::unordered_map<Node, Integer, NodeHashFunction> tmp;
+ std::unordered_map<Node, Integer> tmp;
std::vector<Node> stack;
stack.push_back(urem[0]);
while (!stack.empty())
AssertionPipeline* assertionsToPreprocess)
{
std::vector<Node> assertions(assertionsToPreprocess->ref());
- std::unordered_map<Node, std::vector<Node>, NodeHashFunction> equations;
+ std::unordered_map<Node, std::vector<Node>> equations;
while (!assertions.empty())
{
}
}
- std::unordered_map<Node, Node, NodeHashFunction> subst;
+ std::unordered_map<Node, Node> subst;
NodeManager* nm = NodeManager::currentNM();
for (const auto& eq : equations)
{
if (eq.second.size() <= 1) { continue; }
- std::unordered_map<Node, Node, NodeHashFunction> res;
+ std::unordered_map<Node, Node> res;
BVGauss::Result ret = gaussElimRewriteForUrem(eq.second, res);
Trace("bv-gauss-elim") << "result: "
<< (ret == BVGauss::Result::INVALID
std::vector<Integer>& rhs,
std::vector<std::vector<Integer>>& lhs);
- static Result gaussElimRewriteForUrem(
- const std::vector<Node>& equations,
- std::unordered_map<Node, Node, NodeHashFunction>& res);
+ static Result gaussElimRewriteForUrem(const std::vector<Node>& equations,
+ std::unordered_map<Node, Node>& res);
static unsigned getMinBwExpr(Node expr);
};
namespace preprocessing {
namespace passes {
-using NodeMap = std::unordered_map<Node, Node, NodeHashFunction>;
+using NodeMap = std::unordered_map<Node, Node>;
using namespace cvc5::theory;
namespace {
PreprocessingPassResult BvIntroPow2::applyInternal(
AssertionPipeline* assertionsToPreprocess)
{
- std::unordered_map<Node, Node, NodeHashFunction> cache;
+ std::unordered_map<Node, Node> cache;
for (unsigned i = 0, size = assertionsToPreprocess->size(); i < size; ++i)
{
Node cur = (*assertionsToPreprocess)[i];
namespace preprocessing {
namespace passes {
-typedef std::unordered_map<Node, Node, NodeHashFunction> NodeNodeMap;
+typedef std::unordered_map<Node, Node> NodeNodeMap;
class BVToBool : public PreprocessingPass
{
namespace preprocessing {
namespace passes {
-using CDNodeMap = context::CDHashMap<Node, Node, NodeHashFunction>;
+using CDNodeMap = context::CDHashMap<Node, Node>;
class BVToInt : public PreprocessingPass
{
* A set of constraints of the form 0 <= x < 2^k
* These are added for every new integer variable that we introduce.
*/
- context::CDHashSet<Node, NodeHashFunction> d_rangeAssertions;
+ context::CDHashSet<Node> d_rangeAssertions;
/**
* Useful constants
namespace preprocessing {
namespace passes {
-using CDNodeMap = context::CDHashMap<Node, Node, NodeHashFunction>;
+using CDNodeMap = context::CDHashMap<Node, Node>;
class ForeignTheoryRewrite : public PreprocessingPass
{
// collect free variables in all assertions
std::vector<Node> free_vars;
std::vector<TNode> visit;
- std::unordered_set<TNode, TNodeHashFunction> visited;
+ std::unordered_set<TNode> visited;
for (const Node& as : assertions)
{
Trace("cegqi-gn") << " " << as << std::endl;
{
NodeManager* nm = NodeManager::currentNM();
SkolemManager* sm = nm->getSkolemManager();
- std::unordered_map<Node, Node, TNodeHashFunction>::iterator it;
+ std::unordered_map<Node, Node>::iterator it;
std::vector<Node> visit;
TNode cur;
visit.push_back(n);
// must also get free variables in lambda
std::vector<Node> lvars;
std::vector<TypeNode> ftypes;
- std::unordered_set<Node, NodeHashFunction> fvs;
+ std::unordered_set<Node> fvs;
expr::getFreeVariables(cur, fvs);
std::vector<Node> nvars;
std::vector<Node> vars;
Trace("ho-elim-assert") << "Ho-elim assertion: " << n << std::endl;
NodeManager* nm = NodeManager::currentNM();
SkolemManager* sm = nm->getSkolemManager();
- std::unordered_map<Node, Node, NodeHashFunction>::iterator it;
+ std::unordered_map<Node, Node>::iterator it;
std::map<Node, Node> preReplace;
std::map<Node, Node>::iterator itr;
std::vector<TNode> visit;
<< std::endl;
if (typeChanged)
{
- std::unordered_map<TNode, Node, TNodeHashFunction>::iterator ito =
+ std::unordered_map<TNode, Node>::iterator ito =
d_visited_op.find(op);
if (ito == d_visited_op.end())
{
* Stores the set of nodes we have current visited and their results
* in steps [1] and [2] of this pass.
*/
- std::unordered_map<Node, Node, NodeHashFunction> d_visited;
+ std::unordered_map<Node, Node> d_visited;
/**
* Stores the mapping from functions f to their corresponding function H(f)
* in the encoding for step [2] of this pass.
*/
- std::unordered_map<TNode, Node, TNodeHashFunction> d_visited_op;
+ std::unordered_map<TNode, Node> d_visited_op;
/** The set of all function types encountered in assertions. */
- std::unordered_set<TypeNode, TypeNodeHashFunction> d_funTypes;
+ std::unordered_set<TypeNode> d_funTypes;
/**
* Get ho apply uf, this returns App_{@_{T1 x T2 ... x Tn -> T}}
using namespace std;
using namespace cvc5::theory;
-using NodeMap = std::unordered_map<Node, Node, NodeHashFunction>;
+using NodeMap = std::unordered_map<Node, Node>;
namespace {
Node zero = nm->mkConst(Rational(0)), one = nm->mkConst(Rational(1));
Node trueNode = nm->mkConst(true);
- unordered_map<TNode, Node, TNodeHashFunction> intVars;
+ unordered_map<TNode, Node> intVars;
for (TNode v0 : d_boolVars)
{
if (propagator->isAssigned(v0))
PreprocessingPassResult NlExtPurify::applyInternal(
AssertionPipeline* assertionsToPreprocess)
{
- unordered_map<Node, Node, NodeHashFunction> cache;
- unordered_map<Node, Node, NodeHashFunction> bcache;
+ unordered_map<Node, Node> cache;
+ unordered_map<Node, Node> bcache;
std::vector<Node> var_eq;
unsigned size = assertionsToPreprocess->size();
for (unsigned i = 0; i < size; ++i)
namespace preprocessing {
namespace passes {
-using NodeMap = std::unordered_map<Node, Node, NodeHashFunction>;
+using NodeMap = std::unordered_map<Node, Node>;
class NlExtPurify : public PreprocessingPass
{
<< "Resize non-clausal learned literals to " << j << std::endl;
learned_literals.resize(j);
- std::unordered_set<TNode, TNodeHashFunction> s;
+ std::unordered_set<TNode> s;
for (size_t i = 0, size = assertionsToPreprocess->size(); i < size; ++i)
{
Node assertion = (*assertionsToPreprocess)[i];
static Node mkGeqOne(Node v);
// x -> <geqZero, leqOne>
- typedef context::CDHashMap<Node, std::pair<Node, Node>, NodeHashFunction>
- CDNode2PairMap;
+ typedef context::CDHashMap<Node, std::pair<Node, Node>> CDNode2PairMap;
CDNode2PairMap d_pbBounds;
theory::SubstitutionMap d_subCache;
- typedef std::unordered_set<Node, NodeHashFunction> NodeSet;
+ typedef std::unordered_set<Node> NodeSet;
NodeSet d_learningCache;
context::CDO<unsigned> d_pbs;
class RealToInt : public PreprocessingPass
{
- using NodeMap = context::CDHashMap<Node, Node, NodeHashFunction>;
+ using NodeMap = context::CDHashMap<Node, Node>;
public:
RealToInt(PreprocessingPassContext* preprocContext);
std::vector<Node> free_functions;
std::vector<TNode> visit;
- std::unordered_set<TNode, TNodeHashFunction> visited;
+ std::unordered_set<TNode> visited;
// add top-level conjuncts to eassertions
std::vector<Node> assertions_proc = assertions;
NodeManager* nm = NodeManager::currentNM();
// initialize the candidate rewrite
- std::unordered_map<TNode, bool, TNodeHashFunction> visited;
- std::unordered_map<TNode, bool, TNodeHashFunction>::iterator it;
+ std::unordered_map<TNode, bool> visited;
+ std::unordered_map<TNode, bool>::iterator it;
std::vector<TNode> visit;
// Get all usable terms from the input. A term is usable if it does not
// contain a quantified subterm
{
NodeManager* nm = NodeManager::currentNM();
TheoryEngine* te = d_preprocContext->getTheoryEngine();
- std::unordered_map<TNode, Node, TNodeHashFunction> visited;
- std::unordered_map<TNode, Node, TNodeHashFunction>::iterator it;
+ std::unordered_map<TNode, Node> visited;
+ std::unordered_map<TNode, Node>::iterator it;
std::vector<TNode> visit;
TNode cur;
visit.push_back(n);
/** number of expressions eliminated due to unconstrained simplification */
IntStat d_numUnconstrainedElim;
- using TNodeCountMap = std::unordered_map<TNode, unsigned, TNodeHashFunction>;
- using TNodeMap = std::unordered_map<TNode, TNode, TNodeHashFunction>;
- using TNodeSet = std::unordered_set<TNode, TNodeHashFunction>;
+ using TNodeCountMap = std::unordered_map<TNode, unsigned>;
+ using TNodeMap = std::unordered_map<TNode, TNode>;
+ using TNodeSet = std::unordered_set<TNode>;
TNodeCountMap d_visited;
TNodeMap d_visitedOnce;
void PreprocessingPassContext::recordSymbolsInAssertions(
const std::vector<Node>& assertions)
{
- std::unordered_set<TNode, TNodeHashFunction> visited;
- std::unordered_set<Node, NodeHashFunction> syms;
+ std::unordered_set<TNode> visited;
+ std::unordered_set<Node> syms;
for (TNode cn : assertions)
{
expr::getSymbols(cn, syms, visited);
return d_circuitPropagator;
}
- context::CDHashSet<Node, NodeHashFunction>& getSymsInAssertions()
- {
- return d_symsInAssertions;
- }
+ context::CDHashSet<Node>& getSymsInAssertions() { return d_symsInAssertions; }
void spendResource(Resource r);
* The (user-context-dependent) set of symbols that occur in at least one
* assertion in the current user context.
*/
- context::CDHashSet<Node, NodeHashFunction> d_symsInAssertions;
+ context::CDHashSet<Node> d_symsInAssertions;
}; // class PreprocessingPassContext
return true;
}
- unordered_map<Node, bool, NodeHashFunction>::iterator it;
+ unordered_map<Node, bool>::iterator it;
it = d_leavesConstCache.find(e);
if (it != d_leavesConstCache.end())
{
Node ITESimplifier::getSimpVar(TypeNode t)
{
- std::unordered_map<TypeNode, Node, TypeNode::HashFunction>::iterator it;
+ std::unordered_map<TypeNode, Node>::iterator it;
it = d_simpVars.find(t);
if (it != d_simpVars.end())
{
d_simpContextCache[c] = result;
return result;
}
-typedef std::unordered_set<Node, NodeHashFunction> NodeSet;
+typedef std::unordered_set<Node> NodeSet;
void countReachable_(Node x, Kind k, NodeSet& visited, uint32_t& reached)
{
if (visited.find(x) != visited.end())
size_t cache_size() const { return d_cache.size(); }
private:
- typedef std::unordered_map<Node, bool, NodeHashFunction> NodeBoolMap;
+ typedef std::unordered_map<Node, bool> NodeBoolMap;
NodeBoolMap d_cache;
};
void clear();
private:
- typedef std::unordered_map<Node, uint32_t, NodeHashFunction> NodeCountMap;
+ typedef std::unordered_map<Node, uint32_t> NodeCountMap;
NodeCountMap d_reachCount;
bool d_skipVariables;
size_t cache_size() const;
private:
- typedef std::unordered_map<Node, uint32_t, NodeHashFunction> NodeCountMap;
+ typedef std::unordered_map<Node, uint32_t> NodeCountMap;
NodeCountMap d_termITEHeight;
}; /* class TermITEHeightCounter */
AssertionPipeline* d_assertions;
IncomingArcCounter d_incoming;
- typedef std::unordered_map<Node, Node, NodeHashFunction> NodeMap;
+ typedef std::unordered_map<Node, Node> NodeMap;
NodeMap d_compressed;
void reset();
// constant
// or termITE(cnd, ConstantIte, ConstantIte)
typedef std::vector<Node> NodeVec;
- typedef std::unordered_map<Node, NodeVec*, NodeHashFunction>
- ConstantLeavesMap;
+ typedef std::unordered_map<Node, NodeVec*> ConstantLeavesMap;
ConstantLeavesMap d_constantLeaves;
// d_constantLeaves satisfies the following invariants:
typedef std::pair<Node, Node> NodePair;
using NodePairHashFunction =
- PairHashFunction<Node, Node, NodeHashFunction, NodeHashFunction>;
+ PairHashFunction<Node, Node, std::hash<Node>, std::hash<Node>>;
typedef std::unordered_map<NodePair, Node, NodePairHashFunction> NodePairMap;
NodePairMap d_constantIteEqualsConstantCache;
NodePairMap d_replaceOverCache;
Node replaceOver(Node n, Node replaceWith, Node simpVar);
Node replaceOverTermIte(Node term, Node simpAtom, Node simpVar);
- std::unordered_map<Node, bool, NodeHashFunction> d_leavesConstCache;
+ std::unordered_map<Node, bool> 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;
+ std::unordered_map<TypeNode, Node> d_simpVars;
Node getSimpVar(TypeNode t);
- typedef std::unordered_map<Node, Node, NodeHashFunction> NodeMap;
+ typedef std::unordered_map<Node, Node> NodeMap;
NodeMap d_simpContextCache;
Node createSimpContext(TNode c, Node& iteNode, Node& simpVar);
Node d_true;
Node d_false;
- typedef std::unordered_map<TNode, Node, TNodeHashFunction> TNodeMap;
+ typedef std::unordered_map<TNode, Node> TNodeMap;
class CareSetPtr;
class CareSetPtrVal
return n;
}
NodeManager* nm = NodeManager::currentNM();
- std::unordered_map<TNode, Node, TNodeHashFunction> visited;
- std::unordered_map<TNode, Node, TNodeHashFunction>::iterator it;
+ std::unordered_map<TNode, Node> visited;
+ std::unordered_map<TNode, Node>::iterator it;
std::vector<TNode> visit;
TNode cur;
visit.push_back(n);
class LetBinding
{
using NodeList = context::CDList<Node>;
- using NodeIdMap = context::CDHashMap<Node, uint32_t, NodeHashFunction>;
+ using NodeIdMap = context::CDHashMap<Node, uint32_t>;
public:
LetBinding(uint32_t thresh = 2);
class CnfProof;
-typedef std::unordered_map<Node, Node, NodeHashFunction> NodeToNode;
+typedef std::unordered_map<Node, Node> NodeToNode;
typedef std::unordered_set<ClauseId> ClauseIdSet;
typedef context::CDHashMap<ClauseId, Node> ClauseIdToNode;
typedef std::pair<Node, Node> NodePair;
typedef std::set<NodePair> NodePairSet;
-typedef std::unordered_set<Node, NodeHashFunction> NodeSet;
+typedef std::unordered_set<Node> NodeSet;
class CnfProof {
protected:
} // namespace prop
typedef std::unordered_map<ClauseId, prop::SatClause*> IdToSatClause;
-typedef context::CDHashSet<Node, NodeHashFunction> CDNodeSet;
-typedef context::CDHashMap<Node, std::vector<Node>, NodeHashFunction> CDNodeToNodes;
+typedef context::CDHashSet<Node> CDNodeSet;
+typedef context::CDHashMap<Node, std::vector<Node>> CDNodeToNodes;
typedef std::unordered_set<ClauseId> IdHashSet;
class ProofManager {
LiteralToNodeMap;
/** Cache of what literals have been registered to a node. */
- typedef context::CDInsertHashMap<Node, SatLiteral, NodeHashFunction>
- NodeToLiteralMap;
+ typedef context::CDInsertHashMap<Node, SatLiteral> NodeToLiteralMap;
/**
* Constructs a CnfStream that performs equisatisfiable CNF transformations
context::CDList<TNode> d_booleanVariables;
/** Formulas that we translated that we are notifying */
- context::CDHashSet<Node, NodeHashFunction> d_notifyFormulas;
+ context::CDHashSet<Node> d_notifyFormulas;
/** Map from nodes to literals */
NodeToLiteralMap d_nodeToLiteralMap;
!negated);
}
-void SatProofManager::explainLit(
- SatLiteral lit, std::unordered_set<TNode, TNodeHashFunction>& premises)
+void SatProofManager::explainLit(SatLiteral lit,
+ std::unordered_set<TNode>& premises)
{
Trace("sat-proof") << push << "SatProofManager::explainLit: Lit: " << lit;
Node litNode = getClauseNode(lit);
{
continue;
}
- std::unordered_set<TNode, TNodeHashFunction> childPremises;
+ std::unordered_set<TNode> childPremises;
explainLit(~currLit, childPremises);
// save to resolution chain premises / arguments
Assert(d_cnfStream->getNodeCache().find(currLit)
Trace("sat-proof-debug2")
<< push << "SatProofManager::finalizeProof: saved proofs in chain:\n";
std::map<Node, std::shared_ptr<ProofNode>> links = d_resChains.getLinks();
- std::unordered_set<Node, NodeHashFunction> skip;
+ std::unordered_set<Node> skip;
for (const std::pair<const Node, std::shared_ptr<ProofNode>>& link : links)
{
if (skip.count(link.first))
// we call explainLit on each ~l_i while accumulating the children and
// arguments for the resolution step to conclude false.
std::vector<Node> children{inConflictNode}, args;
- std::unordered_set<TNode, TNodeHashFunction> premises;
+ std::unordered_set<TNode> premises;
for (unsigned i = 0, size = inConflict.size(); i < size; ++i)
{
Assert(d_cnfStream->getNodeCache().find(inConflict[i])
!= d_cnfStream->getNodeCache().end());
- std::unordered_set<TNode, TNodeHashFunction> childPremises;
+ std::unordered_set<TNode> childPremises;
explainLit(~inConflict[i], childPremises);
Node negatedLitNode = d_cnfStream->getNodeCache()[~inConflict[i]];
// save to resolution chain premises / arguments
// mark another iteration for the loop, as some resolution link may be
// connected because of the new justifications
expanded = true;
- std::unordered_set<TNode, TNodeHashFunction> childPremises;
+ std::unordered_set<TNode> childPremises;
explainLit(it->second, childPremises);
// add the premises used in the justification. We know they will have
// been as expanded as possible
* have been used as premises of resolution steps while explaining
* propagations
*/
- void explainLit(prop::SatLiteral lit,
- std::unordered_set<TNode, TNodeHashFunction>& premises);
+ void explainLit(prop::SatLiteral lit, std::unordered_set<TNode>& premises);
/** Build refutation proof starting from conflict clause
*
/** All clauses added to the SAT solver, kept in a context-dependent manner.
*/
- context::CDHashSet<Node, NodeHashFunction> d_assumptions;
+ context::CDHashSet<Node> d_assumptions;
/**
* A placeholder that may be used to store the literal with the final
std::vector<TNode>& activatedSkolems,
bool useDefs)
{
- std::unordered_set<Node, NodeHashFunction> skolems;
+ std::unordered_set<Node> skolems;
getSkolems(literal, skolems);
for (const Node& k : skolems)
{
bool SkolemDefManager::hasSkolems(TNode n) const
{
- std::unordered_set<TNode, TNodeHashFunction> visited;
- std::unordered_set<TNode, TNodeHashFunction>::iterator it;
+ std::unordered_set<TNode> visited;
+ std::unordered_set<TNode>::iterator it;
std::vector<TNode> visit;
TNode cur;
visit.push_back(n);
return n.getAttribute(HasSkolemAttr());
}
-void SkolemDefManager::getSkolems(
- TNode n, std::unordered_set<Node, NodeHashFunction>& skolems) const
+void SkolemDefManager::getSkolems(TNode n,
+ std::unordered_set<Node>& skolems) const
{
- std::unordered_set<TNode, TNodeHashFunction> visited;
- std::unordered_set<TNode, TNodeHashFunction>::iterator it;
+ std::unordered_set<TNode> visited;
+ std::unordered_set<TNode>::iterator it;
std::vector<TNode> visit;
TNode cur;
visit.push_back(n);
*/
class SkolemDefManager
{
- using NodeNodeMap = context::CDInsertHashMap<Node, Node, NodeHashFunction>;
- using NodeSet = context::CDHashSet<Node, NodeHashFunction>;
+ using NodeNodeMap = context::CDInsertHashMap<Node, Node>;
+ using NodeSet = context::CDHashSet<Node>;
public:
SkolemDefManager(context::Context* context,
* @param n The node to traverse
* @param skolems The set where the skolems are added
*/
- void getSkolems(TNode n,
- std::unordered_set<Node, NodeHashFunction>& skolems) const;
+ void getSkolems(TNode n, std::unordered_set<Node>& skolems) const;
/** Does n have skolems having definitions managed by this class? */
bool hasSkolems(TNode n) const;
std::vector<Node>& skAsserts,
std::vector<Node>& sks)
{
- std::unordered_set<Node, NodeHashFunction> skolems;
+ std::unordered_set<Node> skolems;
d_skdm->getSkolems(node, skolems);
for (const Node& k : skolems)
{
* Set of all lemmas that have been "shared" in the portfolio---i.e.,
* all imported and exported lemmas.
*/
- std::unordered_set<Node, NodeHashFunction> d_shared;
+ std::unordered_set<Node> d_shared;
/** The theory preprocessor */
theory::TheoryPreprocessor d_tpp;
*/
class AbstractValues
{
- typedef std::unordered_map<Node, Node, NodeHashFunction> NodeToNodeHashMap;
+ typedef std::unordered_map<Node, Node> NodeToNodeHashMap;
+
public:
AbstractValues(NodeManager* nm);
~AbstractValues();
theory::SubstitutionMap& sm = d_env.getTopLevelSubstitutions().get();
Trace("check-model") << "checkModel: Check assertions..." << std::endl;
- std::unordered_map<Node, Node, NodeHashFunction> cache;
+ std::unordered_map<Node, Node> cache;
// the list of assertions that did not rewrite to true
std::vector<Node> noCheckList;
// Now go through all our user assertions checking if they're satisfied.
ExpandDefs::~ExpandDefs() {}
-Node ExpandDefs::expandDefinitions(
- TNode n, std::unordered_map<Node, Node, NodeHashFunction>& cache)
+Node ExpandDefs::expandDefinitions(TNode n,
+ std::unordered_map<Node, Node>& cache)
{
TrustNode trn = expandDefinitions(n, cache, nullptr);
return trn.isNull() ? Node(n) : trn.getNode();
}
-TrustNode ExpandDefs::expandDefinitions(
- TNode n,
- std::unordered_map<Node, Node, NodeHashFunction>& cache,
- TConvProofGenerator* tpg)
+TrustNode ExpandDefs::expandDefinitions(TNode n,
+ std::unordered_map<Node, Node>& cache,
+ TConvProofGenerator* tpg)
{
const TNode orig = n;
std::stack<std::tuple<Node, Node, bool>> worklist;
}
// maybe it's in the cache
- std::unordered_map<Node, Node, NodeHashFunction>::iterator cacheHit =
- cache.find(n);
+ std::unordered_map<Node, Node>::iterator cacheHit = cache.find(n);
if (cacheHit != cache.end())
{
TNode ret = (*cacheHit).second;
* @param cache Cache of previous results
* @return The expanded term.
*/
- Node expandDefinitions(
- TNode n, std::unordered_map<Node, Node, NodeHashFunction>& cache);
+ Node expandDefinitions(TNode n, std::unordered_map<Node, Node>& cache);
/**
* Set proof node manager, which signals this class to enable proofs using the
* Helper function for above, called to specify if we want proof production
* based on the optional argument tpg.
*/
- theory::TrustNode expandDefinitions(
- TNode n,
- std::unordered_map<Node, Node, NodeHashFunction>& cache,
- TConvProofGenerator* tpg);
+ theory::TrustNode expandDefinitions(TNode n,
+ std::unordered_map<Node, Node>& cache,
+ TConvProofGenerator* tpg);
/** Reference to the environment. */
Env& d_env;
/** Reference to the SMT stats */
}
Node formula = asserts.size() > 1 ? nm->mkNode(AND, asserts) : asserts[0];
- std::unordered_map<TNode, Node, TNodeHashFunction> visited;
- std::unordered_map<TNode, Node, TNodeHashFunction> implicant;
- std::unordered_map<TNode, Node, TNodeHashFunction>::iterator it;
+ std::unordered_map<TNode, Node> visited;
+ std::unordered_map<TNode, Node> implicant;
+ std::unordered_map<TNode, Node>::iterator it;
std::vector<TNode> visit;
TNode cur;
visit.push_back(formula);
{
Trace("model-blocker")
<< "no specific terms to block recognized" << std::endl;
- std::unordered_set<Node, NodeHashFunction> symbols;
+ std::unordered_set<Node> symbols;
for (Node n : tlAsserts)
{
expr::getSymbols(n, symbols);
// otherwise, block all terms that were specified in get-value
else
{
- std::unordered_set<Node, NodeHashFunction> terms;
+ std::unordered_set<Node> terms;
for (Node n : nodesToBlock)
{
Node v = m->getValue(n);
std::vector<Node> vars;
std::vector<Node> subs;
Trace("model-core") << "Assignments: " << std::endl;
- std::unordered_set<TNode, TNodeHashFunction> visited;
+ std::unordered_set<TNode> visited;
std::vector<TNode> visit;
TNode cur;
visit.push_back(formula);
<< ") input " << f << std::endl;
Node curr = f;
std::vector<Node> transChildren;
- std::unordered_set<Node, NodeHashFunction> processed;
+ std::unordered_set<Node> processed;
bool success;
// we connect the proof of f to its source via the map d_src until we
// discover that its source is a preprocessing lemma (a lemma stored in d_src)
*/
class PreprocessProofGenerator : public ProofGenerator
{
- typedef context::CDHashMap<Node, theory::TrustNode, NodeHashFunction>
- NodeTrustNodeMap;
+ typedef context::CDHashMap<Node, theory::TrustNode> NodeTrustNodeMap;
public:
/**
Node Preprocessor::expandDefinitions(const Node& n)
{
- std::unordered_map<Node, Node, NodeHashFunction> cache;
+ std::unordered_map<Node, Node> cache;
return expandDefinitions(n, cache);
}
-Node Preprocessor::expandDefinitions(
- const Node& node, std::unordered_map<Node, Node, NodeHashFunction>& cache)
+Node Preprocessor::expandDefinitions(const Node& node,
+ std::unordered_map<Node, Node>& cache)
{
Trace("smt") << "SMT expandDefinitions(" << node << ")" << endl;
// Substitute out any abstract values in node.
*/
Node expandDefinitions(const Node& n);
/** Same as above, with a cache of previous results. */
- Node expandDefinitions(
- const Node& n, std::unordered_map<Node, Node, NodeHashFunction>& cache);
+ Node expandDefinitions(const Node& n, std::unordered_map<Node, Node>& cache);
/**
* Set proof node manager. Enables proofs in this preprocessor.
*/
{
/** The types for the recursive function definitions */
typedef context::CDList<Node> NodeList;
- typedef std::unordered_map<Node, bool, NodeHashFunction> NodeToBoolHashMap;
+ typedef std::unordered_map<Node, bool> NodeToBoolHashMap;
public:
ProcessAssertions(SmtEngine& smt,
// get crowding lits and the position of the last clause that includes
// them. The factoring step must be added after the last inclusion and before
// its elimination.
- std::unordered_set<TNode, TNodeHashFunction> crowding;
+ std::unordered_set<TNode> crowding;
std::vector<std::pair<Node, size_t>> lastInclusion;
// positions of eliminators of crowding literals, which are the positions of
// the clauses that eliminate crowding literals *after* their last inclusion
// We build it rather than taking conclusionLits because the order may be
// different
std::vector<Node> factoredLits;
- std::unordered_set<TNode, TNodeHashFunction> clauseSet;
+ std::unordered_set<TNode> clauseSet;
for (size_t i = 0, size = chainConclusionLits.size(); i < size; ++i)
{
if (clauseSet.count(chainConclusionLits[i]))
std::vector<Node> easserts = getAssertions();
// must expand definitions
std::vector<Node> eassertsProc;
- std::unordered_map<Node, Node, NodeHashFunction> cache;
+ std::unordered_map<Node, Node> cache;
for (const Node& e : easserts)
{
Node eae = d_pp->expandDefinitions(e, cache);
typedef NodeTemplate<true> Node;
typedef NodeTemplate<false> TNode;
class TypeNode;
-struct NodeHashFunction;
class Env;
class NodeManager;
}
Trace("check-synth-sol") << "Got solution map:\n";
// the set of synthesis conjectures in our assertions
- std::unordered_set<Node, NodeHashFunction> conjs;
+ std::unordered_set<Node> conjs;
// For each of the above conjectures, the functions-to-synthesis and their
// solutions. This is used as a substitution below.
std::map<Node, std::vector<Node>> fvarMap;
// auxiliary assertions
std::vector<Node> auxAssertions;
// expand definitions cache
- std::unordered_map<Node, Node, NodeHashFunction> cache;
+ std::unordered_map<Node, Node> cache;
for (Node assertion : *alist)
{
Notice() << "SygusSolver::checkSynthSolution(): checking assertion "
Node RemoveTermFormulas::getSkolemForNode(Node k) const
{
- context::CDInsertHashMap<Node, Node, NodeHashFunction>::const_iterator itk =
+ context::CDInsertHashMap<Node, Node>::const_iterator itk =
d_skolem_cache.find(k);
if (itk != d_skolem_cache.end())
{
typedef context::CDInsertHashMap<
std::pair<Node, uint32_t>,
Node,
- PairHashFunction<Node, uint32_t, NodeHashFunction> >
+ PairHashFunction<Node, uint32_t, std::hash<Node>>>
TermFormulaCache;
/** term formula removal cache
*
* 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;
+ context::CDInsertHashMap<Node, Node> d_skolem_cache;
/** gets the skolem for node
*
// trivial case
return tw;
}
- std::unordered_set<TNode, TNodeHashFunction>::iterator it;
+ std::unordered_set<TNode>::iterator it;
std::vector<TNode> visit;
TNode cur;
TNode curw;
return !tr.isConst() || !tr.getConst<bool>();
}
-const std::unordered_set<Node, NodeHashFunction>&
-WitnessFormGenerator::getWitnessFormEqs() const
+const std::unordered_set<Node>& WitnessFormGenerator::getWitnessFormEqs() const
{
return d_eqs;
}
* where k is a skolem, containing all rewrite steps used in calls to
* getProofFor during the entire lifetime of this generator.
*/
- const std::unordered_set<Node, NodeHashFunction>& getWitnessFormEqs() const;
+ const std::unordered_set<Node>& getWitnessFormEqs() const;
private:
/**
/** The term conversion proof generator */
TConvProofGenerator d_tcpg;
/** The nodes we have already added rewrite steps for in d_tcpg */
- std::unordered_set<TNode, TNodeHashFunction> d_visited;
+ std::unordered_set<TNode> d_visited;
/** The set of equalities added as proof steps */
- std::unordered_set<Node, NodeHashFunction> d_eqs;
+ std::unordered_set<Node> d_eqs;
/** Lazy proof storing witness intro steps */
LazyCDProof d_wintroPf;
/** CDProof for justifying purification existentials */
Node case_assoccomm(TNode n);
Node case_other(TNode n);
- typedef std::unordered_map<Node, Node, NodeHashFunction> NodeMap;
+ typedef std::unordered_map<Node, Node> NodeMap;
NodeMap d_cache;
};/* class RePairAssocCommutativeOperators */
SubstitutionMap* d_subs;
TheoryModel* d_model;
- typedef std::unordered_map<Node, Node, NodeHashFunction> NodeMap;
+ typedef std::unordered_map<Node, Node> NodeMap;
// cache for reduce vars
NodeMap d_reduceVar; // if reduceVars[n].isNull(), treat reduceVars[n] == n
NodeMap d_reduceGcd;
- typedef std::unordered_map<Node, Integer, NodeHashFunction> NodeIntegerMap;
+ typedef std::unordered_map<Node, Integer> NodeIntegerMap;
NodeIntegerMap d_gcds;
Integer d_one;
context::CDO<unsigned> d_subcount;
- typedef context::CDInsertHashMap<Node, Node, NodeHashFunction> CDNodeMap;
+ typedef context::CDInsertHashMap<Node, Node> CDNodeMap;
CDNodeMap d_skolems;
typedef std::map<Node, std::set<Node> > ImpMap;
bool ArithPreprocess::reduceAssertion(TNode atom)
{
- context::CDHashMap<Node, bool, NodeHashFunction>::const_iterator it =
- d_reduced.find(atom);
+ context::CDHashMap<Node, bool>::const_iterator it = d_reduced.find(atom);
if (it != d_reduced.end())
{
// already computed
bool ArithPreprocess::isReduced(TNode atom) const
{
- context::CDHashMap<Node, bool, NodeHashFunction>::const_iterator it =
- d_reduced.find(atom);
+ context::CDHashMap<Node, bool>::const_iterator it = d_reduced.find(atom);
if (it == d_reduced.end())
{
return false;
/** The operator elimination utility */
OperatorElim& d_opElim;
/** The set of assertions that were reduced */
- context::CDHashMap<Node, bool, NodeHashFunction> d_reduced;
+ context::CDHashMap<Node, bool> d_reduced;
};
} // namespace arith
/**
* Map from a node to it's minimum and maximum.
*/
- typedef context::CDHashMap<Node, DeltaRational, NodeHashFunction> CDNodeToMinMaxMap;
- CDNodeToMinMaxMap d_minMap;
- CDNodeToMinMaxMap d_maxMap;
+ typedef context::CDHashMap<Node, DeltaRational> CDNodeToMinMaxMap;
+ CDNodeToMinMaxMap d_minMap;
+ CDNodeToMinMaxMap d_maxMap;
public:
ArithStaticLearner(context::Context* userContext);
{
Assert(vars.size() == subs.size());
NodeManager* nm = NodeManager::currentNM();
- std::unordered_map<TNode, Node, TNodeHashFunction> visited;
- std::unordered_map<TNode, Node, TNodeHashFunction>::iterator it;
+ std::unordered_map<TNode, Node> visited;
+ std::unordered_map<TNode, Node>::iterator it;
std::vector<Node>::iterator itv;
std::vector<TNode> visit;
TNode cur;
namespace arith {
//Sets of Nodes
-typedef std::unordered_set<Node, NodeHashFunction> NodeSet;
-typedef std::unordered_set<TNode, TNodeHashFunction> TNodeSet;
-typedef context::CDHashSet<Node, NodeHashFunction> CDNodeSet;
+typedef std::unordered_set<Node> NodeSet;
+typedef std::unordered_set<TNode> TNodeSet;
+typedef context::CDHashSet<Node> CDNodeSet;
//Maps from Nodes -> ArithVars, and vice versa
-typedef std::unordered_map<Node, ArithVar, NodeHashFunction> NodeToArithVarMap;
+typedef std::unordered_map<Node, ArithVar> NodeToArithVarMap;
typedef DenseMap<Node> ArithVarToNodeMap;
inline Node mkRationalNode(const Rational& q){
* This is node is potentially both the propagation or
* Rewriter::rewrite(propagation).
*/
- typedef context::CDHashMap<Node, size_t, NodeHashFunction> ExplainMap;
+ typedef context::CDHashMap<Node, size_t> ExplainMap;
ExplainMap d_explanationMap;
ConstraintDatabase& d_constraintDatabase;
typedef context::CDList<ConstraintCP> CDConstraintList;
-typedef std::unordered_map<Node, ConstraintP, NodeHashFunction> NodetoConstraintMap;
+typedef std::unordered_map<Node, ConstraintP> NodetoConstraintMap;
typedef size_t ConstraintRuleID;
static const ConstraintRuleID ConstraintRuleIdSentinel = std::numeric_limits<ConstraintRuleID>::max();
}
Node DioSolver::columnGcdIsOne() const{
- std::unordered_map<Node, Integer, NodeHashFunction> gcdMap;
+ std::unordered_map<Node, Integer> gcdMap;
std::deque<TrailIndex>::const_iterator iter, end;
for(iter = d_currentF.begin(), end = d_currentF.end(); iter != end; ++iter){
* We maintain a map from the variables associated with proofs to an input constraint.
* These variables can then be used in polynomial manipulations.
*/
- typedef std::unordered_map<Node, InputConstraintIndex, NodeHashFunction> NodeToInputConstraintIndexMap;
+ typedef std::unordered_map<Node, InputConstraintIndex>
+ NodeToInputConstraintIndexMap;
NodeToInputConstraintIndexMap d_varToInputConstraintMap;
Node proofVariableToReason(const Variable& v) const{
*/
class InferenceManager : public InferenceManagerBuffered
{
- using NodeSet = context::CDHashSet<Node, NodeHashFunction>;
+ using NodeSet = context::CDHashSet<Node>;
public:
InferenceManager(TheoryArith& ta, ArithState& astate, ProofNodeManager* pnm);
// ( x*y, x*z, y ) for each pair of monomials ( x*y, x*z ) with common factors
std::map<Node, std::map<Node, Node> > d_mono_diff;
/** the set of monomials we should apply tangent planes to */
- std::unordered_set<Node, NodeHashFunction> d_tplane_refine;
+ std::unordered_set<Node> d_tplane_refine;
};
} // namespace nl
Trace("nl-ext-comp") << "Compute redundancies for " << lemmas.size()
<< " lemmas." << std::endl;
// naive
- std::unordered_set<Node, NodeHashFunction> r_lemmas;
+ std::unordered_set<Node> r_lemmas;
for (std::map<int, std::map<Node, std::map<Node, Node> > >::iterator itb =
cmp_infers.begin();
itb != cmp_infers.end();
void check();
private:
- using NodeSet = context::CDHashSet<Node, NodeHashFunction>;
+ using NodeSet = context::CDHashSet<Node>;
/** Basic data that is shared with other checks */
ExtState* d_data;
*/
class IAndSolver
{
- typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
+ typedef context::CDHashSet<Node> NodeSet;
public:
IAndSolver(InferenceManager& im, ArithState& state, NlModel& model);
std::vector<Node> ICPSolver::collectVariables(const Node& n) const
{
- std::unordered_set<TNode, TNodeHashFunction> tmp;
+ std::unordered_set<TNode> tmp;
expr::getVariables(n, tmp);
std::vector<Node> res;
for (const auto& t : tmp)
auto poly = std::get<0>(comp);
std::vector<Candidate> result;
- std::unordered_set<TNode, TNodeHashFunction> vars;
+ std::unordered_set<TNode> vars;
expr::getVariables(n, vars);
for (const auto& v : vars)
{
// all remaining variables are constrained to their exact model values
Trace("nl-ext-cm-debug") << " set exact bounds for remaining variables..."
<< std::endl;
- std::unordered_set<TNode, TNodeHashFunction> visited;
+ std::unordered_set<TNode> visited;
std::vector<TNode> visit;
TNode cur;
for (const Node& a : assertions)
NodeManager* nm = NodeManager::currentNM();
// the list of variables that occur as a monomial in msum, and whose value
// is so far unconstrained in the model.
- std::unordered_set<Node, NodeHashFunction> unc_vars;
+ std::unordered_set<Node> unc_vars;
// the list of variables that occur as a factor in a monomial, and whose
// value is so far unconstrained in the model.
- std::unordered_set<Node, NodeHashFunction> unc_vars_factor;
+ std::unordered_set<Node> unc_vars_factor;
for (std::pair<const Node, Node>& m : msum)
{
Node v = m.first;
Trace("nl-ext-cms-debug")
<< "* Try univariate quadratic analysis..." << std::endl;
std::vector<Node> vs_invalid;
- std::unordered_set<Node, NodeHashFunction> vs;
+ std::unordered_set<Node> vs;
std::map<Node, Node> v_a;
std::map<Node, Node> v_b;
// get coefficients...
* These literals are exempt from check-model, since they are satisfied by
* definition of our model construction.
*/
- std::unordered_map<Node, Node, NodeHashFunction> d_check_model_solved;
+ std::unordered_map<Node, Node> d_check_model_solved;
/** did we use an approximation on this call to last-call effort? */
bool d_used_approx;
}; /* class NlModel */
BoundInference bounds;
- std::unordered_set<Node, NodeHashFunction> init_assertions;
+ std::unordered_set<Node> init_assertions;
for (Theory::assertions_iterator it = d_containing.facts_begin();
it != d_containing.facts_end();
*/
class NonlinearExtension
{
- typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
+ typedef context::CDHashSet<Node> NodeSet;
public:
NonlinearExtension(TheoryArith& containing,
// compute the concavity
int region = -1;
- std::unordered_map<Node, int, NodeHashFunction>::iterator itr =
- d_tstate.d_tf_region.find(tf);
+ std::unordered_map<Node, int>::iterator itr = d_tstate.d_tf_region.find(tf);
if (itr != d_tstate.d_tf_region.end())
{
region = itr->second;
* arguments that contain transcendental functions.
*/
std::map<Node, Node> d_trMaster;
- std::map<Node, std::unordered_set<Node, NodeHashFunction>> d_trSlaves;
+ std::map<Node, std::unordered_set<Node>> d_trSlaves;
/** concavity region for transcendental functions
*
* of transcendental functions whose arguments have model
* values that reside in valid regions.
*/
- std::unordered_map<Node, int, NodeHashFunction> d_tf_region;
+ std::unordered_map<Node, int> d_tf_region;
/**
* Maps representives of a congruence class to the members of that class.
*
* each transcendental function application. We store this set for each
* Taylor degree.
*/
- std::unordered_map<Node,
- std::map<unsigned, std::vector<Node>>,
- NodeHashFunction>
+ std::unordered_map<Node, std::map<unsigned, std::vector<Node>>>
d_secant_points;
/** PI
// Delta lasts at least the duration of the function call
const Rational& delta = d_partialModel.getDelta();
- std::unordered_set<TNode, TNodeHashFunction> shared = d_containing.currentlySharedTerms();
+ std::unordered_set<TNode> shared = d_containing.currentlySharedTerms();
// TODO:
// This is not very good for user push/pop....
Node flattenImplication(Node imp){
NodeBuilder nb(kind::OR);
- std::unordered_set<Node, NodeHashFunction> included;
+ std::unordered_set<Node> included;
Node left = imp[0];
Node right = imp[1];
* A superset of all of the assertions that currently are not the literal for
* their constraint do not match constraint literals. Not just the witnesses.
*/
- context::CDInsertHashMap<Node, ConstraintP, NodeHashFunction> d_assertionsThatDoNotMatchTheirLiterals;
-
+ context::CDInsertHashMap<Node, ConstraintP>
+ d_assertionsThatDoNotMatchTheirLiterals;
/** Returns true if x is of type Integer. */
inline bool isInteger(ArithVar x) const {
/**
* Contains all nodes that have been preregistered
*/
- context::CDHashSet<Node, NodeHashFunction> d_preregisteredNodes;
-
+ context::CDHashSet<Node> d_preregisteredNodes;
/**
* Manages information about the assignment and upper and lower bounds on
}
};/* class Info */
-
-typedef std::unordered_map<Node, Info*, NodeHashFunction> CNodeInfoMap;
+typedef std::unordered_map<Node, Info*> CNodeInfoMap;
/**
* Class keeping track of the following information for canonical
}
void TheoryArrays::weakEquivAddSecondary(TNode index, TNode arrayFrom, TNode arrayTo, TNode reason) {
- std::unordered_set<TNode, TNodeHashFunction> marked;
+ std::unordered_set<TNode> marked;
vector<TNode> index_trail;
vector<TNode>::iterator it, iend;
Node equivalence_trail = reason;
std::vector<Node> arrays;
eq::EqClassesIterator eqcs_i = eq::EqClassesIterator(d_equalityEngine);
- for (; !eqcs_i.isFinished(); ++eqcs_i) {
+ for (; !eqcs_i.isFinished(); ++eqcs_i)
+ {
Node eqc = (*eqcs_i);
if (!eqc.getType().isArray())
{
continue;
}
eq::EqClassIterator eqc_i = eq::EqClassIterator(eqc, d_equalityEngine);
- for (; !eqc_i.isFinished(); ++eqc_i) {
+ for (; !eqc_i.isFinished(); ++eqc_i)
+ {
Node n = *eqc_i;
- // If this EC is an array type and it contains something other than STORE nodes, we have to compute a representative explicitly
+ // If this EC is an array type and it contains something other than STORE
+ // nodes, we have to compute a representative explicitly
if (termSet.find(n) != termSet.end())
{
if (n.getKind() != kind::STORE)
// Build a list of all the relevant reads, indexed by the store representative
std::map<Node, std::vector<Node> > selects;
set<Node>::iterator set_it = termSet.begin(), set_it_end = termSet.end();
- for (; set_it != set_it_end; ++set_it) {
+ for (; set_it != set_it_end; ++set_it)
+ {
Node n = *set_it;
- // If this term is a select, record that the EC rep of its store parameter is being read from using this term
- if (n.getKind() == kind::SELECT) {
+ // If this term is a select, record that the EC rep of its store parameter
+ // is being read from using this term
+ if (n.getKind() == kind::SELECT)
+ {
selects[d_equalityEngine->getRepresentative(n[0])].push_back(n);
}
}
TypeSet defaultValuesSet;
// Compute all default values already in use
- //if (fullModel) {
- for (size_t i=0; i<arrays.size(); ++i) {
- TNode nrep = d_equalityEngine->getRepresentative(arrays[i]);
- d_mayEqualEqualityEngine.addTerm(nrep); // add the term in case it isn't there already
- TNode mayRep = d_mayEqualEqualityEngine.getRepresentative(nrep);
- it = d_defValues.find(mayRep);
- if (it != d_defValues.end()) {
- defaultValuesSet.add(nrep.getType().getArrayConstituentType(), (*it).second);
- }
+ // if (fullModel) {
+ for (size_t i = 0; i < arrays.size(); ++i)
+ {
+ TNode nrep = d_equalityEngine->getRepresentative(arrays[i]);
+ d_mayEqualEqualityEngine.addTerm(
+ nrep); // add the term in case it isn't there already
+ TNode mayRep = d_mayEqualEqualityEngine.getRepresentative(nrep);
+ it = d_defValues.find(mayRep);
+ if (it != d_defValues.end())
+ {
+ defaultValuesSet.add(nrep.getType().getArrayConstituentType(),
+ (*it).second);
}
+ }
//}
- // Loop through all array equivalence classes that need a representative computed
- for (size_t i = 0; i < arrays.size(); ++i)
+ // Loop through all array equivalence classes that need a representative
+ // computed
+ for (size_t i = 0; i < arrays.size(); ++i)
+ {
+ TNode n = arrays[i];
+ TNode nrep = d_equalityEngine->getRepresentative(n);
+
+ // if (fullModel) {
+ // Compute default value for this array - there is one default value for
+ // every mayEqual equivalence class
+ TNode mayRep = d_mayEqualEqualityEngine.getRepresentative(nrep);
+ it = d_defValues.find(mayRep);
+ // If this mayEqual EC doesn't have a default value associated, get the next
+ // available default value for the associated array element type
+ if (it == d_defValues.end())
{
- TNode n = arrays[i];
- TNode nrep = d_equalityEngine->getRepresentative(n);
-
- // if (fullModel) {
- // Compute default value for this array - there is one default value for
- // every mayEqual equivalence class
- TNode mayRep = d_mayEqualEqualityEngine.getRepresentative(nrep);
- it = d_defValues.find(mayRep);
- // If this mayEqual EC doesn't have a default value associated, get the next available default value for the associated array element type
- if (it == d_defValues.end()) {
- TypeNode valueType = nrep.getType().getArrayConstituentType();
- rep = defaultValuesSet.nextTypeEnum(valueType);
- if (rep.isNull()) {
- Assert(defaultValuesSet.getSet(valueType)->begin()
- != defaultValuesSet.getSet(valueType)->end());
- rep = *(defaultValuesSet.getSet(valueType)->begin());
- }
- Trace("arrays-models") << "New default value = " << rep << endl;
- d_defValues[mayRep] = rep;
- }
- else {
- rep = (*it).second;
+ TypeNode valueType = nrep.getType().getArrayConstituentType();
+ rep = defaultValuesSet.nextTypeEnum(valueType);
+ if (rep.isNull())
+ {
+ Assert(defaultValuesSet.getSet(valueType)->begin()
+ != defaultValuesSet.getSet(valueType)->end());
+ rep = *(defaultValuesSet.getSet(valueType)->begin());
}
+ Trace("arrays-models") << "New default value = " << rep << endl;
+ d_defValues[mayRep] = rep;
+ }
+ else
+ {
+ rep = (*it).second;
+ }
- // Build the STORE_ALL term with the default value
- rep = nm->mkConst(ArrayStoreAll(nrep.getType(), rep));
- /*
+ // Build the STORE_ALL term with the default value
+ rep = nm->mkConst(ArrayStoreAll(nrep.getType(), rep));
+ /*
+ }
+ else {
+ std::unordered_map<Node, Node>::iterator it = d_skolemCache.find(n);
+ if (it == d_skolemCache.end()) {
+ rep = nm->mkSkolem("array_collect_model_var", n.getType(), "base model
+ variable for array collectModelInfo"); d_skolemCache[n] = rep;
}
else {
- std::unordered_map<Node, Node, NodeHashFunction>::iterator it = d_skolemCache.find(n);
- if (it == d_skolemCache.end()) {
- rep = nm->mkSkolem("array_collect_model_var", n.getType(), "base model variable for array collectModelInfo");
- d_skolemCache[n] = rep;
- }
- else {
- rep = (*it).second;
- }
+ rep = (*it).second;
}
+ }
*/
// For each read, require that the rep stores the right value
vector<Node>& reads = selects[nrep];
- for (unsigned j = 0; j < reads.size(); ++j) {
+ for (unsigned j = 0; j < reads.size(); ++j)
+ {
rep = nm->mkNode(kind::STORE, rep, reads[j][1], reads[j]);
}
if (!m->assertEquality(n, rep, true))
{
return false;
}
- if (!n.isConst()) {
+ if (!n.isConst())
+ {
m->assertSkeleton(rep);
}
}
// the call to SkolemCache::getExtIndexSkolem should be deterministic, but use
// cache anyways for now
Node skolem;
- std::unordered_map<Node, Node, NodeHashFunction>::iterator it = d_skolemCache.find(ref);
+ std::unordered_map<Node, Node>::iterator it = d_skolemCache.find(ref);
if (it == d_skolemCache.end()) {
Assert(ref.getKind() == kind::NOT && ref[0].getKind() == kind::EQUAL);
// make the skolem using the skolem cache utility
void explain(TNode literal, Node& exp);
/** For debugging only- checks invariants about when things are preregistered*/
- context::CDHashSet<Node, NodeHashFunction > d_isPreRegistered;
+ context::CDHashSet<Node> d_isPreRegistered;
/** Helper for preRegisterTerm, also used internally */
void preRegisterTermInternal(TNode n);
context::CDQueue<RowLemmaType> d_RowQueue;
context::CDHashSet<RowLemmaType, RowLemmaTypeHashFunction > d_RowAlreadyAdded;
- typedef context::CDHashSet<Node, NodeHashFunction> CDNodeSet;
+ typedef context::CDHashSet<Node> CDNodeSet;
CDNodeSet d_sharedArrays;
CDNodeSet d_sharedOther;
// When a new read term is created, we check the index to see if we know the model value. If so, we add it to d_constReads (and d_constReadsList)
// If not, we push it onto d_reads and figure out where it goes at computeCareGraph time.
// d_constReadsList is used as a backup in case we can't compute the model at computeCareGraph time.
- typedef std::unordered_map<Node, CTNodeList*, NodeHashFunction> CNodeNListMap;
+ typedef std::unordered_map<Node, CTNodeList*> CNodeNListMap;
CNodeNListMap d_constReads;
context::CDList<TNode> d_reads;
context::CDList<TNode> d_constReadsList;
};/* class ContextPopper */
ContextPopper d_contextPopper;
- std::unordered_map<Node, Node, NodeHashFunction> d_skolemCache;
+ std::unordered_map<Node, Node> d_skolemCache;
context::CDO<unsigned> d_skolemIndex;
std::vector<Node> d_skolemAssertions;
// List of nodes that need permanent references in this context
context::CDList<Node> d_permRef;
context::CDList<Node> d_modelConstraints;
- context::CDHashSet<Node, NodeHashFunction > d_lemmasSaved;
+ context::CDHashSet<Node> d_lemmasSaved;
std::vector<Node> d_lemmas;
// Default values for each mayEqual equivalence class
- typedef context::CDHashMap<Node,Node,NodeHashFunction> DefValMap;
+ typedef context::CDHashMap<Node, Node> DefValMap;
DefValMap d_defValues;
typedef std::unordered_map<std::pair<TNode, TNode>, CTNodeList*, TNodePairHashFunction> ReadBucketMap;
// Bad case: have to recompute value counts and/or possibly switch out
// default value
store = n;
- std::unordered_set<TNode, TNodeHashFunction> indexSet;
- std::unordered_map<TNode, uint32_t, TNodeHashFunction> elementsMap;
- std::unordered_map<TNode, uint32_t, TNodeHashFunction>::iterator it;
+ std::unordered_set<TNode> indexSet;
+ std::unordered_map<TNode, uint32_t> elementsMap;
+ std::unordered_map<TNode, uint32_t>::iterator it;
uint32_t count;
uint32_t max = 0;
TNode maxValue;
// The following declarations allow us to put functions in the .cpp file
// instead of the header, since we know which instantiations are needed.
-template void UnionFind<Node, NodeHashFunction>::notify();
+template void UnionFind<Node, std::hash<Node>>::notify();
-template void UnionFind<TNode, TNodeHashFunction>::notify();
+template void UnionFind<TNode, std::hash<TNode>>::notify();
} // namespace arrays
} // namespace theory
/** We index the requests in this vector, it's a list */
context::CDList<Element> d_requests;
- typedef context::CDHashMap<Node, element_index, NodeHashFunction> trigger_to_list_map;
+ typedef context::CDHashMap<Node, element_index> trigger_to_list_map;
/** Map from triggers, to the list of elements they trigger */
trigger_to_list_map d_triggerToRequestMap;
*/
class InferenceManager : public InferenceManagerBuffered
{
- typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
+ typedef context::CDHashSet<Node> NodeSet;
public:
InferenceManager(Theory& t, SolverState& s, ProofNodeManager* pnm);
size_t MakeBagOpHashFunction::operator()(const MakeBagOp& op) const
{
- return TypeNodeHashFunction()(op.getType());
+ return std::hash<TypeNode>()(op.getType());
}
MakeBagOp::MakeBagOp(const TypeNode& elementType)
*/
class TermRegistry
{
- typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeMap;
+ typedef context::CDHashMap<Node, Node> NodeMap;
public:
TermRegistry(SolverState& state, InferenceManager& im);
ASSIGNED_TO_FALSE,
};
- typedef std::unordered_map<Node, std::vector<Node>, NodeHashFunction>
- BackEdgesMap;
+ typedef std::unordered_map<Node, std::vector<Node>> BackEdgesMap;
/**
* Construct a new CircuitPropagator.
/**
* Assignment status of each node.
*/
- typedef context::CDHashMap<TNode, AssignmentStatus, TNodeHashFunction>
- AssignmentMap;
+ typedef context::CDHashMap<TNode, AssignmentStatus> AssignmentMap;
/**
* Assign Node in circuit with the value and add it to the queue; note
/** Nodes that have been attached already (computed forward edges for) */
// All the nodes we've visited so far
- context::CDHashSet<Node, NodeHashFunction> d_seen;
+ context::CDHashSet<Node> d_seen;
AssignmentMap d_state;
return Node::null();
}
// remove duplicates while keeping the order of children
- std::unordered_set<TNode, TNodeHashFunction> clauseSet;
+ std::unordered_set<TNode> clauseSet;
std::vector<Node> disjuncts;
unsigned size = children[0].getNumChildren();
for (unsigned i = 0; i < size; ++i)
{
Assert(children.size() == 1);
Assert(args.size() == 1);
- std::unordered_set<Node, NodeHashFunction> clauseSet1, clauseSet2;
+ std::unordered_set<Node> clauseSet1, clauseSet2;
if (children[0].getKind() == kind::OR)
{
clauseSet1.insert(children[0].begin(), children[0].end());
Node falseNode = nm->mkConst(false);
std::vector<Node> clauseNodes;
// literals to be removed from the virtual lhs clause of the resolution
- std::unordered_map<Node, unsigned, NodeHashFunction> lhsElim;
+ std::unordered_map<Node, unsigned> lhsElim;
for (std::size_t i = 0, argsSize = args.size(); i < argsSize; i = i + 2)
{
// whether pivot should occur as is or negated depends on the polarity of
for (std::size_t i = 0, childrenSize = children.size(); i < childrenSize;
++i)
{
- std::unordered_set<Node, NodeHashFunction> elim;
+ std::unordered_set<Node> elim;
// literals to be removed from "first" clause
if (i < childrenSize - 1)
{
}
Trace("bool-pfcheck") << "clause: " << clauseNodes << "\n";
// check that set representation is the same as of the given conclusion
- std::unordered_set<Node, NodeHashFunction> clauseComputed{
- clauseNodes.begin(), clauseNodes.end()};
+ std::unordered_set<Node> clauseComputed{clauseNodes.begin(),
+ clauseNodes.end()};
Trace("bool-pfcheck") << "clauseSet: " << clauseComputed << "\n" << pop;
if (clauseComputed.empty())
{
{
return Node::null();
}
- std::unordered_set<Node, NodeHashFunction> clauseGiven{args[0].begin(),
- args[0].end()};
+ std::unordered_set<Node> clauseGiven{args[0].begin(), args[0].end()};
return clauseComputed == clauseGiven ? args[0] : Node::null();
}
if (id == PfRule::SPLIT)
*/
RewriteResponse flattenNode(TNode n, TNode trivialNode, TNode skipNode)
{
- typedef std::unordered_set<TNode, TNodeHashFunction> node_set;
+ typedef std::unordered_set<TNode> node_set;
node_set visited;
visited.insert(skipNode);
return ret;
}
-Node TheoryBuiltinRewriter::getLambdaForArrayRepresentationRec( TNode a, TNode bvl, unsigned bvlIndex,
- std::unordered_map< TNode, Node, TNodeHashFunction >& visited ){
- std::unordered_map< TNode, Node, TNodeHashFunction >::iterator it = visited.find( a );
+Node TheoryBuiltinRewriter::getLambdaForArrayRepresentationRec(
+ TNode a,
+ TNode bvl,
+ unsigned bvlIndex,
+ std::unordered_map<TNode, Node>& visited)
+{
+ std::unordered_map<TNode, Node>::iterator it = visited.find(a);
if( it==visited.end() ){
Node ret;
if( bvlIndex<bvl.getNumChildren() ){
Node TheoryBuiltinRewriter::getLambdaForArrayRepresentation( TNode a, TNode bvl ){
Assert(a.getType().isArray());
- std::unordered_map< TNode, Node, TNodeHashFunction > visited;
+ std::unordered_map<TNode, Node> visited;
Trace("builtin-rewrite-debug") << "Get lambda for : " << a << ", with variables " << bvl << std::endl;
Node body = getLambdaForArrayRepresentationRec( a, bvl, 0, visited );
if( !body.isNull() ){
// conversions between lambdas and arrays
private:
/** recursive helper for getLambdaForArrayRepresentation */
- static Node getLambdaForArrayRepresentationRec( TNode a, TNode bvl, unsigned bvlIndex,
- std::unordered_map< TNode, Node, TNodeHashFunction >& visited );
+ static Node getLambdaForArrayRepresentationRec(
+ TNode a,
+ TNode bvl,
+ unsigned bvlIndex,
+ std::unordered_map<TNode, Node>& visited);
/** recursive helper for getArrayRepresentationForLambda */
static Node getArrayRepresentationForLambdaRec(TNode n, TypeNode retType);
typedef std::vector<TNode> ArgsVec;
class AbstractionModule {
- using NodeVecMap =
- std::unordered_map<Node, std::vector<Node>, NodeHashFunction>;
- using NodeTNodeMap = std::unordered_map<Node, TNode, NodeHashFunction>;
- using TNodeTNodeMap = std::unordered_map<TNode, TNode, TNodeHashFunction>;
- using NodeNodeMap = std::unordered_map<Node, Node, NodeHashFunction>;
- using TNodeNodeMap = std::unordered_map<Node, TNode, NodeHashFunction>;
- using TNodeSet = std::unordered_set<TNode, TNodeHashFunction>;
+ using NodeVecMap = std::unordered_map<Node, std::vector<Node>>;
+ using NodeTNodeMap = std::unordered_map<Node, TNode>;
+ using TNodeTNodeMap = std::unordered_map<TNode, TNode>;
+ using NodeNodeMap = std::unordered_map<Node, Node>;
+ using TNodeNodeMap = std::unordered_map<Node, TNode>;
+ using TNodeSet = std::unordered_set<TNode>;
using IntNodeMap = std::unordered_map<unsigned, Node>;
using IndexMap = std::unordered_map<unsigned, unsigned>;
using SkolemMap = std::unordered_map<unsigned, std::vector<Node> >;
- using SignatureMap = std::unordered_map<TNode, unsigned, TNodeHashFunction>;
+ using SignatureMap = std::unordered_map<TNode, unsigned>;
struct Statistics {
SizeStat<NodeNodeMap> d_numFunctionsAbstracted;
};
class ArgsTable {
- std::unordered_map<TNode, ArgsTableEntry, TNodeHashFunction > d_data;
+ std::unordered_map<TNode, ArgsTableEntry> d_data;
bool hasEntry(TNode signature) const;
public:
- typedef std::unordered_map<TNode, ArgsTableEntry, TNodeHashFunction >::iterator iterator;
- ArgsTable() {}
- void addEntry(TNode signature, const ArgsVec& args);
- ArgsTableEntry& getEntry(TNode signature);
- iterator begin() { return d_data.begin(); }
- iterator end() { return d_data.end(); }
+ typedef std::unordered_map<TNode, ArgsTableEntry>::iterator iterator;
+ ArgsTable() {}
+ void addEntry(TNode signature, const ArgsVec& args);
+ ArgsTableEntry& getEntry(TNode signature);
+ iterator begin() { return d_data.begin(); }
+ iterator end() { return d_data.end(); }
};
/**
static Abc_Ntk_t* currentAigNtk();
private:
- typedef std::unordered_map<TNode, Abc_Obj_t*, TNodeHashFunction> TNodeAigMap;
- typedef std::unordered_map<Node, Abc_Obj_t*, NodeHashFunction> NodeAigMap;
+ typedef std::unordered_map<TNode, Abc_Obj_t*> TNodeAigMap;
+ typedef std::unordered_map<Node, Abc_Obj_t*> NodeAigMap;
static thread_local Abc_Ntk_t* s_abcAigNetwork;
std::unique_ptr<context::Context> d_nullContext;
namespace theory {
namespace bv {
-typedef std::unordered_set<Node, NodeHashFunction> NodeSet;
-typedef std::unordered_set<TNode, TNodeHashFunction> TNodeSet;
+typedef std::unordered_set<Node> NodeSet;
+typedef std::unordered_set<TNode> TNodeSet;
/**
* The Bitblaster that manages the mapping between Nodes
{
protected:
typedef std::vector<T> Bits;
- typedef std::unordered_map<Node, Bits, NodeHashFunction> TermDefMap;
- typedef std::unordered_set<TNode, TNodeHashFunction> TNodeSet;
- typedef std::unordered_map<Node, Node, NodeHashFunction> ModelCache;
+ typedef std::unordered_map<Node, Bits> TermDefMap;
+ typedef std::unordered_set<TNode> TNodeSet;
+ typedef std::unordered_map<Node, Node> ModelCache;
typedef void (*TermBBStrategy)(TNode, Bits&, TBitblaster<T>*);
typedef T (*AtomBBStrategy)(TNode, TBitblaster<T>*);
private:
context::Context* d_context;
- typedef std::unordered_set<TNode, TNodeHashFunction> TNodeSet;
+ typedef std::unordered_set<TNode> TNodeSet;
std::unique_ptr<prop::SatSolver> d_satSolver;
std::unique_ptr<BitblastingRegistrar> d_bitblastingRegistrar;
{
std::vector<TNode> visit;
visit.push_back(node);
- std::unordered_set<TNode, TNodeHashFunction> visited;
+ std::unordered_set<TNode> visited;
bool fproofs =
options::proofGranularityMode() != options::ProofGranularityMode::OFF;
/** The associated term conversion proof generator. */
TConvProofGenerator* d_tcpg;
/** Map bit-vector nodes to bit-blasted nodes. */
- std::unordered_map<Node, Node, NodeHashFunction> d_bbMap;
+ std::unordered_map<Node, Node> d_bbMap;
};
} // namespace bv
/** Caches variables for which we already created bits. */
TNodeSet d_variables;
/** Stores bit-blasted atoms. */
- std::unordered_map<Node, Node, NodeHashFunction> d_bbAtoms;
+ std::unordered_map<Node, Node> d_bbAtoms;
/** Theory state. */
TheoryState* d_state;
};
bool collectModelInfo(theory::TheoryModel* m, bool fullModel);
private:
- context::CDHashSet<Node, NodeHashFunction> d_assertionSet;
- context::CDHashSet<Node, NodeHashFunction> d_assumptionSet;
+ context::CDHashSet<Node> d_assertionSet;
+ context::CDHashSet<Node> d_assumptionSet;
context::Context* d_context;
/** Bitblasters */
return (*(d_model->find(left))).second.value < (*(d_model->find(right))).second.value;
}
- };
+ };
- typedef std::unordered_map<TNode, ReasonId, TNodeHashFunction> ReasonToIdMap;
- typedef std::unordered_map<TNode, TermId, TNodeHashFunction> TermNodeToIdMap;
+ typedef std::unordered_map<TNode, ReasonId> ReasonToIdMap;
+ typedef std::unordered_map<TNode, TermId> TermNodeToIdMap;
typedef std::vector<InequalityEdge> Edges;
typedef std::unordered_set<TermId> TermIdSet;
- typedef std::priority_queue<TermId, std::vector<TermId>, QueueComparator> BFSQueue;
- typedef std::unordered_set<TNode, TNodeHashFunction> TNodeSet;
- typedef std::unordered_set<Node, NodeHashFunction> NodeSet;
+ typedef std::priority_queue<TermId, std::vector<TermId>, QueueComparator>
+ BFSQueue;
+ typedef std::unordered_set<TNode> TNodeSet;
+ typedef std::unordered_set<Node> NodeSet;
std::vector<InequalityNode> d_ineqNodes;
std::vector< Edges > d_ineqEdges;
/*** The currently asserted disequalities */
context::CDQueue<TNode> d_disequalities;
- typedef context::CDHashSet<Node, NodeHashFunction> CDNodeSet;
+ typedef context::CDHashSet<Node> CDNodeSet;
CDNodeSet d_disequalitiesAlreadySplit;
Node makeDiseqSplitLemma(TNode diseq);
/** Backtracking mechanisms **/
bool collectModelValues(theory::TheoryModel* model,
const std::set<Node>& termSet);
- typedef std::unordered_set<TNode, TNodeHashFunction>::const_iterator
- vars_iterator;
+ typedef std::unordered_set<TNode>::const_iterator vars_iterator;
vars_iterator beginVars();
vars_iterator endVars();
nb << cur.getOperator();
}
- std::unordered_map<Node, Node, NodeHashFunction>::iterator iit;
+ std::unordered_map<Node, Node>::iterator iit;
for (const TNode& child : cur)
{
iit = d_modelCache.find(child);
* Is cleared at the beginning of a getValue() call if the
* `d_invalidateModelCache` flag is set to true.
*/
- std::unordered_map<Node, Node, NodeHashFunction> d_modelCache;
+ std::unordered_map<Node, Node> d_modelCache;
/** Bit-blaster used to bit-blast atoms/terms. */
std::unique_ptr<BBSimple> d_bitblaster;
BVProofRuleChecker d_bvProofChecker;
/** Stores the SatLiteral for a given fact. */
- context::CDHashMap<Node, prop::SatLiteral, NodeHashFunction>
- d_factLiteralCache;
+ context::CDHashMap<Node, prop::SatLiteral> d_factLiteralCache;
/** Reverse map of `d_factLiteralCache`. */
context::CDHashMap<prop::SatLiteral, Node, prop::SatLiteralHashFunction>
context::Context* d_context;
/** Context dependent set of atoms we already propagated */
- context::CDHashSet<Node, NodeHashFunction> d_alreadyPropagatedSet;
- context::CDHashSet<Node, NodeHashFunction> d_sharedTermsSet;
+ context::CDHashSet<Node> d_alreadyPropagatedSet;
+ context::CDHashSet<Node> d_sharedTermsSet;
std::vector<std::unique_ptr<SubtheorySolver>> d_subtheories;
std::unordered_map<SubTheory, SubtheorySolver*, std::hash<int>>
void check(Theory::Effort e);
void spendResource(Resource r);
- typedef std::unordered_set<TNode, TNodeHashFunction> TNodeSet;
- typedef std::unordered_set<Node, NodeHashFunction> NodeSet;
+ typedef std::unordered_set<TNode> TNodeSet;
+ typedef std::unordered_set<Node> NodeSet;
NodeSet d_staticLearnCache;
- typedef std::unordered_map<Node, Node, NodeHashFunction> NodeToNode;
+ typedef std::unordered_map<Node, Node> NodeToNode;
context::CDO<bool> d_lemmasAdded;
* Keeps a map from nodes to the subtheory that propagated it so that we can
* explain it properly.
*/
- typedef context::CDHashMap<Node, SubTheory, NodeHashFunction> PropagatedMap;
+ typedef context::CDHashMap<Node, SubTheory> PropagatedMap;
PropagatedMap d_propagatedBy;
std::unique_ptr<EagerBitblastSolver> d_eagerSolver;
}
/* Traverse Boolean nodes and collect BV atoms. */
-void collectBVAtoms(TNode n, std::unordered_set<Node, NodeHashFunction>& atoms)
+void collectBVAtoms(TNode n, std::unordered_set<Node>& atoms)
{
std::vector<TNode> visit;
- std::unordered_set<TNode, TNodeHashFunction> visited;
+ std::unordered_set<TNode> visited;
visit.push_back(n);
d_im.trustedLemma(tlem, InferenceId::BV_SIMPLE_LEMMA);
}
- std::unordered_set<Node, NodeHashFunction> bv_atoms;
+ std::unordered_set<Node> bv_atoms;
collectBVAtoms(n, bv_atoms);
for (const Node& nn : bv_atoms)
{
void collectVariables(TNode node, utils::NodeSet& vars)
{
std::vector<TNode> stack;
- std::unordered_set<TNode, TNodeHashFunction> visited;
+ std::unordered_set<TNode> visited;
stack.push_back(node);
while (!stack.empty())
}
};
- typedef std::unordered_map<Node, SubstitutionElement, NodeHashFunction>
- Substitutions;
- typedef std::unordered_map<Node, SubstitutionElement, NodeHashFunction>
- SubstitutionsCache;
+ typedef std::unordered_map<Node, SubstitutionElement> Substitutions;
+ typedef std::unordered_map<Node, SubstitutionElement> SubstitutionsCache;
Substitutions d_substitutions;
SubstitutionsCache d_cache;
WorklistElement() : node(), id(-1) {}
};
-typedef std::unordered_map<Node, Node, NodeHashFunction> NodeNodeMap;
-typedef std::unordered_map<Node, unsigned, NodeHashFunction> NodeIdMap;
-typedef std::unordered_set<TNode, TNodeHashFunction> TNodeSet;
+typedef std::unordered_map<Node, Node> NodeNodeMap;
+typedef std::unordered_map<Node, unsigned> NodeIdMap;
+typedef std::unordered_set<TNode> TNodeSet;
class ExtractSkolemizer
{
ExtractList() : base(1), extracts() {}
void addExtract(Extract& e);
};
- typedef std::unordered_map<Node, ExtractList, NodeHashFunction> VarExtractMap;
+ typedef std::unordered_map<Node, ExtractList> VarExtractMap;
context::Context d_emptyContext;
VarExtractMap d_varToExtract;
theory::SubstitutionMap* d_modelMap;
context::CDQueue<TNode> d_bitblastQueue;
Statistics d_statistics;
- typedef std::unordered_map<Node, Node, NodeHashFunction> NodeMap;
+ typedef std::unordered_map<Node, Node> NodeMap;
NodeMap d_modelCache;
context::CDO<bool> d_validModelCache;
* Bitvector equality solver
*/
class CoreSolver : public SubtheorySolver {
- typedef std::unordered_map<TNode, Node, TNodeHashFunction> ModelValue;
- typedef std::unordered_map<TNode, bool, TNodeHashFunction> TNodeBoolMap;
- typedef std::unordered_set<TNode, TNodeHashFunction> TNodeSet;
-
+ typedef std::unordered_map<TNode, Node> ModelValue;
+ typedef std::unordered_map<TNode, bool> TNodeBoolMap;
+ typedef std::unordered_set<TNode> TNodeSet;
struct Statistics {
IntStat d_numCallstoCheck;
std::unique_ptr<ExtTheory> d_extTheory;
/** To make sure we keep the explanations */
- context::CDHashSet<Node, NodeHashFunction> d_reasons;
+ context::CDHashSet<Node> d_reasons;
ModelValue d_modelValues;
void buildModel();
bool assertFactToEqualityEngine(TNode fact, TNode reason);
/** Whether we need a last call effort check */
bool d_needsLastCallCheck;
/** For extended functions */
- context::CDHashSet<Node, NodeHashFunction> d_extf_range_infer;
- context::CDHashSet<Node, NodeHashFunction> d_extf_collapse_infer;
+ context::CDHashSet<Node> d_extf_range_infer;
+ context::CDHashSet<Node> d_extf_collapse_infer;
/** do extended function inferences
*
Statistics();
};
- context::CDHashSet<Node, NodeHashFunction> d_assertionSet;
+ context::CDHashSet<Node> d_assertionSet;
InequalityGraph d_inequalityGraph;
- context::CDHashMap<Node, TNode, NodeHashFunction> d_explanations;
+ context::CDHashMap<Node, TNode> d_explanations;
context::CDO<bool> d_isComplete;
- typedef std::unordered_set<Node, NodeHashFunction> NodeSet;
+ typedef std::unordered_set<Node> NodeSet;
NodeSet d_ineqTerms;
bool isInequalityOnly(TNode node);
bool addInequality(TNode a, TNode b, bool strict, TNode fact);
**/
class IntBlaster
{
- using CDNodeMap = context::CDHashMap<Node, Node, NodeHashFunction>;
+ using CDNodeMap = context::CDHashMap<Node, Node>;
public:
/**
* Range constraints of the form 0 <= x < 2^k
* These are added for every new integer variable that we introduce.
*/
- context::CDHashSet<Node, NodeHashFunction> d_rangeAssertions;
+ context::CDHashSet<Node> d_rangeAssertions;
/**
* A set of "bitwise" equalities over integers for BITVECTOR_AND
* used in for options::SolveBVAsIntMode::BITWISE
*/
- context::CDHashSet<Node, NodeHashFunction> d_bitwiseAssertions;
+ context::CDHashSet<Node> d_bitwiseAssertions;
/** Useful constants */
Node d_zero;
{}
};
-inline static void insert(std::unordered_map<TNode, Count, TNodeHashFunction>& map, TNode node, bool neg) {
+inline static void insert(std::unordered_map<TNode, Count>& map,
+ TNode node,
+ bool neg)
+{
if(map.find(node) == map.end()) {
Count c = neg? Count(0,1) : Count(1, 0);
map[node] = c;
NodeManager *nm = NodeManager::currentNM();
// this will remove duplicates
- std::unordered_map<TNode, Count, TNodeHashFunction> subterms;
+ std::unordered_map<TNode, Count> subterms;
unsigned size = utils::getSize(node);
BitVector constant = BitVector::mkOnes(size);
for (unsigned i = 0; i < node.getNumChildren(); ++i)
children.push_back(utils::mkConst(constant));
}
- std::unordered_map<TNode, Count, TNodeHashFunction>::const_iterator it =
- subterms.begin();
+ std::unordered_map<TNode, Count>::const_iterator it = subterms.begin();
for (; it != subterms.end(); ++it)
{
Debug("bv-rewrite") << "RewriteRule<FlattenAssocCommut>(" << node << ")" << std::endl;
std::vector<Node> processingStack;
processingStack.push_back(node);
- std::unordered_set<TNode, TNodeHashFunction> processed;
+ std::unordered_set<TNode> processed;
std::vector<Node> children;
Kind kind = node.getKind();
NodeManager *nm = NodeManager::currentNM();
// this will remove duplicates
- std::unordered_map<TNode, Count, TNodeHashFunction> subterms;
+ std::unordered_map<TNode, Count> subterms;
unsigned size = utils::getSize(node);
BitVector constant(size, (unsigned)0);
children.push_back(utils::mkConst(constant));
}
- std::unordered_map<TNode, Count, TNodeHashFunction>::const_iterator it =
- subterms.begin();
+ std::unordered_map<TNode, Count>::const_iterator it = subterms.begin();
for (; it != subterms.end(); ++it)
{
<< std::endl;
NodeManager *nm = NodeManager::currentNM();
- std::unordered_map<TNode, Count, TNodeHashFunction> subterms;
+ std::unordered_map<TNode, Count> subterms;
unsigned size = utils::getSize(node);
BitVector constant;
bool const_set = false;
std::vector<Node> children;
- std::unordered_map<TNode, Count, TNodeHashFunction>::const_iterator it =
- subterms.begin();
+ std::unordered_map<TNode, Count>::const_iterator it = subterms.begin();
unsigned true_count = 0;
bool seen_false = false;
for (; it != subterms.end(); ++it)
TNode t = term.getKind() == kind::NOT ? term[0] : term;
std::vector<TNode> stack;
- std::unordered_map<TNode, bool, TNodeHashFunction> visited;
+ std::unordered_map<TNode, bool> visited;
stack.push_back(t);
while (!stack.empty())
namespace theory {
namespace bv {
-typedef std::unordered_set<Node, NodeHashFunction> NodeSet;
-typedef std::unordered_set<TNode, TNodeHashFunction> TNodeSet;
+typedef std::unordered_set<Node> NodeSet;
+typedef std::unordered_set<TNode> TNodeSet;
namespace utils {
-typedef std::unordered_map<TNode, bool, TNodeHashFunction> TNodeBoolMap;
-typedef std::unordered_set<Node, NodeHashFunction> NodeSet;
+typedef std::unordered_map<TNode, bool> TNodeBoolMap;
+typedef std::unordered_set<Node> NodeSet;
/* Get the bit-width of given node. */
unsigned getSize(TNode node);
*/
class InferProofCons : public ProofGenerator
{
- typedef context::
- CDHashMap<Node, std::shared_ptr<DatatypesInference>, NodeHashFunction>
- NodeDatatypesInferenceMap;
+ typedef context::CDHashMap<Node, std::shared_ptr<DatatypesInference>>
+ NodeDatatypesInferenceMap;
public:
InferProofCons(context::Context* c, ProofNodeManager* pnm);
TNode val;
if (!op.hasAttribute(SygusVarFreeAttribute()))
{
- std::unordered_set<Node, NodeHashFunction> fvs;
+ std::unordered_set<Node> fvs;
if (expr::getFreeVariables(op, fvs))
{
if (fvs.size() == 1)
Node sygusToBuiltin(Node n, bool isExternal)
{
- std::unordered_map<TNode, Node, TNodeHashFunction> visited;
- std::unordered_map<TNode, Node, TNodeHashFunction>::iterator it;
+ std::unordered_map<TNode, Node> visited;
+ std::unordered_map<TNode, Node>::iterator it;
std::vector<TNode> visit;
TNode cur;
unsigned index;
std::vector<Node> eargs;
bool svarsInit = false;
std::vector<Node> svars;
- std::unordered_map<TNode, Node, TNodeHashFunction> visited;
- std::unordered_map<TNode, Node, TNodeHashFunction>::iterator it;
+ std::unordered_map<TNode, Node> visited;
+ std::unordered_map<TNode, Node>::iterator it;
std::vector<TNode> visit;
TNode cur;
unsigned index;
return Node::null();
}
-void getFreeSymbolsSygusType(TypeNode sdt,
- std::unordered_set<Node, NodeHashFunction>& syms)
+void getFreeSymbolsSygusType(TypeNode sdt, std::unordered_set<Node>& syms)
{
// datatype types we need to process
std::vector<TypeNode> typeToProcess;
* We have that { a, b, c, e } are added to syms. Notice that expr::getSymbols
* excludes variables whose kind is BOUND_VARIABLE.
*/
-void getFreeSymbolsSygusType(TypeNode sdt,
- std::unordered_set<Node, NodeHashFunction>& syms);
+void getFreeSymbolsSygusType(TypeNode sdt, std::unordered_set<Node>& syms);
/** Substitute and generalize a sygus datatype type
*
bool success = false;
if( n.getKind()==kind::APPLY_SELECTOR_TOTAL ){
registerTerm(n[0]);
- std::unordered_map<Node, Node, NodeHashFunction>::iterator it =
- d_term_to_anchor.find(n[0]);
+ std::unordered_map<Node, Node>::iterator it = d_term_to_anchor.find(n[0]);
if( it!=d_term_to_anchor.end() ) {
d_term_to_anchor[n] = it->second;
unsigned sel_weight =
}
// add the above symmetry breaking predicates to lemmas
- std::unordered_map<TNode, TNode, TNodeHashFunction> cache;
+ std::unordered_map<TNode, TNode> cache;
Node rlv = getRelevancyCondition(n);
for (std::pair<Node, InferenceId>& sbl : sbLemmas)
{
{
NodeManager* nm = NodeManager::currentNM();
SkolemManager* sm = nm->getSkolemManager();
- std::unordered_map<TNode, Node, TNodeHashFunction> visited;
- std::unordered_map<TNode, Node, TNodeHashFunction>::iterator it;
+ std::unordered_map<TNode, Node> visited;
+ std::unordered_map<TNode, Node>::iterator it;
std::map<Node, Node>::iterator ittb;
std::vector<TNode> visit;
TNode cur;
bool topLevel)
{
//register this term
- std::unordered_map<Node, Node, NodeHashFunction>::iterator ita =
- d_term_to_anchor.find(n);
+ std::unordered_map<Node, Node>::iterator ita = d_term_to_anchor.find(n);
Assert(ita != d_term_to_anchor.end());
Node a = ita->second;
Assert(!a.isNull());
registerSymBreakLemmaForValue(a, nv, dbzet, Node::null(), var_count);
return Node::null();
}else{
- std::unordered_map<Node, Node, NodeHashFunction>& scasv =
- sca.d_search_val[tn];
- std::unordered_map<Node, unsigned, NodeHashFunction>& scasvs =
- sca.d_search_val_sz[tn];
- std::unordered_map<Node, Node, NodeHashFunction>::iterator itsv =
- scasv.find(bvr);
+ std::unordered_map<Node, Node>& scasv = sca.d_search_val[tn];
+ std::unordered_map<Node, unsigned>& scasvs = sca.d_search_val_sz[tn];
+ std::unordered_map<Node, Node>::iterator itsv = scasv.find(bvr);
Node bad_val_bvr;
bool by_examples = false;
if (itsv == scasv.end())
Trace("sygus-sb-debug2")
<< "add lemmas up to size " << max_sz << ", which is (search_size) "
<< csz << " - (depth) " << d << std::endl;
- std::unordered_map<TNode, TNode, TNodeHashFunction> cache;
+ std::unordered_map<TNode, TNode> cache;
for (std::pair<const uint64_t, std::vector<Node>>& sbls : its->second)
{
if (sbls.first <= max_sz)
unsigned SygusExtension::getSearchSizeFor( Node n ) {
Trace("sygus-sb-debug2") << "get search size for term : " << n << std::endl;
- std::unordered_map<Node, Node, NodeHashFunction>::iterator ita =
- d_term_to_anchor.find(n);
+ std::unordered_map<Node, Node>::iterator ita = d_term_to_anchor.find(n);
Assert(ita != d_term_to_anchor.end());
return getSearchSizeForAnchor( ita->second );
}
&& !s.second.empty()))
{
Node rlv = getRelevancyCondition(t);
- std::unordered_map<TNode, TNode, TNodeHashFunction> cache;
+ std::unordered_map<TNode, TNode> cache;
for (const Node& lem : s.second)
{
Node slem = lem.substitute(x, t, cache);
*/
class SygusExtension
{
- typedef context::CDHashMap< Node, int, NodeHashFunction > IntMap;
- typedef context::CDHashMap< Node, Node, NodeHashFunction > NodeMap;
- typedef context::CDHashMap< Node, bool, NodeHashFunction > BoolMap;
- typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
+ typedef context::CDHashMap<Node, int> IntMap;
+ typedef context::CDHashMap<Node, Node> NodeMap;
+ typedef context::CDHashMap<Node, bool> BoolMap;
+ typedef context::CDHashSet<Node> NodeSet;
public:
SygusExtension(TheoryState& s,
* Map from terms (selector chains) to their anchors. The anchor of a
* selector chain S1( ... Sn( x ) ... ) is x.
*/
- std::unordered_map<Node, Node, NodeHashFunction> d_term_to_anchor;
+ std::unordered_map<Node, Node> d_term_to_anchor;
/**
* Map from anchors to the conjecture they are associated with.
*/
* where weight is the selector weight of Si
* (see SygusTermDatabase::getSelectorWeight).
*/
- std::unordered_map<Node, unsigned, NodeHashFunction> d_term_to_depth;
+ std::unordered_map<Node, unsigned> d_term_to_depth;
/**
* Map from terms (selector chains) to whether they are the topmost term
* of their type. For example, if:
* Then, x, S1( x ), and S4( S3( S2( S1( x ) ) ) ) are top-level terms,
* whereas S2( S1( x ) ) and S3( S2( S1( x ) ) ) are not.
*/
- std::unordered_map<Node, bool, NodeHashFunction> d_is_top_level;
+ std::unordered_map<Node, bool> d_is_top_level;
/**
* Returns true if the selector chain n is top-level based on the above
* definition, when tn is the type of n.
* term. The range of this map can be updated if we later encounter a sygus
* term that also rewrites to the builtin value but has a smaller term size.
*/
- std::map<TypeNode, std::unordered_map<Node, Node, NodeHashFunction>>
- d_search_val;
+ std::map<TypeNode, std::unordered_map<Node, Node>> d_search_val;
/** the size of terms in the range of d_search val. */
- std::map<TypeNode, std::unordered_map<Node, unsigned, NodeHashFunction>>
- d_search_val_sz;
+ std::map<TypeNode, std::unordered_map<Node, unsigned>> d_search_val_sz;
/** For each term, whether this cache has processed that term */
- std::unordered_set<Node, NodeHashFunction> d_search_val_proc;
+ std::unordered_set<Node> d_search_val_proc;
};
/** An instance of the above cache, for each anchor */
std::map< Node, SearchCache > d_cache;
* This should be user context-dependent if sygus is updated to work in
* incremental mode.
*/
- std::unordered_map<Node, unsigned, NodeHashFunction> d_simple_proc;
+ std::unordered_map<Node, unsigned> d_simple_proc;
//------------------------end static symmetry breaking
/** Get the canonical free variable for type tn */
private:
typedef context::CDList<Node> NodeList;
/** maps nodes to an index in a vector */
- typedef context::CDHashMap<Node, size_t, NodeHashFunction> NodeUIntMap;
- typedef context::CDHashMap<Node, bool, NodeHashFunction> BoolMap;
- typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeMap;
+ typedef context::CDHashMap<Node, size_t> NodeUIntMap;
+ typedef context::CDHashMap<Node, bool> BoolMap;
+ typedef context::CDHashMap<Node, Node> NodeMap;
private:
//notification class for equality engine
if (check)
{
Kind nck = nc.getKind();
- std::unordered_set<Node, NodeHashFunction> bvs;
+ std::unordered_set<Node> bvs;
if (nck == kind::MATCH_BIND_CASE)
{
for (const Node& v : nc[0])
*/
class EagerProofGenerator : public ProofGenerator
{
- typedef context::CDHashMap<Node, std::shared_ptr<ProofNode>, NodeHashFunction>
- NodeProofNodeMap;
+ typedef context::CDHashMap<Node, std::shared_ptr<ProofNode>> NodeProofNodeMap;
public:
EagerProofGenerator(ProofNodeManager* pnm,
const std::vector<Node>& vals,
bool useRewriter) const
{
- std::unordered_map<Node, Node, NodeHashFunction> visited;
+ std::unordered_map<Node, Node> visited;
return eval(n, args, vals, visited, useRewriter);
}
-Node Evaluator::eval(
- TNode n,
- const std::vector<Node>& args,
- const std::vector<Node>& vals,
- const std::unordered_map<Node, Node, NodeHashFunction>& visited,
- bool useRewriter) const
+Node Evaluator::eval(TNode n,
+ const std::vector<Node>& args,
+ const std::vector<Node>& vals,
+ const std::unordered_map<Node, Node>& visited,
+ bool useRewriter) const
{
Trace("evaluator") << "Evaluating " << n << " under substitution " << args
<< " " << vals << " with visited size = " << visited.size()
<< std::endl;
- std::unordered_map<TNode, Node, NodeHashFunction> evalAsNode;
- std::unordered_map<TNode, EvalResult, TNodeHashFunction> results;
+ std::unordered_map<TNode, Node> evalAsNode;
+ std::unordered_map<TNode, EvalResult> results;
// add visited to results
for (const std::pair<const Node, Node>& p : visited)
{
if (results[p.first].d_tag == EvalResult::INVALID)
{
// could not evaluate, use the evalAsNode map
- std::unordered_map<TNode, Node, NodeHashFunction>::iterator itn =
- evalAsNode.find(p.second);
+ std::unordered_map<TNode, Node>::iterator itn = evalAsNode.find(p.second);
Assert(itn != evalAsNode.end());
Node val = itn->second;
if (useRewriter)
if (ret.isNull() && useRewriter)
{
// should be stored in the evaluation-as-node map
- std::unordered_map<TNode, Node, NodeHashFunction>::iterator itn =
- evalAsNode.find(n);
+ std::unordered_map<TNode, Node>::iterator itn = evalAsNode.find(n);
Assert(itn != evalAsNode.end());
ret = Rewriter::rewrite(itn->second);
}
TNode n,
const std::vector<Node>& args,
const std::vector<Node>& vals,
- std::unordered_map<TNode, Node, NodeHashFunction>& evalAsNode,
- std::unordered_map<TNode, EvalResult, TNodeHashFunction>& results,
+ std::unordered_map<TNode, Node>& evalAsNode,
+ std::unordered_map<TNode, EvalResult>& results,
bool useRewriter) const
{
std::vector<TNode> queue;
queue.emplace_back(n);
- std::unordered_map<TNode, EvalResult, TNodeHashFunction>::iterator itr;
+ std::unordered_map<TNode, EvalResult>::iterator itr;
while (queue.size() != 0)
{
// since the evaluation of op[1] is under a new substitution and thus
// should not be cached. We could alternatively copy evalAsNode to
// evalAsNodeC but favor avoiding this copy for performance reasons.
- std::unordered_map<TNode, Node, NodeHashFunction> evalAsNodeC;
- std::unordered_map<TNode, EvalResult, TNodeHashFunction> resultsC;
+ std::unordered_map<TNode, Node> evalAsNodeC;
+ std::unordered_map<TNode, EvalResult> resultsC;
results[currNode] = evalInternal(op[1],
lambdaArgs,
lambdaVals,
return results[n];
}
-Node Evaluator::reconstruct(
- TNode n,
- std::unordered_map<TNode, EvalResult, TNodeHashFunction>& eresults,
- std::unordered_map<TNode, Node, NodeHashFunction>& evalAsNode) const
+Node Evaluator::reconstruct(TNode n,
+ std::unordered_map<TNode, EvalResult>& eresults,
+ std::unordered_map<TNode, Node>& evalAsNode) const
{
if (n.getNumChildren() == 0)
{
}
Trace("evaluator") << "Evaluator: reconstruct " << n << std::endl;
NodeManager* nm = NodeManager::currentNM();
- std::unordered_map<TNode, EvalResult, TNodeHashFunction>::iterator itr;
- std::unordered_map<TNode, Node, NodeHashFunction>::iterator itn;
+ std::unordered_map<TNode, EvalResult>::iterator itr;
+ std::unordered_map<TNode, Node>::iterator itn;
std::vector<Node> echildren;
if (n.getMetaKind() == kind::metakind::PARAMETERIZED)
{
Node eval(TNode n,
const std::vector<Node>& args,
const std::vector<Node>& vals,
- const std::unordered_map<Node, Node, NodeHashFunction>& visited,
+ const std::unordered_map<Node, Node>& visited,
bool useRewriter = true) const;
private:
* `args` to `vals` and rewriting. Notice that this map contains an entry
* for n in the case that it cannot be evaluated.
*/
- EvalResult evalInternal(
- TNode n,
- const std::vector<Node>& args,
- const std::vector<Node>& vals,
- std::unordered_map<TNode, Node, NodeHashFunction>& evalAsNode,
- std::unordered_map<TNode, EvalResult, TNodeHashFunction>& results,
- bool useRewriter) const;
+ EvalResult evalInternal(TNode n,
+ const std::vector<Node>& args,
+ const std::vector<Node>& vals,
+ std::unordered_map<TNode, Node>& evalAsNode,
+ std::unordered_map<TNode, EvalResult>& results,
+ bool useRewriter) const;
/** reconstruct
*
* This function reconstructs the result of evaluating n using a combination
* above method for some args and vals. This method ensures that the return
* value is equivalent to the rewritten form of n * { args -> vals }.
*/
- Node reconstruct(
- TNode n,
- std::unordered_map<TNode, EvalResult, TNodeHashFunction>& eresults,
- std::unordered_map<TNode, Node, NodeHashFunction>& evalAsNode) const;
+ Node reconstruct(TNode n,
+ std::unordered_map<TNode, EvalResult>& eresults,
+ std::unordered_map<TNode, Node>& evalAsNode) const;
};
} // namespace theory
*/
class ExtTheory
{
- using NodeBoolMap = context::CDHashMap<Node, bool, NodeHashFunction>;
- using NodeExtReducedIdMap =
- context::CDHashMap<Node, ExtReducedId, NodeHashFunction>;
- using NodeSet = context::CDHashSet<Node, NodeHashFunction>;
+ using NodeBoolMap = context::CDHashMap<Node, bool>;
+ using NodeExtReducedIdMap = context::CDHashMap<Node, ExtReducedId>;
+ using NodeSet = context::CDHashSet<Node>;
public:
/** constructor
typedef symfpuSymbolic::traits::ubv ubv;
typedef symfpuSymbolic::traits::sbv sbv;
- typedef context::CDHashMap<Node, uf, NodeHashFunction> fpMap;
- typedef context::CDHashMap<Node, rm, NodeHashFunction> rmMap;
- typedef context::CDHashMap<Node, prop, NodeHashFunction> boolMap;
- typedef context::CDHashMap<Node, ubv, NodeHashFunction> ubvMap;
- typedef context::CDHashMap<Node, sbv, NodeHashFunction> sbvMap;
+ typedef context::CDHashMap<Node, uf> fpMap;
+ typedef context::CDHashMap<Node, rm> rmMap;
+ typedef context::CDHashMap<Node, prop> boolMap;
+ typedef context::CDHashMap<Node, ubv> ubvMap;
+ typedef context::CDHashMap<Node, sbv> sbvMap;
fpMap d_fpMap;
rmMap d_rmMap;
{
using PairTypeNodeHashFunction = PairHashFunction<TypeNode,
TypeNode,
- TypeNodeHashFunction,
- TypeNodeHashFunction>;
+ std::hash<TypeNode>,
+ std::hash<TypeNode>>;
/** Uninterpreted functions for undefined cases of non-total operators. */
- using ComparisonUFMap =
- context::CDHashMap<TypeNode, Node, TypeNodeHashFunction>;
+ using ComparisonUFMap = context::CDHashMap<TypeNode, Node>;
/** Uninterpreted functions for lazy handling of conversions. */
using ConversionUFMap = context::
CDHashMap<std::pair<TypeNode, TypeNode>, Node, PairTypeNodeHashFunction>;
}
}
- std::unordered_set<TNode, TNodeHashFunction> visited;
+ std::unordered_set<TNode> visited;
std::stack<TNode> working;
std::set<TNode> relevantVariables;
for (std::set<Node>::const_iterator i(relevantTerms.begin());
TrustNode explain(TNode n) override;
protected:
- using ConversionAbstractionMap =
- context::CDHashMap<TypeNode, Node, TypeNodeHashFunction>;
- using AbstractionMap = context::CDHashMap<Node, Node, NodeHashFunction>;
+ using ConversionAbstractionMap = context::CDHashMap<TypeNode, Node>;
+ using AbstractionMap = context::CDHashMap<Node, Node>;
/** Equality engine. */
class NotifyClass : public eq::EqualityEngineNotify {
void registerTerm(TNode node);
bool isRegistered(TNode node);
- context::CDHashSet<Node, NodeHashFunction> d_registeredTerms;
+ context::CDHashSet<Node> d_registeredTerms;
/** The word-blaster. Translates FP -> BV. */
std::unique_ptr<FpConverter> d_conv;
|| k == BITVECTOR_SHL;
}
-Node BvInverter::getPathToPv(
- Node lit,
- Node pv,
- Node sv,
- std::vector<unsigned>& path,
- std::unordered_set<TNode, TNodeHashFunction>& visited)
+Node BvInverter::getPathToPv(Node lit,
+ Node pv,
+ Node sv,
+ std::vector<unsigned>& path,
+ std::unordered_set<TNode>& visited)
{
if (visited.find(lit) == visited.end())
{
std::vector<unsigned>& path,
bool projectNl)
{
- std::unordered_set<TNode, TNodeHashFunction> visited;
+ std::unordered_set<TNode> visited;
Node slit = getPathToPv(lit, pv, sv, path, visited);
// if we are able to find a (invertible) path to pv
if (!slit.isNull() && !pvs.isNull())
Node pv,
Node sv,
std::vector<unsigned>& path,
- std::unordered_set<TNode, TNodeHashFunction>& visited);
+ std::unordered_set<TNode>& visited);
/** Helper function for getInv.
*
bool& rew_print)
{
// have we added this term before?
- std::unordered_map<Node, Node, NodeHashFunction>::iterator itac =
- d_add_term_cache.find(sol);
+ std::unordered_map<Node, Node>::iterator itac = d_add_term_cache.find(sol);
if (itac != d_add_term_cache.end())
{
return itac->second;
/** candidate rewrite filter */
CandidateRewriteFilter d_crewrite_filter;
/** the cache for results of addTerm */
- std::unordered_map<Node, Node, NodeHashFunction> d_add_term_cache;
+ std::unordered_map<Node, Node> d_add_term_cache;
};
} // namespace quantifiers
Assert(!s.isNull());
n = d_drewrite->toExternal(n);
Assert(!n.isNull());
- std::map<Node, std::unordered_set<Node, NodeHashFunction> >::iterator it =
- d_pairs.find(n);
+ std::map<Node, std::unordered_set<Node> >::iterator it = d_pairs.find(n);
if (Trace.isOn("crf-match"))
{
Trace("crf-match") << " " << s << " matches " << n
* Stores all relevant pairs returned by this sampler (see registerTerm). In
* detail, if (t,s) is a relevant pair, then t in d_pairs[s].
*/
- std::map<Node, std::unordered_set<Node, NodeHashFunction> > d_pairs;
+ std::map<Node, std::unordered_set<Node> > d_pairs;
/**
* For each (builtin) type, a match trie storing all terms in the domain of
* d_pairs.
Node pv,
CegInstEffort effort)
{
- std::unordered_map<Node, std::vector<unsigned>, NodeHashFunction>::iterator
- iti = d_var_to_inst_id.find(pv);
+ std::unordered_map<Node, std::vector<unsigned>>::iterator iti =
+ d_var_to_inst_id.find(pv);
if (iti == d_var_to_inst_id.end())
{
// no bounds
// get the slack value introduced for the asserted literal
Node curr_slack_val;
- std::unordered_map<Node, Node, NodeHashFunction>::iterator itms =
+ std::unordered_map<Node, Node>::iterator itms =
d_alit_to_model_slack.find(alit);
if (itms != d_alit_to_model_slack.end())
{
Node lit)
{
// result of rewriting the visited term
- std::stack<std::unordered_map<TNode, Node, TNodeHashFunction> > visited;
- visited.push(std::unordered_map<TNode, Node, TNodeHashFunction>());
+ std::stack<std::unordered_map<TNode, Node>> visited;
+ visited.push(std::unordered_map<TNode, Node>());
// whether the visited term contains pv
- std::unordered_map<Node, bool, NodeHashFunction> visited_contains_pv;
- std::unordered_map<TNode, Node, TNodeHashFunction>::iterator it;
- std::unordered_map<TNode, Node, TNodeHashFunction> curr_subs;
+ std::unordered_map<Node, bool> visited_contains_pv;
+ std::unordered_map<TNode, Node>::iterator it;
+ std::unordered_map<TNode, Node> curr_subs;
std::stack<std::stack<TNode> > visit;
TNode cur;
visit.push(std::stack<TNode>());
if (it == visited.top().end())
{
- std::unordered_map<TNode, Node, TNodeHashFunction>::iterator itc =
- curr_subs.find(cur);
+ std::unordered_map<TNode, Node>::iterator itc = curr_subs.find(cur);
if (itc != curr_subs.end())
{
visited.top()[cur] = itc->second;
// of this witness expression since we are
// now in the context { cur[0][0] -> bv },
// hence we push a context here
- visited.push(std::unordered_map<TNode, Node, TNodeHashFunction>());
+ visited.push(std::unordered_map<TNode, Node>());
visit.push(std::stack<TNode>());
}
visited.top()[cur] = Node::null();
if (Trace.isOn("cegqi-bv-nl"))
{
std::vector<TNode> trace_visit;
- std::unordered_set<TNode, TNodeHashFunction> trace_visited;
+ std::unordered_set<TNode> trace_visited;
trace_visit.push_back(result);
do
Node pv,
Node n,
std::vector<Node>& children,
- std::unordered_map<Node, bool, NodeHashFunction>& contains_pv)
+ std::unordered_map<Node, bool>& contains_pv)
{
NodeManager* nm = NodeManager::currentNM();
Trace("cegqi-bv-pp") << "-----remove extracts..." << std::endl;
// map from terms to bitvector extracts applied to that term
std::map<Node, std::vector<Node> > extract_map;
- std::unordered_set<TNode, TNodeHashFunction> visited;
+ std::unordered_set<TNode> visited;
Trace("cegqi-bv-pp-debug2") << "Register ce lemma " << lem << std::endl;
collectExtracts(lem, extract_map, visited);
for (std::pair<const Node, std::vector<Node> >& es : extract_map)
void BvInstantiatorPreprocess::collectExtracts(
Node lem,
- std::map<Node, std::vector<Node> >& extract_map,
- std::unordered_set<TNode, TNodeHashFunction>& visited)
+ std::map<Node, std::vector<Node>>& extract_map,
+ std::unordered_set<TNode>& visited)
{
std::vector<TNode> visit;
TNode cur;
/** identifier counter, used to allocate ids to each solve form */
unsigned d_inst_id_counter;
/** map from variables to list of solved form ids */
- std::unordered_map<Node, std::vector<unsigned>, NodeHashFunction>
- d_var_to_inst_id;
+ std::unordered_map<Node, std::vector<unsigned>> d_var_to_inst_id;
/** for each solved form id, the term for instantiation */
std::unordered_map<unsigned, Node> d_inst_id_to_term;
/** for each solved form id, the corresponding asserted literal */
std::unordered_map<unsigned, Node> d_inst_id_to_alit;
/** map from variable to current id we are processing */
- std::unordered_map<Node, unsigned, NodeHashFunction> d_var_to_curr_inst_id;
+ std::unordered_map<Node, unsigned> d_var_to_curr_inst_id;
/** the amount of slack we added for asserted literals */
- std::unordered_map<Node, Node, NodeHashFunction> d_alit_to_model_slack;
+ std::unordered_map<Node, Node> d_alit_to_model_slack;
//--------------------------------end solved forms
/** rewrite assertion for solve pv
*
* where we guarantee that all subterms of terms in children
* appear in the domain of contains_pv.
*/
- Node rewriteTermForSolvePv(
- Node pv,
- Node n,
- std::vector<Node>& children,
- std::unordered_map<Node, bool, NodeHashFunction>& contains_pv);
+ Node rewriteTermForSolvePv(Node pv,
+ Node n,
+ std::vector<Node>& children,
+ std::unordered_map<Node, bool>& contains_pv);
/** process literal, called from processAssertion
*
* lit is the literal to solve for pv that has been rewritten according to
* visited is the terms we've already visited.
*/
void collectExtracts(Node lem,
- std::map<Node, std::vector<Node> >& extract_map,
- std::unordered_set<TNode, TNodeHashFunction>& visited);
+ std::map<Node, std::vector<Node>>& extract_map,
+ std::unordered_set<TNode>& visited);
};
} // namespace quantifiers
return coeff;
}
-Node normalizePvMult(
- TNode pv,
- const std::vector<Node>& children,
- std::unordered_map<Node, bool, NodeHashFunction>& contains_pv)
+Node normalizePvMult(TNode pv,
+ const std::vector<Node>& children,
+ std::unordered_map<Node, bool>& contains_pv)
{
bool neg, neg_coeff = false;
bool found_pv = false;
#ifdef CVC5_ASSERTIONS
namespace {
-bool isLinearPlus(
- TNode n,
- TNode pv,
- std::unordered_map<Node, bool, NodeHashFunction>& contains_pv)
+bool isLinearPlus(TNode n,
+ TNode pv,
+ std::unordered_map<Node, bool>& contains_pv)
{
Node coeff;
Assert(n.getAttribute(BvLinearAttribute()));
} // namespace
#endif
-Node normalizePvPlus(
- Node pv,
- const std::vector<Node>& children,
- std::unordered_map<Node, bool, NodeHashFunction>& contains_pv)
+Node normalizePvPlus(Node pv,
+ const std::vector<Node>& children,
+ std::unordered_map<Node, bool>& contains_pv)
{
NodeManager* nm;
NodeBuilder nb_c(BITVECTOR_PLUS);
return result;
}
-Node normalizePvEqual(
- Node pv,
- const std::vector<Node>& children,
- std::unordered_map<Node, bool, NodeHashFunction>& contains_pv)
+Node normalizePvEqual(Node pv,
+ const std::vector<Node>& children,
+ std::unordered_map<Node, bool>& contains_pv)
{
Assert(children.size() == 2);
* a null node otherwise. If pv does not occur in children it returns a
* multiplication over children.
*/
-Node normalizePvMult(
- TNode pv,
- const std::vector<Node>& children,
- std::unordered_map<Node, bool, NodeHashFunction>& contains_pv);
+Node normalizePvMult(TNode pv,
+ const std::vector<Node>& children,
+ std::unordered_map<Node, bool>& contains_pv);
/**
* Normalizes the children of a BITVECTOR_PLUS w.r.t. pv. contains_pv marks
* a null node otherwise. If pv does not occur in children it returns an
* addition over children.
*/
-Node normalizePvPlus(
- Node pv,
- const std::vector<Node>& children,
- std::unordered_map<Node, bool, NodeHashFunction>& contains_pv);
+Node normalizePvPlus(Node pv,
+ const std::vector<Node>& children,
+ std::unordered_map<Node, bool>& contains_pv);
/**
* Linearize an equality w.r.t. pv such that pv only occurs once. contains_pv
*
* pv * (-a - 1) = c - b.
*/
-Node normalizePvEqual(
- Node pv,
- const std::vector<Node>& children,
- std::unordered_map<Node, bool, NodeHashFunction>& contains_pv);
+Node normalizePvEqual(Node pv,
+ const std::vector<Node>& children,
+ std::unordered_map<Node, bool>& contains_pv);
} // namespace utils
} // namespace quantifiers
CegHandledStatus CegInstantiator::isCbqiTerm(Node n)
{
CegHandledStatus ret = CEG_HANDLED;
- std::unordered_set<TNode, TNodeHashFunction> visited;
+ std::unordered_set<TNode> visited;
std::vector<TNode> visit;
TNode cur;
visit.push_back(n);
}
Trace("cegqi-inst-debug") << "[3] try based on assertions." << std::endl;
d_curr_iphase[pv] = CEG_INST_PHASE_ASSERTION;
- std::unordered_set<Node, NodeHashFunction> lits;
+ std::unordered_set<Node> lits;
for (unsigned r = 0; r < 2; r++)
{
TheoryId tid = r == 0 ? Theory::theoryOf(pvtn) : THEORY_UF;
bool CegInstantiator::canApplyBasicSubstitution( Node n, std::vector< Node >& non_basic ){
Assert(d_prog_var.find(n) != d_prog_var.end());
if( !non_basic.empty() ){
- for (std::unordered_set<Node, NodeHashFunction>::iterator it =
- d_prog_var[n].begin();
+ for (std::unordered_set<Node>::iterator it = d_prog_var[n].begin();
it != d_prog_var[n].end();
++it)
{
Node CegInstantiator::getBoundVariable(TypeNode tn)
{
unsigned index = 0;
- std::unordered_map<TypeNode, unsigned, TypeNodeHashFunction>::iterator itb =
+ std::unordered_map<TypeNode, unsigned>::iterator itb =
d_bound_var_index.find(tn);
if (itb != d_bound_var_index.end())
{
}
// register variables that were introduced during TheoryEngine preprocessing
- std::unordered_set<Node, NodeHashFunction> ceSyms;
+ std::unordered_set<Node> ceSyms;
expr::getSymbols(lem, ceSyms);
- std::unordered_set<Node, NodeHashFunction> qSyms;
+ std::unordered_set<Node> qSyms;
expr::getSymbols(d_quant, qSyms);
// all variables that are in counterexample lemma but not in quantified
// formula
/** cache from nodes to the set of variables it contains
* (from the quantified formula we are instantiating).
*/
- std::unordered_map<Node,
- std::unordered_set<Node, NodeHashFunction>,
- NodeHashFunction>
- d_prog_var;
+ std::unordered_map<Node, std::unordered_set<Node>> d_prog_var;
/** cache of the set of terms that we have established are
* ineligible for instantiation.
*/
- std::unordered_set<Node, NodeHashFunction> d_inelig;
+ std::unordered_set<Node> d_inelig;
/** ensures n is in d_prog_var and d_inelig. */
void computeProgVars(Node n);
//-------------------------------end globally cached
/** map from types to representatives of that type */
std::map<TypeNode, std::vector<Node> > d_curr_type_eqc;
/** solved asserts */
- std::unordered_set<Node, NodeHashFunction> d_solved_asserts;
+ std::unordered_set<Node> d_solved_asserts;
/** process assertions
* This is called once at the beginning of check to
* set up all necessary information for constructing instantiations,
/** cache bound variables for type returned
* by getBoundVariable(...).
*/
- std::unordered_map<TypeNode, std::vector<Node>, TypeNodeHashFunction>
- d_bound_var;
+ std::unordered_map<TypeNode, std::vector<Node>> d_bound_var;
/** current index of bound variables for type.
* The next call to getBoundVariable(...) for
* type tn returns the d_bound_var_index[tn]^th
* element of d_bound_var[tn], or a fresh variable
* if not in bounds.
*/
- std::unordered_map<TypeNode, unsigned, TypeNodeHashFunction>
- d_bound_var_index;
+ std::unordered_map<TypeNode, unsigned> d_bound_var_index;
//-------------------------------end cached per round
//-------------------------------data per theory
*/
std::vector<Node> d_vars;
/** set form of d_vars */
- std::unordered_set<Node, NodeHashFunction> d_vars_set;
+ std::unordered_set<Node> d_vars_set;
/** index of variables reported in instantiation */
std::vector<unsigned> d_var_order_index;
/** number of input variables
*/
class InstStrategyCegqi : public QuantifiersModule
{
- typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
- typedef context::CDHashMap< Node, int, NodeHashFunction> NodeIntMap;
+ typedef context::CDHashSet<Node> NodeSet;
+ typedef context::CDHashMap<Node, int> NodeIntMap;
public:
InstStrategyCegqi(QuantifiersState& qs,
return d_qnqe.find(q) != d_qnqe.end();
}
-bool NestedQe::getNestedQuantification(
- Node q, std::unordered_set<Node, NodeHashFunction>& nqs)
+bool NestedQe::getNestedQuantification(Node q, std::unordered_set<Node>& nqs)
{
expr::getKindSubterms(q[1], kind::FORALL, true, nqs);
return !nqs.empty();
bool NestedQe::hasNestedQuantification(Node q)
{
- std::unordered_set<Node, NodeHashFunction> nqs;
+ std::unordered_set<Node> nqs;
return getNestedQuantification(q, nqs);
}
inputExists = true;
}
Assert(q.getKind() == kind::FORALL);
- std::unordered_set<Node, NodeHashFunction> nqs;
+ std::unordered_set<Node> nqs;
if (!getNestedQuantification(q, nqs))
{
Trace("cegqi-nested-qe-debug")
class NestedQe
{
- using NodeNodeMap = context::CDHashMap<Node, Node, NodeHashFunction>;
+ using NodeNodeMap = context::CDHashMap<Node, Node>;
public:
NestedQe(context::UserContext* u);
* Get nested quantification. Returns true if q has nested quantifiers.
* Adds each nested quantifier in the body of q to nqs.
*/
- static bool getNestedQuantification(
- Node q, std::unordered_set<Node, NodeHashFunction>& nqs);
+ static bool getNestedQuantification(Node q, std::unordered_set<Node>& nqs);
/**
* Does quantified formula q have nested quantification?
*/
friend class SubsEqcIndex;
friend class TermGenerator;
friend class TermGenEnv;
- typedef context::CDHashMap< Node, Node, NodeHashFunction > NodeMap;
- typedef context::CDHashMap< Node, bool, NodeHashFunction > BoolMap;
-//this class maintains a congruence closure for *universal* facts
-private:
+ typedef context::CDHashMap<Node, Node> NodeMap;
+ typedef context::CDHashMap<Node, bool> BoolMap;
+ // this class maintains a congruence closure for *universal* facts
+ private:
//notification class for equality engine
class NotifyClass : public eq::EqualityEngineNotify {
ConjectureGenerator& d_sg;
void HigherOrderTrigger::collectHoVarApplyTerms(
Node q, std::vector<Node>& ns, std::map<Node, std::vector<Node> >& apps)
{
- std::unordered_map<TNode, Node, TNodeHashFunction> visited;
- std::unordered_map<TNode, Node, TNodeHashFunction>::iterator it;
+ std::unordered_map<TNode, Node> visited;
+ std::unordered_map<TNode, Node>::iterator it;
// whether the visited node is a child of a HO_APPLY chain
- std::unordered_map<TNode, bool, TNodeHashFunction> withinApply;
+ std::unordered_map<TNode, bool> withinApply;
std::vector<TNode> visit;
TNode cur;
for (unsigned i = 0, size = ns.size(); i < size; i++)
std::map<TNode, std::vector<Node> > d_ho_var_bvs;
std::map<TNode, Node> d_ho_var_bvl;
/** the set of types of ho variables */
- std::unordered_set<TypeNode, TypeNodeHashFunction> d_ho_var_types;
+ std::unordered_set<TypeNode> d_ho_var_types;
/** add higher-order type predicate lemmas
*
* Adds lemmas of the form P( f ), where P is the predicate
{
Assert(n1 != n2);
int status = 0;
- std::unordered_set<TNode, TNodeHashFunction> subs_vars;
+ std::unordered_set<TNode> subs_vars;
std::unordered_set<
std::pair<TNode, TNode>,
- PairHashFunction<TNode, TNode, TNodeHashFunction, TNodeHashFunction> >
+ PairHashFunction<TNode, TNode, std::hash<TNode>, std::hash<TNode>>>
visited;
std::vector<std::pair<TNode, TNode> > visit;
std::pair<TNode, TNode> cur;
std::vector<Node>& gts)
{
NodeManager* nm = NodeManager::currentNM();
- std::unordered_map<TNode, Node, TNodeHashFunction> visited;
- std::unordered_map<TNode, Node, TNodeHashFunction>::iterator it;
+ std::unordered_map<TNode, Node> visited;
+ std::unordered_map<TNode, Node>::iterator it;
std::vector<TNode> visit;
TNode cur;
visit.push_back(n);
return Node::null();
}
// now, make sure that no other member of the class is an instance
- std::unordered_map<TNode, Node, TNodeHashFunction> cache;
+ std::unordered_map<TNode, Node> cache;
r_best = getInstance(r_best, eqc, cache);
// store that this representative was chosen at this point
if (d_rep_score.find(r_best) == d_rep_score.end())
//helper functions
-Node EqualityQuery::getInstance(
- Node n,
- const std::vector<Node>& eqc,
- std::unordered_map<TNode, Node, TNodeHashFunction>& cache)
+Node EqualityQuery::getInstance(Node n,
+ const std::vector<Node>& eqc,
+ std::unordered_map<TNode, Node>& cache)
{
if(cache.find(n) != cache.end()) {
return cache[n];
/** processInferences : will merge equivalence classes in master equality engine, if possible */
bool processInferences( Theory::Effort e );
/** node contains */
- Node getInstance( Node n, const std::vector< Node >& eqc, std::unordered_map<TNode, Node, TNodeHashFunction>& cache );
+ Node getInstance(Node n,
+ const std::vector<Node>& eqc,
+ std::unordered_map<TNode, Node>& cache);
/** get score */
int32_t getRepScore(Node n, Node f, size_t index, TypeNode v_tn);
}; /* EqualityQuery */
// the processing terms
std::vector<Node> clauses;
// the terms we have propagated information to
- std::unordered_set<Node, NodeHashFunction> prop_clauses;
+ std::unordered_set<Node> prop_clauses;
// the assignment
std::map<Node, Node> assign;
std::vector<Node> avars;
const std::map<Node, Node>& assign,
const std::map<Kind, bool>& rkinds)
{
- std::unordered_map<TNode, Node, TNodeHashFunction> visited;
- std::unordered_map<TNode, Node, TNodeHashFunction>::iterator it;
+ std::unordered_map<TNode, Node> visited;
+ std::unordered_map<TNode, Node>::iterator it;
std::map<Node, Node>::const_iterator ita;
std::vector<TNode> visit;
TNode cur;
class BoundedIntegers : public QuantifiersModule
{
- typedef context::CDHashMap<Node, bool, NodeHashFunction> NodeBoolMap;
- typedef context::CDHashMap<Node, int, NodeHashFunction> NodeIntMap;
- typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeNodeMap;
+ typedef context::CDHashMap<Node, bool> NodeBoolMap;
+ typedef context::CDHashMap<Node, int> NodeIntMap;
+ typedef context::CDHashMap<Node, Node> NodeNodeMap;
typedef context::CDHashMap<int, bool> IntBoolMap;
private:
//for determining bounds
{
std::vector< Node > d_terms;
// number of arguments that are model-basis terms
- std::unordered_map<Node, unsigned, NodeHashFunction> d_mba_count;
+ std::unordered_map<Node, unsigned> d_mba_count;
bool operator() (int i,int j) {
return (d_mba_count[d_terms[i]] < d_mba_count[d_terms[j]]);
}
std::map<Node, Node > d_quant_cond;
/** A set of quantified formulas that cannot be handled by model-based
* quantifier instantiation */
- std::unordered_set<Node, NodeHashFunction> d_unhandledQuant;
+ std::unordered_set<Node> d_unhandledQuant;
std::map< TypeNode, Node > d_array_cond;
std::map< Node, Node > d_array_term_cond;
std::map< Node, std::vector< int > > d_star_insts;
Assert(Rewriter::rewrite(n) == n);
Trace("fd-eval") << "FunDefEvaluator: evaluate " << n << std::endl;
NodeManager* nm = NodeManager::currentNM();
- std::unordered_map<TNode, unsigned, TNodeHashFunction> funDefCount;
- std::unordered_map<TNode, unsigned, TNodeHashFunction>::iterator itCount;
- std::unordered_map<TNode, Node, TNodeHashFunction> visited;
- std::unordered_map<TNode, Node, TNodeHashFunction>::iterator it;
+ std::unordered_map<TNode, unsigned> funDefCount;
+ std::unordered_map<TNode, unsigned>::iterator itCount;
+ std::unordered_map<TNode, Node> visited;
+ std::unordered_map<TNode, Node>::iterator it;
std::map<Node, FunDefInfo>::const_iterator itf;
std::vector<TNode> visit;
TNode cur;
*/
class Instantiate : public QuantifiersUtil
{
- using NodeInstListMap = context::
- CDHashMap<Node, std::shared_ptr<InstLemmaList>, NodeHashFunction>;
+ using NodeInstListMap =
+ context::CDHashMap<Node, std::shared_ptr<InstLemmaList>>;
public:
Instantiate(QuantifiersState& qs,
* The list of quantified formulas for which the domain of d_c_inst_match_trie
* is valid.
*/
- context::CDHashSet<Node, NodeHashFunction> d_c_inst_match_trie_dom;
+ context::CDHashSet<Node> d_c_inst_match_trie_dom;
/**
* A CDProof storing instantiation steps.
*/
{
return Node::null();
}
- std::unordered_map<Node, Node, NodeHashFunction> subs;
+ std::unordered_map<Node, Node> subs;
if (!expr::match(exists[1], p, subs))
{
return Node::null();
bool QuantifiersBoundInference::mayComplete(TypeNode tn)
{
- std::unordered_map<TypeNode, bool, TypeNodeHashFunction>::iterator it =
- d_may_complete.find(tn);
+ std::unordered_map<TypeNode, bool>::iterator it = d_may_complete.find(tn);
if (it == d_may_complete.end())
{
// cache
/** Whether finite model finding is enabled */
bool d_isFmf;
/** may complete */
- std::unordered_map<TypeNode, bool, TypeNodeHashFunction> d_may_complete;
+ std::unordered_map<TypeNode, bool> d_may_complete;
/** The bounded integers module, which may help infer bounds */
BoundedIntegers* d_bint;
};
bool QuantConflictFind::isPropagatingInstance(Node n) const
{
- std::unordered_set<TNode, TNodeHashFunction> visited;
+ std::unordered_set<TNode> visited;
std::vector<TNode> visit;
TNode cur;
visit.push_back(n);
{
friend class MatchGen;
friend class QuantInfo;
- typedef context::CDHashMap<Node, bool, NodeHashFunction> NodeBoolMap;
-private:
+ typedef context::CDHashMap<Node, bool> NodeBoolMap;
+
+ private:
context::CDO< bool > d_conflict;
std::map< Kind, Node > d_zero;
//for storing nodes created during t-constraint solving (prevents memory leaks)
* one variable per quantified formula at a time.
*/
class QuantDSplit : public QuantifiersModule {
- typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
+ typedef context::CDHashSet<Node> NodeSet;
public:
QuantDSplit(QuantifiersState& qs,
bool QuantifiersMacros::containsBadOp(Node n, Node op, bool reqGround)
{
- std::unordered_set<TNode, TNodeHashFunction> visited;
- std::unordered_set<TNode, TNodeHashFunction>::iterator it;
+ std::unordered_set<TNode> visited;
+ std::unordered_set<TNode>::iterator it;
std::vector<TNode> visit;
TNode cur;
visit.push_back(n);
{
// compute variables in itm->first, these are not eligible for
// elimination
- std::unordered_set<Node, NodeHashFunction> fvs;
+ std::unordered_set<Node> fvs;
expr::getFreeVariables(m.first, fvs);
for (const Node& v : fvs)
{
}
// traverse the body, invalidate variables if they occur in places other than
// the bounds they occur in
- std::unordered_map<TNode, std::unordered_set<int>, TNodeHashFunction>
- evisited;
+ std::unordered_map<TNode, std::unordered_set<int>> evisited;
std::vector<TNode> evisit;
std::vector<int> evisit_pol;
TNode ecur;
return body;
}
-Node QuantifiersRewriter::computePrenex(
- Node q,
- Node body,
- std::unordered_set<Node, NodeHashFunction>& args,
- std::unordered_set<Node, NodeHashFunction>& nargs,
- bool pol,
- bool prenexAgg)
+Node QuantifiersRewriter::computePrenex(Node q,
+ Node body,
+ std::unordered_set<Node>& args,
+ std::unordered_set<Node>& nargs,
+ bool pol,
+ bool prenexAgg)
{
NodeManager* nm = NodeManager::currentNM();
Kind k = body.getKind();
}
else
{
- std::unordered_set<Node, NodeHashFunction> argsSet;
- std::unordered_set<Node, NodeHashFunction> nargsSet;
+ std::unordered_set<Node> argsSet;
+ std::unordered_set<Node> nargsSet;
Node q;
Node nn = computePrenex(q, n, argsSet, nargsSet, true, true);
Assert(n != nn || argsSet.empty());
}
else
{
- std::unordered_set<Node, NodeHashFunction> argsSet, nargsSet;
+ std::unordered_set<Node> argsSet, nargsSet;
n = computePrenex(f, n, argsSet, nargsSet, true, false);
Assert(nargsSet.empty());
args.insert(args.end(), argsSet.begin(), argsSet.end());
*/
static Node computePrenex(Node q,
Node body,
- std::unordered_set<Node, NodeHashFunction>& args,
- std::unordered_set<Node, NodeHashFunction>& nargs,
+ std::unordered_set<Node>& args,
+ std::unordered_set<Node>& nargs,
bool pol,
bool prenexAgg);
/**
private:
/** cache of all terms registered to this generator */
- std::unordered_set<Node, NodeHashFunction> d_terms;
+ std::unordered_set<Node> d_terms;
/** the threshold used by this module for maximum number of sat points */
unsigned d_deqThresh;
/**
Trace("si-prt-debug") << "...normalized invocations to " << cr
<< std::endl;
// now must check if it has other bound variables
- std::unordered_set<Node, NodeHashFunction> fvs;
+ std::unordered_set<Node> fvs;
expr::getFreeVariables(cr, fvs);
// bound variables must be contained in the single invocation variables
for (const Node& bv : fvs)
Trace("si-prt") << "...not single invocation." << std::endl;
singleInvocation = false;
// rename bound variables with maximal overlap with si_vars
- std::unordered_set<Node, NodeHashFunction> fvs;
+ std::unordered_set<Node> fvs;
expr::getFreeVariables(cr, fvs);
std::vector<Node> termsNs;
std::vector<Node> subsNs;
Trace("si-prt") << ".....got si=" << singleInvocation
<< ", result : " << cr << std::endl;
d_conjuncts[2].push_back(cr);
- std::unordered_set<Node, NodeHashFunction> fvs;
+ std::unordered_set<Node> fvs;
expr::getFreeVariables(cr, fvs);
d_all_vars.insert(fvs.begin(), fvs.end());
if (singleInvocation)
std::vector<Node> d_si_vars;
/** every free variable of conjuncts[2] */
- std::unordered_set<Node, NodeHashFunction> d_all_vars;
+ std::unordered_set<Node> d_all_vars;
/** map from functions to first-order variables that anti-skolemized them */
std::map<Node, Node> d_func_fo_var;
/** map from first-order variables to the function it anti-skolemized */
bool Skolemize::getSkolemConstants(Node q, std::vector<Node>& skolems)
{
- std::unordered_map<Node, std::vector<Node>, NodeHashFunction>::iterator it =
+ std::unordered_map<Node, std::vector<Node>>::iterator it =
d_skolem_constants.find(q);
if (it != d_skolem_constants.end())
{
Node Skolemize::getSkolemConstant(Node q, unsigned i)
{
- std::unordered_map<Node, std::vector<Node>, NodeHashFunction>::iterator it =
+ std::unordered_map<Node, std::vector<Node>>::iterator it =
d_skolem_constants.find(q);
if (it != d_skolem_constants.end())
{
Node Skolemize::getSkolemizedBody(Node f)
{
Assert(f.getKind() == FORALL);
- std::unordered_map<Node, Node, NodeHashFunction>::iterator it =
- d_skolem_body.find(f);
+ std::unordered_map<Node, Node>::iterator it = d_skolem_body.find(f);
if (it == d_skolem_body.end())
{
std::vector<TypeNode> fvTypes;
void Skolemize::getSkolemTermVectors(
std::map<Node, std::vector<Node> >& sks) const
{
- std::unordered_map<Node, std::vector<Node>, NodeHashFunction>::const_iterator
- itk;
+ std::unordered_map<Node, std::vector<Node>>::const_iterator itk;
for (const auto& p : d_skolemized)
{
Node q = p.first;
*/
class Skolemize
{
- typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeNodeMap;
+ typedef context::CDHashMap<Node, Node> NodeNodeMap;
public:
Skolemize(QuantifiersState& qs, TermRegistry& tr, ProofNodeManager* pnm);
/** quantified formulas that have been skolemized */
NodeNodeMap d_skolemized;
/** map from quantified formulas to the list of skolem constants */
- std::unordered_map<Node, std::vector<Node>, NodeHashFunction>
- d_skolem_constants;
+ std::unordered_map<Node, std::vector<Node>> d_skolem_constants;
/** map from quantified formulas to their skolemized body */
- std::unordered_map<Node, Node, NodeHashFunction> d_skolem_body;
+ std::unordered_map<Node, Node> d_skolem_body;
/** Pointer to the proof node manager */
ProofNodeManager* d_pnm;
/** Eager proof generator for skolemization lemmas */
for (unsigned r = 0; r < 2; r++)
{
- std::unordered_set<Node, NodeHashFunction>& rlemmas =
+ std::unordered_set<Node>& rlemmas =
r == 0 ? d_refinement_lemma_unit : d_refinement_lemma_conj;
for (const Node& lem : rlemmas)
{
// Maybe we already evaluated some terms in refinement lemmas.
// In particular, the example eval cache for f may have some evaluations
// cached, which we add to evalVisited and pass to the evaluator below.
- std::unordered_map<Node, Node, NodeHashFunction> evalVisited;
+ std::unordered_map<Node, Node> evalVisited;
ExampleInfer* ei = d_parent->getExampleInfer();
for (unsigned i = 0, vsize = vs.size(); i < vsize; i++)
{
Evaluator* eval = d_tds->getEvaluator();
for (unsigned r = 0; r < 2; r++)
{
- std::unordered_set<Node, NodeHashFunction>& rlemmas =
+ std::unordered_set<Node>& rlemmas =
r == 0 ? d_refinement_lemma_unit : d_refinement_lemma_conj;
for (const Node& lem : rlemmas)
{
/** refinement lemmas */
std::vector<Node> d_refinement_lemmas;
/** (processed) conjunctions of refinement lemmas that are not unit */
- std::unordered_set<Node, NodeHashFunction> d_refinement_lemma_conj;
+ std::unordered_set<Node> d_refinement_lemma_conj;
/** (processed) conjunctions of refinement lemmas that are unit */
- std::unordered_set<Node, NodeHashFunction> d_refinement_lemma_unit;
+ std::unordered_set<Node> d_refinement_lemma_unit;
/** substitution entailed by d_refinement_lemma_unit */
std::vector<Node> d_rl_eval_hds;
std::vector<Node> d_rl_vals;
/** all variables appearing in refinement lemmas */
- std::unordered_set<Node, NodeHashFunction> d_refinement_lemma_vars;
+ std::unordered_set<Node> d_refinement_lemma_vars;
/** adds lem as a refinement lemma */
void addRefinementLemma(Node lem);
{
// check refinement points
Node etsrn = d == 0 ? etsr : etsr.negate();
- std::unordered_set<Node, NodeHashFunction> visited;
+ std::unordered_set<Node> visited;
std::vector<Node> pt;
Node rid = cfilter.getRefinementPt(this, etsrn, visited, pt);
if (!rid.isNull())
Node CegisCoreConnective::Component::getRefinementPt(
CegisCoreConnective* p,
Node n,
- std::unordered_set<Node, NodeHashFunction>& visited,
+ std::unordered_set<Node>& visited,
std::vector<Node>& ss)
{
std::vector<Node> ctx;
bool CegisCoreConnective::getUnsatCore(
SmtEngine& smt,
- const std::unordered_set<Node, NodeHashFunction>& queryAsserts,
+ const std::unordered_set<Node>& queryAsserts,
std::vector<Node>& uasserts) const
{
UnsatCore uc = smt.getUnsatCore();
}
return nm->mkConst(!expRes);
}
- std::unordered_map<Node, Node, NodeHashFunction>& ec = d_eval_cache[n];
+ std::unordered_map<Node, Node>& ec = d_eval_cache[n];
if (!id.isNull())
{
- std::unordered_map<Node, Node, NodeHashFunction>::iterator it = ec.find(id);
+ std::unordered_map<Node, Node>::iterator it = ec.find(id);
if (it != ec.end())
{
return it->second;
? d_true
: (asserts.size() == 1 ? asserts[0] : nm->mkNode(AND, asserts));
std::vector<Node> mvs;
- std::unordered_set<Node, NodeHashFunction> visited;
+ std::unordered_set<Node> visited;
bool addSuccess = true;
// Ensure that the current conjunction evaluates to false on all refinement
// points. We get refinement points until we have exhausted.
// "Let U be a subset of D such that S ^ U ^ ~B is unsat."
// and uasserts is set to U.
std::vector<Node> uasserts;
- std::unordered_set<Node, NodeHashFunction> queryAsserts;
+ std::unordered_set<Node> queryAsserts;
queryAsserts.insert(ccheck.getFormula());
queryAsserts.insert(d_sc);
bool hasQuery = getUnsatCore(*checkSol, queryAsserts, uasserts);
// "Let W be a subset of D such that S ^ W is unsat."
// and uasserts is set to W.
uasserts.clear();
- std::unordered_set<Node, NodeHashFunction> queryAsserts2;
+ std::unordered_set<Node> queryAsserts2;
queryAsserts2.insert(d_sc);
getUnsatCore(*checkSc, queryAsserts2, uasserts);
falseCore = true;
*/
Node getRefinementPt(CegisCoreConnective* p,
Node n,
- std::unordered_set<Node, NodeHashFunction>& visited,
+ std::unordered_set<Node>& visited,
std::vector<Node>& ss);
/** Get term pool, i.e. pool(A)/pool(B) in the algorithms above */
void getTermPool(std::vector<Node>& passerts) const;
* If one of the formulas in queryAsserts was in the unsat core, then this
* method returns true. Otherwise, this method returns false.
*/
- bool getUnsatCore(
- SmtEngine& smt,
- const std::unordered_set<Node, NodeHashFunction>& queryAsserts,
- std::vector<Node>& uasserts) const;
+ bool getUnsatCore(SmtEngine& smt,
+ const std::unordered_set<Node>& queryAsserts,
+ std::vector<Node>& uasserts) const;
/**
* Return the result of checking satisfiability of formula n.
* If n was satisfiable, then we store the model for d_vars in mvs.
*/
Node evaluate(Node n, Node id, const std::vector<Node>& mvs);
/** A cache of the above function */
- std::unordered_map<Node,
- std::unordered_map<Node, Node, NodeHashFunction>,
- NodeHashFunction>
- d_eval_cache;
+ std::unordered_map<Node, std::unordered_map<Node, Node>> d_eval_cache;
/** The evaluator utility used for the above function */
Evaluator d_eval;
//-----------------------------------end for evaluation
}
// collect variables occurring in value
std::vector<Node> vars;
- std::unordered_set<Node, NodeHashFunction> visited;
+ std::unordered_set<Node> visited;
collectVars(value, vars, visited);
// partition permutation variables
d_curr_ind = 0;
Trace("synth-stream-concrete") << " ..permutting vars :";
- std::unordered_set<Node, NodeHashFunction> seen_vars;
+ std::unordered_set<Node> seen_vars;
for (const Node& v_cons : vars)
{
Assert(cons_var.find(v_cons) != cons_var.end());
return it->second.size();
}
-void EnumStreamPermutation::collectVars(
- Node n,
- std::vector<Node>& vars,
- std::unordered_set<Node, NodeHashFunction>& visited)
+void EnumStreamPermutation::collectVars(Node n,
+ std::vector<Node>& vars,
+ std::unordered_set<Node>& visited)
{
if (visited.find(n) != visited.end())
{
/** value to which we are generating permutations */
Node d_value;
/** generated permutations (modulo rewriting) */
- std::unordered_set<Node, NodeHashFunction> d_perm_values;
+ std::unordered_set<Node> d_perm_values;
/** retrieves variables occurring in value */
void collectVars(Node n,
std::vector<Node>& vars,
- std::unordered_set<Node, NodeHashFunction>& visited);
+ std::unordered_set<Node>& visited);
/** Utility for stepwise application of Heap's algorithm for permutation
*
* see https://en.wikipedia.org/wiki/Heap%27s_algorithm
*/
Node d_last;
/** generated combinations */
- std::unordered_set<Node, NodeHashFunction> d_comb_values;
+ std::unordered_set<Node> d_comb_values;
/** permutation utility */
EnumStreamPermutation d_stream_permutations;
/** Utility for stepwise generation of ordered subsets of size k from n
d_examplesOut[v].clear();
d_examplesTerm[v].clear();
}
- std::map<std::pair<bool, bool>, std::unordered_set<Node, NodeHashFunction>>
- visited;
+ std::map<std::pair<bool, bool>, std::unordered_set<Node>> visited;
// n is negated conjecture
if (!collectExamples(n, visited, true, false))
{
bool ExampleInfer::collectExamples(
Node n,
- std::map<std::pair<bool, bool>, std::unordered_set<Node, NodeHashFunction>>&
- visited,
+ std::map<std::pair<bool, bool>, std::unordered_set<Node>>& visited,
bool hasPol,
bool pol)
{
*/
bool collectExamples(
Node n,
- std::map<std::pair<bool, bool>,
- std::unordered_set<Node, NodeHashFunction>>& visited,
+ std::map<std::pair<bool, bool>, std::unordered_set<Node>>& visited,
bool hasPol,
bool pol);
/** Pointer to the sygus term database */
d_vars.insert(d_vars.end(), vars.begin(), vars.end());
// compute its free variables
- std::unordered_set<Node, NodeHashFunction> fvs;
+ std::unordered_set<Node> fvs;
expr::getFreeVariables(n, fvs);
for (size_t i = 0, vsize = vars.size(); i < vsize; i++)
{
{
}
-const std::unordered_set<Node, NodeHashFunction>&
-RConsObligationInfo::getBuiltins() const
+const std::unordered_set<Node>& RConsObligationInfo::getBuiltins() const
{
return d_builtins;
}
d_builtins.emplace(builtin);
}
-const std::unordered_set<Node, NodeHashFunction>&
-RConsObligationInfo::getCandidateSolutions() const
+const std::unordered_set<Node>& RConsObligationInfo::getCandidateSolutions()
+ const
{
return d_candSols;
}
d_watchSet.emplace(candSol);
}
-const std::unordered_set<Node, NodeHashFunction>&
-RConsObligationInfo::getWatchSet() const
+const std::unordered_set<Node>& RConsObligationInfo::getWatchSet() const
{
return d_watchSet;
}
{
std::stringstream ss;
ss << "([";
- std::unordered_set<Node, NodeHashFunction>::const_iterator it =
- obInfo.getBuiltins().cbegin();
+ std::unordered_set<Node>::const_iterator it = obInfo.getBuiltins().cbegin();
ss << *it;
++it;
while (it != obInfo.getBuiltins().cend())
void RConsObligationInfo::printCandSols(
const Node& root,
- const std::unordered_map<Node, RConsObligationInfo, NodeHashFunction>&
- obInfo)
+ const std::unordered_map<Node, RConsObligationInfo>& obInfo)
{
- std::unordered_set<Node, NodeHashFunction> visited;
+ std::unordered_set<Node> visited;
std::vector<Node> stack;
stack.push_back(root);
for (const Node& j : obInfo.at(k).getCandidateSolutions())
{
Trace("sygus-rcons") << datatypes::utils::sygusToBuiltin(j) << " ";
- std::unordered_set<TNode, TNodeHashFunction> subObs;
+ std::unordered_set<TNode> subObs;
expr::getVariables(j, subObs);
for (const TNode& l : subObs)
{
/**
* @return equivalent builtin terms to reconstruct for this class' obligation
*/
- const std::unordered_set<Node, NodeHashFunction>& getBuiltins() const;
+ const std::unordered_set<Node>& getBuiltins() const;
/**
* Add candidate solution to the set of candidate solutions for the
/**
* @return set of candidate solutions for this class' obligation
*/
- const std::unordered_set<Node, NodeHashFunction>& getCandidateSolutions()
- const;
+ const std::unordered_set<Node>& getCandidateSolutions() const;
/**
* Add candidate solution to the set of candidate solutions waiting for the
* @return set of candidate solutions waiting for this class' obligation
* to be solved
*/
- const std::unordered_set<Node, NodeHashFunction>& getWatchSet() const;
+ const std::unordered_set<Node>& getWatchSet() const;
/**
* Return a string representation of an obligation.
*/
static void printCandSols(
const Node& root,
- const std::unordered_map<Node, RConsObligationInfo, NodeHashFunction>&
- obInfo);
+ const std::unordered_map<Node, RConsObligationInfo>& obInfo);
private:
/** Equivalent builtin terms for this class' obligation.
* To solve the obligation, one of these builtin terms must be reconstructed
* in the specified grammar (sygus datatype type) of the obligation.
*/
- std::unordered_set<Node, NodeHashFunction> d_builtins;
+ std::unordered_set<Node> d_builtins;
/** A set of candidate solutions to this class' obligation.
*
* Each candidate solution is a sygus datatype term containing skolem subterms
* where c_z1 and c_z2 are skolems. Notice that `d_candSols` may contain a
* pure term that solves the obligation ((c_+ c_x c_y) in this example).
*/
- std::unordered_set<Node, NodeHashFunction> d_candSols;
+ std::unordered_set<Node> d_candSols;
/** A set of candidate solutions waiting for this class' obligation to
* be solved.
*
* the watch-set of c_z2. Similarly, (c_+ c_z1 c_z2) and (c_+ c_z1 c_y) are in
* the watch-set of c_z1.
*/
- std::unordered_set<Node, NodeHashFunction> d_watchSet;
+ std::unordered_set<Node> d_watchSet;
};
} // namespace quantifiers
* possible to have multiple obligations to reconstruct the same builtin term
* from different sygus datatype types.
*/
- std::unordered_map<Node, Node, NodeHashFunction> d_ob;
+ std::unordered_map<Node, Node> d_ob;
};
} // namespace quantifiers
{
NodeManager* nm = NodeManager::currentNM();
SkolemManager* sm = nm->getSkolemManager();
- std::unordered_set<Node, NodeHashFunction> symset;
+ std::unordered_set<Node> symset;
for (size_t i = 0, size = asserts.size(); i < size; i++)
{
expr::getSymbols(asserts[i], symset);
Node n, std::map<TypeNode, int>& vcounter)
{
NodeManager* nm = NodeManager::currentNM();
- std::unordered_map<TNode, Node, TNodeHashFunction> visited;
- std::unordered_map<TNode, Node, TNodeHashFunction>::iterator it;
+ std::unordered_map<TNode, Node> visited;
+ std::unordered_map<TNode, Node>::iterator it;
std::vector<TNode> visit;
TNode cur;
visit.push_back(n);
/** the list of sygus terms we have enumerated */
std::vector<Node> d_terms;
/** the set of builtin terms corresponding to the above list */
- std::unordered_set<Node, NodeHashFunction> d_bterms;
+ std::unordered_set<Node> d_bterms;
/**
* The index of first term whose size is greater than or equal to that size,
* if it exists.
* lemma that entails ~is-C( d_enum ) was registered to
* TermDbSygus::registerSymBreakLemma.
*/
- std::unordered_set<Node, NodeHashFunction> d_sbExcTlCons;
+ std::unordered_set<Node> d_sbExcTlCons;
//-------------------------------- end externally specified symmetry breaking
};
/** the current term */
Node d_currTerm;
/** cache of (enumerated) builtin values we have enumerated so far */
- std::unordered_set<Node, NodeHashFunction> d_cache;
+ std::unordered_set<Node> d_cache;
};
} // namespace quantifiers
std::vector<Node>& vals,
std::vector<Node>& exps)
{
- std::map<Node, std::unordered_set<Node, NodeHashFunction> >::iterator its =
- d_subterms.find(a);
+ std::map<Node, std::unordered_set<Node> >::iterator its = d_subterms.find(a);
if (its == d_subterms.end())
{
return;
/** sygus term database associated with this utility */
TermDbSygus* d_tds;
/** the set of evaluation terms we have already processed */
- std::unordered_set<Node, NodeHashFunction> d_eval_processed;
+ std::unordered_set<Node> d_eval_processed;
/** map from evaluation heads to evaluation function applications */
std::map<Node, std::vector<Node> > d_evals;
/**
* This maps anchor terms to the set of shared selector chains with
* them as an anchor, for example x may map to { x, x.1, x.2, x.1.1 }.
*/
- std::map<Node, std::unordered_set<Node, NodeHashFunction> > d_subterms;
+ std::map<Node, std::unordered_set<Node> > d_subterms;
};
} // namespace quantifiers
}
void CegGrammarConstructor::collectTerms(
- Node n,
- std::map<TypeNode, std::unordered_set<Node, NodeHashFunction>>& consts)
+ Node n, std::map<TypeNode, std::unordered_set<Node>>& consts)
{
- std::unordered_map<TNode, bool, TNodeHashFunction> visited;
- std::unordered_map<TNode, bool, TNodeHashFunction>::iterator it;
+ std::unordered_map<TNode, bool> visited;
+ std::unordered_map<TNode, bool>::iterator it;
std::stack<TNode> visit;
TNode cur;
visit.push(n);
// now, construct the grammar
Trace("cegqi") << "SynthConjecture : convert to deep embedding..."
<< std::endl;
- std::map<TypeNode, std::unordered_set<Node, NodeHashFunction>> extra_cons;
+ std::map<TypeNode, std::unordered_set<Node>> extra_cons;
if( options::sygusAddConstGrammar() ){
Trace("cegqi") << "SynthConjecture : collect constants..." << std::endl;
collectTerms( q[1], extra_cons );
}
- std::map<TypeNode, std::unordered_set<Node, NodeHashFunction>> exc_cons;
- std::map<TypeNode, std::unordered_set<Node, NodeHashFunction>> inc_cons;
+ std::map<TypeNode, std::unordered_set<Node>> exc_cons;
+ std::map<TypeNode, std::unordered_set<Node>> inc_cons;
NodeManager* nm = NodeManager::currentNM();
// check which arguments are irrelevant
std::unordered_set<unsigned> arg_irrelevant;
d_parent->getProcess()->getIrrelevantArgs(sf, arg_irrelevant);
- std::unordered_set<Node, NodeHashFunction> term_irlv;
+ std::unordered_set<Node> term_irlv;
// convert to term
for (const unsigned& arg : arg_irrelevant)
{
Node CegGrammarConstructor::convertToEmbedding(Node n)
{
NodeManager* nm = NodeManager::currentNM();
- std::unordered_map<TNode, Node, TNodeHashFunction> visited;
- std::unordered_map<TNode, Node, TNodeHashFunction>::iterator it;
+ std::unordered_map<TNode, Node> visited;
+ std::unordered_map<TNode, Node>::iterator it;
std::stack<TNode> visit;
TNode cur;
visit.push(n);
TypeNode range,
Node bvl,
const std::string& fun,
- std::map<TypeNode, std::unordered_set<Node, NodeHashFunction>>& extra_cons,
- std::map<TypeNode, std::unordered_set<Node, NodeHashFunction>>&
- exclude_cons,
- const std::map<TypeNode, std::unordered_set<Node, NodeHashFunction>>&
- include_cons,
- std::unordered_set<Node, NodeHashFunction>& term_irrelevant,
+ std::map<TypeNode, std::unordered_set<Node>>& extra_cons,
+ std::map<TypeNode, std::unordered_set<Node>>& exclude_cons,
+ const std::map<TypeNode, std::unordered_set<Node>>& include_cons,
+ std::unordered_set<Node>& term_irrelevant,
std::vector<SygusDatatypeGenerator>& sdts,
std::set<TypeNode>& unres)
{
// create placeholders for collected types
std::vector<TypeNode> unres_types;
std::map<TypeNode, TypeNode> type_to_unres;
- std::map<TypeNode, std::unordered_set<Node, NodeHashFunction>>::const_iterator
- itc;
+ std::map<TypeNode, std::unordered_set<Node>>::const_iterator itc;
// maps types to the index of its "any term" grammar construction
std::map<TypeNode, std::pair<unsigned, bool>> typeToGAnyTerm;
options::SygusGrammarConsMode sgcm = options::sygusGrammarConsMode();
}
else
{
- std::map<TypeNode, std::unordered_set<Node, NodeHashFunction>>::iterator
- itec = extra_cons.find(types[i]);
+ std::map<TypeNode, std::unordered_set<Node>>::iterator itec =
+ extra_cons.find(types[i]);
if (itec != extra_cons.end())
{
- for (std::unordered_set<Node, NodeHashFunction>::iterator set_it =
- itec->second.begin();
+ for (std::unordered_set<Node>::iterator set_it = itec->second.begin();
set_it != itec->second.end();
++set_it)
{
TypeNode range,
Node bvl,
const std::string& fun,
- std::map<TypeNode, std::unordered_set<Node, NodeHashFunction>>& extra_cons,
- std::map<TypeNode, std::unordered_set<Node, NodeHashFunction>>&
- exclude_cons,
- std::map<TypeNode, std::unordered_set<Node, NodeHashFunction>>&
- include_cons,
- std::unordered_set<Node, NodeHashFunction>& term_irrelevant)
+ std::map<TypeNode, std::unordered_set<Node>>& extra_cons,
+ std::map<TypeNode, std::unordered_set<Node>>& exclude_cons,
+ std::map<TypeNode, std::unordered_set<Node>>& include_cons,
+ std::unordered_set<Node>& term_irrelevant)
{
Trace("sygus-grammar-def") << "*** Make sygus default type " << range << ", make datatypes..." << std::endl;
- for (std::map<TypeNode, std::unordered_set<Node, NodeHashFunction>>::iterator
- it = extra_cons.begin();
+ for (std::map<TypeNode, std::unordered_set<Node>>::iterator it =
+ extra_cons.begin();
it != extra_cons.end();
++it)
{
TypeNode range,
Node bvl,
const std::string& fun,
- std::map<TypeNode, std::unordered_set<Node, NodeHashFunction>>& extra_cons,
- std::map<TypeNode, std::unordered_set<Node, NodeHashFunction>>&
- exclude_cons,
- std::map<TypeNode, std::unordered_set<Node, NodeHashFunction>>&
- include_cons,
- std::unordered_set<Node, NodeHashFunction>& term_irrelevant);
+ std::map<TypeNode, std::unordered_set<Node>>& extra_cons,
+ std::map<TypeNode, std::unordered_set<Node>>& exclude_cons,
+ std::map<TypeNode, std::unordered_set<Node>>& include_cons,
+ std::unordered_set<Node>& term_irrelevant);
/**
* Make the default sygus datatype type corresponding to builtin type range.
Node bvl,
const std::string& fun)
{
- std::map<TypeNode, std::unordered_set<Node, NodeHashFunction>> extra_cons;
- std::map<TypeNode, std::unordered_set<Node, NodeHashFunction>> exclude_cons;
- std::map<TypeNode, std::unordered_set<Node, NodeHashFunction>> include_cons;
- std::unordered_set<Node, NodeHashFunction> term_irrelevant;
+ std::map<TypeNode, std::unordered_set<Node>> extra_cons;
+ std::map<TypeNode, std::unordered_set<Node>> exclude_cons;
+ std::map<TypeNode, std::unordered_set<Node>> include_cons;
+ std::unordered_set<Node> term_irrelevant;
return mkSygusDefaultType(range,
bvl,
fun,
/** is the syntax restricted? */
bool d_is_syntax_restricted;
/** collect terms */
- void collectTerms(
- Node n,
- std::map<TypeNode, std::unordered_set<Node, NodeHashFunction>>& consts);
+ void collectTerms(Node n,
+ std::map<TypeNode, std::unordered_set<Node>>& consts);
//---------------- grammar construction
/** A class for generating sygus datatypes */
class SygusDatatypeGenerator
/** Should we include constructor with operator op? */
bool shouldInclude(Node op) const;
/** The constructors that should be excluded. */
- std::unordered_set<Node, NodeHashFunction> d_exclude_cons;
+ std::unordered_set<Node> d_exclude_cons;
/**
* If this set is non-empty, then only include variables and constructors
* from it.
*/
- std::unordered_set<Node, NodeHashFunction> d_include_cons;
+ std::unordered_set<Node> d_include_cons;
/** The sygus datatype we are generating. */
SygusDatatype d_sdt;
};
TypeNode range,
Node bvl,
const std::string& fun,
- std::map<TypeNode, std::unordered_set<Node, NodeHashFunction>>&
- extra_cons,
- std::map<TypeNode, std::unordered_set<Node, NodeHashFunction>>&
- exclude_cons,
- const std::map<TypeNode, std::unordered_set<Node, NodeHashFunction>>&
- include_cons,
- std::unordered_set<Node, NodeHashFunction>& term_irrelevant,
+ std::map<TypeNode, std::unordered_set<Node>>& extra_cons,
+ std::map<TypeNode, std::unordered_set<Node>>& exclude_cons,
+ const std::map<TypeNode, std::unordered_set<Node>>& include_cons,
+ std::unordered_set<Node>& term_irrelevant,
std::vector<SygusDatatypeGenerator>& sdts,
std::set<TypeNode>& unres);
const Node& conj)
{
Trace("sygus-interpol-debug") << "Collect symbols..." << std::endl;
- std::unordered_set<Node, NodeHashFunction> symSetAxioms;
- std::unordered_set<Node, NodeHashFunction> symSetConj;
+ std::unordered_set<Node> symSetAxioms;
+ std::unordered_set<Node> symSetConj;
for (size_t i = 0, size = axioms.size(); i < size; i++)
{
expr::getSymbols(axioms[i], symSetAxioms);
void SygusInterpol::getIncludeCons(
const std::vector<Node>& axioms,
const Node& conj,
- std::map<TypeNode, std::unordered_set<Node, NodeHashFunction>>& result)
+ std::map<TypeNode, std::unordered_set<Node>>& result)
{
NodeManager* nm = NodeManager::currentNM();
Assert(options::produceInterpols() != options::ProduceInterpols::NONE);
else if (options::produceInterpols() == options::ProduceInterpols::SHARED)
{
// Get operators from axioms
- std::map<TypeNode, std::unordered_set<Node, NodeHashFunction>>
- include_cons_axioms;
+ std::map<TypeNode, std::unordered_set<Node>> include_cons_axioms;
Node tmpAssumptions =
(axioms.size() == 1 ? axioms[0] : nm->mkNode(kind::AND, axioms));
expr::getOperatorsMap(tmpAssumptions, include_cons_axioms);
// Get operators from conj
- std::map<TypeNode, std::unordered_set<Node, NodeHashFunction>>
- include_cons_conj;
+ std::map<TypeNode, std::unordered_set<Node>> include_cons_conj;
expr::getOperatorsMap(conj, include_cons_conj);
// Compute intersection
- for (std::map<TypeNode,
- std::unordered_set<Node, NodeHashFunction>>::iterator it =
+ for (std::map<TypeNode, std::unordered_set<Node>>::iterator it =
include_cons_axioms.begin();
it != include_cons_axioms.end();
it++)
{
TypeNode tn = it->first;
- std::unordered_set<Node, NodeHashFunction> axiomsOps = it->second;
- std::map<TypeNode, std::unordered_set<Node, NodeHashFunction>>::iterator
- concIter = include_cons_conj.find(tn);
+ std::unordered_set<Node> axiomsOps = it->second;
+ std::map<TypeNode, std::unordered_set<Node>>::iterator concIter =
+ include_cons_conj.find(tn);
if (concIter != include_cons_conj.end())
{
- std::unordered_set<Node, NodeHashFunction> conjOps = concIter->second;
+ std::unordered_set<Node> conjOps = concIter->second;
for (const Node& n : axiomsOps)
{
if (conjOps.find(n) != conjOps.end())
{
if (result.find(tn) == result.end())
{
- result[tn] = std::unordered_set<Node, NodeHashFunction>();
+ result[tn] = std::unordered_set<Node>();
}
result[tn].insert(n);
}
else
{
// set default grammar
- std::map<TypeNode, std::unordered_set<Node, NodeHashFunction>> extra_cons;
- std::map<TypeNode, std::unordered_set<Node, NodeHashFunction>> exclude_cons;
- std::map<TypeNode, std::unordered_set<Node, NodeHashFunction>> include_cons;
+ std::map<TypeNode, std::unordered_set<Node>> extra_cons;
+ std::map<TypeNode, std::unordered_set<Node>> exclude_cons;
+ std::map<TypeNode, std::unordered_set<Node>> include_cons;
getIncludeCons(axioms, conj, include_cons);
- std::unordered_set<Node, NodeHashFunction> terms_irrelevant;
+ std::unordered_set<Node> terms_irrelevant;
itpGTypeS = CegGrammarConstructor::mkSygusDefaultType(
NodeManager::currentNM()->booleanType(),
d_ibvlShared,
* @param conj input argument
* @param result the return value
*/
- void getIncludeCons(
- const std::vector<Node>& axioms,
- const Node& conj,
- std::map<TypeNode, std::unordered_set<Node, NodeHashFunction>>& result);
+ void getIncludeCons(const std::vector<Node>& axioms,
+ const Node& conj,
+ std::map<TypeNode, std::unordered_set<Node>>& result);
/**
* Set up the grammar for the interpol-to-synthesis.
/**
* unordered set for shared symbols between axioms and conjecture.
*/
- std::unordered_set<Node, NodeHashFunction> d_symSetShared;
+ std::unordered_set<Node> d_symSetShared;
/**
* free variables created from d_syms.
*/
bool EvalSygusInvarianceTest::invariant(TermDbSygus* tds, Node nvn, Node x)
{
TNode tnvn = nvn;
- std::unordered_map<TNode, TNode, TNodeHashFunction> cache;
+ std::unordered_map<TNode, TNode> cache;
for (const Node& c : d_terms)
{
Node conj_subs = c.substitute(d_var, tnvn, cache);
*/
bool d_is_conjunctive;
/** cache of n -> the simplified form of eval( n ) */
- std::unordered_map<Node, Node, NodeHashFunction> d_visited;
+ std::unordered_map<Node, Node> d_visited;
};
/** EquivSygusInvarianceTest
Assert(f.getType().isFunction());
// initialize the arguments
- std::unordered_map<TypeNode, unsigned, TypeNodeHashFunction>
- type_to_init_deq_id;
+ std::unordered_map<TypeNode, unsigned> type_to_init_deq_id;
std::vector<TypeNode> argTypes = f.getType().getArgTypes();
for (unsigned j = 0; j < argTypes.size(); j++)
{
{
if (n.isVar())
{
- std::unordered_map<Node, unsigned, NodeHashFunction>::iterator ita =
- d_arg_var_num.find(n);
+ std::unordered_map<Node, unsigned>::iterator ita = d_arg_var_num.find(n);
if (ita != d_arg_var_num.end())
{
arg_index = ita->second;
Node SynthConjectureProcessFun::inferDefinition(
Node n,
- std::unordered_map<Node, unsigned, NodeHashFunction>& term_to_arg_carry,
- std::unordered_map<Node,
- std::unordered_set<Node, NodeHashFunction>,
- NodeHashFunction>& free_vars)
+ std::unordered_map<Node, unsigned>& term_to_arg_carry,
+ std::unordered_map<Node, std::unordered_set<Node>>& free_vars)
{
- std::unordered_map<TNode, Node, TNodeHashFunction> visited;
- std::unordered_map<TNode, Node, TNodeHashFunction>::iterator it;
+ std::unordered_map<TNode, Node> visited;
+ std::unordered_map<TNode, Node>::iterator it;
std::stack<TNode> visit;
TNode cur;
visit.push(n);
else
{
// if it is term used by another argument, use it
- std::unordered_map<Node, unsigned, NodeHashFunction>::iterator itt =
+ std::unordered_map<Node, unsigned>::iterator itt =
term_to_arg_carry.find(cur);
if (itt != term_to_arg_carry.end())
{
}
unsigned rid = args[id];
// for merging previously equivalent definitions
- std::unordered_map<Node, unsigned, NodeHashFunction> prev_defs;
+ std::unordered_map<Node, unsigned> prev_defs;
for (unsigned j = 0; j < args.size(); j++)
{
unsigned i = args[j];
else
{
Node t = d_arg_props[i].d_template;
- std::unordered_map<Node, unsigned, NodeHashFunction>::iterator itt =
- prev_defs.find(t);
+ std::unordered_map<Node, unsigned>::iterator itt = prev_defs.find(t);
if (itt != prev_defs.end())
{
// merge previously equivalent definitions
std::vector<Node>& ns,
std::vector<Node>& ks,
Node nf,
- std::unordered_set<Node, NodeHashFunction>& synth_fv,
- std::unordered_map<Node,
- std::unordered_set<Node, NodeHashFunction>,
- NodeHashFunction>& free_vars)
+ std::unordered_set<Node>& synth_fv,
+ std::unordered_map<Node, std::unordered_set<Node>>& free_vars)
{
Assert(ns.size() == ks.size());
Trace("sygus-process-arg-deps") << "Process " << ns.size()
// get the relevant variables
// relevant variables are those that appear in the body of the conjunction
- std::unordered_set<Node, NodeHashFunction> rlv_vars;
+ std::unordered_set<Node> rlv_vars;
Assert(free_vars.find(nf) != free_vars.end());
rlv_vars = free_vars[nf];
// get the single occurrence variables
// single occurrence variables are those that appear in only one position,
// as an argument to the function-to-synthesize.
- std::unordered_map<Node, bool, NodeHashFunction> single_occ_variables;
+ std::unordered_map<Node, bool> single_occ_variables;
for (unsigned index = 0; index < ns.size(); index++)
{
Node n = ns[index];
Node nn = n[i];
if (nn.isVar())
{
- std::unordered_map<Node, bool, NodeHashFunction>::iterator its =
+ std::unordered_map<Node, bool>::iterator its =
single_occ_variables.find(nn);
if (its == single_occ_variables.end())
{
}
else
{
- std::unordered_map<Node,
- std::unordered_set<Node, NodeHashFunction>,
- NodeHashFunction>::iterator itf = free_vars.find(nn);
+ std::unordered_map<Node, std::unordered_set<Node>>::iterator itf =
+ free_vars.find(nn);
Assert(itf != free_vars.end());
- for (std::unordered_set<Node, NodeHashFunction>::iterator itfv =
- itf->second.begin();
+ for (std::unordered_set<Node>::iterator itfv = itf->second.begin();
itfv != itf->second.end();
++itfv)
{
std::unordered_map<unsigned, Node> n_arg_map;
// terms to the argument that is carrying it.
// the arguments in the range of this map must be marked as relevant.
- std::unordered_map<Node, unsigned, NodeHashFunction> term_to_arg_carry;
+ std::unordered_map<Node, unsigned> term_to_arg_carry;
// map of terms to (unprocessed) arguments where it occurs
- std::unordered_map<Node, std::vector<unsigned>, NodeHashFunction>
- term_to_args;
+ std::unordered_map<Node, std::vector<unsigned>> term_to_args;
// initialize
for (unsigned a = 0; a < n.getNumChildren(); a++)
// list of all arguments
std::vector<Node> arg_list;
// now look at the terms for unprocessed arguments
- for (std::unordered_map<Node, std::vector<unsigned>, NodeHashFunction>::
- iterator it = term_to_args.begin();
+ for (std::unordered_map<Node, std::vector<unsigned>>::iterator it =
+ term_to_args.begin();
it != term_to_args.end();
++it)
{
{
infer_def_t = Node::null();
// see if we can infer a definition
- for (std::unordered_map<Node, std::vector<unsigned>, NodeHashFunction>::
- iterator it = term_to_args.begin();
+ for (std::unordered_map<Node, std::vector<unsigned>>::iterator it =
+ term_to_args.begin();
it != term_to_args.end();
++it)
{
while (arg_list_counter < arg_list.size() && !success)
{
Node curr = arg_list[arg_list_counter];
- std::unordered_map<Node, std::vector<unsigned>, NodeHashFunction>::
- iterator it = term_to_args.find(curr);
+ std::unordered_map<Node, std::vector<unsigned>>::iterator it =
+ term_to_args.find(curr);
if (it != term_to_args.end())
{
Trace("sygus-process-arg-deps") << " *** Decide relevant " << curr
// get the base on the conjecture
Node base = q[1];
- std::unordered_set<Node, NodeHashFunction> synth_fv;
+ std::unordered_set<Node> synth_fv;
if (base.getKind() == NOT && base[0].getKind() == FORALL)
{
for (unsigned j = 0, size = base[0][0].getNumChildren(); j < size; j++)
return false;
}
-void SynthConjectureProcess::processConjunct(
- Node n, Node f, std::unordered_set<Node, NodeHashFunction>& synth_fv)
+void SynthConjectureProcess::processConjunct(Node n,
+ Node f,
+ std::unordered_set<Node>& synth_fv)
{
Trace("sygus-process-arg-deps") << "Process conjunct: " << std::endl;
Trace("sygus-process-arg-deps") << " " << n << " for synth fun " << f
// first, flatten the conjunct
// make a copy of free variables since we may add new ones
- std::unordered_set<Node, NodeHashFunction> synth_fv_n = synth_fv;
- std::unordered_map<Node, Node, NodeHashFunction> defs;
+ std::unordered_set<Node> synth_fv_n = synth_fv;
+ std::unordered_map<Node, Node> defs;
Node nf = flatten(n, f, synth_fv_n, defs);
Trace("sygus-process-arg-deps") << "Flattened to: " << std::endl;
Trace("sygus-process-arg-deps") << " " << nf << std::endl;
// get free variables in nf
- std::unordered_map<Node,
- std::unordered_set<Node, NodeHashFunction>,
- NodeHashFunction>
- free_vars;
+ std::unordered_map<Node, std::unordered_set<Node>> free_vars;
getFreeVariables(nf, synth_fv_n, free_vars);
// get free variables in each application
std::vector<Node> ns;
std::vector<Node> ks;
- for (std::unordered_map<Node, Node, NodeHashFunction>::iterator it =
- defs.begin();
+ for (std::unordered_map<Node, Node>::iterator it = defs.begin();
it != defs.end();
++it)
{
Node SynthConjectureProcess::SynthConjectureProcess::flatten(
Node n,
Node f,
- std::unordered_set<Node, NodeHashFunction>& synth_fv,
- std::unordered_map<Node, Node, NodeHashFunction>& defs)
+ std::unordered_set<Node>& synth_fv,
+ std::unordered_map<Node, Node>& defs)
{
- std::unordered_map<Node, Node, NodeHashFunction> visited;
- std::unordered_map<Node, Node, NodeHashFunction>::iterator it;
+ std::unordered_map<Node, Node> visited;
+ std::unordered_map<Node, Node>::iterator it;
std::stack<Node> visit;
Node cur;
visit.push(n);
void SynthConjectureProcess::getFreeVariables(
Node n,
- std::unordered_set<Node, NodeHashFunction>& synth_fv,
- std::unordered_map<Node,
- std::unordered_set<Node, NodeHashFunction>,
- NodeHashFunction>& free_vars)
+ std::unordered_set<Node>& synth_fv,
+ std::unordered_map<Node, std::unordered_set<Node>>& free_vars)
{
// first must compute free variables in each subterm of n,
// as well as contains_synth_fun
- std::unordered_map<Node, bool, NodeHashFunction> visited;
- std::unordered_map<Node, bool, NodeHashFunction>::iterator it;
+ std::unordered_map<Node, bool> visited;
+ std::unordered_map<Node, bool>::iterator it;
std::stack<Node> visit;
Node cur;
visit.push(n);
std::vector<Node>& ns,
std::vector<Node>& ks,
Node nf,
- std::unordered_set<Node, NodeHashFunction>& synth_fv,
- std::unordered_map<Node,
- std::unordered_set<Node, NodeHashFunction>,
- NodeHashFunction>& free_vars);
+ std::unordered_set<Node>& synth_fv,
+ std::unordered_map<Node, std::unordered_set<Node>>& free_vars);
/** is the i^th argument of the function-to-synthesize of this class relevant?
*/
bool isArgRelevant(unsigned i);
/** map from d_arg_vars to the argument #
* they represent.
*/
- std::unordered_map<Node, unsigned, NodeHashFunction> d_arg_var_num;
+ std::unordered_map<Node, unsigned> d_arg_var_num;
/** check match
* This function returns true iff we can infer:
* cn * { x -> n_arg_map[d_arg_var_num[x]] | x in d_arg_vars } = n
*/
Node inferDefinition(
Node n,
- std::unordered_map<Node, unsigned, NodeHashFunction>& term_to_arg_carry,
- std::unordered_map<Node,
- std::unordered_set<Node, NodeHashFunction>,
- NodeHashFunction>& free_vars);
+ std::unordered_map<Node, unsigned>& term_to_arg_carry,
+ std::unordered_map<Node, std::unordered_set<Node>>& free_vars);
/** Assign relevant definition
*
* If def is non-null,
* is the set of (inner) universal variables in the synthesis
* conjecture.
*/
- void processConjunct(Node n,
- Node f,
- std::unordered_set<Node, NodeHashFunction>& synth_fv);
+ void processConjunct(Node n, Node f, std::unordered_set<Node>& synth_fv);
/** flatten
*
* Flattens all applications of f in term n.
*/
Node flatten(Node n,
Node f,
- std::unordered_set<Node, NodeHashFunction>& synth_fv,
- std::unordered_map<Node, Node, NodeHashFunction>& defs);
+ std::unordered_set<Node>& synth_fv,
+ std::unordered_map<Node, Node>& defs);
/** get free variables
* Constructs a map of all free variables that occur in n
* from synth_fv and stores them in the map free_vars.
*/
void getFreeVariables(
Node n,
- std::unordered_set<Node, NodeHashFunction>& synth_fv,
- std::unordered_map<Node,
- std::unordered_set<Node, NodeHashFunction>,
- NodeHashFunction>& free_vars);
+ std::unordered_set<Node>& synth_fv,
+ std::unordered_map<Node, std::unordered_set<Node>>& free_vars);
/** for each synth-fun, information that is specific to this conjecture */
std::map<Node, SynthConjectureProcessFun> d_sf_info;
// the set of unique (up to rewriting) patterns/shapes in the grammar used by
// matching
- std::unordered_map<TypeNode, std::vector<Node>, TypeNodeHashFunction> pool;
+ std::unordered_map<TypeNode, std::vector<Node>> pool;
uint64_t count = 0;
// obligations generated by match. Note that we might have already seen (and
// even solved) those obligations, hence the name "candidate obligations"
- std::unordered_map<Node, Node, NodeHashFunction> candObs;
+ std::unordered_map<Node, Node> candObs;
// the builtin terms corresponding to sygus variables in the grammar are bound
// variables. However, we want the `match` method to treat them as ground
// terms. So, we add redundant substitutions
Node SygusReconstruct::mkGround(Node n) const
{
// get the set of bound variables in n
- std::unordered_set<TNode, TNodeHashFunction> vars;
+ std::unordered_set<TNode> vars;
expr::getVariables(n, vars);
- std::unordered_map<TNode, TNode, TNodeHashFunction> subs;
+ std::unordered_map<TNode, TNode> subs;
// generate a ground value for each one of those variables
for (const TNode& var : vars)
}
void SygusReconstruct::printPool(
- const std::unordered_map<TypeNode, std::vector<Node>, TypeNodeHashFunction>&
- pool) const
+ const std::unordered_map<TypeNode, std::vector<Node>>& pool) const
{
Trace("sygus-rcons") << "\nPool:\n[";
namespace theory {
namespace quantifiers {
-using ObligationSet = std::unordered_set<Node, NodeHashFunction>;
-using TypeObligationSetMap =
- std::unordered_map<TypeNode, ObligationSet, TypeNodeHashFunction>;
+using ObligationSet = std::unordered_set<Node>;
+using TypeObligationSetMap = std::unordered_map<TypeNode, ObligationSet>;
/** SygusReconstruct
*
*
* @param pool a pool of patterns/shapes to print
*/
- void printPool(const std::unordered_map<TypeNode,
- std::vector<Node>,
- TypeNodeHashFunction>& pool) const;
+ void printPool(
+ const std::unordered_map<TypeNode, std::vector<Node>>& pool) const;
/** pointer to the sygus term database */
TermDbSygus* d_tds;
SygusStatistics& d_stats;
/** a map from an obligation to its reconstruction info */
- std::unordered_map<Node, RConsObligationInfo, NodeHashFunction> d_obInfo;
+ std::unordered_map<Node, RConsObligationInfo> d_obInfo;
/** a map from a sygus datatype type to its reconstruction info */
- std::unordered_map<TypeNode, RConsTypeInfo, TypeNodeHashFunction> d_stnInfo;
+ std::unordered_map<TypeNode, RConsTypeInfo> d_stnInfo;
/** a map from an obligation to its sygus solution (if it exists) */
- std::unordered_map<TNode, TNode, TNodeHashFunction> d_sol;
+ std::unordered_map<TNode, TNode> d_sol;
/** a map from a candidate solution to its sub-obligations */
- std::unordered_map<Node, std::vector<Node>, NodeHashFunction> d_subObs;
+ std::unordered_map<Node, std::vector<Node>> d_subObs;
/** a map from a candidate solution to its parent obligation */
- std::unordered_map<Node, Node, NodeHashFunction> d_parentOb;
+ std::unordered_map<Node, Node> d_parentOb;
/** a cache of sygus variables treated as ground terms by matching */
- std::unordered_map<Node, Node, NodeHashFunction> d_sygusVars;
+ std::unordered_map<Node, Node> d_sygusVars;
/** A trie for filtering out redundant terms from the paterns pool */
expr::MatchTrie d_poolTrie;
bool SygusRepairConst::mustRepair(Node n)
{
- std::unordered_set<TNode, TNodeHashFunction> visited;
+ std::unordered_set<TNode> visited;
std::vector<TNode> visit;
TNode cur;
visit.push_back(n);
}
NodeManager* nm = NodeManager::currentNM();
// get the most general candidate skeleton of n
- std::unordered_map<TNode, Node, TNodeHashFunction> visited;
- std::unordered_map<TNode, Node, TNodeHashFunction>::iterator it;
+ std::unordered_map<TNode, Node> visited;
+ std::unordered_map<TNode, Node>::iterator it;
std::vector<TNode> visit;
TNode cur;
visit.push_back(n);
// now, we must replace all terms of the form eval( z_i, t1...tn ) with
// a fresh first-order variable w_i, where z_i is a variable introduced in
// the skeleton inference step (z_i is a variable in sk_vars).
- std::unordered_map<TNode, Node, TNodeHashFunction> visited;
- std::unordered_map<TNode, Node, TNodeHashFunction>::iterator it;
+ std::unordered_map<TNode, Node> visited;
+ std::unordered_map<TNode, Node>::iterator it;
std::vector<TNode> visit;
TNode cur;
visit.push_back(body);
// should have at least one restriction
Assert(restrictLA);
- std::unordered_set<TNode, TNodeHashFunction> visited;
- std::unordered_set<TNode, TNodeHashFunction>::iterator it;
+ std::unordered_set<TNode> visited;
+ std::unordered_set<TNode>::iterator it;
std::vector<TNode> visit;
TNode cur;
visit.push_back(n);
/** reverse map of d_sk_to_fo */
std::map<Node, Node> d_fo_to_sk;
/** a cache of satisfiability queries of the form [***] above we have tried */
- std::unordered_set<Node, NodeHashFunction> d_queries;
+ std::unordered_set<Node> d_queries;
/**
* Register information for sygus type tn, tprocessed stores the set of
* already registered types.
if (ret_dt.isNull() && !retValMod)
{
bool firstTime = true;
- std::unordered_set<Node, NodeHashFunction> intersection;
- std::map<TypeNode, std::unordered_set<Node, NodeHashFunction>>::iterator
- pit;
+ std::unordered_set<Node> intersection;
+ std::map<TypeNode, std::unordered_set<Node>>::iterator pit;
for (size_t i = 0, nvals = x.d_vals.size(); i < nvals; i++)
{
if (x.d_vals[i].getConst<bool>())
* A -> ite( A, B, C ) | ...
* where terms of type B and C can both act as solutions.
*/
- std::map<size_t,
- std::map<TypeNode, std::unordered_set<Node, NodeHashFunction>>>
- d_psolutions;
+ std::map<size_t, std::map<TypeNode, std::unordered_set<Node>>> d_psolutions;
/**
* This flag is set to true if the solution construction was
* non-deterministic with respect to failure/success.
using BoolNodePair = std::pair<bool, Node>;
using BoolNodePairHashFunction =
- PairHashFunction<bool, Node, BoolHashFunction, NodeHashFunction>;
+ PairHashFunction<bool, Node, BoolHashFunction, std::hash<Node>>;
using BoolNodePairMap =
std::unordered_map<BoolNodePair, Node, BoolNodePairHashFunction>;
-using NodePairMap = std::unordered_map<Node, Node, NodeHashFunction>;
+using NodePairMap = std::unordered_map<Node, Node>;
using NodePair = std::pair<Node, Node>;
class SynthConjecture;
/** Whether we are additionally using information gain heuristics */
bool d_useCondPoolIGain;
/* Functions-to-synthesize (a.k.a. candidates) with unification strategies */
- std::unordered_set<Node, NodeHashFunction> d_unif_candidates;
+ std::unordered_set<Node> d_unif_candidates;
/** construct sol */
Node constructSol(Node f,
Node e,
/** gathered evaluation point heads */
std::vector<Node> d_hds;
/** all enumerated model values for conditions */
- std::unordered_set<Node, NodeHashFunction> d_cond_mvs;
+ std::unordered_set<Node> d_cond_mvs;
/** get condition enumerator */
Node getConditionEnumerator() const { return d_cond_enum; }
/** set conditions */
Node d_false;
/** Accumulates solutions built when considering all enumerated condition
* values (which may generate repeated solutions) */
- std::unordered_set<Node, NodeHashFunction> d_sols;
+ std::unordered_set<Node> d_sols;
/**
* Conditional enumerator variables corresponding to the condition values in
* d_conds. These are used for generating separation lemmas during
class SynthEngine : public QuantifiersModule
{
- typedef context::CDHashMap<Node, bool, NodeHashFunction> NodeBoolMap;
+ typedef context::CDHashMap<Node, bool> NodeBoolMap;
public:
SynthEngine(QuantifiersState& qs,
return rewriteNode(res);
}
-Node TermDbSygus::evaluateWithUnfolding(
- Node n, std::unordered_map<Node, Node, NodeHashFunction>& visited)
+Node TermDbSygus::evaluateWithUnfolding(Node n,
+ std::unordered_map<Node, Node>& visited)
{
- std::unordered_map<Node, Node, NodeHashFunction>::iterator it =
- visited.find(n);
+ std::unordered_map<Node, Node>::iterator it = visited.find(n);
if( it==visited.end() ){
Node ret = n;
while (ret.getKind() == DT_SYGUS_EVAL
Node TermDbSygus::evaluateWithUnfolding(Node n)
{
- std::unordered_map<Node, Node, NodeHashFunction> visited;
+ std::unordered_map<Node, Node> visited;
return evaluateWithUnfolding(n, visited);
}
*/
Node evaluateWithUnfolding(Node n);
/** same as above, but with a cache of visited nodes */
- Node evaluateWithUnfolding(
- Node n, std::unordered_map<Node, Node, NodeHashFunction>& visited);
+ Node evaluateWithUnfolding(Node n, std::unordered_map<Node, Node>& visited);
/** is evaluation point?
*
* Returns true if n is of the form eval( x, c1...cn ) for some variable x
*/
void getMaxGroundTerms(TNode n,
TypeNode tn,
- std::unordered_set<Node, NodeHashFunction>& terms,
- std::unordered_set<TNode, TNodeHashFunction>& cache,
+ std::unordered_set<Node>& terms,
+ std::unordered_set<TNode>& cache,
bool skip_quant = false)
{
if (options::sygusInstTermSel() != options::SygusInstTermSelMode::MAX
* term was already found in a subterm.
* @param skip_quant: Do not traverse quantified formulas (skip quantifiers).
*/
-void getMinGroundTerms(
- TNode n,
- TypeNode tn,
- std::unordered_set<Node, NodeHashFunction>& terms,
- std::unordered_map<TNode, std::pair<bool, bool>, TNodeHashFunction>& cache,
- bool skip_quant = false)
+void getMinGroundTerms(TNode n,
+ TypeNode tn,
+ std::unordered_set<Node>& terms,
+ std::unordered_map<TNode, std::pair<bool, bool>>& cache,
+ bool skip_quant = false)
{
if (options::sygusInstTermSel() != options::SygusInstTermSelMode::MIN
&& options::sygusInstTermSel() != options::SygusInstTermSelMode::BOTH)
* @param extra_cons: A map of TypeNode to constants, which are added in
* addition to the default grammar.
*/
-void addSpecialValues(
- const TypeNode& tn,
- std::map<TypeNode, std::unordered_set<Node, NodeHashFunction>>& extra_cons)
+void addSpecialValues(const TypeNode& tn,
+ std::map<TypeNode, std::unordered_set<Node>>& extra_cons)
{
if (tn.isBitVector())
{
Trace("sygus-inst") << "Register " << q << std::endl;
- std::map<TypeNode, std::unordered_set<Node, NodeHashFunction>> extra_cons;
- std::map<TypeNode, std::unordered_set<Node, NodeHashFunction>> exclude_cons;
- std::map<TypeNode, std::unordered_set<Node, NodeHashFunction>> include_cons;
- std::unordered_set<Node, NodeHashFunction> term_irrelevant;
+ std::map<TypeNode, std::unordered_set<Node>> extra_cons;
+ std::map<TypeNode, std::unordered_set<Node>> exclude_cons;
+ std::map<TypeNode, std::unordered_set<Node>> include_cons;
+ std::unordered_set<Node> term_irrelevant;
/* Collect relevant local ground terms for each variable type. */
if (options::sygusInstScope() == options::SygusInstScope::IN
|| options::sygusInstScope() == options::SygusInstScope::BOTH)
{
- std::unordered_map<TypeNode,
- std::unordered_set<Node, NodeHashFunction>,
- TypeNodeHashFunction>
- relevant_terms;
+ std::unordered_map<TypeNode, std::unordered_set<Node>> relevant_terms;
for (const Node& var : q[0])
{
TypeNode tn = var.getType();
/* Collect relevant ground terms for type tn. */
if (relevant_terms.find(tn) == relevant_terms.end())
{
- std::unordered_set<Node, NodeHashFunction> terms;
- std::unordered_set<TNode, TNodeHashFunction> cache_max;
- std::unordered_map<TNode, std::pair<bool, bool>, TNodeHashFunction>
- cache_min;
+ std::unordered_set<Node> terms;
+ std::unordered_set<TNode> cache_max;
+ std::unordered_map<TNode, std::pair<bool, bool>> cache_min;
getMinGroundTerms(q, tn, terms, cache_min);
getMaxGroundTerms(q, tn, terms, cache_max);
/* Collect relevant ground terms for type tn. */
if (d_global_terms.find(tn) == d_global_terms.end())
{
- std::unordered_set<Node, NodeHashFunction> terms;
- std::unordered_set<TNode, TNodeHashFunction> cache_max;
- std::unordered_map<TNode, std::pair<bool, bool>, TNodeHashFunction>
- cache_min;
+ std::unordered_set<Node> terms;
+ std::unordered_set<TNode> cache_max;
+ std::unordered_map<TNode, std::pair<bool, bool>> cache_min;
for (const Node& a : d_notified_assertions)
{
bool sendEvalUnfoldLemmas(const std::vector<Node>& lemmas);
/* Maps quantifiers to a vector of instantiation constants. */
- std::unordered_map<Node, std::vector<Node>, NodeHashFunction>
- d_inst_constants;
+ std::unordered_map<Node, std::vector<Node>> d_inst_constants;
/* Maps quantifiers to a vector of DT_SYGUS_EVAL terms. */
- std::unordered_map<Node, std::vector<Node>, NodeHashFunction> d_var_eval;
+ std::unordered_map<Node, std::vector<Node>> d_var_eval;
/* Maps quantified formulas to registered counterexample literals. */
- std::unordered_map<Node, Node, NodeHashFunction> d_ce_lits;
+ std::unordered_map<Node, Node> d_ce_lits;
/* Decision strategies registered for quantified formulas. */
- std::unordered_map<Node, std::unique_ptr<DecisionStrategy>, NodeHashFunction>
- d_dstrat;
+ std::unordered_map<Node, std::unique_ptr<DecisionStrategy>> d_dstrat;
/* Currently active quantifiers. */
- std::unordered_set<Node, NodeHashFunction> d_active_quant;
+ std::unordered_set<Node> d_active_quant;
/* Currently inactive quantifiers. */
- std::unordered_set<Node, NodeHashFunction> d_inactive_quant;
+ std::unordered_set<Node> d_inactive_quant;
/* Registered counterexample lemma cache. */
- std::unordered_map<Node, Node, NodeHashFunction> d_ce_lemmas;
+ std::unordered_map<Node, Node> d_ce_lemmas;
/* Indicates whether a counterexample lemma was added for a quantified
* formula in the current context. */
- context::CDHashSet<Node, NodeHashFunction> d_ce_lemma_added;
+ context::CDHashSet<Node> d_ce_lemma_added;
/* Set of global ground terms in assertions (outside of quantifiers). */
- context::CDHashMap<TypeNode,
- std::unordered_set<Node, NodeHashFunction>,
- TypeNodeHashFunction>
- d_global_terms;
+ context::CDHashMap<TypeNode, std::unordered_set<Node>> d_global_terms;
/* Assertions sent by ppNotifyAssertions. */
- context::CDHashSet<Node, NodeHashFunction> d_notified_assertions;
+ context::CDHashSet<Node> d_notified_assertions;
};
} // namespace quantifiers
void SygusSampler::computeFreeVariables(Node n, std::vector<Node>& fvs)
{
- std::unordered_set<TNode, TNodeHashFunction> visited;
- std::unordered_set<TNode, TNodeHashFunction>::iterator it;
+ std::unordered_set<TNode> visited;
+ std::unordered_set<TNode>::iterator it;
std::vector<TNode> visit;
TNode cur;
visit.push_back(n);
// compute free variables in n for each type
std::map<unsigned, std::vector<Node> > fvs;
- std::unordered_set<TNode, TNodeHashFunction> visited;
- std::unordered_set<TNode, TNodeHashFunction>::iterator it;
+ std::unordered_set<TNode> visited;
+ std::unordered_set<TNode>::iterator it;
std::vector<TNode> visit;
TNode cur;
visit.push_back(n);
computeFreeVariables(a, fvs);
std::vector<Node> fv_found;
- std::unordered_set<TNode, TNodeHashFunction> visited;
- std::unordered_set<TNode, TNodeHashFunction>::iterator it;
+ std::unordered_set<TNode> visited;
+ std::unordered_set<TNode>::iterator it;
std::vector<TNode> visit;
TNode cur;
visit.push_back(b);
Node TermDb::getOrMakeTypeFreshVariable(TypeNode tn)
{
- std::unordered_map<TypeNode, Node, TypeNodeHashFunction>::iterator it =
- d_type_fv.find(tn);
+ std::unordered_map<TypeNode, Node>::iterator it = d_type_fv.find(tn);
if (it == d_type_fv.end())
{
SkolemManager* sm = NodeManager::currentNM()->getSkolemManager();
* lazily for performance reasons.
*/
class TermDb : public QuantifiersUtil {
- using NodeBoolMap = context::CDHashMap<Node, bool, NodeHashFunction>;
+ using NodeBoolMap = context::CDHashMap<Node, bool>;
using NodeList = context::CDList<Node>;
- using NodeSet = context::CDHashSet<Node, NodeHashFunction>;
- using TypeNodeDbListMap = context::
- CDHashMap<TypeNode, std::shared_ptr<DbList>, TypeNodeHashFunction>;
- using NodeDbListMap =
- context::CDHashMap<Node, std::shared_ptr<DbList>, NodeHashFunction>;
+ using NodeSet = context::CDHashSet<Node>;
+ using TypeNodeDbListMap =
+ context::CDHashMap<TypeNode, std::shared_ptr<DbList>>;
+ using NodeDbListMap = context::CDHashMap<Node, std::shared_ptr<DbList>>;
public:
TermDb(QuantifiersState& qs,
Node d_true;
Node d_false;
/** map from type nodes to a fresh variable we introduced */
- std::unordered_map<TypeNode, Node, TypeNodeHashFunction> d_type_fv;
+ std::unordered_map<TypeNode, Node> d_type_fv;
/** inactive map */
NodeBoolMap d_inactive_map;
/** count of the number of non-redundant ground terms per operator */
{
Trace("term-db-enum") << "Get enumerate term " << tn << " " << index
<< std::endl;
- std::unordered_map<TypeNode, size_t, TypeNodeHashFunction>::iterator it =
- d_typ_enum_map.find(tn);
+ std::unordered_map<TypeNode, size_t>::iterator it = d_typ_enum_map.find(tn);
size_t teIndex;
if (it == d_typ_enum_map.end())
{
*/
QuantifiersBoundInference* d_qbi;
/** ground terms enumerated for types */
- std::unordered_map<TypeNode, std::vector<Node>, TypeNodeHashFunction>
- d_enum_terms;
+ std::unordered_map<TypeNode, std::vector<Node>> d_enum_terms;
/** map from type to the index of its type enumerator in d_typ_enum. */
- std::unordered_map<TypeNode, size_t, TypeNodeHashFunction> d_typ_enum_map;
+ std::unordered_map<TypeNode, size_t> d_typ_enum_map;
/** type enumerators */
std::vector<TypeEnumerator> d_typ_enum;
};
// if we have yet to compute terms on this round
if (dom.d_currTerms.empty())
{
- std::unordered_set<Node, NodeHashFunction> reps;
+ std::unordered_set<Node> reps;
// eliminate modulo equality
for (const Node& t : dom.d_terms)
{
*/
class TermRegistry
{
- using NodeSet = context::CDHashSet<Node, NodeHashFunction>;
+ using NodeSet = context::CDHashSet<Node>;
public:
TermRegistry(QuantifiersState& qs,
//quantified simplify
Node TermUtil::getQuantSimplify( Node n ) {
- std::unordered_set<Node, NodeHashFunction> fvs;
+ std::unordered_set<Node> fvs;
expr::getFreeVariables(n, fvs);
if (fvs.empty())
{
Kind k,
std::vector<Node>& vars)
{
- std::unordered_set<TNode, TNodeHashFunction> visited;
- std::unordered_set<TNode, TNodeHashFunction>::iterator it;
+ std::unordered_set<TNode> visited;
+ std::unordered_set<TNode>::iterator it;
std::vector<TNode> visit;
TNode cur;
visit.push_back(n);
// TODO: organize this more/review this, github issue #1163
class QuantifiersEngine {
friend class ::cvc5::TheoryEngine;
- typedef context::CDHashMap< Node, bool, NodeHashFunction > BoolMap;
- typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
+ typedef context::CDHashMap<Node, bool> BoolMap;
+ typedef context::CDHashSet<Node> NodeSet;
public:
QuantifiersEngine(quantifiers::QuantifiersState& qstate,
d_computed = true;
d_rset.clear();
Trace("rel-manager") << "RelevanceManager::computeRelevance..." << std::endl;
- std::unordered_map<TNode, int, TNodeHashFunction> cache;
+ std::unordered_map<TNode, int> cache;
for (const Node& node: d_input)
{
TNode n = node;
bool RelevanceManager::updateJustifyLastChild(
TNode cur,
std::vector<int>& childrenJustify,
- std::unordered_map<TNode, int, TNodeHashFunction>& cache)
+ std::unordered_map<TNode, int>& cache)
{
// This method is run when we are informed that child index of cur
// has justify status lastChildJustify. We return true if we would like to
return false;
}
-int RelevanceManager::justify(
- TNode n, std::unordered_map<TNode, int, TNodeHashFunction>& cache)
+int RelevanceManager::justify(TNode n, std::unordered_map<TNode, int>& cache)
{
// the vector of values of children
- std::unordered_map<TNode, std::vector<int>, TNodeHashFunction> childJustify;
- std::unordered_map<TNode, int, TNodeHashFunction>::iterator it;
- std::unordered_map<TNode, std::vector<int>, TNodeHashFunction>::iterator itc;
+ std::unordered_map<TNode, std::vector<int>> childJustify;
+ std::unordered_map<TNode, int>::iterator it;
+ std::unordered_map<TNode, std::vector<int>>::iterator itc;
std::vector<TNode> visit;
TNode cur;
visit.push_back(n);
return d_rset.find(lit) != d_rset.end();
}
-const std::unordered_set<TNode, TNodeHashFunction>&
-RelevanceManager::getRelevantAssertions(bool& success)
+const std::unordered_set<TNode>& RelevanceManager::getRelevantAssertions(
+ bool& success)
{
if (!d_computed)
{
*
* The value of this return is only valid if success was not updated to false.
*/
- const std::unordered_set<TNode, TNodeHashFunction>& getRelevantAssertions(
- bool& success);
+ const std::unordered_set<TNode>& getRelevantAssertions(bool& success);
private:
/**
* This method returns 1 if we justified n to be true, -1 means
* justified n to be false, 0 means n could not be justified.
*/
- int justify(TNode n,
- std::unordered_map<TNode, int, TNodeHashFunction>& cache);
+ int justify(TNode n, std::unordered_map<TNode, int>& cache);
/** Is the top symbol of cur a Boolean connective? */
bool isBooleanConnective(TNode cur);
/**
* @return True if we wish to visit the next child. If this is the case, then
* the justify value of the current child is added to childrenJustify.
*/
- bool updateJustifyLastChild(
- TNode cur,
- std::vector<int>& childrenJustify,
- std::unordered_map<TNode, int, TNodeHashFunction>& cache);
+ bool updateJustifyLastChild(TNode cur,
+ std::vector<int>& childrenJustify,
+ std::unordered_map<TNode, int>& cache);
/** The valuation object, used to query current value of theory literals */
Valuation d_val;
/** The input assertions */
NodeList d_input;
/** The current relevant selection. */
- std::unordered_set<TNode, TNodeHashFunction> d_rset;
+ std::unordered_set<TNode> d_rset;
/** Have we computed the relevant selection this round? */
bool d_computed;
/**
namespace {
-bool containsStoreAll(Node n, std::unordered_set<Node, NodeHashFunction>& cache)
+bool containsStoreAll(Node n, std::unordered_set<Node>& cache)
{
if( std::find( cache.begin(), cache.end(), n )==cache.end() ){
cache.insert(n);
void RepSet::add( TypeNode tn, Node n ){
//for now, do not add array constants FIXME
if( tn.isArray() ){
- std::unordered_set<Node, NodeHashFunction> cache;
+ std::unordered_set<Node> cache;
if( containsStoreAll( n, cache ) ){
return;
}
if (d_rewriteStack == nullptr)
{
- d_rewriteStack.reset(new std::unordered_set<Node, NodeHashFunction>());
+ d_rewriteStack.reset(new std::unordered_set<Node>());
}
#endif
/** The proof generator */
std::unique_ptr<TConvProofGenerator> d_tpg;
#ifdef CVC5_ASSERTIONS
- std::unique_ptr<std::unordered_set<Node, NodeHashFunction>> d_rewriteStack =
- nullptr;
+ std::unique_ptr<std::unordered_set<Node>> d_rewriteStack = nullptr;
#endif /* CVC5_ASSERTIONS */
};/* class Rewriter */
class TheorySep : public Theory {
typedef context::CDList<Node> NodeList;
- typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
- typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeNodeMap;
+ typedef context::CDHashSet<Node> NodeSet;
+ typedef context::CDHashMap<Node, Node> NodeNodeMap;
/////////////////////////////////////////////////////////////////////////////
// MISC
*/
class CardinalityExtension
{
- typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
+ typedef context::CDHashSet<Node> NodeSet;
public:
/**
*/
class InferenceManager : public InferenceManagerBuffered
{
- typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
+ typedef context::CDHashSet<Node> NodeSet;
public:
InferenceManager(Theory& t, SolverState& s, ProofNodeManager* pnm);
size_t SingletonOpHashFunction::operator()(const SingletonOp& op) const
{
- return TypeNodeHashFunction()(op.getType());
+ return std::hash<TypeNode>()(op.getType());
}
SingletonOp::SingletonOp(const TypeNode& elementType)
/** map from node pairs and identifiers to skolems */
std::map<Node, std::map<Node, std::map<SkolemId, Node> > > d_skolemCache;
/** the set of all skolems we have generated */
- std::unordered_set<Node, NodeHashFunction> d_allSkolems;
+ std::unordered_set<Node> d_allSkolems;
};
} // namespace sets
*/
class SolverState : public TheoryState
{
- typedef context::CDHashMap<Node, size_t, NodeHashFunction> NodeIntMap;
+ typedef context::CDHashMap<Node, size_t> NodeIntMap;
public:
SolverState(context::Context* c,
*/
class TermRegistry
{
- typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeMap;
+ typedef context::CDHashMap<Node, Node> NodeMap;
public:
TermRegistry(SolverState& state,
class TheorySets;
class TheorySetsPrivate {
- typedef context::CDHashMap< Node, bool, NodeHashFunction> NodeBoolMap;
- typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
+ typedef context::CDHashMap<Node, bool> NodeBoolMap;
+ typedef context::CDHashSet<Node> NodeSet;
public:
void eqNotifyNewClass(TNode t);
typedef std::map< Node, std::vector< Node > >::iterator MEM_IT;
typedef std::map< kind::Kind_t, std::vector< Node > >::iterator KIND_TERM_IT;
-typedef std::map< Node, std::unordered_set< Node, NodeHashFunction > >::iterator TC_GRAPH_IT;
+typedef std::map<Node, std::unordered_set<Node> >::iterator TC_GRAPH_IT;
typedef std::map< Node, std::map< kind::Kind_t, std::vector< Node > > >::iterator TERM_IT;
-typedef std::map< Node, std::map< Node, std::unordered_set< Node, NodeHashFunction > > >::iterator TC_IT;
+typedef std::map<Node, std::map<Node, std::unordered_set<Node> > >::iterator
+ TC_IT;
TheorySetsRels::TheorySetsRels(SolverState& s,
InferenceManager& im,
NodeManager* nm = NodeManager::currentNM();
Node join_image_rel = join_image_term[0];
- std::unordered_set< Node, NodeHashFunction > hasChecked;
+ std::unordered_set<Node> hasChecked;
Node join_image_rel_rep = getRepresentative( join_image_rel );
std::vector< Node >::iterator mem_rep_it = (*rel_mem_it).second.begin();
MEM_IT rel_mem_exp_it = d_rReps_memberReps_exp_cache.find( join_image_rel_rep );
if( tc_graph_it != (tc_it->second).end() ) {
(tc_graph_it->second).insert( mem_rep_snd );
} else {
- std::unordered_set< Node, NodeHashFunction > sets;
+ std::unordered_set<Node> sets;
sets.insert( mem_rep_snd );
(tc_it->second)[mem_rep_fst] = sets;
}
} else {
std::map< Node, Node > exp_map;
- std::unordered_set< Node, NodeHashFunction > sets;
- std::map< Node, std::unordered_set<Node, NodeHashFunction> > element_map;
+ std::unordered_set<Node> sets;
+ std::map<Node, std::unordered_set<Node> > element_map;
sets.insert( mem_rep_snd );
element_map[mem_rep_fst] = sets;
d_tcr_tcGraph[tc_rel] = element_map;
TC_IT tc_it = d_rRep_tcGraph.find( getRepresentative(tc_rel[0]) );
if( tc_it != d_rRep_tcGraph.end() ) {
bool isReachable = false;
- std::unordered_set<Node, NodeHashFunction> seen;
+ std::unordered_set<Node> seen;
isTCReachable( getRepresentative( RelsUtils::nthElementOfTuple(mem_rep, 0) ),
getRepresentative( RelsUtils::nthElementOfTuple(mem_rep, 1) ), seen, tc_it->second, isReachable );
return isReachable;
return false;
}
- void TheorySetsRels::isTCReachable( Node start, Node dest, std::unordered_set<Node, NodeHashFunction>& hasSeen,
- std::map< Node, std::unordered_set< Node, NodeHashFunction > >& tc_graph, bool& isReachable ) {
+ void TheorySetsRels::isTCReachable(
+ Node start,
+ Node dest,
+ std::unordered_set<Node>& hasSeen,
+ std::map<Node, std::unordered_set<Node> >& tc_graph,
+ bool& isReachable)
+ {
if(hasSeen.find(start) == hasSeen.end()) {
hasSeen.insert(start);
}
isReachable = true;
return;
} else {
- std::unordered_set< Node, NodeHashFunction >::iterator set_it = pair_set_it->second.begin();
+ std::unordered_set<Node>::iterator set_it = pair_set_it->second.begin();
while( set_it != pair_set_it->second.end() ) {
// need to check if *set_it has been looked already
void TheorySetsRels::buildTCGraphForRel( Node tc_rel ) {
std::map< Node, Node > rel_tc_graph_exps;
- std::map< Node, std::unordered_set<Node, NodeHashFunction> > rel_tc_graph;
+ std::map<Node, std::unordered_set<Node> > rel_tc_graph;
Node rel_rep = getRepresentative( tc_rel[0] );
Node tc_rel_rep = getRepresentative( tc_rel );
Node fst_element_rep = getRepresentative( RelsUtils::nthElementOfTuple( members[i], 0 ));
Node snd_element_rep = getRepresentative( RelsUtils::nthElementOfTuple( members[i], 1 ));
Node tuple_rep = RelsUtils::constructPair( rel_rep, fst_element_rep, snd_element_rep );
- std::map< Node, std::unordered_set<Node, NodeHashFunction> >::iterator rel_tc_graph_it = rel_tc_graph.find( fst_element_rep );
+ std::map<Node, std::unordered_set<Node> >::iterator rel_tc_graph_it =
+ rel_tc_graph.find(fst_element_rep);
if( rel_tc_graph_it == rel_tc_graph.end() ) {
- std::unordered_set< Node, NodeHashFunction > snd_elements;
+ std::unordered_set<Node> snd_elements;
snd_elements.insert( snd_element_rep );
rel_tc_graph[fst_element_rep] = snd_elements;
rel_tc_graph_exps[tuple_rep] = exps[i];
}
}
- void TheorySetsRels::doTCInference( std::map< Node, std::unordered_set<Node, NodeHashFunction> > rel_tc_graph, std::map< Node, Node > rel_tc_graph_exps, Node tc_rel ) {
+ void TheorySetsRels::doTCInference(
+ std::map<Node, std::unordered_set<Node> > rel_tc_graph,
+ std::map<Node, Node> rel_tc_graph_exps,
+ Node tc_rel)
+ {
Trace("rels-debug") << "[Theory::Rels] ****** doTCInference !" << std::endl;
for (TC_GRAPH_IT tc_graph_it = rel_tc_graph.begin();
tc_graph_it != rel_tc_graph.end();
++tc_graph_it)
{
- for (std::unordered_set<Node, NodeHashFunction>::iterator
- snd_elements_it = tc_graph_it->second.begin();
+ for (std::unordered_set<Node>::iterator snd_elements_it =
+ tc_graph_it->second.begin();
snd_elements_it != tc_graph_it->second.end();
++snd_elements_it)
{
std::vector< Node > reasons;
- std::unordered_set<Node, NodeHashFunction> seen;
+ std::unordered_set<Node> seen;
Node tuple = RelsUtils::constructPair( tc_rel, getRepresentative( tc_graph_it->first ), getRepresentative( *snd_elements_it) );
Assert(rel_tc_graph_exps.find(tuple) != rel_tc_graph_exps.end());
Node exp = rel_tc_graph_exps.find( tuple )->second;
Trace("rels-debug") << "[Theory::Rels] ****** Done with doTCInference !" << std::endl;
}
- void TheorySetsRels::doTCInference(Node tc_rel, std::vector< Node > reasons, std::map< Node, std::unordered_set< Node, NodeHashFunction > >& tc_graph,
- std::map< Node, Node >& rel_tc_graph_exps, Node start_node_rep, Node cur_node_rep, std::unordered_set< Node, NodeHashFunction >& seen ) {
+ void TheorySetsRels::doTCInference(
+ Node tc_rel,
+ std::vector<Node> reasons,
+ std::map<Node, std::unordered_set<Node> >& tc_graph,
+ std::map<Node, Node>& rel_tc_graph_exps,
+ Node start_node_rep,
+ Node cur_node_rep,
+ std::unordered_set<Node>& seen)
+ {
NodeManager* nm = NodeManager::currentNM();
Node tc_mem = RelsUtils::constructPair( tc_rel, RelsUtils::nthElementOfTuple((reasons.front())[0], 0), RelsUtils::nthElementOfTuple((reasons.back())[0], 1) );
std::vector< Node > all_reasons( reasons );
seen.insert( cur_node_rep );
TC_GRAPH_IT cur_set = tc_graph.find( cur_node_rep );
if( cur_set != tc_graph.end() ) {
- for (std::unordered_set<Node, NodeHashFunction>::iterator set_it =
- cur_set->second.begin();
+ for (std::unordered_set<Node>::iterator set_it = cur_set->second.begin();
set_it != cur_set->second.end();
++set_it)
{
*/
class TheorySetsRels {
typedef context::CDList<Node> NodeList;
- typedef context::CDHashSet< Node, NodeHashFunction > NodeSet;
- typedef context::CDHashMap< Node, Node, NodeHashFunction > NodeMap;
+ typedef context::CDHashSet<Node> NodeSet;
+ typedef context::CDHashMap<Node, Node> NodeMap;
-public:
- TheorySetsRels(SolverState& s,
- InferenceManager& im,
- SkolemCache& skc,
- TermRegistry& treg);
-
- ~TheorySetsRels();
- /**
- * Invoke the check method with effort level e. At a high level, this class
- * will make calls to TheorySetsPrivate::processInference to assert facts,
- * lemmas, and conflicts. If this class makes no such call, then the current
- * set of assertions is satisfiable with respect to relations.
- */
- void check(Theory::Effort e);
- /** Is kind k a kind that belongs to the relation theory? */
- static bool isRelationKind(Kind k);
-
-private:
+ public:
+ TheorySetsRels(SolverState& s,
+ InferenceManager& im,
+ SkolemCache& skc,
+ TermRegistry& treg);
+
+ ~TheorySetsRels();
+ /**
+ * Invoke the check method with effort level e. At a high level, this class
+ * will make calls to TheorySetsPrivate::processInference to assert facts,
+ * lemmas, and conflicts. If this class makes no such call, then the current
+ * set of assertions is satisfiable with respect to relations.
+ */
+ void check(Theory::Effort e);
+ /** Is kind k a kind that belongs to the relation theory? */
+ static bool isRelationKind(Kind k);
+
+ private:
/** True and false constant nodes */
Node d_trueNode;
Node d_falseNode;
std::vector<Node> d_pending;
NodeSet d_shared_terms;
-
- std::unordered_set< Node, NodeHashFunction > d_rel_nodes;
+ std::unordered_set<Node> d_rel_nodes;
std::map< Node, std::vector<Node> > d_tuple_reps;
std::map< Node, TupleTrie > d_membership_trie;
/** Symbolic tuple variables that has been reduced to concrete ones */
- std::unordered_set< Node, NodeHashFunction > d_symbolic_tuples;
+ std::unordered_set<Node> d_symbolic_tuples;
/** Mapping between relation and its member representatives */
std::map< Node, std::vector< Node > > d_rReps_memberReps_cache;
std::map< Node, std::map<kind::Kind_t, std::vector<Node> > > d_terms_cache;
/** Mapping between transitive closure relation TC(r) and its TC graph constructed based on the members of r*/
- std::map< Node, std::map< Node, std::unordered_set<Node, NodeHashFunction> > > d_rRep_tcGraph;
- std::map< Node, std::map< Node, std::unordered_set<Node, NodeHashFunction> > > d_tcr_tcGraph;
+ std::map<Node, std::map<Node, std::unordered_set<Node> > > d_rRep_tcGraph;
+ std::map<Node, std::map<Node, std::unordered_set<Node> > > d_tcr_tcGraph;
std::map< Node, std::map< Node, Node > > d_tcr_tcGraph_exps;
private:
void applyTCRule( Node mem, Node rel, Node rel_rep, Node exp);
void buildTCGraphForRel( Node tc_rel );
void doTCInference();
- void doTCInference( std::map< Node, std::unordered_set<Node, NodeHashFunction> > rel_tc_graph, std::map< Node, Node > rel_tc_graph_exps, Node tc_rel );
- void doTCInference(Node tc_rel, std::vector< Node > reasons, std::map< Node, std::unordered_set< Node, NodeHashFunction > >& tc_graph,
- std::map< Node, Node >& rel_tc_graph_exps, Node start_node_rep, Node cur_node_rep, std::unordered_set< Node, NodeHashFunction >& seen );
+ void doTCInference(std::map<Node, std::unordered_set<Node> > rel_tc_graph,
+ std::map<Node, Node> rel_tc_graph_exps,
+ Node tc_rel);
+ void doTCInference(Node tc_rel,
+ std::vector<Node> reasons,
+ std::map<Node, std::unordered_set<Node> >& tc_graph,
+ std::map<Node, Node>& rel_tc_graph_exps,
+ Node start_node_rep,
+ Node cur_node_rep,
+ std::unordered_set<Node>& seen);
void composeMembersForRels( Node );
void computeMembersForBinOpRel( Node );
void computeMembersForJoinImageTerm( Node );
bool isTCReachable( Node mem_rep, Node tc_rel );
- void isTCReachable( Node start, Node dest, std::unordered_set<Node, NodeHashFunction>& hasSeen,
- std::map< Node, std::unordered_set< Node, NodeHashFunction > >& tc_graph, bool& isReachable );
+ void isTCReachable(Node start,
+ Node dest,
+ std::unordered_set<Node>& hasSeen,
+ std::map<Node, std::unordered_set<Node> >& tc_graph,
+ bool& isReachable);
/** Helper functions */
bool hasTerm( Node a );
IntStat d_statSharedTerms;
// Needs to be a map from Nodes as after a backtrack they might not exist
- typedef std::unordered_map<Node, shared_terms_list, TNodeHashFunction> SharedTermsMap;
+ typedef std::unordered_map<Node, shared_terms_list> SharedTermsMap;
/** A map from atoms to a list of shared terms */
SharedTermsMap d_atomsToTerms;
SharedTermsTheoriesMap d_termsToTheories;
/** Map from term to theories that have already been notified about the shared term */
- typedef context::CDHashMap<TNode, theory::TheoryIdSet, TNodeHashFunction>
- AlreadyNotifiedMap;
+ typedef context::CDHashMap<TNode, theory::TheoryIdSet> AlreadyNotifiedMap;
AlreadyNotifiedMap d_alreadyNotifiedMap;
/** The registered equalities for propagation */
- typedef context::CDHashSet<Node, NodeHashFunction> RegisteredEqualitiesSet;
+ typedef context::CDHashSet<Node> RegisteredEqualitiesSet;
RegisteredEqualitiesSet d_registeredEqualities;
private:
// c.isNull() means c = 1
bool isOverApprox = !c.isNull() && c.getConst<Rational>().sgn() == -1;
std::vector<Node>& approx = mApprox[v];
- std::unordered_set<Node, NodeHashFunction> visited;
+ std::unordered_set<Node> visited;
std::vector<Node> toProcess;
toProcess.push_back(v);
do
<< ", strict=" << strict << std::endl;
// Find candidates variables to compute substitutions for
- std::unordered_set<Node, NodeHashFunction> candVars;
+ std::unordered_set<Node> candVars;
std::vector<Node> toVisit = {assumption};
while (!toVisit.empty())
{
*/
class BaseSolver
{
- using NodeSet = context::CDHashSet<Node, NodeHashFunction>;
+ using NodeSet = context::CDHashSet<Node>;
public:
BaseSolver(SolverState& s, InferenceManager& im);
// the possible inferences
std::vector<CoreInferInfo> pinfer;
// compute normal forms that are effectively unique
- std::unordered_map<Node, size_t, NodeHashFunction> nfCache;
+ std::unordered_map<Node, size_t> nfCache;
std::vector<size_t> nfIndices;
bool hasConstIndex = false;
for (size_t i = 0, nnforms = normal_forms.size(); i < nnforms; i++)
class CoreSolver
{
friend class InferenceManager;
- using NodeIntMap = context::CDHashMap<Node, int, NodeHashFunction>;
+ using NodeIntMap = context::CDHashMap<Node, int>;
public:
CoreSolver(SolverState& s,
bool has_nreduce = false;
std::vector<Node> terms = d_extt.getActive();
// the set of terms we have done extf inferences for
- std::unordered_set<Node, NodeHashFunction> inferProcessed;
+ std::unordered_set<Node> inferProcessed;
for (const Node& n : terms)
{
// Setup information about n, including if it is equal to a constant.
*/
class ExtfSolver
{
- typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
+ typedef context::CDHashSet<Node> NodeSet;
public:
ExtfSolver(SolverState& s,
*/
class InferProofCons : public ProofGenerator
{
- typedef context::CDHashMap<Node, std::shared_ptr<InferInfo>, NodeHashFunction>
- NodeInferInfoMap;
+ typedef context::CDHashMap<Node, std::shared_ptr<InferInfo>> NodeInferInfoMap;
public:
InferProofCons(context::Context* c,
*/
class InferenceManager : public InferenceManagerBuffered
{
- typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
- typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeNodeMap;
+ typedef context::CDHashSet<Node> NodeSet;
+ typedef context::CDHashMap<Node, Node> NodeNodeMap;
friend class InferInfo;
public:
RegExpConstType RegExpOpr::getRegExpConstType(Node r)
{
Assert(r.getType().isRegExp());
- std::unordered_map<Node, RegExpConstType, NodeHashFunction>::iterator it;
+ std::unordered_map<Node, RegExpConstType>::iterator it;
std::vector<TNode> visit;
TNode cur;
visit.push_back(r);
Node RegExpOpr::removeIntersection(Node r) {
Assert(checkConstRegExp(r));
NodeManager* nm = NodeManager::currentNM();
- std::unordered_map<TNode, Node, TNodeHashFunction> visited;
- std::unordered_map<TNode, Node, TNodeHashFunction>::iterator it;
+ std::unordered_map<TNode, Node> visited;
+ std::unordered_map<TNode, Node>::iterator it;
std::vector<TNode> visit;
TNode cur;
visit.push_back(r);
std::map<PairNodeStr, Node> d_dv_cache;
std::map<PairNodeStr, std::pair<Node, int> > d_deriv_cache;
/** cache mapping regular expressions to whether they contain constants */
- std::unordered_map<Node, RegExpConstType, NodeHashFunction> d_constCache;
+ std::unordered_map<Node, RegExpConstType> d_constCache;
std::map<Node, std::pair<std::set<unsigned>, std::set<Node> > > d_fset_cache;
std::map<PairNodes, Node> d_inter_cache;
std::map<Node, std::vector<PairNodes> > d_split_cache;
NodeManager* nm = NodeManager::currentNM();
// representatives of strings that are the LHS of positive memberships that
// we unfolded
- std::unordered_set<Node, NodeHashFunction> repUnfold;
+ std::unordered_set<Node> repUnfold;
// check positive (e=0), then negative (e=1) memberships
for (unsigned e = 0; e < 2; e++)
{
bool RegExpSolver::checkEqcInclusion(std::vector<Node>& mems)
{
- std::unordered_set<Node, NodeHashFunction> remove;
+ std::unordered_set<Node> remove;
for (const Node& m1 : mems)
{
class RegExpSolver
{
typedef context::CDList<Node> NodeList;
- typedef context::CDHashMap<Node, bool, NodeHashFunction> NodeBoolMap;
- typedef context::CDHashMap<Node, int, NodeHashFunction> NodeIntMap;
- typedef context::CDHashMap<Node, unsigned, NodeHashFunction> NodeUIntMap;
- typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeNodeMap;
- typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
+ typedef context::CDHashMap<Node, bool> NodeBoolMap;
+ typedef context::CDHashMap<Node, int> NodeIntMap;
+ typedef context::CDHashMap<Node, unsigned> NodeUIntMap;
+ typedef context::CDHashMap<Node, Node> NodeNodeMap;
+ typedef context::CDHashSet<Node> NodeSet;
public:
RegExpSolver(SolverState& s,
/** map from node pairs and identifiers to skolems */
std::map<Node, std::map<Node, std::map<SkolemId, Node> > > d_skolemCache;
/** the set of all skolems we have generated */
- std::unordered_set<Node, NodeHashFunction> d_allSkolems;
+ std::unordered_set<Node> d_allSkolems;
};
} // namespace strings
*/
class StringsFmf
{
- typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
+ typedef context::CDHashSet<Node> NodeSet;
public:
StringsFmf(context::Context* c,
return d_functionsTerms;
}
-const context::CDHashSet<Node, NodeHashFunction>& TermRegistry::getInputVars()
- const
+const context::CDHashSet<Node>& TermRegistry::getInputVars() const
{
return d_inputVars;
}
*/
class TermRegistry
{
- typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
- typedef context::CDHashSet<TypeNode, TypeNodeHashFunction> TypeNodeSet;
- typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeNodeMap;
+ typedef context::CDHashSet<Node> NodeSet;
+ typedef context::CDHashSet<TypeNode, std::hash<TypeNode>> TypeNodeSet;
+ typedef context::CDHashMap<Node, Node> NodeNodeMap;
public:
TermRegistry(SolverState& s,
* Get the "input variables", corresponding to the set of leaf nodes of
* string-like type that have been preregistered as terms to this object.
*/
- const context::CDHashSet<Node, NodeHashFunction>& getInputVars() const;
+ const context::CDHashSet<Node>& getInputVars() const;
/** Returns true if any str.code terms have been preregistered */
bool hasStringCode() const;
//---------------------------- end queries
Trace("strings-debug-model") << d_esolver.debugPrintModel() << std::endl;
}
Trace("strings-model") << "TheoryStrings::collectModelValues" << std::endl;
- std::map<TypeNode, std::unordered_set<Node, NodeHashFunction> > repSet;
+ std::map<TypeNode, std::unordered_set<Node> > repSet;
// Generate model
// get the relevant string equivalence classes
for (const Node& s : termSet)
repSet[tn].insert(r);
}
}
- for (const std::pair<const TypeNode,
- std::unordered_set<Node, NodeHashFunction> >& rst :
- repSet)
+ for (const std::pair<const TypeNode, std::unordered_set<Node> >& rst : repSet)
{
// get partition of strings of equal lengths, per type
std::map<TypeNode, std::vector<std::vector<Node> > > colT;
return true;
}
-bool TheoryStrings::collectModelInfoType(
- TypeNode tn,
- const std::unordered_set<Node, NodeHashFunction>& repSet,
- std::vector<std::vector<Node> >& col,
- std::vector<Node>& lts,
- TheoryModel* m)
+bool TheoryStrings::collectModelInfoType(TypeNode tn,
+ const std::unordered_set<Node>& repSet,
+ std::vector<std::vector<Node> >& col,
+ std::vector<Node>& lts,
+ TheoryModel* m)
{
NodeManager* nm = NodeManager::currentNM();
std::map< Node, Node > processed;
*/
class TheoryStrings : public Theory {
friend class InferenceManager;
- typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
- typedef context::CDHashSet<TypeNode, TypeNodeHashFunction> TypeNodeSet;
+ typedef context::CDHashSet<Node> NodeSet;
+ typedef context::CDHashSet<TypeNode, std::hash<TypeNode>> TypeNodeSet;
+
public:
TheoryStrings(context::Context* c,
context::UserContext* u,
*
* Returns false if a conflict is discovered while doing this assignment.
*/
- bool collectModelInfoType(
- TypeNode tn,
- const std::unordered_set<Node, NodeHashFunction>& repSet,
- std::vector<std::vector<Node> >& col,
- std::vector<Node>& lts,
- TheoryModel* m);
+ bool collectModelInfoType(TypeNode tn,
+ const std::unordered_set<Node>& repSet,
+ std::vector<std::vector<Node>>& col,
+ std::vector<Node>& lts,
+ TheoryModel* m);
/** assert pending fact
*
return;
}
// otherwise, traverse
- std::unordered_set<TNode, TNodeHashFunction> visited;
- std::unordered_set<TNode, TNodeHashFunction>::iterator it;
+ std::unordered_set<TNode> visited;
+ std::unordered_set<TNode>::iterator it;
std::vector<TNode> visit;
TNode cur;
visit.push_back(n);
std::vector<Node> tconj;
getConjuncts(t, tconj);
// map from conjuncts to their free symbols
- std::map<Node, std::unordered_set<Node, NodeHashFunction> > tcFv;
+ std::map<Node, std::unordered_set<Node> > tcFv;
- std::unordered_set<Node, NodeHashFunction> reqSet;
+ std::unordered_set<Node> reqSet;
std::vector<Node> reqSubs;
std::map<Node, unsigned> reqVarToIndex;
for (const Node& v : reqVars)
for (const Node& tc : tconj)
{
// ensure we've computed its free symbols
- std::map<Node, std::unordered_set<Node, NodeHashFunction> >::iterator
- itf = tcFv.find(tc);
+ std::map<Node, std::unordered_set<Node> >::iterator itf = tcFv.find(tc);
if (itf == tcFv.end())
{
expr::getSymbols(tc, tcFv[tc]);
Trace("subs-min") << "--- Compute values for subterms..." << std::endl;
// the value of each subterm in n under the substitution
- std::unordered_map<TNode, Node, TNodeHashFunction> value;
- std::unordered_map<TNode, Node, TNodeHashFunction>::iterator it;
+ std::unordered_map<TNode, Node> value;
+ std::unordered_map<TNode, Node>::iterator it;
std::vector<TNode> visit;
TNode cur;
visit.push_back(n);
}
Trace("subs-min") << "--- Compute relevant variables..." << std::endl;
- std::unordered_set<Node, NodeHashFunction> rlvFv;
+ std::unordered_set<Node> rlvFv;
// only variables that occur in assertions are relevant
visit.push_back(n);
- std::unordered_set<TNode, TNodeHashFunction> visited;
- std::unordered_set<TNode, TNodeHashFunction>::iterator itv;
+ std::unordered_set<TNode> visited;
+ std::unordered_set<TNode>::iterator itv;
do
{
cur = visit.back();
*
* This map is context-dependent.
*/
-class SubstitutionMap {
-
-public:
-
- typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeMap;
+class SubstitutionMap
+{
+ public:
+ typedef context::CDHashMap<Node, Node> NodeMap;
typedef NodeMap::iterator iterator;
typedef NodeMap::const_iterator const_iterator;
-private:
-
- typedef std::unordered_map<Node, Node, NodeHashFunction> NodeCache;
+ private:
+ typedef std::unordered_map<Node, Node> NodeCache;
/** A dummy context used by this class if none is provided */
context::Context d_context;
Node internalSubstitute(TNode t, NodeCache& cache);
/** Helper class to invalidate cache on user pop */
- class CacheInvalidator : public context::ContextNotifyObj {
+ class CacheInvalidator : public context::ContextNotifyObj
+ {
bool& d_cacheInvalidated;
- protected:
- void contextNotifyPop() override { d_cacheInvalidated = true; }
- public:
- CacheInvalidator(context::Context* context, bool& cacheInvalidated) :
- context::ContextNotifyObj(context),
- d_cacheInvalidated(cacheInvalidated) {
+ protected:
+ void contextNotifyPop() override { d_cacheInvalidated = true; }
+
+ public:
+ CacheInvalidator(context::Context* context, bool& cacheInvalidated)
+ : context::ContextNotifyObj(context),
+ d_cacheInvalidated(cacheInvalidated)
+ {
}
- };/* class SubstitutionMap::CacheInvalidator */
+ }; /* class SubstitutionMap::CacheInvalidator */
/**
* This object is notified on user pop and marks the SubstitutionMap's
/**
* Returns true iff x is in the substitution map
*/
- bool hasSubstitution(TNode x) const {
+ bool hasSubstitution(TNode x) const
+ {
return d_substitutions.find(x) != d_substitutions.end();
}
* is mainly intended for constructing assertions about what has
* already been put in the map.
*/
- TNode getSubstitution(TNode x) const {
- AssertArgument(hasSubstitution(x), x, "element not in this substitution map");
+ TNode getSubstitution(TNode x) const
+ {
+ AssertArgument(
+ hasSubstitution(x), x, "element not in this substitution map");
return (*d_substitutions.find(x)).second;
}
/**
* Apply the substitutions to the node.
*/
- Node apply(TNode t, bool doRewrite = false) const {
+ Node apply(TNode t, bool doRewrite = false) const
+ {
return const_cast<SubstitutionMap*>(this)->apply(t, doRewrite);
}
- iterator begin() {
- return d_substitutions.begin();
- }
+ iterator begin() { return d_substitutions.begin(); }
- iterator end() {
- return d_substitutions.end();
- }
+ iterator end() { return d_substitutions.end(); }
- const_iterator begin() const {
- return d_substitutions.begin();
- }
+ const_iterator begin() const { return d_substitutions.begin(); }
- const_iterator end() const {
- return d_substitutions.end();
- }
+ const_iterator end() const { return d_substitutions.end(); }
- bool empty() const {
- return d_substitutions.empty();
- }
+ bool empty() const { return d_substitutions.empty(); }
/**
* Print to the output stream
void print(std::ostream& out) const;
void debugPrint() const;
-};/* class SubstitutionMap */
+}; /* class SubstitutionMap */
inline std::ostream& operator << (std::ostream& out, const SubstitutionMap& subst) {
subst.print(out);
/** The engine */
TheoryEngine* d_engine;
- typedef context::CDHashMap<TNode, theory::TheoryIdSet, TNodeHashFunction>
- TNodeToTheorySetMap;
+ typedef context::CDHashMap<TNode, theory::TheoryIdSet> TNodeToTheorySetMap;
/**
* Map from terms to the theories that have already had this term pre-registered.
* been visited already, we need to visit it again, since we need to associate it with both atoms.
*/
class SharedTermsVisitor {
- using TNodeVisitedMap =
- std::unordered_map<TNode, theory::TheoryIdSet, TNodeHashFunction>;
- using TNodeToTheorySetMap =
- context::CDHashMap<TNode, theory::TheoryIdSet, TNodeHashFunction>;
+ using TNodeVisitedMap = std::unordered_map<TNode, theory::TheoryIdSet>;
+ using TNodeToTheorySetMap = context::CDHashMap<TNode, theory::TheoryIdSet>;
/**
* String representation of the visited map, for debugging purposes.
*/
return tm->isLegalElimination(x, val);
}
-std::unordered_set<TNode, TNodeHashFunction> Theory::currentlySharedTerms() const{
- std::unordered_set<TNode, TNodeHashFunction> currentlyShared;
+std::unordered_set<TNode> Theory::currentlySharedTerms() const
+{
+ std::unordered_set<TNode> currentlyShared;
for (shared_terms_iterator i = shared_terms_begin(),
i_end = shared_terms_end(); i != i_end; ++i) {
currentlyShared.insert (*i);
* This is a utility function for constructing a copy of the currently shared terms
* in a queriable form. As this is
*/
- std::unordered_set<TNode, TNodeHashFunction> currentlySharedTerms() const;
+ std::unordered_set<TNode> currentlySharedTerms() const;
/**
* This allows the theory to be queried for whether a literal, lit, is
return d_sharedSolver->getEqualityStatus(a, b);
}
-const std::unordered_set<TNode, TNodeHashFunction>&
-TheoryEngine::getRelevantAssertions(bool& success)
+const std::unordered_set<TNode>& TheoryEngine::getRelevantAssertions(
+ bool& success)
{
// if we are not in SAT mode, or there is no relevance manager, we fail
if (!d_inSatMode || d_relManager == nullptr)
struct AtomsCollect {
std::vector<TNode> d_atoms;
- std::unordered_set<TNode, TNodeHashFunction> d_visited;
-
-public:
+ std::unordered_set<TNode> d_visited;
+ public:
typedef void return_type;
bool alreadyVisited(TNode current, TNode parent) {
// vector of trust nodes to explain at the end
std::vector<std::pair<TheoryId, TrustNode>> texplains;
// cache of nodes we have already explained by some theory
- std::unordered_map<Node, size_t, NodeHashFunction> cache;
+ std::unordered_map<Node, size_t> cache;
while (i < explanationVector.size()) {
// Get the current literal to explain
};/* struct NodeTheoryPair */
struct NodeTheoryPairHashFunction {
- NodeHashFunction hashFunction;
+ std::hash<Node> hashFunction;
// Hash doesn't take into account the timestamp
size_t operator()(const NodeTheoryPair& pair) const {
- uint64_t hash = fnv1a::fnv1a_64(NodeHashFunction()(pair.d_node));
+ uint64_t hash = fnv1a::fnv1a_64(std::hash<Node>()(pair.d_node));
return static_cast<size_t>(fnv1a::fnv1a_64(pair.d_theory, hash));
}
};/* struct NodeTheoryPairHashFunction */
* An empty set of relevant assertions, which is returned as a dummy value for
* getRelevantAssertions when relevance is disabled.
*/
- std::unordered_set<TNode, TNodeHashFunction> d_emptyRelevantSet;
+ std::unordered_set<TNode> d_emptyRelevantSet;
/** are we in eager model building mode? (see setEagerModelBuilding). */
bool d_eager_model_building;
* relevance manager failed to compute relevant assertions due to an internal
* error.
*/
- const std::unordered_set<TNode, TNodeHashFunction>& getRelevantAssertions(
- bool& success);
+ const std::unordered_set<TNode>& getRelevantAssertions(bool& success);
/**
* Forwards an entailment check according to the given theoryOfMode.
*/
class TheoryEngineProofGenerator : public ProofGenerator
{
- typedef context::
- CDHashMap<Node, std::shared_ptr<LazyCDProof>, NodeHashFunction>
- NodeLazyCDProofMap;
+ typedef context::CDHashMap<Node, std::shared_ptr<LazyCDProof>>
+ NodeLazyCDProofMap;
public:
TheoryEngineProofGenerator(ProofNodeManager* pnm, context::UserContext* u);
*/
class TheoryInferenceManager
{
- typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
+ typedef context::CDHashSet<Node> NodeSet;
public:
/**
Node TheoryModel::getModelValue(TNode n) const
{
- std::unordered_map<Node, Node, NodeHashFunction>::iterator it = d_modelCache.find(n);
+ std::unordered_map<Node, Node>::iterator it = d_modelCache.find(n);
if (it != d_modelCache.end()) {
return (*it).second;
}
/** are we using model cores? */
bool d_using_model_core;
/** symbols that are in the model core */
- std::unordered_set<Node, NodeHashFunction> d_model_core;
+ std::unordered_set<Node> d_model_core;
/** Get model value function.
*
* This function is a helper function for getValue.
virtual void addTermInternal(TNode n);
private:
/** cache for getModelValue */
- mutable std::unordered_map<Node, Node, NodeHashFunction> d_modelCache;
+ mutable std::unordered_map<Node, Node> d_modelCache;
//---------------------------- separation logic
/** the value of the heap */
void TheoryEngineModelBuilder::addToTypeList(
TypeNode tn,
std::vector<TypeNode>& type_list,
- std::unordered_set<TypeNode, TypeNodeHashFunction>& visiting)
+ std::unordered_set<TypeNode>& visiting)
{
if (std::find(type_list.begin(), type_list.end(), tn) == type_list.end())
{
// the set of equivalence classes that are "assignable", i.e. those that have
// an assignable expression in them (see isAssignable), and have not already
// been assigned a constant.
- std::unordered_set<Node, NodeHashFunction> assignableEqc;
+ std::unordered_set<Node> assignableEqc;
// The set of equivalence classes that are "evaluable", i.e. those that have
// an expression in them that is not assignable, and have not already been
// assigned a constant.
- std::unordered_set<Node, NodeHashFunction> evaluableEqc;
+ std::unordered_set<Node> evaluableEqc;
// Assigner objects for relevant equivalence classes that require special
// ways of assigning values, e.g. those that take into account assignment
// exclusion sets.
// should we compute assigner objects?
bool computeAssigners = tm->hasAssignmentExclusionSets();
// the set of exclusion sets we have processed
- std::unordered_set<Node, NodeHashFunction> processedExcSet;
+ std::unordered_set<Node> processedExcSet;
for (; !eqcs_i.isFinished(); ++eqcs_i)
{
Node eqc = *eqcs_i;
{
assertedReps[eqc] = rep;
typeRepSet.add(eqct.getBaseType(), eqc);
- std::unordered_set<TypeNode, TypeNodeHashFunction> visiting;
+ std::unordered_set<TypeNode> visiting;
addToTypeList(eqct.getBaseType(), type_list, visiting);
}
else
{
typeNoRepSet.add(eqct, eqc);
- std::unordered_set<TypeNode, TypeNodeHashFunction> visiting;
+ std::unordered_set<TypeNode> visiting;
addToTypeList(eqct, type_list, visiting);
}
*/
class TheoryEngineModelBuilder
{
- typedef std::unordered_map<Node, Node, NodeHashFunction> NodeMap;
- typedef std::unordered_set<Node, NodeHashFunction> NodeSet;
+ typedef std::unordered_map<Node, Node> NodeMap;
+ typedef std::unordered_set<Node> NodeSet;
public:
TheoryEngineModelBuilder();
* For example, if tn is (Array Int Bool) and type_list is empty,
* then we append ( Int, Bool, (Array Int Bool) ) to type_list.
*/
- void addToTypeList(
- TypeNode tn,
- std::vector<TypeNode>& type_list,
- std::unordered_set<TypeNode, TypeNodeHashFunction>& visiting);
+ void addToTypeList(TypeNode tn,
+ std::vector<TypeNode>& type_list,
+ std::unordered_set<TypeNode>& visiting);
/** assign function f based on the model m.
* This construction is based on "table form". For example:
* (f 0 1) = 1
*/
class TheoryPreprocessor
{
- typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeMap;
+ typedef context::CDHashMap<Node, Node> NodeMap;
public:
/** Constructs a theory preprocessor */
}
children.clear();
// remove duplicates while keeping the order of children
- std::unordered_set<TNode, TNodeHashFunction> clauseSet;
+ std::unordered_set<TNode> clauseSet;
unsigned size = n.getNumChildren();
for (unsigned i = 0; i < size; ++i)
{
*/
class TrustSubstitutionMap : public ProofGenerator
{
- using NodeUIntMap = context::CDHashMap<Node, size_t, NodeHashFunction>;
+ using NodeUIntMap = context::CDHashMap<Node, size_t>;
public:
TrustSubstitutionMap(context::Context* c,
// this is necessary for parametric types whose values are constructed from
// other types to ensure that we do not enumerate subterms of other
// previously enumerated values
- std::unordered_set<TNode, TNodeHashFunction> visited;
+ std::unordered_set<TNode> visited;
addSubTerms(n, visited);
++(*te);
return n;
}
void TypeSet::addSubTerms(TNode n,
- std::unordered_set<TNode, TNodeHashFunction>& visited,
+ std::unordered_set<TNode>& visited,
bool topLevel)
{
if (visited.find(n) == visited.end())
class TypeSet
{
public:
- typedef std::unordered_map<TypeNode, std::set<Node>*, TypeNodeHashFunction>
- TypeSetMap;
- typedef std::unordered_map<TypeNode, TypeEnumerator*, TypeNodeHashFunction>
- TypeToTypeEnumMap;
+ typedef std::unordered_map<TypeNode, std::set<Node>*> TypeSetMap;
+ typedef std::unordered_map<TypeNode, TypeEnumerator*> TypeToTypeEnumMap;
typedef TypeSetMap::iterator iterator;
typedef TypeSetMap::const_iterator const_iterator;
* (very low expression depth).
*/
void addSubTerms(TNode n,
- std::unordered_set<TNode, TNodeHashFunction>& visited,
+ std::unordered_set<TNode>& visited,
bool topLevel = true);
}; /* class TypeSet */
class CardinalityExtension
{
protected:
- typedef context::CDHashMap<Node, bool, NodeHashFunction> NodeBoolMap;
- typedef context::CDHashMap<Node, int, NodeHashFunction> NodeIntMap;
+ typedef context::CDHashMap<Node, bool> NodeBoolMap;
+ typedef context::CDHashMap<Node, int> NodeIntMap;
public:
/**
Node conclusion,
std::vector<Node>& premises,
CDProof* p,
- std::unordered_set<Node, NodeHashFunction>& assumptions) const
+ std::unordered_set<Node>& assumptions) const
{
Trace("eqproof-conv")
<< "EqProof::expandTransitivityForDisequalities: check if need "
Node conclusion,
std::vector<std::vector<Node>>& transitivityMatrix,
CDProof* p,
- std::unordered_map<Node, Node, NodeHashFunction>& visited,
- std::unordered_set<Node, NodeHashFunction>& assumptions,
+ std::unordered_map<Node, Node>& visited,
+ std::unordered_set<Node>& assumptions,
bool isNary) const
{
Trace("eqproof-conv") << "EqProof::reduceNestedCongruence: building for " << i
Node EqProof::addToProof(CDProof* p) const
{
- std::unordered_map<Node, Node, NodeHashFunction> cache;
- std::unordered_set<Node, NodeHashFunction> assumptions;
+ std::unordered_map<Node, Node> cache;
+ std::unordered_set<Node> assumptions;
Node conclusion = addToProof(p, cache, assumptions);
Trace("eqproof-conv") << "EqProof::addToProof: root of proof: " << conclusion
<< "\n";
return newConclusion;
}
-Node EqProof::addToProof(
- CDProof* p,
- std::unordered_map<Node, Node, NodeHashFunction>& visited,
- std::unordered_set<Node, NodeHashFunction>& assumptions) const
+Node EqProof::addToProof(CDProof* p,
+ std::unordered_map<Node, Node>& visited,
+ std::unordered_set<Node>& assumptions) const
{
- std::unordered_map<Node, Node, NodeHashFunction>::const_iterator it =
- visited.find(d_node);
+ std::unordered_map<Node, Node>::const_iterator it = visited.find(d_node);
if (it != visited.end())
{
Trace("eqproof-conv") << "EqProof::addToProof: already processed " << d_node
* equalities)
* @return the node that is the conclusion of the proof as added to p.
*/
- Node addToProof(
- CDProof* p,
- std::unordered_map<Node, Node, NodeHashFunction>& visited,
- std::unordered_set<Node, NodeHashFunction>& assumptions) const;
+ Node addToProof(CDProof* p,
+ std::unordered_map<Node, Node>& visited,
+ std::unordered_set<Node>& assumptions) const;
/** Removes all reflexivity steps, i.e. (= t t), from premises. */
void cleanReflPremises(std::vector<Node>& premises) const;
Node conclusion,
std::vector<Node>& premises,
CDProof* p,
- std::unordered_set<Node, NodeHashFunction>& assumptions) const;
+ std::unordered_set<Node>& assumptions) const;
/** Expand coarse-grained transitivity steps for theory disequalities
*
Node conclusion,
std::vector<std::vector<Node>>& transitivityMatrix,
CDProof* p,
- std::unordered_map<Node, Node, NodeHashFunction>& visited,
- std::unordered_set<Node, NodeHashFunction>& assumptions,
+ std::unordered_map<Node, Node>& visited,
+ std::unordered_set<Node>& assumptions,
bool isNary) const;
}; /* class EqProof */
KindMap d_congruenceKindsExtOperators;
/** Map from nodes to their ids */
- std::unordered_map<TNode, EqualityNodeId, TNodeHashFunction> d_nodeIds;
+ std::unordered_map<TNode, EqualityNodeId> d_nodeIds;
/** Map from function applications to their ids */
typedef std::unordered_map<FunctionApplication, EqualityNodeId, FunctionApplicationHashFunction> ApplicationIdsMap;
NodeNodeMap::const_iterator itus = d_uf_std_skolem.find(f);
if (itus == d_uf_std_skolem.end())
{
- std::unordered_set<Node, NodeHashFunction> fvs;
+ std::unordered_set<Node> fvs;
expr::getFreeVariables(f, fvs);
Node lem;
if (!fvs.empty())
*/
class HoExtension
{
- typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
- typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeNodeMap;
+ typedef context::CDHashSet<Node> NodeSet;
+ typedef context::CDHashMap<Node, Node> NodeNodeMap;
public:
HoExtension(TheoryState& state, TheoryInferenceManager& im);
*/
class ProofEqEngine : public EagerProofGenerator
{
- typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
- typedef context::CDHashMap<Node, std::shared_ptr<ProofNode>, NodeHashFunction>
- NodeProofMap;
+ typedef context::CDHashSet<Node> NodeSet;
+ typedef context::CDHashMap<Node, std::shared_ptr<ProofNode>> NodeProofMap;
public:
ProofEqEngine(context::Context* c,
}
TNode SymmetryBreaker::Template::find(TNode n) {
- unordered_map<TNode, TNode, TNodeHashFunction>::iterator i = d_reps.find(n);
+ unordered_map<TNode, TNode>::iterator i = d_reps.find(n);
if(i == d_reps.end()) {
return n;
} else {
break;
}
}
- unordered_map<TNode, set<TNode>, TNodeHashFunction>& ps = t.partitions();
+ unordered_map<TNode, set<TNode>>& ps = t.partitions();
for (auto& kv : ps)
{
Debug("ufsymm") << "UFSYMM partition*: " << kv.first;
}
if(!d_template.match(phi)) {
// we hit a bad match, extract the partitions and reset the template
- unordered_map<TNode, set<TNode>, TNodeHashFunction>& ps = d_template.partitions();
+ unordered_map<TNode, set<TNode>>& ps = d_template.partitions();
Debug("ufsymm") << "UFSYMM hit a bad match---have " << ps.size() << " partitions:" << endl;
- for(unordered_map<TNode, set<TNode>, TNodeHashFunction>::iterator i = ps.begin();
- i != ps.end();
- ++i) {
+ for (unordered_map<TNode, set<TNode>>::iterator i = ps.begin();
+ i != ps.end();
+ ++i)
+ {
Debug("ufsymm") << "UFSYMM partition: " << (*i).first;
set<TNode>& p = (*i).second;
if(Debug.isOn("ufsymm")) {
class Template {
Node d_template;
NodeBuilder d_assertions;
- std::unordered_map<TNode, std::set<TNode>, TNodeHashFunction> d_sets;
- std::unordered_map<TNode, TNode, TNodeHashFunction> d_reps;
+ std::unordered_map<TNode, std::set<TNode>> d_sets;
+ std::unordered_map<TNode, TNode> d_reps;
TNode find(TNode n);
bool matchRecursive(TNode t, TNode n);
public:
Template();
bool match(TNode n);
- std::unordered_map<TNode, std::set<TNode>, TNodeHashFunction>& partitions() { return d_sets; }
+ std::unordered_map<TNode, std::set<TNode>>& partitions() { return d_sets; }
Node assertions() {
switch(d_assertions.getNumChildren()) {
case 0: return Node::null();
typedef TNode Term;
typedef std::list<Term> Terms;
typedef std::set<Term> TermEq;
- typedef std::unordered_map<Term, TermEq, TNodeHashFunction> TermEqs;
-
-private:
+ typedef std::unordered_map<Term, TermEq> TermEqs;
+ private:
/**
* This class wasn't initially built to be incremental. It should
* be attached to a UserContext so that it clears everything when
Permutations d_permutations;
Terms d_terms;
Template d_template;
- std::unordered_map<Node, Node, NodeHashFunction> d_normalizationCache;
+ std::unordered_map<Node, Node> d_normalizationCache;
TermEqs d_termEqs;
TermEqs d_termEqsOnly;
vector<TNode> workList;
workList.push_back(n);
- std::unordered_set<TNode, TNodeHashFunction> processed;
+ std::unordered_set<TNode> processed;
while(!workList.empty()) {
n = workList.back();
// The only symbol in ~x (x is a boolean varible) should be x
Node x = d_skolemManager->mkDummySkolem("x", d_nodeManager->booleanType());
Node n = d_nodeManager->mkNode(NOT, x);
- std::unordered_set<Node, NodeHashFunction> syms;
+ std::unordered_set<Node> syms;
getSymbols(n, syms);
ASSERT_EQ(syms.size(), 1);
ASSERT_NE(syms.find(x), syms.end());
Node res = d_nodeManager->mkNode(AND, left, right);
// symbols
- std::unordered_set<Node, NodeHashFunction> syms;
+ std::unordered_set<Node> syms;
getSymbols(res, syms);
// assertions
TEST_F(TestNodeBlackNodeAlgorithm, get_operators_map)
{
// map to store result
- std::map<TypeNode, std::unordered_set<Node, NodeHashFunction> > result =
- std::map<TypeNode, std::unordered_set<Node, NodeHashFunction> >();
+ std::map<TypeNode, std::unordered_set<Node> > result =
+ std::map<TypeNode, std::unordered_set<Node> >();
// create test formula
Node x = d_skolemManager->mkDummySkolem("x", d_nodeManager->integerType());
Node a = d_skolemManager->mkDummySkolem("a", integer);
Node n1 = d_nodeManager->mkNode(MULT, two, x);
- std::unordered_map<Node, Node, NodeHashFunction> subs;
+ std::unordered_map<Node, Node> subs;
// check reflexivity
ASSERT_TRUE(match(n1, n1, subs));
d_two);
std::vector<Node> eqs = {eq1, eq2, eq3};
- std::unordered_map<Node, Node, NodeHashFunction> res;
+ std::unordered_map<Node, Node> res;
BVGauss::Result ret = BVGauss::gaussElimRewriteForUrem(eqs, res);
ASSERT_EQ(ret, BVGauss::Result::UNIQUE);
ASSERT_EQ(res.size(), 3);
d_two);
std::vector<Node> eqs = {eq1, eq2, eq3};
- std::unordered_map<Node, Node, NodeHashFunction> res;
+ std::unordered_map<Node, Node> res;
BVGauss::Result ret = BVGauss::gaussElimRewriteForUrem(eqs, res);
ASSERT_EQ(ret, BVGauss::Result::UNIQUE);
ASSERT_EQ(res.size(), 3);
TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_partial1a)
{
- std::unordered_map<Node, Node, NodeHashFunction> res;
+ std::unordered_map<Node, Node> res;
BVGauss::Result ret;
/* -------------------------------------------------------------------
TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_partial1b)
{
- std::unordered_map<Node, Node, NodeHashFunction> res;
+ std::unordered_map<Node, Node> res;
BVGauss::Result ret;
/* -------------------------------------------------------------------
TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_partial2)
{
- std::unordered_map<Node, Node, NodeHashFunction> res;
+ std::unordered_map<Node, Node> res;
BVGauss::Result ret;
/* -------------------------------------------------------------------
TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_partial3)
{
- std::unordered_map<Node, Node, NodeHashFunction> res;
+ std::unordered_map<Node, Node> res;
BVGauss::Result ret;
/* -------------------------------------------------------------------
TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_partial4)
{
- std::unordered_map<Node, Node, NodeHashFunction> res;
+ std::unordered_map<Node, Node> res;
BVGauss::Result ret;
/* -------------------------------------------------------------------
TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_partial5)
{
- std::unordered_map<Node, Node, NodeHashFunction> res;
+ std::unordered_map<Node, Node> res;
BVGauss::Result ret;
/* -------------------------------------------------------------------
TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_partial6)
{
- std::unordered_map<Node, Node, NodeHashFunction> res;
+ std::unordered_map<Node, Node> res;
BVGauss::Result ret;
/* -------------------------------------------------------------------
TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_with_expr_partial)
{
- std::unordered_map<Node, Node, NodeHashFunction> res;
+ std::unordered_map<Node, Node> res;
BVGauss::Result ret;
/* -------------------------------------------------------------------
TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_nary_partial)
{
- std::unordered_map<Node, Node, NodeHashFunction> res;
+ std::unordered_map<Node, Node> res;
BVGauss::Result ret;
/* -------------------------------------------------------------------
TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_not_invalid1)
{
- std::unordered_map<Node, Node, NodeHashFunction> res;
+ std::unordered_map<Node, Node> res;
BVGauss::Result ret;
/* -------------------------------------------------------------------
TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_not_invalid2)
{
- std::unordered_map<Node, Node, NodeHashFunction> res;
+ std::unordered_map<Node, Node> res;
BVGauss::Result ret;
/* -------------------------------------------------------------------
TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_invalid)
{
- std::unordered_map<Node, Node, NodeHashFunction> res;
+ std::unordered_map<Node, Node> res;
BVGauss::Result ret;
/* -------------------------------------------------------------------
AssertionPipeline apipe;
apipe.push_back(a);
passes::BVGauss bgauss(nullptr, "bv-gauss-unit");
- std::unordered_map<Node, Node, NodeHashFunction> res;
+ std::unordered_map<Node, Node> res;
PreprocessingPassResult pres = bgauss.applyInternal(&apipe);
ASSERT_EQ(pres, PreprocessingPassResult::NO_CONFLICT);
Node resx = d_nodeManager->mkNode(
apipe.push_back(eq4);
apipe.push_back(eq5);
passes::BVGauss bgauss(nullptr, "bv-gauss-unit");
- std::unordered_map<Node, Node, NodeHashFunction> res;
+ std::unordered_map<Node, Node> res;
PreprocessingPassResult pres = bgauss.applyInternal(&apipe);
ASSERT_EQ(pres, PreprocessingPassResult::NO_CONFLICT);
Node resx1 = d_nodeManager->mkNode(
apipe.push_back(eq1);
apipe.push_back(eq2);
passes::BVGauss bgauss(nullptr, "bv-gauss-unit");
- std::unordered_map<Node, Node, NodeHashFunction> res;
+ std::unordered_map<Node, Node> res;
PreprocessingPassResult pres = bgauss.applyInternal(&apipe);
ASSERT_EQ(pres, PreprocessingPassResult::NO_CONFLICT);
ASSERT_EQ(apipe.size(), 4);
Node zero = mkZero(32);
Node one = mkOne(32);
BvLinearAttribute is_linear;
- std::unordered_map<Node, bool, NodeHashFunction> contains_x;
+ std::unordered_map<Node, bool> contains_x;
contains_x[x] = true;
contains_x[neg_x] = true;
Node c = mkVar(32);
Node d = mkVar(32);
BvLinearAttribute is_linear;
- std::unordered_map<Node, bool, NodeHashFunction> contains_x;
+ std::unordered_map<Node, bool> contains_x;
contains_x[x] = true;
contains_x[neg_x] = true;
Node one = mkOne(32);
Node ntrue = mkTrue();
BvLinearAttribute is_linear;
- std::unordered_map<Node, bool, NodeHashFunction> contains_x;
+ std::unordered_map<Node, bool> contains_x;
contains_x[x] = true;
contains_x[neg_x] = true;
{
TypeEnumerator te(d_nodeManager->mkArrayType(d_nodeManager->integerType(),
d_nodeManager->integerType()));
- std::unordered_set<Node, NodeHashFunction> elts;
+ std::unordered_set<Node> elts;
for (uint32_t i = 0; i < 1000; ++i)
{
ASSERT_FALSE(te.isFinished());
projects / cvc5.git / commitdiff