## BooleanFunctions Module

This module implements functions for generating some special boolean functions like arithmetic circuits for addition, subtraction, multiplication, threshold functions, the hidden weighted bit functions, the queen's problem, and the pigeonhole problems.

### Functions and values

 Function or value Description  ComputePrimeNumbers m  Full Usage: ComputePrimeNumbers m Parameters: m : int Returns: Set compute prime numbers up to number m m : int Returns: Set  MkBitmatrix x m n  Full Usage: MkBitmatrix x m n Parameters: x : string m : int n : int Returns: BoolExpr[][] Make a nxn-bit matrix with variables names xij where x is given as argument x : string m : int n : int Returns: BoolExpr[][]  MkBitvector x n  Full Usage: MkBitvector x n Parameters: x : string n : int Returns: BoolExpr[] Make a n-bit vector with variables names xi where x is given as argument x : string n : int Returns: BoolExpr[]  MkClique3 x  Full Usage: MkClique3 x Parameters: x : BoolExpr[][] Returns: BoolExpr This formula lists all directed graphs that have a triangle. x : BoolExpr[][] Returns: BoolExpr  MkDirectStorageAccess x y  Full Usage: MkDirectStorageAccess x y Parameters: x : BoolExpr[] y : BoolExpr[] Returns: BoolExpr DirectStorageAccess: Interpret variables x as an address adr given as a binary number and select bit y[adr] of the vector y x : BoolExpr[] y : BoolExpr[] Returns: BoolExpr  MkExactlyKofN k x  Full Usage: MkExactlyKofN k x Parameters: k : int x : BoolExpr[] Returns: BoolExpr This function computes the boolean formula that holds iff exactly k of the formulas in the given bitvector hold. k : int x : BoolExpr[] Returns: BoolExpr  MkHiddenWeightedBit n  Full Usage: MkHiddenWeightedBit n Parameters: n : int Returns: BoolExpr This function computes the hidden weighted bit function which has only exponentially sized BDDs. It is the disjunction of all formulas x[k] & (MkExactlyKofN (k+1) x) for k in [0..n-1] where n is the length of x, and moreover at least one of the x[i] must hold. n : int Returns: BoolExpr  MkListNatAdd x  Full Usage: MkListNatAdd x Parameters: x : BoolExpr[][] Returns: BoolExpr[] Generate the propositional formulas for the sum bits of the addition of m different n-bit radix-2 numbers (given as rows of a matrix x). x : BoolExpr[][] Returns: BoolExpr[]  MkMultiples k x  Full Usage: MkMultiples k x Parameters: k : int x : BoolExpr[] Returns: BoolExpr generate a boolean expression on variables x that is satisfiable iff the assignment to x represents a multiple of k as a radix-2 number k : int x : BoolExpr[] Returns: BoolExpr  MkNatAdd x y  Full Usage: MkNatAdd x y Parameters: x : BoolExpr[] y : BoolExpr[] Returns: BoolExpr[] Generate the propositional formulas for the sum bits of the addition of the radix-2 numbers given as the arguments (as boolean variables). x : BoolExpr[] y : BoolExpr[] Returns: BoolExpr[]  MkNatLes x y  Full Usage: MkNatLes x y Parameters: x : BoolExpr[] y : BoolExpr[] Returns: BoolExpr Generate the propositional formula to check x x : BoolExpr[] y : BoolExpr[] Returns: BoolExpr  MkNatMul x y  Full Usage: MkNatMul x y Parameters: x : BoolExpr[] y : BoolExpr[] Returns: BoolExpr[] This function computes the circuit for radix-2 multiplication x : BoolExpr[] y : BoolExpr[] Returns: BoolExpr[]  MkNatSub x y  Full Usage: MkNatSub x y Parameters: x : BoolExpr[] y : BoolExpr[] Returns: BoolExpr[] Generate the propositional formulas for the sum bits of the subtraction of the radix-2 numbers given as the arguments (as boolean variables). x : BoolExpr[] y : BoolExpr[] Returns: BoolExpr[]  MkPopulationCount x  Full Usage: MkPopulationCount x Parameters: x : BoolExpr[] Returns: BoolExpr[] This function computes the population count, i.e., the number of bits that are true as radix-2 number with the minimal number of bits. x : BoolExpr[] Returns: BoolExpr[]  MkPrime x  Full Usage: MkPrime x Parameters: x : BoolExpr[] Returns: BoolExpr generate a boolean expression on variables x that is satisfiable iff the assignment to x represents a prime number as a radix-2 number x : BoolExpr[] Returns: BoolExpr  MkSquares x  Full Usage: MkSquares x Parameters: x : BoolExpr[] Returns: BoolExpr generate a boolean expression on variables x that is satisfiable iff the assignment to x represents a square number as a radix-2 number x : BoolExpr[] Returns: BoolExpr  MkThresholdMoreThanK k x  Full Usage: MkThresholdMoreThanK k x Parameters: k : int x : BoolExpr[] Returns: BoolExpr This function computes the threshold function, i.e., the generated formula holds iff k k : int x : BoolExpr[] Returns: BoolExpr  NatSetToBoolExpr x s  Full Usage: NatSetToBoolExpr x s Parameters: x : BoolExpr[] s : Set Returns: BoolExpr convert numbers in set s to a boolean expression assuming that all elements can be represented as radix-2 number with the bits from x x : BoolExpr[] s : Set Returns: BoolExpr  ZeroExtend x n  Full Usage: ZeroExtend x n Parameters: x : BoolExpr[] n : int Returns: BoolExpr[] ZeroExtend adds n false bits as most significant bits to extend the length of a bitvector without changing its value as a radix-2 number. x : BoolExpr[] n : int Returns: BoolExpr[]  pigeonhole N  Full Usage: pigeonhole N Parameters: N : int Returns: BoolExpr pigeonhole P N states that N : int Returns: BoolExpr  queen N  Full Usage: queen N Parameters: N : int Returns: BoolExpr compute propositional logic formula to state that N queens can be placed on a NxN board such that none can beat any other one. N : int Returns: BoolExpr