Support for parenthesized arithmetic expressions.

docs/polyhedral-term-syntax.md

@@ -3,22 +3,38 @@
 The `pacti.contracts.PolyhedralIoContract.from_strings()` API invokes a parser for `pacti.terms.polyhedra.PolyhedralTerm` to construct the assumptions and guarantees of a `PolyhedralIoContract`. The syntactic `expression` of a `PolyhedralTerm` is defined by the following BNF grammar in the `pacti.terms.polyhedra.syntax.grammar` module:
 
 ```text
+floating_point_number = 
+ ( '0'..'9'+ ('.' '0'..'9'*)? | '.' '0'..'9'+ )
+ ('E' | 'e') ('-' | '+')? '0'..'9'+ )?;
 
-variable = ('a'..'z' | 'A'..'Z'), ('a'..'z' | 'A'..'Z' | '0'..'9' | '_')*;
+operation = '+' | '-' | '*' | '/';
 
-floating_point_number = '0'..'9'+, ("." , '0'..'9'+)?, (("e" | "E"), ("-" | "+")?, '0'..'9'+)?;
+arithmetic_expr =
+ floating_point_number (operation floating_point_number)*;
 
-number_and_variable = floating_point_number, ("*" , variable)?;
+paren_arith_expr = '(' arithmetic_expr ')';
 
-term = variable | floating_point_number | number_and_variable | (floating_point_number '*'?)? "(" terms ")";
+variable = 'a'..'z' | 'A'..'Z' ('a'..'z' | 'A'..'Z' | '0'..'9' | '_')*;
+
+symbol = '+' | '-';
+
+only_variable = variable | paren_terms;
+
+number_and_variable = 
+ (floating_point_number | paren_arith_expr) '*'? variable
+ | (floating_point_number | paren_arith_expr) '*'? paren_terms;
+
+only_number = floating_point_number | paren_arith_expr;
+
+term = only_variable | number_and_variable | only_number;
 
 first_term = ("-" | "+")?, term;
 
 signed_term = ("-" | "+") , term;
 
 terms = first_term, signed_term*;
 
-abs_term = floating_point_number?, "|", terms, "|";
+abs_term = (floating_point_number | paren_arith_expr)?, "|", terms, "|";
 
 positive_abs_term = "+", abs_term;
 
@@ -30,7 +46,7 @@ addl_abs_or_term = positive_abs_term | signed_term;
 
 abs_or_terms = first_abs_or_term, addl_abs_or_term*;
 
-paren_abs_or_terms = (floating_point_number, '*'?)? "(", abs_or_terms, ")";
+paren_abs_or_terms = ((floating_point_number | paren_arith_expr), '*'?)? "(", abs_or_terms, ")";
 
 first_paren_abs_or_terms = "+"? paren_abs_or_terms | first_abs_or_term;
 
@@ -76,6 +92,7 @@ Parsing rules produce an intermediate representation that facilitates performing
  - An `AbsoluteTerm` with no `coefficient` and a `term_list` with `constant=3` and no `factors`.
  - `4|x+2x|` is equivalent to `4|3x|`, yielding:
  - An `AbsoluteTerm` with `coefficient=4` and a `term_list` with `constant=0` and no `factors={'x'=3}`.
+ - `(2/3)x` is approximatively `0.66666x`
 
 - The parsing of `first_abs_or_term` or `addl_abs_or_term` each produces a `pacti.terms.polyhedra.syntax.grammar.PolyhedralSyntaxAbsoluteTermOrTerm`, which represents the union of `PolyhedralSyntaxAbsoluteTerm` and `PolyhedralSyntaxTermList` as the constituents of the side of an `expression`.
 
@@ -98,6 +115,8 @@ Parsing rules produce an intermediate representation that facilitates performing
  - `coefficient=None` and a `term_list` with `constant=-3` and `factors={'x':-1}`;
  - `coefficient=3.0` and a `term_list` with `constant=0` and `factors={'y':4, 't':5}`.
 
+- Wherever the grammar accepts a floating point number as a constant, one can replace that constant with a parenthesized arithmetic expression involving the four operations: `+`, `-`, `*`, and `/`.
+
 - The parsing of `expression` produces an `pacti.terms.polyhedra.syntax.grammar.PolyhedralSyntaxExpression` that, in the serializer module, is converted to a `pacti.terms.polyhedra.PolyhedralTerm`. The parser handles three forms of `expression`:
  - The parsing of `equality_expression` handles the syntax of equality expressions of the form: `LHS ('==' | '=') RHS` where `LHS` and `RHS` are parsed as `terms`,
  which allows for parenthesis around terms but excludes absolute value terms.

examples/grammar/expressions.py

@@ -2,8 +2,12 @@
 
 
 for s in [
- # "x",
+ "x",
+ "(2/3)x",
  "(2x+1)",
+ "1+10+2x",
+ "1+2x-10",
+ "1+2x-10",
  "3(2x+1)",
  "-x+2(1+x)",
  "(4y + 5t)+2(4y + 5t)",
@@ -75,6 +79,8 @@
 
 for s in [
  "2|x| <= 0",
+ "2|x| <= (1/3)",
+ "2|x| <= (1/3-2)",
  "|x| <= 2|x|",
  "3|x| + y >= 3|y|",
  "|-x + 3| + 3 |4y + 5t| - 7z <= 8t - |x - y|",

src/pacti/terms/polyhedra/syntax/grammar.py

@@ -304,14 +304,29 @@ def _parse_expression(tokens: pp.ParseResults) -> PolyhedralSyntaxExpression:
 # Produces a float
 floating_point_number = (
  pp.Combine(
- pp.Word(pp.nums)
- + pp.Optional("." + pp.Optional(pp.Word(pp.nums)))
+ pp.Or([pp.Word(pp.nums) + pp.Optional("." + pp.Optional(pp.Word(pp.nums))), "." + pp.Word(pp.nums)])
  + pp.Optional(pp.CaselessLiteral("E") + pp.Optional(pp.oneOf("+ -")) + pp.Word(pp.nums))
  )
  .set_parse_action(lambda t: float(t[0])) # noqa: WPS348
  .set_name("floating_point_number") # noqa: WPS348
 )
 
+# Basic arithmetic operations
+plus, minus, mult, div = map(pp.Literal, "+-*/")
+
+# Using infixNotation to manage precedence of operations
+arithmetic_expr = pp.infixNotation(
+ floating_point_number,
+ [
+ (mult | div, 2, pp.opAssoc.LEFT, lambda s, l, t: t[0][0] * t[0][2] if t[0][1] == "*" else t[0][0] / t[0][2]),
+ (plus | minus, 2, pp.opAssoc.LEFT, lambda s, l, t: t[0][0] + t[0][2] if t[0][1] == "+" else t[0][0] - t[0][2]),
+ ],
+)
+
+paren_arith_expr = pp.Group(
+ pp.Suppress("(") + arithmetic_expr + pp.Suppress(")")
+).setParseAction(lambda t: t[0][0])
+
 variable = pp.Word(pp.alphas, pp.alphanums + "_").set_name("variable")
 symbol = pp.oneOf("+ -").set_name("symbol")
 
@@ -324,19 +339,21 @@ def _parse_expression(tokens: pp.ParseResults) -> PolyhedralSyntaxExpression:
 only_variable = variable.set_parse_action(_parse_only_variable)
 
 # Produces a PolyhedralSyntaxTermList
-number_and_variable = (floating_point_number + pp.Optional("*") + variable).set_parse_action(_parse_number_and_variable)
+number_and_variable = ((floating_point_number ^ paren_arith_expr) + pp.Optional("*") + variable).set_parse_action(
+ _parse_number_and_variable
+)
 
 # Produces a float
-only_number = floating_point_number
+only_number = floating_point_number ^ paren_arith_expr
 
 # Add support for parenthesized terms
 # Produces a PolyhedralSyntaxTermList
 only_variable |= paren_terms
 
 # Produces a PolyhedralSyntaxTermList
-number_and_variable |= pp.Group(floating_point_number + pp.Optional("*") + paren_terms).set_parse_action(
- _parse_factor_paren_terms
-)
+number_and_variable |= pp.Group(
+ (floating_point_number ^ paren_arith_expr) + pp.Optional("*") + paren_terms
+).set_parse_action(_parse_factor_paren_terms)
 
 # Produces a PolyhedralSyntaxTermList
 only_number |= paren_terms
@@ -361,7 +378,7 @@ def _parse_expression(tokens: pp.ParseResults) -> PolyhedralSyntaxExpression:
 
 # Produces an PolyhedralSyntaxAbsoluteTerm
 abs_term = (
- pp.Group(pp.Optional(floating_point_number + pp.Optional("*")) + "|" + terms + "|")
+ pp.Group(pp.Optional((floating_point_number ^ paren_arith_expr) + pp.Optional("*")) + "|" + terms + "|")
  .set_parse_action(_parse_absolute_term) # noqa: WPS348
  .set_name("abs_term") # noqa: WPS348
 )
@@ -403,7 +420,7 @@ def _parse_expression(tokens: pp.ParseResults) -> PolyhedralSyntaxExpression:
 
 # Produces an PolyhedralSyntaxAbsoluteTermList
 paren_abs_or_terms = (
- pp.Group(pp.Optional(floating_point_number + pp.Optional("*")) + "(" + abs_or_terms + ")")
+ pp.Group(pp.Optional((floating_point_number ^ paren_arith_expr) + pp.Optional("*")) + "(" + abs_or_terms + ")")
  .set_parse_action(_parse_paren_abs_or_terms) # noqa: WPS348
  .set_name("paren_abs_or_terms") # noqa: WPS348
 )

tests/test_examples.py

@@ -30,6 +30,7 @@ def test_examples1() -> None:
  unecessary_simplification.simplify()
  assert unecessary_simplification == contract_comp
 
+
 def test_examples2() -> None:
  contract1 = {
  "input_vars": ["u_1"],
@@ -57,18 +58,13 @@ def test_examples2() -> None:
  unecessary_simplification.simplify()
  assert unecessary_simplification == contract_comp
 
+
 def test_IoContract_compose_and_quotient_tactics():
  contract1 = iocontract.IoContract(
- assumptions=PolyhedralTermList(),
- guarantees=PolyhedralTermList(),
- input_vars=[],
- output_vars=[]
+ assumptions=PolyhedralTermList(), guarantees=PolyhedralTermList(), input_vars=[], output_vars=[]
  )
  contract2 = iocontract.IoContract(
- assumptions=PolyhedralTermList(),
- guarantees=PolyhedralTermList(),
- input_vars=[],
- output_vars=[]
+ assumptions=PolyhedralTermList(), guarantees=PolyhedralTermList(), input_vars=[], output_vars=[]
  )
  result1, _ = contract1.compose_tactics(contract2, tactics_order=None)
  assert isinstance(result1, iocontract.IoContract)
@@ -80,4 +76,4 @@ def test_IoContract_compose_and_quotient_tactics():
 if __name__ == "__main__":
  test_examples1()
  test_examples2()
- test_IoContract_compose_tactics()
+ test_IoContract_compose_tactics()

tests/test_polyhedral_contract_simplification.py

@@ -1,35 +1,30 @@
 from pacti.contracts import PolyhedralIoContract
 
+
 def test1_simplified() -> None:
  c = PolyhedralIoContract.from_strings(
- input_vars=["x"], 
- output_vars=[], 
- assumptions=["|x| <= 10"], 
- guarantees=["x <= 100"],
- simplify=True)
+ input_vars=["x"], output_vars=[], assumptions=["|x| <= 10"], guarantees=["x <= 100"], simplify=True
+ )
  assert 1 == len(c.inputvars)
  assert "x" == c.inputvars[0].name
- 
+
  assert 0 == len(c.outputvars)
  assert 2 == len(c.a.terms)
  assert 0 == len(c.g.terms)
 
+
 def test1_not_simplified() -> None:
  c = PolyhedralIoContract.from_strings(
- input_vars=["x"], 
- output_vars=[], 
- assumptions=["|x| <= 10"], 
- guarantees=["x <= 100"],
- simplify=False)
+ input_vars=["x"], output_vars=[], assumptions=["|x| <= 10"], guarantees=["x <= 100"], simplify=False
+ )
  assert 1 == len(c.inputvars)
  assert "x" == c.inputvars[0].name
- 
+
  assert 0 == len(c.outputvars)
  assert 2 == len(c.a.terms)
  assert 1 == len(c.g.terms)
 
 
-
 if __name__ == "__main__":
  test1_simplified()
- test1_not_simplified()
+ test1_not_simplified()

tests/test_polyhedral_terms.py

@@ -41,6 +41,7 @@ def test_polyhedral_var_elim_by_refinement_2() -> None:
  (reference2, _) = reference.elim_vars_by_refining(context, vars_elim, simplify=False, tactics_order=[])
  assert reference2.terms == reference.terms
 
+
 def test_polyhedral_var_elim_by_refinement_3() -> None:
  # the context can transform the reference
  x = Var("x")
@@ -98,7 +99,7 @@ def test_polyhedral_var_elim_by_relaxation_7() -> None:
  vars_elim = [y]
  (reference1, _) = reference.elim_vars_by_relaxing(context, vars_elim)
  assert reference1.terms == expected.terms
- 
+
  (reference2, _) = reference.elim_vars_by_relaxing(context, vars_elim, simplify=False)
  assert reference2.terms == expected.terms
 
@@ -121,31 +122,23 @@ def test_issue171() -> None:
 
 def test_relaxing1() -> None:
  constraints = to_pts(
- ["1*dt0 + 1*t0 <= 0.0", 
-  "-1*t0 <= 0.0", 
-  "-1*dt0 - 1*t0 + 1*t1 <= 0.0", 
-  "1*dt0 + 1*t0 - 1*t1 <= 0.0"]
+ ["1*dt0 + 1*t0 <= 0.0", "-1*t0 <= 0.0", "-1*dt0 - 1*t0 + 1*t1 <= 0.0", "1*dt0 + 1*t0 - 1*t1 <= 0.0"]
+ )
+ (transformed, tactics) = constraints.elim_vars_by_relaxing(
+ PolyhedralTermList([]), [Var("t0"), Var("dt0")], simplify=False
  )
- (transformed, tactics) = constraints.elim_vars_by_relaxing(PolyhedralTermList([]), [Var("t0"), Var("dt0")], simplify=False)
  expected = to_pts(["1*t1 <= 0", "0 <= 0"])
  assert expected == transformed
 
 
 def test_relaxing2() -> None:
  constraints = to_pts(
- ["1*dt0 + 1*t0 <= 0.0", 
- "-1*t0 <= 0.0", 
- "-1*dt0 - 1*t0 + 1*t1 <= 0.0", 
- "1*dt0 + 1*t0 - 1*t1 <= 0.0"]
- )
- context = to_pts(
- ["-dt0 <= -1",
- "dt0 <= 0"]
+ ["1*dt0 + 1*t0 <= 0.0", "-1*t0 <= 0.0", "-1*dt0 - 1*t0 + 1*t1 <= 0.0", "1*dt0 + 1*t0 - 1*t1 <= 0.0"]
  )
+ context = to_pts(["-dt0 <= -1", "dt0 <= 0"])
  with pytest.raises(ValueError):
  _ = constraints.elim_vars_by_relaxing(context, [Var("t0"), Var("dt0")], simplify=True)
-
-
+
  (transformed1, _) = constraints.elim_vars_by_relaxing(context, [Var("t0"), Var("dt0")], simplify=False)
  expected = to_pts(["1*t1 <= 0", "0 <= 0", "-1*t1 <= -1"])
  assert expected == transformed1
@@ -154,5 +147,6 @@ def test_relaxing2() -> None:
  expected = to_pts(["1*t1 <= 0", "-1*t0 <= 0", "0 <= 0", "-1*t1 <= -1"])
  assert expected == transformed2
 
+
 if __name__ == "__main__":
  test_relaxing2()