TO_BE_DOCUMENTED. More...

#include <prop.h>

Inheritance diagram for propt:

Collaboration diagram for propt:

Public Types
enum class	resultt { P_SATISFIABLE , P_UNSATISFIABLE , P_ERROR }

Public Member Functions
	propt (message_handlert &message_handler)

virtual	~propt ()

virtual literalt	land (literalt a, literalt b)=0

virtual literalt	lor (literalt a, literalt b)=0

virtual literalt	land (const bvt &bv)=0

virtual literalt	lor (const bvt &bv)=0

virtual literalt	lxor (literalt a, literalt b)=0

virtual literalt	lxor (const bvt &bv)=0

virtual literalt	lnand (literalt a, literalt b)=0

virtual literalt	lnor (literalt a, literalt b)=0

virtual literalt	lequal (literalt a, literalt b)=0

virtual literalt	limplies (literalt a, literalt b)=0

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

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 void	lcnf (const bvt &bv)=0

virtual bool	has_set_to () const

virtual bool	cnf_handled_well () const

virtual bool	has_assumptions () const

virtual literalt	new_variable ()=0

virtual void	set_variable_name (literalt, const irep_idt &)

virtual size_t	no_variables () const =0

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

virtual std::string	solver_text () const =0

resultt	prop_solve ()

resultt	prop_solve (const bvt &assumptions)

virtual tvt	l_get (literalt a) const =0

virtual void	set_assignment (literalt a, bool value)=0

virtual bool	is_in_conflict (literalt l) const =0
	Returns true if an assumption is in the final conflict. More...

virtual bool	has_is_in_conflict () const

virtual void	set_frozen (literalt)

virtual void	set_time_limit_seconds (uint32_t)

std::size_t	get_number_of_solver_calls () const

Protected Member Functions
virtual resultt	do_prop_solve (const bvt &assumptions)=0

Protected Attributes
bvt	lcnf_bv

messaget	log

std::size_t	number_of_solver_calls = 0

Detailed Description

TO_BE_DOCUMENTED.

Definition at line 24 of file prop.h.

Member Enumeration Documentation

◆ resultt

enum propt::resultt

strong

Enumerator
P_SATISFIABLE
P_UNSATISFIABLE
P_ERROR

Definition at line 101 of file prop.h.

Constructor & Destructor Documentation

◆ propt()

propt::propt ( message_handlert & message_handler )

inlineexplicit

Definition at line 27 of file prop.h.

◆ ~propt()

virtual propt::~propt ( )

inlinevirtual

Definition at line 31 of file prop.h.

Member Function Documentation

◆ cnf_handled_well()

virtual bool propt::cnf_handled_well ( ) const

inlinevirtual

Definition at line 85 of file prop.h.

◆ do_prop_solve()

virtual resultt propt::do_prop_solve ( const bvt & assumptions )

protectedpure virtual

Implemented in satcheck_zcoret, satcheck_zchaff_baset, satcheck_picosatt, satcheck_minisat1_coret, satcheck_minisat1_baset, satcheck_lingelingt, satcheck_ipasirt, satcheck_glucose_baset< T >, satcheck_glucose_baset< Glucose::Solver >, satcheck_glucose_baset< Glucose::SimpSolver >, satcheck_cadical_baset, satcheck_booleforce_baset, pbs_dimacs_cnft, external_satt, satcheck_minisat2_baset< T >, satcheck_minisat2_baset< Minisat::SimpSolver >, satcheck_minisat2_baset< Minisat::Solver >, dimacs_cnf_dumpt, and cnf_clause_listt.

◆ get_number_of_solver_calls()

std::size_t propt::get_number_of_solver_calls ( ) const

Definition at line 52 of file prop.cpp.

◆ has_assumptions()

virtual bool propt::has_assumptions ( ) const

inlinevirtual

Reimplemented in satcheck_minisat2_baset< T >, satcheck_minisat2_baset< Minisat::SimpSolver >, satcheck_minisat2_baset< Minisat::Solver >, satcheck_ipasirt, external_satt, satcheck_picosatt, satcheck_minisat1_baset, satcheck_lingelingt, satcheck_glucose_baset< T >, satcheck_glucose_baset< Glucose::Solver >, satcheck_glucose_baset< Glucose::SimpSolver >, and satcheck_cadical_baset.

Definition at line 88 of file prop.h.

◆ has_is_in_conflict()

virtual bool propt::has_is_in_conflict ( ) const

inlinevirtual

Reimplemented in satcheck_minisat2_baset< T >, satcheck_minisat2_baset< Minisat::SimpSolver >, satcheck_minisat2_baset< Minisat::Solver >, satcheck_ipasirt, external_satt, satcheck_picosatt, satcheck_minisat1_baset, satcheck_lingelingt, satcheck_glucose_baset< T >, satcheck_glucose_baset< Glucose::Solver >, satcheck_glucose_baset< Glucose::SimpSolver >, and satcheck_cadical_baset.

Definition at line 114 of file prop.h.

◆ has_set_to()

virtual bool propt::has_set_to ( ) const

inlinevirtual

Definition at line 81 of file prop.h.

◆ is_in_conflict()

virtual bool propt::is_in_conflict ( literalt l ) const

pure virtual

Returns true if an assumption is in the final conflict.

Note that only literals that are assumptions (see set_assumptions) may be queried.

Returns: true iff the given literal is part of the final conflict

Implemented in external_satt, satcheck_minisat1_baset, dimacs_cnft, satcheck_picosatt, satcheck_minisat2_baset< T >, satcheck_minisat2_baset< Minisat::SimpSolver >, satcheck_minisat2_baset< Minisat::Solver >, satcheck_lingelingt, satcheck_ipasirt, satcheck_glucose_baset< T >, satcheck_glucose_baset< Glucose::Solver >, satcheck_glucose_baset< Glucose::SimpSolver >, and satcheck_cadical_baset.

◆ l_get()

◆ l_set_to()

virtual void propt::l_set_to	(	literalt	a,
		bool	value
	)

inlinevirtual

Definition at line 47 of file prop.h.

◆ l_set_to_false()

void propt::l_set_to_false ( literalt a )

inline

Definition at line 54 of file prop.h.

◆ l_set_to_true()

void propt::l_set_to_true ( literalt a )

inline

Definition at line 52 of file prop.h.

◆ land() [1/2]

virtual literalt propt::land ( const bvt & bv )

pure virtual

Implemented in cnft.

◆ land() [2/2]

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

pure virtual

Implemented in cnft.

◆ lcnf() [1/4]

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

pure virtual

Implemented in satcheck_minisat2_baset< T >, satcheck_minisat2_baset< Minisat::SimpSolver >, satcheck_minisat2_baset< Minisat::Solver >, satcheck_ipasirt, satcheck_picosatt, satcheck_lingelingt, satcheck_glucose_baset< T >, satcheck_glucose_baset< Glucose::Solver >, satcheck_glucose_baset< Glucose::SimpSolver >, satcheck_cadical_baset, satcheck_booleforce_baset, dimacs_cnf_dumpt, cnf_clause_listt, qbf_squolem_coret, qbf_squolemt, qbf_bdd_coret, and satcheck_minisat1_baset.

◆ lcnf() [2/4]

void propt::lcnf	(	literalt	l0,
		literalt	l1
	)

inline

Definition at line 58 of file prop.h.

◆ lcnf() [3/4]

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

inline

Definition at line 61 of file prop.h.

◆ lcnf() [4/4]

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

inline

Definition at line 70 of file prop.h.

◆ lequal()

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

pure virtual

Implemented in cnft.

◆ limplies()

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

pure virtual

Implemented in cnft.

◆ lnand()

virtual literalt propt::lnand	(	literalt	a,
		literalt	b
	)

pure virtual

Implemented in cnft.

◆ lnor()

virtual literalt propt::lnor	(	literalt	a,
		literalt	b
	)

pure virtual

Implemented in cnft.

◆ lor() [1/2]

virtual literalt propt::lor ( const bvt & bv )

pure virtual

Implemented in cnft, and qbf_bdd_coret.

◆ lor() [2/2]

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

pure virtual

Implemented in cnft, and qbf_bdd_coret.

◆ lselect()

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

pure virtual

Implemented in cnft.

◆ lxor() [1/2]

virtual literalt propt::lxor ( const bvt & bv )

pure virtual

Implemented in cnft.

◆ lxor() [2/2]

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

pure virtual

Implemented in cnft.

◆ new_variable()

virtual literalt propt::new_variable ( )

pure virtual

Implemented in qbf_bdd_certificatet, cnft, and qbf_bdd_coret.

◆ new_variables()

bvt propt::new_variables ( std::size_t width )

virtual

generates a bitvector of given width with new variables

Returns: bitvector

Reimplemented in cnft.

Definition at line 30 of file prop.cpp.

◆ no_variables()

virtual size_t propt::no_variables ( ) const

pure virtual

Implemented in cnft.

◆ prop_solve() [1/2]

propt::resultt propt::prop_solve ( )

Definition at line 39 of file prop.cpp.

◆ prop_solve() [2/2]

propt::resultt propt::prop_solve ( const bvt & assumptions )

Definition at line 46 of file prop.cpp.

◆ set_assignment()

virtual void propt::set_assignment	(	literalt	a,
		bool	value
	)

pure virtual

Implemented in external_satt, satcheck_zchaff_baset, satcheck_picosatt, satcheck_minisat2_baset< T >, satcheck_minisat2_baset< Minisat::SimpSolver >, satcheck_minisat2_baset< Minisat::Solver >, satcheck_minisat1_baset, satcheck_lingelingt, satcheck_ipasirt, satcheck_glucose_baset< T >, satcheck_glucose_baset< Glucose::Solver >, satcheck_glucose_baset< Glucose::SimpSolver >, satcheck_cadical_baset, and dimacs_cnft.

◆ set_equal()

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

virtual

asserts a==b in the propositional formula

Definition at line 12 of file prop.cpp.

◆ set_frozen()

virtual void propt::set_frozen ( literalt )

inlinevirtual

Reimplemented in satcheck_minisat_simplifiert, satcheck_lingelingt, and satcheck_glucose_simplifiert.

Definition at line 117 of file prop.h.

◆ set_time_limit_seconds()

virtual void propt::set_time_limit_seconds ( uint32_t )

inlinevirtual

Reimplemented in satcheck_minisat2_baset< T >, satcheck_minisat2_baset< Minisat::SimpSolver >, and satcheck_minisat2_baset< Minisat::Solver >.

Definition at line 120 of file prop.h.

◆ set_variable_name()

virtual void propt::set_variable_name	(	literalt	,
		const irep_idt &
	)

inlinevirtual

Definition at line 95 of file prop.h.

◆ solver_text()

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

pure virtual

Member Data Documentation

◆ lcnf_bv

bvt propt::lcnf_bv

protected

Definition at line 132 of file prop.h.

◆ log

messaget propt::log

protected

Definition at line 134 of file prop.h.

◆ number_of_solver_calls

std::size_t propt::number_of_solver_calls = 0

protected

Definition at line 135 of file prop.h.

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

/home/runner/work/cbmc/cbmc/src/solvers/prop/prop.h
/home/runner/work/cbmc/cbmc/src/solvers/prop/prop.cpp

Public Types

Public Member Functions

Protected Member Functions

Protected Attributes

Detailed Description

Member Enumeration Documentation

◆ resultt

Constructor & Destructor Documentation

◆ propt()

◆ ~propt()

Member Function Documentation

◆ cnf_handled_well()

◆ do_prop_solve()

◆ get_number_of_solver_calls()

◆ has_assumptions()

◆ has_is_in_conflict()

◆ has_set_to()

◆ is_in_conflict()

◆ l_get()

◆ l_set_to()

◆ l_set_to_false()

◆ l_set_to_true()

◆ land() [1/2]

◆ land() [2/2]

◆ lcnf() [1/4]

◆ lcnf() [2/4]

◆ lcnf() [3/4]

◆ lcnf() [4/4]

◆ lequal()

◆ limplies()

◆ lnand()

◆ lnor()

◆ lor() [1/2]

◆ lor() [2/2]

◆ lselect()

◆ lxor() [1/2]

◆ lxor() [2/2]

◆ new_variable()

◆ new_variables()

◆ no_variables()

◆ prop_solve() [1/2]

◆ prop_solve() [2/2]

◆ set_assignment()

◆ set_equal()

◆ set_frozen()

◆ set_time_limit_seconds()

◆ set_variable_name()

◆ solver_text()

Member Data Documentation

◆ lcnf_bv

◆ log

◆ number_of_solver_calls