CaDiCaL::ExternalPropagator Class Reference

#include <cadical.hpp>

Public Member Functions
virtual	~ExternalPropagator ()
virtual void	notify_assignment (const std::vector< int > &lits)=0
virtual void	notify_new_decision_level ()=0
virtual void	notify_backtrack (size_t new_level)=0
virtual bool	cb_check_found_model (const std::vector< int > &model)=0
virtual int	cb_decide ()
virtual int	cb_propagate ()
virtual int	cb_add_reason_clause_lit (int propagated_lit)
virtual bool	cb_has_external_clause (bool &is_forgettable)=0
virtual int	cb_add_external_clause_lit ()=0

Public Attributes
bool	is_lazy = false
bool	are_reasons_forgettable

Detailed Description

Definition at line 1208 of file cadical.hpp.

Constructor & Destructor Documentation

~ExternalPropagator()

virtual CaDiCaL::ExternalPropagator::~ExternalPropagator ( )

inlinevirtual

Definition at line 1215 of file cadical.hpp.

{}

Member Function Documentation

cb_add_external_clause_lit()

virtual int CaDiCaL::ExternalPropagator::cb_add_external_clause_lit ( )

pure virtual

cb_add_reason_clause_lit()

virtual int CaDiCaL::ExternalPropagator::cb_add_reason_clause_lit ( int propagated_lit )

inlinevirtual

Definition at line 1254 of file cadical.hpp.

                                                            {
    (void) propagated_lit;
    return 0;
  };

cb_check_found_model()

virtual bool CaDiCaL::ExternalPropagator::cb_check_found_model ( const std::vector< int > & model )

pure virtual

cb_decide()

virtual int CaDiCaL::ExternalPropagator::cb_decide ( )

inlinevirtual

Definition at line 1237 of file cadical.hpp.

{ return 0; };

cb_has_external_clause()

virtual bool CaDiCaL::ExternalPropagator::cb_has_external_clause ( bool & is_forgettable )

pure virtual

cb_propagate()

virtual int CaDiCaL::ExternalPropagator::cb_propagate ( )

inlinevirtual

Definition at line 1244 of file cadical.hpp.

{ return 0; };

notify_assignment()

virtual void CaDiCaL::ExternalPropagator::notify_assignment ( const std::vector< int > & lits )

pure virtual

notify_backtrack()

virtual void CaDiCaL::ExternalPropagator::notify_backtrack ( size_t new_level )

pure virtual

notify_new_decision_level()

virtual void CaDiCaL::ExternalPropagator::notify_new_decision_level ( )

pure virtual

Member Data Documentation

are_reasons_forgettable

bool CaDiCaL::ExternalPropagator::are_reasons_forgettable

Initial value:

=
      false

Definition at line 1212 of file cadical.hpp.

is_lazy

bool CaDiCaL::ExternalPropagator::is_lazy = false

Definition at line 1211 of file cadical.hpp.

---

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

• src/sat/cadical/cadical.hpp