diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-08-25 19:04:39 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-08-25 19:04:39 -0500 |
commit | 34eac85599875517732d53a5cc1acd3ab60479d1 (patch) | |
tree | ebfa9e493b32aba67d85d6d0bb7a6b468fac5fd4 /src/preprocessing | |
parent | c5eb77b96cd67b8d80ee8901a3f0b5ae7d54aab2 (diff) |
Replace Expr-level datatype with Node-level DType (#4875)
This PR makes two simultaneous changes:
The new API uses Node-level DType instead of Expr-level Datatype. This required converting 2 of the last remaining calls in the parser that used Expr to use the new API.
Internally constructed datatypes (e.g. for sygus) use Node-level DType instead of Expr-level Datatype. Note this required moving a block of code for handling a corner case of sygus from Datatype -> DType.
This PR removes :
ExprManger::mkDatatypeType.
The Expr-level datatype itself. This PR removes all references to its include file.
It also updates one remaining unit test from Expr -> Node.
This PR will enable further removal of other datatype-specific things in the Expr layer.
Diffstat (limited to 'src/preprocessing')
-rw-r--r-- | src/preprocessing/passes/synth_rew_rules.cpp | 22 |
1 files changed, 11 insertions, 11 deletions
diff --git a/src/preprocessing/passes/synth_rew_rules.cpp b/src/preprocessing/passes/synth_rew_rules.cpp index d0ebe5f19..b34ff59f5 100644 --- a/src/preprocessing/passes/synth_rew_rules.cpp +++ b/src/preprocessing/passes/synth_rew_rules.cpp @@ -241,7 +241,7 @@ PreprocessingPassResult SynthRewRulesPass::applyInternal( Trace("srs-input") << "Construct unresolved types..." << std::endl; // each canonical subterm corresponds to a grammar type - std::set<Type> unres; + std::set<TypeNode> unres; std::vector<SygusDatatype> sdts; // make unresolved types for each canonical term std::map<Node, TypeNode> cterm_to_utype; @@ -253,7 +253,7 @@ PreprocessingPassResult SynthRewRulesPass::applyInternal( std::string tname = ss.str(); TypeNode tnu = nm->mkSort(tname, ExprManager::SORT_FLAG_PLACEHOLDER); cterm_to_utype[ct] = tnu; - unres.insert(tnu.toType()); + unres.insert(tnu); sdts.push_back(SygusDatatype(tname)); } Trace("srs-input") << "...finished." << std::endl; @@ -369,19 +369,19 @@ PreprocessingPassResult SynthRewRulesPass::applyInternal( Trace("srs-input") << "Make mutual datatype types for subterms..." << std::endl; // extract the datatypes - std::vector<Datatype> datatypes; + std::vector<DType> datatypes; for (unsigned i = 0, ndts = sdts.size(); i < ndts; i++) { datatypes.push_back(sdts[i].getDatatype()); } - std::vector<DatatypeType> types = nm->toExprManager()->mkMutualDatatypeTypes( - datatypes, unres, ExprManager::DATATYPE_FLAG_PLACEHOLDER); + std::vector<TypeNode> types = nm->mkMutualDatatypeTypes( + datatypes, unres, NodeManager::DATATYPE_FLAG_PLACEHOLDER); Trace("srs-input") << "...finished." << std::endl; Assert(types.size() == unres.size()); std::map<Node, TypeNode> subtermTypes; for (unsigned i = 0, ncterms = cterms.size(); i < ncterms; i++) { - subtermTypes[cterms[i]] = TypeNode::fromType(types[i]); + subtermTypes[cterms[i]] = types[i]; } Trace("srs-input") << "Construct the top-level types..." << std::endl; @@ -418,12 +418,12 @@ PreprocessingPassResult SynthRewRulesPass::applyInternal( } // set that this is a sygus datatype sdttl.initializeDatatype(t, sygusVarList, false, false); - Datatype dttl = sdttl.getDatatype(); - DatatypeType tlt = nm->toExprManager()->mkDatatypeType( - dttl, ExprManager::DATATYPE_FLAG_PLACEHOLDER); - tlGrammarTypes[t] = TypeNode::fromType(tlt); + DType dttl = sdttl.getDatatype(); + TypeNode tlt = + nm->mkDatatypeType(dttl, NodeManager::DATATYPE_FLAG_PLACEHOLDER); + tlGrammarTypes[t] = tlt; Trace("srs-input") << "Grammar is: " << std::endl; - Trace("srs-input") << tlt.getDatatype() << std::endl; + Trace("srs-input") << tlt.getDType() << std::endl; } Trace("srs-input") << "...finished." << std::endl; |