From 48e10a9e2dd19dbd8a47068bab0f6286e8764ad3 Mon Sep 17 00:00:00 2001 From: Ken McMillan Date: Thu, 19 Dec 2013 11:05:56 -0800 Subject: [PATCH 01/12] dealing with incompleteness issues in duality --- src/duality/duality.h | 2 ++ src/duality/duality_rpfp.cpp | 22 ++++++++++++++++------ src/duality/duality_solver.cpp | 8 +++++++- src/interp/iz3translate.cpp | 4 ++++ src/muz/duality/duality_dl_interface.cpp | 3 +++ 5 files changed, 32 insertions(+), 7 deletions(-) diff --git a/src/duality/duality.h b/src/duality/duality.h index 979071639..cc6d81b1a 100644 --- a/src/duality/duality.h +++ b/src/duality/duality.h @@ -1005,6 +1005,8 @@ private: /** Object thrown on cancellation */ struct Canceled {}; + /** Object thrown on incompleteness */ + struct Incompleteness {}; }; } diff --git a/src/duality/duality_rpfp.cpp b/src/duality/duality_rpfp.cpp index a5e2b9167..162175721 100644 --- a/src/duality/duality_rpfp.cpp +++ b/src/duality/duality_rpfp.cpp @@ -2289,6 +2289,7 @@ namespace Duality { } void RPFP::InterpolateByCases(Node *root, Node *node){ + bool axioms_added = false; aux_solver.push(); AddEdgeToSolver(node->Outgoing); node->Annotation.SetEmpty(); @@ -2320,15 +2321,24 @@ namespace Duality { std::vector case_lits; itp = StrengthenFormulaByCaseSplitting(itp, case_lits); SetAnnotation(node,itp); + node->Annotation.Formula.simplify(); } 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!"; + if(!axioms_added){ + // add the axioms in the off chance they are useful + const std::vector &theory = ls->get_axioms(); + for(unsigned i = 0; i < theory.size(); i++) + aux_solver.add(theory[i]); + } + else { + 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_solver.cpp b/src/duality/duality_solver.cpp index 13c839186..6ef9d7746 100644 --- a/src/duality/duality_solver.cpp +++ b/src/duality/duality_solver.cpp @@ -1731,6 +1731,7 @@ namespace Duality { virtual bool Build(){ stack.back().level = tree->slvr.get_scope_level(); + bool was_sat = true; while (true) { @@ -1760,8 +1761,11 @@ namespace Duality { if(RecordUpdate(node)) update_count++; } - if(update_count == 0) + if(update_count == 0){ + if(was_sat) + throw Incompleteness(); reporter->Message("backtracked without learning"); + } } tree->ComputeProofCore(); // need to compute the proof core before popping solver while(1) { @@ -1796,8 +1800,10 @@ namespace Duality { HandleUpdatedNodes(); if(stack.size() == 1) return false; + was_sat = false; } else { + was_sat = true; tree->Push(); std::vector &expansions = stack.back().expansions; for(unsigned i = 0; i < expansions.size(); i++){ diff --git a/src/interp/iz3translate.cpp b/src/interp/iz3translate.cpp index fae914292..2fbc173a9 100755 --- a/src/interp/iz3translate.cpp +++ b/src/interp/iz3translate.cpp @@ -1642,6 +1642,10 @@ public: res = iproof->make_axiom(lits); break; } + case PR_IFF_TRUE: { // turns p into p <-> true, noop for us + res = args[0]; + break; + } default: assert(0 && "translate_main: unsupported proof rule"); throw unsupported(); diff --git a/src/muz/duality/duality_dl_interface.cpp b/src/muz/duality/duality_dl_interface.cpp index 12dd4ff3e..1409212d4 100644 --- a/src/muz/duality/duality_dl_interface.cpp +++ b/src/muz/duality/duality_dl_interface.cpp @@ -213,6 +213,9 @@ lbool dl_interface::query(::expr * query) { catch (Duality::solver::cancel_exception &exn){ throw default_exception("duality canceled"); } + catch (Duality::Solver::Incompleteness &exn){ + throw default_exception("incompleteness"); + } // profile! From c98b853917c857b9b1d434cc647329baf29b9df3 Mon Sep 17 00:00:00 2001 From: Ken McMillan Date: Sat, 21 Dec 2013 16:54:35 -0800 Subject: [PATCH 02/12] speeding up Generalize and adding Lazy Propagation --- src/duality/duality.h | 65 ++++++- src/duality/duality_profiling.cpp | 2 + src/duality/duality_rpfp.cpp | 313 ++++++++++++++++++++++++++---- src/duality/duality_solver.cpp | 127 +++++++++++- src/duality/duality_wrapper.cpp | 5 +- src/duality/duality_wrapper.h | 12 ++ src/interp/iz3proof_itp.cpp | 18 +- 7 files changed, 491 insertions(+), 51 deletions(-) diff --git a/src/duality/duality.h b/src/duality/duality.h index cc6d81b1a..b29a6a610 100644 --- a/src/duality/duality.h +++ b/src/duality/duality.h @@ -98,7 +98,7 @@ namespace Duality { bool IsClosedFormula(const Term &t); Term AdjustQuantifiers(const Term &t); -private: +protected: void SummarizeRec(hash_set &memo, std::vector &lits, int &ops, const Term &t); int CountOperatorsRec(hash_set &memo, const Term &t); @@ -309,7 +309,7 @@ private: LogicSolver *ls; - private: + protected: int nodeCount; int edgeCount; @@ -324,7 +324,7 @@ private: public: model dualModel; - private: + protected: literals dualLabels; std::list stack; std::vector axioms; // only saved here for printing purposes @@ -829,7 +829,7 @@ private: */ void ComputeProofCore(); - private: + protected: void ClearProofCore(){ if(proof_core) @@ -947,6 +947,8 @@ private: expr SimplifyOr(std::vector &lits); + expr SimplifyAnd(std::vector &lits); + void SetAnnotation(Node *root, const expr &t); void AddEdgeToSolver(Edge *edge); @@ -959,9 +961,11 @@ private: expr NegateLit(const expr &f); + expr GetEdgeFormula(Edge *e, int persist, bool with_children, bool underapprox); }; - /** RPFP solver base class. */ + + /** RPFP solver base class. */ class Solver { @@ -1044,3 +1048,54 @@ namespace std { } }; } + +namespace Duality { + /** Caching version of RPFP. Instead of asserting constraints, returns assumption literals */ + + class RPFP_caching : public RPFP { + public: + + /** appends assumption literals for edge to lits. if with_children is true, + includes that annotation of the edge's children. + */ + void AssertEdgeCache(Edge *e, std::vector &lits, bool with_children = false); + + /** appends assumption literals for node to lits */ + void AssertNodeCache(Node *, std::vector lits); + + /** check assumption lits, and return core */ + check_result CheckCore(const std::vector &assumps, std::vector &core); + + /** Clone another RPFP into this one, keeping a map */ + void Clone(RPFP *other); + + /** Get the clone of a node */ + Node *GetNodeClone(Node *other_node); + + /** Get the clone of an edge */ + Edge *GetEdgeClone(Edge *other_edge); + + /** Try to strengthen the parent of an edge */ + void GeneralizeCache(Edge *edge); + + /** Try to propagate some facts from children to parents of edge. + Return true if success. */ + bool PropagateCache(Edge *edge); + + /** Construct a caching RPFP using a LogicSolver */ + RPFP_caching(LogicSolver *_ls) : RPFP(_ls) {} + + protected: + hash_map AssumptionLits; + hash_map NodeCloneMap; + hash_map EdgeCloneMap; + + void GetAssumptionLits(const expr &fmla, std::vector &lits, hash_map *opt_map = 0); + + void GreedyReduceCache(std::vector &assumps, std::vector &core); + + void FilterCore(std::vector &core, std::vector &full_core); + + }; + +} diff --git a/src/duality/duality_profiling.cpp b/src/duality/duality_profiling.cpp index bec32c51a..3b392a91a 100755 --- a/src/duality/duality_profiling.cpp +++ b/src/duality/duality_profiling.cpp @@ -26,6 +26,7 @@ Revision History: #include #include "duality_wrapper.h" +#include "iz3profiling.h" namespace Duality { @@ -103,6 +104,7 @@ namespace Duality { output_time(*pfs, it->second.t); (*pfs) << std::endl; } + profiling::print(os); // print the interpolation stats } void timer_start(const char *name){ diff --git a/src/duality/duality_rpfp.cpp b/src/duality/duality_rpfp.cpp index 162175721..a95561f5d 100644 --- a/src/duality/duality_rpfp.cpp +++ b/src/duality/duality_rpfp.cpp @@ -519,6 +519,20 @@ namespace Duality { const expr &lit = args[i]; expr atom, val; if(IsLiteral(lit,atom,val)){ + if(atom.is_app() && atom.decl().get_decl_kind() == Equal) + if(pol ? eq(val,ctx.bool_val(true)) : eq(val,ctx.bool_val(false))){ + expr lhs = atom.arg(0), rhs = atom.arg(1); + if(lhs.is_numeral()) + std::swap(lhs,rhs); + if(rhs.is_numeral() && lhs.is_app()){ + for(unsigned j = 0; j < args.size(); j++) + if(j != i){ + smemo.clear(); + smemo[lhs] = rhs; + args[j] = SubstRec(smemo,args[j]); + } + } + } for(unsigned j = 0; j < args.size(); j++) if(j != i){ smemo.clear(); @@ -711,6 +725,39 @@ namespace Duality { #endif + expr RPFP::GetEdgeFormula(Edge *e, int persist, bool with_children, bool underapprox) + { + if (e->dual.null()) { + timer_start("ReducedDualEdge"); + e->dual = ReducedDualEdge(e); + timer_stop("ReducedDualEdge"); + timer_start("getting children"); + if(with_children) + for(unsigned i = 0; i < e->Children.size(); i++) + e->dual = e->dual && GetAnnotation(e->Children[i]); + if(underapprox){ + std::vector cus(e->Children.size()); + for(unsigned i = 0; i < e->Children.size(); i++) + cus[i] = !UnderapproxFlag(e->Children[i]) || GetUnderapprox(e->Children[i]); + expr cnst = conjoin(cus); + e->dual = e->dual && cnst; + } + timer_stop("getting children"); + timer_start("Persisting"); + std::list::reverse_iterator it = stack.rbegin(); + for(int i = 0; i < persist && it != stack.rend(); i++) + it++; + if(it != stack.rend()) + it->edges.push_back(e); + timer_stop("Persisting"); + //Console.WriteLine("{0}", cnst); + } + return e->dual; + timer_start("solver add"); + slvr.add(e->dual); + timer_stop("solver add"); + } + /** For incremental solving, asserts the constraint associated * with this edge in the SMT context. If this edge is removed, * you must pop the context accordingly. The second argument is @@ -732,41 +779,40 @@ namespace Duality { { if(eq(e->F.Formula,ctx.bool_val(true)) && (!with_children || e->Children.empty())) return; - if (e->dual.null()) - { - timer_start("ReducedDualEdge"); - e->dual = ReducedDualEdge(e); - timer_stop("ReducedDualEdge"); - timer_start("getting children"); - if(with_children) - for(unsigned i = 0; i < e->Children.size(); i++) - e->dual = e->dual && GetAnnotation(e->Children[i]); - if(underapprox){ - std::vector cus(e->Children.size()); - for(unsigned i = 0; i < e->Children.size(); i++) - cus[i] = !UnderapproxFlag(e->Children[i]) || GetUnderapprox(e->Children[i]); - expr cnst = conjoin(cus); - e->dual = e->dual && cnst; - } - timer_stop("getting children"); - timer_start("Persisting"); - std::list::reverse_iterator it = stack.rbegin(); - for(int i = 0; i < persist && it != stack.rend(); i++) - it++; - if(it != stack.rend()) - it->edges.push_back(e); -#if 0 - if(persist != 0) - Z3_persist_ast(ctx,e->dual,persist); -#endif - timer_stop("Persisting"); - //Console.WriteLine("{0}", cnst); - } + expr fmla = GetEdgeFormula(e, persist, with_children, underapprox); timer_start("solver add"); slvr.add(e->dual); timer_stop("solver add"); } + // caching verion of above + void RPFP_caching::AssertEdgeCache(Edge *e, std::vector &lits, bool with_children){ + if(eq(e->F.Formula,ctx.bool_val(true)) && (!with_children || e->Children.empty())) + return; + expr fmla = GetEdgeFormula(e, 0, with_children, false); + GetAssumptionLits(fmla,lits); + } + + void RPFP_caching::GetAssumptionLits(const expr &fmla, std::vector &lits, hash_map *opt_map){ + std::vector conjs; + CollectConjuncts(fmla,conjs); + for(unsigned i = 0; i < conjs.size(); i++){ + const expr &conj = conjs[i]; + std::pair foo(conj,expr(ctx)); + std::pair::iterator, bool> bar = AssumptionLits.insert(foo); + Term &res = bar.first->second; + if(bar.second){ + func_decl pred = ctx.fresh_func_decl("@alit", ctx.bool_sort()); + res = pred(); + slvr.add(ctx.make(Implies,res,conj)); + // std::cout << res << ": " << conj << "\n"; + } + if(opt_map) + (*opt_map)[res] = conj; + lits.push_back(res); + } + } + void RPFP::ConstrainParent(Edge *parent, Node *child){ ConstrainEdgeLocalized(parent,GetAnnotation(child)); } @@ -786,6 +832,53 @@ namespace Duality { } } + // caching version of above + void RPFP_caching::AssertNodeCache(Node *n, std::vector lits){ + if (n->dual.null()) + { + n->dual = GetUpperBound(n); + stack.back().nodes.push_back(n); + GetAssumptionLits(n->dual,lits); + } + } + + /** Clone another RPFP into this one, keeping a map */ + void RPFP_caching::Clone(RPFP *other){ + for(unsigned i = 0; i < other->nodes.size(); i++) + NodeCloneMap[other->nodes[i]] = CloneNode(other->nodes[i]); + for(unsigned i = 0; i < other->edges.size(); i++){ + Edge *edge = other->edges[i]; + std::vector cs; + for(unsigned j = 0; j < edge->Children.size(); j++) + // cs.push_back(NodeCloneMap[edge->Children[j]]); + cs.push_back(CloneNode(edge->Children[j])); + EdgeCloneMap[edge] = CreateEdge(NodeCloneMap[edge->Parent],edge->F,cs); + } + } + + /** Get the clone of a node */ + RPFP::Node *RPFP_caching::GetNodeClone(Node *other_node){ + return NodeCloneMap[other_node]; + } + + /** Get the clone of an edge */ + RPFP::Edge *RPFP_caching::GetEdgeClone(Edge *other_edge){ + return EdgeCloneMap[other_edge]; + } + + /** check assumption lits, and return core */ + check_result RPFP_caching::CheckCore(const std::vector &assumps, std::vector &core){ + core.resize(assumps.size()); + unsigned core_size; + check_result res = slvr.check(assumps.size(),(expr *)&assumps[0],&core_size,&core[0]); + if(res == unsat) + core.resize(core_size); + else + core.clear(); + return res; + } + + /** Assert a constraint on an edge in the SMT context. */ @@ -970,6 +1063,7 @@ namespace Duality { check_result RPFP::Check(Node *root, std::vector underapproxes, std::vector *underapprox_core ) { + timer_start("Check"); ClearProofCore(); // if (dualModel != null) dualModel.Dispose(); check_result res; @@ -1002,6 +1096,7 @@ namespace Duality { // check_result temp = slvr.check(); } dualModel = slvr.get_model(); + timer_stop("Check"); return res; } @@ -1927,10 +2022,14 @@ namespace Duality { for(int i = 0; i < num_args; i++) CollectConjuncts(f.arg(i),lits,false); } - else if(pos) - lits.push_back(f); - else - lits.push_back(!f); + else if(pos){ + if(!eq(f,ctx.bool_val(true))) + lits.push_back(f); + } + else { + if(!eq(f,ctx.bool_val(false))) + lits.push_back(!f); + } } struct TermLt { @@ -2253,6 +2352,45 @@ namespace Duality { } } + void RPFP_caching::FilterCore(std::vector &core, std::vector &full_core){ + hash_set core_set; + std::copy(full_core.begin(),full_core.end(),std::inserter(core_set,core_set.begin())); + std::vector new_core; + for(unsigned i = 0; i < core.size(); i++) + if(core_set.find(core[i]) != core_set.end()) + new_core.push_back(core[i]); + core.swap(new_core); + } + + void RPFP_caching::GreedyReduceCache(std::vector &assumps, std::vector &core){ + std::vector lits = assumps, full_core; + std::copy(core.begin(),core.end(),std::inserter(lits,lits.end())); + + // verify + check_result res = CheckCore(lits,full_core); + if(res != unsat) + throw "should be unsat"; + FilterCore(core,full_core); + + std::vector dummy; + if(CheckCore(full_core,dummy) != unsat) + throw "should be unsat"; + + for(unsigned i = 0; i < core.size(); ){ + expr temp = core[i]; + std::swap(core[i],core.back()); + core.pop_back(); + lits.resize(assumps.size()); + std::copy(core.begin(),core.end(),std::inserter(lits,lits.end())); + res = CheckCore(lits,full_core); + if(res != unsat){ + core.push_back(temp); + std::swap(core[i],core.back()); + i++; + } + } + } + expr RPFP::NegateLit(const expr &f){ if(f.is_app() && f.decl().get_decl_kind() == Not) return f.arg(0); @@ -2278,6 +2416,14 @@ namespace Duality { return ctx.make(Or,lits); } + expr RPFP::SimplifyAnd(std::vector &lits){ + if(lits.size() == 0) + return ctx.bool_val(true); + if(lits.size() == 1) + return lits[0]; + return ctx.make(And,lits); + } + // set up edge constraint in aux solver void RPFP::AddEdgeToSolver(Edge *edge){ if(!edge->dual.null()) @@ -2321,7 +2467,7 @@ namespace Duality { std::vector case_lits; itp = StrengthenFormulaByCaseSplitting(itp, case_lits); SetAnnotation(node,itp); - node->Annotation.Formula.simplify(); + node->Annotation.Formula = node->Annotation.Formula.simplify(); } if(node->Annotation.IsEmpty()){ @@ -2330,6 +2476,7 @@ namespace Duality { const std::vector &theory = ls->get_axioms(); for(unsigned i = 0; i < theory.size(); i++) aux_solver.add(theory[i]); + axioms_added = true; } else { std::cout << "bad in InterpolateByCase -- core:\n"; @@ -2350,6 +2497,7 @@ namespace Duality { } void RPFP::Generalize(Node *root, Node *node){ + timer_start("Generalize"); aux_solver.push(); AddEdgeToSolver(node->Outgoing); expr fmla = GetAnnotation(node); @@ -2359,8 +2507,103 @@ namespace Duality { aux_solver.pop(1); NegateLits(conjuncts); SetAnnotation(node,SimplifyOr(conjuncts)); + timer_stop("Generalize"); } + + // caching version of above + void RPFP_caching::GeneralizeCache(Edge *edge){ + timer_start("Generalize"); + Node *node = edge->Parent; + std::vector assumps, core, conjuncts; + AssertEdgeCache(edge,assumps); + for(unsigned i = 0; i < edge->Children.size(); i++){ + expr ass = GetAnnotation(edge->Children[i]); + std::vector clauses; + CollectConjuncts(ass.arg(1),clauses); + for(unsigned j = 0; j < clauses.size(); j++) + GetAssumptionLits(ass.arg(0) || clauses[j],assumps); + } + expr fmla = GetAnnotation(node); + assumps.push_back(fmla.arg(0).arg(0)); + std::vector lits; + CollectConjuncts(!fmla.arg(1),lits); +#if 0 + for(unsigned i = 0; i < lits.size(); i++){ + const expr &lit = lits[i]; + if(lit.is_app() && lit.decl().get_decl_kind() == Equal){ + lits[i] = ctx.make(Leq,lit.arg(0),lit.arg(1)); + lits.push_back(ctx.make(Leq,lit.arg(1),lit.arg(0))); + } + } +#endif + hash_map lit_map; + for(unsigned i = 0; i < lits.size(); i++) + GetAssumptionLits(lits[i],core,&lit_map); + GreedyReduceCache(assumps,core); + for(unsigned i = 0; i < core.size(); i++) + conjuncts.push_back(lit_map[core[i]]); + NegateLits(conjuncts); + SetAnnotation(node,SimplifyOr(conjuncts)); + timer_stop("Generalize"); + } + + // caching version of above + bool RPFP_caching::PropagateCache(Edge *edge){ + timer_start("PropagateCache"); + bool some = false; + { + std::vector candidates, skip; + Node *node = edge->Parent; + CollectConjuncts(node->Annotation.Formula,skip); + for(unsigned i = 0; i < edge->Children.size(); i++){ + Node *child = edge->Children[i]; + if(child->map == node->map){ + CollectConjuncts(child->Annotation.Formula,candidates); + break; + } + } + if(candidates.empty()) goto done; + hash_set skip_set; + std::copy(skip.begin(),skip.end(),std::inserter(skip_set,skip_set.begin())); + std::vector new_candidates; + for(unsigned i = 0; i < candidates.size(); i++) + if(skip_set.find(candidates[i]) == skip_set.end()) + new_candidates.push_back(candidates[i]); + candidates.swap(new_candidates); + if(candidates.empty()) goto done; + std::vector assumps, core, conjuncts; + AssertEdgeCache(edge,assumps); + for(unsigned i = 0; i < edge->Children.size(); i++){ + expr ass = GetAnnotation(edge->Children[i]); + std::vector clauses; + CollectConjuncts(ass.arg(1),clauses); + for(unsigned j = 0; j < clauses.size(); j++) + GetAssumptionLits(ass.arg(0) || clauses[j],assumps); + } + for(unsigned i = 0; i < candidates.size(); i++){ + unsigned old_size = assumps.size(); + node->Annotation.Formula = candidates[i]; + expr fmla = GetAnnotation(node); + assumps.push_back(fmla.arg(0).arg(0)); + GetAssumptionLits(!fmla.arg(1),assumps); + std::vector full_core; + check_result res = CheckCore(assumps,full_core); + if(res == unsat) + conjuncts.push_back(candidates[i]); + assumps.resize(old_size); + } + if(conjuncts.empty()) + goto done; + SetAnnotation(node,SimplifyAnd(conjuncts)); + some = true; + } + done: + timer_stop("PropagateCache"); + return some; + } + + /** Push a scope. Assertions made after Push can be undone by Pop. */ void RPFP::Push() diff --git a/src/duality/duality_solver.cpp b/src/duality/duality_solver.cpp index 6ef9d7746..7318b020d 100644 --- a/src/duality/duality_solver.cpp +++ b/src/duality/duality_solver.cpp @@ -44,7 +44,7 @@ Revision History: // #define TOP_DOWN // #define EFFORT_BOUNDED_STRAT #define SKIP_UNDERAPPROX_NODES - +#define USE_RPFP_CLONE namespace Duality { @@ -115,8 +115,25 @@ namespace Duality { Report = false; StratifiedInlining = false; RecursionBound = -1; +#ifdef USE_RPFP_CLONE + clone_ls = new RPFP::iZ3LogicSolver(ctx); + clone_rpfp = new RPFP_caching(clone_ls); + clone_rpfp->Clone(rpfp); +#endif } + ~Duality(){ +#ifdef USE_RPFP_CLONE + delete clone_rpfp; + delete clone_ls; +#endif + } + +#ifdef USE_RPFP_CLONE + RPFP::LogicSolver *clone_ls; + RPFP_caching *clone_rpfp; +#endif + typedef RPFP::Node Node; typedef RPFP::Edge Edge; @@ -1309,6 +1326,7 @@ namespace Duality { node. */ bool SatisfyUpperBound(Node *node){ if(node->Bound.IsFull()) return true; + Propagate(); reporter->Bound(node); int start_decs = rpfp->CumulativeDecisions(); DerivationTree *dtp = new DerivationTreeSlow(this,unwinding,reporter,heuristic,FullExpand); @@ -1412,6 +1430,70 @@ namespace Duality { } } + // Propagate conjuncts up the unwinding + void Propagate(){ + reporter->Message("beginning propagation"); + timer_start("Propagate"); + std::vector sorted_nodes = unwinding->nodes; + std::sort(sorted_nodes.begin(),sorted_nodes.end(),std::less()); // sorts by sequence number + hash_map > facts; + for(unsigned i = 0; i < sorted_nodes.size(); i++){ + Node *node = sorted_nodes[i]; + std::set &node_facts = facts[node->map]; + if(!(node->Outgoing && indset->Contains(node))) + continue; + std::vector conj_vec; + unwinding->CollectConjuncts(node->Annotation.Formula,conj_vec); + std::set conjs; + std::copy(conj_vec.begin(),conj_vec.end(),std::inserter(conjs,conjs.begin())); + if(!node_facts.empty()){ + RPFP *checker = new RPFP(rpfp->ls); + slvr.push(); + Node *root = checker->CloneNode(node); + Edge *edge = node->Outgoing; + // checker->AssertNode(root); + std::vector cs; + for(unsigned j = 0; j < edge->Children.size(); j++){ + Node *oc = edge->Children[j]; + Node *nc = checker->CloneNode(oc); + nc->Annotation = oc->Annotation; // is this needed? + cs.push_back(nc); + } + Edge *checker_edge = checker->CreateEdge(root,edge->F,cs); + checker->AssertEdge(checker_edge, 0, true, false); + std::vector propagated; + for(std::set ::iterator it = node_facts.begin(), en = node_facts.end(); it != en;){ + const expr &fact = *it; + if(conjs.find(fact) == conjs.end()){ + root->Bound.Formula = fact; + slvr.push(); + checker->AssertNode(root); + check_result res = checker->Check(root); + slvr.pop(); + if(res != unsat){ + std::set ::iterator victim = it; + ++it; + node_facts.erase(victim); // if it ain't true, nix it + continue; + } + propagated.push_back(fact); + } + ++it; + } + slvr.pop(); + for(unsigned i = 0; i < propagated.size(); i++){ + root->Annotation.Formula = propagated[i]; + UpdateNodeToNode(node,root); + } + delete checker; + } + for(std::set ::iterator it = conjs.begin(), en = conjs.end(); it != en; ++it){ + expr foo = *it; + node_facts.insert(foo); + } + } + timer_stop("Propagate"); + } /** This class represents a derivation tree. */ class DerivationTree { @@ -1757,7 +1839,9 @@ namespace Duality { tree->SolveSingleNode(top,node); if(expansions.size() == 1 && NodeTooComplicated(node)) SimplifyNode(node); - tree->Generalize(top,node); + else + node->Annotation.Formula = tree->RemoveRedundancy(node->Annotation.Formula).simplify(); + Generalize(node); if(RecordUpdate(node)) update_count++; } @@ -1791,7 +1875,14 @@ namespace Duality { RemoveExpansion(node); } stack.pop_back(); - if(prev_level_used || stack.size() == 1) break; + if(stack.size() == 1)break; + if(prev_level_used){ + Node *node = stack.back().expansions[0]; + if(!Propagate(node)) break; + if(!RecordUpdate(node)) break; // shouldn't happen! + RemoveUpdateNodesAtCurrentLevel(); // this level is about to be deleted -- remove its children from update list + continue; + } 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++) @@ -1833,8 +1924,10 @@ namespace Duality { void SimplifyNode(Node *node){ // have to destroy the old proof to get a new interpolant + timer_start("SimplifyNode"); tree->PopPush(); tree->InterpolateByCases(top,node); + timer_stop("SimplifyNode"); } bool LevelUsedInProof(unsigned level){ @@ -1933,6 +2026,34 @@ namespace Duality { throw "can't unmap node"; } + void Generalize(Node *node){ +#ifndef USE_RPFP_CLONE + tree->Generalize(top,node); +#else + RPFP_caching *clone_rpfp = duality->clone_rpfp; + Edge *clone_edge = clone_rpfp->GetEdgeClone(node->Outgoing->map); + Node *clone_node = clone_edge->Parent; + clone_node->Annotation = node->Annotation; + for(unsigned i = 0; i < clone_edge->Children.size(); i++) + clone_edge->Children[i]->Annotation = node->map->Outgoing->Children[i]->Annotation; + clone_rpfp->GeneralizeCache(clone_edge); + node->Annotation = clone_node->Annotation; + } +#endif + + bool Propagate(Node *node){ + RPFP_caching *clone_rpfp = duality->clone_rpfp; + Edge *clone_edge = clone_rpfp->GetEdgeClone(node->Outgoing->map); + Node *clone_node = clone_edge->Parent; + clone_node->Annotation = node->map->Annotation; + for(unsigned i = 0; i < clone_edge->Children.size(); i++) + clone_edge->Children[i]->Annotation = node->map->Outgoing->Children[i]->Annotation; + bool res = clone_rpfp->PropagateCache(clone_edge); + if(res) + node->Annotation = clone_node->Annotation; + return res; + } + }; diff --git a/src/duality/duality_wrapper.cpp b/src/duality/duality_wrapper.cpp index 55883202f..26bdf52d7 100644 --- a/src/duality/duality_wrapper.cpp +++ b/src/duality/duality_wrapper.cpp @@ -504,7 +504,10 @@ expr context::make_quant(decl_kind op, const std::vector &_sorts, const st add(linear_assumptions[i][j]); } - check_result res = check(); + check_result res = unsat; + + if(!m_solver->get_proof()) + res = check(); if(res == unsat){ diff --git a/src/duality/duality_wrapper.h b/src/duality/duality_wrapper.h index a36f93b40..fa4eca77b 100755 --- a/src/duality/duality_wrapper.h +++ b/src/duality/duality_wrapper.h @@ -1393,6 +1393,18 @@ namespace std { }; } +// to make Duality::ast usable in ordered collections +namespace std { + template <> + class less { + public: + bool operator()(const Duality::expr &s, const Duality::expr &t) const { + // return s.raw() < t.raw(); + return s.raw()->get_id() < t.raw()->get_id(); + } + }; +} + // to make Duality::func_decl hashable namespace hash_space { template <> diff --git a/src/interp/iz3proof_itp.cpp b/src/interp/iz3proof_itp.cpp index 75d14bca1..8b78a7135 100644 --- a/src/interp/iz3proof_itp.cpp +++ b/src/interp/iz3proof_itp.cpp @@ -2170,7 +2170,8 @@ class iz3proof_itp_impl : public iz3proof_itp { for(unsigned i = 0; i < prem_cons.size(); i++){ const ast &lit = prem_cons[i]; if(get_term_type(lit) == LitA) - linear_comb(thing,coeffs[i],lit); + // Farkas rule seems to assume strict integer inequalities are rounded + linear_comb(thing,coeffs[i],lit,true /*round_off*/); } thing = simplify_ineq(thing); for(unsigned i = 0; i < prem_cons.size(); i++){ @@ -2195,9 +2196,9 @@ class iz3proof_itp_impl : public iz3proof_itp { /** Set P to P + cQ, where P and Q are linear inequalities. Assumes P is 0 <= y or 0 < y. */ - void linear_comb(ast &P, const ast &c, const ast &Q){ + void linear_comb(ast &P, const ast &c, const ast &Q, bool round_off = false){ ast Qrhs; - bool strict = op(P) == Lt; + bool qstrict = false; if(is_not(Q)){ ast nQ = arg(Q,0); switch(op(nQ)){ @@ -2209,11 +2210,11 @@ class iz3proof_itp_impl : public iz3proof_itp { break; case Geq: Qrhs = make(Sub,arg(nQ,1),arg(nQ,0)); - strict = true; + qstrict = true; break; case Leq: Qrhs = make(Sub,arg(nQ,0),arg(nQ,1)); - strict = true; + qstrict = true; break; default: throw proof_error(); @@ -2229,17 +2230,20 @@ class iz3proof_itp_impl : public iz3proof_itp { break; case Lt: Qrhs = make(Sub,arg(Q,1),arg(Q,0)); - strict = true; + qstrict = true; break; case Gt: Qrhs = make(Sub,arg(Q,0),arg(Q,1)); - strict = true; + qstrict = true; break; default: throw proof_error(); } } Qrhs = make(Times,c,Qrhs); + bool pstrict = op(P) == Lt, strict = pstrict || qstrict; + if(pstrict && qstrict && round_off) + Qrhs = make(Sub,Qrhs,make_int(rational(1))); if(strict) P = make(Lt,arg(P,0),make(Plus,arg(P,1),Qrhs)); else From 9e88691c69ef4f9c7f1059c225a343c9a3e5861d Mon Sep 17 00:00:00 2001 From: Ken McMillan Date: Sun, 22 Dec 2013 18:33:40 -0800 Subject: [PATCH 03/12] optimizing solver performance in duality --- src/duality/duality.h | 45 +++++- src/duality/duality_rpfp.cpp | 169 +++++++++++++++++++---- src/duality/duality_solver.cpp | 128 +++++++++++++++-- src/duality/duality_wrapper.cpp | 1 + src/duality/duality_wrapper.h | 18 ++- src/muz/duality/duality_dl_interface.cpp | 1 - 6 files changed, 311 insertions(+), 51 deletions(-) diff --git a/src/duality/duality.h b/src/duality/duality.h index b29a6a610..b88e5011f 100644 --- a/src/duality/duality.h +++ b/src/duality/duality.h @@ -350,7 +350,7 @@ protected: proof_core = 0; } - ~RPFP(); + virtual ~RPFP(); /** Symbolic representation of a relational transformer */ class Transformer @@ -962,6 +962,22 @@ protected: expr NegateLit(const expr &f); expr GetEdgeFormula(Edge *e, int persist, bool with_children, bool underapprox); + + virtual void slvr_add(const expr &e); + + virtual void slvr_pop(int i); + + virtual void slvr_push(); + + virtual check_result slvr_check(unsigned n = 0, expr * const assumptions = 0, unsigned *core_size = 0, expr *core = 0); + + virtual lbool ls_interpolate_tree(TermTree *assumptions, + TermTree *&interpolants, + model &_model, + TermTree *goals = 0, + bool weak = false); + + virtual bool proof_core_contains(const expr &e); }; @@ -1085,16 +1101,43 @@ namespace Duality { /** Construct a caching RPFP using a LogicSolver */ RPFP_caching(LogicSolver *_ls) : RPFP(_ls) {} + /** Constraint an edge by its child's annotation. Return + assumption lits. */ + void ConstrainParentCache(Edge *parent, Node *child, std::vector &lits); + + virtual ~RPFP_caching(){} + protected: hash_map AssumptionLits; hash_map NodeCloneMap; hash_map EdgeCloneMap; + std::vector alit_stack; + std::vector alit_stack_sizes; void GetAssumptionLits(const expr &fmla, std::vector &lits, hash_map *opt_map = 0); void GreedyReduceCache(std::vector &assumps, std::vector &core); void FilterCore(std::vector &core, std::vector &full_core); + void ConstrainEdgeLocalizedCache(Edge *e, const Term &tl, std::vector &lits); + + virtual void slvr_add(const expr &e); + + virtual void slvr_pop(int i); + + virtual void slvr_push(); + + virtual check_result slvr_check(unsigned n = 0, expr * const assumptions = 0, unsigned *core_size = 0, expr *core = 0); + + virtual lbool ls_interpolate_tree(TermTree *assumptions, + TermTree *&interpolants, + model &_model, + TermTree *goals = 0, + bool weak = false); + + virtual bool proof_core_contains(const expr &e); + + void GetTermTreeAssertionLiterals(TermTree *assumptions); }; diff --git a/src/duality/duality_rpfp.cpp b/src/duality/duality_rpfp.cpp index a95561f5d..04b4d075e 100644 --- a/src/duality/duality_rpfp.cpp +++ b/src/duality/duality_rpfp.cpp @@ -732,9 +732,6 @@ namespace Duality { e->dual = ReducedDualEdge(e); timer_stop("ReducedDualEdge"); timer_start("getting children"); - if(with_children) - for(unsigned i = 0; i < e->Children.size(); i++) - e->dual = e->dual && GetAnnotation(e->Children[i]); if(underapprox){ std::vector cus(e->Children.size()); for(unsigned i = 0; i < e->Children.size(); i++) @@ -753,9 +750,6 @@ namespace Duality { //Console.WriteLine("{0}", cnst); } return e->dual; - timer_start("solver add"); - slvr.add(e->dual); - timer_stop("solver add"); } /** For incremental solving, asserts the constraint associated @@ -781,8 +775,11 @@ namespace Duality { return; expr fmla = GetEdgeFormula(e, persist, with_children, underapprox); timer_start("solver add"); - slvr.add(e->dual); + slvr_add(e->dual); timer_stop("solver add"); + if(with_children) + for(unsigned i = 0; i < e->Children.size(); i++) + ConstrainParent(e,e->Children[i]); } // caching verion of above @@ -791,8 +788,97 @@ namespace Duality { return; expr fmla = GetEdgeFormula(e, 0, with_children, false); GetAssumptionLits(fmla,lits); + if(with_children) + for(unsigned i = 0; i < e->Children.size(); i++) + ConstrainParentCache(e,e->Children[i],lits); } + void RPFP::slvr_add(const expr &e){ + slvr.add(e); + } + + void RPFP_caching::slvr_add(const expr &e){ + GetAssumptionLits(e,alit_stack); + } + + void RPFP::slvr_pop(int i){ + slvr.pop(i); + } + + void RPFP::slvr_push(){ + slvr.push(); + } + + void RPFP_caching::slvr_pop(int i){ + for(int j = 0; j < i; j++){ + alit_stack.resize(alit_stack_sizes.back()); + alit_stack_sizes.pop_back(); + } + } + + void RPFP_caching::slvr_push(){ + alit_stack_sizes.push_back(alit_stack.size()); + } + + check_result RPFP::slvr_check(unsigned n, expr * const assumptions, unsigned *core_size, expr *core){ + return slvr.check(n, assumptions, core_size, core); + } + + check_result RPFP_caching::slvr_check(unsigned n, expr * const assumptions, unsigned *core_size, expr *core){ + slvr_push(); + if(n && assumptions) + std::copy(assumptions,assumptions+n,std::inserter(alit_stack,alit_stack.end())); + check_result res; + if(core_size && core){ + std::vector full_core(alit_stack.size()), core1(n); + std::copy(assumptions,assumptions+n,core1.begin()); + res = slvr.check(alit_stack.size(), &alit_stack[0], core_size, &full_core[0]); + full_core.resize(*core_size); + if(res == unsat){ + FilterCore(core1,full_core); + *core_size = core1.size(); + std::copy(core1.begin(),core1.end(),core); + } + } + else + res = slvr.check(alit_stack.size(), &alit_stack[0]); + slvr_pop(1); + return res; + } + + lbool RPFP::ls_interpolate_tree(TermTree *assumptions, + TermTree *&interpolants, + model &_model, + TermTree *goals, + bool weak){ + return ls->interpolate_tree(assumptions, interpolants, _model, goals, weak); + } + + lbool RPFP_caching::ls_interpolate_tree(TermTree *assumptions, + TermTree *&interpolants, + model &_model, + TermTree *goals, + bool weak){ + GetTermTreeAssertionLiterals(assumptions); + return ls->interpolate_tree(assumptions, interpolants, _model, goals, weak); + } + + void RPFP_caching::GetTermTreeAssertionLiterals(TermTree *assumptions){ + std::vector alits; + hash_map map; + GetAssumptionLits(assumptions->getTerm(),alits,&map); + std::vector &ts = assumptions->getTerms(); + for(unsigned i = 0; i < ts.size(); i++) + GetAssumptionLits(ts[i],alits,&map); + assumptions->setTerm(ctx.bool_val(true)); + ts = alits; + for(unsigned i = 0; i < alits.size(); i++) + ts.push_back(ctx.make(Implies,alits[i],map[alits[i]])); + for(unsigned i = 0; i < assumptions->getChildren().size(); i++) + GetTermTreeAssertionLiterals(assumptions->getChildren()[i]); + return; + } + void RPFP_caching::GetAssumptionLits(const expr &fmla, std::vector &lits, hash_map *opt_map){ std::vector conjs; CollectConjuncts(fmla,conjs); @@ -817,6 +903,10 @@ namespace Duality { ConstrainEdgeLocalized(parent,GetAnnotation(child)); } + void RPFP_caching::ConstrainParentCache(Edge *parent, Node *child, std::vector &lits){ + ConstrainEdgeLocalizedCache(parent,GetAnnotation(child),lits); + } + /** For incremental solving, asserts the negation of the upper bound associated * with a node. @@ -828,7 +918,7 @@ namespace Duality { { n->dual = GetUpperBound(n); stack.back().nodes.push_back(n); - slvr.add(n->dual); + slvr_add(n->dual); } } @@ -892,9 +982,15 @@ namespace Duality { { e->constraints.push_back(tl); stack.back().constraints.push_back(std::pair(e,tl)); - slvr.add(tl); + slvr_add(tl); } + void RPFP_caching::ConstrainEdgeLocalizedCache(Edge *e, const Term &tl, std::vector &lits) + { + e->constraints.push_back(tl); + stack.back().constraints.push_back(std::pair(e,tl)); + GetAssumptionLits(tl,lits); + } /** Declare a constant in the background theory. */ @@ -971,7 +1067,7 @@ namespace Duality { // if (dualLabels != null) dualLabels.Dispose(); timer_start("interpolate_tree"); - lbool res = ls->interpolate_tree(tree, interpolant, dualModel,goals,true); + lbool res = ls_interpolate_tree(tree, interpolant, dualModel,goals,true); timer_stop("interpolate_tree"); if (res == l_false) { @@ -1017,7 +1113,7 @@ namespace Duality { ClearProofCore(); timer_start("interpolate_tree"); - lbool res = ls->interpolate_tree(tree, interpolant, dualModel,0,true); + lbool res = ls_interpolate_tree(tree, interpolant, dualModel,0,true); timer_stop("interpolate_tree"); if (res == l_false) { @@ -1068,22 +1164,22 @@ namespace Duality { // if (dualModel != null) dualModel.Dispose(); check_result res; if(!underapproxes.size()) - res = slvr.check(); + res = slvr_check(); else { std::vector us(underapproxes.size()); for(unsigned i = 0; i < underapproxes.size(); i++) us[i] = UnderapproxFlag(underapproxes[i]); - slvr.check(); // TODO: no idea why I need to do this + slvr_check(); // TODO: no idea why I need to do this if(underapprox_core){ std::vector unsat_core(us.size()); unsigned core_size = 0; - res = slvr.check(us.size(),&us[0],&core_size,&unsat_core[0]); + res = slvr_check(us.size(),&us[0],&core_size,&unsat_core[0]); underapprox_core->resize(core_size); for(unsigned i = 0; i < core_size; i++) (*underapprox_core)[i] = UnderapproxFlagRev(unsat_core[i]); } else { - res = slvr.check(us.size(),&us[0]); + res = slvr_check(us.size(),&us[0]); bool dump = false; if(dump){ std::vector cnsts; @@ -1093,7 +1189,7 @@ namespace Duality { ls->write_interpolation_problem("temp.smt",cnsts,std::vector()); } } - // check_result temp = slvr.check(); + // check_result temp = slvr_check(); } dualModel = slvr.get_model(); timer_stop("Check"); @@ -1101,10 +1197,12 @@ namespace Duality { } check_result RPFP::CheckUpdateModel(Node *root, std::vector assumps){ - // check_result temp1 = slvr.check(); // no idea why I need to do this + // 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(); + check_result res = slvr_check(assumps.size(),&assumps[0]); + model mod = slvr.get_model(); + if(!mod.null()) + dualModel = mod;; return res; } @@ -1117,8 +1215,6 @@ namespace Duality { return dualModel.eval(tl); } - - /** Returns true if the given node is empty in the primal solution. For proecudure summaries, this means that the procedure is not called in the current counter-model. */ @@ -2609,14 +2705,14 @@ namespace Duality { void RPFP::Push() { stack.push_back(stack_entry()); - slvr.push(); + slvr_push(); } /** Pop a scope (see Push). Note, you cannot pop axioms. */ void RPFP::Pop(int num_scopes) { - slvr.pop(num_scopes); + slvr_pop(num_scopes); for (int i = 0; i < num_scopes; i++) { stack_entry &back = stack.back(); @@ -2634,15 +2730,15 @@ namespace Duality { all the popped constraints */ void RPFP::PopPush(){ - slvr.pop(1); - slvr.push(); + 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); + slvr_add((*it)->dual); for(std::list::iterator it = back.nodes.begin(), en = back.nodes.end(); it != en; ++it) - slvr.add((*it)->dual); + slvr_add((*it)->dual); for(std::list >::iterator it = back.constraints.begin(), en = back.constraints.end(); it != en; ++it) - slvr.add((*it).second); + slvr_add((*it).second); } @@ -3121,12 +3217,25 @@ namespace Duality { } } + bool RPFP::proof_core_contains(const expr &e){ + return proof_core->find(e) != proof_core->end(); + } + + bool RPFP_caching::proof_core_contains(const expr &e){ + std::vector foo; + GetAssumptionLits(e,foo); + for(unsigned i = 0; i < foo.size(); i++) + if(proof_core->find(foo[i]) != proof_core->end()) + return true; + return false; + } + bool RPFP::EdgeUsedInProof(Edge *edge){ ComputeProofCore(); - if(!edge->dual.null() && proof_core->find(edge->dual) != proof_core->end()) + if(!edge->dual.null() && proof_core_contains(edge->dual)) return true; for(unsigned i = 0; i < edge->constraints.size(); i++) - if(proof_core->find(edge->constraints[i]) != proof_core->end()) + if(proof_core_contains(edge->constraints[i])) return true; return false; } diff --git a/src/duality/duality_solver.cpp b/src/duality/duality_solver.cpp index 7318b020d..1faf838b0 100644 --- a/src/duality/duality_solver.cpp +++ b/src/duality/duality_solver.cpp @@ -37,7 +37,7 @@ Revision History: #define MINIMIZE_CANDIDATES // #define MINIMIZE_CANDIDATES_HARDER #define BOUNDED -#define CHECK_CANDS_FROM_IND_SET +// #define CHECK_CANDS_FROM_IND_SET #define UNDERAPPROX_NODES #define NEW_EXPAND #define EARLY_EXPAND @@ -45,6 +45,10 @@ Revision History: // #define EFFORT_BOUNDED_STRAT #define SKIP_UNDERAPPROX_NODES #define USE_RPFP_CLONE +#define KEEP_EXPANSIONS +#define USE_CACHING_RPFP +// #define PROPAGATE_BEFORE_CHECK +#define USE_NEW_GEN_CANDS namespace Duality { @@ -115,11 +119,19 @@ namespace Duality { Report = false; StratifiedInlining = false; RecursionBound = -1; + { + scoped_no_proof no_proofs_please(ctx.m()); #ifdef USE_RPFP_CLONE clone_ls = new RPFP::iZ3LogicSolver(ctx); clone_rpfp = new RPFP_caching(clone_ls); clone_rpfp->Clone(rpfp); #endif +#ifdef USE_NEW_GEN_CANDS + gen_cands_ls = new RPFP::iZ3LogicSolver(ctx); + gen_cands_rpfp = new RPFP_caching(gen_cands_ls); + gen_cands_rpfp->Clone(rpfp); +#endif + } } ~Duality(){ @@ -127,12 +139,21 @@ namespace Duality { delete clone_rpfp; delete clone_ls; #endif +#ifdef USE_NEW_GEN_CANDS + delete gen_cands_rpfp; + delete gen_cands_ls; +#endif } #ifdef USE_RPFP_CLONE RPFP::LogicSolver *clone_ls; RPFP_caching *clone_rpfp; #endif +#ifdef USE_NEW_GEN_CANDS + RPFP::LogicSolver *gen_cands_ls; + RPFP_caching *gen_cands_rpfp; +#endif + typedef RPFP::Node Node; typedef RPFP::Edge Edge; @@ -1102,7 +1123,8 @@ namespace Duality { void ExtractCandidateFromCex(Edge *edge, RPFP *checker, Node *root, Candidate &candidate){ candidate.edge = edge; for(unsigned j = 0; j < edge->Children.size(); j++){ - Edge *lb = root->Outgoing->Children[j]->Outgoing; + Node *node = root->Outgoing->Children[j]; + Edge *lb = node->Outgoing; std::vector &insts = insts_of_node[edge->Children[j]]; #ifndef MINIMIZE_CANDIDATES for(int k = insts.size()-1; k >= 0; k--) @@ -1112,8 +1134,8 @@ namespace Duality { { Node *inst = insts[k]; if(indset->Contains(inst)){ - if(checker->Empty(lb->Parent) || - eq(checker->Eval(lb,NodeMarker(inst)),ctx.bool_val(true))){ + if(checker->Empty(node) || + eq(lb ? checker->Eval(lb,NodeMarker(inst)) : checker->dualModel.eval(NodeMarker(inst)),ctx.bool_val(true))){ candidate.Children.push_back(inst); goto next_child; } @@ -1183,6 +1205,25 @@ namespace Duality { #endif + Node *CheckerForEdgeClone(Edge *edge, RPFP_caching *checker){ + Edge *gen_cands_edge = gen_cands_rpfp->GetEdgeClone(edge); + Node *root = gen_cands_edge->Parent; + root->Outgoing = gen_cands_edge; + GenNodeSolutionFromIndSet(edge->Parent, root->Bound); +#if 0 + if(root->Bound.IsFull()) + return = 0; +#endif + checker->AssertNode(root); + for(unsigned j = 0; j < edge->Children.size(); j++){ + Node *oc = edge->Children[j]; + Node *nc = gen_cands_edge->Children[j]; + GenNodeSolutionWithMarkers(oc,nc->Annotation,true); + } + checker->AssertEdge(gen_cands_edge,1,true); + return root; + } + /** If the current proposed solution is not inductive, use the induction failure to generate candidates for extension. */ void GenCandidatesFromInductionFailure(bool full_scan = false){ @@ -1192,6 +1233,7 @@ namespace Duality { Edge *edge = edges[i]; if(!full_scan && updated_nodes.find(edge->Parent) == updated_nodes.end()) continue; +#ifndef USE_RPFP_CLONE slvr.push(); RPFP *checker = new RPFP(rpfp->ls); Node *root = CheckerForEdge(edge,checker); @@ -1203,6 +1245,17 @@ namespace Duality { } slvr.pop(1); delete checker; +#else + clone_rpfp->Push(); + Node *root = CheckerForEdgeClone(edge,clone_rpfp); + if(clone_rpfp->Check(root) != unsat){ + Candidate candidate; + ExtractCandidateFromCex(edge,clone_rpfp,root,candidate); + reporter->InductionFailure(edge,candidate.Children); + candidates.push_back(candidate); + } + clone_rpfp->Pop(1); +#endif } updated_nodes.clear(); timer_stop("GenCandIndFail"); @@ -1326,7 +1379,9 @@ namespace Duality { node. */ bool SatisfyUpperBound(Node *node){ if(node->Bound.IsFull()) return true; +#ifdef PROPAGATE_BEFORE_CHECK Propagate(); +#endif reporter->Bound(node); int start_decs = rpfp->CumulativeDecisions(); DerivationTree *dtp = new DerivationTreeSlow(this,unwinding,reporter,heuristic,FullExpand); @@ -1544,7 +1599,13 @@ namespace Duality { constrained = _constrained; false_approx = true; timer_start("Derive"); +#ifndef USE_CACHING_RPFP tree = _tree ? _tree : new RPFP(rpfp->ls); +#else + RPFP::LogicSolver *cache_ls = new RPFP::iZ3LogicSolver(ctx); + cache_ls->slvr->push(); + tree = _tree ? _tree : new RPFP_caching(cache_ls); +#endif tree->HornClauses = rpfp->HornClauses; tree->Push(); // so we can clear out the solver later when finished top = CreateApproximatedInstance(root); @@ -1556,19 +1617,27 @@ namespace Duality { timer_start("Pop"); tree->Pop(1); timer_stop("Pop"); +#ifdef USE_CACHING_RPFP + cache_ls->slvr->pop(1); + delete cache_ls; +#endif timer_stop("Derive"); return res; } #define WITH_CHILDREN - Node *CreateApproximatedInstance(RPFP::Node *from){ - Node *to = tree->CloneNode(from); - to->Annotation = from->Annotation; + void InitializeApproximatedInstance(RPFP::Node *to){ + to->Annotation = to->map->Annotation; #ifndef WITH_CHILDREN tree->CreateLowerBoundEdge(to); #endif leaves.push_back(to); + } + + Node *CreateApproximatedInstance(RPFP::Node *from){ + Node *to = tree->CloneNode(from); + InitializeApproximatedInstance(to); return to; } @@ -1637,13 +1706,23 @@ namespace Duality { virtual void ExpandNode(RPFP::Node *p){ // tree->RemoveEdge(p->Outgoing); - Edge *edge = duality->GetNodeOutgoing(p->map,last_decs); - std::vector &cs = edge->Children; - std::vector children(cs.size()); - for(unsigned i = 0; i < cs.size(); i++) - children[i] = CreateApproximatedInstance(cs[i]); - Edge *ne = tree->CreateEdge(p, p->map->Outgoing->F, children); - ne->map = p->map->Outgoing->map; + Edge *ne = p->Outgoing; + if(ne) { + reporter->Message("Recycling edge..."); + std::vector &cs = ne->Children; + for(unsigned i = 0; i < cs.size(); i++) + InitializeApproximatedInstance(cs[i]); + // ne->dual = expr(); + } + else { + Edge *edge = duality->GetNodeOutgoing(p->map,last_decs); + std::vector &cs = edge->Children; + std::vector children(cs.size()); + for(unsigned i = 0; i < cs.size(); i++) + children[i] = CreateApproximatedInstance(cs[i]); + ne = tree->CreateEdge(p, p->map->Outgoing->F, children); + ne->map = p->map->Outgoing->map; + } #ifndef WITH_CHILDREN tree->AssertEdge(ne); // assert the edge in the solver #else @@ -1785,12 +1864,25 @@ namespace Duality { void RemoveExpansion(RPFP::Node *p){ Edge *edge = p->Outgoing; Node *parent = edge->Parent; +#ifndef KEEP_EXPANSIONS std::vector cs = edge->Children; tree->DeleteEdge(edge); for(unsigned i = 0; i < cs.size(); i++) tree->DeleteNode(cs[i]); +#endif leaves.push_back(parent); } + + // remove all the descendants of tree root (but not root itself) + void RemoveTree(RPFP *tree, RPFP::Node *root){ + Edge *edge = root->Outgoing; + std::vector cs = edge->Children; + tree->DeleteEdge(edge); + for(unsigned i = 0; i < cs.size(); i++){ + RemoveTree(tree,cs[i]); + tree->DeleteNode(cs[i]); + } + } }; class DerivationTreeSlow : public DerivationTree { @@ -1852,6 +1944,7 @@ namespace Duality { } } tree->ComputeProofCore(); // need to compute the proof core before popping solver + bool propagated = false; while(1) { std::vector &expansions = stack.back().expansions; bool prev_level_used = LevelUsedInProof(stack.size()-2); // need to compute this before pop @@ -1881,16 +1974,21 @@ namespace Duality { if(!Propagate(node)) break; if(!RecordUpdate(node)) break; // shouldn't happen! RemoveUpdateNodesAtCurrentLevel(); // this level is about to be deleted -- remove its children from update list + propagated = true; continue; } + if(propagated) break; // propagation invalidates the proof core, so disable non-chron backtrack 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) + if(stack.size() == 1){ + if(top->Outgoing) + tree->DeleteEdge(top->Outgoing); // in case we kept the tree return false; + } was_sat = false; } else { diff --git a/src/duality/duality_wrapper.cpp b/src/duality/duality_wrapper.cpp index 26bdf52d7..51f357653 100644 --- a/src/duality/duality_wrapper.cpp +++ b/src/duality/duality_wrapper.cpp @@ -44,6 +44,7 @@ namespace Duality { m_solver = (*sf)(m(), p, true, true, true, ::symbol::null); m_solver->updt_params(p); // why do we have to do this? canceled = false; + m_mode = m().proof_mode(); } expr context::constant(const std::string &name, const sort &ty){ diff --git a/src/duality/duality_wrapper.h b/src/duality/duality_wrapper.h index fa4eca77b..76b28a426 100755 --- a/src/duality/duality_wrapper.h +++ b/src/duality/duality_wrapper.h @@ -50,6 +50,7 @@ Revision History: #include"scoped_ctrl_c.h" #include"cancel_eh.h" #include"scoped_timer.h" +#include"scoped_proof.h" namespace Duality { @@ -718,6 +719,7 @@ namespace Duality { m_model = s; return *this; } + bool null() const {return !m_model;} expr eval(expr const & n, bool model_completion=true) const { ::model * _m = m_model.get(); @@ -811,6 +813,7 @@ namespace Duality { ::solver *m_solver; model the_model; bool canceled; + proof_gen_mode m_mode; public: solver(context & c, bool extensional = false); solver(context & c, ::solver *s):object(c),the_model(c) { m_solver = s; canceled = false;} @@ -824,6 +827,7 @@ namespace Duality { m_ctx = s.m_ctx; m_solver = s.m_solver; the_model = s.the_model; + m_mode = s.m_mode; return *this; } struct cancel_exception {}; @@ -832,11 +836,12 @@ namespace Duality { throw(cancel_exception()); } // void set(params const & p) { Z3_solver_set_params(ctx(), m_solver, p); check_error(); } - void push() { m_solver->push(); } - void pop(unsigned n = 1) { m_solver->pop(n); } + void push() { scoped_proof_mode spm(m(),m_mode); m_solver->push(); } + void pop(unsigned n = 1) { scoped_proof_mode spm(m(),m_mode); m_solver->pop(n); } // void reset() { Z3_solver_reset(ctx(), m_solver); check_error(); } - void add(expr const & e) { m_solver->assert_expr(e); } + void add(expr const & e) { scoped_proof_mode spm(m(),m_mode); m_solver->assert_expr(e); } check_result check() { + scoped_proof_mode spm(m(),m_mode); checkpoint(); lbool r = m_solver->check_sat(0,0); model_ref m; @@ -845,6 +850,7 @@ namespace Duality { return to_check_result(r); } check_result check_keep_model(unsigned n, expr * const assumptions, unsigned *core_size = 0, expr *core = 0) { + scoped_proof_mode spm(m(),m_mode); model old_model(the_model); check_result res = check(n,assumptions,core_size,core); if(the_model == 0) @@ -852,6 +858,7 @@ namespace Duality { return res; } check_result check(unsigned n, expr * const assumptions, unsigned *core_size = 0, expr *core = 0) { + scoped_proof_mode spm(m(),m_mode); checkpoint(); std::vector< ::expr *> _assumptions(n); for (unsigned i = 0; i < n; i++) { @@ -876,6 +883,7 @@ namespace Duality { } #if 0 check_result check(expr_vector assumptions) { + scoped_proof_mode spm(m(),m_mode); unsigned n = assumptions.size(); z3array _assumptions(n); for (unsigned i = 0; i < n; i++) { @@ -900,17 +908,19 @@ namespace Duality { int get_num_decisions(); void cancel(){ + scoped_proof_mode spm(m(),m_mode); canceled = true; if(m_solver) m_solver->cancel(); } - unsigned get_scope_level(){return m_solver->get_scope_level();} + unsigned get_scope_level(){ scoped_proof_mode spm(m(),m_mode); return m_solver->get_scope_level();} void show(); void show_assertion_ids(); proof get_proof(){ + scoped_proof_mode spm(m(),m_mode); return proof(ctx(),m_solver->get_proof()); } diff --git a/src/muz/duality/duality_dl_interface.cpp b/src/muz/duality/duality_dl_interface.cpp index 1409212d4..397d50655 100644 --- a/src/muz/duality/duality_dl_interface.cpp +++ b/src/muz/duality/duality_dl_interface.cpp @@ -35,7 +35,6 @@ Revision History: #include "model_smt2_pp.h" #include "model_v2_pp.h" #include "fixedpoint_params.hpp" -#include "scoped_proof.h" // template class symbol_table; From 673ba137e55716c4e137ec38ea2bc03219da9b3c Mon Sep 17 00:00:00 2001 From: Ken McMillan Date: Mon, 23 Dec 2013 11:17:38 -0800 Subject: [PATCH 04/12] added qe_lite preprocessing pass to duality --- src/duality/duality_rpfp.cpp | 45 ++++++++++++++++++++++++++++++++- src/duality/duality_wrapper.cpp | 11 ++++++++ src/duality/duality_wrapper.h | 3 +++ 3 files changed, 58 insertions(+), 1 deletion(-) diff --git a/src/duality/duality_rpfp.cpp b/src/duality/duality_rpfp.cpp index 04b4d075e..036a0c86a 100644 --- a/src/duality/duality_rpfp.cpp +++ b/src/duality/duality_rpfp.cpp @@ -2802,7 +2802,7 @@ namespace Duality { bool Z3User::is_variable(const Term &t){ if(!t.is_app()) - return false; + return t.is_var(); return t.decl().get_decl_kind() == Uninterpreted && t.num_args() == 0; } @@ -2951,6 +2951,8 @@ namespace Duality { arg.decl().get_decl_kind() == Uninterpreted); } +#define USE_QE_LITE + void RPFP::FromClauses(const std::vector &unskolemized_clauses){ hash_map pmap; func_decl fail_pred = ctx.fresh_func_decl("@Fail", ctx.bool_sort()); @@ -2958,6 +2960,7 @@ namespace Duality { std::vector clauses(unskolemized_clauses); // first, skolemize the clauses +#ifndef USE_QE_LITE for(unsigned i = 0; i < clauses.size(); i++){ expr &t = clauses[i]; if (t.is_quantifier() && t.is_quantifier_forall()) { @@ -2974,11 +2977,32 @@ namespace Duality { t = SubstBound(subst,t.body()); } } +#else + std::vector > substs(clauses.size()); +#endif // create the nodes from the heads of the clauses for(unsigned i = 0; i < clauses.size(); i++){ Term &clause = clauses[i]; + +#ifdef USE_QE_LITE + Term &t = clause; + if (t.is_quantifier() && t.is_quantifier_forall()) { + int bound = t.get_quantifier_num_bound(); + std::vector sorts; + std::vector names; + for(int j = 0; j < bound; j++){ + sort the_sort = t.get_quantifier_bound_sort(j); + symbol name = t.get_quantifier_bound_name(j); + expr skolem = ctx.constant(symbol(ctx,name),sort(ctx,the_sort)); + substs[i][bound-1-j] = skolem; + } + clause = t.body(); + } + +#endif + if(clause.is_app() && clause.decl().get_decl_kind() == Uninterpreted) clause = implies(ctx.bool_val(true),clause); if(!canonical_clause(clause)) @@ -3010,6 +3034,13 @@ namespace Duality { seen.insert(arg); Indparams.push_back(arg); } +#ifdef USE_QE_LITE + { + hash_map > sb_memo; + for(unsigned j = 0; j < Indparams.size(); j++) + Indparams[j] = SubstBoundRec(sb_memo, substs[i], 0, Indparams[j]); + } +#endif Node *node = CreateNode(R(Indparams.size(),&Indparams[0])); //nodes.push_back(node); pmap[R] = node; @@ -3055,6 +3086,18 @@ namespace Duality { body = RemoveLabels(body,lbls); body = body.simplify(); +#ifdef USE_QE_LITE + std::set idxs; + for(unsigned j = 0; j < Indparams.size(); j++) + if(Indparams[j].is_var()) + idxs.insert(Indparams[j].get_index_value()); + body = body.qe_lite(idxs,false); + hash_map > sb_memo; + body = SubstBoundRec(sb_memo,substs[i],0,body); + for(unsigned j = 0; j < Indparams.size(); j++) + Indparams[j] = SubstBoundRec(sb_memo, substs[i], 0, Indparams[j]); +#endif + // Create the edge Transformer T = CreateTransformer(Relparams,Indparams,body); Edge *edge = CreateEdge(Parent,T,Children); diff --git a/src/duality/duality_wrapper.cpp b/src/duality/duality_wrapper.cpp index 51f357653..dd1828214 100644 --- a/src/duality/duality_wrapper.cpp +++ b/src/duality/duality_wrapper.cpp @@ -339,6 +339,17 @@ expr context::make_quant(decl_kind op, const std::vector &_sorts, const st return ctx().cook(result); } + expr expr::qe_lite(const std::set &idxs, bool index_of_bound) const { + ::qe_lite qe(m()); + expr_ref result(to_expr(raw()),m()); + proof_ref pf(m()); + uint_set uis; + for(std::set::const_iterator it=idxs.begin(), en = idxs.end(); it != en; ++it) + uis.insert(*it); + qe(uis,index_of_bound,result); + 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 76b28a426..0b20cb08d 100755 --- a/src/duality/duality_wrapper.h +++ b/src/duality/duality_wrapper.h @@ -26,6 +26,7 @@ Revision History: #include #include #include +#include #include"version.h" #include @@ -561,6 +562,8 @@ namespace Duality { expr qe_lite() const; + expr qe_lite(const std::set &idxs, bool index_of_bound) const; + friend expr clone_quantifier(const expr &, const expr &); friend expr clone_quantifier(const expr &q, const expr &b, const std::vector &patterns); From 1b9f1ea6b32713078e9eff0ea60836be4a295364 Mon Sep 17 00:00:00 2001 From: Ken McMillan Date: Mon, 23 Dec 2013 11:47:24 -0800 Subject: [PATCH 05/12] remove assert on failed label compuation in duality --- src/duality/duality_rpfp.cpp | 2 +- src/duality/duality_solver.cpp | 1 + 2 files changed, 2 insertions(+), 1 deletion(-) diff --git a/src/duality/duality_rpfp.cpp b/src/duality/duality_rpfp.cpp index 036a0c86a..ec3e9164f 100644 --- a/src/duality/duality_rpfp.cpp +++ b/src/duality/duality_rpfp.cpp @@ -1492,7 +1492,7 @@ namespace Duality { } } /* Unreachable! */ - throw "error in RPFP::GetLabelsRec"; + // throw "error in RPFP::GetLabelsRec"; goto done; } else if(k == Not) { diff --git a/src/duality/duality_solver.cpp b/src/duality/duality_solver.cpp index 1faf838b0..f264d5569 100644 --- a/src/duality/duality_solver.cpp +++ b/src/duality/duality_solver.cpp @@ -1620,6 +1620,7 @@ namespace Duality { #ifdef USE_CACHING_RPFP cache_ls->slvr->pop(1); delete cache_ls; + tree->ls = rpfp->ls; #endif timer_stop("Derive"); return res; From 11ba2178a9c99bec2518dc1349a55e4f1306463e Mon Sep 17 00:00:00 2001 From: Ken McMillan Date: Tue, 24 Dec 2013 17:20:12 -0800 Subject: [PATCH 06/12] speeding up interpolation in RPFP_caching --- src/duality/duality.h | 1 + src/duality/duality_rpfp.cpp | 74 +++++++++++++++++++++++++--------- src/duality/duality_solver.cpp | 5 +++ src/duality/duality_wrapper.h | 1 + 4 files changed, 63 insertions(+), 18 deletions(-) diff --git a/src/duality/duality.h b/src/duality/duality.h index b88e5011f..b587c519d 100644 --- a/src/duality/duality.h +++ b/src/duality/duality.h @@ -1139,6 +1139,7 @@ namespace Duality { void GetTermTreeAssertionLiterals(TermTree *assumptions); + void GetTermTreeAssertionLiteralsRec(TermTree *assumptions); }; } diff --git a/src/duality/duality_rpfp.cpp b/src/duality/duality_rpfp.cpp index ec3e9164f..46902e9a5 100644 --- a/src/duality/duality_rpfp.cpp +++ b/src/duality/duality_rpfp.cpp @@ -863,7 +863,7 @@ namespace Duality { return ls->interpolate_tree(assumptions, interpolants, _model, goals, weak); } - void RPFP_caching::GetTermTreeAssertionLiterals(TermTree *assumptions){ + void RPFP_caching::GetTermTreeAssertionLiteralsRec(TermTree *assumptions){ std::vector alits; hash_map map; GetAssumptionLits(assumptions->getTerm(),alits,&map); @@ -879,6 +879,51 @@ namespace Duality { return; } + void RPFP_caching::GetTermTreeAssertionLiterals(TermTree *assumptions){ + // optimize binary case + if(assumptions->getChildren().size() == 1 + && assumptions->getChildren()[0]->getChildren().size() == 0){ + hash_map map; + TermTree *child = assumptions->getChildren()[0]; + std::vector dummy; + GetAssumptionLits(child->getTerm(),dummy,&map); + std::vector &ts = child->getTerms(); + for(unsigned i = 0; i < ts.size(); i++) + GetAssumptionLits(ts[i],dummy,&map); + std::vector assumps; + slvr.get_proof().get_assumptions(assumps); + if(!proof_core){ // save the proof core for later use + proof_core = new hash_set; + for(unsigned i = 0; i < assumps.size(); i++) + proof_core->insert(assumps[i]); + } + std::vector *cnsts[2] = {&child->getTerms(),&assumptions->getTerms()}; + for(unsigned i = 0; i < assumps.size(); i++){ + expr &ass = assumps[i]; + expr alit = (ass.is_app() && ass.decl().get_decl_kind() == Implies) ? ass.arg(0) : ass; + bool isA = map.find(alit) != map.end(); + cnsts[isA ? 0 : 1]->push_back(ass); + } + } + else + GetTermTreeAssertionLiteralsRec(assumptions); + } + + 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){ + proof_core = new hash_set; + AddToProofCore(*proof_core); + } + } + + void RPFP_caching::GetAssumptionLits(const expr &fmla, std::vector &lits, hash_map *opt_map){ std::vector conjs; CollectConjuncts(fmla,conjs); @@ -2616,13 +2661,19 @@ namespace Duality { for(unsigned i = 0; i < edge->Children.size(); i++){ expr ass = GetAnnotation(edge->Children[i]); std::vector clauses; - CollectConjuncts(ass.arg(1),clauses); - for(unsigned j = 0; j < clauses.size(); j++) - GetAssumptionLits(ass.arg(0) || clauses[j],assumps); + if(!ass.is_true()){ + CollectConjuncts(ass.arg(1),clauses); + for(unsigned j = 0; j < clauses.size(); j++) + GetAssumptionLits(ass.arg(0) || clauses[j],assumps); + } } expr fmla = GetAnnotation(node); - assumps.push_back(fmla.arg(0).arg(0)); std::vector lits; + if(fmla.is_true()){ + timer_stop("Generalize"); + return; + } + assumps.push_back(fmla.arg(0).arg(0)); CollectConjuncts(!fmla.arg(1),lits); #if 0 for(unsigned i = 0; i < lits.size(); i++){ @@ -3246,19 +3297,6 @@ 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){ - proof_core = new hash_set; - AddToProofCore(*proof_core); - } - } bool RPFP::proof_core_contains(const expr &e){ return proof_core->find(e) != proof_core->end(); diff --git a/src/duality/duality_solver.cpp b/src/duality/duality_solver.cpp index f264d5569..33318b207 100644 --- a/src/duality/duality_solver.cpp +++ b/src/duality/duality_solver.cpp @@ -1937,6 +1937,8 @@ namespace Duality { Generalize(node); if(RecordUpdate(node)) update_count++; + else + heuristic->Update(node->map); // make it less likely to expand this node in future } if(update_count == 0){ if(was_sat) @@ -2018,6 +2020,9 @@ namespace Duality { } bool NodeTooComplicated(Node *node){ + int ops = tree->CountOperators(node->Annotation.Formula); + if(ops > 10) return true; + node->Annotation.Formula = tree->RemoveRedundancy(node->Annotation.Formula).simplify(); return tree->CountOperators(node->Annotation.Formula) > 3; } diff --git a/src/duality/duality_wrapper.h b/src/duality/duality_wrapper.h index 0b20cb08d..0de3a7d49 100755 --- a/src/duality/duality_wrapper.h +++ b/src/duality/duality_wrapper.h @@ -451,6 +451,7 @@ namespace Duality { bool is_datatype() const { return get_sort().is_datatype(); } bool is_relation() const { return get_sort().is_relation(); } bool is_finite_domain() const { return get_sort().is_finite_domain(); } + bool is_true() const {return is_app() && decl().get_decl_kind() == True; } bool is_numeral() const { return is_app() && decl().get_decl_kind() == OtherArith && m().is_unique_value(to_expr(raw())); From f380e31a6b6f15322ac6ff4f112e6f2db3822a0f Mon Sep 17 00:00:00 2001 From: Ken McMillan Date: Thu, 9 Jan 2014 17:16:10 -0800 Subject: [PATCH 07/12] runs the integer/cntrol svcomp examples from the Horn repo --- src/duality/duality.h | 130 ++++++- src/duality/duality_rpfp.cpp | 609 +++++++++++++++++++++++++++++++- src/duality/duality_solver.cpp | 74 +++- src/duality/duality_wrapper.cpp | 17 +- src/duality/duality_wrapper.h | 21 +- src/interp/iz3mgr.cpp | 19 +- src/interp/iz3mgr.h | 4 +- src/interp/iz3translate.cpp | 4 +- 8 files changed, 814 insertions(+), 64 deletions(-) diff --git a/src/duality/duality.h b/src/duality/duality.h index b587c519d..8c469b9e4 100644 --- a/src/duality/duality.h +++ b/src/duality/duality.h @@ -36,12 +36,11 @@ namespace Duality { struct Z3User { context &ctx; - solver &slvr; typedef func_decl FuncDecl; typedef expr Term; - Z3User(context &_ctx, solver &_slvr) : ctx(_ctx), slvr(_slvr){} + Z3User(context &_ctx) : ctx(_ctx){} const char *string_of_int(int n); @@ -53,6 +52,8 @@ namespace Duality { Term SubstRec(hash_map &memo, const Term &t); + Term SubstRec(hash_map &memo, hash_map &map, const Term &t); + void Strengthen(Term &x, const Term &y); // return the func_del of an app if it is uninterpreted @@ -77,14 +78,14 @@ namespace Duality { void Summarize(const Term &t); - int CumulativeDecisions(); - int CountOperators(const Term &t); Term SubstAtom(hash_map &memo, const expr &t, const expr &atom, const expr &val); Term RemoveRedundancy(const Term &t); + Term IneqToEq(const Term &t); + bool IsLiteral(const expr &lit, expr &atom, expr &val); expr Negate(const expr &f); @@ -98,6 +99,9 @@ namespace Duality { bool IsClosedFormula(const Term &t); Term AdjustQuantifiers(const Term &t); + + FuncDecl RenumberPred(const FuncDecl &f, int n); + protected: void SummarizeRec(hash_set &memo, std::vector &lits, int &ops, const Term &t); @@ -108,6 +112,7 @@ protected: 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); + Term IneqToEqRec(hash_map &memo, const Term &t); }; @@ -256,9 +261,9 @@ protected: } #endif - iZ3LogicSolver(context &c) : LogicSolver(c) { + iZ3LogicSolver(context &c, bool models = true) : LogicSolver(c) { ctx = ictx = &c; - slvr = islvr = new interpolating_solver(*ictx); + slvr = islvr = new interpolating_solver(*ictx, models); need_goals = false; islvr->SetWeakInterpolants(true); } @@ -308,7 +313,7 @@ protected: } LogicSolver *ls; - + protected: int nodeCount; int edgeCount; @@ -340,7 +345,7 @@ protected: inherit the axioms. */ - RPFP(LogicSolver *_ls) : Z3User(*(_ls->ctx), *(_ls->slvr)), dualModel(*(_ls->ctx)), aux_solver(_ls->aux_solver) + RPFP(LogicSolver *_ls) : Z3User(*(_ls->ctx)), dualModel(*(_ls->ctx)), aux_solver(_ls->aux_solver) { ls = _ls; nodeCount = 0; @@ -574,7 +579,7 @@ protected: * you must pop the context accordingly. The second argument is * the number of pushes we are inside. */ - void AssertEdge(Edge *e, int persist = 0, bool with_children = false, bool underapprox = false); + virtual 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. */ @@ -808,9 +813,31 @@ protected: /** Edges of the graph. */ std::vector edges; + /** Fuse a vector of transformers. If the total number of inputs of the transformers + is N, then the result is an N-ary transfomer whose output is the union of + the outputs of the given transformers. The is, suppose we have a vetor of transfoermers + {T_i(r_i1,...,r_iN(i) : i=1..M}. The the result is a transformer + + F(r_11,...,r_iN(1),...,r_M1,...,r_MN(M)) = + T_1(r_11,...,r_iN(1)) U ... U T_M(r_M1,...,r_MN(M)) + */ + + Transformer Fuse(const std::vector &trs); + + /** Fuse edges so that each node is the output of at most one edge. This + transformation is solution-preserving, but changes the numbering of edges in + counterexamples. + */ + void FuseEdges(); + + void RemoveDeadNodes(); + Term SubstParams(const std::vector &from, const std::vector &to, const Term &t); + Term SubstParamsNoCapture(const std::vector &from, + const std::vector &to, const Term &t); + Term Localize(Edge *e, const Term &t); void EvalNodeAsConstraint(Node *p, Transformer &res); @@ -829,6 +856,12 @@ protected: */ void ComputeProofCore(); + int CumulativeDecisions(); + + solver &slvr(){ + return *ls->slvr; + } + protected: void ClearProofCore(){ @@ -962,7 +995,37 @@ protected: expr NegateLit(const expr &f); expr GetEdgeFormula(Edge *e, int persist, bool with_children, bool underapprox); + + bool IsVar(const expr &t); + + void GetVarsRec(hash_set &memo, const expr &cnst, std::vector &vars); + + expr UnhoistPullRec(hash_map & memo, const expr &w, hash_map & init_defs, hash_map & const_params, hash_map &const_params_inv, std::vector &new_params); + + void AddParamsToTransformer(Transformer &trans, const std::vector ¶ms); + + expr AddParamsToApp(const expr &app, const func_decl &new_decl, const std::vector ¶ms); + + expr GetRelRec(hash_set &memo, const expr &t, const func_decl &rel); + + expr GetRel(Edge *edge, int child_idx); + + void GetDefs(const expr &cnst, hash_map &defs); + + void GetDefsRec(const expr &cnst, hash_map &defs); + + void AddParamsToNode(Node *node, const std::vector ¶ms); + + void UnhoistLoop(Edge *loop_edge, Edge *init_edge); + + void Unhoist(); + Term ElimIteRec(hash_map &memo, const Term &t, std::vector &cnsts); + + Term ElimIte(const Term &t); + + void MarkLiveNodes(hash_map > &outgoing, hash_set &live_nodes, Node *node); + virtual void slvr_add(const expr &e); virtual void slvr_pop(int i); @@ -978,6 +1041,7 @@ protected: bool weak = false); virtual bool proof_core_contains(const expr &e); + }; @@ -1065,6 +1129,9 @@ namespace std { }; } +// #define LIMIT_STACK_WEIGHT 5 + + namespace Duality { /** Caching version of RPFP. Instead of asserting constraints, returns assumption literals */ @@ -1105,6 +1172,10 @@ namespace Duality { assumption lits. */ void ConstrainParentCache(Edge *parent, Node *child, std::vector &lits); +#ifdef LIMIT_STACK_WEIGHT + virtual void AssertEdge(Edge *e, int persist = 0, bool with_children = false, bool underapprox = false); +#endif + virtual ~RPFP_caching(){} protected: @@ -1113,7 +1184,31 @@ namespace Duality { hash_map EdgeCloneMap; std::vector alit_stack; std::vector alit_stack_sizes; + hash_map > edge_solvers; +#ifdef LIMIT_STACK_WEIGHT + struct weight_counter { + int val; + weight_counter(){val = 0;} + void swap(weight_counter &other){ + std::swap(val,other.val); + } + }; + + struct big_stack_entry { + weight_counter weight_added; + std::vector new_alits; + std::vector alit_stack; + std::vector alit_stack_sizes; + }; + + std::vector new_alits; + weight_counter weight_added; + std::vector big_stack; +#endif + + + void GetAssumptionLits(const expr &fmla, std::vector &lits, hash_map *opt_map = 0); void GreedyReduceCache(std::vector &assumps, std::vector &core); @@ -1140,6 +1235,23 @@ namespace Duality { void GetTermTreeAssertionLiterals(TermTree *assumptions); void GetTermTreeAssertionLiteralsRec(TermTree *assumptions); + + LogicSolver *SolverForEdge(Edge *edge, bool models); + + public: + struct scoped_solver_for_edge { + LogicSolver *orig_ls; + RPFP_caching *rpfp; + scoped_solver_for_edge(RPFP_caching *_rpfp, Edge *edge, bool models = false){ + rpfp = _rpfp; + orig_ls = rpfp->ls; + rpfp->ls = rpfp->SolverForEdge(edge,models); + } + ~scoped_solver_for_edge(){ + rpfp->ls = orig_ls; + } + }; + }; } diff --git a/src/duality/duality_rpfp.cpp b/src/duality/duality_rpfp.cpp index 46902e9a5..ad89c1314 100644 --- a/src/duality/duality_rpfp.cpp +++ b/src/duality/duality_rpfp.cpp @@ -104,7 +104,7 @@ namespace Duality { lits.push_back(t); } - int Z3User::CumulativeDecisions(){ + int RPFP::CumulativeDecisions(){ #if 0 std::string stats = Z3_statistics_to_string(ctx); int pos = stats.find("decisions:"); @@ -113,7 +113,7 @@ namespace Duality { std::string val = stats.substr(pos,end-pos); return atoi(val.c_str()); #endif - return slvr.get_num_decisions(); + return slvr().get_num_decisions(); } @@ -370,6 +370,38 @@ namespace Duality { return res; } + Z3User::Term Z3User::SubstRec(hash_map &memo, hash_map &map, 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(SubstRec(memo, map, t.arg(i))); + hash_map::iterator it = map.find(f); + if(it != map.end()) + f = it->second; + res = f(args.size(),&args[0]); + } + else if (t.is_quantifier()) + { + std::vector pats; + t.get_patterns(pats); + for(unsigned i = 0; i < pats.size(); i++) + pats[i] = SubstRec(memo, map, pats[i]); + Term body = SubstRec(memo, map, t.body()); + res = clone_quantifier(t, body, pats); + } + // res = CloneQuantifier(t,SubstRec(memo, t.body())); + else res = t; + return res; + } + bool Z3User::IsLiteral(const expr &lit, expr &atom, expr &val){ if(!(lit.is_quantifier() && IsClosedFormula(lit))){ if(!lit.is_app()) @@ -594,6 +626,50 @@ namespace Duality { return t; } + Z3User::Term Z3User::IneqToEqRec(hash_map &memo, 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(IneqToEqRec(memo, t.arg(i))); + + decl_kind k = f.get_decl_kind(); + if(k == And){ + for(int i = 0; i < nargs-1; i++){ + if((args[i].is_app() && args[i].decl().get_decl_kind() == Geq && + args[i+1].is_app() && args[i+1].decl().get_decl_kind() == Leq) + || + (args[i].is_app() && args[i].decl().get_decl_kind() == Leq && + args[i+1].is_app() && args[i+1].decl().get_decl_kind() == Geq)) + if(eq(args[i].arg(0),args[i+1].arg(0)) && eq(args[i].arg(1),args[i+1].arg(1))){ + args[i] = ctx.make(Equal,args[i].arg(0),args[i].arg(1)); + args[i+1] = ctx.bool_val(true); + } + } + } + res = f(args.size(),&args[0]); + } + else if (t.is_quantifier()) + { + Term body = IneqToEqRec(memo,t.body()); + res = clone_quantifier(t, body); + } + else res = t; + return res; + } + + Z3User::Term Z3User::IneqToEq(const Term &t){ + hash_map memo; + return IneqToEqRec(memo,t); + } + Z3User::Term Z3User::SubstRecHide(hash_map &memo, const Term &t, int number) { std::pair foo(t,expr(ctx)); @@ -632,6 +708,51 @@ namespace Duality { return some_diff ? SubstRec(memo,t) : t; } + RPFP::Term RPFP::SubstParamsNoCapture(const std::vector &from, + const std::vector &to, const Term &t){ + hash_map memo; + bool some_diff = false; + for(unsigned i = 0; i < from.size(); i++) + if(i < to.size() && !eq(from[i],to[i])){ + memo[from[i]] = to[i]; + // if the new param is not being mapped to anything else, we need to rename it to prevent capture + // note, if the new param *is* mapped later in the list, it will override this substitution + const expr &w = to[i]; + if(memo.find(w) == memo.end()){ + std::string old_name = w.decl().name().str(); + func_decl fresh = ctx.fresh_func_decl(old_name.c_str(), w.get_sort()); + expr y = fresh(); + memo[w] = y; + } + some_diff = true; + } + return some_diff ? SubstRec(memo,t) : t; + } + + + + RPFP::Transformer RPFP::Fuse(const std::vector &trs){ + assert(!trs.empty()); + const std::vector ¶ms = trs[0]->IndParams; + std::vector fmlas(trs.size()); + fmlas[0] = trs[0]->Formula; + for(unsigned i = 1; i < trs.size(); i++) + fmlas[i] = SubstParamsNoCapture(trs[i]->IndParams,params,trs[i]->Formula); + std::vector rel_params = trs[0]->RelParams; + for(unsigned i = 1; i < trs.size(); i++){ + const std::vector ¶ms2 = trs[i]->RelParams; + hash_map map; + for(unsigned j = 0; j < params2.size(); j++){ + func_decl rel = RenumberPred(params2[j],rel_params.size()); + rel_params.push_back(rel); + map[params2[j]] = rel; + } + hash_map memo; + fmlas[i] = SubstRec(memo,map,fmlas[i]); + } + return Transformer(rel_params,params,ctx.make(Or,fmlas),trs[0]->owner); + } + void Z3User::Strengthen(Term &x, const Term &y) { @@ -782,6 +903,25 @@ namespace Duality { ConstrainParent(e,e->Children[i]); } + +#ifdef LIMIT_STACK_WEIGHT + void RPFP_caching::AssertEdge(Edge *e, int persist, bool with_children, bool underapprox) + { + unsigned old_new_alits = new_alits.size(); + if(eq(e->F.Formula,ctx.bool_val(true)) && (!with_children || e->Children.empty())) + return; + expr fmla = GetEdgeFormula(e, persist, with_children, underapprox); + timer_start("solver add"); + slvr_add(e->dual); + timer_stop("solver add"); + if(old_new_alits < new_alits.size()) + weight_added.val++; + if(with_children) + for(unsigned i = 0; i < e->Children.size(); i++) + ConstrainParent(e,e->Children[i]); + } +#endif + // caching verion of above void RPFP_caching::AssertEdgeCache(Edge *e, std::vector &lits, bool with_children){ if(eq(e->F.Formula,ctx.bool_val(true)) && (!with_children || e->Children.empty())) @@ -794,7 +934,7 @@ namespace Duality { } void RPFP::slvr_add(const expr &e){ - slvr.add(e); + slvr().add(e); } void RPFP_caching::slvr_add(const expr &e){ @@ -802,37 +942,70 @@ namespace Duality { } void RPFP::slvr_pop(int i){ - slvr.pop(i); + slvr().pop(i); } void RPFP::slvr_push(){ - slvr.push(); + slvr().push(); } void RPFP_caching::slvr_pop(int i){ for(int j = 0; j < i; j++){ +#ifdef LIMIT_STACK_WEIGHT + if(alit_stack_sizes.empty()){ + if(big_stack.empty()) + throw "stack underflow"; + for(unsigned k = 0; k < new_alits.size(); k++){ + if(AssumptionLits.find(new_alits[k]) == AssumptionLits.end()) + throw "foo!"; + AssumptionLits.erase(new_alits[k]); + } + big_stack_entry &bsb = big_stack.back(); + bsb.alit_stack_sizes.swap(alit_stack_sizes); + bsb.alit_stack.swap(alit_stack); + bsb.new_alits.swap(new_alits); + bsb.weight_added.swap(weight_added); + big_stack.pop_back(); + slvr().pop(1); + continue; + } +#endif alit_stack.resize(alit_stack_sizes.back()); alit_stack_sizes.pop_back(); } } void RPFP_caching::slvr_push(){ +#ifdef LIMIT_STACK_WEIGHT + if(weight_added.val > LIMIT_STACK_WEIGHT){ + big_stack.resize(big_stack.size()+1); + big_stack_entry &bsb = big_stack.back(); + bsb.alit_stack_sizes.swap(alit_stack_sizes); + bsb.alit_stack.swap(alit_stack); + bsb.new_alits.swap(new_alits); + bsb.weight_added.swap(weight_added); + slvr().push(); + for(unsigned i = 0; i < bsb.alit_stack.size(); i++) + slvr().add(bsb.alit_stack[i]); + return; + } +#endif alit_stack_sizes.push_back(alit_stack.size()); } check_result RPFP::slvr_check(unsigned n, expr * const assumptions, unsigned *core_size, expr *core){ - return slvr.check(n, assumptions, core_size, core); + return slvr().check(n, assumptions, core_size, core); } check_result RPFP_caching::slvr_check(unsigned n, expr * const assumptions, unsigned *core_size, expr *core){ - slvr_push(); + unsigned oldsiz = alit_stack.size(); if(n && assumptions) std::copy(assumptions,assumptions+n,std::inserter(alit_stack,alit_stack.end())); check_result res; if(core_size && core){ std::vector full_core(alit_stack.size()), core1(n); std::copy(assumptions,assumptions+n,core1.begin()); - res = slvr.check(alit_stack.size(), &alit_stack[0], core_size, &full_core[0]); + res = slvr().check(alit_stack.size(), &alit_stack[0], core_size, &full_core[0]); full_core.resize(*core_size); if(res == unsat){ FilterCore(core1,full_core); @@ -841,8 +1014,8 @@ namespace Duality { } } else - res = slvr.check(alit_stack.size(), &alit_stack[0]); - slvr_pop(1); + res = slvr().check(alit_stack.size(), &alit_stack[0]); + alit_stack.resize(oldsiz); return res; } @@ -891,7 +1064,7 @@ namespace Duality { for(unsigned i = 0; i < ts.size(); i++) GetAssumptionLits(ts[i],dummy,&map); std::vector assumps; - slvr.get_proof().get_assumptions(assumps); + slvr().get_proof().get_assumptions(assumps); if(!proof_core){ // save the proof core for later use proof_core = new hash_set; for(unsigned i = 0; i < assumps.size(); i++) @@ -911,7 +1084,7 @@ namespace Duality { void RPFP::AddToProofCore(hash_set &core){ std::vector assumps; - slvr.get_proof().get_assumptions(assumps); + slvr().get_proof().get_assumptions(assumps); for(unsigned i = 0; i < assumps.size(); i++) core.insert(assumps[i]); } @@ -935,7 +1108,10 @@ namespace Duality { if(bar.second){ func_decl pred = ctx.fresh_func_decl("@alit", ctx.bool_sort()); res = pred(); - slvr.add(ctx.make(Implies,res,conj)); +#ifdef LIMIT_STACK_WEIGHT + new_alits.push_back(conj); +#endif + slvr().add(ctx.make(Implies,res,conj)); // std::cout << res << ": " << conj << "\n"; } if(opt_map) @@ -979,15 +1155,18 @@ namespace Duality { /** Clone another RPFP into this one, keeping a map */ void RPFP_caching::Clone(RPFP *other){ +#if 0 for(unsigned i = 0; i < other->nodes.size(); i++) NodeCloneMap[other->nodes[i]] = CloneNode(other->nodes[i]); +#endif for(unsigned i = 0; i < other->edges.size(); i++){ Edge *edge = other->edges[i]; + Node *parent = CloneNode(edge->Parent); std::vector cs; for(unsigned j = 0; j < edge->Children.size(); j++) // cs.push_back(NodeCloneMap[edge->Children[j]]); cs.push_back(CloneNode(edge->Children[j])); - EdgeCloneMap[edge] = CreateEdge(NodeCloneMap[edge->Parent],edge->F,cs); + EdgeCloneMap[edge] = CreateEdge(parent,edge->F,cs); } } @@ -1005,7 +1184,7 @@ namespace Duality { check_result RPFP_caching::CheckCore(const std::vector &assumps, std::vector &core){ core.resize(assumps.size()); unsigned core_size; - check_result res = slvr.check(assumps.size(),(expr *)&assumps[0],&core_size,&core[0]); + check_result res = slvr().check(assumps.size(),(expr *)&assumps[0],&core_size,&core[0]); if(res == unsat) core.resize(core_size); else @@ -1063,7 +1242,7 @@ namespace Duality { void RPFP::RemoveAxiom(const Term &t) { - slvr.RemoveInterpolationAxiom(t); + slvr().RemoveInterpolationAxiom(t); } #endif @@ -1236,7 +1415,7 @@ namespace Duality { } // check_result temp = slvr_check(); } - dualModel = slvr.get_model(); + dualModel = slvr().get_model(); timer_stop("Check"); return res; } @@ -1245,7 +1424,7 @@ namespace Duality { // check_result temp1 = slvr_check(); // no idea why I need to do this ClearProofCore(); check_result res = slvr_check(assumps.size(),&assumps[0]); - model mod = slvr.get_model(); + model mod = slvr().get_model(); if(!mod.null()) dualModel = mod;; return res; @@ -1706,6 +1885,57 @@ namespace Duality { return res; } + RPFP::Term RPFP::ElimIteRec(hash_map &memo, const Term &t, std::vector &cnsts){ + std::pair foo(t,expr(ctx)); + std::pair::iterator, bool> bar = memo.insert(foo); + Term &res = bar.first->second; + if(bar.second){ + if(t.is_app()){ + int nargs = t.num_args(); + std::vector args; + if(t.decl().get_decl_kind() == Equal){ + expr lhs = t.arg(0); + expr rhs = t.arg(1); + if(rhs.decl().get_decl_kind() == Ite){ + expr rhs_args[3]; + lhs = ElimIteRec(memo,lhs,cnsts); + for(int i = 0; i < 3; i++) + rhs_args[i] = ElimIteRec(memo,rhs.arg(i),cnsts); + res = (rhs_args[0] && (lhs == rhs_args[1])) || ((!rhs_args[0]) && (lhs == rhs_args[2])); + goto done; + } + } + if(t.decl().get_decl_kind() == Ite){ + func_decl sym = ctx.fresh_func_decl("@ite", t.get_sort()); + res = sym(); + cnsts.push_back(ElimIteRec(memo,ctx.make(Equal,res,t),cnsts)); + } + else { + for(int i = 0; i < nargs; i++) + args.push_back(ElimIteRec(memo,t.arg(i),cnsts)); + res = t.decl()(args.size(),&args[0]); + } + } + else if(t.is_quantifier()) + res = clone_quantifier(t,ElimIteRec(memo,t.body(),cnsts)); + else + res = t; + } + done: + return res; + } + + RPFP::Term RPFP::ElimIte(const Term &t){ + hash_map memo; + std::vector cnsts; + expr res = ElimIteRec(memo,t,cnsts); + if(!cnsts.empty()){ + cnsts.push_back(res); + res = ctx.make(And,cnsts); + } + return res; + } + void RPFP::Implicant(hash_map &memo, const Term &f, std::vector &lits, hash_set &dont_cares){ hash_set done[2]; ImplicantRed(memo,f,lits,done,true, dont_cares); @@ -2622,7 +2852,7 @@ namespace Duality { else { std::cout << "bad in InterpolateByCase -- core:\n"; std::vector assumps; - slvr.get_proof().get_assumptions(assumps); + slvr().get_proof().get_assumptions(assumps); for(unsigned i = 0; i < assumps.size(); i++) assumps[i].show(); throw "ack!"; @@ -2651,10 +2881,20 @@ namespace Duality { timer_stop("Generalize"); } + RPFP::LogicSolver *RPFP_caching::SolverForEdge(Edge *edge, bool models){ + uptr &p = edge_solvers[edge]; + if(!p.get()){ + scoped_no_proof no_proofs_please(ctx.m()); // no proofs + p.set(new iZ3LogicSolver(ctx,models)); // no models + } + return p.get(); + } + // caching version of above void RPFP_caching::GeneralizeCache(Edge *edge){ timer_start("Generalize"); + scoped_solver_for_edge ssfe(this,edge); Node *node = edge->Parent; std::vector assumps, core, conjuncts; AssertEdgeCache(edge,assumps); @@ -2698,6 +2938,7 @@ namespace Duality { // caching version of above bool RPFP_caching::PropagateCache(Edge *edge){ timer_start("PropagateCache"); + scoped_solver_for_edge ssfe(this,edge); bool some = false; { std::vector candidates, skip; @@ -2723,6 +2964,8 @@ namespace Duality { AssertEdgeCache(edge,assumps); for(unsigned i = 0; i < edge->Children.size(); i++){ expr ass = GetAnnotation(edge->Children[i]); + if(eq(ass,ctx.bool_val(true))) + continue; std::vector clauses; CollectConjuncts(ass.arg(1),clauses); for(unsigned j = 0; j < clauses.size(); j++) @@ -2807,6 +3050,17 @@ namespace Duality { return ctx.function(name.c_str(), nargs, &sorts[0], t.get_sort()); } + Z3User::FuncDecl Z3User::RenumberPred(const FuncDecl &f, int n) + { + std::string name = f.name().str(); + name = name.substr(0,name.rfind('_')) + "_" + string_of_int(n); + int arity = f.arity(); + std::vector domain; + for(int i = 0; i < arity; i++) + domain.push_back(f.domain(i)); + return ctx.function(name.c_str(), arity, &domain[0], f.range()); + } + // Scan the clause body for occurrences of the predicate unknowns RPFP::Term RPFP::ScanBody(hash_map &memo, @@ -3135,6 +3389,7 @@ namespace Duality { Term labeled = body; std::vector lbls; // TODO: throw this away for now body = RemoveLabels(body,lbls); + // body = IneqToEq(body); // UFO converts x=y to (x<=y & x >= y). Undo this. body = body.simplify(); #ifdef USE_QE_LITE @@ -3155,9 +3410,325 @@ namespace Duality { edge->labeled = labeled;; // remember for label extraction // edges.push_back(edge); } + + // undo hoisting of expressions out of loops + RemoveDeadNodes(); + Unhoist(); + // FuseEdges(); } + // The following mess is used to undo hoisting of expressions outside loops by compilers + + expr RPFP::UnhoistPullRec(hash_map & memo, const expr &w, hash_map & init_defs, hash_map & const_params, hash_map &const_params_inv, std::vector &new_params){ + if(memo.find(w) != memo.end()) + return memo[w]; + expr res; + if(init_defs.find(w) != init_defs.end()){ + expr d = init_defs[w]; + std::vector vars; + hash_set get_vars_memo; + GetVarsRec(get_vars_memo,d,vars); + hash_map map; + for(unsigned j = 0; j < vars.size(); j++){ + expr x = vars[j]; + map[x] = UnhoistPullRec(memo,x,init_defs,const_params,const_params_inv,new_params); + } + expr defn = SubstRec(map,d); + res = defn; + } + else if(const_params_inv.find(w) == const_params_inv.end()){ + std::string old_name = w.decl().name().str(); + func_decl fresh = ctx.fresh_func_decl(old_name.c_str(), w.get_sort()); + expr y = fresh(); + const_params[y] = w; + const_params_inv[w] = y; + new_params.push_back(y); + res = y; + } + else + res = const_params_inv[w]; + memo[w] = res; + return res; + } + + void RPFP::AddParamsToTransformer(Transformer &trans, const std::vector ¶ms){ + std::copy(params.begin(),params.end(),std::inserter(trans.IndParams,trans.IndParams.end())); + } + + expr RPFP::AddParamsToApp(const expr &app, const func_decl &new_decl, const std::vector ¶ms){ + int n = app.num_args(); + std::vector args(n); + for (int i = 0; i < n; i++) + args[i] = app.arg(i); + std::copy(params.begin(),params.end(),std::inserter(args,args.end())); + return new_decl(args); + } + + expr RPFP::GetRelRec(hash_set &memo, const expr &t, const func_decl &rel){ + if(memo.find(t) != memo.end()) + return expr(); + memo.insert(t); + if (t.is_app()) + { + func_decl f = t.decl(); + if(f == rel) + return t; + int nargs = t.num_args(); + for(int i = 0; i < nargs; i++){ + expr res = GetRelRec(memo,t.arg(i),rel); + if(!res.null()) + return res; + } + } + else if (t.is_quantifier()) + return GetRelRec(memo,t.body(),rel); + return expr(); + } + + expr RPFP::GetRel(Edge *edge, int child_idx){ + func_decl &rel = edge->F.RelParams[child_idx]; + hash_set memo; + return GetRelRec(memo,edge->F.Formula,rel); + } + + void RPFP::GetDefsRec(const expr &cnst, hash_map &defs){ + if(cnst.is_app()){ + switch(cnst.decl().get_decl_kind()){ + case And: { + int n = cnst.num_args(); + for(int i = 0; i < n; i++) + GetDefsRec(cnst.arg(i),defs); + break; + } + case Equal: { + expr lhs = cnst.arg(0); + expr rhs = cnst.arg(1); + if(IsVar(lhs)) + defs[lhs] = rhs; + break; + } + default: + break; + } + } + } + + void RPFP::GetDefs(const expr &cnst, hash_map &defs){ + // GetDefsRec(IneqToEq(cnst),defs); + GetDefsRec(cnst,defs); + } + + bool RPFP::IsVar(const expr &t){ + return t.is_app() && t.num_args() == 0 && t.decl().get_decl_kind() == Uninterpreted; + } + + void RPFP::GetVarsRec(hash_set &memo, const expr &t, std::vector &vars){ + if(memo.find(t) != memo.end()) + return; + memo.insert(t); + if (t.is_app()) + { + if(IsVar(t)){ + vars.push_back(t); + return; + } + int nargs = t.num_args(); + for(int i = 0; i < nargs; i++){ + GetVarsRec(memo,t.arg(i),vars); + } + } + else if (t.is_quantifier()) + GetVarsRec(memo,t.body(),vars); + } + + void RPFP::AddParamsToNode(Node *node, const std::vector ¶ms){ + int arity = node->Annotation.IndParams.size(); + std::vector domain; + for(int i = 0; i < arity; i++) + domain.push_back(node->Annotation.IndParams[i].get_sort()); + for(unsigned i = 0; i < params.size(); i++) + domain.push_back(params[i].get_sort()); + std::string old_name = node->Name.name().str(); + func_decl fresh = ctx.fresh_func_decl(old_name.c_str(), domain, ctx.bool_sort()); + node->Name = fresh; + AddParamsToTransformer(node->Annotation,params); + AddParamsToTransformer(node->Bound,params); + AddParamsToTransformer(node->Underapprox,params); + } + + void RPFP::UnhoistLoop(Edge *loop_edge, Edge *init_edge){ + loop_edge->F.Formula = IneqToEq(loop_edge->F.Formula); + init_edge->F.Formula = IneqToEq(init_edge->F.Formula); + expr pre = GetRel(loop_edge,0); + if(pre.null()) + return; // this means the loop got simplified away + int nparams = loop_edge->F.IndParams.size(); + hash_map const_params, const_params_inv; + std::vector work_list; + // find the parameters that are constant in the loop + for(int i = 0; i < nparams; i++){ + if(eq(pre.arg(i),loop_edge->F.IndParams[i])){ + const_params[pre.arg(i)] = init_edge->F.IndParams[i]; + const_params_inv[init_edge->F.IndParams[i]] = pre.arg(i); + work_list.push_back(pre.arg(i)); + } + } + // get the definitions in the initialization + hash_map defs,memo,subst; + GetDefs(init_edge->F.Formula,defs); + // try to pull them inside the loop + std::vector new_params; + for(unsigned i = 0; i < work_list.size(); i++){ + expr v = work_list[i]; + expr w = const_params[v]; + expr def = UnhoistPullRec(memo,w,defs,const_params,const_params_inv,new_params); + if(!eq(def,v)) + subst[v] = def; + } + // do the substitutions + if(subst.empty()) + return; + subst[pre] = pre; // don't substitute inside the precondition itself + loop_edge->F.Formula = SubstRec(subst,loop_edge->F.Formula); + loop_edge->F.Formula = ElimIte(loop_edge->F.Formula); + init_edge->F.Formula = ElimIte(init_edge->F.Formula); + // add the new parameters + if(new_params.empty()) + return; + Node *parent = loop_edge->Parent; + AddParamsToNode(parent,new_params); + AddParamsToTransformer(loop_edge->F,new_params); + AddParamsToTransformer(init_edge->F,new_params); + std::vector &incoming = parent->Incoming; + for(unsigned i = 0; i < incoming.size(); i++){ + Edge *in_edge = incoming[i]; + std::vector &chs = in_edge->Children; + for(unsigned j = 0; j < chs.size(); j++) + if(chs[j] == parent){ + expr lit = GetRel(in_edge,j); + expr new_lit = AddParamsToApp(lit,parent->Name,new_params); + func_decl fd = SuffixFuncDecl(new_lit,j); + int nargs = new_lit.num_args(); + std::vector args; + for(int k = 0; k < nargs; k++) + args.push_back(new_lit.arg(k)); + new_lit = fd(nargs,&args[0]); + in_edge->F.RelParams[j] = fd; + hash_map map; + map[lit] = new_lit; + in_edge->F.Formula = SubstRec(map,in_edge->F.Formula); + } + } + } + + void RPFP::Unhoist(){ + hash_map > outgoing; + for(unsigned i = 0; i < edges.size(); i++) + outgoing[edges[i]->Parent].push_back(edges[i]); + for(unsigned i = 0; i < nodes.size(); i++){ + Node *node = nodes[i]; + std::vector &outs = outgoing[node]; + // if we're not a simple loop with one entry, give up + if(outs.size() == 2){ + for(int j = 0; j < 2; j++){ + Edge *loop_edge = outs[j]; + Edge *init_edge = outs[1-j]; + if(loop_edge->Children.size() == 1 && loop_edge->Children[0] == loop_edge->Parent){ + UnhoistLoop(loop_edge,init_edge); + break; + } + } + } + } + } + + void RPFP::FuseEdges(){ + hash_map > outgoing; + for(unsigned i = 0; i < edges.size(); i++){ + outgoing[edges[i]->Parent].push_back(edges[i]); + } + hash_set edges_to_delete; + for(unsigned i = 0; i < nodes.size(); i++){ + Node *node = nodes[i]; + std::vector &outs = outgoing[node]; + if(outs.size() > 1 && outs.size() <= 16){ + std::vector trs(outs.size()); + for(unsigned j = 0; j < outs.size(); j++) + trs[j] = &outs[j]->F; + Transformer tr = Fuse(trs); + std::vector chs; + for(unsigned j = 0; j < outs.size(); j++) + for(unsigned k = 0; k < outs[j]->Children.size(); k++) + chs.push_back(outs[j]->Children[k]); + Edge *fedge = CreateEdge(node,tr,chs); + for(unsigned j = 0; j < outs.size(); j++) + edges_to_delete.insert(outs[j]); + } + } + std::vector new_edges; + hash_set all_nodes; + for(unsigned j = 0; j < edges.size(); j++){ + if(edges_to_delete.find(edges[j]) == edges_to_delete.end()){ +#if 0 + if(all_nodes.find(edges[j]->Parent) != all_nodes.end()) + throw "help!"; + all_nodes.insert(edges[j]->Parent); +#endif + new_edges.push_back(edges[j]); + } + else + delete edges[j]; + } + edges.swap(new_edges); + } + + void RPFP::MarkLiveNodes(hash_map > &outgoing, hash_set &live_nodes, Node *node){ + if(live_nodes.find(node) != live_nodes.end()) + return; + live_nodes.insert(node); + std::vector &outs = outgoing[node]; + for(unsigned i = 0; i < outs.size(); i++) + for(unsigned j = 0; j < outs[i]->Children.size(); j++) + MarkLiveNodes(outgoing, live_nodes,outs[i]->Children[j]); + } + + void RPFP::RemoveDeadNodes(){ + hash_map > outgoing; + for(unsigned i = 0; i < edges.size(); i++) + outgoing[edges[i]->Parent].push_back(edges[i]); + hash_set live_nodes; + for(unsigned i = 0; i < nodes.size(); i++) + if(!nodes[i]->Bound.IsFull()) + MarkLiveNodes(outgoing,live_nodes,nodes[i]); + std::vector new_edges; + for(unsigned j = 0; j < edges.size(); j++){ + if(live_nodes.find(edges[j]->Parent) != live_nodes.end()) + new_edges.push_back(edges[j]); + else { + Edge *edge = edges[j]; + 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; + } + } + } + delete edge; + } + } + edges.swap(new_edges); + std::vector new_nodes; + for(unsigned j = 0; j < nodes.size(); j++){ + if(live_nodes.find(nodes[j]) != live_nodes.end()) + new_nodes.push_back(nodes[j]); + else + delete nodes[j]; + } + nodes.swap(new_nodes); + } void RPFP::WriteSolution(std::ostream &s){ for(unsigned i = 0; i < nodes.size(); i++){ diff --git a/src/duality/duality_solver.cpp b/src/duality/duality_solver.cpp index 33318b207..91532960b 100644 --- a/src/duality/duality_solver.cpp +++ b/src/duality/duality_solver.cpp @@ -45,8 +45,8 @@ Revision History: // #define EFFORT_BOUNDED_STRAT #define SKIP_UNDERAPPROX_NODES #define USE_RPFP_CLONE -#define KEEP_EXPANSIONS -#define USE_CACHING_RPFP +// #define KEEP_EXPANSIONS +// #define USE_CACHING_RPFP // #define PROPAGATE_BEFORE_CHECK #define USE_NEW_GEN_CANDS @@ -105,7 +105,7 @@ namespace Duality { public: Duality(RPFP *_rpfp) : ctx(_rpfp->ctx), - slvr(_rpfp->slvr), + slvr(_rpfp->slvr()), nodes(_rpfp->nodes), edges(_rpfp->edges) { @@ -122,7 +122,7 @@ namespace Duality { { scoped_no_proof no_proofs_please(ctx.m()); #ifdef USE_RPFP_CLONE - clone_ls = new RPFP::iZ3LogicSolver(ctx); + clone_ls = new RPFP::iZ3LogicSolver(ctx, false); // no models needed for this one clone_rpfp = new RPFP_caching(clone_ls); clone_rpfp->Clone(rpfp); #endif @@ -842,8 +842,10 @@ namespace Duality { Node *child = chs[i]; if(TopoSort[child] < TopoSort[node->map]){ Node *leaf = LeafMap[child]; - if(!indset->Contains(leaf)) + if(!indset->Contains(leaf)){ + node->Outgoing->F.Formula = ctx.bool_val(false); // make this a proper leaf, else bogus cex return node->Outgoing; + } } } @@ -1206,7 +1208,7 @@ namespace Duality { Node *CheckerForEdgeClone(Edge *edge, RPFP_caching *checker){ - Edge *gen_cands_edge = gen_cands_rpfp->GetEdgeClone(edge); + Edge *gen_cands_edge = checker->GetEdgeClone(edge); Node *root = gen_cands_edge->Parent; root->Outgoing = gen_cands_edge; GenNodeSolutionFromIndSet(edge->Parent, root->Bound); @@ -1233,7 +1235,7 @@ namespace Duality { Edge *edge = edges[i]; if(!full_scan && updated_nodes.find(edge->Parent) == updated_nodes.end()) continue; -#ifndef USE_RPFP_CLONE +#ifndef USE_NEW_GEN_CANDS slvr.push(); RPFP *checker = new RPFP(rpfp->ls); Node *root = CheckerForEdge(edge,checker); @@ -1246,15 +1248,16 @@ namespace Duality { slvr.pop(1); delete checker; #else - clone_rpfp->Push(); - Node *root = CheckerForEdgeClone(edge,clone_rpfp); - if(clone_rpfp->Check(root) != unsat){ + RPFP_caching::scoped_solver_for_edge(gen_cands_rpfp,edge,true /* models */); + gen_cands_rpfp->Push(); + Node *root = CheckerForEdgeClone(edge,gen_cands_rpfp); + if(gen_cands_rpfp->Check(root) != unsat){ Candidate candidate; - ExtractCandidateFromCex(edge,clone_rpfp,root,candidate); + ExtractCandidateFromCex(edge,gen_cands_rpfp,root,candidate); reporter->InductionFailure(edge,candidate.Children); candidates.push_back(candidate); } - clone_rpfp->Pop(1); + gen_cands_rpfp->Pop(1); #endif } updated_nodes.clear(); @@ -1555,7 +1558,7 @@ namespace Duality { public: DerivationTree(Duality *_duality, RPFP *rpfp, Reporter *_reporter, Heuristic *_heuristic, bool _full_expand) - : slvr(rpfp->slvr), + : slvr(rpfp->slvr()), ctx(rpfp->ctx) { duality = _duality; @@ -1709,7 +1712,7 @@ namespace Duality { // tree->RemoveEdge(p->Outgoing); Edge *ne = p->Outgoing; if(ne) { - reporter->Message("Recycling edge..."); + // reporter->Message("Recycling edge..."); std::vector &cs = ne->Children; for(unsigned i = 0; i < cs.size(); i++) InitializeApproximatedInstance(cs[i]); @@ -1905,14 +1908,14 @@ namespace Duality { virtual bool Build(){ - stack.back().level = tree->slvr.get_scope_level(); + stack.back().level = tree->slvr().get_scope_level(); bool was_sat = true; while (true) { lbool res; - unsigned slvr_level = tree->slvr.get_scope_level(); + unsigned slvr_level = tree->slvr().get_scope_level(); if(slvr_level != stack.back().level) throw "stacks out of sync!"; @@ -2002,11 +2005,11 @@ namespace Duality { tree->FixCurrentState(expansions[i]->Outgoing); } #if 0 - if(tree->slvr.check() == unsat) + if(tree->slvr().check() == unsat) throw "help!"; #endif stack.push_back(stack_entry()); - stack.back().level = tree->slvr.get_scope_level(); + stack.back().level = tree->slvr().get_scope_level(); if(ExpandSomeNodes(false,1)){ continue; } @@ -2135,6 +2138,7 @@ namespace Duality { tree->Generalize(top,node); #else RPFP_caching *clone_rpfp = duality->clone_rpfp; + if(!node->Outgoing->map) return; Edge *clone_edge = clone_rpfp->GetEdgeClone(node->Outgoing->map); Node *clone_node = clone_edge->Parent; clone_node->Annotation = node->Annotation; @@ -2142,10 +2146,11 @@ namespace Duality { clone_edge->Children[i]->Annotation = node->map->Outgoing->Children[i]->Annotation; clone_rpfp->GeneralizeCache(clone_edge); node->Annotation = clone_node->Annotation; - } #endif + } bool Propagate(Node *node){ +#ifdef USE_RPFP_CLONE RPFP_caching *clone_rpfp = duality->clone_rpfp; Edge *clone_edge = clone_rpfp->GetEdgeClone(node->Outgoing->map); Node *clone_node = clone_edge->Parent; @@ -2156,6 +2161,9 @@ namespace Duality { if(res) node->Annotation = clone_node->Annotation; return res; +#else + return false; +#endif } }; @@ -2179,6 +2187,11 @@ namespace Duality { Duality *parent; bool some_updates; +#define NO_CONJ_ON_SIMPLE_LOOPS +#ifdef NO_CONJ_ON_SIMPLE_LOOPS + hash_set simple_loops; +#endif + Node *&covered_by(Node *node){ return cm[node].covered_by; } @@ -2213,6 +2226,24 @@ namespace Duality { Covering(Duality *_parent){ parent = _parent; some_updates = false; + +#ifdef NO_CONJ_ON_SIMPLE_LOOPS + hash_map > outgoing; + for(unsigned i = 0; i < parent->rpfp->edges.size(); i++) + outgoing[parent->rpfp->edges[i]->Parent].push_back(parent->rpfp->edges[i]); + for(unsigned i = 0; i < parent->rpfp->nodes.size(); i++){ + Node * node = parent->rpfp->nodes[i]; + std::vector &outs = outgoing[node]; + if(outs.size() == 2){ + for(int j = 0; j < 2; j++){ + Edge *loop_edge = outs[j]; + if(loop_edge->Children.size() == 1 && loop_edge->Children[0] == loop_edge->Parent) + simple_loops.insert(node); + } + } + } +#endif + } bool IsCoveredRec(hash_set &memo, Node *node){ @@ -2375,6 +2406,11 @@ namespace Duality { } bool CouldCover(Node *covered, Node *covering){ +#ifdef NO_CONJ_ON_SIMPLE_LOOPS + // Forsimple loops, we rely on propagation, not covering + if(simple_loops.find(covered->map) != simple_loops.end()) + return false; +#endif #ifdef UNDERAPPROX_NODES // if(parent->underapprox_map.find(covering) != parent->underapprox_map.end()) // return parent->underapprox_map[covering] == covered; diff --git a/src/duality/duality_wrapper.cpp b/src/duality/duality_wrapper.cpp index dd1828214..24f6a5e20 100644 --- a/src/duality/duality_wrapper.cpp +++ b/src/duality/duality_wrapper.cpp @@ -30,10 +30,11 @@ Revision History: namespace Duality { - solver::solver(Duality::context& c, bool extensional) : object(c), the_model(c) { + solver::solver(Duality::context& c, bool extensional, bool models) : object(c), the_model(c) { params_ref p; p.set_bool("proof", true); // this is currently useless - p.set_bool("model", true); + if(models) + 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 @@ -374,6 +375,18 @@ expr context::make_quant(decl_kind op, const std::vector &_sorts, const st } + unsigned func_decl::arity() const { + return (to_func_decl(raw())->get_arity()); + } + + sort func_decl::domain(unsigned i) const { + return sort(ctx(),(to_func_decl(raw())->get_domain(i))); + } + + sort func_decl::range() const { + return sort(ctx(),(to_func_decl(raw())->get_range())); + } + func_decl context::fresh_func_decl(char const * prefix, const std::vector &domain, sort const & range){ std::vector < ::sort * > _domain(domain.size()); for(unsigned i = 0; i < domain.size(); i++) diff --git a/src/duality/duality_wrapper.h b/src/duality/duality_wrapper.h index 0de3a7d49..94e8d2642 100755 --- a/src/duality/duality_wrapper.h +++ b/src/duality/duality_wrapper.h @@ -819,7 +819,7 @@ namespace Duality { bool canceled; proof_gen_mode m_mode; public: - solver(context & c, bool extensional = false); + solver(context & c, bool extensional = false, bool models = true); 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() { @@ -1308,8 +1308,8 @@ namespace Duality { class interpolating_solver : public solver { public: - interpolating_solver(context &ctx) - : solver(ctx) + interpolating_solver(context &ctx, bool models = true) + : solver(ctx, true, models) { weak_mode = false; } @@ -1373,6 +1373,21 @@ namespace Duality { typedef double clock_t; clock_t current_time(); inline void output_time(std::ostream &os, clock_t time){os << time;} + + template class uptr { + public: + X *ptr; + uptr(){ptr = 0;} + void set(X *_ptr){ + if(ptr) delete ptr; + ptr = _ptr; + } + X *get(){ return ptr;} + ~uptr(){ + if(ptr) delete ptr; + } + }; + }; // to make Duality::ast hashable diff --git a/src/interp/iz3mgr.cpp b/src/interp/iz3mgr.cpp index f35dae93f..994d10e06 100644 --- a/src/interp/iz3mgr.cpp +++ b/src/interp/iz3mgr.cpp @@ -640,9 +640,9 @@ void iz3mgr::get_assign_bounds_rule_coeffs(const ast &proof, std::vector &coeffs, const std::vector &ineqs){ +iz3mgr::ast iz3mgr::sum_inequalities(const std::vector &coeffs, const std::vector &ineqs, bool round_off){ ast zero = make_int("0"); ast thing = make(Leq,zero,zero); for(unsigned i = 0; i < ineqs.size(); i++){ - linear_comb(thing,coeffs[i],ineqs[i]); + linear_comb(thing,coeffs[i],ineqs[i], round_off); } thing = simplify_ineq(thing); return thing; diff --git a/src/interp/iz3mgr.h b/src/interp/iz3mgr.h index 645c72ccb..c3bde91c5 100644 --- a/src/interp/iz3mgr.h +++ b/src/interp/iz3mgr.h @@ -606,9 +606,9 @@ class iz3mgr { return d; } - void linear_comb(ast &P, const ast &c, const ast &Q); + void linear_comb(ast &P, const ast &c, const ast &Q, bool round_off = false); - ast sum_inequalities(const std::vector &coeffs, const std::vector &ineqs); + ast sum_inequalities(const std::vector &coeffs, const std::vector &ineqs, bool round_off = false); ast simplify_ineq(const ast &ineq){ ast res = make(op(ineq),arg(ineq,0),z3_simplify(arg(ineq,1))); diff --git a/src/interp/iz3translate.cpp b/src/interp/iz3translate.cpp index 2fbc173a9..abddb4bda 100755 --- a/src/interp/iz3translate.cpp +++ b/src/interp/iz3translate.cpp @@ -1079,7 +1079,7 @@ public: my_cons.push_back(mk_not(arg(con,i))); my_coeffs.push_back(farkas_coeffs[i]); } - ast farkas_con = normalize_inequality(sum_inequalities(my_coeffs,my_cons)); + ast farkas_con = normalize_inequality(sum_inequalities(my_coeffs,my_cons,true /* round_off */)); my_cons.push_back(mk_not(farkas_con)); my_coeffs.push_back(make_int("1")); std::vector my_hyps; @@ -1103,7 +1103,7 @@ public: my_cons.push_back(conc(prem(proof,i-1))); my_coeffs.push_back(farkas_coeffs[i]); } - ast farkas_con = normalize_inequality(sum_inequalities(my_coeffs,my_cons)); + ast farkas_con = normalize_inequality(sum_inequalities(my_coeffs,my_cons,true /* round_off */)); std::vector my_hyps; for(int i = 1; i < nargs; i++) my_hyps.push_back(prems[i-1]); From f111dd4e612ba2b0edfc9476f94aec2a5c093b94 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Tue, 28 Jan 2014 14:00:42 +0000 Subject: [PATCH 08/12] Fixes for the build on OS X 10.9 --- src/api/api_interp.cpp | 1 + src/interp/iz3hash.h | 2 +- src/interp/iz3mgr.cpp | 4 ++-- src/interp/iz3mgr.h | 1 + src/interp/iz3pp.cpp | 10 +++++----- 5 files changed, 10 insertions(+), 8 deletions(-) diff --git a/src/api/api_interp.cpp b/src/api/api_interp.cpp index 560ee5885..98722022c 100644 --- a/src/api/api_interp.cpp +++ b/src/api/api_interp.cpp @@ -17,6 +17,7 @@ Revision History: --*/ #include #include +#include #include"z3.h" #include"api_log_macros.h" #include"api_context.h" diff --git a/src/interp/iz3hash.h b/src/interp/iz3hash.h index 75d9aa604..94f282265 100755 --- a/src/interp/iz3hash.h +++ b/src/interp/iz3hash.h @@ -66,7 +66,7 @@ Revision History: namespace stl_ext { template <> class hash { - stl_ext::hash H; + stl_ext::hash H; public: size_t operator()(const std::string &s) const { return H(s.c_str()); diff --git a/src/interp/iz3mgr.cpp b/src/interp/iz3mgr.cpp index f35dae93f..b85df81be 100644 --- a/src/interp/iz3mgr.cpp +++ b/src/interp/iz3mgr.cpp @@ -172,7 +172,7 @@ iz3mgr::ast iz3mgr::make_quant(opr op, const std::vector &bvs, ast &body){ std::vector names; - std::vector types; + std::vector types; std::vector bound_asts; unsigned num_bound = bvs.size(); @@ -485,7 +485,7 @@ void iz3mgr::get_farkas_coeffs(const ast &proof, std::vector& coeffs){ get_farkas_coeffs(proof,rats); coeffs.resize(rats.size()); for(unsigned i = 0; i < rats.size(); i++){ - sort *is = m().mk_sort(m_arith_fid, INT_SORT); + class sort *is = m().mk_sort(m_arith_fid, INT_SORT); ast coeff = cook(m_arith_util.mk_numeral(rats[i],is)); coeffs[i] = coeff; } diff --git a/src/interp/iz3mgr.h b/src/interp/iz3mgr.h index 645c72ccb..7da247287 100644 --- a/src/interp/iz3mgr.h +++ b/src/interp/iz3mgr.h @@ -22,6 +22,7 @@ Revision History: #include +#include #include "iz3hash.h" #include"well_sorted.h" diff --git a/src/interp/iz3pp.cpp b/src/interp/iz3pp.cpp index df6fcaf53..31b375c0f 100644 --- a/src/interp/iz3pp.cpp +++ b/src/interp/iz3pp.cpp @@ -58,20 +58,20 @@ namespace stl_ext { class free_func_visitor { ast_manager& m; func_decl_set m_funcs; - obj_hashtable m_sorts; + obj_hashtable m_sorts; public: free_func_visitor(ast_manager& m): m(m) {} void operator()(var * n) { } void operator()(app * n) { m_funcs.insert(n->get_decl()); - sort* s = m.get_sort(n); + class sort* s = m.get_sort(n); if (s->get_family_id() == null_family_id) { m_sorts.insert(s); } } void operator()(quantifier * n) { } func_decl_set& funcs() { return m_funcs; } - obj_hashtable& sorts() { return m_sorts; } + obj_hashtable& sorts() { return m_sorts; } }; class iz3pp_helper : public iz3mgr { @@ -146,8 +146,8 @@ void iz3pp(ast_manager &m, func_decl_set &funcs = visitor.funcs(); func_decl_set::iterator it = funcs.begin(), end = funcs.end(); - obj_hashtable& sorts = visitor.sorts(); - obj_hashtable::iterator sit = sorts.begin(), send = sorts.end(); + obj_hashtable& sorts = visitor.sorts(); + obj_hashtable::iterator sit = sorts.begin(), send = sorts.end(); From 19830bcd333e904aa26485b1e2d932bbe0f79ca7 Mon Sep 17 00:00:00 2001 From: Ken McMillan Date: Tue, 28 Jan 2014 11:43:00 -0800 Subject: [PATCH 09/12] fix a few warnings --- src/cmd_context/interpolant_cmds.cpp | 3 ++- src/duality/duality_rpfp.cpp | 2 +- src/interp/iz3translate_direct.cpp | 2 ++ 3 files changed, 5 insertions(+), 2 deletions(-) diff --git a/src/cmd_context/interpolant_cmds.cpp b/src/cmd_context/interpolant_cmds.cpp index 2a7de3176..318569cd5 100644 --- a/src/cmd_context/interpolant_cmds.cpp +++ b/src/cmd_context/interpolant_cmds.cpp @@ -139,10 +139,11 @@ static void get_interpolant(cmd_context & ctx, expr * t, params_ref &m_params) { get_interpolant_and_maybe_check(ctx,t,m_params,false); } +#if 0 static void get_and_check_interpolant(cmd_context & ctx, params_ref &m_params, expr * t) { get_interpolant_and_maybe_check(ctx,t,m_params,true); } - +#endif static void compute_interpolant_and_maybe_check(cmd_context & ctx, expr * t, params_ref &m_params, bool check){ diff --git a/src/duality/duality_rpfp.cpp b/src/duality/duality_rpfp.cpp index ad89c1314..17b93d35b 100644 --- a/src/duality/duality_rpfp.cpp +++ b/src/duality/duality_rpfp.cpp @@ -3661,7 +3661,7 @@ namespace Duality { for(unsigned j = 0; j < outs.size(); j++) for(unsigned k = 0; k < outs[j]->Children.size(); k++) chs.push_back(outs[j]->Children[k]); - Edge *fedge = CreateEdge(node,tr,chs); + CreateEdge(node,tr,chs); for(unsigned j = 0; j < outs.size(); j++) edges_to_delete.insert(outs[j]); } diff --git a/src/interp/iz3translate_direct.cpp b/src/interp/iz3translate_direct.cpp index 4b7d47e0f..0ce3297af 100755 --- a/src/interp/iz3translate_direct.cpp +++ b/src/interp/iz3translate_direct.cpp @@ -58,7 +58,9 @@ namespace stl_ext { static int lemma_count = 0; +#if 0 static int nll_lemma_count = 0; +#endif #define SHOW_LEMMA_COUNT -1 // One half of a resolution. We need this to distinguish From 9ba4b532f621fadc89f29aa395ac62da6f8f5555 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 2 Feb 2014 13:48:02 +0100 Subject: [PATCH 10/12] testing simplex Signed-off-by: Nikolaj Bjorner --- src/math/simplex/simplex.h | 8 +- src/math/simplex/simplex_def.h | 88 ++++++++++++++------ src/math/simplex/sparse_matrix.h | 8 +- src/math/simplex/sparse_matrix_def.h | 28 ++----- src/test/simplex.cpp | 118 ++++++++++++++++++++++++++- 5 files changed, 199 insertions(+), 51 deletions(-) diff --git a/src/math/simplex/simplex.h b/src/math/simplex/simplex.h index 974aa7cfb..bcc76c64f 100644 --- a/src/math/simplex/simplex.h +++ b/src/math/simplex/simplex.h @@ -111,7 +111,7 @@ namespace simplex { typedef typename matrix::col_iterator col_iterator; void ensure_var(var_t v); - row add_row(unsigned num_vars, var_t base, var_t const* vars, numeral const* coeffs); + row add_row(var_t base, unsigned num_vars, var_t const* vars, numeral const* coeffs); void del_row(row const& r); void set_lower(var_t var, eps_numeral const& b); void set_upper(var_t var, eps_numeral const& b); @@ -125,6 +125,9 @@ namespace simplex { eps_numeral const& get_value(var_t v); void display(std::ostream& out) const; + unsigned get_num_vars() const { return m_vars.size(); } + + private: var_t select_var_to_fix(); @@ -159,10 +162,11 @@ namespace simplex { bool outside_bounds(var_t v) const { return below_lower(v) || above_upper(v); } bool is_free(var_t v) const { return !m_vars[v].m_lower_valid && !m_vars[v].m_upper_valid; } bool is_non_free(var_t v) const { return !is_free(v); } - unsigned get_num_vars() const { return m_vars.size(); } bool is_base(var_t x) const { return m_vars[x].m_is_base; } + void add_patch(var_t v); bool well_formed() const; + bool well_formed_row(row const& r) const; bool is_feasible() const; }; diff --git a/src/math/simplex/simplex_def.h b/src/math/simplex/simplex_def.h index 46915695f..631b89ce7 100644 --- a/src/math/simplex/simplex_def.h +++ b/src/math/simplex/simplex_def.h @@ -30,13 +30,26 @@ namespace simplex { SASSERT(found); ); scoped_numeral base_coeff(m); + scoped_eps_numeral value(em), tmp(em); row r = M.mk_row(); for (unsigned i = 0; i < num_vars; ++i) { - M.add(r, coeffs[i], vars[i]); - if (vars[i] == base) { - m.set(base_coeff, coeffs[i]); + if (!m.is_zero(coeffs[i])) { + var_t v = vars[i]; + M.add_var(r, coeffs[i], v); + if (v == base) { + m.set(base_coeff, coeffs[i]); + } + else { + SASSERT(!is_base(v)); + em.mul(m_vars[v].m_value, coeffs[i], tmp); + em.add(value, tmp, value); + } } } + em.neg(value); + em.div(value, base_coeff, value); + SASSERT(!m.is_zero(base_coeff)); + SASSERT(!m_vars[base].m_is_base); while (m_row2base.size() <= r.id()) { m_row2base.push_back(null_var); } @@ -44,9 +57,20 @@ namespace simplex { m_vars[base].m_base2row = r.id(); m_vars[base].m_is_base = true; m.set(m_vars[base].m_base_coeff, base_coeff); + em.set(m_vars[base].m_value, value); + add_patch(base); + SASSERT(well_formed_row(r)); return r; } + template + void simplex::add_patch(var_t v) { + SASSERT(is_base(v)); + if (outside_bounds(v)) { + m_to_patch.insert(v); + } + } + template void simplex::del_row(row const& r) { m_vars[m_row2base[r.id()]].m_is_base = false; @@ -114,8 +138,12 @@ namespace simplex { if (vi.m_lower_valid) out << em.to_string(vi.m_lower); else out << "-oo"; out << ":"; if (vi.m_upper_valid) out << em.to_string(vi.m_upper); else out << "oo"; - out << "]"; - if (vi.m_is_base) out << " b:" << vi.m_base2row; + out << "] "; + if (vi.m_is_base) out << "b:" << vi.m_base2row << " "; + col_iterator it = M.col_begin(i), end = M.col_end(i); + for (; it != end; ++it) { + out << "r" << it.get_row().id() << " "; + } out << "\n"; } } @@ -134,6 +162,7 @@ namespace simplex { unsigned num_iterations = 0; unsigned num_repeated = 0; var_t v = null_var; + SASSERT(well_formed()); while ((v = select_var_to_fix()) != null_var) { if (m_cancel || num_iterations > m_max_iterations) { return l_undef; @@ -143,8 +172,8 @@ namespace simplex { return l_false; } ++num_iterations; - SASSERT(well_formed()); } + SASSERT(well_formed()); return l_true; } @@ -188,18 +217,18 @@ namespace simplex { m.set(x_jI.m_base_coeff, a_ij); x_jI.m_is_base = true; x_iI.m_is_base = false; - if (outside_bounds(x_j)) { - m_to_patch.insert(x_j); - } + add_patch(x_j); + SASSERT(well_formed_row(row(r_i))); + col_iterator it = M.col_begin(x_j), end = M.col_end(x_j); scoped_numeral a_kj(m), g(m); for (; it != end; ++it) { row r_k = it.get_row(); - if (r_k != r_i) { + if (r_k.id() != r_i) { a_kj = it.get_row_entry().m_coeff; a_kj.neg(); M.mul(r_k, a_ij); - M.add(r_k, a_kj, r_i); + M.add(r_k, a_kj, row(r_i)); var_t s = m_row2base[r_k.id()]; numeral& coeff = m_vars[s].m_base_coeff; m.mul(coeff, a_ij, coeff); @@ -207,6 +236,7 @@ namespace simplex { if (!m.is_one(g)) { m.div(coeff, g, coeff); } + SASSERT(well_formed_row(row(r_k))); } } } @@ -240,8 +270,8 @@ namespace simplex { void simplex::update_value_core(var_t v, eps_numeral const& delta) { eps_numeral& val = m_vars[v].m_value; em.add(val, delta, val); - if (is_base(v) && outside_bounds(v)) { - m_to_patch.insert(v); + if (is_base(v)) { + add_patch(v); } } @@ -705,18 +735,7 @@ namespace simplex { var_t s = m_row2base[i]; if (s == null_var) continue; SASSERT(i == m_vars[s].m_base2row); - // - // TBD: extract coefficient of base variable and compare - // with m_vars[s].m_base_coeff; - // - // check that sum of assignments add up to 0 for every row. - row_iterator it = M.row_begin(row(i)), end = M.row_end(row(i)); - scoped_eps_numeral sum(em), tmp(em); - for (; it != end; ++it) { - em.mul(m_vars[it->m_var].m_value, it->m_coeff, tmp); - sum += tmp; - } - SASSERT(em.is_zero(sum)); + SASSERT(well_formed_row(row(i))); } return true; } @@ -729,6 +748,25 @@ namespace simplex { return true; } + template + bool simplex::well_formed_row(row const& r) const { + + // + // TBD: extract coefficient of base variable and compare + // with m_vars[s].m_base_coeff; + // + // check that sum of assignments add up to 0 for every row. + row_iterator it = M.row_begin(r), end = M.row_end(r); + scoped_eps_numeral sum(em), tmp(em); + for (; it != end; ++it) { + em.mul(m_vars[it->m_var].m_value, it->m_coeff, tmp); + sum += tmp; + } + SASSERT(em.is_zero(sum)); + + return true; + } + }; #endif diff --git a/src/math/simplex/sparse_matrix.h b/src/math/simplex/sparse_matrix.h index 6a85d69f0..d16d1d1cf 100644 --- a/src/math/simplex/sparse_matrix.h +++ b/src/math/simplex/sparse_matrix.h @@ -92,8 +92,7 @@ namespace simplex { void del_row_entry(unsigned idx); void compress(manager& m, vector & cols); void compress_if_needed(manager& m, vector & cols); - void save_var_pos(svector & result_map) const; - void reset_var_pos(svector & result_map) const; + void save_var_pos(svector & result_map, unsigned_vector& idxs) const; bool is_coeff_of(var_t v, numeral const & expected) const; int get_idx_of(var_t v) const; }; @@ -125,6 +124,7 @@ namespace simplex { svector m_dead_rows; // rows to recycle vector m_columns; // per var svector m_var_pos; // temporary map from variables to positions in row + unsigned_vector m_var_pos_idx; // indices in m_var_pos bool well_formed_row(unsigned row_id) const; bool well_formed_column(unsigned column_id) const; @@ -138,7 +138,7 @@ namespace simplex { class row { unsigned m_id; public: - row(unsigned r):m_id(r) {} + explicit row(unsigned r):m_id(r) {} row():m_id(UINT_MAX) {} bool operator!=(row const& other) const { return m_id != other.m_id; @@ -149,7 +149,7 @@ namespace simplex { void ensure_var(var_t v); row mk_row(); - void add(row r, numeral const& n, var_t var); + void add_var(row r, numeral const& n, var_t var); void add(row r, numeral const& n, row src); void mul(row r, numeral const& n); void neg(row r); diff --git a/src/math/simplex/sparse_matrix_def.h b/src/math/simplex/sparse_matrix_def.h index 20e9d676f..a170ee47f 100644 --- a/src/math/simplex/sparse_matrix_def.h +++ b/src/math/simplex/sparse_matrix_def.h @@ -134,31 +134,18 @@ namespace simplex { \brief Fill the map var -> pos/idx */ template - inline void sparse_matrix::_row::save_var_pos(svector & result_map) const { + inline void sparse_matrix::_row::save_var_pos(svector & result_map, unsigned_vector& idxs) const { typename vector<_row_entry>::const_iterator it = m_entries.begin(); typename vector<_row_entry>::const_iterator end = m_entries.end(); unsigned idx = 0; for (; it != end; ++it, ++idx) { if (!it->is_dead()) { result_map[it->m_var] = idx; + idxs.push_back(it->m_var); } } } - /** - \brief Reset the map var -> pos/idx. That is for all variables v in the row, set result[v] = -1 - This method can be viewed as the "inverse" of save_var_pos. - */ - template - inline void sparse_matrix::_row::reset_var_pos(svector & result_map) const { - typename vector<_row_entry>::const_iterator it = m_entries.begin(); - typename vector<_row_entry>::const_iterator end = m_entries.end(); - for (; it != end; ++it) { - if (!it->is_dead()) { - result_map[it->m_var] = -1; - } - } - } template int sparse_matrix::_row::get_idx_of(var_t v) const { @@ -316,7 +303,7 @@ namespace simplex { } template - void sparse_matrix::add(row dst, numeral const& n, var_t v) { + void sparse_matrix::add_var(row dst, numeral const& n, var_t v) { _row& r = m_rows[dst.id()]; column& c = m_columns[v]; unsigned r_idx; @@ -339,7 +326,7 @@ namespace simplex { _row & r1 = m_rows[row1.id()]; _row & r2 = m_rows[row2.id()]; - r1.save_var_pos(m_var_pos); + r1.save_var_pos(m_var_pos, m_var_pos_idx); // // loop over variables in row2, @@ -376,7 +363,6 @@ namespace simplex { } \ } \ } \ - ((void) 0) if (m.is_one(n)) { @@ -394,7 +380,11 @@ namespace simplex { m.add(r_entry.m_coeff, tmp, r_entry.m_coeff)); } - r1.reset_var_pos(m_var_pos); + // reset m_var_pos: + for (unsigned i = 0; i < m_var_pos_idx.size(); ++i) { + m_var_pos[m_var_pos_idx[i]] = -1; + } + m_var_pos_idx.reset(); r1.compress_if_needed(m, m_columns); } diff --git a/src/test/simplex.cpp b/src/test/simplex.cpp index def6f8be3..986caa30b 100644 --- a/src/test/simplex.cpp +++ b/src/test/simplex.cpp @@ -3,11 +3,123 @@ #include "simplex.h" #include "simplex_def.h" #include "mpq_inf.h" +#include "vector.h" +#include "rational.h" +#define R rational typedef simplex::simplex Simplex; +typedef simplex::sparse_matrix sparse_matrix; + +static vector vec(int i, int j) { + vector nv; + nv.resize(2); + nv[0] = R(i); + nv[1] = R(j); + return nv; +} + +static vector vec(int i, int j, int k) { + vector nv = vec(i, j); + nv.push_back(R(k)); + return nv; +} + +static vector vec(int i, int j, int k, int l) { + vector nv = vec(i, j, k); + nv.push_back(R(l)); + return nv; +} + +static vector vec(int i, int j, int k, int l, int x) { + vector nv = vec(i, j, k, l); + nv.push_back(R(x)); + return nv; +} + +static vector vec(int i, int j, int k, int l, int x, int y) { + vector nv = vec(i, j, k, l, x); + nv.push_back(R(y)); + return nv; +} + +static vector vec(int i, int j, int k, int l, int x, int y, int z) { + vector nv = vec(i, j, k, l, x, y); + nv.push_back(R(z)); + return nv; +} + + + +void add_row(Simplex& S, vector const& _v, R const& _b, bool is_eq = false) { + unsynch_mpz_manager m; + unsigned_vector vars; + vector v(_v); + R b(_b); + R l(denominator(b)); + scoped_mpz_vector coeffs(m); + for (unsigned i = 0; i < v.size(); ++i) { + l = lcm(l, denominator(v[i])); + vars.push_back(i); + S.ensure_var(i); + } + b *= l; + b.neg(); + for (unsigned i = 0; i < v.size(); ++i) { + v[i] *= l; + coeffs.push_back(v[i].to_mpq().numerator()); + } + unsigned nv = S.get_num_vars(); + vars.push_back(nv); + vars.push_back(nv+1); + S.ensure_var(nv); + S.ensure_var(nv+1); + coeffs.push_back(mpz(-1)); + coeffs.push_back(b.to_mpq().numerator()); + mpq_inf one(mpq(1),mpq(0)); + mpq_inf zero(mpq(0),mpq(0)); + SASSERT(vars.size() == coeffs.size()); + std::cout << coeffs.size() << " " << nv << "\n"; + for (unsigned i = 0; i < vars.size(); ++i) std::cout << vars[i] << " "; + std::cout << "\n"; + S.set_lower(nv, zero); + if (is_eq) S.set_upper(nv, zero); + S.set_lower(nv+1, one); + S.set_upper(nv+1, one); + S.add_row(nv, coeffs.size(), vars.c_ptr(), coeffs.c_ptr()); +} + +static void feas(Simplex& S) { + S.display(std::cout); + lbool is_sat = S.make_feasible(); + std::cout << "feasible: " << is_sat << "\n"; + S.display(std::cout); +} + +static void test1() { + Simplex S; + add_row(S, vec(1,0), R(1)); + add_row(S, vec(0,1), R(1)); + add_row(S, vec(1,1), R(1)); + feas(S); +} + +static void test2() { + Simplex S; + add_row(S, vec(1, 0), R(1)); + add_row(S, vec(0, 1), R(1)); + add_row(S, vec(1, 1), R(1), true); + feas(S); +} + +static void test3() { + Simplex S; + add_row(S, vec(-1, 0), R(-1)); + add_row(S, vec(0, -1), R(-1)); + add_row(S, vec(1, 1), R(1), true); + feas(S); +} void tst_simplex() { - simplex::sparse_matrix M; Simplex S; std::cout << "simplex\n"; @@ -37,4 +149,8 @@ void tst_simplex() { is_sat = S.make_feasible(); std::cout << "feasible: " << is_sat << "\n"; S.display(std::cout); + + test1(); + test2(); + test3(); } From 480ec049c0f31823fe18e3e42adce8c26f1501c0 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 2 Feb 2014 14:11:35 +0100 Subject: [PATCH 11/12] working on simplex Signed-off-by: Nikolaj Bjorner --- src/math/simplex/simplex.h | 2 ++ src/math/simplex/simplex_def.h | 26 ++++++++++++++++---------- src/test/simplex.cpp | 14 +++++++++++--- 3 files changed, 29 insertions(+), 13 deletions(-) diff --git a/src/math/simplex/simplex.h b/src/math/simplex/simplex.h index bcc76c64f..f7125588e 100644 --- a/src/math/simplex/simplex.h +++ b/src/math/simplex/simplex.h @@ -97,6 +97,7 @@ namespace simplex { unsigned m_blands_rule_threshold; random_gen m_random; uint_set m_left_basis; + unsigned m_infeasible_var; public: simplex(): @@ -112,6 +113,7 @@ namespace simplex { void ensure_var(var_t v); row add_row(var_t base, unsigned num_vars, var_t const* vars, numeral const* coeffs); + row get_infeasible_row(); void del_row(row const& r); void set_lower(var_t var, eps_numeral const& b); void set_upper(var_t var, eps_numeral const& b); diff --git a/src/math/simplex/simplex_def.h b/src/math/simplex/simplex_def.h index 631b89ce7..b08d4d0ff 100644 --- a/src/math/simplex/simplex_def.h +++ b/src/math/simplex/simplex_def.h @@ -24,11 +24,6 @@ namespace simplex { template typename simplex::row simplex::add_row(var_t base, unsigned num_vars, var_t const* vars, numeral const* coeffs) { - DEBUG_CODE( - bool found = false; - for (unsigned i = 0; !found && i < num_vars; ++i) found = vars[i] == base; - SASSERT(found); - ); scoped_numeral base_coeff(m); scoped_eps_numeral value(em), tmp(em); row r = M.mk_row(); @@ -49,7 +44,7 @@ namespace simplex { em.neg(value); em.div(value, base_coeff, value); SASSERT(!m.is_zero(base_coeff)); - SASSERT(!m_vars[base].m_is_base); + SASSERT(!is_base(base)); while (m_row2base.size() <= r.id()) { m_row2base.push_back(null_var); } @@ -63,6 +58,14 @@ namespace simplex { return r; } + template + typename simplex::row + simplex::get_infeasible_row() { + SASSERT(is_base(m_infeasible_var)); + unsigned row_id = m_vars[m_infeasible_var].m_base2row; + return row(row_id); + } + template void simplex::add_patch(var_t v) { SASSERT(is_base(v)); @@ -140,10 +143,10 @@ namespace simplex { if (vi.m_upper_valid) out << em.to_string(vi.m_upper); else out << "oo"; out << "] "; if (vi.m_is_base) out << "b:" << vi.m_base2row << " "; - col_iterator it = M.col_begin(i), end = M.col_end(i); - for (; it != end; ++it) { - out << "r" << it.get_row().id() << " "; - } + //col_iterator it = M.col_begin(i), end = M.col_end(i); + //for (; it != end; ++it) { + // out << "r" << it.get_row().id() << " "; + //} out << "\n"; } } @@ -159,6 +162,7 @@ namespace simplex { template lbool simplex::make_feasible() { m_left_basis.reset(); + m_infeasible_var = null_var; unsigned num_iterations = 0; unsigned num_repeated = 0; var_t v = null_var; @@ -169,6 +173,7 @@ namespace simplex { } check_blands_rule(v, num_repeated); if (!make_var_feasible(v)) { + m_infeasible_var = v; return l_false; } ++num_iterations; @@ -529,6 +534,7 @@ namespace simplex { pivot(x_i, x_j, a_ij); move_to_bound(x_i, inc == m.is_pos(a_ij)); + SASSERT(well_formed_row(row(m_vars[x_j].m_base2row))); } return l_true; } diff --git a/src/test/simplex.cpp b/src/test/simplex.cpp index 986caa30b..37d4501f7 100644 --- a/src/test/simplex.cpp +++ b/src/test/simplex.cpp @@ -78,9 +78,6 @@ void add_row(Simplex& S, vector const& _v, R const& _b, bool is_eq = false) { mpq_inf one(mpq(1),mpq(0)); mpq_inf zero(mpq(0),mpq(0)); SASSERT(vars.size() == coeffs.size()); - std::cout << coeffs.size() << " " << nv << "\n"; - for (unsigned i = 0; i < vars.size(); ++i) std::cout << vars[i] << " "; - std::cout << "\n"; S.set_lower(nv, zero); if (is_eq) S.set_upper(nv, zero); S.set_lower(nv+1, one); @@ -119,6 +116,16 @@ static void test3() { feas(S); } +static void test4() { + Simplex S; + add_row(S, vec(1, 0), R(1)); + add_row(S, vec(0, -1), R(-1)); + add_row(S, vec(1, 1), R(1), true); + feas(S); +} + + + void tst_simplex() { Simplex S; @@ -153,4 +160,5 @@ void tst_simplex() { test1(); test2(); test3(); + test4(); } From f45ad4bdc01835774d6445fc7421b30259f4a3a6 Mon Sep 17 00:00:00 2001 From: Ken McMillan Date: Mon, 10 Feb 2014 12:56:39 -0800 Subject: [PATCH 12/12] disable silly warnings and add needed header for VS --- src/cmd_context/interpolant_cmds.cpp | 2 +- src/duality/duality_profiling.cpp | 6 ++++++ src/duality/duality_rpfp.cpp | 12 ++++++++++-- src/duality/duality_solver.cpp | 7 +++++++ src/duality/duality_wrapper.cpp | 7 +++++++ src/duality/duality_wrapper.h | 1 - src/interp/iz3base.cpp | 6 ++++++ src/interp/iz3checker.cpp | 7 +++++++ src/interp/iz3interp.cpp | 8 ++++++++ src/interp/iz3mgr.cpp | 9 +++++++++ src/interp/iz3mgr.h | 1 + src/interp/iz3profiling.cpp | 7 +++++++ src/interp/iz3proof.cpp | 6 ++++++ src/interp/iz3proof_itp.cpp | 7 +++++++ src/interp/iz3translate.cpp | 7 +++++++ src/interp/iz3translate_direct.cpp | 8 ++++++++ src/muz/duality/duality_dl_interface.cpp | 6 ++++++ 17 files changed, 103 insertions(+), 4 deletions(-) diff --git a/src/cmd_context/interpolant_cmds.cpp b/src/cmd_context/interpolant_cmds.cpp index 318569cd5..7fd44c088 100644 --- a/src/cmd_context/interpolant_cmds.cpp +++ b/src/cmd_context/interpolant_cmds.cpp @@ -114,7 +114,7 @@ static void get_interpolant_and_maybe_check(cmd_context & ctx, expr * t, params_ ptr_vector::const_iterator it = ctx.begin_assertions(); ptr_vector::const_iterator end = ctx.end_assertions(); - ptr_vector cnsts(end - it); + ptr_vector cnsts((unsigned)(end - it)); for (int i = 0; it != end; ++it, ++i) cnsts[i] = *it; diff --git a/src/duality/duality_profiling.cpp b/src/duality/duality_profiling.cpp index 3b392a91a..a4e9e0240 100755 --- a/src/duality/duality_profiling.cpp +++ b/src/duality/duality_profiling.cpp @@ -25,6 +25,12 @@ Revision History: #include #include +#ifdef WIN32 +#pragma warning(disable:4996) +#pragma warning(disable:4800) +#pragma warning(disable:4267) +#endif + #include "duality_wrapper.h" #include "iz3profiling.h" diff --git a/src/duality/duality_rpfp.cpp b/src/duality/duality_rpfp.cpp index 17b93d35b..2d52ab283 100644 --- a/src/duality/duality_rpfp.cpp +++ b/src/duality/duality_rpfp.cpp @@ -21,13 +21,21 @@ Revision History: -#include "duality.h" -#include "duality_profiling.h" +#ifdef WIN32 +#pragma warning(disable:4996) +#pragma warning(disable:4800) +#pragma warning(disable:4267) +#endif + #include #include #include #include + +#include "duality.h" +#include "duality_profiling.h" + #ifndef WIN32 // #define Z3OPS #endif diff --git a/src/duality/duality_solver.cpp b/src/duality/duality_solver.cpp index 91532960b..973ad769c 100644 --- a/src/duality/duality_solver.cpp +++ b/src/duality/duality_solver.cpp @@ -19,6 +19,12 @@ Revision History: --*/ +#ifdef WIN32 +#pragma warning(disable:4996) +#pragma warning(disable:4800) +#pragma warning(disable:4267) +#endif + #include "duality.h" #include "duality_profiling.h" @@ -26,6 +32,7 @@ Revision History: #include #include #include +#include // TODO: make these official options or get rid of them diff --git a/src/duality/duality_wrapper.cpp b/src/duality/duality_wrapper.cpp index 24f6a5e20..cf2c803cb 100644 --- a/src/duality/duality_wrapper.cpp +++ b/src/duality/duality_wrapper.cpp @@ -18,6 +18,13 @@ Revision History: --*/ +#ifdef WIN32 +#pragma warning(disable:4996) +#pragma warning(disable:4800) +#pragma warning(disable:4267) +#pragma warning(disable:4101) +#endif + #include "duality_wrapper.h" #include #include "smt_solver.h" diff --git a/src/duality/duality_wrapper.h b/src/duality/duality_wrapper.h index 94e8d2642..2b0045023 100755 --- a/src/duality/duality_wrapper.h +++ b/src/duality/duality_wrapper.h @@ -1466,6 +1466,5 @@ namespace std { }; } - #endif diff --git a/src/interp/iz3base.cpp b/src/interp/iz3base.cpp index f316c22cf..26146bfa3 100755 --- a/src/interp/iz3base.cpp +++ b/src/interp/iz3base.cpp @@ -18,6 +18,12 @@ Revision History: --*/ +#ifdef WIN32 +#pragma warning(disable:4996) +#pragma warning(disable:4800) +#pragma warning(disable:4267) +#pragma warning(disable:4101) +#endif #include "iz3base.h" #include diff --git a/src/interp/iz3checker.cpp b/src/interp/iz3checker.cpp index b4e55af20..d423ba48f 100755 --- a/src/interp/iz3checker.cpp +++ b/src/interp/iz3checker.cpp @@ -17,6 +17,13 @@ Revision History: --*/ +#ifdef WIN32 +#pragma warning(disable:4996) +#pragma warning(disable:4800) +#pragma warning(disable:4267) +#pragma warning(disable:4101) +#endif + #include "iz3base.h" #include "iz3checker.h" diff --git a/src/interp/iz3interp.cpp b/src/interp/iz3interp.cpp index 56dc1ccec..c204cc35d 100755 --- a/src/interp/iz3interp.cpp +++ b/src/interp/iz3interp.cpp @@ -18,6 +18,14 @@ Revision History: --*/ /* Copyright 2011 Microsoft Research. */ + +#ifdef WIN32 +#pragma warning(disable:4996) +#pragma warning(disable:4800) +#pragma warning(disable:4267) +#pragma warning(disable:4101) +#endif + #include #include #include diff --git a/src/interp/iz3mgr.cpp b/src/interp/iz3mgr.cpp index aa8e8abe3..6664cd2fe 100644 --- a/src/interp/iz3mgr.cpp +++ b/src/interp/iz3mgr.cpp @@ -18,6 +18,15 @@ Revision History: --*/ +#ifdef WIN32 +#pragma warning(disable:4996) +#pragma warning(disable:4800) +#pragma warning(disable:4267) +#pragma warning(disable:4101) +#pragma warning(disable:4805) +#pragma warning(disable:4800) +#endif + #include "iz3mgr.h" #include diff --git a/src/interp/iz3mgr.h b/src/interp/iz3mgr.h index 51a9a8697..e974a199b 100644 --- a/src/interp/iz3mgr.h +++ b/src/interp/iz3mgr.h @@ -263,6 +263,7 @@ class iz3mgr { default:; } assert(0); + return 0; } ast arg(const ast &t, int i){ diff --git a/src/interp/iz3profiling.cpp b/src/interp/iz3profiling.cpp index 262254271..2c4a31d58 100755 --- a/src/interp/iz3profiling.cpp +++ b/src/interp/iz3profiling.cpp @@ -17,6 +17,13 @@ Revision History: --*/ +#ifdef WIN32 +#pragma warning(disable:4996) +#pragma warning(disable:4800) +#pragma warning(disable:4267) +#pragma warning(disable:4101) +#endif + #include "iz3profiling.h" #include diff --git a/src/interp/iz3proof.cpp b/src/interp/iz3proof.cpp index 968a4b25a..3fefea73f 100755 --- a/src/interp/iz3proof.cpp +++ b/src/interp/iz3proof.cpp @@ -18,6 +18,12 @@ Revision History: --*/ +#ifdef WIN32 +#pragma warning(disable:4996) +#pragma warning(disable:4800) +#pragma warning(disable:4267) +#pragma warning(disable:4101) +#endif #include "iz3proof.h" #include "iz3profiling.h" diff --git a/src/interp/iz3proof_itp.cpp b/src/interp/iz3proof_itp.cpp index 8b78a7135..61ed78463 100644 --- a/src/interp/iz3proof_itp.cpp +++ b/src/interp/iz3proof_itp.cpp @@ -17,6 +17,13 @@ Revision History: --*/ +#ifdef WIN32 +#pragma warning(disable:4996) +#pragma warning(disable:4800) +#pragma warning(disable:4267) +#pragma warning(disable:4101) +#endif + #include "iz3proof_itp.h" #ifndef WIN32 diff --git a/src/interp/iz3translate.cpp b/src/interp/iz3translate.cpp index abddb4bda..6a1b665cf 100755 --- a/src/interp/iz3translate.cpp +++ b/src/interp/iz3translate.cpp @@ -17,6 +17,13 @@ Revision History: --*/ +#ifdef WIN32 +#pragma warning(disable:4996) +#pragma warning(disable:4800) +#pragma warning(disable:4267) +#pragma warning(disable:4101) +#endif + #include "iz3translate.h" #include "iz3proof.h" #include "iz3profiling.h" diff --git a/src/interp/iz3translate_direct.cpp b/src/interp/iz3translate_direct.cpp index 0ce3297af..a85c9a1c5 100755 --- a/src/interp/iz3translate_direct.cpp +++ b/src/interp/iz3translate_direct.cpp @@ -20,6 +20,14 @@ Revision History: --*/ +#ifdef WIN32 +#pragma warning(disable:4996) +#pragma warning(disable:4800) +#pragma warning(disable:4267) +#pragma warning(disable:4101) +#pragma warning(disable:4390) +#endif + #include "iz3translate.h" #include "iz3proof.h" #include "iz3profiling.h" diff --git a/src/muz/duality/duality_dl_interface.cpp b/src/muz/duality/duality_dl_interface.cpp index 397d50655..248aca163 100644 --- a/src/muz/duality/duality_dl_interface.cpp +++ b/src/muz/duality/duality_dl_interface.cpp @@ -38,6 +38,12 @@ Revision History: // template class symbol_table; +#ifdef WIN32 +#pragma warning(disable:4996) +#pragma warning(disable:4800) +#pragma warning(disable:4267) +#pragma warning(disable:4101) +#endif #include "duality.h" #include "duality_profiling.h"