Number of sentences and sentential forms generated by a grammar In this question, I'm considering only &quot;finite grammars&quot;. A finite grammar can only produce a finite number of distinct sentences. The following grammar is finite in my definition:
S         → AB
A         → B | a 
B         → a | b

It can only generate the following finite number of sentences: aa, ab, ba, bb
On the other hand, the following grammar is not finite:
S         → AB
A         → AA | B | a 
B         → a | b

Because it can create an infinite number of sentences: aa, aaa, aaaa, aaaaa, ...
Now to the actual question. Suppose the following finite grammar:
S         → variable = math_expr
variable  → a | b | c 
math_expr → INT | function
function  → func_1() | func_2(INT, INT, INT, INT)
INT       → 1 | 2 | 3 | 4 | 5

I want to know if there is some kind of formula that calculate the number of sentences and sentential forms that can be generated by a finite grammar.
Example of sentences: b = func_2(2,4,3,3), a = func_1()
Example of sentential forms: b = func_2(2,2,INT,INT), c = math_expr,  S
At the moment, I am able to know the number of sentences and sentential forms by applying a Breadth-First Search (BFS) starting from the S node.
However, because I'm working with search in program synthesis, it would be great to know the size of the domain without the need of applying an exhaustive search on it.
Question: How can I find the number of sentences and sentential forms given only an arbitrary finite grammar?
For the first finite grammar I showed here, the answer is easy to calculate by hand:
Sentences: aa, ab, ba, bb
Sentential forms: S, AB, BB, aB, bB, Aa, Ab
So the final answer would be 4 + 7 = 11
However, for the second finite grammar I showed, it is not that easy to calculate it.
PS.: In my original problem, I am working with program synthesis with a Domain Specific Language (DSL). I tagged CFG with the hope that the same applies, granted I'm not 100% sure.
If the context-free grammar is unambiguous, you can count the number of sentences it generates in a linear scan with a carefully chosen order.
I'll assume we have removed all useless symbols and cycles from the grammar.  If it is finite and free of useless symbols and cycles, then it should not contain any recursion.
Let $N(A)$ denote the number of sentences that can be constructed starting from nonterminal $A$, i.e., $N(A) = |L(A)|$.  If the grammar is unambiguous and has no recursion, you can compute $N(A)$ for each nonterminal as follows.  Construct a dependency graph with one vertex per nonterminal, and an edge $A \to B$ whenever the grammar contains a rule $B ::= \cdots A \cdots$, i.e., a rule with $B$ on the left-hand side and $A$ on the right-hand side.  If the grammar has no recursion, then this is a dag.  Visit the vertices of this graph in topologically sorted order.  Then it is easy to compute the number of sentences: for example, if we have the rule $A ::= BaC | DE$, then we have
$$N(A) = N(BaC) + N(DE) = N(B) N(a) N(C) + N(D) N(E).$$
That's an example, but you can do the same for any number of alternatives on the right-hand side and any string of symbols in each alternative.  Note that we have the base case $N(a) = 1$, for any terminal $a$.
I expect this can be adjusted to count the number of sentential forms as well, but I haven't tried to work out the details.
This relies crucially on the grammar to be unambiguous.  If the grammar is ambiguous, I'm not sure whether there is any efficient algorithm -- I just don't know.
For unambiguous grammars, see also https://en.wikipedia.org/wiki/Chomsky%E2%80%93Sch%C3%BCtzenberger_enumeration_theorem, which shows how to count the number of sentences of a particular length, even if the grammar is not finite.