diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-11-25 10:46:41 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-11-25 10:46:41 -0600 |
commit | de14432ebd850dab001bb860db102e86ec734f97 (patch) | |
tree | c3d425c58d27e5e28b00e2870d2f30c48d0f68f0 /test/unit | |
parent | 03979b02fb0296aefdfeb0c00e6eb4ea5ac01cc8 (diff) |
Use symbol manager for printing responses get-model (#5516)
This makes symbol manager be in charge of determining which sorts and terms to print in response to get-model. This eliminates the need for the parser to call ExprManager::mkVar (and similar methods) with custom flags.
This requires significant simplifications to the printers for models, where instead of a NodeCommand, we take a Sort or Term to print in the model.
This is one of the last remaining steps for migrating the parser to the new API.
The next step will be to remove a lot of the internal infrastructure for managing expression names, commands to print in models, node commands, node listeners, etc.
Diffstat (limited to 'test/unit')
-rw-r--r-- | test/unit/parser/parser_black.h | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/test/unit/parser/parser_black.h b/test/unit/parser/parser_black.h index 3b0bbb139..ef8f2e3cf 100644 --- a/test/unit/parser/parser_black.h +++ b/test/unit/parser/parser_black.h @@ -259,8 +259,6 @@ public: tryGoodInput("a : INT = 5; a: INT;"); // decl after define, compatible tryGoodInput("a : TYPE; a : INT;"); // ok, sort and variable symbol spaces distinct tryGoodInput("a : TYPE; a : INT; b : a;"); // ok except a is both INT and sort `a' - //tryGoodInput("a : [0..0]; b : [-5..5]; c : [-1..1]; d : [ _ .._];"); // subranges - tryGoodInput("a : [ _..1]; b : [_.. 0]; c :[_..-1];"); tryGoodInput("DATATYPE list = nil | cons(car:INT,cdr:list) END; DATATYPE cons = null END;"); tryGoodInput("DATATYPE tree = node(data:list), list = cons(car:tree,cdr:list) | nil END;"); //tryGoodInput("DATATYPE tree = node(data:[list,list,ARRAY tree OF list]), list = cons(car:ARRAY list OF tree,cdr:BITVECTOR(32)) END;"); |