Bugfixes and cleanups to support backtracing in mcarith.

SRI-CSL · Sep 26, 2023 · b2eb4fc · b2eb4fc
1 parent c017ba4
commit b2eb4fc
Show file tree

Hide file tree

Showing 6 changed files with 197 additions and 148 deletions.
diff --git a/src/api/yices_api.c b/src/api/yices_api.c
@@ -10772,9 +10772,11 @@ static void yices_get_arith_value(model_t *mdl, term_t t, arithval_struct_t *r)
   if (object_is_rational(vtbl, v)) {
     r->tag = ARITHVAL_RATIONAL;
     r->val.q = vtbl_rational(vtbl, v);
+#ifdef HAVE_MCSAT
   } else if (object_is_algebraic(vtbl, v)) {
     r->tag = ARITHVAL_ALGEBRAIC;
     r->val.p = vtbl_algebraic_number(vtbl, v);
+#endif
   } else {
     // should not happen since t is an arithmetic term
     set_error_code(INTERNAL_EXCEPTION);

diff --git a/src/context/context.c b/src/context/context.c
@@ -5349,6 +5349,7 @@ static void create_simplex_solver(context_t *ctx, bool automatic) {
  * Create an initialize the simplex solver and attach it to the core
  * or to the egraph if the egraph exists.
  */
+#ifdef HAVE_MCSAT
 static void create_mcarith_solver(context_t *ctx) {
   mcarith_solver_t *solver;
   smt_mode_t cmode;
@@ -5380,7 +5381,12 @@ static void create_mcarith_solver(context_t *ctx) {
   ctx->arith_solver = solver;
   ctx->arith = *mcarith_arith_interface(solver);
 }
-
+#else
+static void create_mcarith_solver(context_t *ctx) {
+  fprintf(stderr, "mcarithmetic solver not supported.\n");
+  exit(-1);
+}
+#endif
 
 /*
  * Create IDL/SIMPLEX solver based on ctx->dl_profile
@@ -5777,9 +5783,6 @@ void init_context(context_t *ctx, term_table_t *terms, smt_logic_t logic,
   ctx->en_quant = false;
 }
 
-
-void arithval_in_model_delete(arithval_in_model_t* v);
-
 void arithval_in_model_delete(arithval_in_model_t* v) {
   switch (v->tag) {
   case ARITHVAL_RATIONAL:
@@ -5802,8 +5805,7 @@ void arithval_in_model_reset(arithval_in_model_t* v) {
       break;
 #ifdef HAVE_MCSAT
     case ARITHVAL_ALGEBRAIC:
-      lp_algebraic_number_destruct(&v->
-      val.alg_number);
+      lp_algebraic_number_destruct(&v->val.alg_number);
       v->tag = ARITHVAL_RATIONAL;
       q_init(&v->val.q);
       break;

diff --git a/src/context/context_solver.c b/src/context/context_solver.c
@@ -887,7 +887,6 @@ static value_t bool_value(context_t *ctx, value_table_t *vtbl, literal_t l) {
   return v;
 }
 
-
 /*
  * Value of arithmetic variable x in ctx->arith_solver
  */

diff --git a/src/context/context_types.h b/src/context/context_types.h
@@ -258,25 +258,14 @@ enum {
 typedef enum arithval_tag {
   ARITHVAL_ERROR,
   ARITHVAL_RATIONAL,
-#ifdef HAVE_MCSAT
   ARITHVAL_ALGEBRAIC,
-#endif
 } arithval_tag_t;
 
 /*
  * Tagged union to represent pointers to either rational or algebraic numbers.
  * The flag can ERROR/RATIONAL/ALGEBRAIC
  */
-typedef struct {
-  arithval_tag_t tag;
-  union {
-    rational_t q;
-#ifdef HAVE_MCSAT
-    lp_algebraic_number_t alg_number;
-#endif
-  } val;
-} arithval_in_model_t;
-
+typedef struct arithval_in_model_s arithval_in_model_t;
 
 /**************************
  *  ARITHMETIC INTERFACE  *
@@ -662,6 +651,16 @@ typedef struct dl_data_s {
  *  CONTEXT   *
  *************/
 
+struct arithval_in_model_s {
+  arithval_tag_t tag;
+  union {
+    rational_t q;
+#ifdef HAVE_MCSAT
+    lp_algebraic_number_t alg_number;
+#endif
+  } val;
+};
+
 struct context_s {
   // mode + architecture + logic code
   context_mode_t mode;