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

src/api/api_interp.cpp

@@ -617,7 +617,7 @@ extern "C" {
         }
 
         for (unsigned j = 0; j < num - 1; j++)
-            if (read_parents[j] == SHRT_MIN){
+            if (read_parents[j] == SHRT_MAX){
             read_error << "formula " << j + 1 << ": unreferenced";
             goto fail;
             }
@@ -717,4 +717,4 @@ Z3_lbool Z3_API Z3_interpolate(__in Z3_context ctx,
                                __in unsigned incremental,
                                __in unsigned num_theory,
                                __in_ecount(num_theory) Z3_ast *theory);
-#endif
+#endif

src/cmd_context/basic_cmds.cpp

@@ -241,7 +241,6 @@ protected:
     symbol      m_produce_models;
     symbol      m_produce_assignments;
     symbol      m_produce_interpolants;
-    symbol      m_check_interpolants;
     symbol      m_regular_output_channel;
     symbol      m_diagnostic_output_channel;
     symbol      m_random_seed;
@@ -256,7 +255,6 @@ protected:
             s == m_print_success || s == m_print_warning || s == m_expand_definitions || 
             s == m_interactive_mode || s == m_produce_proofs || s == m_produce_unsat_cores ||
             s == m_produce_models || s == m_produce_assignments || s == m_produce_interpolants ||
-	    s == m_check_interpolants ||
 	    s == m_regular_output_channel || s == m_diagnostic_output_channel || 
             s == m_random_seed || s == m_verbosity || s == m_global_decls;
     }
@@ -275,7 +273,6 @@ public:
         m_produce_models(":produce-models"),
         m_produce_assignments(":produce-assignments"),
         m_produce_interpolants(":produce-interpolants"),
-        m_check_interpolants(":check-interpolants"),
         m_regular_output_channel(":regular-output-channel"),
         m_diagnostic_output_channel(":diagnostic-output-channel"),
         m_random_seed(":random-seed"),
@@ -347,9 +344,6 @@ class set_option_cmd : public set_get_option_cmd {
             check_not_initialized(ctx, m_produce_interpolants);
             ctx.set_produce_interpolants(to_bool(value));
         }
-        else if (m_option == m_check_interpolants) {
-	    ctx.set_check_interpolants(to_bool(value));
-        }
         else if (m_option == m_produce_unsat_cores) {
             check_not_initialized(ctx, m_produce_unsat_cores);
             ctx.set_produce_unsat_cores(to_bool(value));

src/cmd_context/cmd_context.cpp

@@ -397,10 +397,6 @@ void cmd_context::set_produce_interpolants(bool f) {
     // set_solver_factory(mk_smt_solver_factory());
 }
 
-void cmd_context::set_check_interpolants(bool f) {
-    m_params.m_check_interpolants = f;
-}
-
 bool cmd_context::produce_models() const { 
     return m_params.m_model;
 }
@@ -414,10 +410,6 @@ bool cmd_context::produce_interpolants() const {
     return m_params.m_proof;
 }
 
-bool cmd_context::check_interpolants() const { 
-    return m_params.m_check_interpolants;
-}
-
 bool cmd_context::produce_unsat_cores() const { 
     return m_params.m_unsat_core;
 }

src/cmd_context/cmd_context.h

@@ -279,7 +279,6 @@ public:
     bool produce_models() const;
     bool produce_proofs() const;
     bool produce_interpolants() const;
-    bool check_interpolants() const;
     bool produce_unsat_cores() const;
     bool well_sorted_check_enabled() const;
     bool validate_model_enabled() const;
@@ -287,7 +286,6 @@ public:
     void set_produce_unsat_cores(bool flag);
     void set_produce_proofs(bool flag);
     void set_produce_interpolants(bool flag);
-    void set_check_interpolants(bool flag);
     bool produce_assignments() const { return m_produce_assignments; }
     void set_produce_assignments(bool flag) { m_produce_assignments = flag; }
     void set_status(status st) { m_status = st; }

src/cmd_context/context_params.cpp

@@ -61,9 +61,6 @@ void context_params::set(char const * param, char const * value) {
     else if (p == "proof") {
         set_bool(m_proof, param, value);
     }
-    else if (p == "check_interpolants") {
-        set_bool(m_check_interpolants, param, value);
-    }
     else if (p == "model") {
         set_bool(m_model, param, value);
     }
@@ -105,7 +102,6 @@ void context_params::updt_params(params_ref const & p) {
     m_well_sorted_check = p.get_bool("type_check", p.get_bool("well_sorted_check", true));
     m_auto_config       = p.get_bool("auto_config", true);
     m_proof             = p.get_bool("proof", false);
-    m_check_interpolants = p.get_bool("check_interpolants", false);
     m_model             = p.get_bool("model", true);
     m_model_validate    = p.get_bool("model_validate", false);
     m_trace             = p.get_bool("trace", false);
@@ -120,7 +116,6 @@ void context_params::collect_param_descrs(param_descrs & d) {
     d.insert("well_sorted_check", CPK_BOOL, "type checker", "true");
     d.insert("type_check", CPK_BOOL, "type checker (alias for well_sorted_check)", "true");
     d.insert("auto_config", CPK_BOOL, "use heuristics to automatically select solver and configure it", "true");
-    d.insert("check_interpolants", CPK_BOOL, "check correctness of interpolants", "false");
     d.insert("model_validate", CPK_BOOL, "validate models produced by solvers", "false");
     d.insert("trace", CPK_BOOL, "trace generation for VCC", "false");
     d.insert("trace_file_name", CPK_STRING, "trace out file name (see option 'trace')", "z3.log");

src/cmd_context/context_params.h

@@ -30,7 +30,6 @@ public:
     bool        m_auto_config;
     bool        m_proof;
     bool        m_interpolants;
-    bool        m_check_interpolants;
     bool        m_debug_ref_count;
     bool        m_trace;
     std::string m_trace_file_name;

src/cmd_context/interpolant_cmds.cpp

@@ -65,7 +65,7 @@ static void show_interpolant_and_maybe_check(cmd_context & ctx,
   s.cleanup();
 
   // verify, for the paranoid...
-  if(check || ctx.check_interpolants()){
+  if(check || interp_params(m_params).check()){
     std::ostringstream err;
     ast_manager &_m = ctx.m();
 

src/duality/duality.h

@@ -104,6 +104,8 @@ namespace Duality {
 
       FuncDecl RenumberPred(const FuncDecl &f, int n);
 
+      FuncDecl NumberPred(const FuncDecl &f, int n);
+
     Term ExtractStores(hash_map<ast, Term> &memo, const Term &t, std::vector<expr> &cnstrs, hash_map<ast,expr> &renaming);
 
 
@@ -488,9 +490,10 @@ protected:
 	std::vector<Edge *> Incoming;
 	Term dual;
 	Node *map;
+	unsigned recursion_bound;
 	
       Node(const FuncDecl &_Name, const Transformer &_Annotation, const Transformer &_Bound, const Transformer &_Underapprox, const Term &_dual, RPFP *_owner, int _number)
-	: Name(_Name), Annotation(_Annotation), Bound(_Bound), Underapprox(_Underapprox), dual(_dual) {owner = _owner; number = _number; Outgoing = 0;}
+	: Name(_Name), Annotation(_Annotation), Bound(_Bound), Underapprox(_Underapprox), dual(_dual) {owner = _owner; number = _number; Outgoing = 0; recursion_bound = UINT_MAX;}
       };
       
       /** Create a node in the graph. The input is a term R(v_1...v_n)
@@ -829,7 +832,7 @@ protected:
 #ifdef _WINDOWS
        __declspec(dllexport)
 #endif
-       void FromClauses(const std::vector<Term> &clauses);
+       void FromClauses(const std::vector<Term> &clauses, const std::vector<unsigned> *bounds = 0);
 
        void FromFixpointContext(fixedpoint fp, std::vector<Term> &queries);
 
@@ -902,6 +905,10 @@ protected:
 
       int CumulativeDecisions();
 
+      void GreedyReduceNodes(std::vector<Node *> &nodes);
+
+      check_result CheckWithConstrainedNodes(std::vector<Node *> &posnodes,std::vector<Node *> &negnodes);
+
       solver &slvr(){
 	return *ls->slvr;
       }

src/duality/duality_profiling.cpp

@@ -125,8 +125,18 @@ namespace Duality {
 
   void timer_stop(const char *name){
     if(current->name != name || !current->parent){
+#if 0
       std::cerr << "imbalanced timer_start and timer_stop";
       exit(1);
+#endif
+      // in case we lost a timer stop due to an exception
+      while(current->name != name && current->parent)
+	current = current->parent;
+      if(current->parent){
+	current->time += (current_time() - current->start_time);
+	current = current->parent;
+      }
+      return;
     }
     current->time += (current_time() - current->start_time);
     current = current->parent;

src/duality/duality_rpfp.cpp

@@ -2816,6 +2816,62 @@ namespace Duality {
     }
   }
 
+  void foobar(){
+  }
+
+  void RPFP::GreedyReduceNodes(std::vector<Node *> &nodes){
+    std::vector<expr> lits;
+    for(unsigned i = 0; i < nodes.size(); i++){
+      Term b; std::vector<Term> v;
+      RedVars(nodes[i], b, v);
+      lits.push_back(!b);
+      expr bv = dualModel.eval(b);
+      if(eq(bv,ctx.bool_val(true))){
+	check_result  res = slvr_check(lits.size(),&lits[0]);
+	if(res == unsat)
+	  lits.pop_back();
+	else
+	  foobar();
+      }
+    }
+  }
+
+  check_result RPFP::CheckWithConstrainedNodes(std::vector<Node *> &posnodes,std::vector<Node *> &negnodes){
+    timer_start("Check");
+    std::vector<expr> lits;
+    for(unsigned i = 0; i < posnodes.size(); i++){
+      Term b; std::vector<Term> v;
+      RedVars(posnodes[i], b, v);
+      lits.push_back(b);
+    }
+    for(unsigned i = 0; i < negnodes.size(); i++){
+      Term b; std::vector<Term> v;
+      RedVars(negnodes[i], b, v);
+      lits.push_back(!b);
+    }
+    check_result res = slvr_check(lits.size(),&lits[0]);
+    if(res == unsat && posnodes.size()){
+      lits.resize(posnodes.size());
+      res = slvr_check(lits.size(),&lits[0]);
+    }
+    dualModel = slvr().get_model();
+#if 0
+    if(!dualModel.null()){
+      std::cout << "posnodes called:\n";
+      for(unsigned i = 0; i < posnodes.size(); i++)
+	if(!Empty(posnodes[i]))
+	  std::cout << posnodes[i]->Name.name() << "\n";
+      std::cout << "negnodes called:\n";
+      for(unsigned i = 0; i < negnodes.size(); i++)
+	if(!Empty(negnodes[i]))
+	  std::cout << negnodes[i]->Name.name() << "\n";
+    }
+#endif
+    timer_stop("Check");
+    return res;
+  }
+
+
   void RPFP_caching::FilterCore(std::vector<expr> &core, std::vector<expr> &full_core){
     hash_set<ast> core_set;
     std::copy(full_core.begin(),full_core.end(),std::inserter(core_set,core_set.begin()));
@@ -3333,6 +3389,17 @@ namespace Duality {
 	  return ctx.function(name.c_str(), arity, &domain[0], f.range());
         }
 
+  Z3User::FuncDecl Z3User::NumberPred(const FuncDecl &f, int n)
+        {
+	  std::string name = f.name().str();
+	  name = name + "_" + string_of_int(n);
+	  int arity = f.arity();
+	  std::vector<sort> domain;
+	  for(int i = 0; i < arity; i++)
+	    domain.push_back(f.domain(i));
+	  return ctx.function(name.c_str(), arity, &domain[0], f.range());
+        }
+
   // Scan the clause body for occurrences of the predicate unknowns
 
   RPFP::Term RPFP::ScanBody(hash_map<ast,Term> &memo, 
@@ -3570,7 +3637,7 @@ namespace Duality {
 
 #define USE_QE_LITE
 
-  void RPFP::FromClauses(const std::vector<Term> &unskolemized_clauses){
+  void RPFP::FromClauses(const std::vector<Term> &unskolemized_clauses, const std::vector<unsigned> *bounds){
     hash_map<func_decl,Node *> pmap;
     func_decl fail_pred = ctx.fresh_func_decl("@Fail", ctx.bool_sort());
     
@@ -3663,6 +3730,7 @@ namespace Duality {
 	pmap[R] = node;
         if (is_query)
           node->Bound = CreateRelation(std::vector<Term>(), ctx.bool_val(false));
+	node->recursion_bound = bounds ? 0 : UINT_MAX;
       }
     }
 
@@ -3728,6 +3796,8 @@ namespace Duality {
       Transformer T = CreateTransformer(Relparams,Indparams,body);
       Edge *edge = CreateEdge(Parent,T,Children);
       edge->labeled = labeled;; // remember for label extraction
+      if(bounds)
+	Parent->recursion_bound = std::max(Parent->recursion_bound,(*bounds)[i]);
       // edges.push_back(edge);
     }
 

src/duality/duality_solver.cpp

@@ -33,6 +33,7 @@ Revision History:
 #include <map>
 #include <list>
 #include <iterator>
+#include <sstream>
 
 // TODO: make these official options or get rid of them
 
@@ -254,6 +255,13 @@ namespace Duality {
       
       /** Called when done expanding a tree */
       virtual void Done() {}
+
+      /** Ask whether a node should be used/unused in the tree. Returns,
+	  1 if yes, -1 if no, and 0 if don't care. */
+
+      virtual int UseNode(Node *node){
+	return 0;
+      }
     };
     
     /** The Proposer class proposes conjectures eagerly. These can come
@@ -301,10 +309,11 @@ namespace Duality {
     hash_set<Node *> overapproxes;
     std::vector<Proposer *> proposers;
     std::string ConjectureFile;
+    bool stratified_inlining_done;
 
 #ifdef BOUNDED
     struct Counter {
-      int val;
+      unsigned val;
       Counter(){val = 0;}
     };
     typedef std::map<Node *,Counter> NodeToCounter;
@@ -313,6 +322,13 @@ namespace Duality {
     
     /** Solve the problem. */
     virtual bool Solve(){
+      PreSolve();
+      bool res = SolveMain();  // does the actual work
+      PostSolve();
+      return res;
+    }
+
+    void PreSolve(){
       reporter = Report ? CreateStdoutReporter(rpfp) : new Reporter(rpfp);
       conj_reporter = ConjectureFile.empty() ? 0 : CreateConjectureFileReporter(rpfp,ConjectureFile); 
 #ifndef LOCALIZE_CONJECTURES
@@ -321,6 +337,10 @@ namespace Duality {
       heuristic = !cex.get_tree() ? (Heuristic *)(new LocalHeuristic(rpfp))
 	: (Heuristic *)(new ReplayHeuristic(rpfp,cex));
 #endif
+      // determine if we are recursion bounded
+      for(unsigned i = 0; i < rpfp->nodes.size(); i++)
+	if(rpfp->nodes[i]->recursion_bound < UINT_MAX)
+	  RecursionBound = 0;
       cex.clear(); // in case we didn't use it for heuristic
       if(unwinding) delete unwinding;
       unwinding = new RPFP(rpfp->ls);
@@ -337,9 +357,10 @@ namespace Duality {
 	  return false;
 #endif
       StratifiedLeafCount = -1;
-      timer_start("SolveMain");
+      stratified_inlining_done = false;
-      bool res = SolveMain();  // does the actual work
+    }
-      timer_stop("SolveMain");
+
+    void PostSolve(){
       //  print_profile(std::cout);
       delete indset;
       delete heuristic;
@@ -349,7 +370,16 @@ namespace Duality {
 	delete conj_reporter;
       for(unsigned i = 0; i < proposers.size(); i++)
 	delete proposers[i];
-      return res;
+    }
+
+    bool RecheckBounds(){
+      for(unsigned i = 0; i < unwinding->nodes.size(); i++){
+	Node *node = unwinding->nodes[i];
+	node->Bound = node->map->Bound;
+	if(!SatisfyUpperBound(node))
+	  return false;
+      }
+      return true;
     }
 
     void CreateInitialUnwinding(){
@@ -412,6 +442,7 @@ namespace Duality {
     bool StratifiedInlining; // Do stratified inlining as preprocessing step
     int RecursionBound;  // Recursion bound for bounded verification
     bool BatchExpand;
+    bool EnableRestarts; 
     
     bool SetBoolOption(bool &opt, const std::string &value){
       if(value == "0") {
@@ -459,9 +490,12 @@ namespace Duality {
       if(option == "conjecture_file"){
 	ConjectureFile = value;
       }
+      if(option == "enable_restarts"){
+        return SetBoolOption(EnableRestarts,value);
+      }
       return false;
     }
-    
+
     /** Create an instance of a node in the unwinding. Set its
 	annotation to true, and mark it unexpanded. */
     Node* CreateNodeInstance(Node *node, int number = 0){
@@ -768,6 +802,15 @@ namespace Duality {
       annot.Simplify();
     }    
 
+    bool NodeSolutionFromIndSetFull(Node *node){
+      std::vector<Node *> &insts = insts_of_node[node];
+      for(unsigned j = 0; j < insts.size(); j++)
+	if(indset->Contains(insts[j]))
+	  if(insts[j]->Annotation.IsFull())
+	    return true;
+      return false;
+    }
+
     bool recursionBounded;
 
     /** See if the solution might be bounded. */
@@ -780,10 +823,8 @@ namespace Duality {
 	std::vector<Node *> &insts = insts_of_node[node];
 	for(unsigned j = 0; j < insts.size(); j++)
 	  if(indset->Contains(insts[j]))
-	    if(NodePastRecursionBound(insts[j])){
+	    if(NodePastRecursionBound(insts[j],true))
 	      recursionBounded = true;
-	      return;
-	    }
       }
     }    
 
@@ -801,12 +842,18 @@ namespace Duality {
     }
 
 #ifdef BOUNDED
-    bool NodePastRecursionBound(Node *node){
+    bool NodePastRecursionBound(Node *node, bool report = false){
       if(RecursionBound < 0) return false;
       NodeToCounter &backs = back_edges[node];
       for(NodeToCounter::iterator it = backs.begin(), en = backs.end(); it != en; ++it){
-	if(it->second.val > RecursionBound)
+	if(it->second.val > it->first->recursion_bound){
+	  if(report){
+	    std::ostringstream os;
+	    os << "cut off " << it->first->Name.name() << " at depth " << it->second.val;
+	    reporter->Message(os.str());
+	  }
 	  return true;
+	}
       }
       return false;
     }
@@ -892,6 +939,9 @@ namespace Duality {
     */
 
     bool DoStratifiedInlining(){
+      if(stratified_inlining_done)
+	return true;
+      stratified_inlining_done = true;
       DoTopoSort();
       int depth = 1; // TODO: make this an option
       std::vector<hash_map<Node *,Node *> > unfolding_levels(depth+1);
@@ -1034,10 +1084,17 @@ namespace Duality {
 	h->SetOldNode(node);
     }
 
+    bool SolveMain(){
+      timer_start("SolveMain");
+      bool res = SolveMainInt();  // does the actual work
+      timer_stop("SolveMain");
+      return res;
+    }
+
     /** This does the actual solving work. We try to generate
 	candidates for extension. If we succed, we extend the
 	unwinding. If we fail, we have a solution. */
-    bool SolveMain(){
+    bool SolveMainInt(){
       if(StratifiedInlining && !DoStratifiedInlining())
 	return false;
 #ifdef BOUNDED
@@ -1405,16 +1462,18 @@ namespace Duality {
 	slvr.pop(1);
 	delete checker;
 #else
-	RPFP_caching::scoped_solver_for_edge ssfe(gen_cands_rpfp,edge,true /* models */, true /*axioms*/);
+	if(!NodeSolutionFromIndSetFull(edge->Parent)){
-	gen_cands_rpfp->Push();
+	  RPFP_caching::scoped_solver_for_edge ssfe(gen_cands_rpfp,edge,true /* models */, true /*axioms*/);
-	Node *root = CheckerForEdgeClone(edge,gen_cands_rpfp);
+	  gen_cands_rpfp->Push();
-	if(gen_cands_rpfp->Check(root) != unsat){
+	  Node *root = CheckerForEdgeClone(edge,gen_cands_rpfp);
-	  Candidate candidate;
+	  if(gen_cands_rpfp->Check(root) != unsat){
-	  ExtractCandidateFromCex(edge,gen_cands_rpfp,root,candidate);
+	    Candidate candidate;
-	  reporter->InductionFailure(edge,candidate.Children);
+	    ExtractCandidateFromCex(edge,gen_cands_rpfp,root,candidate);
-	  candidates.push_back(candidate);
+	    reporter->InductionFailure(edge,candidate.Children);
+	    candidates.push_back(candidate);
+	  }
+	  gen_cands_rpfp->Pop(1);
 	}
-	gen_cands_rpfp->Pop(1);
 #endif
       }
       updated_nodes.clear();
@@ -1767,6 +1826,7 @@ namespace Duality {
       }
       timer_stop("Propagate");
     }
+    
 
     /** This class represents a derivation tree. */
     class DerivationTree {
@@ -2118,6 +2178,8 @@ namespace Duality {
 
       hash_map<Node *, expr> updates;
 
+      int restart_interval;
+
       DerivationTreeSlow(Duality *_duality, RPFP *rpfp, Reporter *_reporter, Heuristic *_heuristic, bool _full_expand) 
 	: DerivationTree(_duality, rpfp, _reporter, _heuristic, _full_expand) {
 	stack.push_back(stack_entry());
@@ -2126,6 +2188,7 @@ namespace Duality {
       struct DoRestart {};
 
       virtual bool Build(){
+	restart_interval = 3;
 	while (true) {
 	  try {
 	    return BuildMain();
@@ -2136,15 +2199,47 @@ namespace Duality {
 	    while(stack.size() > 1)
 	      PopLevel();
 	    reporter->Message("restarted");
+	    restart_interval += 1;
 	  }
 	}
       }
 
+
+      // When we check, try to use the same children that were used in the
+      // previous counterexample.
+      check_result Check(){
+#if 0
+	std::vector<Node *> posnodes, negnodes;
+	std::vector<Node *> &expansions = stack.back().expansions;
+	for(unsigned i = 0; i < expansions.size(); i++){
+	  Node *node = expansions[i];
+	  std::vector<Node*> &chs = node->Outgoing->Children;
+	  for(unsigned j = 0; j < chs.size(); j++){
+	    Node *ch = chs[j];
+	    int use = heuristic->UseNode(ch); 
+	    if(use == 1)
+	      posnodes.push_back(ch);
+	    else if (use == -1)
+	      negnodes.push_back(ch);
+	  }
+	}
+	if(!(posnodes.empty() && negnodes.empty())){
+	  check_result res = tree->CheckWithConstrainedNodes(posnodes,negnodes);
+	  if(res != unsat){
+	    reporter->Message("matched previous counterexample");
+	    return res;
+	  }
+	}
+#endif
+	return tree->Check(top);
+      }
+
       bool BuildMain(){
 
 	stack.back().level = tree->slvr().get_scope_level();
 	bool was_sat = true;
 	int update_failures = 0;
+	int total_updates = 0;
 
 	while (true)
 	{
@@ -2156,7 +2251,7 @@ namespace Duality {
 	  reporter->Depth(stack.size());
 
 	  //	  res = tree->Solve(top, 1);            // incremental solve, keep interpolants for one pop
-	  check_result foo = tree->Check(top);
+	  check_result foo = Check();
 	  res = foo == unsat ? l_false : l_true;
 
 	  if (res == l_false) {
@@ -2168,32 +2263,50 @@ namespace Duality {
 	      int update_count = 0;
 	      for(unsigned i = 0; i < expansions.size(); i++){
 		Node *node = expansions[i];
-		tree->SolveSingleNode(top,node);
-#ifdef NO_GENERALIZE
-		node->Annotation.Formula = tree->RemoveRedundancy(node->Annotation.Formula).simplify();
-#else
 		try {
+		  tree->SolveSingleNode(top,node);
+#ifdef NO_GENERALIZE
+		  node->Annotation.Formula = tree->RemoveRedundancy(node->Annotation.Formula).simplify();
+#else
 		  if(expansions.size() == 1 && NodeTooComplicated(node))
 		    SimplifyNode(node);
 		  else
 		    node->Annotation.Formula = tree->RemoveRedundancy(node->Annotation.Formula).simplify();
 		  Generalize(node);
+#endif
 		}
 		catch(const RPFP::Bad &){
 		  // bad interpolants can get us here
 		  throw DoRestart();
 		}
-#endif
+		catch(char const *msg){
-		if(RecordUpdate(node))
+		  // bad interpolants can get us here
+		  reporter->Message(std::string("interpolation failure:") + msg);
+		  throw DoRestart();
+		}
+		if(RecordUpdate(node)){
 		  update_count++;
+		  total_updates++;
+		}
 		else
 		  heuristic->Update(node->map); // make it less likely to expand this node in future
 	      }
+#if 1
+	      if(duality->EnableRestarts)
+		if(total_updates >= restart_interval)
+		  throw DoRestart();
+#endif
 	      if(update_count == 0){
 		if(was_sat){
 		  update_failures++;
-		  if(update_failures > 10)
+		  if(update_failures > 10){
-		    throw Incompleteness();
+		    for(unsigned i = 0; i < expansions.size(); i++){
+		      Node *node = expansions[i];
+		      node->map->Annotation.SetFull();
+		      reporter->Message("incompleteness: cleared annotation");
+		    }
+		    throw DoRestart();
+		  }
 		}
 		reporter->Message("backtracked without learning");
 	      }
@@ -2234,6 +2347,10 @@ namespace Duality {
 	    tree->Push();
 	    std::vector<Node *> &expansions = stack.back().expansions;
 #ifndef NO_DECISIONS
+#if 0
+	    if(expansions.size() > 0)
+	      tree->GreedyReduceNodes(expansions[0]->Outgoing->Children); // try to reduce number of children
+#endif
 	    for(unsigned i = 0; i < expansions.size(); i++){
 	      tree->FixCurrentState(expansions[i]->Outgoing);
 	    }
@@ -2253,15 +2370,42 @@ namespace Duality {
 	    if(ExpandSomeNodes(false,expand_max))
 	      continue;
 	    tree->Pop(1);
+	    node_order.clear();
 	    while(stack.size() > 1){
 	      tree->Pop(1);	
+	      std::vector<Node *> &expansions = stack.back().expansions;
+	      for(unsigned i = 0; i < expansions.size(); i++)
+		node_order.push_back(expansions[i]);
 	      stack.pop_back();
 	    }
+#if 0
+	    Reduce();
+#endif
 	    return true;
 	  }
 	}
       }
       
+      std::vector<Node *> node_order;
+
+      void Reduce(){
+	tree->Push();
+	// tree->AssertNode(top); // assert the negation of the top-level spec
+	for(int i = node_order.size()-1; i >= 0; --i){
+	  Edge *edge = node_order[i]->Outgoing;
+	  if(edge){
+	    for(unsigned j = 0; j < edge->Children.size(); j++){
+	      Node *ch = edge->Children[j];
+	      if(!ch->Outgoing)
+		ch->Annotation.SetEmpty();
+	    }
+	    tree->AssertEdge(edge,0,true);
+	  }
+	}
+	tree->GreedyReduceNodes(node_order); // try to reduce the counterexample size
+	tree->Pop(1);
+      }
+
       void PopLevel(){
 	std::vector<Node *> &expansions = stack.back().expansions;
 	tree->Pop(1);	
@@ -2860,17 +3004,7 @@ namespace Duality {
 	return name;
       }
 
-      virtual void ChooseExpand(const std::set<RPFP::Node *> &choices, std::set<RPFP::Node *> &best, bool high_priority, bool best_only){
+      Node *MatchNode(Node *node){
-	if(!high_priority || !old_cex.get_tree()){
-	  Heuristic::ChooseExpand(choices,best,false);
-	  return;
-	}
-	// first, try to match the derivatino tree nodes to the old cex
-	std::set<Node *> matched, unmatched;
-	for(std::set<Node *>::iterator it = choices.begin(), en = choices.end(); it != en; ++it){
-	  Node *node = (*it);
-	  if(cex_map.empty())
-	    cex_map[node] = old_cex.get_root();  // match the root nodes
 	  if(cex_map.find(node) == cex_map.end()){ // try to match an unmatched node
 	    Node *parent = node->Incoming[0]->Parent; // assumes we are a tree!
 	    if(cex_map.find(parent) == cex_map.end())
@@ -2893,7 +3027,30 @@ namespace Duality {
 	      cex_map[chs[i]] = 0;
 	  }
 	matching_done:
-	  Node *old_node = cex_map[node];
+	  return cex_map[node];
+      }
+
+      int UseNode(Node *node){
+	if (!old_cex.get_tree())
+	  return 0;
+	Node *old_node = MatchNode(node);
+	if(!old_node)
+	  return 0;
+	return old_cex.get_tree()->Empty(old_node) ? -1 : 1;
+      }
+
+      virtual void ChooseExpand(const std::set<RPFP::Node *> &choices, std::set<RPFP::Node *> &best, bool high_priority, bool best_only){
+	if(cex_map.empty())
+	  cex_map[*(choices.begin())] = old_cex.get_root();  // match the root nodes
+	if(!high_priority || !old_cex.get_tree()){
+	  Heuristic::ChooseExpand(choices,best,false);
+	  return;
+	}
+	// first, try to match the derivatino tree nodes to the old cex
+	std::set<Node *> matched, unmatched;
+	for(std::set<Node *>::iterator it = choices.begin(), en = choices.end(); it != en; ++it){
+	  Node *node = (*it);
+	  Node *old_node = MatchNode(node);
 	  if(!old_node)
 	    unmatched.insert(node);
 	  else if(old_cex.get_tree()->Empty(old_node))
@@ -3168,8 +3325,233 @@ namespace Duality {
     
   };
 
+
+  class DualityDepthBounded : public Solver {
+
+    Duality *duality;
+    context &ctx;                        // Z3 context
+    solver &slvr;                        // Z3 solver
+
+  public:
+    DualityDepthBounded(RPFP *_rpfp) :
+      ctx(_rpfp->ctx),
+      slvr(_rpfp->slvr()){
+      rpfp = _rpfp;
+      DepthBoundRPFP();
+      duality = alloc(Duality,drpfp);
+    }
+
+    ~DualityDepthBounded(){
+      dealloc(duality);
+      delete drpfp;
+    }
+
+    bool Solve(){
+      int depth_bound = 10;
+      bool res;
+      SetMaxDepthRPFP(depth_bound);
+      duality->PreSolve();
+      while(true){
+	res = duality->SolveMain();
+	if(!res || GetSolution())
+	  break;
+	depth_bound++;
+	SetMaxDepthRPFP(depth_bound);
+	res = duality->RecheckBounds();
+	if(!res)
+	  break;
+      }
+      duality->PostSolve();
+      if(!res)
+	ConvertCex();
+      return res;
+    }
+
+    Counterexample &GetCounterexample(){
+      return cex;
+    }
+
+    bool SetOption(const std::string &option, const std::string &value){
+      return duality->SetOption(option,value);
+    }
+
+    virtual void LearnFrom(Solver *old_solver){
+      DualityDepthBounded *old = dynamic_cast<DualityDepthBounded *>(old_solver);
+      if(old){
+	duality->LearnFrom(old->duality);
+      }
+    }
+
+    bool IsResultRecursionBounded(){
+      return duality->IsResultRecursionBounded();
+    }
+
+    void Cancel(){
+      duality->Cancel();
+    }
+
+    typedef RPFP::Node Node;
+    typedef RPFP::Edge Edge;
+    RPFP *rpfp, *drpfp;
+    hash_map<Node *, Node *> db_map, db_rev_map;
+    hash_map<Edge *, Edge *> db_edge_rev_map;
+    std::vector<expr> db_saved_bounds;
+    Counterexample cex;
+
+    expr AddParamToRels(hash_map<ast,expr> &memo, hash_map<func_decl,func_decl> &rmap, const expr &p, const expr &t) {
+      std::pair<ast,expr> foo(t,expr(ctx));
+      std::pair<hash_map<ast,expr>::iterator, bool> bar = memo.insert(foo);
+      expr &res = bar.first->second;
+      if(!bar.second) return res;
+
+      if (t.is_app())
+	{
+	  func_decl f = t.decl();
+	  std::vector<expr> args;
+	  int nargs = t.num_args();
+	  for(int i = 0; i < nargs; i++)
+	    args.push_back(AddParamToRels(memo, rmap, p, t.arg(i)));
+	  hash_map<func_decl,func_decl>::iterator rit = rmap.find(f);
+	  if(rit != rmap.end()){
+	    args.push_back(p);
+	    res = (rit->second)(args);
+	    res = ctx.make(And,res,ctx.make(Geq,p,ctx.int_val(0)));
+	  }
+	  else
+	    res = f(args);
+	}
+      else if (t.is_quantifier())
+      {
+	expr body = AddParamToRels(memo, rmap, p, t.body());
+	res = clone_quantifier(t, body);
+      }
+      else res = t;
+      return res;
+    }
+
+
+    void DepthBoundRPFP(){
+      drpfp = new RPFP(rpfp->ls);
+      expr dvar = ctx.int_const("@depth");
+      expr dmax = ctx.int_const("@depth_max");
+      for(unsigned i = 0; i < rpfp->nodes.size(); i++){
+	Node *node = rpfp->nodes[i];
+	std::vector<sort> arg_sorts;
+	const std::vector<expr> &params = node->Annotation.IndParams;
+	for(unsigned j = 0; j < params.size(); j++)
+	  arg_sorts.push_back(params[j].get_sort());
+	arg_sorts.push_back(ctx.int_sort());
+	std::string new_name = std::string("@db@") + node->Name.name().str();
+	func_decl f = ctx.function(new_name.c_str(),arg_sorts.size(), &arg_sorts[0],ctx.bool_sort());
+	std::vector<expr> args = params;
+	args.push_back(dvar);
+	expr pat = f(args);
+	Node *dnode = drpfp->CreateNode(pat);
+	db_map[node] = dnode;
+	db_rev_map[dnode] = node;
+	expr bound_fmla = node->Bound.Formula;
+	if(!eq(bound_fmla,ctx.bool_val(true))){
+	  bound_fmla = implies(dvar == dmax,bound_fmla);
+	  dnode->Bound.Formula = bound_fmla;
+	}
+	db_saved_bounds.push_back(bound_fmla);
+	//	dnode->Annotation.Formula = ctx.make(And,node->Annotation.Formula,ctx.make(Geq,dvar,ctx.int_val(0)));
+      }
+      for(unsigned i = 0; i < rpfp->edges.size(); i++){
+	Edge *edge = rpfp->edges[i];
+	std::vector<Node *> new_children;
+	std::vector<func_decl> new_relparams;
+	hash_map<func_decl,func_decl> rmap;
+	for(unsigned j = 0; j < edge->Children.size(); j++){
+	  Node *ch = edge->Children[j];
+	  Node *nch = db_map[ch];
+	  func_decl f = nch->Name;
+	  func_decl sf = drpfp->NumberPred(f,j);
+	  new_children.push_back(nch);
+	  new_relparams.push_back(sf);
+	  rmap[edge->F.RelParams[j]] = sf;
+	}
+	std::vector<expr> new_indparams = edge->F.IndParams;
+	new_indparams.push_back(dvar);
+	hash_map<ast,expr> memo;
+	expr new_fmla = AddParamToRels(memo,rmap,ctx.make(Sub,dvar,ctx.int_val(1)),edge->F.Formula);
+	RPFP::Transformer new_t = drpfp->CreateTransformer(new_relparams,new_indparams,new_fmla);
+	Node *new_parent = db_map[edge->Parent];
+	db_edge_rev_map[drpfp->CreateEdge(new_parent,new_t,new_children)] = edge;
+      }
+    }
+
+    void SetMaxDepthRPFP(int depth){
+      hash_map<ast,expr> subst;
+      expr dmax = ctx.int_const("@depth_max");
+      subst[dmax] = ctx.int_val(depth);
+      for(unsigned i = 0; i < drpfp->nodes.size(); i++){
+	Node *node = drpfp->nodes[i];
+	expr fmla = db_saved_bounds[i];
+	fmla = drpfp->SubstRec(subst,fmla);
+	node->Bound.Formula = fmla;
+      }
+    }
+
+    void ConvertCex(){
+      cex.clear();
+      RPFP *tree = new RPFP(rpfp->ls);
+      Node *root;
+      Counterexample &dctx = duality->GetCounterexample();
+      hash_map<Node *, Node *> ctx_node_map;
+      for(unsigned i = 0; i < dctx.get_tree()->nodes.size(); i++){
+	Node *dnode = dctx.get_tree()->nodes[i];
+	Node *onode = db_rev_map[dnode->map->map];
+	Node *node = tree->CloneNode(onode);
+	node->number = dnode->number; // numbers have to match for model to make sense
+	ctx_node_map[dnode] = node;
+	if(dnode == dctx.get_root())
+	  root = node;
+      }
+      for(unsigned i = 0; i < dctx.get_tree()->edges.size(); i++){
+	Edge *dedge = dctx.get_tree()->edges[i];
+	Edge *oedge = db_edge_rev_map[dedge->map];
+	Node *parent = ctx_node_map[dedge->Parent];
+	std::vector<Node *> chs;
+	for(unsigned j = 0; j < dedge->Children.size(); j++)
+	  chs.push_back(ctx_node_map[dedge->Children[j]]);
+	Edge *edge = tree->CreateEdge(parent,oedge->F,chs);
+	edge->number = dedge->number; // numbers have to match for model to make sense
+	edge->map = oedge;
+      }
+      tree->dualModel = dctx.get_tree()->dualModel;
+      cex.set(tree,root);
+    }
+
+    bool GetSolution(){
+      for(unsigned i = 0; i < rpfp->nodes.size(); i++)
+	if(!drpfp->nodes[i]->Annotation.SubsetEq(rpfp->nodes[i]->Bound))
+	  return false;
+      expr dvar = ctx.int_const("@depth");
+      hash_map<ast,expr> subst;
+      subst[dvar] = ctx.int_val(INT_MAX);
+      for(unsigned i = 0; i < rpfp->nodes.size(); i++){
+	expr fmla = drpfp->nodes[i]->Annotation.Formula;
+	fmla = drpfp->SubstRec(subst,fmla);
+	fmla = fmla.simplify();
+	rpfp->nodes[i]->Annotation.Formula = fmla;
+      }
+      return true;
+    }
+
+    void UndoDepthBoundRPFP(){
+#if 0
+      if(cex.get_tree()){
+	// here, need to map the cex back...
+      }
+      // also need to map the proof back, but we don't...
+#endif
+    }
+  };
+
   Solver *Solver::Create(const std::string &solver_class, RPFP *rpfp){
-    Duality *s = alloc(Duality,rpfp);
+    //    Solver *s = alloc(DualityDepthBounded,rpfp);
+    Solver *s = alloc(Duality,rpfp);
     return s;
   }
 

src/interp/iz3params.pyg

@@ -2,4 +2,5 @@ def_module_params('interp',
                   description='interpolation parameters',
                   export=True,
                   params=(('profile', BOOL, False, '(INTERP) profile interpolation'),
+                          ('check', BOOL, False, '(INTERP) check interpolants'),
                           ))

src/muz/base/dl_context.cpp

@@ -246,6 +246,7 @@ namespace datalog {
         m_rule_fmls_head = 0;
         m_rule_fmls.reset();
         m_rule_names.reset();
+        m_rule_bounds.reset();
         m_argument_var_names.reset();
         m_preds.reset();
         m_preds_by_name.reset();
@@ -474,9 +475,10 @@ namespace datalog {
         return new_pred;
     }
 
-    void context::add_rule(expr* rl, symbol const& name) {
+  void context::add_rule(expr* rl, symbol const& name, unsigned bound) {
         m_rule_fmls.push_back(rl);
         m_rule_names.push_back(name);
+	m_rule_bounds.push_back(bound);
     }
 
     void context::flush_add_rules() {
@@ -983,6 +985,9 @@ namespace datalog {
             flush_add_rules();
             break;
         case DUALITY_ENGINE:
+	    // this lets us use duality with SAS 2013 abstraction
+	    if(quantify_arrays())
+	      flush_add_rules();
 	    break;
         default:
             UNREACHABLE();
@@ -1102,12 +1107,13 @@ namespace datalog {
         }
     }
    
-    void context::get_raw_rule_formulas(expr_ref_vector& rules, svector<symbol>& names){
+  void context::get_raw_rule_formulas(expr_ref_vector& rules, svector<symbol>& names, vector<unsigned> &bounds){
         for (unsigned i = 0; i < m_rule_fmls.size(); ++i) {
-            expr_ref r = bind_variables(m_rule_fmls[i].get(), true);
+	    expr_ref r = bind_variables(m_rule_fmls[i].get(), true);
-            rules.push_back(r.get());
+	    rules.push_back(r.get());
-            //            rules.push_back(m_rule_fmls[i].get());
+	    //            rules.push_back(m_rule_fmls[i].get());
-            names.push_back(m_rule_names[i]);
+	    names.push_back(m_rule_names[i]);
+	    bounds.push_back(m_rule_bounds[i]);
         }
     }
 
@@ -1125,6 +1131,7 @@ namespace datalog {
                 m_rule_names[i] = m_rule_names.back();
                 m_rule_fmls.pop_back();
                 m_rule_names.pop_back();
+                m_rule_bounds.pop_back();
                 --i;
             }
         }

src/muz/base/dl_context.h

@@ -194,6 +194,7 @@ namespace datalog {
         unsigned           m_rule_fmls_head;
         expr_ref_vector    m_rule_fmls;
         svector<symbol>    m_rule_names;
+        vector<unsigned>   m_rule_bounds;
         expr_ref_vector    m_background;
         model_converter_ref m_mc;
         proof_converter_ref m_pc;
@@ -366,7 +367,7 @@ namespace datalog {
         rule_set & get_rules() { flush_add_rules(); return m_rule_set; }
 
         void get_rules_as_formulas(expr_ref_vector& fmls, svector<symbol>& names);
-        void get_raw_rule_formulas(expr_ref_vector& fmls, svector<symbol>& names);
+        void get_raw_rule_formulas(expr_ref_vector& fmls, svector<symbol>& names, vector<unsigned> &bounds);
 
         void add_fact(app * head);
         void add_fact(func_decl * pred, const relation_fact & fact);
@@ -383,7 +384,7 @@ namespace datalog {
         /**
            Method exposed from API for adding rules.
         */
-        void add_rule(expr* rl, symbol const& name);
+        void add_rule(expr* rl, symbol const& name, unsigned bound = UINT_MAX);
         
 
         /**

src/muz/base/fixedpoint_params.pyg

@@ -78,6 +78,7 @@ def_module_params('fixedpoint',
 			  ('batch_expand', BOOL, False, 'DUALITY: use batch expansion'),
                           ('dump_aig', SYMBOL, '', 'Dump clauses in AIG text format (AAG) to the given file name'),
 			  ('conjecture_file', STRING, '', 'DUALITY: save conjectures to file'),
+			  ('enable_restarts', BOOL, False, 'DUALITY: enable restarts'),
                           ))
 
 

src/muz/duality/duality_dl_interface.cpp

@@ -37,6 +37,7 @@ Revision History:
 #include "fixedpoint_params.hpp"
 #include "used_vars.h"
 #include "func_decl_dependencies.h"
+#include "dl_transforms.h"
 
 // template class symbol_table<family_id>;
 
@@ -155,8 +156,41 @@ lbool dl_interface::query(::expr * query) {
 
   expr_ref_vector rules(m_ctx.get_manager());
   svector< ::symbol> names;  
+  vector<unsigned> bounds;
   // m_ctx.get_rules_as_formulas(rules, names);
-   m_ctx.get_raw_rule_formulas(rules, names);
+
+
+  // If using SAS 2013 abstractiion, we need to perform some transforms
+  expr_ref query_ref(m_ctx.get_manager());
+  if(m_ctx.quantify_arrays()){
+    datalog::rule_manager& rm = m_ctx.get_rule_manager();
+    rm.mk_query(query, m_ctx.get_rules());
+    apply_default_transformation(m_ctx);
+    datalog::rule_set &rs = m_ctx.get_rules();
+    if(m_ctx.get_rules().get_output_predicates().empty())
+        query_ref = m_ctx.get_manager().mk_false();
+    else {
+        func_decl_ref query_pred(m_ctx.get_manager());
+	query_pred = m_ctx.get_rules().get_output_predicate();
+	ptr_vector<sort> sorts;
+	unsigned nargs = query_pred.get()->get_arity();
+	expr_ref_vector vars(m_ctx.get_manager());
+	for(unsigned i = 0; i < nargs; i++){
+	  ::sort *s = query_pred.get()->get_domain(i);
+	  vars.push_back(m_ctx.get_manager().mk_var(nargs-1-i,s));
+	}
+	query_ref = m_ctx.get_manager().mk_app(query_pred.get(),nargs,vars.c_ptr());
+	query = query_ref.get();
+    }
+    unsigned nrules = rs.get_num_rules();
+    for(unsigned i = 0; i < nrules; i++){
+      expr_ref f(m_ctx.get_manager());
+      rs.get_rule(i)->to_formula(f);
+      rules.push_back(f);
+    }
+  }
+  else 
+    m_ctx.get_raw_rule_formulas(rules, names, bounds);
 
   // get all the rules as clauses
   std::vector<expr> &clauses = _d->clauses;
@@ -200,6 +234,7 @@ lbool dl_interface::query(::expr * query) {
   expr qc = implies(q,_d->ctx.bool_val(false));
   qc = _d->ctx.make_quant(Forall,b_sorts,b_names,qc);
   clauses.push_back(qc);
+  bounds.push_back(UINT_MAX);
   
   // get the background axioms
   unsigned num_asserts = m_ctx.get_num_assertions();
@@ -243,13 +278,21 @@ lbool dl_interface::query(::expr * query) {
 	  expr c = implies(_d->ctx.bool_val(false),f(args));
 	  c = _d->ctx.make_quant(Forall,args,c);
 	  clauses.push_back(c);
+	  bounds.push_back(UINT_MAX);
 	}
       }
     }
   }
+  unsigned rb = m_ctx.get_params().recursion_bound();
+  std::vector<unsigned> std_bounds;
+  for(unsigned i = 0; i < bounds.size(); i++){
+    unsigned b = bounds[i];
+    if (b == UINT_MAX) b = rb;
+    std_bounds.push_back(b);
+  }
 
   // creates 1-1 map between clauses and rpfp edges
-  _d->rpfp->FromClauses(clauses);
+  _d->rpfp->FromClauses(clauses,&std_bounds);
 
   // populate the edge-to-clause map
   for(unsigned i = 0; i < _d->rpfp->edges.size(); ++i)
@@ -271,11 +314,13 @@ lbool dl_interface::query(::expr * query) {
   rs->SetOption("stratified_inlining",m_ctx.get_params().stratified_inlining() ? "1" : "0");
   rs->SetOption("batch_expand",m_ctx.get_params().batch_expand() ? "1" : "0");
   rs->SetOption("conjecture_file",m_ctx.get_params().conjecture_file());
-  unsigned rb = m_ctx.get_params().recursion_bound();
+  rs->SetOption("enable_restarts",m_ctx.get_params().enable_restarts() ? "1" : "0");
+#if 0
   if(rb != UINT_MAX){
     std::ostringstream os; os << rb;
     rs->SetOption("recursion_bound", os.str());
   }
+#endif
 
   // Solve!
   bool ans;

src/muz/fp/dl_cmds.cpp

@@ -100,7 +100,7 @@ struct dl_context {
         dlctx().set_predicate_representation(pred, num_kinds, kinds);        
     }
     
-    void add_rule(expr * rule, symbol const& name) {
+    void add_rule(expr * rule, symbol const& name, unsigned bound) {
         init();
         if (m_collected_cmds) {
             expr_ref rl = m_context->bind_variables(rule, true);
@@ -110,7 +110,7 @@ struct dl_context {
             m_trail.push(push_back_vector<dl_context, svector<symbol> >(m_collected_cmds->m_names));
         }
         else {
-            m_context->add_rule(rule, name);
+	    m_context->add_rule(rule, name, bound);
         }
     }    
 
@@ -151,19 +151,22 @@ class dl_rule_cmd : public cmd {
     mutable unsigned     m_arg_idx;
     expr*        m_t;
     symbol       m_name;
+    unsigned     m_bound;
 public:
     dl_rule_cmd(dl_context * dl_ctx):
         cmd("rule"),
         m_dl_ctx(dl_ctx),       
         m_arg_idx(0),
-        m_t(0) {}
+        m_t(0),
-    virtual char const * get_usage() const { return "(forall (q) (=> (and body) head)) :optional-name"; }
+        m_bound(UINT_MAX) {}
+    virtual char const * get_usage() const { return "(forall (q) (=> (and body) head)) :optional-name :optional-recursion-bound"; }
     virtual char const * get_descr(cmd_context & ctx) const { return "add a Horn rule."; }
     virtual unsigned get_arity() const { return VAR_ARITY; }
     virtual cmd_arg_kind next_arg_kind(cmd_context & ctx) const { 
         switch(m_arg_idx) {
         case 0: return CPK_EXPR;
         case 1: return CPK_SYMBOL;
+        case 2: return CPK_UINT;
         default: return CPK_SYMBOL;
         }
     }
@@ -173,13 +176,18 @@ public:
     }
     virtual void set_next_arg(cmd_context & ctx, symbol const & s) {
         m_name = s;
+        m_arg_idx++;
+    }
+    virtual void set_next_arg(cmd_context & ctx, unsigned bound) {
+        m_bound = bound;
+        m_arg_idx++;
     }
     virtual void reset(cmd_context & ctx) { m_dl_ctx->reset(); prepare(ctx); }
-    virtual void prepare(cmd_context& ctx) { m_arg_idx = 0; m_name = symbol::null; }
+    virtual void prepare(cmd_context& ctx) { m_arg_idx = 0; m_name = symbol::null; m_bound = UINT_MAX; }
     virtual void finalize(cmd_context & ctx) { 
     }
     virtual void execute(cmd_context & ctx) {
-        m_dl_ctx->add_rule(m_t, m_name);
+      m_dl_ctx->add_rule(m_t, m_name, m_bound);
     }
 };
 

src/muz/transforms/dl_transforms.cpp

@@ -71,7 +71,8 @@ namespace datalog {
         transf.register_plugin(alloc(datalog::mk_quantifier_instantiation, ctx, 32000));
 
         transf.register_plugin(alloc(datalog::mk_bit_blast, ctx, 35000));
-        transf.register_plugin(alloc(datalog::mk_array_blast, ctx, 36000));
+        if (!ctx.get_params().quantify_arrays())
+	  transf.register_plugin(alloc(datalog::mk_array_blast, ctx, 36000));
         transf.register_plugin(alloc(datalog::mk_karr_invariants, ctx, 36010));
         if (ctx.get_params().magic()) {
             transf.register_plugin(alloc(datalog::mk_magic_symbolic, ctx, 36020));

src/smt/smt_context.h

@@ -54,7 +54,11 @@ Revision History:
 // the case that each context only references a few expressions.
 // Using a map instead of a vector for the literals can compress space 
 // consumption.
+#ifdef SPARSE_MAP
+#define USE_BOOL_VAR_VECTOR 0
+#else
 #define USE_BOOL_VAR_VECTOR 1
+#endif
 
 namespace smt {
 
@@ -69,6 +73,7 @@ namespace smt {
         std::string last_failure_as_string() const;
         void set_progress_callback(progress_callback *callback);
 
+
     protected:
         ast_manager &               m_manager;
         smt_params &                m_fparams;
@@ -106,7 +111,7 @@ namespace smt {
         // -----------------------------------
         enode *                     m_true_enode;
         enode *                     m_false_enode;
-        ptr_vector<enode>           m_app2enode;    // app -> enode
+        app2enode_t                 m_app2enode;    // app -> enode
         ptr_vector<enode>           m_enodes;
         plugin_manager<theory>      m_theories;     // mapping from theory_id -> theory
         ptr_vector<theory>          m_theory_set;   // set of theories for fast traversal

src/smt/smt_enode.cpp

@@ -24,7 +24,7 @@ namespace smt {
     /**
        \brief Initialize an enode in the given memory position.
     */
-    enode * enode::init(ast_manager & m, void * mem, ptr_vector<enode> const & app2enode, app * owner, 
+    enode * enode::init(ast_manager & m, void * mem, app2enode_t const & app2enode, app * owner, 
                         unsigned generation, bool suppress_args, bool merge_tf, unsigned iscope_lvl,
                         bool cgc_enabled, bool update_children_parent) {
         SASSERT(m.is_bool(owner) || !merge_tf);
@@ -60,7 +60,7 @@ namespace smt {
         return n;
     }
 
-    enode * enode::mk(ast_manager & m, region & r, ptr_vector<enode> const & app2enode, app * owner, 
+    enode * enode::mk(ast_manager & m, region & r, app2enode_t const & app2enode, app * owner, 
                            unsigned generation, bool suppress_args, bool merge_tf, unsigned iscope_lvl,
                            bool cgc_enabled, bool update_children_parent) {
         SASSERT(m.is_bool(owner) || !merge_tf);
@@ -69,7 +69,7 @@ namespace smt {
         return init(m, mem, app2enode, owner, generation, suppress_args, merge_tf, iscope_lvl, cgc_enabled, update_children_parent);
     }
 
-    enode * enode::mk_dummy(ast_manager & m, ptr_vector<enode> const & app2enode, app * owner) {
+    enode * enode::mk_dummy(ast_manager & m, app2enode_t const & app2enode, app * owner) {
         unsigned sz           = get_enode_size(owner->get_num_args());
         void * mem            = alloc_svect(char, sz);
         return init(m, mem, app2enode, owner, 0, false, false, 0, true, false);

src/smt/smt_enode.h

@@ -38,6 +38,29 @@ namespace smt {
         }
     };
 
+    /** \ brief Use sparse maps in SMT solver.
+
+	Define this to use hash maps rather than vectors over ast
+	nodes. This is useful in the case there are many solvers, each
+	referencing few nodes from a large ast manager. There is some
+	unknown performance penalty for this. */
+
+    // #define SPARSE_MAP
+
+#ifndef SPARSE_MAP
+    typedef ptr_vector<enode> app2enode_t;    // app -> enode
+#else
+    class app2enode_t : public u_map<enode *> {
+    public:
+      void setx(unsigned x, enode *val, enode *def){
+	if(val == 0)
+	  erase(x);
+	else
+	  insert(x,val);
+      }
+    };
+#endif
+
     class tmp_enode;
 
     /**
@@ -115,7 +138,7 @@ namespace smt {
 
         friend class tmp_enode;
 
-        static enode * init(ast_manager & m, void * mem, ptr_vector<enode> const & app2enode, app * owner, 
+        static enode * init(ast_manager & m, void * mem, app2enode_t const & app2enode, app * owner, 
                             unsigned generation, bool suppress_args, bool merge_tf, unsigned iscope_lvl,
                             bool cgc_enabled, bool update_children_parent);
     public:
@@ -124,11 +147,11 @@ namespace smt {
             return sizeof(enode) + num_args * sizeof(enode*);
         }
         
-        static enode * mk(ast_manager & m, region & r, ptr_vector<enode> const & app2enode, app * owner, 
+        static enode * mk(ast_manager & m, region & r, app2enode_t const & app2enode, app * owner, 
                           unsigned generation, bool suppress_args, bool merge_tf, unsigned iscope_lvl,
                           bool cgc_enabled, bool update_children_parent);
 
-        static enode * mk_dummy(ast_manager & m, ptr_vector<enode> const & app2enode, app * owner);
+        static enode * mk_dummy(ast_manager & m, app2enode_t const & app2enode, app * owner);
         
         static void del_dummy(enode * n) { dealloc_svect(reinterpret_cast<char*>(n)); }
 

src/smt/theory_array_base.cpp

@@ -376,8 +376,10 @@ namespace smt {
         enode_vector::const_iterator end = r->end_parents();
         for (; it != end; ++it) {
             enode * parent       = *it;
+#if 0
             if (!ctx.is_relevant(parent))
                 continue;
+#endif
             unsigned    num_args = parent->get_num_args();
             if (is_store(parent)) {
                 SET_ARRAY(parent->get_arg(0));
@@ -399,6 +401,7 @@ namespace smt {
         return false;
     }
 
+#if 0
     void theory_array_base::collect_shared_vars(sbuffer<theory_var> & result) {
         TRACE("array_shared", tout << "collecting shared vars...\n";);
         context & ctx = get_context();
@@ -420,6 +423,31 @@ namespace smt {
         }
         unmark_enodes(to_unmark.size(), to_unmark.c_ptr());
     }
+#else
+    void theory_array_base::collect_shared_vars(sbuffer<theory_var> & result) {
+        TRACE("array_shared", tout << "collecting shared vars...\n";);
+        context & ctx = get_context();
+        ptr_buffer<enode> to_unmark;
+        unsigned num_vars = get_num_vars();
+        for (unsigned i = 0; i < num_vars; i++) {
+	    enode * n = get_enode(i);
+            if (ctx.is_relevant(n)) {
+	        enode * r = n->get_root();
+		if (!r->is_marked()){
+		    if(is_array_sort(r) && ctx.is_shared(r)) {
+		      TRACE("array_shared", tout << "new shared var: #" << r->get_owner_id() << "\n";);
+		      theory_var r_th_var = r->get_th_var(get_id());
+		      SASSERT(r_th_var != null_theory_var);
+		      result.push_back(r_th_var);
+		    }
+		    r->set_mark();
+		    to_unmark.push_back(r);
+		}
+            }
+        }
+        unmark_enodes(to_unmark.size(), to_unmark.c_ptr());
+    }
+#endif
 
     /**
        \brief Create interface variables for shared array variables.

src/util/map.h

@@ -131,7 +131,7 @@ public:
     value const& get(key const& k, value const& default_value) const {
         entry* e = find_core(k);
         if (e) {
-            return e->m_value;
+	  return e->get_data().m_value;
         }
         else {
             return default_value;