polybori.cnf | index ../../../../lib/python2.7/dist-packages/polybori/cnf.py

Classes

``

__builtin__.object
  CNFEncoder
    CryptoMiniSatEncoder

class CNFEncoder(__builtin__.object)

``

Methods defined here:

__init__(self, r, random_seed=16)

clauses(self, f)
  `>>> from polybori import *
  >>> r = declare_ring(["x", "y", "z"], dict())
  >>> e = CNFEncoder(r)
  >>> e.clauses(r.variable(0)*r.variable(1)*r.variable(2)) # doctest:+ELLIPSIS
  [{...x: 0...}]
  >>> e.clauses(r.variable(1)+r.variable(0)) # doctest:+ELLIPSIS
  [{...x: 1...}, {...y: 1...}]
  >>> [sorted(c.iteritems()) for c in e.clauses(r.variable(0)*r.variable(1)*r.variable(2))]
  [[(z, 0), (y, 0), (x, 0)]]
  >>> [sorted(c.iteritems()) for c in e.clauses(r.variable(1)+r.variable(0))]
  [[(y, 1), (x, 0)], [(y, 0), (x, 1)]]`

dimacs_cnf(self, polynomial_system)
  `>>> from polybori import *
  >>> r = declare_ring(["x", "y", "z"], dict())
  >>> e = CNFEncoder(r)
  >>> e.dimacs_cnf([r.variable(0)*r.variable(1)*r.variable(2)])
  'c cnf generated by PolyBoRi\np cnf 3 1\n-1 -2 -3 0'
  >>> e.dimacs_cnf([r.variable(1)+r.variable(0)])
  'c cnf generated by PolyBoRi\np cnf 3 2\n1 -2 0\n-1 2 0'
  >>> e.dimacs_cnf([r.variable(0)*r.variable(1)*r.variable(2), r.variable(1)+r.variable(0)])
  'c cnf generated by PolyBoRi\np cnf 3 3\n-1 -2 -3 0\n-1 2 0\n1 -2 0'`

dimacs_encode_clause(self, c)

dimacs_encode_polynomial(self, p)
  `>>> from polybori import *
  >>> d=dict()
  >>> r = declare_ring(["x", "y", "z"], d)
  >>> e = CNFEncoder(r)
  >>> e.dimacs_encode_polynomial(d["x"]+d["y"]+d["z"])
  ['1 2 -3 0', '1 -2 3 0', '-1 -2 -3 0', '-1 2 3 0']`

polynomial_clauses(self, f)
  `>>> from polybori import *
  >>> r = declare_ring(["x", "y", "z"], dict())
  >>> e = CNFEncoder(r)
  >>> e.polynomial_clauses(r.variable(0)*r.variable(1)*r.variable(2))
  [x*y*z]
  >>> v = r.variable
  >>> p = v(1)*v(2)+v(2)*v(0)+1
  >>> groebner_basis([p], heuristic = False)==groebner_basis(e.polynomial_clauses(p), heuristic = False)
  True`

to_dimacs_index(self, v)

zero_blocks(self, f)
  `divides the zero set of f into blocks
  >>> from polybori import *
  >>> r = declare_ring(["x", "y", "z"], dict())
  >>> e = CNFEncoder(r)
  >>> e.zero_blocks(r.variable(0)*r.variable(1)*r.variable(2))
  [{y: 0}, {z: 0}, {x: 0}]`

Data descriptors defined here:

__dict__
  `dictionary for instance variables (if defined)`

__weakref__
  `list of weak references to the object (if defined)`

class CryptoMiniSatEncoder(CNFEncoder)

``

Method resolution order:
  CryptoMiniSatEncoder
  CNFEncoder
  __builtin__.object

Methods defined here:

dimacs_cnf(self, polynomial_system)
  `>>> from polybori import *
  >>> r = declare_ring(["x", "y", "z"], dict())
  >>> e = CryptoMiniSatEncoder(r)
  >>> e.dimacs_cnf([r.variable(0)*r.variable(1)*r.variable(2)])
  'c cnf generated by PolyBoRi\np cnf 3 1\n-1 -2 -3 0\nc g 1 x*y*z\nc v 1 x\nc v 2 y\nc v 3 z'
  >>> e.dimacs_cnf([r.variable(1)+r.variable(0)])
  'c cnf generated by PolyBoRi\np cnf 3 1\nx1 2 0\nc g 2 x + y\nc v 1 x\nc v 2 y'
  >>> e.dimacs_cnf([r.variable(0)*r.variable(1)*r.variable(2), r.variable(1)+r.variable(0)])
  'c cnf generated by PolyBoRi\np cnf 3 2\n-1 -2 -3 0\nc g 3 x*y*z\nx1 2 0\nc g 4 x + y\nc v 1 x\nc v 2 y\nc v 3 z'`

dimacs_encode_polynomial(self, p)
  `>>> from polybori import *
  >>> d=dict()
  >>> r = declare_ring(["x", "y", "z"], d)
  >>> e = CryptoMiniSatEncoder(r)
  >>> p = d["x"]+d["y"]+d["z"]
  >>> p.deg()
  1
  >>> len(p)
  3
  >>> e.dimacs_encode_polynomial(p)
  ['x1 2 3 0\nc g 1 x + y + z']
  >>> e.dimacs_encode_polynomial(p+1)
  ['x1 2 -3 0\nc g 2 x + y + z + 1']`

Data and other attributes defined here:

group_counter = 0

Methods inherited from CNFEncoder:

__init__(self, r, random_seed=16)

clauses(self, f)
  `>>> from polybori import *
  >>> r = declare_ring(["x", "y", "z"], dict())
  >>> e = CNFEncoder(r)
  >>> e.clauses(r.variable(0)*r.variable(1)*r.variable(2)) # doctest:+ELLIPSIS
  [{...x: 0...}]
  >>> e.clauses(r.variable(1)+r.variable(0)) # doctest:+ELLIPSIS
  [{...x: 1...}, {...y: 1...}]
  >>> [sorted(c.iteritems()) for c in e.clauses(r.variable(0)*r.variable(1)*r.variable(2))]
  [[(z, 0), (y, 0), (x, 0)]]
  >>> [sorted(c.iteritems()) for c in e.clauses(r.variable(1)+r.variable(0))]
  [[(y, 1), (x, 0)], [(y, 0), (x, 1)]]`

dimacs_encode_clause(self, c)

polynomial_clauses(self, f)
  `>>> from polybori import *
  >>> r = declare_ring(["x", "y", "z"], dict())
  >>> e = CNFEncoder(r)
  >>> e.polynomial_clauses(r.variable(0)*r.variable(1)*r.variable(2))
  [x*y*z]
  >>> v = r.variable
  >>> p = v(1)*v(2)+v(2)*v(0)+1
  >>> groebner_basis([p], heuristic = False)==groebner_basis(e.polynomial_clauses(p), heuristic = False)
  True`

to_dimacs_index(self, v)

zero_blocks(self, f)
  `divides the zero set of f into blocks
  >>> from polybori import *
  >>> r = declare_ring(["x", "y", "z"], dict())
  >>> e = CNFEncoder(r)
  >>> e.zero_blocks(r.variable(0)*r.variable(1)*r.variable(2))
  [{y: 0}, {z: 0}, {x: 0}]`

Data descriptors inherited from CNFEncoder:

__dict__
  `dictionary for instance variables (if defined)`

__weakref__
  `list of weak references to the object (if defined)`

Functions

``

ite = if_then_else(...)
  `if_then_else( (object)arg1, (BooleSet)arg2, (BooleSet)arg3) -> BooleSet :
  if-then else operator
  C++ signature :
  polybori::BooleSet if_then_else(int,polybori::BooleSet,polybori::BooleSet)
  if_then_else( (Variable)arg1, (BooleSet)arg2, (BooleSet)arg3) -> BooleSet :
  if-then else operator
  C++ signature :
  polybori::BooleSet if_then_else(polybori::BooleVariable,polybori::BooleSet,polybori::BooleSet)`

ll_red_nf_redsb(...)
  `ll_red_nf_redsb( (Polynomial)arg1, (BooleSet)arg2) -> Polynomial :
  C++ signature :
  polybori::BoolePolynomial ll_red_nf_redsb(polybori::BoolePolynomial,polybori::BooleSet)`

Data
`` |  | lp = polybori.dynamic.PyPolyBoRi.OrderCode.lp