/dports/math/cvc4/CVC4-1.7/src/theory/quantifiers/ |
H A D | candidate_rewrite_database.cpp | 37 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 D | expr_miner_manager.cpp | 30 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 D | candidate_rewrite_filter.cpp | 206 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 D | sygus_sampler.cpp | 31 : 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 D | expr_miner_manager.h | 106 TermDbSygus* d_tds; variable
|
/dports/math/cvc4/CVC4-1.7/src/theory/datatypes/ |
H A D | sygus_simple_sym.cpp | 157 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 D | datatypes_sygus.cpp | 40 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 D | sygus_simple_sym.h | 90 quantifiers::TermDbSygus* d_tds;
|
/dports/math/cvc4/CVC4-1.7/src/theory/quantifiers/sygus/ |
H A D | sygus_pbe.cpp | 271 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 D | enum_stream_substitution.cpp | 33 : 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 D | synth_conjecture.cpp | 46 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 D | sygus_unif_io.cpp | 545 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 D | sygus_enumerator.cpp | 28 : 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 D | cegis.cpp | 84 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 D | sygus_eval_unfold.cpp | 29 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 D | cegis_unif.cpp | 61 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 D | sygus_unif.cpp | 30 : 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 D | sygus_unif_rl.cpp | 109 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 D | sygus_repair_const.cpp | 37 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 D | enum_stream_substitution.h | 73 quantifiers::TermDbSygus* d_tds; 214 quantifiers::TermDbSygus* d_tds;
|
H A D | sygus_module.cpp | 22 : d_qe(qe), d_tds(qe->getTermDatabaseSygus()), d_parent(p) in SygusModule()
|
H A D | sygus_enumerator.h | 60 TermDbSygus* d_tds; 149 TermDbSygus* d_tds; variable
|
H A D | sygus_grammar_norm.h | 134 : d_qe(qe), d_tds(d_qe->getTermDatabaseSygus()) in SygusGrammarNorm() 399 TermDbSygus* d_tds; variable
|
H A D | sygus_eval_unfold.h | 89 TermDbSygus* d_tds;
|
H A D | sygus_module.h | 142 quantifiers::TermDbSygus* d_tds; variable
|