measure the cost of term by counting and multiply a constant
check Term have non-terminal
count Term have how many terminals
count Term have how many non-terminals
check the given smt string passing all condition by z3
just change one non-terminal
parse sygus string and make ast
Find the synth-fun list body by BFS
Find the synth-fun list body by using heap
find the correct synth-fun body of sygus string
change sort of Ast to term of Ast
change first SynthFun with given DefineFun
verify the given sygus ast and the presumed answer body of synth-fun