Searched refs:active_lbl (Results 1 – 2 of 2) sorted by relevance
| /dports/math/cvc4/CVC4-1.7/src/theory/sep/ |
| H A D | theory_sep.cpp | 641 std::map< Node, bool > active_lbl; in check() local
658 active_lbl[s_lbl] = true; in check()
710 …nst = instantiateLabel( s_atom, s_lbl, s_lbl, o_b_lbl_mval, visited, d_pto_model, tn, active_lbl ); in check()
1297 TypeNode rtn, std::map< Node, bool >& active_lbl, unsigned ind ) { in instantiateLabel()
1299 if( options::sepMinimalRefine() && lbl!=o_lbl && active_lbl.find( lbl )!=active_lbl.end() ){ in instantiateLabel()
1335 …antiateLabel( n[sub_index], o_lbl, sub_lbl, lbl_mval, visited, pto_model, rtn, active_lbl, ind+1 ); 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 | 308 TypeNode rtn, std::map< Node, bool >& active_lbl, unsigned ind = 0 );
|