Preprocessor.preprocess의 invfunclist가 갱신되지 않음

[cushionbadak]

SyGuSML/src/solver/preprocessor.ml

Line 452 in 8821515

analysisCmd ((changeInvConstraintToConstraint (InvConstraint(s, s_pre, s_trans, s_post)) invfunclist) @ t) signature logiclist invfunclist (ftGrammars, ftFwdDecls, ftRecursion)

Preprocessor.preprocess 내의 analysisCmd 함수에서, Cmd가 inv-constraint로 시작하는 경우에도, 그 외의 어느 경우에도 analysisCmd 함수에 넘겨진 invfunclist의 값을 갱신한 값은 나타나지 않는다.

[hongjisung]

preprocess 전에
desugar 함수를 먼저 실행하는데
이때 inv-constraint가 constraint로 치환되어서 그런 것으로 보임

preprocess 함수 실행할때는
syntax sugar인
inv-constraint, synth-inv, declare-datatype 등은 ast에서 없어야 함