remove simplify dependencies

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

src/ast/rewriter/bv_elim2.cpp

@@ -0,0 +1,115 @@
+
+/*++
+Copyright (c) 2015 Microsoft Corporation
+
+--*/
+
+#include "ast/rewriter/bv_elim2.h"
+#include "ast/bv_decl_plugin.h"
+#include "ast/rewriter/var_subst.h"
+#include "ast/rewriter/rewriter_def.h"
+#include <sstream>
+
+bool bv_elim_cfg::reduce_quantifier(quantifier * q, 
+                                expr * body, 
+                                expr * const * new_patterns, 
+                                expr * const * new_no_patterns,
+                                expr_ref & result,
+                                proof_ref & result_pr) {
+
+
+    svector<symbol>  names, _names;
+    sort_ref_buffer  sorts(m), _sorts(m);
+    expr_ref_buffer  pats(m);
+    expr_ref_buffer  no_pats(m);
+    expr_ref_buffer  subst_map(m), _subst_map(m);
+    var_subst        subst(m);
+    bv_util          bv(m);
+    expr_ref         new_body(m);
+    expr*            old_body = body;
+    unsigned num_decls = q->get_num_decls();
+    family_id bfid = m.mk_family_id("bv");
+
+    //
+    // Traverse sequence of bound variables to eliminate
+    // bit-vecctor variables and replace them by 
+    // Booleans.
+    // 
+    unsigned var_idx = 0;
+    bool found = false;
+    for (unsigned i = num_decls; i > 0; ) {
+        --i;
+        sort*  s  = q->get_decl_sort(i);
+        symbol nm = q->get_decl_name(i);
+
+        if (bv.is_bv_sort(s)) {
+            // convert n-bit bit-vector variable into sequence of n-Booleans.
+            unsigned num_bits = bv.get_bv_size(s);
+            expr_ref_buffer args(m);
+            expr_ref bv(m);
+            found = true;
+            for (unsigned j = 0; j < num_bits; ++j) {
+                std::ostringstream new_name;
+                new_name << nm.str();
+                new_name << "_";
+                new_name << j;
+                var* v = m.mk_var(var_idx++, m.mk_bool_sort());                
+                args.push_back(v);
+                _sorts.push_back(m.mk_bool_sort());
+                _names.push_back(symbol(new_name.str().c_str()));
+            }
+            bv = m.mk_app(bfid, OP_MKBV, 0, 0, args.size(), args.c_ptr());
+            _subst_map.push_back(bv.get());
+        }
+        else {
+            _subst_map.push_back(m.mk_var(var_idx++, s));
+            _sorts.push_back(s);
+            _names.push_back(nm);
+        }
+    }
+    if (!found) {
+        return false;
+    }
+    // 
+    // reverse the vectors.
+    // 
+    SASSERT(_names.size() == _sorts.size());
+    for (unsigned i = _names.size(); i > 0; ) {
+        --i;
+        names.push_back(_names[i]);
+        sorts.push_back(_sorts[i]);
+    }
+    for (unsigned i = _subst_map.size(); i > 0; ) {
+        --i;
+        subst_map.push_back(_subst_map[i]);
+    }
+
+    expr* const* sub  = subst_map.c_ptr();
+    unsigned sub_size = subst_map.size();
+
+    subst(old_body, sub_size, sub, new_body);
+
+    for (unsigned j = 0; j < q->get_num_patterns(); j++) {
+        expr_ref pat(m);        
+        subst(new_patterns[j], sub_size, sub, pat);
+        pats.push_back(pat);
+    }
+    for (unsigned j = 0; j < q->get_num_no_patterns(); j++) {
+        expr_ref nopat(m);
+        subst(new_no_patterns[j], sub_size, sub, nopat);
+        no_pats.push_back(nopat);
+    }
+
+    result = m.mk_quantifier(true, 
+                        names.size(),
+                        sorts.c_ptr(),
+                        names.c_ptr(),
+                        new_body.get(),
+                        q->get_weight(),
+                        q->get_qid(),
+                        q->get_skid(),
+                        pats.size(), pats.c_ptr(),
+                        no_pats.size(), no_pats.c_ptr());
+    result_pr = m.mk_rewrite(q, result);
+    return true;
+}

src/ast/rewriter/bv_elim2.h

@@ -0,0 +1,50 @@
+/*++
+Copyright (c) 2006 Microsoft Corporation
+
+Module Name:
+
+    bv_elim.h
+
+Abstract:
+
+    Eliminate bit-vectors variables from clauses, by
+    replacing them by bound Boolean variables.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2008-12-16.
+
+Revision History:
+
+--*/
+#ifndef BV_ELIM2_H_
+#define BV_ELIM2_H_
+
+#include "ast/ast.h"
+#include "ast/rewriter/rewriter.h"
+
+class bv_elim_cfg : public default_rewriter_cfg {
+    ast_manager& m;
+public:
+    bv_elim_cfg(ast_manager& m) : m(m) {}
+
+    bool reduce_quantifier(quantifier * old_q, 
+                           expr * new_body, 
+                           expr * const * new_patterns, 
+                           expr * const * new_no_patterns,
+                           expr_ref & result,
+                           proof_ref & result_pr);
+};
+
+class bv_elim_rw : public rewriter_tpl<bv_elim_cfg> {
+protected:
+    bv_elim_cfg  m_cfg;
+public:
+    bv_elim_rw(ast_manager & m):
+        rewriter_tpl<bv_elim_cfg>(m, m.proofs_enabled(), m_cfg),
+        m_cfg(m)
+    {} 
+};
+
+#endif /* BV_ELIM_H_ */
+

src/ast/rewriter/elim_bounds2.cpp

@@ -0,0 +1,203 @@
+/*++
+Copyright (c) 2006 Microsoft Corporation
+
+Module Name:
+
+    elim_bounds2.cpp
+
+Abstract:
+
+    <abstract>
+
+Author:
+
+    Leonardo de Moura (leonardo) 2008-06-28.
+
+Revision History:
+
+--*/
+
+#ifndef ELIM_BOUNDS_H_
+#define ELIM_BOUNDS_H_
+
+#include "ast/used_vars.h"
+#include "util/obj_hashtable.h"
+#include "ast/rewriter/var_subst.h"
+#include "ast/rewriter/elim_bounds2.h"
+#include "ast/ast_pp.h"
+
+elim_bounds_cfg::elim_bounds_cfg(ast_manager & m):
+    m(m),
+    m_util(m) {
+}
+
+/**
+   \brief Find bounds of the form
+
+   (<= x k)
+   (<= (+ x (* -1 y)) k)
+   (<= (+ x (* -1 t)) k)
+   (<= (+ t (* -1 x)) k)
+
+   x and y are a bound variables, t is a ground term and k is a numeral
+
+   It also detects >=, and the atom can be negated.
+*/
+bool elim_bounds_cfg::is_bound(expr * n, var * & lower, var * & upper) {
+    upper    = 0;
+    lower    = 0;
+    bool neg = false;
+    if (m.is_not(n)) {
+        n   = to_app(n)->get_arg(0);
+        neg = true;
+    }
+
+    expr* l = 0, *r = 0;
+    bool le  = false;
+    if (m_util.is_le(n, l, r) && m_util.is_numeral(r)) {
+        n  = l;
+        le = true;
+    }
+    else if (m_util.is_ge(n, l, r) && m_util.is_numeral(r)) {
+        n  = l;
+        le = false;
+    }
+    else {
+        return false;
+    }
+
+    if (neg)
+        le = !le;
+
+    if (is_var(n)) {
+        upper = to_var(n);
+    }
+    else if (m_util.is_add(n, l, r)) {
+        expr * arg1 = l;
+        expr * arg2 = r;
+        if (is_var(arg1))
+            upper   = to_var(arg1);
+        else if (!is_ground(arg1))
+            return false;
+        rational k;
+        bool is_int;
+        if (m_util.is_mul(arg2) && m_util.is_numeral(to_app(arg2)->get_arg(0), k, is_int) && k.is_minus_one()) {
+            arg2    = to_app(arg2)->get_arg(1);
+            if (is_var(arg2))
+                lower = to_var(arg2);
+            else if (!is_ground(arg2))
+                return false; // not supported
+        }
+        else {
+            return false; // not supported
+        }
+    }
+    else {
+        return false;
+    }
+
+    if (!le)
+        std::swap(upper, lower);
+
+    return true;
+}
+
+bool elim_bounds_cfg::is_bound(expr * n) {
+    var * lower, * upper;
+    return is_bound(n, lower, upper);
+}
+
+
+bool elim_bounds_cfg::reduce_quantifier(quantifier * q, 
+                                     expr * n, 
+                                     expr * const * new_patterns, 
+                                     expr * const * new_no_patterns,
+                                     expr_ref & result,
+                                     proof_ref & result_pr) {
+    if (!q->is_forall()) {
+        return false;
+    }
+    unsigned num_vars = q->get_num_decls();
+    ptr_buffer<expr> atoms;
+    if (m.is_or(n))
+        atoms.append(to_app(n)->get_num_args(), to_app(n)->get_args());
+    else
+        atoms.push_back(n);
+    used_vars          used_vars;
+    // collect non-candidates
+    for (expr * a : atoms) {
+        if (!is_bound(a))
+            used_vars.process(a);
+    }
+    if (used_vars.uses_all_vars(q->get_num_decls())) {
+        return false;
+    }
+    // collect candidates
+    obj_hashtable<var> lowers;
+    obj_hashtable<var> uppers;
+    obj_hashtable<var> candidate_set;
+    ptr_buffer<var>    candidates;
+#define ADD_CANDIDATE(V) if (!lowers.contains(V) && !uppers.contains(V)) { candidate_set.insert(V); candidates.push_back(V); }
+    for (expr * a : atoms) {
+        var * lower = 0;
+        var * upper = 0;
+        if (is_bound(a, lower, upper)) {
+            if (lower != 0 && !used_vars.contains(lower->get_idx()) && lower->get_idx() < num_vars) {
+                ADD_CANDIDATE(lower);
+                lowers.insert(lower);
+            }
+            if (upper != 0 && !used_vars.contains(upper->get_idx()) && upper->get_idx() < num_vars) {
+                ADD_CANDIDATE(upper);
+                uppers.insert(upper);
+            }
+        }
+    }
+    TRACE("elim_bounds", tout << "candidates:\n"; for (unsigned i = 0; i < candidates.size(); i++) tout << mk_pp(candidates[i], m) << "\n";);
+    // remove candidates that have lower and upper bounds
+
+    for (var * v : candidates) {
+        if (lowers.contains(v) && uppers.contains(v))
+            candidate_set.erase(v);
+    }
+    TRACE("elim_bounds", tout << "candidates after filter:\n"; for (unsigned i = 0; i < candidates.size(); i++) tout << mk_pp(candidates[i], m) << "\n";);
+    if (candidate_set.empty()) {
+        return false;
+    }
+    // remove bounds that contain variables in candidate_set
+    unsigned j = 0;
+    for (unsigned i = 0; i < atoms.size(); ++i) {
+        expr * a = atoms[i];
+        var * lower = 0;
+        var * upper = 0;
+        if (is_bound(a, lower, upper) && ((lower != 0 && candidate_set.contains(lower)) || (upper != 0 && candidate_set.contains(upper))))
+            continue;
+        atoms[j] = a;
+        j++;
+    }
+    if (j == atoms.size()) {
+        return false;
+    }
+    atoms.resize(j);
+    expr * new_body = 0;
+    switch (atoms.size()) {
+    case 0:
+        result = m.mk_false();
+        result_pr = m.mk_rewrite(q, result);
+        TRACE("elim_bounds", tout << mk_pp(q, m) << "\n" << result << "\n";);
+        return true;
+    case 1:
+        new_body = atoms[0];
+        break;
+    default:
+        new_body = m.mk_or(atoms.size(), atoms.c_ptr());
+        break;
+    }
+    quantifier_ref new_q(m);
+    new_q = m.update_quantifier(q, new_body);
+    elim_unused_vars(m, new_q, params_ref(), result);
+    result_pr = m.mk_rewrite(q, result);
+    TRACE("elim_bounds", tout << mk_pp(q, m) << "\n" << result << "\n";);
+    return true;
+}
+
+#endif /* ELIM_BOUNDS_H_ */

src/ast/rewriter/elim_bounds2.h

@@ -0,0 +1,77 @@
+/*++
+Copyright (c) 2006 Microsoft Corporation
+
+Module Name:
+
+    elim_bounds2.h
+
+Abstract:
+
+    <abstract>
+
+Author:
+
+    Leonardo de Moura (leonardo) 2008-06-28.
+
+Revision History:
+
+--*/
+#ifndef ELIM_BOUNDS2_H_
+#define ELIM_BOUNDS2_H_
+
+#include "ast/ast.h"
+#include "ast/arith_decl_plugin.h"
+#include "ast/rewriter/rewrite.h"
+
+/**
+   \brief Functor for eliminating irrelevant bounds in quantified formulas.
+   
+   Example:
+   (forall (x Int) (y Int) (or (not (>= y x) (not (>= x 0)) (= (select a x) 1))))
+
+   The bound (>= y x) is irrelevant and can be eliminated.
+
+   This can be easily proved by using Fourier-Motzkin elimination.
+
+   Limitations & Assumptions:
+   - It assumes the input formula was already simplified.
+   - It can only handle bounds in the diff-logic fragment.
+
+   \remark This operation is subsumed by Fourier-Motzkin elimination.
+*/
+class elim_bounds_cfg : public default_rewriter_cfg {
+    ast_manager &      m;
+    arith_util         m_util;
+    bool is_bound(expr * n, var * & lower, var * & upper);
+    bool is_bound(expr * n);
+public:
+    elim_bounds_cfg(ast_manager & m);
+    
+    bool reduce_quantifier(quantifier * old_q, 
+                           expr * new_body, 
+                           expr * const * new_patterns, 
+                           expr * const * new_no_patterns,
+                           expr_ref & result,
+                           proof_ref & result_pr);
+};
+
+/**
+   \brief Functor for applying elim_bounds2 in all
+   universal quantifiers in an expression.
+
+   Assumption: the formula was already skolemized.
+*/
+class elim_bounds_rw : public rewriter_tpl<elim_bounds_cfg> {
+protected:
+    elim_bounds_cfg  m_cfg;
+public:
+    elim_bounds_rw(ast_manager & m):
+        rewriter_tpl<elim_bounds_cfg>(m, m.proofs_enabled(), m_cfg),
+        m_cfg(m)
+    {} 
+
+    virtual ~elim_bounds_rw() {}
+};
+
+#endif /* ELIM_BOUNDS2_H_ */
+