| /dports/math/z3/z3-z3-4.8.13/src/nlsat/ |
| H A D | nlsat_justification.h | 69 justification(bool):m_data(TAG(void *, nullptr, DECISION)) { SASSERT(is_decision()); } in justification()
74 bool is_decision() const { return get_kind() == DECISION; } in is_decision() function
|
| H A D | nlsat_solver.cpp | 1144 if (j.is_decision()) in assign()
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/nlsat/ |
| H A D | nlsat_justification.h | 69 justification(bool):m_data(TAG(void *, nullptr, DECISION)) { SASSERT(is_decision()); } in justification()
74 bool is_decision() const { return get_kind() == DECISION; } in is_decision() function
|
| H A D | nlsat_solver.cpp | 1144 if (j.is_decision()) in assign()
|
| /dports/math/py-cryptominisat/cryptominisat-5.8.0/src/ |
| H A D | sqlstats.h | 141 , const bool is_decision
|
| H A D | clause.h | 118 is_decision = false; in ClauseStats()
126 uint32_t is_decision:1; member
|
| H A D | sqlitestats.h | 106 , const bool is_decision
|
| H A D | searcher.h | 308 , const bool is_decision
422 const bool is_decision);
|
| H A D | searcher.cpp | 1576 const bool is_decision) in dump_var_for_learnt_cl() argument
1581 assert(is_decision || varData[v].reason == PropBy()); in dump_var_for_learnt_cl()
1599 , const bool is_decision in dump_sql_clause_data() argument
1603 if (is_decision) { in dump_sql_clause_data()
1605 dump_var_for_learnt_cl(l.var(), clid, is_decision); in dump_sql_clause_data()
1609 dump_var_for_learnt_cl(v, clid, is_decision); in dump_sql_clause_data()
1628 , is_decision in dump_sql_clause_data()
1670 , const bool is_decision in handle_last_confl() argument
1765 , is_decision in handle_last_confl()
1779 cl->stats.is_decision = is_decision; in handle_last_confl()
|
| H A D | sqlitestats.cpp | 739 , const bool is_decision in dump_clause_stats() argument
763 sqlite3_bind_int (stmt_clause_stats, bindAt++, is_decision); in dump_clause_stats()
|
| /dports/math/cryptominisat/cryptominisat-5.8.0/src/ |
| H A D | sqlstats.h | 141 , const bool is_decision
|
| H A D | clause.h | 118 is_decision = false; in ClauseStats()
126 uint32_t is_decision:1; member
|
| H A D | sqlitestats.h | 106 , const bool is_decision
|
| H A D | searcher.h | 308 , const bool is_decision
422 const bool is_decision);
|
| H A D | searcher.cpp | 1576 const bool is_decision) in dump_var_for_learnt_cl() argument
1581 assert(is_decision || varData[v].reason == PropBy()); in dump_var_for_learnt_cl()
1599 , const bool is_decision in dump_sql_clause_data() argument
1603 if (is_decision) { in dump_sql_clause_data()
1605 dump_var_for_learnt_cl(l.var(), clid, is_decision); in dump_sql_clause_data()
1609 dump_var_for_learnt_cl(v, clid, is_decision); in dump_sql_clause_data()
1628 , is_decision in dump_sql_clause_data()
1670 , const bool is_decision in handle_last_confl() argument
1765 , is_decision in handle_last_confl()
1779 cl->stats.is_decision = is_decision; in handle_last_confl()
|
| H A D | sqlitestats.cpp | 739 , const bool is_decision in dump_clause_stats() argument
763 sqlite3_bind_int (stmt_clause_stats, bindAt++, is_decision); in dump_clause_stats()
|
| /dports/math/py-cryptominisat/cryptominisat-5.8.0/ |
| H A D | cmsat_tablestructure.sql | 188 `is_decision` int(20) NOT NULL,
|
| /dports/math/cryptominisat/cryptominisat-5.8.0/ |
| H A D | cmsat_tablestructure.sql | 188 `is_decision` int(20) NOT NULL,
|
| /dports/math/yices/yices-2.6.2/src/mcsat/ |
| H A D | solver.c | 393 bool is_decision; in trail_token_add() local
395 is_decision = tk->x != variable_null; in trail_token_add()
398 if (is_decision) { in trail_token_add()
415 if (is_decision) { in trail_token_add()
421 if (ctx_trace_enabled(&tk->ctx->ctx, "mcsat::propagation::check") && !is_decision) { in trail_token_add()
|
| /dports/math/z3/z3-z3-4.8.13/src/sat/ |
| H A D | sat_lookahead.cpp | 2081 bool lookahead::backtrack(literal_vector& trail, bool_vector & is_decision) { in backtrack() argument
2085 if (is_decision.back()) { in backtrack()
2089 is_decision.back() = false; in backtrack()
2094 is_decision.pop_back(); in backtrack()
|
| H A D | sat_lookahead.h | 546 bool backtrack(literal_vector& trail, bool_vector & is_decision);
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/sat/ |
| H A D | sat_lookahead.cpp | 2081 bool lookahead::backtrack(literal_vector& trail, bool_vector & is_decision) { in backtrack() argument
2085 if (is_decision.back()) { in backtrack()
2089 is_decision.back() = false; in backtrack()
2094 is_decision.pop_back(); in backtrack()
|
| H A D | sat_lookahead.h | 542 bool backtrack(literal_vector& trail, bool_vector & is_decision);
|