From beaf8b212dfadb47328942c23a7649ab44a014cb Mon Sep 17 00:00:00 2001 From: ajreynol Date: Tue, 24 May 2016 18:18:00 -0500 Subject: [PATCH] Improvements to symmetry breaking in sygus search. Minor fix for getting instantiations of non-registered quantifiers in sygus. --- src/options/quantifiers_options | 2 + src/theory/datatypes/datatypes_sygus.cpp | 291 ++++++++++++------ .../quantifiers/quantifiers_rewriter.cpp | 3 +- src/theory/quantifiers_engine.cpp | 9 +- 4 files changed, 214 insertions(+), 91 deletions(-) diff --git a/src/options/quantifiers_options b/src/options/quantifiers_options index 456ab04c2..980179378 100644 --- a/src/options/quantifiers_options +++ b/src/options/quantifiers_options @@ -54,6 +54,8 @@ option purifyQuant --purify-quant bool :default false purify quantified formulas option elimExtArithQuant --elim-ext-arith-quant bool :default true eliminate extended arithmetic symbols in quantified formulas +option condRewriteQuant --cond-rewrite-quant bool :default true + conditional rewriting of quantified formulas #### E-matching options diff --git a/src/theory/datatypes/datatypes_sygus.cpp b/src/theory/datatypes/datatypes_sygus.cpp index b32a70212..4514453db 100644 --- a/src/theory/datatypes/datatypes_sygus.cpp +++ b/src/theory/datatypes/datatypes_sygus.cpp @@ -402,6 +402,60 @@ void SygusSplit::registerSygusTypeConstructorArg( TypeNode tnn, const Datatype& } } +class ReqTrie { +public: + ReqTrie() : d_req_kind( UNDEFINED_KIND ){} + std::map< unsigned, ReqTrie > d_children; + Kind d_req_kind; + TypeNode d_req_type; + Node d_req_const; + void print( const char * c, int indent = 0 ){ + if( d_req_kind!=UNDEFINED_KIND ){ + Trace(c) << d_req_kind << " "; + }else if( !d_req_type.isNull() ){ + Trace(c) << d_req_type; + }else if( !d_req_const.isNull() ){ + Trace(c) << d_req_const; + }else{ + Trace(c) << "_"; + } + Trace(c) << std::endl; + for( std::map< unsigned, ReqTrie >::iterator it = d_children.begin(); it != d_children.end(); ++it ){ + for( int i=0; i<=indent; i++ ) { Trace(c) << " "; } + Trace(c) << it->first << " : "; + it->second.print( c, indent+1 ); + } + } + bool satisfiedBy( quantifiers::TermDbSygus * tdb, TypeNode tn ){ + if( d_req_kind!=UNDEFINED_KIND ){ + int c = tdb->getKindArg( tn, d_req_kind ); + if( c!=-1 ){ + const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype(); + for( std::map< unsigned, ReqTrie >::iterator it = d_children.begin(); it != d_children.end(); ++it ){ + if( it->firstgetArgType( dt[c], it->first ); + if( !it->second.satisfiedBy( tdb, tnc ) ){ + return false; + } + }else{ + return false; + } + } + return true; + }else{ + return false; + } + }else if( !d_req_const.isNull() ){ + return tdb->hasConst( tn, d_req_const ); + }else if( !d_req_type.isNull() ){ + return tn==d_req_type; + }else{ + return true; + } + } +}; + + //this function gets all easy redundant cases, before consulting rewriters bool SygusSplit::considerSygusSplitKind( const Datatype& dt, const Datatype& pdt, TypeNode tn, TypeNode tnp, Kind k, Kind parent, int arg ) { Assert( d_tds->hasKind( tn, k ) ); @@ -419,107 +473,168 @@ bool SygusSplit::considerSygusSplitKind( const Datatype& dt, const Datatype& pdt return arg==firstArg; } } - //push - if( parent==NOT || parent==BITVECTOR_NOT || parent==UMINUS || parent==BITVECTOR_NEG || k==ITE ){ - //negation normal form - if( parent==k && isArgDatatype( dt[c], 0, pdt ) ){ - return false; - } - Kind nk = UNDEFINED_KIND; - Kind reqk = UNDEFINED_KIND; //required kind for all children - std::map< unsigned, Kind > reqkc; //required kind for some children - if( parent==NOT ){ - if( k==AND ) { - nk = OR;reqk = NOT; - }else if( k==OR ){ - nk = AND;reqk = NOT; - }else if( k==IFF ) { - nk = XOR; - }else if( k==XOR ) { - nk = IFF; - } - }else if( parent==BITVECTOR_NOT ){ - if( k==BITVECTOR_AND ) { - nk = BITVECTOR_OR;reqk = BITVECTOR_NOT; - }else if( k==BITVECTOR_OR ){ - nk = BITVECTOR_AND;reqk = BITVECTOR_NOT; - }else if( k==BITVECTOR_XNOR ) { - nk = BITVECTOR_XOR; - }else if( k==BITVECTOR_XOR ) { - nk = BITVECTOR_XNOR; - } - }else if( parent==UMINUS ){ - if( k==PLUS ){ - nk = PLUS;reqk = UMINUS; - } - }else if( parent==BITVECTOR_NEG ){ - if( k==PLUS ){ - nk = PLUS;reqk = BITVECTOR_NEG; - } - }else if( k==ITE ){ - //ITE lifting - if( parent!=ITE ){ - nk = ITE; - reqkc[1] = parent; - reqkc[2] = parent; - } - } - if( nk!=UNDEFINED_KIND ){ - Trace("sygus-split-debug") << "Push " << parent << " over " << k << " to " << nk; - if( reqk!=UNDEFINED_KIND ){ - Trace("sygus-split-debug") << ", reqk = " << reqk; + //describes the shape of an alternate term to construct + // we check whether this term is in the sygus grammar below + ReqTrie rt; + bool rt_valid = false; + + //construct rt by cases + if( parent==NOT || parent==BITVECTOR_NOT || parent==UMINUS || parent==BITVECTOR_NEG ){ + rt_valid = true; + //negation normal form + if( parent==k ){ + rt.d_req_type = d_tds->getArgType( dt[c], 0 ); + }else{ + Kind reqk = UNDEFINED_KIND; //required kind for all children + std::map< unsigned, Kind > reqkc; //required kind for some children + if( parent==NOT ){ + if( k==AND ) { + rt.d_req_kind = OR;reqk = NOT; + }else if( k==OR ){ + rt.d_req_kind = AND;reqk = NOT; + }else if( k==IFF ) { + rt.d_req_kind = XOR; + }else if( k==XOR ) { + rt.d_req_kind = IFF; + }else if( k==ITE ){ + rt.d_req_kind = ITE;reqkc[1] = NOT;reqkc[2] = NOT; + rt.d_children[0].d_req_type = d_tds->getArgType( dt[c], 0 ); + }else if( k==LEQ || k==GT ){ + // (not (~ x y)) -----> (~ (+ y 1) x) + rt.d_req_kind = k; + rt.d_children[0].d_req_kind = PLUS; + rt.d_children[0].d_children[0].d_req_type = d_tds->getArgType( dt[c], 1 ); + rt.d_children[0].d_children[1].d_req_const = NodeManager::currentNM()->mkConst( Rational( 1 ) ); + rt.d_children[1].d_req_type = d_tds->getArgType( dt[c], 0 ); + //TODO: other possibilities? + }else if( k==LT || k==GEQ ){ + // (not (~ x y)) -----> (~ y (+ x 1)) + rt.d_req_kind = k; + rt.d_children[0].d_req_type = d_tds->getArgType( dt[c], 1 ); + rt.d_children[1].d_req_kind = PLUS; + rt.d_children[1].d_children[0].d_req_type = d_tds->getArgType( dt[c], 0 ); + rt.d_children[1].d_children[1].d_req_const = NodeManager::currentNM()->mkConst( Rational( 1 ) ); + }else{ + rt_valid = false; + } + }else if( parent==BITVECTOR_NOT ){ + if( k==BITVECTOR_AND ) { + rt.d_req_kind = BITVECTOR_OR;reqk = BITVECTOR_NOT; + }else if( k==BITVECTOR_OR ){ + rt.d_req_kind = BITVECTOR_AND;reqk = BITVECTOR_NOT; + }else if( k==BITVECTOR_XNOR ) { + rt.d_req_kind = BITVECTOR_XOR; + }else if( k==BITVECTOR_XOR ) { + rt.d_req_kind = BITVECTOR_XNOR; + }else{ + rt_valid = false; + } + }else if( parent==UMINUS ){ + if( k==PLUS ){ + rt.d_req_kind = PLUS;reqk = UMINUS; + }else{ + rt_valid = false; + } + }else if( parent==BITVECTOR_NEG ){ + if( k==PLUS ){ + rt.d_req_kind = PLUS;reqk = BITVECTOR_NEG; + }else{ + rt_valid = false; + } } - Trace("sygus-split-debug") << "?" << std::endl; - int pcr = d_tds->getKindArg( tnp, nk ); - if( pcr!=-1 ){ - Assert( pcr<(int)pdt.getNumConstructors() ); - if( reqk!=UNDEFINED_KIND || !reqkc.empty() ){ + if( rt_valid && ( reqk!=UNDEFINED_KIND || !reqkc.empty() ) ){ + int pcr = d_tds->getKindArg( tnp, rt.d_req_kind ); + if( pcr!=-1 ){ + Assert( pcr<(int)pdt.getNumConstructors() ); //must have same number of arguments if( pdt[pcr].getNumArgs()==dt[c].getNumArgs() ){ for( unsigned i=0; igetArgType( pdt[pcr], i ); - Assert( datatypes::DatatypesRewriter::isTypeDatatype( tna ) ); - std::vector< Kind > rks; - if( reqk!=UNDEFINED_KIND ){ - rks.push_back( reqk ); - } - std::map< unsigned, Kind >::iterator itr = reqkc.find( i ); - if( itr!=reqkc.end() ){ - rks.push_back( itr->second ); - } - for( unsigned j=0; jgetKindArg( tna, rkc ); - if( nindex!=-1 ){ - const Datatype& adt = ((DatatypeType)(tn).toType()).getDatatype(); - if( d_tds->getArgType( dt[c], i )!=d_tds->getArgType( adt[nindex], 0 ) ){ - Trace("sygus-split-debug") << "...arg " << i << " type mismatch." << std::endl; - return true; - } - }else{ - Trace("sygus-split-debug") << "...argument " << i << " does not have " << rkc << "." << std::endl; - return true; + Kind rk = reqk; + if( reqk==UNDEFINED_KIND ){ + std::map< unsigned, Kind >::iterator itr = reqkc.find( i ); + if( itr!=reqkc.end() ){ + rk = itr->second; } } + if( rk!=UNDEFINED_KIND ){ + rt.d_children[i].d_req_kind = rk; + rt.d_children[i].d_children[0].d_req_type = d_tds->getArgType( dt[c], i ); + } } - Trace("sygus-split-debug") << "...success" << std::endl; - return false; }else{ - Trace("sygus-split-debug") << "...#arg mismatch." << std::endl; + rt_valid = false; } }else{ - return !isTypeMatch( pdt[pcr], dt[c] ); + rt_valid = false; } - }else{ - Trace("sygus-split-debug") << "...operator not available." << std::endl; } } + }else if( k==MINUS || k==BITVECTOR_SUB ){ + if( parent==EQUAL || + parent==MINUS || parent==BITVECTOR_SUB || + parent==LEQ || parent==LT || parent==GEQ || parent==GT ){ + int oarg = arg==0 ? 1 : 0; + // (~ x (- y z)) ----> (~ (+ x z) y) + // (~ (- y z) x) ----> (~ y (+ x z)) + rt.d_req_kind = parent; + rt.d_children[arg].d_req_type = d_tds->getArgType( dt[c], 0 ); + rt.d_children[oarg].d_req_kind = k==MINUS ? PLUS : BITVECTOR_PLUS; + rt.d_children[oarg].d_children[0].d_req_type = d_tds->getArgType( pdt[pc], oarg ); + rt.d_children[oarg].d_children[1].d_req_type = d_tds->getArgType( dt[c], 1 ); + rt_valid = true; + }else if( parent==PLUS || parent==BITVECTOR_PLUS ){ + // (+ x (- y z)) -----> (- (+ x y) z) + // (+ (- y z) x) -----> (- (+ x y) z) + rt.d_req_kind = parent==PLUS ? MINUS : BITVECTOR_SUB; + int oarg = arg==0 ? 1 : 0; + rt.d_children[0].d_req_kind = parent; + rt.d_children[0].d_children[0].d_req_type = d_tds->getArgType( pdt[pc], oarg ); + rt.d_children[0].d_children[1].d_req_type = d_tds->getArgType( dt[c], 0 ); + rt.d_children[1].d_req_type = d_tds->getArgType( dt[c], 1 ); + rt_valid = true; + } + }else if( k==ITE ){ + if( parent!=ITE ){ + // (o X (ite y z w) X') -----> (ite y (o X z X') (o X w X')) + rt.d_req_kind = ITE; + rt.d_children[0].d_req_type = d_tds->getArgType( dt[c], 0 ); + unsigned n_args = pdt[pc].getNumArgs(); + for( unsigned r=1; r<=2; r++ ){ + rt.d_children[r].d_req_kind = parent; + for( unsigned q=0; qgetArgType( dt[c], r ); + }else{ + rt.d_children[r].d_children[q].d_req_type = d_tds->getArgType( pdt[pc], q ); + } + } + } + rt_valid = true; + //TODO: this increases term size but is probably a good idea + } + }else if( k==NOT ){ + if( parent==ITE ){ + // (ite (not y) z w) -----> (ite y w z) + rt.d_req_kind = ITE; + rt.d_children[0].d_req_type = d_tds->getArgType( dt[c], 0 ); + rt.d_children[1].d_req_type = d_tds->getArgType( pdt[pc], 2 ); + rt.d_children[2].d_req_type = d_tds->getArgType( pdt[pc], 1 ); + } } - if( parent==MINUS || parent==BITVECTOR_SUB ){ - - + Trace("sygus-consider-split") << "Consider sygus split kind " << k << ", parent = " << parent << ", arg = " << arg << "?" << std::endl; + if( rt_valid ){ + rt.print("sygus-consider-split"); + //check if it meets the requirements + if( rt.satisfiedBy( d_tds, tnp ) ){ + Trace("sygus-consider-split") << "...success!" << std::endl; + //do not need to consider the kind in the search since there are ways to construct equivalent terms + return false; + }else{ + Trace("sygus-consider-split") << "...failed." << std::endl; + } + Trace("sygus-consider-split") << std::endl; } + //must consider this kind in the search return true; } @@ -622,6 +737,7 @@ bool SygusSplit::isGenericRedundant( TypeNode tn, Node g, bool active ) { d_gen_terms[tn][gr] = g; d_gen_terms_inactive[tn][gr] = g; Trace("sygus-gnf-debug") << "...not redundant." << std::endl; + Trace("sygus-nf-reg") << "*** Sygus (generic) normal form : normal form of " << g << " is " << gr << std::endl; }else{ Trace("sygus-gnf-debug") << "...redundant." << std::endl; Trace("sygus-nf") << "* Sygus normal form : simplify since " << g << " and " << itg->second << " both rewrite to " << gr << std::endl; @@ -855,6 +971,7 @@ bool SygusSymBreak::processCurrentProgram( Node a, TypeNode at, int depth, Node }else{ d_redundant[at][prog] = false; red = false; + Trace("sygus-nf-reg") << "*** Sygus normal form : normal form of " << prog << " is " << progr << std::endl; } }else{ rep_prog = itnp->second; @@ -864,6 +981,7 @@ bool SygusSymBreak::processCurrentProgram( Node a, TypeNode at, int depth, Node d_redundant[at].erase( rep_prog ); d_redundant[at][prog] = false; red = false; + Trace("sygus-nf-reg") << "*** Sygus normal form : normal form of " << prog << " is " << progr << " (redundant but smaller than " << rep_prog << ") " << std::endl; }else{ Assert( prog!=itnp->second ); d_redundant[at][prog] = true; @@ -1096,6 +1214,7 @@ bool SygusSymBreak::processCurrentProgram( Node a, TypeNode at, int depth, Node } }else{ red = it->second; + Trace("sygus-nf-debug") << "Already processed, redundant : " << red << std::endl; } if( red ){ if( std::find( d_lemmas_reported[at][prog].begin(), d_lemmas_reported[at][prog].end(), a )==d_lemmas_reported[at][prog].end() ){ diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index b51e7d971..511337b40 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -1542,8 +1542,7 @@ bool QuantifiersRewriter::doOperation( Node q, int computeOption, QAttributes& q }else if( computeOption==COMPUTE_NNF ){ return true; }else if( computeOption==COMPUTE_PROCESS_TERMS ){ - return true; - //return options::iteLiftQuant()!=ITE_LIFT_QUANT_MODE_NONE || options::iteCondVarSplitQuant(); + return options::condRewriteQuant(); }else if( computeOption==COMPUTE_COND_SPLIT ){ return ( options::iteDtTesterSplitQuant() || options::condVarSplitQuant() ) && !is_strict_trigger; }else if( computeOption==COMPUTE_PRENEX ){ diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index ebf89c0b8..8b51e94b5 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -641,6 +641,7 @@ bool QuantifiersEngine::registerQuantifier( Node f ){ d_term_db->makeInstantiationConstantsFor( f ); d_term_db->computeAttributes( f ); for( unsigned i=0; iidentify() << "..." << std::endl; d_modules[i]->preRegisterQuantifier( f ); } QuantifiersModule * qm = getOwner( f ); @@ -653,6 +654,7 @@ bool QuantifiersEngine::registerQuantifier( Node f ){ } //register with each module for( unsigned i=0; iidentify() << "..." << std::endl; d_modules[i]->registerQuantifier( f ); } //TODO: remove this @@ -886,9 +888,9 @@ Node QuantifiersEngine::getSubstitute( Node n, std::vector< Node >& terms ){ Node QuantifiersEngine::getInstantiation( Node q, std::vector< Node >& vars, std::vector< Node >& terms, bool doVts ){ Node body; + Assert( vars.size()==terms.size() ); //process partial instantiation if necessary - if( d_term_db->d_vars[q].size()!=vars.size() ){ - Assert( vars.size()==terms.size() ); + if( q[0].getNumChildren()!=vars.size() ){ body = q[ 1 ].substitute( vars.begin(), vars.end(), terms.begin(), terms.end() ); std::vector< Node > uninst_vars; //doing a partial instantiation, must add quantifier for all uninstantiated variables @@ -897,13 +899,14 @@ Node QuantifiersEngine::getInstantiation( Node q, std::vector< Node >& vars, std uninst_vars.push_back( q[0][i] ); } } + Trace("partial-inst") << "Partially instantiating with " << vars.size() << " / " << q[0].getNumChildren() << " for " << q << std::endl; + Assert( !uninst_vars.empty() ); Node bvl = NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, uninst_vars ); body = NodeManager::currentNM()->mkNode( FORALL, bvl, body ); Trace("partial-inst") << "Partial instantiation : " << q << std::endl; Trace("partial-inst") << " : " << body << std::endl; }else{ if( options::cbqi() ){ - Assert( vars.size()==terms.size() ); body = q[ 1 ].substitute( vars.begin(), vars.end(), terms.begin(), terms.end() ); }else{ //do optimized version -- 2.30.2