From 97d43d56d74f3af68d1d022c66ee158a41b24757 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Fri, 23 Jan 2015 14:53:19 +0100 Subject: [PATCH] CEGQI fairness based on term height. Fix sygus-nf fairness bug for wrongly applied selectors. --- src/theory/datatypes/datatypes_rewriter.h | 50 ++++++++++++----- src/theory/datatypes/datatypes_sygus.cpp | 45 +++++++++------ src/theory/datatypes/kinds | 3 + src/theory/datatypes/theory_datatypes.cpp | 55 ++++++++++++++++--- .../datatypes/theory_datatypes_type_rules.h | 20 +++++++ .../quantifiers/ce_guided_instantiation.cpp | 17 +++++- src/theory/quantifiers/modes.h | 2 + src/theory/quantifiers/options | 2 +- src/theory/quantifiers/options_handlers.h | 5 ++ 9 files changed, 157 insertions(+), 42 deletions(-) diff --git a/src/theory/datatypes/datatypes_rewriter.h b/src/theory/datatypes/datatypes_rewriter.h index 90703774b..29a95b38f 100644 --- a/src/theory/datatypes/datatypes_rewriter.h +++ b/src/theory/datatypes/datatypes_rewriter.h @@ -169,22 +169,46 @@ public: } } } - if(in.getKind() == kind::DT_SIZE && in[0].getKind()==kind::APPLY_CONSTRUCTOR ){ - std::vector< Node > children; - for( unsigned i=0; imkNode( kind::DT_SIZE, in[0][i] ) ); + if(in.getKind() == kind::DT_SIZE ){ + if( in[0].getKind()==kind::APPLY_CONSTRUCTOR ){ + std::vector< Node > children; + for( unsigned i=0; imkNode( kind::DT_SIZE, in[0][i] ) ); + } + } + Node res; + if( !children.empty() ){ + children.push_back( NodeManager::currentNM()->mkConst( Rational(1) ) ); + res = children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( kind::PLUS, children ); + }else{ + res = NodeManager::currentNM()->mkConst( Rational(0) ); } + Trace("datatypes-rewrite") << "DatatypesRewriter::postRewrite: rewrite size " << in << " to " << res << std::endl; + return RewriteResponse(REWRITE_AGAIN_FULL, res ); } - Node res; - if( !children.empty() ){ - children.push_back( NodeManager::currentNM()->mkConst( Rational(1) ) ); - res = children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( kind::PLUS, children ); - }else{ - res = NodeManager::currentNM()->mkConst( Rational(0) ); + }else if(in.getKind() == kind::DT_HEIGHT_BOUND ){ + if( in[0].getKind()==kind::APPLY_CONSTRUCTOR ){ + std::vector< Node > children; + Node res; + Rational r = in[1].getConst(); + Rational rmo = Rational( r-Rational(1) ); + for( unsigned i=0; imkConst(false); + break; + }else{ + children.push_back( NodeManager::currentNM()->mkNode( kind::DT_HEIGHT_BOUND, in[0][i], NodeManager::currentNM()->mkConst(rmo) ) ); + } + } + } + if( res.isNull() ){ + res = children.size()==0 ? NodeManager::currentNM()->mkConst(true) : ( children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( kind::AND, children ) ); + } + Trace("datatypes-rewrite") << "DatatypesRewriter::postRewrite: rewrite height " << in << " to " << res << std::endl; + return RewriteResponse(REWRITE_AGAIN_FULL, res ); } - Trace("datatypes-rewrite") << "DatatypesRewriter::postRewrite: rewrite " << in << " to " << res << std::endl; - return RewriteResponse(REWRITE_AGAIN_FULL, res ); } if(in.getKind() == kind::TUPLE_SELECT && in[0].getKind() == kind::TUPLE) { diff --git a/src/theory/datatypes/datatypes_sygus.cpp b/src/theory/datatypes/datatypes_sygus.cpp index 84bcb5814..b68206b48 100644 --- a/src/theory/datatypes/datatypes_sygus.cpp +++ b/src/theory/datatypes/datatypes_sygus.cpp @@ -136,7 +136,11 @@ void SygusSplit::getSygusSplits( Node n, const Datatype& dt, std::vector< Node > } } } - + + // we are splitting on a term that may later have no semantics : guard this case + Node ptest = DatatypesRewriter::mkTester( n[0], csIndex, pdt ).negate(); + Trace("sygus-split-debug") << "Parent guard : " << ptest << std::endl; + d_splits[n].push_back( ptest ); } for( unsigned i=0; i reqk_arg; //TODO - 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( 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; + 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; + } + } + 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; + } } - //NAND,NOR if( nk!=UNDEFINED_KIND ){ Trace("sygus-split-debug") << "Push " << parent << " over " << k << " to " << nk; if( reqk!=UNDEFINED_KIND ){ diff --git a/src/theory/datatypes/kinds b/src/theory/datatypes/kinds index 8c25e2a86..55db44c29 100644 --- a/src/theory/datatypes/kinds +++ b/src/theory/datatypes/kinds @@ -167,4 +167,7 @@ typerule RECORD_UPDATE ::CVC4::theory::datatypes::RecordUpdateTypeRule operator DT_SIZE 1 "datatypes size" typerule DT_SIZE ::CVC4::theory::datatypes::DtSizeTypeRule +operator DT_HEIGHT_BOUND 1 "datatypes height bound" +typerule DT_HEIGHT_BOUND ::CVC4::theory::datatypes::DtHeightBoundTypeRule + endtheory diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index 82804e565..501b3d86e 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -60,6 +60,7 @@ TheoryDatatypes::TheoryDatatypes(Context* c, UserContext* u, OutputChannel& out, d_equalityEngine.addFunctionKind(kind::APPLY_CONSTRUCTOR); d_equalityEngine.addFunctionKind(kind::APPLY_SELECTOR_TOTAL); d_equalityEngine.addFunctionKind(kind::DT_SIZE); + d_equalityEngine.addFunctionKind(kind::DT_HEIGHT_BOUND); d_equalityEngine.addFunctionKind(kind::APPLY_TESTER); //d_equalityEngine.addFunctionKind(kind::APPLY_UF); @@ -134,7 +135,7 @@ void TheoryDatatypes::check(Effort e) { TimerStat::CodeTimer checkTimer(d_checkTime); - Trace("datatypes-debug") << "Check effort " << e << std::endl; + Trace("datatypes-check") << "Check effort " << e << std::endl; while(!done() && !d_conflict) { // Get all the assertions Assertion assertion = get(); @@ -994,7 +995,7 @@ void TheoryDatatypes::addTester( Node t, EqcInfo* eqc, Node n ){ } void TheoryDatatypes::addSelector( Node s, EqcInfo* eqc, Node n, bool assertFacts ) { - Debug("datatypes-debug") << "Add selector : " << s << " to eqc(" << n << ")" << std::endl; + Trace("dt-collapse-sel") << "Add selector : " << s << " to eqc(" << n << ")" << std::endl; //check to see if it is redundant NodeListMap::iterator sel_i = d_selector_apps.find( n ); Assert( sel_i != d_selector_apps.end() ); @@ -1002,7 +1003,8 @@ void TheoryDatatypes::addSelector( Node s, EqcInfo* eqc, Node n, bool assertFact NodeList* sel = (*sel_i).second; for( NodeList::const_iterator j = sel->begin(); j != sel->end(); ++j ){ Node ss = *j; - if( s.getOperator()==ss.getOperator() ){ + if( s.getOperator()==ss.getOperator() && ( s.getKind()!=DT_HEIGHT_BOUND || s[1]==ss[1] ) ){ + Trace("dt-collapse-sel") << "...redundant." << std::endl; return; } } @@ -1056,21 +1058,33 @@ void TheoryDatatypes::collapseSelector( Node s, Node c ) { Assert( c.getKind()==APPLY_CONSTRUCTOR ); Trace("dt-collapse-sel") << "collapse selector : " << s << " " << c << std::endl; Node r; + bool wrong = false; if( s.getKind()==kind::APPLY_SELECTOR_TOTAL ){ //Trace("dt-collapse-sel") << "Indices : " << Datatype::indexOf(c.getOperator().toExpr()) << " " << Datatype::cindexOf(s.getOperator().toExpr()) << std::endl; + wrong = Datatype::indexOf(c.getOperator().toExpr())!=Datatype::cindexOf(s.getOperator().toExpr()); + //if( wrong ){ + // return; + //} //if( Datatype::indexOf(c.getOperator().toExpr())!=Datatype::cindexOf(s.getOperator().toExpr()) ){ // mkExpDefSkolem( s.getOperator(), s[0].getType(), s.getType() ); // r = NodeManager::currentNM()->mkNode( kind::APPLY_UF, d_exp_def_skolem[s.getOperator().toExpr()], s[0] ); //}else{ r = NodeManager::currentNM()->mkNode( kind::APPLY_SELECTOR_TOTAL, s.getOperator(), c ); - }else if( s.getKind()==kind::DT_SIZE ){ - r = NodeManager::currentNM()->mkNode( kind::DT_SIZE, c ); + }else if( s.getKind()==DT_SIZE ){ + r = NodeManager::currentNM()->mkNode( DT_SIZE, c ); + }else if( s.getKind()==DT_HEIGHT_BOUND ){ + r = NodeManager::currentNM()->mkNode( DT_HEIGHT_BOUND, c, s[1] ); + if( r==d_true ){ + return; + } } Node rr = Rewriter::rewrite( r ); if( s!=rr ){ Node eq_exp = c.eqNode( s[0] ); Node eq = rr.getType().isBoolean() ? s.iffNode( rr ) : s.eqNode( rr ); - Trace("datatypes-infer") << "DtInfer : collapse sel : " << eq << " by " << eq_exp << std::endl; + Trace("datatypes-infer") << "DtInfer : collapse sel"; + Trace("datatypes-infer") << ( wrong ? " wrong" : ""); + Trace("datatypes-infer") << " : " << eq << " by " << eq_exp << std::endl; d_pending.push_back( eq ); d_pending_exp[ eq ] = eq_exp; @@ -1102,7 +1116,9 @@ void TheoryDatatypes::computeCareGraph(){ for( unsigned j=i+1; j().isZero() ){ + std::vector< Node > children; + const Datatype& dt = ((DatatypeType)(n[0].getType()).toType()).getDatatype(); + for( unsigned i=0; imkNode( IFF, n, children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( OR, children ) ); + } + Trace("datatypes-infer") << "DtInfer : zero height : " << lem << std::endl; + d_pending.push_back( lem ); + d_pending_exp[ lem ] = d_true; + d_infer.push_back( lem ); + } } } } diff --git a/src/theory/datatypes/theory_datatypes_type_rules.h b/src/theory/datatypes/theory_datatypes_type_rules.h index 3044a2bf1..b97645ecb 100644 --- a/src/theory/datatypes/theory_datatypes_type_rules.h +++ b/src/theory/datatypes/theory_datatypes_type_rules.h @@ -567,6 +567,26 @@ public: } };/* class DtSizeTypeRule */ +class DtHeightBoundTypeRule { +public: + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) + throw (TypeCheckingExceptionPrivate, AssertionException) { + if( check ) { + TypeNode t = n[0].getType(check); + if (!t.isDatatype()) { + throw TypeCheckingExceptionPrivate(n, "expecting datatype height bound term to have datatype argument."); + } + if( n[1].getKind()!=kind::CONST_RATIONAL ){ + throw TypeCheckingExceptionPrivate(n, "datatype height bound must be a constant"); + } + if( n[1].getConst().getNumerator().sgn()==-1 ){ + throw TypeCheckingExceptionPrivate(n, "datatype height bound must be non-negative"); + } + } + return nodeManager->integerType(); + } +};/* class DtHeightBoundTypeRule */ + }/* CVC4::theory::datatypes namespace */ }/* CVC4::theory namespace */ diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp index b1850b373..bb53c9cfb 100644 --- a/src/theory/quantifiers/ce_guided_instantiation.cpp +++ b/src/theory/quantifiers/ce_guided_instantiation.cpp @@ -73,7 +73,8 @@ Node CegInstantiation::CegConjecture::getLiteral( QuantifiersEngine * qe, int i std::map< int, Node >::iterator it = d_lits.find( i ); if( it==d_lits.end() ){ Trace("cegqi-engine") << "******* CEGQI : allocate size literal " << i << std::endl; - Node lit = NodeManager::currentNM()->mkNode( LEQ, d_measure_term, NodeManager::currentNM()->mkConst( Rational( i ) ) ); + Node c = NodeManager::currentNM()->mkConst( Rational( i ) ); + Node lit = NodeManager::currentNM()->mkNode( LEQ, d_measure_term, c ); lit = Rewriter::rewrite( lit ); d_lits[i] = lit; @@ -81,6 +82,17 @@ Node CegInstantiation::CegConjecture::getLiteral( QuantifiersEngine * qe, int i Trace("cegqi-lemma") << "Fairness split : " << lem << std::endl; qe->getOutputChannel().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; + for( unsigned j=0; jmkNode( DT_HEIGHT_BOUND, d_candidates[j], c ) ); + } + Node hlem = NodeManager::currentNM()->mkNode( OR, lit.negate(), lem_c.size()==1 ? lem_c[0] : NodeManager::currentNM()->mkNode( AND, lem_c ) ); + Trace("cegqi-lemma") << "Fairness expansion (dt-height-pred) : " << hlem << std::endl; + qe->getOutputChannel().lemma( hlem ); + } return lit; }else{ return it->second; @@ -158,6 +170,9 @@ void CegInstantiation::registerQuantifier( Node q ) { if( it!=d_uf_measure.end() ){ 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 + mc.push_back( NodeManager::currentNM()->mkSkolem( "K", NodeManager::currentNM()->integerType() ) ); } } if( !mc.empty() ){ diff --git a/src/theory/quantifiers/modes.h b/src/theory/quantifiers/modes.h index 5e692ace1..a6c52274f 100644 --- a/src/theory/quantifiers/modes.h +++ b/src/theory/quantifiers/modes.h @@ -128,6 +128,8 @@ typedef enum { CEGQI_FAIR_UF_DT_SIZE, /** enforce fairness by datatypes size */ CEGQI_FAIR_DT_SIZE, + /** enforce fairness by datatypes height bound */ + CEGQI_FAIR_DT_HEIGHT_PRED, /** do not use fair strategy for CEGQI */ CEGQI_FAIR_NONE, } CegqiFairMode; diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options index 009a0ada6..560e29c3b 100644 --- a/src/theory/quantifiers/options +++ b/src/theory/quantifiers/options @@ -198,7 +198,7 @@ option ceGuidedInstFair --cegqi-fair=MODE CVC4::theory::quantifiers::CegqiFairMo if and how to apply fairness for cegqi option sygusDecompose --sygus-decompose bool :default false decompose single invocation synthesis conjectures -option sygusNormalForm --sygus-normal-form bool :default true +option sygusNormalForm --sygus-nf bool :default true only search for sygus builtin terms that are in normal form option sygusNormalFormArg --sygus-nf-arg bool :default true account for relationship between arguments of operations in sygus normal form diff --git a/src/theory/quantifiers/options_handlers.h b/src/theory/quantifiers/options_handlers.h index e9f85d454..fdfad21b9 100644 --- a/src/theory/quantifiers/options_handlers.h +++ b/src/theory/quantifiers/options_handlers.h @@ -184,6 +184,9 @@ uf-dt-size \n\ default | dt-size \n\ + Default, enforce fairness using size theory operator.\n\ \n\ +dt-height-bound \n\ ++ Enforce fairness by height bound predicate.\n\ +\n\ none \n\ + Do not enforce fairness. \n\ \n\ @@ -379,6 +382,8 @@ inline CegqiFairMode stringToCegqiFairMode(std::string option, std::string optar return CEGQI_FAIR_UF_DT_SIZE; } else if(optarg == "default" || optarg == "dt-size") { return CEGQI_FAIR_DT_SIZE; + } else if(optarg == "dt-height-bound" ){ + return CEGQI_FAIR_DT_HEIGHT_PRED; } else if(optarg == "none") { return CEGQI_FAIR_NONE; } else if(optarg == "help") { -- 2.30.2