adding support for non-extensional arrays in duality

src/duality/duality.h

@@ -31,6 +31,8 @@ using namespace stl_ext;
 
 namespace Duality {
 
+  class implicant_solver;
+
   /* Generic operations on Z3 formulas */
 
   struct Z3User {
@@ -104,6 +106,9 @@ namespace Duality {
 
       FuncDecl RenumberPred(const FuncDecl &f, int n);
 
+    Term ExtractStores(hash_map<ast, Term> &memo, const Term &t, std::vector<expr> &cnstrs, hash_map<ast,expr> &renaming);
+
+
 protected:
 
       void SummarizeRec(hash_set<ast> &memo, std::vector<expr> &lits, int &ops, const Term &t);
@@ -602,6 +607,8 @@ protected:
       void FixCurrentState(Edge *root);
     
       void FixCurrentStateFull(Edge *edge, const expr &extra);
+      
+      void FixCurrentStateFull(Edge *edge, const std::vector<expr> &assumps, const hash_map<ast,expr> &renaming);
 
       /** Declare a constant in the background theory. */
 
@@ -944,10 +951,12 @@ protected:
       Term UnderapproxFormula(const Term &f, hash_set<ast> &dont_cares);
 
       void ImplicantFullRed(hash_map<ast,int> &memo, const Term &f, std::vector<Term> &lits,
-			    hash_set<ast> &done, hash_set<ast> &dont_cares);
+			    hash_set<ast> &done, hash_set<ast> &dont_cares, bool extensional = true);
 
-      Term UnderapproxFullFormula(const Term &f, hash_set<ast> &dont_cares);
+    public:
+      Term UnderapproxFullFormula(const Term &f, bool extensional = true);
 
+    protected:
       Term ToRuleRec(Edge *e,  hash_map<ast,Term> &memo, const Term &t, std::vector<expr> &quants);
 
       hash_map<ast,Term> resolve_ite_memo;
@@ -988,6 +997,8 @@ protected:
 
       void AddEdgeToSolver(Edge *edge);
 
+      void AddEdgeToSolver(implicant_solver &aux_solver, Edge *edge);
+
       void AddToProofCore(hash_set<ast> &core);
 
       void GetGroundLitsUnderQuants(hash_set<ast> *memo, const Term &f, std::vector<Term> &res, int under);

src/duality/duality_rpfp.cpp

@@ -410,6 +410,33 @@ namespace Duality {
     return res;
   }
 
+  Z3User::Term Z3User::ExtractStores(hash_map<ast, Term> &memo, const Term &t, std::vector<expr> &cnstrs, hash_map<ast,expr> &renaming)
+  {
+    std::pair<ast,Term> foo(t,expr(ctx));
+    std::pair<hash_map<ast,Term>::iterator, bool> bar = memo.insert(foo);
+    Term &res = bar.first->second;
+    if(!bar.second) return res;
+    if (t.is_app()) {
+      func_decl f = t.decl();
+      std::vector<Term> args;
+      int nargs = t.num_args();
+      for(int i = 0; i < nargs; i++)
+	args.push_back(ExtractStores(memo, t.arg(i),cnstrs,renaming));
+      res = f(args.size(),&args[0]);
+      if(f.get_decl_kind() == Store){
+	func_decl fresh = ctx.fresh_func_decl("@arr", res.get_sort());
+	expr y = fresh();
+	expr equ = ctx.make(Equal,y,res);
+	cnstrs.push_back(equ);
+	renaming[y] = res;
+	res = y;
+      }
+    }
+    else res = t;
+    return res;
+  }
+
+
   bool Z3User::IsLiteral(const expr &lit, expr &atom, expr &val){
     if(!(lit.is_quantifier() && IsClosedFormula(lit))){
       if(!lit.is_app())
@@ -1851,7 +1878,7 @@ namespace Duality {
   }
 
   void RPFP::ImplicantFullRed(hash_map<ast,int> &memo, const Term &f, std::vector<Term> &lits,
-			      hash_set<ast> &done, hash_set<ast> &dont_cares){
+			      hash_set<ast> &done, hash_set<ast> &dont_cares, bool extensional){
     if(done.find(f) != done.end())
       return; /* already processed */
     if(f.is_app()){
@@ -1859,7 +1886,7 @@ namespace Duality {
       decl_kind k = f.decl().get_decl_kind();
       if(k == Implies || k == Iff || k == And || k == Or || k == Not){
 	for(int i = 0; i < nargs; i++)
-	  ImplicantFullRed(memo,f.arg(i),lits,done,dont_cares);
+	  ImplicantFullRed(memo,f.arg(i),lits,done,dont_cares, extensional);
 	goto done;
       }
     }
@@ -1867,6 +1894,15 @@ namespace Duality {
       if(dont_cares.find(f) == dont_cares.end()){
 	int b = SubtermTruth(memo,f);
 	if(b != 0 && b != 1) goto done;
+	if(f.is_app() && f.decl().get_decl_kind() == Equal && f.arg(0).is_array()){
+	  if(b == 1 && !extensional){
+	    expr x = dualModel.eval(f.arg(0)); expr y = dualModel.eval(f.arg(1));
+	    if(!eq(x,y))
+	      b = 0;
+	  }
+	  if(b == 0)
+	    goto done;
+	}
 	expr bv = (b==1) ? f : !f;
 	lits.push_back(bv);
       }
@@ -1988,12 +2024,16 @@ namespace Duality {
     return conjoin(lits);
   }
 
-  RPFP::Term RPFP::UnderapproxFullFormula(const Term &f, hash_set<ast> &dont_cares){
+  RPFP::Term RPFP::UnderapproxFullFormula(const Term &f, bool extensional){
+    hash_set<ast> dont_cares;
+    resolve_ite_memo.clear();
+    timer_start("UnderapproxFormula");
     /* first compute truth values of subterms */
     hash_map<ast,int> memo;
     hash_set<ast> done;
     std::vector<Term> lits;
-    ImplicantFullRed(memo,f,lits,done,dont_cares);
+    ImplicantFullRed(memo,f,lits,done,dont_cares, extensional);
+    timer_stop("UnderapproxFormula");
     /* return conjunction of literals */
     return conjoin(lits);
   }
@@ -2538,22 +2578,6 @@ namespace Duality {
     ConstrainEdgeLocalized(edge,eu);
   }
 
-  void RPFP::FixCurrentStateFull(Edge *edge, const expr &extra){
-    hash_set<ast> dont_cares;
-    resolve_ite_memo.clear();
-    timer_start("UnderapproxFormula");
-    Term dual = edge->dual.null() ? ctx.bool_val(true) : edge->dual;
-    for(unsigned i = 0; i < edge->constraints.size(); i++)
-      dual = dual && edge->constraints[i];
-    // dual = dual && extra;
-    Term eu = UnderapproxFullFormula(dual,dont_cares);
-    timer_stop("UnderapproxFormula");
-    ConstrainEdgeLocalized(edge,eu);
-  }
-
-  
-  
-
   void RPFP::GetGroundLitsUnderQuants(hash_set<ast> *memo, const Term &f, std::vector<Term> &res, int under){
     if(memo[under].find(f) != memo[under].end())
       return;
@@ -2836,7 +2860,91 @@ namespace Duality {
     return ctx.make(And,lits);
   }
 
-    // set up edge constraint in aux solver
+
+  /* This is a wrapper for a solver that is intended to compute
+     implicants from models. It works around a problem in Z3 with
+     models in the non-extensional array theory. It does this by
+     naming all of the store terms in a formula. That is, (store ...)
+     is replaced by "name" with an added constraint name = (store
+     ...). This allows us to determine from the model whether an array
+     equality is true or false (it is false if the two sides are
+     mapped to different function symbols, even if they have the same
+     contents).
+   */
+
+  struct implicant_solver {
+    RPFP *owner;
+    solver &aux_solver;
+    std::vector<expr> assumps, namings;
+    std::vector<int> assump_stack, naming_stack;
+    hash_map<ast,expr> renaming, renaming_memo;
+    
+    void add(const expr &e){
+      expr t = e;
+      if(!aux_solver.extensional_array_theory()){
+	unsigned i = namings.size();
+	t = owner->ExtractStores(renaming_memo,t,namings,renaming);
+	for(; i < namings.size(); i++)
+	  aux_solver.add(namings[i]);
+      }
+      assumps.push_back(t);
+      aux_solver.add(t);
+    }
+
+    void push() {
+      assump_stack.push_back(assumps.size());
+      naming_stack.push_back(namings.size());
+      aux_solver.push();
+    }
+
+    // When we pop the solver, we have to re-add any namings that were lost
+
+    void pop(int n) {
+      aux_solver.pop(n);
+      int new_assumps = assump_stack[assump_stack.size()-n];
+      int new_namings = naming_stack[naming_stack.size()-n];
+      for(unsigned i = new_namings; i < namings.size(); i++)
+	aux_solver.add(namings[i]);
+      assumps.resize(new_assumps);
+      namings.resize(new_namings);
+      assump_stack.resize(assump_stack.size()-1);
+      naming_stack.resize(naming_stack.size()-1);
+    }
+
+    check_result check() {
+      return aux_solver.check();
+    }
+
+    model get_model() {
+      return aux_solver.get_model();
+    }
+    
+    expr get_implicant() {
+      owner->dualModel = aux_solver.get_model();
+      expr dual = owner->ctx.make(And,assumps);
+      bool ext = aux_solver.extensional_array_theory();
+      expr eu = owner->UnderapproxFullFormula(dual,ext);
+      // if we renamed store terms, we have to undo
+      if(!ext)
+	eu = owner->SubstRec(renaming,eu);
+      return eu;
+    }
+    
+    implicant_solver(RPFP *_owner, solver &_aux_solver) 
+      : owner(_owner), aux_solver(_aux_solver)
+      {}
+  };
+
+  // set up edge constraint in aux solver
+  void RPFP::AddEdgeToSolver(implicant_solver &aux_solver, Edge *edge){
+    if(!edge->dual.null())
+      aux_solver.add(edge->dual);
+    for(unsigned i = 0; i < edge->constraints.size(); i++){
+      expr tl = edge->constraints[i];
+      aux_solver.add(tl);
+    }
+  }
+
   void RPFP::AddEdgeToSolver(Edge *edge){
     if(!edge->dual.null())
       aux_solver.add(edge->dual);
@@ -2853,28 +2961,29 @@ namespace Duality {
     const std::vector<expr> &theory = ls->get_axioms();
     for(unsigned i = 0; i < theory.size(); i++)
       axioms_needed.insert(theory[i]);
-    aux_solver.push();
+    implicant_solver is(this,aux_solver);
-    AddEdgeToSolver(node->Outgoing);
+    is.push();
+    AddEdgeToSolver(is,node->Outgoing);
     node->Annotation.SetEmpty();
     hash_set<ast> *core = new hash_set<ast>;
     core->insert(node->Outgoing->dual);
     while(1){
-      aux_solver.push();
+      is.push();
       expr annot = !GetAnnotation(node);
-      aux_solver.add(annot);
+      is.add(annot);
-      if(aux_solver.check() == unsat){
+      if(is.check() == unsat){
-	aux_solver.pop(1);
+	is.pop(1);
 	break;
       }
-      dualModel = aux_solver.get_model();
+      is.pop(1);
-      aux_solver.pop(1);
       Push();
-      FixCurrentStateFull(node->Outgoing,annot);
+      ConstrainEdgeLocalized(node->Outgoing,is.get_implicant());
-       ConstrainEdgeLocalized(node->Outgoing,!GetAnnotation(node));
+      ConstrainEdgeLocalized(node->Outgoing,!GetAnnotation(node)); //TODO: need this?
       check_result foo = Check(root);
-      if(foo != unsat)
+      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++){
@@ -2890,7 +2999,7 @@ namespace Duality {
 
       {
 	expr itp = GetAnnotation(node);
-	dualModel = aux_solver.get_model();
+	dualModel = is.get_model(); // TODO: what does this mean?
 	std::vector<expr> case_lits;
 	itp = StrengthenFormulaByCaseSplitting(itp, case_lits);
 	SetAnnotation(node,itp);
@@ -2898,14 +3007,14 @@ namespace Duality {
       }
 
       for(unsigned i = 0; i < axioms_to_add.size(); i++)
-	aux_solver.add(axioms_to_add[i]);
+	is.add(axioms_to_add[i]);
       
       if(node->Annotation.IsEmpty()){
 	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]);
+	    is.add(theory[i]);
 	  axioms_added = true;
 	}
 	else {
@@ -2923,7 +3032,7 @@ namespace Duality {
     if(proof_core)
       delete proof_core; // shouldn't happen
     proof_core = core;
-    aux_solver.pop(1);
+    is.pop(1);
     timer_stop("InterpolateByCases");
   }
 

src/duality/duality_solver.cpp

@@ -131,6 +131,7 @@ namespace Duality {
       Report = false;
       StratifiedInlining = false;
       RecursionBound = -1;
+      BatchExpand = false;
       {
 	scoped_no_proof no_proofs_please(ctx.m());
 #ifdef USE_RPFP_CLONE
@@ -365,6 +366,7 @@ namespace Duality {
     bool Report;         // spew on stdout
     bool StratifiedInlining; // Do stratified inlining as preprocessing step
     int RecursionBound;  // Recursion bound for bounded verification
+    bool BatchExpand;
     
     bool SetBoolOption(bool &opt, const std::string &value){
       if(value == "0") {
@@ -403,6 +405,9 @@ namespace Duality {
       if(option == "stratified_inlining"){
         return SetBoolOption(StratifiedInlining,value);
       }
+      if(option == "batch_expand"){
+        return SetBoolOption(BatchExpand,value);
+      }
       if(option == "recursion_bound"){
         return SetIntOption(RecursionBound,value);
       }
@@ -2016,7 +2021,7 @@ namespace Duality {
 	  }
 	  else {
 	    was_sat = true;
-	    tree->Push();
+	    tree->Push();
 	    std::vector<Node *> &expansions = stack.back().expansions;
 #ifndef NO_DECISIONS
 	    for(unsigned i = 0; i < expansions.size(); i++){
@@ -2027,11 +2032,16 @@ namespace Duality {
 	    if(tree->slvr().check() == unsat)
 	      throw "help!";
 #endif
-	    stack.push_back(stack_entry());
+	    int expand_max = 1;
-	    stack.back().level = tree->slvr().get_scope_level();
+	    if(0&&duality->BatchExpand){
-	    if(ExpandSomeNodes(false,1)){
+	      int thing = stack.size() * 0.1;
-	      continue;
+	      expand_max = std::max(1,thing);
+	      if(expand_max > 1)
+		std::cout << "foo!\n";
 	    }
+
+	    if(ExpandSomeNodes(false,expand_max))
+	      continue;
 	    while(stack.size() > 1){
 	      tree->Pop(1);	
 	      stack.pop_back();
@@ -2090,6 +2100,8 @@ namespace Duality {
       std::list<Node *> updated_nodes;
 
       virtual void ExpandNode(RPFP::Node *p){
+	stack.push_back(stack_entry());
+	stack.back().level = tree->slvr().get_scope_level();
 	stack.back().expansions.push_back(p);
 	DerivationTree::ExpandNode(p);
 	std::vector<Node *> &new_nodes = p->Outgoing->Children;

src/duality/duality_wrapper.cpp

@@ -37,7 +37,7 @@ Revision History:
 
 namespace Duality {
 
-  solver::solver(Duality::context& c, bool extensional, bool models) : object(c), the_model(c) {
+  solver::solver(Duality::context& c, bool _extensional, bool models) : object(c), the_model(c) {
     params_ref p;
     p.set_bool("proof", true); // this is currently useless
     if(models)
@@ -47,7 +47,8 @@ namespace Duality {
     p.set_bool("mbqi",mbqi); // just to test
     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)
+    extensional = mbqi && (true || _extensional);
+    if(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);
@@ -657,6 +658,18 @@ expr context::make_quant(decl_kind op, const std::vector<sort> &_sorts, const st
     pp.display_smt2(std::cout, m_solver->get_assertion(n-1));
   }
 
+  void solver::print(const char *filename) {
+    std::ofstream f(filename);
+    unsigned n = m_solver->get_num_assertions();
+    if(!n)
+      return;
+    ast_smt_pp pp(m());
+    for (unsigned i = 0; i < n-1; ++i)
+      pp.add_assumption(m_solver->get_assertion(i));
+    pp.display_smt2(f, m_solver->get_assertion(n-1));
+  }
+
+
   void solver::show_assertion_ids() {
 #if 0
     unsigned n = m_solver->get_num_assertions();

src/duality/duality_wrapper.h

@@ -819,6 +819,7 @@ namespace Duality {
         model the_model;
 	bool canceled;
 	proof_gen_mode m_mode;
+	bool extensional;
     public:
         solver(context & c, bool extensional = false, bool models = true);
         solver(context & c, ::solver *s):object(c),the_model(c) { m_solver = s; canceled = false;}
@@ -922,6 +923,7 @@ namespace Duality {
 	unsigned get_scope_level(){ scoped_proof_mode spm(m(),m_mode); return m_solver->get_scope_level();}
 
 	void show();
+	void print(const char *filename);
 	void show_assertion_ids();
 
 	proof get_proof(){
@@ -929,6 +931,7 @@ namespace Duality {
 	  return proof(ctx(),m_solver->get_proof());
 	}
 
+	bool extensional_array_theory() {return extensional;}
     };
 
 #if 0

src/muz/base/fixedpoint_params.pyg

@@ -75,6 +75,7 @@ def_module_params('fixedpoint',
 			  ('recursion_bound', UINT, UINT_MAX, 'DUALITY: Recursion bound for stratified inlining'),
 			  ('profile', BOOL, False, 'DUALITY: profile run time'),
 			  ('mbqi', BOOL, True, 'DUALITY: use model-based quantifier instantion'),
+			  ('batch_expand', BOOL, False, 'DUALITY: use batch expansion'),
                           ('dump_aig', SYMBOL, '', 'Dump clauses in AIG text format (AAG) to the given file name'),
                           ))
 

src/muz/duality/duality_dl_interface.cpp

@@ -205,6 +205,7 @@ lbool dl_interface::query(::expr * query) {
   rs->SetOption("feasible_edges",m_ctx.get_params().feasible_edges() ? "1" : "0");
   rs->SetOption("use_underapprox",m_ctx.get_params().use_underapprox() ? "1" : "0");
   rs->SetOption("stratified_inlining",m_ctx.get_params().stratified_inlining() ? "1" : "0");
+  rs->SetOption("batch_expand",m_ctx.get_params().batch_expand() ? "1" : "0");
   unsigned rb = m_ctx.get_params().recursion_bound();
   if(rb != UINT_MAX){
     std::ostringstream os; os << rb;