| 2012-07-08 |
Morgan Deters | Bugs resolved by this commit: #314, #322, #359, #364... |
tree | commitdiff |
| 2012-07-07 |
Morgan Deters | Various fixes to documentation---typos, some incomplete... |
tree | commitdiff |
| 2012-06-22 |
François Bobot | TPTP: add parser for cnf and fof |
tree | commitdiff |
| 2012-06-17 |
Kshitij Bansal | --decision=justification-stoponly : use decision engine... |
tree | commitdiff |
| 2012-06-16 |
Dejan Jovanović | changing theoryOf in shared mode with arrays to move... |
tree | commitdiff |
| 2012-06-14 |
Kshitij Bansal | fix cout, fix statname, rm deadcode |
tree | commitdiff |
| 2012-06-14 |
Tim King | Brings the tuning branch into trunk. This includes... |
tree | commitdiff |
| 2012-06-12 |
Morgan Deters | fix ordering issue of --dump-to and --default-dag-thres... |
tree | commitdiff |
| 2012-06-11 |
Morgan Deters | Merge from quantifiers2-trunkmerge branch. |
tree | commitdiff |
| 2012-06-09 |
Morgan Deters | Cleanup and comments for the dag-ifier. Also some... |
tree | commitdiff |
| 2012-06-09 |
Morgan Deters | Dagification of output expressions. |
tree | commitdiff |
| 2012-06-08 |
Morgan Deters | The option --arith-presolve-lemmas had previously been... |
tree | commitdiff |
| 2012-06-08 |
Morgan Deters | Extend Printer infrastructure also to the "Result"... |
tree | commitdiff |
| 2012-06-08 |
Morgan Deters | minor fixes, for Mac OS |
tree | commitdiff |
| 2012-06-08 |
Kshitij Bansal | threadlocal |
tree | commitdiff |
| 2012-06-08 |
Kshitij Bansal | Merge from decision branch (till r3663) |
tree | commitdiff |
| 2012-06-06 |
Dejan Jovanović | Changes to the combination mechanism, lots of details... |
tree | commitdiff |
| 2012-06-04 |
Clark Barrett | Added preprocessing pass that propagates unconstrained... |
tree | commitdiff |
| 2012-05-30 |
Clark Barrett | Added BitwiseEq bitvector rewrite |
tree | commitdiff |
| 2012-05-22 |
Tim King | This commit merges in the branch arithmetic/cprop. |
tree | commitdiff |
| 2012-05-18 |
Tim King | This commit adds TypeNode::leastCommonTypeNode(). ... |
tree | commitdiff |
| 2012-05-18 |
Tim King | This commit removes the dead psuedoboolean code. |
tree | commitdiff |
| 2012-05-17 |
Liana Hadarean | Fixed bug 338: |
tree | commitdiff |
| 2012-05-14 |
Morgan Deters | in debug builds, -d can be used for trace tags that... |
tree | commitdiff |
| 2012-05-13 |
Dejan Jovanović | fixing build warnings |
tree | commitdiff |
| 2012-05-11 |
Morgan Deters | fix regex in Debug_tags and Trace_tags generation for... |
tree | commitdiff |
| 2012-05-11 |
Morgan Deters | fix typo in sed line |
tree | commitdiff |
| 2012-05-11 |
Clark Barrett | Disabled arith-rewrite-equalities by default unless... |
tree | commitdiff |
| 2012-05-11 |
Clark Barrett | Added some ITE rewrites, |
tree | commitdiff |
| 2012-05-09 |
Morgan Deters | fix an issue which breaks language bindings (so this... |
tree | commitdiff |
| 2012-05-09 |
Morgan Deters | --disable-tracing at configure time now disables Trace... |
tree | commitdiff |
| 2012-05-09 |
Dejan Jovanović | * simplifying equality engine interface |
tree | commitdiff |
| 2012-05-09 |
Kshitij Bansal | Merge from decision branch (ITE support) |
tree | commitdiff |
| 2012-05-09 |
Dejan Jovanović | Fixing the debug tags generation and related methods... |
tree | commitdiff |
| 2012-05-08 |
Liana Hadarean | Merging in bvprop branch, with proper bit-vector propag... |
tree | commitdiff |
| 2012-05-04 |
François Bobot | options: fail if the debug or trace tag specified doesn... |
tree | commitdiff |
| 2012-05-04 |
François Bobot | fix: getNumTraceTags, getNumDebugTags |
tree | commitdiff |
| 2012-04-30 |
Clark Barrett | Added map from skolem variables to new ite formulas... |
tree | commitdiff |
| 2012-04-27 |
Tim King | This merges in the branch cvc4/branches/arithmetic... |
tree | commitdiff |
| 2012-04-23 |
Kshitij Bansal | Merge from decision branch -- partially working justifi... |
tree | commitdiff |
| 2012-04-17 |
Kshitij Bansal | A dummy decision engine. Expected performance impact... |
tree | commitdiff |
| 2012-04-17 |
Tim King | Merges branches/arithmetic/atom-database r2979 through... |
tree | commitdiff |
| 2012-04-13 |
Morgan Deters | Fix SExpr name qualification for swig, and #include... |
tree | commitdiff |
| 2012-04-12 |
Tim King | Adds an operator<< to SExpr::SexprTypes. This fixes... |
tree | commitdiff |
| 2012-04-11 |
Morgan Deters | merge from arrays-clark branch |
tree | commitdiff |
| 2012-04-06 |
Morgan Deters | * Fix ITEs and functions in CVC language printer. |
tree | commitdiff |
| 2012-04-04 |
Liana Hadarean | * added propagation as lemmas to TheoryBV: |
tree | commitdiff |
| 2012-04-02 |
Tim King | - Merged in the branch cdlist-cleanup. |
tree | commitdiff |
| 2012-03-28 |
Morgan Deters | fix swig-ignored interface name; hopefully fixes Debian... |
tree | commitdiff |
| 2012-03-26 |
Dejan Jovanović | Global registry of SAT solvers, where they are register... |
tree | commitdiff |
| 2012-03-23 |
Tim King | Removed the variableRemovalEnabled option and d_removed... |
tree | commitdiff |
| 2012-03-22 |
Liana Hadarean | Merged updated version of the bitvector theory: |
tree | commitdiff |
| 2012-03-21 |
Morgan Deters | Disable nonclausal simplification for QF_SAT benchmarks... |
tree | commitdiff |
| 2012-03-09 |
Morgan Deters | Some work on the dump infrastructure to support portfol... |
tree | commitdiff |
| 2012-03-07 |
Morgan Deters | fix some Java compatibility-layer interface problems... |
tree | commitdiff |
| 2012-03-02 |
Dejan Jovanović | CDMap -> CDHashMap |
tree | commitdiff |
| 2012-03-01 |
Morgan Deters | Partial merge from kind-backend branch, including Minis... |
tree | commitdiff |
| 2012-02-28 |
Tim King | This commit merges in branches/arithmetic/internalbb... |
tree | commitdiff |
| 2012-02-25 |
Liana Hadarean | Refactored CnfStream to work with the bv theory Bitblaster: |
tree | commitdiff |
| 2012-02-22 |
Morgan Deters | Fixes to documentation / fixes for MacOS |
tree | commitdiff |
| 2012-02-21 |
Morgan Deters | fix src/util/hash.h to specialize GNU's hash template... |
tree | commitdiff |
| 2012-02-21 |
Morgan Deters | don't require libboost_thread (its presence is detected... |
tree | commitdiff |
| 2012-02-20 |
Morgan Deters | fix "make dist" |
tree | commitdiff |
| 2012-02-20 |
Morgan Deters | portfolio merge |
tree | commitdiff |
| 2012-02-20 |
Morgan Deters | By default, ONLY enable symmetry breaker ONLY for QF_UF... |
tree | commitdiff |
| 2012-02-16 |
Tim King | Last commit accidentally lacked r2778 and r2779 from... |
tree | commitdiff |
| 2012-02-15 |
Tim King | This commit merges into trunk the branch branches/arith... |
tree | commitdiff |
| 2012-02-12 |
Morgan Deters | copyright year updated to 2012 |
tree | commitdiff |
| 2011-12-14 |
Andrew Reynolds | added minor documentation for parametric datatypes... |
tree | commitdiff |
| 2011-11-22 |
Morgan Deters | More language bindings work: |
tree | commitdiff |
| 2011-11-16 |
Morgan Deters | Addressed many of the concerns raised in the public... |
tree | commitdiff |
| 2011-11-15 |
Morgan Deters | Bindings work (ocaml bindings are now sort of working... |
tree | commitdiff |
| 2011-11-15 |
Morgan Deters | additional minor changes to get python binding on bette... |
tree | commitdiff |
| 2011-11-15 |
Morgan Deters | fixes for python language binding, added python example |
tree | commitdiff |
| 2011-11-06 |
Morgan Deters | datatype stuff in compatibility interface implemented |
tree | commitdiff |
| 2011-11-04 |
Morgan Deters | STRING_TYPE and CONST_STRING and associate type infrast... |
tree | commitdiff |
| 2011-11-02 |
Morgan Deters | Only print a shortlist of most-commonly-used options... |
tree | commitdiff |
| 2011-11-02 |
Morgan Deters | give an option error if the user specifies --proof... |
tree | commitdiff |
| 2011-11-02 |
Morgan Deters | better Integer asserts when there's overflow on convers... |
tree | commitdiff |
| 2011-10-31 |
Morgan Deters | fixes to assertions in GMP to match CLN behavior |
tree | commitdiff |
| 2011-10-31 |
Tim King | Added assertions to the CLN implementation of Integer... |
tree | commitdiff |
| 2011-10-29 |
Morgan Deters | Support for SMT-LIBv2 (get-proof), CVC-style DUMP_PROOF... |
tree | commitdiff |
| 2011-10-28 |
Morgan Deters | * ability to output NodeBuilders without first converti... |
tree | commitdiff |
| 2011-10-28 |
Liana Hadarean | merged the proofgen3 branch into trunk: |
tree | commitdiff |
| 2011-10-25 |
Kshitij Bansal | Initialize resource limit and millisecond limit options |
tree | commitdiff |
| 2011-10-23 |
Morgan Deters | Implement changes from yesterday morning's meeting... |
tree | commitdiff |
| 2011-10-21 |
Morgan Deters | add gcc version information to Configuration, and warn... |
tree | commitdiff |
| 2011-10-17 |
Dejan Jovanović | Sharing work |
tree | commitdiff |
| 2011-10-13 |
Morgan Deters | Interruption, time-out, and deterministic time-out... |
tree | commitdiff |
| 2011-10-07 |
Morgan Deters | Some new Datatype public functionality, as per Chris... |
tree | commitdiff |
| 2011-10-05 |
Morgan Deters | minor visibility fixes |
tree | commitdiff |
| 2011-10-05 |
Morgan Deters | remove some debugging code that slowed down last night... |
tree | commitdiff |
| 2011-10-04 |
Tim King | Disabling the variable removal hueristic by default. |
tree | commitdiff |
| 2011-10-04 |
Morgan Deters | cvc3 compatibility layer; and another libantlr3c v3... |
tree | commitdiff |
| 2011-10-03 |
Morgan Deters | user push/pop support in minisat and simplification... |
tree | commitdiff |
| 2011-09-30 |
Morgan Deters | interfaces fixes and cleanups...and examples of each... |
tree | commitdiff |
| 2011-09-29 |
Morgan Deters | compatibility work, documentation |
tree | commitdiff |
| 2011-09-29 |
Morgan Deters | build system fixes |
tree | commitdiff |
| 2011-09-29 |
Morgan Deters | some test fixes |
tree | commitdiff |
| 2011-09-28 |
Morgan Deters | variety of visibility fixes (should clean up some of... |
tree | commitdiff |
| next |
projects / cvc5.git / history