cprover
satcheck_limmat.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 #include "satcheck_limmat.h"
10 
11 #include <cassert>
12 
13 extern "C"
14 {
15 #include "limmat.h"
16 }
17 
19 {
20  solver=new_Limmat(NULL);
21 }
22 
24 {
25  if(solver!=NULL)
26  delete_Limmat(solver);
27 }
28 
30 {
31  if(a.is_true())
32  return tvt(true);
33  else if(a.is_false())
34  return tvt(false);
35 
36  tvt result;
37  unsigned v=a.var_no();
38 
39  assert(v<assignment.size());
40 
41  switch(assignment[v])
42  {
43  case 0: result=tvt(false); break;
44  case 1: result=tvt(true); break;
45  default: result=tvt(tvt::tv_enumt::TV_UNKNOWN); break;
46  }
47 
48  if(a.sign())
49  result=!result;
50 
51  return result;
52 }
53 
54 const std::string satcheck_limmatt::solver_text()
55 {
56  return std::string("Limmat version ")+version_Limmat();
57 }
58 
60 {
61  for(clausest::iterator it=clauses.begin();
62  it!=clauses.end();
63  it++)
64  // it=clauses.erase(it))
65  {
66  int *clause=new int[it->size()+1];
67 
68  for(unsigned j=0; j<it->size(); j++)
69  clause[j]=(*it)[j].dimacs();
70 
71  // zero-terminated
72  clause[it->size()]=0;
73 
74  add_Limmat(solver, clause);
75 
76  delete clause;
77  }
78 }
79 
81 {
82  copy_cnf();
83 
84  {
85  std::string msg=
86  std::to_string(maxvar_Limmat(solver))+" variables, "+
87  std::to_string(clauses_Limmat(solver))+" clauses";
88  messaget::status() << msg << messaget::eom;
89  }
90 
91  int status=sat_Limmat(solver, -1);
92 
93  {
94  std::string msg;
95 
96  switch(status)
97  {
98  case 0:
99  msg="SAT checker: instance is UNSATISFIABLE";
100  break;
101 
102  case 1:
103  msg="SAT checker: instance is SATISFIABLE";
104  break;
105 
106  default:
107  msg="SAT checker failed: unknown result";
108  break;
109  }
110 
111  messaget::status() << msg << messaget::eom;
112  }
113 
114  if(status==0)
115  {
116  assignment.clear();
117  return P_UNSATISFIABLE;
118  }
119 
120  if(status==1)
121  {
122  assignment.resize(no_variables()+1, 2); // unknown is default
123 
124  for(const int *a=assignment_Limmat(solver); *a!=0; a++)
125  {
126  int v=*a;
127  if(v<0)
128  v=-v;
129  assert((unsigned)v<assignment.size());
130  assignment[v]=(*a)>=0;
131  }
132 
133  return P_SATISFIABLE;
134  }
135 
136  return P_ERROR;
137 }
mstreamt & result()
Definition: message.h:233
mstreamt & status()
Definition: message.h:238
virtual ~satcheck_limmatt()
virtual tvt l_get(literalt a) const
virtual resultt prop_solve()
static mstreamt & eom(mstreamt &m)
Definition: message.h:193
bool is_true() const
Definition: literal.h:155
Definition: threeval.h:19
var_not var_no() const
Definition: literal.h:82
resultt
Definition: prop.h:94
struct Limmat * solver
virtual const std::string solver_text()
bool sign() const
Definition: literal.h:87
virtual size_t no_variables() const override
Definition: cnf.h:38
std::vector< unsigned char > assignment
bool is_false() const
Definition: literal.h:160