From 19c1c7aa73d120c1b0f389d32212cec3ff486139 Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Thu, 17 Aug 2023 17:59:40 +0200 Subject: [PATCH] minor comments, skolem = false --- src/math/polysat/univariate/univariate_solver.cpp | 3 ++- src/math/polysat/univariate/univariate_solver.h | 2 +- 2 files changed, 3 insertions(+), 2 deletions(-) diff --git a/src/math/polysat/univariate/univariate_solver.cpp b/src/math/polysat/univariate/univariate_solver.cpp index dd54e262c..fd0f214ca 100644 --- a/src/math/polysat/univariate/univariate_solver.cpp +++ b/src/math/polysat/univariate/univariate_solver.cpp @@ -345,13 +345,14 @@ namespace polysat { parity = mk_numeral(get_parity(get_offset(v_coeff))); return parity; } - parity = m.mk_fresh_const("parity", bv->mk_sort(bit_width)); + parity = m.mk_fresh_const("parity", bv->mk_sort(bit_width), false); expr* parity_1 = bv->mk_bv_add(parity, mk_numeral(1)); // if v = 0 // then parity = N // else v = (v >> parity) << parity // && v != (v >> parity+1) << parity+1 // TODO: what about: v[k:] = 0 && v[k+1:] != 0 ==> parity = k for each k? + // TODO: helper axioms like parity <= N etc.? add(m.mk_ite( m.mk_eq(v, mk_numeral(0)), m.mk_eq(parity, mk_numeral(bit_width)), diff --git a/src/math/polysat/univariate/univariate_solver.h b/src/math/polysat/univariate/univariate_solver.h index 59c82b15e..ad7840a4e 100644 --- a/src/math/polysat/univariate/univariate_solver.h +++ b/src/math/polysat/univariate/univariate_solver.h @@ -74,7 +74,7 @@ namespace polysat { bool find_max(rational& out_max); /** - * Find up to two viable values. + * Find up to two models. * * Precondition: check() returned l_true * returns: true on success, false on resource out