Home
last modified time | relevance | path

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

/dports/math/cvc4/CVC4-1.7/src/theory/
H A Dext_theory.cpp219 if (sendLemma(lem, true)) in doInferencesInternal()
268 if (sendLemma(lem)) in doInferencesInternal()
340 bool ExtTheory::sendLemma(Node lem, bool preprocess) in sendLemma() function in CVC4::theory::ExtTheory
H A Dext_theory.h197 bool sendLemma(Node lem, bool preprocess = false);
/dports/math/cvc4/CVC4-1.7/src/theory/sets/
H A Dtheory_sets_rels.h175 void sendLemma( Node fact, Node reason, const char * c );
H A Dtheory_sets_rels.cpp1062 void TheorySetsRels::sendLemma(Node conc, Node ant, const char * c) { in sendLemma() function in CVC4::theory::sets::TheorySetsRels
1161 …sendLemma(skolem.eqNode(NodeManager::currentNM()->mkNode(kind::SINGLETON,n)), d_trueNode, "share-t… in makeSharedTerm()
1201 sendLemma(tuple_reduction_lemma, d_trueNode, "tuple-reduction"); in reduceTupleVar()
/dports/math/cvc4/CVC4-1.7/src/theory/sep/
H A Dtheory_sep.h321 void sendLemma( std::vector< Node >& ant, Node conc, const char * c, bool infer = false );
H A Dtheory_sep.cpp1653 sendLemma( exp, n_conc, "PTO_NEG_PROP" ); in addPto()
1678 sendLemma( exp, p1[0][1].eqNode( p2[0][1] ), "PTO_PROP" ); in mergePto()
1682 void TheorySep::sendLemma( std::vector< Node >& ant, Node conc, const char * c, bool infer ) { in sendLemma() function in CVC4::theory::sep::TheorySep
/dports/math/cvc4/CVC4-1.7/src/theory/strings/
H A Dtheory_strings.h766 void sendLemma(Node ant, Node conc, const char* c);
H A Dtheory_strings.cpp4084 sendLemma( eq_exp, eq, c ); in sendInference()
4096 void TheoryStrings::sendLemma( Node ant, Node conc, const char * c ) { in sendLemma() function in CVC4::theory::strings::TheoryStrings
4129 sendLemma( d_true, eqs, c ); in sendInfer()