From ad0863ae8333c4dcd950153e0db8cd4565a250b3 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Fri, 12 Jun 2015 14:15:14 +0200 Subject: Accelerate sygus solution reconstruction for constants and id functions. Minor changes to sygus type registration. Print sygus let solutions assuming fixed variable names. --- src/parser/smt2/smt2.cpp | 15 ++++++++++----- 1 file changed, 10 insertions(+), 5 deletions(-) (limited to 'src/parser/smt2') diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 47022da3e..8ed8e40a1 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -1001,17 +1001,22 @@ void Smt2::mkSygusDatatype( CVC4::Datatype& dt, std::vector& ops, void Smt2::addSygusDatatypeConstructor( CVC4::Datatype& dt, CVC4::Expr op, std::string& cname, std::vector< CVC4::Type >& cargs, CVC4::Expr& let_body, std::vector< CVC4::Expr >& let_args, unsigned let_num_input_args ) { - + Debug("parser-sygus") << "--> Add constructor " << cname << " to " << dt.getName() << std::endl; + if( !let_body.isNull() ){ + Debug("parser-sygus") << " let body = " << let_body << ", args = " << let_args.size() << "," << let_num_input_args << std::endl; + //TODO : remove arguments not occurring in body + //if this is a self identity function, ignore + if( let_args.size()==0 && let_args[0]==let_body ){ + Debug("parser-sygus") << " identity function " << cargs[0] << " to " << dt.getName() << std::endl; + //TODO + } + } std::string name = dt.getName() + "_" + cname; std::string testerId("is-"); testerId.append(name); checkDeclaration(name, CHECK_UNDECLARED, SYM_VARIABLE); checkDeclaration(testerId, CHECK_UNDECLARED, SYM_VARIABLE); CVC4::DatatypeConstructor c(name, testerId ); - Debug("parser-sygus") << "--> Add constructor " << cname << " to " << dt.getName() << std::endl; - if( !let_body.isNull() ){ - Debug("parser-sygus") << " let body = " << let_body << ", args = " << let_args.size() << "," << let_num_input_args << std::endl; - } c.setSygus( op, let_body, let_args, let_num_input_args ); for( unsigned j=0; j