edits

Author: kuldeepmeel

manthan.py

@@ -156,7 +156,7 @@ def finish(status):
                 cprint("c [manthan] negative unates", NegUnate)
 
         Unates = PosUnate + NegUnate
-        if Unates:
+        if Unates and args.apply_unates == 1:
             qdimacs_list, unsat = _apply_unates_to_qdimacs(
                 qdimacs_list, PosUnate, NegUnate)
             if unsat:
@@ -175,6 +175,9 @@ def finish(status):
                 shutil.copyfile(qdimacs_path, keep_path)
                 if getattr(args, "verbose", 0) >= 1:
                     cprint("c [manthan] saved unate-substituted qdimacs:", keep_path)
+        elif Unates and args.apply_unates == 0:
+            if args.verbose:
+                cprint("c [manthan] unates detected; substitution disabled (--apply-unates=0)")
 
     else:
         Unates = []
@@ -333,7 +336,13 @@ def finish(status):
                 shutil.copyfile(errorformula, last_errorformula_path)
                 cprint("c [manthan] last successful error formula:", last_errorformula_path)
         if check == 0:
-            cprint("c [manthan] error --- ABC network read fail")
+            errorformula = temp_path(temp_stem + "_errorformula.v")
+            if args.debug_keep and not os.path.isfile(errorformula):
+                errorformula = os.path.abspath(temp_stem + "_errorformula.v")
+            cprint("c [manthan] error --- file_generation_cex failed to read error formula")
+            cprint("c [manthan] errorformula:", errorformula)
+            if not args.verbose:
+                cprint("c [manthan] hint: rerun with --verb=1 to see ABC stderr")
             status = "failed"
             break
         if ret == 0:
@@ -442,6 +451,15 @@ def finish(status):
         choices=[0, 1],
         help="enable preprocess: 1; disable: 0; default 1",
     )
+    parser.add_argument(
+        "--apply-unates",
+        nargs="?",
+        const=1,
+        default=1,
+        type=int,
+        choices=[0, 1],
+        help="substitute unates into the spec: 1; disable substitution: 0; default 1",
+    )
     parser.add_argument(
         "--multiclass",
         nargs="?",

src/repair.py

@@ -433,6 +433,9 @@ def repair(repaircnf, ind, Xvar, Yvar, YvarOrder, UniqueVars, Unates, sigma, inp
             repaired.append(repairvar)
             if args.verbose:
                 cprint("c [repair] gk formula is UNSAT; creating beta formula")
+            if not any(abs(lit) == repairvar for lit in clisty):
+                cprint("c [repair] repaired literal %s missing in core; returning early" % repairvar)
+                return 0, repairfunctions
 
             beta_terms = []
             for x_lit in clistx:
@@ -460,12 +463,7 @@ def repair(repaircnf, ind, Xvar, Yvar, YvarOrder, UniqueVars, Unates, sigma, inp
                 if y_lit < 0:
                     beta_terms.append("~o%s" % (y))
                 else:
-                    beta_terms.append("o%s" % (y))
-
-            if not any(abs(lit) == repairvar for lit in clisty):
-                if args.verbose:
-                    cprint("c [repair] repaired literal %s missing in core; proceeding with core-based repair" % repairvar)
-            
+                    beta_terms.append("o%s" % (y))            
             if args.verbose >= 2:
                 cprint("c [repair] Repair function for w%s: %s" % (repairvar, " & ".join(beta_terms)))
             repairfunctions[repairvar] = " & ".join(beta_terms) if beta_terms else "1'b1"