How would one compare two parse tree to find ambiguity in a Context Free Grammar by using Z3 solver? -


example grammar:

e ::= e + e | n

i need prove grammar ambiguous due following 2 paths:

e -> e + e -> e + e + e -> n + e + e e -> e + e -> n + e -> n + e + e

the idea 1 compare functions "sets" symbol1(symbol,index,time) (for specific time t) , symbol2(symbol,index,time) - finding equivalent - having different predecessor (i.e @ time t-1)

the problem have no idea how compare 2 functions symbol1 , symbol2

i can post code, if you're interested .... (its page , half worth, might inappropriately long?).

the code written in z3py.

checking whether cfg ambiguous undecidable in general. however, if restrict number of rule applications small number, can try generating possible strings many applications , check whether can reach same string using different number of steps. in case, don't think smt solvers fit kind of problem since number of strings derivable can grow exponentially number of steps; require keep number of steps small number, making problem uninteresting.

of course, if know property of grammar in advance, can come custom algorithm take advantage of it. (say if it's lalr(1) parseable.) in case other algorithmic methods better compared smt based solution.


Comments

Post a Comment

Popular posts from this blog

SPSS keyboard combination alters encoding -

my question not have programming practical issue on spss. accident keyword combination cannot remember because did not intend press changed encoding in spss , text in data in different language english shown small boxes. nevertheless, when kind of analysis performed different language text shown in output. does know reason? tried change encoding did not produce result. first, @ edit > options , see whether setting unicode or locale. might fix it. if have text in multiple languages, want unicode. otherwise, may have specific locale set wrong. can change set locale, need know locale want use.
Read more

Add new record to the table by click on the button in Microsoft Access -

in ms access form want implement separate button, adds new record table. in order added button , attached button event: private sub btnaddrec_click() refresh codecontextobject on error resume next docmd.gotorecord , , acnewrec if err.number <> 0 btnaddrec.enabled = false end if end end sub everything ok when open window , click btnaddrec button, problem when first of perform navigation through existed records , after click on button. got runtime error: 2105: «you can't go specified record. may @ end of recordset» . how solve issue, need have ability add new record on click on specific button, no matter, have walked or not walked through records before. thanks. i created simple form field call description (and autonumber) , created button code follows click event. filled number of records , navigated through them, clicked addnewrec button. form navigated new record without issues. able click addnewrec button directly after
Read more

javascript - jQuery .height() return 0 when visible but non-0 when hidden -

i have problem here right opposite others: in jquery cannot height of element when it's visible, when hidden. have html code: <div id="filtering-filter-holder"> <div id="filtering-filter-holder-inner"></div> </div> basic css it: #filtering-filter-holder { display: none; position: absolute; width: 420px; min-height: 100px; padding: 5px 5px 5px 5px; background-color: #ffffff; border: 1px solid #164372; } and finally, js in document.ready(): $('div.filtering-filter-headline').mouseenter(function() { var el = $(this).parent().find('div.filtering-filter-content'); if ($('div#filtering-filter-holder').is(':visible')) { $('div#filtering-filter-holder-inner').stop(true, true).fadeout(300, function() { $('div#filtering-filter-holder-inner').html($(el).html()); var height = $('div#filtering-filter-holder-inner&#
Read more