Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable

.gitattributes

@@ -1 +1,4 @@
+# Set default behaviour, in case users don't have core.autocrlf set.
+* text=auto
+
 src/api/dotnet/Properties/AssemblyInfo.cs text eol=crlf

src/duality/duality.h

@@ -118,7 +118,11 @@ protected:
       expr FinishAndOr(const std::vector<expr> &args, bool is_and);
       expr PullCommonFactors(std::vector<expr> &args, bool is_and);
       Term IneqToEqRec(hash_map<ast, Term> &memo, const Term &t);
-
+      Term CloneQuantAndSimp(const expr &t, const expr &body, bool is_forall);
+      Term PushQuantifier(const expr &t, const expr &body, bool is_forall);
+      void CollectJuncts(const Term &f, std::vector<Term> &lits, decl_kind op, bool negate);
+      Term DeleteBoundRec(hash_map<int,hash_map<ast,Term> > &memo, int level, int num, const Term &t);
+      Term DeleteBound(int level, int num, const Term &t);
 
 };
 

src/duality/duality_rpfp.cpp

@@ -548,24 +548,52 @@ namespace Duality {
       return foo;
   }
 
-  Z3User::Term Z3User::CloneQuantAndSimp(const expr &t, const expr &body){
-    if(t.is_quantifier_forall() && body.is_app() && body.decl().get_decl_kind() == And){
-      int nargs = body.num_args();
-      std::vector<expr> args(nargs);
-      for(int i = 0; i < nargs; i++)
-	args[i] = CloneQuantAndSimp(t, body.arg(i));
-      return ctx.make(And,args);
+  Z3User::Term Z3User::PushQuantifier(const expr &t, const expr &body, bool is_forall){
+    if(t.get_quantifier_num_bound() == 1){
+      std::vector<expr> fmlas,free,not_free;
+      CollectJuncts(body,fmlas, is_forall ? Or : And, false);
+      for(unsigned i = 0; i < fmlas.size(); i++){
+	const expr &fmla = fmlas[i];
+	if(fmla.has_free(0))
+	  free.push_back(fmla);
+	else
+	  not_free.push_back(fmla);
       }
-    if(!t.is_quantifier_forall() && body.is_app() && body.decl().get_decl_kind() == Or){
-      int nargs = body.num_args();
-      std::vector<expr> args(nargs);
-      for(int i = 0; i < nargs; i++)
-	args[i] = CloneQuantAndSimp(t, body.arg(i));
-      return ctx.make(Or,args);
+      decl_kind op = is_forall ? Or : And;
+      if(free.empty())
+	return SimplifyAndOr(not_free,op == And);
+      expr q = clone_quantifier(is_forall ? Forall : Exists,t, SimplifyAndOr(free, op == And));
+      if(!not_free.empty())
+	q = ctx.make(op,q,DeleteBound(0,1,SimplifyAndOr(not_free, op == And)));
+      return q;
     }
-    return clone_quantifier(t,body);
+    return clone_quantifier(is_forall ? Forall : Exists,t,body);
   }
 
+  Z3User::Term Z3User::CloneQuantAndSimp(const expr &t, const expr &body, bool is_forall){
+    if(body.is_app()){
+      if(body.decl().get_decl_kind() == (is_forall ? And : Or)){ // quantifier distributes
+	int nargs = body.num_args();
+	std::vector<expr> args(nargs);
+	for(int i = 0; i < nargs; i++)
+	  args[i] = CloneQuantAndSimp(t, body.arg(i), is_forall);
+	return SimplifyAndOr(args, body.decl().get_decl_kind() == And);
+      }
+      else if(body.decl().get_decl_kind() == (is_forall ? Or : And)){ // quantifier distributes
+	return PushQuantifier(t,body,is_forall); // may distribute partially
+      }
+      else if(body.decl().get_decl_kind() == Not){
+	return ctx.make(Not,CloneQuantAndSimp(t,body.arg(0),!is_forall));
+      }
+    }
+    if(t.get_quantifier_num_bound() == 1 && !body.has_free(0))
+      return DeleteBound(0,1,body); // drop the quantifier
+    return clone_quantifier(is_forall ? Forall : Exists,t,body);
+  }
+
+  Z3User::Term Z3User::CloneQuantAndSimp(const expr &t, const expr &body){
+    return CloneQuantAndSimp(t,body,t.is_quantifier_forall());
+  }
 
   Z3User::Term Z3User::SubstAtom(hash_map<ast, Term> &memo, const expr &t, const expr &atom, const expr &val){
     std::pair<ast,Term> foo(t,expr(ctx));
@@ -659,7 +687,7 @@ namespace Duality {
     else if (t.is_quantifier())
       {
 	Term body = RemoveRedundancyRec(memo,smemo,t.body());
-	res = clone_quantifier(t, body);
+	res = CloneQuantAndSimp(t, body);
       }
     else res = t;
     return res;
@@ -2468,6 +2496,20 @@ namespace Duality {
     }
   }
 
+  void Z3User::CollectJuncts(const Term &f, std::vector<Term> &lits, decl_kind op, bool negate){
+    if(f.is_app() && f.decl().get_decl_kind() == Not)
+      CollectJuncts(f.arg(0), lits, (op == And) ? Or : And, !negate);
+    else if(f.is_app() && f.decl().get_decl_kind() == op){
+      int num_args = f.num_args();
+      for(int i = 0; i < num_args; i++)
+	CollectJuncts(f.arg(i),lits,op,negate);
+    }
+    else {
+      expr junct = negate ? Negate(f) : f;
+      lits.push_back(junct);
+    }
+  }
+
   struct TermLt {
     bool operator()(const expr &x, const expr &y){
       unsigned xid = x.get_id();
@@ -3418,6 +3460,46 @@ namespace Duality {
     return SubstBoundRec(memo, subst, 0, t);
   }
 
+  // Eliminate the deBruijn indices from level to level+num-1
+  Z3User::Term Z3User::DeleteBoundRec(hash_map<int,hash_map<ast,Term> > &memo, int level, int num, const Term &t)
+  {
+    std::pair<ast,Term> foo(t,expr(ctx));
+    std::pair<hash_map<ast,Term>::iterator, bool> bar = memo[level].insert(foo);
+    Term &res = bar.first->second;
+    if(!bar.second) return res;
+    if (t.is_app())
+      {
+	func_decl f = t.decl();
+	std::vector<Term> args;
+	int nargs = t.num_args();
+	for(int i = 0; i < nargs; i++)
+	  args.push_back(DeleteBoundRec(memo, level, num, t.arg(i)));
+	res = f(args.size(),&args[0]);
+      }
+    else if (t.is_quantifier()){
+      int bound = t.get_quantifier_num_bound();
+      std::vector<expr> pats;
+      t.get_patterns(pats);
+      for(unsigned i = 0; i < pats.size(); i++)
+	pats[i] = DeleteBoundRec(memo, level + bound, num, pats[i]);
+      res = clone_quantifier(t, DeleteBoundRec(memo, level + bound, num, t.body()), pats);
+    }
+    else if (t.is_var()) {
+      int idx = t.get_index_value();
+      if(idx >= level){
+	res = ctx.make_var(idx-num,t.get_sort());
+      }
+      else res = t;
+    }
+    else res = t;
+    return res;
+  }
+  
+  Z3User::Term Z3User::DeleteBound(int level, int num, const Term &t){
+    hash_map<int,hash_map<ast,Term> > memo;
+    return DeleteBoundRec(memo, level, num, t);
+  }
+
   int Z3User::MaxIndex(hash_map<ast,int> &memo, const Term &t)
   {
     std::pair<ast,int> foo(t,-1);

src/duality/duality_wrapper.cpp

@@ -341,6 +341,12 @@ expr context::make_quant(decl_kind op, const std::vector<sort> &_sorts, const st
     return simplify(p);
   }
   
+  expr context::make_var(int idx, const sort &s){
+    ::sort * a = to_sort(s.raw());
+    return cook(m().mk_var(idx,a));
+  }
+
+
   expr expr::qe_lite() const {
     ::qe_lite qe(m());
     expr_ref result(to_expr(raw()),m());
@@ -374,6 +380,12 @@ expr context::make_quant(decl_kind op, const std::vector<sort> &_sorts, const st
     return q.ctx().cook(q.m().update_quantifier(thing, is_forall, num_patterns, &_patterns[0], to_expr(b.raw())));
   }
 
+  expr clone_quantifier(decl_kind dk, const expr &q, const expr &b){
+    quantifier *thing = to_quantifier(q.raw());
+    bool is_forall = dk == Forall;
+    return q.ctx().cook(q.m().update_quantifier(thing, is_forall, to_expr(b.raw())));
+  }
+
   void expr::get_patterns(std::vector<expr> &pats) const {
     quantifier *thing = to_quantifier(raw());
     unsigned num_patterns = thing->get_num_patterns();

src/duality/duality_wrapper.h

@@ -238,7 +238,7 @@ namespace Duality {
 
       expr make_quant(decl_kind op, const std::vector<expr> &bvs, const expr &body);
       expr make_quant(decl_kind op, const std::vector<sort> &_sorts, const std::vector<symbol> &_names, const expr &body);
-
+      expr make_var(int idx, const sort &s);
 
       decl_kind get_decl_kind(const func_decl &t);
 
@@ -466,6 +466,16 @@ namespace Duality {
 	bool is_label (bool &pos,std::vector<symbol> &names) const ;
 	bool is_ground() const {return to_app(raw())->is_ground();}
 	bool has_quantifiers() const {return to_app(raw())->has_quantifiers();}
+	bool has_free(int idx) const {
+	  used_vars proc;
+	  proc.process(to_expr(raw()));
+	  return proc.contains(idx);
+	}
+	unsigned get_max_var_idx_plus_1() const {
+	  used_vars proc;
+	  proc.process(to_expr(raw()));
+	  return proc.get_max_found_var_idx_plus_1();
+	}
 
         // operator Z3_app() const { assert(is_app()); return reinterpret_cast<Z3_app>(m_ast); }
         func_decl decl() const {return func_decl(ctx(),to_app(raw())->get_decl());}
@@ -573,6 +583,8 @@ namespace Duality {
 
         friend expr clone_quantifier(const expr &q, const expr &b, const std::vector<expr> &patterns);
 
+	friend expr clone_quantifier(decl_kind, const expr &, const expr &);
+
         friend std::ostream & operator<<(std::ostream & out, expr const & m){
 	  m.ctx().print_expr(out,m);
 	  return out;

src/interp/iz3hash.h

@@ -464,7 +464,9 @@ namespace hash_space {
 
       Value &operator[](const Key& key) {
 	std::pair<Key,Value> kvp(key,Value());
-	return lookup(kvp,true)->val.second;
+	return 
+	hashtable<std::pair<Key,Value>,Key,HashFun,proj1<Key,Value>,EqFun>::
+         lookup(kvp,true)->val.second;
       }
   };
 

src/interp/iz3proof_itp.cpp

@@ -814,6 +814,10 @@ 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
+	if(!rewrites_from_to(equa,lhs,rhs)){
+	  lhs = arg(arg(neg_equality,0),0); // the equality proved is ambiguous, sadly
+	  rhs = arg(arg(neg_equality,0),1);
+	}
 	LitType lhst = get_term_type(lhs), rhst = get_term_type(rhs);
 	if(lhst != LitMixed && rhst != LitMixed)
 	  return unmixed_eq2ineq(lhs, rhs, op(arg(neg_equality,0)), equa, cond);
@@ -1671,9 +1675,20 @@ class iz3proof_itp_impl : public iz3proof_itp {
     return head;
   }
 
-  // split a rewrite chain into head and tail at last non-mixed term
+  bool has_mixed_summands(const ast &e){
+    if(op(e) == Plus){
+      int nargs = num_args(e);
+      for(int i = 0; i < nargs; i++)
+	if(has_mixed_summands(arg(e,i)))
+	  return true;
+      return false;
+    }
+    return get_term_type(e) == LitMixed;
+  }
+  
+  // split a rewrite chain into head and tail at last sum with no mixed sumands
   ast get_right_movers(const ast &chain, const ast &rhs, ast &tail, ast &mid){
-    if(is_true(chain) || get_term_type(rhs) != LitMixed){
+    if(is_true(chain) || !has_mixed_summands(rhs)){
       mid = rhs;
       tail = mk_true();
       return chain;
@@ -1686,11 +1701,11 @@ class iz3proof_itp_impl : public iz3proof_itp {
     return res;
   }
   
-  // split a rewrite chain into head and tail at first non-mixed term
+  // split a rewrite chain into head and tail at first sum with no mixed sumands
   ast get_left_movers(const ast &chain, const ast &lhs, ast &tail, ast &mid){
     if(is_true(chain)){
       mid = lhs; 
-      if(get_term_type(lhs) != LitMixed){
+      if(!has_mixed_summands(lhs)){
 	tail = mk_true();
 	return chain;
       }
@@ -1790,10 +1805,21 @@ class iz3proof_itp_impl : public iz3proof_itp {
   }
 
 
+  bool rewrites_from_to(const ast &chain, const ast &lhs, const ast &rhs){
+    if(is_true(chain))
+      return lhs == rhs;
+    ast last = chain_last(chain);
+    ast rest = chain_rest(chain);
+    ast mid = subst_in_pos(rhs,rewrite_pos(last),rewrite_lhs(last));
+    return rewrites_from_to(rest,lhs,mid);
+  }
+
+  struct bad_ineq_inference {};
+
   ast chain_ineqs(opr comp_op, LitType t, const ast &chain, const ast &lhs, const ast &rhs){
     if(is_true(chain)){
       if(lhs != rhs)
-	throw "bad ineq inference";
+	throw bad_ineq_inference();
       return make(Leq,make_int(rational(0)),make_int(rational(0)));
     }
     ast last = chain_last(chain);
@@ -2656,9 +2682,11 @@ class iz3proof_itp_impl : public iz3proof_itp {
     pf = make_refl(e);  // proof that e = e
 
     prover::range erng = pv->ast_scope(e);
+#if 0
     if(!(erng.lo > erng.hi) && pv->ranges_intersect(pv->ast_scope(e),rng)){
       return e; // this term occurs in range, so it's O.K.
     }
+#endif
 
     hash_map<ast,ast>::iterator it = localization_map.find(e);