git.libre-soc.org Git - cvc5.git/history

[cvc5.git] / src / parser / smt2 / smt2.h

2021-11-02	Andrew Reynolds	Improve syntax for fmf cardinality constraints (#7556)	blob \| commitdiff \| raw
2021-10-14	Andrew Reynolds	Improve parser for tuple select (#7364)	blob \| commitdiff \| raw \| diff to current
2021-09-22	Andrew Reynolds	Minimal fixing version for tuple update parsing (#7228)	blob \| commitdiff \| raw \| diff to current
2021-09-01	Gereon Kremer	No longer use direct access to options in driver (...	blob \| commitdiff \| raw \| diff to current
2021-08-27	Gereon Kremer	Handle languages as strings in driver (#7074)	blob \| commitdiff \| raw \| diff to current
2021-08-26	Gereon Kremer	Consolidate language types (#7065)	blob \| commitdiff \| raw \| diff to current
2021-06-03	Andrew Reynolds	Simplify automatic set-logic in smt2 parser (#6678)	blob \| commitdiff \| raw \| diff to current
2021-05-14	Andres Noetzli	Decouple parser creation from input selection (#6533)	blob \| commitdiff \| raw \| diff to current
2021-04-19	Gereon Kremer	Remove linking against gmp and cln in tests and parser...	blob \| commitdiff \| raw \| diff to current
2021-04-14	Aina Niemetz	Rename public and private headers in src/include. ...	blob \| commitdiff \| raw \| diff to current
2021-04-12	Aina Niemetz	Refactor and update copyright headers. (#6316)	blob \| commitdiff \| raw \| diff to current
2021-04-09	Aina Niemetz	Rename CVC4__ header guards to CVC5__. (#6326)	blob \| commitdiff \| raw \| diff to current
2021-04-06	Aina Niemetz	New C++ Api: Rename and move headers. (#6292)	blob \| commitdiff \| raw \| diff to current
2021-04-01	Aina Niemetz	Rename namespace CVC5 to cvc5. (#6258)	blob \| commitdiff \| raw \| diff to current
2021-03-31	Aina Niemetz	Rename namespace CVC4 to CVC5. (#6249)	blob \| commitdiff \| raw \| diff to current
2021-03-18	Abdalrhman Mohamed	Eliminate more uses of SExpr. (#6149)	blob \| commitdiff \| raw \| diff to current
2021-03-09	Aina Niemetz	Update copyright headers to 2021. (#6081)	blob \| commitdiff \| raw \| diff to current
2021-03-06	Mathias Preiner	Remove SMT-LIB 2.5 and 2.0 support. (#6068)	blob \| commitdiff \| raw \| diff to current
2020-12-03	Andrew Reynolds	Refactor handling of global declarations (#5577)	blob \| commitdiff \| raw \| diff to current
2020-11-30	Abdalrhman Mohamed	Eliminate uses of SExpr from the parser. (#5496)	blob \| commitdiff \| raw \| diff to current
2020-11-18	Andrew Reynolds	Use symbol manager for get assignment (#5451)	blob \| commitdiff \| raw \| diff to current
2020-11-16	Andrew Reynolds	Cleaning up scopes in preparation for symbol manager...	blob \| commitdiff \| raw \| diff to current
2020-11-09	Andrew Reynolds	Add symbol manager (#5380)	blob \| commitdiff \| raw \| diff to current
2020-10-27	Abdalrhman Mohamed	Refactor DeclareSygusVarCommand and SynthFunCommand...	blob \| commitdiff \| raw \| diff to current
2020-10-09	Andres Noetzli	reset-assertions: Remove all non-global symbols in...	blob \| commitdiff \| raw \| diff to current
2020-09-22	Mathias Preiner	Update copyright header script to support CMake and...	blob \| commitdiff \| raw \| diff to current
2020-09-16	Abdalrhman Mohamed	Dump commands in internal code using command printing...	blob \| commitdiff \| raw \| diff to current
2020-08-04	Abdalrhman Mohamed	Modify the smt2 parser to use the Sygus grammar. (...	blob \| commitdiff \| raw \| diff to current
2020-06-25	Andrew Reynolds	Remove sygus1 parser (#4651)	blob \| commitdiff \| raw \| diff to current
2020-06-16	Aina Niemetz	Update copyright headers.	blob \| commitdiff \| raw \| diff to current
2020-06-01	Andres Noetzli	Do not parse ->/lambda unless --uf-ho enabled (#4544)	blob \| commitdiff \| raw \| diff to current
2020-03-28	Abdalrhman Mohamed	Change is-cons to (_ is cons) in Sygus benchmarks....	blob \| commitdiff \| raw \| diff to current
2020-03-19	Andres Noetzli	Only allow bv2nat/int2bv with BV and integer logic...	blob \| commitdiff \| raw \| diff to current
2020-03-12	Andrew Reynolds	Convert most instances of dataypes in parsers to the...	blob \| commitdiff \| raw \| diff to current
2020-03-06	Andrew Reynolds	Remove tester name from APIs (#3929)	blob \| commitdiff \| raw \| diff to current
2020-03-05	Andrew Reynolds	Migrate a majority of the functionality in parsers...	blob \| commitdiff \| raw \| diff to current
2020-02-27	Andrew Reynolds	Update purifySygusGTerm to the new API (#3830)	blob \| commitdiff \| raw \| diff to current
2020-02-26	Andrew Reynolds	Refactor type ascriptions in the parser (#3825)	blob \| commitdiff \| raw \| diff to current
2020-02-26	Andrew Reynolds	Minor cleaning of smt2 parser (#3823)	blob \| commitdiff \| raw \| diff to current
2020-02-14	Andrew Reynolds	Remove quantifiers rewrite rules infrastructure (#3754)	blob \| commitdiff \| raw \| diff to current
2020-02-14	Andrew Reynolds	Update sygus v1 parser to use ParseOp utility (#3756)	blob \| commitdiff \| raw \| diff to current
2020-01-07	Andrew Reynolds	Fix unary minus parse check (#3594)	blob \| commitdiff \| raw \| diff to current
2019-12-06	Andrew Reynolds	Add ExprManager as argument to Datatype (#3535)	blob \| commitdiff \| raw \| diff to current
2019-12-02	makaimann	OpTerm Refactor: Allow retrieving OpTerm used to create...	blob \| commitdiff \| raw \| diff to current
2019-10-08	Andres Noetzli	[SMT2 Parser] Move code of `rewriterulesCommand` (...	blob \| commitdiff \| raw \| diff to current
2019-10-03	Andres Noetzli	[SMT2 Parser] Move code of `sygusCommand` (#3335)	blob \| commitdiff \| raw \| diff to current
2019-09-13	Andrew Reynolds	Disallow let in sygus grammars, check for free variable...	blob \| commitdiff \| raw \| diff to current
2019-09-06	Mathias Preiner	Remove SMT1 parser. (#3228)	blob \| commitdiff \| raw \| diff to current
2019-08-13	Andrew Reynolds	Introduce smt2 parsing utility ParseOp and refactor...	blob \| commitdiff \| raw \| diff to current
2019-08-12	Andrew Reynolds	Clean smt2 parsing of named attributes (#3172)	blob \| commitdiff \| raw \| diff to current
2019-07-01	Andrew Reynolds	Support sygus version 2 format (#3066)	blob \| commitdiff \| raw \| diff to current
2019-06-21	Andres Noetzli	Fix and simplify handling of --force-logic (#3062)	blob \| commitdiff \| raw \| diff to current
2019-06-12	Andres Noetzli	Refactor parser to define fewer tokens for symbols...	blob \| commitdiff \| raw \| diff to current
2019-04-24	Mathias Preiner	Do not use __ prefix for header guards. (#2974)	blob \| commitdiff \| raw \| diff to current
2019-04-16	Andres Noetzli	Make bv{add,mul,and,or,xor,xnor} left-associative ...	blob \| commitdiff \| raw \| diff to current
2019-03-26	Aina Niemetz	Update copyright headers.	blob \| commitdiff \| raw \| diff to current
2018-11-27	Andres Noetzli	Reduce lookahead when parsing string literals (#2721)	blob \| commitdiff \| raw \| diff to current
2018-10-18	Haniel Barbosa	Introducing internal commands for SyGuS commands (...	blob \| commitdiff \| raw \| diff to current
2018-09-26	Haniel Barbosa	Makes SyGuS parsing more robust in invariant problems...	blob \| commitdiff \| raw \| diff to current
2018-08-09	Aina Niemetz	Plug solver API object into parser. (#2240)	blob \| commitdiff \| raw \| diff to current
2018-07-14	Andrew Reynolds	sygusComp2018: update semantics for declare-fun in...	blob \| commitdiff \| raw \| diff to current
2018-06-25	Aina Niemetz	Updated copyright headers.	blob \| commitdiff \| raw \| diff to current
2018-06-05	Andres Noetzli	Only enable transcendentals if logic is N[I]RAT (#2052)	blob \| commitdiff \| raw \| diff to current
2018-05-29	Andres Noetzli	Make user's SMT2 version override file version (#2004)	blob \| commitdiff \| raw \| diff to current
2018-05-29	Andres Noetzli	Track input language in a single place (#2003)	blob \| commitdiff \| raw \| diff to current
2018-05-03	Andrew Reynolds	Initial support for string standard in smt lib 2.6...	blob \| commitdiff \| raw \| diff to current
2018-03-05	Mathias Preiner	Enable -Wsuggest-override by default. (#1643)	blob \| commitdiff \| raw \| diff to current
2018-01-06	Tim King	Removing throw specifiers from src/parser/. (#1486)	blob \| commitdiff \| raw \| diff to current
2017-12-07	Andrew Reynolds	Add command for define-fun-rec and add to API (#1412)	blob \| commitdiff \| raw \| diff to current
2017-11-24	Andrew Reynolds	Ho parsing and regressions (#1350)	blob \| commitdiff \| raw \| diff to current
2017-11-22	Andrew Reynolds	Sygus Lambda Grammars (#1390)	blob \| commitdiff \| raw \| diff to current
2017-10-11	Andrew Reynolds	Move unsat core names to smt engine (#1192)	blob \| commitdiff \| raw \| diff to current
2017-10-03	Andrew Reynolds	Op overload parser (#1162)	blob \| commitdiff \| raw \| diff to current
2017-07-21	Tim King	Merge branch 'master' into cleanup-regexp	blob \| commitdiff \| raw \| diff to current
2017-07-21	Tim King	Moving from the gnu extensions for hash maps to the...	blob \| commitdiff \| raw \| diff to current
2017-07-10	ajreynol	Merge datatype shared selectors/sygus comp 2017 branch...	blob \| commitdiff \| raw \| diff to current
2017-07-07	Mathias Preiner	Update copyright headers.	blob \| commitdiff \| raw \| diff to current
2017-03-16	ajreynol	Parsing support for SMT LIB 2.6. Minor fixes for printi...	blob \| commitdiff \| raw \| diff to current
2016-11-16	Clark Barrett	Merge pull request #108 from timothy-king/smt2-parser...	blob \| commitdiff \| raw \| diff to current
2016-11-14	Tim King	Adding garbage collection for the Smt2 Parser for Comma...	blob \| commitdiff \| raw \| diff to current
2016-11-01	ajreynol	Revert change to datatypes API for passing pointers...	blob \| commitdiff \| raw \| diff to current
2016-11-01	ajreynol	Working memory leak free version, changes interface...	blob \| commitdiff \| raw \| diff to current
2016-07-05	PaulMeng	Merge branch 'master' of https://github.com/CVC4/CVC4.git	blob \| commitdiff \| raw \| diff to current
2016-06-20	Guy	Merge branch 'master' of https://github.com/CVC4/CVC4	blob \| commitdiff \| raw \| diff to current
2016-06-17	ajreynol	Support for separation logic. Enable cbqi by default...	blob \| commitdiff \| raw \| diff to current
2016-04-20	PaulMeng	update from the master	blob \| commitdiff \| raw \| diff to current
2016-04-09	Guy	Merge branch 'master' of https://github.com/CVC4/CVC4	blob \| commitdiff \| raw \| diff to current
2016-04-04	Tim King	Updating the copyright headers and scripts.	blob \| commitdiff \| raw \| diff to current
2016-01-28	Tim King	Adding listeners to Options.	blob \| commitdiff \| raw \| diff to current
2015-07-31	ajreynol	Sygus support for inductive datatypes.	blob \| commitdiff \| raw \| diff to current
2015-07-28	Tianyi Liang	Merge branch 'master' of https://github.com/CVC4/CVC4	blob \| commitdiff \| raw \| diff to current
2015-07-20	ajreynol	Squashed merge of SygusComp 2015 branch.	blob \| commitdiff \| raw \| diff to current
2015-06-11	ajreynol	Handle duplicate operators in sygus grammars. Parse...	blob \| commitdiff \| raw \| diff to current
2015-06-11	ajreynol	Update experimental scripts. Support top-level non...	blob \| commitdiff \| raw \| diff to current
2015-06-10	ajreynol	Support for printing solutions involving LetGTerm sygus...	blob \| commitdiff \| raw \| diff to current
2015-06-10	ajreynol	Parse support for sygus LetGTerm.	blob \| commitdiff \| raw \| diff to current
2015-06-03	ajreynol	Refactoring of sygus parsing, properly parse Constant...	blob \| commitdiff \| raw \| diff to current
2015-05-12	barrettcw	Merge pull request #74 from finnhaedicke/namespace_minisat	blob \| commitdiff \| raw \| diff to current
2015-05-11	ajreynol	Allow sygus with no syntactic restrictions for LIA...	blob \| commitdiff \| raw \| diff to current
2015-05-11	ajreynol	Support for arbitrary constants/variables in Sygus...	blob \| commitdiff \| raw \| diff to current
next

RSS Atom