declutter spacer_manager

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/ast/expr_abstract.h

@@ -33,6 +33,7 @@ public:
 };
 
 void expr_abstract(ast_manager& m, unsigned base, unsigned num_bound, expr* const* bound, expr* n, expr_ref&  result);
+inline expr_ref expr_abstract(ast_manager& m, unsigned base, unsigned num_bound, expr* const* bound, expr* n) { expr_ref r(m); expr_abstract(m, base, num_bound, bound, n); return r; }
 expr_ref mk_forall(ast_manager& m, unsigned num_bound, app* const* bound, expr* n);
 expr_ref mk_exists(ast_manager& m, unsigned num_bound, app* const* bound, expr* n);
 

src/ast/rewriter/bool_rewriter.h

@@ -145,6 +145,27 @@ public:
         if (mk_or_core(num_args, args, result) == BR_FAILED)
             result = m().mk_or(num_args, args);
     }
+    expr_ref mk_or(unsigned num_args, expr * const * args) {
+        expr_ref result(m());
+        mk_or(num_args, args, result);
+        return result;
+    }
+    expr_ref mk_and(unsigned num_args, expr * const * args) {
+        expr_ref result(m());
+        mk_and(num_args, args, result);
+        return result;
+    }
+    expr_ref mk_or(expr_ref_vector const& args) {
+        expr_ref result(m());
+        mk_or(args.size(), args.c_ptr(), result);
+        return result;
+    }
+    expr_ref mk_and(expr_ref_vector const& args) {
+        expr_ref result(m());
+        mk_and(args.size(), args.c_ptr(), result);
+        return result;
+    }
+
     void mk_and(expr * arg1, expr * arg2, expr_ref & result) {
         expr * args[2] = {arg1, arg2};
         mk_and(2, args, result);

src/muz/spacer/spacer_manager.cpp

@@ -61,22 +61,19 @@ typedef hashtable<symbol, symbol_hash_proc, symbol_eq_proc> symbol_set;
 expr_ref inductive_property::fixup_clause(expr* fml) const
 {
     expr_ref_vector disjs(m);
-    flatten_or(fml, disjs);
+    flatten_or(fml, disjs);    
-    expr_ref result(m);
+    return bool_rewriter(m).mk_or(disjs);
-    bool_rewriter(m).mk_or(disjs.size(), disjs.c_ptr(), result);
-    return result;
 }
 
 expr_ref inductive_property::fixup_clauses(expr* fml) const
 {
     expr_ref_vector conjs(m);
-    expr_ref result(m);
     flatten_and(fml, conjs);
-    for (unsigned i = 0; i < conjs.size(); ++i) {
+    unsigned i = 0;
-        conjs[i] = fixup_clause(conjs.get(i));
+    for (expr* c : conjs) {
+        conjs[i++] = fixup_clause(c);
     }
-    bool_rewriter(m).mk_and(conjs.size(), conjs.c_ptr(), result);
+    return bool_rewriter(m).mk_and(conjs);
-    return result;
 }
 
 std::string inductive_property::to_string() const
@@ -90,20 +87,15 @@ std::string inductive_property::to_string() const
 
 void inductive_property::to_model(model_ref& md) const {
     md = alloc(model, m);
-    vector<relation_info> const& rs = m_relation_info;
+    for (relation_info const& ri : m_relation_info) {
-    expr_ref_vector conjs(m);
-    for (relation_info const& ri_ : rs) {
-        relation_info ri(ri_);
-        func_decl * pred = ri.m_pred;
         expr_ref prop = fixup_clauses(ri.m_body);
         func_decl_ref_vector const& sig = ri.m_vars;
-        expr_ref q(m);
         expr_ref_vector sig_vars(m);
         for (unsigned j = 0; j < sig.size(); ++j) {
             sig_vars.push_back(m.mk_const(sig[sig.size() - j - 1]));
         }
-        expr_abstract(m, 0, sig_vars.size(), sig_vars.c_ptr(), prop, q);
+        expr_ref q = expr_abstract(m, 0, sig_vars.size(), sig_vars.c_ptr(), prop);
-        md->register_decl(pred, q);
+        md->register_decl(ri.m_pred, q);
     }
     TRACE("spacer", tout << *md;);
     apply(const_cast<model_converter_ref&>(m_mc), md);
@@ -125,37 +117,33 @@ void inductive_property::display(datalog::rule_manager& rm, ptr_vector<datalog::
     func_decl_set bound_decls, aux_decls;
     collect_decls_proc collect_decls(bound_decls, aux_decls);
 
-    for (unsigned i = 0; i < m_relation_info.size(); ++i) {
+    for (auto const& ri : m_relation_info) {
-        bound_decls.insert(m_relation_info[i].m_pred);
+        bound_decls.insert(ri.m_pred);
-        func_decl_ref_vector const& sig = m_relation_info[i].m_vars;
+        for (func_decl* b : ri.m_vars) {
-        for (unsigned j = 0; j < sig.size(); ++j) {
+            bound_decls.insert(b);
-            bound_decls.insert(sig[j]);
         }
-        for_each_expr(collect_decls, m_relation_info[i].m_body);
+        for_each_expr(collect_decls, ri.m_body);
     }
-    for (unsigned i = 0; i < rules.size(); ++i) {
+    for (auto* r : rules) {
-        bound_decls.insert(rules[i]->get_decl());
+        bound_decls.insert(r->get_decl());
     }
-    for (unsigned i = 0; i < rules.size(); ++i) {
+    for (auto* r : rules) {
-        unsigned u_sz = rules[i]->get_uninterpreted_tail_size();
+        unsigned u_sz = r->get_uninterpreted_tail_size();
-        unsigned t_sz = rules[i]->get_tail_size();
+        unsigned t_sz =  r->get_tail_size();
         for (unsigned j = u_sz; j < t_sz; ++j) {
-            for_each_expr(collect_decls, rules[i]->get_tail(j));
+            for_each_expr(collect_decls, r->get_tail(j));
         }
     }
     smt2_pp_environment_dbg env(m);
-    func_decl_set::iterator it = aux_decls.begin(), end = aux_decls.end();
+    for (func_decl* f : aux_decls) {
-    for (; it != end; ++it) {
+        ast_smt2_pp(out, f, env) << "\n";
-        func_decl* f = *it;
-        ast_smt2_pp(out, f, env);
-        out << "\n";
     }
 
     out << to_string() << "\n";
-    for (unsigned i = 0; i < rules.size(); ++i) {
+    for (auto* r : rules) {
         out << "(push)\n";
         out << "(assert (not\n";
-        rm.display_smt2(*rules[i], out);
+        rm.display_smt2(*r, out);
         out << "))\n";
         out << "(check-sat)\n";
         out << "(pop)\n";