From 85e7b1845164f56f8c044e911ccc18d79d1c58d5 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 1 Sep 2018 18:22:10 -0700 Subject: [PATCH] fix name to divisible, guard under smtlib2_compliant as sugguested in #1757 Signed-off-by: Nikolaj Bjorner --- src/ast/arith_decl_plugin.cpp | 10 ++++++---- src/opt/opt_context.cpp | 2 +- src/sat/ba_solver.cpp | 20 ++++++++++---------- 3 files changed, 17 insertions(+), 15 deletions(-) diff --git a/src/ast/arith_decl_plugin.cpp b/src/ast/arith_decl_plugin.cpp index db3604a99..cdf18875c 100644 --- a/src/ast/arith_decl_plugin.cpp +++ b/src/ast/arith_decl_plugin.cpp @@ -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& 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)); diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index e5c0bcddb..5d4eb3fc5 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -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;); } diff --git a/src/sat/ba_solver.cpp b/src/sat/ba_solver.cpp index 4226b9791..de6635d09 100644 --- a/src/sat/ba_solver.cpp +++ b/src/sat/ba_solver.cpp @@ -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