Parser improvement #569
Parser improvement #569
Conversation
It starts to look like using a reentrant parser with custom name is not supported by flex/bison combination. This is the last commit where I still have an attempt at writing the system like that.
It looks like flex + bison combination does not support at the same time having a custom name for a parser and a reentrant parser. This commit removes the custom name for a parser so that we can use reentrancy.
|
At the moment the cluster doesn't let me log in so I haven't tested the code on real instances unfortunately. On separate benchmarking the parser code seems to be 20% faster compared to previous parser code, so I'm optimistic that this is an improvement. However, the code shouldn't be merged before someone can test it against master in a larger scale. |
QF_UF
|
|
There are some cases that I believe to be new stack overflows in
|
| @@ -145,6 +142,9 @@ int main( int argc, char * argv[] ) | |||
| opensmt_error( "SMTLIB 1.2 format is not supported in this version, sorry" ); | |||
| } | |||
| else if ( extension != NULL && strcmp( extension, ".smt2" ) == 0 ) { | |||
| std::filebuf fb; | |||
| fb.open(filename, std::ios::in); | |||
| std::istream is(&fb); | |||
There was a problem hiding this comment.
What are these added lines doing?
| @@ -0,0 +1,101 @@ | |||
| // | |||
| // Created by Antti Hyvärinen on 26.10.22. | |||
| // | |||
| itp_alg_ps, itp_alg_psw, itp_alg_pss, itp_euf_alg_strong, | ||
| itp_euf_alg_weak, itp_euf_alg_random, itp_lra_alg_strong, | ||
| itp_lra_alg_weak, itp_lra_alg_factor, itp_lra_alg_decomposing_strong, | ||
| itp_lra_alg_decomposing_weak}; |
There was a problem hiding this comment.
Maybe this enum should be split into separate enums for propositional, euf and lra interpolation algorithms?
| inline void setProduceModels( ) { insertOption(o_produce_models, new SMTOption(1)); } | ||
| inline bool setRandomSeed(int seed) { insertOption(o_random_seed, new SMTOption(seed)); return true; } | ||
| inline int getRandomSeed ( ) const { return optionTable.find(o_random_seed) != optionTable.end() ? optionTable.at(o_random_seed).getIntVal(): 91648253; } | ||
| inline void setProduceModels( ) { insertOption(o_produce_models, SMTOption(1)); } |
There was a problem hiding this comment.
Should this option have boolean value?
|
I don't see any immediate source of new stack overflows. It will be interesting to find out! |
This PR, at its core, suggests the use of a more structured parser for smt-lib2. The parser uses when possible
std::unique_ptrs for facilitating memory management. In addition it uses structs that improves readability compared to the uniform ASTNode approach used by the previous parser.In cases where smt-lib instances typically might use very deeply nested structures, the code resorts to raw pointers to avoid stack overflow on destructors of
unique_ptrs. For these cases the code uses custom destructors that delete structures in (reverse?) topological order.The change affects much of the interpret and option code, and I made relatively light refreshing on these parts as well.