diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-04-08 12:15:27 +0200 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-04-08 12:15:33 +0200 |
commit | 4448f36d5c60c05aa2fca3bc760f534cf9926caa (patch) | |
tree | 6c10032e7f2de811b0361fa50f5f4b5355a43d64 /src/theory/quantifiers | |
parent | c871e203705d3e191b8c8028a3f22bca6adb0d16 (diff) |
Make fun-def quantifiers carry the function app they define, make fun-def utilities more robust. Fix bug in conjecture generation for non-parameterized operators.
Diffstat (limited to 'src/theory/quantifiers')
-rwxr-xr-x | src/theory/quantifiers/conjecture_generator.cpp | 11 | ||||
-rwxr-xr-x | src/theory/quantifiers/conjecture_generator.h | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/fun_def_process.cpp | 105 | ||||
-rw-r--r-- | src/theory/quantifiers/term_database.cpp | 38 | ||||
-rw-r--r-- | src/theory/quantifiers/term_database.h | 4 |
5 files changed, 101 insertions, 59 deletions
diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp index 520ea5e70..48d3f3902 100755 --- a/src/theory/quantifiers/conjecture_generator.cpp +++ b/src/theory/quantifiers/conjecture_generator.cpp @@ -285,8 +285,12 @@ Node ConjectureGenerator::getFreeVar( TypeNode tn, unsigned i ) { while( d_free_var[tn].size()<=i ){
std::stringstream oss;
oss << tn;
+ std::string typ_name = oss.str();
+ while( typ_name[0]=='(' ){
+ typ_name.erase( typ_name.begin() );
+ }
std::stringstream os;
- os << oss.str()[0] << i;
+ os << typ_name[0] << i;
Node x = NodeManager::currentNM()->mkBoundVar( os.str().c_str(), tn );
d_free_var_num[x] = d_free_var[tn].size();
d_free_var[tn].push_back( x );
@@ -1713,7 +1717,9 @@ Node TermGenerator::getTerm( TermGenEnv * s ) { Node f = s->getTgFunc( d_typ, d_status_num );
if( d_children.size()==s->d_func_args[f].size() ){
std::vector< Node > children;
- children.push_back( f );
+ if( s->d_tg_func_param[f] ){
+ children.push_back( f );
+ }
for( unsigned i=0; i<d_children.size(); i++ ){
Node nc = s->d_tg_alloc[d_children[i]].getTerm( s );
if( nc.isNull() ){
@@ -1776,6 +1782,7 @@ void TermGenEnv::collectSignatureInformation() { d_func_kind[it->first] = nn.getKind();
d_typ_tg_funcs[tnull].push_back( it->first );
d_typ_tg_funcs[nn.getType()].push_back( it->first );
+ d_tg_func_param[it->first] = ( nn.getMetaKind() == kind::metakind::PARAMETERIZED );
Trace("sg-rel-sig") << "Will enumerate function applications of : " << it->first << ", #args = " << d_func_args[it->first].size() << ", kind = " << nn.getKind() << std::endl;
getTermDatabase()->computeUfEqcTerms( it->first );
}
diff --git a/src/theory/quantifiers/conjecture_generator.h b/src/theory/quantifiers/conjecture_generator.h index 462fadfce..2d8e8e403 100755 --- a/src/theory/quantifiers/conjecture_generator.h +++ b/src/theory/quantifiers/conjecture_generator.h @@ -138,6 +138,8 @@ public: std::map< TypeNode, unsigned > d_var_limit;
//the functions we can currently generate
std::map< TypeNode, std::vector< TNode > > d_typ_tg_funcs;
+ // whether functions must add operators
+ std::map< TNode, bool > d_tg_func_param;
//the equivalence classes (if applicable) that match the currently generated term
bool d_gen_relevant_terms;
//relevant equivalence classes
diff --git a/src/theory/quantifiers/fun_def_process.cpp b/src/theory/quantifiers/fun_def_process.cpp index 0bc365ec7..b80d9d744 100644 --- a/src/theory/quantifiers/fun_def_process.cpp +++ b/src/theory/quantifiers/fun_def_process.cpp @@ -32,66 +32,71 @@ void FunDefFmf::simplify( std::vector< Node >& assertions, bool doRewrite ) { std::vector< int > fd_assertions; //first pass : find defined functions, transform quantifiers for( unsigned i=0; i<assertions.size(); i++ ){ - if( assertions[i].getKind()==FORALL ){ - if( quantifiers::TermDb::isFunDef( assertions[i] ) ){ - Assert( assertions[i][1].getKind()==EQUAL || assertions[i][1].getKind()==IFF ); - Node n = assertions[i][1][0]; - Assert( n.getKind()==APPLY_UF ); - Node f = n.getOperator(); - - //check if already defined, if so, throw error - if( d_sorts.find( f )!=d_sorts.end() ){ - Message() << "Cannot define function " << f << " more than once." << std::endl; - exit( 0 ); - } + Node n = TermDb::getFunDefHead( assertions[i] ); + if( !n.isNull() ){ + Assert( n.getKind()==APPLY_UF ); + Node f = n.getOperator(); - //create a sort S that represents the inputs of the function - std::stringstream ss; - ss << "I_" << f; - TypeNode iType = NodeManager::currentNM()->mkSort( ss.str() ); - d_sorts[f] = iType; + //check if already defined, if so, throw error + if( d_sorts.find( f )!=d_sorts.end() ){ + Message() << "Cannot define function " << f << " more than once." << std::endl; + exit( 0 ); + } + + Node bd = TermDb::getFunDefBody( assertions[i] ); + Assert( !bd.isNull() ); + bd = NodeManager::currentNM()->mkNode( n.getType().isBoolean() ? IFF : EQUAL, n, bd ); - //create functions f1...fn mapping from this sort to concrete elements - for( unsigned j=0; j<n.getNumChildren(); j++ ){ - TypeNode typ = NodeManager::currentNM()->mkFunctionType( iType, n[j].getType() ); - std::stringstream ss; - ss << f << "_arg_" << j; - d_input_arg_inj[f].push_back( NodeManager::currentNM()->mkSkolem( ss.str(), typ, "op created during fun def fmf" ) ); - } + //create a sort S that represents the inputs of the function + std::stringstream ss; + ss << "I_" << f; + TypeNode iType = NodeManager::currentNM()->mkSort( ss.str() ); + d_sorts[f] = iType; - //construct new quantifier forall S. F[f1(S)/x1....fn(S)/xn] - std::vector< Node > children; - Node bv = NodeManager::currentNM()->mkBoundVar("?i", iType ); - Node bvl = NodeManager::currentNM()->mkNode( kind::BOUND_VAR_LIST, bv ); - std::vector< Node > subs; - std::vector< Node > vars; - for( unsigned j=0; j<n.getNumChildren(); j++ ){ - vars.push_back( n[j] ); - subs.push_back( NodeManager::currentNM()->mkNode( APPLY_UF, d_input_arg_inj[f][j], bv ) ); - } - Node bd = assertions[i][1].substitute( vars.begin(), vars.end(), subs.begin(), subs.end() ); + //create functions f1...fn mapping from this sort to concrete elements + for( unsigned j=0; j<n.getNumChildren(); j++ ){ + TypeNode typ = NodeManager::currentNM()->mkFunctionType( iType, n[j].getType() ); + std::stringstream ss; + ss << f << "_arg_" << j; + d_input_arg_inj[f].push_back( NodeManager::currentNM()->mkSkolem( ss.str(), typ, "op created during fun def fmf" ) ); + } - Trace("fmf-fun-def") << "FMF fun def: rewrite " << assertions[i] << std::endl; - Trace("fmf-fun-def") << " to " << std::endl; - assertions[i] = NodeManager::currentNM()->mkNode( FORALL, bvl, bd ); - Trace("fmf-fun-def") << " " << assertions[i] << std::endl; - fd_assertions.push_back( i ); + //construct new quantifier forall S. F[f1(S)/x1....fn(S)/xn] + std::vector< Node > children; + Node bv = NodeManager::currentNM()->mkBoundVar("?i", iType ); + Node bvl = NodeManager::currentNM()->mkNode( kind::BOUND_VAR_LIST, bv ); + std::vector< Node > subs; + std::vector< Node > vars; + for( unsigned j=0; j<n.getNumChildren(); j++ ){ + vars.push_back( n[j] ); + subs.push_back( NodeManager::currentNM()->mkNode( APPLY_UF, d_input_arg_inj[f][j], bv ) ); } + bd = bd.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() ); + + Trace("fmf-fun-def") << "FMF fun def: rewrite " << assertions[i] << std::endl; + Trace("fmf-fun-def") << " to " << std::endl; + assertions[i] = NodeManager::currentNM()->mkNode( FORALL, bvl, bd ); + assertions[i] = Rewriter::rewrite( assertions[i] ); + Trace("fmf-fun-def") << " " << assertions[i] << std::endl; + fd_assertions.push_back( i ); } } //second pass : rewrite assertions for( unsigned i=0; i<assertions.size(); i++ ){ int is_fd = std::find( fd_assertions.begin(), fd_assertions.end(), i )!=fd_assertions.end() ? 1 : 0; - std::vector< Node > constraints; - Trace("fmf-fun-def-rewrite") << "Rewriting " << assertions[i] << ", is_fd = " << is_fd << std::endl; - Node n = simplify( assertions[i], true, true, constraints, is_fd ); - Assert( constraints.empty() ); - if( n!=assertions[i] ){ - n = Rewriter::rewrite( n ); - Trace("fmf-fun-def-rewrite") << "FMF fun def : rewrite " << assertions[i] << std::endl; - Trace("fmf-fun-def-rewrite") << " to " << std::endl; - Trace("fmf-fun-def-rewrite") << " " << n << std::endl; - assertions[i] = n; + //constant boolean function definitions do not add domain constraints + if( is_fd==0 || ( is_fd==1 && ( assertions[i][1].getKind()==EQUAL || assertions[i][1].getKind()==IFF ) ) ){ + std::vector< Node > constraints; + Trace("fmf-fun-def-rewrite") << "Rewriting " << assertions[i] << ", is_fd = " << is_fd << std::endl; + Node n = simplify( assertions[i], true, true, constraints, is_fd ); + Assert( constraints.empty() ); + if( n!=assertions[i] ){ + n = Rewriter::rewrite( n ); + Trace("fmf-fun-def-rewrite") << "FMF fun def : rewrite " << assertions[i] << std::endl; + Trace("fmf-fun-def-rewrite") << " to " << std::endl; + Trace("fmf-fun-def-rewrite") << " " << n << std::endl; + assertions[i] = n; + } } } } diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 2e2007c0a..090d127f1 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -1187,20 +1187,44 @@ Node TermDb::getRewriteRule( Node q ) { } bool TermDb::isFunDef( Node q ) { - if( q.getKind()==FORALL && ( q[1].getKind()==EQUAL || q[1].getKind()==IFF ) && q[1][0].getKind()==APPLY_UF && q.getNumChildren()==3 ){ + return !getFunDefHead( q ).isNull(); +} + +Node TermDb::getFunDefHead( Node q ) { + //&& ( q[1].getKind()==EQUAL || q[1].getKind()==IFF ) && q[1][0].getKind()==APPLY_UF && + if( q.getKind()==FORALL && q.getNumChildren()==3 ){ for( unsigned i=0; i<q[2].getNumChildren(); i++ ){ if( q[2][i].getKind()==INST_ATTRIBUTE ){ if( q[2][i][0].getAttribute(FunDefAttribute()) ){ - return true; + return q[2][i][0]; } } } } - return false; + return Node::null(); +} +Node TermDb::getFunDefBody( Node q ) { + Node h = getFunDefHead( q ); + if( !h.isNull() ){ + if( q[1].getKind()==EQUAL || q[1].getKind()==IFF ){ + if( q[1][0]==h ){ + return q[1][1]; + }else if( q[1][1]==h ){ + return q[1][0]; + } + }else{ + Node atom = q[1].getKind()==NOT ? q[1][0] : q[1]; + bool pol = q[1].getKind()!=NOT; + if( atom==h ){ + return NodeManager::currentNM()->mkConst( pol ); + } + } + } + return Node::null(); } - void TermDb::computeAttributes( Node q ) { + Trace("quant-attr-debug") << "Compute attributes for " << q << std::endl; if( q.getNumChildren()==3 ){ for( unsigned i=0; i<q[2].getNumChildren(); i++ ){ Trace("quant-attr-debug") << "Check : " << q[2][i] << " " << q[2][i].getKind() << std::endl; @@ -1217,9 +1241,9 @@ 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[1][0].getKind()==APPLY_UF ); - Node f = q[1][0].getOperator(); + //Assert( q[1].getKind()==EQUAL || q[1].getKind()==IFF ); + //Assert( q[2][i][0]==q[1][0] || q[2][i][0]==q[1][1] ); + 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; exit( 0 ); diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index e4e34ce7f..db84ba885 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -340,6 +340,10 @@ public: //general queries concerning quantified formulas wrt modules static Node getRewriteRule( Node q ); /** is fun def */ static bool isFunDef( Node q ); + /** get fun def body */ + static Node getFunDefHead( Node q ); + /** get fun def body */ + static Node getFunDefBody( Node q ); //attributes private: std::map< Node, bool > d_qattr_conjecture; |