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/expr | |
| 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/expr')
| -rw-r--r-- | src/expr/datatype.cpp | 4 | ||||
| -rw-r--r-- | src/expr/datatype.h | 2 |
2 files changed, 3 insertions, 3 deletions
diff --git a/src/expr/datatype.cpp b/src/expr/datatype.cpp index 513cb2170..8b6384dcc 100644 --- a/src/expr/datatype.cpp +++ b/src/expr/datatype.cpp @@ -879,11 +879,11 @@ bool DatatypeConstructor::isSygusIdFunc() const { && d_sygus_op[0][0] == d_sygus_op[1]); } -SygusPrintCallback* DatatypeConstructor::getSygusPrintCallback() const +std::shared_ptr<SygusPrintCallback> DatatypeConstructor::getSygusPrintCallback() const { PrettyCheckArgument( isResolved(), this, "this datatype constructor is not yet resolved"); - return d_sygus_pc.get(); + return d_sygus_pc; } Cardinality DatatypeConstructor::getCardinality( Type t ) const throw(IllegalArgumentException) { diff --git a/src/expr/datatype.h b/src/expr/datatype.h index 85ecfb946..b899b0099 100644 --- a/src/expr/datatype.h +++ b/src/expr/datatype.h @@ -300,7 +300,7 @@ class CVC4_PUBLIC DatatypeConstructor { * to handle defined or let expressions that * appear in user-provided grammars. */ - SygusPrintCallback* getSygusPrintCallback() const; + std::shared_ptr<SygusPrintCallback> getSygusPrintCallback() const; /** * Get the tester name for this Datatype constructor. |