From f0bc0137d00946f79e62e223b849e7372cc0109f Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 21 Nov 2018 17:07:17 -0600 Subject: Cache evaluations for PBE (#2699) --- src/theory/quantifiers/sygus/sygus_pbe.h | 26 +++----------------------- 1 file changed, 3 insertions(+), 23 deletions(-) (limited to 'src/theory/quantifiers/sygus/sygus_pbe.h') 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 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& ex, - SygusPbe* cpbe, - unsigned index, - unsigned ntotal); + Node addTerm(Node b, const std::vector& exOut); }; /** trie of candidate solutions tried * This stores information for each (enumerator, type), -- cgit v1.2.3