/dports/math/cvc4/CVC4-1.7/src/proof/ |
H A D | resolution_bitvector_proof.cpp | 101 for (int i = 0; i < confl.size(); ++i) in endBVConflict() 141 Expr confl = conflicts[i]; in finalizeConflicts() local 147 if ((confl.isConst() && confl.getConst<bool>()) in finalizeConflicts() 148 || (confl.getKind() == kind::NOT && confl[0].isConst() in finalizeConflicts() 149 && !confl[0].getConst<bool>())) in finalizeConflicts() 153 else if (confl.getKind() == kind::OR) in finalizeConflicts() 157 if ((confl[k].isConst() && confl[k].getConst<bool>()) in finalizeConflicts() 158 || (confl[k].getKind() == kind::NOT && confl[k][0].isConst() in finalizeConflicts() 174 ClauseId id = d_bbConflictMap[confl]; in finalizeConflicts() 192 if (confl[k] == possibleMatch) in finalizeConflicts() [all …]
|
/dports/sysutils/slurm-wlm/slurm-20.02.7/src/slurmd/slurmstepd/ |
H A D | slurmstepd.c | 266 confl = conf; in read_slurmd_conf_lite() 269 confl = local_conf; in read_slurmd_conf_lite() 288 confl->log_opts.prefix_level = 1; in read_slurmd_conf_lite() 289 confl->log_opts.stderr_level = confl->debug_level; in read_slurmd_conf_lite() 290 confl->log_opts.logfile_level = confl->debug_level; in read_slurmd_conf_lite() 291 confl->log_opts.syslog_level = confl->debug_level; in read_slurmd_conf_lite() 299 if (confl->daemonize) { in read_slurmd_conf_lite() 301 if (confl->logfile) in read_slurmd_conf_lite() 310 log_alter(confl->log_opts, 0, confl->logfile); in read_slurmd_conf_lite() 311 log_set_timefmt(confl->log_fmt); in read_slurmd_conf_lite() [all …]
|
/dports/math/py-cryptominisat/cryptominisat-5.8.0/python/tests/ |
H A D | test_pycryptosat.py | 245 confl = self.solver.get_conflict() 246 self.assertEqual(isinstance(confl, list), True) 247 self.assertNotIn(3, confl) 249 if 2 in confl: 250 self.assertIn(2, confl) 251 elif -4 in confl: 252 self.assertIn(-4, confl) 260 confl = self.solver.get_conflict() 261 self.assertEqual(isinstance(confl, list), True) 262 self.assertNotIn(2, confl) [all …]
|
/dports/math/cryptominisat/cryptominisat-5.8.0/python/tests/ |
H A D | test_pycryptosat.py | 245 confl = self.solver.get_conflict() 246 self.assertEqual(isinstance(confl, list), True) 247 self.assertNotIn(3, confl) 249 if 2 in confl: 250 self.assertIn(2, confl) 251 elif -4 in confl: 252 self.assertIn(-4, confl) 260 confl = self.solver.get_conflict() 261 self.assertEqual(isinstance(confl, list), True) 262 self.assertNotIn(2, confl) [all …]
|
/dports/math/cvc4/CVC4-1.7/src/prop/minisat/core/ |
H A D | Solver.cc | 729 Lit q = ca[confl][j]; in analyze() 761 confl = reason(var(p)); in analyze() 935 CRef confl = CRef_Undef; in propagate() local 943 confl = updateLemmas(); in propagate() 945 return confl; in propagate() 960 confl = updateLemmas(); in propagate() 961 return confl; in propagate() 964 return confl; in propagate() 1007 return confl; in propagate() 1114 confl = cr; in propagateBool() [all …]
|
/dports/math/cvc4/CVC4-1.7/src/theory/bv/ |
H A D | bv_quick_check.cpp | 48 Node confl = utils::mkAnd(conflict); in setConflict() local 50 d_conflict = confl; in setConflict() 316 Node QuickXPlain::minimizeConflict(TNode confl) { in minimizeConflict() argument 320 return confl; in minimizeConflict() 326 Assert (confl.getNumChildren() > 2); in minimizeConflict() 328 for (unsigned i = 0; i < confl.getNumChildren(); ++i) { in minimizeConflict() 329 conflict.push_back(confl[i]); in minimizeConflict() 335 double minimization_ratio = ((double) minimized.size())/confl.getNumChildren(); in minimizeConflict()
|
/dports/math/py-cryptominisat/cryptominisat-5.8.0/src/ |
H A D | propengine.cpp | 168 , PropBy& confl in prop_bin_cl() argument 189 confl = PropBy(~p, i->red()); in prop_bin_cl() 204 , PropBy& confl in prop_long_cl_any_order() argument 230 handle_normal_prop_fail(c, offset, confl); in prop_long_cl_any_order() 273 PropBy confl; in propagate_any_order_fast() local 309 confl = PropBy(~p, i->red()); in propagate_any_order_fast() 378 confl = PropBy(offset); in propagate_any_order_fast() 439 return confl; in propagate_any_order_fast() 445 PropBy confl; in propagate_any_order() local 451 while (qhead < trail.size() && confl.isNULL()) { in propagate_any_order() [all …]
|
H A D | hyperengine.cpp | 46 PropBy confl; in propagate_bfs() local 88 ret = prop_bin_with_ancestor_info(p, k, confl); in propagate_bfs() 90 return analyzeFail(confl); in propagate_bfs() 110 ret = prop_bin_with_ancestor_info(p, k, confl); in propagate_bfs() 112 return analyzeFail(confl); in propagate_bfs() 140 ret = prop_normal_cl_with_ancestor_info(i, j, p, confl); in propagate_bfs() 156 return analyzeFail(confl); in propagate_bfs() 567 , PropBy& confl in prop_bin_with_ancestor_info() argument 589 confl = PropBy(~p, k->red()); in prop_bin_with_ancestor_info() 634 , PropBy& confl in prop_normal_cl_with_ancestor_info() argument [all …]
|
H A D | searcher.cpp | 301 (void) confl; in debug_print_resolving_clause() 303 switch(confl.getType()) { in debug_print_resolving_clause() 362 const PropBy confl in add_literals_from_confl_to_learnt() argument 373 switch (confl.getType()) { in add_literals_from_confl_to_learnt() 658 PropBy confl, in simple_create_learnt_clause() argument 723 confl = PropBy(); in simple_create_learnt_clause() 737 (void) confl; in print_debug_resolution_data() 769 const PropBy confl in analyze_conflict() argument 1257 PropBy confl; in search() local 1326 if (!confl.isNULL()) { in search() [all …]
|
/dports/math/cryptominisat/cryptominisat-5.8.0/src/ |
H A D | propengine.cpp | 168 , PropBy& confl in prop_bin_cl() argument 189 confl = PropBy(~p, i->red()); in prop_bin_cl() 204 , PropBy& confl in prop_long_cl_any_order() argument 230 handle_normal_prop_fail(c, offset, confl); in prop_long_cl_any_order() 273 PropBy confl; in propagate_any_order_fast() local 309 confl = PropBy(~p, i->red()); in propagate_any_order_fast() 378 confl = PropBy(offset); in propagate_any_order_fast() 439 return confl; in propagate_any_order_fast() 445 PropBy confl; in propagate_any_order() local 451 while (qhead < trail.size() && confl.isNULL()) { in propagate_any_order() [all …]
|
H A D | hyperengine.cpp | 46 PropBy confl; in propagate_bfs() local 88 ret = prop_bin_with_ancestor_info(p, k, confl); in propagate_bfs() 90 return analyzeFail(confl); in propagate_bfs() 110 ret = prop_bin_with_ancestor_info(p, k, confl); in propagate_bfs() 112 return analyzeFail(confl); in propagate_bfs() 140 ret = prop_normal_cl_with_ancestor_info(i, j, p, confl); in propagate_bfs() 156 return analyzeFail(confl); in propagate_bfs() 567 , PropBy& confl in prop_bin_with_ancestor_info() argument 589 confl = PropBy(~p, k->red()); in prop_bin_with_ancestor_info() 634 , PropBy& confl in prop_normal_cl_with_ancestor_info() argument [all …]
|
H A D | searcher.cpp | 301 (void) confl; in debug_print_resolving_clause() 303 switch(confl.getType()) { in debug_print_resolving_clause() 362 const PropBy confl in add_literals_from_confl_to_learnt() argument 373 switch (confl.getType()) { in add_literals_from_confl_to_learnt() 658 PropBy confl, in simple_create_learnt_clause() argument 723 confl = PropBy(); in simple_create_learnt_clause() 737 (void) confl; in print_debug_resolution_data() 769 const PropBy confl in analyze_conflict() argument 1257 PropBy confl; in search() local 1326 if (!confl.isNULL()) { in search() [all …]
|
/dports/math/chuffed/chuffed-e04bedd/chuffed/core/ |
H A D | conflict.cpp | 130 confl = NULL; in analyze() 196 Clause* expl = confl; in getLearntClause() 350 for (int i = 0; i < confl->size(); i++) { in findConflictLevel() 351 int l = trailpos[var((*confl)[i])]; in findConflictLevel() 366 if (clevel < decisionLevel() && confl->temp_expl) { in findConflictLevel() 367 confl = Clause_new(*confl); in findConflictLevel() 368 confl->temp_expl = 1; in findConflictLevel() 369 rtrail[clevel].push(confl); in findConflictLevel() 517 assert(confl != NULL); in checkConflict() 518 for (int i = 0; i < confl->size(); i++) { in checkConflict() [all …]
|
/dports/java/openjdk8/jdk8u-jdk8u312-b07.1/hotspot/test/compiler/types/correctness/execution/ |
H A D | TypeProfile.java | 45 T confl = scenario.getConflict(); in execute() local 52 result = methodNotToCompile(scenario, confl); in execute() 53 scenario.check(result, confl); in execute()
|
/dports/java/openjdk8-jre/jdk8u-jdk8u312-b07.1/hotspot/test/compiler/types/correctness/execution/ |
H A D | TypeProfile.java | 45 T confl = scenario.getConflict(); in execute() local 52 result = methodNotToCompile(scenario, confl); in execute() 53 scenario.check(result, confl); in execute()
|
/dports/java/openjdk11/jdk11u-jdk-11.0.13-8-1/test/hotspot/jtreg/compiler/types/correctness/execution/ |
H A D | TypeProfile.java | 45 T confl = scenario.getConflict(); in execute() local 52 result = methodNotToCompile(scenario, confl); in execute() 53 scenario.check(result, confl); in execute()
|
/dports/java/openjdk13/jdk13u-jdk-13.0.10-1-1/test/hotspot/jtreg/compiler/types/correctness/execution/ |
H A D | TypeProfile.java | 45 T confl = scenario.getConflict(); in execute() local 52 result = methodNotToCompile(scenario, confl); in execute() 53 scenario.check(result, confl); in execute()
|
/dports/java/openjdk15/jdk15u-jdk-15.0.6-1-1/test/hotspot/jtreg/compiler/types/correctness/execution/ |
H A D | TypeProfile.java | 45 T confl = scenario.getConflict(); in execute() local 52 result = methodNotToCompile(scenario, confl); in execute() 53 scenario.check(result, confl); in execute()
|
/dports/java/openjdk16/jdk16u-jdk-16.0.2-7-1/test/hotspot/jtreg/compiler/types/correctness/execution/ |
H A D | TypeProfile.java | 45 T confl = scenario.getConflict(); in execute() local 52 result = methodNotToCompile(scenario, confl); in execute() 53 scenario.check(result, confl); in execute()
|
/dports/java/openjdk11-jre/jdk11u-jdk-11.0.13-8-1/test/hotspot/jtreg/compiler/types/correctness/execution/ |
H A D | TypeProfile.java | 45 T confl = scenario.getConflict(); in execute() local 52 result = methodNotToCompile(scenario, confl); in execute() 53 scenario.check(result, confl); in execute()
|
/dports/java/openjdk12/openjdk-jdk12u-jdk-12.0.2-10-4/test/hotspot/jtreg/compiler/types/correctness/execution/ |
H A D | TypeProfile.java | 45 T confl = scenario.getConflict(); in execute() local 52 result = methodNotToCompile(scenario, confl); in execute() 53 scenario.check(result, confl); in execute()
|
/dports/java/openjdk14/jdk14u-jdk-14.0.2-12-1/test/hotspot/jtreg/compiler/types/correctness/execution/ |
H A D | TypeProfile.java | 45 T confl = scenario.getConflict(); in execute() local 52 result = methodNotToCompile(scenario, confl); in execute() 53 scenario.check(result, confl); in execute()
|
/dports/java/openjdk17/jdk17u-jdk-17.0.1-12-1/test/hotspot/jtreg/compiler/types/correctness/execution/ |
H A D | TypeProfile.java | 45 T confl = scenario.getConflict(); in execute() local 52 result = methodNotToCompile(scenario, confl); in execute() 53 scenario.check(result, confl); in execute()
|
/dports/math/py-cryptominisat/cryptominisat-5.8.0/web/ |
H A D | get_data.php | 86 $confl = (int)$row["conflicts"]; 87 if ($confl -$last_confl_for_everyn < $this->everyn && $i < $this->nrows-1) { 91 $last_confl_for_everyn = $confl; 93 array_push($json_subarray, $confl); 382 $confl = (int)$arr["confl"]; 383 array_push($json_tmp, $confl);
|
/dports/math/cryptominisat/cryptominisat-5.8.0/web/ |
H A D | get_data.php | 86 $confl = (int)$row["conflicts"]; 87 if ($confl -$last_confl_for_everyn < $this->everyn && $i < $this->nrows-1) { 91 $last_confl_for_everyn = $confl; 93 array_push($json_subarray, $confl); 382 $confl = (int)$arr["confl"]; 383 array_push($json_tmp, $confl);
|