From 1802e870876d0595d8f6e1f8f283cc6d1f03f13d Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 24 Aug 2018 18:49:22 -0500 Subject: [PATCH] Fix more simple coverity warnings (#2372) --- src/theory/datatypes/theory_datatypes.cpp | 59 +++++-------------- src/theory/datatypes/theory_datatypes.h | 17 +++--- .../quantifiers/cegqi/ceg_bv_instantiator.cpp | 2 +- .../quantifiers/cegqi/inst_strategy_cbqi.cpp | 13 ++-- .../quantifiers/cegqi/inst_strategy_cbqi.h | 11 ++++ .../quantifiers/conjecture_generator.cpp | 22 +++---- src/theory/quantifiers/conjecture_generator.h | 15 ++++- .../ematching/candidate_generator.cpp | 5 +- src/theory/quantifiers/first_order_model.cpp | 8 --- src/theory/quantifiers/first_order_model.h | 6 -- src/theory/quantifiers/fmf/model_builder.cpp | 29 ++------- src/theory/quantifiers/fmf/model_builder.h | 4 -- src/theory/sets/theory_sets_private.cpp | 50 ++++++++-------- src/theory/sets/theory_sets_private.h | 39 ++++++++++-- 14 files changed, 135 insertions(+), 145 deletions(-) diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index 65df3a642..283c70ada 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -41,24 +41,26 @@ namespace CVC4 { namespace theory { namespace datatypes { -TheoryDatatypes::TheoryDatatypes(Context* c, UserContext* u, OutputChannel& out, - Valuation valuation, const LogicInfo& logicInfo) +TheoryDatatypes::TheoryDatatypes(Context* c, + UserContext* u, + OutputChannel& out, + Valuation valuation, + const LogicInfo& logicInfo) : Theory(THEORY_DATATYPES, c, u, out, valuation, logicInfo), - //d_cycle_check(c), - d_hasSeenCycle(c, false), d_infer(c), d_infer_exp(c), - d_term_sk( u ), - d_notify( *this ), + d_term_sk(u), + d_notify(*this), d_equalityEngine(d_notify, c, "theory::datatypes", true), - d_labels( c ), - d_selector_apps( c ), - //d_consEqc( c ), - d_conflict( c, false ), - d_collectTermsCache( c ), - d_functionTerms( c ), - d_singleton_eq( u ), - d_lemmas_produced_c( u ) + d_labels(c), + d_selector_apps(c), + d_conflict(c, false), + d_addedLemma(false), + d_addedFact(false), + d_collectTermsCache(c), + d_functionTerms(c), + d_singleton_eq(u), + d_lemmas_produced_c(u) { // The kinds we are treating as function application in congruence d_equalityEngine.addFunctionKind(kind::APPLY_CONSTRUCTOR); @@ -765,25 +767,6 @@ void TheoryDatatypes::conflict(TNode a, TNode b){ void TheoryDatatypes::eqNotifyNewClass(TNode t){ if( t.getKind()==APPLY_CONSTRUCTOR ){ getOrMakeEqcInfo( t, true ); - //look at all equivalence classes with constructor terms -/* - for( BoolMap::const_iterator it = d_consEqc.begin(); it != d_consEqc.end(); ++it ){ - if( (*it).second ){ - TNode r = (*it).first; - if( r.getType()==t.getType() ){ - EqcInfo * ei = getOrMakeEqcInfo( r, false ); - if( ei && !ei->d_constructor.get().isNull() && ei->d_constructor.get().getOperator()!=t.getOperator() ){ - Node deq = ei->d_constructor.get().eqNode( t ).negate(); - d_pending.push_back( deq ); - d_pending_exp[ deq ] = d_true; - Trace("datatypes-infer") << "DtInfer : diff constructor : " << deq << std::endl; - d_infer.push_back( deq ); - } - } - } - } -*/ - //d_consEqc[t] = true; } } @@ -865,14 +848,7 @@ void TheoryDatatypes::merge( Node t1, Node t2 ){ if( d_conflict ){ return; } - //d_consEqc[t1] = true; } - //AJR: do this? - //else if( cons2.isConst() ){ - // //prefer the constant - // eqc1->d_constructor = cons2; - //} - //d_consEqc[t2] = false; } }else{ Trace("datatypes-debug") << " no eqc info for " << t1 << ", must create" << std::endl; @@ -1998,9 +1974,6 @@ Node TheoryDatatypes::searchForCycle( TNode n, TNode on, for( unsigned i=0; i " << ncons[i] << "!!!!" << std::endl; - //} //add explanation for why the constructor is connected if( n != ncons ) { explainEquality( n, ncons, true, explanation ); diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h index e06bb7408..233ebd052 100644 --- a/src/theory/datatypes/theory_datatypes.h +++ b/src/theory/datatypes/theory_datatypes.h @@ -46,10 +46,6 @@ class TheoryDatatypes : public Theory { typedef context::CDHashMap BoolMap; typedef context::CDHashMap NodeMap; - /** transitive closure to record equivalence/subterm relation. */ - // TransitiveClosureNode d_cycle_check; - /** has seen cycle */ - context::CDO d_hasSeenCycle; /** inferences */ NodeList d_infer; NodeList d_infer_exp; @@ -179,12 +175,19 @@ private: /** selector apps for eqch equivalence class */ NodeIntMap d_selector_apps; std::map< Node, std::vector< Node > > d_selector_apps_data; - /** constructor terms */ - //BoolMap d_consEqc; /** Are we in conflict */ context::CDO d_conflict; - /** Added lemma ? */ + /** added lemma + * + * This flag is set to true during a full effort check if this theory + * called d_out->lemma(...). + */ bool d_addedLemma; + /** added fact + * + * This flag is set to true during a full effort check if this theory + * added an internal fact to its equality engine. + */ bool d_addedFact; /** The conflict node */ Node d_conflictNode; diff --git a/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp index 83098e3ba..3cf605238 100644 --- a/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp +++ b/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp @@ -57,7 +57,7 @@ class CegInstantiatorBvInverterQuery : public BvInverterQuery }; BvInstantiator::BvInstantiator(QuantifiersEngine* qe, TypeNode tn) - : Instantiator(qe, tn) + : Instantiator(qe, tn), d_inst_id_counter(0) { // get the global inverter utility // this must be global since we need to: diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cbqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cbqi.cpp index c281e81ca..ac76ee31f 100644 --- a/src/theory/quantifiers/cegqi/inst_strategy_cbqi.cpp +++ b/src/theory/quantifiers/cegqi/inst_strategy_cbqi.cpp @@ -38,11 +38,14 @@ using namespace CVC4::theory::arith; #define ARITH_INSTANTIATOR_USE_MINUS_DELTA -InstStrategyCbqi::InstStrategyCbqi( QuantifiersEngine * qe ) - : QuantifiersModule( qe ), d_added_cbqi_lemma( qe->getUserContext() ), -d_elim_quants( qe->getSatContext() ), -d_nested_qe_waitlist_size( qe->getUserContext() ), -d_nested_qe_waitlist_proc( qe->getUserContext() ) +InstStrategyCbqi::InstStrategyCbqi(QuantifiersEngine* qe) + : QuantifiersModule(qe), + d_cbqi_set_quant_inactive(false), + d_incomplete_check(false), + d_added_cbqi_lemma(qe->getUserContext()), + d_elim_quants(qe->getSatContext()), + d_nested_qe_waitlist_size(qe->getUserContext()), + d_nested_qe_waitlist_proc(qe->getUserContext()) //, d_added_inst( qe->getUserContext() ) { d_qid_count = 0; diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cbqi.h b/src/theory/quantifiers/cegqi/inst_strategy_cbqi.h index 236904ef2..4334652da 100644 --- a/src/theory/quantifiers/cegqi/inst_strategy_cbqi.h +++ b/src/theory/quantifiers/cegqi/inst_strategy_cbqi.h @@ -37,7 +37,18 @@ class InstStrategyCbqi : public QuantifiersModule { typedef context::CDHashMap< Node, int, NodeHashFunction> NodeIntMap; protected: + /** set quantified formula inactive + * + * This flag is set to true during a full effort check if at least one + * quantified formula is set "inactive", that is, its negation is + * unsatisfiable in the current context. + */ bool d_cbqi_set_quant_inactive; + /** incomplete check + * + * This is set to true during a full effort check if this strategy could + * not find an instantiation for at least one asserted quantified formula. + */ bool d_incomplete_check; /** whether we have added cbqi lemma */ NodeSet d_added_cbqi_lemma; diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp index e82ab617a..a1c132fda 100644 --- a/src/theory/quantifiers/conjecture_generator.cpp +++ b/src/theory/quantifiers/conjecture_generator.cpp @@ -80,16 +80,18 @@ void OpArgIndex::getGroundTerms( ConjectureGenerator * s, std::vector< TNode >& } } - - -ConjectureGenerator::ConjectureGenerator( QuantifiersEngine * qe, context::Context* c ) : QuantifiersModule( qe ), -d_notify( *this ), -d_uequalityEngine(d_notify, c, "ConjectureGenerator::ee", false), -d_ee_conjectures( c ){ - d_fullEffortCount = 0; - d_conj_count = 0; - d_subs_confirmCount = 0; - d_subs_unkCount = 0; +ConjectureGenerator::ConjectureGenerator(QuantifiersEngine* qe, + context::Context* c) + : QuantifiersModule(qe), + d_notify(*this), + d_uequalityEngine(d_notify, c, "ConjectureGenerator::ee", false), + d_ee_conjectures(c), + d_conj_count(0), + d_subs_confirmCount(0), + d_subs_unkCount(0), + d_fullEffortCount(0), + d_hasAddedLemma(false) +{ d_uequalityEngine.addFunctionKind( kind::APPLY_UF ); d_uequalityEngine.addFunctionKind( kind::APPLY_CONSTRUCTOR ); diff --git a/src/theory/quantifiers/conjecture_generator.h b/src/theory/quantifiers/conjecture_generator.h index 6d626038d..a3a0b8795 100644 --- a/src/theory/quantifiers/conjecture_generator.h +++ b/src/theory/quantifiers/conjecture_generator.h @@ -70,10 +70,19 @@ class TermGenEnv; class TermGenerator { -private: + private: unsigned calculateGeneralizationDepth( TermGenEnv * s, std::map< TypeNode, std::vector< int > >& fvs ); -public: - TermGenerator(){} + + public: + TermGenerator() + : d_id(0), + d_status(0), + d_status_num(0), + d_match_status(0), + d_match_status_child_num(0), + d_match_mode(0) + { + } TypeNode d_typ; unsigned d_id; //1 : consider as unique variable diff --git a/src/theory/quantifiers/ematching/candidate_generator.cpp b/src/theory/quantifiers/ematching/candidate_generator.cpp index 4208b11ae..6ea6e50b3 100644 --- a/src/theory/quantifiers/ematching/candidate_generator.cpp +++ b/src/theory/quantifiers/ematching/candidate_generator.cpp @@ -33,8 +33,9 @@ bool CandidateGenerator::isLegalCandidate( Node n ){ return d_qe->getTermDatabase()->isTermActive( n ) && ( !options::cbqi() || !quantifiers::TermUtil::hasInstConstAttr(n) ); } -CandidateGeneratorQE::CandidateGeneratorQE( QuantifiersEngine* qe, Node pat ) : -CandidateGenerator( qe ), d_term_iter( -1 ){ +CandidateGeneratorQE::CandidateGeneratorQE(QuantifiersEngine* qe, Node pat) + : CandidateGenerator(qe), d_term_iter(-1), d_term_iter_limit(0) +{ d_op = qe->getTermDatabase()->getMatchOperator( pat ); Assert( !d_op.isNull() ); } diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp index a8079f775..1e3116f43 100644 --- a/src/theory/quantifiers/first_order_model.cpp +++ b/src/theory/quantifiers/first_order_model.cpp @@ -572,10 +572,6 @@ void FirstOrderModelIG::resetEvaluate(){ d_eval_uf_use_default.clear(); d_eval_uf_model.clear(); d_eval_term_index_order.clear(); - d_eval_formulas = 0; - d_eval_uf_terms = 0; - d_eval_lits = 0; - d_eval_lits_unknown = 0; } //if evaluate( n ) = eVal, @@ -585,7 +581,6 @@ void FirstOrderModelIG::resetEvaluate(){ // if eVal is not 0, then // each n{ri->d_index[0]/x_0...ri->d_index[depIndex]/x_depIndex, */x_(depIndex+1) ... */x_n } is equivalent in the current model int FirstOrderModelIG::evaluate( Node n, int& depIndex, RepSetIterator* ri ){ - ++d_eval_formulas; Debug("fmf-eval-debug2") << "Evaluate " << n << std::endl; //Notice() << "Eval " << n << std::endl; if( n.getKind()==NOT ){ @@ -661,7 +656,6 @@ int FirstOrderModelIG::evaluate( Node n, int& depIndex, RepSetIterator* ri ){ }else if( n.getKind()==FORALL ){ return 0; }else{ - ++d_eval_lits; //Debug("fmf-eval-debug") << "Evaluate literal " << n << std::endl; int retVal = 0; depIndex = ri->getNumTerms()-1; @@ -684,7 +678,6 @@ int FirstOrderModelIG::evaluate( Node n, int& depIndex, RepSetIterator* ri ){ if( retVal!=0 ){ Debug("fmf-eval-debug") << "Evaluate literal: return " << retVal << ", depIndex = " << depIndex << std::endl; }else{ - ++d_eval_lits_unknown; Trace("fmf-eval-amb") << "Neither true nor false : " << n << std::endl; Trace("fmf-eval-amb") << " value : " << val << std::endl; } @@ -731,7 +724,6 @@ Node FirstOrderModelIG::evaluateTerm( Node n, int& depIndex, RepSetIterator* ri //Debug("fmf-eval-debug") << "Evaluate term " << n << " (" << gn << ")" << std::endl; //if it is a defined UF, then consult the interpretation if( d_uf_model_tree.find( op )!=d_uf_model_tree.end() ){ - ++d_eval_uf_terms; int argDepIndex = 0; //make the term model specifically for n makeEvalUfModel( n ); diff --git a/src/theory/quantifiers/first_order_model.h b/src/theory/quantifiers/first_order_model.h index 059250f8d..7da5b2088 100644 --- a/src/theory/quantifiers/first_order_model.h +++ b/src/theory/quantifiers/first_order_model.h @@ -266,12 +266,6 @@ public: /** evaluate functions */ int evaluate( Node n, int& depIndex, RepSetIterator* ri ); Node evaluateTerm( Node n, int& depIndex, RepSetIterator* ri ); -public: - //statistics - int d_eval_formulas; - int d_eval_uf_terms; - int d_eval_lits; - int d_eval_lits_unknown; private: //default evaluate term function Node evaluateTermDefault( Node n, int& depIndex, std::vector< int >& childDepIndex, RepSetIterator* ri ); diff --git a/src/theory/quantifiers/fmf/model_builder.cpp b/src/theory/quantifiers/fmf/model_builder.cpp index d1b7eebb8..c03fc7a32 100644 --- a/src/theory/quantifiers/fmf/model_builder.cpp +++ b/src/theory/quantifiers/fmf/model_builder.cpp @@ -457,24 +457,17 @@ bool QModelBuilderIG::hasConstantDefinition( Node n ){ return false; } -QModelBuilderIG::Statistics::Statistics(): - d_num_quants_init("QModelBuilderIG::Number_Quantifiers", 0), - d_num_partial_quants_init("QModelBuilderIG::Number_Partial_Quantifiers", 0), - d_init_inst_gen_lemmas("QModelBuilderIG::Initialize_Inst_Gen_Lemmas", 0 ), - d_inst_gen_lemmas("QModelBuilderIG::Inst_Gen_Lemmas", 0 ), - d_eval_formulas("QModelBuilderIG::Eval_Formulas", 0 ), - d_eval_uf_terms("QModelBuilderIG::Eval_Uf_Terms", 0 ), - d_eval_lits("QModelBuilderIG::Eval_Lits", 0 ), - d_eval_lits_unknown("QModelBuilderIG::Eval_Lits_Unknown", 0 ) +QModelBuilderIG::Statistics::Statistics() + : d_num_quants_init("QModelBuilderIG::Number_Quantifiers", 0), + d_num_partial_quants_init("QModelBuilderIG::Number_Partial_Quantifiers", + 0), + d_init_inst_gen_lemmas("QModelBuilderIG::Initialize_Inst_Gen_Lemmas", 0), + d_inst_gen_lemmas("QModelBuilderIG::Inst_Gen_Lemmas", 0) { smtStatisticsRegistry()->registerStat(&d_num_quants_init); smtStatisticsRegistry()->registerStat(&d_num_partial_quants_init); smtStatisticsRegistry()->registerStat(&d_init_inst_gen_lemmas); smtStatisticsRegistry()->registerStat(&d_inst_gen_lemmas); - smtStatisticsRegistry()->registerStat(&d_eval_formulas); - smtStatisticsRegistry()->registerStat(&d_eval_uf_terms); - smtStatisticsRegistry()->registerStat(&d_eval_lits); - smtStatisticsRegistry()->registerStat(&d_eval_lits_unknown); } QModelBuilderIG::Statistics::~Statistics(){ @@ -482,10 +475,6 @@ QModelBuilderIG::Statistics::~Statistics(){ smtStatisticsRegistry()->unregisterStat(&d_num_partial_quants_init); smtStatisticsRegistry()->unregisterStat(&d_init_inst_gen_lemmas); smtStatisticsRegistry()->unregisterStat(&d_inst_gen_lemmas); - smtStatisticsRegistry()->unregisterStat(&d_eval_formulas); - smtStatisticsRegistry()->unregisterStat(&d_eval_uf_terms); - smtStatisticsRegistry()->unregisterStat(&d_eval_lits); - smtStatisticsRegistry()->unregisterStat(&d_eval_lits_unknown); } //do exhaustive instantiation @@ -558,12 +547,6 @@ int QModelBuilderIG::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, in } } //print debugging information - if( fmig ){ - d_statistics.d_eval_formulas += fmig->d_eval_formulas; - d_statistics.d_eval_uf_terms += fmig->d_eval_uf_terms; - d_statistics.d_eval_lits += fmig->d_eval_lits; - d_statistics.d_eval_lits_unknown += fmig->d_eval_lits_unknown; - } Trace("inst-fmf-ei") << "For " << f << ", finished: " << std::endl; Trace("inst-fmf-ei") << " Inst Tried: " << d_triedLemmas << std::endl; Trace("inst-fmf-ei") << " Inst Added: " << d_addedLemmas << std::endl; diff --git a/src/theory/quantifiers/fmf/model_builder.h b/src/theory/quantifiers/fmf/model_builder.h index 353883a20..b34f1e580 100644 --- a/src/theory/quantifiers/fmf/model_builder.h +++ b/src/theory/quantifiers/fmf/model_builder.h @@ -148,10 +148,6 @@ class QModelBuilderIG : public QModelBuilder IntStat d_num_partial_quants_init; IntStat d_init_inst_gen_lemmas; IntStat d_inst_gen_lemmas; - IntStat d_eval_formulas; - IntStat d_eval_uf_terms; - IntStat d_eval_lits; - IntStat d_eval_lits_unknown; Statistics(); ~Statistics(); }; diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp index ab9fa6d54..317080ba6 100644 --- a/src/theory/sets/theory_sets_private.cpp +++ b/src/theory/sets/theory_sets_private.cpp @@ -37,25 +37,28 @@ namespace sets { TheorySetsPrivate::TheorySetsPrivate(TheorySets& external, context::Context* c, - context::UserContext* u): - d_rels(NULL), - d_members(c), - d_deq(c), - d_deq_processed(u), - d_keep(c), - d_proxy(u), - d_proxy_to_term(u), - d_lemmas_produced(u), - d_card_processed(u), - d_var_elim(u), - d_external(external), - d_notify(*this), - d_equalityEngine(d_notify, c, "theory::sets::ee", true), - d_conflict(c) + context::UserContext* u) + : d_members(c), + d_deq(c), + d_deq_processed(u), + d_keep(c), + d_sentLemma(false), + d_addedFact(false), + d_full_check_incomplete(false), + d_proxy(u), + d_proxy_to_term(u), + d_lemmas_produced(u), + d_card_enabled(false), + d_card_processed(u), + d_var_elim(u), + d_external(external), + d_notify(*this), + d_equalityEngine(d_notify, c, "theory::sets::ee", true), + d_conflict(c), + d_rels( + new TheorySetsRels(c, u, &d_equalityEngine, &d_conflict, external)), + d_rels_enabled(false) { - - d_rels = new TheorySetsRels(c, u, &d_equalityEngine, &d_conflict, external); - d_true = NodeManager::currentNM()->mkConst( true ); d_false = NodeManager::currentNM()->mkConst( false ); d_zero = NodeManager::currentNM()->mkConst( Rational(0) ); @@ -68,21 +71,14 @@ TheorySetsPrivate::TheorySetsPrivate(TheorySets& external, d_equalityEngine.addFunctionKind(kind::MEMBER); d_equalityEngine.addFunctionKind(kind::SUBSET); - // If cardinality is on. d_equalityEngine.addFunctionKind(kind::CARD); - - d_card_enabled = false; - d_rels_enabled = false; - -}/* TheorySetsPrivate::TheorySetsPrivate() */ +} TheorySetsPrivate::~TheorySetsPrivate(){ - delete d_rels; for (std::pair& current_pair : d_eqc_info) { delete current_pair.second; } -}/* TheorySetsPrivate::~TheorySetsPrivate() */ - +} void TheorySetsPrivate::eqNotifyNewClass(TNode t) { if( t.getKind()==kind::SINGLETON || t.getKind()==kind::EMPTYSET ){ diff --git a/src/theory/sets/theory_sets_private.h b/src/theory/sets/theory_sets_private.h index 31aec85c3..d36e0ddb1 100644 --- a/src/theory/sets/theory_sets_private.h +++ b/src/theory/sets/theory_sets_private.h @@ -46,8 +46,6 @@ class TheorySetsPrivate { typedef context::CDHashMap< Node, int, NodeHashFunction> NodeIntMap; typedef context::CDHashSet NodeSet; typedef context::CDHashMap< Node, Node, NodeHashFunction > NodeMap; -private: - TheorySetsRels * d_rels; public: void eqNotifyNewClass(TNode t); void eqNotifyPreMerge(TNode t1, TNode t2); @@ -113,9 +111,25 @@ private: void addEqualityToExp( Node a, Node b, std::vector< Node >& exp ); void debugPrintSet( Node s, const char * c ); - + + /** sent lemma + * + * This flag is set to true during a full effort check if this theory + * called d_out->lemma(...). + */ bool d_sentLemma; + /** added fact + * + * This flag is set to true during a full effort check if this theory + * added an internal fact to its equality engine. + */ bool d_addedFact; + /** full check incomplete + * + * This flag is set to true during a full effort check if this theory + * is incomplete for some reason (for instance, if we combine cardinality + * with a relation or extended function kind). + */ bool d_full_check_incomplete; NodeMap d_proxy; NodeMap d_proxy_to_term; @@ -139,11 +153,15 @@ private: std::map< Kind, std::map< Node, std::map< Node, Node > > > d_bop_index; std::map< Kind, std::vector< Node > > d_op_list; //cardinality -private: + private: + /** is cardinality enabled? + * + * This flag is set to true during a full effort check if any constraint + * involving cardinality constraints is asserted to this theory. + */ bool d_card_enabled; /** element types of sets for which cardinality is enabled */ std::map d_t_card_enabled; - bool d_rels_enabled; std::map< Node, Node > d_eqc_to_card_term; NodeSet d_card_processed; std::map< Node, std::vector< Node > > d_card_parent; @@ -300,7 +318,16 @@ private: bool isCareArg( Node n, unsigned a ); public: bool isEntailed( Node n, bool pol ); - + + private: + /** subtheory solver for the theory of relations */ + std::unique_ptr d_rels; + /** are relations enabled? + * + * This flag is set to true during a full effort check if any constraint + * involving relational constraints is asserted to this theory. + */ + bool d_rels_enabled; };/* class TheorySetsPrivate */ -- 2.30.2