Home
last modified time | relevance | path

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

/dports/math/cvc4/CVC4-1.7/src/theory/sep/
H A Dtheory_sep.cpp410 … Node nrlem = NodeManager::currentNM()->mkNode( kind::MEMBER, nr, labels[0] ).negate(); in check() local
411 … Trace("sep-lemma") << "Sep::Lemma: sep.nil not in wand antecedant heap : " << nrlem << std::endl; in check()
412 d_out->lemma( nrlem ); in check()
1202 Node nrlem = NodeManager::currentNM()->mkNode( kind::MEMBER, nr, n_lbl ).negate(); in getBaseLabel() local
1203 …Trace("sep-lemma") << "Sep::Lemma: sep.nil not in base label " << tn << " : " << nrlem << std::end… in getBaseLabel()
1204 d_out->lemma( nrlem ); in getBaseLabel()