polybori.cnf
index
../../../../lib/python2.7/site-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(Variable(0)*Variable(1)*Variable(2))
[{y: 0, z: 0, x: 0}]
>>> e.clauses(Variable(1)+Variable(0))
[{y: 0, x: 1}, {y: 1, x: 0}]
dimacs_cnf(self, polynomial_system)
>>> from polybori import *
>>> r = declare_ring(["x", "y", "z"], dict())
>>> e = CNFEncoder(r)
>>> e.dimacs_cnf([Variable(0)*Variable(1)*Variable(2)])
'c cnf generated by PolyBoRi\np cnf 3 1\n-2 -3 -1 0'
>>> e.dimacs_cnf([Variable(1)+Variable(0)])
'c cnf generated by PolyBoRi\np cnf 3 2\n-2 1 0\n2 -1 0'
>>> e.dimacs_cnf([Variable(0)*Variable(1)*Variable(2), Variable(1)+Variable(0)])
'c cnf generated by PolyBoRi\np cnf 3 3\n-2 -3 -1 0\n2 -1 0\n-2 1 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"])
['2 -3 1 0', '-2 3 1 0', '-2 -3 -1 0', '2 3 -1 0']
polynomial_clauses(self, f)
>>> from polybori import *
>>> r = declare_ring(["x", "y", "z"], dict())
>>> e = CNFEncoder(r)
>>> e.polynomial_clauses(Variable(0)*Variable(1)*Variable(2))
[x*y*z]
>>> v = 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(Variable(0)*Variable(1)*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([Variable(0)*Variable(1)*Variable(2)])
'c cnf generated by PolyBoRi\np cnf 3 1\n-2 -3 -1 0\nc g 1 x*y*z\nc v 1 x\nc v 2 y\nc v 3 z'
>>> e.dimacs_cnf([Variable(1)+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([Variable(0)*Variable(1)*Variable(2), Variable(1)+Variable(0)])
'c cnf generated by PolyBoRi\np cnf 3 2\n-2 -3 -1 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(Variable(0)*Variable(1)*Variable(2))
[{y: 0, z: 0, x: 0}]
>>> e.clauses(Variable(1)+Variable(0))
[{y: 0, x: 1}, {y: 1, x: 0}]
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(Variable(0)*Variable(1)*Variable(2))
[x*y*z]
>>> v = 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(Variable(0)*Variable(1)*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
       
change_ordering(...)
change_ordering( (int)arg1) -> None :
 
    C++ signature :
        void change_ordering(int)
global_ring(...)
global_ring() -> Ring :
 
    C++ signature :
        polybori::BoolePolyRing {lvalue} global_ring()
ite = if_then_else(...)
if_then_else( (int)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