From 8d871bf8b5164f8faae0d26c564e443b0d46b760 Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Thu, 21 Jul 2022 11:48:41 +0200 Subject: [PATCH] dead code --- src/math/polysat/solver.cpp | 7 ------- src/math/polysat/solver.h | 2 -- 2 files changed, 9 deletions(-) diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp index 795a10dec..adceb7619 100644 --- a/src/math/polysat/solver.cpp +++ b/src/math/polysat/solver.cpp @@ -1108,13 +1108,6 @@ namespace polysat { add_clause(4, cs, is_redundant); } - void solver::insert_constraint(signed_constraints& cs, signed_constraint c) { - SASSERT(c); - LOG_V("INSERTING: " << c); - cs.push_back(c); - SASSERT(invariant(cs)); - } - void solver::push() { LOG("Push user scope"); push_level(); diff --git a/src/math/polysat/solver.h b/src/math/polysat/solver.h index ff5e3d8b9..22e4ad5f2 100644 --- a/src/math/polysat/solver.h +++ b/src/math/polysat/solver.h @@ -226,9 +226,7 @@ namespace polysat { void add_clause(signed_constraint c1, signed_constraint c2, signed_constraint c3, signed_constraint c4, bool is_redundant); void add_clause(unsigned n, signed_constraint* cs, bool is_redundant); - signed_constraint lit2cnstr(sat::literal lit) const { return m_constraints.lookup(lit); } - static void insert_constraint(signed_constraints& cs, signed_constraint c); bool inc() { return m_lim.inc(); }