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

src/api/dotnet/Readme.NET35

@@ -0,0 +1,9 @@
+The default Z3 bindings for .NET are built for the .NET framework version 4.
+Should the need arise, it is also possible to build them for .NET 3.5; the
+instructions are as follows:
+
+In the project properties of Microsoft.Z3.csproj:
+- Under 'Application': Change Target framework to .NET Framework 3.5
+- Under 'Build': Add FRAMEWORK_LT_4 to the condidional compilation symbols
+- Remove the reference to System.Numerics
+- Install the NuGet Package "Microsoft Code Contracts for Net3.5"

src/api/python/z3.py

@@ -6166,7 +6166,7 @@ class Fixedpoint(Z3PPObject):
             Z3_fixedpoint_add_rule(self.ctx.ref(), self.fixedpoint, head.as_ast(), name)            
         else:
             body = _get_args(body)
-            f    = self.abstract(Implies(And(body),head))
+            f    = self.abstract(Implies(And(body, self.ctx),head))
             Z3_fixedpoint_add_rule(self.ctx.ref(), self.fixedpoint, f.as_ast(), name)
         
     def rule(self, head, body = None, name = None):
@@ -6194,7 +6194,7 @@ class Fixedpoint(Z3PPObject):
             if sz == 1:
                 query = query[0]
             else:
-                query = And(query)
+                query = And(query, self.ctx)
             query = self.abstract(query, False)
             r = Z3_fixedpoint_query(self.ctx.ref(), self.fixedpoint, query.as_ast())
         return CheckSatResult(r)
@@ -6213,7 +6213,7 @@ class Fixedpoint(Z3PPObject):
             name = ""
         name = to_symbol(name, self.ctx)
         body = _get_args(body)
-        f    = self.abstract(Implies(And(body),head))
+        f    = self.abstract(Implies(And(body, self.ctx),head))
         Z3_fixedpoint_update_rule(self.ctx.ref(), self.fixedpoint, f.as_ast(), name)
 
     def get_answer(self):       

src/ast/ast.cpp

@@ -1013,6 +1013,17 @@ func_decl * basic_decl_plugin::mk_ite_decl(sort * s) {
     return m_ite_decls[id];
 }
 
+sort* basic_decl_plugin::join(sort* s1, sort* s2) {
+    if (s1 == s2) return s1;
+    if (s1->get_family_id() == m_manager->m_arith_family_id && 
+        s2->get_family_id() == m_manager->m_arith_family_id) {
+        if (s1->get_decl_kind() == REAL_SORT) {
+            return s1;
+        }
+    }
+    return s2;
+}
+
 func_decl * basic_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters,
                                           unsigned arity, sort * const * domain, sort * range) {
     switch (static_cast<basic_op_kind>(k)) {
@@ -1025,10 +1036,10 @@ func_decl * basic_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters
     case OP_IFF:     return m_iff_decl;
     case OP_IMPLIES: return m_implies_decl;
     case OP_XOR:     return m_xor_decl;
-    case OP_ITE:     return arity == 3 ? mk_ite_decl(domain[1]) : 0;
+    case OP_ITE:     return arity == 3 ? mk_ite_decl(join(domain[1], domain[2])) : 0;
         // eq and oeq must have at least two arguments, they can have more since they are chainable
-    case OP_EQ:      return arity >= 2 ? mk_eq_decl_core("=", OP_EQ, domain[0], m_eq_decls) : 0;
+    case OP_EQ:      return arity >= 2 ? mk_eq_decl_core("=", OP_EQ, join(domain[0],domain[1]), m_eq_decls) : 0;
-    case OP_OEQ:     return arity >= 2 ? mk_eq_decl_core("~", OP_OEQ, domain[0], m_oeq_decls) : 0;
+    case OP_OEQ:     return arity >= 2 ? mk_eq_decl_core("~", OP_OEQ, join(domain[0],domain[1]), m_oeq_decls) : 0;
     case OP_DISTINCT: {
         func_decl_info info(m_family_id, OP_DISTINCT);
         info.set_pairwise();
@@ -1061,10 +1072,12 @@ func_decl * basic_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters
     case OP_IFF:     return m_iff_decl;
     case OP_IMPLIES: return m_implies_decl;
     case OP_XOR:     return m_xor_decl;
-    case OP_ITE:     return num_args == 3 ? mk_ite_decl(m_manager->get_sort(args[1])): 0;
+    case OP_ITE:     return num_args == 3 ? mk_ite_decl(join(m_manager->get_sort(args[1]), m_manager->get_sort(args[2]))): 0;
         // eq and oeq must have at least two arguments, they can have more since they are chainable
-    case OP_EQ:      return num_args >= 2 ? mk_eq_decl_core("=", OP_EQ, m_manager->get_sort(args[0]), m_eq_decls) : 0;
+    case OP_EQ:      return num_args >= 2 ? mk_eq_decl_core("=", OP_EQ, join(m_manager->get_sort(args[0]),
-    case OP_OEQ:     return num_args >= 2 ? mk_eq_decl_core("~", OP_OEQ, m_manager->get_sort(args[0]), m_oeq_decls) : 0;
+                                                                             m_manager->get_sort(args[1])), m_eq_decls) : 0;
+    case OP_OEQ:     return num_args >= 2 ? mk_eq_decl_core("~", OP_OEQ, join(m_manager->get_sort(args[0]),
+                                                                              m_manager->get_sort(args[1])), m_oeq_decls) : 0;
     case OP_DISTINCT:
         return decl_plugin::mk_func_decl(k, num_parameters, parameters, num_args, args, range);
     default:

src/ast/ast.h

@@ -1100,6 +1100,7 @@ protected:
     virtual void set_manager(ast_manager * m, family_id id);
     func_decl * mk_eq_decl_core(char const * name, decl_kind k, sort * s, ptr_vector<func_decl> & cache);
     func_decl * mk_ite_decl(sort * s);
+    sort* join(sort* s1, sort* s2);
 public:
     basic_decl_plugin();
     
@@ -1378,7 +1379,7 @@ enum proof_gen_mode {
 // -----------------------------------
 
 class ast_manager {
-protected:
+    friend class basic_decl_plugin;
 protected:
     struct config {
         typedef ast_manager              value_manager;

src/duality/duality.h

@@ -778,6 +778,10 @@ protected:
       struct Bad {
       };
       
+      // thrown on more serious internal error
+      struct ReallyBad {
+      };
+
       /** Pop a scope (see Push). Note, you cannot pop axioms. */
       
       void Pop(int num_scopes);

src/duality/duality_rpfp.cpp

@@ -2643,6 +2643,10 @@ namespace Duality {
 	GetGroundLitsUnderQuants(memo,f.body(),res,1);
       return;
     }
+    if(f.is_var()){
+      //      std::cout << "foo!\n";
+      return;
+    }
     if(under && f.is_ground())
       res.push_back(f);
   }
@@ -3065,10 +3069,14 @@ namespace Duality {
     node->Annotation.SetEmpty();
     hash_set<ast> *core = new hash_set<ast>;
     core->insert(node->Outgoing->dual);
+    expr prev_annot = ctx.bool_val(false);
+    expr prev_impl = ctx.bool_val(false);
+    int repeated_case_count = 0;
     while(1){
       by_case_counter++;
       is.push();
       expr annot = !GetAnnotation(node);
+      Transformer old_annot = node->Annotation;
       is.add(annot);
       if(is.check() == unsat){
 	is.pop(1);
@@ -3076,12 +3084,25 @@ namespace Duality {
       }
       is.pop(1);
       Push();
-      ConstrainEdgeLocalized(node->Outgoing,is.get_implicant());
+      expr the_impl = is.get_implicant();
+      if(eq(the_impl,prev_impl)){
+	//	std::cout << "got old implicant\n";
+	repeated_case_count++;
+      }
+      prev_impl = the_impl;
+      ConstrainEdgeLocalized(node->Outgoing,the_impl);
       ConstrainEdgeLocalized(node->Outgoing,!GetAnnotation(node)); //TODO: need this?
+      
+      {
 	check_result foo = Check(root);
 	if(foo != unsat){
-	slvr().print("should_be_unsat.smt2");
+	  Pop(1);
-	throw "should be unsat";
+	  is.pop(1);
+	  delete core;
+	  timer_stop("InterpolateByCases");
+	  throw ReallyBad();
+	  // slvr().print("should_be_unsat.smt2");
+	  // throw "should be unsat";
 	}
 	std::vector<expr> assumps, axioms_to_add;
 	slvr().get_proof().get_assumptions(assumps);
@@ -3093,7 +3114,6 @@ namespace Duality {
 	  }
 	}
 	// AddToProofCore(*core);
-      Transformer old_annot = node->Annotation;
 	SolveSingleNode(root,node);
 
 	{
@@ -3124,8 +3144,10 @@ namespace Duality {
 	  bad_count++;
 	}
 #endif
+      }
 
-      if(node->Annotation.IsEmpty()){
+      if(node->Annotation.IsEmpty() || eq(node->Annotation.Formula,prev_annot) || (repeated_case_count > 0 && !axioms_added) || (repeated_case_count >= 10)){
+      looks_bad:
 	if(!axioms_added){
 	  // add the axioms in the off chance they are useful
 	  const std::vector<expr> &theory = ls->get_axioms();
@@ -3134,6 +3156,7 @@ namespace Duality {
 	  axioms_added = true;
 	}
 	else {
+	  //#define KILL_ON_BAD_INTERPOLANT	  
 #ifdef KILL_ON_BAD_INTERPOLANT	  
 	  std::cout << "bad in InterpolateByCase -- core:\n";
 #if 0
@@ -3175,10 +3198,11 @@ namespace Duality {
 	  is.pop(1);
 	  delete core;
 	  timer_stop("InterpolateByCases");
-	  throw Bad();
+	  throw ReallyBad();
 	}
       }
       Pop(1);
+      prev_annot = node->Annotation.Formula;
       node->Annotation.UnionWith(old_annot);
     }
     if(proof_core)

src/duality/duality_solver.cpp

@@ -2279,6 +2279,18 @@ namespace Duality {
 		  // bad interpolants can get us here
 		  throw DoRestart();
 		}
+		catch(const RPFP::ReallyBad &){
+		  // this could be caused by incompleteness
+		  for(unsigned i = 0; i < expansions.size(); i++){
+		    Node *node = expansions[i];
+		    node->map->Annotation.SetFull();
+		    std::vector<Node *> &chs = node->map->Outgoing->Children;
+		    for(unsigned j = 0; j < chs.size(); j++)
+		      chs[j]->Annotation.SetFull();
+		    reporter->Message("incompleteness: cleared annotation and child annotations");
+		  }
+		  throw DoRestart();
+		}
 		catch(char const *msg){
 		  // bad interpolants can get us here
 		  reporter->Message(std::string("interpolation failure:") + msg);

src/interp/iz3mgr.cpp

@@ -778,6 +778,8 @@ int iz3mgr::occurs_in(ast var, ast e){
 
 
 bool iz3mgr::solve_arith(const ast &v, const ast &x, const ast &y, ast &res){
+  if(occurs_in(v,y))
+    return false;
   if(op(x) == Plus){
     int n = num_args(x);
     for(int i = 0; i < n; i++){
@@ -801,8 +803,8 @@ iz3mgr::ast iz3mgr::cont_eq(stl_ext::hash_set<ast> &cont_eq_memo, bool truth, as
     return ast();
   cont_eq_memo.insert(e);
   if(!truth && op(e) == Equal){
-    if(arg(e,0) == v) return(arg(e,1));
+    if(arg(e,0) == v && !occurs_in(v,arg(e,1))) return(arg(e,1));
-    if(arg(e,1) == v) return(arg(e,0));
+    if(arg(e,1) == v && !occurs_in(v,arg(e,0))) 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;

src/interp/iz3mgr.h

@@ -278,7 +278,8 @@ class iz3mgr  {
   }
 
   symb sym(ast t){
-    return to_app(t.raw())->get_decl();
+    raw_ast *_ast = t.raw();
+    return is_app(_ast) ? to_app(_ast)->get_decl() : 0;
   }
 
   std::string string_of_symbol(symb s){

src/interp/iz3proof_itp.cpp

@@ -1027,7 +1027,7 @@ class iz3proof_itp_impl : public iz3proof_itp {
 	linear_comb(Aineqs,coeff,make(Leq,make_int(rational(0)),make(Sub,term2,term1)));
     }
     else {
-      ast pf = extract_rewrites(make(concat,mk_true(),rest),p1);
+      ast pf = extract_rewrites(make(concat,mk_true(),last),p1);
       ast new_normal = fix_normal(term1,term2,pf);
       normals = merge_normal_chains(normals,cons_normal(new_normal,mk_true()), Aproves, Bproves);
     }

src/interp/iz3translate.cpp

@@ -1712,11 +1712,17 @@ public:
 	std::cout << "foo!\n";
 
       // no idea why this shows up
-      if(dk == PR_MODUS_PONENS_OEQ)
+      if(dk == PR_MODUS_PONENS_OEQ){
 	if(conc(prem(proof,0)) == con){
 	  res = translate_main(prem(proof,0),expect_clause);
 	  return res;
 	}
+	if(expect_clause && op(con) == Or){ // skolemization does this
+	  Iproof::node clause = translate_main(prem(proof,0),true);
+	  res = RewriteClause(clause,prem(proof,1));
+	  return res;
+	}
+      }
       
 #if 0
       if(1 && dk == PR_TRANSITIVITY && pr(prem(proof,1)) == PR_COMMUTATIVITY){
@@ -1800,7 +1806,9 @@ public:
 	}
 	break;
       }
-      case PR_MONOTONICITY: {
+      case PR_QUANT_INTRO:
+      case PR_MONOTONICITY:
+	{
 	std::vector<ast> eqs; eqs.resize(args.size());
 	for(unsigned i = 0; i < args.size(); i++)
 	  eqs[i] = conc(prem(proof,i));

src/tactic/bv/bv_size_reduction_tactic.cpp

@@ -151,7 +151,7 @@ struct bv_size_reduction_tactic::imp {
                             // bound is infeasible.
                         } 
                         else {
-                            update_signed_upper(to_app(lhs), val);
+                            update_signed_upper(to_app(rhs), val);
                         }                        
                     }
                     else update_signed_lower(to_app(rhs), val);
@@ -229,17 +229,35 @@ struct bv_size_reduction_tactic::imp {
                         else {
                             // l < u
                             if (l.is_neg()) {
-                                unsigned i_nb = (u - l).get_num_bits();
+                                unsigned l_nb = (-l).get_num_bits();
                                 unsigned v_nb = m_util.get_bv_size(v);
+
+                                if (u.is_neg())
+                                {
+                                    // l <= v <= u <= 0
+                                    unsigned i_nb = l_nb;
+                                    TRACE("bv_size_reduction", tout << " l <= " << v->get_decl()->get_name() << " <= u <= 0 " << " --> " << i_nb << " bits\n";);
+                                    if (i_nb < v_nb) {
+                                        new_const = m.mk_fresh_const(0, m_util.mk_sort(i_nb));
+                                        new_def = m_util.mk_concat(m_util.mk_numeral(numeral(-1), v_nb - i_nb), new_const);
+                                    }
+                                }
+                                else {
+                                    // l <= v <= 0 <= u
+                                    unsigned u_nb = u.get_num_bits();
+                                    unsigned i_nb = ((l_nb > u_nb) ? l_nb : u_nb) + 1;
+                                    TRACE("bv_size_reduction", tout << " l <= " << v->get_decl()->get_name() << " <= 0 <= u " << " --> " << i_nb << " bits\n";);
                                     if (i_nb < v_nb) {
                                         new_const = m.mk_fresh_const(0, m_util.mk_sort(i_nb));
                                         new_def = m_util.mk_sign_extend(v_nb - i_nb, new_const);
                                     }
                                 }
+                            }
                             else {
                                 // 0 <= l <= v <= u
                                 unsigned u_nb = u.get_num_bits();
                                 unsigned v_nb = m_util.get_bv_size(v);
+                                TRACE("bv_size_reduction", tout << l << " <= " << v->get_decl()->get_name() << " <= " << u << " --> " << u_nb << " bits\n";);
                                 if (u_nb < v_nb) {
                                     new_const = m.mk_fresh_const(0, m_util.mk_sort(u_nb));
                                     new_def = m_util.mk_concat(m_util.mk_numeral(numeral(0), v_nb - u_nb), new_const);