From: ajreynol Date: Sat, 31 Jan 2015 17:50:01 +0000 (+0100) Subject: Bug fix fairness for commutative operators in sygus. Minor. X-Git-Tag: cvc5-1.0.0~6412 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=1c78459ede8c4668a0f7d14a63d4505fdb7a4472;p=cvc5.git Bug fix fairness for commutative operators in sygus. Minor. --- diff --git a/src/theory/datatypes/datatypes_sygus.cpp b/src/theory/datatypes/datatypes_sygus.cpp index 353bd1392..e186c94d1 100644 --- a/src/theory/datatypes/datatypes_sygus.cpp +++ b/src/theory/datatypes/datatypes_sygus.cpp @@ -293,7 +293,7 @@ void SygusSplit::registerSygusTypeConstructorArg( TypeNode tnn, const Datatype& if( d_sygus_pc_nred[tnn][csIndex][sIndex][j] ){ Trace("sygus-split-debug") << "Check redundancy of " << dt[j].getSygusOp() << " and " << dto[i].getSygusOp() << " under " << parentKind << std::endl; bool rem = false; - if( isPComm && j>i && tnn==tnno ){ + if( isPComm && j>i && tnn==tnno && d_sygus_pc_nred[tnno][csIndex][osIndex][j] ){ //based on commutativity // use term ordering : constructor index of first argument is not greater than constructor index of second argument rem = true; @@ -500,9 +500,10 @@ bool SygusSplit::considerSygusSplitConst( const Datatype& dt, const Datatype& pd 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() ){ + int status; + Node co = d_util->getTypeValueOffset( c.getType(), c, offset, status ); + Trace("sygus-split-debug") << c << " with offset " << offset << " is " << co << ", status=" << status << std::endl; + if( status==0 && !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; @@ -1191,21 +1192,25 @@ Node SygusUtil::getTypeMaxValue( TypeNode tn ) { } } -Node SygusUtil::getTypeValueOffset( TypeNode tn, Node val, int offset ) { +Node SygusUtil::getTypeValueOffset( TypeNode tn, Node val, int offset, int& status ) { 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 ); + status = -1; if( !offset_val.isNull() ){ if( tn.isInteger() || tn.isReal() ){ val_o = Rewriter::rewrite( NodeManager::currentNM()->mkNode( PLUS, val, offset_val ) ); + status = 0; }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; + d_type_value_offset_status[tn][val][offset] = status; return val_o; }else{ + status = d_type_value_offset_status[tn][val][offset]; return it->second; } } diff --git a/src/theory/datatypes/datatypes_sygus.h b/src/theory/datatypes/datatypes_sygus.h index 33e9fc54a..db44eaa55 100644 --- a/src/theory/datatypes/datatypes_sygus.h +++ b/src/theory/datatypes/datatypes_sygus.h @@ -154,6 +154,7 @@ private: 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; + std::map< TypeNode, std::map< Node, std::map< int, int > > > d_type_value_offset_status; /** is assoc */ bool isAssoc( Kind k ); /** is comm */ @@ -169,7 +170,7 @@ private: /** get value */ Node getTypeValue( TypeNode tn, int val ); /** get value */ - Node getTypeValueOffset( TypeNode tn, Node val, int offset ); + Node getTypeValueOffset( TypeNode tn, Node val, int offset, int& status ); /** get value */ Node getTypeMaxValue( TypeNode tn ); private: diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp index 6d604a345..a64362c14 100644 --- a/src/theory/quantifiers/ce_guided_instantiation.cpp +++ b/src/theory/quantifiers/ce_guided_instantiation.cpp @@ -67,8 +67,10 @@ void CegInstantiation::CegConjecture::assign( QuantifiersEngine * qe, Node q ) { } } } - analyzeSygusConjecture(); d_syntax_guided = true; + if( options::sygusSingleInv() ){ + analyzeSygusConjecture(); + } }else if( qe->getTermDatabase()->isQAttrSynthesis( q ) ){ d_syntax_guided = false; }else{ @@ -263,7 +265,6 @@ 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 ) ){ @@ -276,7 +277,6 @@ bool CegInstantiation::CegConjecture::processSingleInvLiteral( Node lit, bool po }else if( lit.getKind()==IFF || lit.getKind()==EQUAL ){ if( pol ){ for( unsigned r=0; r<2; r++ ){ - 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() ){ @@ -379,13 +379,11 @@ void CegInstantiation::CegConjecture::initializeGuard( QuantifiersEngine * qe ){ Node inst = d_single_inv[1].substitute( vars.begin(), vars.end(), d_single_inv_sk.begin(), d_single_inv_sk.end() ); Node lem = NodeManager::currentNM()->mkNode( OR, d_guard.negate(), inst.negate() ); Trace("cegqi") << "Add single invocation lemma : " << lem << std::endl; - /* inactive for now (until figure out how to use it) qe->getOutputChannel().lemma( lem ); if( Trace.isOn("cegqi-debug") ){ lem = Rewriter::rewrite( lem ); Trace("cegqi-debug") << "...rewritten : " << lem << std::endl; } - */ } } }