Assign true to all variable except one

I have a list of variables and I want to add constraint to z3 solver such as all variables should be False except one variable should be True ..

a,b,c,d= Bool('a,b,c,d')
s = Solver()
allvariables=[a,b,c,d,f] 
for i in allvariables:
     s.add(i==True)
     

Do I need to use Quantifier ?

As stated by @alias, there are alternative encodings of the exactly-one cardinality constraints.

The Sum() function makes life easy:

    from z3 import *
    
    a, b, c, d = Bools('a b c d')
    allvariables = [a, b, c, d]
    s = Solver()
    
    #  exactly one
    s.add(Sum(allvariables) == 1)
    
    res = s.check()
    sol_no = 0
    while (res == sat):
      m = s.model()
      block = []
      sol_no += 1
      print(f"Solution #{sol_no}")
      for var in allvariables:
          v = m.evaluate(var, model_completion=True)
          print("%s = %s " % (var, v)),
          block.append(var != v)
      s.add(Or(block))
      print("")
      res = s.check()

Result are four solutions as expected:

Solution #1
a = False 
b = False 
c = True 
d = False 

Solution #2
a = False 
b = True 
c = False 
d = False 

Solution #3
a = False 
b = False 
c = False 
d = True 

Solution #4
a = True 
b = False 
c = False 
d = False