ivy/test/relarray.ivy

#lang ivy1.7

module array(domain,range) = {

    type this
    alias t = this
    

    # return an empty array

    action empty returns (a:t)

    # return an array with end=s and all values mapped to y
    action create(s:domain,y:range) returns (a:t)

    # mutate an array a so that x in [0,end) maps to y
    action set(a:t,x:domain,y:range) returns (a:t)

    # get the value y such that x in [0,end) maps to y in array a
    action get(a:t,x:domain) returns (y:range) 

    # get the value of end
    action size(a:t) returns (s:domain)
    
    # change the size of the array
    action resize(a:t,s:domain,v:range) returns (a:t)

    # add one element to the array
    action append(a:t,v:range) returns (a:t)

    ########################################
    # Representation
    #
    # Function "end" gives the end value of an array while value(a,x)
    # gives the value that x maps to in a.

    function end(A:t) : domain
    relation value(A:t,X:domain,Y:range)

    ########################################
    # Specification
    #
    # Notice that get and set have the precondition that x is in
    # [0,end).


    object spec = {
	property end(X) >= 0
        property value(A,X,Y1) & value(A,X,Y2) -> Y1 = Y2
 
	after empty {
	    assert end(a) = 0
	}
	before create {
	    assert 0 <= s
	}
	after create {
	    assert end(a) = s & value(a,X,y)
	}
        before set {
	    assert 0 <= x & x < end(a)
	}	       	 
	after set {
            assert end(a) = end(old a);
	    assert value(a,x,Y) <-> Y = y;
            assert X ~= x -> (value(a,X,Y) <-> value(old a,X,Y))
	}
	before get {
	    assert 0 <= x & x < end(a)
	}
	after get {
	    assert value(a,x,y)
	}
	after size {
	    assert s = end(a)
	}
	after resize {
	    assert end(a) = s;
	    assert 0 <= X & X < end(old a) -> value(a,X,Y) <-> value(old a,X,Y);
	    assert end(old a) <= X & X < s -> value(a,X,Y) <-> Y = v
	}
	after append {
	    assert end(a) > end(old a) & ~(end(old a) < X & X < end(a));
	    assert 0 <= X & X < end(old a) -> value(a,X,Y) <-> value(old a,X,Y);
	    assert value(a,end(old a),Y) <-> Y = v
	}
    }

    object impl = {

	# object t_ = {}

	# <<< member
        #     class `t_` : std::vector<`range`> {};
        # >>>

	# interpret t -> <<< `t_` >>>

	interpret t -> <<< std::vector<`range`> >>>

	definition value(a:t,i:domain,v:range) = <<< (0 <= `i` && `i` < `a`.size()) ? `a`[`i`] == `v`: false >>>

	definition end(a:t) = <<< `a`.size() >>>

	implement create {
	    <<<
	        `a`.resize(`s`);
	        for (unsigned i = 0; i < `s`; i++)
	            `a`[i] = y;
	    >>>
	}

	implement empty {
	    <<<
	    >>>
	}

	implement set {
	    <<<
	        if (0 <= `x` && `x` < (`domain`)`a`.size()) 
	            `a`[`x`] = `y`;
	    >>>
	}

	implement get {
	    <<<
	        if (0 <= `x` && `x` < (`domain`)`a`.size()) 
	            `y` = `a`[`x`];
	    >>>
	}

	implement size {
	    <<<
	        `s` = (`domain`) `a`.size();
	    >>>
	}

	implement resize {
	    <<<
	        unsigned __old_size = `a`.size();
	        `a`.resize(`s`);
	        for (unsigned i = __old_size; i < (unsigned)`s`; i++)
	            `a`[i] = v;
            >>>
        }

	implement append {
	    <<<
	        `a`.push_back(`v`);
            >>>
        }

	<<< impl
	    std::ostream &operator <<(std::ostream &s, const `t` &a) {
	        s << '[';
		for (unsigned i = 0; i < a.size(); i++) {
		    if (i != 0)
		        s << ',';
		    s << a[i];
		}
	        s << ']';
		return s;
            }

	    template <>
	    `t` _arg<`t`>(std::vector<ivy_value> &args, unsigned idx, int bound) {
	        ivy_value &arg = args[idx];
	        if (arg.atom.size()) 
	            throw out_of_bounds(idx);
	        `t` a;
	        a.resize(arg.fields.size());
		for (unsigned i = 0; i < a.size(); i++) {
		    a[i] = _arg<`range`>(arg.fields,i,0);
	        }
	        return a;
	    }

	    template <>
	    void __deser<`t`>(ivy_deser &inp, `t` &res) {
	        inp.open_list();
	        while(inp.open_list_elem()) {
		    res.resize(res.size()+1);
	            __deser(inp,res.back());
		    inp.close_list_elem();
                }
		inp.close_list();
	    }

	    template <>
	    void __ser<`t`>(ivy_ser &res, const `t` &inp) {
	        int sz = inp.size();
	        res.open_list(sz);
	        for (unsigned i = 0; i < (unsigned)sz; i++) {
		    res.open_list_elem();
	            __ser(res,inp[i]);
		    res.close_list_elem();
                }
	        res.close_list();
	    }

	    #ifdef Z3PP_H_
	    template <>
            z3::expr __to_solver(gen& g, const z3::expr& z3val, `t`& val) {
	        z3::expr z3end = g.apply("`end`",z3val);
	        z3::expr __ret = z3end  == g.int_to_z3(z3end.get_sort(),val.size());
	        unsigned __sz = val.size();
	        for (unsigned __i = 0; __i < __sz; ++__i)
		    __ret = __ret && __to_solver(g,g.apply("`value`",z3val,g.int_to_z3(g.sort("`domain`"),__i)),val[__i]);
                return __ret;
            }

	    template <>
	    void  __from_solver<`t`>( gen &g, const  z3::expr &v,`t` &res){
	        `domain` __end;
	        __from_solver(g,g.apply("`end`",v),__end);
	        unsigned __sz = (unsigned) __end;
	        res.resize(__sz);
	        for (unsigned __i = 0; __i < __sz; ++__i)
		    __from_solver(g,g.apply("`value`",v,g.int_to_z3(g.sort("`domain`"),__i)),res[__i]);
	    }

	    template <>
	    void  __randomize<`t`>( gen &g, const  z3::expr &v){
	        unsigned __sz = rand() % 4;
                z3::expr val_expr = g.int_to_z3(g.sort("`domain`"),__sz);
                z3::expr pred =  g.apply("`end`",v) == val_expr;
                g.add_alit(pred);
	        for (unsigned __i = 0; __i < __sz; ++__i)
	            __randomize<`range`>(g,g.apply("`value`",v,g.int_to_z3(g.sort("`domain`"),__i)));
	    }
	    #endif

	>>>
    }

    trusted isolate iso = spec,impl

    attribute test = impl
}