Searched refs:divisorTerm (Results 1 – 2 of 2) sorted by relevance
347 TermList divisorTerm=*args[argIndex].term()->nthArgument(1);348 InterpretedType divisor=theory->interpretConstant(divisorTerm);351 newArgs[0]=divisorTerm;361 newArgs[1]=divisorTerm;
2101 TermList divisorTerm = TermList(Term::createConstant(divisorSymb)); in parseRankedFunctionApplication() local2110 env.signature->recordDividesNvalue(divisorTerm); in parseRankedFunctionApplication()2112 Formula* res = new AtomicFormula(Literal::create2(pred,true,divisorTerm,arg)); in parseRankedFunctionApplication()