Home
last modified time | relevance | path

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

/dports/math/cvc4/CVC4-1.7/src/theory/
H A Dtheory_engine.h293 void conflict(TNode conflictNode,
H A Dtheory_engine.cpp206 void TheoryEngine::EngineOutputChannel::conflict(TNode conflictNode, in conflict() argument
210 << "EngineOutputChannel<" << d_theory << ">::conflict(" << conflictNode in conflict()
215 d_engine->conflict(conflictNode, d_theory); in conflict()
/dports/math/cvc4/CVC4-1.7/src/theory/sep/
H A Dtheory_sep.cpp832 Node conflictNode = explain(a.eqNode(b)); in conflict() local
834 d_out->conflict( conflictNode ); in conflict()
/dports/math/cvc4/CVC4-1.7/src/theory/strings/
H A Dtheory_strings.cpp1109 Node conflictNode; in conflict() local
1110 conflictNode = explain( a.eqNode(b) ); in conflict()
1111 Trace("strings-conflict") << "CONFLICT: Eq engine conflict : " << conflictNode << std::endl; in conflict()
1112 d_out->conflict( conflictNode ); in conflict()