Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable

src/ast/rewriter/arith_rewriter.h

@@ -118,7 +118,7 @@ public:
 
     void mk_eq(expr * arg1, expr * arg2, expr_ref & result) {
         if (mk_eq_core(arg1, arg2, result) == BR_FAILED)
-            result = m_util.mk_le(arg1, arg2);
+            result = m_util.mk_eq(arg1, arg2);
     }
     void mk_le(expr * arg1, expr * arg2, expr_ref & result) {
         if (mk_le_core(arg1, arg2, result) == BR_FAILED)

src/muz_qe/dl_mk_coi_filter.cpp

@@ -42,7 +42,7 @@ namespace datalog {
         scoped_ptr<rule_set> result1 = top_down(source);
         scoped_ptr<rule_set> result2 = bottom_up(result1?*result1:source);
         if (!result2) {
-            result2 = result1;
+            result2 = result1.detach();
         }
         return result2.detach();
     }

src/muz_qe/fixedpoint_params.pyg

@@ -49,7 +49,8 @@ def_module_params('fixedpoint',
                           ('use_multicore_generalizer', BOOL, False, "PDR: extract multiple cores for blocking states"),
                           ('use_inductive_generalizer', BOOL, True, "PDR: generalize lemmas using induction strengthening"),
                           ('use_arith_inductive_generalizer', BOOL, False, "PDR: generalize lemmas using arithmetic heuristics for induction strengthening"),
-	                  ('use_convex_hull_generalizer', BOOL, False, "PDR: generalize using convex hulls of lemmas"),
+	                  ('use_convex_closure_generalizer', BOOL, False, "PDR: generalize using convex closures of lemmas"),
+	                  ('use_convex_interior_generalizer', BOOL, False, "PDR: generalize using convex interiors of lemmas"),
                           ('cache_mode', UINT, 0, "PDR: use no (0), symbolic (1) or explicit cache (2) for model search"),
                           ('inductive_reachability_check', BOOL, False, "PDR: assume negation of the cube on the previous level when "
                                                                         "checking for reachability (not only during cube weakening)"),

src/muz_qe/pdr_context.cpp

@@ -1578,7 +1578,9 @@ namespace pdr {
             m_fparams.m_arith_auto_config_simplex = true;
             m_fparams.m_arith_propagate_eqs = false;
             m_fparams.m_arith_eager_eq_axioms = false;
-            if (m_params.use_utvpi() && !m_params.use_convex_hull_generalizer()) {
+            if (m_params.use_utvpi() && 
+                !m_params.use_convex_closure_generalizer() &&
+                !m_params.use_convex_interior_generalizer()) {
                 if (classify.is_dl()) {
                     m_fparams.m_arith_mode = AS_DIFF_LOGIC;
                     m_fparams.m_arith_expand_eqs = true;
@@ -1590,8 +1592,11 @@ namespace pdr {
                 }
             }
         }
-        if (m_params.use_convex_hull_generalizer()) {
-            m_core_generalizers.push_back(alloc(core_convex_hull_generalizer, *this));
+        if (m_params.use_convex_closure_generalizer()) {
+            m_core_generalizers.push_back(alloc(core_convex_hull_generalizer, *this, true));
+        }
+        if (m_params.use_convex_interior_generalizer()) {
+            m_core_generalizers.push_back(alloc(core_convex_hull_generalizer, *this, false));
         }
         if (!use_mc && m_params.use_inductive_generalizer()) {
             m_core_generalizers.push_back(alloc(core_bool_inductive_generalizer, *this, 0));

src/muz_qe/pdr_generalizers.cpp

@@ -147,18 +147,23 @@ namespace pdr {
     }
 
 
-    core_convex_hull_generalizer::core_convex_hull_generalizer(context& ctx):
+    core_convex_hull_generalizer::core_convex_hull_generalizer(context& ctx, bool is_closure):
         core_generalizer(ctx),
         m(ctx.get_manager()),
         a(m),
         m_sigma(m),
-        m_trail(m) {
+        m_trail(m),
+        m_is_closure(is_closure) {
         m_sigma.push_back(m.mk_fresh_const("sigma", a.mk_real()));
         m_sigma.push_back(m.mk_fresh_const("sigma", a.mk_real()));
     }
 
+    void core_convex_hull_generalizer::operator()(model_node& n, expr_ref_vector const& core, bool uses_level, cores& new_cores) {
+        method1(n, core, uses_level, new_cores);
+    }
+
     void core_convex_hull_generalizer::operator()(model_node& n, expr_ref_vector& core, bool& uses_level) {
-        method1(n, core, uses_level);
+        UNREACHABLE();
     }
 
     // use the entire region as starting point for generalization.
@@ -174,20 +179,29 @@ namespace pdr {
     // If Constraints & Transition(y0, y) is unsat, then 
     // update with new core.
     // 
-    void core_convex_hull_generalizer::method1(model_node& n, expr_ref_vector& core, bool& uses_level) {    
+    void core_convex_hull_generalizer::method1(model_node& n, expr_ref_vector const& core, bool uses_level, cores& new_cores) {    
         manager& pm = n.pt().get_pdr_manager();
         expr_ref_vector conv1(m), conv2(m), core1(m), core2(m), eqs(m);
+        unsigned orig_size = new_cores.size();
         if (core.empty()) {
+            new_cores.push_back(std::make_pair(core, uses_level));
             return;
         }        
         add_variables(n, eqs);
         if (!mk_convex(core, 0, conv1)) {
+            new_cores.push_back(std::make_pair(core, uses_level));
             IF_VERBOSE(0, verbose_stream() << "Non-convex: " << mk_pp(pm.mk_and(core), m) << "\n";);
             return;
         }
         conv1.append(eqs);
-        conv1.push_back(a.mk_gt(m_sigma[0].get(), a.mk_numeral(rational(0), a.mk_real())));
-        conv1.push_back(a.mk_gt(m_sigma[1].get(), a.mk_numeral(rational(0), a.mk_real())));
+        if (m_is_closure) {
+            conv1.push_back(a.mk_gt(m_sigma[0].get(), a.mk_numeral(rational(0), a.mk_real())));
+            conv1.push_back(a.mk_gt(m_sigma[1].get(), a.mk_numeral(rational(0), a.mk_real())));
+        }
+        else {
+            conv1.push_back(a.mk_ge(m_sigma[0].get(), a.mk_numeral(rational(0), a.mk_real())));
+            conv1.push_back(a.mk_ge(m_sigma[1].get(), a.mk_numeral(rational(0), a.mk_real())));
+        }
         conv1.push_back(m.mk_eq(a.mk_numeral(rational(1), a.mk_real()), a.mk_add(m_sigma[0].get(), m_sigma[1].get())));
         expr_ref fml = n.pt().get_formulas(n.level(), false);
         expr_ref_vector fmls(m);
@@ -202,24 +216,29 @@ namespace pdr {
             }
             conv2.append(conv1);
             expr_ref state = pm.mk_and(conv2);
-            TRACE("pdr", tout << "Check:\n" << mk_pp(state, m) << "\n";
-                  tout << "New formula:\n" << mk_pp(pm.mk_and(core), m) << "\n";
-                  tout << "Old formula:\n" << mk_pp(fml, m) << "\n";
-
+            TRACE("pdr", 
+                  tout << "Check states:\n" << mk_pp(state, m) << "\n";
+                  tout << "Old states:\n"   << mk_pp(fml, m) << "\n";
                   );
             model_node nd(0, state, n.pt(), n.level());
             pred_transformer::scoped_farkas sf(n.pt(), true);
-            if (l_false == n.pt().is_reachable(nd, &conv2, uses_level)) {
+            bool uses_level1 = uses_level;
+            if (l_false == n.pt().is_reachable(nd, &conv2, uses_level1)) {
+                new_cores.push_back(std::make_pair(conv2, uses_level1));
+
+                expr_ref state1 = pm.mk_and(conv2);
                 TRACE("pdr", 
                       tout << mk_pp(state, m) << "\n";
-                      tout << "Generalized to:\n" << mk_pp(pm.mk_and(conv2), m) << "\n";);
+                      tout << "Generalized to:\n" << mk_pp(state1, m) << "\n";);
                 IF_VERBOSE(0,
                            verbose_stream() << mk_pp(state, m) << "\n";
-                           verbose_stream() << "Generalized to:\n" << mk_pp(pm.mk_and(conv2), m) << "\n";);
-                core.reset();
-                core.append(conv2);
+                           verbose_stream() << "Generalized to:\n" << mk_pp(state1, m) << "\n";);
             }            
         }
+        if (!m_is_closure || new_cores.empty()) {
+            new_cores.push_back(std::make_pair(core, uses_level));
+        }
+
     }
 
     // take as starting point two points from different regions.
@@ -317,12 +336,47 @@ namespace pdr {
         }
     }
 
+    expr_ref core_convex_hull_generalizer::mk_closure(expr* e) {
+        expr* e0, *e1, *e2;
+        expr_ref result(m);
+        if (a.is_lt(e, e1, e2)) {
+            result = a.mk_le(e1, e2);
+        }
+        else if (a.is_gt(e, e1, e2)) {
+            result = a.mk_ge(e1, e2);
+        }
+        else if (m.is_not(e, e0) && a.is_ge(e0, e1, e2)) {
+            result = a.mk_le(e1, e2);
+        }
+        else if (m.is_not(e, e0) && a.is_le(e0, e1, e2)) {
+            result = a.mk_ge(e1, e2);
+        }
+        else if (a.is_ge(e) || a.is_le(e) || m.is_eq(e) ||
+                 (m.is_not(e, e0) && (a.is_gt(e0) || a.is_lt(e0)))) {
+            result = e;
+        }
+        else {
+            IF_VERBOSE(1, verbose_stream() << "Cannot close: " << mk_pp(e, m) << "\n";);
+        }
+        return result;
+    }
+
+    bool core_convex_hull_generalizer::mk_closure(expr_ref_vector& conj) {
+        for (unsigned i = 0; i < conj.size(); ++i) {
+            conj[i] = mk_closure(conj[i].get());
+            if (!conj[i].get()) {
+                return false;
+            }
+        }
+        return true;
+    }
+
     bool core_convex_hull_generalizer::mk_convex(expr_ref_vector const& core, unsigned index, expr_ref_vector& conv) {
         conv.reset();
         for (unsigned i = 0; i < core.size(); ++i) {
             mk_convex(core[i], index, conv);
         }
-        return !conv.empty();
+        return !conv.empty() && mk_closure(conv);
     }
 
     void core_convex_hull_generalizer::mk_convex(expr* fml, unsigned index, expr_ref_vector& conv) {

src/muz_qe/pdr_generalizers.h

@@ -81,16 +81,20 @@ namespace pdr {
         obj_map<func_decl, expr*> m_left;
         obj_map<func_decl, expr*> m_right;
         obj_map<expr, expr*> m_models;
+        bool m_is_closure;
+        expr_ref mk_closure(expr* e);
+        bool mk_closure(expr_ref_vector& conj);
         bool mk_convex(expr_ref_vector const& core, unsigned index, expr_ref_vector& conv);
         void mk_convex(expr* fml, unsigned index, expr_ref_vector& conv);
         bool mk_convex(expr* term, unsigned index, bool is_mul, expr_ref& result);
         bool translate(func_decl* fn, unsigned index, expr_ref& result);
-        void method1(model_node& n, expr_ref_vector& core, bool& uses_level);
+        void method1(model_node& n, expr_ref_vector const& core, bool uses_level, cores& new_cores);
         void method2(model_node& n, expr_ref_vector& core, bool& uses_level);
         void add_variables(model_node& n, expr_ref_vector& eqs);
     public:
-        core_convex_hull_generalizer(context& ctx);
+        core_convex_hull_generalizer(context& ctx, bool is_closure);
         virtual ~core_convex_hull_generalizer() {}
+        virtual void operator()(model_node& n, expr_ref_vector const& core, bool uses_level, cores& new_cores);
         virtual void operator()(model_node& n, expr_ref_vector& core, bool& uses_level);
     };	
 

src/muz_qe/pdr_util.cpp

@@ -42,6 +42,10 @@ Notes:
 #include "arith_decl_plugin.h"
 #include "expr_replacer.h"
 #include "model_smt2_pp.h"
+#include "poly_rewriter.h"
+#include "poly_rewriter_def.h"
+#include "arith_rewriter.h"
+
 
 
 namespace pdr {
@@ -1278,9 +1282,154 @@ namespace pdr {
         return test.is_dl();
     }  
 
+    class arith_normalizer : public poly_rewriter<arith_rewriter_core> {
+        ast_manager& m;
+        arith_util   m_util;
+        enum op_kind { LE, GE, EQ };
+    public:
+        arith_normalizer(ast_manager& m, params_ref const& p = params_ref()): poly_rewriter<arith_rewriter_core>(m, p), m(m), m_util(m) {}
+        
+        br_status mk_app_core(func_decl* f, unsigned num_args, expr* const* args, expr_ref& result) {
+            br_status st = BR_FAILED;
+            if (m.is_eq(f)) {
+                SASSERT(num_args == 2); return mk_eq_core(args[0], args[1], result);
+            }
+
+            if (f->get_family_id() != get_fid()) {
+                return st;
+            }
+            switch (f->get_decl_kind()) {
+            case OP_NUM: st = BR_FAILED; break;
+            case OP_IRRATIONAL_ALGEBRAIC_NUM: st = BR_FAILED; break;
+            case OP_LE:  SASSERT(num_args == 2); st = mk_le_core(args[0], args[1], result); break;
+            case OP_GE:  SASSERT(num_args == 2); st = mk_ge_core(args[0], args[1], result); break;
+            case OP_LT:  SASSERT(num_args == 2); st = mk_lt_core(args[0], args[1], result); break;
+            case OP_GT:  SASSERT(num_args == 2); st = mk_gt_core(args[0], args[1], result); break;
+            default: st = BR_FAILED; break;
+            }
+            return st;
+        }      
+
+    private:
+        
+        br_status mk_eq_core(expr* arg1, expr* arg2, expr_ref& result) {
+            return mk_le_ge_eq_core(arg1, arg2, EQ, result);
+        }
+        br_status mk_le_core(expr* arg1, expr* arg2, expr_ref& result) {
+            return mk_le_ge_eq_core(arg1, arg2, LE, result);
+        }
+        br_status mk_ge_core(expr* arg1, expr* arg2, expr_ref& result) {
+            return mk_le_ge_eq_core(arg1, arg2, GE, result);
+        }
+        br_status mk_lt_core(expr* arg1, expr* arg2, expr_ref& result) {
+            result = m.mk_not(m_util.mk_ge(arg1, arg2));
+            return BR_REWRITE2;
+        }
+        br_status mk_gt_core(expr* arg1, expr* arg2, expr_ref& result) {
+            result = m.mk_not(m_util.mk_le(arg1, arg2));
+            return BR_REWRITE2;
+        }
+
+        br_status mk_le_ge_eq_core(expr* arg1, expr* arg2, op_kind kind, expr_ref& result) {
+            if (m_util.is_real(arg1)) {
+                numeral g(0);
+                get_coeffs(arg1, g);
+                get_coeffs(arg2, g);
+                if (!g.is_one() && !g.is_zero()) {
+                    SASSERT(g.is_pos());
+                    expr_ref new_arg1 = rdiv_polynomial(arg1, g);
+                    expr_ref new_arg2 = rdiv_polynomial(arg2, g);
+                    switch(kind) {
+                    case LE: result = m_util.mk_le(new_arg1, new_arg2); return BR_DONE;
+                    case GE: result = m_util.mk_ge(new_arg1, new_arg2); return BR_DONE;
+                    case EQ: result = m_util.mk_eq(new_arg1, new_arg2); return BR_DONE;
+                    }
+                }
+            }
+            return BR_FAILED;
+        }
+
+        void update_coeff(numeral const& r, numeral& g) {
+            if (g.is_zero() || abs(r) < g) {
+                g = abs(r);
+            }
+        }        
+
+        void get_coeffs(expr* e, numeral& g) {
+            rational r;
+            unsigned sz;
+            expr* const* args = get_monomials(e, sz);
+            for (unsigned i = 0; i < sz; ++i) {
+                expr* arg = args[i];
+                if (!m_util.is_numeral(arg, r)) {
+                    get_power_product(arg, r);
+                }
+                update_coeff(r, g);
+            }
+        }
+
+        expr_ref rdiv_polynomial(expr* e, numeral const& g) {
+            rational r;
+            SASSERT(g.is_pos());
+            SASSERT(!g.is_one());
+            expr_ref_vector monomes(m);
+            unsigned sz;           
+            expr* const* args = get_monomials(e, sz);
+            for (unsigned i = 0; i < sz; ++i) {
+                expr* arg = args[i];
+                if (m_util.is_numeral(arg, r)) {
+                    monomes.push_back(m_util.mk_numeral(r/g, false));
+                }
+                else {
+                    expr* p = get_power_product(arg, r);
+                    r /= g;
+                    if (r.is_one()) {
+                        monomes.push_back(p);
+                    }
+                    else {
+                        monomes.push_back(m_util.mk_mul(m_util.mk_numeral(r, false), p));
+                    }
+                }
+            }
+            expr_ref result(m);
+            mk_add(monomes.size(), monomes.c_ptr(), result);
+            return result;
+        }
+                
+    };
+    
+
+    struct arith_normalizer_cfg: public default_rewriter_cfg {
+        arith_normalizer m_r;
+        bool rewrite_patterns() const { return false; }
+        br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) {
+            return m_r.mk_app_core(f, num, args, result);
+        }
+        arith_normalizer_cfg(ast_manager & m, params_ref const & p):m_r(m,p) {}        
+    };
+
+    class arith_normalizer_star : public rewriter_tpl<arith_normalizer_cfg> {
+        arith_normalizer_cfg m_cfg;
+    public:
+        arith_normalizer_star(ast_manager & m, params_ref const & p):
+            rewriter_tpl<arith_normalizer_cfg>(m, false, m_cfg),
+            m_cfg(m, p) {}
+    };
+
+
+    void normalize_arithmetic(expr_ref& t) {
+        ast_manager& m = t.get_manager();
+        datalog::scoped_no_proof _sp(m);
+        params_ref p;
+        arith_normalizer_star rw(m, p);
+        expr_ref tmp(m);
+        rw(t, tmp);
+        t = tmp;                
+    }
+
 }
 
 template class rewriter_tpl<pdr::ite_hoister_cfg>;
-
+template class rewriter_tpl<pdr::arith_normalizer_cfg>;
 
 

src/muz_qe/pdr_util.h

@@ -142,6 +142,7 @@ namespace pdr {
        Assumption: the model satisfies the conjunctions.       
      */
     void reduce_disequalities(model& model, unsigned threshold, expr_ref& fml);
+
     
 
     /**
@@ -149,6 +150,16 @@ namespace pdr {
      */
     void hoist_non_bool_if(expr_ref& fml);
 
+
+    /**
+       \brief normalize coefficients in polynomials so that least coefficient is 1.
+     */
+    void normalize_arithmetic(expr_ref& t);
+
+
+    /**
+       \brief determine if formulas belong to difference logic or UTVPI fragment.
+     */
     bool is_difference_logic(ast_manager& m, unsigned num_fmls, expr* const* fmls);
 
     bool is_utvpi_logic(ast_manager& m, unsigned num_fmls, expr* const* fmls);

src/test/arith_rewriter.cpp

@@ -2,6 +2,33 @@
 #include "bv_decl_plugin.h"
 #include "ast_pp.h"
 #include "reg_decl_plugins.h"
+#include "th_rewriter.h"
+#include "model.h"
+#include "pdr_util.h"
+#include "smt2parser.h"
+
+
+static expr_ref parse_fml(ast_manager& m, char const* str) {
+    expr_ref result(m);
+    cmd_context ctx(false, &m);
+    ctx.set_ignore_check(true);
+    std::ostringstream buffer;
+    buffer << "(declare-const x Real)\n"
+           << "(declare-const y Real)\n"
+           << "(declare-const z Real)\n"
+           << "(declare-const a Real)\n"
+           << "(declare-const b Real)\n"
+           << "(assert " << str << ")\n";
+    std::istringstream is(buffer.str());
+    VERIFY(parse_smt2_commands(ctx, is));
+    SASSERT(ctx.begin_assertions() != ctx.end_assertions());
+    result = *ctx.begin_assertions();
+    return result;
+}
+
+static char const* example1 = "(<= (+ (* 1.3 x y) (* 2.3 y y) (* (- 1.1 x x))) 2.2)";
+static char const* example2 = "(= (+ 4 3 (- (* 3 x x) (* 5 y)) y) 0)";
+
 
 void tst_arith_rewriter() {
     ast_manager m;
@@ -14,4 +41,19 @@ void tst_arith_rewriter() {
     expr* args[2] = { t1, t2 };
     ar.mk_mul(2, args, result);
     std::cout << mk_pp(result, m) << "\n";
+
+    
+    th_rewriter rw(m);
+    expr_ref fml = parse_fml(m, example1);
+    rw(fml);
+    std::cout << mk_pp(fml, m) << "\n";
+    pdr::normalize_arithmetic(fml);
+    std::cout << mk_pp(fml, m) << "\n";
+
+
+    fml = parse_fml(m, example2);
+    rw(fml);
+    std::cout << mk_pp(fml, m) << "\n";
+    pdr::normalize_arithmetic(fml);
+    std::cout << mk_pp(fml, m) << "\n";
 }

src/test/polynorm.cpp

@@ -109,10 +109,12 @@ void tst_polynorm() {
     reg_decl_plugins(m);
     expr_ref fml(m);
 
-    fml = parse_fml(m, example2);
-
+    fml = parse_fml(m, example1);
     std::cout << mk_pp(fml, m) << "\n";
+    nf(fml);
 
+    fml = parse_fml(m, example2);
+    std::cout << mk_pp(fml, m) << "\n";
     nf(fml);