Go to the documentation of this file.
10 #ifndef CPROVER_SOLVERS_SAT_DIMACS_CNF_H
11 #define CPROVER_SOLVERS_SAT_DIMACS_CNF_H
50 return "DIMACS CNF Dumper";
53 virtual void lcnf(
const bvt &bv);
74 #endif // CPROVER_SOLVERS_SAT_DIMACS_CNF_H
dimacs_cnf_dumpt(std::ostream &_out)
void write_clauses(std::ostream &out)
void write_problem_line(std::ostream &out)
virtual void write_dimacs_cnf(std::ostream &out)
std::vector< literalt > bvt
virtual size_t no_clauses() const
virtual void lcnf(const bvt &bv)
bool is_in_conflict(literalt l) const override
Returns true if an assumption is in the final conflict.
virtual resultt prop_solve()
virtual tvt l_get(literalt) const
virtual const std::string solver_text()
void set_assignment(literalt a, bool value) override
const std::string solver_text() override
virtual ~dimacs_cnf_dumpt()