, поэтому я экспериментирую с boolector , и я достиг точки, где у меня есть N число BoolectorNode, представляющее N другую формулу. Я хотел бы иметь функцию, которая гарантирует, что минимум 0 и максимум N-1 формулы верны одновременно. Я представляю, что с помощью некоторых циклов я могу достичь этого, но мне было интересно, если бы я использовал какую-то ранее существующую функцию, доступную в boolector, я мог бы достичь этого легко.