summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/quantifiers')
-rw-r--r--src/theory/quantifiers/anti_skolem.cpp269
-rw-r--r--src/theory/quantifiers/anti_skolem.h75
-rw-r--r--src/theory/quantifiers/ce_guided_single_inv.cpp104
-rw-r--r--src/theory/quantifiers/ce_guided_single_inv.h11
-rw-r--r--src/theory/quantifiers/quant_split.cpp2
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"
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback