smt

type ADTField struct {
	Name string // Accessor name (auto-generated if not specified)
	Sort string // SMT-LIB sort name
}

type ADTVariant struct {
	Name   string
	Fields []ADTField
}

type CalleeDef struct {
	Name    string
	SMTLib  string // The (define-fun ...) declaration
	ADTDecl string // Any ADT declarations needed (may be empty)
}

type CalleeInfo struct {
	Name       string
	Params     []FunctionParam
	Body       core.CoreExpr
	ReturnSort string
	ADTTypes   map[string][]ADTVariant
}

type EncodeFunctionOpts struct {
	// Program is the full Core program (needed for resolving cross-function calls).
	Program *core.Program
	// SurfaceParams maps function names to their parameter info.
	SurfaceParams map[string][]FunctionParam
	// SurfaceReturnSorts maps function names to their return sort strings.
	SurfaceReturnSorts map[string]string
	// ReturnType is the function's return type (used to discover record types in return position).
	ReturnType types.Type
	// Body is the function body expression (used to discover record types constructed in the body).
	Body core.CoreExpr
	// Contracts are the function's contracts (used to discover record types in ensures clauses).
	Contracts []*core.Contract
	// RecursiveDepth enables bounded recursion unrolling at the given depth (1-10).
	// When > 0 and the function is self-recursive, generates a define-fun chain
	// instead of rejecting. 0 means no unrolling (default behavior).
	RecursiveDepth int
	// HOFInlineDepth controls the unrolling depth for HOF specializations
	// (map, filter, foldl with literal lambda arguments). When > 0, inlinable
	// HOF calls are specialized into recursive functions and unrolled.
	// Default: 3 if not specified and HOF calls are detected.
	HOFInlineDepth int
	// ExtraDeclarations are additional SMT-LIB declarations to prepend
	// (e.g., record types found in ADT constructor fields that need
	// to be declared before the ADT itself).
	ExtraDeclarations []string
	// RecordTypeAliases maps named record type aliases (e.g., "TableCell", "Point")
	// to their TRecord types. These are pre-registered during record type collection
	// so that named sorts take priority over anonymous Record_field1_field2 sorts.
	RecordTypeAliases map[string]*types.TRecord
}

type EncodeResult struct {
	// SMTLib is the complete SMT-LIB program text.
	SMTLib string
	// Declarations are the type/constant declarations.
	Declarations []string
	// Assertions are the assert statements.
	Assertions []string
	// BodyExpr is the encoded function body expression.
	BodyExpr string
}

type FunctionParam struct {
	Name string
	Type types.Type
}

type HOFKind int

type InlinableHOFCall struct {
	Kind    HOFKind
	Lambda  *core.Lambda  // The literal lambda argument
	ListArg core.CoreExpr // The list argument
	InitVal core.CoreExpr // Only for foldl: the initial accumulator value
	// Original is the original App node for replacement
	Original *core.App
}

type InlineResult struct {
	// NewBody is the modified function body with HOF calls replaced
	// by calls to specialized recursive functions.
	NewBody core.CoreExpr
	// Specializations are the unrolled recursive function declarations.
	Specializations []SpecializationResult
}

type ListBuiltinSpec struct {
	Op           string // SMT-LIB operator name
	Unary        bool   // Single argument
	AppendZero   bool   // Append literal 0 as extra argument
	ConsMode     bool   // First arg wrapped in (seq.unit ...)
	ContainsMode bool   // Second arg wrapped in (seq.unit ...) for element containment
	TernaryMode  bool   // Three arguments (e.g., seq.extract xs offset length)
	TailMode     bool   // _list_tail: (seq.extract xs 1 (- (seq.len xs) 1))
}

type ModelBinding struct {
	Name  string `json:"name"`
	Sort  string `json:"sort"`
	Value string `json:"value"`
}

type NumericBuiltinSpec struct {
	Op    string // SMT-LIB operator name (to_real, to_int)
	Unary bool   // Always true for conversions
}

type RecordTypeInfo struct {
	SortName   string            // SMT-LIB sort name (e.g., "Point")
	CtorName   string            // Constructor name (e.g., "mk_Point")
	FieldNames []string          // Sorted field names
	FieldSorts map[string]string // Field name → SMT-LIB sort
}

type RejectionCode string

type SMTContext struct {
	// Declarations accumulates SMT-LIB type declarations.
	Declarations []string
	// Variables maps AILANG parameter names to their SMT-LIB types.
	Variables map[string]string
	// DeclaredTypes tracks which ADT types have been declared.
	DeclaredTypes map[string]bool
	// ResolvedCallees tracks function names that have been resolved
	// as define-fun declarations for cross-function call support.
	ResolvedCallees map[string]bool
}

type SMTRejectionReason struct {
	Code     RejectionCode
	Message  string
	Location string // Source location if available
	Hint     string // Suggestion to make it encodable
}

type SolverConfig struct {
	Z3Path  string        // Path to z3 binary (auto-discovered if empty)
	Timeout time.Duration // Per-function timeout (default 5s)
}

type SolverResult struct {
	Status    SolverStatus
	Model     []ModelBinding // Populated when Status == StatusCounterexample
	Duration  time.Duration
	SMTLib    string // The input SMT-LIB program (for --verbose)
	RawOutput string // Raw Z3 stdout
	Error     string // Error message if Status == StatusError
}

type SolverStatus int

type SpecializationResult struct {
	// Declarations are the SMT-LIB declare-fun/define-fun chain.
	Declarations []string
	// TopLevelName is the top-level unrolled function name.
	TopLevelName string
	// Kind is which HOF was specialized.
	Kind HOFKind
}

type StringBuiltinSpec struct {
	Op         string // SMT-LIB operator name
	FlipArgs   bool   // Swap arg order (e.g., gt → lt with flipped args)
	Unary      bool   // Single argument
	AppendZero bool   // Append literal 0 as extra argument
	SubstrMode bool   // Convert (s, start, end) → (str.substr s start (- end start))
}

type UnrollConfig struct {
	FuncName   string          // Name of the recursive function
	Params     []FunctionParam // Function parameters
	Body       core.CoreExpr   // Original function body
	ReturnSort string          // SMT-LIB return sort
	Depth      int             // Unrolling depth (1-10)
}

type UnrollResult struct {
	// Declarations contains the declare-fun (level 0) and define-fun (levels 1..N).
	Declarations []string
	// TopLevelName is the name of the deepest unrolling (funcName_N).
	TopLevelName string
}