Opened 9 years ago

Closed 9 years ago

#14198 closed enhancement (fixed)

update cryptominisat to most recent upstream release

Reported by: malb Owned by: tbd
Priority: major Milestone: sage-5.8
Component: packages: optional Keywords: cryptominisat
Cc: ncohen Merged in: sage-5.8.beta3
Authors: Martin Albrecht Reviewers: Nathann Cohen
Report Upstream: N/A Work issues:
Branch: Commit:
Dependencies: Stopgaps:

Status badges

Description (last modified by malb)

CryptoMiniSat? 2.9.6 is out and brings minor changes. However, one of those changes allows to resolve #14180.

Install: http://sage.math.washington.edu/home/malb/spkgs/cryptominisat-2.9.6.spkg

Attachments (1)

trac_14198_solverconf_copy.patch (807 bytes) - added by malb 9 years ago.

Download all attachments as: .zip

Change History (9)

comment:1 Changed 9 years ago by malb

  • Description modified (diff)
  • Status changed from new to needs_review

comment:2 Changed 9 years ago by ncohen

  • Reviewers set to Nathann Cohen
  • Status changed from needs_review to positive_review

Everything looks fine, SPKG.txt has been updated, all local changes are committed, all tests pass on the two computers I have access to.

Well, ... :-)

Nathann

comment:3 Changed 9 years ago by ncohen

  • Status changed from positive_review to needs_work

Hmmmmmmmmmmmm O_o

Sorry, but I actually get a doctest error "from time to time". Often, actually, but not always. Here it is :

sage -t -long -optional "devel/sage-main/sage/sat/solvers/cryptominisat/solverconf.pyx"
**********************************************************************
File "/home/ncohen/.Sage/devel/sage-main/sage/sat/solvers/cryptominisat/solverconf.pyx", line 282:
    sage: t == s                                                # optional - cryptominisat
Expected:
    True
Got:
    False
**********************************************************************
1 items had failures:
   1 of  10 in __main__.example_10

Changed 9 years ago by malb

comment:4 Changed 9 years ago by malb

  • Status changed from needs_work to needs_review

Looks like a bug in CryptoMiniSat?'s copy constructor or how we use it. I worked around it.

comment:5 Changed 9 years ago by ncohen

  • Status changed from needs_review to positive_review

Now everything seems right !

Thaaaaaaaaaaaaaaaaaanks !

Nathann

comment:6 Changed 9 years ago by jdemeyer

  • Component changed from packages to optional packages

comment:7 Changed 9 years ago by schilly

spkg is on the server and soon on the mirrors - and double checked that the directory is correct :-)

Last edited 9 years ago by schilly (previous) (diff)

comment:8 Changed 9 years ago by jdemeyer

  • Merged in set to sage-5.8.beta3
  • Resolution set to fixed
  • Status changed from positive_review to closed
Note: See TracTickets for help on using tickets.