-
Notifications
You must be signed in to change notification settings - Fork 1
/
SatSolver.h
103 lines (82 loc) · 2.43 KB
/
SatSolver.h
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
//
// Created by vedad on 18/06/18.
//
#ifndef NANOQBF_SATSOLVER_H
#define NANOQBF_SATSOLVER_H
#include "ipasir.h"
#include "types/Assignment.h"
#include "Logger.h"
#include "types/Clause.h"
#include <vector>
/// A SAT solver interface using IPASIR
class SatSolver
{
public:
/// SatSolver Constructor
inline SatSolver() : solver_(ipasir_init()), num_vars(0), mem_error(false){ }
/// SatSolver Destructor
inline ~SatSolver() { ipasir_release(solver_); }
/// Destroys the currently used #solver_ and requests a new one
inline void reset();
/// Solves the given CNF
inline int solve();
/// Adds a literal to the current clause in the formula inside #solver_
inline void add(Lit l);
/// Pushes the current clause into #solver_
inline void push();
/// Adds a clause from a Clause object to the formula inside #solver_
inline void addClause(const Clause* clause);
/// Gets the Lit representing the found value of \a v
inline Lit getValue(Var v);
/// Reserves \num variable indexes inside #solver_
inline Var reserveVars(unsigned num);
/// Checks whether there was a memory error
inline bool hasMemory() const { return !mem_error; }
private:
void* solver_; ///< IPASIR solver object
unsigned num_vars; ///< number of variables in #solver_
bool mem_error; ///< records that an out of memory error occured
};
inline void SatSolver::reset()
{
ipasir_release(solver_);
solver_ = ipasir_init();
num_vars = 0;
mem_error = false;
}
inline int SatSolver::solve()
{
if (mem_error) return -1;
return ipasir_solve(solver_);
}
inline void SatSolver::add(Lit l)
{
assert(l != 0);
mem_error |= ipasir_add(solver_, l);
if(mem_error) throw std::bad_alloc();
}
inline void SatSolver::push()
{
mem_error |= ipasir_add(solver_, 0);
if(mem_error) throw std::bad_alloc();
}
inline void SatSolver::addClause(const Clause* clause)
{
for(const_lit_iterator l_iter = clause->begin_e(); l_iter != clause->end_e(); l_iter++)
mem_error |= ipasir_add(solver_, *l_iter);
for(const_lit_iterator l_iter = clause->begin_a(); l_iter != clause->end_a(); l_iter++)
mem_error |= ipasir_add(solver_, *l_iter);
mem_error |= ipasir_add(solver_, 0);
if(mem_error) throw std::bad_alloc();
}
inline Lit SatSolver::getValue(Var v)
{
return ipasir_val(solver_, v);
}
inline Var SatSolver::reserveVars(unsigned num)
{
Var res = num_vars + 1;
num_vars += num;
return res;
}
#endif //NANOQBF_SATSOLVER_H