/dports/math/py-cryptominisat/cryptominisat-5.8.0/src/ |
H A D | satzilla_features_calc.cpp | 112 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 D | satzilla_features_to_reconf.cpp | 134 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 D | satzilla_features.h | 42 double numClauses = 0; member
|
H A D | satzilla_features.cpp | 36 cout << "numClauses " << numClauses << ", "; in print_stats()
|
/dports/math/cryptominisat/cryptominisat-5.8.0/src/ |
H A D | satzilla_features_calc.cpp | 112 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 D | satzilla_features_to_reconf.cpp | 134 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 D | satzilla_features.h | 42 double numClauses = 0; member
|
H A D | satzilla_features.cpp | 36 cout << "numClauses " << numClauses << ", "; in print_stats()
|
/dports/textproc/zorba/zorba-2.7.0/src/compiler/expression/ |
H A D | flwor_expr.cpp | 924 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 D | flwor_rules.cpp | 196 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 D | index_join_rule.cpp | 521 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 D | hoist_rules.cpp | 380 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 D | QueryTermExtractor.cpp | 110 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 D | ScorerPerfTest.cpp | 156 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 D | Minisat.cpp | 195 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 D | cnf.h | 130 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 D | CnfParser.java | 49 public int numClauses = 0; field in CnfParser 157 numClauses = parseInt(); in readProblemDef()
|
/dports/math/cvc3/cvc3-2.4.1/src/sat/ |
H A D | cnf.cpp | 67 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 D | dpllt_basic.cpp | 441 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 D | aig_bitblaster.cpp | 402 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 D | plan_visitor.cpp | 881 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 D | expr_tools.cpp | 302 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 D | search_sat.cpp | 269 …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 D | cmsat_tablestructure.sql | 241 `numClauses` int(20) NOT NULL,
|
/dports/math/cryptominisat/cryptominisat-5.8.0/ |
H A D | cmsat_tablestructure.sql | 241 `numClauses` int(20) NOT NULL,
|