diff options
Diffstat (limited to 'proofs/lfsc_checker/expr.cpp')
-rw-r--r-- | proofs/lfsc_checker/expr.cpp | 986 |
1 files changed, 0 insertions, 986 deletions
diff --git a/proofs/lfsc_checker/expr.cpp b/proofs/lfsc_checker/expr.cpp deleted file mode 100644 index 8c8120edb..000000000 --- a/proofs/lfsc_checker/expr.cpp +++ /dev/null @@ -1,986 +0,0 @@ -#include "expr.h" -#include <stdlib.h> -#include <sstream> -#ifdef _MSC_VER -#include <algorithm> -#endif -#include "check.h" - -using namespace std; - -int HoleExpr::next_id = 0; -int Expr::markedCount = 0; - -C_MACROS__ADD_CHUNKING_MEMORY_MANAGEMENT_CC(CExpr,kids,32768); - -//C_MACROS__ADD_CHUNKING_MEMORY_MANAGEMENT_CC(IntCExpr,_n,32768); - -#define USE_HOLE_PATH_COMPRESSION - -void Expr::debug() { - print(cout); - /* - cout << "\nAt " << this << "\n"; - cout << "marked = " << getmark() << "\n"; - */ - cout << "\n"; - cout.flush(); -} - -bool destroy_progs = false; - -#define destroydec(rr) \ - do { \ - Expr *r = rr; \ - int ref = r->data >> 9; \ - ref = ref - 1; \ - if (ref == 0) { \ - _e = r; \ - goto start_destroy; \ - } \ - else \ - r->data = (ref << 9) | (r->data & 511); \ - } while(0) - -//removed from below "ref = ref -1;": r->debugrefcnt(ref,DEC); - -void Expr::destroy(Expr *_e, bool dec_kids) { - start_destroy: - switch (_e->getclass()) { - case INT_EXPR: - delete (IntExpr *)_e; - break; - case SYMS_EXPR: { - SymSExpr *e = (SymSExpr *)_e; - if (e->val && e->val->getop() != PROG) { - Expr *tmp = e->val; - delete e; - destroydec(tmp); - } - else - delete e; - break; - } - case SYM_EXPR: { - SymExpr *e = (SymExpr *)_e; - if (e->val && e->val->getop() != PROG) { - Expr *tmp = e->val; - delete e; - destroydec(tmp); - } - else - delete e; - break; - } - case HOLE_EXPR: { - HoleExpr *e = (HoleExpr *)_e; - if (e->val) { - Expr *tmp = e->val; - delete e; - destroydec(tmp); - } - else - delete e; - break; - } - case CEXPR: { - CExpr *e = (CExpr *)_e; - if (dec_kids) { - Expr **cur = e->kids; - Expr *tmp; - while((tmp = *cur++)) { - if (*cur) - tmp->dec(); - else { - delete e; - destroydec(tmp); - break; - } - } - } - else - delete e; - break; - } - } -} - -Expr *Expr::clone() { - switch (getclass()) { - case INT_EXPR: - case RAT_EXPR: - inc(); - return this; - case SYMS_EXPR: - case SYM_EXPR: { - SymExpr *e = (SymExpr *)this; - if (e->val) - if (e->val->getop() != PROG) - return e->val->clone(); - e->inc(); - return e; - } - case HOLE_EXPR: { - HoleExpr *e = (HoleExpr *)this; - if (e->val) - return e->val->clone(); - e->inc(); - return e; - } - case CEXPR: { - CExpr *e = (CExpr *)this; - int op = e->getop(); - switch(op) { - case LAM: { -#ifdef DEBUG_SYM_NAMES - SymSExpr *var = (SymSExpr *)e->kids[0]; - SymSExpr *newvar = new SymSExpr(*var,SYMS_EXPR); -#else - SymExpr *var = (SymExpr *)e->kids[0]; - SymExpr *newvar = new SymExpr(*var); -#endif - Expr *prev = var->val; - var->val = newvar; - Expr *bod = e->kids[1]->clone(); - var->val = prev; - return new CExpr(LAM,newvar,bod); - } - case PI: { -#ifdef DEBUG_SYM_NAMES - SymSExpr *var = (SymSExpr *)e->kids[0]; - SymSExpr *newvar = new SymSExpr(*var,SYMS_EXPR); -#else - SymExpr *var = (SymExpr *)e->kids[0]; - SymExpr *newvar = new SymExpr(*var); -#endif - Expr *tp = e->kids[1]->clone(); - Expr *prev = var->val; - var->val = newvar; - Expr *bod = e->kids[2]->clone(); - var->val = prev; - Expr* ret = new CExpr(PI,newvar,tp,bod); - if( data&256 ) - ret->data |=256; - return ret; - } - default: { - Expr **cur = e->kids; - Expr *tmp; - int size = 0; - while((*cur++)) - size++; - Expr **kids = new Expr*[size+1]; - kids[size]=0; - cur = e->kids; - bool diff_kid = false; - int i = 0; - while((tmp = *cur++)) { - Expr *c = tmp->clone(); - diff_kid |= (c != tmp); - kids[i++] = c; - } - if (diff_kid) - return new CExpr(op, true /* dummy */, kids); - for (int i = 0, iend = size; i != iend; i++) - kids[i]->dec(); - delete[] kids; - e->inc(); - return e; - } - } - } - } - std::abort(); // should never be reached -} - - -Expr* Expr::build_app(Expr *hd, const std::vector<Expr *> &args, int start) { -#ifndef USE_FLAT_APP - Expr *ret = hd; - for (int i = start, iend = args.size(); i < iend; i++) - ret = new CExpr(APP,ret,args[i]); - return ret; -#else - if( start>=(int)args.size() ) - return hd; - else - { - Expr **kids = new Expr *[args.size() - start + 2]; - kids[0] = hd; - for (int i = start, iend = args.size(); i < iend; i++) - kids[i - start + 1] = args[i]; - kids[args.size() - start + 1] = NULL; - return new CExpr(APP, true /* dummy */, kids); - } -#endif -} - -Expr* Expr::make_app(Expr* e1, Expr* e2 ) -{ - //std::cout << "make app from "; - //e1->print( std::cout ); - //std::cout << " "; - //e2->print( std::cout ); - //std::cout << std::endl; - CExpr *ret; - if( e1->getclass()==CEXPR ){ - int counter = 0; - while( ((CExpr*)e1)->kids[counter] ){ - counter++; - } - Expr **kids = new Expr *[counter + 2]; - counter = 0; - while( ((CExpr*)e1)->kids[counter] ){ - kids[counter] = ((CExpr *)e1)->kids[counter]; - kids[counter]->inc(); - counter++; - } - kids[counter] = e2; - kids[counter + 1] = NULL; - ret = new CExpr(APP, true /* dummy */, kids); - }else{ - ret = new CExpr( APP, e1, e2 ); - } - //ret->print( std::cout ); - //std::cout << std::endl; - return ret; -} - -int Expr::cargCount = 0; - -Expr *Expr::collect_args(std::vector<Expr *> &args, bool follow_defs) { - //cargCount++; - //if( cargCount%1000==0) - //std::cout << cargCount << std::endl; -#ifndef USE_FLAT_APP - CExpr *e = (CExpr *)this; - args.reserve(16); - while( e->getop() == APP ) { - args.push_back(e->kids[1]); - e = (CExpr *)e->kids[0]; - if (follow_defs) - e = (CExpr *)e->followDefs(); - } - std::reverse(args.begin(),args.end()); - return e; -#else - CExpr *e = (CExpr *)this; - args.reserve(16); - if( e->getop()==APP ){ - int counter = 1; - while( e->kids[counter] ) { - args.push_back(e->kids[counter]); - counter++; - } - e = (CExpr*)e->kids[0]; - } - if (follow_defs) - return e->followDefs(); - else - return e; -#endif -} - -Expr *Expr::get_head(bool follow_defs) const { - CExpr *e = (CExpr *)this; - while( e->getop() == APP ) { - e = (CExpr *)e->kids[0]; - if (follow_defs) - e = (CExpr *)e->followDefs(); - } - return e; -} - -Expr *Expr::get_body(int op, bool follow_defs) const { - CExpr *e = (CExpr *)this; - while( e->getop() == op ) { - e = (CExpr *)e->kids[2]; - if (follow_defs) - e = (CExpr *)e->followDefs(); - } - return e; -} - -// if the return value is different from this, then it is a new reference -Expr *CExpr::whr() { - vector<Expr *> args; - if (get_head()->getop() == LAM) { - CExpr *head = (CExpr *)collect_args(args, true); - Expr *cloned_head; - if (head->cloned()) { - // we must clone - head = (CExpr *)head->clone(); - cloned_head = head; - } - else { - head->setcloned(); - cloned_head = 0; - } - int i = 0; - int iend = args.size(); - - /* we will end up incrementing the ref count for all the args, - since each is either pointed to by a var (following a - beta-reduction), or else just an argument in the new - application we build below. */ - - do { - Expr *tmp = args[i++]->followDefs(); - ((SymExpr *)head->kids[0])->val = tmp; - tmp->inc(); - head = (CExpr *)head->kids[1]; - } while(head->getop() == LAM && i < iend); - for (; i < iend; i++) - args[i]->inc(); - head->inc(); - if (cloned_head) - cloned_head->dec(); - return build_app(head,args,i); - } - else - return this; -} - -Expr* CExpr::convert_to_tree_app( Expr* e ) -{ - if( e->getop()==APP ) - { - std::vector< Expr* > kds; - int counter = 1; - while( ((CExpr*)e)->kids[counter] ) - { - kds.push_back( convert_to_tree_app( ((CExpr*)e)->kids[counter] ) ); - counter++; - } - Expr* app = Expr::build_app( e->get_head(), kds ); - //app->inc(); - return app; - } - else - { - return e; - } -} - -Expr* CExpr::convert_to_flat_app( Expr* e ) -{ - if( e->getop()==APP ) - { - std::vector< Expr* > args; - Expr* hd = ((CExpr*)e)->collect_args( args ); - Expr **kids = new Expr *[args.size() + 2]; - kids[0] = hd; - for (size_t a = 0; a < args.size(); a++) { - kids[a + 1] = convert_to_flat_app(args[a]); - } - kids[args.size() + 1] = 0; - CExpr *nce = new CExpr(APP, true /* dummy */, kids); - nce->inc(); - return nce; - } - else - { - return e; - } -} - -bool Expr::defeq(Expr *e) { - /* we handle a few special cases up front, where this Expr might - equal e, even though they have different opclass (i.e., different - structure). */ - - if (this == e) - return true; - int op1 = getop(); - int op2 = e->getop(); - switch (op1) { - case ASCRIBE: - return ((CExpr *)this)->kids[0]->defeq(e); - case APP: { - Expr *tmp = ((CExpr *)this)->whr(); - if (tmp != this) { - bool b = tmp->defeq(e); - tmp->dec(); - return b; - } - if (get_head()->getclass() == HOLE_EXPR) { - vector<Expr *> args; - Expr *head = collect_args(args, true); - Expr *t = e; - t->inc(); - for (int i = 0, iend = args.size(); i < iend; i++) { - // don't worry about SYMS_EXPR's, since we should not be in code here. - if (args[i]->getclass() != SYM_EXPR || args[i]->getexmark()) - /* we cannot fill the hole in this case. Either this is not - a variable or we are using a variable again. */ - return false; - SymExpr *v = (SymExpr *)args[i]; - - // we may have been mapping from expected var v to a computed var - Expr *tmp = (v->val ? v->val : v); - - tmp->inc(); - t = new CExpr(LAM, tmp, t); - args[i]->setexmark(); - } - for (int i = 0, iend = args.size(); i < iend; i++) - args[i]->clearexmark(); -#ifdef DEBUG_HOLES - cout << "Filling hole "; - head->debug(); - cout << "with "; - t->debug(); -#endif - ((HoleExpr *)head)->val = t; - return true; - } - break; - } - case NOT_CEXPR: - switch (getclass()) { - case HOLE_EXPR: { - HoleExpr *h = (HoleExpr *)this; - if (h->val) - return h->val->defeq(e); -#ifdef DEBUG_HOLES - cout << "Filling hole "; - h->debug(); - cout << "with "; - e->debug(); -#endif -#ifdef USE_HOLE_PATH_COMPRESSION - Expr *tmp = e->followDefs(); -#else - Expr *tmp = e; -#endif - h->val = tmp; - tmp->inc(); - return true; - } - case SYMS_EXPR: - case SYM_EXPR: { - SymExpr *s = (SymExpr *)this; - if (s->val) - return s->val->defeq(e); - break; - } - } - break; - } - - switch (op2) { - case ASCRIBE: - return defeq(((CExpr *)e)->kids[0]); - case APP: { - Expr *tmp = ((CExpr *)e)->whr(); - if (tmp != e) { - bool b = defeq(tmp); - tmp->dec(); - return b; - } - break; - } - case NOT_CEXPR: - switch (e->getclass()) { - case HOLE_EXPR: { - HoleExpr *h = (HoleExpr *)e; - if (h->val) - return defeq(h->val); - -#ifdef DEBUG_HOLES - cout << "Filling hole "; - h->debug(); - cout << "with "; - debug(); -#endif -#ifdef USE_HOLE_PATH_COMPRESSION - Expr *tmp = followDefs(); -#else - Expr *tmp = this; -#endif - h->val = tmp; - tmp->inc(); - return true; - } - case SYMS_EXPR: - case SYM_EXPR: { - SymExpr *s = (SymExpr *)e; - if (s->val) - return defeq(s->val); - break; - } - } - break; - } - - /* at this point, e1 and e2 must have the same opclass if they are - to be equal. */ - - if (op1 != op2) - return false; - - if (op1 == NOT_CEXPR) { - switch(getclass()) { - case INT_EXPR: { - IntExpr *i1 = (IntExpr *)this; - IntExpr *i2 = (IntExpr *)e; - return (mpz_cmp(i1->n,i2->n) == 0); - } - case RAT_EXPR: { - RatExpr *r1 = (RatExpr *)this; - RatExpr *r2 = (RatExpr *)e; - return (mpq_cmp(r1->n,r2->n) == 0); - } - case SYMS_EXPR: - case SYM_EXPR: - return (this == e); - } - } - - /* Now op1 and op2 must both be CExprs, and must have the same op to be - equal. */ - - CExpr *e1 = (CExpr *)this; - CExpr *e2 = (CExpr *)e; - - int last = 1; - switch (op1) { - case PI: - if (!e1->kids[1]->defeq(e2->kids[1])) - return false; - last++; - // fall through to LAM case - case LAM: { - - /* It is critical that we point e1's var. (v1) back to e2's (call - it v2). The reason this is critical is that we assume any - holes are in e1. So we could end up with (_ v1) = t. We wish - to fill _ in this case with (\ v2 t). If v2 pointed to v1, we - could not return (\ v1 t), because the fact that v2 points to - v1 would then be lost. - */ - SymExpr *v1 = (SymExpr *)e1->kids[0]; - Expr *prev_v1_val = v1->val; - v1->val = e2->kids[0]->followDefs(); - bool bodies_equal = e1->kids[last]->defeq(e2->kids[last]); - v1->val = prev_v1_val; - return bodies_equal; - } - case APP: -#ifndef USE_FLAT_APP - return (e1->kids[0]->defeq(e2->kids[0]) && - e1->kids[1]->defeq(e2->kids[1])); -#else - { - int counter = 0; - while( e1->kids[counter] ){ - if( e1->kids[counter]!=e2->kids[counter] ){ - if( !e2->kids[counter] || !e1->kids[counter]->defeq( e2->kids[counter] ) ) - return false; - //--- optimization : replace child with equivalent pointer if was defeq - // Heuristic: prefer symbolic kids because they may be cheaper to - // deal with (e.g. in free_in()). - if (e2->kids[counter]->isSymbolic() || - (!e1->kids[counter]->isSymbolic() && - e1->kids[counter]->getrefcnt() < - e2->kids[counter]->getrefcnt())) { - e1->kids[counter]->dec(); - e2->kids[counter]->inc(); - e1->kids[counter] = e2->kids[counter]; - }else{ - e2->kids[counter]->dec(); - e1->kids[counter]->inc(); - e2->kids[counter] = e1->kids[counter]; - } - } - //--- - counter++; - } - return e2->kids[counter]==NULL; - } -#endif - case TYPE: - case KIND: - case MPZ: - // already checked that both exprs have the same opclass. - return true; - } // switch(op1) - - std::abort(); // never reached. -} - -int Expr::fiCounter = 0; - -bool Expr::_free_in(Expr *x, expr_ptr_set_t *visited) { - // fiCounter++; - // if( fiCounter%1==0 ) - // std::cout << fiCounter << std::endl; - if (visited->find(this) != visited->end()) { - return false; - } - - switch (getop()) { - case NOT_CEXPR: - switch (getclass()) { - case HOLE_EXPR: { - HoleExpr *h = (HoleExpr *)this; - if (h->val) return h->val->_free_in(x, visited); - return (h == x); - } - case SYMS_EXPR: - case SYM_EXPR: { - SymExpr *s = (SymExpr *)this; - if (s->val && s->val->getclass() == HOLE_EXPR) - /* we do not need to follow the "val" pointer except in this - one case, when x is a hole (which we do not bother to check - here) */ - return s->val->_free_in(x, visited); - return (s == x); - } - case INT_EXPR: - return false; - } - break; - case LAM: - case PI: - if (x == ((CExpr *)this)->kids[0]) - return false; - // fall through - default: { - // must be a CExpr - assert(this->getclass() == CEXPR); - CExpr *e = (CExpr *)this; - Expr *tmp; - Expr **cur = e->kids; - visited->insert(this); - while ((tmp = *cur++)) - if (tmp->_free_in(x, visited)) return true; - return false; - } - } - std::abort(); // should not be reached -} - -void Expr::calc_free_in(){ - data &= ~256; - data |= 256*((CExpr *)this)->kids[2]->free_in( ((CExpr *)this)->kids[0] ); -} - -string Expr::toString() { - ostringstream oss; - print(oss); - return oss.str(); -} - -static void print_kids(ostream &os, Expr **kids) { - Expr *tmp; - while ((tmp = *kids++)) { - os << " "; - tmp->print(os); - } -} - -static void print_vector(ostream &os, const vector<Expr *> &v) { - for(int i = 0, iend = v.size(); i < iend; i++) { - os << " "; - v[i]->print(os); - } -} - -void Expr::print(ostream &os) { - CExpr *e = (CExpr *)this; // for CEXPR cases - - //std::cout << e->getop() << " "; - /* -#ifdef DEBUG_REFCNT - os << "<"; - char tmp[10]; - sprintf(tmp,"%d",getrefcnt()); - os << tmp << "> "; -#endif -*/ - - switch(getop()) { - case NOT_CEXPR: { - switch(getclass()) { - case INT_EXPR: - { - IntExpr *e = (IntExpr *)this; - if (mpz_sgn(e->n) < 0) { - os << "(~ "; - mpz_t tmp; - mpz_init(tmp); - mpz_neg(tmp,e->n); - char *s = mpz_get_str(0,10,tmp); - os << s; - free(s); - mpz_clear(tmp); - os << ")"; - //os << "mpz"; - } - else { - char *s = mpz_get_str(0,10,e->n); - os << s; - free(s); - //os << "mpz"; - } - break; - } - case RAT_EXPR: - { - RatExpr *e = (RatExpr *)this; - char *s = mpq_get_str(0,10,e->n); - os << s; - if (mpq_sgn(e->n) < 0) { - os << "(~ "; - mpq_t tmp; - mpq_init(tmp); - mpq_neg(tmp,e->n); - char *s = mpq_get_str(0,10,tmp); - os << s; - free(s); - mpq_clear(tmp); - os << ")"; - } - else { - char *s = mpq_get_str(0,10,e->n); - os << s; - free(s); - } - break; - } -#ifndef DEBUG_SYM_NAMES - case SYM_EXPR: - { - SymExpr *e = (SymExpr *)this; - if (e->val) { - if (e->val->getop() == PROG) { - os << e; -#ifdef DEBUG_SYMS - os << "[PROG]"; -#endif - }else{ -#ifdef DEBUG_SYMS - os << e; - os << "[SYM "; -#endif - e->val->print(os); -#ifdef DEBUG_SYMS - os << "]"; -#endif - } - } - else - os << e; - break; - } -#else - case SYM_EXPR: /* if we are debugging sym names, then - SYM_EXPRs are really SymSExprs. */ -#endif - case SYMS_EXPR: { - SymSExpr *e = (SymSExpr *)this; - if (e->val) { - if (e->val->getop() == PROG) { - os << e->s; -#ifdef DEBUG_SYMS - os << "[PROG]"; -#endif - }else{ -#ifdef DEBUG_SYMS - os << e->s; - os << "[SYM "; -#endif - e->val->print(os); -#ifdef DEBUG_SYMS - os << "]"; -#endif - } - } - else - os << e->s; - break; - } - case HOLE_EXPR: - { - HoleExpr *e = (HoleExpr *)this; - if (e->val) { -#ifdef DEBUG_SYMS - os << "_" << "[HOLE "; -#endif - e->val->print(os); -#ifdef DEBUG_SYMS - os << "]"; -#endif - }else { - os << "_"; -#ifdef DEBUG_HOLE_NAMES - char tmp[100]; - sprintf(tmp,"%d",e->id); - os << "[ " << tmp << "]"; -#else - os << "[ " << e << "]"; -#endif - } - break; - } - default: - os << "; unrecognized form of expr"; - break; - } - break; - } // case NOT_CEXPR - case APP: { - os << "("; - vector<Expr *> args; - Expr *head = collect_args(args, false /* follow_defs */); - head->print(os); - print_vector(os, args); - os << ")"; - break; - } - case LAM: - os << "(\\"; - print_kids(os, e->kids); - os << ")"; - break; - case PI: - os << "(!"; - print_kids(os, e->kids); - os << ")"; - break; - case TYPE: - os << "type"; - break; - case KIND: - os << "kind"; - break; - case MPZ: - os << "mpz"; - break; - case MPQ: - os << "mpq"; - break; - case ADD: - os << "(mp_add"; - print_kids(os,e->kids); - os << ")"; - break; - case MUL: - os << "(mp_mul"; - print_kids(os,e->kids); - os << ")"; - break; - case DIV: - os << "(mp_div"; - print_kids(os,e->kids); - os << ")"; - break; - case NEG: - os << "(mp_neg"; - print_kids(os,e->kids); - os << ")"; - break; - case IFNEG: - os << "(ifneg"; - print_kids(os,e->kids); - os << ")"; - break; - case IFZERO: - os << "(ifzero"; - print_kids(os,e->kids); - os << ")"; - break; - case RUN: - os << "(run"; - print_kids(os,e->kids); - os << ")"; - break; - case PROG: - os << "(prog"; - print_kids(os,e->kids); - os << ")"; - break; - case PROGVARS: - os << "("; - print_kids(os,e->kids); - os << ")"; - break; - case MATCH: - os << "(match"; - print_kids(os,e->kids); - os << ")"; - break; - case CASE: - os << "("; - print_kids(os,e->kids); - os << ")"; - break; - case LET: - os << "(let"; - print_kids(os,e->kids); - os << ")"; - break; - case DO: - os << "(do"; - print_kids(os,e->kids); - os << ")"; - break; - case IFMARKED: - os << "(ifmarked"; - print_kids(os,e->kids); - os << ")"; - break; - case COMPARE: - os << "(compare"; - print_kids(os,e->kids); - os << ")"; - break; - case MARKVAR: - os << "(markvar"; - print_kids(os,e->kids); - os << ")"; - break; - case FAIL: - os << "(fail "; - print_kids(os, e->kids); - os << ")"; - break; - case ASCRIBE: - os << "(:"; - print_kids(os, e->kids); - os << ")"; - break; - default: - os << "; unrecognized form of expr(2) " << getop() << " " << getclass(); - } // switch(getop()) -} - -bool Expr::isType( Expr* statType ){ - Expr* typ = this; - while( typ!=statType ){ - if( typ->getop()==PI ){ - typ = ((CExpr*)typ)->kids[2]; - }else{ - return false; - } - } - return true; -} - -int SymExpr::symmCount = 0; -#ifdef MARKVAR_32 -int SymExpr::mark() -{ - if( mark_map.find( this )== mark_map.end() ) - { - symmCount++; - mark_map[this] = 0; - } - return mark_map[this]; -} -void SymExpr::smark( int m ) -{ - mark_map[this] = m; -} -#endif |