Home
last modified time | relevance | path

Searched refs:n_lbl (Results 1 – 4 of 4) sorted by relevance

/dports/math/cvc4/CVC4-1.7/src/theory/datatypes/
H A Dtheory_datatypes.cpp958 size_t n_lbl = (*lbl_i).second; in getLabel() local
959 if( n_lbl>0 && d_labels_data[n][ n_lbl-1 ].getKind()!=kind::NOT ){ in getLabel()
1000 size_t n_lbl = (*lbl_i).second; in getPossibleCons() local
1001 for (size_t i = 0; i < n_lbl; i++) in getPossibleCons()
1079 size_t n_lbl = (*lbl_i).second; in addTester() local
1081 for (size_t i = 0; i < n_lbl; i++) in addTester()
1100 d_labels[n] = n_lbl + 1; in addTester()
1104 d_labels_data[n][n_lbl] = t; in addTester()
1112 n_lbl++; in addTester()
1224 size_t n_lbl = (*lbl_i).second; in addConstructor() local
[all …]
/dports/math/ggobi/ggobi-2.1.11/src/
H A Dbrushing.h99 GtkWidget *nh_lbl, *ns_lbl, *n_lbl; member
H A Dexclusion_ui.c120 gtk_label_set_text (GTK_LABEL (d->clusvui[k].n_lbl), str); in cluster_table_labels_update()
405 d->clusvui[k].n_lbl = gtk_label_new (str); in cluster_add()
407 d->clusvui[k].n_lbl, in cluster_add()
420 gtk_widget_destroy (d->clusvui[k].n_lbl); in cluster_free()
/dports/math/cvc4/CVC4-1.7/src/theory/sep/
H A Dtheory_sep.cpp1132 Node n_lbl = NodeManager::currentNM()->mkSkolem( ss.str(), ltn, "base label" ); in getBaseLabel() local
1133 d_base_label[tn] = n_lbl; in getBaseLabel()
1202 Node nrlem = NodeManager::currentNM()->mkNode( kind::MEMBER, nr, n_lbl ).negate(); in getBaseLabel()
1206 return n_lbl; in getBaseLabel()
1256 Node n_lbl = NodeManager::currentNM()->mkSkolem( ss.str(), ltn, "sep label" ); in getLabel() local
1257 d_label_map[atom][lbl][child] = n_lbl; in getLabel()
1258 d_label_map_parent[n_lbl] = lbl; in getLabel()
1259 return n_lbl; in getLabel()