From 44355002ddea45c8b1abd5b20437b7940c90e6fc Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 6 Sep 2018 15:48:58 -0500 Subject: [PATCH] Further simplify and fix initialization of ce guided instantiation (#2437) --- .../sygus/ce_guided_conjecture.cpp | 3 +- .../quantifiers/sygus/ce_guided_conjecture.h | 2 +- .../sygus/ce_guided_instantiation.cpp | 64 +++++++++++-------- .../sygus/ce_guided_instantiation.h | 5 +- 4 files changed, 43 insertions(+), 31 deletions(-) diff --git a/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp b/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp index 1d070417e..0a212598b 100644 --- a/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp +++ b/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp @@ -202,7 +202,8 @@ bool CegConjecture::isSingleInvocation() const { return d_ceg_si->isSingleInvocation(); } -bool CegConjecture::needsCheck( std::vector< Node >& lem ) { +bool CegConjecture::needsCheck() +{ if( isSingleInvocation() && !d_ceg_si->needsCheck() ){ return false; } diff --git a/src/theory/quantifiers/sygus/ce_guided_conjecture.h b/src/theory/quantifiers/sygus/ce_guided_conjecture.h index 48d307f1e..612a2b4ce 100644 --- a/src/theory/quantifiers/sygus/ce_guided_conjecture.h +++ b/src/theory/quantifiers/sygus/ce_guided_conjecture.h @@ -58,7 +58,7 @@ public: * refinement */ void incrementRefineCount() { d_refine_count++; } /** whether the conjecture is waiting for a call to doCheck below */ - bool needsCheck( std::vector< Node >& lem ); + bool needsCheck(); /** whether the conjecture is waiting for a call to doRefine below */ bool needsRefinement() const; /** do single invocation check diff --git a/src/theory/quantifiers/sygus/ce_guided_instantiation.cpp b/src/theory/quantifiers/sygus/ce_guided_instantiation.cpp index 83a576d37..c59195746 100644 --- a/src/theory/quantifiers/sygus/ce_guided_instantiation.cpp +++ b/src/theory/quantifiers/sygus/ce_guided_instantiation.cpp @@ -52,10 +52,20 @@ QuantifiersModule::QEffort CegInstantiation::needsModel(Theory::Effort e) void CegInstantiation::check(Theory::Effort e, QEffort quant_e) { + // are we at the proper effort level? + unsigned echeck = + d_conj->isSingleInvocation() ? QEFFORT_STANDARD : QEFFORT_MODEL; + if (quant_e != echeck) + { + return; + } + // if we are waiting to assign the conjecture, do it now if (!d_waiting_conj.isNull()) { Node q = d_waiting_conj; + Trace("cegqi-engine") << "--- Conjecture waiting to assign: " << q + << std::endl; d_waiting_conj = Node::null(); if (!d_conj->isAssigned()) { @@ -65,31 +75,29 @@ void CegInstantiation::check(Theory::Effort e, QEffort quant_e) return; } } - unsigned echeck = - d_conj->isSingleInvocation() ? QEFFORT_STANDARD : QEFFORT_MODEL; - if( quant_e==echeck ){ - Trace("cegqi-engine") << "---Counterexample Guided Instantiation Engine---" << std::endl; - Trace("cegqi-engine-debug") << std::endl; - bool active = false; - bool value; - if( d_quantEngine->getValuation().hasSatValue( d_conj->getConjecture(), value ) ) { - active = value; - }else{ - Trace("cegqi-engine-debug") << "...no value for quantified formula." << std::endl; - } - Trace("cegqi-engine-debug") << "Current conjecture status : active : " << active << std::endl; - std::vector< Node > lem; - if( active && d_conj->needsCheck( lem ) ){ - checkCegConjecture( d_conj ); - }else{ - Trace("cegqi-engine-debug") << "...does not need check." << std::endl; - for( unsigned i=0; iaddLemma( lem[i] ); - } - } - Trace("cegqi-engine") << "Finished Counterexample Guided Instantiation engine." << std::endl; + + Trace("cegqi-engine") << "---Counterexample Guided Instantiation Engine---" + << std::endl; + Trace("cegqi-engine-debug") << std::endl; + bool active = false; + bool value; + if (d_quantEngine->getValuation().hasSatValue(d_conj->getConjecture(), value)) + { + active = value; + } + else + { + Trace("cegqi-engine-debug") + << "...no value for quantified formula." << std::endl; } + Trace("cegqi-engine-debug") + << "Current conjecture status : active : " << active << std::endl; + if (active && d_conj->needsCheck()) + { + checkConjecture(d_conj); + } + Trace("cegqi-engine") + << "Finished Counterexample Guided Instantiation engine." << std::endl; } bool CegInstantiation::assignConjecture(Node q) @@ -98,6 +106,7 @@ bool CegInstantiation::assignConjecture(Node q) { return false; } + Trace("cegqi-engine") << "--- Assign conjecture " << q << std::endl; if (options::sygusQePreproc()) { // the following does quantifier elimination as a preprocess step @@ -236,7 +245,7 @@ void CegInstantiation::registerQuantifier(Node q) else { // assign it now - d_conj->assign(q); + assignConjecture(q); } }else{ Assert( d_conj->getEmbeddedConjecture()==q ); @@ -257,7 +266,8 @@ Node CegInstantiation::getNextDecisionRequest( unsigned& priority ) { return Node::null(); } -void CegInstantiation::checkCegConjecture( CegConjecture * conj ) { +void CegInstantiation::checkConjecture(CegConjecture* conj) +{ Node q = conj->getEmbeddedConjecture(); Node aq = conj->getConjecture(); if( Trace.isOn("cegqi-engine-debug") ){ @@ -322,7 +332,7 @@ void CegInstantiation::checkCegConjecture( CegConjecture * conj ) { if (conj->needsRefinement()) { // immediately go to refine candidate - checkCegConjecture(conj); + checkConjecture(conj); return; } } diff --git a/src/theory/quantifiers/sygus/ce_guided_instantiation.h b/src/theory/quantifiers/sygus/ce_guided_instantiation.h index 03b4c4cc1..9c81b6978 100644 --- a/src/theory/quantifiers/sygus/ce_guided_instantiation.h +++ b/src/theory/quantifiers/sygus/ce_guided_instantiation.h @@ -48,8 +48,9 @@ private: */ bool assignConjecture(Node q); /** check conjecture */ - void checkCegConjecture( CegConjecture * conj ); -public: + void checkConjecture(CegConjecture* conj); + + public: CegInstantiation( QuantifiersEngine * qe, context::Context* c ); ~CegInstantiation(); public: -- 2.30.2