-
公开(公告)号：CN117312722A
公开(公告)日：2023-12-29
申请号：CN202311222434.1
申请日：2023-09-21
申请人： 华东师范大学
摘要： 本发明公开了一种基于SMT求解器的多系统任务规划方法，涉及自动化任务规划和调度领域，包括以下步骤：S1：对输入的任务序列进行解析；S2：信息预处理，根据输入的任务序列以及要求输出的序列生成相应的指令模板；S3：子系统建模，生成待求解的初始指令序列；S4：通过交互式工具将自然语言约束转化为符合要求的一阶谓词逻辑公式，并通过Z3库函数添加到SMT求解器中；S5：SMT求解器进行约束求解，子系统的约束加入到SMT求解中后，调用Solver.check(self,*assumptions)方法即可完成求解；S6：根据SMT求解器返回的结果，对任务序列进行分析，生成最终的指令序列。本发明将自然语言约束转化为一阶谓词逻辑公式，通过SMT求解器进行求解，并对结果进行解析，最终得到符合条件的指令序列。
-
公开(公告)号：CN118862765A
公开(公告)日：2024-10-29
申请号：CN202410836706.5
申请日：2024-06-26
申请人： 华东师范大学
IPC分类号： G06F30/33 , G06F119/06
摘要： 本发明公开了一种多线程的VCD文件数据统计工具及其应用方法，属于电子数字技术领域。其结构包括读取VCD文件定义部分、并行读取VCD文件数据部分和计算并输出结果部分。其方法包括读取VCD文件定义部分；根据var_to_number将信号转为对应信号序号；根据var_to_number将信号转为信号标志，根据var_output_name将信号序号转为信号真实名称；对数据进行解析和统计，通过计算得到反转率并直接将信号输出到表格中。本发明采通过本工具使用数据统计的方式来获取各个信号的翻转率进而方便开发人员计算动态功耗。并且采用并行读取的方式进行统计，在数据量较大的情况下会拥有更高的性能，运行时间更短。
-
公开(公告)号：CN117312722B
公开(公告)日：2024-03-19
申请号：CN202311222434.1
申请日：2023-09-21
申请人： 华东师范大学
摘要： 本发明公开了一种基于SMT求解器的多系统任务规划方法，涉及自动化任务规划和调度领域，包括以下步骤：S1：对输入的任务序列进行解析；S2：信息预处理，根据输入的任务序列以及要求输出的序列生成相应的指令模板；S3：子系统建模，生成待求解的初始指令序列；S4：通过交互式工具将自然语言约束转化为符合要求的一阶谓词逻辑公式，并通过Z3库函数添加到SMT求解器中；S5：SMT求解器进行约束求解，子系统的约束加入到SMT求解中后，调用Solver.check(self,*assumptions)方法即可完成求解；S6：根据SMT求解器返回的结果，对任务序列进行分析，生成最终的指令序列。本发明将自然语言约束转化为一阶谓词逻辑公式，通过SMT求解器进行求解，并对结果进行解析，最终得到符合条件的指令序列。
-
-
搜索结果
3 条记录 (耗时 0.025 秒)
