#include <smt2_prop.h>

Inheritance diagram for smt2_propt:

Collaboration diagram for smt2_propt:

Public Member Functions
	smt2_propt (const std::string &_benchmark, const std::string &_source, const std::string &_logic, bool _core_enabled, std::ostream &_out)

virtual	~smt2_propt ()

virtual literalt	land (literalt a, literalt b)

virtual literalt	lor (literalt a, literalt b)

virtual literalt	land (const bvt &bv)

virtual literalt	lor (const bvt &bv)

virtual literalt	lxor (const bvt &bv)

virtual literalt	lxor (literalt a, literalt b)

virtual literalt	lnand (literalt a, literalt b)

virtual literalt	lnor (literalt a, literalt b)

virtual literalt	lequal (literalt a, literalt b)

virtual literalt	limplies (literalt a, literalt b)

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

virtual literalt	new_variable ()

virtual size_t	no_variables () const

virtual void	set_no_variables (size_t no)

virtual void	lcnf (const bvt &bv)

virtual const std::string	solver_text ()

virtual tvt	l_get (literalt literal) const

virtual void	set_assignment (literalt a, bool value)

virtual propt::resultt	prop_solve ()

virtual void	clear ()

virtual void	reset_assignment ()

void	finalize ()

Public Member Functions inherited from propt
	propt ()

virtual	~propt ()

virtual void	set_equal (literalt a, literalt b)
	asserts a==b in the propositional formula More...

virtual void	l_set_to (literalt a, bool value)

void	l_set_to_true (literalt a)

void	l_set_to_false (literalt a)

void	lcnf (literalt l0, literalt l1)

void	lcnf (literalt l0, literalt l1, literalt l2)

void	lcnf (literalt l0, literalt l1, literalt l2, literalt l3)

virtual bool	has_set_to () const

virtual bool	cnf_handled_well () const

virtual void	set_assumptions (const bvt &_assumptions)

virtual bool	has_set_assumptions () const

virtual void	set_variable_name (literalt a, const std::string &name)

bvt	new_variables (std::size_t width)
	generates a bitvector of given width with new variables More...

virtual void	copy_assignment_from (const propt &prop)

virtual bool	is_in_conflict (literalt l) const

virtual bool	has_is_in_conflict () const

virtual void	set_frozen (literalt a)

Public Member Functions inherited from messaget
virtual void	set_message_handler (message_handlert &_message_handler)

message_handlert &	get_message_handler ()

	messaget ()

	messaget (const messaget &other)

	messaget (message_handlert &_message_handler)

virtual	~messaget ()

mstreamt &	get_mstream (unsigned message_level)

mstreamt &	error ()

mstreamt &	warning ()

mstreamt &	result ()

mstreamt &	status ()

mstreamt &	statistics ()

mstreamt &	progress ()

mstreamt &	debug ()

Public Member Functions inherited from prop_assignmentt
virtual	~prop_assignmentt ()

Protected Types
typedef std::set< std::string >	smt2_identifierst

Protected Member Functions
std::string	smt2_literal (literalt l)

literalt	def_smt2_literal ()

literalt	define_new_variable ()

Protected Attributes
size_t	_no_variables

std::ostream &	out

std::vector< tvt >	assignment

smt2_identifierst	smt2_identifiers

bool	core_enabled

Protected Attributes inherited from propt
bvt	lcnf_bv

Protected Attributes inherited from messaget
message_handlert *	message_handler

mstreamt	mstream

Friends
class	smt2_convt

class	smt2_dect

Additional Inherited Members
Public Types inherited from propt
enum	resultt { resultt::P_SATISFIABLE, resultt::P_UNSATISFIABLE, resultt::P_ERROR }

Public Types inherited from messaget
enum	message_levelt { M_ERROR =1, M_WARNING =2, M_RESULT =4, M_STATUS =6, M_STATISTICS =8, M_PROGRESS =9, M_DEBUG =10 }

Static Public Member Functions inherited from messaget
static mstreamt &	eom (mstreamt &m)

static mstreamt &	endl (mstreamt &m)

Detailed Description

Definition at line 20 of file smt2_prop.h.

Member Typedef Documentation

◆ smt2_identifierst

typedef std::set<std::string> smt2_propt::smt2_identifierst

protected

Definition at line 84 of file smt2_prop.h.

Constructor & Destructor Documentation

◆ smt2_propt()

smt2_propt::smt2_propt	(	const std::string &	_benchmark,
		const std::string &	_source,
		const std::string &	_logic,
		bool	_core_enabled,
		std::ostream &	_out
	)

Definition at line 13 of file smt2_prop.cpp.

References _no_variables, core_enabled, and out.

◆ ~smt2_propt()

smt2_propt::~smt2_propt ( )

virtual

Definition at line 37 of file smt2_prop.cpp.

Member Function Documentation

◆ clear()

virtual void smt2_propt::clear ( void )

inlinevirtual

Definition at line 57 of file smt2_prop.h.

References assignment.

◆ def_smt2_literal()

literalt smt2_propt::def_smt2_literal ( )

protected

◆ define_new_variable()

literalt smt2_propt::define_new_variable ( )

protected

Definition at line 254 of file smt2_prop.cpp.

References _no_variables, out, literalt::set(), and smt2_literal().

Referenced by land(), lor(), lselect(), and lxor().

◆ finalize()

void smt2_propt::finalize ( )

Definition at line 41 of file smt2_prop.cpp.

References core_enabled, out, and smt2_identifiers.

◆ l_get()

tvt smt2_propt::l_get ( literalt literal ) const

virtual

Implements propt.

Definition at line 307 of file smt2_prop.cpp.

References assignment, literalt::is_false(), literalt::is_true(), r, literalt::sign(), tvt::TV_UNKNOWN, and literalt::var_no().

◆ land() [1/2]

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

virtual

Implements propt.

Definition at line 117 of file smt2_prop.cpp.

References const_literal(), define_new_variable(), out, and smt2_literal().

Referenced by lnand().

◆ land() [2/2]

literalt smt2_propt::land ( const bvt & bv )

virtual

Implements propt.

Definition at line 61 of file smt2_prop.cpp.

References define_new_variable(), forall_literals, out, and smt2_literal().

◆ lcnf()

void smt2_propt::lcnf ( const bvt & bv )

virtual

Implements propt.

Definition at line 267 of file smt2_prop.cpp.

References out, and smt2_literal().

◆ lequal()

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

virtual

Implements propt.

Definition at line 203 of file smt2_prop.cpp.

References lxor().

◆ limplies()

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

virtual

Implements propt.

Definition at line 208 of file smt2_prop.cpp.

References lor().

◆ lnand()

literalt smt2_propt::lnand	(	literalt	a,
		literalt	b
	)

virtual

Implements propt.

Definition at line 193 of file smt2_prop.cpp.

References land().

◆ lnor()

literalt smt2_propt::lnor	(	literalt	a,
		literalt	b
	)

virtual

Implements propt.

Definition at line 198 of file smt2_prop.cpp.

References lor().

◆ lor() [1/2]

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

virtual

Implements propt.

Definition at line 143 of file smt2_prop.cpp.

References const_literal(), define_new_variable(), out, and smt2_literal().

Referenced by limplies(), and lnor().

◆ lor() [2/2]

literalt smt2_propt::lor ( const bvt & bv )

virtual

Implements propt.

Definition at line 78 of file smt2_prop.cpp.

References define_new_variable(), forall_literals, out, and smt2_literal().

◆ lselect()

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

virtual

Implements propt.

Definition at line 213 of file smt2_prop.cpp.

References const_literal(), define_new_variable(), out, and smt2_literal().

◆ lxor() [1/2]

literalt smt2_propt::lxor ( const bvt & bv )

virtual

Implements propt.

Definition at line 95 of file smt2_prop.cpp.

References const_literal(), define_new_variable(), forall_literals, out, and smt2_literal().

Referenced by lequal().

◆ lxor() [2/2]

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

virtual

Implements propt.

Definition at line 169 of file smt2_prop.cpp.

References const_literal(), new_variable(), out, and smt2_literal().

◆ new_variable()

literalt smt2_propt::new_variable ( void )

virtual

Implements propt.

Definition at line 243 of file smt2_prop.cpp.

References _no_variables, out, literalt::set(), and smt2_literal().

Referenced by lxor().

◆ no_variables()

virtual size_t smt2_propt::no_variables ( ) const

inlinevirtual

Implements propt.

Definition at line 44 of file smt2_prop.h.

References _no_variables.

Referenced by reset_assignment().

◆ prop_solve()

propt::resultt smt2_propt::prop_solve ( )

virtual

Implements propt.

Definition at line 331 of file smt2_prop.cpp.

◆ reset_assignment()

virtual void smt2_propt::reset_assignment ( )

inlinevirtual

Definition at line 62 of file smt2_prop.h.

References assignment, no_variables(), and tvt::TV_UNKNOWN.

◆ set_assignment()

void smt2_propt::set_assignment	(	literalt	a,
		bool	value
	)

virtual

Reimplemented from propt.

Definition at line 321 of file smt2_prop.cpp.

References assignment, literalt::is_false(), literalt::is_true(), and literalt::var_no().

◆ set_no_variables()

virtual void smt2_propt::set_no_variables ( size_t no )

inlinevirtual

Definition at line 45 of file smt2_prop.h.

◆ smt2_literal()

std::string smt2_propt::smt2_literal ( literalt l )

protected

Definition at line 290 of file smt2_prop.cpp.

References const_literal(), literalt::sign(), smt2_identifiers, and literalt::var_no().

Referenced by define_new_variable(), land(), lcnf(), lor(), lselect(), lxor(), and new_variable().

◆ solver_text()

virtual const std::string smt2_propt::solver_text ( )

inlinevirtual

Implements propt.

Definition at line 49 of file smt2_prop.h.

Friends And Related Function Documentation

◆ smt2_convt

friend class smt2_convt

friend

Definition at line 68 of file smt2_prop.h.

◆ smt2_dect

friend class smt2_dect

friend

Definition at line 69 of file smt2_prop.h.

Member Data Documentation

◆ _no_variables

size_t smt2_propt::_no_variables

protected

Definition at line 74 of file smt2_prop.h.

Referenced by define_new_variable(), new_variable(), no_variables(), and smt2_propt().

◆ assignment

std::vector<tvt> smt2_propt::assignment

protected

Definition at line 80 of file smt2_prop.h.

Referenced by clear(), l_get(), reset_assignment(), and set_assignment().

◆ core_enabled

bool smt2_propt::core_enabled

protected

Definition at line 87 of file smt2_prop.h.

Referenced by finalize(), and smt2_propt().

◆ out

std::ostream& smt2_propt::out

protected

Definition at line 75 of file smt2_prop.h.

Referenced by define_new_variable(), finalize(), land(), lcnf(), lor(), lselect(), lxor(), new_variable(), and smt2_propt().

◆ smt2_identifiers

smt2_identifierst smt2_propt::smt2_identifiers

protected

Definition at line 85 of file smt2_prop.h.

Referenced by finalize(), and smt2_literal().

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

solvers/smt2/smt2_prop.h
solvers/smt2/smt2_prop.cpp

Public Member Functions

Protected Types

Protected Member Functions

Protected Attributes

Friends

Additional Inherited Members

Detailed Description

Member Typedef Documentation

◆ smt2_identifierst

Constructor & Destructor Documentation

◆ smt2_propt()

◆ ~smt2_propt()

Member Function Documentation

◆ clear()

◆ def_smt2_literal()

◆ define_new_variable()

◆ finalize()

◆ l_get()

◆ land() [1/2]

◆ land() [2/2]

◆ lcnf()

◆ lequal()

◆ limplies()

◆ lnand()

◆ lnor()

◆ lor() [1/2]

◆ lor() [2/2]

◆ lselect()

◆ lxor() [1/2]

◆ lxor() [2/2]

◆ new_variable()

◆ no_variables()

◆ prop_solve()

◆ reset_assignment()

◆ set_assignment()

◆ set_no_variables()

◆ smt2_literal()

◆ solver_text()

Friends And Related Function Documentation

◆ smt2_convt

◆ smt2_dect

Member Data Documentation

◆ _no_variables

◆ assignment

◆ core_enabled

◆ out

◆ smt2_identifiers