diff options
author | Haniel Barbosa <hanielbbarbosa@gmail.com> | 2017-11-22 21:56:35 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2017-11-22 21:56:35 -0600 |
commit | c9ae6b9812e737ae7932df91fa5f334d6d2588d4 (patch) | |
tree | 61ac786790c044b88cf8589cc588e77760fe22e8 /src/printer | |
parent | 20704741e4609055d61e010b6981c6916d28019a (diff) |
Converting defined functions and let expressions from Sygus grammars to lambdas (#1403)
This partially solves issue #1344. Definitions are expanded when the grammar normalizer is called. When this becomes default then the code that expands definitions elsewhere will be removed.
The PR also contains minor changes to the PrintCallback and SygusGrammarNormalize module.
Diffstat (limited to 'src/printer')
-rw-r--r-- | src/printer/smt2/smt2_printer.cpp | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 82871a1d5..c029c0824 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -1324,7 +1324,7 @@ void Smt2Printer::toStreamSygus(std::ostream& out, TNode n) const throw() { int cIndex = Datatype::indexOf(n.getOperator().toExpr()); Assert(!dt[cIndex].getSygusOp().isNull()); - SygusPrintCallback* spc = dt[cIndex].getSygusPrintCallback(); + SygusPrintCallback* spc = dt[cIndex].getSygusPrintCallback().get(); if (spc != nullptr && options::sygusPrintCallbacks()) { spc->toStreamSygus(this, out, n.toExpr()); |