function s_out = BR_switch_vars(s,v)
% BR_switch_vars - polynomial time distribution of v over ^
% On input:
%     s (string): logical sentence (fully parenthesize)
%     v (int): max variable value (as integer)
% On output:
%     s_out (string): s with v distributed over ^
% Call:
%     ss = BR_switch_vars('(1)',1);
% Author:
%     T. Henderson
%     UU
%     Fall 2018
%

s_out = s;

if isempty(s)|BR_isvariable(s)|BR_only_OR(s)|BR_only_AND(s)
    return
end

if BR_isORop(s)
    [OP1,OP2] = BR_getORargs(s);
    if BR_isliteral(OP1)&BR_only_AND(OP2)
        literals = BR_get_literals(OP2);
        num_literals = length(literals);
        C = ['(',OP1,'v','(',num2str(literals(1)),'))'];
        for k = 2:num_literals
            C = ['(',C,'^(',OP1,'v(',num2str(literals(k)),')))'];
        end
        s_out = C;
        return
    elseif BR_isliteral(OP1)
        ss = BR_switch_vars(OP2,v);
        args = BR_all_and_args(ss);
        num_args = length(args);
        C = ['(',OP1,'v(',args(1).s,'))'];
        for a = 2:num_args
            C = ['(',C,'^(',OP1,'v(',args(a).s,')))'];
        end
        s_out = C;
        return
    end
end

if BR_isANDop(s)
    [OP1,OP2] = BR_getANDargs(s);
    s_out = ['(',BR_switch_vars(OP1,v),'^',BR_switch_vars(OP2,v),')'];
else
    [OP1,OP2] = BR_getORargs(s);
    v = v + 1;
    LHS = ['((-',num2str(v),')v',OP1,')'];
    RHS = ['((',num2str(v),')v',OP2,')'];
    s_out = ['(',BR_switch_vars(LHS,v),'^',BR_switch_vars(RHS,v),')'];
end
