solvers: add ipasir driver

Add the necessary source changes to allow CBMC to use IPASIR solvers.

Author: Norbert Manthey

src/solvers/Makefile

@@ -21,6 +21,14 @@ ifneq ($(MINISAT2),)
   CP_CXXFLAGS += -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS
 endif
 
+ifneq ($(IPASIR),)
+  IPASIR_SRC=sat/satcheck_ipasir.cpp
+  IPASIR_INCLUDE=-I $(IPASIR)
+  IPASIR_LIB=$(IPASIR)/ipasir.a
+  CP_CXXFLAGS += -DHAVE_IPASIR -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS
+  override CXXFLAGS := $(filter-out -pedantic, $(CXXFLAGS))
+endif
+
 ifneq ($(GLUCOSE),)
   GLUCOSE_SRC=sat/satcheck_glucose.cpp
   GLUCOSE_INCLUDE=-I $(GLUCOSE)
@@ -82,6 +90,7 @@ SRC = $(BOOLEFORCE_SRC) \
       $(GLUCOSE_SRC) \
       $(LINGELING_SRC) \
       $(MINISAT2_SRC) \
+      $(IPASIR_SRC) \
       $(MINISAT_SRC) \
       $(PICOSAT_SRC) \
       $(PRECOSAT_SRC) \
@@ -198,6 +207,7 @@ SRC = $(BOOLEFORCE_SRC) \
 
 INCLUDES += -I .. \
   $(CHAFF_INCLUDE) $(BOOLEFORCE_INCLUDE) $(MINISAT_INCLUDE) $(MINISAT2_INCLUDE) \
+  $(IPASIR_INCLUDE) \
   $(SMVSAT_INCLUDE) $(SQUOLEM2_INC) $(CUDD_INCLUDE) $(GLUCOSE_INCLUDE) \
 	$(PRECOSAT_INCLUDE) $(PICOSAT_INCLUDE) $(LINGELING_INCLUDE)
 

src/solvers/prop/literal.h

@@ -193,6 +193,9 @@ inline literalt neg(literalt a) { return !a; }
 inline literalt pos(literalt a) { return a; }
 
 
+inline bool is_false (const literalt &l) { return (l.is_false()); }
+inline bool is_true (const literalt &l) { return (l.is_true()); }
+
 // bit-vectors
 typedef std::vector<literalt> bvt;
 

src/solvers/sat/satcheck.h

@@ -10,7 +10,9 @@ Author: Daniel Kroening, [email protected]
 #ifndef CPROVER_SOLVERS_SAT_SATCHECK_H
 #define CPROVER_SOLVERS_SAT_SATCHECK_H
 
-// this picks the "default" SAT solver
+// This sets a define for the SAT solver
+// based on set flags that come via the compiler
+// command line.
 
 // #define SATCHECK_ZCHAFF
 // #define SATCHECK_MINISAT1
@@ -21,6 +23,42 @@ Author: Daniel Kroening, [email protected]
 // #define SATCHECK_PICOSAT
 // #define SATCHECK_LINGELING
 
+#if defined(HAVE_IPASIR) && !defined(SATCHECK_IPASIR)
+#define SATCHECK_IPASIR
+#endif
+
+#if defined(HAVE_ZCHAFF) && !defined(SATCHECK_ZCHAFF)
+#define SATCHECK_ZCHAFF
+#endif
+
+#if defined(HAVE_MINISAT1) && !defined(SATCHECK_MINISAT1)
+#define SATCHECK_MINISAT1
+#endif
+
+#if defined(HAVE_MINISAT2) && !defined(SATCHECK_MINISAT2)
+#define SATCHECK_MINISAT2
+#endif
+
+#if defined(HAVE_GLUCOSE) && !defined(SATCHECK_GLUCOSE)
+#define SATCHECK_GLUCOSE
+#endif
+
+#if defined(HAVE_BOOLEFORCE) && !defined(SATCHECK_BOOLEFORCE)
+#define SATCHECK_BOOLEFORCE
+#endif
+
+#if defined(HAVE_PRECOSAT) && !defined(SATCHECK_PRECOSAT)
+#define SATCHECK_PRECOSAT
+#endif
+
+#if defined(HAVE_PICOSAT) && !defined(SATCHECK_PICOSAT)
+#define SATCHECK_PICOSAT
+#endif
+
+#if defined(HAVE_LINGELING) && !defined(SATCHECK_LINGELING)
+#define SATCHECK_LINGELING
+#endif
+
 #if defined SATCHECK_ZCHAFF
 
 #include "satcheck_zchaff.h"
@@ -49,6 +87,13 @@ typedef satcheck_minisat1t satcheck_no_simplifiert;
 typedef satcheck_minisat_simplifiert satcheckt;
 typedef satcheck_minisat_no_simplifiert satcheck_no_simplifiert;
 
+#elif defined SATCHECK_IPASIR
+
+#include "satcheck_ipasir.h"
+
+typedef satcheck_ipasirt satcheckt;
+typedef satcheck_ipasirt satcheck_no_simplifiert;
+
 #elif defined SATCHECK_PRECOSAT
 
 #include "satcheck_precosat.h"

src/solvers/sat/satcheck_ipasir.cpp

@@ -0,0 +1,196 @@
+/*******************************************************************\
+
+Module: External SAT Solver Binding
+
+Author: Norbert Manthey, [email protected]
+
+\*******************************************************************/
+
+#ifndef _MSC_VER
+#include <inttypes.h>
+#endif
+
+#include <algorithm>
+#include <cassert>
+#include <stack>
+
+#include <util/threeval.h>
+
+#include "satcheck_ipasir.h"
+
+#ifdef HAVE_IPASIR
+
+extern "C"
+{
+#include <ipasir.h>
+}
+
+/*
+
+Interface description:
+https://github.com/biotomas/ipasir/blob/master/ipasir.h
+
+Representation:
+Variables for a formula start with 1! 0 is used as termination symbol.
+
+*/
+
+tvt satcheck_ipasirt::l_get(literalt a) const
+{
+  if(a.is_true())
+    return tvt(true);
+  else if(a.is_false())
+    return tvt(false);
+
+  tvt result;
+
+  // compare to internal no_variables number
+  if(a.var_no()>=(unsigned)no_variables())
+    return tvt::unknown();
+
+  const int val=ipasir_val(solver, a.var_no());
+
+  if(val>0)
+    result=tvt(true);
+  else if(val<0)
+    result=tvt(false);
+  else
+    return tvt::unknown();
+
+  if(a.sign())
+    result=!result;
+
+  return result;
+}
+
+const std::string satcheck_ipasirt::solver_text()
+{
+  return std::string(ipasir_signature());
+}
+
+void satcheck_ipasirt::lcnf(const bvt &bv)
+{
+  forall_literals(it, bv)
+  {
+    if(it->is_true())
+      return;
+    else if(!it->is_false())
+      INVARIANT(it->var_no()<(unsigned)no_variables(),
+             "reject out of bound variables");
+  }
+
+  forall_literals(it, bv)
+  {
+    if(!it->is_false())
+    {
+      // add literal with correct sign
+      ipasir_add(solver, it->dimacs());
+    }
+  }
+  ipasir_add(solver, 0); // terminate clause
+
+  clause_counter++;
+}
+
+propt::resultt satcheck_ipasirt::prop_solve()
+{
+  INVARIANT(status!=statust::ERROR, "there cannot be an error");
+
+  {
+    messaget::status() <<
+      (no_variables()-1) << " variables, " <<
+      clause_counter << " clauses" << eom;
+  }
+
+  // use the internal representation, as ipasir does not support reporting the
+  // status
+  if(status==statust::UNSAT)
+  {
+    messaget::status() <<
+      "SAT checker inconsistent: instance is UNSATISFIABLE" << eom;
+  }
+  else
+  {
+    // if assumptions contains false, we need this to be UNSAT
+    bvt::const_iterator it = std::find_if(assumptions.begin(),
+      assumptions.end(), is_false);
+    const bool has_false = it != assumptions.end();
+
+    if(has_false)
+    {
+      messaget::status() <<
+        "got FALSE as assumption: instance is UNSATISFIABLE" << eom;
+    }
+    else
+    {
+      forall_literals(it, assumptions)
+        if(!it->is_false())
+          ipasir_assume(solver, it->dimacs());
+
+      // solve the formula, and handle the return code (10=SAT, 20=UNSAT)
+      int solver_state=ipasir_solve(solver);
+      if(10==solver_state)
+      {
+        messaget::status() <<
+          "SAT checker: instance is SATISFIABLE" << eom;
+        status=statust::SAT;
+        return resultt::P_SATISFIABLE;
+      }
+      else if(20==solver_state)
+      {
+        messaget::status() <<
+          "SAT checker: instance is UNSATISFIABLE" << eom;
+      }
+      else
+      {
+        messaget::status() <<
+          "SAT checker: solving returned without solution" << eom;
+        throw "solving inside IPASIR SAT solver has been interrupted";
+      }
+    }
+  }
+
+  status=statust::UNSAT;
+  return resultt::P_UNSATISFIABLE;
+}
+
+void satcheck_ipasirt::set_assignment(literalt a, bool value)
+{
+  INVARIANT(!a.is_constant(), "cannot set an assignment for a constant");
+  INVARIANT(false, "method not supported");
+}
+
+satcheck_ipasirt::satcheck_ipasirt()
+: solver(nullptr)
+{
+  INVARIANT(!solver, "there cannot be a solver already");
+  solver=ipasir_init();
+}
+
+satcheck_ipasirt::~satcheck_ipasirt()
+{
+  if(solver)
+    ipasir_release(solver);
+  solver=nullptr;
+}
+
+bool satcheck_ipasirt::is_in_conflict(literalt a) const
+{
+  return ipasir_failed(solver, a.var_no());
+}
+
+void satcheck_ipasirt::set_assumptions(const bvt &bv)
+{
+  bvt::const_iterator it = std::find_if(bv.begin(), bv.end(), is_true);
+  const bool has_true = it != bv.end();
+
+  if(has_true)
+  {
+    assumptions.clear();
+    return;
+  }
+  // only copy assertions, if there is no false in bt parameter
+  assumptions=bv;
+}
+
+#endif

src/solvers/sat/satcheck_ipasir.h

@@ -0,0 +1,59 @@
+/*******************************************************************\
+
+Module:
+
+Author: Norbert Manthey, [email protected]
+
+Sample compilation command:
+(to be executed from base directory of project)
+
+make clean
+make ipasir-build
+CXXFLAGS=-g IPASIR=../../ipasir LIBSOLVER=$(pwd)/ipasir/libipasir.a \
+  CFLAGS="-Wall -O2 -DSATCHECK_IPSAIR" LINKFLAGS="-static" \
+  make -j 7 -C $(pwd)/src/;
+
+Note: Make sure, the LIBSOLVER variable is set in the environment!
+      The variable should point to the solver you actually want to
+      link against.
+
+\*******************************************************************/
+
+#ifndef CPROVER_SOLVERS_SAT_SATCHECK_IPASIR_H
+#define CPROVER_SOLVERS_SAT_SATCHECK_IPASIR_H
+
+#include "cnf.h"
+
+/// Interface for generic SAT solver interface IPASIR
+class satcheck_ipasirt:public cnf_solvert
+{
+public:
+  satcheck_ipasirt();
+  virtual ~satcheck_ipasirt() override;
+
+  /// This method returns the description produced by the linked SAT solver
+  virtual const std::string solver_text() override;
+
+  virtual resultt prop_solve() override;
+
+  /// This method returns the truth value for a literal of the current SAT model
+  virtual tvt l_get(literalt a) const override final;
+
+  virtual void lcnf(const bvt &bv) override final;
+
+  /* This method is not supported, and currently not called anywhere in CBMC */
+  virtual void set_assignment(literalt a, bool value) override;
+
+  virtual void set_assumptions(const bvt &_assumptions) override;
+
+  virtual bool is_in_conflict(literalt a) const override;
+  virtual bool has_set_assumptions() const override final { return true; }
+  virtual bool has_is_in_conflict() const override final { return true; }
+
+protected:
+  void *solver;
+
+  bvt assumptions;
+};
+
+#endif // CPROVER_SOLVERS_SAT_SATCHECK_IPASIR_H