diff --git a/scripts/mk_project.py b/scripts/mk_project.py index ca62f5c5f..1ec5f05b5 100644 --- a/scripts/mk_project.py +++ b/scripts/mk_project.py @@ -10,7 +10,7 @@ from mk_util import * # Z3 Project definition def init_project_def(): set_version(4, 8, 0, 0) - add_lib('util', []) + add_lib('util', [], includes2install = ['z3_version.h']) add_lib('polynomial', ['util'], 'math/polynomial') add_lib('sat', ['util']) add_lib('nlsat', ['polynomial', 'sat']) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 770e118ee..ebe017739 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -2805,8 +2805,8 @@ def get_full_version_string(major, minor, build, revision): # Update files with the version number def mk_version_dot_h(major, minor, build, revision): c = get_component(UTIL_COMPONENT) - version_template = os.path.join(c.src_dir, 'version.h.in') - version_header_output = os.path.join(c.src_dir, 'version.h') + version_template = os.path.join(c.src_dir, 'z3_version.h.in') + version_header_output = os.path.join(c.src_dir, 'z3_version.h') # Note the substitution names are what is used by the CMake # builds system. If you change these you should change them # in the CMake build too diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 826f87e8c..c497c19ee 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -166,6 +166,8 @@ foreach (header ${libz3_public_headers}) set_property(TARGET libz3 APPEND PROPERTY PUBLIC_HEADER "${CMAKE_SOURCE_DIR}/src/api/${header}") endforeach() +set_property(TARGET libz3 APPEND PROPERTY + PUBLIC_HEADER "${CMAKE_CURRENT_BINARY_DIR}/util/z3_version.h") install(TARGETS libz3 EXPORT Z3_EXPORTED_TARGETS diff --git a/src/api/api_context.cpp b/src/api/api_context.cpp index cc2a13aed..4b3b85399 100644 --- a/src/api/api_context.cpp +++ b/src/api/api_context.cpp @@ -19,7 +19,7 @@ Revision History: --*/ #include #include "api/api_context.h" -#include "util/version.h" +#include "util/z3_version.h" #include "ast/ast_pp.h" #include "ast/ast_ll_pp.h" #include "api/api_log_macros.h" diff --git a/src/api/api_log.cpp b/src/api/api_log.cpp index 1bdbb8735..0f531b98e 100644 --- a/src/api/api_log.cpp +++ b/src/api/api_log.cpp @@ -19,7 +19,7 @@ Revision History: #include "api/z3.h" #include "api/api_log_macros.h" #include "util/util.h" -#include "util/version.h" +#include "util/z3_version.h" std::ostream * g_z3_log = nullptr; bool g_z3_log_enabled = false; diff --git a/src/api/api_solver.cpp b/src/api/api_solver.cpp index fc42acbb9..5a4537a4a 100644 --- a/src/api/api_solver.cpp +++ b/src/api/api_solver.cpp @@ -372,6 +372,21 @@ extern "C" { Z3_CATCH_RETURN(0); } + Z3_ast_vector Z3_API Z3_solver_get_non_units(Z3_context c, Z3_solver s) { + Z3_TRY; + LOG_Z3_solver_get_non_units(c, s); + RESET_ERROR_CODE(); + init_solver(c, s); + Z3_ast_vector_ref * v = alloc(Z3_ast_vector_ref, *mk_c(c), mk_c(c)->m()); + mk_c(c)->save_object(v); + expr_ref_vector fmls = to_solver_ref(s)->get_non_units(mk_c(c)->m()); + for (expr* f : fmls) { + v->m_ast_vector.push_back(f); + } + RETURN_Z3(of_ast_vector(v)); + Z3_CATCH_RETURN(0); + } + static Z3_lbool _solver_check(Z3_context c, Z3_solver s, unsigned num_assumptions, Z3_ast const assumptions[]) { for (unsigned i = 0; i < num_assumptions; i++) { if (!is_expr(to_ast(assumptions[i]))) { diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index e1f263e17..a283571d0 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -2038,6 +2038,8 @@ namespace z3 { stats statistics() const { Z3_stats r = Z3_solver_get_statistics(ctx(), m_solver); check_error(); return stats(ctx(), r); } expr_vector unsat_core() const { Z3_ast_vector r = Z3_solver_get_unsat_core(ctx(), m_solver); check_error(); return expr_vector(ctx(), r); } expr_vector assertions() const { Z3_ast_vector r = Z3_solver_get_assertions(ctx(), m_solver); check_error(); return expr_vector(ctx(), r); } + expr_vector non_units() const { Z3_ast_vector r = Z3_solver_get_non_units(ctx(), m_solver); check_error(); return expr_vector(ctx(), r); } + expr_vector units() const { Z3_ast_vector r = Z3_solver_get_units(ctx(), m_solver); check_error(); return expr_vector(ctx(), r); } expr proof() const { Z3_ast r = Z3_solver_get_proof(ctx(), m_solver); check_error(); return expr(ctx(), r); } friend std::ostream & operator<<(std::ostream & out, solver const & s); diff --git a/src/api/ml/z3.ml b/src/api/ml/z3.ml index 25b437bc4..231587729 100644 --- a/src/api/ml/z3.ml +++ b/src/api/ml/z3.ml @@ -1815,8 +1815,10 @@ struct | _ -> UNKNOWN let get_model x = - let q = Z3native.solver_get_model (gc x) x in - if Z3native.is_null_model q then None else Some q + try + let q = Z3native.solver_get_model (gc x) x in + if Z3native.is_null_model q then None else Some q + with | _ -> None let get_proof x = let q = Z3native.solver_get_proof (gc x) x in @@ -1952,8 +1954,10 @@ struct | _ -> Solver.UNKNOWN let get_model (x:optimize) = - let q = Z3native.optimize_get_model (gc x) x in - if Z3native.is_null_model q then None else Some q + try + let q = Z3native.optimize_get_model (gc x) x in + if Z3native.is_null_model q then None else Some q + with | _ -> None let get_lower (x:handle) = Z3native.optimize_get_lower (gc x.opt) x.opt x.h let get_upper (x:handle) = Z3native.optimize_get_upper (gc x.opt) x.opt x.h diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index 73339d478..a6b05904c 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -6605,7 +6605,12 @@ class Solver(Z3PPObject): _handle_parse_error(e, self.ctx) def cube(self, vars = None): - """Get set of cubes""" + """Get set of cubes + The method takes an optional set of variables that restrict which + variables may be used as a starting point for cubing. + If vars is not None, then the first case split is based on a variable in + this set. + """ self.cube_vs = AstVector(None, self.ctx) if vars is not None: for v in vars: @@ -6621,6 +6626,10 @@ class Solver(Z3PPObject): return def cube_vars(self): + """Access the set of variables that were touched by the most recently generated cube. + This set of variables can be used as a starting point for additional cubes. + The idea is that variables that appear in clauses that are reduced by the most recent + cube are likely more useful to cube on.""" return self.cube_vs def proof(self): @@ -6646,6 +6655,11 @@ class Solver(Z3PPObject): """ return AstVector(Z3_solver_get_units(self.ctx.ref(), self.solver), self.ctx) + def non_units(self): + """Return an AST vector containing all atomic formulas in solver state that are not units. + """ + return AstVector(Z3_solver_get_non_units(self.ctx.ref(), self.solver), self.ctx) + def statistics(self): """Return statistics for the last `check()`. diff --git a/src/api/z3_api.h b/src/api/z3_api.h index 2657e558d..03bce5d5e 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -6121,6 +6121,14 @@ extern "C" { */ Z3_ast_vector Z3_API Z3_solver_get_units(Z3_context c, Z3_solver s); + + /** + \brief Return the set of non units in the solver state. + + def_API('Z3_solver_get_non_units', AST_VECTOR, (_in(CONTEXT), _in(SOLVER))) + */ + Z3_ast_vector Z3_API Z3_solver_get_non_units(Z3_context c, Z3_solver s); + /** \brief Check whether the assertions in a given solver are consistent or not. diff --git a/src/cmd_context/basic_cmds.cpp b/src/cmd_context/basic_cmds.cpp index e65eb1b32..ea5994ece 100644 --- a/src/cmd_context/basic_cmds.cpp +++ b/src/cmd_context/basic_cmds.cpp @@ -17,7 +17,7 @@ Notes: --*/ #include "util/gparams.h" #include "util/env_params.h" -#include "util/version.h" +#include "util/z3_version.h" #include "ast/ast_smt_pp.h" #include "ast/ast_smt2_pp.h" #include "ast/ast_pp_dot.h" diff --git a/src/sat/sat_lookahead.cpp b/src/sat/sat_lookahead.cpp index 3833e2a52..4ca2c5f84 100644 --- a/src/sat/sat_lookahead.cpp +++ b/src/sat/sat_lookahead.cpp @@ -16,6 +16,8 @@ Author: Notes: + + --*/ #include diff --git a/src/sat/sat_params.pyg b/src/sat/sat_params.pyg index 89776c479..113a8133e 100644 --- a/src/sat/sat_params.pyg +++ b/src/sat/sat_params.pyg @@ -50,17 +50,39 @@ def_module_params('sat', ('unit_walk', BOOL, False, 'use unit-walk search instead of CDCL'), ('unit_walk_threads', UINT, 0, 'number of unit-walk search threads to find satisfiable solution'), ('lookahead.cube.cutoff', SYMBOL, 'depth', 'cutoff type used to create lookahead cubes: depth, freevars, psat, adaptive_freevars, adaptive_psat'), + # - depth: the maximal cutoff is fixed to the value of lookahead.cube.depth. + # So if the value is 10, at most 1024 cubes will be generated of length 10. + # - freevars: cutoff based on a variable fraction of lookahead.cube.freevars. + # Cut if the number of current unassigned variables drops below a fraction of number of initial variables. + # - psat: Let psat_heur := (Sum_{clause C} (psat.clause_base ^ {-|C|+1})) / |freevars|^psat.var_exp + # Cut if the value of psat_heur exceeds psat.trigger + # - adaptive_freevars: Cut if the number of current unassigned variables drops below a fraction of free variables + # at the time of the last conflict. The fraction is increased every time the a cutoff is created. + # - adative_psat: Cut based on psat_heur in an adaptive way. ('lookahead.cube.fraction', DOUBLE, 0.4, 'adaptive fraction to create lookahead cubes. Used when lookahead.cube.cutoff is adaptive_freevars or adaptive_psat'), ('lookahead.cube.depth', UINT, 1, 'cut-off depth to create cubes. Used when lookahead.cube.cutoff is depth.'), - ('lookahead.cube.freevars', DOUBLE, 0.8, 'cube free fariable fraction. Used when lookahead.cube.cutoff is freevars'), + ('lookahead.cube.freevars', DOUBLE, 0.8, 'cube free variable fraction. Used when lookahead.cube.cutoff is freevars'), ('lookahead.cube.psat.var_exp', DOUBLE, 1, 'free variable exponent for PSAT cutoff'), ('lookahead.cube.psat.clause_base', DOUBLE, 2, 'clause base for PSAT cutoff'), ('lookahead.cube.psat.trigger', DOUBLE, 5, 'trigger value to create lookahead cubes for PSAT cutoff. Used when lookahead.cube.cutoff is psat'), - ('lookahead_search', BOOL, False, 'use lookahead solver'), ('lookahead.preselect', BOOL, False, 'use pre-selection of subset of variables for branching'), ('lookahead_simplify', BOOL, False, 'use lookahead solver during simplification'), ('lookahead.use_learned', BOOL, False, 'use learned clauses when selecting lookahead literal'), ('lookahead_simplify.bca', BOOL, True, 'add learned binary clauses as part of lookahead simplification'), ('lookahead.global_autarky', BOOL, False, 'prefer to branch on variables that occur in clauses that are reduced'), - ('lookahead.reward', SYMBOL, 'march_cu', 'select lookahead heuristic: ternary, heule_schur (Heule Schur), heuleu (Heule Unit), unit, or march_cu'))) + ('lookahead.reward', SYMBOL, 'march_cu', 'select lookahead heuristic: ternary, heule_schur (Heule Schur), heuleu (Heule Unit), unit, or march_cu')) + # reward function used to determine which literal to cube on. + # - ternary: reward function useful for random 3-SAT instances. Used by Heule and Knuth in March. + # - heule_schur: reward function based on "Schur Number 5", Heule, AAAI 2018 + # The score of a literal lit is: + # Sum_{C in Clauses | lit in C} 2 ^ (- |C|+1) + # * Sum_{lit' in C | lit' != lit} lit_occs(~lit') + # / | C | + # where lit_occs(lit) is the number of clauses containing lit. + # - heuleu: The score of a literal lit is: Sum_{C in Clauses | lit in C} 2 ^ (-|C| + 1) + # - unit: heule_schur + also counts number of unit clauses. + # - march_cu: default reward function used in a version of March + # Each reward function also comes with its own variant of "mix_diff", which + # is the function for combining reward metrics for the positive and negative variant of a literal. + ) diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp index ff55598c2..097d3f0fa 100644 --- a/src/sat/sat_solver/inc_sat_solver.cpp +++ b/src/sat/sat_solver/inc_sat_solver.cpp @@ -259,7 +259,7 @@ public: return m_num_scopes; } - void assert_expr_core2(expr * t, expr * a) override { + void assert_expr_core2(expr * t, expr * a) override { if (a) { m_asmsf.push_back(a); assert_expr_core(m.mk_implies(a, t)); @@ -473,6 +473,7 @@ public: } void convert_internalized() { + m_solver.pop_to_base_level(); if (!is_internalized() && m_fmls_head > 0) { internalize_formulas(); } diff --git a/src/shell/main.cpp b/src/shell/main.cpp index bb1c19b47..1c8b6908d 100644 --- a/src/shell/main.cpp +++ b/src/shell/main.cpp @@ -26,7 +26,7 @@ Revision History: #include "shell/smtlib_frontend.h" #include "shell/z3_log_frontend.h" #include "util/warning.h" -#include "util/version.h" +#include "util/z3_version.h" #include "shell/dimacs_frontend.h" #include "shell/datalog_frontend.h" #include "shell/opt_frontend.h" diff --git a/src/smt/smt_arith_value.cpp b/src/smt/smt_arith_value.cpp index ce4c0d9a9..41679851a 100644 --- a/src/smt/smt_arith_value.cpp +++ b/src/smt/smt_arith_value.cpp @@ -1,4 +1,3 @@ - /*++ Copyright (c) 2018 Microsoft Corporation @@ -17,7 +16,6 @@ Author: Revision History: --*/ -#pragma once; #include "smt/smt_arith_value.h" #include "smt/theory_lra.h" diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index fd2dc0da2..5b1de851e 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -55,7 +55,7 @@ std::ostream& operator<<(std::ostream& out, bound_kind const& k) { } class bound { - smt::bool_var m_bv; + smt::bool_var m_bv; smt::theory_var m_var; bool m_is_int; rational m_value; @@ -165,13 +165,13 @@ class theory_lra::imp { expr_ref_vector m_terms; vector m_coeffs; svector m_vars; - rational m_coeff; + rational m_offset; ptr_vector m_terms_to_internalize; internalize_state(ast_manager& m): m_terms(m) {} void reset() { m_terms.reset(); m_coeffs.reset(); - m_coeff.reset(); + m_offset.reset(); m_vars.reset(); m_terms_to_internalize.reset(); } @@ -197,7 +197,7 @@ class theory_lra::imp { expr_ref_vector& terms() { return m_st.m_terms; } vector& coeffs() { return m_st.m_coeffs; } svector& vars() { return m_st.m_vars; } - rational& coeff() { return m_st.m_coeff; } + rational& offset() { return m_st.m_offset; } ptr_vector& terms_to_internalize() { return m_st.m_terms_to_internalize; } void push(expr* e, rational c) { m_st.m_terms.push_back(e); m_st.m_coeffs.push_back(c); } void set_back(unsigned i) { @@ -216,6 +216,10 @@ class theory_lra::imp { svector m_term_index2theory_var; // reverse map from lp_solver variables to theory variables var_coeffs m_left_side; // constraint left side mutable std::unordered_map m_variable_values; // current model + lp::var_index m_one_var; + lp::var_index m_zero_var; + lp::var_index m_rone_var; + lp::var_index m_rzero_var; enum constraint_source { inequality_source, @@ -331,6 +335,31 @@ class theory_lra::imp { } } + lp::var_index add_const(int c, lp::var_index& var, bool is_int) { + if (var != UINT_MAX) { + return var; + } + app_ref cnst(a.mk_numeral(rational(c), is_int), m); + TRACE("arith", tout << "add " << cnst << "\n";); + enode* e = mk_enode(cnst); + theory_var v = mk_var(cnst); + var = m_solver->add_var(v, true); + m_theory_var2var_index.setx(v, var, UINT_MAX); + m_var_index2theory_var.setx(var, v, UINT_MAX); + m_var_trail.push_back(v); + add_def_constraint(m_solver->add_var_bound(var, lp::GE, rational(c))); + add_def_constraint(m_solver->add_var_bound(var, lp::LE, rational(c))); + return var; + } + + lp::var_index get_one(bool is_int) { + return add_const(1, is_int ? m_one_var : m_rone_var, is_int); + } + + lp::var_index get_zero(bool is_int) { + return add_const(0, is_int ? m_zero_var : m_rzero_var, is_int); + } + void found_not_handled(expr* n) { m_not_handled = n; @@ -375,7 +404,7 @@ class theory_lra::imp { expr_ref_vector & terms = st.terms(); svector& vars = st.vars(); vector& coeffs = st.coeffs(); - rational& coeff = st.coeff(); + rational& offset = st.offset(); rational r; expr* n1, *n2; unsigned index = 0; @@ -415,7 +444,7 @@ class theory_lra::imp { ++index; } else if (a.is_numeral(n, r)) { - coeff += coeffs[index]*r; + offset += coeffs[index]*r; ++index; } else if (a.is_uminus(n, n1)) { @@ -427,7 +456,6 @@ class theory_lra::imp { app* t = to_app(n); internalize_args(t); mk_enode(t); - theory_var v = mk_var(n); coeffs[vars.size()] = coeffs[index]; vars.push_back(v); @@ -550,6 +578,7 @@ class theory_lra::imp { } enode * mk_enode(app * n) { + TRACE("arith", tout << expr_ref(n, m) << "\n";); if (ctx().e_internalized(n)) { return get_enode(n); } @@ -738,10 +767,19 @@ class theory_lra::imp { } bool is_unit_var(scoped_internalize_state& st) { - return st.coeff().is_zero() && st.vars().size() == 1 && st.coeffs()[0].is_one(); + return st.offset().is_zero() && st.vars().size() == 1 && st.coeffs()[0].is_one(); + } + + bool is_one(scoped_internalize_state& st) { + return st.offset().is_one() && st.vars().empty(); + } + + bool is_zero(scoped_internalize_state& st) { + return st.offset().is_zero() && st.vars().empty(); } theory_var internalize_def(app* term, scoped_internalize_state& st) { + TRACE("arith", tout << expr_ref(term, m) << "\n";); if (ctx().e_internalized(term)) { IF_VERBOSE(0, verbose_stream() << "repeated term\n";); return mk_var(term, false); @@ -771,13 +809,24 @@ class theory_lra::imp { if (is_unit_var(st)) { return st.vars()[0]; } + else if (is_one(st)) { + return get_one(a.is_int(term)); + } + else if (is_zero(st)) { + return get_zero(a.is_int(term)); + } else { init_left_side(st); theory_var v = mk_var(term); lp::var_index vi = m_theory_var2var_index.get(v, UINT_MAX); - TRACE("arith", tout << mk_pp(term, m) << " " << v << " " << vi << "\n";); + TRACE("arith", tout << mk_pp(term, m) << " v" << v << "\n";); if (vi == UINT_MAX) { - vi = m_solver->add_term(m_left_side, st.coeff()); + rational const& offset = st.offset(); + if (!offset.is_zero()) { + m_left_side.push_back(std::make_pair(offset, get_one(a.is_int(term)))); + } + SASSERT(!m_left_side.empty()); + vi = m_solver->add_term(m_left_side); m_theory_var2var_index.setx(v, vi, UINT_MAX); if (m_solver->is_term(vi)) { m_term_index2theory_var.setx(m_solver->adjust_term_index(vi), v, UINT_MAX); @@ -806,6 +855,10 @@ public: m_has_int(false), m_arith_eq_adapter(th, ap, a), m_internalize_head(0), + m_one_var(UINT_MAX), + m_zero_var(UINT_MAX), + m_rone_var(UINT_MAX), + m_rzero_var(UINT_MAX), m_not_handled(nullptr), m_asserted_qhead(0), m_assume_eq_head(0), @@ -877,16 +930,18 @@ public: } return true; } + + bool is_arith(enode* n) { + return n && n->get_th_var(get_id()) != null_theory_var; + } void internalize_eq_eh(app * atom, bool_var) { - expr* lhs = 0, *rhs = 0; + TRACE("arith_verbose", tout << mk_pp(atom, m) << "\n";); + expr* lhs = nullptr, *rhs = nullptr; VERIFY(m.is_eq(atom, lhs, rhs)); enode * n1 = get_enode(lhs); enode * n2 = get_enode(rhs); - if (n1->get_th_var(get_id()) != null_theory_var && - n2->get_th_var(get_id()) != null_theory_var && - n1 != n2) { - TRACE("arith_verbose", tout << mk_pp(atom, m) << "\n";); + if (is_arith(n1) && is_arith(n2) && n1 != n2) { m_arith_eq_adapter.mk_axioms(n1, n2); } } @@ -1197,7 +1252,6 @@ public: m_todo_terms.pop_back(); if (m_solver->is_term(vi)) { const lp::lar_term& term = m_solver->get_term(vi); - result += term.m_v * coeff; for (const auto & i: term) { m_todo_terms.push_back(std::make_pair(i.var(), coeff * i.coeff())); } @@ -1234,7 +1288,6 @@ public: m_todo_terms.pop_back(); if (m_solver->is_term(wi)) { const lp::lar_term& term = m_solver->get_term(wi); - result += term.m_v * coeff; for (const auto & i : term) { if (m_variable_values.count(i.var()) > 0) { result += m_variable_values[i.var()] * coeff * i.coeff(); @@ -1255,6 +1308,7 @@ public: void init_variable_values() { reset_variable_values(); if (!m.canceled() && m_solver.get() && th.get_num_vars() > 0) { + TRACE("arith", tout << "update variable values\n";); m_solver->get_model(m_variable_values); } } @@ -1481,8 +1535,8 @@ public: bool all_bounded = true; for (unsigned v = 0; v < nv; ++v) { lp::var_index vi = m_theory_var2var_index[v]; - if (vi == UINT_MAX) - continue; + if (vi == UINT_MAX) + continue; if (!m_solver->is_term(vi) && !var_has_bound(vi, true) && !var_has_bound(vi, false)) { lp::lar_term term; term.add_monomial(rational::one(), vi); @@ -1516,23 +1570,10 @@ public: theory_var v = mk_var(n); theory_var v1 = mk_var(p); theory_var v2 = mk_var(q); - rational r = get_value(v); rational r1 = get_value(v1); - rational r2 = get_value(v2); - rational r3; - if (r2.is_zero()) { - continue; - } - if (r1.is_int() && r2.is_int() && r == div(r1, r2)) { - continue; - } - if (r2.is_neg() || r1.is_neg()) { - // TBD - continue; - } + rational r2; - if (!r1.is_int() || !r2.is_int()) { - // std::cout << r1 << " " << r2 << " " << r << " " << expr_ref(n, m) << "\n"; + if (!r1.is_int() || r1.is_neg()) { // TBD // r1 = 223/4, r2 = 2, r = 219/8 // take ceil(r1), floor(r1), ceil(r2), floor(r2), for floor(r2) > 0 @@ -1542,16 +1583,18 @@ public: continue; } - if (a.is_numeral(q, r3)) { + if (a.is_numeral(q, r2) && r2.is_pos()) { + if (get_value(v) == div(r1, r2)) continue; - SASSERT(r3 == r2 && r2.is_int()); - SASSERT(r1.is_int() && r3.is_int()); rational div_r = div(r1, r2); // p <= q * div(r1, q) + q - 1 => div(p, q) <= div(r1, r2) // p >= q * div(r1, q) => div(r1, q) <= div(p, q) rational mul(1); rational hi = r2 * div_r + r2 - 1; rational lo = r2 * div_r; + + // used to normalize inequalities so they + // don't appear as 8*x >= 15, but x >= 2 expr *n1 = nullptr, *n2 = nullptr; if (a.is_mul(p, n1, n2) && is_numeral(n1, mul) && mul.is_pos()) { p = n2; @@ -1568,7 +1611,7 @@ public: all_divs_valid = false; TRACE("arith", - tout << r1 << " div " << r2 << " = " << r3 << "\n"; + tout << r1 << " div " << r2 << "\n"; literal_vector lits; lits.push_back(~p_le_r1); lits.push_back(n_le_div); @@ -1578,8 +1621,10 @@ public: ctx().display_literals_verbose(tout, lits) << "\n";); continue; } +#if 0 - + // TBD similar for non-linear division. + // better to deal with in nla_solver: all_divs_valid = false; @@ -1610,6 +1655,7 @@ public: lits[0] = pq_rhs; lits[1] = n_ge_div; ctx().display_literals_verbose(tout, lits) << "\n";); +#endif } return all_divs_valid; @@ -1708,17 +1754,13 @@ public: TRACE("arith", tout << "idiv bounds check\n";); return l_false; } - lp::lar_term term; - lp::mpq k; - lp::explanation ex; // TBD, this should be streamlined accross different explanations - bool upper; m_explanation.reset(); - switch(m_lia->check(term, k, ex, upper)) { + switch (m_lia->check()) { case lp::lia_move::sat: return l_true; case lp::lia_move::branch: { TRACE("arith", tout << "branch\n";); - app_ref b = mk_bound(term, k, !upper); + app_ref b = mk_bound(m_lia->get_term(), m_lia->get_offset(), !m_lia->is_upper()); IF_VERBOSE(2, verbose_stream() << "branch " << b << "\n";); // branch on term >= k + 1 // branch on term <= k @@ -1731,13 +1773,13 @@ public: TRACE("arith", tout << "cut\n";); ++m_stats.m_gomory_cuts; // m_explanation implies term <= k - app_ref b = mk_bound(term, k, !upper); + app_ref b = mk_bound(m_lia->get_term(), m_lia->get_offset(), !m_lia->is_upper()); IF_VERBOSE(2, verbose_stream() << "cut " << b << "\n"); - TRACE("arith", dump_cut_lemma(tout, term, k, ex, upper);); + TRACE("arith", dump_cut_lemma(tout, m_lia->get_term(), m_lia->get_offset(), m_lia->get_explanation(), m_lia->is_upper());); m_eqs.reset(); m_core.reset(); m_params.reset(); - for (auto const& ev : ex.m_explanation) { + for (auto const& ev : m_lia->get_explanation().m_explanation) { if (!ev.first.is_zero()) { set_evidence(ev.second); } @@ -1752,7 +1794,7 @@ public: case lp::lia_move::conflict: TRACE("arith", tout << "conflict\n";); // ex contains unsat core - m_explanation = ex.m_explanation; + m_explanation = m_lia->get_explanation().m_explanation; set_conflict1(); return l_false; case lp::lia_move::undef: @@ -2921,7 +2963,7 @@ public: lp::lar_term const& term = m_solver->get_term(vi); TRACE("arith", m_solver->print_term(term, tout) << "\n";); scoped_anum r1(m_nra->am()); - rational c1 = term.m_v * wcoeff; + rational c1(0); m_nra->am().set(r1, c1.to_mpq()); m_nra->am().add(r, r1, r); for (auto const & arg : term) { @@ -2968,6 +3010,7 @@ public: if (!can_get_bound(v)) return false; lp::var_index vi = m_theory_var2var_index[v]; if (m_solver->has_value(vi, val)) { + TRACE("arith", tout << expr_ref(n->get_owner(), m) << " := " << val << "\n";); if (is_int(n) && !val.is_int()) return false; return true; } @@ -3196,7 +3239,6 @@ public: coeffs.find(w, c0); coeffs.insert(w, c0 + ti.coeff() * coeff); } - offset += coeff * term.m_v; } app_ref coeffs2app(u_map const& coeffs, rational const& offset, bool is_int) { diff --git a/src/solver/solver.cpp b/src/solver/solver.cpp index 4044c4a85..0e2128990 100644 --- a/src/solver/solver.cpp +++ b/src/solver/solver.cpp @@ -178,10 +178,19 @@ lbool solver::preferred_sat(expr_ref_vector const& asms, vector return check_sat(0, nullptr); } -bool solver::is_literal(ast_manager& m, expr* e) { - return is_uninterp_const(e) || (m.is_not(e, e) && is_uninterp_const(e)); + +static bool is_m_atom(ast_manager& m, expr* f) { + if (!is_app(f)) return true; + app* _f = to_app(f); + family_id bfid = m.get_basic_family_id(); + if (_f->get_family_id() != bfid) return true; + if (_f->get_num_args() > 0 && m.is_bool(_f->get_arg(0))) return false; + return m.is_eq(f) || m.is_distinct(f); } +bool solver::is_literal(ast_manager& m, expr* e) { + return is_m_atom(m, e) || (m.is_not(e, e) && is_m_atom(m, e)); +} void solver::assert_expr(expr* f) { expr_ref fml(f, get_manager()); @@ -256,3 +265,40 @@ expr_ref_vector solver::get_units(ast_manager& m) { return result; } + + +expr_ref_vector solver::get_non_units(ast_manager& m) { + expr_ref_vector result(m), fmls(m); + get_assertions(fmls); + family_id bfid = m.get_basic_family_id(); + expr_mark marked; + unsigned sz0 = fmls.size(); + for (unsigned i = 0; i < fmls.size(); ++i) { + expr* f = fmls.get(i); + if (marked.is_marked(f)) continue; + marked.mark(f); + if (!is_app(f)) { + if (i >= sz0) result.push_back(f); + continue; + } + app* _f = to_app(f); + if (_f->get_family_id() == bfid) { + // basic objects are true/false/and/or/not/=/distinct + // and proof objects (that are not Boolean). + if (i < sz0 && m.is_not(f) && is_m_atom(m, _f->get_arg(0))) { + marked.mark(_f->get_arg(0)); + } + else if (_f->get_num_args() > 0 && m.is_bool(_f->get_arg(0))) { + fmls.append(_f->get_num_args(), _f->get_args()); + } + else if (i >= sz0 && is_m_atom(m, f)) { + result.push_back(f); + } + } + + else { + if (i >= sz0) result.push_back(f); + } + } + return result; +} diff --git a/src/solver/solver.h b/src/solver/solver.h index c371be284..5329161cd 100644 --- a/src/solver/solver.h +++ b/src/solver/solver.h @@ -236,6 +236,8 @@ public: */ expr_ref_vector get_units(ast_manager& m); + expr_ref_vector get_non_units(ast_manager& m); + class scoped_push { solver& s; bool m_nopop; diff --git a/src/test/lp/gomory_test.h b/src/test/lp/gomory_test.h index 501ad9e1a..972466dc3 100644 --- a/src/test/lp/gomory_test.h +++ b/src/test/lp/gomory_test.h @@ -185,7 +185,6 @@ struct gomory_test { } void print_term(lar_term & t, std::ostream & out) { - lp_assert(is_zero(t.m_v)); vector> row; for (auto p : t.m_coeffs) row.push_back(std::make_pair(p.second, p.first)); diff --git a/src/test/lp/lp.cpp b/src/test/lp/lp.cpp index 6e418fe68..ff9de0e58 100644 --- a/src/test/lp/lp.cpp +++ b/src/test/lp/lp.cpp @@ -2667,13 +2667,20 @@ void test_term() { lar_solver solver; unsigned _x = 0; unsigned _y = 1; + unsigned _one = 2; var_index x = solver.add_var(_x, false); var_index y = solver.add_var(_y, false); + var_index one = solver.add_var(_one, false); + + vector> term_one; + term_one.push_back(std::make_pair((int)1, one)); + solver.add_constraint(term_one, lconstraint_kind::EQ, mpq(0)); vector> term_ls; term_ls.push_back(std::pair((int)1, x)); term_ls.push_back(std::pair((int)1, y)); - var_index z = solver.add_term(term_ls, mpq(3)); + term_ls.push_back(std::make_pair((int)3, one)); + var_index z = solver.add_term(term_ls); vector> ls; ls.push_back(std::pair((int)1, x)); @@ -2743,10 +2750,10 @@ void test_bound_propagation_one_small_sample1() { vector> coeffs; coeffs.push_back(std::pair(1, a)); coeffs.push_back(std::pair(-1, c)); - ls.add_term(coeffs, zero_of_type()); + ls.add_term(coeffs); coeffs.pop_back(); coeffs.push_back(std::pair(-1, b)); - ls.add_term(coeffs, zero_of_type()); + ls.add_term(coeffs); coeffs.clear(); coeffs.push_back(std::pair(1, a)); coeffs.push_back(std::pair(-1, b)); @@ -3485,12 +3492,12 @@ void test_maximize_term() { vector> term_ls; term_ls.push_back(std::pair((int)1, x)); term_ls.push_back(std::pair((int)-1, y)); - unsigned term_x_min_y = solver.add_term(term_ls, mpq(0)); + unsigned term_x_min_y = solver.add_term(term_ls); term_ls.clear(); term_ls.push_back(std::pair((int)2, x)); term_ls.push_back(std::pair((int)2, y)); - unsigned term_2x_pl_2y = solver.add_term(term_ls, mpq(0)); + unsigned term_2x_pl_2y = solver.add_term(term_ls); solver.add_var_bound(term_x_min_y, LE, zero_of_type()); solver.add_var_bound(term_2x_pl_2y, LE, mpq((int)5)); solver.find_feasible_solution(); @@ -3502,8 +3509,7 @@ void test_maximize_term() { std::cout<< "v[" << p.first << "] = " << p.second << std::endl; } std::cout << "calling int_solver\n"; - lar_term t; mpq k; explanation ex; bool upper; - lia_move lm = i_solver.check(t, k, ex, upper); + lia_move lm = i_solver.check(); VERIFY(lm == lia_move::sat); impq term_max; lp_status st = solver.maximize_term(term_2x_pl_2y, term_max); diff --git a/src/util/CMakeLists.txt b/src/util/CMakeLists.txt index 85b6f955c..b6abb785f 100644 --- a/src/util/CMakeLists.txt +++ b/src/util/CMakeLists.txt @@ -1,11 +1,12 @@ -if (EXISTS "${CMAKE_CURRENT_SOURCE_DIR}/version.h") - message(FATAL_ERROR "\"${CMAKE_CURRENT_SOURCE_DIR}/version.h\"" +if (EXISTS "${CMAKE_CURRENT_SOURCE_DIR}/z3_version.h") + message(FATAL_ERROR "\"${CMAKE_CURRENT_SOURCE_DIR}/z3_version.h\"" ${z3_polluted_tree_msg} ) endif() set(Z3_FULL_VERSION "\"${Z3_FULL_VERSION_STR}\"") -configure_file(version.h.cmake.in ${CMAKE_CURRENT_BINARY_DIR}/version.h) +configure_file(z3_version.h.cmake.in ${CMAKE_CURRENT_BINARY_DIR}/z3_version.h) + z3_add_component(util SOURCES diff --git a/src/util/lp/bound_propagator.cpp b/src/util/lp/bound_propagator.cpp index c4fa2aefa..a5c7c976a 100644 --- a/src/util/lp/bound_propagator.cpp +++ b/src/util/lp/bound_propagator.cpp @@ -17,10 +17,6 @@ const impq & bound_propagator::get_upper_bound(unsigned j) const { } void bound_propagator::try_add_bound(mpq v, unsigned j, bool is_low, bool coeff_before_j_is_pos, unsigned row_or_term_index, bool strict) { j = m_lar_solver.adjust_column_index_to_term_index(j); - if (m_lar_solver.is_term(j)) { - // lp treats terms as not having a free coefficient, restoring it below for the outside consumption - v += m_lar_solver.get_term(j).m_v; - } lconstraint_kind kind = is_low? GE : LE; if (strict) diff --git a/src/util/lp/column_info.h b/src/util/lp/column_info.h index 407f40dfc..2a38900c1 100644 --- a/src/util/lp/column_info.h +++ b/src/util/lp/column_info.h @@ -69,16 +69,6 @@ public: m_column_index(static_cast(-1)) {} - column_info(unsigned column_index) : - m_lower_bound_is_set(false), - m_lower_bound_is_strict(false), - m_upper_bound_is_set (false), - m_upper_bound_is_strict (false), - m_is_fixed(false), - m_cost(numeric_traits::zero()), - m_column_index(column_index) { - } - column_info(const column_info & ci) { m_name = ci.m_name; m_lower_bound_is_set = ci.m_lower_bound_is_set; diff --git a/src/util/lp/gomory.cpp b/src/util/lp/gomory.cpp index 53e12c7ec..ad1c02625 100644 --- a/src/util/lp/gomory.cpp +++ b/src/util/lp/gomory.cpp @@ -27,11 +27,15 @@ class gomory::imp { lar_term & m_t; // the term to return in the cut mpq & m_k; // the right side of the cut explanation& m_ex; // the conflict explanation - unsigned m_inf_col; // a basis column which has to be an integer but has a not integral value + unsigned m_inf_col; // a basis column which has to be an integer but has a non integral value const row_strip& m_row; - const int_solver& m_int_solver; - - + const int_solver& m_int_solver; + mpq m_lcm_den; + mpq m_f; + mpq m_one_minus_f; + mpq m_fj; + mpq m_one_minus_fj; + const impq & get_value(unsigned j) const { return m_int_solver.get_value(j); } bool is_real(unsigned j) const { return m_int_solver.is_real(j); } bool at_lower(unsigned j) const { return m_int_solver.at_lower(j); } @@ -41,65 +45,61 @@ class gomory::imp { constraint_index column_lower_bound_constraint(unsigned j) const { return m_int_solver.column_lower_bound_constraint(j); } constraint_index column_upper_bound_constraint(unsigned j) const { return m_int_solver.column_upper_bound_constraint(j); } bool column_is_fixed(unsigned j) const { return m_int_solver.m_lar_solver->column_is_fixed(j); } - void int_case_in_gomory_cut(const mpq & a, unsigned j, - mpq & lcm_den, const mpq& f0, const mpq& one_minus_f0) { - lp_assert(is_int(j) && !a.is_int()); - mpq fj = fractional_part(a); + + void int_case_in_gomory_cut(unsigned j) { + lp_assert(is_int(j) && m_fj.is_pos()); TRACE("gomory_cut_detail", - tout << a << " j=" << j << " k = " << m_k; - tout << ", fj: " << fj << ", "; - tout << "a - fj = " << a - fj << ", "; + tout << " k = " << m_k; + tout << ", fj: " << m_fj << ", "; tout << (at_lower(j)?"at_lower":"at_upper")<< std::endl; ); - lp_assert(fj.is_pos() && (a - fj).is_int()); mpq new_a; - mpq one_minus_fj = 1 - fj; if (at_lower(j)) { - new_a = fj < one_minus_f0? fj / one_minus_f0 : one_minus_fj / f0; + new_a = m_fj <= m_one_minus_f ? m_fj / m_one_minus_f : ((1 - m_fj) / m_f); + lp_assert(new_a.is_pos()); m_k.addmul(new_a, lower_bound(j).x); - m_ex.push_justification(column_lower_bound_constraint(j), new_a); + m_ex.push_justification(column_lower_bound_constraint(j)); } else { lp_assert(at_upper(j)); // the upper terms are inverted: therefore we have the minus - new_a = - (fj < f0? fj / f0 : one_minus_fj / one_minus_f0); + new_a = - (m_fj <= m_f ? m_fj / m_f : ((1 - m_fj) / m_one_minus_f)); + lp_assert(new_a.is_neg()); m_k.addmul(new_a, upper_bound(j).x); - m_ex.push_justification(column_upper_bound_constraint(j), new_a); + m_ex.push_justification(column_upper_bound_constraint(j)); } m_t.add_monomial(new_a, j); - lcm_den = lcm(lcm_den, denominator(new_a)); - TRACE("gomory_cut_detail", tout << "new_a = " << new_a << ", k = " << m_k << ", lcm_den = " << lcm_den << "\n";); + m_lcm_den = lcm(m_lcm_den, denominator(new_a)); + TRACE("gomory_cut_detail", tout << "v" << j << " new_a = " << new_a << ", k = " << m_k << ", m_lcm_den = " << m_lcm_den << "\n";); } - void real_case_in_gomory_cut(const mpq & a, unsigned x_j, const mpq& f0, const mpq& one_minus_f0) { + void real_case_in_gomory_cut(const mpq & a, unsigned j) { TRACE("gomory_cut_detail_real", tout << "real\n";); mpq new_a; - if (at_lower(x_j)) { + if (at_lower(j)) { if (a.is_pos()) { - new_a = a / one_minus_f0; + new_a = a / m_one_minus_f; } else { - new_a = a / f0; - new_a.neg(); + new_a = - a / m_f; } - m_k.addmul(new_a, lower_bound(x_j).x); // is it a faster operation than - // k += lower_bound(x_j).x * new_a; - m_ex.push_justification(column_lower_bound_constraint(x_j), new_a); + m_k.addmul(new_a, lower_bound(j).x); // is it a faster operation than + // k += lower_bound(j).x * new_a; + m_ex.push_justification(column_lower_bound_constraint(j)); } else { - lp_assert(at_upper(x_j)); + lp_assert(at_upper(j)); if (a.is_pos()) { - new_a = a / f0; - new_a.neg(); // the upper terms are inverted. + new_a = - a / m_f; } else { - new_a = a / one_minus_f0; + new_a = a / m_one_minus_f; } - m_k.addmul(new_a, upper_bound(x_j).x); // k += upper_bound(x_j).x * new_a; - m_ex.push_justification(column_upper_bound_constraint(x_j), new_a); + m_k.addmul(new_a, upper_bound(j).x); // k += upper_bound(j).x * new_a; + m_ex.push_justification(column_upper_bound_constraint(j)); } - TRACE("gomory_cut_detail_real", tout << a << "*v" << x_j << " k: " << m_k << "\n";); - m_t.add_monomial(new_a, x_j); + TRACE("gomory_cut_detail_real", tout << a << "*v" << j << " k: " << m_k << "\n";); + m_t.add_monomial(new_a, j); } lia_move report_conflict_from_gomory_cut() { @@ -109,8 +109,9 @@ class gomory::imp { return lia_move::conflict; } - void adjust_term_and_k_for_some_ints_case_gomory(mpq &lcm_den) { + void adjust_term_and_k_for_some_ints_case_gomory() { lp_assert(!m_t.is_empty()); + // k = 1 + sum of m_t at bounds auto pol = m_t.coeffs_as_vector(); m_t.clear(); if (pol.size() == 1) { @@ -131,20 +132,22 @@ class gomory::imp { m_t.add_monomial(mpq(1), v); } } else { - TRACE("gomory_cut_detail", tout << "pol.size() > 1" << std::endl;); - lcm_den = lcm(lcm_den, denominator(m_k)); - lp_assert(lcm_den.is_pos()); - if (!lcm_den.is_one()) { + m_lcm_den = lcm(m_lcm_den, denominator(m_k)); + lp_assert(m_lcm_den.is_pos()); + TRACE("gomory_cut_detail", tout << "pol.size() > 1 den: " << m_lcm_den << std::endl;); + if (!m_lcm_den.is_one()) { // normalize coefficients of integer parameters to be integers. for (auto & pi: pol) { - pi.first *= lcm_den; + pi.first *= m_lcm_den; SASSERT(!is_int(pi.second) || pi.first.is_int()); } - m_k *= lcm_den; + m_k *= m_lcm_den; } // negate everything to return -pol <= -m_k - for (const auto & pi: pol) + for (const auto & pi: pol) { + TRACE("gomory_cut", tout << pi.first << "* " << "v" << pi.second << "\n";); m_t.add_monomial(-pi.first, pi.second); + } m_k.neg(); } TRACE("gomory_cut_detail", tout << "k = " << m_k << std::endl;); @@ -155,21 +158,16 @@ class gomory::imp { return std::string("x") + std::to_string(j); } - void dump_coeff_val(std::ostream & out, const mpq & a) const { + std::ostream& dump_coeff_val(std::ostream & out, const mpq & a) const { if (a.is_int()) { - if ( a >= zero_of_type()) - out << a; - else { - out << "( - " << - a << ") "; - } - } else { - if ( a >= zero_of_type()) - out << "(div " << numerator(a) << " " << denominator(a) << ")"; - else { - out << "(- ( div " << numerator(-a) << " " << denominator(-a) << "))"; - } - + out << a; + } + else if ( a >= zero_of_type()) + out << "(/ " << numerator(a) << " " << denominator(a) << ")"; + else { + out << "(- ( / " << numerator(-a) << " " << denominator(-a) << "))"; } + return out; } template @@ -179,80 +177,82 @@ class gomory::imp { out << " " << var_name(c.var()) << ")"; } - void dump_row_coefficients(std::ostream & out) const { + std::ostream& dump_row_coefficients(std::ostream & out) const { + mpq lc(1); for (const auto& p : m_row) { - if (!column_is_fixed(p.var())) - dump_coeff(out, p); + lc = lcm(lc, denominator(p.coeff())); + } + for (const auto& p : m_row) { + dump_coeff_val(out << " (* ", p.coeff()*lc) << " " << var_name(p.var()) << ")"; } + return out; } void dump_the_row(std::ostream& out) const { out << "; the row, excluding fixed vars\n"; - out << "(assert ( = ( + "; - dump_row_coefficients(out); - out << ") 0))\n"; + out << "(assert ( = ( +"; + dump_row_coefficients(out) << ") 0))\n"; + } + + void dump_declaration(std::ostream& out, unsigned v) const { + out << "(declare-const " << var_name(v) << (is_int(v) ? " Int" : " Real") << ")\n"; } void dump_declarations(std::ostream& out) const { // for a column j the var name is vj for (const auto & p : m_row) { - if (column_is_fixed(p.var())) continue; - out << "(declare-fun " << var_name(p.var()) << " () " - << (is_int(p.var())? "Int" : "Real") << ")\n"; + dump_declaration(out, p.var()); + } + for (const auto& p : m_t) { + unsigned v = p.var(); + if (m_int_solver.m_lar_solver->is_term(v)) { + dump_declaration(out, v); + } } } void dump_lower_bound_expl(std::ostream & out, unsigned j) const { - out << "(assert ( >= " << var_name(j) << " " << lower_bound(j).x << "))\n"; + out << "(assert (>= " << var_name(j) << " " << lower_bound(j).x << "))\n"; } void dump_upper_bound_expl(std::ostream & out, unsigned j) const { - out << "(assert ( <= " << var_name(j) << " " << upper_bound(j).x << "))\n"; + out << "(assert (<= " << var_name(j) << " " << upper_bound(j).x << "))\n"; } void dump_explanations(std::ostream& out) const { for (const auto & p : m_row) { unsigned j = p.var(); - if (column_is_fixed(j)) continue; - if (j == m_inf_col) { + if (j == m_inf_col || (!is_real(j) && p.coeff().is_int())) { continue; } - - if (column_is_fixed(j)) { - dump_lower_bound_expl(out, j); - dump_upper_bound_expl(out, j); - continue; - } - - if (at_lower(j)) { + else if (at_lower(j)) { dump_lower_bound_expl(out, j); } else { + lp_assert(at_upper(j)); dump_upper_bound_expl(out, j); } } } - void dump_terms_coefficients(std::ostream & out) const { + std::ostream& dump_term_coefficients(std::ostream & out) const { for (const auto& p : m_t) { dump_coeff(out, p); } + return out; } - void dump_term_sum(std::ostream & out) const { - out << "( + "; - dump_terms_coefficients(out); - out << ")"; + std::ostream& dump_term_sum(std::ostream & out) const { + return dump_term_coefficients(out << "(+ ") << ")"; } - void dump_term_le_k(std::ostream & out) const { - out << "( <= "; - dump_term_sum(out); - out << m_k << ")"; + std::ostream& dump_term_le_k(std::ostream & out) const { + return dump_term_sum(out << "(<= ") << " " << m_k << ")"; } + void dump_the_cut_assert(std::ostream & out) const { - out <<"(assert (not "; - dump_term_le_k(out); - out << "))\n"; + dump_term_le_k(out << "(assert (not ") << "))\n"; } + + void dump_cut_and_constraints_as_smt_lemma(std::ostream& out) const { dump_declarations(out); dump_the_row(out); @@ -272,55 +272,59 @@ public: // gomory will be t <= k and the current solution has a property t > k m_k = 1; - mpq lcm_den(1); + m_t.clear(); + mpq m_lcm_den(1); bool some_int_columns = false; - mpq f0 = fractional_part(get_value(m_inf_col)); - TRACE("gomory_cut_detail", tout << "f0: " << f0 << ", "; - tout << "1 - f0: " << 1 - f0 << ", get_value(m_inf_col).x - f0 = " << get_value(m_inf_col).x - f0;); - lp_assert(f0.is_pos() && (get_value(m_inf_col).x - f0).is_int()); + mpq m_f = fractional_part(get_value(m_inf_col)); + TRACE("gomory_cut_detail", tout << "m_f: " << m_f << ", "; + tout << "1 - m_f: " << 1 - m_f << ", get_value(m_inf_col).x - m_f = " << get_value(m_inf_col).x - m_f;); + lp_assert(m_f.is_pos() && (get_value(m_inf_col).x - m_f).is_int()); - mpq one_min_f0 = 1 - f0; + mpq one_min_m_f = 1 - m_f; for (const auto & p : m_row) { unsigned j = p.var(); - if (column_is_fixed(j)) { - m_ex.push_justification(column_lower_bound_constraint(j)); - m_ex.push_justification(column_upper_bound_constraint(j)); - continue; - } if (j == m_inf_col) { lp_assert(p.coeff() == one_of_type()); TRACE("gomory_cut_detail", tout << "seeing basic var";); continue; } - // make the format compatible with the format used in: Integrating Simplex with DPLL(T) - mpq a = - p.coeff(); - if (is_real(j)) - real_case_in_gomory_cut(a, j, f0, one_min_f0); - else if (!a.is_int()) { // fj will be zero and no monomial will be added + + // use -p.coeff() to make the format compatible with the format used in: Integrating Simplex with DPLL(T) + if (is_real(j)) { + real_case_in_gomory_cut(- p.coeff(), j); + } else { + if (p.coeff().is_int()) { + // m_fj will be zero and no monomial will be added + continue; + } some_int_columns = true; - int_case_in_gomory_cut(a, j, lcm_den, f0, one_min_f0); + m_fj = fractional_part(-p.coeff()); + m_one_minus_fj = 1 - m_fj; + int_case_in_gomory_cut(j); } } if (m_t.is_empty()) return report_conflict_from_gomory_cut(); if (some_int_columns) - adjust_term_and_k_for_some_ints_case_gomory(lcm_den); + adjust_term_and_k_for_some_ints_case_gomory(); lp_assert(m_int_solver.current_solution_is_inf_on_cut()); - m_int_solver.m_lar_solver->subs_term_columns(m_t, m_k); - TRACE("gomory_cut", tout<<"gomory cut:"; print_linear_combination_of_column_indices_only(m_t, tout); tout << " <= " << m_k << std::endl;); TRACE("gomory_cut_detail", dump_cut_and_constraints_as_smt_lemma(tout);); + m_int_solver.m_lar_solver->subs_term_columns(m_t); + TRACE("gomory_cut", print_linear_combination_of_column_indices_only(m_t, tout << "gomory cut:"); tout << " <= " << m_k << std::endl;); return lia_move::cut; } + imp(lar_term & t, mpq & k, explanation& ex, unsigned basic_inf_int_j, const row_strip& row, const int_solver& int_slv ) : m_t(t), m_k(k), m_ex(ex), m_inf_col(basic_inf_int_j), m_row(row), - m_int_solver(int_slv) - { - } + m_int_solver(int_slv), + m_lcm_den(1), + m_f(fractional_part(get_value(basic_inf_int_j).x)), + m_one_minus_f(1 - m_f) {} }; diff --git a/src/util/lp/int_solver.cpp b/src/util/lp/int_solver.cpp index cc01a0038..83fbe3961 100644 --- a/src/util/lp/int_solver.cpp +++ b/src/util/lp/int_solver.cpp @@ -125,19 +125,19 @@ constraint_index int_solver::column_lower_bound_constraint(unsigned j) const { bool int_solver::current_solution_is_inf_on_cut() const { const auto & x = m_lar_solver->m_mpq_lar_core_solver.m_r_x; - impq v = m_t->apply(x); - mpq sign = *m_upper ? one_of_type() : -one_of_type(); - CTRACE("current_solution_is_inf_on_cut", v * sign <= (*m_k) * sign, - tout << "m_upper = " << *m_upper << std::endl; - tout << "v = " << v << ", k = " << (*m_k) << std::endl; + impq v = m_t.apply(x); + mpq sign = m_upper ? one_of_type() : -one_of_type(); + CTRACE("current_solution_is_inf_on_cut", v * sign <= m_k * sign, + tout << "m_upper = " << m_upper << std::endl; + tout << "v = " << v << ", k = " << m_k << std::endl; ); - return v * sign > (*m_k) * sign; + return v * sign > m_k * sign; } lia_move int_solver::mk_gomory_cut( unsigned inf_col, const row_strip & row) { lp_assert(column_is_int_inf(inf_col)); - gomory gc(*m_t, *m_k, *m_ex, inf_col, row, *this); + gomory gc(m_t, m_k, m_ex, inf_col, row, *this); return gc.create_cut(); } @@ -147,7 +147,7 @@ lia_move int_solver::proceed_with_gomory_cut(unsigned j) { if (!is_gomory_cut_target(row)) return create_branch_on_column(j); - *m_upper = true; + m_upper = true; return mk_gomory_cut(j, row); } @@ -189,7 +189,7 @@ struct check_return_helper { m_lar_solver->set_track_pivoted_rows(m_track_pivoted_rows); if (m_r == lia_move::cut || m_r == lia_move::branch) { int_solver * s = m_lar_solver->get_int_solver(); - m_lar_solver->adjust_cut_for_terms(*(s->m_t), *(s->m_k)); + // m_lar_solver->adjust_cut_for_terms(*(s->m_t), *(s->m_k)); } } }; @@ -373,21 +373,21 @@ lia_move int_solver::make_hnf_cut() { #else vector x0; #endif - lia_move r = m_hnf_cutter.create_cut(*m_t, *m_k, *m_ex, *m_upper, x0); + lia_move r = m_hnf_cutter.create_cut(m_t, m_k, m_ex, m_upper, x0); if (r == lia_move::cut) { TRACE("hnf_cut", - m_lar_solver->print_term(*m_t, tout << "cut:"); - tout << " <= " << *m_k << std::endl; + m_lar_solver->print_term(m_t, tout << "cut:"); + tout << " <= " << m_k << std::endl; for (unsigned i : m_hnf_cutter.constraints_for_explanation()) { m_lar_solver->print_constraint(i, tout); } ); lp_assert(current_solution_is_inf_on_cut()); settings().st().m_hnf_cuts++; - m_ex->clear(); + m_ex.clear(); for (unsigned i : m_hnf_cutter.constraints_for_explanation()) { - m_ex->push_justification(i); + m_ex.push_justification(i); } } return r; @@ -403,10 +403,13 @@ lia_move int_solver::hnf_cut() { return lia_move::undef; } -lia_move int_solver::check(lar_term& t, mpq& k, explanation& ex, bool & upper) { +lia_move int_solver::check() { if (!has_inf_int()) return lia_move::sat; - m_t = &t; m_k = &k; m_ex = &ex; m_upper = &upper; + m_t.clear(); + m_k.reset(); + m_ex.clear(); + m_upper = false; lia_move r = run_gcd_test(); if (r != lia_move::undef) return r; @@ -646,8 +649,8 @@ bool int_solver::gcd_test_for_row(static_matrix> & A, uns void int_solver::add_to_explanation_from_fixed_or_boxed_column(unsigned j) { constraint_index lc, uc; m_lar_solver->get_bound_constraint_witnesses_for_column(j, lc, uc); - m_ex->m_explanation.push_back(std::make_pair(mpq(1), lc)); - m_ex->m_explanation.push_back(std::make_pair(mpq(1), uc)); + m_ex.m_explanation.push_back(std::make_pair(mpq(1), lc)); + m_ex.m_explanation.push_back(std::make_pair(mpq(1), uc)); } void int_solver::fill_explanation_from_fixed_columns(const row_strip & row) { for (const auto & c : row) { @@ -1042,20 +1045,20 @@ const impq& int_solver::lower_bound(unsigned j) const { lia_move int_solver::create_branch_on_column(int j) { TRACE("check_main_int", tout << "branching" << std::endl;); - lp_assert(m_t->is_empty()); + lp_assert(m_t.is_empty()); lp_assert(j != -1); - m_t->add_monomial(mpq(1), m_lar_solver->adjust_column_index_to_term_index(j)); + m_t.add_monomial(mpq(1), m_lar_solver->adjust_column_index_to_term_index(j)); if (is_free(j)) { - *m_upper = true; - *m_k = mpq(0); + m_upper = true; + m_k = mpq(0); } else { - *m_upper = left_branch_is_more_narrow_than_right(j); - *m_k = *m_upper? floor(get_value(j)) : ceil(get_value(j)); + m_upper = left_branch_is_more_narrow_than_right(j); + m_k = m_upper? floor(get_value(j)) : ceil(get_value(j)); } TRACE("arith_int", tout << "branching v" << j << " = " << get_value(j) << "\n"; display_column(tout, j); - tout << "k = " << *m_k << std::endl; + tout << "k = " << m_k << std::endl; ); return lia_move::branch; diff --git a/src/util/lp/int_solver.h b/src/util/lp/int_solver.h index 013f53ce0..17ce20481 100644 --- a/src/util/lp/int_solver.h +++ b/src/util/lp/int_solver.h @@ -39,19 +39,23 @@ public: // fields lar_solver *m_lar_solver; unsigned m_number_of_calls; - lar_term *m_t; // the term to return in the cut - mpq *m_k; // the right side of the cut - explanation *m_ex; // the conflict explanation - bool *m_upper; // we have a cut m_t*x <= k if m_upper is true nad m_t*x >= k otherwise + lar_term m_t; // the term to return in the cut + mpq m_k; // the right side of the cut + explanation m_ex; // the conflict explanation + bool m_upper; // we have a cut m_t*x <= k if m_upper is true nad m_t*x >= k otherwise hnf_cutter m_hnf_cutter; // methods int_solver(lar_solver* lp); // main function to check that the solution provided by lar_solver is valid for integral values, // or provide a way of how it can be adjusted. - lia_move check(lar_term& t, mpq& k, explanation& ex, bool & upper); + lia_move check(); + lar_term const& get_term() const { return m_t; } + mpq const& get_offset() const { return m_k; } + explanation const& get_explanation() const { return m_ex; } + bool is_upper() const { return m_upper; } + bool move_non_basic_column_to_bounds(unsigned j); - lia_move check_wrapper(lar_term& t, mpq& k, explanation& ex); bool is_base(unsigned j) const; bool is_real(unsigned j) const; const impq & lower_bound(unsigned j) const; diff --git a/src/util/lp/lar_constraints.h b/src/util/lp/lar_constraints.h index ac15028bb..6305089b4 100644 --- a/src/util/lp/lar_constraints.h +++ b/src/util/lp/lar_constraints.h @@ -75,7 +75,7 @@ struct lar_term_constraint: public lar_base_constraint { } unsigned size() const override { return m_term->size();} lar_term_constraint(const lar_term *t, lconstraint_kind kind, const mpq& right_side) : lar_base_constraint(kind, right_side), m_term(t) { } - mpq get_free_coeff_of_left_side() const override { return m_term->m_v;} + // mpq get_free_coeff_of_left_side() const override { return m_term->m_v;} }; diff --git a/src/util/lp/lar_solver.cpp b/src/util/lp/lar_solver.cpp index a9bdf19d1..436e6ab04 100644 --- a/src/util/lp/lar_solver.cpp +++ b/src/util/lp/lar_solver.cpp @@ -137,7 +137,7 @@ bool lar_solver::implied_bound_is_correctly_explained(implied_bound const & be, kind = static_cast(-kind); } rs_of_evidence /= ratio; - rs_of_evidence += t->m_v * ratio; + // rs_of_evidence += t->m_v * ratio; } return kind == be.kind() && rs_of_evidence == be.m_bound; @@ -602,7 +602,7 @@ void lar_solver::register_monoid_in_map(std::unordered_map & coe void lar_solver::substitute_terms_in_linear_expression(const vector>& left_side_with_terms, - vector> &left_side, mpq & free_coeff) const { + vector> &left_side) const { std::unordered_map coeffs; for (auto & t : left_side_with_terms) { unsigned j = t.second; @@ -613,7 +613,6 @@ void lar_solver::substitute_terms_in_linear_expression(const vector & ci) { return false; } -column_type lar_solver::get_column_type(const column_info & ci) { - auto ret = ci.get_column_type_no_flipping(); - if (ret == column_type::boxed) { // changing boxed to fixed because of the no span - if (ci.get_lower_bound() == ci.get_upper_bound()) - ret = column_type::fixed; - } - return ret; +column_type lar_solver::get_column_type(unsigned j) const{ + return m_mpq_lar_core_solver.m_column_types[j]; } std::string lar_solver::get_column_name(unsigned j) const { @@ -955,9 +949,9 @@ bool lar_solver::constraint_holds(const lar_base_constraint & constr, std::unord mpq left_side_val = get_left_side_val(constr, var_map); switch (constr.m_kind) { case LE: return left_side_val <= constr.m_right_side; - case LT: return left_side_val < constr.m_right_side; + case LT: return left_side_val < constr.m_right_side; case GE: return left_side_val >= constr.m_right_side; - case GT: return left_side_val > constr.m_right_side; + case GT: return left_side_val > constr.m_right_side; case EQ: return left_side_val == constr.m_right_side; default: lp_unreachable(); @@ -976,8 +970,10 @@ bool lar_solver::the_relations_are_of_same_type(const vectorm_kind); if (kind == GT || kind == LT) strict = true; - if (kind == GE || kind == GT) n_of_G++; - else if (kind == LE || kind == LT) n_of_L++; + if (kind == GE || kind == GT) + n_of_G++; + else if (kind == LE || kind == LT) + n_of_L++; } the_kind_of_sum = n_of_G ? GE : (n_of_L ? LE : EQ); if (strict) @@ -1117,7 +1113,7 @@ bool lar_solver::has_upper_bound(var_index var, constraint_index& ci, mpq& value bool lar_solver::has_value(var_index var, mpq& value) const { if (is_term(var)) { lar_term const& t = get_term(var); - value = t.m_v; + value = 0; for (auto const& cv : t) { impq const& r = get_column_value(cv.var()); if (!numeric_traits::is_zero(r.y)) return false; @@ -1229,8 +1225,7 @@ std::ostream& lar_solver::print_constraints(std::ostream& out) const { std::ostream& lar_solver::print_terms(std::ostream& out) const { for (auto it : m_terms) { - print_term(*it, out); - out << "\n"; + print_term(*it, out) << "\n"; } return out; } @@ -1244,9 +1239,6 @@ std::ostream& lar_solver::print_left_side_of_constraint(const lar_base_constrain } std::ostream& lar_solver::print_term(lar_term const& term, std::ostream & out) const { - if (!numeric_traits::is_zero(term.m_v)) { - out << term.m_v << " + "; - } bool first = true; for (const auto p : term) { mpq val = p.coeff(); @@ -1270,9 +1262,6 @@ std::ostream& lar_solver::print_term(lar_term const& term, std::ostream & out) c } std::ostream& lar_solver::print_term_as_indices(lar_term const& term, std::ostream & out) const { - if (!numeric_traits::is_zero(term.m_v)) { - out << term.m_v << " + "; - } print_linear_combination_of_column_indices_only(term, out); return out; } @@ -1497,7 +1486,7 @@ bool lar_solver::term_is_int(const lar_term * t) const { for (auto const & p : t->m_coeffs) if (! (column_is_int(p.first) && p.second.is_int())) return false; - return t->m_v.is_int(); + return true; } bool lar_solver::var_is_int(var_index v) const { @@ -1598,17 +1587,13 @@ void lar_solver::add_new_var_to_core_fields_for_mpq(bool register_in_basis) { } -var_index lar_solver::add_term_undecided(const vector> & coeffs, - const mpq &m_v) { - push_and_register_term(new lar_term(coeffs, m_v)); +var_index lar_solver::add_term_undecided(const vector> & coeffs) { + push_and_register_term(new lar_term(coeffs)); return m_terms_start_index + m_terms.size() - 1; } #if Z3DEBUG_CHECK_UNIQUE_TERMS -bool lar_solver::term_coeffs_are_ok(const vector> & coeffs, const mpq& v) { - if (coeffs.empty()) { - return is_zero(v); - } +bool lar_solver::term_coeffs_are_ok(const vector> & coeffs) { for (const auto & p : coeffs) { if (column_is_real(p.second)) @@ -1643,12 +1628,11 @@ void lar_solver::push_and_register_term(lar_term* t) { } // terms -var_index lar_solver::add_term(const vector> & coeffs, - const mpq &m_v) { +var_index lar_solver::add_term(const vector> & coeffs) { if (strategy_is_undecided()) - return add_term_undecided(coeffs, m_v); + return add_term_undecided(coeffs); - push_and_register_term(new lar_term(coeffs, m_v)); + push_and_register_term(new lar_term(coeffs)); unsigned adjusted_term_index = m_terms.size() - 1; var_index ret = m_terms_start_index + adjusted_term_index; if (use_tableau() && !coeffs.empty()) { @@ -1656,13 +1640,12 @@ var_index lar_solver::add_term(const vector> & coeffs, if (m_settings.bound_propagation()) m_rows_with_changed_bounds.insert(A_r().row_count() - 1); } - CTRACE("add_term_lar_solver", !m_v.is_zero(), print_term(*m_terms.back(), tout);); lp_assert(m_var_register.size() == A_r().column_count()); return ret; } void lar_solver::add_row_from_term_no_constraint(const lar_term * term, unsigned term_ext_index) { - TRACE("dump_terms", print_term(*term, tout); tout << std::endl;); + TRACE("dump_terms", print_term(*term, tout) << std::endl;); register_new_ext_var_index(term_ext_index, term_is_int(term)); // j will be a new variable unsigned j = A_r().column_count(); @@ -1744,9 +1727,8 @@ void lar_solver::add_var_bound_on_constraint_for_term(var_index j, lconstraint_k // lp_assert(!term_is_int(m_terms[adjusted_term_index]) || right_side.is_int()); unsigned term_j; if (m_var_register.external_is_used(j, term_j)) { - mpq rs = right_side - m_terms[adjusted_term_index]->m_v; m_constraints.push_back(new lar_term_constraint(m_terms[adjusted_term_index], kind, right_side)); - update_column_type_and_bound(term_j, kind, rs, ci); + update_column_type_and_bound(term_j, kind, right_side, ci); } else { add_constraint_from_term_and_create_new_column_row(j, m_terms[adjusted_term_index], kind, right_side); @@ -1755,11 +1737,10 @@ void lar_solver::add_var_bound_on_constraint_for_term(var_index j, lconstraint_k constraint_index lar_solver::add_constraint(const vector>& left_side_with_terms, lconstraint_kind kind_par, const mpq& right_side_parm) { vector> left_side; - mpq rs = -right_side_parm; - substitute_terms_in_linear_expression(left_side_with_terms, left_side, rs); - unsigned term_index = add_term(left_side, zero_of_type()); + substitute_terms_in_linear_expression(left_side_with_terms, left_side); + unsigned term_index = add_term(left_side); constraint_index ci = m_constraints.size(); - add_var_bound_on_constraint_for_term(term_index, kind_par, -rs, ci); + add_var_bound_on_constraint_for_term(term_index, kind_par, right_side_parm, ci); return ci; } @@ -1768,7 +1749,7 @@ void lar_solver::add_constraint_from_term_and_create_new_column_row(unsigned ter add_row_from_term_no_constraint(term, term_j); unsigned j = A_r().column_count() - 1; - update_column_type_and_bound(j, kind, right_side - term->m_v, m_constraints.size()); + update_column_type_and_bound(j, kind, right_side, m_constraints.size()); m_constraints.push_back(new lar_term_constraint(term, kind, right_side)); lp_assert(A_r().column_count() == m_mpq_lar_core_solver.m_r_solver.m_costs.size()); } @@ -2266,15 +2247,6 @@ void lar_solver::set_cut_strategy(unsigned cut_frequency) { } } -void lar_solver::adjust_cut_for_terms(const lar_term& t, mpq & rs) { - for (const auto& p : t) { - if (!is_term(p.var())) continue; - const lar_term & p_term = get_term(p.var()); - if (p_term.m_v.is_zero()) continue; - rs -= p.coeff() * p_term.m_v; - } -} - } // namespace lp diff --git a/src/util/lp/lar_solver.h b/src/util/lp/lar_solver.h index 3c0ed4fbf..cfe581ba3 100644 --- a/src/util/lp/lar_solver.h +++ b/src/util/lp/lar_solver.h @@ -164,13 +164,11 @@ public: // terms - var_index add_term(const vector> & coeffs, - const mpq &m_v); + var_index add_term(const vector> & coeffs); - var_index add_term_undecided(const vector> & coeffs, - const mpq &m_v); + var_index add_term_undecided(const vector> & coeffs); - bool term_coeffs_are_ok(const vector> & coeffs, const mpq& v); + bool term_coeffs_are_ok(const vector> & coeffs); void push_and_register_term(lar_term* t); void add_row_for_term(const lar_term * term, unsigned term_ext_index); @@ -239,8 +237,7 @@ public: void analyze_new_bounds_on_row_tableau( unsigned row_index, - bound_propagator & bp - ); + bound_propagator & bp); void substitute_basis_var_in_terms_for_row(unsigned i); @@ -332,7 +329,7 @@ public: void substitute_terms_in_linear_expression( const vector>& left_side_with_terms, - vector> &left_side, mpq & free_coeff) const; + vector> &left_side) const; void detect_rows_of_bound_change_column_for_nbasic_column(unsigned j); @@ -398,7 +395,7 @@ public: bool try_to_set_fixed(column_info & ci); - column_type get_column_type(const column_info & ci); + column_type get_column_type(unsigned j) const; std::string get_column_name(unsigned j) const; @@ -535,7 +532,7 @@ public: return m_columns_to_ul_pairs()[j].lower_bound_witness(); } - void subs_term_columns(lar_term& t, mpq & rs) { + void subs_term_columns(lar_term& t) { vector> columns_to_subs; for (const auto & m : t.m_coeffs) { unsigned tj = adjust_column_index_to_term_index(m.first); @@ -549,8 +546,6 @@ public: mpq v = it->second; t.m_coeffs.erase(it); t.m_coeffs[p.second] = v; - if (lt.m_v.is_zero()) continue; - rs -= v * lt.m_v; } } @@ -587,6 +582,5 @@ public: lar_term get_term_to_maximize(unsigned ext_j) const; void set_cut_strategy(unsigned cut_frequency); bool sum_first_coords(const lar_term& t, mpq & val) const; - void adjust_cut_for_terms(const lar_term& t, mpq & rs); }; } diff --git a/src/util/lp/lar_term.h b/src/util/lp/lar_term.h index 519847848..e9259b8c0 100644 --- a/src/util/lp/lar_term.h +++ b/src/util/lp/lar_term.h @@ -21,9 +21,9 @@ #include "util/lp/indexed_vector.h" namespace lp { struct lar_term { - // the term evaluates to sum of m_coeffs + m_v + // the term evaluates to sum of m_coeffs std::unordered_map m_coeffs; - mpq m_v; + // mpq m_v; lar_term() {} void add_monomial(const mpq& c, unsigned j) { auto it = m_coeffs.find(j); @@ -37,7 +37,7 @@ struct lar_term { } bool is_empty() const { - return m_coeffs.size() == 0 && is_zero(m_v); + return m_coeffs.size() == 0; // && is_zero(m_v); } unsigned size() const { return static_cast(m_coeffs.size()); } @@ -46,8 +46,7 @@ struct lar_term { return m_coeffs; } - lar_term(const vector>& coeffs, - const mpq & v) : m_v(v) { + lar_term(const vector>& coeffs) { for (const auto & p : coeffs) { add_monomial(p.first, p.second); } @@ -87,7 +86,7 @@ struct lar_term { template T apply(const vector& x) const { - T ret = T(m_v); + T ret(0); for (const auto & t : m_coeffs) { ret += t.second * x[t.first]; } @@ -96,7 +95,6 @@ struct lar_term { void clear() { m_coeffs.clear(); - m_v = zero_of_type(); } struct ival { diff --git a/src/util/lp/lp_core_solver_base.h b/src/util/lp/lp_core_solver_base.h index 41b6fe31d..9a6549917 100644 --- a/src/util/lp/lp_core_solver_base.h +++ b/src/util/lp/lp_core_solver_base.h @@ -577,7 +577,7 @@ public: } void print_column_info(unsigned j, std::ostream & out) const { - out << "j = " << j << ", name = "<< column_name(j); + out << "j = " << j << ",\tname = "<< column_name(j) << "\t"; switch (m_column_types[j]) { case column_type::fixed: case column_type::boxed: @@ -596,11 +596,11 @@ public: lp_assert(false); } // out << "basis heading = " << m_basis_heading[j] << std::endl; - out << " x = " << m_x[j]; + out << "\tx = " << m_x[j]; if (m_basis_heading[j] >= 0) out << " base\n"; else - out << " nbas\n"; + out << " \n"; } bool column_is_free(unsigned j) const { return this->m_column_type[j] == free; } diff --git a/src/util/lp/lp_primal_core_solver_def.h b/src/util/lp/lp_primal_core_solver_def.h index 1e9edbd31..872922f60 100644 --- a/src/util/lp/lp_primal_core_solver_def.h +++ b/src/util/lp/lp_primal_core_solver_def.h @@ -1238,6 +1238,7 @@ template void lp_primal_core_solver::print_column break; case column_type::free_column: out << "( _" << this->m_x[j] << "_)" << std::endl; + break; default: lp_unreachable(); } diff --git a/src/util/lp/lp_solver_def.h b/src/util/lp/lp_solver_def.h index 10c7a6feb..9b385dee6 100644 --- a/src/util/lp/lp_solver_def.h +++ b/src/util/lp/lp_solver_def.h @@ -24,7 +24,7 @@ Revision History: namespace lp { template column_info * lp_solver::get_or_create_column_info(unsigned column) { auto it = m_map_from_var_index_to_column_info.find(column); - return (it == m_map_from_var_index_to_column_info.end())? (m_map_from_var_index_to_column_info[column] = new column_info(static_cast(-1))) : it->second; + return (it == m_map_from_var_index_to_column_info.end())? (m_map_from_var_index_to_column_info[column] = new column_info()) : it->second; } template diff --git a/src/util/version.h.cmake.in b/src/util/z3_version.h.cmake.in similarity index 100% rename from src/util/version.h.cmake.in rename to src/util/z3_version.h.cmake.in diff --git a/src/util/version.h.in b/src/util/z3_version.h.in similarity index 100% rename from src/util/version.h.in rename to src/util/z3_version.h.in