mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-05 10:50:24 +00:00
Code Activity

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

Browse source
This commit is contained in:
Nikolaj Bjorner 2018-12-03 08:45:28 -08:00
commit 226497e530
19 changed files with 48 additions and 862 deletions
Download patch file Download diff file Expand all files Collapse all files

9
CMakeLists.txt
View file

@ -425,6 +425,15 @@ list(APPEND Z3_DEPENDENT_LIBS ${CMAKE_THREAD_LIBS_INIT})
################################################################################ ################################################################################
include(${CMAKE_SOURCE_DIR}/cmake/compiler_warnings.cmake) include(${CMAKE_SOURCE_DIR}/cmake/compiler_warnings.cmake)
################################################################################
# Save Clang optimization records
################################################################################
option(SAVE_CLANG_OPTIMIZATION_RECORDS "Enable saving Clang optimization records." OFF)
if (SAVE_CLANG_OPTIMIZATION_RECORDS)
z3_add_cxx_flag("-fsave-optimization-record" REQUIRED)
endif()
################################################################################ ################################################################################
# If using Ninja, force color output for Clang (and gcc, disabled to check build). # If using Ninja, force color output for Clang (and gcc, disabled to check build).
################################################################################ ################################################################################

2
scripts/mk_genfile_common.py
View file

@ -719,7 +719,7 @@ def mk_install_tactic_cpp_internal(h_files_full_path, path):
fullname, line)) fullname, line))
raise e raise e
except Exception as e: except Exception as e:
_loggeer.error("Failed to read file {}\n".format(h_file)) _logger.error("Failed to read file {}\n".format(h_file))
raise e raise e
# First pass will just generate the tactic factories # First pass will just generate the tactic factories
fout.write('#define ADD_TACTIC_CMD(NAME, DESCR, CODE) ctx.insert(alloc(tactic_cmd, symbol(NAME), DESCR, [](ast_manager &m, const params_ref &p) { return CODE; }))\n') fout.write('#define ADD_TACTIC_CMD(NAME, DESCR, CODE) ctx.insert(alloc(tactic_cmd, symbol(NAME), DESCR, [](ast_manager &m, const params_ref &p) { return CODE; }))\n')

2
src/ast/datatype_decl_plugin.cpp
View file

@ -682,7 +682,7 @@ namespace datatype {
/** /**
\brief Return true if the inductive datatype is well-founded. \brief Return true if the inductive datatype is well-founded.
Pre-condition: The given argument constains the parameters of an inductive datatype. Pre-condition: The given argument constrains the parameters of an inductive datatype.
*/ */
bool util::is_well_founded(unsigned num_types, sort* const* sorts) { bool util::is_well_founded(unsigned num_types, sort* const* sorts) {
buffer<bool> well_founded(num_types, false); buffer<bool> well_founded(num_types, false);

6
src/math/polynomial/upolynomial.cpp
View file

@ -1339,12 +1339,10 @@ namespace upolynomial {
// Return the number of sign changes in the coefficients of p // Return the number of sign changes in the coefficients of p
unsigned manager::sign_changes(unsigned sz, numeral const * p) { unsigned manager::sign_changes(unsigned sz, numeral const * p) {
unsigned r = 0; unsigned r = 0;
int sign, prev_sign; int prev_sign = 0;
sign = 0;
prev_sign = 0;
unsigned i = 0; unsigned i = 0;
for (; i < sz; i++) { for (; i < sz; i++) {
sign = sign_of(p[i]); int sign = sign_of(p[i]);
if (sign == 0) if (sign == 0)
continue; continue;
if (sign != prev_sign && prev_sign != 0) if (sign != prev_sign && prev_sign != 0)

10
src/math/realclosure/realclosure.cpp
View file

@ -154,7 +154,7 @@ namespace realclosure {
struct value { struct value {
unsigned m_ref_count; //!< Reference counter unsigned m_ref_count; //!< Reference counter
bool m_rational; //!< True if the value is represented as an abitrary precision rational value. bool m_rational; //!< True if the value is represented as an arbitrary precision rational value.
mpbqi m_interval; //!< approximation as an interval with binary rational end-points mpbqi m_interval; //!< approximation as an interval with binary rational end-points
// When performing an operation OP, we may have to make the width (upper - lower) of m_interval very small. // When performing an operation OP, we may have to make the width (upper - lower) of m_interval very small.
// The precision (i.e., a small interval) needed for executing OP is usually unnecessary for subsequent operations, // The precision (i.e., a small interval) needed for executing OP is usually unnecessary for subsequent operations,
@ -283,7 +283,7 @@ namespace realclosure {
struct algebraic : public extension { struct algebraic : public extension {
polynomial m_p; polynomial m_p;
mpbqi m_iso_interval; mpbqi m_iso_interval;
sign_det * m_sign_det; //!< != 0 if m_iso_interval constains more than one root of m_p. sign_det * m_sign_det; //!< != 0 if m_iso_interval constrains more than one root of m_p.
unsigned m_sc_idx; //!< != UINT_MAX if m_sign_det != 0, in this case m_sc_idx < m_sign_det->m_sign_conditions.size() unsigned m_sc_idx; //!< != UINT_MAX if m_sign_det != 0, in this case m_sc_idx < m_sign_det->m_sign_conditions.size()
bool m_depends_on_infinitesimals; //!< True if the polynomial p depends on infinitesimal extensions. bool m_depends_on_infinitesimals; //!< True if the polynomial p depends on infinitesimal extensions.
@ -1741,7 +1741,7 @@ namespace realclosure {
\brief In the sign determination algorithm main loop, we keep processing polynomials q, \brief In the sign determination algorithm main loop, we keep processing polynomials q,
and checking whether they discriminate the roots of the target polynomial. and checking whether they discriminate the roots of the target polynomial.
The vectors sc_cardinalities contains the cardinalites of the new realizable sign conditions. The vectors sc_cardinalities contains the cardinalities of the new realizable sign conditions.
That is, we started we a sequence of sign conditions That is, we started we a sequence of sign conditions
sc_1, ..., sc_n, sc_1, ..., sc_n,
If q2_used is true, then we expanded this sequence as If q2_used is true, then we expanded this sequence as
@ -1750,7 +1750,7 @@ namespace realclosure {
Thus, q is useful (i.e., it is a discriminator for the roots of p) IF Thus, q is useful (i.e., it is a discriminator for the roots of p) IF
If !q2_used, then There is an i s.t. sc_cardinalities[2*i] > 0 && sc_cardinalities[2*i] > 0 If !q2_used, then There is an i s.t. sc_cardinalities[2*i] > 0 && sc_cardinalities[2*i] > 0
If q2_used, then There is an i s.t. AtLeatTwo(sc_cardinalities[3*i] > 0, sc_cardinalities[3*i+1] > 0, sc_cardinalities[3*i+2] > 0) If q2_used, then There is an i s.t. AtLeastTwo(sc_cardinalities[3*i] > 0, sc_cardinalities[3*i+1] > 0, sc_cardinalities[3*i+2] > 0)
*/ */
bool keep_new_sc_assignment(unsigned sz, int const * sc_cardinalities, bool q2_used) { bool keep_new_sc_assignment(unsigned sz, int const * sc_cardinalities, bool q2_used) {
SASSERT(q2_used || sz % 2 == 0); SASSERT(q2_used || sz % 2 == 0);
@ -2038,7 +2038,7 @@ namespace realclosure {
// We should keep q only if it discriminated something. // We should keep q only if it discriminated something.
// That is, // That is,
// If !use_q2, then There is an i s.t. sc_cardinalities[2*i] > 0 && sc_cardinalities[2*i] > 0 // If !use_q2, then There is an i s.t. sc_cardinalities[2*i] > 0 && sc_cardinalities[2*i] > 0
// If use_q2, then There is an i s.t. AtLeatTwo(sc_cardinalities[3*i] > 0, sc_cardinalities[3*i+1] > 0, sc_cardinalities[3*i+2] > 0) // If use_q2, then There is an i s.t. AtLeastTwo(sc_cardinalities[3*i] > 0, sc_cardinalities[3*i+1] > 0, sc_cardinalities[3*i+2] > 0)
if (!keep_new_sc_assignment(sc_cardinalities.size(), sc_cardinalities.c_ptr(), use_q2)) { if (!keep_new_sc_assignment(sc_cardinalities.size(), sc_cardinalities.c_ptr(), use_q2)) {
// skip q since it did not reduced the cardinality of the existing sign conditions. // skip q since it did not reduced the cardinality of the existing sign conditions.
continue; continue;

2
src/sat/tactic/sat_tactic.cpp
View file

@ -105,7 +105,7 @@ class sat_tactic : public tactic {
else { else {
// get simplified problem. // get simplified problem.
#if 0 #if 0
IF_VERBOSE(TACTIC_VERBOSITY_LVL, verbose_stream() << "\"formula constains interpreted atoms, recovering formula from sat solver...\"\n";); IF_VERBOSE(TACTIC_VERBOSITY_LVL, verbose_stream() << "\"formula constrains interpreted atoms, recovering formula from sat solver...\"\n";);
#endif #endif
m_solver.pop_to_base_level(); m_solver.pop_to_base_level();
ref<sat2goal::mc> mc; ref<sat2goal::mc> mc;

2
src/smt/smt_setup.cpp
View file

@ -209,7 +209,7 @@ namespace smt {
static void check_no_arithmetic(static_features const & st, char const * logic) { static void check_no_arithmetic(static_features const & st, char const * logic) {
if (st.m_num_arith_ineqs > 0 || st.m_num_arith_terms > 0 || st.m_num_arith_eqs > 0) if (st.m_num_arith_ineqs > 0 || st.m_num_arith_terms > 0 || st.m_num_arith_eqs > 0)
throw default_exception("Benchmark constains arithmetic, but specified logic does not support it."); throw default_exception("Benchmark constrains arithmetic, but specified logic does not support it.");
} }
void setup::setup_QF_UF() { void setup::setup_QF_UF() {

1
src/smt/theory_bv.cpp
View file

@ -1084,7 +1084,6 @@ namespace smt {
for (unsigned i = 0; i <= num_args; i++) { for (unsigned i = 0; i <= num_args; i++) {
expr* arg = (i == num_args)?n:n->get_arg(i); expr* arg = (i == num_args)?n:n->get_arg(i);
sort* s = get_manager().get_sort(arg); sort* s = get_manager().get_sort(arg);
s = get_manager().get_sort(arg);
if (m_util.is_bv_sort(s) && m_util.get_bv_size(arg) > m_params.m_bv_blast_max_size) { if (m_util.is_bv_sort(s) && m_util.get_bv_size(arg) > m_params.m_bv_blast_max_size) {
if (!m_approximates_large_bvs) { if (!m_approximates_large_bvs) {
TRACE("bv", tout << "found large size bit-vector:\n" << mk_pp(n, get_manager()) << "\n";); TRACE("bv", tout << "found large size bit-vector:\n" << mk_pp(n, get_manager()) << "\n";);

10
src/smt/theory_lra.cpp
View file

@ -2283,16 +2283,14 @@ public:
iterator lo_inf = begin1, lo_sup = begin1; iterator lo_inf = begin1, lo_sup = begin1;
iterator hi_inf = begin2, hi_sup = begin2; iterator hi_inf = begin2, hi_sup = begin2;
iterator lo_inf1 = begin1, lo_sup1 = begin1;
iterator hi_inf1 = begin2, hi_sup1 = begin2;
bool flo_inf, fhi_inf, flo_sup, fhi_sup; bool flo_inf, fhi_inf, flo_sup, fhi_sup;
ptr_addr_hashtable<lp_api::bound> visited; ptr_addr_hashtable<lp_api::bound> visited;
for (unsigned i = 0; i < atoms.size(); ++i) { for (unsigned i = 0; i < atoms.size(); ++i) {
lp_api::bound* a1 = atoms[i]; lp_api::bound* a1 = atoms[i];
lo_inf1 = next_inf(a1, lp_api::lower_t, lo_inf, end, flo_inf); iterator lo_inf1 = next_inf(a1, lp_api::lower_t, lo_inf, end, flo_inf);
hi_inf1 = next_inf(a1, lp_api::upper_t, hi_inf, end, fhi_inf); iterator hi_inf1 = next_inf(a1, lp_api::upper_t, hi_inf, end, fhi_inf);
lo_sup1 = next_sup(a1, lp_api::lower_t, lo_sup, end, flo_sup); iterator lo_sup1 = next_sup(a1, lp_api::lower_t, lo_sup, end, flo_sup);
hi_sup1 = next_sup(a1, lp_api::upper_t, hi_sup, end, fhi_sup); iterator hi_sup1 = next_sup(a1, lp_api::upper_t, hi_sup, end, fhi_sup);
if (lo_inf1 != end) lo_inf = lo_inf1; if (lo_inf1 != end) lo_inf = lo_inf1;
if (lo_sup1 != end) lo_sup = lo_sup1; if (lo_sup1 != end) lo_sup = lo_sup1;
if (hi_inf1 != end) hi_inf = hi_inf1; if (hi_inf1 != end) hi_inf = hi_inf1;

29
src/smt/theory_str.cpp
View file

@ -7501,15 +7501,12 @@ namespace smt {
expr_ref newConcat(m); expr_ref newConcat(m);
if (arg1 != a1 || arg2 != a2) { if (arg1 != a1 || arg2 != a2) {
TRACE("str", tout << "resolved concat argument(s) to eqc string constants" << std::endl;); TRACE("str", tout << "resolved concat argument(s) to eqc string constants" << std::endl;);
int iPos = 0;
expr_ref_vector item1(m); expr_ref_vector item1(m);
if (a1 != arg1) { if (a1 != arg1) {
item1.push_back(ctx.mk_eq_atom(a1, arg1)); item1.push_back(ctx.mk_eq_atom(a1, arg1));
iPos += 1;
} }
if (a2 != arg2) { if (a2 != arg2) {
item1.push_back(ctx.mk_eq_atom(a2, arg2)); item1.push_back(ctx.mk_eq_atom(a2, arg2));
iPos += 1;
} }
expr_ref implyL1(mk_and(item1), m); expr_ref implyL1(mk_and(item1), m);
newConcat = mk_concat(arg1, arg2); newConcat = mk_concat(arg1, arg2);
@ -9424,15 +9421,15 @@ namespace smt {
if (lrConstrainedMap.find(var) == lrConstrainedMap.end()) { if (lrConstrainedMap.find(var) == lrConstrainedMap.end()) {
freeVarMap[var] = 1; freeVarMap[var] = 1;
} else { } else {
int lrConstainted = 0; int lrConstrained = 0;
std::map<expr*, int>::iterator lrit = freeVarMap.begin(); std::map<expr*, int>::iterator lrit = freeVarMap.begin();
for (; lrit != freeVarMap.end(); lrit++) { for (; lrit != freeVarMap.end(); lrit++) {
if (lrConstrainedMap[var].find(lrit->first) != lrConstrainedMap[var].end()) { if (lrConstrainedMap[var].find(lrit->first) != lrConstrainedMap[var].end()) {
lrConstainted = 1; lrConstrained = 1;
break; break;
} }
} }
if (lrConstainted == 0) { if (lrConstrained == 0) {
freeVarMap[var] = 1; freeVarMap[var] = 1;
} }
} }
@ -9451,15 +9448,15 @@ namespace smt {
if (lrConstrainedMap.find(var) == lrConstrainedMap.end()) { if (lrConstrainedMap.find(var) == lrConstrainedMap.end()) {
freeVarMap[var] = 1; freeVarMap[var] = 1;
} else { } else {
int lrConstainted = 0; int lrConstrained = 0;
std::map<expr*, int>::iterator lrit = freeVarMap.begin(); std::map<expr*, int>::iterator lrit = freeVarMap.begin();
for (; lrit != freeVarMap.end(); lrit++) { for (; lrit != freeVarMap.end(); lrit++) {
if (lrConstrainedMap[var].find(lrit->first) != lrConstrainedMap[var].end()) { if (lrConstrainedMap[var].find(lrit->first) != lrConstrainedMap[var].end()) {
lrConstainted = 1; lrConstrained = 1;
break; break;
} }
} }
if (lrConstainted == 0) { if (lrConstrained == 0) {
freeVarMap[var] = 1; freeVarMap[var] = 1;
} }
} }
@ -9471,15 +9468,15 @@ namespace smt {
if (lrConstrainedMap.find(var) == lrConstrainedMap.end()) { if (lrConstrainedMap.find(var) == lrConstrainedMap.end()) {
freeVarMap[var] = 1; freeVarMap[var] = 1;
} else { } else {
int lrConstainted = 0; int lrConstrained = 0;
std::map<expr*, int>::iterator lrit = freeVarMap.begin(); std::map<expr*, int>::iterator lrit = freeVarMap.begin();
for (; lrit != freeVarMap.end(); lrit++) { for (; lrit != freeVarMap.end(); lrit++) {
if (lrConstrainedMap[var].find(lrit->first) != lrConstrainedMap[var].end()) { if (lrConstrainedMap[var].find(lrit->first) != lrConstrainedMap[var].end()) {
lrConstainted = 1; lrConstrained = 1;
break; break;
} }
} }
if (lrConstainted == 0) { if (lrConstrained == 0) {
freeVarMap[var] = 1; freeVarMap[var] = 1;
} }
} }
@ -9500,15 +9497,15 @@ namespace smt {
if (lrConstrainedMap.find(var) == lrConstrainedMap.end()) { if (lrConstrainedMap.find(var) == lrConstrainedMap.end()) {
freeVarMap[var] = 1; freeVarMap[var] = 1;
} else { } else {
int lrConstainted = 0; int lrConstrained = 0;
std::map<expr*, int>::iterator lrit = freeVarMap.begin(); std::map<expr*, int>::iterator lrit = freeVarMap.begin();
for (; lrit != freeVarMap.end(); lrit++) { for (; lrit != freeVarMap.end(); lrit++) {
if (lrConstrainedMap[var].find(lrit->first) != lrConstrainedMap[var].end()) { if (lrConstrainedMap[var].find(lrit->first) != lrConstrainedMap[var].end()) {
lrConstainted = 1; lrConstrained = 1;
break; break;
} }
} }
if (lrConstainted == 0) { if (lrConstrained == 0) {
freeVarMap[var] = 1; freeVarMap[var] = 1;
} }
} }
@ -9762,7 +9759,7 @@ namespace smt {
expr_ref concatlenExpr (mk_strlen(concat), m) ; expr_ref concatlenExpr (mk_strlen(concat), m) ;
bool allLeafResolved = true; bool allLeafResolved = true;
if (! get_arith_value(concatlenExpr, lenValue)) { if (! get_arith_value(concatlenExpr, lenValue)) {
// the length fo concat is unresolved yet // the length of concat is unresolved yet
if (get_len_value(concat, lenValue)) { if (get_len_value(concat, lenValue)) {
// but all leaf nodes have length information // but all leaf nodes have length information
TRACE("str", tout << "* length pop-up: " << mk_ismt2_pp(concat, m) << "| = " << lenValue << std::endl;); TRACE("str", tout << "* length pop-up: " << mk_ismt2_pp(concat, m) << "| = " << lenValue << std::endl;);

799
src/tactic/nlsat_smt/nl_purify_tactic.cpp
View file

@ -1,799 +0,0 @@
/*++
Copyright (c) 2015 Microsoft Corporation
Module Name:
nl_purify_tactic.cpp
Abstract:
Tactic for purifying quantifier-free formulas that mix QF_NRA and other theories.
It is designed to allow cooperation between the nlsat solver and other theories
in a decoupled way.
Let goal be formula F.
Let NL goal be formula G.
Assume F is in NNF.
Assume F does not contain mix of real/integers.
Assume F is quantifier-free (please, otherwise we need to reprocess from instantiated satisfiable formula)
For each atomic nl formula f,
- introduce a propositional variable p
- replace f by p
- add clauses p => f to G
For each interface term t,
- introduce interface variable v (or use t if it is already a variable)
- replace t by v
Check satisfiability of G.
If satisfiable, then check assignment to p and interface equalities on F
If unsat:
Retrieve core and add core to G.
else:
For interface equalities from model of F that are not equal in G, add
For interface variables that are equal under one model, but not the other model,
create interface predicate p_vw => v = w, add to both F, G.
Add interface equations to assumptions, recheck F.
If unsat retrieve core add to G.
Author:
Nikolaj Bjorner (nbjorner) 2015-5-5.
Revision History:
--*/
#include "tactic/tactical.h"
#include "tactic/nlsat_smt/nl_purify_tactic.h"
#include "smt/tactic/smt_tactic.h"
#include "ast/rewriter/rewriter.h"
#include "nlsat/tactic/nlsat_tactic.h"
#include "tactic/filter_model_converter.h"
#include "util/obj_pair_hashtable.h"
#include "ast/rewriter/rewriter_def.h"
#include "ast/ast_pp.h"
#include "util/trace.h"
#include "smt/smt_solver.h"
#include "solver/solver.h"
#include "model/model_smt2_pp.h"
#include "ast/rewriter/expr_safe_replace.h"
#include "ast/ast_util.h"
#include "solver/solver2tactic.h"
class nl_purify_tactic : public tactic {
enum polarity_t {
pol_pos,
pol_neg,
pol_dual
};
ast_manager & m;
arith_util m_util;
params_ref m_params;
bool m_produce_proofs;
ref<filter_model_converter> m_fmc;
tactic_ref m_nl_tac; // nlsat tactic
goal_ref m_nl_g; // nlsat goal
ref<solver> m_solver; // SMT solver
expr_ref_vector m_eq_preds; // predicates for equality between pairs of interface variables
svector<lbool> m_eq_values; // truth value of the equality predicates in nlsat
app_ref_vector m_new_reals; // interface real variables
app_ref_vector m_new_preds; // abstraction predicates for smt_solver (hide real constraints)
expr_ref_vector m_asms; // assumptions to pass to SMT solver
ptr_vector<expr> m_ctx_asms; // assumptions passed by context
obj_hashtable<expr> m_ctx_asms_set; // assumptions passed by context
obj_hashtable<expr> m_used_asms;
obj_map<expr, expr*> m_bool2dep;
obj_pair_map<expr,expr,expr*> m_eq_pairs; // map pairs of interface variables to auxiliary predicates
obj_map<expr,expr*> m_interface_cache; // map of compound real expression to interface variable.
obj_map<expr, polarity_t> m_polarities; // polarities of sub-expressions
public:
struct rw_cfg : public default_rewriter_cfg {
enum mode_t {
mode_interface_var,
mode_bool_preds
};
ast_manager& m;
nl_purify_tactic & m_owner;
app_ref_vector& m_new_reals;
app_ref_vector& m_new_preds;
obj_map<expr, polarity_t>& m_polarities;
obj_map<expr,expr*>& m_interface_cache;
expr_ref_vector m_args;
proof_ref_vector m_proofs;
mode_t m_mode;
rw_cfg(nl_purify_tactic & o):
m(o.m),
m_owner(o),
m_new_reals(o.m_new_reals),
m_new_preds(o.m_new_preds),
m_polarities(o.m_polarities),
m_interface_cache(o.m_interface_cache),
m_args(m),
m_proofs(m),
m_mode(mode_interface_var) {
}
virtual ~rw_cfg() {}
arith_util & u() { return m_owner.m_util; }
expr * mk_interface_var(expr* arg, proof_ref& arg_pr) {
expr* r;
if (m_interface_cache.find(arg, r)) {
return r;
}
if (is_uninterp_const(arg)) {
m_interface_cache.insert(arg, arg);
return arg;
}
r = m.mk_fresh_const(nullptr, u().mk_real());
m_new_reals.push_back(to_app(r));
m_owner.m_fmc->insert(to_app(r)->get_decl());
m_interface_cache.insert(arg, r);
expr_ref eq(m);
eq = m.mk_eq(r, arg);
if (is_real_expression(arg)) {
m_owner.m_nl_g->assert_expr(eq); // m.mk_oeq(r, arg)
}
else {
m_owner.m_solver->assert_expr(eq);
}
if (m_owner.m_produce_proofs) {
arg_pr = m.mk_oeq(arg, r);
}
return r;
}
bool is_real_expression(expr* e) {
return is_app(e) && (to_app(e)->get_family_id() == u().get_family_id());
}
void mk_interface_bool(func_decl * f, unsigned num, expr* const* args, expr_ref& result, proof_ref& pr) {
expr_ref old_pred(m.mk_app(f, num, args), m);
polarity_t pol = m_polarities.find(old_pred);
result = m.mk_fresh_const(nullptr, m.mk_bool_sort());
m_polarities.insert(result, pol);
m_new_preds.push_back(to_app(result));
m_owner.m_fmc->insert(to_app(result)->get_decl());
if (pol != pol_neg) {
m_owner.m_nl_g->assert_expr(m.mk_or(m.mk_not(result), old_pred));
}
if (pol != pol_pos) {
m_owner.m_nl_g->assert_expr(m.mk_or(result, m.mk_not(old_pred)));
}
if (m_owner.m_produce_proofs) {
pr = m.mk_oeq(old_pred, result);
}
TRACE("nlsat_smt", tout << old_pred << " : " << result << "\n";);
}
bool reduce_quantifier(quantifier * old_q,
expr * new_body,
expr * const * new_patterns,
expr * const * new_no_patterns,
expr_ref & result,
proof_ref & result_pr) {
throw tactic_exception("quantifiers are not supported in mixed-mode nlsat engine");
}
br_status reduce_app(func_decl * f, unsigned num, expr* const* args, expr_ref& result, proof_ref & pr) {
if (m_mode == mode_bool_preds) {
return reduce_app_bool(f, num, args, result, pr);
}
else {
return reduce_app_real(f, num, args, result, pr);
}
}
br_status reduce_app_bool(func_decl * f, unsigned num, expr* const* args, expr_ref& result, proof_ref & pr) {
if (f->get_family_id() == m.get_basic_family_id()) {
if (f->get_decl_kind() == OP_EQ && u().is_real(args[0])) {
mk_interface_bool(f, num, args, result, pr);
return BR_DONE;
}
else {
return BR_FAILED;
}
}
if (f->get_family_id() == u().get_family_id()) {
switch (f->get_decl_kind()) {
case OP_LE: case OP_GE: case OP_LT: case OP_GT:
// these are the only real cases of non-linear atomic formulas besides equality.
mk_interface_bool(f, num, args, result, pr);
return BR_DONE;
default:
return BR_FAILED;
}
}
return BR_FAILED;
}
// (+ (f x) y)
// (f (+ x y))
//
bool is_arith_op(expr* e) {
return is_app(e) && to_app(e)->get_family_id() == u().get_family_id();
}
br_status reduce_app_real(func_decl * f, unsigned num, expr* const* args, expr_ref& result, proof_ref & pr) {
bool has_interface = false;
bool is_arith = false;
if (f->get_family_id() == u().get_family_id()) {
switch (f->get_decl_kind()) {
case OP_NUM:
case OP_IRRATIONAL_ALGEBRAIC_NUM:
return BR_FAILED;
default:
is_arith = true;
break;
}
}
m_args.reset();
m_proofs.reset();
for (unsigned i = 0; i < num; ++i) {
expr* arg = args[i];
proof_ref arg_pr(m);
if (is_arith && !is_arith_op(arg)) {
has_interface = true;
m_args.push_back(mk_interface_var(arg, arg_pr));
}
else if (!is_arith && u().is_real(arg)) {
has_interface = true;
m_args.push_back(mk_interface_var(arg, arg_pr));
}
else {
m_args.push_back(arg);
}
if (arg_pr) {
m_proofs.push_back(arg_pr);
}
}
if (has_interface) {
result = m.mk_app(f, num, m_args.c_ptr());
if (m_owner.m_produce_proofs) {
pr = m.mk_oeq_congruence(m.mk_app(f, num, args), to_app(result), m_proofs.size(), m_proofs.c_ptr());
}
TRACE("nlsat_smt", tout << result << "\n";);
return BR_DONE;
}
else {
return BR_FAILED;
}
}
};
private:
class rw : public rewriter_tpl<rw_cfg> {
rw_cfg m_cfg;
public:
rw(nl_purify_tactic & o):
rewriter_tpl<rw_cfg>(o.m, o.m_produce_proofs, m_cfg),
m_cfg(o) {
}
void set_bool_mode() {
m_cfg.m_mode = rw_cfg::mode_bool_preds;
}
void set_interface_var_mode() {
m_cfg.m_mode = rw_cfg::mode_interface_var;
}
};
arith_util & u() { return m_util; }
void check_point() {
if (m.canceled()) {
throw tactic_exception(Z3_CANCELED_MSG);
}
}
void display_result(std::ostream& out, goal_ref_buffer const& result) {
for (unsigned i = 0; i < result.size(); ++i) {
result[i]->display_with_dependencies(out << "goal\n");
}
}
void update_eq_values(model_ref& mdl) {
expr_ref tmp(m);
for (unsigned i = 0; i < m_eq_preds.size(); ++i) {
expr* pred = m_eq_preds[i].get();
m_eq_values[i] = l_undef;
if (mdl->eval(pred, tmp)) {
if (m.is_true(tmp)) {
m_eq_values[i] = l_true;
}
else if (m.is_false(tmp)) {
m_eq_values[i] = l_false;
}
}
}
}
void solve(
goal_ref const& g,
goal_ref_buffer& result,
expr_dependency_ref& core,
model_converter_ref& mc) {
while (true) {
check_point();
TRACE("nlsat_smt", m_solver->display(tout << "SMT:\n"); m_nl_g->display(tout << "\nNL:\n"); );
goal_ref tmp_nl = alloc(goal, m, true, false);
model_converter_ref nl_mc;
proof_converter_ref nl_pc;
expr_dependency_ref nl_core(m);
result.reset();
tmp_nl->copy_from(*m_nl_g.get());
(*m_nl_tac)(tmp_nl, result, nl_mc, nl_pc, nl_core);
if (is_decided_unsat(result)) {
core2result(core, g, result);
TRACE("nlsat_smt", tout << "unsat\n";);
break;
}
if (!is_decided_sat(result)) {
TRACE("nlsat_smt", tout << "not a unit\n";);
break;
}
// extract evaluation on interface variables.
// assert booleans that evaluate to true.
// assert equalities between equal interface real variables.
model_ref mdl_nl, mdl_smt;
if (nl_mc.get()) {
model_converter2model(m, nl_mc.get(), mdl_nl);
update_eq_values(mdl_nl);
enforce_equalities(mdl_nl, m_nl_g);
setup_assumptions(mdl_nl);
TRACE("nlsat_smt",
model_smt2_pp(tout << "nl model\n", m, *mdl_nl.get(), 0);
m_solver->display(tout << "smt goal:\n"); tout << "\n";);
}
result.reset();
lbool r = m_solver->check_sat(m_asms.size(), m_asms.c_ptr());
if (r == l_false) {
// extract the core from the result
ptr_vector<expr> ecore, asms;
expr_ref_vector clause(m);
expr_ref fml(m);
get_unsat_core(ecore, asms);
//
// assumptions should also be used for the nlsat tactic,
// but since it does not support assumptions at this time
// we overapproximate the necessary core and accumulate
// all assumptions that are ever used.
//
for (unsigned i = 0; i < asms.size(); ++i) {
m_used_asms.insert(asms[i]);
}
if (ecore.empty()) {
core2result(core, g, result);
break;
}
for (unsigned i = 0; i < ecore.size(); ++i) {
clause.push_back(mk_not(m, ecore[i]));
}
fml = mk_or(m, clause.size(), clause.c_ptr());
m_nl_g->assert_expr(fml);
continue;
}
else if (r == l_true) {
m_solver->get_model(mdl_smt);
if (enforce_equalities(mdl_smt, m_nl_g)) {
// SMT enforced a new equality that wasn't true for nlsat.
continue;
}
TRACE("nlsat_smt",
m_fmc->display(tout << "joint state is sat\n");
nl_mc->display(tout << "nl\n"););
if (mdl_nl.get()) {
merge_models(*mdl_nl.get(), mdl_smt);
}
mc = m_fmc.get();
apply(mc, mdl_smt, 0);
mc = model2model_converter(mdl_smt.get());
result.push_back(alloc(goal, m));
}
else {
TRACE("nlsat_smt", tout << "unknown\n";);
}
break;
}
TRACE("nlsat_smt", display_result(tout, result););
}
void get_unsat_core(ptr_vector<expr>& core, ptr_vector<expr>& asms) {
m_solver->get_unsat_core(core);
for (unsigned i = 0; i < core.size(); ++i) {
if (m_ctx_asms_set.contains(core[i])) {
asms.push_back(core[i]);
core[i] = core.back();
core.pop_back();
--i;
}
}
}
void core2result(expr_dependency_ref & lcore, goal_ref const& g, goal_ref_buffer& result) {
result.reset();
proof * pr = nullptr;
lcore = nullptr;
g->reset();
obj_hashtable<expr>::iterator it = m_used_asms.begin(), end = m_used_asms.end();
for (; it != end; ++it) {
lcore = m.mk_join(lcore, m.mk_leaf(m_bool2dep.find(*it)));
}
g->assert_expr(m.mk_false(), pr, lcore);
TRACE("nlsat_smt", g->display_with_dependencies(tout););
result.push_back(g.get());
}
void setup_assumptions(model_ref& mdl) {
m_asms.reset();
m_asms.append(m_ctx_asms.size(), m_ctx_asms.c_ptr());
app_ref_vector const& fresh_preds = m_new_preds;
expr_ref tmp(m);
for (unsigned i = 0; i < fresh_preds.size(); ++i) {
expr* pred = fresh_preds[i];
if (mdl->eval(pred, tmp)) {
polarity_t pol = m_polarities.find(pred);
// if assumption literals are used to satisfy NL state,
// we have to assume them when satisfying SMT state
if (pol != pol_neg && m.is_false(tmp)) {
m_asms.push_back(m.mk_not(pred));
}
else if (pol != pol_pos && m.is_true(tmp)) {
m_asms.push_back(pred);
}
}
}
for (unsigned i = 0; i < m_eq_preds.size(); ++i) {
expr* pred = m_eq_preds[i].get();
switch (m_eq_values[i]) {
case l_true:
m_asms.push_back(pred);
break;
case l_false:
m_asms.push_back(m.mk_not(pred));
break;
default:
break;
}
}
TRACE("nlsat_smt",
tout << "assumptions:\n" << m_asms << "\n";);
}
bool enforce_equalities(model_ref& mdl, goal_ref const& nl_g) {
TRACE("nlsat_smt", tout << "Enforce equalities " << m_interface_cache.size() << "\n";);
bool new_equality = false;
expr_ref_vector nums(m);
obj_map<expr, expr*> num2var;
obj_map<expr, expr*>::iterator it = m_interface_cache.begin(), end = m_interface_cache.end();
for (; it != end; ++it) {
expr_ref r(m);
expr* v, *w, *pred;
w = it->m_value;
VERIFY(mdl->eval(w, r));
TRACE("nlsat_smt", tout << mk_pp(w, m) << " |-> " << r << "\n";);
nums.push_back(r);
if (num2var.find(r, v)) {
if (!m_eq_pairs.find(v, w, pred)) {
pred = m.mk_fresh_const(nullptr, m.mk_bool_sort());
m_eq_preds.push_back(pred);
m_eq_values.push_back(l_true);
m_fmc->insert(to_app(pred)->get_decl());
nl_g->assert_expr(m.mk_or(m.mk_not(pred), m.mk_eq(w, v)));
nl_g->assert_expr(m.mk_or(pred, m.mk_not(m.mk_eq(w, v))));
m_solver->assert_expr(m.mk_iff(pred, m.mk_eq(w, v)));
new_equality = true;
m_eq_pairs.insert(v, w, pred);
}
else {
// interface equality is already enforced.
}
}
else {
num2var.insert(r, w);
}
}
return new_equality;
}
void merge_models(model const& mdl_nl, model_ref& mdl_smt) {
expr_safe_replace num2num(m);
expr_ref result(m), val2(m);
expr_ref_vector args(m);
unsigned sz = mdl_nl.get_num_constants();
for (unsigned i = 0; i < sz; ++i) {
func_decl* v = mdl_nl.get_constant(i);
if (u().is_real(v->get_range())) {
expr* val = mdl_nl.get_const_interp(v);
if (mdl_smt->eval(v, val2)) {
if (val != val2) {
num2num.insert(val2, val);
}
}
}
}
sz = mdl_smt->get_num_functions();
for (unsigned i = 0; i < sz; ++i) {
func_decl* f = mdl_smt->get_function(i);
if (has_real(f)) {
unsigned arity = f->get_arity();
func_interp* f1 = mdl_smt->get_func_interp(f);
func_interp* f2 = alloc(func_interp, m, f->get_arity());
for (unsigned j = 0; j < f1->num_entries(); ++j) {
args.reset();
func_entry const* entry = f1->get_entry(j);
for (unsigned k = 0; k < arity; ++k) {
translate(num2num, entry->get_arg(k), result);
args.push_back(result);
}
translate(num2num, entry->get_result(), result);
f2->insert_entry(args.c_ptr(), result);
}
translate(num2num, f1->get_else(), result);
f2->set_else(result);
mdl_smt->register_decl(f, f2);
}
}
mdl_smt->copy_const_interps(mdl_nl);
}
bool has_real(func_decl* f) {
for (unsigned i = 0; i < f->get_arity(); ++i) {
if (u().is_real(f->get_domain(i))) return true;
}
return u().is_real(f->get_range());
}
void translate(expr_safe_replace& num2num, expr* e, expr_ref& result) {
result = nullptr;
if (e) {
num2num(e, result);
}
}
void get_polarities(goal const& g) {
ptr_vector<expr> forms;
svector<polarity_t> pols;
unsigned sz = g.size();
for (unsigned i = 0; i < sz; ++i) {
forms.push_back(g.form(i));
pols.push_back(pol_pos);
}
polarity_t p, q;
while (!forms.empty()) {
expr* e = forms.back();
p = pols.back();
forms.pop_back();
pols.pop_back();
if (m_polarities.find(e, q)) {
if (p == q || q == pol_dual) continue;
p = pol_dual;
}
TRACE("nlsat_smt_verbose", tout << mk_pp(e, m) << "\n";);
m_polarities.insert(e, p);
if (is_quantifier(e) || is_var(e)) {
throw tactic_exception("nl-purify tactic does not support quantifiers");
}
SASSERT(is_app(e));
app* a = to_app(e);
func_decl* f = a->get_decl();
if (f->get_family_id() == m.get_basic_family_id() && p != pol_dual) {
switch(f->get_decl_kind()) {
case OP_NOT:
p = neg(p);
break;
case OP_AND:
case OP_OR:
break;
default:
p = pol_dual;
break;
}
}
else {
p = pol_dual;
}
for (unsigned i = 0; i < a->get_num_args(); ++i) {
forms.push_back(a->get_arg(i));
pols.push_back(p);
}
}
}
polarity_t neg(polarity_t p) {
switch (p) {
case pol_pos: return pol_neg;
case pol_neg: return pol_pos;
case pol_dual: return pol_dual;
}
return pol_dual;
}
polarity_t join(polarity_t p, polarity_t q) {
if (p == q) return p;
return pol_dual;
}
void rewrite_goal(rw& r, goal_ref const& g) {
r.reset();
expr_ref new_curr(m);
proof_ref new_pr(m);
unsigned sz = g->size();
for (unsigned i = 0; i < sz; i++) {
expr * curr = g->form(i);
r(curr, new_curr, new_pr);
if (m_produce_proofs) {
proof * pr = g->pr(i);
new_pr = m.mk_modus_ponens(pr, new_pr);
}
g->update(i, new_curr, new_pr, g->dep(i));
}
}
void remove_pure_arith(goal_ref const& g) {
obj_map<expr, bool> is_pure;
unsigned sz = g->size();
for (unsigned i = 0; i < sz; i++) {
expr * curr = g->form(i);
if (is_pure_arithmetic(is_pure, curr)) {
m_nl_g->assert_expr(curr, g->pr(i), g->dep(i));
g->update(i, m.mk_true(), g->pr(i), g->dep(i));
}
}
}
bool is_pure_arithmetic(obj_map<expr, bool>& is_pure, expr* e0) {
ptr_vector<expr> todo;
todo.push_back(e0);
while (!todo.empty()) {
expr* e = todo.back();
if (is_pure.contains(e)) {
todo.pop_back();
continue;
}
if (!is_app(e)) {
todo.pop_back();
is_pure.insert(e, false);
continue;
}
app* a = to_app(e);
bool pure = false, all_found = true, p;
pure |= (a->get_family_id() == u().get_family_id()) && u().is_real(a);
pure |= (m.is_eq(e) && u().is_real(a->get_arg(0)));
pure |= (a->get_family_id() == u().get_family_id()) && m.is_bool(a) && u().is_real(a->get_arg(0));
pure |= (a->get_family_id() == m.get_basic_family_id());
pure |= is_uninterp_const(a) && u().is_real(a);
for (unsigned i = 0; i < a->get_num_args(); ++i) {
if (!is_pure.find(a->get_arg(i), p)) {
todo.push_back(a->get_arg(i));
all_found = false;
}
else {
pure &= p;
}
}
if (all_found) {
is_pure.insert(e, pure);
todo.pop_back();
}
}
return is_pure.find(e0);
}
public:
nl_purify_tactic(ast_manager & m, params_ref const& p):
m(m),
m_util(m),
m_params(p),
m_fmc(nullptr),
m_nl_tac(mk_nlsat_tactic(m, p)),
m_nl_g(nullptr),
m_solver(mk_smt_solver(m, p, symbol::null)),
m_eq_preds(m),
m_new_reals(m),
m_new_preds(m),
m_asms(m)
{}
~nl_purify_tactic() override {}
void updt_params(params_ref const & p) override {
m_params = p;
}
tactic * translate(ast_manager& m) override {
return alloc(nl_purify_tactic, m, m_params);
}
void collect_statistics(statistics & st) const override {
m_nl_tac->collect_statistics(st);
m_solver->collect_statistics(st);
}
void reset_statistics() override {
m_nl_tac->reset_statistics();
}
void cleanup() override {
m_solver = mk_smt_solver(m, m_params, symbol::null);
m_nl_tac->cleanup();
m_eq_preds.reset();
m_eq_values.reset();
m_new_reals.reset();
m_new_preds.reset();
m_eq_pairs.reset();
m_polarities.reset();
m_ctx_asms.reset();
m_ctx_asms_set.reset();
m_used_asms.reset();
m_bool2dep.reset();
}
void operator()(goal_ref const & g,
goal_ref_buffer & result,
model_converter_ref & mc,
proof_converter_ref & pc,
expr_dependency_ref & core) override {
tactic_report report("qfufnl-purify", *g);
TRACE("nlsat_smt", g->display(tout););
m_produce_proofs = g->proofs_enabled();
mc = nullptr; pc = nullptr; core = nullptr;
fail_if_proof_generation("qfufnra-purify", g);
// fail_if_unsat_core_generation("qfufnra-purify", g);
rw r(*this);
expr_ref_vector clauses(m);
m_nl_g = alloc(goal, m, true, false);
m_fmc = alloc(filter_model_converter, m);
// first hoist interface variables,
// then annotate subformulas by polarities,
// finally extract polynomial inequalities by
// creating a place-holder predicate inside the
// original goal and extracting pure nlsat clauses.
r.set_interface_var_mode();
rewrite_goal(r, g);
if (!g->unsat_core_enabled()) {
remove_pure_arith(g);
}
get_polarities(*g.get());
r.set_bool_mode();
rewrite_goal(r, g);
extract_clauses_and_dependencies(g, clauses, m_ctx_asms, m_bool2dep, m_fmc);
TRACE("nlsat_smt", tout << clauses << "\n";);
for (unsigned i = 0; i < m_ctx_asms.size(); ++i) {
m_ctx_asms_set.insert(m_ctx_asms[i]);
}
for (unsigned i = 0; i < clauses.size(); ++i) {
m_solver->assert_expr(clauses[i].get());
}
g->inc_depth();
solve(g, result, core, mc);
}
};
tactic * mk_nl_purify_tactic(ast_manager& m, params_ref const& p) {
return alloc(nl_purify_tactic, m, p);
}

2
src/tactic/sls/sls_engine.cpp
View file

@ -492,7 +492,7 @@ lbool sls_engine::search() {
score = m_tracker.get_top_sum(); score = m_tracker.get_top_sum();
// update assertion weights if a weigthing is enabled (sp < 1024) // update assertion weights if a weighting is enabled (sp < 1024)
if (m_paws) if (m_paws)
{ {
for (unsigned i = 0; i < sz; i++) for (unsigned i = 0; i < sz; i++)

1
src/tactic/tactic.h
View file

@ -78,7 +78,6 @@ protected:
friend class nary_tactical; friend class nary_tactical;
friend class binary_tactical; friend class binary_tactical;
friend class unary_tactical; friend class unary_tactical;
friend class nl_purify_tactic;
}; };

4
src/test/lp/smt_reader.h
View file

@ -193,14 +193,14 @@ namespace lp {
} }
} }
void adjust_rigth_side(formula_constraint & /* c*/, lisp_elem & /*el*/) { void adjust_right_side(formula_constraint & /* c*/, lisp_elem & /*el*/) {
// lp_assert(el.m_head == "0"); // do nothing for the time being // lp_assert(el.m_head == "0"); // do nothing for the time being
} }
void set_constraint_coeffs(formula_constraint & c, lisp_elem & el) { void set_constraint_coeffs(formula_constraint & c, lisp_elem & el) {
lp_assert(el.m_elems.size() == 2); lp_assert(el.m_elems.size() == 2);
set_constraint_coeffs_on_coeff_element(c, el.m_elems[0]); set_constraint_coeffs_on_coeff_element(c, el.m_elems[0]);
adjust_rigth_side(c, el.m_elems[1]); adjust_right_side(c, el.m_elems[1]);
} }

2
src/util/hwf.cpp
View file

@ -303,7 +303,7 @@ void hwf_manager::round_to_integral(mpf_rounding_mode rm, hwf const & x, hwf & o
// CMW: modf is not the right function here. // CMW: modf is not the right function here.
// modf(x.value, &o.value); // modf(x.value, &o.value);
// According to the Intel Architecture manual, the x87-instrunction FRNDINT is the // According to the Intel Architecture manual, the x87-instruction FRNDINT is the
// same in 32-bit and 64-bit mode. The _mm_round_* intrinsics are SSE4 extensions. // same in 32-bit and 64-bit mode. The _mm_round_* intrinsics are SSE4 extensions.
#ifdef _WINDOWS #ifdef _WINDOWS
#if defined(USE_INTRINSICS) && \ #if defined(USE_INTRINSICS) && \

11
src/util/memory_manager.cpp
View file

@ -241,15 +241,8 @@ void * memory::allocate(char const* file, int line, char const* obj, size_t s) {
// when the local counter > SYNCH_THRESHOLD // when the local counter > SYNCH_THRESHOLD
#define SYNCH_THRESHOLD 100000 #define SYNCH_THRESHOLD 100000
#ifdef _WINDOWS thread_local long long g_memory_thread_alloc_size = 0;
// Actually this is VS specific instead of Windows specific. thread_local long long g_memory_thread_alloc_count = 0;
__declspec(thread) long long g_memory_thread_alloc_size = 0;
__declspec(thread) long long g_memory_thread_alloc_count = 0;
#else
// GCC style
__thread long long g_memory_thread_alloc_size = 0;
__thread long long g_memory_thread_alloc_count = 0;
#endif
static void synchronize_counters(bool allocating) { static void synchronize_counters(bool allocating) {
#ifdef PROFILE_MEMORY #ifdef PROFILE_MEMORY

6
src/util/mpz.cpp
View file

@ -30,7 +30,6 @@ Revision History:
#else #else
#error No multi-precision library selected. #error No multi-precision library selected.
#endif #endif
#include <immintrin.h>
// Available GCD algorithms // Available GCD algorithms
// #define EUCLID_GCD // #define EUCLID_GCD
@ -46,6 +45,11 @@ Revision History:
#define LEHMER_GCD #define LEHMER_GCD
#endif #endif
#ifdef _WINDOWS
// This is needed for _tzcnt_u32 and friends.
#include <immintrin.h>
#endif
#if defined(__GNUC__) #if defined(__GNUC__)
#define _trailing_zeros32(X) __builtin_ctz(X) #define _trailing_zeros32(X) __builtin_ctz(X)
#else #else

4
src/util/trace.h
View file

@ -24,10 +24,6 @@ Revision History:
#undef max #undef max
#undef min #undef min
#endif #endif
#ifdef __APPLE__
#undef max
#undef min
#endif
#include<fstream> #include<fstream>
#ifdef _TRACE #ifdef _TRACE

8
src/util/util.h
View file

@ -63,14 +63,6 @@ static_assert(sizeof(int64_t) == 8, "64 bits");
#define VEC2PTR(_x_) ((_x_).size() ? &(_x_)[0] : 0) #define VEC2PTR(_x_) ((_x_).size() ? &(_x_)[0] : 0)
#ifdef _WINDOWS
// Disable thread local declspec as it seems to not work downlevel.
// #define THREAD_LOCAL __declspec(thread)
#define THREAD_LOCAL
#else
#define THREAD_LOCAL
#endif
#ifdef _MSC_VER #ifdef _MSC_VER
# define STD_CALL __cdecl # define STD_CALL __cdecl
#else #else