Boolean[3]-Quiz: keine Variablen, DNF-Syntax

Eine Würfel-Konfig sieht so aus:

BIC { formula_size = 4
    , variables = [ p,r,s,t]
, operators_in_instance = Binu
                                  { functions = [], binary = [ && , <-> , ->] , unary = [ ] , nullary = [  ]
                                  }
    , constraints_for_solution = [ Operators
                                       [ not , &&  , || ]
                                 ]
    , show_syntax_tree_ = True
    , instance_candidates = 100 
}

da entstehen aber auch Instanzen, die nicht alle Variablen enthalten.

Wenn die Konfig nulläre Symbole enthält, entstehen auch Instanzen, die gar keine Variablen enthalten.

Die beschreiben konstante Funktionen, aber diese Instanzen sind nicht lösbar, weil der Student die nicht hinschreiben darf?

Eigentlich doch (denn die nullären Symbole sind da), aber tatsächlich nicht, wenn die Syntax weiter eingeschränkt wird:

Konfig: [ Operators [ !, ||, &&] , Normalform Disjunktiv
    ] 
Instanz: (false  -> ((true  -> true ) -> false )) -> true 

ist äquivalent zu true, die DNF ist eine leere Klausel (or [and []]), das darf man aber nicht hinschreiben. Work-arounds wie x || not x sind zurecht ferboten, weil die Variable x in der Instanz nicht vorkommt.

Lösungsplan

• der Würfel soll sich bemühen, Variablen auch tatsächlich zu verwenden (entweder syntaktisch prüfen oder semantisch - der Werteverlauf des gewürfelten Ausdrucks sollte "möglichst nicht-konstant" sein)
• die Formeln "true" und "false" sollen immer als DNF und CNF akzeptiert werden.

und immer auch

• der Tutor muß einen Knopf erhalten, durch den er für einen Studenten eine neue Instanz erzeugen kann (das ist separates Issue)