sat_iface Class Reference

#include <sat_iface.h>

Inheritance diagram for sat_iface:

Public Member Functions
virtual void	lcnf (const bvt &bv)=0
virtual literalt	lnot (literalt a)=0
virtual literalt	lselect (literalt a, literalt b, literalt c)=0
virtual literalt	lequal (literalt a, literalt b)=0
virtual literalt	limplies (literalt a, literalt b)=0
virtual literalt	lxor (literalt a, literalt b)=0
virtual literalt	land (literalt a, literalt b)=0
virtual literalt	lor (literalt a, literalt b)=0
virtual void	set_equal (literalt a, literalt b)=0
virtual void	assert_lit (const literalt &a)=0
virtual tvt	l_get (const literalt &a)=0
virtual literalt	new_variable ()=0

Member Function Documentation

assert_lit()

virtual void sat_iface::assert_lit ( const literalt & a )

pure virtual

Implemented in minisat_convt.

l_get()

virtual tvt sat_iface::l_get ( const literalt & a )

pure virtual

Implemented in minisat_convt.

land()

virtual literalt sat_iface::land ( literalt a, literalt b )

pure virtual

Implemented in cnf_convt.

lcnf()

virtual void sat_iface::lcnf ( const bvt & bv )

pure virtual

Implemented in minisat_convt.

lequal()

virtual literalt sat_iface::lequal ( literalt a, literalt b )

pure virtual

Implemented in cnf_convt.

limplies()

virtual literalt sat_iface::limplies ( literalt a, literalt b )

pure virtual

Implemented in cnf_convt.

lnot()

virtual literalt sat_iface::lnot ( literalt a )

pure virtual

Implemented in cnf_convt.

lor()

virtual literalt sat_iface::lor ( literalt a, literalt b )

pure virtual

Implemented in cnf_convt.

lselect()

virtual literalt sat_iface::lselect ( literalt a, literalt b, literalt c )

pure virtual

Implemented in cnf_convt.

lxor()

virtual literalt sat_iface::lxor ( literalt a, literalt b )

pure virtual

Implemented in cnf_convt.

new_variable()

virtual literalt sat_iface::new_variable ( )

pure virtual

Implemented in minisat_convt.

set_equal()

virtual void sat_iface::set_equal ( literalt a, literalt b )

pure virtual

Implemented in cnf_convt.

---

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

• src/solvers/sat/sat_iface.h