From 2f216ee5c1952bafae36b9f5905310ca8069181e Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Tue, 3 Nov 2015 15:35:43 +0000 Subject: [PATCH 1/6] Fixed PREFIX for OSX installation. Fixes #124. --- scripts/mk_util.py | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index e53a90127..0baed2968 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -75,7 +75,7 @@ VER_MAJOR=None VER_MINOR=None VER_BUILD=None VER_REVISION=None -PREFIX=os.path.split(os.path.split(os.path.split(PYTHON_PACKAGE_DIR)[0])[0])[0] +PREFIX=sys.prefix GMP=False FOCI2=False FOCI2LIB='' @@ -531,6 +531,7 @@ if os.name == 'nt': elif os.name == 'posix': if os.uname()[0] == 'Darwin': IS_OSX=True + PREFIX="/usr/local" elif os.uname()[0] == 'Linux': IS_LINUX=True elif os.uname()[0] == 'FreeBSD': @@ -1984,6 +1985,7 @@ def mk_config(): print('Prefix: %s' % PREFIX) print('64-bit: %s' % is64()) print('FP math: %s' % FPMATH) + print("Python pkg dir: %s" % PYTHON_PACKAGE_DIR) if GPROF: print('gprof: enabled') print('Python version: %s' % distutils.sysconfig.get_python_version()) @@ -2074,8 +2076,6 @@ def mk_makefile(): # Finalize if VERBOSE: print("Makefile was successfully generated.") - if not IS_WINDOWS: - print(" python packages dir: %s" % PYTHON_PACKAGE_DIR) if DEBUG_MODE: print(" compilation mode: Debug") else: From 715050da0b73b83fe7dad16ff645924d724425d7 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Wed, 4 Nov 2015 13:34:50 +0000 Subject: [PATCH 2/6] Java API comments fix. --- src/api/java/Model.java | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/api/java/Model.java b/src/api/java/Model.java index e9922ac58..28934a1f3 100644 --- a/src/api/java/Model.java +++ b/src/api/java/Model.java @@ -56,7 +56,7 @@ public class Model extends Z3Object Native.getRange(getContext().nCtx(), f.getNativeObject())) == Z3_sort_kind.Z3_ARRAY_SORT .toInt()) throw new Z3Exception( - "Non-zero arity functions and arrays have FunctionInterpretations as a model. Use FuncInterp."); + "Non-zero arity functions and arrays have FunctionInterpretations as a model. Use getFuncInterp."); long n = Native.modelGetConstInterp(getContext().nCtx(), getNativeObject(), f.getNativeObject()); @@ -101,7 +101,7 @@ public class Model extends Z3Object } else { throw new Z3Exception( - "Constant functions do not have a function interpretation; use ConstInterp"); + "Constant functions do not have a function interpretation; use getConstInterp"); } } else { From ebbed7a92e19c43e680eb6514be5fc90f37c221a Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Wed, 4 Nov 2015 15:44:29 +0000 Subject: [PATCH 3/6] Added tactic comments for QF_AUFLIA, QF_AUFBV, QF_UF, and QF_UFBV default tactics. --- src/tactic/smtlogics/qfaufbv_tactic.h | 4 ++++ src/tactic/smtlogics/qfauflia_tactic.h | 4 ++++ src/tactic/smtlogics/qfidl_tactic.h | 4 ++++ src/tactic/smtlogics/qfuf_tactic.h | 4 ++++ src/tactic/smtlogics/qfufbv_tactic.h | 6 +++++- 5 files changed, 21 insertions(+), 1 deletion(-) diff --git a/src/tactic/smtlogics/qfaufbv_tactic.h b/src/tactic/smtlogics/qfaufbv_tactic.h index d4503a5de..1e4a7419f 100644 --- a/src/tactic/smtlogics/qfaufbv_tactic.h +++ b/src/tactic/smtlogics/qfaufbv_tactic.h @@ -25,4 +25,8 @@ class tactic; tactic * mk_qfaufbv_tactic(ast_manager & m, params_ref const & p = params_ref()); +/* + ADD_TACTIC("qfaufbv", "builtin strategy for solving QF_AUFBV problems.", "mk_qfaufbv_tactic(m, p)") +*/ + #endif diff --git a/src/tactic/smtlogics/qfauflia_tactic.h b/src/tactic/smtlogics/qfauflia_tactic.h index 10b790e70..fbf19fec0 100644 --- a/src/tactic/smtlogics/qfauflia_tactic.h +++ b/src/tactic/smtlogics/qfauflia_tactic.h @@ -25,4 +25,8 @@ class tactic; tactic * mk_qfauflia_tactic(ast_manager & m, params_ref const & p = params_ref()); +/* + ADD_TACTIC("qfauflia", "builtin strategy for solving QF_AUFLIA problems.", "mk_qfauflia_tactic(m, p)") +*/ + #endif diff --git a/src/tactic/smtlogics/qfidl_tactic.h b/src/tactic/smtlogics/qfidl_tactic.h index f502dbd89..f892bb8a5 100644 --- a/src/tactic/smtlogics/qfidl_tactic.h +++ b/src/tactic/smtlogics/qfidl_tactic.h @@ -25,4 +25,8 @@ class tactic; tactic * mk_qfidl_tactic(ast_manager & m, params_ref const & p = params_ref()); +/* + ADD_TACTIC("qfidl", "builtin strategy for solving QF_IDL problems.", "mk_qfidl_tactic(m, p)") +*/ + #endif diff --git a/src/tactic/smtlogics/qfuf_tactic.h b/src/tactic/smtlogics/qfuf_tactic.h index 732e1289f..0c81ad57b 100644 --- a/src/tactic/smtlogics/qfuf_tactic.h +++ b/src/tactic/smtlogics/qfuf_tactic.h @@ -26,4 +26,8 @@ class tactic; tactic * mk_qfuf_tactic(ast_manager & m, params_ref const & p); +/* + ADD_TACTIC("qfuf", "builtin strategy for solving QF_UF problems.", "mk_qfuf_tactic(m, p)") +*/ + #endif diff --git a/src/tactic/smtlogics/qfufbv_tactic.h b/src/tactic/smtlogics/qfufbv_tactic.h index e9ffe4dc3..ceb125517 100644 --- a/src/tactic/smtlogics/qfufbv_tactic.h +++ b/src/tactic/smtlogics/qfufbv_tactic.h @@ -7,7 +7,7 @@ Module Name: Abstract: - Tactic for QF_UFBV + Tactic for QF_UFBV Author: @@ -25,4 +25,8 @@ class tactic; tactic * mk_qfufbv_tactic(ast_manager & m, params_ref const & p = params_ref()); +/* + ADD_TACTIC("qfufbv", "builtin strategy for solving QF_UFBV problems.", "mk_qfufbv_tactic(m, p)") +*/ + #endif From d4242e16c5dfc74b66b0a0adcd1a24f2ef11315b Mon Sep 17 00:00:00 2001 From: Patrick Totzke Date: Thu, 5 Nov 2015 16:28:02 +0000 Subject: [PATCH 4/6] add __hash__ to AstRef AstRef objects needs to be hashable in order to be used as keys in python dictionaries --- src/api/python/z3.py | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/api/python/z3.py b/src/api/python/z3.py index 5763db916..84fd7b111 100644 --- a/src/api/python/z3.py +++ b/src/api/python/z3.py @@ -284,6 +284,9 @@ class AstRef(Z3PPObject): def __repr__(self): return obj_to_string(self) + def __hash__(self): + return self.hash() + def sexpr(self): """Return an string representing the AST node in s-expression notation. From c2aee86e4ea95edf268a57d8892c5ea4f5aa306f Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 6 Nov 2015 16:24:44 +0000 Subject: [PATCH 5/6] Added new SMT logic names --- src/cmd_context/cmd_context.cpp | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index 7ed93ab37..b018d62c5 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -507,6 +507,8 @@ bool cmd_context::logic_has_arith_core(symbol const & s) const { s == "QF_AUFLIRA" || s == "QF_AUFNIA" || s == "QF_AUFNIRA" || + s == "QF_ANIA" || + s == "QF_LIRA" || s == "QF_UFLIA" || s == "QF_UFLRA" || s == "QF_UFIDL" || @@ -518,6 +520,7 @@ bool cmd_context::logic_has_arith_core(symbol const & s) const { s == "QF_UFNIA" || s == "QF_UFNIRA" || s == "QF_BVRE" || + s == "ALIA" || s == "AUFLIA" || s == "AUFLIRA" || s == "AUFNIA" || @@ -526,9 +529,12 @@ bool cmd_context::logic_has_arith_core(symbol const & s) const { s == "UFLRA" || s == "UFNRA" || s == "UFNIRA" || + s == "NIA" || + s == "NRA" || s == "UFNIA" || s == "LIA" || s == "LRA" || + s == "UFIDL" || s == "QF_FP" || s == "QF_FPBV" || s == "QF_BVFP" || @@ -583,10 +589,12 @@ bool cmd_context::logic_has_array_core(symbol const & s) const { return s == "QF_AX" || s == "QF_AUFLIA" || + s == "QF_ANIA" || s == "QF_ALIA" || s == "QF_AUFLIRA" || s == "QF_AUFNIA" || s == "QF_AUFNIRA" || + s == "ALIA" || s == "AUFLIA" || s == "AUFLIRA" || s == "AUFNIA" || From a6b3fba03819655a1288ac5e0ef15b111f00d650 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 6 Nov 2015 18:06:23 +0000 Subject: [PATCH 6/6] Build fix, hide debug code in release mode. --- src/smt/smt_context_pp.cpp | 68 +++++++++++++++++++------------------- 1 file changed, 34 insertions(+), 34 deletions(-) diff --git a/src/smt/smt_context_pp.cpp b/src/smt/smt_context_pp.cpp index 8eebe0531..fc837157f 100644 --- a/src/smt/smt_context_pp.cpp +++ b/src/smt/smt_context_pp.cpp @@ -27,19 +27,19 @@ namespace smt { std::ostream& context::display_last_failure(std::ostream& out) const { switch(m_last_search_failure) { - case OK: + case OK: return out << "OK"; - case UNKNOWN: + case UNKNOWN: return out << "UNKNOWN"; case TIMEOUT: return out << "TIMEOUT"; - case MEMOUT: + case MEMOUT: return out << "MEMOUT"; - case CANCELED: + case CANCELED: return out << "CANCELED"; - case NUM_CONFLICTS: + case NUM_CONFLICTS: return out << "NUM_CONFLICTS"; - case THEORY: + case THEORY: if (!m_incomplete_theories.empty()) { ptr_vector::const_iterator it = m_incomplete_theories.begin(); ptr_vector::const_iterator end = m_incomplete_theories.end(); @@ -52,7 +52,7 @@ namespace smt { out << "THEORY"; } return out; - case QUANTIFIERS: + case QUANTIFIERS: return out << "QUANTIFIERS"; } UNREACHABLE(); @@ -78,18 +78,18 @@ namespace smt { r += "))"; break; } - case QUANTIFIERS: r = "(incomplete quantifiers)"; break; + case QUANTIFIERS: r = "(incomplete quantifiers)"; break; case UNKNOWN: r = "incomplete"; break; } return r; } - + void context::display_asserted_formulas(std::ostream & out) const { m_asserted_formulas.display_ll(out, get_pp_visited()); } void context::display_literal(std::ostream & out, literal l) const { - l.display_compact(out, m_bool_var2expr.c_ptr()); + l.display_compact(out, m_bool_var2expr.c_ptr()); } void context::display_literals(std::ostream & out, unsigned num_lits, literal const * lits) const { @@ -151,16 +151,16 @@ namespace smt { for (unsigned i = 0; i < num_lits; i++) { literal l = cls->get_literal(i); display_literal(out, l); - out << ", val: " << get_assignment(l) << ", lvl: " << get_assign_level(l) - << ", ilvl: " << get_intern_level(l.var()) << ", var: " << l.var() << "\n" + out << ", val: " << get_assignment(l) << ", lvl: " << get_assign_level(l) + << ", ilvl: " << get_intern_level(l.var()) << ", var: " << l.var() << "\n" << mk_pp(bool_var2expr(l.var()), m_manager) << "\n\n"; } } - + void context::display_clause(std::ostream & out, clause const * cls) const { cls->display_compact(out, m_manager, m_bool_var2expr.c_ptr()); } - + void context::display_clauses(std::ostream & out, ptr_vector const & v) const { ptr_vector::const_iterator it = v.begin(); ptr_vector::const_iterator end = v.end(); @@ -201,11 +201,11 @@ namespace smt { if (!m_assigned_literals.empty()) { out << "current assignment:\n"; literal_vector::const_iterator it = m_assigned_literals.begin(); - literal_vector::const_iterator end = m_assigned_literals.end(); + literal_vector::const_iterator end = m_assigned_literals.end(); for (; it != end; ++it) { display_literal(out, *it); out << ": "; - display_verbose(tout, m_manager, 1, &*it, m_bool_var2expr.c_ptr()); + DEBUG_CODE({ display_verbose(tout, m_manager, 1, &*it, m_bool_var2expr.c_ptr()); }); out << "\n"; } } @@ -217,7 +217,7 @@ namespace smt { pp.set_status("unknown"); pp.set_logic(logic); literal_vector::const_iterator it = m_assigned_literals.begin(); - literal_vector::const_iterator end = m_assigned_literals.end(); + literal_vector::const_iterator end = m_assigned_literals.end(); for (; it != end; ++it) { expr_ref n(m_manager); literal2expr(*it, n); @@ -302,7 +302,7 @@ namespace smt { th->display(out); } } - + void context::display(std::ostream & out) const { get_pp_visited().reset(); out << "Logical context:\n"; @@ -337,16 +337,16 @@ namespace smt { void context::display_eq_detail(std::ostream & out, enode * n) const { SASSERT(n->is_eq()); - out << "#" << n->get_owner_id() - << ", root: #" << n->get_root()->get_owner_id() + out << "#" << n->get_owner_id() + << ", root: #" << n->get_root()->get_owner_id() << ", cg: #" << n->m_cg->get_owner_id() - << ", val: " << get_assignment(enode2bool_var(n)) - << ", lhs: #" << n->get_arg(0)->get_owner_id() - << ", rhs: #" << n->get_arg(1)->get_owner_id() - << ", lhs->root: #" << n->get_arg(0)->get_root()->get_owner_id() - << ", rhs->root: #" << n->get_arg(1)->get_root()->get_owner_id() + << ", val: " << get_assignment(enode2bool_var(n)) + << ", lhs: #" << n->get_arg(0)->get_owner_id() + << ", rhs: #" << n->get_arg(1)->get_owner_id() + << ", lhs->root: #" << n->get_arg(0)->get_root()->get_owner_id() + << ", rhs->root: #" << n->get_arg(1)->get_root()->get_owner_id() << ", is_marked: " << n->is_marked() - << ", is_relevant: " << is_relevant(n) + << ", is_relevant: " << is_relevant(n) << ", iscope_lvl: " << n->get_iscope_lvl() << "\n"; } @@ -355,7 +355,7 @@ namespace smt { enode_vector::iterator end = n->end_parents(); for (; it != end; ++it) { enode * parent = *it; - if (parent->is_eq()) + if (parent->is_eq()) display_eq_detail(out, parent); } } @@ -448,7 +448,7 @@ namespace smt { g_lemma_id++; } - void context::display_lemma_as_smt_problem(std::ostream & out, unsigned num_antecedents, literal const * antecedents, + void context::display_lemma_as_smt_problem(std::ostream & out, unsigned num_antecedents, literal const * antecedents, unsigned num_eq_antecedents, enode_pair const * eq_antecedents, literal consequent, const char * logic) const { ast_smt_pp pp(m_manager); @@ -472,7 +472,7 @@ namespace smt { pp.display_smt2(out, n); } - void context::display_lemma_as_smt_problem(unsigned num_antecedents, literal const * antecedents, + void context::display_lemma_as_smt_problem(unsigned num_antecedents, literal const * antecedents, unsigned num_eq_antecedents, enode_pair const * eq_antecedents, literal consequent, const char * logic) const { char buffer[BUFFER_SZ]; @@ -534,7 +534,7 @@ namespace smt { n->display_lbls(out); } } - + void context::display_decl2enodes(std::ostream & out) const { out << "decl2enodes:\n"; vector::const_iterator it1 = m_decl2enodes.begin(); @@ -545,7 +545,7 @@ namespace smt { out << "id " << id << " ->"; enode_vector::const_iterator it2 = v.begin(); enode_vector::const_iterator end2 = v.end(); - for (; it2 != end2; ++it2) + for (; it2 != end2; ++it2) out << " #" << (*it2)->get_owner_id(); out << "\n"; } @@ -568,7 +568,7 @@ namespace smt { out << std::right; if (lit_internalized(n)) out << get_assignment(n); - else + else out << "l_undef"; } if (e_internalized(n)) { @@ -577,12 +577,12 @@ namespace smt { } out << "\n"; if (is_app(n)) { - for (unsigned i = 0; i < to_app(n)->get_num_args(); i++) + for (unsigned i = 0; i < to_app(n)->get_num_args(); i++) todo.push_back(to_app(n)->get_arg(i)); } } } - + void context::display(std::ostream& out, b_justification j) const { switch (j.get_kind()) { case b_justification::AXIOM: