git.libre-soc.org Git - cvc5.git/history - src/printer/cvc/cvc

[cvc5.git] / src / printer / cvc / cvc_printer.cpp

2021-01-05	Andrew Reynolds	Remove a few miscellaneous references to the expr layer...	blob \| commitdiff \| raw
2020-12-03	Aina Niemetz	Update copyright headers.	blob \| commitdiff \| raw \| diff to current
2020-12-02	Andrew Reynolds	Use new let binding for cvc printer (#5561)	blob \| commitdiff \| raw \| diff to current
2020-11-25	Andrew Reynolds	Use symbol manager for printing responses get-model...	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-13	yoni206	Model declarations printing options (#5432)	blob \| commitdiff \| raw \| diff to current
2020-11-06	Andrew Reynolds	Simplify printing with respect to expression types...	blob \| commitdiff \| raw \| diff to current
2020-10-30	Andrew Reynolds	Update api::Sort to use TypeNode instead of Type (...	blob \| commitdiff \| raw \| diff to current
2020-10-29	mudathirmahgoub	Add mkInteger to the API (#5274)	blob \| commitdiff \| raw \| diff to current
2020-10-16	Andrew Reynolds	Refactor SMT-level model object (#5277)	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-09-11	Andrew Reynolds	Add witness to cvc printer. (#5057)	blob \| commitdiff \| raw \| diff to current
2020-09-04	Abdalrhman Mohamed	Use Result::Sat instead of BenchmarkStatus in printers...	blob \| commitdiff \| raw \| diff to current
2020-09-02	Abdalrhman Mohamed	Introduce an internal version of Commands. (#4988)	blob \| commitdiff \| raw \| diff to current
2020-08-26	Andrew Reynolds	Replace Expr-level datatype with Node-level DType ...	blob \| commitdiff \| raw \| diff to current
2020-08-18	Abdalrhman Mohamed	Refactor functions that print commands (Part 2) (#4905)	blob \| commitdiff \| raw \| diff to current
2020-08-06	Andrew Reynolds	Updates not related to creation for eliminating Expr...	blob \| commitdiff \| raw \| diff to current
2020-08-06	Andrew Reynolds	Split preprocessor from SmtEngine (#4854)	blob \| commitdiff \| raw \| diff to current
2020-07-14	Andres Noetzli	Use TypeNode/Node in ArrayStoreAll (#4728)	blob \| commitdiff \| raw \| diff to current
2020-07-13	Andres Noetzli	Remove ExprSequence (#4724)	blob \| commitdiff \| raw \| diff to current
2020-07-06	Andrew Reynolds	Front end support for sequences (#4690)	blob \| commitdiff \| raw \| diff to current
2020-06-16	Aina Niemetz	Update copyright headers.	blob \| commitdiff \| raw \| diff to current
2020-03-27	Andrew Reynolds	Support unicode internal representation and escape...	blob \| commitdiff \| raw \| diff to current
2020-03-18	Alex Ozdemir	Move node visitor class from smt_util/ to expr/ (#4110)	blob \| commitdiff \| raw \| diff to current
2020-03-08	Ying Sheng	Explicit end marker for models printed in the CVC langu...	blob \| commitdiff \| raw \| diff to current
2020-03-06	Andrew Reynolds	Simplify DatatypeDeclarationCommand command (#3928)	blob \| commitdiff \| raw \| diff to current
2020-03-05	Mathias Preiner	Enable -Wshadow and fix warnings. (#3909)	blob \| commitdiff \| raw \| diff to current
2020-02-27	Andres Noetzli	Fix -Wshadow warnings in common headers (#3826)	blob \| commitdiff \| raw \| diff to current
2020-02-20	Andrew Reynolds	Remove front-end support for Chain (#3767)	blob \| commitdiff \| raw \| diff to current
2019-12-16	Andrew Reynolds	Move Datatype management to ExprManager (#3568)	blob \| commitdiff \| raw \| diff to current
2019-12-13	Andrew Reynolds	Eliminate Expr-level calls in TypeNode (#3562)	blob \| commitdiff \| raw \| diff to current
2019-10-30	Mathias Preiner	Unify CVC4_CHECK/CVC4_DCHECK/AlwaysAssert/Assert. ...	blob \| commitdiff \| raw \| diff to current
2019-09-27	Andrew Reynolds	CVC print support for recoverable failure (#3323)	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
2019-01-22	Andrew Reynolds	Fix tuple and record CVC printing (#2818)	blob \| commitdiff \| raw \| diff to current
2019-01-03	Alex Ozdemir	[LRA proof] Recording & Printing LRA Proofs (#2758)	blob \| commitdiff \| raw \| diff to current
2018-06-26	Andres Noetzli	Minor improvements in SMT2 and CVC printers (#2089)	blob \| commitdiff \| raw \| diff to current
2018-06-25	Aina Niemetz	Updated copyright headers.	blob \| commitdiff \| raw \| diff to current
2018-06-25	Andres Noetzli	Remove parentheses for prefix ops without args (#2082)	blob \| commitdiff \| raw \| diff to current
2018-05-05	Andrew Reynolds	Fix handling of TO_REAL in cvc printer (#1876)	blob \| commitdiff \| raw \| diff to current
2018-05-05	Andrew Reynolds	Remove special case for record selector printing. ...	blob \| commitdiff \| raw \| diff to current
2018-05-04	Andres Noetzli	Fix printing of multiple datatypes (#1872)	blob \| commitdiff \| raw \| diff to current
2018-05-03	Andrew Reynolds	Fix cvc printer for nullary constructors (#1856)	blob \| commitdiff \| raw \| diff to current
2018-03-05	Aina Niemetz	Add support for check-sat-assuming. (#1637)	blob \| commitdiff \| raw \| diff to current
2018-02-05	Tim King	Cleaning up the printing of theory model representative...	blob \| commitdiff \| raw \| diff to current
2017-11-28	Tim King	Removing throw specifiers from internal Printer hierarc...	blob \| commitdiff \| raw \| diff to current
2017-10-27	Andrew Reynolds	Refactor theory model (#1236)	blob \| commitdiff \| raw \| diff to current
2017-07-13	Aina Niemetz	Merge pull request #188 from aniemetz/cx11	blob \| commitdiff \| raw \| diff to current
2017-07-12	ajreynol	Make type rules more strict for operators whose type...	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-04-20	Andrew Reynolds	Merge pull request #149 from PaulMeng/master	blob \| commitdiff \| raw \| diff to current
2017-04-20	Paul Meng	Support for relational operators identity and join...	blob \| commitdiff \| raw \| diff to current
2017-04-14	ajreynol	Fix nullary operator printers, minor.	blob \| commitdiff \| raw \| diff to current
2017-04-04	Clark Barrett	Merge pull request #141 from 4tXJ7f/remove_def	blob \| commitdiff \| raw \| diff to current
2017-04-03	Andrew Reynolds	Merge pull request #142 from timothy-king/nlAlgMerge	blob \| commitdiff \| raw \| diff to current
2017-04-03	Tim King	Adding a model based axiom instantiation scheme for...	blob \| commitdiff \| raw \| diff to current
2017-03-20	Andrew Reynolds	Merge pull request #135 from PaulMeng/master	blob \| commitdiff \| raw \| diff to current
2017-03-20	Paul Meng	fixed cvc4 parser for set complement	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
2017-01-18	Andrew Reynolds	Merge pull request #128 from 4tXJ7f/fix_lfsc_perf	blob \| commitdiff \| raw \| diff to current
2017-01-14	Clark Barrett	Merge pull request #130 from chadbrewbaker/master	blob \| commitdiff \| raw \| diff to current
2017-01-11	Clark Barrett	Merge pull request #129 from timothy-king/regression...	blob \| commitdiff \| raw \| diff to current
2017-01-11	Tim King	Adding regression test scrubbing.	blob \| commitdiff \| raw \| diff to current
2016-12-07	ajreynol	Added cardinality to cvc language, fixes bug 753. Throw...	blob \| commitdiff \| raw \| diff to current
2016-11-28	Clark Barrett	Merge pull request #112 from 4tXJ7f/fix_mult_distrib	blob \| commitdiff \| raw \| diff to current
2016-11-22	ajreynol	Fix smt2 and cvc printers for testers when output and...	blob \| commitdiff \| raw \| diff to current
2016-11-01	ajreynol	Make tuple and record names unique. Do not print intern...	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-26	Andrew Reynolds	Merge pull request #98 from 4tXJ7f/fix_dist_build	blob \| commitdiff \| raw \| diff to current
2016-10-26	ajreynol	New implementation of sets+cardinality. Merge Paul...	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-08-24	PaulMeng	Merge remote-tracking branch 'origin/master'	blob \| commitdiff \| raw \| diff to current
2016-08-20	Clark Barrett	Fixed two bugs	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-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	ajreynol	Eliminate most of the internal representation infrastru...	blob \| commitdiff \| raw \| diff to current
2016-02-09	PaulMeng	- extend cvc4 frontend parser to accept relational...	blob \| commitdiff \| raw \| diff to current
2016-02-02	Tim King	Moving dump., command., model.*, and ite_removal...	blob \| commitdiff \| raw \| diff to current
2015-12-15	Tim King	Breaking the include cycle between Record and Expr.	blob \| commitdiff \| raw \| diff to current
2015-12-15	Tim King	Refactoring Options Handler & Library Cycle Breaking	blob \| commitdiff \| raw \| diff to current
2014-11-27	Tianyi Liang	Merge branch 'master' of github.com:tiliang/CVC4	blob \| commitdiff \| raw \| diff to current
2014-11-17	Liana Hadarean	Resource-limiting work.	blob \| commitdiff \| raw \| diff to current
2014-11-10	Morgan Deters	Merge branch '1.4.x'	blob \| commitdiff \| raw \| diff to current
2014-11-07	Morgan Deters	Merge branch '1.4.x'	blob \| commitdiff \| raw \| diff to current
2014-11-07	Morgan Deters	Merge branch '1.4.x'	blob \| commitdiff \| raw \| diff to current
2014-11-07	Morgan Deters	Merge branch '1.4.x'	blob \| commitdiff \| raw \| diff to current
2014-11-05	Morgan Deters	Merge branch '1.4.x'	blob \| commitdiff \| raw \| diff to current
2014-10-23	Morgan Deters	Parsing and infrastructure support for SMT-LIBv2.5...	blob \| commitdiff \| raw \| diff to current
2014-10-17	Morgan Deters	Merge branch '1.4.x'	blob \| commitdiff \| raw \| diff to current
next

RSS Atom