From 3f84d0606307ee4257db588d79e0137956e71e7f Mon Sep 17 00:00:00 2001 From: Haniel Barbosa Date: Thu, 22 Feb 2024 23:02:16 -0300 Subject: [PATCH] using the cvc5 names --- carcara/src/ast/mod.rs | 4 ++-- carcara/src/checker/mod.rs | 34 +++++++++++++++++----------------- 2 files changed, 19 insertions(+), 19 deletions(-) diff --git a/carcara/src/ast/mod.rs b/carcara/src/ast/mod.rs index 1bd2b215..97639319 100644 --- a/carcara/src/ast/mod.rs +++ b/carcara/src/ast/mod.rs @@ -432,7 +432,7 @@ pub enum IndexedOperator { impl_str_conversion_traits!(IndexedOperator { BvExtract: "extract", - BvBitOf: "bit_of", + BvBitOf: "bitOf", ZeroExtend: "zero_extend", SignExtend: "sign_extend", RotateLeft: "rotate_left", @@ -537,7 +537,7 @@ impl_str_conversion_traits!(Operator { BvSLe: "bvsle", BvSGt: "bvsgt", BvSGe: "bvsge", - BvBbTerm: "bbterm", + BvBbTerm: "bbT", RareList: "rare-list", }); diff --git a/carcara/src/checker/mod.rs b/carcara/src/checker/mod.rs index 8dcb22c9..0db1dbdf 100644 --- a/carcara/src/checker/mod.rs +++ b/carcara/src/checker/mod.rs @@ -555,23 +555,23 @@ impl<'c> ProofChecker<'c> { "la_mult_pos" => extras::la_mult_pos, "la_mult_neg" => extras::la_mult_neg, "mod_simplify" => extras::mod_simplify, - "bitblast_const" => bitvectors::value, - "bitblast_var" => bitvectors::var, - "bitblast_bvand" => bitvectors::and, - "bitblast_bvor" => bitvectors::or, - "bitblast_bvxor" => bitvectors::xor, - "bitblast_bvxnor" => bitvectors::xnor, - "bitblast_bvnot" => bitvectors::not, - "bitblast_bvcomp" => bitvectors::comp, - "bitblast_bvult" => bitvectors::ult, - "bitblast_bvslt" => bitvectors::slt, - "bitblast_bvadd" => bitvectors::add, - "bitblast_bvmult" => bitvectors::mult, - "bitblast_bvneg" => bitvectors::neg, - "bitblast_equal" => bitvectors::equality, - "bitblast_extract" => bitvectors::extract, - "bitblast_concat" => bitvectors::concat, - "bitblast_sign_extend" => bitvectors::sign_extend, + "bv_bitblast_step_const" => bitvectors::value, + "bv_bitblast_step_var" => bitvectors::var, + "bv_bitblast_step_bvand" => bitvectors::and, + "bv_bitblast_step_bvor" => bitvectors::or, + "bv_bitblast_step_bvxor" => bitvectors::xor, + "bv_bitblast_step_bvxnor" => bitvectors::xnor, + "bv_bitblast_step_bvnot" => bitvectors::not, + "bv_bitblast_step_bvcomp" => bitvectors::comp, + "bv_bitblast_step_bvult" => bitvectors::ult, + "bv_bitblast_step_bvslt" => bitvectors::slt, + "bv_bitblast_step_bvadd" => bitvectors::add, + "bv_bitblast_step_bvmult" => bitvectors::mult, + "bv_bitblast_step_bvneg" => bitvectors::neg, + "bv_bitblast_step_bvequal" => bitvectors::equality, + "bv_bitblast_step_extract" => bitvectors::extract, + "bv_bitblast_step_concat" => bitvectors::concat, + "bv_bitblast_step_sign_extend" => bitvectors::sign_extend, "concat_eq" => strings::concat_eq, "concat_unify" => strings::concat_unify,