cprover
satcheck_ipasir.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Norbert Manthey, nmanthey@amazon.com
6 
7 Sample compilation command:
8 (to be executed from base directory of project)
9 
10 make clean
11 make ipasir-build
12 CXXFLAGS=-g IPASIR=../../ipasir LIBSOLVER=$(pwd)/ipasir/libipasir.a \
13  CFLAGS="-Wall -O2 -DSATCHECK_IPSAIR" LINKFLAGS="-static" \
14  make -j 7 -C $(pwd)/src/;
15 
16 Note: Make sure, the LIBSOLVER variable is set in the environment!
17  The variable should point to the solver you actually want to
18  link against.
19 
20 \*******************************************************************/
21 
22 #ifndef CPROVER_SOLVERS_SAT_SATCHECK_IPASIR_H
23 #define CPROVER_SOLVERS_SAT_SATCHECK_IPASIR_H
24 
25 #include "cnf.h"
26 
29 {
30 public:
32  virtual ~satcheck_ipasirt() override;
33 
35  virtual const std::string solver_text() override;
36 
37  virtual resultt prop_solve() override;
38 
40  virtual tvt l_get(literalt a) const override final;
41 
42  virtual void lcnf(const bvt &bv) override final;
43 
44  /* This method is not supported, and currently not called anywhere in CBMC */
45  virtual void set_assignment(literalt a, bool value) override;
46 
47  virtual void set_assumptions(const bvt &_assumptions) override;
48 
49  virtual bool is_in_conflict(literalt a) const override;
50  virtual bool has_set_assumptions() const override final { return true; }
51  virtual bool has_is_in_conflict() const override final { return true; }
52 
53 protected:
54  void *solver;
55 
57 };
58 
59 #endif // CPROVER_SOLVERS_SAT_SATCHECK_IPASIR_H
CNF Generation, via Tseitin.
virtual resultt prop_solve() override
virtual bool is_in_conflict(literalt a) const override
Returns true if an assumption is in the final conflict.
virtual void lcnf(const bvt &bv) override final
virtual const std::string solver_text() override
This method returns the description produced by the linked SAT solver.
virtual tvt l_get(literalt a) const override final
This method returns the truth value for a literal of the current SAT model.
virtual void set_assumptions(const bvt &_assumptions) override
virtual ~satcheck_ipasirt() override
virtual bool has_is_in_conflict() const override final
Definition: threeval.h:19
resultt
Definition: prop.h:96
virtual void set_assignment(literalt a, bool value) override
Interface for generic SAT solver interface IPASIR.
virtual bool has_set_assumptions() const override final
std::vector< literalt > bvt
Definition: literal.h:200