From f47f24528f5d19ac0affd572f3d34c090e97f9f9 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Thu, 18 Feb 2016 22:50:05 -0600 Subject: Implement dynamic splitting for quantified formulas. Minor refactoring of reductions in quantifiers engine. --- src/theory/quantifiers/alpha_equivalence.cpp | 4 +- src/theory/quantifiers/alpha_equivalence.h | 2 +- src/theory/quantifiers/first_order_model.cpp | 30 ++---- src/theory/quantifiers/first_order_model.h | 10 +- src/theory/quantifiers/inst_strategy_cbqi.cpp | 8 +- src/theory/quantifiers/local_theory_ext.cpp | 113 +++++++++++----------- src/theory/quantifiers/local_theory_ext.h | 4 +- src/theory/quantifiers/quant_split.cpp | 129 ++++++++++++++++++++++++++ src/theory/quantifiers/quant_split.h | 54 +++++++++++ 9 files changed, 262 insertions(+), 92 deletions(-) create mode 100644 src/theory/quantifiers/quant_split.cpp create mode 100644 src/theory/quantifiers/quant_split.h (limited to 'src/theory/quantifiers') diff --git a/src/theory/quantifiers/alpha_equivalence.cpp b/src/theory/quantifiers/alpha_equivalence.cpp index b72f15a01..d49b37e4c 100644 --- a/src/theory/quantifiers/alpha_equivalence.cpp +++ b/src/theory/quantifiers/alpha_equivalence.cpp @@ -79,7 +79,7 @@ bool AlphaEquivalenceTypeNode::registerNode( AlphaEquivalenceTypeNode* aetn, return AlphaEquivalenceNode::registerNode( &(aetn->d_data), qe, q, tt, arg_index ); } -bool AlphaEquivalence::registerQuantifier( Node q ) { +bool AlphaEquivalence::reduceQuantifier( Node q ) { Assert( q.getKind()==FORALL ); Trace("aeq") << "Alpha equivalence : register " << q << std::endl; //construct canonical quantified formula @@ -99,7 +99,7 @@ bool AlphaEquivalence::registerQuantifier( Node q ) { sto.d_tdb = d_qe->getTermDatabase(); std::sort( typs.begin(), typs.end(), sto ); Trace("aeq-debug") << " "; - bool ret = AlphaEquivalenceTypeNode::registerNode( &d_ae_typ_trie, d_qe, q, t, typs, typ_count ); + bool ret = !AlphaEquivalenceTypeNode::registerNode( &d_ae_typ_trie, d_qe, q, t, typs, typ_count ); Trace("aeq") << " ...result : " << ret << std::endl; return ret; } diff --git a/src/theory/quantifiers/alpha_equivalence.h b/src/theory/quantifiers/alpha_equivalence.h index 99517fd2a..18a700842 100644 --- a/src/theory/quantifiers/alpha_equivalence.h +++ b/src/theory/quantifiers/alpha_equivalence.h @@ -48,7 +48,7 @@ public: AlphaEquivalence( QuantifiersEngine* qe ) : d_qe( qe ){} ~AlphaEquivalence(){} - bool registerQuantifier( Node q ); + bool reduceQuantifier( Node q ); }; } diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp index 272f16be8..6c912cdab 100644 --- a/src/theory/quantifiers/first_order_model.cpp +++ b/src/theory/quantifiers/first_order_model.cpp @@ -36,18 +36,11 @@ d_qe( qe ), d_forall_asserts( c ), d_isModelSet( c, false ){ } -void FirstOrderModel::assertQuantifier( Node n, bool reduced ){ - if( !reduced ){ - if( n.getKind()==FORALL ){ - d_forall_asserts.push_back( n ); - }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; +void FirstOrderModel::assertQuantifier( Node n ){ + if( n.getKind()==FORALL ){ + d_forall_asserts.push_back( n ); + }else if( n.getKind()==NOT ){ + Assert( n[0].getKind()==FORALL ); } } @@ -122,20 +115,17 @@ Node FirstOrderModel::getSomeDomainElement(TypeNode tn){ /** 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; + return d_forall_asserts.size()>0; } void FirstOrderModel::reset_round() { d_quant_active.clear(); } +//bool FirstOrderModel::isQuantifierAsserted( TNode q ) { +// return d_forall_asserts.find( q )!=d_forall_asserts.end(); +//} + void FirstOrderModel::setQuantifierActive( TNode q, bool active ) { d_quant_active[q] = active; } diff --git a/src/theory/quantifiers/first_order_model.h b/src/theory/quantifiers/first_order_model.h index d42eb61e3..d5dc62667 100644 --- a/src/theory/quantifiers/first_order_model.h +++ b/src/theory/quantifiers/first_order_model.h @@ -49,8 +49,6 @@ protected: QuantifiersEngine * d_qe; /** 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,13 +57,11 @@ protected: virtual Node getCurrentUfModelValue( Node n, std::vector< Node > & args, bool partial ) = 0; public: //for Theory Quantifiers: /** assert quantifier */ - void assertQuantifier( Node n, bool reduced = false ); + void assertQuantifier( Node n ); /** 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(); } /** initialize model for term */ void initializeModelForTerm( Node n, std::map< Node, bool >& visited ); virtual void processInitializeModelForTerm( Node n ) = 0; @@ -94,14 +90,14 @@ public: 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; public: /** reset round */ void reset_round(); + /** is quantified formula asserted */ + //bool isQuantifierAsserted( TNode q ); /** set quantified formula active/inactive * a quantified formula may be set inactive if for instance: * - it is entailed by other quantified formulas diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp index ad400413e..e6c9b9e6b 100644 --- a/src/theory/quantifiers/inst_strategy_cbqi.cpp +++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp @@ -169,13 +169,15 @@ void InstStrategyCbqi::registerCounterexampleLemma( Node q, Node lem ){ bool InstStrategyCbqi::hasNonCbqiOperator( Node n, std::map< Node, bool >& visited ){ if( visited.find( n )==visited.end() ){ visited[n] = true; - if( n.getKind()!=INST_CONSTANT && TermDb::hasInstConstAttr( n ) ){ + if( n.getKind()!=BOUND_VARIABLE && TermDb::hasBoundVarAttr( n ) ){ if( !inst::Trigger::isCbqiKind( n.getKind() ) ){ Trace("cbqi-debug2") << "Non-cbqi kind : " << n.getKind() << " in " << n << std::endl; return true; }else if( n.getKind()==MULT && ( n.getNumChildren()!=2 || !n[0].isConst() ) ){ Trace("cbqi-debug2") << "Non-linear arithmetic : " << n << std::endl; return true; + }else if( n.getKind()==FORALL ){ + return hasNonCbqiOperator( n[1], visited ); }else{ for( unsigned i=0; igetTermDatabase()->getInstConstantBody( q ); + //Node cb = d_quantEngine->getTermDatabase()->getInstConstantBody( q ); std::map< Node, bool > visited; - ret = !hasNonCbqiVariable( q ) && !hasNonCbqiOperator( cb, visited ); + ret = !hasNonCbqiVariable( q ) && !hasNonCbqiOperator( q[1], visited ); } } } diff --git a/src/theory/quantifiers/local_theory_ext.cpp b/src/theory/quantifiers/local_theory_ext.cpp index 794032c87..86fbdc7f7 100644 --- a/src/theory/quantifiers/local_theory_ext.cpp +++ b/src/theory/quantifiers/local_theory_ext.cpp @@ -1,5 +1,5 @@ /********************* */ -/*! \file quant_util.cpp +/*! \file local_theory_ext.cpp ** \verbatim ** Original author: Andrew Reynolds ** Major contributors: none @@ -31,69 +31,69 @@ 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; +void LtePartialInst::preRegisterQuantifier( Node q ) { + if( !q.getAttribute(LtePartialInstAttribute()) ){ + if( d_do_inst.find( q )!=d_do_inst.end() ){ + if( d_do_inst[q] ){ + d_lte_asserts.push_back( q ); + d_quantEngine->setOwner( q, this ); + } }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 vars; + for( unsigned i=0; i var_order; + bool doInst = true; + for( unsigned i=0; isetOwner( q, this ); } } - - - Trace("lte-partial-inst") << "LTE: ...will " << ( doInst ? "" : "not ") << "instantiate " << q << std::endl; - d_do_inst[q] = doInst; - if( doInst ){ - d_lte_asserts.push_back( q ); - d_needsCheck = true; - } - return doInst; } } @@ -188,7 +188,6 @@ void LtePartialInst::getInstantiations( std::vector< Node >& lemmas ) { Assert( !conj.empty() ); lemmas.push_back( NodeManager::currentNM()->mkNode( OR, q.negate(), conj.size()==1 ? conj[0] : NodeManager::currentNM()->mkNode( AND, conj ) ) ); d_wasInvoked = true; - d_quantEngine->getModel()->markQuantifierReduced( q ); } } } diff --git a/src/theory/quantifiers/local_theory_ext.h b/src/theory/quantifiers/local_theory_ext.h index 6e2ee34af..d802c2cf7 100644 --- a/src/theory/quantifiers/local_theory_ext.h +++ b/src/theory/quantifiers/local_theory_ext.h @@ -55,8 +55,8 @@ private: 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 ); + /** determine whether this quantified formula will be reduced */ + void preRegisterQuantifier( Node q ); /** was invoked */ bool wasInvoked() { return d_wasInvoked; } diff --git a/src/theory/quantifiers/quant_split.cpp b/src/theory/quantifiers/quant_split.cpp new file mode 100644 index 000000000..e874ee5b8 --- /dev/null +++ b/src/theory/quantifiers/quant_split.cpp @@ -0,0 +1,129 @@ +/********************* */ +/*! \file quant_split.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/quant_split.h" +#include "theory/quantifiers/term_database.h" +#include "theory/quantifiers_engine.h" +#include "theory/quantifiers/first_order_model.h" +#include "options/quantifiers_options.h" + +using namespace std; +using namespace CVC4; +using namespace CVC4::kind; +using namespace CVC4::context; +using namespace CVC4::theory; +using namespace CVC4::theory::quantifiers; + + +QuantDSplit::QuantDSplit( QuantifiersEngine * qe, context::Context* c ) : +QuantifiersModule( qe ), d_added_split( qe->getUserContext() ){ + +} + +/** pre register quantifier */ +void QuantDSplit::preRegisterQuantifier( Node q ) { + int max_index = -1; + int max_score = -1; + if( q.getNumChildren()==3 ){ + return; + } + Trace("quant-dsplit-debug") << "Check split quantified formula : " << q << std::endl; + for( unsigned i=0; imax_score ){ + max_index = i; + max_score = score; + } + } + } + } + + if( max_index!=-1 ){ + Trace("quant-dsplit-debug") << "Will split at index " << max_index << "." << std::endl; + d_quant_to_reduce[q] = max_index; + d_quantEngine->setOwner( q, this ); + } +} + +/* whether this module needs to check this round */ +bool QuantDSplit::needsCheck( Theory::Effort e ) { + return e>=Theory::EFFORT_FULL; +} +/* Call during quantifier engine's check */ +void QuantDSplit::check( Theory::Effort e, unsigned quant_e ) { + //flush lemmas ASAP (they are a reduction) + if( quant_e==QuantifiersEngine::QEFFORT_CONFLICT ){ + std::vector< Node > lemmas; + for(std::map< Node, int >::iterator it = d_quant_to_reduce.begin(); it != d_quant_to_reduce.end(); ++it) { + Node q = it->first; + if( d_added_split.find( q )==d_added_split.end() ){ + d_added_split.insert( q ); + std::vector< Node > bvs; + for( unsigned i=0; isecond ){ + bvs.push_back( q[0][i] ); + } + } + std::vector< Node > disj; + disj.push_back( q.negate() ); + TNode svar = q[0][it->second]; + TypeNode tn = svar.getType(); + if( tn.isDatatype() ){ + const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype(); + for( unsigned j=0; j vars; + for( unsigned k=0; kmkBoundVar( tns ); + vars.push_back( v ); + } + std::vector< Node > bvs_cmb; + bvs_cmb.insert( bvs_cmb.end(), bvs.begin(), bvs.end() ); + bvs_cmb.insert( bvs_cmb.end(), vars.begin(), vars.end() ); + vars.insert( vars.begin(), Node::fromExpr( dt[j].getConstructor() ) ); + Node c = NodeManager::currentNM()->mkNode( kind::APPLY_CONSTRUCTOR, vars ); + TNode ct = c; + Node body = q[1].substitute( svar, ct ); + if( !bvs_cmb.empty() ){ + body = NodeManager::currentNM()->mkNode( kind::FORALL, NodeManager::currentNM()->mkNode( kind::BOUND_VAR_LIST, bvs_cmb ), body ); + } + disj.push_back( body ); + } + }else{ + Assert( false ); + } + lemmas.push_back( disj.size()==1 ? disj[0] : NodeManager::currentNM()->mkNode( kind::OR, disj ) ); + } + } + + //add lemmas to quantifiers engine + for( unsigned i=0; iaddLemma( lemmas[i], false ); + } + } +} + diff --git a/src/theory/quantifiers/quant_split.h b/src/theory/quantifiers/quant_split.h new file mode 100644 index 000000000..f40acc2fd --- /dev/null +++ b/src/theory/quantifiers/quant_split.h @@ -0,0 +1,54 @@ +/********************* */ +/*! \file quant_split.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 dynamic quantifiers splitting + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY__QUANT_SPLIT_H +#define __CVC4__THEORY__QUANT_SPLIT_H + +#include "theory/quantifiers_engine.h" +#include "context/cdo.h" + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +class QuantDSplit : public QuantifiersModule { + typedef context::CDHashSet NodeSet; +private: + /** list of relevant quantifiers asserted in the current context */ + std::map< Node, int > d_quant_to_reduce; + /** whether we have instantiated quantified formulas */ + NodeSet d_added_split; +public: + QuantDSplit( QuantifiersEngine * qe, context::Context* c ); + /** determine whether this quantified formula will be reduced */ + void preRegisterQuantifier( Node q ); + + /* 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 "QuantDSplit"; } +}; + +} +} +} + +#endif -- cgit v1.2.3