Bv circuit automata eval analysis improvements (#1003)

opencompl · Feb 7, 2025 · 0f4de5f · 0f4de5f
1 parent d5d4f38
commit 0f4de5f
Show file tree

Hide file tree

Showing 2 changed files with 27 additions and 6 deletions.
diff --git a/SSA/Projects/InstCombine/TacticAuto.lean b/SSA/Projects/InstCombine/TacticAuto.lean
@@ -308,7 +308,7 @@ macro "bv_bench": tactic =>
             "bv_ring" : (bv_ring; done),
             "bv_of_bool" : (bv_of_bool; done),
             "bv_omega" : (bv_omega; done),
-            -- Automata, Classic.
+            -- Automata Classic
             "bv_automata_classic_prop" : (bool_to_prop; bv_automata_classic; done),
             "bv_automata_classic" : (bv_automata_classic; done),
             "bv_normalize_automata_classic" : ((try (solve | bv_normalize)); (try bv_automata_classic); done),
@@ -347,7 +347,9 @@ macro "bv_bench_automata": tactic =>
         all_goals (
           tac_bench (config := { outputType := .csv }) [
             "presburger" : (bv_automata_classic; done),
-            "circuit" : (bv_automata_circuit (config := { backend := .cadical 0 }); done),
+            "normPresburger" : ((try (solve | bv_normalize)); (try bv_automata_classic); done),
+            "circuit" : (bv_automata_circuit (config := { backend := .cadical /- maxIter -/ 4 }); done),
+            "normCircuit" : ((try (solve | bv_normalize); (try bv_automata_circuit (config := { backend := .cadical /- maxIter -/ 4 })); done)),
             "no_uninterpreted" : (bv_automata_fragment_no_uninterpreted),
             "width_ok" : (bv_automata_fragment_width_legal),
             "reflect_ok" : (bv_automata_fragment_reflect),

diff --git a/bv-evaluation/compare-automata-automata-circuit.py b/bv-evaluation/compare-automata-automata-circuit.py
@@ -177,8 +177,8 @@ def setup_logging(db_name : str):
         format='%(asctime)s - %(levelname)s - %(message)s',
         handlers=[logging.FileHandler(f'{db_name}.log', mode='a'), logging.StreamHandler()])
 
-def analyze_uninterpreted_functions(cur : sqlite3.Cursor):
-    """Tabulate all uninterpreted functions"""
+def analyze_errors(cur : sqlite3.Cursor):
+    """Tabulate all errors and catalogue them"""
     logging.info("Analyzing uninterpreted functions")
     rows = cur.execute("""
         SELECT fileTitle, thmName, goalStr, errMsg FROM tests WHERE tactic = "circuit" AND status = "err"
@@ -190,6 +190,7 @@ def analyze_uninterpreted_functions(cur : sqlite3.Cursor):
     KEY_SYMBOLIC_SHIFT_LEFT = "expected shiftLeft by natural number  found symbolic shift amount"
     KEY_UNKNOWN_BOOLEAN_EQUALITY = "only boolean conditionals allowed are 'bv.slt bv = true'  'bv.sle bv = true'. Found"
     KEY_UNKNOWN_BOOLEAN_DISEQUALITY = "Expected typeclass to be 'BitVec w' / 'Nat'  found '   Bool' in"
+    KEY_UNKNOWN = "unknown"
 
     str2explanation = {
       KEY_UNTRUE : "theorems that are established as untrue",
@@ -198,6 +199,7 @@ def analyze_uninterpreted_functions(cur : sqlite3.Cursor):
       KEY_SYMBOLIC_SHIFT_LEFT : "theorems that have symbolic left shift amount",
       KEY_UNKNOWN_BOOLEAN_EQUALITY : "unknown boolean equality",
       KEY_UNKNOWN_BOOLEAN_DISEQUALITY : "unknown boolean disequality",
+      KEY_UNKNOWN : "unknown",
     }
     str2matches = {
       KEY_UNTRUE : [],
@@ -206,11 +208,14 @@ def analyze_uninterpreted_functions(cur : sqlite3.Cursor):
       KEY_SYMBOLIC_SHIFT_LEFT : [],
       KEY_UNKNOWN_BOOLEAN_EQUALITY : [],
       KEY_UNKNOWN_BOOLEAN_DISEQUALITY : [],
+      KEY_UNKNOWN : []
     }
 
 
     HEADERS = ["errMsg", "goalStr", "thmName", "fileTitle"]
     HEADER_COL_WIDTHS = [40, 40, 50, 50]
+
+    unmatched = []
     for row in rows:
         (fileTitle, thmName, goalStr, errMsg) = row
         matched = False
@@ -220,22 +225,36 @@ def analyze_uninterpreted_functions(cur : sqlite3.Cursor):
                 matched = True
                 break
         if not matched:
+            str2matches[KEY_UNKNOWN].append((errMsg, goalStr, thmName, fileTitle))
             print(errMsg)
 
     for s in str2matches:
         NEXAMPLES = 5
-        print(f"{str2explanation[s]} (#{len(str2matches[KEY_UNTRUE])}):")
+        print(f"{str2explanation[s]} (#{len(str2matches[s])}):")
+        if not str2matches[s]: continue
         print(tabulate(str2matches[s][:NEXAMPLES], headers=HEADERS, tablefmt="grid", maxcolwidths=HEADER_COL_WIDTHS))
 
 
+def analyze_uninterpreted_functions(cur : sqlite3.Cursor):
+    """Tabulate all uninterpreted functions"""
+    logging.info("Analyzing uninterpreted functions")
+    rows = cur.execute("""
+        SELECT fileTitle, thmName, goalStr, errMsg FROM tests WHERE tactic = "no_uninterpreted" AND status = "err"
+    """)
+    rows = list(rows)
+    for row in rows:
+        (fileTitle, thmName, goalStr, errMsg) = row
+        print(errMsg)
+    print(f"#problems with uninterpreted functions: {len(rows)}")
+
 # analyze the sqlite db.
 def analyze(db : str):
     con = sqlite3.connect(db)
     cur = con.cursor()
     analyze_uninterpreted_functions(cur)
+    analyze_errors(cur)
     pass
 
-
 if __name__ == "__main__":
   current_time = datetime.datetime.now().strftime('%Y-%m-%d-%H:%M:%S')
   nproc = os.cpu_count()