Add linearization solver for [-1,1] coefficient templates

[moratorium08]

Implement a linearization-based solver that converts polynomial constraints into pure LIA constraints for efficient SMT solving when the number of coefficient variables exceeds the blasting threshold (>10 variables).

Key changes:

• Add polynomial expansion (distribute multiplication over addition)
• Add cubic simplification (c³ = c for c ∈ {-1, 0, 1})
• Add LinearizationContext for managing auxiliary variables
• Add linearize_term to replace products with aux vars
• Add solve_by_linearization as alternative to solve_by_blasting
• Add --force-linearization CLI flag and HOICE_FORCE_LINEARIZATION env var
• Add 29 unit tests covering expansion, linearization, and edge cases

🤖 Generated with Claude Code

[Copilot]

Pull request overview

This PR implements a linearization-based solver for polynomial constraints involving coefficient template variables in the range [-1, 1]. The solver is designed as an alternative to the existing bit-blasting approach when the number of coefficient variables exceeds 10, converting polynomial constraints with products into Linear Integer Arithmetic (LIA) constraints by introducing auxiliary variables.

Key changes:

• Adds polynomial expansion with cubic simplification (c³ = c for c ∈ {-1, 0, 1})
• Introduces auxiliary variables for products (c² → c2, c*d → c_d) with appropriate constraints
• Provides --force-linearization CLI flag for debugging/testing

Reviewed changes

Copilot reviewed 2 out of 2 changed files in this pull request and generated 5 comments.

File	Description
src/common/config.rs	Adds force_linearization configuration field and CLI argument with environment variable support (HOICE_FORCE_LINEARIZATION)
src/absadt/learn.rs	Implements polynomial expansion, linearization logic with auxiliary variable management, solver integration, and 29 unit tests for expansion and linearization functionality

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

[Copilot]

The variable processed is created and populated but never read. It appears to be intended to track which coefficient variables have been handled as squared terms, but this information isn't used. Consider removing this unused variable to improve code clarity.

Suggested change

	let mut processed: HashSet<VarIdx> = HashSet::new();
	for (&idx, &count) in &counts {
	if count >= 2 {
	// c² → c2 (squared variable)
	let c2 = ctx.get_or_create_squared(idx);
	result_coef_terms.push(term::var(c2, typ::int()));
	processed.insert(idx);
	for (&idx, &count) in &counts {
	if count >= 2 {
	// c² → c2 (squared variable)
	let c2 = ctx.get_or_create_squared(idx);
	result_coef_terms.push(term::var(c2, typ::int()));

[Copilot]

Missing test coverage for linearization of products with three or more distinct coefficient variables (e.g., cde). The existing tests cover ccd (squared plus single) but not the case where all variables are distinct. This would help validate whether the implementation correctly handles N-ary products.

[Copilot]

The pairwise linearization approach for products of more than two coefficient variables may produce non-linear results. For example, with three coefficient variables c, d, e appearing as cde, the code creates c_d for cd and keeps e separate, resulting in c_de. However, c_d is itself a coefficient-like variable (constrained to {-1,0,1}), so c_d*e remains a non-linear product of two coefficient variables. Consider either: (1) recursively applying linearization until all products involve at most one coefficient variable, or (2) handling N-ary products by creating auxiliary variables for all combinations, not just pairs.

Suggested change

	// Handle squared terms (c² → c2)
	let mut processed: HashSet<VarIdx> = HashSet::new();
	for (&idx, &count) in &counts {
	if count >= 2 {
	// c² → c2 (squared variable)
	let c2 = ctx.get_or_create_squared(idx);
	result_coef_terms.push(term::var(c2, typ::int()));
	processed.insert(idx);
	}
	}
	// For single occurrences, we need to handle products
	let single_vars: Vec<VarIdx> = counts
	.iter()
	.filter(|(_, &c)| c == 1)
	.map(|(&idx, _)| idx)
	.collect();
	if single_vars.len() >= 2 {
	// Create product variables for pairs
	let mut i = 0;
	while i + 1 < single_vars.len() {
	let c = single_vars[i];
	let d = single_vars[i + 1];
	let c_d = ctx.get_or_create_product(c, d);
	result_coef_terms.push(term::var(c_d, typ::int()));
	i += 2;
	}
	// If odd number, keep the last one
	if i < single_vars.len() {
	result_coef_terms.push(term::var(single_vars[i], typ::int()));
	}
	} else if single_vars.len() == 1 {
	result_coef_terms.push(term::var(single_vars[0], typ::int()));
	// Collect all coefficient-like variables arising in this product:
	// - squared terms (c² → c2), and
	// - singly-occurring coefficient variables.
	let mut coef_like_vars: Vec<VarIdx> = Vec::new();
	// Handle squared terms (c² → c2)
	for (&idx, &count) in &counts {
	if count >= 2 {
	// c² → c2 (squared variable)
	let c2 = ctx.get_or_create_squared(idx);
	coef_like_vars.push(c2);
	}
	}
	// For single occurrences, aggregate them into a single product variable
	let single_vars: Vec<VarIdx> = counts
	.iter()
	.filter(|(_, &c)| c == 1)
	.map(|(&idx, _)| idx)
	.collect();
	if !single_vars.is_empty() {
	// Chain all single-occurrence coefficients into one auxiliary product
	let mut acc = single_vars[0];
	for &v in single_vars.iter().skip(1) {
	acc = ctx.get_or_create_product(acc, v);
	}
	coef_like_vars.push(acc);
	}
	// Finally, combine all coefficient-like variables into at most one term
	if !coef_like_vars.is_empty() {
	let mut acc = coef_like_vars[0];
	for &v in coef_like_vars.iter().skip(1) {
	acc = ctx.get_or_create_product(acc, v);
	}
	result_coef_terms.push(term::var(acc, typ::int()));

[Copilot]

The CArray case returns the original term even after recursively processing the inner term (when new_inner != inner). This means transformations applied to the inner term are discarded. Either properly reconstruct the CArray with the new inner term, or if CArray reconstruction is not feasible, add a comment explaining why this case is expected to be unreachable in coefficient templates.

Suggested change

	term::RTerm::CArray { term: inner, .. } => {
	// CArray is rare in this context, just recurse into the inner term
	// and reconstruct if needed. For now, return original if structure matches.
	let new_inner = linearize_term(inner, ctx, coef_vars);
	if new_inner == *inner {
	term.clone()
	} else {
	// Create a new CArray - this is an edge case not expected in coefficient templates
	term.clone() // Simplified: just return the original
	}
	term::RTerm::CArray { .. } => {
	// Coefficient templates are not expected to contain CArray terms.
	// If this arm is reached, we conservatively leave the array term unchanged,
	// as the linearization procedure only reasons about scalar and datatype terms.
	term.clone()

[Copilot]

The Cartesian product expansion at lines 852-865 can produce exponentially many terms. For example, (a+b)(c+d)(e+f)*(g+h) would produce 2^4=16 terms. With deeply nested sums, this could lead to exponential blowup in both time and memory. Consider adding a check to limit the expansion size or document this limitation in the function's docstring.