Fix Lab1

[TonitaN]

Problem: corrupted smt2-file syntax

Test:

g(x, x) -> h(x, h(x, x))

Broken syntax in smt2 file:

(assert (>= t1 (*  + t5 t4 ))

And there are other problems with the model, please check thoroughly.

[TonitaN]

A similar problem with broken smt2-syntax (paren mismatch):

f(x) -> g(x)

smt2 line with the error:

(assert (>=  t1  (*  t3 t3 ))

[TonitaN]

The first lab still requires fixing. E.g. given the input

f(x) -> g(x)
g(x) -> f(x)

the program constructs the following model

(set-logic QF_NIA)
(declare-fun t0 () Int)
(declare-fun t1 () Int)
(declare-fun t2 () Int)
(declare-fun t3 () Int)

(assert (>=  t1  (*  t3 t3 )))

(assert (>= t0  (+ (* t2  )t2) )))

(assert (and (>= t0 1) (>= t1 0) (>= t2 1) (>= t3 0)))

(assert (or (>  t1  (*  t3 t3 )) (> t0  (+ (* t2  )t2) )) ))

(assert (and (or (> t0 1) (> t1 0)) (or (> t2 1) (> t3 0))))

(check-sat)
(get-model)
(exit)

Besides the bracket mismatch, the assertions are semantically 'strange'. Since the linear terms are only to occur in the model (no compositions are given in the input), but the multiplied coefficients occur.

[TonitaN]

The rewriting lab requires more accurate treating of variables and their substitution. E.g. given the input

n=2
x, y
f(t, t)
f(x, y) -> f(y, x)
f(x, x) -> x

In the first step f(t,t) is rewritten to f(y, t) (thus, the variable y is not substituted with t) instead of f(t, t).

[Thangnv24]

In rewriting lab, variables are distinguished with ',' wirhout space, so input should be:

n=2
x,y
f(t, t)
f(x, y) -> f(y, x)
f(x, x) -> x

The result:

Step 1: 
t
f(t, t)
Step 2: 
t
f(t, t)

In first lab, I did not allow multiple linear terms at the same time, I have fixed it

[TonitaN]

I recommend to use trim methods in such cases, in order to make the input parser more stable.

[Thangnv24]

I have removed the extra spaces in the variables and in the rules, input like this is accepted:

n=2
x,   y, t
f(t, t)
f(x, y) ->   f(y, x)
f(x, x) ->    x

[TonitaN]

Lab1 is now ok! Lab 1-0 still requires some trim methods (despite working ok with the certain spacing), to accept inputs like the following:

n=2
x,y,z
f(t,z)
f(x,y) -> f(y,x)
f(z,x) -> f(z,z)

[TonitaN]

Note: in the test files in the repo, some spaces between constructor args are already omitted.

[TonitaN]

And still some bugs remain. On the following input, I get the term f(,x) besides the right one.

2
x,z,y
f(f(x, x), x)
f(x,x) -> f(f(x,x),x)

[TonitaN]

Consider the test

3
x,z,y
f(f(x, x), x)
f(x,x) -> f(f(x,x),x)
f(x,x) -> h(x)
h(h(x)) -> g(x)

The third rule is processed incorrectly: only the outermost constructor is taken into account. The rules can have an arbitrary nesting both in left- and right-hand sides.

[Thangnv24]

I fixed the errors, please check

[TonitaN]

Python exception in Lab1-1 on input

2
x,z,y
f(f(x, x), x)
f(x,y) -> f(y,x)
f(x,f(x,y)) -> f(f(x,x),x)
f(x,y) -> h(x)
h(h(x)) -> g(x)

[TonitaN]

For future (lab2 - I believe you have not yet announced that it is finished, but in case you haven't see the problems): b**bcba**c((a|c)|(a|c))a**b**a**a**c Regex optimized: b*bcba*c(a|c|c)a*b*a*a*c` There we have even two problems: no idempotency transformation for c, and, more critically, semantics change: (a|c)(a|c) and (a|c|c) have different languages.