Home
last modified time | relevance | path

Searched refs:d_sampler (Results 1 – 9 of 9) sorted by relevance

/dports/math/cvc4/CVC4-1.7/src/theory/quantifiers/
H A Dexpr_miner_manager.cpp47 d_sampler.initialize(tn, vars, nsamples, unique_type_ids); in initialize()
63 d_sampler.initializeSygus(d_tds, f, nsamples, useSygusType); in initializeSygus()
75 d_sampler.getVariables(vars); in enableRewriteRuleSynth()
80 d_crd.initializeSygus(vars, d_qe, d_sygus_fun, &d_sampler); in enableRewriteRuleSynth()
84 d_crd.initialize(vars, &d_sampler); in enableRewriteRuleSynth()
99 d_sampler.getVariables(vars); in enableQueryGeneration()
108 d_qg.initialize(vars, &d_sampler); in enableQueryGeneration()
116 d_sampler.getVariables(vars); in enableFilterWeakSolutions()
117 d_sols.initialize(vars, &d_sampler); in enableFilterWeakSolutions()
125 d_sampler.getVariables(vars); in enableFilterStrongSolutions()
[all …]
H A Dquery_generator.cpp54 unsigned npts = d_sampler->getNumSamplePoints(); in addTerm()
74 Node v = d_sampler->evaluate(nn, index); in addTerm()
153 d_sampler->getSamplePoint(spIndex, pt); in checkQuery()
201 d_sampler->getSamplePoint(spIndex, pt); in checkQuery()
231 LazyTrieEvaluator* ev = d_sampler; in findQueries()
232 unsigned ntotal = d_sampler->getNumSamplePoints(); in findQueries()
H A Dexpr_miner.h41 ExprMiner() : d_sampler(nullptr) {} in ExprMiner()
65 SygusSampler* d_sampler; variable
H A Dcandidate_rewrite_database.cpp96 Node eq_sol = d_sampler->registerTerm(sol); in addTerm()
151 d_sampler->getVariables(vars); in addTerm()
190 d_sampler->addSamplePoint(pt); in addTerm()
193 Node eq_sol_new = d_sampler->registerTerm(sol); in addTerm()
320 d_cdbs[tn].initialize(d_vars, &d_sampler[tn]); in addTerm()
H A Dexpr_miner_manager.h114 SygusSampler d_sampler; variable
H A Dcandidate_rewrite_database.h135 std::map<TypeNode, SygusSampler> d_sampler; variable
H A Dexpr_miner.cpp31 d_sampler = ss; in initialize()
/dports/math/cvc4/CVC4-1.7/src/theory/datatypes/
H A Ddatatypes_sygus.h291 std::map<Node, std::map<TypeNode, quantifiers::SygusSampler>> d_sampler; variable
H A Ddatatypes_sygus.cpp1095 d_sampler[a].find(tn); in registerSearchValue()
1096 if (its == d_sampler[a].end()) in registerSearchValue()
1098 d_sampler[a][tn].initializeSygus( in registerSearchValue()
1100 its = d_sampler[a].find(tn); in registerSearchValue()