Goose  Artifact [852749acd0]

Artifact 852749acd035d1fa4b43d241f6cc50a4907da750b945f4a7b1714611619a96d3:

• File bs/verify/helpers.h — part of check-in [6f98718d3b] at 2020-06-01 01:06:52 on branch trunk — Verifier: refactored type handling and extended it to handle tuple types. (user: achavasse size: 2080)

#ifndef GOOSE_HELPERS_H
#define GOOSE_HELPERS_H

namespace goose::verify
{
    template< typename F >
    void ForEachPredicate( Builder& b, const Term& t, const z3::expr& valExpr, F&& func );

    // Some c++ wrappers that seems to be missing from z3++.h

    // bool xor
    static inline z3::expr mkZ3BoolXor( const z3::expr& a, const z3::expr& b )
    {
        z3::check_context(a, b);
        assert( a.is_bool() && b.is_bool() );
        Z3_ast r = Z3_mk_xor( a.ctx(), a, b );
        a.check_error();
        return z3::expr( a.ctx(), r );
    }

    // A modified version of z3::context::tuple_sort that returns both the tuple constructor's func_decl and the tuple's sort because
    // I don't understand how I am supposed to get the tuple's sort when using the original C++ function, especially since it seems
    // straightforward in the C api (other than the normal suckage expected from a C api).
    //
    // Maybe I'm just missing something but it's hard to tell from the barren doxygen dump offered by z3 in lieu of api documentation
    static inline pair< z3::sort, z3::func_decl >
    mkZ3TupleSort( const char* name, unsigned n,
        const llvm::SmallVector< string, 8 >& names, const llvm::SmallVector< z3::sort, 8 >& sorts,
        llvm::SmallVector< z3::func_decl, 8 >& projs )
    {
        auto& ctx = GetZ3Context();

        z3::array<Z3_symbol> _names(n);
        z3::array<Z3_sort> _sorts(n);

        for( unsigned i = 0; i < n; ++i )
        {
            _names[i] = Z3_mk_string_symbol( ctx, names[i].c_str() );
            _sorts[i] = sorts[i];
        }

        z3::array<Z3_func_decl> _projs(n);
        Z3_symbol _name = Z3_mk_string_symbol(ctx, name);
        Z3_func_decl tuple;
        z3::sort _s = to_sort(ctx, Z3_mk_tuple_sort(ctx, _name, n, _names.ptr(), _sorts.ptr(), &tuple, _projs.ptr()));
        ctx.check_error();

        for( unsigned i = 0; i < n; ++i )
        {
            projs.push_back( z3::func_decl(ctx, _projs[i]) );
        }

        return make_pair( move( _s ), z3::func_decl(ctx, tuple) );
    }
}

#endif