CaDiCaL::Tracer Class Reference

#include <tracer.hpp>

Inheritance diagram for CaDiCaL::Tracer:

Public Member Functions
	Tracer ()
virtual	~Tracer ()
virtual void	add_original_clause (int64_t, bool, const std::vector< int > &, bool=false)
virtual void	add_derived_clause (int64_t, bool, const std::vector< int > &, const std::vector< int64_t > &)
virtual void	delete_clause (int64_t, bool, const std::vector< int > &)
virtual void	demote_clause (uint64_t, const std::vector< int > &)
virtual void	weaken_minus (int64_t, const std::vector< int > &)
virtual void	strengthen (int64_t)
virtual void	report_status (int, int64_t)
virtual void	finalize_clause (int64_t, const std::vector< int > &)
virtual void	begin_proof (int64_t)
virtual void	solve_query ()
virtual void	add_assumption (int)
virtual void	add_constraint (const std::vector< int > &)
virtual void	reset_assumptions ()
virtual void	add_assumption_clause (int64_t, const std::vector< int > &, const std::vector< int64_t > &)
virtual void	conclude_unsat (ConclusionType, const std::vector< int64_t > &)
virtual void	conclude_sat (const std::vector< int > &)
virtual void	conclude_unknown (const std::vector< int > &)

Detailed Description

Definition at line 21 of file tracer.hpp.

Constructor & Destructor Documentation

Tracer()

CaDiCaL::Tracer::Tracer ( )

inline

Definition at line 24 of file tracer.hpp.

{}

~Tracer()

virtual CaDiCaL::Tracer::~Tracer ( )

inlinevirtual

Definition at line 25 of file tracer.hpp.

{}

Member Function Documentation

add_assumption()

virtual void CaDiCaL::Tracer::add_assumption ( int )

inlinevirtual

Reimplemented in CaDiCaL::IdrupTracer, CaDiCaL::LidrupTracer, and CaDiCaL::LratChecker.

Definition at line 110 of file tracer.hpp.

{}

add_assumption_clause()

virtual void CaDiCaL::Tracer::add_assumption_clause ( int64_t , const std::vector< int > & , const std::vector< int64_t > &  )

inlinevirtual

Definition at line 126 of file tracer.hpp.

                                                                  {}

add_constraint()

virtual void CaDiCaL::Tracer::add_constraint ( const std::vector< int > & )

inlinevirtual

Definition at line 115 of file tracer.hpp.

{}

add_derived_clause()

virtual void CaDiCaL::Tracer::add_derived_clause ( int64_t , bool , const std::vector< int > & , const std::vector< int64_t > &  )

inlinevirtual

Definition at line 45 of file tracer.hpp.

                                                               {}

add_original_clause()

virtual void CaDiCaL::Tracer::add_original_clause ( int64_t , bool , const std::vector< int > & , bool = false )

inlinevirtual

Definition at line 37 of file tracer.hpp.

                                                  {}

begin_proof()

virtual void CaDiCaL::Tracer::begin_proof ( int64_t )

inlinevirtual

Reimplemented in CaDiCaL::Checker, CaDiCaL::DratTracer, CaDiCaL::FratTracer, CaDiCaL::IdrupTracer, CaDiCaL::LidrupTracer, CaDiCaL::LratChecker, CaDiCaL::LratTracer, and CaDiCaL::VeripbTracer.

Definition at line 94 of file tracer.hpp.

{}

conclude_sat()

virtual void CaDiCaL::Tracer::conclude_sat ( const std::vector< int > & )

inlinevirtual

Definition at line 140 of file tracer.hpp.

{}

conclude_unknown()

virtual void CaDiCaL::Tracer::conclude_unknown ( const std::vector< int > & )

inlinevirtual

Definition at line 145 of file tracer.hpp.

{}

conclude_unsat()

virtual void CaDiCaL::Tracer::conclude_unsat ( ConclusionType , const std::vector< int64_t > &  )

inlinevirtual

Definition at line 134 of file tracer.hpp.

                                                           {}

delete_clause()

virtual void CaDiCaL::Tracer::delete_clause ( int64_t , bool , const std::vector< int > &  )

inlinevirtual

Definition at line 52 of file tracer.hpp.

{}

demote_clause()

virtual void CaDiCaL::Tracer::demote_clause ( uint64_t , const std::vector< int > &  )

inlinevirtual

Definition at line 58 of file tracer.hpp.

{}

finalize_clause()

virtual void CaDiCaL::Tracer::finalize_clause ( int64_t , const std::vector< int > &  )

inlinevirtual

Definition at line 88 of file tracer.hpp.

{}

report_status()

virtual void CaDiCaL::Tracer::report_status ( int , int64_t  )

inlinevirtual

Reimplemented in CaDiCaL::Checker, CaDiCaL::DratTracer, CaDiCaL::FratTracer, CaDiCaL::IdrupTracer, CaDiCaL::LidrupTracer, CaDiCaL::LratChecker, CaDiCaL::LratTracer, and CaDiCaL::VeripbTracer.

Definition at line 77 of file tracer.hpp.

{}

reset_assumptions()

virtual void CaDiCaL::Tracer::reset_assumptions ( )

inlinevirtual

Reimplemented in CaDiCaL::IdrupTracer, CaDiCaL::LidrupTracer, and CaDiCaL::LratChecker.

Definition at line 119 of file tracer.hpp.

{}

solve_query()

virtual void CaDiCaL::Tracer::solve_query ( )

inlinevirtual

Reimplemented in CaDiCaL::IdrupTracer, and CaDiCaL::LidrupTracer.

Definition at line 105 of file tracer.hpp.

{}

strengthen()

virtual void CaDiCaL::Tracer::strengthen ( int64_t )

inlinevirtual

Reimplemented in CaDiCaL::IdrupTracer, CaDiCaL::LidrupTracer, and CaDiCaL::VeripbTracer.

Definition at line 68 of file tracer.hpp.

{}

weaken_minus()

virtual void CaDiCaL::Tracer::weaken_minus ( int64_t , const std::vector< int > &  )

inlinevirtual

Definition at line 63 of file tracer.hpp.

{}

---

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

• src/sat/cadical/tracer.hpp