| 2012-05-09 |
Kshitij Bansal | rm something for a future merge that sneaked in |
commit | commitdiff | tree |
| 2012-05-09 |
Kshitij Bansal | Merge from decision branch (ITE support) |
commit | commitdiff | tree |
| 2012-05-09 |
Dejan Jovanović | Fixing the debug tags generation and related methods... |
commit | commitdiff | tree |
| 2012-05-08 |
Liana Hadarean | Merging in bvprop branch, with proper bit-vector propag... |
commit | commitdiff | tree |
| 2012-05-07 |
Tim King | Fixing a bug with TheoryArith::ppAssert() and shared... |
commit | commitdiff | tree |
| 2012-05-07 |
Tim King | Fixes a sign bug in the DioSolver. |
commit | commitdiff | tree |
| 2012-05-04 |
Clark Barrett | Guard for expensive Debug trace |
commit | commitdiff | tree |
| 2012-05-04 |
François Bobot | options: fail if the debug or trace tag specified doesn... |
commit | commitdiff | tree |
| 2012-05-04 |
François Bobot | fix: getNumTraceTags, getNumDebugTags |
commit | commitdiff | tree |
| 2012-05-04 |
Tim King | - This fixes a problem where simplex produced the same... |
commit | commitdiff | tree |
| 2012-05-03 |
Dejan Jovanović | Some cleanup starting off from trying to understand... |
commit | commitdiff | tree |
| 2012-05-02 |
Clark Barrett | Changing d_sharedTermsExist to logicInfo.isSharingEnabled() |
commit | commitdiff | tree |
| 2012-04-30 |
Clark Barrett | Added map from skolem variables to new ite formulas... |
commit | commitdiff | tree |
| 2012-04-28 |
Morgan Deters | New LogicInfo functionality. |
commit | commitdiff | tree |
| 2012-04-28 |
Morgan Deters | require boost library (but not the threading support... |
commit | commitdiff | tree |
| 2012-04-28 |
Morgan Deters | undo, again |
commit | commitdiff | tree |
| 2012-04-28 |
Morgan Deters | adding THEORY_QUANTIFIERS and THEORY_REWRITERULES to... |
commit | commitdiff | tree |
| 2012-04-27 |
Morgan Deters | undo previous commit (as it will break a number of... |
commit | commitdiff | tree |
| 2012-04-27 |
Morgan Deters | adding THEORY_QUANTIFIERS and THEORY_REWRITERULES to... |
commit | commitdiff | tree |
| 2012-04-27 |
Morgan Deters | fix parser logic-handling oversights: QF_UFBV should... |
commit | commitdiff | tree |
| 2012-04-27 |
Morgan Deters | break dependence on zlib-dev for now |
commit | commitdiff | tree |
| 2012-04-27 |
Clark Barrett | Fixed warning in decision_engine.h, minor tweak to... |
commit | commitdiff | tree |
| 2012-04-27 |
Tim King | This merges in the branch cvc4/branches/arithmetic... |
commit | commitdiff | tree |
| 2012-04-25 |
Kshitij Bansal | portfolio driver: respect parseOnly option |
commit | commitdiff | tree |
| 2012-04-25 |
Kshitij Bansal | fix for de+lemmas |
commit | commitdiff | tree |
| 2012-04-24 |
Tim King | This commit merges in the branch branches/arithmetic... |
commit | commitdiff | tree |
| 2012-04-23 |
Kshitij Bansal | Merge from decision branch -- partially working justifi... |
commit | commitdiff | tree |
| 2012-04-20 |
Clark Barrett | Updates to array theory - much more lazy about introduc... |
commit | commitdiff | tree |
| 2012-04-19 |
Tim King | In the constructor of DecisionEngine, there were 2... |
commit | commitdiff | tree |
| 2012-04-18 |
Kshitij Bansal | add the missing BINARY variable in some test/regress... |
commit | commitdiff | tree |
| 2012-04-18 |
Kshitij Bansal | cout -> warning. Happening in portfolio |
commit | commitdiff | tree |
| 2012-04-18 |
Dejan Jovanović | disabling the problematic pragma in node_manager.h... |
commit | commitdiff | tree |
| 2012-04-17 |
Dejan Jovanović | Fix for thos annoying "array index" warnings in product... |
commit | commitdiff | tree |
| 2012-04-17 |
Kshitij Bansal | A dummy decision engine. Expected performance impact... |
commit | commitdiff | tree |
| 2012-04-17 |
Tim King | Merges branches/arithmetic/atom-database r2979 through... |
commit | commitdiff | tree |
| 2012-04-14 |
Clark Barrett | Fixed bug in sharing with arrays of different types |
commit | commitdiff | tree |
| 2012-04-13 |
Morgan Deters | Fix SExpr name qualification for swig, and #include... |
commit | commitdiff | tree |
| 2012-04-12 |
Morgan Deters | svn ignore Makefile.in for aufbv regression directory |
commit | commitdiff | tree |
| 2012-04-12 |
Tim King | Adds an operator<< to SExpr::SexprTypes. This fixes... |
commit | commitdiff | tree |
| 2012-04-11 |
Morgan Deters | merge from arrays-clark branch |
commit | commitdiff | tree |
| 2012-04-06 |
François Bobot | * Smt2 printer for datatypes |
commit | commitdiff | tree |
| 2012-04-06 |
Morgan Deters | * Fix ITEs and functions in CVC language printer. |
commit | commitdiff | tree |
| 2012-04-06 |
Morgan Deters | fix distributed builds (and therefore the Debian nightl... |
commit | commitdiff | tree |
| 2012-04-06 |
Dejan Jovanović | processing assertions in bit-vectors even when in fullc... |
commit | commitdiff | tree |
| 2012-04-05 |
Morgan Deters | Support to test the "dumper" mechanism in regressions... |
commit | commitdiff | tree |
| 2012-04-04 |
Dejan Jovanović | some settings in bvminisat |
commit | commitdiff | tree |
| 2012-04-04 |
Liana Hadarean | changed BVMinisat options to use cc_min=0 in propagate... |
commit | commitdiff | tree |
| 2012-04-04 |
Liana Hadarean | changed ccmin_mode in BvMinisat |
commit | commitdiff | tree |
| 2012-04-04 |
Liana Hadarean | * added propagation as lemmas to TheoryBV: |
commit | commitdiff | tree |
| 2012-04-03 |
Tim King | Fix for make dist. |
commit | commitdiff | tree |
| 2012-04-02 |
Tim King | Fix for broken unit tests from the previous commit. |
commit | commitdiff | tree |
| 2012-04-02 |
Tim King | - Merged in the branch cdlist-cleanup. |
commit | commitdiff | tree |
| 2012-04-02 |
Kshitij Bansal | fix for cvc4_logic dump |
commit | commitdiff | tree |
| 2012-04-02 |
Tim King | Removing large and unused regress2 benchmarks to decrea... |
commit | commitdiff | tree |
| 2012-03-30 |
Dejan Jovanović | some more build system fixes |
commit | commitdiff | tree |
| 2012-03-30 |
Dejan Jovanović | fixing some build systme warnings |
commit | commitdiff | tree |
| 2012-03-29 |
Tim King | Fix for bug 316. If the flag @CVC4_TLS_SUPPORTED@ is... |
commit | commitdiff | tree |
| 2012-03-29 |
Tim King | Fixes a linking problem with the new SatSolverConstruct... |
commit | commitdiff | tree |
| 2012-03-29 |
Dejan Jovanović | bringing cryptominisat into the main branch |
commit | commitdiff | tree |
| 2012-03-28 |
Dejan Jovanović | enabling the --disable-arithmetic-propagation option... |
commit | commitdiff | tree |
| 2012-03-28 |
Morgan Deters | fix swig-ignored interface name; hopefully fixes Debian... |
commit | commitdiff | tree |
| 2012-03-28 |
Tim King | Update to the ArithRewriter to remove REWRITE_AGAIN_FUL... |
commit | commitdiff | tree |
| 2012-03-28 |
Dejan Jovanović | Some renaming and refactoring in SAT |
commit | commitdiff | tree |
| 2012-03-28 |
Dejan Jovanović | getting rid of a rewrite in uf sharing, speeds things... |
commit | commitdiff | tree |
| 2012-03-28 |
Liana Hadarean | fixed faulty bv rewrite rule |
commit | commitdiff | tree |
| 2012-03-28 |
Dejan Jovanović | adding an extra cache check in the rewriter, speeds... |
commit | commitdiff | tree |
| 2012-03-26 |
Dejan Jovanović | Global registry of SAT solvers, where they are register... |
commit | commitdiff | tree |
| 2012-03-26 |
Dejan Jovanović | More cleaning up. |
commit | commitdiff | tree |
| 2012-03-26 |
Dejan Jovanović | more datail from the build failure |
commit | commitdiff | tree |
| 2012-03-26 |
Dejan Jovanović | with a small fix |
commit | commitdiff | tree |
| 2012-03-26 |
Dejan Jovanović | forgot to commit this one, fixing build errors |
commit | commitdiff | tree |
| 2012-03-25 |
Dejan Jovanović | moving minisat implementation into their respective... |
commit | commitdiff | tree |
| 2012-03-25 |
Dejan Jovanović | sat_module.h,cpp -> sat_solver.h,cpp (as intended) |
commit | commitdiff | tree |
| 2012-03-25 |
Dejan Jovanović | sat.h,cpp -> theory_proxy.h,cpp (this is what it defines) |
commit | commitdiff | tree |
| 2012-03-24 |
Dejan Jovanović | a cute script to make a video of development from the... |
commit | commitdiff | tree |
| 2012-03-23 |
Tim King | Removed the variableRemovalEnabled option and d_removed... |
commit | commitdiff | tree |
| 2012-03-22 |
Dejan Jovanović | * improving arithmetic getEqualityStatus |
commit | commitdiff | tree |
| 2012-03-22 |
Liana Hadarean | Merged updated version of the bitvector theory: |
commit | commitdiff | tree |
| 2012-03-22 |
Dejan Jovanović | some improvements to the sharing mechanism/interface |
commit | commitdiff | tree |
| 2012-03-21 |
Morgan Deters | Disable nonclausal simplification for QF_SAT benchmarks... |
commit | commitdiff | tree |
| 2012-03-09 |
Morgan Deters | Some work on the dump infrastructure to support portfol... |
commit | commitdiff | tree |
| 2012-03-09 |
Morgan Deters | fix a "lost command" bug and associated memory leak... |
commit | commitdiff | tree |
| 2012-03-09 |
Morgan Deters | Strengthen minisat assertion regarding t-propagations... |
commit | commitdiff | tree |
| 2012-03-09 |
Morgan Deters | minor fixes: to "make dist" in build directories with... |
commit | commitdiff | tree |
| 2012-03-08 |
Morgan Deters | fix "make dist" |
commit | commitdiff | tree |
| 2012-03-08 |
Dejan Jovanović | Fixin the bug Clark found. In final check, enqueued... |
commit | commitdiff | tree |
| 2012-03-08 |
Dejan Jovanović | Removing QUICK_CHECK, and other unused ones, from the... |
commit | commitdiff | tree |
| 2012-03-07 |
François Bobot | cdqueue : fix size(). Thank you Clark for spotting... |
commit | commitdiff | tree |
| 2012-03-07 |
Morgan Deters | fix some Java compatibility-layer interface problems... |
commit | commitdiff | tree |
| 2012-03-06 |
Dejan Jovanović | updating the equality engine to be able to give explana... |
commit | commitdiff | tree |
| 2012-03-03 |
Morgan Deters | Changing the dependency checking; GMP is required ... |
commit | commitdiff | tree |
| 2012-03-02 |
Kshitij Bansal | Remove some commented out code from sat.h |
commit | commitdiff | tree |
| 2012-03-02 |
Tim King | This commit merges in the changes from branches/arithme... |
commit | commitdiff | tree |
| 2012-03-02 |
Dejan Jovanović | CDMap -> CDHashMap |
commit | commitdiff | tree |
| 2012-03-02 |
Morgan Deters | committing the TNode/Node fix that was in the kind... |
commit | commitdiff | tree |
| 2012-03-02 |
Tim King | Renamed CDQueue to CDTrailQueue and CDQueue2 to CDQueue... |
commit | commitdiff | tree |
| 2012-03-01 |
Morgan Deters | Partial merge from kind-backend branch, including Minis... |
commit | commitdiff | tree |
| 2012-03-01 |
François Bobot | cdqueue2 : cdlist that can be used like queue and can... |
commit | commitdiff | tree |
| 2012-03-01 |
Tim King | Fixed a copy paste error where a lower bound was looked... |
commit | commitdiff | tree |
| 2012-02-29 |
Liana Hadarean | This should fix the debian build fails: |
commit | commitdiff | tree |
| next |
projects / cvc5.git / shortlog