mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 08:35:31 +00:00
Code Activity

merged changes from unstable

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2012-11-21 12:41:52 -08:00
commit 6679fc4c0b
46 changed files with 3598 additions and 655 deletions
Download patch file Download diff file Expand all files Collapse all files

17
src/api/api_datalog.cpp
View file

@ -449,6 +449,23 @@ extern "C" {
RETURN_Z3(of_ast_vector(v));
Z3_CATCH_RETURN(0);
}
Z3_ast_vector Z3_API Z3_fixedpoint_get_assertions(
Z3_context c,
Z3_fixedpoint d)
{
Z3_TRY;
LOG_Z3_fixedpoint_get_assertions(c, d);
ast_manager& m = mk_c(c)->m();
Z3_ast_vector_ref* v = alloc(Z3_ast_vector_ref, m);
mk_c(c)->save_object(v);
unsigned num_asserts = to_fixedpoint_ref(d)->ctx().get_num_assertions();
for (unsigned i = 0; i < num_asserts; ++i) {
v->m_ast_vector.push_back(to_fixedpoint_ref(d)->ctx().get_assertion(i));
}
RETURN_Z3(of_ast_vector(v));
Z3_CATCH_RETURN(0);
}
void Z3_API Z3_fixedpoint_set_reduce_assign_callback(
Z3_context c, Z3_fixedpoint d, Z3_fixedpoint_reduce_assign_callback_fptr f) {

17
src/api/dotnet/Fixedpoint.cs
View file

@ -278,6 +278,23 @@ namespace Microsoft.Z3
}
}
/// <summary>
/// Retrieve set of assertions added to fixedpoint context.
/// </summary>
public BoolExpr[] Assertions {
get
{
Contract.Ensures(Contract.Result<BoolExpr[]>() != null);
ASTVector v = new ASTVector(Context, Native.Z3_fixedpoint_get_assertions(Context.nCtx, NativeObject));
uint n = v.Size;
BoolExpr[] res = new BoolExpr[n];
for (uint i = 0; i < n; i++)
res[i] = new BoolExpr(Context, v[i].NativeObject);
return res;
}
}
#region Internal
internal Fixedpoint(Context ctx, IntPtr obj)

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

@ -6145,7 +6145,11 @@ class Fixedpoint(Z3PPObject):
def get_rules(self):
"""retrieve rules that have been added to fixedpoint context"""
return AstVector(Z3_fixedpoint_get_rules(self.ctx.ref(), self.fixedpoint), self.ctx)
def get_assertions(self):
"""retrieve assertions that have been added to fixedpoint context"""
return AstVector(Z3_fixedpoint_get_assertions(self.ctx.ref(), self.fixedpoint), self.ctx)
def __repr__(self):
"""Return a formatted string with all added rules and constraints."""
return self.sexpr()

11
src/api/z3_api.h
View file

@ -5535,7 +5535,7 @@ END_MLAPI_EXCLUDE
of sorts in the domain of \c r. Each sort in the domain should be an integral
(bit-vector, Boolean or or finite domain sort).
The call has the same effect as adding a rule where \r is applied to the arguments.
The call has the same effect as adding a rule where \c r is applied to the arguments.
def_API('Z3_fixedpoint_add_fact', VOID, (_in(CONTEXT), _in(FIXEDPOINT), _in(FUNC_DECL), _in(UINT), _in_array(3, UINT)))
*/
@ -5696,6 +5696,15 @@ END_MLAPI_EXCLUDE
__in Z3_context c,
__in Z3_fixedpoint f);
/**
\brief Retrieve set of background assertions from fixedpoint context.
def_API('Z3_fixedpoint_get_assertions', AST_VECTOR, (_in(CONTEXT),_in(FIXEDPOINT)))
*/
Z3_ast_vector Z3_API Z3_fixedpoint_get_assertions(
__in Z3_context c,
__in Z3_fixedpoint f);
/**
\brief Set parameters on fixedpoint context.

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

8
src/cmd_context/cmd_context.cpp
View file

@ -306,7 +306,7 @@ cmd_context::cmd_context(front_end_params * params, bool main_ctx, ast_manager *
m_params_owner(params == 0),
m_logic(l),
m_interactive_mode(false),
m_global_decls(!this->params().m_smtlib2_compliant), // SMTLIB 2.0 uses scoped decls.
m_global_decls(false), // :global-decls is false by default.
m_print_success(false), // params.m_smtlib2_compliant),
m_random_seed(0),
m_produce_unsat_cores(false),
@ -477,7 +477,8 @@ bool cmd_context::logic_has_bv_core(symbol const & s) const {
s == "QF_UFBV" ||
s == "QF_ABV" ||
s == "QF_AUFBV" ||
s == "QF_BVRE";
s == "QF_BVRE" ||
s == "HORN";
}
bool cmd_context::logic_has_horn(symbol const& s) const {
@ -518,7 +519,8 @@ bool cmd_context::logic_has_array_core(symbol const & s) const {
s == "AUFBV" ||
s == "ABV" ||
s == "QF_ABV" ||
s == "QF_AUFBV";
s == "QF_AUFBV" ||
s == "HORN";
}
bool cmd_context::logic_has_array() const {

2
src/muz_qe/dl_cmds.cpp
View file

@ -315,7 +315,7 @@ private:
if (m_params.get_bool(":print-certificate", false)) {
datalog::context& dlctx = m_dl_ctx->dlctx();
if (!dlctx.display_certificate(ctx.regular_stream())) {
throw cmd_exception("certificates are not supported for selected DL_ENGINE");
throw cmd_exception("certificates are not supported for the selected engine");
}
ctx.regular_stream() << "\n";
}

37
src/muz_qe/dl_context.cpp
View file

@ -238,6 +238,7 @@ namespace datalog {
m_pinned(m),
m_vars(m),
m_rule_set(*this),
m_rule_fmls(m),
m_background(m),
m_closed(false),
m_saturation_was_run(false),
@ -521,10 +522,19 @@ namespace datalog {
}
void context::add_rule(expr* rl, symbol const& name) {
m_rule_fmls.push_back(rl);
m_rule_names.push_back(name);
}
void context::flush_add_rules() {
datalog::rule_manager& rm = get_rule_manager();
datalog::rule_ref_vector rules(rm);
rm.mk_rule(rl, rules, name);
for (unsigned i = 0; i < m_rule_fmls.size(); ++i) {
rm.mk_rule(m_rule_fmls[i].get(), rules, m_rule_names[i]);
}
add_rules(rules);
m_rule_fmls.reset();
m_rule_names.reset();
}
//
@ -1223,6 +1233,7 @@ namespace datalog {
}
void context::new_query() {
flush_add_rules();
if (m_last_result_relation) {
m_last_result_relation->deallocate();
m_last_result_relation = 0;
@ -1512,7 +1523,7 @@ namespace datalog {
switch(get_engine()) {
case DATALOG_ENGINE:
return false;
case PDR_ENGINE:
case QPDR_ENGINE:
ensure_pdr();
m_pdr->display_certificate(out);
return true;
@ -1618,6 +1629,10 @@ namespace datalog {
names.push_back((*it)->name());
}
}
for (unsigned i = 0; i < m_rule_fmls.size(); ++i) {
rules.push_back(m_rule_fmls[i].get());
names.push_back(m_rule_names[i]);
}
smt2_pp_environment_dbg env(m);
pp_params params;
@ -1674,8 +1689,11 @@ namespace datalog {
declare_vars(rules, fresh_names, out);
}
if (num_axioms > 0 && !use_fixedpoint_extensions) {
throw default_exception("Background axioms cannot be used with SMT-LIB2 HORN format");
}
for (unsigned i = 0; i < num_axioms; ++i) {
SASSERT(use_fixedpoint_extensions);
out << "(assert ";
ast_smt2_pp(out, axioms[i], env, params);
out << ")\n";
@ -1683,7 +1701,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 +1711,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";
}

6
src/muz_qe/dl_context.h
View file

@ -96,6 +96,8 @@ namespace datalog {
pred2syms m_argument_var_names;
decl_set m_output_preds;
rule_set m_rule_set;
expr_ref_vector m_rule_fmls;
svector<symbol> m_rule_names;
expr_ref_vector m_background;
scoped_ptr<pdr::dl_interface> m_pdr;
@ -259,6 +261,8 @@ namespace datalog {
void assert_expr(expr* e);
expr_ref get_background_assertion();
unsigned get_num_assertions() { return m_background.size(); }
expr* get_assertion(unsigned i) const { return m_background[i]; }
/**
Method exposed from API for adding rules.
@ -454,6 +458,8 @@ namespace datalog {
private:
void flush_add_rules();
void ensure_pdr();
void ensure_bmc();

1
src/muz_qe/dl_mk_rule_inliner.cpp
View file

@ -194,6 +194,7 @@ namespace datalog {
}
}
// TBD: replace by r.has_quantifiers() and test
bool mk_rule_inliner::has_quantifier(rule const& r) const {
unsigned utsz = r.get_uninterpreted_tail_size();
for (unsigned i = utsz; i < r.get_tail_size(); ++i) {

5
src/muz_qe/dl_mk_slice.cpp
View file

@ -818,6 +818,11 @@ namespace datalog {
}
rule_set * mk_slice::operator()(rule_set const & src, model_converter_ref& mc, proof_converter_ref& pc) {
for (unsigned i = 0; i < src.get_num_rules(); ++i) {
if (src.get_rule(i)->has_quantifiers()) {
return 0;
}
}
ref<slice_proof_converter> spc;
ref<slice_model_converter> smc;
if (pc) {

46
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;
@ -90,6 +90,24 @@ class pdr_tactic : public tactic {
m_ctx.register_predicate(to_app(a)->get_decl(), true);
}
void check_predicate(expr* a) {
expr* a1 = 0;
while (true) {
if (is_quantifier(a)) {
a = to_quantifier(a)->get_expr();
continue;
}
if (m.is_not(a, a1)) {
a = a1;
continue;
}
if (is_predicate(a)) {
register_predicate(a);
}
break;
}
}
enum formula_kind { IS_RULE, IS_QUERY, IS_NONE };
formula_kind get_formula_kind(expr_ref& f) {
@ -99,13 +117,12 @@ class pdr_tactic : public tactic {
expr* a = 0, *a1 = 0;
datalog::flatten_or(f, args);
for (unsigned i = 0; i < args.size(); ++i) {
a = args[i].get();
a = args[i].get();
check_predicate(a);
if (m.is_not(a, a1) && is_predicate(a1)) {
register_predicate(a1);
body.push_back(a1);
}
else if (is_predicate(a)) {
register_predicate(a);
if (head) {
return IS_NONE;
}
@ -139,7 +156,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 +191,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 +227,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 +235,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 +298,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,

31
src/muz_qe/qe_lite.cpp
View file

@ -340,19 +340,32 @@ class der2 {
}
}
void apply_substitution(quantifier * q, expr_ref & r) {
void flatten_args(quantifier* q, unsigned& num_args, expr*const*& args) {
expr * e = q->get_expr();
unsigned num_args = to_app(e)->get_num_args();
num_args = 1;
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();
}
}
void apply_substitution(quantifier * q, expr_ref & r) {
expr * e = q->get_expr();
unsigned num_args = 1;
expr* const* args = &e;
flatten_args(q, num_args, 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);
@ -390,11 +403,7 @@ class der2 {
set_is_variable_proc(is_v);
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();
}
flatten_args(q, num_args, args);
unsigned def_count = 0;
unsigned largest_vinx = 0;

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

4
src/tactic/ufbv/macro_finder_tactic.h
View file

@ -25,4 +25,8 @@ class tactic;
tactic * mk_macro_finder_tactic(ast_manager & m, params_ref const & p = params_ref());
/*
ADD_TACTIC("macro-finder", "Identifies and applies macros.", "mk_macro_finder_tactic(m, p)")
*/
#endif

4
src/tactic/ufbv/quasi_macros_tactic.h
View file

@ -25,4 +25,8 @@ class tactic;
tactic * mk_quasi_macros_tactic(ast_manager & m, params_ref const & p = params_ref());
/*
ADD_TACTIC("quasi-macros", "Identifies and applies quasi-macros.", "mk_quasi_macros_tactic(m, p)")
*/
#endif

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