diff options
Diffstat (limited to 'src/theory/quantifiers')
-rw-r--r-- | src/theory/quantifiers/anti_skolem.cpp | 269 | ||||
-rw-r--r-- | src/theory/quantifiers/anti_skolem.h | 75 | ||||
-rw-r--r-- | src/theory/quantifiers/ce_guided_single_inv.cpp | 104 | ||||
-rw-r--r-- | src/theory/quantifiers/ce_guided_single_inv.h | 11 | ||||
-rw-r--r-- | src/theory/quantifiers/quant_split.cpp | 2 |
5 files changed, 423 insertions, 38 deletions
diff --git a/src/theory/quantifiers/anti_skolem.cpp b/src/theory/quantifiers/anti_skolem.cpp new file mode 100644 index 000000000..47b4d95d1 --- /dev/null +++ b/src/theory/quantifiers/anti_skolem.cpp @@ -0,0 +1,269 @@ +/********************* */ +/*! \file anti_skolem.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 anti-skolemization + ** ( forall x. P[ f( x ) ] ^ forall x. Q[ f( x ) ] ) => forall x. exists y. ( P[ y ] ^ Q[ y ] ) + **/ + +#include "theory/quantifiers/anti_skolem.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; + + +struct sortTypeOrder { + TermDb* d_tdb; + bool operator() (TypeNode i, TypeNode j) { + return d_tdb->getIdForType( i )<d_tdb->getIdForType( j ); + } +}; + +void QuantAntiSkolem::SkQuantTypeCache::add( std::vector< TypeNode >& typs, Node q, unsigned index ) { + if( index==typs.size() ){ + Assert( std::find( d_quants.begin(), d_quants.end(), q )==d_quants.end() ); + d_quants.push_back( q ); + }else{ + d_children[typs[index]].add( typs, q, index+1 ); + } +} + +void QuantAntiSkolem::SkQuantTypeCache::sendLemmas( QuantAntiSkolem * ask ) { + for( std::map< TypeNode, SkQuantTypeCache >::iterator it = d_children.begin(); it != d_children.end(); ++it ){ + it->second.sendLemmas( ask ); + } + if( !d_quants.empty() ){ + ask->sendAntiSkolemizeLemma( d_quants ); + } +} + +bool QuantAntiSkolem::CDSkQuantCache::add( context::Context* c, std::vector< Node >& quants, unsigned index ) { + if( index==quants.size() ){ + if( !d_valid.get() ){ + d_valid.set( true ); + return true; + }else{ + return false; + } + }else{ + Node n = quants[index]; + std::map< Node, CDSkQuantCache* >::iterator it = d_data.find( n ); + CDSkQuantCache* skc; + if( it==d_data.end() ){ + skc = new CDSkQuantCache( c ); + d_data[n] = skc; + }else{ + skc = it->second; + } + return skc->add( c, quants, index+1 ); + } +} + +QuantAntiSkolem::QuantAntiSkolem( QuantifiersEngine * qe ) : QuantifiersModule( qe ){ + d_sqc = new CDSkQuantCache( qe->getUserContext() ); +} + +/* Call during quantifier engine's check */ +void QuantAntiSkolem::check( Theory::Effort e, unsigned quant_e ) { + if( quant_e==QuantifiersEngine::QEFFORT_STANDARD ){ + d_sqtc.clear(); + for( int i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){ + Node q = d_quantEngine->getModel()->getAssertedQuantifier( i ); + if( d_quant_processed.find( q )==d_quant_processed.end() ){ + d_quant_processed[q] = true; + Trace("anti-sk") << "Process quantified formula : " << q << std::endl; + bool success = false; + if( d_quant_sip[q].init( q[1] ) ){ + Trace("anti-sk") << "- Partitioned to single invocation parts : " << std::endl; + d_quant_sip[q].debugPrint( "anti-sk" ); + //check if it is single invocation + if( d_quant_sip[q].isPurelySingleInvocation() ){ + //for now, only do purely single invocation + success = true; + } + }else{ + Trace("anti-sk") << "- Failed to initialize." << std::endl; + } + if( success ){ + //sort the argument variables + d_ask_types[q].insert( d_ask_types[q].end(), d_quant_sip[q].d_arg_types.begin(), d_quant_sip[q].d_arg_types.end() ); + std::map< TypeNode, std::vector< unsigned > > indices; + for( unsigned j=0; j<d_ask_types[q].size(); j++ ){ + indices[d_ask_types[q][j]].push_back( j ); + } + sortTypeOrder sto; + sto.d_tdb = d_quantEngine->getTermDatabase(); + std::sort( d_ask_types[q].begin(), d_ask_types[q].end(), sto ); + //increment j on inner loop + for( unsigned j=0; j<d_ask_types[q].size(); ){ + TypeNode curr = d_ask_types[q][j]; + for( unsigned k=0; k<indices[curr].size(); k++ ){ + Assert( d_ask_types[q][j]==curr ); + d_ask_types_index[q].push_back( indices[curr][k] ); + j++; + } + } + Assert( d_ask_types_index[q].size()==d_ask_types[q].size() ); + }else{ + d_quant_sip.erase( q ); + } + } + //now, activate the quantified formula + std::map< Node, std::vector< TypeNode > >::iterator it = d_ask_types.find( q ); + if( it!=d_ask_types.end() ){ + d_sqtc.add( it->second, q ); + } + } + Trace("anti-sk-debug") << "Process lemmas..." << std::endl; + //send out lemmas for each anti-skolemizable group of quantified formulas + d_sqtc.sendLemmas( this ); + Trace("anti-sk-debug") << "...Finished process lemmas" << std::endl; + } +} + +bool QuantAntiSkolem::sendAntiSkolemizeLemma( std::vector< Node >& quants, bool pconnected ) { + Assert( !quants.empty() ); + std::sort( quants.begin(), quants.end() ); + if( d_sqc->add( d_quantEngine->getUserContext(), quants ) ){ + //partition into connected components + if( pconnected && quants.size()>1 ){ + Trace("anti-sk-debug") << "Partition into connected components..." << std::endl; + int eqc_count = 0; + std::map< Node, int > func_to_eqc; + std::map< int, std::vector< Node > > eqc_to_func; + std::map< int, std::vector< Node > > eqc_to_quant; + for( unsigned i=0; i<quants.size(); i++ ){ + Node q = quants[i]; + std::vector< int > eqcs; + for( std::map< Node, bool >::iterator it = d_quant_sip[q].d_funcs.begin(); it != d_quant_sip[q].d_funcs.end(); ++it ){ + Node f = it->first; + std::map< Node, int >::iterator itf = func_to_eqc.find( f ); + if( itf == func_to_eqc.end() ){ + if( eqcs.empty() ){ + func_to_eqc[f] = eqc_count; + eqc_to_func[eqc_count].push_back( f ); + eqc_count++; + }else{ + func_to_eqc[f] = eqcs[0]; + eqc_to_func[eqcs[0]].push_back( f ); + } + } + if( std::find( eqcs.begin(), eqcs.end(), func_to_eqc[f] )==eqcs.end() ){ + eqcs.push_back( func_to_eqc[f] ); + } + } + Assert( !eqcs.empty() ); + //merge equivalence classes + int id = eqcs[0]; + eqc_to_quant[id].push_back( q ); + for( unsigned j=1; j<eqcs.size(); j++ ){ + int id2 = eqcs[j]; + std::map< int, std::vector< Node > >::iterator itef = eqc_to_func.find( id2 ); + if( itef!=eqc_to_func.end() ){ + for( unsigned k=0; k<itef->second.size(); k++ ){ + func_to_eqc[itef->second[k]] = id; + eqc_to_func[id].push_back( itef->second[k] ); + } + eqc_to_func.erase( id2 ); + } + itef = eqc_to_quant.find( id2 ); + if( itef!=eqc_to_quant.end() ){ + eqc_to_quant[id].insert( eqc_to_quant[id].end(), itef->second.begin(), itef->second.end() ); + eqc_to_quant.erase( id2 ); + } + } + } + if( eqc_to_quant.size()>1 ){ + bool addedLemma = false; + for( std::map< int, std::vector< Node > >::iterator it = eqc_to_quant.begin(); it != eqc_to_quant.end(); ++it ){ + Assert( it->second.size()<quants.size() ); + bool ret = sendAntiSkolemizeLemma( it->second, false ); + addedLemma = addedLemma || ret; + } + return addedLemma; + } + } + + Trace("anti-sk") << "Anti-skolemize group : " << std::endl; + for( unsigned i=0; i<quants.size(); i++ ){ + Trace("anti-sk") << " " << quants[i] << std::endl; + } + + std::vector< Node > outer_vars; + std::vector< Node > inner_vars; + Node q = quants[0]; + for( unsigned i=0; i<d_ask_types[q].size(); i++ ){ + Node v = NodeManager::currentNM()->mkBoundVar( d_ask_types[q][i] ); + Trace("anti-sk-debug") << "Outer var " << i << " : " << v << std::endl; + outer_vars.push_back( v ); + } + + std::map< Node, Node > func_to_var; + std::vector< Node > conj; + for( unsigned i=0; i<quants.size(); i++ ){ + Node q = quants[i]; + Trace("anti-sk-debug") << "Process " << q << std::endl; + std::vector< Node > subs_lhs; + std::vector< Node > subs_rhs; + //get outer variable substitution + Assert( d_ask_types_index[q].size()==d_ask_types[q].size() ); + for( unsigned j=0; j<d_ask_types_index[q].size(); j++ ){ + Trace("anti-sk-debug") << " o_subs : " << d_quant_sip[q].d_si_vars[d_ask_types_index[q][j]] << " -> " << outer_vars[j] << std::endl; + subs_lhs.push_back( d_quant_sip[q].d_si_vars[d_ask_types_index[q][j]] ); + subs_rhs.push_back( outer_vars[j] ); + } + //get function substitution + for( std::map< Node, bool >::iterator it = d_quant_sip[q].d_funcs.begin(); it != d_quant_sip[q].d_funcs.end(); ++it ){ + Node f = it->first; + Node fv = d_quant_sip[q].d_func_fo_var[it->first]; + if( func_to_var.find( f )==func_to_var.end() ){ + Node v = NodeManager::currentNM()->mkBoundVar( fv.getType() ); + Trace("anti-sk-debug") << "Inner var for " << f << " : " << v << std::endl; + inner_vars.push_back( v ); + func_to_var[f] = v; + } + subs_lhs.push_back( fv ); + subs_rhs.push_back( func_to_var[f] ); + Trace("anti-sk-debug") << " i_subs : " << fv << " -> " << func_to_var[f] << std::endl; + } + Node c = d_quant_sip[q].getSingleInvocation(); + if( !subs_lhs.empty() ){ + c = c.substitute( subs_lhs.begin(), subs_lhs.end(), subs_rhs.begin(), subs_rhs.end() ); + } + conj.push_back( c ); + } + Node body = conj.size()==1 ? conj[0] : NodeManager::currentNM()->mkNode( kind::AND, conj ); + if( !inner_vars.empty() ){ + Node bvl = NodeManager::currentNM()->mkNode( kind::BOUND_VAR_LIST, inner_vars ); + body = NodeManager::currentNM()->mkNode( kind::EXISTS, bvl, body ); + } + if( !outer_vars.empty() ){ + Node bvl = NodeManager::currentNM()->mkNode( kind::BOUND_VAR_LIST, outer_vars ); + body = NodeManager::currentNM()->mkNode( kind::FORALL, bvl, body ); + } + Trace("anti-sk") << "Produced : " << body << std::endl; + quants.push_back( body.negate() ); + Node lem = NodeManager::currentNM()->mkNode( kind::AND, quants ).negate(); + Trace("anti-sk-lemma") << "Anti-skolemize lemma : " << lem << std::endl; + quants.pop_back(); + return d_quantEngine->addLemma( lem ); + }else{ + return false; + } +} + diff --git a/src/theory/quantifiers/anti_skolem.h b/src/theory/quantifiers/anti_skolem.h new file mode 100644 index 000000000..cf24e2751 --- /dev/null +++ b/src/theory/quantifiers/anti_skolem.h @@ -0,0 +1,75 @@ +/********************* */ +/*! \file anti_skolem.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_ANTI_SKOLEM_H +#define __CVC4__THEORY__QUANT_ANTI_SKOLEM_H + +#include "theory/quantifiers_engine.h" +#include "context/cdo.h" +#include "theory/quantifiers/ce_guided_single_inv.h" + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +class QuantAntiSkolem : public QuantifiersModule { + typedef context::CDHashSet<Node, NodeHashFunction> NodeSet; +private: + std::map< Node, bool > d_quant_processed; + std::map< Node, SingleInvocationPartition > d_quant_sip; + std::map< Node, std::vector< TypeNode > > d_ask_types; + std::map< Node, std::vector< unsigned > > d_ask_types_index; + + class SkQuantTypeCache { + public: + std::map< TypeNode, SkQuantTypeCache > d_children; + std::vector< Node > d_quants; + void add( std::vector< TypeNode >& typs, Node q, unsigned index = 0 ); + void clear() { + d_children.clear(); + d_quants.clear(); + } + void sendLemmas( QuantAntiSkolem * ask ); + }; + SkQuantTypeCache d_sqtc; + + class CDSkQuantCache { + public: + CDSkQuantCache( context::Context* c ) : d_valid( c, false ){} + std::map< Node, CDSkQuantCache* > d_data; + context::CDO< bool > d_valid; + bool add( context::Context* c, std::vector< Node >& quants, unsigned index = 0 ); + }; + CDSkQuantCache * d_sqc; +public: + bool sendAntiSkolemizeLemma( std::vector< Node >& quants, bool pconnected = true ); +public: + QuantAntiSkolem( QuantifiersEngine * qe ); + + /* 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 "QuantAntiSkolem"; } +}; + +} +} +} + +#endif diff --git a/src/theory/quantifiers/ce_guided_single_inv.cpp b/src/theory/quantifiers/ce_guided_single_inv.cpp index 7ef23077f..80585a33d 100644 --- a/src/theory/quantifiers/ce_guided_single_inv.cpp +++ b/src/theory/quantifiers/ce_guided_single_inv.cpp @@ -149,8 +149,7 @@ void CegConjectureSingleInv::initialize( Node q ) { bool singleInvocation = true; if( type_valid==0 ){ //process the single invocation-ness of the property - d_sip->init( types ); - d_sip->process( qq ); + d_sip->init( types, qq ); Trace("cegqi-si") << "- Partitioned to single invocation parts : " << std::endl; d_sip->debugPrint( "cegqi-si" ); //map from program to bound variables @@ -839,7 +838,41 @@ void CegConjectureSingleInv::preregisterConjecture( Node q ) { d_orig_conjecture = q; } -void SingleInvocationPartition::init( std::vector< TypeNode >& typs ){ +bool SingleInvocationPartition::init( Node n ) { + //first, get types of arguments for functions + std::vector< TypeNode > typs; + std::map< Node, bool > visited; + if( inferArgTypes( n, typs, visited ) ){ + return init( typs, n ); + }else{ + return false; + } +} + +bool SingleInvocationPartition::inferArgTypes( Node n, std::vector< TypeNode >& typs, std::map< Node, bool >& visited ) { + if( visited.find( n )==visited.end() ){ + visited[n] = true; + if( n.getKind()!=FORALL ){ + //if( TermDb::hasBoundVarAttr( n ) ){ + if( n.getKind()==APPLY_UF ){ + for( unsigned i=0; i<n.getNumChildren(); i++ ){ + typs.push_back( n[i].getType() ); + } + return true; + }else{ + for( unsigned i=0; i<n.getNumChildren(); i++ ){ + if( inferArgTypes( n[i], typs, visited ) ){ + return true; + } + } + } + //} + } + } + return false; +} + +bool SingleInvocationPartition::init( std::vector< TypeNode >& typs, Node n ){ Assert( d_arg_types.empty() ); Assert( d_si_vars.empty() ); d_arg_types.insert( d_arg_types.end(), typs.begin(), typs.end() ); @@ -849,6 +882,8 @@ void SingleInvocationPartition::init( std::vector< TypeNode >& typs ){ Node si_v = NodeManager::currentNM()->mkBoundVar( ss.str(), d_arg_types[j] ); d_si_vars.push_back( si_v ); } + process( n ); + return true; } @@ -984,43 +1019,45 @@ bool SingleInvocationPartition::processConjunct( Node n, std::map< Node, bool >& return true; }else{ bool ret = true; - for( unsigned i=0; i<n.getNumChildren(); i++ ){ - if( !processConjunct( n[i], visited, args, terms, subs ) ){ - ret = false; + //if( TermDb::hasBoundVarAttr( n ) ){ + for( unsigned i=0; i<n.getNumChildren(); i++ ){ + if( !processConjunct( n[i], visited, args, terms, subs ) ){ + ret = false; + } } - } - if( ret ){ - if( n.getKind()==APPLY_UF ){ - if( std::find( terms.begin(), terms.end(), n )==terms.end() ){ - Node f = n.getOperator(); - //check if it matches the type requirement - if( isAntiSkolemizableType( f ) ){ - if( args.empty() ){ - //record arguments - for( unsigned i=0; i<n.getNumChildren(); i++ ){ - args.push_back( n[i] ); - } - }else{ - //arguments must be the same as those already recorded - for( unsigned i=0; i<n.getNumChildren(); i++ ){ - if( args[i]!=n[i] ){ - Trace("si-prt-debug") << "...bad invocation : " << n << " at arg " << i << "." << std::endl; - ret = false; - break; + if( ret ){ + if( n.getKind()==APPLY_UF ){ + if( std::find( terms.begin(), terms.end(), n )==terms.end() ){ + Node f = n.getOperator(); + //check if it matches the type requirement + if( isAntiSkolemizableType( f ) ){ + if( args.empty() ){ + //record arguments + for( unsigned i=0; i<n.getNumChildren(); i++ ){ + args.push_back( n[i] ); + } + }else{ + //arguments must be the same as those already recorded + for( unsigned i=0; i<n.getNumChildren(); i++ ){ + if( args[i]!=n[i] ){ + Trace("si-prt-debug") << "...bad invocation : " << n << " at arg " << i << "." << std::endl; + ret = false; + break; + } } } + if( ret ){ + terms.push_back( n ); + subs.push_back( d_func_inv[f] ); + } + }else{ + Trace("si-prt-debug") << "... " << f << " is a bad operator." << std::endl; + ret = false; } - if( ret ){ - terms.push_back( n ); - subs.push_back( d_func_inv[f] ); - } - }else{ - Trace("si-prt-debug") << "... " << f << " is a bad operator." << std::endl; - ret = false; } } } - } + //} visited[n] = ret; return ret; } @@ -1037,6 +1074,7 @@ bool SingleInvocationPartition::isAntiSkolemizableType( Node f ) { ret = true; std::vector< Node > children; children.push_back( f ); + //TODO: permutations of arguments for( unsigned i=0; i<d_arg_types.size(); i++ ){ children.push_back( d_si_vars[i] ); if( tn[i]!=d_arg_types[i] ){ diff --git a/src/theory/quantifiers/ce_guided_single_inv.h b/src/theory/quantifiers/ce_guided_single_inv.h index c414a51bd..fe48a0dc3 100644 --- a/src/theory/quantifiers/ce_guided_single_inv.h +++ b/src/theory/quantifiers/ce_guided_single_inv.h @@ -153,18 +153,19 @@ public: class SingleInvocationPartition { private: + bool inferArgTypes( Node n, std::vector< TypeNode >& typs, std::map< Node, bool >& visited ); + void process( Node n ); bool collectConjuncts( Node n, bool pol, std::vector< Node >& conj ); bool processConjunct( Node n, std::map< Node, bool >& visited, std::vector< Node >& args, std::vector< Node >& terms, std::vector< Node >& subs ); Node getSpecificationInst( Node n, std::map< Node, Node >& lam, std::map< Node, Node >& visited ); void extractInvariant2( Node n, Node& func, int& pol, std::vector< Node >& disjuncts, bool hasPol, std::map< Node, bool >& visited ); public: - void init( std::vector< TypeNode >& typs ); - //inputs - void process( Node n ); - std::vector< TypeNode > d_arg_types; + bool init( Node n ); + bool init( std::vector< TypeNode >& typs, Node n ); //outputs (everything is with bound var) + std::vector< TypeNode > d_arg_types; std::map< Node, bool > d_funcs; std::map< Node, Node > d_func_inv; std::map< Node, Node > d_inv_to_func; @@ -187,6 +188,8 @@ public: void extractInvariant( Node n, Node& func, int& pol, std::vector< Node >& disjuncts ); + bool isPurelySingleInvocation() { return d_conjuncts[1].empty(); } + void debugPrint( const char * c ); }; diff --git a/src/theory/quantifiers/quant_split.cpp b/src/theory/quantifiers/quant_split.cpp index 1ae1c3c5f..bff429e7c 100644 --- a/src/theory/quantifiers/quant_split.cpp +++ b/src/theory/quantifiers/quant_split.cpp @@ -9,7 +9,7 @@ ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** - ** \brief Implementation of local theory ext utilities + ** \brief Implementation of dynamic quantifiers splitting **/ #include "theory/quantifiers/quant_split.h" |