From b6f57c4a9df8f6c17e30168f1f1961b76f83702e Mon Sep 17 00:00:00 2001 From: ajreynol Date: Sat, 31 Jan 2015 11:12:09 +0100 Subject: [PATCH] Lemmas instead of conflicts in sygus sym break (do not expand explanations). Minor improvements to sygus splitting. --- src/theory/datatypes/datatypes_sygus.cpp | 159 ++++++++++++++---- src/theory/datatypes/datatypes_sygus.h | 29 ++-- src/theory/datatypes/theory_datatypes.cpp | 23 ++- .../quantifiers/ce_guided_instantiation.cpp | 21 ++- 4 files changed, 171 insertions(+), 61 deletions(-) diff --git a/src/theory/datatypes/datatypes_sygus.cpp b/src/theory/datatypes/datatypes_sygus.cpp index 3063e85bb..353bd1392 100644 --- a/src/theory/datatypes/datatypes_sygus.cpp +++ b/src/theory/datatypes/datatypes_sygus.cpp @@ -56,11 +56,13 @@ void SygusSplit::getSygusSplits( Node n, const Datatype& dt, std::vector< Node > //register the constructors that are redundant children of argument sIndex of constructor index csIndex of dt registerSygusTypeConstructorArg( tnn, dt, tnnp, pdt, csIndex, sIndex ); - if( options::sygusNormalFormArg() && sIndex==1 && pdt[csIndex].getNumArgs()==2 ){ - arg1 = NodeManager::currentNM()->mkNode( APPLY_SELECTOR_TOTAL, Node::fromExpr( pdt[csIndex][0].getSelector() ), n[0] ); - tn1 = arg1.getType(); - if( !DatatypesRewriter::isTypeDatatype( tn1 ) ){ - arg1 = Node::null(); + if( options::sygusNormalFormArg() ){ + if( sIndex==1 && pdt[csIndex].getNumArgs()==2 ){ + arg1 = NodeManager::currentNM()->mkNode( APPLY_SELECTOR_TOTAL, Node::fromExpr( pdt[csIndex][0].getSelector() ), n[0] ); + tn1 = arg1.getType(); + if( !DatatypesRewriter::isTypeDatatype( tn1 ) ){ + arg1 = Node::null(); + } } } // we are splitting on a term that may later have no semantics : guard this case @@ -99,6 +101,21 @@ void SygusSplit::getSygusSplits( Node n, const Datatype& dt, std::vector< Node > narrow = true; } } + //other constraints on arguments + Kind curr = d_util->getArgKind( tnn, i ); + if( curr!=UNDEFINED_KIND ){ + //ITE children must be distinct when properly typed + if( curr==ITE ){ + if( getArgType( dt[i], 1 )==tnn && getArgType( dt[i], 2 )==tnn ){ + Node arg_ite1 = NodeManager::currentNM()->mkNode( APPLY_SELECTOR_TOTAL, Node::fromExpr( dt[i][1].getSelector() ), n ); + Node arg_ite2 = NodeManager::currentNM()->mkNode( APPLY_SELECTOR_TOTAL, Node::fromExpr( dt[i][2].getSelector() ), n ); + Node deq = arg_ite1.eqNode( arg_ite2 ).negate(); + Trace("sygus-str") << "...ite strengthen " << deq << std::endl; + test_c.push_back( deq ); + narrow = true; + } + } + } //add fairness constraint if( options::ceGuidedInstFair()==quantifiers::CEGQI_FAIR_DT_SIZE ){ Node szl = NodeManager::currentNM()->mkNode( DT_SIZE, n ); @@ -218,16 +235,11 @@ void SygusSplit::registerSygusTypeConstructorArg( TypeNode tnn, const Datatype& }else{ // calculate which constructors we should consider based on normal form for terms //get parent kind - bool hasParentKind = false; - Kind parentKind; - if( d_util->isKindArg( tnnp, csIndex ) ){ - hasParentKind = true; - parentKind = d_util->d_arg_kind[tnnp][csIndex]; - } + Kind parentKind = d_util->getArgKind( tnnp, csIndex ); for( unsigned i=0; id_arg_kind.find( tnn )!=d_util->d_arg_kind.end() && d_util->d_arg_kind[tnn].find( i )!=d_util->d_arg_kind[tnn].end() ){ addSplit = considerSygusSplitKind( dt, pdt, tnn, tnnp, d_util->d_arg_kind[tnn][i], parentKind, sIndex ); if( !addSplit ){ @@ -257,7 +269,7 @@ void SygusSplit::registerSygusTypeConstructorArg( TypeNode tnn, const Datatype& d_sygus_pc_nred[tnn][csIndex][sIndex].push_back( addSplit ); } //compute argument relationships for 2-arg constructors - if( d_util->isKindArg( tnnp, csIndex ) && pdt[csIndex].getNumArgs()==2 ){ + if( parentKind!=UNDEFINED_KIND && pdt[csIndex].getNumArgs()==2 ){ int osIndex = sIndex==0 ? 1 : 0; TypeNode tnno = getArgType( pdt[csIndex], osIndex ); if( DatatypesRewriter::isTypeDatatype( tnno ) ){ @@ -268,7 +280,6 @@ void SygusSplit::registerSygusTypeConstructorArg( TypeNode tnn, const Datatype& Assert( d_sygus_pc_nred[tnn][csIndex].find( sIndex )!=d_sygus_pc_nred[tnn][csIndex].end() ); Assert( d_sygus_pc_nred[tnno][csIndex].find( osIndex )!=d_sygus_pc_nred[tnno][csIndex].end() ); - Kind parentKind = d_util->d_arg_kind[tnnp][csIndex]; bool isPComm = d_util->isComm( parentKind ); std::map< int, bool > larg_consider; for( unsigned i=0; ihasOffsetArg( parent, arg, offset, ok ) ){ + Trace("sygus-split-debug") << parent << " has offset arg " << ok << " " << offset << std::endl; + int ok_arg = d_util->getKindArg( tnp, ok ); + if( ok_arg!=-1 ){ + Trace("sygus-split-debug") << "...at argument " << ok_arg << std::endl; + //other operator be the same type + if( isTypeMatch( pdt[ok_arg], pdt[arg] ) ){ + Node co = d_util->getTypeValueOffset( c.getType(), c, offset ); + Trace("sygus-split-debug") << c << " with offset " << offset << " is " << co << std::endl; + if( !co.isNull() ){ + if( d_util->hasConst( tn, co ) ){ + Trace("sygus-split-debug") << "arg " << arg << " " << c << " in " << parent << " can be treated as " << co << " in " << ok << "..." << std::endl; + return false; + }else{ + Trace("sygus-split-debug") << "Type does not have constant." << std::endl; + } + } + }else{ + Trace("sygus-split-debug") << "Type mismatch." << std::endl; + } + } + } + } return true; } @@ -507,6 +544,19 @@ TypeNode SygusSplit::getArgType( const DatatypeConstructor& c, int i ) { return TypeNode::fromType( ((SelectorType)c[i].getType()).getRangeType() ); } +bool SygusSplit::isTypeMatch( const DatatypeConstructor& c1, const DatatypeConstructor& c2 ){ + if( c1.getNumArgs()!=c2.getNumArgs() ){ + return false; + }else{ + for( unsigned i=0; i::iterator it = d_gen_redundant[tn].find( g ); @@ -707,6 +757,7 @@ Node SygusSymBreak::ProgSearch::getCandidateProgramAtDepth( int depth, Node prog bool SygusSymBreak::processCurrentProgram( Node a, TypeNode at, int depth, Node prog, std::vector< Node >& testers, std::map< Node, std::vector< Node > >& testers_u ) { Assert( a.getType()==at ); + //Assert( !d_util->d_conflict ); std::map< Node, bool >::iterator it = d_redundant[at].find( prog ); bool red; if( it==d_redundant[at].end() ){ @@ -799,14 +850,14 @@ bool SygusSymBreak::processCurrentProgram( Node a, TypeNode at, int depth, Node for( unsigned i=0; i " << rl << std::endl; - d_conflict_gen[at][prog].push_back( rl ); + d_lemma_gen[at][prog].push_back( rl ); } } } } if( !conflict_gen_set ){ for( unsigned i=0; isecond; } if( red ){ - Assert( d_conflict_gen[at][prog].size()==testers.size() ); - std::vector< Node > gtesters; - for( unsigned i=0; i gtesters; + for( unsigned i=0; imkNode( OR, gtesters ); + d_util->d_lemmas.push_back( lem ); + Trace("sygus-sym-break2") << "Sym break lemma : " << lem << std::endl; + }else{ + Trace("sygus-sym-break2") << "repeated lemma for " << prog << " from " << a << std::endl; } - d_util->d_conflictNode = gtesters.size()==1 ? gtesters[0] : NodeManager::currentNM()->mkNode( AND, gtesters ); - Trace("sygus-sym-break2") << "Conflict : " << d_util->d_conflictNode << std::endl; - d_util->d_conflict = true; return false; }else{ return true; @@ -862,7 +918,7 @@ void SygusSymBreak::collectTesters( Node tst, std::map< Node, std::vector< Node } } -SygusUtil::SygusUtil( Context* c ) : d_conflict( c, false ) { +SygusUtil::SygusUtil( Context* c ) { d_split = new SygusSplit( this ); d_sym_break = new SygusSymBreak( this, c ); } @@ -1075,6 +1131,26 @@ bool SygusUtil::isSingularArg( Node n, Kind ik, int arg ) { return false; } +bool SygusUtil::hasOffsetArg( Kind ik, int arg, int& offset, Kind& ok ) { + if( ik==LT ){ + Assert( arg==0 || arg==1 ); + offset = arg==0 ? 1 : -1; + ok = LEQ; + return true; + }else if( ik==BITVECTOR_ULT ){ + Assert( arg==0 || arg==1 ); + offset = arg==0 ? 1 : -1; + ok = BITVECTOR_ULE; + return true; + }else if( ik==BITVECTOR_SLT ){ + Assert( arg==0 || arg==1 ); + offset = arg==0 ? 1 : -1; + ok = BITVECTOR_SLE; + return true; + } + return false; +} + Node SygusUtil::getTypeValue( TypeNode tn, int val ) { std::map< int, Node >::iterator it = d_type_value[tn].find( val ); @@ -1115,6 +1191,25 @@ Node SygusUtil::getTypeMaxValue( TypeNode tn ) { } } +Node SygusUtil::getTypeValueOffset( TypeNode tn, Node val, int offset ) { + std::map< int, Node >::iterator it = d_type_value_offset[tn][val].find( offset ); + if( it==d_type_value_offset[tn][val].end() ){ + Node val_o; + Node offset_val = getTypeValue( tn, offset ); + if( !offset_val.isNull() ){ + if( tn.isInteger() || tn.isReal() ){ + val_o = Rewriter::rewrite( NodeManager::currentNM()->mkNode( PLUS, val, offset_val ) ); + }else if( tn.isBitVector() ){ + val_o = Rewriter::rewrite( NodeManager::currentNM()->mkNode( BITVECTOR_PLUS, val, offset_val ) ); + } + } + d_type_value_offset[tn][val][offset] = val_o; + return val_o; + }else{ + return it->second; + } +} + void SygusUtil::registerSygusType( TypeNode tn ){ if( d_register.find( tn )==d_register.end() ){ if( !DatatypesRewriter::isTypeDatatype( tn ) ){ @@ -1196,14 +1291,20 @@ bool SygusUtil::hasOp( TypeNode tn, Node n ) { return getOpArg( tn, n )!=-1; } -bool SygusUtil::isKindArg( TypeNode tn, int i ) { +Kind SygusUtil::getArgKind( TypeNode tn, int i ) { Assert( isRegistered( tn ) ); std::map< TypeNode, std::map< int, Kind > >::iterator itt = d_arg_kind.find( tn ); if( itt!=d_arg_kind.end() ){ - return itt->second.find( i )!=itt->second.end(); - }else{ - return false; + std::map< int, Kind >::iterator itk = itt->second.find( i ); + if( itk!=itt->second.end() ){ + return itk->second; + } } + return UNDEFINED_KIND; +} + +bool SygusUtil::isKindArg( TypeNode tn, int i ) { + return getArgKind( tn, i )!=UNDEFINED_KIND; } bool SygusUtil::isConstArg( TypeNode tn, int i ) { diff --git a/src/theory/datatypes/datatypes_sygus.h b/src/theory/datatypes/datatypes_sygus.h index f30a0fd0a..33e9fc54a 100644 --- a/src/theory/datatypes/datatypes_sygus.h +++ b/src/theory/datatypes/datatypes_sygus.h @@ -46,19 +46,6 @@ private: // type to (rewritten) to original std::map< TypeNode, std::map< Node, Node > > d_gen_terms; std::map< TypeNode, std::map< Node, bool > > d_gen_redundant; -private: - bool isRegistered( TypeNode tn ); - int getKindArg( TypeNode tn, Kind k ); - int getConstArg( TypeNode tn, Node n ); - int getOpArg( TypeNode tn, Node n ); - bool hasKind( TypeNode tn, Kind k ); - bool hasConst( TypeNode tn, Node n ); - bool hasOp( TypeNode tn, Node n ); - bool isKindArg( TypeNode tn, int i ); - bool isConstArg( TypeNode tn, int i ); -private: - Node getVar( TypeNode tn, int i ); - Node getVarInc( TypeNode tn, std::map< TypeNode, int >& var_count ); private: /** register sygus type */ void registerSygusType( TypeNode tn ); @@ -73,6 +60,8 @@ private: bool isArgDatatype( const DatatypeConstructor& c, int i, const Datatype& dt ); /** get arg type */ TypeNode getArgType( const DatatypeConstructor& c, int i ); + /** is type match */ + bool isTypeMatch( const DatatypeConstructor& c1, const DatatypeConstructor& c2 ); private: // generic cache bool isGenericRedundant( TypeNode tn, Node g ); @@ -117,7 +106,8 @@ private: std::map< Node, ProgSearch * > d_prog_search; std::map< TypeNode, std::map< Node, Node > > d_normalized_to_orig; std::map< TypeNode, std::map< Node, bool > > d_redundant; - std::map< TypeNode, std::map< Node, std::vector< bool > > > d_conflict_gen; + std::map< TypeNode, std::map< Node, std::vector< Node > > > d_lemmas_reported; + std::map< TypeNode, std::map< Node, std::vector< bool > > > d_lemma_gen; Node getAnchor( Node n ); bool processCurrentProgram( Node a, TypeNode at, int depth, Node prog, std::vector< Node >& testers, std::map< Node, std::vector< Node > >& testers_u ); @@ -155,6 +145,7 @@ private: bool hasKind( TypeNode tn, Kind k ); bool hasConst( TypeNode tn, Node n ); bool hasOp( TypeNode tn, Node n ); + Kind getArgKind( TypeNode tn, int i ); bool isKindArg( TypeNode tn, int i ); bool isConstArg( TypeNode tn, int i ); void registerSygusType( TypeNode tn ); @@ -162,6 +153,7 @@ private: //information for builtin types std::map< TypeNode, std::map< int, Node > > d_type_value; std::map< TypeNode, Node > d_type_max_value; + std::map< TypeNode, std::map< Node, std::map< int, Node > > > d_type_value_offset; /** is assoc */ bool isAssoc( Kind k ); /** is comm */ @@ -172,9 +164,13 @@ private: bool isIdempotentArg( Node n, Kind ik, int arg ); /** is singular arg */ bool isSingularArg( Node n, Kind ik, int arg ); + /** get offset arg */ + bool hasOffsetArg( Kind ik, int arg, int& offset, Kind& ok ); /** get value */ Node getTypeValue( TypeNode tn, int val ); /** get value */ + Node getTypeValueOffset( TypeNode tn, Node val, int offset ); + /** get value */ Node getTypeMaxValue( TypeNode tn ); private: Node getVar( TypeNode tn, int i ); @@ -187,8 +183,9 @@ public: SygusUtil( context::Context* c ); SygusSplit * getSplit() { return d_split; } SygusSymBreak * getSymBreak() { return d_sym_break; } - context::CDO d_conflict; - Node d_conflictNode; + //context::CDO d_conflict; + //Node d_conflictNode; + std::vector< Node > d_lemmas; }; diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index 42d06cdb5..063b76102 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -368,17 +368,26 @@ void TheoryDatatypes::assertFact( Node fact, Node exp ){ if( !d_conflict && polarity ){ Trace("dt-tester") << "Assert tester : " << atom << std::endl; if( d_sygus_util ){ - Assert( !d_sygus_util->d_conflict ); + //Assert( !d_sygus_util->d_conflict ); d_sygus_util->getSymBreak()->addTester( atom ); + for( unsigned i=0; id_lemmas.size(); i++ ){ + Trace("dt-lemma-sygus") << "Sygus symmetry breaking lemma : " << d_sygus_util->d_lemmas[i] << std::endl; + d_out->lemma( d_sygus_util->d_lemmas[i] ); + } + d_sygus_util->d_lemmas.clear(); + /* if( d_sygus_util->d_conflict ){ - d_conflict = true; - std::vector< TNode > assumptions; - explain( d_sygus_util->d_conflictNode, assumptions ); - d_conflictNode = mkAnd( assumptions ); - Trace("dt-conflict") << "CONFLICT: sygus symmetry breaking conflict : " << d_conflictNode << std::endl; - d_out->conflict( d_conflictNode ); + //d_conflict = true; + if( !d_sygus_util->d_conflictNode.isNull() ){ + std::vector< TNode > assumptions; + explain( d_sygus_util->d_conflictNode, assumptions ); + d_conflictNode = mkAnd( assumptions ); + Trace("dt-conflict") << "CONFLICT: sygus symmetry breaking conflict : " << d_conflictNode << std::endl; + d_out->conflict( d_conflictNode ); + } return; } + */ } } } diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp index f9b7c4fdc..6d604a345 100644 --- a/src/theory/quantifiers/ce_guided_instantiation.cpp +++ b/src/theory/quantifiers/ce_guided_instantiation.cpp @@ -191,7 +191,7 @@ void CegInstantiation::CegConjecture::analyzeSygusConjecture() { std::map< Node, std::map< Node, std::vector< Node > > >::iterator itp = prog_invoke.find( c ); if( itp!=prog_invoke.end() ){ std::vector< Node > terms; - std::vector< Node > subs; + std::vector< Node > subs; for( std::map< Node, std::vector< Node > >::iterator it2 = itp->second.begin(); it2 != itp->second.end(); ++it2 ){ if( !it2->second.empty() ){ Node prog = it2->first; @@ -235,7 +235,7 @@ void CegInstantiation::CegConjecture::analyzeSygusConjecture() { d_single_inv_arg_sk.push_back( v ); } bd = bd.substitute( vars.begin(), vars.end(), d_single_inv_arg_sk.begin(), d_single_inv_arg_sk.end() ); - + Trace("cegqi-analyze-debug") << " -> " << bd << std::endl; } d_single_inv = NodeManager::currentNM()->mkNode( FORALL, pbvl, bd ); @@ -263,18 +263,21 @@ void CegInstantiation::CegConjecture::analyzeSygusConjecture() { } bool CegInstantiation::CegConjecture::processSingleInvLiteral( Node lit, bool pol, std::map< Node, std::vector< Node > >& case_vals ) { + Trace("ajr-temp") << "Process single inv lit " << lit << " " << pol << std::endl; if( lit.getKind()==NOT ){ return processSingleInvLiteral( lit[0], !pol, case_vals ); }else if( ( lit.getKind()==OR && pol ) || ( lit.getKind()==AND && !pol ) ){ bool exh = true; for( unsigned k=0; k::iterator it = d_single_inv_map_to_prog.find( lit[0] ); + Trace("ajr-temp") << "Check literal " << lit[r] << " at " << r << std::endl; + std::map< Node, Node >::iterator it = d_single_inv_map_to_prog.find( lit[r] ); if( it!=d_single_inv_map_to_prog.end() ){ if( r==1 || d_single_inv_map_to_prog.find( lit[1] )==d_single_inv_map_to_prog.end() ){ case_vals[it->second].push_back( lit[ r==0 ? 1 : 0 ] ); @@ -286,9 +289,9 @@ bool CegInstantiation::CegConjecture::processSingleInvLiteral( Node lit, bool po } return false; } - + bool CegInstantiation::CegConjecture::analyzeSygusConjunct( Node p, Node n, std::map< Node, std::vector< Node > >& children, - std::map< Node, std::map< Node, std::vector< Node > > >& prog_invoke, + std::map< Node, std::map< Node, std::vector< Node > > >& prog_invoke, std::vector< Node >& progs, std::map< Node, std::map< Node, bool > >& contains, bool pol ) { if( ( pol && n.getKind()==OR ) || ( !pol && n.getKind()==AND ) ){ for( unsigned i=0; igetOutputChannel().lemma( lem ); qe->getOutputChannel().requirePhase( lit, true ); - + if( options::ceGuidedInstFair()==CEGQI_FAIR_DT_HEIGHT_PRED ){ //implies height bounds on each candidate variable std::vector< Node > lem_c; @@ -470,7 +473,7 @@ void CegInstantiation::registerQuantifier( Node q ) { mc.push_back( NodeManager::currentNM()->mkNode( APPLY_UF, it->second, d_conj->d_candidates[j] ) ); } }else if( options::ceGuidedInstFair()==CEGQI_FAIR_DT_HEIGHT_PRED ){ - //measure term is a fresh constant + //measure term is a fresh constant mc.push_back( NodeManager::currentNM()->mkSkolem( "K", NodeManager::currentNM()->integerType() ) ); } } -- 2.30.2