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 \name\ and
demonstrate its effectiveness on a number of challenging synthesis
problems defined over OCaml libraries equipped with effectful
specifications.