summaryrefslogtreecommitdiff
path: root/proofs/lfsc_checker/scccode.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'proofs/lfsc_checker/scccode.cpp')
-rw-r--r--proofs/lfsc_checker/scccode.cpp609
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;
+}
+
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback