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 
20 {
21 public:
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;
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