Arithmetic for Mace4

The command set(arithmetic) builds some integer arithmetic into Mace4. It tells Mace4 to interpret several function and predicate symbols as operations and relations over the integers.

The following tables list the supported symbols for integer arithmetic.

Operations Relations

Symbol	Meaning
`+`	Sum
`*`	Product
`-`	Negation
`/`	Integer Division
`mod`	modulus operator*
`min`	Minimum
`max`	Maximum
`abs`	Absolute Value

Symbol	Meaning
`=`	Equal
`<`	Less than
`<=`	Less than or equal
`>`	Greater than
`>=`	Greater than or equal

*The modulus operation is different from C's remainder operation "%" when either of the operands is negative. In fact, C's "%" operation is not defined for negative operands. In Mace4, (-14 mod 5) = 1, (14 mod -5) = -1, and (-14 mod -5) = -4.

Note that - cannot be used as a binary subtraction operation (because LADR does not allow arity-overloading of symbols). Instead of x-y, one must write x+ -y.

Recall that when Mace4 is searching for a model of size n, it is using the set {0,1,...,n-1} as the underlying domain of the model. When set(arithmetic) is in effect, the integer operations and relations are applied to the elements of the domain. However, when evaluating integer expressions, Mace4 is free to go outside of the domain, including negative integers. For example, the constraint A+ -B = C+ -D has A=C=1, B=D=3 as a solution (among many others), and the constraint A + B = 10 is valid for domain sizes less than 10.

However, when assigning possible values to uninterpreted functions and constants (e.g., unknowns A and B), Mace4 will use members of the domain only. For example, given the constraint A + B = 10 with a domain size of 8, Mace4 will not give the solution A=9, B=1.

Division by Zero

Mace4 cannot simply fail (i.e., backtrack and try other values) when it comes to an expression involving division (or mod) by zero, because such expressions can be valid and lead to solutions.

Case 1: some other subexpression validates a formula; for example, 3/0 = 2 | 1+4=5 is valid.

Case 2: instances of x = x; for example, 3/0 = 3/0 is valid. Given an arithmetic equality alpha = beta involving division by zero, Mace4 will simplify it by using ring theory identities, and if simplify(alpha) is identical to simplify(beta), the equation evaluates to TRUE. The simplification procedure is not guaranteed to produce a unique canonical form such that the simplified expressions are identical if alpha = beta. Thus, Mace4 can be incompelte for constraints involving division by zero; that is, it might say that there are no solutions when there are valid solutions. However, we believe that Mace4 is sound; that is, all solutions that it gives are valid.

Arithmetic Changes Parse/Print Properties

When set(arithmetic) is in effect, Mace4 automatically changes the parse/print properties of the arithmetic operations so that arithmetic expressions can be written in a more conventional way. The properties are changed as follows.

  op(490, infix_right, "+").
  op(470, infix_right, "*").
  op(460, infix, "/").
  op(460, infix, "mod").
  op(390, prefix, "-").

These declarations allow, for example, the expression (a * (b * c)) + (d + e) to be written as a * b * c + d + e. When in doubt, include parentheses and observe how Mace4 echoes the formulas in the output file.

Examples

mace4 -n8 -f queens1.in > queens1.out

mace4 -n8 -f queens2.in > queens2.out

mace4 -f send-money.in > send-money.out

mace4 -f zebra2.in > zebra2.out

mace4 -f kenken6.in > kenken6.out

Next Section: Interpformat