cprover
pbs_dimacs_cnf.h
Go to the documentation of this file.
1
/*******************************************************************\
2
3
Module:
4
5
Author: Alex Groce
6
7
\*******************************************************************/
8
9
10
#ifndef CPROVER_SOLVERS_SAT_PBS_DIMACS_CNF_H
11
#define CPROVER_SOLVERS_SAT_PBS_DIMACS_CNF_H
12
13
#include <set>
14
#include <map>
15
#include <iosfwd>
16
17
#include "
dimacs_cnf.h
"
18
19
class
pbs_dimacs_cnft
:
public
dimacs_cnft
20
{
21
public
:
22
pbs_dimacs_cnft
():
23
optimize
(false),
24
maximize
(false),
25
binary_search
(false),
26
goal
(0),
27
opt_sum
(0)
28
{
29
}
30
31
virtual
~pbs_dimacs_cnft
()
32
{
33
}
34
35
virtual
void
write_dimacs_pb
(std::ostream &out);
36
37
bool
optimize
;
38
bool
maximize
;
39
bool
binary_search
;
40
41
std::string
pbs_path
;
42
43
int
goal
;
44
int
opt_sum
;
45
46
std::map<literalt, unsigned>
pb_constraintmap
;
47
48
bool
pbs_solve
();
49
50
virtual
resultt
prop_solve
();
51
52
virtual
tvt
l_get
(
literalt
a)
const
;
53
54
// dummy functions
55
56
virtual
const
std::string
solver_text
()
57
{
58
return
"PBS - Pseudo Boolean/CNF Solver and Optimizer"
;
59
}
60
61
protected
:
62
std::set<int>
assigned
;
63
};
64
65
#endif // CPROVER_SOLVERS_SAT_PBS_DIMACS_CNF_H
pbs_dimacs_cnft::pbs_path
std::string pbs_path
Definition:
pbs_dimacs_cnf.h:41
pbs_dimacs_cnft::goal
int goal
Definition:
pbs_dimacs_cnf.h:43
pbs_dimacs_cnft::prop_solve
virtual resultt prop_solve()
Definition:
pbs_dimacs_cnf.cpp:207
pbs_dimacs_cnft::write_dimacs_pb
virtual void write_dimacs_pb(std::ostream &out)
Definition:
pbs_dimacs_cnf.cpp:19
pbs_dimacs_cnft::binary_search
bool binary_search
Definition:
pbs_dimacs_cnf.h:39
pbs_dimacs_cnft::pbs_solve
bool pbs_solve()
Definition:
pbs_dimacs_cnf.cpp:61
pbs_dimacs_cnft::pbs_dimacs_cnft
pbs_dimacs_cnft()
Definition:
pbs_dimacs_cnf.h:22
pbs_dimacs_cnft::~pbs_dimacs_cnft
virtual ~pbs_dimacs_cnft()
Definition:
pbs_dimacs_cnf.h:31
pbs_dimacs_cnft
Definition:
pbs_dimacs_cnf.h:19
pbs_dimacs_cnft::solver_text
virtual const std::string solver_text()
Definition:
pbs_dimacs_cnf.h:56
propt::resultt
resultt
Definition:
prop.h:96
tvt
Definition:
threeval.h:19
dimacs_cnf.h
pbs_dimacs_cnft::maximize
bool maximize
Definition:
pbs_dimacs_cnf.h:38
literalt
Definition:
literal.h:24
pbs_dimacs_cnft::opt_sum
int opt_sum
Definition:
pbs_dimacs_cnf.h:44
pbs_dimacs_cnft::optimize
bool optimize
Definition:
pbs_dimacs_cnf.h:37
pbs_dimacs_cnft::l_get
virtual tvt l_get(literalt a) const
Definition:
pbs_dimacs_cnf.cpp:244
dimacs_cnft
Definition:
dimacs_cnf.h:17
pbs_dimacs_cnft::pb_constraintmap
std::map< literalt, unsigned > pb_constraintmap
Definition:
pbs_dimacs_cnf.h:46
pbs_dimacs_cnft::assigned
std::set< int > assigned
Definition:
pbs_dimacs_cnf.h:62
solvers
sat
pbs_dimacs_cnf.h
Generated by
1.8.16