From 44506096f7699c19f5f25421013d503fc5a6fff0 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 7 Dec 2023 16:03:30 -0800 Subject: [PATCH] tidy --- src/sat/smt/polysat_core.cpp | 2 +- src/sat/smt/polysat_core.h | 2 -- src/sat/smt/polysat_internalize.cpp | 4 ++-- src/sat/smt/polysat_solver.cpp | 2 +- 4 files changed, 4 insertions(+), 6 deletions(-) diff --git a/src/sat/smt/polysat_core.cpp b/src/sat/smt/polysat_core.cpp index 27d6ee731..931a92992 100644 --- a/src/sat/smt/polysat_core.cpp +++ b/src/sat/smt/polysat_core.cpp @@ -225,7 +225,7 @@ namespace polysat { // constraint is unitary, add to viable set if (vars.size() >= 2 && is_assigned(vars[0]) && !is_assigned(vars[1])) { - // m_viable.add_unitary(vars[1], idx); + m_viable.add_unitary(vars[1], idx); } } m_watch[v].shrink(j); diff --git a/src/sat/smt/polysat_core.h b/src/sat/smt/polysat_core.h index 7fdf8c88c..075840a48 100644 --- a/src/sat/smt/polysat_core.h +++ b/src/sat/smt/polysat_core.h @@ -59,8 +59,6 @@ namespace polysat { var_queue m_var_queue; // priority queue of variables to assign vector m_watch; // watch lists for variables for constraints on m_prop_queue where they occur - vector m_subst; // substitution, one for each size. - // values to split on rational m_value; pvar m_var = 0; diff --git a/src/sat/smt/polysat_internalize.cpp b/src/sat/smt/polysat_internalize.cpp index 80c2fb19b..dd761fdc3 100644 --- a/src/sat/smt/polysat_internalize.cpp +++ b/src/sat/smt/polysat_internalize.cpp @@ -3,11 +3,11 @@ Copyright (c) 2022 Microsoft Corporation Module Name: - polysat_model.cpp + polysat_internalize.cpp Abstract: - PolySAT model generation + PolySAT internalize Author: diff --git a/src/sat/smt/polysat_solver.cpp b/src/sat/smt/polysat_solver.cpp index cee129327..58b2c97d1 100644 --- a/src/sat/smt/polysat_solver.cpp +++ b/src/sat/smt/polysat_solver.cpp @@ -3,7 +3,7 @@ Copyright (c 2022 Microsoft Corporation Module Name: - polysat_internalize.cpp + polysat_solver.cpp Abstract: