Skip to content

Commit d0d5170

Browse files
authored
Condenser support on complex algebraic expressions to expressions (#1842)
Add support for Binary & Unary operations on AlgebraicExpressions -> Expressions
1 parent 1746d8c commit d0d5170

File tree

2 files changed

+93
-60
lines changed

2 files changed

+93
-60
lines changed

pil-analyzer/src/condenser.rs

Lines changed: 85 additions & 48 deletions
Original file line numberDiff line numberDiff line change
@@ -13,8 +13,9 @@ use num_traits::sign::Signed;
1313

1414
use powdr_ast::{
1515
analyzed::{
16-
self, AlgebraicExpression, AlgebraicReference, Analyzed, Challenge, DegreeRange,
17-
Expression, FunctionValueDefinition, Identity, IdentityKind, PolyID, PolynomialReference,
16+
self, AlgebraicBinaryOperation, AlgebraicExpression, AlgebraicReference,
17+
AlgebraicUnaryOperation, Analyzed, Challenge, DegreeRange, Expression,
18+
FunctionValueDefinition, Identity, IdentityKind, PolyID, PolynomialReference,
1819
PolynomialType, PublicDeclaration, Reference, SelectedExpressions, StatementIdentifier,
1920
Symbol, SymbolKind,
2021
},
@@ -24,8 +25,9 @@ use powdr_ast::{
2425
display::format_type_scheme_around_name,
2526
types::{ArrayType, Type},
2627
visitor::{AllChildren, ExpressionVisitable},
27-
ArrayLiteral, BlockExpression, FunctionCall, FunctionKind, LambdaExpression,
28-
LetStatementInsideBlock, Number, Pattern, SourceReference, TypedExpression, UnaryOperation,
28+
ArrayLiteral, BinaryOperation, BlockExpression, FunctionCall, FunctionKind,
29+
LambdaExpression, LetStatementInsideBlock, Number, Pattern, SourceReference,
30+
TypedExpression, UnaryOperation,
2931
},
3032
};
3133
use powdr_number::{BigUint, FieldElement};
@@ -939,6 +941,84 @@ fn shift_local_var_refs(e: &mut Expression, shift: u64) {
939941
.for_each(|e| shift_local_var_refs(e, shift));
940942
}
941943

944+
fn try_algebraic_expression_to_expression<T: FieldElement>(
945+
e: &AlgebraicExpression<T>,
946+
) -> Result<Expression, EvalError> {
947+
Ok(match e {
948+
AlgebraicExpression::Reference(AlgebraicReference {
949+
name,
950+
poly_id: _,
951+
next,
952+
}) => {
953+
let e = Expression::Reference(
954+
SourceRef::unknown(),
955+
Reference::Poly(PolynomialReference {
956+
name: name.clone(),
957+
type_args: None,
958+
}),
959+
);
960+
if *next {
961+
UnaryOperation {
962+
op: parsed::UnaryOperator::Next,
963+
expr: Box::new(e),
964+
}
965+
.into()
966+
} else {
967+
e
968+
}
969+
}
970+
971+
AlgebraicExpression::BinaryOperation(AlgebraicBinaryOperation { left, op, right }) => {
972+
BinaryOperation {
973+
left: Box::new(try_algebraic_expression_to_expression(left)?),
974+
op: (*op).into(),
975+
right: Box::new(try_algebraic_expression_to_expression(right)?),
976+
}
977+
.into()
978+
}
979+
980+
AlgebraicExpression::UnaryOperation(AlgebraicUnaryOperation { op, expr }) => {
981+
UnaryOperation {
982+
op: (*op).into(),
983+
expr: Box::new(try_algebraic_expression_to_expression(expr)?),
984+
}
985+
.into()
986+
}
987+
988+
AlgebraicExpression::Challenge(Challenge { id, stage }) => {
989+
let function = Expression::Reference(
990+
SourceRef::unknown(),
991+
Reference::Poly(PolynomialReference {
992+
name: "std::prelude::challenge".to_string(),
993+
type_args: None,
994+
}),
995+
)
996+
.into();
997+
let arguments = [*stage as u64, *id]
998+
.into_iter()
999+
.map(|x| BigUint::from(x).into())
1000+
.collect();
1001+
Expression::FunctionCall(
1002+
SourceRef::unknown(),
1003+
FunctionCall {
1004+
function,
1005+
arguments,
1006+
},
1007+
)
1008+
}
1009+
1010+
AlgebraicExpression::Number(n) => Number {
1011+
value: n.to_arbitrary_integer(),
1012+
type_: Some(Type::Expr),
1013+
}
1014+
.into(),
1015+
1016+
AlgebraicExpression::PublicReference(s) => {
1017+
Expression::PublicReference(SourceRef::unknown(), s.clone())
1018+
}
1019+
})
1020+
}
1021+
9421022
/// Tries to convert an evaluator value to an expression with the same value.
9431023
fn try_value_to_expression<T: FieldElement>(value: &Value<'_, T>) -> Result<Expression, EvalError> {
9441024
Ok(match value {
@@ -1021,49 +1101,6 @@ fn try_value_to_expression<T: FieldElement>(value: &Value<'_, T>) -> Result<Expr
10211101
"Converting builtin functions to expressions not supported.".to_string(),
10221102
))
10231103
}
1024-
Value::Expression(e) => match e {
1025-
AlgebraicExpression::Reference(AlgebraicReference {
1026-
name,
1027-
poly_id: _,
1028-
next: false,
1029-
}) => Expression::Reference(
1030-
SourceRef::unknown(),
1031-
Reference::Poly(PolynomialReference {
1032-
name: name.clone(),
1033-
type_args: None,
1034-
}),
1035-
),
1036-
AlgebraicExpression::Challenge(Challenge { id, stage }) => {
1037-
let function = Expression::Reference(
1038-
SourceRef::unknown(),
1039-
Reference::Poly(PolynomialReference {
1040-
name: "std::prelude::challenge".to_string(),
1041-
type_args: None,
1042-
}),
1043-
)
1044-
.into();
1045-
let arguments = [*stage as u64, *id]
1046-
.into_iter()
1047-
.map(|x| BigUint::from(x).into())
1048-
.collect();
1049-
Expression::FunctionCall(
1050-
SourceRef::unknown(),
1051-
FunctionCall {
1052-
function,
1053-
arguments,
1054-
},
1055-
)
1056-
}
1057-
AlgebraicExpression::Number(n) => Number {
1058-
value: n.to_arbitrary_integer(),
1059-
type_: Some(Type::Expr),
1060-
}
1061-
.into(),
1062-
_ => {
1063-
return Err(EvalError::TypeError(format!(
1064-
"Converting complex algebraic expressions to expressions not supported: {e}."
1065-
)))
1066-
}
1067-
},
1104+
Value::Expression(e) => try_algebraic_expression_to_expression(e)?,
10681105
})
10691106
}

pil-analyzer/tests/condenser.rs

Lines changed: 8 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -855,12 +855,11 @@ namespace std::prover;
855855
}
856856

857857
#[test]
858-
#[should_panic = "Converting complex algebraic expressions to expressions not supported: std::prover::x + std::prover::y"]
859-
fn capture_not_supported() {
860-
let input = r#"
858+
fn capture_binary_operations() {
859+
let input = r#"namespace std::prelude;
861860
namespace std::prover;
862-
let provide_value = 9;
863-
let eval = -1;
861+
let provide_value = 9;
862+
let eval = -1;
864863
namespace N(16);
865864
(constr || {
866865
let x;
@@ -872,18 +871,15 @@ fn capture_not_supported() {
872871
})();
873872
874873
"#;
875-
let expected = r#"namespace std::prelude;
876-
let challenge = 8;
877-
namespace std::prover;
874+
let expected = r#"namespace std::prover;
878875
let provide_value = 9;
879876
let eval = -1;
877+
col witness x;
880878
col witness y;
881879
{
882-
let x = std::prelude::challenge(0, 4);
883-
let y = std::prover::y;
884-
let t = 2;
880+
let t = std::prover::x + std::prover::y;
885881
query |i| {
886-
std::prover::provide_value(y, i, std::prover::eval(x) + t);
882+
let _: fe = std::prover::eval(t);
887883
}
888884
};
889885
"#;

0 commit comments

Comments
 (0)