Home
last modified time | relevance | path

Searched refs:quantifiers (Results 1 – 25 of 1213) sorted by relevance

12345678910>>...49

/dports/math/cvc4/CVC4-1.7/src/theory/
H A Dquantifiers_engine.h43 namespace quantifiers {
117 quantifiers::BvInverter* getBvInverter() const;
123 quantifiers::QuantEPR* getQuantEPR() const;
125 quantifiers::FirstOrderModel* getModel() const;
127 quantifiers::TermDb* getTermDatabase() const;
131 quantifiers::TermUtil* getTermUtil() const;
137 quantifiers::Instantiate* getInstantiate() const;
139 quantifiers::Skolemize* getSkolemize() const;
229 quantifiers::UserPatMode getInstUserPatMode();
344 std::unique_ptr<quantifiers::QuantEPR> d_qepr;
[all …]
H A Dquantifiers_engine.cpp83 d_term_util(new quantifiers::TermUtil(this)), in QuantifiersEngine()
84 d_term_canon(new quantifiers::TermCanonize), in QuantifiersEngine()
85 d_term_db(new quantifiers::TermDb(c, u, this)), in QuantifiersEngine()
89 d_skolemize(new quantifiers::Skolemize(this, u)), in QuantifiersEngine()
90 d_term_enum(new quantifiers::TermEnumeration), in QuantifiersEngine()
153 d_quant_rel.reset(new quantifiers::QuantRelevance); in QuantifiersEngine()
159 d_qepr.reset(new quantifiers::QuantEPR); in QuantifiersEngine()
190 d_bv_invert.reset(new quantifiers::BvInverter); in QuantifiersEngine()
230 d_fs.reset(new quantifiers::InstStrategyEnum(this)); in QuantifiersEngine()
243 if (options::mbqiMode() == quantifiers::MBQI_FMC in QuantifiersEngine()
[all …]
/dports/math/cvc4/CVC4-1.7/src/options/
H A Dquantifiers_modes.cpp25 case theory::quantifiers::INST_WHEN_PRE_FULL: in operator <<()
28 case theory::quantifiers::INST_WHEN_FULL: in operator <<()
31 case theory::quantifiers::INST_WHEN_FULL_LAST_CALL: in operator <<()
34 case theory::quantifiers::INST_WHEN_LAST_CALL: in operator <<()
46 case theory::quantifiers::LITERAL_MATCH_NONE: in operator <<()
49 case theory::quantifiers::LITERAL_MATCH_USE: in operator <<()
52 case theory::quantifiers::LITERAL_MATCH_AGG_PREDICATE: in operator <<()
55 case theory::quantifiers::LITERAL_MATCH_AGG: in operator <<()
67 case theory::quantifiers::MBQI_NONE: in operator <<()
70 case theory::quantifiers::MBQI_FMC: in operator <<()
[all …]
H A Doptions_handler.cpp662 return theory::quantifiers::MBQI_NONE; in stringToMbqiMode()
664 return theory::quantifiers::MBQI_FMC; in stringToMbqiMode()
666 return theory::quantifiers::MBQI_TRUST; in stringToMbqiMode()
707 return theory::quantifiers::QCF_PROP_EQ; in stringToQcfMode()
761 theory::quantifiers::TriggerActiveSelMode
826 return theory::quantifiers::TERM_DB_ALL; in stringToTermDbMode()
884 theory::quantifiers::CegqiSingleInvMode
903 theory::quantifiers::CegqiSingleInvRconsMode
963 theory::quantifiers::SygusFilterSolMode
992 theory::quantifiers::SygusInvTemplMode
[all …]
H A Doptions_handler.h85 theory::quantifiers::InstWhenMode mode);
86 theory::quantifiers::LiteralMatchMode stringToLiteralMatchMode(
90 theory::quantifiers::MbqiMode stringToMbqiMode(std::string option,
95 theory::quantifiers::QcfMode stringToQcfMode(std::string option,
99 theory::quantifiers::TriggerSelMode stringToTriggerSelMode(
103 theory::quantifiers::PrenexQuantMode stringToPrenexQuantMode(
107 theory::quantifiers::IteLiftQuantMode stringToIteLiftQuantMode(
109 theory::quantifiers::CbqiBvIneqMode stringToCbqiBvIneqMode(
115 theory::quantifiers::CegisSampleMode stringToCegisSampleMode(
123 theory::quantifiers::MacrosQuantMode stringToMacrosQuantMode(
[all …]
H A Dquantifiers_options.toml5 # Whether to mini-scope quantifiers.
14 help = "miniscope quantifiers"
25 help = "miniscope quantifiers for ground subformulas"
39 type = "CVC4::theory::quantifiers::PrenexQuantMode"
53 # Whether to variable-eliminate quantifiers.
203 type = "CVC4::theory::quantifiers::TermDbMode"
204 default = "CVC4::theory::quantifiers::TERM_DB_ALL"
519 type = "CVC4::theory::quantifiers::MbqiMode"
520 default = "CVC4::theory::quantifiers::MBQI_FMC"
641 type = "CVC4::theory::quantifiers::QcfMode"
[all …]
/dports/math/rumur/rumur-2021.09.29/rumur/src/
H A Dgenerate-model.cc71 for (const Quantifier &q : s->quantifiers) in generate_model()
138 for (const Quantifier &q : p->quantifiers) in generate_model()
179 for (const Quantifier &q : s->quantifiers) in generate_model()
227 for (const Quantifier &q : s->quantifiers) in generate_model()
336 for (auto it = r->quantifiers.rbegin(); in generate_model()
337 it != r->quantifiers.rend(); it++) in generate_model()
708 for (auto it = r->quantifiers.rbegin(); it != r->quantifiers.rend(); in generate_model()
908 for (auto it = r->quantifiers.rbegin(); it != r->quantifiers.rend(); in generate_model()
1085 for (auto it = r->quantifiers.rbegin(); it != r->quantifiers.rend(); in generate_model()
1271 for (auto it = r->quantifiers.rbegin(); it != r->quantifiers.rend(); in generate_model()
[all …]
/dports/math/cvc4/CVC4-1.7/src/theory/quantifiers/
H A Dkinds7 theory THEORY_QUANTIFIERS ::CVC4::theory::quantifiers::TheoryQuantifiers "theory/quantifiers/theory…
8 typechecker "theory/quantifiers/theory_quantifiers_type_rules.h"
12 rewriter ::CVC4::theory::quantifiers::QuantifiersRewriter "theory/quantifiers/quantifiers_rewriter.…
49 typerule FORALL ::CVC4::theory::quantifiers::QuantifierForallTypeRule
50 typerule EXISTS ::CVC4::theory::quantifiers::QuantifierExistsTypeRule
52 typerule INST_PATTERN ::CVC4::theory::quantifiers::QuantifierInstPatternTypeRule
56 typerule INST_CLOSURE ::CVC4::theory::quantifiers::QuantifierInstClosureTypeRule
74 typerule REWRITE_RULE ::CVC4::theory::quantifiers::RewriteRuleTypeRule
75 typerule RR_REWRITE ::CVC4::theory::quantifiers::RRRewriteTypeRule
76 typerule RR_REDUCTION ::CVC4::theory::quantifiers::RRRedDedTypeRule
[all …]
H A Dequality_query.cpp32 namespace quantifiers { namespace
130 if( r.isConst() && quantifiers::TermUtil::containsUninterpretedConstant( r ) ){ in getInternalRepresentative()
148 if( options::quantRepMode()==quantifiers::QUANT_REP_MODE_EE ){ in getInternalRepresentative()
262 if( options::cbqi() && quantifiers::TermUtil::hasInstConstAttr(n) ){ //reject in getRepScore()
276 if( options::quantRepMode()==quantifiers::QUANT_REP_MODE_FIRST ){ in getRepScore()
280 Assert( options::quantRepMode()==quantifiers::QUANT_REP_MODE_DEPTH ); in getRepScore()
281 return quantifiers::TermUtil::getTermDepth( n ); in getRepScore()
H A Dquant_util.cpp49 quantifiers::TermDb * QuantifiersModule::getTermDatabase() { in getTermDatabase()
53 quantifiers::TermUtil * QuantifiersModule::getTermUtil() { in getTermUtil()
77 if( quantifiers::TermUtil::hasInstConstAttr(it->first[0]) ){ in initialize()
78 if( !quantifiers::TermUtil::hasInstConstAttr(it->first[1]) ){ in initialize()
83 }else if( quantifiers::TermUtil::hasInstConstAttr(it->first[1]) ){ in initialize()
/dports/math/rumur/rumur-2021.09.29/murphi2c/src/
H A Dgenerate_h.cc79 if (n.quantifiers.empty()) { in visit_propertyrule()
83 for (const Quantifier &q : n.quantifiers) { in visit_propertyrule()
102 if (n.quantifiers.empty()) { in visit_simplerule()
106 for (const Quantifier &q : n.quantifiers) { in visit_simplerule()
123 if (n.quantifiers.empty()) { in visit_simplerule()
127 for (const Quantifier &q : n.quantifiers) { in visit_simplerule()
149 if (n.quantifiers.empty()) { in visit_startstate()
153 for (const Quantifier &q : n.quantifiers) { in visit_startstate()
H A Dgenerate_c.cc90 if (n.quantifiers.empty()) { in visit_propertyrule()
94 for (const Quantifier &q : n.quantifiers) { in visit_propertyrule()
129 if (n.quantifiers.empty()) { in visit_simplerule()
133 for (const Quantifier &q : n.quantifiers) { in visit_simplerule()
172 if (n.quantifiers.empty()) { in visit_simplerule()
176 for (const Quantifier &q : n.quantifiers) { in visit_simplerule()
224 if (n.quantifiers.empty()) { in visit_startstate()
228 for (const Quantifier &q : n.quantifiers) { in visit_startstate()
/dports/math/cvc4/CVC4-1.7/src/theory/quantifiers/sygus/
H A Denum_stream_substitution.h26 namespace quantifiers {
36 EnumStreamPermutation(quantifiers::TermDbSygus* tds);
73 quantifiers::TermDbSygus* d_tds;
168 EnumStreamSubstitution(quantifiers::TermDbSygus* tds);
214 quantifiers::TermDbSygus* d_tds;
284 EnumStreamConcrete(quantifiers::TermDbSygus* tds) : d_ess(tds) {} in EnumStreamConcrete()
/dports/math/cvc4/CVC4-1.7/src/theory/quantifiers/ematching/
H A Dtrigger.cpp140 quantifiers::TermUtil::computeInstConstContainsForQuant( in mkTriggerTerms()
147 Assert( quantifiers::TermUtil::getInstConstAttr(v)==q ); in mkTriggerTerms()
258 if( quantifiers::TermUtil::getInstConstAttr(n)==q ){ in isUsable()
301 if( !quantifiers::TermUtil::hasInstConstAttr(n2) ){ in isUsableEqTerms()
313 else if (!quantifiers::TermUtil::hasInstConstAttr(n2)) in isUsableEqTerms()
408 if( !quantifiers::TermUtil::hasInstConstAttr( t[1] ) ){ in isSimpleTrigger()
490 …if( tstrt==quantifiers::TRIGGER_SEL_MAX || ( tstrt==quantifiers::TRIGGER_SEL_MIN_SINGLE_MAX && !nu… in collectPatTerms2()
513 …if( rm_nu && ( tstrt==quantifiers::TRIGGER_SEL_MIN || ( tstrt==quantifiers::TRIGGER_SEL_MIN_SINGLE… in collectPatTerms2()
630 if( tstrt==quantifiers::TRIGGER_SEL_ALL ){ in collectPatTerms()
803 if( quantifiers::TermUtil::hasInstConstAttr(n[i]) ){ in getInversionVariable()
[all …]
/dports/math/rumur/rumur-2021.09.29/murphi2uclid/src/
H A Dcheck.cc184 for (const Quantifier &q : n.quantifiers) { in visit_ruleset()
193 assert(params.size() >= n.quantifiers.size() && in visit_ruleset()
195 for (size_t i = 0; i < n.quantifiers.size(); ++i) { in visit_ruleset()
197 = params.size() - n.quantifiers.size() + i; in visit_ruleset()
198 assert(params[j] == &n.quantifiers[i] && in visit_ruleset()
203 params.resize(params.size() - n.quantifiers.size()); in visit_ruleset()
209 for (const Quantifier &q : n.quantifiers) in visit_simplerule()
232 for (const Quantifier &q : n.quantifiers) in visit_startstate()
/dports/math/py-mathics/Mathics3-2.2.0/mathics/packages/analytica/
H A Dquantify.m7 (* Convert multi-variable quantifiers into single variable
8 quantifiers. *)
19 (* Reduce scope of quantifiers when possible. *)
49 (* Convert restricted quantifiers into ordinary quantifiers. *)
125 (* Add quantifiers back to Skolemized formula for output. *)
/dports/math/z3/z3-z3-4.8.13/src/params/
H A Dpattern_inference_params_helper.pyg9 …('arith_weight', UINT, 5, 'default weight for quantifiers where the only available pattern has nes…
10 …('non_nested_arith_weight', UINT, 10, 'default weight for quantifiers where the only available pat…
11 … ('pull_quantifiers', BOOL, True, 'pull nested quantifiers, if no pattern was found'),
/dports/math/py-z3-solver/z3-z3-4.8.10/src/params/
H A Dpattern_inference_params_helper.pyg9 …('arith_weight', UINT, 5, 'default weight for quantifiers where the only available pattern has nes…
10 …('non_nested_arith_weight', UINT, 10, 'default weight for quantifiers where the only available pat…
11 … ('pull_quantifiers', BOOL, True, 'pull nested quantifiers, if no pattern was found'),
/dports/math/rumur/rumur-2021.09.29/librumur/src/
H A DRule.cc136 quantifiers = quantifiers_; in Ruleset()
142 for (const Quantifier &q : quantifiers) { in validate()
159 for (const Quantifier &q : quantifiers) in flatten()
160 f->quantifiers.push_back(q); in flatten()
H A Dtraverse.cc172 for (Quantifier &q : n.quantifiers) in visit_propertyrule()
213 for (Quantifier &q : n.quantifiers) in visit_ruleset()
222 for (Quantifier &q : n.quantifiers) in visit_simplerule()
233 for (Quantifier &q : n.quantifiers) in visit_startstate()
443 for (const Quantifier &q : n.quantifiers) in visit_propertyrule()
486 for (const Quantifier &q : n.quantifiers) in visit_ruleset()
495 for (const Quantifier &q : n.quantifiers) in visit_simplerule()
506 for (const Quantifier &q : n.quantifiers) in visit_startstate()
639 for (const Quantifier &q : n.quantifiers) in visit_propertyrule()
680 for (const Quantifier &q : n.quantifiers) in visit_ruleset()
[all …]
/dports/devel/godot2-tools/godot-2.1.6-stable/drivers/nrex/
H A DREADME.md29 * Simple quantifiers `?`, `*` and `+`
30 * Range quantifiers `{0,1}`
31 * Lazy (non-greedy) quantifiers `*?`
70 * Fixed parents of recursive quantifiers not expanding properly
/dports/devel/godot2/godot-2.1.6-stable/drivers/nrex/
H A DREADME.md29 * Simple quantifiers `?`, `*` and `+`
30 * Range quantifiers `{0,1}`
31 * Lazy (non-greedy) quantifiers `*?`
70 * Fixed parents of recursive quantifiers not expanding properly
/dports/math/rumur/rumur-2021.09.29/murphi2murphi/src/
H A DPrinter.cc291 if (!n.quantifiers.empty()) { in visit_propertyrule()
292 top->sync_to(n.quantifiers[0]); in visit_propertyrule()
293 for (const Quantifier &q : n.quantifiers) { in visit_propertyrule()
371 if (!n.quantifiers.empty()) { in visit_ruleset()
372 top->sync_to(n.quantifiers[0]); in visit_ruleset()
373 for (const Quantifier &q : n.quantifiers) { in visit_ruleset()
397 if (!n.quantifiers.empty()) { in visit_simplerule()
398 top->sync_to(n.quantifiers[0]); in visit_simplerule()
399 for (const Quantifier &q : n.quantifiers) { in visit_simplerule()
427 if (!n.quantifiers.empty()) { in visit_startstate()
[all …]
/dports/security/hs-cryptol/cryptol-2.11.0/_cabal_deps/sbv-8.12/Data/SBV/SMT/
H A DSMTLib.hs67 | isSat = ALL `elem` quantifiers
68 | True = EX `elem` quantifiers
69 where quantifiers = map fst (fst qinps) function
/dports/math/z3/z3-z3-4.8.13/src/ast/normal_forms/
H A Dnnf_params.pyg7 …'NNF translation mode: skolem (skolem normal form), quantifiers (skolem normal form + quantifiers …

12345678910>>...49