9225189528

Committed 24 May 2024 02:01PM UTC coverage: 64.72% (-1.0%) from 65.728%

Build # 9225189528

Build Type

Pull #513

github

Committed by

web-flow

Commit Message

Merge bf39b5d9f into f06761440

Pull Request Pull Request #513: Finite Field support

Run Details

818 of 3223 new or added lines in 59 files covered. (25.38%)

14 existing lines in 10 files now uncovered.

80132 of 123813 relevant lines covered (64.72%)

1494021.56 hits per line

Source File
Press 'n' to go to next uncovered line, 'b' for previous

0.0

/src/mcsat/utils/value_version_set.c

/*
 * This file is part of the Yices SMT Solver.
 * Copyright (C) 2017 SRI International.
 *
 * Yices is free software: you can redistribute it and/or modify
 * it under the terms of the GNU General Public License as published by
 * the Free Software Foundation, either version 3 of the License, or
 * (at your option) any later version.
 *
 * Yices is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with Yices.  If not, see <http://www.gnu.org/licenses/>.
 */

#include <stdbool.h>

#include "mcsat/value.h"
#include "mcsat/utils/value_version_set.h"
#include "mcsat/utils/value_hash_map.h"


struct value_version_set_struct {
  value_version_set_type_t type;
  /** current level (0 means all elements, and set is ignored) */
  uint32_t timestamp;
  /** Values stored in the map [value -> ts]. Every map[value] <= timestamp.
   * Union Sets: When the element was added.
   * Intersection Sets: When map[value] = timestamp then element is in the set, otherwise value was in the set previously */
  value_hmap_t map;
  /** Count to perform efficient is_empty checks for intersections */
  uint32_t count;
};

value_version_set_t* value_version_set_new(value_version_set_type_t type) {
  value_version_set_t *set = safe_malloc(sizeof(value_version_set_t));
  set->type = type;
  set->timestamp = 0;
  set->count = 0;
  init_value_hmap(&set->map, 0);
  return set;
}

void value_version_set_delete(value_version_set_t *set) {
  delete_value_hmap(&set->map);
  safe_free(set);
}

uint32_t value_version_set_count(const value_version_set_t *set) {
  if (set->type == VALUE_SET_INTERSECTION && set->timestamp == 0) {
    // set containing "all"
    assert(set->count == 0);
    return UINT32_MAX;
  }
  assert(set->type != VALUE_SET_UNION || set->map.nelems == set->count);
  return set->count;
}

void value_version_set_reset(value_version_set_t *set) {
  set->timestamp = 0;
  set->count = 0;
  value_hmap_reset(&set->map);
}

static
bool value_version_set_push_union(value_version_set_t *set, mcsat_value_t *new_set, size_t new_set_size, void *aux, value_version_set_filter_t f) {
  bool update = false;
  set->timestamp++;
  for (size_t i = 0; i < new_set_size; ++i) {
    mcsat_value_t *new = &new_set[i];
    if (f != NULL && !f(aux, new)) {
      continue;
    }
    value_hmap_pair_t *pair = value_hmap_get(&set->map, new);
    if (pair->val == -1) {
      set->count++;
      update = true;
      pair->val = set->timestamp;
    }
  }
  return update;
}

static
bool value_version_set_push_intersect(value_version_set_t *set, mcsat_value_t *new_set, size_t new_set_size, void *aux, value_version_set_filter_t f) {
  size_t remaining = 0;
  for (size_t i = 0; i < new_set_size; ++i) {
    mcsat_value_t *new = &new_set[i];
    if (f != NULL && !f(aux, new)) {
      continue;
    }
    value_hmap_pair_t *pair = value_hmap_find(&set->map, new);
    if (pair != NULL && pair->val == set->timestamp) {
      pair->val++;
      remaining++;
    }
  }

  set->timestamp++;
  bool update = (remaining != set->count);
  set->count = remaining;
  return update;
}

bool value_version_set_push(value_version_set_t *set, mcsat_value_t *new_set, size_t new_set_size) {
  return value_version_set_push_filter(set, new_set, new_set_size, NULL, NULL);
}

bool value_version_set_push_filter(value_version_set_t *set, mcsat_value_t *new_set, size_t new_set_size, void *aux, value_version_set_filter_t f) {
  if (set->type == VALUE_SET_UNION || (set->type == VALUE_SET_INTERSECTION && set->timestamp == 0)) {
    return value_version_set_push_union(set, new_set, new_set_size, aux, f);
  } else if (set->type == VALUE_SET_INTERSECTION) {
    return value_version_set_push_intersect(set, new_set, new_set_size, aux, f);
  } else {
    assert(false);
    return false;
  }
}

static
uint32_t feasibility_int_set_push_current(void *set, const value_hmap_pair_t *p) {
  uint32_t ts = ((value_version_set_t *) set)->timestamp;
  return p->val == ts ? p->val + 1 : p->val;
}

/** specific push function that requires an not-empty intersection set. Updates all that are not in new_set */
bool value_version_set_push_intersect_inverted(value_version_set_t *set, mcsat_value_t *new_set, size_t new_set_size) {
  assert(set->type == VALUE_SET_INTERSECTION);
  assert(set->timestamp > 0);

  // update all current by one
  value_hmap_update_records(&set->map, set, feasibility_int_set_push_current);
  set->timestamp++;

  // decrement the timestamp of all current that are in new_set to exclude them
  bool update = false;
  for (size_t i = 0; i < new_set_size; ++i) {
    value_hmap_pair_t *pair = value_hmap_find(&set->map, &new_set[i]);
    if (pair != NULL && pair->val == set->timestamp) {
      pair->val--;
      set->count--;
      update = true;
    }
  }

  return update;
}

static
bool feasibility_int_set_pop_is_future_ts(void *aux, const value_hmap_pair_t *p) {
  value_version_set_t *set = (value_version_set_t *) aux;
  uint32_t ts = set->timestamp;
  if (p->val > ts) {
    set->count--;
    return true;
  } else {
    return false;
  }
}

static
uint32_t feasibility_int_set_pop_map_min(void *aux, const value_hmap_pair_t *p) {
  value_version_set_t *set = (value_version_set_t *) aux;
  uint32_t ts = set->timestamp;
  uint32_t ret = p->val > ts ? ts : p->val;
  if (ret >= ts) {
    set->count++;
  }
  return ret;
}

void value_version_set_pop(value_version_set_t *set, size_t count) {
  if (count >= set->timestamp) {
    value_version_set_reset(set);
  } else {
    set->timestamp -= count;
    switch(set->type) {
    case VALUE_SET_UNION:
      value_hmap_remove_records(&set->map, set, feasibility_int_set_pop_is_future_ts);
      break;
    case VALUE_SET_INTERSECTION:
      set->count = 0;
      value_hmap_update_records(&set->map, set, feasibility_int_set_pop_map_min);
      break;
    default:
      assert(false);
    }
  }
}

bool value_version_set_contains(const value_version_set_t *set, const mcsat_value_t *k) {
  value_hmap_pair_t *pair = value_hmap_find(&set->map, k);
  if (pair == NULL) {
    return false;
  } else if (set->type == VALUE_SET_UNION) {
    return true;
  } else {
    return pair->val == set->timestamp;
  }
}

const mcsat_value_t* value_version_set_any(const value_version_set_t *set) {
  value_hmap_pair_t *it;

  if (set->count == 0) {
    return NULL;
  }

  switch(set->type) {
  case VALUE_SET_UNION:
    it = value_hmap_first_record(&set->map);
    return it == NULL ? NULL : it->key;
  case VALUE_SET_INTERSECTION:
    for (it = value_hmap_first_record(&set->map); it != NULL; it = value_hmap_next_record(&set->map, it)) {
      if (it->val == set->timestamp) {
        return it->key;
      }
    }
    assert(false);
    return NULL;
  default:
    assert(false);
    return NULL;
  }
}

uint32_t value_version_set_get_timestamp(const value_version_set_t *set) {
  return set->timestamp;
}

void value_version_set_print(const value_version_set_t *set, FILE *out) {
  value_version_set_print_at(set, set->timestamp, out);
}

void value_version_set_print_at(const value_version_set_t *set, uint32_t timestamp, FILE *out) {
  fprintf(out, "{");
  bool first = true;
  for (value_hmap_pair_t *it = value_hmap_first_record(&set->map); it != NULL; it = value_hmap_next_record(&set->map, it)) {
    if (set->type == VALUE_SET_UNION && it->val > timestamp) {
      continue;
    }
    if (set->type == VALUE_SET_INTERSECTION && it->val < timestamp) {
      continue;
    }
    if (!first) {
      fprintf(out, ", ");
    }
    first = false;
    mcsat_value_print(it->key, out);
  }
  fprintf(out, "}");
}

1	/*
2	* This file is part of the Yices SMT Solver.
3	* Copyright (C) 2017 SRI International.
4	*
5	* Yices is free software: you can redistribute it and/or modify
6	* it under the terms of the GNU General Public License as published by
7	* the Free Software Foundation, either version 3 of the License, or
8	* (at your option) any later version.
9	*
10	* Yices is distributed in the hope that it will be useful,
11	* but WITHOUT ANY WARRANTY; without even the implied warranty of
12	* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
13	* GNU General Public License for more details.
14	*
15	* You should have received a copy of the GNU General Public License
16	* along with Yices. If not, see <http://www.gnu.org/licenses/>.
17	*/
18
19	#include <stdbool.h>
20
21	#include "mcsat/value.h"
22	#include "mcsat/utils/value_version_set.h"
23	#include "mcsat/utils/value_hash_map.h"
24
25
26	struct value_version_set_struct {
27	value_version_set_type_t type;
28	/** current level (0 means all elements, and set is ignored) */
29	uint32_t timestamp;
30	/** Values stored in the map [value -> ts]. Every map[value] <= timestamp.
31	* Union Sets: When the element was added.
32	* Intersection Sets: When map[value] = timestamp then element is in the set, otherwise value was in the set previously */
33	value_hmap_t map;
34	/** Count to perform efficient is_empty checks for intersections */
35	uint32_t count;
36	};
37
NEW 38	value_version_set_t* value_version_set_new(value_version_set_type_t type) {	×
NEW 39	value_version_set_t *set = safe_malloc(sizeof(value_version_set_t));	×
NEW 40	set->type = type;	×
NEW 41	set->timestamp = 0;	×
NEW 42	set->count = 0;	×
NEW 43	init_value_hmap(&set->map, 0);	×
NEW 44	return set;	×
45	}
46
NEW 47	void value_version_set_delete(value_version_set_t *set) {	×
NEW 48	delete_value_hmap(&set->map);	×
NEW 49	safe_free(set);	×
NEW 50	}	×
51
NEW 52	uint32_t value_version_set_count(const value_version_set_t *set) {	×
NEW 53	if (set->type == VALUE_SET_INTERSECTION && set->timestamp == 0) {	×
54	// set containing "all"
55	assert(set->count == 0);
NEW 56	return UINT32_MAX;	×
57	}
58	assert(set->type != VALUE_SET_UNION \|\| set->map.nelems == set->count);
NEW 59	return set->count;	×
60	}
61
NEW 62	void value_version_set_reset(value_version_set_t *set) {	×
NEW 63	set->timestamp = 0;	×
NEW 64	set->count = 0;	×
NEW 65	value_hmap_reset(&set->map);	×
NEW 66	}	×
67
68	static
NEW 69	bool value_version_set_push_union(value_version_set_t set, mcsat_value_t new_set, size_t new_set_size, void *aux, value_version_set_filter_t f) {	×
NEW 70	bool update = false;	×
NEW 71	set->timestamp++;	×
NEW 72	for (size_t i = 0; i < new_set_size; ++i) {	×
NEW 73	mcsat_value_t *new = &new_set[i];	×
NEW 74	if (f != NULL && !f(aux, new)) {	×
NEW 75	continue;	×
76	}
NEW 77	value_hmap_pair_t *pair = value_hmap_get(&set->map, new);	×
NEW 78	if (pair->val == -1) {	×
NEW 79	set->count++;	×
NEW 80	update = true;	×
NEW 81	pair->val = set->timestamp;	×
82	}
83	}
NEW 84	return update;	×
85	}
86
87	static
NEW 88	bool value_version_set_push_intersect(value_version_set_t set, mcsat_value_t new_set, size_t new_set_size, void *aux, value_version_set_filter_t f) {	×
NEW 89	size_t remaining = 0;	×
NEW 90	for (size_t i = 0; i < new_set_size; ++i) {	×
NEW 91	mcsat_value_t *new = &new_set[i];	×
NEW 92	if (f != NULL && !f(aux, new)) {	×
NEW 93	continue;	×
94	}
NEW 95	value_hmap_pair_t *pair = value_hmap_find(&set->map, new);	×
NEW 96	if (pair != NULL && pair->val == set->timestamp) {	×
NEW 97	pair->val++;	×
NEW 98	remaining++;	×
99	}
100	}
101
NEW 102	set->timestamp++;	×
NEW 103	bool update = (remaining != set->count);	×
NEW 104	set->count = remaining;	×
NEW 105	return update;	×
106	}
107
NEW 108	bool value_version_set_push(value_version_set_t set, mcsat_value_t new_set, size_t new_set_size) {	×
NEW 109	return value_version_set_push_filter(set, new_set, new_set_size, NULL, NULL);	×
110	}
111
NEW 112	bool value_version_set_push_filter(value_version_set_t set, mcsat_value_t new_set, size_t new_set_size, void *aux, value_version_set_filter_t f) {	×
NEW 113	if (set->type == VALUE_SET_UNION \|\| (set->type == VALUE_SET_INTERSECTION && set->timestamp == 0)) {	×
NEW 114	return value_version_set_push_union(set, new_set, new_set_size, aux, f);	×
NEW 115	} else if (set->type == VALUE_SET_INTERSECTION) {	×
NEW 116	return value_version_set_push_intersect(set, new_set, new_set_size, aux, f);	×
117	} else {
118	assert(false);
NEW 119	return false;	×
120	}
121	}
122
123	static
NEW 124	uint32_t feasibility_int_set_push_current(void set, const value_hmap_pair_t p) {	×
NEW 125	uint32_t ts = ((value_version_set_t *) set)->timestamp;	×
NEW 126	return p->val == ts ? p->val + 1 : p->val;	×
127	}
128
129	/** specific push function that requires an not-empty intersection set. Updates all that are not in new_set */
NEW 130	bool value_version_set_push_intersect_inverted(value_version_set_t set, mcsat_value_t new_set, size_t new_set_size) {	×
131	assert(set->type == VALUE_SET_INTERSECTION);
132	assert(set->timestamp > 0);
133
134	// update all current by one
NEW 135	value_hmap_update_records(&set->map, set, feasibility_int_set_push_current);	×
NEW 136	set->timestamp++;	×
137
138	// decrement the timestamp of all current that are in new_set to exclude them
NEW 139	bool update = false;	×
NEW 140	for (size_t i = 0; i < new_set_size; ++i) {	×
NEW 141	value_hmap_pair_t *pair = value_hmap_find(&set->map, &new_set[i]);	×
NEW 142	if (pair != NULL && pair->val == set->timestamp) {	×
NEW 143	pair->val--;	×
NEW 144	set->count--;	×
NEW 145	update = true;	×
146	}
147	}
148
NEW 149	return update;	×
150	}
151
152	static
NEW 153	bool feasibility_int_set_pop_is_future_ts(void aux, const value_hmap_pair_t p) {	×
NEW 154	value_version_set_t set = (value_version_set_t ) aux;	×
NEW 155	uint32_t ts = set->timestamp;	×
NEW 156	if (p->val > ts) {	×
NEW 157	set->count--;	×
NEW 158	return true;	×
159	} else {
NEW 160	return false;	×
161	}
162	}
163
164	static
NEW 165	uint32_t feasibility_int_set_pop_map_min(void aux, const value_hmap_pair_t p) {	×
NEW 166	value_version_set_t set = (value_version_set_t ) aux;	×
NEW 167	uint32_t ts = set->timestamp;	×
NEW 168	uint32_t ret = p->val > ts ? ts : p->val;	×
NEW 169	if (ret >= ts) {	×
NEW 170	set->count++;	×
171	}
NEW 172	return ret;	×
173	}
174
NEW 175	void value_version_set_pop(value_version_set_t *set, size_t count) {	×
NEW 176	if (count >= set->timestamp) {	×
NEW 177	value_version_set_reset(set);	×
178	} else {
NEW 179	set->timestamp -= count;	×
NEW 180	switch(set->type) {	×
NEW 181	case VALUE_SET_UNION:	×
NEW 182	value_hmap_remove_records(&set->map, set, feasibility_int_set_pop_is_future_ts);	×
NEW 183	break;	×
NEW 184	case VALUE_SET_INTERSECTION:	×
NEW 185	set->count = 0;	×
NEW 186	value_hmap_update_records(&set->map, set, feasibility_int_set_pop_map_min);	×
NEW 187	break;	×
NEW 188	default:	×
189	assert(false);
190	}
191	}
NEW 192	}	×
193
NEW 194	bool value_version_set_contains(const value_version_set_t set, const mcsat_value_t k) {	×
NEW 195	value_hmap_pair_t *pair = value_hmap_find(&set->map, k);	×
NEW 196	if (pair == NULL) {	×
NEW 197	return false;	×
NEW 198	} else if (set->type == VALUE_SET_UNION) {	×
NEW 199	return true;	×
200	} else {
NEW 201	return pair->val == set->timestamp;	×
202	}
203	}
204
NEW 205	const mcsat_value_t* value_version_set_any(const value_version_set_t *set) {	×
206	value_hmap_pair_t *it;
207
NEW 208	if (set->count == 0) {	×
NEW 209	return NULL;	×
210	}
211
NEW 212	switch(set->type) {	×
NEW 213	case VALUE_SET_UNION:	×
NEW 214	it = value_hmap_first_record(&set->map);	×
NEW 215	return it == NULL ? NULL : it->key;	×
NEW 216	case VALUE_SET_INTERSECTION:	×
NEW 217	for (it = value_hmap_first_record(&set->map); it != NULL; it = value_hmap_next_record(&set->map, it)) {	×
NEW 218	if (it->val == set->timestamp) {	×
NEW 219	return it->key;	×
220	}
221	}
222	assert(false);
NEW 223	return NULL;	×
NEW 224	default:	×
225	assert(false);
NEW 226	return NULL;	×
227	}
228	}
229
NEW 230	uint32_t value_version_set_get_timestamp(const value_version_set_t *set) {	×
NEW 231	return set->timestamp;	×
232	}
233
NEW 234	void value_version_set_print(const value_version_set_t set, FILE out) {	×
NEW 235	value_version_set_print_at(set, set->timestamp, out);	×
NEW 236	}	×
237
NEW 238	void value_version_set_print_at(const value_version_set_t set, uint32_t timestamp, FILE out) {	×
NEW 239	fprintf(out, "{");	×
NEW 240	bool first = true;	×
NEW 241	for (value_hmap_pair_t *it = value_hmap_first_record(&set->map); it != NULL; it = value_hmap_next_record(&set->map, it)) {	×
NEW 242	if (set->type == VALUE_SET_UNION && it->val > timestamp) {	×
NEW 243	continue;	×
244	}
NEW 245	if (set->type == VALUE_SET_INTERSECTION && it->val < timestamp) {	×
NEW 246	continue;	×
247	}
NEW 248	if (!first) {	×
NEW 249	fprintf(out, ", ");	×
250	}
NEW 251	first = false;	×
NEW 252	mcsat_value_print(it->key, out);	×
253	}
NEW 254	fprintf(out, "}");	×
NEW 255	}	×

SRI-CSL / yices2 / 9225189528

Source File Press 'n' to go to next uncovered line, 'b' for previous

Source File
Press 'n' to go to next uncovered line, 'b' for previous