restore some code that was removed during the rebase

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

src/ast/rewriter/arith_rewriter.cpp

@@ -800,7 +800,103 @@ br_status arith_rewriter::mk_idiv_core(expr * arg1, expr * arg2, expr_ref & resu
         result = m_util.mk_numeral(div(v1, v2), is_int);
         return BR_DONE;
     }
+    if (m_util.is_numeral(arg2, v2, is_int) && v2.is_one()) {
+        result = arg1; 
+        return BR_DONE; 
+    } 
+    if (m_util.is_numeral(arg2, v2, is_int) && v2.is_zero()) { 
         return BR_FAILED; 
+    } 
+    if (arg1 == arg2) { 
+        expr_ref zero(m_util.mk_int(0), m()); 
+        result = m().mk_ite(m().mk_eq(arg1, zero), m_util.mk_idiv(zero, zero), m_util.mk_int(1)); 
+        return BR_REWRITE3; 
+    } 
+    if (divides(arg1, arg2, result)) { 
+        return BR_REWRITE_FULL; 
+    }  
+    return BR_FAILED;
+}
+ 
+//  
+// implement div ab ac = floor( ab / ac) = floor (b / c) = div b c 
+//
+bool arith_rewriter::divides(expr* num, expr* den, expr_ref& result) { 
+    expr_fast_mark1 mark; 
+    rational num_r(1), den_r(1); 
+    expr* num_e = nullptr, *den_e = nullptr; 
+    ptr_buffer<expr> args1, args2; 
+    flat_mul(num, args1); 
+    flat_mul(den, args2); 
+    for (expr * arg : args1) { 
+        mark.mark(arg); 
+        if (m_util.is_numeral(arg, num_r)) num_e = arg; 
+    } 
+    for (expr* arg : args2) { 
+        if (mark.is_marked(arg)) { 
+            result = remove_divisor(arg, num, den); 
+            return true; 
+        } 
+        if (m_util.is_numeral(arg, den_r)) den_e = arg; 
+    } 
+    rational g = gcd(num_r, den_r); 
+    if (!g.is_one()) { 
+        SASSERT(g.is_pos()); 
+        // replace num_e, den_e by their gcd reduction. 
+        for (unsigned i = 0; i < args1.size(); ++i) { 
+            if (args1[i] == num_e) { 
+                args1[i] = m_util.mk_numeral(num_r / g, true); 
+                break; 
+            } 
+        } 
+        for (unsigned i = 0; i < args2.size(); ++i) { 
+            if (args2[i] == den_e) { 
+                args2[i] = m_util.mk_numeral(den_r / g, true); 
+                break; 
+            } 
+        } 
+        num = m_util.mk_mul(args1.size(), args1.c_ptr()); 
+        den = m_util.mk_mul(args2.size(), args2.c_ptr()); 
+        result = m_util.mk_idiv(num, den); 
+        return true; 
+    } 
+    return false; 
+} 
+
+expr_ref arith_rewriter::remove_divisor(expr* arg, expr* num, expr* den) { 
+    ptr_buffer<expr> args1, args2; 
+    flat_mul(num, args1); 
+    flat_mul(den, args2); 
+    remove_divisor(arg, args1); 
+    remove_divisor(arg, args2); 
+    expr_ref zero(m_util.mk_int(0), m()); 
+    num = args1.empty() ? m_util.mk_int(1) : m_util.mk_mul(args1.size(), args1.c_ptr()); 
+    den = args2.empty() ? m_util.mk_int(1) : m_util.mk_mul(args2.size(), args2.c_ptr()); 
+    return expr_ref(m().mk_ite(m().mk_eq(zero, arg), m_util.mk_idiv(zero, zero), m_util.mk_idiv(num, den)), m()); 
+} 
+ 
+void arith_rewriter::flat_mul(expr* e, ptr_buffer<expr>& args) { 
+    args.push_back(e); 
+    for (unsigned i = 0; i < args.size(); ++i) { 
+        e = args[i]; 
+        if (m_util.is_mul(e)) { 
+            args.append(to_app(e)->get_num_args(), to_app(e)->get_args()); 
+            args[i] = args.back(); 
+            args.shrink(args.size()-1); 
+            --i; 
+        }                 
+    } 
+} 
+ 
+void arith_rewriter::remove_divisor(expr* d, ptr_buffer<expr>& args) { 
+    for (unsigned i = 0; i < args.size(); ++i) { 
+        if (args[i] == d) { 
+            args[i] = args.back(); 
+            args.shrink(args.size()-1); 
+            return; 
+        } 
+    } 
+    UNREACHABLE(); 
 } 
     
 br_status arith_rewriter::mk_mod_core(expr * arg1, expr * arg2, expr_ref & result) {

src/ast/rewriter/arith_rewriter.h

@@ -95,7 +95,10 @@ class arith_rewriter : public poly_rewriter<arith_rewriter_core> {
     expr_ref neg_monomial(expr * e) const;
     expr * mk_sin_value(rational const & k);
     app * mk_sqrt(rational const & k);
-
+    bool divides(expr* d, expr* n, expr_ref& result);
+    expr_ref remove_divisor(expr* arg, expr* num, expr* den); 
+    void flat_mul(expr* e, ptr_buffer<expr>& args); 
+    void remove_divisor(expr* d, ptr_buffer<expr>& args); 
 public:
     arith_rewriter(ast_manager & m, params_ref const & p = params_ref()):
         poly_rewriter<arith_rewriter_core>(m, p) {

src/ast/simplifier/arith_simplifier_plugin.h

@@ -1,97 +0,0 @@
-/*++
-Copyright (c) 2007 Microsoft Corporation
-
-Module Name:
-
-    arith_simplifier_plugin.h
-
-Abstract:
-
-    Simplifier for the arithmetic family.
-
-Author:
-
-    Leonardo (leonardo) 2008-01-08
-    
---*/
-#ifndef ARITH_SIMPLIFIER_PLUGIN_H_
-#define ARITH_SIMPLIFIER_PLUGIN_H_
-
-#include"basic_simplifier_plugin.h"
-#include"poly_simplifier_plugin.h"
-#include"arith_decl_plugin.h"
-#include"arith_simplifier_params.h"
-
-/**
-   \brief Simplifier for the arith family.
-*/
-class arith_simplifier_plugin : public poly_simplifier_plugin {
-public:
-    enum op_kind {
-        LE, GE, EQ
-    };
-protected:
-    arith_simplifier_params & m_params;
-    arith_util                m_util;
-    basic_simplifier_plugin & m_bsimp;
-    expr_ref                  m_int_zero;
-    expr_ref                  m_real_zero;
-
-    bool is_neg_poly(expr * t) const;
-
-    template<op_kind k>
-    void mk_le_ge_eq_core(expr * arg1, expr * arg2, expr_ref & result);
-
-    void prop_mod_const(expr * e, unsigned depth, numeral const& k, expr_ref& result);
-
-    void gcd_reduce_monomial(expr_ref_vector& monomials, numeral& k);
-
-    void div_monomial(expr_ref_vector& monomials, numeral const& g);
-    void get_monomial_gcd(expr_ref_vector& monomials, numeral& g);
-    bool divides(expr* d, expr* n, expr_ref& quot);
-
-public:
-    arith_simplifier_plugin(ast_manager & m, basic_simplifier_plugin & b, arith_simplifier_params & p);
-    ~arith_simplifier_plugin();
-    arith_util & get_arith_util() { return m_util; }
-    virtual numeral norm(const numeral & n) { return n; }
-    virtual bool is_numeral(expr * n, rational & val) const { bool f; return m_util.is_numeral(n, val, f); }
-    bool is_numeral(expr * n) const { return m_util.is_numeral(n); }
-    virtual bool is_minus_one(expr * n) const { numeral tmp; return is_numeral(n, tmp) && tmp.is_minus_one(); }
-    virtual expr * get_zero(sort * s) const { return m_util.is_int(s) ? m_int_zero.get() : m_real_zero.get(); }
-
-    virtual app * mk_numeral(numeral const & n) { return m_util.mk_numeral(n, m_curr_sort->get_decl_kind() == INT_SORT); }
-    app * mk_numeral(numeral const & n, bool is_int) { return m_util.mk_numeral(n, is_int); }
-    bool is_int_sort(sort const * s) const { return m_util.is_int(s); }
-    bool is_real_sort(sort const * s) const { return m_util.is_real(s); }
-    bool is_arith_sort(sort const * s) const { return is_int_sort(s) || is_real_sort(s); }
-    bool is_int(expr const * n) const { return m_util.is_int(n); }
-    bool is_le(expr const * n) const { return m_util.is_le(n); }
-    bool is_ge(expr const * n) const { return m_util.is_ge(n); }
-
-    virtual bool is_le_ge(expr * n) const { return is_le(n) || is_ge(n); }
-    
-    void mk_le(expr * arg1, expr * arg2, expr_ref & result);
-    void mk_ge(expr * arg1, expr * arg2, expr_ref & result);
-    void mk_lt(expr * arg1, expr * arg2, expr_ref & result);
-    void mk_gt(expr * arg1, expr * arg2, expr_ref & result);
-    void mk_arith_eq(expr * arg1, expr * arg2, expr_ref & result);
-    void mk_div(expr * arg1, expr * arg2, expr_ref & result);
-    void mk_idiv(expr * arg1, expr * arg2, expr_ref & result);
-    void mk_mod(expr * arg1, expr * arg2, expr_ref & result);
-    void mk_rem(expr * arg1, expr * arg2, expr_ref & result);
-    void mk_to_real(expr * arg, expr_ref & result);
-    void mk_to_int(expr * arg, expr_ref & result);
-    void mk_is_int(expr * arg, expr_ref & result);
-    void mk_abs(expr * arg, expr_ref & result);
-
-    virtual bool reduce(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result);
-    virtual bool reduce_eq(expr * lhs, expr * rhs, expr_ref & result);
-
-    bool is_arith_term(expr * n) const;
-
-    void gcd_normalize(numeral & coeff, expr_ref& term);
-
-};
-
-#endif /* ARITH_SIMPLIFIER_PLUGIN_H_ */

src/shell/main.cpp

@@ -296,9 +296,6 @@ void parse_cmd_line_args(int argc, char ** argv) {
 
 int STD_CALL main(int argc, char ** argv) {
     try{
-        DEBUG_CODE( for (int i = 0; i < argc; i++)
-                        std::cout << argv[i] << " ";
-                    std::cout << std::endl;);
         unsigned return_value = 0;
         memory::initialize(0);
         memory::exit_when_out_of_memory(true, "ERROR: out of memory");

src/smt/smt_setup.cpp

@@ -979,7 +979,7 @@ namespace smt {
         if (st.num_theories() == 2 && st.has_uf() && is_arith(st)) {
             if (!st.m_has_real)
                 setup_QF_UFLIA(st);
-            else if (!st.m_has_int)
+            else if (!st.m_has_int && st.m_num_non_linear == 0) 
                 setup_QF_UFLRA();
             else
                 setup_unknown();