PARSER_STATE->checkDeclaration(*i, CHECK_UNDECLARED, SYM_VARIABLE);
api::Term func = PARSER_STATE->mkVar(
*i,
- t.getType(),
+ api::Sort(PARSER_STATE->getSolver(), t.getType()),
ExprManager::VAR_FLAG_GLOBAL | ExprManager::VAR_FLAG_DEFINED);
PARSER_STATE->defineVar(*i, f);
Command* decl =
}
const Datatype & dt = ((DatatypeType)t.getType()).getDatatype();
f2 = SOLVER->mkTerm(
- api::APPLY_SELECTOR, api::Term(dt[0][k].getSelector()), f);
+ api::APPLY_SELECTOR,
+ api::Term(PARSER_STATE->getSolver(), dt[0][k].getSelector()),
+ f);
}
( ( arrayStore[f2]
| DOT ( tupleStore[f2]
}
const Datatype & dt = ((DatatypeType)t.getType()).getDatatype();
f2 = SOLVER->mkTerm(
- api::APPLY_SELECTOR, api::Term(dt[0][id].getSelector()), f);
+ api::APPLY_SELECTOR,
+ api::Term(PARSER_STATE->getSolver(), dt[0][id].getSelector()),
+ f);
}
( ( arrayStore[f2]
| DOT ( tupleStore[f2]
PARSER_STATE->parseError(std::string("no such field `") + id + "' in record");
}
const Datatype & dt = ((DatatypeType)type.getType()).getDatatype();
- f = SOLVER->mkTerm(api::APPLY_SELECTOR,api::Term(dt[0][id].getSelector()), f);
+ f = SOLVER->mkTerm(
+ api::APPLY_SELECTOR,
+ api::Term(PARSER_STATE->getSolver(), dt[0][id].getSelector()),
+ f);
}
| k=numeral
{
PARSER_STATE->parseError(ss.str());
}
const Datatype & dt = ((DatatypeType)type.getType()).getDatatype();
- f = SOLVER->mkTerm(api::APPLY_SELECTOR,api::Term(dt[0][k].getSelector()), f);
+ f = SOLVER->mkTerm(
+ api::APPLY_SELECTOR,
+ api::Term(PARSER_STATE->getSolver(), dt[0][k].getSelector()),
+ f);
}
)
)*
| ABS_TOK LPAREN formula[f] RPAREN
{ f = MK_TERM(CVC4::api::ABS, f); }
| DIVISIBLE_TOK LPAREN formula[f] COMMA n=numeral RPAREN
- { f = MK_TERM(SOLVER->mkOp(CVC4::api::DIVISIBLE,n), f); }
+ { f = MK_TERM(SOLVER->mkOp(CVC4::api::DIVISIBLE, n), f); }
| DISTINCT_TOK LPAREN
formula[f] { args.push_back(f); }
( COMMA formula[f] { args.push_back(f); } )* RPAREN
)
( typeAscription[f, t]
{
- f = PARSER_STATE->applyTypeAscription(f,t).getExpr();
+ f = PARSER_STATE->applyTypeAscription(f,t);
}
)?
;
args.push_back(f);
types.push_back(f.getSort());
api::Sort t = SOLVER->mkTupleSort(types);
- const Datatype& dt = ((DatatypeType)t.getType()).getDatatype();
- args.insert( args.begin(), api::Term(dt[0].getConstructor()) );
+ const Datatype& dt = Datatype(((DatatypeType)t.getType()).getDatatype());
+ args.insert(args.begin(),
+ api::Term(PARSER_STATE->getSolver(), dt[0].getConstructor()));
f = MK_TERM(api::APPLY_CONSTRUCTOR, args);
}
| IDEN_TOK LPAREN formula[f] RPAREN
}
api::Sort dtype = SOLVER->mkTupleSort(types);
const Datatype& dt = ((DatatypeType)dtype.getType()).getDatatype();
- args.insert( args.begin(), dt[0].getConstructor() );
+ args.insert(
+ args.begin(),
+ api::Term(PARSER_STATE->getSolver(), dt[0].getConstructor()));
f = MK_TERM(api::APPLY_CONSTRUCTOR, args);
}
}
{ std::vector<api::Sort> types;
api::Sort dtype = SOLVER->mkTupleSort(types);
const Datatype& dt = ((DatatypeType)dtype.getType()).getDatatype();
- f = MK_TERM(api::APPLY_CONSTRUCTOR, api::Term(dt[0].getConstructor())); }
+ f = MK_TERM(api::APPLY_CONSTRUCTOR,
+ api::Term(PARSER_STATE->getSolver(), dt[0].getConstructor()));
+ }
/* empty record literal */
| PARENHASH HASHPAREN
api::Sort dtype = SOLVER->mkRecordSort(
std::vector<std::pair<std::string, api::Sort>>());
const Datatype& dt = ((DatatypeType)dtype.getType()).getDatatype();
- f = MK_TERM(api::APPLY_CONSTRUCTOR, api::Term(dt[0].getConstructor()));
+ f = MK_TERM(api::APPLY_CONSTRUCTOR,
+ api::Term(PARSER_STATE->getSolver(), dt[0].getConstructor()));
}
/* empty set literal */
| LBRACE RBRACE
}
api::Sort dtype = SOLVER->mkRecordSort(typeIds);
const Datatype& dt = ((DatatypeType)dtype.getType()).getDatatype();
- args.insert( args.begin(), dt[0].getConstructor() );
+ args.insert(args.begin(),
+ api::Term(PARSER_STATE->getSolver(), dt[0].getConstructor()));
f = MK_TERM(api::APPLY_CONSTRUCTOR, args);
}