Jhx/mcarith

Makefile.build

@@ -86,7 +86,8 @@ MKVERSION=./utils/make_source_version
 #
 srcdir = src
 srcsubdirs = mt io terms utils solvers solvers/floyd_warshall \
-    solvers/funs solvers/bv solvers/egraph solvers/cdcl solvers/simplex solvers/quant \
+    solvers/funs solvers/bv solvers/egraph solvers/cdcl solvers/mcarith \
+    solvers/simplex solvers/quant \
     parser_utils model scratch api frontend frontend/common \
     frontend/smt1 frontend/yices frontend/smt2 context exists_forall \
     mcsat mcsat/eq mcsat/weq mcsat/uf mcsat/bool mcsat/ite mcsat/nra mcsat/bv \

src/Makefile

@@ -203,6 +203,7 @@ core_src_c := \
 	solvers/funs/fun_level.c \
 	solvers/funs/fun_solver.c \
 	solvers/funs/stratification.c \
+	solvers/mcarith/mcarith.c \
 	solvers/simplex/arith_atomtable.c \
 	solvers/simplex/arith_vartable.c \
 	solvers/simplex/diophantine_systems.c \
@@ -495,6 +496,7 @@ bin_src_c := \
 	frontend/yices_sat_new.c \
 	frontend/yices_smt.c \
 	frontend/yices_smt2.c \
+	frontend/yices_smt2_lc.c \
 	frontend/yices_smtcomp.c \
 
 #

src/api/context_config.c

@@ -181,7 +181,8 @@ static const int32_t logic2arch[NUM_SMT_LOGICS] = {
   CTX_ARCH_SPLX,       // QF_LRA
   CTX_ARCH_SPLX,       // QF_LIRA
   CTX_ARCH_MCSAT,      // QF_NIA
-  CTX_ARCH_MCSAT,      // QF_NRA
+//  CTX_ARCH_MCSAT, // QF_NRA
+  CTX_ARCH_MCSATARITH, // QF_NRA
   CTX_ARCH_MCSAT,      // QF_NIRA
   CTX_ARCH_SPLX,       // QF_RDL
   CTX_ARCH_EG,         // QF_UF

src/api/yices_api.c

@@ -10731,12 +10731,6 @@ int32_t _o_yices_get_bool_value(model_t *mdl, term_t t, int32_t *val) {
  *   code = EVAL_OVERFLOW
  */
 
-typedef enum arithval_tag {
-  ARITHVAL_ERROR,
-  ARITHVAL_RATIONAL,
-  ARITHVAL_ALGEBRAIC,
-} arithval_tag_t;
-
 /*
  * Tagged union to represent pointers to either rational or algebraic numbers.
  * The flag can ERROR/RATIONAL/ALGEBRAIC
@@ -10778,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);

src/context/context.c

@@ -31,6 +31,7 @@
 #include "solvers/floyd_warshall/idl_floyd_warshall.h"
 #include "solvers/floyd_warshall/rdl_floyd_warshall.h"
 #include "solvers/funs/fun_solver.h"
+#include "solvers/mcarith/mcarith.h"
 #include "solvers/quant/quant_solver.h"
 #include "solvers/simplex/simplex.h"
 #include "terms/poly_buffer_terms.h"
@@ -1486,7 +1487,17 @@ static void __attribute__((noreturn))  bad_divisor(context_t *ctx, term_t t) {
 static thvar_t map_rdiv_to_arith(context_t *ctx, composite_term_t *div) {
   // Could try to evaluate t2 then check whether that's a constant
   assert(div->arity == 2);
-  bad_divisor(ctx, div->arg[1]);
+  thvar_t x;
+  thvar_t num;
+  thvar_t den;
+
+  num = internalize_to_arith(ctx, div->arg[0]);
+  den = internalize_to_arith(ctx, div->arg[1]);
+  if (ctx->arith.create_rdiv == NULL) {
+    bad_divisor(ctx, div->arg[1]);
+  }
+  x = ctx->arith.create_rdiv(ctx->arith_solver, num, den);
+  return x;
 }
 
 
@@ -2652,10 +2663,10 @@ static occ_t internalize_to_eterm(context_t *ctx, term_t t) {
         break;
 
       case ARITH_RDIV:
-	assert(is_arithmetic_type(tau));
-	x = map_rdiv_to_arith(ctx, arith_rdiv_term_desc(terms, r));
-	u = translate_arithvar_to_eterm(ctx, x);
-	break;
+	      assert(is_arithmetic_type(tau));
+  	    x = map_rdiv_to_arith(ctx, arith_rdiv_term_desc(terms, r));
+	      u = translate_arithvar_to_eterm(ctx, x);
+	      break;
 
       case ARITH_IDIV:
 	assert(is_integer_type(tau));
@@ -4961,7 +4972,8 @@ static const uint32_t arch2theories[NUM_ARCH] = {
   IDL_MASK,                    //  CTX_ARCH_AUTO_IDL
   RDL_MASK,                    //  CTX_ARCH_AUTO_RDL
 
-  UF_MASK|ARITH_MASK|FUN_MASK  //  CTX_ARCH_MCSAT
+  UF_MASK|ARITH_MASK|FUN_MASK, //  CTX_ARCH_MCSAT
+  ARITH_MASK                   //  CTX_ARCH_MCSATARITH
 };
 
 
@@ -4979,6 +4991,7 @@ static const uint32_t arch2theories[NUM_ARCH] = {
 #define BVSLVR 0x10
 #define FSLVR  0x20
 #define MCSAT  0x40
+#define AMCSAT 0x80
 
 static const uint8_t arch_components[NUM_ARCH] = {
   0,                        //  CTX_ARCH_NOSOLVERS
@@ -4999,7 +5012,8 @@ static const uint8_t arch_components[NUM_ARCH] = {
   0,                        //  CTX_ARCH_AUTO_IDL
   0,                        //  CTX_ARCH_AUTO_RDL
 
-  MCSAT                     //  CTX_ARCH_MCSAT
+  MCSAT,                    //  CTX_ARCH_MCSAT
+  AMCSAT                    //  CTX_ARCH_MCSATARITH
 };
 
 
@@ -5170,7 +5184,7 @@ bool context_arch_has_fun(context_arch_t arch) {
 }
 
 bool context_arch_has_arith(context_arch_t arch) {
-  return arch_components[arch] & (SPLX|IFW|RFW);
+  return arch_components[arch] & (AMCSAT|SPLX|IFW|RFW);
 }
 
 bool context_arch_has_mcsat(context_arch_t arch) {
@@ -5331,6 +5345,48 @@ static void create_simplex_solver(context_t *ctx, bool automatic) {
   ctx->arith = *simplex_arith_interface(solver);
 }
 
+/*
+ * 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;
+
+  assert(ctx->arith_solver == NULL && ctx->core != NULL);
+
+  cmode = core_mode[ctx->mode];
+  init_mcarith_solver(&solver, ctx);
+
+  // row saving must be enabled unless we're in ONECHECK mode
+  if (ctx->mode != CTX_MODE_ONECHECK) {
+    mcarith_enable_row_saving(solver);
+  }
+
+  if (ctx->egraph != NULL) {
+    // FIXME
+    longjmp(ctx->env, INTERNAL_ERROR);
+    // attach the simplex solver as a satellite solver to the egraph
+//    egraph_attach_arithsolver(ctx->egraph, solver, mcarith_ctrl_interface(solver),
+//                              mcarith_smt_interface(solver), simplex_egraph_interface(solver),
+//                              simplex_arith_egraph_interface(solver));
+  } else {
+    // attach simplex to the core and initialize the core
+    init_smt_core(ctx->core, CTX_DEFAULT_CORE_SIZE, solver, mcarith_ctrl_interface(solver),
+                  mcarith_smt_interface(solver), cmode);
+  }
+
+  //simplex_solver_init_jmpbuf(solver, &ctx->env);
+  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
@@ -5511,7 +5567,9 @@ static void init_solvers(context_t *ctx) {
   }
 
   // Arithmetic solver
-  if (solvers & SPLX) {
+  if (solvers & AMCSAT) {
+    create_mcarith_solver(ctx);
+  } else if (solvers & SPLX) {
     create_simplex_solver(ctx, false);
   } else if (solvers & IFW) {
     create_idl_solver(ctx, false);
@@ -5606,7 +5664,7 @@ static inline bool valid_mode(context_mode_t mode) {
 }
 
 static inline bool valid_arch(context_arch_t arch) {
-  return CTX_ARCH_NOSOLVERS <= arch && arch <= CTX_ARCH_MCSAT;
+  return CTX_ARCH_NOSOLVERS <= arch && arch < NUM_ARCH;
 }
 #endif
 
@@ -5707,7 +5765,8 @@ void init_context(context_t *ctx, term_table_t *terms, smt_logic_t logic,
 
   ctx->bvpoly_buffer = NULL;
 
-  q_init(&ctx->aux);
+  ctx->aval.tag = ARITHVAL_RATIONAL;
+  q_init(&ctx->aval.val.q);
   init_bvconstant(&ctx->bv_buffer);
 
   ctx->trace = NULL;
@@ -5724,7 +5783,39 @@ 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) {
+  switch (v->tag) {
+  case ARITHVAL_RATIONAL:
+    q_clear(&v->val.q);
+    break;
+  #ifdef HAVE_MCSAT
+  case ARITHVAL_ALGEBRAIC:
+    lp_algebraic_number_destruct(&v->val.alg_number);
+  #endif
+  default:
+    break;
+  }
+  v->tag = ARITHVAL_ERROR;
+}
 
+void arithval_in_model_reset(arithval_in_model_t* v) {
+  switch (v->tag) {
+    case ARITHVAL_RATIONAL:
+      q_clear(&v->val.q);
+      break;
+#ifdef HAVE_MCSAT
+    case ARITHVAL_ALGEBRAIC:
+      lp_algebraic_number_destruct(&v->val.alg_number);
+      v->tag = ARITHVAL_RATIONAL;
+      q_init(&v->val.q);
+      break;
+#endif
+    default:
+      v->tag = ARITHVAL_RATIONAL;
+      q_init(&v->val.q);
+      break;
+  }
+}
 
 
 /*
@@ -5807,7 +5898,7 @@ void delete_context(context_t *ctx) {
 
   context_free_bvpoly_buffer(ctx);
 
-  q_clear(&ctx->aux);
+  arithval_in_model_delete(&ctx->aval);
   delete_bvconstant(&ctx->bv_buffer);
 }
 
@@ -5861,7 +5952,7 @@ void reset_context(context_t *ctx) {
 
   context_free_bvpoly_buffer(ctx);
 
-  q_clear(&ctx->aux);
+  arithval_in_model_reset(&ctx->aval);
 }
 
 

src/context/context_solver.c

@@ -887,19 +887,33 @@ 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
  */
 static value_t arith_value(context_t *ctx, value_table_t *vtbl, thvar_t x) {
-  rational_t *a;
+  arithval_in_model_t *a;
   value_t v;
 
   assert(context_has_arith_solver(ctx));
 
-  a = &ctx->aux;
+  a = &ctx->aval;
   if (ctx->arith.value_in_model(ctx->arith_solver, x, a)) {
-    v = vtbl_mk_rational(vtbl, a);
+    switch (a->tag) {
+      case ARITHVAL_RATIONAL:
+        v = vtbl_mk_rational(vtbl, &a->val.q);
+        break;
+#ifdef HAVE_MCSAT
+      case ARITHVAL_ALGEBRAIC:
+        v = vtbl_mk_algebraic(vtbl, &a->val.alg_number);
+        lp_algebraic_number_destruct(&a->val.alg_number);
+        a->tag = ARITHVAL_RATIONAL;
+        q_init(&a->val.q);
+        break;
+#endif
+      default:
+        v = vtbl_mk_unknown(vtbl);
+        break;
+    }
   } else {
     v = vtbl_mk_unknown(vtbl);
   }