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.

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)))))