10 #ifndef CPROVER_SOLVERS_SAT_SATCHECK_SMVSAT_H 11 #define CPROVER_SOLVERS_SAT_SATCHECK_SMVSAT_H 29 virtual void lcnf(
const bvt &bv);
45 assert(l.
var_no()<in_core.size());
46 return in_core[l.
var_no()];
65 void interpolate(
exprt &dest);
68 virtual void lcnf(
const bvt &bv);
75 struct interpolator &interpolator_satsolver,
90 #endif // CPROVER_SOLVERS_SAT_SATCHECK_SMVSAT_H CNF Generation, via Tseitin.
std::vector< short > partition_numbers
virtual resultt prop_solve()
virtual ~satcheck_smvsatt()
entryt(int _g, exprt *_e)
virtual const std::string solver_text()
virtual void lcnf(const bvt &bv)
std::vector< bool > in_core
Base class for all expressions.
void set_partition_no(short p)
satcheck_smvsat_interpolatort()
virtual tvt l_get(literalt a) const
bool is_in_core(literalt l) const
struct sat_instance * satsolver
std::vector< literalt > bvt