mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
merged
This commit is contained in:
commit
84aeba94a5
|
@ -24,6 +24,8 @@ Version 4.3.2
|
|||
|
||||
- Added new option to mk_make to allow users to specify where python bindings (Z3Py) will be installed. (Thanks to Dejan Jovanovic for reporting the problem).
|
||||
|
||||
- Fixed crash reported at http://z3.codeplex.com/workitem/10
|
||||
|
||||
Version 4.3.1
|
||||
=============
|
||||
|
||||
|
|
|
@ -22,6 +22,10 @@ Notes:
|
|||
#include"api_log_macros.h"
|
||||
#include"api_context.h"
|
||||
#include"algebraic_numbers.h"
|
||||
#include"expr2polynomial.h"
|
||||
#include"cancel_eh.h"
|
||||
#include"scoped_timer.h"
|
||||
#include"api_ast_vector.h"
|
||||
|
||||
extern "C" {
|
||||
|
||||
|
@ -318,12 +322,67 @@ extern "C" {
|
|||
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();
|
||||
// TODO
|
||||
return 0;
|
||||
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);
|
||||
}
|
||||
|
||||
|
@ -331,8 +390,31 @@ extern "C" {
|
|||
Z3_TRY;
|
||||
LOG_Z3_algebraic_eval(c, p, n, a);
|
||||
RESET_ERROR_CODE();
|
||||
// TODO
|
||||
return 0;
|
||||
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);
|
||||
}
|
||||
|
||||
|
|
|
@ -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,7 +137,7 @@ namespace api {
|
|||
{
|
||||
if (m_interruptable)
|
||||
(*m_interruptable)();
|
||||
m_manager.set_cancel(true);
|
||||
m().set_cancel(true);
|
||||
}
|
||||
}
|
||||
|
||||
|
@ -196,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;
|
||||
} }
|
||||
|
@ -217,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);
|
||||
}
|
||||
|
@ -325,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
|
||||
|
|
34
src/api/api_polynomial.cpp
Normal file
34
src/api/api_polynomial.cpp
Normal file
|
@ -0,0 +1,34 @@
|
|||
/*++
|
||||
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"api_polynomial.h"
|
||||
|
||||
namespace api {
|
||||
|
||||
pmanager::pmanager():
|
||||
m_pm(m_nm) {
|
||||
}
|
||||
|
||||
pmanager::~pmanager() {
|
||||
}
|
||||
|
||||
void pmanager::set_cancel(bool f) {
|
||||
m_pm.set_cancel(f);
|
||||
}
|
||||
|
||||
};
|
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
|
|
@ -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
|
||||
|
|
|
@ -58,6 +58,29 @@ class Numeral:
|
|||
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):
|
||||
|
@ -481,6 +504,58 @@ class Numeral:
|
|||
|
||||
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
|
||||
|
|
|
@ -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 {
|
||||
|
|
|
@ -592,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() {
|
||||
|
|
|
@ -79,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());
|
||||
}
|
||||
|
@ -99,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) {
|
||||
|
@ -113,6 +117,7 @@ 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) {
|
||||
|
@ -133,4 +138,15 @@ void context_params::init_solver_params(ast_manager & m, solver & s, params_ref
|
|||
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;
|
||||
}
|
||||
|
||||
|
||||
|
|
|
@ -37,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();
|
||||
|
@ -63,6 +64,11 @@ public:
|
|||
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();
|
||||
};
|
||||
|
||||
|
||||
|
|
|
@ -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);
|
||||
|
||||
|
|
|
@ -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
|
||||
|
|
Loading…
Reference in a new issue