dealing with incompleteness issues in duality

src/duality/duality.h

@@ -1005,6 +1005,8 @@ private:
       /** Object thrown on cancellation */
       struct Canceled {};
       
+      /** Object thrown on incompleteness */
+      struct Incompleteness {};
     };
 }
 

src/duality/duality_rpfp.cpp

@@ -2289,6 +2289,7 @@ namespace Duality {
   }
 
   void RPFP::InterpolateByCases(Node *root, Node *node){
+    bool axioms_added = false;
     aux_solver.push();
     AddEdgeToSolver(node->Outgoing);
     node->Annotation.SetEmpty();
@@ -2320,15 +2321,24 @@ namespace Duality {
 	std::vector<expr> case_lits;
 	itp = StrengthenFormulaByCaseSplitting(itp, case_lits);
 	SetAnnotation(node,itp);
+	node->Annotation.Formula.simplify();
       }
 
       if(node->Annotation.IsEmpty()){
-	std::cout << "bad in InterpolateByCase -- core:\n";
-	std::vector<expr> assumps;
-	slvr.get_proof().get_assumptions(assumps);
-	for(unsigned i = 0; i < assumps.size(); i++)
-	  assumps[i].show();
-	throw "ack!";
+	if(!axioms_added){
+	  // add the axioms in the off chance they are useful
+	  const std::vector<expr> &theory = ls->get_axioms();
+	  for(unsigned i = 0; i < theory.size(); i++)
+	    aux_solver.add(theory[i]);
+	}
+	else {
+	  std::cout << "bad in InterpolateByCase -- core:\n";
+	  std::vector<expr> 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);

src/duality/duality_solver.cpp

@@ -1731,6 +1731,7 @@ namespace Duality {
       virtual bool Build(){
 
 	stack.back().level = tree->slvr.get_scope_level();
+	bool was_sat = true;
 
 	while (true)
 	{
@@ -1760,8 +1761,11 @@ namespace Duality {
 		if(RecordUpdate(node))
 		  update_count++;
 	      }
-	      if(update_count == 0)
+	      if(update_count == 0){
+		if(was_sat)
+		  throw Incompleteness();
 		reporter->Message("backtracked without learning");
+	      }
 	    }
 	    tree->ComputeProofCore(); // need to compute the proof core before popping solver
 	    while(1) {
@@ -1796,8 +1800,10 @@ namespace Duality {
 	    HandleUpdatedNodes();
 	    if(stack.size() == 1)
 	      return false;
+	    was_sat = false;
 	  }
 	  else {
+	    was_sat = true;
 	    tree->Push();
 	    std::vector<Node *> &expansions = stack.back().expansions;
 	    for(unsigned i = 0; i < expansions.size(); i++){

src/interp/iz3translate.cpp

@@ -1642,6 +1642,10 @@ public:
 	res = iproof->make_axiom(lits);
 	break;
       }
+      case PR_IFF_TRUE: { // turns p into p <-> true, noop for us
+	res = args[0];
+	break;
+      }
       default:
 	assert(0 && "translate_main: unsupported proof rule");
 	throw unsupported();

src/muz/duality/duality_dl_interface.cpp

@@ -213,6 +213,9 @@ lbool dl_interface::query(::expr * query) {
   catch (Duality::solver::cancel_exception &exn){
     throw default_exception("duality canceled");
   }
+  catch (Duality::Solver::Incompleteness &exn){
+    throw default_exception("incompleteness");
+  }
   
   // profile!