fix regressions in nl/smt

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

scripts/mk_util.py

@@ -85,6 +85,7 @@ VS_PAR=False
 VS_PAR_NUM=8
 GPROF=False
 GIT_HASH=False
+OPTIMIZE=False
 
 FPMATH="Default"
 FPMATH_FLAGS="-mfpmath=sse -msse -msse2"
@@ -551,6 +552,8 @@ def display_help(exit_code):
         print("  -v, --vsproj                  generate Visual Studio Project Files.")
     if IS_WINDOWS:
         print("  -n, --nodotnet                do not generate Microsoft.Z3.dll make rules.")
+    if IS_WINDOWS:
+	print("  --optimize                    generate optimized code during linking.")
     print("  -j, --java                    generate Java bindings.")
     print("  --ml                          generate OCaml bindings.")
     print("  --staticlib                   build Z3 static library.")    
@@ -577,13 +580,13 @@ def display_help(exit_code):
 def parse_options():
     global VERBOSE, DEBUG_MODE, IS_WINDOWS, VS_X64, ONLY_MAKEFILES, SHOW_CPPS, VS_PROJ, TRACE, VS_PAR, VS_PAR_NUM
     global DOTNET_ENABLED, JAVA_ENABLED, ML_ENABLED, STATIC_LIB, PREFIX, GMP, FOCI2, FOCI2LIB, PYTHON_PACKAGE_DIR, GPROF, GIT_HASH
-    global LINUX_X64
+    global LINUX_X64, OPTIMIZE
     try:
         options, remainder = getopt.gnu_getopt(sys.argv[1:],
                                                'b:df:sxhmcvtnp:gj',
                                                ['build=', 'debug', 'silent', 'x64', 'help', 'makefiles', 'showcpp', 'vsproj',
                                                 'trace', 'nodotnet', 'staticlib', 'prefix=', 'gmp', 'foci2=', 'java', 'parallel=', 'gprof',
-                                                'githash=', 'x86', 'ml'])
+                                                'githash=', 'x86', 'ml', 'optimize'])
     except:
         print("ERROR: Invalid command line option")
         display_help(1)
@@ -618,6 +621,8 @@ def parse_options():
             DOTNET_ENABLED = False
         elif opt in ('--staticlib'):
             STATIC_LIB = True
+	elif opt in ('--optimize'):
+	    OPTIMIZE = True
         elif not IS_WINDOWS and opt in ('-p', '--prefix'):
             PREFIX = arg
             PYTHON_PACKAGE_DIR = os.path.join(PREFIX, 'lib', 'python%s' % distutils.sysconfig.get_python_version(), 'dist-packages')
@@ -1781,8 +1786,9 @@ def mk_config():
                     'SLINK_EXTRA_FLAGS=/link /DEBUG /MACHINE:X64 /SUBSYSTEM:WINDOWS /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE:NO\n')
         else:
             # Windows Release mode
+	    if OPTIMIZE:
+		config.write('AR_FLAGS=/nologo /LTCG\n')                
             config.write(
-                'AR_FLAGS=/nologo /LTCG\n'
                 'LINK_FLAGS=/nologo /MD\n'
                 'SLINK_FLAGS=/nologo /LD\n')
             if TRACE:

src/smt/theory_arith.h

@@ -882,10 +882,10 @@ namespace smt {
         template<bool invert>
         void add_tmp_row_entry(row & r, numeral const & coeff, theory_var v);
         enum max_min_t { UNBOUNDED, AT_BOUND, OPTIMIZED, BEST_EFFORT};
-        max_min_t max_min(theory_var v, bool max, bool& has_shared);
+        max_min_t max_min(theory_var v, bool max, bool maintain_integrality, bool& has_shared);
         bool max_min(svector<theory_var> const & vars);
 
-        max_min_t max_min(row& r, bool max, bool& has_shared);
+        max_min_t max_min(row& r, bool max, bool maintain_integrality, bool& has_shared);
         bool unbounded_gain(inf_numeral const & max_gain) const;
         bool safe_gain(inf_numeral const& min_gain, inf_numeral const & max_gain) const;
         void normalize_gain(numeral const& divisor, inf_numeral & max_gain) const;

src/smt/theory_arith_aux.h

@@ -1133,7 +1133,7 @@ namespace smt {
     inf_eps_rational<inf_rational> theory_arith<Ext>::maximize(theory_var v, expr_ref& blocker, bool& has_shared) {
         TRACE("bound_bug", display_var(tout, v); display(tout););
         has_shared = false;
-        max_min_t r = max_min(v, true, has_shared); 
+        max_min_t r = max_min(v, true, true, has_shared); 
         if (r == UNBOUNDED) {
             has_shared = false;
             blocker = get_manager().mk_false();
@@ -1553,13 +1553,14 @@ namespace smt {
     typename theory_arith<Ext>::max_min_t theory_arith<Ext>::max_min(
         row & r, 
         bool max, 
+        bool maintain_integrality, 
         bool& has_shared) {
         m_stats.m_max_min++;
         unsigned best_efforts = 0;
         bool inc = false;
         context& ctx = get_context();
 
-        SASSERT(valid_assignment());
+        SASSERT(!maintain_integrality || valid_assignment());
 
         numeral a_ij, curr_a_ij, coeff, curr_coeff;
         inf_numeral min_gain, max_gain, curr_min_gain, curr_max_gain;
@@ -1633,7 +1634,7 @@ namespace smt {
             
             if (x_j == null_theory_var) {
                 TRACE("opt", tout << "row is " << (max ? "maximized" : "minimized") << "\n";);
-                SASSERT(valid_assignment());
+                SASSERT(!maintain_integrality || valid_assignment());
                 result = OPTIMIZED;
                 break; 
             }
@@ -1648,7 +1649,7 @@ namespace smt {
                     SASSERT(!unbounded_gain(max_gain));
                     update_value(x_j, max_gain);
                     TRACE("opt", tout << "moved v" << x_j << " to upper bound\n";);
-                    SASSERT(valid_assignment());
+                    SASSERT(!maintain_integrality || valid_assignment());
                     continue;
                 }
                 if (!inc && lower(x_j)) {
@@ -1656,7 +1657,7 @@ namespace smt {
                     max_gain.neg();
                     update_value(x_j, max_gain);
                     TRACE("opt", tout << "moved v" << x_j << " to lower bound\n";);
-                    SASSERT(valid_assignment());
+                    SASSERT(!maintain_integrality || valid_assignment());
                     continue;
                 }
                 if (ctx.is_shared(get_enode(x_j))) {
@@ -1681,7 +1682,7 @@ namespace smt {
                     TRACE("opt", tout << "moved v" << x_j << " to lower bound\n";);
                 }
                 update_value(x_j, max_gain);
-                SASSERT(valid_assignment());
+                SASSERT(!maintain_integrality || valid_assignment());
                 continue;
             }
             
@@ -1709,7 +1710,7 @@ namespace smt {
             coeff.neg();
             add_tmp_row(r, coeff, r2);
             SASSERT(r.get_idx_of(x_j) == -1);
-            SASSERT(valid_assignment());
+            SASSERT(!maintain_integrality || valid_assignment());
         }
         TRACE("opt", display(tout););
         return (best_efforts>0)?BEST_EFFORT:result;
@@ -1781,10 +1782,10 @@ namespace smt {
        \brief Maximize/Minimize the given variable. The bounds of v are update if procedure succeeds.
     */
     template<typename Ext>
-    typename theory_arith<Ext>::max_min_t theory_arith<Ext>::max_min(theory_var v, bool max, bool& has_shared) {
+   typename theory_arith<Ext>::max_min_t theory_arith<Ext>::max_min(theory_var v, bool max, bool maintain_integrality, bool& has_shared) {
         expr* e = get_enode(v)->get_owner();
 
-        SASSERT(valid_assignment());
+        SASSERT(!maintain_integrality || valid_assignment());
         SASSERT(!is_quasi_base(v));
         if ((max && at_upper(v)) || (!max && at_lower(v))) {
             TRACE("opt", tout << "At bound: " << mk_pp(e, get_manager()) << "...\n";);
@@ -1803,7 +1804,7 @@ namespace smt {
                     add_tmp_row_entry<true>(m_tmp_row, it->m_coeff, it->m_var);
             }            
         }
-        max_min_t r = max_min(m_tmp_row, max, has_shared);
+        max_min_t r = max_min(m_tmp_row, max, maintain_integrality, has_shared);
         if (r == OPTIMIZED) {
             TRACE("opt", tout << mk_pp(e, get_manager()) << " " << (max ? "max" : "min") << " value is: " << get_value(v) << "\n";
                   display_row(tout, m_tmp_row, true); display_row_info(tout, m_tmp_row););
@@ -1830,9 +1831,9 @@ namespace smt {
         svector<theory_var>::const_iterator it  = vars.begin();
         svector<theory_var>::const_iterator end = vars.end();
         for (; it != end; ++it) {
-            if (max_min(*it, true, has_shared) == OPTIMIZED && !has_shared)
+            if (max_min(*it, true, false, has_shared) == OPTIMIZED && !has_shared)
                 succ = true;
-            if (max_min(*it, false, has_shared) == OPTIMIZED && !has_shared)
+            if (max_min(*it, false, false, has_shared) == OPTIMIZED && !has_shared)
                 succ = true;
         }
         if (succ) {

src/smt/theory_arith_inv.h

@@ -214,10 +214,13 @@ namespace smt {
 
     template<typename Ext>
     bool theory_arith<Ext>::valid_assignment() const {
-        return 
+        if (valid_row_assignment() &&
-            valid_row_assignment() &&
             satisfy_bounds() &&
-            satisfy_integrality();
+            satisfy_integrality()) {
+            return true;
+        }
+        TRACE("arith", display(tout););
+        return false;
     }
 
 #endif

src/smt/theory_arith_nl.h

@@ -2371,7 +2371,7 @@ namespace smt {
             return FC_CONTINUE;
         }
         
-        if (!max_min_nl_vars())
+        if (!max_min_nl_vars()) 
             return FC_CONTINUE;
 
         if (check_monomial_assignments()) {

src/tactic/arith/probe_arith.cpp

@@ -549,9 +549,10 @@ struct is_non_qfufnra_functor {
             case OP_IRRATIONAL_ALGEBRAIC_NUM:
                 return;
             case OP_MUL:
-                if (n->get_num_args() == 2 ||
+                if (n->get_num_args() == 2 &&
-                    (!u.is_numeral(n->get_arg(0)) &&
+                    u.is_real(n->get_arg(0)) && 
-                     !u.is_numeral(n->get_arg(1)))) {
+                    !u.is_numeral(n->get_arg(0)) &&
+                    !u.is_numeral(n->get_arg(1))) {
                     m_has_nonlinear = true;
                 }
                 return;

src/tactic/nlsat_smt/nl_purify_tactic.cpp

@@ -311,16 +311,17 @@ private:
             // assert equalities between equal interface real variables.
 
             model_ref mdl_nl, mdl_smt;
-            model_converter2model(m, nl_mc.get(), mdl_nl);
+            if (mdl_nl.get()) {
-            update_eq_values(mdl_nl);
+                model_converter2model(m, nl_mc.get(), mdl_nl);
-            enforce_equalities(mdl_nl, m_nl_g);
+                update_eq_values(mdl_nl);
-            
+                enforce_equalities(mdl_nl, m_nl_g);
-            setup_assumptions(mdl_nl);
+                
-
+                setup_assumptions(mdl_nl);
-            TRACE("nlsat_smt", 
+                
-                  model_smt2_pp(tout << "nl model\n", m, *mdl_nl.get(), 0);
+                TRACE("nlsat_smt", 
-                  m_solver->display(tout << "smt goal:\n"); tout << "\n";);
+                      model_smt2_pp(tout << "nl model\n", m, *mdl_nl.get(), 0);
-
+                      m_solver->display(tout << "smt goal:\n"); tout << "\n";);
+            }
             result.reset();
             lbool r = m_solver->check_sat(m_asms.size(), m_asms.c_ptr());
             if (r == l_false) {
@@ -352,7 +353,9 @@ private:
                 TRACE("nlsat_smt", 
                       m_fmc->display(tout << "joint state is sat\n");
                       nl_mc->display(tout << "nl\n"););
-                merge_models(*mdl_nl.get(), mdl_smt);
+                if (mdl_nl.get()) {
+                    merge_models(*mdl_nl.get(), mdl_smt);
+                }
                 mc = m_fmc.get();
                 apply(mc, mdl_smt, 0);
                 mc = model2model_converter(mdl_smt.get());