mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-16 13:58:45 +00:00
Code Activity

Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable

Browse source
This commit is contained in:
Leonardo de Moura 2012-11-19 21:31:04 -08:00
parent c9465848dc a20c4ad199
commit 09a62a18c2
15 changed files with 294 additions and 228 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
RELEASE_NOTES
View file

@ -5,6 +5,8 @@ Version 4.3.2
- Added get_version() and get_version_string() to Z3Py
- Added support for FreeBSD. Z3 can be compiled on FreeBSD using g++.
Version 4.3.1
=============

42
configure.ac
View file

@ -101,15 +101,15 @@ AC_PROG_SED
AS_IF([test "$CXX" = "g++"], [
# Enable OpenMP
CXXFLAGS+=" -fopenmp"
LDFLAGS+=" -fopenmp"
SLIBEXTRAFLAGS+=" -fopenmp"
CXXFLAGS="$CXXFLAGS -fopenmp"
LDFLAGS="$LDFLAGS -fopenmp"
SLIBEXTRAFLAGS="$SLIBEXTRAFLAGS -fopenmp"
# Use -mfpmath=sse
CXXFLAGS+=" -mfpmath=sse"
CXXFLAGS="$CXXFLAGS -mfpmath=sse"
],
[test "$CXX" = "clang++"], [
# OpenMP is not supported in clang++
CXXFLAGS+=" -D _NO_OMP_"
CXXFLAGS="$CXXFLAGS -D _NO_OMP_"
],
[
AC_MSG_ERROR([Unsupported compiler: $CXX])
@ -128,28 +128,38 @@ host_os=`uname -s`
AS_IF([test "$host_os" = "Darwin"], [
PLATFORM=osx
SO_EXT=.dylib
SLIBFLAGS+="-dynamiclib"
SLIBFLAGS="$SLIBFLAGS -dynamiclib"
COMP_VERSIONS="-compatibility_version \$(Z3_VERSION) -current_version \$(Z3_VERSION)"
STATIC_FLAGS=
], [test "$host_os" = "Linux"], [
CXXFLAGS=$CXXFLAGS -D _LINUX_
PLATFORM=linux
SO_EXT=.so
LDFLAGS+=" -lrt"
SLIBFLAGS+=" -shared"
LDFLAGS="$LDFLAGS -lrt"
SLIBFLAGS="$SLIBFLAGS -shared"
COMP_VERSIONS=
STATIC_FLAGS=-static
CXXFLAGS+=" -fno-strict-aliasing"
CXXFLAGS="$CXXFLAGS -fno-strict-aliasing"
if test "$CXX" = "clang++"; then
# More flags for clang++ for Linux
CXXFLAGS+=" -Wno-unknown-pragmas -Wno-overloaded-virtual -Wno-unused-value"
CXXFLAGS="$CXXFLAGS -Wno-unknown-pragmas -Wno-overloaded-virtual -Wno-unused-value"
fi
SLIBEXTRAFLAGS+=" -lrt"
SLIBEXTRAFLAGS="$SLIBEXTRAFLAGS -lrt"
], [test "$host_os" = "FreeBSD"], [
CXXFLAGS="$CXXFLAGS -D _FREEBSD_"
PLATFORM=bsd
SO_EXT=.so
LDFLAGS="$LDFLAGS -lrt"
SLIBFLAGS="$SLIBFLAGS -shared"
COMP_VERSIONS=
STATIC_FLAGS=-static
SLIBEXTRAFLAGS="$SLIBEXTRAFLAGS -lrt"
], [test "${host_os:0:6}" = "CYGWIN"], [
PLATFORM=win
SO_EXT=.dll
SLIBFLAGS+="-shared"
SLIBFLAGS="$SLIBFLAGS -shared"
COMP_VERSIONS=
CXXFLAGS+=" -D_CYGWIN -fno-strict-aliasing"
CXXFLAGS="$CXXFLAGS -D_CYGWIN -fno-strict-aliasing"
],
[
AC_MSG_ERROR([Unknown host platform: $host_os])
@ -169,11 +179,11 @@ AC_CHECK_SIZEOF(int *)
if test $ac_cv_sizeof_int_p -eq 8; then
dnl In 64-bit systems we have to compile using -fPIC
CXXFLAGS+=" -fPIC"
CPPFLAGS+=" -D_AMD64_"
CXXFLAGS="$CXXFLAGS -fPIC"
CPPFLAGS="$CPPFLAGS -D_AMD64_"
dnl Only enable use of thread local storage for 64-bit Linux. It is disabled for OSX and 32-bit Linux
if test $PLATFORM = "linux"; then
CPPFLAGS+=" -D_USE_THREAD_LOCAL"
CPPFLAGS="$CPPFLAGS -D_USE_THREAD_LOCAL"
fi
IS_X64="yes"
else

25
src/ast/ast_smt_pp.cpp
View file

@ -29,6 +29,7 @@ Revision History:
#include"vector.h"
#include"for_each_ast.h"
#include"decl_collector.h"
#include"smt2_util.h"
// ---------------------------------------
// smt_renaming
@ -67,32 +68,10 @@ symbol smt_renaming::fix_symbol(symbol s, int k) {
return symbol(buffer.str().c_str());
}
buffer << "|";
if (*data == '|') {
while (*data) {
if (*data == '|') {
if (!data[1]) {
break;
}
buffer << "\\";
}
buffer << *data;
++data;
}
}
else {
while (*data) {
if (*data == '|') {
buffer << "\\";
}
buffer << *data;
++data;
}
}
buffer << mk_smt2_quoted_symbol(s);
if (k > 0) {
buffer << k;
}
buffer << "|";
return symbol(buffer.str().c_str());
}

13
src/muz_qe/dl_context.cpp
View file

@ -1683,7 +1683,8 @@ namespace datalog {
for (unsigned i = 0; i < rules.size(); ++i) {
out << (use_fixedpoint_extensions?"(rule ":"(assert ");
expr* r = rules[i].get();
if (symbol::null != names[i]) {
symbol nm = names[i];
if (symbol::null != nm) {
out << "(! ";
}
if (use_fixedpoint_extensions) {
@ -1692,8 +1693,14 @@ namespace datalog {
else {
out << mk_smt_pp(r, m);
}
if (symbol::null != names[i]) {
out << " :named " << names[i] << ")";
if (symbol::null != nm) {
while (fresh_names.contains(nm)) {
std::ostringstream s;
s << nm << "!";
nm = symbol(s.str().c_str());
}
fresh_names.add(nm);
out << " :named " << nm << ")";
}
out << ")\n";
}

23
src/muz_qe/pdr_tactic.cpp → src/muz_qe/horn_tactic.cpp
View file

@ -3,11 +3,11 @@ Copyright (c) 2012 Microsoft Corporation
Module Name:
pdr_tactic.h
horn_tactic.h
Abstract:
PDR as a tactic to solve Horn clauses.
HORN as a tactic to solve Horn clauses.
Author:
@ -19,10 +19,10 @@ Revision History:
#include"tactical.h"
#include"model_converter.h"
#include"proof_converter.h"
#include"pdr_tactic.h"
#include"horn_tactic.h"
#include"dl_context.h"
class pdr_tactic : public tactic {
class horn_tactic : public tactic {
struct imp {
ast_manager& m;
datalog::context m_ctx;
@ -139,7 +139,7 @@ class pdr_tactic : public tactic {
expr_dependency_ref & core) {
SASSERT(g->is_well_sorted());
mc = 0; pc = 0; core = 0;
tactic_report report("pdr", *g);
tactic_report report("horn", *g);
bool produce_models = g->models_enabled();
bool produce_proofs = g->proofs_enabled();
@ -174,6 +174,7 @@ class pdr_tactic : public tactic {
if (queries.size() != 1) {
q = m.mk_fresh_const("query", m.mk_bool_sort());
register_predicate(q);
for (unsigned i = 0; i < queries.size(); ++i) {
f = mk_rule(queries[i].get(), q);
m_ctx.add_rule(f, symbol::null);
@ -209,7 +210,7 @@ class pdr_tactic : public tactic {
// subgoal is unchanged.
break;
}
TRACE("pdr", g->display(tout););
TRACE("horn", g->display(tout););
SASSERT(g->is_well_sorted());
}
};
@ -217,16 +218,16 @@ class pdr_tactic : public tactic {
params_ref m_params;
imp * m_imp;
public:
pdr_tactic(ast_manager & m, params_ref const & p):
horn_tactic(ast_manager & m, params_ref const & p):
m_params(p) {
m_imp = alloc(imp, m, p);
}
virtual tactic * translate(ast_manager & m) {
return alloc(pdr_tactic, m, m_params);
return alloc(horn_tactic, m, m_params);
}
virtual ~pdr_tactic() {
virtual ~horn_tactic() {
dealloc(m_imp);
}
@ -280,7 +281,7 @@ protected:
}
};
tactic * mk_pdr_tactic(ast_manager & m, params_ref const & p) {
return clean(alloc(pdr_tactic, m, p));
tactic * mk_horn_tactic(ast_manager & m, params_ref const & p) {
return clean(alloc(horn_tactic, m, p));
}

10
src/muz_qe/pdr_tactic.h → src/muz_qe/horn_tactic.h
View file

@ -3,7 +3,7 @@ Copyright (c) 2012 Microsoft Corporation
Module Name:
pdr_tactic.h
horn_tactic.h
Abstract:
@ -16,15 +16,15 @@ Author:
Revision History:
--*/
#ifndef _PDR_TACTIC_H_
#define _PDR_TACTIC_H_
#ifndef _HORN_TACTIC_H_
#define _HORN_TACTIC_H_
#include"params.h"
class ast_manager;
class tactic;
tactic * mk_pdr_tactic(ast_manager & m, params_ref const & p = params_ref());
tactic * mk_horn_tactic(ast_manager & m, params_ref const & p = params_ref());
/*
ADD_TACTIC("pdr", "apply pdr for horn clauses.", "mk_pdr_tactic(m, p)")
ADD_TACTIC("horn", "apply tactic for horn clauses.", "mk_horn_tactic(m, p)")
*/
#endif

2
src/muz_qe/model2expr.h
View file

@ -35,7 +35,9 @@ class mk_fresh_name {
public:
mk_fresh_name(): m_char('A'), m_num(0) {}
void add(ast* a);
void add(symbol const& s) { m_symbols.insert(s); }
symbol next();
bool contains(symbol const& s) const { return m_symbols.contains(s); }
};

29
src/muz_qe/pdr_prop_solver.cpp
View file

@ -26,6 +26,7 @@ Revision History:
#include "model_pp.h"
#include "front_end_params.h"
#include "datatype_decl_plugin.h"
#include "bv_decl_plugin.h"
#include "pdr_farkas_learner.h"
#include "ast_smt2_pp.h"
#include "expr_replacer.h"
@ -94,9 +95,12 @@ namespace pdr {
void expand_literals(expr_ref_vector& conjs) {
arith_util arith(m);
datatype_util dt(m);
bv_util bv(m);
expr* e1, *e2, *c, *val;
for (unsigned i = 0; i < conjs.size(); ++i) {
rational r;
unsigned bv_size;
for (unsigned i = 0; i < conjs.size(); ++i) {
expr* e = conjs[i].get();
if (m.is_eq(e, e1, e2) && arith.is_int_real(e1)) {
conjs[i] = arith.mk_le(e1,e2);
@ -109,7 +113,8 @@ namespace pdr {
}
++i;
}
else if (m.is_eq(e, c, val) && is_app(val) && dt.is_constructor(to_app(val))) {
else if ((m.is_eq(e, c, val) && is_app(val) && dt.is_constructor(to_app(val))) ||
(m.is_eq(e, val, c) && is_app(val) && dt.is_constructor(to_app(val)))){
func_decl* f = to_app(val)->get_decl();
func_decl* r = dt.get_constructor_recognizer(f);
conjs[i] = m.mk_app(r,c);
@ -118,6 +123,24 @@ namespace pdr {
conjs.push_back(m.mk_eq(m.mk_app(acc[i], c), to_app(val)->get_arg(i)));
}
}
else if ((m.is_eq(e, c, val) && bv.is_numeral(val, r, bv_size)) ||
(m.is_eq(e, val, c) && bv.is_numeral(val, r, bv_size))) {
rational two(2);
for (unsigned j = 0; j < bv_size; ++j) {
parameter p(j);
expr* e = m.mk_app(bv.get_family_id(), OP_BIT2BOOL, 1, &p, 1, &c);
if ((r % two).is_zero()) {
e = m.mk_not(e);
}
r = div(r, two);
if (j == 0) {
conjs[i] = e;
}
else {
conjs.push_back(e);
}
}
}
}
}
@ -341,7 +364,7 @@ namespace pdr {
}
fl.get_lemmas(pr, bs, lemmas);
safe.elim_proxies(lemmas);
fl.simplify_lemmas(lemmas); // redundant
fl.simplify_lemmas(lemmas); // redundant?
if (m_fparams.m_arith_mode == AS_DIFF_LOGIC &&
!is_difference_logic(m, lemmas.size(), lemmas.c_ptr())) {
IF_VERBOSE(1,

15
src/muz_qe/qe_lite.cpp
View file

@ -342,17 +342,22 @@ class der2 {
void apply_substitution(quantifier * q, expr_ref & r) {
expr * e = q->get_expr();
unsigned num_args = to_app(e)->get_num_args();
unsigned num_args = 1;
expr* const* args = &e;
if ((q->is_forall() && m.is_or(e)) ||
(q->is_exists() && m.is_and(e))) {
num_args = to_app(e)->get_num_args();
args = to_app(e)->get_args();
}
bool_rewriter rw(m);
// get a new expression
m_new_args.reset();
for(unsigned i = 0; i < num_args; i++) {
int x = m_pos2var[i];
if (x != -1 && m_map[x] != 0)
continue; // this is a disequality/equality with definition (vanishes)
m_new_args.push_back(to_app(e)->get_arg(i));
if (x == -1 || m_map[x] == 0) {
m_new_args.push_back(args[i]);
}
}
expr_ref t(m);

2
src/tactic/fpa/fpa2bv_converter.h
View file

@ -197,4 +197,4 @@ protected:
void convert(model * bv_mdl, model * float_mdl);
};
#endif
#endif

166
src/tactic/fpa/fpa2bv_rewriter.h Normal file
View file

@ -0,0 +1,166 @@
/*++
Copyright (c) 2012 Microsoft Corporation
Module Name:
fpa2bv_rewriter.h
Abstract:
Rewriter for converting FPA to BV
Author:
Christoph (cwinter) 2012-02-09
Notes:
--*/
#ifndef _FPA2BV_REWRITER_H_
#define _FPA2BV_REWRITER_H_
#include"cooperate.h"
#include"rewriter_def.h"
#include"bv_decl_plugin.h"
#include"fpa2bv_converter.h"
struct fpa2bv_rewriter_cfg : public default_rewriter_cfg {
ast_manager & m_manager;
expr_ref_vector m_out;
fpa2bv_converter & m_conv;
unsigned long long m_max_memory;
unsigned m_max_steps;
ast_manager & m() const { return m_manager; }
fpa2bv_rewriter_cfg(ast_manager & m, fpa2bv_converter & c, params_ref const & p):
m_manager(m),
m_out(m),
m_conv(c) {
updt_params(p);
// We need to make sure that the mananger has the BV plugin loaded.
symbol s_bv("bv");
if (!m_manager.has_plugin(s_bv))
m_manager.register_plugin(s_bv, alloc(bv_decl_plugin));
}
~fpa2bv_rewriter_cfg() {
}
void cleanup_buffers() {
m_out.finalize();
}
void updt_params(params_ref const & p) {
m_max_memory = megabytes_to_bytes(p.get_uint(":max-memory", UINT_MAX));
m_max_steps = p.get_uint(":max-steps", UINT_MAX);
}
bool max_steps_exceeded(unsigned num_steps) const {
cooperate("fpa2bv");
if (memory::get_allocation_size() > m_max_memory)
throw tactic_exception(TACTIC_MAX_MEMORY_MSG);
return num_steps > m_max_steps;
}
br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) {
TRACE("fpa2bv_rw", tout << "APP: " << f->get_name() << std::endl; );
if (num == 0 && f->get_family_id() == null_family_id && m_conv.is_float(f->get_range())) {
m_conv.mk_const(f, result);
return BR_DONE;
}
if (num == 0 && f->get_family_id() == null_family_id && m_conv.is_rm_sort(f->get_range())) {
m_conv.mk_rm_const(f, result);
return BR_DONE;
}
if (m().is_eq(f)) {
SASSERT(num == 2);
if (m_conv.is_float(args[0])) {
m_conv.mk_eq(args[0], args[1], result);
return BR_DONE;
}
return BR_FAILED;
}
if (m().is_ite(f)) {
SASSERT(num == 3);
if (m_conv.is_float(args[1])) {
m_conv.mk_ite(args[0], args[1], args[2], result);
return BR_DONE;
}
return BR_FAILED;
}
if (m_conv.is_float_family(f)) {
switch (f->get_decl_kind()) {
case OP_RM_NEAREST_TIES_TO_AWAY:
case OP_RM_NEAREST_TIES_TO_EVEN:
case OP_RM_TOWARD_NEGATIVE:
case OP_RM_TOWARD_POSITIVE:
case OP_RM_TOWARD_ZERO: m_conv.mk_rounding_mode(f, result); return BR_DONE;
case OP_FLOAT_VALUE: m_conv.mk_value(f, num, args, result); return BR_DONE;
case OP_FLOAT_PLUS_INF: m_conv.mk_plus_inf(f, result); return BR_DONE;
case OP_FLOAT_MINUS_INF: m_conv.mk_minus_inf(f, result); return BR_DONE;
case OP_FLOAT_NAN: m_conv.mk_nan(f, result); return BR_DONE;
case OP_FLOAT_ADD: m_conv.mk_add(f, num, args, result); return BR_DONE;
case OP_FLOAT_SUB: m_conv.mk_sub(f, num, args, result); return BR_DONE;
case OP_FLOAT_UMINUS: m_conv.mk_uminus(f, num, args, result); return BR_DONE;
case OP_FLOAT_MUL: m_conv.mk_mul(f, num, args, result); return BR_DONE;
case OP_FLOAT_DIV: m_conv.mk_div(f, num, args, result); return BR_DONE;
case OP_FLOAT_REM: m_conv.mk_remainder(f, num, args, result); return BR_DONE;
case OP_FLOAT_ABS: m_conv.mk_abs(f, num, args, result); return BR_DONE;
case OP_FLOAT_MIN: m_conv.mk_min(f, num, args, result); return BR_DONE;
case OP_FLOAT_MAX: m_conv.mk_max(f, num, args, result); return BR_DONE;
case OP_FLOAT_FUSED_MA: m_conv.mk_fusedma(f, num, args, result); return BR_DONE;
case OP_FLOAT_SQRT: m_conv.mk_sqrt(f, num, args, result); return BR_DONE;
case OP_FLOAT_ROUND_TO_INTEGRAL: m_conv.mk_round_to_integral(f, num, args, result); return BR_DONE;
case OP_FLOAT_EQ: m_conv.mk_float_eq(f, num, args, result); return BR_DONE;
case OP_FLOAT_LT: m_conv.mk_float_lt(f, num, args, result); return BR_DONE;
case OP_FLOAT_GT: m_conv.mk_float_gt(f, num, args, result); return BR_DONE;
case OP_FLOAT_LE: m_conv.mk_float_le(f, num, args, result); return BR_DONE;
case OP_FLOAT_GE: m_conv.mk_float_ge(f, num, args, result); return BR_DONE;
case OP_FLOAT_IS_ZERO: m_conv.mk_is_zero(f, num, args, result); return BR_DONE;
case OP_FLOAT_IS_NZERO: m_conv.mk_is_nzero(f, num, args, result); return BR_DONE;
case OP_FLOAT_IS_PZERO: m_conv.mk_is_pzero(f, num, args, result); return BR_DONE;
case OP_FLOAT_IS_SIGN_MINUS: m_conv.mk_is_sign_minus(f, num, args, result); return BR_DONE;
case OP_TO_FLOAT: m_conv.mk_to_float(f, num, args, result); return BR_DONE;
default:
TRACE("fpa2bv", tout << "unsupported operator: " << f->get_name() << "\n";
for (unsigned i = 0; i < num; i++) tout << mk_ismt2_pp(args[i], m()) << std::endl;);
throw tactic_exception("NYI");
}
}
return BR_FAILED;
}
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) {
return false;
}
bool reduce_var(var * t, expr_ref & result, proof_ref & result_pr) {
return false;
}
};
template class rewriter_tpl<fpa2bv_rewriter_cfg>;
struct fpa2bv_rewriter : public rewriter_tpl<fpa2bv_rewriter_cfg> {
fpa2bv_rewriter_cfg m_cfg;
fpa2bv_rewriter(ast_manager & m, fpa2bv_converter & c, params_ref const & p):
rewriter_tpl<fpa2bv_rewriter_cfg>(m, m.proofs_enabled(), m_cfg),
m_cfg(m, c, p) {
}
};
#endif

148
src/tactic/fpa/fpa2bv_tactic.cpp
View file

@ -17,156 +17,10 @@ Notes:
--*/
#include"tactical.h"
#include"rewriter_def.h"
#include"cooperate.h"
#include"ref_util.h"
#include"bv_decl_plugin.h"
#include"float_decl_plugin.h"
#include"fpa2bv_converter.h"
#include"tactical.h"
#include"fpa2bv_rewriter.h"
#include"simplify_tactic.h"
#include"fpa2bv_tactic.h"
struct fpa2bv_rewriter_cfg : public default_rewriter_cfg {
ast_manager & m_manager;
expr_ref_vector m_out;
fpa2bv_converter & m_conv;
unsigned long long m_max_memory;
unsigned m_max_steps;
ast_manager & m() const { return m_manager; }
fpa2bv_rewriter_cfg(ast_manager & m, fpa2bv_converter & c, params_ref const & p):
m_manager(m),
m_out(m),
m_conv(c) {
updt_params(p);
// We need to make sure that the mananger has the BV plugin loaded.
symbol s_bv("bv");
if (!m_manager.has_plugin(s_bv))
m_manager.register_plugin(s_bv, alloc(bv_decl_plugin));
}
~fpa2bv_rewriter_cfg() {
}
void cleanup_buffers() {
m_out.finalize();
}
void updt_params(params_ref const & p) {
m_max_memory = megabytes_to_bytes(p.get_uint(":max-memory", UINT_MAX));
m_max_steps = p.get_uint(":max-steps", UINT_MAX);
}
bool max_steps_exceeded(unsigned num_steps) const {
cooperate("fpa2bv");
if (memory::get_allocation_size() > m_max_memory)
throw tactic_exception(TACTIC_MAX_MEMORY_MSG);
return num_steps > m_max_steps;
}
br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) {
TRACE("fpa2bv_rw", tout << "APP: " << f->get_name() << std::endl; );
if (num == 0 && f->get_family_id() == null_family_id && m_conv.is_float(f->get_range())) {
m_conv.mk_const(f, result);
return BR_DONE;
}
if (num == 0 && f->get_family_id() == null_family_id && m_conv.is_rm_sort(f->get_range())) {
m_conv.mk_rm_const(f, result);
return BR_DONE;
}
if (m().is_eq(f)) {
SASSERT(num == 2);
if (m_conv.is_float(args[0])) {
m_conv.mk_eq(args[0], args[1], result);
return BR_DONE;
}
return BR_FAILED;
}
if (m().is_ite(f)) {
SASSERT(num == 3);
if (m_conv.is_float(args[1])) {
m_conv.mk_ite(args[0], args[1], args[2], result);
return BR_DONE;
}
return BR_FAILED;
}
if (m_conv.is_float_family(f)) {
switch (f->get_decl_kind()) {
case OP_RM_NEAREST_TIES_TO_AWAY:
case OP_RM_NEAREST_TIES_TO_EVEN:
case OP_RM_TOWARD_NEGATIVE:
case OP_RM_TOWARD_POSITIVE:
case OP_RM_TOWARD_ZERO: m_conv.mk_rounding_mode(f, result); return BR_DONE;
case OP_FLOAT_VALUE: m_conv.mk_value(f, num, args, result); return BR_DONE;
case OP_FLOAT_PLUS_INF: m_conv.mk_plus_inf(f, result); return BR_DONE;
case OP_FLOAT_MINUS_INF: m_conv.mk_minus_inf(f, result); return BR_DONE;
case OP_FLOAT_NAN: m_conv.mk_nan(f, result); return BR_DONE;
case OP_FLOAT_ADD: m_conv.mk_add(f, num, args, result); return BR_DONE;
case OP_FLOAT_SUB: m_conv.mk_sub(f, num, args, result); return BR_DONE;
case OP_FLOAT_UMINUS: m_conv.mk_uminus(f, num, args, result); return BR_DONE;
case OP_FLOAT_MUL: m_conv.mk_mul(f, num, args, result); return BR_DONE;
case OP_FLOAT_DIV: m_conv.mk_div(f, num, args, result); return BR_DONE;
case OP_FLOAT_REM: m_conv.mk_remainder(f, num, args, result); return BR_DONE;
case OP_FLOAT_ABS: m_conv.mk_abs(f, num, args, result); return BR_DONE;
case OP_FLOAT_MIN: m_conv.mk_min(f, num, args, result); return BR_DONE;
case OP_FLOAT_MAX: m_conv.mk_max(f, num, args, result); return BR_DONE;
case OP_FLOAT_FUSED_MA: m_conv.mk_fusedma(f, num, args, result); return BR_DONE;
case OP_FLOAT_SQRT: m_conv.mk_sqrt(f, num, args, result); return BR_DONE;
case OP_FLOAT_ROUND_TO_INTEGRAL: m_conv.mk_round_to_integral(f, num, args, result); return BR_DONE;
case OP_FLOAT_EQ: m_conv.mk_float_eq(f, num, args, result); return BR_DONE;
case OP_FLOAT_LT: m_conv.mk_float_lt(f, num, args, result); return BR_DONE;
case OP_FLOAT_GT: m_conv.mk_float_gt(f, num, args, result); return BR_DONE;
case OP_FLOAT_LE: m_conv.mk_float_le(f, num, args, result); return BR_DONE;
case OP_FLOAT_GE: m_conv.mk_float_ge(f, num, args, result); return BR_DONE;
case OP_FLOAT_IS_ZERO: m_conv.mk_is_zero(f, num, args, result); return BR_DONE;
case OP_FLOAT_IS_NZERO: m_conv.mk_is_nzero(f, num, args, result); return BR_DONE;
case OP_FLOAT_IS_PZERO: m_conv.mk_is_pzero(f, num, args, result); return BR_DONE;
case OP_FLOAT_IS_SIGN_MINUS: m_conv.mk_is_sign_minus(f, num, args, result); return BR_DONE;
case OP_TO_FLOAT: m_conv.mk_to_float(f, num, args, result); return BR_DONE;
default:
TRACE("fpa2bv", tout << "unsupported operator: " << f->get_name() << "\n";
for (unsigned i = 0; i < num; i++) tout << mk_ismt2_pp(args[i], m()) << std::endl;);
throw tactic_exception("NYI");
}
}
return BR_FAILED;
}
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) {
return false;
}
bool reduce_var(var * t, expr_ref & result, proof_ref & result_pr) {
return false;
}
};
template class rewriter_tpl<fpa2bv_rewriter_cfg>;
struct fpa2bv_rewriter : public rewriter_tpl<fpa2bv_rewriter_cfg> {
fpa2bv_rewriter_cfg m_cfg;
fpa2bv_rewriter(ast_manager & m, fpa2bv_converter & c, params_ref const & p):
rewriter_tpl<fpa2bv_rewriter_cfg>(m, m.proofs_enabled(), m_cfg),
m_cfg(m, c, p) {
}
};
class fpa2bv_tactic : public tactic {
struct imp {
ast_manager & m;

2
src/tactic/fpa/qffpa_tactic.cpp
View file

@ -35,4 +35,4 @@ tactic * mk_qffpa_tactic(ast_manager & m, params_ref const & p) {
using_params(mk_simplify_tactic(m, p), sat_simp_p),
mk_sat_tactic(m, p),
mk_fail_if_undecided_tactic());
}
}

4
src/tactic/portfolio/smt_strategic_solver.cpp
View file

@ -33,7 +33,7 @@ Notes:
#include"default_tactic.h"
#include"ufbv_tactic.h"
#include"qffpa_tactic.h"
#include"pdr_tactic.h"
#include"horn_tactic.h"
#include"smt_solver.h"
MK_SIMPLE_TACTIC_FACTORY(qfuf_fct, mk_qfuf_tactic(m, p));
@ -55,7 +55,7 @@ MK_SIMPLE_TACTIC_FACTORY(qfnia_fct, mk_qfnia_tactic(m, p));
MK_SIMPLE_TACTIC_FACTORY(qfnra_fct, mk_qfnra_tactic(m, p));
MK_SIMPLE_TACTIC_FACTORY(qffpa_fct, mk_qffpa_tactic(m, p));
MK_SIMPLE_TACTIC_FACTORY(ufbv_fct, mk_ufbv_tactic(m, p));
MK_SIMPLE_TACTIC_FACTORY(horn_fct, mk_pdr_tactic(m, p));
MK_SIMPLE_TACTIC_FACTORY(horn_fct, mk_horn_tactic(m, p));
static void init(strategic_solver * s) {
s->set_default_tactic(alloc(default_fct));

39
src/util/scoped_timer.cpp
View file

@ -33,15 +33,22 @@ Revision History:
#include<sys/time.h>
#include<sys/errno.h>
#include<pthread.h>
#else
#elif defined(_LINUX_) || defined(_FREEBSD_)
// Linux
#include<csignal>
#include<ctime>
#include<memory.h>
#include"warning.h"
#define CLOCKID CLOCK_PROCESS_CPUTIME_ID
#ifdef _LINUX_
#define CLOCKID CLOCK_PROCESS_CPUTIME_ID
#else
// FreeBSD does not support CLOCK_PROCESS_CPUTIME_ID
#define CLOCKID CLOCK_PROF
#endif
#define SIG SIGRTMIN
// ---------
#else
// Other platforms
#endif
#include"scoped_timer.h"
@ -63,12 +70,14 @@ struct scoped_timer::imp {
pthread_attr_t m_attributes;
unsigned m_interval;
pthread_cond_t m_condition_var;
#else
// Linux
#elif defined(_LINUX_) || defined(_FREEBSD_)
// Linux & FreeBSD
static void * g_timer;
void (*m_old_handler)(int);
void * m_old_timer;
timer_t m_timerid;
#else
// Other
#endif
#if defined(_WINDOWS) || defined(_CYGWIN)
@ -117,10 +126,12 @@ struct scoped_timer::imp {
throw default_exception("failed to destroy pthread condition variable");
return st;
}
#else
#elif defined(_LINUX_) || defined(_FREEBSD_)
static void sig_handler(int) {
static_cast<imp*>(g_timer)->m_eh->operator()();
}
#else
// Other
#endif
@ -142,8 +153,8 @@ struct scoped_timer::imp {
throw default_exception("failed to initialize timer thread attributes");
if (pthread_create(&m_thread_id, &m_attributes, &thread_func, this) != 0)
throw default_exception("failed to start timer thread");
#else
// Linux version
#elif defined(_LINUX_) || defined(_FREEBSD_)
// Linux & FreeBSD
if (omp_in_parallel()) {
// It doesn't work in with more than one thread.
// SIGEV_SIGNAL: the event is handled by the process not by the thread that installed the handler.
@ -172,6 +183,8 @@ struct scoped_timer::imp {
its.it_interval.tv_nsec = 0;
if (timer_settime(m_timerid, 0, &its, NULL) == -1)
throw default_exception("failed to set timer");
#else
// Other platforms
#endif
}
@ -187,14 +200,16 @@ struct scoped_timer::imp {
throw default_exception("failed to join thread");
if (pthread_attr_destroy(&m_attributes) != 0)
throw default_exception("failed to destroy pthread attributes object");
#else
// Linux version
#elif defined(_LINUX_) || defined(_FREEBSD_)
// Linux & FreeBSD
if (omp_in_parallel())
return; // see comments in the constructor.
timer_delete(m_timerid);
if (m_old_handler != SIG_ERR)
signal(SIG, m_old_handler);
g_timer = m_old_timer;
#else
// Other Platforms
#endif
}
@ -203,9 +218,11 @@ struct scoped_timer::imp {
#if defined(_WINDOWS) || defined(_CYGWIN)
#elif defined(__APPLE__) && defined(__MACH__)
// Mac OS X
#else
// Linux
#elif defined(_LINUX_) || defined(_FREEBSD_)
// Linux & FreeBSD
void * scoped_timer::imp::g_timer = 0;
#else
// Other platforms
#endif
scoped_timer::scoped_timer(unsigned ms, event_handler * eh) {