Merge pull request #5549 from tautschnig/fix-ipasir

Make IPASIR support compile

Author: tautschnig

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

src/memory-analyzer/Makefile

@@ -7,14 +7,15 @@ SRC = \
 
 INCLUDES= -I ..
 
-LIBS = \
+OBJ += \
   ../ansi-c/ansi-c$(LIBEXT) \
   ../goto-programs/goto-programs$(LIBEXT) \
   ../linking/linking$(LIBEXT) \
   ../util/util$(LIBEXT) \
   ../big-int/big-int$(LIBEXT) \
   ../langapi/langapi$(LIBEXT)
 
+LIBS =
 
 CLEANFILES = memory-analyzer$(EXEEXT)
 

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();

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