Inconsistent result between cec and &cec
mht208 opened this issue · 2 comments
I have two aig files, a.aig and b.aig, translated from two BTOR (a format used by the SMT solver Boolector) files. The files can be found in abc9_miter_ce.zip. The two files show the associativity of bit-vector addition over 2-bit variables under the same constraint. The two aig files are supposed to be equivalent.
Correct result is obtained using cec.
abc 01> cec a.aig b.aig
Networks are equivalent. Time = 0.03 sec
But &cec produces a different result.
abc 01> &cec a.aig b.aig
Disproved at least one output of the miter (zero-based number 0).
Networks are NOT EQUIVALENT. Time = 0.00 sec
I also construct two miters from a.aig and b.aig. The first miter (miter.aig) is constructed by miter a.aig b.aig; write_aiger miter.aig. The second miter (miter_abc9.aig) is constructed by &r a.aig; &miter b.aig; &write miter_abc9.aig. Using iprove, miter.aig is unsat while miter_abc9.aig is sat.
abc 01> read miter.aig
abc 02> iprove
UNSATISFIABLE Time = 0.03 sec
abc 03> read miter_abc9.aig
abc 04> iprove
SATISFIABLE (output = 0) Time = 0.00 sec
Using &cec separately on miter.aig and miter_abc9.aig, the first one is equivalent while the second one is not equivalent.
abc 01> &r miter.aig
abc 01> &cec -m
Assuming the current network is a single-output miter.
Networks are equivalent. Time = 0.03 sec
abc 01> &r miter_abc9.aig
abc 01> &cec -m
Assuming the current network is a single-output miter.
Disproved at least one output of the miter (zero-based number 0).
Networks are NOT EQUIVALENT. Time = 0.00 sec
Does the inconsistent result come from incorrect usage of abc or probably from &miter?
The inconsistency is because the inputs are ordered differently in a.aig and b.aig. If you normalize the order (e.g. sort by name) both commands would tell you the networks are equivalent.
cec can match PIs either by name or by their order. The default is by name, but it can be changed with -n. &cec can only match PIs by order. It is also the case with miter and &miter.