private function crossTreeConstraint($rule) {
        $op = $rule->getName();
        $num = $rule->count();

        if ($op === "eq" && $num === 2)
            return Logic::equiv($this->crossTreeConstraint($rule->children()[0]),
                                $this->crossTreeConstraint($rule->children()[1]));
        if ($op === "imp" && $num === 2)
            return Logic::implies($this->crossTreeConstraint($rule->children()[0]),
                                  $this->crossTreeConstraint($rule->children()[1]));
        if ($op === "conj" && $num === 2)
            return Logic::_and($this->crossTreeConstraint($rule->children()[0]),
                               $this->crossTreeConstraint($rule->children()[1]));
        if ($op === "disj" && $num === 2)
            return Logic::_or($this->crossTreeConstraint($rule->children()[0]),
                              $this->crossTreeConstraint($rule->children()[1]));
        if ($op === "not" && $num === 1)
            return Logic::not($this->crossTreeConstraint($rule->children()[0]));
        if ($op === "var" && $num === 0)
            return Logic::is($this->model->getFeature((string) $rule));

        throw new ConstraintSolverException("unknown operation $op with $num arguments encountered");
    }