diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-10-29 21:51:18 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-10-29 21:51:18 -0500 |
| commit | 21fd193bdaad1a952845326aa1c84654cfce1503 (patch) | |
| tree | 5d7732c5442dc73120352eb25ed92af9806c0751 /src/smt/command.cpp | |
| parent | 3596632eef07dbe28ea4a4f166c18ad9fe26d4e0 (diff) | |
Update api::Sort to use TypeNode instead of Type (#5363)
This is work towards removing the old API.
This makes TypeNode the backend for Sort instead of Type.
It also updates a unit test for methods isUninterpretedSortParameterized and getUninterpretedSortParamSorts whose implementation was previously buggy due to the implementation of Type-level SortType.
Diffstat (limited to 'src/smt/command.cpp')
| -rw-r--r-- | src/smt/command.cpp | 24 |
1 files changed, 9 insertions, 15 deletions
diff --git a/src/smt/command.cpp b/src/smt/command.cpp index 9b0784831..8a5247dec 100644 --- a/src/smt/command.cpp +++ b/src/smt/command.cpp @@ -602,7 +602,7 @@ void DeclareSygusVarCommand::toStream(std::ostream& out, OutputLanguage language) const { Printer::getPrinter(language)->toStreamCmdDeclareVar( - out, d_var.getNode(), TypeNode::fromType(d_sort.getType())); + out, d_var.getNode(), d_sort.getTypeNode()); } /* -------------------------------------------------------------------------- */ @@ -663,9 +663,9 @@ void SynthFunCommand::toStream(std::ostream& out, out, d_symbol, nodeVars, - TypeNode::fromType(d_sort.getType()), + d_sort.getTypeNode(), d_isInv, - TypeNode::fromType(d_grammar->resolve().getType())); + d_grammar->resolve().getTypeNode()); } /* -------------------------------------------------------------------------- */ @@ -1130,7 +1130,7 @@ void DeclareFunctionCommand::toStream(std::ostream& out, OutputLanguage language) const { Printer::getPrinter(language)->toStreamCmdDeclareFunction( - out, d_func.toString(), TypeNode::fromType(d_sort.getType())); + out, d_func.toString(), d_sort.getTypeNode()); } /* -------------------------------------------------------------------------- */ @@ -1168,7 +1168,7 @@ void DeclareSortCommand::toStream(std::ostream& out, OutputLanguage language) const { Printer::getPrinter(language)->toStreamCmdDeclareType( - out, d_sort.toString(), d_arity, TypeNode::fromType(d_sort.getType())); + out, d_sort.toString(), d_arity, d_sort.getTypeNode()); } /* -------------------------------------------------------------------------- */ @@ -1215,7 +1215,7 @@ void DefineSortCommand::toStream(std::ostream& out, out, d_symbol, api::sortVectorToTypeNodes(d_params), - TypeNode::fromType(d_sort.getType())); + d_sort.getTypeNode()); } /* -------------------------------------------------------------------------- */ @@ -1337,7 +1337,7 @@ void DefineNamedFunctionCommand::toStream(std::ostream& out, out, d_func.toString(), api::termVectorToNodes(d_formals), - TypeNode::fromType(d_func.getSort().getFunctionCodomainSort().getType()), + d_func.getSort().getFunctionCodomainSort().getTypeNode(), d_formula.getNode()); } @@ -2100,10 +2100,7 @@ void GetInterpolCommand::toStream(std::ostream& out, OutputLanguage language) const { Printer::getPrinter(language)->toStreamCmdGetInterpol( - out, - d_name, - d_conj.getNode(), - TypeNode::fromType(d_sygus_grammar->resolve().getType())); + out, d_name, d_conj.getNode(), d_sygus_grammar->resolve().getTypeNode()); } /* -------------------------------------------------------------------------- */ @@ -2189,10 +2186,7 @@ void GetAbductCommand::toStream(std::ostream& out, OutputLanguage language) const { Printer::getPrinter(language)->toStreamCmdGetAbduct( - out, - d_name, - d_conj.getNode(), - TypeNode::fromType(d_sygus_grammar->resolve().getType())); + out, d_name, d_conj.getNode(), d_sygus_grammar->resolve().getTypeNode()); } /* -------------------------------------------------------------------------- */ |