Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable

scripts/mk_project.py

@@ -55,8 +55,8 @@ def init_project_def():
     add_lib('fpa', ['core_tactics', 'bv_tactics', 'sat_tactic'], 'tactic/fpa')
     add_lib('smt_tactic', ['smt'], 'smt/tactic')
     add_lib('sls_tactic', ['tactic', 'normal_forms', 'core_tactics', 'bv_tactics'], 'tactic/sls')
-    add_lib('duality', ['smt', 'interp'])
     add_lib('qe', ['smt','sat'], 'qe')
+    add_lib('duality', ['smt', 'interp', 'qe'])
     add_lib('muz', ['smt', 'sat', 'smt2parser', 'aig_tactic', 'qe'], 'muz/base')
     add_lib('transforms', ['muz', 'hilbert'], 'muz/transforms')
     add_lib('rel', ['muz', 'transforms'], 'muz/rel')

src/api/api_interp.cpp

@@ -42,6 +42,20 @@ Revision History:
 using namespace stl_ext;
 #endif
 
+#ifndef WIN32
+// WARNING: don't make a hash_map with this if the range type
+// has a destructor: you'll get an address dependency!!!
+namespace stl_ext {
+  template <>
+  class hash<Z3_ast> {
+  public:
+    size_t operator()(const Z3_ast p) const {
+      return (size_t) p;
+    }
+  };
+}
+#endif
+
 typedef interpolation_options_struct *Z3_interpolation_options;
 
 extern "C" {
@@ -305,8 +319,8 @@ static void get_file_params(const char *filename, hash_map<std::string,std::stri
       tokenize(first_line.substr(2,first_line.size()-2),tokens);
       for(unsigned i = 0; i < tokens.size(); i++){
 	std::string &tok = tokens[i];
-	int eqpos = tok.find('=');
+	size_t eqpos = tok.find('=');
-	if(eqpos >= 0 && eqpos < (int)tok.size()){
+	if(eqpos >= 0 && eqpos < tok.size()){
 	  std::string left = tok.substr(0,eqpos);
 	  std::string right = tok.substr(eqpos+1,tok.size()-eqpos-1);
 	  params[left] = right;
@@ -363,7 +377,7 @@ extern "C" {
 #else
 
 
-  static Z3_ast and_vec(Z3_context ctx,std::vector<Z3_ast> &c){
+  static Z3_ast and_vec(Z3_context ctx,svector<Z3_ast> &c){
       return (c.size() > 1) ? Z3_mk_and(ctx,c.size(),&c[0]) : c[0];
   }
   
@@ -381,15 +395,15 @@ extern "C" {
       }
     }
     else {
-      std::vector<std::vector<Z3_ast> > chs(num);
+      std::vector<svector<Z3_ast> > chs(num);
       for(int i = 0; i < num-1; i++){
-	std::vector<Z3_ast> &c = chs[i];
+          svector<Z3_ast> &c = chs[i];
 	c.push_back(cnsts[i]);
 	Z3_ast foo = Z3_mk_interp(ctx,and_vec(ctx,c));
 	chs[parents[i]].push_back(foo);
       }
       {
-	std::vector<Z3_ast> &c = chs[num-1];
+	svector<Z3_ast> &c = chs[num-1];
 	c.push_back(cnsts[num-1]);
 	res = and_vec(ctx,c);
       }
@@ -454,7 +468,7 @@ extern "C" {
   static std::string read_msg;
   static std::vector<Z3_ast> read_theory;
 
-  static bool iZ3_parse(Z3_context ctx, const char *filename, const char **error, std::vector<Z3_ast> &assertions){
+  static bool iZ3_parse(Z3_context ctx, const char *filename, const char **error, svector<Z3_ast> &assertions){
     read_error.clear();
     try {
       std::string foo(filename);
@@ -497,25 +511,25 @@ extern "C" {
     hash_map<std::string,std::string> file_params;
     get_file_params(filename,file_params);
     
-    int num_theory = 0;
+    unsigned num_theory = 0;
     if(file_params.find("THEORY") != file_params.end())
       num_theory = atoi(file_params["THEORY"].c_str());
 
-    std::vector<Z3_ast> assertions;
+    svector<Z3_ast> assertions;
     if(!iZ3_parse(ctx,filename,error,assertions))
       return false;
     
-    if(num_theory > (int)assertions.size())
+    if(num_theory > assertions.size())
         num_theory = assertions.size();
-    int num = assertions.size() - num_theory;
+    unsigned num = assertions.size() - num_theory;
 
     read_cnsts.resize(num);
     read_parents.resize(num);
     read_theory.resize(num_theory);
 
-    for(int j = 0; j < num_theory; j++)
+    for(unsigned j = 0; j < num_theory; j++)
       read_theory[j] = assertions[j];
-    for(int j = 0; j < num; j++)
+    for(unsigned j = 0; j < num; j++)
       read_cnsts[j] = assertions[j+num_theory];
     
     if(ret_num_theory)
@@ -529,12 +543,12 @@ extern "C" {
       return true;
     }
 
-    for(int j = 0; j < num; j++)
+    for(unsigned j = 0; j < num; j++)
       read_parents[j] = SHRT_MAX;
     
     hash_map<Z3_ast,int> pred_map;
 
-    for(int j = 0; j < num; j++){
+    for(unsigned j = 0; j < num; j++){
       Z3_ast lhs = 0, rhs = read_cnsts[j];
 
       if(Z3_get_decl_kind(ctx,Z3_get_app_decl(ctx,Z3_to_app(ctx,rhs))) == Z3_OP_IMPLIES){
@@ -588,7 +602,7 @@ extern "C" {
       }
     }
 
-    for(int j = 0; j < num-1; j++)
+    for(unsigned j = 0; j < num-1; j++)
       if(read_parents[j] == SHRT_MIN){
 	read_error << "formula " << j+1 << ": unreferenced";
 	goto fail;

src/ast/ast.cpp

@@ -3161,3 +3161,6 @@ void prexpr(expr_ref &e){
   std::cout << mk_pp(e.get(), e.get_manager()) << std::endl;
 }
 
+void ast_manager::show_id_gen(){
+  std::cout << "id_gen: " << m_expr_id_gen.show_hash() << " " << m_decl_id_gen.show_hash() << "\n";
+}

src/ast/ast.h

@@ -1418,6 +1418,8 @@ protected:
 public:
     typedef expr_dependency_array_manager::ref expr_dependency_array;
 
+    void show_id_gen();
+
 protected:
     small_object_allocator    m_alloc;
     family_manager            m_family_manager;

src/ast/proof_checker/proof_checker.cpp

@@ -479,7 +479,7 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) {
             // otherwise t2 is also a quantifier.
             return true;
         }
-        UNREACHABLE();
+        IF_VERBOSE(0, verbose_stream() << "does not match last rule: " << mk_pp(p, m) << "\n";);
         return false;
     }
     case PR_DER: {
@@ -488,13 +488,12 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) {
             match_fact(p, fact) &&
             match_iff(fact.get(), t1, t2) &&
             match_quantifier(t1, is_forall, decls1, body1) &&
-            is_forall &&
+            is_forall) {
-            match_or(body1.get(), terms1)) {
             // TBD: check that terms are set of equalities.
             // t2 is an instance of a predicate in terms1
             return true;
         }        
-        UNREACHABLE();
+        IF_VERBOSE(0, verbose_stream() << "does not match last rule: " << mk_pp(p, m) << "\n";);
         return false;
     }
     case PR_HYPOTHESIS: {
@@ -832,7 +831,7 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) {
             }
             else {
                 IF_VERBOSE(0, verbose_stream() << "Could not establish complementarity for:\n" << 
-                           mk_pp(lit1, m) << "\n" << mk_pp(lit2, m) << "\n";);
+                           mk_pp(lit1, m) << "\n" << mk_pp(lit2, m) << "\n" << mk_pp(p, m) << "\n";);
             }
             fmls[i] = premise1;
         }

src/duality/duality.h

@@ -79,9 +79,36 @@ namespace Duality {
 
       int CumulativeDecisions();
 
-  private:
+      int CountOperators(const Term &t);
+
+      Term SubstAtom(hash_map<ast, Term> &memo, const expr &t, const expr &atom, const expr &val);
+
+      Term RemoveRedundancy(const Term &t);
+
+      bool IsLiteral(const expr &lit, expr &atom, expr &val);
+
+      expr Negate(const expr &f);
+
+      expr SimplifyAndOr(const std::vector<expr> &args, bool is_and);
+
+      expr ReallySimplifyAndOr(const std::vector<expr> &args, bool is_and);
+
+      int MaxIndex(hash_map<ast,int> &memo, const Term &t);
+
+      bool IsClosedFormula(const Term &t);
+
+      Term AdjustQuantifiers(const Term &t);
+private:
 
       void SummarizeRec(hash_set<ast> &memo, std::vector<expr> &lits, int &ops, const Term &t);
+      int CountOperatorsRec(hash_set<ast> &memo, const Term &t);
+      void RemoveRedundancyOp(bool pol, std::vector<expr> &args, hash_map<ast, Term> &smemo);
+      Term RemoveRedundancyRec(hash_map<ast, Term> &memo, hash_map<ast, Term> &smemo, const Term &t);
+      Term SubstAtomTriv(const expr &foo, const expr &atom, const expr &val);
+      expr ReduceAndOr(const std::vector<expr> &args, bool is_and, std::vector<expr> &res);
+      expr FinishAndOr(const std::vector<expr> &args, bool is_and);
+      expr PullCommonFactors(std::vector<expr> &args, bool is_and);
+
 
 };
 
@@ -142,6 +169,7 @@ namespace Duality {
            context *ctx;   /** Z3 context for formulas */
            solver *slvr;   /** Z3 solver */
            bool need_goals; /** Can the solver use the goal tree to optimize interpolants? */
+	   solver aux_solver; /** For temporary use -- don't leave assertions here. */
 
            /** Tree interpolation. This method assumes the formulas in TermTree
                "assumptions" are currently asserted in the solver. The return
@@ -167,6 +195,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;
 
@@ -178,6 +209,12 @@ namespace Duality {
 	   /** Cancel, throw Canceled object if possible. */
 	   virtual void cancel(){ }
 
+	   /* 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(){}
       };
 
@@ -202,6 +239,10 @@ namespace Duality {
             islvr->AssertInterpolationAxiom(axiom);
         }
 
+	const std::vector<expr> &get_axioms() {
+	  return islvr->GetInterpolationAxioms();
+	}
+
         std::string profile(){
            return islvr->profile();
         }
@@ -215,7 +256,7 @@ namespace Duality {
         }
 #endif
 
-        iZ3LogicSolver(context &c){
+      iZ3LogicSolver(context &c) : LogicSolver(c) {
           ctx = ictx = &c;
           slvr = islvr = new interpolating_solver(*ictx);
           need_goals = false;
@@ -277,6 +318,7 @@ namespace Duality {
       public:
 	std::list<Edge *> edges;
 	std::list<Node *> nodes;
+	std::list<std::pair<Edge *,Term> > constraints;
       };
       
       
@@ -286,6 +328,8 @@ namespace Duality {
       literals dualLabels;
       std::list<stack_entry> stack;
       std::vector<Term> axioms; // only saved here for printing purposes
+      solver &aux_solver;
+      hash_set<ast> *proof_core;
       
     public:
 
@@ -296,13 +340,14 @@ namespace Duality {
 	  inherit the axioms. 
       */
 
-    RPFP(LogicSolver *_ls) : Z3User(*(_ls->ctx), *(_ls->slvr)), dualModel(*(_ls->ctx))
+    RPFP(LogicSolver *_ls) : Z3User(*(_ls->ctx), *(_ls->slvr)), dualModel(*(_ls->ctx)), aux_solver(_ls->aux_solver)
       {
         ls = _ls;
 	nodeCount = 0;
 	edgeCount = 0;
 	stack.push_back(stack_entry());
         HornClauses = false;
+	proof_core = 0;
       }
 
       ~RPFP();
@@ -351,10 +396,10 @@ namespace Duality {
 	bool SubsetEq(const Transformer &other){
 	  Term t = owner->SubstParams(other.IndParams,IndParams,other.Formula);
 	  expr test = Formula && !t;
-	  owner->slvr.push();
+	  owner->aux_solver.push();
-	  owner->slvr.add(test);
+	  owner->aux_solver.add(test);
-	  check_result res = owner->slvr.check();
+	  check_result res = owner->aux_solver.check();
-	  owner->slvr.pop(1);
+	  owner->aux_solver.pop(1);
 	  return res == unsat;
 	}
 
@@ -444,6 +489,19 @@ namespace Duality {
 	return n;
       }
       
+      /** Delete a node. You can only do this if not connected to any edges.*/
+      void DeleteNode(Node *node){
+	if(node->Outgoing || !node->Incoming.empty())
+	  throw "cannot delete RPFP node";
+	for(std::vector<Node *>::iterator it = nodes.end(), en = nodes.begin(); it != en;){
+	  if(*(--it) == node){
+	    nodes.erase(it);
+	    break;
+	  }
+	}
+	delete node;
+      }
+
       /** This class represents a hyper-edge in the RPFP graph */
       
       class Edge
@@ -460,6 +518,7 @@ namespace Duality {
 	hash_map<ast,Term> varMap;
 	Edge *map;
 	Term labeled;
+	std::vector<Term> constraints;
 	
       Edge(Node *_Parent, const Transformer &_F, const std::vector<Node *> &_Children, RPFP *_owner, int _number)
 	: F(_F), Parent(_Parent), Children(_Children), dual(expr(_owner->ctx)) {
@@ -480,6 +539,29 @@ namespace Duality {
 	return e;
       }
       
+      
+      /** Delete a hyper-edge and unlink it from any nodes. */
+      void DeleteEdge(Edge *edge){
+	if(edge->Parent)
+	  edge->Parent->Outgoing = 0;
+	for(unsigned int i = 0; i < edge->Children.size(); i++){
+	  std::vector<Edge *> &ic = edge->Children[i]->Incoming;
+	  for(std::vector<Edge *>::iterator it = ic.begin(), en = ic.end(); it != en; ++it){
+	    if(*it == edge){
+	      ic.erase(it);
+	      break;
+	    }
+	  }
+	}
+	for(std::vector<Edge *>::iterator it = edges.end(), en = edges.begin(); it != en;){
+	  if(*(--it) == edge){
+	    edges.erase(it);
+	    break;
+	  }
+	}
+	delete edge;
+      }
+      
       /** Create an edge that lower-bounds its parent. */
       Edge *CreateLowerBoundEdge(Node *_Parent)
       {
@@ -494,6 +576,9 @@ namespace Duality {
       
       void AssertEdge(Edge *e, int persist = 0, bool with_children = false, bool underapprox = false);
 
+      /* Constrain an edge by the annotation of one of its children. */
+
+      void ConstrainParent(Edge *parent, Node *child);
 
       /** For incremental solving, asserts the negation of the upper bound associated
        * with a node.
@@ -501,6 +586,16 @@ namespace Duality {
       
       void AssertNode(Node *n);
 
+      /** Assert a constraint on an edge in the SMT context. 
+       */
+      void ConstrainEdge(Edge *e, const Term &t);
+      
+      /** Fix the truth values of atomic propositions in the given
+	  edge to their values in the current assignment. */
+      void FixCurrentState(Edge *root);
+    
+      void FixCurrentStateFull(Edge *edge, const expr &extra);
+
       /** Declare a constant in the background theory. */
 
       void DeclareConstant(const FuncDecl &f);
@@ -554,9 +649,13 @@ namespace Duality {
 
       lbool Solve(Node *root, int persist);
       
+      /** Same as Solve, but annotates only a single node. */
+
+      lbool SolveSingleNode(Node *root, Node *node);
+
       /** Get the constraint tree (but don't solve it) */
       
-      TermTree *GetConstraintTree(Node *root);
+      TermTree *GetConstraintTree(Node *root, Node *skip_descendant = 0);
   
       /** Dispose of the dual model (counterexample) if there is one. */
       
@@ -592,6 +691,13 @@ namespace Duality {
 
       Term ComputeUnderapprox(Node *root, int persist);
 
+      /** Try to strengthen the annotation of a node by removing disjuncts. */
+      void Generalize(Node *root, Node *node);
+
+
+      /** Compute disjunctive interpolant for node by case splitting */
+      void InterpolateByCases(Node *root, Node *node);
+
       /** Push a scope. Assertions made after Push can be undone by Pop. */
       
       void Push();
@@ -624,6 +730,16 @@ namespace Duality {
       
       void Pop(int num_scopes);
       
+      /** Erase the proof by performing a Pop, Push and re-assertion of
+	  all the popped constraints */
+      void PopPush();
+
+      /** Return true if the given edge is used in the proof of unsat.
+	  Can be called only after Solve or Check returns an unsat result. */
+      
+      bool EdgeUsedInProof(Edge *edge);
+
+
       /** Convert a collection of clauses to Nodes and Edges in the RPFP.
 	  
 	  Predicate unknowns are uninterpreted predicates not
@@ -707,8 +823,19 @@ namespace Duality {
 
       //      int GetLabelsRec(hash_map<ast,int> *memo, const Term &f, std::vector<symbol> &labels, bool labpos);
 
+      /** Compute and save the proof core for future calls to
+	  EdgeUsedInProof.  You only need to call this if you will pop
+	  the solver before calling EdgeUsedInProof.
+       */
+      void ComputeProofCore();
+
     private:
       
+      void ClearProofCore(){
+	if(proof_core)
+	  delete proof_core;
+	proof_core = 0;
+      }
 
       Term SuffixVariable(const Term &t, int n);
       
@@ -724,10 +851,14 @@ namespace Duality {
 
       Term ReducedDualEdge(Edge *e);
 
-      TermTree *ToTermTree(Node *root);
+      TermTree *ToTermTree(Node *root, Node *skip_descendant = 0);
 
       TermTree *ToGoalTree(Node *root);
 
+      void CollapseTermTreeRec(TermTree *root, TermTree *node);
+
+      TermTree *CollapseTermTree(TermTree *node);
+
       void DecodeTree(Node *root, TermTree *interp, int persist);
 
       Term GetUpperBound(Node *n);
@@ -777,6 +908,11 @@ namespace Duality {
 
       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);
+
+      Term UnderapproxFullFormula(const Term &f, hash_set<ast> &dont_cares);
+
       Term ToRuleRec(Edge *e,  hash_map<ast,Term> &memo, const Term &t, std::vector<expr> &quants);
 
       hash_map<ast,Term> resolve_ite_memo;
@@ -803,6 +939,25 @@ namespace Duality {
 
       Term SubstBound(hash_map<int,Term> &subst, const Term &t);
 
+      void ConstrainEdgeLocalized(Edge *e, const Term &t);
+
+      void GreedyReduce(solver &s, std::vector<expr> &conjuncts);
+      
+      void NegateLits(std::vector<expr> &lits);
+
+      expr SimplifyOr(std::vector<expr> &lits);
+
+      void SetAnnotation(Node *root, const expr &t);
+
+      void AddEdgeToSolver(Edge *edge);
+
+      void AddToProofCore(hash_set<ast> &core);
+
+      void GetGroundLitsUnderQuants(hash_set<ast> *memo, const Term &f, std::vector<Term> &res, int under);
+
+      Term StrengthenFormulaByCaseSplitting(const Term &f, std::vector<expr> &case_lits);
+    
+      expr NegateLit(const expr &f);
 
     };
     
@@ -852,3 +1007,38 @@ namespace Duality {
       
     };
 }
+
+
+// Allow to hash on nodes and edges in deterministic way
+
+namespace hash_space {
+  template <>
+    class hash<Duality::RPFP::Node *> {
+  public:
+    size_t operator()(const Duality::RPFP::Node *p) const {
+      return p->number;
+    }
+  };
+}
+
+namespace hash_space {
+  template <>
+    class hash<Duality::RPFP::Edge *> {
+  public:
+    size_t operator()(const Duality::RPFP::Edge *p) const {
+      return p->number;
+    }
+  };
+}
+
+// allow to walk sets of nodes without address dependency
+
+namespace std {
+  template <>
+    class less<Duality::RPFP::Node *> {
+  public:
+    bool operator()(Duality::RPFP::Node * const &s, Duality::RPFP::Node * const &t) const {
+      return s->number < t->number; // s.raw()->get_id() < t.raw()->get_id();
+    }
+  };
+}

src/duality/duality_rpfp.cpp

@@ -25,6 +25,8 @@ Revision History:
 #include "duality_profiling.h"
 #include <algorithm>
 #include <fstream>
+#include <set>
+#include <iterator>
 
 #ifndef WIN32
 // #define Z3OPS
@@ -89,14 +91,16 @@ namespace Duality {
     if(memo.find(t) != memo.end())
       return;
     memo.insert(t);
+    if(t.is_app()){
       decl_kind k = t.decl().get_decl_kind();
       if(k == And || k == Or || k == Not || k == Implies || k == Iff){
 	ops++;
 	int nargs = t.num_args();
 	for(int i = 0; i < nargs; i++)
 	  SummarizeRec(memo,lits,ops,t.arg(i));
+	return;
+      }
     }
-    else
     lits.push_back(t);
   }
 
@@ -123,6 +127,32 @@ namespace Duality {
     }
   }
 
+  int Z3User::CountOperatorsRec(hash_set<ast> &memo, const Term &t){
+    if(memo.find(t) != memo.end())
+      return 0;
+    memo.insert(t);
+    if(t.is_app()){
+      decl_kind k = t.decl().get_decl_kind();
+      if(k == And || k == Or){
+	int count = 1;
+	int nargs = t.num_args();
+	for(int i = 0; i < nargs; i++)
+	  count += CountOperatorsRec(memo,t.arg(i));
+	return count;
+      }
+      return 0;
+    }
+    if(t.is_quantifier())
+      return CountOperatorsRec(memo,t.body())+2; // count 2 for a quantifier
+    return 0;
+  }
+
+  int Z3User::CountOperators(const Term &t){
+    hash_set<ast> memo;
+    return CountOperatorsRec(memo,t);
+  }
+
+
   Z3User::Term Z3User::conjoin(const std::vector<Term> &args){
     return ctx.make(And,args);
   }
@@ -183,6 +213,7 @@ namespace Duality {
     return clone_quantifier(t,new_body);
   }
 
+
   RPFP::Term RPFP::LocalizeRec(Edge *e,  hash_map<ast,Term> &memo, const Term &t)
   {
     std::pair<ast,Term> foo(t,expr(ctx));
@@ -272,16 +303,21 @@ namespace Duality {
     return implies(b, Localize(e, e->F.Formula));
   }
 
-  TermTree *RPFP::ToTermTree(Node *root)
+  TermTree *RPFP::ToTermTree(Node *root, Node *skip_descendant)
   {
+    if(skip_descendant && root == skip_descendant)
+      return new TermTree(ctx.bool_val(true));
     Edge *e = root->Outgoing;
     if(!e) return new TermTree(ctx.bool_val(true), std::vector<TermTree *>());
     std::vector<TermTree *> children(e->Children.size());
     for(unsigned i = 0; i < children.size(); i++)
-      children[i] = ToTermTree(e->Children[i]);
+      children[i] = ToTermTree(e->Children[i],skip_descendant);
     // Term top = ReducedDualEdge(e);
     Term top = e->dual.null() ? ctx.bool_val(true) : e->dual;
-    return new TermTree(top, children);
+    TermTree *res = new TermTree(top, children);
+    for(unsigned i = 0; i < e->constraints.size(); i++)
+      res->addTerm(e->constraints[i]);
+    return res;
   }
 
   TermTree *RPFP::GetGoalTree(Node *root){
@@ -321,11 +357,229 @@ namespace Duality {
 	res = f(args.size(),&args[0]);
       }
     else if (t.is_quantifier())
-      res = CloneQuantifier(t,SubstRec(memo, t.body()));
+      {
+	std::vector<expr> pats;
+	t.get_patterns(pats);
+	for(unsigned i = 0; i < pats.size(); i++)
+	  pats[i] = SubstRec(memo,pats[i]);
+	Term body = SubstRec(memo,t.body());
+	res = clone_quantifier(t, body, pats);
+      }
+    // res = CloneQuantifier(t,SubstRec(memo, t.body()));
     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())
+	return false;
+      decl_kind k = lit.decl().get_decl_kind();
+      if(k == Not){
+	if(IsLiteral(lit.arg(0),atom,val)){
+	  val = eq(val,ctx.bool_val(true)) ? ctx.bool_val(false) : ctx.bool_val(true); 
+	  return true;
+	}
+	return false;
+      }
+      if(k == And || k == Or || k == Iff || k == Implies)
+	return false;
+    }
+    atom = lit;
+    val = ctx.bool_val(true);
+    return true;
+  }
+
+  expr Z3User::Negate(const expr &f){
+    if(f.is_app() && f.decl().get_decl_kind() == Not)
+      return f.arg(0);
+    else if(eq(f,ctx.bool_val(true)))
+      return ctx.bool_val(false);
+    else if(eq(f,ctx.bool_val(false)))
+      return ctx.bool_val(true);
+    return !f;
+  }
+
+  expr Z3User::ReduceAndOr(const std::vector<expr> &args, bool is_and, std::vector<expr> &res){
+    for(unsigned i = 0; i < args.size(); i++)
+      if(!eq(args[i],ctx.bool_val(is_and))){
+	if(eq(args[i],ctx.bool_val(!is_and)))
+	  return ctx.bool_val(!is_and);
+	res.push_back(args[i]);
+      }
+    return expr();
+  }
+
+  expr Z3User::FinishAndOr(const std::vector<expr> &args, bool is_and){
+    if(args.size() == 0)
+      return ctx.bool_val(is_and);
+    if(args.size() == 1)
+      return args[0];
+    return ctx.make(is_and ? And : Or,args);
+  }
+
+  expr Z3User::SimplifyAndOr(const std::vector<expr> &args, bool is_and){
+    std::vector<expr> sargs;
+    expr res = ReduceAndOr(args,is_and,sargs);
+    if(!res.null()) return res;
+    return FinishAndOr(sargs,is_and);
+  }
+
+  expr Z3User::PullCommonFactors(std::vector<expr> &args, bool is_and){
+    
+    // first check if there's anything to do...
+    if(args.size() < 2)
+      return FinishAndOr(args,is_and);
+    for(unsigned i = 0; i < args.size(); i++){
+      const expr &a = args[i];
+      if(!(a.is_app() && a.decl().get_decl_kind() == (is_and ? Or : And)))
+	return FinishAndOr(args,is_and);
+    }
+    std::vector<expr> common;
+    for(unsigned i = 0; i < args.size(); i++){
+      unsigned n = args[i].num_args();
+      std::vector<expr> v(n),w;
+      for(unsigned j = 0; j < n; j++)
+	v[j] = args[i].arg(j);
+      std::less<ast> comp;
+      std::sort(v.begin(),v.end(),comp);
+      if(i == 0)
+	common.swap(v);
+      else {
+	std::set_intersection(common.begin(),common.end(),v.begin(),v.end(),std::inserter(w,w.begin()),comp);
+	common.swap(w);
+      }
+    }  
+    if(common.empty())
+      return FinishAndOr(args,is_and);
+    std::set<ast> common_set(common.begin(),common.end());
+    for(unsigned i = 0; i < args.size(); i++){
+      unsigned n = args[i].num_args();
+      std::vector<expr> lits;
+      for(unsigned j = 0; j < n; j++){
+	const expr b = args[i].arg(j);
+	if(common_set.find(b) == common_set.end())
+	  lits.push_back(b);
+      }
+      args[i] = SimplifyAndOr(lits,!is_and);
+    }  
+    common.push_back(SimplifyAndOr(args,is_and));
+    return SimplifyAndOr(common,!is_and);
+  }
+
+  expr Z3User::ReallySimplifyAndOr(const std::vector<expr> &args, bool is_and){
+    std::vector<expr> sargs;
+    expr res = ReduceAndOr(args,is_and,sargs);
+    if(!res.null()) return res;
+    return PullCommonFactors(sargs,is_and);
+  }
+
+  Z3User::Term Z3User::SubstAtomTriv(const expr &foo, const expr &atom, const expr &val){
+    if(eq(foo,atom))
+      return val;
+    else if(foo.is_app() && foo.decl().get_decl_kind() == Not && eq(foo.arg(0),atom))
+      return Negate(val);
+    else
+      return foo;
+  }
+
+  Z3User::Term Z3User::SubstAtom(hash_map<ast, Term> &memo, const expr &t, const expr &atom, const expr &val){
+    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();
+      decl_kind k = f.get_decl_kind();
+      
+      // TODO: recur here, but how much? We don't want to be quadractic in formula size
+      
+      if(k == And || k == Or){
+	int nargs = t.num_args();
+	std::vector<Term> args(nargs);
+	for(int i = 0; i < nargs; i++)
+	  args[i] = SubstAtom(memo,t.arg(i),atom,val);
+	res = ReallySimplifyAndOr(args, k==And);
+	return res;
+      }
+    }
+    else if(t.is_quantifier() && atom.is_quantifier()){
+      if(eq(t,atom))
+	res = val;
+      else
+	res = clone_quantifier(t,SubstAtom(memo,t.body(),atom,val));
+      return res;
+    }
+    res = SubstAtomTriv(t,atom,val);
+    return res;
+  }
+
+  void Z3User::RemoveRedundancyOp(bool pol, std::vector<expr> &args, hash_map<ast, Term> &smemo){
+    for(unsigned i = 0; i < args.size(); i++){
+      const expr &lit = args[i];
+      expr atom, val;
+      if(IsLiteral(lit,atom,val)){
+	for(unsigned j = 0; j < args.size(); j++)
+	  if(j != i){
+	    smemo.clear();
+	    args[j] = SubstAtom(smemo,args[j],atom,pol ? val : !val);
+	  }
+      }
+    }
+  }
+  
+
+  Z3User::Term Z3User::RemoveRedundancyRec(hash_map<ast, Term> &memo, hash_map<ast, Term> &smemo, const Term &t)
+  {
+    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(RemoveRedundancyRec(memo, smemo, t.arg(i)));
+
+	decl_kind k = f.get_decl_kind();
+	if(k == And){
+	  RemoveRedundancyOp(true,args,smemo);
+	  res = ReallySimplifyAndOr(args, true);
+	}
+	else if(k == Or){
+	  RemoveRedundancyOp(false,args,smemo);
+	  res = ReallySimplifyAndOr(args, false);
+	}
+	else {
+	  if(k == Equal && args[0].get_id() > args[1].get_id())
+	    std::swap(args[0],args[1]);
+	  res = f(args.size(),&args[0]);
+	}
+      }
+    else if (t.is_quantifier())
+      {
+	Term body = RemoveRedundancyRec(memo,smemo,t.body());
+	res = clone_quantifier(t, body);
+      }
+    else res = t;
+    return res;
+  }
+
+  Z3User::Term Z3User::RemoveRedundancy(const Term &t){
+    hash_map<ast, Term> memo;
+    hash_map<ast, Term> smemo;
+    return RemoveRedundancyRec(memo,smemo,t);
+  }
+
+  Z3User::Term Z3User::AdjustQuantifiers(const Term &t)
+  {
+    if(t.is_quantifier() || (t.is_app() && t.has_quantifiers()))
+      return t.qe_lite();
+    return t;
+  }
+
   Z3User::Term Z3User::SubstRecHide(hash_map<ast, Term> &memo, const Term &t, int number)
   {
     std::pair<ast,Term> foo(t,expr(ctx));
@@ -373,6 +627,19 @@ namespace Duality {
       x = x && y;
   }
 
+  void RPFP::SetAnnotation(Node *root, const expr &t){
+    hash_map<ast, Term> memo;
+    Term b;
+    std::vector<Term> v;
+    RedVars(root, b, v);
+    memo[b] = ctx.bool_val(true);
+    for (unsigned i = 0; i < v.size(); i++)
+      memo[v[i]] = root->Annotation.IndParams[i];
+    Term annot = SubstRec(memo, t);
+    // Strengthen(ref root.Annotation.Formula, annot);
+    root->Annotation.Formula = annot;
+  }
+
   void RPFP::DecodeTree(Node *root, TermTree *interp, int persist)
   {
     std::vector<TermTree *> &ic = interp->getChildren();
@@ -382,16 +649,7 @@ namespace Duality {
 	for (unsigned i = 0; i < nc.size(); i++)
 	  DecodeTree(nc[i], ic[i], persist);
       }
-    hash_map<ast, Term> memo;
+    SetAnnotation(root,interp->getTerm());
-    Term b;
-    std::vector<Term> v;
-    RedVars(root, b, v);
-    memo[b] = ctx.bool_val(true);
-    for (unsigned i = 0; i < v.size(); i++)
-      memo[v[i]] = root->Annotation.IndParams[i];
-    Term annot = SubstRec(memo, interp->getTerm());
-    // Strengthen(ref root.Annotation.Formula, annot);
-    root->Annotation.Formula = annot;
 #if 0
     if(persist != 0)
       Z3_persist_ast(ctx,root->Annotation.Formula,persist);
@@ -509,6 +767,10 @@ namespace Duality {
     timer_stop("solver add");
   }
 
+  void RPFP::ConstrainParent(Edge *parent, Node *child){
+    ConstrainEdgeLocalized(parent,GetAnnotation(child));
+  } 
+
         
   /** For incremental solving, asserts the negation of the upper bound associated
    * with a node.
@@ -524,6 +786,24 @@ namespace Duality {
       }
   }
 
+  /** Assert a constraint on an edge in the SMT context. 
+   */
+
+  void RPFP::ConstrainEdge(Edge *e, const Term &t)
+  {
+    Term tl = Localize(e, t);
+    ConstrainEdgeLocalized(e,tl);
+  }
+
+  void RPFP::ConstrainEdgeLocalized(Edge *e, const Term &tl)
+  {
+    e->constraints.push_back(tl);
+    stack.back().constraints.push_back(std::pair<Edge *,Term>(e,tl));
+    slvr.add(tl);
+  }
+
+
+
   /** Declare a constant in the background theory. */
 
   void RPFP::DeclareConstant(const FuncDecl &f){
@@ -592,6 +872,7 @@ namespace Duality {
     TermTree *goals = NULL;
     if(ls->need_goals)
       goals = GetGoalTree(root);
+    ClearProofCore();
 
     // if (dualModel != null) dualModel.Dispose();
     // if (dualLabels != null) dualLabels.Dispose();
@@ -613,11 +894,54 @@ namespace Duality {
     return res;
   }
   
+  void RPFP::CollapseTermTreeRec(TermTree *root, TermTree *node){
+    root->addTerm(node->getTerm());
+    std::vector<Term> &cnsts = node->getTerms();
+    for(unsigned i = 0; i < cnsts.size(); i++)
+      root->addTerm(cnsts[i]);
+    std::vector<TermTree *> &chs = node->getChildren();
+    for(unsigned i = 0; i < chs.size(); i++){
+      CollapseTermTreeRec(root,chs[i]);
+    }
+  }
+
+  TermTree *RPFP::CollapseTermTree(TermTree *node){
+    std::vector<TermTree *> &chs = node->getChildren();
+    for(unsigned i = 0; i < chs.size(); i++)
+      CollapseTermTreeRec(node,chs[i]);
+    for(unsigned i = 0; i < chs.size(); i++)
+      delete chs[i];
+    chs.clear();
+    return node;
+  }
+    
+  lbool RPFP::SolveSingleNode(Node *root, Node *node)
+  {
+    timer_start("Solve");
+    TermTree *tree = CollapseTermTree(GetConstraintTree(root,node));
+    tree->getChildren().push_back(CollapseTermTree(ToTermTree(node)));
+    TermTree *interpolant = NULL;
+    ClearProofCore();
+
+    timer_start("interpolate_tree");
+    lbool res = ls->interpolate_tree(tree, interpolant, dualModel,0,true);
+    timer_stop("interpolate_tree");
+    if (res == l_false)
+      {
+	DecodeTree(node, interpolant->getChildren()[0], 0);
+	delete interpolant;
+      }
+
+    delete tree;
+    timer_stop("Solve");
+    return res;
+  }
+
   /** Get the constraint tree (but don't solve it) */
   
-  TermTree *RPFP::GetConstraintTree(Node *root)
+  TermTree *RPFP::GetConstraintTree(Node *root, Node *skip_descendant)
   {
-    return AddUpperBound(root, ToTermTree(root));
+    return AddUpperBound(root, ToTermTree(root,skip_descendant));
   }
   
   /** Dispose of the dual model (counterexample) if there is one. */
@@ -646,6 +970,7 @@ namespace Duality {
 
   check_result RPFP::Check(Node *root, std::vector<Node *> underapproxes, std::vector<Node *> *underapprox_core )
         {
+	  ClearProofCore();
 	  // if (dualModel != null) dualModel.Dispose();
 	  check_result res;
 	  if(!underapproxes.size())
@@ -682,6 +1007,7 @@ namespace Duality {
 
   check_result RPFP::CheckUpdateModel(Node *root, std::vector<expr> assumps){
     // check_result temp1 = slvr.check(); // no idea why I need to do this
+    ClearProofCore();
     check_result res = slvr.check_keep_model(assumps.size(),&assumps[0]);
     dualModel = slvr.get_model();
     return res;
@@ -1062,7 +1388,8 @@ namespace Duality {
 	  }
 	}
 	/* Unreachable! */
-	throw "error in RPFP::ImplicantRed";
+	// TODO: need to indicate this failure to caller
+	// std::cerr << "error in RPFP::ImplicantRed";
 	goto done;
       }
       else if(k == Not) {
@@ -1081,6 +1408,31 @@ namespace Duality {
     done[truth].insert(f);
   }
 
+  void RPFP::ImplicantFullRed(hash_map<ast,int> &memo, const Term &f, std::vector<Term> &lits,
+			      hash_set<ast> &done, hash_set<ast> &dont_cares){
+    if(done.find(f) != done.end())
+      return; /* already processed */
+    if(f.is_app()){
+      int nargs = f.num_args();
+      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);
+	goto done;
+      }
+    }
+    {
+      if(dont_cares.find(f) == dont_cares.end()){
+	int b = SubtermTruth(memo,f);
+	if(b != 0 && b != 1) goto done;
+	expr bv = (b==1) ? f : !f;
+	lits.push_back(bv);
+      }
+    }
+  done:
+    done.insert(f);
+  }
+
   RPFP::Term RPFP::ResolveIte(hash_map<ast,int> &memo, const Term &t, std::vector<Term> &lits,
 			hash_set<ast> *done, hash_set<ast> &dont_cares){
     if(resolve_ite_memo.find(t) != resolve_ite_memo.end())
@@ -1143,6 +1495,16 @@ namespace Duality {
     return conjoin(lits);
   }
 
+  RPFP::Term RPFP::UnderapproxFullFormula(const Term &f, hash_set<ast> &dont_cares){
+    /* 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);
+    /* return conjunction of literals */
+    return conjoin(lits);
+  }
+
   struct VariableProjector : Z3User {
   
     struct elim_cand {
@@ -1669,6 +2031,121 @@ namespace Duality {
     return eu;
   }
 
+  void RPFP::FixCurrentState(Edge *edge){
+    hash_set<ast> dont_cares;
+    resolve_ite_memo.clear();
+    timer_start("UnderapproxFormula");
+    Term dual = edge->dual.null() ? ctx.bool_val(true) : edge->dual;
+    Term eu = UnderapproxFormula(dual,dont_cares);
+    timer_stop("UnderapproxFormula");
+    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;
+    memo[under].insert(f);
+    if(f.is_app()){
+      if(!under && !f.has_quantifiers())
+	return;
+      decl_kind k = f.decl().get_decl_kind();
+      if(k == And || k == Or || k == Implies || k == Iff){
+	int num_args = f.num_args();
+	for(int i = 0; i < num_args; i++)
+	  GetGroundLitsUnderQuants(memo,f.arg(i),res,under);
+	return;
+      }
+    }
+    else if (f.is_quantifier()){
+#if 0
+      // treat closed quantified formula as a literal 'cause we hate nested quantifiers
+      if(under && IsClosedFormula(f)) 
+	res.push_back(f);
+      else
+#endif
+	GetGroundLitsUnderQuants(memo,f.body(),res,1);
+      return;
+    }
+    if(under && f.is_ground())
+      res.push_back(f);
+  }
+
+  RPFP::Term RPFP::StrengthenFormulaByCaseSplitting(const Term &f, std::vector<expr> &case_lits){
+    hash_set<ast> memo[2];
+    std::vector<Term> lits;
+    GetGroundLitsUnderQuants(memo, f, lits, 0);
+    hash_set<ast> lits_hash;
+    for(unsigned i = 0; i < lits.size(); i++)
+      lits_hash.insert(lits[i]);
+    hash_map<ast,expr> subst;
+    hash_map<ast,int> stt_memo;
+    std::vector<expr> conjuncts;
+    for(unsigned i = 0; i < lits.size(); i++){
+      const expr &lit = lits[i];
+      if(lits_hash.find(NegateLit(lit)) == lits_hash.end()){
+	case_lits.push_back(lit);
+	bool tval = false;
+	expr atom = lit;
+	if(lit.is_app() && lit.decl().get_decl_kind() == Not){
+	  tval = true;
+	  atom = lit.arg(0);
+	}
+	expr etval = ctx.bool_val(tval);
+	if(atom.is_quantifier())
+	  subst[atom] = etval; // this is a bit desperate, since we can't eval quants
+	else {
+	  int b = SubtermTruth(stt_memo,atom);
+	  if(b == (tval ? 1 : 0))
+	    subst[atom] = etval;
+	  else {
+	    if(b == 0 || b == 1){
+	      etval = ctx.bool_val(b ? true : false);
+	      subst[atom] = etval;
+	      conjuncts.push_back(b ? atom : !atom);
+	    }
+	  }
+	}
+      }
+    }
+    expr g = f;
+    if(!subst.empty()){
+      g = SubstRec(subst,f);
+      if(conjuncts.size())
+	g = g && ctx.make(And,conjuncts);
+      g = g.simplify();
+    }
+#if 1
+    expr g_old = g;
+    g = RemoveRedundancy(g);
+    bool changed = !eq(g,g_old);
+    g = g.simplify();
+    if(changed) {  // a second pass can get some more simplification
+      g = RemoveRedundancy(g);
+      g = g.simplify();
+    }
+#else
+    g = RemoveRedundancy(g);
+    g = g.simplify();
+#endif
+    g = AdjustQuantifiers(g);
+    return g;
+  }
 
   RPFP::Term RPFP::ModelValueAsConstraint(const Term &t){
     if(t.is_array()){
@@ -1712,6 +2189,167 @@ namespace Duality {
     res = CreateRelation(p->Annotation.IndParams,funder);
   }
 
+#if 0
+  void RPFP::GreedyReduce(solver &s, std::vector<expr> &conjuncts){
+    // verify
+    s.push();
+    expr conj = ctx.make(And,conjuncts);
+    s.add(conj);
+    check_result res = s.check();
+    if(res != unsat)
+      throw "should be unsat";
+    s.pop(1);
+	
+    for(unsigned i = 0; i < conjuncts.size(); ){
+      std::swap(conjuncts[i],conjuncts.back());
+      expr save = conjuncts.back();
+      conjuncts.pop_back();
+      s.push();
+      expr conj = ctx.make(And,conjuncts);
+      s.add(conj);
+      check_result res = s.check();
+      s.pop(1);
+      if(res != unsat){
+	conjuncts.push_back(save);
+	std::swap(conjuncts[i],conjuncts.back());
+	i++;
+      }
+    }
+  }
+#endif
+
+  void RPFP::GreedyReduce(solver &s, std::vector<expr> &conjuncts){
+    std::vector<expr> lits(conjuncts.size());
+    for(unsigned i = 0; i < lits.size(); i++){
+      func_decl pred = ctx.fresh_func_decl("@alit", ctx.bool_sort());
+      lits[i] = pred();
+      s.add(ctx.make(Implies,lits[i],conjuncts[i]));
+    }
+    
+    // verify
+    check_result res = s.check(lits.size(),&lits[0]);
+    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());
+      std::swap(lits[i],lits.back());
+      check_result res = s.check(lits.size()-1,&lits[0]);
+      if(res != unsat){
+	std::swap(conjuncts[i],conjuncts.back());
+	std::swap(lits[i],lits.back());
+	i++;
+      }
+      else {
+	conjuncts.pop_back();
+	lits.pop_back();
+      }
+    }
+  }
+
+  expr RPFP::NegateLit(const expr &f){
+    if(f.is_app() && f.decl().get_decl_kind() == Not)
+      return f.arg(0);
+    else
+      return !f;
+  }
+
+  void RPFP::NegateLits(std::vector<expr> &lits){
+    for(unsigned i = 0; i < lits.size(); i++){
+      expr &f = lits[i];
+      if(f.is_app() && f.decl().get_decl_kind() == Not)
+	f = f.arg(0);
+      else
+	f = !f;
+    }
+  }
+
+  expr RPFP::SimplifyOr(std::vector<expr> &lits){
+    if(lits.size() == 0)
+      return ctx.bool_val(false);
+    if(lits.size() == 1)
+      return lits[0];
+    return ctx.make(Or,lits);
+  }
+
+    // set up edge constraint in aux solver
+  void RPFP::AddEdgeToSolver(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::InterpolateByCases(Node *root, Node *node){
+    aux_solver.push();
+    AddEdgeToSolver(node->Outgoing);
+    node->Annotation.SetEmpty();
+    hash_set<ast> *core = new hash_set<ast>;
+    core->insert(node->Outgoing->dual);
+    while(1){
+      aux_solver.push();
+      expr annot = !GetAnnotation(node);
+      aux_solver.add(annot);
+      if(aux_solver.check() == unsat){
+	aux_solver.pop(1);
+	break;
+      }
+      dualModel = aux_solver.get_model();
+      aux_solver.pop(1);
+      Push();
+      FixCurrentStateFull(node->Outgoing,annot);
+       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);
+
+      {
+	expr itp = GetAnnotation(node);
+	dualModel = aux_solver.get_model();
+	std::vector<expr> case_lits;
+	itp = StrengthenFormulaByCaseSplitting(itp, case_lits);
+	SetAnnotation(node,itp);
+      }
+
+      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);
+    }
+    if(proof_core)
+      delete proof_core; // shouldn't happen
+    proof_core = core;
+    aux_solver.pop(1);
+  }
+
+  void RPFP::Generalize(Node *root, Node *node){
+    aux_solver.push();
+    AddEdgeToSolver(node->Outgoing);
+    expr fmla = GetAnnotation(node);
+    std::vector<expr> conjuncts;
+    CollectConjuncts(fmla,conjuncts,false);
+    GreedyReduce(aux_solver,conjuncts);     // try to remove conjuncts one at a tme
+    aux_solver.pop(1);
+    NegateLits(conjuncts);
+    SetAnnotation(node,SimplifyOr(conjuncts));
+  }
 
   /** Push a scope. Assertions made after Push can be undone by Pop. */
 
@@ -1733,10 +2371,26 @@ namespace Duality {
 	  (*it)->dual = expr(ctx,NULL);
 	for(std::list<Node *>::iterator it = back.nodes.begin(), en = back.nodes.end(); it != en; ++it)
 	  (*it)->dual = expr(ctx,NULL);
+	for(std::list<std::pair<Edge *,Term> >::iterator it = back.constraints.begin(), en = back.constraints.end(); it != en; ++it)
+	  (*it).first->constraints.pop_back();
 	stack.pop_back();
       }
   }
   
+  /** Erase the proof by performing a Pop, Push and re-assertion of
+      all the popped constraints */
+
+  void RPFP::PopPush(){
+    slvr.pop(1);
+    slvr.push();
+    stack_entry &back = stack.back();
+    for(std::list<Edge *>::iterator it = back.edges.begin(), en = back.edges.end(); it != en; ++it)
+      slvr.add((*it)->dual);
+    for(std::list<Node *>::iterator it = back.nodes.begin(), en = back.nodes.end(); it != en; ++it)
+      slvr.add((*it)->dual);
+    for(std::list<std::pair<Edge *,Term> >::iterator it = back.constraints.begin(), en = back.constraints.end(); it != en; ++it)
+      slvr.add((*it).second);
+  }
   
   
   
@@ -1880,6 +2534,37 @@ namespace Duality {
     return SubstBoundRec(memo, subst, 0, t);
   }
 
+  int Z3User::MaxIndex(hash_map<ast,int> &memo, const Term &t)
+  {
+    std::pair<ast,int> foo(t,-1);
+    std::pair<hash_map<ast,int>::iterator, bool> bar = memo.insert(foo);
+    int &res = bar.first->second;
+    if(!bar.second) return res;
+    if (t.is_app()){
+      func_decl f = t.decl();
+      int nargs = t.num_args();
+      for(int i = 0; i < nargs; i++){
+	int m = MaxIndex(memo, t.arg(i));
+	if(m > res)
+	  res = m;
+      }
+    }
+    else if (t.is_quantifier()){
+      int bound = t.get_quantifier_num_bound();
+      res = MaxIndex(memo,t.body()) - bound;
+    }
+    else if (t.is_var()) {
+      res = t.get_index_value();
+    }
+    return res;
+  }
+
+  bool Z3User::IsClosedFormula(const Term &t){
+    hash_map<ast,int> memo;
+    return MaxIndex(memo,t) < 0;
+  }
+  
+
   /** Convert a collection of clauses to Nodes and Edges in the RPFP.
 
       Predicate unknowns are uninterpreted predicates not
@@ -2169,8 +2854,32 @@ namespace Duality {
     
   }
 
+  void RPFP::AddToProofCore(hash_set<ast> &core){
+    std::vector<expr> assumps;
+    slvr.get_proof().get_assumptions(assumps);
+    for(unsigned i = 0; i < assumps.size(); i++)
+      core.insert(assumps[i]);
+  }
+  
+  void RPFP::ComputeProofCore(){
+    if(!proof_core){
+      proof_core = new hash_set<ast>;
+      AddToProofCore(*proof_core);
+    }
+  }
+
+  bool RPFP::EdgeUsedInProof(Edge *edge){
+    ComputeProofCore();
+    if(!edge->dual.null() && proof_core->find(edge->dual) != proof_core->end())
+      return true;
+    for(unsigned i = 0; i < edge->constraints.size(); i++)
+      if(proof_core->find(edge->constraints[i]) != proof_core->end())
+	return true;
+    return false;
+  }
 
 RPFP::~RPFP(){
+    ClearProofCore();
     for(unsigned i = 0; i < nodes.size(); i++)
       delete nodes[i];
     for(unsigned i = 0; i < edges.size(); i++)

src/duality/duality_solver.cpp

@@ -184,7 +184,7 @@ namespace Duality {
 	    best.insert(*it);
       }
 #else
-      virtual void ChooseExpand(const std::set<RPFP::Node *> &choices, std::set<RPFP::Node *> &best, bool high_priority=false){
+      virtual void ChooseExpand(const std::set<RPFP::Node *> &choices, std::set<RPFP::Node *> &best, bool high_priority=false, bool best_only=false){
 	if(high_priority) return;
 	int best_score = INT_MAX;
 	int worst_score = 0;
@@ -194,7 +194,7 @@ namespace Duality {
 	  best_score = std::min(best_score,score);
 	  worst_score = std::max(worst_score,score);
 	}
-	int cutoff = best_score + (worst_score-best_score)/2;
+	int cutoff = best_only ? best_score : (best_score + (worst_score-best_score)/2);
 	for(std::set<Node *>::iterator it = choices.begin(), en = choices.end(); it != en; ++it)
 	  if(scores[(*it)->map].updates <= cutoff)
 	    best.insert(*it);
@@ -1270,18 +1270,24 @@ namespace Duality {
       }
     }
 
+    bool UpdateNodeToNode(Node *node, Node *top){
+      if(!node->Annotation.SubsetEq(top->Annotation)){
+	reporter->Update(node,top->Annotation);
+	indset->Update(node,top->Annotation);
+	updated_nodes.insert(node->map);
+	node->Annotation.IntersectWith(top->Annotation);
+	return true;
+      }
+      return false;
+    }
+
     /** Update the unwinding solution, using an interpolant for the
 	derivation tree. */
     void UpdateWithInterpolant(Node *node, RPFP *tree, Node *top){
       if(top->Outgoing)
 	for(unsigned i = 0; i < top->Outgoing->Children.size(); i++)
 	  UpdateWithInterpolant(node->Outgoing->Children[i],tree,top->Outgoing->Children[i]);
-      if(!node->Annotation.SubsetEq(top->Annotation)){
+      UpdateNodeToNode(node, top);
-	reporter->Update(node,top->Annotation);
-	indset->Update(node,top->Annotation);
-	updated_nodes.insert(node->map);
-	node->Annotation.IntersectWith(top->Annotation);
-      }
       heuristic->Update(node);
     }
 
@@ -1305,7 +1311,8 @@ namespace Duality {
       if(node->Bound.IsFull()) return true;
       reporter->Bound(node);
       int start_decs = rpfp->CumulativeDecisions();
-      DerivationTree dt(this,unwinding,reporter,heuristic,FullExpand);
+      DerivationTree *dtp = new DerivationTreeSlow(this,unwinding,reporter,heuristic,FullExpand);
+      DerivationTree &dt = *dtp;
       bool res = dt.Derive(unwinding,node,UseUnderapprox);
       int end_decs = rpfp->CumulativeDecisions();
       // std::cout << "decisions: " << (end_decs - start_decs)  << std::endl;
@@ -1321,6 +1328,7 @@ namespace Duality {
 	UpdateWithInterpolant(node,dt.tree,dt.top);
 	delete dt.tree;
       }
+      delete dtp;
       return !res;
     }
 
@@ -1491,7 +1499,7 @@ namespace Duality {
 	return res != unsat;
       }
 
-      bool Build(){
+      virtual bool Build(){
 #ifdef EFFORT_BOUNDED_STRAT
 	start_decs = tree->CumulativeDecisions();
 #endif
@@ -1545,7 +1553,7 @@ namespace Duality {
 	}
       }
 
-      void ExpandNode(RPFP::Node *p){
+      virtual void ExpandNode(RPFP::Node *p){
 	// tree->RemoveEdge(p->Outgoing);
 	Edge *edge = duality->GetNodeOutgoing(p->map,last_decs);
 	std::vector<RPFP::Node *> &cs = edge->Children;
@@ -1573,6 +1581,7 @@ namespace Duality {
       }
 #else
 #if 0
+
       void ExpansionChoices(std::set<Node *> &best){
 	std::vector <Node *> unused_set, used_set;
 	std::set<Node *> choices;
@@ -1598,12 +1607,12 @@ namespace Duality {
 	heuristic->ChooseExpand(choices, best);
       }
 #else
-      void ExpansionChoicesFull(std::set<Node *> &best, bool high_priority){
+      void ExpansionChoicesFull(std::set<Node *> &best, bool high_priority, bool best_only = false){
 	std::set<Node *> choices;
 	for(std::list<RPFP::Node *>::iterator it = leaves.begin(), en = leaves.end(); it != en; ++it)
 	  if (high_priority || !tree->Empty(*it)) // if used in the counter-model
 	    choices.insert(*it);
-	heuristic->ChooseExpand(choices, best, high_priority);
+	heuristic->ChooseExpand(choices, best, high_priority, best_only);
       }
 
       void ExpansionChoicesRec(std::vector <Node *> &unused_set, std::vector <Node *> &used_set, 
@@ -1641,9 +1650,9 @@ namespace Duality {
       
       std::set<Node *> old_choices;
 
-      void ExpansionChoices(std::set<Node *> &best, bool high_priority){
+      void ExpansionChoices(std::set<Node *> &best, bool high_priority, bool best_only = false){
 	if(!underapprox || constrained || high_priority){
-	  ExpansionChoicesFull(best, high_priority);
+	  ExpansionChoicesFull(best, high_priority,best_only);
 	  return;
 	}
 	std::vector <Node *> unused_set, used_set;
@@ -1668,28 +1677,259 @@ namespace Duality {
 #endif
 #endif
       
-      bool ExpandSomeNodes(bool high_priority = false){
+      bool ExpandSomeNodes(bool high_priority = false, int max = INT_MAX){
 #ifdef EFFORT_BOUNDED_STRAT
 	last_decs = tree->CumulativeDecisions() - start_decs;
 #endif
 	timer_start("ExpandSomeNodes");
 	timer_start("ExpansionChoices");
 	std::set<Node *> choices;
-	ExpansionChoices(choices,high_priority);
+	ExpansionChoices(choices,high_priority,max != INT_MAX);
 	timer_stop("ExpansionChoices");
 	std::list<RPFP::Node *> leaves_copy = leaves; // copy so can modify orig
 	leaves.clear();
+	int count = 0;
 	for(std::list<RPFP::Node *>::iterator it = leaves_copy.begin(), en = leaves_copy.end(); it != en; ++it){
-	  if(choices.find(*it) != choices.end())
+	  if(choices.find(*it) != choices.end() && count < max){
+	    count++;
 	    ExpandNode(*it);
+	  }
 	  else leaves.push_back(*it);
 	}
 	timer_stop("ExpandSomeNodes");
 	return !choices.empty();
       }
 
+      void RemoveExpansion(RPFP::Node *p){
+	Edge *edge = p->Outgoing;
+	Node *parent = edge->Parent; 
+	std::vector<RPFP::Node *> cs = edge->Children;
+	tree->DeleteEdge(edge);
+	for(unsigned i = 0; i < cs.size(); i++)
+	  tree->DeleteNode(cs[i]);
+	leaves.push_back(parent);
+      }
     };
 
+    class DerivationTreeSlow : public DerivationTree {
+    public:
+      
+      struct stack_entry {
+	unsigned level; // SMT solver stack level
+	std::vector<Node *> expansions;
+      };
+
+      std::vector<stack_entry> stack;
+
+      hash_map<Node *, expr> updates;
+
+      DerivationTreeSlow(Duality *_duality, RPFP *rpfp, Reporter *_reporter, Heuristic *_heuristic, bool _full_expand) 
+	: DerivationTree(_duality, rpfp, _reporter, _heuristic, _full_expand) {
+	stack.push_back(stack_entry());
+      }
+
+      virtual bool Build(){
+
+	stack.back().level = tree->slvr.get_scope_level();
+
+	while (true)
+	{
+	  lbool res;
+
+	  unsigned slvr_level = tree->slvr.get_scope_level();
+	  if(slvr_level != stack.back().level)
+	    throw "stacks out of sync!";
+
+	  //	  res = tree->Solve(top, 1);            // incremental solve, keep interpolants for one pop
+	  check_result foo = tree->Check(top);
+	  res = foo == unsat ? l_false : l_true;
+
+	  if (res == l_false) {
+	    if (stack.empty()) // should never happen
+	      return false;
+	    
+	    {
+	      std::vector<Node *> &expansions = stack.back().expansions;
+	      int update_count = 0;
+	      for(unsigned i = 0; i < expansions.size(); i++){
+		Node *node = expansions[i];
+		tree->SolveSingleNode(top,node);
+		if(expansions.size() == 1 && NodeTooComplicated(node))
+		  SimplifyNode(node);
+		tree->Generalize(top,node);
+		if(RecordUpdate(node))
+		  update_count++;
+	      }
+	      if(update_count == 0)
+		reporter->Message("backtracked without learning");
+	    }
+	    tree->ComputeProofCore(); // need to compute the proof core before popping solver
+	    while(1) {
+	      std::vector<Node *> &expansions = stack.back().expansions;
+	      bool prev_level_used = LevelUsedInProof(stack.size()-2); // need to compute this before pop
+	      tree->Pop(1);	
+	      hash_set<Node *> leaves_to_remove;
+	      for(unsigned i = 0; i < expansions.size(); i++){
+		Node *node = expansions[i];
+		//	      if(node != top)
+		//		tree->ConstrainParent(node->Incoming[0],node);
+		std::vector<Node *> &cs = node->Outgoing->Children;
+		for(unsigned i = 0; i < cs.size(); i++){
+		  leaves_to_remove.insert(cs[i]);
+		  UnmapNode(cs[i]);
+		  if(std::find(updated_nodes.begin(),updated_nodes.end(),cs[i]) != updated_nodes.end())
+		    throw "help!";
+		}
+	      }
+	      RemoveLeaves(leaves_to_remove); // have to do this before actually deleting the children
+	      for(unsigned i = 0; i < expansions.size(); i++){
+		Node *node = expansions[i];
+		RemoveExpansion(node);
+	      }
+	      stack.pop_back();
+	      if(prev_level_used || stack.size() == 1) break;
+	      RemoveUpdateNodesAtCurrentLevel(); // this level is about to be deleted -- remove its children from update list
+	      std::vector<Node *> &unused_ex = stack.back().expansions;
+	      for(unsigned i = 0; i < unused_ex.size(); i++)
+		heuristic->Update(unused_ex[i]->map); // make it less likely to expand this node in future
+	    } 
+	    HandleUpdatedNodes();
+	    if(stack.size() == 1)
+	      return false;
+	  }
+	  else {
+	    tree->Push();
+	    std::vector<Node *> &expansions = stack.back().expansions;
+	    for(unsigned i = 0; i < expansions.size(); i++){
+	      tree->FixCurrentState(expansions[i]->Outgoing);
+	    }
+#if 0
+	    if(tree->slvr.check() == unsat)
+	      throw "help!";
+#endif
+	    stack.push_back(stack_entry());
+	    stack.back().level = tree->slvr.get_scope_level();
+	    if(ExpandSomeNodes(false,1)){
+	      continue;
+	    }
+	    while(stack.size() > 1){
+	      tree->Pop(1);	
+	      stack.pop_back();
+	    }
+	    return true;
+	  }
+	}
+      }
+      
+      bool NodeTooComplicated(Node *node){
+	return tree->CountOperators(node->Annotation.Formula) > 3;
+      }
+
+      void SimplifyNode(Node *node){
+	// have to destroy the old proof to get a new interpolant
+	tree->PopPush();
+	tree->InterpolateByCases(top,node);
+      }
+
+      bool LevelUsedInProof(unsigned level){
+	std::vector<Node *> &expansions = stack[level].expansions;
+	for(unsigned i = 0; i < expansions.size(); i++)
+	  if(tree->EdgeUsedInProof(expansions[i]->Outgoing))
+	    return true;
+	return false;
+      }
+
+      void RemoveUpdateNodesAtCurrentLevel() {
+	for(std::list<Node *>::iterator it = updated_nodes.begin(), en = updated_nodes.end(); it != en;){
+	  Node *node = *it;
+	  if(AtCurrentStackLevel(node->Incoming[0]->Parent)){
+	    std::list<Node *>::iterator victim = it;
+	    ++it;
+	    updated_nodes.erase(victim);
+	  }
+	  else
+	    ++it;
+	}
+      }
+
+      void RemoveLeaves(hash_set<Node *> &leaves_to_remove){
+	std::list<RPFP::Node *> leaves_copy;
+	leaves_copy.swap(leaves);
+	for(std::list<RPFP::Node *>::iterator it = leaves_copy.begin(), en = leaves_copy.end(); it != en; ++it){
+	  if(leaves_to_remove.find(*it) == leaves_to_remove.end())
+	    leaves.push_back(*it);
+	}
+      }
+
+      hash_map<Node *, std::vector<Node *> > node_map;
+      std::list<Node *> updated_nodes;
+
+      virtual void ExpandNode(RPFP::Node *p){
+	stack.back().expansions.push_back(p);
+	DerivationTree::ExpandNode(p);
+	std::vector<Node *> &new_nodes = p->Outgoing->Children;
+	for(unsigned i = 0; i < new_nodes.size(); i++){
+	  Node *n = new_nodes[i];
+	  node_map[n->map].push_back(n);
+	}
+      }
+
+      bool RecordUpdate(Node *node){
+	bool res = duality->UpdateNodeToNode(node->map,node);
+	if(res){
+	  std::vector<Node *> to_update = node_map[node->map];
+	  for(unsigned i = 0; i < to_update.size(); i++){
+	    Node *node2 = to_update[i];
+	    // maintain invariant that no nodes on updated list are created at current stack level
+	    if(node2 == node || !(node->Incoming.size() > 0 && AtCurrentStackLevel(node2->Incoming[0]->Parent))){
+	      updated_nodes.push_back(node2);
+	      if(node2 != node)
+		node2->Annotation = node->Annotation;
+	    }
+	  }
+	}
+	return res;
+      }
+      
+      void HandleUpdatedNodes(){
+	for(std::list<Node *>::iterator it = updated_nodes.begin(), en = updated_nodes.end(); it != en;){
+	  Node *node = *it;
+	  node->Annotation = node->map->Annotation;
+	  if(node->Incoming.size() > 0)
+	    tree->ConstrainParent(node->Incoming[0],node);
+	  if(AtCurrentStackLevel(node->Incoming[0]->Parent)){
+	    std::list<Node *>::iterator victim = it;
+	    ++it;
+	    updated_nodes.erase(victim);
+	  }
+	  else
+	    ++it;
+	}
+      }
+      
+      bool AtCurrentStackLevel(Node *node){
+	std::vector<Node *> vec = stack.back().expansions;
+	for(unsigned i = 0; i < vec.size(); i++)
+	  if(vec[i] == node)
+	    return true;
+	return false;
+      }
+
+      void UnmapNode(Node *node){
+	std::vector<Node *> &vec = node_map[node->map];
+	for(unsigned i = 0; i < vec.size(); i++){
+	  if(vec[i] == node){
+	    std::swap(vec[i],vec.back());
+	    vec.pop_back();
+	    return;
+	  }
+	}
+	throw "can't unmap node";
+      }
+
+    };
+
+
     class Covering {
 
       struct cover_info {
@@ -2084,7 +2324,7 @@ namespace Duality {
 	return name;
       }
 
-      virtual void ChooseExpand(const std::set<RPFP::Node *> &choices, std::set<RPFP::Node *> &best, bool high_priority){
+      virtual void ChooseExpand(const std::set<RPFP::Node *> &choices, std::set<RPFP::Node *> &best, bool high_priority, bool best_only){
 	if(!high_priority || !old_cex.tree){
 	  Heuristic::ChooseExpand(choices,best,false);
 	  return;

src/duality/duality_wrapper.cpp

@@ -26,16 +26,23 @@ Revision History:
 #include "expr_abstract.h"
 #include "stopwatch.h"
 #include "model_smt2_pp.h"
+#include "qe_lite.h"
 
 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); 
     p.set_bool("unsat_core", true); 
+    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?
     canceled = false;
   }
 
@@ -323,6 +330,14 @@ expr context::make_quant(decl_kind op, const std::vector<sort> &_sorts, const st
     return simplify(p);
   }
 
+  expr expr::qe_lite() const {
+    ::qe_lite qe(m());
+    expr_ref result(to_expr(raw()),m());
+    proof_ref pf(m());
+    qe(result,pf);
+    return ctx().cook(result);
+  }
+
   expr clone_quantifier(const expr &q, const expr &b){
     return q.ctx().cook(q.m().update_quantifier(to_quantifier(q.raw()), to_expr(b.raw())));
   }
@@ -425,15 +440,18 @@ expr context::make_quant(decl_kind op, const std::vector<sort> &_sorts, const st
   
   static int linearize_assumptions(int num,
 				   TermTree *assumptions,
-				   std::vector<expr> &linear_assumptions, 
+				   std::vector<std::vector <expr> > &linear_assumptions, 
 				   std::vector<int> &parents){
     for(unsigned i = 0; i < assumptions->getChildren().size(); i++)
       num = linearize_assumptions(num, assumptions->getChildren()[i], linear_assumptions, parents);
-    linear_assumptions[num] = assumptions->getTerm();
+    // linear_assumptions[num].push_back(assumptions->getTerm());
     for(unsigned i = 0; i < assumptions->getChildren().size(); i++)
       parents[assumptions->getChildren()[i]->getNumber()] = num;
     parents[num] = SHRT_MAX; // in case we have no parent
-    linear_assumptions[num] = assumptions->getTerm();
+    linear_assumptions[num].push_back(assumptions->getTerm());
+    std::vector<expr> &ts = assumptions->getTerms();
+    for(unsigned i = 0; i < ts.size(); i++)
+      linear_assumptions[num].push_back(ts[i]);
     return num + 1;
   }
 
@@ -462,14 +480,15 @@ expr context::make_quant(decl_kind op, const std::vector<sort> &_sorts, const st
   
   {
     int size = assumptions->number(0);
-    std::vector<expr> linear_assumptions(size);
+    std::vector<std::vector<expr> > linear_assumptions(size);
     std::vector<int> parents(size);
     linearize_assumptions(0,assumptions,linear_assumptions,parents);
 
     ptr_vector< ::ast> _interpolants(size-1);
-    ptr_vector< ::ast>_assumptions(size);
+    vector<ptr_vector< ::ast> >_assumptions(size);
     for(int i = 0; i < size; i++)
-      _assumptions[i] = linear_assumptions[i];
+      for(unsigned j = 0; j < linear_assumptions[i].size(); j++)
+	_assumptions[i].push_back(linear_assumptions[i][j]);
     ::vector<int> _parents; _parents.resize(parents.size());
     for(unsigned i = 0; i < parents.size(); i++)
       _parents[i] = parents[i];
@@ -477,11 +496,12 @@ expr context::make_quant(decl_kind op, const std::vector<sort> &_sorts, const st
     for(unsigned i = 0; i < theory.size(); i++)
       _theory[i] = theory[i];
     
-    push();
     
     if(!incremental){
+      push();
       for(unsigned i = 0; i < linear_assumptions.size(); i++)
-	add(linear_assumptions[i]);
+	for(unsigned j = 0; j < linear_assumptions[i].size(); j++)
+	  add(linear_assumptions[i][j]);
     }
     
     check_result res = check();
@@ -517,6 +537,7 @@ expr context::make_quant(decl_kind op, const std::vector<sort> &_sorts, const st
     }
 #endif
     
+    if(!incremental)
       pop();
 
     return (res == unsat) ? l_false : ((res == sat) ? l_true : l_undef);
@@ -550,6 +571,29 @@ expr context::make_quant(decl_kind op, const std::vector<sort> &_sorts, const st
   }
 
   
+  static void get_assumptions_rec(stl_ext::hash_set<ast> &memo, const proof &pf, std::vector<expr> &assumps){
+    if(memo.find(pf) != memo.end())return;
+    memo.insert(pf);
+    pfrule dk = pf.rule();
+    if(dk == PR_ASSERTED){
+      expr con = pf.conc();
+      assumps.push_back(con);
+    }
+    else {
+      unsigned nprems = pf.num_prems();
+      for(unsigned i = 0; i < nprems; i++){
+	proof arg = pf.prem(i);
+	get_assumptions_rec(memo,arg,assumps);
+      }
+    }
+  }
+
+  void proof::get_assumptions(std::vector<expr> &assumps){
+    stl_ext::hash_set<ast> memo;
+    get_assumptions_rec(memo,*this,assumps);
+  }
+
+
   void ast::show() const{
     std::cout << mk_pp(raw(), m()) << std::endl;
   }
@@ -559,6 +603,40 @@ expr context::make_quant(decl_kind op, const std::vector<sort> &_sorts, const st
     std::cout << std::endl;
   }
   
+  void model::show_hash() const {
+    std::ostringstream ss;
+    model_smt2_pp(ss, m(), *m_model, 0);
+    hash_space::hash<std::string> hasher;
+    unsigned h = hasher(ss.str());
+    std::cout << "model hash: " << h << "\n";
+  }
+
+  void solver::show() {
+    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(std::cout, m_solver->get_assertion(n-1));
+  }
+
+  void solver::show_assertion_ids() {
+#if 0
+    unsigned n = m_solver->get_num_assertions();
+    std::cerr << "assertion ids: ";
+    for (unsigned i = 0; i < n-1; ++i)
+      std::cerr << " " << m_solver->get_assertion(i)->get_id();
+    std::cerr << "\n";
+#else
+    unsigned n = m_solver->get_num_assertions();
+    std::cerr << "assertion ids hash: ";
+    unsigned h = 0;
+    for (unsigned i = 0; i < n-1; ++i)
+      h += m_solver->get_assertion(i)->get_id();
+    std::cerr << h << "\n";
+#endif
+  }
 
   void include_ast_show(ast &a){
     a.show();

src/duality/duality_wrapper.h

@@ -393,6 +393,7 @@ namespace Duality {
       sort array_range() const;
     };
 
+    
     class func_decl : public ast {
     public:
         func_decl() : ast() {}
@@ -412,6 +413,7 @@ namespace Duality {
 
         expr operator()(unsigned n, expr const * args) const;
         expr operator()(const std::vector<expr> &args) const;
+        expr operator()() const;
         expr operator()(expr const & a) const;
         expr operator()(int a) const;
         expr operator()(expr const & a1, expr const & a2) const;
@@ -455,6 +457,8 @@ namespace Duality {
         bool is_quantifier() const {return raw()->get_kind() == AST_QUANTIFIER;}
         bool is_var() const {return raw()->get_kind() == AST_VAR;}
 	bool is_label (bool &pos,std::vector<symbol> &names) const ;
+	bool is_ground() const {return to_app(raw())->is_ground();}
+	bool has_quantifiers() const {return to_app(raw())->has_quantifiers();}
 
         // operator Z3_app() const { assert(is_app()); return reinterpret_cast<Z3_app>(m_ast); }
         func_decl decl() const {return func_decl(ctx(),to_app(raw())->get_decl());}
@@ -554,6 +558,8 @@ namespace Duality {
 
         expr simplify(params const & p) const;
 	
+        expr qe_lite() const;
+
 	friend expr clone_quantifier(const expr &, const expr &);
 
         friend expr clone_quantifier(const expr &q, const expr &b, const std::vector<expr> &patterns);
@@ -593,6 +599,36 @@ namespace Duality {
     };
     
 
+    typedef ::decl_kind pfrule;
+    
+    class proof : public ast {
+    public:
+      proof(context & c):ast(c) {}
+      proof(context & c, ::proof *s):ast(c, s) {}
+      proof(proof const & s):ast(s) {}
+      operator ::proof*() const { return to_app(raw()); }
+      proof & operator=(proof const & s) { return static_cast<proof&>(ast::operator=(s)); }
+
+      pfrule rule() const {
+	::func_decl *d = to_app(raw())->get_decl();
+	return d->get_decl_kind();
+      }
+
+      unsigned num_prems() const {
+	return to_app(raw())->get_num_args() - 1;
+      }
+      
+      expr conc() const {
+	return ctx().cook(to_app(raw())->get_arg(num_prems()));
+      }
+      
+      proof prem(unsigned i) const {
+	return proof(ctx(),to_app(to_app(raw())->get_arg(i)));
+      }
+      
+      void get_assumptions(std::vector<expr> &assumps);
+    };
+
 #if 0
 
 #if Z3_MAJOR_VERSION > 4 || Z3_MAJOR_VERSION == 4 && Z3_MINOR_VERSION >= 3
@@ -691,6 +727,7 @@ namespace Duality {
         }
         
         void show() const;
+	void show_hash() const;
 
         unsigned num_consts() const {return m_model.get()->get_num_constants();}
         unsigned num_funcs() const {return m_model.get()->get_num_functions();}
@@ -775,7 +812,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() {
@@ -867,6 +904,16 @@ namespace Duality {
 	  if(m_solver)
 	    m_solver->cancel();
 	}
+
+	unsigned get_scope_level(){return m_solver->get_scope_level();}
+
+	void show();
+	void show_assertion_ids();
+
+	proof get_proof(){
+	  return proof(ctx(),m_solver->get_proof());
+	}
+
     };
 
 #if 0
@@ -1144,6 +1191,9 @@ namespace Duality {
     inline expr func_decl::operator()(const std::vector<expr> &args) const {
       return operator()(args.size(),&args[0]);
     }
+    inline expr func_decl::operator()() const {
+      return operator()(0,0);
+    }
     inline expr func_decl::operator()(expr const & a) const {
       return operator()(1,&a);
     }
@@ -1199,6 +1249,8 @@ namespace Duality {
 
       inline expr getTerm(){return term;}
 
+      inline std::vector<expr> &getTerms(){return terms;}
+
       inline std::vector<TermTree *> &getChildren(){
 	return children;
       }
@@ -1216,6 +1268,8 @@ namespace Duality {
 
       inline void setTerm(expr t){term = t;}
       
+      inline void addTerm(expr t){terms.push_back(t);}
+
       inline void setChildren(const std::vector<TermTree *> & _children){
 	children = _children;
       }
@@ -1231,6 +1285,7 @@ namespace Duality {
 
     private:
       expr term;
+      std::vector<expr> terms;
       std::vector<TermTree *> children;
       int num;
     };
@@ -1277,6 +1332,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:
@@ -1331,7 +1387,8 @@ namespace std {
     class less<Duality::ast> {
   public:
     bool operator()(const Duality::ast &s, const Duality::ast &t) const {
-      return s.raw() < t.raw(); // s.raw()->get_id() < t.raw()->get_id();
+      // return s.raw() < t.raw();
+      return s.raw()->get_id() < t.raw()->get_id();
     }
   };
 }
@@ -1362,7 +1419,8 @@ namespace std {
     class less<Duality::func_decl> {
   public:
     bool operator()(const Duality::func_decl &s, const Duality::func_decl &t) const {
-      return s.raw() < t.raw(); // s.raw()->get_id() < t.raw()->get_id();
+      // return s.raw() < t.raw();
+      return s.raw()->get_id() < t.raw()->get_id();
     }
   };
 }

src/interp/iz3base.h

@@ -24,6 +24,16 @@ Revision History:
 #include "iz3mgr.h"
 #include "iz3scopes.h"
 
+namespace hash_space {
+  template <>
+    class hash<func_decl *> {
+  public:
+    size_t operator()(func_decl * const &s) const {
+      return (size_t) s;
+    }
+  };
+}
+
 /* Base class for interpolators. Includes an AST manager and a scoping
    object as bases. */
  
@@ -182,6 +192,4 @@ class iz3base : public iz3mgr, public scopes {
 
 
 
-
-
 #endif

src/interp/iz3foci.cpp

@@ -51,6 +51,13 @@ public:
   typedef hash_map<foci2::ast,ast> NodeToAst;
   NodeToAst node_to_ast;                    // maps Z3 ast's to foci expressions
 
+  // We only use this for FuncDeclToSymbol, which has no range destructor
+  struct symb_hash {
+    size_t operator()(const symb &s) const {
+      return (size_t) s;
+    }
+  };
+
   typedef hash_map<symb,foci2::symb> FuncDeclToSymbol; 
   FuncDeclToSymbol func_decl_to_symbol;     // maps Z3 func decls to symbols
 

src/interp/iz3hash.h

@@ -141,6 +141,7 @@ namespace std {
 
 #ifndef WIN32
 
+#if 0
 namespace stl_ext {
   template <class T>
     class hash<T *> {
@@ -150,6 +151,7 @@ namespace stl_ext {
     }
   };
 }
+#endif
 
 #endif
 

src/interp/iz3interp.cpp

@@ -75,15 +75,16 @@ struct frame_reducer : public iz3mgr {
     }
   }
   
-  void get_frames(const std::vector<ast> &z3_preds, 
+  void get_frames(const std::vector<std::vector<ast> >&z3_preds, 
 		  const std::vector<int> &orig_parents,
-		  std::vector<ast> &assertions,
+		  std::vector<std::vector<ast> >&assertions,
 		  std::vector<int> &parents,
 		  z3pf proof){
     frames = z3_preds.size();
     orig_parents_copy = orig_parents;
     for(unsigned i = 0; i < z3_preds.size(); i++)
-      frame_map[z3_preds[i]] = i;
+      for(unsigned j = 0; j < z3_preds[i].size(); j++)
+	frame_map[z3_preds[i][j]] = i;
     used_frames.resize(frames);
     hash_set<ast> memo;
     get_proof_assumptions_rec(proof,memo,used_frames);
@@ -202,7 +203,7 @@ public:
   }                         
 
   void proof_to_interpolant(z3pf proof,
-			    const std::vector<ast> &cnsts,
+			    const std::vector<std::vector<ast> > &cnsts,
 			    const std::vector<int> &parents,
 			    std::vector<ast> &interps,
 			    const std::vector<ast> &theory,
@@ -212,11 +213,12 @@ public:
     test_secondary(cnsts,parents,interps);
     return;
 #endif
+
     profiling::timer_start("Interpolation prep");
 
     // get rid of frames not used in proof
 
-    std::vector<ast> cnsts_vec;
+    std::vector<std::vector<ast> > cnsts_vec;
     std::vector<int> parents_vec;
     frame_reducer fr(*this);
     fr.get_frames(cnsts,parents,cnsts_vec,parents_vec,proof);
@@ -235,10 +237,7 @@ public:
 #define BINARY_INTERPOLATION
 #ifndef BINARY_INTERPOLATION    
     // create a translator
-    std::vector<std::vector<ast> > cnsts_vec_vec(cnsts_vec.size());
+    iz3translation *tr = iz3translation::create(*this,sp,cnsts_vec,parents_vec,theory);
-    for(unsigned i = 0; i < cnsts_vec.size(); i++)
-      cnsts_vec_vec[i].push_back(cnsts_vec[i]);
-    iz3translation *tr = iz3translation::create(*this,sp,cnsts_vec_vec,parents_vec,theory);
     tr_killer.set(tr);
     
     // set the translation options, if needed
@@ -273,7 +272,8 @@ public:
       std::vector<std::vector<ast> > cnsts_vec_vec(2);
       for(unsigned j = 0; j < cnsts_vec.size(); j++){
 	bool is_A = the_base.in_range(j,rng);
-	cnsts_vec_vec[is_A ? 0 : 1].push_back(cnsts_vec[j]);
+	for(unsigned k = 0; k < cnsts_vec[j].size(); k++)
+	  cnsts_vec_vec[is_A ? 0 : 1].push_back(cnsts_vec[j][k]);
       }
 
       killme<iz3translation> tr_killer_i;
@@ -308,6 +308,19 @@ public:
   }
 
 
+  void proof_to_interpolant(z3pf proof,
+			    std::vector<ast> &cnsts,
+			    const std::vector<int> &parents,
+			    std::vector<ast> &interps,
+			    const std::vector<ast> &theory,
+			    interpolation_options_struct *options = 0
+			    ){
+    std::vector<std::vector<ast> > cnsts_vec(cnsts.size());
+    for(unsigned i = 0; i < cnsts.size(); i++)
+      cnsts_vec[i].push_back(cnsts[i]);
+    proof_to_interpolant(proof,cnsts_vec,parents,interps,theory,options);
+  }    
+
   // same as above, but represents the tree using an ast
 
   void proof_to_interpolant(const z3pf &proof,
@@ -322,7 +335,6 @@ public:
     
     to_parents_vec_representation(_cnsts, tree, cnsts, parents, theory, pos_map);
 
-    
     //use the parents vector representation to compute interpolant
     proof_to_interpolant(proof,cnsts,parents,interps,theory,options);
     
@@ -397,6 +409,35 @@ void iz3interpolate(ast_manager &_m_manager,
     interps[i] = itp.uncook(_interps[i]);
 }
 
+void iz3interpolate(ast_manager &_m_manager,
+		    ast *proof,
+		    const ::vector<ptr_vector<ast> > &cnsts,
+		    const ::vector<int> &parents,
+		    ptr_vector<ast> &interps,
+		    const ptr_vector<ast> &theory,
+		    interpolation_options_struct * options)
+{
+  iz3interp itp(_m_manager);
+  if(options)
+    options->apply(itp);
+  std::vector<std::vector<iz3mgr::ast> > _cnsts(cnsts.size());
+  std::vector<int> _parents(parents.size());
+  std::vector<iz3mgr::ast> _interps;
+  std::vector<iz3mgr::ast> _theory(theory.size());
+  for(unsigned i = 0; i < cnsts.size(); i++)
+    for(unsigned j = 0; j < cnsts[i].size(); j++)
+      _cnsts[i].push_back(itp.cook(cnsts[i][j]));
+  for(unsigned i = 0; i < parents.size(); i++)
+    _parents[i] = parents[i];
+  for(unsigned i = 0; i < theory.size(); i++)
+    _theory[i] = itp.cook(theory[i]);
+  iz3mgr::ast _proof = itp.cook(proof);
+  itp.proof_to_interpolant(_proof,_cnsts,_parents,_interps,_theory,options);
+  interps.resize(_interps.size());
+  for(unsigned i = 0; i < interps.size(); i++)
+    interps[i] = itp.uncook(_interps[i]);
+}
+
 void iz3interpolate(ast_manager &_m_manager,
 		    ast *proof,
 		    const ptr_vector<ast> &cnsts,
@@ -461,5 +502,3 @@ void interpolation_options_struct::apply(iz3base &b){
     b.set_option((*it).first,(*it).second);
 }
 
-
-

src/interp/iz3interp.h

@@ -56,6 +56,16 @@ void iz3interpolate(ast_manager &_m_manager,
 		    const ptr_vector<ast> &theory,
 		    interpolation_options_struct * options = 0);
 
+/* Same as above, but each constraint is a vector of formulas. */
+
+void iz3interpolate(ast_manager &_m_manager,
+		    ast *proof,
+		    const vector<ptr_vector<ast> > &cnsts,
+		    const ::vector<int> &parents,
+		    ptr_vector<ast> &interps,
+		    const ptr_vector<ast> &theory,
+		    interpolation_options_struct * options = 0);
+
 /* Compute an interpolant from a proof. This version uses the ast
    representation, for compatibility with the new API. */
 

src/interp/iz3mgr.cpp

@@ -190,7 +190,7 @@ iz3mgr::ast iz3mgr::make_quant(opr op, const std::vector<ast> &bvs, ast &body){
 			     op == Forall, 
 			     names.size(), &types[0], &names[0], abs_body.get(),            
 			     0, 
-			     symbol(),
+			     symbol("itp"),
 			     symbol(),
 			     0, 0,
 			     0, 0
@@ -761,6 +761,19 @@ int iz3mgr::occurs_in(ast var, ast e){
 }
 
 
+bool iz3mgr::solve_arith(const ast &v, const ast &x, const ast &y, ast &res){
+  if(op(x) == Plus){
+    int n = num_args(x);
+    for(int i = 0; i < n; i++){
+      if(arg(x,i) == v){
+	res = z3_simplify(make(Sub, y, make(Sub, x, v)));
+	return true;
+      }
+    }
+  }
+  return false;
+}
+
 // find a controlling equality for a given variable v in a term
 // a controlling equality is of the form v = t, which, being
 // false would force the formula to have the specifid truth value
@@ -774,6 +787,9 @@ iz3mgr::ast iz3mgr::cont_eq(stl_ext::hash_set<ast> &cont_eq_memo, bool truth, as
   if(!truth && op(e) == Equal){
     if(arg(e,0) == v) return(arg(e,1));
     if(arg(e,1) == v) 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;
   }
   if((!truth && op(e) == And) || (truth && op(e) == Or)){
     int nargs = num_args(e);
@@ -815,11 +831,35 @@ iz3mgr::ast iz3mgr::subst(ast var, ast t, ast e){
   return subst(memo,var,t,e);
 }
 
+iz3mgr::ast iz3mgr::subst(stl_ext::hash_map<ast,ast> &subst_memo,ast e){
+  std::pair<ast,ast> foo(e,ast());
+  std::pair<hash_map<ast,ast>::iterator,bool> bar = subst_memo.insert(foo);
+  ast &res = bar.first->second;
+  if(bar.second){
+    int nargs = num_args(e);
+    std::vector<ast> args(nargs);
+    for(int i = 0; i < nargs; i++)
+      args[i] = subst(subst_memo,arg(e,i));
+    opr f = op(e);
+    if(f == Equal && args[0] == args[1]) res = mk_true();
+    else res = clone(e,args);
+  }
+  return res;
+}
+
   // apply a quantifier to a formula, with some optimizations
   // 1) bound variable does not occur -> no quantifier
   // 2) bound variable must be equal to some term -> substitute
 
 iz3mgr::ast iz3mgr::apply_quant(opr quantifier, ast var, ast e){
+  if((quantifier == Forall && op(e) == And)
+     || (quantifier == Exists && op(e) == Or)){
+    int n = num_args(e);
+    std::vector<ast> args(n);
+    for(int i = 0; i < n; i++)
+      args[i] = apply_quant(quantifier,var,arg(e,i));
+    return make(op(e),args);
+  }
   if(!occurs_in(var,e))return e;
   hash_set<ast> cont_eq_memo; 
   ast cterm = cont_eq(cont_eq_memo, quantifier == Forall, var, e);

src/interp/iz3mgr.h

@@ -65,7 +65,7 @@ class ast_i {
     return _ast == other._ast;
   }
   bool lt(const ast_i &other) const {
-    return _ast < other._ast;
+    return _ast->get_id() < other._ast->get_id();
   }
   friend bool operator==(const ast_i &x, const ast_i&y){
     return x.eq(y);
@@ -76,7 +76,7 @@ class ast_i {
   friend bool operator<(const ast_i &x, const ast_i&y){
     return x.lt(y);
   }
-  size_t hash() const {return (size_t)_ast;}
+  size_t hash() const {return _ast->get_id();}
   bool null() const {return !_ast;}
 };
 
@@ -140,7 +140,8 @@ namespace std {
     class less<ast_r> {
   public:
     bool operator()(const ast_r &s, const ast_r &t) const {
-      return s.raw() < t.raw(); // s.raw()->get_id() < t.raw()->get_id();
+      // return s.raw() < t.raw(); 
+      return s.raw()->get_id() < t.raw()->get_id();
     }
   };
 }
@@ -359,6 +360,12 @@ class iz3mgr  {
     return fid == m().get_basic_family_id() && k == BOOL_SORT;
   }
 
+  bool is_array_type(type t){
+    family_id fid = to_sort(t)->get_family_id(); 
+    decl_kind k = to_sort(t)->get_decl_kind();
+    return fid == m_array_fid && k == ARRAY_SORT;
+  }
+
   type get_range_type(symb s){
     return to_func_decl(s)->get_range();
   }
@@ -631,6 +638,9 @@ class iz3mgr  {
   
   ast subst(ast var, ast t, ast e);
 
+  // apply a substitution defined by a map
+  ast subst(stl_ext::hash_map<ast,ast> &map, ast e);
+
   // apply a quantifier to a formula, with some optimizations
   // 1) bound variable does not occur -> no quantifier
   // 2) bound variable must be equal to some term -> substitute
@@ -683,13 +693,14 @@ class iz3mgr  {
 
  protected:
   ast_manager &m_manager;
+  int occurs_in(ast var, ast e);
 
  private:
   ast mki(family_id fid, decl_kind sk, int n, raw_ast **args);
   ast make(opr op, int n, raw_ast **args);
   ast make(symb sym, int n, raw_ast **args);
   int occurs_in1(stl_ext::hash_map<ast,bool> &occurs_in_memo, ast var, ast e);
-  int occurs_in(ast var, ast e);
+  bool solve_arith(const ast &v, const ast &x, const ast &y, ast &res);
   ast cont_eq(stl_ext::hash_set<ast> &cont_eq_memo, bool truth, ast v, ast e);
   ast subst(stl_ext::hash_map<ast,ast> &subst_memo, ast var, ast t, ast e);
 

src/interp/iz3pp.cpp

@@ -40,6 +40,20 @@ Revision History:
 using namespace stl_ext;
 #endif
 
+#ifndef WIN32
+// We promise not to use this for hash_map with range destructor
+namespace stl_ext {
+  template <>
+    class hash<expr *> {
+  public:
+    size_t operator()(const expr *p) const {
+      return (size_t) p;
+    }
+  };
+}
+#endif
+
+
 // TBD: algebraic data-types declarations will not be printed.
 class free_func_visitor {
   ast_manager& m;

src/interp/iz3proof_itp.cpp

@@ -118,6 +118,30 @@ class iz3proof_itp_impl : public iz3proof_itp {
      where t is an arbitrary term */
   symb rewrite_B;
 
+  /* a normalization step is of the form (lhs=rhs) : proof, where "proof"
+     is a proof of lhs=rhs and lhs is a mixed term. If rhs is a mixed term
+     then it must have a greater index than lhs. */
+  symb normal_step;
+
+  /* A chain of normalization steps is either "true" (the null chain)
+     or normal_chain(<step> <tail>), where step is a normalization step
+     and tail is a normalization chain. The lhs of <step> must have
+     a less term index than any lhs in the chain. Moreover, the rhs of
+     <step> may not occur as the lhs of step in <tail>. If we wish to
+     add lhs=rhs to the beginning of <tail> and rhs=rhs' occurs in <tail>
+     we must apply transitivity, transforming <step> to lhs=rhs'. */
+
+  symb normal_chain;
+
+  /* If p is a proof of Q and c is a normalization chain, then normal(p,c)
+     is a proof of Q(c) (that is, Q with all substitutions in c performed). */
+  
+  symb normal;
+
+  /** Stand-ins for quantifiers */
+
+  symb sforall, sexists;
+
 
   ast get_placeholder(ast t){
     hash_map<ast,ast>::iterator it = placeholders.find(t);
@@ -209,6 +233,10 @@ class iz3proof_itp_impl : public iz3proof_itp {
     ast neg_pivot_lit = mk_not(atom);
     if(op(pivot) != Not)
       std::swap(premise1,premise2);
+    if(op(pivot) == Equal && op(arg(pivot,0)) == Select && op(arg(pivot,1)) == Select){
+      neg_pivot_lit = mk_not(neg_pivot_lit);
+      std::swap(premise1,premise2);
+    }      
     return resolve_arith_rec1(memo, neg_pivot_lit, premise1, premise2);
   }
   
@@ -333,9 +361,15 @@ class iz3proof_itp_impl : public iz3proof_itp {
 	break;
       }
       default:
+	{
+	  symb s = sym(itp2);
+	  if(s == sforall || s == sexists)
+	    res = make(s,arg(itp2,0),resolve_arith_rec2(memo, pivot1, conj1, arg(itp2,1)));
+	  else
 	    res = itp2;
 	}
       }
+    }
     return res;
   }
 
@@ -363,9 +397,15 @@ class iz3proof_itp_impl : public iz3proof_itp {
 	break;
       }
       default:
+	{
+	  symb s = sym(itp1);
+	  if(s == sforall || s == sexists)
+	    res = make(s,arg(itp1,0),resolve_arith_rec1(memo, neg_pivot_lit, arg(itp1,1), itp2));
+	  else
 	    res = itp1;
 	}
       }
+    }
     return res;
   }
 
@@ -451,7 +491,12 @@ class iz3proof_itp_impl : public iz3proof_itp {
   hash_map<ast,ast> simplify_memo;
 
   ast simplify(const ast &t){
-    return simplify_rec(t);
+    ast res = normalize(simplify_rec(t));
+#ifdef BOGUS_QUANTS
+    if(localization_vars.size())
+      res = add_quants(z3_simplify(res));
+#endif
+    return res;
   }
 
   ast simplify_rec(const ast &e){
@@ -521,12 +566,18 @@ class iz3proof_itp_impl : public iz3proof_itp {
     throw cannot_simplify();
   }
 
+  bool is_normal_ineq(const ast &ineq){
+    if(sym(ineq) == normal)
+      return is_ineq(arg(ineq,0));
+    return is_ineq(ineq);
+  }
+
   ast simplify_sum(std::vector<ast> &args){
-    ast cond = mk_true();
+    ast Aproves = mk_true(), Bproves = mk_true();
     ast ineq = args[0];
-    if(!is_ineq(ineq)) throw cannot_simplify();
+    if(!is_normal_ineq(ineq)) throw cannot_simplify();
-    sum_cond_ineq(ineq,cond,args[1],args[2]);
+    sum_cond_ineq(ineq,args[1],args[2],Aproves,Bproves);
-    return my_implies(cond,ineq);
+    return my_and(Aproves,my_implies(Bproves,ineq));
   }
 
   ast simplify_rotate_sum(const ast &pl, const ast &pf){
@@ -539,8 +590,10 @@ class iz3proof_itp_impl : public iz3proof_itp {
     return sym(chain) == concat;
   }
   
-  ast ineq_from_chain(const ast &chain, ast &cond){
+#if 0
-    if(is_rewrite_chain(chain)){
+  ast ineq_from_chain_simple(const ast &chain, ast &cond){
+    if(is_true(chain))
+      return chain;
     ast last = chain_last(chain);
     ast rest = chain_rest(chain);
     if(is_true(rest) && is_rewrite_side(LitA,last)
@@ -549,19 +602,30 @@ class iz3proof_itp_impl : public iz3proof_itp {
       return rewrite_rhs(last);
     }
     if(is_rewrite_side(LitB,last) && is_true(rewrite_cond(last)))
-	return ineq_from_chain(rest,cond);
+      return ineq_from_chain_simple(rest,cond);
+    return chain;
   }
+#endif
+
+  ast ineq_from_chain(const ast &chain, ast &Aproves, ast &Bproves){
+    if(is_rewrite_chain(chain))
+      return rewrite_chain_to_normal_ineq(chain,Aproves,Bproves);
     return chain;
   }
 
-  void sum_cond_ineq(ast &ineq, ast &cond, const ast &coeff2, const ast &ineq2){
+
+  void sum_cond_ineq(ast &ineq, const ast &coeff2, const ast &ineq2, ast &Aproves, ast &Bproves){
     opr o = op(ineq2);
     if(o == Implies){
-      sum_cond_ineq(ineq,cond,coeff2,arg(ineq2,1));
+      sum_cond_ineq(ineq,coeff2,arg(ineq2,1),Aproves,Bproves);
-      cond = my_and(cond,arg(ineq2,0));
+      Bproves = my_and(Bproves,arg(ineq2,0));
     }
     else {
-      ast the_ineq = ineq_from_chain(ineq2,cond);
+      ast the_ineq = ineq_from_chain(ineq2,Aproves,Bproves);
+      if(sym(ineq) == normal || sym(the_ineq) == normal){
+	sum_normal_ineq(ineq,coeff2,the_ineq,Aproves,Bproves);
+	return;
+      }
       if(is_ineq(the_ineq))
 	linear_comb(ineq,coeff2,the_ineq);
       else 
@@ -569,6 +633,27 @@ class iz3proof_itp_impl : public iz3proof_itp {
     }
   }
   
+  void destruct_normal(const ast &pf, ast &p, ast &n){
+    if(sym(pf) == normal){
+      p = arg(pf,0);
+      n = arg(pf,1);
+    }
+    else {
+      p = pf;
+      n = mk_true();
+    }
+  }
+
+  void sum_normal_ineq(ast &ineq, const ast &coeff2, const ast &ineq2, ast &Aproves, ast &Bproves){
+    ast in1,in2,n1,n2;
+    destruct_normal(ineq,in1,n1);
+    destruct_normal(ineq2,in2,n2);
+    ast dummy1, dummy2;
+    sum_cond_ineq(in1,coeff2,in2,dummy1,dummy2);
+    n1 = merge_normal_chains(n1,n2, Aproves, Bproves);
+    ineq = make_normal(in1,n1);
+  }
+
   bool is_ineq(const ast &ineq){
     opr o = op(ineq);
     if(o == Not) o = op(arg(ineq,0));
@@ -577,6 +662,12 @@ class iz3proof_itp_impl : public iz3proof_itp {
 
   // divide both sides of inequality by a non-negative integer divisor
   ast idiv_ineq(const ast &ineq1, const ast &divisor){
+    if(sym(ineq1) == normal){
+      ast in1,n1;
+      destruct_normal(ineq1,in1,n1);
+      in1 = idiv_ineq(in1,divisor);
+      return make_normal(in1,n1);
+    }
     if(divisor == make_int(rational(1)))
       return ineq1;
     ast ineq = ineq1;
@@ -585,17 +676,23 @@ class iz3proof_itp_impl : public iz3proof_itp {
     return make(op(ineq),mk_idiv(arg(ineq,0),divisor),mk_idiv(arg(ineq,1),divisor));
   }
   
-  ast rotate_sum_rec(const ast &pl, const ast &pf, ast &cond, ast &ineq){
+  ast rotate_sum_rec(const ast &pl, const ast &pf, ast &Bproves, ast &ineq){
     if(pf == pl)
-      return my_implies(cond,simplify_ineq(ineq));
+      return my_implies(Bproves,simplify_ineq(ineq));
     if(op(pf) == Uninterpreted && sym(pf) == sum){
       if(arg(pf,2) == pl){
-	sum_cond_ineq(ineq,cond,make_int("1"),arg(pf,0));
+	ast Aproves = mk_true();
+	sum_cond_ineq(ineq,make_int("1"),arg(pf,0),Aproves,Bproves);
+	if(!is_true(Aproves))
+	  throw "help!";
 	ineq = idiv_ineq(ineq,arg(pf,1));
-	return my_implies(cond,ineq);
+	return my_implies(Bproves,ineq);
       }
-      sum_cond_ineq(ineq,cond,arg(pf,1),arg(pf,2));
+      ast Aproves = mk_true();
-      return rotate_sum_rec(pl,arg(pf,0),cond,ineq);
+      sum_cond_ineq(ineq,arg(pf,1),arg(pf,2),Aproves,Bproves);
+      if(!is_true(Aproves))
+	throw "help!";
+      return rotate_sum_rec(pl,arg(pf,0),Bproves,ineq);
     }
     throw cannot_simplify();
   }
@@ -605,28 +702,30 @@ class iz3proof_itp_impl : public iz3proof_itp {
       ast equality = arg(neg_equality,0);
       ast x = arg(equality,0);
       ast y = arg(equality,1);
-      ast cond1 = mk_true();
+      ast Aproves1 = mk_true(), Bproves1 = mk_true();
-      ast xleqy = round_ineq(ineq_from_chain(arg(pf,1),cond1));
+      ast xleqy = round_ineq(ineq_from_chain(arg(pf,1),Aproves1,Bproves1));
-      ast yleqx = round_ineq(ineq_from_chain(arg(pf,2),cond1));
+      ast yleqx = round_ineq(ineq_from_chain(arg(pf,2),Aproves1,Bproves1));
       ast ineq1 = make(Leq,make_int("0"),make_int("0"));
-      sum_cond_ineq(ineq1,cond1,make_int("-1"),xleqy);
+      sum_cond_ineq(ineq1,make_int("-1"),xleqy,Aproves1,Bproves1);
-      sum_cond_ineq(ineq1,cond1,make_int("-1"),yleqx);
+      sum_cond_ineq(ineq1,make_int("-1"),yleqx,Aproves1,Bproves1);
-      cond1 = my_and(cond1,z3_simplify(ineq1));
+      Bproves1 = my_and(Bproves1,z3_simplify(ineq1));
-      ast cond2 = mk_true();
+      ast Aproves2 = mk_true(), Bproves2 = mk_true();
       ast ineq2 = make(Leq,make_int("0"),make_int("0"));
-      sum_cond_ineq(ineq2,cond2,make_int("1"),xleqy);
+      sum_cond_ineq(ineq2,make_int("1"),xleqy,Aproves2,Bproves2);
-      sum_cond_ineq(ineq2,cond2,make_int("1"),yleqx);
+      sum_cond_ineq(ineq2,make_int("1"),yleqx,Aproves2,Bproves2);
-      cond2 = z3_simplify(ineq2);
+      Bproves2 = z3_simplify(ineq2);
+      if(!is_true(Aproves1) || !is_true(Aproves2))
+	throw "help!";
       if(get_term_type(x) == LitA){
 	ast iter = z3_simplify(make(Plus,x,get_ineq_rhs(xleqy)));
-	ast rewrite1 = make_rewrite(LitA,top_pos,cond1,make(Equal,x,iter));
+	ast rewrite1 = make_rewrite(LitA,top_pos,Bproves1,make(Equal,x,iter));
-	ast rewrite2 = make_rewrite(LitB,top_pos,cond2,make(Equal,iter,y));
+	ast rewrite2 = make_rewrite(LitB,top_pos,Bproves2,make(Equal,iter,y));
 	return chain_cons(chain_cons(mk_true(),rewrite1),rewrite2);
       }
       if(get_term_type(y) == LitA){
 	ast iter = z3_simplify(make(Plus,y,get_ineq_rhs(yleqx)));
-	ast rewrite2 = make_rewrite(LitA,top_pos,cond1,make(Equal,iter,y));
+	ast rewrite2 = make_rewrite(LitA,top_pos,Bproves1,make(Equal,iter,y));
-	ast rewrite1 = make_rewrite(LitB,top_pos,cond2,make(Equal,x,iter));
+	ast rewrite1 = make_rewrite(LitB,top_pos,Bproves2,make(Equal,x,iter));
 	return chain_cons(chain_cons(mk_true(),rewrite1),rewrite2);
       }
       throw cannot_simplify();
@@ -649,12 +748,19 @@ class iz3proof_itp_impl : public iz3proof_itp {
       ast equa = sep_cond(arg(pf,0),cond);
       if(is_equivrel_chain(equa)){
 	ast lhs,rhs; eq_from_ineq(arg(neg_equality,0),lhs,rhs); // get inequality we need to prove
+	LitType lhst = get_term_type(lhs), rhst = get_term_type(rhs);
+	if(lhst != LitMixed && rhst != LitMixed){
 	  ast ineqs= chain_ineqs(op(arg(neg_equality,0)),LitA,equa,lhs,rhs); // chain must be from lhs to rhs
 	  cond = my_and(cond,chain_conditions(LitA,equa)); 
-	ast Bconds = chain_conditions(LitB,equa); 
+	  ast Bconds = z3_simplify(chain_conditions(LitB,equa)); 
 	  if(is_true(Bconds) && op(ineqs) != And)
 	    return my_implies(cond,ineqs);
 	}
+	else {
+	  ast itp = make(Leq,make_int(rational(0)),make_int(rational(0)));
+	  return make_normal(itp,cons_normal(fix_normal(lhs,rhs,equa),mk_true()));
+	}
+      }
     }
     throw cannot_simplify();
   }
@@ -757,11 +863,57 @@ class iz3proof_itp_impl : public iz3proof_itp {
 	chain = concat_rewrite_chain(chain,split[1]);
       }
     }
-    else // if not an equivalence, must be of form T <-> pred
+    else { // if not an equivalence, must be of form T <-> pred
       chain = concat_rewrite_chain(P,PeqQ);
+    }
     return chain;
   }
 
+  void get_subterm_normals(const ast &ineq1, const ast &ineq2, const ast &chain, ast &normals,
+			   const ast &pos, hash_set<ast> &memo, ast &Aproves, ast &Bproves){
+    opr o1 = op(ineq1);
+    opr o2 = op(ineq2);
+    if(o1 == Not || o1 == Leq || o1 == Lt || o1 == Geq || o1 == Gt || o1 == Plus || o1 == Times){
+      int n = num_args(ineq1);
+      if(o2 != o1 || num_args(ineq2) != n)
+	throw "bad inequality rewriting";
+      for(int i = 0; i < n; i++){
+	ast new_pos = add_pos_to_end(pos,i);
+	get_subterm_normals(arg(ineq1,i), arg(ineq2,i), chain, normals, new_pos, memo, Aproves, Bproves);
+      }
+    }
+    else if(get_term_type(ineq2) == LitMixed && memo.find(ineq2) == memo.end()){
+      memo.insert(ineq2);
+      ast sub_chain = extract_rewrites(chain,pos);
+      if(is_true(sub_chain))
+	throw "bad inequality rewriting";
+      ast new_normal = make_normal_step(ineq2,ineq1,reverse_chain(sub_chain));
+      normals = merge_normal_chains(normals,cons_normal(new_normal,mk_true()), Aproves, Bproves);
+    } 
+  }
+
+  ast rewrite_chain_to_normal_ineq(const ast &chain, ast &Aproves, ast &Bproves){
+    ast tail, pref = get_head_chain(chain,tail,false); // pref  is x=y, tail is x=y -> x'=y'
+    ast head = chain_last(pref);
+    ast ineq1 = rewrite_rhs(head);
+    ast ineq2 = apply_rewrite_chain(ineq1,tail);
+    ast nc = mk_true();
+    hash_set<ast> memo;
+    get_subterm_normals(ineq1,ineq2,tail,nc,top_pos,memo, Aproves, Bproves);
+    ast itp;
+    if(is_rewrite_side(LitA,head)){
+      itp = ineq1;
+      ast mc = z3_simplify(chain_side_proves(LitB,pref));
+      Bproves = my_and(Bproves,mc);
+    }
+    else {
+      itp = make(Leq,make_int(rational(0)),make_int(rational(0)));
+      ast mc = z3_simplify(chain_side_proves(LitA,pref));
+      Aproves = my_and(Aproves,mc);
+    }
+    return make_normal(itp,nc);
+  }
+
   /* Given a chain rewrite chain deriving not P and a rewrite chain deriving P, return an interpolant. */
   ast contra_chain(const ast &neg_chain, const ast &pos_chain){
     // equality is a special case. we use the derivation of x=y to rewrite not(x=y) to not(y=y)
@@ -790,11 +942,18 @@ class iz3proof_itp_impl : public iz3proof_itp {
   }
 
   ast simplify_modpon(const std::vector<ast> &args){
-    ast cond = mk_true();
+    ast Aproves = mk_true(), Bproves = mk_true();
-    ast chain = simplify_modpon_fwd(args,cond);
+    ast chain = simplify_modpon_fwd(args,Bproves);
-    ast Q2 = sep_cond(args[2],cond);
+    ast Q2 = sep_cond(args[2],Bproves);
-    ast interp = is_negation_chain(chain) ? contra_chain(chain,Q2) : contra_chain(Q2,chain);
+    ast interp;
-    return my_implies(cond,interp);
+    if(is_normal_ineq(Q2)){ // inequalities are special
+      ast nQ2 = rewrite_chain_to_normal_ineq(chain,Aproves,Bproves);
+      sum_cond_ineq(nQ2,make_int(rational(1)),Q2,Aproves,Bproves);
+      interp = normalize(nQ2);
+    }
+    else 
+      interp = is_negation_chain(chain) ? contra_chain(chain,Q2) : contra_chain(Q2,chain);
+    return my_and(Aproves,my_implies(Bproves,interp));
   }
 
 
@@ -1035,6 +1194,12 @@ class iz3proof_itp_impl : public iz3proof_itp {
     return make(add_pos,make_int(rational(arg)),pos);
   }
 
+  ast add_pos_to_end(const ast &pos, int i){
+    if(pos == top_pos)
+      return pos_add(i,pos);
+    return make(add_pos,arg(pos,0),add_pos_to_end(arg(pos,1),i));
+  }
+
   /* return the argument number of position, if not top */
   int pos_arg(const ast &pos){
     rational r;
@@ -1170,6 +1335,10 @@ class iz3proof_itp_impl : public iz3proof_itp {
     return make(sym(rew),pos_add(apos,arg(rew,0)),arg(rew,1),arg(rew,2));
   }
 
+  ast rewrite_pos_set(const ast &pos, const ast &rew){
+    return make(sym(rew),pos,arg(rew,1),arg(rew,2));
+  }
+
   ast rewrite_up(const ast &rew){
     return make(sym(rew),arg(arg(rew,0),1),arg(rew,1),arg(rew,2));
   }
@@ -1317,6 +1486,28 @@ class iz3proof_itp_impl : public iz3proof_itp {
     split_chain_rec(chain,res);
   }
 
+  ast extract_rewrites(const ast &chain, const ast &pos){
+    if(is_true(chain))
+      return chain;
+    ast last = chain_last(chain);
+    ast rest = chain_rest(chain);
+    ast new_rest = extract_rewrites(rest,pos);
+    ast p1 = rewrite_pos(last);
+    ast diff;
+    switch(pos_diff(p1,pos,diff)){
+    case -1: {
+      ast new_last = rewrite_pos_set(diff, last);
+      return chain_cons(new_rest,new_last);
+    }
+    case 1:
+      if(rewrite_lhs(last) != rewrite_rhs(last))
+	throw "bad rewrite chain";
+      break;
+    default:;
+    }
+    return new_rest;
+  }
+
   ast down_chain(const ast &chain){
     ast split[2];
     split_chain(chain,split);
@@ -1381,7 +1572,7 @@ class iz3proof_itp_impl : public iz3proof_itp {
     //    ast s = ineq_to_lhs(ineq);
     // ast srhs = arg(s,1);
     ast srhs = arg(ineq,0);
-    if(op(srhs) == Plus && num_args(srhs) == 2){
+    if(op(srhs) == Plus && num_args(srhs) == 2 && arg(ineq,1) == make_int(rational(0))){
       lhs = arg(srhs,0);
       rhs = arg(srhs,1);
       // if(op(lhs) == Times)
@@ -1393,6 +1584,11 @@ class iz3proof_itp_impl : public iz3proof_itp {
 	return;
       }
     }
+    if(op(ineq) == Leq || op(ineq) == Geq){
+      lhs = srhs;
+      rhs = arg(ineq,1);
+      return;
+    }
     throw "bad ineq";
   }
 
@@ -1404,6 +1600,203 @@ class iz3proof_itp_impl : public iz3proof_itp {
     return chain_cons(rest,last);
   }
 
+  ast apply_rewrite_chain(const ast &t, const ast &chain){
+    if(is_true(chain))
+      return t;
+    ast last = chain_last(chain);
+    ast rest = chain_rest(chain);
+    ast mid = apply_rewrite_chain(t,rest);
+    ast res = subst_in_pos(mid,rewrite_pos(last),rewrite_rhs(last));
+    return res;
+  }
+
+  ast drop_rewrites(LitType t, const ast &chain, ast &remainder){
+    if(!is_true(chain)){
+      ast last = chain_last(chain);
+      ast rest = chain_rest(chain);
+      if(is_rewrite_side(t,last)){
+	ast res = drop_rewrites(t,rest,remainder);
+	remainder = chain_cons(remainder,last);
+	return res;
+      }
+    }
+    remainder = mk_true();
+    return chain;
+  }
+
+  // Normalization chains
+
+  ast cons_normal(const ast &first, const ast &rest){
+    return make(normal_chain,first,rest);
+  }
+  
+  ast normal_first(const ast &t){
+    return arg(t,0);
+  }
+
+  ast normal_rest(const ast &t){
+    return arg(t,1);
+  }
+
+  ast normal_lhs(const ast &t){
+    return arg(arg(t,0),0);
+  }
+
+  ast normal_rhs(const ast &t){
+    return arg(arg(t,0),1);
+  }
+
+  ast normal_proof(const ast &t){
+    return arg(t,1);
+  }
+
+  ast make_normal_step(const ast &lhs, const ast &rhs, const ast &proof){
+    return make(normal_step,make_equiv(lhs,rhs),proof);
+  }
+
+  ast make_normal(const ast &ineq, const ast &nrml){
+    if(!is_ineq(ineq))
+      throw "what?";
+    return make(normal,ineq,nrml);
+  }
+
+  ast fix_normal(const ast &lhs, const ast &rhs, const ast &proof){
+    LitType rhst = get_term_type(rhs);
+    if(rhst != LitMixed || ast_id(lhs) < ast_id(rhs))
+      return make_normal_step(lhs,rhs,proof);
+    else
+      return make_normal_step(rhs,lhs,reverse_chain(proof));
+  }
+
+  ast chain_side_proves(LitType side, const ast &chain){
+    LitType other_side = side == LitA ? LitB : LitA;
+    return my_and(chain_conditions(other_side,chain),my_implies(chain_conditions(side,chain),chain_formulas(side,chain)));
+  }
+
+  // Merge two normalization chains
+  ast merge_normal_chains_rec(const ast &chain1, const ast &chain2, hash_map<ast,ast> &trans, ast &Aproves, ast &Bproves){
+    if(is_true(chain1))
+      return chain2;
+    if(is_true(chain2))
+      return chain1;
+    ast f1 = normal_first(chain1);
+    ast f2 = normal_first(chain2);
+    ast lhs1 = normal_lhs(f1);
+    ast lhs2 = normal_lhs(f2);
+    int id1 = ast_id(lhs1);
+    int id2 = ast_id(lhs2);
+    if(id1 < id2) return cons_normal(f1,merge_normal_chains_rec(normal_rest(chain1),chain2,trans,Aproves,Bproves));
+    if(id2 < id1) return cons_normal(f2,merge_normal_chains_rec(chain1,normal_rest(chain2),trans,Aproves,Bproves));
+    ast rhs1 = normal_rhs(f1);
+    ast rhs2 = normal_rhs(f2);
+    LitType t1 = get_term_type(rhs1);
+    LitType t2 = get_term_type(rhs2);
+    int tid1 = ast_id(rhs1);
+    int tid2 = ast_id(rhs2);
+    ast pf1 = normal_proof(f1);
+    ast pf2 = normal_proof(f2);
+    ast new_normal;
+    if(t1 == LitMixed && (t2 != LitMixed || tid2 > tid1)){
+      ast new_proof = concat_rewrite_chain(reverse_chain(pf1),pf2);
+      new_normal = f2;
+      trans[rhs1] = make_normal_step(rhs1,rhs2,new_proof);
+    }
+    else if(t2 == LitMixed && (t1 != LitMixed || tid1 > tid2))
+      return merge_normal_chains_rec(chain2,chain1,trans,Aproves,Bproves);
+    else if(t1 == LitA && t2 == LitB){
+      ast new_proof = concat_rewrite_chain(reverse_chain(pf1),pf2);
+      ast Bproof, Aproof = drop_rewrites(LitB,new_proof,Bproof);
+      ast mcA = chain_side_proves(LitB,Aproof);
+      Bproves = my_and(Bproves,mcA);
+      ast mcB = chain_side_proves(LitA,Bproof);
+      Aproves = my_and(Aproves,mcB);
+      ast rep = apply_rewrite_chain(rhs1,Aproof);
+      new_proof = concat_rewrite_chain(pf1,Aproof);
+      new_normal = make_normal_step(rhs1,rep,new_proof);
+    }
+    else if(t1 == LitA && t2 == LitB)
+      return merge_normal_chains_rec(chain2,chain1,trans,Aproves,Bproves);
+    else if(t1 == LitA) {
+      ast new_proof = concat_rewrite_chain(reverse_chain(pf1),pf2);
+      ast mc = chain_side_proves(LitB,new_proof);
+      Bproves = my_and(Bproves,mc);
+      new_normal = f1; // choice is arbitrary
+    }
+    else { /* t1 = t2 = LitB */
+      ast new_proof = concat_rewrite_chain(reverse_chain(pf1),pf2);
+      ast mc = chain_side_proves(LitA,new_proof);
+      Aproves = my_and(Aproves,mc);
+      new_normal = f1; // choice is arbitrary
+    }
+    return cons_normal(new_normal,merge_normal_chains_rec(normal_rest(chain1),normal_rest(chain2),trans,Aproves,Bproves));
+  }
+
+  ast trans_normal_chain(const ast &chain, hash_map<ast,ast> &trans){
+    if(is_true(chain))
+      return chain;
+    ast f = normal_first(chain);
+    ast r = normal_rest(chain);
+    ast rhs = normal_rhs(f);
+    hash_map<ast,ast>::iterator it = trans.find(rhs);
+    ast new_normal;
+    if(it != trans.end()){
+      const ast &f2 = it->second;
+      ast pf = concat_rewrite_chain(normal_proof(f),normal_proof(f2));
+      new_normal = make_normal_step(normal_lhs(f),normal_rhs(f2),pf);
+    }
+    else
+      new_normal = f;
+    return cons_normal(new_normal,trans_normal_chain(r,trans));
+  }
+
+  ast merge_normal_chains(const ast &chain1, const ast &chain2, ast &Aproves, ast &Bproves){
+    hash_map<ast,ast> trans;
+    ast res = merge_normal_chains_rec(chain1,chain2,trans,Aproves,Bproves);
+    res = trans_normal_chain(res,trans);
+    return res;
+  }
+      
+  bool destruct_cond_ineq(ast t, ast &Aproves, ast &Bproves, ast&ineq){
+    if(op(t) == And){
+      Aproves = arg(t,0);
+      t = arg(t,1);
+    }
+    else
+      Aproves = mk_true();
+    if(op(t) == Implies){
+      Bproves = arg(t,0);
+      t = arg(t,1);
+    }
+    else
+      Bproves = mk_true();
+    if(is_normal_ineq(t)){
+      ineq = t;
+      return true;
+    }
+    return false;
+  }
+
+  ast cons_cond_ineq(const ast &Aproves, const ast &Bproves, const ast &ineq){
+    return my_and(Aproves,my_implies(Bproves,ineq));
+  }
+
+  ast normalize(const ast &ct){
+    ast Aproves,Bproves,t;
+    if(!destruct_cond_ineq(ct,Aproves,Bproves,t))
+      return ct;
+    if(sym(t) != normal)
+      return ct;
+    ast chain = arg(t,1);
+    hash_map<ast,ast> map;
+    for(ast c = chain; !is_true(c); c = normal_rest(c)){
+      ast first = normal_first(c);
+      ast lhs = normal_lhs(first);
+      ast rhs = normal_rhs(first);
+      map[lhs] = rhs;
+    }
+    ast res = subst(map,arg(t,0));
+    return cons_cond_ineq(Aproves,Bproves,res);
+  }
   
   /** Make an assumption node. The given clause is assumed in the given frame. */
   virtual node make_assumption(int frame, const std::vector<ast> &assumption){
@@ -1522,9 +1915,22 @@ class iz3proof_itp_impl : public iz3proof_itp {
     return itp;
   }
 
+  ast capture_localization(ast e){
+    // #define CAPTURE_LOCALIZATION
+#ifdef CAPTURE_LOCALIZATION
+    for(int i = localization_vars.size() - 1; i >= 0; i--){
+      LocVar &lv = localization_vars[i];
+      if(occurs_in(lv.var,e)){
+	symb q = (pv->in_range(lv.frame,rng)) ? sexists : sforall; 
+	e = make(q,make(Equal,lv.var,lv.term),e); // use Equal because it is polymorphic
+      }
+    }
+#endif
+    return e;
+  }
+
   /** Make an axiom node. The conclusion must be an instance of an axiom. */
-  virtual node make_axiom(const std::vector<ast> &conclusion){
+  virtual node make_axiom(const std::vector<ast> &conclusion, prover::range frng){
-    prover::range frng = pv->range_full();
     int nargs = conclusion.size();
     std::vector<ast> largs(nargs);
     std::vector<ast> eqs;
@@ -1546,7 +1952,11 @@ class iz3proof_itp_impl : public iz3proof_itp {
     
     for(unsigned i = 0; i < eqs.size(); i++)
       itp = make_mp(eqs[i],itp,pfs[i]);
-    return itp;
+    return capture_localization(itp);
+  }
+
+  virtual node make_axiom(const std::vector<ast> &conclusion){
+    return make_axiom(conclusion,pv->range_full());
   }
 
   /** Make a Contra node. This rule takes a derivation of the form
@@ -1939,6 +2349,8 @@ class iz3proof_itp_impl : public iz3proof_itp {
   */
 
   ast make_refl(const ast &e){
+    if(get_term_type(e) == LitA)
+      return mk_false();
     return mk_true(); // TODO: is this right?
   }
 
@@ -1972,7 +2384,8 @@ class iz3proof_itp_impl : public iz3proof_itp {
       int nargs = num_args(e);
       if(nargs > 0 /*  && (!is_local(e) || flo <= hi || fhi >= lo) */){
 	prover::range frng = rng;
-	if(op(e) == Uninterpreted){
+	opr o = op(e);
+	if(o == Uninterpreted){
 	  symb f = sym(e);
 	  prover::range srng = pv->sym_range(f);
 	  if(pv->ranges_intersect(srng,rng)) // localize to desired range if possible
@@ -1980,6 +2393,9 @@ class iz3proof_itp_impl : public iz3proof_itp {
 	  else
 	    frng = srng; // this term will be localized
 	}
+	else if(o == Plus || o == Times){ // don't want bound variables inside arith ops
+	  frng = erng; // this term will be localized
+	}
 	std::vector<ast> largs(nargs);
 	std::vector<ast> eqs;
 	std::vector<ast> pfs;
@@ -2006,6 +2422,9 @@ class iz3proof_itp_impl : public iz3proof_itp {
     if(pv->ranges_intersect(pv->ast_scope(e),rng))
       return e; // this term occurs in range, so it's O.K.
 
+    if(is_array_type(get_type(e)))
+      throw "help!";
+
     // choose a frame for the constraint that is close to range
     int frame = pv->range_near(pv->ast_scope(e),rng);
 
@@ -2018,12 +2437,89 @@ class iz3proof_itp_impl : public iz3proof_itp {
     return new_var;
   }
 
+  ast delete_quant(hash_map<ast,ast> &memo, const ast &v, const ast &e){
+    std::pair<ast,ast> foo(e,ast());
+    std::pair<hash_map<ast,ast>::iterator,bool> bar = memo.insert(foo);
+    ast &res = bar.first->second;
+    if(bar.second){
+      opr o = op(e);
+      switch(o){
+      case Or:
+      case And:
+      case Implies: {
+	unsigned nargs = num_args(e);
+	std::vector<ast> args; args.resize(nargs);
+	for(unsigned i = 0; i < nargs; i++)
+	  args[i] = delete_quant(memo, v, arg(e,i));
+	res = make(o,args);
+	break;
+      }
+      case Uninterpreted: {
+	symb s = sym(e);
+	ast w = arg(arg(e,0),0);
+	if(s == sforall || s == sexists){
+	  res = delete_quant(memo,v,arg(e,1));
+	  if(w != v)
+	    res = make(s,w,res);
+	  break;
+	}
+      }
+      default:
+	res = e;
+      }
+    }
+    return res;
+  }
+
+  ast insert_quants(hash_map<ast,ast> &memo, const ast &e){
+    std::pair<ast,ast> foo(e,ast());
+    std::pair<hash_map<ast,ast>::iterator,bool> bar = memo.insert(foo);
+    ast &res = bar.first->second;
+    if(bar.second){
+      opr o = op(e);
+      switch(o){
+      case Or:
+      case And:
+      case Implies: {
+	unsigned nargs = num_args(e);
+	std::vector<ast> args; args.resize(nargs);
+	for(unsigned i = 0; i < nargs; i++)
+	  args[i] = insert_quants(memo, arg(e,i));
+	res = make(o,args);
+	break;
+      }
+      case Uninterpreted: {
+	symb s = sym(e);
+	if(s == sforall || s == sexists){
+	  opr q = (s == sforall) ? Forall : Exists;
+	  ast v = arg(arg(e,0),0);
+	  hash_map<ast,ast> dmemo;
+	  ast body = delete_quant(dmemo,v,arg(e,1));
+	  body = insert_quants(memo,body);
+	  res = apply_quant(q,v,body);
+	  break;
+	}
+      }
+      default:
+	res = e;
+      }
+    }
+    return res;
+  }
+
   ast add_quants(ast e){
+#ifdef CAPTURE_LOCALIZATION
+    if(!localization_vars.empty()){
+      hash_map<ast,ast> memo;
+      e = insert_quants(memo,e);
+    }
+#else
     for(int i = localization_vars.size() - 1; i >= 0; i--){
       LocVar &lv = localization_vars[i];
       opr quantifier = (pv->in_range(lv.frame,rng)) ? Exists : Forall; 
       e = apply_quant(quantifier,lv.var,e);
     }
+#endif
     return e;
   }
 
@@ -2035,7 +2531,11 @@ class iz3proof_itp_impl : public iz3proof_itp {
   /* Return an interpolant from a proof of false */
   ast interpolate(const node &pf){
     // proof of false must be a formula, with quantified symbols
+#ifndef BOGUS_QUANTS
     return add_quants(z3_simplify(pf));
+#else
+    return z3_simplify(pf);
+#endif
   }
 
   ast resolve_with_quantifier(const ast &pivot1, const ast &conj1,
@@ -2055,7 +2555,7 @@ class iz3proof_itp_impl : public iz3proof_itp {
     ast npP = make_mp(make(Iff,nPloc,nP),npPloc,neqpf);
     ast nrP = make_resolution(nP,conj2,npP);
     ast res = make_resolution(Ploc,rP,nrP);
-    return res;
+    return capture_localization(res);
   }
 
   ast get_contra_coeff(const ast &f){
@@ -2141,6 +2641,16 @@ public:
     m().inc_ref(rewrite_A);
     rewrite_B = function("@rewrite_B",3,boolboolbooldom,bool_type());
     m().inc_ref(rewrite_B);
+    normal_step = function("@normal_step",2,boolbooldom,bool_type());
+    m().inc_ref(normal_step);
+    normal_chain = function("@normal_chain",2,boolbooldom,bool_type());
+    m().inc_ref(normal_chain);
+    normal = function("@normal",2,boolbooldom,bool_type());
+    m().inc_ref(normal);
+    sforall = function("@sforall",2,boolbooldom,bool_type());
+    m().inc_ref(sforall);
+    sexists = function("@sexists",2,boolbooldom,bool_type());
+    m().inc_ref(sexists);
   }
 
   ~iz3proof_itp_impl(){

src/interp/iz3proof_itp.h

@@ -70,6 +70,9 @@ class iz3proof_itp : public iz3mgr {
   /** Make an axiom node. The conclusion must be an instance of an axiom. */
   virtual node make_axiom(const std::vector<ast> &conclusion) = 0;
 
+  /** Make an axiom node. The conclusion must be an instance of an axiom. Localize axiom instance to range*/
+  virtual node make_axiom(const std::vector<ast> &conclusion, prover::range) = 0;
+
   /** Make a Contra node. This rule takes a derivation of the form
      Gamma |- False and produces |- \/~Gamma. */
 

src/interp/iz3translate.cpp

@@ -109,36 +109,49 @@ public:
      symbols and assign each to a frame. THe assignment is heuristic.
   */
 
-  void scan_skolems_rec(hash_set<ast> &memo, const ast &proof){
+  int scan_skolems_rec(hash_map<ast,int> &memo, const ast &proof, int frame){
-    std::pair<hash_set<ast>::iterator,bool> bar = memo.insert(proof);
+    std::pair<ast,int> foo(proof,INT_MAX);
-    if(!bar.second)
+    std::pair<AstToInt::iterator, bool> bar = memo.insert(foo);
-      return;
+    int &res = bar.first->second;
+    if(!bar.second) return res;
     pfrule dk = pr(proof);
-    if(dk == PR_SKOLEMIZE){
+    if(dk == PR_ASSERTED){
+      ast ass = conc(proof);
+      res = frame_of_assertion(ass);
+    }
+    else if(dk == PR_SKOLEMIZE){
       ast quanted = arg(conc(proof),0);
       if(op(quanted) == Not)
 	quanted = arg(quanted,0);
-      range r = ast_range(quanted);
+      // range r = ast_range(quanted);
-      if(range_is_empty(r))
+      // if(range_is_empty(r))
-	r = ast_scope(quanted);
+      range r = ast_scope(quanted);
       if(range_is_empty(r))
 	throw "can't skolemize";
-      int frame = range_max(r);
+      if(frame == INT_MAX || !in_range(frame,r))
+	frame = range_max(r); // this is desperation -- may fail
       if(frame >= frames) frame = frames - 1;
       add_frame_range(frame,arg(conc(proof),1));
       r = ast_scope(arg(conc(proof),1));
     }
+    else if(dk==PR_MODUS_PONENS_OEQ){
+      frame = scan_skolems_rec(memo,prem(proof,0),frame);
+      scan_skolems_rec(memo,prem(proof,1),frame);
+    }
     else {
       unsigned nprems = num_prems(proof);
       for(unsigned i = 0; i < nprems; i++){
-	scan_skolems_rec(memo,prem(proof,i));
+	int bar = scan_skolems_rec(memo,prem(proof,i),frame);
+	if(res == INT_MAX || res == bar) res = bar;
+	else if(bar != INT_MAX) res = -1;
       }
     }
+    return res;
   }
 
   void scan_skolems(const ast &proof){
-    hash_set<ast> memo;
+    hash_map<ast,int> memo;
-    scan_skolems_rec(memo,proof);
+    scan_skolems_rec(memo,proof, INT_MAX);
   }
 
   // determine locality of a proof term
@@ -1364,6 +1377,18 @@ public:
     return eq2;
   }
 
+  bool get_store_array(const ast &t, ast &res){
+    if(op(t) == Store){
+      res = t;
+      return true;
+    }
+    int nargs = num_args(t);
+    for(int i = 0; i < nargs; i++)
+      if(get_store_array(arg(t,i),res))
+	return true;
+    return false;
+  }
+
   // translate a Z3 proof term into interpolating proof system
 
   Iproof::node translate_main(ast proof, bool expect_clause = true){
@@ -1448,6 +1473,21 @@ public:
 	}
       }
 
+      /* this is the symmetry rule for ~=, that is, takes x ~= y and yields y ~= x.
+      the proof idiom uses commutativity, monotonicity and mp, but we replace it here
+      with symmtrey and resolution, that is, we prove y = x |- x = y, then resolve
+      with the proof of ~(x=y) to get ~y=x. */
+      if(dk == PR_MODUS_PONENS && pr(prem(proof,1)) == PR_MONOTONICITY && pr(prem(prem(proof,1),0)) == PR_COMMUTATIVITY && num_prems(prem(proof,1)) == 1){
+	Iproof::node ante = translate_main(prem(proof,0),false);
+	ast eq0 = arg(conc(prem(prem(proof,1),0)),0);
+	ast eq1 = arg(conc(prem(prem(proof,1),0)),1);
+	Iproof::node eq1hy = iproof->make_hypothesis(eq1);
+	Iproof::node eq0pf = iproof->make_symmetry(eq0,eq1,eq1hy);
+	std::vector<ast> clause; // just a dummy
+	res = iproof->make_resolution(eq0,clause,ante,eq0pf);
+	return res;
+      }
+
       // translate all the premises
       std::vector<Iproof::node> args(nprems);
       for(unsigned i = 0; i < nprems; i++)
@@ -1578,9 +1618,13 @@ public:
 	    throw unsupported();
 	  }
 	  break;
-	case ArrayTheory: // nothing fancy for this
+	case ArrayTheory: {// nothing fancy for this
-	  res = iproof->make_axiom(lits);
+	  ast store_array;
+	  if(!get_store_array(con,store_array))
+	    throw unsupported();
+	  res = iproof->make_axiom(lits,ast_scope(store_array));
 	  break;
+	}
 	default:
 	  throw unsupported();
 	}

src/interp/iz3translate_direct.cpp

@@ -38,6 +38,24 @@ Revision History:
 using namespace stl_ext;
 #endif
 
+#ifndef WIN32
+
+/* This can introduce an address dependency if the range type of hash_map has
+   a destructor. Since the code in this file is not used and only here for
+   historical comparisons, we allow this non-determinism.
+ */
+namespace stl_ext {
+  template <class T>
+    class hash<T *> {
+  public:
+    size_t operator()(const T *p) const {
+      return (size_t) p;
+    }
+  };
+}
+
+#endif
+
 
 static int lemma_count = 0;
 static int nll_lemma_count = 0;

src/muz/duality/duality_dl_interface.cpp

@@ -472,7 +472,7 @@ static proof_ref extract_proof(dl_interface *d, Solver::Counterexample &cex) {
   expr conc = f(args);
   
 
-  ::vector<proof *> pprems;
+  ::vector< ::proof *> pprems;
   for(unsigned i = 0; i < prems.size(); i++)
     pprems.push_back(prems[i].get());
   

src/smt/params/qi_params.cpp

@@ -27,6 +27,7 @@ void qi_params::updt_params(params_ref const & _p) {
     m_mbqi_max_iterations = p.mbqi_max_iterations();
     m_mbqi_trace = p.mbqi_trace();
     m_mbqi_force_template = p.mbqi_force_template();
+    m_mbqi_id = p.mbqi_id();
     m_qi_profile = p.qi_profile();
     m_qi_profile_freq = p.qi_profile_freq();
     m_qi_max_instances = p.qi_max_instances();

src/smt/params/qi_params.h

@@ -51,6 +51,7 @@ struct qi_params {
     unsigned           m_mbqi_max_iterations;
     bool               m_mbqi_trace;
     unsigned           m_mbqi_force_template;
+    const char *       m_mbqi_id;
 
     qi_params(params_ref const & p = params_ref()):
         /*
@@ -97,7 +98,9 @@ struct qi_params {
         m_mbqi_max_cexs_incr(1),
         m_mbqi_max_iterations(1000),
         m_mbqi_trace(false),
-        m_mbqi_force_template(10) {
+	m_mbqi_force_template(10),
+        m_mbqi_id(0)  
+    {
         updt_params(p);
     }
 

src/smt/params/smt_params_helper.pyg

@@ -21,6 +21,7 @@ def_module_params(module_name='smt',
                           ('mbqi.max_iterations', UINT, 1000, 'maximum number of rounds of MBQI'),
                           ('mbqi.trace', BOOL, False, 'generate tracing messages for Model Based Quantifier Instantiation (MBQI). It will display a message before every round of MBQI, and the quantifiers that were not satisfied'),
                           ('mbqi.force_template', UINT, 10, 'some quantifiers can be used as templates for building interpretations for functions. Z3 uses heuristics to decide whether a quantifier will be used as a template or not. Quantifiers with weight >= mbqi.force_template are forced to be used as a template'),
+                          ('mbqi.id', STRING, '', 'Only use model-based instantiation for quantifiers with id\'s beginning with string'),
                           ('qi.profile', BOOL, False, 'profile quantifier instantiation'),
                           ('qi.profile_freq', UINT, UINT_MAX, 'how frequent results are reported by qi.profile'),
                           ('qi.max_instances', UINT, UINT_MAX, 'maximum number of quantifier instantiations'),

src/smt/smt_model_checker.cpp

@@ -322,6 +322,7 @@ namespace smt {
 
         for (; it != end; ++it) {
             quantifier * q = *it;
+	    if(!m_qm->mbqi_enabled(q)) continue;
             if (m_context->is_relevant(q) && m_context->get_assignment(q) == l_true) {
                 if (m_params.m_mbqi_trace && q->get_qid() != symbol::null) {
                     verbose_stream() << "(smt.mbqi :checking " << q->get_qid() << ")\n";

src/smt/smt_quantifier.cpp

@@ -335,6 +335,10 @@ namespace smt {
         return m_imp->m_plugin->model_based();
     }
 
+    bool quantifier_manager::mbqi_enabled(quantifier *q) const {
+        return m_imp->m_plugin->mbqi_enabled(q);
+    }
+
     void quantifier_manager::adjust_model(proto_model * m) {
         m_imp->m_plugin->adjust_model(m);
     }
@@ -434,8 +438,22 @@ namespace smt {
 
         virtual bool model_based() const { return m_fparams->m_mbqi; }
 
+        virtual bool mbqi_enabled(quantifier *q) const { 
+	  if(!m_fparams->m_mbqi_id) return true;
+	  const symbol &s = q->get_qid();
+	  unsigned len = strlen(m_fparams->m_mbqi_id);
+	  if(s == symbol::null || s.is_numerical())
+	    return len == 0;
+	  return strncmp(s.bare_str(),m_fparams->m_mbqi_id,len) == 0;
+	}
+
+      /* Quantifier id's must begin with the prefix specified by
+	 parameter mbqi.id to be instantiated with MBQI.  The default
+	 value is the empty string, so all quantifiers are
+	 instantiated.
+       */
         virtual void add(quantifier * q) {
-            if (m_fparams->m_mbqi) {
+	  if (m_fparams->m_mbqi && mbqi_enabled(q)) {
 	    m_model_finder->register_quantifier(q);
 	  }
         }

src/smt/smt_quantifier.h

@@ -75,6 +75,7 @@ namespace smt {
         };
 
         bool model_based() const;
+	bool mbqi_enabled(quantifier *q) const; // can mbqi instantiate this quantifier?
         void adjust_model(proto_model * m);
         check_model_result check_model(proto_model * m, obj_map<enode, app *> const & root2value);
         
@@ -144,6 +145,11 @@ namespace smt {
          */
         virtual bool model_based() const = 0;
         
+        /**
+           \brief Is "model based" instantiate allowed to instantiate this quantifier?
+         */
+	virtual bool mbqi_enabled(quantifier *q) const {return true;}
+
         /**
            \brief Give a change to the plugin to adjust the interpretation of unintepreted functions.
            It can basically change the "else" of each uninterpreted function.

src/smt/theory_arith_aux.h

@@ -476,10 +476,11 @@ namespace smt {
         typename vector<row_entry>::const_iterator it  = r.begin_entries();
         typename vector<row_entry>::const_iterator end = r.end_entries();
         for (; it != end; ++it) {                                                                 
-            if (!it->is_dead() && !it->m_coeff.is_int())
+            if (!it->is_dead() && !it->m_coeff.is_int()) {
                 TRACE("gomory_cut", display_row(tout, r, true););
                 return false;
             }
+        }
         return true;
     }
 

src/util/id_gen.h

@@ -57,6 +57,11 @@ public:
         m_free_ids.finalize();
     }
     
+    unsigned show_hash(){
+      unsigned h = string_hash((char *)&m_free_ids[0],m_free_ids.size()*sizeof(unsigned),17);
+      return hash_u_u(h,m_next_id);
+    }
+
     /**
        \brief Return N if the range of ids generated by this module is in the set [0..N)
     */