sillydan1 / expr

Simple variable and environment manipulation language
MIT License
1 stars 0 forks source link

Add minisat driver #12

Open sillydan1 opened 1 year ago

sillydan1 commented 1 year ago

Z3 Prover is nice and all, but more choices are always good.

It should be fairly straight forward to implement another driver that utilizes the C++ interface for minisat.

Take a look at this as a possibility

mingodad commented 10 months ago

Not related but to not open an issue for it: I just added this project grammar/lexer to my online yacc/lex editor/tester at https://mingodad.github.io/parsertl-playground/playground/ , select Expr-lang parser from Examples then click Parse to see the parser tree.

Any feedback is welcome !

mingodad commented 10 months ago

Also I replaced the right recursion by left recursion on rule statements.

https://github.com/mingodad/parsertl-playground/blob/fa2a90e8b89b8156f2a0e1213ec8b1e6a2070749/playground/expr-lang.g#L79

sillydan1 commented 10 months ago

Interesting project :smile: it's a good resource to have for testing the grammar

Is there a specific reason to prefer left recursion over right recursion?

mingodad commented 10 months ago

LALR parser can exaust the internal stack when using right recursion also the parser tree goes deeper with right recursion, see here https://www.gnu.org/software/bison/manual/bison.html#Recursion .