10 #ifndef CPROVER_SOLVERS_QBF_QDIMACS_CORE_H 11 #define CPROVER_SOLVERS_QBF_QDIMACS_CORE_H 36 #endif // CPROVER_SOLVERS_QBF_QDIMACS_CORE_H variable_mapt variable_map
void simplify_extractbits(exprt &expr) const
std::map< unsigned, symbol_mapt > variable_mapt
virtual const exprt f_get(literalt v)=0
virtual modeltypet m_get(literalt a) const =0
virtual bool is_in_core(literalt l) const =0
Base class for all expressions.
virtual tvt l_get(literalt a) const =0
std::pair< exprt, unsigned > symbol_mapt