From 3b64265c27266bbf69ca62037c89be4f7487dc83 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 9 Aug 2013 09:15:04 -0700 Subject: [PATCH 1/3] remove duplicated definition of is_store and is_select Signed-off-by: Nikolaj Bjorner --- src/api/python/z3.py | 29 ++------------------- src/ast/simplifier/bv_simplifier_plugin.cpp | 2 +- src/muz_qe/qe_lite.cpp | 9 ++++++- 3 files changed, 11 insertions(+), 29 deletions(-) diff --git a/src/api/python/z3.py b/src/api/python/z3.py index bbd267292..739a9e61a 100644 --- a/src/api/python/z3.py +++ b/src/api/python/z3.py @@ -3856,32 +3856,6 @@ def is_array(a): """ return isinstance(a, ArrayRef) -def is_select(a): - """Return `True` if `a` is a Z3 array select. - - >>> a = Array('a', IntSort(), IntSort()) - >>> is_select(a) - False - >>> i = Int('i') - >>> is_select(a[i]) - True - """ - return is_app_of(a, Z3_OP_SELECT) - -def is_store(a): - """Return `True` if `a` is a Z3 array store. - - >>> a = Array('a', IntSort(), IntSort()) - >>> is_store(a) - False - >>> i = Int('i') - >>> is_store(a[i]) - False - >>> is_store(Store(a, i, i + 1)) - True - """ - return is_app_of(a, Z3_OP_STORE) - def is_const_array(a): """Return `True` if `a` is a Z3 constant array. @@ -4072,7 +4046,8 @@ def is_select(a): >>> a = Array('a', IntSort(), IntSort()) >>> is_select(a) False - >>> is_select(a[0]) + >>> i = Int('i') + >>> is_select(a[i]) True """ return is_app_of(a, Z3_OP_SELECT) diff --git a/src/ast/simplifier/bv_simplifier_plugin.cpp b/src/ast/simplifier/bv_simplifier_plugin.cpp index 8ee353a76..45fee07e4 100644 --- a/src/ast/simplifier/bv_simplifier_plugin.cpp +++ b/src/ast/simplifier/bv_simplifier_plugin.cpp @@ -179,7 +179,7 @@ bool bv_simplifier_plugin::reduce(func_decl * f, unsigned num_args, expr * const } SASSERT(result.get()); - TRACE("bv_simplifier", + TRACE("bv_simplifier", tout << mk_pp(f, m_manager) << "\n"; for (unsigned i = 0; i < num_args; ++i) { tout << mk_pp(args[i], m_manager) << " "; diff --git a/src/muz_qe/qe_lite.cpp b/src/muz_qe/qe_lite.cpp index f840f19d6..01537b574 100644 --- a/src/muz_qe/qe_lite.cpp +++ b/src/muz_qe/qe_lite.cpp @@ -799,9 +799,15 @@ namespace ar { } /** - Ex A. A[x] = t & Phi where x \not\in A, t. + Ex A. A[x] = t & Phi where x \not\in A, t. A \not\in t, x => Ex A. Phi[store(A,x,t)] + + Perhaps also: + Ex A. store(A,y,z)[x] = t & Phi where x \not\in A, t, y, z, A \not\in y z, t + => + Ex A, v . (x = y => z = t) & Phi[store(store(A,x,t),y,v)] + */ bool solve_select(expr_ref_vector& conjs, unsigned i, expr* e1, expr* e2) { @@ -827,6 +833,7 @@ namespace ar { expr_safe_replace rep(m); rep.insert(A, B); expr_ref tmp(m); + std::cout << mk_pp(e1, m) << " = " << mk_pp(e2, m) << "\n"; for (unsigned j = 0; j < conjs.size(); ++j) { if (i == j) { conjs[j] = m.mk_true(); From 0fd94a033f86f2c8c3750234cabda95d93cad719 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 12 Aug 2013 09:52:10 -0700 Subject: [PATCH 2/3] change non-null test Signed-off-by: Nikolaj Bjorner --- src/api/api_context.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/api/api_context.cpp b/src/api/api_context.cpp index cf179332a..05e1ca675 100644 --- a/src/api/api_context.cpp +++ b/src/api/api_context.cpp @@ -139,7 +139,7 @@ namespace api { if (m_interruptable) (*m_interruptable)(); m().set_cancel(true); - if (m_rcf_manager.get() == 0) + if (m_rcf_manager.get() != 0) m_rcf_manager->set_cancel(true); } } From 6c5f7741b2d100d325228db1de5d1960fc20ea0f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 14 Aug 2013 11:55:23 -0700 Subject: [PATCH 3/3] more on polynorm Signed-off-by: Nikolaj Bjorner --- src/smt/theory_dl.cpp | 2 +- src/test/polynorm.cpp | 109 ++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 110 insertions(+), 1 deletion(-) diff --git a/src/smt/theory_dl.cpp b/src/smt/theory_dl.cpp index 9c3489aec..4ef1bd8e0 100644 --- a/src/smt/theory_dl.cpp +++ b/src/smt/theory_dl.cpp @@ -91,7 +91,7 @@ namespace smt { rational val; if (ctx.e_internalized(rep_of) && th_bv && th_bv->get_fixed_value(rep_of.get(), val)) { - result = m_th.u().mk_numeral(val.get_int64(), s); + result = m_th.u().mk_numeral(val.get_int64(), s); } else { result = m_th.u().mk_numeral(0, s); diff --git a/src/test/polynorm.cpp b/src/test/polynorm.cpp index 092ac022a..3593e98ce 100644 --- a/src/test/polynorm.cpp +++ b/src/test/polynorm.cpp @@ -2,6 +2,7 @@ #include "smt2parser.h" #include "arith_decl_plugin.h" #include "reg_decl_plugins.h" +#include "arith_rewriter.h" #include "ast_pp.h" @@ -27,6 +28,114 @@ static char const* example1 = "(= (+ (- (* x x) (* 2 y)) y) 0)"; static char const* example2 = "(= (+ 4 3 (- (* x x) (* 2 y)) y) 0)"; +class poly_nf { + expr_ref m_coefficient; + expr_ref_vector m_coefficients; + expr_ref_vector m_factors; +public: + poly_nf(ast_manager& m): + m_coefficient(m), + m_coefficients(m), + m_factors(m) {} + + expr_ref& coefficient() { return m_coefficient; } + expr_ref_vector& coefficients() { return m_coefficients; } + expr_ref_vector& factors() { return m_factors; } + + void reset() { + m_coefficient.reset(); + m_coefficients.reset(); + m_factors.reset(); + } + +}; + +class polynorm { + ast_manager& m; + arith_util m_arith; + arith_rewriter m_arith_rw; + th_rewriter m_rw; +public: + polynorm(ast_manager& m): m(m), m_arith(m), m_arith_rw(m), m_rw(m) {} + +private: + expr_ref_vector mk_fresh_constants(unsigned num, sort* s) { + expr_ref_vector result(m); + for (unsigned i = 0; i < num; ++i) { + result.push_back(m.mk_fresh_const("fresh", s)); + } + return result; + } + + expr_ref_vector mk_fresh_reals(unsigned num) { + return mk_fresh_constants(num, m_arith.mk_real()); + } + + expr_ref mk_mul(unsigned num_args, expr* const* args) { + expr_ref result(m); + m_arith_rw.mk_mul(num_args, args, result); + return result; + } + + void nf(expr_ref& term, obj_hashtable& constants, poly_nf& poly) { + + expr_ref_vector& factors = poly.factors(); + expr_ref_vector& coefficients = poly.coefficients(); + expr_ref& coefficient = poly.coefficient(); + + m_rw(term); + + if (m_arith.is_add(term)) { + factors.append(to_app(term)->get_num_args(), to_app(term)->get_args()); + } + else { + factors.push_back(term); + } + for (unsigned i = 0; i < factors.size(); ++i) { + expr* f = factors[i].get(); + unsigned num_args = 1; + expr* const* args = &f; + if (m_arith.is_mul(f)) { + num_args = to_app(f)->get_num_args(); + args = to_app(f)->get_args(); + } + for (unsigned j = 0; j < num_args; ++j) { + if (m_arith.is_numeral(args[j]) || constants.contains(args[j])) { + //consts.push_back(args[j]); + } + else { + // vars.push_back(args[j]); + } + // deal with the relevant corner cases. + } +#if 0 + rational r; + if (m_arith.is_mul(f) && m_arith.is_numeral(to_app(f)->get_arg(0), r)) { + coefficients.push_back(r); + factors[i] = mk_mul(to_app(f)->get_num_args()-1, to_app(f)->get_args()+1); + } + else if (m_arith.is_numeral(f, r)) { + factors[i] = factors.back(); + factors.pop_back(); + SASSERT(coefficient.is_zero()); + SASSERT(!r.is_zero()); + coefficient = r; + --i; // repeat examining 'i' + } + else { + coefficients.push_back(rational(1)); + } +#endif + } + + TRACE("polynorm", + tout << mk_pp(coefficient, m) << "\n"; + for (unsigned i = 0; i < factors.size(); ++i) { + tout << mk_pp(factors[i].get(), m) << " * " << mk_pp(coefficients[i].get(), m) << "\n"; + }); + } +}; + // ast /// sort : ast /// func_decl : ast