diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-05-02 09:16:30 -0500 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-05-02 09:16:36 -0500 |
commit | f65b945119341ae8afa69bd0b7dc005c9fcc768b (patch) | |
tree | c264125578d3b8edd752740701789f7b1e4e26bb /proofs/lfsc_checker | |
parent | 53c301aa808218abe725014e01bddc19fe11a116 (diff) |
Clean up issues related to compiled scc in LFSC. Refactor --partial-trigger, do not combine quantifier prefixes with annotations. Eliminate use of context-dependent attributes in quantifiers.
Diffstat (limited to 'proofs/lfsc_checker')
-rw-r--r-- | proofs/lfsc_checker/scccode.cpp | 602 | ||||
-rw-r--r-- | proofs/lfsc_checker/scccode.h | 16 | ||||
-rw-r--r-- | proofs/lfsc_checker/sccwriter.cpp | 6 |
3 files changed, 5 insertions, 619 deletions
diff --git a/proofs/lfsc_checker/scccode.cpp b/proofs/lfsc_checker/scccode.cpp index 22f26ec88..19712579c 100644 --- a/proofs/lfsc_checker/scccode.cpp +++ b/proofs/lfsc_checker/scccode.cpp @@ -1,609 +1,11 @@ #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* run_compiled_scc( Expr* p, std::vector< Expr* >& args ){ + return NULL; } -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; -} diff --git a/proofs/lfsc_checker/scccode.h b/proofs/lfsc_checker/scccode.h index 6f5efc8b5..2ab549c10 100644 --- a/proofs/lfsc_checker/scccode.h +++ b/proofs/lfsc_checker/scccode.h @@ -7,21 +7,5 @@ void init_compiled_scc(); Expr* run_compiled_scc( Expr* p, std::vector< Expr* >& args ); -inline Expr* f_litvar( Expr* l ); - -inline Expr* f_litpol( Expr* l ); - -inline Expr* f_notb( Expr* b ); - -inline Expr* f_iffb( Expr* b1, Expr* b2 ); - -inline Expr* f_clear_mark( Expr* v ); - -inline Expr* f_append( Expr* c1, Expr* c2 ); - -inline Expr* f_simplify_clause_h( Expr* pol, Expr* c ); - -inline Expr* f_simplify_clause( Expr* c ); - #endif diff --git a/proofs/lfsc_checker/sccwriter.cpp b/proofs/lfsc_checker/sccwriter.cpp index 5c1da2a3f..d93341ab8 100644 --- a/proofs/lfsc_checker/sccwriter.cpp +++ b/proofs/lfsc_checker/sccwriter.cpp @@ -286,7 +286,7 @@ void sccwriter::write_code( Expr* code, std::ostream& os, int ind, const char* r { indent( os, ind ); os << retModString.c_str(); - os << "new IntExpr( " << mpz_get_si( ((IntExpr*)code)->n ) << " );" << std::endl; + os << "new IntExpr( (signed long int)" << mpz_get_si( ((IntExpr*)code)->n ) << " );" << std::endl; indent( os, ind ); os << incString.c_str() << std::endl; } @@ -527,7 +527,7 @@ void sccwriter::write_code( Expr* code, std::ostream& os, int ind, const char* r indent( os, ind ); os << "Expr* "; write_variable( ((SymSExpr*)((CExpr*)code)->kids[0])->s, os ); - os << ";" << std::endl; + 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() ); @@ -841,7 +841,7 @@ void sccwriter::write_expr( Expr* code, std::ostream& os, int ind, std::string& { os << "static "; } - os << "Expr* " << ss.str().c_str() << ";" << std::endl; + os << "Expr* " << ss.str().c_str() << " = NULL;" << std::endl; //write the expression std::ostringstream ss2; ss2 << ss.str().c_str(); |