Engine.fs

module Engine

//--------------------------------------------------------------------

open System.Diagnostics
open System.Collections.Generic

open Common
open IndMap
open PrettyPrinting
open Background

//--------------------------------------------------------------------

let trace = ref 0
let level = ref 0
let module_name = "Engine"

let trace_smt_calls = false

let spaces () =
    let rec F level = if level = 0 then "" else "  " + F (level-1)
    F !level
    
let indent ppt = 
    let rec F level ppt = if level = 0 then ppt else blo2 [ F (level-1) ppt ]
    toString 120 (F !level ppt)

//--------------------------------------------------------------------

let always_unfold_guards = true

//--------------------------------------------------------------------

type FUNCTION_INTERPRETATION =
|   Constructor of (VALUE list -> VALUE)
|   StaticBackground of (VALUE list -> VALUE)
|   StaticUserDefined of (VALUE list -> VALUE) * (string list * TERM) option
|   ControlledInitial of (VALUE list -> VALUE) * (string list * TERM) option
|   ControlledUninitialized
|   Derived of (string list * TERM) option             // string list is the list of arguments, TERM is the body of the derived function

and FUNCTION' =
    FctName of string

and FUNCTION_ATTRS = {
    fct_id    : int;
    fct_kind  : Signature.FCT_KIND;
    fct_types : (TYPE list * TYPE) list;   // !!! to be implemented together with monomorphization
    fct_interpretation : FUNCTION_INTERPRETATION
}

and FCT_ID =
|   FctId of int

and RULE_DEF' =
    RuleName of string

and RULE_DEF_ATTRS = {
    rule_def_id   : int;
    // rule_type : (TYPE list * TYPE);   // !!! to be implemented together with monomorphization
    rule_def  : (string list * RULE) option
}
and RULE_DEF_ID =
|   RuleDefId of int

and ENGINE' = {
    signature       : Signature.SIGNATURE
    initial_state   : State.STATE         // use only for initial state in this module, never use '_dynamic' field - also the second elem. of _dynamic_initial seems not to be used !
    invariants      : Map<string, TERM>   // Added invariants field

    functions       : IndMap<FUNCTION', FUNCTION_ATTRS>
    rule_defs       : IndMap<RULE_DEF', RULE_DEF_ATTRS>
    types           : IndMap<TYPE', TYPE_ATTRS>
    terms           : IndMap<TERM', TERM_ATTRS>
    rules           : IndMap<RULE', RULE_ATTRS>
    supds           : IndMap<S_UPDATE_SET', S_UPDATE_SET_ATTRS>

    TRUE_           : TERM option ref
    FALSE_          : TERM option ref
    AND_            : FCT_ID option ref
    OR_             : FCT_ID option ref
    NOT_            : FCT_ID option ref
    EQUALS_         : FCT_ID option ref
    BOOLEAN_TYPE_   : TYPE option ref

    smt_ctx         : SmtInterface.SMT_CONTEXT
}

and ENGINE = Engine of int

and ENGINES = ResizeArray<ENGINE'>

and TYPE = Type of int

and TYPE' =
| Boolean'
| Integer'
| String'
| Undef'
| Rule'
| TypeParam' of string
| TypeCons' of string * TYPE list
| Subset' of string * TYPE
| Prod' of TYPE list
| Seq' of TYPE
| Powerset' of TYPE
| Bag' of TYPE
| Map' of TYPE * TYPE

and TYPE_ATTRS = {
    type_id : int
    signature_type : Signature.TYPE
    carrier_set : VALUE Set option
}

and TERM' =
|   Value'      of (VALUE)                  // used for special purposes (symbolic evaluation): "partially interpreted term", not an actual term of the language
|   Initial'    of (FCT_ID * VALUE list)    // used for special purposes (symbolic evaluation): "partially interpreted term", not an actual term of the language
|   AppTerm'    of (FCT_ID * TERM list)
|   CondTerm'   of (TERM * TERM * TERM)
|   TupleTerm'  of (TERM list)
|   VarTerm'    of (string * TYPE)
|   QuantTerm'  of (AST.QUANT_KIND * string * TERM * TERM)
|   LetTerm'    of (string * TERM * TERM)
|   DomainTerm' of TYPE                  // AsmetaL construct: finite type (e.g. enum, abstract, subsetof) used as finite set
|   UnfoldedTerm' of ((FCT_ID * VALUE list) * Map<VALUE, TERM>)   // not a part of the language, used internally for unfolding transformation
//  | TupleTerm   of 'annotation * ('annotation ANN_TERM list)

and TERM = Term of int

and TERM_ATTRS = {
    term_id       : int
    term_type     : TYPE
    smt_expr      : SmtInterface.SMT_EXPR option ref
    smt_result    : Dictionary<int, TERM>
    initial_state_eval_res : TERM option ref     // (symbolic) value of the term in the initial state, used also for static functions
}

and TERM_INDUCTION<'fct_id, 'term> = {
    Value      : (VALUE) -> 'term;
    Initial    : ('fct_id * VALUE list) -> 'term;
    AppTerm    : ('fct_id * 'term list) -> 'term;
    CondTerm   : ('term * 'term * 'term) -> 'term;
    TupleTerm  : ('term list) -> 'term;
    VarTerm    : (string * TYPE) -> 'term;
    QuantTerm  : (AST.QUANT_KIND * string * 'term * 'term) -> 'term;
    LetTerm    : (string * 'term * 'term) -> 'term;
    DomainTerm : (TYPE) -> 'term;
    UnfoldedTerm : (('fct_id * VALUE list) * Map<VALUE, 'term>) -> 'term;
}

and S_UPDATE_SET' = Set<(FCT_ID * VALUE list) * TERM>
and S_UPDATE_SET  = S_UpdateSet of int
and S_UPDATE_SET_ATTRS = { s_update_set_id : int }

and RULE' =
|   S_Updates' of S_UPDATE_SET     //Map<FCT_NAME * VALUE list, TERM>   // used for special purposes (symbolic evaluation): "partially interpreted rules", not actual rules of the language
|   UpdateRule' of (FCT_ID * TERM list) * TERM
|   CondRule' of TERM * RULE * RULE
|   ParRule' of RULE list
|   SeqRule' of RULE list
|   IterRule' of RULE
|   LetRule' of string * TERM * RULE
|   ForallRule' of string * TERM * TERM * RULE
|   MacroRuleCall' of RULE_DEF_ID * TERM list
|   UnfoldedRule'  of ((FCT_ID * VALUE list) * Map<VALUE, RULE>)   // not a part of the language, used internally for unfolding transformation


and RULE = Rule of int

and RULE_ATTRS = unit

and RULE_INDUCTION<'term, 'rule> = {
    S_Updates : S_UPDATE_SET -> 'rule;
    UpdateRule : (FCT_ID * 'term list) * 'term -> 'rule;
    CondRule : 'term * 'rule * 'rule -> 'rule;
    ParRule : 'rule list -> 'rule;
    SeqRule : 'rule list -> 'rule;
    IterRule : 'rule -> 'rule;
    LetRule : string * 'term * 'rule -> 'rule;
    ForallRule : string * 'term * 'term * 'rule -> 'rule;
    MacroRuleCall : RULE_DEF_ID * 'term list -> 'rule;     // Map<FCT_NAME * VALUE list, 'term> -> 'rule;
    UnfoldedRule  : ((FCT_ID * VALUE list) * Map<VALUE, 'rule>) -> 'rule;
}

and FCT_DEF_DB = Map<Signature.FCT_NAME, string list * TERM>    // for function definitions
and RULE_DEF_DB = Map<Signature.RULE_NAME, string list * RULE>     // for rule macros

and LOCATION = FCT_ID * VALUE list

and UPDATE = LOCATION * TERM
and UPDATE_SET = Set<UPDATE>
and UPDATE_MAP = Map<FCT_ID, Map<VALUE list, TERM>>

and ENV = Map<string, TERM>

and PATH_COND = Set<TERM> * UPDATE_MAP

and ErrorDetails = ENGINE * string * ErrorDetails'

and ErrorDetails' =
// type errors
|   TypeMismatch of TYPE * TYPE
|   FunctionCallTypeMismatch of (string * TYPE list * TYPE) * TYPE list
|   RuleCallTypeMismatch of string * TYPE list * TYPE list
|   TypeOfResultUnknown of string * TYPE list * TYPE
|   NoMatchingFunctionType of string * TYPE list
|   AmbiguousFunctionCall of string * TYPE list
|   NotAFunctionName of string
|   VariableAlreadyInUse of string
|   UnknownVariable of string
// runtime errors
|   InconsistentUpdates of ENGINE * TERM list option * UPDATE * UPDATE * UPDATE_SET option


let engines = new ENGINES()


exception Error of ErrorDetails

let rec error_msg ((eng, fct_name, details) : ErrorDetails) =
    let type_to_string, type_list_to_string = type_to_string eng, type_list_to_string eng
    (sprintf "error in function Engine.%s:\n" fct_name) +
    match details with
    // type errors
    |   TypeMismatch (ty, ty_sign) ->
            sprintf "type mismatch: %s does not match %s" (ty |> type_to_string) (ty_sign |> type_to_string)
    |   FunctionCallTypeMismatch ((fct_name, sign_args_types, sign_res_type), args_types) ->
            sprintf "function '%s : %s -> %s' called with arguments of type(s): %s"
                fct_name (sign_args_types |> type_list_to_string) (sign_res_type |> type_to_string) (args_types |> type_list_to_string)
    |   RuleCallTypeMismatch (rname, def_args_types, sign_rule_types) ->
            sprintf "rule macro '%s'\n  expecting arguments of type(s):   (%s)\n  called with arguments of type(s): (%s)"
                rname (sign_rule_types |> type_list_to_string) (def_args_types |> type_list_to_string)
    |   TypeOfResultUnknown (fct_name, sign_args_types, sign_res_type) ->
            sprintf "type of result of function %s : %s -> %s is unknown (type parameter '%s cannot be instantiated)"
                fct_name (sign_args_types |> type_list_to_string) (sign_res_type |> type_to_string) (sign_res_type |> type_to_string)
    |   NoMatchingFunctionType (fct_name, args_types) ->
            sprintf "no matching function type found for '%s' with arguments of type(s) (%s)" fct_name (args_types |> type_list_to_string)
    |   AmbiguousFunctionCall (fct_name, args_types) ->
            sprintf "ambiguous function call: multiple matching function types found for '%s' with arguments of type(s) %s" fct_name (args_types |> type_list_to_string)
    |   NotAFunctionName name ->
            sprintf "there is no function name '%s' in the signature" name
    |   VariableAlreadyInUse v ->
            sprintf "variable '%s' already in use" v
    |   UnknownVariable v ->
            sprintf "unknown variable '%s'" v
    // runtime errors
    |   InconsistentUpdates (eng, opt_conditions, u1, u2, opt_u_set) ->
            (   sprintf "\n--- inconsistent updates:\n%s\n%s\n" (show_s_update eng u1) (show_s_update eng u2) ) +
            (   match opt_conditions with    
                |   None -> ""
                |   Some ts ->
                        sprintf "\n--- initial state conditions leading to the inconsistent updates:\n%s\n"
                            (String.concat "\n" (ts >>| term_to_string eng)) ) +
            (   match opt_u_set with
                |   None -> ""
                |   Some U ->
                        sprintf "\n--- updates collected on this path so far:\n%s\n" (String.concat "\n" (List.map (show_s_update eng) (List.ofSeq U))) )

and type'_to_string eng (ty' : TYPE') =
    let type_to_string, type_list_to_string = type_to_string eng, type_list_to_string eng
    match ty' with
    |   TypeParam' a -> "'" ^ a
    |   Undef' -> "Undef"
    |   Boolean' -> "Boolean"
    |   Integer' -> "Integer"
    |   String' -> "String"
    |   Rule' -> "Rule"
    |   TypeCons' (s, tys)  -> if List.isEmpty tys then s else s ^ "(" ^ (tys |> type_list_to_string) ^ ")"
    |   Subset' (tyname, main_type) -> (tyname) ^ " subsetof " ^ (type_to_string main_type)
    |   Prod' tys -> "Prod(" ^ (tys |> type_list_to_string) ^ ")"
    |   Seq' ty -> "Seq(" ^ (type_to_string ty) ^ ")"
    |   Powerset' ty -> "Powerset(" ^ (type_to_string ty) ^ ")"
    |   Bag' ty -> "Bag(" ^ (type_to_string ty) ^ ")"
    |   Map' (ty1, ty2) -> "Map(" ^ (type_to_string ty1) ^ ", " ^ (type_to_string ty2) ^ ")"

and type_to_string eng ty =
    type'_to_string eng (get_type' eng ty)

and type_list_to_string (eng : ENGINE) tys =
    tys >>| type_to_string eng |> String.concat ", "

and fct_type_to_string (eng : ENGINE) (args_type, res_type) =
    sprintf "%s -> %s" (args_type |> type_list_to_string eng) (res_type |> type_to_string eng)

and inline get_signature (Engine eid) : Signature.SIGNATURE =
    engines.[eid].signature

and inline get_fct_id (Engine eid) (name : string) : FCT_ID =
    match engines.[eid].functions |> try_get_index (FctName name) with
    | Some fct_id -> FctId fct_id
    | None -> failwith (sprintf "Engine.get_fct_id: function '%s' not found in global context #%d" name eid)

and inline get_function' (Engine eid) (FctId id) : FUNCTION' * FUNCTION_ATTRS =
    engines.[eid].functions |> get id

and inline fct_name eng fct_id = let (FctName name) = fst (get_function' eng fct_id) in name
and inline fct_kind eng fct_id = (snd (get_function' eng fct_id)).fct_kind
and inline fct_types eng fct_id = (snd (get_function' eng fct_id)).fct_types
and inline fct_interpretation eng fct_id = (snd (get_function' eng fct_id)).fct_interpretation

and inline make_type (eng as Engine eid : ENGINE) (ty' : TYPE') (opt_sign_type : Signature.TYPE option) : TYPE =
    let enum_elems (ty' : TYPE') (S : State.STATE) : VALUE Set option =
        match ty' with
        |   Boolean' -> Some State.boolean_carrier_set
        |   Integer' -> None
        |   String'  -> None
        |   Undef'   -> Some State.undef_carrier_set
        |   Rule' ->
                try Some (Option.get (Map.find "Rule" S._carrier_sets))
                with _ -> failwith "SymbState.enum_finite_type: carrier set of 'Rule' not found or not defined"  // not found: not in map; not defined: None
        |   TypeParam' _ -> None
        |   TypeCons' (tyname, []) ->
                try Some (Option.get (Map.find tyname S._carrier_sets))
                with _ -> failwith (sprintf "SymbState.enum_finite_type: carrier set of '%s' not found" tyname)
        |   Subset' (tyname, _) ->
                try Some (Option.get (Map.find tyname S._carrier_sets))
                with _ -> failwith (sprintf "SymbState.enum_finite_type: carrier set of '%s' not found" tyname)
        |   TypeCons' (tyname, _)  -> failwith (sprintf "SymbState.enum_finite_type: not yet implemented for user-defined type '%s' with type arity > 0" tyname)
        |   Prod' tys ->
                let list_option_list = tys >>| enum_finite_type eng
                match List.foldBack (fun head tail -> 
                                            tail |> Option.bind (fun t -> 
                                            head |> Option.map (fun h -> h::t))
                                        ) list_option_list (Some []) with
                |   Some lists -> ((Common.product_of_lists (lists >>| Set.toList)) >>| TUPLE) |> Set.ofList |> Some
                |   None -> None
        |   Seq' _   -> failwith (sprintf "SymbState.enum_finite_type: not yet implemented for 'Seq' types")
        |   Powerset' _ -> failwith (sprintf "SymbState.enum_finite_type: not yet implemented for 'Powerset' types")
        |   Bag' _ -> failwith (sprintf "SymbState.enum_finite_type: not yet implemented for 'Bag' types")
        |   Map' _ -> failwith (sprintf "SymbState.enum_finite_type: not yet implemented for 'Map' types")
    let rec type'_to_sign_type (ty' : TYPE') : Signature.TYPE =
        let type_to_sign_type ty = type'_to_sign_type (get_type' eng ty)
        match ty' with
        |   Boolean' -> Signature.Boolean
        |   Integer' -> Signature.Integer
        |   String'  -> Signature.String
        |   Undef'   -> Signature.Undef
        |   Rule'    -> Signature.Rule
        |   TypeParam' name -> Signature.TypeParam name
        |   TypeCons' (tyname, ty_args) -> Signature.TypeCons (tyname, ty_args |> List.map type_to_sign_type)
        |   Subset' (tyname, main_ty) -> Signature.Subset (tyname, type_to_sign_type main_ty)
        |   Prod' ty_elems -> Signature.Prod (ty_elems |> List.map (type_to_sign_type))
        |   Seq' elem_ty -> Signature.Seq (type_to_sign_type elem_ty)
        |   Powerset' elem_ty -> Signature.Powerset (type_to_sign_type elem_ty)
        |   Bag' elem_ty -> Signature.Bag (type_to_sign_type elem_ty)
        |   Map' (dom_ty, rng_ty) -> Signature.Map (type_to_sign_type dom_ty, type_to_sign_type rng_ty)
    match IndMap.try_get_index ty' engines.[eid].types with
    |   Some type_id ->
            Type type_id
    |   None ->
            let e = engines.[eid]
            let type_id = e.types |> count
            let attrs = {
                type_id = type_id;
                signature_type = match opt_sign_type with Some sign_ty -> sign_ty | None -> type'_to_sign_type ty';
                carrier_set = try enum_elems ty' e.initial_state with _ -> None        //!!!! temporarily set to None for type where enum_finite_type is not yet implemented
            }
            e.types |> add (ty', attrs) |> Type

and inline get_type eng ty' = make_type eng ty' None        // precond.: type must exist, i.e. must have been created before with make_type called with (Some signature_type)
and get_type' (Engine eid) (Type type_id) = engines.[eid].types |> get_obj type_id

and convert_type (eng as Engine eid) (ty : Signature.TYPE) : TYPE =
    let make_type, convert_type = make_type eng, convert_type eng
    match ty with
    |   Signature.Boolean                    -> make_type Boolean' (Some ty)
    |   Signature.Integer                    -> make_type Integer' (Some ty)
    |   Signature.String                     -> make_type String' (Some ty)
    |   Signature.Undef                      -> make_type Undef' (Some ty)
    |   Signature.Rule                       -> make_type Rule' (Some ty)
    |   Signature.TypeParam name             -> make_type (TypeParam' name) (Some ty)
    |   Signature.Prod ty_elems              -> make_type (Prod' (ty_elems |> List.map convert_type)) (Some ty)
    |   Signature.Seq elem_ty                -> make_type (Seq' (convert_type elem_ty)) (Some ty)
    |   Signature.Powerset elem_ty           -> make_type (Powerset' (convert_type elem_ty)) (Some ty)
    |   Signature.Bag elem_ty                -> make_type (Bag' (convert_type elem_ty)) (Some ty)
    |   Signature.Map (dom_ty, rng_ty)       -> make_type (Map' (convert_type dom_ty, convert_type rng_ty)) (Some ty)
    |   Signature.TypeCons (tyname, ty_args) -> make_type (TypeCons' (tyname, ty_args |> List.map convert_type)) (Some ty)
    |   Signature.Subset (tyname, main_ty)   -> make_type (Subset' (tyname, convert_type main_ty)) (Some ty)

and inline to_signature_type (eng as Engine eid) (Type type_id : TYPE) : Signature.TYPE =
    (snd (engines.[eid].types |> get type_id)).signature_type

and enum_finite_type (eng as Engine eid) (Type type_id : TYPE) : VALUE Set option =
    (snd (engines.[eid].types |> get type_id)).carrier_set

and inline BooleanType (eng : ENGINE) = get_type eng Boolean'
and inline IntegerType (eng : ENGINE) = get_type eng Integer'
and inline StringType (eng : ENGINE) = get_type eng String'
and inline UndefType (eng : ENGINE) = get_type eng Undef'
and inline RuleType (eng : ENGINE) = get_type eng Rule'
and inline TypeParam (eng : ENGINE) (name : string) = get_type eng (TypeParam' name)
and inline ProdType (eng : ENGINE) (ty_elems : TYPE list) = get_type eng (Prod' ty_elems)
and inline SeqType (eng : ENGINE) (elem_ty : TYPE) = get_type eng (Seq' elem_ty)
and inline PowersetType (eng : ENGINE) (elem_ty : TYPE) = get_type eng (Powerset' elem_ty)
and inline BagType (eng : ENGINE) (elem_ty : TYPE) = get_type eng (Bag' elem_ty)
and inline MapType (eng : ENGINE) (dom_ty : TYPE, rng_ty : TYPE) = get_type eng (Map' (dom_ty, rng_ty))
and inline TypeCons (eng : ENGINE) (tyname : string, ty_args : TYPE list) = get_type eng (TypeCons' (tyname, ty_args))
and inline SubsetType (eng : ENGINE) (tyname : string, main_ty : TYPE) = get_type eng (Subset' (tyname, main_ty))

and match_type (eng : ENGINE) (ty : TYPE) (ty_sign : TYPE) (ty_env : Map<string, TYPE>) : Map<string, TYPE> =
    let type_to_string, get_type', match_type = type_to_string eng, get_type' eng, match_type eng
    if !trace > 2 then fprintf stderr "match_type(%s, %s)\n" (ty |> type_to_string) (ty_sign |> type_to_string)
    match (get_type' ty, get_type' ty_sign) with
    |   (_, Subset' (_, ty_sign')) -> match_type ty ty_sign' ty_env
    |   (Subset' (_, ty'), _)      -> match_type ty' ty_sign ty_env
    |   (TypeParam' a, _) ->
            failwith (sprintf "%s: type parameter not allowed in concrete type to be matched to signature type %s"
                (type_to_string ty) (type_to_string ty_sign))
    |   _ ->
            if ty = ty_sign then Map.empty else
                match get_type' ty_sign with
                |   TypeParam' a ->
                        if Map.containsKey a ty_env then
                            if ty = Map.find a ty_env then ty_env
                            else raise (Error (eng, "match_type", TypeMismatch (ty, ty_sign)))
                        else Map.add a ty ty_env
                |   _ -> raise (Error (eng, "match_type", TypeMismatch (ty, ty_sign)))

and match_one_fct_type eng (fct_name : string) (args_types : TYPE list) (sign_fct_type : TYPE list * TYPE) : TYPE =
    let (sign_args_types, sign_res_type) = sign_fct_type
    let result_type sign_res_type ty_env =
        match get_type' eng sign_res_type with
        |   TypeParam' a ->
                try Map.find a ty_env
                with _ -> raise (Error (eng, "match_one_fct_type", TypeOfResultUnknown (fct_name, sign_args_types, sign_res_type)))
        |   _ -> sign_res_type
    let rec match_types = function
        |   ([], [], ty_env : Map<string, TYPE>) ->
                (ty_env, result_type sign_res_type ty_env)
        |   (arg_type :: args_types', sign_arg_type :: sign_arg_types', ty_env) -> 
                let ty_env_1 =
                    try match_type eng arg_type sign_arg_type ty_env
                    with _ -> raise (Error (eng, "match_one_fct_type", FunctionCallTypeMismatch ((fct_name, sign_args_types, sign_res_type), args_types)))
                match_types (args_types', sign_arg_types', ty_env_1)
        |   (_, _, _) -> // arity does not match
                raise (Error (eng, "match_one_fct_type", FunctionCallTypeMismatch ((fct_name, sign_args_types, sign_res_type), args_types)))
//    let (_, result_type) = match_types (args_types, sign_args_types, Map.empty)
    let (_, result_type) =
        match args_types with
        |   [ty] ->
                match get_type' eng ty with
                |   Prod' args_types -> match_types (args_types, sign_args_types, Map.empty)    // one single tuple (x_1, ..., x_n) is equivalent to n arguments x_1, ..., x_n 
                |   _ -> match_types (args_types, sign_args_types, Map.empty)
            |   _ -> match_types (args_types, sign_args_types, Map.empty)
    result_type

and match_fct_type (eng as Engine eid) (fct_name : string) (args_types : TYPE list) (sign_fct_types : list<TYPE list * TYPE>) : TYPE =
    if !trace > 2 then fprintf stderr "\nfunction '%s': match_fct_type (%s) with:\n%s\n" fct_name (args_types |> type_list_to_string eng) (String.concat "," (sign_fct_types >>| fct_type_to_string eng))
    let rec matching_types results candidates =
        match candidates with
        |   [] -> results
        |   sign_fct_type :: candidates' ->
                if !trace > 2 then fprintf stderr "  sign_fct_type = %s\n" (sign_fct_type |> fct_type_to_string eng)
                try match match_one_fct_type eng fct_name args_types sign_fct_type with
                    |   ty -> matching_types (ty :: results) candidates'
                with ex -> matching_types results candidates'
    let results = List.rev (matching_types [] sign_fct_types)
    match results with
    |   [] -> raise (Error (eng, "match_fct_type", NoMatchingFunctionType (fct_name, args_types)))
    |   [ty] -> ty
    |   _ -> raise (Error (eng, "match_fct_type", AmbiguousFunctionCall (fct_name, args_types)))

and type_of_value (eng as Engine eid) x = convert_type eng (Background.type_of_value engines.[eid].signature x)    //!!!! could be made more efficient for cells
and main_type_of eng ty = match get_type' eng ty with Subset' (_, main_type) -> main_type | _ -> ty


and compute_type (eng as Engine eid) (t' : TERM') : TYPE =
    let fct_name, fct_types, type_of_value, get_term_type = fct_name eng, fct_types eng, type_of_value eng, get_term_type eng
    match t' with
    |   Value' x -> type_of_value x
    |   Initial' (f, xs) -> match_fct_type eng (fct_name f) (xs >>| type_of_value) (fct_types f)
    |   AppTerm' (f, ts) -> match_fct_type eng (fct_name f) (ts >>| get_term_type) (fct_types f)
    |   CondTerm' (G, t1, t2) ->
            let ty1 = main_type_of eng (get_term_type t1)
            let ty2 = main_type_of eng (get_term_type t2)
            if ty1 = ty2 then ty1 else failwith "compute_type: types of branches of conditional term do not match"
    |   TupleTerm' ts -> ProdType eng (ts >>| get_term_type)
    |   VarTerm' (v, ty) -> ty
    |   QuantTerm' (_, _, t_set, _) -> BooleanType eng
    |   LetTerm' (_, t1, t2) -> get_term_type t2
    |   DomainTerm' tyname -> PowersetType eng tyname
    |   UnfoldedTerm' ((f, xs), M) -> if Map.isEmpty M then failwith "compute_type: UnfoldedTerm with empty map" else get_term_type (snd (M |> Map.toList |> List.head))

and get_term_type (eng as Engine eid) (t as Term tid : TERM) : TYPE =
    (engines.[eid].terms |> get_attrs tid).term_type

and inline is_boolean_term (eng as Engine eid) (t as Term tid : TERM) : bool =
    let e = engines.[eid]
    match (e.terms |> get_attrs tid).term_type with
    |   Type type_id -> match e.types |> get_obj type_id with Boolean' -> true | _-> false

and inline get_smt_expr (Engine eid) (t as Term tid : TERM) : SmtInterface.SMT_EXPR option =
    !(engines.[eid].terms |> get_attrs tid).smt_expr

and inline set_smt_expr (Engine eid) (t as Term tid : TERM) (smt_expr : SmtInterface.SMT_EXPR) =
    (engines.[eid].terms |> get_attrs tid).smt_expr := Some smt_expr

and inline initial_state_eval_res (Engine eid) (t as Term tid : TERM) : TERM option ref =
    (engines.[eid].terms |> get_attrs tid).initial_state_eval_res

and get_term (eng as Engine eid : ENGINE) (t' : TERM') : TERM =
    match IndMap.try_get_index t' engines.[eid].terms with
    |   Some tid ->
            Term tid
    |   None ->
            let e = engines.[eid]
            let tid = e.terms |> count
            let attrs = {
                term_id    = tid;
                term_type  = compute_type eng t';
                smt_expr   = ref None;
                smt_result = Dictionary<int, TERM>();
                initial_state_eval_res = ref None;
            }
            e.terms |> add (t', attrs) |> Term

and inline get_term'_attrs (Engine eid) (Term tid) = engines.[eid].terms |> get tid
and get_term' (Engine eid) (Term tid) = engines.[eid].terms |> get_obj tid
and inline get_term_attrs (Engine eid) (Term tid) = engines.[eid].terms |> get_attrs tid

and inline Value eng x = get_term eng (Value' x)
and inline Initial eng (f, xs) = get_term eng (Initial' (f, xs))
and inline AppTerm eng (f, ts) = get_term eng (AppTerm' (f, ts))
and inline CondTerm eng (G, t1, t2) = get_term eng (CondTerm' (G, t1, t2))
and inline TupleTerm eng ts = get_term eng (TupleTerm' ts)
and inline VarTerm eng v = get_term eng (VarTerm' v)
and inline QuantTerm eng (q_kind, v, t_set, t_cond) = get_term eng (QuantTerm' (q_kind, v, t_set, t_cond))
and inline LetTerm eng (x, t1, t2) = get_term eng (LetTerm' (x, t1, t2))
and inline DomainTerm eng tyname = get_term eng (DomainTerm' tyname)
and inline UnfoldedTerm eng (loc, M) = get_term eng (UnfoldedTerm' (loc, M))
and inline TRUE (Engine eid) = !engines.[eid].TRUE_ |> Option.get
and inline FALSE (Engine eid) = !engines.[eid].FALSE_ |> Option.get
and inline AND (Engine eid) = !engines.[eid].AND_ |> Option.get
and inline OR (Engine eid) = !engines.[eid].OR_ |> Option.get
and inline NOT (Engine eid) = !engines.[eid].NOT_ |> Option.get
and inline EQUALS (Engine eid) = !engines.[eid].EQUALS_ |> Option.get
and inline BOOLEAN_TYPE (Engine eid) = !engines.[eid].BOOLEAN_TYPE_ |> Option.get

and convert_term (eng : ENGINE) (t : AST.TYPED_TERM) : TERM =
    AST.ann_term_induction (fun x -> x) {
        Value      = fun (_, x) -> Value eng x;
        Initial    = fun (_, (f, xs)) -> Initial eng (get_fct_id eng f, xs);
        AppTerm    = fun (ty, (f, ts)) ->
                        match f with
                        |   Signature.UndefConst    -> Value eng UNDEF
                        |   Signature.BoolConst b   -> Value eng (BOOL b)
                        |   Signature.IntConst i    -> Value eng (INT i)
                        |   Signature.StringConst s -> Value eng (STRING s)
                        |   Signature.FctName f ->
                                let f_id = get_fct_id eng f
                                try
                                    AppTerm eng (f_id, ts)
                                with ex as Signature.Error (Signature.NoMatchingFunctionType (f, tys)) ->
                                    fprintf stderr "convert_term: in term %A\n" (AppTerm eng (f_id, ts))
                                    raise ex;
        TupleTerm  = fun (_, ts) -> TupleTerm eng ts;
        CondTerm   = fun (_, (G, t1, t2)) -> CondTerm eng (G, t1, t2);
        VarTerm    = fun (ty, v) -> VarTerm eng (v, convert_type eng ty);
        QuantTerm  = fun (ty, (q_kind, v, t_set, t_cond)) -> QuantTerm eng (q_kind, v, t_set, t_cond);
        LetTerm    = fun (_, (v, t1, t2)) -> LetTerm eng (v, t1, t2);
        DomainTerm = fun (_, D) -> DomainTerm eng (convert_type eng D);
    } t

and inline get_s_update_set (eng as Engine eid : ENGINE) (us' : S_UPDATE_SET') : S_UPDATE_SET =
    match IndMap.try_get_index us' engines.[eid].supds with
    |   Some uid ->
            S_UpdateSet uid
    |   None ->
            let e = engines.[eid]
            let uid = e.supds |> count
            let attrs : S_UPDATE_SET_ATTRS = {
                s_update_set_id = uid
            }
            e.supds |> add (us', attrs) |> S_UpdateSet

and inline get_s_update_set' (Engine eid) (S_UpdateSet uid : S_UPDATE_SET) : S_UPDATE_SET' =
    engines.[eid].supds |> get uid |> fst

and inline s_update_set_empty (eng as Engine eid) : S_UPDATE_SET =
    get_s_update_set eng Set.empty

and inline s_update_set_is_empty (eng as Engine eid) (S_UpdateSet uid : S_UPDATE_SET) : bool =
    engines.[eid].supds |> get uid |> fst |> Set.isEmpty

and inline s_update_set_union (eng as Engine eid) (S_UpdateSet uid1 : S_UPDATE_SET) (S_UpdateSet uid2 : S_UPDATE_SET) : S_UPDATE_SET =
    let supds = engines.[eid].supds
    let us1, _ = supds |> get uid1
    let us2, _ = supds |> get uid2
    get_s_update_set eng (Set.union us1 us2)

and inline s_update_set_seq_merge_2 (eng as Engine eid) (S_UpdateSet uid1 : S_UPDATE_SET) (S_UpdateSet uid2 : S_UPDATE_SET) : S_UPDATE_SET =
    let supds = engines.[eid].supds
    let us1, _ = supds |> get uid1
    let us2, _ = supds |> get uid2
    get_s_update_set eng (seq_merge_2 eng us1 us2)

and inline s_update_set_to_list (Engine eid) (S_UpdateSet uid : S_UPDATE_SET) : list<(FCT_ID * VALUE list) * TERM> =
    let us', _ = engines.[eid].supds |> get uid
    List.ofSeq us'

and inline get_rule_def_id (Engine eid) (name : string) : RULE_DEF_ID =
    match engines.[eid].rule_defs |> try_get_index (RuleName name) with
    | Some rule_def_id -> RuleDefId rule_def_id
    | None -> failwith (sprintf "Engine.get_named_rule_id: function '%s' not found in global context #%d" name eid)

and inline get_rule_def' (Engine eid) (RuleDefId id : RULE_DEF_ID) : RULE_DEF' * RULE_DEF_ATTRS =
    engines.[eid].rule_defs |> get id

and inline get_rule_name (Engine eid) (RuleDefId id : RULE_DEF_ID) = let RuleName r_name, _ =engines.[eid].rule_defs |> get id in r_name
and inline get_rule_def (eng as Engine eid) (id : RULE_DEF_ID) = (snd (get_rule_def' eng id)).rule_def

and inline get_rule' (Engine eid) (Rule rid) = engines.[eid].rules |> get rid |> fst

and inline get_rule (eng as Engine eid : ENGINE) (R' : RULE') : RULE =
    match IndMap.try_get_index R' engines.[eid].rules with
    |   Some rid ->
            Rule rid
    |   None ->
            let e = engines.[eid]
            let rid = e.rules |> count
            e.rules |> add (R', ()) |> Rule

and inline UpdateRule eng ((f, ts), t_rhs) = get_rule eng (UpdateRule' ((f, ts), t_rhs))
and inline CondRule eng (G, R1, R2) = get_rule eng (CondRule' (G, R1, R2))
and inline ParRule eng Rs = get_rule eng (ParRule' Rs)
and inline SeqRule eng Rs = get_rule eng (SeqRule' Rs)
and inline IterRule eng R' = get_rule eng (IterRule' R')
and inline LetRule eng (v, t1, R') = get_rule eng (LetRule' (v, t1, R'))
and inline MacroRuleCall eng (r, args) = get_rule eng (MacroRuleCall' (r, args))
and inline ForallRule eng (v, t_set, G, R') = get_rule eng (ForallRule' (v, t_set, G, R'))
and inline S_Updates eng upds = get_rule eng (S_Updates' upds)   // Map.map (fun ((f, xs), t_rhs) -> ((get_fct_id eng f, xs), convert_term eng t_rhs)) upds
and inline UnfoldedRule eng (loc, M) = get_rule eng (UnfoldedRule' (loc, M))

and convert_rule (eng : ENGINE) (R : AST.RULE) : RULE =
    AST.rule_induction (convert_term eng) {
        UpdateRule = fun ((f, ts), t_rhs) -> UpdateRule eng ((get_fct_id eng f, ts), t_rhs);
        CondRule   = fun (G, R1, R2) -> CondRule eng (G, R1, R2);
        ParRule    = fun Rs -> ParRule eng Rs;
        SeqRule    = fun Rs -> SeqRule eng Rs;
        IterRule   = fun R' -> IterRule eng R';
        LetRule    = fun (v, t1, R') -> LetRule eng (v, t1, R');
        MacroRuleCall = fun (r_name, args) -> MacroRuleCall eng (get_rule_def_id eng r_name, args);
        ForallRule = fun (v, t_set, G, R') -> ForallRule eng (v, t_set, G, R');
        S_Updates  = fun upds -> S_Updates eng (get_s_update_set eng (Set.map (fun ((f, xs), t_rhs) -> (get_fct_id eng f, xs), convert_term eng t_rhs) upds))
    } R

and new_engine (sign : Signature.SIGNATURE, initial_state : State.STATE, fct_def_db : AST.MACRO_DB, rule_def_db : AST.RULES_DB, invariants : Map<string, AST.TYPED_TERM>, smt_ctx : SmtInterface.SMT_CONTEXT) : ENGINE =
    let eid = engines.Count
    let new_engine = {
        signature       = sign
        initial_state   = initial_state
        invariants      = Map.empty
        functions       = newIndMap<FUNCTION', FUNCTION_ATTRS>()
        rule_defs       = newIndMap<RULE_DEF', RULE_DEF_ATTRS>()
        types           = newIndMap<TYPE', TYPE_ATTRS>()
        terms           = newIndMap<TERM', TERM_ATTRS>()
        rules           = newIndMap<RULE', RULE_ATTRS>()
        supds           = newIndMap<S_UPDATE_SET', S_UPDATE_SET_ATTRS>()
        TRUE_           = ref None
        FALSE_          = ref None
        AND_            = ref None
        OR_             = ref None
        NOT_            = ref None
        EQUALS_         = ref None
        BOOLEAN_TYPE_   = ref None
        smt_ctx         = smt_ctx
    }
    engines.Add new_engine
    let extract_fct_interpretation_if_possible f_name =
        let f_kind = Signature.fct_kind f_name sign
        match f_kind with
        |   Signature.Constructor ->
                Some (Constructor (fun xs -> CELL (f_name, xs)))
        |   Signature.Static ->
                match initial_state._static |> Map.tryFind f_name with
                |   None -> fprintf stderr "Warning: static function '%s' is in signature, but is not defined - ignored\n" f_name; None
                |   Some fct_interp ->
                        if Set.contains f_name (Signature.fct_names Background.signature)   // background functions
                        then Some (StaticBackground fct_interp)
                        else Some (StaticUserDefined (fct_interp, None))        // second component is the AsmetaL definition to be filled in later
        |   Signature.Controlled ->
                match initial_state._dynamic_initial |> fst |> Map.tryFind f_name with
                |   Some fct_def -> Some (ControlledInitial (fct_def, None))    // AsmetaL definition of controlled function initialization will be filled in later
                |   None -> Some ControlledUninitialized
        |   Signature.Derived ->
                match fct_def_db |> Map.tryFind f_name with
                |   Some (args, body) -> Some (Derived None)                    // AsmetaL definition of derived function will be filled in later
                |   None -> failwith (sprintf "Engine.new_engine: derived function '%s' is in signature, but is not defined\n" f_name)
        |   Signature.Monitored -> failwith (sprintf "Engine.new_engine: monitored function '%s' - not implemented" f_name)
        |   Signature.Shared -> failwith (sprintf "Engine.new_engine: shared function '%s' - not implemented" f_name)
        |   Signature.Out -> failwith (sprintf "Engine.new_engine: out function '%s' - not implemented" f_name)
    let extract_rule_def_rhs r_name =
        match rule_def_db |> Map.tryFind r_name with
        |   Some (args, R) -> (args, R)
        |   None -> failwith (sprintf "Engine.new_engine: no definition found for rule macro '%s'\n" r_name)
    let add_functions fct_list =
        fct_list
            |> List.map (fun (name, _) -> name, extract_fct_interpretation_if_possible name)   
            |> List.filter (function (_, None) -> false | _ -> true)
            |> Seq.iteri ( fun i (name, opt_fct_interpretation) ->
                let sign = sign
                match opt_fct_interpretation with
                |   None -> ()
                |   Some fct_interpretation ->
                        new_engine.functions |> add (
                            FctName name, {
                                fct_id   = i;
                                fct_kind = Signature.fct_kind name sign;
                                fct_types = List.map (fun (args_ty, res_ty) -> (args_ty >>| convert_type (Engine eid), convert_type (Engine eid) res_ty)) (Signature.fct_types name sign);
                                fct_interpretation = fct_interpretation
                            }) |> ignore )
    let functions = sign |> Map.toList |> List.filter (fun (name, _) -> Signature.is_function_name name sign)
    // add to engine non-derived functions first, then derived functions
    functions |> List.filter (fun (name, _) -> not (Signature.fct_kind name sign = Signature.Derived)) |> add_functions
    functions |> List.filter (fun (name, _) -> Signature.fct_kind name sign = Signature.Derived) |> add_functions
    // add rules
    rule_def_db |> Map.toList
        |> List.map (fun (name, _) -> (name, extract_rule_def_rhs name))
        |> Seq.iteri (fun i (name, rule_def) ->
            new_engine.rule_defs |> add (
                RuleName name, {
                    rule_def_id   = i;
                    // rule_type = Signature.rule_types name sign;   // !!! to be implemented together with monomorphization
                    rule_def  = None
                }) |> ignore )
    for i in 0..(new_engine.functions |> count) - 1 do
        let FctName f_name, (f_attrs as { fct_interpretation = fct_intp }) = new_engine.functions |> get i
        match fct_intp with
        |   StaticUserDefined (fct_interp, None) ->
                match fct_def_db |> Map.tryFind f_name with
                |   Some (args, body) ->
                        new_engine.functions |> set i (FctName f_name, { f_attrs with fct_interpretation = StaticUserDefined (fct_interp, Some (args, convert_term (Engine eid) body)) })
                |   None -> failwith (sprintf "cannot find definition of static function '%s'\n" f_name)
        |   ControlledInitial (fct_interp, None) ->
                match fct_def_db |> Map.tryFind f_name with
                |   Some (args, body) ->
                        new_engine.functions |> set i (FctName f_name, { f_attrs with fct_interpretation = ControlledInitial (fct_interp, Some (args, convert_term (Engine eid) body)) })
                |   None -> failwith (sprintf "cannot find initial definition of controlled function '%s'\n" f_name)
        |   Derived None ->
                match fct_def_db |> Map.tryFind f_name with
                |   Some (args, body) ->
                        new_engine.functions |> set i (FctName f_name, { f_attrs with fct_interpretation = Derived (Some (args, convert_term (Engine eid) body)) })
                |   None -> failwith (sprintf "cannot find definition of derived function '%s'\n" f_name)
        |   _ -> ()     // if not any of the above cases, do nothing (the entry of fctTable was already completely initialized)
    for i in 0..(new_engine.rule_defs |> count) - 1 do
        let RuleName rd_name, (rd_attrs as { rule_def_id = id; rule_def = _ }) = new_engine.rule_defs |> get i
        let (args, body) = extract_rule_def_rhs rd_name
        new_engine.rule_defs |> set i (RuleName rd_name, { rd_attrs with rule_def = Some (args, convert_rule (Engine eid) body) })
    let new_ctx = {
        new_engine with
            invariants = Map.map (fun _ t -> convert_term (Engine eid) t) invariants
        }
    engines.[eid] <- new_ctx
    engines.[eid].TRUE_   := Some (Value (Engine eid) (BOOL true))
    engines.[eid].FALSE_  := Some (Value (Engine eid) (BOOL false))
    engines.[eid].AND_    := Some (get_fct_id (Engine eid) "and")
    engines.[eid].OR_     := Some (get_fct_id (Engine eid) "or")
    engines.[eid].NOT_    := Some (get_fct_id (Engine eid) "not")
    engines.[eid].EQUALS_ := Some (get_fct_id (Engine eid) "=")
    engines.[eid].BOOLEAN_TYPE_ := Some (BooleanType (Engine eid))
    Engine eid

and get_engine' (Engine eid : ENGINE) : ENGINE' =
    if eid < engines.Count then
        engines.[eid]
    else
        failwith (sprintf "get_engine': engine %d not found" eid)

and initial_state_of (Engine eid) =
    engines.[eid].initial_state

and invariants_of (Engine eid) =
    engines.[eid].invariants

and smt_solver_push (Engine eid) =
    SmtInterface.smt_solver_push engines.[eid].smt_ctx

and smt_solver_pop (Engine eid) =
    SmtInterface.smt_solver_pop engines.[eid].smt_ctx

//--------------------------------------------------------------------

and term_induction (eng: ENGINE) (fct_id : FCT_ID -> 'fct_id) (F : TERM_INDUCTION<'fct_id, 'term>) (t : TERM) :'term =
    let term_ind = term_induction eng fct_id F
    match get_term' eng t with
    |   Value' x              -> F.Value x
    |   Initial' (f, xs)      -> F.Initial (fct_id f, xs)
    |   AppTerm' (f, ts)      -> F.AppTerm (fct_id f, List.map (fun t -> term_ind t) ts)
    |   CondTerm' (G, t1, t2) -> F.CondTerm (term_ind G, term_ind t1, term_ind t2)
    |   TupleTerm' ts         -> F.TupleTerm (List.map (fun t -> term_ind t) ts)
    |   VarTerm' (v, ty)      -> F.VarTerm (v, ty)
    |   QuantTerm' (q_kind, v, t_set, t_cond) -> F.QuantTerm (q_kind, v, term_ind t_set, term_ind t_cond)
    |   LetTerm' (x, t1, t2)  -> F.LetTerm (x, term_ind t1, term_ind t2)
    |   DomainTerm' tyname    -> F.DomainTerm tyname
    |   UnfoldedTerm' ((f, xs), M) -> F.UnfoldedTerm ((fct_id f, xs), Map.map (fun _ t_i -> term_ind t_i) M)

//--------------------------------------------------------------------

and skipRule eng = ParRule eng []

//--------------------------------------------------------------------

and rule_induction (eng: ENGINE) (term : TERM -> 'term) (F : RULE_INDUCTION<'term, 'rule>) (R : RULE) : 'rule =
    let rule_ind = rule_induction eng term
    match get_rule' eng R with
    |   S_Updates' U -> F.S_Updates U   // F.S_Updates (Map.map (fun loc -> fun t_rhs -> term t_rhs) U)
    |   UpdateRule' ((f, ts), t) -> F.UpdateRule ((f, List.map term ts), term t)
    |   CondRule' (G, R1, R2: RULE) -> F.CondRule (term G, rule_ind F R1, rule_ind F R2)
    |   ParRule' Rs -> F.ParRule (List.map (rule_ind F) Rs)
    |   SeqRule' Rs -> F.SeqRule (List.map (rule_ind F) Rs)
    |   IterRule' R -> F.IterRule (rule_ind F R)
    |   LetRule' (v, t, R) -> F.LetRule (v, term t, (rule_ind F) R)
    |   ForallRule' (v, t_set, t_filter, R) -> F.ForallRule (v, term t_set, term t_filter, (rule_ind F) R)
    |   MacroRuleCall' (r, ts) -> F.MacroRuleCall (r, List.map term ts)
    |   UnfoldedRule' ((f, xs), M) -> F.UnfoldedRule ((f, xs), Map.map (fun _ R_i -> rule_ind F R_i) M)

//--------------------------------------------------------------------
//
//  pretty printing
//
//--------------------------------------------------------------------

and pp_list sep = function
|   []         -> []
|   [x]        -> [ x ]
|   (x :: xs') -> x :: (sep @ (pp_list sep xs'))

and pp_name (name : Signature.NAME) =
    (   match name with
    |   Signature.UndefConst -> "undef"
    |   Signature.BoolConst b -> if b then "true" else "false"
    |   Signature.IntConst i -> i.ToString()
    |   Signature.StringConst s -> "\"" + s + "\""
    |   Signature.FctName f -> f ) |> str

and pp_app_term sign = function
    |   (Signature.FctName f, [t1; t2]) when Signature.infix_status f sign <> Signature.NonInfix ->
            blo0 [ str "("; blo0 [ t1; brk 1; str (sprintf "%s " f); t2 ]; str ")" ]
    |   (Signature.FctName f, ts) when ts <> [] ->
            blo0 [ str f; str " "; str "("; blo0 (pp_list [str",";brk 1] ts); str ")" ]
    |   (name, _) -> pp_name name

and pp_location_term sign prefix = function
    |   (f : string, xs : VALUE list) when xs <> [] ->
            blo0 [ str (prefix+"["); str f; str "("; blo0 (pp_list [str",";brk 1] (List.map (fun x -> str (value_to_string x)) xs)); str ")]" ]
    |   (f, _) -> blo0 [ str $"{prefix}[{f}]" ]

and pp_term (eng : ENGINE) (t : TERM) =
    let sign = (get_engine' eng).signature
    let (pp_app_term, pp_location_term) = (pp_app_term sign, pp_location_term sign)
    term_induction eng (fun x -> x) {
        AppTerm  = fun (f, ts) -> pp_app_term (Signature.FctName (fct_name eng f), ts);
        CondTerm = fun (G, t1, t2) -> blo0 [ str "if "; G; line_brk; str "then "; t1; line_brk; str "else "; t2; line_brk; str "endif" ];
        Value    = fun x -> str (value_to_string x);
        Initial  = fun (f, xs) -> pp_location_term "initial" (fct_name eng f, xs);
        TupleTerm = fun ts -> blo0 [ str "("; blo0 (pp_list [str",";brk 1] ts); str ")" ];
        VarTerm = fun (x, _) -> str x;
        QuantTerm = fun (q_kind, v, t_set, t_cond) ->
            blo0 [ str ("("^(AST.quant_kind_to_str q_kind)^" "); str v; str " in "; t_set; str " with "; t_cond; str ")" ];
        LetTerm = fun (v, t1, t2) -> blo0 [ str "let "; str v; str " = "; t1; line_brk; str "in "; t2; line_brk; str "endlet" ];
        DomainTerm = fun tyname -> str (type_to_string eng tyname);
        UnfoldedTerm = fun ((f, xs), M) ->
            let pp_case (x_i, t_i) = blo0 [ pp_location_term "initial" (fct_name eng f, xs); str " = ";  str (value_to_string x_i); str " -> "; t_i ]
            let L = M |> Map.toList |> List.map pp_case
            blo0 [ str "unfolded "; line_brk; blo2 ( pp_list [line_brk] L ); line_brk; str "endunfolded" ];
    } t

and pp_rule (eng : ENGINE)  (R : RULE) =
    let sign = (get_engine' eng).signature
    let (pp_app_term, pp_location_term, pp_term) = (pp_app_term sign, pp_location_term sign, pp_term eng)
    rule_induction eng pp_term {
        S_Updates = fun U ->
                        let pp_elem ((f, xs), t) = blo0 [ str (fct_name eng f); str " "; str "("; blo0 (pp_list [str",";brk 1] (xs >>| fun x -> str (value_to_string x))); str ") := "; (pp_term t) ]
                        let L = s_update_set_to_list eng U >>| pp_elem
                        blo0 [ str "{"; line_brk; blo2 ( pp_list [line_brk] L); line_brk; str "}" ];
        UpdateRule = fun ((f, ts), t) -> blo0 [ pp_app_term (Signature.FctName (fct_name eng f), ts); str " := "; t ];
        CondRule = fun (G, R1, R2) -> blo0 ( str "if " :: G:: str " then " :: line_brk :: blo2 [ R1 ] :: line_brk ::
                                             (if R2 <> str "skip" then [ str "else "; line_brk; blo2 [ R2 ]; line_brk; str "endif" ] else [ str "endif"]) );
        ParRule = fun Rs -> if Rs <> [] then blo0 [ str "par"; line_brk; blo2 ( pp_list [line_brk] Rs); line_brk; str "endpar" ] else str "skip";
        SeqRule = fun Rs -> blo0 [ str "seq"; line_brk; blo2 (pp_list [line_brk] Rs); line_brk; str "endseq" ];
        IterRule = fun R' -> blo0 [ str "iterate "; line_brk; blo2 [ R' ]; line_brk; str "enditerate" ];
        LetRule = fun (v, t, R) -> blo0 [ str "let "; str v; str " = "; t; line_brk; str "in "; R; line_brk; str "endlet" ];
        ForallRule = fun (v, t_set, t_filter, R) -> blo0 [ str "forall "; str v; str " in "; t_set; str " with "; t_filter; str " do"; line_brk; blo2 [ R ]; line_brk; str "endforall" ];
        MacroRuleCall = fun (r, ts) -> blo0 [ str (get_rule_name eng r); str "["; blo0 (pp_list [str",";brk 1] ts); str "]" ];
        UnfoldedRule = fun ((f, xs), M) ->
            let pp_case (x_i, t_i) = blo0 [ pp_location_term "" (fct_name eng f, xs); str " = ";  str (value_to_string x_i); str " -> "; t_i ]
            let L = M |> Map.toList |> List.map pp_case
            blo0 [ str "unfolded "; line_brk; blo2 ( pp_list [line_brk] L ); line_brk; str "endunfolded" ];
    } R


and name_to_string t     = t |> pp_name |> PrettyPrinting.toString 80
and term_to_string eng t = t |> pp_term eng |> PrettyPrinting.toString 80
and rule_to_string eng t = t |> pp_rule eng |> PrettyPrinting.toString 80

//--------------------------------------------------------------------
//
//  function tables
//
//--------------------------------------------------------------------

and show_fct_tables (eng as Engine eid: ENGINE) =
    let e = get_engine' eng
    let index_s = e.functions |> show_index (fun (FctName f_name) -> f_name)
    let show_table_entry (i, FctName f_name, { fct_kind = f_kind; fct_id = f_id; fct_interpretation = f_intp }) =
        if i <> f_id then
            failwith (sprintf "show_fct_tables: function id %d does not match index %d" f_id i)
        else
            sprintf "%d: %s (%s) = [%s]"
                f_id f_name (Signature.fct_kind_to_string f_kind)
                (match f_intp with
                    | Constructor _ -> "constructor"
                    | StaticBackground _ -> "static (background)"
                    | StaticUserDefined _ -> "static (user-defined)"
                    | ControlledInitial _ -> "controlled (initial)"
                    | ControlledUninitialized -> "controlled (uninitialized)"
                    | Derived (Some (args, body)) -> sprintf "derived (%s) = %s" (String.concat ", " args) (term_to_string eng body)
                    | Derived None -> "derived (definition missing)")
    let table_s = e.functions |> show_table show_table_entry
    index_s + table_s

//--------------------------------------------------------------------
//
//  locations, symbolic updates, symbolic update sets
//
//--------------------------------------------------------------------

and location_to_string eng ((f, xs) : LOCATION) : string = Updates.location_to_string (fct_name eng f, xs)

and show_s_update eng ((f, xs), t) =
    let f = fct_name eng f
    sprintf "%s := %s"
        (if List.isEmpty xs then f else sprintf "%s (%s)" f (String.concat ", " (List.map value_to_string xs)))
        (PrettyPrinting.toString 80 (pp_term eng t))

and show_s_update_set eng (U :UPDATE_SET) =
    "{ " +
    ( Set.toList U >>| show_s_update eng
        |> String.concat ", "   ) +
    " }"

and show_s_update_map eng (U :UPDATE_MAP) =
    let s_update_set = Set.ofSeq (Map.toSeq U |> Seq.collect (fun (f : FCT_ID, table) -> table |> Map.toSeq |> Seq.map (fun (args, value) -> (f, args), value)))
    show_s_update_set eng s_update_set

//--------------------------------------------------------------------

and add_s_update eng (U : UPDATE_MAP) (u as (loc as (f, args), value): UPDATE) =
    if !trace > 0 then fprintf stderr "add_s_update: %s\n" (show_s_update eng u)
    Map.change f
        ( function None -> Some (Map.add args value Map.empty)
                 | Some table ->
                        Some (  if Map.containsKey args table
                                then if value <> Map.find args table  // deal with conflicting updates
                                     then raise (Error (eng, "add_s_update", InconsistentUpdates (eng, None, (loc, Map.find args table), (loc, value), None)))
                                     else table
                                else Map.add args value table ) )
        U

and s_update_set'_to_s_update_map eng (U : S_UPDATE_SET') =     // note: S_UPDATE_SET' is then UPDATE_SET
    Set.fold (add_s_update eng) Map.empty U

and s_update_set_to_s_update_map eng (U : S_UPDATE_SET) =
    let U' = get_s_update_set' eng U
    s_update_set'_to_s_update_map eng U'

and consistent eng (U : S_UPDATE_SET') =
    try let x = s_update_set'_to_s_update_map eng U
        in true
    with Failure _ -> false
    
and locations (U : UPDATE_SET) : Set<LOCATION> =
    Set.map (fun (loc, value) -> loc) U

and seq_merge_2 eng (U : UPDATE_SET) (V : UPDATE_SET) =
    if not (consistent eng U)
    then U
    else let U_reduced = Set.filter (fun (loc, _) -> not (Set.contains loc (locations V))) U
         in Set.union U_reduced V

and seq_merge_n eng (Us : UPDATE_SET list) : UPDATE_SET =
    List.fold (seq_merge_2 eng) Set.empty Us

and apply_s_update_map (UM0 : UPDATE_MAP) (UM' : UPDATE_MAP) =
    let update_dynamic_function_table (f_table : Map<VALUE list, TERM>) (updates_of_f : Map<VALUE list, TERM>) =
            Map.fold (fun table args value -> Map.add args value table) f_table updates_of_f
    let apply_to_s_update_map (UM0 : UPDATE_MAP) (UM' : UPDATE_MAP) =
            Map.fold
                ( fun UM f updates_of_f ->
                    Map.change f
                        (function None -> Some (update_dynamic_function_table Map.empty updates_of_f) 
                                | Some f_table -> Some (update_dynamic_function_table f_table updates_of_f)) UM )
                UM0 UM'
    in  apply_to_s_update_map UM0 UM'

and apply_s_update_set eng S U =
    apply_s_update_map S (s_update_set'_to_s_update_map eng U)

and sequel_s_state : ENGINE -> UPDATE_MAP -> UPDATE_SET -> UPDATE_MAP = apply_s_update_set

//--------------------------------------------------------------------

and get_env (env : ENV) (var : string) =
    // fprintf stderr "get_env: looking for variable '%s'\n" var;
    Map.find var env

and add_binding (env : ENV) (var : string, t : TERM) =
    Map.add var t env

and replace_vars (eng : ENGINE) (env : ENV) (t : TERM) : TERM =
    term_induction eng (fun x -> x) {
        Value      = Value eng
        Initial    = Initial eng
        AppTerm    = AppTerm eng
        CondTerm   = CondTerm eng
        TupleTerm  = TupleTerm eng
        VarTerm    = fun (v, _) -> get_env env v
        QuantTerm  = QuantTerm eng
        LetTerm    = LetTerm eng
        DomainTerm = DomainTerm eng
        UnfoldedTerm  = UnfoldedTerm eng
    } t

//--------------------------------------------------------------------

and get_values eng (ts : TERM list) : VALUE list option =    // only if all arguments are values
    List.fold ( function
                |   Some ts -> (fun t -> match get_term' eng t with Value' v -> Some(v :: ts) | _ -> None)
                |   None -> (fun _ -> None) ) (Some []) (List.rev ts)

//--------------------------------------------------------------------

and empty_path_cond : PATH_COND = Set.empty, Map.empty

//--------------------------------------------------------------------
and unfolded_to_cond (CondTermOrRule : ENGINE -> TERM * 'a * 'a -> 'a) eng ((f, xs), M) =
    let elems = M |> Map.toList |> List.rev
    let _, t_n = List.head elems
    let f_xs_term = Initial eng (f, xs)
    List.fold
        (fun acc (x_i, t_i) -> CondTermOrRule eng (s_equals eng (f_xs_term, Value eng x_i), t_i, acc))
        t_n    // no need to test (f_xs) = x_n, as this is the last remaining case
        (List.tail elems)

//--------------------------------------------------------------------
//
//  SMT solver interface
//  
//--------------------------------------------------------------------

and smt_map_term (eng as Engine eid) (t : TERM) : SmtInterface.SMT_EXPR =
    let C = engines[eid].smt_ctx
    let (ctx, con, fct) = (!C.ctx, !C.con, !C.fct)
    let get_term_type' t = get_type' eng (get_term_type eng t)
    let type_to_string, get_type = type_to_string eng, get_type eng

    let smt_map_cond (G_, t1_, t2_) : SmtInterface.SMT_EXPR =
        let err_msg (G, T_G, t1, T_t1, t2, T_t2) =
            failwith (sprintf "smt_map_ITE: type error: for term %s the expected type is (Boolean, T, T), where T is Boolean, Integer or a user-defined type; type (%s, %s, %s) found instead"
                (term_to_string eng (CondTerm eng (G, t1, t2))) (type_to_string T_G) (type_to_string T_t1) (type_to_string T_t2) )
        match (smt_map_term eng G_, get_term_type' G_, smt_map_term eng t1_, get_term_type' t1_, smt_map_term eng t2_, get_term_type' t2_) with
        |   (SmtInterface.SMT_BoolExpr G, Boolean', SmtInterface.SMT_BoolExpr t1, Boolean', SmtInterface.SMT_BoolExpr t2, Boolean') ->
                SmtInterface.SMT_BoolExpr (ctx.MkITE (G, t1 :> Microsoft.Z3.Expr, t2 :> Microsoft.Z3.Expr) :?> Microsoft.Z3.BoolExpr)
        |   (SmtInterface.SMT_BoolExpr G, Boolean', SmtInterface.SMT_IntExpr t1, Integer', SmtInterface.SMT_IntExpr t2, Integer') ->
                SmtInterface.SMT_IntExpr (ctx.MkITE (G, t1 :> Microsoft.Z3.Expr, t2 :> Microsoft.Z3.Expr) :?> Microsoft.Z3.IntExpr)
        |   (SmtInterface.SMT_BoolExpr G, Boolean', SmtInterface.SMT_Expr t1, TypeCons' (tyname1, []), SmtInterface.SMT_Expr t2, TypeCons' (tyname2, [])) ->
                if tyname1 = tyname2
                then SmtInterface.SMT_Expr (ctx.MkITE (G, (t1 : Microsoft.Z3.Expr), (t2 : Microsoft.Z3.Expr)) : Microsoft.Z3.Expr)
                else err_msg (G_, BooleanType eng, t1_, TypeCons eng (tyname1, []), t2_, TypeCons eng (tyname2, []))
        |   (_, T_G, _, T_t1, _, T_t2) -> err_msg (G_, get_type T_G, t1_, get_type T_t1, t2_, get_type T_t2)

    let smt_map_app_term (f_id : FCT_ID, ts) : SmtInterface.SMT_EXPR =
        if !trace > 1 then fprintf stderr "smt_map_app_term: mapping function '%s' with arguments %s\n" (fct_name eng f_id) (String.concat ", " (ts >>| term_to_string eng))
        let FctName f, { fct_id = fct_id; fct_kind = f_kind; fct_interpretation = fct_intp } = get_function' eng f_id
        if (match fct_intp with StaticBackground _ -> true | _ -> false) then 
            let es = ts >>| smt_map_term eng
            //let f' = get_function' eng f
            match (f, es) with
            |   ("=",       [ SmtInterface.SMT_BoolExpr e1; SmtInterface.SMT_BoolExpr e2 ]) -> SmtInterface.SMT_BoolExpr (ctx.MkEq (e1, e2))
            |   ("=",       [ SmtInterface.SMT_IntExpr e1;  SmtInterface.SMT_IntExpr e2 ])  -> SmtInterface.SMT_BoolExpr (ctx.MkEq (e1, e2))
            |   ("=",       [ SmtInterface.SMT_Expr e1;     SmtInterface.SMT_Expr e2 ])     -> SmtInterface.SMT_BoolExpr (ctx.MkEq (e1, e2))
            |   ("!=",      [ SmtInterface.SMT_BoolExpr e1; SmtInterface.SMT_BoolExpr e2 ]) -> SmtInterface.SMT_BoolExpr (ctx.MkNot (ctx.MkEq (e1, e2)))
            |   ("!=",      [ SmtInterface.SMT_IntExpr e1;  SmtInterface.SMT_IntExpr e2 ])  -> SmtInterface.SMT_BoolExpr (ctx.MkNot (ctx.MkEq (e1, e2)))
            |   ("!=",      [ SmtInterface.SMT_Expr e1;     SmtInterface.SMT_Expr e2 ])     -> SmtInterface.SMT_BoolExpr (ctx.MkNot (ctx.MkEq (e1, e2)))
            |   ("not",     [ SmtInterface.SMT_BoolExpr e ])                                -> SmtInterface.SMT_BoolExpr (ctx.MkNot e)
            |   ("and",     [ SmtInterface.SMT_BoolExpr e1; SmtInterface.SMT_BoolExpr e2 ]) -> SmtInterface.SMT_BoolExpr (ctx.MkAnd (e1, e2))
            |   ("or",      [ SmtInterface.SMT_BoolExpr e1; SmtInterface.SMT_BoolExpr e2 ]) -> SmtInterface.SMT_BoolExpr (ctx.MkOr (e1, e2))
            |   ("xor",     [ SmtInterface.SMT_BoolExpr e1; SmtInterface.SMT_BoolExpr e2 ]) -> SmtInterface.SMT_BoolExpr (ctx.MkXor (e1, e2))
            |   ("implies", [ SmtInterface.SMT_BoolExpr e1; SmtInterface.SMT_BoolExpr e2 ]) -> SmtInterface.SMT_BoolExpr (ctx.MkImplies (e1, e2))
            |   ("iff",     [ SmtInterface.SMT_BoolExpr e1; SmtInterface.SMT_BoolExpr e2 ]) -> SmtInterface.SMT_BoolExpr (ctx.MkIff (e1, e2))
            |   (">",       [ SmtInterface.SMT_IntExpr e1;  SmtInterface.SMT_IntExpr e2 ])  -> SmtInterface.SMT_BoolExpr (ctx.MkGt (e1, e2))
            |   (">=",      [ SmtInterface.SMT_IntExpr e1;  SmtInterface.SMT_IntExpr e2 ])  -> SmtInterface.SMT_BoolExpr (ctx.MkGe (e1, e2))
            |   ("<",       [ SmtInterface.SMT_IntExpr e1;  SmtInterface.SMT_IntExpr e2 ])  -> SmtInterface.SMT_BoolExpr (ctx.MkLt (e1, e2))
            |   ("<=",      [ SmtInterface.SMT_IntExpr e1;  SmtInterface.SMT_IntExpr e2 ])  -> SmtInterface.SMT_BoolExpr (ctx.MkLe (e1, e2))
            |   ("+",       [ SmtInterface.SMT_IntExpr e1;  SmtInterface.SMT_IntExpr e2 ])  -> SmtInterface.SMT_IntExpr (ctx.MkAdd (e1, e2) :?> Microsoft.Z3.IntExpr)
            |   ("-",       [ SmtInterface.SMT_IntExpr e1;  SmtInterface.SMT_IntExpr e2 ])  -> SmtInterface.SMT_IntExpr (ctx.MkSub (e1, e2) :?> Microsoft.Z3.IntExpr)
            |   ("*",       [ SmtInterface.SMT_IntExpr e1;  SmtInterface.SMT_IntExpr e2 ])  -> SmtInterface.SMT_IntExpr (ctx.MkMul (e1, e2) :?> Microsoft.Z3.IntExpr)
            |   _ -> failwith (sprintf "smt_map_term_background_function: error (t = %s)" (term_to_string eng (AppTerm eng (FctId fct_id, ts))))
        else failwith (sprintf "smt_map_app_term: '%s' is not a background function" f)   // smt_map_term_user_defined_function initial_flag sign C (f, ts)

    let smt_map_initial (f_id : FCT_ID, ts) : SmtInterface.SMT_EXPR =
        let FctName f, { fct_kind = f_kind } = get_function' eng f_id
        if f_kind = Signature.Controlled then
            let sign = engines.[eid].signature
            let fail (f, dom, ran) =
                failwith (sprintf "smt_map_term_user_defined_function: function '%s : %s -> %s' not found" f (Signature.type_list_to_string dom) (Signature.type_to_string ran))
            match (f, Signature.fct_type f sign, ts >>| fun t -> smt_map_term eng t) with
            |   (f, (dom, Signature.Boolean), es) ->
                    try SmtInterface.SMT_BoolExpr (ctx.MkApp (Map.find f fct, Array.ofList (es >>| SmtInterface.convert_to_expr)) :?> Microsoft.Z3.BoolExpr) with _ -> fail (f, dom, Signature.Boolean)
            |   (f, (dom, Signature.Subset (_, Signature.Boolean)), es) ->       // !!! is it allowed in AsmetaL to have nested subset types? in that case this would fail
                    try SmtInterface.SMT_BoolExpr (ctx.MkApp (Map.find f fct, Array.ofList (es >>| SmtInterface.convert_to_expr)) :?> Microsoft.Z3.BoolExpr) with _ -> fail (f, dom, Signature.Boolean)
            |   (f, (dom, Signature.Integer), es) ->
                    try SmtInterface.SMT_IntExpr (ctx.MkApp (Map.find f fct, Array.ofList (es >>| SmtInterface.convert_to_expr)) :?> Microsoft.Z3.IntExpr) with _ -> fail (f, dom, Signature.Integer)
            |   (f, (dom, Signature.Subset (_, Signature.Integer)), es) ->       // !!! is it allowed in AsmetaL to have nested subset types? in that case this would fail
                    try SmtInterface.SMT_IntExpr (ctx.MkApp (Map.find f fct, Array.ofList (es >>| SmtInterface.convert_to_expr)) :?> Microsoft.Z3.IntExpr) with _ -> fail (f, dom, Signature.Integer)
            |   (f, (dom, (ran as Signature.TypeCons (tyname, []))), es) ->
                    let (kind, ar) = (Signature.type_kind tyname sign, Signature.type_arity tyname sign)
                    if kind <> Signature.EnumType || ar <> 0 then failwith (sprintf "smt_map_term_user_defined_function: types in function '%s : %s -> %s' not supported" f (Signature.type_list_to_string dom) (Signature.type_to_string ran))
                    try SmtInterface.SMT_Expr (ctx.MkApp (Map.find f fct, Array.ofList (es >>| SmtInterface.convert_to_expr))) with _ -> fail (f, dom, ran)
            |   (f, (_, ran), _) -> failwith (sprintf "smt_map_term_user_defined_function : error (t = %s)" (term_to_string eng (AppTerm eng (f_id, ts))))
        else failwith (sprintf "smt_map_initial: '%s' is not a controlled function" f)   // smt_map_term_user_defined_function initial_flag sign C (f, ts)

    match get_smt_expr eng t with
    |   Some e -> e
    |   None ->
            let result = 
                match get_term' eng t with
                |   Value' (INT i)           -> SmtInterface.SMT_IntExpr (ctx.MkInt i)
                |   Value' (BOOL b)          -> SmtInterface.SMT_BoolExpr (ctx.MkBool b)
                |   Value' (CELL (cons, [])) -> SmtInterface.SMT_Expr (Map.find cons (!C.con))
                |   Initial' (f, xs)         -> smt_map_initial (f, xs >>| Value eng)
                |   CondTerm' (G, t1, t2)    -> smt_map_cond (G, t1, t2)
                |   UnfoldedTerm' ((f, xs), M)  -> smt_map_term eng (unfolded_to_cond CondTerm eng ((f, xs), M))
                |   AppTerm' (f, ts)         -> smt_map_app_term (f, ts)
                |   _ -> failwith (sprintf "smt_map_term: not supported (t = %s)" (term_to_string eng t))
            set_smt_expr eng t result
            result

//--------------------------------------------------------------------
//
//  symbolic evaluator
//  
//  through the symbolic evaluation functions:
//  - S or eng   stands for engine
//  - env        stands for variable environment
//
//--------------------------------------------------------------------

and s_not eng t =
    match get_term' eng t with
    |   Value' (BOOL b) -> Value eng (BOOL (not b))
    |   _ -> AppTerm eng (NOT eng, [t])

and s_equals eng (t1, t2) =
    if t1 = t2 then TRUE eng
    else
        match (get_term' eng t1, get_term' eng t2) with
        |   (Value' x1, Value' x2) -> if x1 = x2 then TRUE eng else FALSE eng
        |   (_, _) -> AppTerm eng (EQUALS eng, [t1; t2])

let s_and eng (phi1, phi2)=
    match (get_term' eng phi1, get_term' eng phi2) with
    |   (Value' (BOOL false), _) -> FALSE eng
    |   (Value' (BOOL true), _) -> phi2
    |   (_, Value' (BOOL false)) -> FALSE eng
    |   (_, Value' (BOOL true)) -> phi1
    |   (phi1', phi2') -> if phi1 = phi2 then phi1 else AppTerm eng (AND eng, [phi1; phi2])

let s_or eng (phi1, phi2) =
    match (get_term' eng phi1, get_term' eng phi2) with
    |   (Value' (BOOL false), _) -> phi2
    |   (Value' (BOOL true), _) -> TRUE eng
    |   (_, Value' (BOOL false)) -> phi1
    |   (_, Value' (BOOL true)) -> TRUE eng
    |   (_, _) -> if phi1 = phi2 then phi1 else AppTerm eng (OR eng, [phi1; phi2])

let s_xor eng (phi1, phi2) =
    match (get_term' eng phi1, get_term' eng phi2) with
    |   (Value' (BOOL false), _) -> phi2
    |   (Value' (BOOL true), _) -> s_not eng phi2
    |   (_, Value' (BOOL false)) -> phi1
    |   (_, Value' (BOOL true)) -> s_not eng phi1
    |   (_, _) -> if phi1 = phi2 then FALSE eng else AppTerm eng (get_fct_id eng "xor", [phi1; phi2])

let s_implies eng (phi1, phi2) =
    match (get_term' eng phi1, get_term' eng phi2) with
    |   (Value' (BOOL b1), _) -> s_or eng (Value eng (BOOL (not b1)), phi2)
    |   (_, Value' (BOOL b2)) -> s_or eng (s_not eng phi1, Value eng (BOOL b2))
    |   (_, _) -> if phi1 = phi2 then TRUE eng else AppTerm eng (get_fct_id eng "implies", [phi1; phi2])

let s_iff eng (phi1, phi2) =
    match (get_term' eng phi1, get_term' eng phi2) with
    |   (Value' (BOOL false), _) -> s_not eng phi2
    |   (Value' (BOOL true), _) -> phi2
    |   (_, Value' (BOOL false)) -> s_not eng phi1
    |   (_, Value' (BOOL true)) -> phi1
    |   (_, _) -> if phi1 = phi2 then TRUE eng else AppTerm eng (get_fct_id eng  "iff", [phi1; phi2])


let ctx_condition eng C =
    List.fold (fun a -> fun b -> s_and eng (a, b)) (TRUE eng) (Set.toList C)

let smt_assert (eng as Engine eid) (phi : TERM) =
    let C = engines.[eid].smt_ctx
    if get_term_type eng phi = BooleanType eng
    then match smt_map_term eng phi with
         | SmtInterface.SMT_BoolExpr be -> C.ctr := !C.ctr + 1; (!C.slv).Assert be
         | _ -> failwith (sprintf "smt_assert: error converting Boolean term (term = %s)" (term_to_string eng phi))
    else failwith (sprintf "'smt_assert' expects a Boolean term, %s found instead " (term_to_string eng phi))

let with_extended_path_cond (eng : ENGINE) (G : TERM) (eval_fct : 'a -> ENGINE -> UPDATE_MAP * ENV * PATH_COND -> 'a) (term_or_rule : 'a) (UM : UPDATE_MAP, env : ENV, (C, M) : PATH_COND) : 'a =
    smt_solver_push eng
    smt_assert eng G
    let result = eval_fct term_or_rule eng (UM, env, (Set.add G C, M))
    smt_solver_pop eng
    result

let with_asgn_added_to_path_cond (eng : ENGINE) ((f : FCT_ID, xs : VALUE list), t_rhs : TERM) (eval_fct : 'a -> ENGINE -> UPDATE_MAP * ENV * PATH_COND -> 'a) (term_or_rule : 'a) (UM : UPDATE_MAP, env : ENV, (C, M) : PATH_COND) : 'a =
//  fprintf stderr "with_asgn_added_to_path_cond: adding assignment %s := %s to path condition\n" (location_to_string eng (f, xs)) (term_to_string eng t_rhs)
    let equation = AppTerm eng (EQUALS eng, [Initial eng (f, xs); t_rhs])
    let eval_in_changed_smt_scope (new_C, new_M) equation =
        smt_solver_push eng
        smt_assert eng equation
        let result = eval_fct term_or_rule eng (UM, env, (new_C, new_M))
        smt_solver_pop eng
        result
    let eval_in_unchanged_smt_scope () =
        eval_fct term_or_rule eng (UM, env, (C, M))
    match M.TryGetValue f with
    |   true, f_map ->
            match f_map.TryGetValue xs with
            |   true, f_xs_value ->
                    if f_xs_value <> t_rhs then
                        // if 'initial' location assignments are inconsistent, then the whole path condition is unsatisfiable
                        // note: M is not valid in this case => C must always be checked before using M
                        // (for additional safety, M is cleared)
                        // fprintf stderr "add_asgn: inconsistent assignments %s, %s => this path can never be taken\n" (show_s_update eng ((f, xs), f_xs_value)) (show_s_update eng ((f, xs), t_rhs))
                        eval_in_changed_smt_scope (Set.add (FALSE eng) C, Map.empty) equation
                    else
                        // leave M unchanged as the same assignment is already present
                        //fprintf stderr "add_asgn: assignment %s := %s already present in path condition\n" (location_to_string eng (f, xs)) (term_to_string eng t_rhs)
                        //if not (Set.contains equation C) then failwith "with_asgn_added_to_path_cond: expected equation already in path condition"
                        //Set.add equation C, M
                        eval_in_unchanged_smt_scope ()
                        //eval_in_changed_smt_scope (C, M)
            |   _ -> eval_in_changed_smt_scope (Set.add equation C, Map.add f (Map.add xs t_rhs f_map) M) equation
    |   _ -> eval_in_changed_smt_scope (Set.add equation C, Map.add f (Map.add xs t_rhs Map.empty) M) equation

//--------------------------------------------------------------------

let smt_formula_is_true (eng as Engine eid) (phi : TERM) =
    let C = engines.[eid].smt_ctx
    if get_term_type eng phi = BooleanType eng
    then match smt_map_term eng phi with
         | SmtInterface.SMT_BoolExpr be ->
                C.ctr := !C.ctr + 1;
                let result = ((!C.slv).Check ((!C.ctx).MkNot be) = Microsoft.Z3.Status.UNSATISFIABLE);
                // if trace_smt_calls then fprintf stderr "smt_formula_is_true[scope=%d]: %s -> %b\n" (SmtInterface.smt_scope_id C) (term_to_string eng phi) result;
                result
         | _ -> failwith (sprintf "smt_formula_is_true: error converting Boolean term (term = %s)" (term_to_string eng phi))
    else failwith (sprintf "'smt_formula_is_true' expects a Boolean term, %s found instead " (term_to_string eng phi))

let smt_formula_is_false (eng as Engine eid) (phi : TERM) =
    if trace_smt_calls then fprintf stderr "smt_formula_is_false: %s -> " (term_to_string eng phi)
    let C = engines.[eid].smt_ctx
    if get_term_type eng phi = BooleanType eng
    then match smt_map_term eng phi with
         | SmtInterface.SMT_BoolExpr be ->
                C.ctr := !C.ctr + 1;
                let result = ((!C.slv).Check be = Microsoft.Z3.Status.UNSATISFIABLE);
                // if trace_smt_calls then fprintf stderr "smt_formula_is_false[scope=%d]: %s -> %b\n" (SmtInterface.smt_scope_id C) (term_to_string eng phi) result;
                result
         | _ -> failwith (sprintf "smt_formula_is_false: error converting Boolean term (term = %s)" (term_to_string eng phi))
    else failwith (sprintf "'smt_formula_is_false' expects a Boolean term, %s found instead " (term_to_string eng phi))

let rec interpretation (eng : ENGINE) (UM : UPDATE_MAP) (pc : PATH_COND) (f as FctId f_id) (xs : VALUE list) =
    let Value = Value eng
    let xs = match xs with [TUPLE xs'] -> xs' | _ -> xs    // unpack single tuple (x_1, ..., x_n) into arguments x_1, ..., x_n, if needed
    let eval_fct_definition_in_curr_state (fct_definition as (args, body)) xs =
        let env = List.fold2 (fun env' arg x -> add_binding env' (arg, Value x)) Map.empty args xs
        let body' = body        // alternative: // let body' = replace_vars eng env body
        s_eval_term eng body' (UM, env, pc)
    let eval_fct_definition_in_initial_state (fct_definition as (args, body)) xs =
        let env = List.fold2 (fun env' arg x -> add_binding env' (arg, Value x)) Map.empty args xs
        let body' = body        // alternative: // let body' = replace_vars eng env body
        s_eval_term eng body' (Map.empty, env, empty_path_cond)   //!!!! to be modified if at some point initial state constraints are implemented => path condition may then be non-empty
    let FctName f_name, { fct_interpretation = f_intp; fct_id = f_id } = get_function' eng f
    match f_intp with
    |   Constructor (fct_interpretation : VALUE list -> VALUE) ->
            Value (fct_interpretation xs)
    |   StaticBackground (fct_interpretation : VALUE list -> VALUE) ->
            Value (fct_interpretation xs)
    |   StaticUserDefined (_ : VALUE list -> VALUE, Some (fct_def : string list * TERM)) ->
            // memoization of computed values for static user-defined functions
            let res = initial_state_eval_res eng (AppTerm eng (f, xs >>| Value))
            match !res with
            |   Some t' -> t'
            |   None -> let t' = eval_fct_definition_in_initial_state fct_def xs in res := Some t'; t'
    |   ControlledInitial (_ : VALUE list -> VALUE, Some (fct_def : string list * TERM)) -> 
            try Map.find xs (Map.find (FctId f_id) UM)
            with _ ->
                let res = initial_state_eval_res eng (AppTerm eng (f, xs >>| Value))
                match !res with
                |   Some t' -> t'
                |   None -> let t' = eval_fct_definition_in_initial_state fct_def xs in res := Some t'; t'
    |   ControlledUninitialized ->
            try Map.find xs (Map.find (FctId f_id) UM)
            with _ -> Initial eng (f, xs)
    |   Derived (Some (fct_def : string list * TERM)) ->
            eval_fct_definition_in_curr_state fct_def xs
    |   Derived None ->
            failwith (sprintf "definition of derived function '%s' missing" f_name)
    |   StaticUserDefined (_, None) ->
            failwith (sprintf "definition of static function '%s' missing" f_name)
    |   ControlledInitial (_, None) -> 
            failwith (sprintf "initial state definition of controlled function '%s' missing" f_name)

and symbolic_interpretation (eng : ENGINE) (UM : UPDATE_MAP) (pc : PATH_COND) (f as FctId f_id) (ts : TERM list) =
    let Value = Value eng
    let ts =            // unpack single tuple (t_1, ..., t_n) into arguments t_1, ..., t_n, if needed
        match ts with
        | [t] ->
            match get_type' eng (get_term_type eng t) with
            |   Prod' _ ->  // single argument is of product type, i.e. a tuple => try to extract arguments from tuple
                match get_term' eng t with
                |   TupleTerm' ts' -> ts'
                |   Value' (TUPLE ts') -> ts' >>| Value
                |   _ -> failwith (sprintf "symbolic_interpretation: cannot extract arguments of '%s' from term '%s', which is of product type (i.e. a tuple)" (fct_name eng f) (term_to_string eng t))
            |   _ -> ts     // single argument is not expected to be a tuple => continue normally
        | _ -> ts
    let eval_fct_definition_in_curr_state (fct_definition as (args, body)) (ts : TERM list) =
        let env = List.fold2 (fun env' arg t -> add_binding env' (arg, t)) Map.empty args ts
        let body' = body        // alternative: // let body' = replace_vars eng env body
        s_eval_term eng body' (UM, env, pc)
    let eval_fct_definition_in_initial_state (fct_definition as (args, body)) (ts : TERM list) =
        let env = List.fold2 (fun env' arg t -> add_binding env' (arg, t)) Map.empty args ts
        let body' = body        // alternative: // let body' = replace_vars eng env body
        s_eval_term eng body' (Map.empty, env, empty_path_cond)   //!!!! to be modified if at some point initial state constraints are implemented => path condition may then be non-empty
    let FctName f_name, { fct_interpretation = f_intp; fct_id = f_id } = get_function' eng f
    match f_intp with
    |   Constructor (fct_interpretation : VALUE list -> VALUE) ->
            failwith "symbolic_interpretation: constructor functions not supported"
    |   StaticBackground (fct_interpretation : VALUE list -> VALUE) ->
            failwith "symbolic_interpretation: static background functions not supported"
    |   StaticUserDefined (_ : VALUE list -> VALUE, Some (fct_def : string list * TERM)) ->
            // memoization of computed values for static user-defined functions
            let res = initial_state_eval_res eng (AppTerm eng (f, ts))
            match !res with
            |   Some t' -> t'
            |   None -> let t' = eval_fct_definition_in_initial_state fct_def ts in res := Some t'; t'
    |   ControlledInitial (_ : VALUE list -> VALUE, Some (fct_def : string list * TERM)) -> 
            failwith "symbolic_interpretation: (initialized) controlled functions not supported"
    |   ControlledUninitialized ->
            failwith "symbolic_interpretation: (uninitialized) controlled functions not supported"
    |   Derived (Some (fct_def : string list * TERM)) ->
            eval_fct_definition_in_curr_state fct_def ts
    |   Derived None ->
            failwith (sprintf "definition of derived function '%s' missing" f_name)
    |   StaticUserDefined (_, None) ->
            failwith (sprintf "definition of static function '%s' missing" f_name)
    |   ControlledInitial (_, None) -> 
            failwith (sprintf "initial state definition of controlled function '%s' missing" f_name)

and smt_eval_formula (phi : TERM) (eng as Engine eid: ENGINE) (UM : UPDATE_MAP, env, pc : PATH_COND) =
    // precondition: term_type sign phi = Boolean
    // precondition: phi does not contain variables (i.e., it is fully expanded) - this is the case if smt_eval_formula is applied to the result of s_eval_term
    let enable_caching = true
    let C = engines[eid].smt_ctx
    let result_cache = (get_term_attrs eng phi).smt_result
    let scope_id_stack = !C.scopeIdStack
    let inline smt_reduce_bool_expr phi =
        if get_term_type eng phi = BooleanType eng then
            match smt_map_term eng phi with
            | SmtInterface.SMT_BoolExpr be ->
                    if (C.ctr := !C.ctr + 1; (!C.slv).Check ((!C.ctx).MkNot be) = Microsoft.Z3.Status.UNSATISFIABLE)
                    then TRUE eng
                    else if (C.ctr := !C.ctr + 1; (!C.slv).Check be = Microsoft.Z3.Status.UNSATISFIABLE)
                    then FALSE eng
                    else phi
            | _ -> failwith (sprintf "smt_check_formula: error converting Boolean term (term = %s)" (term_to_string eng phi))
        else failwith (sprintf "'smt_reduce_bool_expr' expects a Boolean term, %s found instead " (term_to_string eng phi))
    let rec find_cached_in_stack (stack : int list) : TERM option =
        match stack with
        |   [] -> None
        |   scope_id :: rest ->
                match result_cache.TryGetValue(scope_id) with
                |   true, found_result -> Some found_result
                |   _ -> find_cached_in_stack rest
    let result =
        if not enable_caching then smt_reduce_bool_expr phi else
            match result_cache.TryGetValue(List.head scope_id_stack) with
            |   true, cached_result ->
                    if !trace > 0 || trace_smt_calls then fprintf stderr "[CACHED AT TOP] "
                    cached_result
            |   _ ->
                match find_cached_in_stack (List.tail scope_id_stack) with
                |   Some cached_result ->
                        if !trace > 0 || trace_smt_calls then fprintf stderr "[CACHED INSIDE] "
                        let inner_result =
                            if cached_result = TRUE eng || cached_result = FALSE eng
                            then cached_result
                            else smt_reduce_bool_expr phi
                        result_cache.Add(SmtInterface.smt_scope_id C, inner_result)
                        inner_result
                |   None ->
                        let inner_result = smt_reduce_bool_expr phi
                        result_cache.Add(SmtInterface.smt_scope_id C, inner_result)
                        inner_result
    if !trace > 0 || trace_smt_calls then fprintf stderr "smt_eval_formula[scope=%d]: %s -> %s\n" (SmtInterface.smt_scope_id C) (term_to_string eng phi) (term_to_string eng result)
    result

and expand_quantifier (q_kind, v, t_set : UPDATE_MAP * ENV * PATH_COND -> TERM, t_cond : UPDATE_MAP * ENV * PATH_COND -> TERM)
                        (eng : ENGINE) (UM : UPDATE_MAP, env : ENV, pc : PATH_COND) : TERM =
    let t_set = t_set (UM, env, pc)
    let t_set_type = get_term_type eng t_set
    let _ =
        match get_type' eng t_set_type with
        |   Powerset' tyname -> tyname
        |   _ -> failwith (sprintf "Engine.expand_quantifier: expected a set or domain type, %s found instead" (type_to_string eng t_set_type))
    match get_term' eng (s_eval_term_with_unfolding eng t_set (UM, env, pc)) with
    |   Value' (Background.SET (_, xs)) ->
            let eval_instance x = t_cond (UM, add_binding env (v, Value eng x), pc)
            let t_conds = List.map eval_instance (Set.toList xs)
            match q_kind with
            |   AST.Forall -> List.fold (fun (t_accum : TERM) -> fun (t1 : TERM) -> s_and eng (t_accum, t1)) (TRUE eng)  t_conds
            |   AST.Exist  -> List.fold (fun (t_accum : TERM) -> fun (t1 : TERM) -> s_or  eng (t_accum, t1)) (FALSE eng) t_conds
            |   AST.ExistUnique -> failwith "Engine.expand_quantifier: 'ExistUnique' not implemented"
    |   CondTerm' (G, t1, t2) ->
            CondTerm eng (G,
                expand_quantifier (q_kind, v, (fun (UM, env, pc) -> t1), t_cond) eng (UM, env, pc),
                expand_quantifier (q_kind, v, (fun (UM, env, pc) -> t2), t_cond) eng (UM, env, pc))
    |   UnfoldedTerm' ((f, xs), M) ->
            UnfoldedTerm eng ((f, xs),
                Map.map (fun _ t_i -> expand_quantifier (q_kind, v, (fun (UM, env, pc) -> t_i), t_cond) eng (UM, env, pc)) M)
    |   x -> failwith (sprintf "Engine.expand_quantifier: not a set (%s)" (term_to_string eng t_set))

and cases eng (condConstructor : ENGINE -> TERM * 'a * 'a -> 'a) (t : TERM) (x_t_list : (VALUE * 'a) list) : 'a =
    // the second element of the pairs in x_t_list is typically of type
    //  - TERM (then the parameter 'condConstructor' should be 'CondTerm'), or
    //  - RULE (then the parameter 'condConstructor' should be 'CondRule')
    let eq t1 t2 = s_equals eng (t1, t2)
    let rec mk_cond_term = function
    |   [] -> failwith "cases: empty list of cases"
    |   [(x1, t1)] -> t1        // does not use x1, because this is the 'else' case
    |   (x1, t1) :: cases' -> condConstructor eng (eq t (Value eng x1), t1, mk_cond_term cases')
    mk_cond_term x_t_list

and s_eval_term_ (eng : ENGINE) (unfold_locations : bool) (t : TERM) (UM : UPDATE_MAP, env : ENV, pc : PATH_COND) : TERM =
    let cases = cases eng CondTerm
    let TRUE, FALSE, get_term', fct_name, fct_kind = TRUE eng, FALSE eng, get_term' eng, fct_name eng, fct_kind eng
    let s_and, s_or, s_not, s_xor, s_implies, s_iff, s_equals = s_and eng, s_or eng, s_not eng, s_xor eng, s_implies eng, s_iff eng, s_equals eng
    let Value, Initial, AppTerm, CondTerm, UnfoldedTerm, VarTerm, LetTerm, DomainTerm, QuantTerm = Value eng, Initial eng, AppTerm eng, CondTerm eng, UnfoldedTerm eng, VarTerm eng, LetTerm eng, DomainTerm eng, QuantTerm eng
    let get_type, get_term_type, get_type', get_values = get_type eng, get_term_type eng, get_type' eng, get_values eng
    let pp_term, term_to_string = pp_term eng, term_to_string eng

    if !trace > 0 then
        fprintf stderr "%s[[ %s ]]_%s - unfold=%b\n" (spaces()) (indent (pp_term t)) (show_s_update_map eng UM) unfold_locations
        level := !level + 1

    let rec eval_term_with_ext_path_cond (unfold_locations : bool) (G : TERM) (t : TERM) (UM : UPDATE_MAP, env : ENV, pc : PATH_COND) =
        with_extended_path_cond eng G (fun t eng -> eval_term unfold_locations t) t (UM, env, pc)

    and eval_term_with_asgn_added_to_path_cond (unfold_locations : bool) ((f : FCT_ID, xs : VALUE list), t_rhs : TERM) (t : TERM) (UM : UPDATE_MAP, env : ENV, pc : PATH_COND) =
        with_asgn_added_to_path_cond eng ((f, xs), t_rhs) (fun t eng -> eval_term unfold_locations t) t (UM, env, pc)

    and eval_app_term (unfold_locations : bool) (fct_id : FCT_ID, ts : TERM list) (UM : UPDATE_MAP, env : ENV, pc : PATH_COND) : TERM = 
        let FctName f_name, { fct_kind = f_kind; fct_interpretation = f_intp }  = get_function' eng fct_id
        // The following lines of code force the unfolding of 'initial' locations contained in this term if 'fct_id' is controlled or derived.
        let unfold_locations = unfold_locations || f_kind = Signature.Controlled || f_kind = Signature.Derived (* || f_kind = Signature.Static *)
        // As an alternative, symbolic interpretation without unfolding may be used for non-recursive derived functions.

        let eval_term t (UM, env, pc) = eval_term unfold_locations t (UM, env, pc)
        let eval_bool_term t (UM, env, pc) = eval_bool_term unfold_locations t (UM, env, pc)

        let rec F ts_initial (ts_past_rev : TERM list, xs_past_opt_rev: VALUE list option) (ts : TERM list) (UM, env, pc) =
            let F_reiterate = F
            let F = F ts_initial
            match ts with
            |   t1 :: ts_fut ->
                    match get_term' t1 with
                    |   CondTerm' (G1, t11, t12) ->
                            CondTerm (G1, F (ts_past_rev, xs_past_opt_rev) (t11 :: ts_fut) (UM, env, pc), F (ts_past_rev, xs_past_opt_rev) (t12 :: ts_fut) (UM, env, pc))
                    |   UnfoldedTerm' ((f, xs), M) ->
                            UnfoldedTerm ((f, xs), Map.map (fun _ t_i -> F (ts_past_rev, xs_past_opt_rev) (t_i :: ts_fut) (UM, env, pc)) M)
                    |   _ ->
                        let t1 = eval_term t1 (UM, env, pc)
                        match get_term' t1 with
                        |   Value' x1     -> F (t1 :: ts_past_rev, Option.map (fun xs -> x1 :: xs) xs_past_opt_rev) ts_fut (UM, env, pc)
                        |   Initial' _    -> F (t1 :: ts_past_rev, None) ts_fut (UM, env, pc)
                        |   AppTerm'  _   -> F (t1 :: ts_past_rev, None) ts_fut (UM, env, pc) 
                        |   TupleTerm' _  -> F (t1 :: ts_past_rev, None) ts_fut (UM, env, pc)   
                        |   CondTerm' _   -> F (ts_past_rev, xs_past_opt_rev) (t1 :: ts_fut) (UM, env, pc)      // reiterate 'lifting' of conditional, if needed, until no conditional left
                        |   UnfoldedTerm' _  -> F (ts_past_rev, xs_past_opt_rev) (t1 :: ts_fut) (UM, env, pc)      // reiterate 'lifting' of unfolded term, if needed, until no unfolded term left
                        |   LetTerm'  _   -> failwith "Engine.eval_app_term: LetTerm should not occur here"
                        |   VarTerm'  _   -> failwith "Engine.eval_app_term: VarTerm should not occur here"
                        |   QuantTerm' _  -> failwith "Engine.eval_app_term: QuantTerm should not occur here"
                        |   DomainTerm' _ -> failwith "Engine.eval_app_term: DomainTerm should not occur here"
            |   [] ->
                    let xs_opt_eval = Option.map List.rev xs_past_opt_rev
                    match xs_opt_eval with
                    |   Some xs ->
                            interpretation eng UM pc fct_id xs       // arguments fully evaluated to values
                    |   None ->
                            let ts_eval = List.rev ts_past_rev
                            match f_kind with
                            |   Signature.Static ->
                                    if AppTerm (fct_id, ts_eval) <> AppTerm (fct_id, ts_initial) then
                                        // fixed point is not reached yet: try reducing further before failing
                                        let ts_eval = ts_eval >>| fun t -> eval_term t (UM, env, pc)
                                        F_reiterate ts_eval ([], Some []) ts_eval (UM, env, pc)
                                    else
                                        match f_name, ts_eval with
                                        |   "and", [ t1; t2 ] -> s_and (t1, t2)
                                        |   "or", [ t1; t2 ]  -> s_or (t1, t2)
                                        |   "xor", [ t1; t2 ] -> s_xor (t1, t2)
                                        |   "implies", [ t1; t2 ] -> s_implies (t1, t2)
                                        |   "iff", [ t1; t2 ] -> s_iff (t1, t2)
                                        |   "=", [ t1; t2 ]   -> s_equals (t1, t2)
                                        |   _, ts             ->
                                                match f_intp with
                                                |   StaticBackground _ -> AppTerm (fct_id, ts)          // if f is a background function, keep term as it is (possibly for SMT mapping later)
                                                |   StaticUserDefined (_, Some _) -> symbolic_interpretation eng UM pc fct_id ts        // if f is user defined, try symbolic evaluation
                                                |   StaticUserDefined (_, None) -> failwith (sprintf "definition of static function '%s' missing" f_name)
                                                |   _ -> failwith (sprintf "Engine.eval_app_term: function '%s' in term '%s': only static functions should occur here" f_name (term_to_string t))
                            |   Signature.Derived ->
                                    // Derived functions are evaluated symbolically, if the arguments could not be fully evaluated.
                                    // !!! Note: this is dangerous for recursive functions, as symbolic evaluation may sometimes not terminate even if the function always terminates.
                                    if AppTerm (fct_id, ts_eval) <> AppTerm (fct_id, ts_initial) then
                                        // fixed point is not reached yet: try reducing further before failing
                                        let ts_eval = ts_eval >>| fun t -> eval_term t (UM, env, pc)
                                        F_reiterate ts_eval ([], Some []) ts_eval (UM, env, pc)
                                    else
                                        symbolic_interpretation eng UM pc fct_id ts_eval
                                    // For the above reason, symbolic interpretation is used only as a fallback, when arguments cannot be fully evaluated even after unfolding.
                                    // As an alternative, symbolic interpretation without unfolding may be used for non-recursive derived functions.
                                    // This alternative implementation may be especially advantageous in combination with memoization.
                            |   Signature.Controlled ->
                                    if AppTerm (fct_id, ts_eval) <> AppTerm (fct_id, ts_initial) then
                                        // fixed point is not reached yet: try reducing further before failing
                                        let ts_eval = ts_eval >>| fun t -> eval_term t (UM, env, pc)
                                        F_reiterate ts_eval ([], Some []) (ts_eval >>| fun t -> eval_term t (UM, env, pc)) (UM, env, pc)
                                        //F_reiterate ts_eval ([], Some []) ts_eval (UM, env, pc)
                                    else
                                        failwith (sprintf "Engine.eval_app_term: arguments of controlled function '%s' must be fully evaluable for unambiguous determination of a location\n('%s' found instead)" f_name (term_to_string (AppTerm (fct_id, ts_eval))))
                            |   other_kind ->
                                    failwith (sprintf "Engine.eval_app_term: function '%s' in term '%s': %s functions are not supported" f_name (term_to_string t) (Signature.fct_kind_to_string other_kind))
        let f_name = fct_name fct_id
        let F (ts_past, xs_past_opt) ts (UM, env, pc) = F ts (ts_past, xs_past_opt) ts (UM, env, pc)
        match f_name, ts with
        |   "and", [ t1; t2 ] ->
                let t1_eval = eval_term t1 (UM, env, pc)
                match get_term' t1_eval with
                |   Value' (BOOL false) -> FALSE
                |   Value' (BOOL true)  -> eval_term t2 (UM, env, pc)     // eval_bool_term_with_ext_path_cond t1_eval t2 (UM, env, pc)           
                |   _ ->
                    let t2_eval = eval_term t2 (UM, env, pc)
                    match get_term' t2_eval with
                    |   Value' (BOOL false) -> FALSE
                    |   Value' (BOOL true)  -> t1_eval            // eval_bool_term t1 (UM, env, pc)
                    |   _ -> if t1_eval = t2_eval then t1_eval else F ([], Some []) [t1_eval; t2_eval] (UM, env, pc)
        |   "or", [ t1; t2 ] ->
                let t1_eval = eval_term t1 (UM, env, pc)
                match get_term' t1_eval with
                |   Value' (BOOL true) -> TRUE
                |   Value' (BOOL false) -> eval_term t2 (UM, env, pc)            // eval_bool_term t2 (UM, env, pc)
                |   _ ->
                    let t2_eval = eval_term t2 (UM, env, pc)
                    match get_term' t2_eval with
                    |   Value' (BOOL true) -> TRUE
                    |   Value' (BOOL false) -> t1_eval           // t1_eval
                    |   _ -> if t1_eval = t2_eval then t1_eval else F ([], Some []) [t1_eval; t2_eval] (UM, env, pc)
        |   "implies", [ t1; t2 ] ->
                let t1_eval = eval_term t1 (UM, env, pc)
                match get_term' t1_eval with
                |   Value' (BOOL false) -> TRUE
                |   Value' (BOOL true)  -> eval_term t2 (UM, env, pc)       // with_extended_path_cond t1' ( fun _ _ -> t2) (S, env, C)
                |   _ ->
                    let t2_eval = eval_term t2 (UM, env, pc)
                    match get_term' t2_eval with
                    |   Value' (BOOL false) -> s_not t1_eval
                    |   Value' (BOOL true)  -> TRUE
                    |   _ -> if t1_eval = t2_eval then TRUE else F ([], Some []) [t1_eval; t2_eval] (UM, env, pc)
        |   "iff", [ t1; t2 ] ->
                let t1_eval = eval_term t1 (UM, env, pc)
                match get_term' t1_eval with
                |   Value' (BOOL false) -> s_not (eval_term t2 (UM, env, pc))
                |   Value' (BOOL true)  -> eval_term t2 (UM, env, pc)
                |   _ ->
                    let t2_eval = eval_term t2 (UM, env, pc)
                    match get_term' t2_eval with
                    |   Value' (BOOL false) -> s_not t1_eval
                    |   Value' (BOOL true)  -> t1_eval
                    |   _ -> if t1_eval = t2_eval then TRUE else F ([], Some []) [t1_eval; t2_eval] (UM, env, pc)
        |   "=", [ t1; t2 ] ->
                let t1_eval = eval_term t1 (UM, env, pc)
                match get_term' t1_eval with
                |   t1' as Value' x1 ->
                    let t2_eval = eval_term t2 (UM, env, pc)
                    match get_term' t2_eval with
                    |   Value' x2 -> Value (BOOL (x1 = x2))
                    |   t2' -> F ([], Some []) [t1_eval; t2_eval] (UM, env, pc)
                |   t1' -> F ([], Some []) [t1_eval; eval_term t2 (UM, env, pc)] (UM, env, pc)
        |   _ ->
        F ([], Some []) ts (UM, env, pc)

    and eval_tuple_term (unfold_locations : bool) (ts : TERM list) (UM : UPDATE_MAP, env : ENV, pc : PATH_COND) : TERM = 
        let eval_term t = eval_term unfold_locations t (UM, env, pc)
        let rec F ts_initial (ts_past_rev : TERM list, xs_past_opt_rev: VALUE list option) (ts : TERM list) =
            let F_reiterate = F
            let F = F ts_initial
            match ts with
            |   t1 :: ts_fut ->
                    match get_term' t1 with
                    |   CondTerm' (G1, t11, t12) ->
                            CondTerm (G1, F (ts_past_rev, xs_past_opt_rev) (t11 :: ts_fut), F (ts_past_rev, xs_past_opt_rev) (t12 :: ts_fut))
                    |   UnfoldedTerm' ((f, xs), M) ->
                            UnfoldedTerm ((f, xs), Map.map (fun _ t_i -> F (ts_past_rev, xs_past_opt_rev) (t_i :: ts_fut)) M)
                    |   _ ->
                        let t1 = eval_term t1
                        match get_term' t1 with
                        |   Value' x1     -> F (t1 :: ts_past_rev, Option.map (fun xs -> x1 :: xs) xs_past_opt_rev) ts_fut
                        |   Initial' _    -> F (t1 :: ts_past_rev, None) ts_fut
                        |   AppTerm'  _   -> F (t1 :: ts_past_rev, None) ts_fut
                        |   TupleTerm' _  -> F (t1 :: ts_past_rev, None) ts_fut
                        |   CondTerm' _   -> F (ts_past_rev, xs_past_opt_rev) (t1 :: ts_fut)        // reiterate 'lifting' of conditional, if needed, until no conditional left
                        |   UnfoldedTerm' _ -> F (ts_past_rev, xs_past_opt_rev) (t1 :: ts_fut)      // reiterate 'lifting' of unfolded term, if needed, until no unfolded term left
                        |   LetTerm'  _   -> failwith "Engine.eval_app_term: LetTerm should not occur here"
                        |   VarTerm'  _   -> failwith "Engine.eval_app_term: VarTerm should not occur here"
                        |   QuantTerm' _  -> failwith "Engine.eval_app_term: QuantTerm should not occur here"
                        |   DomainTerm' _ -> failwith "Engine.eval_app_term: DomainTerm should not occur here"
            |   [] ->
                    let xs_opt_eval = Option.map List.rev xs_past_opt_rev
                    match xs_opt_eval with
                    |   Some xs ->  Value (TUPLE xs)       // arguments fully evaluated to values
                    |   None ->     let ts_eval = List.rev ts_past_rev
                                    if ts_eval <> ts_initial then F_reiterate ts_eval ([], Some []) (ts_eval >>| eval_term) else TupleTerm eng ts_eval
        F ts ([], Some []) ts

    and eval_cond_term unfold_locations (G : TERM, t1 : TERM, t2 : TERM) (UM : UPDATE_MAP, env : ENV, pc : PATH_COND) : TERM =
        let eval_term t (UM, env, pc) = eval_term unfold_locations t (UM, env, pc)
        //let eval_bool_term t (UM, env, pc) = eval_bool_term unfold_locations t (UM, env, pc)
        let G_eval = eval_bool_term (if always_unfold_guards then true else unfold_locations) G (UM, env, pc)
        match get_term' G_eval with
        |   Value' (BOOL true)  -> eval_term t1 (UM, env, pc)
        |   Value' (BOOL false) -> eval_term t2 (UM, env, pc)
        |   CondTerm' (G', G1, G2) ->
                if get_type' (get_term_type G1) <> Boolean' || get_type' (get_term_type G2) <> Boolean'
                then failwith (sprintf "Engine.eval_cond_term: '%s' and '%s' must be boolean terms" (term_to_string G1) (term_to_string G2))
                else eval_term (CondTerm (G', CondTerm (G1, t1, t2), CondTerm (G2, t1, t2))) (UM, env, pc)
        |   UnfoldedTerm' ((f, xs), M) ->
                eval_term (UnfoldedTerm ((f, xs), Map.map (fun _ R_i -> CondTerm (R_i, t1, t2)) M)) (UM, env, pc)
        |   _ ->
                let t1_eval = eval_term_with_ext_path_cond unfold_locations G_eval         t1 (UM, env, pc)
                let t2_eval = eval_term_with_ext_path_cond unfold_locations (s_not G_eval) t2 (UM, env, pc)
                if t1_eval = t2_eval then t1_eval else CondTerm (G_eval, t1_eval, t2_eval)

    and eval_unfolded_term unfold_locations ((fct_id : FCT_ID, xs : VALUE list), cases_M : Map<VALUE, TERM>) (UM : UPDATE_MAP, env : ENV, (pc as (C, pc_M)) : PATH_COND) : TERM =
        let eval_term, eval_bool_term = eval_term unfold_locations, eval_bool_term unfold_locations
        let eval_term_with_asgn_added_to_path_cond = eval_term_with_asgn_added_to_path_cond unfold_locations
        let iterate_through_cases f_xs =
            let eq x = s_equals (f_xs, Value x)
            let rec F cases_list acc =
                match cases_list with
                |   [] -> acc
                |   (x_i, t_i) :: rest ->
                        let eq_x_i_eval = eval_term (eq x_i) (UM, env, pc) 
                        match get_term' eq_x_i_eval with
                        |   Value' (BOOL true)  -> [(x_i, (eval_term_with_asgn_added_to_path_cond ((fct_id, xs), Value x_i) t_i (UM, env, pc)))]
                        |   Value' (BOOL false) -> F rest acc
                        |   _ -> F rest ((x_i, eval_term_with_asgn_added_to_path_cond ((fct_id, xs), Value x_i) t_i (UM, env, pc)) :: acc)
            let new_cases_list = F (Map.toList cases_M) []
            match new_cases_list with
            |   [] -> failwith (sprintf "Engine.eval_unfolded_term: value of term '%s' is outside the expected range" (term_to_string f_xs))
            |   [(x_1, t_1)] -> t_1
            |   (x_1, t_1) :: other_cases ->
                    let all_equal = Seq.forall (fun (_, t_i) -> eval_term (s_equals (t_i, t_1)) (UM, env, pc) = TRUE) other_cases
                    if all_equal then t_1 else UnfoldedTerm ((fct_id, xs), Map.ofList new_cases_list)
        match pc_M |> Map.tryFind fct_id |> Option.bind (Map.tryFind xs) with
        |   Some f_xs_eval ->
            match get_term' f_xs_eval with
            |   Value' x_i ->
                match cases_M |> Map.tryFind x_i with
                |   Some t_i -> eval_term t_i (UM, env, pc)    // no need of eval_rule_with_asgn_added_to_path_cond, because path condition already contains the assignment
                |   None -> failwith (sprintf "Engine.eval_unfolded_term: value '%s' of term '%s' is outside the expected range" (value_to_string x_i) (term_to_string f_xs_eval))
            |   _ -> iterate_through_cases f_xs_eval
        |   None -> iterate_through_cases (Initial (fct_id, xs))

    and eval_let_term unfold_locations (v : string, t1 : TERM, t2 : TERM) (UM : UPDATE_MAP, env : ENV, pc : PATH_COND) : TERM =
        let eval_term t (UM, env, pc) = eval_term unfold_locations t (UM, env, pc)
        let t1 = eval_term t1 (UM, env, pc)
        eval_term t2 (UM, add_binding env (v, t1), pc)

    and eval_domain_term unfold_locations (dom : TYPE) (UM : UPDATE_MAP, env : ENV, pc : PATH_COND) : TERM =
        match enum_finite_type eng dom with
        |   Some xs -> Value (SET (main_type_of eng dom |> to_signature_type eng, xs))
        |   None -> failwith (sprintf "Engine.eval_domain_term: domain of type '%s' is not enumerable" (dom |> type_to_string eng))

    and eval_quant_term (unfold_locations : bool) (q_kind, v, t_set, t_cond) (UM : UPDATE_MAP, env : ENV, pc : PATH_COND) : TERM =
        let eval_term t (UM, env, pc) = eval_term unfold_locations t (UM, env, pc)
        let eval_tset (UM, env, pc) = eval_term t_set (UM, env, pc)
        let eval_tcond (UM, env, pc) = eval_term t_cond (UM, env, pc)
        expand_quantifier (q_kind, v, eval_tset, eval_tcond) eng (UM, env, pc)
    
    and eval_initial (unfold_locations : bool) (t : TERM) (f : FCT_ID, xs : VALUE list) (UM : UPDATE_MAP, env : ENV, (pc as (_, pc_M) : PATH_COND)) : TERM =
        // precondition t = Initial (fct_id, xs)
        match pc_M |> Map.tryFind f |> Option.bind (Map.tryFind xs) with
        |   Some f_xs_value -> f_xs_value
        |   None ->
                if unfold_locations then
                    match enum_finite_type eng (get_term_type t) with
                    |   None -> t
                    |   Some elems when Set.isEmpty elems -> failwith (sprintf "Engine.eval_initial: range of term '%s' is empty" (term_to_string t))       
                    |   Some elems -> UnfoldedTerm ((f, xs), elems |> Set.map (fun x -> x, Value x) |> Map.ofSeq)
                else
                    t

    and eval_term (unfold_locations : bool) (t : TERM) (UM : UPDATE_MAP, env : ENV, pc : PATH_COND) : TERM =
        if !trace > 1 then
            fprintf stderr "%s[[ %s ]]_%s - unfold=%b\n" (spaces()) (indent (pp_term t)) (show_s_update_map eng UM) unfold_locations
            level := !level + 1
        let t_result =
            match get_term' t with
            |   Value' _              -> t
            |   Initial' (f, xs)      -> eval_initial unfold_locations t (f, xs) (UM, env, pc)
            |   VarTerm' (v, ty)      -> eval_term unfold_locations (get_env env v) (UM, env, pc)
            |   AppTerm' (f, ts)      -> eval_app_term unfold_locations (f, ts) (UM, env, pc)
            |   TupleTerm' ts         -> eval_tuple_term unfold_locations ts (UM, env, pc)
            |   CondTerm' (G, t1, t2) -> eval_cond_term unfold_locations (G, t1, t2) (UM, env, pc)
            |   LetTerm' (v, t1, t2)  -> eval_let_term unfold_locations (v, t1, t2) (UM, env, pc)
            |   DomainTerm' dom       -> eval_domain_term unfold_locations dom (UM, env, pc)
            |   QuantTerm' (q_kind, v, t_set, t_cond) -> eval_quant_term unfold_locations (q_kind, v, t_set, t_cond) (UM, env, pc)
            |   UnfoldedTerm' ((f, xs), M) -> eval_unfolded_term unfold_locations ((f, xs), M) (UM, env, pc)
        if !trace > 1 then 
            level := !level - 1
            fprintf stderr "%s-> %s\n" (spaces()) (indent (pp_term t_result))
        t_result

    and eval_bool_term (unfold_locations : bool) t (UM, env, pc) =
        // specialized version for boolean terms, possibly calling SMT solver
        // only to be called for terms known to be boolean
        let t_eval = eval_term unfold_locations t (UM, env, pc)
        match get_term' t_eval with
        |   Value' (BOOL _) ->
                t_eval
        |   _ -> // (* optionally *) if Set.contains t_eval pc then TRUE else if Set.contains (s_not t_eval) pc then FALSE else
                smt_eval_formula t_eval eng (UM, env, pc)

    let t_result =
        match get_type' (get_term_type t) with
        |   Boolean' -> eval_bool_term unfold_locations t (UM, env, pc)
        |   _ -> eval_term unfold_locations t (UM, env, pc)


    t_result

and s_eval_term eng = s_eval_term_ eng false
and s_eval_term_with_unfolding eng = s_eval_term_ eng true

//--------------------------------------------------------------------

and eval_rule (eng : ENGINE) (R : RULE) (UM : UPDATE_MAP, env : ENV, pc : PATH_COND) : RULE =
    let Value, Initial, CondTerm, AppTerm, CondRule, UpdateRule, S_Updates = Value eng, Initial eng, CondTerm eng, AppTerm eng, CondRule eng, UpdateRule eng, S_Updates eng
    let ParRule, SeqRule, IterRule, UnfoldedRule, skipRule = ParRule eng, SeqRule eng, IterRule eng, UnfoldedRule eng, skipRule eng
    let s_equals, s_eval_term, s_eval_term_with_unfolding, eval_rule = s_equals eng, s_eval_term eng, s_eval_term_with_unfolding eng, eval_rule eng
    let get_term_type, get_type', get_term', get_rule', get_s_update_set, get_s_update_set', s_update_set_union, s_update_set_empty =
        get_term_type eng, get_type' eng, get_term' eng, get_rule' eng, get_s_update_set eng, get_s_update_set' eng, s_update_set_union eng, s_update_set_empty eng
    let rule_to_string, term_to_string, pp_rule = rule_to_string eng, term_to_string eng, pp_rule eng

    if !trace > 1 then
        fprintf stderr "%s----------------------\n%seval_rule %s\n%s\n\n" (spaces()) (spaces()) (show_s_update_map eng UM) (indent (pp_rule R))
        level := !level + 1

    let rec eval_rule_with_ext_path_cond (G : TERM) (R : RULE) (UM : UPDATE_MAP, env : ENV, pc : PATH_COND) =
        with_extended_path_cond eng G (fun R eng -> eval_rule R) R (UM, env, pc)

    and eval_rule_with_asgn_added_to_path_cond ((f, xs : VALUE list), t_rhs : TERM) (R : RULE) (UM : UPDATE_MAP, env : ENV, pc : PATH_COND) =
        with_asgn_added_to_path_cond eng ((f, xs), t_rhs) (fun R eng -> eval_rule R) R (UM, env, pc)

    and eval_update_rule ((f_lhs, ts_lhs), t_rhs) (UM : UPDATE_MAP, env : ENV, pc : PATH_COND) : RULE =
        if !trace > 0 then fprintf stderr "eval_update_rule: %s\n" (rule_to_string (UpdateRule ((f_lhs, ts_lhs), t_rhs)))
        let ts_lhs =            // unpack single tuple (t_1, ..., t_n) into arguments t_1, ..., t_n, if needed
            match ts_lhs with
            | [t] ->
                match get_type' (get_term_type t) with
                |   Prod' _ ->  // single argument is of product type, i.e. a tuple => try to extract arguments from tuple
                    match get_term' (s_eval_term t (UM, env, pc)) with
                    |   TupleTerm' ts' -> ts'
                    |   Value' (TUPLE ts') -> ts' >>| Value
                    |   _ -> failwith (sprintf "eval_update_rule: cannot extract arguments of '%s' from term '%s', which is of product type (i.e. a tuple)" (fct_name eng f_lhs) (term_to_string t))
                |   _ -> ts_lhs     // single argument is not expected to be a tuple => continue normally
            | _ -> ts_lhs
        let t_rhs = s_eval_term t_rhs (UM, env, pc)
        match get_term' t_rhs with
        |   CondTerm' (G, t1, t2) ->
                CondRule (G, UpdateRule ((f_lhs, ts_lhs), t1), UpdateRule ((f_lhs, ts_lhs), t2))
        |   UnfoldedTerm' ((f, xs), M) ->
                UnfoldedRule ((f, xs), Map.map (fun _ t_i -> UpdateRule ((f_lhs, ts_lhs), t_i)) M)
        |   _ ->
            let rec F ts_initial (ts_past_rev : TERM list, xs_past_opt_rev : VALUE list option) (ts: TERM list) (UM, env, pc) : RULE =
                let F_reiterate = F
                let F = F ts_initial
                match ts with
                |   (t1 :: ts_fut) ->
                    match get_term' t1 with
                    |   CondTerm' (G1, t11, t12) ->
                            CondRule (G1, F (ts_past_rev, xs_past_opt_rev) (t11 :: ts_fut) (UM, env, pc), F (ts_past_rev, xs_past_opt_rev) (t12 :: ts_fut) (UM, env, pc))
                    |   UnfoldedTerm' ((f, xs), M) ->
                            UnfoldedRule ((f, xs), Map.map (fun _ t_i -> F (ts_past_rev, xs_past_opt_rev) (t_i :: ts_fut) (UM, env, pc)) M)
                    |   _ ->
                        let t1 = s_eval_term_with_unfolding t1 (UM, env, pc)
                        match get_term' t1 with
                        |   Value' x1     -> F (t1 :: ts_past_rev, Option.map (fun xs -> x1 :: xs) xs_past_opt_rev) ts_fut (UM, env, pc)
                        |   Initial' _    -> F (t1 :: ts_past_rev, None) ts_fut (UM, env, pc)
                        |   CondTerm' _   -> F (ts_past_rev, xs_past_opt_rev) (t1 :: ts_fut) (UM, env, pc)      // reiterate 'lifting' of conditional, if needed, until no conditional left
                        |   UnfoldedTerm' _  -> F (ts_past_rev, xs_past_opt_rev) (t1 :: ts_fut) (UM, env, pc)      // reiterate 'lifting' of unfolded term, if needed, until no unfolded term left
                        |   AppTerm' _    -> F (t1 :: ts_past_rev, None) ts_fut (UM, env, pc)
                        |   TupleTerm' _  -> F (t1 :: ts_past_rev, None) ts_fut (UM, env, pc)
                        |   LetTerm' _    -> failwith "Engine.eval_update_rule: LetTerm should not occur here"
                        |   VarTerm' _    -> failwith "Engine.eval_update_rule: VarTerm should not occur here"
                        |   DomainTerm' _ -> failwith "Engine.eval_update_rule: DomainTerm should not occur here"
                        |   QuantTerm' _  -> failwith "Engine.eval_update_rule: QuantTerm should not occur here"
                |   [] ->
                    let ts_eval = List.rev ts_past_rev
                    let xs_opt_eval = Option.map List.rev xs_past_opt_rev
                    match xs_opt_eval with
                    |   Some xs ->
                            S_Updates (get_s_update_set (Set.singleton ((f_lhs, xs), s_eval_term t_rhs (UM, env, pc))))
                    |   None ->
                            if AppTerm (f_lhs, ts_eval) <> AppTerm (f_lhs, ts_initial) then
                                // fixed point is not reached yet: try reducing further before failing
                                F_reiterate ts_eval ([], Some []) ts_eval (UM, env, pc)
                            else
                                failwith (sprintf "Engine.eval_update_rule: arguments of controlled function '%s' must be fully evaluable for unambiguous determination of a location\n('%s' found instead)" (fct_name eng f_lhs) (term_to_string (AppTerm (f_lhs, ts_eval))))
            F ts_lhs ([], Some []) ts_lhs (UM, env, pc)

    and eval_cond_rule (G, R1, R2) (UM, env, pc) = 
        let G = if always_unfold_guards then s_eval_term_with_unfolding G (UM, env, pc) else s_eval_term G (UM, env, pc)
        match get_term' G with
        |   Value' (BOOL true)  -> eval_rule R1 (UM, env, pc)
        |   Value' (BOOL false) -> eval_rule R2 (UM, env, pc)
        |   CondTerm' (G', G1, G2) ->
                if get_type' (get_term_type G1) <> Boolean' || get_type' (get_term_type G2) <> Boolean'
                then failwith (sprintf "Engine.eval_cond_rule: '%s' and '%s' must be boolean terms" (term_to_string G1) (term_to_string G2))
                else eval_rule (CondRule (G', CondRule (G1, R1, R2), CondRule (G2, R1, R2))) (UM, env, pc)
        |   UnfoldedTerm' ((f, xs), M) ->
                eval_rule (UnfoldedRule ((f, xs), Map.map (fun _ R_i -> CondRule (R_i, R1, R2)) M)) (UM, env, pc)
        |   _ ->    let R1' = eval_rule_with_ext_path_cond G             R1 (UM, env, pc)
                    let R2' = eval_rule_with_ext_path_cond (s_not eng G) R2 (UM, env, pc)
                    if R1' = R2' then R1' else CondRule (G, R1', R2')

    and eval_unfolded_rule ((fct_id : FCT_ID, xs : VALUE list), cases_M : Map<VALUE, RULE>) (UM : UPDATE_MAP, env : ENV, (pc as (C, pc_M)) : PATH_COND) : RULE =
        let iterate_through_cases f_xs =
            let eq x = s_equals (f_xs, Value x)
            let rec F cases_list acc =
                match cases_list with
                |   [] -> acc
                |   (x_i, R_i) :: rest ->
                        let eq_x_i_eval = s_eval_term (eq x_i) (UM, env, pc) 
                        match get_term' eq_x_i_eval with
                        |   Value' (BOOL true)  -> [(x_i , eval_rule_with_asgn_added_to_path_cond ((fct_id, xs), Value x_i) R_i (UM, env, pc))]
                        |   Value' (BOOL false) -> F rest acc
                        |   _ -> F rest ((x_i, eval_rule_with_asgn_added_to_path_cond ((fct_id, xs), Value x_i) R_i (UM, env, pc)) :: acc)
            let new_cases_list = F (Map.toList cases_M) []
            match new_cases_list with
            |   [] -> failwith (sprintf "Engine.eval_unfolded_rule: value of term '%s' is outside the expected range" (term_to_string f_xs))
            |   [(x_1, R_1)] -> R_1
            |   (x_1, R_1) :: other_cases ->
                    let all_equal = List.forall (fun (_, R_i) -> R_i = R_1) other_cases           // !!!! use better equality check ?
                    if all_equal then R_1 else UnfoldedRule ((fct_id, xs), Map.ofList new_cases_list)
        match pc_M |> Map.tryFind fct_id |> Option.bind (Map.tryFind xs) with
        |   Some f_xs_eval ->
            match get_term' f_xs_eval with
            |   Value' x_i ->
                match cases_M |> Map.tryFind x_i with
                |   Some t_i -> eval_rule t_i (UM, env, pc)    // no need of eval_rule_with_asgn_added_to_path_cond, because path condition already contains the assignment
                |   None -> failwith (sprintf "Engine.eval_unfolded_rule: value '%s' of term '%s' is outside the expected range" (value_to_string x_i) (term_to_string f_xs_eval))
            |   _ -> iterate_through_cases f_xs_eval
        |   None -> iterate_through_cases (Initial (fct_id, xs))

    and eval_par_rule Rs (UM, env, pc) =
        match Rs with
        |   []          -> S_Updates s_update_set_empty
        |   [R1]        -> eval_rule R1 (UM, env, pc)
        |   R1 :: Rs    -> List.fold (fun R1 R2 -> eval_binary_par_rule R1 R2 (UM, env, pc)) R1 Rs

    and eval_binary_par_rule R1 R2 (UM, env, pc) : RULE =
        let R1_eval = eval_rule R1 (UM, env, pc)
        match get_rule' R1_eval with
        |   S_Updates' U1 ->
                let R2_eval = eval_rule R2 (UM, env, pc)
                match get_rule' R2_eval with
                |   S_Updates' U2 ->
                        S_Updates (s_update_set_union U1 U2)
                |   CondRule' (G2, R21, R22) ->
                        eval_rule (CondRule (G2, ParRule [ S_Updates U1; R21 ], ParRule [ S_Updates U1; R22 ])) (UM, env, pc)
                |   UnfoldedRule' ((f, xs), M) ->
                        eval_rule (UnfoldedRule ((f, xs), Map.map (fun _ R2_i -> ParRule [ S_Updates U1; R2_i ]) M)) (UM, env, pc)
                |   _ -> failwith (sprintf "eval_binary_par_rule: %s" (rule_to_string R2_eval))
        |   CondRule' (G1, R11, R12) ->
                eval_rule (CondRule (G1, ParRule [ R11; R2 ], ParRule [ R12; R2 ])) (UM, env, pc)
        |   UnfoldedRule' ((f, xs), M) ->
                eval_rule (UnfoldedRule ((f, xs), Map.map (fun _ R1_i -> ParRule [ R1_i; R2 ]) M)) (UM, env, pc)
        |   _ -> failwith (sprintf "eval_binary_par_rule: %s" (rule_to_string R1_eval))

    and eval_seq_rule Rs (UM, env, pc) =
        match Rs with
        |   []          -> S_Updates s_update_set_empty
        |   [R1]        -> eval_rule R1 (UM, env, pc)
        |   R1 :: Rs    -> List.fold (fun R1 R2 -> eval_binary_seq_rule R1 R2 (UM, env, pc)) R1 Rs

    and eval_binary_seq_rule R1 R2 (UM, env, pc): RULE = 
        let R1_eval = eval_rule R1 (UM, env, pc)
        match get_rule' R1_eval with
        |   S_Updates' U1 ->
                let S' =
                    try sequel_s_state eng UM (get_s_update_set' U1)
                    with Error (_, _, InconsistentUpdates (C, _, u1, u2, _)) ->
                            raise (Error (eng, "eval_rule.eval_binary_seq_rule",
                                InconsistentUpdates (C, Some (List.ofSeq (fst pc)), u1, u2, Some (get_s_update_set' U1))))
                let R2_eval = eval_rule R2 (S', env, pc)
                match get_rule' R2_eval with
                |   S_Updates' U2 ->
                        S_Updates (s_update_set_seq_merge_2 eng U1 U2)
                |   CondRule' (G2, R21, R22) ->
                        eval_rule (CondRule (G2, SeqRule [ S_Updates U1; R21 ], SeqRule [ S_Updates U1; R22 ])) (UM, env, pc)
                |   UnfoldedRule' ((f, xs), M) ->
                        eval_rule (UnfoldedRule ((f, xs), Map.map (fun _ R2_i -> SeqRule [ S_Updates U1; R2_i ]) M)) (UM, env, pc)
                |   _ -> failwith (sprintf "eval_binary_seq_rule: %s" (rule_to_string R2_eval))
        |   CondRule' (G1, R11, R12) ->
                eval_rule (CondRule (G1, SeqRule [ R11; R2 ], SeqRule [ R12; R2 ])) (UM, env, pc)
        |   UnfoldedRule' ((f, xs), M) ->
                eval_rule (UnfoldedRule ((f, xs), Map.map (fun _ R1_i -> SeqRule [ R1_i; R2 ]) M)) (UM, env, pc)
        |   _ -> failwith (sprintf "eval_binary_seq_rule: %s" (rule_to_string R1_eval))

    and eval_iter_rule R (UM, env, pc) =
        match get_rule' (eval_rule R (UM, env, pc)) with
        |   S_Updates' U ->
                if s_update_set_is_empty eng U
                then S_Updates s_update_set_empty
                else eval_rule (SeqRule [ S_Updates U; IterRule R ]) (UM, env, pc)
        |   CondRule' (G, R1, R2) ->
                //eval_rule (SeqRule [ CondRule (G, R1, R2); IterRule R ]) (UM, env, pc)
                eval_rule (CondRule (G, SeqRule [R1; IterRule R], SeqRule [R2; IterRule R])) (UM, env, pc)
        |   UnfoldedRule' ((f, xs), M) ->
                eval_rule (UnfoldedRule ((f, xs), Map.map (fun _ R_i -> SeqRule [ R_i; IterRule R ]) M)) (UM, env, pc)
        |   R' -> failwith (sprintf "eval_iter_rule - R'' = %s" (rule_to_string (get_rule eng R')))

    and eval_let_rule (v, t, R) (UM, env, pc) =
        let t' = s_eval_term t (UM, env, pc)
        let R' = eval_rule R (UM, add_binding env (v, t'), pc)
        R'

    and eval_forall_rule (v, ts, G, R) (UM, env, pc) =
        match get_term' (s_eval_term ts (UM, env, pc)) with
        |   Value' (SET (_, xs)) ->
                let eval_instance x =
                    let env' = let t_x = Value x in add_binding env (v, t_x)
                    CondRule (s_eval_term G (UM, env', pc), eval_rule R (UM, env', pc), skipRule)
                let Rs = List.map (fun x -> eval_instance x) (Set.toList xs)
                eval_rule (ParRule Rs) (UM, env, pc)
        |   x -> failwith (sprintf "eval_forall_rule: not a set (%A): %A v" ts x)

    and eval_macro_rule_call (r, args) (UM, env, pc) : RULE =
        let rname = get_rule_name eng r
        let sign_rule_type = Signature.rule_type_as_fct_type rname (get_signature eng)
        let convert_to_sign_types tys = List.map (fun ty -> to_signature_type eng ty) tys 
        let args_types = convert_to_sign_types (args >>| get_term_type) >>| Signature.main_type_of
        let sign_rule_type = (fst sign_rule_type >>| Signature.main_type_of, snd sign_rule_type |> Signature.main_type_of)
        match args_types with
        |   [Signature.Prod tys] ->
                // single tuple arg (x_1, ..., x_n) is equivalent to multiple args x_1, ..., x_n
                try Signature.match_fct_type rname tys [sign_rule_type] |> ignore
                with _ -> raise (Error (eng, "eval_macro_rule_call", RuleCallTypeMismatch (rname, tys >>| convert_type eng, fst sign_rule_type >>| convert_type eng)))
                match get_term' (s_eval_term (List.head args) (UM, env, pc)) with
                |   TupleTerm' ts     -> eval_macro_rule_call (r, ts) (UM, env, pc)    // unpack tuple argument
                |   Value' (TUPLE xs) -> eval_macro_rule_call (r, xs >>| Value) (UM, env, pc)    // unpack tuple argument
                |   _ -> failwith (sprintf "eval_macro_rule_call: expected tuple as single argument, got '%s'" (term_to_string (List.head args)))
        |   _ ->
                // normal case: one (non-tuple) arguments, or n arguments with n != 1
                try Signature.match_fct_type rname args_types [sign_rule_type] |> ignore
                with _ -> raise (Error (eng, "eval_macro_rule_call", RuleCallTypeMismatch (rname, args_types >>| convert_type eng, fst sign_rule_type >>| convert_type eng)))
                let (formals, body) =
                    match get_rule_def eng r with
                    |   Some (formals, body) -> (formals, body)
                    |   None -> failwith (sprintf "eval_macro_rule_call: macro rule '%s' not defined" (get_rule_name eng r))
                let env' =
                    List.fold2 (fun env_ formal arg -> add_binding env_ (formal, s_eval_term arg (UM, env, pc))) env formals args
                eval_rule body (UM, env', pc)
        
 
    and eval_rule R (UM, env, pc) =
        match get_rule' R with
        |   UpdateRule' ((f, ts), t) -> eval_update_rule ((f, ts), t) (UM, env, pc)
        |   CondRule' (G, R1, R2)    -> eval_cond_rule (G, R1, R2) (UM, env, pc)
        |   ParRule' Rs              -> eval_par_rule Rs (UM, env, pc)
        |   SeqRule' Rs              -> eval_seq_rule Rs (UM, env, pc)
        |   IterRule' R              -> eval_iter_rule R (UM, env, pc)
        |   LetRule' (v, t, R)       -> eval_let_rule (v, t, R) (UM, env, pc) 
        |   ForallRule' (v, t, G, R) -> eval_forall_rule (v, t, G, R) (UM, env, pc) 
        |   MacroRuleCall' (r, args) -> eval_macro_rule_call (r, args) (UM, env, pc)
        |   UnfoldedRule' ((f, xs), M)  -> eval_unfolded_rule ((f, xs), M) (UM, env, pc)
        |   S_Updates' S             -> R

    let R_eval = eval_rule R (UM, env, pc)

    if !trace > 1 then
        level := !level - 1
        fprintf stderr "%seval_rule result = \n%s\n%s----------------------\n" (spaces()) (indent (pp_rule R)) (spaces())

    R_eval


//--------------------------------------------------------------------
// convert partially evaluated terms and rules to regular ones

let reconvert_unfolded (CondTermOrRule : ENGINE -> TERM * 'a * 'a -> 'a) eng ((f, xs), M) =
    let elems = M |> Map.toList |> List.rev
    let _, t_n = List.head elems
    let f_xs_term = AppTerm eng (f, xs >>| Value eng)
    List.fold
        (fun acc (x_i, t_i) -> CondTermOrRule eng (s_equals eng (f_xs_term, Value eng x_i), t_i, acc))
        t_n    // no need to test (f_xs) = x_n, as this is the last remaining case
        (List.tail elems)

let rec reconvert_value (eng : ENGINE) x =
    match x with
    |   UNDEF    -> Value eng x
    |   BOOL b   -> Value eng x
    |   INT i    -> Value eng x
    |   STRING s -> Value eng x
    |   SET (_, fs) -> //AppTerm (FctName "asSet", ?????)
                    failwith "reconvert_value: SET not implemented yet"
    |   CELL (tag, args) -> AppTerm eng (get_fct_id eng tag, args >>| reconvert_value eng)
    |   TUPLE ts -> TupleTerm eng (ts >>| reconvert_value eng)

let reconvert_term (eng : ENGINE) t =
    term_induction eng (fun x -> x) {
        Value      = fun x -> reconvert_value eng x;
        Initial    = fun (f, xs) -> AppTerm eng (f, xs >>| Value eng);
        AppTerm    = AppTerm eng;
        CondTerm   = CondTerm eng;
        TupleTerm  = TupleTerm eng;
        VarTerm    = VarTerm eng;
        QuantTerm  = QuantTerm eng;
        LetTerm    = LetTerm eng;
        DomainTerm = DomainTerm eng;
        UnfoldedTerm  = reconvert_unfolded CondTerm eng;
    } t
let reconvert_rule (eng : ENGINE) R = 
    rule_induction eng (reconvert_term eng) {
        UpdateRule = UpdateRule eng;
        CondRule   = CondRule eng;
        ParRule    = ParRule eng;
        SeqRule    = SeqRule eng;
        IterRule   = IterRule eng;
        LetRule    = LetRule eng;
        MacroRuleCall = MacroRuleCall eng;
        ForallRule = ForallRule eng;
        S_Updates  = fun upds -> ParRule eng (List.map (fun ((f, xs), t_rhs) -> UpdateRule eng ((f, xs >>| Value eng), reconvert_term eng t_rhs)) (s_update_set_to_list eng upds))
        UnfoldedRule  = reconvert_unfolded CondRule eng;
    } R

//--------------------------------------------------------------------

let count_s_updates eng = rule_induction eng (fun _ -> ()) {
    S_Updates = fun _ -> 1;
    CondRule  = fun (_, R1, R2) -> R1 + R2;
    UnfoldedRule = fun ((f, xs), M) -> Map.toList M >>| snd |> List.sum;
    UpdateRule = fun _ -> failwith "count_s_updates: there should be no UpdateRule here";
    ParRule   = fun _  -> failwith "count_s_updates: there should be no ParRule here";
    SeqRule   = fun _  -> failwith "count_s_updates: there should be no SeqRule here";
    IterRule  = fun _  -> failwith "count_s_updates: there should be no IterRule here";
    LetRule   = fun _  -> failwith "count_s_updates: there should be no LetRule here";
    MacroRuleCall = fun _ -> failwith "count_s_updates: there should be no MacroRuleCall here";
    ForallRule = fun _ -> failwith "count_s_updates: there should be no ForallRule here";
}

//--------------------------------------------------------------------

let name_size name = 1

let term_size eng =
    term_induction eng name_size {
        Value = fun _ -> 1;
        AppTerm = fun (f, ts : int list) -> 1 + f + List.sum ts;
        TupleTerm = fun ts -> 1 + List.sum ts;
        CondTerm = fun (G, t1, t2) -> 1 + G + t1 + t2;
        Initial = fun _ -> 1;
        VarTerm = fun _ -> 1;
        QuantTerm = fun (q_kind, v, t_set, t_cond) -> 1 + t_set + t_cond;
        LetTerm = fun (v, t1, t2) -> 1 + t1 + t2;
        DomainTerm = fun _ -> 1;
        UnfoldedTerm = fun ((f, xs), M) -> 1 + f + List.sum (Map.toList M >>| snd)
    }

let rule_size eng =
    rule_induction eng (term_size eng) {
        S_Updates = fun U -> Set.count (get_s_update_set' eng U);   // not relevant, but define somehow to allow printing for debugging
        UpdateRule = fun ((f, ts), t) -> 1 + 1 + List.sum ts + t;
        CondRule = fun (G, R1, R2) -> 1 + G + R1 + R2;
        ParRule = fun Rs -> 1 + List.sum Rs;
        SeqRule = fun Rs -> 1 + List.sum Rs;
        IterRule = fun R' -> 1 + R';
        LetRule = fun (_, t, R) -> 1 + t + R;
        ForallRule = fun (_, t_set, t_filter, R) -> 1 + t_set + t_filter + R;
        MacroRuleCall = fun (r, ts) -> 1 + 1 + List.sum ts;
        UnfoldedRule = fun ((f, xs), M) -> 1 + 1 + List.sum (Map.toList M >>| snd);
    }

//--------------------------------------------------------------------
// first element of pair returned is the number of S_Updates rules, i.e. paths in the decision tree

let collect_distinct_symbolic_update_sets eng = rule_induction eng (fun _ -> 0) {
    S_Updates = fun SUS -> Set.singleton SUS;
    CondRule  = fun (_, R1, R2) -> Set.union R1 R2;
    UnfoldedRule = fun ((f, xs), M) -> Map.toList M >>| snd |> Set.unionMany;
    UpdateRule = fun _ -> failwith "collect_distinct_symbolic_update_sets: there should be no UpdateRule here";
    ParRule   = fun _  -> failwith "collect_distinct_symbolic_update_sets: there should be no ParRule here";
    SeqRule   = fun _  -> failwith "collect_distinct_symbolic_update_sets: there should be no SeqRule here";
    IterRule  = fun _  -> failwith "collect_distinct_symbolic_update_sets: there should be no IterRule here";
    LetRule   = fun _  -> failwith "collect_distinct_symbolic_update_sets: there should be no LetRule here";
    MacroRuleCall = fun _ -> failwith "collect_distinct_symbolic_update_sets: there should be no MacroRuleCall here";
    ForallRule = fun _ -> failwith "collect_distinct_symbolic_update_sets: there should be no ForallRule here";
} 

let symbolic_execution (eng : ENGINE) (R_in : RULE) (steps : int) : int * int option * RULE =
    if (!trace > 2) then fprintf stderr "symbolic_execution\n"
    if (steps < 0) then failwith "Engine.symbolic_execution: number of steps must be >= 0"
    //  if (!trace > 2) then fprintf stderr "---\n%s\n---\n" (Signature.signature_to_string (signature_of C))
    let R_in_n_times = [ for _ in 1..steps -> R_in ]
    let R_in' = SeqRule eng (R_in_n_times @ [ skipRule eng ])      // this is to force the application of the symbolic update sets of R_in, thus identifying any inconsistent update sets
    let R_out = eval_rule eng R_in' (Map.empty, Map.empty, empty_path_cond)
    (count_s_updates eng R_out, Some (Set.count (collect_distinct_symbolic_update_sets eng R_out)), reconvert_rule eng R_out)

let symbolic_execution_for_invariant_checking (eng : ENGINE) (opt_steps : int option) (R_in : RULE) : unit =
    let Initial, Value, CondRule, UpdateRule, S_Updates = Initial eng, Value eng, CondRule eng, UpdateRule eng, S_Updates eng
    let ParRule, SeqRule, IterRule, skipRule = ParRule eng, SeqRule eng, IterRule eng, skipRule eng
    let s_not, s_equals, with_extended_path_cond = s_not eng, s_equals eng, with_extended_path_cond eng

    let eval_rule_with_asgn_added_to_path_cond ((f, xs : VALUE list), t_rhs : TERM) (R : RULE) (UM : UPDATE_MAP, env : ENV, pc : PATH_COND) =
        with_asgn_added_to_path_cond eng ((f, xs), t_rhs) (fun R eng -> eval_rule eng R) R (UM, env, pc)

    let proc = Process.GetCurrentProcess()
    let capture_cpu_time (proc : Process) =
        (proc.TotalProcessorTime, proc.UserProcessorTime, proc.PrivilegedProcessorTime)
    let measure_cpu_time (proc : Process) (cpu0, usr0, sys0) =
        let (cpu1, usr1, sys1) = capture_cpu_time proc
        ( (cpu1 - cpu0).TotalMilliseconds, (usr1 - usr0).TotalMilliseconds, (sys1 - sys0).TotalMilliseconds )
    let (cpu0, usr0, sys0) = capture_cpu_time proc
    if (!trace > 2) then fprintf stderr "symbolic_execution_for_invariant_checking\n"
    match opt_steps with
    |   Some n -> if n < 0 then failwith "Engine.symbolic_execution_for_invariant_checking: number of steps must be >= 0"
    |   None -> ()
    let UM0 = Map.empty
    let invs = Map.toList (invariants_of eng)
    let counters = ref Map.empty
    let reset_counters () = counters := Map.empty
    let update_counters f inv_id = counters := Map.change inv_id (function Some (m, v, u) -> Some (f (m, v, u)) | None -> Some (f (0, 0, 0))) (!counters)
    let print_counters i () =
        printf "\n--- S_%d summary:\n\n" i
        Map.map (fun inv_id (m, v, u) -> printf "'%s': met on %d paths / definitely violated on %d paths / possibly violated on %d paths\n" inv_id m v u) !counters |> ignore
        let (cpu, usr, sys) = measure_cpu_time proc (cpu0, usr0, sys0)
        print_time (cpu, usr, sys)
        |> ignore
    let rec traverse i conditions R (UM, env, pc) =
        let initial_state_conditions_to_reach_this_state ts =
            sprintf "- this path is taken when the following conditions hold in the initial state:\n%s"
                (String.concat "\n" (List.rev ts >>| fun t -> term_to_string eng (reconvert_term eng t)))
        let show_cumulative_updates sign updates =
            "- cumulative update set for this path:\n" ^
            String.concat "\n"
                (Set.toList updates >>| fun ((f, xs), t) ->
                    sprintf "%s%s := %s"
                        (fct_name eng f) (if List.isEmpty xs then "" else "("^(String.concat ", " (xs >>| value_to_string))^")")
                        (term_to_string sign t))
        let met inv_id =
            update_counters (function (m, v, u) -> (m + 1, v, u)) inv_id
            ""
        let possibly_violated inv_id conditions (updates : UPDATE_SET) t t' = 
            update_counters (function (m, v, u) -> (m, v, u + 1)) inv_id
            sprintf "\n!!! invariant '%s' possibly violated in S_%d:\n%s\n\n- in this state and path, it symbolically evaluates to:\n%s\n\n%s\n\n%s\n\n---------------\n"
                inv_id i (term_to_string eng t) (term_to_string eng t')
                (initial_state_conditions_to_reach_this_state conditions)
                (show_cumulative_updates eng updates)
        let definitely_violated inv_id conditions updates t t' =
            update_counters (function (m, v, u) -> (m, v + 1, u)) inv_id
            sprintf "\n!!! invariant '%s' definitely violated in S_%d:\n%s\n\n- in this state and path, it symbolically evaluates to:\n%s\n\n%s\n\n%s\n\n---------------\n"
                inv_id i (term_to_string eng t) (term_to_string eng t')
                (initial_state_conditions_to_reach_this_state conditions)
                (show_cumulative_updates eng updates)
        let check_invariants invs S0 conditions updates =
            let check_one (inv_id, t) =
                let t' = s_eval_term eng t (apply_s_update_set eng S0 updates, Map.empty, empty_path_cond)
                match get_term' eng (smt_eval_formula t' eng (apply_s_update_set eng S0 updates, Map.empty, empty_path_cond)) with
                |   Value' (BOOL true)  -> met inv_id
                |   Value' (BOOL false) -> definitely_violated inv_id conditions updates t t'
                |   _                   -> possibly_violated inv_id conditions updates t t'
            printf "%s" (String.concat "" (List.filter (fun s -> s <> "") (List.map check_one invs)))
        match get_rule' eng R with      // check invariants on all paths of state S' = S0 + R by traversing tree of R
        |   CondRule' (G, R1, R2) ->
                with_extended_path_cond G         (fun () eng (UM, env, pc) -> traverse i (G::conditions) R1 (UM, env, pc))       () (UM, env, pc)
                with_extended_path_cond (s_not G) (fun () eng (UM, env, pc) -> traverse i (s_not G::conditions) R2 (UM, env, pc)) () (UM, env, pc)
        |   UnfoldedRule' ((f, xs), M) ->
                Map.iter    (fun x_i R_i -> with_asgn_added_to_path_cond eng
                                                ((f, xs), Value x_i)
                                                (fun R eng -> traverse i (s_equals (Initial (f, xs), Value x_i) :: conditions) R_i) () (UM, env, pc))
                            M
        |   S_Updates' updates    ->
                check_invariants invs UM0 conditions (get_s_update_set' eng updates)
        |   R -> failwith (sprintf "symbolic_execution_for_invariant_checking: there should be no such rule here: %s\n" (rule_to_string eng (get_rule eng R)))
    let state_header i = printf "\n=== state S_%d =====================================\n" i
    let rec F R_acc R_in i =
        reset_counters ()
        state_header i
        traverse i [] R_acc  (UM0, Map.empty, empty_path_cond)
        print_counters i ()
        if (match opt_steps with Some n -> i < n | None -> true)
        then let R_acc = eval_rule eng (SeqRule ([ R_acc; R_in; skipRule ])) (UM0, Map.empty, empty_path_cond)
             F R_acc R_in (i+1)
    F (S_Updates (s_update_set_empty eng)) (SeqRule ([ R_in; skipRule ])) 0
    printf "\n=================================================\n"


//--------------------------------------------------------------------
// sequential run with symbolic state enumeration
(*
let symbolic_sequential_asm_run (eng : ENGINE) (R_in : RULE) (steps : int) : int * int option * RULE =
    if steps <= 0 then failwith "Engine.symbolic_sequential_asm_run: number of steps must be >= 1"
    let IMPLIES = get_fct_id eng "implies"

    let s_eval_term, eval_rule = s_eval_term eng, eval_rule eng
    let AppTerm, AND, OR, TRUE, FALSE = AppTerm eng, AND eng, OR eng, TRUE eng, FALSE eng

    let out_rule_explore_states (R : RULE) (starting_state as (UM0, pc0): S_UPDATE_SET * PATH_COND) (result : Map<S_UPDATE_SET, PATH_COND> ref) : unit =
        // this functions merge the paths P(S) leading to a same symbolic state S into one path p(S), with path condition of p(S) = disjunction of all path conditions in P(S)
        // R is expected to be in decision tree form, i.e. to consist of CondRule and S_Updates only
        let UM0 = s_update_set_to_s_update_map eng UM0
        let rec F (R : RULE) (UM, env, pc) =
            match get_rule' eng R with
            |   S_Updates' U ->
                    match Map.tryFind U !result with
                    |   None ->
                            let pc_conjunction = Set.fold (fun acc cond -> s_and eng (acc, cond)) TRUE pc
                            // fprintf stderr "path condition reduced to single formula: %s\n" (term_to_string eng pc_formula)
                            result := Map.add U (Set.singleton pc_conjunction) !result
                    |   Some pc_existing ->
                            if Set.count pc_existing <> 1 then
                                failwith (sprintf "out_rule_to_state_list: (existing) path condition as a set { %s } not expected here\n  (at this point the path condition should have been reduced to a single formula)" (Set.toList pc_existing >>| term_to_string eng |> String.concat ", "))
                            else
                                let pc_existing_formula = Set.toList pc_existing |> List.head
                                let pc_formula = Set.fold (fun acc cond -> s_and eng (acc, cond)) TRUE pc
                                //let pcs_disjunction = s_eval_term (AppTerm (OR, [pc_existing_formula; pc_formula])) (UM0, Map.empty, pc0)
                                let pcs_disjunction = s_or eng (pc_existing_formula, pc_formula)
                                result := Map.add U (Set.singleton pcs_disjunction) !result
            |   CondRule' (G, R1, R2) ->
                    F R1 (UM, env, Set.union pc (Set.singleton G))
                    F R2 (UM, env, Set.union pc (Set.singleton (s_not eng G)))
            |   _ -> failwith (sprintf "out_rule_to_state_list: unexpected rule %s" (rule_to_string eng R))
        F R (UM0, Map.empty, pc0)

    let rec execute_step (R : RULE) (starting_states : (S_UPDATE_SET * PATH_COND) list) : Map<S_UPDATE_SET, PATH_COND> =
        let result = ref (Map.empty : Map<S_UPDATE_SET, PATH_COND>)
        match starting_states with
        |   [] ->
            failwith "Engine.symbolic_sequential_asm_run.execute_step: no starting states"
        |   _ ->
            for UM, pc in starting_states do
                let R_out = eval_rule R (s_update_set_to_s_update_map eng UM, Map.empty, pc)
                //let pc_conjuction = Set.fold (fun acc cond -> s_eval_term (AppTerm (AND, [ acc; cond ])) (s_update_set_to_s_update_map eng UM, Map.empty, pc)) TRUE pc
                let pc_conjuction = Set.fold (fun acc cond -> s_and eng (acc, cond)) TRUE pc
                out_rule_explore_states R_out (UM, Set.singleton pc_conjuction) result
        !result

    let list_symbolic_states successor_states =
        fprintf stderr "\nsymbolic_sequential_asm_run: after %d step(s), %d successor symbolic states generated:\n" steps (Map.count successor_states)
        Map.iter (fun S pc ->
            fprintf stderr "- symbolic state with update set:\n"
            Set.iter (fun ((f, xs), t_rhs) ->
                fprintf stderr "    %s%s := %s\n"
                    (fct_name eng f) (if List.isEmpty xs then "" else "("^(String.concat ", " (xs >>| value_to_string))^")")
                    (term_to_string eng t_rhs)
            ) (get_s_update_set' eng S)
            fprintf stderr "  reached under path condition(s):\n"
            Set.iter (fun cond ->
                fprintf stderr "    %s\n\n" (term_to_string eng cond)
            ) pc
        ) successor_states

    if (!trace > 2) then fprintf stderr "symbolic_sequential_asm_run\n"
    if (steps <= 0) then failwith "Engine.symbolic_sequential_asm_run: number of steps must be >= 1"

    let initial_state = get_s_update_set eng Set.empty, (Set.empty : PATH_COND)
    
    let iterate1 n initial_state =
        let rec F n current_states =
            if n = 0 then current_states
            else
                let successor_states = execute_step R_in current_states
                F (n - 1) (Map.toList successor_states)
        Map.ofList (F n [ initial_state ])

    let make_cond_rule successor_states : RULE =
        let R_out_rule =
            Map.foldBack (fun S pc acc ->
                let pc_conjuction = Set.fold (fun acc cond -> s_and eng (acc, cond)) TRUE pc
                CondRule eng (pc_conjuction, S_Updates eng S, acc)
            ) successor_states (S_Updates eng (get_s_update_set eng Set.empty))
        R_out_rule

    let iterate2 (n : int) =
        let rec F R no_of_states_reached i =
            if i <= 0 then R, no_of_states_reached else
                let successor_states = execute_step (SeqRule eng [ R; R_in ]) [ initial_state ]
                let R_out = eval_rule (make_cond_rule successor_states) (Map.empty, Map.empty, Set.empty)
                fprintf stderr "\nAfter step %d: %d symbolic states reached, generated rule:\n%s\n" (steps - i + 1) (Map.count successor_states) (indent (pp_rule eng R_out))
                F R_out (Map.count successor_states)(i - 1)
        let R_out, no_of_states_reached = F (skipRule eng) 1 n
        fprintf stderr "*** FINISHED ***"
        R_out, no_of_states_reached

    let iteration_kind = 2          // 1 = iterate1, 2 = iterate2

    if iteration_kind = 1 then
        let states_after_n_steps = iterate1 steps initial_state
        let R_out = eval_rule (make_cond_rule states_after_n_steps) (Map.empty, Map.empty, Set.empty)
        list_symbolic_states states_after_n_steps
        count_s_updates eng R_out, Some (Map.count states_after_n_steps), reconvert_rule eng R_out
    else  // iteration_kind = 2
        let R_out, no_of_states_reached = iterate2 steps
        count_s_updates eng R_out, Some no_of_states_reached, reconvert_rule eng R_out
*)