这项工作的重点是有效地为可理解性模态理论(SMT)公式生成不同的解决方案,针对位向量,数组和未解释函数的理论,这是软件和硬件测试的关键任务。 生成多样化的 SMT 解决方案有助于在验证和测试过程中发现故障并检测安全违规行为,从而产生 SMT 采样问题,即构建少量解决方案,同时实现对约束空间的全面覆盖。 虽然高覆盖率对于探索系统行为至关重要,但减少解决方案的数量非常重要,因为过度的解决方案会增加测试时间和资源使用,从而破坏了效率。 在这项工作中,我们介绍了PanSampler,一种新颖的SMT采样器,通过少量解决方案实现高覆盖。 它集成了三种新颖的技术,即具有多样性感知的SMT算法,抽象语法树(AST)引导的评分函数和采样后优化技术,增强了其实际性能。 它迭代采样解决方案,评估候选人,并使用本地搜索来改进解决方案,确保少量样本的高覆盖率。 对实际基准的广泛实验表明,PanSampler具有显着更强的达到高目标覆盖率的能力,同时需要比当前采样器更少的解决方案来实现相同的覆盖水平。 此外,我们从实际软件系统收集的实践主题的经验评估表明,PanSampler实现了更高的故障检测能力,并将所需的测试用例数量从32.6%减少到76.4%,以达到相同的故障检测效率,从而大大提高了测试效率。 PanSampler推进SMT采样,降低了软件测试和硬件验证的成本。