diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-11-21 17:07:17 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-11-21 17:07:17 -0600 |
commit | f0bc0137d00946f79e62e223b849e7372cc0109f (patch) | |
tree | 4ac703379828f80a8e17d0f75951ee59fb3ffc7f /src/theory/quantifiers/sygus/sygus_pbe.h | |
parent | 1e7ce9dcc5268c8e13466f63ac2c4159d71a583a (diff) |
Cache evaluations for PBE (#2699)
Diffstat (limited to 'src/theory/quantifiers/sygus/sygus_pbe.h')
-rw-r--r-- | src/theory/quantifiers/sygus/sygus_pbe.h | 26 |
1 files changed, 3 insertions, 23 deletions
diff --git a/src/theory/quantifiers/sygus/sygus_pbe.h b/src/theory/quantifiers/sygus/sygus_pbe.h index a62100692..dc7f1cc51 100644 --- a/src/theory/quantifiers/sygus/sygus_pbe.h +++ b/src/theory/quantifiers/sygus/sygus_pbe.h @@ -269,35 +269,15 @@ class SygusPbe : public SygusModule public: PbeTrie() {} ~PbeTrie() {} - /** the data for this node in the trie */ - Node d_lazy_child; /** the children for this node in the trie */ std::map<Node, PbeTrie> d_children; /** clear this trie */ void clear() { d_children.clear(); } /** - * Add term b as a value enumerated for enumerator e to the trie. - * - * cpbe : reference to the parent pbe utility which stores the examples, - * index : the index of the example we are processing, - * ntotal : the total of the examples for enumerator e. + * Add term b whose value on examples is exOut to the trie. Return + * the first term registered to this trie whose evaluation was exOut. */ - Node addPbeExample(TypeNode etn, - Node e, - Node b, - SygusPbe* cpbe, - unsigned index, - unsigned ntotal); - - private: - /** Helper function for above, called when we get the current example ex. */ - Node addPbeExampleEval(TypeNode etn, - Node e, - Node b, - std::vector<Node>& ex, - SygusPbe* cpbe, - unsigned index, - unsigned ntotal); + Node addTerm(Node b, const std::vector<Node>& exOut); }; /** trie of candidate solutions tried * This stores information for each (enumerator, type), |