summaryrefslogtreecommitdiff
path: root/src/parser
AgeCommit message (Expand)Author
2019-12-06Add ExprManager as argument to Datatype (#3535)Andrew Reynolds
2019-12-02OpTerm Refactor: Allow retrieving OpTerm used to create Term in public C++ AP...makaimann
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-25Better front-end type checking for SyGuS (#3496)Andrew Reynolds
2019-11-18Use -Wimplicit-fallthrough (#3464)Andres Noetzli
2019-11-15Fix wrong kind in sygus version 1 parser (#3463)Andrew Reynolds
2019-11-13Allow (set-logic ...) after (reset) (#3457)Andres Noetzli
2019-11-04Avoid non-well-founded sygus grammars (#3434)Andrew Reynolds
2019-10-27Fix global-declarations support (#3403)Andres Noetzli
2019-10-11Check that logic is set when synth-fun command is encountered (#3384)Andrew Reynolds
2019-10-10Make order of theories explicit in the source code. (#3379)Aina Niemetz
2019-10-08Avoid printing success for `--force-logic` (#3363)Andres Noetzli
2019-10-08[CVC Parser] Add support for regular expressions (#3346)Andres Noetzli
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-25Add isParameterized function to Expr (#3303)Andrew Reynolds
2019-09-25Use separate CMake project for CVC4 examples. (#3196)Mathias Preiner
2019-09-16parser: Improve error message for unrecognized input file format. (#3285)Aina Niemetz
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-26Remove unnecessary code from Cvc.g (#3213)Andrew Reynolds
2019-08-17 Cleaning make bound var in smt2 parser (#3192)Andrew Reynolds
2019-08-17Mark symbols introduced by named attributes as defined. (#3190)Andrew Reynolds
2019-08-14cmake: Export CVC4 library interface. (#3179)Mathias Preiner
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-31Parsing THF and adding several regressions (#3131)Haniel Barbosa
2019-07-29Model blocker feature (#3112)Andrew Reynolds
2019-07-29Support get-abduct smt2 command (#3122)Andrew Reynolds
2019-07-23Fix sygus datatype parsing in sygus v1 format (#3113)Andrew Reynolds
2019-07-16Add support for str.tolower and str.toupper (#3092)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-05-06Add support for re.all (#2980)Andres Noetzli
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-24Do not use __ prefix for header guards. (#2974)Mathias Preiner
2019-04-16Make bv{add,mul,and,or,xor,xnor} left-associative (#2955)Andres Noetzli
2019-03-28Fix issues in cvc parser (#2901)Andrew Reynolds
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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback