summaryrefslogtreecommitdiff
path: root/src/printer/cvc/cvc_printer.cpp
AgeCommit message (Expand)Author
2017-03-20fixed cvc4 parser for set complementPaul Meng
2017-03-07More fixes for printing/parsing sets, fix kind name.ajreynol
2017-03-06Support for set compliment and universe set. Simplify approach for sep.nil no...ajreynol
2017-03-02Eliminate Boolean term conversion. Generalizes removeITE pass to remove Boole...ajreynol
2017-01-10Adding regression test scrubbing.Tim King
2016-12-07Added cardinality to cvc language, fixes bug 753. Throw logic exception when ...ajreynol
2016-11-22Fix smt2 and cvc printers for testers when output and input languages are dif...ajreynol
2016-11-01Make tuple and record names unique. Do not print internal datatype declaratio...ajreynol
2016-11-01Working memory leak free version, changes interface to pointers.ajreynol
2016-10-26New implementation of sets+cardinality. Merge Paul Meng's relation solver as...ajreynol
2016-10-13Revert "Merge branch 'origin' of https://github.com/CVC4/CVC4.git"Tim King
2016-08-24Merge remote-tracking branch 'origin/master'PaulMeng
2016-08-19Fixed two bugsClark Barrett
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-02-15Merge remote-tracking branch 'origin/master'PaulMeng
2016-02-15Eliminate most of the internal representation infrastructure for tuples and r...ajreynol
2016-02-09- extend cvc4 frontend parser to accept relational operators (product,PaulMeng
2016-02-02Moving dump.*, command.*, model.*, and ite_removal.* from smt_util/ to smt/. ...Tim King
2015-12-15Breaking the include cycle between Record and Expr.Tim King
2015-12-14Refactoring Options Handler & Library Cycle BreakingTim King
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-08Add unsat cores support to CVC native language.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-03More array constants and parsing: better error messages, extend to CVC presen...Morgan Deters
2014-10-03Minor fixes to CVC printer.Morgan Deters
2014-07-10membership cvc token changed to `IS_IN' to avoid conflict with IN used for letKshitij Bansal
2014-07-09sets cvc printerKshitij Bansal
2014-07-01Update copyrights.Morgan Deters
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-04Add operator support (resolves bug #563).Morgan Deters
2014-04-10Expand definitions in theory datatypes, now has the expected semantics for in...Andrew Reynolds
2014-03-05Improving support for POW in arithmetic. Resolves bug 549.Tim King
2013-12-24Merge branch '1.3.x'Morgan Deters
2013-12-24Better automatic handling of output language setting.Morgan Deters
2013-12-23Proof-checking code; fixups of segfaults and missing functionality in proof g...Morgan Deters
2013-12-05Update copyrights, add missing file-level documentation; fix perms.Morgan Deters
2013-11-27General pre-release cleanup commitMorgan Deters
2013-11-19Add fair strategy for finite model finding multiple sorts --uf-ss-fair.Andrew Reynolds
2013-11-10Flatten libcvc4 build structure; remove some #include interdependencesMorgan Deters
2013-07-06Model output is now const; this related to bug 519Morgan Deters
2013-04-02Regenerated copyrights: canonicalized names, no emailsMorgan Deters
2013-04-01update copyrightsMorgan Deters
2013-03-26Fixes for warnings from clang++, from -std=gnu++0x, from swig, and from javacMorgan Deters
2013-03-22Support for Boolean term conversion in datatypes.Morgan Deters
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback