summaryrefslogtreecommitdiff
path: root/src/printer/smt2/smt2_printer.cpp
AgeCommit message (Expand)Author
2016-08-24Merge remote-tracking branch 'origin/master'PaulMeng
2016-07-20Infrastructure for storing and printing heap models for separation logic. Ens...ajreynol
2016-07-06Add comment field for model, resolves hack for printing sep logic models.ajreynol
2016-07-05Merge branch 'master' of https://github.com/CVC4/CVC4.gitPaulMeng
2016-06-17Cleanup from last commit, treat sep.nil as variable kind.ajreynol
2016-06-17Support for separation logic. Enable cbqi by default for pure BV.ajreynol
2016-05-06Minor clean up, fixes related to sygus.ajreynol
2016-04-20update from the masterPaulMeng
2016-04-15change transitive closure operator name to TCLOUSREPaulMeng
2016-04-09cardinality operation for finite sets (based on my thesis / ijcar16 paper)Kshitij Bansal
2016-04-03Updating the copyright headers and scripts.Tim King
2016-03-23squash-merge from proof branchGuy
2016-02-15Merge remote-tracking branch 'origin/master'PaulMeng
2016-02-15extended smt parser for the finite relationsPaulMeng
2016-02-15Eliminate most of the internal representation infrastructure for tuples and r...ajreynol
2015-12-18Modifying emptyset.h and sexpr. Adding SetLanguage.Tim King
2015-12-14Refactoring Options Handler & Library Cycle BreakingTim King
2015-11-26Front-end support for get-value of sort cardinality, minor fixes for sygus so...ajreynol
2015-10-15Change semantics of str.substr to allow endpoint out of bounds, and return em...ajreynol
2015-07-20Squashed merge of SygusComp 2015 branch.ajreynol
2015-06-30fix smt2 parameterized sort printingKshitij Bansal
2015-06-12Make sygus an output language. Parse declare-fun in sygus. Minor improvemen...ajreynol
2015-04-28Fix smt2 printing of fun-def. Simplification of mbqi interface.ajreynol
2015-03-28printer change for string smtlib2Tianyi Liang
2015-01-19Adding tests for get-value output for arithmetic.Tim King
2015-01-11adjusted to both v2.0 and v2.5 string literalsTianyi Liang
2015-01-09blocked unprintable characters in string literals;Tianyi Liang
2015-01-08switch ascii encoding to unsigned charTianyi Liang
2014-12-06Added C++/Java api examples;Tianyi Liang
2014-12-03Floating point infrastructure.Martin Brain
2014-11-17Resource-limiting work.Liana Hadarean
2014-10-23Parsing and infrastructure support for SMT-LIBv2.5 input and output languages.Morgan Deters
2014-10-06Print array constants in SMT-LIB models with new syntax.Morgan Deters
2014-10-06Support for RESET command in CVC native language (and infrastructure for supp...Morgan Deters
2014-10-03Merge branch '1.4.x'Morgan Deters
2014-10-03Fix output of integer-valued real constants in SMT-LIB models (thanks Christo...Morgan Deters
2014-08-26Improved SMT-LIBv2 language support for unsat cores.Morgan Deters
2014-08-23Unsat core printing.Morgan Deters
2014-08-22Unsat core infrastruture and API (SMT-LIB compliance to come).Morgan Deters
2014-08-22Fix operator-printing issue in SMT2.Morgan Deters
2014-07-01Update copyrights.Morgan Deters
2014-06-30Merge pull request #47 from kbansal/setsKshitij Bansal
2014-06-29sets: "insert" operatorKshitij Bansal
2014-06-25rename subseteq to subset in smtlib, all kinds and smt operator names are now...Kshitij Bansal
2014-06-22Renaming of SMT2 operator names, kinds for set theoryKshitij Bansal
2014-06-22Output language "cvc3" (as opposed to "cvc" or "cvc4") produces output for CVC3:Morgan Deters
2014-06-22Minor cleanup stuff.Morgan Deters
2014-06-21Some minor cleanup and documentation.Morgan Deters
2014-06-19For casc : print models of functions rewritten by sort inference.ajreynol
2014-06-06Sets translate, and other short fixesKshitij Bansal
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback