Merge pull request #4078 from jix/smtbmc-cexenum-support

Improvements to smtbmc/witness to support counter-example enumeration

backends/smt2/smtbmc.py

@@ -1327,6 +1327,9 @@ def write_yw_trace(steps, index, allregs=False, filename=None):
                 sig = yw.add_sig(word_path, overlap_start, overlap_end - overlap_start, True)
                 mem_init_values.append((sig, overlap_bits.replace("x", "?")))
 
+        exprs = []
+        all_sigs = []
+
         for i, k in enumerate(steps):
             step_values = WitnessValues()
 
@@ -1337,8 +1340,15 @@ def write_yw_trace(steps, index, allregs=False, filename=None):
             else:
                 sigs = seqs
 
+            exprs.extend(smt.witness_net_expr(topmod, f"s{k}", sig) for sig in sigs)
+
+            all_sigs.append(sigs)
+
+        bvs = iter(smt.get_list(exprs))
+
+        for sigs in all_sigs:
             for sig in sigs:
-                value = smt.bv2bin(smt.get(smt.witness_net_expr(topmod, f"s{k}", sig)))
+                value = smt.bv2bin(next(bvs))
                 step_values[sig["sig"]] = value
             yw.step(step_values)
 

backends/smt2/smtbmc_incremental.py

@@ -194,9 +194,31 @@ class Incremental:
 
         return "Bool"
 
+    def expr_smtlib(self, expr, smt_out):
+        self.expr_arg_len(expr, 2)
+
+        smtlib_expr = expr[1]
+        sort = expr[2]
+
+        if not isinstance(smtlib_expr, str):
+            raise InteractiveError(
+                "raw SMT-LIB expression has to be a string, "
+                f"got {json.dumps(smtlib_expr)}"
+            )
+
+        if not isinstance(sort, str):
+            raise InteractiveError(
+                f"raw SMT-LIB sort has to be a string, got {json.dumps(sort)}"
+            )
+
+        smt_out.append(smtlib_expr)
+        return sort
+
     def expr_label(self, expr, smt_out):
         if len(expr) != 3:
-            raise InteractiveError(f'expected ["!", label, sub_expr], got {expr!r}')
+            raise InteractiveError(
+                f'expected ["!", label, sub_expr], got {json.dumps(expr)}'
+            )
         label = expr[1]
         subexpr = expr[2]
 
@@ -226,6 +248,7 @@ class Incremental:
         "or": expr_andor,
         "=": expr_eq,
         "yw": expr_yw,
+        "smtlib": expr_smtlib,
         "!": expr_label,
     }
 
@@ -251,7 +274,8 @@ class Incremental:
                         )
                     ):
                         raise InteractiveError(
-                            f"required sort {json.dumps(required_sort)} found sort {json.dumps(sort)}"
+                            f"required sort {json.dumps(required_sort)} "
+                            f"found sort {json.dumps(sort)}"
                         )
             return sort
         raise InteractiveError(f"unknown expression {json.dumps(expr[0])}")
@@ -287,6 +311,14 @@ class Incremental:
     def cmd_check(self, cmd):
         return smtbmc.smt_check_sat()
 
+    def cmd_smtlib(self, cmd):
+        command = cmd.get("command")
+        if not isinstance(command, str):
+            raise InteractiveError(
+                f"raw SMT-LIB command must be a string, found {json.dumps(command)}"
+            )
+        smtbmc.smt.write(command)
+
     def cmd_design_hierwitness(self, cmd=None):
         allregs = (cmd is None) or bool(cmd.get("allreges", False))
         if self._cached_hierwitness[allregs] is not None:
@@ -326,13 +358,17 @@ class Incremental:
 
         map_steps = {i: int(j) for i, j in enumerate(steps)}
 
-        smtbmc.ywfile_constraints(path, constraints, map_steps=map_steps, skip_x=skip_x)
+        last_step = smtbmc.ywfile_constraints(
+            path, constraints, map_steps=map_steps, skip_x=skip_x
+        )
 
         self._yw_constraints[name] = {
             map_steps.get(i, i): [smtexpr for cexfile, smtexpr in constraint_list]
             for i, constraint_list in constraints.items()
         }
 
+        return dict(last_step=last_step)
+
     def cmd_ping(self, cmd):
         return cmd
 
@@ -344,6 +380,7 @@ class Incremental:
         "push": cmd_push,
         "pop": cmd_pop,
         "check": cmd_check,
+        "smtlib": cmd_smtlib,
         "design_hierwitness": cmd_design_hierwitness,
         "write_yw_trace": cmd_write_yw_trace,
         "read_yw_trace": cmd_read_yw_trace,

backends/smt2/witness.py

@@ -183,7 +183,8 @@ This requires a Yosys witness AIGER map file as generated by 'write_aiger -ywmap
 @click.argument("mapfile", type=click.File("r"))
 @click.argument("output", type=click.File("w"))
 @click.option("--skip-x", help="Leave input x bits unassigned.", is_flag=True)
-def aiw2yw(input, mapfile, output, skip_x):
+@click.option("--present-only", help="Only include bits present in at least one time step.", is_flag=True)
+def aiw2yw(input, mapfile, output, skip_x, present_only):
     input_name = input.name
     click.echo(f"Converting AIGER witness trace {input_name!r} to Yosys witness trace {output.name!r}...")
     click.echo(f"Using Yosys witness AIGER map file {mapfile.name!r}")
@@ -211,16 +212,23 @@ def aiw2yw(input, mapfile, output, skip_x):
     if not re.match(r'[0]*$', ffline):
         raise click.ClickException(f"{input_name}: non-default initial state not supported")
 
-    outyw = WriteWitness(output, 'yosys-witness aiw2yw')
+    if not present_only:
+        outyw = WriteWitness(output, "yosys-witness aiw2yw")
 
-    for clock in aiger_map.clocks:
-        outyw.add_clock(clock["path"], clock["offset"], clock["edge"])
+        for clock in aiger_map.clocks:
+            outyw.add_clock(clock["path"], clock["offset"], clock["edge"])
 
-    for (path, offset), id in aiger_map.sigmap.bit_to_id.items():
-        outyw.add_sig(path, offset, init_only=id in aiger_map.init_inputs)
+        for (path, offset), id in aiger_map.sigmap.bit_to_id.items():
+            outyw.add_sig(path, offset, init_only=id in aiger_map.init_inputs)
 
     missing = set()
+    seen = set()
 
+    buffered_steps = []
+
+    skip = "x?" if skip_x else "?"
+
+    t = -1
     while True:
         inline = next(input, None)
         if inline is None:
@@ -232,17 +240,20 @@ def aiw2yw(input, mapfile, output, skip_x):
         if inline.startswith("#"):
             continue
 
-        if not re.match(r'[01x]*$', ffline):
+        t += 1
+
+        if not re.match(r"[01x]*$", inline):
             raise click.ClickException(f"{input_name}: unexpected data in AIGER witness file")
 
         if len(inline) != aiger_map.input_count:
             raise click.ClickException(
-                    f"{input_name}: {mapfile.name}: number of inputs does not match, "
-                    f"{len(inline)} in witness, {aiger_map.input_count} in map file")
+                f"{input_name}: {mapfile.name}: number of inputs does not match, "
+                f"{len(inline)} in witness, {aiger_map.input_count} in map file"
+            )
 
         values = WitnessValues()
         for i, v in enumerate(inline):
-            if outyw.t > 0 and i in aiger_map.init_inputs:
+            if v in skip or (t > 0 and i in aiger_map.init_inputs):
                 continue
 
             try:
@@ -250,11 +261,29 @@ def aiw2yw(input, mapfile, output, skip_x):
             except IndexError:
                 bit = None
             if bit is None:
-                missing.insert(i)
+                missing.add(i)
+            elif present_only:
+                seen.add(i)
 
             values[bit] = v
 
-        outyw.step(values, skip_x=skip_x)
+        if present_only:
+            buffered_steps.append(values)
+        else:
+            outyw.step(values)
+
+    if present_only:
+        outyw = WriteWitness(output, "yosys-witness aiw2yw")
+
+        for clock in aiger_map.clocks:
+            outyw.add_clock(clock["path"], clock["offset"], clock["edge"])
+
+        for (path, offset), id in aiger_map.sigmap.bit_to_id.items():
+            if id in seen:
+                outyw.add_sig(path, offset, init_only=id in aiger_map.init_inputs)
+
+        for values in buffered_steps:
+            outyw.step(values)
 
     outyw.end_trace()