summaryrefslogtreecommitdiff
path: root/src/printer/smt2
AgeCommit message (Expand)Author
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
2012-08-03fix uses of getMetaKind() from outside the expr package. (they now use isCon...Morgan Deters
2012-07-27Merge quantifiers2-trunk:François Bobot
2012-07-17SMT-LIBv2 compliance updates:Morgan Deters
2012-07-14Applying Dejan's patch for bug #369, which resolves it by adding a new (let.....Morgan Deters
2012-07-12merged fmf-devel branch, includes support for SMT2 command get-value and (ext...Andrew Reynolds
2012-06-14some changes to make CVC4 work nicely with trace executor for application tra...Morgan Deters
2012-06-11Merge from quantifiers2-trunkmerge branch.Morgan Deters
2012-06-09Cleanup and comments for the dag-ifier. Also some unit testing for it.Morgan Deters
2012-06-09Dagification of output expressions.Morgan Deters
2012-06-07Adding EchoCommand and associated printer and parser rules:Morgan Deters
2012-05-17Fixed bug 338:Liana Hadarean
2012-05-15This commit removes the CONST_INTEGER kind from nodes. This code comes from t...Tim King
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback