@@ -282,8 +282,6 @@ namespace nlsat {
282
282
// then only the factors that are zero in the current interpretation needed to be considered.
283
283
// I don't want to create a nested conjunction in the clause.
284
284
// Then, I assert p_i1 * ... * p_im != 0
285
- bool is_linear = true ;
286
- unsigned x = max_var (p);
287
285
{
288
286
restore_factors _restore (m_factors, m_factors_save);
289
287
factor (p, m_factors);
@@ -296,33 +294,10 @@ namespace nlsat {
296
294
if (is_zero (sign (f))) {
297
295
m_zero_fs.push_back (m_factors.get (i));
298
296
m_is_even.push_back (false );
299
- is_linear &= m_pm.degree (f, x) <= 1 ;
300
297
}
301
298
}
302
299
}
303
-
304
- if (!is_linear) {
305
- scoped_anum_vector& roots = m_roots_tmp;
306
- roots.reset ();
307
- m_am.isolate_roots (p, undef_var_assignment (m_assignment, x), roots);
308
- unsigned num_roots = roots.size ();
309
- if (num_roots > 0 ) {
310
- anum const & x_val = m_assignment.value (x);
311
- for (unsigned i = 0 ; i < num_roots; i++) {
312
- int s = m_am.compare (x_val, roots[i]);
313
- if (s != 0 )
314
- continue ;
315
- TRACE (" nlsat_explain" , tout << " adding (zero assumption) root " << " \n " );
316
- add_root_literal (atom::ROOT_EQ, x, i + 1 , p);
317
- return ;
318
- }
319
- display (verbose_stream () << " polynomial " , p);
320
- m_solver.display (verbose_stream ());
321
- UNREACHABLE ();
322
- }
323
- }
324
300
SASSERT (!m_zero_fs.empty ()); // one of the factors must be zero in the current interpretation, since p is zero in it.
325
-
326
301
literal l = m_solver.mk_ineq_literal (atom::EQ, m_zero_fs.size (), m_zero_fs.data (), m_is_even.data ());
327
302
l.neg ();
328
303
TRACE (" nlsat_explain" , tout << " adding (zero assumption) literal:\n " ; display (tout, l); tout << " \n " ;);
0 commit comments