From a0fd3f7be612061f37aaaaed170fe61bba58040b Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <mt@debian.org>
Date: Sun, 8 Apr 2018 13:04:57 +0100
Subject: [PATCH] Remove support for Limmat as a SAT solver

It wasn't available via configuration options anymore anyway and
Limmat's victory at the SAT competition dates back to 2002.
---
 src/solvers/CMakeLists.txt          |   4 -
 src/solvers/Makefile                |   8 --
 src/solvers/sat/satcheck_limmat.cpp | 137 ----------------------------
 src/solvers/sat/satcheck_limmat.h   |  33 -------
 4 files changed, 182 deletions(-)
 delete mode 100644 src/solvers/sat/satcheck_limmat.cpp
 delete mode 100644 src/solvers/sat/satcheck_limmat.h

diff --git a/src/solvers/CMakeLists.txt b/src/solvers/CMakeLists.txt
index 5acd6652114..f41995fd662 100644
--- a/src/solvers/CMakeLists.txt
+++ b/src/solvers/CMakeLists.txt
@@ -44,9 +44,6 @@ set(booleforce_source
 set(minibdd_source
     ${CMAKE_CURRENT_SOURCE_DIR}/miniBDD/example.cpp
 )
-set(limmat_source
-    ${CMAKE_CURRENT_SOURCE_DIR}/sat/satcheck_limmat.cpp
-)
 
 file(GLOB_RECURSE sources "*.cpp" "*.h")
 list(REMOVE_ITEM sources
@@ -62,7 +59,6 @@ list(REMOVE_ITEM sources
     ${lingeling_source}
     ${booleforce_source}
     ${minibdd_source}
-    ${limmat_source}
 )
 
 add_library(solvers ${sources})
diff --git a/src/solvers/Makefile b/src/solvers/Makefile
index 20100504caa..8a2b869783f 100644
--- a/src/solvers/Makefile
+++ b/src/solvers/Makefile
@@ -77,13 +77,6 @@ ifneq ($(LINGELING),)
   CP_CXXFLAGS += -DHAVE_LINGELING
 endif
 
-ifneq ($(LIMMAT),)
-  LIMMAT_SRC=sat/satcheck_limmat.cpp
-  LIMMAT_INCLUDE=-I $(LIMMAT)
-  LIMMAT_LIB=$(LIMMAT)/liblimmat$(LIBEXT)
-  CP_CXXFLAGS += -DHAVE_LIMMAT
-endif
-
 SRC = $(BOOLEFORCE_SRC) \
       $(CHAFF_SRC) \
       $(CUDD_SRC) \
@@ -96,7 +89,6 @@ SRC = $(BOOLEFORCE_SRC) \
       $(PRECOSAT_SRC) \
       $(SMVSAT_SRC) \
       $(SQUOLEM2_SRC) \
-      $(LIMMAT_SRC) \
       cvc/cvc_conv.cpp \
       cvc/cvc_dec.cpp \
       flattening/arrays.cpp \
diff --git a/src/solvers/sat/satcheck_limmat.cpp b/src/solvers/sat/satcheck_limmat.cpp
deleted file mode 100644
index 10fd310ff35..00000000000
--- a/src/solvers/sat/satcheck_limmat.cpp
+++ /dev/null
@@ -1,137 +0,0 @@
-/*******************************************************************\
-
-Module:
-
-Author: Daniel Kroening, kroening@kroening.com
-
-\*******************************************************************/
-
-#include "satcheck_limmat.h"
-
-#include <cassert>
-
-extern "C"
-{
-#include "limmat.h"
-}
-
-satcheck_limmatt::satcheck_limmatt()
-{
-  solver=new_Limmat(NULL);
-}
-
-satcheck_limmatt::~satcheck_limmatt()
-{
-  if(solver!=NULL)
-    delete_Limmat(solver);
-}
-
-tvt satcheck_limmatt::l_get(literalt a) const
-{
-  if(a.is_true())
-    return tvt(true);
-  else if(a.is_false())
-    return tvt(false);
-
-  tvt result;
-  unsigned v=a.var_no();
-
-  assert(v<assignment.size());
-
-  switch(assignment[v])
-  {
-    case 0: result=tvt(false); break;
-    case 1: result=tvt(true); break;
-    default: result=tvt(tvt::tv_enumt::TV_UNKNOWN); break;
-  }
-
-  if(a.sign())
-    result=!result;
-
-  return result;
-}
-
-const std::string satcheck_limmatt::solver_text()
-{
-  return std::string("Limmat version ")+version_Limmat();
-}
-
-void satcheck_limmatt::copy_cnf()
-{
-  for(clausest::iterator it=clauses.begin();
-      it!=clauses.end();
-      it++)
-      // it=clauses.erase(it))
-  {
-    int *clause=new int[it->size()+1];
-
-    for(unsigned j=0; j<it->size(); j++)
-      clause[j]=(*it)[j].dimacs();
-
-    // zero-terminated
-    clause[it->size()]=0;
-
-    add_Limmat(solver, clause);
-
-    delete clause;
-  }
-}
-
-propt::resultt satcheck_limmatt::prop_solve()
-{
-  copy_cnf();
-
-  {
-    std::string msg=
-      std::to_string(maxvar_Limmat(solver))+" variables, "+
-      std::to_string(clauses_Limmat(solver))+" clauses";
-    messaget::status() << msg << messaget::eom;
-  }
-
-  int status=sat_Limmat(solver, -1);
-
-  {
-    std::string msg;
-
-    switch(status)
-    {
-     case 0:
-      msg="SAT checker: instance is UNSATISFIABLE";
-      break;
-
-     case 1:
-      msg="SAT checker: instance is SATISFIABLE";
-      break;
-
-     default:
-      msg="SAT checker failed: unknown result";
-      break;
-    }
-
-    messaget::status() << msg << messaget::eom;
-  }
-
-  if(status==0)
-  {
-    assignment.clear();
-    return P_UNSATISFIABLE;
-  }
-
-  if(status==1)
-  {
-    assignment.resize(no_variables()+1, 2); // unknown is default
-
-    for(const int *a=assignment_Limmat(solver); *a!=0; a++)
-    {
-      int v=*a;
-      if(v<0)
-        v=-v;
-      assert((unsigned)v<assignment.size());
-      assignment[v]=(*a)>=0;
-    }
-
-    return P_SATISFIABLE;
-  }
-
-  return P_ERROR;
-}
diff --git a/src/solvers/sat/satcheck_limmat.h b/src/solvers/sat/satcheck_limmat.h
deleted file mode 100644
index 91e8e3d9df8..00000000000
--- a/src/solvers/sat/satcheck_limmat.h
+++ /dev/null
@@ -1,33 +0,0 @@
-/*******************************************************************\
-
-Module:
-
-Author: Daniel Kroening, kroening@kroening.com
-
-\*******************************************************************/
-
-
-#ifndef CPROVER_SOLVERS_SAT_SATCHECK_LIMMAT_H
-#define CPROVER_SOLVERS_SAT_SATCHECK_LIMMAT_H
-
-#include <vector>
-#include "dimacs_cnf.h"
-
-class satcheck_limmatt:public dimacs_cnft
-{
- public:
-  satcheck_limmatt();
-  virtual ~satcheck_limmatt();
-
-  virtual const std::string solver_text();
-  virtual resultt prop_solve();
-  virtual tvt l_get(literalt a) const;
-
-  void copy_cnf();
-
- protected:
-  struct Limmat *solver;
-  std::vector<unsigned char> assignment;
-};
-
-#endif // CPROVER_SOLVERS_SAT_SATCHECK_LIMMAT_H