mirror of
https://github.com/Z3Prover/z3
synced 2025-04-07 18:05:21 +00:00
fix name to divisible, guard under smtlib2_compliant as sugguested in #1757
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
94ffa3963e
commit
85e7b18451
|
@ -21,6 +21,7 @@ Revision History:
|
|||
#include "math/polynomial/algebraic_numbers.h"
|
||||
#include "util/id_gen.h"
|
||||
#include "ast/ast_smt2_pp.h"
|
||||
#include "util/gparams.h"
|
||||
|
||||
struct arith_decl_plugin::algebraic_numbers_wrapper {
|
||||
unsynch_mpq_manager m_qmanager;
|
||||
|
@ -487,7 +488,7 @@ func_decl * arith_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters
|
|||
if (arity != 1 || domain[0] != m_int_decl || num_parameters != 1 || !parameters[0].is_int()) {
|
||||
m_manager->raise_exception("invalid divides application. Expects integer parameter and one argument of sort integer");
|
||||
}
|
||||
return m_manager->mk_func_decl(symbol("divides"), 1, &m_int_decl, m_manager->mk_bool_sort(),
|
||||
return m_manager->mk_func_decl(symbol("divisible"), 1, &m_int_decl, m_manager->mk_bool_sort(),
|
||||
func_decl_info(m_family_id, k, num_parameters, parameters));
|
||||
}
|
||||
|
||||
|
@ -512,7 +513,7 @@ func_decl * arith_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters
|
|||
if (num_args != 1 || m_manager->get_sort(args[0]) != m_int_decl || num_parameters != 1 || !parameters[0].is_int()) {
|
||||
m_manager->raise_exception("invalid divides application. Expects integer parameter and one argument of sort integer");
|
||||
}
|
||||
return m_manager->mk_func_decl(symbol("divides"), 1, &m_int_decl, m_manager->mk_bool_sort(),
|
||||
return m_manager->mk_func_decl(symbol("divisible"), 1, &m_int_decl, m_manager->mk_bool_sort(),
|
||||
func_decl_info(m_family_id, k, num_parameters, parameters));
|
||||
}
|
||||
if (m_manager->int_real_coercions() && use_coercion(k)) {
|
||||
|
@ -549,8 +550,9 @@ void arith_decl_plugin::get_op_names(svector<builtin_name>& op_names, symbol con
|
|||
op_names.push_back(builtin_name("*",OP_MUL));
|
||||
op_names.push_back(builtin_name("/",OP_DIV));
|
||||
op_names.push_back(builtin_name("div",OP_IDIV));
|
||||
// clashes with user-defined functions
|
||||
// op_names.push_back(builtin_name("divides",OP_IDIVIDES));
|
||||
if (gparams::get_value("smtlib2_compliant") == "true") {
|
||||
op_names.push_back(builtin_name("divisible",OP_IDIVIDES));
|
||||
}
|
||||
op_names.push_back(builtin_name("rem",OP_REM));
|
||||
op_names.push_back(builtin_name("mod",OP_MOD));
|
||||
op_names.push_back(builtin_name("to_real",OP_TO_REAL));
|
||||
|
|
|
@ -351,7 +351,7 @@ namespace opt {
|
|||
void context::get_model_core(model_ref& mdl) {
|
||||
mdl = m_model;
|
||||
fix_model(mdl);
|
||||
mdl->set_model_completion(true);
|
||||
if (mdl) mdl->set_model_completion(true);
|
||||
TRACE("opt", tout << *mdl;);
|
||||
}
|
||||
|
||||
|
|
|
@ -1551,10 +1551,10 @@ namespace sat {
|
|||
if (k == 1 && lit == null_literal) {
|
||||
literal_vector _lits(lits);
|
||||
s().mk_clause(_lits.size(), _lits.c_ptr(), learned);
|
||||
return 0;
|
||||
return nullptr;
|
||||
}
|
||||
if (!learned && clausify(lit, lits.size(), lits.c_ptr(), k)) {
|
||||
return 0;
|
||||
return nullptr;
|
||||
}
|
||||
void * mem = m_allocator.allocate(card::get_obj_size(lits.size()));
|
||||
card* c = new (mem) card(next_id(), lit, lits, k);
|
||||
|
@ -1615,7 +1615,7 @@ namespace sat {
|
|||
bool units = true;
|
||||
for (wliteral wl : wlits) units &= wl.first == 1;
|
||||
if (k == 0 && lit == null_literal) {
|
||||
return 0;
|
||||
return nullptr;
|
||||
}
|
||||
if (units || k == 1) {
|
||||
literal_vector lits;
|
||||
|
@ -3405,7 +3405,7 @@ namespace sat {
|
|||
return;
|
||||
}
|
||||
for (wliteral l : p1) {
|
||||
SASSERT(m_weights[l.second.index()] == 0);
|
||||
SASSERT(m_weights.size() <= l.second.index() || m_weights[l.second.index()] == 0);
|
||||
m_weights.setx(l.second.index(), l.first, 0);
|
||||
mark_visited(l.second);
|
||||
}
|
||||
|
@ -3837,8 +3837,8 @@ namespace sat {
|
|||
reset_active_var_set();
|
||||
m_wlits.reset();
|
||||
uint64_t sum = 0;
|
||||
if (m_bound == 1) return 0;
|
||||
if (m_overflow) return 0;
|
||||
if (m_bound == 1) return nullptr;
|
||||
if (m_overflow) return nullptr;
|
||||
|
||||
for (bool_var v : m_active_vars) {
|
||||
int coeff = get_int_coeff(v);
|
||||
|
@ -3850,7 +3850,7 @@ namespace sat {
|
|||
}
|
||||
|
||||
if (m_overflow || sum >= UINT_MAX/2) {
|
||||
return 0;
|
||||
return nullptr;
|
||||
}
|
||||
else {
|
||||
return add_pb_ge(null_literal, m_wlits, m_bound, true);
|
||||
|
@ -3905,7 +3905,7 @@ namespace sat {
|
|||
++k;
|
||||
}
|
||||
if (k == 1) {
|
||||
return 0;
|
||||
return nullptr;
|
||||
}
|
||||
while (!m_wlits.empty()) {
|
||||
wliteral wl = m_wlits.back();
|
||||
|
@ -3928,7 +3928,7 @@ namespace sat {
|
|||
++num_max_level;
|
||||
}
|
||||
}
|
||||
if (m_overflow) return 0;
|
||||
if (m_overflow) return nullptr;
|
||||
|
||||
if (slack >= k) {
|
||||
#if 0
|
||||
|
@ -3937,7 +3937,7 @@ namespace sat {
|
|||
std::cout << "not asserting\n";
|
||||
display(std::cout, m_A, true);
|
||||
#endif
|
||||
return 0;
|
||||
return nullptr;
|
||||
}
|
||||
|
||||
// produce asserting cardinality constraint
|
||||
|
|
Loading…
Reference in a new issue