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 154 status() <<
"converting AIG, " 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
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++)
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
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 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())
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())
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));
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);
569 std::vector<bool> n_pos, n_neg;
570 n_pos.resize(
aig.
nodes.size(),
false);
571 n_neg.resize(
aig.
nodes.size(),
false);
577 for(std::size_t n=
aig.
nodes.size() - 1; n!=0; n--)
583 n,
aig.
nodes[n], n_pos[n], n_neg[n], p_usage_count, n_usage_count);
literalt land(literalt a, literalt b) override
literalt lnor(literalt a, literalt b) override
resultt prop_solve() override
void lcnf(literalt l0, literalt l1)
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)
virtual literalt new_variable()=0
literalt lnand(literalt a, literalt b) override
virtual void l_set_to(literalt a, bool value)
literalt new_and_node(literalt a, literalt b)
virtual size_t no_variables() const =0
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.
virtual tvt l_get(literalt a) const =0
virtual resultt prop_solve()=0
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
aig_plus_constraintst aig
std::vector< literalt > bvt