Searched refs:d_sampler (Results 1 – 9 of 9) sorted by relevance
/dports/math/cvc4/CVC4-1.7/src/theory/quantifiers/ |
H A D | expr_miner_manager.cpp | 47 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 D | query_generator.cpp | 54 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 D | expr_miner.h | 41 ExprMiner() : d_sampler(nullptr) {} in ExprMiner() 65 SygusSampler* d_sampler; variable
|
H A D | candidate_rewrite_database.cpp | 96 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 D | expr_miner_manager.h | 114 SygusSampler d_sampler; variable
|
H A D | candidate_rewrite_database.h | 135 std::map<TypeNode, SygusSampler> d_sampler; variable
|
H A D | expr_miner.cpp | 31 d_sampler = ss; in initialize()
|
/dports/math/cvc4/CVC4-1.7/src/theory/datatypes/ |
H A D | datatypes_sygus.h | 291 std::map<Node, std::map<TypeNode, quantifiers::SygusSampler>> d_sampler; variable
|
H A D | datatypes_sygus.cpp | 1095 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()
|