diff options
Diffstat (limited to 'src/theory/quantifiers/sygus_sampler.h')
-rw-r--r-- | src/theory/quantifiers/sygus_sampler.h | 33 |
1 files changed, 24 insertions, 9 deletions
diff --git a/src/theory/quantifiers/sygus_sampler.h b/src/theory/quantifiers/sygus_sampler.h index 28f715b34..3a2c42b9d 100644 --- a/src/theory/quantifiers/sygus_sampler.h +++ b/src/theory/quantifiers/sygus_sampler.h @@ -2,9 +2,9 @@ /*! \file sygus_sampler.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Tim King, Mathias Preiner + ** Andrew Reynolds, FabianWolff, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -194,14 +194,15 @@ class SygusSampler : public LazyTrieEvaluator }; /** a trie for samples */ PtTrie d_samples_trie; - /** type of nodes we will be registering with this class */ - TypeNode d_tn; /** the sygus type for this sampler (if applicable). */ TypeNode d_ftn; - /** whether we are registering terms of type d_ftn */ + /** whether we are registering terms of sygus types with this sampler */ bool d_use_sygus_type; - /** map from builtin terms to the sygus term they correspond to */ - std::map<Node, Node> d_builtin_to_sygus; + /** + * For each (sygus) type, a map from builtin terms to the sygus term they + * correspond to. + */ + std::map<TypeNode, std::map<Node, Node> > d_builtin_to_sygus; /** all variables we are sampling values for */ std::vector<Node> d_vars; /** type variables @@ -235,8 +236,22 @@ class SygusSampler : public LazyTrieEvaluator * that type. */ std::map<TypeNode, std::vector<Node> > d_type_consts; - /** the lazy trie */ - LazyTrie d_trie; + /** a lazy trie for each type + * + * This stores the evaluation of all terms registered to this class. + * + * Notice if we are registering sygus terms with this class, then terms + * are grouped into this trie according to their sygus type, and not their + * builtin type. For example, for grammar: + * A -> x | B+1 + * B -> x | 0 | 1 | B+B + * If we register C^B_+( C^B_x(), C^B_0() ) and C^A_x() with this class, + * then x+0 is registered to d_trie[B] and x is registered to d_trie[A], + * and no rewrite rule is reported. The reason for this is that otherwise + * we would end up reporting many useless rewrites since the same builtin + * term can be generated by multiple sygus types (e.g. C^B_x() and C^A_x()). + */ + std::map<TypeNode, LazyTrie> d_trie; /** is this sampler valid? * * A sampler can be invalid if sample points cannot be generated for a type |