Searched refs:d_theory (Results 1 – 10 of 10) sorted by relevance
| /dports/math/cvc4/CVC4-1.7/src/proof/ |
| H A D | proof_output_channel.cpp | 81 : d_theory(theory) in MyPreRegisterVisitor()
90 d_theory->preRegisterTerm(current); in visit()
|
| H A D | proof_output_channel.h | 64 theory::Theory* d_theory; variable
|
| H A D | lemma_proof.cpp | 22 d_theory(theory), d_literalToProve(literalToProve) { in ProofStep()
26 return d_theory; in getTheory()
|
| H A D | theory_proof.h | 208 theory::Theory* d_theory;
214 : d_theory(th) in TheoryProof()
|
| H A D | lemma_proof.h | 41 theory::TheoryId d_theory;
|
| H A D | theory_proof.cpp | 1013 Assert(d_theory!=NULL); in printTheoryLemmaProof()
1020 Trace("pf::tp") << ";; Print theory lemma proof, theory id = " << d_theory->getId() << std::endl; in printTheoryLemmaProof()
1022 if (d_theory->getId()==theory::THEORY_UF) { in printTheoryLemmaProof()
1026 } else if (d_theory->getId()==theory::THEORY_ARRAYS) { in printTheoryLemmaProof()
1030 } else if (d_theory->getId() == theory::THEORY_ARITH) { in printTheoryLemmaProof()
1046 d_theory->getId() == theory::Theory::theoryOf(strippedLit)) { in printTheoryLemmaProof()
|
| /dports/math/cvc4/CVC4-1.7/src/theory/ |
| H A D | theory_engine.h | 280 theory::TheoryId d_theory; variable
284 : d_engine(engine), d_statistics(theory), d_theory(theory) {} in EngineOutputChannel()
310 << "EngineOutputChannel<" << d_theory << ">::restart(" << restartVar in demandRestart()
325 d_engine->setIncomplete(d_theory); in setIncomplete()
|
| H A D | theory_engine.cpp | 85 Debug("theory::lemma") << "EngineOutputChannel<" << d_theory << ">::lemma(" in lemma()
91 PROOF({ registerLemmaRecipe(lemma, lemma, preprocess, d_theory); }); in lemma()
95 sendAtoms ? d_theory : theory::THEORY_LAST); in lemma()
186 Debug("theory::lemma") << "EngineOutputChannel<" << d_theory << ">::lemma(" in splitLemma()
194 d_engine->lemma(lemma, RULE_SPLIT, false, removable, false, d_theory); in splitLemma()
199 Debug("theory::propagate") << "EngineOutputChannel<" << d_theory in propagate()
203 return d_engine->propagate(literal, d_theory); in propagate()
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/sets/ |
| H A D | theory_sets_private.h | 288 TheorySetsPrivate& d_theory; variable
291 NotifyClass(TheorySetsPrivate& theory): d_theory(theory) {} in NotifyClass()
|
| H A D | theory_sets_private.cpp | 2293 return d_theory.propagate(equality); in eqNotifyTriggerEquality()
2296 return d_theory.propagate(equality.notNode()); in eqNotifyTriggerEquality()
2305 return d_theory.propagate(predicate); in eqNotifyTriggerPredicate()
2307 return d_theory.propagate(predicate.notNode()); in eqNotifyTriggerPredicate()
2315 d_theory.propagate( value ? t1.eqNode( t2 ) : t1.eqNode( t2 ).negate() ); in eqNotifyTriggerTermEquality()
2322 d_theory.conflict(t1, t2); in eqNotifyConstantTermMerge()
2328 d_theory.eqNotifyNewClass(t); in eqNotifyNewClass()
2334 d_theory.eqNotifyPreMerge(t1, t2); in eqNotifyPreMerge()
2340 d_theory.eqNotifyPostMerge(t1, t2); in eqNotifyPostMerge()
2346 d_theory.eqNotifyDisequal(t1, t2, reason); in eqNotifyDisequal()
|