14 #include <satsolvercore.h> 15 #include <interpolator.h> 20 sat_instance_new_type(SATSOLVERCORE1,
no_variables(),
true);
48 case 0: result=
tvt(
false);
break;
49 case 1: result=
tvt(
true);
break;
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);
157 if(partition_numbers.size()<=clause_id)
158 partition_numbers.resize(clause_id+1, -1);
160 partition_numbers[clause_id]=partition_no;
170 struct interpolator *interpolator_satsolver=
175 for(
unsigned i=0; i<partition_numbers.size(); i++)
177 short p=partition_numbers[i];
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;
197 stack.push(
entryt(output, &dest));
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 ...
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)