From 180f55bbdaaec6f2eee07c6c973cef2af2558add Mon Sep 17 00:00:00 2001 From: Ken McMillan Date: Tue, 11 Mar 2014 18:20:42 -0700 Subject: [PATCH] adding support for non-extensional arrays in duality --- src/duality/duality.h | 15 +- src/duality/duality_rpfp.cpp | 183 ++++++++++++++++++----- src/duality/duality_solver.cpp | 22 ++- src/duality/duality_wrapper.cpp | 17 ++- src/duality/duality_wrapper.h | 3 + src/muz/base/fixedpoint_params.pyg | 1 + src/muz/duality/duality_dl_interface.cpp | 1 + 7 files changed, 196 insertions(+), 46 deletions(-) diff --git a/src/duality/duality.h b/src/duality/duality.h index 12ba21516..137279899 100755 --- a/src/duality/duality.h +++ b/src/duality/duality.h @@ -31,6 +31,8 @@ using namespace stl_ext; namespace Duality { + class implicant_solver; + /* Generic operations on Z3 formulas */ struct Z3User { @@ -104,6 +106,9 @@ namespace Duality { FuncDecl RenumberPred(const FuncDecl &f, int n); + Term ExtractStores(hash_map &memo, const Term &t, std::vector &cnstrs, hash_map &renaming); + + protected: void SummarizeRec(hash_set &memo, std::vector &lits, int &ops, const Term &t); @@ -602,6 +607,8 @@ protected: void FixCurrentState(Edge *root); void FixCurrentStateFull(Edge *edge, const expr &extra); + + void FixCurrentStateFull(Edge *edge, const std::vector &assumps, const hash_map &renaming); /** Declare a constant in the background theory. */ @@ -944,10 +951,12 @@ protected: Term UnderapproxFormula(const Term &f, hash_set &dont_cares); void ImplicantFullRed(hash_map &memo, const Term &f, std::vector &lits, - hash_set &done, hash_set &dont_cares); + hash_set &done, hash_set &dont_cares, bool extensional = true); - Term UnderapproxFullFormula(const Term &f, hash_set &dont_cares); + public: + Term UnderapproxFullFormula(const Term &f, bool extensional = true); + protected: Term ToRuleRec(Edge *e, hash_map &memo, const Term &t, std::vector &quants); hash_map resolve_ite_memo; @@ -988,6 +997,8 @@ protected: void AddEdgeToSolver(Edge *edge); + void AddEdgeToSolver(implicant_solver &aux_solver, Edge *edge); + void AddToProofCore(hash_set &core); void GetGroundLitsUnderQuants(hash_set *memo, const Term &f, std::vector &res, int under); diff --git a/src/duality/duality_rpfp.cpp b/src/duality/duality_rpfp.cpp index 550f94f2d..2d871c324 100755 --- a/src/duality/duality_rpfp.cpp +++ b/src/duality/duality_rpfp.cpp @@ -410,6 +410,33 @@ namespace Duality { return res; } + Z3User::Term Z3User::ExtractStores(hash_map &memo, const Term &t, std::vector &cnstrs, hash_map &renaming) + { + std::pair foo(t,expr(ctx)); + std::pair::iterator, bool> bar = memo.insert(foo); + Term &res = bar.first->second; + if(!bar.second) return res; + if (t.is_app()) { + func_decl f = t.decl(); + std::vector args; + int nargs = t.num_args(); + for(int i = 0; i < nargs; i++) + args.push_back(ExtractStores(memo, t.arg(i),cnstrs,renaming)); + res = f(args.size(),&args[0]); + if(f.get_decl_kind() == Store){ + func_decl fresh = ctx.fresh_func_decl("@arr", res.get_sort()); + expr y = fresh(); + expr equ = ctx.make(Equal,y,res); + cnstrs.push_back(equ); + renaming[y] = res; + res = y; + } + } + else res = t; + return res; + } + + bool Z3User::IsLiteral(const expr &lit, expr &atom, expr &val){ if(!(lit.is_quantifier() && IsClosedFormula(lit))){ if(!lit.is_app()) @@ -1851,7 +1878,7 @@ namespace Duality { } void RPFP::ImplicantFullRed(hash_map &memo, const Term &f, std::vector &lits, - hash_set &done, hash_set &dont_cares){ + hash_set &done, hash_set &dont_cares, bool extensional){ if(done.find(f) != done.end()) return; /* already processed */ if(f.is_app()){ @@ -1859,7 +1886,7 @@ namespace Duality { decl_kind k = f.decl().get_decl_kind(); if(k == Implies || k == Iff || k == And || k == Or || k == Not){ for(int i = 0; i < nargs; i++) - ImplicantFullRed(memo,f.arg(i),lits,done,dont_cares); + ImplicantFullRed(memo,f.arg(i),lits,done,dont_cares, extensional); goto done; } } @@ -1867,6 +1894,15 @@ namespace Duality { if(dont_cares.find(f) == dont_cares.end()){ int b = SubtermTruth(memo,f); if(b != 0 && b != 1) goto done; + if(f.is_app() && f.decl().get_decl_kind() == Equal && f.arg(0).is_array()){ + if(b == 1 && !extensional){ + expr x = dualModel.eval(f.arg(0)); expr y = dualModel.eval(f.arg(1)); + if(!eq(x,y)) + b = 0; + } + if(b == 0) + goto done; + } expr bv = (b==1) ? f : !f; lits.push_back(bv); } @@ -1988,12 +2024,16 @@ namespace Duality { return conjoin(lits); } - RPFP::Term RPFP::UnderapproxFullFormula(const Term &f, hash_set &dont_cares){ + RPFP::Term RPFP::UnderapproxFullFormula(const Term &f, bool extensional){ + hash_set dont_cares; + resolve_ite_memo.clear(); + timer_start("UnderapproxFormula"); /* first compute truth values of subterms */ hash_map memo; hash_set done; std::vector lits; - ImplicantFullRed(memo,f,lits,done,dont_cares); + ImplicantFullRed(memo,f,lits,done,dont_cares, extensional); + timer_stop("UnderapproxFormula"); /* return conjunction of literals */ return conjoin(lits); } @@ -2538,22 +2578,6 @@ namespace Duality { ConstrainEdgeLocalized(edge,eu); } - void RPFP::FixCurrentStateFull(Edge *edge, const expr &extra){ - hash_set dont_cares; - resolve_ite_memo.clear(); - timer_start("UnderapproxFormula"); - Term dual = edge->dual.null() ? ctx.bool_val(true) : edge->dual; - for(unsigned i = 0; i < edge->constraints.size(); i++) - dual = dual && edge->constraints[i]; - // dual = dual && extra; - Term eu = UnderapproxFullFormula(dual,dont_cares); - timer_stop("UnderapproxFormula"); - ConstrainEdgeLocalized(edge,eu); - } - - - - void RPFP::GetGroundLitsUnderQuants(hash_set *memo, const Term &f, std::vector &res, int under){ if(memo[under].find(f) != memo[under].end()) return; @@ -2836,7 +2860,91 @@ namespace Duality { return ctx.make(And,lits); } - // set up edge constraint in aux solver + + /* This is a wrapper for a solver that is intended to compute + implicants from models. It works around a problem in Z3 with + models in the non-extensional array theory. It does this by + naming all of the store terms in a formula. That is, (store ...) + is replaced by "name" with an added constraint name = (store + ...). This allows us to determine from the model whether an array + equality is true or false (it is false if the two sides are + mapped to different function symbols, even if they have the same + contents). + */ + + struct implicant_solver { + RPFP *owner; + solver &aux_solver; + std::vector assumps, namings; + std::vector assump_stack, naming_stack; + hash_map renaming, renaming_memo; + + void add(const expr &e){ + expr t = e; + if(!aux_solver.extensional_array_theory()){ + unsigned i = namings.size(); + t = owner->ExtractStores(renaming_memo,t,namings,renaming); + for(; i < namings.size(); i++) + aux_solver.add(namings[i]); + } + assumps.push_back(t); + aux_solver.add(t); + } + + void push() { + assump_stack.push_back(assumps.size()); + naming_stack.push_back(namings.size()); + aux_solver.push(); + } + + // When we pop the solver, we have to re-add any namings that were lost + + void pop(int n) { + aux_solver.pop(n); + int new_assumps = assump_stack[assump_stack.size()-n]; + int new_namings = naming_stack[naming_stack.size()-n]; + for(unsigned i = new_namings; i < namings.size(); i++) + aux_solver.add(namings[i]); + assumps.resize(new_assumps); + namings.resize(new_namings); + assump_stack.resize(assump_stack.size()-1); + naming_stack.resize(naming_stack.size()-1); + } + + check_result check() { + return aux_solver.check(); + } + + model get_model() { + return aux_solver.get_model(); + } + + expr get_implicant() { + owner->dualModel = aux_solver.get_model(); + expr dual = owner->ctx.make(And,assumps); + bool ext = aux_solver.extensional_array_theory(); + expr eu = owner->UnderapproxFullFormula(dual,ext); + // if we renamed store terms, we have to undo + if(!ext) + eu = owner->SubstRec(renaming,eu); + return eu; + } + + implicant_solver(RPFP *_owner, solver &_aux_solver) + : owner(_owner), aux_solver(_aux_solver) + {} + }; + + // set up edge constraint in aux solver + void RPFP::AddEdgeToSolver(implicant_solver &aux_solver, Edge *edge){ + if(!edge->dual.null()) + aux_solver.add(edge->dual); + for(unsigned i = 0; i < edge->constraints.size(); i++){ + expr tl = edge->constraints[i]; + aux_solver.add(tl); + } + } + void RPFP::AddEdgeToSolver(Edge *edge){ if(!edge->dual.null()) aux_solver.add(edge->dual); @@ -2853,28 +2961,29 @@ namespace Duality { const std::vector &theory = ls->get_axioms(); for(unsigned i = 0; i < theory.size(); i++) axioms_needed.insert(theory[i]); - aux_solver.push(); - AddEdgeToSolver(node->Outgoing); + implicant_solver is(this,aux_solver); + is.push(); + AddEdgeToSolver(is,node->Outgoing); node->Annotation.SetEmpty(); hash_set *core = new hash_set; core->insert(node->Outgoing->dual); while(1){ - aux_solver.push(); + is.push(); expr annot = !GetAnnotation(node); - aux_solver.add(annot); - if(aux_solver.check() == unsat){ - aux_solver.pop(1); + is.add(annot); + if(is.check() == unsat){ + is.pop(1); break; } - dualModel = aux_solver.get_model(); - aux_solver.pop(1); + is.pop(1); Push(); - FixCurrentStateFull(node->Outgoing,annot); - ConstrainEdgeLocalized(node->Outgoing,!GetAnnotation(node)); + ConstrainEdgeLocalized(node->Outgoing,is.get_implicant()); + ConstrainEdgeLocalized(node->Outgoing,!GetAnnotation(node)); //TODO: need this? check_result foo = Check(root); - if(foo != unsat) + if(foo != unsat){ + slvr().print("should_be_unsat.smt2"); throw "should be unsat"; - + } std::vector assumps, axioms_to_add; slvr().get_proof().get_assumptions(assumps); for(unsigned i = 0; i < assumps.size(); i++){ @@ -2890,7 +2999,7 @@ namespace Duality { { expr itp = GetAnnotation(node); - dualModel = aux_solver.get_model(); + dualModel = is.get_model(); // TODO: what does this mean? std::vector case_lits; itp = StrengthenFormulaByCaseSplitting(itp, case_lits); SetAnnotation(node,itp); @@ -2898,14 +3007,14 @@ namespace Duality { } for(unsigned i = 0; i < axioms_to_add.size(); i++) - aux_solver.add(axioms_to_add[i]); + is.add(axioms_to_add[i]); if(node->Annotation.IsEmpty()){ if(!axioms_added){ // add the axioms in the off chance they are useful const std::vector &theory = ls->get_axioms(); for(unsigned i = 0; i < theory.size(); i++) - aux_solver.add(theory[i]); + is.add(theory[i]); axioms_added = true; } else { @@ -2923,7 +3032,7 @@ namespace Duality { if(proof_core) delete proof_core; // shouldn't happen proof_core = core; - aux_solver.pop(1); + is.pop(1); timer_stop("InterpolateByCases"); } diff --git a/src/duality/duality_solver.cpp b/src/duality/duality_solver.cpp index c7eec7e9f..3c69d79c0 100755 --- a/src/duality/duality_solver.cpp +++ b/src/duality/duality_solver.cpp @@ -131,6 +131,7 @@ namespace Duality { Report = false; StratifiedInlining = false; RecursionBound = -1; + BatchExpand = false; { scoped_no_proof no_proofs_please(ctx.m()); #ifdef USE_RPFP_CLONE @@ -365,6 +366,7 @@ namespace Duality { bool Report; // spew on stdout bool StratifiedInlining; // Do stratified inlining as preprocessing step int RecursionBound; // Recursion bound for bounded verification + bool BatchExpand; bool SetBoolOption(bool &opt, const std::string &value){ if(value == "0") { @@ -403,6 +405,9 @@ namespace Duality { if(option == "stratified_inlining"){ return SetBoolOption(StratifiedInlining,value); } + if(option == "batch_expand"){ + return SetBoolOption(BatchExpand,value); + } if(option == "recursion_bound"){ return SetIntOption(RecursionBound,value); } @@ -2016,7 +2021,7 @@ namespace Duality { } else { was_sat = true; - tree->Push(); + tree->Push(); std::vector &expansions = stack.back().expansions; #ifndef NO_DECISIONS for(unsigned i = 0; i < expansions.size(); i++){ @@ -2027,11 +2032,16 @@ namespace Duality { if(tree->slvr().check() == unsat) throw "help!"; #endif - stack.push_back(stack_entry()); - stack.back().level = tree->slvr().get_scope_level(); - if(ExpandSomeNodes(false,1)){ - continue; + int expand_max = 1; + if(0&&duality->BatchExpand){ + int thing = stack.size() * 0.1; + expand_max = std::max(1,thing); + if(expand_max > 1) + std::cout << "foo!\n"; } + + if(ExpandSomeNodes(false,expand_max)) + continue; while(stack.size() > 1){ tree->Pop(1); stack.pop_back(); @@ -2090,6 +2100,8 @@ namespace Duality { std::list updated_nodes; virtual void ExpandNode(RPFP::Node *p){ + stack.push_back(stack_entry()); + stack.back().level = tree->slvr().get_scope_level(); stack.back().expansions.push_back(p); DerivationTree::ExpandNode(p); std::vector &new_nodes = p->Outgoing->Children; diff --git a/src/duality/duality_wrapper.cpp b/src/duality/duality_wrapper.cpp index 345fef562..0f6198edd 100755 --- a/src/duality/duality_wrapper.cpp +++ b/src/duality/duality_wrapper.cpp @@ -37,7 +37,7 @@ Revision History: namespace Duality { - solver::solver(Duality::context& c, bool extensional, bool models) : object(c), the_model(c) { + solver::solver(Duality::context& c, bool _extensional, bool models) : object(c), the_model(c) { params_ref p; p.set_bool("proof", true); // this is currently useless if(models) @@ -47,7 +47,8 @@ namespace Duality { p.set_bool("mbqi",mbqi); // just to test p.set_str("mbqi.id","itp"); // use mbqi for quantifiers in interpolants p.set_uint("mbqi.max_iterations",1); // use mbqi for quantifiers in interpolants - if(true || extensional) + extensional = mbqi && (true || _extensional); + if(extensional) p.set_bool("array.extensional",true); scoped_ptr sf = mk_smt_solver_factory(); m_solver = (*sf)(m(), p, true, true, true, ::symbol::null); @@ -657,6 +658,18 @@ expr context::make_quant(decl_kind op, const std::vector &_sorts, const st pp.display_smt2(std::cout, m_solver->get_assertion(n-1)); } + void solver::print(const char *filename) { + std::ofstream f(filename); + unsigned n = m_solver->get_num_assertions(); + if(!n) + return; + ast_smt_pp pp(m()); + for (unsigned i = 0; i < n-1; ++i) + pp.add_assumption(m_solver->get_assertion(i)); + pp.display_smt2(f, m_solver->get_assertion(n-1)); + } + + void solver::show_assertion_ids() { #if 0 unsigned n = m_solver->get_num_assertions(); diff --git a/src/duality/duality_wrapper.h b/src/duality/duality_wrapper.h index febc3f1f1..ccc0800b2 100755 --- a/src/duality/duality_wrapper.h +++ b/src/duality/duality_wrapper.h @@ -819,6 +819,7 @@ namespace Duality { model the_model; bool canceled; proof_gen_mode m_mode; + bool extensional; public: solver(context & c, bool extensional = false, bool models = true); solver(context & c, ::solver *s):object(c),the_model(c) { m_solver = s; canceled = false;} @@ -922,6 +923,7 @@ namespace Duality { unsigned get_scope_level(){ scoped_proof_mode spm(m(),m_mode); return m_solver->get_scope_level();} void show(); + void print(const char *filename); void show_assertion_ids(); proof get_proof(){ @@ -929,6 +931,7 @@ namespace Duality { return proof(ctx(),m_solver->get_proof()); } + bool extensional_array_theory() {return extensional;} }; #if 0 diff --git a/src/muz/base/fixedpoint_params.pyg b/src/muz/base/fixedpoint_params.pyg index 5eec77f39..e201c2a19 100644 --- a/src/muz/base/fixedpoint_params.pyg +++ b/src/muz/base/fixedpoint_params.pyg @@ -75,6 +75,7 @@ def_module_params('fixedpoint', ('recursion_bound', UINT, UINT_MAX, 'DUALITY: Recursion bound for stratified inlining'), ('profile', BOOL, False, 'DUALITY: profile run time'), ('mbqi', BOOL, True, 'DUALITY: use model-based quantifier instantion'), + ('batch_expand', BOOL, False, 'DUALITY: use batch expansion'), ('dump_aig', SYMBOL, '', 'Dump clauses in AIG text format (AAG) to the given file name'), )) diff --git a/src/muz/duality/duality_dl_interface.cpp b/src/muz/duality/duality_dl_interface.cpp index e7c7976f6..0c2a9e48a 100755 --- a/src/muz/duality/duality_dl_interface.cpp +++ b/src/muz/duality/duality_dl_interface.cpp @@ -205,6 +205,7 @@ lbool dl_interface::query(::expr * query) { 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"); + rs->SetOption("batch_expand",m_ctx.get_params().batch_expand() ? "1" : "0"); unsigned rb = m_ctx.get_params().recursion_bound(); if(rb != UINT_MAX){ std::ostringstream os; os << rb;