git.libre-soc.org Git - cvc5.git/history - src/parser/smt2/smt2.cpp

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

2019-07-29	Andrew Reynolds	Support get-abduct smt2 command (#3122)	blob \| commitdiff \| raw
2019-07-23	Andrew Reynolds	Fix sygus datatype parsing in sygus v1 format (#3113)	blob \| commitdiff \| raw \| diff to current
2019-07-16	Andrew Reynolds	Add support for str.tolower and str.toupper (#3092)	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-05-06	Andres Noetzli	Add support for re.all (#2980)	blob \| commitdiff \| raw \| diff to current
2019-04-30	Andrew Reynolds	Eliminate APPLY kind (#2976)	blob \| commitdiff \| raw \| diff to current
2019-03-26	Aina Niemetz	Update copyright headers.	blob \| commitdiff \| raw \| diff to current
2018-11-21	Andrew Reynolds	Support string replace all (#2704)	blob \| commitdiff \| raw \| diff to current
2018-10-18	Haniel Barbosa	Introducing internal commands for SyGuS commands (...	blob \| commitdiff \| raw \| diff to current
2018-10-03	Andres Noetzli	Allow (_ to_fp ...) in strict parsing mode (#2566)	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-22	Andrew Reynolds	Fix processing of nested Variable construct in sygus...	blob \| commitdiff \| raw \| diff to current
2018-08-21	Andrew Reynolds	Warn and enable quantifiers when using sygus + logics...	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-08-07	Andrew Reynolds	Add RegLan to smt2/sygus parsers. (#2276)	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	Track input language in a single place (#2003)	blob \| commitdiff \| raw \| diff to current
2018-05-22	Andrew Reynolds	Parse error for sygus grammar term with multiple let...	blob \| commitdiff \| raw \| diff to current
2018-05-08	Andrew Reynolds	Support for str.<= and str.< (#1882)	blob \| commitdiff \| raw \| diff to current
2018-05-07	Andrew Reynolds	Add support for str.code (#1821)	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-07	Mathias Preiner	Make statistics output consistent. (#1647)	blob \| commitdiff \| raw \| diff to current
2018-02-28	Aina Niemetz	Remove unused code in pushDefineFunRecScop in smt2...	blob \| commitdiff \| raw \| diff to current
2018-02-07	Andrew Reynolds	Add remaining transcendental functions (#1551)	blob \| commitdiff \| raw \| diff to current
2017-12-28	Arjun Viswanathan	Rel smt parser (#1446)	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-12-01	Andres Noetzli	Fix reset-assertions (#1413)	blob \| commitdiff \| raw \| diff to current
2017-12-01	Andrew Reynolds	Refactor and generalize PBE strategies (#1410)	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-11-05	Andrew Reynolds	Make higher-order a flag in logic info. (#1318)	blob \| commitdiff \| raw \| diff to current
2017-10-20	Andrew Reynolds	Make Sygus conjectures higher-order (#1244)	blob \| commitdiff \| raw \| diff to current
2017-10-12	Andrew Reynolds	Sygus logics (#1226)	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-10	Andrew Reynolds	Split term database (#1206)	blob \| commitdiff \| raw \| diff to current
2017-10-03	Andrew Reynolds	Op overload parser (#1162)	blob \| commitdiff \| raw \| diff to current
2017-09-05	Andrew Reynolds	Remove support for conversions between uint32/uint16...	blob \| commitdiff \| raw \| diff to current
2017-08-25	Aina Niemetz	Added missing includes (algorithm).	blob \| commitdiff \| raw \| diff to current
2017-07-10	ajreynol	Merge ntExt branch. Adds support for transcendental...	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-07-05	ajreynol	Non-linear supported in ALL logics. Minor fixes for...	blob \| commitdiff \| raw \| diff to current
2017-03-07	ajreynol	More fixes for printing/parsing sets, fix kind name.	blob \| commitdiff \| raw \| diff to current
2017-03-06	ajreynol	Support for set compliment and universe set. Simplify...	blob \| commitdiff \| raw \| diff to current
2017-03-02	ajreynol	Eliminate Boolean term conversion. Generalizes removeIT...	blob \| commitdiff \| raw \| diff to current
2016-11-18	Clark Barrett	Merge pull request #110 from 4tXJ7f/fix_makefiles	blob \| commitdiff \| raw \| diff to current
2016-11-18	Clark Barrett	Add support for set-logic ALL, fix compiler error in...	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-10-13	Tim King	Revert "Merge branch 'origin' of https://github.com...	blob \| commitdiff \| raw \| diff to current
2016-10-11	Paul Meng	Merge branch 'origin' of https://github.com/CVC4/CVC4.git	blob \| commitdiff \| raw \| diff to current
2016-09-14	ajreynol	Support for unique variable generation in node manager.	blob \| commitdiff \| raw \| diff to current
2016-08-24	PaulMeng	Merge remote-tracking branch 'origin/master'	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	Cleanup from last commit, treat sep.nil as variable...	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-05-05	ajreynol	Compute term indices lazily in TermDb. Optimization...	blob \| commitdiff \| raw \| diff to current
2016-04-20	PaulMeng	update from the master	blob \| commitdiff \| raw \| diff to current
2016-04-15	PaulMeng	change transitive closure operator name to TCLOUSRE	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-09	Kshitij Bansal	cardinality operation for finite sets (based on my...	blob \| commitdiff \| raw \| diff to current
2016-04-04	Tim King	Updating the copyright headers and scripts.	blob \| commitdiff \| raw \| diff to current
2016-02-15	PaulMeng	Merge remote-tracking branch 'origin/master'	blob \| commitdiff \| raw \| diff to current
2016-02-15	PaulMeng	extended smt parser for the finite relations	blob \| commitdiff \| raw \| diff to current
2016-02-02	Tim King	Moving dump., command., model.*, and ite_removal...	blob \| commitdiff \| raw \| diff to current
2016-01-28	Tim King	Adding listeners to Options.	blob \| commitdiff \| raw \| diff to current
2015-12-15	Tim King	Refactoring Options Handler & Library Cycle Breaking	blob \| commitdiff \| raw \| diff to current
2015-09-18	ajreynol	More work mixing UF and sygus.	blob \| commitdiff \| raw \| diff to current
2015-08-01	ajreynol	Simplification/improvement to solving deltas in LRA...	blob \| commitdiff \| raw \| diff to current
2015-08-01	ajreynol	Support for default grammar for datatypes in sygus...	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-25	ajreynol	Add option --sygus-inv-templ for synthesizing strengthe...	blob \| commitdiff \| raw \| diff to current
2015-07-20	ajreynol	Squashed merge of SygusComp 2015 branch.	blob \| commitdiff \| raw \| diff to current
2015-06-12	ajreynol	Make sygus an output language. Parse declare-fun in...	blob \| commitdiff \| raw \| diff to current
2015-06-12	ajreynol	Accelerate sygus solution reconstruction for constants...	blob \| commitdiff \| raw \| diff to current
2015-06-11	ajreynol	Avoid naming conflicts in sygus, refactor. Add missing...	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-06-02	ajreynol	Flatten sygus grammars during parsing. Remove duplicate...	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
2015-04-23	Clark Barrett	Merge branch 'master' into google	blob \| commitdiff \| raw \| diff to current
2015-04-23	Liana Hadarean	Added option for --check-unsat-cores and various core...	blob \| commitdiff \| raw \| diff to current
2015-04-22	Kshitij Bansal	Merge pull request #73 from kbansal/parser-dont-tokenize	blob \| commitdiff \| raw \| diff to current
2015-04-17	Kshitij Bansal	Merge pull request #72 from kbansal/decision-requirephase	blob \| commitdiff \| raw \| diff to current
2015-04-16	ajreynol	Handle (degenerate) case of synthesis conjectures for...	blob \| commitdiff \| raw \| diff to current
2015-04-16	Kshitij Bansal	string parser builtinop changes	blob \| commitdiff \| raw \| diff to current
2015-04-16	Kshitij Bansal	fp builtinop parser changes	blob \| commitdiff \| raw \| diff to current
2015-04-16	Kshitij Bansal	THEORY_INTS parser changes	blob \| commitdiff \| raw \| diff to current
2015-04-16	Kshitij Bansal	THEORY_REAL_INTS parser changes	blob \| commitdiff \| raw \| diff to current
next

RSS Atom