#include "verify.h"
#include "builtins/builtins.h"
#include "helpers.inl"

using namespace goose::diagnostics;

namespace goose::verify
{
    Z3Val BuildZ3ValFromConstant( Builder& b, const Value& val )
    {
        optional< TypeInfo > tinfo;

        tinfo = TypeCache::GetInstance().getTypeInfo( b.context(), val.type() );

        if( !tinfo )
            tinfo = TypeCache::GetInstance().uninterpretedTypeInfo();

        auto zexpr = tinfo->build( b, val );
        return Z3Val { move( zexpr ), *EIRToValue( val.type() ), val.locationId() };
    }

    optional< Z3Val > TryBuildZ3ValFromConstant( Builder& b, const Value& val )
    {
        auto tinfo = TypeCache::GetInstance().getTypeInfo( b.context(), val.type() );
        if( !tinfo )
            return nullopt;

        auto zexpr = tinfo->build( b, val );
        return Z3Val { move( zexpr ), *EIRToValue( val.type() ), val.locationId() };
    }

    Z3Val BuildZ3ConstantFromType( Builder& b, const Value& type, const string& name )
    {
        auto tinfo = TypeCache::GetInstance().getTypeInfo( b.context(), ValueToEIR( type ) );
        if( !tinfo )
            tinfo = TypeCache::GetInstance().uninterpretedTypeInfo();

        assert( tinfo->sort );
        return Z3Val { GetZ3Context().constant( name.c_str(), *tinfo->sort ), type, type.locationId() };
    }

    optional< Z3Val > TryBuildZ3ConstantFromType( Builder& b, const Value& type, const string& name )
    {
        auto tinfo = TypeCache::GetInstance().getTypeInfo( b.context(), ValueToEIR( type ) );
        if( !tinfo )
            return nullopt;

        assert( tinfo->sort );
        return Z3Val { GetZ3Context().constant( name.c_str(), *tinfo->sort ), type, type.locationId() };
    }

    Z3Val BuildZ3ConstantFromType( Builder& b, const Term& type, const string& name )
    {
        auto tinfo = TypeCache::GetInstance().getTypeInfo( b.context(), type );
        if( !tinfo )
            tinfo = TypeCache::GetInstance().uninterpretedTypeInfo();

        assert( tinfo->sort );
        auto tval = *EIRToValue( type );
        return Z3Val { GetZ3Context().constant( name.c_str(), *tinfo->sort ), tval, tval.locationId() };
    }

    optional< Z3Val > TryBuildZ3ConstantFromType( Builder& b, const Term& type, const string& name )
    {
        auto tinfo = TypeCache::GetInstance().getTypeInfo( b.context(), type );
        if( !tinfo )
            return nullopt;

        assert( tinfo->sort );
        auto tval = *EIRToValue( type );
        return Z3Val { GetZ3Context().constant( name.c_str(), *tinfo->sort ), tval, tval.locationId() };
    }

    z3::expr GetAsBitVec( const z3::expr& expr, const Value& type )
    {
        if( expr.is_bv() )
            return expr;

        assert( expr.is_int() );

        auto intType = FromValue< builtins::IntegerType >( type );
        assert( intType );

        return z3::int2bv( intType->m_numBits, expr );
    }

    z3::expr GetAsBitVec( const Z3Val& zv )
    {
        return GetAsBitVec( zv.expr, zv.type );
    }

    z3::expr GetAsInt( const z3::expr& expr, const Value& type )
    {
        if( expr.is_int() )
            return expr;

        assert( expr.is_bv() );

        auto intType = FromValue< builtins::IntegerType >( type );
        assert( intType );

        return z3::bv2int( expr, intType->m_signed );
    }

    z3::expr GetAsInt( const Z3Val& zv )
    {
        return GetAsInt( zv.expr, zv.type );
    }

    z3::expr Coerce( const Z3Val& val, const Z3Val& to )
    {
        return Coerce( val.expr, to );
    }

    z3::expr Coerce( const z3::expr& expr, const Z3Val& to )
    {
        if( to.expr.is_int() )
            return GetAsInt( expr, to.type );
        else if( to.expr.is_bv() )
            return GetAsBitVec( expr, to.type );
        else
            return expr;
    }

    template< typename I, typename F >
    bool BuildZ3UnaryExpr( Builder& b, const I& instr, F&& func )
    {
        auto operand = b.pop();
        if( !operand )
            return false;

        b.push( Z3Val{ func( operand->expr ), operand->type, instr.locationId() } );
        return true;
    }

    template< typename I, typename F >
    bool BuildZ3BinExpr( Builder& b, const I& instr, F&& func )
    {
        auto rhs = b.pop();
        if( !rhs )
            return false;

        auto lhs = b.pop();
        if( !lhs )
            return false;

        if( lhs->expr.get_sort().sort_kind() == rhs->expr.get_sort().sort_kind() )
        {
            b.push( Z3Val{ func( lhs->expr, rhs->expr, lhs->type ), lhs->type, instr.locationId() } );
            return true;
        }

        // If we are trying to do an operation on a mix of bitvec and int,
        // convert the int to a bitvec first.
        if( lhs->expr.is_bv() )
        {
            assert( rhs->expr.is_int() );
            b.push( Z3Val{ func( lhs->expr, GetAsBitVec( *rhs ), lhs->type ), lhs->type, instr.locationId() } );
            return true;
        }
        else
        {
            assert( lhs->expr.is_int() );
            b.push( Z3Val{ func( GetAsBitVec( *lhs ), rhs->expr, lhs->type ), lhs->type, instr.locationId() } );
            return true;
        }

        return false;
    }

    template< typename I, typename F >
    bool BuildZ3BinBitwiseExpr( Builder& b, const I& instr, F&& func )
    {
        auto rhs = b.pop();
        if( !rhs )
            return false;

        auto lhs = b.pop();
        if( !lhs )
            return false;

        if( ValueToEIR( lhs->type ) == GetValueType< BigInt >() )
        {
            DiagnosticsManager::GetInstance().emitErrorMessage( 0, "verifier error: bitwise operands can't be ct_int." );
            return false;
        }

        if( ValueToEIR( rhs->type ) == GetValueType< BigInt >() )
        {
            DiagnosticsManager::GetInstance().emitErrorMessage( 0, "verifier error: bitwise operands can't be ct_int." );
            return false;
        }

        if( lhs->expr.get_sort().sort_kind() == rhs->expr.get_sort().sort_kind() )
        {
            b.push( Z3Val{ func( lhs->expr, rhs->expr, lhs->type ), lhs->type, instr.locationId() } );
            return true;
        }

        // If we are trying to do an operation on a mix of bitvec and int,
        // convert the int to a bitvec first.
        if( lhs->expr.is_bv() )
        {
            assert( rhs->expr.is_int() );
            b.push( Z3Val{ func( lhs->expr, GetAsBitVec( *rhs ), lhs->type ), lhs->type, instr.locationId() } );
            return true;
        }
        else
        {
            assert( lhs->expr.is_int() );
            b.push( Z3Val{ func( GetAsBitVec( *lhs ), rhs->expr, lhs->type ), lhs->type, instr.locationId() } );
            return true;
        }

        return false;
    }

    template< typename I, typename F >
    bool BuildZ3BinBoolExpr( Builder& b, const I& instr, F&& func )
    {
        auto rhs = b.pop();
        if( !rhs )
            return false;

        auto lhs = b.pop();
        if( !lhs )
            return false;

        if( lhs->expr.get_sort().sort_kind() == rhs->expr.get_sort().sort_kind() )
        {
            b.push( Z3Val{ func( lhs->expr, rhs->expr, lhs->type ), *EIRToValue( GetValueType< bool >() ), instr.locationId() } );
            return true;
        }

        // If we are trying to do an operation on a mix of bitvec and int,
        // convert the int to a bitvec first.
        if( lhs->expr.is_bv() )
        {
            assert( rhs->expr.is_int() );
            b.push( Z3Val{ func( lhs->expr, GetAsBitVec( *rhs ), lhs->type ), *EIRToValue( GetValueType< bool >() ), instr.locationId() } );
            return true;
        }
        else
        {
            cout << lhs->expr << endl;
            assert( lhs->expr.is_int() );
            b.push( Z3Val{ func( GetAsBitVec( *lhs ), rhs->expr, lhs->type ), *EIRToValue( GetValueType< bool >() ), instr.locationId() } );
            return true;
        }

        return false;
    }

    template< typename I, typename F >
    bool BuildZ3BinLogicExpr( Builder& b, const I& instr, F&& func )
    {
        auto rhs = b.pop();
        if( !rhs )
            return false;

        auto lhs = b.pop();
        if( !lhs )
            return false;

        if( !lhs->expr.is_bool() )
            return false;

        if( !rhs->expr.is_bool() )
            return false;

        b.push( Z3Val{ func( lhs->expr, rhs->expr, lhs->type ), *EIRToValue( GetValueType< bool >() ), instr.locationId() } );
        return true;
    }

    template< typename RT, typename I, typename F >
    bool BuildZ3BinSeqExpr( Builder& b, const I& instr, F&& func )
    {
        auto rhs = b.pop();
        if( !rhs )
            return false;

        auto lhs = b.pop();
        if( !lhs )
            return false;

        if( !lhs->expr.is_seq() )
            return false;

        if( !rhs->expr.is_seq() )
            return false;

        b.push( Z3Val{
            func( lhs->expr, rhs->expr ),
            *EIRToValue( GetValueType< RT >() ),
            instr.locationId() } );
        return true;
    }

    bool BuildZ3Op( Builder& b, const cir::InstrSeq& is )
    {
        for( const auto& instr : is )
        {
            if( !BuildZ3Op( b, instr ) )
                return false;
        }

        return true;
    }

    template< typename T >
    bool BuildZ3Op( Builder& b, const T& instr )
    {
        return false;
    }

    bool BuildZ3Op( Builder& b, const Load& instr )
    {
        optional< Z3Val > zv;

        if( auto cstAddr = b.pop< Address >() )
            zv = LoadFromAddress( b, *cstAddr, instr.type().get() );
        else if( auto gfa = b.pop< GhostFuncApplication >() )
            zv = LoadFromAddress( b, *gfa );
        else if( auto symAddr = b.pop< Z3Val >() )
            zv = BuildZ3ConstantFromType( b, instr.type().get(), format( "val{}", b.newUniqueId() ) );

        if( !zv )
            return false;

        if( b.mustLoadAssume() )
            ForEachPredicate( b, instr.type().get(), zv->expr, [&]( auto&& z3expr, auto locId )
            {
                b.assume( z3expr );
            } );

        zv->loc = instr.locationId();
        b.push( move( *zv ) );
        return true;
    }

    bool BuildZ3Op( Builder& b, const Store& instr )
    {
        auto addr = b.pop< Stack::Slot >();
        if( !addr )
            return false;

        auto zv = b.pop();
        if( !zv )
            return false;

        ForEachPredicate( b, instr.type().get(), zv->expr, [&]( auto&& z3expr, auto locId )
        {
            if( !instr.srcLocId().invalid() && !instr.destLocId().invalid() )
            {
                DiagnosticsContext dc( instr.destLocId(), "...to this." );
                DiagnosticsContext dc2( instr.srcLocId(), "When assigning this..." );
                b.checkAssertion( z3expr, locId );
            }
            else
                b.checkAssertion( z3expr, locId );
        } );

        if( const auto* cstAddr = get_if< Address >( &*addr ) )
            StoreToAddress( b, *cstAddr, move( *zv ) );
        else if( const auto* gfa = get_if< GhostFuncApplication >( &*addr ) )
            StoreToAddress( b, *gfa, move( *zv ) );

        return true;
    }

    // Implemented in call.cpp
    extern bool BuildZ3Op( Builder& b, const Call& instr );
    extern bool BuildZ3Op( Builder& b, const CallCheck& instr );

    bool BuildZ3Op( Builder& b, const CreateTemporary& instr )
    {
        auto zv = b.pop();
        if( !zv )
            return false;

        b.setTemporary( instr.index(), move( *zv ) );
        return true;
    }

    bool BuildZ3Op( Builder& b, const GetTemporary& instr )
    {
        auto zv = b.getTemporary( instr.index() );
        if( !zv )
            return false;

        b.push( move( *zv ) );
        return true;
    }

    bool BuildZ3Op( Builder& b, const AllocVar& instr )
    {
        auto tinfo = TypeCache::GetInstance().getTypeInfo( b.context(), instr.type().get() );
        if( !tinfo )
            tinfo = TypeCache::GetInstance().uninterpretedTypeInfo();

        b.setVar( instr.index(), Z3Val{ tinfo->undefined( b ), *EIRToValue( instr.type().get() ), instr.locationId() } );
        return true;
    }

    // Implemented in phi.cpp
    bool BuildZ3Op( Builder& b, const Phi& instr );

    bool BuildZ3Op( Builder& b, const Not& instr )
    {
        return BuildZ3UnaryExpr( b, instr, []( auto&& operand )
        {
            if( operand.is_bool() )
                return !operand;

            assert( operand.is_bv() );
            return ~operand;
        } );
    }

    bool BuildZ3Op( Builder& b, const And& instr )
    {
        return BuildZ3BinBitwiseExpr( b, instr, []( auto&& lhs, auto&& rhs, auto&& type )
        {
            if( lhs.is_bool() && rhs.is_bool() )
                return lhs && rhs;

            auto lhsBV = GetAsBitVec( lhs, type );
            auto rhsBV = GetAsBitVec( rhs, type );
            return lhsBV & rhsBV;
        } );
    }

    bool BuildZ3Op( Builder& b, const Or& instr )
    {
        return BuildZ3BinBitwiseExpr( b, instr, []( auto&& lhs, auto&& rhs, auto&& type )
        {
            if( lhs.is_bool() && rhs.is_bool() )
                return lhs || rhs;

            auto lhsBV = GetAsBitVec( lhs, type );
            auto rhsBV = GetAsBitVec( rhs, type );
            return lhsBV | rhsBV;
        } );
    }

    bool BuildZ3Op( Builder& b, const Xor& instr )
    {
        return BuildZ3BinBitwiseExpr( b, instr, []( auto&& lhs, auto&& rhs, auto&& type )
        {
            if( lhs.is_bool() && rhs.is_bool() )
                return lhs ^ rhs;

            auto lhsBV = GetAsBitVec( lhs, type );
            auto rhsBV = GetAsBitVec( rhs, type );
            return lhsBV ^ rhsBV;
        } );
    }

    bool BuildZ3Op( Builder& b, const Implies& instr )
    {
        return BuildZ3BinLogicExpr( b, instr, []( auto&& lhs, auto&& rhs, auto&& type )
        {
            return z3::implies( lhs, rhs );
        } );
    }

    bool BuildZ3Op( Builder& b, const IsPrefixOf& instr )
    {
        return BuildZ3BinSeqExpr< bool >( b, instr, []( auto&& lhs, auto&& rhs )
        {
            return z3::prefixof( lhs, rhs );
        } );
    }

    bool BuildZ3Op( Builder& b, const Shl& instr )
    {
        return BuildZ3BinBitwiseExpr( b, instr, []( auto&& lhs, auto&& rhs, auto&& type )
        {
            auto lhsBV = GetAsBitVec( lhs, type );
            auto rhsBV = GetAsBitVec( rhs, type );
            return z3::shl( lhsBV, rhsBV );
        } );
    }

    bool BuildZ3Op( Builder& b, const LShr& instr )
    {
        return BuildZ3BinBitwiseExpr( b, instr, []( auto&& lhs, auto&& rhs, auto&& type )
        {
            auto lhsBV = GetAsBitVec( lhs, type );
            auto rhsBV = GetAsBitVec( rhs, type );
            return z3::lshr( lhsBV, rhsBV );
        } );
    }

    bool BuildZ3Op( Builder& b, const AShr& instr )
    {
        return BuildZ3BinBitwiseExpr( b, instr, []( auto&& lhs, auto&& rhs, auto&& type )
        {
            auto lhsBV = GetAsBitVec( lhs, type );
            auto rhsBV = GetAsBitVec( rhs, type );
            return z3::ashr( lhsBV, rhsBV );
        } );
    }

    bool BuildZ3Op( Builder& b, const Add& instr )
    {
        return BuildZ3BinExpr( b, instr, []( auto&& lhs, auto&& rhs, auto&& type ) { return lhs + rhs; } );
    }

    bool BuildZ3Op( Builder& b, const Sub& instr )
    {
        return BuildZ3BinExpr( b, instr, []( auto&& lhs, auto&& rhs, auto&& type ) { return lhs - rhs; } );
    }

    bool BuildZ3Op( Builder& b, const Mul& instr )
    {
        return BuildZ3BinExpr( b, instr, []( auto&& lhs, auto&& rhs, auto&& type ) { return lhs * rhs; } );
    }

    bool BuildZ3Op( Builder& b, const UDiv& instr )
    {
        return BuildZ3BinExpr( b, instr, []( auto&& lhs, auto&& rhs, auto&& type ) { return z3::udiv( lhs, rhs ); } );
    }

    bool BuildZ3Op( Builder& b, const SDiv& instr )
    {
        return BuildZ3BinExpr( b, instr, []( auto&& lhs, auto&& rhs, auto&& type ) { return lhs / rhs; } );
    }

    bool BuildZ3Op( Builder& b, const URem& instr )
    {
        return BuildZ3BinExpr( b, instr, []( auto&& lhs, auto&& rhs, auto&& type ) { return z3::urem( lhs, rhs ); } );
    }

    bool BuildZ3Op( Builder& b, const SRem& instr )
    {
        return BuildZ3BinExpr( b, instr, []( auto&& lhs, auto&& rhs, auto&& type )
        {
            if( lhs.is_bv() )
                return z3::srem( lhs, rhs );

            return z3::rem( lhs, rhs );
        } );
    }

    bool BuildZ3Op( Builder& b, const Eq& instr )
    {
        return BuildZ3BinBoolExpr( b, instr, []( auto&& lhs, auto&& rhs, auto&& type ) { return lhs == rhs; } );
    }

    bool BuildZ3Op( Builder& b, const Neq& instr )
    {
        return BuildZ3BinBoolExpr( b, instr, []( auto&& lhs, auto&& rhs, auto&& type ) { return lhs != rhs; } );
    }

    bool BuildZ3Op( Builder& b, const UGT& instr )
    {
        return BuildZ3BinBoolExpr( b, instr, []( auto&& lhs, auto&& rhs, auto&& type ) { return z3::ugt( lhs, rhs ); } );
    }

    bool BuildZ3Op( Builder& b, const UGE& instr )
    {
        return BuildZ3BinBoolExpr( b, instr, []( auto&& lhs, auto&& rhs, auto&& type ) { return z3::uge( lhs, rhs ); } );
    }

    bool BuildZ3Op( Builder& b, const ULT& instr )
    {
        return BuildZ3BinBoolExpr( b, instr, []( auto&& lhs, auto&& rhs, auto&& type ) { return z3::ult( lhs, rhs ); } );
    }

    bool BuildZ3Op( Builder& b, const ULE& instr )
    {
        return BuildZ3BinBoolExpr( b, instr, []( auto&& lhs, auto&& rhs, auto&& type ) { return z3::ule( lhs, rhs ); } );
    }

    bool BuildZ3Op( Builder& b, const SGT& instr )
    {
        return BuildZ3BinBoolExpr( b, instr, []( auto&& lhs, auto&& rhs, auto&& type ) { return lhs > rhs; } );
    }

    bool BuildZ3Op( Builder& b, const SGE& instr )
    {
        return BuildZ3BinBoolExpr( b, instr, []( auto&& lhs, auto&& rhs, auto&& type ) { return lhs >= rhs; } );
    }

    bool BuildZ3Op( Builder& b, const SLT& instr )
    {
        return BuildZ3BinBoolExpr( b, instr, []( auto&& lhs, auto&& rhs, auto&& type ) { return lhs < rhs; } );
    }

    bool BuildZ3Op( Builder& b, const SLE& instr )
    {
        return BuildZ3BinBoolExpr( b, instr, []( auto&& lhs, auto&& rhs, auto&& type ) { return lhs <= rhs; } );
    }

    bool BuildZ3Op( Builder& b, const Assert& instr )
    {
        auto cond = b.pop();
        if( !cond )
            return false;

        b.checkAssertion( cond->expr, cond->loc );
        return true;
    }

    bool BuildZ3Op( Builder& b, const Placeholder& instr )
    {
        const auto* expr = b.retrievePlaceholder( instr.name() );
        if( expr )
        {
            b.push( Z3Val{ *expr, *EIRToValue( instr.type().get() ), instr.locationId() } );
            return true;
        }

        auto result = BuildZ3ConstantFromType( b, instr.type().get(), format( "p{}", instr.name().str() ) );
        b.push( move( result ) );
        return true;
    }

    bool BuildZ3Op( Builder& b, const PHOverrideSet& instr )
    {
        auto phExpr = b.pop();
        if( !phExpr )
            return false;

        return b.setPlaceholder( instr.name(), phExpr->expr );
    }

    bool BuildZ3Op( Builder& b, const PHOverrideClear& instr )
    {
        b.unsetPlaceholder( instr.name() );
        return true;
    }

    bool BuildZ3Op( Builder& b, const PushConstant& instr )
    {
        auto v = TryBuildZ3ExprFromValue( b, instr.value().get() );
        if( v )
            b.push( move( *v ) );
        else
            b.push( instr.value().get() );
        return true;
    }

    bool BuildZ3Op( Builder& b, const VarAddr& instr )
    {
        b.push( Address( {}, Address::Origin::Stack, instr.varIndex(), instr.locationId() ) );
        return true;
    }

    bool BuildZ3Op( Builder& b, const TempAddr& instr )
    {
        auto initVal = b.pop();
        if( !initVal )
            return false;

        b.push( Address( {}, Address::Origin::Stack, instr.tempIndex(), instr.locationId() ) );
        return !!b.setVar( instr.tempIndex(), move( *initVal ) );
    }

    bool BuildZ3Op( Builder& b, const Select& instr )
    {
        if( auto cstBaseLoc = b.pop< Address >() )
        {
            b.push( Address::Select( move( *cstBaseLoc ), instr.memberIndex(), instr.locationId() ) );
            return true;
        }

        auto symBaseLoc = b.pop();
        if( !symBaseLoc )
            return false;

        const auto& tc = TypeCache::GetInstance();

        auto ltExpr = tc.addrLifetimeGetter()( symBaseLoc->expr );
        auto originExpr = tc.addrOriginGetter()( symBaseLoc->expr );
        auto pathExpr = tc.addrPathGetter()( symBaseLoc->expr );

        b.push( Z3Val
        {
            tc.addrCtor()(
                ltExpr,
                originExpr,
                z3::concat( pathExpr, GetZ3Context().int_val( instr.memberIndex() ).unit() )
            ),

            *EIRToValue( GetValueType< cir::Address >() ),
            instr.locationId()
        } );

        return true;
    }

    bool BuildZ3Op( Builder& b, const GhostCall& instr )
    {
        auto gfunc = b.pop< Value >();
        if( !gfunc )
            return false;

        auto argCount = instr.numArgs();
        llvm::SmallVector< Z3Val, 16 > args;
        args.reserve( argCount );

        for( uint32_t argIndex = 0; argIndex < argCount; ++argIndex )
        {
            auto zv = b.pop();
            if( !zv )
                return false;

            args.emplace_back( move( *zv ) );
        }

        GhostFuncApplication gfa( move( *gfunc ), instr.locationId() );

        gfa.args().reserve( args.size() );
        for( auto it = args.rbegin(); it != args.rend(); ++it )
            gfa.args().emplace_back( move( *it ) );

        b.push( move( gfa ) );
        return true;
    }

    bool BuildZ3Op( Builder& b, const ForAllSetup& instr )
    {
        auto argCount = instr.numArgs();
        b.beginForAll( argCount );

        for( uint32_t i = 0; i < argCount; ++i )
        {
            auto name = b.pop< StringId >();
            if( !name )
                return false;

            auto type = b.pop< Term >();
            if( !type )
                return false;

            if( !b.declareForAllVar( *name, move( *type ) ) )
                return false;
        }

        return true;
    }

    bool BuildZ3Op( Builder& b, const ForAll& instr )
    {
        auto expr = b.pop();
        if( !expr )
            return false;

        return b.pushForAll( move( *expr ), instr.locationId() );
    }

    bool BuildZ3Op( Builder& b, const PushType& instr )
    {
        b.push( instr.type() );
        return true;
    }

    bool BuildZ3Op( Builder& b, const PushStringId& instr )
    {
        b.push( instr.stringId() );
        return true;
    }

    bool BuildZ3Op( Builder& b, const cir::InlineCall& instr )
    {
        G_ERROR( "InlineCall encountered during verification" );
        return false;
    }

    bool BuildZ3Op( Builder& b, const cir::Instruction& instr )
    {
        return visit( [&]( auto&& e )
        {
            return BuildZ3Op( b, e );
        }, instr );
    }

    Z3Val BuildZ3ExprFromValue( Builder& b, const Value& val )
    {
        if( val.isConstant() )
            return BuildZ3ValFromConstant( b, val );

        if( BuildZ3Op( b, *val.cir() ) )
        {
            auto result = b.pop();
            if( result )
                return *result;
        }

        return BuildZ3ConstantFromType( b, val.type(), format( "val{}", b.newUniqueId() ) );
    }

    optional< Z3Val > TryBuildZ3ExprFromValue( Builder& b, const Value& val )
    {
        if( val.isPoison() )
            return nullopt;

        if( val.isConstant() )
            return TryBuildZ3ValFromConstant( b, val );

        if( BuildZ3Op( b, *val.cir() ) )
            return b.pop();

        return TryBuildZ3ConstantFromType( b, val.type(), format( "val{}", b.newUniqueId() ) );
    }
}
