/*****************************************************************************/
/*!
* \file theory_uf.cpp
*
* Author: Clark Barrett
*
* Created: Fri Jan 24 02:07:59 2003
*
* <hr>
*
* License to use, copy, modify, sell and/or distribute this software
* and its documentation for any purpose is hereby granted without
* royalty, subject to the terms and conditions defined in the \ref
* LICENSE file provided with this distribution.
*
* <hr>
*
*/
/*****************************************************************************/
#include "theory_uf.h"
#include "uf_proof_rules.h"
#include "typecheck_exception.h"
#include "parser_exception.h"
#include "smtlib_exception.h"
#include "command_line_flags.h"
#include "theory_core.h"
// HACK: include theory_records.h to access the TUPLE_TYPE kind
#include "theory_records.h"
using namespace std;
using namespace CVC3;
///////////////////////////////////////////////////////////////////////////////
// TheoryUF Public Methods //
///////////////////////////////////////////////////////////////////////////////
TheoryUF::TheoryUF(TheoryCore* core)//, bool useAckermann)
: Theory(core, "Uninterpreted Functions"),
d_applicationsInModel(core->getFlags()["applications"].getBool()),
d_funApplications(core->getCM()->getCurrentContext()),
d_funApplicationsIdx(core->getCM()->getCurrentContext(), 0)
// d_useAckermann(useAckermann)
{
d_rules = createProofRules();
// Register new local kinds with ExprManager
getEM()->newKind(TRANS_CLOSURE, "_TRANS_CLOSURE");
getEM()->newKind(OLD_ARROW, "_OLD_ARROW", true);
vector<int> kinds;
//TODO: should this stuff really be in theory_uf?
kinds.push_back(TYPEDECL);
kinds.push_back(LAMBDA);
kinds.push_back(ARROW);
kinds.push_back(OLD_ARROW);
kinds.push_back(UFUNC);
kinds.push_back(TRANS_CLOSURE);
registerTheory(this, kinds);
}
TheoryUF::~TheoryUF() {
delete d_rules;
}
//TODO: clean up transitive closure tables
// be sure to free CD objects
void TheoryUF::assertFact(const Theorem& e)
{
const Expr& expr = e.getExpr();
switch (expr.getKind()) {
case NOT:
break;
case APPLY:
if (expr.getOpExpr().computeTransClosure()) {
enqueueFact(d_rules->relToClosure(e));
}
else if (expr.getOpKind() == TRANS_CLOSURE) {
// const Expr& rel = expr.getFun();
DebugAssert(expr.isApply(), "Should be apply");
Expr rel = resolveID(expr.getOpExpr().getName());
DebugAssert(!rel.isNull(), "Expected known identifier");
DebugAssert(rel.isSymbol() && rel.getKind()==UFUNC && expr.arity()==2,
"Unexpected use of transitive closure: "+expr.toString());
// Insert into transitive closure table
ExprMap<TCMapPair*>::iterator i = d_transClosureMap.find(rel);
TCMapPair* pTable;
if (i == d_transClosureMap.end()) {
pTable = new TCMapPair();
d_transClosureMap[rel] = pTable;
}
else {
pTable = (*i).second;
}
ExprMap<CDList<Theorem>*>::iterator i2 = pTable->appearsFirstMap.find(expr[0]);
CDList<Theorem>* pList;
if (i2 == pTable->appearsFirstMap.end()) {
pList = new(true) CDList<Theorem>(theoryCore()->getCM()->getCurrentContext());
pTable->appearsFirstMap[expr[0]] = pList;
}
else {
pList = (*i2).second;
}
pList->push_back(e);
i2 = pTable->appearsSecondMap.find(expr[1]);
if (i2 == pTable->appearsSecondMap.end()) {
pList = new(true) CDList<Theorem>(theoryCore()->getCM()->getCurrentContext());
pTable->appearsSecondMap[expr[1]] = pList;
}
else {
pList = (*i2).second;
}
pList->push_back(e);
// Compute transitive closure with existing relations
size_t s,l;
i2 = pTable->appearsFirstMap.find(expr[1]);
if (i2 != pTable->appearsFirstMap.end()) {
pList = (*i2).second;
s = pList->size();
for (l = 0; l < s; ++l) {
enqueueFact(d_rules->relTrans(e,(*pList)[l]));
}
}
i2 = pTable->appearsSecondMap.find(expr[0]);
if (i2 != pTable->appearsSecondMap.end()) {
pList = (*i2).second;
s = pList->size();
for (l = 0; l < s; ++l) {
enqueueFact(d_rules->relTrans((*pList)[l],e));
}
}
}
break;
default:
break;
}
}
void TheoryUF::checkSat(bool fullEffort)
{
// Check for any unexpanded lambdas
for(; d_funApplicationsIdx < d_funApplications.size();
d_funApplicationsIdx = d_funApplicationsIdx + 1) {
const Expr& e = d_funApplications[d_funApplicationsIdx];
if(e.getOp().getExpr().isLambda()) {
IF_DEBUG(debugger.counter("Expanded lambdas (checkSat)")++);
enqueueFact(d_rules->applyLambda(e));
}
}
}
Theorem TheoryUF::rewrite(const Expr& e)
{
if (e.isApply()) {
const Expr& op = e.getOpExpr();
int opKind = op.getKind();
switch(opKind) {
case LAMBDA: {
Theorem res = d_rules->applyLambda(e);
// Simplify recursively
res = transitivityRule(res, simplify(res.getRHS()));
IF_DEBUG(debugger.counter("Expanded lambdas")++);
return res;
}
default: // A truly uninterpreted function
if (e.getType().isBool()) return reflexivityRule(e);
else return rewriteCC(e);
}
}
else {
e.setRewriteNormal();
return reflexivityRule(e);
}
}
void TheoryUF::setup(const Expr& e)
{
if (e.getKind() != APPLY) return;
// if (d_useAckermann) {
// Theorem thm = getCommonRules()->varIntroSkolem(e);
// theoryCore()->addToVarDB(thm.getRHS());
// enqueueFact(thm);
// }
// else {
setupCC(e);
// }
// Add this function application for concrete model generation
TRACE("model", "TheoryUF: add function application ", e, "");
d_funApplications.push_back(e);
}
void TheoryUF::update(const Theorem& e, const Expr& d)
{
/*
int k, ar(d.arity());
const Theorem& dEQdsig = d.getSig();
if (!dEQdsig.isNull()) {
Expr dsig = dEQdsig.getRHS();
Theorem thm = updateHelper(d);
const Expr& sigNew = thm.getRHS();
if (sigNew == dsig) return;
dsig.setRep(Theorem());
const Theorem& repEQsigNew = sigNew.getRep();
if (!repEQsigNew.isNull()) {
d.setSig(Theorem());
enqueueFact(transitivityRule(repEQsigNew, symmetryRule(thm)));
}
else {
for (k = 0; k < ar; ++k) {
if (sigNew[k] != dsig[k]) {
sigNew[k].addToNotify(this, d);
}
}
d.setSig(thm);
sigNew.setRep(thm);
if (d_compute_trans_closure && d.getKind() == APPLY &&
d.arity() == 2 && findExpr(d).isTrue()) {
thm = iffTrueElim(transitivityRule(symmetryRule(thm),find(d)));
enqueueFact(d_rules->relToClosure(thm));
}
}
}
*/
// Record the original signature
const Theorem& dEQdsig = d.getSig();
if (!dEQdsig.isNull()) {
const Expr& dsig = dEQdsig.getRHS();
Theorem thm = updateHelper(d);
const Expr& sigNew = thm.getRHS();
if (sigNew == dsig) {
// TRACE_MSG("facts update", "updateCC["+getName()+"]() [no change] => }");
return;
}
dsig.setRep(Theorem());
const Theorem& repEQsigNew = sigNew.getRep();
if (!repEQsigNew.isNull()) {
d.setSig(Theorem());
enqueueFact(transitivityRule(repEQsigNew, symmetryRule(thm)));
}
else if (d.getType().isBool()) {
d.setSig(Theorem());
enqueueFact(thm);
}
else {
int k, ar(d.arity());
for (k = 0; k < ar; ++k) {
if (sigNew[k] != dsig[k]) {
sigNew[k].addToNotify(this, d);
}
}
d.setSig(thm);
sigNew.setRep(thm);
if (dsig != sigNew && d.isApply() && findExpr(d).isTrue()) {
if (d.getOpExpr().computeTransClosure()) {
thm = getCommonRules()->iffTrueElim(transitivityRule(symmetryRule(thm),
find(d)));
enqueueFact(d_rules->relToClosure(thm));
}
else if (d.getOpKind() == TRANS_CLOSURE) {
thm = getCommonRules()->iffTrueElim(transitivityRule(symmetryRule(thm),
find(d)));
enqueueFact(thm);
}
}
}
}
}
void TheoryUF::checkType(const Expr& e)
{
switch (e.getKind()) {
case ARROW: {
if (e.arity() < 2) throw Exception
("Function type needs at least two arguments"
+e.toString());
Expr::iterator i = e.begin(), iend = e.end();
for (; i != iend; ) {
Type t(*i);
++i;
if (i == iend && t.isBool()) break;
if (t.isBool()) throw Exception
("Function argument types must be non-Boolean: "
+e.toString());
if (t.isFunction()) throw Exception
("Function domain or range types cannot be functions: "
+e.toString());
}
break;
}
case TYPEDECL: {
break;
}
default:
DebugAssert(false, "Unexpected kind in TheoryUF::checkType"
+getEM()->getKindName(e.getKind()));
}
}
void TheoryUF::computeType(const Expr& e)
{
switch (e.getKind()) {
case LAMBDA: {
vector<Type> args;
const vector<Expr>& vars = e.getVars();
DebugAssert(vars.size() > 0,
"TheorySimulate::computeType("+e.toString()+")");
for(vector<Expr>::const_iterator i=vars.begin(), iend=vars.end();
i!=iend; ++i)
args.push_back((*i).getType());
e.setType(Type::funType(args, e.getBody().getType()));
break;
}
case APPLY: {
theoryOf(APPLY)->computeType(e);
break;
}
case TRANS_CLOSURE: {
DebugAssert(e.isSymbol(), "Expected symbol");
Expr funExpr = resolveID(e.getName());
if (funExpr.isNull()) {
throw TypecheckException
("Attempt to take transitive closure of unknown id: "
+e.getName());
}
Type funType = funExpr.getType();
if(!funType.isFunction()) {
throw TypecheckException
("Attempt to take transitive closure of non-function:\n\n"
+funExpr.toString() + "\n\n which has type: "
+funType.toString());
}
if(funType.arity()!=3) {
throw TypecheckException
("Attempt to take transitive closure of non-binary function:\n\n"
+funExpr.toString() + "\n\n which has type: "
+funType.toString());
}
if (!funType[2].isBool()) {
throw TypecheckException
("Attempt to take transitive closure of function:\n\n"
+funExpr.toString() + "\n\n which does not return BOOLEAN");
}
e.setType(funType);
break;
}
default:
DebugAssert(false,"Unexpected type: "+e.toString());
break;
}
}
Type TheoryUF::computeBaseType(const Type& t) {
const Expr& e = t.getExpr();
switch(e.getKind()) {
case ARROW: {
DebugAssert(e.arity() > 0, "Expected non-empty ARROW");
vector<Expr> kids;
for(Expr::iterator i=e.begin(), iend=e.end(); i!=iend; ++i) {
kids.push_back(getBaseType(Type(*i)).getExpr());
}
return Type(Expr(e.getOp(), kids));
}
case TYPEDECL: return t;
default:
DebugAssert(false,
"TheoryUF::computeBaseType("+t.toString()+")");
return t;
}
}
void TheoryUF::computeModelTerm(const Expr& e, std::vector<Expr>& v) {
for(CDList<Expr>::const_iterator i=d_funApplications.begin(),
iend=d_funApplications.end(); i!=iend; ++i) {
if((*i).isApply() && (*i).getOp().getExpr() == e) {
// Add both the function application
// getModelTerm(*i, v);
v.push_back(*i);
// and the arguments to the model terms. Reason: the argument
// to the function better be a concrete value, and it might not
// necessarily be in the current list of model terms.
for(Expr::iterator j=(*i).begin(), jend=(*i).end(); j!=jend; ++j)
// getModelTerm(*j, v);
v.push_back(*j);
}
}
}
void TheoryUF::computeModel(const Expr& e, std::vector<Expr>& vars) {
// Repeat the same search for applications of e as in
// computeModelTerm(), but this time get the concrete values of the
// arguments, and return the applications of e to concrete values in
// vars.
// We'll assign 'e' a value later.
vars.push_back(e);
// Map of f(c) to val for concrete values of c and val
ExprHashMap<Expr> appls;
for(CDList<Expr>::const_iterator i=d_funApplications.begin(),
iend=d_funApplications.end(); i!=iend; ++i) {
if((*i).isApply() && (*i).getOp().getExpr() == e) {
// Update all arguments with concrete values
vector<Theorem> thms;
vector<unsigned> changed;
for(int j=0; j<(*i).arity(); ++j) {
Theorem asst(getModelValue((*i)[j]));
if(asst.getLHS()!=asst.getRHS()) {
thms.push_back(asst);
changed.push_back(j);
}
}
Expr var;
if(changed.size()>0) {
// Arguments changed. Compute the new application, and assign
// it a concrete value
Theorem subst = substitutivityRule(*i, changed, thms);
assignValue(transitivityRule(symmetryRule(subst), getModelValue(*i)));
var = subst.getRHS();
} else
var = *i;
if(d_applicationsInModel) vars.push_back(var);
// Record it in the map
appls[var] = getModelValue(var).getRHS();
}
}
// Create a LAMBDA expression for e
if(appls.size()==0) { // Leave it fully uninterpreted
assignValue(reflexivityRule(e));
} else {
// Bound vars
vector<Expr> args;
Type tp(e.getType());
static unsigned count(0);
DebugAssert(tp.isFunction(), "TheoryUF::computeModel("+e.toString()
+" : "+tp.toString()+")");
for(int i=0, iend=tp.arity()-1; i<iend; ++i) {
Expr v = getEM()->newBoundVarExpr("uf", int2string(count++));
v.setType(tp[i]);
args.push_back(v);
}
DebugAssert(args.size()>0, "TheoryUF::computeModel()");
ExprHashMap<Expr>::iterator i=appls.begin(), iend=appls.end();
DebugAssert(i!=iend, "TheoryUF::computeModel(): empty appls hash");
// Use one of the concrete values as a default
Expr res((*i).second); ++i;
for(; i!=iend; ++i) {
// Optimization: if the current value is the same as that of the
// next application, skip this case; i.e. keep 'res' instead of
// building ite(cond, res, res).
if((*i).second == res) continue;
// Create an ITE condition
Expr cond;
vector<Expr> eqs;
for(int j=0, jend=args.size(); j<jend; ++j)
eqs.push_back(args[j].eqExpr((*i).first[j]));
if(eqs.size()==1)
cond = eqs[0];
else
cond = andExpr(eqs);
// Create an ITE
res = cond.iteExpr((*i).second, res);
}
res = lambdaExpr(args, res);
assignValue(e, res);
}
}
Expr TheoryUF::computeTCC(const Expr& e)
{
switch (e.getKind()) {
case APPLY: {
// Compute subtype predicates from the domain types applied to
// the corresponding arguments. That is, if f: (T0,..,Tn)->T,
// and e = f(e0,...,en), then the TCC is
//
// pred_T0(e0) & ... & pred_Tn(en) & TCC(e),
//
// where the last TCC(e) is the conjunction of TCCs for the
// arguments, which ensures that all arguments are defined.
//
// If the operator is a lambda-expression, compute the TCC for
// the beta-reduced expression. We do this in a somewhat sneaky
// but an efficient way: first, compute TCC of the op.body
// (which depends on the bound vars), then wrap that into
// lambda, and apply it to the arguments:
//
// (LAMBDA(x0...xn): TCC(op.body)) (e0 ... en)
//
// The reason it is more efficient is that TCC(op.body) is cached,
// and doesn't change with the arguments.
vector<Expr> preds;
preds.push_back(Theory::computeTCC(e));
DebugAssert(e.isApply(), "Should be application");
Expr op(e.getOp().getExpr());
Type funType(op.getType());
DebugAssert(funType.isFunction() || funType.isBool(),
"TheoryUF::computeTCC(): funType = "
+funType.toString());
if(funType.isFunction()) {
DebugAssert(funType.arity() == e.arity()+1,
"TheoryUF::computeTCC(): funType = "
+funType.toString()+"\n e = "+e.toString());
for(int i=0, iend=e.arity(); i<iend; ++i) {
// Optimization: if the type of the formal argument is
// exactly the same as the type of the actual, then skip the
// type predicate for that argument
if(funType[i] != e[i].getType())
preds.push_back(getTypePred(funType[i], e[i]));
}
}
// Now strip off all the LETDECL
while(op.getKind()==LETDECL) op = op[1];
// and add a TCC for the lambda-expression
if(op.isLambda()) {
preds.push_back(Expr(lambdaExpr(op.getVars(),
getTCC(op.getBody())).mkOp(),
e.getKids()));
}
return rewriteAnd(andExpr(preds)).getRHS();
}
case LAMBDA:
return trueExpr();
default:
DebugAssert(false,"Unexpected type: "+e.toString());
return trueExpr();
}
}
///////////////////////////////////////////////////////////////////////////////
// Pretty-printing //
///////////////////////////////////////////////////////////////////////////////
ExprStream& TheoryUF::print(ExprStream& os, const Expr& e) {
switch(os.lang()) {
case SIMPLIFY_LANG:
switch(e.getKind()) {
case OLD_ARROW:
case ARROW:
os<<"ERROR:ARROW:unsupported in Simplify\n";
break;
case LAMBDA: {
os<<"ERROR:LAMBDA:unsupported in Simplify\n";
break;
}
case TRANS_CLOSURE:
os<<"ERROR:TRANS_CLOSURE:unsupported in Simplify\n";
break;
case TYPEDECL:
os<<"ERROR:TYPEDECL:unsupported in Simplify\n";
break;
case UFUNC:
case APPLY:
if(e.isApply()) os << "(" << e.getOp().getExpr()<<" ";
if(e.arity() > 0) {
bool first(true);
for (Expr::iterator i=e.begin(), iend=e.end(); i!=iend; ++i) {
if(first) first = false;
else os << " " ;
os << *i;
}
os << ")";
}
break;
default: {
DebugAssert(false, "TheoryUF::print: Unexpected expression: "
+getEM()->getKindName(e.getKind()));
}
}
break; // end of case SIMPLIFY_LANGUAGE
case PRESENTATION_LANG:
switch(e.getKind()) {
case OLD_ARROW:
case ARROW:
if(e.arity() < 2) e.printAST(os);
else {
if(e.arity() == 2)
os << e[0];
else {
os << "(" << push;
bool first(true);
for(int i=0, iend=e.arity()-1; i<iend; ++i) {
if(first) first=false;
else os << "," << space;
os << e[i];
}
os << push << ")" << pop << pop;
}
os << space << "-> " << space << e[e.arity()-1];
}
break;
case TYPEDECL:
// If it's straight from the parser, we may have several type
// names in one declaration. Print these in LISP format.
// Otherwise, print the name of the type.
if(e.arity() != 1) e.printAST(os);
else os << e[0].getString();
break;
case LAMBDA: {
DebugAssert(e.isLambda(), "Expected Lambda");
os << "(" << push << "LAMBDA" << space << push;
const vector<Expr>& vars = e.getVars();
bool first(true);
os << "(" << push;
for(vector<Expr>::const_iterator i=vars.begin(), iend=vars.end();
i!=iend; ++i) {
if(first) first = false;
else os << push << "," << pop << space;
os << *i;
// The lambda Expr may be in a raw parsed form, in which case
// the type is not assigned yet
if(i->isVar())
os << ":" << space << pushdag << (*i).getType() << popdag;
}
os << push << "): " << pushdag << push
<< e.getBody() << push << ")";
break;
}
case APPLY:
os << e.getOpExpr();
if(e.arity() > 0) {
os << "(" << push;
bool first(true);
for (Expr::iterator i=e.begin(), iend=e.end(); i!=iend; ++i) {
if(first) first = false;
else os << "," << space;
os << *i;
}
os << push << ")";
}
break;
case TRANS_CLOSURE:
DebugAssert(e.isSymbol(), "Expected symbol");
os << e.getName() << "*";
break;
case UFUNC:
DebugAssert(e.isSymbol(), "Expected symbol");
os << e.getName();
break;
default: {
DebugAssert(false, "TheoryUF::print: Unexpected expression: "
+getEM()->getKindName(e.getKind()));
}
}
break; // end of case PRESENTATION_LANGUAGE
case SMTLIB_LANG:
switch(e.getKind()) {
case OLD_ARROW:
case ARROW: {
if(e.arity() < 2) {
throw SmtlibException("TheoryUF::print: Expected 2 or more arguments to ARROW");
// e.print(os);
}
d_theoryUsed = true;
os << push;
int iend = e.arity();
if (e[iend-1].getKind() == BOOLEAN) --iend;
for(int i=0; i<iend; ++i) {
if (i != 0) os << space;
os << e[i];
}
break;
}
case TYPEDECL:
if (e.arity() == 1 && e[0].isString()) {
os << e[0].getString();
break;
}
// If it's straight from the parser, we may have several type
// names in one declaration. Print these in LISP format.
// Otherwise, print the name of the type.
throw SmtlibException("TheoryUF::print: TYPEDECL not supported");
// if(e.arity() != 1) e.print(os);
// else if(e[0].isString()) os << e[0].getString();
// else e[0].print(os);
break;
case APPLY:
if (e.arity() == 0) os << e.getOp().getExpr();
else {
os << "(" << push << e.getOp().getExpr();
for (int i=0, iend=e.arity(); i<iend; ++i)
os << space << e[i];
if (e.getOpKind() == TRANS_CLOSURE) {
os << space << ":transclose";
}
os << push << ")";
}
break;
case TRANS_CLOSURE:
os << e.getName();
break;
case UFUNC:
DebugAssert(e.isSymbol(), "Expected symbol");
os << e.getName();
break;
default: {
DebugAssert(false, "TheoryUF::print: SMTLIB_LANG: Unexpected expression: "
+getEM()->getKindName(e.getKind()));
}
}
break; // End of SMT_LIB
case LISP_LANG:
switch(e.getKind()) {
case OLD_ARROW:
case ARROW:
if(e.arity() < 2) e.printAST(os);
os << "(" << push << "ARROW";
for(int i=0, iend=e.arity(); i<iend; ++i)
os << space << e[i];
os << push << ")";
break;
case TRANS_CLOSURE:
e.printAST(os);
break;
case TYPEDECL:
// If it's straight from the parser, we may have several type
// names in one declaration. Print these in LISP format.
// Otherwise, print the name of the type.
if(e.arity() != 1) e.printAST(os);
else if(e[0].isString()) os << e[0].getString();
else e[0].print(os);
break;
case LAMBDA: {
DebugAssert(e.isLambda(), "Expected LAMBDA");
os << "(" << push << "LAMBDA" << space;
const vector<Expr>& vars = e.getVars();
bool first(true);
os << "(" << push;
for(vector<Expr>::const_iterator i=vars.begin(), iend=vars.end();
i!=iend; ++i) {
if(first) first = false;
else os << space;
os << "(" << push << *i;
// The expression may be in a raw parsed form, in which case
// the type is not assigned yet
if(i->isVar())
os << space << pushdag << (*i).getType() << popdag;
os << push << ")" << pop << pop;
}
os << push << ")" << pop << pop << pushdag
<< e.getBody() << push << ")";
break;
}
case APPLY:
DebugAssert(e.isApply(), "Expected Apply");
if (e.arity() == 0) os << e.getOp().getExpr();
else {
os << "(" << push << e.getOp().getExpr();
for (int i=0, iend=e.arity(); i<iend; ++i)
os << space << e[i];
os << push << ")";
}
break;
default: {
DebugAssert(false, "TheoryUF::print: Unexpected expression: "
+getEM()->getKindName(e.getKind()));
}
}
break; // End of LISP_LANG
default:
// Print the top node in the default format, continue with
// pretty-printing for children.
e.printAST(os);
break;
}
return os;
}
//////////////////////////////////////////////////////////////////////////////
//parseExprOp:
//translating special Exprs to regular EXPR??
///////////////////////////////////////////////////////////////////////////////
Expr
TheoryUF::parseExprOp(const Expr& e) {
// If the expression is not a list, it must have been already
// parsed, so just return it as is.
if(RAW_LIST != e.getKind()) return e;
DebugAssert(e.arity() > 0,
"TheoryUF::parseExprOp:\n e = "+e.toString());
const Expr& c1 = e[0][0];
int kind = getEM()->getKind(c1.getString());
switch(kind) {
case OLD_ARROW: {
if (!theoryCore()->getFlags()["old-func-syntax"].getBool()) {
throw ParserException("You seem to be using the old syntax for function types.\n"
"Please convert to the new syntax or run with +old-func-syntax");
}
DebugAssert(e.arity()==3,"Expected arity 3 in OLD_ARROW");
Expr arg = parseExpr(e[1]);
vector<Expr> k;
if (arg.getOpKind() == TUPLE_TYPE) {
Expr::iterator i = arg.begin(), iend=arg.end();
for (; i != iend; ++i) {
k.push_back(*i);
}
}
else k.push_back(arg);
k.push_back(parseExpr(e[2]));
return Expr(ARROW, k);
}
case ARROW:
case TYPEDECL: {
vector<Expr> k;
Expr::iterator i = e.begin(), iend=e.end();
// Skip first element of the vector of kids in 'e'.
// The first element is the operator.
++i;
// Parse the kids of e and push them into the vector 'k'
for(; i!=iend; ++i)
k.push_back(parseExpr(*i));
return Expr(kind, k, e.getEM());
break;
}
case TRANS_CLOSURE: {
if(e.arity() != 4)
throw ParserException("Wrong number of arguments to "
"TRANS_CLOSURE expression\n"
" (expected 3 arguments): "+e.toString());
const string& name = e[1][0].getString();
Expr funExpr = resolveID(name);
if (funExpr.isNull())
throw ParserException("Attempt to take transitive closure of unknown "
"predicate"+name);
return transClosureExpr(name, parseExpr(e[2]), parseExpr(e[3]));
}
case LAMBDA: { // (LAMBDA ((v1 ... vn tp1) ...) body)
if(!(e.arity() == 3 && e[1].getKind() == RAW_LIST && e[1].arity() > 0))
throw ParserException("Bad LAMBDA expression: "+e.toString());
// Iterate through the groups of bound variables
vector<pair<string,Type> > vars; // temporary stack of bound variables
for(Expr::iterator i=e[1].begin(), iend=e[1].end(); i!=iend; ++i) {
if(i->getKind() != RAW_LIST || i->arity() < 2)
throw ParserException("Bad variable declaration block in LAMBDA "
"expression: "+i->toString()+
"\n e = "+e.toString());
// Iterate through individual bound vars in the group. The
// last element is the type, which we have to rebuild and
// parse, since it is used in the creation of bound variables.
Type tp(parseExpr((*i)[i->arity()-1]));
for(int j=0, jend=i->arity()-1; j<jend; ++j) {
if((*i)[j].getKind() != ID)
throw ParserException("Bad variable declaration in LAMBDA"
" expression: "+(*i)[j].toString()+
"\n e = "+e.toString());
vars.push_back(pair<string,Type>((*i)[j][0].getString(), tp));
}
}
// Create all the bound vars and save them in a vector
vector<Expr> boundVars;
for(vector<pair<string,Type> >::iterator i=vars.begin(), iend=vars.end();
i!=iend; ++i)
boundVars.push_back(addBoundVar(i->first, i->second));
// Rebuild the body
Expr body(parseExpr(e[2]));
// Build the resulting Expr as (LAMBDA (vars) body)
return lambdaExpr(boundVars, body);
break;
}
// case APPLY:
default: { // Application of an uninterpreted function
if(e.arity() < 2)
throw ParserException("Bad function application: "+e.toString());
Expr::iterator i=e.begin(), iend=e.end();
Expr op(parseExpr(*i)); ++i;
vector<Expr> args;
for(; i!=iend; ++i) args.push_back(parseExpr(*i));
return Expr(op.mkOp(), args);
}
}
return e;
}
Expr TheoryUF::lambdaExpr(const vector<Expr>& vars, const Expr& body) {
return getEM()->newClosureExpr(LAMBDA, vars, body);
}
Expr TheoryUF::transClosureExpr(const std::string& name, const Expr& e1,
const Expr& e2) {
return Expr(getEM()->newSymbolExpr(name, TRANS_CLOSURE).mkOp(), e1, e2);
}
syntax highlighted by Code2HTML, v. 0.9.1