10#ifndef CPROVER_SOLVERS_SAT_PBS_DIMACS_CNF_H
11#define CPROVER_SOLVERS_SAT_PBS_DIMACS_CNF_H
57 return "PBS - Pseudo Boolean/CNF Solver and Optimizer";
pbs_dimacs_cnft(message_handlert &message_handler)
tvt l_get(literalt a) const override
virtual ~pbs_dimacs_cnft()
const std::string solver_text() override
resultt do_prop_solve() override
virtual void write_dimacs_pb(std::ostream &out)
std::map< literalt, unsigned > pb_constraintmap
resultt
The result of goto verifying.