diff options
Diffstat (limited to 'proofs/lfsc_checker/scccode.cpp')
-rw-r--r-- | proofs/lfsc_checker/scccode.cpp | 609 |
1 files changed, 609 insertions, 0 deletions
diff --git a/proofs/lfsc_checker/scccode.cpp b/proofs/lfsc_checker/scccode.cpp new file mode 100644 index 000000000..cff762a08 --- /dev/null +++ b/proofs/lfsc_checker/scccode.cpp @@ -0,0 +1,609 @@ +#include "scccode.h" + +Expr* e_pos; +Expr* e_neg; +Expr* e_tt; +Expr* e_ff; +Expr* e_cln; +Expr* e_clc; +Expr* e_concat; +Expr* e_clr; +Expr* e_litvar; +Expr* e_litpol; +Expr* e_notb; +Expr* e_iffb; +Expr* e_clear_mark; +Expr* e_append; +Expr* e_simplify_clause_h; +Expr* e_simplify_clause; + +void init_compiled_scc(){ + e_pos = symbols->get("pos").first; + e_neg = symbols->get("neg").first; + e_tt = symbols->get("tt").first; + e_ff = symbols->get("ff").first; + e_cln = symbols->get("cln").first; + e_clc = symbols->get("clc").first; + e_concat = symbols->get("concat").first; + e_clr = symbols->get("clr").first; + e_litvar = progs["litvar"]; + e_litpol = progs["litpol"]; + e_notb = progs["notb"]; + e_iffb = progs["iffb"]; + e_clear_mark = progs["clear_mark"]; + e_append = progs["append"]; + e_simplify_clause_h = progs["simplify_clause_h"]; + e_simplify_clause = progs["simplify_clause"]; +} + +Expr* run_compiled_scc( Expr* p, std::vector< Expr* >& args ){ + if( p==e_litvar ){ + return f_litvar( args[0] ); + }else if( p==e_litpol ){ + return f_litpol( args[0] ); + }else if( p==e_notb ){ + return f_notb( args[0] ); + }else if( p==e_iffb ){ + return f_iffb( args[0], args[1] ); + }else if( p==e_clear_mark ){ + return f_clear_mark( args[0] ); + }else if( p==e_append ){ + return f_append( args[0], args[1] ); + }else if( p==e_simplify_clause_h ){ + return f_simplify_clause_h( args[0], args[1] ); + }else if( p==e_simplify_clause ){ + return f_simplify_clause( args[0] ); + }else{ + return NULL; + } +} + +Expr* f_litvar( Expr* l ){ + Expr* e0; + l->inc(); + Expr* e1 = l->followDefs()->get_head(); + Expr* e2; + e2 = e_pos; + e2->inc(); + Expr* e3; + e3 = e_neg; + e3->inc(); + if( e1==e2 ){ + Expr* x = ((CExpr*)l->followDefs())->kids[1]; + e0 = x; + e0->inc(); + }else if( e1==e3 ){ + Expr* x = ((CExpr*)l->followDefs())->kids[1]; + e0 = x; + e0->inc(); + }else{ + std::cout << "Could not find match for expression in function f_litvar "; + e1->print( std::cout ); + std::cout << std::endl; + exit( 1 ); + } + l->dec(); + e2->dec(); + e3->dec(); + return e0; +} + +Expr* f_litpol( Expr* l ){ + Expr* e0; + l->inc(); + Expr* e1 = l->followDefs()->get_head(); + Expr* e2; + e2 = e_pos; + e2->inc(); + Expr* e3; + e3 = e_neg; + e3->inc(); + if( e1==e2 ){ + Expr* x = ((CExpr*)l->followDefs())->kids[1]; + e0 = e_tt; + e0->inc(); + }else if( e1==e3 ){ + Expr* x = ((CExpr*)l->followDefs())->kids[1]; + e0 = e_ff; + e0->inc(); + }else{ + std::cout << "Could not find match for expression in function f_litpol "; + e1->print( std::cout ); + std::cout << std::endl; + exit( 1 ); + } + l->dec(); + e2->dec(); + e3->dec(); + return e0; +} + +Expr* f_notb( Expr* b ){ + Expr* e0; + b->inc(); + Expr* e1 = b->followDefs()->get_head(); + Expr* e2; + e2 = e_ff; + e2->inc(); + Expr* e3; + e3 = e_tt; + e3->inc(); + if( e1==e2 ){ + e0 = e_tt; + e0->inc(); + }else if( e1==e3 ){ + e0 = e_ff; + e0->inc(); + }else{ + std::cout << "Could not find match for expression in function f_notb "; + e1->print( std::cout ); + std::cout << std::endl; + exit( 1 ); + } + b->dec(); + e2->dec(); + e3->dec(); + return e0; +} + +Expr* f_iffb( Expr* b1, Expr* b2 ){ + Expr* e0; + b1->inc(); + Expr* e1 = b1->followDefs()->get_head(); + Expr* e2; + e2 = e_tt; + e2->inc(); + Expr* e3; + e3 = e_ff; + e3->inc(); + if( e1==e2 ){ + e0 = b2; + e0->inc(); + }else if( e1==e3 ){ + b2->inc(); + e0 = f_notb( b2 ); + b2->dec(); + }else{ + std::cout << "Could not find match for expression in function f_iffb "; + e1->print( std::cout ); + std::cout << std::endl; + exit( 1 ); + } + b1->dec(); + e2->dec(); + e3->dec(); + return e0; +} + +Expr* f_clear_mark( Expr* v ){ + Expr* e0; + v->inc(); + if ( ((SymExpr*)v->followDefs())->getmark(0)){ + v->inc(); + if ( ((SymExpr*)v->followDefs())->getmark(0)) + ((SymExpr*)v->followDefs())->clearmark(0); + else + ((SymExpr*)v->followDefs())->setmark(0); + e0 = v; + e0->inc(); + v->dec(); + }else{ + e0 = v; + e0->inc(); + } + v->dec(); + return e0; +} + +Expr* f_append( Expr* c1, Expr* c2 ){ + Expr* e0; + c1->inc(); + Expr* e1 = c1->followDefs()->get_head(); + Expr* e2; + e2 = e_cln; + e2->inc(); + Expr* e3; + e3 = e_clc; + e3->inc(); + if( e1==e2 ){ + e0 = c2; + e0->inc(); + }else if( e1==e3 ){ + Expr* l = ((CExpr*)c1->followDefs())->kids[1]; + Expr* c1h = ((CExpr*)c1->followDefs())->kids[2]; + l->inc(); + Expr* e4; + c1h->inc(); + c2->inc(); + e4 = f_append( c1h, c2 ); + c1h->dec(); + c2->dec(); + static Expr* e5; + e5 = e_clc; + e5->inc(); + e0 = new CExpr( APP, e5, l, e4 ); + }else{ + std::cout << "Could not find match for expression in function f_append "; + e1->print( std::cout ); + std::cout << std::endl; + exit( 1 ); + } + c1->dec(); + e2->dec(); + e3->dec(); + return e0; +} + +Expr* f_simplify_clause_h( Expr* pol, Expr* c ){ + Expr* e0; + c->inc(); + Expr* e1 = c->followDefs()->get_head(); + Expr* e2; + e2 = e_cln; + e2->inc(); + Expr* e3; + e3 = e_clc; + e3->inc(); + Expr* e4; + e4 = e_concat; + e4->inc(); + Expr* e5; + e5 = e_clr; + e5->inc(); + if( e1==e2 ){ + e0 = e_cln; + e0->inc(); + }else if( e1==e3 ){ + Expr* l = ((CExpr*)c->followDefs())->kids[1]; + Expr* c1 = ((CExpr*)c->followDefs())->kids[2]; + Expr* v; + l->inc(); + v = f_litvar( l ); + l->dec(); + Expr* e6; + Expr* e7; + l->inc(); + e7 = f_litpol( l ); + l->dec(); + pol->inc(); + e6 = f_iffb( e7, pol ); + e7->dec(); + pol->dec(); + Expr* e8 = e6->followDefs()->get_head(); + Expr* e9; + e9 = e_tt; + e9->inc(); + Expr* e10; + e10 = e_ff; + e10->inc(); + if( e8==e9 ){ + Expr* m; + v->inc(); + if ( ((SymExpr*)v->followDefs())->getmark(0)){ + m = e_tt; + m->inc(); + }else{ + Expr* e11; + v->inc(); + if ( ((SymExpr*)v->followDefs())->getmark(0)) + ((SymExpr*)v->followDefs())->clearmark(0); + else + ((SymExpr*)v->followDefs())->setmark(0); + e11 = v; + e11->inc(); + v->dec(); + e11->dec(); + m = e_ff; + m->inc(); + } + v->dec(); + Expr* ch; + pol->inc(); + c1->inc(); + ch = f_simplify_clause_h( pol, c1 ); + pol->dec(); + c1->dec(); + m->inc(); + Expr* e12 = m->followDefs()->get_head(); + Expr* e13; + e13 = e_tt; + e13->inc(); + Expr* e14; + e14 = e_ff; + e14->inc(); + if( e12==e13 ){ + Expr* e15; + v->inc(); + if ( ((SymExpr*)v->followDefs())->getmark(1)){ + e15 = v; + e15->inc(); + }else{ + v->inc(); + if ( ((SymExpr*)v->followDefs())->getmark(1)) + ((SymExpr*)v->followDefs())->clearmark(1); + else + ((SymExpr*)v->followDefs())->setmark(1); + e15 = v; + e15->inc(); + v->dec(); + } + v->dec(); + e15->dec(); + e0 = ch; + e0->inc(); + }else if( e12==e14 ){ + Expr* e16; + Expr* e17; + v->inc(); + if ( ((SymExpr*)v->followDefs())->getmark(1)){ + v->inc(); + if ( ((SymExpr*)v->followDefs())->getmark(1)) + ((SymExpr*)v->followDefs())->clearmark(1); + else + ((SymExpr*)v->followDefs())->setmark(1); + e17 = v; + e17->inc(); + v->dec(); + }else{ + e17 = v; + e17->inc(); + } + v->dec(); + e17->dec(); + v->inc(); + if ( ((SymExpr*)v->followDefs())->getmark(0)) + ((SymExpr*)v->followDefs())->clearmark(0); + else + ((SymExpr*)v->followDefs())->setmark(0); + e16 = v; + e16->inc(); + v->dec(); + e16->dec(); + l->inc(); + ch->inc(); + static Expr* e18; + e18 = e_clc; + e18->inc(); + e0 = new CExpr( APP, e18, l, ch ); + }else{ + std::cout << "Could not find match for expression in function f_simplify_clause_h "; + e12->print( std::cout ); + std::cout << std::endl; + exit( 1 ); + } + m->dec(); + e13->dec(); + e14->dec(); + ch->dec(); + m->dec(); + }else if( e8==e10 ){ + l->inc(); + Expr* e19; + pol->inc(); + c1->inc(); + e19 = f_simplify_clause_h( pol, c1 ); + pol->dec(); + c1->dec(); + static Expr* e20; + e20 = e_clc; + e20->inc(); + e0 = new CExpr( APP, e20, l, e19 ); + }else{ + std::cout << "Could not find match for expression in function f_simplify_clause_h "; + e8->print( std::cout ); + std::cout << std::endl; + exit( 1 ); + } + e6->dec(); + e9->dec(); + e10->dec(); + v->dec(); + }else if( e1==e4 ){ + Expr* c1 = ((CExpr*)c->followDefs())->kids[1]; + Expr* c2 = ((CExpr*)c->followDefs())->kids[2]; + pol->inc(); + Expr* e21 = pol->followDefs()->get_head(); + Expr* e22; + e22 = e_ff; + e22->inc(); + Expr* e23; + e23 = e_tt; + e23->inc(); + if( e21==e22 ){ + Expr* e24; + pol->inc(); + c1->inc(); + e24 = f_simplify_clause_h( pol, c1 ); + pol->dec(); + c1->dec(); + Expr* e25; + pol->inc(); + c2->inc(); + e25 = f_simplify_clause_h( pol, c2 ); + pol->dec(); + c2->dec(); + static Expr* e26; + e26 = e_concat; + e26->inc(); + e0 = new CExpr( APP, e26, e24, e25 ); + }else if( e21==e23 ){ + Expr* e27; + pol->inc(); + c1->inc(); + e27 = f_simplify_clause_h( pol, c1 ); + pol->dec(); + c1->dec(); + Expr* e28; + pol->inc(); + c2->inc(); + e28 = f_simplify_clause_h( pol, c2 ); + pol->dec(); + c2->dec(); + e0 = f_append( e27, e28 ); + e27->dec(); + e28->dec(); + }else{ + std::cout << "Could not find match for expression in function f_simplify_clause_h "; + e21->print( std::cout ); + std::cout << std::endl; + exit( 1 ); + } + pol->dec(); + e22->dec(); + e23->dec(); + }else if( e1==e5 ){ + Expr* l = ((CExpr*)c->followDefs())->kids[1]; + Expr* c1 = ((CExpr*)c->followDefs())->kids[2]; + Expr* e29; + Expr* e30; + l->inc(); + e30 = f_litpol( l ); + l->dec(); + pol->inc(); + e29 = f_iffb( e30, pol ); + e30->dec(); + pol->dec(); + Expr* e31 = e29->followDefs()->get_head(); + Expr* e32; + e32 = e_ff; + e32->inc(); + Expr* e33; + e33 = e_tt; + e33->inc(); + if( e31==e32 ){ + l->inc(); + Expr* e34; + pol->inc(); + c1->inc(); + e34 = f_simplify_clause_h( pol, c1 ); + pol->dec(); + c1->dec(); + static Expr* e35; + e35 = e_clr; + e35->inc(); + e0 = new CExpr( APP, e35, l, e34 ); + }else if( e31==e33 ){ + Expr* v; + l->inc(); + v = f_litvar( l ); + l->dec(); + Expr* m; + v->inc(); + if ( ((SymExpr*)v->followDefs())->getmark(0)){ + m = e_tt; + m->inc(); + }else{ + Expr* e36; + v->inc(); + if ( ((SymExpr*)v->followDefs())->getmark(0)) + ((SymExpr*)v->followDefs())->clearmark(0); + else + ((SymExpr*)v->followDefs())->setmark(0); + e36 = v; + e36->inc(); + v->dec(); + e36->dec(); + m = e_ff; + m->inc(); + } + v->dec(); + Expr* ch; + pol->inc(); + c1->inc(); + ch = f_simplify_clause_h( pol, c1 ); + pol->dec(); + c1->dec(); + v->inc(); + if ( ((SymExpr*)v->followDefs())->getmark(1)){ + m->inc(); + Expr* e37 = m->followDefs()->get_head(); + Expr* e38; + e38 = e_tt; + e38->inc(); + Expr* e39; + e39 = e_ff; + e39->inc(); + if( e37==e38 ){ + e0 = ch; + e0->inc(); + }else if( e37==e39 ){ + Expr* e40; + Expr* e41; + v->inc(); + if ( ((SymExpr*)v->followDefs())->getmark(1)) + ((SymExpr*)v->followDefs())->clearmark(1); + else + ((SymExpr*)v->followDefs())->setmark(1); + e41 = v; + e41->inc(); + v->dec(); + e41->dec(); + v->inc(); + if ( ((SymExpr*)v->followDefs())->getmark(0)) + ((SymExpr*)v->followDefs())->clearmark(0); + else + ((SymExpr*)v->followDefs())->setmark(0); + e40 = v; + e40->inc(); + v->dec(); + e40->dec(); + e0 = ch; + e0->inc(); + }else{ + std::cout << "Could not find match for expression in function f_simplify_clause_h "; + e37->print( std::cout ); + std::cout << std::endl; + exit( 1 ); + } + m->dec(); + e38->dec(); + e39->dec(); + }else{ + e0 = NULL; + } + v->dec(); + ch->dec(); + m->dec(); + v->dec(); + }else{ + std::cout << "Could not find match for expression in function f_simplify_clause_h "; + e31->print( std::cout ); + std::cout << std::endl; + exit( 1 ); + } + e29->dec(); + e32->dec(); + e33->dec(); + }else{ + std::cout << "Could not find match for expression in function f_simplify_clause_h "; + e1->print( std::cout ); + std::cout << std::endl; + exit( 1 ); + } + c->dec(); + e2->dec(); + e3->dec(); + e4->dec(); + e5->dec(); + return e0; +} + +Expr* f_simplify_clause( Expr* c ){ + Expr* e0; + static Expr* e1; + e1 = e_tt; + e1->inc(); + Expr* e2; + static Expr* e3; + e3 = e_ff; + e3->inc(); + c->inc(); + e2 = f_simplify_clause_h( e3, c ); + e3->dec(); + c->dec(); + e0 = f_simplify_clause_h( e1, e2 ); + e1->dec(); + e2->dec(); + return e0; +} + |