Home
last modified time | relevance | path

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

/dports/math/cvc4/CVC4-1.7/src/theory/uf/
H A Dequality_engine_types.h76 MERGED_THROUGH_TRANS, enumerator
96 case MERGED_THROUGH_TRANS:
H A Dequality_engine.cpp948 eqp->d_id = eq::MERGED_THROUGH_TRANS; in explainEquality()
973 if (eqpc->d_id == eq::MERGED_THROUGH_TRANS) { in explainEquality()
1287 eqp->d_id = MERGED_THROUGH_TRANS; in getExplanation()
/dports/math/cvc4/CVC4-1.7/src/theory/arrays/
H A Darray_proof_reconstruction.cpp164 childProof->d_id = theory::eq::MERGED_THROUGH_TRANS; in notify()
/dports/math/cvc4/CVC4-1.7/src/proof/
H A Darith_proof.cpp107 Assert(pf.d_id == theory::eq::MERGED_THROUGH_TRANS); in toStreamRecLFSC()
114 subTrans->d_id = theory::eq::MERGED_THROUGH_TRANS; in toStreamRecLFSC()
410 case theory::eq::MERGED_THROUGH_TRANS: { in toStreamRecLFSC()
H A Darray_proof.cpp49 if (tag == theory::eq::MERGED_THROUGH_TRANS) return "Transitivity"; in printTag()
143 (pf.d_children[neg]->d_id == theory::eq::MERGED_THROUGH_TRANS)) { in toStreamRecLFSC()
454 case theory::eq::MERGED_THROUGH_TRANS: in toStreamRecLFSC()
H A Dtheory_proof.cpp1397 Assert(pf.d_id == theory::eq::MERGED_THROUGH_TRANS); in assertAndPrint()
1401 subTrans->d_id = theory::eq::MERGED_THROUGH_TRANS; in assertAndPrint()
H A Duf_proof.cpp320 case theory::eq::MERGED_THROUGH_TRANS: { in toStreamRecLFSC()