Home       Trees       Indices       Help   
Project Homepage
Package zeroinstall :: Package injector :: Module sat :: Class SATProblem
[frames] | no frames]

Class SATProblem

source code

object --+
         |
        SATProblem
Instance Methods
 
__init__(self)
x.__init__(...) initializes x; see help(type(x)) for signature		 source code
int
get_decision_level(self) source code
int
add_variable(self, obj) source code
bool
enqueue(self, lit, reason) source code
 
undo_one(self) source code
 
cancel(self) source code
 
cancel_until(self, level) source code
 
propagate(self) source code
 
impossible(self) source code
VarInfo
get_varinfo_for_lit(self, lit) source code
bool | None
lit_value(self, lit) source code
 
watch_lit(self, lit, cb) source code
[str]
name_lits(self, lst) source code
str
name_lit(self, lit) source code
zeroinstall.injector.sat.UnionClause | bool
add_clause(self, lits) source code
zeroinstall.injector.sat.AtMostOneClause
at_most_one(self, lits) source code
 
analyse(self, cause) source code
bool
run_solver(self, decide) source code

Inherited from object: __delattr__, __format__, __getattribute__, __hash__, __new__, __reduce__, __reduce_ex__, __repr__, __setattr__, __sizeof__, __str__, __subclasshook__

Properties

Inherited from object: __class__

Method Details

__init__(self)
(Constructor)

source code 

x.__init__(...) initializes x; see help(type(x)) for signature

Overrides: object.__init__
(inherited documentation)

enqueue(self, lit, reason)

source code 
Parameters:
  • lit (int)
Returns: bool

cancel_until(self, level)

source code 
Parameters:
  • level (int)

get_varinfo_for_lit(self, lit)

source code 
Parameters:
  • lit (int)
Returns: VarInfo

lit_value(self, lit)

source code 
Parameters:
  • lit (int)
Returns: bool | None

watch_lit(self, lit, cb)

source code 
Parameters:
  • lit (int)

name_lits(self, lst)

source code 
Parameters:
  • lst ([int])
Returns: [str]

name_lit(self, lit)

source code 
Parameters:
  • lit (int)
Returns: str

add_clause(self, lits)

source code 
Parameters:
  • lits ([int])
Returns: zeroinstall.injector.sat.UnionClause | bool

at_most_one(self, lits)

source code 
Parameters:
  • lits ([int])
Returns: zeroinstall.injector.sat.AtMostOneClause

   Home       Trees       Indices       Help   
Project Homepage
Generated by Epydoc 3.0.1 on Tue Mar 26 18:14:07 2013 http://epydoc.sourceforge.net