An implementation of StandardExAllSolver presented in section 6.1 of the paper. As stated in the paper, this implementation boils down to exhaustive enumeration of possible solutions, and as such isn't effective. It can be used to better understand how the synthesis procedure works and provides a lot of debugging output. Do not use this procedure for solving real problems.

An implementation of RefinedExAllSolver presented in section 6.2 of the paper. This is an improved version of standardExAllProcedure. It only keeps input values \(|\vec I|\) in \(S\) and uses different synthesis constraints on synthesis and verification steps.

This procedure is not part of the paper. It uses forall quantification directly when creating variables from the \(T\) set. As consequence it requires an SMT-solver than can handle foralls (for instance, Z3). This procedure is the easiest to understand.

First step of each synthesis procedure. Given a library of components and a number of program's inputs, it creates existentially quantified location variables (members of set \(L\) in the paper) for each component and for the program itself.

Second step of each synthesis procedure. It applies constraints on location variables from section 5 of the original paper. These constraints include well-formedness constraint \(ψ_{wfp}\), acyclicity constraint \(ψ_{acyc}\) and consistency constraint \(ψ_{cons}\). Constraints are not returned from this function, but are applied immediately. Section 5 of the paper also talks about connectivity constraint \(ψ_{conn}\), which is not created here.

Third step of the synthesis process. It creates variables that represent actual inputs/outputs values (members of the set \(T\) in the paper). This function resembles createProgramLocs, but unlike it allows creating both existentially and universally quantified variables. Standard and Refined procedures pass sbvExists to create existentially quantified variables, while exAllProcedure uses sbvForall.

Last building block of the synthesis process. This function creates \(ψ_{conn}\) and \(φ_{lib}\) constraints and return them.