From 4448f36d5c60c05aa2fca3bc760f534cf9926caa Mon Sep 17 00:00:00 2001 From: ajreynol Date: Wed, 8 Apr 2015 12:15:27 +0200 Subject: [PATCH] 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. --- src/parser/smt2/Smt2.g | 34 +++--- .../quantifiers/conjecture_generator.cpp | 11 +- src/theory/quantifiers/conjecture_generator.h | 2 + src/theory/quantifiers/fun_def_process.cpp | 105 +++++++++--------- src/theory/quantifiers/term_database.cpp | 38 +++++-- src/theory/quantifiers/term_database.h | 4 + 6 files changed, 118 insertions(+), 76 deletions(-) diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index eac16372a..8b7c0bda2 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -913,12 +913,10 @@ smt25Command[CVC4::Command*& cmd] term[expr, expr2] { PARSER_STATE->popScope(); std::string attr_name("fun-def"); - Type t = EXPR_MANAGER->booleanType(); - Expr avar = PARSER_STATE->mkVar(attr_name, t); - aexpr = MK_EXPR(kind::INST_ATTRIBUTE, avar); - aexpr = MK_EXPR(kind::INST_PATTERN_LIST, aexpr ); + aexpr = MK_EXPR(kind::INST_ATTRIBUTE, func_app); + aexpr = MK_EXPR(kind::INST_PATTERN_LIST, aexpr); //set the attribute to denote this is a function definition - static_cast($cmd)->addCommand( new SetUserAttributeCommand( attr_name, avar ) ); + static_cast($cmd)->addCommand( new SetUserAttributeCommand( attr_name, func_app ) ); //assert it Expr as = EXPR_MANAGER->mkExpr(kind::FORALL, EXPR_MANAGER->mkExpr(kind::BOUND_VAR_LIST, bvs), MK_EXPR( func_app.getType().isBoolean() ? kind::IFF : kind::EQUAL, func_app, expr ), aexpr); static_cast($cmd)->addCommand( new AssertCommand(as, false) ); @@ -952,14 +950,6 @@ smt25Command[CVC4::Command*& cmd] RPAREN_TOK LPAREN_TOK { - std::string attr_name("fun-def"); - Type t = EXPR_MANAGER->booleanType(); - Expr avar = PARSER_STATE->mkVar(attr_name, t); - aexpr = MK_EXPR(kind::INST_ATTRIBUTE, avar); - aexpr = MK_EXPR(kind::INST_PATTERN_LIST, aexpr ); - //set the attribute to denote these are function definitions - static_cast($cmd)->addCommand( new SetUserAttributeCommand( attr_name, avar ) ); - //set up the first scope if( sortedVarNamesList.empty() ){ PARSER_STATE->parseError(std::string("Must define at least one function in define-funs-rec")); @@ -980,6 +970,12 @@ smt25Command[CVC4::Command*& cmd] term[expr,expr2] { func_defs.push_back( expr ); + + std::string attr_name("fun-def"); + aexpr = MK_EXPR(kind::INST_ATTRIBUTE, func_app); + aexpr = MK_EXPR(kind::INST_PATTERN_LIST, aexpr ); + //set the attribute to denote these are function definitions + static_cast($cmd)->addCommand( new SetUserAttributeCommand( attr_name, func_app ) ); //assert it Expr as = EXPR_MANAGER->mkExpr(kind::FORALL, EXPR_MANAGER->mkExpr(kind::BOUND_VAR_LIST, bvs), MK_EXPR( func_app.getType().isBoolean() ? kind::IFF : kind::EQUAL, func_app, expr ), aexpr); static_cast($cmd)->addCommand( new AssertCommand(as, false) ); @@ -1752,7 +1748,10 @@ attribute[CVC4::Expr& expr,CVC4::Expr& retExpr, std::string& attr] ss << "warning: Attribute " << attr << " does not take a value (ignoring)"; PARSER_STATE->warning(ss.str()); } + Expr avar; bool success = true; + std::string attr_name = attr; + attr_name.erase( attr_name.begin() ); if( attr==":fun-def" ){ if( ( expr.getKind()!=kind::EQUAL && expr.getKind()!=kind::IFF ) || expr[0].getKind()!=kind::APPLY_UF ){ success = false; @@ -1776,14 +1775,15 @@ attribute[CVC4::Expr& expr,CVC4::Expr& retExpr, std::string& attr] std::stringstream ss; ss << "warning: Function definition should be an equality whose LHS is an uninterpreted function applied to unique variables."; PARSER_STATE->warning(ss.str()); + }else{ + avar = expr[0]; } + }else{ + Type t = EXPR_MANAGER->booleanType(); + avar = PARSER_STATE->mkVar(attr_name, t); } if( success ){ - std::string attr_name = attr; - attr_name.erase( attr_name.begin() ); //will set the attribute on auxiliary var (preserves attribute on formula through rewriting) - Type t = EXPR_MANAGER->booleanType(); - Expr avar = PARSER_STATE->mkVar(attr_name, t); retExpr = MK_EXPR(kind::INST_ATTRIBUTE, avar); Command* c = new SetUserAttributeCommand( attr_name, avar ); c->setMuted(true); 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; id_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; imkSort( 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; jmkFunctionType( 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; jmkNode( 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; jmkFunctionType( 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; jmkNode( 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 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; imkConst( 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 d_qattr_conjecture; -- 2.30.2