Searched refs:TheoryAxiom (Results 1 – 4 of 4) sorted by relevance
492 struct TheoryAxiom { struct493 TheoryAxiom(InferenceRule r) : rule(r) {} in TheoryAxiom() argument616 Inference(const TheoryAxiom& ta);
387 Inference::Inference(const TheoryAxiom& ta) { in Inference()
92 Clause* cl = Clause::fromStack(lit_stack, TheoryAxiom(rule)); in addTheoryClauseFromLits()837 …addAndOutputTheoryUnit(new FormulaUnit(axiom, TheoryAxiom(InferenceRule::THA_BOOLEAN_ARRAY_EXTENSI… in addBooleanArrayExtensionalityAxioms()909 …addAndOutputTheoryUnit(new FormulaUnit(ax, TheoryAxiom(InferenceRule::THA_BOOLEAN_ARRAY_WRITE1)),C… in addBooleanArrayWriteAxioms()925 …addAndOutputTheoryUnit(new FormulaUnit(ax2, TheoryAxiom(InferenceRule::THA_BOOLEAN_ARRAY_WRITE2)),… in addBooleanArrayWriteAxioms()1214 axiom = Clause::fromStack(lits, TheoryAxiom(InferenceRule::TERM_ALGEBRA_EXHAUSTIVENESS_AXIOM)); in addExhaustivenessAxiom()1231 … axiom = new FormulaUnit(universal, TheoryAxiom(InferenceRule::TERM_ALGEBRA_EXHAUSTIVENESS_AXIOM)); in addExhaustivenessAxiom()
376 Inference inf1 = TheoryAxiom(rule); in performMathInductionOne()379 Inference inf2 = TheoryAxiom(rule); in performMathInductionOne()