summaryrefslogtreecommitdiff
path: root/src/parser/smt2/Smt2.g
AgeCommit message (Expand)Author
2020-08-25Replace Expr-level datatype with Node-level DType (#4875)Andrew Reynolds
2020-08-04Modify the smt2 parser to use the Sygus grammar. (#4829)Abdalrhman Mohamed
2020-07-13Debug instantiations output (#4739)Andrew Reynolds
2020-07-13Statistics on instantiations per quantified formula. (#4719)Andrew Reynolds
2020-07-06Front end support for sequences (#4690)Andrew Reynolds
2020-06-30Interpolation step 1 (#4638)Ying Sheng
2020-06-25Remove sygus1 parser (#4651)Andrew Reynolds
2020-06-18Add logic check for define-fun(s)-rec (#4577)Andres Noetzli
2020-06-16Update copyright headers.Aina Niemetz
2020-06-06Keep definitions when global-declarations enabled (#4572)Andres Noetzli
2020-06-05Smt2 parsing support for nested recursive datatypes (#4575)Andrew Reynolds
2020-06-04Add a method for retrieving base of a constant array through API (#4494)makaimann
2020-06-03New C++ Api: First batch of API guards. (#4557)Aina Niemetz
2020-06-03Do not apply unconstrained simplification when quantifiers are present (#4532)Andrew Reynolds
2020-06-02New C++ API: Keep reference to solver object in non-solver objects. (#4549)Aina Niemetz
2020-06-01Do not parse ->/lambda unless --uf-ho enabled (#4544)Andres Noetzli
2020-05-19Renamed operator CHOICE to WITNESS (#4207)mudathirmahgoub
2020-04-03New C++ API: Remove Op::getSort(). (#4208)Aina Niemetz
2020-03-31Support char smt-lib syntax (#4188)Andrew Reynolds
2020-03-30Frontend support for the choice operator (#4175)mudathirmahgoub
2020-03-28Stop printing datatype declaration for Sygus V1 grammar. (#4168)Abdalrhman Mohamed
2020-03-27Support unicode internal representation and escape sequences (#3852)Andrew Reynolds
2020-03-20Parse error for SyGuS version 1.0 vs 2.0 (#4057)Andrew Reynolds
2020-03-18Only allow bv2nat/int2bv with BV and integer logic (#4118)Andres Noetzli
2020-03-12Convert most instances of dataypes in parsers to the new API (#4054)Andrew Reynolds
2020-03-09Clean up more uses of ExprManager in parsers (#3932)Andrew Reynolds
2020-03-06Simplify DatatypeDeclarationCommand command (#3928)Andrew Reynolds
2020-03-06Remove tester name from APIs (#3929)Andrew Reynolds
2020-03-06Make sygus datatype building independent of parser in sygus v2 (#3923)Andrew Reynolds
2020-03-05Migrate a majority of the functionality in parsers to the new API (#3838)Andrew Reynolds
2020-03-05Enable -Wshadow and fix warnings. (#3909)Mathias Preiner
2020-02-27Refactor operator applications in the parser (#3831)Andrew Reynolds
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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback