| /dports/math/vampire/vampire-4.5.1/FMB/ |
| H A D | SortInference.cpp | 357 unsigned argSort; in doInference() local
359 argSort=seen++; in doInference()
388 unsigned argSort; in doInference() local
390 argSort=seen++; in doInference()
536 cout << argSort << " "; in doInference()
539 if(parentSet[argSort]){ in doInference()
552 parentSet[argSort]=true; in doInference()
554 _sig->parents[argSort] = getDistinctSort(argSort,vampireSort); in doInference()
595 if(parentSet[argSort]){ in doInference()
610 _sig->parents[argSort] = getDistinctSort(argSort,vampireSort); in doInference()
[all …]
|
| /dports/www/opencart/opencart-3.0.3.8/upload/catalog/model/extension/payment/ |
| H A D | alipay_cross.php | 57 $para_sort = $this->argSort($para_filter);
94 $para_sort = $this->argSort($para_filter);
138 function argSort($para) { function in ModelExtensionPaymentAlipayCross
|
| /dports/math/vampire/vampire-4.5.1/Shell/ |
| H A D | EqualityAxiomatizer.cpp | 125 unsigned argSort = ft->arg(ai); in saturateEqSorts() local
126 if(argSort==rngSort) { in saturateEqSorts()
129 isc.addImplication(argSort, rngSort); in saturateEqSorts()
|
| H A D | TermAlgebra.hpp | 44 unsigned argSort(unsigned ith);
|
| H A D | TermAlgebra.cpp | 46 unsigned TermAlgebraConstructor::argSort(unsigned ith) { return _type->arg(ith); } in argSort() function in Shell::TermAlgebraConstructor
|
| H A D | TheoryAxioms.cpp | 1193 if (c->argSort(j) == Sorts::SRT_BOOL) { in addExhaustivenessAxiom()
1284 …= Literal::createEquality(true, TermList(j * 2, false), TermList(j * 2 + 1, false), c->argSort(j)); in addInjectivityAxiom()
1362 if (c->argSort(i) != c->rangeSort()) continue; in addSubtermDefinitions()
|
| /dports/math/vampire/vampire-4.5.1/Kernel/ |
| H A D | SortHelper.cpp | 766 unsigned argSort = getResultSort(ta); in areImmediateSortsValid() local
767 if (eqSrt != argSort) { in areImmediateSortsValid()
780 unsigned argSort = getResultSort(ta); in areImmediateSortsValid() local
781 if (type.arg(i) != argSort) { in areImmediateSortsValid()
|
| /dports/math/vampire/vampire-4.5.1/Inferences/ |
| H A D | Induction.cpp | 459 if(con->argSort(i) == ta_sort){ in performStructInductionOne()
532 if(con->argSort(j)==ta_sort){ in performStructInductionTwo()
547 if(con->argSort(j) == ta_sort){ in performStructInductionTwo()
629 if(con->argSort(j)==ta_sort){ in performStructInductionThree()
648 if(con->argSort(j) == ta_sort){ in performStructInductionThree()
|
| /dports/math/vampire/vampire-4.5.1/Api/ |
| H A D | Helper.cpp | 516 Sort argSort = getSort(args[i]); in ensureArgumentsSortsMatch() local
517 if(argSort.isValid() && parentSort!=argSort) { in ensureArgumentsSortsMatch()
|
| /dports/math/vampire/vampire-4.5.1/Parse/ |
| H A D | SMTLIB2.hpp | 323 Interpretation getUnaryMinusInterpretation(unsigned argSort);
|
| H A D | SMTLIB2.cpp | 636 unsigned argSort = results.pop(); in declareSort() local
640 lookup->insert(argName,argSort); in declareSort()
1187 Interpretation SMTLIB2::getUnaryMinusInterpretation(unsigned argSort) in getUnaryMinusInterpretation() argument
1191 switch(argSort) { in getUnaryMinusInterpretation()
1197 USER_ERROR("invalid sort "+env.sorts->sortName(argSort)+" for interpretation -"); in getUnaryMinusInterpretation()
|
| /dports/math/vampire/vampire-4.5.1/Indexing/ |
| H A D | ClauseCodeTree.cpp | 666 unsigned argSort = SortHelper::getEqualityArgumentSort(lit); in canEnterLiteral() local
667 if(idxVarSort!=argSort) { in canEnterLiteral()
|
| /dports/lang/maude/maude-2.7.1/src/Mixfix/ |
| H A D | mixfixModule.cc | 1247 Sort* argSort = opDecls[i].getDomainAndRange()[argNr]; in mayAssoc() local
1250 if (leq(opDecls[j].getDomainAndRange()[nrArgs], argSort)) in mayAssoc()
|
| /dports/misc/mnn/MNN-1.2.0/source/backend/coreml/mlmodel/proto/ |
| H A D | NeuralNetwork.proto | 696 ArgSortLayerParams argSort = 1461; field
|