diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-05-05 18:44:47 -0500 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-05-05 18:44:56 -0500 |
commit | c87ee73ad3d51c238700f236c18e425b80e8e7ac (patch) | |
tree | aa4214b0fa7d6ef275605253fee88899fa3ce230 /proofs | |
parent | a2923ec61b601b0e3f4f78f22fffc1c2421f0d81 (diff) |
Compute term indices lazily in TermDb. Optimization for qcf to recognize irrelevant quantifiers based on irrelevant functions. Fix rewriter for prefix merges. Minor optimizations for LFSC. Work on --literal-matching. Updates to inst propagate, move instantiation filtering within qe. Enable sygus for string inputs.
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/signatures/th_bv_bitblast.plf | 38 |
5 files changed, 67 insertions, 21 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/signatures/th_bv_bitblast.plf b/proofs/signatures/th_bv_bitblast.plf index 8e8c51857..580b54418 100644 --- a/proofs/signatures/th_bv_bitblast.plf +++ b/proofs/signatures/th_bv_bitblast.plf @@ -280,7 +280,34 @@ (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)) @@ -322,15 +349,6 @@ ;; 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)) - ;; (program concat ((a bblt) (b bblt)) bblt ;; (match a (bbltn b) ;; ((bbltc ai a') (bbltc ai (concat a' b))))) |