mirror of
https://github.com/Z3Prover/z3
synced 2025-10-10 01:41:57 +00:00
merged
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura
commit
265bdbe757
76 changed files with 3991 additions and 1422 deletions
422
src/api/api_algebraic.cpp
Normal file
422
src/api/api_algebraic.cpp
Normal file
|
|
@ -0,0 +1,422 @@
|
|||
/*++
|
||||
Copyright (c) 2012 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
api_algebraic.cpp
|
||||
|
||||
Abstract:
|
||||
|
||||
Additional APIs for handling Z3 algebraic numbers encoded as
|
||||
Z3_ASTs
|
||||
|
||||
Author:
|
||||
|
||||
Leonardo de Moura (leonardo) 2012-12-07
|
||||
|
||||
Notes:
|
||||
|
||||
--*/
|
||||
#include<iostream>
|
||||
#include"z3.h"
|
||||
#include"api_log_macros.h"
|
||||
#include"api_context.h"
|
||||
#include"api_ast_vector.h"
|
||||
#include"algebraic_numbers.h"
|
||||
#include"expr2polynomial.h"
|
||||
#include"cancel_eh.h"
|
||||
#include"scoped_timer.h"
|
||||
|
||||
|
||||
#define CHECK_IS_ALGEBRAIC(ARG, RET) { \
|
||||
if (!Z3_algebraic_is_value_core(c, ARG)) { \
|
||||
SET_ERROR_CODE(Z3_INVALID_ARG); \
|
||||
return RET; \
|
||||
} \
|
||||
}
|
||||
|
||||
#define CHECK_IS_ALGEBRAIC_X(ARG, RET) { \
|
||||
if (!Z3_algebraic_is_value_core(c, ARG)) { \
|
||||
SET_ERROR_CODE(Z3_INVALID_ARG); \
|
||||
RETURN_Z3(RET); \
|
||||
} \
|
||||
}
|
||||
|
||||
static arith_util & au(Z3_context c) {
|
||||
return mk_c(c)->autil();
|
||||
}
|
||||
|
||||
static algebraic_numbers::manager & am(Z3_context c) {
|
||||
return au(c).am();
|
||||
}
|
||||
|
||||
static bool is_rational(Z3_context c, Z3_ast a) {
|
||||
return au(c).is_numeral(to_expr(a));
|
||||
}
|
||||
|
||||
static bool is_irrational(Z3_context c, Z3_ast a) {
|
||||
return au(c).is_irrational_algebraic_numeral(to_expr(a));
|
||||
}
|
||||
|
||||
static rational get_rational(Z3_context c, Z3_ast a) {
|
||||
SASSERT(is_rational(c, a));
|
||||
rational r;
|
||||
VERIFY(au(c).is_numeral(to_expr(a), r));
|
||||
return r;
|
||||
}
|
||||
|
||||
static algebraic_numbers::anum const & get_irrational(Z3_context c, Z3_ast a) {
|
||||
SASSERT(is_irrational(c, a));
|
||||
return au(c).to_irrational_algebraic_numeral(to_expr(a));
|
||||
}
|
||||
|
||||
extern "C" {
|
||||
|
||||
bool Z3_algebraic_is_value_core(Z3_context c, Z3_ast a) {
|
||||
api::context * _c = mk_c(c);
|
||||
return
|
||||
is_expr(a) &&
|
||||
(_c->autil().is_numeral(to_expr(a)) ||
|
||||
_c->autil().is_irrational_algebraic_numeral(to_expr(a)));
|
||||
}
|
||||
|
||||
Z3_bool Z3_API Z3_algebraic_is_value(Z3_context c, Z3_ast a) {
|
||||
Z3_TRY;
|
||||
LOG_Z3_algebraic_is_value(c, a);
|
||||
RESET_ERROR_CODE();
|
||||
return Z3_algebraic_is_value_core(c, a) ? Z3_TRUE : Z3_FALSE;
|
||||
Z3_CATCH_RETURN(Z3_FALSE);
|
||||
}
|
||||
|
||||
Z3_bool Z3_API Z3_algebraic_is_pos(Z3_context c, Z3_ast a) {
|
||||
return Z3_algebraic_sign(c, a) > 0;
|
||||
}
|
||||
|
||||
Z3_bool Z3_API Z3_algebraic_is_neg(Z3_context c, Z3_ast a) {
|
||||
return Z3_algebraic_sign(c, a) < 0;
|
||||
}
|
||||
|
||||
Z3_bool Z3_API Z3_algebraic_is_zero(Z3_context c, Z3_ast a) {
|
||||
return Z3_algebraic_sign(c, a) == 0;
|
||||
}
|
||||
|
||||
int Z3_API Z3_algebraic_sign(Z3_context c, Z3_ast a) {
|
||||
Z3_TRY;
|
||||
LOG_Z3_algebraic_sign(c, a);
|
||||
RESET_ERROR_CODE();
|
||||
CHECK_IS_ALGEBRAIC(a, 0);
|
||||
if (is_rational(c, a)) {
|
||||
rational v = get_rational(c, a);
|
||||
if (v.is_pos()) return 1;
|
||||
else if (v.is_neg()) return -1;
|
||||
else return 0;
|
||||
}
|
||||
else {
|
||||
algebraic_numbers::anum const & v = get_irrational(c, a);
|
||||
if (am(c).is_pos(v)) return 1;
|
||||
else if (am(c).is_neg(v)) return -1;
|
||||
else return 0;
|
||||
}
|
||||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
||||
#define BIN_OP(RAT_OP, IRAT_OP) \
|
||||
algebraic_numbers::manager & _am = am(c); \
|
||||
ast * r = 0; \
|
||||
if (is_rational(c, a)) { \
|
||||
rational av = get_rational(c, a); \
|
||||
if (is_rational(c, b)) { \
|
||||
rational bv = get_rational(c, b); \
|
||||
r = au(c).mk_numeral(av RAT_OP bv, false); \
|
||||
} \
|
||||
else { \
|
||||
algebraic_numbers::anum const & bv = get_irrational(c, b); \
|
||||
scoped_anum _av(_am); \
|
||||
_am.set(_av, av.to_mpq()); \
|
||||
scoped_anum _r(_am); \
|
||||
_am.IRAT_OP(_av, bv, _r); \
|
||||
r = au(c).mk_numeral(_r, false); \
|
||||
} \
|
||||
} \
|
||||
else { \
|
||||
algebraic_numbers::anum const & av = get_irrational(c, a); \
|
||||
if (is_rational(c, b)) { \
|
||||
rational bv = get_rational(c, b); \
|
||||
scoped_anum _bv(_am); \
|
||||
_am.set(_bv, bv.to_mpq()); \
|
||||
scoped_anum _r(_am); \
|
||||
_am.IRAT_OP(av, _bv, _r); \
|
||||
r = au(c).mk_numeral(_r, false); \
|
||||
} \
|
||||
else { \
|
||||
algebraic_numbers::anum const & bv = get_irrational(c, b); \
|
||||
scoped_anum _r(_am); \
|
||||
_am.IRAT_OP(av, bv, _r); \
|
||||
r = au(c).mk_numeral(_r, false); \
|
||||
} \
|
||||
} \
|
||||
mk_c(c)->save_ast_trail(r); \
|
||||
RETURN_Z3(of_ast(r));
|
||||
|
||||
|
||||
Z3_ast Z3_API Z3_algebraic_add(Z3_context c, Z3_ast a, Z3_ast b) {
|
||||
Z3_TRY;
|
||||
LOG_Z3_algebraic_add(c, a, b);
|
||||
RESET_ERROR_CODE();
|
||||
CHECK_IS_ALGEBRAIC_X(a, 0);
|
||||
CHECK_IS_ALGEBRAIC_X(b, 0);
|
||||
BIN_OP(+,add);
|
||||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
||||
Z3_ast Z3_API Z3_algebraic_sub(Z3_context c, Z3_ast a, Z3_ast b) {
|
||||
Z3_TRY;
|
||||
LOG_Z3_algebraic_sub(c, a, b);
|
||||
RESET_ERROR_CODE();
|
||||
CHECK_IS_ALGEBRAIC_X(a, 0);
|
||||
CHECK_IS_ALGEBRAIC_X(b, 0);
|
||||
BIN_OP(-,sub);
|
||||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
||||
Z3_ast Z3_API Z3_algebraic_mul(Z3_context c, Z3_ast a, Z3_ast b) {
|
||||
Z3_TRY;
|
||||
LOG_Z3_algebraic_mul(c, a, b);
|
||||
RESET_ERROR_CODE();
|
||||
CHECK_IS_ALGEBRAIC_X(a, 0);
|
||||
CHECK_IS_ALGEBRAIC_X(b, 0);
|
||||
BIN_OP(*,mul);
|
||||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
||||
Z3_ast Z3_API Z3_algebraic_div(Z3_context c, Z3_ast a, Z3_ast b) {
|
||||
Z3_TRY;
|
||||
LOG_Z3_algebraic_div(c, a, b);
|
||||
RESET_ERROR_CODE();
|
||||
CHECK_IS_ALGEBRAIC_X(a, 0);
|
||||
CHECK_IS_ALGEBRAIC_X(b, 0);
|
||||
if ((is_rational(c, b) && get_rational(c, b).is_zero()) ||
|
||||
(!is_rational(c, b) && am(c).is_zero(get_irrational(c, b)))) {
|
||||
SET_ERROR_CODE(Z3_INVALID_ARG);
|
||||
RETURN_Z3(0);
|
||||
}
|
||||
BIN_OP(/,div);
|
||||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
||||
Z3_ast Z3_API Z3_algebraic_root(Z3_context c, Z3_ast a, unsigned k) {
|
||||
Z3_TRY;
|
||||
LOG_Z3_algebraic_root(c, a, k);
|
||||
RESET_ERROR_CODE();
|
||||
CHECK_IS_ALGEBRAIC_X(a, 0);
|
||||
if (k % 2 == 0) {
|
||||
if ((is_rational(c, a) && get_rational(c, a).is_neg()) ||
|
||||
(!is_rational(c, a) && am(c).is_neg(get_irrational(c, a)))) {
|
||||
SET_ERROR_CODE(Z3_INVALID_ARG);
|
||||
RETURN_Z3(0);
|
||||
}
|
||||
}
|
||||
algebraic_numbers::manager & _am = am(c);
|
||||
scoped_anum _r(_am);
|
||||
if (is_rational(c, a)) {
|
||||
scoped_anum av(_am);
|
||||
_am.set(av, get_rational(c, a).to_mpq());
|
||||
_am.root(av, k, _r);
|
||||
}
|
||||
else {
|
||||
algebraic_numbers::anum const & av = get_irrational(c, a);
|
||||
_am.root(av, k, _r);
|
||||
}
|
||||
expr * r = au(c).mk_numeral(_r, false);
|
||||
mk_c(c)->save_ast_trail(r);
|
||||
RETURN_Z3(of_ast(r));
|
||||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
||||
Z3_ast Z3_API Z3_algebraic_power(Z3_context c, Z3_ast a, unsigned k) {
|
||||
Z3_TRY;
|
||||
LOG_Z3_algebraic_power(c, a, k);
|
||||
RESET_ERROR_CODE();
|
||||
CHECK_IS_ALGEBRAIC_X(a, 0);
|
||||
algebraic_numbers::manager & _am = am(c);
|
||||
scoped_anum _r(_am);
|
||||
if (is_rational(c, a)) {
|
||||
scoped_anum av(_am);
|
||||
_am.set(av, get_rational(c, a).to_mpq());
|
||||
_am.power(av, k, _r);
|
||||
}
|
||||
else {
|
||||
algebraic_numbers::anum const & av = get_irrational(c, a);
|
||||
_am.power(av, k, _r);
|
||||
}
|
||||
expr * r = au(c).mk_numeral(_r, false);
|
||||
mk_c(c)->save_ast_trail(r);
|
||||
RETURN_Z3(of_ast(r));
|
||||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
||||
#define BIN_PRED(RAT_PRED, IRAT_PRED) \
|
||||
algebraic_numbers::manager & _am = am(c); \
|
||||
bool r; \
|
||||
if (is_rational(c, a)) { \
|
||||
rational av = get_rational(c, a); \
|
||||
if (is_rational(c, b)) { \
|
||||
rational bv = get_rational(c, b); \
|
||||
r = av RAT_PRED bv; \
|
||||
} \
|
||||
else { \
|
||||
algebraic_numbers::anum const & bv = get_irrational(c, b); \
|
||||
scoped_anum _av(_am); \
|
||||
_am.set(_av, av.to_mpq()); \
|
||||
r = _am.IRAT_PRED(_av, bv); \
|
||||
} \
|
||||
} \
|
||||
else { \
|
||||
algebraic_numbers::anum const & av = get_irrational(c, a); \
|
||||
if (is_rational(c, b)) { \
|
||||
rational bv = get_rational(c, b); \
|
||||
scoped_anum _bv(_am); \
|
||||
_am.set(_bv, bv.to_mpq()); \
|
||||
r = _am.IRAT_PRED(av, _bv); \
|
||||
} \
|
||||
else { \
|
||||
algebraic_numbers::anum const & bv = get_irrational(c, b); \
|
||||
r = _am.IRAT_PRED(av, bv); \
|
||||
} \
|
||||
} \
|
||||
return r ? Z3_TRUE : Z3_FALSE;
|
||||
|
||||
|
||||
Z3_bool Z3_API Z3_algebraic_lt(Z3_context c, Z3_ast a, Z3_ast b) {
|
||||
Z3_TRY;
|
||||
LOG_Z3_algebraic_lt(c, a, b);
|
||||
RESET_ERROR_CODE();
|
||||
CHECK_IS_ALGEBRAIC(a, 0);
|
||||
CHECK_IS_ALGEBRAIC(b, 0);
|
||||
BIN_PRED(<,lt);
|
||||
Z3_CATCH_RETURN(Z3_FALSE);
|
||||
}
|
||||
|
||||
Z3_bool Z3_API Z3_algebraic_gt(Z3_context c, Z3_ast a, Z3_ast b) {
|
||||
return Z3_algebraic_lt(c, b, a);
|
||||
}
|
||||
|
||||
Z3_bool Z3_API Z3_algebraic_le(Z3_context c, Z3_ast a, Z3_ast b) {
|
||||
return !Z3_algebraic_lt(c, b, a);
|
||||
}
|
||||
|
||||
Z3_bool Z3_API Z3_algebraic_ge(Z3_context c, Z3_ast a, Z3_ast b) {
|
||||
return !Z3_algebraic_lt(c, a, b);
|
||||
}
|
||||
|
||||
Z3_bool Z3_API Z3_algebraic_eq(Z3_context c, Z3_ast a, Z3_ast b) {
|
||||
Z3_TRY;
|
||||
LOG_Z3_algebraic_eq(c, a, b);
|
||||
RESET_ERROR_CODE();
|
||||
CHECK_IS_ALGEBRAIC(a, 0);
|
||||
CHECK_IS_ALGEBRAIC(b, 0);
|
||||
BIN_PRED(==,eq);
|
||||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
||||
Z3_bool Z3_API Z3_algebraic_neq(Z3_context c, Z3_ast a, Z3_ast b) {
|
||||
return !Z3_algebraic_eq(c, a, b);
|
||||
}
|
||||
|
||||
static bool to_anum_vector(Z3_context c, unsigned n, Z3_ast a[], scoped_anum_vector & as) {
|
||||
algebraic_numbers::manager & _am = am(c);
|
||||
scoped_anum tmp(_am);
|
||||
for (unsigned i = 0; i < n; i++) {
|
||||
if (is_rational(c, a[i])) {
|
||||
_am.set(tmp, get_rational(c, a[i]).to_mpq());
|
||||
as.push_back(tmp);
|
||||
}
|
||||
else if (is_irrational(c, a[i])) {
|
||||
as.push_back(get_irrational(c, a[i]));
|
||||
}
|
||||
else {
|
||||
return false;
|
||||
}
|
||||
}
|
||||
return true;
|
||||
}
|
||||
|
||||
class vector_var2anum : public polynomial::var2anum {
|
||||
scoped_anum_vector const & m_as;
|
||||
public:
|
||||
vector_var2anum(scoped_anum_vector & as):m_as(as) {}
|
||||
virtual ~vector_var2anum() {}
|
||||
virtual algebraic_numbers::manager & m() const { return m_as.m(); }
|
||||
virtual bool contains(polynomial::var x) const { return static_cast<unsigned>(x) < m_as.size(); }
|
||||
virtual algebraic_numbers::anum const & operator()(polynomial::var x) const { return m_as.get(x); }
|
||||
};
|
||||
|
||||
Z3_ast_vector Z3_API Z3_algebraic_roots(Z3_context c, Z3_ast p, unsigned n, Z3_ast a[]) {
|
||||
Z3_TRY;
|
||||
LOG_Z3_algebraic_roots(c, p, n, a);
|
||||
RESET_ERROR_CODE();
|
||||
polynomial::manager & pm = mk_c(c)->pm();
|
||||
polynomial_ref _p(pm);
|
||||
polynomial::scoped_numeral d(pm.m());
|
||||
expr2polynomial converter(mk_c(c)->m(), pm, 0, true);
|
||||
if (!converter.to_polynomial(to_expr(p), _p, d) ||
|
||||
static_cast<unsigned>(max_var(_p)) >= n + 1) {
|
||||
SET_ERROR_CODE(Z3_INVALID_ARG);
|
||||
return 0;
|
||||
}
|
||||
algebraic_numbers::manager & _am = am(c);
|
||||
scoped_anum_vector as(_am);
|
||||
if (!to_anum_vector(c, n, a, as)) {
|
||||
SET_ERROR_CODE(Z3_INVALID_ARG);
|
||||
return 0;
|
||||
}
|
||||
scoped_anum_vector roots(_am);
|
||||
{
|
||||
cancel_eh<algebraic_numbers::manager> eh(_am);
|
||||
api::context::set_interruptable(*(mk_c(c)), eh);
|
||||
scoped_timer timer(mk_c(c)->params().m_timeout, &eh);
|
||||
vector_var2anum v2a(as);
|
||||
_am.isolate_roots(_p, v2a, roots);
|
||||
}
|
||||
Z3_ast_vector_ref* result = alloc(Z3_ast_vector_ref, mk_c(c)->m());
|
||||
mk_c(c)->save_object(result);
|
||||
for (unsigned i = 0; i < roots.size(); i++) {
|
||||
result->m_ast_vector.push_back(au(c).mk_numeral(roots.get(i), false));
|
||||
}
|
||||
RETURN_Z3(of_ast_vector(result));
|
||||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
||||
int Z3_API Z3_algebraic_eval(Z3_context c, Z3_ast p, unsigned n, Z3_ast a[]) {
|
||||
Z3_TRY;
|
||||
LOG_Z3_algebraic_eval(c, p, n, a);
|
||||
RESET_ERROR_CODE();
|
||||
polynomial::manager & pm = mk_c(c)->pm();
|
||||
polynomial_ref _p(pm);
|
||||
polynomial::scoped_numeral d(pm.m());
|
||||
expr2polynomial converter(mk_c(c)->m(), pm, 0, true);
|
||||
if (!converter.to_polynomial(to_expr(p), _p, d) ||
|
||||
static_cast<unsigned>(max_var(_p)) >= n) {
|
||||
SET_ERROR_CODE(Z3_INVALID_ARG);
|
||||
return 0;
|
||||
}
|
||||
algebraic_numbers::manager & _am = am(c);
|
||||
scoped_anum_vector as(_am);
|
||||
if (!to_anum_vector(c, n, a, as)) {
|
||||
SET_ERROR_CODE(Z3_INVALID_ARG);
|
||||
return 0;
|
||||
}
|
||||
{
|
||||
cancel_eh<algebraic_numbers::manager> eh(_am);
|
||||
api::context::set_interruptable(*(mk_c(c)), eh);
|
||||
scoped_timer timer(mk_c(c)->params().m_timeout, &eh);
|
||||
vector_var2anum v2a(as);
|
||||
int r = _am.eval_sign_at(_p, v2a);
|
||||
if (r > 0) return 1;
|
||||
else if (r < 0) return -1;
|
||||
else return 0;
|
||||
}
|
||||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
||||
};
|
||||
|
|
@ -324,7 +324,8 @@ extern "C" {
|
|||
switch (_a->get_kind()) {
|
||||
case AST_APP: {
|
||||
expr * e = to_expr(_a);
|
||||
if (is_numeral_sort(c, of_sort(mk_c(c)->m().get_sort(e))) && mk_c(c)->m().is_value(e))
|
||||
// Real algebraic numbers are not considered Z3_NUMERAL_AST
|
||||
if (is_numeral_sort(c, of_sort(mk_c(c)->m().get_sort(e))) && mk_c(c)->m().is_unique_value(e))
|
||||
return Z3_NUMERAL_AST;
|
||||
return Z3_APP_AST;
|
||||
}
|
||||
|
|
|
|||
|
|
@ -82,13 +82,13 @@ namespace api {
|
|||
context::context(context_params * p, bool user_ref_count):
|
||||
m_params(p != 0 ? *p : context_params()),
|
||||
m_user_ref_count(user_ref_count),
|
||||
m_manager(m_params.m_proof ? PGM_FINE : PGM_DISABLED, m_params.m_trace ? m_params.m_trace_file_name.c_str() : 0),
|
||||
m_plugins(m_manager),
|
||||
m_arith_util(m_manager),
|
||||
m_bv_util(m_manager),
|
||||
m_datalog_util(m_manager),
|
||||
m_last_result(m_manager),
|
||||
m_ast_trail(m_manager),
|
||||
m_manager(m_params.mk_ast_manager()),
|
||||
m_plugins(m()),
|
||||
m_arith_util(m()),
|
||||
m_bv_util(m()),
|
||||
m_datalog_util(m()),
|
||||
m_last_result(m()),
|
||||
m_ast_trail(m()),
|
||||
m_replay_stack() {
|
||||
|
||||
m_solver = 0;
|
||||
|
|
@ -102,22 +102,16 @@ namespace api {
|
|||
m_smtlib_parser_has_decls = false;
|
||||
|
||||
z3_bound_num_procs();
|
||||
//
|
||||
// Configuration parameter settings.
|
||||
//
|
||||
if (m_params.m_debug_ref_count) {
|
||||
m_manager.debug_ref_count();
|
||||
}
|
||||
|
||||
m_error_handler = &default_error_handler;
|
||||
|
||||
m_basic_fid = m_manager.get_basic_family_id();
|
||||
m_arith_fid = m_manager.get_family_id("arith");
|
||||
m_bv_fid = m_manager.get_family_id("bv");
|
||||
m_array_fid = m_manager.get_family_id("array");
|
||||
m_dt_fid = m_manager.get_family_id("datatype");
|
||||
m_datalog_fid = m_manager.get_family_id("datalog_relation");
|
||||
m_dt_plugin = static_cast<datatype_decl_plugin*>(m_manager.get_plugin(m_dt_fid));
|
||||
m_basic_fid = m().get_basic_family_id();
|
||||
m_arith_fid = m().get_family_id("arith");
|
||||
m_bv_fid = m().get_family_id("bv");
|
||||
m_array_fid = m().get_family_id("array");
|
||||
m_dt_fid = m().get_family_id("datatype");
|
||||
m_datalog_fid = m().get_family_id("datalog_relation");
|
||||
m_dt_plugin = static_cast<datatype_decl_plugin*>(m().get_plugin(m_dt_fid));
|
||||
|
||||
if (!m_user_ref_count) {
|
||||
m_replay_stack.push_back(0);
|
||||
|
|
@ -143,6 +137,7 @@ namespace api {
|
|||
{
|
||||
if (m_interruptable)
|
||||
(*m_interruptable)();
|
||||
m().set_cancel(true);
|
||||
}
|
||||
}
|
||||
|
||||
|
|
@ -195,12 +190,12 @@ namespace api {
|
|||
expr * context::mk_and(unsigned num_exprs, expr * const * exprs) {
|
||||
switch(num_exprs) {
|
||||
case 0:
|
||||
return m_manager.mk_true();
|
||||
return m().mk_true();
|
||||
case 1:
|
||||
save_ast_trail(exprs[0]);
|
||||
return exprs[0];
|
||||
default: {
|
||||
expr * a = m_manager.mk_and(num_exprs, exprs);
|
||||
expr * a = m().mk_and(num_exprs, exprs);
|
||||
save_ast_trail(a);
|
||||
return a;
|
||||
} }
|
||||
|
|
@ -216,7 +211,7 @@ namespace api {
|
|||
SASSERT(m_replay_stack.size() > num_scopes);
|
||||
unsigned j = m_replay_stack.size() - num_scopes - 1;
|
||||
if (!m_replay_stack[j]) {
|
||||
m_replay_stack[j] = alloc(ast_ref_vector, m_manager);
|
||||
m_replay_stack[j] = alloc(ast_ref_vector, m());
|
||||
}
|
||||
m_replay_stack[j]->push_back(n);
|
||||
}
|
||||
|
|
@ -324,7 +319,7 @@ namespace api {
|
|||
smt::kernel & context::get_smt_kernel() {
|
||||
if (!m_solver) {
|
||||
m_fparams.updt_params(m_params);
|
||||
m_solver = alloc(smt::kernel, m_manager, m_fparams);
|
||||
m_solver = alloc(smt::kernel, m(), m_fparams);
|
||||
}
|
||||
return *m_solver;
|
||||
}
|
||||
|
|
|
|||
|
|
@ -32,6 +32,7 @@ Revision History:
|
|||
#include"event_handler.h"
|
||||
#include"tactic_manager.h"
|
||||
#include"context_params.h"
|
||||
#include"api_polynomial.h"
|
||||
|
||||
namespace smtlib {
|
||||
class parser;
|
||||
|
|
@ -45,7 +46,7 @@ namespace api {
|
|||
struct add_plugins { add_plugins(ast_manager & m); };
|
||||
context_params m_params;
|
||||
bool m_user_ref_count; //!< if true, the user is responsible for managing referenc counters.
|
||||
ast_manager m_manager;
|
||||
scoped_ptr<ast_manager> m_manager;
|
||||
add_plugins m_plugins;
|
||||
|
||||
arith_util m_arith_util;
|
||||
|
|
@ -81,6 +82,8 @@ namespace api {
|
|||
Z3_ast_print_mode m_print_mode;
|
||||
|
||||
event_handler * m_interruptable; // Reference to an object that can be interrupted by Z3_interrupt
|
||||
|
||||
pmanager m_pmanager;
|
||||
public:
|
||||
// Scoped obj for setting m_interruptable
|
||||
class set_interruptable {
|
||||
|
|
@ -98,10 +101,10 @@ namespace api {
|
|||
|
||||
context(context_params * p, bool user_ref_count = false);
|
||||
~context();
|
||||
ast_manager & m() { return m_manager; }
|
||||
ast_manager & m() const { return *(m_manager.get()); }
|
||||
|
||||
context_params & params() { return m_params; }
|
||||
bool produce_proofs() const { return m_manager.proofs_enabled(); }
|
||||
bool produce_proofs() const { return m().proofs_enabled(); }
|
||||
bool produce_models() const { return m_params.m_model; }
|
||||
bool produce_unsat_cores() const { return m_params.m_unsat_core; }
|
||||
bool use_auto_config() const { return m_params.m_auto_config; }
|
||||
|
|
@ -167,6 +170,13 @@ namespace api {
|
|||
|
||||
void check_sorts(ast * n);
|
||||
|
||||
// ------------------------
|
||||
//
|
||||
// Polynomial manager & caches
|
||||
//
|
||||
// -----------------------
|
||||
polynomial::manager & pm() { return m_pmanager.pm(); }
|
||||
|
||||
// ------------------------
|
||||
//
|
||||
// Solver interface for backward compatibility
|
||||
|
|
|
|||
84
src/api/api_polynomial.cpp
Normal file
84
src/api/api_polynomial.cpp
Normal file
|
|
@ -0,0 +1,84 @@
|
|||
/*++
|
||||
Copyright (c) 2012 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
api_polynomial.cpp
|
||||
|
||||
Abstract:
|
||||
|
||||
Polynomial manager and caches for the external API.
|
||||
|
||||
Author:
|
||||
|
||||
Leonardo de Moura (leonardo) 2012-12-08
|
||||
|
||||
Notes:
|
||||
|
||||
--*/
|
||||
#include<iostream>
|
||||
#include"z3.h"
|
||||
#include"api_log_macros.h"
|
||||
#include"api_context.h"
|
||||
#include"api_polynomial.h"
|
||||
#include"api_ast_vector.h"
|
||||
#include"expr2polynomial.h"
|
||||
#include"cancel_eh.h"
|
||||
#include"scoped_timer.h"
|
||||
#include"expr2var.h"
|
||||
|
||||
namespace api {
|
||||
|
||||
pmanager::pmanager():
|
||||
m_pm(m_nm) {
|
||||
}
|
||||
|
||||
pmanager::~pmanager() {
|
||||
}
|
||||
|
||||
void pmanager::set_cancel(bool f) {
|
||||
m_pm.set_cancel(f);
|
||||
}
|
||||
|
||||
};
|
||||
|
||||
extern "C" {
|
||||
|
||||
Z3_ast_vector Z3_API Z3_polynomial_subresultants(Z3_context c, Z3_ast p, Z3_ast q, Z3_ast x) {
|
||||
Z3_TRY;
|
||||
LOG_Z3_polynomial_subresultants(c, p, q, x);
|
||||
RESET_ERROR_CODE();
|
||||
polynomial::manager & pm = mk_c(c)->pm();
|
||||
polynomial_ref _p(pm), _q(pm);
|
||||
polynomial::scoped_numeral d(pm.m());
|
||||
default_expr2polynomial converter(mk_c(c)->m(), pm);
|
||||
if (!converter.to_polynomial(to_expr(p), _p, d) ||
|
||||
!converter.to_polynomial(to_expr(q), _q, d)) {
|
||||
SET_ERROR_CODE(Z3_INVALID_ARG);
|
||||
return 0;
|
||||
}
|
||||
Z3_ast_vector_ref* result = alloc(Z3_ast_vector_ref, mk_c(c)->m());
|
||||
mk_c(c)->save_object(result);
|
||||
if (converter.is_var(to_expr(x))) {
|
||||
expr2var const & mapping = converter.get_mapping();
|
||||
unsigned v_x = mapping.to_var(to_expr(x));
|
||||
polynomial_ref_vector rs(pm);
|
||||
polynomial_ref r(pm);
|
||||
expr_ref _r(mk_c(c)->m());
|
||||
{
|
||||
cancel_eh<polynomial::manager> eh(pm);
|
||||
api::context::set_interruptable(*(mk_c(c)), eh);
|
||||
scoped_timer timer(mk_c(c)->params().m_timeout, &eh);
|
||||
pm.psc_chain(_p, _q, v_x, rs);
|
||||
}
|
||||
for (unsigned i = 0; i < rs.size(); i++) {
|
||||
r = rs.get(i);
|
||||
converter.to_expr(r, true, _r);
|
||||
result->m_ast_vector.push_back(_r);
|
||||
}
|
||||
}
|
||||
RETURN_Z3(of_ast_vector(result));
|
||||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
||||
};
|
||||
39
src/api/api_polynomial.h
Normal file
39
src/api/api_polynomial.h
Normal file
|
|
@ -0,0 +1,39 @@
|
|||
/*++
|
||||
Copyright (c) 2012 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
api_polynomial.h
|
||||
|
||||
Abstract:
|
||||
|
||||
Polynomial manager and caches for the external API.
|
||||
|
||||
Author:
|
||||
|
||||
Leonardo de Moura (leonardo) 2012-12-08
|
||||
|
||||
Notes:
|
||||
|
||||
--*/
|
||||
#ifndef _API_POLYNOMIAL_H_
|
||||
#define _API_POLYNOMIAL_H_
|
||||
|
||||
#include"polynomial.h"
|
||||
|
||||
namespace api {
|
||||
|
||||
class pmanager {
|
||||
unsynch_mpz_manager m_nm;
|
||||
polynomial::manager m_pm;
|
||||
// TODO: add support for caching expressions -> polynomial and back
|
||||
public:
|
||||
pmanager();
|
||||
virtual ~pmanager();
|
||||
polynomial::manager & pm() { return m_pm; }
|
||||
void set_cancel(bool f);
|
||||
};
|
||||
|
||||
};
|
||||
|
||||
#endif
|
||||
|
|
@ -36,17 +36,7 @@ extern "C" {
|
|||
static void init_solver_core(Z3_context c, Z3_solver _s) {
|
||||
ast_manager & m = mk_c(c)->m();
|
||||
Z3_solver_ref * s = to_solver(_s);
|
||||
s->m_solver->set_produce_proofs(mk_c(c)->produce_proofs());
|
||||
s->m_solver->set_produce_unsat_cores(s->m_params.get_bool("unsat_core", mk_c(c)->produce_unsat_cores()));
|
||||
s->m_solver->set_produce_models(s->m_params.get_bool("model", mk_c(c)->produce_models()));
|
||||
if (!mk_c(c)->use_auto_config()) {
|
||||
params_ref p = s->m_params;
|
||||
p.set_bool("auto_config", false);
|
||||
s->m_solver->updt_params(p);
|
||||
}
|
||||
else {
|
||||
s->m_solver->updt_params(s->m_params);
|
||||
}
|
||||
mk_c(c)->params().init_solver_params(mk_c(c)->m(), *(s->m_solver), s->m_params);
|
||||
s->m_solver->init(m, s->m_logic);
|
||||
s->m_initialized = true;
|
||||
}
|
||||
|
|
|
|||
|
|
@ -1,4 +1,3 @@
|
|||
Java bindings
|
||||
-------------
|
||||
|
||||
This is currently "working in progress".
|
||||
|
|
@ -1126,6 +1126,27 @@ def Var(idx, s):
|
|||
_z3_assert(is_sort(s), "Z3 sort expected")
|
||||
return _to_expr_ref(Z3_mk_bound(s.ctx_ref(), idx, s.ast), s.ctx)
|
||||
|
||||
def RealVar(idx, ctx=None):
|
||||
"""
|
||||
Create a real free variable. Free variables are used to create quantified formulas.
|
||||
They are also used to create polynomials.
|
||||
|
||||
>>> RealVar(0)
|
||||
Var(0)
|
||||
"""
|
||||
return Var(idx, RealSort(ctx))
|
||||
|
||||
def RealVarVector(n, ctx=None):
|
||||
"""
|
||||
Create a list of Real free variables.
|
||||
The variables have ids: 0, 1, ..., n-1
|
||||
|
||||
>>> x0, x1, x2, x3 = RealVarVector(4)
|
||||
>>> x2
|
||||
Var(2)
|
||||
"""
|
||||
return [ RealVar(i, ctx) for i in range(n) ]
|
||||
|
||||
#########################################
|
||||
#
|
||||
# Booleans
|
||||
|
|
|
|||
564
src/api/python/z3num.py
Normal file
564
src/api/python/z3num.py
Normal file
|
|
@ -0,0 +1,564 @@
|
|||
############################################
|
||||
# Copyright (c) 2012 Microsoft Corporation
|
||||
#
|
||||
# Z3 Python interface for Z3 numerals
|
||||
#
|
||||
# Author: Leonardo de Moura (leonardo)
|
||||
############################################
|
||||
from z3 import *
|
||||
from z3core import *
|
||||
from z3printer import *
|
||||
|
||||
def _to_numeral(num, ctx=None):
|
||||
if isinstance(num, Numeral):
|
||||
return num
|
||||
else:
|
||||
return Numeral(num, ctx)
|
||||
|
||||
class Numeral:
|
||||
"""
|
||||
A Z3 numeral can be used to perform computations over arbitrary
|
||||
precision integers, rationals and real algebraic numbers.
|
||||
It also automatically converts python numeric values.
|
||||
|
||||
>>> Numeral(2)
|
||||
2
|
||||
>>> Numeral("3/2") + 1
|
||||
5/2
|
||||
>>> Numeral(Sqrt(2))
|
||||
1.4142135623?
|
||||
>>> Numeral(Sqrt(2)) + 2
|
||||
3.4142135623?
|
||||
>>> Numeral(Sqrt(2)) + Numeral(Sqrt(3))
|
||||
3.1462643699?
|
||||
|
||||
Z3 numerals can be used to perform computations with
|
||||
values in a Z3 model.
|
||||
|
||||
>>> s = Solver()
|
||||
>>> x = Real('x')
|
||||
>>> s.add(x*x == 2)
|
||||
>>> s.add(x > 0)
|
||||
>>> s.check()
|
||||
sat
|
||||
>>> m = s.model()
|
||||
>>> m[x]
|
||||
1.4142135623?
|
||||
>>> m[x] + 1
|
||||
1.4142135623? + 1
|
||||
|
||||
The previous result is a Z3 expression.
|
||||
|
||||
>>> (m[x] + 1).sexpr()
|
||||
'(+ (root-obj (+ (^ x 2) (- 2)) 2) 1.0)'
|
||||
|
||||
>>> Numeral(m[x]) + 1
|
||||
2.4142135623?
|
||||
>>> Numeral(m[x]).is_pos()
|
||||
True
|
||||
>>> Numeral(m[x])**2
|
||||
2
|
||||
|
||||
We can also isolate the roots of polynomials.
|
||||
|
||||
>>> x0, x1, x2 = RealVarVector(3)
|
||||
>>> r0 = isolate_roots(x0**5 - x0 - 1)
|
||||
>>> r0
|
||||
[1.1673039782?]
|
||||
|
||||
In the following example, we are isolating the roots
|
||||
of a univariate polynomial (on x1) obtained after substituting
|
||||
x0 -> r0[0]
|
||||
|
||||
>>> r1 = isolate_roots(x1**2 - x0 + 1, [ r0[0] ])
|
||||
>>> r1
|
||||
[-0.4090280898?, 0.4090280898?]
|
||||
|
||||
Similarly, in the next example we isolate the roots of
|
||||
a univariate polynomial (on x2) obtained after substituting
|
||||
x0 -> r0[0] and x1 -> r1[0]
|
||||
|
||||
>>> isolate_roots(x1*x2 + x0, [ r0[0], r1[0] ])
|
||||
[2.8538479564?]
|
||||
|
||||
"""
|
||||
def __init__(self, num, ctx=None):
|
||||
if isinstance(num, Ast):
|
||||
self.ast = num
|
||||
self.ctx = z3._get_ctx(ctx)
|
||||
elif isinstance(num, RatNumRef) or isinstance(num, AlgebraicNumRef):
|
||||
self.ast = num.ast
|
||||
self.ctx = num.ctx
|
||||
elif isinstance(num, ArithRef):
|
||||
r = simplify(num)
|
||||
self.ast = r.ast
|
||||
self.ctx = r.ctx
|
||||
else:
|
||||
v = RealVal(num, ctx)
|
||||
self.ast = v.ast
|
||||
self.ctx = v.ctx
|
||||
Z3_inc_ref(self.ctx_ref(), self.as_ast())
|
||||
assert Z3_algebraic_is_value(self.ctx_ref(), self.ast)
|
||||
|
||||
def __del__(self):
|
||||
Z3_dec_ref(self.ctx_ref(), self.as_ast())
|
||||
|
||||
def is_integer(self):
|
||||
""" Return True if the numeral is integer.
|
||||
|
||||
>>> Numeral(2).is_integer()
|
||||
True
|
||||
>>> (Numeral(Sqrt(2)) * Numeral(Sqrt(2))).is_integer()
|
||||
True
|
||||
>>> Numeral(Sqrt(2)).is_integer()
|
||||
False
|
||||
>>> Numeral("2/3").is_integer()
|
||||
False
|
||||
"""
|
||||
return self.is_rational() and self.denominator() == 1
|
||||
|
||||
def is_rational(self):
|
||||
""" Return True if the numeral is rational.
|
||||
|
||||
>>> Numeral(2).is_rational()
|
||||
True
|
||||
>>> Numeral("2/3").is_rational()
|
||||
True
|
||||
>>> Numeral(Sqrt(2)).is_rational()
|
||||
False
|
||||
|
||||
"""
|
||||
return Z3_get_ast_kind(self.ctx_ref(), self.as_ast()) == Z3_NUMERAL_AST
|
||||
|
||||
def denominator(self):
|
||||
""" Return the denominator if `self` is rational.
|
||||
|
||||
>>> Numeral("2/3").denominator()
|
||||
3
|
||||
"""
|
||||
assert(self.is_rational())
|
||||
return Numeral(Z3_get_denominator(self.ctx_ref(), self.as_ast()), self.ctx)
|
||||
|
||||
def numerator(self):
|
||||
""" Return the numerator if `self` is rational.
|
||||
|
||||
>>> Numeral("2/3").numerator()
|
||||
2
|
||||
"""
|
||||
assert(self.is_rational())
|
||||
return Numeral(Z3_get_numerator(self.ctx_ref(), self.as_ast()), self.ctx)
|
||||
|
||||
|
||||
def is_irrational(self):
|
||||
""" Return True if the numeral is irrational.
|
||||
|
||||
>>> Numeral(2).is_irrational()
|
||||
False
|
||||
>>> Numeral("2/3").is_irrational()
|
||||
False
|
||||
>>> Numeral(Sqrt(2)).is_irrational()
|
||||
True
|
||||
"""
|
||||
return not self.is_rational()
|
||||
|
||||
def as_long(self):
|
||||
""" Return a numeral (that is an integer) as a Python long.
|
||||
|
||||
>>> (Numeral(10)**20).as_long()
|
||||
100000000000000000000L
|
||||
"""
|
||||
assert(self.is_integer())
|
||||
return long(Z3_get_numeral_string(self.ctx_ref(), self.as_ast()))
|
||||
|
||||
def approx(self, precision=10):
|
||||
"""Return a numeral that approximates the numeral `self`.
|
||||
The result `r` is such that |r - self| <= 1/10^precision
|
||||
|
||||
If `self` is rational, then the result is `self`.
|
||||
|
||||
>>> x = Numeral(2).root(2)
|
||||
>>> x.approx(20)
|
||||
6838717160008073720548335/4835703278458516698824704
|
||||
>>> x.approx(5)
|
||||
2965821/2097152
|
||||
>>> Numeral(2).approx(10)
|
||||
2
|
||||
"""
|
||||
return self.upper(precision)
|
||||
|
||||
def upper(self, precision=10):
|
||||
"""Return a upper bound that approximates the numeral `self`.
|
||||
The result `r` is such that r - self <= 1/10^precision
|
||||
|
||||
If `self` is rational, then the result is `self`.
|
||||
|
||||
>>> x = Numeral(2).root(2)
|
||||
>>> x.upper(20)
|
||||
6838717160008073720548335/4835703278458516698824704
|
||||
>>> x.upper(5)
|
||||
2965821/2097152
|
||||
>>> Numeral(2).upper(10)
|
||||
2
|
||||
"""
|
||||
if self.is_rational():
|
||||
return self
|
||||
else:
|
||||
return Numeral(Z3_get_algebraic_number_upper(self.ctx_ref(), self.as_ast(), precision), self.ctx)
|
||||
|
||||
def lower(self, precision=10):
|
||||
"""Return a lower bound that approximates the numeral `self`.
|
||||
The result `r` is such that self - r <= 1/10^precision
|
||||
|
||||
If `self` is rational, then the result is `self`.
|
||||
|
||||
>>> x = Numeral(2).root(2)
|
||||
>>> x.lower(20)
|
||||
1709679290002018430137083/1208925819614629174706176
|
||||
>>> Numeral("2/3").lower(10)
|
||||
2/3
|
||||
"""
|
||||
if self.is_rational():
|
||||
return self
|
||||
else:
|
||||
return Numeral(Z3_get_algebraic_number_lower(self.ctx_ref(), self.as_ast(), precision), self.ctx)
|
||||
|
||||
def sign(self):
|
||||
""" Return the sign of the numeral.
|
||||
|
||||
>>> Numeral(2).sign()
|
||||
1
|
||||
>>> Numeral(-3).sign()
|
||||
-1
|
||||
>>> Numeral(0).sign()
|
||||
0
|
||||
"""
|
||||
return Z3_algebraic_sign(self.ctx_ref(), self.ast)
|
||||
|
||||
def is_pos(self):
|
||||
""" Return True if the numeral is positive.
|
||||
|
||||
>>> Numeral(2).is_pos()
|
||||
True
|
||||
>>> Numeral(-3).is_pos()
|
||||
False
|
||||
>>> Numeral(0).is_pos()
|
||||
False
|
||||
"""
|
||||
return Z3_algebraic_is_pos(self.ctx_ref(), self.ast)
|
||||
|
||||
def is_neg(self):
|
||||
""" Return True if the numeral is negative.
|
||||
|
||||
>>> Numeral(2).is_neg()
|
||||
False
|
||||
>>> Numeral(-3).is_neg()
|
||||
True
|
||||
>>> Numeral(0).is_neg()
|
||||
False
|
||||
"""
|
||||
return Z3_algebraic_is_neg(self.ctx_ref(), self.ast)
|
||||
|
||||
def is_zero(self):
|
||||
""" Return True if the numeral is zero.
|
||||
|
||||
>>> Numeral(2).is_zero()
|
||||
False
|
||||
>>> Numeral(-3).is_zero()
|
||||
False
|
||||
>>> Numeral(0).is_zero()
|
||||
True
|
||||
>>> sqrt2 = Numeral(2).root(2)
|
||||
>>> sqrt2.is_zero()
|
||||
False
|
||||
>>> (sqrt2 - sqrt2).is_zero()
|
||||
True
|
||||
"""
|
||||
return Z3_algebraic_is_zero(self.ctx_ref(), self.ast)
|
||||
|
||||
def __add__(self, other):
|
||||
""" Return the numeral `self + other`.
|
||||
|
||||
>>> Numeral(2) + 3
|
||||
5
|
||||
>>> Numeral(2) + Numeral(4)
|
||||
6
|
||||
>>> Numeral("2/3") + 1
|
||||
5/3
|
||||
"""
|
||||
return Numeral(Z3_algebraic_add(self.ctx_ref(), self.ast, _to_numeral(other, self.ctx).ast), self.ctx)
|
||||
|
||||
def __radd__(self, other):
|
||||
""" Return the numeral `other + self`.
|
||||
|
||||
>>> 3 + Numeral(2)
|
||||
5
|
||||
"""
|
||||
return Numeral(Z3_algebraic_add(self.ctx_ref(), self.ast, _to_numeral(other, self.ctx).ast), self.ctx)
|
||||
|
||||
def __sub__(self, other):
|
||||
""" Return the numeral `self - other`.
|
||||
|
||||
>>> Numeral(2) - 3
|
||||
-1
|
||||
"""
|
||||
return Numeral(Z3_algebraic_sub(self.ctx_ref(), self.ast, _to_numeral(other, self.ctx).ast), self.ctx)
|
||||
|
||||
def __rsub__(self, other):
|
||||
""" Return the numeral `other - self`.
|
||||
|
||||
>>> 3 - Numeral(2)
|
||||
1
|
||||
"""
|
||||
return Numeral(Z3_algebraic_sub(self.ctx_ref(), _to_numeral(other, self.ctx).ast, self.ast), self.ctx)
|
||||
|
||||
def __mul__(self, other):
|
||||
""" Return the numeral `self * other`.
|
||||
>>> Numeral(2) * 3
|
||||
6
|
||||
"""
|
||||
return Numeral(Z3_algebraic_mul(self.ctx_ref(), self.ast, _to_numeral(other, self.ctx).ast), self.ctx)
|
||||
|
||||
def __rmul__(self, other):
|
||||
""" Return the numeral `other * mul`.
|
||||
>>> 3 * Numeral(2)
|
||||
6
|
||||
"""
|
||||
return Numeral(Z3_algebraic_mul(self.ctx_ref(), self.ast, _to_numeral(other, self.ctx).ast), self.ctx)
|
||||
|
||||
def __div__(self, other):
|
||||
""" Return the numeral `self / other`.
|
||||
>>> Numeral(2) / 3
|
||||
2/3
|
||||
>>> Numeral(2).root(2) / 3
|
||||
0.4714045207?
|
||||
>>> Numeral(Sqrt(2)) / Numeral(Sqrt(3))
|
||||
0.8164965809?
|
||||
"""
|
||||
return Numeral(Z3_algebraic_div(self.ctx_ref(), self.ast, _to_numeral(other, self.ctx).ast), self.ctx)
|
||||
|
||||
def __rdiv__(self, other):
|
||||
""" Return the numeral `other / self`.
|
||||
>>> 3 / Numeral(2)
|
||||
3/2
|
||||
>>> 3 / Numeral(2).root(2)
|
||||
2.1213203435?
|
||||
"""
|
||||
return Numeral(Z3_algebraic_div(self.ctx_ref(), _to_numeral(other, self.ctx).ast, self.ast), self.ctx)
|
||||
|
||||
def root(self, k):
|
||||
""" Return the numeral `self^(1/k)`.
|
||||
|
||||
>>> sqrt2 = Numeral(2).root(2)
|
||||
>>> sqrt2
|
||||
1.4142135623?
|
||||
>>> sqrt2 * sqrt2
|
||||
2
|
||||
>>> sqrt2 * 2 + 1
|
||||
3.8284271247?
|
||||
>>> (sqrt2 * 2 + 1).sexpr()
|
||||
'(root-obj (+ (^ x 2) (* (- 2) x) (- 7)) 2)'
|
||||
"""
|
||||
return Numeral(Z3_algebraic_root(self.ctx_ref(), self.ast, k), self.ctx)
|
||||
|
||||
def power(self, k):
|
||||
""" Return the numeral `self^k`.
|
||||
|
||||
>>> sqrt3 = Numeral(3).root(2)
|
||||
>>> sqrt3
|
||||
1.7320508075?
|
||||
>>> sqrt3.power(2)
|
||||
3
|
||||
"""
|
||||
return Numeral(Z3_algebraic_power(self.ctx_ref(), self.ast, k), self.ctx)
|
||||
|
||||
def __pow__(self, k):
|
||||
""" Return the numeral `self^k`.
|
||||
|
||||
>>> sqrt3 = Numeral(3).root(2)
|
||||
>>> sqrt3
|
||||
1.7320508075?
|
||||
>>> sqrt3**2
|
||||
3
|
||||
"""
|
||||
return self.power(k)
|
||||
|
||||
def __lt__(self, other):
|
||||
""" Return True if `self < other`.
|
||||
|
||||
>>> Numeral(Sqrt(2)) < 2
|
||||
True
|
||||
>>> Numeral(Sqrt(3)) < Numeral(Sqrt(2))
|
||||
False
|
||||
>>> Numeral(Sqrt(2)) < Numeral(Sqrt(2))
|
||||
False
|
||||
"""
|
||||
return Z3_algebraic_lt(self.ctx_ref(), self.ast, _to_numeral(other, self.ctx).ast)
|
||||
|
||||
def __rlt__(self, other):
|
||||
""" Return True if `other < self`.
|
||||
|
||||
>>> 2 < Numeral(Sqrt(2))
|
||||
False
|
||||
"""
|
||||
return self > other
|
||||
|
||||
def __gt__(self, other):
|
||||
""" Return True if `self > other`.
|
||||
|
||||
>>> Numeral(Sqrt(2)) > 2
|
||||
False
|
||||
>>> Numeral(Sqrt(3)) > Numeral(Sqrt(2))
|
||||
True
|
||||
>>> Numeral(Sqrt(2)) > Numeral(Sqrt(2))
|
||||
False
|
||||
"""
|
||||
return Z3_algebraic_gt(self.ctx_ref(), self.ast, _to_numeral(other, self.ctx).ast)
|
||||
|
||||
def __rgt__(self, other):
|
||||
""" Return True if `other > self`.
|
||||
|
||||
>>> 2 > Numeral(Sqrt(2))
|
||||
True
|
||||
"""
|
||||
return self < other
|
||||
|
||||
|
||||
def __le__(self, other):
|
||||
""" Return True if `self <= other`.
|
||||
|
||||
>>> Numeral(Sqrt(2)) <= 2
|
||||
True
|
||||
>>> Numeral(Sqrt(3)) <= Numeral(Sqrt(2))
|
||||
False
|
||||
>>> Numeral(Sqrt(2)) <= Numeral(Sqrt(2))
|
||||
True
|
||||
"""
|
||||
return Z3_algebraic_le(self.ctx_ref(), self.ast, _to_numeral(other, self.ctx).ast)
|
||||
|
||||
def __rle__(self, other):
|
||||
""" Return True if `other <= self`.
|
||||
|
||||
>>> 2 <= Numeral(Sqrt(2))
|
||||
False
|
||||
"""
|
||||
return self >= other
|
||||
|
||||
def __ge__(self, other):
|
||||
""" Return True if `self >= other`.
|
||||
|
||||
>>> Numeral(Sqrt(2)) >= 2
|
||||
False
|
||||
>>> Numeral(Sqrt(3)) >= Numeral(Sqrt(2))
|
||||
True
|
||||
>>> Numeral(Sqrt(2)) >= Numeral(Sqrt(2))
|
||||
True
|
||||
"""
|
||||
return Z3_algebraic_ge(self.ctx_ref(), self.ast, _to_numeral(other, self.ctx).ast)
|
||||
|
||||
def __rge__(self, other):
|
||||
""" Return True if `other >= self`.
|
||||
|
||||
>>> 2 >= Numeral(Sqrt(2))
|
||||
True
|
||||
"""
|
||||
return self <= other
|
||||
|
||||
def __eq__(self, other):
|
||||
""" Return True if `self == other`.
|
||||
|
||||
>>> Numeral(Sqrt(2)) == 2
|
||||
False
|
||||
>>> Numeral(Sqrt(3)) == Numeral(Sqrt(2))
|
||||
False
|
||||
>>> Numeral(Sqrt(2)) == Numeral(Sqrt(2))
|
||||
True
|
||||
"""
|
||||
return Z3_algebraic_eq(self.ctx_ref(), self.ast, _to_numeral(other, self.ctx).ast)
|
||||
|
||||
def __ne__(self, other):
|
||||
""" Return True if `self != other`.
|
||||
|
||||
>>> Numeral(Sqrt(2)) != 2
|
||||
True
|
||||
>>> Numeral(Sqrt(3)) != Numeral(Sqrt(2))
|
||||
True
|
||||
>>> Numeral(Sqrt(2)) != Numeral(Sqrt(2))
|
||||
False
|
||||
"""
|
||||
return Z3_algebraic_neq(self.ctx_ref(), self.ast, _to_numeral(other, self.ctx).ast)
|
||||
|
||||
def __str__(self):
|
||||
if Z3_is_numeral_ast(self.ctx_ref(), self.ast):
|
||||
return str(RatNumRef(self.ast, self.ctx))
|
||||
else:
|
||||
return str(AlgebraicNumRef(self.ast, self.ctx))
|
||||
|
||||
def __repr__(self):
|
||||
return self.__str__()
|
||||
|
||||
def sexpr(self):
|
||||
return Z3_ast_to_string(self.ctx_ref(), self.as_ast())
|
||||
|
||||
def as_ast(self):
|
||||
return self.ast
|
||||
|
||||
def ctx_ref(self):
|
||||
return self.ctx.ref()
|
||||
|
||||
def eval_sign_at(p, vs):
|
||||
"""
|
||||
Evaluate the sign of the polynomial `p` at `vs`. `p` is a Z3
|
||||
Expression containing arithmetic operators: +, -, *, ^k where k is
|
||||
an integer; and free variables x that is_var(x) is True. Moreover,
|
||||
all variables must be real.
|
||||
|
||||
The result is 1 if the polynomial is positive at the given point,
|
||||
-1 if negative, and 0 if zero.
|
||||
|
||||
>>> x0, x1, x2 = RealVarVector(3)
|
||||
>>> eval_sign_at(x0**2 + x1*x2 + 1, (Numeral(0), Numeral(1), Numeral(2)))
|
||||
1
|
||||
>>> eval_sign_at(x0**2 - 2, [ Numeral(Sqrt(2)) ])
|
||||
0
|
||||
>>> eval_sign_at((x0 + x1)*(x0 + x2), (Numeral(0), Numeral(Sqrt(2)), Numeral(Sqrt(3))))
|
||||
1
|
||||
"""
|
||||
num = len(vs)
|
||||
_vs = (Ast * num)()
|
||||
for i in range(num):
|
||||
_vs[i] = vs[i].ast
|
||||
return Z3_algebraic_eval(p.ctx_ref(), p.as_ast(), num, _vs)
|
||||
|
||||
def isolate_roots(p, vs=[]):
|
||||
"""
|
||||
Given a multivariate polynomial p(x_0, ..., x_{n-1}, x_n), returns the
|
||||
roots of the univariate polynomial p(vs[0], ..., vs[len(vs)-1], x_n).
|
||||
|
||||
Remarks:
|
||||
* p is a Z3 expression that contains only arithmetic terms and free variables.
|
||||
* forall i in [0, n) vs is a numeral.
|
||||
|
||||
The result is a list of numerals
|
||||
|
||||
>>> x0 = RealVar(0)
|
||||
>>> isolate_roots(x0**5 - x0 - 1)
|
||||
[1.1673039782?]
|
||||
>>> x1 = RealVar(1)
|
||||
>>> isolate_roots(x0**2 - x1**4 - 1, [ Numeral(Sqrt(3)) ])
|
||||
[-1.1892071150?, 1.1892071150?]
|
||||
>>> x2 = RealVar(2)
|
||||
>>> isolate_roots(x2**2 + x0 - x1, [ Numeral(Sqrt(3)), Numeral(Sqrt(2)) ])
|
||||
[]
|
||||
"""
|
||||
num = len(vs)
|
||||
_vs = (Ast * num)()
|
||||
for i in range(num):
|
||||
_vs[i] = vs[i].ast
|
||||
_roots = AstVector(Z3_algebraic_roots(p.ctx_ref(), p.as_ast(), num, _vs), p.ctx)
|
||||
return [ Numeral(r) for r in _roots ]
|
||||
|
||||
if __name__ == "__main__":
|
||||
import doctest
|
||||
if doctest.testmod().failed:
|
||||
exit(1)
|
||||
|
||||
37
src/api/python/z3poly.py
Normal file
37
src/api/python/z3poly.py
Normal file
|
|
@ -0,0 +1,37 @@
|
|||
############################################
|
||||
# Copyright (c) 2012 Microsoft Corporation
|
||||
#
|
||||
# Z3 Python interface for Z3 polynomials
|
||||
#
|
||||
# Author: Leonardo de Moura (leonardo)
|
||||
############################################
|
||||
from z3 import *
|
||||
|
||||
def subresultants(p, q, x):
|
||||
"""
|
||||
Return the non-constant subresultants of 'p' and 'q' with respect to the "variable" 'x'.
|
||||
|
||||
'p', 'q' and 'x' are Z3 expressions where 'p' and 'q' are arithmetic terms.
|
||||
Note that, any subterm that cannot be viewed as a polynomial is assumed to be a variable.
|
||||
Example: f(a) is a considered to be a variable b in the polynomial
|
||||
|
||||
f(a)*f(a) + 2*f(a) + 1
|
||||
|
||||
>>> x, y = Reals('x y')
|
||||
>>> subresultants(2*x + y, 3*x - 2*y + 2, x)
|
||||
[-7*y + 4]
|
||||
>>> r = subresultants(3*y*x**2 + y**3 + 1, 2*x**3 + y + 3, x)
|
||||
>>> r[0]
|
||||
4*y**9 + 12*y**6 + 27*y**5 + 162*y**4 + 255*y**3 + 4
|
||||
>>> r[1]
|
||||
-6*y**4 + -6*y
|
||||
"""
|
||||
return AstVector(Z3_polynomial_subresultants(p.ctx_ref(), p.as_ast(), q.as_ast(), x.as_ast()), p.ctx)
|
||||
|
||||
if __name__ == "__main__":
|
||||
import doctest
|
||||
if doctest.testmod().failed:
|
||||
exit(1)
|
||||
|
||||
|
||||
|
||||
|
|
@ -24,6 +24,8 @@ Notes:
|
|||
#include<stdio.h>
|
||||
#include"z3_macros.h"
|
||||
#include"z3_api.h"
|
||||
#include"z3_algebraic.h"
|
||||
#include"z3_polynomial.h"
|
||||
|
||||
#undef __in
|
||||
#undef __out
|
||||
|
|
|
|||
226
src/api/z3_algebraic.h
Normal file
226
src/api/z3_algebraic.h
Normal file
|
|
@ -0,0 +1,226 @@
|
|||
/*++
|
||||
Copyright (c) 2012 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
z3_algebraic.h
|
||||
|
||||
Abstract:
|
||||
|
||||
Additional APIs for handling Z3 algebraic numbers encoded as
|
||||
Z3_ASTs
|
||||
|
||||
Author:
|
||||
|
||||
Leonardo de Moura (leonardo) 2012-12-07
|
||||
|
||||
Notes:
|
||||
|
||||
--*/
|
||||
|
||||
#ifndef _Z3_ALGEBRAIC_H_
|
||||
#define _Z3_ALGEBRAIC_H_
|
||||
|
||||
#ifdef __cplusplus
|
||||
extern "C" {
|
||||
#endif // __cplusplus
|
||||
|
||||
/**
|
||||
\brief Return Z3_TRUE if \c can be used as value in the Z3 real algebraic
|
||||
number package.
|
||||
|
||||
def_API('Z3_algebraic_is_value', BOOL, (_in(CONTEXT), _in(AST)))
|
||||
*/
|
||||
Z3_bool Z3_API Z3_algebraic_is_value(__in Z3_context c, __in Z3_ast a);
|
||||
|
||||
/**
|
||||
\brief Return the Z3_TRUE if \c a is positive, and Z3_FALSE otherwise.
|
||||
|
||||
\pre Z3_algebraic_is_value(c, a)
|
||||
|
||||
def_API('Z3_algebraic_is_pos', BOOL, (_in(CONTEXT), _in(AST)))
|
||||
*/
|
||||
Z3_bool Z3_API Z3_algebraic_is_pos(__in Z3_context c, __in Z3_ast a);
|
||||
|
||||
/**
|
||||
\brief Return the Z3_TRUE if \c a is negative, and Z3_FALSE otherwise.
|
||||
|
||||
\pre Z3_algebraic_is_value(c, a)
|
||||
|
||||
def_API('Z3_algebraic_is_neg', BOOL, (_in(CONTEXT), _in(AST)))
|
||||
*/
|
||||
Z3_bool Z3_API Z3_algebraic_is_neg(__in Z3_context c, __in Z3_ast a);
|
||||
|
||||
/**
|
||||
\brief Return the Z3_TRUE if \c a is zero, and Z3_FALSE otherwise.
|
||||
|
||||
\pre Z3_algebraic_is_value(c, a)
|
||||
|
||||
def_API('Z3_algebraic_is_zero', BOOL, (_in(CONTEXT), _in(AST)))
|
||||
*/
|
||||
Z3_bool Z3_API Z3_algebraic_is_zero(__in Z3_context c, __in Z3_ast a);
|
||||
|
||||
/**
|
||||
\brief Return 1 if \c a is positive, 0 if \c a is zero, and -1 if \c a is negative.
|
||||
|
||||
\pre Z3_algebraic_is_value(c, a)
|
||||
|
||||
def_API('Z3_algebraic_sign', INT, (_in(CONTEXT), _in(AST)))
|
||||
*/
|
||||
int Z3_API Z3_algebraic_sign(__in Z3_context c, __in Z3_ast a);
|
||||
|
||||
/**
|
||||
\brief Return the value a + b.
|
||||
|
||||
\pre Z3_algebraic_is_value(c, a)
|
||||
\pre Z3_algebraic_is_value(c, b)
|
||||
\post Z3_algebraic_is_value(c, result)
|
||||
|
||||
def_API('Z3_algebraic_add', AST, (_in(CONTEXT), _in(AST), _in(AST)))
|
||||
*/
|
||||
Z3_ast Z3_API Z3_algebraic_add(__in Z3_context c, __in Z3_ast a, __in Z3_ast b);
|
||||
|
||||
/**
|
||||
\brief Return the value a - b.
|
||||
|
||||
\pre Z3_algebraic_is_value(c, a)
|
||||
\pre Z3_algebraic_is_value(c, b)
|
||||
\post Z3_algebraic_is_value(c, result)
|
||||
|
||||
def_API('Z3_algebraic_sub', AST, (_in(CONTEXT), _in(AST), _in(AST)))
|
||||
*/
|
||||
Z3_ast Z3_API Z3_algebraic_sub(__in Z3_context c, __in Z3_ast a, __in Z3_ast b);
|
||||
|
||||
/**
|
||||
\brief Return the value a * b.
|
||||
|
||||
\pre Z3_algebraic_is_value(c, a)
|
||||
\pre Z3_algebraic_is_value(c, b)
|
||||
\post Z3_algebraic_is_value(c, result)
|
||||
|
||||
def_API('Z3_algebraic_mul', AST, (_in(CONTEXT), _in(AST), _in(AST)))
|
||||
*/
|
||||
Z3_ast Z3_API Z3_algebraic_mul(__in Z3_context c, __in Z3_ast a, __in Z3_ast b);
|
||||
|
||||
/**
|
||||
\brief Return the value a / b.
|
||||
|
||||
\pre Z3_algebraic_is_value(c, a)
|
||||
\pre Z3_algebraic_is_value(c, b)
|
||||
\pre !Z3_algebraic_is_zero(c, b)
|
||||
\post Z3_algebraic_is_value(c, result)
|
||||
|
||||
def_API('Z3_algebraic_div', AST, (_in(CONTEXT), _in(AST), _in(AST)))
|
||||
*/
|
||||
Z3_ast Z3_API Z3_algebraic_div(__in Z3_context c, __in Z3_ast a, __in Z3_ast b);
|
||||
|
||||
/**
|
||||
\brief Return the a^(1/k)
|
||||
|
||||
\pre Z3_algebraic_is_value(c, a)
|
||||
\pre k is even => !Z3_algebraic_is_neg(c, a)
|
||||
\post Z3_algebraic_is_value(c, result)
|
||||
|
||||
def_API('Z3_algebraic_root', AST, (_in(CONTEXT), _in(AST), _in(UINT)))
|
||||
*/
|
||||
Z3_ast Z3_API Z3_algebraic_root(__in Z3_context c, __in Z3_ast a, __in unsigned k);
|
||||
|
||||
/**
|
||||
\brief Return the a^k
|
||||
|
||||
\pre Z3_algebraic_is_value(c, a)
|
||||
\post Z3_algebraic_is_value(c, result)
|
||||
|
||||
def_API('Z3_algebraic_power', AST, (_in(CONTEXT), _in(AST), _in(UINT)))
|
||||
*/
|
||||
Z3_ast Z3_API Z3_algebraic_power(__in Z3_context c, __in Z3_ast a, __in unsigned k);
|
||||
|
||||
/**
|
||||
\brief Return Z3_TRUE if a < b, and Z3_FALSE otherwise.
|
||||
|
||||
\pre Z3_algebraic_is_value(c, a)
|
||||
\pre Z3_algebraic_is_value(c, b)
|
||||
|
||||
def_API('Z3_algebraic_lt', BOOL, (_in(CONTEXT), _in(AST), _in(AST)))
|
||||
*/
|
||||
Z3_bool Z3_API Z3_algebraic_lt(__in Z3_context c, __in Z3_ast a, __in Z3_ast b);
|
||||
|
||||
/**
|
||||
\brief Return Z3_TRUE if a > b, and Z3_FALSE otherwise.
|
||||
|
||||
\pre Z3_algebraic_is_value(c, a)
|
||||
\pre Z3_algebraic_is_value(c, b)
|
||||
|
||||
def_API('Z3_algebraic_gt', BOOL, (_in(CONTEXT), _in(AST), _in(AST)))
|
||||
*/
|
||||
Z3_bool Z3_API Z3_algebraic_gt(__in Z3_context c, __in Z3_ast a, __in Z3_ast b);
|
||||
|
||||
/**
|
||||
\brief Return Z3_TRUE if a <= b, and Z3_FALSE otherwise.
|
||||
|
||||
\pre Z3_algebraic_is_value(c, a)
|
||||
\pre Z3_algebraic_is_value(c, b)
|
||||
|
||||
def_API('Z3_algebraic_le', BOOL, (_in(CONTEXT), _in(AST), _in(AST)))
|
||||
*/
|
||||
Z3_bool Z3_API Z3_algebraic_le(__in Z3_context c, __in Z3_ast a, __in Z3_ast b);
|
||||
|
||||
/**
|
||||
\brief Return Z3_TRUE if a >= b, and Z3_FALSE otherwise.
|
||||
|
||||
\pre Z3_algebraic_is_value(c, a)
|
||||
\pre Z3_algebraic_is_value(c, b)
|
||||
|
||||
def_API('Z3_algebraic_ge', BOOL, (_in(CONTEXT), _in(AST), _in(AST)))
|
||||
*/
|
||||
Z3_bool Z3_API Z3_algebraic_ge(__in Z3_context c, __in Z3_ast a, __in Z3_ast b);
|
||||
|
||||
/**
|
||||
\brief Return Z3_TRUE if a == b, and Z3_FALSE otherwise.
|
||||
|
||||
\pre Z3_algebraic_is_value(c, a)
|
||||
\pre Z3_algebraic_is_value(c, b)
|
||||
|
||||
def_API('Z3_algebraic_eq', BOOL, (_in(CONTEXT), _in(AST), _in(AST)))
|
||||
*/
|
||||
Z3_bool Z3_API Z3_algebraic_eq(__in Z3_context c, __in Z3_ast a, __in Z3_ast b);
|
||||
|
||||
/**
|
||||
\brief Return Z3_TRUE if a != b, and Z3_FALSE otherwise.
|
||||
|
||||
\pre Z3_algebraic_is_value(c, a)
|
||||
\pre Z3_algebraic_is_value(c, b)
|
||||
|
||||
def_API('Z3_algebraic_neq', BOOL, (_in(CONTEXT), _in(AST), _in(AST)))
|
||||
*/
|
||||
Z3_bool Z3_API Z3_algebraic_neq(__in Z3_context c, __in Z3_ast a, __in Z3_ast b);
|
||||
|
||||
/**
|
||||
\brief Given a multivariate polynomial p(x_0, ..., x_{n-1}, x_n), returns the
|
||||
roots of the univariate polynomial p(a[0], ..., a[n-1], x_n).
|
||||
|
||||
\pre p is a Z3 expression that contains only arithmetic terms and free variables.
|
||||
\pre forall i in [0, n) Z3_algebraic_is_value(c, a[i])
|
||||
\post forall r in result Z3_algebraic_is_value(c, result)
|
||||
|
||||
def_API('Z3_algebraic_roots', AST_VECTOR, (_in(CONTEXT), _in(AST), _in(UINT), _in_array(2, AST)))
|
||||
*/
|
||||
Z3_ast_vector Z3_API Z3_algebraic_roots(__in Z3_context c, __in Z3_ast p, __in unsigned n, __in Z3_ast a[]);
|
||||
|
||||
/**
|
||||
\brief Given a multivariate polynomial p(x_0, ..., x_{n-1}), return the
|
||||
sign of p(a[0], ..., a[n-1]).
|
||||
|
||||
\pre p is a Z3 expression that contains only arithmetic terms and free variables.
|
||||
\pre forall i in [0, n) Z3_algebraic_is_value(c, a[i])
|
||||
|
||||
def_API('Z3_algebraic_eval', INT, (_in(CONTEXT), _in(AST), _in(UINT), _in_array(2, AST)))
|
||||
*/
|
||||
int Z3_API Z3_algebraic_eval(__in Z3_context c, __in Z3_ast p, __in unsigned n, __in Z3_ast a[]);
|
||||
|
||||
|
||||
#ifdef __cplusplus
|
||||
};
|
||||
#endif // __cplusplus
|
||||
|
||||
#endif
|
||||
45
src/api/z3_polynomial.h
Normal file
45
src/api/z3_polynomial.h
Normal file
|
|
@ -0,0 +1,45 @@
|
|||
/*++
|
||||
Copyright (c) 2012 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
z3_polynomial.h
|
||||
|
||||
Abstract:
|
||||
|
||||
Additional APIs for polynomials.
|
||||
|
||||
Author:
|
||||
|
||||
Leonardo de Moura (leonardo) 2012-12-09
|
||||
|
||||
Notes:
|
||||
|
||||
--*/
|
||||
|
||||
#ifndef _Z3_POLYNOMIAL_H_
|
||||
#define _Z3_POLYNOMIAL_H_
|
||||
|
||||
#ifdef __cplusplus
|
||||
extern "C" {
|
||||
#endif // __cplusplus
|
||||
|
||||
/**
|
||||
\brief Return the nonzero subresultants of \c p and \c q with respect to the "variable" \c x.
|
||||
|
||||
\pre \c p, \c q and \c x are Z3 expressions where \c p and \c q are arithmetic terms.
|
||||
Note that, any subterm that cannot be viewed as a polynomial is assumed to be a variable.
|
||||
Example: f(a) is a considered to be a variable in the polynomial
|
||||
|
||||
f(a)*f(a) + 2*f(a) + 1
|
||||
|
||||
def_API('Z3_polynomial_subresultants', AST_VECTOR, (_in(CONTEXT), _in(AST), _in(AST), _in(AST)))
|
||||
*/
|
||||
Z3_ast_vector Z3_API Z3_polynomial_subresultants(__in Z3_context c, __in Z3_ast p, __in Z3_ast q, __in Z3_ast x);
|
||||
|
||||
|
||||
#ifdef __cplusplus
|
||||
};
|
||||
#endif // __cplusplus
|
||||
|
||||
#endif
|
||||
|
|
@ -38,13 +38,6 @@ struct arith_decl_plugin::algebraic_numbers_wrapper {
|
|||
|
||||
unsigned mk_id(algebraic_numbers::anum const & val) {
|
||||
SASSERT(!m_amanager.is_rational(val));
|
||||
// TODO: avoid linear scan. Use hashtable based on the floor of val
|
||||
unsigned sz = m_nums.size();
|
||||
for (unsigned i = 0; i < sz; i++) {
|
||||
algebraic_numbers::anum const & other = m_nums.get(i);
|
||||
if (m_amanager.eq(val, other))
|
||||
return i;
|
||||
}
|
||||
unsigned new_id = m_id_gen.mk();
|
||||
m_nums.reserve(new_id+1);
|
||||
m_amanager.set(m_nums[new_id], val);
|
||||
|
|
@ -71,13 +64,13 @@ struct arith_decl_plugin::algebraic_numbers_wrapper {
|
|||
|
||||
};
|
||||
|
||||
arith_decl_plugin::algebraic_numbers_wrapper & arith_decl_plugin::aw() {
|
||||
arith_decl_plugin::algebraic_numbers_wrapper & arith_decl_plugin::aw() const {
|
||||
if (m_aw == 0)
|
||||
m_aw = alloc(algebraic_numbers_wrapper);
|
||||
const_cast<arith_decl_plugin*>(this)->m_aw = alloc(algebraic_numbers_wrapper);
|
||||
return *m_aw;
|
||||
}
|
||||
|
||||
algebraic_numbers::manager & arith_decl_plugin::am() {
|
||||
algebraic_numbers::manager & arith_decl_plugin::am() const {
|
||||
return aw().m_amanager;
|
||||
}
|
||||
|
||||
|
|
@ -509,16 +502,43 @@ void arith_decl_plugin::get_op_names(svector<builtin_name>& op_names, symbol con
|
|||
}
|
||||
}
|
||||
|
||||
bool arith_decl_plugin::is_value(app* e) const {
|
||||
return is_app_of(e, m_family_id, OP_NUM);
|
||||
bool arith_decl_plugin::is_value(app * e) const {
|
||||
return
|
||||
is_app_of(e, m_family_id, OP_NUM) ||
|
||||
is_app_of(e, m_family_id, OP_IRRATIONAL_ALGEBRAIC_NUM) ||
|
||||
is_app_of(e, m_family_id, OP_PI) ||
|
||||
is_app_of(e, m_family_id, OP_E);
|
||||
}
|
||||
|
||||
bool arith_decl_plugin::are_distinct(app* a, app* b) const {
|
||||
bool arith_decl_plugin::is_unique_value(app * e) const {
|
||||
return
|
||||
is_app_of(e, m_family_id, OP_NUM) ||
|
||||
is_app_of(e, m_family_id, OP_PI) ||
|
||||
is_app_of(e, m_family_id, OP_E);
|
||||
}
|
||||
|
||||
bool arith_decl_plugin::are_equal(app * a, app * b) const {
|
||||
if (decl_plugin::are_equal(a, b)) {
|
||||
return true;
|
||||
}
|
||||
|
||||
if (is_app_of(a, m_family_id, OP_IRRATIONAL_ALGEBRAIC_NUM) && is_app_of(b, m_family_id, OP_IRRATIONAL_ALGEBRAIC_NUM)) {
|
||||
return am().eq(aw().to_anum(a->get_decl()), aw().to_anum(b->get_decl()));
|
||||
}
|
||||
|
||||
return false;
|
||||
}
|
||||
|
||||
bool arith_decl_plugin::are_distinct(app * a, app * b) const {
|
||||
TRACE("are_distinct_bug", tout << mk_ismt2_pp(a, *m_manager) << "\n" << mk_ismt2_pp(b, *m_manager) << "\n";);
|
||||
if (decl_plugin::are_distinct(a,b)) {
|
||||
return true;
|
||||
}
|
||||
|
||||
if (is_app_of(a, m_family_id, OP_IRRATIONAL_ALGEBRAIC_NUM) && is_app_of(b, m_family_id, OP_IRRATIONAL_ALGEBRAIC_NUM)) {
|
||||
return am().neq(aw().to_anum(a->get_decl()), aw().to_anum(b->get_decl()));
|
||||
}
|
||||
|
||||
#define is_non_zero(e) is_app_of(e,m_family_id, OP_NUM) && !to_app(e)->get_decl()->get_parameter(0).get_rational().is_zero()
|
||||
|
||||
if (is_app_of(a, m_family_id, OP_ADD) &&
|
||||
|
|
|
|||
|
|
@ -141,8 +141,8 @@ public:
|
|||
virtual ~arith_decl_plugin();
|
||||
virtual void finalize();
|
||||
|
||||
algebraic_numbers::manager & am();
|
||||
algebraic_numbers_wrapper & aw();
|
||||
algebraic_numbers::manager & am() const;
|
||||
algebraic_numbers_wrapper & aw() const;
|
||||
|
||||
virtual void del(parameter const & p);
|
||||
virtual parameter translate(parameter const & p, decl_plugin & target);
|
||||
|
|
@ -159,9 +159,13 @@ public:
|
|||
virtual func_decl * mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters,
|
||||
unsigned num_args, expr * const * args, sort * range);
|
||||
|
||||
virtual bool is_value(app* e) const;
|
||||
virtual bool is_value(app * e) const;
|
||||
|
||||
virtual bool are_distinct(app* a, app* b) const;
|
||||
virtual bool is_unique_value(app * e) const;
|
||||
|
||||
virtual bool are_equal(app * a, app * b) const;
|
||||
|
||||
virtual bool are_distinct(app * a, app * b) const;
|
||||
|
||||
virtual void get_op_names(svector<builtin_name> & op_names, symbol const & logic);
|
||||
|
||||
|
|
@ -180,7 +184,7 @@ public:
|
|||
|
||||
virtual expr * get_some_value(sort * s);
|
||||
|
||||
void set_cancel(bool f);
|
||||
virtual void set_cancel(bool f);
|
||||
};
|
||||
|
||||
class arith_util {
|
||||
|
|
|
|||
|
|
@ -872,6 +872,10 @@ bool basic_decl_plugin::is_value(app* a) const {
|
|||
return a->get_decl() == m_true_decl || a->get_decl() == m_false_decl;
|
||||
}
|
||||
|
||||
bool basic_decl_plugin::is_unique_value(app* a) const {
|
||||
return is_value(a);
|
||||
}
|
||||
|
||||
void basic_decl_plugin::finalize() {
|
||||
#define DEC_REF(FIELD) if (FIELD) { m_manager->dec_ref(FIELD); }
|
||||
#define DEC_ARRAY_REF(FIELD) m_manager->dec_array_ref(FIELD.size(), FIELD.begin())
|
||||
|
|
@ -1151,6 +1155,10 @@ bool model_value_decl_plugin::is_value(app* n) const {
|
|||
return is_app_of(n, m_family_id, OP_MODEL_VALUE);
|
||||
}
|
||||
|
||||
bool model_value_decl_plugin::is_unique_value(app* n) const {
|
||||
return is_value(n);
|
||||
}
|
||||
|
||||
// -----------------------------------
|
||||
//
|
||||
// user_sort_plugin
|
||||
|
|
@ -1328,6 +1336,12 @@ ast_manager::~ast_manager() {
|
|||
}
|
||||
}
|
||||
|
||||
void ast_manager::set_cancel(bool f) {
|
||||
for (unsigned i = 0; i < m_plugins.size(); i++) {
|
||||
m_plugins[i]->set_cancel(f);
|
||||
}
|
||||
}
|
||||
|
||||
void ast_manager::compact_memory() {
|
||||
m_alloc.consolidate();
|
||||
unsigned capacity = m_ast_table.capacity();
|
||||
|
|
@ -1442,6 +1456,27 @@ bool ast_manager::is_value(expr* e) const {
|
|||
return false;
|
||||
}
|
||||
|
||||
bool ast_manager::is_unique_value(expr* e) const {
|
||||
decl_plugin const * p = 0;
|
||||
if (is_app(e)) {
|
||||
p = get_plugin(to_app(e)->get_family_id());
|
||||
return p && p->is_unique_value(to_app(e));
|
||||
}
|
||||
return false;
|
||||
}
|
||||
|
||||
bool ast_manager::are_equal(expr * a, expr * b) const {
|
||||
if (is_app(a) && is_app(b)) {
|
||||
app* ap = to_app(a), *bp = to_app(b);
|
||||
decl_plugin const * p = get_plugin(ap->get_family_id());
|
||||
if (!p) {
|
||||
p = get_plugin(bp->get_family_id());
|
||||
}
|
||||
return p && p->are_equal(ap, bp);
|
||||
}
|
||||
return false;
|
||||
}
|
||||
|
||||
bool ast_manager::are_distinct(expr* a, expr* b) const {
|
||||
if (is_app(a) && is_app(b)) {
|
||||
app* ap = to_app(a), *bp = to_app(b);
|
||||
|
|
|
|||
|
|
@ -921,6 +921,8 @@ public:
|
|||
virtual ~decl_plugin() {}
|
||||
virtual void finalize() {}
|
||||
|
||||
virtual void set_cancel(bool f) {}
|
||||
|
||||
virtual decl_plugin * mk_fresh() = 0;
|
||||
|
||||
family_id get_family_id() const { return m_family_id; }
|
||||
|
|
@ -933,9 +935,39 @@ public:
|
|||
virtual func_decl * mk_func_decl(decl_kind k, unsigned num_parameters, parameter const* parameters,
|
||||
unsigned num_args, expr * const * args, sort * range);
|
||||
|
||||
virtual bool is_value(app*) const { return false; }
|
||||
/**
|
||||
\brief Return true if the plugin can decide whether two
|
||||
interpreted constants are equal or not.
|
||||
|
||||
For all a, b:
|
||||
If is_value(a) and is_value(b)
|
||||
Then,
|
||||
are_equal(a, b) != are_distinct(a, b)
|
||||
|
||||
The may be much more expensive than checking a pointer.
|
||||
|
||||
virtual bool are_distinct(app* a, app* b) const { return a != b && is_value(a) && is_value(b); }
|
||||
We need this because some plugin values are too expensive too canonize.
|
||||
*/
|
||||
virtual bool is_value(app * a) const { return false; }
|
||||
|
||||
/**
|
||||
\brief Return true if \c a is a unique plugin value.
|
||||
The following property should hold for unique theory values:
|
||||
|
||||
For all a, b:
|
||||
If is_unique_value(a) and is_unique_value(b)
|
||||
Then,
|
||||
a == b (pointer equality)
|
||||
IFF
|
||||
the interpretations of these theory terms are equal.
|
||||
|
||||
\remark This is a stronger version of is_value.
|
||||
*/
|
||||
virtual bool is_unique_value(app * a) const { return false; }
|
||||
|
||||
virtual bool are_equal(app * a, app * b) const { return a == b && is_unique_value(a) && is_unique_value(b); }
|
||||
|
||||
virtual bool are_distinct(app * a, app * b) const { return a != b && is_unique_value(a) && is_unique_value(b); }
|
||||
|
||||
virtual void get_op_names(svector<builtin_name> & op_names, symbol const & logic = symbol()) {}
|
||||
|
||||
|
|
@ -1080,6 +1112,8 @@ public:
|
|||
virtual void get_sort_names(svector<builtin_name> & sort_names, symbol const & logic);
|
||||
|
||||
virtual bool is_value(app* a) const;
|
||||
|
||||
virtual bool is_unique_value(app* a) const;
|
||||
|
||||
sort * mk_bool_sort() const { return m_bool_sort; }
|
||||
sort * mk_proof_sort() const { return m_proof_sort; }
|
||||
|
|
@ -1116,7 +1150,6 @@ public:
|
|||
|
||||
virtual decl_plugin * mk_fresh() { return alloc(label_decl_plugin); }
|
||||
|
||||
|
||||
virtual sort * mk_sort(decl_kind k, unsigned num_parameters, parameter const * parameters);
|
||||
|
||||
/**
|
||||
|
|
@ -1198,6 +1231,8 @@ public:
|
|||
unsigned arity, sort * const * domain, sort * range);
|
||||
|
||||
virtual bool is_value(app* n) const;
|
||||
|
||||
virtual bool is_unique_value(app* a) const;
|
||||
};
|
||||
|
||||
// -----------------------------------
|
||||
|
|
@ -1367,6 +1402,9 @@ public:
|
|||
ast_manager(ast_manager const & src, bool disable_proofs = false);
|
||||
~ast_manager();
|
||||
|
||||
// propagate cancellation signal to decl_plugins
|
||||
void set_cancel(bool f);
|
||||
|
||||
bool has_trace_stream() const { return m_trace_stream != 0; }
|
||||
std::ostream & trace_stream() { SASSERT(has_trace_stream()); return *m_trace_stream; }
|
||||
|
||||
|
|
@ -1442,9 +1480,13 @@ public:
|
|||
*/
|
||||
void set_next_expr_id(unsigned id);
|
||||
|
||||
bool is_value(expr* e) const;
|
||||
bool is_value(expr * e) const;
|
||||
|
||||
bool is_unique_value(expr * e) const;
|
||||
|
||||
bool are_distinct(expr* a, expr* b) const;
|
||||
bool are_equal(expr * a, expr * b) const;
|
||||
|
||||
bool are_distinct(expr * a, expr * b) const;
|
||||
|
||||
bool contains(ast * a) const { return m_ast_table.contains(a); }
|
||||
|
||||
|
|
|
|||
|
|
@ -260,8 +260,10 @@ public:
|
|||
virtual func_decl * mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters,
|
||||
unsigned num_args, expr * const * args, sort * range);
|
||||
|
||||
virtual bool is_value(app* e) const;
|
||||
virtual bool is_value(app * e) const;
|
||||
|
||||
virtual bool is_unique_value(app * e) const { return is_value(e); }
|
||||
|
||||
virtual void get_op_names(svector<builtin_name> & op_names, symbol const & logic);
|
||||
|
||||
virtual void get_sort_names(svector<builtin_name> & sort_names, symbol const & logic);
|
||||
|
|
|
|||
|
|
@ -146,6 +146,9 @@ public:
|
|||
virtual bool is_fully_interp(sort const * s) const;
|
||||
|
||||
virtual bool is_value(app* e) const;
|
||||
|
||||
virtual bool is_unique_value(app * e) const { return is_value(e); }
|
||||
|
||||
private:
|
||||
bool is_value_visit(expr * arg, ptr_buffer<app> & todo) const;
|
||||
};
|
||||
|
|
|
|||
|
|
@ -130,7 +130,8 @@ namespace datalog {
|
|||
|
||||
virtual void get_sort_names(svector<builtin_name> & sort_names, symbol const & logic);
|
||||
|
||||
virtual bool is_value(app* e) const { return is_app_of(e, m_family_id, OP_DL_CONSTANT); }
|
||||
virtual bool is_value(app * e) const { return is_app_of(e, m_family_id, OP_DL_CONSTANT); }
|
||||
virtual bool is_unique_value(app * e) const { return is_value(e); }
|
||||
|
||||
};
|
||||
|
||||
|
|
|
|||
|
|
@ -49,21 +49,24 @@ struct expr2polynomial::imp {
|
|||
polynomial::polynomial_ref_vector m_presult_stack;
|
||||
polynomial::scoped_numeral_vector m_dresult_stack;
|
||||
|
||||
bool m_use_var_idxs;
|
||||
|
||||
volatile bool m_cancel;
|
||||
|
||||
imp(expr2polynomial & w, ast_manager & am, polynomial::manager & pm, expr2var * e2v):
|
||||
imp(expr2polynomial & w, ast_manager & am, polynomial::manager & pm, expr2var * e2v, bool use_var_idxs):
|
||||
m_wrapper(w),
|
||||
m_am(am),
|
||||
m_autil(am),
|
||||
m_pm(pm),
|
||||
m_expr2var(e2v == 0 ? alloc(expr2var, am) : e2v),
|
||||
m_expr2var_owner(e2v == 0),
|
||||
m_expr2var(e2v == 0 && !use_var_idxs ? alloc(expr2var, am) : e2v),
|
||||
m_expr2var_owner(e2v == 0 && !use_var_idxs),
|
||||
m_var2expr(am),
|
||||
m_cached_domain(am),
|
||||
m_cached_polynomials(pm),
|
||||
m_cached_denominators(pm.m()),
|
||||
m_presult_stack(pm),
|
||||
m_dresult_stack(pm.m()),
|
||||
m_use_var_idxs(use_var_idxs),
|
||||
m_cancel(false) {
|
||||
}
|
||||
|
||||
|
|
@ -95,6 +98,14 @@ struct expr2polynomial::imp {
|
|||
cooperate("expr2polynomial");
|
||||
}
|
||||
|
||||
void throw_not_polynomial() {
|
||||
throw default_exception("the given expression is not a polynomial");
|
||||
}
|
||||
|
||||
void throw_no_int_var() {
|
||||
throw default_exception("integer variables are not allowed in the given polynomial");
|
||||
}
|
||||
|
||||
void push_frame(app * t) {
|
||||
m_frame_stack.push_back(frame(t));
|
||||
}
|
||||
|
|
@ -127,14 +138,26 @@ struct expr2polynomial::imp {
|
|||
}
|
||||
|
||||
void store_var_poly(expr * t) {
|
||||
polynomial::var x = m_expr2var->to_var(t);
|
||||
if (x == UINT_MAX) {
|
||||
bool is_int = m_autil.is_int(t);
|
||||
x = m_wrapper.mk_var(is_int);
|
||||
m_expr2var->insert(t, x);
|
||||
if (x >= m_var2expr.size())
|
||||
m_var2expr.resize(x+1, 0);
|
||||
m_var2expr.set(x, t);
|
||||
polynomial::var x;
|
||||
if (m_use_var_idxs) {
|
||||
SASSERT(::is_var(t));
|
||||
if (m_autil.is_int(t))
|
||||
throw_no_int_var();
|
||||
unsigned idx = to_var(t)->get_idx();
|
||||
while (idx >= m_pm.num_vars())
|
||||
m_pm.mk_var();
|
||||
x = static_cast<polynomial::var>(idx);
|
||||
}
|
||||
else {
|
||||
x = m_expr2var->to_var(t);
|
||||
if (x == UINT_MAX) {
|
||||
bool is_int = m_autil.is_int(t);
|
||||
x = m_wrapper.mk_var(is_int);
|
||||
m_expr2var->insert(t, x);
|
||||
if (x >= m_var2expr.size())
|
||||
m_var2expr.resize(x+1, 0);
|
||||
m_var2expr.set(x, t);
|
||||
}
|
||||
}
|
||||
polynomial::numeral one(1);
|
||||
store_result(t, pm().mk_polynomial(x), one);
|
||||
|
|
@ -160,7 +183,10 @@ struct expr2polynomial::imp {
|
|||
rational k;
|
||||
SASSERT(t->get_num_args() == 2);
|
||||
if (!m_autil.is_numeral(t->get_arg(1), k) || !k.is_int() || !k.is_unsigned()) {
|
||||
store_var_poly(t);
|
||||
if (m_use_var_idxs)
|
||||
throw_not_polynomial();
|
||||
else
|
||||
store_var_poly(t);
|
||||
return true;
|
||||
}
|
||||
push_frame(t);
|
||||
|
|
@ -168,6 +194,8 @@ struct expr2polynomial::imp {
|
|||
}
|
||||
default:
|
||||
// can't handle operator
|
||||
if (m_use_var_idxs)
|
||||
throw_not_polynomial();
|
||||
store_var_poly(t);
|
||||
return true;
|
||||
}
|
||||
|
|
@ -190,6 +218,8 @@ struct expr2polynomial::imp {
|
|||
|
||||
SASSERT(is_app(t));
|
||||
if (!m_autil.is_arith_expr(t)) {
|
||||
if (m_use_var_idxs)
|
||||
throw_not_polynomial();
|
||||
store_var_poly(t);
|
||||
return true;
|
||||
}
|
||||
|
|
@ -378,19 +408,25 @@ struct expr2polynomial::imp {
|
|||
|
||||
for (unsigned i = 0; i < sz; i++) {
|
||||
margs.reset();
|
||||
polynomial::monomial * m = pm().get_monomial(p, i);
|
||||
polynomial::monomial * _m = pm().get_monomial(p, i);
|
||||
polynomial::numeral const & a = pm().coeff(p, i);
|
||||
if (!nm().is_one(a)) {
|
||||
margs.push_back(m_autil.mk_numeral(rational(a), is_int));
|
||||
}
|
||||
unsigned msz = pm().size(m);
|
||||
unsigned msz = pm().size(_m);
|
||||
for (unsigned j = 0; j < msz; j++) {
|
||||
polynomial::var x = pm().get_var(m, j);
|
||||
expr * t = m_var2expr.get(x);
|
||||
if (m_wrapper.is_int(x) && !is_int) {
|
||||
t = m_autil.mk_to_real(t);
|
||||
polynomial::var x = pm().get_var(_m, j);
|
||||
expr * t;
|
||||
if (m_use_var_idxs) {
|
||||
t = m().mk_var(x, m_autil.mk_real());
|
||||
}
|
||||
unsigned d = pm().degree(m, j);
|
||||
else {
|
||||
t = m_var2expr.get(x);
|
||||
if (m_wrapper.is_int(x) && !is_int) {
|
||||
t = m_autil.mk_to_real(t);
|
||||
}
|
||||
}
|
||||
unsigned d = pm().degree(_m, j);
|
||||
if (use_power && d > 1) {
|
||||
margs.push_back(m_autil.mk_power(t, m_autil.mk_numeral(rational(d), is_int)));
|
||||
}
|
||||
|
|
@ -426,8 +462,8 @@ struct expr2polynomial::imp {
|
|||
}
|
||||
};
|
||||
|
||||
expr2polynomial::expr2polynomial(ast_manager & am, polynomial::manager & pm, expr2var * e2v) {
|
||||
m_imp = alloc(imp, *this, am, pm, e2v);
|
||||
expr2polynomial::expr2polynomial(ast_manager & am, polynomial::manager & pm, expr2var * e2v, bool use_var_idxs) {
|
||||
m_imp = alloc(imp, *this, am, pm, e2v, use_var_idxs);
|
||||
}
|
||||
|
||||
expr2polynomial::~expr2polynomial() {
|
||||
|
|
@ -451,10 +487,12 @@ void expr2polynomial::to_expr(polynomial::polynomial_ref const & p, bool use_pow
|
|||
}
|
||||
|
||||
bool expr2polynomial::is_var(expr * t) const {
|
||||
SASSERT(!m_imp->m_use_var_idxs);
|
||||
return m_imp->m_expr2var->is_var(t);
|
||||
}
|
||||
|
||||
expr2var const & expr2polynomial::get_mapping() const {
|
||||
SASSERT(!m_imp->m_use_var_idxs);
|
||||
return *(m_imp->m_expr2var);
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -29,7 +29,24 @@ class expr2polynomial {
|
|||
struct imp;
|
||||
imp * m_imp;
|
||||
public:
|
||||
expr2polynomial(ast_manager & am, polynomial::manager & pm, expr2var * e2v);
|
||||
expr2polynomial(ast_manager & am,
|
||||
polynomial::manager & pm,
|
||||
expr2var * e2v,
|
||||
/*
|
||||
If true, the expressions converted into
|
||||
polynomials should only contain Z3 free variables.
|
||||
A Z3 variable x, with idx i, is converted into
|
||||
the variable i of the polynomial manager pm.
|
||||
|
||||
An exception is thrown if there is a mismatch between
|
||||
the sorts x and the variable in the polynomial manager.
|
||||
|
||||
The argument e2v is ignored when use_var_idxs is true.
|
||||
|
||||
Moreover, only real variables are allowed.
|
||||
*/
|
||||
bool use_var_idxs = false
|
||||
);
|
||||
virtual ~expr2polynomial();
|
||||
|
||||
ast_manager & m() const;
|
||||
|
|
@ -63,6 +80,8 @@ public:
|
|||
|
||||
/**
|
||||
\brief Return the mapping from expressions to variables
|
||||
|
||||
\pre the object was created using use_var_idxs = false.
|
||||
*/
|
||||
expr2var const & get_mapping() const;
|
||||
|
||||
|
|
@ -74,10 +93,10 @@ public:
|
|||
/**
|
||||
\brief Return true if the variable is associated with an expression of integer sort.
|
||||
*/
|
||||
virtual bool is_int(polynomial::var x) const = 0;
|
||||
virtual bool is_int(polynomial::var x) const { UNREACHABLE(); return false; }
|
||||
|
||||
protected:
|
||||
virtual polynomial::var mk_var(bool is_int) = 0;
|
||||
virtual polynomial::var mk_var(bool is_int) { UNREACHABLE(); return polynomial::null_var; }
|
||||
};
|
||||
|
||||
class default_expr2polynomial : public expr2polynomial {
|
||||
|
|
|
|||
|
|
@ -141,6 +141,7 @@ public:
|
|||
virtual void get_op_names(svector<builtin_name> & op_names, symbol const & logic);
|
||||
virtual void get_sort_names(svector<builtin_name> & sort_names, symbol const & logic);
|
||||
virtual bool is_value(app* e) const;
|
||||
virtual bool is_unique_value(app* e) const { return is_value(e); }
|
||||
|
||||
mpf_manager & fm() { return m_fm; }
|
||||
func_decl * mk_value_decl(mpf const & v);
|
||||
|
|
|
|||
|
|
@ -5,7 +5,7 @@ def_module_params(class_name='pattern_inference_params_helper',
|
|||
params=(('max_multi_patterns', UINT, 0, 'when patterns are not provided, the prover uses a heuristic to infer them, this option sets the threshold on the number of extra multi-patterns that can be created; by default, the prover creates at most one multi-pattern when there is no unary pattern'),
|
||||
('block_loop_patterns', BOOL, True, 'block looping patterns during pattern inference'),
|
||||
('arith', UINT, 1, '0 - do not infer patterns with arithmetic terms, 1 - use patterns with arithmetic terms if there is no other pattern, 2 - always use patterns with arithmetic terms'),
|
||||
('use_database', BOOL, True, 'use pattern database'),
|
||||
('use_database', BOOL, False, 'use pattern database'),
|
||||
('arith_weight', UINT, 5, 'default weight for quantifiers where the only available pattern has nested arithmetic terms'),
|
||||
('non_nested_arith_weight', UINT, 10, 'default weight for quantifiers where the only available pattern has non nested arithmetic terms'),
|
||||
('pull_quantifiers', BOOL, True, 'pull nested quantifiers, if no pattern was found'),
|
||||
|
|
|
|||
|
|
@ -732,7 +732,7 @@ br_status bool_rewriter::mk_distinct_core(unsigned num_args, expr * const * args
|
|||
return BR_DONE;
|
||||
}
|
||||
visited.mark(arg);
|
||||
if (!m().is_value(arg))
|
||||
if (!m().is_unique_value(arg))
|
||||
all_value = false;
|
||||
}
|
||||
if (all_value) {
|
||||
|
|
|
|||
|
|
@ -200,7 +200,12 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
|
|||
expr * mk_eq_value(expr * lhs, expr * value) {
|
||||
SASSERT(m().is_value(value));
|
||||
if (m().is_value(lhs)) {
|
||||
return lhs == value ? m().mk_true() : m().mk_false();
|
||||
if (m().are_equal(lhs, value)) {
|
||||
return m().mk_true();
|
||||
}
|
||||
else if (m().are_distinct(lhs, value)) {
|
||||
return m().mk_false();
|
||||
}
|
||||
}
|
||||
return m().mk_eq(lhs, value);
|
||||
}
|
||||
|
|
|
|||
|
|
@ -112,7 +112,10 @@ public:
|
|||
|
||||
virtual void get_sort_names(svector<builtin_name> & sort_names, symbol const & logic);
|
||||
|
||||
virtual bool is_value(app* e) const;
|
||||
virtual bool is_value(app * e) const;
|
||||
|
||||
virtual bool is_unique_value(app * e) const { return is_value(e); }
|
||||
|
||||
|
||||
};
|
||||
|
||||
|
|
|
|||
|
|
@ -293,7 +293,7 @@ bool array_simplifier_plugin::all_const_array(unsigned num_args, expr* const* ar
|
|||
|
||||
bool array_simplifier_plugin::all_values(unsigned num_args, expr* const* args) const {
|
||||
for (unsigned i = 0; i < num_args; ++i) {
|
||||
if (!m_manager.is_value(args[i])) {
|
||||
if (!m_manager.is_unique_value(args[i])) {
|
||||
return false;
|
||||
}
|
||||
}
|
||||
|
|
@ -331,7 +331,7 @@ lbool array_simplifier_plugin::eq_default(expr* def, unsigned arity, unsigned nu
|
|||
if (st[i][arity] == def) {
|
||||
continue;
|
||||
}
|
||||
if (m_manager.is_value(st[i][arity]) && m_manager.is_value(def)) {
|
||||
if (m_manager.is_unique_value(st[i][arity]) && m_manager.is_unique_value(def)) {
|
||||
return l_false;
|
||||
}
|
||||
return l_undef;
|
||||
|
|
@ -342,7 +342,7 @@ lbool array_simplifier_plugin::eq_default(expr* def, unsigned arity, unsigned nu
|
|||
bool array_simplifier_plugin::insert_table(expr* def, unsigned arity, unsigned num_st, expr*const* const* st, arg_table& table) {
|
||||
for (unsigned i = 0; i < num_st; ++i ) {
|
||||
for (unsigned j = 0; j < arity; ++j) {
|
||||
if (!m_manager.is_value(st[i][j])) {
|
||||
if (!m_manager.is_unique_value(st[i][j])) {
|
||||
return false;
|
||||
}
|
||||
}
|
||||
|
|
@ -380,12 +380,12 @@ lbool array_simplifier_plugin::eq_stores(expr* def, unsigned arity, unsigned num
|
|||
table2.erase(e1);
|
||||
continue;
|
||||
}
|
||||
if (m_manager.is_value(v1) && m_manager.is_value(v2)) {
|
||||
if (m_manager.is_unique_value(v1) && m_manager.is_unique_value(v2)) {
|
||||
return l_false;
|
||||
}
|
||||
return l_undef;
|
||||
}
|
||||
else if (m_manager.is_value(v1) && m_manager.is_value(def) && v1 != def) {
|
||||
else if (m_manager.is_unique_value(v1) && m_manager.is_unique_value(def) && v1 != def) {
|
||||
return l_false;
|
||||
}
|
||||
}
|
||||
|
|
@ -394,7 +394,7 @@ lbool array_simplifier_plugin::eq_stores(expr* def, unsigned arity, unsigned num
|
|||
for (; it != end; ++it) {
|
||||
args_entry const & e = *it;
|
||||
expr* v = e.m_args[arity];
|
||||
if (m_manager.is_value(v) && m_manager.is_value(def) && v != def) {
|
||||
if (m_manager.is_unique_value(v) && m_manager.is_unique_value(def) && v != def) {
|
||||
return l_false;
|
||||
}
|
||||
}
|
||||
|
|
@ -431,7 +431,7 @@ bool array_simplifier_plugin::reduce_eq(expr * lhs, expr * rhs, expr_ref & resul
|
|||
return false;
|
||||
}
|
||||
}
|
||||
else if (m_manager.is_value(c1) && m_manager.is_value(c2)) {
|
||||
else if (m_manager.is_unique_value(c1) && m_manager.is_unique_value(c2)) {
|
||||
result = m_manager.mk_false();
|
||||
return true;
|
||||
}
|
||||
|
|
@ -464,7 +464,7 @@ array_simplifier_plugin::mk_select_const(expr* m, app* index, expr_ref& result)
|
|||
//
|
||||
// Unfold and cache the store while searching for value of index.
|
||||
//
|
||||
while (is_store(a) && m_manager.is_value(to_app(a)->get_arg(1))) {
|
||||
while (is_store(a) && m_manager.is_unique_value(to_app(a)->get_arg(1))) {
|
||||
app* b = to_app(a);
|
||||
app* c = to_app(b->get_arg(1));
|
||||
|
||||
|
|
@ -728,7 +728,7 @@ void array_simplifier_plugin::mk_select(unsigned num_args, expr * const * args,
|
|||
return;
|
||||
}
|
||||
|
||||
bool is_const_select = num_args == 2 && m_manager.is_value(args[1]);
|
||||
bool is_const_select = num_args == 2 && m_manager.is_unique_value(args[1]);
|
||||
app* const_index = is_const_select?to_app(args[1]):0;
|
||||
unsigned num_const_stores = 0;
|
||||
expr_ref tmp(m_manager);
|
||||
|
|
@ -766,7 +766,7 @@ void array_simplifier_plugin::mk_select(unsigned num_args, expr * const * args,
|
|||
expr * else_branch = 0;
|
||||
entry[0] = nested_array;
|
||||
if (is_const_select) {
|
||||
if (m_manager.is_value(to_app(m)->get_arg(1))) {
|
||||
if (m_manager.is_unique_value(to_app(m)->get_arg(1))) {
|
||||
app* const_index2 = to_app(to_app(m)->get_arg(1));
|
||||
//
|
||||
// we found the value, all other stores are different.
|
||||
|
|
|
|||
|
|
@ -37,6 +37,7 @@ Notes:
|
|||
#include"well_sorted.h"
|
||||
#include"model_evaluator.h"
|
||||
#include"for_each_expr.h"
|
||||
#include"scoped_timer.h"
|
||||
|
||||
func_decls::func_decls(ast_manager & m, func_decl * f):
|
||||
m_decls(TAG(func_decl*, f, 0)) {
|
||||
|
|
@ -591,14 +592,9 @@ void cmd_context::init_manager() {
|
|||
SASSERT(m_manager == 0);
|
||||
SASSERT(m_pmanager == 0);
|
||||
m_check_sat_result = 0;
|
||||
m_manager = alloc(ast_manager,
|
||||
produce_proofs() ? PGM_FINE : PGM_DISABLED,
|
||||
m_params.m_trace ? m_params.m_trace_file_name.c_str() : 0);
|
||||
m_manager = m_params.mk_ast_manager();
|
||||
m_pmanager = alloc(pdecl_manager, *m_manager);
|
||||
init_manager_core(true);
|
||||
// PARAM-TODO
|
||||
// if (params().m_smtlib2_compliant)
|
||||
// m_manager->enable_int_real_coercions(false);
|
||||
}
|
||||
|
||||
void cmd_context::init_external_manager() {
|
||||
|
|
@ -1304,9 +1300,11 @@ void cmd_context::check_sat(unsigned num_assumptions, expr * const * assumptions
|
|||
if (m_solver) {
|
||||
m_check_sat_result = m_solver.get(); // solver itself stores the result.
|
||||
m_solver->set_progress_callback(this);
|
||||
unsigned timeout = m_params.m_timeout;
|
||||
scoped_watch sw(*this);
|
||||
cancel_eh<solver> eh(*m_solver);
|
||||
scoped_ctrl_c ctrlc(eh);
|
||||
scoped_timer timer(timeout, &eh);
|
||||
lbool r;
|
||||
try {
|
||||
r = m_solver->check_sat(num_assumptions, assumptions);
|
||||
|
|
@ -1444,15 +1442,9 @@ void cmd_context::validate_model() {
|
|||
}
|
||||
|
||||
void cmd_context::init_solver_options(solver * s) {
|
||||
m_solver->set_produce_unsat_cores(produce_unsat_cores());
|
||||
m_solver->set_produce_models(produce_models());
|
||||
m_solver->set_produce_proofs(produce_proofs());
|
||||
params_ref p;
|
||||
m_params.init_solver_params(m(), *m_solver, p);
|
||||
m_solver->init(m(), m_logic);
|
||||
if (!m_params.m_auto_config) {
|
||||
params_ref p;
|
||||
p.set_bool("auto_config", false);
|
||||
m_solver->updt_params(p);
|
||||
}
|
||||
}
|
||||
|
||||
void cmd_context::set_solver(solver * s) {
|
||||
|
|
|
|||
|
|
@ -20,6 +20,8 @@ Notes:
|
|||
#include"context_params.h"
|
||||
#include"gparams.h"
|
||||
#include"params.h"
|
||||
#include"ast.h"
|
||||
#include"solver.h"
|
||||
|
||||
context_params::context_params() {
|
||||
updt_params();
|
||||
|
|
@ -39,7 +41,7 @@ void context_params::set_bool(bool & opt, char const * param, char const * value
|
|||
|
||||
void context_params::set(char const * param, char const * value) {
|
||||
std::string p = param;
|
||||
unsigned n = p.size();
|
||||
unsigned n = static_cast<unsigned>(p.size());
|
||||
for (unsigned i = 0; i < n; i++) {
|
||||
if (p[i] >= 'A' && p[i] <= 'Z')
|
||||
p[i] = p[i] - 'A' + 'a';
|
||||
|
|
@ -77,6 +79,9 @@ void context_params::set(char const * param, char const * value) {
|
|||
else if (p == "debug_ref_count") {
|
||||
set_bool(m_debug_ref_count, param, value);
|
||||
}
|
||||
else if (p == "smtlib2_compliant") {
|
||||
set_bool(m_smtlib2_compliant, param, value);
|
||||
}
|
||||
else {
|
||||
throw default_exception("unknown parameter '%s'", p.c_str());
|
||||
}
|
||||
|
|
@ -97,6 +102,7 @@ void context_params::updt_params(params_ref const & p) {
|
|||
m_trace_file_name = p.get_str("trace_file_name", "z3.log");
|
||||
m_unsat_core = p.get_bool("unsat_core", false);
|
||||
m_debug_ref_count = p.get_bool("debug_ref_count", false);
|
||||
m_smtlib2_compliant = p.get_bool("smtlib2_compliant", false);
|
||||
}
|
||||
|
||||
void context_params::collect_param_descrs(param_descrs & d) {
|
||||
|
|
@ -111,4 +117,36 @@ void context_params::collect_param_descrs(param_descrs & d) {
|
|||
d.insert("trace_file_name", CPK_STRING, "trace out file name (see option 'trace')", "z3.log");
|
||||
d.insert("unsat_core", CPK_BOOL, "unsat-core generation for solvers, this parameter can be overwritten when creating a solver, not every solver in Z3 supports unsat core generation", "false");
|
||||
d.insert("debug_ref_count", CPK_BOOL, "debug support for AST reference counting", "false");
|
||||
d.insert("smtlib2_compliant", CPK_BOOL, "enable/disable SMT-LIB 2.0 compliance", "false");
|
||||
}
|
||||
|
||||
params_ref context_params::merge_default_params(params_ref const & p) {
|
||||
if (!m_auto_config && !p.contains("auto_config")) {
|
||||
params_ref new_p = p;
|
||||
new_p.set_bool("auto_config", false);
|
||||
return new_p;
|
||||
}
|
||||
else {
|
||||
return p;
|
||||
}
|
||||
}
|
||||
|
||||
void context_params::init_solver_params(ast_manager & m, solver & s, params_ref const & p) {
|
||||
s.set_produce_proofs(m.proofs_enabled() && m_proof);
|
||||
s.set_produce_models(p.get_bool("model", m_model));
|
||||
s.set_produce_unsat_cores(p.get_bool("unsat_core", m_unsat_core));
|
||||
s.updt_params(merge_default_params(p));
|
||||
}
|
||||
|
||||
ast_manager * context_params::mk_ast_manager() {
|
||||
ast_manager * r = alloc(ast_manager,
|
||||
m_proof ? PGM_FINE : PGM_DISABLED,
|
||||
m_trace ? m_trace_file_name.c_str() : 0);
|
||||
if (m_smtlib2_compliant)
|
||||
r->enable_int_real_coercions(false);
|
||||
if (m_debug_ref_count)
|
||||
r->debug_ref_count();
|
||||
return r;
|
||||
}
|
||||
|
||||
|
||||
|
|
|
|||
|
|
@ -21,6 +21,8 @@ Notes:
|
|||
#define _CONTEXT_PARAMS_H_
|
||||
|
||||
#include"params.h"
|
||||
class ast_manager;
|
||||
class solver;
|
||||
|
||||
class context_params {
|
||||
void set_bool(bool & opt, char const * param, char const * value);
|
||||
|
|
@ -35,6 +37,7 @@ public:
|
|||
bool m_model;
|
||||
bool m_model_validate;
|
||||
bool m_unsat_core;
|
||||
bool m_smtlib2_compliant; // it must be here because it enable/disable the use of coercions in the ast_manager.
|
||||
unsigned m_timeout;
|
||||
|
||||
context_params();
|
||||
|
|
@ -45,6 +48,27 @@ public:
|
|||
/*
|
||||
REG_PARAMS('context_params::collect_param_descrs')
|
||||
*/
|
||||
|
||||
/**
|
||||
\brief Goodie for updating the solver params
|
||||
based on the configuration of the context_params object.
|
||||
|
||||
This method is used when creating solvers from the
|
||||
cmd_context and API.
|
||||
*/
|
||||
void init_solver_params(ast_manager & m, solver & s, params_ref const & p);
|
||||
|
||||
/**
|
||||
\brief Include in p parameters derived from this context_params.
|
||||
These are parameters that are meaningful for tactics and solvers.
|
||||
Example: auto_config
|
||||
*/
|
||||
params_ref merge_default_params(params_ref const & p);
|
||||
|
||||
/**
|
||||
\brief Create an AST manager using this configuration.
|
||||
*/
|
||||
ast_manager * mk_ast_manager();
|
||||
};
|
||||
|
||||
|
||||
|
|
|
|||
|
|
@ -36,7 +36,7 @@ tactic_cmd::~tactic_cmd() {
|
|||
dealloc(m_factory);
|
||||
}
|
||||
|
||||
tactic * tactic_cmd::mk(ast_manager & m) {
|
||||
tactic * tactic_cmd::mk(ast_manager & m) {
|
||||
return (*m_factory)(m, params_ref());
|
||||
}
|
||||
|
||||
|
|
@ -185,7 +185,7 @@ public:
|
|||
}
|
||||
|
||||
virtual void execute(cmd_context & ctx) {
|
||||
params_ref p = ps();
|
||||
params_ref p = ctx.params().merge_default_params(ps());
|
||||
tactic_ref tref = using_params(sexpr2tactic(ctx, m_tactic), p);
|
||||
tref->set_logic(ctx.get_logic());
|
||||
ast_manager & m = ctx.m();
|
||||
|
|
@ -295,7 +295,7 @@ public:
|
|||
}
|
||||
|
||||
virtual void execute(cmd_context & ctx) {
|
||||
params_ref p = ps();
|
||||
params_ref p = ctx.params().merge_default_params(ps());
|
||||
tactic_ref tref = using_params(sexpr2tactic(ctx, m_tactic), p);
|
||||
{
|
||||
tactic & t = *(tref.get());
|
||||
|
|
|
|||
|
|
@ -64,6 +64,8 @@ namespace algebraic_numbers {
|
|||
static void collect_param_descrs(param_descrs & r) { get_param_descrs(r); }
|
||||
|
||||
void set_cancel(bool f);
|
||||
|
||||
void cancel() { set_cancel(true); }
|
||||
|
||||
void updt_params(params_ref const & p);
|
||||
|
||||
|
|
|
|||
|
|
@ -219,6 +219,7 @@ namespace polynomial {
|
|||
void set_zp(uint64 p);
|
||||
|
||||
void set_cancel(bool f);
|
||||
void cancel() { set_cancel(true); }
|
||||
|
||||
/**
|
||||
\brief Abstract event handler.
|
||||
|
|
|
|||
|
|
@ -49,10 +49,10 @@ void func_entry::set_result(ast_manager & m, expr * r) {
|
|||
m_result = r;
|
||||
}
|
||||
|
||||
bool func_entry::eq_args(unsigned arity, expr * const * args) const {
|
||||
bool func_entry::eq_args(ast_manager & m, unsigned arity, expr * const * args) const {
|
||||
unsigned i = 0;
|
||||
for (; i < arity; i++) {
|
||||
if (m_args[i] != args[i])
|
||||
if (!m.are_equal(m_args[i], args[i]))
|
||||
return false;
|
||||
}
|
||||
return true;
|
||||
|
|
@ -131,7 +131,7 @@ bool func_interp::is_constant() const {
|
|||
}
|
||||
|
||||
/**
|
||||
\brief Return a func_entry e such that e.m_args[i] == args[i] for all i in [0, m_arity).
|
||||
\brief Return a func_entry e such that m().are_equal(e.m_args[i], args[i]) for all i in [0, m_arity).
|
||||
If such entry does not exist then return 0, and store set
|
||||
args_are_values to true if for all entries e e.args_are_values() is true.
|
||||
*/
|
||||
|
|
@ -140,7 +140,7 @@ func_entry * func_interp::get_entry(expr * const * args) const {
|
|||
ptr_vector<func_entry>::const_iterator end = m_entries.end();
|
||||
for (; it != end; ++it) {
|
||||
func_entry * curr = *it;
|
||||
if (curr->eq_args(m_arity, args))
|
||||
if (curr->eq_args(m(), m_arity, args))
|
||||
return curr;
|
||||
}
|
||||
return 0;
|
||||
|
|
|
|||
|
|
@ -58,9 +58,9 @@ public:
|
|||
expr * get_arg(unsigned idx) const { return m_args[idx]; }
|
||||
expr * const * get_args() const { return m_args; }
|
||||
/**
|
||||
\brief Return true if m_args[i] == args[i] for all i in [0, arity)
|
||||
\brief Return true if m.are_equal(m_args[i], args[i]) for all i in [0, arity)
|
||||
*/
|
||||
bool eq_args(unsigned arity, expr * const * args) const;
|
||||
bool eq_args(ast_manager & m, unsigned arity, expr * const * args) const;
|
||||
};
|
||||
|
||||
class func_interp {
|
||||
|
|
|
|||
File diff suppressed because it is too large
Load diff
|
|
@ -35,83 +35,23 @@ namespace datalog {
|
|||
ast_manager& m;
|
||||
smt_params m_fparams;
|
||||
smt::kernel m_solver;
|
||||
obj_map<func_decl, sort*> m_pred2sort;
|
||||
obj_map<sort, func_decl*> m_sort2pred;
|
||||
obj_map<func_decl, func_decl*> m_pred2newpred;
|
||||
obj_map<func_decl, ptr_vector<func_decl> > m_pred2args;
|
||||
ast_ref_vector m_pinned;
|
||||
rule_set m_rules;
|
||||
func_decl_ref m_query_pred;
|
||||
expr_ref m_answer;
|
||||
volatile bool m_cancel;
|
||||
proof_converter_ref m_pc;
|
||||
sort_ref m_path_sort;
|
||||
bv_util m_bv;
|
||||
unsigned m_bit_width;
|
||||
|
||||
lbool check_query();
|
||||
|
||||
proof_ref get_proof(model_ref& md, app* trace, app* path);
|
||||
|
||||
void checkpoint();
|
||||
|
||||
void declare_datatypes();
|
||||
|
||||
void compile_nonlinear();
|
||||
|
||||
void mk_rule_vars_nonlinear(rule& r, unsigned rule_id, expr* trace_arg, expr* path_arg, expr_ref_vector& sub);
|
||||
|
||||
expr_ref mk_var_nonlinear(func_decl* pred, sort* s, unsigned idx, expr* path_arg, expr* trace_arg);
|
||||
|
||||
expr_ref mk_arg_nonlinear(func_decl* pred, unsigned idx, expr* path_arg, expr* trace_arg);
|
||||
|
||||
void mk_subst(rule& r, expr* path, app* trace, expr_ref_vector& sub);
|
||||
class nonlinear_dt;
|
||||
class nonlinear;
|
||||
class qlinear;
|
||||
class linear;
|
||||
|
||||
bool is_linear() const;
|
||||
|
||||
lbool check_nonlinear();
|
||||
void setup_nonlinear();
|
||||
bool check_model_nonlinear(model_ref& md, expr* trace);
|
||||
void mk_answer_nonlinear(model_ref& md, expr_ref& trace, expr_ref& path);
|
||||
|
||||
func_decl_ref mk_predicate(func_decl* p);
|
||||
|
||||
func_decl_ref mk_rule(func_decl* p, unsigned rule_idx);
|
||||
|
||||
// linear check
|
||||
lbool check_linear();
|
||||
lbool check_linear(unsigned level);
|
||||
void compile_linear();
|
||||
void compile_linear(unsigned level);
|
||||
void compile_linear(rule& r, unsigned level);
|
||||
expr_ref mk_level_predicate(symbol const& name, unsigned level);
|
||||
expr_ref mk_level_predicate(func_decl* p, unsigned level);
|
||||
expr_ref mk_level_arg(func_decl* pred, unsigned idx, unsigned level);
|
||||
expr_ref mk_level_rule(func_decl* p, unsigned rule_idx, unsigned level);
|
||||
expr_ref mk_level_var(func_decl* pred, sort* s, unsigned rule_id, unsigned idx, unsigned level);
|
||||
void get_model_linear(unsigned level);
|
||||
void setup_linear();
|
||||
|
||||
void assert_expr(expr* e);
|
||||
|
||||
void mk_rule_vars(rule& r, unsigned level, unsigned rule_id, expr_ref_vector& sub);
|
||||
|
||||
// quantified linear check
|
||||
void compile_qlinear();
|
||||
void setup_qlinear();
|
||||
lbool check_qlinear();
|
||||
lbool get_model_qlinear();
|
||||
sort_ref mk_index_sort();
|
||||
var_ref mk_index_var();
|
||||
void mk_qrule_vars(datalog::rule const& r, unsigned i, expr_ref_vector& sub);
|
||||
expr_ref mk_q_var(func_decl* pred, sort* s, unsigned rule_id, unsigned idx);
|
||||
expr_ref mk_q_arg(func_decl* pred, unsigned idx, bool is_current);
|
||||
expr_ref mk_q_one();
|
||||
expr_ref mk_q_num(unsigned i);
|
||||
expr_ref eval_q(model_ref& model, expr* t, unsigned i);
|
||||
expr_ref eval_q(model_ref& model, func_decl* f, unsigned i);
|
||||
func_decl_ref mk_q_rule(func_decl* f, unsigned rule_id);
|
||||
func_decl_ref mk_q_func_decl(func_decl* f);
|
||||
|
||||
public:
|
||||
bmc(context& ctx);
|
||||
|
|
@ -131,6 +71,10 @@ namespace datalog {
|
|||
void reset_statistics();
|
||||
|
||||
expr_ref get_answer();
|
||||
|
||||
// direct access to (new) non-linear compiler.
|
||||
void compile(rule_set const& rules, expr_ref_vector& fmls, unsigned level);
|
||||
expr_ref compile_query(func_decl* query_pred, unsigned level);
|
||||
};
|
||||
};
|
||||
|
||||
|
|
|
|||
|
|
@ -715,6 +715,8 @@ namespace datalog {
|
|||
check_positive_predicates(r);
|
||||
break;
|
||||
case BMC_ENGINE:
|
||||
check_positive_predicates(r);
|
||||
break;
|
||||
case QBMC_ENGINE:
|
||||
check_existential_tail(r);
|
||||
check_positive_predicates(r);
|
||||
|
|
|
|||
|
|
@ -18,7 +18,8 @@ Revision History:
|
|||
--*/
|
||||
|
||||
#include "dl_mk_array_blast.h"
|
||||
#include "expr_replacer.h"
|
||||
#include "expr_safe_replace.h"
|
||||
|
||||
|
||||
namespace datalog {
|
||||
|
||||
|
|
@ -54,9 +55,10 @@ namespace datalog {
|
|||
unsigned tsz = r.get_tail_size();
|
||||
expr_ref_vector conjs(m), new_conjs(m);
|
||||
expr_ref tmp(m);
|
||||
expr_substitution sub(m);
|
||||
expr_safe_replace sub(m);
|
||||
uint_set lhs_vars, rhs_vars;
|
||||
bool change = false;
|
||||
bool inserted = false;
|
||||
|
||||
for (unsigned i = 0; i < utsz; ++i) {
|
||||
new_conjs.push_back(r.get_tail(i));
|
||||
|
|
@ -81,6 +83,7 @@ namespace datalog {
|
|||
}
|
||||
else {
|
||||
sub.insert(x, y);
|
||||
inserted = true;
|
||||
}
|
||||
}
|
||||
else {
|
||||
|
|
@ -89,7 +92,7 @@ namespace datalog {
|
|||
new_conjs.push_back(tmp);
|
||||
}
|
||||
}
|
||||
if (sub.empty() && !change) {
|
||||
if (!inserted && !change) {
|
||||
rules.add_rule(&r);
|
||||
return false;
|
||||
}
|
||||
|
|
@ -99,11 +102,9 @@ namespace datalog {
|
|||
r.to_formula(fml1);
|
||||
body = m.mk_and(new_conjs.size(), new_conjs.c_ptr());
|
||||
head = r.get_head();
|
||||
scoped_ptr<expr_replacer> replace = mk_default_expr_replacer(m);
|
||||
replace->set_substitution(&sub);
|
||||
(*replace)(body);
|
||||
sub(body);
|
||||
m_rewriter(body);
|
||||
(*replace)(head);
|
||||
sub(head);
|
||||
m_rewriter(head);
|
||||
fml2 = m.mk_implies(body, head);
|
||||
rm.mk_rule(fml2, new_rules, r.name());
|
||||
|
|
|
|||
|
|
@ -60,7 +60,7 @@ namespace datalog {
|
|||
obj_map<expr, unsigned> indices;
|
||||
bool_rewriter bwr(m);
|
||||
rule_ref r(const_cast<rule*>(&rl), rm);
|
||||
sort_ref_vector sorts(m);
|
||||
ptr_vector<sort> sorts;
|
||||
expr_ref_vector revsub(m), conjs(m);
|
||||
rl.get_vars(sorts);
|
||||
revsub.resize(sorts.size());
|
||||
|
|
@ -72,8 +72,8 @@ namespace datalog {
|
|||
if (is_var(e)) {
|
||||
unsigned v = to_var(e)->get_idx();
|
||||
SASSERT(v < valid.size());
|
||||
if (sorts[v].get()) {
|
||||
SASSERT(s == sorts[v].get());
|
||||
if (sorts[v]) {
|
||||
SASSERT(s == sorts[v]);
|
||||
if (valid[v]) {
|
||||
revsub[v] = w;
|
||||
valid[v] = false;
|
||||
|
|
@ -92,8 +92,8 @@ namespace datalog {
|
|||
}
|
||||
}
|
||||
for (unsigned i = 0; i < sorts.size(); ++i) {
|
||||
if (valid[i] && sorts[i].get() && !revsub[i].get()) {
|
||||
revsub[i] = m.mk_var(m_idx++, sorts[i].get());
|
||||
if (valid[i] && sorts[i] && !revsub[i].get()) {
|
||||
revsub[i] = m.mk_var(m_idx++, sorts[i]);
|
||||
}
|
||||
}
|
||||
var_subst vs(m, false);
|
||||
|
|
@ -112,7 +112,7 @@ namespace datalog {
|
|||
app_ref pred(m), head(m);
|
||||
expr_ref fml1(m), fml2(m), fml(m);
|
||||
app_ref_vector tail(m);
|
||||
sort_ref_vector sorts1(m), sorts2(m);
|
||||
ptr_vector<sort> sorts1, sorts2;
|
||||
expr_ref_vector conjs1(m), conjs(m);
|
||||
rule_ref res(rm);
|
||||
bool_rewriter bwr(m);
|
||||
|
|
|
|||
366
src/muz_qe/dl_mk_extract_quantifiers2.cpp
Normal file
366
src/muz_qe/dl_mk_extract_quantifiers2.cpp
Normal file
|
|
@ -0,0 +1,366 @@
|
|||
/*++
|
||||
Copyright (c) 2012 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
dl_mk_extract_quantifiers2.cpp
|
||||
|
||||
Abstract:
|
||||
|
||||
Remove universal quantifiers over interpreted predicates in the body.
|
||||
|
||||
Author:
|
||||
|
||||
Nikolaj Bjorner (nbjorner) 2012-11-21
|
||||
|
||||
Revision History:
|
||||
|
||||
--*/
|
||||
|
||||
#include"dl_mk_extract_quantifiers2.h"
|
||||
#include"ast_pp.h"
|
||||
#include"dl_bmc_engine.h"
|
||||
#include"smt_quantifier.h"
|
||||
#include"smt_context.h"
|
||||
|
||||
namespace datalog {
|
||||
|
||||
|
||||
mk_extract_quantifiers2::mk_extract_quantifiers2(context & ctx) :
|
||||
rule_transformer::plugin(101, false),
|
||||
m_ctx(ctx),
|
||||
m(ctx.get_manager()),
|
||||
rm(ctx.get_rule_manager()),
|
||||
m_query_pred(m),
|
||||
m_quantifiers(m),
|
||||
m_refs(m)
|
||||
{}
|
||||
|
||||
mk_extract_quantifiers2::~mk_extract_quantifiers2() {
|
||||
reset();
|
||||
}
|
||||
|
||||
void mk_extract_quantifiers2::set_query(func_decl* q) {
|
||||
m_query_pred = q;
|
||||
}
|
||||
|
||||
bool mk_extract_quantifiers2::matches_signature(func_decl* head, expr_ref_vector const& binding) {
|
||||
unsigned sz = head->get_arity();
|
||||
if (sz != binding.size()) {
|
||||
return false;
|
||||
}
|
||||
for (unsigned i = 0; i < sz; ++i) {
|
||||
if (head->get_domain(i) != m.get_sort(binding[sz-i-1])) {
|
||||
return false;
|
||||
}
|
||||
}
|
||||
return true;
|
||||
}
|
||||
|
||||
bool mk_extract_quantifiers2::matches_quantifier(quantifier* q, expr_ref_vector const& binding) {
|
||||
unsigned sz = q->get_num_decls();
|
||||
if (sz != binding.size()) {
|
||||
return false;
|
||||
}
|
||||
for (unsigned i = 0; i < sz; ++i) {
|
||||
if (q->get_decl_sort(i) != m.get_sort(binding[sz-i-1])) {
|
||||
return false;
|
||||
}
|
||||
}
|
||||
return true;
|
||||
}
|
||||
|
||||
bool mk_extract_quantifiers2::mk_abstract_expr(expr_ref& term) {
|
||||
if (!is_app(term)) {
|
||||
return false;
|
||||
}
|
||||
expr* r;
|
||||
if (m_map.find(term, r)) {
|
||||
term = r;
|
||||
return true;
|
||||
}
|
||||
if (to_app(term)->get_family_id() == null_family_id) {
|
||||
return false;
|
||||
}
|
||||
expr_ref_vector args(m);
|
||||
expr_ref tmp(m);
|
||||
for (unsigned i = 0; i < to_app(term)->get_num_args(); ++i) {
|
||||
tmp = to_app(term)->get_arg(i);
|
||||
if (!mk_abstract_expr(tmp)) {
|
||||
return false;
|
||||
}
|
||||
args.push_back(tmp);
|
||||
}
|
||||
tmp = m.mk_app(to_app(term)->get_decl(), args.size(), args.c_ptr());
|
||||
m_refs.push_back(tmp);
|
||||
m_map.insert(term, tmp);
|
||||
term = tmp;
|
||||
return true;
|
||||
}
|
||||
|
||||
bool mk_extract_quantifiers2::mk_abstract_binding(expr_ref_vector const& binding, expr_ref_vector& result) {
|
||||
for (unsigned i = 0; i < binding.size(); ++i) {
|
||||
expr_ref tmp(m);
|
||||
tmp = binding[i];
|
||||
if (!mk_abstract_expr(tmp)) {
|
||||
return false;
|
||||
}
|
||||
result.push_back(tmp);
|
||||
}
|
||||
return true;
|
||||
}
|
||||
|
||||
void mk_extract_quantifiers2::mk_abstraction_map(rule& r, expr_ref_vector const& binding) {
|
||||
m_map.reset();
|
||||
unsigned sz = binding.size();
|
||||
SASSERT(sz == r.get_decl()->get_arity());
|
||||
for (unsigned i = 0; i < sz; ++i) {
|
||||
m_map.insert(binding[sz-i-1], r.get_head()->get_arg(i));
|
||||
SASSERT(m.get_sort(binding[sz-i-1]) == m.get_sort(r.get_head()->get_arg(i)));
|
||||
}
|
||||
// todo: also make bindings for variables in rule body.
|
||||
}
|
||||
|
||||
void mk_extract_quantifiers2::match_bindings(unsigned i, unsigned j, unsigned k) {
|
||||
expr_ref_vector resb(m);
|
||||
rule* r = m_qrules[i];
|
||||
quantifier* q = m_quantifiers[i].get();
|
||||
expr_ref_vector const& ruleb = m_rule_bindings[i][j];
|
||||
expr_ref_vector const& quantb = m_quantifier_bindings[i][k];
|
||||
mk_abstraction_map(*r, ruleb);
|
||||
if (!mk_abstract_binding(quantb, resb)) {
|
||||
return;
|
||||
}
|
||||
expr_ref inst(m), tmp(m);
|
||||
var_shifter shift(m);
|
||||
|
||||
for (unsigned l = 0; l < resb.size(); ++l) {
|
||||
tmp = resb[l].get();
|
||||
shift(tmp, q->get_num_decls(), tmp);
|
||||
resb[l] = tmp;
|
||||
}
|
||||
|
||||
instantiate(m, q, resb.c_ptr(), inst);
|
||||
if (!m_seen.contains(r)) {
|
||||
m_seen.insert(r, alloc(obj_hashtable<expr>));
|
||||
}
|
||||
obj_hashtable<expr>& seen = *m_seen.find(r);
|
||||
if (seen.contains(inst)) {
|
||||
return;
|
||||
}
|
||||
seen.insert(inst);
|
||||
m_refs.push_back(inst);
|
||||
if (!m_quantifier_instantiations.contains(r, q)) {
|
||||
m_quantifier_instantiations.insert(r, q, alloc(expr_ref_vector, m));
|
||||
}
|
||||
expr_ref_vector* vec = 0;
|
||||
VERIFY(m_quantifier_instantiations.find(r, q, vec));
|
||||
vec->push_back(inst);
|
||||
TRACE("dl", tout << "matched: " << mk_pp(q, m) << "\n" << mk_pp(inst, m) << "\n";);
|
||||
}
|
||||
|
||||
app_ref mk_extract_quantifiers2::ensure_app(expr* e) {
|
||||
if (is_app(e)) {
|
||||
return app_ref(to_app(e), m);
|
||||
}
|
||||
else {
|
||||
return app_ref(m.mk_eq(e, m.mk_true()), m);
|
||||
}
|
||||
}
|
||||
|
||||
void mk_extract_quantifiers2::extract(rule& r, rule_set& new_rules) {
|
||||
unsigned utsz = r.get_uninterpreted_tail_size();
|
||||
unsigned tsz = r.get_tail_size();
|
||||
bool has_quantifier = false;
|
||||
expr_ref_vector conjs(m);
|
||||
for (unsigned i = utsz; i < tsz; ++i) {
|
||||
conjs.push_back(r.get_tail(i));
|
||||
}
|
||||
datalog::flatten_and(conjs);
|
||||
for (unsigned j = 0; j < conjs.size(); ++j) {
|
||||
expr* e = conjs[j].get();
|
||||
quantifier* q;
|
||||
if (rule_manager::is_forall(m, e, q)) {
|
||||
m_quantifiers.push_back(q);
|
||||
m_qrules.push_back(&r);
|
||||
m_rule_bindings.push_back(vector<expr_ref_vector>());
|
||||
m_quantifier_bindings.push_back(vector<expr_ref_vector>());
|
||||
has_quantifier = true;
|
||||
}
|
||||
}
|
||||
if (!has_quantifier) {
|
||||
new_rules.add_rule(&r);
|
||||
}
|
||||
}
|
||||
|
||||
void mk_extract_quantifiers2::apply(rule& r, rule_set& new_rules) {
|
||||
expr_ref_vector tail(m), conjs(m);
|
||||
expr_ref fml(m);
|
||||
unsigned utsz = r.get_uninterpreted_tail_size();
|
||||
unsigned tsz = r.get_tail_size();
|
||||
for (unsigned i = 0; i < utsz; ++i) {
|
||||
SASSERT(!r.is_neg_tail(i));
|
||||
tail.push_back(r.get_tail(i));
|
||||
}
|
||||
bool has_quantifier = false;
|
||||
for (unsigned i = utsz; i < tsz; ++i) {
|
||||
conjs.push_back(r.get_tail(i));
|
||||
}
|
||||
datalog::flatten_and(conjs);
|
||||
for (unsigned j = 0; j < conjs.size(); ++j) {
|
||||
expr* e = conjs[j].get();
|
||||
quantifier* q;
|
||||
if (rule_manager::is_forall(m, e, q)) {
|
||||
expr_ref_vector* ls;
|
||||
if (m_quantifier_instantiations.find(&r,q,ls)) {
|
||||
tail.append(*ls);
|
||||
}
|
||||
has_quantifier = true;
|
||||
}
|
||||
else {
|
||||
tail.push_back(e);
|
||||
}
|
||||
}
|
||||
if (has_quantifier) {
|
||||
fml = m.mk_implies(m.mk_and(tail.size(), tail.c_ptr()), r.get_head());
|
||||
rule_ref_vector rules(rm);
|
||||
rm.mk_rule(fml, rules, r.name());
|
||||
for (unsigned i = 0; i < rules.size(); ++i) {
|
||||
new_rules.add_rule(rules[i].get());
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
#if 0
|
||||
class mk_extract_quantifiers2::instance_plugin : public smt::quantifier_instance_plugin {
|
||||
mk_extract_quantifiers2& ex;
|
||||
ast_manager& m;
|
||||
expr_ref_vector m_refs;
|
||||
obj_hashtable<expr> m_bindings;
|
||||
public:
|
||||
instance_plugin(mk_extract_quantifiers2& ex): ex(ex), m(ex.m), m_refs(m) {}
|
||||
|
||||
virtual void operator()(quantifier* q, unsigned num_bindings, smt::enode*const* bindings) {
|
||||
expr_ref_vector binding(m);
|
||||
ptr_vector<sort> sorts;
|
||||
for (unsigned i = 0; i < num_bindings; ++i) {
|
||||
binding.push_back(bindings[i]->get_owner());
|
||||
sorts.push_back(m.get_sort(binding[i].get()));
|
||||
}
|
||||
func_decl* f = m.mk_func_decl(symbol("T"), sorts.size(), sorts.c_ptr(), m.mk_bool_sort());
|
||||
expr_ref tup(m);
|
||||
tup = m.mk_app(f, binding.size(), binding.c_ptr());
|
||||
if (!m_bindings.contains(tup)) {
|
||||
m_bindings.insert(tup);
|
||||
m_refs.push_back(tup);
|
||||
ex.m_bindings.push_back(binding);
|
||||
TRACE("dl", tout << "insert\n" << mk_pp(q, m) << "\n" << mk_pp(tup, m) << "\n";);
|
||||
}
|
||||
}
|
||||
};
|
||||
|
||||
#endif
|
||||
|
||||
void mk_extract_quantifiers2::reset() {
|
||||
{
|
||||
obj_pair_map<rule,quantifier, expr_ref_vector*>::iterator
|
||||
it = m_quantifier_instantiations.begin(),
|
||||
end = m_quantifier_instantiations.end();
|
||||
for (; it != end; ++it) {
|
||||
dealloc(it->get_value());
|
||||
}
|
||||
}
|
||||
{
|
||||
obj_map<rule,obj_hashtable<expr>*>::iterator
|
||||
it = m_seen.begin(),
|
||||
end = m_seen.end();
|
||||
for (; it != end; ++it) {
|
||||
dealloc(it->m_value);
|
||||
}
|
||||
}
|
||||
m_quantifier_instantiations.reset();
|
||||
m_seen.reset();
|
||||
m_has_quantifiers = false;
|
||||
m_quantifiers.reset();
|
||||
m_qrules.reset();
|
||||
m_bindings.reset();
|
||||
m_rule_bindings.reset();
|
||||
m_quantifier_bindings.reset();
|
||||
m_refs.reset();
|
||||
}
|
||||
|
||||
rule_set * mk_extract_quantifiers2::operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc) {
|
||||
reset();
|
||||
rule_set::iterator it = source.begin(), end = source.end();
|
||||
for (; !m_has_quantifiers && it != end; ++it) {
|
||||
m_has_quantifiers = (*it)->has_quantifiers();
|
||||
}
|
||||
if (!m_has_quantifiers) {
|
||||
return 0;
|
||||
}
|
||||
|
||||
rule_set* rules = alloc(rule_set, m_ctx);
|
||||
it = source.begin();
|
||||
for (; it != end; ++it) {
|
||||
extract(**it, *rules);
|
||||
}
|
||||
|
||||
bmc bmc(m_ctx);
|
||||
expr_ref_vector fmls(m);
|
||||
bmc.compile(source, fmls, 0); // TBD: use cancel_eh to terminate without base-case.
|
||||
bmc.compile(source, fmls, 1);
|
||||
bmc.compile(source, fmls, 2);
|
||||
// bmc.compile(source, fmls, 3);
|
||||
expr_ref query = bmc.compile_query(m_query_pred, 2);
|
||||
fmls.push_back(query);
|
||||
smt_params fparams;
|
||||
fparams.m_relevancy_lvl = 0;
|
||||
fparams.m_model = true;
|
||||
fparams.m_model_compact = true;
|
||||
fparams.m_mbqi = true;
|
||||
smt::kernel solver(m, fparams);
|
||||
TRACE("dl",
|
||||
for (unsigned i = 0; i < fmls.size(); ++i) {
|
||||
tout << mk_pp(fmls[i].get(), m) << "\n";
|
||||
});
|
||||
|
||||
for (unsigned i = 0; i < fmls.size(); ++i) {
|
||||
solver.assert_expr(fmls[i].get());
|
||||
}
|
||||
#if 0
|
||||
smt::context& ctx = solver.get_context();
|
||||
smt::quantifier_manager* qm = ctx.get_quantifier_manager();
|
||||
qm->get_plugin()->set_instance_plugin(alloc(instance_plugin, *this));
|
||||
#endif
|
||||
lbool res = solver.check();
|
||||
|
||||
for (unsigned i = 0; i < m_bindings.size(); ++i) {
|
||||
expr_ref_vector& binding = m_bindings[i];
|
||||
for (unsigned j = 0; j < m_qrules.size(); ++j) {
|
||||
rule* r = m_qrules[j];
|
||||
if (matches_signature(r->get_decl(), binding)) {
|
||||
m_rule_bindings[j].push_back(binding);
|
||||
}
|
||||
else if (matches_quantifier(m_quantifiers[j].get(), binding)) {
|
||||
m_quantifier_bindings[j].push_back(binding);
|
||||
}
|
||||
}
|
||||
}
|
||||
for (unsigned i = 0; i < m_qrules.size(); ++i) {
|
||||
for (unsigned j = 0; j < m_rule_bindings[i].size(); ++j) {
|
||||
for (unsigned k = 0; k < m_quantifier_bindings[i].size(); ++k) {
|
||||
match_bindings(i, j, k);
|
||||
}
|
||||
}
|
||||
}
|
||||
it = source.begin();
|
||||
for (; it != end; ++it) {
|
||||
apply(**it, *rules);
|
||||
}
|
||||
|
||||
return rules;
|
||||
}
|
||||
|
||||
};
|
||||
|
||||
|
||||
91
src/muz_qe/dl_mk_extract_quantifiers2.h
Normal file
91
src/muz_qe/dl_mk_extract_quantifiers2.h
Normal file
|
|
@ -0,0 +1,91 @@
|
|||
/*++
|
||||
Copyright (c) 2012 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
dl_mk_extract_quantifiers2.h
|
||||
|
||||
Abstract:
|
||||
|
||||
Replace universal quantifiers over interpreted predicates in the body
|
||||
by instantiations mined using bounded model checking search.
|
||||
|
||||
Author:
|
||||
|
||||
Nikolaj Bjorner (nbjorner) 2012-11-21
|
||||
|
||||
Revision History:
|
||||
|
||||
--*/
|
||||
#ifndef _DL_MK_EXTRACT_QUANTIFIERS2_H_
|
||||
#define _DL_MK_EXTRACT_QUANTIFIERS2_H_
|
||||
|
||||
#include"dl_context.h"
|
||||
#include"dl_rule_set.h"
|
||||
#include"dl_rule_transformer.h"
|
||||
#include"obj_pair_hashtable.h"
|
||||
|
||||
namespace datalog {
|
||||
|
||||
/**
|
||||
\brief Extract universal quantifiers from rules.
|
||||
*/
|
||||
class mk_extract_quantifiers2 : public rule_transformer::plugin {
|
||||
context& m_ctx;
|
||||
ast_manager& m;
|
||||
rule_manager& rm;
|
||||
func_decl_ref m_query_pred;
|
||||
quantifier_ref_vector m_quantifiers;
|
||||
ptr_vector<rule> m_qrules;
|
||||
vector<expr_ref_vector>m_bindings;
|
||||
vector<vector<expr_ref_vector> > m_rule_bindings;
|
||||
vector<vector<expr_ref_vector> > m_quantifier_bindings;
|
||||
obj_pair_map<rule,quantifier, expr_ref_vector*> m_quantifier_instantiations;
|
||||
obj_map<rule, obj_hashtable<expr>*> m_seen;
|
||||
|
||||
bool m_has_quantifiers;
|
||||
obj_map<expr,expr*> m_map;
|
||||
expr_ref_vector m_refs;
|
||||
|
||||
class instance_plugin;
|
||||
|
||||
void reset();
|
||||
|
||||
void extract(rule& r, rule_set& new_rules);
|
||||
|
||||
void apply(rule& r, rule_set& new_rules);
|
||||
|
||||
app_ref ensure_app(expr* e);
|
||||
|
||||
bool matches_signature(func_decl* head, expr_ref_vector const& binding);
|
||||
|
||||
bool matches_quantifier(quantifier* q, expr_ref_vector const& binding);
|
||||
|
||||
void match_bindings(unsigned i, unsigned j, unsigned k);
|
||||
|
||||
bool mk_abstract_expr(expr_ref& term);
|
||||
|
||||
bool mk_abstract_binding(expr_ref_vector const& binding, expr_ref_vector& result);
|
||||
|
||||
void mk_abstraction_map(rule& r, expr_ref_vector const& binding);
|
||||
|
||||
public:
|
||||
/**
|
||||
\brief Create rule transformer that extracts universal quantifiers (over recursive predicates).
|
||||
*/
|
||||
mk_extract_quantifiers2(context & ctx);
|
||||
|
||||
virtual ~mk_extract_quantifiers2();
|
||||
|
||||
void set_query(func_decl* q);
|
||||
|
||||
rule_set * operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc);
|
||||
|
||||
bool has_quantifiers() { return m_has_quantifiers; }
|
||||
|
||||
};
|
||||
|
||||
};
|
||||
|
||||
#endif /* _DL_MK_EXTRACT_QUANTIFIERS2_H_ */
|
||||
|
||||
|
|
@ -136,14 +136,14 @@ namespace datalog {
|
|||
expr_ref_vector rule_unifier::get_rule_subst(const rule& r, bool is_tgt) {
|
||||
SASSERT(m_ready);
|
||||
expr_ref_vector result(m);
|
||||
sort_ref_vector sorts(m);
|
||||
ptr_vector<sort> sorts;
|
||||
expr_ref v(m), w(m);
|
||||
r.get_vars(sorts);
|
||||
for (unsigned i = 0; i < sorts.size(); ++i) {
|
||||
if (!sorts[i].get()) {
|
||||
if (!sorts[i]) {
|
||||
sorts[i] = m.mk_bool_sort();
|
||||
}
|
||||
v = m.mk_var(i, sorts[i].get());
|
||||
v = m.mk_var(i, sorts[i]);
|
||||
m_subst.apply(2, m_deltas, expr_offset(v, is_tgt?0:1), w);
|
||||
result.push_back(w);
|
||||
}
|
||||
|
|
|
|||
|
|
@ -41,6 +41,7 @@ Revision History:
|
|||
#include"expr_replacer.h"
|
||||
#include"bool_rewriter.h"
|
||||
#include"qe_lite.h"
|
||||
#include"expr_safe_replace.h"
|
||||
|
||||
namespace datalog {
|
||||
|
||||
|
|
@ -130,17 +131,15 @@ namespace datalog {
|
|||
return index;
|
||||
}
|
||||
// replace vars by de-bruijn indices
|
||||
expr_substitution sub(m);
|
||||
expr_safe_replace rep(m);
|
||||
for (unsigned i = 0; i < vars.size(); ++i) {
|
||||
app* v = vars[i].get();
|
||||
if (names) {
|
||||
names->push_back(v->get_decl()->get_name());
|
||||
}
|
||||
sub.insert(v, m.mk_var(index++,m.get_sort(v)));
|
||||
rep.insert(v, m.mk_var(index++,m.get_sort(v)));
|
||||
}
|
||||
scoped_ptr<expr_replacer> rep = mk_default_expr_replacer(m);
|
||||
rep->set_substitution(&sub);
|
||||
(*rep)(fml);
|
||||
rep(fml);
|
||||
return index;
|
||||
}
|
||||
|
||||
|
|
@ -936,7 +935,7 @@ namespace datalog {
|
|||
}
|
||||
}
|
||||
|
||||
void rule::get_vars(sort_ref_vector& sorts) const {
|
||||
void rule::get_vars(ptr_vector<sort>& sorts) const {
|
||||
sorts.reset();
|
||||
used_vars used;
|
||||
get_used_vars(used);
|
||||
|
|
|
|||
|
|
@ -244,7 +244,7 @@ namespace datalog {
|
|||
|
||||
void norm_vars(rule_manager & rm);
|
||||
|
||||
void get_vars(sort_ref_vector& sorts) const;
|
||||
void get_vars(ptr_vector<sort>& sorts) const;
|
||||
|
||||
void to_formula(expr_ref& result) const;
|
||||
|
||||
|
|
|
|||
|
|
@ -440,7 +440,7 @@ namespace pdr {
|
|||
unsigned ut_size = r.get_uninterpreted_tail_size();
|
||||
unsigned t_size = r.get_tail_size();
|
||||
var_subst vs(m, false);
|
||||
sort_ref_vector vars(m);
|
||||
ptr_vector<sort> vars;
|
||||
uint_set empty_index_set;
|
||||
qe_lite qe(m);
|
||||
|
||||
|
|
|
|||
|
|
@ -2365,7 +2365,7 @@ namespace smt2 {
|
|||
parser(cmd_context & ctx, std::istream & is, bool interactive, params_ref const & p):
|
||||
m_ctx(ctx),
|
||||
m_params(p),
|
||||
m_scanner(ctx, is, interactive, p),
|
||||
m_scanner(ctx, is, interactive),
|
||||
m_curr(scanner::NULL_TOKEN),
|
||||
m_curr_cmd(0),
|
||||
m_num_bindings(0),
|
||||
|
|
|
|||
|
|
@ -242,7 +242,7 @@ namespace smt2 {
|
|||
}
|
||||
}
|
||||
|
||||
scanner::scanner(cmd_context & ctx, std::istream& stream, bool interactive, params_ref const & _p):
|
||||
scanner::scanner(cmd_context & ctx, std::istream& stream, bool interactive):
|
||||
m_ctx(ctx),
|
||||
m_interactive(interactive),
|
||||
m_spos(0),
|
||||
|
|
@ -254,9 +254,8 @@ namespace smt2 {
|
|||
m_bend(0),
|
||||
m_stream(stream),
|
||||
m_cache_input(false) {
|
||||
|
||||
parser_params p(_p);
|
||||
m_smtlib2_compliant = p.smt2_compliant();
|
||||
|
||||
m_smtlib2_compliant = ctx.params().m_smtlib2_compliant;
|
||||
|
||||
for (int i = 0; i < 256; ++i) {
|
||||
m_normalized[i] = (char) i;
|
||||
|
|
|
|||
|
|
@ -76,7 +76,7 @@ namespace smt2 {
|
|||
EOF_TOKEN
|
||||
};
|
||||
|
||||
scanner(cmd_context & ctx, std::istream& stream, bool interactive = false, params_ref const & p = params_ref());
|
||||
scanner(cmd_context & ctx, std::istream& stream, bool interactive = false);
|
||||
|
||||
~scanner() {}
|
||||
|
||||
|
|
|
|||
|
|
@ -3,4 +3,4 @@ def_module_params('parser',
|
|||
params=(('ignore_user_patterns', BOOL, False, 'ignore patterns provided by the user'),
|
||||
('ignore_bad_patterns', BOOL, True, 'ignore malformed patterns'),
|
||||
('error_for_visual_studio', BOOL, False, 'display error messages in Visual Studio format'),
|
||||
('smt2_compliant', BOOL, False, 'enable/disable SMT-LIB 2.0 compliance')))
|
||||
))
|
||||
|
|
|
|||
|
|
@ -142,6 +142,14 @@ namespace smt {
|
|||
}
|
||||
};
|
||||
|
||||
struct initn : public instruction {
|
||||
// We need that because starting at Z3 3.0, some associative
|
||||
// operators (e.g., + and *) are represented using n-ary
|
||||
// applications.
|
||||
// We do not need the extra field for INIT1, ..., INIT6.
|
||||
unsigned m_num_args;
|
||||
};
|
||||
|
||||
struct compare : public instruction {
|
||||
unsigned m_reg1;
|
||||
unsigned m_reg2;
|
||||
|
|
@ -608,7 +616,18 @@ namespace smt {
|
|||
instruction * mk_init(unsigned n) {
|
||||
SASSERT(n >= 1);
|
||||
opcode op = n <= 6 ? static_cast<opcode>(INIT1 + n - 1) : INITN;
|
||||
return mk_instr<instruction>(op, sizeof(instruction));
|
||||
if (op == INITN) {
|
||||
// We store the actual number of arguments for INITN.
|
||||
// Starting at Z3 3.0, some associative operators
|
||||
// (e.g., + and *) are represented using n-ary
|
||||
// applications.
|
||||
initn * r = mk_instr<initn>(op, sizeof(initn));
|
||||
r->m_num_args = n;
|
||||
return r;
|
||||
}
|
||||
else {
|
||||
return mk_instr<instruction>(op, sizeof(instruction));
|
||||
}
|
||||
}
|
||||
|
||||
public:
|
||||
|
|
@ -2345,6 +2364,8 @@ namespace smt {
|
|||
case INITN:
|
||||
m_app = m_registers[0];
|
||||
m_num_args = m_app->get_num_args();
|
||||
if (m_num_args != static_cast<const initn *>(m_pc)->m_num_args)
|
||||
goto backtrack;
|
||||
for (unsigned i = 0; i < m_num_args; i++)
|
||||
m_registers[i+1] = m_app->get_arg(i);
|
||||
m_pc = m_pc->m_next;
|
||||
|
|
@ -3982,3 +4003,8 @@ namespace smt {
|
|||
}
|
||||
};
|
||||
|
||||
#ifdef Z3DEBUG
|
||||
void pp(smt::code_tree * c) {
|
||||
c->display(std::cout);
|
||||
}
|
||||
#endif
|
||||
|
|
|
|||
|
|
@ -32,6 +32,7 @@ void smt_params::updt_local_params(params_ref const & _p) {
|
|||
m_delay_units = p.delay_units();
|
||||
m_delay_units_threshold = p.delay_units_threshold();
|
||||
m_preprocess = _p.get_bool("preprocess", true); // hidden parameter
|
||||
m_soft_timeout = p.soft_timeout();
|
||||
if (_p.get_bool("arith.greatest_error_pivot", false))
|
||||
m_arith_pivot_strategy = ARITH_PIVOT_GREATEST_ERROR;
|
||||
else if (_p.get_bool("arith.least_error_pivot", false))
|
||||
|
|
@ -48,7 +49,6 @@ void smt_params::updt_params(params_ref const & p) {
|
|||
|
||||
void smt_params::updt_params(context_params const & p) {
|
||||
m_auto_config = p.m_auto_config;
|
||||
m_soft_timeout = p.m_timeout;
|
||||
m_model = p.m_model;
|
||||
m_model_validate = p.m_model_validate;
|
||||
}
|
||||
|
|
|
|||
|
|
@ -7,13 +7,14 @@ def_module_params(module_name='smt',
|
|||
('relevancy', UINT, 2, 'relevancy propagation heuristic: 0 - disabled, 1 - relevancy is tracked by only affects quantifier instantiation, 2 - relevancy is tracked, and an atom is only asserted if it is relevant'),
|
||||
('macro_finder', BOOL, False, 'try to find universally quantified formulas that can be viewed as macros'),
|
||||
('ematching', BOOL, True, 'E-Matching based quantifier instantiation'),
|
||||
('phase_selection', UINT, 4, 'phase selection heuristic: 0 - always false, 1 - always true, 2 - phase caching, 3 - phase caching conservative, 4 - phase caching conservative 2, 5 - random, 6 - number of occurrences'),
|
||||
('phase_selection', UINT, 3, 'phase selection heuristic: 0 - always false, 1 - always true, 2 - phase caching, 3 - phase caching conservative, 4 - phase caching conservative 2, 5 - random, 6 - number of occurrences'),
|
||||
('restart_strategy', UINT, 1, '0 - geometric, 1 - inner-outer-geometric, 2 - luby, 3 - fixed, 4 - arithmetic'),
|
||||
('restart_factor', DOUBLE, 1.1, 'when using geometric (or inner-outer-geometric) progression of restarts, it specifies the constant used to multiply the currect restart threshold'),
|
||||
('case_split', UINT, 1, '0 - case split based on variable activity, 1 - similar to 0, but delay case splits created during the search, 2 - similar to 0, but cache the relevancy, 3 - case split based on relevancy (structural splitting), 4 - case split on relevancy and activity, 5 - case split on relevancy and current goal'),
|
||||
('delay_units', BOOL, False, 'if true then z3 will not restart when a unit clause is learned'),
|
||||
('delay_units_threshold', UINT, 32, 'maximum number of learned unit clauses before restarting, ingored if delay_units is false'),
|
||||
('pull_nested_quantifiers', BOOL, False, 'pull nested quantifiers'),
|
||||
('soft_timeout', UINT, 0, 'soft timeout (0 means no timeout)'),
|
||||
('mbqi', BOOL, True, 'model based quantifier instantiation (MBQI)'),
|
||||
('mbqi.max_cexs', UINT, 1, 'initial maximal number of counterexamples used in MBQI, each counterexample generates a quantifier instantiation'),
|
||||
('mbqi.max_cexs_incr', UINT, 0, 'increment for MBQI_MAX_CEXS, the increment is performed after each round of MBQI'),
|
||||
|
|
|
|||
|
|
@ -155,7 +155,7 @@ bool eval(func_interp & fi, simplifier & s, expr * const * args, expr_ref & resu
|
|||
basic_simplifier_plugin * bs = static_cast<basic_simplifier_plugin*>(s.get_plugin(fi.m().get_basic_family_id()));
|
||||
for (unsigned k = 0; k < fi.num_entries(); k++) {
|
||||
func_entry const * curr = fi.get_entry(k);
|
||||
SASSERT(!curr->eq_args(fi.get_arity(), args));
|
||||
SASSERT(!curr->eq_args(fi.m(), fi.get_arity(), args));
|
||||
if (!actuals_are_values || !curr->args_are_values()) {
|
||||
expr_ref_buffer eqs(fi.m());
|
||||
unsigned i = fi.get_arity();
|
||||
|
|
|
|||
|
|
@ -907,7 +907,7 @@ namespace smt {
|
|||
}
|
||||
enode * e = enode::mk(m_manager, m_region, m_app2enode, n, generation, suppress_args, merge_tf, m_scope_lvl, cgc_enabled, true);
|
||||
TRACE("mk_enode_detail", tout << "e.get_num_args() = " << e->get_num_args() << "\n";);
|
||||
if (n->get_num_args() == 0 && m_manager.is_value(n))
|
||||
if (n->get_num_args() == 0 && m_manager.is_unique_value(n))
|
||||
e->mark_as_interpreted();
|
||||
TRACE("mk_var_bug", tout << "mk_enode: " << id << "\n";);
|
||||
TRACE("generation", tout << "mk_enode: " << id << " " << generation << "\n";);
|
||||
|
|
|
|||
|
|
@ -139,6 +139,7 @@ public:
|
|||
ast_manager & m = in->m();
|
||||
TRACE("smt_tactic", tout << this << "\nAUTO_CONFIG: " << fparams().m_auto_config << " HIDIV0: " << fparams().m_hi_div0 << " "
|
||||
<< " PREPROCESS: " << fparams().m_preprocess << "\n";
|
||||
tout << "RELEVANCY: " << fparams().m_relevancy_lvl << "\n";
|
||||
tout << "fail-if-inconclusive: " << m_fail_if_inconclusive << "\n";
|
||||
tout << "params_ref: " << m_params_ref << "\n";);
|
||||
TRACE("smt_tactic_detail", in->display(tout););
|
||||
|
|
|
|||
|
|
@ -49,6 +49,8 @@ public:
|
|||
|
||||
virtual bool is_value(app*) const;
|
||||
|
||||
virtual bool is_unique_value(app * a) const { return is_value(a); }
|
||||
|
||||
bool is_value(func_decl *) const;
|
||||
|
||||
virtual void get_op_names(svector<builtin_name> & op_names, symbol const & logic);
|
||||
|
|
|
|||
|
|
@ -355,12 +355,12 @@ struct cofactor_elim_term_ite::imp {
|
|||
expr * lhs;
|
||||
expr * rhs;
|
||||
if (m.is_eq(t, lhs, rhs)) {
|
||||
if (m.is_value(lhs)) {
|
||||
if (m.is_unique_value(lhs)) {
|
||||
m_term = rhs;
|
||||
m_value = to_app(lhs);
|
||||
TRACE("set_cofactor_atom", tout << "term:\n" << mk_ismt2_pp(m_term, m) << "\nvalue: " << mk_ismt2_pp(m_value, m) << "\n";);
|
||||
}
|
||||
else if (m.is_value(rhs)) {
|
||||
else if (m.is_unique_value(rhs)) {
|
||||
m_term = lhs;
|
||||
m_value = to_app(rhs);
|
||||
TRACE("set_cofactor_atom", tout << "term:\n" << mk_ismt2_pp(m_term, m) << "\nvalue: " << mk_ismt2_pp(m_value, m) << "\n";);
|
||||
|
|
|
|||
|
|
@ -128,7 +128,7 @@ struct reduce_args_tactic::imp {
|
|||
unsigned j = n->get_num_args();
|
||||
while (j > 0) {
|
||||
--j;
|
||||
if (m_manager.is_value(n->get_arg(j)))
|
||||
if (m_manager.is_unique_value(n->get_arg(j)))
|
||||
return;
|
||||
}
|
||||
m_non_cadidates.insert(d);
|
||||
|
|
@ -185,13 +185,13 @@ struct reduce_args_tactic::imp {
|
|||
it->m_value.reserve(j);
|
||||
while (j > 0) {
|
||||
--j;
|
||||
it->m_value.set(j, m_manager.is_value(n->get_arg(j)));
|
||||
it->m_value.set(j, m_manager.is_unique_value(n->get_arg(j)));
|
||||
}
|
||||
} else {
|
||||
SASSERT(j == it->m_value.size());
|
||||
while (j > 0) {
|
||||
--j;
|
||||
it->m_value.set(j, it->m_value.get(j) && m_manager.is_value(n->get_arg(j)));
|
||||
it->m_value.set(j, it->m_value.get(j) && m_manager.is_unique_value(n->get_arg(j)));
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -559,10 +559,10 @@ public:
|
|||
ts.push_back(m_ts.get(i)->translate(*new_m));
|
||||
}
|
||||
|
||||
unsigned finished_id = UINT_MAX;
|
||||
par_exception_kind ex_kind;
|
||||
unsigned finished_id = UINT_MAX;
|
||||
par_exception_kind ex_kind = DEFAULT_EX;
|
||||
std::string ex_msg;
|
||||
unsigned error_code;
|
||||
unsigned error_code = 0;
|
||||
|
||||
#pragma omp parallel for
|
||||
for (int i = 0; i < static_cast<int>(sz); i++) {
|
||||
|
|
@ -734,8 +734,8 @@ public:
|
|||
|
||||
bool found_solution = false;
|
||||
bool failed = false;
|
||||
par_exception_kind ex_kind;
|
||||
unsigned error_code;
|
||||
par_exception_kind ex_kind = DEFAULT_EX;
|
||||
unsigned error_code = 0;
|
||||
std::string ex_msg;
|
||||
|
||||
#pragma omp parallel for
|
||||
|
|
@ -1242,8 +1242,7 @@ public:
|
|||
virtual void updt_params(params_ref const & p) {
|
||||
TRACE("using_params",
|
||||
tout << "before p: " << p << "\n";
|
||||
tout << "m_params: " << m_params << "\n";
|
||||
;);
|
||||
tout << "m_params: " << m_params << "\n";);
|
||||
|
||||
params_ref new_p = p;
|
||||
new_p.append(m_params);
|
||||
|
|
|
|||
|
|
@ -62,9 +62,8 @@ tactic * mk_ufbv_preprocessor_tactic(ast_manager & m, params_ref const & p) {
|
|||
tactic * mk_ufbv_tactic(ast_manager & m, params_ref const & p) {
|
||||
params_ref main_p(p);
|
||||
main_p.set_bool("mbqi", true);
|
||||
main_p.set_uint("mbqi_max_iterations", -1);
|
||||
main_p.set_uint("mbqi.max_iterations", UINT_MAX);
|
||||
main_p.set_bool("elim_and", true);
|
||||
main_p.set_bool("solver", true);
|
||||
|
||||
tactic * t = and_then(repeat(mk_ufbv_preprocessor_tactic(m, main_p), 2),
|
||||
mk_smt_tactic_using(false, main_p));
|
||||
|
|
|
|||
|
|
@ -260,8 +260,8 @@ public:
|
|||
\brief c <- a - b
|
||||
*/
|
||||
void sub(interval const & a, interval const & b, interval & c) {
|
||||
m().sub(a.m_lower, b.m_lower, c.m_lower);
|
||||
m().sub(a.m_upper, b.m_upper, c.m_upper);
|
||||
m().sub(a.m_lower, b.m_upper, c.m_lower);
|
||||
m().sub(a.m_upper, b.m_lower, c.m_upper);
|
||||
}
|
||||
|
||||
private:
|
||||
|
|
|
|||
|
|
@ -165,7 +165,7 @@ public:
|
|||
if (*name == ':')
|
||||
name++;
|
||||
std::string tmp = name;
|
||||
unsigned n = tmp.size();
|
||||
unsigned n = static_cast<unsigned>(tmp.size());
|
||||
for (unsigned i = 0; i < n; i++) {
|
||||
if (tmp[i] >= 'A' && tmp[i] <= 'Z')
|
||||
tmp[i] = tmp[i] - 'A' + 'a';
|
||||
|
|
|
|||
|
|
@ -21,13 +21,15 @@ Notes:
|
|||
#include"symbol.h"
|
||||
#include"dictionary.h"
|
||||
|
||||
params_ref params_ref::g_empty_params_ref;
|
||||
|
||||
std::string norm_param_name(char const * n) {
|
||||
if (n == 0)
|
||||
return "_";
|
||||
if (*n == ':')
|
||||
n++;
|
||||
std::string r = n;
|
||||
unsigned sz = r.size();
|
||||
unsigned sz = static_cast<unsigned>(r.size());
|
||||
if (sz == 0)
|
||||
return "_";
|
||||
for (unsigned i = 0; i < sz; i++) {
|
||||
|
|
@ -133,7 +135,7 @@ struct param_descrs::imp {
|
|||
if (smt2_style)
|
||||
out << ':';
|
||||
char const * s = it2->bare_str();
|
||||
unsigned n = strlen(s);
|
||||
unsigned n = static_cast<unsigned>(strlen(s));
|
||||
for (unsigned i = 0; i < n; i++) {
|
||||
if (smt2_style && s[i] == '_')
|
||||
out << '-';
|
||||
|
|
|
|||
|
|
@ -31,6 +31,8 @@ class params;
|
|||
class param_descrs;
|
||||
|
||||
class params_ref {
|
||||
static params_ref g_empty_params_ref;
|
||||
|
||||
params * m_params;
|
||||
void init();
|
||||
void copy_core(params const * p);
|
||||
|
|
@ -38,7 +40,9 @@ public:
|
|||
params_ref():m_params(0) {}
|
||||
params_ref(params_ref const & p);
|
||||
~params_ref();
|
||||
|
||||
|
||||
static params_ref const & get_empty() { return g_empty_params_ref; }
|
||||
|
||||
params_ref & operator=(params_ref const & p);
|
||||
|
||||
// copy params from src
|
||||
|
|
|
|||
|
|
@ -43,7 +43,7 @@ Revision History:
|
|||
#define CLOCKID CLOCK_PROCESS_CPUTIME_ID
|
||||
#else
|
||||
// FreeBSD does not support CLOCK_PROCESS_CPUTIME_ID
|
||||
#define CLOCKID CLOCK_PROF
|
||||
#define CLOCKID CLOCK_MONOTONIC
|
||||
#endif
|
||||
#define SIG SIGRTMIN
|
||||
// ---------
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue