The paper focuses on the automatic generating of the witnesses for the word equation satisfiability problem by means of specializing an interpreter which tests whether a composition of variable substitutions of a given word equation system produces its solution. We specialize such an interpreter w.r.t. the equation system, while the substitutions are unknown. We show that several variants of such interpreters, when specialized using the basic unfold/fold specialization methods, are able to construct the whole solution sets for some classes of the word equations whose left- and right-hand sides share variables. We prove that the specialization process wrt the constructed interpreters gives a simple syntactic criterion of the satisfiability of the equations considered, and show that the suggested approach can solve some equations not solvable by Z3str3 and CVC4, the widely-used SMT-solvers.

翻译：本文侧重于自动生成单方程相对性问题的证人,其方法是专门聘请一名口译员来测试某一单方程系统变量替代的构成是否产生解决办法。我们专门为这种方程系统指定了一个口译员w.r.t.t.,而替代则未知。我们显示,这些口译员在使用基本的展出/倍化专业化方法进行专门化时,能够为左侧和右侧共同变量的某几类单词方程构建全套解决方案。我们证明,所构建的口译员的专业化过程为所考虑方程的可比较性提供了一个简单的综合标准,并表明所建议的方法可以解决一些被广泛使用的SMT-溶解器Z3str3和CVC4无法溶解的方程。