summaryrefslogtreecommitdiff
path: root/src/util
AgeCommit message (Expand)Author
2012-08-22Cap finite cardinalities at 2^64, as discussed in the meeting last week.Morgan Deters
2012-08-20fixes for java bindingsMorgan Deters
2012-08-16ArrayStoreAll should (for now) only allow constant expressions, as it is itse...Morgan Deters
2012-08-16fix exceptions and mkConst() in java bindingMorgan Deters
2012-08-14Fixes to integer wrapper classes:Morgan Deters
2012-08-07small fixesDejan Jovanović
2012-08-07Some items from the CVC4 public interface review:Morgan Deters
2012-08-03ArrayStoreAll infrastructureMorgan Deters
2012-08-03fix uses of getMetaKind() from outside the expr package. (they now use isCon...Morgan Deters
2012-08-02array-store-all classMorgan Deters
2012-08-01fixes to some *clean targetsMorgan Deters
2012-08-01some fixes for Mac OSMorgan Deters
2012-07-31Options merge. This commit:Morgan Deters
2012-07-27Minor cleanup after today's commits:Morgan Deters
2012-07-27removing unecessary filesAndrew Reynolds
2012-07-27Merge quantifiers2-trunk:François Bobot
2012-07-18removing output operator for SExprTypes, which is never used (and SExprTypes ...Morgan Deters
2012-07-17SMT-LIBv2 compliance updates:Morgan Deters
2012-07-16Support for having two SmtEngines with the same ExprManager.Morgan Deters
2012-07-14Type enumerator infrastructure and uninterpreted constant support. No suppor...Morgan Deters
2012-07-12merged fmf-devel branch, includes support for SMT2 command get-value and (ext...Andrew Reynolds
2012-07-10small changes:Dejan Jovanović
2012-07-08Bugs resolved by this commit: #314, #322, #359, #364, #365.Morgan Deters
2012-07-07Various fixes to documentation---typos, some incomplete documentation fixed, ...Morgan Deters
2012-06-22TPTP: add parser for cnf and fofFrançois Bobot
2012-06-17--decision=justification-stoponly : use decision engine only for stoppingKshitij Bansal
2012-06-16changing theoryOf in shared mode with arrays to move equalities to arraysDejan Jovanović
2012-06-14fix cout, fix statname, rm deadcodeKshitij Bansal
2012-06-14Brings the tuning branch into trunk. This includes the changes from restricte...Tim King
2012-06-12fix ordering issue of --dump-to and --default-dag-thresh. now can be specifi...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-08The option --arith-presolve-lemmas had previously been renamed --unate-lemmas.Morgan Deters
2012-06-08Extend Printer infrastructure also to the "Result" class, meaning that differ...Morgan Deters
2012-06-08minor fixes, for Mac OSMorgan Deters
2012-06-08threadlocalKshitij Bansal
2012-06-08Merge from decision branch (till r3663)Kshitij Bansal
2012-06-06Changes to the combination mechanism, lots of details. Not done yet, there ar...Dejan Jovanović
2012-06-04Added preprocessing pass that propagates unconstrained values - solves all ofClark Barrett
2012-05-30Added BitwiseEq bitvector rewriteClark Barrett
2012-05-22This commit merges in the branch arithmetic/cprop.Tim King
2012-05-18This commit adds TypeNode::leastCommonTypeNode(). The special case for arith...Tim King
2012-05-18This commit removes the dead psuedoboolean code.Tim King
2012-05-17Fixed bug 338:Liana Hadarean
2012-05-14in debug builds, -d can be used for trace tags that aren't also debug tagsMorgan Deters
2012-05-13fixing build warningsDejan Jovanović
2012-05-11fix regex in Debug_tags and Trace_tags generation for Mac OSMorgan Deters
2012-05-11fix typo in sed lineMorgan Deters
2012-05-11Disabled arith-rewrite-equalities by default unless in a pure arithmetic theoryClark Barrett
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback