Searched refs:conflict_clause (Results 1 – 9 of 9) sorted by relevance
| /dports/finance/odoo/odoo-19d77c2a03335eb95a686bd69a1b56b38e87d609/odoo/addons/website/models/ |
| H A D | ir_translation.py | 17 conflict_clause = """
25 conflict_clause = " ON CONFLICT DO NOTHING"
38 AND specific.website_id IS NOT NULL""" + conflict_clause.format(
59 AND s_menu.website_id IS NOT NULL""" + conflict_clause.format(
|
| /dports/math/yices/yices-2.6.2/src/mcsat/bool/ |
| H A D | bool_plugin.c | 700 mcsat_clause_t* conflict_clause; in bool_plugin_get_conflict() local
705 conflict_clause = clause_db_get_clause(&bp->clause_db, bp->conflict); in bool_plugin_get_conflict()
710 for (i = 0; i < conflict_clause->size; ++ i) { in bool_plugin_get_conflict()
711 l_i = conflict_clause->literals[i]; in bool_plugin_get_conflict()
|
| /dports/math/z3/z3-z3-4.8.13/src/nlsat/ |
| H A D | nlsat_solver.cpp | 1519 clause * conflict_clause; in search() local
1521 conflict_clause = process_clauses(m_bwatches[m_bk]); in search()
1523 conflict_clause = process_clauses(m_watches[m_xk]); in search()
1524 if (conflict_clause == nullptr) in search()
1526 if (!resolve(*conflict_clause)) in search()
1974 clause const * conflict_clause = &conflict; in resolve() local
1981 … TRACE("nlsat", tout << "resolve, conflicting clause:\n"; display(tout, *conflict_clause) << "\n"; in resolve()
1990 resolve_clause(null_bool_var, *conflict_clause); in resolve()
2117 if (lemma_is_clause(*conflict_clause)) { in resolve()
2119 VERIFY(process_clause(*conflict_clause, true)); in resolve()
[all …]
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/nlsat/ |
| H A D | nlsat_solver.cpp | 1519 clause * conflict_clause; in search() local
1521 conflict_clause = process_clauses(m_bwatches[m_bk]); in search()
1523 conflict_clause = process_clauses(m_watches[m_xk]); in search()
1524 if (conflict_clause == nullptr) in search()
1526 if (!resolve(*conflict_clause)) in search()
1974 clause const * conflict_clause = &conflict; in resolve() local
1981 … TRACE("nlsat", tout << "resolve, conflicting clause:\n"; display(tout, *conflict_clause) << "\n"; in resolve()
1990 resolve_clause(null_bool_var, *conflict_clause); in resolve()
2117 if (lemma_is_clause(*conflict_clause)) { in resolve()
2119 VERIFY(process_clause(*conflict_clause, true)); in resolve()
[all …]
|
| /dports/math/cvc4/CVC4-1.7/src/prop/bvminisat/core/ |
| H A D | Solver.cc | 1312 vec<Lit> conflict_clause; in explain() local
1313 conflict_clause.push(p); in explain()
1315 conflict_clause.push(~explanation[i]); in explain()
1317 d_bvp->endBVConflict(conflict_clause); in explain()
|
| /dports/math/z3/z3-z3-4.8.13/src/smt/ |
| H A D | theory_pb.h | 380 bool resolve_conflict(card& c, literal_vector const& conflict_clause);
|
| H A D | theory_str_regex.cpp | 691 expr_ref conflict_clause(m.mk_not(mk_and(conflict_terms)), m); in solve_regex_automata() local
692 assert_axiom(conflict_clause); in solve_regex_automata()
693 add_persisted_axiom(conflict_clause); in solve_regex_automata()
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/smt/ |
| H A D | theory_pb.h | 380 bool resolve_conflict(card& c, literal_vector const& conflict_clause);
|
| H A D | theory_str_regex.cpp | 714 expr_ref conflict_clause(m.mk_not(mk_and(conflict_terms)), m); in solve_regex_automata() local
715 assert_axiom(conflict_clause); in solve_regex_automata()
716 add_persisted_axiom(conflict_clause); in solve_regex_automata()
|