From: ajreynol Date: Thu, 29 Jan 2015 12:08:31 +0000 (+0100) Subject: Restrict LtePartialInst instantiations based on E-matching, promote to quantifiers... X-Git-Tag: cvc5-1.0.0~6416 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=51d642e075466bc6655cae9752350f6760b2bd0f;p=cvc5.git Restrict LtePartialInst instantiations based on E-matching, promote to quantifiers module. Refactor QuantifiersEngine registration and check. --- diff --git a/src/Makefile.am b/src/Makefile.am index c72e11809..184ef5d56 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -327,6 +327,8 @@ libcvc4_la_SOURCES = \ theory/quantifiers/conjecture_generator.cpp \ theory/quantifiers/ce_guided_instantiation.h \ theory/quantifiers/ce_guided_instantiation.cpp \ + theory/quantifiers/local_theory_ext.h \ + theory/quantifiers/local_theory_ext.cpp \ theory/quantifiers/fun_def_process.h \ theory/quantifiers/fun_def_process.cpp \ theory/quantifiers/options_handlers.h \ diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp index d4f32becc..eef354e75 100644 --- a/src/theory/quantifiers/first_order_model.cpp +++ b/src/theory/quantifiers/first_order_model.cpp @@ -36,14 +36,21 @@ d_qe( qe ), d_axiom_asserted( c, false ), d_forall_asserts( c ), d_isModelSet( c } -void FirstOrderModel::assertQuantifier( Node n ){ - if( n.getKind()==FORALL ){ - d_forall_asserts.push_back( n ); - if( n.getAttribute(AxiomAttribute()) ){ - d_axiom_asserted = true; +void FirstOrderModel::assertQuantifier( Node n, bool reduced ){ + if( !reduced ){ + if( n.getKind()==FORALL ){ + d_forall_asserts.push_back( n ); + if( n.getAttribute(AxiomAttribute()) ){ + d_axiom_asserted = true; + } + }else if( n.getKind()==NOT ){ + Assert( n[0].getKind()==FORALL ); } - }else if( n.getKind()==NOT ){ - Assert( n[0].getKind()==FORALL ); + }else{ + Assert( n.getKind()==FORALL ); + Assert( d_forall_to_reduce.find( n )==d_forall_to_reduce.end() ); + d_forall_to_reduce[n] = true; + Trace("quant") << "Mark to reduce : " << n << std::endl; } } @@ -112,6 +119,18 @@ Node FirstOrderModel::getSomeDomainElement(TypeNode tn){ return d_rep_set.d_type_reps[tn][0]; } +/** needs check */ +bool FirstOrderModel::checkNeeded() { + return d_forall_asserts.size()>0 || !d_forall_to_reduce.empty(); +} + +/** mark reduced */ +void FirstOrderModel::markQuantifierReduced( Node q ) { + Assert( d_forall_to_reduce.find( q )!=d_forall_to_reduce.end() ); + d_forall_to_reduce.erase( q ); + Trace("quant") << "Mark reduced : " << q << std::endl; +} + void FirstOrderModel::reset_round() { d_quant_active.clear(); } diff --git a/src/theory/quantifiers/first_order_model.h b/src/theory/quantifiers/first_order_model.h index 77ccad247..c2cd88e17 100644 --- a/src/theory/quantifiers/first_order_model.h +++ b/src/theory/quantifiers/first_order_model.h @@ -51,6 +51,8 @@ protected: context::CDO< bool > d_axiom_asserted; /** list of quantifiers asserted in the current context */ context::CDList d_forall_asserts; + /** list of quantifiers that have been marked to reduce */ + std::map< Node, bool > d_forall_to_reduce; /** is model set */ context::CDO< bool > d_isModelSet; /** get variable id */ @@ -59,11 +61,13 @@ protected: virtual Node getCurrentUfModelValue( Node n, std::vector< Node > & args, bool partial ) = 0; public: //for Theory Quantifiers: /** assert quantifier */ - void assertQuantifier( Node n ); + void assertQuantifier( Node n, bool reduced = false ); /** get number of asserted quantifiers */ int getNumAssertedQuantifiers() { return (int)d_forall_asserts.size(); } /** get asserted quantifier */ Node getAssertedQuantifier( int i ) { return d_forall_asserts[i]; } + /** get number to reduce quantifiers */ + unsigned getNumToReduceQuantifiers() { return d_forall_to_reduce.size(); } /** bool axiom asserted */ bool isAxiomAsserted() { return d_axiom_asserted; } /** initialize model for term */ @@ -92,6 +96,10 @@ public: } /** get some domain element */ Node getSomeDomainElement(TypeNode tn); + /** do we need to do any work? */ + bool checkNeeded(); + /** mark reduced */ + void markQuantifierReduced( Node q ); private: //list of inactive quantified formulas std::map< TNode, bool > d_quant_active; diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp index 6a2bd5e2e..f378b4913 100644 --- a/src/theory/quantifiers/inst_strategy_cbqi.cpp +++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp @@ -19,6 +19,7 @@ #include "theory/theory_engine.h" #include "theory/quantifiers/options.h" #include "theory/quantifiers/term_database.h" +#include "theory/quantifiers/first_order_model.h" using namespace std; using namespace CVC4; @@ -255,9 +256,9 @@ void InstStrategySimplex::debugPrint( const char* c ){ //} } Debug(c) << std::endl; - - for( int q=0; qgetNumQuantifiers(); q++ ){ - Node f = d_quantEngine->getQuantifier( q ); + + for( int i=0; i<(int)d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){ + Node f = d_quantEngine->getModel()->getAssertedQuantifier( i ); Debug(c) << f << std::endl; Debug(c) << " Inst constants: "; for( int i=0; i<(int)d_quantEngine->getTermDatabase()->getNumInstantiationConstants( f ); i++ ){ diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp index b53919aaf..518921433 100644 --- a/src/theory/quantifiers/instantiation_engine.cpp +++ b/src/theory/quantifiers/instantiation_engine.cpp @@ -64,11 +64,11 @@ void InstantiationEngine::finishInit(){ d_instStrategies.push_back( d_i_ag ); } - //local theory extensions - if( options::localTheoryExt() ){ - d_i_lte = new InstStrategyLocalTheoryExt( d_quantEngine ); - d_instStrategies.push_back( d_i_lte ); - } + //local theory extensions TODO? + //if( options::localTheoryExt() ){ + // d_i_lte = new InstStrategyLocalTheoryExt( d_quantEngine ); + // d_instStrategies.push_back( d_i_lte ); + //} //full saturation : instantiate from relevant domain, then arbitrary terms if( options::fullSaturateQuant() ){ diff --git a/src/theory/quantifiers/local_theory_ext.cpp b/src/theory/quantifiers/local_theory_ext.cpp new file mode 100644 index 000000000..d62fa02c2 --- /dev/null +++ b/src/theory/quantifiers/local_theory_ext.cpp @@ -0,0 +1,249 @@ +/********************* */ +/*! \file quant_util.cpp + ** \verbatim + ** Original author: Andrew Reynolds + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2014 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Implementation of local theory ext utilities + **/ + +#include "theory/quantifiers/local_theory_ext.h" +#include "theory/quantifiers/term_database.h" +#include "theory/quantifiers_engine.h" +#include "theory/quantifiers/first_order_model.h" + +using namespace std; +using namespace CVC4; +using namespace CVC4::kind; +using namespace CVC4::context; +using namespace CVC4::theory; +using namespace CVC4::theory::quantifiers; + + +LtePartialInst::LtePartialInst( QuantifiersEngine * qe, context::Context* c ) : +QuantifiersModule( qe ), d_wasInvoked( false ), d_needsCheck( false ){ + +} + +/** add quantifier */ +bool LtePartialInst::addQuantifier( Node q ) { + if( d_do_inst.find( q )!=d_do_inst.end() ){ + if( d_do_inst[q] ){ + d_lte_asserts.push_back( q ); + return true; + }else{ + return false; + } + }else{ + d_vars[q].clear(); + d_pat_var_order[q].clear(); + //check if this quantified formula is eligible for partial instantiation + std::map< Node, bool > vars; + for( unsigned i=0; i var_order; + bool doInst = true; + for( unsigned i=0; i& pat_var_order, std::map< Node, int >& var_order ) { + std::map< Node, int >::iterator it = var_order.find( v ); + if( it==var_order.end() ){ + return false; + }else if( std::find( pat_var_order.begin(), pat_var_order.end(), it->second )!=pat_var_order.end() ){ + return false; + }else{ + pat_var_order.push_back( it->second ); + return true; + } +} + +void LtePartialInst::getEligibleInstVars( Node n, std::map< Node, bool >& vars ) { + if( n.getKind()!=APPLY_UF || n.getType().isBoolean() ){ + for( unsigned i=0; i=Theory::EFFORT_FULL && d_needsCheck; +} +/* Call during quantifier engine's check */ +void LtePartialInst::check( Theory::Effort e, unsigned quant_e ) { + //flush lemmas ASAP (they are a reduction) + if( quant_e==QuantifiersEngine::QEFFORT_CONFLICT && d_needsCheck ){ + std::vector< Node > lemmas; + getInstantiations( lemmas ); + //add lemmas to quantifiers engine + for( unsigned i=0; iaddLemma( lemmas[i], false ); + } + d_needsCheck = false; + } +} + + +void LtePartialInst::reset() { + d_reps.clear(); + eq::EqualityEngine* ee = d_quantEngine->getMasterEqualityEngine(); + eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( ee ); + while( !eqcs_i.isFinished() ){ + TNode r = (*eqcs_i); + TypeNode tn = r.getType(); + d_reps[tn].push_back( r ); + ++eqcs_i; + } +} + + +/** get instantiations */ +void LtePartialInst::getInstantiations( std::vector< Node >& lemmas ) { + Trace("lte-partial-inst") << "LTE : get instantiations, # quant = " << d_lte_asserts.size() << std::endl; + reset(); + for( unsigned i=0; i bvs; + for( unsigned j=0; jmkNode( BOUND_VAR_LIST, bvs ); + } + std::vector< Node > conj; + std::vector< Node > terms; + std::vector< TypeNode > types; + for( unsigned j=0; jmkNode( OR, q.negate(), conj.size()==1 ? conj[0] : NodeManager::currentNM()->mkNode( AND, conj ) ) ); + d_wasInvoked = true; + d_quantEngine->getModel()->markQuantifierReduced( q ); + } + } +} + +void LtePartialInst::getPartialInstantiations( std::vector< Node >& conj, Node q, Node bvl, + std::vector< Node >& vars, std::vector< Node >& terms, std::vector< TypeNode >& types, TermArgTrie * curr, + unsigned pindex, unsigned paindex, unsigned iindex ){ + if( iindex==vars.size() ){ + Node body = q[1].substitute( vars.begin(), vars.end(), terms.begin(), terms.end() ); + if( bvl.isNull() ){ + conj.push_back( body ); + Trace("lte-partial-inst") << " - ground conjunct : " << body << std::endl; + }else{ + Node nq; + if( q.getNumChildren()==3 ){ + Node ipl = q[2].substitute( vars.begin(), vars.end(), terms.begin(), terms.end() ); + nq = NodeManager::currentNM()->mkNode( FORALL, bvl, body, ipl ); + }else{ + nq = NodeManager::currentNM()->mkNode( FORALL, bvl, body ); + } + Trace("lte-partial-inst") << " - quantified conjunct : " << nq << std::endl; + LtePartialInstAttribute ltpia; + nq.setAttribute(ltpia,true); + conj.push_back( nq ); + } + }else{ + Assert( pindexgetTermDatabase()->getTermArgTrie( pat.getOperator() ); + } + for( std::map< TNode, TermArgTrie >::iterator it = curr->d_data.begin(); it != curr->d_data.end(); ++it ){ + terms[d_pat_var_order[q][iindex]] = it->first; + getPartialInstantiations( conj, q, bvl, vars, terms, types, &it->second, pindex, paindex+1, iindex+1 ); + } + } + }else{ + std::map< TypeNode, std::vector< Node > >::iterator it = d_reps.find( types[iindex] ); + if( it!=d_reps.end() ){ + Trace("lte-partial-inst-debug") << it->second.size() << " reps of type " << types[iindex] << std::endl; + for( unsigned i=0; isecond.size(); i++ ){ + terms[d_pat_var_order[q][iindex]] = it->second[i]; + getPartialInstantiations( conj, q, bvl, vars, terms, types, NULL, pindex+1, 0, iindex+1 ); + } + }else{ + Trace("lte-partial-inst-debug") << "No reps found of type " << types[iindex] << std::endl; + } + } + } +} diff --git a/src/theory/quantifiers/local_theory_ext.h b/src/theory/quantifiers/local_theory_ext.h new file mode 100644 index 000000000..6e2ee34af --- /dev/null +++ b/src/theory/quantifiers/local_theory_ext.h @@ -0,0 +1,79 @@ +/********************* */ +/*! \file local_theory_ext.h + ** \verbatim + ** Original author: Andrew Reynolds + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2014 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief local theory extensions util + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY__LOCAL_THEORY_EXT_H +#define __CVC4__THEORY__LOCAL_THEORY_EXT_H + +#include "theory/quantifiers_engine.h" +#include "context/cdo.h" + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +class TermArgTrie; + +class LtePartialInst : public QuantifiersModule { +private: + // was this module invoked + bool d_wasInvoked; + // needs check + bool d_needsCheck; + //representatives per type + std::map< TypeNode, std::vector< Node > > d_reps; + // should we instantiate quantifier + std::map< Node, bool > d_do_inst; + // have we instantiated quantifier + std::map< Node, bool > d_inst; + std::map< Node, std::vector< Node > > d_vars; + std::map< Node, std::vector< int > > d_pat_var_order; + /** list of relevant quantifiers asserted in the current context */ + std::vector< Node > d_lte_asserts; + /** reset */ + void reset(); + /** get instantiations */ + void getInstantiations( std::vector< Node >& lemmas ); + void getPartialInstantiations( std::vector< Node >& conj, Node q, Node bvl, + std::vector< Node >& vars, std::vector< Node >& inst, std::vector< TypeNode >& types, TermArgTrie * curr, + unsigned pindex, unsigned paindex, unsigned iindex ); + /** get eligible inst variables */ + void getEligibleInstVars( Node n, std::map< Node, bool >& vars ); + + bool addVariableToPatternList( Node v, std::vector< int >& pat_var_order, std::map< Node, int >& var_order ); +public: + LtePartialInst( QuantifiersEngine * qe, context::Context* c ); + /** add quantifier : special form of registration */ + bool addQuantifier( Node q ); + /** was invoked */ + bool wasInvoked() { return d_wasInvoked; } + + /* whether this module needs to check this round */ + bool needsCheck( Theory::Effort e ); + /* Call during quantifier engine's check */ + void check( Theory::Effort e, unsigned quant_e ); + /* Called for new quantifiers */ + void registerQuantifier( Node q ) {} + void assertNode( Node n ) {} + /** Identify this module (for debugging, dynamic configuration, etc..) */ + std::string identify() const { return "LtePartialInst"; } + +}; + +} +} +} + +#endif diff --git a/src/theory/quantifiers/quant_util.cpp b/src/theory/quantifiers/quant_util.cpp index 088ba093f..f73bc7bb2 100644 --- a/src/theory/quantifiers/quant_util.cpp +++ b/src/theory/quantifiers/quant_util.cpp @@ -255,142 +255,3 @@ void QuantPhaseReq::getPolarity( Node n, int child, bool hasPol, bool pol, bool& } } } - - -QuantLtePartialInst::QuantLtePartialInst( QuantifiersEngine * qe, context::Context* c ) : d_wasInvoked( false ), d_qe( qe ), d_lte_asserts( c ){ - -} - -/** add quantifier */ -bool QuantLtePartialInst::addQuantifier( Node q ) { - if( d_do_inst.find( q )!=d_do_inst.end() ){ - if( d_do_inst[q] ){ - d_lte_asserts.push_back( q ); - return true; - }else{ - return false; - } - }else{ - d_vars[q].clear(); - //check if this quantified formula is eligible for partial instantiation - std::map< Node, bool > vars; - for( unsigned i=0; i& vars ) { - if( n.getKind()!=APPLY_UF || n.getType().isBoolean() ){ - for( unsigned i=0; igetMasterEqualityEngine(); - eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( ee ); - while( !eqcs_i.isFinished() ){ - TNode r = (*eqcs_i); - TypeNode tn = r.getType(); - d_reps[tn].push_back( r ); - ++eqcs_i; - } -} - -/** get instantiations */ -void QuantLtePartialInst::getInstantiations( std::vector< Node >& lemmas ) { - Trace("lte-partial-inst") << "LTE : get instantiations, # quant = " << d_lte_asserts.size() << std::endl; - reset(); - for( unsigned i=0; i bvs; - for( unsigned j=0; jmkNode( BOUND_VAR_LIST, bvs ); - } - std::vector< Node > conj; - std::vector< Node > terms; - std::vector< TypeNode > types; - for( unsigned j=0; jmkNode( OR, q.negate(), conj.size()==1 ? conj[0] : NodeManager::currentNM()->mkNode( AND, conj ) ) ); - d_wasInvoked = true; - } - } -} - -void QuantLtePartialInst::getPartialInstantiations( std::vector< Node >& conj, Node q, Node bvl, - std::vector< Node >& vars, std::vector< Node >& terms, std::vector< TypeNode >& types, unsigned index ){ - if( index==vars.size() ){ - Node body = q[1].substitute( vars.begin(), vars.end(), terms.begin(), terms.end() ); - if( bvl.isNull() ){ - conj.push_back( body ); - Trace("lte-partial-inst") << " - ground conjunct : " << body << std::endl; - }else{ - Node nq; - if( q.getNumChildren()==3 ){ - Node ipl = q[2].substitute( vars.begin(), vars.end(), terms.begin(), terms.end() ); - nq = NodeManager::currentNM()->mkNode( FORALL, bvl, body, ipl ); - }else{ - nq = NodeManager::currentNM()->mkNode( FORALL, bvl, body ); - } - Trace("lte-partial-inst") << " - quantified conjunct : " << nq << std::endl; - LtePartialInstAttribute ltpia; - nq.setAttribute(ltpia,true); - conj.push_back( nq ); - } - }else{ - std::map< TypeNode, std::vector< Node > >::iterator it = d_reps.find( types[index] ); - if( it!=d_reps.end() ){ - terms.push_back( Node::null() ); - Trace("lte-partial-inst-debug") << it->second.size() << " reps of type " << types[index] << std::endl; - for( unsigned i=0; isecond.size(); i++ ){ - terms[index] = it->second[i]; - getPartialInstantiations( conj, q, bvl, vars, terms, types, index+1 ); - } - terms.pop_back(); - }else{ - Trace("lte-partial-inst-debug") << "No reps found of type " << types[index] << std::endl; - } - } -} diff --git a/src/theory/quantifiers/quant_util.h b/src/theory/quantifiers/quant_util.h index 116211bfb..d7e220b2e 100644 --- a/src/theory/quantifiers/quant_util.h +++ b/src/theory/quantifiers/quant_util.h @@ -110,38 +110,6 @@ public: virtual void setLiberal( bool l ) = 0; };/* class EqualityQuery */ -class QuantLtePartialInst { -private: - // was this module invoked - bool d_wasInvoked; - //representatives per type - std::map< TypeNode, std::vector< Node > > d_reps; - // should we instantiate quantifier - std::map< Node, bool > d_do_inst; - // have we instantiated quantifier - std::map< Node, bool > d_inst; - std::map< Node, std::vector< Node > > d_vars; - /** pointer to quant engine */ - QuantifiersEngine * d_qe; - /** list of relevant quantifiers asserted in the current context */ - context::CDList d_lte_asserts; - /** reset */ - void reset(); - /** get instantiations */ - void getPartialInstantiations( std::vector< Node >& conj, Node q, Node bvl, - std::vector< Node >& vars, std::vector< Node >& inst, std::vector< TypeNode >& types, unsigned index ); - /** get eligible inst variables */ - void getEligibleInstVars( Node n, std::map< Node, bool >& vars ); -public: - QuantLtePartialInst( QuantifiersEngine * qe, context::Context* c ); - /** add quantifier */ - bool addQuantifier( Node q ); - /** get instantiations */ - void getInstantiations( std::vector< Node >& lemmas ); - /** was invoked */ - bool wasInvoked() { return d_wasInvoked; } -}; - } } diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 7fb6c0bb7..a1a6dcefc 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -30,6 +30,7 @@ #include "theory/quantifiers/quant_conflict_find.h" #include "theory/quantifiers/conjecture_generator.h" #include "theory/quantifiers/ce_guided_instantiation.h" +#include "theory/quantifiers/local_theory_ext.h" #include "theory/quantifiers/relevant_domain.h" #include "theory/uf/options.h" #include "theory/uf/theory_uf.h" @@ -154,7 +155,8 @@ d_lemmas_produced_c(u){ d_ceg_inst = NULL; } if( options::ltePartialInst() ){ - d_lte_part_inst = new QuantLtePartialInst( this, c ); + d_lte_part_inst = new quantifiers::LtePartialInst( this, c ); + d_modules.push_back( d_lte_part_inst ); }else{ d_lte_part_inst = NULL; } @@ -260,10 +262,6 @@ void QuantifiersEngine::check( Theory::Effort e ){ } if( e==Theory::EFFORT_FULL ){ d_ierCounter++; - //process partial instantiations for LTE - if( d_lte_part_inst ){ - d_lte_part_inst->getInstantiations( d_lemmas_waiting ); - } }else if( e==Theory::EFFORT_LAST_CALL ){ d_ierCounter_lc++; } @@ -271,8 +269,8 @@ void QuantifiersEngine::check( Theory::Effort e ){ bool needsModel = false; bool needsFullModel = false; std::vector< QuantifiersModule* > qm; - if( d_model->getNumAssertedQuantifiers()>0 ){ - needsCheck = e>=Theory::EFFORT_LAST_CALL; //always need to check at or above last call + if( d_model->checkNeeded() ){ + needsCheck = needsCheck || e>=Theory::EFFORT_LAST_CALL; //always need to check at or above last call for( int i=0; i<(int)d_modules.size(); i++ ){ if( d_modules[i]->needsCheck( e ) ){ qm.push_back( d_modules[i] ); @@ -288,21 +286,27 @@ void QuantifiersEngine::check( Theory::Effort e ){ } if( needsCheck ){ Trace("quant-engine") << "Quantifiers Engine check, level = " << e << std::endl; - Trace("quant-engine-debug") << " modules to check : "; - for( unsigned i=0; iidentify() << " "; + if( Trace.isOn("quant-engine-debug") ){ + Trace("quant-engine-debug") << " modules to check : "; + for( unsigned i=0; iidentify() << " "; + } + Trace("quant-engine-debug") << std::endl; + Trace("quant-engine-debug") << " # quantified formulas = " << d_model->getNumAssertedQuantifiers() << std::endl; + if( d_model->getNumToReduceQuantifiers()>0 ){ + Trace("quant-engine-debug") << " # quantified formulas to reduce = " << d_model->getNumToReduceQuantifiers() << std::endl; + } + if( !d_lemmas_waiting.empty() ){ + Trace("quant-engine-debug") << " lemmas waiting = " << d_lemmas_waiting.size() << std::endl; + } + Trace("quant-engine-debug") << " Theory engine finished : " << !d_te->needCheck() << std::endl; + Trace("quant-engine-debug") << "Resetting all modules..." << std::endl; } - Trace("quant-engine-debug") << std::endl; - Trace("quant-engine-debug") << " # quantified formulas = " << d_model->getNumAssertedQuantifiers() << std::endl; - if( !d_lemmas_waiting.empty() ){ - Trace("quant-engine-debug") << " lemmas waiting = " << d_lemmas_waiting.size() << std::endl; + if( Trace.isOn("quant-engine-ee") ){ + Trace("quant-engine-ee") << "Equality engine : " << std::endl; + debugPrintEqualityEngine( "quant-engine-ee" ); } - Trace("quant-engine-debug") << " Theory engine finished : " << !d_te->needCheck() << std::endl; - Trace("quant-engine-ee") << "Equality engine : " << std::endl; - debugPrintEqualityEngine( "quant-engine-ee" ); - - Trace("quant-engine-debug") << "Resetting all modules..." << std::endl; //reset relevant information d_conflict = false; d_hasAddedLemma = false; @@ -406,36 +410,54 @@ void QuantifiersEngine::check( Theory::Effort e ){ } } -void QuantifiersEngine::registerQuantifier( Node f ){ - if( std::find( d_quants.begin(), d_quants.end(), f )==d_quants.end() ){ +bool QuantifiersEngine::registerQuantifier( Node f ){ + std::map< Node, bool >::iterator it = d_quants.find( f ); + if( it==d_quants.end() ){ Trace("quant") << "QuantifiersEngine : Register quantifier "; Trace("quant") << " : " << f << std::endl; - d_quants.push_back( f ); - ++(d_statistics.d_num_quant); Assert( f.getKind()==FORALL ); - //make instantiation constants for f - d_term_db->makeInstantiationConstantsFor( f ); - d_term_db->computeAttributes( f ); - QuantifiersModule * qm = getOwner( f ); - if( qm!=NULL ){ - Trace("quant") << " Owner : " << qm->identify() << std::endl; - } - //register with quantifier relevance - if( d_quant_rel ){ - d_quant_rel->registerQuantifier( f ); - } - //register with each module - for( int i=0; i<(int)d_modules.size(); i++ ){ - d_modules[i]->registerQuantifier( f ); + + //check whether we should apply a reduction + bool reduced = false; + if( d_lte_part_inst && !f.getAttribute(LtePartialInstAttribute()) ){ + Trace("lte-partial-inst") << "LTE: Partially instantiate " << f << "?" << std::endl; + if( d_lte_part_inst->addQuantifier( f ) ){ + reduced = true; + } } - Node ceBody = d_term_db->getInstConstantBody( f ); - //generate the phase requirements - d_phase_reqs[f] = new QuantPhaseReq( ceBody, true ); - //also register it with the strong solver - if( options::finiteModelFind() ){ - ((uf::TheoryUF*)d_te->theoryOf( THEORY_UF ))->getStrongSolver()->registerQuantifier( f ); + if( reduced ){ + d_model->assertQuantifier( f, true ); + d_quants[f] = false; + return false; + }else{ + //make instantiation constants for f + d_term_db->makeInstantiationConstantsFor( f ); + d_term_db->computeAttributes( f ); + QuantifiersModule * qm = getOwner( f ); + if( qm!=NULL ){ + Trace("quant") << " Owner : " << qm->identify() << std::endl; + } + //register with quantifier relevance + if( d_quant_rel ){ + d_quant_rel->registerQuantifier( f ); + } + //register with each module + for( int i=0; i<(int)d_modules.size(); i++ ){ + d_modules[i]->registerQuantifier( f ); + } + Node ceBody = d_term_db->getInstConstantBody( f ); + //generate the phase requirements + d_phase_reqs[f] = new QuantPhaseReq( ceBody, true ); + //also register it with the strong solver + if( options::finiteModelFind() ){ + ((uf::TheoryUF*)d_te->theoryOf( THEORY_UF ))->getStrongSolver()->registerQuantifier( f ); + } + d_quants[f] = true; + return true; } + }else{ + return it->second; } } @@ -464,18 +486,14 @@ void QuantifiersEngine::assertQuantifier( Node f, bool pol ){ } //assert to modules TODO : handle !pol if( pol ){ - if( d_lte_part_inst && !f.getAttribute(LtePartialInstAttribute()) ){ - Trace("lte-partial-inst") << "LTE: Partially instantiate " << f << "?" << std::endl; - if( d_lte_part_inst->addQuantifier( f ) ){ - return; - } - } //register the quantifier - registerQuantifier( f ); + bool nreduced = registerQuantifier( f ); //assert it to each module - d_model->assertQuantifier( f ); - for( int i=0; i<(int)d_modules.size(); i++ ){ - d_modules[i]->assertNode( f ); + if( nreduced ){ + d_model->assertQuantifier( f ); + for( int i=0; i<(int)d_modules.size(); i++ ){ + d_modules[i]->assertNode( f ); + } } } } diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index eb4470eec..78609914f 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -89,6 +89,7 @@ namespace quantifiers { class QModelBuilder; class ConjectureGenerator; class CegInstantiation; + class LtePartialInst; }/* CVC4::theory::quantifiers */ namespace inst { @@ -135,7 +136,7 @@ private: /** ceg instantiation */ quantifiers::CegInstantiation * d_ceg_inst; /** lte partial instantiation */ - QuantLtePartialInst * d_lte_part_inst; + quantifiers::LtePartialInst * d_lte_part_inst; public: //effort levels enum { QEFFORT_CONFLICT, @@ -144,7 +145,7 @@ public: //effort levels }; private: /** list of all quantifiers seen */ - std::vector< Node > d_quants; + std::map< Node, bool > d_quants; /** list of all lemmas produced */ //std::map< Node, bool > d_lemmas_produced; BoolMap d_lemmas_produced_c; @@ -217,6 +218,8 @@ public: //modules quantifiers::ConjectureGenerator * getConjectureGenerator() { return d_sg_gen; } /** ceg instantiation */ quantifiers::CegInstantiation * getCegInstantiation() { return d_ceg_inst; } + /** local theory ext partial inst */ + quantifiers::LtePartialInst * getLtePartialInst() { return d_lte_part_inst; } private: /** owner of quantified formulas */ std::map< Node, QuantifiersModule * > d_owner; @@ -233,7 +236,7 @@ public: /** check at level */ void check( Theory::Effort e ); /** register quantifier */ - void registerQuantifier( Node f ); + bool registerQuantifier( Node f ); /** register quantifier */ void registerPattern( std::vector & pattern); /** assert universal quantifier */ @@ -282,11 +285,6 @@ public: bool getInstWhenNeedsCheck( Theory::Effort e ); /** set instantiation level attr */ static void setInstantiationLevelAttr( Node n, uint64_t level ); -public: - /** get number of quantifiers */ - int getNumQuantifiers() { return (int)d_quants.size(); } - /** get quantifier */ - Node getQuantifier( int i ) { return d_quants[i]; } public: /** get model */ quantifiers::FirstOrderModel* getModel() { return d_model; }