43 :
Theory(core,
"Uninterpreted Functions"),
44 d_applicationsInModel(core->getFlags()[
"applications"].getBool()),
45 d_funApplications(core->getCM()->getCurrentContext()),
46 d_funApplicationsIdx(core->getCM()->getCurrentContext(), 0),
47 d_sharedIdx1(core->getCM()->getCurrentContext(), 0),
48 d_sharedIdx2(core->getCM()->getCurrentContext(), 0),
49 d_sharedTermsMap(core->getCM()->getCurrentContext())
62 kinds.push_back(
ARROW);
64 kinds.push_back(
UFUNC);
93 DebugAssert(!rel.isNull(),
"Expected known identifier");
95 "Unexpected use of transitive closure: "+expr.
toString());
105 pTable = (*i).second;
115 pList = (*i2).second;
125 pList = (*i2).second;
133 pList = (*i2).second;
135 for (l = 0; l < s; ++l) {
142 pList = (*i2).second;
144 for (l = 0; l < s; ++l) {
159 bool enqueued =
false;
164 IF_DEBUG(debugger.counter(
"Expanded lambdas (checkSat)")++;)
171 if (!fullEffort || enqueued)
return;
180 for( ; d_sharedIdx2 <
d_sharedIdx1; d_sharedIdx2 = d_sharedIdx2 + 1 ) {
185 if( f1 != f2 &&
find(f1).getRHS() !=
find(f2).getRHS() && f1_fun == f2_fun ) {
186 for(
int k = 0; k < f1.
arity(); ++k ) {
194 if( !
simplify(eq).getRHS().isBoolConst() ) {
221 IF_DEBUG(debugger.counter(
"Expanded lambdas")++;)
252 TRACE(
"model",
"TheoryUF: add function application ", e,
"");
297 if (sigNew == dsig) {
303 if (!repEQsigNew.
isNull()) {
312 int k, ar(d.
arity());
313 for (k = 0; k < ar; ++k) {
314 if (sigNew[k] != dsig[k]) {
342 (
"Function type needs at least two arguments"
345 for (; i != iend; ) {
348 if (i == iend && t.
isBool())
break;
350 (
"Function argument types must be non-Boolean: "
353 (
"Function domain or range types cannot be functions: "
362 DebugAssert(
false,
"Unexpected kind in TheoryUF::checkType"
369 bool enumerate,
bool computeSize)
378 bool getSize = enumerate || computeSize;
379 for (; i != iend; ) {
391 thisSize = thisSize * size;
393 if (thisSize > 1000000) thisSize = 0;
422 const vector<Expr>& vars = e.
getVars();
424 "TheorySimulate::computeType("+e.
toString()+
")");
425 for(vector<Expr>::const_iterator i=vars.begin(), iend=vars.end();
427 args.push_back((*i).getType());
438 if (funExpr.isNull()) {
440 (
"Attempt to take transitive closure of unknown id: "
443 Type funType = funExpr.getType();
446 (
"Attempt to take transitive closure of non-function:\n\n"
447 +funExpr.toString() +
"\n\n which has type: "
450 if(funType.
arity()!=3) {
452 (
"Attempt to take transitive closure of non-binary function:\n\n"
453 +funExpr.toString() +
"\n\n which has type: "
456 if (!funType[2].isBool()) {
458 (
"Attempt to take transitive closure of function:\n\n"
459 +funExpr.toString() +
"\n\n which does not return BOOLEAN");
485 "TheoryUF::computeBaseType("+t.
toString()+
")");
494 if((*i).isApply() && (*i).getOp().getExpr() == e) {
521 if((*i).isApply() && (*i).getOp().getExpr() == e) {
523 vector<Theorem> thms;
524 vector<unsigned> changed;
525 for(
int j=0; j<(*i).arity(); ++j) {
528 thms.push_back(asst);
529 changed.push_back(j);
533 if(changed.size()>0) {
547 if(appls.
size()==0) {
553 static unsigned count(0);
555 +
" : "+tp.toString()+
")");
556 for(
int i=0, iend=tp.arity()-1; i<iend; ++i) {
562 DebugAssert(args.size()>0,
"TheoryUF::computeModel()");
564 DebugAssert(i!=iend,
"TheoryUF::computeModel(): empty appls hash");
566 Expr res((*i).second); ++i;
567 for(; i!=iend; ++i) {
571 if((*i).second == res)
continue;
576 for(
int j=0, jend=args.size(); j<jend; ++j)
577 eqs.push_back(args[j].eqExpr((*i).first[j]));
583 res = cond.
iteExpr((*i).second, res);
619 Type funType(op.getType());
620 DebugAssert(funType.isFunction() || funType.isBool(),
621 "TheoryUF::computeTCC(): funType = "
622 +funType.toString());
623 if(funType.isFunction()) {
625 "TheoryUF::computeTCC(): funType = "
626 +funType.toString()+
"\n e = "+e.
toString());
627 for(
int i=0, iend=e.
arity(); i<iend; ++i) {
631 if(funType[i] != e[i].getType())
636 while(op.getKind()==
LETDECL) op = op[1];
678 for(
int i = 0, iend = e.
arity(); i < iend; ++i )
681 os <<
space <<
":transclose";
694 DebugAssert(
false,
"TheoryUF::print: SMTLIB_LANG: Unexpected expression: "
706 os<<
"ERROR:ARROW:unsupported in Simplify\n";
709 os<<
"ERROR:LAMBDA:unsupported in Simplify\n";
713 os<<
"ERROR:TRANS_CLOSURE:unsupported in Simplify\n";
716 os<<
"ERROR:TYPEDECL:unsupported in Simplify\n";
724 if(first) first =
false;
732 DebugAssert(
false,
"TheoryUF::print: Unexpected expression: "
746 for(
int i=0, iend=e.
arity()-1; i<iend; ++i) {
747 if(first) first=
false;
752 os <<
" > " << e[e.
arity()-1];
757 os<<
"ERROR:LAMBDA:unsupported in TPTP\n";
761 os<<
"ERROR:TRANS_CLOSURE:unsupported in TPTP\n";
778 if(first) first =
false;
786 DebugAssert(
false,
"TheoryUF::print: Unexpected expression: "
804 for(
int i=0, iend=e.
arity()-1; i<iend; ++i) {
805 if(first) first=
false;
806 else os <<
"," <<
space;
809 os << push <<
")" <<
pop <<
pop;
824 const vector<Expr>& vars = e.
getVars();
827 for(vector<Expr>::const_iterator i=vars.begin(), iend=vars.end();
829 if(first) first =
false;
830 else os << push <<
"," <<
pop <<
space;
837 os << push <<
"): " <<
pushdag << push
847 if(first) first =
false;
848 else os <<
"," <<
space;
863 DebugAssert(
false,
"TheoryUF::print: Unexpected expression: "
873 throw SmtlibException(
"TheoryUF::print: Expected 2 or more arguments to ARROW");
878 bool oldDagFlag = os.
dagFlag(
false);
879 int iend = e.
arity();
880 if (e[iend-1].getKind() ==
BOOLEAN) --iend;
881 for(
int i=0; i<iend; ++i) {
882 if (i != 0) os <<
space;
898 throw SmtlibException(
"TheoryUF::print: Expected 2 or more arguments to ARROW");
902 bool oldDagFlag = os.
dagFlag(
false);
904 for(
int i = 0; i < e.
arity() - 1; ++i ) {
923 os <<
"(" <<
push <<
"ARROW";
924 for(
int i=0, iend=e.
arity(); i<iend; ++i)
936 else if(e[0].isString()) os << e[0].
getString();
941 os <<
"(" << push <<
"LAMBDA" <<
space;
942 const vector<Expr>& vars = e.
getVars();
945 for(vector<Expr>::const_iterator i=vars.begin(), iend=vars.end();
947 if(first) first =
false;
949 os <<
"(" << push << *i;
954 os << push <<
")" <<
pop <<
pop;
965 for (
int i=0, iend=e.
arity(); i<iend; ++i)
971 DebugAssert(
false,
"TheoryUF::print: Unexpected expression: "
985 for (
int i=1, iend=e.arity(); i<iend; ++i)
986 os <<
"," <<
space << e[i];
997 throw SmtlibException(
"TheoryUF::print: Unexpected expression for SPASS_LANG: "
1021 "TheoryUF::parseExprOp:\n e = "+e.
toString());
1029 for(; i!=iend; ++i) args.push_back(
parseExpr(*i));
1034 "Expected identifier");
1039 if (!
theoryCore()->getFlags()[
"old-func-syntax"].getBool()) {
1040 throw ParserException(
"You seem to be using the old syntax for function types.\n"
1041 "Please convert to the new syntax or run with +old-func-syntax");
1048 for (; i != iend; ++i) {
1052 else k.push_back(arg);
1072 "TRANS_CLOSURE expression\n"
1073 " (expected 3 arguments): "+e.
toString());
1074 const string& name = e[1][0].
getString();
1077 throw ParserException(
"Attempt to take transitive closure of unknown "
1085 vector<pair<string,Type> > vars;
1087 if(i->getKind() !=
RAW_LIST || i->arity() < 2)
1089 "expression: "+i->toString()+
1095 for(
int j=0, jend=i->arity()-1; j<jend; ++j) {
1096 if((*i)[j].getKind() !=
ID)
1098 " expression: "+(*i)[j].toString()+
1100 vars.push_back(pair<string,Type>((*i)[j][0].getString(), tp));
1104 vector<Expr> boundVars;
1105 for(vector<pair<string,Type> >::iterator i=vars.begin(), iend=vars.end();
1107 boundVars.push_back(
addBoundVar(i->first, i->second));
1121 for(; i!=iend; ++i) args.push_back(
parseExpr(*i));