From 6f95e3c711d39b531eb0a8ac0e098c89a5737ce2 Mon Sep 17 00:00:00 2001 From: Tim King Date: Sat, 18 Nov 2017 16:27:46 -0800 Subject: [PATCH] Names the Effort enum of QuantConflictFind class. (#1354) * Changes the Effort level of QuantConflictFind to an enum class. Adding a third value to the enum to indicate not being set. Minor refactoring related to this change. Resolves CID 1172043. * Fixing a missed assertion. Fixing a few compiler warnings. * Switching back to an enum from an enum class. --- .../quantifiers/quant_conflict_find.cpp | 98 ++++++++++++------- src/theory/quantifiers/quant_conflict_find.h | 29 ++++-- src/theory/quantifiers/quantifiers_rewriter.h | 2 +- src/theory/quantifiers/rewrite_engine.cpp | 2 +- src/theory/quantifiers/sygus_process_conj.cpp | 2 +- src/theory/quantifiers/sygus_process_conj.h | 3 +- 6 files changed, 90 insertions(+), 46 deletions(-) diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp index baf499d67..442e3b230 100644 --- a/src/theory/quantifiers/quant_conflict_find.cpp +++ b/src/theory/quantifiers/quant_conflict_find.cpp @@ -560,7 +560,7 @@ bool QuantInfo::isMatchSpurious( QuantConflictFind * p ) { for( int i=0; i::iterator it = d_match.find( i ); if( !d_match[i].isNull() ){ - if( !getCurrentCanBeEqual( p, i, d_match[i], p->d_effort==QuantConflictFind::effort_conflict ) ){ + if (!getCurrentCanBeEqual(p, i, d_match[i], p->atConflictEffort())) { return true; } } @@ -571,7 +571,7 @@ bool QuantInfo::isMatchSpurious( QuantConflictFind * p ) { bool QuantInfo::isTConstraintSpurious( QuantConflictFind * p, std::vector< Node >& terms ) { if( options::qcfEagerTest() ){ //check whether the instantiation evaluates as expected - if( p->d_effort==QuantConflictFind::effort_conflict ){ + if (p->atConflictEffort()) { Trace("qcf-instance-check") << "Possible conflict instance for " << d_q << " : " << std::endl; std::map< TNode, TNode > subs; for( unsigned i=0; igetTermUtil()->substituteBoundVariables(it->first, d_q, terms); cons = it->second ? cons : cons.negate(); - if( !entailmentTest( p, cons, p->d_effort==QuantConflictFind::effort_conflict ) ){ + if (!entailmentTest(p, cons, p->atConflictEffort())) { return true; } } @@ -721,7 +721,7 @@ bool QuantInfo::completeMatch( QuantConflictFind * p, std::vector< int >& assign if( slv_v==-1 ){ Trace("qcf-tconstraint-debug") << "...will solve for var #" << vn << std::endl; slv_v = vn; - if( p->d_effort!=QuantConflictFind::effort_conflict ){ + if (!p->atConflictEffort()) { break; } }else{ @@ -758,7 +758,7 @@ bool QuantInfo::completeMatch( QuantConflictFind * p, std::vector< int >& assign if( v==d_vars[index] ){ sum = lhs; }else{ - if( p->d_effort==QuantConflictFind::effort_conflict ){ + if (p->atConflictEffort()) { Kind kn = k; if( d_vars[index].getKind()==PLUS ){ kn = MINUS; @@ -1334,7 +1334,7 @@ void MatchGen::reset( QuantConflictFind * p, bool tgt, QuantInfo * qi ) { if( d_tgt ){ success = p->areMatchEqual( nn[0], nn[1] ); }else{ - if( p->d_effort==QuantConflictFind::effort_conflict ){ + if (p->atConflictEffort()) { success = p->areDisequal( nn[0], nn[1] ); }else{ success = p->areMatchDisequal( nn[0], nn[1] ); @@ -1377,7 +1377,8 @@ void MatchGen::reset( QuantConflictFind * p, bool tgt, QuantInfo * qi ) { }else{ if( d_tgt && d_n.getKind()==FORALL ){ //fail - }else if( d_n.getKind()==FORALL && p->d_effort==QuantConflictFind::effort_conflict && !options::qcfNestedConflict() ){ + } else if (d_n.getKind() == FORALL && p->atConflictEffort() && + !options::qcfNestedConflict()) { //fail }else{ //reset the first child to d_tgt @@ -1898,14 +1899,13 @@ bool MatchGen::isHandled( TNode n ) { return true; } - -QuantConflictFind::QuantConflictFind( QuantifiersEngine * qe, context::Context* c ) : -QuantifiersModule( qe ), -d_conflict( c, false ) { - d_fid_count = 0; - d_true = NodeManager::currentNM()->mkConst(true); - d_false = NodeManager::currentNM()->mkConst(false); -} +QuantConflictFind::QuantConflictFind(QuantifiersEngine* qe, context::Context* c) + : QuantifiersModule(qe), + d_conflict(c, false), + d_true(NodeManager::currentNM()->mkConst(true)), + d_false(NodeManager::currentNM()->mkConst(false)), + d_effort(EFFORT_INVALID), + d_needs_computeRelEqr() {} Node QuantConflictFind::mkEqNode( Node a, Node b ) { return a.eqNode( b ); @@ -1945,16 +1945,6 @@ void QuantConflictFind::registerQuantifier( Node q ) { } } -short QuantConflictFind::getMaxQcfEffort() { - if( options::qcfMode()==QCF_CONFLICT_ONLY ){ - return effort_conflict; - }else if( options::qcfMode()==QCF_PROP_EQ || options::qcfMode()==QCF_PARTIAL ){ - return effort_prop_eq; - }else{ - return 0; - } -} - bool QuantConflictFind::areMatchEqual( TNode n1, TNode n2 ) { //if( d_effort==QuantConflictFind::effort_mc ){ // return n1==n2 || !areDisequal( n1, n2 ); @@ -1964,7 +1954,7 @@ bool QuantConflictFind::areMatchEqual( TNode n1, TNode n2 ) { } bool QuantConflictFind::areMatchDisequal( TNode n1, TNode n2 ) { - //if( d_effort==QuantConflictFind::effort_conflict ){ + // if( d_effort==QuantConflictFind::Effort::Conflict ){ // return areDisequal( n1, n2 ); //}else{ return n1!=n2; @@ -2030,6 +2020,29 @@ void QuantConflictFind::setIrrelevantFunction( TNode f ) { } } +namespace { + +// Returns the beginning of a range of efforts. The range can be iterated +// through as unsigned using operator++. +inline QuantConflictFind::Effort QcfEffortStart() { + return QuantConflictFind::EFFORT_CONFLICT; +} + +// Returns the beginning of a range of efforts. The value returned is included +// in the range. +inline QuantConflictFind::Effort QcfEffortEnd() { + switch (options::qcfMode()) { + case QCF_PROP_EQ: + case QCF_PARTIAL: + return QuantConflictFind::EFFORT_PROP_EQ; + case QCF_CONFLICT_ONLY: + default: + return QuantConflictFind::EFFORT_PROP_EQ; + } +} + +} // namespace + /** check */ void QuantConflictFind::check(Theory::Effort level, QEffort quant_e) { @@ -2063,10 +2076,9 @@ void QuantConflictFind::check(Theory::Effort level, QEffort quant_e) debugPrint("qcf-debug"); Trace("qcf-debug") << std::endl; } - short end_e = getMaxQcfEffort(); bool isConflict = false; - for( short e = effort_conflict; e<=end_e; e++ ){ - d_effort = e; + for (unsigned e = QcfEffortStart(), end = QcfEffortEnd(); e <= end; ++e) { + d_effort = static_cast(e); Trace("qcf-check") << "Checking quantified formulas at effort " << e << "..." << std::endl; for( unsigned i=0; igetModel()->getNumAssertedQuantifiers(); i++ ){ Node q = d_quantEngine->getModel()->getAssertedQuantifier( i, true ); @@ -2104,7 +2116,8 @@ void QuantConflictFind::check(Theory::Effort level, QEffort quant_e) Node inst = d_quantEngine->getInstantiation( q, terms ); Debug("qcf-check-inst") << "Check instantiation " << inst << "..." << std::endl; Assert( !getTermDatabase()->isEntailed( inst, true ) ); - Assert( getTermDatabase()->isEntailed( inst, false ) || e>effort_conflict ); + Assert(getTermDatabase()->isEntailed(inst, false) || + e > EFFORT_CONFLICT); } if( d_quantEngine->addInstantiation( q, terms ) ){ Trace("qcf-check") << " ... Added instantiation" << std::endl; @@ -2112,7 +2125,7 @@ void QuantConflictFind::check(Theory::Effort level, QEffort quant_e) qi->debugPrintMatch("qcf-inst"); Trace("qcf-inst") << std::endl; ++addedLemmas; - if( e==effort_conflict ){ + if (e == EFFORT_CONFLICT) { d_quantEngine->markRelevant( q ); ++(d_quantEngine->d_statistics.d_instantiations_qcf); if( options::qcfAllConflict() ){ @@ -2121,7 +2134,7 @@ void QuantConflictFind::check(Theory::Effort level, QEffort quant_e) d_conflict.set( true ); } break; - }else if( e==effort_prop_eq ){ + } else if (e == EFFORT_PROP_EQ) { d_quantEngine->markRelevant( q ); ++(d_quantEngine->d_statistics.d_instantiations_qcf); } @@ -2164,7 +2177,11 @@ void QuantConflictFind::check(Theory::Effort level, QEffort quant_e) double clSet2 = double(clock())/double(CLOCKS_PER_SEC); Trace("qcf-engine") << "Finished conflict find engine, time = " << (clSet2-clSet); if( addedLemmas>0 ){ - Trace("qcf-engine") << ", effort = " << ( d_effort==effort_conflict ? "conflict" : ( d_effort==effort_prop_eq ? "prop_eq" : "mc" ) ); + Trace("qcf-engine") + << ", effort = " + << (d_effort == EFFORT_CONFLICT + ? "conflict" + : (d_effort == EFFORT_PROP_EQ ? "prop_eq" : "mc")); Trace("qcf-engine") << ", addedLemmas = " << addedLemmas; } Trace("qcf-engine") << std::endl; @@ -2276,6 +2293,21 @@ TNode QuantConflictFind::getZero( Kind k ) { } } +std::ostream& operator<<(std::ostream& os, const QuantConflictFind::Effort& e) { + switch (e) { + case QuantConflictFind::EFFORT_INVALID: + os << "Invalid"; + break; + case QuantConflictFind::EFFORT_CONFLICT: + os << "Conflict"; + break; + case QuantConflictFind::EFFORT_PROP_EQ: + os << "PropEq"; + break; + } + return os; +} + } /* namespace CVC4::theory::quantifiers */ } /* namespace CVC4::theory */ } /* namespace CVC4 */ diff --git a/src/theory/quantifiers/quant_conflict_find.h b/src/theory/quantifiers/quant_conflict_find.h index 0e5fe3c18..8a1043ded 100644 --- a/src/theory/quantifiers/quant_conflict_find.h +++ b/src/theory/quantifiers/quant_conflict_find.h @@ -17,6 +17,9 @@ #ifndef QUANT_CONFLICT_FIND #define QUANT_CONFLICT_FIND +#include +#include + #include "context/cdhashmap.h" #include "context/cdchunk_list.h" #include "theory/quantifiers_engine.h" @@ -202,7 +205,6 @@ private: void setIrrelevantFunction( TNode f ); private: std::map< Node, Node > d_op_node; - int d_fid_count; std::map< Node, int > d_fid; Node mkEqNode( Node a, Node b ); public: //for ground terms @@ -214,14 +216,23 @@ private: private: //for equivalence classes // type -> list(eqc) std::map< TypeNode, std::vector< TNode > > d_eqcs; -public: - enum { - effort_conflict, - effort_prop_eq, + + public: + enum Effort : unsigned { + EFFORT_CONFLICT, + EFFORT_PROP_EQ, + EFFORT_INVALID, }; - short d_effort; - void setEffort( int e ) { d_effort = e; } - static short getMaxQcfEffort(); + void setEffort(Effort e) { d_effort = e; } + + inline bool atConflictEffort() const { + return d_effort == QuantConflictFind::EFFORT_CONFLICT; + } + + private: + Effort d_effort; + + public: bool areMatchEqual( TNode n1, TNode n2 ); bool areMatchDisequal( TNode n1, TNode n2 ); public: @@ -270,6 +281,8 @@ public: std::string identify() const { return "QcfEngine"; } }; +std::ostream& operator<<(std::ostream& os, const QuantConflictFind::Effort& e); + } /* namespace CVC4::theory::quantifiers */ } /* namespace CVC4::theory */ } /* namespace CVC4 */ diff --git a/src/theory/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h index d1f819726..b179110e7 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.h +++ b/src/theory/quantifiers/quantifiers_rewriter.h @@ -26,7 +26,7 @@ namespace CVC4 { namespace theory { namespace quantifiers { -class QAttributes; +struct QAttributes; class QuantifiersRewriter { private: diff --git a/src/theory/quantifiers/rewrite_engine.cpp b/src/theory/quantifiers/rewrite_engine.cpp index 2c85bceb8..337d61976 100644 --- a/src/theory/quantifiers/rewrite_engine.cpp +++ b/src/theory/quantifiers/rewrite_engine.cpp @@ -119,7 +119,7 @@ int RewriteEngine::checkRewriteRule( Node f, Theory::Effort e ) { if( qcf ){ //reset QCF module qcf->computeRelevantEqr(); - qcf->setEffort( QuantConflictFind::effort_conflict ); + qcf->setEffort(QuantConflictFind::EFFORT_CONFLICT); //get the proper quantifiers info std::map< Node, QuantInfo >::iterator it = d_qinfo.find( f ); if( it!=d_qinfo.end() ){ diff --git a/src/theory/quantifiers/sygus_process_conj.cpp b/src/theory/quantifiers/sygus_process_conj.cpp index 06ce99007..4c0e992e0 100644 --- a/src/theory/quantifiers/sygus_process_conj.cpp +++ b/src/theory/quantifiers/sygus_process_conj.cpp @@ -519,7 +519,7 @@ void CegConjectureProcessFun::getIrrelevantArgs( } } -CegConjectureProcess::CegConjectureProcess(QuantifiersEngine* qe) : d_qe(qe) {} +CegConjectureProcess::CegConjectureProcess(QuantifiersEngine* qe) {} CegConjectureProcess::~CegConjectureProcess() {} Node CegConjectureProcess::preSimplify(Node q) { diff --git a/src/theory/quantifiers/sygus_process_conj.h b/src/theory/quantifiers/sygus_process_conj.h index f5966c55f..0b9a25532 100644 --- a/src/theory/quantifiers/sygus_process_conj.h +++ b/src/theory/quantifiers/sygus_process_conj.h @@ -353,8 +353,7 @@ class CegConjectureProcess NodeHashFunction>& free_vars); /** for each synth-fun, information that is specific to this conjecture */ std::map d_sf_info; - /** reference to quantifier engine */ - QuantifiersEngine* d_qe; + /** get component vector */ void getComponentVector(Kind k, Node n, std::vector& args); }; -- 2.30.2