  Given a specification $\varphi(X,Y)$ over inputs $X$ and output $Y$, defined
over a background theory $\mathbb{T}$, the problem of program synthesis is to
design a program $f$ such that $Y=f(X)$ satisfies the specification $\varphi$.
Over the past decade, syntax-guided synthesis (SyGuS) has emerged as a dominant
approach for program synthesis where in addition to the specification
$\varphi$, the end-user also specifies a grammar $L$ to aid the underlying
synthesis engine. This paper investigates the feasibility of synthesis
techniques without grammar, a sub-class defined as $\mathbb{T}$-constrained
synthesis.
  We show that $\mathbb{T}$-constrained synthesis can be reduced to
DQF($\mathbb{T}$), i.e., to the problem of finding a witness of a Dependency
Quantified Formula Modulo Theory. When the underlying theory is the theory of
bitvectors, the corresponding DQF(BV) problem can be further reduced to
Dependency Quantified Boolean Formulas (DQBF). We rely on the progress in DQBF
solving to design DQBF-based synthesizers that outperform the domain-specific
program synthesis techniques, thereby positioning DQBF as a core representation
language for program synthesis. Our empirical analysis shows that
$\mathbb{T}$-constrained synthesis can achieve significantly better performance
than syntax-guided approaches. Furthermore, the general-purpose DQBF solvers
perform on par with domain-specific synthesis techniques.
