Merge remote-tracking branch 'origin/master' into HEAD

.github/workflows/main.yml

@@ -17,7 +17,7 @@ jobs:
     - name: Install dependencies
       run: |
         python -m pip install --upgrade pip 
-        python -m pip install antlr4-python3-runtime==4.8  
+        python -m pip install antlr4-python3-runtime==4.9.2  
     - name: Run Unittests
       run: |
         python -m unittest tests/runtests.py

README.md

@@ -27,7 +27,7 @@ Requirements:
 - antlr4 python runtime  
 ``` bash
 git clone https://github.com/testsmt/yinyang.git 
-pip3 install antlr4-python3-runtime==4.8  
+pip3 install antlr4-python3-runtime==4.9.2  
 ```
 
 
@@ -57,3 +57,4 @@ Additional Ressources
 ----------
 - [Citing yinyang](https://yinyang.readthedocs.io/en/latest/building_on.html#citing-yinyang)
 - [Project website](https://testsmt.github.io/) with bug statistics, talk videos, etc.
+- [Google Open Source Peer Bonus](https://opensource.googleblog.com/2021/04/announcing-first-group-of-google-open-source-peer-bonus-winners.html#:~:text=The%20Google%20Open%20Source%20Peer,exceptional%20contributions%20to%20open%20source.) 

docs/installation.rst

@@ -12,6 +12,6 @@ The following commands clone yinyang and install the antlr4 python runtime.
 .. code-block:: bash
 
     $ git clone https://github.com/testsmt/yinyang.git 
-    $ pip3 install antlr4-python3-runtime==4.8  
+    $ pip3 install antlr4-python3-runtime==4.9.2  
 
 

src/args.py

@@ -99,7 +99,7 @@
 )
 parser.add_argument(
     "-fl", "--file-size-limit",
-    default=20000,
+    default=100000,
     type=int,
     help="file size limit on seed formula in bytes"
 )

src/parsing/SMTLIBv2.g4

@@ -7,8 +7,7 @@
  * The MIT License (MIT)
  *
  * Copyright (c) 2017 Julian Thome <[email protected]>
- *
- * Modified by Dominik Winterer <[email protected]> 
+ *               2020 Dominik Winterer <[email protected]> 
  *
  * Permission is hereby granted, free of charge, to any person obtaining a copy of
  * this software and associated documentation files (the "Software"), to deal in
@@ -145,9 +144,6 @@ CMD_CheckSatAssuming
 CMD_CheckSatUsing
     : 'check-sat-using'
     ;
-/*CMD_Apply*/
-    /*: 'apply'*/
-    /*;*/
 
 CMD_Labels
     : 'labels'
@@ -327,9 +323,6 @@ GRW_Decimal
 GRW_Exists
     : 'exists'
     ;
-/*GRW_Lambda*/
-    /*: 'lambda'*/
-    /*;*/
 GRW_Hexadecimal
     : 'HEXADECIMAL'
     ;
@@ -601,7 +594,6 @@ generalReservedWord
     | GRW_Binary
     | GRW_Decimal
     | GRW_Exists
-    /*| GRW_Lambda*/
     | GRW_Hexadecimal
     | GRW_Forall
     | GRW_Let
@@ -731,8 +723,8 @@ spec_constant
     | string
     | b_value
     | reg_const
-    | ParOpen GRW_Underscore ' bv' numeral numeral ParClose
     ;
+
 s_expr
     : spec_constant
     | symbol
@@ -799,6 +791,7 @@ match_case
 
 term
     : spec_constant
+    | ParOpen GRW_Underscore symbol numeral ParClose
     | qual_identifier
     | ParOpen qual_identifier term+ ParClose
     | ParOpen ParOpen GRW_Underscore qual_identifier term+ ParClose ParClose
@@ -863,7 +856,6 @@ logic
     : ParOpen PS_Logic symbol logic_attribue+ ParClose
     ;
 
-
 // Scripts
 
 sort_dec
@@ -922,9 +914,6 @@ cmd_checkSatAssuming
 cmd_checkSatUsing
     : CMD_CheckSatUsing
     ;
-/*cmd_apply*/
-    /*: CMD_Apply*/
-    /*;*/
 
 cmd_minimize
     : CMD_Minimize
@@ -1103,9 +1092,6 @@ par_or_else
 par_or
     : TAC_ParOr
     ;
-/*repeat*/
-    /*: TAC_Repeat*/
-    /*;*/
 
 tryFor
     : TAC_TryFor