merge useful utilities from qsat

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

src/ast/arith_decl_plugin.cpp

@@ -664,3 +664,45 @@ algebraic_numbers::anum const & arith_util::to_irrational_algebraic_numeral(expr
     SASSERT(is_irrational_algebraic_numeral(n));
     return plugin().aw().to_anum(to_app(n)->get_decl());
 }
+
+expr_ref arith_util::mk_mul_simplify(expr_ref_vector const& args) {
+    return mk_mul_simplify(args.size(), args.c_ptr());
+
+}
+expr_ref arith_util::mk_mul_simplify(unsigned sz, expr* const* args) {
+    expr_ref result(m_manager);
+    
+    switch (sz) {
+    case 0:
+        result = mk_numeral(rational(1), true);
+        break;
+    case 1:
+        result = args[0];
+        break;
+    default:
+        result = mk_mul(sz, args);
+        break;                    
+    }
+    return result;
+}
+
+expr_ref arith_util::mk_add_simplify(expr_ref_vector const& args) {
+    return mk_add_simplify(args.size(), args.c_ptr());
+
+}
+expr_ref arith_util::mk_add_simplify(unsigned sz, expr* const* args) {
+    expr_ref result(m_manager);
+    
+    switch (sz) {
+    case 0:
+        result = mk_numeral(rational(0), true);
+        break;
+    case 1:
+        result = args[0];
+        break;
+    default:
+        result = mk_add(sz, args);
+        break;                    
+    }
+    return result;
+}

src/ast/arith_decl_plugin.h

@@ -149,7 +149,6 @@ protected:
     func_decl * m_mod_0_decl;
     func_decl * m_u_asin_decl;
     func_decl * m_u_acos_decl;
-
     ptr_vector<app> m_small_ints;
     ptr_vector<app> m_small_reals;
 
@@ -416,6 +415,11 @@ public:
         return m_manager.mk_eq(lhs, rhs);
     }
 
+    expr_ref mk_mul_simplify(expr_ref_vector const& args);
+    expr_ref mk_mul_simplify(unsigned sz, expr* const* args);
+
+    expr_ref mk_add_simplify(expr_ref_vector const& args);
+    expr_ref mk_add_simplify(unsigned sz, expr* const* args);
 };
 
 #endif /* ARITH_DECL_PLUGIN_H_ */

src/ast/ast_smt2_pp.cpp

@@ -1200,6 +1200,14 @@ std::ostream& operator<<(std::ostream& out, app_ref const&  e) {
     return out << mk_ismt2_pp(e.get(), e.get_manager());
 }
 
+std::ostream& operator<<(std::ostream& out, func_decl_ref const&  e) {
+    return out << mk_ismt2_pp(e.get(), e.get_manager());
+}
+
+std::ostream& operator<<(std::ostream& out, sort_ref const&  e) {
+    return out << mk_ismt2_pp(e.get(), e.get_manager());
+}
+
 std::ostream& operator<<(std::ostream& out, expr_ref_vector const&  e) {
     for (unsigned i = 0; i < e.size(); ++i) {
         out << mk_ismt2_pp(e[i], e.get_manager());
@@ -1216,6 +1224,18 @@ std::ostream& operator<<(std::ostream& out, app_ref_vector const&  e) {
     return out;
 }
 
+std::ostream& operator<<(std::ostream& out, func_decl_ref_vector const&  e) {
+    for (unsigned i = 0; i < e.size(); ++i) 
+        out << mk_ismt2_pp(e[i], e.get_manager()) << "\n";
+    return out;
+}
+
+std::ostream& operator<<(std::ostream& out, sort_ref_vector const&  e) {
+    for (unsigned i = 0; i < e.size(); ++i) 
+        out << mk_ismt2_pp(e[i], e.get_manager()) << "\n";
+    return out;
+}
+
 #ifdef Z3DEBUG
 void pp(expr const * n, ast_manager & m) {
     std::cout << mk_ismt2_pp(const_cast<expr*>(n), m) << std::endl;

src/ast/ast_smt2_pp.h

@@ -117,8 +117,13 @@ std::ostream& operator<<(std::ostream& out, mk_ismt2_pp const & p);
 
 std::ostream& operator<<(std::ostream& out, expr_ref const& e);
 std::ostream& operator<<(std::ostream& out, app_ref const& e);
+std::ostream& operator<<(std::ostream& out, func_decl_ref const& e);
+std::ostream& operator<<(std::ostream& out, sort_ref const& e);
+
 
 std::ostream& operator<<(std::ostream& out, expr_ref_vector const& e);
 std::ostream& operator<<(std::ostream& out, app_ref_vector const& e);
+std::ostream& operator<<(std::ostream& out, func_decl_ref_vector const& e);
+std::ostream& operator<<(std::ostream& out, sort_ref_vector const& e);
 
 #endif

src/ast/ast_util.cpp

@@ -170,7 +170,6 @@ app* mk_and(ast_manager & m, unsigned num_args, app * const * args) {
     return to_app(mk_and(m, num_args, (expr* const*) args));
 }
 
-
 expr * mk_or(ast_manager & m, unsigned num_args, expr * const * args) {
     if (num_args == 0)
         return m.mk_false();
@@ -188,10 +187,43 @@ expr * mk_not(ast_manager & m, expr * arg) {
     expr * atom;
     if (m.is_not(arg, atom))
         return atom;
+    else if (m.is_true(arg)) 
+        return m.mk_false();
+    else if (m.is_false(arg))
+        return m.mk_true();
     else
         return m.mk_not(arg);
 }
 
+expr_ref push_not(const expr_ref& e) {
+    ast_manager& m = e.get_manager();
+    if (!is_app(e)) {
+        return expr_ref(m.mk_not(e), m);
+    }
+    app* a = to_app(e);
+    if (m.is_and(a)) {
+        if (a->get_num_args() == 0) {
+            return expr_ref(m.mk_false(), m);
+        }
+        expr_ref_vector args(m);
+        for (unsigned i = 0; i < a->get_num_args(); ++i) {
+            args.push_back(push_not(expr_ref(a->get_arg(i), m)));
+        }
+        return mk_or(args);
+    }
+    if (m.is_or(a)) {
+        if (a->get_num_args() == 0) {
+            return expr_ref(m.mk_true(), m);
+        }
+        expr_ref_vector args(m);
+        for (unsigned i = 0; i < a->get_num_args(); ++i) {
+            args.push_back(push_not(expr_ref(a->get_arg(i), m)));
+        }
+        return mk_and(args);
+    }
+    return expr_ref(mk_not(m, e), m);    
+}
+
 expr * expand_distinct(ast_manager & m, unsigned num_args, expr * const * args) {
     expr_ref_buffer new_diseqs(m);
     for (unsigned i = 0; i < num_args; i++) {
@@ -201,6 +233,24 @@ expr * expand_distinct(ast_manager & m, unsigned num_args, expr * const * args)
     return mk_and(m, new_diseqs.size(), new_diseqs.c_ptr());
 }
 
+expr* mk_distinct(ast_manager& m, unsigned num_args, expr * const * args) {
+    switch (num_args) {
+    case 0:
+    case 1:
+        return m.mk_true();
+    case 2:
+        return m.mk_not(m.mk_eq(args[0], args[1]));
+    default:
+        return m.mk_distinct(num_args, args);
+    }
+}
+
+expr_ref mk_distinct(expr_ref_vector const& args) {
+    ast_manager& m = args.get_manager();
+    return expr_ref(mk_distinct(m, args.size(), args.c_ptr()), m);
+}
+
+
 void flatten_and(expr_ref_vector& result) {
     ast_manager& m = result.get_manager();
     expr* e1, *e2, *e3;

src/ast/ast_util.h

@@ -121,18 +121,29 @@ app  * mk_or(ast_manager & m, unsigned num_args, app * const * args);
 inline app_ref mk_or(app_ref_vector const& args) { return app_ref(mk_or(args.get_manager(), args.size(), args.c_ptr()), args.get_manager()); }
 inline expr_ref mk_or(expr_ref_vector const& args) { return expr_ref(mk_or(args.get_manager(), args.size(), args.c_ptr()), args.get_manager()); }
 
-
 /**
    Return a          if arg = (not a)
    Retur (not arg)   otherwise
  */
 expr * mk_not(ast_manager & m, expr * arg);
 
+/**
+   Negate and push over conjunction or disjunction.
+ */
+expr_ref push_not(const expr_ref& arg);
+
 /**
    Return the expression (and (not (= args[0] args[1])) (not (= args[0] args[2])) ... (not (= args[num_args-2] args[num_args-1])))
 */
 expr * expand_distinct(ast_manager & m, unsigned num_args, expr * const * args);
 
+/**
+   Create simplified distinct term. Binary distinct becomes a single disequality.
+ */
+expr * mk_distinct(ast_manager& m, unsigned num_args, expr * const * args);
+
+expr_ref mk_distinct(expr_ref_vector const& args);
+
 /**
    \brief Collect top-level conjunctions and disjunctions.
 */

src/ast/bv_decl_plugin.cpp

@@ -865,6 +865,12 @@ sort * bv_util::mk_sort(unsigned bv_size) {
     return m_manager.mk_sort(get_fid(), BV_SORT, 1, p);
 }
 
+unsigned bv_util::get_int2bv_size(parameter const& p) {
+    int sz;
+    VERIFY(m_plugin->get_int2bv_size(1, &p, sz));
+    return static_cast<unsigned>(sz);
+}
+
 app * bv_util::mk_bv2int(expr* e) {
     sort* s = m_manager.mk_sort(m_manager.mk_family_id("arith"), INT_SORT);
     parameter p(s);

src/ast/bv_decl_plugin.h

@@ -234,7 +234,6 @@ protected:
 
     func_decl * mk_mkbv(unsigned arity, sort * const * domain);
 
-    bool get_int2bv_size(unsigned num_parameters, parameter const * parameters, int & result);
 
     func_decl * mk_num_decl(unsigned num_parameters, parameter const * parameters, unsigned arity);
 
@@ -267,6 +266,8 @@ public:
 
     virtual expr * get_some_value(sort * s);
 
+    bool get_int2bv_size(unsigned num_parameters, parameter const * parameters, int & result);
+
     virtual bool is_considered_uninterpreted(func_decl * f) {
         if (f->get_family_id() != get_family_id())
             return false;
@@ -390,6 +391,8 @@ public:
         return static_cast<unsigned>(s->get_parameter(0).get_int());
     }
     unsigned get_bv_size(expr const * n) const { return get_bv_size(m_manager.get_sort(n)); }
+    unsigned get_int2bv_size(parameter const& p);
+
 
     app * mk_ule(expr * arg1, expr * arg2) { return m_manager.mk_app(get_fid(), OP_ULEQ, arg1, arg2); }
     app * mk_sle(expr * arg1, expr * arg2) { return m_manager.mk_app(get_fid(), OP_SLEQ, arg1, arg2); }
@@ -427,6 +430,7 @@ public:
     app * mk_bvumul_no_ovfl(expr* m, expr* n) { return m_manager.mk_app(get_fid(), OP_BUMUL_NO_OVFL, n, m); }
 
     app * mk_bv(unsigned n, expr* const* es) { return m_manager.mk_app(get_fid(), OP_MKBV, n, es); }
+
 };
 
 #endif /* BV_DECL_PLUGIN_H_ */

src/ast/datatype_decl_plugin.cpp

@@ -1000,3 +1000,25 @@ void datatype_util::display_datatype(sort *s0, std::ostream& strm) {
     }
 
 }
+
+bool datatype_util::is_func_decl(datatype_op_kind k, unsigned num_params, parameter const* params, func_decl* f) {
+    bool eq = 
+        f->get_decl_kind() == k &&
+        f->get_family_id() == m_family_id &&
+        f->get_num_parameters() == num_params;
+    for (unsigned i = 0; eq && i < num_params; ++i) {
+        eq = params[i] == f->get_parameter(i);
+    }
+    return eq;
+}
+
+bool datatype_util::is_constructor_of(unsigned num_params, parameter const* params, func_decl* f) {
+    return 
+        num_params == 2 &&
+        m_family_id == f->get_family_id() &&
+        OP_DT_CONSTRUCTOR == f->get_decl_kind() &&
+        2 == f->get_num_parameters() &&
+        params[0] == f->get_parameter(0) &&
+        params[1] == f->get_parameter(1);
+}
+

src/ast/datatype_decl_plugin.h

@@ -209,6 +209,8 @@ public:
     func_decl * get_recognizer_constructor(func_decl * recognizer);
     family_id get_family_id() const { return m_family_id; }
     bool are_siblings(sort * s1, sort * s2);
+    bool is_func_decl(datatype_op_kind k, unsigned num_params, parameter const* params, func_decl* f);
+    bool is_constructor_of(unsigned num_params, parameter const* params, func_decl* f);
     void reset();
     void display_datatype(sort *s, std::ostream& strm);
 

src/ast/expr_abstract.cpp

@@ -22,6 +22,10 @@ Notes:
 
 void expr_abstractor::operator()(unsigned base, unsigned num_bound, expr* const* bound, expr* n, expr_ref& result) {
     
+    if (num_bound == 0) {
+        result = n;
+        return;
+    }
     expr * curr = 0, *b = 0;
     SASSERT(n->get_ref_count() > 0);
 
@@ -106,3 +110,27 @@ void expr_abstract(ast_manager& m, unsigned base, unsigned num_bound, expr* cons
     expr_abstractor abs(m);
     abs(base, num_bound, bound, n, result);
 }
+
+expr_ref mk_quantifier(bool is_forall, ast_manager& m, unsigned num_bound, app* const* bound, expr* n) {
+    expr_ref result(m);
+    expr_abstract(m, 0, num_bound, (expr* const*)bound, n, result);    
+    if (num_bound > 0) {
+        ptr_vector<sort> sorts;
+        svector<symbol> names;
+        for (unsigned i = 0; i < num_bound; ++i) {
+            sorts.push_back(m.get_sort(bound[i]));
+            names.push_back(bound[i]->get_decl()->get_name());
+        }
+        result = m.mk_quantifier(is_forall, num_bound, sorts.c_ptr(), names.c_ptr(), result);
+    }
+    return result;
+
+}
+
+expr_ref mk_forall(ast_manager& m, unsigned num_bound, app* const* bound, expr* n) {
+    return mk_quantifier(true, m, num_bound, bound, n);
+}
+
+expr_ref mk_exists(ast_manager& m, unsigned num_bound, app* const* bound, expr* n) {
+    return mk_quantifier(false, m, num_bound, bound, n);
+}

src/ast/expr_abstract.h

@@ -33,6 +33,8 @@ public:
 };
 
 void expr_abstract(ast_manager& m, unsigned base, unsigned num_bound, expr* const* bound, expr* n, expr_ref&  result);
+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);
 
 #endif
 

src/ast/rewriter/expr_safe_replace.cpp

@@ -30,6 +30,14 @@ void expr_safe_replace::insert(expr* src, expr* dst) {
     m_subst.insert(src, dst);
 }
 
+void expr_safe_replace::operator()(expr_ref_vector& es) {
+    expr_ref val(m);
+    for (unsigned i = 0; i < es.size(); ++i) {
+        (*this)(es[i].get(), val);
+        es[i] = val;
+    }
+}
+
 void expr_safe_replace::operator()(expr* e, expr_ref& res) {
     m_todo.push_back(e);
     expr* a, *b;

src/ast/rewriter/expr_safe_replace.h

@@ -42,6 +42,8 @@ public:
 
     void operator()(expr* src, expr_ref& e);
 
+    void operator()(expr_ref_vector& es);
+
     void apply_substitution(expr* s, expr* def, expr_ref& t);
 
     void reset();

src/ast/rewriter/quant_hoist.cpp

@@ -73,7 +73,7 @@ public:
         unsigned nd = q->get_num_decls();
         for (unsigned i = 0; i < nd; ++i) {
             sort* s = q->get_decl_sort(i);
-            app* a = m.mk_fresh_const("x", s);
+            app* a = m.mk_fresh_const(q->get_decl_name(i).str().c_str(), s);
             vars.push_back(a);
         }
         expr * const * exprs = (expr* const*) (vars.c_ptr() + vars.size()- nd);
@@ -154,9 +154,7 @@ private:
     }
     
     quantifier_type& negate(quantifier_type& qt) {
-        TRACE("qe", display(qt, tout); tout << "\n";);
         qt = static_cast<quantifier_type>(qt ^0x1);
-        TRACE("qe", display(qt, tout); tout << "\n";);
         return qt;
     }
     
@@ -205,6 +203,7 @@ private:
         case AST_APP: {
             expr_ref_vector args(m);
             expr_ref tmp(m);
+            expr* t1, *t2, *t3;
             unsigned num_args = 0;
             app* a = to_app(fml);
             if (m.is_and(fml)) {
@@ -228,16 +227,35 @@ private:
                 negate(qt);
                 result = m.mk_not(tmp);
             }
-            else if (m.is_implies(fml)) {
-                pull_quantifier(to_app(fml)->get_arg(0), negate(qt), vars, tmp);
+            else if (m.is_implies(fml, t1, t2)) {
+                pull_quantifier(t1, negate(qt), vars, tmp);
                 negate(qt);
-                pull_quantifier(to_app(fml)->get_arg(1), qt, vars, result);
+                pull_quantifier(t2, qt, vars, result);
                 result = m.mk_implies(tmp, result);
             }
-            else if (m.is_ite(fml)) {
-                pull_quantifier(to_app(fml)->get_arg(1), qt, vars, tmp);
-                pull_quantifier(to_app(fml)->get_arg(2), qt, vars, result);
-                result = m.mk_ite(to_app(fml)->get_arg(0), tmp, result);
+            else if (m.is_ite(fml, t1, t2, t3)) {
+                expr_ref tt1(m), tt2(m), tt3(m), ntt1(m), nt1(m);
+                pull_quantifier(t2, qt, vars, tt2);
+                pull_quantifier(t3, qt, vars, tt3);
+                if (has_quantifiers(t1)) {
+                    pull_quantifier(t1, qt, vars, tt1);
+                    nt1 = m.mk_not(t1);
+                    pull_quantifier(nt1, qt, vars, ntt1);
+                    result = m.mk_and(m.mk_or(ntt1, tt2), m.mk_or(tt1, tt3));
+                }
+                else {
+                    result = m.mk_ite(t1, tt2, tt3);
+                }
+            }
+            else if ((m.is_eq(fml, t1, t2) && m.is_bool(t1)) || m.is_iff(fml, t1, t2)) {
+                expr_ref tt1(m), tt2(m), ntt1(m), ntt2(m), nt1(m), nt2(m);
+                pull_quantifier(t1, qt, vars, tt1);
+                pull_quantifier(t2, qt, vars, tt2);
+                nt1 = m.mk_not(t1);
+                nt2 = m.mk_not(t2);
+                pull_quantifier(nt1, qt, vars, ntt1);
+                pull_quantifier(nt2, qt, vars, ntt2);
+                result = m.mk_and(m.mk_or(ntt1, tt2), m.mk_or(ntt2, tt1));
             }
             else {
                 // the formula contains a quantifier, but it is "inaccessible"