summaryrefslogtreecommitdiff
path: root/src/printer/cvc
AgeCommit message (Expand)Author
2016-02-15Eliminate most of the internal representation infrastructure for tuples and r...ajreynol
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
2013-03-21Some model and printing fixes for defined functions in input.Morgan Deters
2013-02-24added option --model-u-dt-enum for outputting uninterpreted sorts as datatype...Andrew Reynolds
2012-12-18Fix printing of EXISTS in CVC language printerMorgan Deters
2012-12-12* fixed bug 481 by adding check for division by 0 in bit-vector division circuitlianah
2012-12-01another part of last commitMorgan Deters
2012-11-30internal variables (skolems) aren't printed as part of the modelMorgan Deters
2012-11-30Partial fix for bug 435; still needs some effort.Morgan Deters
2012-11-27First chunk of boolean-terms support.Morgan Deters
2012-11-27Tuples and records merge. Resolves bug 270.Morgan Deters
2012-11-17* Fix for bug 445 agreed to in meeting 11/13/2012: always dump in ALL_SUPPORT...Morgan Deters
2012-11-16Fix dumping of array-select expressions in CVC native language.Morgan Deters
2012-11-14Fix for bug 407. mkAnonymousFunction() in the parser no longer uses ':'. CVC ...Tim King
2012-10-11Standardizing copyright notice. Touches **ALL** sources, guys, sorry.. it'sMorgan Deters
2012-10-05Bug-related:Morgan Deters
2012-10-05BoolExpr removed and replaced with ExprDejan Jovanović
2012-09-26Finish off SEXPR kind work.Morgan Deters
2012-09-24some api changesDejan Jovanović
2012-09-21Fixes for datatype dumping and printing. Add a new test case for dumping.Morgan Deters
2012-09-21SMT-LIBv2 compliance updates:Morgan Deters
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback