main.py

#!/usr/bin/env python 
# -*- coding:UTF-8 -*-
# 
"""
main
"""
import sys, pprint,os,json,time, copy,re
from typing import Dict
from utils import autogenerator_python_prove_file,run_all_python_prove_file_in_dir_autogenerated,delete_all_files_in_dir_autogenerated
from GologProgramTree import action_args_declear_andlist_dict_define_in_GologTree_Nests_assgined_in_main_regression #   dict : 'hig_name(=xxx)' -> {'arg_1':'BlockType';'arg_6':'BlockType';......} 

def main():
    """
    main process:
    1. "Dict for Theorems which will be proved" write into jsonfiles in "./autogenerated/domain_steps_configJSON/{0}_{1}_config.json".format(domainname,whichStepToProve). whichStepToProve = 'I','G', Preconditions of actions,effects of actions
    2. path_of_template_py = "./autogenerated/domain_template/{0}_template.py".format(domainname)
    3. using "jsonfiles" and "path_of_template_py", function autogenerator_python_prove_file will generate goals of provefiles in "./autogenerated/{0}_*.py".format(domainname)
    """
    import argparse
    # PARSE ARGUMENTS
    args_parser = argparse.ArgumentParser(description='hig-low sound abstraction prove.')
    #args_parser.add_argument('path_qnp_file', help='Path to domain file (qnp) -- NOT OPTIONAL')
    args_parser.add_argument('-domainname', default = "blocks_clear", help='domainname for qnp/pddl/refinementmap/constraint files -- OPTIONAL FOR TEST & DEBUG.')
    args_parser.add_argument('-DEBUG', default = 'False', help='print DEBUG message or not -- OPTIONAL FOR TEST')
    args_parser.add_argument('-timeout_number', default = 10, help='the autogenerated prove file wait for timeout_number(s).if timeout,it will return unknown message and then please open the file and add some Necessary constraint message. -- OPTIONAL FOR PROVE')
    params = vars(args_parser.parse_args())
    domainname = params['domainname']
    # domainname = "blocks_clear" # default test demo
    # domainname = "gripper"
    # domainname = "onAB"
    # domainname = "logistic"
    # domainname = "getlast"
    # domainname = "findA"
    # domainname = "corner"
    
    if params['DEBUG'] == 'False':
        DEBUG = False
    else:
        DEBUG = True
    
    DEBUG = False
    
    timeout_number = params['timeout_number']

    domain  = "examples/{0}/{0}_d.txt".format(domainname)
    problem = "examples/{0}/{0}_p.txt".format(domainname)
    
    # ==========================================================
    # delete all files in dir autogenerated before
    # ==========================================================

    delete_all_files_in_dir_autogenerated()

    # ==========================================================
    # PDDL parser
    # ==========================================================
    from refinementMapParser import PDDL_RefinementMap_Parser
    from GologProgramTree import Nested_list2FOLExp
    from Regression import Regression

    parser = PDDL_RefinementMap_Parser()
    # region
    # print('---------------------------- scan_tokens(domain)')
    # pprint.pprint(parser.scan_tokens(domain))
    # print('---------------------------- scan_tokens(problem)')
    # pprint.pprint(parser.scan_tokens(problem))
    # print('---------------------------- Domain name + Actions')
    # endregion
    parser.parse_domain(domain)
    parser.parse_problem(problem)
    if DEBUG == True:
        print('Domain name: ' + parser.domain_name)
    # region    
    # print("types :",end = '')
    # print(parser.types)
    # print('Objects: ' + str(parser.objects)) 
    # print("ConsForSorts :",end = '')
    # print(parser.ConsForSorts) 
    # print("predicates :",end = '')
    # print(parser.predicates)
    # print("predicates_transitive_closure :",end = '')
    # print(parser.predicates_transitive_closure)
    # print("actions is:")
    if DEBUG == True:
        for act in parser.actions:
            print(act)
    # print('---------------------------- problem name + anyelse')
    # print('Problem name: ' + parser.problem_name)
    # print('State: ' + str(parser.state))
    # print('.goalstateNestList: ' + str(parser.goalstateNestList))
    # print('Positive goals: ' + str(parser.positive_goals))
    # print('Negative goals: ' + str(parser.negative_goals))
    # endregion
    
    # ==========================================================
    # RefinementMap parser
    # ==========================================================
    
    domainRefinementMapName = "refinementMap/{0}_RefinementMap.txt".format(domainname)
    parser.parser_refinementMap(domainRefinementMapName)
    # region    
    if DEBUG == True:
        print('---------------------------- RefinementMap ')
        print(parser.refinementMap_name)
    # print(parser.refinementMap_fluents)
    # print(parser.refinementMap_variables)
    
    # ==========================================================
    # QNP parser
    # ==========================================================

    from QNPparser import QNP_Parser
    qnpfile = "examples/{0}/{0}.qnp".format(domainname)
    qnp_parser = QNP_Parser(qnpfile)
    # region
    if DEBUG == True:
        print("-"*30,"qnp parser")
        print(qnp_parser.name)
    # print(qnp_parser.initstate)
    # print(qnp_parser.goalstate)
    # print(qnp_parser.stateRepresentation_variables)
    # print(qnp_parser.stateRepresentation_fluents)
    # print(qnp_parser.actionscount)
    # for eachaction in qnp_parser.actionlist:
    #     print(eachaction.name)
    #     print(eachaction.prestate)
    #     print(eachaction.effstate)
    # endregion

    # ==========================================================
    # Refinement Map process
    # ==========================================================

    refinementMap_Dict = dict()
    for each in parser.refinementMap_fluents:
        refinementMap_Dict[each[0][0]] = Nested_list2FOLExp().run(copy.deepcopy(each[1]))
    for each in parser.refinementMap_variables:
        refinementMap_Dict[each[0][0]] = Nested_list2FOLExp().run(copy.deepcopy(each[2]))
    if DEBUG == True:
        print("refinementMap_Dict is:")
        print(refinementMap_Dict)#{'H': 'Exists(x,(holding(x)))', 'n': 'Exists(x,(above(x,A)))'}
    # print(type(parser.refinementMap_actionsMap))
    if DEBUG == True:
        for eachactionmap in parser.refinementMap_actionsMap:
            print(eachactionmap) # Golog programs

    eachgolog_set_of_s_io = dict()# hig act name --> set for situation tree==>gennerate the regression order"poset""
    eachgolog_set_of_s_act = dict()
    for eachactionmap in parser.refinementMap_actionsMap:
        # print(eachactionmap.act_map_golog_dict)                            # {'putaside': <__main__.GologNode object}
        for hig_name,eachgolog in eachactionmap.act_map_golog_dict.items():  # only run one times because"higname --> GologTree with GologNode "
            if DEBUG == True:
                print('\nhig action \"'+ hig_name + '\" map to golog program:\n')
                print(type(eachgolog))  # <class 'refinementMapParser.GologNode'>
                print(eachgolog)
            eachgolog_set_of_s_act[hig_name] = eachgolog.s_act# set of tuple (situation,action)
            eachgolog_set_of_s_io[hig_name] = eachgolog.set_of_s_io # set of input/output situation combination
    
    from collections import defaultdict 
    def build_reverse_eachgolog_set_of_s_io_order_list(eachgolog_set_of_s_io):
        from topologicalSort import Graph
        reverse_eachgolog_set_of_s_io_order_list = dict()
        reverse_situation_tree = dict()
        each_situation_action_args = dict()
        for eachactionmap in parser.refinementMap_actionsMap:
            for hig_name,golog_tree in eachactionmap.act_map_golog_dict.items():  # only run one times because"higname --> GologTree with GologNode "
                each_situation_action_args[hig_name] = golog_tree.situation_action_args
                dict_situation_map_number = dict() # 's1'-->2, index 
                all_unique_str = set()
                for each in eachgolog_set_of_s_io[hig_name]:
                    all_unique_str.add(each[0])
                    all_unique_str.add(each[1])
                all_unique_list = list(all_unique_str)
                for index in range(0,len(all_unique_list)):
                    dict_situation_map_number[all_unique_list[index]] = index
                reverse_dict_situation_map_number = {v: k for k, v in dict_situation_map_number.items()} #  number ==map==> situation 
                g = Graph(len(all_unique_list))
                for each in eachgolog_set_of_s_io[hig_name] :# {(s,s1),(s,s2),...(sn,s_)}
                    g.add_edge(dict_situation_map_number[each[1]],dict_situation_map_number[each[0]])# reverse the poset arrow ,because regression need a invert order 
                reverse_eachgolog_set_of_s_io_order_list[hig_name] =  g.topological_sort()        #stack = []
                g_graph_str = defaultdict(list) 
                for key,value in g.graph.items():
                    templist_value = []
                    for each in value:
                        templist_value.append(reverse_dict_situation_map_number[each])
                    g_graph_str[reverse_dict_situation_map_number[key]] = templist_value
                reverse_situation_tree[hig_name] = g_graph_str
                for index in range(0,len(reverse_eachgolog_set_of_s_io_order_list[hig_name])):
                    reverse_eachgolog_set_of_s_io_order_list[hig_name][index] = all_unique_list[reverse_eachgolog_set_of_s_io_order_list[hig_name][index]] # 's*' = list[index],index convert to str
                
        return reverse_eachgolog_set_of_s_io_order_list,reverse_situation_tree,each_situation_action_args
    
    reverse_eachgolog_set_of_s_io_order_list,reverse_situation_tree,each_situation_action_args = build_reverse_eachgolog_set_of_s_io_order_list(eachgolog_set_of_s_io)
       
    # {'pickabove': ['s_', 's1', 's'], 'putaside': ['s_', 's1', 's2', 's']} {'Pick-at-source': ['s_', 's1', 's'], 'Drop-at-target': ['s_', 's1', 's'], 'Move': ['s_', 's1', 's'], 'Leave': ['s_', 's1', 's']}

    def write_json_config_file2theoremConfigJson(domainname,whichStepToProve,low_to_prove_for_this_step,hig_to_prove_for_this_step):
        """""Dict for Theorems which will be proved" write into jsonfiles in "./autogenerated/domain_steps_configJSON/{0}_{1}_config.json".format(domainname,whichStepToProve). whichStepToProve = 'I','G', Preconditions of actions,effects of actions
        If we do no write out and only use Dict() in python is OK, need not this file.Why we write out this json config file just for cheack whether the "low theorem" and "hig theorem" is true or false. 
        """
        json_file = "./autogenerated/domain_steps_configJSON/{0}_{1}_config.json".format(domainname,whichStepToProve) #whichStepToProve = 'I','G', Preconditions of actions,effects of actions

        # write
        obj = {
            "domain_name":domainname,
            "file_name":"./autogenerated/{0}_{1}.py".format(domainname,whichStepToProve),
            "LOW_THEOREM":low_to_prove_for_this_step,
            "HIG_THEOREM":hig_to_prove_for_this_step
        }

        with open(json_file, mode='w',encoding='utf-8') as fs:
            fs.write(json.dumps(obj,ensure_ascii=False,indent=1)) 
    
    if DEBUG == True:
        print("topological Sort reverse order for \'Regrassion\':")
        print(reverse_eachgolog_set_of_s_io_order_list)
            # topological Sort reverse order for 'Regrassion':
        print("reverse order for situation tree for Regrassion:")
        print(reverse_situation_tree)
            # reverse order for situation tree for Regrassion:
        print('each golog set of situation_action:')
        print(eachgolog_set_of_s_act)
            # each golog set of situation_action:
        print(each_situation_action_args)
        


    # pres/effs of actions:
    # ==========================================================
    # Regression
    # ==========================================================

    # declare object and sort for pre:
    regressionObj = Regression(domainname,parser,qnp_parser,reverse_eachgolog_set_of_s_io_order_list,reverse_situation_tree,eachgolog_set_of_s_act,each_situation_action_args) # input the pddl parser to auto generate SSA,Poss for each pddl.acts/pddl.predicates
    golobal_tree_mid_act_args_name2sort = regressionObj.golobal_tree_mid_act_args_name2sort # use this for the template_pre.py with middle situtation_action_args:sorts.
    # print(golobal_tree_mid_act_args_name2sort) 

    # >>>>>>>>>>>>>>>>>>>>>>>>>>>>>> pre of actions:
    def wrapper_predicate_tcfml(args_TypeInput_str,tcfml_name):
        tcfmlObj = parser.predicates_transitive_closure_fml[tcfml_name]
        args,fmlcnf = tcfmlObj.parameters,tcfmlObj.fmlcnf
        fml = Nested_list2FOLExp().run(copy.deepcopy(fmlcnf))
        defaultArgsStr = tcfmlObj.get_default_args_str()
        defaultArgslist = defaultArgsStr.split(',')
        args_TypeInputlist = args_TypeInput_str.split(',')
        counter = 0
        fml_without_tcfml = fml
        for d in defaultArgslist:
            fml_without_tcfml = fml_without_tcfml.replace(','+defaultArgslist[counter]+',',','+args_TypeInputlist[counter]+',')
            fml_without_tcfml = fml_without_tcfml.replace('('+defaultArgslist[counter]+',','('+args_TypeInputlist[counter]+',')
            counter = counter + 1
        return fml_without_tcfml

    def rerplace_predicate_tcfml_withcnf(fml_for_this_step):
        fml = fml_for_this_step
        if(parser.predicates_transitive_closure_fml != {}):
            for tcfml_name,tcfml_obj in parser.predicates_transitive_closure_fml.items():
                if tcfml_name in fml:
                    predicate_match_Obj_list = re.findall( r'' + tcfml_name + '\('+'([^()]*?)'+'\)', fml, re.M)
                    for real_args_TypeInput_str in predicate_match_Obj_list:
                        tcfml_origin = tcfml_name + '(' + real_args_TypeInput_str + ')'
                        changeto = wrapper_predicate_tcfml(real_args_TypeInput_str,tcfml_name)
                        fml = fml.replace(tcfml_origin,changeto)
        return fml

    for eachactionmap in parser.refinementMap_actionsMap:
        for hig_name,eachgolog in eachactionmap.act_map_golog_dict.items():  # only run one times because"higname --> GologTree with GologNode "
            if DEBUG == True:
                print('\nhig action \"'+ hig_name + '\" map to golog program:\n')
                print(eachgolog.dump_golog_tree_pre())
                print("after regression:")

            eachgolog_dump_golog_tree_pre = eachgolog.dump_golog_tree_pre()
            # 
            dump_golog_tree_pre_afterOnestep = regressionObj.one_step_regression_with_all_poss_ssa(eachgolog_dump_golog_tree_pre,hig_name,'s1')
            # 's_i'
            dump_golog_tree_pre_afterMultiplesteps = regressionObj.loop_regression_with_all_poss_ssa(eachgolog_dump_golog_tree_pre,hig_name)
            # print()
            low_to_prove_for_this_step = dump_golog_tree_pre_afterMultiplesteps
            if DEBUG == True:
                print(low_to_prove_for_this_step) 

            # (s_i)s ，s_i，’,s_i‘
            low_to_prove_for_this_step = low_to_prove_for_this_step.replace(',s_i)',')')
            low_to_prove_for_this_step = low_to_prove_for_this_step.replace('(s_i)','') # arm_empty(s_i) --> arm-empty
            if DEBUG == True:
                print("s_i：")
                print(low_to_prove_for_this_step)
            
            
            # print("\nqnp actions is:")
            def hig_action_pre(qnp_actions_dicts):
                hig_to_prove_for_this_step = 'And('
                for key,value in qnp_actions_dicts.items():
                    if value == 'False': # fluents
                        hig_to_prove_for_this_step += ('Not('+ refinementMap_Dict[key] +'),')
                    elif value == 'True':
                        hig_to_prove_for_this_step += (refinementMap_Dict[key]+',')
                    elif value == '=0': # fluents
                        hig_to_prove_for_this_step += ('Not('+ refinementMap_Dict[key] +'),')
                    elif value == '>0':
                        hig_to_prove_for_this_step += (refinementMap_Dict[key]+',')
                if hig_to_prove_for_this_step[-1] == ',':
                    hig_to_prove_for_this_step = hig_to_prove_for_this_step[:-1]
                hig_to_prove_for_this_step += ')' 
                return hig_to_prove_for_this_step
            
            hig_to_prove_for_this_step = ''
            for eachaction in qnp_parser.actionlist:
                if  eachaction.name.upper() == hig_name.upper(): # 'pickabove' in refinementmap.txt + 'pickabove' in *.qnp is OK.but please keep them the same name.
                    hig_to_prove_for_this_step = hig_action_pre(eachaction.prestate)
                    

            whichStepToProve = hig_name+'_pre'

            low_to_prove_for_this_step = rerplace_predicate_tcfml_withcnf(low_to_prove_for_this_step)
            hig_to_prove_for_this_step = rerplace_predicate_tcfml_withcnf(hig_to_prove_for_this_step)
            write_json_config_file2theoremConfigJson(domainname,whichStepToProve,low_to_prove_for_this_step,hig_to_prove_for_this_step)
    
    
    print("Refinement Mapping",'\n',refinementMap_Dict)
    for eachactionmap in parser.refinementMap_actionsMap:# print(eachactionmap.act_map_golog_dict)                            
        for hig_name,golog_root in eachactionmap.act_map_golog_dict.items():  # only run one times because"higname --> GologTree with GologNode "
            for eachaction in qnp_parser.actionlist:
                if eachaction.name == hig_name:
                    poss_pre = golog_root.dump_golog_tree_pre()
                    print('-'*30)
                    print(eachaction.name)
                    print("Action: ",poss_pre,"\n")
                    poss_pre = regressionObj.loop_regression_with_all_poss_ssa(poss_pre,hig_name)
                    poss_pre = poss_pre.replace(',s_i)',')')
                    poss_pre = poss_pre.replace('(s_i)','')
                    print("Poss formula after regression:",poss_pre,"\n\n\n")

    # >>>>>>>>>>>>>>>>>>>>>>>>>>>>>> eff of actions:
    # 1 
    regressionObj.generate_exists_and_universal_regression_map_dict()
    exists_regression_map_dict_file = "./autogenerated/{0}_exists_ssa.json".format(domainname)
    # read cotents in json file :
    exists_regression_map = {}
    with open(exists_regression_map_dict_file, mode='r') as fs:
        exists_regression_map = json.load(fs)
    # print(exists_regression_map)   
     
    # 2 
    univer_regression_map_dict_file = "./autogenerated/{0}_univer_ssa.json".format(domainname)
    univer_regression_map = {}
    with open(univer_regression_map_dict_file, mode='r') as fs:
        univer_regression_map = json.load(fs)
    # print(univer_regression_map)     # 

    def write_json_config_eff_fluent(domainname,hig_name,eff_fluent,Exists_Regression,Fluent_s_i,Univer_Regression,poss_pre):
        """""Dict for Theorems which will be proved" write into jsonfiles in "./autogenerated/domain_steps_configJSON/{0}_{1}_config.json".format(domainname,whichStepToProve). whichStepToProve = 'I','G', Preconditions of actions,effects of actions
        If we do no write out and only use Dict() in python is OK, need not this file.Why we write out this json config file just for cheack whether the "low theorem" and "hig theorem" is true or false. 
        """
        json_file = "./autogenerated/domain_steps_configJSON/{0}_{1}_eff_{2}_config.json".format(domainname,hig_name,eff_fluent) #
        # write
        obj = {
            "domain_name":domainname,
            "file_name":"./autogenerated/{2}_{0}_eff_{1}.py".format(hig_name,eff_fluent,domainname),
            "Exists_Regression":Exists_Regression,
            "Fluent_s_i":Fluent_s_i,
            "Univer_Regression":Univer_Regression,
            "poss_pre":poss_pre
        }
        with open(json_file, mode='w',encoding='utf-8') as fs:
            fs.write(json.dumps(obj,ensure_ascii=False,indent=1))
        # read cotents in json file for check:
   
    for eachactionmap in parser.refinementMap_actionsMap:# print(eachactionmap.act_map_golog_dict)                            
        for hig_name,golog_root in eachactionmap.act_map_golog_dict.items():  # only run one times because"higname --> GologTree with GologNode "

            def add_s_o_for_formula (formula):
                formula_with_s_o = formula
                for predicate,_ in parser.predicates.items(): # 
                    if predicate == formula:
                        formula_with_s_o = predicate + '(s_o)'
                    # 's_o'，
                    predicate_match_Obj_list = re.findall( r'' + predicate + '\('+'([^()]*?)'+'\)', formula, re.M)
                    if predicate_match_Obj_list == []:
                        continue
                    for each_predicate_args in predicate_match_Obj_list:
                        if each_predicate_args == '':
                            formula_with_s_o = formula_with_s_o.replace(predicate+'()',predicate+'(s_o)')
                        else: 
                            formula_with_s_o = formula_with_s_o.replace(predicate+'('+each_predicate_args+')',predicate+'('+each_predicate_args+',s_o)')
                return formula_with_s_o

            for eachaction in qnp_parser.actionlist:
                if eachaction.name == hig_name:
                    # 1.  
                    for each_hig_fluent_in_eff in qnp_parser.stateRepresentation_fluents: 
                        if each_hig_fluent_in_eff in eachaction.effstate:
                            poss_pre = golog_root.dump_golog_tree_pre()
                            poss_pre = regressionObj.loop_regression_with_all_poss_ssa(poss_pre,hig_name)
                            poss_pre = poss_pre.replace(',s_i)',')')
                            poss_pre = poss_pre.replace('(s_i)','')
                            
                            m_P_formula = refinementMap_Dict[each_hig_fluent_in_eff] 
                            m_P_formula_with_s_o = add_s_o_for_formula(m_P_formula) 
                            true_or_false = eachaction.effstate[each_hig_fluent_in_eff] 
                            
                            # ===============================
                            if true_or_false == 'True':# 
                                # 
                                formula_to_be_prove_exists = regressionObj.dump_regression_exists(m_P_formula_with_s_o,golog_root,hig_name) 
                                formula_to_be_prove_univer = regressionObj.dump_regression_universal(m_P_formula_with_s_o,golog_root,hig_name) 
                                formula_to_be_prove_exists = regressionObj.loop_regression_with_all_poss_ssa(formula_to_be_prove_exists,hig_name) 
                                formula_to_be_prove_univer = regressionObj.loop_regression_with_all_poss_ssa(formula_to_be_prove_univer,hig_name) 
                            else:# False
                                formula_to_be_prove_exists = regressionObj.dump_regression_exists('Not('+m_P_formula_with_s_o+')',golog_root,hig_name) 
                                formula_to_be_prove_univer = regressionObj.dump_regression_universal('Not('+m_P_formula_with_s_o+')',golog_root,hig_name) 
                                # 'Not('+
                                formula_to_be_prove_exists = regressionObj.loop_regression_with_all_poss_ssa(formula_to_be_prove_exists,hig_name) 
                                formula_to_be_prove_univer = regressionObj.loop_regression_with_all_poss_ssa(formula_to_be_prove_univer,hig_name) 
                            # 's_i'
                            formula_to_be_prove_exists = formula_to_be_prove_exists.replace(',s_i)',')')
                            formula_to_be_prove_exists = formula_to_be_prove_exists.replace('(s_i)','')
                            formula_to_be_prove_univer = formula_to_be_prove_univer.replace(',s_i)',')')
                            formula_to_be_prove_univer = formula_to_be_prove_univer.replace('(s_i)','')
                            if true_or_false == 'True':
                                write_json_config_eff_fluent(domainname,hig_name,each_hig_fluent_in_eff,formula_to_be_prove_exists,m_P_formula,formula_to_be_prove_univer,poss_pre)
                            else:#'False'
                                write_json_config_eff_fluent(domainname,hig_name,each_hig_fluent_in_eff,formula_to_be_prove_exists,'Not('+ m_P_formula + ')',formula_to_be_prove_univer,poss_pre)
                    
                    # 2.  
                    predicate_exists_ssa = exists_regression_map[hig_name] #  gologssa
                    predicate_univer_ssa = univer_regression_map[hig_name]
                    # print(refinementMap_Dict)#{'H': 'Exists(x,(holding(x)))', 'n': 'Exists(x,(above(x,A)))'}#  H   n ：
                    # start
                    for each_hig_func_number in qnp_parser.stateRepresentation_variables:#  ['b', 'c', 'g']
                        if each_hig_func_number in eachaction.effstate:
                            hig_num_prove_dict = {} # ， for each each_hig_func_number & hig_name
                            # 's_i'
                            hig_action_poss_fml = regressionObj.loop_regression_with_all_poss_ssa(golog_root.dump_golog_tree_pre(),hig_name)
                            hig_action_poss_fml = hig_action_poss_fml.replace(',s_i)',')')
                            hig_action_poss_fml = hig_action_poss_fml.replace('(s_i)','')
                            hig_num_prove_dict['hig_action_poss_fml'] = hig_action_poss_fml
                            for each_map_list in parser.refinementMap_variables:
                                hig_variables_name = each_map_list[0][0]
                                countinged_obj = each_map_list[1][0]
                                # print(countinged_obj)#'#x'
                                hig_num_prove_dict['countinged_obj'] = countinged_obj[1:]# 'x'
                                counting_mapped_formula = each_map_list[2] #the whole list() ['exists', ['?x', '-', 'Blocktype'], ['above', '?x', 'A']]
                                vars_declare_list = copy.deepcopy(counting_mapped_formula[1]) # like ['?x', '-', 'BlockType', '?y', '-', 'gripper']
                                vars_declare_map_sort = {}
                                vars_list = []
                                while(vars_declare_list):
                                    cur = vars_declare_list.pop(0)
                                    if cur[0] == '?':
                                        vars_list.append(cur[1:])
                                    if vars_declare_list != [] and cur == '-':
                                        # skip '-'
                                        the_right_sort = vars_declare_list.pop(0) # BlockType
                                        for var in vars_list:
                                            vars_declare_map_sort[var] = the_right_sort
                                        vars_list = [] # clear the recorded one
                                hig_num_prove_dict['predicate_args_list_vars_map_sort'] = vars_declare_map_sort
                                countinged_predicte_list = each_map_list[2][2]# ['above', '?x', 'A']
                                predicate_of_counting_term = countinged_predicte_list[0]
                                hig_num_prove_dict['predicate'] = predicate_of_counting_term
                                predicate_args_list = countinged_predicte_list[1:]
                                hig_num_prove_dict['predicate_args_list'] = predicate_args_list
                                if_is_transitive_closure = False
                                if predicate_of_counting_term in parser.predicates_transitive_closure.keys():
                                    if_is_transitive_closure = True
                                    hig_num_prove_dict['predicate_tc_base'] = parser.predicates_transitive_closure[predicate_of_counting_term]
                                    #  on = predicates_transitive_closure[above]
                                hig_num_prove_dict['if_is_transitive_closure'] = if_is_transitive_closure
                                if  hig_variables_name == each_hig_func_number:
                                    # prepare functions
                                    def p_fml_s_i (char_var,e_or_u = ''):
                                        nonlocal countinged_predicte_list
                                        nonlocal if_is_transitive_closure
                                        if if_is_transitive_closure == True:# it is transitive closure,need more process
                                            predicate = 'TC_p_fml_' + e_or_u
                                        else:# it is not transitive closure
                                            predicate = countinged_predicte_list[0]
                                        # 
                                        formula_with_s_i = predicate + '('
                                        pred_arg_str = ''
                                        for each in countinged_predicte_list[1:]:
                                            if each == '?'+countinged_obj[1:]:
                                                each = char_var# 'x'/'y'
                                            pred_arg_str += each + ','
                                        if pred_arg_str[-1] == ',':
                                            pred_arg_str = pred_arg_str[:-1]# delete the last ','
                                        formula_with_s_i += pred_arg_str + ')'  
                                        return formula_with_s_i
                                    def q_fml_s_o (char_var,e_or_u = ''):
                                        nonlocal countinged_predicte_list
                                        nonlocal if_is_transitive_closure
                                        if if_is_transitive_closure == True:# it is transitive closure,need more process
                                            predicate = 'TC_q_fml_' + e_or_u
                                        else:# it is not transitive closure
                                            predicate = countinged_predicte_list[0]
                                        formula_with_s_o = predicate + '('
                                        pred_arg_str = ''
                                        for each in countinged_predicte_list[1:]:
                                            if each == '?'+countinged_obj[1:]:
                                                each = char_var# 'x'/'y'
                                            pred_arg_str += each + ','
                                        if pred_arg_str[-1] == ',':
                                            pred_arg_str = pred_arg_str[:-1]# delete the last ','
                                        formula_with_s_o += pred_arg_str + ')'                                    
                                        return formula_with_s_o
                                    # print(hig_variables_name) # 'n'
                                    inc_or_dec = eachaction.effstate[each_hig_func_number] #'Dec'/'Inc'
                                    hig_num_prove_dict['eff_inc_or_dec'] = inc_or_dec
                                    # 'Dec': counting(countinged_obj,counting_mapped_formula,s_o) == counting(countinged_obj,counting_mapped_formula,s_i) - 1
                                    # 'Inc': counting(...,s_o) == counting(...,s_i) + 1

                                    # 1. ：
                                    if if_is_transitive_closure == True:
                                        tcargs_declare_sort_dict = {}
                                        tcargs_TypeInput_str = str()
                                        tcarg_number = 0
                                        for variable,TypeValues in parser.predicates[hig_num_prove_dict['predicate_tc_base']].items():
                                            if variable[0] == '?':
                                                tcarg_number = tcarg_number + 1
                                                tcargs_declare_sort_dict['tcarg_'+str(tcarg_number)] = TypeValues
                                                tcargs_TypeInput_str += ','+ 'tcarg_'+str(tcarg_number)
                                            else: # A,B ...
                                                tcarg_number = tcarg_number + 1
                                                tcargs_declare_sort_dict['tcarg_'+str(tcarg_number)] = TypeValues
                                                tcargs_TypeInput_str += ','+ variable
                                        tcargs_TypeInput_str = tcargs_TypeInput_str[1:]# ，
                                        hig_num_prove_dict['tcargs_declare_sort'] = tcargs_declare_sort_dict
                                        predicate_ssa_left = hig_num_prove_dict['predicate_tc_base'] + '(' + tcargs_TypeInput_str + ')' # on(tcarg_1,tcarg_2)
                                        hig_num_prove_dict['q_fml_u_and_e'] = predicate_ssa_left
                                        formula_to_be_prove_exists = regressionObj.dump_regression_exists(hig_num_prove_dict['predicate_tc_base'] + '(' + tcargs_TypeInput_str + ',s_o)',golog_root,hig_name) 
                                        formula_to_be_prove_univer = regressionObj.dump_regression_universal(hig_num_prove_dict['predicate_tc_base'] + '(' + tcargs_TypeInput_str + ',s_o)',golog_root,hig_name) 
                                        # 'Not('+
                                        formula_to_be_prove_exists = regressionObj.loop_regression_with_all_poss_ssa(formula_to_be_prove_exists,hig_name) # ，
                                        formula_to_be_prove_univer = regressionObj.loop_regression_with_all_poss_ssa(formula_to_be_prove_univer,hig_name) # ，
                                        # 's_i'
                                        formula_to_be_prove_exists = formula_to_be_prove_exists.replace(',s_i)',')')
                                        formula_to_be_prove_exists = formula_to_be_prove_exists.replace('(s_i)','')
                                        formula_to_be_prove_univer = formula_to_be_prove_univer.replace(',s_i)',')')
                                        formula_to_be_prove_univer = formula_to_be_prove_univer.replace('(s_i)','')
                                        # 
                                        hig_num_prove_dict['p_fml_e'] =  formula_to_be_prove_exists
                                        hig_num_prove_dict['p_fml_u']  = formula_to_be_prove_univer
                                        wanted_e = '' # sound but not incomplete proveing method formula str 
                                        wanted_u = ''
                                        if inc_or_dec == 'Dec':
                                            wanted_e = 'And('+ \
                                                'Exists(x,And('+p_fml_s_i('x','e')+',Not('+q_fml_s_o('x','e') +'))),'+\
                                                'ForAll(x,Implies(' +q_fml_s_o('x','e')+','+p_fml_s_i('x','e') +')),'+\
                                                'ForAll([x,y],Implies('+\
                                                    'And(' + \
                                                    p_fml_s_i('x','e')+',Not('+q_fml_s_o('x','e')+'),'+\
                                                    p_fml_s_i('y','e')+',Not('+q_fml_s_o('y','e')+')' +\
                                                    '),'+'x==y' +\
                                                    '))'\
                                                +')'
                                            wanted_u = 'And('+ \
                                                'Exists(x,And('+p_fml_s_i('x','u')+',Not('+q_fml_s_o('x','u') +'))),'+\
                                                'ForAll(x,Implies(' +q_fml_s_o('x','u')+','+p_fml_s_i('x','u') +')),'+\
                                                'ForAll([x,y],Implies('+\
                                                    'And(' + \
                                                    p_fml_s_i('x','u')+',Not('+q_fml_s_o('x','u')+'),'+\
                                                    p_fml_s_i('y','u')+',Not('+q_fml_s_o('y','u')+')' +\
                                                    '),'+'x==y' +\
                                                    '))'\
                                                +')'
                                        else:#'Inc'
                                            wanted_e = 'And('+ \
                                                'Exists(x,And('+q_fml_s_o('x','e')+',Not('+p_fml_s_i('x','e') +'))),'+\
                                                'ForAll(x,Implies(' +p_fml_s_i('x','e')+','+q_fml_s_o('x','e') +')),'+\
                                                'ForAll([x,y],Implies('+\
                                                    'And(' + \
                                                    q_fml_s_o('x','e')+',Not('+p_fml_s_i('x','e')+'),'+\
                                                    q_fml_s_o('y','e')+',Not('+p_fml_s_i('y','e')+')' +\
                                                    '),'+'x==y' +\
                                                    '))'\
                                                +')'
                                            wanted_u = 'And('+ \
                                                'Exists(x,And('+q_fml_s_o('x','u')+',Not('+p_fml_s_i('x','u') +'))),'+\
                                                'ForAll(x,Implies(' +p_fml_s_i('x','u')+','+q_fml_s_o('x','u') +')),'+\
                                                'ForAll([x,y],Implies('+\
                                                    'And(' + \
                                                    q_fml_s_o('x','u')+',Not('+p_fml_s_i('x','u')+'),'+\
                                                    q_fml_s_o('y','u')+',Not('+p_fml_s_i('y','u')+')' +\
                                                    '),'+'x==y' +\
                                                    '))'\
                                                +')'
                                            hig_num_prove_dict['wanted_e'] = wanted_e
                                            hig_num_prove_dict['wanted_u'] = wanted_u
                                        # print(inc_or_dec)
                                    
                                    # 2. 
                                    else :
                                        args_declare_sort_dict = {}
                                        args_TypeInput_str = str()
                                        copy_args_TypeInput_str = str()
                                        args_TypeInput_str_except_countinged_obj = str()  # 
                                        predicate_args_list = each_map_list[2][2]
                                        countinged_object = hig_num_prove_dict['countinged_obj'] # 'x'
                                        for each_arg in predicate_args_list[1:]:# pddl
                                        # for variable,TypeValues in parser.predicates[hig_num_prove_dict['predicate']].items():# pddl
                                            if each_arg[0] == '?':
                                                args_TypeInput_str += ','+ each_arg[1:]
                                                if hig_num_prove_dict['countinged_obj'] == each_arg[1:]:# 
                                                    copy_args_TypeInput_str += ','+ each_arg[1:]+'_copy' # xx_copy
                                                else :
                                                    copy_args_TypeInput_str += ','+ each_arg[1:] 
                                                    args_TypeInput_str_except_countinged_obj +=  each_arg[1:] + ','
                                            else: # A,B ...
                                                args_TypeInput_str += ','+ each_arg
                                                copy_args_TypeInput_str += ','+ each_arg
                                        args_TypeInput_str_except_countinged_obj = args_TypeInput_str_except_countinged_obj[:-1]
                                        args_TypeInput_str = args_TypeInput_str[1:]# ， pddl 'x,room'
                                        args_TypeInput_str_s_i = args_TypeInput_str + ',s_i' # 'x,A,s_i'
                                        args_TypeInput_str_s_o = args_TypeInput_str + ',s_o' # 'x,A,s_o'
                                        copy_args_TypeInput_str = copy_args_TypeInput_str[1:]
                                        copy_args_TypeInput_str_s_i = copy_args_TypeInput_str + ',s_i'# 'x_copy,A,s_i'
                                        copy_args_TypeInput_str_s_o = copy_args_TypeInput_str + ',s_o'# 'x_copy,A,s_o'
                                        predicate_name = hig_num_prove_dict['predicate']
                                        wanted_e = '' # sound but not incomplete proveing method formula str 
                                        wanted_u = ''
                                        
                                        ### formula for counting predicate(maybe a transitive closure formula)
                                        predicate_name_args_str_s_i = predicate_name+'('+args_TypeInput_str_s_i+')'
                                        predicate_name_args_str_s_o = predicate_name+'('+args_TypeInput_str_s_o+')'
                                        copy_predicate_name_args_str_s_i = predicate_name+'('+copy_args_TypeInput_str_s_i+')'
                                        copy_predicate_name_args_str_s_o = predicate_name+'('+copy_args_TypeInput_str_s_o+')'
                                        def wrapper_tcfml(args_TypeInput_str,predicate_name,si,so):
                                            tcfmlObj = parser.predicates_transitive_closure_fml[predicate_name]
                                            args,fmlcnf = tcfmlObj.parameters,tcfmlObj.fmlcnf
                                            fml,_ = Nested_list2FOLExp().run_s(copy.deepcopy(fmlcnf),si,so)
                                            defaultArgsStr = tcfmlObj.get_default_args_str()
                                            defaultArgslist = defaultArgsStr.split(',')
                                            args_TypeInputlist = args_TypeInput_str.split(',')
                                            counter = 0
                                            fml_without_tcfml = fml
                                            for d in defaultArgslist:
                                                fml_without_tcfml = fml_without_tcfml.replace(','+defaultArgslist[counter]+',',','+args_TypeInputlist[counter]+',')
                                                fml_without_tcfml = fml_without_tcfml.replace('('+defaultArgslist[counter]+',','('+args_TypeInputlist[counter]+',')
                                                counter = counter + 1
                                            return fml_without_tcfml
                                        # for "transitive closure formula"
                                        for name,tcfmlObj in parser.predicates_transitive_closure_fml.items():
                                            if(name == predicate_name):# place 'tcfml' by "fml", then do regression
                                                predicate_name_args_str_s_i = wrapper_tcfml(args_TypeInput_str,predicate_name,'s_i','s_o') 
                                                predicate_name_args_str_s_o = wrapper_tcfml(args_TypeInput_str,predicate_name,'s_o','s_o')
                                                copy_predicate_name_args_str_s_i = wrapper_tcfml(copy_args_TypeInput_str,predicate_name,'s_i','s_o') 
                                                copy_predicate_name_args_str_s_o = wrapper_tcfml(copy_args_TypeInput_str,predicate_name,'s_o','s_o')
                                        if args_TypeInput_str_except_countinged_obj == '':
                                            if inc_or_dec == 'Dec':
                                                need_to_proveed = 'And('+ \
                                                    'Exists('+countinged_object+',And('+predicate_name_args_str_s_i+',Not('+predicate_name_args_str_s_o+'))),'+\
                                                    'ForAll('+countinged_object+',Implies(' +predicate_name_args_str_s_o+','+predicate_name_args_str_s_i+')),'+\
                                                    'ForAll(['+countinged_object+','+countinged_object+'_copy],Implies('+\
                                                        'And(' + \
                                                        predicate_name_args_str_s_i+',Not('+predicate_name_args_str_s_o+'),'+\
                                                        copy_predicate_name_args_str_s_i+',Not('+copy_predicate_name_args_str_s_o+')' +\
                                                        '),'+countinged_object+'=='+countinged_object+'_copy' +\
                                                        '))'\
                                                    +')'
                                            else:#'Inc'
                                                need_to_proveed = 'And('+ \
                                                    'Exists('+countinged_object+',And('+predicate_name_args_str_s_o+',Not('+predicate_name_args_str_s_i+'))),'+\
                                                    'ForAll('+countinged_object+',Implies(' +predicate_name_args_str_s_i+','+predicate_name_args_str_s_o +')),'+\
                                                    'ForAll(['+countinged_object+','+countinged_object+'_copy],Implies('+\
                                                        'And(' + \
                                                        predicate_name_args_str_s_o+',Not('+predicate_name_args_str_s_i+'),'+\
                                                        copy_predicate_name_args_str_s_o+',Not('+copy_predicate_name_args_str_s_i+')' +\
                                                        '),'+''+countinged_object+'=='+countinged_object+'_copy' +\
                                                        '))'\
                                                    +')'
                                        else: # args_TypeInput_str_except_countinged_obj 
                                            if inc_or_dec == 'Dec':
                                                need_to_proveed = 'And('+ \
                                                'Exists('+'['+ args_TypeInput_str_except_countinged_obj + '],'+\
                                                    'Exists('+countinged_object+',And('+predicate_name_args_str_s_i+',Not('+predicate_name_args_str_s_o+')))'+\
                                                '),'+\
                                                'ForAll('+'['+ args_TypeInput_str_except_countinged_obj + '],'+\
                                                    'ForAll('+countinged_object+',Implies(' +predicate_name_args_str_s_o+','+predicate_name_args_str_s_i+'))'+\
                                                '),'+\
                                                'ForAll('+'['+ args_TypeInput_str_except_countinged_obj + '],'+\
                                                    'ForAll(['+countinged_object+','+countinged_object+'_copy],Implies('+\
                                                        'And(' + \
                                                        predicate_name_args_str_s_i+',Not('+predicate_name_args_str_s_o+'),'+\
                                                        copy_predicate_name_args_str_s_i+',Not('+copy_predicate_name_args_str_s_o+')' +\
                                                        '),'+countinged_object+'=='+countinged_object+'_copy' +\
                                                        '))'\
                                                ')'+\
                                                ')'
                                            else:#'Inc'
                                                need_to_proveed = 'And('+ \
                                                'Exists('+'['+ args_TypeInput_str_except_countinged_obj + '],'+\
                                                    'Exists('+countinged_object+',And('+predicate_name_args_str_s_o+',Not('+predicate_name_args_str_s_i+')))'+\
                                                '),'+\
                                                'ForAll('+'['+ args_TypeInput_str_except_countinged_obj + '],'+\
                                                    'ForAll('+countinged_object+',Implies(' +predicate_name_args_str_s_i+','+predicate_name_args_str_s_o +'))'+\
                                                '),'+\
                                                'ForAll('+'['+ args_TypeInput_str_except_countinged_obj + '],'+\
                                                    'ForAll(['+countinged_object+','+countinged_object+'_copy],Implies('+\
                                                        'And(' + \
                                                        predicate_name_args_str_s_o+',Not('+predicate_name_args_str_s_i+'),'+\
                                                        copy_predicate_name_args_str_s_o+',Not('+copy_predicate_name_args_str_s_i+')' +\
                                                        '),'+''+countinged_object+'=='+countinged_object+'_copy' +\
                                                        '))'\
                                                ')'+\
                                                ')'
                                        hig_num_prove_dict['need_to_proveed'] = need_to_proveed
                                        
                                        regression_e = regressionObj.dump_regression_exists(need_to_proveed,golog_root,hig_name) 
                                        #bak = regression_e
                                        regression_e = regressionObj.loop_regression_with_all_poss_ssa(regression_e,hig_name) # ，
                                        regression_e = regression_e.replace(',s_i)',')')
                                        regression_e = regression_e.replace('(s_i)','')
                                        # print(regression_e)
                                        hig_num_prove_dict['regression_e'] = regression_e
                                        regression_u = regressionObj.dump_regression_universal(need_to_proveed,golog_root,hig_name) 
                                        #bak = regression_u
                                        regression_u = regressionObj.loop_regression_with_all_poss_ssa(regression_u,hig_name) # ，
                                        regression_u = regression_u.replace(',s_i)',')')
                                        regression_u = regression_u.replace('(s_i)','')
                                        hig_num_prove_dict['regression_u'] = regression_u
                                    json_file = "./autogenerated/domain_steps_configJSON/{0}_{1}_eff_{2}_config.json".format(domainname,hig_name,each_hig_func_number) #
                                    with open(json_file, mode='w',encoding='utf-8') as fs:
                                        fs.write(json.dumps(hig_num_prove_dict,ensure_ascii=False,indent=1))


    # ==========================================================
    # write template py
    # ==========================================================
    
    def write_template_py(taskstr,template_py_to_be_writed,hig_action_name = None,eff_fluent = None ,eff_number_dict = None ):
        """ taskstr:'I','G','pre','eff_fluent','eff_number'
        write template py,,2I/G/pre,3eff_fluents,4eff_number.
         write_template_py('I',eff_template_py_to_be_writed,hig_name,each_hig_func_number,hig_num_prove_dict) """
        with open(template_py_to_be_writed,'w',encoding = 'utf-8') as templatefile:
            # The fixed head tags
            templatefile.write('# -*- coding: UTF-8 -*-\n')
            templatefile.write('#!/usr/bin/env python\n')
            templatefile.write('#-------------------------------------------------------------------------------\n')
            templatefile.write('# Name:        Automatic verification of sound abstraction for Generalized Planning.\n')
            templatefile.write('# Purpose:     low level 2 hig level description describe and prove\n')
            templatefile.write('#\n')
            templatefile.write('# Author:      this file is autogenerated by "main.py/autogenerator_python_prove_file()"\n')
            templatefile.write('#\n')
            templatefile.write('# Created:     ' + time.strftime("%a %b %d %H:%M:%S %Y", time.localtime()) +'\n' )
            templatefile.write('# Copyright:   (c) Tridu33 2021\n')
            templatefile.write('# Licence:     <MIT licence>\n')
            templatefile.write('#-------------------------------------------------------------------------------\n')
            templatefile.write('from z3 import *\n')
            templatefile.write('from func_timeout import func_set_timeout\n')
            templatefile.write('import func_timeout,time,os\n')
            # templatefile.write('import os\n')
            sys.path.append("..") 
            templatefile.write('\n')
            # Dict(): for preprocess/define/DeclareSort()Cons()EnumSort()  
            allclassTypes = []
            all_EnumSort_constants = []
            for parser_object_key,parser_object_value in parser.objects.items():
                parser_object_value_Enumtype = str(parser_object_key)
                allclassTypes.append(parser_object_value_Enumtype)
                parser_object_value_EnumObjects1 = str()
                parser_object_value_EnumObjects2 = str()
                for cur in parser_object_value:
                    parser_object_value_EnumObjects1 += ','+ cur
                    parser_object_value_EnumObjects2 += ',\''+ cur + '\''                    
                if len(parser_object_value) > 1:
                    templatefile.write('{0}, ({1}) = EnumSort(\'{0}\', ({2}))\n'.format(parser_object_value_Enumtype,parser_object_value_EnumObjects1[1:],parser_object_value_EnumObjects2[1:]))
                else: # len(parser_object_value) == 1. 'vehicle'-->['Vehicle']
                    templatefile.write('{0} = Datatype(\'{0}\')\n'.format(parser_object_key))
                    templatefile.write('{0}.declare(\'{0}\')\n'.format(parser_object_key))
                    templatefile.write('{0} = {0}.create()\n'.format(parser_object_key))
                    templatefile.write('{0} = Const(\'{0}\',{1})\n'.format(parser_object_value[0],parser_object_key))
                all_EnumSort_constants = all_EnumSort_constants + parser_object_value_EnumObjects1[1:].split(',')
            templatefile.write('\n')
            # Dict:[x y ,...]--> theRightType
            for key,value in parser.ConsForSorts.items():
                if value not in allclassTypes:
                    allclassTypes.append(value)
                    templatefile.write('{0} = DeclareSort("{0}")\n'.format(value))
                templatefile.write('{0} = Const(\'{0}\', {1})\n'.format(key[1:],value))
            templatefile.write('\n')

            templatefile.write('# declare mid situation action args:objects --> sort \n')
            if hig_action_name != None:
                for obj,sort in golobal_tree_mid_act_args_name2sort[hig_action_name].items():
                    # if obj == 'B':
                    #     print()
                    if obj not in all_EnumSort_constants:
                        templatefile.write('{0} = Const(\'{0}\', {1})\n'.format(obj,sort))
            templatefile.write('# mid temp refinement map action args declared in andlist \'exists\' or \'forall\'\n')
            if action_args_declear_andlist_dict_define_in_GologTree_Nests_assgined_in_main_regression != {}: # 
                for obj,sort in action_args_declear_andlist_dict_define_in_GologTree_Nests_assgined_in_main_regression.items():
                    obj = obj[1:] 
                    templatefile.write('{0} = Const(\'{0}\', {1})\n'.format(obj,sort)) 
                    #  dict : 'hig_name(=xxx)' -> {'arg_1':'BlockType';'arg_6':'BlockType';......} 
            # Predicates
            templatefile.write('# declare Predicates \n')
            for key,value in parser.predicates.items():
                if not value:
                    templatefile.write('{0} = Bool(\'{0}\')\n'.format(key)) # templatefile.write('arm_empty = Bool(\'arm-empty\')\n')
                    # copy Predicates in s situation Declares for s' situation with suffix "_"
                    # templatefile.write('{0}_ = Bool(\'{0}\')\n'.format(key)) # templatefile.write('arm_empty = Bool(\'arm-empty\')\n')#，
                else:
                    parser_predicates_TypeInput = str()
                    for TypeValues in value.values():
                        parser_predicates_TypeInput += ','+TypeValues
                    templatefile.write('{0} = Function(\'{0}\'{1},BoolSort())\n'.format(key,parser_predicates_TypeInput)) # templatefile.write('on = Function(\'onplus\', BlockType, BlockType, BoolSort())\n')
                    # copy Predicates in s situation Declares for s' situation with suffix "_"
                    # templatefile.write('{0}_ = Function(\'{0}\'{1},BoolSort())\n'.format(key,parser_predicates_TypeInput)) # templatefile.write('on_ = Function(\'onplus\', BlockType, BlockType, BoolSort())\n')
            templatefile.write('\n')
            # transitive closure
            for key,value in parser.predicates_transitive_closure.items():
                templatefile.write('{0} = TransitiveClosure({1})\n'.format(key,value))
                # copy Predicates in s situation Declares for s' situation with suffix "_"
                # templatefile.write('{0}_ = TransitiveClosure({1})\n'.format(key,value)) # templatefile.write('above_ = TransitiveClosure(on)\n')
            
            # transitive closure fml
            # for name,tcfmlObj in parser.predicates_transitive_closure_fml.items():
            #     args,fmlcnf = tcfmlObj.parameters,tcfmlObj.fmlcnf
            #     #fml = Nested_list2FOLExp().run(copy.deepcopy(fmlcnf))
            #     parser_predicates_TypeInput = str()
            #     for NameAndTypeValues in args:
            #         parser_predicates_TypeInput += ',' + NameAndTypeValues[1]
            #     templatefile.write('{0} = Function(\'{0}\'{1},BoolSort())# \n'.format(name,parser_predicates_TypeInput))
                
            templatefile.write('\n')
            # load constrain axtioms         
            templatefile.write('# load and exec domain constraint file of \"{0}\" given by users.\n'.format(domainname))
            
            templatefile.write('grader_father_src_path = os.path.abspath(os.path.dirname(__file__)+os.path.sep+"..")\n')
            #templatefile.write('grader_father_src_path = os.path.abspath(os.path.join(os.getcwd(), ".."))\n')
            if eff_fluent != None and eff_number_dict != None:# 4 arg,eff_number
                # 
                templatefile.write('for line in open(\'./constrainsConfig/{0}_constrain.txt\',\'r\'): \n'.format(domainname))
                #templatefile.write('for line in open(grader_father_src_path+"/constrainsConfig/{0}_constrain.txt",\'r\'): \n'.format(domainname))
            else:# I/G/pre/eff_fluents
                templatefile.write('for line in open(\'./constrainsConfig/{0}_constrain.txt\',\'r\'): \n'.format(domainname))
                #templatefile.write('for line in open(grader_father_src_path+"/constrainsConfig/%(domain_name)s_constrain.txt",\'r\'): \n')
            templatefile.write('    exec(line)\n')
            if eff_fluent != None and eff_number_dict != None:
                templatefile.write('@func_set_timeout({0})\n'.format(timeout_number)) # timeout_number =  5 s 
                templatefile.write('def myprove2(f1,f2):\n')
                templatefile.write('    s1 = Solver()\n')
                templatefile.write('    s1.add(Not(f1))\n')
                templatefile.write('    s2 = Solver()\n')
                templatefile.write('    s2.add(Not(f2))\n')
                templatefile.write('    # print(s1.sexpr())\n')
                templatefile.write('    if s1.check() == unsat and s2.check() == unsat:\n')
                templatefile.write('        del s1\n')
                templatefile.write('        del s2\n')
                templatefile.write('        print(os.path.basename(__file__)[:-3]+" is proved.")\n')
                templatefile.write('    else:\n')
                templatefile.write('        print(os.path.basename(__file__)[:-3]+" failed to prove")\n')
                templatefile.write('\n')
            templatefile.write('\n')
            templatefile.write('@func_set_timeout({0})\n'.format(timeout_number)) # timeout_number =  5 s 
            templatefile.write('def myprove(f):\n')
            templatefile.write('    s = Solver()\n')
            templatefile.write('    s.add(Not(f))\n')
            templatefile.write('    # print(s.sexpr())\n')
            templatefile.write('    if s.check() == unsat:\n')
            templatefile.write('        del s\n')
            templatefile.write('        print(os.path.basename(__file__)[:-3]+" is proved.")\n')
            templatefile.write('    else:\n')
            templatefile.write('        print(os.path.basename(__file__)[:-3]+" failed to prove")\n')
            templatefile.write('############################### start to prove! ####################################\n')
            if eff_fluent == None and eff_number_dict == None:# .this means "I/G/pre"
                templatefile.write('low = %(LOW_THEOREM)s\n')
                templatefile.write('hig = %(HIG_THEOREM)s\n')
                # templatefile.write('goal = \\ \n')
                templatefile.write('goal = And(\n')
                if 'G' == taskstr:
                    templatefile.write('    Implies(\n')
                    templatefile.write('        And(constraint,hig),\n')
                    templatefile.write('        low\n')
                    templatefile.write('    )\n')
                if 'I' == taskstr or 'pre' == taskstr:
                    # templatefile.write('    ,\n')
                    templatefile.write('    Implies(\n')
                    templatefile.write('        And(constraint,simplify(low)),\n')
                    templatefile.write('        simplify(hig)\n')
                    templatefile.write('    )\n')
                templatefile.write(')\n')
                templatefile.write('try:\n')
                templatefile.write('    # print(simplify(goal))\n')
                templatefile.write('    myprove(goal)\n')
                templatefile.write('except func_timeout.exceptions.FunctionTimedOut:\n')
                templatefile.write('    print(\'timeout and unknown,please open \\\'\'+os.path.basename(__file__)+\'\\\' and try.\')\n')
            elif eff_fluent != None and eff_number_dict == None:# 3 arg,eff_fluents
                # eff_fluent
                # templatefile.write('exists_regression = %(Exists_Regression)s\n')
                templatefile.write('poss_pre = %(poss_pre)s\n')
                templatefile.write('fluent_s_i = %(Fluent_s_i)s\n')
                templatefile.write('univer_regression = %(Univer_Regression)s\n')
                templatefile.write('goal = Implies(And(constraint,poss_pre),univer_regression) \n')
                templatefile.write('try:\n')
                templatefile.write('    # print(simplify(goal))\n')
                templatefile.write('    myprove(goal)\n')
                templatefile.write('except func_timeout.exceptions.FunctionTimedOut:\n')
                templatefile.write('    print(\'timeout and unknown,please open \\\'\'+os.path.basename(__file__)+\'\\\' and try.\')\n')
                # templatefile.write('myprove(goal)\n')
            elif eff_fluent != None and eff_number_dict != None:# 4 arg,eff_number
                if eff_number_dict['if_is_transitive_closure']==True: 
                    # 
                    templatefile.write('# exists regression ------------------------------------------------------\n')
                    type_declare_str = ''  # 'BlockType,Blocktype,'
                    tcarg_n_str = '' 
                    tcargSort = ''
                    for tcarg_n,tcarg_n_sort in eff_number_dict['tcargs_declare_sort'].items():
                        templatefile.write('{0} = Const(\'{0}\', {1}) \n'.format(tcarg_n,tcarg_n_sort))#  on ontc_fml()
                        # on(x,y)  "predicate_tc_base": "on","predicate": "above",
                        type_declare_str += tcarg_n_sort + ','
                        tcargSort = tcarg_n_sort
                        tcarg_n_str += tcarg_n + ','
                    tcarg_n_str = tcarg_n_str[:-1] 
                    #1 exists
                    templatefile.write('# p_e\n')
                    templatefile.write('P_fml_e = Function(\'P_fml_e\',{0}BoolSort())\n'.format(type_declare_str))
                    templatefile.write('TC_p_fml_e = TransitiveClosure(P_fml_e)\n')# 
                    templatefile.write('assign_p_fml_e = And(\n')
                    templatefile.write('    ForAll([{0}],Implies(P_fml_e({0}),TC_p_fml_e({0}))),\n'.format(tcarg_n_str))
                    templatefile.write('    ForAll ([{0}],P_fml_e({0}) == \\\n'.format(tcarg_n_str))
                    templatefile.write('        {0}\n'.format(eff_number_dict['p_fml_e']))
                    templatefile.write('    )\n')
                    templatefile.write(')\n')
                    templatefile.write('# q_e\n')
                    templatefile.write('q_fml_e = Function(\'q_fml_e\',{0}BoolSort()) \n'.format(type_declare_str))# on， on on
                    templatefile.write('TC_q_fml_e = TransitiveClosure(q_fml_e)\n')# on(x,y,s_o), above
                    templatefile.write('assign_q_fml_e = And(\n')
                    templatefile.write('    ForAll([{0}],Implies(P_fml_e({0}),TC_p_fml_e({0}))),\n'.format(tcarg_n_str))# 
                    templatefile.write('    ForAll ([{0}],P_fml_e({0}) == {1}({0}))\n'.format(tcarg_n_str,eff_number_dict["predicate_tc_base"]) )
                    templatefile.write(')\n')
                    
                    templatefile.write('# constraint tcarg_1,tcarg_2 tcarg_3\n')
                    templatefile.write('# +\n')
                    templatefile.write('TC_c_arg1 = Const(\'TC_c_arg1\', {0})\n'.format(tcargSort))
                    templatefile.write('TC_c_arg2 = Const(\'TC_c_arg2\', {0})\n'.format(tcargSort))
                    templatefile.write('TC_c_arg3 = Const(\'TC_c_arg3\', {0})\n'.format(tcargSort))
                    templatefile.write('TC_constraint_e = And(\n')
                    templatefile.write('    ForAll(TC_c_arg2,Exists(TC_c_arg1,And(TC_p_fml_e(TC_c_arg1,TC_c_arg2),clear(TC_c_arg1)))),\n')
                    templatefile.write('    ForAll([TC_c_arg1,TC_c_arg2,TC_c_arg3],Implies(And(TC_p_fml_e(TC_c_arg1,TC_c_arg2),TC_p_fml_e(TC_c_arg3,TC_c_arg2),clear(TC_c_arg1),clear(TC_c_arg3)),TC_c_arg1==TC_c_arg3))\n')
                    templatefile.write(')\n')
                    
                    predicate_args_list_vars_map_sort = hig_num_prove_dict['predicate_args_list_vars_map_sort']
                    countinged_obj = hig_num_prove_dict['countinged_obj'] # "countinged_obj": "x" predicate_args_list 
                    if '?'+countinged_obj not in hig_num_prove_dict["predicate_args_list"]:
                        raise Exception (' countinged_obj must in  hig_num_prove_dict[\'predicate_args_list\']')
                    fml_arg_str = '' 
                    fml_arg_str_copy = '' 
                    for each in hig_num_prove_dict["predicate_args_list"]: # ['?x','A']
                        if each[0] == '?':
                            fml_arg_str += each[1:] + ',' # '?x'
                            if each[1:] == countinged_obj:# '?x'[1:] == 'x','?y'[1:] != 'x'
                                fml_arg_str_copy += each[1:] + '_copy'  + ',' # == countinged_obj + '_copy'  + ','
                                for var_name,arg_sort in predicate_args_list_vars_map_sort.items(): # "predicate_args_list_vars_map_sort"==>"x": "BlockType"
                                    if var_name == countinged_obj: # must found because we build 'predicate_args_list_vars_map_sort' from the same nested list as well as 'predicate_args_list'
                                        templatefile.write('{0}_copy = Const(\'{0}_copy\', {1})\n'.format(countinged_obj,arg_sort)) 
                            else :
                                fml_arg_str_copy += each[1:] + ','
                        else:
                            fml_arg_str += each  + ',' # 'A'
                            fml_arg_str_copy += each + ','
                    fml_arg_str = fml_arg_str[:-1]# 'x,A' in 'TC_p_fml_e(x,A)'
                    fml_arg_str_copy = fml_arg_str_copy[:-1] # 'x_copy,A' in 'TC_p_fml_e(x_copy,A)'.

                    if hig_num_prove_dict['eff_inc_or_dec'] == 'Dec':
                        templatefile.write('# Dec effect: \n')
                        templatefile.write('wanted_e = And(\n')
                        templatefile.write('    Exists({0},And(TC_p_fml_e({1}),Not(TC_q_fml_e({1})))),\n'.format(countinged_obj,fml_arg_str))
                        templatefile.write('    ForAll({0},Implies(TC_q_fml_e({1}),TC_p_fml_e({1}))),\n'.format(countinged_obj,fml_arg_str))
                        templatefile.write('    ForAll([{0},{1}],Implies(And(TC_p_fml_e({2}),Not(TC_q_fml_e({2})),TC_p_fml_e({3}),Not(TC_q_fml_e({3}))),{0}=={1}))\n'.format(countinged_obj,countinged_obj+'_copy',fml_arg_str,fml_arg_str_copy))
                        templatefile.write(')\n')
                    else: # 'Inc'
                        templatefile.write('# Inc effect \n')
                        templatefile.write('wanted_e = And(\n')
                        templatefile.write('    Exists({0},And(TC_q_fml_e({1}),Not(TC_p_fml_e({1})))),\n'.format(countinged_obj,fml_arg_str))
                        templatefile.write('    ForAll({0},Implies(TC_p_fml_e({1}),TC_q_fml_e({1}))),\n'.format(countinged_obj,fml_arg_str))
                        templatefile.write('    ForAll([{0},{1}],Implies(And(TC_q_fml_e({2}),Not(TC_p_fml_e({2})),TC_q_fml_e({3}),Not(TC_p_fml_e({3}))),{0}=={1}))\n'.format(countinged_obj,countinged_obj+'_copy',fml_arg_str,fml_arg_str_copy))
                        templatefile.write(')\n')
                    templatefile.write('# goal_e\n')
                    templatefile.write('goal_e = Implies(And(constraint,assign_p_fml_e,assign_q_fml_e,TC_constraint_e),wanted_e)\n')
                    #2 universal
                    templatefile.write('# univer regression ----------------------------------------------\n')
                    templatefile.write('# p_u\n')
                    templatefile.write('p_fml_u = Function(\'p_fml_u\',{0}BoolSort())\n'.format(type_declare_str))
                    templatefile.write('TC_p_fml_u = TransitiveClosure(p_fml_u)\n')
                    templatefile.write('assign_p_fml_u = And(\n')
                    templatefile.write('    ForAll([{0}],Implies(p_fml_u({0}),TC_p_fml_u({0}))),\n'.format(tcarg_n_str))
                    templatefile.write('        ForAll ([{0}],p_fml_u({0}) == \\\n'.format(tcarg_n_str))
                    templatefile.write('            {0}\n'.format(eff_number_dict['p_fml_u']))
                    templatefile.write('    )\n')
                    templatefile.write(')\n')
                    templatefile.write('# q_u\n')
                    templatefile.write('q_fml_u = Function(\'q_fml_u\',{0}BoolSort())\n'.format(type_declare_str))
                    templatefile.write('TC_q_fml_u = TransitiveClosure(q_fml_u)\n')
                    templatefile.write('assign_q_fml_u = And(\n')
                    templatefile.write('        ForAll([{0}],Implies(q_fml_u({0}),TC_q_fml_u({0}))),\n'.format(tcarg_n_str))
                    templatefile.write('        ForAll ([{0}],q_fml_u({0}) == on({0}))\n'.format(tcarg_n_str))
                    templatefile.write(')\n')
                    
                    templatefile.write('# TC in z3-solver  constraint\n')
                    templatefile.write('TC_constraint_u = And(\n')
                    templatefile.write('    ForAll(TC_c_arg2,Exists(TC_c_arg1,And(TC_p_fml_u(TC_c_arg1,TC_c_arg2),clear(TC_c_arg1)))),\n'.format())
                    templatefile.write('    ForAll([TC_c_arg1,TC_c_arg2,TC_c_arg3],Implies(And(TC_p_fml_u(TC_c_arg1,TC_c_arg2),TC_p_fml_u(TC_c_arg3,TC_c_arg2),clear(TC_c_arg1),clear(TC_c_arg3)),TC_c_arg1==TC_c_arg3))\n')
                    templatefile.write(')\n')
                    
                    if hig_num_prove_dict['eff_inc_or_dec'] == 'Dec':
                        templatefile.write('# Dec effect: \n')
                        templatefile.write('wanted_u = And(\n')
                        templatefile.write('    Exists({0},And(TC_p_fml_u({1}),Not(TC_q_fml_u({1})))),\n'.format(countinged_obj,fml_arg_str))
                        templatefile.write('    ForAll({0},Implies(TC_q_fml_u({1}),TC_p_fml_u({1}))),\n'.format(countinged_obj,fml_arg_str))
                        templatefile.write('    ForAll([{0},{1}],Implies(And(TC_p_fml_u({2}),Not(TC_q_fml_u({2})),TC_p_fml_u({3}),Not(TC_q_fml_u({3}))),{0}=={1}))\n'.format(countinged_obj,countinged_obj+'_copy',fml_arg_str,fml_arg_str_copy))
                        templatefile.write(')\n')
                    else:#'Inc'
                        templatefile.write('#  Inc effect: \n')
                        templatefile.write('wanted_u = And(\n')
                        templatefile.write('    Exists({0},And(TC_q_fml_u({1}),Not(TC_p_fml_u({1})))),\n'.format(countinged_obj,fml_arg_str))
                        templatefile.write('    ForAll({0},Implies(TC_p_fml_u({1}),TC_q_fml_u({1}))),\n'.format(countinged_obj,fml_arg_str))
                        templatefile.write('    ForAll([{0},{1}],Implies(And(TC_q_fml_u({2}),Not(TC_p_fml_u({2})),TC_q_fml_u({3}),Not(TC_p_fml_u({3}))),{0}=={1}))\n'.format(countinged_obj,countinged_obj+'_copy',fml_arg_str,fml_arg_str_copy))
                        templatefile.write(')\n')
                    templatefile.write('# goal_u\n')
                    templatefile.write('goal_u = Implies(And(constraint,assign_p_fml_u,assign_q_fml_u,TC_constraint_u),wanted_u)\n')
                    # 3
                    templatefile.write('# start to prove ----------------------------------------------\n')
                    templatefile.write('# print(simplify(goal_e))\n')
                    templatefile.write('# print(simplify(goal_u))\n')
                    # templatefile.write('myprove(And(goal_e,goal_u))\n')
                    templatefile.write('try:\n')
                    # templatefile.write('    myprove(goal_u)\n')
                    # templatefile.write('    myprove(goal_e)\n')
                    templatefile.write('    myprove2(goal_e,goal_u)\n')
                    templatefile.write('except func_timeout.exceptions.FunctionTimedOut:\n')
                    templatefile.write('    print(\'timeout and unknown,please open \\\'\'+os.path.basename(__file__)+\'\\\' and try.\')\n')
                else:
                    # not transitive closure 
                    templatefile.write('# exists regression ------------------------------------------------------\n')
                    for tcarg_n,tcarg_n_sort in eff_number_dict['predicate_args_list_vars_map_sort'].items():
                        if tcarg_n == eff_number_dict['countinged_obj']:# grippercx,yx_copy
                            templatefile.write('{0}_copy = Const(\'{0}_copy\', {1}) \n\n'.format(tcarg_n,tcarg_n_sort))# ，’_copy‘
                    templatefile.write('hig_action_poss_fml = {0}\n'.format(eff_number_dict['hig_action_poss_fml']))
                    templatefile.write('regression_e = {0}\n'.format(eff_number_dict['regression_e']))
                    templatefile.write('regression_u = {0}\n'.format(eff_number_dict['regression_u']))
                    templatefile.write('\n')
                    templatefile.write('goal_e = Implies(And(hig_action_poss_fml,constraint),regression_e)\n')
                    templatefile.write('goal_u = Implies(And(hig_action_poss_fml,constraint),regression_u)\n')
                    templatefile.write('try:\n')
                    # templatefile.write('    myprove(And(goal_e,goal_u))\n')
                    templatefile.write('    myprove2(goal_e,goal_u)\n')
                    templatefile.write('except func_timeout.exceptions.FunctionTimedOut:\n')
                    templatefile.write('    print(\'timeout and unknown,please open \\\'\'+os.path.basename(__file__)+\'\\\' and try.\')\n')
            else :
                raise Exception("No match call for \'def write_template_py\'.")
            templatefile.close()
            # COMMAND_RUN = 'notepad {0}'.format(template_py_to_be_writed)
            #os.system(COMMAND_RUN) # open and see the template_py_to_be_writed file.
    template_py_to_be_writed_G = r"{0}/autogenerated/domain_template/{1}_G_template.py".format(os.path.dirname(os.path.abspath(__file__)),domainname)
    template_py_to_be_writed_I = r"{0}/autogenerated/domain_template/{1}_I_template.py".format(os.path.dirname(os.path.abspath(__file__)),domainname)
    
    # for 'I'/'G'
    write_template_py('I',template_py_to_be_writed_I) 
    write_template_py('G',template_py_to_be_writed_G) 

    # for pre. ============================================================================================     each hig aciton name 'pickabove'/'putaside'
    for eachactionmap in parser.refinementMap_actionsMap:
        for hig_name,_ in eachactionmap.act_map_golog_dict.items():  # only run one times because"higname --> GologTree with GologNode "
            pre_template_py_to_be_writed = r"{0}/autogenerated/domain_template/{1}_template_{2}.py".format(os.path.dirname(os.path.abspath(__file__)),domainname,hig_name)
            write_template_py( 'pre',pre_template_py_to_be_writed,hig_name)
    
    # for eff.=============================================================================================       
    for eachactionmap in parser.refinementMap_actionsMap:# print(eachactionmap.act_map_golog_dict)                            # {'putaside': <__main__.GologNode object}
        for hig_name,_ in eachactionmap.act_map_golog_dict.items():  # only run one times because"higname --> GologTree with GologNode "
            for eachaction in qnp_parser.actionlist:# ‘pickabove’ & 'putaside'.like: {'n': 'Dec', 'H': 'True'}
                if eachaction.name == hig_name:
                    # 1.  
                    for each_hig_fluent_in_eff in qnp_parser.stateRepresentation_fluents:  #    ['T']
                        if each_hig_fluent_in_eff in eachaction.effstate:
                            eff_template_py_to_be_writed = r"{0}/autogenerated/domain_template/{1}_{2}_eff_{3}_template.py".format(os.path.dirname(os.path.abspath(__file__)),domainname,each_hig_fluent_in_eff,hig_name)
                            write_template_py('eff_fluent',eff_template_py_to_be_writed,hig_name,each_hig_fluent_in_eff)
                            autogenerator_python_prove_file(domainname,'placeholder_will_not_be_used_in_this_call',hig_name,each_hig_fluent_in_eff)
                    # 2.  
                    for each_hig_func_number in qnp_parser.stateRepresentation_variables:#  ['b', 'c', 'g']
                        if each_hig_func_number in eachaction.effstate:
                            json_file = r"./autogenerated/domain_steps_configJSON/{0}_{1}_eff_{2}_config.json".format(domainname,hig_name,each_hig_func_number) #
                            hig_num_prove_dict = {} # 
                            with open(json_file, mode='r') as fs:
                                hig_num_prove_dict = json.load(fs)
                            # print(f'contents readed from {json_file}is :\n')
                            # print(obj)  
                            eff_template_py_to_be_writed = r"./autogenerated/{0}_{1}_eff_{2}.py".format(domainname,hig_name,each_hig_func_number) 
                            write_template_py('eff_number',eff_template_py_to_be_writed,hig_name,each_hig_func_number,hig_num_prove_dict) # 
        
    #COMMAND_RUN = 'notepad "{0}/autogenerated/domain_template/{1}_template.py"'.format(os.path.dirname(__file__),domainname)
    #os.system(COMMAND_RUN) # open the python template file for watching.

    # ==========================================================
    # generate the correct "low theorem" --> "hig theorem" and write goals out into json config files "./autogenerated/domain_steps_configJSON/{0}_{1}_config.json"
    # steps of how to map hig level description into low level golog FOL formula and prove:
    # 1. I
    # 2. G
    # 3. pres of actions
    # 4. effs of actions
    # ==========================================================

    prove_tasks_list = ['I','G']
    for eachaction in qnp_parser.actionlist:
        prove_tasks_list.append(eachaction.name+'_pre')
    for eachaction in qnp_parser.actionlist:
        for key ,_ in eachaction.effstate.items():
            prove_tasks_list.append(eachaction.name+'_eff_'+ key)

    # list of prove theorem tasks:
    # print('*'*30)
    print("prove_tasks_list with "+str(len(prove_tasks_list)),end=' elements is:')
    print(prove_tasks_list) #['I','G','pickabove_pre','pickabove_eff','putaside_pre','putaside_eff']

    # region 

    
    # I
    whichStepToProve = prove_tasks_list[0]
    
    low_to_prove_for_this_step = Nested_list2FOLExp().run(copy.deepcopy(parser.state))
    low_to_prove_for_this_step = "And(" + low_to_prove_for_this_step + ")"
    # print(low_to_prove_for_this_step) #  And(clear(G),on_table(A),on_table(x),arm_empty,Exists(x,(And(above(G,x),Or(above(x,A),x==A)))))
    hig_to_prove_for_this_step = 'And('
    for key,value in qnp_parser.initstate.items():
        if value == 'False': # fluents
            hig_to_prove_for_this_step += ('Not('+ refinementMap_Dict[key] +'),')
        elif value == 'True':
            hig_to_prove_for_this_step += (refinementMap_Dict[key]+',')
        elif value == '=0': # fluents
            hig_to_prove_for_this_step += ('Not('+ refinementMap_Dict[key] +'),')
        elif value == '>0':
            hig_to_prove_for_this_step += (refinementMap_Dict[key]+',')
    if hig_to_prove_for_this_step[-1] == ',':
        hig_to_prove_for_this_step = hig_to_prove_for_this_step[:-1]
    hig_to_prove_for_this_step += ')'

    low_to_prove_for_this_step = rerplace_predicate_tcfml_withcnf(low_to_prove_for_this_step)
    hig_to_prove_for_this_step = rerplace_predicate_tcfml_withcnf(hig_to_prove_for_this_step)
    write_json_config_file2theoremConfigJson(domainname,whichStepToProve,low_to_prove_for_this_step,hig_to_prove_for_this_step)
    
    # G
    whichStepToProve = prove_tasks_list[1]
    low_to_prove_for_this_step = 'And('+Nested_list2FOLExp().run(copy.deepcopy(parser.goalstateNestList)) +')' # print(low_to_prove_for_this_step) # "clear(A)"
    # print(qnp_parser.goalstate)
    if DEBUG == True:
        print(refinementMap_Dict)
    hig_to_prove_for_this_step = 'And('
    for key,value in qnp_parser.goalstate.items():
        if value == 'False': # fluents
            hig_to_prove_for_this_step += ('Not('+ refinementMap_Dict[key] +'),')
        elif value == 'True':
            hig_to_prove_for_this_step += (refinementMap_Dict[key]+',')
        elif value == '=0': # fluents
            hig_to_prove_for_this_step += ('Not('+ refinementMap_Dict[key] +'),')
        elif value == '>0':
            hig_to_prove_for_this_step += (refinementMap_Dict[key]+',')
    if hig_to_prove_for_this_step[-1] == ',':
        hig_to_prove_for_this_step = hig_to_prove_for_this_step[:-1]
    hig_to_prove_for_this_step += ')'
    
    #print(hig_to_prove_for_this_step) #And(Not(Exists(x,(above(x,A)))))
    low_to_prove_for_this_step = rerplace_predicate_tcfml_withcnf(low_to_prove_for_this_step)
    hig_to_prove_for_this_step = rerplace_predicate_tcfml_withcnf(hig_to_prove_for_this_step)
    write_json_config_file2theoremConfigJson(domainname,whichStepToProve,low_to_prove_for_this_step,hig_to_prove_for_this_step)
    # endregion

    # ==========================================================
    # generate the python_prove*_file we want 
    # with "./midfile/{domainname}_*I/G_config.json" and "{domainnaoe}_template.py"
    # ==========================================================

    # 'I','G', Preconditions of actions,effects of actions: the init goal need to be proved.
    # I
    try:
        autogenerator_python_prove_file(domainname,prove_tasks_list[0])
    except Exception as err:
        print('Exception:',err)
    # G
    try:
        autogenerator_python_prove_file(domainname,prove_tasks_list[1])
    except Exception as err:
        print('Exception:',err)
    

    # ==========================================================
    # generate the python_prove*_file we want 
    # with "./midfile/{domainname}_*Pre/Eff_config.json" and "{domainnaoe}_template.py"
    # ==========================================================
    
    # pres/effs of actions:
    
    # pre  
    for eachactionmap in parser.refinementMap_actionsMap:
        # print(eachactionmap.act_map_golog_dict)                   
        for hig_name,_ in eachactionmap.act_map_golog_dict.items():  # only run one times because"higname --> GologTree with GologNode "
            try:
                autogenerator_python_prove_file(domainname,hig_name+'_pre',hig_name) # for eachaction in qnp_parser.actionlist:
            except Exception as err:
                print('Exception:',err)

    # ==========================================================
    # run_all_python_prove_file_in_dir_autogenerated
    # ==========================================================

    run_all_python_prove_file_in_dir_autogenerated()
    
    # if all results show "proved",including: 'I','G', Preconditions of actions,effects of actions
    # then all is Done.



if __name__ == '__main__':
    import time
    start_time = time.perf_counter()
    main()
    end_time = time.perf_counter()
    print('it cost: ',end_time - start_time,'(s).')