几周前 浅尝 z3，貌似和 prolog 有点像。于是继 四年前 再做个原型：输入「甲有问题或乙有问题。若甲有问题则乙有问题。」输出「乙有问题」

为支持无空格语法，仍使用rply定制版的按语法分词。主要语法规则如下：

        @分析器母机.语法规则("代码 : 各句 句号")
        def 代码(片段):
            if s.check() != z3.sat:
                raise ValueError("有误")
            
            结果 = s.model()
            for 某项 in 结果:
                if 结果[某项]:
                    return str(某项) + '有问题'

        @分析器母机.语法规则("各句 : 结构句")
        @分析器母机.语法规则("各句 : 各句 句号 结构句")
        def 各句(片段):
            if len(片段) == 1:
                return f"{片段[0]}"
            if len(片段) == 3:
                return f"{片段[0]} {片段[2]}"

        @分析器母机.语法规则("结构句 : 句 或者 句")
        def 或者(片段):
            新布尔量 = z3.Bools(
                [片段[0], 片段[2]]
            )
            各值[片段[0]] = 新布尔量[0]
            各值[片段[2]] = 新布尔量[1]

            s.add(functools.reduce(self.或者, list(各值.values())))

        @分析器母机.语法规则("结构句 : 假设 句 那么 句")
        def 假设(片段):
            假定条件 = 片段[1]
            关联结果 = 片段[3]
            s.add(z3.If(
                    各值[假定条件] == True,
                    各值[关联结果] == True,
                    True,
                ))
            
        @分析器母机.语法规则("句 : 标识符 有问题")
        def 句(片段):
            return 片段[0].getstr()

为简短起见，z3部分直接集成在了语法分析处理里。虽然 分词时回退次数超出了内置上限，不过至少此例运行速度尚可。完整代码 在此。