View Source cure_smt_translator (cure v0.7.0)

Cure SMT-LIB Translator

Translates Cure type constraints and expressions into SMT-LIB format for consumption by external SMT solvers (Z3, CVC5).

Features

  • Full translation of Cure expressions to SMT-LIB s-expressions
  • Type mapping (Int, Nat, Bool, Float to SMT types)
  • Logic inference (QF_LIA, QF_LRA, etc.)
  • Variable declaration generation
  • Assertion generation from constraints

Usage 

% Translate a constraint to SMT-LIB query
Constraint = #binary_op_expr{op = '>', left = var(x), right = lit(0)},
Env = #{x => {type, int}},
Query = cure_smt_translator:generate_query(Constraint, Env).
% => \"(set-logic QF_LIA)\\n(declare-const x Int)\\n(assert (> x 0))\\n(check-sat)\\n\"

Summary

Types

expr()
smt_logic()

Functions

collect_variables(Constraint, Env)

Collect all variables from a constraint.

declare_variable(VarName, Env)

Generate SMT-LIB declaration for a variable.

generate_constraint_check_query(ValueExpr, Predicate, Env)

Generate SMT-LIB query to check if a value satisfies a constraint.

generate_query(Constraint, Env)

Generate a complete SMT-LIB query from a Cure constraint.

generate_query(Constraint, Env, Opts)

Generate SMT-LIB query with options.

generate_refinement_subtype_query(Pred1, Pred2, Var, BaseType)

Generate SMT-LIB query to check refinement type subtyping.

infer_logic(Constraint)

Infer the appropriate SMT-LIB logic for a constraint.

translate_expr(Expr)

Translate a Cure expression to SMT-LIB s-expression.

translate_expr/2

Types

expr()

-type expr() ::
          #literal_expr{value :: term(), location :: term()} |
          #identifier_expr{name :: term(), location :: term()} |
          #function_call_expr{function :: term(), args :: term(), location :: term()} |
          #match_expr{expr :: term(), patterns :: term(), location :: term()} |
          #let_expr{bindings :: term(), body :: term(), location :: term()} |
          #binary_op_expr{op :: term(), left :: term(), right :: term(), location :: term()} |
          #unary_op_expr{op :: term(), operand :: term(), location :: term()} |
          #list_expr{elements :: term(), location :: term()} |
          #vector_expr{elements :: term(), location :: term()} |
          #tuple_expr{elements :: term(), location :: term()} |
          #record_expr{name :: term(), fields :: term(), location :: term()} |
          #field_access_expr{record :: term(), field :: term(), location :: term()} |
          #record_update_expr{name :: term(), base :: term(), fields :: term(), location :: term()} |
          #lambda_expr{params :: term(), body :: term(), location :: term()} |
          #forall_expr{variables :: term(), body :: term(), location :: term()} |
          #exists_expr{variables :: term(), body :: term(), location :: term()} |
          #fsm_spawn_expr{fsm_name :: term(),
                          init_args :: term(),
                          init_state :: term(),
                          location :: term()} |
          #fsm_send_expr{target :: term(), message :: term(), location :: term()} |
          #fsm_receive_expr{patterns :: term(), timeout :: term(), location :: term()} |
          #fsm_state_expr{location :: term()} |
          #melquiades_send_expr{message :: term(), target :: term(), location :: term()} |
          #qualified_call_expr{trait_name :: term(),
                               type_args :: term(),
                               method_name :: term(),
                               receiver :: term(),
                               args :: term(),
                               location :: term()}.

smt_logic()

-type smt_logic() :: 'QF_LIA' | 'QF_LRA' | 'QF_LIRA' | 'QF_NIA' | 'QF_NRA' | 'QF_UFLIA'.

Functions

collect_variables(Constraint, Env)

-spec collect_variables(expr(), map()) -> [atom()].

Collect all variables from a constraint.

Traverses the AST to find all variable references.

Arguments

  • Constraint - Cure AST expression
  • Env - Environment (for type information)

Returns

  • [atom()] - List of variable names (deduplicated)

declare_variable(VarName, Env)

-spec declare_variable(atom(), map()) -> iolist().

Generate SMT-LIB declaration for a variable.

Creates a (declare-const ...) declaration based on the variable's type.

Arguments

  • VarName - Variable name (atom)
  • Env - Environment with type information

Returns

  • iolist() - SMT-LIB declaration

generate_constraint_check_query(ValueExpr, Predicate, Env)

-spec generate_constraint_check_query(expr(), expr(), map()) -> iolist().

Generate SMT-LIB query to check if a value satisfies a constraint.

Arguments

  • ValueExpr - Expression representing the value
  • Predicate - Constraint predicate
  • Env - Environment with variable types

Returns

  • iolist() - SMT-LIB query

Example 

% Check if 5 satisfies (x > 0)
Value = #literal_expr{value = 5},
Pred = #binary_op_expr{op = '>', left = var(x), right = lit(0)},
Query = generate_constraint_check_query(Value, Pred, #{x => {type, int}}).

generate_query(Constraint, Env)

-spec generate_query(expr(), map()) -> iolist().

Generate a complete SMT-LIB query from a Cure constraint.

Produces a full SMT-LIB query including logic declaration, variable declarations, assertions, and check-sat command.

Arguments

  • Constraint - Cure AST expression representing the constraint
  • Env - Environment mapping variables to types

Returns

  • iolist() - SMT-LIB query as iolist (use iolist_to_binary/1 to convert)

Example 

Constraint = #binary_op_expr{op = '+', left = var(x), right = var(y)},
Query = generate_query(Constraint, #{x => {type, int}, y => {type, int}}).

generate_query(Constraint, Env, Opts)

-spec generate_query(expr(), map(), map()) -> iolist().

Generate SMT-LIB query with options.

Options

  • {get_model, boolean()} - Include (get-model) command (default: true)
  • {logic, smt_logic()} - Override logic inference
  • {timeout, integer()} - Solver timeout hint in milliseconds

generate_refinement_subtype_query(Pred1, Pred2, Var, BaseType)

-spec generate_refinement_subtype_query(expr(), expr(), atom(), atom()) -> iolist().

Generate SMT-LIB query to check refinement type subtyping.

Checks if refinement type with predicate Pred1 is a subtype of refinement type with predicate Pred2. This is equivalent to proving: ∀Var. Pred1 => Pred2

Arguments

  • Pred1 - Predicate of subtype (e.g., x > 0)
  • Pred2 - Predicate of supertype (e.g., x /= 0)
  • Var - Refinement variable name
  • BaseType - Base type (int, real, bool)

Returns

  • iolist() - SMT-LIB query

Example 

% Check if Positive <: NonZero
% i.e., ∀x. (x > 0) => (x ≠ 0)
Pred1 = #binary_op_expr{op = '>', left = var(x), right = lit(0)},
Pred2 = #binary_op_expr{op = '/=', left = var(x), right = lit(0)},
Query = generate_refinement_subtype_query(Pred1, Pred2, x, int).

infer_logic(Constraint)

-spec infer_logic(expr()) -> smt_logic().

Infer the appropriate SMT-LIB logic for a constraint.

Analyzes the constraint to determine which SMT-LIB logic is required.

Logics

  • QF_LIA - Quantifier-free linear integer arithmetic
  • QF_LRA - Quantifier-free linear real arithmetic
  • QF_LIRA - Quantifier-free linear integer/real arithmetic
  • QF_NIA - Quantifier-free nonlinear integer arithmetic
  • LIA - Linear integer arithmetic (with quantifiers)
  • LRA - Linear real arithmetic (with quantifiers)
  • NIA - Nonlinear integer arithmetic (with quantifiers)

Arguments

  • Constraint - Cure AST expression

Returns

  • smt_logic() - Inferred logic

translate_expr(Expr)

-spec translate_expr(expr()) -> iolist().

Translate a Cure expression to SMT-LIB s-expression.

Converts Cure AST expressions to SMT-LIB format recursively.

Arguments

  • Expr - Cure AST expression

Returns

  • iolist() - SMT-LIB s-expression

translate_expr/2

-spec translate_expr(expr(), map()) -> iolist().