philzook58

philzook58

% Follow paper exactly.  https://arxiv.org/abs/1804.02452 See Appendix A
% Difference from unison model.mzn: Try not using integers. Try to use better minizinc syntax. Much simplified

include "globals.mzn";

%% ---------------------------------------
%% PARAMETERS
%% ---------------------------------------

% Type definitions

philzook58

def matrix_to_eqs(m):
   nrows, ncols = m.shape
   gens = [sy.Dummy() for i in range(ncols)]
   eqs = m @ sy.Matrix(gens)
   return eqs, gens
def eqs_to_matrix(eqns, gens):
    return sy.Matrix( [[ eq.coeff(g) for g in gens] for eq in eqns])

philzook58

philzook58

{
 "cells": [
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "# ZX calculus in Catlab"
   ]
  },
  {

philzook58

from collections import Counter
class FinSet():
    def init(self, dom ,cod , f):
        '''  In order to specify a morphism, we need to give a python set that is the domain, a python set 
        that is the codomain, and a dictionary f that encodes a function between these two sets.
        We could by assumption just use f.keys() implicitly as the domain, however the codomain is not inferable from just f.
        In other categories that domain might not be either, so we chose to require both symmettrically.
        '''
        assert( dom == set(f.keys())) # f has value for everything in domain
        assert( all( [y in cod for y in f.value()] )) # f has only values in codomain

philzook58

class IntOrderCat():
    def __init__(self, dom, cod):
        assert(dom <= cod)
        self.cod = cod
        self.dom = dom
        self.f = ()
    def idd(n):
        return IntOrderCat(n,n)
    def compose(f,g):
        assert( f.dom == g.cod )

philzook58

import numpy as np
import scipy
import scipy.linalg
# https://docs.scipy.org/doc/numpy/user/basics.subclassing.html
class FinVect(np.ndarray):
    def __new__(cls, input_array, info=None):
        # Input array is an already formed ndarray instance
        # We first cast to be our class type
        
        obj = np.asarray(input_array).view(cls)

philzook58

def controller(Cat,pend_step, pos, vel):
   acc = Cat.idd(3)
   for i in range(10):
      acc = acc @ pend_step
   init = Cat.const(pos) * Cat.const(vel) * Cat.idd(1) 
   return acc @ init

philzook58

from z3 import *

def compare_and_swap_z3(x,y):
    x1, y1 = FreshInt(), FreshInt()
    c = If(x <= y, And(x1 == x, y1 == y) , And(x1 == y, y1 == x) )
    return x1, y1, c
    
# predicates of interest
def sorted_list(x): # list is sorted
    return And([x <= y for x,y in zip(x , x[1:])])