Home
last modified time | relevance | path

Searched refs:premLst (Results 1 – 5 of 5) sorted by relevance

/dports/math/vampire/vampire-4.5.1/Inferences/
H A DDistinctEqualitySimplifier.cpp70 UnitList* premLst = 0; in simplify() local
71 UnitList::pushFromIterator(Stack<Unit*>::Iterator(prems), premLst); in simplify()
72 ASS(premLst); // at least, because of "prems.push(cl);" above in simplify()
75 SimplifyingInferenceMany(InferenceRule::DISTINCT_EQUALITY_REMOVAL, premLst)); in simplify()
H A DHyperSuperposition.cpp316 UnitList* premLst = 0; in tryUnifyingSuperpositioins() local
317 UnitList::pushFromIterator(ClauseStack::Iterator(premises), premLst); in tryUnifyingSuperpositioins()
318 UnitList::push(cl, premLst); in tryUnifyingSuperpositioins()
320 …romStack(resLits, GeneratingInferenceMany(InferenceRule::HYPER_SUPERPOSITION_GENERATING, premLst)); in tryUnifyingSuperpositioins()
471 UnitList* premLst = 0; in tryGetContradictionFromUnification() local
472 UnitList::pushFromIterator(ClauseStack::Iterator(premStack), premLst); in tryGetContradictionFromUnification()
473 UnitList::push(cl, premLst); in tryGetContradictionFromUnification()
475 GeneratingInferenceMany(InferenceRule::HYPER_SUPERPOSITION_SIMPLIFYING, premLst)); in tryGetContradictionFromUnification()
H A DURResolution.cpp166 UnitList* premLst = 0; in generateClause() local
167 UnitList::push(_orig, premLst); in generateClause()
179 UnitList::push(premise, premLst); in generateClause()
182 Inference inf(GeneratingInferenceMany(InferenceRule::UNIT_RESULTING_RESOLUTION, premLst)); in generateClause()
/dports/math/vampire/vampire-4.5.1/Kernel/
H A DFormulaTransformer.cpp485 UnitList* premLst = 0; in apply() local
486 UnitList::pushFromIterator(UnitStack::Iterator(prems), premLst); in apply()
487 UnitList::push(unit, premLst); in apply()
489 res = new FormulaUnit(newForm, FormulaTransformationMany(_infRule, premLst)); in apply()
520 UnitList* premLst = 0; in apply() local
521 UnitList::pushFromIterator(UnitStack::Iterator(prems), premLst); in apply()
522 UnitList::push(cl, premLst); in apply()
524 …= Clause::fromIterator(LiteralStack::Iterator(lits), FormulaTransformationMany(_infRule, premLst)); in apply()
/dports/math/vampire/vampire-4.5.1/SAT/
H A DTWLSolver.cpp1376 SATClauseList* premLst = 0; in getZeroImpliedCertificate() local
1377 SATClauseList::pushFromIterator(SATClauseStack::Iterator(prems), premLst); in getZeroImpliedCertificate()
1378 SATInference* inf = new PropInference(premLst); in getZeroImpliedCertificate()