10 #ifndef CPROVER_SOLVERS_SAT_SATCHECK_SMVSAT_H 11 #define CPROVER_SOLVERS_SAT_SATCHECK_SMVSAT_H 29 virtual void lcnf(
const bvt &bv);
68 virtual void lcnf(
const bvt &bv);
75 struct interpolator &interpolator_satsolver,
90 #endif // CPROVER_SOLVERS_SAT_SATCHECK_SMVSAT_H CNF Generation, via Tseitin.
void interpolate(exprt &dest)
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.
virtual resultt prop_solve()
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
void build_aig(struct interpolator &interpolator_satsolver, int output, exprt &dest)
std::vector< literalt > bvt
virtual void lcnf(const bvt &bv)