From e939dd2bc59eae7b0a2c6c696157b7f8b214ba8a Mon Sep 17 00:00:00 2001 From: Ken McMillan Date: Tue, 30 Apr 2013 13:07:49 -0700 Subject: [PATCH] still integrating duality --- src/ast/ast.cpp | 7 +++++++ src/duality/duality.h | 17 ++++++++++------- src/duality/duality_rpfp.cpp | 2 +- src/duality/duality_solver.cpp | 5 ++++- src/duality/duality_wrapper.cpp | 8 +++----- src/interp/iz3interp.cpp | 12 ++++++++++++ src/interp/iz3interp.h | 7 +++++++ src/muz_qe/dl_context.cpp | 21 ++++++++++++++++----- src/muz_qe/dl_context.h | 1 + src/muz_qe/duality_dl_interface.cpp | 10 +++++----- 10 files changed, 66 insertions(+), 24 deletions(-) diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp index 797e118a7..8ecaed172 100644 --- a/src/ast/ast.cpp +++ b/src/ast/ast.cpp @@ -3152,4 +3152,11 @@ void scoped_mark::pop_scope(unsigned num_scopes) { } } +// Added by KLM for use in GDB + +// show an expr_ref on stdout + +void prexpr(expr_ref &e){ + std::cout << mk_pp(e.get(), e.get_manager()) << std::endl; +} diff --git a/src/duality/duality.h b/src/duality/duality.h index 1017e0b60..1ee9eca08 100644 --- a/src/duality/duality.h +++ b/src/duality/duality.h @@ -156,10 +156,11 @@ namespace Duality { virtual lbool interpolate_tree(TermTree *assumptions, - TermTree *&interpolants, - model &_model, - TermTree *goals = 0 - ) = 0; + TermTree *&interpolants, + model &_model, + TermTree *goals = 0, + bool weak = false + ) = 0; /** Assert a background axiom. */ virtual void assert_axiom(const expr &axiom) = 0; @@ -181,11 +182,13 @@ namespace Duality { interpolating_solver *islvr; /** iZ3 solver */ lbool interpolate_tree(TermTree *assumptions, - TermTree *&interpolants, - model &_model, - TermTree *goals = 0) + TermTree *&interpolants, + model &_model, + TermTree *goals = 0, + bool weak = false) { literals _labels; + islvr->SetWeakInterpolants(weak); return islvr->interpolate_tree(assumptions,interpolants,_model,_labels,true); } diff --git a/src/duality/duality_rpfp.cpp b/src/duality/duality_rpfp.cpp index ca6061520..78c2b6955 100644 --- a/src/duality/duality_rpfp.cpp +++ b/src/duality/duality_rpfp.cpp @@ -585,7 +585,7 @@ namespace Duality { // if (dualLabels != null) dualLabels.Dispose(); timer_start("interpolate_tree"); - lbool res = ls->interpolate_tree(tree, interpolant, dualModel,goals); + lbool res = ls->interpolate_tree(tree, interpolant, dualModel,goals,true); timer_stop("interpolate_tree"); if (res == l_false) { diff --git a/src/duality/duality_solver.cpp b/src/duality/duality_solver.cpp index 799b94c20..bd02db976 100644 --- a/src/duality/duality_solver.cpp +++ b/src/duality/duality_solver.cpp @@ -294,7 +294,9 @@ namespace Duality { /** Return the counterexample */ virtual Counterexample GetCounterexample(){ - return cex; + Counterexample res = cex; + cex.tree = 0; // Cex now belongs to caller + return res; } // options @@ -879,6 +881,7 @@ namespace Duality { #endif if(_cex) *_cex = cex; else delete cex.tree; // delete the cex if not required + cex.tree = 0; node->Bound = save; // put back original bound timer_stop("ProveConjecture"); return false; diff --git a/src/duality/duality_wrapper.cpp b/src/duality/duality_wrapper.cpp index b106709f1..17638335d 100644 --- a/src/duality/duality_wrapper.cpp +++ b/src/duality/duality_wrapper.cpp @@ -467,14 +467,12 @@ expr context::make_quant(decl_kind op, const std::vector &_sorts, const st if(res == unsat){ - // TODO -#if 0 + interpolation_options_struct opts; if(weak_mode) - Z3_set_interpolation_option(options,"weak","1"); -#endif + opts.set("weak","1"); ::ast *proof = m_solver->get_proof(); - iz3interpolate(m(),proof,_assumptions,_parents,_interpolants,_theory,0); + iz3interpolate(m(),proof,_assumptions,_parents,_interpolants,_theory,&opts); std::vector linearized_interpolants(_interpolants.size()); for(unsigned i = 0; i < _interpolants.size(); i++) diff --git a/src/interp/iz3interp.cpp b/src/interp/iz3interp.cpp index 6a9c54716..aac8648ba 100755 --- a/src/interp/iz3interp.cpp +++ b/src/interp/iz3interp.cpp @@ -323,6 +323,8 @@ void iz3interpolate(ast_manager &_m_manager, interpolation_options_struct * options) { iz3interp itp(_m_manager); + if(options) + options->apply(itp); std::vector _cnsts(cnsts.size()); std::vector _parents(parents.size()); std::vector _interps; @@ -348,6 +350,8 @@ void iz3interpolate(ast_manager &_m_manager, interpolation_options_struct * options) { iz3interp itp(_m_manager); + if(options) + options->apply(itp); std::vector _cnsts(cnsts.size()); std::vector _interps; for(unsigned i = 0; i < cnsts.size(); i++) @@ -369,6 +373,8 @@ lbool iz3interpolate(ast_manager &_m_manager, interpolation_options_struct * options) { iz3interp itp(_m_manager); + if(options) + options->apply(itp); iz3mgr::ast _tree = itp.cook(tree); std::vector _cnsts; itp.assert_conjuncts(s,_cnsts,_tree); @@ -391,6 +397,12 @@ lbool iz3interpolate(ast_manager &_m_manager, return res; } +void interpolation_options_struct::apply(iz3base &b){ + for(stl_ext::hash_map::iterator it = map.begin(), en = map.end(); + it != en; + ++it) + b.set_option((*it).first,(*it).second); +} diff --git a/src/interp/iz3interp.h b/src/interp/iz3interp.h index 7174205f1..62f967c02 100644 --- a/src/interp/iz3interp.h +++ b/src/interp/iz3interp.h @@ -23,8 +23,15 @@ Revision History: #include "iz3hash.h" #include "solver.h" +class iz3base; + struct interpolation_options_struct { stl_ext::hash_map map; +public: + void set(const std::string &name, const std::string &value){ + map[name] = value; + } + void apply(iz3base &b); }; /** This object is thrown if a tree interpolation problem is mal-formed */ diff --git a/src/muz_qe/dl_context.cpp b/src/muz_qe/dl_context.cpp index 082b44815..ef8168607 100644 --- a/src/muz_qe/dl_context.cpp +++ b/src/muz_qe/dl_context.cpp @@ -1013,13 +1013,15 @@ namespace datalog { } lbool context::query(expr* query) { - new_query(); - rule_set::iterator it = m_rule_set.begin(), end = m_rule_set.end(); - rule_ref r(m_rule_manager); - for (; it != end; ++it) { + if(get_engine() != DUALITY_ENGINE) { + new_query(); + rule_set::iterator it = m_rule_set.begin(), end = m_rule_set.end(); + rule_ref r(m_rule_manager); + for (; it != end; ++it) { r = *it; check_rule(r); - } + } + } switch(get_engine()) { case DATALOG_ENGINE: return rel_query(query); @@ -1259,6 +1261,15 @@ namespace datalog { } } + void context::get_raw_rule_formulas(expr_ref_vector& rules, svector& names){ + for (unsigned i = 0; i < m_rule_fmls.size(); ++i) { + expr_ref r = bind_variables(m_rule_fmls[i].get(), true); + rules.push_back(r.get()); + // rules.push_back(m_rule_fmls[i].get()); + names.push_back(m_rule_names[i]); + } + } + void context::get_rules_as_formulas(expr_ref_vector& rules, svector& names) { expr_ref fml(m); datalog::rule_manager& rm = get_rule_manager(); diff --git a/src/muz_qe/dl_context.h b/src/muz_qe/dl_context.h index c9d0bec77..16295498b 100644 --- a/src/muz_qe/dl_context.h +++ b/src/muz_qe/dl_context.h @@ -238,6 +238,7 @@ namespace datalog { rule_set const & get_rules() { flush_add_rules(); return m_rule_set; } void get_rules_as_formulas(expr_ref_vector& fmls, svector& names); + void get_raw_rule_formulas(expr_ref_vector& fmls, svector& names); void add_fact(app * head); void add_fact(func_decl * pred, const relation_fact & fact); diff --git a/src/muz_qe/duality_dl_interface.cpp b/src/muz_qe/duality_dl_interface.cpp index 6ccaaf52f..ee1eca712 100644 --- a/src/muz_qe/duality_dl_interface.cpp +++ b/src/muz_qe/duality_dl_interface.cpp @@ -119,9 +119,9 @@ void dl_interface::check_reset() { m_ctx.ensure_opened(); expr_ref_vector rules(m_ctx.get_manager()); - svector< ::symbol> names; - - m_ctx.get_rules_as_formulas(rules, names); + svector< ::symbol> names; + // m_ctx.get_rules_as_formulas(rules, names); + m_ctx.get_raw_rule_formulas(rules, names); // get all the rules as clauses std::vector &clauses = _d->clauses; @@ -132,7 +132,7 @@ void dl_interface::check_reset() { } // turn the query into a clause - expr q(_d->ctx,query); + expr q(_d->ctx,m_ctx.bind_variables(query,false)); std::vector b_sorts; std::vector b_names; @@ -146,7 +146,7 @@ void dl_interface::check_reset() { } expr qc = implies(q,_d->ctx.bool_val(false)); - qc = _d->ctx.make_quant(Exists,b_sorts,b_names,qc); + qc = _d->ctx.make_quant(Forall,b_sorts,b_names,qc); clauses.push_back(qc); // get the background axioms