From b3ebcfe55855589d3b2fb4dbeda1310a64a23862 Mon Sep 17 00:00:00 2001 From: Murphy Berzish Date: Wed, 29 Nov 2017 18:20:59 -0500 Subject: [PATCH 01/19] correctly check third argument of str.indexof in theory_str --- src/smt/theory_str.cpp | 47 ++++++++++++++++++++++-------------------- src/smt/theory_str.h | 2 +- 2 files changed, 26 insertions(+), 23 deletions(-) diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index 7936b581c..a931ae458 100644 --- a/src/smt/theory_str.cpp +++ b/src/smt/theory_str.cpp @@ -641,7 +641,6 @@ namespace smt { } app * theory_str::mk_indexof(expr * haystack, expr * needle) { - // TODO check meaning of the third argument here app * indexof = u.str.mk_index(haystack, needle, mk_int(0)); m_trail.push_back(indexof); // immediately force internalization so that axiom setup does not fail @@ -844,14 +843,7 @@ namespace smt { instantiate_axiom_Contains(e); } else if (u.str.is_index(a)) { instantiate_axiom_Indexof(e); - /* TODO NEXT: Indexof2/Lastindexof rewrite? - } else if (is_Indexof2(e)) { - instantiate_axiom_Indexof2(e); - } else if (is_LastIndexof(e)) { - instantiate_axiom_LastIndexof(e); - */ } else if (u.str.is_extract(a)) { - // TODO check semantics of substr vs. extract instantiate_axiom_Substr(e); } else if (u.str.is_replace(a)) { instantiate_axiom_Replace(e); @@ -1232,27 +1224,37 @@ namespace smt { context & ctx = get_context(); ast_manager & m = get_manager(); - app * expr = e->get_owner(); - if (axiomatized_terms.contains(expr)) { - TRACE("str", tout << "already set up Indexof axiom for " << mk_pp(expr, m) << std::endl;); + app * ex = e->get_owner(); + if (axiomatized_terms.contains(ex)) { + TRACE("str", tout << "already set up str.indexof axiom for " << mk_pp(ex, m) << std::endl;); return; } - axiomatized_terms.insert(expr); + SASSERT(ex->get_num_args() == 3); + // if the third argument is exactly the integer 0, we can use this "simple" indexof; + // otherwise, we call the "extended" version + expr * startingPosition = ex->get_arg(2); + rational startingInteger; + if (!m_autil.is_numeral(startingPosition, startingInteger) || !startingInteger.is_zero()) { + // "extended" indexof term with prefix + instantiate_axiom_Indexof_extended(e); + return; + } + axiomatized_terms.insert(ex); - TRACE("str", tout << "instantiate Indexof axiom for " << mk_pp(expr, m) << std::endl;); + TRACE("str", tout << "instantiate str.indexof axiom for " << mk_pp(ex, m) << std::endl;); expr_ref x1(mk_str_var("x1"), m); expr_ref x2(mk_str_var("x2"), m); expr_ref indexAst(mk_int_var("index"), m); - expr_ref condAst(mk_contains(expr->get_arg(0), expr->get_arg(1)), m); + expr_ref condAst(mk_contains(ex->get_arg(0), ex->get_arg(1)), m); SASSERT(condAst); // ----------------------- // true branch expr_ref_vector thenItems(m); // args[0] = x1 . args[1] . x2 - thenItems.push_back(ctx.mk_eq_atom(expr->get_arg(0), mk_concat(x1, mk_concat(expr->get_arg(1), x2)))); + thenItems.push_back(ctx.mk_eq_atom(ex->get_arg(0), mk_concat(x1, mk_concat(ex->get_arg(1), x2)))); // indexAst = |x1| thenItems.push_back(ctx.mk_eq_atom(indexAst, mk_strlen(x1))); // args[0] = x3 . x4 @@ -1260,11 +1262,11 @@ namespace smt { // /\ ! contains(x3, args[1]) expr_ref x3(mk_str_var("x3"), m); expr_ref x4(mk_str_var("x4"), m); - expr_ref tmpLen(m_autil.mk_add(indexAst, mk_strlen(expr->get_arg(1)), mk_int(-1)), m); + expr_ref tmpLen(m_autil.mk_add(indexAst, mk_strlen(ex->get_arg(1)), mk_int(-1)), m); SASSERT(tmpLen); - thenItems.push_back(ctx.mk_eq_atom(expr->get_arg(0), mk_concat(x3, x4))); + thenItems.push_back(ctx.mk_eq_atom(ex->get_arg(0), mk_concat(x3, x4))); thenItems.push_back(ctx.mk_eq_atom(mk_strlen(x3), tmpLen)); - thenItems.push_back(mk_not(m, mk_contains(x3, expr->get_arg(1)))); + thenItems.push_back(mk_not(m, mk_contains(x3, ex->get_arg(1)))); expr_ref thenBranch(m.mk_and(thenItems.size(), thenItems.c_ptr()), m); SASSERT(thenBranch); @@ -1276,7 +1278,7 @@ namespace smt { expr_ref breakdownAssert(m.mk_ite(condAst, thenBranch, elseBranch), m); SASSERT(breakdownAssert); - expr_ref reduceToIndex(ctx.mk_eq_atom(expr, indexAst), m); + expr_ref reduceToIndex(ctx.mk_eq_atom(ex, indexAst), m); SASSERT(reduceToIndex); expr_ref finalAxiom(m.mk_and(breakdownAssert, reduceToIndex), m); @@ -1284,18 +1286,19 @@ namespace smt { assert_axiom(finalAxiom); } - void theory_str::instantiate_axiom_Indexof2(enode * e) { + void theory_str::instantiate_axiom_Indexof_extended(enode * e) { context & ctx = get_context(); ast_manager & m = get_manager(); app * expr = e->get_owner(); if (axiomatized_terms.contains(expr)) { - TRACE("str", tout << "already set up Indexof2 axiom for " << mk_pp(expr, m) << std::endl;); + TRACE("str", tout << "already set up extended str.indexof axiom for " << mk_pp(expr, m) << std::endl;); return; } + SASSERT(expr->get_num_args() == 3); axiomatized_terms.insert(expr); - TRACE("str", tout << "instantiate Indexof2 axiom for " << mk_pp(expr, m) << std::endl;); + TRACE("str", tout << "instantiate extended str.indexof axiom for " << mk_pp(expr, m) << std::endl;); // ------------------------------------------------------------------------------- // if (arg[2] >= length(arg[0])) // ite2 diff --git a/src/smt/theory_str.h b/src/smt/theory_str.h index 03fd31162..dd2ca585b 100644 --- a/src/smt/theory_str.h +++ b/src/smt/theory_str.h @@ -447,7 +447,7 @@ protected: void instantiate_axiom_suffixof(enode * e); void instantiate_axiom_Contains(enode * e); void instantiate_axiom_Indexof(enode * e); - void instantiate_axiom_Indexof2(enode * e); + void instantiate_axiom_Indexof_extended(enode * e); void instantiate_axiom_LastIndexof(enode * e); void instantiate_axiom_Substr(enode * e); void instantiate_axiom_Replace(enode * e); From 9554723b44860733e8a633de724aa06bb9ed9a99 Mon Sep 17 00:00:00 2001 From: Murphy Berzish Date: Wed, 6 Dec 2017 20:50:03 -0500 Subject: [PATCH 02/19] use safer mk_and in extended indexof --- src/smt/theory_str.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index a931ae458..4f84ed2f7 100644 --- a/src/smt/theory_str.cpp +++ b/src/smt/theory_str.cpp @@ -1330,7 +1330,7 @@ namespace smt { ite2ElseItems.push_back(ctx.mk_eq_atom(indexAst, mk_indexof(suffix, expr->get_arg(1)))); ite2ElseItems.push_back(ctx.mk_eq_atom(expr->get_arg(2), prefixLen)); ite2ElseItems.push_back(ite3); - expr_ref ite2Else(m.mk_and(ite2ElseItems.size(), ite2ElseItems.c_ptr()), m); + expr_ref ite2Else(mk_and(ite2ElseItems), m); SASSERT(ite2Else); expr_ref ite2(m.mk_ite( From 4cc936285113df07f6492cf791f7850e933cda54 Mon Sep 17 00:00:00 2001 From: Bruce Mitchener Date: Wed, 7 Mar 2018 13:18:39 +0700 Subject: [PATCH 03/19] Make proof_checker more const correct. --- src/ast/proofs/proof_checker.cpp | 52 ++++++++++++++++---------------- src/ast/proofs/proof_checker.h | 50 +++++++++++++++--------------- 2 files changed, 51 insertions(+), 51 deletions(-) diff --git a/src/ast/proofs/proof_checker.cpp b/src/ast/proofs/proof_checker.cpp index 9ba52a402..bd50e6c2a 100644 --- a/src/ast/proofs/proof_checker.cpp +++ b/src/ast/proofs/proof_checker.cpp @@ -922,7 +922,7 @@ void proof_checker::set_false(expr_ref& e, unsigned position, expr_ref& lit) { } } -bool proof_checker::match_fact(proof* p, expr_ref& fact) { +bool proof_checker::match_fact(proof const* p, expr_ref& fact) const { if (m.is_proof(p) && m.has_fact(p)) { fact = m.get_fact(p); @@ -938,13 +938,13 @@ void proof_checker::add_premise(proof* p) { } } -bool proof_checker::match_proof(proof* p) { +bool proof_checker::match_proof(proof const* p) const { return m.is_proof(p) && m.get_num_parents(p) == 0; } -bool proof_checker::match_proof(proof* p, proof_ref& p0) { +bool proof_checker::match_proof(proof const* p, proof_ref& p0) const { if (m.is_proof(p) && m.get_num_parents(p) == 1) { p0 = m.get_parent(p, 0); @@ -953,7 +953,7 @@ bool proof_checker::match_proof(proof* p, proof_ref& p0) { return false; } -bool proof_checker::match_proof(proof* p, proof_ref& p0, proof_ref& p1) { +bool proof_checker::match_proof(proof const* p, proof_ref& p0, proof_ref& p1) const { if (m.is_proof(p) && m.get_num_parents(p) == 2) { p0 = m.get_parent(p, 0); @@ -963,7 +963,7 @@ bool proof_checker::match_proof(proof* p, proof_ref& p0, proof_ref& p1) { return false; } -bool proof_checker::match_proof(proof* p, proof_ref_vector& parents) { +bool proof_checker::match_proof(proof const* p, proof_ref_vector& parents) const { if (m.is_proof(p)) { for (unsigned i = 0; i < m.get_num_parents(p); ++i) { parents.push_back(m.get_parent(p, i)); @@ -974,7 +974,7 @@ bool proof_checker::match_proof(proof* p, proof_ref_vector& parents) { } -bool proof_checker::match_binary(expr* e, func_decl_ref& d, expr_ref& t1, expr_ref& t2) { +bool proof_checker::match_binary(expr const* e, func_decl_ref& d, expr_ref& t1, expr_ref& t2) const { if (e->get_kind() == AST_APP && to_app(e)->get_num_args() == 2) { d = to_app(e)->get_decl(); @@ -986,7 +986,7 @@ bool proof_checker::match_binary(expr* e, func_decl_ref& d, expr_ref& t1, expr_r } -bool proof_checker::match_app(expr* e, func_decl_ref& d, expr_ref_vector& terms) { +bool proof_checker::match_app(expr const* e, func_decl_ref& d, expr_ref_vector& terms) const { if (e->get_kind() == AST_APP) { d = to_app(e)->get_decl(); for (unsigned i = 0; i < to_app(e)->get_num_args(); ++i) { @@ -997,9 +997,9 @@ bool proof_checker::match_app(expr* e, func_decl_ref& d, expr_ref_vector& terms) return false; } -bool proof_checker::match_quantifier(expr* e, bool& is_univ, sort_ref_vector& sorts, expr_ref& body) { +bool proof_checker::match_quantifier(expr const* e, bool& is_univ, sort_ref_vector& sorts, expr_ref& body) const { if (is_quantifier(e)) { - quantifier* q = to_quantifier(e); + quantifier const* q = to_quantifier(e); is_univ = q->is_forall(); body = q->get_expr(); for (unsigned i = 0; i < q->get_num_decls(); ++i) { @@ -1010,7 +1010,7 @@ bool proof_checker::match_quantifier(expr* e, bool& is_univ, sort_ref_vector& so return false; } -bool proof_checker::match_op(expr* e, decl_kind k, expr_ref& t1, expr_ref& t2) { +bool proof_checker::match_op(expr const* e, decl_kind k, expr_ref& t1, expr_ref& t2) const { if (e->get_kind() == AST_APP && to_app(e)->get_family_id() == m.get_basic_family_id() && to_app(e)->get_decl_kind() == k && @@ -1022,7 +1022,7 @@ bool proof_checker::match_op(expr* e, decl_kind k, expr_ref& t1, expr_ref& t2) { return false; } -bool proof_checker::match_op(expr* e, decl_kind k, expr_ref_vector& terms) { +bool proof_checker::match_op(expr const* e, decl_kind k, expr_ref_vector& terms) const { if (e->get_kind() == AST_APP && to_app(e)->get_family_id() == m.get_basic_family_id() && to_app(e)->get_decl_kind() == k) { @@ -1035,7 +1035,7 @@ bool proof_checker::match_op(expr* e, decl_kind k, expr_ref_vector& terms) { } -bool proof_checker::match_op(expr* e, decl_kind k, expr_ref& t) { +bool proof_checker::match_op(expr const* e, decl_kind k, expr_ref& t) const { if (e->get_kind() == AST_APP && to_app(e)->get_family_id() == m.get_basic_family_id() && to_app(e)->get_decl_kind() == k && @@ -1046,39 +1046,39 @@ bool proof_checker::match_op(expr* e, decl_kind k, expr_ref& t) { return false; } -bool proof_checker::match_not(expr* e, expr_ref& t) { +bool proof_checker::match_not(expr const* e, expr_ref& t) const { return match_op(e, OP_NOT, t); } -bool proof_checker::match_or(expr* e, expr_ref_vector& terms) { +bool proof_checker::match_or(expr const* e, expr_ref_vector& terms) const { return match_op(e, OP_OR, terms); } -bool proof_checker::match_and(expr* e, expr_ref_vector& terms) { +bool proof_checker::match_and(expr const* e, expr_ref_vector& terms) const { return match_op(e, OP_AND, terms); } -bool proof_checker::match_iff(expr* e, expr_ref& t1, expr_ref& t2) { +bool proof_checker::match_iff(expr const* e, expr_ref& t1, expr_ref& t2) const { return match_op(e, OP_IFF, t1, t2); } -bool proof_checker::match_equiv(expr* e, expr_ref& t1, expr_ref& t2) { +bool proof_checker::match_equiv(expr const* e, expr_ref& t1, expr_ref& t2) const { return match_oeq(e, t1, t2) || match_eq(e, t1, t2); } -bool proof_checker::match_implies(expr* e, expr_ref& t1, expr_ref& t2) { +bool proof_checker::match_implies(expr const* e, expr_ref& t1, expr_ref& t2) const { return match_op(e, OP_IMPLIES, t1, t2); } -bool proof_checker::match_eq(expr* e, expr_ref& t1, expr_ref& t2) { +bool proof_checker::match_eq(expr const* e, expr_ref& t1, expr_ref& t2) const { return match_op(e, OP_EQ, t1, t2) || match_iff(e, t1, t2); } -bool proof_checker::match_oeq(expr* e, expr_ref& t1, expr_ref& t2) { +bool proof_checker::match_oeq(expr const* e, expr_ref& t1, expr_ref& t2) const { return match_op(e, OP_OEQ, t1, t2); } -bool proof_checker::match_negated(expr* a, expr* b) { +bool proof_checker::match_negated(expr const* a, expr* b) const { expr_ref t(m); return (match_not(a, t) && t.get() == b) || @@ -1186,14 +1186,14 @@ void proof_checker::get_hypotheses(proof* p, expr_ref_vector& ante) { } -bool proof_checker::match_nil(expr* e) const { +bool proof_checker::match_nil(expr const* e) const { return is_app(e) && to_app(e)->get_family_id() == m_hyp_fid && to_app(e)->get_decl_kind() == OP_NIL; } -bool proof_checker::match_cons(expr* e, expr_ref& a, expr_ref& b) const { +bool proof_checker::match_cons(expr const* e, expr_ref& a, expr_ref& b) const { if (is_app(e) && to_app(e)->get_family_id() == m_hyp_fid && to_app(e)->get_decl_kind() == OP_CONS) { @@ -1205,7 +1205,7 @@ bool proof_checker::match_cons(expr* e, expr_ref& a, expr_ref& b) const { } -bool proof_checker::match_atom(expr* e, expr_ref& a) const { +bool proof_checker::match_atom(expr const* e, expr_ref& a) const { if (is_app(e) && to_app(e)->get_family_id() == m_hyp_fid && to_app(e)->get_decl_kind() == OP_ATOM) { @@ -1227,7 +1227,7 @@ expr* proof_checker::mk_nil() { return m_nil.get(); } -bool proof_checker::is_hypothesis(proof* p) const { +bool proof_checker::is_hypothesis(proof const* p) const { return m.is_proof(p) && p->get_decl_kind() == PR_HYPOTHESIS; @@ -1253,7 +1253,7 @@ expr* proof_checker::mk_hyp(unsigned num_hyps, expr * const * hyps) { } } -void proof_checker::dump_proof(proof * pr) { +void proof_checker::dump_proof(proof const* pr) { if (!m_dump_lemmas) return; SASSERT(m.has_fact(pr)); diff --git a/src/ast/proofs/proof_checker.h b/src/ast/proofs/proof_checker.h index ccb815c61..ac0e31dbd 100644 --- a/src/ast/proofs/proof_checker.h +++ b/src/ast/proofs/proof_checker.h @@ -77,39 +77,39 @@ private: bool check1_spc(proof* p, expr_ref_vector& side_conditions); bool check_arith_proof(proof* p); bool check_arith_literal(bool is_pos, app* lit, rational const& coeff, expr_ref& sum, bool& is_strict); - bool match_fact(proof* p, expr_ref& fact); + bool match_fact(proof const* p, expr_ref& fact) const; void add_premise(proof* p); - bool match_proof(proof* p); - bool match_proof(proof* p, proof_ref& p0); - bool match_proof(proof* p, proof_ref& p0, proof_ref& p1); - bool match_proof(proof* p, proof_ref_vector& parents); - bool match_binary(expr* e, func_decl_ref& d, expr_ref& t1, expr_ref& t2); - bool match_op(expr* e, decl_kind k, expr_ref& t1, expr_ref& t2); - bool match_op(expr* e, decl_kind k, expr_ref& t); - bool match_op(expr* e, decl_kind k, expr_ref_vector& terms); - bool match_iff(expr* e, expr_ref& t1, expr_ref& t2); - bool match_implies(expr* e, expr_ref& t1, expr_ref& t2); - bool match_eq(expr* e, expr_ref& t1, expr_ref& t2); - bool match_oeq(expr* e, expr_ref& t1, expr_ref& t2); - bool match_not(expr* e, expr_ref& t); - bool match_or(expr* e, expr_ref_vector& terms); - bool match_and(expr* e, expr_ref_vector& terms); - bool match_app(expr* e, func_decl_ref& d, expr_ref_vector& terms); - bool match_quantifier(expr*, bool& is_univ, sort_ref_vector&, expr_ref& body); - bool match_negated(expr* a, expr* b); - bool match_equiv(expr* a, expr_ref& t1, expr_ref& t2); + bool match_proof(proof const* p) const; + bool match_proof(proof const* p, proof_ref& p0) const; + bool match_proof(proof const* p, proof_ref& p0, proof_ref& p1) const; + bool match_proof(proof const* p, proof_ref_vector& parents) const; + bool match_binary(expr const* e, func_decl_ref& d, expr_ref& t1, expr_ref& t2) const; + bool match_op(expr const* e, decl_kind k, expr_ref& t1, expr_ref& t2) const; + bool match_op(expr const* e, decl_kind k, expr_ref& t) const; + bool match_op(expr const* e, decl_kind k, expr_ref_vector& terms) const; + bool match_iff(expr const* e, expr_ref& t1, expr_ref& t2) const; + bool match_implies(expr const* e, expr_ref& t1, expr_ref& t2) const; + bool match_eq(expr const* e, expr_ref& t1, expr_ref& t2) const; + bool match_oeq(expr const* e, expr_ref& t1, expr_ref& t2) const; + bool match_not(expr const* e, expr_ref& t) const; + bool match_or(expr const* e, expr_ref_vector& terms) const; + bool match_and(expr const* e, expr_ref_vector& terms) const; + bool match_app(expr const* e, func_decl_ref& d, expr_ref_vector& terms) const; + bool match_quantifier(expr const*, bool& is_univ, sort_ref_vector&, expr_ref& body) const; + bool match_negated(expr const* a, expr* b) const; + bool match_equiv(expr const* a, expr_ref& t1, expr_ref& t2) const; void get_ors(expr* e, expr_ref_vector& ors); void get_hypotheses(proof* p, expr_ref_vector& ante); - bool match_nil(expr* e) const; - bool match_cons(expr* e, expr_ref& a, expr_ref& b) const; - bool match_atom(expr* e, expr_ref& a) const; + bool match_nil(expr const* e) const; + bool match_cons(expr const* e, expr_ref& a, expr_ref& b) const; + bool match_atom(expr const* e, expr_ref& a) const; expr* mk_nil(); expr* mk_cons(expr* a, expr* b); expr* mk_atom(expr* e); - bool is_hypothesis(proof* p) const; + bool is_hypothesis(proof const* p) const; expr* mk_hyp(unsigned num_hyps, expr * const * hyps); - void dump_proof(proof * pr); + void dump_proof(proof const* pr); void dump_proof(unsigned num_antecedents, expr * const * antecedents, expr * consequent); void set_false(expr_ref& e, unsigned idx, expr_ref& lit); From 0b54a915131526df59208def2fa097fd6fd1dbb1 Mon Sep 17 00:00:00 2001 From: Bruce Mitchener Date: Wed, 7 Mar 2018 13:29:13 +0700 Subject: [PATCH 04/19] Force color output with Ninja. --- CMakeLists.txt | 14 ++++++++++++++ 1 file changed, 14 insertions(+) diff --git a/CMakeLists.txt b/CMakeLists.txt index 69a0ca123..a222551ae 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -409,6 +409,20 @@ list(APPEND Z3_DEPENDENT_LIBS ${CMAKE_THREAD_LIBS_INIT}) ################################################################################ include(${CMAKE_SOURCE_DIR}/cmake/compiler_warnings.cmake) +################################################################################ +# If using Ninja, force color output for Clang and gcc. +################################################################################ +if (UNIX AND CMAKE_GENERATOR STREQUAL "Ninja") + if (CMAKE_CXX_COMPILER_ID STREQUAL "Clang") + set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -fcolor-diagnostics") + set(CMAKE_C_FLAGS "${CMAKE_C_FLAGS} -fcolor-diagnostics") + endif() + if (CMAKE_CXX_COMPILER_ID STREQUAL "GNU") + set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -fdiagnostics-color") + set(CMAKE_C_FLAGS "${CMAKE_C_FLAGS} -fdiagnostics-color") + endif() +endif() + ################################################################################ # Option to control what type of library we build ################################################################################ From 246941f2d30b9865229759e0d8707fc8c7de6763 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 7 Mar 2018 14:26:38 -0800 Subject: [PATCH 05/19] fix #1522 Signed-off-by: Nikolaj Bjorner --- src/ast/ast.cpp | 53 +++++++++++++++++++------------------ src/ast/ast_pp_util.cpp | 7 ++++- src/ast/ast_pp_util.h | 4 +++ src/muz/base/dl_context.cpp | 32 +++++++++++++--------- src/test/quant_elim.cpp | 2 ++ 5 files changed, 58 insertions(+), 40 deletions(-) diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp index c27651fca..127967374 100644 --- a/src/ast/ast.cpp +++ b/src/ast/ast.cpp @@ -1536,34 +1536,35 @@ void ast_manager::copy_families_plugins(ast_manager const & from) { // assigned in the order that they are created, this can result in differing // family ids. To avoid this, we first assign all family ids and only then inherit plugins. for (family_id fid = 0; from.m_family_manager.has_family(fid); fid++) { - symbol fid_name = from.get_family_name(fid); - if (!m_family_manager.has_family(fid)) { - family_id new_fid = mk_family_id(fid_name); - (void)new_fid; - TRACE("copy_families_plugins", tout << "new target fid created: " << new_fid << " fid_name: " << fid_name << "\n";); - } + symbol fid_name = from.get_family_name(fid); + if (!m_family_manager.has_family(fid)) { + family_id new_fid = mk_family_id(fid_name); + (void)new_fid; + TRACE("copy_families_plugins", tout << "new target fid created: " << new_fid << " fid_name: " << fid_name << "\n";); + } } for (family_id fid = 0; from.m_family_manager.has_family(fid); fid++) { - SASSERT(from.is_builtin_family_id(fid) == is_builtin_family_id(fid)); - SASSERT(!from.is_builtin_family_id(fid) || m_family_manager.has_family(fid)); - symbol fid_name = from.get_family_name(fid); - TRACE("copy_families_plugins", tout << "copying: " << fid_name << ", src fid: " << fid - << ", target has_family: " << m_family_manager.has_family(fid) << "\n"; - if (m_family_manager.has_family(fid)) tout << get_family_id(fid_name) << "\n";); - TRACE("copy_families_plugins", tout << "target fid: " << get_family_id(fid_name) << "\n";); - SASSERT(fid == get_family_id(fid_name)); - if (from.has_plugin(fid) && !has_plugin(fid)) { - decl_plugin * new_p = from.get_plugin(fid)->mk_fresh(); - register_plugin(fid, new_p); - SASSERT(new_p->get_family_id() == fid); - SASSERT(has_plugin(fid)); - } - if (from.has_plugin(fid)) { - get_plugin(fid)->inherit(from.get_plugin(fid), trans); - } - SASSERT(from.m_family_manager.has_family(fid) == m_family_manager.has_family(fid)); - SASSERT(from.get_family_id(fid_name) == get_family_id(fid_name)); - SASSERT(!from.has_plugin(fid) || has_plugin(fid)); + SASSERT(from.is_builtin_family_id(fid) == is_builtin_family_id(fid)); + SASSERT(!from.is_builtin_family_id(fid) || m_family_manager.has_family(fid)); + symbol fid_name = from.get_family_name(fid); + (void)fid_name; + TRACE("copy_families_plugins", tout << "copying: " << fid_name << ", src fid: " << fid + << ", target has_family: " << m_family_manager.has_family(fid) << "\n"; + if (m_family_manager.has_family(fid)) tout << get_family_id(fid_name) << "\n";); + TRACE("copy_families_plugins", tout << "target fid: " << get_family_id(fid_name) << "\n";); + SASSERT(fid == get_family_id(fid_name)); + if (from.has_plugin(fid) && !has_plugin(fid)) { + decl_plugin * new_p = from.get_plugin(fid)->mk_fresh(); + register_plugin(fid, new_p); + SASSERT(new_p->get_family_id() == fid); + SASSERT(has_plugin(fid)); + } + if (from.has_plugin(fid)) { + get_plugin(fid)->inherit(from.get_plugin(fid), trans); + } + SASSERT(from.m_family_manager.has_family(fid) == m_family_manager.has_family(fid)); + SASSERT(from.get_family_id(fid_name) == get_family_id(fid_name)); + SASSERT(!from.has_plugin(fid) || has_plugin(fid)); } } diff --git a/src/ast/ast_pp_util.cpp b/src/ast/ast_pp_util.cpp index 37785e072..23c9ebe51 100644 --- a/src/ast/ast_pp_util.cpp +++ b/src/ast/ast_pp_util.cpp @@ -46,13 +46,18 @@ void ast_pp_util::display_decls(std::ostream& out) { n = coll.get_num_decls(); for (unsigned i = 0; i < n; ++i) { func_decl* f = coll.get_func_decls()[i]; - if (f->get_family_id() == null_family_id) { + if (f->get_family_id() == null_family_id && !m_removed.contains(f)) { ast_smt2_pp(out, f, env); out << "\n"; } } } +void ast_pp_util::remove_decl(func_decl* f) { + m_removed.insert(f); +} + + void ast_pp_util::display_asserts(std::ostream& out, expr_ref_vector const& fmls, bool neat) { if (neat) { smt2_pp_environment_dbg env(m); diff --git a/src/ast/ast_pp_util.h b/src/ast/ast_pp_util.h index 964a862a2..1b2686511 100644 --- a/src/ast/ast_pp_util.h +++ b/src/ast/ast_pp_util.h @@ -20,9 +20,11 @@ Revision History: #define AST_PP_UTIL_H_ #include "ast/decl_collector.h" +#include "util/obj_hashtable.h" class ast_pp_util { ast_manager& m; + obj_hashtable m_removed; public: decl_collector coll; @@ -35,6 +37,8 @@ class ast_pp_util { void collect(expr_ref_vector const& es); + void remove_decl(func_decl* f); + void display_decls(std::ostream& out); void display_asserts(std::ostream& out, expr_ref_vector const& fmls, bool neat = true); diff --git a/src/muz/base/dl_context.cpp b/src/muz/base/dl_context.cpp index 47d7cc357..521cf0dc9 100644 --- a/src/muz/base/dl_context.cpp +++ b/src/muz/base/dl_context.cpp @@ -1106,6 +1106,16 @@ namespace datalog { names.push_back(m_rule_names[i]); } } + + static std::ostream& display_symbol(std::ostream& out, symbol const& nm) { + if (is_smt2_quoted_symbol(nm)) { + out << mk_smt2_quoted_symbol(nm); + } + else { + out << nm; + } + return out; + } void context::display_smt2(unsigned num_queries, expr* const* qs, std::ostream& out) { ast_manager& m = get_manager(); @@ -1148,13 +1158,13 @@ namespace datalog { if (!use_fixedpoint_extensions) { out << "(set-logic HORN)\n"; } + for (func_decl * f : rels) + visitor.remove_decl(f); visitor.display_decls(out); - func_decl_set::iterator it = rels.begin(), end = rels.end(); - for (; it != end; ++it) { - func_decl* f = *it; + + for (func_decl * f : rels) display_rel_decl(out, f); - } if (use_fixedpoint_extensions && do_declare_vars) { declare_vars(rules, fresh_names, out); @@ -1185,13 +1195,7 @@ namespace datalog { nm = symbol(s.str().c_str()); } fresh_names.add(nm); - if (is_smt2_quoted_symbol(nm)) { - out << mk_smt2_quoted_symbol(nm); - } - else { - out << nm; - } - out << ")"; + display_symbol(out, nm) << ")"; } out << ")\n"; } @@ -1219,7 +1223,8 @@ namespace datalog { PP(qfn); out << ")\n"; } - out << "(query " << fn->get_name() << ")\n"; + out << "(query "; + display_symbol(out, fn->get_name()) << ")\n"; } } else { @@ -1238,7 +1243,8 @@ namespace datalog { void context::display_rel_decl(std::ostream& out, func_decl* f) { smt2_pp_environment_dbg env(m); - out << "(declare-rel " << f->get_name() << " ("; + out << "(declare-rel "; + display_symbol(out, f->get_name()) << " ("; for (unsigned i = 0; i < f->get_arity(); ++i) { ast_smt2_pp(out, f->get_domain(i), env); if (i + 1 < f->get_arity()) { diff --git a/src/test/quant_elim.cpp b/src/test/quant_elim.cpp index 12fca706d..f376e2c1d 100644 --- a/src/test/quant_elim.cpp +++ b/src/test/quant_elim.cpp @@ -13,6 +13,7 @@ Copyright (c) 2015 Microsoft Corporation #include "ast/reg_decl_plugins.h" +#if 0 static void test_qe(ast_manager& m, lbool expected_outcome, expr* fml, char const* option) { // enable_trace("bit2int"); @@ -48,6 +49,7 @@ static void test_qe(ast_manager& m, lbool expected_outcome, expr* fml, char cons //exit(-1); } } +#endif static void test_formula(lbool expected_outcome, char const* fml) { ast_manager m; From a7caa2fd2a5b5d888956fcc0391ff034ce91b9b7 Mon Sep 17 00:00:00 2001 From: Murphy Berzish Date: Wed, 7 Mar 2018 18:16:11 -0500 Subject: [PATCH 06/19] remove useless get_assignments in theory_str final check --- src/smt/theory_str.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index b900f9368..e0f0909cc 100644 --- a/src/smt/theory_str.cpp +++ b/src/smt/theory_str.cpp @@ -8734,8 +8734,8 @@ namespace smt { context & ctx = get_context(); ast_manager & m = get_manager(); - expr_ref_vector assignments(m); - ctx.get_assignments(assignments); + //expr_ref_vector assignments(m); + //ctx.get_assignments(assignments); if (opt_VerifyFinalCheckProgress) { finalCheckProgressIndicator = false; From 02a969670124399e07c982b038cc861667e1b3ff Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 8 Mar 2018 11:19:00 -0500 Subject: [PATCH 07/19] fix #1521 Signed-off-by: Nikolaj Bjorner --- src/smt/theory_arith_core.h | 24 +++++++++++++++--------- 1 file changed, 15 insertions(+), 9 deletions(-) diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h index fe62efbf4..3393634b6 100644 --- a/src/smt/theory_arith_core.h +++ b/src/smt/theory_arith_core.h @@ -469,7 +469,8 @@ namespace smt { if (negated) l_conseq.neg(); TRACE("arith_axiom", tout << mk_pp(ante, m) << "\n" << mk_pp(conseq, m) << "\n"; - tout << s_ante << "\n" << s_conseq << "\n";); + tout << s_ante << "\n" << s_conseq << "\n"; + tout << l_ante << "\n" << l_conseq << "\n";); // literal lits[2] = {l_ante, l_conseq}; mk_clause(l_ante, l_conseq, 0, nullptr); @@ -589,13 +590,14 @@ namespace smt { } // - // create the term: s := to_real(to_int(x)) - x + // create the term: s := x - to_real(to_int(x)) // add the bounds 0 <= s < 1 // template void theory_arith::mk_to_int_axiom(app * n) { SASSERT(m_util.is_to_int(n)); - ast_manager & m = get_manager(); + ast_manager & m = get_manager(); + context & ctx = get_context(); expr* x = n->get_arg(0); // to_int (to_real x) = x @@ -603,11 +605,15 @@ namespace smt { mk_axiom(m.mk_false(), m.mk_eq(to_app(x)->get_arg(0), n)); return; } - expr* to_r = m_util.mk_to_real(n); - expr_ref lo(m_util.mk_le(to_r, x), m); - expr_ref hi(m_util.mk_lt(x, m_util.mk_add(to_r, m_util.mk_numeral(rational(1), false))), m); - mk_axiom(m.mk_false(), lo); - mk_axiom(m.mk_false(), hi); + expr_ref to_r(m_util.mk_to_real(n), m); + expr_ref diff(m_util.mk_add(x, m_util.mk_mul(m_util.mk_real(-1), to_r)), m); + + expr_ref lo(m_util.mk_ge(diff, m_util.mk_real(0)), m); + expr_ref hi(m_util.mk_ge(diff, m_util.mk_real(1)), m); + hi = m.mk_not(hi); + + mk_axiom(m.mk_false(), lo, false); + mk_axiom(m.mk_false(), hi, false); } template @@ -1202,7 +1208,7 @@ namespace smt { template bool theory_arith::internalize_atom(app * n, bool gate_ctx) { - TRACE("arith_internalize", tout << "internalising atom:\n" << mk_pp(n, this->get_manager()) << "\n";); + TRACE("arith_internalize", tout << "internalizing atom:\n" << mk_pp(n, this->get_manager()) << "\n";); context & ctx = get_context(); SASSERT(m_util.is_le(n) || m_util.is_ge(n) || m_util.is_is_int(n)); SASSERT(!ctx.b_internalized(n)); From bf6975122be10ec7d4e872a274bac525d33a03a9 Mon Sep 17 00:00:00 2001 From: Murphy Berzish Date: Thu, 8 Mar 2018 12:37:44 -0500 Subject: [PATCH 08/19] integrate contains and indexof in theory_str --- src/smt/theory_str.cpp | 29 +++++++++++++++++++++++++++++ 1 file changed, 29 insertions(+) diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index cb4a11c89..9dfd0475b 100644 --- a/src/smt/theory_str.cpp +++ b/src/smt/theory_str.cpp @@ -1284,6 +1284,21 @@ namespace smt { expr_ref finalAxiom(m.mk_and(breakdownAssert, reduceToIndex), m); SASSERT(finalAxiom); assert_axiom(finalAxiom); + + { + // heuristic: integrate with str.contains information + // (but don't introduce it if it isn't already in the instance) + expr_ref haystack(ex->get_arg(0), m), needle(ex->get_arg(1), m), startIdx(ex->get_arg(2), m); + expr_ref zeroAst(mk_int(0), m); + // (H contains N) <==> (H indexof N, i) >= 0 + expr_ref premise(u.str.mk_contains(haystack, needle), m); + ctx.internalize(premise, false); + expr_ref conclusion(m_autil.mk_ge(ex, zeroAst), m); + expr_ref containsAxiom(ctx.mk_eq_atom(premise, conclusion), m); + SASSERT(containsAxiom); + // we can't assert this during init_search as it breaks an invariant if the instance becomes inconsistent + m_delayed_axiom_setup_terms.push_back(containsAxiom); + } } void theory_str::instantiate_axiom_Indexof_extended(enode * e) { @@ -1353,6 +1368,20 @@ namespace smt { expr_ref reduceTerm(ctx.mk_eq_atom(expr, resAst), m); SASSERT(reduceTerm); assert_axiom(reduceTerm); + + { + // heuristic: integrate with str.contains information + // (but don't introduce it if it isn't already in the instance) + expr_ref haystack(expr->get_arg(0), m), needle(expr->get_arg(1), m), startIdx(expr->get_arg(2), m); + // (H contains N) <==> (H indexof N, i) >= 0 + expr_ref premise(u.str.mk_contains(haystack, needle), m); + ctx.internalize(premise, false); + expr_ref conclusion(m_autil.mk_ge(expr, zeroAst), m); + expr_ref containsAxiom(ctx.mk_eq_atom(premise, conclusion), m); + SASSERT(containsAxiom); + // we can't assert this during init_search as it breaks an invariant if the instance becomes inconsistent + m_delayed_axiom_setup_terms.push_back(containsAxiom); + } } void theory_str::instantiate_axiom_LastIndexof(enode * e) { From 878a6ca14ffd1eb9f1b26083ebb16533019cca2f Mon Sep 17 00:00:00 2001 From: Bruce Mitchener Date: Fri, 9 Mar 2018 14:29:22 +0700 Subject: [PATCH 09/19] Fix typos. --- CMakeLists.txt | 2 +- scripts/mk_consts_files.py | 2 +- src/api/c++/z3++.h | 2 +- src/api/dotnet/Context.cs | 10 +++++----- src/api/java/Context.java | 10 +++++----- src/api/python/z3/z3.py | 12 ++++++------ src/api/z3_fpa.h | 8 ++++---- src/api/z3_interp.h | 4 ++-- src/ast/rewriter/rewriter_def.h | 2 +- src/interp/iz3checker.cpp | 2 +- src/muz/base/fixedpoint_params.pyg | 8 ++++---- src/muz/transforms/dl_mk_array_instantiation.h | 2 +- src/muz/transforms/dl_mk_interp_tail_simplifier.h | 2 +- src/muz/transforms/dl_mk_rule_inliner.h | 2 +- src/muz/transforms/dl_mk_scale.h | 2 +- src/tactic/aig/aig.cpp | 2 +- src/tactic/tactic_exception.h | 2 +- src/tactic/tactical.h | 2 +- 18 files changed, 38 insertions(+), 38 deletions(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index 69a0ca123..7bc60e135 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -434,7 +434,7 @@ else() endif() ################################################################################ -# Postion independent code +# Position independent code ################################################################################ # This is required because code built in the components will end up in a shared # library. If not building a shared library ``-fPIC`` isn't needed and would add diff --git a/scripts/mk_consts_files.py b/scripts/mk_consts_files.py index d0502c19d..39d4e9439 100755 --- a/scripts/mk_consts_files.py +++ b/scripts/mk_consts_files.py @@ -72,7 +72,7 @@ def main(args): if count == 0: logging.info('No files generated. You need to specific an output directory' - ' for the relevant langauge bindings') + ' for the relevant language bindings') # TODO: Add support for other bindings return 0 diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index 49f6cfbf3..42467cb22 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -989,7 +989,7 @@ namespace z3 { /** \brief sequence and regular expression operations. - + is overloaeded as sequence concatenation and regular expression union. + + is overloaded as sequence concatenation and regular expression union. concat is overloaded to handle sequences and regular expressions */ expr extract(expr const& offset, expr const& length) const { diff --git a/src/api/dotnet/Context.cs b/src/api/dotnet/Context.cs index cbd6a1bac..b3b24a6d1 100644 --- a/src/api/dotnet/Context.cs +++ b/src/api/dotnet/Context.cs @@ -2515,7 +2515,7 @@ namespace Microsoft.Z3 /// - /// Concatentate sequences. + /// Concatenate sequences. /// public SeqExpr MkConcat(params SeqExpr[] t) { @@ -3597,7 +3597,7 @@ namespace Microsoft.Z3 } /// - /// Create a tactic that fails if the goal is not triviall satisfiable (i.e., empty) + /// Create a tactic that fails if the goal is not trivially satisfiable (i.e., empty) /// or trivially unsatisfiable (i.e., contains `false'). /// public Tactic FailIfNotDecided() @@ -4656,7 +4656,7 @@ namespace Microsoft.Z3 /// Conversion of a floating-point term into a bit-vector. /// /// - /// Produces a term that represents the conversion of the floating-poiunt term t into a + /// Produces a term that represents the conversion of the floating-point term t into a /// bit-vector term of size sz in 2's complement format (signed when signed==true). If necessary, /// the result will be rounded according to rounding mode rm. /// @@ -4677,7 +4677,7 @@ namespace Microsoft.Z3 /// Conversion of a floating-point term into a real-numbered term. /// /// - /// Produces a term that represents the conversion of the floating-poiunt term t into a + /// Produces a term that represents the conversion of the floating-point term t into a /// real number. Note that this type of conversion will often result in non-linear /// constraints over real terms. /// @@ -4696,7 +4696,7 @@ namespace Microsoft.Z3 /// /// The size of the resulting bit-vector is automatically determined. Note that /// IEEE 754-2008 allows multiple different representations of NaN. This conversion - /// knows only one NaN and it will always produce the same bit-vector represenatation of + /// knows only one NaN and it will always produce the same bit-vector representation of /// that NaN. /// /// FloatingPoint term. diff --git a/src/api/java/Context.java b/src/api/java/Context.java index ba96209b3..3c5caadee 100644 --- a/src/api/java/Context.java +++ b/src/api/java/Context.java @@ -1978,7 +1978,7 @@ public class Context implements AutoCloseable { } /** - * Concatentate sequences. + * Concatenate sequences. */ public SeqExpr mkConcat(SeqExpr... t) { @@ -2781,7 +2781,7 @@ public class Context implements AutoCloseable { } /** - * Create a tactic that fails if the goal is not triviall satisfiable (i.e., + * Create a tactic that fails if the goal is not trivially satisfiable (i.e., * empty) or trivially unsatisfiable (i.e., contains `false'). **/ public Tactic failIfNotDecided() @@ -3769,7 +3769,7 @@ public class Context implements AutoCloseable { * @param sz Size of the resulting bit-vector. * @param signed Indicates whether the result is a signed or unsigned bit-vector. * Remarks: - * Produces a term that represents the conversion of the floating-poiunt term t into a + * Produces a term that represents the conversion of the floating-point term t into a * bit-vector term of size sz in 2's complement format (signed when signed==true). If necessary, * the result will be rounded according to rounding mode rm. * @throws Z3Exception @@ -3786,7 +3786,7 @@ public class Context implements AutoCloseable { * Conversion of a floating-point term into a real-numbered term. * @param t FloatingPoint term * Remarks: - * Produces a term that represents the conversion of the floating-poiunt term t into a + * Produces a term that represents the conversion of the floating-point term t into a * real number. Note that this type of conversion will often result in non-linear * constraints over real terms. * @throws Z3Exception @@ -3802,7 +3802,7 @@ public class Context implements AutoCloseable { * Remarks: * The size of the resulting bit-vector is automatically determined. Note that * IEEE 754-2008 allows multiple different representations of NaN. This conversion - * knows only one NaN and it will always produce the same bit-vector represenatation of + * knows only one NaN and it will always produce the same bit-vector representation of * that NaN. * @throws Z3Exception **/ diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index 1cfb10179..e68d7280d 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -2428,7 +2428,7 @@ def is_rational_value(a): return is_arith(a) and a.is_real() and _is_numeral(a.ctx, a.as_ast()) def is_algebraic_value(a): - """Return `True` if `a` is an algerbraic value of sort Real. + """Return `True` if `a` is an algebraic value of sort Real. >>> is_algebraic_value(RealVal("3/5")) False @@ -4437,7 +4437,7 @@ class Datatype: """Declare constructor named `name` with the given accessors `args`. Each accessor is a pair `(name, sort)`, where `name` is a string and `sort` a Z3 sort or a reference to the datatypes being declared. - In the followin example `List.declare('cons', ('car', IntSort()), ('cdr', List))` + In the following example `List.declare('cons', ('car', IntSort()), ('cdr', List))` declares the constructor named `cons` that builds a new List using an integer and a List. It also declares the accessors `car` and `cdr`. The accessor `car` extracts the integer of a `cons` cell, and `cdr` the list of a `cons` cell. After all constructors were declared, we use the method create() to create @@ -4457,7 +4457,7 @@ class Datatype: return "Datatype(%s, %s)" % (self.name, self.constructors) def create(self): - """Create a Z3 datatype based on the constructors declared using the mehtod `declare()`. + """Create a Z3 datatype based on the constructors declared using the method `declare()`. The function `CreateDatatypes()` must be used to define mutually recursive datatypes. @@ -8874,7 +8874,7 @@ class FPNumRef(FPRef): def isSubnormal(self): return Z3_fpa_is_numeral_subnormal(self.ctx.ref(), self.as_ast()) - """Indicates whether the numeral is postitive.""" + """Indicates whether the numeral is positive.""" def isPositive(self): return Z3_fpa_is_numeral_positive(self.ctx.ref(), self.as_ast()) @@ -9670,7 +9670,7 @@ def fpToIEEEBV(x, ctx=None): The size of the resulting bit-vector is automatically determined. Note that IEEE 754-2008 allows multiple different representations of NaN. This conversion - knows only one NaN and it will always produce the same bit-vector represenatation of + knows only one NaN and it will always produce the same bit-vector representation of that NaN. >>> x = FP('x', FPSort(8, 24)) @@ -9845,7 +9845,7 @@ def Empty(s): raise Z3Exception("Non-sequence, non-regular expression sort passed to Empty") def Full(s): - """Create the regular expression that accepts the universal langauge + """Create the regular expression that accepts the universal language >>> e = Full(ReSort(SeqSort(IntSort()))) >>> print(e) re.all diff --git a/src/api/z3_fpa.h b/src/api/z3_fpa.h index 358a3c619..7d237c6e7 100644 --- a/src/api/z3_fpa.h +++ b/src/api/z3_fpa.h @@ -756,7 +756,7 @@ extern "C" { /** \brief Conversion of a floating-point term into an unsigned bit-vector. - Produces a term that represents the conversion of the floating-poiunt term t into a + Produces a term that represents the conversion of the floating-point term t into a bit-vector term of size sz in unsigned 2's complement format. If necessary, the result will be rounded according to rounding mode rm. @@ -772,7 +772,7 @@ extern "C" { /** \brief Conversion of a floating-point term into a signed bit-vector. - Produces a term that represents the conversion of the floating-poiunt term t into a + Produces a term that represents the conversion of the floating-point term t into a bit-vector term of size sz in signed 2's complement format. If necessary, the result will be rounded according to rounding mode rm. @@ -788,7 +788,7 @@ extern "C" { /** \brief Conversion of a floating-point term into a real-numbered term. - Produces a term that represents the conversion of the floating-poiunt term t into a + Produces a term that represents the conversion of the floating-point term t into a real number. Note that this type of conversion will often result in non-linear constraints over real terms. @@ -1011,7 +1011,7 @@ extern "C" { determined. Note that IEEE 754-2008 allows multiple different representations of NaN. This conversion - knows only one NaN and it will always produce the same bit-vector represenatation of + knows only one NaN and it will always produce the same bit-vector representation of that NaN. def_API('Z3_mk_fpa_to_ieee_bv', AST, (_in(CONTEXT),_in(AST))) diff --git a/src/api/z3_interp.h b/src/api/z3_interp.h index bcee0e22d..2441d4339 100644 --- a/src/api/z3_interp.h +++ b/src/api/z3_interp.h @@ -98,7 +98,7 @@ extern "C" { Interpolant may not necessarily be computable from all proofs. To be sure an interpolant can be computed, the proof - must be generated by an SMT solver for which interpoaltion is + must be generated by an SMT solver for which interpolation is supported, and the premises must be expressed using only theories and operators for which interpolation is supported. @@ -199,7 +199,7 @@ extern "C" { (implies (and c1 ... cn f) v) where c1 .. cn are the children of v (which must precede v in the file) - and f is the formula assiciated to node v. The last formula in the + and f is the formula associated to node v. The last formula in the file is the root vertex, and is represented by the predicate "false". A solution to a tree interpolation problem can be thought of as a diff --git a/src/ast/rewriter/rewriter_def.h b/src/ast/rewriter/rewriter_def.h index 658fb2e05..878f4ef4c 100644 --- a/src/ast/rewriter/rewriter_def.h +++ b/src/ast/rewriter/rewriter_def.h @@ -358,7 +358,7 @@ void rewriter_tpl::process_app(app * t, frame & fr) { if (ProofGen) { NOT_IMPLEMENTED_YET(); // We do not support the use of bindings in proof generation mode. - // Thus we have to apply the subsitution here, and + // Thus we have to apply the substitution here, and // beta_reducer subst(m()); // subst.set_bindings(new_num_args, new_args); // expr_ref r2(m()); diff --git a/src/interp/iz3checker.cpp b/src/interp/iz3checker.cpp index cfea511ad..511342819 100644 --- a/src/interp/iz3checker.cpp +++ b/src/interp/iz3checker.cpp @@ -43,7 +43,7 @@ struct iz3checker : iz3base { /* HACK: for tree interpolants, we assume that uninterpreted functions are global. This is because in the current state of the tree interpolation code, symbols that appear in sibling sub-trees have to be global, and - we have no way to eliminate such function symbols. When tree interpoaltion is + we have no way to eliminate such function symbols. When tree interpolation is fixed, we can tree function symbols the same as constant symbols. */ bool is_tree; diff --git a/src/muz/base/fixedpoint_params.pyg b/src/muz/base/fixedpoint_params.pyg index 0c2f03460..753a45e06 100644 --- a/src/muz/base/fixedpoint_params.pyg +++ b/src/muz/base/fixedpoint_params.pyg @@ -33,7 +33,7 @@ def_module_params('fixedpoint', "updated relation was modified or not"), ('datalog.compile_with_widening', BOOL, False, "widening will be used to compile recursive rules"), - ('datalog.default_table_checked', BOOL, False, "if true, the detault " + + ('datalog.default_table_checked', BOOL, False, "if true, the default " + 'table will be default_table inside a wrapper that checks that its results ' + 'are the same as of default_table_checker table'), ('datalog.default_table_checker', SYMBOL, 'null', "see default_table_checked"), @@ -59,7 +59,7 @@ def_module_params('fixedpoint', ('duality.full_expand', BOOL, False, 'Fully expand derivation trees'), ('duality.no_conj', BOOL, False, 'No forced covering (conjectures)'), ('duality.feasible_edges', BOOL, True, - 'Don\'t expand definitley infeasible edges'), + 'Don\'t expand definitely infeasible edges'), ('duality.use_underapprox', BOOL, False, 'Use underapproximations'), ('duality.stratified_inlining', BOOL, False, 'Use stratified inlining'), ('duality.recursion_bound', UINT, UINT_MAX, @@ -130,7 +130,7 @@ def_module_params('fixedpoint', ('xform.magic', BOOL, False, "perform symbolic magic set transformation"), ('xform.scale', BOOL, False, - "add scaling variable to linear real arithemtic clauses"), + "add scaling variable to linear real arithmetic clauses"), ('xform.inline_linear', BOOL, True, "try linear inlining method"), ('xform.inline_eager', BOOL, True, "try eager inlining of rules"), ('xform.inline_linear_branch', BOOL, False, @@ -176,7 +176,7 @@ def_module_params('fixedpoint', ('spacer.elim_aux', BOOL, True, "Eliminate auxiliary variables in reachability facts"), ('spacer.reach_as_init', BOOL, True, "Extend initial rules with computed reachability facts"), ('spacer.blast_term_ite', BOOL, True, "Expand non-Boolean ite-terms"), - ('spacer.nondet_tie_break', BOOL, False, "Break ties in obligation queue non-deterministicly"), + ('spacer.nondet_tie_break', BOOL, False, "Break ties in obligation queue non-deterministically"), ('spacer.reach_dnf', BOOL, True, "Restrict reachability facts to DNF"), ('bmc.linear_unrolling_depth', UINT, UINT_MAX, "Maximal level to explore"), ('spacer.split_farkas_literals', BOOL, False, "Split Farkas literals"), diff --git a/src/muz/transforms/dl_mk_array_instantiation.h b/src/muz/transforms/dl_mk_array_instantiation.h index cd5715a4f..b2e80ab84 100644 --- a/src/muz/transforms/dl_mk_array_instantiation.h +++ b/src/muz/transforms/dl_mk_array_instantiation.h @@ -26,7 +26,7 @@ Implementation: 1) Dealing with multiple quantifiers -> The options fixedpoint.xform.instantiate_arrays.nb_quantifier gives the number of quantifiers per array. - 2) Inforcing the instantiation -> We suggest an option (enforce_instantiation) to enforce this abstraction. This transforms + 2) Enforcing the instantiation -> We suggest an option (enforce_instantiation) to enforce this abstraction. This transforms P(a) into P(i, a[i]). This enforces the solver to limit the space search at the cost of imprecise results. This option corresponds to fixedpoint.xform.instantiate_arrays.enforce diff --git a/src/muz/transforms/dl_mk_interp_tail_simplifier.h b/src/muz/transforms/dl_mk_interp_tail_simplifier.h index 713827588..0d4c65d11 100644 --- a/src/muz/transforms/dl_mk_interp_tail_simplifier.h +++ b/src/muz/transforms/dl_mk_interp_tail_simplifier.h @@ -53,7 +53,7 @@ namespace datalog { */ void reset(rule * r); - /** Reset subtitution and unify tail tgt_idx of the target rule and the head of the src rule */ + /** Reset substitution and unify tail tgt_idx of the target rule and the head of the src rule */ bool unify(expr * e1, expr * e2); void get_result(rule_ref & res); diff --git a/src/muz/transforms/dl_mk_rule_inliner.h b/src/muz/transforms/dl_mk_rule_inliner.h index 27b6dd418..9146343fa 100644 --- a/src/muz/transforms/dl_mk_rule_inliner.h +++ b/src/muz/transforms/dl_mk_rule_inliner.h @@ -45,7 +45,7 @@ namespace datalog { : m(ctx.get_manager()), m_rm(ctx.get_rule_manager()), m_context(ctx), m_interp_simplifier(ctx), m_subst(m), m_unif(m), m_ready(false), m_normalize(true) {} - /** Reset subtitution and unify tail tgt_idx of the target rule and the head of the src rule */ + /** Reset substitution and unify tail tgt_idx of the target rule and the head of the src rule */ bool unify_rules(rule const& tgt, unsigned tgt_idx, rule const& src); /** diff --git a/src/muz/transforms/dl_mk_scale.h b/src/muz/transforms/dl_mk_scale.h index c171a1d06..94090ec93 100644 --- a/src/muz/transforms/dl_mk_scale.h +++ b/src/muz/transforms/dl_mk_scale.h @@ -7,7 +7,7 @@ Module Name: Abstract: - Add scale factor to linear (Real) arithemetic Horn clauses. + Add scale factor to linear (Real) arithmetic Horn clauses. The transformation replaces occurrences of isolated constants by a scale multiplied to each constant. diff --git a/src/tactic/aig/aig.cpp b/src/tactic/aig/aig.cpp index 40c68f72a..6afac32b8 100644 --- a/src/tactic/aig/aig.cpp +++ b/src/tactic/aig/aig.cpp @@ -267,7 +267,7 @@ struct aig_manager::imp { } if (b == r) { if (sign1) { - // subsitution + // substitution // not (a and b) and r --> (not a) and r IF b == r l = a; l.invert(); diff --git a/src/tactic/tactic_exception.h b/src/tactic/tactic_exception.h index 177524726..bdf2636a9 100644 --- a/src/tactic/tactic_exception.h +++ b/src/tactic/tactic_exception.h @@ -7,7 +7,7 @@ Module Name: Abstract: - Tactic expection object. + Tactic exception object. Author: diff --git a/src/tactic/tactical.h b/src/tactic/tactical.h index 169566f39..9ec2f901f 100644 --- a/src/tactic/tactical.h +++ b/src/tactic/tactical.h @@ -47,7 +47,7 @@ tactic * or_else(tactic * t1, tactic * t2, tactic * t3, tactic * t4, tactic * t5 tactic * repeat(tactic * t, unsigned max = UINT_MAX); /** - \brief Fails if \c t produeces more than \c threshold subgoals. + \brief Fails if \c t produces more than \c threshold subgoals. Otherwise, it behaves like \c t. */ tactic * fail_if_branching(tactic * t, unsigned threshold = 1); From ba603307fcb39cdc12a6d0283ddc9632ca436478 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 9 Mar 2018 05:32:01 -0500 Subject: [PATCH 10/19] remove stale deprecated annotation #1525 Signed-off-by: Nikolaj Bjorner --- src/api/z3_api.h | 5 ----- 1 file changed, 5 deletions(-) diff --git a/src/api/z3_api.h b/src/api/z3_api.h index 500533e91..f7c218963 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -1477,7 +1477,6 @@ extern "C" { /*@{*/ /** - \deprecated \brief Create a configuration object for the Z3 context object. Configurations are created in order to assign parameters prior to creating @@ -1510,7 +1509,6 @@ extern "C" { Z3_config Z3_API Z3_mk_config(void); /** - \deprecated \brief Delete the given configuration object. \sa Z3_mk_config @@ -1520,7 +1518,6 @@ extern "C" { void Z3_API Z3_del_config(Z3_config c); /** - \deprecated \brief Set a configuration parameter. The following parameters can be set for @@ -1537,7 +1534,6 @@ extern "C" { /*@{*/ /** - \deprecated \brief Create a context using the given configuration. After a context is created, the configuration cannot be changed, @@ -1617,7 +1613,6 @@ extern "C" { void Z3_API Z3_dec_ref(Z3_context c, Z3_ast a); /** - \deprecated \brief Set a value of a context parameter. \sa Z3_global_param_set From ae165a539e476a032f83ce252582f7b94b644e20 Mon Sep 17 00:00:00 2001 From: Pierre Pronchery Date: Fri, 9 Mar 2018 14:20:31 +0100 Subject: [PATCH 11/19] Fix parameter expansion when configuring Z3 --- configure | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/configure b/configure index 29408d3e7..807fba392 100755 --- a/configure +++ b/configure @@ -14,4 +14,4 @@ if ! $PYTHON -c "print('testing')" > /dev/null ; then exit 1 fi -$PYTHON scripts/mk_make.py $* +$PYTHON scripts/mk_make.py "$@" From e5a19816943fd1fdf3c93ff0ac7dfe1871fc1807 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 9 Mar 2018 15:40:35 -0500 Subject: [PATCH 12/19] disable GCC flag change to see if this affects build Signed-off-by: Nikolaj Bjorner --- CMakeLists.txt | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index f20c4fb10..62045016a 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -410,17 +410,17 @@ list(APPEND Z3_DEPENDENT_LIBS ${CMAKE_THREAD_LIBS_INIT}) include(${CMAKE_SOURCE_DIR}/cmake/compiler_warnings.cmake) ################################################################################ -# If using Ninja, force color output for Clang and gcc. +# If using Ninja, force color output for Clang (and gcc, disabled to check build). ################################################################################ if (UNIX AND CMAKE_GENERATOR STREQUAL "Ninja") if (CMAKE_CXX_COMPILER_ID STREQUAL "Clang") set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -fcolor-diagnostics") set(CMAKE_C_FLAGS "${CMAKE_C_FLAGS} -fcolor-diagnostics") endif() - if (CMAKE_CXX_COMPILER_ID STREQUAL "GNU") - set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -fdiagnostics-color") - set(CMAKE_C_FLAGS "${CMAKE_C_FLAGS} -fdiagnostics-color") - endif() +# if (CMAKE_CXX_COMPILER_ID STREQUAL "GNU") +# set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -fdiagnostics-color") +# set(CMAKE_C_FLAGS "${CMAKE_C_FLAGS} -fdiagnostics-color") +# endif() endif() ################################################################################ From 6e87622c8a770c497cafbf972dbd96eaa34eb67c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 10 Mar 2018 13:55:01 -0500 Subject: [PATCH 13/19] remove references to deprecated uses of PROOF_MODE #1531 Signed-off-by: Nikolaj Bjorner --- src/api/api_ast.cpp | 3 -- src/api/dotnet/Expr.cs | 38 +---------------- src/api/java/Expr.java | 55 ++----------------------- src/api/z3_api.h | 23 +---------- src/ast/ast.cpp | 31 -------------- src/ast/ast.h | 11 ++--- src/ast/proofs/proof_checker.cpp | 27 ------------ src/smt/theory_arith_core.h | 1 - src/smt/theory_str.cpp | 2 + src/tactic/core/ctx_simplify_tactic.cpp | 2 +- src/tactic/core/dom_simplify_tactic.cpp | 4 +- 11 files changed, 16 insertions(+), 181 deletions(-) diff --git a/src/api/api_ast.cpp b/src/api/api_ast.cpp index 3f5a0fcf1..1f4a86903 100644 --- a/src/api/api_ast.cpp +++ b/src/api/api_ast.cpp @@ -919,7 +919,6 @@ extern "C" { case PR_REWRITE: return Z3_OP_PR_REWRITE; case PR_REWRITE_STAR: return Z3_OP_PR_REWRITE_STAR; case PR_PULL_QUANT: return Z3_OP_PR_PULL_QUANT; - case PR_PULL_QUANT_STAR: return Z3_OP_PR_PULL_QUANT_STAR; case PR_PUSH_QUANT: return Z3_OP_PR_PUSH_QUANT; case PR_ELIM_UNUSED_VARS: return Z3_OP_PR_ELIM_UNUSED_VARS; case PR_DER: return Z3_OP_PR_DER; @@ -936,9 +935,7 @@ extern "C" { case PR_IFF_OEQ: return Z3_OP_PR_IFF_OEQ; case PR_NNF_POS: return Z3_OP_PR_NNF_POS; case PR_NNF_NEG: return Z3_OP_PR_NNF_NEG; - case PR_NNF_STAR: return Z3_OP_PR_NNF_STAR; case PR_SKOLEMIZE: return Z3_OP_PR_SKOLEMIZE; - case PR_CNF_STAR: return Z3_OP_PR_CNF_STAR; case PR_MODUS_PONENS_OEQ: return Z3_OP_PR_MODUS_PONENS_OEQ; case PR_TH_LEMMA: return Z3_OP_PR_TH_LEMMA; case PR_HYPER_RESOLVE: return Z3_OP_PR_HYPER_RESOLVE; diff --git a/src/api/dotnet/Expr.cs b/src/api/dotnet/Expr.cs index 0726f9d53..9310d1e7d 100644 --- a/src/api/dotnet/Expr.cs +++ b/src/api/dotnet/Expr.cs @@ -932,7 +932,7 @@ namespace Microsoft.Z3 /// Indicates whether the term is a proof by condensed transitivity of a relation /// /// - /// Condensed transitivity proof. This proof object is only used if the parameter PROOF_MODE is 1. + /// Condensed transitivity proof. /// It combines several symmetry and transitivity proofs. /// Example: /// T1: (R a b) @@ -1035,14 +1035,11 @@ namespace Microsoft.Z3 /// /// /// A proof for rewriting an expression t into an expression s. - /// This proof object is used if the parameter PROOF_MODE is 1. /// This proof object can have n antecedents. /// The antecedents are proofs for equalities used as substitution rules. - /// The object is also used in a few cases if the parameter PROOF_MODE is 2. - /// The cases are: + /// The object is used in a few cases: /// - When applying contextual simplification (CONTEXT_SIMPLIFIER=true) /// - When converting bit-vectors to Booleans (BIT2BOOL=true) - /// - When pulling ite expression up (PULL_CHEAP_ITE_TREES=true) /// public bool IsProofRewriteStar { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_REWRITE_STAR; } } @@ -1054,15 +1051,6 @@ namespace Microsoft.Z3 /// public bool IsProofPullQuant { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_PULL_QUANT; } } - /// - /// Indicates whether the term is a proof for pulling quantifiers out. - /// - /// - /// A proof for (iff P Q) where Q is in prenex normal form. - /// This proof object is only used if the parameter PROOF_MODE is 1. - /// This proof object has no antecedents - /// - public bool IsProofPullQuantStar { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_PULL_QUANT_STAR; } } /// /// Indicates whether the term is a proof for pushing quantifiers in. @@ -1304,28 +1292,6 @@ namespace Microsoft.Z3 /// public bool IsProofNNFNeg { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_NNF_NEG; } } - /// - /// Indicates whether the term is a proof for (~ P Q) here Q is in negation normal form. - /// - /// - /// A proof for (~ P Q) where Q is in negation normal form. - /// - /// This proof object is only used if the parameter PROOF_MODE is 1. - /// - /// This proof object may have n antecedents. Each antecedent is a PR_DEF_INTRO. - /// - public bool IsProofNNFStar { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_NNF_STAR; } } - - /// - /// Indicates whether the term is a proof for (~ P Q) where Q is in conjunctive normal form. - /// - /// - /// A proof for (~ P Q) where Q is in conjunctive normal form. - /// This proof object is only used if the parameter PROOF_MODE is 1. - /// This proof object may have n antecedents. Each antecedent is a PR_DEF_INTRO. - /// - public bool IsProofCNFStar { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_CNF_STAR; } } - /// /// Indicates whether the term is a proof for a Skolemization step /// diff --git a/src/api/java/Expr.java b/src/api/java/Expr.java index 7b20b7993..db5c33e79 100644 --- a/src/api/java/Expr.java +++ b/src/api/java/Expr.java @@ -1398,8 +1398,7 @@ public class Expr extends AST /** * Indicates whether the term is a proof by condensed transitivity of a * relation - * Remarks: Condensed transitivity proof. This proof object is - * only used if the parameter PROOF_MODE is 1. It combines several symmetry + * Remarks: Condensed transitivity proof. It combines several symmetry * and transitivity proofs. Example: T1: (R a b) T2: (R c b) T3: (R c d) * [trans* T1 T2 T3]: (R a d) R must be a symmetric and transitive relation. * @@ -1506,14 +1505,11 @@ public class Expr extends AST /** * Indicates whether the term is a proof by rewriting * Remarks: A proof for - * rewriting an expression t into an expression s. This proof object is used - * if the parameter PROOF_MODE is 1. This proof object can have n + * rewriting an expression t into an expression s. This proof object can have n * antecedents. The antecedents are proofs for equalities used as - * substitution rules. The object is also used in a few cases if the - * parameter PROOF_MODE is 2. The cases are: - When applying contextual + * substitution rules. The object is used in a few cases . The cases are: - When applying contextual * simplification (CONTEXT_SIMPLIFIER=true) - When converting bit-vectors to - * Booleans (BIT2BOOL=true) - When pulling ite expression up - * (PULL_CHEAP_ITE_TREES=true) + * Booleans (BIT2BOOL=true) * @throws Z3Exception on error * @return a boolean **/ @@ -1534,17 +1530,6 @@ public class Expr extends AST return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_PULL_QUANT; } - /** - * Indicates whether the term is a proof for pulling quantifiers out. - * - * Remarks: A proof for (iff P Q) where Q is in prenex normal form. This * proof object is only used if the parameter PROOF_MODE is 1. This proof * object has no antecedents - * @throws Z3Exception on error - * @return a boolean - **/ - public boolean isProofPullQuantStar() - { - return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_PULL_QUANT_STAR; - } /** * Indicates whether the term is a proof for pushing quantifiers in. @@ -1804,38 +1789,6 @@ public class Expr extends AST return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_NNF_NEG; } - /** - * Indicates whether the term is a proof for (~ P Q) here Q is in negation - * normal form. - * Remarks: A proof for (~ P Q) where Q is in negation normal - * form. - * - * This proof object is only used if the parameter PROOF_MODE is 1. - * - * This proof object may have n antecedents. Each antecedent is a - * PR_DEF_INTRO. - * @throws Z3Exception on error - * @return a boolean - **/ - public boolean isProofNNFStar() - { - return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_NNF_STAR; - } - - /** - * Indicates whether the term is a proof for (~ P Q) where Q is in - * conjunctive normal form. - * Remarks: A proof for (~ P Q) where Q is in - * conjunctive normal form. This proof object is only used if the parameter - * PROOF_MODE is 1. This proof object may have n antecedents. Each - * antecedent is a PR_DEF_INTRO. - * @throws Z3Exception on error - * @return a boolean - **/ - public boolean isProofCNFStar() - { - return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_CNF_STAR; - } /** * Indicates whether the term is a proof for a Skolemization step diff --git a/src/api/z3_api.h b/src/api/z3_api.h index f7c218963..88d6aa1cf 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -459,7 +459,7 @@ typedef enum [trans T1 T2]: (R t u) } - - Z3_OP_PR_TRANSITIVITY_STAR: Condensed transitivity proof. This proof object is only used if the parameter PROOF_MODE is 1. + - Z3_OP_PR_TRANSITIVITY_STAR: Condensed transitivity proof. It combines several symmetry and transitivity proofs. Example: @@ -539,21 +539,14 @@ typedef enum } - Z3_OP_PR_REWRITE_STAR: A proof for rewriting an expression t into an expression s. - This proof object is used if the parameter PROOF_MODE is 1. This proof object can have n antecedents. The antecedents are proofs for equalities used as substitution rules. - The object is also used in a few cases if the parameter PROOF_MODE is 2. - The cases are: + The proof rule is used in a few cases. The cases are: - When applying contextual simplification (CONTEXT_SIMPLIFIER=true) - When converting bit-vectors to Booleans (BIT2BOOL=true) - - When pulling ite expression up (PULL_CHEAP_ITE_TREES=true) - Z3_OP_PR_PULL_QUANT: A proof for (iff (f (forall (x) q(x)) r) (forall (x) (f (q x) r))). This proof object has no antecedents. - - Z3_OP_PR_PULL_QUANT_STAR: A proof for (iff P Q) where Q is in prenex normal form. - This proof object is only used if the parameter PROOF_MODE is 1. - This proof object has no antecedents. - - Z3_OP_PR_PUSH_QUANT: A proof for: \nicebox{ @@ -726,15 +719,6 @@ typedef enum [nnf-neg T1 T2 T3 T4]: (~ (not (iff s_1 s_2)) (and (or r_1 r_2) (or r_1' r_2'))) } - - Z3_OP_PR_NNF_STAR: A proof for (~ P Q) where Q is in negation normal form. - - This proof object is only used if the parameter PROOF_MODE is 1. - - This proof object may have n antecedents. Each antecedent is a PR_DEF_INTRO. - - - Z3_OP_PR_CNF_STAR: A proof for (~ P Q) where Q is in conjunctive normal form. - This proof object is only used if the parameter PROOF_MODE is 1. - This proof object may have n antecedents. Each antecedent is a PR_DEF_INTRO. - Z3_OP_PR_SKOLEMIZE: Proof for: @@ -1142,7 +1126,6 @@ typedef enum { Z3_OP_PR_REWRITE, Z3_OP_PR_REWRITE_STAR, Z3_OP_PR_PULL_QUANT, - Z3_OP_PR_PULL_QUANT_STAR, Z3_OP_PR_PUSH_QUANT, Z3_OP_PR_ELIM_UNUSED_VARS, Z3_OP_PR_DER, @@ -1159,8 +1142,6 @@ typedef enum { Z3_OP_PR_IFF_OEQ, Z3_OP_PR_NNF_POS, Z3_OP_PR_NNF_NEG, - Z3_OP_PR_NNF_STAR, - Z3_OP_PR_CNF_STAR, Z3_OP_PR_SKOLEMIZE, Z3_OP_PR_MODUS_PONENS_OEQ, Z3_OP_PR_TH_LEMMA, diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp index 127967374..7e143e1a3 100644 --- a/src/ast/ast.cpp +++ b/src/ast/ast.cpp @@ -663,7 +663,6 @@ basic_decl_plugin::basic_decl_plugin(): m_not_or_elim_decl(nullptr), m_rewrite_decl(nullptr), m_pull_quant_decl(nullptr), - m_pull_quant_star_decl(nullptr), m_push_quant_decl(nullptr), m_elim_unused_vars_decl(nullptr), m_der_decl(nullptr), @@ -827,7 +826,6 @@ func_decl * basic_decl_plugin::mk_proof_decl(basic_op_kind k, unsigned num_paren case PR_REWRITE: return mk_proof_decl("rewrite", k, 0, m_rewrite_decl); case PR_REWRITE_STAR: return mk_proof_decl("rewrite*", k, num_parents, m_rewrite_star_decls); case PR_PULL_QUANT: return mk_proof_decl("pull-quant", k, 0, m_pull_quant_decl); - case PR_PULL_QUANT_STAR: return mk_proof_decl("pull-quant*", k, 0, m_pull_quant_star_decl); case PR_PUSH_QUANT: return mk_proof_decl("push-quant", k, 0, m_push_quant_decl); case PR_ELIM_UNUSED_VARS: return mk_proof_decl("elim-unused", k, 0, m_elim_unused_vars_decl); case PR_DER: return mk_proof_decl("der", k, 0, m_der_decl); @@ -844,8 +842,6 @@ func_decl * basic_decl_plugin::mk_proof_decl(basic_op_kind k, unsigned num_paren case PR_IFF_OEQ: return mk_proof_decl("iff~", k, 1, m_iff_oeq_decl); case PR_NNF_POS: return mk_proof_decl("nnf-pos", k, num_parents, m_nnf_pos_decls); case PR_NNF_NEG: return mk_proof_decl("nnf-neg", k, num_parents, m_nnf_neg_decls); - case PR_NNF_STAR: return mk_proof_decl("nnf*", k, num_parents, m_nnf_star_decls); - case PR_CNF_STAR: return mk_proof_decl("cnf*", k, num_parents, m_cnf_star_decls); case PR_SKOLEMIZE: return mk_proof_decl("sk", k, 0, m_skolemize_decl); case PR_MODUS_PONENS_OEQ: return mk_proof_decl("mp~", k, 2, m_mp_oeq_decl); case PR_TH_LEMMA: return mk_proof_decl("th-lemma", k, num_parents, m_th_lemma_decls); @@ -949,7 +945,6 @@ void basic_decl_plugin::finalize() { DEC_REF(m_not_or_elim_decl); DEC_REF(m_rewrite_decl); DEC_REF(m_pull_quant_decl); - DEC_REF(m_pull_quant_star_decl); DEC_REF(m_push_quant_decl); DEC_REF(m_elim_unused_vars_decl); DEC_REF(m_der_decl); @@ -975,8 +970,6 @@ void basic_decl_plugin::finalize() { DEC_ARRAY_REF(m_apply_def_decls); DEC_ARRAY_REF(m_nnf_pos_decls); DEC_ARRAY_REF(m_nnf_neg_decls); - DEC_ARRAY_REF(m_nnf_star_decls); - DEC_ARRAY_REF(m_cnf_star_decls); DEC_ARRAY_REF(m_th_lemma_decls); DEC_REF(m_hyper_res_decl0); @@ -2844,12 +2837,6 @@ proof * ast_manager::mk_pull_quant(expr * e, quantifier * q) { return mk_app(m_basic_family_id, PR_PULL_QUANT, mk_iff(e, q)); } -proof * ast_manager::mk_pull_quant_star(expr * e, quantifier * q) { - if (proofs_disabled()) - return nullptr; - return mk_app(m_basic_family_id, PR_PULL_QUANT_STAR, mk_iff(e, q)); -} - proof * ast_manager::mk_push_quant(quantifier * q, expr * e) { if (proofs_disabled()) return nullptr; @@ -3094,15 +3081,6 @@ proof * ast_manager::mk_nnf_neg(expr * s, expr * t, unsigned num_proofs, proof * return mk_app(m_basic_family_id, PR_NNF_NEG, args.size(), args.c_ptr()); } -proof * ast_manager::mk_nnf_star(expr * s, expr * t, unsigned num_proofs, proof * const * proofs) { - if (proofs_disabled()) - return nullptr; - ptr_buffer args; - args.append(num_proofs, (expr**) proofs); - args.push_back(mk_oeq(s, t)); - return mk_app(m_basic_family_id, PR_NNF_STAR, args.size(), args.c_ptr()); -} - proof * ast_manager::mk_skolemization(expr * q, expr * e) { if (proofs_disabled()) return nullptr; @@ -3111,15 +3089,6 @@ proof * ast_manager::mk_skolemization(expr * q, expr * e) { return mk_app(m_basic_family_id, PR_SKOLEMIZE, mk_oeq(q, e)); } -proof * ast_manager::mk_cnf_star(expr * s, expr * t, unsigned num_proofs, proof * const * proofs) { - if (proofs_disabled()) - return nullptr; - ptr_buffer args; - args.append(num_proofs, (expr**) proofs); - args.push_back(mk_oeq(s, t)); - return mk_app(m_basic_family_id, PR_CNF_STAR, args.size(), args.c_ptr()); -} - proof * ast_manager::mk_and_elim(proof * p, unsigned i) { if (proofs_disabled()) return nullptr; diff --git a/src/ast/ast.h b/src/ast/ast.h index 55fea1b69..68e02d791 100644 --- a/src/ast/ast.h +++ b/src/ast/ast.h @@ -1042,11 +1042,11 @@ enum basic_op_kind { PR_UNDEF, PR_TRUE, PR_ASSERTED, PR_GOAL, PR_MODUS_PONENS, PR_REFLEXIVITY, PR_SYMMETRY, PR_TRANSITIVITY, PR_TRANSITIVITY_STAR, PR_MONOTONICITY, PR_QUANT_INTRO, PR_DISTRIBUTIVITY, PR_AND_ELIM, PR_NOT_OR_ELIM, PR_REWRITE, PR_REWRITE_STAR, PR_PULL_QUANT, - PR_PULL_QUANT_STAR, PR_PUSH_QUANT, PR_ELIM_UNUSED_VARS, PR_DER, PR_QUANT_INST, + PR_PUSH_QUANT, PR_ELIM_UNUSED_VARS, PR_DER, PR_QUANT_INST, PR_HYPOTHESIS, PR_LEMMA, PR_UNIT_RESOLUTION, PR_IFF_TRUE, PR_IFF_FALSE, PR_COMMUTATIVITY, PR_DEF_AXIOM, - PR_DEF_INTRO, PR_APPLY_DEF, PR_IFF_OEQ, PR_NNF_POS, PR_NNF_NEG, PR_NNF_STAR, PR_SKOLEMIZE, PR_CNF_STAR, + PR_DEF_INTRO, PR_APPLY_DEF, PR_IFF_OEQ, PR_NNF_POS, PR_NNF_NEG, PR_SKOLEMIZE, PR_MODUS_PONENS_OEQ, PR_TH_LEMMA, PR_HYPER_RESOLVE, LAST_BASIC_PR }; @@ -1080,7 +1080,6 @@ protected: func_decl * m_not_or_elim_decl; func_decl * m_rewrite_decl; func_decl * m_pull_quant_decl; - func_decl * m_pull_quant_star_decl; func_decl * m_push_quant_decl; func_decl * m_elim_unused_vars_decl; func_decl * m_der_decl; @@ -1106,8 +1105,6 @@ protected: ptr_vector m_apply_def_decls; ptr_vector m_nnf_pos_decls; ptr_vector m_nnf_neg_decls; - ptr_vector m_nnf_star_decls; - ptr_vector m_cnf_star_decls; ptr_vector m_th_lemma_decls; func_decl * m_hyper_res_decl0; @@ -2182,7 +2179,6 @@ public: proof * mk_oeq_rewrite(expr * s, expr * t); proof * mk_rewrite_star(expr * s, expr * t, unsigned num_proofs, proof * const * proofs); proof * mk_pull_quant(expr * e, quantifier * q); - proof * mk_pull_quant_star(expr * e, quantifier * q); proof * mk_push_quant(quantifier * q, expr * e); proof * mk_elim_unused_vars(quantifier * q, expr * r); proof * mk_der(quantifier * q, expr * r); @@ -2201,9 +2197,8 @@ public: proof * mk_nnf_pos(expr * s, expr * t, unsigned num_proofs, proof * const * proofs); proof * mk_nnf_neg(expr * s, expr * t, unsigned num_proofs, proof * const * proofs); - proof * mk_nnf_star(expr * s, expr * t, unsigned num_proofs, proof * const * proofs); proof * mk_skolemization(expr * q, expr * e); - proof * mk_cnf_star(expr * s, expr * t, unsigned num_proofs, proof * const * proofs); + proof * mk_and_elim(proof * p, unsigned i); proof * mk_not_or_elim(proof * p, unsigned i); diff --git a/src/ast/proofs/proof_checker.cpp b/src/ast/proofs/proof_checker.cpp index bd50e6c2a..0e16abd11 100644 --- a/src/ast/proofs/proof_checker.cpp +++ b/src/ast/proofs/proof_checker.cpp @@ -440,16 +440,6 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) { IF_VERBOSE(0, verbose_stream() << "Expected proof of equivalence with a quantifier:\n" << mk_bounded_pp(p, m);); return false; } - case PR_PULL_QUANT_STAR: { - if (match_proof(p) && - match_fact(p, fact) && - match_iff(fact.get(), t1, t2)) { - // TBD: check the enchilada. - return true; - } - IF_VERBOSE(0, verbose_stream() << "Expected proof of equivalence:\n" << mk_bounded_pp(p, m);); - return false; - } case PR_PUSH_QUANT: { if (match_proof(p) && match_fact(p, fact) && @@ -730,10 +720,6 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) { // TBD: return true; } - case PR_NNF_STAR: { - // TBD: - return true; - } case PR_SKOLEMIZE: { // (exists ?x (p ?x y)) -> (p (sk y) y) // (not (forall ?x (p ?x y))) -> (not (p (sk y) y)) @@ -755,19 +741,6 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) { UNREACHABLE(); return false; } - case PR_CNF_STAR: { - for (unsigned i = 0; i < proofs.size(); ++i) { - if (match_op(proofs[i].get(), PR_DEF_INTRO, terms)) { - // ok - } - else { - UNREACHABLE(); - return false; - } - } - // coarse grain CNF conversion. - return true; - } case PR_MODUS_PONENS_OEQ: { if (match_fact(p, fact) && match_proof(p, p0, p1) && diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h index 3393634b6..46388fcf4 100644 --- a/src/smt/theory_arith_core.h +++ b/src/smt/theory_arith_core.h @@ -597,7 +597,6 @@ namespace smt { void theory_arith::mk_to_int_axiom(app * n) { SASSERT(m_util.is_to_int(n)); ast_manager & m = get_manager(); - context & ctx = get_context(); expr* x = n->get_arg(0); // to_int (to_real x) = x diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index 9dfd0475b..3335370eb 100644 --- a/src/smt/theory_str.cpp +++ b/src/smt/theory_str.cpp @@ -5595,6 +5595,8 @@ namespace smt { // merge arg0 and arg1 expr * arg0 = to_app(node)->get_arg(0); expr * arg1 = to_app(node)->get_arg(1); + SASSERT(arg0 != node); + SASSERT(arg1 != node); expr * arg0DeAlias = dealias_node(arg0, varAliasMap, concatAliasMap); expr * arg1DeAlias = dealias_node(arg1, varAliasMap, concatAliasMap); get_grounded_concats(arg0DeAlias, varAliasMap, concatAliasMap, varConstMap, concatConstMap, varEqConcatMap, groundedMap); diff --git a/src/tactic/core/ctx_simplify_tactic.cpp b/src/tactic/core/ctx_simplify_tactic.cpp index 6ad9c0812..93a0b2e88 100644 --- a/src/tactic/core/ctx_simplify_tactic.cpp +++ b/src/tactic/core/ctx_simplify_tactic.cpp @@ -582,7 +582,7 @@ struct ctx_simplify_tactic::imp { for (unsigned i = 0; !g.inconsistent() && i < sz; ++i) { expr * t = g.form(i); process(t, r); - proof* new_pr = m.mk_modus_ponens(g.pr(i), m.mk_rewrite_star(t, r, 0, nullptr)); // TODO :-) + proof* new_pr = m.mk_modus_ponens(g.pr(i), m.mk_rewrite(t, r)); g.update(i, r, new_pr, g.dep(i)); } } diff --git a/src/tactic/core/dom_simplify_tactic.cpp b/src/tactic/core/dom_simplify_tactic.cpp index e8d3150af..47f96a7d9 100644 --- a/src/tactic/core/dom_simplify_tactic.cpp +++ b/src/tactic/core/dom_simplify_tactic.cpp @@ -382,7 +382,7 @@ void dom_simplify_tactic::simplify_goal(goal& g) { change |= r != g.form(i); proof* new_pr = nullptr; if (g.proofs_enabled()) { - new_pr = m.mk_modus_ponens(g.pr(i), m.mk_rewrite_star(g.form(i), r, 0, nullptr)); + new_pr = m.mk_modus_ponens(g.pr(i), m.mk_rewrite(g.form(i), r)); } g.update(i, r, new_pr, g.dep(i)); } @@ -402,7 +402,7 @@ void dom_simplify_tactic::simplify_goal(goal& g) { CTRACE("simplify", r != g.form(i), tout << r << " " << mk_pp(g.form(i), m) << "\n";); proof* new_pr = nullptr; if (g.proofs_enabled()) { - new_pr = m.mk_modus_ponens(g.pr(i), m.mk_rewrite_star(g.form(i), r, 0, nullptr)); + new_pr = m.mk_modus_ponens(g.pr(i), m.mk_rewrite(g.form(i), r)); } g.update(i, r, new_pr, g.dep(i)); } From 0ce200144923fe5856054bcad11c9f5471f0d791 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 10 Mar 2018 11:39:22 -0800 Subject: [PATCH 14/19] fix build Signed-off-by: Nikolaj Bjorner --- examples/tptp/tptp5.cpp | 11 ----------- scripts/mk_util.py | 9 +++++++-- 2 files changed, 7 insertions(+), 13 deletions(-) diff --git a/examples/tptp/tptp5.cpp b/examples/tptp/tptp5.cpp index b2736df4c..772440b42 100644 --- a/examples/tptp/tptp5.cpp +++ b/examples/tptp/tptp5.cpp @@ -1609,7 +1609,6 @@ public: display_inference(out, "rewrite", "thm", p); break; case Z3_OP_PR_PULL_QUANT: - case Z3_OP_PR_PULL_QUANT_STAR: display_inference(out, "pull_quant", "thm", p); break; case Z3_OP_PR_PUSH_QUANT: @@ -1669,12 +1668,6 @@ public: case Z3_OP_PR_NNF_NEG: display_inference(out, "nnf_neg", "sab", p); break; - case Z3_OP_PR_NNF_STAR: - display_inference(out, "nnf", "sab", p); - break; - case Z3_OP_PR_CNF_STAR: - display_inference(out, "cnf", "sab", p); - break; case Z3_OP_PR_SKOLEMIZE: display_inference(out, "skolemize", "sab", p); break; @@ -1706,10 +1699,6 @@ public: return display_hyp_inference(out, "modus_ponens", "thm", conclusion, hyp, hyp2); } case Z3_OP_PR_NNF_POS: - case Z3_OP_PR_NNF_STAR: - return display_hyp_inference(out, "nnf", "sab", conclusion, hyp); - case Z3_OP_PR_CNF_STAR: - return display_hyp_inference(out, "cnf", "sab", conclusion, hyp); case Z3_OP_PR_SKOLEMIZE: return display_hyp_inference(out, "skolemize", "sab", conclusion, hyp); case Z3_OP_PR_TRANSITIVITY: diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 03256125c..fecc207d8 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -889,8 +889,13 @@ def is_CXX_gpp(): return is_compiler(CXX, 'g++') def is_clang_in_gpp_form(cc): - version_string = check_output([cc, '--version']).encode('utf-8').decode('utf-8') - return version_string.find('clang') != -1 + str = check_output([cc, '--version']) + try: + version_string = str.encode('utf-8') + except: + version_string = str + clang = 'clang'.encode('utf-8') + return version_string.find(clang) != -1 def is_CXX_clangpp(): if is_compiler(CXX, 'g++'): From 58544925048b8559880edb20ccca385c895f1acb Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 10 Mar 2018 11:59:42 -0800 Subject: [PATCH 15/19] add stdbool.h to see whether build system breaks #1526 Signed-off-by: Nikolaj Bjorner --- src/api/z3.h | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/api/z3.h b/src/api/z3.h index 99929f33b..b29f1d6ba 100644 --- a/src/api/z3.h +++ b/src/api/z3.h @@ -21,7 +21,8 @@ Notes: #ifndef Z3_H_ #define Z3_H_ -#include +#include +#include #include "z3_macros.h" #include "z3_api.h" #include "z3_ast_containers.h" From 3d9139f6efaf9f6fb4a2f6226384a5824ae986a6 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 10 Mar 2018 12:07:55 -0800 Subject: [PATCH 16/19] bump revision Signed-off-by: Nikolaj Bjorner --- CMakeLists.txt | 2 +- scripts/mk_project.py | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index 62045016a..4d8c15493 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -34,7 +34,7 @@ endif() ################################################################################ set(Z3_VERSION_MAJOR 4) set(Z3_VERSION_MINOR 6) -set(Z3_VERSION_PATCH 1) +set(Z3_VERSION_PATCH 2) set(Z3_VERSION_TWEAK 0) set(Z3_VERSION "${Z3_VERSION_MAJOR}.${Z3_VERSION_MINOR}.${Z3_VERSION_PATCH}.${Z3_VERSION_TWEAK}") set(Z3_FULL_VERSION_STR "${Z3_VERSION}") # Note this might be modified diff --git a/scripts/mk_project.py b/scripts/mk_project.py index 8f75e97ed..2f7402760 100644 --- a/scripts/mk_project.py +++ b/scripts/mk_project.py @@ -9,7 +9,7 @@ from mk_util import * # Z3 Project definition def init_project_def(): - set_version(4, 6, 1, 0) + set_version(4, 6, 2, 0) add_lib('util', []) add_lib('lp', ['util'], 'util/lp') add_lib('polynomial', ['util'], 'math/polynomial') From 5651d00751a1eb40b94db86f00cb7d3ec9711c4d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 12 Mar 2018 13:21:31 -0700 Subject: [PATCH 17/19] fix #1534 Signed-off-by: Nikolaj Bjorner --- src/math/polynomial/upolynomial.cpp | 18 ++++++++---------- src/smt/theory_str.cpp | 18 ++++++++++-------- src/smt/theory_str.h | 9 +++++---- 3 files changed, 23 insertions(+), 22 deletions(-) diff --git a/src/math/polynomial/upolynomial.cpp b/src/math/polynomial/upolynomial.cpp index f7cc16de2..cc2442981 100644 --- a/src/math/polynomial/upolynomial.cpp +++ b/src/math/polynomial/upolynomial.cpp @@ -781,17 +781,15 @@ namespace upolynomial { set(q.size(), q.c_ptr(), C); m().set(bound, p); } + else if (q.size() < C.size() || m().m().is_even(p) || m().m().is_even(bound)) { + // discard accumulated image, it was affected by unlucky primes + TRACE("mgcd", tout << "discarding image\n";); + set(q.size(), q.c_ptr(), C); + m().set(bound, p); + } else { - if (q.size() < C.size()) { - // discard accumulated image, it was affected by unlucky primes - TRACE("mgcd", tout << "discarding image\n";); - set(q.size(), q.c_ptr(), C); - m().set(bound, p); - } - else { - CRA_combine_images(q, p, C, bound); - TRACE("mgcd", tout << "new combined:\n"; display_star(tout, C); tout << "\n";); - } + CRA_combine_images(q, p, C, bound); + TRACE("mgcd", tout << "new combined:\n"; display_star(tout, C); tout << "\n";); } numeral_vector & candidate = q; get_primitive(C, candidate); diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index 3335370eb..0016b8f36 100644 --- a/src/smt/theory_str.cpp +++ b/src/smt/theory_str.cpp @@ -5553,7 +5553,8 @@ namespace smt { return node; } - void theory_str::get_grounded_concats(expr* node, std::map & varAliasMap, + void theory_str::get_grounded_concats(unsigned depth, + expr* node, std::map & varAliasMap, std::map & concatAliasMap, std::map & varConstMap, std::map & concatConstMap, std::map > & varEqConcatMap, std::map, std::set > > & groundedMap) { @@ -5568,6 +5569,9 @@ namespace smt { if (groundedMap.find(node) != groundedMap.end()) { return; } + IF_VERBOSE(100, verbose_stream() << "concats " << depth << "\n"; + if (depth > 100) verbose_stream() << mk_pp(node, get_manager()) << "\n"; + ); // haven't computed grounded concats for "node" (de-aliased) // --------------------------------------------------------- @@ -5595,12 +5599,10 @@ namespace smt { // merge arg0 and arg1 expr * arg0 = to_app(node)->get_arg(0); expr * arg1 = to_app(node)->get_arg(1); - SASSERT(arg0 != node); - SASSERT(arg1 != node); expr * arg0DeAlias = dealias_node(arg0, varAliasMap, concatAliasMap); expr * arg1DeAlias = dealias_node(arg1, varAliasMap, concatAliasMap); - get_grounded_concats(arg0DeAlias, varAliasMap, concatAliasMap, varConstMap, concatConstMap, varEqConcatMap, groundedMap); - get_grounded_concats(arg1DeAlias, varAliasMap, concatAliasMap, varConstMap, concatConstMap, varEqConcatMap, groundedMap); + get_grounded_concats(depth + 1, arg0DeAlias, varAliasMap, concatAliasMap, varConstMap, concatConstMap, varEqConcatMap, groundedMap); + get_grounded_concats(depth + 1, arg1DeAlias, varAliasMap, concatAliasMap, varConstMap, concatConstMap, varEqConcatMap, groundedMap); std::map, std::set >::iterator arg0_grdItor = groundedMap[arg0DeAlias].begin(); std::map, std::set >::iterator arg1_grdItor; @@ -5650,7 +5652,7 @@ namespace smt { else if (varEqConcatMap.find(node) != varEqConcatMap.end()) { expr * eqConcat = varEqConcatMap[node].begin()->first; expr * deAliasedEqConcat = dealias_node(eqConcat, varAliasMap, concatAliasMap); - get_grounded_concats(deAliasedEqConcat, varAliasMap, concatAliasMap, varConstMap, concatConstMap, varEqConcatMap, groundedMap); + get_grounded_concats(depth + 1, deAliasedEqConcat, varAliasMap, concatAliasMap, varConstMap, concatConstMap, varEqConcatMap, groundedMap); std::map, std::set >::iterator grdItor = groundedMap[deAliasedEqConcat].begin(); for (; grdItor != groundedMap[deAliasedEqConcat].end(); grdItor++) { @@ -5859,8 +5861,8 @@ namespace smt { expr* strDeAlias = dealias_node(str, varAliasMap, concatAliasMap); expr* subStrDeAlias = dealias_node(subStr, varAliasMap, concatAliasMap); - get_grounded_concats(strDeAlias, varAliasMap, concatAliasMap, varConstMap, concatConstMap, varEqConcatMap, groundedMap); - get_grounded_concats(subStrDeAlias, varAliasMap, concatAliasMap, varConstMap, concatConstMap, varEqConcatMap, groundedMap); + get_grounded_concats(0, strDeAlias, varAliasMap, concatAliasMap, varConstMap, concatConstMap, varEqConcatMap, groundedMap); + get_grounded_concats(0, subStrDeAlias, varAliasMap, concatAliasMap, varConstMap, concatConstMap, varEqConcatMap, groundedMap); // debugging print_grounded_concat(strDeAlias, groundedMap); diff --git a/src/smt/theory_str.h b/src/smt/theory_str.h index 9288bac7c..64ede71b5 100644 --- a/src/smt/theory_str.h +++ b/src/smt/theory_str.h @@ -495,10 +495,11 @@ protected: std::map & concatAliasMap, std::map & varConstMap, std::map & concatConstMap, std::map > & varEqConcatMap); expr * dealias_node(expr * node, std::map & varAliasMap, std::map & concatAliasMap); - void get_grounded_concats(expr* node, std::map & varAliasMap, - std::map & concatAliasMap, std::map & varConstMap, - std::map & concatConstMap, std::map > & varEqConcatMap, - std::map, std::set > > & groundedMap); + void get_grounded_concats(unsigned depth, + expr* node, std::map & varAliasMap, + std::map & concatAliasMap, std::map & varConstMap, + std::map & concatConstMap, std::map > & varEqConcatMap, + std::map, std::set > > & groundedMap); void print_grounded_concat(expr * node, std::map, std::set > > & groundedMap); void check_subsequence(expr* str, expr* strDeAlias, expr* subStr, expr* subStrDeAlias, expr* boolVar, std::map, std::set > > & groundedMap); From 5f7bd993de4b83d95e22921d424a7902d0480f83 Mon Sep 17 00:00:00 2001 From: Pierre Pronchery Date: Tue, 13 Mar 2018 21:37:22 +0100 Subject: [PATCH 18/19] Add support for NetBSD Originally from David Holland . --- CMakeLists.txt | 3 +++ scripts/mk_util.py | 17 ++++++++++++++++- src/util/scoped_timer.cpp | 18 +++++++++--------- src/util/stopwatch.h | 5 +++++ 4 files changed, 33 insertions(+), 10 deletions(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index 4d8c15493..c11c272be 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -240,6 +240,9 @@ elseif ("${CMAKE_SYSTEM_NAME}" STREQUAL "Darwin") elseif ("${CMAKE_SYSTEM_NAME}" MATCHES "FreeBSD") message(STATUS "Platform: FreeBSD") list(APPEND Z3_COMPONENT_CXX_DEFINES "-D_FREEBSD_") +elseif ("${CMAKE_SYSTEM_NAME}" MATCHES "NetBSD") + message(STATUS "Platform: NetBSD") + list(APPEND Z3_COMPONENT_CXX_DEFINES "-D_NetBSD_") elseif ("${CMAKE_SYSTEM_NAME}" MATCHES "OpenBSD") message(STATUS "Platform: OpenBSD") list(APPEND Z3_COMPONENT_CXX_DEFINES "-D_OPENBSD_") diff --git a/scripts/mk_util.py b/scripts/mk_util.py index fecc207d8..99de61703 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -69,6 +69,7 @@ IS_WINDOWS=False IS_LINUX=False IS_OSX=False IS_FREEBSD=False +IS_NETBSD=False IS_OPENBSD=False IS_CYGWIN=False IS_CYGWIN_MINGW=False @@ -141,6 +142,9 @@ def is_linux(): def is_freebsd(): return IS_FREEBSD +def is_netbsd(): + return IS_NETBSD + def is_openbsd(): return IS_OPENBSD @@ -604,6 +608,8 @@ elif os.name == 'posix': IS_LINUX=True elif os.uname()[0] == 'FreeBSD': IS_FREEBSD=True + elif os.uname()[0] == 'NetBSD': + IS_NETBSD=True elif os.uname()[0] == 'OpenBSD': IS_OPENBSD=True elif os.uname()[0][:6] == 'CYGWIN': @@ -1245,7 +1251,7 @@ def get_so_ext(): sysname = os.uname()[0] if sysname == 'Darwin': return 'dylib' - elif sysname == 'Linux' or sysname == 'FreeBSD' or sysname == 'OpenBSD': + elif sysname == 'Linux' or sysname == 'FreeBSD' or sysname == 'NetBSD' or sysname == 'OpenBSD': return 'so' elif sysname == 'CYGWIN' or sysname.startswith('MSYS_NT') or sysname.startswith('MINGW'): return 'dll' @@ -1795,6 +1801,8 @@ class JavaDLLComponent(Component): t = t.replace('PLATFORM', 'linux') elif IS_FREEBSD: t = t.replace('PLATFORM', 'freebsd') + elif IS_NETBSD: + t = t.replace('PLATFORM', 'netbsd') elif IS_OPENBSD: t = t.replace('PLATFORM', 'openbsd') elif IS_CYGWIN: @@ -2504,6 +2512,13 @@ def mk_config(): LDFLAGS = '%s -lrt' % LDFLAGS SLIBFLAGS = '-shared' SLIBEXTRAFLAGS = '%s -lrt' % SLIBEXTRAFLAGS + elif sysname == 'NetBSD': + CXXFLAGS = '%s -D_NETBSD_' % CXXFLAGS + OS_DEFINES = '-D_NETBSD_' + SO_EXT = '.so' + LDFLAGS = '%s -lrt' % LDFLAGS + SLIBFLAGS = '-shared' + SLIBEXTRAFLAGS = '%s -lrt' % SLIBEXTRAFLAGS elif sysname == 'OpenBSD': CXXFLAGS = '%s -D_OPENBSD_' % CXXFLAGS OS_DEFINES = '-D_OPENBSD_' diff --git a/src/util/scoped_timer.cpp b/src/util/scoped_timer.cpp index 1ecca8ffe..a2a0cc269 100644 --- a/src/util/scoped_timer.cpp +++ b/src/util/scoped_timer.cpp @@ -33,8 +33,8 @@ Revision History: #include #include #include -#elif defined(_LINUX_) || defined(_FREEBSD_) -// Linux +#elif defined(_LINUX_) || defined(_FREEBSD_) || defined(_NetBSD_) +// Linux & FreeBSD & NetBSD #include #include #include @@ -66,8 +66,8 @@ struct scoped_timer::imp { pthread_mutex_t m_mutex; pthread_cond_t m_condition_var; struct timespec m_end_time; -#elif defined(_LINUX_) || defined(_FREEBSD_) - // Linux & FreeBSD +#elif defined(_LINUX_) || defined(_FREEBSD_) || defined(_NETBSD_) + // Linux & FreeBSD & NetBSD pthread_t m_thread_id; pthread_mutex_t m_mutex; pthread_cond_t m_cond; @@ -104,7 +104,7 @@ struct scoped_timer::imp { return st; } -#elif defined(_LINUX_) || defined(_FREEBSD_) +#elif defined(_LINUX_) || defined(_FREEBSD_) || defined(_NETBSD_) static void* thread_func(void *arg) { scoped_timer::imp *st = static_cast(arg); @@ -175,8 +175,8 @@ struct scoped_timer::imp { if (pthread_create(&m_thread_id, &m_attributes, &thread_func, this) != 0) throw default_exception("failed to start timer thread"); -#elif defined(_LINUX_) || defined(_FREEBSD_) - // Linux & FreeBSD +#elif defined(_LINUX_) || defined(_FREEBSD_) || defined(_NETBSD_) + // Linux & FreeBSD & NetBSD m_ms = ms; m_initialized = false; m_signal_sent = false; @@ -216,8 +216,8 @@ struct scoped_timer::imp { throw default_exception("failed to destroy pthread condition variable"); if (pthread_attr_destroy(&m_attributes) != 0) throw default_exception("failed to destroy pthread attributes object"); -#elif defined(_LINUX_) || defined(_FREEBSD_) - // Linux & FreeBSD +#elif defined(_LINUX_) || defined(_FREEBSD_) || defined(_NETBSD_) + // Linux & FreeBSD & NetBSD bool init = false; // spin until timer thread has been created diff --git a/src/util/stopwatch.h b/src/util/stopwatch.h index 9ba707af0..83e03a2f7 100644 --- a/src/util/stopwatch.h +++ b/src/util/stopwatch.h @@ -134,6 +134,11 @@ public: #include +#ifndef CLOCK_PROCESS_CPUTIME_ID +/* BSD */ +# define CLOCK_PROCESS_CPUTIME_ID CLOCK_MONOTONIC +#endif + class stopwatch { unsigned long long m_time; // elapsed time in ns bool m_running; From 2b2aee3c18bee27bee94908d650596e7e5424b64 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 14 Mar 2018 07:29:26 -0700 Subject: [PATCH 19/19] remove unused operators #1530 Signed-off-by: Nikolaj Bjorner --- src/api/ml/z3.ml | 3 --- 1 file changed, 3 deletions(-) diff --git a/src/api/ml/z3.ml b/src/api/ml/z3.ml index 120b0ddfd..5766c79f9 100644 --- a/src/api/ml/z3.ml +++ b/src/api/ml/z3.ml @@ -1402,7 +1402,6 @@ struct let is_rewrite (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_PR_REWRITE) let is_rewrite_star (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_PR_REWRITE_STAR) let is_pull_quant (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_PR_PULL_QUANT) - let is_pull_quant_star (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_PR_PULL_QUANT_STAR) let is_push_quant (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_PR_PUSH_QUANT) let is_elim_unused_vars (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_PR_ELIM_UNUSED_VARS) let is_der (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_PR_DER) @@ -1419,8 +1418,6 @@ struct let is_iff_oeq (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_PR_IFF_OEQ) let is_nnf_pos (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_PR_NNF_POS) let is_nnf_neg (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_PR_NNF_NEG) - let is_nnf_star (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_PR_NNF_STAR) - let is_cnf_star (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_PR_CNF_STAR) let is_skolemize (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_PR_SKOLEMIZE) let is_modus_ponens_oeq (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_PR_MODUS_PONENS_OEQ) let is_theory_lemma (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_PR_TH_LEMMA)