mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-03 01:40:22 +00:00
Code Activity

annotate enode hash as signed character to address issue #210

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2015-09-29 14:14:29 -07:00
parent 074ff58739
commit 77c423b9aa
4 changed files with 10 additions and 10 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/parsers/smt2/smt2scanner.cpp
View file

@ -92,7 +92,7 @@ namespace smt2 {
scanner::token scanner::read_symbol_core() { scanner::token scanner::read_symbol_core() {
while (true) { while (true) {
char c = curr(); char c = curr();
char n = m_normalized[static_cast<unsigned char>(c)]; signed char n = m_normalized[static_cast<unsigned char>(c)];
if (n == 'a' || n == '0' || n == '-') { if (n == 'a' || n == '0' || n == '-') {
m_string.push_back(c); m_string.push_back(c);
next(); next();
@ -257,7 +257,7 @@ namespace smt2 {
m_smtlib2_compliant = ctx.params().m_smtlib2_compliant; m_smtlib2_compliant = ctx.params().m_smtlib2_compliant;
for (int i = 0; i < 256; ++i) { for (int i = 0; i < 256; ++i) {
m_normalized[i] = (char) i; m_normalized[i] = (signed char) i;
} }
m_normalized[static_cast<int>('\t')] = ' '; m_normalized[static_cast<int>('\t')] = ' ';
m_normalized[static_cast<int>('\r')] = ' '; m_normalized[static_cast<int>('\r')] = ' ';

2
src/parsers/smt2/smt2scanner.h
View file

@ -42,7 +42,7 @@ namespace smt2 {
rational m_number; rational m_number;
unsigned m_bv_size; unsigned m_bv_size;
// end of data // end of data
char m_normalized[256]; signed char m_normalized[256];
#define SCANNER_BUFFER_SIZE 1024 #define SCANNER_BUFFER_SIZE 1024
char m_buffer[SCANNER_BUFFER_SIZE]; char m_buffer[SCANNER_BUFFER_SIZE];
unsigned m_bpos; unsigned m_bpos;

2
src/smt/smt_enode.cpp
View file

@ -216,7 +216,7 @@ namespace smt {
// m_lbl_hash should be different from -1, if and only if, // m_lbl_hash should be different from -1, if and only if,
// there is a pattern that contains the enode. So, // there is a pattern that contains the enode. So,
// I use a trail to restore the value of m_lbl_hash to -1. // I use a trail to restore the value of m_lbl_hash to -1.
ctx.push_trail(value_trail<context, char>(m_lbl_hash)); ctx.push_trail(value_trail<context, signed char>(m_lbl_hash));
unsigned h = hash_u(get_owner_id()); unsigned h = hash_u(get_owner_id());
m_lbl_hash = h & (APPROX_SET_CAPACITY - 1); m_lbl_hash = h & (APPROX_SET_CAPACITY - 1);
// propagate modification to the root m_lbls set. // propagate modification to the root m_lbls set.

12
src/smt/smt_enode.h
View file

@ -52,11 +52,11 @@ namespace smt {
#else #else
class app2enode_t : public u_map<enode *> { class app2enode_t : public u_map<enode *> {
public: public:
void setx(unsigned x, enode *val, enode *def){ void setx(unsigned x, enode *val, enode *def){
if(val == 0) if (val == 0)
erase(x); erase(x);
else else
insert(x,val); insert(x,val);
} }
}; };
#endif #endif
@ -105,7 +105,7 @@ namespace smt {
enode_vector m_parents; //!< Parent enodes of the equivalence class. enode_vector m_parents; //!< Parent enodes of the equivalence class.
theory_var_list m_th_var_list; //!< List of theories that 'care' about this enode. theory_var_list m_th_var_list; //!< List of theories that 'care' about this enode.
trans_justification m_trans; //!< A justification for the enode being equal to its root. trans_justification m_trans; //!< A justification for the enode being equal to its root.
char m_lbl_hash; //!< It is different from -1, if enode is used in a pattern signed char m_lbl_hash; //!< It is different from -1, if enode is used in a pattern
approx_set m_lbls; approx_set m_lbls;
approx_set m_plbls; approx_set m_plbls;
enode * m_args[0]; //!< Cached args enode * m_args[0]; //!< Cached args