summaryrefslogtreecommitdiff
path: root/src/parser/smt2
diff options
context:
space:
mode:
Diffstat (limited to 'src/parser/smt2')
-rw-r--r--src/parser/smt2/Smt2.g33
-rw-r--r--src/parser/smt2/smt2.cpp19
-rw-r--r--src/parser/smt2/smt2.h7
3 files changed, 41 insertions, 18 deletions
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index d591c29de..62bf7e974 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(SOLVER, 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;
}
@@ -1692,7 +1692,13 @@ termNonVariable[CVC4::api::Term& expr, CVC4::api::Term& expr2]
std::vector<api::Sort> argTypes;
}
: LPAREN_TOK quantOp[kind]
- { PARSER_STATE->pushScope(true); }
+ {
+ if (!PARSER_STATE->isTheoryEnabled(theory::THEORY_QUANTIFIERS))
+ {
+ PARSER_STATE->parseError("Quantifier used in non-quantified logic.");
+ }
+ PARSER_STATE->pushScope(true);
+ }
boundVarList[bvl]
term[f, f2] RPAREN_TOK
{
@@ -1791,8 +1797,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(
+ SOLVER,
+ Datatype::datatypeOf(ef)[Datatype::indexOf(ef)]
+ .getSpecializedConstructorType(expr.getSort().getType()));
}
argTypes = type.getConstructorDomainSorts();
}
@@ -1914,10 +1922,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; }
;
@@ -2513,7 +2521,8 @@ constructorDef[CVC4::api::DatatypeDecl& type]
}
: symbol[id,CHECK_NONE,SYM_VARIABLE]
{
- ctor = new api::DatatypeConstructorDecl(id);
+ ctor = new api::DatatypeConstructorDecl(
+ SOLVER->mkDatatypeConstructorDecl(id));
}
( LPAREN_TOK selector[*ctor] RPAREN_TOK )*
{ // make the constructor
@@ -2630,8 +2639,8 @@ CHAR_TOK : { PARSER_STATE->isTheoryEnabled(theory::THEORY_STRINGS) }? 'char';
TUPLE_CONST_TOK: { PARSER_STATE->isTheoryEnabled(theory::THEORY_DATATYPES) }? 'mkTuple';
TUPLE_SEL_TOK: { PARSER_STATE->isTheoryEnabled(theory::THEORY_DATATYPES) }? 'tupSel';
-HO_ARROW_TOK : { PARSER_STATE->getLogic().isHigherOrder() }? '->';
-HO_LAMBDA_TOK : { PARSER_STATE->getLogic().isHigherOrder() }? 'lambda';
+HO_ARROW_TOK : { PARSER_STATE->isHoEnabled() }? '->';
+HO_LAMBDA_TOK : { PARSER_STATE->isHoEnabled() }? 'lambda';
/**
* A sequence of printable ASCII characters (except backslash) that starts
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 91260d1db..608e47a6b 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -315,6 +315,12 @@ bool Smt2::isTheoryEnabled(theory::TheoryId theory) const
return d_logic.isTheoryEnabled(theory);
}
+bool Smt2::isHoEnabled() const
+{
+ return getLogic().isHigherOrder()
+ && d_solver->getExprManager()->getOptions().getUfHo();
+}
+
bool Smt2::logicIsSet() {
return d_logicSet;
}
@@ -1371,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;
@@ -1475,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;
}
@@ -1565,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)
@@ -1770,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/smt2/smt2.h b/src/parser/smt2/smt2.h
index 35d088601..af1e36795 100644
--- a/src/parser/smt2/smt2.h
+++ b/src/parser/smt2/smt2.h
@@ -98,6 +98,13 @@ class Smt2 : public Parser
bool isTheoryEnabled(theory::TheoryId theory) const;
+ /**
+ * Checks if higher-order support is enabled.
+ *
+ * @return true if higher-order support is enabled, false otherwise
+ */
+ bool isHoEnabled() const;
+
bool logicIsSet() override;
/**
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback