Searched refs:premLst (Results 1 – 5 of 5) sorted by relevance
/dports/math/vampire/vampire-4.5.1/Inferences/ |
H A D | DistinctEqualitySimplifier.cpp | 70 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 D | HyperSuperposition.cpp | 316 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 D | URResolution.cpp | 166 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 D | FormulaTransformer.cpp | 485 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 D | TWLSolver.cpp | 1376 SATClauseList* premLst = 0; in getZeroImpliedCertificate() local 1377 SATClauseList::pushFromIterator(SATClauseStack::Iterator(prems), premLst); in getZeroImpliedCertificate() 1378 SATInference* inf = new PropInference(premLst); in getZeroImpliedCertificate()
|