Conditionals and Implications#

The modelling layer supports two important modifier operations:

  • .only_if(literal)

  • .implies(target)

Conditional Enforcement: only_if()#

only_if(lit) means “enforce this constraint only when lit is true”.

Supported on:

  • hermax.model.Literal

  • hermax.model.Clause

  • hermax.model.ClauseGroup

  • hermax.model.PBConstraint

Examples:

# If g is true, enforce (a OR b)
gated_clause = (a | b).only_if(g)

# If g is true, enforce a PB inequality
gated_pb = (2 * a + b <= 2).only_if(g)

Chaining gates is supported and remains sound:

chained = (a | b).only_if(g1).only_if(g2)
# Meaning: (g1 AND g2) -> (a OR b)

Implication: implies()#

src.implies(dst) is implemented as a safe form of half-reification.

Supported source forms#

  • hermax.model.Literal

  • hermax.model.Clause

  • hermax.model.PBConstraint

Unsupported source forms#

  • hermax.model.ClauseGroup