  Component-based synthesis seeks to build programs using the APIs provided by
a set of libraries. Oftentimes, these APIs have effects, which make it
challenging to reason about the correctness of potential synthesis candidates.
This is because changes to global state made by effectful library procedures
affect how they may be composed together, yielding an intractably large search
space that can confound typical enumerative synthesis techniques. If the nature
of these effects are exposed as part of their specification, however, deductive
synthesis approaches can be used to help guide the search for components. In
this paper, we present a new specification-guided synthesis procedure that uses
Hoare-style pre- and post-conditions to express fine-grained effects of
potential library component candidates to drive a bi-directional synthesis
search strategy. The procedure alternates between a forward search process that
seeks to build larger terms given an existing context but which is otherwise
unaware of the actual goal, alongside a backward search mechanism that seeks
terms consistent with the desired goal but which is otherwise unaware of the
context from which these terms must be synthesized. To further improve
efficiency and scalability, we integrate a conflict-driven learning procedure
into the synthesis algorithm that provides a semantic characterization of
previously encountered unsuccessful search paths that is used to prune the
space of possible candidates as synthesis proceeds. We have implemented our
ideas in a tool called Cobalt and demonstrate its effectiveness on a number of
challenging synthesis problems defined over OCaml libraries equipped with
effectful specifications.
