diff --git a/scripts/mk_project.py b/scripts/mk_project.py index 6e352f06f..f2c688525 100644 --- a/scripts/mk_project.py +++ b/scripts/mk_project.py @@ -55,8 +55,8 @@ def init_project_def(): add_lib('fpa', ['core_tactics', 'bv_tactics', 'sat_tactic'], 'tactic/fpa') add_lib('smt_tactic', ['smt'], 'smt/tactic') add_lib('sls_tactic', ['tactic', 'normal_forms', 'core_tactics', 'bv_tactics'], 'tactic/sls') - add_lib('duality', ['smt', 'interp']) add_lib('qe', ['smt','sat'], 'qe') + add_lib('duality', ['smt', 'interp', 'qe']) add_lib('muz', ['smt', 'sat', 'smt2parser', 'aig_tactic', 'qe'], 'muz/base') add_lib('transforms', ['muz', 'hilbert'], 'muz/transforms') add_lib('rel', ['muz', 'transforms'], 'muz/rel') diff --git a/src/api/api_interp.cpp b/src/api/api_interp.cpp index 00503566e..560ee5885 100644 --- a/src/api/api_interp.cpp +++ b/src/api/api_interp.cpp @@ -42,6 +42,20 @@ Revision History: using namespace stl_ext; #endif +#ifndef WIN32 +// WARNING: don't make a hash_map with this if the range type +// has a destructor: you'll get an address dependency!!! +namespace stl_ext { + template <> + class hash { + public: + size_t operator()(const Z3_ast p) const { + return (size_t) p; + } + }; +} +#endif + typedef interpolation_options_struct *Z3_interpolation_options; extern "C" { @@ -305,8 +319,8 @@ static void get_file_params(const char *filename, hash_map= 0 && eqpos < (int)tok.size()){ + size_t eqpos = tok.find('='); + if(eqpos >= 0 && eqpos < tok.size()){ std::string left = tok.substr(0,eqpos); std::string right = tok.substr(eqpos+1,tok.size()-eqpos-1); params[left] = right; @@ -363,8 +377,8 @@ extern "C" { #else - static Z3_ast and_vec(Z3_context ctx,std::vector &c){ - return (c.size() > 1) ? Z3_mk_and(ctx,c.size(),&c[0]) : c[0]; + static Z3_ast and_vec(Z3_context ctx,svector &c){ + return (c.size() > 1) ? Z3_mk_and(ctx,c.size(),&c[0]) : c[0]; } static Z3_ast parents_vector_to_tree(Z3_context ctx, int num, Z3_ast *cnsts, int *parents){ @@ -381,15 +395,15 @@ extern "C" { } } else { - std::vector > chs(num); + std::vector > chs(num); for(int i = 0; i < num-1; i++){ - std::vector &c = chs[i]; + svector &c = chs[i]; c.push_back(cnsts[i]); Z3_ast foo = Z3_mk_interp(ctx,and_vec(ctx,c)); chs[parents[i]].push_back(foo); } { - std::vector &c = chs[num-1]; + svector &c = chs[num-1]; c.push_back(cnsts[num-1]); res = and_vec(ctx,c); } @@ -454,7 +468,7 @@ extern "C" { static std::string read_msg; static std::vector read_theory; - static bool iZ3_parse(Z3_context ctx, const char *filename, const char **error, std::vector &assertions){ + static bool iZ3_parse(Z3_context ctx, const char *filename, const char **error, svector &assertions){ read_error.clear(); try { std::string foo(filename); @@ -496,26 +510,26 @@ extern "C" { hash_map file_params; get_file_params(filename,file_params); - - int num_theory = 0; + + unsigned num_theory = 0; if(file_params.find("THEORY") != file_params.end()) num_theory = atoi(file_params["THEORY"].c_str()); - std::vector assertions; + svector assertions; if(!iZ3_parse(ctx,filename,error,assertions)) return false; - if(num_theory > (int)assertions.size()) - num_theory = assertions.size(); - int num = assertions.size() - num_theory; + if(num_theory > assertions.size()) + num_theory = assertions.size(); + unsigned num = assertions.size() - num_theory; read_cnsts.resize(num); read_parents.resize(num); read_theory.resize(num_theory); - for(int j = 0; j < num_theory; j++) + for(unsigned j = 0; j < num_theory; j++) read_theory[j] = assertions[j]; - for(int j = 0; j < num; j++) + for(unsigned j = 0; j < num; j++) read_cnsts[j] = assertions[j+num_theory]; if(ret_num_theory) @@ -529,12 +543,12 @@ extern "C" { return true; } - for(int j = 0; j < num; j++) + for(unsigned j = 0; j < num; j++) read_parents[j] = SHRT_MAX; hash_map pred_map; - for(int j = 0; j < num; j++){ + for(unsigned j = 0; j < num; j++){ Z3_ast lhs = 0, rhs = read_cnsts[j]; if(Z3_get_decl_kind(ctx,Z3_get_app_decl(ctx,Z3_to_app(ctx,rhs))) == Z3_OP_IMPLIES){ @@ -588,7 +602,7 @@ extern "C" { } } - for(int j = 0; j < num-1; j++) + for(unsigned j = 0; j < num-1; j++) if(read_parents[j] == SHRT_MIN){ read_error << "formula " << j+1 << ": unreferenced"; goto fail; diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp index bdf1c18db..b000201b7 100644 --- a/src/ast/ast.cpp +++ b/src/ast/ast.cpp @@ -3161,3 +3161,6 @@ void prexpr(expr_ref &e){ std::cout << mk_pp(e.get(), e.get_manager()) << std::endl; } +void ast_manager::show_id_gen(){ + std::cout << "id_gen: " << m_expr_id_gen.show_hash() << " " << m_decl_id_gen.show_hash() << "\n"; +} diff --git a/src/ast/ast.h b/src/ast/ast.h index 2c3843587..68f08e1ac 100644 --- a/src/ast/ast.h +++ b/src/ast/ast.h @@ -1418,6 +1418,8 @@ protected: public: typedef expr_dependency_array_manager::ref expr_dependency_array; + void show_id_gen(); + protected: small_object_allocator m_alloc; family_manager m_family_manager; diff --git a/src/ast/proof_checker/proof_checker.cpp b/src/ast/proof_checker/proof_checker.cpp index 85e0cc791..41c43b26c 100644 --- a/src/ast/proof_checker/proof_checker.cpp +++ b/src/ast/proof_checker/proof_checker.cpp @@ -479,7 +479,7 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) { // otherwise t2 is also a quantifier. return true; } - UNREACHABLE(); + IF_VERBOSE(0, verbose_stream() << "does not match last rule: " << mk_pp(p, m) << "\n";); return false; } case PR_DER: { @@ -488,13 +488,12 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) { match_fact(p, fact) && match_iff(fact.get(), t1, t2) && match_quantifier(t1, is_forall, decls1, body1) && - is_forall && - match_or(body1.get(), terms1)) { + is_forall) { // TBD: check that terms are set of equalities. // t2 is an instance of a predicate in terms1 return true; - } - UNREACHABLE(); + } + IF_VERBOSE(0, verbose_stream() << "does not match last rule: " << mk_pp(p, m) << "\n";); return false; } case PR_HYPOTHESIS: { @@ -832,7 +831,7 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) { } else { IF_VERBOSE(0, verbose_stream() << "Could not establish complementarity for:\n" << - mk_pp(lit1, m) << "\n" << mk_pp(lit2, m) << "\n";); + mk_pp(lit1, m) << "\n" << mk_pp(lit2, m) << "\n" << mk_pp(p, m) << "\n";); } fmls[i] = premise1; } diff --git a/src/duality/duality.h b/src/duality/duality.h index 166e8ef0d..979071639 100644 --- a/src/duality/duality.h +++ b/src/duality/duality.h @@ -79,9 +79,36 @@ namespace Duality { int CumulativeDecisions(); - private: + int CountOperators(const Term &t); + + Term SubstAtom(hash_map &memo, const expr &t, const expr &atom, const expr &val); + + Term RemoveRedundancy(const Term &t); + + bool IsLiteral(const expr &lit, expr &atom, expr &val); + + expr Negate(const expr &f); + + expr SimplifyAndOr(const std::vector &args, bool is_and); + + expr ReallySimplifyAndOr(const std::vector &args, bool is_and); + + int MaxIndex(hash_map &memo, const Term &t); + + bool IsClosedFormula(const Term &t); + + Term AdjustQuantifiers(const Term &t); +private: void SummarizeRec(hash_set &memo, std::vector &lits, int &ops, const Term &t); + int CountOperatorsRec(hash_set &memo, const Term &t); + void RemoveRedundancyOp(bool pol, std::vector &args, hash_map &smemo); + Term RemoveRedundancyRec(hash_map &memo, hash_map &smemo, const Term &t); + Term SubstAtomTriv(const expr &foo, const expr &atom, const expr &val); + 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); + }; @@ -142,6 +169,7 @@ namespace Duality { context *ctx; /** Z3 context for formulas */ solver *slvr; /** Z3 solver */ bool need_goals; /** Can the solver use the goal tree to optimize interpolants? */ + solver aux_solver; /** For temporary use -- don't leave assertions here. */ /** Tree interpolation. This method assumes the formulas in TermTree "assumptions" are currently asserted in the solver. The return @@ -167,6 +195,9 @@ namespace Duality { /** Assert a background axiom. */ virtual void assert_axiom(const expr &axiom) = 0; + /** Get the background axioms. */ + virtual const std::vector &get_axioms() = 0; + /** Return a string describing performance. */ virtual std::string profile() = 0; @@ -178,6 +209,12 @@ namespace Duality { /** Cancel, throw Canceled object if possible. */ virtual void cancel(){ } + /* Note: aux solver uses extensional array theory, since it + needs to be able to produce counter-models for + interpolants the have array equalities in them. + */ + LogicSolver(context &c) : aux_solver(c,true){} + virtual ~LogicSolver(){} }; @@ -202,6 +239,10 @@ namespace Duality { islvr->AssertInterpolationAxiom(axiom); } + const std::vector &get_axioms() { + return islvr->GetInterpolationAxioms(); + } + std::string profile(){ return islvr->profile(); } @@ -215,7 +256,7 @@ namespace Duality { } #endif - iZ3LogicSolver(context &c){ + iZ3LogicSolver(context &c) : LogicSolver(c) { ctx = ictx = &c; slvr = islvr = new interpolating_solver(*ictx); need_goals = false; @@ -277,6 +318,7 @@ namespace Duality { public: std::list edges; std::list nodes; + std::list > constraints; }; @@ -286,7 +328,9 @@ namespace Duality { literals dualLabels; std::list stack; std::vector axioms; // only saved here for printing purposes - + solver &aux_solver; + hash_set *proof_core; + public: /** Construct an RPFP graph with a given interpolating prover context. It is allowed to @@ -296,13 +340,14 @@ namespace Duality { inherit the axioms. */ - RPFP(LogicSolver *_ls) : Z3User(*(_ls->ctx), *(_ls->slvr)), dualModel(*(_ls->ctx)) + RPFP(LogicSolver *_ls) : Z3User(*(_ls->ctx), *(_ls->slvr)), dualModel(*(_ls->ctx)), aux_solver(_ls->aux_solver) { ls = _ls; nodeCount = 0; edgeCount = 0; stack.push_back(stack_entry()); HornClauses = false; + proof_core = 0; } ~RPFP(); @@ -351,10 +396,10 @@ namespace Duality { bool SubsetEq(const Transformer &other){ Term t = owner->SubstParams(other.IndParams,IndParams,other.Formula); expr test = Formula && !t; - owner->slvr.push(); - owner->slvr.add(test); - check_result res = owner->slvr.check(); - owner->slvr.pop(1); + owner->aux_solver.push(); + owner->aux_solver.add(test); + check_result res = owner->aux_solver.check(); + owner->aux_solver.pop(1); return res == unsat; } @@ -444,6 +489,19 @@ namespace Duality { return n; } + /** Delete a node. You can only do this if not connected to any edges.*/ + void DeleteNode(Node *node){ + if(node->Outgoing || !node->Incoming.empty()) + throw "cannot delete RPFP node"; + for(std::vector::iterator it = nodes.end(), en = nodes.begin(); it != en;){ + if(*(--it) == node){ + nodes.erase(it); + break; + } + } + delete node; + } + /** This class represents a hyper-edge in the RPFP graph */ class Edge @@ -460,6 +518,7 @@ namespace Duality { hash_map varMap; Edge *map; Term labeled; + std::vector constraints; Edge(Node *_Parent, const Transformer &_F, const std::vector &_Children, RPFP *_owner, int _number) : F(_F), Parent(_Parent), Children(_Children), dual(expr(_owner->ctx)) { @@ -480,6 +539,29 @@ namespace Duality { return e; } + + /** Delete a hyper-edge and unlink it from any nodes. */ + void DeleteEdge(Edge *edge){ + if(edge->Parent) + edge->Parent->Outgoing = 0; + for(unsigned int i = 0; i < edge->Children.size(); i++){ + std::vector &ic = edge->Children[i]->Incoming; + for(std::vector::iterator it = ic.begin(), en = ic.end(); it != en; ++it){ + if(*it == edge){ + ic.erase(it); + break; + } + } + } + for(std::vector::iterator it = edges.end(), en = edges.begin(); it != en;){ + if(*(--it) == edge){ + edges.erase(it); + break; + } + } + delete edge; + } + /** Create an edge that lower-bounds its parent. */ Edge *CreateLowerBoundEdge(Node *_Parent) { @@ -494,13 +576,26 @@ namespace Duality { void AssertEdge(Edge *e, int persist = 0, bool with_children = false, bool underapprox = false); - + /* Constrain an edge by the annotation of one of its children. */ + + void ConstrainParent(Edge *parent, Node *child); + /** For incremental solving, asserts the negation of the upper bound associated * with a node. * */ void AssertNode(Node *n); + /** Assert a constraint on an edge in the SMT context. + */ + void ConstrainEdge(Edge *e, const Term &t); + + /** Fix the truth values of atomic propositions in the given + edge to their values in the current assignment. */ + void FixCurrentState(Edge *root); + + void FixCurrentStateFull(Edge *edge, const expr &extra); + /** Declare a constant in the background theory. */ void DeclareConstant(const FuncDecl &f); @@ -554,9 +649,13 @@ namespace Duality { lbool Solve(Node *root, int persist); + /** Same as Solve, but annotates only a single node. */ + + lbool SolveSingleNode(Node *root, Node *node); + /** Get the constraint tree (but don't solve it) */ - TermTree *GetConstraintTree(Node *root); + TermTree *GetConstraintTree(Node *root, Node *skip_descendant = 0); /** Dispose of the dual model (counterexample) if there is one. */ @@ -592,6 +691,13 @@ namespace Duality { Term ComputeUnderapprox(Node *root, int persist); + /** Try to strengthen the annotation of a node by removing disjuncts. */ + void Generalize(Node *root, Node *node); + + + /** Compute disjunctive interpolant for node by case splitting */ + void InterpolateByCases(Node *root, Node *node); + /** Push a scope. Assertions made after Push can be undone by Pop. */ void Push(); @@ -623,6 +729,16 @@ namespace Duality { /** Pop a scope (see Push). Note, you cannot pop axioms. */ void Pop(int num_scopes); + + /** Erase the proof by performing a Pop, Push and re-assertion of + all the popped constraints */ + void PopPush(); + + /** Return true if the given edge is used in the proof of unsat. + Can be called only after Solve or Check returns an unsat result. */ + + bool EdgeUsedInProof(Edge *edge); + /** Convert a collection of clauses to Nodes and Edges in the RPFP. @@ -707,8 +823,19 @@ namespace Duality { // int GetLabelsRec(hash_map *memo, const Term &f, std::vector &labels, bool labpos); + /** Compute and save the proof core for future calls to + EdgeUsedInProof. You only need to call this if you will pop + the solver before calling EdgeUsedInProof. + */ + void ComputeProofCore(); + private: + void ClearProofCore(){ + if(proof_core) + delete proof_core; + proof_core = 0; + } Term SuffixVariable(const Term &t, int n); @@ -724,10 +851,14 @@ namespace Duality { Term ReducedDualEdge(Edge *e); - TermTree *ToTermTree(Node *root); + TermTree *ToTermTree(Node *root, Node *skip_descendant = 0); TermTree *ToGoalTree(Node *root); + void CollapseTermTreeRec(TermTree *root, TermTree *node); + + TermTree *CollapseTermTree(TermTree *node); + void DecodeTree(Node *root, TermTree *interp, int persist); Term GetUpperBound(Node *n); @@ -777,6 +908,11 @@ namespace Duality { Term UnderapproxFormula(const Term &f, hash_set &dont_cares); + void ImplicantFullRed(hash_map &memo, const Term &f, std::vector &lits, + hash_set &done, hash_set &dont_cares); + + Term UnderapproxFullFormula(const Term &f, hash_set &dont_cares); + Term ToRuleRec(Edge *e, hash_map &memo, const Term &t, std::vector &quants); hash_map resolve_ite_memo; @@ -803,6 +939,25 @@ namespace Duality { Term SubstBound(hash_map &subst, const Term &t); + void ConstrainEdgeLocalized(Edge *e, const Term &t); + + void GreedyReduce(solver &s, std::vector &conjuncts); + + void NegateLits(std::vector &lits); + + expr SimplifyOr(std::vector &lits); + + void SetAnnotation(Node *root, const expr &t); + + void AddEdgeToSolver(Edge *edge); + + void AddToProofCore(hash_set &core); + + void GetGroundLitsUnderQuants(hash_set *memo, const Term &f, std::vector &res, int under); + + Term StrengthenFormulaByCaseSplitting(const Term &f, std::vector &case_lits); + + expr NegateLit(const expr &f); }; @@ -852,3 +1007,38 @@ namespace Duality { }; } + + +// Allow to hash on nodes and edges in deterministic way + +namespace hash_space { + template <> + class hash { + public: + size_t operator()(const Duality::RPFP::Node *p) const { + return p->number; + } + }; +} + +namespace hash_space { + template <> + class hash { + public: + size_t operator()(const Duality::RPFP::Edge *p) const { + return p->number; + } + }; +} + +// allow to walk sets of nodes without address dependency + +namespace std { + template <> + class less { + public: + bool operator()(Duality::RPFP::Node * const &s, Duality::RPFP::Node * const &t) const { + return s->number < t->number; // s.raw()->get_id() < t.raw()->get_id(); + } + }; +} diff --git a/src/duality/duality_rpfp.cpp b/src/duality/duality_rpfp.cpp index 1c2927da8..a5e2b9167 100644 --- a/src/duality/duality_rpfp.cpp +++ b/src/duality/duality_rpfp.cpp @@ -25,6 +25,8 @@ Revision History: #include "duality_profiling.h" #include #include +#include +#include #ifndef WIN32 // #define Z3OPS @@ -89,15 +91,17 @@ namespace Duality { if(memo.find(t) != memo.end()) return; memo.insert(t); - decl_kind k = t.decl().get_decl_kind(); - if(k == And || k == Or || k == Not || k == Implies || k == Iff){ - ops++; - int nargs = t.num_args(); - for(int i = 0; i < nargs; i++) - SummarizeRec(memo,lits,ops,t.arg(i)); + if(t.is_app()){ + decl_kind k = t.decl().get_decl_kind(); + if(k == And || k == Or || k == Not || k == Implies || k == Iff){ + ops++; + int nargs = t.num_args(); + for(int i = 0; i < nargs; i++) + SummarizeRec(memo,lits,ops,t.arg(i)); + return; + } } - else - lits.push_back(t); + lits.push_back(t); } int Z3User::CumulativeDecisions(){ @@ -123,6 +127,32 @@ namespace Duality { } } + int Z3User::CountOperatorsRec(hash_set &memo, const Term &t){ + if(memo.find(t) != memo.end()) + return 0; + memo.insert(t); + if(t.is_app()){ + decl_kind k = t.decl().get_decl_kind(); + if(k == And || k == Or){ + int count = 1; + int nargs = t.num_args(); + for(int i = 0; i < nargs; i++) + count += CountOperatorsRec(memo,t.arg(i)); + return count; + } + return 0; + } + if(t.is_quantifier()) + return CountOperatorsRec(memo,t.body())+2; // count 2 for a quantifier + return 0; + } + + int Z3User::CountOperators(const Term &t){ + hash_set memo; + return CountOperatorsRec(memo,t); + } + + Z3User::Term Z3User::conjoin(const std::vector &args){ return ctx.make(And,args); } @@ -183,6 +213,7 @@ namespace Duality { return clone_quantifier(t,new_body); } + RPFP::Term RPFP::LocalizeRec(Edge *e, hash_map &memo, const Term &t) { std::pair foo(t,expr(ctx)); @@ -272,16 +303,21 @@ namespace Duality { return implies(b, Localize(e, e->F.Formula)); } - TermTree *RPFP::ToTermTree(Node *root) + TermTree *RPFP::ToTermTree(Node *root, Node *skip_descendant) { + if(skip_descendant && root == skip_descendant) + return new TermTree(ctx.bool_val(true)); Edge *e = root->Outgoing; if(!e) return new TermTree(ctx.bool_val(true), std::vector()); std::vector children(e->Children.size()); for(unsigned i = 0; i < children.size(); i++) - children[i] = ToTermTree(e->Children[i]); + children[i] = ToTermTree(e->Children[i],skip_descendant); // Term top = ReducedDualEdge(e); Term top = e->dual.null() ? ctx.bool_val(true) : e->dual; - return new TermTree(top, children); + TermTree *res = new TermTree(top, children); + for(unsigned i = 0; i < e->constraints.size(); i++) + res->addTerm(e->constraints[i]); + return res; } TermTree *RPFP::GetGoalTree(Node *root){ @@ -321,11 +357,229 @@ namespace Duality { res = f(args.size(),&args[0]); } else if (t.is_quantifier()) - res = CloneQuantifier(t,SubstRec(memo, t.body())); + { + std::vector pats; + t.get_patterns(pats); + for(unsigned i = 0; i < pats.size(); i++) + pats[i] = SubstRec(memo,pats[i]); + Term body = SubstRec(memo,t.body()); + res = clone_quantifier(t, body, pats); + } + // res = CloneQuantifier(t,SubstRec(memo, t.body())); else res = t; return res; } + bool Z3User::IsLiteral(const expr &lit, expr &atom, expr &val){ + if(!(lit.is_quantifier() && IsClosedFormula(lit))){ + if(!lit.is_app()) + return false; + decl_kind k = lit.decl().get_decl_kind(); + if(k == Not){ + if(IsLiteral(lit.arg(0),atom,val)){ + val = eq(val,ctx.bool_val(true)) ? ctx.bool_val(false) : ctx.bool_val(true); + return true; + } + return false; + } + if(k == And || k == Or || k == Iff || k == Implies) + return false; + } + atom = lit; + val = ctx.bool_val(true); + return true; + } + + expr Z3User::Negate(const expr &f){ + if(f.is_app() && f.decl().get_decl_kind() == Not) + return f.arg(0); + else if(eq(f,ctx.bool_val(true))) + return ctx.bool_val(false); + else if(eq(f,ctx.bool_val(false))) + return ctx.bool_val(true); + return !f; + } + + expr Z3User::ReduceAndOr(const std::vector &args, bool is_and, std::vector &res){ + for(unsigned i = 0; i < args.size(); i++) + if(!eq(args[i],ctx.bool_val(is_and))){ + if(eq(args[i],ctx.bool_val(!is_and))) + return ctx.bool_val(!is_and); + res.push_back(args[i]); + } + return expr(); + } + + expr Z3User::FinishAndOr(const std::vector &args, bool is_and){ + if(args.size() == 0) + return ctx.bool_val(is_and); + if(args.size() == 1) + return args[0]; + return ctx.make(is_and ? And : Or,args); + } + + expr Z3User::SimplifyAndOr(const std::vector &args, bool is_and){ + std::vector sargs; + expr res = ReduceAndOr(args,is_and,sargs); + if(!res.null()) return res; + return FinishAndOr(sargs,is_and); + } + + expr Z3User::PullCommonFactors(std::vector &args, bool is_and){ + + // first check if there's anything to do... + if(args.size() < 2) + return FinishAndOr(args,is_and); + for(unsigned i = 0; i < args.size(); i++){ + const expr &a = args[i]; + if(!(a.is_app() && a.decl().get_decl_kind() == (is_and ? Or : And))) + return FinishAndOr(args,is_and); + } + std::vector common; + for(unsigned i = 0; i < args.size(); i++){ + unsigned n = args[i].num_args(); + std::vector v(n),w; + for(unsigned j = 0; j < n; j++) + v[j] = args[i].arg(j); + std::less comp; + std::sort(v.begin(),v.end(),comp); + if(i == 0) + common.swap(v); + else { + std::set_intersection(common.begin(),common.end(),v.begin(),v.end(),std::inserter(w,w.begin()),comp); + common.swap(w); + } + } + if(common.empty()) + return FinishAndOr(args,is_and); + std::set common_set(common.begin(),common.end()); + for(unsigned i = 0; i < args.size(); i++){ + unsigned n = args[i].num_args(); + std::vector lits; + for(unsigned j = 0; j < n; j++){ + const expr b = args[i].arg(j); + if(common_set.find(b) == common_set.end()) + lits.push_back(b); + } + args[i] = SimplifyAndOr(lits,!is_and); + } + common.push_back(SimplifyAndOr(args,is_and)); + return SimplifyAndOr(common,!is_and); + } + + expr Z3User::ReallySimplifyAndOr(const std::vector &args, bool is_and){ + std::vector sargs; + expr res = ReduceAndOr(args,is_and,sargs); + if(!res.null()) return res; + return PullCommonFactors(sargs,is_and); + } + + Z3User::Term Z3User::SubstAtomTriv(const expr &foo, const expr &atom, const expr &val){ + if(eq(foo,atom)) + return val; + else if(foo.is_app() && foo.decl().get_decl_kind() == Not && eq(foo.arg(0),atom)) + return Negate(val); + else + return foo; + } + + Z3User::Term Z3User::SubstAtom(hash_map &memo, const expr &t, const expr &atom, const expr &val){ + std::pair foo(t,expr(ctx)); + std::pair::iterator, bool> bar = memo.insert(foo); + Term &res = bar.first->second; + if(!bar.second) return res; + if (t.is_app()){ + func_decl f = t.decl(); + decl_kind k = f.get_decl_kind(); + + // TODO: recur here, but how much? We don't want to be quadractic in formula size + + if(k == And || k == Or){ + int nargs = t.num_args(); + std::vector args(nargs); + for(int i = 0; i < nargs; i++) + args[i] = SubstAtom(memo,t.arg(i),atom,val); + res = ReallySimplifyAndOr(args, k==And); + return res; + } + } + else if(t.is_quantifier() && atom.is_quantifier()){ + if(eq(t,atom)) + res = val; + else + res = clone_quantifier(t,SubstAtom(memo,t.body(),atom,val)); + return res; + } + res = SubstAtomTriv(t,atom,val); + return res; + } + + void Z3User::RemoveRedundancyOp(bool pol, std::vector &args, hash_map &smemo){ + for(unsigned i = 0; i < args.size(); i++){ + const expr &lit = args[i]; + expr atom, val; + if(IsLiteral(lit,atom,val)){ + for(unsigned j = 0; j < args.size(); j++) + if(j != i){ + smemo.clear(); + args[j] = SubstAtom(smemo,args[j],atom,pol ? val : !val); + } + } + } + } + + + Z3User::Term Z3User::RemoveRedundancyRec(hash_map &memo, hash_map &smemo, const Term &t) + { + std::pair foo(t,expr(ctx)); + std::pair::iterator, bool> bar = memo.insert(foo); + Term &res = bar.first->second; + if(!bar.second) return res; + if (t.is_app()) + { + func_decl f = t.decl(); + std::vector args; + int nargs = t.num_args(); + for(int i = 0; i < nargs; i++) + args.push_back(RemoveRedundancyRec(memo, smemo, t.arg(i))); + + decl_kind k = f.get_decl_kind(); + if(k == And){ + RemoveRedundancyOp(true,args,smemo); + res = ReallySimplifyAndOr(args, true); + } + else if(k == Or){ + RemoveRedundancyOp(false,args,smemo); + res = ReallySimplifyAndOr(args, false); + } + else { + if(k == Equal && args[0].get_id() > args[1].get_id()) + std::swap(args[0],args[1]); + res = f(args.size(),&args[0]); + } + } + else if (t.is_quantifier()) + { + Term body = RemoveRedundancyRec(memo,smemo,t.body()); + res = clone_quantifier(t, body); + } + else res = t; + return res; + } + + Z3User::Term Z3User::RemoveRedundancy(const Term &t){ + hash_map memo; + hash_map smemo; + return RemoveRedundancyRec(memo,smemo,t); + } + + Z3User::Term Z3User::AdjustQuantifiers(const Term &t) + { + if(t.is_quantifier() || (t.is_app() && t.has_quantifiers())) + return t.qe_lite(); + return t; + } + Z3User::Term Z3User::SubstRecHide(hash_map &memo, const Term &t, int number) { std::pair foo(t,expr(ctx)); @@ -373,6 +627,19 @@ namespace Duality { x = x && y; } + void RPFP::SetAnnotation(Node *root, const expr &t){ + hash_map memo; + Term b; + std::vector v; + RedVars(root, b, v); + memo[b] = ctx.bool_val(true); + for (unsigned i = 0; i < v.size(); i++) + memo[v[i]] = root->Annotation.IndParams[i]; + Term annot = SubstRec(memo, t); + // Strengthen(ref root.Annotation.Formula, annot); + root->Annotation.Formula = annot; + } + void RPFP::DecodeTree(Node *root, TermTree *interp, int persist) { std::vector &ic = interp->getChildren(); @@ -382,16 +649,7 @@ namespace Duality { for (unsigned i = 0; i < nc.size(); i++) DecodeTree(nc[i], ic[i], persist); } - hash_map memo; - Term b; - std::vector v; - RedVars(root, b, v); - memo[b] = ctx.bool_val(true); - for (unsigned i = 0; i < v.size(); i++) - memo[v[i]] = root->Annotation.IndParams[i]; - Term annot = SubstRec(memo, interp->getTerm()); - // Strengthen(ref root.Annotation.Formula, annot); - root->Annotation.Formula = annot; + SetAnnotation(root,interp->getTerm()); #if 0 if(persist != 0) Z3_persist_ast(ctx,root->Annotation.Formula,persist); @@ -509,6 +767,10 @@ namespace Duality { timer_stop("solver add"); } + void RPFP::ConstrainParent(Edge *parent, Node *child){ + ConstrainEdgeLocalized(parent,GetAnnotation(child)); + } + /** For incremental solving, asserts the negation of the upper bound associated * with a node. @@ -524,6 +786,24 @@ namespace Duality { } } + /** Assert a constraint on an edge in the SMT context. + */ + + void RPFP::ConstrainEdge(Edge *e, const Term &t) + { + Term tl = Localize(e, t); + ConstrainEdgeLocalized(e,tl); + } + + void RPFP::ConstrainEdgeLocalized(Edge *e, const Term &tl) + { + e->constraints.push_back(tl); + stack.back().constraints.push_back(std::pair(e,tl)); + slvr.add(tl); + } + + + /** Declare a constant in the background theory. */ void RPFP::DeclareConstant(const FuncDecl &f){ @@ -592,6 +872,7 @@ namespace Duality { TermTree *goals = NULL; if(ls->need_goals) goals = GetGoalTree(root); + ClearProofCore(); // if (dualModel != null) dualModel.Dispose(); // if (dualLabels != null) dualLabels.Dispose(); @@ -613,11 +894,54 @@ namespace Duality { return res; } + void RPFP::CollapseTermTreeRec(TermTree *root, TermTree *node){ + root->addTerm(node->getTerm()); + std::vector &cnsts = node->getTerms(); + for(unsigned i = 0; i < cnsts.size(); i++) + root->addTerm(cnsts[i]); + std::vector &chs = node->getChildren(); + for(unsigned i = 0; i < chs.size(); i++){ + CollapseTermTreeRec(root,chs[i]); + } + } + + TermTree *RPFP::CollapseTermTree(TermTree *node){ + std::vector &chs = node->getChildren(); + for(unsigned i = 0; i < chs.size(); i++) + CollapseTermTreeRec(node,chs[i]); + for(unsigned i = 0; i < chs.size(); i++) + delete chs[i]; + chs.clear(); + return node; + } + + lbool RPFP::SolveSingleNode(Node *root, Node *node) + { + timer_start("Solve"); + TermTree *tree = CollapseTermTree(GetConstraintTree(root,node)); + tree->getChildren().push_back(CollapseTermTree(ToTermTree(node))); + TermTree *interpolant = NULL; + ClearProofCore(); + + timer_start("interpolate_tree"); + lbool res = ls->interpolate_tree(tree, interpolant, dualModel,0,true); + timer_stop("interpolate_tree"); + if (res == l_false) + { + DecodeTree(node, interpolant->getChildren()[0], 0); + delete interpolant; + } + + delete tree; + timer_stop("Solve"); + return res; + } + /** Get the constraint tree (but don't solve it) */ - TermTree *RPFP::GetConstraintTree(Node *root) + TermTree *RPFP::GetConstraintTree(Node *root, Node *skip_descendant) { - return AddUpperBound(root, ToTermTree(root)); + return AddUpperBound(root, ToTermTree(root,skip_descendant)); } /** Dispose of the dual model (counterexample) if there is one. */ @@ -646,6 +970,7 @@ namespace Duality { check_result RPFP::Check(Node *root, std::vector underapproxes, std::vector *underapprox_core ) { + ClearProofCore(); // if (dualModel != null) dualModel.Dispose(); check_result res; if(!underapproxes.size()) @@ -682,6 +1007,7 @@ namespace Duality { check_result RPFP::CheckUpdateModel(Node *root, std::vector assumps){ // check_result temp1 = slvr.check(); // no idea why I need to do this + ClearProofCore(); check_result res = slvr.check_keep_model(assumps.size(),&assumps[0]); dualModel = slvr.get_model(); return res; @@ -1062,7 +1388,8 @@ namespace Duality { } } /* Unreachable! */ - throw "error in RPFP::ImplicantRed"; + // TODO: need to indicate this failure to caller + // std::cerr << "error in RPFP::ImplicantRed"; goto done; } else if(k == Not) { @@ -1081,6 +1408,31 @@ namespace Duality { done[truth].insert(f); } + void RPFP::ImplicantFullRed(hash_map &memo, const Term &f, std::vector &lits, + hash_set &done, hash_set &dont_cares){ + if(done.find(f) != done.end()) + return; /* already processed */ + if(f.is_app()){ + int nargs = f.num_args(); + decl_kind k = f.decl().get_decl_kind(); + if(k == Implies || k == Iff || k == And || k == Or || k == Not){ + for(int i = 0; i < nargs; i++) + ImplicantFullRed(memo,f.arg(i),lits,done,dont_cares); + goto done; + } + } + { + if(dont_cares.find(f) == dont_cares.end()){ + int b = SubtermTruth(memo,f); + if(b != 0 && b != 1) goto done; + expr bv = (b==1) ? f : !f; + lits.push_back(bv); + } + } + done: + done.insert(f); + } + RPFP::Term RPFP::ResolveIte(hash_map &memo, const Term &t, std::vector &lits, hash_set *done, hash_set &dont_cares){ if(resolve_ite_memo.find(t) != resolve_ite_memo.end()) @@ -1143,6 +1495,16 @@ namespace Duality { return conjoin(lits); } + RPFP::Term RPFP::UnderapproxFullFormula(const Term &f, hash_set &dont_cares){ + /* first compute truth values of subterms */ + hash_map memo; + hash_set done; + std::vector lits; + ImplicantFullRed(memo,f,lits,done,dont_cares); + /* return conjunction of literals */ + return conjoin(lits); + } + struct VariableProjector : Z3User { struct elim_cand { @@ -1669,6 +2031,121 @@ namespace Duality { return eu; } + void RPFP::FixCurrentState(Edge *edge){ + hash_set dont_cares; + resolve_ite_memo.clear(); + timer_start("UnderapproxFormula"); + Term dual = edge->dual.null() ? ctx.bool_val(true) : edge->dual; + Term eu = UnderapproxFormula(dual,dont_cares); + timer_stop("UnderapproxFormula"); + ConstrainEdgeLocalized(edge,eu); + } + + void RPFP::FixCurrentStateFull(Edge *edge, const expr &extra){ + hash_set dont_cares; + resolve_ite_memo.clear(); + timer_start("UnderapproxFormula"); + Term dual = edge->dual.null() ? ctx.bool_val(true) : edge->dual; + for(unsigned i = 0; i < edge->constraints.size(); i++) + dual = dual && edge->constraints[i]; + // dual = dual && extra; + Term eu = UnderapproxFullFormula(dual,dont_cares); + timer_stop("UnderapproxFormula"); + ConstrainEdgeLocalized(edge,eu); + } + + + + + void RPFP::GetGroundLitsUnderQuants(hash_set *memo, const Term &f, std::vector &res, int under){ + if(memo[under].find(f) != memo[under].end()) + return; + memo[under].insert(f); + if(f.is_app()){ + if(!under && !f.has_quantifiers()) + return; + decl_kind k = f.decl().get_decl_kind(); + if(k == And || k == Or || k == Implies || k == Iff){ + int num_args = f.num_args(); + for(int i = 0; i < num_args; i++) + GetGroundLitsUnderQuants(memo,f.arg(i),res,under); + return; + } + } + else if (f.is_quantifier()){ +#if 0 + // treat closed quantified formula as a literal 'cause we hate nested quantifiers + if(under && IsClosedFormula(f)) + res.push_back(f); + else +#endif + GetGroundLitsUnderQuants(memo,f.body(),res,1); + return; + } + if(under && f.is_ground()) + res.push_back(f); + } + + RPFP::Term RPFP::StrengthenFormulaByCaseSplitting(const Term &f, std::vector &case_lits){ + hash_set memo[2]; + std::vector lits; + GetGroundLitsUnderQuants(memo, f, lits, 0); + hash_set lits_hash; + for(unsigned i = 0; i < lits.size(); i++) + lits_hash.insert(lits[i]); + hash_map subst; + hash_map stt_memo; + std::vector conjuncts; + for(unsigned i = 0; i < lits.size(); i++){ + const expr &lit = lits[i]; + if(lits_hash.find(NegateLit(lit)) == lits_hash.end()){ + case_lits.push_back(lit); + bool tval = false; + expr atom = lit; + if(lit.is_app() && lit.decl().get_decl_kind() == Not){ + tval = true; + atom = lit.arg(0); + } + expr etval = ctx.bool_val(tval); + if(atom.is_quantifier()) + subst[atom] = etval; // this is a bit desperate, since we can't eval quants + else { + int b = SubtermTruth(stt_memo,atom); + if(b == (tval ? 1 : 0)) + subst[atom] = etval; + else { + if(b == 0 || b == 1){ + etval = ctx.bool_val(b ? true : false); + subst[atom] = etval; + conjuncts.push_back(b ? atom : !atom); + } + } + } + } + } + expr g = f; + if(!subst.empty()){ + g = SubstRec(subst,f); + if(conjuncts.size()) + g = g && ctx.make(And,conjuncts); + g = g.simplify(); + } +#if 1 + expr g_old = g; + g = RemoveRedundancy(g); + bool changed = !eq(g,g_old); + g = g.simplify(); + if(changed) { // a second pass can get some more simplification + g = RemoveRedundancy(g); + g = g.simplify(); + } +#else + g = RemoveRedundancy(g); + g = g.simplify(); +#endif + g = AdjustQuantifiers(g); + return g; + } RPFP::Term RPFP::ModelValueAsConstraint(const Term &t){ if(t.is_array()){ @@ -1712,6 +2189,167 @@ namespace Duality { res = CreateRelation(p->Annotation.IndParams,funder); } +#if 0 + void RPFP::GreedyReduce(solver &s, std::vector &conjuncts){ + // verify + s.push(); + expr conj = ctx.make(And,conjuncts); + s.add(conj); + check_result res = s.check(); + if(res != unsat) + throw "should be unsat"; + s.pop(1); + + for(unsigned i = 0; i < conjuncts.size(); ){ + std::swap(conjuncts[i],conjuncts.back()); + expr save = conjuncts.back(); + conjuncts.pop_back(); + s.push(); + expr conj = ctx.make(And,conjuncts); + s.add(conj); + check_result res = s.check(); + s.pop(1); + if(res != unsat){ + conjuncts.push_back(save); + std::swap(conjuncts[i],conjuncts.back()); + i++; + } + } + } +#endif + + void RPFP::GreedyReduce(solver &s, std::vector &conjuncts){ + std::vector lits(conjuncts.size()); + for(unsigned i = 0; i < lits.size(); i++){ + func_decl pred = ctx.fresh_func_decl("@alit", ctx.bool_sort()); + lits[i] = pred(); + s.add(ctx.make(Implies,lits[i],conjuncts[i])); + } + + // verify + check_result res = s.check(lits.size(),&lits[0]); + if(res != unsat){ + // add the axioms in the off chance they are useful + const std::vector &theory = ls->get_axioms(); + for(unsigned i = 0; i < theory.size(); i++) + s.add(theory[i]); + if(s.check(lits.size(),&lits[0]) != unsat) + throw "should be unsat"; + } + + for(unsigned i = 0; i < conjuncts.size(); ){ + std::swap(conjuncts[i],conjuncts.back()); + std::swap(lits[i],lits.back()); + check_result res = s.check(lits.size()-1,&lits[0]); + if(res != unsat){ + std::swap(conjuncts[i],conjuncts.back()); + std::swap(lits[i],lits.back()); + i++; + } + else { + conjuncts.pop_back(); + lits.pop_back(); + } + } + } + + expr RPFP::NegateLit(const expr &f){ + if(f.is_app() && f.decl().get_decl_kind() == Not) + return f.arg(0); + else + return !f; + } + + void RPFP::NegateLits(std::vector &lits){ + for(unsigned i = 0; i < lits.size(); i++){ + expr &f = lits[i]; + if(f.is_app() && f.decl().get_decl_kind() == Not) + f = f.arg(0); + else + f = !f; + } + } + + expr RPFP::SimplifyOr(std::vector &lits){ + if(lits.size() == 0) + return ctx.bool_val(false); + if(lits.size() == 1) + return lits[0]; + return ctx.make(Or,lits); + } + + // set up edge constraint in aux solver + void RPFP::AddEdgeToSolver(Edge *edge){ + if(!edge->dual.null()) + aux_solver.add(edge->dual); + for(unsigned i = 0; i < edge->constraints.size(); i++){ + expr tl = edge->constraints[i]; + aux_solver.add(tl); + } + } + + void RPFP::InterpolateByCases(Node *root, Node *node){ + aux_solver.push(); + AddEdgeToSolver(node->Outgoing); + node->Annotation.SetEmpty(); + hash_set *core = new hash_set; + core->insert(node->Outgoing->dual); + while(1){ + aux_solver.push(); + expr annot = !GetAnnotation(node); + aux_solver.add(annot); + if(aux_solver.check() == unsat){ + aux_solver.pop(1); + break; + } + dualModel = aux_solver.get_model(); + aux_solver.pop(1); + Push(); + FixCurrentStateFull(node->Outgoing,annot); + ConstrainEdgeLocalized(node->Outgoing,!GetAnnotation(node)); + check_result foo = Check(root); + if(foo != unsat) + throw "should be unsat"; + AddToProofCore(*core); + Transformer old_annot = node->Annotation; + SolveSingleNode(root,node); + + { + expr itp = GetAnnotation(node); + dualModel = aux_solver.get_model(); + std::vector case_lits; + itp = StrengthenFormulaByCaseSplitting(itp, case_lits); + SetAnnotation(node,itp); + } + + if(node->Annotation.IsEmpty()){ + std::cout << "bad in InterpolateByCase -- core:\n"; + std::vector assumps; + 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); + } + if(proof_core) + delete proof_core; // shouldn't happen + proof_core = core; + aux_solver.pop(1); + } + + void RPFP::Generalize(Node *root, Node *node){ + aux_solver.push(); + AddEdgeToSolver(node->Outgoing); + expr fmla = GetAnnotation(node); + std::vector conjuncts; + CollectConjuncts(fmla,conjuncts,false); + GreedyReduce(aux_solver,conjuncts); // try to remove conjuncts one at a tme + aux_solver.pop(1); + NegateLits(conjuncts); + SetAnnotation(node,SimplifyOr(conjuncts)); + } /** Push a scope. Assertions made after Push can be undone by Pop. */ @@ -1733,10 +2371,26 @@ namespace Duality { (*it)->dual = expr(ctx,NULL); for(std::list::iterator it = back.nodes.begin(), en = back.nodes.end(); it != en; ++it) (*it)->dual = expr(ctx,NULL); + for(std::list >::iterator it = back.constraints.begin(), en = back.constraints.end(); it != en; ++it) + (*it).first->constraints.pop_back(); stack.pop_back(); } } + /** Erase the proof by performing a Pop, Push and re-assertion of + all the popped constraints */ + + void RPFP::PopPush(){ + slvr.pop(1); + slvr.push(); + stack_entry &back = stack.back(); + for(std::list::iterator it = back.edges.begin(), en = back.edges.end(); it != en; ++it) + slvr.add((*it)->dual); + for(std::list::iterator it = back.nodes.begin(), en = back.nodes.end(); it != en; ++it) + slvr.add((*it)->dual); + for(std::list >::iterator it = back.constraints.begin(), en = back.constraints.end(); it != en; ++it) + slvr.add((*it).second); + } @@ -1880,6 +2534,37 @@ namespace Duality { return SubstBoundRec(memo, subst, 0, t); } + int Z3User::MaxIndex(hash_map &memo, const Term &t) + { + std::pair foo(t,-1); + std::pair::iterator, bool> bar = memo.insert(foo); + int &res = bar.first->second; + if(!bar.second) return res; + if (t.is_app()){ + func_decl f = t.decl(); + int nargs = t.num_args(); + for(int i = 0; i < nargs; i++){ + int m = MaxIndex(memo, t.arg(i)); + if(m > res) + res = m; + } + } + else if (t.is_quantifier()){ + int bound = t.get_quantifier_num_bound(); + res = MaxIndex(memo,t.body()) - bound; + } + else if (t.is_var()) { + res = t.get_index_value(); + } + return res; + } + + bool Z3User::IsClosedFormula(const Term &t){ + hash_map memo; + return MaxIndex(memo,t) < 0; + } + + /** Convert a collection of clauses to Nodes and Edges in the RPFP. Predicate unknowns are uninterpreted predicates not @@ -2169,8 +2854,32 @@ 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::EdgeUsedInProof(Edge *edge){ + ComputeProofCore(); + if(!edge->dual.null() && proof_core->find(edge->dual) != proof_core->end()) + return true; + for(unsigned i = 0; i < edge->constraints.size(); i++) + if(proof_core->find(edge->constraints[i]) != proof_core->end()) + return true; + return false; + } RPFP::~RPFP(){ + ClearProofCore(); for(unsigned i = 0; i < nodes.size(); i++) delete nodes[i]; for(unsigned i = 0; i < edges.size(); i++) diff --git a/src/duality/duality_solver.cpp b/src/duality/duality_solver.cpp index 0043998d2..13c839186 100644 --- a/src/duality/duality_solver.cpp +++ b/src/duality/duality_solver.cpp @@ -184,7 +184,7 @@ namespace Duality { best.insert(*it); } #else - virtual void ChooseExpand(const std::set &choices, std::set &best, bool high_priority=false){ + virtual void ChooseExpand(const std::set &choices, std::set &best, bool high_priority=false, bool best_only=false){ if(high_priority) return; int best_score = INT_MAX; int worst_score = 0; @@ -194,13 +194,13 @@ namespace Duality { best_score = std::min(best_score,score); worst_score = std::max(worst_score,score); } - int cutoff = best_score + (worst_score-best_score)/2; + int cutoff = best_only ? best_score : (best_score + (worst_score-best_score)/2); for(std::set::iterator it = choices.begin(), en = choices.end(); it != en; ++it) if(scores[(*it)->map].updates <= cutoff) best.insert(*it); } #endif - + /** Called when done expanding a tree */ virtual void Done() {} }; @@ -1270,18 +1270,24 @@ namespace Duality { } } + bool UpdateNodeToNode(Node *node, Node *top){ + if(!node->Annotation.SubsetEq(top->Annotation)){ + reporter->Update(node,top->Annotation); + indset->Update(node,top->Annotation); + updated_nodes.insert(node->map); + node->Annotation.IntersectWith(top->Annotation); + return true; + } + return false; + } + /** Update the unwinding solution, using an interpolant for the derivation tree. */ void UpdateWithInterpolant(Node *node, RPFP *tree, Node *top){ if(top->Outgoing) for(unsigned i = 0; i < top->Outgoing->Children.size(); i++) UpdateWithInterpolant(node->Outgoing->Children[i],tree,top->Outgoing->Children[i]); - if(!node->Annotation.SubsetEq(top->Annotation)){ - reporter->Update(node,top->Annotation); - indset->Update(node,top->Annotation); - updated_nodes.insert(node->map); - node->Annotation.IntersectWith(top->Annotation); - } + UpdateNodeToNode(node, top); heuristic->Update(node); } @@ -1305,7 +1311,8 @@ namespace Duality { if(node->Bound.IsFull()) return true; reporter->Bound(node); int start_decs = rpfp->CumulativeDecisions(); - DerivationTree dt(this,unwinding,reporter,heuristic,FullExpand); + DerivationTree *dtp = new DerivationTreeSlow(this,unwinding,reporter,heuristic,FullExpand); + DerivationTree &dt = *dtp; bool res = dt.Derive(unwinding,node,UseUnderapprox); int end_decs = rpfp->CumulativeDecisions(); // std::cout << "decisions: " << (end_decs - start_decs) << std::endl; @@ -1321,6 +1328,7 @@ namespace Duality { UpdateWithInterpolant(node,dt.tree,dt.top); delete dt.tree; } + delete dtp; return !res; } @@ -1491,7 +1499,7 @@ namespace Duality { return res != unsat; } - bool Build(){ + virtual bool Build(){ #ifdef EFFORT_BOUNDED_STRAT start_decs = tree->CumulativeDecisions(); #endif @@ -1545,7 +1553,7 @@ namespace Duality { } } - void ExpandNode(RPFP::Node *p){ + virtual void ExpandNode(RPFP::Node *p){ // tree->RemoveEdge(p->Outgoing); Edge *edge = duality->GetNodeOutgoing(p->map,last_decs); std::vector &cs = edge->Children; @@ -1573,6 +1581,7 @@ namespace Duality { } #else #if 0 + void ExpansionChoices(std::set &best){ std::vector unused_set, used_set; std::set choices; @@ -1598,12 +1607,12 @@ namespace Duality { heuristic->ChooseExpand(choices, best); } #else - void ExpansionChoicesFull(std::set &best, bool high_priority){ + void ExpansionChoicesFull(std::set &best, bool high_priority, bool best_only = false){ std::set choices; for(std::list::iterator it = leaves.begin(), en = leaves.end(); it != en; ++it) if (high_priority || !tree->Empty(*it)) // if used in the counter-model choices.insert(*it); - heuristic->ChooseExpand(choices, best, high_priority); + heuristic->ChooseExpand(choices, best, high_priority, best_only); } void ExpansionChoicesRec(std::vector &unused_set, std::vector &used_set, @@ -1641,9 +1650,9 @@ namespace Duality { std::set old_choices; - void ExpansionChoices(std::set &best, bool high_priority){ + void ExpansionChoices(std::set &best, bool high_priority, bool best_only = false){ if(!underapprox || constrained || high_priority){ - ExpansionChoicesFull(best, high_priority); + ExpansionChoicesFull(best, high_priority,best_only); return; } std::vector unused_set, used_set; @@ -1668,28 +1677,259 @@ namespace Duality { #endif #endif - bool ExpandSomeNodes(bool high_priority = false){ + bool ExpandSomeNodes(bool high_priority = false, int max = INT_MAX){ #ifdef EFFORT_BOUNDED_STRAT last_decs = tree->CumulativeDecisions() - start_decs; #endif timer_start("ExpandSomeNodes"); timer_start("ExpansionChoices"); std::set choices; - ExpansionChoices(choices,high_priority); + ExpansionChoices(choices,high_priority,max != INT_MAX); timer_stop("ExpansionChoices"); std::list leaves_copy = leaves; // copy so can modify orig leaves.clear(); + int count = 0; for(std::list::iterator it = leaves_copy.begin(), en = leaves_copy.end(); it != en; ++it){ - if(choices.find(*it) != choices.end()) + if(choices.find(*it) != choices.end() && count < max){ + count++; ExpandNode(*it); + } else leaves.push_back(*it); } timer_stop("ExpandSomeNodes"); return !choices.empty(); } + void RemoveExpansion(RPFP::Node *p){ + Edge *edge = p->Outgoing; + Node *parent = edge->Parent; + std::vector cs = edge->Children; + tree->DeleteEdge(edge); + for(unsigned i = 0; i < cs.size(); i++) + tree->DeleteNode(cs[i]); + leaves.push_back(parent); + } }; + class DerivationTreeSlow : public DerivationTree { + public: + + struct stack_entry { + unsigned level; // SMT solver stack level + std::vector expansions; + }; + + std::vector stack; + + hash_map updates; + + DerivationTreeSlow(Duality *_duality, RPFP *rpfp, Reporter *_reporter, Heuristic *_heuristic, bool _full_expand) + : DerivationTree(_duality, rpfp, _reporter, _heuristic, _full_expand) { + stack.push_back(stack_entry()); + } + + virtual bool Build(){ + + stack.back().level = tree->slvr.get_scope_level(); + + while (true) + { + lbool res; + + unsigned slvr_level = tree->slvr.get_scope_level(); + if(slvr_level != stack.back().level) + throw "stacks out of sync!"; + + // res = tree->Solve(top, 1); // incremental solve, keep interpolants for one pop + check_result foo = tree->Check(top); + res = foo == unsat ? l_false : l_true; + + if (res == l_false) { + if (stack.empty()) // should never happen + return false; + + { + std::vector &expansions = stack.back().expansions; + int update_count = 0; + for(unsigned i = 0; i < expansions.size(); i++){ + Node *node = expansions[i]; + tree->SolveSingleNode(top,node); + if(expansions.size() == 1 && NodeTooComplicated(node)) + SimplifyNode(node); + tree->Generalize(top,node); + if(RecordUpdate(node)) + update_count++; + } + if(update_count == 0) + reporter->Message("backtracked without learning"); + } + tree->ComputeProofCore(); // need to compute the proof core before popping solver + while(1) { + std::vector &expansions = stack.back().expansions; + bool prev_level_used = LevelUsedInProof(stack.size()-2); // need to compute this before pop + tree->Pop(1); + hash_set leaves_to_remove; + for(unsigned i = 0; i < expansions.size(); i++){ + Node *node = expansions[i]; + // if(node != top) + // tree->ConstrainParent(node->Incoming[0],node); + std::vector &cs = node->Outgoing->Children; + for(unsigned i = 0; i < cs.size(); i++){ + leaves_to_remove.insert(cs[i]); + UnmapNode(cs[i]); + if(std::find(updated_nodes.begin(),updated_nodes.end(),cs[i]) != updated_nodes.end()) + throw "help!"; + } + } + RemoveLeaves(leaves_to_remove); // have to do this before actually deleting the children + for(unsigned i = 0; i < expansions.size(); i++){ + Node *node = expansions[i]; + RemoveExpansion(node); + } + stack.pop_back(); + if(prev_level_used || stack.size() == 1) break; + RemoveUpdateNodesAtCurrentLevel(); // this level is about to be deleted -- remove its children from update list + std::vector &unused_ex = stack.back().expansions; + for(unsigned i = 0; i < unused_ex.size(); i++) + heuristic->Update(unused_ex[i]->map); // make it less likely to expand this node in future + } + HandleUpdatedNodes(); + if(stack.size() == 1) + return false; + } + else { + tree->Push(); + std::vector &expansions = stack.back().expansions; + for(unsigned i = 0; i < expansions.size(); i++){ + tree->FixCurrentState(expansions[i]->Outgoing); + } +#if 0 + if(tree->slvr.check() == unsat) + throw "help!"; +#endif + stack.push_back(stack_entry()); + stack.back().level = tree->slvr.get_scope_level(); + if(ExpandSomeNodes(false,1)){ + continue; + } + while(stack.size() > 1){ + tree->Pop(1); + stack.pop_back(); + } + return true; + } + } + } + + bool NodeTooComplicated(Node *node){ + return tree->CountOperators(node->Annotation.Formula) > 3; + } + + void SimplifyNode(Node *node){ + // have to destroy the old proof to get a new interpolant + tree->PopPush(); + tree->InterpolateByCases(top,node); + } + + bool LevelUsedInProof(unsigned level){ + std::vector &expansions = stack[level].expansions; + for(unsigned i = 0; i < expansions.size(); i++) + if(tree->EdgeUsedInProof(expansions[i]->Outgoing)) + return true; + return false; + } + + void RemoveUpdateNodesAtCurrentLevel() { + for(std::list::iterator it = updated_nodes.begin(), en = updated_nodes.end(); it != en;){ + Node *node = *it; + if(AtCurrentStackLevel(node->Incoming[0]->Parent)){ + std::list::iterator victim = it; + ++it; + updated_nodes.erase(victim); + } + else + ++it; + } + } + + void RemoveLeaves(hash_set &leaves_to_remove){ + std::list leaves_copy; + leaves_copy.swap(leaves); + for(std::list::iterator it = leaves_copy.begin(), en = leaves_copy.end(); it != en; ++it){ + if(leaves_to_remove.find(*it) == leaves_to_remove.end()) + leaves.push_back(*it); + } + } + + hash_map > node_map; + std::list updated_nodes; + + virtual void ExpandNode(RPFP::Node *p){ + stack.back().expansions.push_back(p); + DerivationTree::ExpandNode(p); + std::vector &new_nodes = p->Outgoing->Children; + for(unsigned i = 0; i < new_nodes.size(); i++){ + Node *n = new_nodes[i]; + node_map[n->map].push_back(n); + } + } + + bool RecordUpdate(Node *node){ + bool res = duality->UpdateNodeToNode(node->map,node); + if(res){ + std::vector to_update = node_map[node->map]; + for(unsigned i = 0; i < to_update.size(); i++){ + Node *node2 = to_update[i]; + // maintain invariant that no nodes on updated list are created at current stack level + if(node2 == node || !(node->Incoming.size() > 0 && AtCurrentStackLevel(node2->Incoming[0]->Parent))){ + updated_nodes.push_back(node2); + if(node2 != node) + node2->Annotation = node->Annotation; + } + } + } + return res; + } + + void HandleUpdatedNodes(){ + for(std::list::iterator it = updated_nodes.begin(), en = updated_nodes.end(); it != en;){ + Node *node = *it; + node->Annotation = node->map->Annotation; + if(node->Incoming.size() > 0) + tree->ConstrainParent(node->Incoming[0],node); + if(AtCurrentStackLevel(node->Incoming[0]->Parent)){ + std::list::iterator victim = it; + ++it; + updated_nodes.erase(victim); + } + else + ++it; + } + } + + bool AtCurrentStackLevel(Node *node){ + std::vector vec = stack.back().expansions; + for(unsigned i = 0; i < vec.size(); i++) + if(vec[i] == node) + return true; + return false; + } + + void UnmapNode(Node *node){ + std::vector &vec = node_map[node->map]; + for(unsigned i = 0; i < vec.size(); i++){ + if(vec[i] == node){ + std::swap(vec[i],vec.back()); + vec.pop_back(); + return; + } + } + throw "can't unmap node"; + } + + }; + + class Covering { struct cover_info { @@ -2084,7 +2324,7 @@ namespace Duality { return name; } - virtual void ChooseExpand(const std::set &choices, std::set &best, bool high_priority){ + virtual void ChooseExpand(const std::set &choices, std::set &best, bool high_priority, bool best_only){ if(!high_priority || !old_cex.tree){ Heuristic::ChooseExpand(choices,best,false); return; diff --git a/src/duality/duality_wrapper.cpp b/src/duality/duality_wrapper.cpp index fef70e031..55883202f 100644 --- a/src/duality/duality_wrapper.cpp +++ b/src/duality/duality_wrapper.cpp @@ -26,16 +26,23 @@ Revision History: #include "expr_abstract.h" #include "stopwatch.h" #include "model_smt2_pp.h" +#include "qe_lite.h" namespace Duality { - solver::solver(Duality::context& c) : object(c), the_model(c) { + solver::solver(Duality::context& c, bool extensional) : object(c), the_model(c) { params_ref p; p.set_bool("proof", true); // this is currently useless p.set_bool("model", true); p.set_bool("unsat_core", true); + p.set_bool("mbqi",true); + p.set_str("mbqi.id","itp"); // use mbqi for quantifiers in interpolants + p.set_uint("mbqi.max_iterations",1); // use mbqi for quantifiers in interpolants + if(true || extensional) + p.set_bool("array.extensional",true); scoped_ptr sf = mk_smt_solver_factory(); m_solver = (*sf)(m(), p, true, true, true, ::symbol::null); + m_solver->updt_params(p); // why do we have to do this? canceled = false; } @@ -323,6 +330,14 @@ expr context::make_quant(decl_kind op, const std::vector &_sorts, const st return simplify(p); } + expr expr::qe_lite() const { + ::qe_lite qe(m()); + expr_ref result(to_expr(raw()),m()); + proof_ref pf(m()); + qe(result,pf); + return ctx().cook(result); + } + expr clone_quantifier(const expr &q, const expr &b){ return q.ctx().cook(q.m().update_quantifier(to_quantifier(q.raw()), to_expr(b.raw()))); } @@ -425,15 +440,18 @@ expr context::make_quant(decl_kind op, const std::vector &_sorts, const st static int linearize_assumptions(int num, TermTree *assumptions, - std::vector &linear_assumptions, + std::vector > &linear_assumptions, std::vector &parents){ for(unsigned i = 0; i < assumptions->getChildren().size(); i++) num = linearize_assumptions(num, assumptions->getChildren()[i], linear_assumptions, parents); - linear_assumptions[num] = assumptions->getTerm(); + // linear_assumptions[num].push_back(assumptions->getTerm()); for(unsigned i = 0; i < assumptions->getChildren().size(); i++) parents[assumptions->getChildren()[i]->getNumber()] = num; parents[num] = SHRT_MAX; // in case we have no parent - linear_assumptions[num] = assumptions->getTerm(); + linear_assumptions[num].push_back(assumptions->getTerm()); + std::vector &ts = assumptions->getTerms(); + for(unsigned i = 0; i < ts.size(); i++) + linear_assumptions[num].push_back(ts[i]); return num + 1; } @@ -462,14 +480,15 @@ expr context::make_quant(decl_kind op, const std::vector &_sorts, const st { int size = assumptions->number(0); - std::vector linear_assumptions(size); + std::vector > linear_assumptions(size); std::vector parents(size); linearize_assumptions(0,assumptions,linear_assumptions,parents); ptr_vector< ::ast> _interpolants(size-1); - ptr_vector< ::ast>_assumptions(size); + vector >_assumptions(size); for(int i = 0; i < size; i++) - _assumptions[i] = linear_assumptions[i]; + for(unsigned j = 0; j < linear_assumptions[i].size(); j++) + _assumptions[i].push_back(linear_assumptions[i][j]); ::vector _parents; _parents.resize(parents.size()); for(unsigned i = 0; i < parents.size(); i++) _parents[i] = parents[i]; @@ -477,11 +496,12 @@ expr context::make_quant(decl_kind op, const std::vector &_sorts, const st for(unsigned i = 0; i < theory.size(); i++) _theory[i] = theory[i]; - push(); if(!incremental){ + push(); for(unsigned i = 0; i < linear_assumptions.size(); i++) - add(linear_assumptions[i]); + for(unsigned j = 0; j < linear_assumptions[i].size(); j++) + add(linear_assumptions[i][j]); } check_result res = check(); @@ -517,7 +537,8 @@ expr context::make_quant(decl_kind op, const std::vector &_sorts, const st } #endif - pop(); + if(!incremental) + pop(); return (res == unsat) ? l_false : ((res == sat) ? l_true : l_undef); @@ -549,6 +570,29 @@ expr context::make_quant(decl_kind op, const std::vector &_sorts, const st return ""; } + + static void get_assumptions_rec(stl_ext::hash_set &memo, const proof &pf, std::vector &assumps){ + if(memo.find(pf) != memo.end())return; + memo.insert(pf); + pfrule dk = pf.rule(); + if(dk == PR_ASSERTED){ + expr con = pf.conc(); + assumps.push_back(con); + } + else { + unsigned nprems = pf.num_prems(); + for(unsigned i = 0; i < nprems; i++){ + proof arg = pf.prem(i); + get_assumptions_rec(memo,arg,assumps); + } + } + } + + void proof::get_assumptions(std::vector &assumps){ + stl_ext::hash_set memo; + get_assumptions_rec(memo,*this,assumps); + } + void ast::show() const{ std::cout << mk_pp(raw(), m()) << std::endl; @@ -559,6 +603,40 @@ expr context::make_quant(decl_kind op, const std::vector &_sorts, const st std::cout << std::endl; } + void model::show_hash() const { + std::ostringstream ss; + model_smt2_pp(ss, m(), *m_model, 0); + hash_space::hash hasher; + unsigned h = hasher(ss.str()); + std::cout << "model hash: " << h << "\n"; + } + + void solver::show() { + unsigned n = m_solver->get_num_assertions(); + if(!n) + return; + ast_smt_pp pp(m()); + for (unsigned i = 0; i < n-1; ++i) + pp.add_assumption(m_solver->get_assertion(i)); + pp.display_smt2(std::cout, m_solver->get_assertion(n-1)); + } + + void solver::show_assertion_ids() { +#if 0 + unsigned n = m_solver->get_num_assertions(); + std::cerr << "assertion ids: "; + for (unsigned i = 0; i < n-1; ++i) + std::cerr << " " << m_solver->get_assertion(i)->get_id(); + std::cerr << "\n"; +#else + unsigned n = m_solver->get_num_assertions(); + std::cerr << "assertion ids hash: "; + unsigned h = 0; + for (unsigned i = 0; i < n-1; ++i) + h += m_solver->get_assertion(i)->get_id(); + std::cerr << h << "\n"; +#endif + } void include_ast_show(ast &a){ a.show(); diff --git a/src/duality/duality_wrapper.h b/src/duality/duality_wrapper.h index 21ed45479..a36f93b40 100755 --- a/src/duality/duality_wrapper.h +++ b/src/duality/duality_wrapper.h @@ -393,6 +393,7 @@ namespace Duality { sort array_range() const; }; + class func_decl : public ast { public: func_decl() : ast() {} @@ -412,6 +413,7 @@ namespace Duality { expr operator()(unsigned n, expr const * args) const; expr operator()(const std::vector &args) const; + expr operator()() const; expr operator()(expr const & a) const; expr operator()(int a) const; expr operator()(expr const & a1, expr const & a2) const; @@ -455,6 +457,8 @@ namespace Duality { bool is_quantifier() const {return raw()->get_kind() == AST_QUANTIFIER;} bool is_var() const {return raw()->get_kind() == AST_VAR;} bool is_label (bool &pos,std::vector &names) const ; + bool is_ground() const {return to_app(raw())->is_ground();} + bool has_quantifiers() const {return to_app(raw())->has_quantifiers();} // operator Z3_app() const { assert(is_app()); return reinterpret_cast(m_ast); } func_decl decl() const {return func_decl(ctx(),to_app(raw())->get_decl());} @@ -554,6 +558,8 @@ namespace Duality { expr simplify(params const & p) const; + expr qe_lite() const; + friend expr clone_quantifier(const expr &, const expr &); friend expr clone_quantifier(const expr &q, const expr &b, const std::vector &patterns); @@ -593,6 +599,36 @@ namespace Duality { }; + typedef ::decl_kind pfrule; + + class proof : public ast { + public: + proof(context & c):ast(c) {} + proof(context & c, ::proof *s):ast(c, s) {} + proof(proof const & s):ast(s) {} + operator ::proof*() const { return to_app(raw()); } + proof & operator=(proof const & s) { return static_cast(ast::operator=(s)); } + + pfrule rule() const { + ::func_decl *d = to_app(raw())->get_decl(); + return d->get_decl_kind(); + } + + unsigned num_prems() const { + return to_app(raw())->get_num_args() - 1; + } + + expr conc() const { + return ctx().cook(to_app(raw())->get_arg(num_prems())); + } + + proof prem(unsigned i) const { + return proof(ctx(),to_app(to_app(raw())->get_arg(i))); + } + + void get_assumptions(std::vector &assumps); + }; + #if 0 #if Z3_MAJOR_VERSION > 4 || Z3_MAJOR_VERSION == 4 && Z3_MINOR_VERSION >= 3 @@ -691,6 +727,7 @@ namespace Duality { } void show() const; + void show_hash() const; unsigned num_consts() const {return m_model.get()->get_num_constants();} unsigned num_funcs() const {return m_model.get()->get_num_functions();} @@ -775,7 +812,7 @@ namespace Duality { model the_model; bool canceled; public: - solver(context & c); + solver(context & c, bool extensional = false); solver(context & c, ::solver *s):object(c),the_model(c) { m_solver = s; canceled = false;} solver(solver const & s):object(s), the_model(s.the_model) { m_solver = s.m_solver; canceled = false;} ~solver() { @@ -867,6 +904,16 @@ namespace Duality { if(m_solver) m_solver->cancel(); } + + unsigned get_scope_level(){return m_solver->get_scope_level();} + + void show(); + void show_assertion_ids(); + + proof get_proof(){ + return proof(ctx(),m_solver->get_proof()); + } + }; #if 0 @@ -1144,6 +1191,9 @@ namespace Duality { inline expr func_decl::operator()(const std::vector &args) const { return operator()(args.size(),&args[0]); } + inline expr func_decl::operator()() const { + return operator()(0,0); + } inline expr func_decl::operator()(expr const & a) const { return operator()(1,&a); } @@ -1199,6 +1249,8 @@ namespace Duality { inline expr getTerm(){return term;} + inline std::vector &getTerms(){return terms;} + inline std::vector &getChildren(){ return children; } @@ -1215,6 +1267,8 @@ namespace Duality { } inline void setTerm(expr t){term = t;} + + inline void addTerm(expr t){terms.push_back(t);} inline void setChildren(const std::vector & _children){ children = _children; @@ -1231,6 +1285,7 @@ namespace Duality { private: expr term; + std::vector terms; std::vector children; int num; }; @@ -1277,6 +1332,7 @@ namespace Duality { void SetWeakInterpolants(bool weak); void SetPrintToFile(const std::string &file_name); + const std::vector &GetInterpolationAxioms() {return theory;} const char *profile(); private: @@ -1331,7 +1387,8 @@ namespace std { class less { public: bool operator()(const Duality::ast &s, const Duality::ast &t) const { - return s.raw() < t.raw(); // s.raw()->get_id() < t.raw()->get_id(); + // return s.raw() < t.raw(); + return s.raw()->get_id() < t.raw()->get_id(); } }; } @@ -1362,7 +1419,8 @@ namespace std { class less { public: bool operator()(const Duality::func_decl &s, const Duality::func_decl &t) const { - return s.raw() < t.raw(); // s.raw()->get_id() < t.raw()->get_id(); + // return s.raw() < t.raw(); + return s.raw()->get_id() < t.raw()->get_id(); } }; } diff --git a/src/interp/iz3base.h b/src/interp/iz3base.h index 30ac57bae..6bf09bb85 100755 --- a/src/interp/iz3base.h +++ b/src/interp/iz3base.h @@ -24,6 +24,16 @@ Revision History: #include "iz3mgr.h" #include "iz3scopes.h" +namespace hash_space { + template <> + class hash { + public: + size_t operator()(func_decl * const &s) const { + return (size_t) s; + } + }; +} + /* Base class for interpolators. Includes an AST manager and a scoping object as bases. */ @@ -182,6 +192,4 @@ class iz3base : public iz3mgr, public scopes { - - #endif diff --git a/src/interp/iz3foci.cpp b/src/interp/iz3foci.cpp index 85e090c5b..1d81a1b15 100755 --- a/src/interp/iz3foci.cpp +++ b/src/interp/iz3foci.cpp @@ -51,6 +51,13 @@ public: typedef hash_map NodeToAst; NodeToAst node_to_ast; // maps Z3 ast's to foci expressions + // We only use this for FuncDeclToSymbol, which has no range destructor + struct symb_hash { + size_t operator()(const symb &s) const { + return (size_t) s; + } + }; + typedef hash_map FuncDeclToSymbol; FuncDeclToSymbol func_decl_to_symbol; // maps Z3 func decls to symbols diff --git a/src/interp/iz3hash.h b/src/interp/iz3hash.h index f6767c037..75d9aa604 100755 --- a/src/interp/iz3hash.h +++ b/src/interp/iz3hash.h @@ -141,6 +141,7 @@ namespace std { #ifndef WIN32 +#if 0 namespace stl_ext { template class hash { @@ -150,6 +151,7 @@ namespace stl_ext { } }; } +#endif #endif diff --git a/src/interp/iz3interp.cpp b/src/interp/iz3interp.cpp index 92afc5723..56dc1ccec 100755 --- a/src/interp/iz3interp.cpp +++ b/src/interp/iz3interp.cpp @@ -75,15 +75,16 @@ struct frame_reducer : public iz3mgr { } } - void get_frames(const std::vector &z3_preds, + void get_frames(const std::vector >&z3_preds, const std::vector &orig_parents, - std::vector &assertions, + std::vector >&assertions, std::vector &parents, z3pf proof){ frames = z3_preds.size(); orig_parents_copy = orig_parents; for(unsigned i = 0; i < z3_preds.size(); i++) - frame_map[z3_preds[i]] = i; + for(unsigned j = 0; j < z3_preds[i].size(); j++) + frame_map[z3_preds[i][j]] = i; used_frames.resize(frames); hash_set memo; get_proof_assumptions_rec(proof,memo,used_frames); @@ -202,7 +203,7 @@ public: } void proof_to_interpolant(z3pf proof, - const std::vector &cnsts, + const std::vector > &cnsts, const std::vector &parents, std::vector &interps, const std::vector &theory, @@ -212,11 +213,12 @@ public: test_secondary(cnsts,parents,interps); return; #endif + profiling::timer_start("Interpolation prep"); // get rid of frames not used in proof - std::vector cnsts_vec; + std::vector > cnsts_vec; std::vector parents_vec; frame_reducer fr(*this); fr.get_frames(cnsts,parents,cnsts_vec,parents_vec,proof); @@ -235,10 +237,7 @@ public: #define BINARY_INTERPOLATION #ifndef BINARY_INTERPOLATION // create a translator - std::vector > cnsts_vec_vec(cnsts_vec.size()); - for(unsigned i = 0; i < cnsts_vec.size(); i++) - cnsts_vec_vec[i].push_back(cnsts_vec[i]); - iz3translation *tr = iz3translation::create(*this,sp,cnsts_vec_vec,parents_vec,theory); + iz3translation *tr = iz3translation::create(*this,sp,cnsts_vec,parents_vec,theory); tr_killer.set(tr); // set the translation options, if needed @@ -273,7 +272,8 @@ public: std::vector > cnsts_vec_vec(2); for(unsigned j = 0; j < cnsts_vec.size(); j++){ bool is_A = the_base.in_range(j,rng); - cnsts_vec_vec[is_A ? 0 : 1].push_back(cnsts_vec[j]); + for(unsigned k = 0; k < cnsts_vec[j].size(); k++) + cnsts_vec_vec[is_A ? 0 : 1].push_back(cnsts_vec[j][k]); } killme tr_killer_i; @@ -308,6 +308,19 @@ public: } + void proof_to_interpolant(z3pf proof, + std::vector &cnsts, + const std::vector &parents, + std::vector &interps, + const std::vector &theory, + interpolation_options_struct *options = 0 + ){ + std::vector > cnsts_vec(cnsts.size()); + for(unsigned i = 0; i < cnsts.size(); i++) + cnsts_vec[i].push_back(cnsts[i]); + proof_to_interpolant(proof,cnsts_vec,parents,interps,theory,options); + } + // same as above, but represents the tree using an ast void proof_to_interpolant(const z3pf &proof, @@ -322,7 +335,6 @@ public: to_parents_vec_representation(_cnsts, tree, cnsts, parents, theory, pos_map); - //use the parents vector representation to compute interpolant proof_to_interpolant(proof,cnsts,parents,interps,theory,options); @@ -397,6 +409,35 @@ void iz3interpolate(ast_manager &_m_manager, interps[i] = itp.uncook(_interps[i]); } +void iz3interpolate(ast_manager &_m_manager, + ast *proof, + const ::vector > &cnsts, + const ::vector &parents, + ptr_vector &interps, + const ptr_vector &theory, + interpolation_options_struct * options) +{ + iz3interp itp(_m_manager); + if(options) + options->apply(itp); + std::vector > _cnsts(cnsts.size()); + std::vector _parents(parents.size()); + std::vector _interps; + std::vector _theory(theory.size()); + for(unsigned i = 0; i < cnsts.size(); i++) + for(unsigned j = 0; j < cnsts[i].size(); j++) + _cnsts[i].push_back(itp.cook(cnsts[i][j])); + for(unsigned i = 0; i < parents.size(); i++) + _parents[i] = parents[i]; + for(unsigned i = 0; i < theory.size(); i++) + _theory[i] = itp.cook(theory[i]); + iz3mgr::ast _proof = itp.cook(proof); + itp.proof_to_interpolant(_proof,_cnsts,_parents,_interps,_theory,options); + interps.resize(_interps.size()); + for(unsigned i = 0; i < interps.size(); i++) + interps[i] = itp.uncook(_interps[i]); +} + void iz3interpolate(ast_manager &_m_manager, ast *proof, const ptr_vector &cnsts, @@ -461,5 +502,3 @@ void interpolation_options_struct::apply(iz3base &b){ b.set_option((*it).first,(*it).second); } - - diff --git a/src/interp/iz3interp.h b/src/interp/iz3interp.h index 62f967c02..52aa716c3 100644 --- a/src/interp/iz3interp.h +++ b/src/interp/iz3interp.h @@ -56,6 +56,16 @@ void iz3interpolate(ast_manager &_m_manager, const ptr_vector &theory, interpolation_options_struct * options = 0); +/* Same as above, but each constraint is a vector of formulas. */ + +void iz3interpolate(ast_manager &_m_manager, + ast *proof, + const vector > &cnsts, + const ::vector &parents, + ptr_vector &interps, + const ptr_vector &theory, + interpolation_options_struct * options = 0); + /* Compute an interpolant from a proof. This version uses the ast representation, for compatibility with the new API. */ diff --git a/src/interp/iz3mgr.cpp b/src/interp/iz3mgr.cpp index faa4a636d..f35dae93f 100644 --- a/src/interp/iz3mgr.cpp +++ b/src/interp/iz3mgr.cpp @@ -190,7 +190,7 @@ iz3mgr::ast iz3mgr::make_quant(opr op, const std::vector &bvs, ast &body){ op == Forall, names.size(), &types[0], &names[0], abs_body.get(), 0, - symbol(), + symbol("itp"), symbol(), 0, 0, 0, 0 @@ -761,6 +761,19 @@ int iz3mgr::occurs_in(ast var, ast e){ } +bool iz3mgr::solve_arith(const ast &v, const ast &x, const ast &y, ast &res){ + if(op(x) == Plus){ + int n = num_args(x); + for(int i = 0; i < n; i++){ + if(arg(x,i) == v){ + res = z3_simplify(make(Sub, y, make(Sub, x, v))); + return true; + } + } + } + return false; +} + // find a controlling equality for a given variable v in a term // a controlling equality is of the form v = t, which, being // false would force the formula to have the specifid truth value @@ -774,6 +787,9 @@ iz3mgr::ast iz3mgr::cont_eq(stl_ext::hash_set &cont_eq_memo, bool truth, as if(!truth && op(e) == Equal){ if(arg(e,0) == v) return(arg(e,1)); if(arg(e,1) == v) return(arg(e,0)); + ast res; + if(solve_arith(v,arg(e,0),arg(e,1),res)) return res; + if(solve_arith(v,arg(e,1),arg(e,0),res)) return res; } if((!truth && op(e) == And) || (truth && op(e) == Or)){ int nargs = num_args(e); @@ -815,11 +831,35 @@ iz3mgr::ast iz3mgr::subst(ast var, ast t, ast e){ return subst(memo,var,t,e); } +iz3mgr::ast iz3mgr::subst(stl_ext::hash_map &subst_memo,ast e){ + std::pair foo(e,ast()); + std::pair::iterator,bool> bar = subst_memo.insert(foo); + ast &res = bar.first->second; + if(bar.second){ + int nargs = num_args(e); + std::vector args(nargs); + for(int i = 0; i < nargs; i++) + args[i] = subst(subst_memo,arg(e,i)); + opr f = op(e); + if(f == Equal && args[0] == args[1]) res = mk_true(); + else res = clone(e,args); + } + return res; +} + // apply a quantifier to a formula, with some optimizations // 1) bound variable does not occur -> no quantifier // 2) bound variable must be equal to some term -> substitute iz3mgr::ast iz3mgr::apply_quant(opr quantifier, ast var, ast e){ + if((quantifier == Forall && op(e) == And) + || (quantifier == Exists && op(e) == Or)){ + int n = num_args(e); + std::vector args(n); + for(int i = 0; i < n; i++) + args[i] = apply_quant(quantifier,var,arg(e,i)); + return make(op(e),args); + } if(!occurs_in(var,e))return e; hash_set cont_eq_memo; ast cterm = cont_eq(cont_eq_memo, quantifier == Forall, var, e); diff --git a/src/interp/iz3mgr.h b/src/interp/iz3mgr.h index f6c0bdf87..645c72ccb 100644 --- a/src/interp/iz3mgr.h +++ b/src/interp/iz3mgr.h @@ -65,7 +65,7 @@ class ast_i { return _ast == other._ast; } bool lt(const ast_i &other) const { - return _ast < other._ast; + return _ast->get_id() < other._ast->get_id(); } friend bool operator==(const ast_i &x, const ast_i&y){ return x.eq(y); @@ -76,7 +76,7 @@ class ast_i { friend bool operator<(const ast_i &x, const ast_i&y){ return x.lt(y); } - size_t hash() const {return (size_t)_ast;} + size_t hash() const {return _ast->get_id();} bool null() const {return !_ast;} }; @@ -140,7 +140,8 @@ namespace std { class less { public: bool operator()(const ast_r &s, const ast_r &t) const { - return s.raw() < t.raw(); // s.raw()->get_id() < t.raw()->get_id(); + // return s.raw() < t.raw(); + return s.raw()->get_id() < t.raw()->get_id(); } }; } @@ -359,6 +360,12 @@ class iz3mgr { return fid == m().get_basic_family_id() && k == BOOL_SORT; } + bool is_array_type(type t){ + family_id fid = to_sort(t)->get_family_id(); + decl_kind k = to_sort(t)->get_decl_kind(); + return fid == m_array_fid && k == ARRAY_SORT; + } + type get_range_type(symb s){ return to_func_decl(s)->get_range(); } @@ -631,6 +638,9 @@ class iz3mgr { ast subst(ast var, ast t, ast e); + // apply a substitution defined by a map + ast subst(stl_ext::hash_map &map, ast e); + // apply a quantifier to a formula, with some optimizations // 1) bound variable does not occur -> no quantifier // 2) bound variable must be equal to some term -> substitute @@ -683,13 +693,14 @@ class iz3mgr { protected: ast_manager &m_manager; + int occurs_in(ast var, ast e); private: ast mki(family_id fid, decl_kind sk, int n, raw_ast **args); ast make(opr op, int n, raw_ast **args); ast make(symb sym, int n, raw_ast **args); int occurs_in1(stl_ext::hash_map &occurs_in_memo, ast var, ast e); - int occurs_in(ast var, ast e); + bool solve_arith(const ast &v, const ast &x, const ast &y, ast &res); ast cont_eq(stl_ext::hash_set &cont_eq_memo, bool truth, ast v, ast e); ast subst(stl_ext::hash_map &subst_memo, ast var, ast t, ast e); diff --git a/src/interp/iz3pp.cpp b/src/interp/iz3pp.cpp index 1f9351453..df6fcaf53 100644 --- a/src/interp/iz3pp.cpp +++ b/src/interp/iz3pp.cpp @@ -40,6 +40,20 @@ Revision History: using namespace stl_ext; #endif +#ifndef WIN32 +// We promise not to use this for hash_map with range destructor +namespace stl_ext { + template <> + class hash { + public: + size_t operator()(const expr *p) const { + return (size_t) p; + } + }; +} +#endif + + // TBD: algebraic data-types declarations will not be printed. class free_func_visitor { ast_manager& m; diff --git a/src/interp/iz3proof_itp.cpp b/src/interp/iz3proof_itp.cpp index a2d05f7f9..75d14bca1 100644 --- a/src/interp/iz3proof_itp.cpp +++ b/src/interp/iz3proof_itp.cpp @@ -118,6 +118,30 @@ class iz3proof_itp_impl : public iz3proof_itp { where t is an arbitrary term */ symb rewrite_B; + /* a normalization step is of the form (lhs=rhs) : proof, where "proof" + is a proof of lhs=rhs and lhs is a mixed term. If rhs is a mixed term + then it must have a greater index than lhs. */ + symb normal_step; + + /* A chain of normalization steps is either "true" (the null chain) + or normal_chain( ), where step is a normalization step + and tail is a normalization chain. The lhs of must have + a less term index than any lhs in the chain. Moreover, the rhs of + may not occur as the lhs of step in . If we wish to + add lhs=rhs to the beginning of and rhs=rhs' occurs in + we must apply transitivity, transforming to lhs=rhs'. */ + + symb normal_chain; + + /* If p is a proof of Q and c is a normalization chain, then normal(p,c) + is a proof of Q(c) (that is, Q with all substitutions in c performed). */ + + symb normal; + + /** Stand-ins for quantifiers */ + + symb sforall, sexists; + ast get_placeholder(ast t){ hash_map::iterator it = placeholders.find(t); @@ -209,6 +233,10 @@ class iz3proof_itp_impl : public iz3proof_itp { ast neg_pivot_lit = mk_not(atom); if(op(pivot) != Not) std::swap(premise1,premise2); + if(op(pivot) == Equal && op(arg(pivot,0)) == Select && op(arg(pivot,1)) == Select){ + neg_pivot_lit = mk_not(neg_pivot_lit); + std::swap(premise1,premise2); + } return resolve_arith_rec1(memo, neg_pivot_lit, premise1, premise2); } @@ -333,7 +361,13 @@ class iz3proof_itp_impl : public iz3proof_itp { break; } default: - res = itp2; + { + symb s = sym(itp2); + if(s == sforall || s == sexists) + res = make(s,arg(itp2,0),resolve_arith_rec2(memo, pivot1, conj1, arg(itp2,1))); + else + res = itp2; + } } } return res; @@ -363,7 +397,13 @@ class iz3proof_itp_impl : public iz3proof_itp { break; } default: - res = itp1; + { + symb s = sym(itp1); + if(s == sforall || s == sexists) + res = make(s,arg(itp1,0),resolve_arith_rec1(memo, neg_pivot_lit, arg(itp1,1), itp2)); + else + res = itp1; + } } } return res; @@ -451,7 +491,12 @@ class iz3proof_itp_impl : public iz3proof_itp { hash_map simplify_memo; ast simplify(const ast &t){ - return simplify_rec(t); + ast res = normalize(simplify_rec(t)); +#ifdef BOGUS_QUANTS + if(localization_vars.size()) + res = add_quants(z3_simplify(res)); +#endif + return res; } ast simplify_rec(const ast &e){ @@ -521,12 +566,18 @@ class iz3proof_itp_impl : public iz3proof_itp { throw cannot_simplify(); } + bool is_normal_ineq(const ast &ineq){ + if(sym(ineq) == normal) + return is_ineq(arg(ineq,0)); + return is_ineq(ineq); + } + ast simplify_sum(std::vector &args){ - ast cond = mk_true(); + ast Aproves = mk_true(), Bproves = mk_true(); ast ineq = args[0]; - if(!is_ineq(ineq)) throw cannot_simplify(); - sum_cond_ineq(ineq,cond,args[1],args[2]); - return my_implies(cond,ineq); + if(!is_normal_ineq(ineq)) throw cannot_simplify(); + sum_cond_ineq(ineq,args[1],args[2],Aproves,Bproves); + return my_and(Aproves,my_implies(Bproves,ineq)); } ast simplify_rotate_sum(const ast &pl, const ast &pf){ @@ -539,29 +590,42 @@ class iz3proof_itp_impl : public iz3proof_itp { return sym(chain) == concat; } - ast ineq_from_chain(const ast &chain, ast &cond){ - if(is_rewrite_chain(chain)){ - ast last = chain_last(chain); - ast rest = chain_rest(chain); - if(is_true(rest) && is_rewrite_side(LitA,last) - && is_true(rewrite_lhs(last))){ - cond = my_and(cond,rewrite_cond(last)); - return rewrite_rhs(last); - } - if(is_rewrite_side(LitB,last) && is_true(rewrite_cond(last))) - return ineq_from_chain(rest,cond); +#if 0 + ast ineq_from_chain_simple(const ast &chain, ast &cond){ + if(is_true(chain)) + return chain; + ast last = chain_last(chain); + ast rest = chain_rest(chain); + if(is_true(rest) && is_rewrite_side(LitA,last) + && is_true(rewrite_lhs(last))){ + cond = my_and(cond,rewrite_cond(last)); + return rewrite_rhs(last); } + if(is_rewrite_side(LitB,last) && is_true(rewrite_cond(last))) + return ineq_from_chain_simple(rest,cond); + return chain; + } +#endif + + ast ineq_from_chain(const ast &chain, ast &Aproves, ast &Bproves){ + if(is_rewrite_chain(chain)) + return rewrite_chain_to_normal_ineq(chain,Aproves,Bproves); return chain; } - void sum_cond_ineq(ast &ineq, ast &cond, const ast &coeff2, const ast &ineq2){ + + void sum_cond_ineq(ast &ineq, const ast &coeff2, const ast &ineq2, ast &Aproves, ast &Bproves){ opr o = op(ineq2); if(o == Implies){ - sum_cond_ineq(ineq,cond,coeff2,arg(ineq2,1)); - cond = my_and(cond,arg(ineq2,0)); + sum_cond_ineq(ineq,coeff2,arg(ineq2,1),Aproves,Bproves); + Bproves = my_and(Bproves,arg(ineq2,0)); } else { - ast the_ineq = ineq_from_chain(ineq2,cond); + ast the_ineq = ineq_from_chain(ineq2,Aproves,Bproves); + if(sym(ineq) == normal || sym(the_ineq) == normal){ + sum_normal_ineq(ineq,coeff2,the_ineq,Aproves,Bproves); + return; + } if(is_ineq(the_ineq)) linear_comb(ineq,coeff2,the_ineq); else @@ -569,6 +633,27 @@ class iz3proof_itp_impl : public iz3proof_itp { } } + void destruct_normal(const ast &pf, ast &p, ast &n){ + if(sym(pf) == normal){ + p = arg(pf,0); + n = arg(pf,1); + } + else { + p = pf; + n = mk_true(); + } + } + + void sum_normal_ineq(ast &ineq, const ast &coeff2, const ast &ineq2, ast &Aproves, ast &Bproves){ + ast in1,in2,n1,n2; + destruct_normal(ineq,in1,n1); + destruct_normal(ineq2,in2,n2); + ast dummy1, dummy2; + sum_cond_ineq(in1,coeff2,in2,dummy1,dummy2); + n1 = merge_normal_chains(n1,n2, Aproves, Bproves); + ineq = make_normal(in1,n1); + } + bool is_ineq(const ast &ineq){ opr o = op(ineq); if(o == Not) o = op(arg(ineq,0)); @@ -577,6 +662,12 @@ class iz3proof_itp_impl : public iz3proof_itp { // divide both sides of inequality by a non-negative integer divisor ast idiv_ineq(const ast &ineq1, const ast &divisor){ + if(sym(ineq1) == normal){ + ast in1,n1; + destruct_normal(ineq1,in1,n1); + in1 = idiv_ineq(in1,divisor); + return make_normal(in1,n1); + } if(divisor == make_int(rational(1))) return ineq1; ast ineq = ineq1; @@ -585,17 +676,23 @@ class iz3proof_itp_impl : public iz3proof_itp { return make(op(ineq),mk_idiv(arg(ineq,0),divisor),mk_idiv(arg(ineq,1),divisor)); } - ast rotate_sum_rec(const ast &pl, const ast &pf, ast &cond, ast &ineq){ + ast rotate_sum_rec(const ast &pl, const ast &pf, ast &Bproves, ast &ineq){ if(pf == pl) - return my_implies(cond,simplify_ineq(ineq)); + return my_implies(Bproves,simplify_ineq(ineq)); if(op(pf) == Uninterpreted && sym(pf) == sum){ if(arg(pf,2) == pl){ - sum_cond_ineq(ineq,cond,make_int("1"),arg(pf,0)); + ast Aproves = mk_true(); + sum_cond_ineq(ineq,make_int("1"),arg(pf,0),Aproves,Bproves); + if(!is_true(Aproves)) + throw "help!"; ineq = idiv_ineq(ineq,arg(pf,1)); - return my_implies(cond,ineq); + return my_implies(Bproves,ineq); } - sum_cond_ineq(ineq,cond,arg(pf,1),arg(pf,2)); - return rotate_sum_rec(pl,arg(pf,0),cond,ineq); + ast Aproves = mk_true(); + sum_cond_ineq(ineq,arg(pf,1),arg(pf,2),Aproves,Bproves); + if(!is_true(Aproves)) + throw "help!"; + return rotate_sum_rec(pl,arg(pf,0),Bproves,ineq); } throw cannot_simplify(); } @@ -605,28 +702,30 @@ class iz3proof_itp_impl : public iz3proof_itp { ast equality = arg(neg_equality,0); ast x = arg(equality,0); ast y = arg(equality,1); - ast cond1 = mk_true(); - ast xleqy = round_ineq(ineq_from_chain(arg(pf,1),cond1)); - ast yleqx = round_ineq(ineq_from_chain(arg(pf,2),cond1)); + ast Aproves1 = mk_true(), Bproves1 = mk_true(); + ast xleqy = round_ineq(ineq_from_chain(arg(pf,1),Aproves1,Bproves1)); + ast yleqx = round_ineq(ineq_from_chain(arg(pf,2),Aproves1,Bproves1)); ast ineq1 = make(Leq,make_int("0"),make_int("0")); - sum_cond_ineq(ineq1,cond1,make_int("-1"),xleqy); - sum_cond_ineq(ineq1,cond1,make_int("-1"),yleqx); - cond1 = my_and(cond1,z3_simplify(ineq1)); - ast cond2 = mk_true(); + sum_cond_ineq(ineq1,make_int("-1"),xleqy,Aproves1,Bproves1); + sum_cond_ineq(ineq1,make_int("-1"),yleqx,Aproves1,Bproves1); + Bproves1 = my_and(Bproves1,z3_simplify(ineq1)); + ast Aproves2 = mk_true(), Bproves2 = mk_true(); ast ineq2 = make(Leq,make_int("0"),make_int("0")); - sum_cond_ineq(ineq2,cond2,make_int("1"),xleqy); - sum_cond_ineq(ineq2,cond2,make_int("1"),yleqx); - cond2 = z3_simplify(ineq2); + sum_cond_ineq(ineq2,make_int("1"),xleqy,Aproves2,Bproves2); + sum_cond_ineq(ineq2,make_int("1"),yleqx,Aproves2,Bproves2); + Bproves2 = z3_simplify(ineq2); + if(!is_true(Aproves1) || !is_true(Aproves2)) + throw "help!"; if(get_term_type(x) == LitA){ ast iter = z3_simplify(make(Plus,x,get_ineq_rhs(xleqy))); - ast rewrite1 = make_rewrite(LitA,top_pos,cond1,make(Equal,x,iter)); - ast rewrite2 = make_rewrite(LitB,top_pos,cond2,make(Equal,iter,y)); + ast rewrite1 = make_rewrite(LitA,top_pos,Bproves1,make(Equal,x,iter)); + ast rewrite2 = make_rewrite(LitB,top_pos,Bproves2,make(Equal,iter,y)); return chain_cons(chain_cons(mk_true(),rewrite1),rewrite2); } if(get_term_type(y) == LitA){ ast iter = z3_simplify(make(Plus,y,get_ineq_rhs(yleqx))); - ast rewrite2 = make_rewrite(LitA,top_pos,cond1,make(Equal,iter,y)); - ast rewrite1 = make_rewrite(LitB,top_pos,cond2,make(Equal,x,iter)); + ast rewrite2 = make_rewrite(LitA,top_pos,Bproves1,make(Equal,iter,y)); + ast rewrite1 = make_rewrite(LitB,top_pos,Bproves2,make(Equal,x,iter)); return chain_cons(chain_cons(mk_true(),rewrite1),rewrite2); } throw cannot_simplify(); @@ -649,11 +748,18 @@ class iz3proof_itp_impl : public iz3proof_itp { ast equa = sep_cond(arg(pf,0),cond); if(is_equivrel_chain(equa)){ ast lhs,rhs; eq_from_ineq(arg(neg_equality,0),lhs,rhs); // get inequality we need to prove - ast ineqs= chain_ineqs(op(arg(neg_equality,0)),LitA,equa,lhs,rhs); // chain must be from lhs to rhs - cond = my_and(cond,chain_conditions(LitA,equa)); - ast Bconds = chain_conditions(LitB,equa); - if(is_true(Bconds) && op(ineqs) != And) - return my_implies(cond,ineqs); + LitType lhst = get_term_type(lhs), rhst = get_term_type(rhs); + if(lhst != LitMixed && rhst != LitMixed){ + ast ineqs= chain_ineqs(op(arg(neg_equality,0)),LitA,equa,lhs,rhs); // chain must be from lhs to rhs + cond = my_and(cond,chain_conditions(LitA,equa)); + ast Bconds = z3_simplify(chain_conditions(LitB,equa)); + if(is_true(Bconds) && op(ineqs) != And) + return my_implies(cond,ineqs); + } + else { + ast itp = make(Leq,make_int(rational(0)),make_int(rational(0))); + return make_normal(itp,cons_normal(fix_normal(lhs,rhs,equa),mk_true())); + } } } throw cannot_simplify(); @@ -757,11 +863,57 @@ class iz3proof_itp_impl : public iz3proof_itp { chain = concat_rewrite_chain(chain,split[1]); } } - else // if not an equivalence, must be of form T <-> pred + else { // if not an equivalence, must be of form T <-> pred chain = concat_rewrite_chain(P,PeqQ); + } return chain; } + void get_subterm_normals(const ast &ineq1, const ast &ineq2, const ast &chain, ast &normals, + const ast &pos, hash_set &memo, ast &Aproves, ast &Bproves){ + opr o1 = op(ineq1); + opr o2 = op(ineq2); + if(o1 == Not || o1 == Leq || o1 == Lt || o1 == Geq || o1 == Gt || o1 == Plus || o1 == Times){ + int n = num_args(ineq1); + if(o2 != o1 || num_args(ineq2) != n) + throw "bad inequality rewriting"; + for(int i = 0; i < n; i++){ + ast new_pos = add_pos_to_end(pos,i); + get_subterm_normals(arg(ineq1,i), arg(ineq2,i), chain, normals, new_pos, memo, Aproves, Bproves); + } + } + else if(get_term_type(ineq2) == LitMixed && memo.find(ineq2) == memo.end()){ + memo.insert(ineq2); + ast sub_chain = extract_rewrites(chain,pos); + if(is_true(sub_chain)) + throw "bad inequality rewriting"; + ast new_normal = make_normal_step(ineq2,ineq1,reverse_chain(sub_chain)); + normals = merge_normal_chains(normals,cons_normal(new_normal,mk_true()), Aproves, Bproves); + } + } + + ast rewrite_chain_to_normal_ineq(const ast &chain, ast &Aproves, ast &Bproves){ + ast tail, pref = get_head_chain(chain,tail,false); // pref is x=y, tail is x=y -> x'=y' + ast head = chain_last(pref); + ast ineq1 = rewrite_rhs(head); + ast ineq2 = apply_rewrite_chain(ineq1,tail); + ast nc = mk_true(); + hash_set memo; + get_subterm_normals(ineq1,ineq2,tail,nc,top_pos,memo, Aproves, Bproves); + ast itp; + if(is_rewrite_side(LitA,head)){ + itp = ineq1; + ast mc = z3_simplify(chain_side_proves(LitB,pref)); + Bproves = my_and(Bproves,mc); + } + else { + itp = make(Leq,make_int(rational(0)),make_int(rational(0))); + ast mc = z3_simplify(chain_side_proves(LitA,pref)); + Aproves = my_and(Aproves,mc); + } + return make_normal(itp,nc); + } + /* Given a chain rewrite chain deriving not P and a rewrite chain deriving P, return an interpolant. */ ast contra_chain(const ast &neg_chain, const ast &pos_chain){ // equality is a special case. we use the derivation of x=y to rewrite not(x=y) to not(y=y) @@ -790,11 +942,18 @@ class iz3proof_itp_impl : public iz3proof_itp { } ast simplify_modpon(const std::vector &args){ - ast cond = mk_true(); - ast chain = simplify_modpon_fwd(args,cond); - ast Q2 = sep_cond(args[2],cond); - ast interp = is_negation_chain(chain) ? contra_chain(chain,Q2) : contra_chain(Q2,chain); - return my_implies(cond,interp); + ast Aproves = mk_true(), Bproves = mk_true(); + ast chain = simplify_modpon_fwd(args,Bproves); + ast Q2 = sep_cond(args[2],Bproves); + ast interp; + if(is_normal_ineq(Q2)){ // inequalities are special + ast nQ2 = rewrite_chain_to_normal_ineq(chain,Aproves,Bproves); + sum_cond_ineq(nQ2,make_int(rational(1)),Q2,Aproves,Bproves); + interp = normalize(nQ2); + } + else + interp = is_negation_chain(chain) ? contra_chain(chain,Q2) : contra_chain(Q2,chain); + return my_and(Aproves,my_implies(Bproves,interp)); } @@ -1035,6 +1194,12 @@ class iz3proof_itp_impl : public iz3proof_itp { return make(add_pos,make_int(rational(arg)),pos); } + ast add_pos_to_end(const ast &pos, int i){ + if(pos == top_pos) + return pos_add(i,pos); + return make(add_pos,arg(pos,0),add_pos_to_end(arg(pos,1),i)); + } + /* return the argument number of position, if not top */ int pos_arg(const ast &pos){ rational r; @@ -1170,6 +1335,10 @@ class iz3proof_itp_impl : public iz3proof_itp { return make(sym(rew),pos_add(apos,arg(rew,0)),arg(rew,1),arg(rew,2)); } + ast rewrite_pos_set(const ast &pos, const ast &rew){ + return make(sym(rew),pos,arg(rew,1),arg(rew,2)); + } + ast rewrite_up(const ast &rew){ return make(sym(rew),arg(arg(rew,0),1),arg(rew,1),arg(rew,2)); } @@ -1317,6 +1486,28 @@ class iz3proof_itp_impl : public iz3proof_itp { split_chain_rec(chain,res); } + ast extract_rewrites(const ast &chain, const ast &pos){ + if(is_true(chain)) + return chain; + ast last = chain_last(chain); + ast rest = chain_rest(chain); + ast new_rest = extract_rewrites(rest,pos); + ast p1 = rewrite_pos(last); + ast diff; + switch(pos_diff(p1,pos,diff)){ + case -1: { + ast new_last = rewrite_pos_set(diff, last); + return chain_cons(new_rest,new_last); + } + case 1: + if(rewrite_lhs(last) != rewrite_rhs(last)) + throw "bad rewrite chain"; + break; + default:; + } + return new_rest; + } + ast down_chain(const ast &chain){ ast split[2]; split_chain(chain,split); @@ -1381,7 +1572,7 @@ class iz3proof_itp_impl : public iz3proof_itp { // ast s = ineq_to_lhs(ineq); // ast srhs = arg(s,1); ast srhs = arg(ineq,0); - if(op(srhs) == Plus && num_args(srhs) == 2){ + if(op(srhs) == Plus && num_args(srhs) == 2 && arg(ineq,1) == make_int(rational(0))){ lhs = arg(srhs,0); rhs = arg(srhs,1); // if(op(lhs) == Times) @@ -1393,6 +1584,11 @@ class iz3proof_itp_impl : public iz3proof_itp { return; } } + if(op(ineq) == Leq || op(ineq) == Geq){ + lhs = srhs; + rhs = arg(ineq,1); + return; + } throw "bad ineq"; } @@ -1404,7 +1600,204 @@ class iz3proof_itp_impl : public iz3proof_itp { return chain_cons(rest,last); } + ast apply_rewrite_chain(const ast &t, const ast &chain){ + if(is_true(chain)) + return t; + ast last = chain_last(chain); + ast rest = chain_rest(chain); + ast mid = apply_rewrite_chain(t,rest); + ast res = subst_in_pos(mid,rewrite_pos(last),rewrite_rhs(last)); + return res; + } + ast drop_rewrites(LitType t, const ast &chain, ast &remainder){ + if(!is_true(chain)){ + ast last = chain_last(chain); + ast rest = chain_rest(chain); + if(is_rewrite_side(t,last)){ + ast res = drop_rewrites(t,rest,remainder); + remainder = chain_cons(remainder,last); + return res; + } + } + remainder = mk_true(); + return chain; + } + + // Normalization chains + + ast cons_normal(const ast &first, const ast &rest){ + return make(normal_chain,first,rest); + } + + ast normal_first(const ast &t){ + return arg(t,0); + } + + ast normal_rest(const ast &t){ + return arg(t,1); + } + + ast normal_lhs(const ast &t){ + return arg(arg(t,0),0); + } + + ast normal_rhs(const ast &t){ + return arg(arg(t,0),1); + } + + ast normal_proof(const ast &t){ + return arg(t,1); + } + + ast make_normal_step(const ast &lhs, const ast &rhs, const ast &proof){ + return make(normal_step,make_equiv(lhs,rhs),proof); + } + + ast make_normal(const ast &ineq, const ast &nrml){ + if(!is_ineq(ineq)) + throw "what?"; + return make(normal,ineq,nrml); + } + + ast fix_normal(const ast &lhs, const ast &rhs, const ast &proof){ + LitType rhst = get_term_type(rhs); + if(rhst != LitMixed || ast_id(lhs) < ast_id(rhs)) + return make_normal_step(lhs,rhs,proof); + else + return make_normal_step(rhs,lhs,reverse_chain(proof)); + } + + ast chain_side_proves(LitType side, const ast &chain){ + LitType other_side = side == LitA ? LitB : LitA; + return my_and(chain_conditions(other_side,chain),my_implies(chain_conditions(side,chain),chain_formulas(side,chain))); + } + + // Merge two normalization chains + ast merge_normal_chains_rec(const ast &chain1, const ast &chain2, hash_map &trans, ast &Aproves, ast &Bproves){ + if(is_true(chain1)) + return chain2; + if(is_true(chain2)) + return chain1; + ast f1 = normal_first(chain1); + ast f2 = normal_first(chain2); + ast lhs1 = normal_lhs(f1); + ast lhs2 = normal_lhs(f2); + int id1 = ast_id(lhs1); + int id2 = ast_id(lhs2); + if(id1 < id2) return cons_normal(f1,merge_normal_chains_rec(normal_rest(chain1),chain2,trans,Aproves,Bproves)); + if(id2 < id1) return cons_normal(f2,merge_normal_chains_rec(chain1,normal_rest(chain2),trans,Aproves,Bproves)); + ast rhs1 = normal_rhs(f1); + ast rhs2 = normal_rhs(f2); + LitType t1 = get_term_type(rhs1); + LitType t2 = get_term_type(rhs2); + int tid1 = ast_id(rhs1); + int tid2 = ast_id(rhs2); + ast pf1 = normal_proof(f1); + ast pf2 = normal_proof(f2); + ast new_normal; + if(t1 == LitMixed && (t2 != LitMixed || tid2 > tid1)){ + ast new_proof = concat_rewrite_chain(reverse_chain(pf1),pf2); + new_normal = f2; + trans[rhs1] = make_normal_step(rhs1,rhs2,new_proof); + } + else if(t2 == LitMixed && (t1 != LitMixed || tid1 > tid2)) + return merge_normal_chains_rec(chain2,chain1,trans,Aproves,Bproves); + else if(t1 == LitA && t2 == LitB){ + ast new_proof = concat_rewrite_chain(reverse_chain(pf1),pf2); + ast Bproof, Aproof = drop_rewrites(LitB,new_proof,Bproof); + ast mcA = chain_side_proves(LitB,Aproof); + Bproves = my_and(Bproves,mcA); + ast mcB = chain_side_proves(LitA,Bproof); + Aproves = my_and(Aproves,mcB); + ast rep = apply_rewrite_chain(rhs1,Aproof); + new_proof = concat_rewrite_chain(pf1,Aproof); + new_normal = make_normal_step(rhs1,rep,new_proof); + } + else if(t1 == LitA && t2 == LitB) + return merge_normal_chains_rec(chain2,chain1,trans,Aproves,Bproves); + else if(t1 == LitA) { + ast new_proof = concat_rewrite_chain(reverse_chain(pf1),pf2); + ast mc = chain_side_proves(LitB,new_proof); + Bproves = my_and(Bproves,mc); + new_normal = f1; // choice is arbitrary + } + else { /* t1 = t2 = LitB */ + ast new_proof = concat_rewrite_chain(reverse_chain(pf1),pf2); + ast mc = chain_side_proves(LitA,new_proof); + Aproves = my_and(Aproves,mc); + new_normal = f1; // choice is arbitrary + } + return cons_normal(new_normal,merge_normal_chains_rec(normal_rest(chain1),normal_rest(chain2),trans,Aproves,Bproves)); + } + + ast trans_normal_chain(const ast &chain, hash_map &trans){ + if(is_true(chain)) + return chain; + ast f = normal_first(chain); + ast r = normal_rest(chain); + ast rhs = normal_rhs(f); + hash_map::iterator it = trans.find(rhs); + ast new_normal; + if(it != trans.end()){ + const ast &f2 = it->second; + ast pf = concat_rewrite_chain(normal_proof(f),normal_proof(f2)); + new_normal = make_normal_step(normal_lhs(f),normal_rhs(f2),pf); + } + else + new_normal = f; + return cons_normal(new_normal,trans_normal_chain(r,trans)); + } + + ast merge_normal_chains(const ast &chain1, const ast &chain2, ast &Aproves, ast &Bproves){ + hash_map trans; + ast res = merge_normal_chains_rec(chain1,chain2,trans,Aproves,Bproves); + res = trans_normal_chain(res,trans); + return res; + } + + bool destruct_cond_ineq(ast t, ast &Aproves, ast &Bproves, ast&ineq){ + if(op(t) == And){ + Aproves = arg(t,0); + t = arg(t,1); + } + else + Aproves = mk_true(); + if(op(t) == Implies){ + Bproves = arg(t,0); + t = arg(t,1); + } + else + Bproves = mk_true(); + if(is_normal_ineq(t)){ + ineq = t; + return true; + } + return false; + } + + ast cons_cond_ineq(const ast &Aproves, const ast &Bproves, const ast &ineq){ + return my_and(Aproves,my_implies(Bproves,ineq)); + } + + ast normalize(const ast &ct){ + ast Aproves,Bproves,t; + if(!destruct_cond_ineq(ct,Aproves,Bproves,t)) + return ct; + if(sym(t) != normal) + return ct; + ast chain = arg(t,1); + hash_map map; + for(ast c = chain; !is_true(c); c = normal_rest(c)){ + ast first = normal_first(c); + ast lhs = normal_lhs(first); + ast rhs = normal_rhs(first); + map[lhs] = rhs; + } + ast res = subst(map,arg(t,0)); + return cons_cond_ineq(Aproves,Bproves,res); + } + /** Make an assumption node. The given clause is assumed in the given frame. */ virtual node make_assumption(int frame, const std::vector &assumption){ if(!weak){ @@ -1522,9 +1915,22 @@ class iz3proof_itp_impl : public iz3proof_itp { return itp; } + ast capture_localization(ast e){ + // #define CAPTURE_LOCALIZATION +#ifdef CAPTURE_LOCALIZATION + for(int i = localization_vars.size() - 1; i >= 0; i--){ + LocVar &lv = localization_vars[i]; + if(occurs_in(lv.var,e)){ + symb q = (pv->in_range(lv.frame,rng)) ? sexists : sforall; + e = make(q,make(Equal,lv.var,lv.term),e); // use Equal because it is polymorphic + } + } +#endif + return e; + } + /** Make an axiom node. The conclusion must be an instance of an axiom. */ - virtual node make_axiom(const std::vector &conclusion){ - prover::range frng = pv->range_full(); + virtual node make_axiom(const std::vector &conclusion, prover::range frng){ int nargs = conclusion.size(); std::vector largs(nargs); std::vector eqs; @@ -1546,7 +1952,11 @@ class iz3proof_itp_impl : public iz3proof_itp { for(unsigned i = 0; i < eqs.size(); i++) itp = make_mp(eqs[i],itp,pfs[i]); - return itp; + return capture_localization(itp); + } + + virtual node make_axiom(const std::vector &conclusion){ + return make_axiom(conclusion,pv->range_full()); } /** Make a Contra node. This rule takes a derivation of the form @@ -1939,6 +2349,8 @@ class iz3proof_itp_impl : public iz3proof_itp { */ ast make_refl(const ast &e){ + if(get_term_type(e) == LitA) + return mk_false(); return mk_true(); // TODO: is this right? } @@ -1972,7 +2384,8 @@ class iz3proof_itp_impl : public iz3proof_itp { int nargs = num_args(e); if(nargs > 0 /* && (!is_local(e) || flo <= hi || fhi >= lo) */){ prover::range frng = rng; - if(op(e) == Uninterpreted){ + opr o = op(e); + if(o == Uninterpreted){ symb f = sym(e); prover::range srng = pv->sym_range(f); if(pv->ranges_intersect(srng,rng)) // localize to desired range if possible @@ -1980,6 +2393,9 @@ class iz3proof_itp_impl : public iz3proof_itp { else frng = srng; // this term will be localized } + else if(o == Plus || o == Times){ // don't want bound variables inside arith ops + frng = erng; // this term will be localized + } std::vector largs(nargs); std::vector eqs; std::vector pfs; @@ -2006,6 +2422,9 @@ class iz3proof_itp_impl : public iz3proof_itp { if(pv->ranges_intersect(pv->ast_scope(e),rng)) return e; // this term occurs in range, so it's O.K. + if(is_array_type(get_type(e))) + throw "help!"; + // choose a frame for the constraint that is close to range int frame = pv->range_near(pv->ast_scope(e),rng); @@ -2018,12 +2437,89 @@ class iz3proof_itp_impl : public iz3proof_itp { return new_var; } + ast delete_quant(hash_map &memo, const ast &v, const ast &e){ + std::pair foo(e,ast()); + std::pair::iterator,bool> bar = memo.insert(foo); + ast &res = bar.first->second; + if(bar.second){ + opr o = op(e); + switch(o){ + case Or: + case And: + case Implies: { + unsigned nargs = num_args(e); + std::vector args; args.resize(nargs); + for(unsigned i = 0; i < nargs; i++) + args[i] = delete_quant(memo, v, arg(e,i)); + res = make(o,args); + break; + } + case Uninterpreted: { + symb s = sym(e); + ast w = arg(arg(e,0),0); + if(s == sforall || s == sexists){ + res = delete_quant(memo,v,arg(e,1)); + if(w != v) + res = make(s,w,res); + break; + } + } + default: + res = e; + } + } + return res; + } + + ast insert_quants(hash_map &memo, const ast &e){ + std::pair foo(e,ast()); + std::pair::iterator,bool> bar = memo.insert(foo); + ast &res = bar.first->second; + if(bar.second){ + opr o = op(e); + switch(o){ + case Or: + case And: + case Implies: { + unsigned nargs = num_args(e); + std::vector args; args.resize(nargs); + for(unsigned i = 0; i < nargs; i++) + args[i] = insert_quants(memo, arg(e,i)); + res = make(o,args); + break; + } + case Uninterpreted: { + symb s = sym(e); + if(s == sforall || s == sexists){ + opr q = (s == sforall) ? Forall : Exists; + ast v = arg(arg(e,0),0); + hash_map dmemo; + ast body = delete_quant(dmemo,v,arg(e,1)); + body = insert_quants(memo,body); + res = apply_quant(q,v,body); + break; + } + } + default: + res = e; + } + } + return res; + } + ast add_quants(ast e){ +#ifdef CAPTURE_LOCALIZATION + if(!localization_vars.empty()){ + hash_map memo; + e = insert_quants(memo,e); + } +#else for(int i = localization_vars.size() - 1; i >= 0; i--){ LocVar &lv = localization_vars[i]; opr quantifier = (pv->in_range(lv.frame,rng)) ? Exists : Forall; e = apply_quant(quantifier,lv.var,e); } +#endif return e; } @@ -2035,7 +2531,11 @@ class iz3proof_itp_impl : public iz3proof_itp { /* Return an interpolant from a proof of false */ ast interpolate(const node &pf){ // proof of false must be a formula, with quantified symbols +#ifndef BOGUS_QUANTS return add_quants(z3_simplify(pf)); +#else + return z3_simplify(pf); +#endif } ast resolve_with_quantifier(const ast &pivot1, const ast &conj1, @@ -2055,7 +2555,7 @@ class iz3proof_itp_impl : public iz3proof_itp { ast npP = make_mp(make(Iff,nPloc,nP),npPloc,neqpf); ast nrP = make_resolution(nP,conj2,npP); ast res = make_resolution(Ploc,rP,nrP); - return res; + return capture_localization(res); } ast get_contra_coeff(const ast &f){ @@ -2141,6 +2641,16 @@ public: m().inc_ref(rewrite_A); rewrite_B = function("@rewrite_B",3,boolboolbooldom,bool_type()); m().inc_ref(rewrite_B); + normal_step = function("@normal_step",2,boolbooldom,bool_type()); + m().inc_ref(normal_step); + normal_chain = function("@normal_chain",2,boolbooldom,bool_type()); + m().inc_ref(normal_chain); + normal = function("@normal",2,boolbooldom,bool_type()); + m().inc_ref(normal); + sforall = function("@sforall",2,boolbooldom,bool_type()); + m().inc_ref(sforall); + sexists = function("@sexists",2,boolbooldom,bool_type()); + m().inc_ref(sexists); } ~iz3proof_itp_impl(){ diff --git a/src/interp/iz3proof_itp.h b/src/interp/iz3proof_itp.h index 299f391ea..4d76e3a92 100644 --- a/src/interp/iz3proof_itp.h +++ b/src/interp/iz3proof_itp.h @@ -70,6 +70,9 @@ class iz3proof_itp : public iz3mgr { /** Make an axiom node. The conclusion must be an instance of an axiom. */ virtual node make_axiom(const std::vector &conclusion) = 0; + /** Make an axiom node. The conclusion must be an instance of an axiom. Localize axiom instance to range*/ + virtual node make_axiom(const std::vector &conclusion, prover::range) = 0; + /** Make a Contra node. This rule takes a derivation of the form Gamma |- False and produces |- \/~Gamma. */ diff --git a/src/interp/iz3translate.cpp b/src/interp/iz3translate.cpp index 4ea755eff..fae914292 100755 --- a/src/interp/iz3translate.cpp +++ b/src/interp/iz3translate.cpp @@ -109,36 +109,49 @@ public: symbols and assign each to a frame. THe assignment is heuristic. */ - void scan_skolems_rec(hash_set &memo, const ast &proof){ - std::pair::iterator,bool> bar = memo.insert(proof); - if(!bar.second) - return; + int scan_skolems_rec(hash_map &memo, const ast &proof, int frame){ + std::pair foo(proof,INT_MAX); + std::pair bar = memo.insert(foo); + int &res = bar.first->second; + if(!bar.second) return res; pfrule dk = pr(proof); - if(dk == PR_SKOLEMIZE){ + if(dk == PR_ASSERTED){ + ast ass = conc(proof); + res = frame_of_assertion(ass); + } + else if(dk == PR_SKOLEMIZE){ ast quanted = arg(conc(proof),0); if(op(quanted) == Not) quanted = arg(quanted,0); - range r = ast_range(quanted); - if(range_is_empty(r)) - r = ast_scope(quanted); + // range r = ast_range(quanted); + // if(range_is_empty(r)) + range r = ast_scope(quanted); if(range_is_empty(r)) throw "can't skolemize"; - int frame = range_max(r); + if(frame == INT_MAX || !in_range(frame,r)) + frame = range_max(r); // this is desperation -- may fail if(frame >= frames) frame = frames - 1; add_frame_range(frame,arg(conc(proof),1)); r = ast_scope(arg(conc(proof),1)); } + else if(dk==PR_MODUS_PONENS_OEQ){ + frame = scan_skolems_rec(memo,prem(proof,0),frame); + scan_skolems_rec(memo,prem(proof,1),frame); + } else { unsigned nprems = num_prems(proof); for(unsigned i = 0; i < nprems; i++){ - scan_skolems_rec(memo,prem(proof,i)); + int bar = scan_skolems_rec(memo,prem(proof,i),frame); + if(res == INT_MAX || res == bar) res = bar; + else if(bar != INT_MAX) res = -1; } } + return res; } void scan_skolems(const ast &proof){ - hash_set memo; - scan_skolems_rec(memo,proof); + hash_map memo; + scan_skolems_rec(memo,proof, INT_MAX); } // determine locality of a proof term @@ -1364,6 +1377,18 @@ public: return eq2; } + bool get_store_array(const ast &t, ast &res){ + if(op(t) == Store){ + res = t; + return true; + } + int nargs = num_args(t); + for(int i = 0; i < nargs; i++) + if(get_store_array(arg(t,i),res)) + return true; + return false; + } + // translate a Z3 proof term into interpolating proof system Iproof::node translate_main(ast proof, bool expect_clause = true){ @@ -1448,6 +1473,21 @@ public: } } + /* this is the symmetry rule for ~=, that is, takes x ~= y and yields y ~= x. + the proof idiom uses commutativity, monotonicity and mp, but we replace it here + with symmtrey and resolution, that is, we prove y = x |- x = y, then resolve + with the proof of ~(x=y) to get ~y=x. */ + if(dk == PR_MODUS_PONENS && pr(prem(proof,1)) == PR_MONOTONICITY && pr(prem(prem(proof,1),0)) == PR_COMMUTATIVITY && num_prems(prem(proof,1)) == 1){ + Iproof::node ante = translate_main(prem(proof,0),false); + ast eq0 = arg(conc(prem(prem(proof,1),0)),0); + ast eq1 = arg(conc(prem(prem(proof,1),0)),1); + Iproof::node eq1hy = iproof->make_hypothesis(eq1); + Iproof::node eq0pf = iproof->make_symmetry(eq0,eq1,eq1hy); + std::vector clause; // just a dummy + res = iproof->make_resolution(eq0,clause,ante,eq0pf); + return res; + } + // translate all the premises std::vector args(nprems); for(unsigned i = 0; i < nprems; i++) @@ -1578,9 +1618,13 @@ public: throw unsupported(); } break; - case ArrayTheory: // nothing fancy for this - res = iproof->make_axiom(lits); + case ArrayTheory: {// nothing fancy for this + ast store_array; + if(!get_store_array(con,store_array)) + throw unsupported(); + res = iproof->make_axiom(lits,ast_scope(store_array)); break; + } default: throw unsupported(); } diff --git a/src/interp/iz3translate_direct.cpp b/src/interp/iz3translate_direct.cpp index 853ecbe86..4b7d47e0f 100755 --- a/src/interp/iz3translate_direct.cpp +++ b/src/interp/iz3translate_direct.cpp @@ -38,6 +38,24 @@ Revision History: using namespace stl_ext; #endif +#ifndef WIN32 + +/* This can introduce an address dependency if the range type of hash_map has + a destructor. Since the code in this file is not used and only here for + historical comparisons, we allow this non-determinism. + */ +namespace stl_ext { + template + class hash { + public: + size_t operator()(const T *p) const { + return (size_t) p; + } + }; +} + +#endif + static int lemma_count = 0; static int nll_lemma_count = 0; diff --git a/src/muz/duality/duality_dl_interface.cpp b/src/muz/duality/duality_dl_interface.cpp index 25dfcebbd..12dd4ff3e 100644 --- a/src/muz/duality/duality_dl_interface.cpp +++ b/src/muz/duality/duality_dl_interface.cpp @@ -472,7 +472,7 @@ static proof_ref extract_proof(dl_interface *d, Solver::Counterexample &cex) { expr conc = f(args); - ::vector pprems; + ::vector< ::proof *> pprems; for(unsigned i = 0; i < prems.size(); i++) pprems.push_back(prems[i].get()); diff --git a/src/smt/params/qi_params.cpp b/src/smt/params/qi_params.cpp index f5506d35b..60fcd6fc4 100644 --- a/src/smt/params/qi_params.cpp +++ b/src/smt/params/qi_params.cpp @@ -27,6 +27,7 @@ void qi_params::updt_params(params_ref const & _p) { m_mbqi_max_iterations = p.mbqi_max_iterations(); m_mbqi_trace = p.mbqi_trace(); m_mbqi_force_template = p.mbqi_force_template(); + m_mbqi_id = p.mbqi_id(); m_qi_profile = p.qi_profile(); m_qi_profile_freq = p.qi_profile_freq(); m_qi_max_instances = p.qi_max_instances(); diff --git a/src/smt/params/qi_params.h b/src/smt/params/qi_params.h index 0cd817f22..bca3ad3fc 100644 --- a/src/smt/params/qi_params.h +++ b/src/smt/params/qi_params.h @@ -51,6 +51,7 @@ struct qi_params { unsigned m_mbqi_max_iterations; bool m_mbqi_trace; unsigned m_mbqi_force_template; + const char * m_mbqi_id; qi_params(params_ref const & p = params_ref()): /* @@ -97,7 +98,9 @@ struct qi_params { m_mbqi_max_cexs_incr(1), m_mbqi_max_iterations(1000), m_mbqi_trace(false), - m_mbqi_force_template(10) { + m_mbqi_force_template(10), + m_mbqi_id(0) + { updt_params(p); } diff --git a/src/smt/params/smt_params_helper.pyg b/src/smt/params/smt_params_helper.pyg index 07c68f759..50bb6422b 100644 --- a/src/smt/params/smt_params_helper.pyg +++ b/src/smt/params/smt_params_helper.pyg @@ -21,6 +21,7 @@ def_module_params(module_name='smt', ('mbqi.max_iterations', UINT, 1000, 'maximum number of rounds of MBQI'), ('mbqi.trace', BOOL, False, 'generate tracing messages for Model Based Quantifier Instantiation (MBQI). It will display a message before every round of MBQI, and the quantifiers that were not satisfied'), ('mbqi.force_template', UINT, 10, 'some quantifiers can be used as templates for building interpretations for functions. Z3 uses heuristics to decide whether a quantifier will be used as a template or not. Quantifiers with weight >= mbqi.force_template are forced to be used as a template'), + ('mbqi.id', STRING, '', 'Only use model-based instantiation for quantifiers with id\'s beginning with string'), ('qi.profile', BOOL, False, 'profile quantifier instantiation'), ('qi.profile_freq', UINT, UINT_MAX, 'how frequent results are reported by qi.profile'), ('qi.max_instances', UINT, UINT_MAX, 'maximum number of quantifier instantiations'), diff --git a/src/smt/smt_model_checker.cpp b/src/smt/smt_model_checker.cpp index 53f3af961..526447f9f 100644 --- a/src/smt/smt_model_checker.cpp +++ b/src/smt/smt_model_checker.cpp @@ -322,6 +322,7 @@ namespace smt { for (; it != end; ++it) { quantifier * q = *it; + if(!m_qm->mbqi_enabled(q)) continue; if (m_context->is_relevant(q) && m_context->get_assignment(q) == l_true) { if (m_params.m_mbqi_trace && q->get_qid() != symbol::null) { verbose_stream() << "(smt.mbqi :checking " << q->get_qid() << ")\n"; diff --git a/src/smt/smt_quantifier.cpp b/src/smt/smt_quantifier.cpp index d56fe0cff..8fd0e08bc 100644 --- a/src/smt/smt_quantifier.cpp +++ b/src/smt/smt_quantifier.cpp @@ -335,6 +335,10 @@ namespace smt { return m_imp->m_plugin->model_based(); } + bool quantifier_manager::mbqi_enabled(quantifier *q) const { + return m_imp->m_plugin->mbqi_enabled(q); + } + void quantifier_manager::adjust_model(proto_model * m) { m_imp->m_plugin->adjust_model(m); } @@ -434,10 +438,24 @@ namespace smt { virtual bool model_based() const { return m_fparams->m_mbqi; } + virtual bool mbqi_enabled(quantifier *q) const { + if(!m_fparams->m_mbqi_id) return true; + const symbol &s = q->get_qid(); + unsigned len = strlen(m_fparams->m_mbqi_id); + if(s == symbol::null || s.is_numerical()) + return len == 0; + return strncmp(s.bare_str(),m_fparams->m_mbqi_id,len) == 0; + } + + /* Quantifier id's must begin with the prefix specified by + parameter mbqi.id to be instantiated with MBQI. The default + value is the empty string, so all quantifiers are + instantiated. + */ virtual void add(quantifier * q) { - if (m_fparams->m_mbqi) { - m_model_finder->register_quantifier(q); - } + if (m_fparams->m_mbqi && mbqi_enabled(q)) { + m_model_finder->register_quantifier(q); + } } virtual void del(quantifier * q) { diff --git a/src/smt/smt_quantifier.h b/src/smt/smt_quantifier.h index 19113229c..e3d626157 100644 --- a/src/smt/smt_quantifier.h +++ b/src/smt/smt_quantifier.h @@ -75,6 +75,7 @@ namespace smt { }; bool model_based() const; + bool mbqi_enabled(quantifier *q) const; // can mbqi instantiate this quantifier? void adjust_model(proto_model * m); check_model_result check_model(proto_model * m, obj_map const & root2value); @@ -144,6 +145,11 @@ namespace smt { */ virtual bool model_based() const = 0; + /** + \brief Is "model based" instantiate allowed to instantiate this quantifier? + */ + virtual bool mbqi_enabled(quantifier *q) const {return true;} + /** \brief Give a change to the plugin to adjust the interpretation of unintepreted functions. It can basically change the "else" of each uninterpreted function. diff --git a/src/smt/theory_arith_aux.h b/src/smt/theory_arith_aux.h index 9f77934e5..7593e9a52 100644 --- a/src/smt/theory_arith_aux.h +++ b/src/smt/theory_arith_aux.h @@ -475,10 +475,11 @@ namespace smt { bool theory_arith::all_coeff_int(row const & r) const { typename vector::const_iterator it = r.begin_entries(); typename vector::const_iterator end = r.end_entries(); - for (; it != end; ++it) { - if (!it->is_dead() && !it->m_coeff.is_int()) + for (; it != end; ++it) { + if (!it->is_dead() && !it->m_coeff.is_int()) { TRACE("gomory_cut", display_row(tout, r, true);); return false; + } } return true; } diff --git a/src/util/id_gen.h b/src/util/id_gen.h index b1713b524..c6d22246d 100644 --- a/src/util/id_gen.h +++ b/src/util/id_gen.h @@ -57,6 +57,11 @@ public: m_free_ids.finalize(); } + unsigned show_hash(){ + unsigned h = string_hash((char *)&m_free_ids[0],m_free_ids.size()*sizeof(unsigned),17); + return hash_u_u(h,m_next_id); + } + /** \brief Return N if the range of ids generated by this module is in the set [0..N) */