use crate::ast::{
BinaryOp, Cardinality, Effect, Expr, ExprKind, InvariantAssertion, InvariantDecl,
InvariantQuantifier, Literal, NumericLiteral, TypeRef, UnaryOp,
};
use crate::compiler::{CompiledProgram, ValueType, normalize_name};
use crate::engine::{Input, Query, constant_value, resolve_rule_bindings};
use crate::smtlib::{
SMTLIB_QUERY_SCHEMA_VERSION, SmtLibExportError, SmtLibMetadata, SmtLibQuery, SmtSourceLocation,
SmtSymbol, SmtSymbolEncoding,
};
use crate::value::{
Value, checked_decimal_add, checked_decimal_div, checked_decimal_mul, checked_decimal_sub,
parse_decimal,
};
use chrono::NaiveDate;
use rust_decimal::Decimal;
use serde::{Deserialize, Serialize};
use std::collections::{BTreeMap, BTreeSet};
use std::fmt::Write as _;
use z3::ast::{Ast, Bool, Int};
use z3::{Params, SatResult, Solver, full_version};
const Z3_TIMEOUT_MS: u32 = 5_000;
const FINITE_ARITHMETIC_VALUE_LIMIT: usize = 256;
#[derive(Clone, Copy, Debug, Default, PartialEq, Eq)]
pub enum SolverMode {
#[default]
Auto,
Off,
Z3,
}
#[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize)]
pub struct SolverMetadata {
pub backend: String,
pub version: String,
pub logic: String,
}
pub(crate) enum SolverOutcome {
Proved(SolverMetadata),
Counterexample {
input: Input,
metadata: SolverMetadata,
},
Witness {
input: Input,
metadata: SolverMetadata,
},
Refuted(SolverMetadata),
Unavailable(String),
Unsupported(String),
Unknown(String),
}
#[derive(Clone, Debug, PartialEq, Eq, PartialOrd, Ord)]
struct FieldKey {
binding: String,
field: String,
}
#[derive(Clone)]
enum SymbolInfo {
Bool(Bool),
Int(Int),
Decimal {
scaled: Int,
mantissa: Int,
scale: Int,
},
Enum {
expression: Int,
type_name: String,
variants: Vec<String>,
},
}
#[derive(Clone)]
struct BooleanTerm {
truth: Bool,
conflict: Bool,
}
#[derive(Clone)]
struct IntTerm {
value: Int,
valid: Bool,
bounds: Option<Interval>,
}
#[derive(Clone)]
struct DecimalTerm {
scaled: Int,
valid: Bool,
}
#[derive(Clone, Copy)]
struct Interval {
lower: i128,
upper: i128,
}
impl Interval {
fn within_i64(self) -> bool {
self.lower >= i128::from(i64::MIN) && self.upper <= i128::from(i64::MAX)
}
}
struct CandidateFormula {
rule: String,
value: CandidateValueFormula,
active: Bool,
valid: Bool,
}
#[derive(Clone)]
enum CandidateValueFormula {
Concrete(Value),
Bool(Bool),
Int(Int),
Decimal(Int),
}
struct Translator<'a> {
program: &'a CompiledProgram,
invariant: &'a InvariantDecl,
solver: &'a Solver,
binding_entities: BTreeMap<String, String>,
symbols: BTreeMap<FieldKey, SymbolInfo>,
uses_nonlinear_arithmetic: bool,
}
impl<'a> Translator<'a> {
fn new(
program: &'a CompiledProgram,
invariant: &'a InvariantDecl,
solver: &'a Solver,
) -> Result<Self, String> {
let binding_entities = invariant
.variables
.iter()
.map(|variable| {
(
normalize_name(&variable.name.value),
normalize_name(&variable.ty.value),
)
})
.collect::<BTreeMap<_, _>>();
let mut translator = Self {
program,
invariant,
solver,
binding_entities,
symbols: BTreeMap::new(),
uses_nonlinear_arithmetic: false,
};
translator.declare_supported_fields()?;
Ok(translator)
}
fn declare_supported_fields(&mut self) -> Result<(), String> {
for variable in &self.invariant.variables {
let binding = normalize_name(&variable.name.value);
let entity = self
.program
.entity(&variable.ty.value)
.ok_or_else(|| format!("unknown assertion record `{}`", variable.ty.value))?;
for field in &entity.fields {
if field.optional {
continue;
}
let key = FieldKey {
binding: binding.clone(),
field: normalize_name(&field.name.value),
};
let symbol_name = format!("v{}", self.symbols.len());
let symbol = match &field.ty {
TypeRef::Bool => SymbolInfo::Bool(Bool::new_const(symbol_name)),
TypeRef::Int => SymbolInfo::Int(Int::new_const(symbol_name)),
TypeRef::Decimal => {
let mantissa = Int::new_const(format!("{symbol_name}_mantissa"));
let scale = Int::new_const(format!("{symbol_name}_scale"));
SymbolInfo::Decimal {
scaled: decimal_scaled_expression(&mantissa, &scale),
mantissa,
scale,
}
}
TypeRef::Named(type_name) => {
let declaration = self.program.enum_decl(type_name).ok_or_else(|| {
format!("field `{binding}.{}` is not an enum", field.name.value)
})?;
let variants = declaration
.variants
.iter()
.map(|variant| variant.value.clone())
.collect::<Vec<_>>();
if variants.is_empty() {
return Err(format!(
"enum field `{binding}.{}` has no values",
field.name.value
));
}
SymbolInfo::Enum {
expression: Int::new_const(symbol_name),
type_name: type_name.clone(),
variants,
}
}
TypeRef::String | TypeRef::Date | TypeRef::Duration | TypeRef::Unknown => {
continue;
}
};
match &symbol {
SymbolInfo::Int(expression) => {
let (lower, upper) = int_bounds(field)?;
self.solver.assert(expression.ge(Int::from_i64(lower)));
self.solver.assert(expression.le(Int::from_i64(upper)));
}
SymbolInfo::Decimal {
scaled,
mantissa,
scale,
} => {
let maximum = decimal_mantissa_numeral(Decimal::MAX);
let minimum = decimal_mantissa_numeral(Decimal::MIN);
self.solver.assert(mantissa.ge(minimum));
self.solver.assert(mantissa.le(maximum));
self.solver.assert(scale.ge(Int::from_i64(0)));
self.solver
.assert(scale.le(Int::from_u64(u64::from(Decimal::MAX_SCALE))));
if let Some(range) = &field.range {
let lower = numeric_decimal(&range.start).ok_or_else(|| {
format!("invalid Decimal lower bound for `{}`", field.name.value)
})?;
let upper = numeric_decimal(&range.end).ok_or_else(|| {
format!("invalid Decimal upper bound for `{}`", field.name.value)
})?;
self.solver.assert(scaled.ge(decimal_scaled_numeral(lower)));
self.solver.assert(scaled.le(decimal_scaled_numeral(upper)));
}
if let Some(domain) = &field.domain {
let allowed = domain
.values
.iter()
.map(|expression| {
constant_value(
self.program,
expression,
Some(&TypeRef::Decimal),
)
.and_then(|value| {
match value {
Value::Decimal(value) => {
Ok(Ast::eq(scaled, decimal_scaled_numeral(value)))
}
Value::Int(value) => Ok(Ast::eq(
scaled,
decimal_scaled_numeral(Decimal::from(value)),
)),
_ => Err("Decimal domain contains a non-number".into()),
}
})
})
.collect::<Result<Vec<_>, String>>()?;
self.solver.assert(bool_or(allowed));
}
}
SymbolInfo::Enum {
expression,
variants,
..
} => {
self.solver.assert(expression.ge(Int::from_i64(0)));
self.solver
.assert(expression.lt(Int::from_u64(variants.len() as u64)));
}
SymbolInfo::Bool(_) => {}
}
self.symbols.insert(key, symbol);
}
}
Ok(())
}
fn query_formula(&mut self) -> Result<Bool, String> {
let (decision_name, arguments) = match &self.invariant.assertion {
InvariantAssertion::Cardinality {
decision,
arguments,
..
} => (&decision.value, arguments.as_slice()),
InvariantAssertion::Implication { expectation, .. } => (
&expectation.decision.value,
expectation.arguments.as_slice(),
),
};
let query = Query {
decision: normalize_name(decision_name),
arguments: arguments
.iter()
.map(|argument| match &argument.kind {
ExprKind::Name(name) => Ok(normalize_name(name)),
_ => Err(
"the assertion decision must receive record parameters directly".to_owned(),
),
})
.collect::<Result<Vec<_>, _>>()?,
};
let decision = self
.program
.decision(&query.decision)
.ok_or_else(|| format!("unknown decision `{}`", query.decision))?;
let candidate_rule_names = self
.program
.rules()
.iter()
.filter(|(_, rule)| rule_directly_decides(rule, &query.decision))
.map(|(name, _)| name.clone())
.collect::<BTreeSet<_>>();
let relevant_rules = self
.program
.rules()
.iter()
.filter(|(name, rule)| {
candidate_rule_names.contains(*name)
|| matches!(&rule.effect, Effect::Override { rule, .. }
if candidate_rule_names.contains(&normalize_name(&rule.value)))
})
.map(|(_, rule)| rule)
.collect::<Vec<_>>();
let mut candidates = Vec::new();
let mut overrides = BTreeMap::<String, Vec<Bool>>::new();
let mut query_conflicts = Vec::new();
for rule in relevant_rules {
let parameter_names = rule
.parameters
.iter()
.map(|parameter| normalize_name(¶meter.name.value))
.collect::<BTreeSet<_>>();
if let Effect::Decide {
decision: target,
arguments,
..
} = &rule.effect
{
if normalize_name(&target.value) == query.decision
&& (arguments.len() != query.arguments.len()
|| arguments.iter().any(|argument| {
!matches!(&argument.kind, ExprKind::Name(name)
if parameter_names.contains(&normalize_name(name)))
}))
{
return Err(format!(
"rule `{}` uses a dynamic decision argument",
rule.name.value
));
}
}
let Ok(receivers) =
resolve_rule_bindings(rule, decision, &query, &self.binding_entities)
else {
continue;
};
let condition = self.translate_bool(&rule.condition, &receivers)?;
query_conflicts.push(condition.conflict.clone());
let active = condition.truth;
let rule_name = normalize_name(&rule.name.value);
match &rule.effect {
Effect::Override { rule: target, .. }
if candidate_rule_names.contains(&normalize_name(&target.value)) =>
{
overrides
.entry(normalize_name(&target.value))
.or_default()
.push(active.clone());
}
Effect::Decide {
decision: target,
arguments,
value,
..
} if normalize_name(&target.value) == query.decision
&& effect_matches_query(arguments, &query, &receivers) =>
{
let (value, valid) = self.translate_candidate_value(
value,
&decision.return_type.value,
&receivers,
)?;
query_conflicts.push(bool_and(active.clone(), valid.clone().not()));
candidates.push(CandidateFormula {
rule: rule_name,
value,
active: active.clone(),
valid,
});
}
Effect::Decide { .. } | Effect::Override { .. } | Effect::Invalid { .. } => {}
}
}
let mut present = Vec::new();
for candidate in candidates {
let override_active =
bool_or(overrides.get(&candidate.rule).cloned().unwrap_or_default());
let alive = bool_and(
bool_and(candidate.active, candidate.valid),
override_active.not(),
);
present.push((candidate.value, alive));
}
let any_present = bool_or(present.iter().map(|(_, formula)| formula.clone()).collect());
let gap = any_present.not();
let mut overlaps = Vec::new();
for left in 0..present.len() {
for right in left + 1..present.len() {
let both_alive = bool_and(present[left].1.clone(), present[right].1.clone());
let different = candidate_values_equal(&present[left].0, &present[right].0)?.not();
overlaps.push(bool_and(both_alive, different));
}
}
let overlap = bool_or(overlaps);
let query_conflict = bool_or(query_conflicts);
match &self.invariant.assertion {
InvariantAssertion::Cardinality { cardinality, .. } => {
let cardinality_failure = match cardinality {
Cardinality::ExactlyOne => bool_or(vec![gap, overlap]),
Cardinality::Many if decision.cardinality == Cardinality::Many => {
bool_lit(false)
}
Cardinality::ZeroOrOne | Cardinality::Many => overlap.clone(),
};
let failure = bool_or(vec![query_conflict, cardinality_failure]);
Ok(match self.invariant.quantifier {
InvariantQuantifier::All => failure,
InvariantQuantifier::Some => failure.not(),
})
}
InvariantAssertion::Implication {
condition,
expectation,
..
} => {
let invariant_receivers = self
.binding_entities
.keys()
.map(|binding| (binding.clone(), binding.clone()))
.collect::<BTreeMap<_, _>>();
let premise = self.translate_bool(condition, &invariant_receivers)?;
let expected = constant_value(
self.program,
&expectation.value,
Some(&decision.return_type.value),
)
.map_err(|error| format!("assertion expectation is not constant: {error}"))?;
let expected_present = bool_or(
present
.iter()
.map(|(value, alive)| {
Ok(bool_and(
alive.clone(),
candidate_equals_value(value, &expected)?,
))
})
.collect::<Result<Vec<_>, String>>()?,
);
let conflict = if decision.cardinality == Cardinality::Many {
bool_lit(false)
} else {
overlap.clone()
};
let undefined = if decision.cardinality == Cardinality::ExactlyOne {
gap.clone()
} else {
bool_lit(false)
};
let relation_failure = match expectation.operator {
crate::ast::CompareOp::Equal => expected_present.not(),
crate::ast::CompareOp::NotEqual => expected_present,
};
let bad_result =
bool_or(vec![query_conflict, conflict, undefined, relation_failure]);
Ok(match self.invariant.quantifier {
InvariantQuantifier::All => {
bool_or(vec![premise.conflict, bool_and(premise.truth, bad_result)])
}
InvariantQuantifier::Some => bool_and(
bool_and(premise.conflict.not(), premise.truth),
bad_result.not(),
),
})
}
}
}
fn translate_candidate_value(
&mut self,
expression: &Expr,
expected: &TypeRef,
receivers: &BTreeMap<String, String>,
) -> Result<(CandidateValueFormula, Bool), String> {
match expected {
TypeRef::Bool => {
let value = self.translate_bool(expression, receivers)?;
Ok((
CandidateValueFormula::Bool(value.truth),
value.conflict.not(),
))
}
TypeRef::Int => {
let value = self.translate_int(expression, receivers)?;
Ok((CandidateValueFormula::Int(value.value), value.valid))
}
TypeRef::Decimal => {
let total_on_finite_domain =
self.finite_decimal_values(expression, receivers).is_some();
let value = self.translate_scaled_numeric(expression, receivers)?;
Ok((
CandidateValueFormula::Decimal(value.scaled),
if total_on_finite_domain {
bool_lit(true)
} else {
value.valid
},
))
}
_ => constant_value(self.program, expression, Some(expected))
.map(|value| (CandidateValueFormula::Concrete(value), bool_lit(true)))
.map_err(|error| {
format!(
"dynamic {expected:?} candidate is outside the solver fragment: {error}"
)
}),
}
}
fn translate_bool(
&mut self,
expression: &Expr,
receivers: &BTreeMap<String, String>,
) -> Result<BooleanTerm, String> {
match &expression.kind {
ExprKind::Literal(Literal::Bool(value)) => Ok(boolean_known(bool_lit(*value))),
ExprKind::Literal(Literal::Unknown) => {
Err("`unknown` is outside the solver's total Boolean fragment".into())
}
ExprKind::Field { .. } => {
let (key, field) = self.direct_field(expression, receivers)?;
if field.optional {
return Err(format!(
"optional field `{}.{}` is outside the solver fragment",
key.binding, key.field
));
}
if field.ty != TypeRef::Bool {
return Err(format!("field `{}.{}` is not Bool", key.binding, key.field));
}
match self.symbols.get(&key) {
Some(SymbolInfo::Bool(expression)) => Ok(boolean_known(expression.clone())),
_ => Err(format!(
"missing Bool solver symbol for `{}.{}`",
key.binding, key.field
)),
}
}
ExprKind::Unary {
operator: UnaryOp::Not,
operand,
} => {
let operand = self.translate_bool(operand, receivers)?;
Ok(boolean_not(operand))
}
ExprKind::Binary {
left,
operator: BinaryOp::And,
right,
} => {
let left = self.translate_bool(left, receivers)?;
let right = self.translate_bool(right, receivers)?;
Ok(boolean_and(left, right))
}
ExprKind::Binary {
left,
operator: BinaryOp::Or,
right,
} => {
let left = self.translate_bool(left, receivers)?;
let right = self.translate_bool(right, receivers)?;
Ok(boolean_or(left, right))
}
ExprKind::Binary {
left,
operator:
operator @ (BinaryOp::Equal
| BinaryOp::NotEqual
| BinaryOp::Greater
| BinaryOp::GreaterEqual
| BinaryOp::Less
| BinaryOp::LessEqual),
right,
} => self.translate_comparison(left, *operator, right, receivers),
ExprKind::Call { callee, arguments } => {
let (expression, derive_receivers) =
self.inline_entity_derive(&callee.value, arguments, receivers)?;
self.translate_bool(&expression, &derive_receivers)
}
ExprKind::Binary { .. }
| ExprKind::Unary { .. }
| ExprKind::Literal(_)
| ExprKind::Name(_) => Err("unsupported Boolean expression in solver fragment".into()),
}
}
fn translate_comparison(
&mut self,
left: &Expr,
operator: BinaryOp,
right: &Expr,
receivers: &BTreeMap<String, String>,
) -> Result<BooleanTerm, String> {
let left_type = self
.program
.type_of_span(left.span)
.ok_or_else(|| "missing compiled type for comparison".to_owned())?;
let right_type = self
.program
.type_of_span(right.span)
.ok_or_else(|| "missing compiled type for comparison".to_owned())?;
if matches!(left_type, ValueType::Decimal) || matches!(right_type, ValueType::Decimal) {
if !matches!(left_type, ValueType::Int | ValueType::Decimal)
|| !matches!(right_type, ValueType::Int | ValueType::Decimal)
{
return Err("Decimal comparison requires numeric operands".into());
}
let left = self.translate_scaled_numeric(left, receivers)?;
let right = self.translate_scaled_numeric(right, receivers)?;
return numeric_comparison(
operator,
left.scaled,
left.valid,
right.scaled,
right.valid,
);
}
match left_type {
ValueType::Int => {
if !matches!(right_type, ValueType::Int) {
return Err("mixed numeric comparison is outside the solver fragment".into());
}
let left = self.translate_int(left, receivers)?;
let right = self.translate_int(right, receivers)?;
Ok(numeric_comparison(
operator,
left.value,
left.valid,
right.value,
right.valid,
)?)
}
ValueType::Bool => {
if !matches!(operator, BinaryOp::Equal | BinaryOp::NotEqual) {
return Err("ordered Bool comparison is not supported".into());
}
let left = self.translate_bool(left, receivers)?;
let right = self.translate_bool(right, receivers)?;
let valid = bool_and(left.conflict.not(), right.conflict.not());
let equal = Ast::eq(&left.truth, right.truth);
let truth = if operator == BinaryOp::Equal {
equal
} else {
equal.not()
};
Ok(BooleanTerm {
truth: bool_and(valid.clone(), truth),
conflict: valid.not(),
})
}
ValueType::Enum(type_name) => {
if !matches!(operator, BinaryOp::Equal | BinaryOp::NotEqual) {
return Err("ordered enum comparison is not supported".into());
}
let left = self.translate_enum(left, receivers, type_name)?;
let right = self.translate_enum(right, receivers, type_name)?;
let equal = Ast::eq(&left, right);
Ok(boolean_known(if operator == BinaryOp::Equal {
equal
} else {
equal.not()
}))
}
ValueType::Decimal => unreachable!("Decimal comparisons return above"),
ValueType::String
| ValueType::Date
| ValueType::Duration
| ValueType::Entity(_)
| ValueType::State(_)
| ValueType::Unknown
| ValueType::Error => {
Err("comparison type is outside the solver arithmetic fragment".into())
}
}
}
fn finite_int_values(
&self,
expression: &Expr,
receivers: &BTreeMap<String, String>,
) -> Option<BTreeSet<i64>> {
if !matches!(
self.program.type_of_span(expression.span),
Some(ValueType::Int)
) {
return None;
}
match &expression.kind {
ExprKind::Literal(Literal::Number(NumericLiteral::Int(value))) => {
Some(BTreeSet::from([*value]))
}
ExprKind::Field { .. } => {
let (_, field) = self.direct_field(expression, receivers).ok()?;
if field.optional || field.ty != TypeRef::Int {
return None;
}
if let Some(domain) = &field.domain {
let mut values = BTreeSet::new();
for expression in &domain.values {
let Value::Int(value) =
constant_value(self.program, expression, Some(&TypeRef::Int)).ok()?
else {
return None;
};
values.insert(value);
}
return (values.len() <= FINITE_ARITHMETIC_VALUE_LIMIT).then_some(values);
}
let (lower, upper) = int_bounds(field).ok()?;
let count = i128::from(upper)
.checked_sub(i128::from(lower))?
.checked_add(1)?;
if count < 0 || usize::try_from(count).ok()? > FINITE_ARITHMETIC_VALUE_LIMIT {
return None;
}
Some((lower..=upper).collect())
}
ExprKind::Unary {
operator: UnaryOp::Negate,
operand,
} => {
let mut values = BTreeSet::new();
for value in self.finite_int_values(operand, receivers)? {
values.insert(value.checked_neg()?);
}
Some(values)
}
ExprKind::Binary {
left,
operator: operator @ (BinaryOp::Add | BinaryOp::Subtract | BinaryOp::Multiply),
right,
} => self.finite_int_binary_values(left, *operator, right, receivers),
ExprKind::Call { callee, arguments } => match normalize_name(&callee.value).as_str() {
"min" | "max" => {
let [left, right] = arguments.as_slice() else {
return None;
};
let left_values = self.finite_int_values(left, receivers)?;
let right_values = self.finite_int_values(right, receivers)?;
if left_values.len().checked_mul(right_values.len())?
> FINITE_ARITHMETIC_VALUE_LIMIT
{
return None;
}
let is_max = normalize_name(&callee.value) == "max";
let mut values = BTreeSet::new();
for left in &left_values {
for right in &right_values {
values.insert(if is_max {
(*left).max(*right)
} else {
(*left).min(*right)
});
}
}
Some(values)
}
"abs" => {
let [argument] = arguments.as_slice() else {
return None;
};
let mut values = BTreeSet::new();
for value in self.finite_int_values(argument, receivers)? {
values.insert(value.checked_abs()?);
}
Some(values)
}
_ => {
let (expression, derive_receivers) = self
.inline_entity_derive(&callee.value, arguments, receivers)
.ok()?;
self.finite_int_values(&expression, &derive_receivers)
}
},
_ => None,
}
}
fn finite_int_binary_values(
&self,
left: &Expr,
operator: BinaryOp,
right: &Expr,
receivers: &BTreeMap<String, String>,
) -> Option<BTreeSet<i64>> {
let left_values = self.finite_int_values(left, receivers)?;
let right_values = self.finite_int_values(right, receivers)?;
if left_values.len().checked_mul(right_values.len())? > FINITE_ARITHMETIC_VALUE_LIMIT {
return None;
}
let mut values = BTreeSet::new();
for left in &left_values {
for right in &right_values {
let value = match operator {
BinaryOp::Add => left.checked_add(*right),
BinaryOp::Subtract => left.checked_sub(*right),
BinaryOp::Multiply => left.checked_mul(*right),
_ => return None,
}?;
values.insert(value);
if values.len() > FINITE_ARITHMETIC_VALUE_LIMIT {
return None;
}
}
}
Some(values)
}
fn finite_decimal_values(
&self,
expression: &Expr,
receivers: &BTreeMap<String, String>,
) -> Option<BTreeSet<Decimal>> {
if matches!(
self.program.type_of_span(expression.span),
Some(ValueType::Int)
) {
return self
.finite_int_values(expression, receivers)
.map(|values| values.into_iter().map(Decimal::from).collect());
}
if !matches!(
self.program.type_of_span(expression.span),
Some(ValueType::Decimal)
) {
return None;
}
match &expression.kind {
ExprKind::Literal(Literal::Number(value)) => {
Some(BTreeSet::from([numeric_decimal(value)?]))
}
ExprKind::Field { .. } => {
let (_, field) = self.direct_field(expression, receivers).ok()?;
if field.optional || field.ty != TypeRef::Decimal {
return None;
}
if let Some(domain) = &field.domain {
let mut values = BTreeSet::new();
for expression in &domain.values {
let value =
constant_value(self.program, expression, Some(&TypeRef::Decimal))
.ok()?;
let value = match value {
Value::Decimal(value) => value,
Value::Int(value) => Decimal::from(value),
_ => return None,
};
values.insert(value);
}
return (values.len() <= FINITE_ARITHMETIC_VALUE_LIMIT).then_some(values);
}
let range = field.range.as_ref()?;
let lower = numeric_decimal(&range.start)?;
let upper = numeric_decimal(&range.end)?;
(lower == upper).then(|| BTreeSet::from([lower]))
}
ExprKind::Unary {
operator: UnaryOp::Negate,
operand,
} => {
let mut values = BTreeSet::new();
for value in self.finite_decimal_values(operand, receivers)? {
values.insert(checked_decimal_sub(Decimal::ZERO, value).ok()?);
}
Some(values)
}
ExprKind::Binary {
left,
operator:
operator @ (BinaryOp::Add
| BinaryOp::Subtract
| BinaryOp::Multiply
| BinaryOp::Divide),
right,
} => self.finite_decimal_binary_values(left, *operator, right, receivers),
ExprKind::Call { callee, arguments } => match normalize_name(&callee.value).as_str() {
"min" | "max" => {
let [left, right] = arguments.as_slice() else {
return None;
};
let left_values = self.finite_decimal_values(left, receivers)?;
let right_values = self.finite_decimal_values(right, receivers)?;
if left_values.len().checked_mul(right_values.len())?
> FINITE_ARITHMETIC_VALUE_LIMIT
{
return None;
}
let is_max = normalize_name(&callee.value) == "max";
let mut values = BTreeSet::new();
for left in &left_values {
for right in &right_values {
values.insert(if is_max {
(*left).max(*right)
} else {
(*left).min(*right)
});
}
}
Some(values)
}
"abs" => {
let [argument] = arguments.as_slice() else {
return None;
};
let mut values = BTreeSet::new();
for value in self.finite_decimal_values(argument, receivers)? {
values.insert(if value < Decimal::ZERO {
checked_decimal_sub(Decimal::ZERO, value).ok()?
} else {
value
});
}
Some(values)
}
_ => {
let (expression, derive_receivers) = self
.inline_entity_derive(&callee.value, arguments, receivers)
.ok()?;
self.finite_decimal_values(&expression, &derive_receivers)
}
},
_ => None,
}
}
fn finite_decimal_binary_values(
&self,
left: &Expr,
operator: BinaryOp,
right: &Expr,
receivers: &BTreeMap<String, String>,
) -> Option<BTreeSet<Decimal>> {
let left_values = self.finite_decimal_values(left, receivers)?;
let right_values = self.finite_decimal_values(right, receivers)?;
if left_values.len().checked_mul(right_values.len())? > FINITE_ARITHMETIC_VALUE_LIMIT {
return None;
}
let mut values = BTreeSet::new();
for left in &left_values {
for right in &right_values {
let value = match operator {
BinaryOp::Add => checked_decimal_add(*left, *right),
BinaryOp::Subtract => checked_decimal_sub(*left, *right),
BinaryOp::Multiply => checked_decimal_mul(*left, *right),
BinaryOp::Divide => checked_decimal_div(*left, *right),
_ => return None,
}
.ok()?;
values.insert(value);
if values.len() > FINITE_ARITHMETIC_VALUE_LIMIT {
return None;
}
}
}
Some(values)
}
fn translate_scaled_numeric(
&mut self,
expression: &Expr,
receivers: &BTreeMap<String, String>,
) -> Result<DecimalTerm, String> {
match self.program.type_of_span(expression.span) {
Some(ValueType::Int) => {
let value = self.translate_int(expression, receivers)?;
let scale = power_of_ten(Decimal::MAX_SCALE);
Ok(DecimalTerm {
scaled: Int::mul(&[&value.value, &scale]),
valid: value.valid,
})
}
Some(ValueType::Decimal) => self.translate_decimal(expression, receivers),
_ => Err("expected an Int or Decimal expression".into()),
}
}
fn translate_decimal(
&mut self,
expression: &Expr,
receivers: &BTreeMap<String, String>,
) -> Result<DecimalTerm, String> {
match &expression.kind {
ExprKind::Literal(Literal::Number(value)) => numeric_decimal(value)
.map(|value| DecimalTerm {
scaled: decimal_scaled_numeral(value),
valid: bool_lit(true),
})
.ok_or_else(|| "invalid Decimal literal in solver expression".into()),
ExprKind::Field { .. } => {
let (key, field) = self.direct_field(expression, receivers)?;
if field.optional {
return Err(format!(
"optional field `{}.{}` is outside the solver fragment",
key.binding, key.field
));
}
if field.ty != TypeRef::Decimal {
return Err(format!(
"field `{}.{}` is not Decimal",
key.binding, key.field
));
}
match self.symbols.get(&key) {
Some(SymbolInfo::Decimal { scaled, .. }) => Ok(DecimalTerm {
scaled: scaled.clone(),
valid: bool_lit(true),
}),
_ => Err(format!(
"missing Decimal solver symbol for `{}.{}`",
key.binding, key.field
)),
}
}
ExprKind::Unary {
operator: UnaryOp::Negate,
operand,
} => {
let operand = self.translate_scaled_numeric(operand, receivers)?;
Ok(DecimalTerm {
scaled: operand.scaled.unary_minus(),
valid: operand.valid,
})
}
ExprKind::Call { callee, arguments } => match normalize_name(&callee.value).as_str() {
"min" | "max" => {
self.translate_decimal_min_max(&callee.value, arguments, receivers)
}
"abs" => self.translate_decimal_abs(arguments, receivers),
_ => {
let (expression, derive_receivers) =
self.inline_entity_derive(&callee.value, arguments, receivers)?;
self.translate_scaled_numeric(&expression, &derive_receivers)
}
},
ExprKind::Binary {
left,
operator:
operator @ (BinaryOp::Add
| BinaryOp::Subtract
| BinaryOp::Multiply
| BinaryOp::Divide),
right,
} => self.translate_decimal_arithmetic(left, *operator, right, receivers),
ExprKind::Binary { .. } => {
Err("unsupported Decimal expression in solver fragment".into())
}
_ => Err("unsupported Decimal expression in solver fragment".into()),
}
}
fn translate_decimal_arithmetic(
&mut self,
left: &Expr,
operator: BinaryOp,
right: &Expr,
receivers: &BTreeMap<String, String>,
) -> Result<DecimalTerm, String> {
let left_term = self.translate_scaled_numeric(left, receivers)?;
let right_term = self.translate_scaled_numeric(right, receivers)?;
let operands_valid = bool_and(left_term.valid, right_term.valid);
let scale = power_of_ten(Decimal::MAX_SCALE);
let (scaled, operation_valid) = match operator {
BinaryOp::Add => {
let scaled = Int::add(&[&left_term.scaled, &right_term.scaled]);
let valid = decimal_representable(&scaled);
(scaled, valid)
}
BinaryOp::Subtract => {
let scaled = Int::sub(&[&left_term.scaled, &right_term.scaled]);
let valid = decimal_representable(&scaled);
(scaled, valid)
}
BinaryOp::Multiply => {
if depends_on_input(left, receivers) && depends_on_input(right, receivers) {
self.uses_nonlinear_arithmetic = true;
}
let numerator = Int::mul(&[&left_term.scaled, &right_term.scaled]);
let divisible = Ast::eq(&numerator.modulo(&scale), Int::from_i64(0));
let scaled = numerator.div(&scale);
let valid = bool_and(divisible, decimal_representable(&scaled));
(scaled, valid)
}
BinaryOp::Divide => {
if depends_on_input(right, receivers) {
self.uses_nonlinear_arithmetic = true;
}
let numerator = Int::mul(&[&left_term.scaled, &scale]);
let nonzero = Ast::ne(&right_term.scaled, Int::from_i64(0));
let divisible = Ast::eq(&numerator.modulo(&right_term.scaled), Int::from_i64(0));
let scaled = numerator.div(&right_term.scaled);
let valid = bool_and(nonzero, bool_and(divisible, decimal_representable(&scaled)));
(scaled, valid)
}
_ => return Err("expected Decimal arithmetic".into()),
};
Ok(DecimalTerm {
scaled,
valid: bool_and(operands_valid, operation_valid),
})
}
fn translate_decimal_min_max(
&mut self,
callee: &str,
arguments: &[Expr],
receivers: &BTreeMap<String, String>,
) -> Result<DecimalTerm, String> {
let [left_expression, right_expression] = arguments else {
return Err(format!("builtin `{callee}` expects exactly two arguments"));
};
let left = self.translate_scaled_numeric(left_expression, receivers)?;
let right = self.translate_scaled_numeric(right_expression, receivers)?;
let select_left = if normalize_name(callee) == "max" {
left.scaled.ge(&right.scaled)
} else {
left.scaled.le(&right.scaled)
};
Ok(DecimalTerm {
scaled: select_left.ite(&left.scaled, &right.scaled),
valid: bool_and(left.valid, right.valid),
})
}
fn translate_decimal_abs(
&mut self,
arguments: &[Expr],
receivers: &BTreeMap<String, String>,
) -> Result<DecimalTerm, String> {
let [argument] = arguments else {
return Err("builtin `abs` expects exactly one argument".into());
};
let value = self.translate_scaled_numeric(argument, receivers)?;
let non_negative = value.scaled.ge(Int::from_i64(0));
let negated = value.scaled.unary_minus();
Ok(DecimalTerm {
scaled: non_negative.ite(&value.scaled, &negated),
valid: value.valid,
})
}
fn translate_int(
&mut self,
expression: &Expr,
receivers: &BTreeMap<String, String>,
) -> Result<IntTerm, String> {
match &expression.kind {
ExprKind::Literal(Literal::Number(NumericLiteral::Int(value))) => Ok(IntTerm {
value: Int::from_i64(*value),
valid: bool_lit(true),
bounds: Some(Interval {
lower: i128::from(*value),
upper: i128::from(*value),
}),
}),
ExprKind::Field { .. } => {
let (key, field) = self.direct_field(expression, receivers)?;
if field.optional {
return Err(format!(
"optional field `{}.{}` is outside the solver fragment",
key.binding, key.field
));
}
if field.ty != TypeRef::Int {
return Err(format!("field `{}.{}` is not Int", key.binding, key.field));
}
let Some(SymbolInfo::Int(symbol)) = self.symbols.get(&key) else {
return Err(format!(
"missing Int solver symbol for `{}.{}`",
key.binding, key.field
));
};
let (lower, upper) = int_bounds(field)?;
Ok(IntTerm {
value: symbol.clone(),
valid: bool_lit(true),
bounds: Some(Interval {
lower: i128::from(lower),
upper: i128::from(upper),
}),
})
}
ExprKind::Unary {
operator: UnaryOp::Negate,
operand,
} => {
let value = self.translate_int(operand, receivers)?;
let bounds = value.bounds.and_then(interval_negate);
let operation_valid = int_result_valid(&value.value.unary_minus(), bounds);
Ok(IntTerm {
value: value.value.unary_minus(),
valid: bool_and(value.valid, operation_valid),
bounds,
})
}
ExprKind::Binary {
left,
operator: BinaryOp::Add,
right,
} => {
let left = self.translate_int(left, receivers)?;
let right = self.translate_int(right, receivers)?;
let value = Int::add(&[&left.value, &right.value]);
let bounds = interval_pair(left.bounds, right.bounds, interval_add);
Ok(IntTerm {
valid: bool_and(
bool_and(left.valid, right.valid),
int_result_valid(&value, bounds),
),
value,
bounds,
})
}
ExprKind::Binary {
left,
operator: BinaryOp::Subtract,
right,
} => {
let left = self.translate_int(left, receivers)?;
let right = self.translate_int(right, receivers)?;
let value = Int::sub(&[&left.value, &right.value]);
let bounds = interval_pair(left.bounds, right.bounds, interval_subtract);
Ok(IntTerm {
valid: bool_and(
bool_and(left.valid, right.valid),
int_result_valid(&value, bounds),
),
value,
bounds,
})
}
ExprKind::Binary {
left,
operator: BinaryOp::Multiply,
right,
} => {
if depends_on_input(left, receivers) && depends_on_input(right, receivers) {
self.uses_nonlinear_arithmetic = true;
}
let left = self.translate_int(left, receivers)?;
let right = self.translate_int(right, receivers)?;
let value = Int::mul(&[&left.value, &right.value]);
let bounds = interval_pair(left.bounds, right.bounds, interval_multiply);
Ok(IntTerm {
valid: bool_and(
bool_and(left.valid, right.valid),
int_result_valid(&value, bounds),
),
value,
bounds,
})
}
ExprKind::Binary {
operator: BinaryOp::Divide,
..
} => Err("integer division is outside the exact solver fragment".into()),
ExprKind::Call { callee, arguments } => match normalize_name(&callee.value).as_str() {
"min" | "max" => self.translate_int_min_max(&callee.value, arguments, receivers),
"abs" => self.translate_int_abs(arguments, receivers),
_ => {
let (expression, derive_receivers) =
self.inline_entity_derive(&callee.value, arguments, receivers)?;
self.translate_int(&expression, &derive_receivers)
}
},
_ => Err("unsupported integer expression in solver fragment".into()),
}
}
fn translate_int_min_max(
&mut self,
callee: &str,
arguments: &[Expr],
receivers: &BTreeMap<String, String>,
) -> Result<IntTerm, String> {
let [left_expression, right_expression] = arguments else {
return Err(format!("builtin `{callee}` expects exactly two arguments"));
};
let left = self.translate_int(left_expression, receivers)?;
let right = self.translate_int(right_expression, receivers)?;
let is_max = normalize_name(callee) == "max";
let bounds = interval_min_max(left.bounds, right.bounds, is_max);
let select_left = if is_max {
left.value.ge(&right.value)
} else {
left.value.le(&right.value)
};
Ok(IntTerm {
value: select_left.ite(&left.value, &right.value),
valid: bool_and(left.valid, right.valid),
bounds,
})
}
fn translate_int_abs(
&mut self,
arguments: &[Expr],
receivers: &BTreeMap<String, String>,
) -> Result<IntTerm, String> {
let [argument] = arguments else {
return Err("builtin `abs` expects exactly one argument".into());
};
let value = self.translate_int(argument, receivers)?;
let non_negative = value.value.ge(Int::from_i64(0));
let bounds = value.bounds.and_then(interval_abs);
let operation_valid = if value
.bounds
.is_some_and(|bounds| bounds.lower > i128::from(i64::MIN))
{
bool_lit(true)
} else {
Ast::ne(&value.value, Int::from_i64(i64::MIN))
};
let negated = value.value.unary_minus();
Ok(IntTerm {
value: non_negative.ite(&value.value, &negated),
valid: bool_and(value.valid, operation_valid),
bounds,
})
}
fn translate_enum(
&mut self,
expression: &Expr,
receivers: &BTreeMap<String, String>,
type_name: &str,
) -> Result<Int, String> {
if matches!(expression.kind, ExprKind::Field { .. }) {
let (key, field) = self.direct_field(expression, receivers)?;
if field.optional {
return Err(format!(
"optional field `{}.{}` is outside the solver fragment",
key.binding, key.field
));
}
return match self.symbols.get(&key) {
Some(SymbolInfo::Enum { expression, .. }) => Ok(expression.clone()),
_ => Err(format!(
"missing enum solver symbol for `{}.{}`",
key.binding, key.field
)),
};
}
let value = constant_value(
self.program,
expression,
Some(&TypeRef::Named(type_name.to_owned())),
)?;
let Value::Enum { variant, .. } = value else {
return Err("expected an enum constant".into());
};
let declaration = self
.program
.enum_decl(type_name)
.ok_or_else(|| format!("unknown enum `{type_name}`"))?;
let index = declaration
.variants
.iter()
.position(|candidate| normalize_name(&candidate.value) == normalize_name(&variant))
.ok_or_else(|| format!("unknown `{type_name}` variant `{variant}`"))?;
Ok(Int::from_u64(index as u64))
}
fn direct_field<'b>(
&self,
expression: &Expr,
receivers: &BTreeMap<String, String>,
) -> Result<(FieldKey, &'b crate::ast::FieldDecl), String>
where
'a: 'b,
{
let ExprKind::Field { receiver, field } = &expression.kind else {
return Err("expected a direct field access".into());
};
let ExprKind::Name(receiver_name) = &receiver.kind else {
return Err("indirect field receivers are outside the solver fragment".into());
};
let receiver_name = normalize_name(receiver_name);
let binding = receivers.get(&receiver_name).ok_or_else(|| {
format!("receiver `{receiver_name}` is not bound to an assertion record parameter")
})?;
let entity = self
.binding_entities
.get(binding)
.ok_or_else(|| format!("binding `{binding}` has no assertion record type"))?;
let declaration = self
.program
.field(entity, &field.value)
.ok_or_else(|| format!("unknown field `{}`", field.value))?;
Ok((
FieldKey {
binding: binding.clone(),
field: normalize_name(&field.value),
},
declaration,
))
}
fn inline_entity_derive(
&self,
name: &str,
arguments: &[Expr],
receivers: &BTreeMap<String, String>,
) -> Result<(Expr, BTreeMap<String, String>), String> {
let derive = self
.program
.derive(name)
.cloned()
.ok_or_else(|| format!("function `{name}` is outside the solver fragment"))?;
if derive.parameters.len() != arguments.len() {
return Err(format!("fn `{name}` has an incompatible argument count"));
}
let mut mapped = receivers.clone();
let mut scalar_arguments = BTreeMap::new();
for (parameter, argument) in derive.parameters.iter().zip(arguments) {
if self.program.entity(¶meter.ty.value).is_none() {
scalar_arguments.insert(normalize_name(¶meter.name.value), argument.clone());
continue;
}
let ExprKind::Name(argument_name) = &argument.kind else {
return Err(format!(
"fn `{name}` must receive record parameters directly for solver inlining"
));
};
let binding = receivers
.get(&normalize_name(argument_name))
.ok_or_else(|| format!("fn `{name}` argument is not a bound record"))?;
mapped.insert(normalize_name(¶meter.name.value), binding.clone());
}
Ok((
substitute_scalar_arguments(&derive.expression, &scalar_arguments),
mapped,
))
}
fn materialize_input(&self) -> Result<Input, String> {
let solver_model = self
.solver
.get_model()
.ok_or_else(|| "Z3 did not return a model".to_owned())?;
let mut model = BTreeMap::new();
for (key, symbol) in &self.symbols {
let value = match symbol {
SymbolInfo::Bool(expression) => Value::Bool(
solver_model
.eval(expression, true)
.and_then(|value| value.as_bool())
.ok_or_else(|| "solver returned a non-Bool model value".to_owned())?,
),
SymbolInfo::Int(expression) => Value::Int(
solver_model
.eval(expression, true)
.and_then(|value| value.as_i64())
.ok_or_else(|| "solver returned an out-of-range Int".to_owned())?,
),
SymbolInfo::Decimal {
mantissa, scale, ..
} => {
let mantissa = solver_model
.eval(mantissa, true)
.ok_or_else(|| "solver omitted a Decimal mantissa".to_owned())?;
let mantissa = z3_int_i128(&mantissa)
.ok_or_else(|| "solver returned an invalid Decimal mantissa".to_owned())?;
let scale = solver_model
.eval(scale, true)
.and_then(|value| value.as_u64())
.and_then(|value| u32::try_from(value).ok())
.filter(|value| *value <= Decimal::MAX_SCALE)
.ok_or_else(|| "solver returned an invalid Decimal scale".to_owned())?;
let value = Decimal::try_from_i128_with_scale(mantissa, scale)
.map_err(|error| format!("solver Decimal is not representable: {error}"))?;
Value::decimal(value)
}
SymbolInfo::Enum {
expression,
type_name,
variants,
} => {
let index = solver_model
.eval(expression, true)
.and_then(|value| value.as_u64())
.and_then(|value| usize::try_from(value).ok())
.filter(|index| *index < variants.len())
.ok_or_else(|| "solver returned an invalid enum index".to_owned())?;
Value::Enum {
type_name: type_name.clone(),
variant: variants[index].clone(),
}
}
};
model.insert(key.clone(), value);
}
let mut input = Input::new();
for variable in &self.invariant.variables {
let binding = normalize_name(&variable.name.value);
let entity = self
.program
.entity(&variable.ty.value)
.ok_or_else(|| format!("unknown record `{}`", variable.ty.value))?;
let mut fields = BTreeMap::new();
for field in &entity.fields {
let key = FieldKey {
binding: binding.clone(),
field: normalize_name(&field.name.value),
};
if let Some(value) = model.get(&key) {
fields.insert(field.name.value.clone(), value.clone());
} else if !field.optional {
fields.insert(
field.name.value.clone(),
default_field_value(self.program, field)?,
);
}
}
input.insert(&variable.name.value, &variable.ty.value, fields);
}
Ok(input)
}
fn exported_symbols(&self) -> Result<Vec<SmtSymbol>, String> {
let mut symbols = self
.symbols
.iter()
.map(|(key, symbol)| {
let entity = self.binding_entities.get(&key.binding).ok_or_else(|| {
format!(
"solver symbol `{}.{}` has no assertion record",
key.binding, key.field
)
})?;
let field = self.program.field(entity, &key.field).ok_or_else(|| {
format!(
"solver symbol `{}.{}` has no compiled field",
key.binding, key.field
)
})?;
let encoding = match symbol {
SymbolInfo::Bool(expression) => SmtSymbolEncoding::Bool {
symbol: expression.to_string(),
},
SymbolInfo::Int(expression) => SmtSymbolEncoding::Int {
symbol: expression.to_string(),
},
SymbolInfo::Decimal {
mantissa, scale, ..
} => SmtSymbolEncoding::DecimalMantissaScale {
mantissa_symbol: mantissa.to_string(),
scale_symbol: scale.to_string(),
canonical_scale: Decimal::MAX_SCALE,
},
SymbolInfo::Enum {
expression,
type_name,
variants,
} => SmtSymbolEncoding::EnumIndex {
symbol: expression.to_string(),
type_name: type_name.clone(),
variants: variants.clone(),
},
};
Ok(SmtSymbol {
binding: key.binding.clone(),
entity: entity.clone(),
field: key.field.clone(),
encoding,
source: source_location(self.program, field.span),
})
})
.collect::<Result<Vec<_>, String>>()?;
symbols.sort_by(|left, right| {
symbol_ordinal(&left.encoding)
.cmp(&symbol_ordinal(&right.encoding))
.then_with(|| left.binding.cmp(&right.binding))
.then_with(|| left.field.cmp(&right.field))
});
Ok(symbols)
}
}
pub(crate) fn export_invariant_smtlib(
program: &CompiledProgram,
invariant_name: &str,
) -> Result<SmtLibQuery, SmtLibExportError> {
let invariant =
program
.invariant(invariant_name)
.ok_or_else(|| SmtLibExportError::UnknownInvariant {
invariant: invariant_name.to_owned(),
})?;
let solver = Solver::new();
let mut translator = Translator::new(program, invariant, &solver).map_err(|reason| {
SmtLibExportError::Unsupported {
invariant: invariant.name.value.clone(),
reason,
}
})?;
let query_formula =
translator
.query_formula()
.map_err(|reason| SmtLibExportError::Unsupported {
invariant: invariant.name.value.clone(),
reason,
})?;
let logic = if translator.uses_nonlinear_arithmetic {
"QF_NIA"
} else {
"QF_LIA"
};
let symbols =
translator
.exported_symbols()
.map_err(|reason| SmtLibExportError::Unsupported {
invariant: invariant.name.value.clone(),
reason,
})?;
solver.assert(query_formula);
let serialized = solver.to_smt2();
if serialized.trim().is_empty() {
return Err(SmtLibExportError::Unsupported {
invariant: invariant.name.value.clone(),
reason: "Z3 could not serialize the translated query as SMT-LIB2".into(),
});
}
let query_kind = match invariant.quantifier {
InvariantQuantifier::All => "invariant_violation",
InvariantQuantifier::Some => "invariant_witness",
};
let script = render_smtlib_script(
&invariant.name.value,
logic,
query_kind,
&symbols,
&serialized,
);
Ok(SmtLibQuery {
invariant: invariant.name.value.clone(),
source: source_location(program, invariant.span),
metadata: SmtLibMetadata {
schema_version: SMTLIB_QUERY_SCHEMA_VERSION.into(),
generator: "tess".into(),
generator_version: env!("CARGO_PKG_VERSION").into(),
logic: logic.into(),
query: query_kind.into(),
},
symbols,
script,
})
}
pub(crate) fn solve_invariant(
program: &CompiledProgram,
invariant: &InvariantDecl,
mode: SolverMode,
) -> SolverOutcome {
if mode == SolverMode::Off {
return SolverOutcome::Unavailable("embedded solver use is disabled".into());
}
let solver = Solver::new();
let mut params = Params::new();
params.set_u32("timeout", Z3_TIMEOUT_MS);
solver.set_params(¶ms);
let mut translator = match Translator::new(program, invariant, &solver) {
Ok(translator) => translator,
Err(error) => return SolverOutcome::Unsupported(error),
};
let query_formula = match translator.query_formula() {
Ok(query_formula) => query_formula,
Err(error) => return SolverOutcome::Unsupported(error),
};
let metadata = SolverMetadata {
backend: "z3".into(),
version: full_version().to_owned(),
logic: if translator.uses_nonlinear_arithmetic {
"QF_NIA".into()
} else {
"QF_LIA".into()
},
};
solver.assert(&query_formula);
match (invariant.quantifier, solver.check()) {
(InvariantQuantifier::All, SatResult::Unsat) => SolverOutcome::Proved(metadata),
(InvariantQuantifier::All, SatResult::Sat) => match translator.materialize_input() {
Ok(input) => SolverOutcome::Counterexample { input, metadata },
Err(error) => SolverOutcome::Unknown(error),
},
(InvariantQuantifier::Some, SatResult::Unsat) => SolverOutcome::Refuted(metadata),
(InvariantQuantifier::Some, SatResult::Sat) => match translator.materialize_input() {
Ok(input) => SolverOutcome::Witness { input, metadata },
Err(error) => SolverOutcome::Unknown(error),
},
(_, SatResult::Unknown) => SolverOutcome::Unknown(
solver
.get_reason_unknown()
.unwrap_or_else(|| "Z3 returned unknown or reached its timeout".to_owned()),
),
}
}
fn render_smtlib_script(
invariant: &str,
logic: &str,
query_kind: &str,
symbols: &[SmtSymbol],
body: &str,
) -> String {
let invariant = smt_comment_value(invariant);
let body = canonicalize_z3_local_names(body.trim_start());
let mut output = String::new();
writeln!(output, "; Tess SMT-LIB query").expect("writing to a String cannot fail");
writeln!(output, "; schema: {SMTLIB_QUERY_SCHEMA_VERSION}")
.expect("writing to a String cannot fail");
writeln!(output, "; generator: tess {}", env!("CARGO_PKG_VERSION"))
.expect("writing to a String cannot fail");
writeln!(output, "; assertion: {invariant}").expect("writing to a String cannot fail");
let semantics = match query_kind {
"invariant_violation" => "sat means assertion violation",
"invariant_witness" => "sat means assertion witness",
_ => "sat means query target is reachable",
};
writeln!(output, "; semantics: {semantics}").expect("writing to a String cannot fail");
for symbol in symbols {
writeln!(
output,
"; symbol: {} -> {}.{} ({}.{}) @ {}:{}:{}",
encoding_symbol_names(&symbol.encoding),
smt_comment_value(&symbol.binding),
smt_comment_value(&symbol.field),
smt_comment_value(&symbol.entity),
smt_comment_value(&symbol.field),
smt_comment_value(&symbol.source.file),
symbol.source.line,
symbol.source.column
)
.expect("writing to a String cannot fail");
}
writeln!(output, "(set-logic {logic})").expect("writing to a String cannot fail");
output.push_str(&body);
output
}
fn encoding_symbol_names(encoding: &SmtSymbolEncoding) -> String {
match encoding {
SmtSymbolEncoding::Bool { symbol }
| SmtSymbolEncoding::Int { symbol }
| SmtSymbolEncoding::EnumIndex { symbol, .. } => symbol.clone(),
SmtSymbolEncoding::DecimalMantissaScale {
mantissa_symbol,
scale_symbol,
..
} => format!("{mantissa_symbol},{scale_symbol}"),
}
}
fn canonicalize_z3_local_names(body: &str) -> String {
let bytes = body.as_bytes();
let mut names = BTreeMap::<String, String>::new();
let mut output = String::with_capacity(body.len());
let mut cursor = 0;
while cursor < bytes.len() {
if bytes[cursor] == b'$' && bytes.get(cursor + 1) == Some(&b'x') {
let mut end = cursor + 2;
while bytes.get(end).is_some_and(u8::is_ascii_digit) {
end += 1;
}
if end > cursor + 2 {
let original = &body[cursor..end];
let next_index = names.len();
let canonical = names
.entry(original.to_owned())
.or_insert_with(|| format!("$t{next_index}"));
output.push_str(canonical);
cursor = end;
continue;
}
}
let character = body[cursor..]
.chars()
.next()
.expect("cursor is within the string");
output.push(character);
cursor += character.len_utf8();
}
output
}
fn smt_comment_value(value: &str) -> String {
value.replace(['\r', '\n'], " ")
}
fn source_location(program: &CompiledProgram, span: crate::source::Span) -> SmtSourceLocation {
let source = program.source();
let (line, column) = source.line_col(span.start);
SmtSourceLocation {
file: source.name_at(span.start).to_owned(),
span: source.local_span(span).unwrap_or(span),
line,
column,
}
}
fn primary_symbol(encoding: &SmtSymbolEncoding) -> &str {
match encoding {
SmtSymbolEncoding::Bool { symbol }
| SmtSymbolEncoding::Int { symbol }
| SmtSymbolEncoding::EnumIndex { symbol, .. } => symbol,
SmtSymbolEncoding::DecimalMantissaScale {
mantissa_symbol, ..
} => mantissa_symbol,
}
}
fn symbol_ordinal(encoding: &SmtSymbolEncoding) -> usize {
let symbol = primary_symbol(encoding);
let digits = symbol
.strip_prefix('v')
.unwrap_or(symbol)
.chars()
.take_while(char::is_ascii_digit)
.collect::<String>();
digits.parse().unwrap_or(usize::MAX)
}
fn comparison(operator: BinaryOp, left: Int, right: Int) -> Result<Bool, String> {
Ok(match operator {
BinaryOp::Equal => Ast::eq(&left, right),
BinaryOp::NotEqual => Ast::ne(&left, right),
BinaryOp::Greater => left.gt(right),
BinaryOp::GreaterEqual => left.ge(right),
BinaryOp::Less => left.lt(right),
BinaryOp::LessEqual => left.le(right),
_ => return Err("expected a comparison operator".into()),
})
}
fn candidate_values_equal(
left: &CandidateValueFormula,
right: &CandidateValueFormula,
) -> Result<Bool, String> {
match (left, right) {
(CandidateValueFormula::Concrete(left), CandidateValueFormula::Concrete(right)) => {
Ok(bool_lit(left == right))
}
(CandidateValueFormula::Bool(left), CandidateValueFormula::Bool(right)) => {
Ok(Ast::eq(left, right))
}
(CandidateValueFormula::Int(left), CandidateValueFormula::Int(right))
| (CandidateValueFormula::Decimal(left), CandidateValueFormula::Decimal(right)) => {
Ok(Ast::eq(left, right))
}
_ => Err("candidate values have incompatible solver representations".into()),
}
}
fn candidate_equals_value(
candidate: &CandidateValueFormula,
expected: &Value,
) -> Result<Bool, String> {
match (candidate, expected) {
(CandidateValueFormula::Concrete(candidate), expected) => {
Ok(bool_lit(candidate == expected))
}
(CandidateValueFormula::Bool(candidate), Value::Bool(expected)) => {
Ok(Ast::eq(candidate, Bool::from_bool(*expected)))
}
(CandidateValueFormula::Int(candidate), Value::Int(expected)) => {
Ok(Ast::eq(candidate, Int::from_i64(*expected)))
}
(CandidateValueFormula::Decimal(candidate), Value::Decimal(expected)) => {
Ok(Ast::eq(candidate, decimal_scaled_numeral(*expected)))
}
(CandidateValueFormula::Decimal(candidate), Value::Int(expected)) => Ok(Ast::eq(
candidate,
decimal_scaled_numeral(Decimal::from(*expected)),
)),
_ => Err("expected value has an incompatible solver representation".into()),
}
}
fn numeric_comparison(
operator: BinaryOp,
left: Int,
left_valid: Bool,
right: Int,
right_valid: Bool,
) -> Result<BooleanTerm, String> {
let valid = bool_and(left_valid, right_valid);
let truth = comparison(operator, left, right)?;
Ok(BooleanTerm {
truth: bool_and(valid.clone(), truth),
conflict: valid.not(),
})
}
fn boolean_known(truth: Bool) -> BooleanTerm {
BooleanTerm {
truth,
conflict: bool_lit(false),
}
}
fn boolean_not(value: BooleanTerm) -> BooleanTerm {
BooleanTerm {
truth: bool_and(value.conflict.clone().not(), value.truth.not()),
conflict: value.conflict,
}
}
fn boolean_and(left: BooleanTerm, right: BooleanTerm) -> BooleanTerm {
let right_false = bool_and(right.conflict.clone().not(), right.truth.clone().not());
let conflict = bool_or(vec![
bool_and(left.conflict.clone(), right_false.not()),
bool_and(left.truth.clone(), right.conflict),
]);
BooleanTerm {
truth: bool_and(left.truth, right.truth),
conflict,
}
}
fn boolean_or(left: BooleanTerm, right: BooleanTerm) -> BooleanTerm {
let left_false = bool_and(left.conflict.clone().not(), left.truth.clone().not());
let conflict = bool_or(vec![
bool_and(left.conflict, right.truth.clone().not()),
bool_and(left_false, right.conflict),
]);
BooleanTerm {
truth: bool_or(vec![left.truth, right.truth]),
conflict,
}
}
fn interval_pair(
left: Option<Interval>,
right: Option<Interval>,
operation: fn(Interval, Interval) -> Option<Interval>,
) -> Option<Interval> {
operation(left?, right?)
}
fn interval_negate(value: Interval) -> Option<Interval> {
Some(Interval {
lower: value.upper.checked_neg()?,
upper: value.lower.checked_neg()?,
})
}
fn interval_add(left: Interval, right: Interval) -> Option<Interval> {
Some(Interval {
lower: left.lower.checked_add(right.lower)?,
upper: left.upper.checked_add(right.upper)?,
})
}
fn interval_subtract(left: Interval, right: Interval) -> Option<Interval> {
Some(Interval {
lower: left.lower.checked_sub(right.upper)?,
upper: left.upper.checked_sub(right.lower)?,
})
}
fn interval_multiply(left: Interval, right: Interval) -> Option<Interval> {
let products = [
left.lower.checked_mul(right.lower)?,
left.lower.checked_mul(right.upper)?,
left.upper.checked_mul(right.lower)?,
left.upper.checked_mul(right.upper)?,
];
Some(Interval {
lower: *products.iter().min().expect("four products"),
upper: *products.iter().max().expect("four products"),
})
}
fn interval_min_max(
left: Option<Interval>,
right: Option<Interval>,
is_max: bool,
) -> Option<Interval> {
let left = left?;
let right = right?;
Some(if is_max {
Interval {
lower: left.lower.max(right.lower),
upper: left.upper.max(right.upper),
}
} else {
Interval {
lower: left.lower.min(right.lower),
upper: left.upper.min(right.upper),
}
})
}
fn interval_abs(value: Interval) -> Option<Interval> {
let lower_abs = value.lower.checked_abs()?;
let upper_abs = value.upper.checked_abs()?;
Some(Interval {
lower: if value.lower <= 0 && value.upper >= 0 {
0
} else {
lower_abs.min(upper_abs)
},
upper: lower_abs.max(upper_abs),
})
}
fn int_result_valid(value: &Int, bounds: Option<Interval>) -> Bool {
if bounds.is_some_and(Interval::within_i64) {
bool_lit(true)
} else {
int_representable(value)
}
}
fn int_representable(value: &Int) -> Bool {
bool_and(
value.ge(Int::from_i64(i64::MIN)),
value.le(Int::from_i64(i64::MAX)),
)
}
fn decimal_representable(scaled: &Int) -> Bool {
let maximum_mantissa = decimal_mantissa_numeral(Decimal::MAX);
let mut alternatives = Vec::with_capacity((Decimal::MAX_SCALE + 1) as usize);
for removed_scale in 0..=Decimal::MAX_SCALE {
let power = power_of_ten(removed_scale);
let limit = Int::mul(&[&maximum_mantissa, &power]);
let divisible = Ast::eq(&scaled.modulo(&power), Int::from_i64(0));
let in_range = bool_and(scaled.ge(limit.unary_minus()), scaled.le(limit));
alternatives.push(bool_and(divisible, in_range));
}
bool_or(alternatives)
}
fn bool_lit(value: bool) -> Bool {
Bool::from_bool(value)
}
fn bool_and(left: Bool, right: Bool) -> Bool {
Bool::and(&[left, right])
}
fn bool_or(mut formulas: Vec<Bool>) -> Bool {
match formulas.len() {
0 => bool_lit(false),
1 => formulas.pop().expect("one Boolean formula"),
_ => Bool::or(&formulas),
}
}
fn effect_matches_query(
arguments: &[Expr],
query: &Query,
receivers: &BTreeMap<String, String>,
) -> bool {
arguments.len() == query.arguments.len()
&& arguments
.iter()
.zip(&query.arguments)
.all(|(argument, query_binding)| {
let ExprKind::Name(parameter) = &argument.kind else {
return false;
};
receivers.get(&normalize_name(parameter)) == Some(&normalize_name(query_binding))
})
}
fn rule_directly_decides(rule: &crate::ast::RuleDecl, decision: &str) -> bool {
matches!(&rule.effect, Effect::Decide { decision: target, .. }
if normalize_name(&target.value) == decision)
}
fn depends_on_input(expression: &Expr, receivers: &BTreeMap<String, String>) -> bool {
match &expression.kind {
ExprKind::Field { .. } => true,
ExprKind::Name(name) => receivers.contains_key(&normalize_name(name)),
ExprKind::Call { arguments, .. } => arguments
.iter()
.any(|argument| depends_on_input(argument, receivers)),
ExprKind::Unary { operand, .. } => depends_on_input(operand, receivers),
ExprKind::Binary { left, right, .. } => {
depends_on_input(left, receivers) || depends_on_input(right, receivers)
}
ExprKind::Literal(_) => false,
}
}
fn substitute_scalar_arguments(expression: &Expr, arguments: &BTreeMap<String, Expr>) -> Expr {
let argument = match &expression.kind {
ExprKind::Name(name) => arguments.get(&normalize_name(name)),
_ => None,
};
if let Some(argument) = argument {
return argument.clone();
}
let mut substituted = expression.clone();
match &mut substituted.kind {
ExprKind::Field { receiver, .. } => {
**receiver = substitute_scalar_arguments(receiver, arguments);
}
ExprKind::Call {
arguments: call_arguments,
..
} => {
for argument in call_arguments {
*argument = substitute_scalar_arguments(argument, arguments);
}
}
ExprKind::Unary { operand, .. } => {
**operand = substitute_scalar_arguments(operand, arguments);
}
ExprKind::Binary { left, right, .. } => {
**left = substitute_scalar_arguments(left, arguments);
**right = substitute_scalar_arguments(right, arguments);
}
ExprKind::Literal(_) | ExprKind::Name(_) => {}
}
substituted
}
fn int_bounds(field: &crate::ast::FieldDecl) -> Result<(i64, i64), String> {
let Some(range) = &field.range else {
return Ok((i64::MIN, i64::MAX));
};
let (NumericLiteral::Int(lower), NumericLiteral::Int(upper)) = (&range.start, &range.end)
else {
return Err(format!(
"Int field `{}` has non-integer bounds",
field.name.value
));
};
Ok((*lower, *upper))
}
fn default_field_value(
program: &CompiledProgram,
field: &crate::ast::FieldDecl,
) -> Result<Value, String> {
Ok(match &field.ty {
TypeRef::Bool => Value::Bool(false),
TypeRef::Int => {
let (lower, upper) = int_bounds(field)?;
Value::Int(lower.max(0).min(upper))
}
TypeRef::Decimal => {
let value = field
.range
.as_ref()
.and_then(|range| numeric_decimal(&range.start))
.unwrap_or(Decimal::ZERO);
Value::decimal(value)
}
TypeRef::String => Value::String(String::new()),
TypeRef::Date => {
Value::Date(NaiveDate::from_ymd_opt(1970, 1, 1).expect("valid epoch date"))
}
TypeRef::Duration => Value::Duration(0),
TypeRef::Named(type_name) => {
let variant = program
.enum_decl(type_name)
.and_then(|declaration| declaration.variants.first())
.ok_or_else(|| format!("field `{}` has no enum values", field.name.value))?;
Value::Enum {
type_name: type_name.clone(),
variant: variant.value.clone(),
}
}
TypeRef::Unknown => {
return Err(format!(
"field `{}` has an unresolved type",
field.name.value
));
}
})
}
fn power_of_ten(exponent: u32) -> Int {
let numeral = format!("1{}", "0".repeat(exponent as usize));
numeral
.parse()
.expect("a power of ten is a valid Z3 integer")
}
fn decimal_mantissa_numeral(value: Decimal) -> Int {
value
.mantissa()
.to_string()
.parse()
.expect("a Decimal mantissa is a valid Z3 integer")
}
fn decimal_scaled_expression(mantissa: &Int, scale: &Int) -> Int {
let mut expression = mantissa.clone();
for candidate_scale in (0..Decimal::MAX_SCALE).rev() {
let factor = power_of_ten(Decimal::MAX_SCALE - candidate_scale);
let candidate = Int::mul(&[mantissa, &factor]);
let selected = Ast::eq(scale, Int::from_u64(u64::from(candidate_scale)));
expression = selected.ite(&candidate, &expression);
}
expression
}
fn decimal_scaled_numeral(value: Decimal) -> Int {
let value = value.normalize();
let mantissa = value.mantissa();
if mantissa == 0 {
return Int::from_i64(0);
}
let mut magnitude = mantissa.unsigned_abs().to_string();
magnitude.extend(std::iter::repeat_n(
'0',
(Decimal::MAX_SCALE - value.scale()) as usize,
));
let numeral = if mantissa.is_negative() {
format!("-{magnitude}")
} else {
magnitude
};
numeral
.parse()
.expect("a scaled Decimal is a valid Z3 integer")
}
fn z3_int_i128(value: &Int) -> Option<i128> {
let rendered = value.to_string();
if let Ok(value) = rendered.parse() {
return Some(value);
}
rendered
.strip_prefix("(- ")?
.strip_suffix(')')?
.parse::<i128>()
.ok()?
.checked_neg()
}
fn numeric_decimal(literal: &NumericLiteral) -> Option<Decimal> {
match literal {
NumericLiteral::Int(value) => Some(Decimal::from(*value)),
NumericLiteral::Decimal(value) => parse_decimal(value).ok(),
}
}
#[cfg(test)]
mod tests {
use super::*;
use crate::SourceFile;
fn compile_text(source: &str) -> CompiledProgram {
let output = crate::compile_source(SourceFile::new("solver.tes", source));
assert!(
!output.has_errors(),
"{}",
output
.diagnostics
.iter()
.map(|diagnostic| diagnostic.message.as_str())
.collect::<Vec<_>>()
.join("; ")
);
output.program.expect("compiled solver fixture")
}
fn intervals() -> Vec<Interval> {
(-3_i128..=3)
.flat_map(|lower| (lower..=3).map(move |upper| Interval { lower, upper }))
.collect()
}
fn values(interval: Interval) -> impl Iterator<Item = i128> {
interval.lower..=interval.upper
}
#[test]
fn interval_arithmetic_matches_small_exhaustive_oracles() {
for left in intervals() {
let negated = interval_negate(left).unwrap();
let expected = values(left).map(|value| -value).collect::<Vec<_>>();
assert_eq!(negated.lower, *expected.iter().min().unwrap());
assert_eq!(negated.upper, *expected.iter().max().unwrap());
let absolute = interval_abs(left).unwrap();
let expected = values(left).map(i128::abs).collect::<Vec<_>>();
assert_eq!(absolute.lower, *expected.iter().min().unwrap());
assert_eq!(absolute.upper, *expected.iter().max().unwrap());
for right in intervals() {
let pairs = || {
values(left).flat_map(move |left| values(right).map(move |right| (left, right)))
};
for (actual, expected) in [
(
interval_add(left, right).unwrap(),
pairs()
.map(|(left, right)| left + right)
.collect::<Vec<_>>(),
),
(
interval_subtract(left, right).unwrap(),
pairs()
.map(|(left, right)| left - right)
.collect::<Vec<_>>(),
),
(
interval_multiply(left, right).unwrap(),
pairs()
.map(|(left, right)| left * right)
.collect::<Vec<_>>(),
),
(
interval_min_max(Some(left), Some(right), false).unwrap(),
pairs()
.map(|(left, right)| left.min(right))
.collect::<Vec<_>>(),
),
(
interval_min_max(Some(left), Some(right), true).unwrap(),
pairs()
.map(|(left, right)| left.max(right))
.collect::<Vec<_>>(),
),
] {
assert_eq!(actual.lower, *expected.iter().min().unwrap());
assert_eq!(actual.upper, *expected.iter().max().unwrap());
}
}
}
}
#[test]
fn interval_overflow_drops_the_optimization_instead_of_wrapping() {
let maximum = Interval {
lower: i128::MAX,
upper: i128::MAX,
};
let minimum = Interval {
lower: i128::MIN,
upper: i128::MIN,
};
assert!(interval_add(maximum, Interval { lower: 1, upper: 1 }).is_none());
assert!(interval_subtract(minimum, Interval { lower: 1, upper: 1 }).is_none());
assert!(interval_multiply(maximum, Interval { lower: 2, upper: 2 }).is_none());
assert!(interval_negate(minimum).is_none());
assert!(interval_abs(minimum).is_none());
assert!(
Interval {
lower: i128::from(i64::MIN),
upper: i128::from(i64::MAX),
}
.within_i64()
);
assert!(!maximum.within_i64());
assert!(!minimum.within_i64());
}
#[test]
fn existential_cardinality_returns_a_witness_or_exact_refutation() {
let satisfiable = compile_text(
r"mod SomeSolver
enum Result:
Yes
record E:
x: Int 0..2
dec d(e E) -> Result
policy::yes @yes policy:
A value of one produces Yes.
rule yes(e E):
e.x = 1 => d(e) = Yes
assert some reachable(e E):
d(e)
",
);
let invariant = satisfiable.invariant("reachable").unwrap();
let SolverOutcome::Witness { input, metadata } =
solve_invariant(&satisfiable, invariant, SolverMode::Z3)
else {
panic!("expected an existential witness")
};
assert_eq!(metadata.logic, "QF_LIA");
assert_eq!(input.bindings["e"].fields["x"], Value::Int(1));
let impossible = compile_text(
r"mod SomeSolver
enum Result:
Yes
record E:
x: Int 0..2
dec d(e E) -> Result
assert some reachable(e E):
d(e)
",
);
assert!(matches!(
solve_invariant(
&impossible,
impossible.invariant("reachable").unwrap(),
SolverMode::Z3
),
SolverOutcome::Refuted(_)
));
}
#[test]
fn existential_implication_requires_a_true_premise_and_good_result() {
let impossible = compile_text(
r"mod SomeSolver
enum Result:
No
record E:
x: Int 0..1
dec d(e E) -> Result
policy::false_premise @false premise:
Only zero produces No.
rule only_false_premise(e E):
e.x = 0 => d(e) = No
assert some reachable(e E):
e.x > 0 => d(e) = No
",
);
assert!(matches!(
solve_invariant(
&impossible,
impossible.invariant("reachable").unwrap(),
SolverMode::Z3
),
SolverOutcome::Refuted(_)
));
let satisfiable = compile_text(
r"mod SomeSolver
enum Result:
No
Yes
record E:
x: Int 0..2
dec d(e E) -> Result
policy::result @result policy:
Zero produces No and one produces Yes.
rule no(e E):
e.x = 0 => d(e) = No
rule yes(e E):
e.x = 1 => d(e) = Yes
assert some reachable(e E):
e.x > 0 => d(e) = Yes
",
);
let SolverOutcome::Witness { input, .. } = solve_invariant(
&satisfiable,
satisfiable.invariant("reachable").unwrap(),
SolverMode::Z3,
) else {
panic!("expected a non-vacuous implication witness")
};
assert_eq!(input.bindings["e"].fields["x"], Value::Int(1));
}
#[test]
fn implication_treats_an_empty_optional_decision_as_not_equal() {
let program = compile_text(
r"mod Solver
enum Result:
Yes
record E:
x: Int 0..1
dec d(e E) -> Result?
assert universal(e E):
true => d(e) != Yes
assert some existential(e E):
true => d(e) != Yes
",
);
assert!(matches!(
solve_invariant(
&program,
program.invariant("universal").unwrap(),
SolverMode::Z3
),
SolverOutcome::Proved(_)
));
assert!(matches!(
solve_invariant(
&program,
program.invariant("existential").unwrap(),
SolverMode::Z3
),
SolverOutcome::Witness { .. }
));
}
#[test]
fn finite_decimal_totality_elides_expensive_validity_formula() {
let exact = compile_text(
r"mod Solver
record E:
amount: Decimal {1.0, 2.0}
rate: Decimal {0.25, 0.50}
split: Int 1..2
hold: Bool
fn payout(amount Decimal, rate Decimal, split Int) -> Decimal:
amount * rate / split
dec d(e E) -> Decimal?
policy::payout @payout policy:
Available payouts use the declared formula.
rule available(e E):
not e.hold => d(e) = payout(e.amount, e.rate, e.split)
assert safe(e E):
d(e)?
",
);
let query = export_invariant_smtlib(&exact, "safe").unwrap();
assert_eq!(query.metadata.logic, "QF_NIA");
assert!(
!query.script.contains("(mod "),
"a proved-finite candidate should not retain Decimal validity moduli\n{}",
query.script
);
assert!(matches!(
solve_invariant(&exact, exact.invariant("safe").unwrap(), SolverMode::Z3),
SolverOutcome::Proved(_)
));
let inexact = compile_text(
r"mod Solver
record E:
amount: Decimal {1.0}
split: Int 3..3
hold: Bool
fn payout(amount Decimal, split Int) -> Decimal:
amount / split
dec d(e E) -> Decimal?
policy::payout @payout policy:
Available payouts use division.
rule available(e E):
not e.hold => d(e) = payout(e.amount, e.split)
assert safe(e E):
d(e)?
",
);
let query = export_invariant_smtlib(&inexact, "safe").unwrap();
assert!(query.script.contains("(mod "));
let SolverOutcome::Counterexample { input, .. } =
solve_invariant(&inexact, inexact.invariant("safe").unwrap(), SolverMode::Z3)
else {
panic!("an inexact finite Decimal combination must remain a conflict")
};
assert!(
crate::analysis::replay_invariant_violation(&inexact, "safe", &input)
.unwrap()
.is_some()
);
let partially_invalid = compile_text(
r"mod Solver
record E:
amount: Decimal {1.0}
split: Int 0..1
hold: Bool
fn payout(amount Decimal, split Int) -> Decimal:
(amount / split) * 0
dec d(e E) -> Decimal?
policy::payout @payout policy:
Available payouts may divide by zero.
rule available(e E):
not e.hold => d(e) = payout(e.amount, e.split)
assert safe(e E):
d(e)?
",
);
let SolverOutcome::Counterexample { input, .. } = solve_invariant(
&partially_invalid,
partially_invalid.invariant("safe").unwrap(),
SolverMode::Z3,
) else {
panic!("an invalid inner division must not be hidden by multiplication by zero")
};
assert!(
crate::analysis::replay_invariant_violation(&partially_invalid, "safe", &input)
.unwrap()
.is_some()
);
let over_limit = compile_text(
r"mod Solver
record E:
amount: Decimal {1.0}
offset: Int 0..256
hold: Bool
fn payout(amount Decimal, offset Int) -> Decimal:
amount + offset
dec d(e E) -> Decimal?
policy::payout @payout policy:
Available payouts add an offset.
rule available(e E):
not e.hold => d(e) = payout(e.amount, e.offset)
assert safe(e E):
d(e)?
",
);
let query = export_invariant_smtlib(&over_limit, "safe").unwrap();
assert!(
query.script.contains("(mod "),
"257 finite values must retain the bounded symbolic fallback"
);
}
#[test]
fn existential_decimal_product_uses_exact_nonlinear_arithmetic() {
let program = compile_text(
r"mod SomeSolver
enum Result:
Yes
record E:
left: Decimal 0.0..2.0
right: Decimal 0.0..2.0
dec d(e E) -> Result
policy::product @product policy:
A product of two produces Yes.
rule product(e E):
e.left * e.right = 2.0 => d(e) = Yes
assert some reachable(e E):
d(e)
",
);
let SolverOutcome::Witness { input, metadata } = solve_invariant(
&program,
program.invariant("reachable").unwrap(),
SolverMode::Z3,
) else {
panic!("expected a nonlinear Decimal witness")
};
assert_eq!(metadata.logic, "QF_NIA");
let left = input.bindings["e"].fields["left"]
.as_decimal()
.expect("Decimal left field");
let right = input.bindings["e"].fields["right"]
.as_decimal()
.expect("Decimal right field");
assert_eq!(left.checked_mul(right), Some(Decimal::from(2)));
}
}