From 141236e9751b2e0fb1255dab91e19b102143b89e Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 22 Nov 2012 15:51:47 -0800 Subject: [PATCH] fix seg-fault bugs reported by Arie Signed-off-by: Nikolaj Bjorner --- src/api/python/z3.py | 1 - src/muz_qe/dl_context.cpp | 2 +- src/muz_qe/dl_context.h | 1 - src/muz_qe/pdr_context.cpp | 18 ++++++++++++++---- src/muz_qe/pdr_dl_interface.cpp | 2 +- src/muz_qe/qe_lite.cpp | 2 -- 6 files changed, 16 insertions(+), 10 deletions(-) diff --git a/src/api/python/z3.py b/src/api/python/z3.py index 537717c40..a71db82c5 100644 --- a/src/api/python/z3.py +++ b/src/api/python/z3.py @@ -827,7 +827,6 @@ class ExprRef(AstRef): else: return [] - def _to_expr_ref(a, ctx): if isinstance(a, Pattern): return PatternRef(a, ctx) diff --git a/src/muz_qe/dl_context.cpp b/src/muz_qe/dl_context.cpp index 47d0dbe75..91e396671 100644 --- a/src/muz_qe/dl_context.cpp +++ b/src/muz_qe/dl_context.cpp @@ -954,7 +954,6 @@ namespace datalog { p.insert(":default-relation", CPK_SYMBOL, "default relation implementation: 'external_relation', 'pentagon'"); p.insert(":generate-explanations", CPK_BOOL, "if true, signature of relations will be extended to contain explanations for facts"); - p.insert(":explanations-on-relation-level", CPK_BOOL, "if true, explanations are generated as history of each relation, " "rather than per fact (:generate-explanations must be set to true for this option to have any effect)"); @@ -983,6 +982,7 @@ namespace datalog { p.insert(":profile-timeout-milliseconds", CPK_UINT, "instructions and rules that took less than the threshold will not be printed when printed the instruction/rule list"); p.insert(":print-with-fixedpoint-extensions", CPK_BOOL, "(default true) use SMT-LIB2 fixedpoint extensions, instead of pure SMT2, when printing rules"); + PRIVATE_PARAMS( p.insert(":dbg-fpr-nonempty-relation-signature", CPK_BOOL, "if true, finite_product_relation will attempt to avoid creating inner relation with empty signature " diff --git a/src/muz_qe/dl_context.h b/src/muz_qe/dl_context.h index 903500cda..229bbc474 100644 --- a/src/muz_qe/dl_context.h +++ b/src/muz_qe/dl_context.h @@ -77,7 +77,6 @@ namespace datalog { typedef obj_map sort_domain_map; typedef vector > fact_vector; - ast_manager & m; front_end_params& m_fparams; params_ref m_params; diff --git a/src/muz_qe/pdr_context.cpp b/src/muz_qe/pdr_context.cpp index 404e81c24..f056342a2 100644 --- a/src/muz_qe/pdr_context.cpp +++ b/src/muz_qe/pdr_context.cpp @@ -1140,6 +1140,19 @@ namespace pdr { e->get_data().m_value->add_rule(pred_rules[i]); } } + datalog::rule_set::iterator rit = rules.begin(), rend = rules.end(); + for (; rit != rend; ++rit) { + datalog::rule* r = *rit; + pred_transformer* pt; + unsigned utz = r->get_uninterpreted_tail_size(); + for (unsigned i = 0; i < utz; ++i) { + func_decl* pred = r->get_decl(i); + if (!rels.find(pred, pt)) { + pt = alloc(pred_transformer, *this, get_pdr_manager(), pred); + rels.insert(pred, pt); + } + } + } // Initialize use list dependencies decl2rel::iterator it = rels.begin(), end = rels.end(); for (; it != end; ++it) { @@ -1149,10 +1162,7 @@ namespace pdr { obj_hashtable::iterator itf = deps.begin(), endf = deps.end(); for (; itf != endf; ++itf) { TRACE("pdr", tout << mk_pp(pred, m) << " " << mk_pp(*itf, m) << "\n";); - if (!rels.find(*itf, pt_user)) { - pt_user = alloc(pred_transformer, *this, get_pdr_manager(), *itf); - rels.insert(*itf, pt_user); - } + VERIFY (rels.find(*itf, pt_user)); pt_user->add_use(pt); } } diff --git a/src/muz_qe/pdr_dl_interface.cpp b/src/muz_qe/pdr_dl_interface.cpp index cae84d3ff..be31f4724 100644 --- a/src/muz_qe/pdr_dl_interface.cpp +++ b/src/muz_qe/pdr_dl_interface.cpp @@ -246,7 +246,7 @@ proof_ref dl_interface::get_proof() { } void dl_interface::collect_params(param_descrs& p) { - p.insert(":bfs-model-search", CPK_BOOL, "PDR: (default true) use BFS strategy for expanding model search"); + p.insert(":bfs-model-search", CPK_BOOL, "PDR: (default true) use BFS strategy for expanding model search"); p.insert(":use-farkas", CPK_BOOL, "PDR: (default true) use lemma generator based on Farkas (for linear real arithmetic)"); p.insert(":generate-proof-trace", CPK_BOOL, "PDR: (default false) trace for 'sat' answer as proof object"); p.insert(":inline-proofs", CPK_BOOL, "PDR: (default true) run PDR with proof mode turned on and extract " diff --git a/src/muz_qe/qe_lite.cpp b/src/muz_qe/qe_lite.cpp index 8a14aeb4c..6baa7ad80 100644 --- a/src/muz_qe/qe_lite.cpp +++ b/src/muz_qe/qe_lite.cpp @@ -342,8 +342,6 @@ class der2 { void flatten_args(quantifier* q, unsigned& num_args, expr*const*& args) { expr * e = q->get_expr(); - num_args = 1; - args = &e; if ((q->is_forall() && m.is_or(e)) || (q->is_exists() && m.is_and(e))) { num_args = to_app(e)->get_num_args();