mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
Merge branch 'master' of https://github.com/Z3Prover/z3
This commit is contained in:
commit
a8e7974011
|
@ -234,22 +234,18 @@ if ("${CMAKE_SYSTEM_NAME}" STREQUAL "Linux")
|
|||
if ("${TARGET_ARCHITECTURE}" STREQUAL "x86_64")
|
||||
list(APPEND Z3_COMPONENT_CXX_DEFINES "-D_USE_THREAD_LOCAL")
|
||||
endif()
|
||||
z3_add_cxx_flag("-fno-strict-aliasing" REQUIRED)
|
||||
elseif ("${CMAKE_SYSTEM_NAME}" STREQUAL "Darwin")
|
||||
# Does OSX really not need any special flags?
|
||||
message(STATUS "Platform: Darwin")
|
||||
elseif ("${CMAKE_SYSTEM_NAME}" MATCHES "FreeBSD")
|
||||
message(STATUS "Platform: FreeBSD")
|
||||
list(APPEND Z3_COMPONENT_CXX_DEFINES "-D_FREEBSD_")
|
||||
z3_add_cxx_flag("-fno-strict-aliasing" REQUIRED)
|
||||
elseif ("${CMAKE_SYSTEM_NAME}" MATCHES "OpenBSD")
|
||||
message(STATUS "Platform: OpenBSD")
|
||||
list(APPEND Z3_COMPONENT_CXX_DEFINES "-D_OPENBSD_")
|
||||
z3_add_cxx_flag("-fno-strict-aliasing" REQUIRED)
|
||||
elseif (CYGWIN)
|
||||
message(STATUS "Platform: Cygwin")
|
||||
list(APPEND Z3_COMPONENT_CXX_DEFINES "-D_CYGWIN")
|
||||
z3_add_cxx_flag("-fno-strict-aliasing" REQUIRED)
|
||||
elseif (WIN32)
|
||||
message(STATUS "Platform: Windows")
|
||||
list(APPEND Z3_COMPONENT_CXX_DEFINES "-D_WINDOWS")
|
||||
|
|
|
@ -2443,26 +2443,26 @@ def mk_config():
|
|||
SO_EXT = '.dylib'
|
||||
SLIBFLAGS = '-dynamiclib'
|
||||
elif sysname == 'Linux':
|
||||
CXXFLAGS = '%s -fno-strict-aliasing -D_LINUX_' % CXXFLAGS
|
||||
CXXFLAGS = '%s -D_LINUX_' % CXXFLAGS
|
||||
OS_DEFINES = '-D_LINUX_'
|
||||
SO_EXT = '.so'
|
||||
LDFLAGS = '%s -lrt' % LDFLAGS
|
||||
SLIBFLAGS = '-shared'
|
||||
SLIBEXTRAFLAGS = '%s -lrt' % SLIBEXTRAFLAGS
|
||||
elif sysname == 'FreeBSD':
|
||||
CXXFLAGS = '%s -fno-strict-aliasing -D_FREEBSD_' % CXXFLAGS
|
||||
CXXFLAGS = '%s -D_FREEBSD_' % CXXFLAGS
|
||||
OS_DEFINES = '-D_FREEBSD_'
|
||||
SO_EXT = '.so'
|
||||
LDFLAGS = '%s -lrt' % LDFLAGS
|
||||
SLIBFLAGS = '-shared'
|
||||
SLIBEXTRAFLAGS = '%s -lrt' % SLIBEXTRAFLAGS
|
||||
elif sysname == 'OpenBSD':
|
||||
CXXFLAGS = '%s -fno-strict-aliasing -D_OPENBSD_' % CXXFLAGS
|
||||
CXXFLAGS = '%s -D_OPENBSD_' % CXXFLAGS
|
||||
OS_DEFINES = '-D_OPENBSD_'
|
||||
SO_EXT = '.so'
|
||||
SLIBFLAGS = '-shared'
|
||||
elif sysname[:6] == 'CYGWIN':
|
||||
CXXFLAGS = '%s -D_CYGWIN -fno-strict-aliasing' % CXXFLAGS
|
||||
CXXFLAGS = '%s -D_CYGWIN' % CXXFLAGS
|
||||
OS_DEFINES = '-D_CYGWIN'
|
||||
SO_EXT = '.dll'
|
||||
SLIBFLAGS = '-shared'
|
||||
|
|
|
@ -1215,6 +1215,44 @@ struct
|
|||
let mk_numeral ctx v size = Z3native.mk_numeral ctx v (mk_sort ctx size)
|
||||
end
|
||||
|
||||
module Seq =
|
||||
struct
|
||||
let mk_seq_sort = Z3native.mk_seq_sort
|
||||
let is_seq_sort = Z3native.is_seq_sort
|
||||
let mk_re_sort = Z3native.mk_re_sort
|
||||
let is_re_sort = Z3native.is_re_sort
|
||||
let mk_string_sort = Z3native.mk_string_sort
|
||||
let is_string_sort = Z3native.is_string_sort
|
||||
let mk_string = Z3native.mk_string
|
||||
let is_string = Z3native.is_string
|
||||
let get_string = Z3native.get_string
|
||||
let mk_seq_empty = Z3native.mk_seq_empty
|
||||
let mk_seq_unit = Z3native.mk_seq_unit
|
||||
let mk_seq_concat ctx args = Z3native.mk_seq_concat ctx (List.length args) args
|
||||
let mk_seq_prefix = Z3native.mk_seq_prefix
|
||||
let mk_seq_suffix = Z3native.mk_seq_suffix
|
||||
let mk_seq_contains = Z3native.mk_seq_contains
|
||||
let mk_seq_extract = Z3native.mk_seq_extract
|
||||
let mk_seq_replace = Z3native.mk_seq_replace
|
||||
let mk_seq_at = Z3native.mk_seq_at
|
||||
let mk_seq_length = Z3native.mk_seq_length
|
||||
let mk_seq_index = Z3native.mk_seq_index
|
||||
let mk_str_to_int = Z3native.mk_str_to_int
|
||||
let mk_int_to_str = Z3native.mk_int_to_str
|
||||
let mk_seq_to_re = Z3native.mk_seq_to_re
|
||||
let mk_seq_in_re = Z3native.mk_seq_in_re
|
||||
let mk_re_plus = Z3native.mk_re_plus
|
||||
let mk_re_star = Z3native.mk_re_star
|
||||
let mk_re_option = Z3native.mk_re_option
|
||||
let mk_re_union ctx args = Z3native.mk_re_union ctx (List.length args) args
|
||||
let mk_re_concat ctx args = Z3native.mk_re_concat ctx (List.length args) args
|
||||
let mk_re_range = Z3native.mk_re_range
|
||||
let mk_re_loop = Z3native.mk_re_loop
|
||||
let mk_re_intersect = Z3native.mk_re_intersect
|
||||
let mk_re_complement = Z3native.mk_re_complement
|
||||
let mk_re_empty = Z3native.mk_re_empty
|
||||
let mk_re_full = Z3native.mk_re_full
|
||||
end
|
||||
|
||||
module FloatingPoint =
|
||||
struct
|
||||
|
|
|
@ -1825,6 +1825,116 @@ sig
|
|||
val mk_numeral : context -> string -> int -> Expr.expr
|
||||
end
|
||||
|
||||
(** Sequences, Strings and Regular Expressions **)
|
||||
module Seq :
|
||||
sig
|
||||
(* create a sequence sort *)
|
||||
val mk_seq_sort : context -> Sort.sort -> Sort.sort
|
||||
|
||||
(* test if sort is a sequence sort *)
|
||||
val is_seq_sort : context -> Sort.sort -> bool
|
||||
|
||||
(* create regular expression sorts over sequences of the argument sort *)
|
||||
val mk_re_sort : context -> Sort.sort -> Sort.sort
|
||||
|
||||
(* test if sort is a regular expression sort *)
|
||||
val is_re_sort : context -> Sort.sort -> bool
|
||||
|
||||
(* create string sort *)
|
||||
val mk_string_sort : context -> Sort.sort
|
||||
|
||||
(* test if sort is a string sort (a sequence of 8-bit bit-vectors) *)
|
||||
val is_string_sort : context -> Sort.sort -> bool
|
||||
|
||||
(* create a string literal *)
|
||||
val mk_string : context -> string -> Expr.expr
|
||||
|
||||
(* test if expression is a string *)
|
||||
val is_string : context -> Expr.expr -> bool
|
||||
|
||||
(* retrieve string from string Expr.expr *)
|
||||
val get_string : context -> Expr.expr -> string
|
||||
|
||||
(* the empty sequence over base sort *)
|
||||
val mk_seq_empty : context -> Sort.sort -> Expr.expr
|
||||
|
||||
(* a unit sequence *)
|
||||
val mk_seq_unit : context -> Expr.expr -> Expr.expr
|
||||
|
||||
(* sequence concatenation *)
|
||||
val mk_seq_concat : context -> Expr.expr list -> Expr.expr
|
||||
|
||||
(* predicate if the first argument is a prefix of the second *)
|
||||
val mk_seq_prefix : context -> Expr.expr -> Expr.expr -> Expr.expr
|
||||
|
||||
(* predicate if the first argument is a suffix of the second *)
|
||||
val mk_seq_suffix : context -> Expr.expr -> Expr.expr -> Expr.expr
|
||||
|
||||
(* predicate if the first argument contains the second *)
|
||||
val mk_seq_contains : context -> Expr.expr -> Expr.expr -> Expr.expr
|
||||
|
||||
(* extract sub-sequence starting at index given by second argument and of length provided by third argument *)
|
||||
val mk_seq_extract : context -> Expr.expr -> Expr.expr -> Expr.expr -> Expr.expr
|
||||
|
||||
(* replace first occurrence of second argument by third *)
|
||||
val mk_seq_replace : context -> Expr.expr -> Expr.expr -> Expr.expr -> Expr.expr
|
||||
|
||||
(* a unit sequence at index provided by second argument *)
|
||||
val mk_seq_at : context -> Expr.expr -> Expr.expr -> Expr.expr
|
||||
|
||||
(* length of a sequence *)
|
||||
val mk_seq_length : context -> Expr.expr -> Expr.expr
|
||||
|
||||
(* index of the first occurrence of the second argument in the first *)
|
||||
val mk_seq_index : context -> Expr.expr -> Expr.expr -> Expr.expr -> Expr.expr
|
||||
|
||||
(* retrieve integer expression encoded in string *)
|
||||
val mk_str_to_int : context -> Expr.expr -> Expr.expr
|
||||
|
||||
(* convert an integer expression to a string *)
|
||||
val mk_int_to_str : context -> Expr.expr -> Expr.expr
|
||||
|
||||
(* create regular expression that accepts the argument sequence *)
|
||||
val mk_seq_to_re : context -> Expr.expr -> Expr.expr
|
||||
|
||||
(* regular expression membership predicate *)
|
||||
val mk_seq_in_re : context -> Expr.expr -> Expr.expr -> Expr.expr
|
||||
|
||||
(* regular expression plus *)
|
||||
val mk_re_plus : context -> Expr.expr -> Expr.expr
|
||||
|
||||
(* regular expression star *)
|
||||
val mk_re_star : context -> Expr.expr -> Expr.expr
|
||||
|
||||
(* optional regular expression *)
|
||||
val mk_re_option : context -> Expr.expr -> Expr.expr
|
||||
|
||||
(* union of regular expressions *)
|
||||
val mk_re_union : context -> Expr.expr list -> Expr.expr
|
||||
|
||||
(* concatenation of regular expressions* )
|
||||
val mk_re_concat : context -> Expr.expr list -> Expr.expr
|
||||
|
||||
(* regular expression for the range between two characters *)
|
||||
val mk_re_range : context -> Expr.expr -> Expr.expr -> Expr.expr
|
||||
|
||||
(* bounded loop regular expression *)
|
||||
val mk_re_loop : context -> Expr.expr -> int -> int -> Expr.expr
|
||||
|
||||
(* intersection of regular expressions *)
|
||||
val mk_re_intersect : context -> int -> Expr.expr list -> Expr.expr
|
||||
|
||||
(* the regular expression complement *)
|
||||
val mk_re_complement : context -> Expr.expr -> Expr.expr
|
||||
|
||||
(* the regular expression that accepts no sequences *)
|
||||
val mk_re_empty : context -> Sort.sort -> Expr.expr
|
||||
|
||||
(* the regular expression that accepts all sequences *)
|
||||
val mk_re_full : context -> Sort.sort -> Expr.expr
|
||||
|
||||
end
|
||||
|
||||
(** Floating-Point Arithmetic *)
|
||||
module FloatingPoint :
|
||||
sig
|
||||
|
|
|
@ -35,7 +35,7 @@ Revision History:
|
|||
|
||||
parameter::~parameter() {
|
||||
if (m_kind == PARAM_RATIONAL) {
|
||||
reinterpret_cast<rational *>(m_rational)->~rational();
|
||||
dealloc(m_rational);
|
||||
}
|
||||
}
|
||||
|
||||
|
@ -50,14 +50,14 @@ parameter& parameter::operator=(parameter const& other) {
|
|||
return *this;
|
||||
}
|
||||
if (m_kind == PARAM_RATIONAL) {
|
||||
reinterpret_cast<rational *>(m_rational)->~rational();
|
||||
dealloc(m_rational);
|
||||
}
|
||||
m_kind = other.m_kind;
|
||||
switch(other.m_kind) {
|
||||
case PARAM_INT: m_int = other.get_int(); break;
|
||||
case PARAM_AST: m_ast = other.get_ast(); break;
|
||||
case PARAM_SYMBOL: new (m_symbol) symbol(other.get_symbol()); break;
|
||||
case PARAM_RATIONAL: new (m_rational) rational(other.get_rational()); break;
|
||||
case PARAM_SYMBOL: m_symbol = other.m_symbol; break;
|
||||
case PARAM_RATIONAL: m_rational = alloc(rational, other.get_rational()); break;
|
||||
case PARAM_DOUBLE: m_dval = other.m_dval; break;
|
||||
case PARAM_EXTERNAL: m_ext_id = other.m_ext_id; break;
|
||||
default:
|
||||
|
|
|
@ -102,8 +102,8 @@ private:
|
|||
union {
|
||||
int m_int; // for PARAM_INT
|
||||
ast* m_ast; // for PARAM_AST
|
||||
char m_symbol[sizeof(symbol)]; // for PARAM_SYMBOL
|
||||
char m_rational[sizeof(rational)]; // for PARAM_RATIONAL
|
||||
void const* m_symbol; // for PARAM_SYMBOL
|
||||
rational* m_rational; // for PARAM_RATIONAL
|
||||
double m_dval; // for PARAM_DOUBLE (remark: this is not used in float_decl_plugin)
|
||||
unsigned m_ext_id; // for PARAM_EXTERNAL
|
||||
};
|
||||
|
@ -114,12 +114,10 @@ public:
|
|||
explicit parameter(int val): m_kind(PARAM_INT), m_int(val) {}
|
||||
explicit parameter(unsigned val): m_kind(PARAM_INT), m_int(val) {}
|
||||
explicit parameter(ast * p): m_kind(PARAM_AST), m_ast(p) {}
|
||||
explicit parameter(symbol const & s): m_kind(PARAM_SYMBOL) { new (m_symbol) symbol(s); }
|
||||
explicit parameter(rational const & r): m_kind(PARAM_RATIONAL) { new (m_rational) rational(r); }
|
||||
explicit parameter(symbol const & s): m_kind(PARAM_SYMBOL), m_symbol(s.c_ptr()) {}
|
||||
explicit parameter(rational const & r): m_kind(PARAM_RATIONAL), m_rational(alloc(rational, r)) {}
|
||||
explicit parameter(double d):m_kind(PARAM_DOUBLE), m_dval(d) {}
|
||||
explicit parameter(const char *s):m_kind(PARAM_SYMBOL) {
|
||||
new (m_symbol) symbol(s);
|
||||
}
|
||||
explicit parameter(const char *s):m_kind(PARAM_SYMBOL), m_symbol(symbol(s).c_ptr()) {}
|
||||
explicit parameter(unsigned ext_id, bool):m_kind(PARAM_EXTERNAL), m_ext_id(ext_id) {}
|
||||
parameter(parameter const&);
|
||||
|
||||
|
@ -156,8 +154,8 @@ public:
|
|||
|
||||
int get_int() const { SASSERT(is_int()); return m_int; }
|
||||
ast * get_ast() const { SASSERT(is_ast()); return m_ast; }
|
||||
symbol const & get_symbol() const { SASSERT(is_symbol()); return *(reinterpret_cast<const symbol *>(m_symbol)); }
|
||||
rational const & get_rational() const { SASSERT(is_rational()); return *(reinterpret_cast<const rational *>(m_rational)); }
|
||||
symbol get_symbol() const { SASSERT(is_symbol()); return symbol::mk_symbol_from_c_ptr(m_symbol); }
|
||||
rational const & get_rational() const { SASSERT(is_rational()); return *m_rational; }
|
||||
double get_double() const { SASSERT(is_double()); return m_dval; }
|
||||
unsigned get_ext_id() const { SASSERT(is_external()); return m_ext_id; }
|
||||
|
||||
|
|
|
@ -18,7 +18,6 @@ Revision History:
|
|||
--*/
|
||||
|
||||
#include "util/debug.h"
|
||||
#include "util/optional.h"
|
||||
#include "ast/ast_pp.h"
|
||||
#include "muz/rel/dl_interval_relation.h"
|
||||
#include "muz/rel/dl_relation_manager.h"
|
||||
|
|
|
@ -32,10 +32,8 @@ using namespace spacer;
|
|||
sym_mux::sym_mux(ast_manager & m, const std::vector<std::string> & suffixes)
|
||||
: m(m), m_ref_holder(m), m_next_sym_suffix_idx(0), m_suffixes(suffixes)
|
||||
{
|
||||
unsigned suf_sz = m_suffixes.size();
|
||||
for (unsigned i = 0; i < suf_sz; ++i) {
|
||||
symbol suff_sym = symbol(m_suffixes[i].c_str());
|
||||
m_used_suffixes.insert(suff_sym);
|
||||
for (std::string const& s : m_suffixes) {
|
||||
m_used_suffixes.insert(symbol(s.c_str()));
|
||||
}
|
||||
}
|
||||
|
||||
|
|
|
@ -239,7 +239,7 @@ namespace smt {
|
|||
for (; it != end; ++it) {
|
||||
theory_var b = it->get_base_var();
|
||||
if (b == null_theory_var) {
|
||||
TRACE("theory_arith_int", display_row(tout << "null: ", *it, true); );
|
||||
TRACE("arith_int", display_row(tout << "null: ", *it, true); );
|
||||
continue;
|
||||
}
|
||||
bool is_tight = false;
|
||||
|
@ -257,7 +257,7 @@ namespace smt {
|
|||
const_coeff = u->get_value().get_rational();
|
||||
}
|
||||
if (!is_tight) {
|
||||
TRACE("theory_arith_int",
|
||||
TRACE("arith_int",
|
||||
display_row(tout << "!tight: ", *it, true);
|
||||
display_var(tout, b);
|
||||
);
|
||||
|
|
|
@ -681,8 +681,7 @@ namespace smt {
|
|||
SASSERT(is_pure_monomial(var2expr(v)));
|
||||
expr * m = var2expr(v);
|
||||
rational val(1), v_val;
|
||||
for (unsigned i = 0; i < to_app(m)->get_num_args(); i++) {
|
||||
expr * arg = to_app(m)->get_arg(i);
|
||||
for (expr* arg : *to_app(m)) {
|
||||
theory_var curr = expr2var(arg);
|
||||
SASSERT(curr != null_theory_var);
|
||||
v_val = get_value(curr, computed_epsilon);
|
||||
|
@ -742,7 +741,6 @@ namespace smt {
|
|||
continue;
|
||||
bool computed_epsilon = false;
|
||||
bool r = check_monomial_assignment(v, computed_epsilon);
|
||||
SASSERT(!computed_epsilon); // integer variables do not use epsilon
|
||||
if (!r) {
|
||||
expr * m = get_enode(v)->get_owner();
|
||||
SASSERT(is_pure_monomial(m));
|
||||
|
@ -1249,11 +1247,9 @@ namespace smt {
|
|||
}
|
||||
|
||||
// Update the number of occurrences in the result vector.
|
||||
typename var2num_occs::iterator it2 = m_var2num_occs.begin();
|
||||
typename var2num_occs::iterator end2 = m_var2num_occs.end();
|
||||
for (; it2 != end2; ++it2) {
|
||||
if ((*it2).m_value > 1)
|
||||
varinfo.push_back(var_num_occs((*it2).m_key, (*it2).m_value));
|
||||
for (auto const& vn : m_var2num_occs) {
|
||||
if (vn.m_value > 1)
|
||||
varinfo.push_back(var_num_occs(vn.m_key, vn.m_value));
|
||||
}
|
||||
}
|
||||
|
||||
|
@ -1265,18 +1261,16 @@ namespace smt {
|
|||
SASSERT(!p.empty());
|
||||
TRACE("p2expr_bug", display_coeff_exprs(tout, p););
|
||||
ptr_buffer<expr> args;
|
||||
sbuffer<coeff_expr>::const_iterator it = p.begin();
|
||||
sbuffer<coeff_expr>::const_iterator end = p.end();
|
||||
for (; it != end; ++it) {
|
||||
rational const & c = it->first;
|
||||
expr * var = it->second;
|
||||
for (coeff_expr const& ce : p) {
|
||||
rational const & c = ce.first;
|
||||
expr * var = ce.second;
|
||||
if (!c.is_one()) {
|
||||
rational c2;
|
||||
expr * m = 0;
|
||||
if (m_util.is_numeral(var, c2))
|
||||
m = m_util.mk_numeral(c*c2, m_util.is_int(var));
|
||||
m = m_util.mk_numeral(c*c2, m_util.is_int(var) && c.is_int() && c2.is_int());
|
||||
else
|
||||
m = m_util.mk_mul(m_util.mk_numeral(c, m_util.is_int(var)), var);
|
||||
m = m_util.mk_mul(m_util.mk_numeral(c, c.is_int() && m_util.is_int(var)), var);
|
||||
m_nl_new_exprs.push_back(m);
|
||||
args.push_back(m);
|
||||
}
|
||||
|
@ -1453,8 +1447,7 @@ namespace smt {
|
|||
SASSERT(is_pure_monomial(m));
|
||||
unsigned idx = 0;
|
||||
ptr_buffer<expr> new_args;
|
||||
for (unsigned i = 0; i < to_app(m)->get_num_args(); i++) {
|
||||
expr * arg = to_app(m)->get_arg(i);
|
||||
for (expr * arg : *to_app(m)) {
|
||||
if (arg == var) {
|
||||
if (idx < d)
|
||||
idx++;
|
||||
|
@ -1487,17 +1480,15 @@ namespace smt {
|
|||
tout << "min_degree: " << d << "\n";);
|
||||
sbuffer<coeff_expr> e; // monomials/x^d where var occurs with degree d
|
||||
sbuffer<coeff_expr> r; // rest
|
||||
sbuffer<coeff_expr>::const_iterator it = p.begin();
|
||||
sbuffer<coeff_expr>::const_iterator end = p.end();
|
||||
for (; it != end; ++it) {
|
||||
expr * m = it->second;
|
||||
for (auto const& kv : p) {
|
||||
expr * m = kv.second;
|
||||
expr * f = factor(m, var, d);
|
||||
if (get_degree_of(m, var) == d) {
|
||||
e.push_back(coeff_expr(it->first, f));
|
||||
e.push_back(coeff_expr(kv.first, f));
|
||||
}
|
||||
else {
|
||||
SASSERT(get_degree_of(m, var) > d);
|
||||
r.push_back(coeff_expr(it->first, f));
|
||||
r.push_back(coeff_expr(kv.first, f));
|
||||
}
|
||||
}
|
||||
expr * s = cross_nested(e, 0);
|
||||
|
@ -1623,16 +1614,12 @@ namespace smt {
|
|||
return true;
|
||||
std::stable_sort(varinfo.begin(), varinfo.end(), var_num_occs_lt());
|
||||
TRACE("cross_nested", tout << "var num occs:\n";
|
||||
sbuffer<var_num_occs>::const_iterator it = varinfo.begin();
|
||||
sbuffer<var_num_occs>::const_iterator end = varinfo.end();
|
||||
for (; it != end ; ++it) {
|
||||
tout << mk_bounded_pp(it->first, get_manager()) << " -> " << it->second << "\n";
|
||||
for (auto const& kv : varinfo) {
|
||||
tout << mk_bounded_pp(kv.first, get_manager()) << " -> " << kv.second << "\n";
|
||||
});
|
||||
sbuffer<var_num_occs>::const_iterator it = varinfo.begin();
|
||||
sbuffer<var_num_occs>::const_iterator end = varinfo.end();
|
||||
for (; it != end; ++it) {
|
||||
for (auto const& kv : varinfo) {
|
||||
m_nl_new_exprs.reset();
|
||||
expr * var = it->first;
|
||||
expr * var = kv.first;
|
||||
expr * cn = cross_nested(p, var);
|
||||
// Remark: cn may not be well-sorted because, since a row may contain mixed integer/real monomials.
|
||||
// This is not really a problem, since evaluate_as_interval will work even if cn is not well-sorted.
|
||||
|
@ -1731,10 +1718,7 @@ namespace smt {
|
|||
*/
|
||||
template<typename Ext>
|
||||
bool theory_arith<Ext>::is_cross_nested_consistent(svector<theory_var> const & nl_cluster) {
|
||||
svector<theory_var>::const_iterator it = nl_cluster.begin();
|
||||
svector<theory_var>::const_iterator end = nl_cluster.end();
|
||||
for (; it != end; ++it) {
|
||||
theory_var v = *it;
|
||||
for (theory_var v : nl_cluster) {
|
||||
if (!is_base(v))
|
||||
continue;
|
||||
m_stats.m_nl_cross_nested++;
|
||||
|
@ -1765,10 +1749,7 @@ namespace smt {
|
|||
template<typename Ext>
|
||||
void theory_arith<Ext>::init_grobner_var_order(svector<theory_var> const & nl_cluster, grobner & gb) {
|
||||
// Initialize variable order
|
||||
svector<theory_var>::const_iterator it = nl_cluster.begin();
|
||||
svector<theory_var>::const_iterator end = nl_cluster.end();
|
||||
for (; it != end; ++it) {
|
||||
theory_var v = *it;
|
||||
for (theory_var v : nl_cluster) {
|
||||
expr * var = var2expr(v);
|
||||
|
||||
if (is_fixed(v)) {
|
||||
|
@ -1905,10 +1886,7 @@ namespace smt {
|
|||
template<typename Ext>
|
||||
void theory_arith<Ext>::init_grobner(svector<theory_var> const & nl_cluster, grobner & gb) {
|
||||
init_grobner_var_order(nl_cluster, gb);
|
||||
svector<theory_var>::const_iterator it = nl_cluster.begin();
|
||||
svector<theory_var>::const_iterator end = nl_cluster.end();
|
||||
for (; it != end; ++it) {
|
||||
theory_var v = *it;
|
||||
for (theory_var v : nl_cluster) {
|
||||
if (is_base(v)) {
|
||||
row const & r = m_rows[get_var_row(v)];
|
||||
add_row_to_gb(r, gb);
|
||||
|
@ -2296,10 +2274,7 @@ namespace smt {
|
|||
eqs.reset();
|
||||
gb.get_equations(eqs);
|
||||
TRACE("grobner_bug", tout << "after gb\n";);
|
||||
ptr_vector<grobner::equation>::const_iterator it = eqs.begin();
|
||||
ptr_vector<grobner::equation>::const_iterator end = eqs.end();
|
||||
for (; it != end; ++it) {
|
||||
grobner::equation * eq = *it;
|
||||
for (grobner::equation* eq : eqs) {
|
||||
TRACE("grobner_bug", gb.display_equation(tout, *eq););
|
||||
if (is_inconsistent(eq, gb))
|
||||
return GB_PROGRESS;
|
||||
|
@ -2310,9 +2285,7 @@ namespace smt {
|
|||
// then assert bounds for x, and continue
|
||||
gb_result result = GB_FAIL;
|
||||
if (m_params.m_nl_arith_gb_eqs) {
|
||||
it = eqs.begin();
|
||||
for (; it != end; ++it) {
|
||||
grobner::equation * eq = *it;
|
||||
for (grobner::equation* eq : eqs) {
|
||||
if (!eq->is_linear_combination()) {
|
||||
TRACE("non_linear", tout << "processing new equality:\n"; gb.display_equation(tout, *eq););
|
||||
TRACE("non_linear_bug", tout << "processing new equality:\n"; gb.display_equation(tout, *eq););
|
||||
|
@ -2331,9 +2304,8 @@ namespace smt {
|
|||
// I only consider linear equations... (HACK)
|
||||
// Moreover, I do not change the weight of a variable more than once in this loop.
|
||||
bool modified = false;
|
||||
it = eqs.begin();
|
||||
for (; it != end; ++it) {
|
||||
grobner::equation const * eq = *it;
|
||||
|
||||
for (grobner::equation const* eq : eqs) {
|
||||
unsigned num_monomials = eq->get_num_monomials();
|
||||
CTRACE("grobner_bug", num_monomials <= 0, gb.display_equation(tout, *eq););
|
||||
if (num_monomials == 0)
|
||||
|
@ -2370,13 +2342,11 @@ namespace smt {
|
|||
bool theory_arith<Ext>::max_min_nl_vars() {
|
||||
var_set already_found;
|
||||
svector<theory_var> vars;
|
||||
for (unsigned j = 0; j < m_nl_monomials.size(); ++j) {
|
||||
theory_var v = m_nl_monomials[j];
|
||||
for (theory_var v : m_nl_monomials) {
|
||||
mark_var(v, vars, already_found);
|
||||
expr * n = var2expr(v);
|
||||
SASSERT(is_pure_monomial(n));
|
||||
for (unsigned i = 0; i < to_app(n)->get_num_args(); i++) {
|
||||
expr * curr = to_app(n)->get_arg(i);
|
||||
for (expr * curr : *to_app(n)) {
|
||||
theory_var v = expr2var(curr);
|
||||
SASSERT(v != null_theory_var);
|
||||
mark_var(v, vars, already_found);
|
||||
|
|
|
@ -18,6 +18,7 @@ Revision History:
|
|||
--*/
|
||||
#include "util/trace.h"
|
||||
#include "util/debug.h"
|
||||
#include "util/memory_manager.h"
|
||||
#include "util/optional.h"
|
||||
|
||||
static void tst1() {
|
||||
|
|
|
@ -63,10 +63,7 @@ class array_map {
|
|||
}
|
||||
|
||||
void really_flush() {
|
||||
typename vector<optional<entry> >::iterator it = m_map.begin();
|
||||
typename vector<optional<entry> >::iterator end = m_map.end();
|
||||
for (; it != end; ++it) {
|
||||
optional<entry> & e = *it;
|
||||
for (optional<entry> & e : m_map) {
|
||||
if (e) {
|
||||
m_plugin.del_eh(e->m_key, e->m_data);
|
||||
e.set_invalid();
|
||||
|
|
|
@ -21,26 +21,27 @@ Revision History:
|
|||
#ifndef OPTIONAL_H_
|
||||
#define OPTIONAL_H_
|
||||
|
||||
template<typename T>
|
||||
template<class T>
|
||||
class optional {
|
||||
char m_obj[sizeof(T)];
|
||||
T* m_obj;
|
||||
char m_initialized;
|
||||
|
||||
void construct(const T & val) {
|
||||
m_initialized = 1;
|
||||
new (reinterpret_cast<void *>(m_obj)) T(val);
|
||||
m_obj = alloc(T, val);
|
||||
}
|
||||
|
||||
void destroy() {
|
||||
if (m_initialized == 1) {
|
||||
reinterpret_cast<T *>(m_obj)->~T();
|
||||
dealloc(m_obj);
|
||||
m_obj = 0;
|
||||
}
|
||||
m_initialized = 0;
|
||||
}
|
||||
|
||||
public:
|
||||
optional():
|
||||
m_initialized(0) {}
|
||||
m_obj(0), m_initialized(0) {}
|
||||
|
||||
explicit optional(const T & val) {
|
||||
construct(val);
|
||||
|
@ -65,7 +66,7 @@ public:
|
|||
|
||||
T * get() const {
|
||||
if (m_initialized == 1) {
|
||||
return reinterpret_cast<T *>(m_obj);
|
||||
return m_obj;
|
||||
}
|
||||
else {
|
||||
return 0;
|
||||
|
@ -80,22 +81,22 @@ public:
|
|||
|
||||
T * operator->() {
|
||||
SASSERT(m_initialized==1);
|
||||
return reinterpret_cast<T *>(m_obj);
|
||||
return m_obj;
|
||||
}
|
||||
|
||||
T const * operator->() const {
|
||||
SASSERT(m_initialized==1);
|
||||
return reinterpret_cast<T const *>(m_obj);
|
||||
return m_obj;
|
||||
}
|
||||
|
||||
const T & operator*() const {
|
||||
SASSERT(m_initialized==1);
|
||||
return *reinterpret_cast<T const*>(m_obj);
|
||||
return *m_obj;
|
||||
}
|
||||
|
||||
T & operator*() {
|
||||
SASSERT(m_initialized==1);
|
||||
return *reinterpret_cast<T *>(m_obj);
|
||||
return *m_obj;
|
||||
}
|
||||
|
||||
optional & operator=(const T & val) {
|
||||
|
|
Loading…
Reference in a new issue