Skip to content

DSAIL Language Guide

DSAIL is Jaxon's domain-specific language (DSL) for expressing policy constraints, logical constructs, and other rules that compile to SMT solver inputs. DSAIL is designed to validate compliance with policy requirements by checking for satisfiability (SAT) or unsatisfiability (UNSAT). Each assert statement will be tested independently to see if it holds under possible assignments of variables.

Overview

DSAIL programs consist of:

  • Version: An optional version tag version 1.0;. Omitting this version tag will use the newest interpreter.
  • Variable Declarations: Declare variabels of type boolean, real, integer, symbol.
  • Optional Assignments: Set default, constant, or initial values for variables.
  • Assertions: Define logical constraints, arithmetic expressions, and policy rules to satisfy.
  • Optional Function Definitions: Encapsulate repeated logic or more complex expressions.
  • Optional Quantifiers: Use forAll or exists to express universal or existential constraints.

When compiled, the resulting formula is passed to an SMT solver to check if the constraints are SAT (i.e., they can be satisfied) or UNSAT (they cannot all be satisfied). Each assert statement can be assessed individually and may resolve to TRUE, FALSE, or UNKNOWN.

Handling Unknown Variables

Unbound variables - those not assigned using a let, not provided a value by inference-time questions, or otherwise constrained - may lead to UNKNOWN results. To handle these cases, DSAIL supports completion policies that determine how unknowns are resolved:

  • neutral (default): Leave unknowns as UNKNOWN. Use for general queries or when explicit uncertainty reporting is required.
  • pessimistic: Treat unknowns as violations (FALSE). Best for compliance and safety checks where uncertainty should fail the assertion.
  • optimistic: Treat unknowns as passing (TRUE). Use when you want to give benefit of the doubt.

You can specify a completion policy per assertion using square brackets:

declare age as integer;

// Default (neutral): leaves unknown age as UNKNOWN
assert AgeCheck {
  age >= 18
};

// Neutral policy (explicit)
assert DebugCheck [neutral] {
  test_condition
};

// Pessimistic policy: treats unknown as failure
assert SafetyCheck [pessimistic] {
  safety_score > 0.8
};

// Optimistic policy: treats unknown as passing
assert BestEffortCheck [optimistic] {
  optional_field != ""
};

Recommendation: For compliance and policy checking, always explicitly use [pessimistic] to ensure that uncertain conditions fail rather than pass through undetected. The default [neutral] policy is best for exploratory queries where you want to see what is unknown.

Basic Syntax

  • Statements end with a semicolon (;) unless enclosed in braces (e.g., the assert block).
  • Block statements are in curly braces ({ ... }).
  • Identifiers are alphanumeric and underscores (_).

Example:

version 1.0;
declare x as boolean;
let x = true;

assert myAssertion {
  x
};

Data Types

DSAIL supports the following core types.

  • Boolean: Truth values (true or false).

  • Integer: Integer values (e.g., 0, 42, -3).

  • Real: Floating values (e.g., 3.14, -0.5).

  • Symbol: Fixed values (e.g., "purple"). Used primarily for enumerating collections of values that don't logically map to the above data types.

Collections

DSAIL also includes collections for grouping data:

Arrays

An array in DSAIL is declared with typed keys and typed values, much like an ordered dictionary or map. Each key must be unique, and each entry is accessible by its key.

declare myPrices as array[integer] of real;
  • Key type: In the example above, integer is the type for the array’s indices.
  • Value type: real is the type for the values.

Access is typically done within expressions or assertions by referencing myPrices[key].

Arrays may be used in quantifiers (forAll, exists) by iterating over known keys.

Example Usage

declare myPrices as array[integer] of real;

// Possibly assign a specific index:
let myPrices[0] = 10.99;
let myPrices[1] = 20.50;

assert priceCheck {
  myPrices[0] < myPrices[1]
};

Sets

A set in DSAIL contains a collection of typed elements without repetition. Typically used in quantifiers, membership checks, or cardinality constraints.

declare tenantIDs as set of integer;
  • Element type: integer in the above example.
  • Membership is tested through expressions like x in tenantIDs.
  • Used with forAll(x in tenantIDs, ...) or exists(x in tenantIDs, ...).

Example Usage

declare tenantIDs as set of integer;

assert hasTenants {
  // e.g., the set is not empty
  Exists(x in tenantIDs)
};

assert allPositiveIDs {
  forAll(x in tenantIDs, x > 0)
};

Both arrays and sets allow more advanced constraints (e.g., checking membership, ordering, or cardinalities) depending on the solver features. By default, they offer a straightforward means to group data for quantifier-based rules.

Declarations

Use declare to introduce a new variable and specify its type. The variable is initially unbound (unknown) unless given a default with let.

declare myBool as boolean;
declare myNumber as real;
declare mySymbol as symbol;

Purpose

  • Establishes a typed variable for later usage in assertions or assignments.
  • An unbound variable can unify to any value of its declared type.

Assignment

Use let to assign a value to a previously declared variable. This can be done any time after declare. If omitted, the solver may leave it as unknown, which can still satisfy certain constraints depending on the logic.

let myBool = true;
let myNumber = 42;
let mySymbol = "Large";

Purpose

  • Fixes a variable to a specific value.
  • Overwrites any previous assignment if repeated.

Assertions

Use assert <name> { <formula> } to express a logical formula that must hold for SAT. Each assertion can be viewed independently to check compliance with a specific policy rule.

assert myRule {
  And(myBool, Not(false))
};

Inside the braces

  • You can write logical formulas with And, Or, Not, Imply, etc.
  • If the formula is unsatisfiable, this particular assert fails.
    • Unsatisfiable means there is no possible value that unbound variables could be assigned such that a true value could be returned.

Naming

  • The <name> is an identifier to distinguish this assertion.
  • Helpful for referencing specific rule compliance in results.

Logical Operators

DSAIL provides the standard logical operators, treating them as functions/constraints akin to SMT-LIB or Z3:

  • And(expr1, expr2, ...) Returns true if and only if all expressions are true.

  • Or(expr1, expr2, ...) Returns true if at least one expression is true.

  • Not(expr) Returns the logical negation of expr.

  • Imply(expr1, expr2) Equivalent to (Not(expr1) Or (expr2)). Useful for expressing “if expr1 then expr2.”

  • Distinct(val1, val2, ...) Returns true if all arguments are pairwise different.

Examples

assert rule_with_logic {
  And(
    myBool,
    Or(Not(myBool), true),
    Imply(myBool, myNumber < 50)
  )
};

Relational Operators

Relational operators in DSAIL are typically used for numeric comparisons but also for equality checks on booleans, symbols, etc.

  • Equality: ==
  • Inequality: !=
  • Less than: <
  • Greater than: >
  • Less than or equal: <=
  • Greater than or equal: >=

These appear within assertions or function definitions, for example:

assert numeric_check {
  myNumber <= 100
};

assert equality_check {
  mySymbol == "Apple"
};

Arithmetic

DSAIL supports standard arithmetic operators that mirror those directly supported by SMT solvers like Z3. These can be used in assertions, function bodies, variable assignments, or any context involving numeric expressions.

The following arithmetic operations are available:

  • Addition: +
  • Subtraction: -
  • Multiplication: *
  • Division: / (real division only; integer division must be modeled explicitly).
  • Negation: unary -

All operations are strictly typed. Mixing incompatible types (e.g., int and boolean) is not allowed. Parentheses for grouping are supported.

Example Usage

declare baseRent as real;
declare surcharge as real;
declare tax as real;
declare totalRent as real;

let baseRent = 1200.0;
let surcharge = 150.0;

let totalRent = (baseRent + surcharge) * tax;

assert rentWithinLimit {
  totalRent <= 1400.0 
};

Quantifiers

Quantifiers resemble those in SMT-LIB or first-order logic. They allow you to express constraints over a range or set of values (though domain usage is typically required for meaningful iteration).

  • forAll(variableName in domain, formula) States that formula must hold for every element in domain.

  • exists(variableName in domain, formula) States that there is at least one element in domain for which formula holds.

Example

declare myInt as integer;

domain intDomain = [1, 2, 3, 4]; // example domain definition

assert universal_rule {
  forAll(x in intDomain, x > 0)
};

assert existential_rule {
  exists(x in intDomain, x == 2)
};

Functions

DSAIL supports defining named functions that encapsulate custom or repeated logic. The general form:

function <name>(param1 as Type1, param2 as Type2, ...) as ReturnType {
  // Return a formula or expression
  // e.g., And(), Or(), arithmetic, etc.
};

Inside the function

You write a formula or expression that can include local references to the parameters. The function’s return type must match the expression type.

Usage Example

function isPositive(value as integer) as boolean {
  value > 0
};

assert checkPositivity {
  isPositive(myInt)
};

Example Program

Below is a more complete example illustrating various language features:

declare landlordMentionedPreferNoSection8 as boolean;
declare landlordMentionedAdvertisingNoSection8 as boolean;
declare landlordStatedProposedRent as real;
declare localMarketAverageRent as real;

let localMarketAverageRent = 1000.0;

assert fact_mandatory_acceptance {
  Not(
    Or(
      landlordMentionedPreferNoSection8,
      landlordMentionedAdvertisingNoSection8
    )
  )
};

assert fact_rent_reasonableness {
  landlordStatedProposedRent <= (localMarketAverageRent * 1.1)
};

The following are shown in the above example:

  • Variables declared for a compliance scenario.
  • A default value of 10000.0 set for localMarketAverageRent. Note that this value may be overridden at inference time by an external input.
  • An assertion checking that the landlord has not refused or advertised refusal of Section 8.
    • This assertion will be satisfied if landlordMentionedPreferNoSection8 and landlordMentionedAdvertisingNoSection8 are both False or unbound, as assertions will seek the presence of a possible solution whenever unbound variables are involved. Intuitively, satisfaction is the default and programs should be "oriented" based on this intuition.
  • A rent reasonableness rule comparing the proposed rent to local average.