Home
last modified time | relevance | path

Searched refs:divisorTerm (Results 1 – 2 of 2) sorted by relevance

/dports/math/vampire/vampire-4.5.1/Inferences/
H A DInterpretedSimplifier.cpp347 TermList divisorTerm=*args[argIndex].term()->nthArgument(1);
348 InterpretedType divisor=theory->interpretConstant(divisorTerm);
351 newArgs[0]=divisorTerm;
361 newArgs[1]=divisorTerm;
/dports/math/vampire/vampire-4.5.1/Parse/
H A DSMTLIB2.cpp2101 TermList divisorTerm = TermList(Term::createConstant(divisorSymb)); in parseRankedFunctionApplication() local
2110 env.signature->recordDividesNvalue(divisorTerm); in parseRankedFunctionApplication()
2112 Formula* res = new AtomicFormula(Literal::create2(pred,true,divisorTerm,arg)); in parseRankedFunctionApplication()