cnf_convt Class Reference

#include <cnf_conv.h>

Inheritance diagram for cnf_convt:

Public Member Functions
	cnf_convt (cnf_iface *cnf_api)
	~cnf_convt ()
virtual literalt	lnot (literalt a)
virtual literalt	lselect (literalt a, literalt b, literalt c)
virtual literalt	lequal (literalt a, literalt b)
virtual literalt	limplies (literalt a, literalt b)
virtual literalt	lxor (literalt a, literalt b)
virtual literalt	lor (literalt a, literalt b)
virtual literalt	land (literalt a, literalt b)
virtual void	gate_xor (literalt a, literalt b, literalt o)
virtual void	gate_or (literalt a, literalt b, literalt o)
virtual void	gate_and (literalt a, literalt b, literalt o)
virtual void	set_equal (literalt a, literalt b)
Public Member Functions inherited from sat_iface
virtual void	lcnf (const bvt &bv)=0
virtual void	assert_lit (const literalt &a)=0
virtual tvt	l_get (const literalt &a)=0
virtual literalt	new_variable ()=0

Public Attributes
cnf_iface *	cnf_api

Constructor & Destructor Documentation

cnf_convt()

cnf_convt::cnf_convt

(

cnf_iface *

cnf_api

)

~cnf_convt()

cnf_convt::~cnf_convt

(

)

Member Function Documentation

gate_and()

void cnf_convt::gate_and ( literalt a, literalt b, literalt o )

virtual

gate_or()

void cnf_convt::gate_or ( literalt a, literalt b, literalt o )

virtual

gate_xor()

void cnf_convt::gate_xor ( literalt a, literalt b, literalt o )

virtual

land()

literalt cnf_convt::land ( literalt a, literalt b )

virtual

Implements sat_iface.

lequal()

literalt cnf_convt::lequal ( literalt a, literalt b )

virtual

Implements sat_iface.

limplies()

literalt cnf_convt::limplies ( literalt a, literalt b )

virtual

Implements sat_iface.

lnot()

literalt cnf_convt::lnot ( literalt a )

virtual

Implements sat_iface.

lor()

literalt cnf_convt::lor ( literalt a, literalt b )

virtual

Implements sat_iface.

lselect()

literalt cnf_convt::lselect ( literalt a, literalt b, literalt c )

virtual

Implements sat_iface.

lxor()

literalt cnf_convt::lxor ( literalt a, literalt b )

virtual

Implements sat_iface.

set_equal()

void cnf_convt::set_equal ( literalt a, literalt b )

virtual

Implements sat_iface.

Member Data Documentation

cnf_api

cnf_iface* cnf_convt::cnf_api

---

The documentation for this class was generated from the following files:

• src/solvers/sat/cnf_conv.h
• src/solvers/sat/cnf_conv.cpp