}
// get unlocked copy, modify, copy and relock
LogicInfo log(d_logic.getUnlockedCopy());
- log.enableQuantifiers();
- log.enableTheory(theory::THEORY_UF);
- log.enableTheory(theory::THEORY_DATATYPES);
- log.enableIntegers();
- log.enableHigherOrder();
+ // enable everything needed for sygus
+ log.enableSygus();
d_logic = log;
d_logic.lock();
}
}
}
Kind sk = sop.getKind() != kind::BUILTIN
- ? kind::APPLY_UF
+ ? getKindForFunction(sop)
: getExprManager()->operatorToKind(sop);
Debug("parser-sygus") << ": operator " << sop << " with " << sop.getKind() << " " << sk << std::endl;
Expr e = getExprManager()->mkExpr( sk, children );