summaryrefslogtreecommitdiff
path: root/src/parser
diff options
context:
space:
mode:
Diffstat (limited to 'src/parser')
-rw-r--r--src/parser/cvc/Cvc.g43
-rw-r--r--src/parser/parser.cpp55
-rw-r--r--src/parser/parser.h12
-rw-r--r--src/parser/smt2/Smt2.g18
-rw-r--r--src/parser/smt2/smt2.cpp13
-rw-r--r--src/parser/tptp/Tptp.g4
6 files changed, 84 insertions, 61 deletions
diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index 8e4152e2e..fdb6a081c 100644
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -1159,7 +1159,7 @@ declareVariables[std::unique_ptr<CVC4::Command>* cmd, CVC4::api::Sort& t,
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 =
@@ -1654,7 +1654,9 @@ tupleStore[CVC4::api::Term& f]
}
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]
@@ -1687,7 +1689,9 @@ recordStore[CVC4::api::Term& f]
}
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]
@@ -1831,7 +1835,10 @@ postfixTerm[CVC4::api::Term& f]
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
{
@@ -1846,7 +1853,10 @@ postfixTerm[CVC4::api::Term& f]
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);
}
)
)*
@@ -1857,7 +1867,7 @@ postfixTerm[CVC4::api::Term& 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
@@ -1868,7 +1878,7 @@ postfixTerm[CVC4::api::Term& f]
)
( typeAscription[f, t]
{
- f = PARSER_STATE->applyTypeAscription(f,t).getExpr();
+ f = PARSER_STATE->applyTypeAscription(f,t);
}
)?
;
@@ -1885,8 +1895,9 @@ relationTerm[CVC4::api::Term& f]
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
@@ -2136,7 +2147,9 @@ simpleTerm[CVC4::api::Term& f]
}
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);
}
}
@@ -2146,7 +2159,9 @@ simpleTerm[CVC4::api::Term& f]
{ 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
@@ -2154,7 +2169,8 @@ simpleTerm[CVC4::api::Term& f]
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
@@ -2252,7 +2268,8 @@ simpleTerm[CVC4::api::Term& f]
}
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);
}
diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index c860d14c7..b24f9ae9d 100644
--- a/src/parser/parser.cpp
+++ b/src/parser/parser.cpp
@@ -82,14 +82,9 @@ api::Term Parser::getSymbol(const std::string& name, SymbolType type)
{
checkDeclaration(name, CHECK_DECLARED, type);
assert(isDeclared(name, type));
-
- if (type == SYM_VARIABLE) {
- // Functions share var namespace
- return d_symtab->lookup(name);
- }
-
- assert(false); // Unhandled(type);
- return Expr();
+ assert(type == SYM_VARIABLE);
+ // Functions share var namespace
+ return api::Term(d_solver, d_symtab->lookup(name));
}
api::Term Parser::getVariable(const std::string& name)
@@ -166,7 +161,7 @@ api::Sort Parser::getSort(const std::string& name)
{
checkDeclaration(name, CHECK_DECLARED, SYM_SORT);
assert(isDeclared(name, SYM_SORT));
- api::Sort t = api::Sort(d_symtab->lookupType(name));
+ api::Sort t = api::Sort(d_solver, d_symtab->lookupType(name));
return t;
}
@@ -175,8 +170,8 @@ api::Sort Parser::getSort(const std::string& name,
{
checkDeclaration(name, CHECK_DECLARED, SYM_SORT);
assert(isDeclared(name, SYM_SORT));
- api::Sort t =
- api::Sort(d_symtab->lookupType(name, api::sortVectorToTypes(params)));
+ api::Sort t = api::Sort(
+ d_solver, d_symtab->lookupType(name, api::sortVectorToTypes(params)));
return t;
}
@@ -237,7 +232,8 @@ std::vector<api::Term> Parser::bindBoundVars(
std::vector<api::Term> vars;
for (std::pair<std::string, api::Sort>& i : sortedVarNames)
{
- vars.push_back(bindBoundVar(i.first, i.second.getType()));
+ vars.push_back(
+ bindBoundVar(i.first, api::Sort(d_solver, i.second.getType())));
}
return vars;
}
@@ -251,7 +247,7 @@ api::Term Parser::mkAnonymousFunction(const std::string& prefix,
}
stringstream name;
name << prefix << "_anon_" << ++d_anonymousFunctionCount;
- return mkVar(name.str(), type.getType(), flags);
+ return mkVar(name.str(), api::Sort(d_solver, type.getType()), flags);
}
std::vector<api::Term> Parser::bindVars(const std::vector<std::string> names,
@@ -334,7 +330,8 @@ void Parser::defineParameterizedType(const std::string& name,
api::Sort Parser::mkSort(const std::string& name, uint32_t flags)
{
Debug("parser") << "newSort(" << name << ")" << std::endl;
- api::Sort type = d_solver->getExprManager()->mkSort(name, flags);
+ api::Sort type =
+ api::Sort(d_solver, d_solver->getExprManager()->mkSort(name, flags));
defineType(
name,
type,
@@ -348,8 +345,9 @@ api::Sort Parser::mkSortConstructor(const std::string& name,
{
Debug("parser") << "newSortConstructor(" << name << ", " << arity << ")"
<< std::endl;
- api::Sort type =
- d_solver->getExprManager()->mkSortConstructor(name, arity, flags);
+ api::Sort type = api::Sort(
+ d_solver,
+ d_solver->getExprManager()->mkSortConstructor(name, arity, flags));
defineType(
name,
vector<api::Sort>(arity),
@@ -379,8 +377,10 @@ api::Sort Parser::mkUnresolvedTypeConstructor(
{
Debug("parser") << "newSortConstructor(P)(" << name << ", " << params.size()
<< ")" << std::endl;
- api::Sort unresolved = d_solver->getExprManager()->mkSortConstructor(
- name, params.size(), ExprManager::SORT_FLAG_PLACEHOLDER);
+ api::Sort unresolved =
+ api::Sort(d_solver,
+ d_solver->getExprManager()->mkSortConstructor(
+ name, params.size(), ExprManager::SORT_FLAG_PLACEHOLDER));
defineType(name, params, unresolved);
api::Sort t = getSort(name, params);
d_unresolved.insert(unresolved);
@@ -588,11 +588,12 @@ api::Term Parser::applyTypeAscription(api::Term t, api::Sort s)
Expr e = t.getExpr();
const DatatypeConstructor& dtc =
Datatype::datatypeOf(e)[Datatype::indexOf(e)];
- t = api::Term(em->mkExpr(
- kind::APPLY_TYPE_ASCRIPTION,
- em->mkConst(
- AscriptionType(dtc.getSpecializedConstructorType(s.getType()))),
- e));
+ t = api::Term(
+ d_solver,
+ em->mkExpr(kind::APPLY_TYPE_ASCRIPTION,
+ em->mkConst(AscriptionType(
+ dtc.getSpecializedConstructorType(s.getType()))),
+ e));
}
// the type of t does not match the sort s by design (constructor type
// vs datatype type), thus we use an alternative check here.
@@ -624,7 +625,7 @@ api::Term Parser::mkVar(const std::string& name,
uint32_t flags)
{
return api::Term(
- d_solver->getExprManager()->mkVar(name, type.getType(), flags));
+ d_solver, d_solver->getExprManager()->mkVar(name, type.getType(), flags));
}
//!!!!!!!!!!! temporary
@@ -892,16 +893,16 @@ std::vector<unsigned> Parser::processAdHocStringEsc(const std::string& s)
return str;
}
-Expr Parser::mkStringConstant(const std::string& s)
+api::Term Parser::mkStringConstant(const std::string& s)
{
ExprManager* em = d_solver->getExprManager();
if (language::isInputLang_smt2_6(em->getOptions().getInputLanguage()))
{
- return d_solver->mkString(s, true).getExpr();
+ return api::Term(d_solver, d_solver->mkString(s, true).getExpr());
}
// otherwise, we must process ad-hoc escape sequences
std::vector<unsigned> str = processAdHocStringEsc(s);
- return d_solver->mkString(str).getExpr();
+ return api::Term(d_solver, d_solver->mkString(str).getExpr());
}
} /* CVC4::parser namespace */
diff --git a/src/parser/parser.h b/src/parser/parser.h
index 7941cfdd5..b5dc83902 100644
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -808,7 +808,7 @@ public:
inline SymbolTable* getSymbolTable() const {
return d_symtab;
}
-
+
//------------------------ operator overloading
/** is this function overloaded? */
bool isOverloadedFunction(api::Term fun)
@@ -822,7 +822,8 @@ public:
*/
api::Term getOverloadedConstantForType(const std::string& name, api::Sort t)
{
- return d_symtab->getOverloadedConstantForType(name, t.getType());
+ return api::Term(d_solver,
+ d_symtab->getOverloadedConstantForType(name, t.getType()));
}
/**
@@ -833,8 +834,9 @@ public:
api::Term getOverloadedFunctionForTypes(const std::string& name,
std::vector<api::Sort>& argTypes)
{
- return d_symtab->getOverloadedFunctionForTypes(
- name, api::sortVectorToTypes(argTypes));
+ return api::Term(d_solver,
+ d_symtab->getOverloadedFunctionForTypes(
+ name, api::sortVectorToTypes(argTypes)));
}
//------------------------ end operator overloading
/**
@@ -845,7 +847,7 @@ public:
* SMT-LIB 2.6 or higher), or otherwise calling the solver to construct
* the string.
*/
- Expr mkStringConstant(const std::string& s);
+ api::Term mkStringConstant(const std::string& s);
private:
/** ad-hoc string escaping
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 95f4b1a67..081990a45 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -101,7 +101,7 @@ namespace CVC4 {
struct myExpr : public CVC4::api::Term {
myExpr() : CVC4::api::Term() {}
myExpr(void*) : CVC4::api::Term() {}
- myExpr(const Expr& e) : CVC4::api::Term(e) {}
+ myExpr(const Expr& e) : CVC4::api::Term(d_solver, e) {}
myExpr(const myExpr& e) : CVC4::api::Term(e) {}
};/* struct myExpr */
}/* CVC4::parser::smt2 namespace */
@@ -286,7 +286,7 @@ command [std::unique_ptr<CVC4::Command>* cmd]
{ PARSER_STATE->popScope();
// Do NOT call mkSort, since that creates a new sort!
// This name is not its own distinct sort, it's an alias.
- PARSER_STATE->defineParameterizedType(name, sorts, t.getType());
+ PARSER_STATE->defineParameterizedType(name, sorts, t);
cmd->reset(new DefineTypeCommand(
name, api::sortVectorToTypes(sorts), t.getType()));
}
@@ -800,7 +800,7 @@ sygusGrammarV1[CVC4::api::Sort & ret,
PARSER_STATE->getUnresolvedSorts().clear();
- ret = datatypeTypes[0];
+ ret = api::Sort(PARSER_STATE->getSolver(), datatypeTypes[0]);
};
// SyGuS grammar term.
@@ -893,7 +893,7 @@ sygusGTerm[CVC4::SygusGTerm& sgt, const std::string& fun]
<< "expression " << atomTerm << std::endl;
std::stringstream ss;
ss << atomTerm;
- sgt.d_op.d_expr = atomTerm.getExpr();
+ sgt.d_op.d_expr = atomTerm;
sgt.d_name = ss.str();
sgt.d_gterm_type = SygusGTerm::gterm_op;
}
@@ -1791,8 +1791,10 @@ termNonVariable[CVC4::api::Term& expr, CVC4::api::Term& expr2]
Expr ef = f.getExpr();
if (Datatype::datatypeOf(ef).isParametric())
{
- type = Datatype::datatypeOf(ef)[Datatype::indexOf(ef)]
- .getSpecializedConstructorType(expr.getSort().getType());
+ type = api::Sort(
+ PARSER_STATE->getSolver(),
+ Datatype::datatypeOf(ef)[Datatype::indexOf(ef)]
+ .getSpecializedConstructorType(expr.getSort().getType()));
}
argTypes = type.getConstructorDomainSorts();
}
@@ -1914,10 +1916,10 @@ termNonVariable[CVC4::api::Term& expr, CVC4::api::Term& expr2]
sorts.emplace_back(arg.getSort());
terms.emplace_back(arg);
}
- expr = SOLVER->mkTuple(sorts, terms).getExpr();
+ expr = SOLVER->mkTuple(sorts, terms);
}
| /* an atomic term (a term with no subterms) */
- termAtomic[atomTerm] { expr = atomTerm.getExpr(); }
+ termAtomic[atomTerm] { expr = atomTerm; }
;
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 9ca2194f4..608e47a6b 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -1377,7 +1377,7 @@ void Smt2::mkSygusDatatype(api::DatatypeDecl& dt,
if( std::find( types.begin(), types.end(), t )==types.end() ){
types.push_back( t );
//identity element
- api::Sort bt = dt.getDatatype().getSygusType();
+ api::Sort bt = api::Sort(d_solver, dt.getDatatype().getSygusType());
Debug("parser-sygus") << ": make identity function for " << bt << ", argument type " << t << std::endl;
std::stringstream ss;
@@ -1481,7 +1481,7 @@ api::Term Smt2::purifySygusGTerm(api::Term term,
api::Term ret = d_solver->mkVar(term.getSort());
Trace("parser-sygus2-debug")
<< "...unresolved non-terminal, intro " << ret << std::endl;
- args.push_back(ret.getExpr());
+ args.push_back(api::Term(d_solver, ret.getExpr()));
cargs.push_back(itn->second);
return ret;
}
@@ -1571,8 +1571,7 @@ void Smt2::parseOpApplyTypeAscription(ParseOp& p, api::Sort type)
Trace("parser-qid") << " " << p.d_expr.getKind() << " " << p.d_expr.getSort();
Trace("parser-qid") << std::endl;
// otherwise, we process the type ascription
- p.d_expr =
- applyTypeAscription(api::Term(p.d_expr), api::Sort(type)).getExpr();
+ p.d_expr = applyTypeAscription(p.d_expr, type);
}
api::Term Smt2::parseOpToExpr(ParseOp& p)
@@ -1776,8 +1775,10 @@ api::Term Smt2::applyParseOp(ParseOp& p, std::vector<api::Term>& args)
parseError(ss.str());
}
const Datatype& dt = ((DatatypeType)t.getType()).getDatatype();
- api::Term ret = d_solver->mkTerm(
- api::APPLY_SELECTOR, api::Term(dt[0][n].getSelector()), args[0]);
+ api::Term ret =
+ d_solver->mkTerm(api::APPLY_SELECTOR,
+ api::Term(d_solver, dt[0][n].getSelector()),
+ args[0]);
Debug("parser") << "applyParseOp: return selector " << ret << std::endl;
return ret;
}
diff --git a/src/parser/tptp/Tptp.g b/src/parser/tptp/Tptp.g
index c2f4675b1..c1d60ca31 100644
--- a/src/parser/tptp/Tptp.g
+++ b/src/parser/tptp/Tptp.g
@@ -1441,7 +1441,7 @@ tffLetTermBinding[std::vector<CVC4::api::Term> & bvlist,
PARSER_STATE->checkLetBinding(bvlist, lhs, rhs, false);
std::vector<api::Term> lchildren(++lhs.begin(), lhs.end());
rhs = MK_TERM(api::LAMBDA, MK_TERM(api::BOUND_VAR_LIST, lchildren), rhs);
- lhs = api::Term(lhs.getExpr().getOperator());
+ lhs = api::Term(PARSER_STATE->getSolver(), lhs.getExpr().getOperator());
}
| LPAREN_TOK tffLetTermBinding[bvlist, lhs, rhs] RPAREN_TOK
;
@@ -1463,7 +1463,7 @@ tffLetFormulaBinding[std::vector<CVC4::api::Term> & bvlist,
PARSER_STATE->checkLetBinding(bvlist, lhs, rhs, true);
std::vector<api::Term> lchildren(++lhs.begin(), lhs.end());
rhs = MK_TERM(api::LAMBDA, MK_TERM(api::BOUND_VAR_LIST, lchildren), rhs);
- lhs = api::Term(lhs.getExpr().getOperator());
+ lhs = api::Term(PARSER_STATE->getSolver(), lhs.getExpr().getOperator());
}
| LPAREN_TOK tffLetFormulaBinding[bvlist, lhs, rhs] RPAREN_TOK
;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback