Branch more during container size realization

Author: pschanely

crosshair/libimpl/builtinslib.py

@@ -1411,6 +1411,13 @@ def __gt__(self, other):
                     )
         return ret
 
+    def __ch_realize__(self) -> object:
+        # TODO: Bisect-search with small bounded ranges?
+        choice_conformity = (
+            1.0 if self._ch_minimum is None and self._ch_maximum is None else 0.9
+        )
+        return context_statespace().find_model_value(self.var, choice_conformity)
+
     def _ch_intersect_bounds(
         self, new_min: Optional[int], new_max: Optional[int]
     ) -> None:

crosshair/libimpl/builtinslib_test.py

@@ -10,6 +10,7 @@
 import sys
 from abc import ABC, abstractmethod
 from array import array
+from bisect import bisect_left
 from numbers import Integral
 from typing import (
     Callable,
@@ -1778,6 +1779,22 @@ def f(ls: List[int], i: int) -> List[int]:
     check_states(f, CONFIRMED)
 
 
+def test_list_can_realize_nonzero_length_without_exhausting_other_paths() -> None:
+    def f(x: int, ls: List[int]) -> list[int]:
+        """
+        post: len(_) < 5
+        """
+        lslen = len(ls)
+        with NoTracing():
+            realize(lslen)
+
+        haystack = list(range(1000))
+        y = bisect_left(haystack, x)
+        return ls
+
+    check_states(f, POST_FAIL)
+
+
 def test_list_range_fail() -> None:
     def f(ls: List[int]) -> List[int]:
         """

crosshair/libimpl/datetimelib_ch_test.py

@@ -181,6 +181,11 @@ def check_date_ctime(dt: date) -> ResultComparison:
 
 def check_date_strftime(dt: date, fmt: str) -> ResultComparison:
     """post: _"""
+    # not using skipIf because this is invoked via `test_builtin`:
+    if sys.version_info < (3, 13):
+        # strftime null character handling aligned between python and C
+        # implementations in https://github.com/python/cpython/pull/125657
+        return True
     return compare_results(_invoker("strftime"), dt, fmt)
 
 
@@ -303,6 +308,11 @@ def check_time_isoformat(tm: time) -> ResultComparison:
 
 def check_time_strftime(tm: time, fmt: str) -> ResultComparison:
     """post: _"""
+    # not using skipIf because this is invoked via `test_builtin`:
+    if sys.version_info < (3, 13):
+        # strftime null character handling aligned between python and C
+        # implementations in https://github.com/python/cpython/pull/125657
+        return True
     return compare_results(_invoker("strftime"), tm, fmt)
 
 

crosshair/statespace.py

@@ -962,7 +962,7 @@ def raise_not_deterministic(
         else:
             raise exc
 
-    def find_model_value(self, expr: z3.ExprRef) -> Any:
+    def find_model_value(self, expr: z3.ExprRef, choice_conformity=1.0) -> Any:
         with NoTracing():
             while True:
                 if isinstance(self._search_position, NodeStem):
@@ -980,7 +980,9 @@ def find_model_value(self, expr: z3.ExprRef) -> Any:
                     debug("  Traceback: ", ch_stack())
                     debug(" *** End Not Deterministic Debug *** ")
                     raise NotDeterministic
-                (chosen, _, next_node) = node.choose(self, probability_true=1.0)
+                (chosen, _, next_node) = node.choose(
+                    self, probability_true=choice_conformity
+                )
                 self.choices_made.append(node)
                 self._search_position = next_node
                 if chosen: