diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-08-10 14:26:02 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2019-08-10 14:26:02 -0500 |
| commit | 03a99a427eaa8c679ede508e11561467a2291334 (patch) | |
| tree | b74688f17420c9d8a352b22eed339983d4e369ab /src/parser/smt2/smt2.cpp | |
| parent | d1f3225e26b9d64f065048885053392b10994e71 (diff) | |
Simplify how defined functions are tracked during parsing (#3177)
Diffstat (limited to 'src/parser/smt2/smt2.cpp')
| -rw-r--r-- | src/parser/smt2/smt2.cpp | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 039f573f9..be0306a9e 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -1171,7 +1171,7 @@ void Smt2::processSygusLetConstructor( std::vector< CVC4::Expr >& let_vars, Type ft = getExprManager()->mkFunctionType(fsorts, let_body.getType()); std::stringstream ss; ss << datatypes[index].getName() << "_let"; - Expr let_func = mkFunction(ss.str(), ft, ExprManager::VAR_FLAG_DEFINED); + Expr let_func = mkVar(ss.str(), ft, ExprManager::VAR_FLAG_DEFINED); d_sygus_defined_funs.push_back( let_func ); preemptCommand( new DefineFunctionCommand(ss.str(), let_func, let_define_args, let_body) ); @@ -1338,7 +1338,7 @@ void Smt2::mkSygusDatatype( CVC4::Datatype& dt, std::vector<CVC4::Expr>& ops, // the given name. spc = std::make_shared<printer::SygusNamedPrintCallback>(cnames[i]); } - else if (isDefinedFunction(ops[i])) + else if (ops[i].getKind() == kind::VARIABLE) { Debug("parser-sygus") << "--> Defined function " << ops[i] << std::endl; |