Hi Valerie,

please direct such questions to [sage-support] which I CCed.

On Tuesday 31 Dec 2013 10:51:06 you wrote:
> Hi Dr Martin,
> 
> 
> I downloaded the CryptoMiniSat package from
> http://www.sagemath.org/packages/optional/ and
> 
> would like to save the clauses derived from a polynomial system in a file. I
> did the following:
> 
> sage: from sage.sat.converters.polybori import CNFEncoder
> sage: from sage.sat.solvers import CryptoMiniSat
> sage: cms = CryptoMiniSat

This should read CryptoMiniSat()

> sage: fn = tmp_filename()
> sage: phi = CNFEncoder(cms,R)
> sage:phi(F) # F is a system of Booleanpolynomials
> 
> sage:cms.clauses(fn)
> 
> But I received the error message
> 
> AttributeError: 'sage.sat.solvers.cryptominisat.cryptominisat.Crypt' object
> has no attribute 'clauses'
> 
> But from http://sagenb.org/src/sat/solvers/cryptominisat/cryptominisat.pyx,
> the 'clauses' function is contained in the CryptoMiniSat module.
> 
> 
> May I know whether there was something wrong with my commands or that the
> CryptoMiniSat module does not have the attribute 'clauses'? If so, how may
> I go about doing it? 
> 
> Also, is there a possibility for multi-threading for CryptoMiniSat in Sage?
> 
> 
> Valerie

Cheers,
Martin

--
name: Martin Albrecht
_pgp: http://pgp.mit.edu:11371/pks/lookup?op=get&search=0x6532AFB4
_otr: 47F43D1A 5D68C36F 468BAEBA 640E8856 D7951CCF
_www: http://martinralbrecht.wordpress.com/
_jab: [email protected]

Attachment: signature.asc
Description: This is a digitally signed message part.

Reply via email to