From 9d611997b3057df4d72f4279ea8df54ccd8174f2 Mon Sep 17 00:00:00 2001 From: Ken McMillan Date: Wed, 22 May 2013 15:18:50 -0700 Subject: [PATCH] fixing labels in duality --- src/duality/duality.h | 8 ++- src/duality/duality_rpfp.cpp | 101 ++++++++++++++++++++++++++-- src/duality/duality_wrapper.cpp | 11 +-- src/muz_qe/duality_dl_interface.cpp | 16 ++--- 4 files changed, 114 insertions(+), 22 deletions(-) diff --git a/src/duality/duality.h b/src/duality/duality.h index 033cea660..0a580a463 100644 --- a/src/duality/duality.h +++ b/src/duality/duality.h @@ -434,6 +434,7 @@ namespace Duality { hash_map relMap; hash_map varMap; Edge *map; + Term labeled; Edge(Node *_Parent, const Transformer &_F, const std::vector &_Children, RPFP *_owner, int _number) : F(_F), Parent(_Parent), Children(_Children), dual(expr(_owner->ctx)) { @@ -634,8 +635,7 @@ namespace Duality { #ifdef WIN32 __declspec(dllexport) #endif - void FromClauses(const std::vector &clauses, - std::vector > &clause_labels); + void FromClauses(const std::vector &clauses); void FromFixpointContext(fixedpoint fp, std::vector &queries); @@ -674,6 +674,10 @@ namespace Duality { int EvalTruth(hash_map &memo, Edge *e, const Term &f); + void GetLabels(Edge *e, std::vector &labels); + + int GetLabelsRec(hash_map *memo, const Term &f, std::vector &labels, bool labpos); + private: diff --git a/src/duality/duality_rpfp.cpp b/src/duality/duality_rpfp.cpp index 13752401b..334e0a056 100644 --- a/src/duality/duality_rpfp.cpp +++ b/src/duality/duality_rpfp.cpp @@ -838,6 +838,95 @@ namespace Duality { return SubtermTruth(memo,tl); } + /** Compute truth values of all boolean subterms in current model. + Assumes formulas has been simplified by Z3, so only boolean ops + ands and, or, not. Returns result in memo. + */ + + int RPFP::GetLabelsRec(hash_map *memo, const Term &f, std::vector &labels, bool labpos){ + if(memo[labpos].find(f) != memo[labpos].end()){ + return memo[labpos][f]; + } + int res; + if(f.is_app()){ + int nargs = f.num_args(); + decl_kind k = f.decl().get_decl_kind(); + if(k == Implies){ + res = GetLabelsRec(memo,!f.arg(0) || f.arg(1), labels, labpos); + goto done; + } + if(k == And) { + res = 1; + for(int i = 0; i < nargs; i++){ + int ar = GetLabelsRec(memo,f.arg(i), labels, labpos); + if(ar == 0){ + res = 0; + goto done; + } + if(ar == 2)res = 2; + } + goto done; + } + else if(k == Or) { + res = 0; + for(int i = 0; i < nargs; i++){ + int ar = GetLabelsRec(memo,f.arg(i), labels, labpos); + if(ar == 1){ + res = 1; + goto done; + } + if(ar == 2)res = 2; + } + goto done; + } + else if(k == Not) { + int ar = GetLabelsRec(memo,f.arg(0), labels, !labpos); + res = (ar == 0) ? 1 : ((ar == 1) ? 0 : 2); + goto done; + } + } + { + bool pos; std::vector names; + if(f.is_label(pos,names)){ + res = GetLabelsRec(memo,f.arg(0), labels, labpos); + if(pos == labpos && res == (pos ? 1 : 0)) + for(unsigned i = 0; i < names.size(); i++) + labels.push_back(names[i]); + goto done; + } + } + { + expr bv = dualModel.eval(f); + if(bv.is_app() && bv.decl().get_decl_kind() == Equal && + bv.arg(0).is_array()){ + bv = EvalArrayEquality(bv); + } + // Hack!!!! array equalities can occur negatively! + if(bv.is_app() && bv.decl().get_decl_kind() == Not && + bv.arg(0).decl().get_decl_kind() == Equal && + bv.arg(0).arg(0).is_array()){ + bv = dualModel.eval(!EvalArrayEquality(bv.arg(0))); + } + if(eq(bv,ctx.bool_val(true))) + res = 1; + else if(eq(bv,ctx.bool_val(false))) + res = 0; + else + res = 2; + } + done: + memo[labpos][f] = res; + return res; + } + + void RPFP::GetLabels(Edge *e, std::vector &labels){ + if(!e->map || e->map->labeled.null()) + return; + Term tl = Localize(e, e->map->labeled); + hash_map memo[2]; + GetLabelsRec(memo,tl,labels,true); + } + #ifdef Z3OPS static Z3_subterm_truth *stt; #endif @@ -1742,8 +1831,7 @@ namespace Duality { arg.decl().get_decl_kind() == Uninterpreted); } - void RPFP::FromClauses(const std::vector &unskolemized_clauses, - std::vector > &clause_labels){ + void RPFP::FromClauses(const std::vector &unskolemized_clauses){ hash_map pmap; func_decl fail_pred = ctx.fresh_func_decl("@Fail", ctx.bool_sort()); @@ -1810,7 +1898,6 @@ namespace Duality { // create the edges - clause_labels.resize(clauses.size()); for(unsigned i = 0; i < clauses.size(); i++){ Term clause = clauses[i]; Term body = clause.arg(0); @@ -1841,13 +1928,15 @@ namespace Duality { hash_map scan_memo; std::vector Children; body = ScanBody(scan_memo,body,pmap,Relparams,Children); - body = RemoveLabels(body,clause_labels[i]); + Term labeled = body; + std::vector lbls; // TODO: throw this away for now + body = RemoveLabels(body,lbls); body = body.simplify(); // Create the edge Transformer T = CreateTransformer(Relparams,Indparams,body); - // Edge *edge = - CreateEdge(Parent,T,Children); + Edge *edge = CreateEdge(Parent,T,Children); + edge->labeled = labeled;; // remember for label extraction // edges.push_back(edge); } } diff --git a/src/duality/duality_wrapper.cpp b/src/duality/duality_wrapper.cpp index bed347ef4..9ac3ec53e 100644 --- a/src/duality/duality_wrapper.cpp +++ b/src/duality/duality_wrapper.cpp @@ -25,6 +25,7 @@ Revision History: #include "statistics.h" #include "expr_abstract.h" #include "stopwatch.h" +#include "model_smt2_pp.h" namespace Duality { @@ -534,18 +535,20 @@ expr context::make_quant(decl_kind op, const std::vector &_sorts, const st std::cout << mk_pp(raw(), m()) << std::endl; } -#if 0 void model::show() const { - std::cout << Z3_model_to_string(ctx(), m_model) << std::endl; + model_smt2_pp(std::cout, m(), *m_model, 0); + std::cout << std::endl; } - Z3_ast ast_to_track = 0; -#endif void include_ast_show(ast &a){ a.show(); } + void include_model_show(model &a){ + a.show(); + } + bool expr::is_label (bool &pos,std::vector &names) const { buffer< ::symbol> _names; bool res = m().is_label(to_expr(raw()),pos,_names); diff --git a/src/muz_qe/duality_dl_interface.cpp b/src/muz_qe/duality_dl_interface.cpp index e2ee25a2f..e57ba5826 100644 --- a/src/muz_qe/duality_dl_interface.cpp +++ b/src/muz_qe/duality_dl_interface.cpp @@ -161,7 +161,7 @@ void dl_interface::check_reset() { } // creates 1-1 map between clauses and rpfp edges - _d->rpfp->FromClauses(clauses,_d->clause_labels); + _d->rpfp->FromClauses(clauses); // populate the edge-to-clause map for(unsigned i = 0; i < _d->rpfp->edges.size(); ++i) @@ -265,16 +265,12 @@ static void print_proof(dl_interface *d, std::ostream& out, Solver::Counterexamp out << " )\n"; out << " (labels"; - std::vector &labels = d->dd()->clause_labels[orig_clause]; - { - hash_map memo; - for(unsigned j = 0; j < labels.size(); j++){ - RPFP::label_struct &lab = labels[j]; - int truth = cex.tree->EvalTruth(memo,&edge,lab.value); - if(truth == 1 && lab.pos || truth == 0 && !lab.pos) - out << " " << lab.name; - } + std::vector labels; + cex.tree->GetLabels(&edge,labels); + for(unsigned j = 0; j < labels.size(); j++){ + out << " " << labels[j]; } + out << " )\n"; // reference the proofs of all the children, in syntactic order