Merge branch 'master' of https://github.com/Z3Prover/z3

src/ast/arith_decl_plugin.h

@@ -290,6 +290,8 @@ public:
     bool is_asin(expr const* n) const { return is_app_of(n, m_afid, OP_ASIN); }
     bool is_acos(expr const* n) const { return is_app_of(n, m_afid, OP_ACOS); }
     bool is_atan(expr const* n) const { return is_app_of(n, m_afid, OP_ATAN); }
+    bool is_pi(expr * arg) { return is_app_of(arg, m_afid, OP_PI); }
+    bool is_e(expr * arg) { return is_app_of(arg, m_afid, OP_E); }
 
     MATCH_UNARY(is_uminus);
     MATCH_UNARY(is_to_real);
@@ -307,8 +309,13 @@ public:
     MATCH_BINARY(is_idiv);
     MATCH_BINARY(is_power);
 
-    bool is_pi(expr * arg) { return is_app_of(arg, m_afid, OP_PI); }
+    MATCH_UNARY(is_sin);
-    bool is_e(expr * arg) { return is_app_of(arg, m_afid, OP_E); }
+    MATCH_UNARY(is_asin);
+    MATCH_UNARY(is_cos);
+    MATCH_UNARY(is_acos);
+    MATCH_UNARY(is_tan);
+    MATCH_UNARY(is_atan);
+
 };
 
 class arith_util : public arith_recognizers {
@@ -355,6 +362,9 @@ public:
     app * mk_int(int i) {
         return mk_numeral(rational(i), true);
     }
+    app * mk_real(int i) {
+        return mk_numeral(rational(i), false);
+    }
     app * mk_le(expr * arg1, expr * arg2) const { return m_manager.mk_app(m_afid, OP_LE, arg1, arg2); }
     app * mk_ge(expr * arg1, expr * arg2) const { return m_manager.mk_app(m_afid, OP_GE, arg1, arg2); }
     app * mk_lt(expr * arg1, expr * arg2) const { return m_manager.mk_app(m_afid, OP_LT, arg1, arg2); }

src/ast/fpa/fpa2bv_converter.cpp

@@ -3641,11 +3641,11 @@ void fpa2bv_converter::unpack(expr * e, expr_ref & sgn, expr_ref & sig, expr_ref
             // the maximum shift is `sbits', because after that the mantissa
             // would be zero anyways. So we can safely cut the shift variable down,
             // as long as we check the higher bits.
-            expr_ref sh(m), is_sh_zero(m), sl(m), sbits_s(m), short_shift(m);
+            expr_ref zero_ems(m), sh(m), is_sh_zero(m), sl(m), sbits_s(m), short_shift(m);
-            zero_s = m_bv_util.mk_numeral(0, sbits-1);
+            zero_ems = m_bv_util.mk_numeral(0, ebits - sbits);
             sbits_s = m_bv_util.mk_numeral(sbits, sbits);
             sh = m_bv_util.mk_extract(ebits-1, sbits, shift);
-            m_simp.mk_eq(zero_s, sh, is_sh_zero);
+            m_simp.mk_eq(zero_ems, sh, is_sh_zero);
             short_shift = m_bv_util.mk_extract(sbits-1, 0, shift);
             m_simp.mk_ite(is_sh_zero, short_shift, sbits_s, sl);
             denormal_sig = m_bv_util.mk_bv_shl(denormal_sig, sl);

src/ast/rewriter/arith_rewriter.cpp

@@ -1196,11 +1196,17 @@ expr * arith_rewriter::mk_sin_value(rational const & k) {
 }
 
 br_status arith_rewriter::mk_sin_core(expr * arg, expr_ref & result) {
-    if (is_app_of(arg, get_fid(), OP_ASIN)) {
+    expr * m, *x;
+    if (m_util.is_asin(arg, x)) {
         // sin(asin(x)) == x
-        result = to_app(arg)->get_arg(0);
+        result = x;
         return BR_DONE;
     }
+    if (m_util.is_acos(arg, x)) {
+        // sin(acos(x)) == sqrt(1 - x^2)
+        result = m_util.mk_power(m_util.mk_sub(m_util.mk_real(1), m_util.mk_mul(x,x)), m_util.mk_numeral(rational(1,2), false));
+        return BR_REWRITE_FULL;
+    }
     rational k;
     if (is_numeral(arg, k) && k.is_zero()) {
         // sin(0) == 0
@@ -1214,7 +1220,6 @@ br_status arith_rewriter::mk_sin_core(expr * arg, expr_ref & result) {
             return BR_REWRITE_FULL;
     }
 
-    expr * m;
     if (is_pi_offset(arg, k, m)) {
         rational k_prime = mod(floor(k), rational(2)) + k - floor(k);
         SASSERT(k_prime >= rational(0) && k_prime < rational(2));
@@ -1250,11 +1255,15 @@ br_status arith_rewriter::mk_sin_core(expr * arg, expr_ref & result) {
 }
 
 br_status arith_rewriter::mk_cos_core(expr * arg, expr_ref & result) {
-    if (is_app_of(arg, get_fid(), OP_ACOS)) {
+    expr* x;
+    if (m_util.is_acos(arg, x)) {
         // cos(acos(x)) == x
-        result = to_app(arg)->get_arg(0);
+        result = x;
         return BR_DONE;
     }
+    if (m_util.is_asin(arg, x)) {
+        // cos(asin(x)) == ...
+    }
 
     rational k;
     if (is_numeral(arg, k) && k.is_zero()) {

src/smt/smt_quantifier.cpp

@@ -147,6 +147,7 @@ namespace smt {
             }
             m_qi_queue.init_search_eh();
             m_plugin->init_search_eh();
+            TRACE("smt_params", m_params.display(tout); );
         }
         
         void assign_eh(quantifier * q) {

src/tactic/arith/purify_arith_tactic.cpp

@@ -170,8 +170,8 @@ struct purify_arith_proc {
         }
         std::pair<expr*, expr*> pair;
         if (!m_sin_cos.find(to_app(theta), pair)) {
-            pair.first = m().mk_fresh_const(0, m_util.mk_real());
+            pair.first = m().mk_fresh_const(0, u().mk_real());
-            pair.second = m().mk_fresh_const(0, m_util.mk_real());            
+            pair.second = m().mk_fresh_const(0, u().mk_real());            
             m_sin_cos.insert(to_app(theta), pair);
             m_pinned.push_back(pair.first);
             m_pinned.push_back(pair.second);
@@ -681,6 +681,8 @@ struct purify_arith_proc {
         }
     };
 
+    expr * mk_real_zero() { return u().mk_numeral(rational(0), false); }
+
     struct rw : public rewriter_tpl<rw_cfg> {
         rw_cfg m_cfg;
         rw(purify_arith_proc & o):
@@ -781,13 +783,15 @@ struct purify_arith_proc {
             mc = concat(mc.get(), emc);
             obj_map<app, std::pair<expr*,expr*> >::iterator it = m_sin_cos.begin(), end = m_sin_cos.end();
             for (; it != end; ++it) {
-                emc->insert(it->m_key->get_decl(), m_util.mk_asin(it->m_value.first));
+                emc->insert(it->m_key->get_decl(), 
+                            m().mk_ite(u().mk_ge(it->m_value.first, mk_real_zero()), u().mk_acos(it->m_value.second), 
+                                       u().mk_add(u().mk_acos(u().mk_uminus(it->m_value.second)), u().mk_pi())));
             }
 
         }
-        // given values for x, y find value for theta
-        // x, y are rational
     }
+
+
 };
 
 class purify_arith_tactic : public tactic {

src/tactic/ufbv/ufbv_tactic.cpp

@@ -40,12 +40,12 @@ tactic * mk_ufbv_preprocessor_tactic(ast_manager & m, params_ref const & p) {
     no_elim_and.set_bool("elim_and", false);
 
     return and_then(
-		mk_trace_tactic("ufbv_pre"),
+        mk_trace_tactic("ufbv_pre"),
                 and_then(mk_simplify_tactic(m, p),
                          mk_propagate_values_tactic(m, p),
                          and_then(using_params(mk_macro_finder_tactic(m, no_elim_and), no_elim_and), 
-				  mk_simplify_tactic(m, p)),
+                  mk_simplify_tactic(m, p)),
-                         and_then(mk_snf_tactic(m, p), mk_simplify_tactic(m, p)),			 
+                         and_then(mk_snf_tactic(m, p), mk_simplify_tactic(m, p)),             
                          mk_elim_and_tactic(m, p),
                          mk_solve_eqs_tactic(m, p),
                          and_then(mk_der_fp_tactic(m, p), mk_simplify_tactic(m, p)),
@@ -56,7 +56,7 @@ tactic * mk_ufbv_preprocessor_tactic(ast_manager & m, params_ref const & p) {
                          and_then(mk_quasi_macros_tactic(m, p), mk_simplify_tactic(m, p)),
                          and_then(mk_der_fp_tactic(m, p), mk_simplify_tactic(m, p)),
                          mk_simplify_tactic(m, p)),
-		mk_trace_tactic("ufbv_post"));
+        mk_trace_tactic("ufbv_post"));
 }
 
 tactic * mk_ufbv_tactic(ast_manager & m, params_ref const & p) {