fun eval(interpretation : Map<String, Boolean>) : Boolean {
        return when ( this ) {
            is Variable -> interpretation.get(variable)!!
            is Conjunction -> left.eval(interpretation) && right.eval(interpretation)
            is Disjunction -> left.eval(interpretation) || right.eval(interpretation)
            is Implication -> left.eval(interpretation).not() || right.eval(interpretation)
            is Equivalence -> left.eval(interpretation) == right.eval(interpretation)
            is Negation -> formula.eval(interpretation).not()

            else -> throw Exception("something bad happened in Eval")
        }
    }

    fun negate() : Formula {
        return when ( this ) {
            is Variable -> Negation(Variable(variable))
            is Conjunction -> Disjunction(left.negate(), right.negate())
            is Disjunction -> Conjunction(left.negate(), right.negate())
            is Equivalence -> Disjunction(Conjunction(left.negate(), right), Conjunction(left, right.negate()))
            is Implication -> Conjunction(left, right.negate())
            is Negation ->  formula

            else -> throw Exception("something bad happened in Negate")
        }
    }

    fun simplify() : Formula {
        when {
                ( this is Conjunction ) -> {
                    return when {
                        this.right is True -> this.left.simplify()
                        this.left is False || this.right is False -> False()
                        this.left is True -> this.right.simplify()
                        this.left == this.right -> this.left.simplify()
                        this.left == this.right.negate() -> False()
                        else -> this
                    }
                }
                ( this is Disjunction ) -> {
                    return when {
                        this.left is True || this.right is True -> True()
                        this.left is False -> this.right.simplify()
                        this.right is False -> this.left.simplify()
                        this.left == this.right.negate() -> False()
                        this.left == this.right -> this.left.simplify()
                        else -> this
                    }
                }
                ( this is Negation ) -> {
                    return when {
                        this.formula is Negation -> this.formula.formula.simplify()
                        else -> return this
                    }
                }
                else -> return this
            }
        }