14 #include <satsolvercore.h> 15 #include <interpolator.h> 20 sat_instance_new_type(SATSOLVERCORE1,
no_variables(),
true);
61 return std::string(
"SMVSAT");
71 int *lits=
new int[tmp.size()+1];
73 for(
unsigned i=0; i<tmp.size(); i++)
74 lits[i]=tmp[i].dimacs();
96 msg=
"SAT checker: instance is UNSATISFIABLE";
100 msg=
"SAT checker: instance is SATISFIABLE";
104 msg=
"SAT checker failed: unknown result";
114 return P_UNSATISFIABLE;
120 return P_SATISFIABLE;
132 if(
result==P_UNSATISFIABLE)
147 int *lits=
new int[tmp.size()+1];
149 for(
unsigned i=0; i<tmp.size(); i++)
150 lits[i]=tmp[i].dimacs();
155 unsigned clause_id=sat_instance_add_clause(
satsolver, lits);
170 struct interpolator *interpolator_satsolver=
179 interpolator_satsolver->set_clause_partition(i, p);
182 int output=interpolator_satsolver->interpolate(0, 0);
184 build_aig(*interpolator_satsolver, output, dest);
186 delete interpolator_satsolver;
191 struct interpolator &interpolator_satsolver,
195 std::stack<entryt>
stack;
199 while(!
stack.empty())
205 int n=invert?-x.
g:x.
g;
213 else if(n<=satsolver->num_variables())
216 e.
set(ID_identifier, n);
223 unsigned g0=interpolator_satsolver.aig_arg(n, 0);
224 unsigned g1=interpolator_satsolver.aig_arg(n, 1);
void interpolate(exprt &dest)
bool process_clause(const bvt &bv, bvt &dest)
filter 'true' from clause, eliminate duplicates, recognise trivially satisfied clauses ...
std::vector< short > partition_numbers
virtual resultt prop_solve()
static mstreamt & eom(mstreamt &m)
virtual ~satcheck_smvsatt()
const irep_idt & id() const
virtual const std::string solver_text()
virtual void lcnf(const bvt &bv)
Base class for all expressions.
virtual resultt prop_solve()
virtual tvt l_get(literalt a) const
struct sat_instance * satsolver
virtual size_t no_variables() const override
void build_aig(struct interpolator &interpolator_satsolver, int output, exprt &dest)
std::vector< literalt > bvt
virtual void lcnf(const bvt &bv)
void set(const irep_namet &name, const irep_idt &value)