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<CommandSequence*>($cmd)->addCommand( new SetUserAttributeCommand( attr_name, avar ) );
+ static_cast<CommandSequence*>($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<CommandSequence*>($cmd)->addCommand( new AssertCommand(as, false) );
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<CommandSequence*>($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"));
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<CommandSequence*>($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<CommandSequence*>($cmd)->addCommand( new AssertCommand(as, false) );
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;
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);
while( d_free_var[tn].size()<=i ){\r
std::stringstream oss;\r
oss << tn;\r
+ std::string typ_name = oss.str();\r
+ while( typ_name[0]=='(' ){\r
+ typ_name.erase( typ_name.begin() );\r
+ }\r
std::stringstream os;\r
- os << oss.str()[0] << i;\r
+ os << typ_name[0] << i;\r
Node x = NodeManager::currentNM()->mkBoundVar( os.str().c_str(), tn );\r
d_free_var_num[x] = d_free_var[tn].size();\r
d_free_var[tn].push_back( x );\r
Node f = s->getTgFunc( d_typ, d_status_num );\r
if( d_children.size()==s->d_func_args[f].size() ){\r
std::vector< Node > children;\r
- children.push_back( f );\r
+ if( s->d_tg_func_param[f] ){\r
+ children.push_back( f );\r
+ }\r
for( unsigned i=0; i<d_children.size(); i++ ){\r
Node nc = s->d_tg_alloc[d_children[i]].getTerm( s );\r
if( nc.isNull() ){\r
d_func_kind[it->first] = nn.getKind();\r
d_typ_tg_funcs[tnull].push_back( it->first );\r
d_typ_tg_funcs[nn.getType()].push_back( it->first );\r
+ d_tg_func_param[it->first] = ( nn.getMetaKind() == kind::metakind::PARAMETERIZED );\r
Trace("sg-rel-sig") << "Will enumerate function applications of : " << it->first << ", #args = " << d_func_args[it->first].size() << ", kind = " << nn.getKind() << std::endl;\r
getTermDatabase()->computeUfEqcTerms( it->first );\r
}\r
std::map< TypeNode, unsigned > d_var_limit;\r
//the functions we can currently generate\r
std::map< TypeNode, std::vector< TNode > > d_typ_tg_funcs;\r
+ // whether functions must add operators\r
+ std::map< TNode, bool > d_tg_func_param;\r
//the equivalence classes (if applicable) that match the currently generated term\r
bool d_gen_relevant_terms;\r
//relevant equivalence classes\r
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;
+ }
}
}
}
}
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;
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 );
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;
projects / cvc5.git / commitdiff