@@ -211,43 +211,48 @@ export class PolicyGenerator {
211211 returnType : 'any' ,
212212 statements : ( writer ) => {
213213 writer . write ( `
214- const assertions: any[] = [];
215- if ('OR' in args) {
216- const tempAssertions: any[] = [];
217- for (const arg of args.OR) {
218- tempAssertions.push(buildAssertion(z3, variables, arg, user, fieldStringValueMap));
219- }
220- const orAssertion = z3.Or(...tempAssertions);
221- assertions.push(orAssertion);
222- }
223-
224- // handle string conditions
225- // TODO: handle string conditions for user properties
226- const condition = checkStringCondition(args, fieldStringValueMap);
227- if (condition === false) {
228- return z3.Bool.val(false);
229- }
230-
231- const tempAssertions: any[] = [];
232-
233- for (const property of Object.keys(args)) {
234- const condition = args[property];
235- // TODO: handle nested properties
236- const variable = variables[property];
237- if (variable) {
238- tempAssertions.push(...processCondition(variable, condition, z3));
239- }
240- }
214+ const processedVariables = Object.keys(variables).reduce((acc, key) => {
215+ const newKey = key.replace(/^_/, '');
216+ acc[newKey] = variables[key];
217+ return acc;
218+ }, {} as Record<string, any>);
219+ const assertions: any[] = [];
220+ if ('OR' in args) {
221+ const tempAssertions: any[] = [];
222+ for (const arg of args.OR) {
223+ tempAssertions.push(buildAssertion(z3, processedVariables, arg, user, fieldStringValueMap));
224+ }
225+ const orAssertion = z3.Or(...tempAssertions);
226+ assertions.push(orAssertion);
227+ }
228+
229+ // handle string conditions
230+ // TODO: handle string conditions for user properties
231+ const condition = checkStringCondition(args, fieldStringValueMap);
232+ if (condition === false) {
233+ return z3.Bool.val(false);
234+ }
235+
236+ const tempAssertions: any[] = [];
241237
242- // avoid empty assertions in case of unique value or boolean
243- if (tempAssertions.length > 1) {
244- const andAssertion = z3.And(...tempAssertions);
245- assertions.push(andAssertion);
246- } else if (tempAssertions.length === 1) {
247- assertions.push(...tempAssertions);
248- }
238+ for (const property of Object.keys(args)) {
239+ const condition = args[property];
240+ // TODO: handle nested properties
241+ const variable = processedVariables[property];
242+ if (variable) {
243+ tempAssertions.push(...processCondition(variable, condition, z3));
244+ }
245+ }
249246
250- return z3.And(...assertions);
247+ // avoid empty assertions in case of unique value or boolean
248+ if (tempAssertions.length > 1) {
249+ const andAssertion = z3.And(...tempAssertions);
250+ assertions.push(andAssertion);
251+ } else if (tempAssertions.length === 1) {
252+ assertions.push(...tempAssertions);
253+ }
254+
255+ return z3.And(...assertions);
251256 ` ) ;
252257 } ,
253258 } ) ;
@@ -1052,17 +1057,15 @@ export class PolicyGenerator {
10521057 expressions . forEach ( ( expr ) => {
10531058 const variables = this . collectVariablesTypes ( expr ) ;
10541059 Object . keys ( variables ) . forEach ( ( key ) => {
1055- if ( ! result [ key ] ) {
1056- switch ( variables [ key ] ) {
1057- case 'NumberLiteral' :
1058- result [ key ] = `z3.Int.const("${ key } ")` ;
1059- break ;
1060- case 'BooleanLiteral' :
1061- result [ key ] = `z3.Bool.const("${ key } ")` ;
1062- break ;
1063- default :
1064- break ;
1065- }
1060+ switch ( variables [ key ] ) {
1061+ case 'NumberLiteral' :
1062+ result [ `_${ key } ` ] = `z3.Int.const("${ key } ")` ;
1063+ break ;
1064+ case 'BooleanLiteral' :
1065+ result [ `_${ key } ` ] = `z3.Bool.const("${ key } ")` ;
1066+ break ;
1067+ default :
1068+ break ;
10661069 }
10671070 } ) ;
10681071 } ) ;
0 commit comments