| /dports/math/vampire/vampire-4.5.1/Kernel/ |
| H A D | TermTransformer.cpp | 78 TermList *argLst = &args.top() - (orig->arity() - 1); in transform() local
80 args.push(TermList(Term::create(orig, argLst))); in transform()
128 TermList* argLst = &args.top() - (term->arity() - 1); in transform() local
131 return Literal::create(static_cast<Literal*>(term), argLst); in transform()
133 return Term::create(term, argLst); in transform()
269 TermList* argLst = 0; in transform() local
274 argLst=&args.top() - (orig->arity()-1); in transform()
280 args.push(transformSubterm(TermList(Term::create(orig,argLst)))); in transform()
307 TermList* argLst=&args.top() - (term->arity() - 1); in transform() local
309 return Literal::create(static_cast<Literal*>(term), argLst); in transform()
[all …]
|
| H A D | SubstHelper.hpp | 358 TermList* argLst=&args->top() - (orig->arity()-1); in applyImpl() local
360 bool shouldShare=!noSharing && canBeShared(argLst, orig->arity()); in applyImpl()
364 newTrm=Term::create(orig,argLst); in applyImpl()
367 newTrm=Term::createNonShared(orig,argLst); in applyImpl()
422 TermList* argLst=&args->top() - (trm->arity()-1); in applyImpl() local
427 result=Literal::create(lit,argLst); in applyImpl()
430 bool shouldShare=!noSharing && canBeShared(argLst, trm->arity()); in applyImpl()
432 result=Term::create(trm,argLst); in applyImpl()
434 result=Term::createNonShared(trm,argLst); in applyImpl()
|
| H A D | EqHelper.cpp | 126 TermList* argLst=&args.top() - (orig->arity()-1); in replace() local
129 args.push(TermList(Term::create(orig,argLst))); in replace()
166 TermList* argLst=&args.top() - (trm0->arity()-1); in replace() local
170 return Literal::create(lit,argLst); in replace()
172 return Term::create(trm0,argLst); in replace()
|
| H A D | RobSubstitution.cpp | 638 TermList* argLst=&args.top() - (orig->arity()-1); in apply() local
641 constructed.setTerm(Term::create(orig,argLst)); in apply()
|
| /dports/math/vampire/vampire-4.5.1/Inferences/ |
| H A D | InterpretedSimplifier.cpp | 798 TermList* argLst=&args.top() - (orig->arity()-1);
803 …if(simplifyFunction(itp, argLst, sfRes) && _ordering->compare(sfRes,TermList(orig))==Ordering::LES…
812 newTrm=Term::create(orig,argLst);
855 TermList* argLst=&args.top() - (lit->arity()-1);
859 if(simplifyPredicate(itp, argLst, lit, constant, res, constantTrue)) {
868 res=Literal::create(lit,argLst);
|
| /dports/math/vampire/vampire-4.5.1/Shell/ |
| H A D | FunctionDefinition.cpp | 594 TermList* argLst=&args.top() - (orig->arity()-1); in applyDefinitions() local
596 Term* newTrm=Term::create(orig,argLst); in applyDefinitions()
679 TermList* argLst=&args.top() - (lit->arity()-1); in applyDefinitions() local
680 return Literal::create(static_cast<Literal*>(lit),argLst); in applyDefinitions()
|
| /dports/math/vampire/vampire-4.5.1/Parse/ |
| H A D | SMTLIB2.cpp | 1609 FormulaList* argLst = nullptr; in parseAsBuiltinFormulaSymbol() local
1620 FormulaList::push(argFla,argLst); in parseAsBuiltinFormulaSymbol()
1629 res = new JunctionFormula( (fs==FS_AND) ? AND : OR, argLst); in parseAsBuiltinFormulaSymbol()
1631 res = argLst->head(); in parseAsBuiltinFormulaSymbol()
1632 FormulaList::destroy(argLst); in parseAsBuiltinFormulaSymbol()
1720 FormulaList* argLst = nullptr; in parseAsBuiltinFormulaSymbol() local
1728 FormulaList::push(lastConjunct,argLst); in parseAsBuiltinFormulaSymbol()
1757 if (argLst == nullptr) { // there were only two arguments, let's return lastConjunct in parseAsBuiltinFormulaSymbol()
1761 FormulaList::push(lastConjunct,argLst); in parseAsBuiltinFormulaSymbol()
1763 Formula* res = new JunctionFormula( AND, argLst); in parseAsBuiltinFormulaSymbol()
|
| H A D | SMTLIB.cpp | 993 FormulaList* argLst = 0; in tryReadConnective() local
994 FormulaList::pushFromIterator(FormulaStack::Iterator(argForms), argLst); in tryReadConnective()
995 res = new JunctionFormula( (fsym==FS_AND) ? AND : OR, argLst); in tryReadConnective()
|
| /dports/multimedia/opentoonz/opentoonz-1.5.0/toonz/sources/include/tw/ |
| H A D | message.h | 129 DVAPI int multipleChoicesQuestion(const string &question, const ArgList &argLst,
|