Age | Commit message (Expand) | Author |
2012-07-27 | removing unecessary files | Andrew Reynolds |
2012-07-27 | Merge quantifiers2-trunk: | François Bobot |
2012-07-18 | removing output operator for SExprTypes, which is never used (and SExprTypes ... | Morgan Deters |
2012-07-17 | SMT-LIBv2 compliance updates: | Morgan Deters |
2012-07-16 | Support for having two SmtEngines with the same ExprManager. | Morgan Deters |
2012-07-14 | Type enumerator infrastructure and uninterpreted constant support. No suppor... | Morgan Deters |
2012-07-12 | merged fmf-devel branch, includes support for SMT2 command get-value and (ext... | Andrew Reynolds |
2012-07-10 | small changes: | Dejan Jovanović |
2012-07-08 | Bugs resolved by this commit: #314, #322, #359, #364, #365. | Morgan Deters |
2012-07-07 | Various fixes to documentation---typos, some incomplete documentation fixed, ... | Morgan Deters |
2012-06-22 | TPTP: add parser for cnf and fof | François Bobot |
2012-06-17 | --decision=justification-stoponly : use decision engine only for stopping | Kshitij Bansal |
2012-06-16 | changing theoryOf in shared mode with arrays to move equalities to arrays | Dejan Jovanović |
2012-06-14 | fix cout, fix statname, rm deadcode | Kshitij Bansal |
2012-06-14 | Brings the tuning branch into trunk. This includes the changes from restricte... | Tim King |
2012-06-12 | fix ordering issue of --dump-to and --default-dag-thresh. now can be specifi... | Morgan Deters |
2012-06-11 | Merge from quantifiers2-trunkmerge branch. | Morgan Deters |
2012-06-09 | Cleanup and comments for the dag-ifier. Also some unit testing for it. | Morgan Deters |
2012-06-09 | Dagification of output expressions. | Morgan Deters |
2012-06-08 | The option --arith-presolve-lemmas had previously been renamed --unate-lemmas. | Morgan Deters |
2012-06-08 | Extend Printer infrastructure also to the "Result" class, meaning that differ... | Morgan Deters |
2012-06-08 | minor fixes, for Mac OS | Morgan Deters |
2012-06-08 | threadlocal | Kshitij Bansal |
2012-06-08 | Merge from decision branch (till r3663) | Kshitij Bansal |
2012-06-06 | Changes to the combination mechanism, lots of details. Not done yet, there ar... | Dejan Jovanović |
2012-06-04 | Added preprocessing pass that propagates unconstrained values - solves all of | Clark Barrett |
2012-05-30 | Added BitwiseEq bitvector rewrite | Clark Barrett |
2012-05-22 | This commit merges in the branch arithmetic/cprop. | Tim King |
2012-05-18 | This commit adds TypeNode::leastCommonTypeNode(). The special case for arith... | Tim King |
2012-05-18 | This commit removes the dead psuedoboolean code. | Tim King |
2012-05-17 | Fixed bug 338: | Liana Hadarean |
2012-05-14 | in debug builds, -d can be used for trace tags that aren't also debug tags | Morgan Deters |
2012-05-13 | fixing build warnings | Dejan Jovanović |
2012-05-11 | fix regex in Debug_tags and Trace_tags generation for Mac OS | Morgan Deters |
2012-05-11 | fix typo in sed line | Morgan Deters |
2012-05-11 | Disabled arith-rewrite-equalities by default unless in a pure arithmetic theory | Clark Barrett |
2012-05-11 | Added some ITE rewrites, | Clark Barrett |
2012-05-09 | fix an issue which breaks language bindings (so this commit fixes debian nigh... | Morgan Deters |
2012-05-09 | --disable-tracing at configure time now disables Trace() and Debug() gestures... | Morgan Deters |
2012-05-09 | * simplifying equality engine interface | Dejan Jovanović |
2012-05-09 | Merge from decision branch (ITE support) | Kshitij Bansal |
2012-05-09 | Fixing the debug tags generation and related methods in configuration.cpp tha... | Dejan Jovanović |
2012-05-08 | Merging in bvprop branch, with proper bit-vector propagation. | Liana Hadarean |
2012-05-04 | options: fail if the debug or trace tag specified doesn't exist (-d -t) | François Bobot |
2012-05-04 | fix: getNumTraceTags, getNumDebugTags | François Bobot |
2012-04-30 | Added map from skolem variables to new ite formulas in ite removal. | Clark Barrett |
2012-04-27 | This merges in the branch cvc4/branches/arithmetic/matrix into trunk. | Tim King |
2012-04-23 | Merge from decision branch -- partially working justification heuristic | Kshitij Bansal |
2012-04-17 | A dummy decision engine. Expected performance impact: none. | Kshitij Bansal |
2012-04-17 | Merges branches/arithmetic/atom-database r2979 through 3247 into trunk. Belo... | Tim King |