From 8320144af00269061870a058bfdd7b6c7d3b29ac Mon Sep 17 00:00:00 2001 From: Ken McMillan Date: Fri, 15 Nov 2013 11:24:02 -0800 Subject: [PATCH 01/21] fixed bug in duality logging --- src/duality/duality_rpfp.cpp | 18 ++++++++++-------- 1 file changed, 10 insertions(+), 8 deletions(-) diff --git a/src/duality/duality_rpfp.cpp b/src/duality/duality_rpfp.cpp index 1c2927da8..fe5ad8672 100644 --- a/src/duality/duality_rpfp.cpp +++ b/src/duality/duality_rpfp.cpp @@ -89,15 +89,17 @@ namespace Duality { if(memo.find(t) != memo.end()) return; memo.insert(t); - decl_kind k = t.decl().get_decl_kind(); - if(k == And || k == Or || k == Not || k == Implies || k == Iff){ - ops++; - int nargs = t.num_args(); - for(int i = 0; i < nargs; i++) - SummarizeRec(memo,lits,ops,t.arg(i)); + if(t.is_app()){ + decl_kind k = t.decl().get_decl_kind(); + if(k == And || k == Or || k == Not || k == Implies || k == Iff){ + ops++; + int nargs = t.num_args(); + for(int i = 0; i < nargs; i++) + SummarizeRec(memo,lits,ops,t.arg(i)); + return; + } } - else - lits.push_back(t); + lits.push_back(t); } int Z3User::CumulativeDecisions(){ From a93f8b04e56235531e46cfbdb5df1df128ed6122 Mon Sep 17 00:00:00 2001 From: Ken McMillan Date: Thu, 21 Nov 2013 18:10:21 -0800 Subject: [PATCH 02/21] working on duality and quantified arithmetic in interpolation --- src/duality/duality.h | 75 ++++++- src/duality/duality_rpfp.cpp | 129 ++++++++++-- src/duality/duality_solver.cpp | 208 +++++++++++++++++- src/duality/duality_wrapper.cpp | 19 +- src/duality/duality_wrapper.h | 8 + src/interp/iz3interp.cpp | 62 +++++- src/interp/iz3interp.h | 10 + src/interp/iz3mgr.cpp | 16 ++ src/interp/iz3mgr.h | 3 + src/interp/iz3proof_itp.cpp | 359 ++++++++++++++++++++++++++++++-- 10 files changed, 829 insertions(+), 60 deletions(-) diff --git a/src/duality/duality.h b/src/duality/duality.h index 166e8ef0d..158ad84d9 100644 --- a/src/duality/duality.h +++ b/src/duality/duality.h @@ -277,6 +277,7 @@ namespace Duality { public: std::list edges; std::list nodes; + std::list constraints; }; @@ -286,6 +287,8 @@ namespace Duality { literals dualLabels; std::list stack; std::vector axioms; // only saved here for printing purposes + solver aux_solver; + public: @@ -296,7 +299,7 @@ namespace Duality { inherit the axioms. */ - RPFP(LogicSolver *_ls) : Z3User(*(_ls->ctx), *(_ls->slvr)), dualModel(*(_ls->ctx)) + RPFP(LogicSolver *_ls) : Z3User(*(_ls->ctx), *(_ls->slvr)), dualModel(*(_ls->ctx)), aux_solver(*(_ls->ctx)) { ls = _ls; nodeCount = 0; @@ -351,10 +354,10 @@ namespace Duality { bool SubsetEq(const Transformer &other){ Term t = owner->SubstParams(other.IndParams,IndParams,other.Formula); expr test = Formula && !t; - owner->slvr.push(); - owner->slvr.add(test); - check_result res = owner->slvr.check(); - owner->slvr.pop(1); + owner->aux_solver.push(); + owner->aux_solver.add(test); + check_result res = owner->aux_solver.check(); + owner->aux_solver.pop(1); return res == unsat; } @@ -444,6 +447,19 @@ namespace Duality { return n; } + /** Delete a node. You can only do this if not connected to any edges.*/ + void DeleteNode(Node *node){ + if(node->Outgoing || !node->Incoming.empty()) + throw "cannot delete RPFP node"; + for(std::vector::iterator it = nodes.end(), en = nodes.begin(); it != en;){ + if(*(--it) == node){ + nodes.erase(it); + break; + } + } + delete node; + } + /** This class represents a hyper-edge in the RPFP graph */ class Edge @@ -460,6 +476,7 @@ namespace Duality { hash_map varMap; Edge *map; Term labeled; + std::vector constraints; Edge(Node *_Parent, const Transformer &_F, const std::vector &_Children, RPFP *_owner, int _number) : F(_F), Parent(_Parent), Children(_Children), dual(expr(_owner->ctx)) { @@ -480,6 +497,29 @@ namespace Duality { return e; } + + /** Delete a hyper-edge and unlink it from any nodes. */ + void DeleteEdge(Edge *edge){ + if(edge->Parent) + edge->Parent->Outgoing = 0; + for(unsigned int i = 0; i < edge->Children.size(); i++){ + std::vector &ic = edge->Children[i]->Incoming; + for(std::vector::iterator it = ic.begin(), en = ic.end(); it != en; ++it){ + if(*it == edge){ + ic.erase(it); + break; + } + } + } + for(std::vector::iterator it = edges.end(), en = edges.begin(); it != en;){ + if(*(--it) == edge){ + edges.erase(it); + break; + } + } + delete edge; + } + /** Create an edge that lower-bounds its parent. */ Edge *CreateLowerBoundEdge(Node *_Parent) { @@ -494,13 +534,25 @@ namespace Duality { void AssertEdge(Edge *e, int persist = 0, bool with_children = false, bool underapprox = false); - + /* Constrain an edge by the annotation of one of its children. */ + + void ConstrainParent(Edge *parent, Node *child); + /** For incremental solving, asserts the negation of the upper bound associated * with a node. * */ void AssertNode(Node *n); + /** Assert a constraint on an edge in the SMT context. + */ + void ConstrainEdge(Edge *e, const Term &t); + + /** Fix the truth values of atomic propositions in the given + edge to their values in the current assignment. */ + void FixCurrentState(Edge *root); + + /** Declare a constant in the background theory. */ void DeclareConstant(const FuncDecl &f); @@ -592,6 +644,9 @@ namespace Duality { Term ComputeUnderapprox(Node *root, int persist); + /** Try to strengthen the annotation of a node by removing disjuncts. */ + void Generalize(Node *node); + /** Push a scope. Assertions made after Push can be undone by Pop. */ void Push(); @@ -803,7 +858,15 @@ namespace Duality { Term SubstBound(hash_map &subst, const Term &t); + void ConstrainEdgeLocalized(Edge *e, const Term &t); + void GreedyReduce(solver &s, std::vector &conjuncts); + + void NegateLits(std::vector &lits); + + expr SimplifyOr(std::vector &lits); + + void SetAnnotation(Node *root, const expr &t); }; /** RPFP solver base class. */ diff --git a/src/duality/duality_rpfp.cpp b/src/duality/duality_rpfp.cpp index fe5ad8672..17e3de6bb 100644 --- a/src/duality/duality_rpfp.cpp +++ b/src/duality/duality_rpfp.cpp @@ -283,7 +283,10 @@ namespace Duality { children[i] = ToTermTree(e->Children[i]); // Term top = ReducedDualEdge(e); Term top = e->dual.null() ? ctx.bool_val(true) : e->dual; - return new TermTree(top, children); + TermTree *res = new TermTree(top, children); + for(unsigned i = 0; i < e->constraints.size(); i++) + res->addTerm(e->constraints[i]); + return res; } TermTree *RPFP::GetGoalTree(Node *root){ @@ -375,6 +378,19 @@ namespace Duality { x = x && y; } + void RPFP::SetAnnotation(Node *root, const expr &t){ + hash_map memo; + Term b; + std::vector v; + RedVars(root, b, v); + memo[b] = ctx.bool_val(true); + for (unsigned i = 0; i < v.size(); i++) + memo[v[i]] = root->Annotation.IndParams[i]; + Term annot = SubstRec(memo, t); + // Strengthen(ref root.Annotation.Formula, annot); + root->Annotation.Formula = annot; + } + void RPFP::DecodeTree(Node *root, TermTree *interp, int persist) { std::vector &ic = interp->getChildren(); @@ -384,16 +400,7 @@ namespace Duality { for (unsigned i = 0; i < nc.size(); i++) DecodeTree(nc[i], ic[i], persist); } - hash_map memo; - Term b; - std::vector v; - RedVars(root, b, v); - memo[b] = ctx.bool_val(true); - for (unsigned i = 0; i < v.size(); i++) - memo[v[i]] = root->Annotation.IndParams[i]; - Term annot = SubstRec(memo, interp->getTerm()); - // Strengthen(ref root.Annotation.Formula, annot); - root->Annotation.Formula = annot; + SetAnnotation(root,interp->getTerm()); #if 0 if(persist != 0) Z3_persist_ast(ctx,root->Annotation.Formula,persist); @@ -511,6 +518,10 @@ namespace Duality { timer_stop("solver add"); } + void RPFP::ConstrainParent(Edge *parent, Node *child){ + ConstrainEdgeLocalized(parent,GetAnnotation(child)); + } + /** For incremental solving, asserts the negation of the upper bound associated * with a node. @@ -526,6 +537,24 @@ namespace Duality { } } + /** Assert a constraint on an edge in the SMT context. + */ + + void RPFP::ConstrainEdge(Edge *e, const Term &t) + { + Term tl = Localize(e, t); + ConstrainEdgeLocalized(e,tl); + } + + void RPFP::ConstrainEdgeLocalized(Edge *e, const Term &tl) + { + e->constraints.push_back(tl); + stack.back().constraints.push_back(e); + slvr.add(tl); + } + + + /** Declare a constant in the background theory. */ void RPFP::DeclareConstant(const FuncDecl &f){ @@ -1064,7 +1093,7 @@ namespace Duality { } } /* Unreachable! */ - throw "error in RPFP::ImplicantRed"; + std::cerr << "error in RPFP::ImplicantRed"; goto done; } else if(k == Not) { @@ -1671,6 +1700,17 @@ namespace Duality { return eu; } + void RPFP::FixCurrentState(Edge *edge){ + hash_set dont_cares; + resolve_ite_memo.clear(); + timer_start("UnderapproxFormula"); + Term dual = edge->dual.null() ? ctx.bool_val(true) : edge->dual; + Term eu = UnderapproxFormula(dual,dont_cares); + timer_stop("UnderapproxFormula"); + ConstrainEdgeLocalized(edge,eu); + } + + RPFP::Term RPFP::ModelValueAsConstraint(const Term &t){ if(t.is_array()){ @@ -1714,6 +1754,69 @@ namespace Duality { res = CreateRelation(p->Annotation.IndParams,funder); } + void RPFP::GreedyReduce(solver &s, std::vector &conjuncts){ + // verify + s.push(); + expr conj = ctx.make(And,conjuncts); + s.add(conj); + check_result res = s.check(); + s.pop(1); + if(res != unsat) + throw "should be unsat"; + + for(unsigned i = 0; i < conjuncts.size(); ){ + std::swap(conjuncts[i],conjuncts.back()); + expr save = conjuncts.back(); + conjuncts.pop_back(); + s.push(); + expr conj = ctx.make(And,conjuncts); + s.add(conj); + check_result res = s.check(); + s.pop(1); + if(res != unsat){ + conjuncts.push_back(save); + std::swap(conjuncts[i],conjuncts.back()); + i++; + } + } + } + + void RPFP::NegateLits(std::vector &lits){ + for(unsigned i = 0; i < lits.size(); i++){ + expr &f = lits[i]; + if(f.is_app() && f.decl().get_decl_kind() == Not) + f = f.arg(0); + else + f = !f; + } + } + + expr RPFP::SimplifyOr(std::vector &lits){ + if(lits.size() == 0) + return ctx.bool_val(false); + if(lits.size() == 1) + return lits[0]; + return ctx.make(Or,lits); + } + + void RPFP::Generalize(Node *node){ + std::vector conjuncts; + expr fmla = GetAnnotation(node); + CollectConjuncts(fmla,conjuncts,false); + // try to remove conjuncts one at a tme + aux_solver.push(); + Edge *edge = node->Outgoing; + 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); + } + GreedyReduce(aux_solver,conjuncts); + aux_solver.pop(1); + NegateLits(conjuncts); + SetAnnotation(node,SimplifyOr(conjuncts)); + } /** Push a scope. Assertions made after Push can be undone by Pop. */ @@ -1735,6 +1838,8 @@ namespace Duality { (*it)->dual = expr(ctx,NULL); for(std::list::iterator it = back.nodes.begin(), en = back.nodes.end(); it != en; ++it) (*it)->dual = expr(ctx,NULL); + for(std::list::iterator it = back.constraints.begin(), en = back.constraints.end(); it != en; ++it) + (*it)->constraints.pop_back(); stack.pop_back(); } } diff --git a/src/duality/duality_solver.cpp b/src/duality/duality_solver.cpp index 0043998d2..afa1c7683 100644 --- a/src/duality/duality_solver.cpp +++ b/src/duality/duality_solver.cpp @@ -1270,18 +1270,24 @@ namespace Duality { } } + bool UpdateNodeToNode(Node *node, Node *top){ + if(!node->Annotation.SubsetEq(top->Annotation)){ + reporter->Update(node,top->Annotation); + indset->Update(node,top->Annotation); + updated_nodes.insert(node->map); + node->Annotation.IntersectWith(top->Annotation); + return true; + } + return false; + } + /** Update the unwinding solution, using an interpolant for the derivation tree. */ void UpdateWithInterpolant(Node *node, RPFP *tree, Node *top){ if(top->Outgoing) for(unsigned i = 0; i < top->Outgoing->Children.size(); i++) UpdateWithInterpolant(node->Outgoing->Children[i],tree,top->Outgoing->Children[i]); - if(!node->Annotation.SubsetEq(top->Annotation)){ - reporter->Update(node,top->Annotation); - indset->Update(node,top->Annotation); - updated_nodes.insert(node->map); - node->Annotation.IntersectWith(top->Annotation); - } + UpdateNodeToNode(node, top); heuristic->Update(node); } @@ -1305,7 +1311,8 @@ namespace Duality { if(node->Bound.IsFull()) return true; reporter->Bound(node); int start_decs = rpfp->CumulativeDecisions(); - DerivationTree dt(this,unwinding,reporter,heuristic,FullExpand); + DerivationTree *dtp = new DerivationTreeSlow(this,unwinding,reporter,heuristic,FullExpand); + DerivationTree &dt = *dtp; bool res = dt.Derive(unwinding,node,UseUnderapprox); int end_decs = rpfp->CumulativeDecisions(); // std::cout << "decisions: " << (end_decs - start_decs) << std::endl; @@ -1321,6 +1328,7 @@ namespace Duality { UpdateWithInterpolant(node,dt.tree,dt.top); delete dt.tree; } + delete dtp; return !res; } @@ -1491,7 +1499,7 @@ namespace Duality { return res != unsat; } - bool Build(){ + virtual bool Build(){ #ifdef EFFORT_BOUNDED_STRAT start_decs = tree->CumulativeDecisions(); #endif @@ -1545,7 +1553,7 @@ namespace Duality { } } - void ExpandNode(RPFP::Node *p){ + virtual void ExpandNode(RPFP::Node *p){ // tree->RemoveEdge(p->Outgoing); Edge *edge = duality->GetNodeOutgoing(p->map,last_decs); std::vector &cs = edge->Children; @@ -1573,6 +1581,7 @@ namespace Duality { } #else #if 0 + void ExpansionChoices(std::set &best){ std::vector unused_set, used_set; std::set choices; @@ -1668,7 +1677,7 @@ namespace Duality { #endif #endif - bool ExpandSomeNodes(bool high_priority = false){ + bool ExpandSomeNodes(bool high_priority = false, int max = INT_MAX){ #ifdef EFFORT_BOUNDED_STRAT last_decs = tree->CumulativeDecisions() - start_decs; #endif @@ -1679,17 +1688,194 @@ namespace Duality { timer_stop("ExpansionChoices"); std::list leaves_copy = leaves; // copy so can modify orig leaves.clear(); + int count = 0; for(std::list::iterator it = leaves_copy.begin(), en = leaves_copy.end(); it != en; ++it){ - if(choices.find(*it) != choices.end()) + if(choices.find(*it) != choices.end() && count < max){ + count++; ExpandNode(*it); + } else leaves.push_back(*it); } timer_stop("ExpandSomeNodes"); return !choices.empty(); } + void RemoveExpansion(RPFP::Node *p){ + Edge *edge = p->Outgoing; + Node *parent = edge->Parent; + std::vector cs = edge->Children; + tree->DeleteEdge(edge); + for(unsigned i = 0; i < cs.size(); i++) + tree->DeleteNode(cs[i]); + leaves.push_back(parent); + } }; + class DerivationTreeSlow : public DerivationTree { + public: + + struct stack_entry { + unsigned level; // SMT solver stack level + std::vector expansions; + }; + + std::vector stack; + + hash_map updates; + + DerivationTreeSlow(Duality *_duality, RPFP *rpfp, Reporter *_reporter, Heuristic *_heuristic, bool _full_expand) + : DerivationTree(_duality, rpfp, _reporter, _heuristic, _full_expand) { + stack.push_back(stack_entry()); + } + + virtual bool Build(){ + + stack.back().level = tree->slvr.get_scope_level(); + + while (true) + { + lbool res; + + unsigned slvr_level = tree->slvr.get_scope_level(); + if(slvr_level != stack.back().level) + throw "stacks out of sync!"; + + res = tree->Solve(top, 1); // incremental solve, keep interpolants for one pop + + if (res == l_false) { + if (stack.empty()) // should never happen + return false; + + std::vector &expansions = stack.back().expansions; + int update_count = 0; + for(unsigned i = 0; i < expansions.size(); i++){ + tree->Generalize(expansions[i]); + if(RecordUpdate(expansions[i])) + update_count++; + } + if(update_count == 0) + std::cout << "backtracked without learning\n"; + tree->Pop(1); + hash_set leaves_to_remove; + for(unsigned i = 0; i < expansions.size(); i++){ + Node *node = expansions[i]; + // if(node != top) + // tree->ConstrainParent(node->Incoming[0],node); + std::vector &cs = node->Outgoing->Children; + for(unsigned i = 0; i < cs.size(); i++){ + leaves_to_remove.insert(cs[i]); + UnmapNode(cs[i]); + if(std::find(updated_nodes.begin(),updated_nodes.end(),cs[i]) != updated_nodes.end()) + throw "help!"; + } + RemoveExpansion(node); + } + RemoveLeaves(leaves_to_remove); + stack.pop_back(); + HandleUpdatedNodes(); + if(stack.size() == 1) + return false; + } + else { + tree->Push(); + std::vector &expansions = stack.back().expansions; + for(unsigned i = 0; i < expansions.size(); i++){ + tree->FixCurrentState(expansions[i]->Outgoing); + } + if(tree->slvr.check() == unsat) + throw "help!"; + stack.push_back(stack_entry()); + stack.back().level = tree->slvr.get_scope_level(); + if(ExpandSomeNodes(false,1)){ + continue; + } + while(stack.size() > 1){ + tree->Pop(1); + stack.pop_back(); + } + return true; + } + } + } + + void RemoveLeaves(hash_set &leaves_to_remove){ + std::list leaves_copy; + leaves_copy.swap(leaves); + for(std::list::iterator it = leaves_copy.begin(), en = leaves_copy.end(); it != en; ++it){ + if(leaves_to_remove.find(*it) == leaves_to_remove.end()) + leaves.push_back(*it); + } + } + + hash_map > node_map; + std::list updated_nodes; + + virtual void ExpandNode(RPFP::Node *p){ + stack.back().expansions.push_back(p); + DerivationTree::ExpandNode(p); + std::vector &new_nodes = p->Outgoing->Children; + for(unsigned i = 0; i < new_nodes.size(); i++){ + Node *n = new_nodes[i]; + node_map[n->map].push_back(n); + } + } + + bool RecordUpdate(Node *node){ + bool res = duality->UpdateNodeToNode(node->map,node); + if(res){ + std::vector to_update = node_map[node->map]; + for(unsigned i = 0; i < to_update.size(); i++){ + Node *node2 = to_update[i]; + // maintain invariant that no nodes on updated list are created at current stack level + if(node2 == node || !(node->Incoming.size() > 0 && AtCurrentStackLevel(node2->Incoming[0]->Parent))){ + updated_nodes.push_back(node2); + if(node2 != node) + node2->Annotation = node->Annotation; + } + } + } + return res; + } + + void HandleUpdatedNodes(){ + for(std::list::iterator it = updated_nodes.begin(), en = updated_nodes.end(); it != en;){ + Node *node = *it; + node->Annotation = node->map->Annotation; + if(node->Incoming.size() > 0) + tree->ConstrainParent(node->Incoming[0],node); + if(AtCurrentStackLevel(node->Incoming[0]->Parent)){ + std::list::iterator victim = it; + ++it; + updated_nodes.erase(victim); + } + else + ++it; + } + } + + bool AtCurrentStackLevel(Node *node){ + std::vector vec = stack.back().expansions; + for(unsigned i = 0; i < vec.size(); i++) + if(vec[i] == node) + return true; + return false; + } + + void UnmapNode(Node *node){ + std::vector &vec = node_map[node->map]; + for(unsigned i = 0; i < vec.size(); i++){ + if(vec[i] == node){ + std::swap(vec[i],vec.back()); + vec.pop_back(); + return; + } + } + throw "can't unmap node"; + } + + }; + + class Covering { struct cover_info { diff --git a/src/duality/duality_wrapper.cpp b/src/duality/duality_wrapper.cpp index fef70e031..dd64052a0 100644 --- a/src/duality/duality_wrapper.cpp +++ b/src/duality/duality_wrapper.cpp @@ -425,15 +425,18 @@ expr context::make_quant(decl_kind op, const std::vector &_sorts, const st static int linearize_assumptions(int num, TermTree *assumptions, - std::vector &linear_assumptions, + std::vector > &linear_assumptions, std::vector &parents){ for(unsigned i = 0; i < assumptions->getChildren().size(); i++) num = linearize_assumptions(num, assumptions->getChildren()[i], linear_assumptions, parents); - linear_assumptions[num] = assumptions->getTerm(); + // linear_assumptions[num].push_back(assumptions->getTerm()); for(unsigned i = 0; i < assumptions->getChildren().size(); i++) parents[assumptions->getChildren()[i]->getNumber()] = num; parents[num] = SHRT_MAX; // in case we have no parent - linear_assumptions[num] = assumptions->getTerm(); + linear_assumptions[num].push_back(assumptions->getTerm()); + std::vector &ts = assumptions->getTerms(); + for(unsigned i = 0; i < ts.size(); i++) + linear_assumptions[num].push_back(ts[i]); return num + 1; } @@ -462,14 +465,15 @@ expr context::make_quant(decl_kind op, const std::vector &_sorts, const st { int size = assumptions->number(0); - std::vector linear_assumptions(size); + std::vector > linear_assumptions(size); std::vector parents(size); linearize_assumptions(0,assumptions,linear_assumptions,parents); ptr_vector< ::ast> _interpolants(size-1); - ptr_vector< ::ast>_assumptions(size); + vector >_assumptions(size); for(int i = 0; i < size; i++) - _assumptions[i] = linear_assumptions[i]; + for(unsigned j = 0; j < linear_assumptions[i].size(); j++) + _assumptions[i].push_back(linear_assumptions[i][j]); ::vector _parents; _parents.resize(parents.size()); for(unsigned i = 0; i < parents.size(); i++) _parents[i] = parents[i]; @@ -481,7 +485,8 @@ expr context::make_quant(decl_kind op, const std::vector &_sorts, const st if(!incremental){ for(unsigned i = 0; i < linear_assumptions.size(); i++) - add(linear_assumptions[i]); + for(unsigned j = 0; j < linear_assumptions[i].size(); j++) + add(linear_assumptions[i][j]); } check_result res = check(); diff --git a/src/duality/duality_wrapper.h b/src/duality/duality_wrapper.h index 21ed45479..291ddfbcf 100755 --- a/src/duality/duality_wrapper.h +++ b/src/duality/duality_wrapper.h @@ -867,6 +867,9 @@ namespace Duality { if(m_solver) m_solver->cancel(); } + + unsigned get_scope_level(){return m_solver->get_scope_level();} + }; #if 0 @@ -1199,6 +1202,8 @@ namespace Duality { inline expr getTerm(){return term;} + inline std::vector &getTerms(){return terms;} + inline std::vector &getChildren(){ return children; } @@ -1215,6 +1220,8 @@ namespace Duality { } inline void setTerm(expr t){term = t;} + + inline void addTerm(expr t){terms.push_back(t);} inline void setChildren(const std::vector & _children){ children = _children; @@ -1231,6 +1238,7 @@ namespace Duality { private: expr term; + std::vector terms; std::vector children; int num; }; diff --git a/src/interp/iz3interp.cpp b/src/interp/iz3interp.cpp index 92afc5723..7ef7e6aa2 100755 --- a/src/interp/iz3interp.cpp +++ b/src/interp/iz3interp.cpp @@ -75,15 +75,16 @@ struct frame_reducer : public iz3mgr { } } - void get_frames(const std::vector &z3_preds, + void get_frames(const std::vector >&z3_preds, const std::vector &orig_parents, - std::vector &assertions, + std::vector >&assertions, std::vector &parents, z3pf proof){ frames = z3_preds.size(); orig_parents_copy = orig_parents; for(unsigned i = 0; i < z3_preds.size(); i++) - frame_map[z3_preds[i]] = i; + for(unsigned j = 0; j < z3_preds[i].size(); j++) + frame_map[z3_preds[i][j]] = i; used_frames.resize(frames); hash_set memo; get_proof_assumptions_rec(proof,memo,used_frames); @@ -202,7 +203,7 @@ public: } void proof_to_interpolant(z3pf proof, - const std::vector &cnsts, + const std::vector > &cnsts, const std::vector &parents, std::vector &interps, const std::vector &theory, @@ -216,7 +217,7 @@ public: // get rid of frames not used in proof - std::vector cnsts_vec; + std::vector > cnsts_vec; std::vector parents_vec; frame_reducer fr(*this); fr.get_frames(cnsts,parents,cnsts_vec,parents_vec,proof); @@ -235,10 +236,7 @@ public: #define BINARY_INTERPOLATION #ifndef BINARY_INTERPOLATION // create a translator - std::vector > cnsts_vec_vec(cnsts_vec.size()); - for(unsigned i = 0; i < cnsts_vec.size(); i++) - cnsts_vec_vec[i].push_back(cnsts_vec[i]); - iz3translation *tr = iz3translation::create(*this,sp,cnsts_vec_vec,parents_vec,theory); + iz3translation *tr = iz3translation::create(*this,sp,cnsts_vec,parents_vec,theory); tr_killer.set(tr); // set the translation options, if needed @@ -273,7 +271,8 @@ public: std::vector > cnsts_vec_vec(2); for(unsigned j = 0; j < cnsts_vec.size(); j++){ bool is_A = the_base.in_range(j,rng); - cnsts_vec_vec[is_A ? 0 : 1].push_back(cnsts_vec[j]); + for(unsigned k = 0; k < cnsts_vec[j].size(); k++) + cnsts_vec_vec[is_A ? 0 : 1].push_back(cnsts_vec[j][k]); } killme tr_killer_i; @@ -308,6 +307,19 @@ public: } + void proof_to_interpolant(z3pf proof, + std::vector &cnsts, + const std::vector &parents, + std::vector &interps, + const std::vector &theory, + interpolation_options_struct *options = 0 + ){ + std::vector > cnsts_vec(cnsts.size()); + for(unsigned i = 0; i < cnsts.size(); i++) + cnsts_vec[i].push_back(cnsts[i]); + proof_to_interpolant(proof,cnsts_vec,parents,interps,theory,options); + } + // same as above, but represents the tree using an ast void proof_to_interpolant(const z3pf &proof, @@ -322,7 +334,6 @@ public: to_parents_vec_representation(_cnsts, tree, cnsts, parents, theory, pos_map); - //use the parents vector representation to compute interpolant proof_to_interpolant(proof,cnsts,parents,interps,theory,options); @@ -397,6 +408,35 @@ void iz3interpolate(ast_manager &_m_manager, interps[i] = itp.uncook(_interps[i]); } +void iz3interpolate(ast_manager &_m_manager, + ast *proof, + const ::vector > &cnsts, + const ::vector &parents, + ptr_vector &interps, + const ptr_vector &theory, + 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; + std::vector _theory(theory.size()); + for(unsigned i = 0; i < cnsts.size(); i++) + for(unsigned j = 0; j < cnsts[i].size(); j++) + _cnsts[i].push_back(itp.cook(cnsts[i][j])); + for(unsigned i = 0; i < parents.size(); i++) + _parents[i] = parents[i]; + for(unsigned i = 0; i < theory.size(); i++) + _theory[i] = itp.cook(theory[i]); + iz3mgr::ast _proof = itp.cook(proof); + itp.proof_to_interpolant(_proof,_cnsts,_parents,_interps,_theory,options); + interps.resize(_interps.size()); + for(unsigned i = 0; i < interps.size(); i++) + interps[i] = itp.uncook(_interps[i]); +} + void iz3interpolate(ast_manager &_m_manager, ast *proof, const ptr_vector &cnsts, diff --git a/src/interp/iz3interp.h b/src/interp/iz3interp.h index 62f967c02..52aa716c3 100644 --- a/src/interp/iz3interp.h +++ b/src/interp/iz3interp.h @@ -56,6 +56,16 @@ void iz3interpolate(ast_manager &_m_manager, const ptr_vector &theory, interpolation_options_struct * options = 0); +/* Same as above, but each constraint is a vector of formulas. */ + +void iz3interpolate(ast_manager &_m_manager, + ast *proof, + const vector > &cnsts, + const ::vector &parents, + ptr_vector &interps, + const ptr_vector &theory, + interpolation_options_struct * options = 0); + /* Compute an interpolant from a proof. This version uses the ast representation, for compatibility with the new API. */ diff --git a/src/interp/iz3mgr.cpp b/src/interp/iz3mgr.cpp index faa4a636d..24df25f4e 100644 --- a/src/interp/iz3mgr.cpp +++ b/src/interp/iz3mgr.cpp @@ -815,6 +815,22 @@ iz3mgr::ast iz3mgr::subst(ast var, ast t, ast e){ return subst(memo,var,t,e); } +iz3mgr::ast iz3mgr::subst(stl_ext::hash_map &subst_memo,ast e){ + std::pair foo(e,ast()); + std::pair::iterator,bool> bar = subst_memo.insert(foo); + ast &res = bar.first->second; + if(bar.second){ + int nargs = num_args(e); + std::vector args(nargs); + for(int i = 0; i < nargs; i++) + args[i] = subst(subst_memo,arg(e,i)); + opr f = op(e); + if(f == Equal && args[0] == args[1]) res = mk_true(); + else res = clone(e,args); + } + return res; +} + // apply a quantifier to a formula, with some optimizations // 1) bound variable does not occur -> no quantifier // 2) bound variable must be equal to some term -> substitute diff --git a/src/interp/iz3mgr.h b/src/interp/iz3mgr.h index f6c0bdf87..760feb000 100644 --- a/src/interp/iz3mgr.h +++ b/src/interp/iz3mgr.h @@ -631,6 +631,9 @@ class iz3mgr { ast subst(ast var, ast t, ast e); + // apply a substitution defined by a map + ast subst(stl_ext::hash_map &map, ast e); + // apply a quantifier to a formula, with some optimizations // 1) bound variable does not occur -> no quantifier // 2) bound variable must be equal to some term -> substitute diff --git a/src/interp/iz3proof_itp.cpp b/src/interp/iz3proof_itp.cpp index a2d05f7f9..60bdcde9a 100644 --- a/src/interp/iz3proof_itp.cpp +++ b/src/interp/iz3proof_itp.cpp @@ -118,6 +118,28 @@ class iz3proof_itp_impl : public iz3proof_itp { where t is an arbitrary term */ symb rewrite_B; + /* a normalization step is of the form (lhs=rhs) : proof, where "proof" + is a proof of lhs=rhs and lhs is a mixed term. If rhs is a mixed term + then it must have a greater index than lhs. */ + symb normal_step; + + /* A chain of normalization steps is either "true" (the null chain) + or normal_chain( ), where step is a normalization step + and tail is a normalization chain. The lhs of must have + a less term index than any lhs in the chain. Moreover, the rhs of + may not occur as the lhs of step in . If we wish to + add lhs=rhs to the beginning of and rhs=rhs' occurs in + we must apply transitivity, transforming to lhs=rhs'. */ + + symb normal_chain; + + /* If p is a proof of Q and c is a normalization chain, then normal(p,c) + is a proof of Q(c) (that is, Q with all substitutions in c performed). */ + + symb normal; + + + ast get_placeholder(ast t){ hash_map::iterator it = placeholders.find(t); @@ -521,10 +543,16 @@ class iz3proof_itp_impl : public iz3proof_itp { throw cannot_simplify(); } + bool is_normal_ineq(const ast &ineq){ + if(sym(ineq) == normal) + return is_ineq(arg(ineq,0)); + return is_ineq(ineq); + } + ast simplify_sum(std::vector &args){ ast cond = mk_true(); ast ineq = args[0]; - if(!is_ineq(ineq)) throw cannot_simplify(); + if(!is_normal_ineq(ineq)) throw cannot_simplify(); sum_cond_ineq(ineq,cond,args[1],args[2]); return my_implies(cond,ineq); } @@ -540,6 +568,8 @@ class iz3proof_itp_impl : public iz3proof_itp { } ast ineq_from_chain(const ast &chain, ast &cond){ + if(sym(chain) == normal) + throw "normalized inequalities not supported here"; if(is_rewrite_chain(chain)){ ast last = chain_last(chain); ast rest = chain_rest(chain); @@ -561,6 +591,13 @@ class iz3proof_itp_impl : public iz3proof_itp { cond = my_and(cond,arg(ineq2,0)); } else { + if(sym(ineq) == normal || sym(ineq2) == normal){ + ast Aproves = mk_true(); + sum_normal_ineq(ineq,coeff2,ineq2,Aproves,cond); + if(!is_true(Aproves)) + throw "Aproves not handled in sum_cond_ineq"; + return; + } ast the_ineq = ineq_from_chain(ineq2,cond); if(is_ineq(the_ineq)) linear_comb(ineq,coeff2,the_ineq); @@ -569,6 +606,27 @@ class iz3proof_itp_impl : public iz3proof_itp { } } + void destruct_normal(const ast &pf, ast &p, ast &n){ + if(sym(pf) == normal){ + p = arg(pf,0); + n = arg(pf,1); + } + else { + p = pf; + n = mk_true(); + } + } + + void sum_normal_ineq(ast &ineq, const ast &coeff2, const ast &ineq2, ast &Aproves, ast &Bproves){ + ast in1,in2,n1,n2; + destruct_normal(ineq,in1,n1); + destruct_normal(ineq2,in2,n2); + ast dummy; + sum_cond_ineq(in1,dummy,coeff2,in2); + n1 = merge_normal_chains(n1,n2, Aproves, Bproves); + ineq = make(normal,in1,n1); + } + bool is_ineq(const ast &ineq){ opr o = op(ineq); if(o == Not) o = op(arg(ineq,0)); @@ -577,6 +635,12 @@ class iz3proof_itp_impl : public iz3proof_itp { // divide both sides of inequality by a non-negative integer divisor ast idiv_ineq(const ast &ineq1, const ast &divisor){ + if(sym(ineq1) == normal){ + ast in1,n1; + destruct_normal(ineq1,in1,n1); + in1 = idiv_ineq(in1,divisor); + return make(normal,in1,n1); + } if(divisor == make_int(rational(1))) return ineq1; ast ineq = ineq1; @@ -649,11 +713,18 @@ class iz3proof_itp_impl : public iz3proof_itp { ast equa = sep_cond(arg(pf,0),cond); if(is_equivrel_chain(equa)){ ast lhs,rhs; eq_from_ineq(arg(neg_equality,0),lhs,rhs); // get inequality we need to prove - ast ineqs= chain_ineqs(op(arg(neg_equality,0)),LitA,equa,lhs,rhs); // chain must be from lhs to rhs - cond = my_and(cond,chain_conditions(LitA,equa)); - ast Bconds = chain_conditions(LitB,equa); - if(is_true(Bconds) && op(ineqs) != And) - return my_implies(cond,ineqs); + LitType lhst = get_term_type(lhs), rhst = get_term_type(rhs); + if(lhst != LitMixed && rhst != LitMixed){ + ast ineqs= chain_ineqs(op(arg(neg_equality,0)),LitA,equa,lhs,rhs); // chain must be from lhs to rhs + cond = my_and(cond,chain_conditions(LitA,equa)); + ast Bconds = z3_simplify(chain_conditions(LitB,equa)); + if(is_true(Bconds) && op(ineqs) != And) + return my_implies(cond,ineqs); + } + else { + ast itp = make(Leq,make_int(rational(0)),make_int(rational(0))); + return make(normal,itp,cons_normal(fix_normal(lhs,rhs,equa),mk_true())); + } } } throw cannot_simplify(); @@ -757,11 +828,57 @@ class iz3proof_itp_impl : public iz3proof_itp { chain = concat_rewrite_chain(chain,split[1]); } } - else // if not an equivalence, must be of form T <-> pred + else { // if not an equivalence, must be of form T <-> pred chain = concat_rewrite_chain(P,PeqQ); + } return chain; } + void get_subterm_normals(const ast &ineq1, const ast &ineq2, const ast &chain, ast &normals, + const ast &pos, hash_set &memo, ast &Aproves, ast &Bproves){ + opr o1 = op(ineq1); + opr o2 = op(ineq2); + if(o1 == Not || o1 == Leq || o1 == Lt || o1 == Geq || o1 == Gt || o1 == Plus || o1 == Times){ + int n = num_args(ineq1); + if(o2 != o1 || num_args(ineq2) != n) + throw "bad inequality rewriting"; + for(int i = 0; i < n; i++){ + ast new_pos = add_pos_to_end(pos,i); + get_subterm_normals(arg(ineq1,i), arg(ineq2,i), chain, normals, new_pos, memo, Aproves, Bproves); + } + } + else if(get_term_type(ineq2) == LitMixed && memo.find(ineq2) == memo.end()){ + memo.insert(ineq2); + ast sub_chain = extract_rewrites(chain,pos); + if(is_true(sub_chain)) + throw "bad inequality rewriting"; + ast new_normal = make_normal(ineq2,ineq1,reverse_chain(sub_chain)); + normals = merge_normal_chains(normals,cons_normal(new_normal,mk_true()), Aproves, Bproves); + } + } + + ast rewrite_chain_to_normal_ineq(const ast &chain, ast &Aproves, ast &Bproves){ + ast tail, pref = get_head_chain(chain,tail,false); // pref is x=y, tail is x=y -> x'=y' + ast head = chain_last(pref); + ast ineq1 = rewrite_rhs(head); + ast ineq2 = apply_rewrite_chain(ineq1,tail); + ast nc = mk_true(); + hash_set memo; + get_subterm_normals(ineq1,ineq2,tail,nc,top_pos,memo, Aproves, Bproves); + ast itp; + if(is_rewrite_side(LitA,head)){ + itp = ineq1; + ast mc = z3_simplify(chain_side_proves(LitB,pref)); + Bproves = my_and(Bproves,mc); + } + else { + itp = make(Leq,make_int(rational(0)),make_int(rational(0))); + ast mc = z3_simplify(chain_side_proves(LitA,pref)); + Aproves = my_and(Aproves,mc); + } + return make(normal,itp,nc); + } + /* Given a chain rewrite chain deriving not P and a rewrite chain deriving P, return an interpolant. */ ast contra_chain(const ast &neg_chain, const ast &pos_chain){ // equality is a special case. we use the derivation of x=y to rewrite not(x=y) to not(y=y) @@ -790,11 +907,18 @@ class iz3proof_itp_impl : public iz3proof_itp { } ast simplify_modpon(const std::vector &args){ - ast cond = mk_true(); - ast chain = simplify_modpon_fwd(args,cond); - ast Q2 = sep_cond(args[2],cond); - ast interp = is_negation_chain(chain) ? contra_chain(chain,Q2) : contra_chain(Q2,chain); - return my_implies(cond,interp); + ast Aproves = mk_true(), Bproves = mk_true(); + ast chain = simplify_modpon_fwd(args,Bproves); + ast Q2 = sep_cond(args[2],Bproves); + ast interp; + if(is_normal_ineq(Q2)){ // inequalities are special + ast nQ2 = rewrite_chain_to_normal_ineq(chain,Aproves,Bproves); + sum_cond_ineq(nQ2,Bproves,make_int(rational(1)),Q2); + interp = normalize(nQ2); + } + else + interp = is_negation_chain(chain) ? contra_chain(chain,Q2) : contra_chain(Q2,chain); + return my_and(Aproves,my_implies(Bproves,interp)); } @@ -1035,6 +1159,12 @@ class iz3proof_itp_impl : public iz3proof_itp { return make(add_pos,make_int(rational(arg)),pos); } + ast add_pos_to_end(const ast &pos, int i){ + if(pos == top_pos) + return pos_add(i,pos); + return make(add_pos,arg(pos,0),add_pos_to_end(arg(pos,1),i)); + } + /* return the argument number of position, if not top */ int pos_arg(const ast &pos){ rational r; @@ -1170,6 +1300,10 @@ class iz3proof_itp_impl : public iz3proof_itp { return make(sym(rew),pos_add(apos,arg(rew,0)),arg(rew,1),arg(rew,2)); } + ast rewrite_pos_set(const ast &pos, const ast &rew){ + return make(sym(rew),pos,arg(rew,1),arg(rew,2)); + } + ast rewrite_up(const ast &rew){ return make(sym(rew),arg(arg(rew,0),1),arg(rew,1),arg(rew,2)); } @@ -1317,6 +1451,28 @@ class iz3proof_itp_impl : public iz3proof_itp { split_chain_rec(chain,res); } + ast extract_rewrites(const ast &chain, const ast &pos){ + if(is_true(chain)) + return chain; + ast last = chain_last(chain); + ast rest = chain_rest(chain); + ast new_rest = extract_rewrites(rest,pos); + ast p1 = rewrite_pos(last); + ast diff; + switch(pos_diff(p1,pos,diff)){ + case -1: { + ast new_last = rewrite_pos_set(diff, last); + return chain_cons(new_rest,new_last); + } + case 1: + if(rewrite_lhs(last) != rewrite_rhs(last)) + throw "bad rewrite chain"; + break; + default:; + } + return new_rest; + } + ast down_chain(const ast &chain){ ast split[2]; split_chain(chain,split); @@ -1381,7 +1537,7 @@ class iz3proof_itp_impl : public iz3proof_itp { // ast s = ineq_to_lhs(ineq); // ast srhs = arg(s,1); ast srhs = arg(ineq,0); - if(op(srhs) == Plus && num_args(srhs) == 2){ + if(op(srhs) == Plus && num_args(srhs) == 2 && arg(ineq,1) == make_int(rational(0))){ lhs = arg(srhs,0); rhs = arg(srhs,1); // if(op(lhs) == Times) @@ -1393,6 +1549,11 @@ class iz3proof_itp_impl : public iz3proof_itp { return; } } + if(op(ineq) == Leq){ + lhs = srhs; + rhs = arg(ineq,1); + return; + } throw "bad ineq"; } @@ -1404,7 +1565,171 @@ class iz3proof_itp_impl : public iz3proof_itp { return chain_cons(rest,last); } + ast apply_rewrite_chain(const ast &t, const ast &chain){ + if(is_true(chain)) + return t; + ast last = chain_last(chain); + ast rest = chain_rest(chain); + ast mid = apply_rewrite_chain(t,rest); + ast res = subst_in_pos(mid,rewrite_pos(last),rewrite_rhs(last)); + return res; + } + ast drop_rewrites(LitType t, const ast &chain, ast &remainder){ + if(!is_true(chain)){ + ast last = chain_last(chain); + ast rest = chain_rest(chain); + if(is_rewrite_side(t,last)){ + ast res = drop_rewrites(t,rest,remainder); + remainder = chain_cons(remainder,last); + return res; + } + } + remainder = mk_true(); + return chain; + } + + // Normalization chains + + ast cons_normal(const ast &first, const ast &rest){ + return make(normal_chain,first,rest); + } + + ast normal_first(const ast &t){ + return arg(t,0); + } + + ast normal_rest(const ast &t){ + return arg(t,1); + } + + ast normal_lhs(const ast &t){ + return arg(arg(t,0),1); + } + + ast normal_rhs(const ast &t){ + return arg(arg(t,0),1); + } + + ast normal_proof(const ast &t){ + return arg(t,1); + } + + ast make_normal(const ast &lhs, const ast &rhs, const ast &proof){ + return make(normal_step,make_equiv(lhs,rhs),proof); + } + + ast fix_normal(const ast &lhs, const ast &rhs, const ast &proof){ + LitType rhst = get_term_type(rhs); + if(rhst != LitMixed || ast_id(lhs) < ast_id(rhs)) + return make_normal(lhs,rhs,proof); + else + return make_normal(rhs,lhs,reverse_chain(proof)); + } + + ast chain_side_proves(LitType side, const ast &chain){ + LitType other_side = side == LitA ? LitB : LitA; + return my_and(chain_conditions(other_side,chain),my_implies(chain_conditions(side,chain),chain_formulas(side,chain))); + } + + // Merge two normalization chains + ast merge_normal_chains_rec(const ast &chain1, const ast &chain2, hash_map &trans, ast &Aproves, ast &Bproves){ + if(is_true(chain1)) + return chain2; + if(is_true(chain2)) + return chain1; + ast f1 = normal_first(chain1); + ast f2 = normal_first(chain2); + ast lhs1 = normal_lhs(f1); + ast lhs2 = normal_lhs(f2); + int id1 = ast_id(lhs1); + int id2 = ast_id(lhs2); + if(id1 < id2) return cons_normal(f1,merge_normal_chains_rec(normal_rest(chain1),chain2,trans,Aproves,Bproves)); + if(id2 < id1) return cons_normal(f2,merge_normal_chains_rec(chain1,normal_rest(chain2),trans,Aproves,Bproves)); + ast rhs1 = normal_rhs(f1); + ast rhs2 = normal_rhs(f2); + LitType t1 = get_term_type(rhs1); + LitType t2 = get_term_type(rhs2); + int tid1 = ast_id(rhs1); + int tid2 = ast_id(rhs2); + ast pf1 = normal_proof(f1); + ast pf2 = normal_proof(f2); + ast new_normal; + if(t1 == LitMixed && (t2 != LitMixed || tid2 > tid1)){ + ast new_proof = concat_rewrite_chain(reverse_chain(pf1),pf2); + new_normal = f2; + trans[rhs1] = make_normal(rhs1,rhs2,new_proof); + } + else if(t2 == LitMixed && (t1 != LitMixed || tid1 > tid2)) + return merge_normal_chains_rec(chain2,chain1,trans,Aproves,Bproves); + else if(t1 == LitA && t2 == LitB){ + ast new_proof = concat_rewrite_chain(reverse_chain(pf1),pf2); + ast Bproof, Aproof = drop_rewrites(LitB,new_proof,Bproof); + ast mcA = chain_side_proves(LitB,Aproof); + Bproves = my_and(Bproves,mcA); + ast mcB = chain_side_proves(LitA,Bproof); + Aproves = my_and(Aproves,mcB); + ast rep = apply_rewrite_chain(rhs1,Aproof); + new_proof = concat_rewrite_chain(pf1,Aproof); + new_normal = make_normal(rhs1,rep,new_proof); + } + else if(t1 == LitA && t2 == LitB) + return merge_normal_chains_rec(chain2,chain1,trans,Aproves,Bproves); + else if(t1 == LitA) { + ast new_proof = concat_rewrite_chain(reverse_chain(pf1),pf2); + ast mc = chain_side_proves(LitB,new_proof); + Bproves = my_and(Bproves,mc); + new_normal = f1; // choice is arbitrary + } + else { /* t1 = t2 = LitB */ + ast new_proof = concat_rewrite_chain(reverse_chain(pf1),pf2); + ast mc = chain_side_proves(LitA,new_proof); + Aproves = my_and(Aproves,mc); + new_normal = f1; // choice is arbitrary + } + return cons_normal(new_normal,merge_normal_chains_rec(normal_rest(chain1),normal_rest(chain2),trans,Aproves,Bproves)); + } + + ast trans_normal_chain(const ast &chain, hash_map &trans){ + if(is_true(chain)) + return chain; + ast f = normal_first(chain); + ast r = normal_rest(chain); + ast rhs = normal_rhs(f); + hash_map::iterator it = trans.find(rhs); + ast new_normal; + if(it != trans.end()){ + const ast &f2 = it->second; + ast pf = concat_rewrite_chain(normal_proof(f),normal_proof(f2)); + new_normal = make_normal(normal_lhs(f),normal_rhs(f2),pf); + } + else + new_normal = f; + return cons_normal(new_normal,trans_normal_chain(r,trans)); + } + + ast merge_normal_chains(const ast &chain1, const ast &chain2, ast &Aproves, ast &Bproves){ + hash_map trans; + ast res = merge_normal_chains_rec(chain1,chain2,trans,Aproves,Bproves); + res = trans_normal_chain(res,trans); + return res; + } + + ast normalize(const ast &t){ + if(sym(t) != normal) + return t; + ast chain = arg(t,1); + hash_map map; + for(ast c = chain; !is_true(c); c = normal_rest(c)){ + ast first = normal_first(c); + ast lhs = normal_lhs(first); + ast rhs = normal_rhs(first); + map[lhs] = rhs; + } + ast res = subst(map,arg(t,0)); + return res; + } + /** Make an assumption node. The given clause is assumed in the given frame. */ virtual node make_assumption(int frame, const std::vector &assumption){ if(!weak){ @@ -1939,6 +2264,8 @@ class iz3proof_itp_impl : public iz3proof_itp { */ ast make_refl(const ast &e){ + if(get_term_type(e) == LitA) + return mk_false(); return mk_true(); // TODO: is this right? } @@ -2141,6 +2468,12 @@ public: m().inc_ref(rewrite_A); rewrite_B = function("@rewrite_B",3,boolboolbooldom,bool_type()); m().inc_ref(rewrite_B); + normal_step = function("@normal_step",2,boolbooldom,bool_type()); + m().inc_ref(normal_step); + normal_chain = function("@normal_chain",2,boolbooldom,bool_type()); + m().inc_ref(normal_chain); + normal = function("@normal",2,boolbooldom,bool_type()); + m().inc_ref(normal); } ~iz3proof_itp_impl(){ From a3462ba6aa47237a01e2c62669b408493e3b62d9 Mon Sep 17 00:00:00 2001 From: Ken McMillan Date: Wed, 27 Nov 2013 17:39:49 -0800 Subject: [PATCH 03/21] working on duality --- src/duality/duality.h | 43 ++++- src/duality/duality_rpfp.cpp | 79 ++++++++- src/duality/duality_solver.cpp | 107 ++++++++---- src/duality/duality_wrapper.cpp | 37 ++++- src/duality/duality_wrapper.h | 37 +++++ src/interp/iz3interp.cpp | 2 - src/interp/iz3mgr.h | 6 + src/interp/iz3proof_itp.cpp | 200 +++++++++++++++-------- src/interp/iz3proof_itp.h | 3 + src/interp/iz3translate.cpp | 20 ++- src/muz/duality/duality_dl_interface.cpp | 2 +- 11 files changed, 415 insertions(+), 121 deletions(-) diff --git a/src/duality/duality.h b/src/duality/duality.h index 158ad84d9..fb3761626 100644 --- a/src/duality/duality.h +++ b/src/duality/duality.h @@ -142,6 +142,7 @@ namespace Duality { context *ctx; /** Z3 context for formulas */ solver *slvr; /** Z3 solver */ bool need_goals; /** Can the solver use the goal tree to optimize interpolants? */ + solver aux_solver; /** For temporary use -- don't leave assertions here. */ /** Tree interpolation. This method assumes the formulas in TermTree "assumptions" are currently asserted in the solver. The return @@ -178,6 +179,8 @@ namespace Duality { /** Cancel, throw Canceled object if possible. */ virtual void cancel(){ } + LogicSolver(context &c) : aux_solver(c){} + virtual ~LogicSolver(){} }; @@ -215,7 +218,7 @@ namespace Duality { } #endif - iZ3LogicSolver(context &c){ + iZ3LogicSolver(context &c) : LogicSolver(c) { ctx = ictx = &c; slvr = islvr = new interpolating_solver(*ictx); need_goals = false; @@ -287,9 +290,9 @@ namespace Duality { literals dualLabels; std::list stack; std::vector axioms; // only saved here for printing purposes - solver aux_solver; - - + solver &aux_solver; + hash_set *proof_core; + public: /** Construct an RPFP graph with a given interpolating prover context. It is allowed to @@ -299,13 +302,14 @@ namespace Duality { inherit the axioms. */ - RPFP(LogicSolver *_ls) : Z3User(*(_ls->ctx), *(_ls->slvr)), dualModel(*(_ls->ctx)), aux_solver(*(_ls->ctx)) + RPFP(LogicSolver *_ls) : Z3User(*(_ls->ctx), *(_ls->slvr)), dualModel(*(_ls->ctx)), aux_solver(_ls->aux_solver) { ls = _ls; nodeCount = 0; edgeCount = 0; stack.push_back(stack_entry()); HornClauses = false; + proof_core = 0; } ~RPFP(); @@ -606,9 +610,13 @@ namespace Duality { lbool Solve(Node *root, int persist); + /** Same as Solve, but annotates only a single node. */ + + lbool SolveSingleNode(Node *root, Node *node); + /** Get the constraint tree (but don't solve it) */ - TermTree *GetConstraintTree(Node *root); + TermTree *GetConstraintTree(Node *root, Node *skip_descendant = 0); /** Dispose of the dual model (counterexample) if there is one. */ @@ -678,6 +686,12 @@ namespace Duality { /** Pop a scope (see Push). Note, you cannot pop axioms. */ void Pop(int num_scopes); + + /** Return true if the given edge is used in the proof of unsat. + Can be called only after Solve or Check returns an unsat result. */ + + bool EdgeUsedInProof(Edge *edge); + /** Convert a collection of clauses to Nodes and Edges in the RPFP. @@ -762,8 +776,19 @@ namespace Duality { // int GetLabelsRec(hash_map *memo, const Term &f, std::vector &labels, bool labpos); + /** Compute and save the proof core for future calls to + EdgeUsedInProof. You only need to call this if you will pop + the solver before calling EdgeUsedInProof. + */ + void ComputeProofCore(); + private: + void ClearProofCore(){ + if(proof_core) + delete proof_core; + proof_core = 0; + } Term SuffixVariable(const Term &t, int n); @@ -779,10 +804,14 @@ namespace Duality { Term ReducedDualEdge(Edge *e); - TermTree *ToTermTree(Node *root); + TermTree *ToTermTree(Node *root, Node *skip_descendant = 0); TermTree *ToGoalTree(Node *root); + void CollapseTermTreeRec(TermTree *root, TermTree *node); + + TermTree *CollapseTermTree(TermTree *node); + void DecodeTree(Node *root, TermTree *interp, int persist); Term GetUpperBound(Node *n); diff --git a/src/duality/duality_rpfp.cpp b/src/duality/duality_rpfp.cpp index 17e3de6bb..6b32bb080 100644 --- a/src/duality/duality_rpfp.cpp +++ b/src/duality/duality_rpfp.cpp @@ -185,6 +185,7 @@ namespace Duality { return clone_quantifier(t,new_body); } + RPFP::Term RPFP::LocalizeRec(Edge *e, hash_map &memo, const Term &t) { std::pair foo(t,expr(ctx)); @@ -274,13 +275,15 @@ namespace Duality { return implies(b, Localize(e, e->F.Formula)); } - TermTree *RPFP::ToTermTree(Node *root) + TermTree *RPFP::ToTermTree(Node *root, Node *skip_descendant) { + if(skip_descendant && root == skip_descendant) + return new TermTree(ctx.bool_val(true)); Edge *e = root->Outgoing; if(!e) return new TermTree(ctx.bool_val(true), std::vector()); std::vector children(e->Children.size()); for(unsigned i = 0; i < children.size(); i++) - children[i] = ToTermTree(e->Children[i]); + children[i] = ToTermTree(e->Children[i],skip_descendant); // Term top = ReducedDualEdge(e); Term top = e->dual.null() ? ctx.bool_val(true) : e->dual; TermTree *res = new TermTree(top, children); @@ -623,6 +626,7 @@ namespace Duality { TermTree *goals = NULL; if(ls->need_goals) goals = GetGoalTree(root); + ClearProofCore(); // if (dualModel != null) dualModel.Dispose(); // if (dualLabels != null) dualLabels.Dispose(); @@ -644,11 +648,54 @@ namespace Duality { return res; } + void RPFP::CollapseTermTreeRec(TermTree *root, TermTree *node){ + root->addTerm(node->getTerm()); + std::vector &cnsts = node->getTerms(); + for(unsigned i = 0; i < cnsts.size(); i++) + root->addTerm(cnsts[i]); + std::vector &chs = node->getChildren(); + for(unsigned i = 0; i < chs.size(); i++){ + CollapseTermTreeRec(root,chs[i]); + } + } + + TermTree *RPFP::CollapseTermTree(TermTree *node){ + std::vector &chs = node->getChildren(); + for(unsigned i = 0; i < chs.size(); i++) + CollapseTermTreeRec(node,chs[i]); + for(unsigned i = 0; i < chs.size(); i++) + delete chs[i]; + chs.clear(); + return node; + } + + lbool RPFP::SolveSingleNode(Node *root, Node *node) + { + timer_start("Solve"); + TermTree *tree = CollapseTermTree(GetConstraintTree(root,node)); + tree->getChildren().push_back(CollapseTermTree(ToTermTree(node))); + TermTree *interpolant = NULL; + ClearProofCore(); + + timer_start("interpolate_tree"); + lbool res = ls->interpolate_tree(tree, interpolant, dualModel,0,true); + timer_stop("interpolate_tree"); + if (res == l_false) + { + DecodeTree(node, interpolant->getChildren()[0], 0); + delete interpolant; + } + + delete tree; + timer_stop("Solve"); + return res; + } + /** Get the constraint tree (but don't solve it) */ - TermTree *RPFP::GetConstraintTree(Node *root) + TermTree *RPFP::GetConstraintTree(Node *root, Node *skip_descendant) { - return AddUpperBound(root, ToTermTree(root)); + return AddUpperBound(root, ToTermTree(root,skip_descendant)); } /** Dispose of the dual model (counterexample) if there is one. */ @@ -677,6 +724,7 @@ namespace Duality { check_result RPFP::Check(Node *root, std::vector underapproxes, std::vector *underapprox_core ) { + ClearProofCore(); // if (dualModel != null) dualModel.Dispose(); check_result res; if(!underapproxes.size()) @@ -713,6 +761,7 @@ namespace Duality { check_result RPFP::CheckUpdateModel(Node *root, std::vector assumps){ // check_result temp1 = slvr.check(); // no idea why I need to do this + ClearProofCore(); check_result res = slvr.check_keep_model(assumps.size(),&assumps[0]); dualModel = slvr.get_model(); return res; @@ -1760,9 +1809,9 @@ namespace Duality { expr conj = ctx.make(And,conjuncts); s.add(conj); check_result res = s.check(); - s.pop(1); if(res != unsat) throw "should be unsat"; + s.pop(1); for(unsigned i = 0; i < conjuncts.size(); ){ std::swap(conjuncts[i],conjuncts.back()); @@ -2276,8 +2325,28 @@ namespace Duality { } + void RPFP::ComputeProofCore(){ + if(!proof_core){ + std::vector assumps; + slvr.get_proof().get_assumptions(assumps); + proof_core = new hash_set; + for(unsigned i = 0; i < assumps.size(); i++) + proof_core->insert(assumps[i]); + } + } + + bool RPFP::EdgeUsedInProof(Edge *edge){ + ComputeProofCore(); + if(!edge->dual.null() && proof_core->find(edge->dual) != proof_core->end()) + return true; + for(unsigned i = 0; i < edge->constraints.size(); i++) + if(proof_core->find(edge->constraints[i]) != proof_core->end()) + return true; + return false; + } RPFP::~RPFP(){ + ClearProofCore(); for(unsigned i = 0; i < nodes.size(); i++) delete nodes[i]; for(unsigned i = 0; i < edges.size(); i++) diff --git a/src/duality/duality_solver.cpp b/src/duality/duality_solver.cpp index afa1c7683..86b95a657 100644 --- a/src/duality/duality_solver.cpp +++ b/src/duality/duality_solver.cpp @@ -184,7 +184,7 @@ namespace Duality { best.insert(*it); } #else - virtual void ChooseExpand(const std::set &choices, std::set &best, bool high_priority=false){ + virtual void ChooseExpand(const std::set &choices, std::set &best, bool high_priority=false, bool best_only=false){ if(high_priority) return; int best_score = INT_MAX; int worst_score = 0; @@ -194,13 +194,13 @@ namespace Duality { best_score = std::min(best_score,score); worst_score = std::max(worst_score,score); } - int cutoff = best_score + (worst_score-best_score)/2; + int cutoff = best_only ? best_score : (best_score + (worst_score-best_score)/2); for(std::set::iterator it = choices.begin(), en = choices.end(); it != en; ++it) if(scores[(*it)->map].updates <= cutoff) best.insert(*it); } #endif - + /** Called when done expanding a tree */ virtual void Done() {} }; @@ -1607,12 +1607,12 @@ namespace Duality { heuristic->ChooseExpand(choices, best); } #else - void ExpansionChoicesFull(std::set &best, bool high_priority){ + void ExpansionChoicesFull(std::set &best, bool high_priority, bool best_only = false){ std::set choices; for(std::list::iterator it = leaves.begin(), en = leaves.end(); it != en; ++it) if (high_priority || !tree->Empty(*it)) // if used in the counter-model choices.insert(*it); - heuristic->ChooseExpand(choices, best, high_priority); + heuristic->ChooseExpand(choices, best, high_priority, best_only); } void ExpansionChoicesRec(std::vector &unused_set, std::vector &used_set, @@ -1650,9 +1650,9 @@ namespace Duality { std::set old_choices; - void ExpansionChoices(std::set &best, bool high_priority){ + void ExpansionChoices(std::set &best, bool high_priority, bool best_only = false){ if(!underapprox || constrained || high_priority){ - ExpansionChoicesFull(best, high_priority); + ExpansionChoicesFull(best, high_priority,best_only); return; } std::vector unused_set, used_set; @@ -1684,7 +1684,7 @@ namespace Duality { timer_start("ExpandSomeNodes"); timer_start("ExpansionChoices"); std::set choices; - ExpansionChoices(choices,high_priority); + ExpansionChoices(choices,high_priority,max != INT_MAX); timer_stop("ExpansionChoices"); std::list leaves_copy = leaves; // copy so can modify orig leaves.clear(); @@ -1740,38 +1740,54 @@ namespace Duality { if(slvr_level != stack.back().level) throw "stacks out of sync!"; - res = tree->Solve(top, 1); // incremental solve, keep interpolants for one pop + // res = tree->Solve(top, 1); // incremental solve, keep interpolants for one pop + check_result foo = tree->Check(top); + res = foo == unsat ? l_false : l_true; if (res == l_false) { if (stack.empty()) // should never happen return false; - std::vector &expansions = stack.back().expansions; - int update_count = 0; - for(unsigned i = 0; i < expansions.size(); i++){ - tree->Generalize(expansions[i]); - if(RecordUpdate(expansions[i])) - update_count++; - } - if(update_count == 0) - std::cout << "backtracked without learning\n"; - tree->Pop(1); - hash_set leaves_to_remove; - for(unsigned i = 0; i < expansions.size(); i++){ - Node *node = expansions[i]; - // if(node != top) - // tree->ConstrainParent(node->Incoming[0],node); - std::vector &cs = node->Outgoing->Children; - for(unsigned i = 0; i < cs.size(); i++){ - leaves_to_remove.insert(cs[i]); - UnmapNode(cs[i]); - if(std::find(updated_nodes.begin(),updated_nodes.end(),cs[i]) != updated_nodes.end()) - throw "help!"; + { + std::vector &expansions = stack.back().expansions; + int update_count = 0; + for(unsigned i = 0; i < expansions.size(); i++){ + Node *node = expansions[i]; + tree->SolveSingleNode(top,node); + tree->Generalize(node); + if(RecordUpdate(node)) + update_count++; } - RemoveExpansion(node); + if(update_count == 0) + std::cout << "backtracked without learning\n"; } - RemoveLeaves(leaves_to_remove); - stack.pop_back(); + tree->ComputeProofCore(); // need to compute the proof core before popping solver + while(1) { + std::vector &expansions = stack.back().expansions; + bool prev_level_used = LevelUsedInProof(stack.size()-2); // need to compute this before pop + tree->Pop(1); + hash_set leaves_to_remove; + for(unsigned i = 0; i < expansions.size(); i++){ + Node *node = expansions[i]; + // if(node != top) + // tree->ConstrainParent(node->Incoming[0],node); + std::vector &cs = node->Outgoing->Children; + for(unsigned i = 0; i < cs.size(); i++){ + leaves_to_remove.insert(cs[i]); + UnmapNode(cs[i]); + if(std::find(updated_nodes.begin(),updated_nodes.end(),cs[i]) != updated_nodes.end()) + throw "help!"; + } + RemoveExpansion(node); + } + RemoveLeaves(leaves_to_remove); + stack.pop_back(); + if(prev_level_used || stack.size() == 1) break; + RemoveUpdateNodesAtCurrentLevel(); // this level is about to be deleted -- remove its children from update list + std::vector &unused_ex = stack.back().expansions; + for(unsigned i = 0; i < unused_ex.size(); i++) + heuristic->Update(unused_ex[i]->map); // make it less likely to expand this node in future + } HandleUpdatedNodes(); if(stack.size() == 1) return false; @@ -1782,8 +1798,10 @@ namespace Duality { for(unsigned i = 0; i < expansions.size(); i++){ tree->FixCurrentState(expansions[i]->Outgoing); } +#if 0 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)){ @@ -1798,6 +1816,27 @@ namespace Duality { } } + bool LevelUsedInProof(unsigned level){ + std::vector &expansions = stack[level].expansions; + for(unsigned i = 0; i < expansions.size(); i++) + if(tree->EdgeUsedInProof(expansions[i]->Outgoing)) + return true; + return false; + } + + void RemoveUpdateNodesAtCurrentLevel() { + for(std::list::iterator it = updated_nodes.begin(), en = updated_nodes.end(); it != en;){ + Node *node = *it; + if(AtCurrentStackLevel(node->Incoming[0]->Parent)){ + std::list::iterator victim = it; + ++it; + updated_nodes.erase(victim); + } + else + ++it; + } + } + void RemoveLeaves(hash_set &leaves_to_remove){ std::list leaves_copy; leaves_copy.swap(leaves); @@ -2270,7 +2309,7 @@ namespace Duality { return name; } - virtual void ChooseExpand(const std::set &choices, std::set &best, bool high_priority){ + virtual void ChooseExpand(const std::set &choices, std::set &best, bool high_priority, bool best_only){ if(!high_priority || !old_cex.tree){ Heuristic::ChooseExpand(choices,best,false); return; diff --git a/src/duality/duality_wrapper.cpp b/src/duality/duality_wrapper.cpp index dd64052a0..e70847d47 100644 --- a/src/duality/duality_wrapper.cpp +++ b/src/duality/duality_wrapper.cpp @@ -481,9 +481,9 @@ expr context::make_quant(decl_kind op, const std::vector &_sorts, const st for(unsigned i = 0; i < theory.size(); i++) _theory[i] = theory[i]; - push(); if(!incremental){ + push(); for(unsigned i = 0; i < linear_assumptions.size(); i++) for(unsigned j = 0; j < linear_assumptions[i].size(); j++) add(linear_assumptions[i][j]); @@ -522,7 +522,8 @@ expr context::make_quant(decl_kind op, const std::vector &_sorts, const st } #endif - pop(); + if(!incremental) + pop(); return (res == unsat) ? l_false : ((res == sat) ? l_true : l_undef); @@ -554,6 +555,29 @@ expr context::make_quant(decl_kind op, const std::vector &_sorts, const st return ""; } + + static void get_assumptions_rec(stl_ext::hash_set &memo, const proof &pf, std::vector &assumps){ + if(memo.find(pf) != memo.end())return; + memo.insert(pf); + pfrule dk = pf.rule(); + if(dk == PR_ASSERTED){ + expr con = pf.conc(); + assumps.push_back(con); + } + else { + unsigned nprems = pf.num_prems(); + for(unsigned i = 0; i < nprems; i++){ + proof arg = pf.prem(i); + get_assumptions_rec(memo,arg,assumps); + } + } + } + + void proof::get_assumptions(std::vector &assumps){ + stl_ext::hash_set memo; + get_assumptions_rec(memo,*this,assumps); + } + void ast::show() const{ std::cout << mk_pp(raw(), m()) << std::endl; @@ -564,6 +588,15 @@ expr context::make_quant(decl_kind op, const std::vector &_sorts, const st std::cout << std::endl; } + void solver::show() { + 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(std::cout, m_solver->get_assertion(n-1)); + } void include_ast_show(ast &a){ a.show(); diff --git a/src/duality/duality_wrapper.h b/src/duality/duality_wrapper.h index 291ddfbcf..fc94e53f2 100755 --- a/src/duality/duality_wrapper.h +++ b/src/duality/duality_wrapper.h @@ -393,6 +393,7 @@ namespace Duality { sort array_range() const; }; + class func_decl : public ast { public: func_decl() : ast() {} @@ -593,6 +594,36 @@ namespace Duality { }; + typedef ::decl_kind pfrule; + + class proof : public ast { + public: + proof(context & c):ast(c) {} + proof(context & c, ::proof *s):ast(c, s) {} + proof(proof const & s):ast(s) {} + operator ::proof*() const { return to_app(raw()); } + proof & operator=(proof const & s) { return static_cast(ast::operator=(s)); } + + pfrule rule() const { + ::func_decl *d = to_app(raw())->get_decl(); + return d->get_decl_kind(); + } + + unsigned num_prems() const { + return to_app(raw())->get_num_args() - 1; + } + + expr conc() const { + return ctx().cook(to_app(raw())->get_arg(num_prems())); + } + + proof prem(unsigned i) const { + return proof(ctx(),to_app(to_app(raw())->get_arg(i))); + } + + void get_assumptions(std::vector &assumps); + }; + #if 0 #if Z3_MAJOR_VERSION > 4 || Z3_MAJOR_VERSION == 4 && Z3_MINOR_VERSION >= 3 @@ -870,6 +901,12 @@ namespace Duality { unsigned get_scope_level(){return m_solver->get_scope_level();} + void show(); + + proof get_proof(){ + return proof(ctx(),m_solver->get_proof()); + } + }; #if 0 diff --git a/src/interp/iz3interp.cpp b/src/interp/iz3interp.cpp index 7ef7e6aa2..9196e24d9 100755 --- a/src/interp/iz3interp.cpp +++ b/src/interp/iz3interp.cpp @@ -501,5 +501,3 @@ void interpolation_options_struct::apply(iz3base &b){ b.set_option((*it).first,(*it).second); } - - diff --git a/src/interp/iz3mgr.h b/src/interp/iz3mgr.h index 760feb000..6d0daa89a 100644 --- a/src/interp/iz3mgr.h +++ b/src/interp/iz3mgr.h @@ -359,6 +359,12 @@ class iz3mgr { return fid == m().get_basic_family_id() && k == BOOL_SORT; } + bool is_array_type(type t){ + family_id fid = to_sort(t)->get_family_id(); + decl_kind k = to_sort(t)->get_decl_kind(); + return fid == m_array_fid && k == ARRAY_SORT; + } + type get_range_type(symb s){ return to_func_decl(s)->get_range(); } diff --git a/src/interp/iz3proof_itp.cpp b/src/interp/iz3proof_itp.cpp index 60bdcde9a..f8537d6eb 100644 --- a/src/interp/iz3proof_itp.cpp +++ b/src/interp/iz3proof_itp.cpp @@ -473,7 +473,12 @@ class iz3proof_itp_impl : public iz3proof_itp { hash_map simplify_memo; ast simplify(const ast &t){ - return simplify_rec(t); + ast res = normalize(simplify_rec(t)); +#ifdef BOGUS_QUANTS + if(localization_vars.size()) + res = add_quants(z3_simplify(res)); +#endif + return res; } ast simplify_rec(const ast &e){ @@ -550,11 +555,11 @@ class iz3proof_itp_impl : public iz3proof_itp { } ast simplify_sum(std::vector &args){ - ast cond = mk_true(); + ast Aproves = mk_true(), Bproves = mk_true(); ast ineq = args[0]; if(!is_normal_ineq(ineq)) throw cannot_simplify(); - sum_cond_ineq(ineq,cond,args[1],args[2]); - return my_implies(cond,ineq); + sum_cond_ineq(ineq,args[1],args[2],Aproves,Bproves); + return my_and(Aproves,my_implies(Bproves,ineq)); } ast simplify_rotate_sum(const ast &pl, const ast &pf){ @@ -567,38 +572,42 @@ class iz3proof_itp_impl : public iz3proof_itp { return sym(chain) == concat; } - ast ineq_from_chain(const ast &chain, ast &cond){ - if(sym(chain) == normal) - throw "normalized inequalities not supported here"; - if(is_rewrite_chain(chain)){ - ast last = chain_last(chain); - ast rest = chain_rest(chain); - if(is_true(rest) && is_rewrite_side(LitA,last) - && is_true(rewrite_lhs(last))){ - cond = my_and(cond,rewrite_cond(last)); - return rewrite_rhs(last); - } - if(is_rewrite_side(LitB,last) && is_true(rewrite_cond(last))) - return ineq_from_chain(rest,cond); +#if 0 + ast ineq_from_chain_simple(const ast &chain, ast &cond){ + if(is_true(chain)) + return chain; + ast last = chain_last(chain); + ast rest = chain_rest(chain); + if(is_true(rest) && is_rewrite_side(LitA,last) + && is_true(rewrite_lhs(last))){ + cond = my_and(cond,rewrite_cond(last)); + return rewrite_rhs(last); } + if(is_rewrite_side(LitB,last) && is_true(rewrite_cond(last))) + return ineq_from_chain_simple(rest,cond); + return chain; + } +#endif + + ast ineq_from_chain(const ast &chain, ast &Aproves, ast &Bproves){ + if(is_rewrite_chain(chain)) + return rewrite_chain_to_normal_ineq(chain,Aproves,Bproves); return chain; } - void sum_cond_ineq(ast &ineq, ast &cond, const ast &coeff2, const ast &ineq2){ + + void sum_cond_ineq(ast &ineq, const ast &coeff2, const ast &ineq2, ast &Aproves, ast &Bproves){ opr o = op(ineq2); if(o == Implies){ - sum_cond_ineq(ineq,cond,coeff2,arg(ineq2,1)); - cond = my_and(cond,arg(ineq2,0)); + sum_cond_ineq(ineq,coeff2,arg(ineq2,1),Aproves,Bproves); + Bproves = my_and(Bproves,arg(ineq2,0)); } else { - if(sym(ineq) == normal || sym(ineq2) == normal){ - ast Aproves = mk_true(); - sum_normal_ineq(ineq,coeff2,ineq2,Aproves,cond); - if(!is_true(Aproves)) - throw "Aproves not handled in sum_cond_ineq"; + ast the_ineq = ineq_from_chain(ineq2,Aproves,Bproves); + if(sym(ineq) == normal || sym(the_ineq) == normal){ + sum_normal_ineq(ineq,coeff2,the_ineq,Aproves,Bproves); return; } - ast the_ineq = ineq_from_chain(ineq2,cond); if(is_ineq(the_ineq)) linear_comb(ineq,coeff2,the_ineq); else @@ -621,10 +630,10 @@ class iz3proof_itp_impl : public iz3proof_itp { ast in1,in2,n1,n2; destruct_normal(ineq,in1,n1); destruct_normal(ineq2,in2,n2); - ast dummy; - sum_cond_ineq(in1,dummy,coeff2,in2); + ast dummy1, dummy2; + sum_cond_ineq(in1,coeff2,in2,dummy1,dummy2); n1 = merge_normal_chains(n1,n2, Aproves, Bproves); - ineq = make(normal,in1,n1); + ineq = make_normal(in1,n1); } bool is_ineq(const ast &ineq){ @@ -639,7 +648,7 @@ class iz3proof_itp_impl : public iz3proof_itp { ast in1,n1; destruct_normal(ineq1,in1,n1); in1 = idiv_ineq(in1,divisor); - return make(normal,in1,n1); + return make_normal(in1,n1); } if(divisor == make_int(rational(1))) return ineq1; @@ -649,17 +658,23 @@ class iz3proof_itp_impl : public iz3proof_itp { return make(op(ineq),mk_idiv(arg(ineq,0),divisor),mk_idiv(arg(ineq,1),divisor)); } - ast rotate_sum_rec(const ast &pl, const ast &pf, ast &cond, ast &ineq){ + ast rotate_sum_rec(const ast &pl, const ast &pf, ast &Bproves, ast &ineq){ if(pf == pl) - return my_implies(cond,simplify_ineq(ineq)); + return my_implies(Bproves,simplify_ineq(ineq)); if(op(pf) == Uninterpreted && sym(pf) == sum){ if(arg(pf,2) == pl){ - sum_cond_ineq(ineq,cond,make_int("1"),arg(pf,0)); + ast Aproves = mk_true(); + sum_cond_ineq(ineq,make_int("1"),arg(pf,0),Aproves,Bproves); + if(!is_true(Aproves)) + throw "help!"; ineq = idiv_ineq(ineq,arg(pf,1)); - return my_implies(cond,ineq); + return my_implies(Bproves,ineq); } - sum_cond_ineq(ineq,cond,arg(pf,1),arg(pf,2)); - return rotate_sum_rec(pl,arg(pf,0),cond,ineq); + ast Aproves = mk_true(); + sum_cond_ineq(ineq,arg(pf,1),arg(pf,2),Aproves,Bproves); + if(!is_true(Aproves)) + throw "help!"; + return rotate_sum_rec(pl,arg(pf,0),Bproves,ineq); } throw cannot_simplify(); } @@ -669,28 +684,30 @@ class iz3proof_itp_impl : public iz3proof_itp { ast equality = arg(neg_equality,0); ast x = arg(equality,0); ast y = arg(equality,1); - ast cond1 = mk_true(); - ast xleqy = round_ineq(ineq_from_chain(arg(pf,1),cond1)); - ast yleqx = round_ineq(ineq_from_chain(arg(pf,2),cond1)); + ast Aproves1 = mk_true(), Bproves1 = mk_true(); + ast xleqy = round_ineq(ineq_from_chain(arg(pf,1),Aproves1,Bproves1)); + ast yleqx = round_ineq(ineq_from_chain(arg(pf,2),Aproves1,Bproves1)); ast ineq1 = make(Leq,make_int("0"),make_int("0")); - sum_cond_ineq(ineq1,cond1,make_int("-1"),xleqy); - sum_cond_ineq(ineq1,cond1,make_int("-1"),yleqx); - cond1 = my_and(cond1,z3_simplify(ineq1)); - ast cond2 = mk_true(); + sum_cond_ineq(ineq1,make_int("-1"),xleqy,Aproves1,Bproves1); + sum_cond_ineq(ineq1,make_int("-1"),yleqx,Aproves1,Bproves1); + Bproves1 = my_and(Bproves1,z3_simplify(ineq1)); + ast Aproves2 = mk_true(), Bproves2 = mk_true(); ast ineq2 = make(Leq,make_int("0"),make_int("0")); - sum_cond_ineq(ineq2,cond2,make_int("1"),xleqy); - sum_cond_ineq(ineq2,cond2,make_int("1"),yleqx); - cond2 = z3_simplify(ineq2); + sum_cond_ineq(ineq2,make_int("1"),xleqy,Aproves2,Bproves2); + sum_cond_ineq(ineq2,make_int("1"),yleqx,Aproves2,Bproves2); + Bproves2 = z3_simplify(ineq2); + if(!is_true(Aproves1) || !is_true(Aproves2)) + throw "help!"; if(get_term_type(x) == LitA){ ast iter = z3_simplify(make(Plus,x,get_ineq_rhs(xleqy))); - ast rewrite1 = make_rewrite(LitA,top_pos,cond1,make(Equal,x,iter)); - ast rewrite2 = make_rewrite(LitB,top_pos,cond2,make(Equal,iter,y)); + ast rewrite1 = make_rewrite(LitA,top_pos,Bproves1,make(Equal,x,iter)); + ast rewrite2 = make_rewrite(LitB,top_pos,Bproves2,make(Equal,iter,y)); return chain_cons(chain_cons(mk_true(),rewrite1),rewrite2); } if(get_term_type(y) == LitA){ ast iter = z3_simplify(make(Plus,y,get_ineq_rhs(yleqx))); - ast rewrite2 = make_rewrite(LitA,top_pos,cond1,make(Equal,iter,y)); - ast rewrite1 = make_rewrite(LitB,top_pos,cond2,make(Equal,x,iter)); + ast rewrite2 = make_rewrite(LitA,top_pos,Bproves1,make(Equal,iter,y)); + ast rewrite1 = make_rewrite(LitB,top_pos,Bproves2,make(Equal,x,iter)); return chain_cons(chain_cons(mk_true(),rewrite1),rewrite2); } throw cannot_simplify(); @@ -723,7 +740,7 @@ class iz3proof_itp_impl : public iz3proof_itp { } else { ast itp = make(Leq,make_int(rational(0)),make_int(rational(0))); - return make(normal,itp,cons_normal(fix_normal(lhs,rhs,equa),mk_true())); + return make_normal(itp,cons_normal(fix_normal(lhs,rhs,equa),mk_true())); } } } @@ -852,7 +869,7 @@ class iz3proof_itp_impl : public iz3proof_itp { ast sub_chain = extract_rewrites(chain,pos); if(is_true(sub_chain)) throw "bad inequality rewriting"; - ast new_normal = make_normal(ineq2,ineq1,reverse_chain(sub_chain)); + ast new_normal = make_normal_step(ineq2,ineq1,reverse_chain(sub_chain)); normals = merge_normal_chains(normals,cons_normal(new_normal,mk_true()), Aproves, Bproves); } } @@ -876,7 +893,7 @@ class iz3proof_itp_impl : public iz3proof_itp { ast mc = z3_simplify(chain_side_proves(LitA,pref)); Aproves = my_and(Aproves,mc); } - return make(normal,itp,nc); + return make_normal(itp,nc); } /* Given a chain rewrite chain deriving not P and a rewrite chain deriving P, return an interpolant. */ @@ -913,7 +930,7 @@ class iz3proof_itp_impl : public iz3proof_itp { ast interp; if(is_normal_ineq(Q2)){ // inequalities are special ast nQ2 = rewrite_chain_to_normal_ineq(chain,Aproves,Bproves); - sum_cond_ineq(nQ2,Bproves,make_int(rational(1)),Q2); + sum_cond_ineq(nQ2,make_int(rational(1)),Q2,Aproves,Bproves); interp = normalize(nQ2); } else @@ -1549,7 +1566,7 @@ class iz3proof_itp_impl : public iz3proof_itp { return; } } - if(op(ineq) == Leq){ + if(op(ineq) == Leq || op(ineq) == Geq){ lhs = srhs; rhs = arg(ineq,1); return; @@ -1604,7 +1621,7 @@ class iz3proof_itp_impl : public iz3proof_itp { } ast normal_lhs(const ast &t){ - return arg(arg(t,0),1); + return arg(arg(t,0),0); } ast normal_rhs(const ast &t){ @@ -1615,16 +1632,22 @@ class iz3proof_itp_impl : public iz3proof_itp { return arg(t,1); } - ast make_normal(const ast &lhs, const ast &rhs, const ast &proof){ + ast make_normal_step(const ast &lhs, const ast &rhs, const ast &proof){ return make(normal_step,make_equiv(lhs,rhs),proof); } + ast make_normal(const ast &ineq, const ast &nrml){ + if(!is_ineq(ineq)) + throw "what?"; + return make(normal,ineq,nrml); + } + ast fix_normal(const ast &lhs, const ast &rhs, const ast &proof){ LitType rhst = get_term_type(rhs); if(rhst != LitMixed || ast_id(lhs) < ast_id(rhs)) - return make_normal(lhs,rhs,proof); + return make_normal_step(lhs,rhs,proof); else - return make_normal(rhs,lhs,reverse_chain(proof)); + return make_normal_step(rhs,lhs,reverse_chain(proof)); } ast chain_side_proves(LitType side, const ast &chain){ @@ -1658,7 +1681,7 @@ class iz3proof_itp_impl : public iz3proof_itp { if(t1 == LitMixed && (t2 != LitMixed || tid2 > tid1)){ ast new_proof = concat_rewrite_chain(reverse_chain(pf1),pf2); new_normal = f2; - trans[rhs1] = make_normal(rhs1,rhs2,new_proof); + trans[rhs1] = make_normal_step(rhs1,rhs2,new_proof); } else if(t2 == LitMixed && (t1 != LitMixed || tid1 > tid2)) return merge_normal_chains_rec(chain2,chain1,trans,Aproves,Bproves); @@ -1671,7 +1694,7 @@ class iz3proof_itp_impl : public iz3proof_itp { Aproves = my_and(Aproves,mcB); ast rep = apply_rewrite_chain(rhs1,Aproof); new_proof = concat_rewrite_chain(pf1,Aproof); - new_normal = make_normal(rhs1,rep,new_proof); + new_normal = make_normal_step(rhs1,rep,new_proof); } else if(t1 == LitA && t2 == LitB) return merge_normal_chains_rec(chain2,chain1,trans,Aproves,Bproves); @@ -1701,7 +1724,7 @@ class iz3proof_itp_impl : public iz3proof_itp { if(it != trans.end()){ const ast &f2 = it->second; ast pf = concat_rewrite_chain(normal_proof(f),normal_proof(f2)); - new_normal = make_normal(normal_lhs(f),normal_rhs(f2),pf); + new_normal = make_normal_step(normal_lhs(f),normal_rhs(f2),pf); } else new_normal = f; @@ -1715,9 +1738,36 @@ class iz3proof_itp_impl : public iz3proof_itp { return res; } - ast normalize(const ast &t){ + bool destruct_cond_ineq(ast t, ast &Aproves, ast &Bproves, ast&ineq){ + if(op(t) == And){ + Aproves = arg(t,0); + t = arg(t,1); + } + else + Aproves = mk_true(); + if(op(t) == Implies){ + Bproves = arg(t,0); + t = arg(t,1); + } + else + Bproves = mk_true(); + if(is_normal_ineq(t)){ + ineq = t; + return true; + } + return false; + } + + ast cons_cond_ineq(const ast &Aproves, const ast &Bproves, const ast &ineq){ + return my_and(Aproves,my_implies(Bproves,ineq)); + } + + ast normalize(const ast &ct){ + ast Aproves,Bproves,t; + if(!destruct_cond_ineq(ct,Aproves,Bproves,t)) + return ct; if(sym(t) != normal) - return t; + return ct; ast chain = arg(t,1); hash_map map; for(ast c = chain; !is_true(c); c = normal_rest(c)){ @@ -1727,7 +1777,7 @@ class iz3proof_itp_impl : public iz3proof_itp { map[lhs] = rhs; } ast res = subst(map,arg(t,0)); - return res; + return cons_cond_ineq(Aproves,Bproves,res); } /** Make an assumption node. The given clause is assumed in the given frame. */ @@ -1848,8 +1898,7 @@ class iz3proof_itp_impl : public iz3proof_itp { } /** Make an axiom node. The conclusion must be an instance of an axiom. */ - virtual node make_axiom(const std::vector &conclusion){ - prover::range frng = pv->range_full(); + virtual node make_axiom(const std::vector &conclusion, prover::range frng){ int nargs = conclusion.size(); std::vector largs(nargs); std::vector eqs; @@ -1874,6 +1923,10 @@ class iz3proof_itp_impl : public iz3proof_itp { return itp; } + virtual node make_axiom(const std::vector &conclusion){ + return make_axiom(conclusion,pv->range_full()); + } + /** Make a Contra node. This rule takes a derivation of the form Gamma |- False and produces |- \/~Gamma. */ @@ -2299,7 +2352,8 @@ class iz3proof_itp_impl : public iz3proof_itp { int nargs = num_args(e); if(nargs > 0 /* && (!is_local(e) || flo <= hi || fhi >= lo) */){ prover::range frng = rng; - if(op(e) == Uninterpreted){ + opr o = op(e); + if(o == Uninterpreted){ symb f = sym(e); prover::range srng = pv->sym_range(f); if(pv->ranges_intersect(srng,rng)) // localize to desired range if possible @@ -2307,6 +2361,9 @@ class iz3proof_itp_impl : public iz3proof_itp { else frng = srng; // this term will be localized } + else if(o == Plus || o == Times){ // don't want bound variables inside arith ops + frng = erng; // this term will be localized + } std::vector largs(nargs); std::vector eqs; std::vector pfs; @@ -2333,6 +2390,9 @@ class iz3proof_itp_impl : public iz3proof_itp { if(pv->ranges_intersect(pv->ast_scope(e),rng)) return e; // this term occurs in range, so it's O.K. + if(is_array_type(get_type(e))) + throw "help!"; + // choose a frame for the constraint that is close to range int frame = pv->range_near(pv->ast_scope(e),rng); @@ -2362,7 +2422,11 @@ class iz3proof_itp_impl : public iz3proof_itp { /* Return an interpolant from a proof of false */ ast interpolate(const node &pf){ // proof of false must be a formula, with quantified symbols +#ifndef BOGUS_QUANTS return add_quants(z3_simplify(pf)); +#else + return z3_simplify(pf); +#endif } ast resolve_with_quantifier(const ast &pivot1, const ast &conj1, diff --git a/src/interp/iz3proof_itp.h b/src/interp/iz3proof_itp.h index 299f391ea..4d76e3a92 100644 --- a/src/interp/iz3proof_itp.h +++ b/src/interp/iz3proof_itp.h @@ -70,6 +70,9 @@ class iz3proof_itp : public iz3mgr { /** Make an axiom node. The conclusion must be an instance of an axiom. */ virtual node make_axiom(const std::vector &conclusion) = 0; + /** Make an axiom node. The conclusion must be an instance of an axiom. Localize axiom instance to range*/ + virtual node make_axiom(const std::vector &conclusion, prover::range) = 0; + /** Make a Contra node. This rule takes a derivation of the form Gamma |- False and produces |- \/~Gamma. */ diff --git a/src/interp/iz3translate.cpp b/src/interp/iz3translate.cpp index 4ea755eff..7dfa48cdd 100755 --- a/src/interp/iz3translate.cpp +++ b/src/interp/iz3translate.cpp @@ -1364,6 +1364,18 @@ public: return eq2; } + bool get_store_array(const ast &t, ast &res){ + if(op(t) == Store){ + res = t; + return true; + } + int nargs = num_args(t); + for(int i = 0; i < nargs; i++) + if(get_store_array(arg(t,i),res)) + return true; + return false; + } + // translate a Z3 proof term into interpolating proof system Iproof::node translate_main(ast proof, bool expect_clause = true){ @@ -1578,9 +1590,13 @@ public: throw unsupported(); } break; - case ArrayTheory: // nothing fancy for this - res = iproof->make_axiom(lits); + case ArrayTheory: {// nothing fancy for this + ast store_array; + if(!get_store_array(con,store_array)) + throw unsupported(); + res = iproof->make_axiom(lits,ast_scope(store_array)); break; + } default: throw unsupported(); } diff --git a/src/muz/duality/duality_dl_interface.cpp b/src/muz/duality/duality_dl_interface.cpp index 25dfcebbd..12dd4ff3e 100644 --- a/src/muz/duality/duality_dl_interface.cpp +++ b/src/muz/duality/duality_dl_interface.cpp @@ -472,7 +472,7 @@ static proof_ref extract_proof(dl_interface *d, Solver::Counterexample &cex) { expr conc = f(args); - ::vector pprems; + ::vector< ::proof *> pprems; for(unsigned i = 0; i < prems.size(); i++) pprems.push_back(prems[i].get()); From 56b3406ee56c2f3fd9679131d1be02df99926d29 Mon Sep 17 00:00:00 2001 From: Ken McMillan Date: Tue, 10 Dec 2013 11:41:25 -0800 Subject: [PATCH 04/21] added mbqi.id option, working on quantifiers in duality --- src/duality/duality.h | 26 +++- src/duality/duality_rpfp.cpp | 200 ++++++++++++++++++++++++--- src/duality/duality_solver.cpp | 16 ++- src/duality/duality_wrapper.cpp | 4 + src/duality/duality_wrapper.h | 4 + src/interp/iz3mgr.cpp | 26 +++- src/interp/iz3mgr.h | 3 +- src/interp/iz3proof_itp.cpp | 125 ++++++++++++++++- src/smt/params/qi_params.cpp | 1 + src/smt/params/qi_params.h | 5 +- src/smt/params/smt_params_helper.pyg | 1 + src/smt/smt_model_checker.cpp | 1 + src/smt/smt_quantifier.cpp | 24 +++- src/smt/smt_quantifier.h | 6 + 14 files changed, 409 insertions(+), 33 deletions(-) diff --git a/src/duality/duality.h b/src/duality/duality.h index fb3761626..7a1e88f3c 100644 --- a/src/duality/duality.h +++ b/src/duality/duality.h @@ -79,9 +79,12 @@ namespace Duality { int CumulativeDecisions(); + int CountOperators(const Term &t); + private: void SummarizeRec(hash_set &memo, std::vector &lits, int &ops, const Term &t); + int CountOperatorsRec(hash_set &memo, const Term &t); }; @@ -280,7 +283,7 @@ namespace Duality { public: std::list edges; std::list nodes; - std::list constraints; + std::list > constraints; }; @@ -556,6 +559,7 @@ namespace Duality { edge to their values in the current assignment. */ void FixCurrentState(Edge *root); + void FixCurrentStateFull(Edge *edge); /** Declare a constant in the background theory. */ @@ -653,7 +657,11 @@ namespace Duality { Term ComputeUnderapprox(Node *root, int persist); /** Try to strengthen the annotation of a node by removing disjuncts. */ - void Generalize(Node *node); + void Generalize(Node *root, Node *node); + + + /** Compute disjunctive interpolant for node by case splitting */ + void InterpolateByCases(Node *root, Node *node); /** Push a scope. Assertions made after Push can be undone by Pop. */ @@ -687,6 +695,10 @@ namespace Duality { void Pop(int num_scopes); + /** Erase the proof by performing a Pop, Push and re-assertion of + all the popped constraints */ + void PopPush(); + /** Return true if the given edge is used in the proof of unsat. Can be called only after Solve or Check returns an unsat result. */ @@ -861,6 +873,11 @@ namespace Duality { 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); + + Term UnderapproxFullFormula(const Term &f, hash_set &dont_cares); + Term ToRuleRec(Edge *e, hash_map &memo, const Term &t, std::vector &quants); hash_map resolve_ite_memo; @@ -896,6 +913,11 @@ namespace Duality { expr SimplifyOr(std::vector &lits); void SetAnnotation(Node *root, const expr &t); + + void AddEdgeToSolver(Edge *edge); + + void AddToProofCore(hash_set &core); + }; /** RPFP solver base class. */ diff --git a/src/duality/duality_rpfp.cpp b/src/duality/duality_rpfp.cpp index 6b32bb080..c582e19fc 100644 --- a/src/duality/duality_rpfp.cpp +++ b/src/duality/duality_rpfp.cpp @@ -125,6 +125,32 @@ namespace Duality { } } + int Z3User::CountOperatorsRec(hash_set &memo, const Term &t){ + if(memo.find(t) != memo.end()) + return 0; + memo.insert(t); + if(t.is_app()){ + decl_kind k = t.decl().get_decl_kind(); + if(k == And || k == Or){ + int count = 1; + int nargs = t.num_args(); + for(int i = 0; i < nargs; i++) + count += CountOperatorsRec(memo,t.arg(i)); + return count; + } + return 0; + } + if(t.is_quantifier()) + return CountOperatorsRec(memo,t.body())+1; + return 0; + } + + int Z3User::CountOperators(const Term &t){ + hash_set memo; + return CountOperatorsRec(memo,t); + } + + Z3User::Term Z3User::conjoin(const std::vector &args){ return ctx.make(And,args); } @@ -329,7 +355,15 @@ namespace Duality { res = f(args.size(),&args[0]); } else if (t.is_quantifier()) - res = CloneQuantifier(t,SubstRec(memo, t.body())); + { + std::vector pats; + t.get_patterns(pats); + for(unsigned i = 0; i < pats.size(); i++) + pats[i] = SubstRec(memo,pats[i]); + Term body = SubstRec(memo,t.body()); + res = clone_quantifier(t, body, pats); + } + // res = CloneQuantifier(t,SubstRec(memo, t.body())); else res = t; return res; } @@ -552,7 +586,7 @@ namespace Duality { void RPFP::ConstrainEdgeLocalized(Edge *e, const Term &tl) { e->constraints.push_back(tl); - stack.back().constraints.push_back(e); + stack.back().constraints.push_back(std::pair(e,tl)); slvr.add(tl); } @@ -1142,7 +1176,8 @@ namespace Duality { } } /* Unreachable! */ - std::cerr << "error in RPFP::ImplicantRed"; + // TODO: need to indicate this failure to caller + // std::cerr << "error in RPFP::ImplicantRed"; goto done; } else if(k == Not) { @@ -1161,6 +1196,31 @@ namespace Duality { done[truth].insert(f); } + void RPFP::ImplicantFullRed(hash_map &memo, const Term &f, std::vector &lits, + hash_set &done, hash_set &dont_cares){ + if(done.find(f) != done.end()) + return; /* already processed */ + if(f.is_app()){ + int nargs = f.num_args(); + 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); + goto done; + } + } + { + if(dont_cares.find(f) == dont_cares.end()){ + int b = SubtermTruth(memo,f); + if(b != 0 && b != 1) goto done; + expr bv = (b==1) ? f : !f; + lits.push_back(bv); + } + } + done: + done.insert(f); + } + RPFP::Term RPFP::ResolveIte(hash_map &memo, const Term &t, std::vector &lits, hash_set *done, hash_set &dont_cares){ if(resolve_ite_memo.find(t) != resolve_ite_memo.end()) @@ -1223,6 +1283,16 @@ namespace Duality { return conjoin(lits); } + RPFP::Term RPFP::UnderapproxFullFormula(const Term &f, hash_set &dont_cares){ + /* first compute truth values of subterms */ + hash_map memo; + hash_set done; + std::vector lits; + ImplicantFullRed(memo,f,lits,done,dont_cares); + /* return conjunction of literals */ + return conjoin(lits); + } + struct VariableProjector : Z3User { struct elim_cand { @@ -1759,6 +1829,17 @@ namespace Duality { ConstrainEdgeLocalized(edge,eu); } + void RPFP::FixCurrentStateFull(Edge *edge){ + 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]; + Term eu = UnderapproxFullFormula(dual,dont_cares); + timer_stop("UnderapproxFormula"); + ConstrainEdgeLocalized(edge,eu); + } RPFP::Term RPFP::ModelValueAsConstraint(const Term &t){ @@ -1803,6 +1884,7 @@ namespace Duality { res = CreateRelation(p->Annotation.IndParams,funder); } +#if 0 void RPFP::GreedyReduce(solver &s, std::vector &conjuncts){ // verify s.push(); @@ -1829,6 +1911,36 @@ namespace Duality { } } } +#endif + + void RPFP::GreedyReduce(solver &s, std::vector &conjuncts){ + std::vector lits(conjuncts.size()); + for(unsigned i = 0; i < lits.size(); i++){ + func_decl pred = ctx.fresh_func_decl("@alit", ctx.bool_sort()); + lits[i] = pred(); + s.add(ctx.make(Implies,lits[i],conjuncts[i])); + } + + // verify + check_result res = s.check(lits.size(),&lits[0]); + if(res != unsat) + throw "should be unsat"; + + for(unsigned i = 0; i < conjuncts.size(); ){ + std::swap(conjuncts[i],conjuncts.back()); + std::swap(lits[i],lits.back()); + check_result res = s.check(lits.size()-1,&lits[0]); + if(res != unsat){ + std::swap(conjuncts[i],conjuncts.back()); + std::swap(lits[i],lits.back()); + i++; + } + else { + conjuncts.pop_back(); + lits.pop_back(); + } + } + } void RPFP::NegateLits(std::vector &lits){ for(unsigned i = 0; i < lits.size(); i++){ @@ -1848,20 +1960,56 @@ namespace Duality { return ctx.make(Or,lits); } - void RPFP::Generalize(Node *node){ - std::vector conjuncts; - expr fmla = GetAnnotation(node); - CollectConjuncts(fmla,conjuncts,false); - // try to remove conjuncts one at a tme - aux_solver.push(); - Edge *edge = node->Outgoing; + // set up edge constraint in aux solver + void RPFP::AddEdgeToSolver(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); } - GreedyReduce(aux_solver,conjuncts); + } + + void RPFP::InterpolateByCases(Node *root, Node *node){ + aux_solver.push(); + AddEdgeToSolver(node->Outgoing); + node->Annotation.SetEmpty(); + hash_set *core = new hash_set; + core->insert(node->Outgoing->dual); + while(1){ + aux_solver.push(); + aux_solver.add(!GetAnnotation(node)); + if(aux_solver.check() == unsat){ + aux_solver.pop(1); + break; + } + dualModel = aux_solver.get_model(); + aux_solver.pop(1); + Push(); + FixCurrentStateFull(node->Outgoing); + ConstrainEdgeLocalized(node->Outgoing,!GetAnnotation(node)); + check_result foo = Check(root); + if(foo != unsat) + throw "should be unsat"; + AddToProofCore(*core); + Transformer old_annot = node->Annotation; + SolveSingleNode(root,node); + Pop(1); + node->Annotation.UnionWith(old_annot); + } + if(proof_core) + delete proof_core; // shouldn't happen + proof_core = core; + aux_solver.pop(1); + } + + void RPFP::Generalize(Node *root, Node *node){ + aux_solver.push(); + AddEdgeToSolver(node->Outgoing); + expr fmla = GetAnnotation(node); + std::vector conjuncts; + CollectConjuncts(fmla,conjuncts,false); + GreedyReduce(aux_solver,conjuncts); // try to remove conjuncts one at a tme aux_solver.pop(1); NegateLits(conjuncts); SetAnnotation(node,SimplifyOr(conjuncts)); @@ -1887,12 +2035,26 @@ namespace Duality { (*it)->dual = expr(ctx,NULL); for(std::list::iterator it = back.nodes.begin(), en = back.nodes.end(); it != en; ++it) (*it)->dual = expr(ctx,NULL); - for(std::list::iterator it = back.constraints.begin(), en = back.constraints.end(); it != en; ++it) - (*it)->constraints.pop_back(); + for(std::list >::iterator it = back.constraints.begin(), en = back.constraints.end(); it != en; ++it) + (*it).first->constraints.pop_back(); stack.pop_back(); } } + /** Erase the proof by performing a Pop, Push and re-assertion of + all the popped constraints */ + + void RPFP::PopPush(){ + slvr.pop(1); + slvr.push(); + stack_entry &back = stack.back(); + for(std::list::iterator it = back.edges.begin(), en = back.edges.end(); it != en; ++it) + slvr.add((*it)->dual); + for(std::list::iterator it = back.nodes.begin(), en = back.nodes.end(); it != en; ++it) + slvr.add((*it)->dual); + for(std::list >::iterator it = back.constraints.begin(), en = back.constraints.end(); it != en; ++it) + slvr.add((*it).second); + } @@ -2325,13 +2487,17 @@ namespace Duality { } + void RPFP::AddToProofCore(hash_set &core){ + std::vector assumps; + slvr.get_proof().get_assumptions(assumps); + for(unsigned i = 0; i < assumps.size(); i++) + core.insert(assumps[i]); + } + void RPFP::ComputeProofCore(){ if(!proof_core){ - std::vector assumps; - slvr.get_proof().get_assumptions(assumps); proof_core = new hash_set; - for(unsigned i = 0; i < assumps.size(); i++) - proof_core->insert(assumps[i]); + AddToProofCore(*proof_core); } } diff --git a/src/duality/duality_solver.cpp b/src/duality/duality_solver.cpp index 86b95a657..40ddf25b1 100644 --- a/src/duality/duality_solver.cpp +++ b/src/duality/duality_solver.cpp @@ -1754,12 +1754,14 @@ namespace Duality { for(unsigned i = 0; i < expansions.size(); i++){ Node *node = expansions[i]; tree->SolveSingleNode(top,node); - tree->Generalize(node); + if(expansions.size() == 1 && NodeTooComplicated(node)) + SimplifyNode(node); + tree->Generalize(top,node); if(RecordUpdate(node)) update_count++; } if(update_count == 0) - std::cout << "backtracked without learning\n"; + reporter->Message("backtracked without learning"); } tree->ComputeProofCore(); // need to compute the proof core before popping solver while(1) { @@ -1816,6 +1818,16 @@ namespace Duality { } } + bool NodeTooComplicated(Node *node){ + return tree->CountOperators(node->Annotation.Formula) > 5; + } + + void SimplifyNode(Node *node){ + // have to destroy the old proof to get a new interpolant + tree->PopPush(); + tree->InterpolateByCases(top,node); + } + bool LevelUsedInProof(unsigned level){ std::vector &expansions = stack[level].expansions; for(unsigned i = 0; i < expansions.size(); i++) diff --git a/src/duality/duality_wrapper.cpp b/src/duality/duality_wrapper.cpp index e70847d47..988b03d6d 100644 --- a/src/duality/duality_wrapper.cpp +++ b/src/duality/duality_wrapper.cpp @@ -34,8 +34,12 @@ namespace Duality { p.set_bool("proof", true); // this is currently useless p.set_bool("model", true); p.set_bool("unsat_core", true); + p.set_bool("mbqi",true); + 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 scoped_ptr sf = mk_smt_solver_factory(); m_solver = (*sf)(m(), p, true, true, true, ::symbol::null); + m_solver->updt_params(p); // why do we have to do this? canceled = false; } diff --git a/src/duality/duality_wrapper.h b/src/duality/duality_wrapper.h index fc94e53f2..c9860941b 100755 --- a/src/duality/duality_wrapper.h +++ b/src/duality/duality_wrapper.h @@ -413,6 +413,7 @@ namespace Duality { expr operator()(unsigned n, expr const * args) const; expr operator()(const std::vector &args) const; + expr operator()() const; expr operator()(expr const & a) const; expr operator()(int a) const; expr operator()(expr const & a1, expr const & a2) const; @@ -1184,6 +1185,9 @@ namespace Duality { inline expr func_decl::operator()(const std::vector &args) const { return operator()(args.size(),&args[0]); } + inline expr func_decl::operator()() const { + return operator()(0,0); + } inline expr func_decl::operator()(expr const & a) const { return operator()(1,&a); } diff --git a/src/interp/iz3mgr.cpp b/src/interp/iz3mgr.cpp index 24df25f4e..f35dae93f 100644 --- a/src/interp/iz3mgr.cpp +++ b/src/interp/iz3mgr.cpp @@ -190,7 +190,7 @@ iz3mgr::ast iz3mgr::make_quant(opr op, const std::vector &bvs, ast &body){ op == Forall, names.size(), &types[0], &names[0], abs_body.get(), 0, - symbol(), + symbol("itp"), symbol(), 0, 0, 0, 0 @@ -761,6 +761,19 @@ int iz3mgr::occurs_in(ast var, ast e){ } +bool iz3mgr::solve_arith(const ast &v, const ast &x, const ast &y, ast &res){ + if(op(x) == Plus){ + int n = num_args(x); + for(int i = 0; i < n; i++){ + if(arg(x,i) == v){ + res = z3_simplify(make(Sub, y, make(Sub, x, v))); + return true; + } + } + } + return false; +} + // find a controlling equality for a given variable v in a term // a controlling equality is of the form v = t, which, being // false would force the formula to have the specifid truth value @@ -774,6 +787,9 @@ iz3mgr::ast iz3mgr::cont_eq(stl_ext::hash_set &cont_eq_memo, bool truth, as if(!truth && op(e) == Equal){ if(arg(e,0) == v) return(arg(e,1)); if(arg(e,1) == v) return(arg(e,0)); + ast res; + if(solve_arith(v,arg(e,0),arg(e,1),res)) return res; + if(solve_arith(v,arg(e,1),arg(e,0),res)) return res; } if((!truth && op(e) == And) || (truth && op(e) == Or)){ int nargs = num_args(e); @@ -836,6 +852,14 @@ iz3mgr::ast iz3mgr::subst(stl_ext::hash_map &subst_memo,ast e){ // 2) bound variable must be equal to some term -> substitute iz3mgr::ast iz3mgr::apply_quant(opr quantifier, ast var, ast e){ + if((quantifier == Forall && op(e) == And) + || (quantifier == Exists && op(e) == Or)){ + int n = num_args(e); + std::vector args(n); + for(int i = 0; i < n; i++) + args[i] = apply_quant(quantifier,var,arg(e,i)); + return make(op(e),args); + } if(!occurs_in(var,e))return e; hash_set cont_eq_memo; ast cterm = cont_eq(cont_eq_memo, quantifier == Forall, var, e); diff --git a/src/interp/iz3mgr.h b/src/interp/iz3mgr.h index 6d0daa89a..7bdc2ecce 100644 --- a/src/interp/iz3mgr.h +++ b/src/interp/iz3mgr.h @@ -692,13 +692,14 @@ class iz3mgr { protected: ast_manager &m_manager; + int occurs_in(ast var, ast e); private: ast mki(family_id fid, decl_kind sk, int n, raw_ast **args); ast make(opr op, int n, raw_ast **args); ast make(symb sym, int n, raw_ast **args); int occurs_in1(stl_ext::hash_map &occurs_in_memo, ast var, ast e); - int occurs_in(ast var, ast e); + bool solve_arith(const ast &v, const ast &x, const ast &y, ast &res); ast cont_eq(stl_ext::hash_set &cont_eq_memo, bool truth, ast v, ast e); ast subst(stl_ext::hash_map &subst_memo, ast var, ast t, ast e); diff --git a/src/interp/iz3proof_itp.cpp b/src/interp/iz3proof_itp.cpp index f8537d6eb..75d14bca1 100644 --- a/src/interp/iz3proof_itp.cpp +++ b/src/interp/iz3proof_itp.cpp @@ -135,10 +135,12 @@ class iz3proof_itp_impl : public iz3proof_itp { /* If p is a proof of Q and c is a normalization chain, then normal(p,c) is a proof of Q(c) (that is, Q with all substitutions in c performed). */ - + symb normal; - + /** Stand-ins for quantifiers */ + + symb sforall, sexists; ast get_placeholder(ast t){ @@ -231,6 +233,10 @@ class iz3proof_itp_impl : public iz3proof_itp { ast neg_pivot_lit = mk_not(atom); if(op(pivot) != Not) std::swap(premise1,premise2); + if(op(pivot) == Equal && op(arg(pivot,0)) == Select && op(arg(pivot,1)) == Select){ + neg_pivot_lit = mk_not(neg_pivot_lit); + std::swap(premise1,premise2); + } return resolve_arith_rec1(memo, neg_pivot_lit, premise1, premise2); } @@ -355,7 +361,13 @@ class iz3proof_itp_impl : public iz3proof_itp { break; } default: - res = itp2; + { + symb s = sym(itp2); + if(s == sforall || s == sexists) + res = make(s,arg(itp2,0),resolve_arith_rec2(memo, pivot1, conj1, arg(itp2,1))); + else + res = itp2; + } } } return res; @@ -385,7 +397,13 @@ class iz3proof_itp_impl : public iz3proof_itp { break; } default: - res = itp1; + { + symb s = sym(itp1); + if(s == sforall || s == sexists) + res = make(s,arg(itp1,0),resolve_arith_rec1(memo, neg_pivot_lit, arg(itp1,1), itp2)); + else + res = itp1; + } } } return res; @@ -1897,6 +1915,20 @@ class iz3proof_itp_impl : public iz3proof_itp { return itp; } + ast capture_localization(ast e){ + // #define CAPTURE_LOCALIZATION +#ifdef CAPTURE_LOCALIZATION + for(int i = localization_vars.size() - 1; i >= 0; i--){ + LocVar &lv = localization_vars[i]; + if(occurs_in(lv.var,e)){ + symb q = (pv->in_range(lv.frame,rng)) ? sexists : sforall; + e = make(q,make(Equal,lv.var,lv.term),e); // use Equal because it is polymorphic + } + } +#endif + return e; + } + /** Make an axiom node. The conclusion must be an instance of an axiom. */ virtual node make_axiom(const std::vector &conclusion, prover::range frng){ int nargs = conclusion.size(); @@ -1920,7 +1952,7 @@ class iz3proof_itp_impl : public iz3proof_itp { for(unsigned i = 0; i < eqs.size(); i++) itp = make_mp(eqs[i],itp,pfs[i]); - return itp; + return capture_localization(itp); } virtual node make_axiom(const std::vector &conclusion){ @@ -2405,12 +2437,89 @@ class iz3proof_itp_impl : public iz3proof_itp { return new_var; } + ast delete_quant(hash_map &memo, const ast &v, const ast &e){ + std::pair foo(e,ast()); + std::pair::iterator,bool> bar = memo.insert(foo); + ast &res = bar.first->second; + if(bar.second){ + opr o = op(e); + switch(o){ + case Or: + case And: + case Implies: { + unsigned nargs = num_args(e); + std::vector args; args.resize(nargs); + for(unsigned i = 0; i < nargs; i++) + args[i] = delete_quant(memo, v, arg(e,i)); + res = make(o,args); + break; + } + case Uninterpreted: { + symb s = sym(e); + ast w = arg(arg(e,0),0); + if(s == sforall || s == sexists){ + res = delete_quant(memo,v,arg(e,1)); + if(w != v) + res = make(s,w,res); + break; + } + } + default: + res = e; + } + } + return res; + } + + ast insert_quants(hash_map &memo, const ast &e){ + std::pair foo(e,ast()); + std::pair::iterator,bool> bar = memo.insert(foo); + ast &res = bar.first->second; + if(bar.second){ + opr o = op(e); + switch(o){ + case Or: + case And: + case Implies: { + unsigned nargs = num_args(e); + std::vector args; args.resize(nargs); + for(unsigned i = 0; i < nargs; i++) + args[i] = insert_quants(memo, arg(e,i)); + res = make(o,args); + break; + } + case Uninterpreted: { + symb s = sym(e); + if(s == sforall || s == sexists){ + opr q = (s == sforall) ? Forall : Exists; + ast v = arg(arg(e,0),0); + hash_map dmemo; + ast body = delete_quant(dmemo,v,arg(e,1)); + body = insert_quants(memo,body); + res = apply_quant(q,v,body); + break; + } + } + default: + res = e; + } + } + return res; + } + ast add_quants(ast e){ +#ifdef CAPTURE_LOCALIZATION + if(!localization_vars.empty()){ + hash_map memo; + e = insert_quants(memo,e); + } +#else for(int i = localization_vars.size() - 1; i >= 0; i--){ LocVar &lv = localization_vars[i]; opr quantifier = (pv->in_range(lv.frame,rng)) ? Exists : Forall; e = apply_quant(quantifier,lv.var,e); } +#endif return e; } @@ -2446,7 +2555,7 @@ class iz3proof_itp_impl : public iz3proof_itp { ast npP = make_mp(make(Iff,nPloc,nP),npPloc,neqpf); ast nrP = make_resolution(nP,conj2,npP); ast res = make_resolution(Ploc,rP,nrP); - return res; + return capture_localization(res); } ast get_contra_coeff(const ast &f){ @@ -2538,6 +2647,10 @@ public: m().inc_ref(normal_chain); normal = function("@normal",2,boolbooldom,bool_type()); m().inc_ref(normal); + sforall = function("@sforall",2,boolbooldom,bool_type()); + m().inc_ref(sforall); + sexists = function("@sexists",2,boolbooldom,bool_type()); + m().inc_ref(sexists); } ~iz3proof_itp_impl(){ diff --git a/src/smt/params/qi_params.cpp b/src/smt/params/qi_params.cpp index f5506d35b..60fcd6fc4 100644 --- a/src/smt/params/qi_params.cpp +++ b/src/smt/params/qi_params.cpp @@ -27,6 +27,7 @@ void qi_params::updt_params(params_ref const & _p) { m_mbqi_max_iterations = p.mbqi_max_iterations(); m_mbqi_trace = p.mbqi_trace(); m_mbqi_force_template = p.mbqi_force_template(); + m_mbqi_id = p.mbqi_id(); m_qi_profile = p.qi_profile(); m_qi_profile_freq = p.qi_profile_freq(); m_qi_max_instances = p.qi_max_instances(); diff --git a/src/smt/params/qi_params.h b/src/smt/params/qi_params.h index 0cd817f22..bca3ad3fc 100644 --- a/src/smt/params/qi_params.h +++ b/src/smt/params/qi_params.h @@ -51,6 +51,7 @@ struct qi_params { unsigned m_mbqi_max_iterations; bool m_mbqi_trace; unsigned m_mbqi_force_template; + const char * m_mbqi_id; qi_params(params_ref const & p = params_ref()): /* @@ -97,7 +98,9 @@ struct qi_params { m_mbqi_max_cexs_incr(1), m_mbqi_max_iterations(1000), m_mbqi_trace(false), - m_mbqi_force_template(10) { + m_mbqi_force_template(10), + m_mbqi_id(0) + { updt_params(p); } diff --git a/src/smt/params/smt_params_helper.pyg b/src/smt/params/smt_params_helper.pyg index 07c68f759..50bb6422b 100644 --- a/src/smt/params/smt_params_helper.pyg +++ b/src/smt/params/smt_params_helper.pyg @@ -21,6 +21,7 @@ def_module_params(module_name='smt', ('mbqi.max_iterations', UINT, 1000, 'maximum number of rounds of MBQI'), ('mbqi.trace', BOOL, False, 'generate tracing messages for Model Based Quantifier Instantiation (MBQI). It will display a message before every round of MBQI, and the quantifiers that were not satisfied'), ('mbqi.force_template', UINT, 10, 'some quantifiers can be used as templates for building interpretations for functions. Z3 uses heuristics to decide whether a quantifier will be used as a template or not. Quantifiers with weight >= mbqi.force_template are forced to be used as a template'), + ('mbqi.id', STRING, '', 'Only use model-based instantiation for quantifiers with id\'s beginning with string'), ('qi.profile', BOOL, False, 'profile quantifier instantiation'), ('qi.profile_freq', UINT, UINT_MAX, 'how frequent results are reported by qi.profile'), ('qi.max_instances', UINT, UINT_MAX, 'maximum number of quantifier instantiations'), diff --git a/src/smt/smt_model_checker.cpp b/src/smt/smt_model_checker.cpp index 53f3af961..526447f9f 100644 --- a/src/smt/smt_model_checker.cpp +++ b/src/smt/smt_model_checker.cpp @@ -322,6 +322,7 @@ namespace smt { for (; it != end; ++it) { quantifier * q = *it; + if(!m_qm->mbqi_enabled(q)) continue; if (m_context->is_relevant(q) && m_context->get_assignment(q) == l_true) { if (m_params.m_mbqi_trace && q->get_qid() != symbol::null) { verbose_stream() << "(smt.mbqi :checking " << q->get_qid() << ")\n"; diff --git a/src/smt/smt_quantifier.cpp b/src/smt/smt_quantifier.cpp index d56fe0cff..8fd0e08bc 100644 --- a/src/smt/smt_quantifier.cpp +++ b/src/smt/smt_quantifier.cpp @@ -335,6 +335,10 @@ namespace smt { return m_imp->m_plugin->model_based(); } + bool quantifier_manager::mbqi_enabled(quantifier *q) const { + return m_imp->m_plugin->mbqi_enabled(q); + } + void quantifier_manager::adjust_model(proto_model * m) { m_imp->m_plugin->adjust_model(m); } @@ -434,10 +438,24 @@ namespace smt { virtual bool model_based() const { return m_fparams->m_mbqi; } + virtual bool mbqi_enabled(quantifier *q) const { + if(!m_fparams->m_mbqi_id) return true; + const symbol &s = q->get_qid(); + unsigned len = strlen(m_fparams->m_mbqi_id); + if(s == symbol::null || s.is_numerical()) + return len == 0; + return strncmp(s.bare_str(),m_fparams->m_mbqi_id,len) == 0; + } + + /* Quantifier id's must begin with the prefix specified by + parameter mbqi.id to be instantiated with MBQI. The default + value is the empty string, so all quantifiers are + instantiated. + */ virtual void add(quantifier * q) { - if (m_fparams->m_mbqi) { - m_model_finder->register_quantifier(q); - } + if (m_fparams->m_mbqi && mbqi_enabled(q)) { + m_model_finder->register_quantifier(q); + } } virtual void del(quantifier * q) { diff --git a/src/smt/smt_quantifier.h b/src/smt/smt_quantifier.h index 19113229c..e3d626157 100644 --- a/src/smt/smt_quantifier.h +++ b/src/smt/smt_quantifier.h @@ -75,6 +75,7 @@ namespace smt { }; bool model_based() const; + bool mbqi_enabled(quantifier *q) const; // can mbqi instantiate this quantifier? void adjust_model(proto_model * m); check_model_result check_model(proto_model * m, obj_map const & root2value); @@ -144,6 +145,11 @@ namespace smt { */ virtual bool model_based() const = 0; + /** + \brief Is "model based" instantiate allowed to instantiate this quantifier? + */ + virtual bool mbqi_enabled(quantifier *q) const {return true;} + /** \brief Give a change to the plugin to adjust the interpretation of unintepreted functions. It can basically change the "else" of each uninterpreted function. From 70433869159cfb37f9c2243f5bbb0f7929b0a985 Mon Sep 17 00:00:00 2001 From: Ken McMillan Date: Tue, 10 Dec 2013 14:34:14 -0800 Subject: [PATCH 05/21] enabled extensional arrays in duality and added theory axioms lazily in GreedyReduce --- src/duality/duality.h | 13 ++++++++++++- src/duality/duality_rpfp.cpp | 20 +++++++++++++++++--- src/duality/duality_wrapper.cpp | 4 +++- src/duality/duality_wrapper.h | 3 ++- 4 files changed, 34 insertions(+), 6 deletions(-) diff --git a/src/duality/duality.h b/src/duality/duality.h index 7a1e88f3c..f1e848f0d 100644 --- a/src/duality/duality.h +++ b/src/duality/duality.h @@ -171,6 +171,9 @@ namespace Duality { /** Assert a background axiom. */ virtual void assert_axiom(const expr &axiom) = 0; + /** Get the background axioms. */ + virtual const std::vector &get_axioms() = 0; + /** Return a string describing performance. */ virtual std::string profile() = 0; @@ -182,7 +185,11 @@ namespace Duality { /** Cancel, throw Canceled object if possible. */ virtual void cancel(){ } - LogicSolver(context &c) : aux_solver(c){} + /* Note: aux solver uses extensional array theory, since it + needs to be able to produce counter-models for + interpolants the have array equalities in them. + */ + LogicSolver(context &c) : aux_solver(c,true){} virtual ~LogicSolver(){} }; @@ -208,6 +215,10 @@ namespace Duality { islvr->AssertInterpolationAxiom(axiom); } + const std::vector &get_axioms() { + return islvr->GetInterpolationAxioms(); + } + std::string profile(){ return islvr->profile(); } diff --git a/src/duality/duality_rpfp.cpp b/src/duality/duality_rpfp.cpp index c582e19fc..3fc755d85 100644 --- a/src/duality/duality_rpfp.cpp +++ b/src/duality/duality_rpfp.cpp @@ -1923,8 +1923,14 @@ namespace Duality { // verify check_result res = s.check(lits.size(),&lits[0]); - if(res != unsat) - throw "should be unsat"; + if(res != unsat){ + // 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++) + s.add(theory[i]); + if(s.check(lits.size(),&lits[0]) != unsat) + throw "should be unsat"; + } for(unsigned i = 0; i < conjuncts.size(); ){ std::swap(conjuncts[i],conjuncts.back()); @@ -1987,13 +1993,21 @@ namespace Duality { aux_solver.pop(1); Push(); FixCurrentStateFull(node->Outgoing); - ConstrainEdgeLocalized(node->Outgoing,!GetAnnotation(node)); + // ConstrainEdgeLocalized(node->Outgoing,!GetAnnotation(node)); check_result foo = Check(root); if(foo != unsat) throw "should be unsat"; AddToProofCore(*core); Transformer old_annot = node->Annotation; SolveSingleNode(root,node); + if(node->Annotation.IsEmpty()){ + std::cout << "bad in InterpolateByCase -- core:\n"; + std::vector assumps; + slvr.get_proof().get_assumptions(assumps); + for(unsigned i = 0; i < assumps.size(); i++) + assumps[i].show(); + throw "ack!"; + } Pop(1); node->Annotation.UnionWith(old_annot); } diff --git a/src/duality/duality_wrapper.cpp b/src/duality/duality_wrapper.cpp index 988b03d6d..30531ce51 100644 --- a/src/duality/duality_wrapper.cpp +++ b/src/duality/duality_wrapper.cpp @@ -29,7 +29,7 @@ Revision History: namespace Duality { - solver::solver(Duality::context& c) : object(c), the_model(c) { + solver::solver(Duality::context& c, bool extensional) : object(c), the_model(c) { params_ref p; p.set_bool("proof", true); // this is currently useless p.set_bool("model", true); @@ -37,6 +37,8 @@ namespace Duality { p.set_bool("mbqi",true); 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) + p.set_bool("array.extensional",true); scoped_ptr sf = mk_smt_solver_factory(); m_solver = (*sf)(m(), p, true, true, true, ::symbol::null); m_solver->updt_params(p); // why do we have to do this? diff --git a/src/duality/duality_wrapper.h b/src/duality/duality_wrapper.h index c9860941b..f69bc642e 100755 --- a/src/duality/duality_wrapper.h +++ b/src/duality/duality_wrapper.h @@ -807,7 +807,7 @@ namespace Duality { model the_model; bool canceled; public: - solver(context & c); + solver(context & c, bool extensional = false); solver(context & c, ::solver *s):object(c),the_model(c) { m_solver = s; canceled = false;} solver(solver const & s):object(s), the_model(s.the_model) { m_solver = s.m_solver; canceled = false;} ~solver() { @@ -1326,6 +1326,7 @@ namespace Duality { void SetWeakInterpolants(bool weak); void SetPrintToFile(const std::string &file_name); + const std::vector &GetInterpolationAxioms() {return theory;} const char *profile(); private: From d45cbb3cb2c1de662fd43083b2addf381a6527cf Mon Sep 17 00:00:00 2001 From: Ken McMillan Date: Tue, 10 Dec 2013 16:26:35 -0800 Subject: [PATCH 06/21] fixed interpolation bug --- src/duality/duality_rpfp.cpp | 2 +- src/interp/iz3translate.cpp | 15 +++++++++++++++ 2 files changed, 16 insertions(+), 1 deletion(-) diff --git a/src/duality/duality_rpfp.cpp b/src/duality/duality_rpfp.cpp index 3fc755d85..f37545b48 100644 --- a/src/duality/duality_rpfp.cpp +++ b/src/duality/duality_rpfp.cpp @@ -1993,7 +1993,7 @@ namespace Duality { aux_solver.pop(1); Push(); FixCurrentStateFull(node->Outgoing); - // ConstrainEdgeLocalized(node->Outgoing,!GetAnnotation(node)); + ConstrainEdgeLocalized(node->Outgoing,!GetAnnotation(node)); check_result foo = Check(root); if(foo != unsat) throw "should be unsat"; diff --git a/src/interp/iz3translate.cpp b/src/interp/iz3translate.cpp index 7dfa48cdd..63f3dd251 100755 --- a/src/interp/iz3translate.cpp +++ b/src/interp/iz3translate.cpp @@ -1460,6 +1460,21 @@ public: } } + /* this is the symmetry rule for ~=, that is, takes x ~= y and yields y ~= x. + the proof idiom uses commutativity, monotonicity and mp, but we replace it here + with symmtrey and resolution, that is, we prove y = x |- x = y, then resolve + with the proof of ~(x=y) to get ~y=x. */ + if(dk == PR_MODUS_PONENS && pr(prem(proof,1)) == PR_MONOTONICITY && pr(prem(prem(proof,1),0)) == PR_COMMUTATIVITY && num_prems(prem(proof,1)) == 1){ + Iproof::node ante = translate_main(prem(proof,0),false); + ast eq0 = arg(conc(prem(prem(proof,1),0)),0); + ast eq1 = arg(conc(prem(prem(proof,1),0)),1); + Iproof::node eq1hy = iproof->make_hypothesis(eq1); + Iproof::node eq0pf = iproof->make_symmetry(eq0,eq1,eq1hy); + std::vector clause; // just a dummy + res = iproof->make_resolution(eq0,clause,ante,eq0pf); + return res; + } + // translate all the premises std::vector args(nprems); for(unsigned i = 0; i < nprems; i++) From ea8eb74744f04da7f517d8ef09485b57dc8d330b Mon Sep 17 00:00:00 2001 From: Ken McMillan Date: Wed, 11 Dec 2013 16:25:59 -0800 Subject: [PATCH 07/21] simplifying quantified interpolants in duality --- src/duality/duality.h | 21 ++- src/duality/duality_rpfp.cpp | 235 +++++++++++++++++++++++++++++++++- src/duality/duality_wrapper.h | 2 + 3 files changed, 254 insertions(+), 4 deletions(-) diff --git a/src/duality/duality.h b/src/duality/duality.h index f1e848f0d..4539b4711 100644 --- a/src/duality/duality.h +++ b/src/duality/duality.h @@ -81,10 +81,23 @@ namespace Duality { int CountOperators(const Term &t); + Term SubstAtom(hash_map &memo, const expr &t, const expr &atom, const expr &val); + + Term RemoveRedundancy(const Term &t); + + bool IsLiteral(const expr &lit, expr &atom, expr &val); + + expr Negate(const expr &f); + + expr SimplifyAndOr(const std::vector &args, bool is_and); + private: void SummarizeRec(hash_set &memo, std::vector &lits, int &ops, const Term &t); int CountOperatorsRec(hash_set &memo, const Term &t); + void RemoveRedundancyOp(bool pol, std::vector &args, hash_map &smemo); + Term RemoveRedundancyRec(hash_map &memo, hash_map &smemo, const Term &t); + Term SubstAtomTriv(const expr &foo, const expr &atom, const expr &val); }; @@ -570,7 +583,7 @@ namespace Duality { edge to their values in the current assignment. */ void FixCurrentState(Edge *root); - void FixCurrentStateFull(Edge *edge); + void FixCurrentStateFull(Edge *edge, const expr &extra); /** Declare a constant in the background theory. */ @@ -929,6 +942,12 @@ namespace Duality { void AddToProofCore(hash_set &core); + void GetGroundLitsUnderQuants(hash_set *memo, const Term &f, std::vector &res, int under); + + Term StrengthenFormulaByCaseSplitting(const Term &f, std::vector &case_lits); + + expr NegateLit(const expr &f); + }; /** RPFP solver base class. */ diff --git a/src/duality/duality_rpfp.cpp b/src/duality/duality_rpfp.cpp index f37545b48..5260dc7e9 100644 --- a/src/duality/duality_rpfp.cpp +++ b/src/duality/duality_rpfp.cpp @@ -368,6 +368,136 @@ namespace Duality { return res; } + bool Z3User::IsLiteral(const expr &lit, expr &atom, expr &val){ + if(!lit.is_app()) + return false; + decl_kind k = lit.decl().get_decl_kind(); + if(k == Not){ + if(IsLiteral(lit.arg(0),atom,val)){ + val = eq(val,ctx.bool_val(true)) ? ctx.bool_val(false) : ctx.bool_val(true); + return true; + } + return false; + } + if(k == And || k == Or || k == Iff || k == Implies) + return false; + atom = lit; + val = ctx.bool_val(true); + return true; + } + + expr Z3User::Negate(const expr &f){ + if(f.is_app() && f.decl().get_decl_kind() == Not) + return f.arg(0); + else if(eq(f,ctx.bool_val(true))) + return ctx.bool_val(false); + else if(eq(f,ctx.bool_val(false))) + return ctx.bool_val(true); + return !f; + } + + expr Z3User::SimplifyAndOr(const std::vector &args, bool is_and){ + std::vector sargs; + for(unsigned i = 0; i < args.size(); i++) + if(!eq(args[i],ctx.bool_val(is_and))){ + if(eq(args[i],ctx.bool_val(!is_and))) + return ctx.bool_val(!is_and); + sargs.push_back(args[i]); + } + if(sargs.size() == 0) + return ctx.bool_val(is_and); + if(sargs.size() == 1) + return sargs[0]; + return ctx.make(is_and ? And : Or,sargs); + } + + Z3User::Term Z3User::SubstAtomTriv(const expr &foo, const expr &atom, const expr &val){ + if(eq(foo,atom)) + return val; + else if(foo.is_app() && foo.decl().get_decl_kind() == Not && eq(foo.arg(0),atom)) + return Negate(val); + else + return foo; + } + + Z3User::Term Z3User::SubstAtom(hash_map &memo, const expr &t, const expr &atom, const expr &val){ + 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(); + decl_kind k = f.get_decl_kind(); + + // TODO: recur here, but how much? We don't want to be quadractic in formula size + + if(k == And || k == Or){ + int nargs = t.num_args(); + std::vector args(nargs); + for(int i = 0; i < nargs; i++) + args[i] = SubstAtom(memo,t.arg(i),atom,val); + res = SimplifyAndOr(args,k == And); + return res; + } + } + res = SubstAtomTriv(t,atom,val); + return res; + } + + void Z3User::RemoveRedundancyOp(bool pol, std::vector &args, hash_map &smemo){ + for(unsigned i = 0; i < args.size(); i++){ + const expr &lit = args[i]; + expr atom, val; + if(IsLiteral(lit,atom,val)){ + for(unsigned j = 0; j < args.size(); j++) + if(j != i){ + smemo.clear(); + args[j] = SubstAtom(smemo,args[j],atom,pol ? val : !val); + } + } + } + } + + + Z3User::Term Z3User::RemoveRedundancyRec(hash_map &memo, hash_map &smemo, const Term &t) + { + 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(RemoveRedundancyRec(memo, smemo, t.arg(i))); + + decl_kind k = f.get_decl_kind(); + if(k == And) + RemoveRedundancyOp(true,args,smemo); + else if(k == Or) + RemoveRedundancyOp(false,args,smemo); + if(k == Equal && args[0].get_id() > args[1].get_id()) + std::swap(args[0],args[1]); + + res = f(args.size(),&args[0]); + } + else if (t.is_quantifier()) + { + Term body = RemoveRedundancyRec(memo,smemo,t.body()); + res = clone_quantifier(t, body); + } + else res = t; + return res; + } + + Z3User::Term Z3User::RemoveRedundancy(const Term &t){ + hash_map memo; + hash_map smemo; + return RemoveRedundancyRec(memo,smemo,t); + } + Z3User::Term Z3User::SubstRecHide(hash_map &memo, const Term &t, int number) { std::pair foo(t,expr(ctx)); @@ -1829,18 +1959,100 @@ namespace Duality { ConstrainEdgeLocalized(edge,eu); } - void RPFP::FixCurrentStateFull(Edge *edge){ + 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; + memo[under].insert(f); + if(f.is_app()){ + if(!under && !f.has_quantifiers()) + return; + decl_kind k = f.decl().get_decl_kind(); + if(k == And || k == Or || k == Implies || k == Iff){ + int num_args = f.num_args(); + for(int i = 0; i < num_args; i++) + GetGroundLitsUnderQuants(memo,f.arg(i),res,under); + return; + } + } + else if (f.is_quantifier()){ + GetGroundLitsUnderQuants(memo,f.body(),res,1); + return; + } + if(under && f.is_ground()) + res.push_back(f); + } + + RPFP::Term RPFP::StrengthenFormulaByCaseSplitting(const Term &f, std::vector &case_lits){ + hash_set memo[2]; + std::vector lits; + GetGroundLitsUnderQuants(memo, f, lits, 0); + hash_set lits_hash; + for(unsigned i = 0; i < lits.size(); i++) + lits_hash.insert(lits[i]); + hash_map subst; + hash_map stt_memo; + std::vector conjuncts; + for(unsigned i = 0; i < lits.size(); i++){ + const expr &lit = lits[i]; + if(lits_hash.find(NegateLit(lit)) == lits_hash.end()){ + case_lits.push_back(lit); + bool tval = false; + expr atom = lit; + if(lit.is_app() && lit.decl().get_decl_kind() == Not){ + tval = true; + atom = lit.arg(0); + } + expr etval = ctx.bool_val(tval); + int b = SubtermTruth(stt_memo,atom); + if(b == (tval ? 1 : 0)) + subst[atom] = etval; + else { + if(b == 0 || b == 1){ + etval = ctx.bool_val(b ? true : false); + subst[atom] = etval; + conjuncts.push_back(b ? atom : !atom); + } + } + } + } + expr g = f; + if(!subst.empty()){ + g = SubstRec(subst,f); + if(conjuncts.size()) + g = g && ctx.make(And,conjuncts); + g = g.simplify(); + } +#if 0 + expr g_old = g; + g = RemoveRedundancy(g); + bool changed = !eq(g,g_old); + g = g.simplify(); + if(changed) { // a second pass can get some more simplification + g = RemoveRedundancy(g); + g = g.simplify(); + } +#else + g = RemoveRedundancy(g); + g = g.simplify(); +#endif + return g; + } RPFP::Term RPFP::ModelValueAsConstraint(const Term &t){ if(t.is_array()){ @@ -1948,6 +2160,13 @@ namespace Duality { } } + expr RPFP::NegateLit(const expr &f){ + if(f.is_app() && f.decl().get_decl_kind() == Not) + return f.arg(0); + else + return !f; + } + void RPFP::NegateLits(std::vector &lits){ for(unsigned i = 0; i < lits.size(); i++){ expr &f = lits[i]; @@ -1984,7 +2203,8 @@ namespace Duality { core->insert(node->Outgoing->dual); while(1){ aux_solver.push(); - aux_solver.add(!GetAnnotation(node)); + expr annot = !GetAnnotation(node); + aux_solver.add(annot); if(aux_solver.check() == unsat){ aux_solver.pop(1); break; @@ -1992,7 +2212,7 @@ namespace Duality { dualModel = aux_solver.get_model(); aux_solver.pop(1); Push(); - FixCurrentStateFull(node->Outgoing); + FixCurrentStateFull(node->Outgoing,annot); ConstrainEdgeLocalized(node->Outgoing,!GetAnnotation(node)); check_result foo = Check(root); if(foo != unsat) @@ -2000,6 +2220,15 @@ namespace Duality { AddToProofCore(*core); Transformer old_annot = node->Annotation; SolveSingleNode(root,node); + + { + expr itp = GetAnnotation(node); + dualModel = aux_solver.get_model(); + std::vector case_lits; + itp = StrengthenFormulaByCaseSplitting(itp, case_lits); + SetAnnotation(node,itp); + } + if(node->Annotation.IsEmpty()){ std::cout << "bad in InterpolateByCase -- core:\n"; std::vector assumps; diff --git a/src/duality/duality_wrapper.h b/src/duality/duality_wrapper.h index f69bc642e..e0824d4be 100755 --- a/src/duality/duality_wrapper.h +++ b/src/duality/duality_wrapper.h @@ -457,6 +457,8 @@ namespace Duality { bool is_quantifier() const {return raw()->get_kind() == AST_QUANTIFIER;} bool is_var() const {return raw()->get_kind() == AST_VAR;} bool is_label (bool &pos,std::vector &names) const ; + bool is_ground() const {return to_app(raw())->is_ground();} + bool has_quantifiers() const {return to_app(raw())->has_quantifiers();} // operator Z3_app() const { assert(is_app()); return reinterpret_cast(m_ast); } func_decl decl() const {return func_decl(ctx(),to_app(raw())->get_decl());} From 2cc813219172f702af7b581c2cd90cd22d68d8e7 Mon Sep 17 00:00:00 2001 From: Ken McMillan Date: Thu, 12 Dec 2013 18:25:24 -0800 Subject: [PATCH 08/21] still simplifying quantified interpolants in duality --- src/duality/duality.h | 12 ++- src/duality/duality_rpfp.cpp | 179 ++++++++++++++++++++++++++++------- src/interp/iz3translate.cpp | 37 +++++--- 3 files changed, 183 insertions(+), 45 deletions(-) diff --git a/src/duality/duality.h b/src/duality/duality.h index 4539b4711..82d729104 100644 --- a/src/duality/duality.h +++ b/src/duality/duality.h @@ -91,13 +91,23 @@ namespace Duality { expr SimplifyAndOr(const std::vector &args, bool is_and); + expr ReallySimplifyAndOr(const std::vector &args, bool is_and); + + int MaxIndex(hash_map &memo, const Term &t); + + bool IsClosedFormula(const Term &t); + private: void SummarizeRec(hash_set &memo, std::vector &lits, int &ops, const Term &t); int CountOperatorsRec(hash_set &memo, const Term &t); void RemoveRedundancyOp(bool pol, std::vector &args, hash_map &smemo); Term RemoveRedundancyRec(hash_map &memo, hash_map &smemo, const Term &t); - Term SubstAtomTriv(const expr &foo, const expr &atom, const expr &val); + Term SubstAtomTriv(const expr &foo, const expr &atom, const expr &val); + expr ReduceAndOr(const std::vector &args, bool is_and, std::vector &res); + expr FinishAndOr(const std::vector &args, bool is_and); + expr PullCommonFactors(std::vector &args, bool is_and); + }; diff --git a/src/duality/duality_rpfp.cpp b/src/duality/duality_rpfp.cpp index 5260dc7e9..3fd74993c 100644 --- a/src/duality/duality_rpfp.cpp +++ b/src/duality/duality_rpfp.cpp @@ -25,6 +25,7 @@ Revision History: #include "duality_profiling.h" #include #include +#include #ifndef WIN32 // #define Z3OPS @@ -369,18 +370,20 @@ namespace Duality { } bool Z3User::IsLiteral(const expr &lit, expr &atom, expr &val){ - if(!lit.is_app()) - return false; - decl_kind k = lit.decl().get_decl_kind(); - if(k == Not){ - if(IsLiteral(lit.arg(0),atom,val)){ - val = eq(val,ctx.bool_val(true)) ? ctx.bool_val(false) : ctx.bool_val(true); - return true; + if(!(lit.is_quantifier() && IsClosedFormula(lit))){ + if(!lit.is_app()) + return false; + decl_kind k = lit.decl().get_decl_kind(); + if(k == Not){ + if(IsLiteral(lit.arg(0),atom,val)){ + val = eq(val,ctx.bool_val(true)) ? ctx.bool_val(false) : ctx.bool_val(true); + return true; + } + return false; } - return false; + if(k == And || k == Or || k == Iff || k == Implies) + return false; } - if(k == And || k == Or || k == Iff || k == Implies) - return false; atom = lit; val = ctx.bool_val(true); return true; @@ -396,19 +399,78 @@ namespace Duality { return !f; } - expr Z3User::SimplifyAndOr(const std::vector &args, bool is_and){ - std::vector sargs; + expr Z3User::ReduceAndOr(const std::vector &args, bool is_and, std::vector &res){ for(unsigned i = 0; i < args.size(); i++) if(!eq(args[i],ctx.bool_val(is_and))){ if(eq(args[i],ctx.bool_val(!is_and))) return ctx.bool_val(!is_and); - sargs.push_back(args[i]); + res.push_back(args[i]); } - if(sargs.size() == 0) + return expr(); + } + + expr Z3User::FinishAndOr(const std::vector &args, bool is_and){ + if(args.size() == 0) return ctx.bool_val(is_and); - if(sargs.size() == 1) - return sargs[0]; - return ctx.make(is_and ? And : Or,sargs); + if(args.size() == 1) + return args[0]; + return ctx.make(is_and ? And : Or,args); + } + + expr Z3User::SimplifyAndOr(const std::vector &args, bool is_and){ + std::vector sargs; + expr res = ReduceAndOr(args,is_and,sargs); + if(!res.null()) return res; + return FinishAndOr(sargs,is_and); + } + + expr Z3User::PullCommonFactors(std::vector &args, bool is_and){ + + // first check if there's anything to do... + if(args.size() < 2) + return FinishAndOr(args,is_and); + for(unsigned i = 0; i < args.size(); i++){ + const expr &a = args[i]; + if(!(a.is_app() && a.decl().get_decl_kind() == (is_and ? Or : And))) + return FinishAndOr(args,is_and); + } + std::vector common; + for(unsigned i = 0; i < args.size(); i++){ + unsigned n = args[i].num_args(); + std::vector v(n),w; + for(unsigned j = 0; j < n; j++) + v[j] = args[i].arg(j); + std::less comp; + std::sort(v.begin(),v.end(),comp); + if(i == 0) + common.swap(v); + else { + std::set_intersection(common.begin(),common.end(),v.begin(),v.end(),std::back_inserter(w),comp); + common.swap(w); + } + } + if(common.empty()) + return FinishAndOr(args,is_and); + std::set common_set(common.begin(),common.end()); + for(unsigned i = 0; i < args.size(); i++){ + unsigned n = args[i].num_args(); + std::vector lits; + for(unsigned j = 0; j < n; j++){ + const expr b = args[i].arg(j); + if(common_set.find(b) == common_set.end()) + lits.push_back(b); + } + args[i] = SimplifyAndOr(lits,!is_and); + } + common.push_back(SimplifyAndOr(args,is_and)); + return SimplifyAndOr(common,!is_and); + } + + expr Z3User::ReallySimplifyAndOr(const std::vector &args, bool is_and){ + std::vector sargs; + expr res = ReduceAndOr(args,is_and,sargs); + if(!res.null()) return res; + return PullCommonFactors(sargs,is_and); } Z3User::Term Z3User::SubstAtomTriv(const expr &foo, const expr &atom, const expr &val){ @@ -436,10 +498,17 @@ namespace Duality { std::vector args(nargs); for(int i = 0; i < nargs; i++) args[i] = SubstAtom(memo,t.arg(i),atom,val); - res = SimplifyAndOr(args,k == And); + res = ReallySimplifyAndOr(args, k==And); return res; } } + else if(t.is_quantifier() && atom.is_quantifier()){ + if(eq(t,atom)) + res = val; + else + res = clone_quantifier(t,SubstAtom(memo,t.body(),atom,val)); + return res; + } res = SubstAtomTriv(t,atom,val); return res; } @@ -474,14 +543,19 @@ namespace Duality { args.push_back(RemoveRedundancyRec(memo, smemo, t.arg(i))); decl_kind k = f.get_decl_kind(); - if(k == And) + if(k == And){ RemoveRedundancyOp(true,args,smemo); - else if(k == Or) + res = ReallySimplifyAndOr(args, true); + } + else if(k == Or){ RemoveRedundancyOp(false,args,smemo); - if(k == Equal && args[0].get_id() > args[1].get_id()) - std::swap(args[0],args[1]); - - res = f(args.size(),&args[0]); + res = ReallySimplifyAndOr(args, false); + } + else { + if(k == Equal && args[0].get_id() > args[1].get_id()) + std::swap(args[0],args[1]); + res = f(args.size(),&args[0]); + } } else if (t.is_quantifier()) { @@ -1991,7 +2065,13 @@ namespace Duality { } } else if (f.is_quantifier()){ - GetGroundLitsUnderQuants(memo,f.body(),res,1); +#if 0 + // treat closed quantified formula as a literal 'cause we hate nested quantifiers + if(under && IsClosedFormula(f)) + res.push_back(f); + else +#endif + GetGroundLitsUnderQuants(memo,f.body(),res,1); return; } if(under && f.is_ground()) @@ -2019,14 +2099,18 @@ namespace Duality { atom = lit.arg(0); } expr etval = ctx.bool_val(tval); - int b = SubtermTruth(stt_memo,atom); - if(b == (tval ? 1 : 0)) - subst[atom] = etval; + if(atom.is_quantifier()) + subst[atom] = etval; // this is a bit desperate, since we can't eval quants else { - if(b == 0 || b == 1){ - etval = ctx.bool_val(b ? true : false); + int b = SubtermTruth(stt_memo,atom); + if(b == (tval ? 1 : 0)) subst[atom] = etval; - conjuncts.push_back(b ? atom : !atom); + else { + if(b == 0 || b == 1){ + etval = ctx.bool_val(b ? true : false); + subst[atom] = etval; + conjuncts.push_back(b ? atom : !atom); + } } } } @@ -2038,7 +2122,7 @@ namespace Duality { g = g && ctx.make(And,conjuncts); g = g.simplify(); } -#if 0 +#if 1 expr g_old = g; g = RemoveRedundancy(g); bool changed = !eq(g,g_old); @@ -2441,6 +2525,37 @@ namespace Duality { return SubstBoundRec(memo, subst, 0, t); } + int Z3User::MaxIndex(hash_map &memo, const Term &t) + { + std::pair foo(t,-1); + std::pair::iterator, bool> bar = memo.insert(foo); + int &res = bar.first->second; + if(!bar.second) return res; + if (t.is_app()){ + func_decl f = t.decl(); + int nargs = t.num_args(); + for(int i = 0; i < nargs; i++){ + int m = MaxIndex(memo, t.arg(i)); + if(m > res) + res = m; + } + } + else if (t.is_quantifier()){ + int bound = t.get_quantifier_num_bound(); + res = MaxIndex(memo,t.body()) - bound; + } + else if (t.is_var()) { + res = t.get_index_value(); + } + return res; + } + + bool Z3User::IsClosedFormula(const Term &t){ + hash_map memo; + return MaxIndex(memo,t) < 0; + } + + /** Convert a collection of clauses to Nodes and Edges in the RPFP. Predicate unknowns are uninterpreted predicates not diff --git a/src/interp/iz3translate.cpp b/src/interp/iz3translate.cpp index 63f3dd251..fae914292 100755 --- a/src/interp/iz3translate.cpp +++ b/src/interp/iz3translate.cpp @@ -109,36 +109,49 @@ public: symbols and assign each to a frame. THe assignment is heuristic. */ - void scan_skolems_rec(hash_set &memo, const ast &proof){ - std::pair::iterator,bool> bar = memo.insert(proof); - if(!bar.second) - return; + int scan_skolems_rec(hash_map &memo, const ast &proof, int frame){ + std::pair foo(proof,INT_MAX); + std::pair bar = memo.insert(foo); + int &res = bar.first->second; + if(!bar.second) return res; pfrule dk = pr(proof); - if(dk == PR_SKOLEMIZE){ + if(dk == PR_ASSERTED){ + ast ass = conc(proof); + res = frame_of_assertion(ass); + } + else if(dk == PR_SKOLEMIZE){ ast quanted = arg(conc(proof),0); if(op(quanted) == Not) quanted = arg(quanted,0); - range r = ast_range(quanted); - if(range_is_empty(r)) - r = ast_scope(quanted); + // range r = ast_range(quanted); + // if(range_is_empty(r)) + range r = ast_scope(quanted); if(range_is_empty(r)) throw "can't skolemize"; - int frame = range_max(r); + if(frame == INT_MAX || !in_range(frame,r)) + frame = range_max(r); // this is desperation -- may fail if(frame >= frames) frame = frames - 1; add_frame_range(frame,arg(conc(proof),1)); r = ast_scope(arg(conc(proof),1)); } + else if(dk==PR_MODUS_PONENS_OEQ){ + frame = scan_skolems_rec(memo,prem(proof,0),frame); + scan_skolems_rec(memo,prem(proof,1),frame); + } else { unsigned nprems = num_prems(proof); for(unsigned i = 0; i < nprems; i++){ - scan_skolems_rec(memo,prem(proof,i)); + int bar = scan_skolems_rec(memo,prem(proof,i),frame); + if(res == INT_MAX || res == bar) res = bar; + else if(bar != INT_MAX) res = -1; } } + return res; } void scan_skolems(const ast &proof){ - hash_set memo; - scan_skolems_rec(memo,proof); + hash_map memo; + scan_skolems_rec(memo,proof, INT_MAX); } // determine locality of a proof term From cf3ede92adb26b48496021375034e9db157f5db8 Mon Sep 17 00:00:00 2001 From: Ken McMillan Date: Thu, 12 Dec 2013 18:35:43 -0800 Subject: [PATCH 09/21] fix for broken windows stl --- src/duality/duality_rpfp.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/duality/duality_rpfp.cpp b/src/duality/duality_rpfp.cpp index 3fd74993c..bf6857b68 100644 --- a/src/duality/duality_rpfp.cpp +++ b/src/duality/duality_rpfp.cpp @@ -445,7 +445,7 @@ namespace Duality { if(i == 0) common.swap(v); else { - std::set_intersection(common.begin(),common.end(),v.begin(),v.end(),std::back_inserter(w),comp); + std::set_intersection(common.begin(),common.end(),v.begin(),v.end(),std::inserter(w,w.begin()),comp); common.swap(w); } } From bfa6c9967677655106a178799560fe071379e1fd Mon Sep 17 00:00:00 2001 From: Ken McMillan Date: Thu, 12 Dec 2013 18:38:09 -0800 Subject: [PATCH 10/21] still trying to get stl to work --- src/duality/duality_rpfp.cpp | 1 + 1 file changed, 1 insertion(+) diff --git a/src/duality/duality_rpfp.cpp b/src/duality/duality_rpfp.cpp index bf6857b68..e3f6da63d 100644 --- a/src/duality/duality_rpfp.cpp +++ b/src/duality/duality_rpfp.cpp @@ -26,6 +26,7 @@ Revision History: #include #include #include +#include #ifndef WIN32 // #define Z3OPS From a410e7f7168db5e34c7cd88e0af39dccd7d400d8 Mon Sep 17 00:00:00 2001 From: Ken McMillan Date: Fri, 13 Dec 2013 12:21:54 -0800 Subject: [PATCH 11/21] fussing with qe in duality --- scripts/mk_project.py | 2 +- src/duality/duality.h | 3 ++- src/duality/duality_rpfp.cpp | 8 ++++++++ src/duality/duality_solver.cpp | 2 +- src/duality/duality_wrapper.cpp | 9 +++++++++ src/duality/duality_wrapper.h | 2 ++ 6 files changed, 23 insertions(+), 3 deletions(-) diff --git a/scripts/mk_project.py b/scripts/mk_project.py index 6e352f06f..f2c688525 100644 --- a/scripts/mk_project.py +++ b/scripts/mk_project.py @@ -55,8 +55,8 @@ def init_project_def(): add_lib('fpa', ['core_tactics', 'bv_tactics', 'sat_tactic'], 'tactic/fpa') add_lib('smt_tactic', ['smt'], 'smt/tactic') add_lib('sls_tactic', ['tactic', 'normal_forms', 'core_tactics', 'bv_tactics'], 'tactic/sls') - add_lib('duality', ['smt', 'interp']) add_lib('qe', ['smt','sat'], 'qe') + add_lib('duality', ['smt', 'interp', 'qe']) add_lib('muz', ['smt', 'sat', 'smt2parser', 'aig_tactic', 'qe'], 'muz/base') add_lib('transforms', ['muz', 'hilbert'], 'muz/transforms') add_lib('rel', ['muz', 'transforms'], 'muz/rel') diff --git a/src/duality/duality.h b/src/duality/duality.h index 82d729104..f20d664be 100644 --- a/src/duality/duality.h +++ b/src/duality/duality.h @@ -97,7 +97,8 @@ namespace Duality { bool IsClosedFormula(const Term &t); - private: + Term AdjustQuantifiers(const Term &t); +private: void SummarizeRec(hash_set &memo, std::vector &lits, int &ops, const Term &t); int CountOperatorsRec(hash_set &memo, const Term &t); diff --git a/src/duality/duality_rpfp.cpp b/src/duality/duality_rpfp.cpp index e3f6da63d..ef62d38c1 100644 --- a/src/duality/duality_rpfp.cpp +++ b/src/duality/duality_rpfp.cpp @@ -573,6 +573,13 @@ namespace Duality { return RemoveRedundancyRec(memo,smemo,t); } + Z3User::Term Z3User::AdjustQuantifiers(const Term &t) + { + if(t.is_quantifier() || (t.is_app() && t.has_quantifiers())) + return t.qe_lite(); + return t; + } + Z3User::Term Z3User::SubstRecHide(hash_map &memo, const Term &t, int number) { std::pair foo(t,expr(ctx)); @@ -2136,6 +2143,7 @@ namespace Duality { g = RemoveRedundancy(g); g = g.simplify(); #endif + g = AdjustQuantifiers(g); return g; } diff --git a/src/duality/duality_solver.cpp b/src/duality/duality_solver.cpp index 40ddf25b1..073f4dce9 100644 --- a/src/duality/duality_solver.cpp +++ b/src/duality/duality_solver.cpp @@ -1819,7 +1819,7 @@ namespace Duality { } bool NodeTooComplicated(Node *node){ - return tree->CountOperators(node->Annotation.Formula) > 5; + return tree->CountOperators(node->Annotation.Formula) > 3; } void SimplifyNode(Node *node){ diff --git a/src/duality/duality_wrapper.cpp b/src/duality/duality_wrapper.cpp index 30531ce51..14fe545e0 100644 --- a/src/duality/duality_wrapper.cpp +++ b/src/duality/duality_wrapper.cpp @@ -26,6 +26,7 @@ Revision History: #include "expr_abstract.h" #include "stopwatch.h" #include "model_smt2_pp.h" +#include "qe_lite.h" namespace Duality { @@ -329,6 +330,14 @@ expr context::make_quant(decl_kind op, const std::vector &_sorts, const st return simplify(p); } + expr expr::qe_lite() const { + ::qe_lite qe(m()); + expr_ref result(to_expr(raw()),m()); + proof_ref pf(m()); + qe(result,pf); + return ctx().cook(result); + } + expr clone_quantifier(const expr &q, const expr &b){ return q.ctx().cook(q.m().update_quantifier(to_quantifier(q.raw()), to_expr(b.raw()))); } diff --git a/src/duality/duality_wrapper.h b/src/duality/duality_wrapper.h index e0824d4be..fec1f08d1 100755 --- a/src/duality/duality_wrapper.h +++ b/src/duality/duality_wrapper.h @@ -558,6 +558,8 @@ namespace Duality { expr simplify(params const & p) const; + expr qe_lite() const; + friend expr clone_quantifier(const expr &, const expr &); friend expr clone_quantifier(const expr &q, const expr &b, const std::vector &patterns); From 044959853069d6b134548151500901450db7095c Mon Sep 17 00:00:00 2001 From: Ken McMillan Date: Fri, 13 Dec 2013 12:41:51 -0800 Subject: [PATCH 12/21] fussing more with qe in duality --- src/duality/duality_rpfp.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/duality/duality_rpfp.cpp b/src/duality/duality_rpfp.cpp index ef62d38c1..a5e2b9167 100644 --- a/src/duality/duality_rpfp.cpp +++ b/src/duality/duality_rpfp.cpp @@ -143,7 +143,7 @@ namespace Duality { return 0; } if(t.is_quantifier()) - return CountOperatorsRec(memo,t.body())+1; + return CountOperatorsRec(memo,t.body())+2; // count 2 for a quantifier return 0; } From ac9a7748e827e081cb2c030c23f983fc1d5f972d Mon Sep 17 00:00:00 2001 From: Ken McMillan Date: Fri, 13 Dec 2013 13:14:04 -0800 Subject: [PATCH 13/21] trying to fix address depedency in duality_solver.cpp --- src/duality/duality.h | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/src/duality/duality.h b/src/duality/duality.h index f20d664be..ebf6c8632 100644 --- a/src/duality/duality.h +++ b/src/duality/duality.h @@ -1007,3 +1007,15 @@ private: }; } + +// allow to walk sets of nodes without address dependency + +namespace std { + template <> + class less { + public: + bool operator()(Duality::RPFP::Node * const &s, Duality::RPFP::Node * const &t) const { + return s->number < t->number; // s.raw()->get_id() < t.raw()->get_id(); + } + }; +} From bb61f17989c67812f410d7ff8b067b104759d448 Mon Sep 17 00:00:00 2001 From: Ken McMillan Date: Fri, 13 Dec 2013 13:45:40 -0800 Subject: [PATCH 14/21] trying to figure out address dependency --- src/duality/duality_wrapper.cpp | 9 +++++++++ src/duality/duality_wrapper.h | 1 + 2 files changed, 10 insertions(+) diff --git a/src/duality/duality_wrapper.cpp b/src/duality/duality_wrapper.cpp index 14fe545e0..0b1c688b9 100644 --- a/src/duality/duality_wrapper.cpp +++ b/src/duality/duality_wrapper.cpp @@ -513,6 +513,7 @@ expr context::make_quant(decl_kind op, const std::vector &_sorts, const st opts.set("weak","1"); ::ast *proof = m_solver->get_proof(); + show_assertion_ids(); iz3interpolate(m(),proof,_assumptions,_parents,_interpolants,_theory,&opts); std::vector linearized_interpolants(_interpolants.size()); @@ -613,6 +614,14 @@ 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::show_assertion_ids() { + unsigned n = m_solver->get_num_assertions(); + std::cerr << "assertion ids: "; + for (unsigned i = 0; i < n-1; ++i) + std::cerr << " " << m_solver->get_assertion(i)->get_id(); + std::cerr << "\n"; + } + void include_ast_show(ast &a){ a.show(); } diff --git a/src/duality/duality_wrapper.h b/src/duality/duality_wrapper.h index fec1f08d1..f0988013d 100755 --- a/src/duality/duality_wrapper.h +++ b/src/duality/duality_wrapper.h @@ -907,6 +907,7 @@ namespace Duality { unsigned get_scope_level(){return m_solver->get_scope_level();} void show(); + void show_assertion_ids(); proof get_proof(){ return proof(ctx(),m_solver->get_proof()); From 3764064e98d48d6c720950837579042e28534f8d Mon Sep 17 00:00:00 2001 From: Ken McMillan Date: Fri, 13 Dec 2013 18:41:35 -0800 Subject: [PATCH 15/21] fixed some address dependencies --- src/ast/ast.cpp | 3 +++ src/ast/ast.h | 2 ++ src/duality/duality_wrapper.cpp | 18 +++++++++++++++++- src/duality/duality_wrapper.h | 4 +++- src/interp/iz3interp.cpp | 1 + src/interp/iz3mgr.h | 3 ++- src/util/id_gen.h | 5 +++++ 7 files changed, 33 insertions(+), 3 deletions(-) diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp index bdf1c18db..b000201b7 100644 --- a/src/ast/ast.cpp +++ b/src/ast/ast.cpp @@ -3161,3 +3161,6 @@ void prexpr(expr_ref &e){ std::cout << mk_pp(e.get(), e.get_manager()) << std::endl; } +void ast_manager::show_id_gen(){ + std::cout << "id_gen: " << m_expr_id_gen.show_hash() << " " << m_decl_id_gen.show_hash() << "\n"; +} diff --git a/src/ast/ast.h b/src/ast/ast.h index 2c3843587..68f08e1ac 100644 --- a/src/ast/ast.h +++ b/src/ast/ast.h @@ -1418,6 +1418,8 @@ protected: public: typedef expr_dependency_array_manager::ref expr_dependency_array; + void show_id_gen(); + protected: small_object_allocator m_alloc; family_manager m_family_manager; diff --git a/src/duality/duality_wrapper.cpp b/src/duality/duality_wrapper.cpp index 0b1c688b9..08c5d1f8a 100644 --- a/src/duality/duality_wrapper.cpp +++ b/src/duality/duality_wrapper.cpp @@ -513,7 +513,6 @@ expr context::make_quant(decl_kind op, const std::vector &_sorts, const st opts.set("weak","1"); ::ast *proof = m_solver->get_proof(); - show_assertion_ids(); iz3interpolate(m(),proof,_assumptions,_parents,_interpolants,_theory,&opts); std::vector linearized_interpolants(_interpolants.size()); @@ -604,6 +603,14 @@ expr context::make_quant(decl_kind op, const std::vector &_sorts, const st std::cout << std::endl; } + void model::show_hash() const { + std::ostringstream ss; + model_smt2_pp(ss, m(), *m_model, 0); + std::hash hasher; + unsigned h = hasher(ss.str()); + std::cout << "model hash: " << h << "\n"; + } + void solver::show() { unsigned n = m_solver->get_num_assertions(); if(!n) @@ -615,11 +622,20 @@ expr context::make_quant(decl_kind op, const std::vector &_sorts, const st } void solver::show_assertion_ids() { +#if 0 unsigned n = m_solver->get_num_assertions(); std::cerr << "assertion ids: "; for (unsigned i = 0; i < n-1; ++i) std::cerr << " " << m_solver->get_assertion(i)->get_id(); std::cerr << "\n"; +#else + unsigned n = m_solver->get_num_assertions(); + std::cerr << "assertion ids hash: "; + unsigned h = 0; + for (unsigned i = 0; i < n-1; ++i) + h += m_solver->get_assertion(i)->get_id(); + std::cerr << h << "\n"; +#endif } void include_ast_show(ast &a){ diff --git a/src/duality/duality_wrapper.h b/src/duality/duality_wrapper.h index f0988013d..256560d02 100755 --- a/src/duality/duality_wrapper.h +++ b/src/duality/duality_wrapper.h @@ -727,6 +727,7 @@ namespace Duality { } void show() const; + void show_hash() const; unsigned num_consts() const {return m_model.get()->get_num_constants();} unsigned num_funcs() const {return m_model.get()->get_num_functions();} @@ -1386,7 +1387,8 @@ namespace std { class less { public: bool operator()(const Duality::ast &s, const Duality::ast &t) const { - return s.raw() < t.raw(); // s.raw()->get_id() < t.raw()->get_id(); + // return s.raw() < t.raw(); + return s.raw()->get_id() < t.raw()->get_id(); } }; } diff --git a/src/interp/iz3interp.cpp b/src/interp/iz3interp.cpp index 9196e24d9..56dc1ccec 100755 --- a/src/interp/iz3interp.cpp +++ b/src/interp/iz3interp.cpp @@ -213,6 +213,7 @@ public: test_secondary(cnsts,parents,interps); return; #endif + profiling::timer_start("Interpolation prep"); // get rid of frames not used in proof diff --git a/src/interp/iz3mgr.h b/src/interp/iz3mgr.h index 7bdc2ecce..39c14c724 100644 --- a/src/interp/iz3mgr.h +++ b/src/interp/iz3mgr.h @@ -140,7 +140,8 @@ namespace std { class less { public: bool operator()(const ast_r &s, const ast_r &t) const { - return s.raw() < t.raw(); // s.raw()->get_id() < t.raw()->get_id(); + // return s.raw() < t.raw(); + return s.raw()->get_id() < t.raw()->get_id(); } }; } diff --git a/src/util/id_gen.h b/src/util/id_gen.h index b1713b524..c6d22246d 100644 --- a/src/util/id_gen.h +++ b/src/util/id_gen.h @@ -57,6 +57,11 @@ public: m_free_ids.finalize(); } + unsigned show_hash(){ + unsigned h = string_hash((char *)&m_free_ids[0],m_free_ids.size()*sizeof(unsigned),17); + return hash_u_u(h,m_next_id); + } + /** \brief Return N if the range of ids generated by this module is in the set [0..N) */ From eee2d7af94bf0fcbf7a2b7e5d2f1fa427db4e81d Mon Sep 17 00:00:00 2001 From: Ken McMillan Date: Sat, 14 Dec 2013 12:47:02 -0800 Subject: [PATCH 16/21] porting to linux --- src/duality/duality_wrapper.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/duality/duality_wrapper.cpp b/src/duality/duality_wrapper.cpp index 08c5d1f8a..705d71abe 100644 --- a/src/duality/duality_wrapper.cpp +++ b/src/duality/duality_wrapper.cpp @@ -606,7 +606,7 @@ expr context::make_quant(decl_kind op, const std::vector &_sorts, const st void model::show_hash() const { std::ostringstream ss; model_smt2_pp(ss, m(), *m_model, 0); - std::hash hasher; + stl_ext::hash hasher; unsigned h = hasher(ss.str()); std::cout << "model hash: " << h << "\n"; } From 909408d6ef50dc8ff718ffebef8d21bac408d312 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 15 Dec 2013 10:58:23 +0200 Subject: [PATCH 17/21] fix is_all_int bug Signed-off-by: Nikolaj Bjorner --- src/api/api_interp.cpp | 38 ++++++++++++------------- src/ast/proof_checker/proof_checker.cpp | 11 ++++--- src/smt/theory_arith_aux.h | 5 ++-- 3 files changed, 27 insertions(+), 27 deletions(-) diff --git a/src/api/api_interp.cpp b/src/api/api_interp.cpp index 00503566e..a1d874b4f 100644 --- a/src/api/api_interp.cpp +++ b/src/api/api_interp.cpp @@ -305,8 +305,8 @@ static void get_file_params(const char *filename, hash_map= 0 && eqpos < (int)tok.size()){ + size_t eqpos = tok.find('='); + if(eqpos >= 0 && eqpos < tok.size()){ std::string left = tok.substr(0,eqpos); std::string right = tok.substr(eqpos+1,tok.size()-eqpos-1); params[left] = right; @@ -363,8 +363,8 @@ extern "C" { #else - static Z3_ast and_vec(Z3_context ctx,std::vector &c){ - return (c.size() > 1) ? Z3_mk_and(ctx,c.size(),&c[0]) : c[0]; + static Z3_ast and_vec(Z3_context ctx,svector &c){ + return (c.size() > 1) ? Z3_mk_and(ctx,c.size(),&c[0]) : c[0]; } static Z3_ast parents_vector_to_tree(Z3_context ctx, int num, Z3_ast *cnsts, int *parents){ @@ -381,15 +381,15 @@ extern "C" { } } else { - std::vector > chs(num); + std::vector > chs(num); for(int i = 0; i < num-1; i++){ - std::vector &c = chs[i]; + svector &c = chs[i]; c.push_back(cnsts[i]); Z3_ast foo = Z3_mk_interp(ctx,and_vec(ctx,c)); chs[parents[i]].push_back(foo); } { - std::vector &c = chs[num-1]; + svector &c = chs[num-1]; c.push_back(cnsts[num-1]); res = and_vec(ctx,c); } @@ -454,7 +454,7 @@ extern "C" { static std::string read_msg; static std::vector read_theory; - static bool iZ3_parse(Z3_context ctx, const char *filename, const char **error, std::vector &assertions){ + static bool iZ3_parse(Z3_context ctx, const char *filename, const char **error, svector &assertions){ read_error.clear(); try { std::string foo(filename); @@ -496,26 +496,26 @@ extern "C" { hash_map file_params; get_file_params(filename,file_params); - - int num_theory = 0; + + unsigned num_theory = 0; if(file_params.find("THEORY") != file_params.end()) num_theory = atoi(file_params["THEORY"].c_str()); - std::vector assertions; + svector assertions; if(!iZ3_parse(ctx,filename,error,assertions)) return false; - if(num_theory > (int)assertions.size()) - num_theory = assertions.size(); - int num = assertions.size() - num_theory; + if(num_theory > assertions.size()) + num_theory = assertions.size(); + unsigned num = assertions.size() - num_theory; read_cnsts.resize(num); read_parents.resize(num); read_theory.resize(num_theory); - for(int j = 0; j < num_theory; j++) + for(unsigned j = 0; j < num_theory; j++) read_theory[j] = assertions[j]; - for(int j = 0; j < num; j++) + for(unsigned j = 0; j < num; j++) read_cnsts[j] = assertions[j+num_theory]; if(ret_num_theory) @@ -529,12 +529,12 @@ extern "C" { return true; } - for(int j = 0; j < num; j++) + for(unsigned j = 0; j < num; j++) read_parents[j] = SHRT_MAX; hash_map pred_map; - for(int j = 0; j < num; j++){ + for(unsigned j = 0; j < num; j++){ Z3_ast lhs = 0, rhs = read_cnsts[j]; if(Z3_get_decl_kind(ctx,Z3_get_app_decl(ctx,Z3_to_app(ctx,rhs))) == Z3_OP_IMPLIES){ @@ -588,7 +588,7 @@ extern "C" { } } - for(int j = 0; j < num-1; j++) + for(unsigned j = 0; j < num-1; j++) if(read_parents[j] == SHRT_MIN){ read_error << "formula " << j+1 << ": unreferenced"; goto fail; diff --git a/src/ast/proof_checker/proof_checker.cpp b/src/ast/proof_checker/proof_checker.cpp index 85e0cc791..41c43b26c 100644 --- a/src/ast/proof_checker/proof_checker.cpp +++ b/src/ast/proof_checker/proof_checker.cpp @@ -479,7 +479,7 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) { // otherwise t2 is also a quantifier. return true; } - UNREACHABLE(); + IF_VERBOSE(0, verbose_stream() << "does not match last rule: " << mk_pp(p, m) << "\n";); return false; } case PR_DER: { @@ -488,13 +488,12 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) { match_fact(p, fact) && match_iff(fact.get(), t1, t2) && match_quantifier(t1, is_forall, decls1, body1) && - is_forall && - match_or(body1.get(), terms1)) { + is_forall) { // TBD: check that terms are set of equalities. // t2 is an instance of a predicate in terms1 return true; - } - UNREACHABLE(); + } + IF_VERBOSE(0, verbose_stream() << "does not match last rule: " << mk_pp(p, m) << "\n";); return false; } case PR_HYPOTHESIS: { @@ -832,7 +831,7 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) { } else { IF_VERBOSE(0, verbose_stream() << "Could not establish complementarity for:\n" << - mk_pp(lit1, m) << "\n" << mk_pp(lit2, m) << "\n";); + mk_pp(lit1, m) << "\n" << mk_pp(lit2, m) << "\n" << mk_pp(p, m) << "\n";); } fmls[i] = premise1; } diff --git a/src/smt/theory_arith_aux.h b/src/smt/theory_arith_aux.h index 9f77934e5..7593e9a52 100644 --- a/src/smt/theory_arith_aux.h +++ b/src/smt/theory_arith_aux.h @@ -475,10 +475,11 @@ namespace smt { bool theory_arith::all_coeff_int(row const & r) const { typename vector::const_iterator it = r.begin_entries(); typename vector::const_iterator end = r.end_entries(); - for (; it != end; ++it) { - if (!it->is_dead() && !it->m_coeff.is_int()) + for (; it != end; ++it) { + if (!it->is_dead() && !it->m_coeff.is_int()) { TRACE("gomory_cut", display_row(tout, r, true);); return false; + } } return true; } From ebc8a43fe39f556b7cc47151d201befd446f7f57 Mon Sep 17 00:00:00 2001 From: Ken McMillan Date: Sun, 15 Dec 2013 15:49:06 -0800 Subject: [PATCH 18/21] removing address dependencies --- src/api/api_interp.cpp | 14 ++++++++++++++ src/duality/duality.h | 23 +++++++++++++++++++++++ src/duality/duality_wrapper.h | 3 ++- src/interp/iz3base.h | 9 ++++++++- src/interp/iz3foci.cpp | 9 ++++++++- src/interp/iz3hash.h | 2 ++ src/interp/iz3mgr.h | 4 ++-- src/interp/iz3pp.cpp | 14 ++++++++++++++ src/interp/iz3translate.cpp | 11 +++++++++-- src/interp/iz3translate_direct.cpp | 18 ++++++++++++++++++ 10 files changed, 100 insertions(+), 7 deletions(-) diff --git a/src/api/api_interp.cpp b/src/api/api_interp.cpp index 00503566e..622c7cf94 100644 --- a/src/api/api_interp.cpp +++ b/src/api/api_interp.cpp @@ -42,6 +42,20 @@ Revision History: using namespace stl_ext; #endif +#ifndef WIN32 +// WARNING: don't make a hash_map with this if the range type +// has a destructor: you'll get an address dependency!!! +namespace stl_ext { + template <> + class hash { + public: + size_t operator()(const Z3_ast p) const { + return (size_t) p; + } + }; +} +#endif + typedef interpolation_options_struct *Z3_interpolation_options; extern "C" { diff --git a/src/duality/duality.h b/src/duality/duality.h index ebf6c8632..7729d2175 100644 --- a/src/duality/duality.h +++ b/src/duality/duality.h @@ -1008,6 +1008,29 @@ private: }; } + +// Allow to hash on nodes and edges in deterministic way + +namespace stl_ext { + template <> + class hash { + public: + size_t operator()(const Duality::RPFP::Node *p) const { + return p->number; + } + }; +} + +namespace stl_ext { + template <> + class hash { + public: + size_t operator()(const Duality::RPFP::Edge *p) const { + return p->number; + } + }; +} + // allow to walk sets of nodes without address dependency namespace std { diff --git a/src/duality/duality_wrapper.h b/src/duality/duality_wrapper.h index 256560d02..a36f93b40 100755 --- a/src/duality/duality_wrapper.h +++ b/src/duality/duality_wrapper.h @@ -1419,7 +1419,8 @@ namespace std { class less { public: bool operator()(const Duality::func_decl &s, const Duality::func_decl &t) const { - return s.raw() < t.raw(); // s.raw()->get_id() < t.raw()->get_id(); + // return s.raw() < t.raw(); + return s.raw()->get_id() < t.raw()->get_id(); } }; } diff --git a/src/interp/iz3base.h b/src/interp/iz3base.h index 30ac57bae..e19ae894d 100755 --- a/src/interp/iz3base.h +++ b/src/interp/iz3base.h @@ -146,7 +146,14 @@ class iz3base : public iz3mgr, public scopes { ranges(){scope_computed = false;} }; - stl_ext::hash_map sym_range_hash; + // We only use this for sym_range_hash, which has no range destructor + struct symb_hash { + size_t operator()(const symb &s) const { + return (size_t) s; + } + }; + + stl_ext::hash_map sym_range_hash; stl_ext::hash_map ast_ranges_hash; stl_ext::hash_map simplify_memo; stl_ext::hash_map frame_map; // map assertions to frames diff --git a/src/interp/iz3foci.cpp b/src/interp/iz3foci.cpp index 85e090c5b..fe20f1372 100755 --- a/src/interp/iz3foci.cpp +++ b/src/interp/iz3foci.cpp @@ -51,7 +51,14 @@ public: typedef hash_map NodeToAst; NodeToAst node_to_ast; // maps Z3 ast's to foci expressions - typedef hash_map FuncDeclToSymbol; + // We only use this for FuncDeclToSymbol, which has no range destructor + struct symb_hash { + size_t operator()(const symb &s) const { + return (size_t) s; + } + }; + + typedef hash_map FuncDeclToSymbol; FuncDeclToSymbol func_decl_to_symbol; // maps Z3 func decls to symbols typedef hash_map SymbolToFuncDecl; diff --git a/src/interp/iz3hash.h b/src/interp/iz3hash.h index f6767c037..75d9aa604 100755 --- a/src/interp/iz3hash.h +++ b/src/interp/iz3hash.h @@ -141,6 +141,7 @@ namespace std { #ifndef WIN32 +#if 0 namespace stl_ext { template class hash { @@ -150,6 +151,7 @@ namespace stl_ext { } }; } +#endif #endif diff --git a/src/interp/iz3mgr.h b/src/interp/iz3mgr.h index 39c14c724..645c72ccb 100644 --- a/src/interp/iz3mgr.h +++ b/src/interp/iz3mgr.h @@ -65,7 +65,7 @@ class ast_i { return _ast == other._ast; } bool lt(const ast_i &other) const { - return _ast < other._ast; + return _ast->get_id() < other._ast->get_id(); } friend bool operator==(const ast_i &x, const ast_i&y){ return x.eq(y); @@ -76,7 +76,7 @@ class ast_i { friend bool operator<(const ast_i &x, const ast_i&y){ return x.lt(y); } - size_t hash() const {return (size_t)_ast;} + size_t hash() const {return _ast->get_id();} bool null() const {return !_ast;} }; diff --git a/src/interp/iz3pp.cpp b/src/interp/iz3pp.cpp index 1f9351453..df6fcaf53 100644 --- a/src/interp/iz3pp.cpp +++ b/src/interp/iz3pp.cpp @@ -40,6 +40,20 @@ Revision History: using namespace stl_ext; #endif +#ifndef WIN32 +// We promise not to use this for hash_map with range destructor +namespace stl_ext { + template <> + class hash { + public: + size_t operator()(const expr *p) const { + return (size_t) p; + } + }; +} +#endif + + // TBD: algebraic data-types declarations will not be printed. class free_func_visitor { ast_manager& m; diff --git a/src/interp/iz3translate.cpp b/src/interp/iz3translate.cpp index fae914292..88e4f1174 100755 --- a/src/interp/iz3translate.cpp +++ b/src/interp/iz3translate.cpp @@ -619,7 +619,14 @@ public: return 1; } - void symbols_out_of_scope_rec(hash_set &memo, hash_set &symb_memo, int frame, const ast &t){ + // We only use this for debugging purposes + struct symb_hash { + size_t operator()(const symb &s) const { + return (size_t) s; + } + }; + + void symbols_out_of_scope_rec(hash_set &memo, hash_set &symb_memo, int frame, const ast &t){ if(memo.find(t) != memo.end()) return; memo.insert(t); @@ -638,7 +645,7 @@ public: void symbols_out_of_scope(int frame, const ast &t){ hash_set memo; - hash_set symb_memo; + hash_set symb_memo; symbols_out_of_scope_rec(memo,symb_memo,frame,t); } diff --git a/src/interp/iz3translate_direct.cpp b/src/interp/iz3translate_direct.cpp index 44c907d1d..eaef956b7 100755 --- a/src/interp/iz3translate_direct.cpp +++ b/src/interp/iz3translate_direct.cpp @@ -37,6 +37,24 @@ Revision History: using namespace stl_ext; #endif +#ifndef WIN32 + +/* This can introduce an address dependency if the range type of hash_map has + a destructor. Since the code in this file is not used and only here for + historical comparisons, we allow this non-determinism. + */ +namespace stl_ext { + template + class hash { + public: + size_t operator()(const T *p) const { + return (size_t) p; + } + }; +} + +#endif + static int lemma_count = 0; static int nll_lemma_count = 0; From 852f53d6a6120d56aa8b6c06c53d560645213b71 Mon Sep 17 00:00:00 2001 From: Ken McMillan Date: Sun, 15 Dec 2013 17:24:51 -0800 Subject: [PATCH 19/21] fixed memory error --- src/duality/duality_solver.cpp | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/duality/duality_solver.cpp b/src/duality/duality_solver.cpp index 073f4dce9..13c839186 100644 --- a/src/duality/duality_solver.cpp +++ b/src/duality/duality_solver.cpp @@ -1780,9 +1780,12 @@ namespace Duality { if(std::find(updated_nodes.begin(),updated_nodes.end(),cs[i]) != updated_nodes.end()) throw "help!"; } + } + RemoveLeaves(leaves_to_remove); // have to do this before actually deleting the children + for(unsigned i = 0; i < expansions.size(); i++){ + Node *node = expansions[i]; RemoveExpansion(node); } - RemoveLeaves(leaves_to_remove); stack.pop_back(); if(prev_level_used || stack.size() == 1) break; RemoveUpdateNodesAtCurrentLevel(); // this level is about to be deleted -- remove its children from update list From 1e8c04be8e9384d6163bd2154b8e22f657181c1f Mon Sep 17 00:00:00 2001 From: Ken McMillan Date: Sun, 15 Dec 2013 17:31:46 -0800 Subject: [PATCH 20/21] fixing templates for broken windows hash functions --- src/duality/duality.h | 4 ++-- src/duality/duality_wrapper.cpp | 2 +- src/interp/iz3base.h | 18 ++++++++++-------- src/interp/iz3foci.cpp | 2 +- src/interp/iz3translate.cpp | 11 ++--------- 5 files changed, 16 insertions(+), 21 deletions(-) diff --git a/src/duality/duality.h b/src/duality/duality.h index 7729d2175..979071639 100644 --- a/src/duality/duality.h +++ b/src/duality/duality.h @@ -1011,7 +1011,7 @@ private: // Allow to hash on nodes and edges in deterministic way -namespace stl_ext { +namespace hash_space { template <> class hash { public: @@ -1021,7 +1021,7 @@ namespace stl_ext { }; } -namespace stl_ext { +namespace hash_space { template <> class hash { public: diff --git a/src/duality/duality_wrapper.cpp b/src/duality/duality_wrapper.cpp index 705d71abe..55883202f 100644 --- a/src/duality/duality_wrapper.cpp +++ b/src/duality/duality_wrapper.cpp @@ -606,7 +606,7 @@ expr context::make_quant(decl_kind op, const std::vector &_sorts, const st void model::show_hash() const { std::ostringstream ss; model_smt2_pp(ss, m(), *m_model, 0); - stl_ext::hash hasher; + hash_space::hash hasher; unsigned h = hasher(ss.str()); std::cout << "model hash: " << h << "\n"; } diff --git a/src/interp/iz3base.h b/src/interp/iz3base.h index e19ae894d..7c56b06a6 100755 --- a/src/interp/iz3base.h +++ b/src/interp/iz3base.h @@ -146,14 +146,7 @@ class iz3base : public iz3mgr, public scopes { ranges(){scope_computed = false;} }; - // We only use this for sym_range_hash, which has no range destructor - struct symb_hash { - size_t operator()(const symb &s) const { - return (size_t) s; - } - }; - - stl_ext::hash_map sym_range_hash; + stl_ext::hash_map sym_range_hash; stl_ext::hash_map ast_ranges_hash; stl_ext::hash_map simplify_memo; stl_ext::hash_map frame_map; // map assertions to frames @@ -187,6 +180,15 @@ class iz3base : public iz3mgr, public scopes { }; +namespace hash_space { + template <> + class hash { + public: + size_t operator()(const iz3mgr::symb &s) const { + return (size_t) s; + } + }; +} diff --git a/src/interp/iz3foci.cpp b/src/interp/iz3foci.cpp index fe20f1372..1d81a1b15 100755 --- a/src/interp/iz3foci.cpp +++ b/src/interp/iz3foci.cpp @@ -58,7 +58,7 @@ public: } }; - typedef hash_map FuncDeclToSymbol; + typedef hash_map FuncDeclToSymbol; FuncDeclToSymbol func_decl_to_symbol; // maps Z3 func decls to symbols typedef hash_map SymbolToFuncDecl; diff --git a/src/interp/iz3translate.cpp b/src/interp/iz3translate.cpp index 88e4f1174..fae914292 100755 --- a/src/interp/iz3translate.cpp +++ b/src/interp/iz3translate.cpp @@ -619,14 +619,7 @@ public: return 1; } - // We only use this for debugging purposes - struct symb_hash { - size_t operator()(const symb &s) const { - return (size_t) s; - } - }; - - void symbols_out_of_scope_rec(hash_set &memo, hash_set &symb_memo, int frame, const ast &t){ + void symbols_out_of_scope_rec(hash_set &memo, hash_set &symb_memo, int frame, const ast &t){ if(memo.find(t) != memo.end()) return; memo.insert(t); @@ -645,7 +638,7 @@ public: void symbols_out_of_scope(int frame, const ast &t){ hash_set memo; - hash_set symb_memo; + hash_set symb_memo; symbols_out_of_scope_rec(memo,symb_memo,frame,t); } From 3588d4a1ca94fa0186e9a4fcc05c93173de505e7 Mon Sep 17 00:00:00 2001 From: Ken McMillan Date: Mon, 16 Dec 2013 12:41:43 -0800 Subject: [PATCH 21/21] fixing templates for broken windows hash functions --- src/interp/iz3base.h | 21 ++++++++++----------- 1 file changed, 10 insertions(+), 11 deletions(-) diff --git a/src/interp/iz3base.h b/src/interp/iz3base.h index 7c56b06a6..6bf09bb85 100755 --- a/src/interp/iz3base.h +++ b/src/interp/iz3base.h @@ -24,6 +24,16 @@ Revision History: #include "iz3mgr.h" #include "iz3scopes.h" +namespace hash_space { + template <> + class hash { + public: + size_t operator()(func_decl * const &s) const { + return (size_t) s; + } + }; +} + /* Base class for interpolators. Includes an AST manager and a scoping object as bases. */ @@ -180,17 +190,6 @@ class iz3base : public iz3mgr, public scopes { }; -namespace hash_space { - template <> - class hash { - public: - size_t operator()(const iz3mgr::symb &s) const { - return (size_t) s; - } - }; -} - - #endif