fixes and performance improvements for interp and duality

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,56 +3084,70 @@ 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");
-	throw "should be unsat";
-      }
-      std::vector<expr> assumps, axioms_to_add;
-      slvr().get_proof().get_assumptions(assumps);
-      for(unsigned i = 0; i < assumps.size(); i++){
-	(*core).insert(assumps[i]);
-	if(axioms_needed.find(assumps[i]) != axioms_needed.end()){
-	  axioms_to_add.push_back(assumps[i]);
-	  axioms_needed.erase(assumps[i]);
-	}
-      }
-      // AddToProofCore(*core);
-      Transformer old_annot = node->Annotation;
-      SolveSingleNode(root,node);
-
-      {
-	expr itp = GetAnnotation(node);
-	dualModel = is.get_model(); // TODO: what does this mean?
-	std::vector<expr> case_lits;
-	itp = StrengthenFormulaByCaseSplitting(itp, case_lits);
-	SetAnnotation(node,itp);
-	node->Annotation.Formula = node->Annotation.Formula.simplify();
-      }
-
-      for(unsigned i = 0; i < axioms_to_add.size(); i++)
-	is.add(axioms_to_add[i]);
       
-#define TEST_BAD
-#ifdef TEST_BAD
       {
-	static int bad_count = 0, num_bads = 1;
+	check_result foo = Check(root);
-	if(bad_count >= num_bads){
+	if(foo != unsat){
-	  bad_count = 0;
-	  num_bads = num_bads * 2;
 	  Pop(1);
 	  is.pop(1);
 	  delete core;
 	  timer_stop("InterpolateByCases");
-	  throw Bad();
+	  throw ReallyBad();
+	  // slvr().print("should_be_unsat.smt2");
+	  // throw "should be unsat";
 	}
-	bad_count++;
+	std::vector<expr> assumps, axioms_to_add;
-      }
+	slvr().get_proof().get_assumptions(assumps);
-#endif
+	for(unsigned i = 0; i < assumps.size(); i++){
+	  (*core).insert(assumps[i]);
+	  if(axioms_needed.find(assumps[i]) != axioms_needed.end()){
+	    axioms_to_add.push_back(assumps[i]);
+	    axioms_needed.erase(assumps[i]);
+	  }
+	}
+	// AddToProofCore(*core);
+	SolveSingleNode(root,node);
 
-      if(node->Annotation.IsEmpty()){
+	{
+	  expr itp = GetAnnotation(node);
+	  dualModel = is.get_model(); // TODO: what does this mean?
+	  std::vector<expr> case_lits;
+	  itp = StrengthenFormulaByCaseSplitting(itp, case_lits);
+	  SetAnnotation(node,itp);
+	  node->Annotation.Formula = node->Annotation.Formula.simplify();
+	}
+
+	for(unsigned i = 0; i < axioms_to_add.size(); i++)
+	  is.add(axioms_to_add[i]);
+      
+#define TEST_BAD
+#ifdef TEST_BAD
+	{
+	  static int bad_count = 0, num_bads = 1;
+	  if(bad_count >= num_bads){
+	    bad_count = 0;
+	    num_bads = num_bads * 2;
+	    Pop(1);
+	    is.pop(1);
+	    delete core;
+	    timer_stop("InterpolateByCases");
+	    throw Bad();
+	  }
+	  bad_count++;
+	}
+#endif
+      }
+
+      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){