cprover
Loading...
Searching...
No Matches
satcheck_ipasir.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: Norbert Manthey, nmanthey@amazon.com
6
7See \ref compilation-and-development-subsection-sat-solver for build
8instructions.
9
10\*******************************************************************/
11
12#ifndef CPROVER_SOLVERS_SAT_SATCHECK_IPASIR_H
13#define CPROVER_SOLVERS_SAT_SATCHECK_IPASIR_H
14
15#include "cnf.h"
16
18
21{
22public:
24 virtual ~satcheck_ipasirt() override;
25
27 const std::string solver_text() override;
28
30 tvt l_get(literalt a) const override final;
31
32 void lcnf(const bvt &bv) override final;
33
34 /* This method is not supported, and currently not called anywhere in CBMC */
35 void set_assignment(literalt a, bool value) override;
36
37 void set_assumptions(const bvt &_assumptions) override;
38
39 bool is_in_conflict(literalt a) const override;
40 bool has_set_assumptions() const override final
41 {
42 return true;
43 }
44 bool has_is_in_conflict() const override final
45 {
46 return true;
47 }
48
49protected:
51
52 void *solver;
53
55};
56
57#endif // CPROVER_SOLVERS_SAT_SATCHECK_IPASIR_H
resultt
Definition prop.h:98
Interface for generic SAT solver interface IPASIR.
bool has_set_assumptions() const override final
void set_assumptions(const bvt &_assumptions) override
tvt l_get(literalt a) const override final
This method returns the truth value for a literal of the current SAT model.
resultt do_prop_solve() override
bool has_is_in_conflict() const override final
virtual ~satcheck_ipasirt() override
satcheck_ipasirt(message_handlert &message_handler)
void lcnf(const bvt &bv) override final
void set_assignment(literalt a, bool value) override
bool is_in_conflict(literalt a) const override
Returns true if an assumption is in the final conflict.
const std::string solver_text() override
This method returns the description produced by the linked SAT solver.
Definition threeval.h:20
CNF Generation, via Tseitin.
Capability to collect the statistics of the complexity of individual solver queries.
std::vector< literalt > bvt
Definition literal.h:201