summaryrefslogtreecommitdiff
path: root/proofs
diff options
context:
space:
mode:
Diffstat (limited to 'proofs')
-rw-r--r--proofs/lfsc_checker/check.cpp2
-rw-r--r--proofs/lfsc_checker/expr.cpp2
-rw-r--r--proofs/lfsc_checker/expr.h45
-rw-r--r--proofs/lfsc_checker/main.cpp1
-rw-r--r--proofs/signatures/th_bv_bitblast.plf38
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)))))
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback