How can i remove multiple declaration of same variable when translating from IR->Z3.

[siddharth0998]

Dslx file :

fn muladd(a: u8, b: u8, c: u8) -> u8 { 
  assert!(a != u8:42, "lucky number");
  (a * b) + c 
}

#[test]
fn muladd_test() {
  assert!(muladd(u8:1, u8:1, u8: 1)==u8:2,"Hello");
}

IR file:

top fn __simple_assert__muladd(a: bits[8] id=17, b: bits[8] id=18, c: bits[8] id=19) -> bits[8] {
  literal.29: bits[8] = literal(value=42, id=29, pos=[(0,1,15)])
  after_all.20: token = after_all(id=20)
  ne.30: bits[1] = ne(a, literal.29, id=30, pos=[(0,1,10)])
  umul.33: bits[8] = umul(a, b, id=33, pos=[(0,2,3)])
  assert_34: token = assert(after_all.20, ne.30, message="Assertion failure via assert! @ /media/sourav/SSD/xls_program/simple_assert.x:2:10-2:38", label="lucky number", id=37)
  ret add.35: bits[8] = add(umul.33, c, id=35, pos=[(0,2,3)])
}

Output :

(declare-fun a () (_ BitVec 8))
(declare-fun a () (_ BitVec 8))
(assert (not (= a #x2a)))

(declare-fun b () (_ BitVec 8))
(declare-fun c () (_ BitVec 8))
(bvadd ((_ extract 7 0) (bvmul ((_ zero_extend 1) a) ((_ zero_extend 1) b))) c)

HandleAssert Code :

absl::Status IrTranslator::HandleAssert(Assert* assert) {

  Z3_solver solver = Z3_mk_solver(ctx_);
  Z3_solver_inc_ref(ctx_, solver);
  
  Z3_ast a = GetBitVec(assert->condition()->operand(0));
  Z3_ast b = GetBitVec(assert->condition()->operand(1));

  Z3_ast eq = Z3_mk_eq(ctx_, a, b);
  Z3_ast neq = Z3_mk_not(ctx_, eq);

  Z3_solver_assert(ctx_, solver, neq);
  std::cout << Z3_solver_to_string(ctx_, solver) << std::endl;

  Z3_solver_dec_ref(ctx_, solver);

  return absl::OkStatus();
  }

here in output below line is printing twice this should not be the case

  (declare-fun a () (_ BitVec 8))
  (declare-fun a () (_ BitVec 8)).

[proppy]

Assuming this is related to #1549 and you're attempting to add support to new nodes to the IR -> Z3 translation logic.

If you look at other functions in https://github.com/google/xls/blob/main/xls/solvers/z3_ir_translator.cc, you'll notice that none of them is printing anything to stdout.

Instead https://github.com/google/xls/blob/main/xls/solvers/smtlib_emitter_main.cc#L61 is doing the printing after converting the IR graph to a Z3 AST, w/ Z3_ast_to_string.

So adding support for new nodes should be done by augmenting the Z3 AST w/ the appropriate Z3 objects in the corresponding Handle* functions instead of directly printing to stdout.

Hope that helps.

[siddharth0998]

So adding support for new nodes should be done by augmenting the Z3 AST w/ the appropriate Z3 objects in the corresponding Handle* functions instead of directly printing to stdout.

i tried to implement like this but it is still not working can you elaborate more on this how can i do this? i am not understanding it.