Searched refs:getTheory (Results 1 – 8 of 8) sorted by relevance
25 theory::TheoryId LemmaProofRecipe::ProofStep::getTheory() const { in getTheory() function in CVC4::LemmaProofRecipe::ProofStep90 Debug(tag) << "\tStep #" << count << ": " << "\t[" << step.getTheory() << "] "; in dump()132 theory::TheoryId LemmaProofRecipe::getTheory() const { in getTheory() function in CVC4::LemmaProofRecipe134 return d_proofSteps.back().getTheory(); in getTheory()224 out << " theory = " << step.getTheory(); in operator <<()234 out << "\n theory = " << recipe.getTheory(); in operator <<()
35 theory::TheoryId getTheory() const;49 theory::TheoryId getTheory() const;
233 return pm->getCnfProof()->getProofRecipe(nodes).getTheory(); in getTheoryForLemma()516 if (currentStep->getTheory() != theory::THEORY_BV) { in finalizeBvConflicts()744 theory::TheoryId theory_id = currentStep->getTheory(); in printTheoryLemmas()
405 Debug("pf::lemmasUnsatCore") << "\t[owner = " << recipe.getTheory() in getLemmasInUnsatCore()407 …if (recipe.simpleLemma() && recipe.getTheory() == theory && seen.find(recipe.getOriginalLemma()) =… in getLemmasInUnsatCore()
41 Theory* getTheory(int i) const { return d_tlist[i]; } in getTheory() function
487 n, c, thss->getTheory()->getValuation())); in SortModel()505 d_thss->getTheory()->getDecisionManager()->registerStrategy( in initialize()623 a = d_thss->getTheory()->d_equalityEngine.getRepresentative( a ); in assertDisequal()624 b = d_thss->getTheory()->d_equalityEngine.getRepresentative( b ); in assertDisequal()663 Assert( a == d_thss->getTheory()->d_equalityEngine.getRepresentative( a ) ); in areDisequal()664 Assert( b == d_thss->getTheory()->d_equalityEngine.getRepresentative( b ) ); in areDisequal()839 << d_thss->getTheory()->d_valuation.getAssertionLevel() << std::endl; in assertCardinality()
367 TheoryUF* getTheory() { return d_th; } in getTheory() function
102 os << "[" << l.getTheory(i)->getName() << ", " << l.getExpr(i) << "]\n"; in operator <<()178 L->getTheory(k)->update(e, L->getExpr(k)); in processNotify()