Home
last modified time | relevance | path

Searched refs:numClauses (Results 1 – 25 of 42) sorted by relevance

12

/dports/math/py-cryptominisat/cryptominisat-5.8.0/src/
H A Dsatzilla_features_calc.cpp112 satzilla_feat.numClauses = solver->longIrredCls.size() + solver->binTri.irredBins; in fill_vars_cls()
155 satzilla_feat.vcg_cls_mean /= (double)satzilla_feat.numClauses; in calculate_clause_stats()
156 satzilla_feat.pnr_cls_mean /= (double)satzilla_feat.numClauses; in calculate_clause_stats()
157 satzilla_feat.horn /= (double)satzilla_feat.numClauses; in calculate_clause_stats()
158 satzilla_feat.binary = float_div(solver->binTri.irredBins, satzilla_feat.numClauses); in calculate_clause_stats()
174 double _size = myVars[vv].size / (double)satzilla_feat.numClauses; in calculate_variable_stats()
185 double _horn = myVars[vv].horn / (double)satzilla_feat.numClauses; in calculate_variable_stats()
244 double _size = myVars[vv].size / (double)satzilla_feat.numClauses; in calculate_extra_var_stats()
250 double _horn = myVars[vv].horn / (double)satzilla_feat.numClauses; in calculate_extra_var_stats()
368 if (satzilla_feat.numVars > 0 && satzilla_feat.numClauses > 0) { in extract()
[all …]
H A Dsatzilla_features_to_reconf.cpp134 if ((satzilla_feat.numClauses > 24521.00000) && in get_score0()
171 if ((satzilla_feat.numClauses > 3631149.00000) && in get_score0()
239 if ((satzilla_feat.numClauses > 252434.00000) && in get_score4()
376 if ((satzilla_feat.numClauses > 17097.00000) && in get_score6()
550 if ((satzilla_feat.numClauses > 54199.00000) && in get_score12()
628 if ((satzilla_feat.numClauses < 7548140.00000) && in get_score16()
641 if ((satzilla_feat.numClauses < 108335.00000) && in get_score16()
698 if ((satzilla_feat.numClauses > 84464.00000) && in get_score17()
H A Dsatzilla_features.h42 double numClauses = 0; member
H A Dsatzilla_features.cpp36 cout << "numClauses " << numClauses << ", "; in print_stats()
/dports/math/cryptominisat/cryptominisat-5.8.0/src/
H A Dsatzilla_features_calc.cpp112 satzilla_feat.numClauses = solver->longIrredCls.size() + solver->binTri.irredBins; in fill_vars_cls()
155 satzilla_feat.vcg_cls_mean /= (double)satzilla_feat.numClauses; in calculate_clause_stats()
156 satzilla_feat.pnr_cls_mean /= (double)satzilla_feat.numClauses; in calculate_clause_stats()
157 satzilla_feat.horn /= (double)satzilla_feat.numClauses; in calculate_clause_stats()
158 satzilla_feat.binary = float_div(solver->binTri.irredBins, satzilla_feat.numClauses); in calculate_clause_stats()
174 double _size = myVars[vv].size / (double)satzilla_feat.numClauses; in calculate_variable_stats()
185 double _horn = myVars[vv].horn / (double)satzilla_feat.numClauses; in calculate_variable_stats()
244 double _size = myVars[vv].size / (double)satzilla_feat.numClauses; in calculate_extra_var_stats()
250 double _horn = myVars[vv].horn / (double)satzilla_feat.numClauses; in calculate_extra_var_stats()
368 if (satzilla_feat.numVars > 0 && satzilla_feat.numClauses > 0) { in extract()
[all …]
H A Dsatzilla_features_to_reconf.cpp134 if ((satzilla_feat.numClauses > 24521.00000) && in get_score0()
171 if ((satzilla_feat.numClauses > 3631149.00000) && in get_score0()
239 if ((satzilla_feat.numClauses > 252434.00000) && in get_score4()
376 if ((satzilla_feat.numClauses > 17097.00000) && in get_score6()
550 if ((satzilla_feat.numClauses > 54199.00000) && in get_score12()
628 if ((satzilla_feat.numClauses < 7548140.00000) && in get_score16()
641 if ((satzilla_feat.numClauses < 108335.00000) && in get_score16()
698 if ((satzilla_feat.numClauses > 84464.00000) && in get_score17()
H A Dsatzilla_features.h42 double numClauses = 0; member
H A Dsatzilla_features.cpp36 cout << "numClauses " << numClauses << ", "; in print_stats()
/dports/textproc/zorba/zorba-2.7.0/src/compiler/expression/
H A Dflwor_expr.cpp924 csize numClauses = num_clauses(); in set_where() local
927 for (i = 0; i < numClauses; ++i) in set_where()
936 if (i == numClauses) in set_where()
960 csize numClauses = num_clauses(); in remove_where_clause() local
978 csize numClauses = num_clauses(); in get_where() local
994 csize numClauses = num_clauses(); in get_group_clause() local
1010 csize numClauses = num_clauses(); in get_order_clause() local
1027 csize numClauses = num_clauses(); in num_forlet_clauses() local
1053 csize numClauses = theClauses.size(); in defines_variable() local
1122 ulong numClauses = num_clauses(); in compute_scripting_kind() local
[all …]
/dports/textproc/zorba/zorba-2.7.0/src/compiler/rewriter/rules/
H A Dflwor_rules.cpp196 csize numClauses = flwor.num_clauses(); in RULE_REWRITE_PRE() local
201 if (numClauses == 0) in RULE_REWRITE_PRE()
209 if (numClauses == 1 && in RULE_REWRITE_PRE()
232 for (csize i = 0; i < numClauses; ++i) in RULE_REWRITE_PRE()
277 for (csize i = 0; i < numClauses; ++i) in RULE_REWRITE_PRE()
397 --numClauses; in RULE_REWRITE_PRE()
443 --numClauses; in RULE_REWRITE_PRE()
755 csize numClauses = flwor.num_clauses(); in safe_to_fold_single_use() local
1453 --numClauses; in RULE_REWRITE_PRE()
1936 i == numClauses-1 && in RULE_REWRITE_PRE()
[all …]
H A Dindex_join_rule.cpp521 csize numClauses = innerFlwor->num_clauses(); in rewriteJoin() local
524 mostInnerVarPos < numClauses-1) in rewriteJoin()
526 ZORBA_ASSERT(mostInnerVarPos < numClauses-1); in rewriteJoin()
532 for (csize i = mostInnerVarPos+1; i < numClauses; ++i) in rewriteJoin()
537 for (csize i = numClauses - 1; i > mostInnerVarPos; --i) in rewriteJoin()
H A Dhoist_rules.cpp380 csize numClauses = trycatch->clause_count(); in try_hoisting() local
382 for (csize i = 0; i < numClauses; ++i) in try_hoisting()
/dports/textproc/clucene/clucene-core-2.3.3.4/src/contribs-lib/CLucene/highlighter/
H A DQueryTermExtractor.cpp110 uint32_t numClauses = query->getClauseCount(); in getTermsFromBooleanQuery() local
111 BooleanClause** queryClauses = _CL_NEWARRAY(BooleanClause*,numClauses); in getTermsFromBooleanQuery()
114 for (uint32_t i = 0; i < numClauses; i++) in getTermsFromBooleanQuery()
/dports/textproc/luceneplusplus/LucenePlusPlus-rel_3.0.8/src/test/search/
H A DScorerPerfTest.cpp156 int32_t numClauses = r->nextInt(maxClauses - 1) + 2; // min 2 clauses in doConjunctions() local
159 for (int32_t j = 0; j < numClauses; ++j) { in doConjunctions()
177 int32_t numClauses = r->nextInt(maxClauses - 1) + 2; // min 2 clauses in doNestedConjunctions() local
179 for (int32_t j = 0; j < numClauses; ++j) { in doNestedConjunctions()
/dports/math/ogdf/OGDF/src/ogdf/external/
H A DMinisat.cpp195 int numClauses = -1; in readDimacs() local
196 in >> numVars >> numClauses; in readDimacs()
197 if (numVars < 0 || numClauses < 0) { in readDimacs()
222 if(clauseCount != numClauses) { in readDimacs()
/dports/math/cvc3/cvc3-2.4.1/src/include/
H A Dcnf.h130 virtual unsigned numClauses() const = 0;
161 unsigned numClauses() const { return d_formula.size(); } in numClauses() function
186 unsigned numClauses() const { return d_formula.size(); } in numClauses() function
/dports/math/jacop/jacop-4.8.0/src/main/java/org/jacop/jasat/utils/
H A DCnfParser.java49 public int numClauses = 0; field in CnfParser
157 numClauses = parseInt(); in readProblemDef()
/dports/math/cvc3/cvc3-2.4.1/src/sat/
H A Dcnf.cpp67 for (i = 0, iend = cnf.numClauses(); i != iend; ++i) { in copy()
100 for (i = 0, iend = cnf.numClauses(); i != iend; ++i) { in operator +=()
H A Ddpllt_basic.cpp441 if (d_assertions->numClauses() > 0) { in checkSat()
480 if (d_assertions->numClauses() > 0) { in continueCheck()
/dports/math/cvc4/CVC4-1.7/src/theory/bv/bitblast/
H A Daig_bitblaster.cpp402 unsigned numClauses = pCnf->nClauses; in assertToSatSolver() local
405 d_statistics.d_numClauses += numClauses; in assertToSatSolver()
415 for (unsigned i = 0; i < numClauses; i++ ) { in assertToSatSolver()
/dports/textproc/zorba/zorba-2.7.0/src/compiler/codegen/
H A Dplan_visitor.cpp881 csize numClauses = v.num_clauses(); in begin_visit() local
891 for (csize i = 0; i < numClauses; ++i) in begin_visit()
939 ++numClauses; in begin_visit()
951 while (i < numClauses) in begin_visit()
993 ++numClauses; in begin_visit()
996 if (i == numClauses -1 || in begin_visit()
997 (i < numClauses - 1 && in begin_visit()
1008 ++numClauses; in begin_visit()
1043 ++numClauses; in begin_visit()
1048 for (csize i = 0; i < numClauses; ++i) in begin_visit()
[all …]
/dports/textproc/zorba/zorba-2.7.0/src/compiler/rewriter/tools/
H A Dexpr_tools.cpp302 csize numClauses = trycatch->clause_count(); in index_flwor_vars() local
304 for (csize i = 0; i < numClauses; ++i) in index_flwor_vars()
494 csize numClauses = trycatch->clause_count(); in build_expr_to_vars_map() local
496 for (csize i = 0; i < numClauses; ++i) in build_expr_to_vars_map()
/dports/math/cvc3/cvc3-2.4.1/src/search/
H A Dsearch_sat.cpp269 …Core() && d_pendingLemmasNext == d_pendingLemmas.size() && d_lemmasNext == d_lemmas.numClauses()) { in checkConsistent()
336 DebugAssert(d_lemmasNext <= d_lemmas.numClauses(), ""); in getNewClauses()
337 if (d_lemmasNext == d_lemmas.numClauses()) return false; in getNewClauses()
341 } while (d_lemmasNext < d_lemmas.numClauses()); in getNewClauses()
728 DebugAssert(d_lemmasNext == d_lemmas.numClauses(), in check()
/dports/math/py-cryptominisat/cryptominisat-5.8.0/
H A Dcmsat_tablestructure.sql241 `numClauses` int(20) NOT NULL,
/dports/math/cryptominisat/cryptominisat-5.8.0/
H A Dcmsat_tablestructure.sql241 `numClauses` int(20) NOT NULL,

12