__call__ notation, new is_* predicates, rename keyword to admit

Author: philzook58

README.md

@@ -41,7 +41,7 @@ assert not isinstance(simple_taut, smt.ExprRef)
 # kd.lemma will throw an error if the theorem is not provable
 try:
     false_lemma = kd.lemma(smt.Implies(p, smt.And(p, q)))
-    assert False # This will not be reached
+    print("This will not be reached")
 except kd.kernel.LemmaError as e:
     pass
 
@@ -58,7 +58,7 @@ or_idem = kd.lemma(smt.ForAll([x], x | x == x))
 # But the point of Knuckledragger is really for the things Z3 can't do in one shot
 
 # Knuckledragger support algebraic datatypes and induction
-Nat = kd.Inductive("Nat", strict=False)
+Nat = kd.Inductive("Nat", admit=True)
 Zero = Nat.declare("Zero")
 Succ = Nat.declare("Succ", ("pred", Nat))
 Nat = Nat.create()

kdrag/config.py

@@ -3,6 +3,7 @@
 """
 
 solver = None
+# admit_enabled = True
 # timeout = 1000
 
 # TODO: Someday, when it is annoyingly slow to check built in theories, we can add a flag to disable them

kdrag/notation.py

@@ -27,6 +27,27 @@
 smt.ArrayRef.__call__ = lambda self, arg: self[arg]
 
 
+def quantifier_call(self, *args):
+    """
+    Instantiate a quantifier. This does substitution
+    >>> x,y = smt.Ints("x y")
+    >>> smt.Lambda([x,y], x + 1)(2,3)
+    2 + 1
+
+    To apply a Lambda without substituting, use square brackets
+    >>> smt.Lambda([x,y], x + 1)[2,3]
+    Select(Lambda([x, y], x + 1), 2, 3)
+    """
+    if self.num_vars() != len(args):
+        raise TypeError("Wrong number of arguments", self, args)
+    return smt.substitute_vars(
+        self.body(), *(smt._py2expr(arg) for arg in reversed(args))
+    )
+
+
+smt.QuantifierRef.__call__ = quantifier_call
+
+
 class SortDispatch:
     """
     Sort dispatch is modeled after functools.singledispatch
@@ -114,6 +135,12 @@ def QForAll(vs: list[smt.ExprRef], *hyp_conc) -> smt.BoolRef:
 
     If variables have a property `wf` attached, this is added as a hypothesis.
 
+    There is no downside to always using this compared to `smt.ForAll` and it can avoid some errors.
+
+    >>> x,y = smt.Ints("x y")
+    >>> QForAll([x,y], x > 0, y > 0, x + y > 0)
+    ForAll([x, y], Implies(And(x > 0, y > 0), x + y > 0))
+
     """
     conc = hyp_conc[-1]
     hyps = hyp_conc[:-1]
@@ -187,13 +214,13 @@ def datatype_call(self, *args):
 records = {}
 
 
-def Record(name: str, *fields, pred=None) -> smt.DatatypeSortRef:
+def Record(name: str, *fields, pred=None, admit=False) -> smt.DatatypeSortRef:
     """
     Define a record datatype.
     The optional argument `pred` will add a well-formedness condition to the record
     giving something akin to a refinement type.
     """
-    if name in records:
+    if not admit and name in records:
         raise Exception("Record already defined", name)
     rec = smt.Datatype(name)
     rec.declare(name, *fields)
@@ -219,9 +246,24 @@ def Record(name: str, *fields, pred=None) -> smt.DatatypeSortRef:
     return rec
 
 
-def NewType(name: str, sort: smt.SortRef, pred=None) -> smt.DatatypeSortRef:
+def NewType(
+    name: str, sort: smt.SortRef, pred=None, admit=False
+) -> smt.DatatypeSortRef:
     """Minimal wrapper around a sort for sort based overloading"""
-    return Record(name, ("val", sort), pred=pred)
+    return Record(name, ("val", sort), pred=pred, admit=admit)
+
+
+def Enum(name, args, admit=False):
+    """Shorthand for simple enumeration datatypes. Similar to python's Enum.
+    >>> Color = Enum("Color", "Red Green Blue")
+    >>> smt.And(Color.Red != Color.Green, Color.Red != Color.Blue)
+    And(Red != Green, Red != Blue)
+    """
+    T = kd.Inductive(name, admit=admit)
+    for c in args.split():
+        T.declare(c)
+    T = T.create()
+    return T
 
 
 def induct_inductive(DT: smt.DatatypeSortRef, x=None, P=None) -> kd.kernel.Proof:
@@ -257,9 +299,9 @@ def induct_inductive(DT: smt.DatatypeSortRef, x=None, P=None) -> kd.kernel.Proof
         )
 
 
-def Inductive(name: str, strict=True) -> smt.DatatypeSortRef:
+def Inductive(name: str, admit=False) -> smt.DatatypeSortRef:
     """Declare datatypes with auto generated induction principles. Wrapper around z3.Datatype"""
-    if strict and name in records:
+    if not admit and name in records:
         raise Exception(
             "Datatype with that name already defined. Use keyword strict=False to override",
             name,
@@ -271,7 +313,7 @@ def Inductive(name: str, strict=True) -> smt.DatatypeSortRef:
     def create():
         dt = oldcreate()
         # Sanity check no duplicate names. Causes confusion.
-        if strict:
+        if not admit:
             names = set()
             for i in range(dt.num_constructors()):
                 cons = dt.constructor(i)
@@ -284,7 +326,6 @@ def create():
                     if n in names:
                         raise Exception("Duplicate field name", n)
                     names.add(n)
-        x = smt.FreshConst(dt, prefix="x")
         kd.notation.induct.register(dt, lambda x: induct_inductive(dt, x=x))
         records[name] = dt
         return dt
@@ -318,6 +359,10 @@ def cond(*cases, default=None) -> smt.ExprRef:
     return acc
 
 
+def conde(*cases):
+    return smt.Or([smt.And(c) for c in cases])
+
+
 class Cond:
     def __init__(self):
         self.cases = []

kdrag/smt.py

@@ -15,6 +15,49 @@
     solver = "z3"
     from z3 import *
 
+    _py2expr = z3.z3._py2expr
+
+    def is_if(x: z3.ExprRef) -> bool:
+        """
+        Check if an expression is an if-then-else.
+        >>> is_if(z3.If(True, 1, 2))
+        True
+        """
+        return z3.is_app_of(x, z3.Z3_OP_ITE)
+
+    def is_constructor(x: z3.ExprRef) -> bool:
+        """
+        Check if an expression is a constructor.
+        >>> Color = z3.Datatype("Color")
+        >>> Color.declare("red")
+        >>> Color = Color.create()
+        >>> is_constructor(Color.red)
+        True
+        """
+        return z3.is_app_of(x, z3.Z3_OP_DT_CONSTRUCTOR)
+
+    def is_accessor(x: z3.ExprRef) -> bool:
+        """
+        Check if an expression is an accessor.
+        >>> Color = z3.Datatype("Color")
+        >>> Color.declare("red", ("r", z3.IntSort()))
+        >>> Color = Color.create()
+        >>> is_accessor(Color.r(Color.red(3)))
+        True
+        """
+        return z3.is_app_of(x, z3.Z3_OP_DT_ACCESSOR)
+
+    def is_recognizer(x: z3.ExprRef) -> bool:
+        """
+        Check if recognizer.
+                >>> Color = z3.Datatype("Color")
+        >>> Color.declare("red")
+        >>> Color = Color.create()
+        >>> is_recognizer(Color.is_red(Color.red))
+        True
+        """
+        return z3.is_app_of(x, z3.Z3_OP_DT_IS)
+
     Z3Solver = Solver
 elif solver == VAMPIRESOLVER:
     from z3 import *