Home
last modified time | relevance | path

Searched refs:lemmas (Results 1 – 25 of 304) sorted by relevance

12345678910>>...13

/dports/textproc/py-nltk/nltk-3.4.1/nltk/metrics/
H A Dpaice.py26 def get_words_from_dictionary(lemmas): argument
37 for lemma in lemmas:
38 words.update(set(lemmas[lemma]))
138 def _calculate(lemmas, stems): argument
154 n = sum(len(lemmas[word]) for word in lemmas)
158 for lemma in lemmas:
219 def __init__(self, lemmas, stems): argument
228 self.lemmas = lemmas
346 lemmas = {
360 for lemma in sorted(lemmas):
[all …]
/dports/math/cvc4/CVC4-1.7/src/theory/datatypes/
H A Ddatatypes_sygus.h93 void assertFact(Node n, bool polarity, std::vector<Node>& lemmas);
100 void preRegisterTerm(TNode n, std::vector<Node>& lemmas);
109 void check(std::vector<Node>& lemmas);
319 void registerTerm(Node n, std::vector<Node>& lemmas);
393 std::vector<Node>& lemmas,
436 std::vector<Node>& lemmas);
556 void registerSizeTerm(Node e, std::vector<Node>& lemmas);
596 Node getOrMkMeasureValue(std::vector<Node>& lemmas);
614 Node getOrMkActiveMeasureValue(std::vector<Node>& lemmas,
653 void incrementCurrentSearchSize( Node m, std::vector< Node >& lemmas );
[all …]
H A Ddatatypes_sygus.cpp57 registerTerm( n, lemmas ); in assertTester()
114 lemmas.push_back( blem ); in assertFact()
173 registerTerm( n[0], lemmas ); in registerTerm()
356 lemmas.push_back(sslem); in assertTesterInternal()
1170 std::vector<Node>& lemmas) in registerSymBreakLemmaForValue() argument
1349 lemmas.push_back(slem); in registerSizeTerm()
1536 if (!lemmas.empty()) in check()
1619 return check(lemmas); in check()
1624 if (lemmas.empty()) in check()
1695 lemmas.push_back( split ); in checkValue()
[all …]
/dports/math/cvc4/CVC4-1.7/src/theory/sets/
H A Dtheory_sets_private.h59 …void assertInference( Node fact, Node exp, std::vector< Node >& lemmas, const char * c, int inferT…
66 void checkSubtypes( std::vector< Node >& lemmas );
67 void checkDownwardsClosure( std::vector< Node >& lemmas );
68 void checkUpwardsClosure( std::vector< Node >& lemmas );
69 void checkDisequalities( std::vector< Node >& lemmas );
73 void flushLemmas( std::vector< Node >& lemmas, bool preprocess = false );
170 void checkCardBuildGraph( std::vector< Node >& lemmas );
171 void registerCardinalityTerm( Node n, std::vector< Node >& lemmas );
172 void checkCardCycles( std::vector< Node >& lemmas );
174 void checkNormalForms( std::vector< Node >& lemmas, std::vector< Node >& intro_sets );
[all …]
H A Dtheory_sets_private.cpp497 std::vector< Node > lemmas; in split() local
498 lemmas.push_back( lem ); in split()
499 flushLemmas( lemmas ); in split()
536 std::vector< Node > lemmas; in fullEffortCheck() local
671 flushLemmas( lemmas ); in fullEffortCheck()
691 checkSubtypes( lemmas ); in fullEffortCheck()
697 flushLemmas( lemmas ); in fullEffortCheck()
701 flushLemmas( lemmas ); in fullEffortCheck()
1096 flushLemmas( lemmas ); in checkCardCycles()
1115 flushLemmas( lemmas ); in checkCardCyclesRec()
[all …]
/dports/math/z3/z3-z3-4.8.13/src/muz/spacer/
H A Dspacer_json.cpp79 static std::ostream &json_marshal(std::ostream &out, const lemma_ref_vector &lemmas) { in json_marshal() argument
82 for (auto l:lemmas) { in json_marshal()
123 for (auto *l : n->lemmas()) { in marshal_lemmas_new()
142 std::ostringstream lemmas; in marshal() local
145 marshal_lemmas_old(lemmas); in marshal()
147 marshal_lemmas_new(lemmas); in marshal()
187 out << "\"lemmas\":{\n" << lemmas.str() << "\n}\n}\n"; in marshal()
/dports/math/py-z3-solver/z3-z3-4.8.10/src/muz/spacer/
H A Dspacer_json.cpp79 static std::ostream &json_marshal(std::ostream &out, const lemma_ref_vector &lemmas) { in json_marshal() argument
82 for (auto l:lemmas) { in json_marshal()
123 for (auto *l : n->lemmas()) { in marshal_lemmas_new()
142 std::ostringstream lemmas; in marshal() local
145 marshal_lemmas_old(lemmas); in marshal()
147 marshal_lemmas_new(lemmas); in marshal()
187 out << "\"lemmas\":{\n" << lemmas.str() << "\n}\n}\n"; in marshal()
/dports/math/cvc4/CVC4-1.7/src/options/
H A Ddatatypes_options.toml64 long = "dt-infer-as-lemmas"
68 help = "always send lemmas out instead of making internal inferences"
77 help = "when applicable, blast splitting lemmas for all variables at once"
95 help = "simple sygus symmetry breaking lemmas"
104 help = "use aggressive checks for simple sygus symmetry breaking lemmas"
113 help = "dynamic sygus symmetry breaking lemmas"
121 help = "sygus symmetry breaking lemmas based on pbe conjectures"
139 help = "lazily add symmetry breaking lemmas for terms"
148 help = "add relevancy conditions to symmetry breaking lemmas"
H A Dsets_options.toml8 long = "sets-proxy-lemmas"
12 help = "introduce proxy variables eagerly to shorten lemmas"
17 long = "sets-infer-as-lemmas"
21 help = "send inferences as lemmas"
/dports/math/cvc4/CVC4-1.7/contrib/
H A Drun-script-smtcomp2017-unsat-cores20 …finishwith --enable-miplib-trick --miplib-trick-subs=4 --use-approx --lemmas-on-replay-failure --r…
57 finishwith --no-arrays-eager-index --arrays-eager-lemmas --decision=justification
60 finishwith --no-arrays-eager-index --arrays-eager-lemmas --decision=internal
63 finishwith --decision=justification --no-arrays-eager-index --arrays-eager-lemmas
66 finishwith --decision=justification-stoponly --no-arrays-eager-index --arrays-eager-lemmas
H A Drun-script-smtcomp2018-unsat-cores20 …finishwith --miplib-trick --miplib-trick-subs=4 --use-approx --lemmas-on-replay-failure --replay-e…
57 finishwith --no-arrays-eager-index --arrays-eager-lemmas --decision=justification
60 finishwith --no-arrays-eager-index --arrays-eager-lemmas --decision=internal
63 finishwith --decision=justification --no-arrays-eager-index --arrays-eager-lemmas
66 finishwith --decision=justification-stoponly --no-arrays-eager-index --arrays-eager-lemmas
H A Drun-script-smtcomp201629 …trywith 200 --enable-miplib-trick --miplib-trick-subs=4 --use-approx --lemmas-on-replay-failure --…
34 …finishwith --enable-miplib-trick --miplib-trick-subs=4 --use-approx --lemmas-on-replay-failure --r…
116 finishwith --no-arrays-eager-index --arrays-eager-lemmas --decision=justification
119 finishwith --no-arrays-eager-index --arrays-eager-lemmas --decision=internal
122 finishwith --decision=justification --no-arrays-eager-index --arrays-eager-lemmas
126 finishwith --decision=justification-stoponly --no-arrays-eager-index --arrays-eager-lemmas
H A Drun-script-smtcomp2014-application29 …runcvc4 --enable-miplib-trick --miplib-trick-subs=4 --lemmas-on-replay-failure --replay-early-clos…
33 …runcvc4 --enable-miplib-trick --miplib-trick-subs=4 --lemmas-on-replay-failure --replay-early-clos…
45 runcvc4 --no-arrays-eager-index --arrays-eager-lemmas
H A Drun-script-smtcomp201729 …trywith 200 --enable-miplib-trick --miplib-trick-subs=4 --use-approx --lemmas-on-replay-failure --…
34 …finishwith --enable-miplib-trick --miplib-trick-subs=4 --use-approx --lemmas-on-replay-failure --r…
134 finishwith --no-arrays-eager-index --arrays-eager-lemmas --decision=justification
137 finishwith --no-arrays-eager-index --arrays-eager-lemmas --decision=internal
140 finishwith --decision=justification --no-arrays-eager-index --arrays-eager-lemmas
144 finishwith --decision=justification-stoponly --no-arrays-eager-index --arrays-eager-lemmas
/dports/textproc/zorba/zorba-2.7.0/scripts/
H A Dzt-wn-compile98 my @lemmas;
122 @lemmas = sort keys %index;
124 map { $index{ $_ }{ id } = $lemma_id++ } @lemmas;
187 map { push( @words, $lemmas[ $_ ] ) } @{ $synsets{ $ss_key }{ word_ids } };
312 my $num_lemmas = @lemmas;
328 for my $lemma ( @lemmas ) {
/dports/textproc/py-nltk/nltk-3.4.1/nltk/stem/
H A Dwordnet.py41 lemmas = wordnet._morphy(word, pos)
42 return min(lemmas, key=len) if lemmas else word
/dports/math/cadical/cadical-1.0.3-cb89cbf/test/cnf/
H A Ddrat-trim.c331 while (*lemmas) { in printProof()
332 int lit = *lemmas++; in printProof()
336 while (*lemmas) { in printProof()
337 int lit = *lemmas++; in printProof()
924 S->time = lemmas[ID]; in verify()
930 int lit = lemmas[0]; in verify()
950 removeWatch (S, lemmas, 0), removeWatch (S, lemmas, 1); in verify()
953 removeWatch (S, lemmas, 0), removeWatch (S, lemmas, 1); } in verify()
976 if (lemmas[1]) in verify()
977 addWatch (S, lemmas, 0), addWatch (S, lemmas, 1); in verify()
[all …]
/dports/math/cvc4/CVC4-1.7/src/theory/quantifiers/sygus/
H A Dsygus_unif_rl.h61 void notifyEnumeration(Node e, Node v, std::vector<Node>& lemmas) override;
64 std::vector<Node>& lemmas) override;
117 std::vector<Node>& lemmas) override;
214 Node buildSol(Node cons, std::vector<Node>& lemmas);
216 Node buildSolAllCond(Node cons, std::vector<Node>& lemmas);
229 Node buildSolMinCond(Node cons, std::vector<Node>& lemmas);
/dports/textproc/py-nltk/nltk-3.4.1/nltk/test/
H A Dpaice.doctest6 Given a list of words with their real lemmas and stems according to stemming algorithm under evalua…
16 >>> lemmas = {'kneel': ['kneel', 'knelt'],
24 >>> p = Paice(lemmas, stems)
/dports/math/cvc4/CVC4-1.7/src/theory/quantifiers/
H A Dquant_split.cpp91 std::vector< Node > lemmas; in check() local
134 … lemmas.push_back( disj.size()==1 ? disj[0] : NodeManager::currentNM()->mkNode( kind::OR, disj ) ); in check()
140 for( unsigned i=0; i<lemmas.size(); i++ ){ in check()
141 Trace("quant-dsplit") << "QuantDSplit lemma : " << lemmas[i] << std::endl; in check()
142 d_quantEngine->addLemma( lemmas[i], false ); in check()
/dports/math/cvc4/CVC4-1.7/src/theory/arith/
H A Dnonlinear_extension.cpp703 lemmas.clear(); in flushLemmas()
1870 return lemmas; in checkSplitZero()
2273 d_waiting_lemmas.end(), lemmas.begin(), lemmas.end()); in checkLastCall()
2280 d_waiting_lemmas.end(), lemmas.begin(), lemmas.end()); in checkLastCall()
3140 return lemmas; in checkMonomialSign()
3372 return lemmas; in checkTangentPlanes()
3590 return lemmas; in checkMonomialInferBounds()
3705 return lemmas; in checkFactoring()
3863 return lemmas; in checkMonomialInferResBounds()
3969 return lemmas; in checkTranscendentalInitialRefine()
[all …]
/dports/math/yices/yices-2.6.2/src/mcsat/bool/
H A Dbool_plugin.c51 ivector_t lemmas; member
140 init_ivector(&bp->lemmas, 0); in bool_plugin_construct()
173 delete_ivector(&bp->lemmas); in bool_plugin_destruct()
226 ivector_push(&bp->lemmas, clause_ref); in bool_plugin_new_lemma_notify()
390 for (i = 0; i < bp->lemmas.size; ++ i) { in bool_plugin_rescale_clause_scores()
391 clause = bp->lemmas.data[i]; in bool_plugin_rescale_clause_scores()
843 …int_array_sort2(bp->lemmas.data, bp->lemmas.size, (void*) db, bool_plugin_clause_compare_for_remov… in bool_plugin_gc_mark()
847 clause_ref = bp->lemmas.data[i]; in bool_plugin_gc_mark()
930 clause_ref = bp->lemmas.data[i]; in bool_plugin_remove_stale_clauses()
937 ivector_shrink(&bp->lemmas, to_keep); in bool_plugin_remove_stale_clauses()
[all …]
/dports/textproc/irstlm/irstlm-5.80.03/src/
H A Dlmmacro.cpp636 char *lemmas[BUFSIZ]; in map() local
670 lemmas[i] = strdup(lemma); in map()
673 lemmas[i] = strdup("_unk_"); in map()
678 Micro2MacroMapping(&tag_ng, out, lemmas); in map()
752 void lmmacro::Micro2MacroMapping(ngram *in, ngram *out, char **lemmas) in Micro2MacroMapping() argument
762 …BOSE(3,"lemmas[" << i << "]=" << lemmas[i] << " -> class -> " << lexicaltoken2classMap[lmtable::ge… in Micro2MacroMapping()
765 VERBOSE(3,"lemmas[" << i << "]=" << lemmas[i] << endl); in Micro2MacroMapping()
777 const char *curr_lemma = lemmas[i]; in Micro2MacroMapping()
787 sprintf(tag_lemma, "%s_%s", curr_macrotag, lemmas[microsize]); in Micro2MacroMapping()
792 free(lemmas[microsize]); in Micro2MacroMapping()
[all …]
/dports/math/z3/z3-z3-4.8.13/src/test/
H A Dpb2bv.cpp44 expr_ref_vector lemmas(m); in test1() local
45 rw.flush_side_constraints(lemmas); in test1()
46 std::cout << lemmas << "\n"; in test1()
56 expr_ref_vector lemmas(m); in test_semantics() local
65 rw.flush_side_constraints(lemmas); in test_semantics()
66 std::cout << "lemmas: " << lemmas << "\n"; in test_semantics()
78 solver.assert_expr(lemmas); in test_semantics()
/dports/math/py-z3-solver/z3-z3-4.8.10/src/test/
H A Dpb2bv.cpp44 expr_ref_vector lemmas(m); in test1() local
45 rw.flush_side_constraints(lemmas); in test1()
46 std::cout << lemmas << "\n"; in test1()
56 expr_ref_vector lemmas(m); in test_semantics() local
65 rw.flush_side_constraints(lemmas); in test_semantics()
66 std::cout << "lemmas: " << lemmas << "\n"; in test_semantics()
78 solver.assert_expr(lemmas); in test_semantics()

12345678910>>...13