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
virtual tvt l_get(literalt a) const
std::string pbs_path
virtual resultt prop_solve()
virtual void write_dimacs_pb(std::ostream &out)
virtual ~pbs_dimacs_cnft()
virtual const std::string solver_text()
Definition: threeval.h:19
resultt
Definition: prop.h:96
std::map< literalt, unsigned > pb_constraintmap
std::set< int > assigned