nullary and unary ands and ors

[yoni206]

This PR is a proposal to make our pythonic API act similarly to z3 when the user tries to create nullary/unary and/or terms.

our current main:

>>> x = Bool("x")
>>> And(x)
Traceback (most recent call last):
  File "<stdin>", line 1, in <module>
  File "/home/panda/git/cvc5_pythonic_api/cvc5_pythonic_api/cvc5_pythonic.py", line 1720, in And
    return _nary_kind_builder(Kind.AND, *args)
  File "/home/panda/git/cvc5_pythonic_api/cvc5_pythonic_api/cvc5_pythonic.py", line 1125, in _nary_kind_builder
    return _to_expr_ref(ctx.solver.mkTerm(kind, *[a.ast for a in args]), ctx)
  File "cvc5.pxi", line 1438, in cvc5_python_base.Solver.mkTerm
RuntimeError: Invalid kind 'AND', expected Terms with kind AND must have at least 2 children and at most 67108863 children (the one under construction has 1)
>>> And()
Traceback (most recent call last):
  ...  
>>> solve(And())
Traceback (most recent call last):
  ...
>>> solve(Or())
Traceback (most recent call last):
...

After this PR:

>>> x = Bool("x")
>>> And(x)
x
>>> And()
True
>>> solve(And())
[]
>>> solve(Or())
no solution

z3:

>>> x = Bool("x")
>>> And(x)
And(x)
>>> And()
And
>>> solve(And())
[]
>>> solve(Or())
no solution

There will still be a difference between the printing of such terms (z3: And, And(x), cvc5: True, x), but at least it will be supported and will have the same semantics.

What do you think?