add case for abs (normally simplified, but not with default_tactic=smt).

src/ast/arith_decl_plugin.h

@@ -302,6 +302,7 @@ public:
     bool is_is_int(expr const * n) const { return is_app_of(n, arith_family_id, OP_IS_INT); }
     bool is_power(expr const * n) const { return is_app_of(n, arith_family_id, OP_POWER); }
     bool is_power0(expr const * n) const { return is_app_of(n, arith_family_id, OP_POWER0); }
+    bool is_abs(expr const* n) const { return is_app_of(n, arith_family_id, OP_ABS); }
 
     bool is_int(sort const * s) const { return is_sort_of(s, arith_family_id, INT_SORT); }
     bool is_int(expr const * n) const { return is_int(n->get_sort()); }
@@ -341,6 +342,7 @@ public:
     MATCH_UNARY(is_to_real);
     MATCH_UNARY(is_to_int);
     MATCH_UNARY(is_is_int);
+    MATCH_UNARY(is_abs);
     MATCH_BINARY(is_sub);
     MATCH_BINARY(is_add);
     MATCH_BINARY(is_mul);

src/sat/smt/arith_axioms.cpp

@@ -49,6 +49,14 @@ namespace arith {
         }
     }
 
+    void solver::mk_abs_axiom(app* n) {
+        expr* x = nullptr;
+        VERIFY(a.is_abs(n, x));
+        literal is_nonneg = mk_literal(a.mk_ge(x, a.mk_numeral(rational::zero(), n->get_sort())));
+        add_clause(~is_nonneg, eq_internalize(n, x));
+        add_clause(is_nonneg, eq_internalize(n, a.mk_uminus(x)));
+    }
+
     // t = n^0
     void solver::mk_power0_axioms(app* t, app* n) {
         expr_ref p0(a.mk_power0(n, t->get_arg(1)), m);

src/sat/smt/arith_internalize.cpp

@@ -237,9 +237,10 @@ namespace arith {
                 if (!is_first) {
                     // skip recursive internalization
                 }
-                else if (a.is_to_int(n, n1)) {
+                else if (a.is_to_int(n, n1)) 
                     mk_to_int_axiom(t);                
-                }
+                else if (a.is_abs(n)) 
+                    mk_abs_axiom(t);                
                 else if (a.is_idiv(n, n1, n2)) {
                     if (!a.is_numeral(n2, r) || r.is_zero()) found_underspecified(n);
                     m_idiv_terms.push_back(n);

src/sat/smt/arith_solver.h

@@ -263,6 +263,7 @@ namespace arith {
         // axioms
         void mk_div_axiom(expr* p, expr* q);
         void mk_to_int_axiom(app* n);
+        void mk_abs_axiom(app* n);
         void mk_is_int_axiom(expr* n);
         void mk_idiv_mod_axioms(expr* p, expr* q);
         void mk_rem_axiom(expr* dividend, expr* divisor);