summaryrefslogtreecommitdiff
path: root/src/parser/smt2/Smt2.g
AgeCommit message (Expand)Author
2020-02-26Move fix for vacuous sygus types out of the parser (#3820)Andrew Reynolds
2020-02-26Refactor type ascriptions in the parser (#3825)Andrew Reynolds
2020-02-26Minor cleaning of smt2 parser (#3823)Andrew Reynolds
2020-02-24Fix bugs related to printing Sygus commands (#3804)Abdalrhman Mohamed
2020-02-17Using ParseOp in TPTP (#3764)Haniel Barbosa
2020-02-17Support dumping Sygus commands. (#3763)Abdalrhman Mohamed
2020-02-14Remove quantifiers rewrite rules infrastructure (#3754)Andrew Reynolds
2020-02-13Update sygus v1 parser to use ParseOp utility (#3756)Andrew Reynolds
2019-12-13Add support for set comprehension (#3312)Andrew Reynolds
2019-12-06Add ExprManager as argument to Datatype (#3535)Andrew Reynolds
2019-11-29improving parsing error messages related to HOL (#3510)Haniel Barbosa
2019-11-29Check free variables in assertions when using SyGuS (#3504)Andrew Reynolds
2019-11-04Avoid non-well-founded sygus grammars (#3434)Andrew Reynolds
2019-10-11Check that logic is set when synth-fun command is encountered (#3384)Andrew Reynolds
2019-10-07[SMT2 Parser] Move code of `rewriterulesCommand` (#3334)Andres Noetzli
2019-10-03[SMT2 Parser] Move code of `sygusCommand` (#3335)Andres Noetzli
2019-09-29Avoid cases of empty sygus grammars (#3301)Andrew Reynolds
2019-09-27Support smt2 language "match" term (#3258)Andrew Reynolds
2019-09-13Disallow let in sygus grammars, check for free variables in sygus constructor...Andrew Reynolds
2019-09-06Remove parsing/printing of meta-info command. (#3260)Mathias Preiner
2019-09-06Remove SMT1 parser. (#3228)Mathias Preiner
2019-08-17 Cleaning make bound var in smt2 parser (#3192)Andrew Reynolds
2019-08-13Introduce smt2 parsing utility ParseOp and refactor (#3165)Andrew Reynolds
2019-08-12Clean smt2 parsing of named attributes (#3172)Andrew Reynolds
2019-08-10Simplify how defined functions are tracked during parsing (#3177)Andrew Reynolds
2019-08-06Properly parse qualified identifiers (#3111)Andrew Reynolds
2019-07-29Model blocker feature (#3112)Andrew Reynolds
2019-07-29Support get-abduct smt2 command (#3122)Andrew Reynolds
2019-07-01Support sygus version 2 format (#3066)Andrew Reynolds
2019-06-21Fix and simplify handling of --force-logic (#3062)Andres Noetzli
2019-06-12Refactor parser to define fewer tokens for symbols (#2936)Andres Noetzli
2019-06-11Do not require sygus constructors to be flattened (#3049)Andrew Reynolds
2019-04-29Eliminate APPLY kind (#2976)Andrew Reynolds
2019-04-25New C++ API: Clean up API: mkVar vs mkConst vs mkBoundVar. (#2977)Aina Niemetz
2019-04-16Make bv{add,mul,and,or,xor,xnor} left-associative (#2955)Andres Noetzli
2019-03-26Update copyright headers.Aina Niemetz
2019-03-19Make declare-datatype(s) a standard, non-extended command in the Smt2 parser....Andrew Reynolds
2019-03-18New C++: Remove redundant mkVar function.Aina Niemetz
2019-01-10New C++ API: Get rid of mkConst functions (simplify API). (#2783)Aina Niemetz
2019-01-03API/Smt2 parser: refactor termAtomic (#2674)Andres Noetzli
2018-11-27Reduce lookahead when parsing string literals (#2721)Andres Noetzli
2018-10-20Remove antlr_undefines.h. (#2664)Mathias Preiner
2018-10-18Introducing internal commands for SyGuS commands (#2627)Haniel Barbosa
2018-09-26Makes SyGuS parsing more robust in invariant problems (#2509)Haniel Barbosa
2018-08-27Make division chainable in the smt2 parser (#2367)Andrew Reynolds
2018-08-20 Remove support for prototype (non-sygus) synthesis (#2338)Andrew Reynolds
2018-08-17Split sygus grammar to its own ANTLR grammar (#2307)Andrew Reynolds
2018-08-07Simplify and improve the sygus parser (#2266)Andrew Reynolds
2018-08-06Remove support for Enum sygus syntax. (#2264)Andrew Reynolds
2018-08-02Parse standard separation logic inputs (#2257)Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback