diff options
Diffstat (limited to 'proofs')
-rw-r--r-- | proofs/lfsc_checker/check.cpp | 2 | ||||
-rw-r--r-- | proofs/lfsc_checker/expr.cpp | 2 | ||||
-rw-r--r-- | proofs/lfsc_checker/expr.h | 45 | ||||
-rw-r--r-- | proofs/lfsc_checker/main.cpp | 1 | ||||
-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 | ||||
-rw-r--r-- | proofs/signatures/Makefile.am | 3 | ||||
-rwxr-xr-x | proofs/signatures/th_arrays.plf | 2 | ||||
-rw-r--r-- | proofs/signatures/th_bv.plf | 46 | ||||
-rw-r--r-- | proofs/signatures/th_bv_bitblast.plf | 220 | ||||
-rw-r--r-- | proofs/signatures/th_bv_rewrites.plf | 22 | ||||
-rwxr-xr-x | proofs/signatures/th_quant.plf | 5 |
13 files changed, 233 insertions, 739 deletions
diff --git a/proofs/lfsc_checker/check.cpp b/proofs/lfsc_checker/check.cpp index c96791aeb..22e326cda 100644 --- a/proofs/lfsc_checker/check.cpp +++ b/proofs/lfsc_checker/check.cpp @@ -24,7 +24,7 @@ int colnum = 1; const char *filename = 0; FILE *curfile = 0; -//#define USE_HASH_MAPS +//#define USE_HASH_MAPS //AJR: deprecated symmap2 progs; std::vector< Expr* > ascHoles; diff --git a/proofs/lfsc_checker/expr.cpp b/proofs/lfsc_checker/expr.cpp index ae0e49531..5cb774fbf 100644 --- a/proofs/lfsc_checker/expr.cpp +++ b/proofs/lfsc_checker/expr.cpp @@ -34,7 +34,6 @@ bool destroy_progs = false; Expr *r = rr; \ int ref = r->data >> 9; \ ref = ref - 1; \ - r->debugrefcnt(ref,DEC); \ if (ref == 0) { \ _e = r; \ goto start_destroy; \ @@ -43,6 +42,7 @@ bool destroy_progs = false; 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: diff --git a/proofs/lfsc_checker/expr.h b/proofs/lfsc_checker/expr.h index 32a62ab33..5a505a3d9 100644 --- a/proofs/lfsc_checker/expr.h +++ b/proofs/lfsc_checker/expr.h @@ -8,9 +8,9 @@ #include <map> #include "chunking_memory_management.h" -#define USE_FLAT_APP +#define USE_FLAT_APP //AJR: off deprecated #define MARKVAR_32 -#define DEBUG_SYM_NAMES +//#define DEBUG_SYM_NAMES //#define DEBUG_SYMS // Expr class @@ -66,7 +66,6 @@ protected: enum { INC, DEC, CREATE }; void debugrefcnt(int ref, int what) { -#ifdef DEBUG_REFCNT std::cout << "["; debug(); switch(what) { @@ -83,10 +82,6 @@ protected: char tmp[10]; sprintf(tmp,"%d",ref); std::cout << tmp << "]\n"; -#else - (void)ref; - (void)what; -#endif } Expr(int _class, int _op) @@ -114,14 +109,18 @@ public: // std::cout << " " << ref << std::endl; //} ref = ref<4194303 ? ref + 1 : ref; +#ifdef DEBUG_REFCNT debugrefcnt(ref,INC); +#endif data = (ref << 9) | (data & 511); } static void destroy(Expr *, bool); inline void dec(bool dec_kids = true) { int ref = getrefcnt(); ref = ref - 1; +#ifdef DEBUG_REFCNT debugrefcnt(ref,DEC); +#endif if (ref == 0) destroy(this,dec_kids); else @@ -131,10 +130,10 @@ public: //must pass statType (the expr representing "type") to this function bool isType( Expr* statType ); - inline bool isDatatype() { + inline bool isDatatype() const { return getclass() == SYMS_EXPR || getop() == MPZ || getop() == MPQ; } - inline bool isArithTerm() { + inline bool isArithTerm() const { return getop() == ADD || getop() == NEG; } @@ -188,13 +187,17 @@ public: CExpr(int _op) : Expr(CEXPR, _op), kids() { kids = new Expr *[1]; kids[0] = 0; +#ifdef DEBUG_REFCNT debugrefcnt(1,CREATE); +#endif } CExpr(int _op, Expr *e1) : Expr(CEXPR, _op), kids() { kids = new Expr *[2]; kids[0] = e1; kids[1] = 0; +#ifdef DEBUG_REFCNT debugrefcnt(1,CREATE); +#endif } CExpr(int _op, Expr *e1, Expr *e2) : Expr(CEXPR, _op), kids() { @@ -202,7 +205,9 @@ public: kids[0] = e1; kids[1] = e2; kids[2] = 0; +#ifdef DEBUG_REFCNT debugrefcnt(1,CREATE); +#endif } CExpr(int _op, Expr *e1, Expr *e2, Expr *e3) : Expr(CEXPR, _op), kids() { @@ -211,7 +216,9 @@ public: kids[1] = e2; kids[2] = e3; kids[3] = 0; +#ifdef DEBUG_REFCNT debugrefcnt(1,CREATE); +#endif } CExpr(int _op, Expr *e1, Expr *e2, Expr *e3, Expr *e4) : Expr(CEXPR, _op), kids() { @@ -221,7 +228,9 @@ public: kids[2] = e3; kids[3] = e4; kids[4] = 0; +#ifdef DEBUG_REFCNT debugrefcnt(1,CREATE); +#endif } CExpr(int _op, const std::vector<Expr *> &_kids) : Expr(CEXPR, _op), kids() { @@ -230,13 +239,17 @@ public: for (i = 0; i < iend; i++) kids[i] = _kids[i]; kids[i] = 0; +#ifdef DEBUG_REFCNT debugrefcnt(1,CREATE); +#endif } // _kids must be null-terminated. CExpr(int _op, bool dummy, Expr **_kids) : Expr(CEXPR, _op), kids(_kids) { (void)dummy; +#ifdef DEBUG_REFCNT debugrefcnt(1,CREATE); +#endif } Expr *whr(); @@ -253,7 +266,9 @@ class IntExpr : public Expr { } IntExpr(mpz_t _n) : Expr(INT_EXPR, 0), n() { mpz_init_set(n,_n); +#ifdef DEBUG_REFCNT debugrefcnt(1,CREATE); +#endif } IntExpr(signed long int _n ) : Expr(INT_EXPR, 0), n() { mpz_init_set_si( n, _n ); @@ -271,7 +286,9 @@ class RatExpr : public Expr { RatExpr(mpq_t _n) : Expr(RAT_EXPR, 0), n() { mpq_init( n ); mpq_set(n,_n); +#ifdef DEBUG_REFCNT debugrefcnt(1,CREATE); +#endif mpq_canonicalize( n ); } RatExpr(signed long int _n1, unsigned long int _n2 ) : Expr(RAT_EXPR, 0), n() { @@ -290,15 +307,19 @@ class SymExpr : public Expr { : Expr(theclass, 0), val(0) { (void)_s; +#ifdef DEBUG_REFCNT if (theclass == SYM_EXPR) debugrefcnt(1,CREATE); +#endif } SymExpr(const SymExpr &e, int theclass = SYM_EXPR) : Expr(theclass, 0), val(0) { (void)e; +#ifdef DEBUG_REFCNT if (theclass == SYM_EXPR) debugrefcnt(1,CREATE); +#endif } #ifdef MARKVAR_32 private: @@ -317,12 +338,16 @@ class SymSExpr : public SymExpr { SymSExpr(std::string _s, int theclass = SYMS_EXPR) : SymExpr(_s, theclass), s(_s) { +#ifdef DEBUG_REFCNT debugrefcnt(1,CREATE); +#endif } SymSExpr(const SymSExpr &e, int theclass = SYMS_EXPR) : SymExpr(e, theclass), s(e.s) { +#ifdef DEBUG_REFCNT debugrefcnt(1,CREATE); +#endif } }; @@ -338,7 +363,9 @@ public: #ifdef DEBUG_HOLE_NAMES id = next_id++; #endif +#ifdef DEBUG_REFCNT debugrefcnt(1,CREATE); +#endif } Expr *val; // may be set during subst(), defeq(), and clone(). }; diff --git a/proofs/lfsc_checker/main.cpp b/proofs/lfsc_checker/main.cpp index 80f36e69f..1d8ba5809 100644 --- a/proofs/lfsc_checker/main.cpp +++ b/proofs/lfsc_checker/main.cpp @@ -133,6 +133,7 @@ int main(int argc, char **argv) { a.files.clear(); #endif + std::cout << "Proof checked successfully!" << std::endl << std::endl; std::cout << "time = " << (int)clock() - check_time << std::endl; std::cout << "sym count = " << SymExpr::symmCount << std::endl; std::cout << "marked count = " << Expr::markedCount << std::endl; 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(); diff --git a/proofs/signatures/Makefile.am b/proofs/signatures/Makefile.am index 2b6d16cfd..5947ad3f0 100644 --- a/proofs/signatures/Makefile.am +++ b/proofs/signatures/Makefile.am @@ -3,7 +3,8 @@ # add support for more theories, just list them here in the same order # you would to the LFSC proof-checker binary. # -CORE_PLFS = sat.plf smt.plf th_base.plf th_arrays.plf th_bv.plf th_bv_bitblast.plf th_real.plf th_int.plf + +CORE_PLFS = sat.plf smt.plf th_base.plf th_arrays.plf th_bv.plf th_bv_bitblast.plf th_bv_rewrites.plf th_real.plf th_int.plf noinst_LTLIBRARIES = libsignatures.la diff --git a/proofs/signatures/th_arrays.plf b/proofs/signatures/th_arrays.plf index 5ed3d2f6f..b54a4ed5b 100755 --- a/proofs/signatures/th_arrays.plf +++ b/proofs/signatures/th_arrays.plf @@ -60,4 +60,4 @@ (! u1 (! k (term s1) (! u2 (th_holds (or (= _ t1 t2) (not (= _ (apply _ _ (apply _ _ (read s1 s2) t1) k) (apply _ _ (apply _ _ (read s1 s2) t2) k))))) (holds cln))) - (holds cln))))))) + (holds cln)))))))
\ No newline at end of file diff --git a/proofs/signatures/th_bv.plf b/proofs/signatures/th_bv.plf index c93541085..6012e052a 100644 --- a/proofs/signatures/th_bv.plf +++ b/proofs/signatures/th_bv.plf @@ -8,7 +8,7 @@ (program mp_ispos ((x mpz)) formula (mp_ifneg x false true)) - + (program mpz_eq ((x mpz) (y mpz)) formula (mp_ifzero (mpz_sub x y) true false)) @@ -21,7 +21,7 @@ (program mpz_ ((x mpz) (y mpz)) formula (mp_ifzero (mpz_sub x y) true false)) - + ; "bitvec" is a term of type "sort" ; (declare BitVec sort) (declare BitVec (!n mpz sort)) @@ -37,7 +37,7 @@ (declare bvc (! b bit (! v bv bv))) ; calculate the length of a bitvector -;; (program bv_len ((v bv)) mpz +;; (program bv_len ((v bv)) mpz ;; (match v ;; (bvn 0) ;; ((bvc b v') (mp_add (bv_len v') 1)))) @@ -48,7 +48,26 @@ (! n mpz (! v bv (term (BitVec n))))) - + +(program bv_constants_are_disequal ((x bv) (y bv)) formula + (match x + (bvn (fail formula)) + ((bvc bx x') + (match y + (bvn (fail formula)) + ((bvc by y') (match bx + (b0 (match by (b0 (bv_constants_are_disequal x' y')) (b1 (true)))) + (b1 (match by (b0 (true)) (b1 (bv_constants_are_disequal x' y')))) + )) + )) +)) + +(declare bv_disequal_constants + (! n mpz + (! x bv + (! y bv + (! c (^ (bv_constants_are_disequal x y) true) + (th_holds (not (= (BitVec n) (a_bv n x) (a_bv n y))))))))) ; a bv variable (declare var_bv type) @@ -61,7 +80,7 @@ ; bit vector binary operators (define bvop2 (! n mpz - (! x (term (BitVec n)) + (! x (term (BitVec n)) (! y (term (BitVec n)) (term (BitVec n)))))) @@ -88,7 +107,7 @@ ; bit vector unary operators (define bvop1 (! n mpz - (! x (term (BitVec n)) + (! x (term (BitVec n)) (term (BitVec n))))) @@ -111,8 +130,8 @@ (! t1 (term (BitVec m)) (! t2 (term (BitVec m')) (term (BitVec n)))))))) - -;; side-condition fails in signature only?? + +;; side-condition fails in signature only?? ;; (! s (^ (mp_add m m') n) ;; (declare repeat bvopp) @@ -147,22 +166,22 @@ (term (BitVec n))))))) - -;; TODO: add checks for valid typing for these operators + +;; TODO: add checks for valid typing for these operators ;; (! c1 (^ (mpz_lte i j) ;; (! c2 (^ (mpz_lt i n) true) ;; (! c3 (^ (mp_ifneg i false true) true) -;; (! c4 (^ (mp_ifneg j false true) true) +;; (! c4 (^ (mp_ifneg j false true) true) ;; (! s (^ (mp_add (mpz_sub i j) 1) m) - + ; bit vector predicates (define bvpred (! n mpz (! x (term (BitVec n)) (! y (term (BitVec n)) formula)))) - + (declare bvult bvpred) (declare bvule bvpred) (declare bvugt bvpred) @@ -171,4 +190,3 @@ (declare bvsle bvpred) (declare bvsgt bvpred) (declare bvsge bvpred) - diff --git a/proofs/signatures/th_bv_bitblast.plf b/proofs/signatures/th_bv_bitblast.plf index 8e8c51857..3cc1ec296 100644 --- a/proofs/signatures/th_bv_bitblast.plf +++ b/proofs/signatures/th_bv_bitblast.plf @@ -4,7 +4,7 @@ (declare bbltc (! f formula (! v bblt bblt))) ; calculate the length of a bit-blasted term -(program bblt_len ((v bblt)) mpz +(program bblt_len ((v bblt)) mpz (match v (bbltn 0) ((bbltc b v') (mp_add (bblt_len v') 1)))) @@ -25,6 +25,7 @@ (bblast_term n x y))))) +; Binds a symbol to the bblast_term to be used later on. (declare decl_bblast (! n mpz (! b bblt @@ -34,6 +35,16 @@ (! u (! v (bblast_term n t b) (holds cln)) (holds cln)))))))) +(declare decl_bblast_with_alias + (! n mpz + (! b bblt + (! t (term (BitVec n)) + (! a (term (BitVec n)) + (! bb (bblast_term n t b) + (! e (th_holds (= _ t a)) + (! s (^ (bblt_len b) n) + (! u (! v (bblast_term n a b) (holds cln)) + (holds cln)))))))))) ; a predicate to represent the n^th bit of a bitvector term (declare bitof @@ -46,31 +57,31 @@ ;; BITBLASTING RULES ;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; BITBLAST CONSTANT ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; (program bblast_const ((v bv) (n mpz)) bblt - (mp_ifneg n (match v (bvn bbltn) + (mp_ifneg n (match v (bvn bbltn) (default (fail bblt))) (match v ((bvc b v') (bbltc (match b (b0 false) (b1 true)) (bblast_const v' (mp_add n (~ 1))))) (default (fail bblt))))) - + (declare bv_bbl_const (! n mpz (! f bblt (! v bv (! c (^ (bblast_const v (mp_add n (~ 1))) f) (bblast_term n (a_bv n v) f)))))) - + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; BITBLAST VARIABLE ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; (program bblast_var ((x var_bv) (n mpz)) bblt - (mp_ifneg n bbltn + (mp_ifneg n bbltn (bbltc (bitof x n) (bblast_var x (mp_add n (~ 1)))))) (declare bv_bbl_var (! n mpz @@ -79,18 +90,16 @@ (! c (^ (bblast_var x (mp_add n (~ 1))) f) (bblast_term n (a_var_bv n x) f)))))) - ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; BITBLAST CONCAT ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; (program bblast_concat ((x bblt) (y bblt)) bblt - (match x + (match x (bbltn (match y ((bbltc by y') (bbltc by (bblast_concat x y'))) (bbltn bbltn))) ((bbltc bx x') (bbltc bx (bblast_concat x' y))))) - - + (declare bv_bbl_concat (! n mpz (! m mpz (! m1 mpz @@ -104,36 +113,34 @@ (! c (^ (bblast_concat xb yb ) rb) (bblast_term n (concat n m m1 x y) rb))))))))))))) - ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; BITBLAST EXTRACT ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; (program bblast_extract_rec ((x bblt) (i mpz) (j mpz) (n mpz)) bblt - (match x + (match x ((bbltc bx x') (mp_ifneg (mpz_sub (mpz_sub j n) 1) (mp_ifneg (mpz_sub (mpz_sub n i) 1) (bbltc bx (bblast_extract_rec x' i j (mpz_sub n 1))) (bblast_extract_rec x' i j (mpz_sub n 1))) - + bbltn)) (bbltn bbltn))) (program bblast_extract ((x bblt) (i mpz) (j mpz) (n mpz)) bblt - (bblast_extract_rec x i j (mpz_sub n 1))) + (bblast_extract_rec x i j (mpz_sub n 1))) (declare bv_bbl_extract (! n mpz (! i mpz (! j mpz (! m mpz - (! x (term (BitVec m)) + (! x (term (BitVec m)) (! xb bblt (! rb bblt (! xbb (bblast_term m x xb) (! c ( ^ (bblast_extract xb i j m) rb) (bblast_term n (extract n i j m x) rb))))))))))) - ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; BITBLAST ZERO/SIGN EXTEND ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; @@ -148,42 +155,38 @@ (declare bv_bbl_zero_extend (! n mpz (! k mpz (! m mpz - (! x (term (BitVec m)) + (! x (term (BitVec m)) (! xb bblt (! rb bblt (! xbb (bblast_term m x xb) (! c ( ^ (bblast_zextend xb k m) rb) (bblast_term n (zero_extend n k m x) rb)))))))))) - (program bblast_sextend ((x bblt) (i mpz)) bblt (match x (bbltn (fail bblt)) - ((bbltc xb x') (extend_rec x (mpz_sub i 1) xb)))) + ((bbltc xb x') (extend_rec x (mpz_sub i 1) xb)))) (declare bv_bbl_sign_extend (! n mpz (! k mpz (! m mpz - (! x (term (BitVec m)) + (! x (term (BitVec m)) (! xb bblt (! rb bblt (! xbb (bblast_term m x xb) (! c ( ^ (bblast_sextend xb k m) rb) (bblast_term n (sign_extend n k m x) rb)))))))))) - - - + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; BITBLAST BVAND ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - + (program bblast_bvand ((x bblt) (y bblt)) bblt - (match x + (match x (bbltn (match y (bbltn bbltn) (default (fail bblt)))) - ((bbltc bx x') (match y + ((bbltc bx x') (match y (bbltn (fail bblt)) ((bbltc by y') (bbltc (and bx by) (bblast_bvand x' y'))))))) - - + (declare bv_bbl_bvand (! n mpz (! x (term (BitVec n)) (! y (term (BitVec n)) @@ -199,11 +202,10 @@ ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; (program bblast_bvnot ((x bblt)) bblt - (match x - (bbltn bbltn) + (match x + (bbltn bbltn) ((bbltc bx x') (bbltc (not bx) (bblast_bvnot x'))))) - - + (declare bv_bbl_bvnot (! n mpz (! x (term (BitVec n)) (! xb bblt @@ -215,15 +217,14 @@ ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; BITBLAST BVOR ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - + (program bblast_bvor ((x bblt) (y bblt)) bblt - (match x + (match x (bbltn (match y (bbltn bbltn) (default (fail bblt)))) - ((bbltc bx x') (match y + ((bbltc bx x') (match y (bbltn (fail bblt)) ((bbltc by y') (bbltc (or bx by) (bblast_bvor x' y'))))))) - - + (declare bv_bbl_bvor (! n mpz (! x (term (BitVec n)) (! y (term (BitVec n)) @@ -238,15 +239,14 @@ ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; BITBLAST BVXOR ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - + (program bblast_bvxor ((x bblt) (y bblt)) bblt - (match x + (match x (bbltn (match y (bbltn bbltn) (default (fail bblt)))) - ((bbltc bx x') (match y + ((bbltc bx x') (match y (bbltn (fail bblt)) ((bbltc by y') (bbltc (xor bx by) (bblast_bvxor x' y'))))))) - - + (declare bv_bbl_bvxor (! n mpz (! x (term (BitVec n)) (! y (term (BitVec n)) @@ -262,8 +262,8 @@ ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; BITBLAST BVADD ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - -;; return the carry bit after adding x y + +;; return the carry bit after adding x y ;; FIXME: not the most efficient thing in the world (program bblast_bvadd_carry ((a bblt) (b bblt) (carry formula)) formula (match a @@ -272,7 +272,7 @@ (bbltn (fail formula)) ((bbltc bi b') (or (and ai bi) (and (xor ai bi) (bblast_bvadd_carry a' b' carry)))))))) -;; ripple carry adder where carry is the initial carry bit +;; ripple carry adder where carry is the initial carry bit (program bblast_bvadd ((a bblt) (b bblt) (carry formula)) bblt (match a ( bbltn (match b (bbltn bbltn) (default (fail bblt)))) @@ -280,8 +280,35 @@ (bbltn (fail bblt)) ((bbltc bi b') (bbltc (xor (xor ai bi) (bblast_bvadd_carry a' b' carry)) (bblast_bvadd a' b' carry))))))) - - + + +(program reverse_help ((x bblt) (acc bblt)) bblt +(match x + (bbltn acc) + ((bbltc xi x') (reverse_help x' (bbltc xi acc))))) + + +(program reverseb ((x bblt)) bblt + (reverse_help x bbltn)) + + +; AJR: use this version? +;(program bblast_bvadd_2h ((a bblt) (b bblt) (carry formula)) bblt +;(match a +; ( bbltn (match b (bbltn bbltn) (default (fail bblt)))) +; ((bbltc ai a') (match b +; (bbltn (fail bblt)) +; ((bbltc bi b') +; (let carry' (or (and ai bi) (and (xor ai bi) carry)) +; (bbltc (xor (xor ai bi) carry) +; (bblast_bvadd_2h a' b' carry')))))))) + +;(program bblast_bvadd_2 ((a bblt) (b bblt) (carry formula)) bblt +;(let ar (reverseb a) ;; reverse a and b so that we can build the circuit +;(let br (reverseb b) ;; from the least significant bit up +;(let ret (bblast_bvadd_2h ar br carry) +; (reverseb ret))))) + (declare bv_bbl_bvadd (! n mpz (! x (term (BitVec n)) (! y (term (BitVec n)) @@ -293,7 +320,6 @@ (! c (^ (bblast_bvadd xb yb false) rb) (bblast_term n (bvadd n x y) rb))))))))))) - ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; BITBLAST BVNEG ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; @@ -304,8 +330,8 @@ (program bblast_bvneg ((x bblt) (n mpz)) bblt (bblast_bvadd (bblast_bvnot x) (bblast_zero n) true)) - - + + (declare bv_bbl_bvneg (! n mpz (! x (term (BitVec n)) (! xb bblt @@ -319,23 +345,14 @@ ;; BITBLAST BVMUL ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - -;; shift add multiplier - -(program reverse_help ((x bblt) (acc bblt)) bblt -(match x - (bbltn acc) - ((bbltc xi x') (reverse_help x' (bbltc xi acc))))) - -(program reverseb ((x bblt)) bblt - (reverse_help x bbltn)) +;; shift add multiplier ;; (program concat ((a bblt) (b bblt)) bblt ;; (match a (bbltn b) ;; ((bbltc ai a') (bbltc ai (concat a' b))))) - + (program top_k_bits ((a bblt) (k mpz)) bblt (mp_ifzero k bbltn (match a (bbltn (fail bblt)) @@ -344,7 +361,7 @@ (program bottom_k_bits ((a bblt) (k mpz)) bblt (reverseb (top_k_bits (reverseb a) k))) -;; assumes the least signigicant bit is at the beginning of the list +;; assumes the least signigicant bit is at the beginning of the list (program k_bit ((a bblt) (k mpz)) formula (mp_ifneg k (fail formula) (match a (bbltn (fail formula)) @@ -353,7 +370,7 @@ (program and_with_bit ((a bblt) (bt formula)) bblt (match a (bbltn bbltn) ((bbltc ai a') (bbltc (and bt ai) (and_with_bit a' bt))))) - + ;; a is going to be the current result ;; carry is going to be false initially ;; b is the and of a and b[k] @@ -377,19 +394,19 @@ (let ak (top_k_bits a k') (let b' (and_with_bit ak (k_bit b k)) (mp_ifzero (mpz_sub k' 1) - (mult_step_k_h res b' bbltn false k) + (mult_step_k_h res b' bbltn false k) (let res' (mult_step_k_h res b' bbltn false k) (mult_step a b (reverseb res') n (mp_add k 1)))))))) (program bblast_bvmul ((a bblt) (b bblt) (n mpz)) bblt -(let ar (reverseb a) ;; reverse a and b so that we can build the circuit +(let ar (reverseb a) ;; reverse a and b so that we can build the circuit (let br (reverseb b) ;; from the least significant bit up (let res (and_with_bit ar (k_bit br 0)) - (mp_ifzero (mpz_sub n 1) ;; if multiplying 1 bit numbers no need to call mult_step + (mp_ifzero (mpz_sub n 1) ;; if multiplying 1 bit numbers no need to call mult_step res (mult_step ar br res n 1)))))) - + (declare bv_bbl_bvmul (! n mpz (! x (term (BitVec n)) (! y (term (BitVec n)) @@ -402,18 +419,18 @@ (bblast_term n (bvmul n x y) rb))))))))))) - + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; BITBLAST EQUALS ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - + ; bit blast x = y ; for x,y of size n, it will return a conjuction (x.0 = y.0 ^ ( ... ^ (x.{n-1} = y.{n-1}))) ; f is the accumulator formula that builds the equality in the right order (program bblast_eq_rec ((x bblt) (y bblt) (f formula)) formula - (match x + (match x (bbltn (match y (bbltn f) (default (fail formula)))) - ((bbltc fx x') (match y + ((bbltc fx x') (match y (bbltn (fail formula)) ((bbltc fy y') (bblast_eq_rec x' y' (and (iff fx fy) f))))) (default (fail formula)))) @@ -423,7 +440,23 @@ ((bbltc bx x') (match y ((bbltc by y') (bblast_eq_rec x' y' (iff bx by))) (default (fail formula)))) (default (fail formula)))) - + + +;; TODO: a temporary bypass for rewrites that we don't support yet. As soon +;; as we do, remove this rule. + +(declare bv_bbl_=_false + (! n mpz + (! x (term (BitVec n)) + (! y (term (BitVec n)) + (! bx bblt + (! by bblt + (! f formula + (! bbx (bblast_term n x bx) + (! bby (bblast_term n y by) + (! c (^ (bblast_eq bx by) f) + (th_holds (iff (= (BitVec n) x y) false)))))))))))) + (declare bv_bbl_= (! n mpz (! x (term (BitVec n)) @@ -436,11 +469,22 @@ (! c (^ (bblast_eq bx by) f) (th_holds (iff (= (BitVec n) x y) f)))))))))))) - +(declare bv_bbl_=_swap + (! n mpz + (! x (term (BitVec n)) + (! y (term (BitVec n)) + (! bx bblt + (! by bblt + (! f formula + (! bbx (bblast_term n x bx) + (! bby (bblast_term n y by) + (! c (^ (bblast_eq by bx) f) + (th_holds (iff (= (BitVec n) x y) f)))))))))))) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; BITBLAST BVULT ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - + (program bblast_bvult ((x bblt) (y bblt) (n mpz)) formula (match x ( bbltn (fail formula)) @@ -465,7 +509,7 @@ ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; BITBLAST BVSLT ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - + (program bblast_bvslt ((x bblt) (y bblt) (n mpz)) formula (match x ( bbltn (fail formula)) @@ -488,7 +532,6 @@ (! bby (bblast_term n y by) (! c (^ (bblast_bvslt bx by n) f) (th_holds (iff (bvslt n x y) f)))))))))))) - ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; @@ -525,8 +568,8 @@ ;; REWRITE RULES ;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - - + + ; rewrite rule : ; x + y = y + x (declare bvadd_symm @@ -534,7 +577,7 @@ (! x (term (BitVec n)) (! y (term (BitVec n)) (th_holds (= (BitVec n) (bvadd _ x y) (bvadd _ y x))))))) - + ;; (declare bvcrazy_rewrite ;; (! n mpz ;; (! x (term (BitVec n)) @@ -546,12 +589,12 @@ ;; (! s (^ (rewrite_scc xn yn) true) ;; (! u (! x (term (BitVec n)) (holds cln)) ;; (holds cln))))))))))) - + ;; (th_holds (= (BitVec n) (bvadd x y) (bvadd y x))))))) - - -; necessary? + + +; necessary? ;; (program calc_bvand ((a bv) (b bv)) bv ;; (match a ;; (bvn (match b (bvn bvn) (default (fail bv)))) @@ -560,7 +603,7 @@ ;; (default (fail bv)))))) ;; ; rewrite rule (w constants) : -;; ; a & b = c +;; ; a & b = c ;; (declare bvand_const (! c bv ;; (! a bv ;; (! b bv @@ -568,7 +611,7 @@ ;; (th_holds (= BitVec (bvand (a_bv a) (a_bv b)) (a_bv c)))))))) -;; making constant bit-vectors +;; making constant bit-vectors (program mk_ones ((n mpz)) bv (mp_ifzero n bvn (bvc b1 (mk_ones (mpz_sub n 1))))) @@ -576,7 +619,7 @@ (mp_ifzero n bvn (bvc b0 (mk_ones (mpz_sub n 1))))) - + ;; (bvxnor a b) => (bvnot (bvxor a b)) ;; (declare bvxnor_elim ;; (! n mpz @@ -603,7 +646,7 @@ ;; (! rwb (rw_term _ b (a_bv _ zero_bits)) ;; (rw_term _ (bvxor _ a b) ;; a')))))))))) - + ;; ;; (bvxor a 11) => (bvnot a) ;; (declare bvxor_one ;; (! n mpz @@ -617,7 +660,7 @@ ;; (rw_term _ (bvxor _ a b) ;; (bvnot _ a'))))))))))) - + ;; ;; (bvnot (bvnot a)) => a ;; (declare bvnot_idemp ;; (! n mpz @@ -626,4 +669,3 @@ ;; (! rwa (rw_term _ a a') ;; (rw_term _ (bvnot _ (bvnot _ a)) ;; a')))))) - diff --git a/proofs/signatures/th_bv_rewrites.plf b/proofs/signatures/th_bv_rewrites.plf new file mode 100644 index 000000000..bf5dea9e9 --- /dev/null +++ b/proofs/signatures/th_bv_rewrites.plf @@ -0,0 +1,22 @@ +; +; Equality swap +; + +(declare rr_bv_eq + (! n mpz + (! t1 (term (BitVec n)) + (! t2 (term (BitVec n)) + (th_holds (iff (= (BitVec n) t2 t1) (= (BitVec n) t1 t2))))))) + +; +; Additional rules... +; + +; +; Default, if nothing else applied +; + +(declare rr_bv_default + (! t1 formula + (! t2 formula + (th_holds (iff t1 t2)))))) diff --git a/proofs/signatures/th_quant.plf b/proofs/signatures/th_quant.plf index d85b2115c..e212f835d 100755 --- a/proofs/signatures/th_quant.plf +++ b/proofs/signatures/th_quant.plf @@ -14,10 +14,7 @@ (match ti ((apply si1 si2 ti1 ti2) (match (is_inst_t ti1 t1 k) (tt (is_inst_t ti2 t2 k)) (ff ff))) (default ff))) - (default - (match ti - ((apply si1 si2 ti1 ti2) ff) - (default (eqterm ti (ifmarked t k t))))))) + (default (eqterm ti (ifmarked t k t))))) (program is_inst_f ((fi formula) (f formula) (k term)) bool (match f |