enabled extensional arrays in duality and added theory axioms lazily in GreedyReduce

src/duality/duality.h

@@ -171,6 +171,9 @@ namespace Duality {
            /** Assert a background axiom. */
            virtual void assert_axiom(const expr &axiom) = 0;
 
+	   /** Get the background axioms. */
+	   virtual const std::vector<expr> &get_axioms() = 0;
+
            /** Return a string describing performance. */
            virtual std::string profile() = 0;
 
@@ -182,7 +185,11 @@ namespace Duality {
 	   /** Cancel, throw Canceled object if possible. */
 	   virtual void cancel(){ }
 
-           LogicSolver(context &c) : aux_solver(c){}
+	   /* Note: aux solver uses extensional array theory, since it
+	      needs to be able to produce counter-models for
+	      interpolants the have array equalities in them.
+	   */
+           LogicSolver(context &c) : aux_solver(c,true){}
 
 	   virtual ~LogicSolver(){}
       };
@@ -208,6 +215,10 @@ namespace Duality {
             islvr->AssertInterpolationAxiom(axiom);
         }
 
+	const std::vector<expr> &get_axioms() {
+	  return islvr->GetInterpolationAxioms();
+	}
+
         std::string profile(){
            return islvr->profile();
         }

src/duality/duality_rpfp.cpp

@@ -1923,8 +1923,14 @@ namespace Duality {
     
     // verify
     check_result res = s.check(lits.size(),&lits[0]);
-    if(res != unsat)
-      throw "should be unsat";
+    if(res != unsat){
+      // 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++)
+	s.add(theory[i]);
+      if(s.check(lits.size(),&lits[0]) != unsat)
+	throw "should be unsat";
+    }
     
     for(unsigned i = 0; i < conjuncts.size(); ){
       std::swap(conjuncts[i],conjuncts.back());
@@ -1987,13 +1993,21 @@ namespace Duality {
       aux_solver.pop(1);
       Push();
       FixCurrentStateFull(node->Outgoing);
-      ConstrainEdgeLocalized(node->Outgoing,!GetAnnotation(node));
+      // ConstrainEdgeLocalized(node->Outgoing,!GetAnnotation(node));
       check_result foo = Check(root);
       if(foo != unsat)
 	throw "should be unsat";
       AddToProofCore(*core);
       Transformer old_annot = node->Annotation;
       SolveSingleNode(root,node);
+      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!";
+      }
       Pop(1);
       node->Annotation.UnionWith(old_annot);
     }

src/duality/duality_wrapper.cpp

@@ -29,7 +29,7 @@ Revision History:
 
 namespace Duality {
 
-  solver::solver(Duality::context& c) : object(c), the_model(c) {
+  solver::solver(Duality::context& c, bool extensional) : object(c), the_model(c) {
     params_ref p;
     p.set_bool("proof", true); // this is currently useless
     p.set_bool("model", true); 
@@ -37,6 +37,8 @@ namespace Duality {
     p.set_bool("mbqi",true);
     p.set_str("mbqi.id","itp"); // use mbqi for quantifiers in interpolants
     p.set_uint("mbqi.max_iterations",1); // use mbqi for quantifiers in interpolants
+    if(true || extensional)
+      p.set_bool("array.extensional",true);
     scoped_ptr<solver_factory> sf = mk_smt_solver_factory();
     m_solver = (*sf)(m(), p, true, true, true, ::symbol::null);
     m_solver->updt_params(p); // why do we have to do this?

src/duality/duality_wrapper.h

@@ -807,7 +807,7 @@ namespace Duality {
         model the_model;
 	bool canceled;
     public:
-        solver(context & c);
+        solver(context & c, bool extensional = false);
         solver(context & c, ::solver *s):object(c),the_model(c) { m_solver = s; canceled = false;}
         solver(solver const & s):object(s), the_model(s.the_model) { m_solver = s.m_solver; canceled = false;}
         ~solver() {
@@ -1326,6 +1326,7 @@ namespace Duality {
       void SetWeakInterpolants(bool weak);
       void SetPrintToFile(const std::string &file_name);
       
+      const std::vector<expr> &GetInterpolationAxioms() {return theory;}
       const char *profile();
       
     private: