From e5f4c9302d2f68e52b246210080e129c199bdb41 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Fri, 6 Nov 2020 22:10:54 +0000
Subject: [PATCH] Make IPASIR support compile

Hardness support was added to minisat2 only, and 89641a2 failed to
update the IPASIR interface.

Also cleanup the list of phony targets in the top-level Makefile, and
ensure that linking of the memory analyzer succeeds even in presence of
LIBS set on the make command line.

Fixes: #5345
---
 src/Makefile                        |  2 +-
 src/memory-analyzer/Makefile        |  3 ++-
 src/solvers/sat/satcheck_ipasir.cpp |  7 +++++--
 src/solvers/sat/satcheck_ipasir.h   | 22 ++++++++++++++++++++--
 4 files changed, 28 insertions(+), 6 deletions(-)

diff --git a/src/Makefile b/src/Makefile
index 953ec2be9cf..2bd3e7218c1 100644
--- a/src/Makefile
+++ b/src/Makefile
@@ -163,4 +163,4 @@ cadical-download:
 doc :
 	doxygen
 
-.PHONY: ipasir-build minisat2-download glucose-download
+.PHONY: minisat2-download cudd-download glucose-download cadical-download
diff --git a/src/memory-analyzer/Makefile b/src/memory-analyzer/Makefile
index 870918156ad..41bb6c4d414 100644
--- a/src/memory-analyzer/Makefile
+++ b/src/memory-analyzer/Makefile
@@ -7,7 +7,7 @@ SRC = \
 
 INCLUDES= -I ..
 
-LIBS = \
+OBJ += \
   ../ansi-c/ansi-c$(LIBEXT) \
   ../goto-programs/goto-programs$(LIBEXT) \
   ../linking/linking$(LIBEXT) \
@@ -15,6 +15,7 @@ LIBS = \
   ../big-int/big-int$(LIBEXT) \
   ../langapi/langapi$(LIBEXT)
 
+LIBS =
 
 CLEANFILES = memory-analyzer$(EXEEXT)
 
diff --git a/src/solvers/sat/satcheck_ipasir.cpp b/src/solvers/sat/satcheck_ipasir.cpp
index c3853b957c4..44192c0a0d3 100644
--- a/src/solvers/sat/satcheck_ipasir.cpp
+++ b/src/solvers/sat/satcheck_ipasir.cpp
@@ -90,6 +90,9 @@ void satcheck_ipasirt::lcnf(const bvt &bv)
   }
   ipasir_add(solver, 0); // terminate clause
 
+  with_solver_hardness(
+    [&bv](solver_hardnesst &hardness) { hardness.register_clause(bv); });
+
   clause_counter++;
 }
 
@@ -158,8 +161,8 @@ void satcheck_ipasirt::set_assignment(literalt a, bool value)
   INVARIANT(false, "method not supported");
 }
 
-satcheck_ipasirt::satcheck_ipasirt()
-: solver(nullptr)
+satcheck_ipasirt::satcheck_ipasirt(message_handlert &message_handler)
+  : cnf_solvert(message_handler), solver(nullptr)
 {
   INVARIANT(!solver, "there cannot be a solver already");
   solver=ipasir_init();
diff --git a/src/solvers/sat/satcheck_ipasir.h b/src/solvers/sat/satcheck_ipasir.h
index 107620cfafc..0ab6192a6b8 100644
--- a/src/solvers/sat/satcheck_ipasir.h
+++ b/src/solvers/sat/satcheck_ipasir.h
@@ -14,11 +14,13 @@ instructions.
 
 #include "cnf.h"
 
+#include <solvers/hardness_collector.h>
+
 /// Interface for generic SAT solver interface IPASIR
-class satcheck_ipasirt:public cnf_solvert
+class satcheck_ipasirt : public cnf_solvert, public hardness_collectort
 {
 public:
-  satcheck_ipasirt();
+  satcheck_ipasirt(message_handlert &message_handler);
   virtual ~satcheck_ipasirt() override;
 
   /// This method returns the description produced by the linked SAT solver
@@ -44,12 +46,28 @@ class satcheck_ipasirt:public cnf_solvert
     return true;
   }
 
+  void
+  with_solver_hardness(std::function<void(solver_hardnesst &)> handler) override
+  {
+    if(solver_hardness.has_value())
+    {
+      handler(solver_hardness.value());
+    }
+  }
+
+  void enable_hardness_collection() override
+  {
+    solver_hardness = solver_hardnesst{};
+  }
+
 protected:
   resultt do_prop_solve() override;
 
   void *solver;
 
   bvt assumptions;
+
+  optionalt<solver_hardnesst> solver_hardness;
 };
 
 #endif // CPROVER_SOLVERS_SAT_SATCHECK_IPASIR_H