From feb5360999aa8cfdc56f521148d8d05791c70ceb Mon Sep 17 00:00:00 2001 From: Ken McMillan Date: Sun, 28 Apr 2013 16:29:55 -0700 Subject: [PATCH] integrating duality --- src/duality/duality.h | 7 +- src/duality/duality_rpfp.cpp | 6 + src/duality/duality_solver.cpp | 4 + src/duality/duality_wrapper.cpp | 31 +++ src/duality/duality_wrapper.h | 11 +- src/muz_qe/dl_context.cpp | 4 +- src/muz_qe/duality_dl_interface.cpp | 333 ++++++++++++++++++++++++++++ src/muz_qe/duality_dl_interface.h | 76 +++++++ src/muz_qe/fixedpoint_params.pyg | 6 + 9 files changed, 473 insertions(+), 5 deletions(-) create mode 100644 src/muz_qe/duality_dl_interface.cpp create mode 100644 src/muz_qe/duality_dl_interface.h diff --git a/src/duality/duality.h b/src/duality/duality.h index c75ecfa61..1017e0b60 100644 --- a/src/duality/duality.h +++ b/src/duality/duality.h @@ -171,6 +171,7 @@ namespace Duality { const std::vector &assumptions, const std::vector &theory ){} + virtual ~LogicSolver(){} }; /** This solver uses iZ3. */ @@ -205,8 +206,8 @@ namespace Duality { } #endif - iZ3LogicSolver(context c){ - ctx = ictx = new interpolating_context(c); + iZ3LogicSolver(context &c){ + ctx = ictx = &c; slvr = islvr = new interpolating_solver(*ictx); need_goals = false; islvr->SetWeakInterpolants(true); @@ -221,7 +222,7 @@ namespace Duality { #endif } ~iZ3LogicSolver(){ - delete ictx; + // delete ictx; delete islvr; } }; diff --git a/src/duality/duality_rpfp.cpp b/src/duality/duality_rpfp.cpp index 6b176a574..ca6061520 100644 --- a/src/duality/duality_rpfp.cpp +++ b/src/duality/duality_rpfp.cpp @@ -590,7 +590,12 @@ namespace Duality { if (res == l_false) { DecodeTree(root, interpolant->getChildren()[0], persist); + delete interpolant; } + + delete tree; + if(goals) + delete goals; timer_stop("Solve"); return res; @@ -828,6 +833,7 @@ namespace Duality { return res; } + #ifdef Z3OPS static Z3_subterm_truth *stt; #endif diff --git a/src/duality/duality_solver.cpp b/src/duality/duality_solver.cpp index d5c6579d1..799b94c20 100644 --- a/src/duality/duality_solver.cpp +++ b/src/duality/duality_solver.cpp @@ -267,6 +267,8 @@ namespace Duality { // print_profile(std::cout); delete indset; delete heuristic; + delete unwinding; + delete reporter; return res; } @@ -1284,6 +1286,8 @@ namespace Duality { DerivationTree dt(this,unwinding,reporter,heuristic,FullExpand); bool res = dt.Derive(unwinding,node,UseUnderapprox,true); // build full tree if(!res) throw "Duality internal error in BuildFullCex"; + if(cex.tree) + delete cex.tree; cex.tree = dt.tree; cex.root = dt.top; } diff --git a/src/duality/duality_wrapper.cpp b/src/duality/duality_wrapper.cpp index e5a8e31f4..b106709f1 100644 --- a/src/duality/duality_wrapper.cpp +++ b/src/duality/duality_wrapper.cpp @@ -161,6 +161,33 @@ expr context::make_quant(decl_kind op, const std::vector &bvs, const expr return cook(result.get()); } +expr context::make_quant(decl_kind op, const std::vector &_sorts, const std::vector &_names, const expr &body){ + if(_sorts.size() == 0) return body; + + + std::vector< ::symbol> names; + std::vector< ::sort *> types; + std::vector< ::expr *> bound_asts; + unsigned num_bound = _sorts.size(); + + for (unsigned i = 0; i < num_bound; ++i) { + names.push_back(_names[i]); + types.push_back(to_sort(_sorts[i].raw())); + } + expr_ref result(m()); + result = m().mk_quantifier( + op == Forall, + names.size(), &types[0], &names[0], to_expr(body.raw()), + 0, + ::symbol(), + ::symbol(), + 0, 0, + 0, 0 + ); + return cook(result.get()); +} + + decl_kind func_decl::get_decl_kind() const { return ctx().get_decl_kind(*this); } @@ -453,6 +480,10 @@ expr context::make_quant(decl_kind op, const std::vector &bvs, const expr for(unsigned i = 0; i < _interpolants.size(); i++) linearized_interpolants[i] = expr(ctx(),_interpolants[i]); + // since iz3interpolant returns interpolants with one ref count, we decrement here + for(unsigned i = 0; i < _interpolants.size(); i++) + m().dec_ref(_interpolants[i]); + unlinearize_interpolants(0,assumptions,linearized_interpolants,interpolant); interpolant->setTerm(ctx().bool_val(false)); } diff --git a/src/duality/duality_wrapper.h b/src/duality/duality_wrapper.h index 0afad2df9..20557e3e2 100755 --- a/src/duality/duality_wrapper.h +++ b/src/duality/duality_wrapper.h @@ -234,6 +234,7 @@ namespace Duality { expr make(decl_kind op, const expr &arg0, const expr &arg1, const expr &arg2); expr make_quant(decl_kind op, const std::vector &bvs, const expr &body); + expr make_quant(decl_kind op, const std::vector &_sorts, const std::vector &_names, const expr &body); decl_kind get_decl_kind(const func_decl &t); @@ -771,7 +772,10 @@ namespace Duality { solver(context & c); solver(context & c, ::solver *s):object(c),the_model(c) { m_solver = s; } solver(solver const & s):object(s), the_model(s.the_model) { m_solver = s.m_solver;} - ~solver() { } + ~solver() { + if(m_solver) + dealloc(m_solver); + } operator ::solver*() const { return m_solver; } solver & operator=(solver const & s) { m_ctx = s.m_ctx; @@ -1202,6 +1206,11 @@ namespace Duality { num = _num; } + ~TermTree(){ + for(unsigned i = 0; i < children.size(); i++) + delete children[i]; + } + private: expr term; std::vector children; diff --git a/src/muz_qe/dl_context.cpp b/src/muz_qe/dl_context.cpp index 931a96ced..082b44815 100644 --- a/src/muz_qe/dl_context.cpp +++ b/src/muz_qe/dl_context.cpp @@ -1186,7 +1186,9 @@ namespace datalog { m_tab->display_certificate(out); return true; case DUALITY_ENGINE: - return false; + ensure_duality(); + m_duality->display_certificate(out); + return true; default: return false; } diff --git a/src/muz_qe/duality_dl_interface.cpp b/src/muz_qe/duality_dl_interface.cpp new file mode 100644 index 000000000..6ccaaf52f --- /dev/null +++ b/src/muz_qe/duality_dl_interface.cpp @@ -0,0 +1,333 @@ +/*++ +Copyright (c) 2013 Microsoft Corporation + +Module Name: + + duality_dl_interface.cpp + +Abstract: + + SMT2 interface for Duality + +Author: + + Krystof Hoder (t-khoder) 2011-9-22. + Modified by Ken McMIllan (kenmcmil) 2013-4-18. + +Revision History: + +--*/ + +#include "dl_cmds.h" +#include "dl_context.h" +#include "dl_mk_coi_filter.h" +#include "dl_mk_interp_tail_simplifier.h" +#include "dl_mk_subsumption_checker.h" +#include "dl_mk_rule_inliner.h" +#include "dl_rule.h" +#include "dl_rule_transformer.h" +#include "dl_mk_extract_quantifiers.h" +#include "smt2parser.h" +#include "duality_dl_interface.h" +#include "dl_rule_set.h" +#include "dl_mk_slice.h" +#include "dl_mk_unfold.h" +#include "dl_mk_coalesce.h" +#include "expr_abstract.h" +#include "model_smt2_pp.h" + +#include "duality.h" + +using namespace Duality; + +namespace Duality { + + enum DualityStatus {StatusModel, StatusRefutation, StatusUnknown, StatusNull}; + + class duality_data { + public: + context ctx; + RPFP::LogicSolver *ls; + RPFP *rpfp; + + DualityStatus status; + std::vector clauses; + hash_map map; // edges to clauses + Solver::Counterexample cex; + + duality_data(ast_manager &_m) : ctx(_m,config(params_ref())) { + ls = 0; + rpfp = 0; + status = StatusNull; + } + ~duality_data(){ + if(rpfp) + dealloc(rpfp); + if(ls) + dealloc(ls); + if(cex.tree) + delete cex.tree; + } + }; + + +dl_interface::dl_interface(datalog::context& dl_ctx) : m_ctx(dl_ctx) + +{ + _d = alloc(duality_data,dl_ctx.get_manager()); + _d->ls = alloc(RPFP::iZ3LogicSolver,_d->ctx); + _d->rpfp = alloc(RPFP,_d->ls); +} + + +dl_interface::~dl_interface() { + dealloc(_d); +} + + +// +// Check if the new rules are weaker so that we can +// re-use existing context. +// +#if 0 +void dl_interface::check_reset() { + // TODO + datalog::rule_ref_vector const& new_rules = m_ctx.get_rules().get_rules(); + datalog::rule_ref_vector const& old_rules = m_old_rules.get_rules(); + bool is_subsumed = !old_rules.empty(); + for (unsigned i = 0; is_subsumed && i < new_rules.size(); ++i) { + is_subsumed = false; + for (unsigned j = 0; !is_subsumed && j < old_rules.size(); ++j) { + if (m_ctx.check_subsumes(*old_rules[j], *new_rules[i])) { + is_subsumed = true; + } + } + if (!is_subsumed) { + TRACE("pdr", new_rules[i]->display(m_ctx, tout << "Fresh rule ");); + m_context->reset(); + } + } + m_old_rules.reset(); + m_old_rules.add_rules(new_rules.size(), new_rules.c_ptr()); +} +#endif + + + lbool dl_interface::query(::expr * query) { + // TODO: you can only call this once! + // we restore the initial state in the datalog context + m_ctx.ensure_opened(); + + expr_ref_vector rules(m_ctx.get_manager()); + svector< ::symbol> names; + + m_ctx.get_rules_as_formulas(rules, names); + + // get all the rules as clauses + std::vector &clauses = _d->clauses; + clauses.clear(); + for (unsigned i = 0; i < rules.size(); ++i) { + expr e(_d->ctx,rules[i].get()); + clauses.push_back(e); + } + + // turn the query into a clause + expr q(_d->ctx,query); + + std::vector b_sorts; + std::vector b_names; + if (q.is_quantifier() && !q.is_quantifier_forall()) { + int bound = q.get_quantifier_num_bound(); + for(int j = 0; j < bound; j++){ + b_sorts.push_back(q.get_quantifier_bound_sort(j)); + b_names.push_back(q.get_quantifier_bound_name(j)); + } + q = q.arg(0); + } + + expr qc = implies(q,_d->ctx.bool_val(false)); + qc = _d->ctx.make_quant(Exists,b_sorts,b_names,qc); + clauses.push_back(qc); + + // get the background axioms + unsigned num_asserts = m_ctx.get_num_assertions(); + for (unsigned i = 0; i < num_asserts; ++i) { + expr e(_d->ctx,m_ctx.get_assertion(i)); + _d->rpfp->AssertAxiom(e); + } + + // creates 1-1 map between clauses and rpfp edges + _d->rpfp->FromClauses(clauses); + + // populate the edge-to-clause map + for(unsigned i = 0; i < _d->rpfp->edges.size(); ++i) + _d->map[_d->rpfp->edges[i]] = i; + + // create a solver object + + Solver *rs = Solver::Create("duality", _d->rpfp); + + // set its options + IF_VERBOSE(1, rs->SetOption("report","1");); + rs->SetOption("full_expand",m_ctx.get_params().full_expand() ? "1" : "0"); + rs->SetOption("no_conj",m_ctx.get_params().no_conj() ? "1" : "0"); + rs->SetOption("feasible_edges",m_ctx.get_params().feasible_edges() ? "1" : "0"); + rs->SetOption("use_underapprox",m_ctx.get_params().use_underapprox() ? "1" : "0"); + rs->SetOption("stratified_inlining",m_ctx.get_params().stratified_inlining() ? "1" : "0"); + unsigned rb = m_ctx.get_params().recursion_bound(); + if(rb != UINT_MAX){ + std::ostringstream os; os << rb; + rs->SetOption("recursion_bound", os.str()); + } + + // Solve! + bool ans = rs->Solve(); + + // save the result and counterexample if there is one + _d->status = ans ? StatusModel : StatusRefutation; + _d->cex = rs->GetCounterexample(); + + dealloc(rs); + + // true means the RPFP problem is SAT, so the query is UNSAT + return ans ? l_false : l_true; +} + +expr_ref dl_interface::get_cover_delta(int level, ::func_decl* pred_orig) { + SASSERT(false); + return expr_ref(m_ctx.get_manager()); +} + + void dl_interface::add_cover(int level, ::func_decl* pred, ::expr* property) { + SASSERT(false); +} + + unsigned dl_interface::get_num_levels(::func_decl* pred) { + SASSERT(false); + return 0; +} + + void dl_interface::collect_statistics(::statistics& st) const { +} + +void dl_interface::reset_statistics() { +} + +static void print_proof(dl_interface *d, std::ostream& out, Solver::Counterexample &cex) { + context &ctx = d->dd()->ctx; + RPFP::Node &node = *cex.root; + RPFP::Edge &edge = *node.Outgoing; + + // first, prove the children (that are actually used) + + for(unsigned i = 0; i < edge.Children.size(); i++){ + if(!cex.tree->Empty(edge.Children[i])){ + Solver::Counterexample foo = cex; + foo.root = edge.Children[i]; + print_proof(d,out,foo); + } + } + + // print the label and the proved fact + + out << "(" << node.number; + out << " (" << node.Name.name(); + for(unsigned i = 0; i < edge.F.IndParams.size(); i++) + out << " " << cex.tree->Eval(&edge,edge.F.IndParams[i]); + out << ")\n"; + + // print the substitution + + out << " (\n"; + RPFP::Edge *orig_edge = edge.map; + int orig_clause = d->dd()->map[orig_edge]; + expr &t = d->dd()->clauses[orig_clause]; + if (t.is_quantifier() && t.is_quantifier_forall()) { + int bound = t.get_quantifier_num_bound(); + std::vector sorts; + std::vector names; + hash_map subst; + for(int j = 0; j < bound; j++){ + sort the_sort = t.get_quantifier_bound_sort(j); + symbol name = t.get_quantifier_bound_name(j); + expr skolem = ctx.constant(symbol(ctx,name),sort(ctx,the_sort)); + out << " (= " << skolem << " " << cex.tree->Eval(&edge,skolem) << ")\n"; + } + } + out << " )\n"; + + // reference the proofs of all the children, in syntactic order + // "true" means the child is not needed + + out << " ("; + for(unsigned i = 0; i < edge.Children.size(); i++){ + if(!cex.tree->Empty(edge.Children[i])) + out << " " << edge.Children[i]->number; + else + out << " true"; + } + out << " )"; + out << ")\n"; +} + + +void dl_interface::display_certificate(std::ostream& out) { + if(_d->status == StatusModel){ + ast_manager &m = m_ctx.get_manager(); + model_ref md = get_model(); + model_smt2_pp(out, m, *md.get(), 0); + } + else if(_d->status == StatusRefutation){ + out << "(\n"; + // negation of the query is the last clause -- prove it + print_proof(this,out,_d->cex); + out << ")\n"; + } +} + +expr_ref dl_interface::get_answer() { + SASSERT(false); + return expr_ref(m_ctx.get_manager()); +} + +void dl_interface::cancel() { +} + +void dl_interface::cleanup() { +} + +void dl_interface::updt_params() { +} + +model_ref dl_interface::get_model() { + ast_manager &m = m_ctx.get_manager(); + model_ref md(alloc(::model, m)); + std::vector &nodes = _d->rpfp->nodes; + expr_ref_vector conjs(m); + for (unsigned i = 0; i < nodes.size(); ++i) { + RPFP::Node *node = nodes[i]; + func_decl &pred = node->Name; + expr_ref prop(m); + prop = to_expr(node->Annotation.Formula); + std::vector ¶ms = node->Annotation.IndParams; + expr_ref q(m); + expr_ref_vector sig_vars(m); + for (unsigned j = 0; j < params.size(); ++j) + sig_vars.push_back(params[params.size()-j-1]); // TODO: why backwards? + expr_abstract(m, 0, sig_vars.size(), sig_vars.c_ptr(), prop, q); + if (params.empty()) { + md->register_decl(pred, q); + } + else { + ::func_interp* fi = alloc(::func_interp, m, params.size()); + fi->set_else(q); + md->register_decl(pred, fi); + } + } + return md; +} + +proof_ref dl_interface::get_proof() { + return proof_ref(m_ctx.get_manager()); +} +} diff --git a/src/muz_qe/duality_dl_interface.h b/src/muz_qe/duality_dl_interface.h new file mode 100644 index 000000000..332c3f12c --- /dev/null +++ b/src/muz_qe/duality_dl_interface.h @@ -0,0 +1,76 @@ +/*++ +Copyright (c) 2013 Microsoft Corporation + +Module Name: + + duality_dl_interface.h + +Abstract: + + SMT2 interface for Duality + +Author: + + Krystof Hoder (t-khoder) 2011-9-22. + Modified by Ken McMIllan (kenmcmil) 2013-4-18. + +Revision History: + +--*/ + +#ifndef _DUALITY_DL_INTERFACE_H_ +#define _DUALITY_DL_INTERFACE_H_ + +#include "lbool.h" +#include "dl_rule.h" +#include "dl_rule_set.h" +#include "statistics.h" + +namespace datalog { + class context; +} + +namespace Duality { + + class duality_data; + + class dl_interface { + duality_data *_d; + datalog::context &m_ctx; + + public: + dl_interface(datalog::context& ctx); + ~dl_interface(); + + lbool query(expr* query); + + void cancel(); + + void cleanup(); + + void display_certificate(std::ostream& out); + + void collect_statistics(statistics& st) const; + + void reset_statistics(); + + expr_ref get_answer(); + + unsigned get_num_levels(func_decl* pred); + + expr_ref get_cover_delta(int level, func_decl* pred); + + void add_cover(int level, func_decl* pred, expr* property); + + void updt_params(); + + model_ref get_model(); + + proof_ref get_proof(); + + duality_data *dd(){return _d;} + }; +} + + +#endif diff --git a/src/muz_qe/fixedpoint_params.pyg b/src/muz_qe/fixedpoint_params.pyg index c2cfadd14..567a35216 100644 --- a/src/muz_qe/fixedpoint_params.pyg +++ b/src/muz_qe/fixedpoint_params.pyg @@ -58,6 +58,12 @@ def_module_params('fixedpoint', ('print_certificate', BOOL, False, 'print certificate for reachability or non-reachability'), ('print_statistics', BOOL, False, 'print statistics'), ('tab_selection', SYMBOL, 'weight', 'selection method for tabular strategy: weight (default), first, var-use'), + ('full_expand', BOOL, False, 'DUALITY: Fully expand derivation trees'), + ('no_conj', BOOL, False, 'DUALITY: No forced covering (conjectures)'), + ('feasible_edges', BOOL, True, 'DUALITY: Don\'t expand definitley infeasible edges'), + ('use_underapprox', BOOL, False, 'DUALITY: Use underapproximations'), + ('stratified_inlining', BOOL, False, 'DUALITY: Use stratified inlining'), + ('recursion_bound', UINT, UINT_MAX, 'DUALITY: Recursion bound for stratified inlining'), ))