8762094294

Committed 20 Apr 2024 02:54AM UTC coverage: 65.727% (+0.2%) from 65.524%

Build # 8762094294

Build Type

push

github

Committed by

ahmed-irfan

Commit Message

learning interval

Run Details

8 of 8 new or added lines in 1 file covered. (100.0%)

958 existing lines in 6 files now uncovered.

79985 of 121693 relevant lines covered (65.73%)

1517744.44 hits per line

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

70.75

/src/mcsat/value.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 "mcsat/value.h"

#include <assert.h>

#include "utils/memalloc.h"
#include "utils/hash_functions.h"

#include "api/yices_api_lock_free.h"

const mcsat_value_t mcsat_value_none = { VALUE_NONE, { true } };
const mcsat_value_t mcsat_value_true = { VALUE_BOOLEAN, { true } };
const mcsat_value_t mcsat_value_false = { VALUE_BOOLEAN, { false } };

void mcsat_value_construct_default(mcsat_value_t* value) {
  value->type = VALUE_NONE;
}

void mcsat_value_construct_bool(mcsat_value_t* value, bool b) {
  value->type = VALUE_BOOLEAN;
  value->b = b;
}

void mcsat_value_construct_rational(mcsat_value_t* value, const rational_t* q) {
  value->type = VALUE_RATIONAL;
  q_init(&value->q);
  q_set(&value->q, q);
}

void mcsat_value_construct_lp_value(mcsat_value_t* value, const lp_value_t* lp_value) {
  value->type = VALUE_LIBPOLY;
  lp_value_construct_copy(&value->lp_value, lp_value);
}

void mcsat_value_construct_lp_value_direct(mcsat_value_t *value, lp_value_type_t type, void* data) {
  value->type = VALUE_LIBPOLY;
  lp_value_construct(&value->lp_value, type, data);
}

void mcsat_value_construct_bv_value(mcsat_value_t* value, const bvconstant_t* bvvalue) {
  value->type = VALUE_BV;
  init_bvconstant(&value->bv_value);
  if (bvvalue != NULL) {
    bvconstant_copy(&value->bv_value, bvvalue->bitsize, bvvalue->data);
  }
}

void mcsat_value_construct_copy(mcsat_value_t* value, const mcsat_value_t* from) {
  value->type = from->type;
  switch (value->type) {
  case VALUE_NONE:
    break;
  case VALUE_BOOLEAN:
    value->b = from->b;
    break;
  case VALUE_RATIONAL:
    q_init(&value->q);
    q_set(&value->q, &from->q);
    break;
  case VALUE_LIBPOLY:
    lp_value_construct_copy(&value->lp_value, &from->lp_value);
    break;
  case VALUE_BV:
    init_bvconstant(&value->bv_value);
    bvconstant_copy(&value->bv_value, from->bv_value.bitsize, from->bv_value.data);
    break;
  default:
    assert(false);
  }
}

void mcsat_value_construct_copy_n(mcsat_value_t *value, const mcsat_value_t *from, uint32_t n) {
  uint32_t i;
  for (i = 0; i < n; ++ i) {
    mcsat_value_construct_copy(value + i, from + i);
  }
}


/** Construct a MCSAT value from a constant term */
void mcsat_value_construct_from_constant_term(mcsat_value_t* t_value, term_table_t* terms, term_t t) {
  term_kind_t t_kind = term_kind(terms, t);
  switch (t_kind) {
  case BV_CONSTANT: {
    bvconst_term_t* t_desc = bvconst_term_desc(terms, t);
    bvconstant_t t_bvconst;
    init_bvconstant(&t_bvconst);
    bvconstant_set_bitsize(&t_bvconst, t_desc->bitsize);
    bvconstant_copy(&t_bvconst, t_desc->bitsize, t_desc->data);
    mcsat_value_construct_bv_value(t_value, &t_bvconst);
    delete_bvconstant(&t_bvconst);
    break;
  }
  case BV64_CONSTANT: {
    // Propagate constant value (it's first time we see it, so should be safe
    bvconst64_term_t* t_desc = bvconst64_term_desc(terms, t);
    bvconstant_t t_bvconst;
    init_bvconstant(&t_bvconst);
    bvconstant_set_bitsize(&t_bvconst, t_desc->bitsize);
    bvconstant_copy64(&t_bvconst, t_desc->bitsize, t_desc->value);
    mcsat_value_construct_bv_value(t_value, &t_bvconst);
    delete_bvconstant(&t_bvconst);
    break;
  }
  case CONSTANT_TERM: {
    // Boolean terms case
    if (t == true_term || t == false_term) {
      mcsat_value_construct_bool(t_value, t == true_term);
    } else {
      // scalar case
      int32_t int_value;
      _o_yices_scalar_const_value(t, &int_value);
      rational_t q;
      q_init(&q);
      q_set32(&q, int_value);
      mcsat_value_construct_rational(t_value, &q);
      q_clear(&q);
    }
    break;
  }
  case ARITH_CONSTANT: {
    lp_rational_t rat_value;
    lp_rational_construct(&rat_value);
    q_get_mpq(rational_term_desc(terms, t), &rat_value);
    lp_value_t lp_value;
    lp_value_construct(&lp_value, LP_VALUE_RATIONAL, &rat_value);
    mcsat_value_construct_lp_value(t_value, &lp_value);
    lp_value_destruct(&lp_value);
    lp_rational_destruct(&rat_value);
    break;
  }
  default:
    assert(false);
  }
}


mcsat_value_t* mcsat_value_new_default() {
  mcsat_value_t* result = (mcsat_value_t*) safe_malloc(sizeof(mcsat_value_t));
  mcsat_value_construct_default(result);
  return result;
}

mcsat_value_t* mcsat_value_new_bool(bool b) {
  mcsat_value_t* result = (mcsat_value_t*) safe_malloc(sizeof(mcsat_value_t));
  mcsat_value_construct_bool(result, b);
  return result;
}

mcsat_value_t* mcsat_value_new_rational(const rational_t *q) {
  mcsat_value_t* result = (mcsat_value_t*) safe_malloc(sizeof(mcsat_value_t));
  mcsat_value_construct_rational(result, q);
  return result;
}

mcsat_value_t* mcsat_value_new_lp_value(const lp_value_t *lp_value) {
  mcsat_value_t* result = (mcsat_value_t*) safe_malloc(sizeof(mcsat_value_t));
  mcsat_value_construct_lp_value(result, lp_value);
  return result;
}

mcsat_value_t* mcsat_value_new_bv_value(const bvconstant_t *bv_value) {
  mcsat_value_t* result = (mcsat_value_t*) safe_malloc(sizeof(mcsat_value_t));
  mcsat_value_construct_bv_value(result, bv_value);
  return result;
}

mcsat_value_t* mcsat_value_new_copy(const mcsat_value_t *from) {
  mcsat_value_t* result = (mcsat_value_t*) safe_malloc(sizeof(mcsat_value_t));
  mcsat_value_construct_copy(result, from);
  return result;
}

void mcsat_value_destruct(mcsat_value_t* value) {
  switch (value->type) {
  case VALUE_NONE:
    break;
  case VALUE_BOOLEAN:
    break;
  case VALUE_RATIONAL:
    q_clear(&value->q);
    break;
  case VALUE_LIBPOLY:
    lp_value_destruct(&value->lp_value);
    break;
  case VALUE_BV:
    delete_bvconstant(&value->bv_value);
    break;
  default:
    assert(false);
  }
}

void mcsat_value_delete(mcsat_value_t* value) {
  mcsat_value_destruct(value);
  safe_free(value);
}

void mcsat_value_assign(mcsat_value_t* value, const mcsat_value_t* from) {
  if (value != from) {
    mcsat_value_destruct(value);
    mcsat_value_construct_copy(value, from);
  }
}

void mcsat_value_print(const mcsat_value_t* value, FILE* out) {
  switch (value->type) {
  case VALUE_NONE:
    fprintf(out, "<NONE>");
    break;
  case VALUE_BOOLEAN:
    if (value->b) {
      fprintf(out, "true");
    } else {
      fprintf(out, "false");
    }
    break;
  case VALUE_RATIONAL:
    q_print(out, (rational_t*) &value->q);
    break;
  case VALUE_LIBPOLY:
    lp_value_print(&value->lp_value, out);
    break;
  case VALUE_BV:
    bvconst_print(out, value->bv_value.data, value->bv_value.bitsize);
    break;
  default:
    assert(false);
  }
}

bool mcsat_value_eq(const mcsat_value_t* v1, const mcsat_value_t* v2) {
  if (v1 == v2) {
    return true;
  }
  switch (v1->type) {
  case VALUE_BOOLEAN:
    assert(v2->type == VALUE_BOOLEAN);
    return v1->b == v2->b;
  case VALUE_RATIONAL:
    if (v2->type == VALUE_RATIONAL) {
      return q_cmp(&v1->q, &v2->q) == 0;
    } else {
      assert(v2->type == VALUE_LIBPOLY);
      mpq_t v1_mpq;
      mpq_init(v1_mpq);
      q_get_mpq((rational_t*)&v1->q, v1_mpq);
      lp_value_t v1_lp;
      lp_value_construct_none(&v1_lp);
      lp_value_assign_raw(&v1_lp, LP_VALUE_RATIONAL, &v1_mpq);
      int cmp = lp_value_cmp(&v1_lp, &v2->lp_value);
      lp_value_destruct(&v1_lp);
      mpq_clear(v1_mpq);
      return cmp == 0;
    }
  case VALUE_LIBPOLY:
    if (v2->type == VALUE_LIBPOLY) {
      return lp_value_cmp(&v1->lp_value, &v2->lp_value) == 0;
    } else {
      assert(v1->type == VALUE_RATIONAL);
      mpq_t v2_mpq;
      mpq_init(v2_mpq);
      q_get_mpq((rational_t*)&v2->q, v2_mpq);
      lp_value_t v2_lp;
      lp_value_construct_none(&v2_lp);
      lp_value_assign_raw(&v2_lp, LP_VALUE_RATIONAL, &v2_mpq);
      int cmp = lp_value_cmp(&v1->lp_value, &v2_lp);
      lp_value_destruct(&v2_lp);
      mpq_clear(v2_mpq);
      return cmp == 0;
    }
  case VALUE_BV: {
    assert(v2->type == VALUE_BV);
    assert(v1->bv_value.bitsize == v2->bv_value.bitsize);
    return bvconst_eq(v1->bv_value.data, v2->bv_value.data, v1->bv_value.width);
  }
  default:
    assert(false);
    return false;
  }
}

uint32_t mcsat_value_hash(const mcsat_value_t* v) {
  switch (v->type) {
  case VALUE_BOOLEAN:
    return v->b;
  case VALUE_RATIONAL:
  {
    mpq_t v_mpq;
    mpq_init(v_mpq);
    q_get_mpq((rational_t*)&v->q, v_mpq);
    lp_value_t v_lp;
    lp_value_construct_none(&v_lp);
    lp_value_assign_raw(&v_lp, LP_VALUE_RATIONAL, &v_mpq);
    uint32_t hash = lp_value_hash(&v_lp);
    lp_value_destruct(&v_lp);
    mpq_clear(v_mpq);
    return hash;
  }
  case VALUE_LIBPOLY:
    return lp_value_hash(&v->lp_value);
  case VALUE_BV: {
    bvconst_normalize(v->bv_value.data, v->bv_value.bitsize);
    return bvconst_hash(v->bv_value.data, v->bv_value.bitsize);
  }
  default:
    assert(false);
    return 0;
  }
}

term_t mcsat_value_to_term(const mcsat_value_t* mcsat_value, term_manager_t* tm) {

  term_t result = NULL_TERM;

  switch (mcsat_value->type) {
  case VALUE_BOOLEAN:
    if (mcsat_value->b) {
      result = true_term;
    } else {
      result = false_term;
    }
    break;
  case VALUE_BV: {
    const bvconstant_t* bv = &mcsat_value->bv_value;
    result = mk_bv_constant(tm, (bvconstant_t*) bv);
    break;
  }
  case VALUE_RATIONAL: {
    result = mk_arith_constant(tm, (rational_t*) &mcsat_value->q);
    break;
  }
  case VALUE_LIBPOLY:
    if (lp_value_is_rational(&mcsat_value->lp_value)) {
      lp_rational_t lp_q;
      lp_rational_construct(&lp_q);
      lp_value_get_rational(&mcsat_value->lp_value, &lp_q);
      rational_t q;
      q_init(&q);
      q_set_mpq(&q, &lp_q);
      result = mk_arith_constant(tm, &q);
      q_clear(&q);
      lp_rational_destruct(&lp_q);
    } else {
      assert(false);
      result = NULL_TERM;
    }
    break;
  default:
    assert(false);
  }

  return result;
}

value_t mcsat_value_to_value(const mcsat_value_t* mcsat_value, type_table_t *types, type_t type, value_table_t* vtbl) {
  value_t value = null_value;
  switch (mcsat_value->type) {
  case VALUE_BOOLEAN:
    value = vtbl_mk_bool(vtbl, mcsat_value->b);
    break;
  case VALUE_RATIONAL: {
    type_kind_t kind = type_kind(types, type);
    if (kind == UNINTERPRETED_TYPE || kind == SCALAR_TYPE) {
      int32_t id;
      bool ok = q_get32((rational_t *)&mcsat_value->q, &id);
      (void) ok; // unused in release build
      assert(ok);
      value = vtbl_mk_const(vtbl, type, id, NULL);
    } else {
      value = vtbl_mk_rational(vtbl, (rational_t *) &mcsat_value->q);
    }
    break;
  }
  case VALUE_LIBPOLY:
    if (lp_value_is_rational(&mcsat_value->lp_value)) {
      lp_rational_t lp_q;
      lp_rational_construct(&lp_q);
      lp_value_get_rational(&mcsat_value->lp_value, &lp_q);
      rational_t q;
      q_init(&q);
      q_set_mpq(&q, &lp_q);
      type_kind_t kind = type_kind(types, type);
      if (kind == UNINTERPRETED_TYPE || kind == SCALAR_TYPE) {
        int32_t id;
        bool ok = q_get32(&q, &id);
        (void) ok; // unused in release build
        assert(ok);
        value = vtbl_mk_const(vtbl, type, id, NULL);
      } else {
        value = vtbl_mk_rational(vtbl, &q);
      }
      q_clear(&q);
      lp_rational_destruct(&lp_q);
    } else {
      value = vtbl_mk_algebraic(vtbl, (void*) &mcsat_value->lp_value.value.a);
    }
    break;
  case VALUE_BV:
    value = vtbl_mk_bv_from_bv(vtbl, mcsat_value->bv_value.bitsize, mcsat_value->bv_value.data);
    break;
  default:
    assert(false);
  }
  return value;
}

void mcsat_value_construct_from_value(mcsat_value_t* mcsat_value, value_table_t* vtbl, value_t v) {
  value_kind_t v_kind = object_kind(vtbl, v);
  switch (v_kind) {
  case BOOLEAN_VALUE:
    mcsat_value_construct_bool(mcsat_value, is_true(vtbl, v));
    break;
  case RATIONAL_VALUE: {
    rational_t* value_q = vtbl_rational(vtbl, v);
    mpq_t value_mpq;
    mpq_init(value_mpq);
    q_get_mpq(value_q, value_mpq);
    lp_value_t value_lp;
    lp_value_construct(&value_lp, LP_VALUE_RATIONAL, value_mpq);
    mcsat_value_construct_lp_value(mcsat_value, &value_lp);
    lp_value_destruct(&value_lp);
    mpq_clear(value_mpq);
    break;
  }
  case ALGEBRAIC_VALUE: {
    lp_algebraic_number_t* a = vtbl_algebraic_number(vtbl, v);
    lp_value_t value_lp;
    lp_value_construct(&value_lp, LP_VALUE_ALGEBRAIC, a);
    mcsat_value_construct_lp_value(mcsat_value, &value_lp);
    lp_value_destruct(&value_lp);
    break;
  }
  case BITVECTOR_VALUE: {
    value_bv_t* v1 = vtbl_bitvector(vtbl, v);
    bvconstant_t v2;
    init_bvconstant(&v2);
    bvconstant_copy(&v2, v1->nbits, v1->data);
    mcsat_value_construct_bv_value(mcsat_value, &v2);
    delete_bvconstant(&v2);
    break;
  }
  default:
    assert(false);
  }
}

bool mcsat_value_is_zero(const mcsat_value_t* value) {
  switch (value->type) {
  case VALUE_RATIONAL:
    return q_is_zero(&value->q);
  case VALUE_LIBPOLY: {
    lp_rational_t zero;
    lp_rational_construct(&zero);
    int cmp = lp_value_cmp_rational(&value->lp_value, &zero);
    lp_rational_destruct(&zero);
    return cmp == 0;
  }
  default:
    return false;
  }
}

bool mcsat_value_is_true(const mcsat_value_t* value) {
  return value->type == VALUE_BOOLEAN && value->b;
}

bool mcsat_value_is_false(const mcsat_value_t* value) {
  return value->type == VALUE_BOOLEAN && !value->b;
}

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 "mcsat/value.h"
20
21	#include <assert.h>
22
23	#include "utils/memalloc.h"
24	#include "utils/hash_functions.h"
25
26	#include "api/yices_api_lock_free.h"
27
28	const mcsat_value_t mcsat_value_none = { VALUE_NONE, { true } };
29	const mcsat_value_t mcsat_value_true = { VALUE_BOOLEAN, { true } };
30	const mcsat_value_t mcsat_value_false = { VALUE_BOOLEAN, { false } };
31
32	void mcsat_value_construct_default(mcsat_value_t* value) {	352,924✔
33	value->type = VALUE_NONE;	352,924✔
34	}	352,924✔
35
36	void mcsat_value_construct_bool(mcsat_value_t* value, bool b) {	36✔
37	value->type = VALUE_BOOLEAN;	36✔
38	value->b = b;	36✔
39	}	36✔
40
41	void mcsat_value_construct_rational(mcsat_value_t* value, const rational_t* q) {	148,114✔
42	value->type = VALUE_RATIONAL;	148,114✔
43	q_init(&value->q);	148,114✔
44	q_set(&value->q, q);	148,114✔
45	}	148,114✔
46
47	void mcsat_value_construct_lp_value(mcsat_value_t* value, const lp_value_t* lp_value) {	12,410✔
48	value->type = VALUE_LIBPOLY;	12,410✔
49	lp_value_construct_copy(&value->lp_value, lp_value);	12,410✔
50	}	12,410✔
51
52	void mcsat_value_construct_lp_value_direct(mcsat_value_t value, lp_value_type_t type, void data) {	×
53	value->type = VALUE_LIBPOLY;	×
UNCOV 54	lp_value_construct(&value->lp_value, type, data);	×
UNCOV 55	}	×
56
57	void mcsat_value_construct_bv_value(mcsat_value_t* value, const bvconstant_t* bvvalue) {	510,254✔
58	value->type = VALUE_BV;	510,254✔
59	init_bvconstant(&value->bv_value);	510,254✔
60	if (bvvalue != NULL) {	510,254✔
61	bvconstant_copy(&value->bv_value, bvvalue->bitsize, bvvalue->data);	509,610✔
62	}
63	}	510,254✔
64
65	void mcsat_value_construct_copy(mcsat_value_t* value, const mcsat_value_t* from) {	1,691,957✔
66	value->type = from->type;	1,691,957✔
67	switch (value->type) {	1,691,957✔
68	case VALUE_NONE:	91✔
69	break;	91✔
70	case VALUE_BOOLEAN:	1,243,857✔
71	value->b = from->b;	1,243,857✔
72	break;	1,243,857✔
73	case VALUE_RATIONAL:	301,403✔
74	q_init(&value->q);	301,403✔
75	q_set(&value->q, &from->q);	301,403✔
76	break;	301,403✔
77	case VALUE_LIBPOLY:	29,684✔
78	lp_value_construct_copy(&value->lp_value, &from->lp_value);	29,684✔
79	break;	29,684✔
80	case VALUE_BV:	116,922✔
81	init_bvconstant(&value->bv_value);	116,922✔
82	bvconstant_copy(&value->bv_value, from->bv_value.bitsize, from->bv_value.data);	116,922✔
83	break;	116,922✔
84	default:	1,691,957✔
85	assert(false);
86	}
87	}	1,691,957✔
88
89	void mcsat_value_construct_copy_n(mcsat_value_t value, const mcsat_value_t from, uint32_t n) {	34✔
90	uint32_t i;
91	for (i = 0; i < n; ++ i) {	1,939✔
92	mcsat_value_construct_copy(value + i, from + i);	1,905✔
93	}
94	}	34✔
95
96
97	/** Construct a MCSAT value from a constant term */
98	void mcsat_value_construct_from_constant_term(mcsat_value_t* t_value, term_table_t* terms, term_t t) {	3,476✔
99	term_kind_t t_kind = term_kind(terms, t);	3,476✔
100	switch (t_kind) {	3,476✔
101	case BV_CONSTANT: {	1✔
102	bvconst_term_t* t_desc = bvconst_term_desc(terms, t);	1✔
103	bvconstant_t t_bvconst;
104	init_bvconstant(&t_bvconst);	1✔
105	bvconstant_set_bitsize(&t_bvconst, t_desc->bitsize);	1✔
106	bvconstant_copy(&t_bvconst, t_desc->bitsize, t_desc->data);	1✔
107	mcsat_value_construct_bv_value(t_value, &t_bvconst);	1✔
108	delete_bvconstant(&t_bvconst);	1✔
109	break;	1✔
110	}
111	case BV64_CONSTANT: {	3,321✔
112	// Propagate constant value (it's first time we see it, so should be safe
113	bvconst64_term_t* t_desc = bvconst64_term_desc(terms, t);	3,321✔
114	bvconstant_t t_bvconst;
115	init_bvconstant(&t_bvconst);	3,321✔
116	bvconstant_set_bitsize(&t_bvconst, t_desc->bitsize);	3,321✔
117	bvconstant_copy64(&t_bvconst, t_desc->bitsize, t_desc->value);	3,321✔
118	mcsat_value_construct_bv_value(t_value, &t_bvconst);	3,321✔
119	delete_bvconstant(&t_bvconst);	3,321✔
120	break;	3,321✔
121	}
122	case CONSTANT_TERM: {	4✔
123	// Boolean terms case
124	if (t == true_term \|\| t == false_term) {	4✔
125	mcsat_value_construct_bool(t_value, t == true_term);	3✔
126	} else {
127	// scalar case
128	int32_t int_value;
129	_o_yices_scalar_const_value(t, &int_value);	1✔
130	rational_t q;
131	q_init(&q);	1✔
132	q_set32(&q, int_value);	1✔
133	mcsat_value_construct_rational(t_value, &q);	1✔
134	q_clear(&q);	1✔
135	}
136	break;	4✔
137	}
138	case ARITH_CONSTANT: {	150✔
139	lp_rational_t rat_value;
140	lp_rational_construct(&rat_value);	150✔
141	q_get_mpq(rational_term_desc(terms, t), &rat_value);	150✔
142	lp_value_t lp_value;
143	lp_value_construct(&lp_value, LP_VALUE_RATIONAL, &rat_value);	150✔
144	mcsat_value_construct_lp_value(t_value, &lp_value);	150✔
145	lp_value_destruct(&lp_value);	150✔
146	lp_rational_destruct(&rat_value);	150✔
147	break;	150✔
148	}
149	default:	3,476✔
150	assert(false);
151	}
152	}	3,476✔
153
154
155	mcsat_value_t* mcsat_value_new_default() {	×
156	mcsat_value_t* result = (mcsat_value_t*) safe_malloc(sizeof(mcsat_value_t));	×
157	mcsat_value_construct_default(result);	×
UNCOV 158	return result;	×
159	}
160
161	mcsat_value_t* mcsat_value_new_bool(bool b) {	×
162	mcsat_value_t* result = (mcsat_value_t*) safe_malloc(sizeof(mcsat_value_t));	×
163	mcsat_value_construct_bool(result, b);	×
UNCOV 164	return result;	×
165	}
166
167	mcsat_value_t* mcsat_value_new_rational(const rational_t *q) {	×
168	mcsat_value_t* result = (mcsat_value_t*) safe_malloc(sizeof(mcsat_value_t));	×
169	mcsat_value_construct_rational(result, q);	×
UNCOV 170	return result;	×
171	}
172
UNCOV 173	mcsat_value_t* mcsat_value_new_lp_value(const lp_value_t *lp_value) {	×
UNCOV 174	mcsat_value_t* result = (mcsat_value_t*) safe_malloc(sizeof(mcsat_value_t));	×
UNCOV 175	mcsat_value_construct_lp_value(result, lp_value);	×
UNCOV 176	return result;	×
177	}
178
UNCOV 179	mcsat_value_t* mcsat_value_new_bv_value(const bvconstant_t *bv_value) {	×
UNCOV 180	mcsat_value_t* result = (mcsat_value_t*) safe_malloc(sizeof(mcsat_value_t));	×
UNCOV 181	mcsat_value_construct_bv_value(result, bv_value);	×
UNCOV 182	return result;	×
183	}
184
185	mcsat_value_t* mcsat_value_new_copy(const mcsat_value_t *from) {	178,580✔
186	mcsat_value_t* result = (mcsat_value_t*) safe_malloc(sizeof(mcsat_value_t));	178,580✔
187	mcsat_value_construct_copy(result, from);	178,580✔
188	return result;	178,580✔
189	}
190
191	void mcsat_value_destruct(mcsat_value_t* value) {	2,715,695✔
192	switch (value->type) {	2,715,695✔
193	case VALUE_NONE:	353,015✔
194	break;	353,015✔
195	case VALUE_BOOLEAN:	1,243,893✔
196	break;	1,243,893✔
197	case VALUE_RATIONAL:	449,517✔
198	q_clear(&value->q);	449,517✔
199	break;	449,517✔
200	case VALUE_LIBPOLY:	42,094✔
201	lp_value_destruct(&value->lp_value);	42,094✔
202	break;	42,094✔
203	case VALUE_BV:	627,176✔
204	delete_bvconstant(&value->bv_value);	627,176✔
205	break;	627,176✔
206	default:	2,715,695✔
207	assert(false);
208	}
209	}	2,715,695✔
210
211	void mcsat_value_delete(mcsat_value_t* value) {	178,580✔
212	mcsat_value_destruct(value);	178,580✔
213	safe_free(value);	178,580✔
214	}	178,580✔
215
216	void mcsat_value_assign(mcsat_value_t* value, const mcsat_value_t* from) {	1,511,472✔
217	if (value != from) {	1,511,472✔
218	mcsat_value_destruct(value);	1,511,472✔
219	mcsat_value_construct_copy(value, from);	1,511,472✔
220	}
221	}	1,511,472✔
222
223	void mcsat_value_print(const mcsat_value_t* value, FILE* out) {	×
224	switch (value->type) {	×
225	case VALUE_NONE:	×
226	fprintf(out, "<NONE>");	×
227	break;	×
228	case VALUE_BOOLEAN:	×
229	if (value->b) {	×
230	fprintf(out, "true");	×
231	} else {
UNCOV 232	fprintf(out, "false");	×
233	}
234	break;	×
UNCOV 235	case VALUE_RATIONAL:	×
UNCOV 236	q_print(out, (rational_t*) &value->q);	×
UNCOV 237	break;	×
UNCOV 238	case VALUE_LIBPOLY:	×
UNCOV 239	lp_value_print(&value->lp_value, out);	×
UNCOV 240	break;	×
UNCOV 241	case VALUE_BV:	×
UNCOV 242	bvconst_print(out, value->bv_value.data, value->bv_value.bitsize);	×
UNCOV 243	break;	×
UNCOV 244	default:	×
245	assert(false);
246	}
UNCOV 247	}	×
248
249	bool mcsat_value_eq(const mcsat_value_t* v1, const mcsat_value_t* v2) {	109,143,875✔
250	if (v1 == v2) {	109,143,875✔
251	return true;	266,169✔
252	}
253	switch (v1->type) {	108,877,706✔
254	case VALUE_BOOLEAN:	8,714,812✔
255	assert(v2->type == VALUE_BOOLEAN);
256	return v1->b == v2->b;	8,714,812✔
257	case VALUE_RATIONAL:	99,184,224✔
258	if (v2->type == VALUE_RATIONAL) {	99,184,224✔
259	return q_cmp(&v1->q, &v2->q) == 0;	99,184,224✔
260	} else {
261	assert(v2->type == VALUE_LIBPOLY);
262	mpq_t v1_mpq;
UNCOV 263	mpq_init(v1_mpq);	×
UNCOV 264	q_get_mpq((rational_t*)&v1->q, v1_mpq);	×
265	lp_value_t v1_lp;
266	lp_value_construct_none(&v1_lp);	×
267	lp_value_assign_raw(&v1_lp, LP_VALUE_RATIONAL, &v1_mpq);	×
UNCOV 268	int cmp = lp_value_cmp(&v1_lp, &v2->lp_value);	×
269	lp_value_destruct(&v1_lp);	×
270	mpq_clear(v1_mpq);	×
271	return cmp == 0;	×
272	}
273	case VALUE_LIBPOLY:	505,744✔
274	if (v2->type == VALUE_LIBPOLY) {	505,744✔
275	return lp_value_cmp(&v1->lp_value, &v2->lp_value) == 0;	505,744✔
276	} else {
277	assert(v1->type == VALUE_RATIONAL);
278	mpq_t v2_mpq;
UNCOV 279	mpq_init(v2_mpq);	×
UNCOV 280	q_get_mpq((rational_t*)&v2->q, v2_mpq);	×
281	lp_value_t v2_lp;
UNCOV 282	lp_value_construct_none(&v2_lp);	×
283	lp_value_assign_raw(&v2_lp, LP_VALUE_RATIONAL, &v2_mpq);	×
UNCOV 284	int cmp = lp_value_cmp(&v1->lp_value, &v2_lp);	×
UNCOV 285	lp_value_destruct(&v2_lp);	×
UNCOV 286	mpq_clear(v2_mpq);	×
UNCOV 287	return cmp == 0;	×
288	}
289	case VALUE_BV: {	472,926✔
290	assert(v2->type == VALUE_BV);
291	assert(v1->bv_value.bitsize == v2->bv_value.bitsize);
292	return bvconst_eq(v1->bv_value.data, v2->bv_value.data, v1->bv_value.width);	472,926✔
293	}
UNCOV 294	default:	×
295	assert(false);
UNCOV 296	return false;	×
297	}
298	}
299
300	uint32_t mcsat_value_hash(const mcsat_value_t* v) {	14,654,140✔
301	switch (v->type) {	14,654,140✔
302	case VALUE_BOOLEAN:	972,539✔
303	return v->b;	972,539✔
304	case VALUE_RATIONAL:	13,415,982✔
305	{
306	mpq_t v_mpq;
307	mpq_init(v_mpq);	13,415,982✔
308	q_get_mpq((rational_t*)&v->q, v_mpq);	13,415,982✔
309	lp_value_t v_lp;
310	lp_value_construct_none(&v_lp);	13,415,982✔
311	lp_value_assign_raw(&v_lp, LP_VALUE_RATIONAL, &v_mpq);	13,415,982✔
312	uint32_t hash = lp_value_hash(&v_lp);	13,415,982✔
313	lp_value_destruct(&v_lp);	13,415,982✔
314	mpq_clear(v_mpq);	13,415,982✔
315	return hash;	13,415,982✔
316	}
317	case VALUE_LIBPOLY:	219,468✔
318	return lp_value_hash(&v->lp_value);	219,468✔
319	case VALUE_BV: {	46,151✔
320	bvconst_normalize(v->bv_value.data, v->bv_value.bitsize);	46,151✔
321	return bvconst_hash(v->bv_value.data, v->bv_value.bitsize);	46,151✔
322	}
323	default:	×
324	assert(false);
UNCOV 325	return 0;	×
326	}
327	}
328
329	term_t mcsat_value_to_term(const mcsat_value_t* mcsat_value, term_manager_t* tm) {	360✔
330
331	term_t result = NULL_TERM;	360✔
332
333	switch (mcsat_value->type) {	360✔
334	case VALUE_BOOLEAN:	3✔
335	if (mcsat_value->b) {	3✔
UNCOV 336	result = true_term;	×
337	} else {
338	result = false_term;	3✔
339	}
340	break;	3✔
341	case VALUE_BV: {	357✔
342	const bvconstant_t* bv = &mcsat_value->bv_value;	357✔
343	result = mk_bv_constant(tm, (bvconstant_t*) bv);	357✔
344	break;	357✔
345	}
346	case VALUE_RATIONAL: {	×
347	result = mk_arith_constant(tm, (rational_t*) &mcsat_value->q);	×
UNCOV 348	break;	×
349	}
350	case VALUE_LIBPOLY:	×
UNCOV 351	if (lp_value_is_rational(&mcsat_value->lp_value)) {	×
352	lp_rational_t lp_q;
UNCOV 353	lp_rational_construct(&lp_q);	×
UNCOV 354	lp_value_get_rational(&mcsat_value->lp_value, &lp_q);	×
355	rational_t q;
UNCOV 356	q_init(&q);	×
UNCOV 357	q_set_mpq(&q, &lp_q);	×
UNCOV 358	result = mk_arith_constant(tm, &q);	×
UNCOV 359	q_clear(&q);	×
UNCOV 360	lp_rational_destruct(&lp_q);	×
361	} else {
362	assert(false);
UNCOV 363	result = NULL_TERM;	×
364	}
UNCOV 365	break;	×
366	default:	360✔
367	assert(false);
368	}
369
370	return result;	360✔
371	}
372
373	value_t mcsat_value_to_value(const mcsat_value_t* mcsat_value, type_table_t types, type_t type, value_table_t vtbl) {	103✔
374	value_t value = null_value;	103✔
375	switch (mcsat_value->type) {	103✔
376	case VALUE_BOOLEAN:	22✔
377	value = vtbl_mk_bool(vtbl, mcsat_value->b);	22✔
378	break;	22✔
379	case VALUE_RATIONAL: {	11✔
380	type_kind_t kind = type_kind(types, type);	11✔
381	if (kind == UNINTERPRETED_TYPE \|\| kind == SCALAR_TYPE) {	22✔
382	int32_t id;
383	bool ok = q_get32((rational_t *)&mcsat_value->q, &id);	11✔
384	(void) ok; // unused in release build
385	assert(ok);
386	value = vtbl_mk_const(vtbl, type, id, NULL);	11✔
387	} else {
UNCOV 388	value = vtbl_mk_rational(vtbl, (rational_t *) &mcsat_value->q);	×
389	}
390	break;	11✔
391	}
392	case VALUE_LIBPOLY:	67✔
393	if (lp_value_is_rational(&mcsat_value->lp_value)) {	67✔
394	lp_rational_t lp_q;
395	lp_rational_construct(&lp_q);	55✔
396	lp_value_get_rational(&mcsat_value->lp_value, &lp_q);	55✔
397	rational_t q;
398	q_init(&q);	55✔
399	q_set_mpq(&q, &lp_q);	55✔
400	type_kind_t kind = type_kind(types, type);	55✔
401	if (kind == UNINTERPRETED_TYPE \|\| kind == SCALAR_TYPE) {	57✔
402	int32_t id;
403	bool ok = q_get32(&q, &id);	2✔
404	(void) ok; // unused in release build
405	assert(ok);
406	value = vtbl_mk_const(vtbl, type, id, NULL);	2✔
407	} else {
408	value = vtbl_mk_rational(vtbl, &q);	53✔
409	}
410	q_clear(&q);	55✔
411	lp_rational_destruct(&lp_q);	55✔
412	} else {
413	value = vtbl_mk_algebraic(vtbl, (void*) &mcsat_value->lp_value.value.a);	12✔
414	}
415	break;	67✔
416	case VALUE_BV:	3✔
417	value = vtbl_mk_bv_from_bv(vtbl, mcsat_value->bv_value.bitsize, mcsat_value->bv_value.data);	3✔
418	break;	3✔
419	default:	103✔
420	assert(false);
421	}
422	return value;	103✔
423	}
424
425	void mcsat_value_construct_from_value(mcsat_value_t* mcsat_value, value_table_t* vtbl, value_t v) {	180✔
426	value_kind_t v_kind = object_kind(vtbl, v);	180✔
427	switch (v_kind) {	180✔
428	case BOOLEAN_VALUE:	33✔
429	mcsat_value_construct_bool(mcsat_value, is_true(vtbl, v));	33✔
430	break;	33✔
431	case RATIONAL_VALUE: {	123✔
432	rational_t* value_q = vtbl_rational(vtbl, v);	123✔
433	mpq_t value_mpq;
434	mpq_init(value_mpq);	123✔
435	q_get_mpq(value_q, value_mpq);	123✔
436	lp_value_t value_lp;
437	lp_value_construct(&value_lp, LP_VALUE_RATIONAL, value_mpq);	123✔
438	mcsat_value_construct_lp_value(mcsat_value, &value_lp);	123✔
439	lp_value_destruct(&value_lp);	123✔
440	mpq_clear(value_mpq);	123✔
441	break;	123✔
442	}
UNCOV 443	case ALGEBRAIC_VALUE: {	×
UNCOV 444	lp_algebraic_number_t* a = vtbl_algebraic_number(vtbl, v);	×
445	lp_value_t value_lp;
UNCOV 446	lp_value_construct(&value_lp, LP_VALUE_ALGEBRAIC, a);	×
UNCOV 447	mcsat_value_construct_lp_value(mcsat_value, &value_lp);	×
UNCOV 448	lp_value_destruct(&value_lp);	×
UNCOV 449	break;	×
450	}
451	case BITVECTOR_VALUE: {	24✔
452	value_bv_t* v1 = vtbl_bitvector(vtbl, v);	24✔
453	bvconstant_t v2;
454	init_bvconstant(&v2);	24✔
455	bvconstant_copy(&v2, v1->nbits, v1->data);	24✔
456	mcsat_value_construct_bv_value(mcsat_value, &v2);	24✔
457	delete_bvconstant(&v2);	24✔
458	break;	24✔
459	}
460	default:	180✔
461	assert(false);
462	}
463	}	180✔
464
465	bool mcsat_value_is_zero(const mcsat_value_t* value) {	12✔
466	switch (value->type) {	12✔
UNCOV 467	case VALUE_RATIONAL:	×
UNCOV 468	return q_is_zero(&value->q);	×
469	case VALUE_LIBPOLY: {	12✔
470	lp_rational_t zero;
471	lp_rational_construct(&zero);	12✔
472	int cmp = lp_value_cmp_rational(&value->lp_value, &zero);	12✔
473	lp_rational_destruct(&zero);	12✔
474	return cmp == 0;	12✔
475	}
UNCOV 476	default:	×
UNCOV 477	return false;	×
478	}
479	}
480
481	bool mcsat_value_is_true(const mcsat_value_t* value) {	815,389✔
482	return value->type == VALUE_BOOLEAN && value->b;	815,389✔
483	}
484
UNCOV 485	bool mcsat_value_is_false(const mcsat_value_t* value) {	×
UNCOV 486	return value->type == VALUE_BOOLEAN && !value->b;	×
487	}

SRI-CSL / yices2 / 8762094294

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