diff options
| -rw-r--r-- | src/theory/quantifiers/sygus_grammar_norm.cpp | 10 | ||||
| -rw-r--r-- | src/theory/quantifiers/sygus_grammar_norm.h | 41 |
2 files changed, 32 insertions, 19 deletions
diff --git a/src/theory/quantifiers/sygus_grammar_norm.cpp b/src/theory/quantifiers/sygus_grammar_norm.cpp index 1b5cd3452..6776aca15 100644 --- a/src/theory/quantifiers/sygus_grammar_norm.cpp +++ b/src/theory/quantifiers/sygus_grammar_norm.cpp @@ -35,7 +35,7 @@ namespace quantifiers { bool OpPosTrie::getOrMakeType(TypeNode tn, TypeNode& unres_tn, - std::vector<unsigned> op_pos, + const std::vector<unsigned>& op_pos, unsigned ind) { if (ind == op_pos.size()) @@ -274,7 +274,7 @@ std::map<TypeNode, Node> SygusGrammarNorm::d_tn_to_id = {}; * * returns true if collected anything */ -SygusGrammarNorm::Transf* SygusGrammarNorm::inferTransf( +std::unique_ptr<SygusGrammarNorm::Transf> SygusGrammarNorm::inferTransf( TypeNode tn, const Datatype& dt, const std::vector<unsigned>& op_pos) { NodeManager* nm = NodeManager::currentNM(); @@ -295,7 +295,7 @@ SygusGrammarNorm::Transf* SygusGrammarNorm::inferTransf( Trace("sygus-gnorm") << "...drop transf, " << rindices.size() << "/" << op_pos.size() << " constructors." << std::endl; Assert(rindices.size() < op_pos.size()); - return new TransfDrop(rindices); + return std::unique_ptr<Transf>(new TransfDrop(rindices)); } } @@ -363,7 +363,7 @@ SygusGrammarNorm::Transf* SygusGrammarNorm::inferTransf( Trace("sygus-gnorm") << "...chain transf." << std::endl; Trace("sygus-grammar-normalize-infer") << "\tInfering chain transformation\n"; - return new TransfChain(chain_op_pos, elem_pos); + return std::unique_ptr<Transf>(new TransfChain(chain_op_pos, elem_pos)); } return nullptr; } @@ -417,7 +417,7 @@ TypeNode SygusGrammarNorm::normalizeSygusRec(TypeNode tn, /* Determine normalization transformation based on sygus type and given * operators */ - Transf* transformation = inferTransf(tn, dt, op_pos); + std::unique_ptr<Transf> transformation = inferTransf(tn, dt, op_pos); /* If a transformation was selected, apply it */ if (transformation != nullptr) { diff --git a/src/theory/quantifiers/sygus_grammar_norm.h b/src/theory/quantifiers/sygus_grammar_norm.h index d1894ac2e..f72a83e5a 100644 --- a/src/theory/quantifiers/sygus_grammar_norm.h +++ b/src/theory/quantifiers/sygus_grammar_norm.h @@ -17,7 +17,16 @@ #ifndef __CVC4__THEORY__QUANTIFIERS__SYGUS_GRAMMAR_NORM_H #define __CVC4__THEORY__QUANTIFIERS__SYGUS_GRAMMAR_NORM_H +#include <map> +#include <memory> +#include <string> +#include <vector> + +#include "expr/datatype.h" +#include "expr/node.h" #include "expr/node_manager_attributes.h" // for VarNameAttr +#include "expr/type.h" +#include "expr/type_node.h" #include "theory/quantifiers/term_util.h" #include "theory/quantifiers_engine.h" @@ -78,7 +87,7 @@ class OpPosTrie */ bool getOrMakeType(TypeNode tn, TypeNode& unres_tn, - std::vector<unsigned> op_pos, + const std::vector<unsigned>& op_pos, unsigned ind = 0); /** clear all data from this trie */ void clear() { d_children.clear(); } @@ -241,6 +250,8 @@ class SygusGrammarNorm class Transf { public: + virtual ~Transf() {} + /** abstract function for building normalized types * * Builds normalized types for the operators specifed by the positions in @@ -262,12 +273,14 @@ class SygusGrammarNorm class TransfDrop : public Transf { public: - TransfDrop(std::vector<unsigned>& indices) : d_drop_indices(indices) {} + TransfDrop(const std::vector<unsigned>& indices) : d_drop_indices(indices) + { + } /** build type */ - virtual void buildType(SygusGrammarNorm* sygus_norm, - TypeObject& to, - const Datatype& dt, - std::vector<unsigned>& op_pos); + void buildType(SygusGrammarNorm* sygus_norm, + TypeObject& to, + const Datatype& dt, + std::vector<unsigned>& op_pos) override; private: std::vector<unsigned> d_drop_indices; @@ -294,7 +307,7 @@ class SygusGrammarNorm class TransfChain : public Transf { public: - TransfChain(unsigned chain_op_pos, std::vector<unsigned>& elem_pos) + TransfChain(unsigned chain_op_pos, const std::vector<unsigned>& elem_pos) : d_chain_op_pos(chain_op_pos), d_elem_pos(elem_pos){}; /** builds types encoding a chain in which each link contains a repetition @@ -322,10 +335,10 @@ class SygusGrammarNorm * transformation and so on until all operators originally given are * considered. */ - virtual void buildType(SygusGrammarNorm* sygus_norm, - TypeObject& to, - const Datatype& dt, - std::vector<unsigned>& op_pos) override; + void buildType(SygusGrammarNorm* sygus_norm, + TypeObject& to, + const Datatype& dt, + std::vector<unsigned>& op_pos) override; /** Whether operator is chainable for the type (e.g. PLUS for Int) * @@ -430,9 +443,9 @@ class SygusGrammarNorm * * TODO: #1304: Infer more complex transformations */ - Transf* inferTransf(TypeNode tn, - const Datatype& dt, - const std::vector<unsigned>& op_pos); + std::unique_ptr<Transf> inferTransf(TypeNode tn, + const Datatype& dt, + const std::vector<unsigned>& op_pos); }; /* class SygusGrammarNorm */ } // namespace quantifiers |