From f5c048775ba14493a2e206c4601c4528b08b2fb1 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 10 May 2015 09:42:11 -0700
Subject: [PATCH] add facility to solve QF_NRA + QF_UF(and other theories) in
 joint solver to allow broader use of QF_NRA core

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/tactic/arith/probe_arith.cpp          | 25 +++++++++++++++++++----
 src/tactic/nlsat_smt/nl_purify_tactic.cpp | 13 ++++++++++++
 2 files changed, 34 insertions(+), 4 deletions(-)

diff --git a/src/tactic/arith/probe_arith.cpp b/src/tactic/arith/probe_arith.cpp
index ae287e2b5..327b074b9 100644
--- a/src/tactic/arith/probe_arith.cpp
+++ b/src/tactic/arith/probe_arith.cpp
@@ -518,13 +518,19 @@ struct is_non_qfufnra_functor {
     struct found {};
     ast_manager & m;
     arith_util    u;
+    bool          m_has_nonlinear;
 
-    is_non_qfufnra_functor(ast_manager & _m): m(_m), u(m) {}
+    is_non_qfufnra_functor(ast_manager & _m): 
+        m(_m), u(m), m_has_nonlinear(false) {}
 
     void throw_found() {
         throw found();
     }
 
+    bool has_nonlinear() const {
+        return m_has_nonlinear;
+    }
+
     void operator()(var * x) {
         throw_found();
     }    
@@ -539,14 +545,25 @@ struct is_non_qfufnra_functor {
             switch (n->get_decl_kind()) {
             case OP_LE:  case OP_GE: case OP_LT: case OP_GT:
             case OP_ADD: case OP_UMINUS: case OP_SUB: case OP_ABS: 
-            case OP_NUM: case OP_MUL:
+            case OP_NUM: 
             case OP_IRRATIONAL_ALGEBRAIC_NUM:
                 return;
+            case OP_MUL:
+                if (n->get_num_args() == 2 ||
+                    (!u.is_numeral(n->get_arg(0)) &&
+                     !u.is_numeral(n->get_arg(1)))) {
+                    m_has_nonlinear = true;
+                }
+                return;
             case OP_IDIV: case OP_DIV: case OP_REM: case OP_MOD:
-            case OP_POWER:
                 if (!u.is_numeral(n->get_arg(1)))
                     throw_found();
                 return;
+            case OP_POWER: 
+                if (!u.is_numeral(n->get_arg(1)))
+                    throw_found();
+                m_has_nonlinear = true;
+                return;
             case OP_IS_INT:
             case OP_TO_INT:
             case OP_TO_REAL:
@@ -618,7 +635,7 @@ public:
 
 static bool is_qfufnra(goal const& g) {
     is_non_qfufnra_functor p(g.m());
-    return !test(g, p);    
+    return !test(g, p) && p.has_nonlinear();
 }
 
 class is_qfufnra_probe : public probe {
diff --git a/src/tactic/nlsat_smt/nl_purify_tactic.cpp b/src/tactic/nlsat_smt/nl_purify_tactic.cpp
index ef2e881dc..dd0a76f15 100644
--- a/src/tactic/nlsat_smt/nl_purify_tactic.cpp
+++ b/src/tactic/nlsat_smt/nl_purify_tactic.cpp
@@ -130,9 +130,22 @@ public:
             r = m.mk_fresh_const(0, u().mk_real());
             m_new_reals.push_back(to_app(r));
             m_interface_cache.insert(arg, r);
+            expr_ref eq(m);
+            eq = m.mk_eq(r, arg);
+            if (is_real_expression(arg)) {
+                m_nl_cnstrs.push_back(eq);
+                m_nl_cnstr_prs.push_back(m.mk_oeq(r, arg));
+            }
+            else {
+                m_owner.m_solver->assert_expr(eq);
+            }
             return r;
         }
 
+        bool is_real_expression(expr* e) {
+            return is_app(e) && (to_app(e)->get_family_id() == u().get_family_id());
+        }
+
         void mk_interface_bool(func_decl * f, unsigned num, expr* const* args, expr_ref& result) {
             expr_ref old_pred(m.mk_app(f, num, args), m);
             polarity_t pol;