Report of Errors while testing Manthan on certain benchmark(s)

[Rkus990]

Below is a report of errors encountered while testing Manthan for certain benchmarks (these benchmarks are not reported in beyond-manthan.txt)

1. Factorization8 benchmark: (factorization8_skolem.v file generated could not be read by ABC)

python3 manthan.py ./benchmarks/Factorization/qdimacs/factorization8.qdimacs
c configuring dependency paths
c Did not install dependencies from source code, using precomplied binaries
c starting Manthan
c parsing
c count X (universally quantified variables) variables 8
c count Y (existentially quantified variables) variables 87
c preprocessing: finding unates (constant functions)
c count of positive unates 11
c count of negative unates 8
c finding uniquely defined functions
c count of uniquely defined variables 59
c generating samples
c generated samples.. learning candidate functions via decision learning
c generated candidate functions for all variables.
c verification check UNSAT
c no more repair needed
c number of repairs needed to converge 98
c Total time taken 5.730388402938843
Skolem functions are stored at factorization8_skolem.v

---

Reading factorization8_skolem.v with abc:
abc 01> read ./factorization8_skolem.v
./factorization8_skolem.v (line 1281): Parse_FormulaParser(): Incorrect state.
Reading network from file has failed.

---

2. Factorization10 benchmark: (factorization10_skolem.v file generated could not be read by ABC)

python3 manthan.py ./benchmarks/Factorization/qdimacs/factorization10.qdimacs
c configuring dependency paths
c Did not install dependencies from source code, using precomplied binaries
c starting Manthan
c parsing
c count X (universally quantified variables) variables 10
c count Y (existentially quantified variables) variables 141
c preprocessing: finding unates (constant functions)
c count of positive unates 13
c count of negative unates 11
c finding uniquely defined functions
c count of uniquely defined variables 106
c generating samples
c generated samples.. learning candidate functions via decision learning
c generated candidate functions for all variables.
c verification check UNSAT
c no more repair needed
c number of repairs needed to converge 565
c Total time taken 36.33930587768555
Skolem functions are stored at factorization10_skolem.v

---

Reading factorization10_skolem.v with abc:

abc 01> read ./factorization10_skolem.v
./factorization10_skolem.v (line 4015): Parse_FormulaParser(): Incorrect state.
Reading network from file has failed.

---

3. Factorization12 benchmark: (factorization12_skolem.v file was not generated.)

python3 manthan.py ./benchmarks/Factorization/qdimacs/factorization12.qdimacs
c configuring dependency paths
c Did not install dependencies from source code, using precomplied binaries
c starting Manthan
c parsing
c count X (universally quantified variables) variables 12
c count Y (existentially quantified variables) variables 207
c preprocessing: finding unates (constant functions)
c count of positive unates 15
c count of negative unates 14
c finding uniquely defined functions
c count of uniquely defined variables 165
c generating samples
c generated samples.. learning candidate functions via decision learning
c generated candidate functions for all variables.
c error --- ABC network read fail

---

4. Factorization14 benchmark: (factorization14_skolem.v file was not generated.)

Run1: (ABC network read fail)
python3 manthan.py ./benchmarks/Factorization/qdimacs/factorization14.qdimacs
c configuring dependency paths
c Did not install dependencies from source code, using precomplied binaries
c starting Manthan
c parsing
c count X (universally quantified variables) variables 14
c count Y (existentially quantified variables) variables 281
c preprocessing: finding unates (constant functions)
c count of positive unates 19
c count of negative unates 12
c finding uniquely defined functions
c count of uniquely defined variables 235
c generating samples
c generated samples.. learning candidate functions via decision learning
c generated candidate functions for all variables.
c error --- ABC network read fail

Run 2: (No synthesis) (perhaps due to default maxrepairiter = 5000?)
python3 manthan.py benchmarks/factorization14.qdimacs
c configuring dependency paths
c Did not install dependencies from source code, using precomplied binaries
c starting Manthan
c parsing
c count X (universally quantified variables) variables 14
c count Y (existentially quantified variables) variables 281
c preprocessing: finding unates (constant functions)
c count of positive unates 19
c count of negative unates 12
c finding uniquely defined functions
c count of uniquely defined variables 235
c generating samples
c generated samples.. learning candidate functions via decision learning
c generated candidate functions for all variables.
c number of maximum allowed repair iteration reached
c could not synthesize functions

---

5. decomposition32 benchmark (decomposition32_skolem.v file generated could not read by ABC.)

Run1: Default run: does not synthesize function.

python3 manthan.py ./benchmarks/Arithmetic/qdimacs/decomposition32.qdimacs --logtime
c configuring dependency paths
c Did not install dependencies from source code, using precomplied binaries
c starting Manthan
c parsing
c count X (universally quantified variables) variables 32
c count Y (existentially quantified variables) variables 253
c preprocessing: finding unates (constant functions)
c count of positive unates 33
c count of negative unates 32
c finding uniquely defined functions
c count of uniquely defined variables 125
c generating samples
c generated samples.. learning candidate functions via decision learning
c generated candidate functions for all variables.
c number of maximum allowed repair iteration reached
c could not synthesize functions

---

preprocessing time:0.048201799392700195
unique function finding:0.05613422393798828
generating samples:1.6961398124694824
candidate learning:2.9643406867980957
repair time:1223.5683856010437
totaltime:1228.3410036563873

---

Run2: Change maxrepairiter 14000 (this is since 5000 repairs took ~20.5 min; doing so for <=1 hr timeout) synthesizes skolem function but decomposition32_skolem.v file so generated could not read by ABC.
python3 manthan.py ./benchmarks/Arithmetic/qdimacs/decomposition32.qdimacs --logtime --maxrepairitr 14000
c configuring dependency paths
c Did not install dependencies from source code, using precomplied binaries
c starting Manthan
c parsing
c count X (universally quantified variables) variables 32
c count Y (existentially quantified variables) variables 253
c preprocessing: finding unates (constant functions)
c count of positive unates 33
c count of negative unates 32
c finding uniquely defined functions
c count of uniquely defined variables 125
c generating samples
c generated samples.. learning candidate functions via decision learning
c generated candidate functions for all variables.
c verification check UNSAT
c no more repair needed
c number of repairs needed to converge 6043
c Total time taken 1729.755434513092
Skolem functions are stored at decomposition32_skolem.v

---

preprocessing time:0.0914618968963623
unique function finding:0.056552886962890625
generating samples:1.7441890239715576
candidate learning:3.01041579246521
repair time:1724.8438985347748
totaltime:1729.75546336174

---

Error reading decomposition32_skolem.v with abc:

abc 11> read ./decomposition32_skolem.v
./decomposition32_skolem.v (line 43390): Parse_FormulaParser(): Incorrect state.
Reading network from file has failed.

---

6. decomposition64 benchmark (Timeout, decomposition64_skolem.v file was not generated, ABC network read fail error after ~4 hrs)

python3 manthan.py ./benchmarks/Arithmetic/qdimacs/decomposition64.qdimacs --logtime --maxrepairitr 14000
c configuring dependency paths
c Did not install dependencies from source code, using precomplied binaries
c starting Manthan
c parsing
c count X (universally quantified variables) variables 64
c count Y (existentially quantified variables) variables 508
c preprocessing: finding unates (constant functions)
c count of positive unates 64
c count of negative unates 64
c finding uniquely defined functions
c count of uniquely defined variables 253
c generating samples
c generated samples.. learning candidate functions via decision learning
c generated candidate functions for all variables.
c error --- ABC network read fail

---

preprocessing time:0.3454887866973877
unique function finding:0.1925520896911621
generating samples:3.4857187271118164
candidate learning:12.828465461730957
repair time:13836.111461639404
totaltime:13852.98039317131

---

7. small-swap1-fixpoint4 benchmark (small-swap1-fixpoint4_skolem.v file was not generated.)

python3 manthan.py ./benchmarks/QBFEval2017/qdimacs/small-swap1-fixpoint-4.qdimacs --logtime --maxrepairitr 14000
c configuring dependency paths
c Did not install dependencies from source code, using precomplied binaries
c starting Manthan
c parsing
c count X (universally quantified variables) variables 300
c count Y (existentially quantified variables) variables 954
c preprocessing: finding unates (constant functions)
c count of positive unates 0
c count of negative unates 0
c finding uniquely defined functions
c count of uniquely defined variables 714
c generating samples
c generated samples.. learning candidate functions via decision learning
c generated candidate functions for all variables.
c number of maximum allowed repair iteration reached
c could not synthesize functions

---

preprocessing time:1.0780119895935059
unique function finding:0.9673247337341309
generating samples:8.07258939743042
candidate learning:36.9544894695282
repair time:615.6708221435547
totaltime:662.7883698940277

---

8. sortnetsort7.AE.stepl.005 benchmark (sortnetsort7.AE.stepl.005_skolem.v file was not generated)

python3 manthan.py ./benchmarks/QBFEval2017/qdimacs/sortnetsort7.AE.stepl.005.qdimacs --logtime --maxrepairitr 14000
c configuring dependency paths
c Did not install dependencies from source code, using precomplied binaries
c starting Manthan
c parsing
c count X (universally quantified variables) variables 405
c count Y (existentially quantified variables) variables 1845
c preprocessing: finding unates (constant functions)
c count of positive unates 0
c count of negative unates 105
c finding uniquely defined functions
c count of uniquely defined variables 0
c generating samples
c generated samples.. learning candidate functions via decision learning
c generated candidate functions for all variables.
c error --- ABC network read fail

---

preprocessing time:2.5354599952697754
unique function finding:5.829728126525879
generating samples:12.975327491760254
candidate learning:684.209431886673
repair time:2030.659107208252
totaltime:2736.2568933963776

---

Further, all the benchmarks are tested on the machine having following specs:

System Specs summary:

Architecture: x86_64
CPU op-mode(s): 32-bit, 64-bit
Byte Order: Little Endian
Address sizes: 39 bits physical, 48 bits virtual
CPU(s): 12
On-line CPU(s) list: 0-11
Thread(s) per core: 2
Core(s) per socket: 6
Socket(s): 1
NUMA node(s): 1
Vendor ID: GenuineIntel
CPU family: 6
Model: 158
Model name: Intel(R) Core(TM) i7-8700 CPU @ 3.20GHz
Stepping: 10
CPU MHz: 4371.694
CPU max MHz: 4600.0000
CPU min MHz: 800.0000
BogoMIPS: 6399.96

---

Distributor ID: Ubuntu
Description: Ubuntu 20.04.6 LTS

---

RAM:

              total        used        free      shared  buff/cache   available
Mem:             31Gi        19Gi        8.3Gi      1.0Gi  3.1Gi   9.9Gi
Swap:             29Gi        3.7Gi        26Gi      

---

Attachments:

factorization8.qdimacs.txt
factorization10.qdimacs.txt
factorization12.qdimacs.txt
factorization14.qdimacs.txt
decomposition32.qdimacs.txt
decomposition64.qdimacs.txt
small-swap1-fixpoint-4.qdimacs.txt
sortnetsort7.AE.stepl.005.qdimacs.txt
factorization8_skolem.v.txt
factorization10_skolem.v.txt
decomposition32_skolem.v.txt
beyond-manthan.txt