Searched refs:lbl_v (Results 1 – 2 of 2) sorted by relevance
| /dports/math/cvc4/CVC4-1.7/src/theory/sep/ |
| H A D | theory_sep.cpp | 1296 Node TheorySep::instantiateLabel( Node n, Node o_lbl, Node lbl, Node lbl_v, std::map< Node, Node >&… in instantiateLabel() argument
1298 Trace("sep-inst-debug") << "Instantiate label " << n << " " << lbl << " " << lbl_v << std::endl; in instantiateLabel()
1306 Trace("sep-inst") << n << "[" << lbl << "] :: " << lbl_v << std::endl; in instantiateLabel()
1402 return NodeManager::currentNM()->mkNode( kind::SEP_LABEL, n, lbl_v ); in instantiateLabel()
1426 …entNM()->mkNode( kind::EQUAL, NodeManager::currentNM()->mkNode( kind::SINGLETON, n[0] ), lbl_v ) ); in instantiateLabel()
1432 return lbl_v.eqNode( NodeManager::currentNM()->mkConst(EmptySet(lbl_v.getType().toType())) ); in instantiateLabel()
1442 … Node aln = instantiateLabel( n[i], o_lbl, lbl, lbl_v, visited, pto_model, rtn, active_lbl, ind ); in instantiateLabel()
|
| H A D | theory_sep.h | 307 …Node instantiateLabel( Node n, Node o_lbl, Node lbl, Node lbl_v, std::map< Node, Node >& visited, …
|