Home
last modified time | relevance | path

Searched refs:d_tds (Results 1 – 25 of 33) sorted by relevance

12

/dports/math/cvc4/CVC4-1.7/src/theory/quantifiers/
H A Dcandidate_rewrite_database.cpp37 d_tds(nullptr), in CandidateRewriteDatabase()
50 d_tds = nullptr; in initialize()
65 d_tds = d_qe->getTermDatabaseSygus(); in initializeSygus()
67 d_crewrite_filter.initialize(ss, d_tds, d_using_sygus); in initializeSygus()
109 Assert(d_tds != nullptr); in addTerm()
110 solb = d_tds->sygusToBuiltin(sol); in addTerm()
111 eq_solb = d_tds->sygusToBuiltin(eq_sol); in addTerm()
241 Assert(d_tds != nullptr); in addTerm()
247 unsigned sz = d_tds->getSygusTermSize(sol); in addTerm()
248 unsigned eqsz = d_tds->getSygusTermSize(eq_sol); in addTerm()
[all …]
H A Dexpr_miner_manager.cpp30 d_tds(nullptr) in ExpressionMinerManager()
45 d_tds = nullptr; in initialize()
61 d_tds = qe->getTermDatabaseSygus(); in initializeSygus()
63 d_sampler.initializeSygus(d_tds, f, nsamples, useSygusType); in initializeSygus()
138 solb = d_tds->sygusToBuiltin(sol); in addTerm()
H A Dcandidate_rewrite_filter.cpp206 d_tds(nullptr), in CandidateRewriteFilter()
219 d_tds = tds; in initialize()
237 bn = d_tds->sygusToBuiltin(n); in filterPair()
238 beq_n = d_tds->sygusToBuiltin(eq_n); in filterPair()
356 bn = d_tds->sygusToBuiltin(n); in registerRelevantPair()
357 beq_n = d_tds->sygusToBuiltin(eq_n); in registerRelevantPair()
H A Dsygus_sampler.cpp31 : d_tds(nullptr), d_use_sygus_type(false), d_is_valid(false) in SygusSampler()
40 d_tds = nullptr; in initialize()
90 d_tds = tds; in initializeSygus()
275 bn = d_tds->sygusToBuiltin(n); in registerTerm()
696 TypeNode tnc = d_tds->getArgType(dtc, i); in getSygusRandomValue()
711 Node ret = d_tds->mkGeneric(dt, cindex, pre); in getSygusRandomValue()
765 TypeNode tnc = d_tds->getArgType(dtc, j); in registerSygusType()
H A Dexpr_miner_manager.h106 TermDbSygus* d_tds; variable
/dports/math/cvc4/CVC4-1.7/src/theory/datatypes/
H A Dsygus_simple_sym.cpp157 Assert(d_tds->hasKind(tn, k)); in considerArgKind()
158 Assert(d_tds->hasKind(tnp, pk)); in considerArgKind()
162 int c = d_tds->getKindConsNum(tn, k); in considerArgKind()
163 int pc = d_tds->getKindConsNum(tnp, pk); in considerArgKind()
402 if (rt.satisfiedBy(d_tds, tnp)) in considerArgKind()
432 int pc = d_tds->getKindConsNum(tnp, pk); in considerConst()
456 if (d_tds->hasConst(tn, co)) in considerConst()
477 Assert(d_tds->hasKind(tnp, pk)); in considerConst()
478 int pc = d_tds->getKindConsNum(tnp, pk); in considerConst()
502 if (d_tds->hasConst(tnp, sc)) in considerConst()
[all …]
H A Ddatatypes_sygus.cpp40 d_tds(qe->getTermDatabaseSygus()), in SygusSymBreakNew()
939 return d_tds->getFreeVar(tn, 0); in getFreeVar()
1034 Node bv = d_tds->sygusToBuiltin(cnv, tn); in registerSearchValue()
1040 if( d_tds->involvesDivByZero( bvr ) ){ in registerSearchValue()
1143 eset.init(d_tds, tn, aconj, a, bvr); in registerSearchValue()
1287 if (!d_tds->isEnumerator(e)) in registerSizeTerm()
1499 if (d_tds->hasSymBreakLemmas(anchors)) in check()
1511 if (!d_tds->isBasicEnumerator(a)) in check()
1514 d_tds->getSymBreakLemmas(a, sbl); in check()
1532 d_tds->clearSymBreakLemmas(a); in check()
[all …]
H A Dsygus_simple_sym.h90 quantifiers::TermDbSygus* d_tds;
/dports/math/cvc4/CVC4-1.7/src/theory/quantifiers/sygus/
H A Dsygus_pbe.cpp271 Node ag = d_tds->getActiveGuardForEnumerator(e); in initialize()
278 lem = d_tds->getExtRewriter()->extendedRewrite(lem); in initialize()
317 e = d_tds->getSynthFunForEnumerator(e); in hasExamples()
329 e = d_tds->getSynthFunForEnumerator(e); in getNumExamples()
342 e = d_tds->getSynthFunForEnumerator(e); in getExample()
356 e = d_tds->getSynthFunForEnumerator(e); in getExampleOut()
372 if (d_tds->isVariableAgnosticEnumerator(e)) in addSearchVal()
378 Node ee = d_tds->getSynthFunForEnumerator(e); in addSearchVal()
405 e = d_tds->getSynthFunForEnumerator(e); in evaluateBuiltin()
413 return d_tds->evaluateBuiltin(tn, bn, it->second[i]); in evaluateBuiltin()
[all …]
H A Denum_stream_substitution.cpp33 : d_tds(tds), d_first(true), d_curr_ind(0) in EnumStreamPermutation()
52 d_tds->getSubfieldTypes(tn, sf_types); in reset()
87 d_var_classes[d_tds->getSubclassForVar(tn, var)].push_back(var); in reset()
124 d_tds->getExtRewriter()->extendedRewrite(bultin_value)); in getNext()
194 d_tds->getExtRewriter()->extendedRewrite(bultin_perm_value); in getNext()
331 : d_tds(tds), d_stream_permutations(tds), d_curr_ind(0) in EnumStreamSubstitution()
343 d_tds->getSubfieldTypes(tn, sf_types); in initialize()
364 Assert(d_tds->getSubclassForVar(tn, v) > 0); in initialize()
365 d_var_classes[d_tds->getSubclassForVar(tn, v)].push_back(v); in initialize()
513 d_tds->sygusToBuiltin(comb_value, comb_value.getType()); in getNext()
[all …]
H A Dsynth_conjecture.cpp46 d_tds(qe->getTermDatabaseSygus()), in SynthConjecture()
526 lem = d_tds->getEagerUnfold(lem, visited_n); in doCheck()
717 Node g = d_tds->getActiveGuardForEnumerator(e); in getEnumeratedValues()
784 TermDbSygus* d_tds; member in CVC4::theory::quantifiers::EnumValGeneratorBasic
795 bool isEnum = d_tds->isEnumerator(e); in getEnumeratedValue()
808 if (!isEnum || d_tds->isPassiveEnumerator(e)) in getEnumeratedValue()
820 if (d_tds->isVariableAgnosticEnumerator(e)) in getEnumeratedValue()
829 Assert(d_tds->isBasicEnumerator(e)); in getEnumeratedValue()
898 if (!d_tds->isBasicEnumerator(e)) in getEnumeratedValue()
1036 Assert(d_tds->isEnumerator(cprog)); in excludeCurrentSolution()
[all …]
H A Dsygus_unif_io.cpp545 Node res = d_tds->evaluateBuiltin(xtn, bv, d_examples[j]); in computeExamples()
573 Node bv = d_tds->sygusToBuiltin(v, xtn); in notifyEnumeration()
574 bv = d_tds->getExtRewriter()->extendedRewrite(bv); in notifyEnumeration()
582 Evaluator* ev = d_tds->getEvaluator(); in notifyEnumeration()
623 Assert(d_tds->isEnumerator(e)); in notifyEnumeration()
624 bool isPassive = d_tds->isPassiveEnumerator(e); in notifyEnumeration()
725 << d_tds->sygusToBuiltin(v) << std::endl; in notifyEnumeration()
863 d_sol_term_size = d_tds->getSygusTermSize(vcc); in constructSolutionNode()
895 TypeNode xbt = d_tds->sygusToBuiltinType(e.getType()); in useStrContainsEnumeratorExclude()
996 d_tds->getExplain()->getExplanationFor(e, v, exp, ncset); in getExplanationForEnumeratorExclude()
[all …]
H A Dsygus_enumerator.cpp28 : d_tds(tds), d_parent(p), d_tlEnum(nullptr), d_abortSize(-1) in SygusEnumerator()
46 d_tds->getSymBreakLemmas(e, sbl); in initialize()
47 Node ag = d_tds->getActiveGuardForEnumerator(e); in initialize()
56 if (!d_tds->isSymBreakLemmaTemplate(lem)) in initialize()
143 : d_tds(nullptr), in TermCache()
160 d_tds = tds; in initialize()
313 Node bn = d_tds->sygusToBuiltin(n); in addTerm()
314 Node bnr = d_tds->getExtRewriter()->extendedRewrite(bn); in addTerm()
323 d_tds, d_enum, options::sygusSamples(), false); in addTerm()
542 d_tcache[tn].initialize(d_enum, tn, d_tds, pbe); in initializeTermCache()
[all …]
H A Dcegis.cpp84 d_tds->registerSygusType(ctn); in processInitialize()
85 if (d_tds->hasSubtermSymbolicCons(ctn)) in processInitialize()
94 d_tds->registerEnumerator( in processInitialize()
125 if (!d_tds->isPassiveEnumerator(v)) in addEvalLemmas()
242 d_tds->getExplain()->getExplanationForEquality( in constructCandidates()
310 slem = d_tds->getExtRewriter()->extendedRewrite(slem); in addRefinementLemma()
359 if (lem[i].isConst() && d_tds->isEvaluationPoint(lem[1 - i])) in addRefinementLemmaConjunct()
371 if (d_tds->isEvaluationPoint(term)) in addRefinementLemmaConjunct()
475 Node lemcsu = vsit.doEvaluateWithUnfolding(d_tds, lemcs); in getRefinementEvalLemmas()
503 d_tds->getExplain()->getExplanationFor( in getRefinementEvalLemmas()
H A Dsygus_eval_unfold.cpp29 SygusEvalUnfold::SygusEvalUnfold(TermDbSygus* tds) : d_tds(tds) {} in SygusEvalUnfold()
82 SygusExplain* sy_exp = d_tds->getExplain(); in registerModelValue()
116 Node bTerm = d_tds->sygusToBuiltin(vn, tn); in registerModelValue()
151 res = d_tds->unfold(eval_fun, vtm, exp); in registerModelValue()
162 res = d_tds->evaluateWithUnfolding(eval_fun); in registerModelValue()
H A Dcegis_unif.cpp61 d_tds->registerEnumerator(f, f, d_parent, eroleNonUnif); in processInitialize()
203 unsigned prev_size = d_tds->getSygusTermSize(prev_val); in getEnumValues()
204 unsigned curr_size = d_tds->getSygusTermSize(curr_val); in getEnumValues()
254 Assert(d_tds->isEnumerator(eu)); in setConditions()
256 if (d_tds->isPassiveEnumerator(eu)) in setConditions()
258 Node g = d_tds->getActiveGuardForEnumerator(eu); in setConditions()
259 Node exp_exc = d_tds->getExplain() in setConditions()
346 << "... " << d_tds->sygusToBuiltin(sol, sol.getType()) << "\n"; in processConstructCandidates()
400 d_tds = d_qe->getTermDatabaseSygus(); in CegisUnifEnumDecisionStrategy()
470 d_tds->registerEnumerator( in mkLiteral()
[all …]
H A Dsygus_unif.cpp30 : d_qe(nullptr), d_tds(nullptr), d_enableMinimality(false) in SygusUnif()
42 d_tds = qe->getTermDatabaseSygus(); in initializeCandidate()
59 ssize = d_tds->getSygusTermSize(n); in getMinimalTerm()
H A Dsygus_unif_rl.cpp109 nv = d_tds->evaluateWithUnfolding(tmp); in purifyLemma()
530 << d_unif->d_tds->sygusToBuiltin(condv, condv.getType()) << "\n"; in setConditions()
878 << d_dt->d_unif->d_tds->sygusToBuiltin( in extractSol()
911 << d_dt->d_unif->d_tds->sygusToBuiltin(d_dt->d_conds[index], in extractSol()
914 << d_dt->d_unif->d_tds->sygusToBuiltin(cache[cur], in extractSol()
955 << d_unif->d_tds->sygusToBuiltin( in recomputeSolHeuristically()
989 << (d_unif->d_tds->sygusToBuiltin(v1, v1.getType()) in buildDtInfoGain()
1026 << d_unif->d_tds->sygusToBuiltin( in buildDtInfoGain()
1060 TermDbSygus* tds = d_unif->d_tds; in getEntropy()
1104 Node builtin_cond = d_dt->d_unif->d_tds->sygusToBuiltin(cond, tn); in computeCond()
[all …]
H A Dsygus_repair_const.cpp37 d_tds = d_qe->getTermDatabaseSygus(); in SygusRepairConst()
89 TypeNode tnc = d_tds->getArgType(dtc, j); in registerSygusType()
290 Node fov_m_to_sygus = d_tds->getProxyVariable(v.getType(), fov_m); in repairSolution()
389 Node sk_var = d_tds->getFreeVarInc(n.getType(), free_var_count); in getSkeleton()
434 child = d_tds->getFreeVarInc(cn.getType(), free_var_count); in getSkeleton()
476 body = d_tds->evaluateWithUnfolding(body); in getFoQuery()
485 TypeNode builtinType = d_tds->sygusToBuiltinType(v.getType()); in getFoQuery()
H A Denum_stream_substitution.h73 quantifiers::TermDbSygus* d_tds;
214 quantifiers::TermDbSygus* d_tds;
H A Dsygus_module.cpp22 : d_qe(qe), d_tds(qe->getTermDatabaseSygus()), d_parent(p) in SygusModule()
H A Dsygus_enumerator.h60 TermDbSygus* d_tds;
149 TermDbSygus* d_tds; variable
H A Dsygus_grammar_norm.h134 : d_qe(qe), d_tds(d_qe->getTermDatabaseSygus()) in SygusGrammarNorm()
399 TermDbSygus* d_tds; variable
H A Dsygus_eval_unfold.h89 TermDbSygus* d_tds;
H A Dsygus_module.h142 quantifiers::TermDbSygus* d_tds; variable

12