From: ajreynol Date: Thu, 16 Apr 2015 10:34:27 +0000 (+0200) Subject: Fix option --quant-fun-wd. Add mk_starexec script to contrib. X-Git-Tag: cvc5-1.0.0~6354 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=1c95df5efa3727a8b709049ef26ebb3fe6f0c6eb;p=cvc5.git Fix option --quant-fun-wd. Add mk_starexec script to contrib. --- diff --git a/contrib/mk_starexec b/contrib/mk_starexec new file mode 100644 index 000000000..aafe1f0c2 --- /dev/null +++ b/contrib/mk_starexec @@ -0,0 +1,9 @@ +#!/bin/bash +# Run : mk_starexec [TEXT] +# Run from directory containing cvc4 binary and subdirectory starexec/ containing the starexec space, i.e. subdirectory bin/ with configuration files. +# Generates file cvc4-[TEXT].tgz that can be uploaded to starexec. +strip cvc4 +cp cvc4 ./starexec/bin/cvc4 +cd starexec +tar -czf ../cvc4-$1.tgz . +rm bin/cvc4 \ No newline at end of file diff --git a/src/theory/quantifiers/inst_strategy_e_matching.cpp b/src/theory/quantifiers/inst_strategy_e_matching.cpp index 249b71130..414df2882 100644 --- a/src/theory/quantifiers/inst_strategy_e_matching.cpp +++ b/src/theory/quantifiers/inst_strategy_e_matching.cpp @@ -240,20 +240,24 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f, Theory::Effort effor d_patTerms[1][f].clear(); std::vector< Node > patTermsF; //well-defined function: can assume LHS is only trigger - Node bd = d_quantEngine->getTermDatabase()->getInstConstantBody( f ); - if( d_quantEngine->getTermDatabase()->isQAttrFunDef( f ) && options::quantFunWellDefined() ){ - Assert( bd.getKind()==EQUAL || bd.getKind()==IFF ); - Assert( bd[0].getKind()==APPLY_UF ); - patTermsF.push_back( bd[0] ); - }else{ - Trigger::collectPatTerms( d_quantEngine, f, bd, patTermsF, d_tr_strategy, d_user_no_gen[f], true ); + if( options::quantFunWellDefined() ){ + Node hd = TermDb::getFunDefHead( f ); + if( !hd.isNull() ){ + hd = d_quantEngine->getTermDatabase()->getInstConstantNode( hd, f ); + patTermsF.push_back( hd ); + } } - Trace("auto-gen-trigger") << "Collected pat terms for " << bd << ", no-patterns : " << d_user_no_gen[f].size() << std::endl; - Trace("auto-gen-trigger") << " "; - for( int i=0; i<(int)patTermsF.size(); i++ ){ - Trace("auto-gen-trigger") << patTermsF[i] << " "; + //otherwise, use algorithm for collecting pattern terms + if( patTermsF.empty() ){ + Node bd = d_quantEngine->getTermDatabase()->getInstConstantBody( f ); + Trigger::collectPatTerms( d_quantEngine, f, bd, patTermsF, d_tr_strategy, d_user_no_gen[f], true ); + Trace("auto-gen-trigger") << "Collected pat terms for " << bd << ", no-patterns : " << d_user_no_gen[f].size() << std::endl; + Trace("auto-gen-trigger") << " "; + for( int i=0; i<(int)patTermsF.size(); i++ ){ + Trace("auto-gen-trigger") << patTermsF[i] << " "; + } + Trace("auto-gen-trigger") << std::endl; } - Trace("auto-gen-trigger") << std::endl; //extend to literal matching (if applicable) d_quantEngine->getPhaseReqTerms( f, patTermsF ); //sort into single/multi triggers diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 090d127f1..e6f1ceee0 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -1241,8 +1241,7 @@ void TermDb::computeAttributes( Node q ) { if( avar.getAttribute(FunDefAttribute()) ){ Trace("quant-attr") << "Attribute : function definition : " << q << std::endl; d_qattr_fundef[q] = true; - //Assert( q[1].getKind()==EQUAL || q[1].getKind()==IFF ); - //Assert( q[2][i][0]==q[1][0] || q[2][i][0]==q[1][1] ); + //get operator directly from pattern Node f = q[2][i][0].getOperator(); if( d_fun_defs.find( f )!=d_fun_defs.end() ){ Message() << "Cannot define function " << f << " more than once." << std::endl;