mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-13 20:38:43 +00:00
Code Activity

Merge branch 'master' of https://github.com/Z3Prover/z3

Browse source
This commit is contained in:
Lev Nachmanson 2018-09-25 13:34:23 -07:00
parent 0b2b6b1306 af41255a9d
commit e68deab443
36 changed files with 443 additions and 317 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
scripts/mk_project.py
View file

@ -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'])

4
scripts/mk_util.py
View file

@ -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

2
src/CMakeLists.txt
View file

@ -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

2
src/api/api_context.cpp
View file

@ -19,7 +19,7 @@ Revision History:
--*/
#include<typeinfo>
#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"

2
src/api/api_log.cpp
View file

@ -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;

15
src/api/api_solver.cpp
View file

@ -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]))) {

2
src/api/c++/z3++.h
View file

@ -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);

12
src/api/ml/z3.ml
View file

@ -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

16
src/api/python/z3/z3.py
View file

@ -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()`.

8
src/api/z3_api.h
View file

@ -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.

2
src/cmd_context/basic_cmds.cpp
View file

@ -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"

2
src/sat/sat_lookahead.cpp
View file

@ -16,6 +16,8 @@ Author:
Notes:
--*/
#include <cmath>

28
src/sat/sat_params.pyg
View file

@ -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.
)

3
src/sat/sat_solver/inc_sat_solver.cpp
View file

@ -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();
}

2
src/shell/main.cpp
View file

@ -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"

2
src/smt/smt_arith_value.cpp
View file

@ -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"

144
src/smt/theory_lra.cpp
View file

@ -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<rational> m_coeffs;
svector<theory_var> m_vars;
rational m_coeff;
rational m_offset;
ptr_vector<expr> 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<rational>& coeffs() { return m_st.m_coeffs; }
svector<theory_var>& vars() { return m_st.m_vars; }
rational& coeff() { return m_st.m_coeff; }
rational& offset() { return m_st.m_offset; }
ptr_vector<expr>& 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<theory_var> 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<lp::var_index, rational> 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<theory_var>& vars = st.vars();
vector<rational>& 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<rational> const& coeffs, rational const& offset, bool is_int) {

50
src/solver/solver.cpp
View file

@ -178,10 +178,19 @@ lbool solver::preferred_sat(expr_ref_vector const& asms, vector<expr_ref_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;
}

2
src/solver/solver.h
View file

@ -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;

1
src/test/lp/gomory_test.h
View file

@ -185,7 +185,6 @@ struct gomory_test {
}
void print_term(lar_term & t, std::ostream & out) {
lp_assert(is_zero(t.m_v));
vector<std::pair<mpq, unsigned>> row;
for (auto p : t.m_coeffs)
row.push_back(std::make_pair(p.second, p.first));

20
src/test/lp/lp.cpp
View file

@ -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<std::pair<mpq, var_index>> term_one;
term_one.push_back(std::make_pair((int)1, one));
solver.add_constraint(term_one, lconstraint_kind::EQ, mpq(0));
vector<std::pair<mpq, var_index>> term_ls;
term_ls.push_back(std::pair<mpq, var_index>((int)1, x));
term_ls.push_back(std::pair<mpq, var_index>((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<std::pair<mpq, var_index>> ls;
ls.push_back(std::pair<mpq, var_index>((int)1, x));
@ -2743,10 +2750,10 @@ void test_bound_propagation_one_small_sample1() {
vector<std::pair<mpq, var_index>> coeffs;
coeffs.push_back(std::pair<mpq, var_index>(1, a));
coeffs.push_back(std::pair<mpq, var_index>(-1, c));
ls.add_term(coeffs, zero_of_type<mpq>());
ls.add_term(coeffs);
coeffs.pop_back();
coeffs.push_back(std::pair<mpq, var_index>(-1, b));
ls.add_term(coeffs, zero_of_type<mpq>());
ls.add_term(coeffs);
coeffs.clear();
coeffs.push_back(std::pair<mpq, var_index>(1, a));
coeffs.push_back(std::pair<mpq, var_index>(-1, b));
@ -3485,12 +3492,12 @@ void test_maximize_term() {
vector<std::pair<mpq, var_index>> term_ls;
term_ls.push_back(std::pair<mpq, var_index>((int)1, x));
term_ls.push_back(std::pair<mpq, var_index>((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<mpq, var_index>((int)2, x));
term_ls.push_back(std::pair<mpq, var_index>((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<mpq>());
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);

7
src/util/CMakeLists.txt
View file

@ -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

4
src/util/lp/bound_propagator.cpp
View file

@ -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)

10
src/util/lp/column_info.h
View file

@ -69,16 +69,6 @@ public:
m_column_index(static_cast<unsigned>(-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<T>::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;

228
src/util/lp/gomory.cpp
View file

@ -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<mpq>& 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<mpq>())
out << a;
else {
out << "( - " << - a << ") ";
}
} else {
if ( a >= zero_of_type<mpq>())
out << "(div " << numerator(a) << " " << denominator(a) << ")";
else {
out << "(- ( div " << numerator(-a) << " " << denominator(-a) << "))";
}
out << a;
}
else if ( a >= zero_of_type<mpq>())
out << "(/ " << numerator(a) << " " << denominator(a) << ")";
else {
out << "(- ( / " << numerator(-a) << " " << denominator(-a) << "))";
}
return out;
}
template <typename T>
@ -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<mpq>());
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<mpq>& 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) {}
};

53
src/util/lp/int_solver.cpp
View file

@ -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<mpq>() : -one_of_type<mpq>();
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<mpq>() : -one_of_type<mpq>();
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<mpq> & 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<mpq> 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<mpq, numeric_pair<mpq>> & 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<mpq> & 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;

16
src/util/lp/int_solver.h
View file

@ -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;

2
src/util/lp/lar_constraints.h
View file

@ -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;}
};

78
src/util/lp/lar_solver.cpp
View file

@ -137,7 +137,7 @@ bool lar_solver::implied_bound_is_correctly_explained(implied_bound const & be,
kind = static_cast<lconstraint_kind>(-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<var_index, mpq> & coe
void lar_solver::substitute_terms_in_linear_expression(const vector<std::pair<mpq, var_index>>& left_side_with_terms,
vector<std::pair<mpq, var_index>> &left_side, mpq & free_coeff) const {
vector<std::pair<mpq, var_index>> &left_side) const {
std::unordered_map<var_index, mpq> 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<std::pair<mp
for (auto & p : term.coeffs()){
register_monoid_in_map(coeffs, t.first * p.second , p.first);
}
free_coeff += t.first * term.m_v;
}
}
@ -910,13 +909,8 @@ bool lar_solver::try_to_set_fixed(column_info<mpq> & ci) {
return false;
}
column_type lar_solver::get_column_type(const column_info<mpq> & 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 vector<std::pair<mpq, unsi
flip_kind(m_constraints[con_ind]->m_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<mpq>::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<mpq>::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<mpq>::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<std::pair<mpq, var_index>> & coeffs,
const mpq &m_v) {
push_and_register_term(new lar_term(coeffs, m_v));
var_index lar_solver::add_term_undecided(const vector<std::pair<mpq, var_index>> & 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<std::pair<mpq, var_index>> & coeffs, const mpq& v) {
if (coeffs.empty()) {
return is_zero(v);
}
bool lar_solver::term_coeffs_are_ok(const vector<std::pair<mpq, var_index>> & 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<std::pair<mpq, var_index>> & coeffs,
const mpq &m_v) {
var_index lar_solver::add_term(const vector<std::pair<mpq, var_index>> & 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<std::pair<mpq, var_index>> & 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<std::pair<mpq, var_index>>& left_side_with_terms, lconstraint_kind kind_par, const mpq& right_side_parm) {
vector<std::pair<mpq, var_index>> 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<mpq>());
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

20
src/util/lp/lar_solver.h
View file

@ -164,13 +164,11 @@ public:
// terms
var_index add_term(const vector<std::pair<mpq, var_index>> & coeffs,
const mpq &m_v);
var_index add_term(const vector<std::pair<mpq, var_index>> & coeffs);
var_index add_term_undecided(const vector<std::pair<mpq, var_index>> & coeffs,
const mpq &m_v);
var_index add_term_undecided(const vector<std::pair<mpq, var_index>> & coeffs);
bool term_coeffs_are_ok(const vector<std::pair<mpq, var_index>> & coeffs, const mpq& v);
bool term_coeffs_are_ok(const vector<std::pair<mpq, var_index>> & 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<std::pair<mpq, var_index>>& left_side_with_terms,
vector<std::pair<mpq, var_index>> &left_side, mpq & free_coeff) const;
vector<std::pair<mpq, var_index>> &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<mpq> & ci);
column_type get_column_type(const column_info<mpq> & 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<std::pair<unsigned,unsigned>> 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);
};
}

12
src/util/lp/lar_term.h
View file

@ -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<unsigned, mpq> 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<unsigned>(m_coeffs.size()); }
@ -46,8 +46,7 @@ struct lar_term {
return m_coeffs;
}
lar_term(const vector<std::pair<mpq, unsigned>>& coeffs,
const mpq & v) : m_v(v) {
lar_term(const vector<std::pair<mpq, unsigned>>& coeffs) {
for (const auto & p : coeffs) {
add_monomial(p.first, p.second);
}
@ -87,7 +86,7 @@ struct lar_term {
template <typename T>
T apply(const vector<T>& 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<mpq>();
}
struct ival {

6
src/util/lp/lp_core_solver_base.h
View file

@ -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; }

1
src/util/lp/lp_primal_core_solver_def.h
View file

@ -1238,6 +1238,7 @@ template <typename T, typename X> void lp_primal_core_solver<T, X>::print_column
break;
case column_type::free_column:
out << "( _" << this->m_x[j] << "_)" << std::endl;
break;
default:
lp_unreachable();
}

2
src/util/lp/lp_solver_def.h
View file

@ -24,7 +24,7 @@ Revision History:
namespace lp {
template <typename T, typename X> column_info<T> * lp_solver<T, X>::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<T>(static_cast<unsigned>(-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<T>()) : it->second;
}
template <typename T, typename X>

0
src/util/version.h.cmake.in → src/util/z3_version.h.cmake.in
View file

0
src/util/version.h.in → src/util/z3_version.h.in
View file