16 #define USE_AIG_COMPACT 29 literal=
land(*it, literal);
41 literal=
land(
neg(*it), literal);
51 literal=
lxor(*it, literal);
134 #ifdef USE_AIG_COMPACT 149 return solver.l_get(a);
154 status() <<
"converting AIG, " 155 << aig.nodes.size() <<
" nodes" <<
eom;
158 return solver.prop_solve();
165 std::vector<bool> &n_pos,
166 std::vector<bool> &n_neg)
168 std::stack<literalt> queue;
171 for(aig_plus_constraintst::constraintst::const_iterator
172 c_it=aig.constraints.begin();
173 c_it!=aig.constraints.end();
177 while(!queue.empty())
186 unsigned var_no=l.
var_no();
189 if(sign?n_neg[var_no]:n_pos[var_no])
193 sign?n_neg[var_no]=1:n_pos[var_no]=1;
199 queue.push(node.
a^sign);
200 queue.push(node.
b^sign);
205 unsigned pos_only=0, neg_only=0, mixed=0;
207 for(
unsigned n=0; n<aig.nodes.size(); n++)
209 if(aig.nodes[n].is_and())
211 if(n_neg[n] && n_pos[n])
220 statistics() <<
"Pos only: " << pos_only <<
"\n" 221 <<
"Neg only: " << neg_only <<
"\n" 222 <<
"Mixed: " << mixed <<
eom;
230 std::vector<unsigned> &p_usage_count,
231 std::vector<unsigned> &n_usage_count)
233 for(aig_plus_constraintst::constraintst::const_iterator
234 c_it=aig.constraints.begin();
235 c_it!=aig.constraints.end();
238 if(!((*c_it).is_constant()))
242 ++n_usage_count[(*c_it).var_no()];
246 ++p_usage_count[(*c_it).var_no()];
251 for(
unsigned n=0; n<aig.nodes.size(); n++)
259 ++n_usage_count[node.
a.
var_no()];
263 ++p_usage_count[node.
a.
var_no()];
268 ++n_usage_count[node.
b.
var_no()];
272 ++p_usage_count[node.
b.
var_no()];
281 unsigned usedOncePositive=0;
282 unsigned usedOnceNegative=0;
283 unsigned usedTwicePositive=0;
284 unsigned usedTwiceNegative=0;
285 unsigned usedTwiceMixed=0;
286 unsigned usedThreeTimes=0;
289 for(
unsigned n=0; n<aig.nodes.size(); n++)
291 switch(p_usage_count[n] + n_usage_count[n])
293 case 0: ++unused;
break;
295 if(p_usage_count[n]==1)
302 if(p_usage_count[n]>=2)
306 else if(n_usage_count[n]>=2)
312 assert(p_usage_count[n]==1 && n_usage_count[n]==1);
316 case 3: ++usedThreeTimes;
break;
317 default: ++usedMore;
break;
322 <<
"Used once: " << usedOncePositive + usedOnceNegative
323 <<
" (P: " << usedOncePositive
324 <<
", N: " << usedOnceNegative <<
") " 326 << usedTwicePositive + usedTwiceNegative + usedTwiceMixed
327 <<
" (P: " << usedTwicePositive
328 <<
", N: " << usedTwiceNegative
329 <<
", M: " << usedTwiceMixed <<
") " 330 <<
"Used three times: " << usedThreeTimes <<
" " 331 <<
"Used more: " << usedMore
343 bool n_pos,
bool n_neg,
344 std::vector<unsigned> &p_usage_count,
345 std::vector<unsigned> &n_usage_count)
347 if(p_usage_count[n]>0 || n_usage_count[n]>0)
354 #ifdef USE_AIG_COMPACT 363 aig.nodes[l.
var_no()].is_and() &&
364 p_usage_count[l.
var_no()] == 1 &&
365 n_usage_count[l.
var_no()] == 0)
369 body.push_back(rep.
b);
371 --p_usage_count[l.
var_no()];
394 if(body.size() == 2 && body[0].sign() && body[1].sign())
396 const aigt::nodet &left=aig.nodes[body[0].var_no()];
397 const aigt::nodet &right=aig.nodes[body[1].var_no()];
401 if(left.
a==
neg(right.
a))
403 if(p_usage_count[body[0].var_no()]==0 &&
404 n_usage_count[body[0].var_no()]==1 &&
405 p_usage_count[body[1].var_no()]==0 &&
406 n_usage_count[body[1].var_no()]==1)
426 lits[1]=
neg(right.
b);
437 --n_usage_count[body[0].var_no()];
438 --n_usage_count[body[1].var_no()];
449 if(body.size() == 3 && body[0].sign() && body[1].sign() && body[2].sign())
451 const aigt::nodet &left=aig.nodes[body[0].var_no()];
452 const aigt::nodet &mid=aig.nodes[body[1].var_no()];
453 const aigt::nodet &right=aig.nodes[body[2].var_no()];
457 if(p_usage_count[body[0].var_no()]==0 &&
458 n_usage_count[body[0].var_no()]==1 &&
459 p_usage_count[body[1].var_no()]==0 &&
460 n_usage_count[body[1].var_no()]==1 &&
461 p_usage_count[body[2].var_no()]==0 &&
462 n_usage_count[body[2].var_no()]==1)
468 if(a==right.
b && b==mid.
b && c==right.
a)
510 --n_usage_count[body[0].var_no()];
511 --n_usage_count[body[1].var_no()];
512 --n_usage_count[body[2].var_no()];
543 lits.push_back(
neg(*it));
545 lits.push_back(
pos(o));
554 while(solver.no_variables()<=aig.nodes.size())
555 solver.new_variable();
559 std::vector<unsigned> p_usage_count;
560 std::vector<unsigned> n_usage_count;
561 p_usage_count.resize(aig.nodes.size(), 0);
562 n_usage_count.resize(aig.nodes.size(), 0);
564 this->usage_count(p_usage_count, n_usage_count);
569 std::vector<bool> n_pos, n_neg;
570 n_pos.resize(aig.nodes.size(),
false);
571 n_neg.resize(aig.nodes.size(),
false);
573 this->compute_phase(n_pos, n_neg);
577 for(std::size_t n=aig.nodes.size() - 1; n!=0; n--)
579 if(aig.nodes[n].is_and())
583 n, aig.nodes[n], n_pos[n], n_neg[n], p_usage_count, n_usage_count);
585 convert_node(n, aig.nodes[n],
true,
true, p_usage_count, n_usage_count);
593 for(
const auto &c_it : aig.constraints)
594 solver.l_set_to(c_it,
true);
literalt land(literalt a, literalt b) override
literalt lnor(literalt a, literalt b) override
resultt prop_solve() override
literalt lxor(literalt a, literalt b) override
void set_equal(literalt a, literalt b) override
asserts a==b in the propositional formula
unsignedbv_typet size_type()
static mstreamt & eom(mstreamt &m)
#define forall_literals(it, bv)
void l_set_to_true(literalt a)
literalt lnand(literalt a, literalt b) override
literalt new_and_node(literalt a, literalt b)
literalt lselect(literalt a, literalt b, literalt c) override
literalt lequal(literalt a, literalt b) override
literalt const_literal(bool value)
void convert_node(unsigned n, const aigt::nodet &node, bool n_pos, bool n_neg, std::vector< unsigned > &p_usage_count, std::vector< unsigned > &n_usage_count)
Convert one AIG node, including special handling of a couple of cases.
void usage_count(std::vector< unsigned > &p_usage_count, std::vector< unsigned > &n_usage_count)
Compact encoding for single usage variable.
void compute_phase(std::vector< bool > &n_pos, std::vector< bool > &n_neg)
Compute the phase information needed for Plaisted-Greenbaum encoding.
tvt l_get(literalt a) const override
literalt limplies(literalt a, literalt b) override
literalt lor(literalt a, literalt b) override
std::vector< literalt > bvt