smtrat::UnsatCore< Solver, Strategy > Class Template Reference

#include <UnsatCore.h>

Inheritance diagram for smtrat::UnsatCore< Solver, Strategy >:

Collaboration diagram for smtrat::UnsatCore< Solver, Strategy >:

Public Member Functions
	UnsatCore (Solver &s)
void	add_annotated_name (const FormulaT &formula, const std::string &name)
void	remove_annotated_name (const FormulaT &formula)
void	reset ()
bool	active () const
std::pair< Answer, FormulasT >	compute_core (const FormulasT &formulas)
std::pair< Answer, std::vector< std::string > >	compute ()

Private Attributes
std::map< FormulaT, std::string >	mAnnotatedNames
std::vector< FormulaT >	mFormulas
Solver &	mSolver

Detailed Description

template<typename Solver, UnsatCoreStrategy Strategy>
class smtrat::UnsatCore< Solver, Strategy >

Definition at line 26 of file UnsatCore.h.

Constructor & Destructor Documentation

UnsatCore()

template<typename Solver , UnsatCoreStrategy Strategy>

smtrat::UnsatCore< Solver, Strategy >::UnsatCore ( Solver &  s )

inline

Definition at line 33 of file UnsatCore.h.

Member Function Documentation

active()

template<typename Solver , UnsatCoreStrategy Strategy>

bool smtrat::UnsatCore< Solver, Strategy >::active ( ) const

inline

Definition at line 49 of file UnsatCore.h.

add_annotated_name()

template<typename Solver , UnsatCoreStrategy Strategy>

void smtrat::UnsatCore< Solver, Strategy >::add_annotated_name ( const FormulaT &  formula, const std::string &  name  )

inline

Definition at line 35 of file UnsatCore.h.

Here is the caller graph for this function:

compute()

template<typename Solver , UnsatCoreStrategy Strategy>

std::pair<Answer,std::vector<std::string> > smtrat::UnsatCore< Solver, Strategy >::compute ( )

inline

Definition at line 79 of file UnsatCore.h.

Here is the call graph for this function:

Here is the caller graph for this function:

compute_core()

template<typename Solver , UnsatCoreStrategy Strategy>

std::pair<Answer,FormulasT> smtrat::UnsatCore< Solver, Strategy >::compute_core ( const FormulasT &  formulas )

inline

Definition at line 53 of file UnsatCore.h.

Here is the call graph for this function:

Here is the caller graph for this function:

remove_annotated_name()

template<typename Solver , UnsatCoreStrategy Strategy>

void smtrat::UnsatCore< Solver, Strategy >::remove_annotated_name ( const FormulaT &  formula )

inline

Definition at line 40 of file UnsatCore.h.

Here is the call graph for this function:

Here is the caller graph for this function:

reset()

template<typename Solver , UnsatCoreStrategy Strategy>

void smtrat::UnsatCore< Solver, Strategy >::reset ( )

inline

Definition at line 45 of file UnsatCore.h.

Here is the caller graph for this function:

Field Documentation

mAnnotatedNames

template<typename Solver , UnsatCoreStrategy Strategy>

std::map<FormulaT, std::string> smtrat::UnsatCore< Solver, Strategy >::mAnnotatedNames

private

Definition at line 28 of file UnsatCore.h.

mFormulas

template<typename Solver , UnsatCoreStrategy Strategy>

std::vector<FormulaT> smtrat::UnsatCore< Solver, Strategy >::mFormulas

private

Definition at line 29 of file UnsatCore.h.

mSolver

template<typename Solver , UnsatCoreStrategy Strategy>

Solver& smtrat::UnsatCore< Solver, Strategy >::mSolver

private

Definition at line 30 of file UnsatCore.h.

---

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

• smtrat-unsat-cores/UnsatCore.h