Check for non-constant bv rotate btor2 frontend

Correct y2 rotate by fixed amount

Refer #10

src/dpa/avr_word_netlist.cpp

@@ -875,11 +875,11 @@ Inst* OpInst::create(OpInst::OpType op, InstL exps, int o_size, bool to_simplify
 // 			assert(0);
 // 		}
 // 	}
-	if (op == BitWiseNand || op == BitWiseNor) {
-		string temp = op == BitWiseNand ? "BitWiseNand" : "BitWiseNor";
-		cout << temp << endl << exps << endl;
-		assert(0);
-	}
+	// if (op == BitWiseNand || op == BitWiseNor) {
+	// 	string temp = op == BitWiseNand ? "BitWiseNand" : "BitWiseNor";
+	// 	cout << temp << endl << exps << endl;
+	// 	assert(0);
+	// }
 
 	// 	if(op == BitWiseXor || op == LogXor){
 	// 		string temp = op == BitWiseXor ? "BitWiseXor" : "LogXor";

src/reach/avr_word_netlist.cpp

@@ -1919,11 +1919,11 @@ Inst* OpInst::create(OpInst::OpType op, InstL exps, int o_size, bool to_simplify
 		}
 	}
 
-	if (op == BitWiseNand || op == BitWiseNor) {
-		string temp = op == BitWiseNand ? "BitWiseNand" : "BitWiseNor";
-		cout << temp << endl << exps << endl;
-		assert(0);
-	}
+	// if (op == BitWiseNand || op == BitWiseNor) {
+	// 	string temp = op == BitWiseNand ? "BitWiseNand" : "BitWiseNor";
+	// 	cout << temp << endl << exps << endl;
+	// 	assert(0);
+	// }
 
 	if (Config::g_uf_no_bitwise)
 	if (op == BitWiseNot || op == BitWiseAnd || op == BitWiseOr) {

src/reach/reach_bt.cpp

@@ -2364,10 +2364,12 @@ void bt_API::inst2yices(Inst*e, bool bvAllConstraints) {
 						res = boolector_not(g_ctx, res);
 				}
 					break;
+				case OpInst::RotateR:
 				case OpInst::VRotateR:{
 					bt_loge("TODO");
 				}
 				  break;
+				case OpInst::RotateL:
 				case OpInst::VRotateL:{
 					bt_loge("TODO");
 				}

src/reach/reach_m5.cpp

@@ -3188,10 +3188,12 @@ void m5_API::inst2yices(Inst*e, bool bvAllConstraints) {
 					res = bit;
 				}
 					break;
+				case OpInst::RotateR:
 				case OpInst::VRotateR:{
 					m5_loge("TODO");
 				}
 				  break;
+				case OpInst::RotateL:
 				case OpInst::VRotateL:{
 					m5_loge("TODO");
 				}

src/reach/reach_y2.cpp

@@ -1781,7 +1781,10 @@ void y2_API::add_variable(y2_expr& lhs, Inst*e) {
 }
 
 void y2_API::add_gate_constraint(y2_expr& lhs, y2_expr_ptr rhs, std::string comment, Inst*e, bool asConstraint, bool checkType) {
-	assert(rhs != Y2_INVALID_EXPR);
+	if (rhs == Y2_INVALID_EXPR) {
+		cout << "Error encountered for " << *e << " with comment: " << comment << endl;
+		assert(0);
+	}
 
 	if (checkType) {
 		if (e->get_sort_type() == bvtype) {
@@ -7209,6 +7212,35 @@ void y2_API::inst2yices(Inst*e, bool bvAllConstraints)
 					res = bit;
 				}
 					break;
+
+				case OpInst::RotateL:
+				case OpInst::RotateR: {
+					assert(y_ch.size() == 2);
+					InstL::const_iterator ve_it = ch->begin(), ve_it2 = ch->begin();
+					ve_it2++;
+					NumInst* num = NumInst::as(*ve_it2);
+					// cout << "Rotate: " << *e << endl;
+					if (num != 0)
+					{
+						int rotate_amount = num->get_mpz()->get_si() % e->get_size();
+						// cout << "rotate_amount: " << rotate_amount << endl;
+						if (rotate_amount != 0) {
+							if (o == OpInst::RotateL)
+							{
+								res = yices_rotate_left(a, rotate_amount);
+							} else {
+								res = yices_rotate_right(a, rotate_amount);
+							}
+						} else {
+							res = a;
+						}
+					} else {
+						cout << "Expected second operand as number in " << *e << endl;
+						assert(0);
+					}
+					assert(res != -1);
+				}
+					break;
 				case OpInst::VRotateR:{
 					const InstL* ch = e->get_children();
 					InstL::const_iterator ve_it = ch->begin();
@@ -7364,6 +7396,7 @@ void y2_API::inst2yices(Inst*e, bool bvAllConstraints)
 					break;
 				}
 				default:
+					cout << "Error converting expression to yices equivalent: " << *e << endl;
 					assert(0);
 				}
 			} else if (m_mapper->fetch_op(e) == TheoryMapper::EUF_OP || m_mapper->fetch_op(e) == TheoryMapper::CLU_OP) {

src/vwn/avr_word_netlist.cpp

@@ -906,11 +906,11 @@ Inst* OpInst::create(OpInst::OpType op, InstL exps, int o_size, bool to_simplify
 // 			assert(0);
 // 		}
 // 	}
-	if (op == BitWiseNand || op == BitWiseNor) {
-		string temp = op == BitWiseNand ? "BitWiseNand" : "BitWiseNor";
-		cout << temp << endl << exps << endl;
-		assert(0);
-	}
+	// if (op == BitWiseNand || op == BitWiseNor) {
+	// 	string temp = op == BitWiseNand ? "BitWiseNand" : "BitWiseNor";
+	// 	cout << temp << endl << exps << endl;
+	// 	assert(0);
+	// }
 
 	// 	if(op == BitWiseXor || op == LogXor){
 	// 		string temp = op == BitWiseXor ? "BitWiseXor" : "LogXor";

src/vwn/btor2_frontend.cpp

@@ -739,12 +739,24 @@ void Btor2Frontend::get_node(NODE_INFO& info, InstL& args) {
 	case BTOR2_TAG_rol: {
 		assert(args.size() == 2);
 		assert(args.front()->get_size() == args.back()->get_size());
-		opt = OpInst::RotateL;
+		Inst* arg2 = args.back();
+		if (NumInst::as(arg2)) {
+			opt = OpInst::RotateL;
+		} else {
+			opt = OpInst::VRotateL;
+			btor2_loge("unsupported (rotate by non-constant amount): " << t.name << " arg2: " << *arg2);
+		}
 	} break;
 	case BTOR2_TAG_ror: {
 		assert(args.size() == 2);
 		assert(args.front()->get_size() == args.back()->get_size());
-		opt = OpInst::RotateR;
+		Inst* arg2 = args.back();
+		if (NumInst::as(arg2)) {
+			opt = OpInst::RotateR;
+		} else {
+			opt = OpInst::VRotateR;
+			btor2_loge("unsupported (rotate by non-constant amount): " << t.name << " arg2: " << *arg2);
+		}
 	} break;
 	case BTOR2_TAG_saddo: {
 		assert(sort.sz == 1);

xtras/issue10_case2.btor2

@@ -0,0 +1,39 @@
+1 sort bitvec 7
+2 sort bitvec 4
+3 const 2 1010
+4 constd 2 -8
+5 inc 2 4
+6 ror 2 3 5
+7 uext 1 6 3
+8 state 1 bv2_7
+9 neg 1 8
+10 sort bitvec 6
+11 zero 10
+12 sext 1 11 1
+13 state 1 bv0_7
+14 sll 1 12 13
+15 init 1 13 9
+16 state 1 bv1_7
+17 dec 1 16
+18 consth 1 01
+19 smod 1 13 18
+20 srl 1 17 19
+21 neg 1 20
+22 next 1 13 21
+23 init 1 16 14
+24 and 1 8 13
+25 next 1 16 24
+26 init 1 8 7
+27 sort bitvec 8
+28 input 2 input1_4
+29 sext 27 28 4
+30 slice 1 29 6 0
+31 next 1 8 30
+32 sort bitvec 1
+33 const 32 1
+34 neg 32 33
+35 sra 1 13 13
+36 add 1 13 13
+37 ult 32 35 36
+38 neq 32 34 37
+39 bad 38