diff options
author | Aina Niemetz <aina.niemetz@gmail.com> | 2017-08-25 15:39:16 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2017-08-25 15:39:16 -0700 |
commit | dfa69ff98a14fcc0f2387e59a0c9994ef440e7d0 (patch) | |
tree | 23031231926757cb9b8aab425d8354683a3a66d7 /proofs/lfsc_checker/sccwriter.cpp | |
parent | 378a0c45070ec033493c52e4fa92e6d03b89b6c0 (diff) |
Move LFSC checker out of the CVC repository. (#222)
LFSC now lives outside of the CVC4 repository and is not part of the CVC4 distribution
anymore. As a consequence, we
+ Add --with-lfsc and --with-lfsc-directory as configure options.
In the case where CVC4 has not been built with integrated LFSC, all code that interacts with
LFSC is disabled.
+ Disable proof checking if CVC4_USE_LFSC is not defined.
Configuring the build with --check-proofs but without --with-lfsc results in an error.
+ Do not call LFSC's cleanup function (but we should in the future).
LFSC checker segfaults during cleanup on regression testcase regress0/bv/core/bitvec7.smt.
Disabled call to lfscc_cleanup until the problem in lfscc is fixed.
+ Disable building with LFSC for the distcheck travis build since it is not part of the distribution
anymore. Further, make distcheck with LFSC would require to call contrib/get-lfsc-checker
before calling make check on the temp build (the build of the unpacked distribution tar ball).
Diffstat (limited to 'proofs/lfsc_checker/sccwriter.cpp')
-rw-r--r-- | proofs/lfsc_checker/sccwriter.cpp | 977 |
1 files changed, 0 insertions, 977 deletions
diff --git a/proofs/lfsc_checker/sccwriter.cpp b/proofs/lfsc_checker/sccwriter.cpp deleted file mode 100644 index d93341ab8..000000000 --- a/proofs/lfsc_checker/sccwriter.cpp +++ /dev/null @@ -1,977 +0,0 @@ -#include "sccwriter.h" - -#include <fstream> -#include <sstream> - -int sccwriter::exprCount = 0; -int sccwriter::strCount = 0; -int sccwriter::argsCount = 0; -int sccwriter::rnumCount = 0; - -int sccwriter::get_prog_index( const std::string& str ) -{ - for( int a=0; a<(int)progNames.size(); a++ ){ - if( progNames[a]==str ){ - return a; - } - } - return -1; -} - -int sccwriter::get_prog_index_by_expr( Expr* e ) -{ - for( int a=0; a<(int)progPtrs.size(); a++ ){ - if( progPtrs[a]==e ){ - return a; - } - } - return -1; -} - -bool sccwriter::is_var( const std::string& str ) -{ - for( int a=0; a<(int)vars.size(); a++ ){ - if( vars[a]==str ){ - return true; - } - } - return false; -} - -void sccwriter::add_global_sym( const std::string& str ) -{ - for( int a=0; a<(int)globalSyms.size(); a++ ){ - if( globalSyms[a]==str ){ - return; - } - } - globalSyms.push_back( str ); -} - -void sccwriter::indent( std::ostream& os, int ind ) -{ - for( int a=0; a<ind; a++ ) - { - os << " "; - } -} - -void sccwriter::write_function_header( std::ostream& os, int index, int opts ) -{ - //write the function header - std::string fname; - get_function_name( progNames[index], fname ); - os << "Expr* " << fname.c_str() << "( "; - CExpr* progvars = (CExpr*)get_prog( index )->kids[1]; - int counter = 0; - //write each argument - while( progvars->kids[counter] ) - { - if( counter!=0 ) - { - os << ", "; - } - os << "Expr* "; - write_variable( ((SymSExpr*)progvars->kids[counter])->s, os ); - //add to vars if options are set to do so - if( opts&opt_write_add_args ) - { - vars.push_back( ((SymSExpr*)progvars->kids[counter])->s ); - } - counter++; - } - os << " )"; - if( opts&opt_write_call_debug ) - { - os << "{" << std::endl; - indent( os, 1 ); - os << "std::cout << \"Call function " << fname.c_str() << " with arguments \";" << std::endl; - counter = 0; - while( progvars->kids[counter] ) - { - if( counter!=0 ) - { - indent( os, 1 ); - os << "std::cout << \", \";" << std::endl; - } - indent( os, 1 ); - write_variable( ((SymSExpr*)progvars->kids[counter])->s, os ); - os << "->print( std::cout );" << std::endl; - counter++; - } - indent( os, 1 ); - os << "std::cout << std::endl;" << std::endl; - } -} - -void sccwriter::get_function_name( const std::string& pname, std::string& fname ) -{ - fname = std::string( "f_" ); - fname.append( pname ); -} - -void sccwriter::write_variable( const std::string& n, std::ostream& os ) -{ - std::string nn; - get_var_name( n, nn ); - os << nn.c_str(); -} - -void sccwriter::get_var_name( const std::string& n, std::string& nn ) { - nn = std::string( n.c_str() ); - for( int i = 0; i <(int)n.length(); i++ ){ - char c = n[i]; - if (c <= 47) - c += 65; - else if (c >= 58 && c <= 64) - c += 97-58; - if ((c >= 91 && c <= 94) || c == 96) - c += 104-91; - else if (c >= 123) - c -= 4; - nn[i] = c; - } -} - -void sccwriter::write_file() -{ - static std::string filename( "scccode" ); - - //writer the h file - std::fstream fsh; - std::string fnameh( filename ); - fnameh.append(".h"); - fsh.open( fnameh.c_str(), std::ios::out ); - //write the header in h - fsh << "#ifndef SCC_CODE_H" << std::endl; - fsh << "#define SCC_CODE_H" << std::endl << std::endl; - //include necessary files in h file - fsh << "#include \"check.h\"" << std::endl << std::endl; - //write the init function - fsh << "void init_compiled_scc();" << std::endl << std::endl; - //write the entry function - fsh << "Expr* run_compiled_scc( Expr* p, std::vector< Expr* >& args );" << std::endl << std::endl; - //write the side condition code functions - for( int n=0; n<(int)progs.size(); n++ ) - { - //write the header in the h file - fsh << "inline "; - write_function_header( fsh, n ); - fsh << ";" << std::endl << std::endl; - } - fsh << "#endif" << std::endl << std::endl; - fsh.close(); - - - //writer the cpp code - std::fstream fsc; - std::string fnamec( filename ); - fnamec.append(".cpp"); - fsc.open( fnamec.c_str(), std::ios::out ); - //include the h file in the cpp - fsc << "#include \"scccode.h\"" << std::endl << std::endl; - std::ostringstream fsc_funcs; - //write the side condition code functions - for( currProgram=0; currProgram<(int)progs.size(); currProgram++ ) - { - //reset naming counters - vars.clear(); - exprCount = 0; - strCount = 0; - argsCount = 0; - rnumCount = 0; - - //for debugging - std::cout << "program #" << currProgram << " " << progNames[currProgram].c_str() << std::endl; - - //write the function header - write_function_header( fsc_funcs, currProgram, opt_write_add_args|options ); - if( (options&opt_write_call_debug)==0 ) - { - fsc_funcs << "{" << std::endl; - } - //write the code - //std::vector< std::string > cleanVec; - //write_code( get_prog( n )->kids[2], fsc, 1, "return ", cleanVec ); - //debug_write_code( progs[n].second->kids[2], fsc, 1 ); - std::string expr; - write_expr( get_prog( currProgram )->kids[2], fsc_funcs, 1, expr ); - indent( fsc_funcs, 1 ); - fsc_funcs << "return " << expr.c_str() << ";" << std::endl; - fsc_funcs << "}" << std::endl << std::endl; - } - //write the predefined symbols necessary - symbols and progs - for( int a=0; a<(int)globalSyms.size(); a++ ) - { - fsc << "Expr* e_" << globalSyms[a].c_str() << ";" << std::endl; - } - for( int a=0; a<(int)progs.size(); a++ ) - { - fsc << "Expr* e_" << progNames[a].c_str() << ";" << std::endl; - } - fsc << std::endl; - //write the init function - initialize symbols and progs - fsc << "void init_compiled_scc(){" << std::endl; - for( int a=0; a<(int)globalSyms.size(); a++ ) - { - indent( fsc, 1 ); - fsc << "e_" << globalSyms[a].c_str() << " = symbols->get(\"" << globalSyms[a].c_str() << "\").first;" << std::endl; - } - for( int a=0; a<(int)progs.size(); a++ ) - { - indent( fsc, 1 ); - fsc << "e_" << progNames[a].c_str() << " = progs[\"" << progNames[a].c_str() << "\"];" << std::endl; - } - fsc << "}" << std::endl << std::endl; - fsc << "Expr* run_compiled_scc( Expr* p, std::vector< Expr* >& args ){" << std::endl; - //for( int n=0; n<(int)progs.size(); n++ ){ - // indent( fsc, 1 ); - // fsc << "static std::string s_" << progNames[n].c_str() << " = std::string( \"" << progNames[n].c_str() << "\" );" << std::endl; - //} - for( int n=0; n<(int)progs.size(); n++ ){ - indent( fsc, 1 ); - if( n!=0 ){ - fsc << "}else "; - } - //for each function, test to see if the string matches the name of the function - fsc << "if( p==e_" << progNames[n].c_str() << " ){" << std::endl; - indent( fsc, 2 ); - std::string fname; - get_function_name( progNames[n], fname ); - //map the function to the proper function - fsc << "return " << fname.c_str() << "( "; - //write the arguments to the function from args - CExpr* progvars = (CExpr*)get_prog( n )->kids[1]; - int counter = 0; - bool firstTime = true; - while( progvars->kids[counter] ) - { - if( !firstTime ) - { - fsc << ", "; - } - fsc << "args[" << counter << "]"; - firstTime = false; - counter++; - } - fsc << " );" << std::endl; - } - indent( fsc, 1 ); - fsc << "}else{" << std::endl; - indent( fsc, 2 ); - //return null in the case the function could not be found - fsc << "return NULL;" << std::endl; - indent( fsc, 1 ); - fsc << "}" << std::endl; - fsc << "}" << std::endl << std::endl; - fsc << fsc_funcs.str().c_str(); - - fsc.close(); -} - -void sccwriter::write_code( Expr* code, std::ostream& os, int ind, const char* retModStr, int opts ) -{ - std::string retModString; - std::string incString; - if ( retModStr ) - { - retModString = std::string( retModStr ); - retModString.append( " = " ); - incString = std::string( retModStr ); - incString.append( "->inc();" ); - } - switch( code->getclass() ) - { - case INT_EXPR: - { - indent( os, ind ); - os << retModString.c_str(); - os << "new IntExpr( (signed long int)" << mpz_get_si( ((IntExpr*)code)->n ) << " );" << std::endl; - indent( os, ind ); - os << incString.c_str() << std::endl; - } - break; - case RAT_EXPR: - { - mpz_t num, den; - mpz_init(num); - mpz_init(den); - mpq_get_num( num, ((RatExpr*)code)->n ); - mpq_get_den( den, ((RatExpr*)code)->n ); - indent( os, ind ); - os << retModString.c_str(); - os << "new RatExpr( " << mpz_get_si( num ) << ", " << mpz_get_si( den ) << " );" << std::endl; - indent( os, ind ); - os << incString.c_str() << std::endl; - } - break; - case SYMS_EXPR: - { - //if it is a variable, simply write it to buffer - if( is_var( ((SymSExpr*)code)->s ) ) - { - indent( os, ind ); - os << retModString.c_str(); - write_variable( ((SymSExpr*)code)->s.c_str(), os ); - os << ";" << std::endl; - } - else //else must look at symbol lookup table - { - std::string var; - get_var_name( ((SymSExpr*)code)->s, var ); - indent( os, ind ); - os << retModString.c_str() << "e_" << var.c_str() << ";" << std::endl; - add_global_sym( var ); - } - indent( os, ind ); - os << incString.c_str() << std::endl; - } - break; - default: - switch( code->getop() ) - { - case APP: - { - //collect the arguments - std::vector< Expr* > argVector; - code->collect_args( argVector ); - //write the arguments - std::vector< std::string > args; - for( int a=0; a<(int)argVector.size(); a++ ) - { - std::string expr; - write_expr( argVector[a], os, ind, expr ); - args.push_back( expr ); - } - //write_args( (CExpr*)code, os, ind, 1, args ); - Expr* hd = code->get_head(); - //map to a program in the case that it is a program - if( hd->getop()==PROG && get_prog_index_by_expr( hd )!=-1 ) - { - indent( os, ind ); - os << retModString << "f_" << progNames[ get_prog_index_by_expr( hd ) ].c_str() << "( "; - for( int a=0; a<(int)args.size(); a++ ) - { - os << args[a].c_str(); - if( a!=(int)( args.size()-1 ) ){ - os << ", "; - } - } - os << " );" << std::endl; - for( int a=0; a<(int)args.size(); a++ ) - { - write_dec( args[a], os, ind ); - } - } - else - { -#ifdef USE_FLAT_APP - std::string expr; - write_expr( hd, os, ind, expr ); - indent( os, ind ); - os << retModString << "new CExpr( APP, "; - os << expr.c_str() << ", "; - for( int a=0; a<(int)args.size(); a++ ) - { - os << args[a].c_str(); - if( a!=(int)( args.size()-1 ) ){ - os << ", "; - } - } - os << " );" << std::endl; -#else - std::string expr; - write_expr( hd, os, ind, expr ); - indent( os, ind ); - os << retModString; - for( int a=0; a<(int)args.size(); a++ ) - { - os << "new CExpr( APP, "; - } - os << expr.c_str() << ", "; - for( int a=0; a<(int)args.size(); a++ ) - { - os << args[a].c_str(); - os << " )"; - if( a!=(int)( args.size()-1 ) ){ - os << ", "; - } - } - os << ";" << std::endl; -#endif - //indent( os, ind ); - //os << expr.c_str() << "->dec();" << std::endl; - } - } - break; - case MATCH: - { - //calculate the value for the expression - std::string expr; - write_expr( ((CExpr*)code)->kids[0], os, ind, expr ); - //get the head - std::ostringstream sshd; - sshd << "e" << exprCount; - exprCount++; - indent( os, ind ); - os << "Expr* " << sshd.str().c_str() << " = " << expr.c_str() << "->followDefs()->get_head();" << std::endl; - //write the arguments - std::vector< std::string > args; - write_args( (CExpr*)code, os, ind, 1, args ); - bool encounterDefault = false; - //now make an if statement corresponding to the match - int a = 0; - while( ((CExpr*)code)->kids[a+1] ) - { - indent( os, ind ); - if( a!=0 ){ - os << "}else"; - } - if( ((CExpr*)code)->kids[a+1]->getop()!=CASE ){ - encounterDefault = true; - os << "{" << std::endl; - //write the body of the case - write_code( ((CExpr*)code)->kids[a+1], os, ind+1, retModStr ); - indent( os, ind ); - os << "}" << std::endl; - }else{ - if( a!=0 ) - os << " "; - os << "if( " << sshd.str().c_str() << "==" << args[a].c_str() << " ){" << std::endl; - //collect args from the variable in the code - std::ostringstream ssargs; - ssargs << "args" << argsCount; - argsCount++; -#ifndef USE_FLAT_APP - indent( os, ind+1 ); - os << "std::vector< Expr* > " << ssargs.str().c_str() << ";" << std::endl; - indent( os, ind+1 ); - os << expr.c_str() << "->followDefs()->collect_args( " << ssargs.str().c_str() << " );" << std::endl; -#endif - //set the variables defined in the pattern equal to the arguments - std::vector< Expr* > caseArgs; - ((CExpr*)((CExpr*)code)->kids[a+1])->kids[0]->collect_args( caseArgs ); - for( int b=0; b<(int)caseArgs.size(); b++ ) - { - indent( os, ind+1 ); - os << "Expr* "; - write_variable( ((SymSExpr*)caseArgs[b])->s.c_str(), os ); -#ifdef USE_FLAT_APP - os << " = ((CExpr*)" << expr.c_str() << "->followDefs())->kids[" << b+1 << "];" << std::endl; -#else - os << " = " << ssargs.str().c_str() << "[" << b << "];" << std::endl; -#endif - vars.push_back( ((SymSExpr*)caseArgs[b])->s ); - } - //write the body of the case - write_code( ((CExpr*)code)->kids[a+1], os, ind+1, retModStr, opt_write_case_body ); - } - a++; - } - if( !encounterDefault ) - { - indent( os, ind ); - os << "}else{" << std::endl; - indent( os, ind + 1 ); - os << "std::cout << \"Could not find match for expression in function f_"; - os << progNames[currProgram].c_str() << " \";" << std::endl; - indent( os, ind + 1 ); - os << sshd.str().c_str() << "->print( std::cout );" << std::endl; - indent( os, ind + 1 ); - os << "std::cout << std::endl;" << std::endl; - indent( os, ind + 1 ); - os << "exit( 1 );" << std::endl; - indent( os, ind ); - os << "}" << std::endl; - } - write_dec( expr, os, ind ); - for( int a=0; a<(int)args.size(); a++ ) - { - write_dec( args[a], os, ind ); - } - } - break; - case CASE: - if( opts&opt_write_case_body ) - { - write_code( ((CExpr*)code)->kids[1], os, ind, retModStr ); - } - else - { - write_code( ((CExpr*)code)->kids[0]->get_head(), os, ind, retModStr ); - } - break; - case DO: - { - //write each of the children in sequence - int counter = 0; - while( ((CExpr*)code)->kids[counter] ) - { - if( ((CExpr*)code)->kids[counter+1]==NULL ) - { - write_code( ((CExpr*)code)->kids[counter], os, ind, retModStr ); - } - else - { - std::string expr; - write_expr( ((CExpr*)code)->kids[counter], os, ind, expr ); - //clean up memory - write_dec( expr, os, ind ); - } - counter++; - } - } - break; - case LET: - { - indent( os, ind ); - os << "Expr* "; - write_variable( ((SymSExpr*)((CExpr*)code)->kids[0])->s, os ); - os << " = NULL;" << std::endl; - std::ostringstream ss; - write_variable( ((SymSExpr*)((CExpr*)code)->kids[0])->s, ss ); - write_code( ((CExpr*)code)->kids[1], os, ind, ss.str().c_str() ); - //add it to the variables - vars.push_back( ((SymSExpr*)((CExpr*)code)->kids[0])->s ); - write_code( ((CExpr*)code)->kids[2], os, ind, retModStr ); - //clean up memory - indent( os, ind ); - write_variable( ((SymSExpr*)((CExpr*)code)->kids[0])->s, os ); - os << "->dec();" << std::endl; - } - break; - case FAIL: - { - indent( os, ind ); - os << retModString.c_str() << "NULL;" << std::endl; - } - break; -#ifndef MARKVAR_32 - case MARKVAR: - { - //calculate the value for the expression - std::string expr; - write_expr( ((CExpr*)code)->kids[0], os, ind, expr, opt_write_check_sym_expr ); - //set the mark on the expression - indent( os, ind ); - os << "if (" << expr.c_str() << "->followDefs()->getmark())" << std::endl; - indent( os, ind+1 ); - os << expr.c_str() << "->followDefs()->clearmark();" << std::endl; - indent( os, ind ); - os << "else" << std::endl; - indent( os, ind+1 ); - os << expr.c_str() << "->followDefs()->setmark();" << std::endl; - //write the return if necessary - if( retModStr!=NULL ){ - indent( os, ind ); - os << retModString.c_str() << expr.c_str() << ";" << std::endl; - indent( os, ind ); - os << incString.c_str() << std::endl; - } - write_dec( expr, os, ind ); - } - break; - case IFMARKED: - { - //calculate the value for the expression - std::string expr; - write_expr( ((CExpr*)code)->kids[0], os, ind, expr, opt_write_check_sym_expr ); - //if mark is set, write code for kids[1] - indent( os, ind ); - os << "if (" << expr.c_str() << "->followDefs()->getmark()){" << std::endl; - write_code( ((CExpr*)code)->kids[1], os, ind+1, retModStr ); - //else write code for kids[2] - indent( os, ind ); - os << "}else{" << std::endl; - write_code( ((CExpr*)code)->kids[2], os, ind+1, retModStr ); - indent( os, ind ); - os << "}" << std::endl; - //clean up memory - write_dec( expr, os, ind ); - } - break; -#else - case MARKVAR: - { - //calculate the value for the expression - std::string expr; - write_expr( ((CExpr*)code)->kids[1], os, ind, expr, opt_write_check_sym_expr ); - //set the mark on the expression - indent( os, ind ); - os << "if ( ((SymExpr*)" << expr.c_str() << "->followDefs())->getmark("; - os << ((IntExpr*)((CExpr*)code)->kids[0])->get_num() << "))" << std::endl; - indent( os, ind+1 ); - os << "((SymExpr*)" << expr.c_str() << "->followDefs())->clearmark("; - os << ((IntExpr*)((CExpr*)code)->kids[0])->get_num() << ");" << std::endl; - indent( os, ind ); - os << "else" << std::endl; - indent( os, ind+1 ); - os << "((SymExpr*)" << expr.c_str() << "->followDefs())->setmark("; - os << ((IntExpr*)((CExpr*)code)->kids[0])->get_num() << ");" << std::endl; - //write the return if necessary - if( retModStr!=NULL ){ - indent( os, ind ); - os << retModString.c_str() << expr.c_str() << ";" << std::endl; - indent( os, ind ); - os << incString.c_str() << std::endl; - } - write_dec( expr, os, ind ); - } - break; - case COMPARE: - { - std::string expr1, expr2; - write_expr( ((CExpr*)code)->kids[0], os, ind, expr1, opt_write_check_sym_expr ); - write_expr( ((CExpr*)code)->kids[1], os, ind, expr2, opt_write_check_sym_expr ); - indent( os, ind ); - os << "if( ((SymExpr*)" << expr1.c_str() << ")->followDefs() < ((SymExpr*)" << expr2.c_str() << ")->followDefs() ){" << std::endl; - write_code( ((CExpr*)code)->kids[2], os, ind+1, retModStr ); - indent( os, ind ); - os << "}else{" << std::endl; - write_code( ((CExpr*)code)->kids[3], os, ind+1, retModStr ); - indent( os, ind ); - os << "}" << std::endl; - //clean up memory - write_dec( expr1, os, ind ); - write_dec( expr2, os, ind ); - } - break; - case IFMARKED: - { - //calculate the value for the expression - std::string expr; - write_expr( ((CExpr*)code)->kids[1], os, ind, expr, opt_write_check_sym_expr ); - //if mark is set, write code for kids[1] - indent( os, ind ); - os << "if ( ((SymExpr*)" << expr.c_str() << "->followDefs())->getmark("; - os << ((IntExpr*)((CExpr*)code)->kids[0])->get_num() << ")){" << std::endl; - write_code( ((CExpr*)code)->kids[2], os, ind+1, retModStr ); - //else write code for kids[2] - indent( os, ind ); - os << "}else{" << std::endl; - write_code( ((CExpr*)code)->kids[3], os, ind+1, retModStr ); - indent( os, ind ); - os << "}" << std::endl; - //clean up memory - write_dec( expr, os, ind ); - } - break; -#endif - case ADD: - case MUL: - case DIV: - { - //calculate the value for the first expression - std::string expr1; - write_expr( ((CExpr*)code)->kids[0], os, ind, expr1 ); - //calculate the value for the second expression - std::string expr2; - write_expr( ((CExpr*)code)->kids[1], os, ind, expr2 ); - std::ostringstream ss; - ss << "rnum" << rnumCount; - rnumCount++; - indent( os, ind ); - os << "if( " << expr1.c_str() << "->followDefs()->getclass()==INT_EXPR ){" << std::endl; - indent( os, ind+1 ); - os << "mpz_t " << ss.str().c_str() << ";" << std::endl; - indent( os, ind+1 ); - os << "mpz_init(" << ss.str().c_str() << ");" << std::endl; - indent( os, ind+1 ); - os << "mpz_"; - if( code->getop()==ADD ) - os << "add"; - else - os << "mul"; - os << "( " << ss.str().c_str() << ", ((IntExpr*)" << expr1.c_str() << "->followDefs())->n, ((IntExpr*)" << expr2.c_str() << "->followDefs())->n);" << std::endl; - indent( os, ind+1 ); - os << retModString.c_str() << "new IntExpr(" << ss.str().c_str() << ");" << std::endl; - indent( os, ind ); - os << "}else if( " << expr1.c_str() << "->followDefs()->getclass()==RAT_EXPR ){" << std::endl; - indent( os, ind+1 ); - os << "mpq_t " << ss.str().c_str() << ";" << std::endl; - indent( os, ind+1 ); - os << "mpq_init(" << ss.str().c_str() << ");" << std::endl; - indent( os, ind+1 ); - os << "mpq_"; - if( code->getop()==ADD ) - os << "add"; - else if( code->getop()==MUL ) - os << "mul"; - else - os << "div"; - os << "( " << ss.str().c_str() << ", ((RatExpr*)" << expr1.c_str() << "->followDefs())->n, ((RatExpr*)" << expr2.c_str() << "->followDefs())->n);" << std::endl; - indent( os, ind+1 ); - os << retModString.c_str() << "new RatExpr(" << ss.str().c_str() << ");" << std::endl; - indent( os, ind ); - os << "}" << std::endl; - //clean up memory - write_dec( expr1, os, ind ); - write_dec( expr2, os, ind ); - } - break; - case NEG: - { - //calculate the value for the first expression - std::string expr1; - write_expr( ((CExpr*)code)->kids[0], os, ind, expr1 ); - std::ostringstream ss; - ss << "rnum" << rnumCount; - rnumCount++; - indent( os, ind ); - os << "if( " << expr1.c_str() << "->followDefs()->getclass()==INT_EXPR ){" << std::endl; - indent( os, ind+1 ); - os << "mpz_t " << ss.str().c_str() << ";" << std::endl; - indent( os, ind+1 ); - os << "mpz_init(" << ss.str().c_str() << ");" << std::endl; - indent( os, ind+1 ); - os << "mpz_neg( " << ss.str().c_str() << ", ((IntExpr*)" << expr1.c_str() << "->followDefs())->n );" << std::endl; - indent( os, ind+1 ); - os << retModString.c_str() << "new IntExpr(" << ss.str().c_str() << ");" << std::endl; - indent( os, ind ); - os << "}else if( " << expr1.c_str() << "->followDefs()->getclass()==RAT_EXPR ){" << std::endl; - indent( os, ind+1 ); - os << "mpq_t " << ss.str().c_str() << ";" << std::endl; - indent( os, ind+1 ); - os << "mpq_init(" << ss.str().c_str() << ");" << std::endl; - indent( os, ind+1 ); - os << "mpq_neg( " << ss.str().c_str() << ", ((RatExpr*)" << expr1.c_str() << "->followDefs())->n );" << std::endl; - indent( os, ind+1 ); - os << retModString.c_str() << "new RatExpr(" << ss.str().c_str() << ");" << std::endl; - indent( os, ind ); - os << "}" << std::endl; - //clean up memory - write_dec( expr1, os, ind ); - } - break; - case IFNEG: - case IFZERO: - { - std::string expr1; - write_expr( ((CExpr*)code)->kids[0], os, ind, expr1 ); - indent( os, ind ); - os << "if( " << expr1.c_str() << "->followDefs()->getclass()==INT_EXPR ){" << std::endl; - indent( os, ind+1 ); - os << "if( mpz_sgn( ((IntExpr *)" << expr1.c_str() << "->followDefs())->n ) "; - if( code->getop()==IFNEG ) - os << "<"; - else - os << "=="; - os << " 0 ){" << std::endl; - write_code( ((CExpr*)code)->kids[1], os, ind+2, retModStr ); - indent( os, ind+1 ); - os << "}else{" << std::endl; - write_code( ((CExpr*)code)->kids[2], os, ind+2, retModStr ); - indent( os, ind+1 ); - os << "}" << std::endl; - indent( os, ind ); - os << "}else if( " << expr1.c_str() << "->followDefs()->getclass()==RAT_EXPR ){" << std::endl; - indent( os, ind+1 ); - os << "if( mpq_sgn( ((RatExpr *)" << expr1.c_str() << "->followDefs())->n ) "; - if( code->getop()==IFNEG ) - os << "<"; - else - os << "=="; - os << " 0 ){" << std::endl; - write_code( ((CExpr*)code)->kids[1], os, ind+2, retModStr ); - indent( os, ind+1 ); - os << "}else{" << std::endl; - write_code( ((CExpr*)code)->kids[2], os, ind+2, retModStr ); - indent( os, ind+1 ); - os << "}" << std::endl; - indent( os, ind ); - os << "}" << std::endl; - //clean up memory - write_dec( expr1, os, ind ); - } - break; - case RUN:/*?*/break; - case PI:/*?*/break; - case LAM:/*?*/break; - case TYPE:/*?*/break; - case KIND:/*?*/break; - case ASCRIBE:/*?*/break; - case MPZ:/*?*/break; - case PROG:/*?*/break; - case PROGVARS:/*?*/break; - case PAT:/*?*/break; - } - break; - } -} - -void sccwriter::write_args( CExpr* code, std::ostream& os, int ind, int childCounter, - std::vector< std::string >& args, int opts ) -{ - bool encounterCase = false; - while( code->kids[childCounter] && - (!encounterCase || code->kids[childCounter]->getop()==CASE ) ) - { - encounterCase = encounterCase || code->kids[childCounter]->getop()==CASE; - if( code->kids[childCounter]->getclass()==SYMS_EXPR ) - { - args.push_back( ((SymSExpr*)code->kids[childCounter])->s ); - } - else - { - //calculate the value for the argument - std::string expr; - write_expr( code->kids[childCounter], os, ind, expr, opts ); - args.push_back( expr ); - } - childCounter++; - } -} - -void sccwriter::write_expr( Expr* code, std::ostream& os, int ind, std::string& expr, int opts ) -{ - if( code->getclass()==SYMS_EXPR && is_var( ((SymSExpr*)code)->s ) ) - { - get_var_name( ((SymSExpr*)code)->s, expr ); - indent( os, ind ); - os << expr.c_str() << "->inc();" << std::endl; - } - else - { - std::ostringstream ss; - ss << "e" << exprCount; - exprCount++; - //declare the expression - indent( os, ind ); - if( code->getclass()==SYMS_EXPR && !is_var( ((SymSExpr*)code)->s ) ) - { - os << "static "; - } - os << "Expr* " << ss.str().c_str() << " = NULL;" << std::endl; - //write the expression - std::ostringstream ss2; - ss2 << ss.str().c_str(); - write_code( code, os, ind, ss2.str().c_str(), opts ); - - //if is not a sym expression, then decrement the expression and return null - if( opts&opt_write_check_sym_expr ) - { - indent( os, ind ); - os << "if (" << expr.c_str() << "->getclass() != SYM_EXPR) {" << std::endl; - indent( os, ind+1 ); - os << "exit( 1 );" << std::endl; - indent( os, ind ); - os << "}" << std::endl; - } - - expr = std::string( ss.str().c_str() ); - vars.push_back( expr ); - } - //increment the counter for memory management - //indent( os, ind ); - //os << expr.c_str() << "->inc();" << std::endl; -} - -void sccwriter::write_dec( const std::string& expr, std::ostream& os, int ind ) -{ - bool wd = true; - if( wd ) - { - indent( os, ind ); - os << expr.c_str() << "->dec();" << std::endl; - } -} - -void sccwriter::debug_write_code( Expr* code, std::ostream& os, int ind ) -{ - indent( os, ind ); - switch( code->getclass() ) - { - case INT_EXPR: - os << "int_expr"; - break; - case HOLE_EXPR: - os << "hole_expr"; - break; - case SYM_EXPR: - os << "sym_expr"; - break; - case SYMS_EXPR: - os << "syms_expr: " << ((SymSExpr*)code)->s.c_str(); - break; - default: - switch( code->getop() ) - { - case APP: - os << "app"; - break; - case PI: - os << "pi"; - break; - case LAM: - os << "lam"; - break; - case TYPE: - os << "type"; - break; - case KIND: - os << "kind"; - break; - case ASCRIBE: - os << "ascribe"; - break; - case MPZ: - os << "mpz"; - break; - case PROG: - os << "prog"; - break; - case PROGVARS: - os << "progvars"; - break; - case MATCH: - os << "match"; - break; - case CASE: - os << "case"; - break; - case PAT: - os << "pat"; - break; - case DO: - os << "do"; - break; - case ADD: - os << "add"; - break; - case NEG: - os << "neg"; - break; - case LET: - os << "let"; - break; - case RUN: - os << "run"; - break; - case FAIL: - os << "fail"; - break; - case MARKVAR: - os << "markvar"; - break; - case IFMARKED: - os << "ifmarked"; - break; - case COMPARE: - os << "compare"; - break; - default: - os << "???"; - break; - } - } - os << std::endl; - if( code->getop()!=0 ) - { - CExpr* ce = (CExpr*)code; - int counter = 0; - while( ce->kids[counter] ){ - debug_write_code( ce->kids[counter], os, ind+1 ); - counter++; - } - } -} |