smt_symmetry_breaking

add_node_to_colored_graph(arg, _, _, ArgNodeId) :-
    color(arg, Color),
    bliss_interface:add_node('arg', Color, ArgNodeId), !.

add_node_to_colored_graph(Category, Symbol, Type, NodeId) :-
    ( Category == pred, IsPred = true, IsExpr = false
    ; Category == expr, IsExpr = true, IsPred = false
    ),
    ( ( (IsPred, have_seen_pred(Symbol, TNodeId))
    ; (IsExpr, have_seen_expr(Symbol, Type, TNodeId))
    )
    -> NodeId = TNodeId
    ; get_color_for_type(Type, Symbol, Color),
    term_to_label(Symbol, ASymbol),
    bliss_interface:add_node(ASymbol, Color, NodeId),
    ( IsExpr
    -> log_seen_expr(Symbol, Type, NodeId)
    ; log_seen_pred(Symbol, NodeId)
    )
    %asserta(node_id_to_ast(NodeId,b(Symbol,Type,[])))
    ), !.

add_node_to_colored_graph(upred, USymbol, pred, NodeId) :-
    seen_upred(USymbol, TNodeId),
    !,
    NodeId = TNodeId.

add_node_to_colored_graph(upred, USymbol, pred, NodeId) :-
    get_next_color(Color),
    bliss_interface:add_node(USymbol, Color, NodeId),
    asserta(seen_upred(USymbol,NodeId)), !.

add_node_to_colored_graph(uexpr, USymbol, _, NodeId) :-
    seen_uexpr(USymbol, TNodeId),
    !,
    NodeId = TNodeId.

add_node_to_colored_graph(uexpr, USymbol, _, NodeId) :-
    get_next_color(Color),
    bliss_interface:add_node(USymbol, Color, NodeId),
    asserta(seen_uexpr(USymbol,NodeId)), !.

add_nodes_from_ast_list_commutative(_, []).

add_nodes_from_ast_list_commutative(RootNodeId, [Id|T]) :-
    get_texpr_expr_functor_and_type(Id, IdExpr, IdType, IdFunctor),
    add_term_and_symbol_nodes_to_graph(IdExpr, IdType, IdFunctor, IdRootNodeId),
    add_node_to_colored_graph(arg, IdExpr, IdType, IdNodeId),
    bliss_interface:add_edge(IdNodeId, IdRootNodeId),
    bliss_interface:add_edge(RootNodeId, IdNodeId),
    build_colored_graph(IdExpr, IdType, IdRootNodeId),
    add_nodes_from_ast_list_commutative(RootNodeId, T).

add_sbps_from_generator([], _, _, Acc, Acc).

add_sbps_from_generator([FirstVarAst|T], Generator, EnumeratedSets, Acc, NAcc) :-
    FirstVarAst = b(Node,_,_),
    ast_to_node_id(Node, NType, FirstVarId), % use stored type since it can e.g. be either set(couple(integer,boolean)) or seq(boolean)
    NFirstVarAst = b(Node,NType,[]),
    !,
    image_of_generator(Generator, FirstVarId, ImageId),
    node_id_to_ast(ImageId, ImageAst),
    get_texpr_expr(ImageAst, Id1),
    ( Id1 == Node
    -> % tautology
    add_sbps_from_generator(T, Generator, EnumeratedSets, Acc, NAcc)
    ; safe_create_texpr(equal(NFirstVarAst,ImageAst), pred, [], Eq),
    ( (
    \+ has_enumerated_set_type(NFirstVarAst, EnumeratedSets),
    less_eq_for_type_except_enumerated_set(NFirstVarAst, ImageAst, LEq)
    )
    -> extend_conj_acc(Acc, LEq, NAcc1)
    ; NAcc1 = Acc
    ),
    add_sbps_from_generator_eq_acc(T, Generator, Eq, EnumeratedSets, NAcc1, NAcc)
).

add_sbps_from_generator([FirstVarAst|_], _, _, _, _) :-
    add_warning(smt_symmetry_breaking, 'Missing node id in symmetry breaking graph for AST ', [FirstVarAst]), !,
    fail.

add_sbps_from_generator_eq_acc([], _, _, _, Acc, Acc).

add_sbps_from_generator_eq_acc([VarAst|T], Generator, EqAcc, EnumeratedSets, Acc, NAcc) :-
    VarAst = b(Node,_,_),
    ast_to_node_id(Node, NType, VarId),
    NVarAst = b(Node,NType,[]),
    image_of_generator(Generator, VarId, ImageId),
    node_id_to_ast(ImageId, ImageAst),
    get_texpr_expr(ImageAst, Id1),
    ( Id1 == Node
    -> % tautology
    add_sbps_from_generator_eq_acc(T, Generator, EqAcc, EnumeratedSets, Acc, NAcc)
    ; safe_create_texpr(equal(NVarAst,ImageAst), pred, [], Eq),
    ( (
    \+ has_enumerated_set_type(NVarAst, EnumeratedSets),
    less_eq_for_type_except_enumerated_set(NVarAst, ImageAst, LEq)
    )
    -> safe_create_texpr(negation(EqAcc), pred, [], NegEqAcc),
    safe_create_texpr(disjunct(NegEqAcc,LEq), pred, [], Impl),
    extend_conj_acc(Acc, Impl, NAcc1),
    safe_create_texpr(conjunct(EqAcc,Eq), pred, [], NEqAcc)
    ; NAcc1 = Acc,
    NEqAcc = EqAcc
    ),
    add_sbps_from_generator_eq_acc(T, Generator, NEqAcc, EnumeratedSets, NAcc1, NAcc)
).

add_sbps_from_generators([], _, _, Acc, Acc).

add_sbps_from_generators([Generator|T], VariableOrdering, EnumeratedSets, Acc, SBPs) :-
    add_sbps_from_generator(VariableOrdering, Generator, EnumeratedSets, Acc , NAcc),
    add_sbps_from_generators(T, VariableOrdering, EnumeratedSets, NAcc, SBPs).

add_sbps_to_quantifiers(b(Expr,Type,Info), EnumeratedSets, NSmtFormula) :-
    !,
    add_sbps_to_quantifiers_expr(Expr, EnumeratedSets, NExpr),
    safe_create_texpr(NExpr, Type, Info, NSmtFormula).

add_sbps_to_quantifiers(Formula, _, Formula).

add_sbps_to_quantifiers_expr(forall(Ids,Lhs,Rhs), EnumeratedSets, NExpr) :-
    !,
    get_top_level_symmetry_breaking_predicates(Rhs, EnumeratedSets, SBPs),
    log_found_sbps(SBPs),
    add_sbps_to_quantifiers(Rhs, EnumeratedSets, NRhs),
    ( SBPs = b(truth,pred,_)
    -> NExpr = forall(Ids,Lhs,NRhs)
    ; safe_create_texpr(conjunct(SBPs,Lhs), pred, [], NLhs),
    NExpr = forall(Ids,NLhs,NRhs)
).

add_sbps_to_quantifiers_expr(exists(Ids,Body), EnumeratedSets, NExpr) :-
    !,
    get_top_level_symmetry_breaking_predicates(Body, EnumeratedSets, SBPs),
    log_found_sbps(SBPs),
    add_sbps_to_quantifiers(Body, EnumeratedSets, NBody),
    ( SBPs = b(truth,pred,_)
    -> NExpr = exists(Ids,NBody)
    ; safe_create_texpr(conjunct(SBPs,NBody), pred, [], NNBody),
    NExpr = exists(Ids,NNBody)
).

add_sbps_to_quantifiers_expr(Expr, _, NExpr) :-
    ( is_interpreted_symbol(Expr)
    ; is_uninterpreted_symbol(Expr)
    ),
    !,
    NExpr = Expr.

add_sbps_to_quantifiers_expr(Expr, EnumeratedSets, NExpr) :-
    functor(Expr, Functor, 2),
    !,
    arg(1, Expr, Arg1),
    arg(2, Expr, Arg2),
    add_sbps_to_quantifiers(Arg1, EnumeratedSets, NArg1),
    add_sbps_to_quantifiers(Arg2, EnumeratedSets, NArg2),
    functor(NExpr, Functor, 2),
    arg(1, NExpr, NArg1),
    arg(2, NExpr, NArg2).

add_sbps_to_quantifiers_expr(Expr, EnumeratedSets, NExpr) :-
    functor(Expr, Functor, 1),
    !,
    arg(1, Expr, Arg),
    add_sbps_to_quantifiers(Arg, EnumeratedSets, NArg),
    functor(NExpr, Functor, 1),
    arg(1, NExpr, NArg).

add_sbps_to_quantifiers_expr(Expr, _, Expr).

add_symmetry_breaking_predicates(SmtFormula, NSmtFormula) :-
    reset_found_sbps,
    b_get_global_enumerated_sets(EnumeratedSets),
    safe_time_out(add_symmetry_breaking_predicates(SmtFormula, EnumeratedSets, NSmtFormula), 10000, TORes),
    ( TORes == time_out
    -> NSmtFormula = SmtFormula
    ; true
).

add_symmetry_breaking_predicates(SmtFormula, EnumeratedSets, NSmtFormula) :-
    ( get_top_level_symmetry_breaking_predicates(SmtFormula, EnumeratedSets, SymBreakPs)
    -> log_found_sbps(SymBreakPs)
    ; add_message(smt_symmetry_breaking, 'Skip top-level symmetry breaking due to failure'),
    SymBreakPs = b(truth,pred,[])
    ),
    add_sbps_to_quantifiers(SmtFormula, EnumeratedSets, TSmtFormula),
    safe_create_texpr(conjunct(SymBreakPs,TSmtFormula), pred, [] ,NSmtFormula).

add_term_and_symbol_nodes_to_graph(Term, Type, _, RootNodeId) :-
    is_interpreted_symbol(Term),
    ( have_seen_expr(Term, Type, TNodeId)
    -> TRootNodeId = TNodeId
    ; get_next_color(Color),
    term_to_label(Term, ATerm),
    bliss_interface:add_node(ATerm, Color, RootNodeId),
    log_seen_expr(Term, Type, RootNodeId)
    %asserta(ast_to_node_id(Term,Type,RootNodeId))
    %asserta(node_id_to_ast(RootNodeId,b(Term,Type,[])))
    ), !,
    RootNodeId = TRootNodeId.

add_term_and_symbol_nodes_to_graph(Term, Type, _, RootNodeId) :-
    is_uninterpreted_symbol(Term),
    ( have_seen_expr(Term, Type, TNodeId)
    -> TRootNodeId = TNodeId
    ; get_color_for_type(Type, Term, Color),
    term_to_label(Term, ATerm),
    bliss_interface:add_node(ATerm, Color, RootNodeId),
    log_seen_expr(Term, Type, RootNodeId),
    asserta(ast_to_node_id(Term,Type,RootNodeId)),
    asserta(node_id_to_ast(RootNodeId,b(Term,Type,[])))
    ), !,
    RootNodeId = TRootNodeId.

add_term_and_symbol_nodes_to_graph(Term, Type, Functor, RootNodeId) :-
    categorize_type(Type, Category, SymbolCategory),
    add_node_to_colored_graph(SymbolCategory, Functor, Type, SymbolNodeId),
    add_node_to_colored_graph(Category, Term, Type, RootNodeId),
    % add an edge from the root node to the symbol node
    bliss_interface:add_edge(RootNodeId, SymbolNodeId).

associative_ast_to_list(Functor, Expr, AstList) :-
    associative_ast_to_list(Functor, Expr, [], AstList).

associative_ast_to_list(Functor, b(Expr,_,_), Acc, AstList) :-
    functor(Expr, Functor, 2),
    !,
    arg(1, Expr, Arg1),
    arg(2, Expr, Arg2),
    associative_ast_to_list(Functor, Arg1, Acc, NAcc),
    associative_ast_to_list(Functor, Arg2, NAcc, AstList).

associative_ast_to_list(_, Ast, Acc, [Ast|Acc]).

build_colored_graph(SmtFormula) :-
    get_texpr_expr_functor_and_type(SmtFormula, Expr, Type, ExprFunctor),
    add_term_and_symbol_nodes_to_graph(Expr, Type, ExprFunctor, RootNodeId),
    build_colored_graph(Expr, Type, RootNodeId).

build_colored_graph(truth, pred, _) :-
    !.

build_colored_graph(falsity, pred, _) :-
    !.

build_colored_graph(Expr, _, RootNodeId) :-
    ( Expr = set_extension(List)
    ; Expr = sequence_extension(List)
    ; Expr = rec(List)
    ),
    !,
    build_colored_graph_from_set(List, RootNodeId).

build_colored_graph(Expr, Type, RootNodeId) :-
    ( Expr = let_predicate(Ids, EqVals, Body)
    ; Expr = let_expression(Ids, EqVals, Body)
    ; Expr = lazy_let_pred(Ids, EqVals, Body)
    ),
    !,
    % non-commutative
    zip_to_equalities_conj(Ids, EqVals, EqsConj),
    get_texpr_expr_functor_and_type(EqsConj, EqsExpr, EqsType, EqsFunctor),
    get_texpr_expr_functor_and_type(Body, BodyExpr, BodyType, BodyFunctor),
    add_term_and_symbol_nodes_to_graph(EqsExpr, EqsType, EqsFunctor, EqsRootNodeId),
    add_term_and_symbol_nodes_to_graph(BodyExpr, BodyType, BodyFunctor, BodyRootNodeId),
    add_node_to_colored_graph(arg, EqsExpr, EqsType, EqsNodeId),
    add_node_to_colored_graph(arg, BodyExpr, BodyType, BodyNodeId),
    bliss_interface:add_edge(EqsNodeId, EqsRootNodeId),
    bliss_interface:add_edge(BodyNodeId, BodyRootNodeId),
    bliss_interface:add_edge(EqsNodeId, BodyNodeId),
    bliss_interface:add_edge(RootNodeId, EqsNodeId),
    build_colored_graph(EqsExpr, EqsType, EqsRootNodeId),
    build_colored_graph(BodyExpr, Type, BodyRootNodeId).

build_colored_graph(partition(Set,AstList), _, RootNodeId) :-
    !,
    get_texpr_expr_functor_and_type(Set, SetExpr, SetType, SetFunctor),
    add_term_and_symbol_nodes_to_graph(SetExpr, SetType, SetFunctor, SetRootNodeId),
    add_nodes_from_ast_list_commutative(RootNodeId, AstList),
    add_node_to_colored_graph(arg, SetExpr, SetType, SetNodeId),
    bliss_interface:add_edge(SetNodeId, SetRootNodeId),
    bliss_interface:add_edge(RootNodeId, SetNodeId),
    build_colored_graph(SetExpr, SetType, SetRootNodeId).

build_colored_graph(if_then_else(Cond,If,Else), _, RootNodeId) :-
    % non-commutative
    !,
    get_texpr_expr_functor_and_type(Cond, CondExpr, CondType, CondFunctor),
    get_texpr_expr_functor_and_type(If, IfExpr, IfType, IfFunctor),
    get_texpr_expr_functor_and_type(Else, ElseExpr, ElseType, ElseFunctor),
    add_term_and_symbol_nodes_to_graph(CondExpr, CondType, CondFunctor, CondRootNodeId),
    add_term_and_symbol_nodes_to_graph(IfExpr, IfType, IfFunctor, IfRootNodeId),
    add_term_and_symbol_nodes_to_graph(ElseExpr, ElseType, ElseFunctor, ElseRootNodeId),
    add_node_to_colored_graph(arg, CondExpr, CondType, CondNodeId),
    add_node_to_colored_graph(arg, IfExpr, IfType, IfNodeId),
    add_node_to_colored_graph(arg, ElseExpr, ElseType, ElseNodeId),
    bliss_interface:add_edge(CondNodeId, CondRootNodeId),
    bliss_interface:add_edge(IfNodeId, IfRootNodeId),
    bliss_interface:add_edge(ElseNodeId, ElseRootNodeId),
    bliss_interface:add_edge(CondNodeId, IfNodeId),
    bliss_interface:add_edge(IfNodeId, ElseNodeId),
    bliss_interface:add_edge(RootNodeId, CondNodeId),
    build_colored_graph(CondExpr, CondType, CondRootNodeId),
    build_colored_graph(IfExpr, IfType, IfRootNodeId),
    build_colored_graph(ElseExpr, ElseType, ElseRootNodeId).

build_colored_graph(assertion_expression(Cond,_ErrMsg,Expr), _, RootNodeId) :-
    % non-commutative
    !,
    get_texpr_expr_functor_and_type(Cond, CondExpr, CondType, CondFunctor),
    get_texpr_expr_functor_and_type(Expr, ExprExpr, ExprType, ExprFunctor),
    add_term_and_symbol_nodes_to_graph(CondExpr, CondType, CondFunctor, CondRootNodeId),
    add_term_and_symbol_nodes_to_graph(ExprExpr, ExprType, ExprFunctor, ExprRootNodeId),
    add_node_to_colored_graph(arg, CondExpr, CondType, CondNodeId),
    add_node_to_colored_graph(arg, ExprExpr, ExprType, ExprNodeId),
    bliss_interface:add_edge(CondNodeId, CondRootNodeId),
    bliss_interface:add_edge(ExprNodeId, ExprRootNodeId),
    bliss_interface:add_edge(CondNodeId, ExprNodeId),
    bliss_interface:add_edge(RootNodeId, CondNodeId),
    build_colored_graph(CondExpr, CondType, CondRootNodeId),
    build_colored_graph(ExprExpr, ExprType, ExprRootNodeId).

build_colored_graph(forall(Ids,Lhs,Rhs), pred, RootNodeId) :-
    !,
    ( Lhs = b(truth,pred,_) % typing information might have been removed
    -> Body = Rhs
    ; Body = b(implication(Lhs,Rhs),pred,[])
    ),
    create_nodes_for_ids(Ids),
    get_texpr_expr_functor_and_type(Body, BodyExpr, BodyType, BodyFunctor),
    add_term_and_symbol_nodes_to_graph(BodyExpr, BodyType, BodyFunctor, ArgRootNodeId),
    add_node_to_colored_graph(arg, BodyExpr, BodyType, ArgNodeId),
    bliss_interface:add_edge(ArgNodeId, ArgRootNodeId),
    bliss_interface:add_edge(RootNodeId, ArgNodeId),
    build_colored_graph(BodyExpr, BodyType, ArgRootNodeId).

build_colored_graph(Expr, _, RootNodeId) :-
    ( Expr = comprehension_set(Ids,Body)
    ; Expr = exists(Ids,Body)
    ),
    !,
    create_nodes_for_ids(Ids),
    get_texpr_expr_functor_and_type(Body, BodyExpr, BodyType, BodyFunctor),
    add_term_and_symbol_nodes_to_graph(BodyExpr, BodyType, BodyFunctor, ArgRootNodeId),
    add_node_to_colored_graph(arg, BodyExpr, BodyType, ArgNodeId),
    bliss_interface:add_edge(ArgNodeId, ArgRootNodeId),
    bliss_interface:add_edge(RootNodeId, ArgNodeId),
    build_colored_graph(BodyExpr, BodyType, ArgRootNodeId).

build_colored_graph(Fun, _, RootNodeId) :-
    functor(Fun, Functor, 3),
    member(Functor, [lambda,general_sum,general_product,quantified_union,quantified_intersection]),
    arg(2, Fun, Pred),
    arg(3, Fun, LExpr),
    % non-commutative
    !,
    get_texpr_expr_functor_and_type(LExpr, LExprExpr, LExprType, LExprFunctor),
    get_texpr_expr_functor_and_type(Pred, PredExpr, PredType, PredFunctor),
    add_term_and_symbol_nodes_to_graph(LExpr, LExprExpr, LExprFunctor, LExprRootNodeId),
    add_term_and_symbol_nodes_to_graph(Pred, PredType, PredFunctor, PredRootNodeId),
    add_node_to_colored_graph(arg, LExprExpr, LExprType, LExprNodeId),
    add_node_to_colored_graph(arg, PredExpr, PredType, PredNodeId),
    bliss_interface:add_edge(LExprNodeId, LExprRootNodeId),
    bliss_interface:add_edge(PredNodeId, PredRootNodeId),
    bliss_interface:add_edge(LExprNodeId, PredNodeId),
    bliss_interface:add_edge(RootNodeId, LExprNodeId),
    build_colored_graph(LExprExpr, LExprType, LExprRootNodeId),
    build_colored_graph(PredExpr, PredType, PredRootNodeId).

build_colored_graph(record_field(Record, FieldName), Type, RootNodeId) :-
    % treated as a non-commutative operator but needs special case since the field name is just a Prolog atom and no B AST node
    !,
    get_texpr_expr_functor_and_type(Record, RecordExpr, RecordType, RecordFunctor),
    add_term_and_symbol_nodes_to_graph(RecordExpr, RecordType, RecordFunctor, RecordRootNodeId),
    ( have_seen_expr(FieldName, Type, TNodeId)
    -> FieldNameRootNodeId = TNodeId
    ; get_next_color(Color),
    bliss_interface:add_node(FieldName, Color, FieldNameRootNodeId),
    log_seen_expr(FieldName, Type, FieldNameRootNodeId)
    %asserta(ast_to_node_id(Term,Type,RootNodeId))
    %asserta(node_id_to_ast(RootNodeId,b(Term,Type,[])))
    ),
    add_node_to_colored_graph(arg, RecordExpr, RecordType, RecordNodeId),
    add_node_to_colored_graph(arg, FieldName, record_key, FieldNameNodeId), % use an artificial type record_key
    % one edge from the argument node to the argument's root node
    bliss_interface:add_edge(RecordNodeId, RecordRootNodeId),
    bliss_interface:add_edge(FieldNameNodeId, FieldNameRootNodeId),
    % edge from first to second argument to represent the ordering
    bliss_interface:add_edge(RecordNodeId, FieldNameNodeId),
    % add an edge from the root node to the first argument's argument node
    bliss_interface:add_edge(RootNodeId, RecordNodeId),
    build_colored_graph(RecordExpr, RecordType, RecordRootNodeId).

build_colored_graph(Binary, _Type, RootNodeId) :-
    functor(Binary, Functor, Arity),
    Arity == 2,
    is_associative(Functor),
    !,
    split_associative_node(Binary, AstList),
    add_nodes_from_ast_list_commutative(RootNodeId, AstList).

build_colored_graph(Binary, _Type, RootNodeId) :-
    functor(Binary, Functor, Arity),
    Arity == 2,
    \+ is_binary_interpreted_symbol(Binary),
    !,
    arg(1, Binary, Arg1),
    arg(2, Binary, Arg2),
    get_texpr_expr_functor_and_type(Arg1, Arg1Expr, Arg1Type, Arg1Functor),
    get_texpr_expr_functor_and_type(Arg2, Arg2Expr, Arg2Type, Arg2Functor),
    % root nodes for arguments
    add_term_and_symbol_nodes_to_graph(Arg1Expr, Arg1Type, Arg1Functor, Arg1RootNodeId),
    add_term_and_symbol_nodes_to_graph(Arg2Expr, Arg2Type, Arg2Functor, Arg2RootNodeId),
    ( is_commutative_but_not_associative(Functor)
    -> % add an edge from the root node to the root node of each argument
    bliss_interface:add_edge(RootNodeId, Arg1RootNodeId),
    bliss_interface:add_edge(RootNodeId, Arg2RootNodeId)
    ; % special argument node for each argument
    add_node_to_colored_graph(arg, Arg1Expr, Arg1Type, Arg1NodeId),
    add_node_to_colored_graph(arg, Arg2Expr, Arg2Type, Arg2NodeId),
    % one edge from the argument node to the argument's root node
    bliss_interface:add_edge(Arg1NodeId, Arg1RootNodeId),
    bliss_interface:add_edge(Arg2NodeId, Arg2RootNodeId),
    % edge from first to second argument to represent the ordering
    bliss_interface:add_edge(Arg1NodeId, Arg2NodeId),
    % add an edge from the root node to the first argument's argument node
    bliss_interface:add_edge(RootNodeId, Arg1NodeId)
    ),
    build_colored_graph(Arg1Expr, Arg1Type, Arg1RootNodeId),
    build_colored_graph(Arg2Expr, Arg2Type, Arg2RootNodeId).

build_colored_graph(Term, _, _) :-
    ( is_interpreted_symbol(Term)
    ; is_uninterpreted_symbol(Term)
    ),
    !.

build_colored_graph(Unary, _Type, RootNodeId) :-
    functor(Unary, _Functor, Arity),
    Arity == 1,
    !,
    arg(1, Unary, Arg),
    get_texpr_expr_functor_and_type(Arg, ArgExpr, ArgType, ArgFunctor),
    % root node for argument
    add_term_and_symbol_nodes_to_graph(ArgExpr, ArgType, ArgFunctor, ArgRootNodeId),
    % special argument node for each argument
    add_node_to_colored_graph(arg, ArgExpr, ArgType, ArgNodeId),
    % one edge from the argument node to the argument's root node
    bliss_interface:add_edge(ArgNodeId, ArgRootNodeId),
    % add an edge from the root node to the first argument's argument node
    bliss_interface:add_edge(RootNodeId, ArgNodeId),
    build_colored_graph(ArgExpr, ArgType, ArgRootNodeId).

build_colored_graph(Expr, _Type, _ExprRootNodeId) :-
    add_warning(smt_symmetry_breaking, 'Missing implementation in build_colored_graph/3 for: ', [Expr]), !,
    fail.

build_colored_graph_from_set([], _).

build_colored_graph_from_set([Elm|T], RootNodeId) :-
    % commutative
    ( Elm = field(_,FieldElm) % Note: we treat records as sets for symmetry breaking, i.e., it's just a collection with no order
    -> get_texpr_expr_functor_and_type(FieldElm, ElmExpr, ElmType, ElmFunctor)
    ; get_texpr_expr_functor_and_type(Elm, ElmExpr, ElmType, ElmFunctor)
    ),
    add_term_and_symbol_nodes_to_graph(ElmExpr, ElmType, ElmFunctor, ElmRootNodeId),
    bliss_interface:add_edge(RootNodeId, ElmRootNodeId),
    build_colored_graph(ElmExpr, ElmType, ElmRootNodeId),
    build_colored_graph_from_set(T, RootNodeId).

categorize_type(Type, Category, SymbolCategory) :-
    Type == pred,
    !,
    Category = pred,
    SymbolCategory = upred.

categorize_type(_, expr, uexpr).

cmp_typed_identifier(b(identifier(Id1),_,_), b(identifier(Id2),_,_)) :-
    Id1 @< Id2.

create_nodes_for_ids([]).

create_nodes_for_ids([b(identifier(Id),Type,_)|T]) :-
    add_term_and_symbol_nodes_to_graph(identifier(Id), Type, identifier, _),
    create_nodes_for_ids(T).

expr_functor(b(Expr,_,_), Functor) :-
    !,
    functor(Expr, Functor, _).

expr_functor(Expr, Functor) :-
    functor(Expr, Functor, _).

extend_conj_acc(b(truth,pred,[]), TConj, Conj) :-
    !,
    Conj = TConj.

extend_conj_acc(Acc, Conj, b(conjunct(Acc,Conj),pred,[])).

extend_type_acc(Acc, Type, TypedVar, NAcc) :-
    select((Type,TypedVars), Acc, RAcc),
    !,
    NAcc = [(Type,[TypedVar|TypedVars])|RAcc].

extend_type_acc(Acc, Type, TypedVar, NAcc) :-
    NAcc = [(Type,[TypedVar])|Acc].

found_sbps(0).

get_amount_of_found_sbps(FoundSBPs) :-
    found_sbps(FoundSBPs).

get_color_for_type(Type, _, Color) :-
    color(Type, TColor),
    !,
    Color = TColor.

get_color_for_type(Type, _, Color) :-
    get_next_color(Color),
    asserta(color(Type,Color)).

get_next_color(Color) :-
    retract(next_color(Color)),
    Color1 is Color + 1,
    asserta(next_color(Color1)).

get_sbps_from_generators(Generators, VariableOrdering, EnumeratedSets, SBPs) :-
    add_sbps_from_generators(Generators, VariableOrdering, EnumeratedSets, b(truth,pred,[]), SBPs).

get_texpr_expr_functor_and_type(b(Expr,Type,_), Expr, Type, Functor) :-
    functor(Expr, Functor, _).

get_top_level_symmetry_breaking_predicates(SmtFormula, EnumeratedSets, SBPs) :-
    get_top_level_symmetry_breaking_predicates(SmtFormula, EnumeratedSets, SBPs, _).

get_top_level_symmetry_breaking_predicates(SmtFormula, EnumeratedSets, SBPs, Generators) :-
    find_typed_identifier_uses(SmtFormula, [], UsedIds),
    remove_all_infos_and_ground(SmtFormula, CSmtFormula),
    order_variables(UsedIds, _TypeOrdering, VariableOrdering),
    ( VariableOrdering == []
    -> SBPs = b(truth,pred,[])
    ; init_graph,
    build_colored_graph(CSmtFormula),
    %graph_to_dot_file('sym_graph.dot'),
    !,
    bliss_interface:find_automorphisms(TGenerators),
    %nl, write('Generators: '), write(Generators),nl,
    get_sbps_from_generators(TGenerators, VariableOrdering, EnumeratedSets, TSBPs),
    !,
    SBPs = TSBPs,
    Generators = TGenerators
).

get_top_level_symmetry_breaking_predicates_decomposed(SmtFormula, SBPs) :-
    ( SmtFormula = b(truth,pred,_)
    ; SmtFormula = b(falsity,pred,_)
    ),
    !,
    SBPs = b(truth,pred,[]).

get_top_level_symmetry_breaking_predicates_decomposed(SmtFormula, SBPs) :-
    findall(DeferredSetId, b_get_machine_set(DeferredSetId), DeferredSetIds),
    predicate_components_in_scope(SmtFormula, DeferredSetIds, Components),
    b_get_global_enumerated_sets(EnumeratedSets),
    get_top_level_symmetry_breaking_predicates_from_components(Components, EnumeratedSets, SBPs).

get_top_level_symmetry_breaking_predicates_from_components([component(SingleComponent,_)|T], EnumeratedSets, SBPs) :-
    reset_found_sbps,
    get_top_level_symmetry_breaking_predicates(SingleComponent, EnumeratedSets, CSBPs),
    log_found_sbps(CSBPs),
    get_top_level_symmetry_breaking_predicates_from_components(T, CSBPs, EnumeratedSets, SBPs).

get_top_level_symmetry_breaking_predicates_from_components([], Acc, _, Acc).

get_top_level_symmetry_breaking_predicates_from_components([component(SingleComponent,_)|T], Acc, EnumeratedSets, SBPs) :-
    get_top_level_symmetry_breaking_predicates(SingleComponent, EnumeratedSets, CSBPs),
    log_found_sbps(CSBPs),
    conjunct_predicates([Acc,CSBPs], NAcc),
    get_top_level_symmetry_breaking_predicates_from_components(T, NAcc, EnumeratedSets, SBPs).

has_enumerated_set_type(b(_,Type,_), EnumeratedSets) :-
    Type = global(EnumSet),
    member(EnumSet, EnumeratedSets).

have_seen_expr(Term, Type, NodeId) :-
    norm_expr_check(b(Term,Type,[]), Norm),
    seen_expr(Norm, NodeId).

have_seen_pred(Term, NodeId) :-
    norm_pred_check(b(Term,pred,[]), Norm),
    seen_pred(Norm, NodeId).

image_of_cycle(true, [Id], ImageId, Id, ImageId).

image_of_cycle(false, [Id], _, Id, Id).

image_of_cycle(_, [Id,TImageId|_], _, Id, ImageId) :-
    ImageId = TImageId.

image_of_cycle(MapLastToFirst, [_|T], FirstCycleId, Id, ImageId) :-
    image_of_cycle(MapLastToFirst, T, FirstCycleId, Id, ImageId).

image_of_cycle(MapLastToFirst, [FirstCycleId|T], Id, ImageId) :-
    image_of_cycle(MapLastToFirst, [FirstCycleId|T], FirstCycleId, Id, ImageId).

image_of_generator([], Id, Id). % identity

image_of_generator([Cycle|_], Id, ImageId) :-
    image_of_cycle(false, Cycle, Id, TImageId),
    !,
    ImageId = TImageId.

image_of_generator([_|T], Id, ImageId) :-
    image_of_generator(T, Id, ImageId).

init_graph :-
    bliss_interface:init_bliss_interface,
    bliss_interface:init_directed_graph,
    retractall(node_id_to_ast(_,_)),
    retractall(ast_to_node_id(_,_,_)),
    retractall(seen_pred(_,_)),
    retractall(seen_upred(_,_)),
    retractall(seen_expr(_,_)),
    retractall(seen_uexpr(_,_)),
    retractall(color(_,_)),
    asserta(color(arg, 0)), % all argument nodes have the same unique color
    retractall(next_color(_)),
    asserta(next_color(1)).

is_associative(conjunct).

is_associative(disjunct).

is_associative(add).

is_associative(multiplication).

is_associative(union).

is_associative(intersection).

is_binary_interpreted_symbol(interval(A,B)) :-
    is_interpreted_symbol(A),
    is_interpreted_symbol(B).

is_commutative_but_not_associative(equivalence).

is_commutative_but_not_associative(equal).

is_commutative_but_not_associative(not_equal).

is_interpreted_symbol(Symbol) :-
    is_binary_interpreted_symbol(Symbol).

is_interpreted_symbol(boolean_true).

is_interpreted_symbol(boolean_false).

is_interpreted_symbol(max_int).

is_interpreted_symbol(min_int).

is_interpreted_symbol(empty_set).

is_interpreted_symbol(empty_sequence).

is_interpreted_symbol(bool_set).

is_interpreted_symbol(real_set).

is_interpreted_symbol(float_set).

is_interpreted_symbol(string_set).

is_interpreted_symbol(real(_)).

is_interpreted_symbol(integer(_)).

is_interpreted_symbol(string(_)).

is_interpreted_symbol(value(_)).

is_interpreted_symbol(integer_set(_)).

is_interpreted_symbol(event_b_identity).

is_uninterpreted_symbol(identifier(_)).

less_eq_for_type_except_enumerated_set(VarAst, ImageAst, LEq) :-
    OrderedList = [VarAst,ImageAst],
    LEq = b(external_pred_call('LEQ_SYM', OrderedList),pred,[]).

less_eq_for_type_except_enumerated_set(VarAst, ImageAst, _) :-
    VarAst = b(_,TypeA,_),
    ImageAst = b(_,TypeB,_),
    TypeA \== TypeB,
    % don't throw an error here since we fail and CDCL(T) can try to solve without symmetry breaking
    add_warning(less_eq_for_type_except_enumerated_set, 'Differently typed permutation mapping. Encoding for SMT symmetry breaking is defective.', [VarAst,ImageAst]), !,
    fail.

log_found_sbps(SymBreakPs) :-
    SymBreakPs \= b(truth,pred,_),
    conjunction_to_list(SymBreakPs, L),
    length(L, Len),
    retract(found_sbps(FoundSBPs)),
    NFoundSBPs is FoundSBPs + Len,
    asserta(found_sbps(NFoundSBPs)).

log_found_sbps(_).

log_seen_expr(Term, Type, RootNodeId) :-
    norm_expr_check(b(Term,Type,[]), Norm),
    asserta(seen_expr(Norm, RootNodeId)).

log_seen_pred(Term, RootNodeId) :-
    norm_pred_check(b(Term,pred,[]), Norm),
    asserta(seen_pred(Norm, RootNodeId)).

order_variables(TypedVars, TypeOrdering, VariableOrdering) :-
    order_variables_by_type(TypedVars, [], VarsOrderedByType),
    order_variables_within_typed_group(VarsOrderedByType, [], [], TypeOrdering, VariableOrdering).

order_variables_by_type([], Acc, Acc).

order_variables_by_type([TypedVar|T], Acc, VarsOrderedByType) :-
    TypedVar = b(_,Type,_),
    extend_type_acc(Acc, Type, TypedVar, NAcc),
    order_variables_by_type(T, NAcc, VarsOrderedByType).

order_variables_within_typed_group([], VAcc, TAcc, TAcc, VAcc).

order_variables_within_typed_group([(Type,TypeVars)|T], VAcc, TAcc, TypeOrdering, VariableOrdering) :-
    samsort(cmp_typed_identifier, TypeVars, STypeVars),
    append(STypeVars, VAcc, NVAcc),
    order_variables_within_typed_group(T, NVAcc, [Type|TAcc], TypeOrdering, VariableOrdering).

reset_found_sbps :-
    retractall(found_sbps(_)),
    asserta(found_sbps(0)).

split_associative_node(conjunct(A,B), AstList) :-
    !,
    conjunction_to_list(b(conjunct(A,B),pred,[]), AstList).

split_associative_node(disjunct(A,B), AstList) :-
    !,
    disjunction_to_list(b(disjunct(A,B),pred,[]), AstList).

split_associative_node(Expr, AstList) :-
    functor(Expr, Functor, 2),
    member(Functor, [add,multiplication,union,intersection]),
    associative_ast_to_list(Functor, b(Expr,_,_), AstList).

term_to_label(Term, Atom) :-
    Term =.. [Functor|Args],
    maplist(expr_functor, Args, ArgFunctors),
    NTerm =.. [Functor|ArgFunctors],
    write_to_codes(NTerm, Codes),
    atom_codes(Atom, Codes).

test(order_variables_empty, [true((VariableOrdering == ExpectedVars, TypeOrdering == ExpectedTypes))]) :-
    Variables = [],
    order_variables(Variables, TypeOrdering, VariableOrdering),
    ExpectedVars = [],
    ExpectedTypes = [].

test(order_variables_single_type, [true((VariableOrdering == ExpectedVars, TypeOrdering == ExpectedTypes))]) :-
    Variables = [b(identifier(c),integer,[]),b(identifier(a),integer,[]),b(identifier(b),integer,[])],
    order_variables(Variables, TypeOrdering, VariableOrdering),
    ExpectedVars = [b(identifier(a),integer,[]),b(identifier(b),integer,[]),b(identifier(c),integer,[])],
    ExpectedTypes = [integer].

test(order_variables_two_types, [true((VariableOrdering == ExpectedVars, TypeOrdering == ExpectedTypes))]) :-
    Variables = [b(identifier(c),integer,[]),b(identifier(d),set(integer),[]),b(identifier(a),integer,[]),b(identifier(e),set(integer),[]),b(identifier(b),integer,[]),b(identifier(f),set(integer),[])],
    order_variables(Variables, TypeOrdering, VariableOrdering),
    ExpectedVars = [b(identifier(a),integer,[]),b(identifier(b),integer,[]),b(identifier(c),integer,[]),b(identifier(d),set(integer),[]),b(identifier(e),set(integer),[]),b(identifier(f),set(integer),[])],
    ExpectedTypes = [integer,set(integer)].

test(order_variables_two_types_set_first, [true((VariableOrdering == ExpectedVars, TypeOrdering == ExpectedTypes))]) :-
    Variables = [b(identifier(d),set(integer),[]),b(identifier(a),integer,[])],
    order_variables(Variables, TypeOrdering, VariableOrdering),
    ExpectedVars = [b(identifier(d),set(integer),[]),b(identifier(a),integer,[])],
    ExpectedTypes = [set(integer),integer].

test(order_variables_two_types_integer_first, [true((VariableOrdering == ExpectedVars, TypeOrdering == ExpectedTypes))]) :-
    Variables = [b(identifier(a),integer,[]),b(identifier(d),set(integer),[])],
    order_variables(Variables, TypeOrdering, VariableOrdering),
    ExpectedVars = [b(identifier(a),integer,[]),b(identifier(d),set(integer),[])],
    ExpectedTypes = [integer,set(integer)].

test(order_variables_three_types, [true((VariableOrdering == ExpectedVars, TypeOrdering == ExpectedTypes))]) :-
    Variables = [b(identifier(c),integer,[]),b(identifier(d),set(integer),[]),b(identifier(a),integer,[]),b(identifier(e),set(integer),[]),b(identifier(b),integer,[]),b(identifier(f),set(set(string)),[])],
    order_variables(Variables, TypeOrdering, VariableOrdering),
    ExpectedVars = [b(identifier(d),set(integer),[]),b(identifier(e),set(integer),[]),b(identifier(a),integer,[]),b(identifier(b),integer,[]),b(identifier(c),integer,[]),b(identifier(f),set(set(string)),[])],
    ExpectedTypes = [set(integer),integer,set(set(string))].

zip_to_equalities_conj([Id|T], [EqVal|VT], Eqs) :-
    zip_to_equalities_conj(T, VT, b(equal(Id,EqVal),pred,[]), Eqs).

zip_to_equalities_conj([], [], Acc, Acc).

zip_to_equalities_conj([Id|T], [EqVal|VT], Acc, Eqs) :-
    safe_create_texpr(conjunct(b(equal(Id,EqVal),pred,[]),Acc), pred, [], NAcc),
    zip_to_equalities_conj(T, VT, NAcc, Eqs).