cprover
satcheck_precosat.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Michael Tautschnig, michael.tautschnig@cs.ox.ac.uk
6 
7 \*******************************************************************/
8 
9 
10 #ifndef CPROVER_SOLVERS_SAT_SATCHECK_PRECOSAT_H
11 #define CPROVER_SOLVERS_SAT_SATCHECK_PRECOSAT_H
12 
13 #include "cnf.h"
14 
15 namespace PrecoSat // NOLINT(readability/namespace)
16 {
17 class Solver; // NOLINT(readability/identifiers)
18 }
19 
21 {
22 public:
24  virtual ~satcheck_precosatt();
25 
26  virtual const std::string solver_text();
27  virtual resultt prop_solve();
28  virtual tvt l_get(literalt a) const;
29 
30  virtual void lcnf(const bvt &bv);
31  virtual void set_assignment(literalt a, bool value);
32 
33  // PicoSAT has this, PrecoSAT doesn't
34  // virtual bool is_in_conflict(literalt a) const;
35  // virtual void set_assumptions(const bvt &_assumptions);
36  virtual bool has_set_assumptions() const { return false; }
37  virtual bool has_is_in_conflict() const { return false; }
38 
39 protected:
40  PrecoSat::Solver *solver;
41  // bvt assumptions;
42 };
43 
44 #endif // CPROVER_SOLVERS_SAT_SATCHECK_PRECOSAT_H
CNF Generation, via Tseitin.
virtual const std::string solver_text()
virtual void lcnf(const bvt &bv)
virtual void set_assignment(literalt a, bool value)
virtual tvt l_get(literalt a) const
Definition: threeval.h:19
resultt
Definition: prop.h:94
virtual bool has_is_in_conflict() const
PrecoSat::Solver * solver
virtual resultt prop_solve()
virtual bool has_set_assumptions() const
std::vector< literalt > bvt
Definition: literal.h:197