cnfgen.clihelpers.transformation_helpers module

Transformation Helpers for command line

Copyright (C) 2012, 2013, 2014, 2015, 2016, 2019, 2020, 2021 Massimo Lauria <massimo.lauria@uniroma1.it> https://massimolauria.net/cnfgen/

class AllEqualsSubstitutionCmd

Bases: cnfgen.clihelpers.transformation_helpers.TransformationHelper

Methods

setup_command_line(parser)	Setup the command line parser for this transformation subcommand
transform_cnf(F, args)	Build the new CNF by applying the transformation

description = 'substitute x with predicate x1==x2==...==xN (i.e. all equals)'

name = 'eq'

static setup_command_line(parser)

Setup the command line parser for this transformation subcommand

static transform_cnf(F, args)

Build the new CNF by applying the transformation

class AnythingButKSubstitutionCmd

Bases: cnfgen.clihelpers.transformation_helpers.TransformationHelper

Methods

setup_command_line(parser)	Setup the command line parser for this transformation subcommand
transform_cnf(F, args)	Build the new CNF by applying the transformation

description = 'substitute x with x1 + x2 + ... + xN != K'

name = 'anybut'

static setup_command_line(parser)

Setup the command line parser for this transformation subcommand

static transform_cnf(F, args)

Build the new CNF by applying the transformation

class AtLeastKSubstitutionCmd

Bases: cnfgen.clihelpers.transformation_helpers.TransformationHelper

Methods

setup_command_line(parser)	Setup the command line parser for this transformation subcommand
transform_cnf(F, args)	Build the new CNF by applying the transformation

description = 'substitute x with x1 + x2 + ... + xN >= K'

name = 'atleast'

static setup_command_line(parser)

Setup the command line parser for this transformation subcommand

static transform_cnf(F, args)

Build the new CNF by applying the transformation

class AtMostKSubstitutionCmd

Bases: cnfgen.clihelpers.transformation_helpers.TransformationHelper

Methods

setup_command_line(parser)	Setup the command line parser for this transformation subcommand
transform_cnf(F, args)	Build the new CNF by applying the transformation

description = 'substitute x with x1 + x2 + ... + xN <= K'

name = 'atmost'

static setup_command_line(parser)

Setup the command line parser for this transformation subcommand

static transform_cnf(F, args)

Build the new CNF by applying the transformation

class ExactlyKSubstitutionCmd

Bases: cnfgen.clihelpers.transformation_helpers.TransformationHelper

Methods

setup_command_line(parser)	Setup the command line parser for this transformation subcommand
transform_cnf(F, args)	Build the new CNF by applying the transformation

description = 'substitute x with x1 + x2 + ... + xN == K'

name = 'exact'

static setup_command_line(parser)

Setup the command line parser for this transformation subcommand

static transform_cnf(F, args)

Build the new CNF by applying the transformation

class ExactlyOneSubstitutionCmd

Bases: cnfgen.clihelpers.transformation_helpers.TransformationHelper

Methods

setup_command_line(parser)	Setup the command line parser for this transformation subcommand
transform_cnf(F, args)	Build the new CNF by applying the transformation

description = 'substitute x with x1 + x2 + ... + xN = 1'

name = 'one'

static setup_command_line(parser)

Setup the command line parser for this transformation subcommand

static transform_cnf(F, args)

Build the new CNF by applying the transformation

class FlipCmd

Bases: cnfgen.clihelpers.transformation_helpers.TransformationHelper

Methods

setup_command_line(parser)	Setup the command line parser for this transformation subcommand
transform_cnf(F, args)	Build the new CNF by applying the transformation

description = 'negate all variables in the formula'

name = 'flip'

static setup_command_line(parser)

Setup the command line parser for this transformation subcommand

static transform_cnf(F, args)

Build the new CNF by applying the transformation

class FormulaLiftingCmd

Bases: cnfgen.clihelpers.transformation_helpers.TransformationHelper

Lifting

Methods

setup_command_line(parser)	Setup the command line parser for this transformation subcommand
transform_cnf(F, args)	Build the new CNF by applying the transformation

description = 'one dimensional lifting x --> x1 y1 OR ... OR xN yN, with y1+..+yN = 1'

name = 'lift'

static setup_command_line(parser)

Setup the command line parser for this transformation subcommand

static transform_cnf(F, args)

Build the new CNF by applying the transformation

class IfThenElseSubstitutionCmd

Bases: cnfgen.clihelpers.transformation_helpers.TransformationHelper

Methods

setup_command_line(parser)	Setup the command line parser for this transformation subcommand
transform_cnf(F, args)	Build the new CNF by applying the transformation

description = 'substitute x with "if X then Y else Z"'

name = 'ite'

static setup_command_line(parser)

Setup the command line parser for this transformation subcommand

static transform_cnf(F, args)

Build the new CNF by applying the transformation

class MajCompressionCmd

Bases: cnfgen.clihelpers.transformation_helpers.TransformationHelper

Methods

setup_command_line(parser)	Setup the command line parser for this transformation subcommand
transform_cnf(F, args)	Build the new CNF by applying the transformation

description = 'variable compression using Majority'

name = 'majcomp'

static setup_command_line(parser)

Setup the command line parser for this transformation subcommand

static transform_cnf(F, args)

Build the new CNF by applying the transformation

class MajSubstitution

Bases: cnfgen.clihelpers.transformation_helpers.TransformationHelper

Methods

setup_command_line(parser)	Setup the command line parser for this transformation subcommand
transform_cnf(F, args)	Build the new CNF by applying the transformation

description = 'substitute x with Majority(x1,x2,...,xN)'

name = 'maj'

static setup_command_line(parser)

Setup the command line parser for this transformation subcommand

static transform_cnf(F, args)

Build the new CNF by applying the transformation

class NeqSubstitutionCmd

Bases: cnfgen.clihelpers.transformation_helpers.TransformationHelper

Methods

setup_command_line(parser)	Setup the command line parser for this transformation subcommand
transform_cnf(F, args)	Build the new CNF by applying the transformation

description = 'substitute x with |{x1,x2,...,xN}|>1 (i.e. not all equals)'

name = 'neq'

static setup_command_line(parser)

Setup the command line parser for this transformation subcommand

static transform_cnf(F, args)

Build the new CNF by applying the transformation

class NoSubstitutionCmd

Bases: cnfgen.clihelpers.transformation_helpers.TransformationHelper

Methods

setup_command_line(parser)	Setup the command line parser for this transformation subcommand
transform_cnf(F, args)	Build the new CNF by applying the transformation

description = 'no transformation'

name = 'none'

static setup_command_line(parser)

Setup the command line parser for this transformation subcommand

static transform_cnf(F, args)

Build the new CNF by applying the transformation

class OrSubstitutionCmd

Bases: cnfgen.clihelpers.transformation_helpers.TransformationHelper

Methods

setup_command_line(parser)	Setup the command line parser for this transformation subcommand
transform_cnf(F, args)	Build the new CNF by applying the transformation

description = 'substitute variable x with OR(x1,x2,...,xN)'

name = 'or'

static setup_command_line(parser)

Setup the command line parser for this transformation subcommand

static transform_cnf(F, args)

Build the new CNF by applying the transformation

class ShuffleCmd

Bases: cnfgen.clihelpers.transformation_helpers.TransformationHelper

Shuffle

Methods

setup_command_line(parser)	Setup the command line parser for this transformation subcommand
transform_cnf(F, args)	Build the new CNF by applying the transformation

description = 'Permute variables, clauses and polarity of literals at random'

name = 'shuffle'

static setup_command_line(parser)

Setup the command line parser for this transformation subcommand

static transform_cnf(F, args)

Build the new CNF by applying the transformation

class TransformationHelper

Bases: object

Command line helper for a formula family

Methods

setup_command_line(parser)	Setup the command line parser for this transformation subcommand
transform_cnf(F, args)	Build the new CNF by applying the transformation

description = ''

name = ''

static setup_command_line(parser)

Setup the command line parser for this transformation subcommand

static transform_cnf(F, args)

Build the new CNF by applying the transformation

class XorCompressionCmd

Bases: cnfgen.clihelpers.transformation_helpers.TransformationHelper

Methods

setup_command_line(parser)	Setup the command line parser for this transformation subcommand
transform_cnf(F, args)	Build the new CNF by applying the transformation

description = 'variable compression using XOR'

name = 'xorcomp'

static setup_command_line(parser)

Setup the command line parser for this transformation subcommand

static transform_cnf(F, args)

Build the new CNF by applying the transformation

class XorSubstitutionCmd

Bases: cnfgen.clihelpers.transformation_helpers.TransformationHelper

Methods

setup_command_line(parser)	Setup the command line parser for this transformation subcommand
transform_cnf(F, args)	Build the new CNF by applying the transformation

description = 'substitute variable x with XOR(x1,x2,...,xN)'

name = 'xor'

static setup_command_line(parser)

Setup the command line parser for this transformation subcommand

static transform_cnf(F, args)

Build the new CNF by applying the transformation