cprover
satcheck_precosat.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Michael Tautschnig, michael.tautschnig@cs.ox.ac.uk
6 
7 \*******************************************************************/
8 
9 #include "satcheck_precosat.h"
10 
11 #include <cassert>
12 
13 #include <util/threeval.h>
14 
15 #include <precosat.hh>
16 
17 #ifndef HAVE_PRECOSAT
18 #error "Expected HAVE_PRECOSAT"
19 #endif
20 
21 #define precosat_lit(a) ((a).var_no()*2 + !(a).sign())
22 
24 {
25  if(a.is_constant())
26  return tvt(a.sign());
27 
28  tvt result;
29 
30  if(a.var_no()>solver->getMaxVar())
32 
33  const int val=solver->val(precosat_lit(a));
34  if(val>0)
35  result=tvt(true);
36  else if(val<0)
37  result=tvt(false);
38  else
40 
41  return result;
42 }
43 
45 {
46  return "PrecoSAT";
47 }
48 
50 {
51  bvt new_bv;
52 
53  if(process_clause(bv, new_bv))
54  return;
55 
56  forall_literals(it, new_bv)
57  solver->add(precosat_lit(*it));
58 
59  solver->add(0);
60 
62 }
63 
65 {
66  assert(status!=ERROR);
67 
68  // We start counting at 1, thus there is one variable fewer.
69  {
70  std::string msg=
71  std::to_string(no_variables()-1)+" variables, "+
72  std::to_string(solver->getAddedOrigClauses())+" clauses";
73  messaget::status() << msg << messaget::eom;
74  }
75 
76  std::string msg;
77 
78  const int res=solver->solve();
79  if(res==1)
80  {
81  msg="SAT checker: instance is SATISFIABLE";
82  messaget::status() << msg << messaget::eom;
83  status=SAT;
84  return P_SATISFIABLE;
85  }
86  else
87  {
88  assert(res==-1);
89  msg="SAT checker: instance is UNSATISFIABLE";
90  messaget::status() << msg << messaget::eom;
91  }
92 
93  status=UNSAT;
94  return P_UNSATISFIABLE;
95 }
96 
98 {
99  assert(false);
100 }
101 
103  solver(new PrecoSat::Solver())
104 {
105  solver->init();
106 }
107 
109 {
110  delete solver;
111 }
112 
113 /*
114 void satcheck_precosatt::set_assumptions(const bvt &bv)
115 {
116  assumptions=bv;
117 
118  forall_literals(it, assumptions)
119  assert(!it->is_constant());
120 }
121 */
mstreamt & result()
Definition: message.h:233
size_t clause_counter
Definition: cnf.h:81
virtual const std::string solver_text()
mstreamt & status()
Definition: message.h:238
bool process_clause(const bvt &bv, bvt &dest)
filter &#39;true&#39; from clause, eliminate duplicates, recognise trivially satisfied clauses ...
Definition: cnf.cpp:416
virtual void lcnf(const bvt &bv)
static mstreamt & eom(mstreamt &m)
Definition: message.h:193
#define forall_literals(it, bv)
Definition: literal.h:199
#define precosat_lit(a)
virtual void set_assignment(literalt a, bool value)
virtual tvt l_get(literalt a) const
Definition: threeval.h:19
var_not var_no() const
Definition: literal.h:82
resultt
Definition: prop.h:94
PrecoSat::Solver * solver
bool is_constant() const
Definition: literal.h:165
bool sign() const
Definition: literal.h:87
virtual resultt prop_solve()
virtual size_t no_variables() const override
Definition: cnf.h:38
std::vector< literalt > bvt
Definition: literal.h:197