16032530443

Committed 02 Jul 2025 06:08PM UTC coverage: 60.349% (-5.0%) from 65.357%

Build # 16032530443

Build Type

Pull #582

github

Committed by

web-flow

Commit Message

Merge b7e09d316 into b3af64ab1

Pull Request Pull Request #582: Update ci

Run Details

63716 of 105580 relevant lines covered (60.35%)

1127640.75 hits per line

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

6.99

/src/api/context_config.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/>.
 */

/*
 * OBJECT TO STORE CONTEXT CONFIGURATIONS
 */

#include <stdbool.h>
#include <assert.h>

#include "api/context_config.h"
#include "utils/memalloc.h"
#include "utils/string_utils.h"


/*
 * Mapping from strings to context modes (cf. string_utils.h)
 */
static const char * const mode_names[NUM_MODES] = {
  "interactive",
  "multi-checks",
  "one-shot",
  "push-pop",
};

static const int32_t mode[NUM_MODES] = {
  CTX_MODE_INTERACTIVE,
  CTX_MODE_MULTICHECKS,
  CTX_MODE_ONECHECK,
  CTX_MODE_PUSHPOP,
};

static const char * const solver_type_names[NUM_SOLVER_TYPES] = {
  "dpllt",
  "mcsat"
};

static const int32_t solver_type[NUM_SOLVER_TYPES] = {
  CTX_SOLVER_TYPE_DPLLT,
  CTX_SOLVER_TYPE_MCSAT
};

/*
 * Solver codes
 */
static const char * const solver_code_names[NUM_SOLVER_CODES] = {
  "auto",
  "default",
  "ifw",
  "none",
  "rfw",
  "simplex",
};

static const int32_t solver_code[NUM_SOLVER_CODES] = {
  CTX_CONFIG_AUTO,
  CTX_CONFIG_DEFAULT,
  CTX_CONFIG_ARITH_IFW,
  CTX_CONFIG_NONE,
  CTX_CONFIG_ARITH_RFW,
  CTX_CONFIG_ARITH_SIMPLEX,
};


/*
 * Descriptor fields (other than "logic")
 */
typedef enum ctx_config_key {
  CTX_CONFIG_KEY_MODE,
  CTX_CONFIG_KEY_SOLVER_TYPE,
  CTX_CONFIG_KEY_TRACE_TAGS,
  CTX_CONFIG_KEY_ARITH_FRAGMENT,
  CTX_CONFIG_KEY_UF_SOLVER,
  CTX_CONFIG_KEY_ARRAY_SOLVER,
  CTX_CONFIG_KEY_BV_SOLVER,
  CTX_CONFIG_KEY_ARITH_SOLVER,
  CTX_CONFIG_KEY_MODEL_INTERPOLATION,
} ctx_config_key_t;

#define NUM_CONFIG_KEYS (CTX_CONFIG_KEY_MODEL_INTERPOLATION+1)


static const char *const config_key_names[NUM_CONFIG_KEYS] = {
  "arith-fragment",
  "arith-solver",
  "array-solver",
  "bv-solver",
  "mode",
  "model-interpolation",
  "solver-type",
  "trace",
  "uf-solver",
};

static const int32_t config_key[NUM_CONFIG_KEYS] = {
  CTX_CONFIG_KEY_ARITH_FRAGMENT,
  CTX_CONFIG_KEY_ARITH_SOLVER,
  CTX_CONFIG_KEY_ARRAY_SOLVER,
  CTX_CONFIG_KEY_BV_SOLVER,
  CTX_CONFIG_KEY_MODE,
  CTX_CONFIG_KEY_MODEL_INTERPOLATION,
  CTX_CONFIG_KEY_SOLVER_TYPE,
  CTX_CONFIG_KEY_TRACE_TAGS,
  CTX_CONFIG_KEY_UF_SOLVER,
};




/*
 * CONTEXT SETTING FOR A GIVEN LOGIC CODE
 */

/*
 * Conversion of SMT logic code to a default architecture code
 * -1 means not supported
 *
 * We don't use AUTO_IDL, AUTO_RDL, IFW or RFW here since
 * the Floyd-Warshall solvers don't support all use modes.
 *
 * IMPORTANT: this array is used by the API in config_for_logic.
 */
static const int32_t logic2arch[NUM_SMT_LOGICS] = {
  CTX_ARCH_NOSOLVERS,  // NONE

  -1,                  // AX
  -1,                  // BV  (supported by EF)
  -1,                  // FFA
  -1,                  // IDL (supported by EF)
  -1,                  // LIA (supported by EF)
  -1,                  // LRA (supported by EF)
  -1,                  // LIRA
  -1,                  // NIA
  -1,                  // NRA
  -1,                  // NIRA
  -1,                  // RDL
  -1,                  // UF
  -1,                  // ABV
  -1,                  // ALIA
  -1,                  // ALRA
  -1,                  // ALIRA
  -1,                  // ANIA
  -1,                  // ANRA
  -1,                  // ANIRA
  -1,                  // AUF
  -1,                  // BVLRA
  -1,                  // UFBV
  -1,                  // UFBVLIA
  -1,                  // UFIDL
  -1,                  // UFLIA
  -1,                  // UFLRA
  -1,                  // UFLIRA
  -1,                  // UFNIA
  -1,                  // UFNRA
  -1,                  // UFNIRA
  -1,                  // UFRDL
  -1,                  // AUFBV
  -1,                  // AUFBVLIA
  -1,                  // AUFBVNIA
  -1,                  // AUFLIA
  -1,                  // AUFLRA
  -1,                  // AUFLIRA
  -1,                  // AUFNIA
  -1,                  // AUFNRA
  -1,                  // AUFNIRA

  CTX_ARCH_EGFUN,      // QF_AX
  CTX_ARCH_BV,         // QF_BV
  CTX_ARCH_MCSAT,      // QF_FFA
  CTX_ARCH_SPLX,       // QF_IDL
  CTX_ARCH_SPLX,       // QF_LIA
  CTX_ARCH_SPLX,       // QF_LRA
  CTX_ARCH_SPLX,       // QF_LIRA
  CTX_ARCH_MCSAT,      // QF_NIA
  CTX_ARCH_MCSAT,      // QF_NRA
  CTX_ARCH_MCSAT,      // QF_NIRA
  CTX_ARCH_SPLX,       // QF_RDL
  CTX_ARCH_EG,         // QF_UF
  CTX_ARCH_EGFUNBV,    // QF_ABV
  CTX_ARCH_EGFUNSPLX,  // QF_ALIA
  CTX_ARCH_EGFUNSPLX,  // QF_ALRA
  CTX_ARCH_EGFUNSPLX,  // QF_ALIRA
  CTX_ARCH_MCSAT,      // QF_ANIA
  CTX_ARCH_MCSAT,      // QF_ANRA
  CTX_ARCH_MCSAT,      // QF_ANIRA
  CTX_ARCH_EGFUN,      // QF_AUF
  CTX_ARCH_EGSPLXBV,   // QF_BVLRA
  CTX_ARCH_EGBV,       // QF_UFBV
  CTX_ARCH_EGSPLXBV,   // QF_UFBVLIA

  CTX_ARCH_EGSPLX,     // QF_UFIDL
  CTX_ARCH_EGSPLX,     // QF_UFLIA
  CTX_ARCH_EGSPLX,     // QF_UFLRA
  CTX_ARCH_EGSPLX,     // QF_UFLIRA
  CTX_ARCH_MCSAT,      // QF_UFNIA
  CTX_ARCH_MCSAT,      // QF_UFNRA
  CTX_ARCH_MCSAT,      // QF_UFNIRA
  CTX_ARCH_EGSPLX,     // QF_UFRDL
  CTX_ARCH_EGFUNBV,    // QF_AUFBV
  CTX_ARCH_EGFUNSPLXBV, // QF_AUFBVLIA
  CTX_ARCH_MCSAT,      // QF_AUFBVNIA
  CTX_ARCH_EGFUNSPLX,  // QF_AUFLIA
  CTX_ARCH_EGFUNSPLX,  // QF_AUFLRA
  CTX_ARCH_EGFUNSPLX,  // QF_AUFLIRA
  CTX_ARCH_MCSAT,      // QF_AUFNIA
  CTX_ARCH_MCSAT,      // QF_AUFNRA
  CTX_ARCH_MCSAT,      // QF_AUFNIRA

  CTX_ARCH_EGFUNSPLXBV,  // ALL interpreted as QF_AUFLIRA + QF_BV
};



/*
 * WHICH ARITHMETIC FRAGMENTS REQUIRE THE DIOPHANTINE SUBSOLVER
 */
static const bool fragment2iflag[NUM_ARITH_FRAGMENTS+1] = {
  false,  // IDL
  false,  // RDL
  true,   // LIA
  false,  // LRA
  true,   // LIRA
  true,   // NIA
  false,  // NRA
  true,   // NIRA
  false,  // FFA
  false,  // no arithmetic
};


/*
 * Default configuration:
 * - enable PUSH/POP
 * - solver type = DPLL(T)
 * - no logic specified
 * - arith fragment = LIRA
 * - all solvers set to defaults
 */
static const ctx_config_t default_config = {
  CTX_MODE_PUSHPOP,       // mode
  CTX_SOLVER_TYPE_DPLLT,  // DPLLT solver
  SMT_UNKNOWN,            // logic
  CTX_CONFIG_DEFAULT,     // uf
  CTX_CONFIG_DEFAULT,     // array
  CTX_CONFIG_DEFAULT,     // bv
  CTX_CONFIG_DEFAULT,     // arith
  ARITH_LIRA,             // fragment
  false,                  // model interpolation
  NULL,                   // trace tags
};





/*
 * DIRECT CONFIGURATION
 */
int32_t arch_for_logic(smt_logic_t code) {
  assert(code != SMT_UNKNOWN);
  return logic2arch[code];
}

bool iflag_for_logic(smt_logic_t code) {
  assert(code != SMT_UNKNOWN);
  return fragment2iflag[arith_fragment(code)];
}



/*
 * CONFIG OBJECT
 */

/*
 * Initialize config to the default configuration
 */
void init_config_to_defaults(ctx_config_t *config) {
  *config = default_config;
}



/*
 * Set a default configuration to support the given logic
 * - return -1 if the logic name is not recognized
 * - return -2 if we don't support the logic yet
 * - return 0 otherwise
 *
 * If the function returns 0, the logic field is updated.
 * All other fields are left unchanged.
 */
int32_t config_set_logic(ctx_config_t *config, const char *logic) {
  smt_logic_t code;
  int32_t r;

  code = smt_logic_code(logic);
  if (code == SMT_UNKNOWN) {
    r = -1;
  } else if (logic2arch[code] < 0) {
    r = -2;
  } else {
    config->logic = (smt_logic_t) code;
    r = 0;
  }

  return r;
}


/*
 * Convert value to a solver
 */
static int32_t set_solver_code(const char *value, solver_code_t *dest) {
  int32_t v, r;

  v = parse_as_keyword(value, solver_code_names, solver_code, NUM_SOLVER_CODES);
  if (v < 0) {
    r = -2;
  } else if (v >= CTX_CONFIG_AUTO) {
    r = -3;
  } else {
    assert(v == CTX_CONFIG_DEFAULT || v == CTX_CONFIG_NONE);
    *dest = (solver_code_t) v;
    r = 0;
  }

  return r;
}


/*
 * Set an individual field in config
 * - key = field name
 * - value = value for that field
 *
 * Return code:
 *   -1 if the key is not recognized
 *   -2 if the value is not recognized
 *   -3 if the value is not valid for the key
 *    0 otherwise
 */
int32_t config_set_field(ctx_config_t *config, const char *key, const char *value) {
  int32_t k, v, r;
  arith_fragment_t arith;

  r = 0; // return code

  k = parse_as_keyword(key, config_key_names, config_key, NUM_CONFIG_KEYS);
  switch (k) {
  case CTX_CONFIG_KEY_MODE:
    v = parse_as_keyword(value, mode_names, mode, NUM_MODES);
    if (v < 0) {
      r = -2;
    } else {
      config->mode = v;
    }
    break;

  case CTX_CONFIG_KEY_SOLVER_TYPE:
    v = parse_as_keyword(value, solver_type_names, solver_type, NUM_SOLVER_TYPES);
    if (v < 0) {
      r = -2;
    } else {
      config->solver_type = v;
    }
    break;

  case CTX_CONFIG_KEY_TRACE_TAGS:
    config->trace_tags = safe_strdup(value);
    break;

  case CTX_CONFIG_KEY_ARITH_FRAGMENT:
    arith = arith_fragment_code(value);
    if (arith == ARITH_NONE) {
      r = -2;
    } else {
      config->arith_fragment = arith;
    }
    break;

  case CTX_CONFIG_KEY_UF_SOLVER:
    r = set_solver_code(value, &config->uf_config);
    break;

  case CTX_CONFIG_KEY_ARRAY_SOLVER:
    r = set_solver_code(value, &config->array_config);
    break;

  case CTX_CONFIG_KEY_BV_SOLVER:
    r = set_solver_code(value, &config->bv_config);
    break;

  case CTX_CONFIG_KEY_ARITH_SOLVER:
    v = parse_as_keyword(value, solver_code_names, solver_code, NUM_SOLVER_CODES);
    if (v < 0) {
      r = -2;
    } else {
      assert(0 <= v && v <= NUM_SOLVER_CODES);
      config->arith_config = v;
    }
    break;
  case CTX_CONFIG_KEY_MODEL_INTERPOLATION:
    v = parse_as_boolean(value, &config->model_interpolation);
    if (v < 0) {
      r = -2;
    }
    break;
  default:
    assert(k == -1);
    r = -1;
    break;
  }

  return r;
}



/*
 * Auxiliary functions to build architecture codes incrementally
 * - each function takes an integer a: a is either a valid architecture
 *   code or -1
 * - then the function adds a new solver component to a: this results
 *   in either a new valid code or -1 if the new component is not compatible with a.
 *
 * Important: we assume that the components are added in the following
 * order: egraph, array solver, bitvector solver, arithmetic solver
 */
static inline int32_t arch_add_egraph(int32_t a) {
  if (a == CTX_ARCH_NOSOLVERS) {
    a = CTX_ARCH_EG;
  } else {
    a = -1;
  }
  return a;
}

static int32_t arch_add_array(int32_t a) {
  if (a == CTX_ARCH_EG || a == CTX_ARCH_NOSOLVERS) {
    a = CTX_ARCH_EGFUN; // array requires egraph so we add both implicitly
  } else {
    a = -1;
  }
  return a;
}

static int32_t arch_add_bv(int32_t a) {
  switch (a) {
  case CTX_ARCH_NOSOLVERS:
    a = CTX_ARCH_BV;
    break;

  case CTX_ARCH_EG:
    a = CTX_ARCH_EGBV;
    break;

  case CTX_ARCH_EGFUN:
    a = CTX_ARCH_EGFUNBV;
    break;

  case CTX_ARCH_SPLX:
    a = CTX_ARCH_EGSPLXBV;
    break;

  default:
    a = -1;
    break;
  }

  return a;
}

// add the simplex solver
static int32_t arch_add_simplex(int32_t a) {
  switch (a) {
  case CTX_ARCH_NOSOLVERS:
    a = CTX_ARCH_SPLX;
    break;

  case CTX_ARCH_BV:
    a = CTX_ARCH_EGSPLXBV;
    break;

  case CTX_ARCH_EG:
    a = CTX_ARCH_EGSPLX;
    break;

  case CTX_ARCH_EGFUN:
    a = CTX_ARCH_EGFUNSPLX;
    break;

  case CTX_ARCH_EGBV:
    a = CTX_ARCH_EGSPLXBV;
    break;

  case CTX_ARCH_EGFUNBV:
    a = CTX_ARCH_EGFUNSPLXBV;
    break;

  default:
    a = -1;
    break;
  }

  return a;
}

// add a Floyd-Warshall solver
static int32_t arch_add_ifw(int32_t a) {
  if (a == CTX_ARCH_NOSOLVERS) {
    a = CTX_ARCH_IFW;
  } else {
    a = -1;
  }
  return a;
}

static int32_t arch_add_rfw(int32_t a) {
  if (a == CTX_ARCH_NOSOLVERS) {
    a = CTX_ARCH_RFW;
  } else {
    a = -1;
  }
  return a;
}


// add solver identified by code c to a
static int32_t arch_add_arith(int32_t a, solver_code_t c) {
  switch (c) {
  case CTX_CONFIG_NONE:  // no arithmetic solver
    break;

  case CTX_CONFIG_DEFAULT:  // simplex is the default
  case CTX_CONFIG_AUTO:     // auto = simplex here too
  case CTX_CONFIG_ARITH_SIMPLEX:
    a = arch_add_simplex(a);
    break;

  case CTX_CONFIG_ARITH_IFW:
    a = arch_add_ifw(a);
    break;

  case CTX_CONFIG_ARITH_RFW:
    a = arch_add_rfw(a);
    break;
  }
  return a;
}


/*
 * Check whether the architecture code a is compatible with mode
 * - current restriction: IFW and RFW don't support PUSH/POP or MULTIPLE CHECKS
 */
static bool arch_supports_mode(context_arch_t a, context_mode_t mode) {
  return (a != CTX_ARCH_IFW && a != CTX_ARCH_RFW) || mode == CTX_MODE_ONECHECK;
}


/*
 * Check whether the architecture is supported.
 */
static bool arch_is_supported(context_arch_t a) {
#if HAVE_MCSAT
  return true; // all architectures are supported
#else
  return a != CTX_ARCH_MCSAT;
#endif
}


/*
 * Check whether config is valid (and supported by this version of Yices)
 * and convert it to a tuple (arch, mode, iflag, qflag)
 * - arch = architecture code as defined in context.h
 * - mode = one of the context's modes
 * - iflag = true if the integer solver (in simplex) is required
 * - qflag = true if support for quantifiers is required
 *
 * Return code:
 *   0 if the config is valid and supported
 *  -1 if the config is invalid
 *  -2 if the config is valid but not currently supported
 *  -3 if the solver combination is valid but does not support the specified mode
 */
int32_t decode_config(const ctx_config_t *config, smt_logic_t *logic, context_arch_t *arch, context_mode_t *mode, bool *iflag, bool *qflag) {
  smt_logic_t logic_code;
  int32_t a, r;

  r = 0; // default return code

  logic_code = config->logic;
  if (logic_code != SMT_UNKNOWN) {
    /*
     * The intended logic is specified
     */
    assert(0 <= logic_code && logic_code < NUM_SMT_LOGICS);

    /*
     * Special case: difference logic + mode = ONECHECK + arith_config == AUTO
     */
    if (config->arith_config == CTX_CONFIG_AUTO && config->mode == CTX_MODE_ONECHECK) {
      if (logic_code == QF_IDL) {
        *logic = QF_IDL;
        *arch = CTX_ARCH_AUTO_IDL;
        *mode = CTX_MODE_ONECHECK;
        *iflag = false;
        *qflag = false;
        goto done;
      }

      if (logic_code == QF_RDL) {
        *logic = QF_RDL;
        *arch = CTX_ARCH_AUTO_RDL;
        *mode = CTX_MODE_ONECHECK;
        *iflag = false;
        *qflag = false;
        goto done;
      }
    }

    a = logic2arch[logic_code];
    if (a < 0 || !arch_is_supported(a)) {
      // not supported
      r = -2;
    } else {
      // good configuration
      *logic = logic_code;
      *arch = (context_arch_t) a;
      *iflag = iflag_for_logic(logic_code);
      *qflag = qflag_for_logic(logic_code);
      *mode = config->mode;
    }

  } else if (config->solver_type == CTX_SOLVER_TYPE_MCSAT) {
    if (arch_is_supported(CTX_ARCH_MCSAT)) {
      /*
       * MCSAT solver/no logic specified
       */
      *logic = SMT_UNKNOWN;
      *arch = CTX_ARCH_MCSAT;
      *mode = CTX_MODE_PUSHPOP;
      *iflag = false;
      *qflag = false;
    } else {
      // not compiled with MCSAT support so this is not supported
      r = -2;
    }

  } else {
    /*
     * No logic specified.
     */

    a = CTX_ARCH_NOSOLVERS;
    if (config->uf_config == CTX_CONFIG_DEFAULT) {
      a = arch_add_egraph(a);
    }
    if (config->array_config == CTX_CONFIG_DEFAULT) {
      a = arch_add_array(a);
    }
    if (config->bv_config == CTX_CONFIG_DEFAULT) {
      a = arch_add_bv(a);
    }
    a = arch_add_arith(a, config->arith_config);

    // a is either -1 or an architecture code
    if (a < 0) {
      r = -1; // invalid combination of solvers
    } else if (arch_supports_mode(a, config->mode)) {
      // good configuration
      *logic = SMT_UNKNOWN;
      *arch = (context_arch_t) a;
      *iflag = fragment2iflag[config->arith_fragment];
      *qflag = false;
      *mode = config->mode;
    } else {
      // mode is not supported by the solvers
      r = -3;
    }
  }

 done:
  return r;
}


/*
 * Cleanup a configutation descriptor
 */
void delete_config(ctx_config_t *config) {
  safe_free(config->trace_tags);
}


/*
 * Check whether a logic is supported by the MCSAT solver
 */
bool logic_is_supported_by_mcsat(smt_logic_t code) {
  return code == SMT_ALL || !logic_has_quantifiers(code);
}

/*
 * Check whether a logic requires the MCSAT solver
 */
bool logic_requires_mcsat(smt_logic_t code) {
  return arch_for_logic(code) == CTX_ARCH_MCSAT;
}

/*
 * Check whether a logic is supported by the exists/forall solver
 * - logics with quantifiers and BV or linear arithmetic are supported
 * - logic "NONE" == purely Boolean is supported too
 */
bool logic_is_supported_by_ef(smt_logic_t code) {
  return code == NONE || code == BV || code == IDL || code == LRA || code == RDL || code == LIA || code == UF;
}


/*
 * Context architecture for a logic supported by EF
 */
int32_t ef_arch_for_logic(smt_logic_t code) {
  switch (code) {
  case NONE:
    return CTX_ARCH_NOSOLVERS;

  case UF:
    return CTX_ARCH_EG;

  case BV:
    return CTX_ARCH_BV;

  case IDL:
  case LRA:
  case RDL:
  case LIA:
    return CTX_ARCH_SPLX;

  default:
    return -1;
  }
}

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	/*
20	* OBJECT TO STORE CONTEXT CONFIGURATIONS
21	*/
22
23	#include <stdbool.h>
24	#include <assert.h>
25
26	#include "api/context_config.h"
27	#include "utils/memalloc.h"
28	#include "utils/string_utils.h"
29
30
31	/*
32	* Mapping from strings to context modes (cf. string_utils.h)
33	*/
34	static const char * const mode_names[NUM_MODES] = {
35	"interactive",
36	"multi-checks",
37	"one-shot",
38	"push-pop",
39	};
40
41	static const int32_t mode[NUM_MODES] = {
42	CTX_MODE_INTERACTIVE,
43	CTX_MODE_MULTICHECKS,
44	CTX_MODE_ONECHECK,
45	CTX_MODE_PUSHPOP,
46	};
47
48	static const char * const solver_type_names[NUM_SOLVER_TYPES] = {
49	"dpllt",
50	"mcsat"
51	};
52
53	static const int32_t solver_type[NUM_SOLVER_TYPES] = {
54	CTX_SOLVER_TYPE_DPLLT,
55	CTX_SOLVER_TYPE_MCSAT
56	};
57
58	/*
59	* Solver codes
60	*/
61	static const char * const solver_code_names[NUM_SOLVER_CODES] = {
62	"auto",
63	"default",
64	"ifw",
65	"none",
66	"rfw",
67	"simplex",
68	};
69
70	static const int32_t solver_code[NUM_SOLVER_CODES] = {
71	CTX_CONFIG_AUTO,
72	CTX_CONFIG_DEFAULT,
73	CTX_CONFIG_ARITH_IFW,
74	CTX_CONFIG_NONE,
75	CTX_CONFIG_ARITH_RFW,
76	CTX_CONFIG_ARITH_SIMPLEX,
77	};
78
79
80	/*
81	* Descriptor fields (other than "logic")
82	*/
83	typedef enum ctx_config_key {
84	CTX_CONFIG_KEY_MODE,
85	CTX_CONFIG_KEY_SOLVER_TYPE,
86	CTX_CONFIG_KEY_TRACE_TAGS,
87	CTX_CONFIG_KEY_ARITH_FRAGMENT,
88	CTX_CONFIG_KEY_UF_SOLVER,
89	CTX_CONFIG_KEY_ARRAY_SOLVER,
90	CTX_CONFIG_KEY_BV_SOLVER,
91	CTX_CONFIG_KEY_ARITH_SOLVER,
92	CTX_CONFIG_KEY_MODEL_INTERPOLATION,
93	} ctx_config_key_t;
94
95	#define NUM_CONFIG_KEYS (CTX_CONFIG_KEY_MODEL_INTERPOLATION+1)
96
97
98	static const char *const config_key_names[NUM_CONFIG_KEYS] = {
99	"arith-fragment",
100	"arith-solver",
101	"array-solver",
102	"bv-solver",
103	"mode",
104	"model-interpolation",
105	"solver-type",
106	"trace",
107	"uf-solver",
108	};
109
110	static const int32_t config_key[NUM_CONFIG_KEYS] = {
111	CTX_CONFIG_KEY_ARITH_FRAGMENT,
112	CTX_CONFIG_KEY_ARITH_SOLVER,
113	CTX_CONFIG_KEY_ARRAY_SOLVER,
114	CTX_CONFIG_KEY_BV_SOLVER,
115	CTX_CONFIG_KEY_MODE,
116	CTX_CONFIG_KEY_MODEL_INTERPOLATION,
117	CTX_CONFIG_KEY_SOLVER_TYPE,
118	CTX_CONFIG_KEY_TRACE_TAGS,
119	CTX_CONFIG_KEY_UF_SOLVER,
120	};
121
122
123
124
125	/*
126	* CONTEXT SETTING FOR A GIVEN LOGIC CODE
127	*/
128
129	/*
130	* Conversion of SMT logic code to a default architecture code
131	* -1 means not supported
132	*
133	* We don't use AUTO_IDL, AUTO_RDL, IFW or RFW here since
134	* the Floyd-Warshall solvers don't support all use modes.
135	*
136	* IMPORTANT: this array is used by the API in config_for_logic.
137	*/
138	static const int32_t logic2arch[NUM_SMT_LOGICS] = {
139	CTX_ARCH_NOSOLVERS, // NONE
140
141	-1, // AX
142	-1, // BV (supported by EF)
143	-1, // FFA
144	-1, // IDL (supported by EF)
145	-1, // LIA (supported by EF)
146	-1, // LRA (supported by EF)
147	-1, // LIRA
148	-1, // NIA
149	-1, // NRA
150	-1, // NIRA
151	-1, // RDL
152	-1, // UF
153	-1, // ABV
154	-1, // ALIA
155	-1, // ALRA
156	-1, // ALIRA
157	-1, // ANIA
158	-1, // ANRA
159	-1, // ANIRA
160	-1, // AUF
161	-1, // BVLRA
162	-1, // UFBV
163	-1, // UFBVLIA
164	-1, // UFIDL
165	-1, // UFLIA
166	-1, // UFLRA
167	-1, // UFLIRA
168	-1, // UFNIA
169	-1, // UFNRA
170	-1, // UFNIRA
171	-1, // UFRDL
172	-1, // AUFBV
173	-1, // AUFBVLIA
174	-1, // AUFBVNIA
175	-1, // AUFLIA
176	-1, // AUFLRA
177	-1, // AUFLIRA
178	-1, // AUFNIA
179	-1, // AUFNRA
180	-1, // AUFNIRA
181
182	CTX_ARCH_EGFUN, // QF_AX
183	CTX_ARCH_BV, // QF_BV
184	CTX_ARCH_MCSAT, // QF_FFA
185	CTX_ARCH_SPLX, // QF_IDL
186	CTX_ARCH_SPLX, // QF_LIA
187	CTX_ARCH_SPLX, // QF_LRA
188	CTX_ARCH_SPLX, // QF_LIRA
189	CTX_ARCH_MCSAT, // QF_NIA
190	CTX_ARCH_MCSAT, // QF_NRA
191	CTX_ARCH_MCSAT, // QF_NIRA
192	CTX_ARCH_SPLX, // QF_RDL
193	CTX_ARCH_EG, // QF_UF
194	CTX_ARCH_EGFUNBV, // QF_ABV
195	CTX_ARCH_EGFUNSPLX, // QF_ALIA
196	CTX_ARCH_EGFUNSPLX, // QF_ALRA
197	CTX_ARCH_EGFUNSPLX, // QF_ALIRA
198	CTX_ARCH_MCSAT, // QF_ANIA
199	CTX_ARCH_MCSAT, // QF_ANRA
200	CTX_ARCH_MCSAT, // QF_ANIRA
201	CTX_ARCH_EGFUN, // QF_AUF
202	CTX_ARCH_EGSPLXBV, // QF_BVLRA
203	CTX_ARCH_EGBV, // QF_UFBV
204	CTX_ARCH_EGSPLXBV, // QF_UFBVLIA
205
206	CTX_ARCH_EGSPLX, // QF_UFIDL
207	CTX_ARCH_EGSPLX, // QF_UFLIA
208	CTX_ARCH_EGSPLX, // QF_UFLRA
209	CTX_ARCH_EGSPLX, // QF_UFLIRA
210	CTX_ARCH_MCSAT, // QF_UFNIA
211	CTX_ARCH_MCSAT, // QF_UFNRA
212	CTX_ARCH_MCSAT, // QF_UFNIRA
213	CTX_ARCH_EGSPLX, // QF_UFRDL
214	CTX_ARCH_EGFUNBV, // QF_AUFBV
215	CTX_ARCH_EGFUNSPLXBV, // QF_AUFBVLIA
216	CTX_ARCH_MCSAT, // QF_AUFBVNIA
217	CTX_ARCH_EGFUNSPLX, // QF_AUFLIA
218	CTX_ARCH_EGFUNSPLX, // QF_AUFLRA
219	CTX_ARCH_EGFUNSPLX, // QF_AUFLIRA
220	CTX_ARCH_MCSAT, // QF_AUFNIA
221	CTX_ARCH_MCSAT, // QF_AUFNRA
222	CTX_ARCH_MCSAT, // QF_AUFNIRA
223
224	CTX_ARCH_EGFUNSPLXBV, // ALL interpreted as QF_AUFLIRA + QF_BV
225	};
226
227
228
229	/*
230	* WHICH ARITHMETIC FRAGMENTS REQUIRE THE DIOPHANTINE SUBSOLVER
231	*/
232	static const bool fragment2iflag[NUM_ARITH_FRAGMENTS+1] = {
233	false, // IDL
234	false, // RDL
235	true, // LIA
236	false, // LRA
237	true, // LIRA
238	true, // NIA
239	false, // NRA
240	true, // NIRA
241	false, // FFA
242	false, // no arithmetic
243	};
244
245
246	/*
247	* Default configuration:
248	* - enable PUSH/POP
249	* - solver type = DPLL(T)
250	* - no logic specified
251	* - arith fragment = LIRA
252	* - all solvers set to defaults
253	*/
254	static const ctx_config_t default_config = {
255	CTX_MODE_PUSHPOP, // mode
256	CTX_SOLVER_TYPE_DPLLT, // DPLLT solver
257	SMT_UNKNOWN, // logic
258	CTX_CONFIG_DEFAULT, // uf
259	CTX_CONFIG_DEFAULT, // array
260	CTX_CONFIG_DEFAULT, // bv
261	CTX_CONFIG_DEFAULT, // arith
262	ARITH_LIRA, // fragment
263	false, // model interpolation
264	NULL, // trace tags
265	};
266
267
268
269
270
271	/*
272	* DIRECT CONFIGURATION
273	*/
274	int32_t arch_for_logic(smt_logic_t code) {	2,653✔
275	assert(code != SMT_UNKNOWN);
276	return logic2arch[code];	2,653✔
277	}
278
279	bool iflag_for_logic(smt_logic_t code) {	1,446✔
280	assert(code != SMT_UNKNOWN);
281	return fragment2iflag[arith_fragment(code)];	1,446✔
282	}
283
284
285
286	/*
287	* CONFIG OBJECT
288	*/
289
290	/*
291	* Initialize config to the default configuration
292	*/
293	void init_config_to_defaults(ctx_config_t *config) {	×
294	*config = default_config;	×
295	}	×
296
297
298
299	/*
300	* Set a default configuration to support the given logic
301	* - return -1 if the logic name is not recognized
302	* - return -2 if we don't support the logic yet
303	* - return 0 otherwise
304	*
305	* If the function returns 0, the logic field is updated.
306	* All other fields are left unchanged.
307	*/
308	int32_t config_set_logic(ctx_config_t config, const char logic) {	×
309	smt_logic_t code;
310	int32_t r;
311
312	code = smt_logic_code(logic);	×
313	if (code == SMT_UNKNOWN) {	×
314	r = -1;	×
315	} else if (logic2arch[code] < 0) {	×
316	r = -2;	×
317	} else {
318	config->logic = (smt_logic_t) code;	×
319	r = 0;	×
320	}
321
322	return r;	×
323	}
324
325
326	/*
327	* Convert value to a solver
328	*/
329	static int32_t set_solver_code(const char value, solver_code_t dest) {	×
330	int32_t v, r;
331
332	v = parse_as_keyword(value, solver_code_names, solver_code, NUM_SOLVER_CODES);	×
333	if (v < 0) {	×
334	r = -2;	×
335	} else if (v >= CTX_CONFIG_AUTO) {	×
336	r = -3;	×
337	} else {
338	assert(v == CTX_CONFIG_DEFAULT \|\| v == CTX_CONFIG_NONE);
339	*dest = (solver_code_t) v;	×
340	r = 0;	×
341	}
342
343	return r;	×
344	}
345
346
347	/*
348	* Set an individual field in config
349	* - key = field name
350	* - value = value for that field
351	*
352	* Return code:
353	* -1 if the key is not recognized
354	* -2 if the value is not recognized
355	* -3 if the value is not valid for the key
356	* 0 otherwise
357	*/
358	int32_t config_set_field(ctx_config_t config, const char key, const char *value) {	×
359	int32_t k, v, r;
360	arith_fragment_t arith;
361
362	r = 0; // return code	×
363
364	k = parse_as_keyword(key, config_key_names, config_key, NUM_CONFIG_KEYS);	×
365	switch (k) {	×
366	case CTX_CONFIG_KEY_MODE:	×
367	v = parse_as_keyword(value, mode_names, mode, NUM_MODES);	×
368	if (v < 0) {	×
369	r = -2;	×
370	} else {
371	config->mode = v;	×
372	}
373	break;	×
374
375	case CTX_CONFIG_KEY_SOLVER_TYPE:	×
376	v = parse_as_keyword(value, solver_type_names, solver_type, NUM_SOLVER_TYPES);	×
377	if (v < 0) {	×
378	r = -2;	×
379	} else {
380	config->solver_type = v;	×
381	}
382	break;	×
383
384	case CTX_CONFIG_KEY_TRACE_TAGS:	×
385	config->trace_tags = safe_strdup(value);	×
386	break;	×
387
388	case CTX_CONFIG_KEY_ARITH_FRAGMENT:	×
389	arith = arith_fragment_code(value);	×
390	if (arith == ARITH_NONE) {	×
391	r = -2;	×
392	} else {
393	config->arith_fragment = arith;	×
394	}
395	break;	×
396
397	case CTX_CONFIG_KEY_UF_SOLVER:	×
398	r = set_solver_code(value, &config->uf_config);	×
399	break;	×
400
401	case CTX_CONFIG_KEY_ARRAY_SOLVER:	×
402	r = set_solver_code(value, &config->array_config);	×
403	break;	×
404
405	case CTX_CONFIG_KEY_BV_SOLVER:	×
406	r = set_solver_code(value, &config->bv_config);	×
407	break;	×
408
409	case CTX_CONFIG_KEY_ARITH_SOLVER:	×
410	v = parse_as_keyword(value, solver_code_names, solver_code, NUM_SOLVER_CODES);	×
411	if (v < 0) {	×
412	r = -2;	×
413	} else {
414	assert(0 <= v && v <= NUM_SOLVER_CODES);
415	config->arith_config = v;	×
416	}
417	break;	×
418	case CTX_CONFIG_KEY_MODEL_INTERPOLATION:	×
419	v = parse_as_boolean(value, &config->model_interpolation);	×
420	if (v < 0) {	×
421	r = -2;	×
422	}
423	break;	×
424	default:	×
425	assert(k == -1);
426	r = -1;	×
427	break;	×
428	}
429
430	return r;	×
431	}
432
433
434
435	/*
436	* Auxiliary functions to build architecture codes incrementally
437	* - each function takes an integer a: a is either a valid architecture
438	* code or -1
439	* - then the function adds a new solver component to a: this results
440	* in either a new valid code or -1 if the new component is not compatible with a.
441	*
442	* Important: we assume that the components are added in the following
443	* order: egraph, array solver, bitvector solver, arithmetic solver
444	*/
445	static inline int32_t arch_add_egraph(int32_t a) {	×
446	if (a == CTX_ARCH_NOSOLVERS) {	×
447	a = CTX_ARCH_EG;	×
448	} else {
449	a = -1;	×
450	}
451	return a;	×
452	}
453
454	static int32_t arch_add_array(int32_t a) {	×
455	if (a == CTX_ARCH_EG \|\| a == CTX_ARCH_NOSOLVERS) {	×
456	a = CTX_ARCH_EGFUN; // array requires egraph so we add both implicitly	×
457	} else {
458	a = -1;	×
459	}
460	return a;	×
461	}
462
463	static int32_t arch_add_bv(int32_t a) {	×
464	switch (a) {	×
465	case CTX_ARCH_NOSOLVERS:	×
466	a = CTX_ARCH_BV;	×
467	break;	×
468
469	case CTX_ARCH_EG:	×
470	a = CTX_ARCH_EGBV;	×
471	break;	×
472
473	case CTX_ARCH_EGFUN:	×
474	a = CTX_ARCH_EGFUNBV;	×
475	break;	×
476
477	case CTX_ARCH_SPLX:	×
478	a = CTX_ARCH_EGSPLXBV;	×
479	break;	×
480
481	default:	×
482	a = -1;	×
483	break;	×
484	}
485
486	return a;	×
487	}
488
489	// add the simplex solver
490	static int32_t arch_add_simplex(int32_t a) {	×
491	switch (a) {	×
492	case CTX_ARCH_NOSOLVERS:	×
493	a = CTX_ARCH_SPLX;	×
494	break;	×
495
496	case CTX_ARCH_BV:	×
497	a = CTX_ARCH_EGSPLXBV;	×
498	break;	×
499
500	case CTX_ARCH_EG:	×
501	a = CTX_ARCH_EGSPLX;	×
502	break;	×
503
504	case CTX_ARCH_EGFUN:	×
505	a = CTX_ARCH_EGFUNSPLX;	×
506	break;	×
507
508	case CTX_ARCH_EGBV:	×
509	a = CTX_ARCH_EGSPLXBV;	×
510	break;	×
511
512	case CTX_ARCH_EGFUNBV:	×
513	a = CTX_ARCH_EGFUNSPLXBV;	×
514	break;	×
515
516	default:	×
517	a = -1;	×
518	break;	×
519	}
520
521	return a;	×
522	}
523
524	// add a Floyd-Warshall solver
525	static int32_t arch_add_ifw(int32_t a) {	×
526	if (a == CTX_ARCH_NOSOLVERS) {	×
527	a = CTX_ARCH_IFW;	×
528	} else {
529	a = -1;	×
530	}
531	return a;	×
532	}
533
534	static int32_t arch_add_rfw(int32_t a) {	×
535	if (a == CTX_ARCH_NOSOLVERS) {	×
536	a = CTX_ARCH_RFW;	×
537	} else {
538	a = -1;	×
539	}
540	return a;	×
541	}
542
543
544	// add solver identified by code c to a
545	static int32_t arch_add_arith(int32_t a, solver_code_t c) {	×
546	switch (c) {	×
547	case CTX_CONFIG_NONE: // no arithmetic solver	×
548	break;	×
549
550	case CTX_CONFIG_DEFAULT: // simplex is the default	×
551	case CTX_CONFIG_AUTO: // auto = simplex here too
552	case CTX_CONFIG_ARITH_SIMPLEX:
553	a = arch_add_simplex(a);	×
554	break;	×
555
556	case CTX_CONFIG_ARITH_IFW:	×
557	a = arch_add_ifw(a);	×
558	break;	×
559
560	case CTX_CONFIG_ARITH_RFW:	×
561	a = arch_add_rfw(a);	×
562	break;	×
563	}
564	return a;	×
565	}
566
567
568	/*
569	* Check whether the architecture code a is compatible with mode
570	* - current restriction: IFW and RFW don't support PUSH/POP or MULTIPLE CHECKS
571	*/
572	static bool arch_supports_mode(context_arch_t a, context_mode_t mode) {	×
573	return (a != CTX_ARCH_IFW && a != CTX_ARCH_RFW) \|\| mode == CTX_MODE_ONECHECK;	×
574	}
575
576
577	/*
578	* Check whether the architecture is supported.
579	*/
580	static bool arch_is_supported(context_arch_t a) {	×
581	#if HAVE_MCSAT
582	return true; // all architectures are supported
583	#else
584	return a != CTX_ARCH_MCSAT;	×
585	#endif
586	}
587
588
589	/*
590	* Check whether config is valid (and supported by this version of Yices)
591	* and convert it to a tuple (arch, mode, iflag, qflag)
592	* - arch = architecture code as defined in context.h
593	* - mode = one of the context's modes
594	* - iflag = true if the integer solver (in simplex) is required
595	* - qflag = true if support for quantifiers is required
596	*
597	* Return code:
598	* 0 if the config is valid and supported
599	* -1 if the config is invalid
600	* -2 if the config is valid but not currently supported
601	* -3 if the solver combination is valid but does not support the specified mode
602	*/
603	int32_t decode_config(const ctx_config_t config, smt_logic_t logic, context_arch_t arch, context_mode_t mode, bool iflag, bool qflag) {	×
604	smt_logic_t logic_code;
605	int32_t a, r;
606
607	r = 0; // default return code	×
608
609	logic_code = config->logic;	×
610	if (logic_code != SMT_UNKNOWN) {	×
611	/*
612	* The intended logic is specified
613	*/
614	assert(0 <= logic_code && logic_code < NUM_SMT_LOGICS);
615
616	/*
617	* Special case: difference logic + mode = ONECHECK + arith_config == AUTO
618	*/
619	if (config->arith_config == CTX_CONFIG_AUTO && config->mode == CTX_MODE_ONECHECK) {	×
620	if (logic_code == QF_IDL) {	×
621	*logic = QF_IDL;	×
622	*arch = CTX_ARCH_AUTO_IDL;	×
623	*mode = CTX_MODE_ONECHECK;	×
624	*iflag = false;	×
625	*qflag = false;	×
626	goto done;	×
627	}
628
629	if (logic_code == QF_RDL) {	×
630	*logic = QF_RDL;	×
631	*arch = CTX_ARCH_AUTO_RDL;	×
632	*mode = CTX_MODE_ONECHECK;	×
633	*iflag = false;	×
634	*qflag = false;	×
635	goto done;	×
636	}
637	}
638
639	a = logic2arch[logic_code];	×
640	if (a < 0 \|\| !arch_is_supported(a)) {	×
641	// not supported
642	r = -2;	×
643	} else {
644	// good configuration
645	*logic = logic_code;	×
646	*arch = (context_arch_t) a;	×
647	*iflag = iflag_for_logic(logic_code);	×
648	*qflag = qflag_for_logic(logic_code);	×
649	*mode = config->mode;	×
650	}
651
652	} else if (config->solver_type == CTX_SOLVER_TYPE_MCSAT) {	×
653	if (arch_is_supported(CTX_ARCH_MCSAT)) {	×
654	/*
655	* MCSAT solver/no logic specified
656	*/
657	*logic = SMT_UNKNOWN;	×
658	*arch = CTX_ARCH_MCSAT;	×
659	*mode = CTX_MODE_PUSHPOP;	×
660	*iflag = false;	×
661	*qflag = false;	×
662	} else {
663	// not compiled with MCSAT support so this is not supported
664	r = -2;	×
665	}
666
667	} else {
668	/*
669	* No logic specified.
670	*/
671
672	a = CTX_ARCH_NOSOLVERS;	×
673	if (config->uf_config == CTX_CONFIG_DEFAULT) {	×
674	a = arch_add_egraph(a);	×
675	}
676	if (config->array_config == CTX_CONFIG_DEFAULT) {	×
677	a = arch_add_array(a);	×
678	}
679	if (config->bv_config == CTX_CONFIG_DEFAULT) {	×
680	a = arch_add_bv(a);	×
681	}
682	a = arch_add_arith(a, config->arith_config);	×
683
684	// a is either -1 or an architecture code
685	if (a < 0) {	×
686	r = -1; // invalid combination of solvers	×
687	} else if (arch_supports_mode(a, config->mode)) {	×
688	// good configuration
689	*logic = SMT_UNKNOWN;	×
690	*arch = (context_arch_t) a;	×
691	*iflag = fragment2iflag[config->arith_fragment];	×
692	*qflag = false;	×
693	*mode = config->mode;	×
694	} else {
695	// mode is not supported by the solvers
696	r = -3;	×
697	}
698	}
699
700	done:	×
701	return r;	×
702	}
703
704
705	/*
706	* Cleanup a configutation descriptor
707	*/
708	void delete_config(ctx_config_t *config) {	×
709	safe_free(config->trace_tags);	×
710	}	×
711
712
713	/*
714	* Check whether a logic is supported by the MCSAT solver
715	*/
716	bool logic_is_supported_by_mcsat(smt_logic_t code) {	×
717	return code == SMT_ALL \|\| !logic_has_quantifiers(code);	×
718	}
719
720	/*
721	* Check whether a logic requires the MCSAT solver
722	*/
723	bool logic_requires_mcsat(smt_logic_t code) {	931✔
724	return arch_for_logic(code) == CTX_ARCH_MCSAT;	931✔
725	}
726
727	/*
728	* Check whether a logic is supported by the exists/forall solver
729	* - logics with quantifiers and BV or linear arithmetic are supported
730	* - logic "NONE" == purely Boolean is supported too
731	*/
732	bool logic_is_supported_by_ef(smt_logic_t code) {	931✔
733	return code == NONE \|\| code == BV \|\| code == IDL \|\| code == LRA \|\| code == RDL \|\| code == LIA \|\| code == UF;	931✔
734	}
735
736
737	/*
738	* Context architecture for a logic supported by EF
739	*/
740	int32_t ef_arch_for_logic(smt_logic_t code) {	692✔
741	switch (code) {	692✔
742	case NONE:	×
743	return CTX_ARCH_NOSOLVERS;	×
744
745	case UF:	114✔
746	return CTX_ARCH_EG;	114✔
747
748	case BV:	24✔
749	return CTX_ARCH_BV;	24✔
750
751	case IDL:	554✔
752	case LRA:
753	case RDL:
754	case LIA:
755	return CTX_ARCH_SPLX;	554✔
756
757	default:	×
758	return -1;	×
759	}
760	}

SRI-CSL / yices2 / 16032530443

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