removing dependencies on simplifier

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

src/ast/rewriter/elim_bounds.cpp

@@ -0,0 +1,203 @@
+/*++
+Copyright (c) 2006 Microsoft Corporation
+
+Module Name:
+
+    elim_bounds.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_bounds.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_bounds.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/rewriter.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_ */
+