diff options
Diffstat (limited to 'src/theory/quantifiers/sygus_sampler.h')
-rw-r--r-- | src/theory/quantifiers/sygus_sampler.h | 13 |
1 files changed, 8 insertions, 5 deletions
diff --git a/src/theory/quantifiers/sygus_sampler.h b/src/theory/quantifiers/sygus_sampler.h index 85606adc6..3695270e1 100644 --- a/src/theory/quantifiers/sygus_sampler.h +++ b/src/theory/quantifiers/sygus_sampler.h @@ -19,15 +19,18 @@ #define CVC5__THEORY__QUANTIFIERS__SYGUS_SAMPLER_H #include <map> -#include "theory/evaluator.h" #include "theory/quantifiers/lazy_trie.h" -#include "theory/quantifiers/sygus/term_database_sygus.h" #include "theory/quantifiers/term_enumeration.h" namespace cvc5 { + +class Env; + namespace theory { namespace quantifiers { +class TermDbSygus; + /** SygusSampler * * This class can be used to test whether two expressions are equivalent @@ -65,7 +68,7 @@ namespace quantifiers { class SygusSampler : public LazyTrieEvaluator { public: - SygusSampler(); + SygusSampler(Env& env); ~SygusSampler() override {} /** initialize @@ -178,14 +181,14 @@ class SygusSampler : public LazyTrieEvaluator void checkEquivalent(Node bv, Node bvr, std::ostream& out); protected: + /** The environment we are using to evaluate terms and samples */ + Env& d_env; /** sygus term database of d_qe */ TermDbSygus* d_tds; /** term enumerator object (used for random sampling) */ TermEnumeration d_tenum; /** samples */ std::vector<std::vector<Node> > d_samples; - /** evaluator class */ - Evaluator d_eval; /** data structure to check duplication of sample points */ class PtTrie { |