summaryrefslogtreecommitdiff
path: root/src/printer/smt2
AgeCommit message (Expand)Author
2014-01-28merge internal and user of charat & substr into oneTianyi Liang
2014-01-18strings with new ideasTianyi Liang
2014-01-17Merge branch '1.3.x'Morgan Deters
2014-01-17Fix for quote-escaping in smt2 printerMorgan Deters
2014-01-16adds partial functionsTianyi Liang
2014-01-15adds smt2 print for stringsTianyi Liang
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-12-05Fixes related to parametric datatype printing.Morgan Deters
2013-11-27General pre-release cleanup commitMorgan Deters
2013-11-10Flatten libcvc4 build structure; remove some #include interdependencesMorgan Deters
2013-09-18Support for bv2nat/int2bv in parser and BV rewriter.Morgan Deters
2013-09-05Fix declare-fun/define-fun in dumps; resolves bugs 408 and 385; also fix a se...Morgan Deters
2013-07-11Support for TPTP's TFF0 (with arithmetic)Morgan Deters
2013-07-06Model output is now const; this related to bug 519Morgan Deters
2013-06-27Minor printer cleanup for SMT-LIBv2 symbols "div" and "mod".Morgan Deters
2013-06-24Support for abs, to_int, is_int, divisible in SMT-LIB; also --rewrite-divk al...Morgan Deters
2013-06-09another fix for array-store-all printingMorgan Deters
2013-06-09Better array-store-all output for SMT-LIB.Morgan Deters
2013-05-29Merge branch '1.2.x'Morgan Deters
2013-05-29SMT-LIB printer updates (some missing cases).Morgan Deters
2013-05-14Add support for quantifier patterns in smt2 printer.Andrew Reynolds
2013-05-01Fix to dumping re: boolean terms, datatypesMorgan 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-21Some model and printing fixes for defined functions in input.Morgan Deters
2013-03-20Properly |quote| symbols in SMT-LIBv2 output.Morgan Deters
2013-02-24added option --model-u-dt-enum for outputting uninterpreted sorts as datatype...Andrew Reynolds
2013-01-08SMT-LIB get-model output now is easier to machine-parse: contains (model...) ...Morgan 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-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-12minor bug fixes for quantifiers, added sort inference module (not ready to be...Andrew Reynolds
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-21SMT-LIBv2 compliance updates:Morgan Deters
2012-09-20some bugfixes that come as a result of debugging some CASCADE/C stuff..Morgan Deters
2012-09-19General subscriber infrastructure for NodeManager, as discussed in theMorgan Deters
2012-09-18SMT-LIBv2 compliance regarding outputting "unknown".Morgan Deters
2012-09-12Adding model assertions after SAT responses.Morgan Deters
2012-09-11Partially reverting the changes made in 4308. There is now both an Expr and N...Tim King
2012-09-10modified getValue to return Expr instead of NodeAndrew Reynolds
2012-08-31merge from fmf-devel branch. more updates to models: now with collectModelIn...Andrew Reynolds
2012-08-24fix get-value output in a couple ways; this fixes bug #378Morgan Deters
2012-08-09minor isConst()-related fixes to printing; also add some debugging stuff to s...Morgan Deters
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback