some interpolation fixes, plus some options to remove features for testing in duality

src/duality/duality_solver.cpp

@@ -44,12 +44,17 @@ Revision History:
 // #define TOP_DOWN
 // #define EFFORT_BOUNDED_STRAT
 #define SKIP_UNDERAPPROX_NODES
-#define USE_RPFP_CLONE
 // #define KEEP_EXPANSIONS
 // #define USE_CACHING_RPFP
 // #define PROPAGATE_BEFORE_CHECK
+
+#define USE_RPFP_CLONE
 #define USE_NEW_GEN_CANDS
 
+//#define NO_PROPAGATE
+//#define NO_GENERALIZE
+//#define NO_DECISIONS
+
 namespace Duality {
 
   // TODO: must be a better place for this...
@@ -1933,11 +1938,15 @@ namespace Duality {
 	      for(unsigned i = 0; i < expansions.size(); i++){
 		Node *node = expansions[i];
 		tree->SolveSingleNode(top,node);
+#ifdef NO_GENERALIZE
+		node->Annotation.Formula = tree->RemoveRedundancy(node->Annotation.Formula).simplify();
+#else
 		if(expansions.size() == 1 && NodeTooComplicated(node))
 		  SimplifyNode(node);
 		else
 		  node->Annotation.Formula = tree->RemoveRedundancy(node->Annotation.Formula).simplify();
 		Generalize(node);
+#endif
 		if(RecordUpdate(node))
 		  update_count++;
 		else
@@ -1977,7 +1986,9 @@ namespace Duality {
 	      if(stack.size() == 1)break;
 	      if(prev_level_used){
 		Node *node = stack.back().expansions[0];
+#ifndef NO_PROPAGATE
 		if(!Propagate(node)) break;
+#endif
 		if(!RecordUpdate(node)) break; // shouldn't happen!
 		RemoveUpdateNodesAtCurrentLevel(); // this level is about to be deleted -- remove its children from update list
 		propagated = true;
@@ -2001,9 +2012,11 @@ namespace Duality {
 	    was_sat = true;
 	    tree->Push();
 	    std::vector<Node *> &expansions = stack.back().expansions;
+#ifndef NO_DECISIONS
 	    for(unsigned i = 0; i < expansions.size(); i++){
 	      tree->FixCurrentState(expansions[i]->Outgoing);
 	    }
+#endif
 #if 0
 	    if(tree->slvr().check() == unsat)
 	      throw "help!";

src/interp/iz3mgr.cpp

@@ -684,10 +684,13 @@ void iz3mgr::linear_comb(ast &P, const ast &c, const ast &Q, bool round_off){
       throw "not an inequality";
     }
   }
-  Qrhs = make(Times,c,Qrhs);
+  bool pstrict = op(P) == Lt;
-  bool pstrict = op(P) == Lt, strict = pstrict || qstrict;
+  if(qstrict && round_off && (pstrict || !(c == make_int(rational(1))))){
-  if(pstrict && qstrict && round_off)
     Qrhs = make(Sub,Qrhs,make_int(rational(1)));
+    qstrict = false;
+  }
+  Qrhs = make(Times,c,Qrhs);
+  bool strict = pstrict || qstrict;
   if(strict)
     P = make(Lt,arg(P,0),make(Plus,arg(P,1),Qrhs));
   else

src/interp/iz3proof_itp.cpp

@@ -677,8 +677,11 @@ class iz3proof_itp_impl : public iz3proof_itp {
   }
   
   ast rotate_sum_rec(const ast &pl, const ast &pf, ast &Bproves, ast &ineq){
-    if(pf == pl)
+    if(pf == pl){
+      if(sym(ineq) == normal)
+	return my_implies(Bproves,ineq);
       return my_implies(Bproves,simplify_ineq(ineq));
+    }
     if(op(pf) == Uninterpreted && sym(pf) == sum){
       if(arg(pf,2) == pl){
 	ast Aproves = mk_true();
@@ -829,6 +832,8 @@ class iz3proof_itp_impl : public iz3proof_itp {
     ast equa = sep_cond(args[0],cond);
     if(is_equivrel_chain(equa))
       return my_implies(cond,reverse_chain(equa));
+    if(is_negation_chain(equa))
+      return commute_negation_chain(equa);
     throw cannot_simplify();
   }
 
@@ -1443,6 +1448,50 @@ class iz3proof_itp_impl : public iz3proof_itp {
     return is_negation_chain(rest);
   }
 
+  ast commute_negation_chain(const ast &chain){
+    if(is_true(chain))
+      return chain;
+    ast last = chain_last(chain);
+    ast rest = chain_rest(chain);
+    if(is_true(rest)){
+      ast old = rewrite_rhs(last);
+      if(!(op(old) == Not))
+	throw "bad negative equality chain";
+      ast equ = arg(old,0);
+      if(!is_equivrel(equ))
+	throw "bad negative equality chain";
+      last = rewrite_update_rhs(last,top_pos,make(Not,make(op(equ),arg(equ,1),arg(equ,0))),make(True));
+      return chain_cons(rest,last);
+    }
+    ast pos = rewrite_pos(last);
+    if(pos == top_pos)
+      throw "bad negative equality chain";
+    int idx = pos_arg(pos);
+    if(idx != 0)
+      throw "bad negative equality chain";
+    pos = arg(pos,1);
+    if(pos == top_pos){
+      ast lhs = rewrite_lhs(last);
+      ast rhs = rewrite_rhs(last);
+      if(op(lhs) != Equal || op(rhs) != Equal)
+	throw "bad negative equality chain";
+      last = make_rewrite(rewrite_side(last),rewrite_pos(last),rewrite_cond(last),
+			  make(Iff,make(Equal,arg(lhs,1),arg(lhs,0)),make(Equal,arg(rhs,1),arg(rhs,0))));
+    }
+    else {
+      idx = pos_arg(pos);
+      if(idx == 0)
+	idx = 1;
+      else if(idx == 1)
+	idx = 0;
+      else
+	throw "bad negative equality chain";
+      pos = pos_add(0,pos_add(idx,arg(pos,1)));
+      last = make_rewrite(rewrite_side(last),pos,rewrite_cond(last),rewrite_equ(last));
+    }
+    return chain_cons(commute_negation_chain(rest),last);
+  }
+
   // split a rewrite chain into head and tail at last top-level rewrite
   ast get_head_chain(const ast &chain, ast &tail, bool is_not = true){
     ast last = chain_last(chain);
@@ -2240,10 +2289,19 @@ class iz3proof_itp_impl : public iz3proof_itp {
 	throw proof_error();
       }
     }
-    Qrhs = make(Times,c,Qrhs);
+#if 0
     bool pstrict = op(P) == Lt, strict = pstrict || qstrict;
     if(pstrict && qstrict && round_off)
       Qrhs = make(Sub,Qrhs,make_int(rational(1)));
+#else
+    bool pstrict = op(P) == Lt;
+    if(qstrict && round_off && (pstrict || !(c == make_int(rational(1))))){
+      Qrhs = make(Sub,Qrhs,make_int(rational(1)));
+      qstrict = false;
+    }
+    Qrhs = make(Times,c,Qrhs);
+    bool strict = pstrict || qstrict;
+#endif
     if(strict)
       P = make(Lt,arg(P,0),make(Plus,arg(P,1),Qrhs));
     else
@@ -2427,7 +2485,7 @@ class iz3proof_itp_impl : public iz3proof_itp {
       return e; // this term occurs in range, so it's O.K.
 
     if(is_array_type(get_type(e)))
-      throw "help!";
+      std::cerr << "WARNING: array quantifier\n";
 
     // choose a frame for the constraint that is close to range
     int frame = pv->range_near(pv->ast_scope(e),rng);

src/interp/iz3translate.cpp

@@ -181,6 +181,13 @@ public:
       get_Z3_lits(con, lits);
       iproof->make_axiom(lits);
     }
+    else if(dk == PR_MODUS_PONENS && pr(prem(proof,0)) == PR_QUANT_INST
+	    && get_locality_rec(prem(proof,1)) == INT_MAX){
+      std::vector<ast> lits;
+      ast con = conc(proof);
+      get_Z3_lits(con, lits);
+      iproof->make_axiom(lits);
+    }
     else {
       unsigned nprems = num_prems(proof);
       for(unsigned i = 0; i < nprems; i++){
@@ -1264,6 +1271,84 @@ public:
     return make(Plus,args);
   }
 
+
+  ast replace_summands_with_fresh_vars(const ast &t, hash_map<ast,ast> &map){
+    if(op(t) == Plus){
+      int nargs = num_args(t);
+      std::vector<ast> args(nargs);
+      for(int i = 0; i < nargs; i++)
+	args[i] = replace_summands_with_fresh_vars(arg(t,i),map);
+      return make(Plus,args);
+    }
+    if(op(t) == Times)
+      return make(Times,arg(t,0),replace_summands_with_fresh_vars(arg(t,1),map));
+    if(map.find(t) == map.end())
+      map[t] =  mk_fresh_constant("@s",get_type(t));
+    return map[t];
+  }
+
+  ast painfully_normalize_ineq(const ast &ineq, hash_map<ast,ast> &map){
+    ast res = normalize_inequality(ineq);
+    ast lhs = arg(res,0);
+    lhs = replace_summands_with_fresh_vars(lhs,map);
+    res = make(op(res),SortSum(lhs),arg(res,1));
+    return res;
+  }
+
+  Iproof::node painfully_reconstruct_farkas(const std::vector<ast> &prems, const std::vector<Iproof::node> &pfs, const ast &con){
+    int nprems = prems.size();
+    std::vector<ast> pcons(nprems),npcons(nprems);
+    hash_map<ast,ast> pcon_to_pf, npcon_to_pcon, pain_map;
+    for(int i = 0; i < nprems; i++){
+      pcons[i] = conc(prems[i]);
+      npcons[i] = painfully_normalize_ineq(pcons[i],pain_map);
+      pcon_to_pf[npcons[i]] = pfs[i];
+      npcon_to_pcon[npcons[i]] = pcons[i];
+    }
+    // ast leq = make(Leq,arg(con,0),arg(con,1));
+    ast ncon = painfully_normalize_ineq(mk_not(con),pain_map);
+    pcons.push_back(mk_not(con));
+    npcons.push_back(ncon);
+    // ast assumps = make(And,pcons);
+    ast new_proof;
+    if(is_sat(npcons,new_proof))
+      throw "Proof error!";
+    pfrule dk = pr(new_proof);
+    int nnp = num_prems(new_proof);
+    std::vector<Iproof::node> my_prems;
+    std::vector<ast> farkas_coeffs, my_pcons;
+
+    if(dk == PR_TH_LEMMA 
+       && get_theory_lemma_theory(new_proof) == ArithTheory
+       && get_theory_lemma_kind(new_proof) == FarkasKind)
+      get_farkas_coeffs(new_proof,farkas_coeffs);
+    else if(dk == PR_UNIT_RESOLUTION && nnp == 2){
+      for(int i = 0; i < nprems; i++)
+	farkas_coeffs.push_back(make_int(rational(1)));
+    }
+    else
+      throw "cannot reconstruct farkas proof";
+
+    for(int i = 0; i < nnp; i++){
+      ast p = conc(prem(new_proof,i));
+      p = really_normalize_ineq(p);
+      if(pcon_to_pf.find(p) != pcon_to_pf.end()){
+	my_prems.push_back(pcon_to_pf[p]);
+	my_pcons.push_back(npcon_to_pcon[p]);
+      }
+      else if(p == ncon){
+	my_prems.push_back(iproof->make_hypothesis(mk_not(con)));
+	my_pcons.push_back(mk_not(con));
+      }
+      else
+	throw "cannot reconstruct farkas proof";
+    }
+    Iproof::node res = iproof->make_farkas(mk_false(),my_prems,my_pcons,farkas_coeffs);
+    return res;
+  }
+
+
+
   ast really_normalize_ineq(const ast &ineq){
     ast res = normalize_inequality(ineq);
     res = make(op(res),SortSum(arg(res,0)),arg(res,1));
@@ -1302,7 +1387,7 @@ public:
 	farkas_coeffs.push_back(make_int(rational(1)));
     }
     else
-      throw "cannot reconstruct farkas proof";
+      return painfully_reconstruct_farkas(prems,pfs,con);
 
     for(int i = 0; i < nnp; i++){
       ast p = conc(prem(new_proof,i));
@@ -1445,10 +1530,12 @@ public:
 	lits.push_back(from_ast(con));
 
       // pattern match some idioms
-      if(dk == PR_MODUS_PONENS && pr(prem(proof,0)) == PR_QUANT_INST && pr(prem(proof,1)) == PR_REWRITE ) {
+      if(dk == PR_MODUS_PONENS && pr(prem(proof,0)) == PR_QUANT_INST){
+	if(get_locality_rec(prem(proof,1)) == INT_MAX) {
 	  res = iproof->make_axiom(lits);
 	  return res;
 	}
+      }
       if(dk == PR_MODUS_PONENS && expect_clause && op(con) == Or){
 	Iproof::node clause = translate_main(prem(proof,0),true);
 	res = RewriteClause(clause,prem(proof,1));
@@ -1620,9 +1707,10 @@ public:
 	  break;
 	case ArrayTheory: {// nothing fancy for this
 	  ast store_array;
-	  if(!get_store_array(con,store_array))
+	  if(get_store_array(con,store_array))
-	    throw unsupported();
 	    res = iproof->make_axiom(lits,ast_scope(store_array));
+	  else
+	    res = iproof->make_axiom(lits); // for array extensionality axiom
 	  break;
 	}
 	default: