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. It also doesn't support constant components. 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.

Special version of createProgramVarsWith for constant components. A constant component is a component having specArity \(=0\). The original paper slightly touches this topic in the last paragraph of section 7. This function always uses existential quantification and only operates on constant components. The Program returned from this function contains undefined values for programIOs and non-constant programInstructions. The user is expected to call createProgramVarsWith later and then use combineProgramVars to merge two results.

Given a Program of constant-only components and a Program of non-constant components, combine them into a single Program.

Smart version of getValue for Instruction. For each component it gets solutions for location variable, effectively turning 'Instruction SLocation (comp a)' into 'Instruction Location (comp a)'. For constant components it additionaly fills 'comp a' part of the structure with its returning value.