diff --git a/Makefile.build b/Makefile.build index 08c3629db..193aed0fe 100644 --- a/Makefile.build +++ b/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 \ diff --git a/src/Makefile b/src/Makefile index 9a14fc6ba..4e69dcea9 100644 --- a/src/Makefile +++ b/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 \ # diff --git a/src/api/context_config.c b/src/api/context_config.c index adaccc4a2..f9bfe0ae6 100644 --- a/src/api/context_config.c +++ b/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 diff --git a/src/api/yices_api.c b/src/api/yices_api.c index faed13510..ff4f915c1 100644 --- a/src/api/yices_api.c +++ b/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); diff --git a/src/context/context.c b/src/context/context.c index 7b7ec2d20..f4c08b1d0 100644 --- a/src/context/context.c +++ b/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); } diff --git a/src/context/context_solver.c b/src/context/context_solver.c index 32288b506..17ce6f0da 100644 --- a/src/context/context_solver.c +++ b/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); } diff --git a/src/context/context_types.h b/src/context/context_types.h index b1e5775ea..5b130b8b1 100644 --- a/src/context/context_types.h +++ b/src/context/context_types.h @@ -54,6 +54,10 @@ #include "mcsat/solver.h" +#ifdef HAVE_MCSAT +#include +#endif + /*********************** * OPTIONAL FEATURES * **********************/ @@ -190,11 +194,12 @@ typedef enum { CTX_ARCH_AUTO_IDL, // either simplex or integer floyd-warshall CTX_ARCH_AUTO_RDL, // either simplex or real floyd-warshall - CTX_ARCH_MCSAT // mcsat solver + CTX_ARCH_MCSAT, // mcsat solver + CTX_ARCH_MCSATARITH, // use mcsat just for arithmetic } context_arch_t; -#define NUM_ARCH (CTX_ARCH_MCSAT+1) +#define NUM_ARCH (CTX_ARCH_MCSATARITH+1) /* @@ -247,7 +252,20 @@ enum { }; +/** + * Tag for representing a value returned by arithmetic solver. + */ +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 + */ +typedef struct arithval_in_model_s arithval_in_model_t; /************************** * ARITHMETIC INTERFACE * @@ -381,7 +399,7 @@ enum { * 21) bool arith_var_is_int(void *solver, thvar_t x): * - return true if x is an integer variable, false otherwise. * - * + * * Exception mechanism * ------------------- * When the solver is created and initialized it's given a pointer b to a jmp_buf internal to @@ -401,6 +419,7 @@ typedef thvar_t (*create_arith_var_fun_t)(void *solver, bool is_int); typedef thvar_t (*create_arith_const_fun_t)(void *solver, rational_t *q); typedef thvar_t (*create_arith_poly_fun_t)(void *solver, polynomial_t *p, thvar_t *map); typedef thvar_t (*create_arith_pprod_fun_t)(void *solver, pprod_t *p, thvar_t *map); +typedef thvar_t (*create_arith_rdiv_fun_t)(void* solver, thvar_t num, thvar_t den); typedef literal_t (*create_arith_atom_fun_t)(void *solver, thvar_t x); typedef literal_t (*create_arith_patom_fun_t)(void *solver, polynomial_t *p, thvar_t *map); @@ -417,7 +436,7 @@ typedef eterm_t (*eterm_of_var_fun_t)(void *solver, thvar_t v); typedef void (*build_model_fun_t)(void *solver); typedef void (*free_model_fun_t)(void *solver); -typedef bool (*arith_val_in_model_fun_t)(void *solver, thvar_t x, rational_t *v); +typedef bool (*arith_val_in_model_fun_t)(void *solver, thvar_t x, arithval_in_model_t* v); typedef bool (*arith_var_is_int_fun_t)(void *solver, thvar_t x); @@ -426,6 +445,7 @@ typedef struct arith_interface_s { create_arith_const_fun_t create_const; create_arith_poly_fun_t create_poly; create_arith_pprod_fun_t create_pprod; + create_arith_rdiv_fun_t create_rdiv; create_arith_atom_fun_t create_eq_atom; create_arith_atom_fun_t create_ge_atom; @@ -631,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; @@ -716,7 +746,9 @@ struct context_s { bvpoly_buffer_t *bvpoly_buffer; // auxiliary buffers for model construction - rational_t aux; +// rational_t aux; + arithval_in_model_t aval; + bvconstant_t bv_buffer; // for exception handling @@ -759,7 +791,7 @@ enum { TYPE_ERROR = -2, // general errors FREE_VARIABLE_IN_FORMULA = -3, - LOGIC_NOT_SUPPORTED = -4, + LOGIC_NOT_SUPPORTED = -4, UF_NOT_SUPPORTED = -5, SCALAR_NOT_SUPPORTED = -6, TUPLE_NOT_SUPPORTED = -7, diff --git a/src/frontend/smt2/smt2_commands.c b/src/frontend/smt2/smt2_commands.c index af6483f4f..1af25123e 100644 --- a/src/frontend/smt2/smt2_commands.c +++ b/src/frontend/smt2/smt2_commands.c @@ -76,6 +76,7 @@ #include "mt/threads.h" #include "mt/thread_macros.h" +#define FORCE_MCSAT_ARITH /* * DUMP CONTEXT: FOR TESTING/DEBUGGING @@ -2587,6 +2588,9 @@ static void init_smt2_context(smt2_globals_t *g) { iflag = iflag_for_logic(logic); qflag = qflag_for_logic(logic); +#ifdef FORCE_MCSAT_ARITH + arch = CTX_ARCH_MCSATARITH; +#else if (g->mcsat) { // force MCSAT independent of the logic arch = CTX_ARCH_MCSAT; @@ -2606,6 +2610,7 @@ static void init_smt2_context(smt2_globals_t *g) { break; } } +#endif if (arch == CTX_ARCH_MCSAT) { iflag = false; diff --git a/src/frontend/yices_smt2_lc.c b/src/frontend/yices_smt2_lc.c new file mode 100644 index 000000000..47f95f7c6 --- /dev/null +++ b/src/frontend/yices_smt2_lc.c @@ -0,0 +1,1128 @@ +/* + * 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 . + */ + +/* + * Yices solver: input in the SMT-LIB 2.0 language + */ + +#if defined(CYGWIN) || defined(MINGW) +#ifndef __YICES_DLLSPEC__ +#define __YICES_DLLSPEC__ __declspec(dllexport) +#endif +#endif + +#include +#include +#include +#include +#include +#include +#include + +#if defined(MINGW) +/* + * We call isatty(STDIN_FILENO) to check whether stdin is a terminal. + * + * On Windows/MINGW, isatty is called _isatty. The macro STDIN_FILENO + * appears to be defined in mingw/include/stdio.h. Not clear whether + * it exists in Windows? There is a function isatty declared in io.h, + * but it is deprecated. + * + * NOTE: the windows function _isatty doesn't have the same behavior + * as isatty on Unix. It returns a non-zero value if the file + * descriptor is associated with a character device (which is true of + * terminals but of other files too). + */ +#include +#ifndef STDIN_FILENO +#define STDIN_FILENO (_fileno(stdin)) +#endif +#define isatty _isatty + +#else +// Should work on all Unix variants +#include +#endif + +#include "frontend/common/parameters.h" +#include "frontend/smt2/smt2_commands.h" +#include "frontend/smt2/smt2_lexer.h" +#include "frontend/smt2/smt2_parser.h" +#include "frontend/smt2/smt2_term_stack.h" +#include "io/simple_printf.h" +#include "solvers/cdcl/delegate.h" +#include "utils/command_line.h" +#include "solvers/quant/quant_parameters.h" + +#include "yices.h" +#include "yices_exit_codes.h" + +/* + * yices_rev is set up at compile time in yices_version.c + */ +extern const char * const yices_rev; + +/* + * Global objects: + * - lexer/parser/stack: for processing the SMT2 input + * - incremental: if this flag is true, support for push/pop + * and multiple check_sat is enabled. Otherwise, the solver + * is configured to handle a set of declarations/assertions + * followed by a single call to (check_sat). + * - interactive: set option :print-success to true. + * and print a prompt before parsing commands if stdin is a terminal. + * - timeout: command-line option + * + * - filename = name of the input file (NULL means read stdin) + */ +static lexer_t lexer; +static parser_t parser; +static tstack_t stack; + +static bool incremental; +static bool interactive; +static bool smt2_model_format; +static bool bvdecimal; +static bool show_stats; +static int32_t verbosity; +static uint32_t timeout; +static char *filename; +static char *delegate; +static char *dimacsfile; + +// mcsat options +static bool mcsat; +static bool mcsat_nra_mgcd; +static bool mcsat_nra_nlsat; +static bool mcsat_nra_bound; +static int32_t mcsat_nra_bound_min; +static int32_t mcsat_nra_bound_max; +static int32_t mcsat_bv_var_size; + +static pvector_t trace_tags; + +// ef solver options +static bool ef_en_ematch; +static int32_t ef_mbqi_max_iter; +static int32_t ef_mbqi_max_lemma_per_round; + +static int32_t ef_ematch_inst_per_round; +static int32_t ef_ematch_inst_per_search; +static int32_t ef_ematch_inst_total; +static int32_t ef_ematch_rounds_per_search; +static int32_t ef_ematch_search_total; + +static int32_t ef_ematch_trial_fdepth; +static int32_t ef_ematch_trial_vdepth; +static int32_t ef_ematch_trial_fapps; +static int32_t ef_ematch_trial_matches; + +static int32_t ef_ematch_cnstr_epsilon; +static double ef_ematch_cnstr_alpha; +static int32_t ef_ematch_term_epsilon; +static double ef_ematch_term_alpha; + +static int32_t ef_ematch_cnstr_mode; +static int32_t ef_ematch_term_mode; + + +/**************************** + * COMMAND-LINE ARGUMENTS * + ***************************/ + +typedef enum optid { + show_version_opt, // print version and exit + show_help_opt, // print help and exit + show_mcsat_help_opt, // print help about the mcsat options + show_stats_opt, // show statistics after all commands are processed + verbosity_opt, // set verbosity on the command line + incremental_opt, // enable incremental mode + interactive_opt, // enable interactive mode + smt2format_opt, // use SMT-LIB2 format for models + bvdecimal_opt, // use (_ bv n) for bit-vector constants + timeout_opt, // give a timeout + delegate_opt, // use an external sat solver + dimacs_opt, // bitblast then export to DIMACS + mcsat_opt, // enable mcsat + mcsat_nra_mgcd_opt, // use the mgcd instead psc in projection + mcsat_nra_nlsat_opt, // use the nlsat projection instead of brown single-cell + mcsat_nra_bound_opt, // search by increasing bound + mcsat_nra_bound_min_opt, // set initial bound + mcsat_nra_bound_max_opt, // set maximal bound + mcsat_bv_var_size_opt, // set size of bitvector variables + trace_opt, // enable a trace tag + show_ef_help_opt, // print help about the ef options + ematch_en_opt, // enable ematching + mbqi_max_iter_opt, // set max mbqi iterations + mbqi_lemmas_per_round_opt, // set max mbqi lemmas per round + ematch_inst_per_round_opt, // set max ematch instances per round + ematch_inst_per_search_opt, // set max ematch instances per search + ematch_inst_total_opt, // set max ematch instances + ematch_rounds_per_search_opt, // set max ematch rounds per search + ematch_search_total_opt, // set max ematch rounds per search + ematch_trial_fdepth_opt, // set max function depth in each ematch trial + ematch_trial_vdepth_opt, // set max variable depth in each ematch trial + ematch_trial_fapps_opt, // set max function apps in each ematch trial + ematch_trial_matches_opt, // set max matches in each ematch trial + ematch_cnstr_epsilon_opt, // set ematch constraint learner epsilon + ematch_cnstr_alpha_opt, // set ematch constraint learner learning rate + ematch_term_epsilon_opt, // set ematch term learner epsilon + ematch_term_alpha_opt, // set ematch term learner learning rate + ematch_cnstr_mode_opt, // set cnstr mode in ematching + ematch_term_mode_opt, // set term mode in ematching +} optid_t; + +#define NUM_OPTIONS (ematch_term_mode_opt+1) + +/* + * Option descriptors + */ +static option_desc_t options[NUM_OPTIONS] = { + { "version", 'V', FLAG_OPTION, show_version_opt }, + { "help", 'h', FLAG_OPTION, show_help_opt }, + { "mcsat-help", '0', FLAG_OPTION, show_mcsat_help_opt }, + { "stats", 's', FLAG_OPTION, show_stats_opt }, + { "verbosity", 'v', MANDATORY_INT, verbosity_opt }, + { "timeout", 't', MANDATORY_INT, timeout_opt }, + { "incremental", '\0', FLAG_OPTION, incremental_opt }, + { "interactive", '\0', FLAG_OPTION, interactive_opt }, + { "smt2-model-format", '\0', FLAG_OPTION, smt2format_opt }, + { "bvconst-in-decimal", '\0', FLAG_OPTION, bvdecimal_opt }, + { "delegate", '\0', MANDATORY_STRING, delegate_opt }, + { "dimacs", '\0', MANDATORY_STRING, dimacs_opt }, + { "mcsat", '\0', FLAG_OPTION, mcsat_opt }, + { "mcsat-nra-mgcd", '\0', FLAG_OPTION, mcsat_nra_mgcd_opt }, + { "mcsat-nra-nlsat", '\0', FLAG_OPTION, mcsat_nra_nlsat_opt }, + { "mcsat-nra-bound", '\0', FLAG_OPTION, mcsat_nra_bound_opt }, + { "mcsat-nra-bound-min", '\0', MANDATORY_INT, mcsat_nra_bound_min_opt }, + { "mcsat-nra-bound-max", '\0', MANDATORY_INT, mcsat_nra_bound_max_opt }, + { "mcsat-bv-var-size", '\0', MANDATORY_INT, mcsat_bv_var_size_opt }, + { "trace", 't', MANDATORY_STRING, trace_opt }, + { "ef-help", '0', FLAG_OPTION, show_ef_help_opt }, + { "ematch", '\0', FLAG_OPTION, ematch_en_opt }, + { "mbqi-max-iter", '\0', MANDATORY_INT, mbqi_max_iter_opt }, + { "mbqi-lemmas-per-round", '\0', MANDATORY_INT, mbqi_lemmas_per_round_opt }, + { "ematch-inst-per-round", '\0', MANDATORY_INT, ematch_inst_per_round_opt }, + { "ematch-inst-per-search", '\0', MANDATORY_INT, ematch_inst_per_search_opt }, + { "ematch-inst-total", '\0', MANDATORY_INT, ematch_inst_total_opt }, + { "ematch-rounds-per-search", '\0', MANDATORY_INT, ematch_rounds_per_search_opt }, + { "ematch-search-total", '\0', MANDATORY_INT, ematch_search_total_opt }, + { "ematch-trial-fdepth", '\0', MANDATORY_INT, ematch_trial_fdepth_opt }, + { "ematch-trial-vdepth", '\0', MANDATORY_INT, ematch_trial_vdepth_opt }, + { "ematch-trial-fapps", '\0', MANDATORY_INT, ematch_trial_fapps_opt }, + { "ematch-trial-matches", '\0', MANDATORY_INT, ematch_trial_matches_opt }, + { "ematch-cnstr-epsilon", '\0', MANDATORY_INT, ematch_cnstr_epsilon_opt }, + { "ematch-cnstr-alpha", '\0', MANDATORY_FLOAT, ematch_cnstr_alpha_opt }, + { "ematch-term-epsilon", '\0', MANDATORY_INT, ematch_term_epsilon_opt }, + { "ematch-term-alpha", '\0', MANDATORY_FLOAT, ematch_term_alpha_opt }, + { "ematch-cnstr-mode", '\0', MANDATORY_STRING, ematch_cnstr_mode_opt }, + { "ematch-term-mode", '\0', MANDATORY_STRING, ematch_term_mode_opt }, +}; + + +/* + * Processing of command-line + */ +static void print_version(void) { + printf("Yices %s\n" + "Copyright SRI International.\n" + "Linked with GMP %s\n" + "Copyright Free Software Foundation, Inc.\n" + "Build date: %s\n" + "Platform: %s (%s)\n" + "Revision: %s\n", + yices_version, gmp_version, + yices_build_date, yices_build_arch, yices_build_mode, yices_rev); + fflush(stdout); +} + +static void print_help(const char *progname) { + printf("Usage: %s [option] filename\n" + " or %s [option]\n\n", progname, progname); + printf("Option summary:\n" + " --version, -V Show version and exit\n" + " --help, -h Print this message and exit\n" + " --verbosity= Set verbosity level (default = 0)\n" + " -v \n" + " --timeout= Set a timeout in seconds (default = no timeout)\n" + " -t \n" + " --stats, -s Print statistics once all commands have been processed\n" + " --incremental Enable support for push/pop\n" + " --interactive Run in interactive mode (ignored if a filename is given)\n" + " --smt2-model-format Display models in the SMT-LIB 2 format (default = false)\n" + " --bvconst-in-decimal Display bit-vector constants as decimal numbers (default = false)\n" + " --delegate= Use an external SAT solver (can be cadical, cryptominisat, kissat, or y2sat)\n" + " --dimacs= Bitblast and export to a file (in DIMACS format)\n" + " --mcsat Use the MCSat solver\n" + " --mcsat-help Show the MCSat options\n" + " --ef-help Show the EF options\n" + "\n" + "For bug reports and other information, please see http://yices.csl.sri.com/\n"); + fflush(stdout); +} + +static void print_mcsat_help(const char *progname) { + printf("Usage: %s [option] filename\n" + " or %s [option]\n\n", progname, progname); + printf("MCSat options:\n" + " --mcsat-nra-mgcd Use model-based GCD instead of PSC for projection\n" + " --mcsat-nra-nlsat Use NLSAT projection instead of Brown's single-cell construction\n" + " --mcsat-nra-bound Search by increasing the bound on variable magnitude\n" + " --mcsat-nra-bound-min= Set initial lower bound\n" + " --mcsat-nra-bound-max= Set maximal bound for search\n" + " --mcsat-bv-var-size= Set size of bit-vector variables in MCSAT search" + "\n"); + fflush(stdout); +} + +static void print_ef_help(const char *progname) { + printf("Usage: %s [option] filename\n" + " or %s [option]\n\n", progname, progname); + printf("EF options:\n"); + printf(" --ematch Toggle enabling/disabling ematching (default: %s)\n", (DEF_EMATCH_EN?"true":"false")); + printf(" --ematch-cnstr-mode= Set the ematching constraint mode (can be epsilongreedy, random, all) (default: epsilongreedy)\n"); + printf(" --ematch-term-mode= Set the ematching term mode (can be epsilongreedy, random, all) (default: epsilongreedy)\n"); + printf("\n"); + printf(" Learner options\n"); + printf(" --ematch-cnstr-epsilon= Set the minimum epsilon for ematch constraint learner (between 0-%d) (default: %d)\n", CNSTR_RL_EPSILON_MAX, CNSTR_RL_EPSILON_MIN); + printf(" --ematch-cnstr-alpha= Set the learning rate for ematch constraint learner (between 0-1) (default: %.2f)\n", CNSTR_RL_ALPHA_DEFAULT); + printf(" --ematch-term-epsilon= Set the minimum epsilon for ematch term learner (between 0-%d) (default: %d)\n", TERM_RL_EPSILON_MAX, TERM_RL_EPSILON_MIN); + printf(" --ematch-term-alpha= Set the learning rate for ematch term learner (between 0-1) (default: %.2f)\n", TERM_RL_ALPHA_DEFAULT); + printf("\n"); + printf(" Fine-grained options\n"); + printf(" (mbqi)\n"); + printf(" --mbqi-max-iter= Set the max number of mbqi iterations (default: %d)\n", DEF_MBQI_MAX_ITERS); + printf(" --mbqi-lemmas-per-round= Set the max number of lemmas per mbqi round (default: %d)\n", DEF_MBQI_MAX_LEMMAS_PER_ROUND); + printf(" (ematch)\n"); + printf(" --ematch-inst-per-round= Set the max number of instances per ematch round (default: %d)\n", DEFAULT_MAX_INSTANCES_PER_ROUND); + printf(" --ematch-inst-per-search= Set the max number of instances per ematch seach (default: %d)\n", DEFAULT_MAX_INSTANCES_PER_SEARCH); + printf(" --ematch-inst-total= Set the max number of ematch instances total (default: %d)\n", DEFAULT_MAX_INSTANCES); + printf(" --ematch-rounds-per-search= Set the max number of rounds per ematch seach (default: %d)\n", DEFAULT_MAX_ROUNDS_PER_SEARCH); + printf(" --ematch-search-total= Set the max number of ematch searches total (default: %d)\n", DEFAULT_MAX_SEARCH); + printf(" (ematch trial)\n"); + printf(" --ematch-trial-matches= Set the max matches allowed in each ematch trial (default: %d)\n", DEF_MAX_MATCHES); + printf(" --ematch-trial-fapps= Set the max function apps considered in each ematch trial (default: %d)\n", DEF_MAX_FAPPS); + printf(" --ematch-trial-fdepth= Set the max function depth allowed in each fapp considered during ematch trial (default: %d)\n", DEF_MAX_FDEPTH); + printf(" --ematch-trial-vdepth= Set the max function depth allowed in each match considered during ematch trial (default: %d)\n", DEF_MAX_VDEPTH); + fflush(stdout); +} + +/* + * Message for unrecognized options or other errors on the command line. + */ +static void print_usage(const char *progname) { + fprintf(stderr, "Usage: %s [options] filename\n", progname); + fprintf(stderr, "Try '%s --help' for more information\n", progname); +} + +/* + * Utility: make a copy of string s + * - we limit the copy to MAX_STRING_COPY_LEN characters + * - return NULL if that fails + * + * 16000 bytes should be more than enough in practice for a filename. + * For example on Linux/ext4 filesystem: PATH_MAX=4096 bytes. + * We produce an error if somebody tries a name longer than that. + */ +#define MAX_STRING_COPY_LEN 16000 + +static char *copy_string(const char *s) { + size_t len; + char *c; + + c = NULL; + len = strlen(s); + if (len <= MAX_STRING_COPY_LEN) { + c = (char *) safe_malloc(len + 1); + strcpy(c, s); + } + return c; +} + + +/* + * Parse the command line and process options + */ +static void parse_command_line(int argc, char *argv[]) { + cmdline_parser_t parser; + cmdline_elem_t elem; + optid_t k; + int32_t v; + int code; + bool unknown_delegate; + + filename = NULL; + incremental = false; + interactive = false; + smt2_model_format = false; + bvdecimal = false; + show_stats = false; + verbosity = 0; + timeout = 0; + delegate = NULL; + dimacsfile = NULL; + + mcsat = false; + mcsat_nra_mgcd = false; + mcsat_nra_nlsat = false; + mcsat_nra_bound = false; + mcsat_nra_bound_min = -1; + mcsat_nra_bound_max = -1; + mcsat_bv_var_size = -1; + + init_pvector(&trace_tags, 5); + + ef_en_ematch = DEF_EMATCH_EN; + ef_mbqi_max_iter = -1; + ef_mbqi_max_lemma_per_round = -1; + ef_ematch_inst_per_round = -1; + ef_ematch_inst_per_search = -1; + ef_ematch_inst_total = -1; + ef_ematch_rounds_per_search = -1; + ef_ematch_search_total = -1; + ef_ematch_trial_fdepth = -1; + ef_ematch_trial_vdepth = -1; + ef_ematch_trial_fapps = -1; + ef_ematch_trial_matches = -1; + ef_ematch_cnstr_epsilon = -1; + ef_ematch_cnstr_alpha = -1; + ef_ematch_term_epsilon = -1; + ef_ematch_term_alpha = -1; + ef_ematch_cnstr_mode = -1; + ef_ematch_term_mode = -1; + + init_cmdline_parser(&parser, options, NUM_OPTIONS, argv, argc); + + for (;;) { + cmdline_parse_element(&parser, &elem); + switch (elem.status) { + case cmdline_done: + goto done; + + case cmdline_argument: + if (filename == NULL) { + filename = elem.arg; + } else { + fprintf(stderr, "%s: too many arguments\n", parser.command_name); + goto bad_usage; + } + break; + + case cmdline_option: + k = elem.key; + switch (k) { + case show_version_opt: + print_version(); + code = YICES_EXIT_SUCCESS; + goto exit; + + case show_help_opt: + print_help(parser.command_name); + code = YICES_EXIT_SUCCESS; + goto exit; + + case show_mcsat_help_opt: + print_mcsat_help(parser.command_name); + code = YICES_EXIT_SUCCESS; + goto exit; + + case show_stats_opt: + show_stats = true; + break; + + case verbosity_opt: + v = elem.i_value; + if (v < 0) { + fprintf(stderr, "%s: the verbosity level must be non-negative\n", parser.command_name); + goto bad_usage; + } + verbosity = v; + break; + + case timeout_opt: + v = elem.i_value; + if (v < 0) { + fprintf(stderr, "%s: the timeout must be non-negative\n", parser.command_name); + goto bad_usage; + } + timeout = v; + break; + + case incremental_opt: + incremental = true; + break; + + case interactive_opt: + interactive = true; + break; + + case delegate_opt: + if (delegate == NULL) { + unknown_delegate = true; + if (supported_delegate(elem.s_value, &unknown_delegate)) { + delegate = copy_string(elem.s_value); + } else if (unknown_delegate) { + fprintf(stderr, "%s: unknown delegate: %s (choices are 'y2sat' or 'cadical' or 'kissat' or 'cryptominisat')\n", + parser.command_name, elem.s_value); + goto bad_usage; + } else { + fprintf(stderr, "%s: unsupported delegate: this version was not compiled to support %s\n", parser.command_name, elem.s_value); + goto bad_usage; + } + } else if (strcmp(elem.s_value, delegate) != 0) { + fprintf(stderr, "%s: can't have several delegates\n", parser.command_name); + goto bad_usage; + } + break; + + case dimacs_opt: + if (dimacsfile == NULL) { + dimacsfile = copy_string(elem.s_value); + if (dimacsfile == NULL) { + // copy_string failed + fprintf(stderr, "%s: file-name %s is too long\n", parser.command_name, elem.s_value); + code = YICES_EXIT_USAGE; + goto exit; + } + } else { + fprintf(stderr, "%s: can't give more than one dimacs file\n", parser.command_name); + goto bad_usage; + } + break; + + case smt2format_opt: + smt2_model_format = true; + break; + + case bvdecimal_opt: + bvdecimal = true; + break; + + case mcsat_opt: + if (! yices_has_mcsat()) goto no_mcsat; + mcsat = true; + break; + + case mcsat_nra_mgcd_opt: + if (! yices_has_mcsat()) goto no_mcsat; + mcsat_nra_mgcd = true; + break; + + case mcsat_nra_nlsat_opt: + if (! yices_has_mcsat()) goto no_mcsat; + mcsat_nra_nlsat = true; + break; + + case mcsat_nra_bound_opt: + if (! yices_has_mcsat()) goto no_mcsat; + mcsat_nra_bound = true; + break; + + case mcsat_nra_bound_min_opt: + if (! yices_has_mcsat()) goto no_mcsat; + if (! validate_integer_option(&parser, &elem, 0, INT32_MAX)) goto bad_usage; + mcsat_nra_bound_min = elem.i_value; + break; + + case mcsat_nra_bound_max_opt: + if (! yices_has_mcsat()) goto no_mcsat; + if (! validate_integer_option(&parser, &elem, 0, INT32_MAX)) goto bad_usage; + mcsat_nra_bound_max = elem.i_value; + break; + + case mcsat_bv_var_size_opt: + if (! yices_has_mcsat()) goto no_mcsat; + if (! validate_integer_option(&parser, &elem, 0, INT32_MAX)) goto bad_usage; + mcsat_bv_var_size = elem.i_value; + break; + + case show_ef_help_opt: + print_ef_help(parser.command_name); + code = YICES_EXIT_SUCCESS; + goto exit; + + case ematch_en_opt: + ef_en_ematch = !ef_en_ematch; + break; + + case mbqi_max_iter_opt: + if (! validate_integer_option(&parser, &elem, 0, INT32_MAX)) goto bad_usage; + ef_mbqi_max_iter = elem.i_value; + break; + + case mbqi_lemmas_per_round_opt: + if (! validate_integer_option(&parser, &elem, 0, INT32_MAX)) goto bad_usage; + ef_mbqi_max_lemma_per_round = elem.i_value; + break; + + case ematch_inst_per_round_opt: + if (! validate_integer_option(&parser, &elem, 0, INT32_MAX)) goto bad_usage; + ef_ematch_inst_per_round = elem.i_value; + break; + + case ematch_inst_per_search_opt: + if (! validate_integer_option(&parser, &elem, 0, INT32_MAX)) goto bad_usage; + ef_ematch_inst_per_search = elem.i_value; + break; + + case ematch_inst_total_opt: + if (! validate_integer_option(&parser, &elem, 0, INT32_MAX)) goto bad_usage; + ef_ematch_inst_total = elem.i_value; + break; + + case ematch_rounds_per_search_opt: + if (! validate_integer_option(&parser, &elem, 0, INT32_MAX)) goto bad_usage; + ef_ematch_rounds_per_search = elem.i_value; + break; + + case ematch_search_total_opt: + if (! validate_integer_option(&parser, &elem, 0, INT32_MAX)) goto bad_usage; + ef_ematch_search_total = elem.i_value; + break; + + case ematch_trial_fdepth_opt: + if (! validate_integer_option(&parser, &elem, 0, INT32_MAX)) goto bad_usage; + ef_ematch_trial_fdepth = elem.i_value; + break; + + case ematch_trial_vdepth_opt: + if (! validate_integer_option(&parser, &elem, 0, INT32_MAX)) goto bad_usage; + ef_ematch_trial_vdepth = elem.i_value; + break; + + case ematch_trial_fapps_opt: + if (! validate_integer_option(&parser, &elem, 0, INT32_MAX)) goto bad_usage; + ef_ematch_trial_fapps = elem.i_value; + break; + + case ematch_trial_matches_opt: + if (! validate_integer_option(&parser, &elem, 0, INT32_MAX)) goto bad_usage; + ef_ematch_trial_matches = elem.i_value; + break; + + case ematch_cnstr_epsilon_opt: + if (! validate_integer_option(&parser, &elem, 0, CNSTR_RL_EPSILON_MAX)) goto bad_usage; + ef_ematch_cnstr_epsilon = elem.i_value; + break; + + case ematch_cnstr_alpha_opt: + if (! validate_double_option(&parser, &elem, 0.0, false, 1.0, false)) goto bad_usage; + ef_ematch_cnstr_alpha = elem.d_value; + break; + + case ematch_term_epsilon_opt: + if (! validate_integer_option(&parser, &elem, 0, TERM_RL_EPSILON_MAX)) goto bad_usage; + ef_ematch_term_epsilon = elem.i_value; + break; + + case ematch_term_alpha_opt: + if (! validate_double_option(&parser, &elem, 0.0, false, 1.0, false)) goto bad_usage; + ef_ematch_term_alpha = elem.d_value; + break; + + case ematch_cnstr_mode_opt: + ef_ematch_cnstr_mode = supported_ematch_mode(elem.s_value); + if (ef_ematch_cnstr_mode < 0) { + fprintf(stderr, "%s: unsupported ematching constraint mode: %s\n", parser.command_name, elem.s_value); + goto bad_usage; + } + break; + + case ematch_term_mode_opt: + ef_ematch_term_mode = supported_ematch_mode(elem.s_value); + if (ef_ematch_term_mode < 0) { + fprintf(stderr, "%s: unsupported ematching term mode: %s\n", parser.command_name, elem.s_value); + goto bad_usage; + } + break; + + case trace_opt: + pvector_push(&trace_tags, elem.s_value); + break; + } + break; + + case cmdline_error: + cmdline_print_error(&parser, &elem); + fprintf(stderr, "Try %s --help for more information\n", parser.command_name); + code = YICES_EXIT_USAGE; + goto exit; + } + } + + done: + if (incremental && delegate != NULL) { + fprintf(stderr, "%s: delegate %s does not support incremental mode\n", parser.command_name, delegate); + code = YICES_EXIT_USAGE; + goto exit; + } + + if (incremental && dimacsfile != NULL) { + fprintf(stderr, "%s: export to DIMACS is not supported in incremental mode\n", parser.command_name); + code = YICES_EXIT_USAGE; + goto exit; + } + + // force interactive to false if there's a filename + if (filename != NULL) { + interactive = false; + } + return; + + /* + * Error conditions + */ + no_mcsat: + fprintf(stderr, "mcsat is not supported: %s was not compiled with mcsat support\n", parser.command_name); + code = YICES_EXIT_USAGE; + goto exit; + + bad_usage: + print_usage(parser.command_name); + code = YICES_EXIT_USAGE; + + exit: + // cleanup then exit + // code is either YICES_EXIT_SUCCESS or YICES_EXIT_USAGE. + delete_pvector(&trace_tags); + exit(code); +} + +static void setup_mcsat(void) { + aval_t aval_true; + if (mcsat) { + smt2_enable_mcsat(); + } + + aval_true = attr_vtbl_symbol(__smt2_globals.avtbl, "true"); + + if (mcsat_nra_mgcd) { + smt2_set_option(":yices-mcsat-nra-mgcd", aval_true); + } + + if (mcsat_nra_nlsat) { + smt2_set_option(":yices-mcsat-nra-nlsat", aval_true); + } + + if (mcsat_nra_bound) { + smt2_set_option(":yices-mcsat-nra-bound", aval_true); + } + + if (mcsat_nra_bound_min >= 0) { + aval_t aval_bound_min; + rational_t q; + q_init(&q); + q_set32(&q, mcsat_nra_bound_min); + aval_bound_min = attr_vtbl_rational(__smt2_globals.avtbl, &q); + smt2_set_option(":yices-mcsat-nra-bound-min", aval_bound_min); + q_clear(&q); + } + + if (mcsat_nra_bound_max >= 0) { + aval_t aval_bound_max; + rational_t q; + q_init(&q); + q_set32(&q, mcsat_nra_bound_max); + aval_bound_max = attr_vtbl_rational(__smt2_globals.avtbl, &q); + smt2_set_option(":yices-mcsat-nra-bound-max", aval_bound_max); + q_clear(&q); + } + + if (mcsat_bv_var_size > 0) { + aval_t aval_bv_var_size; + rational_t q; + q_init(&q); + q_set32(&q, mcsat_bv_var_size); + aval_bv_var_size = attr_vtbl_rational(__smt2_globals.avtbl, &q); + smt2_set_option(":yices-mcsat-bv-var-size", aval_bv_var_size); + q_clear(&q); + } +} + +static void setup_ef(void) { + aval_t aval_true, aval_false; + + aval_true = attr_vtbl_symbol(__smt2_globals.avtbl, "true"); + aval_false = attr_vtbl_symbol(__smt2_globals.avtbl, "false"); + + if (ef_en_ematch != DEF_EMATCH_EN) { + smt2_set_option(":yices-ematch-en", (ef_en_ematch ? aval_true : aval_false)); + } + + if (ef_mbqi_max_iter >= 0) { + aval_t aval_max; + rational_t q; + q_init(&q); + q_set32(&q, ef_mbqi_max_iter); + aval_max = attr_vtbl_rational(__smt2_globals.avtbl, &q); + smt2_set_option(":yices-ef-max-iters", aval_max); + q_clear(&q); + } + + if (ef_mbqi_max_lemma_per_round >= 0) { + aval_t aval_max; + rational_t q; + q_init(&q); + q_set32(&q, ef_mbqi_max_lemma_per_round); + aval_max = attr_vtbl_rational(__smt2_globals.avtbl, &q); + smt2_set_option(":yices-ef-max-lemmas-per-round", aval_max); + q_clear(&q); + } + + if (ef_ematch_inst_per_round >= 0) { + aval_t aval_max; + rational_t q; + q_init(&q); + q_set32(&q, ef_ematch_inst_per_round); + aval_max = attr_vtbl_rational(__smt2_globals.avtbl, &q); + smt2_set_option(":yices-ematch-inst-per-round", aval_max); + q_clear(&q); + } + + if (ef_ematch_inst_per_search >= 0) { + aval_t aval_max; + rational_t q; + q_init(&q); + q_set32(&q, ef_ematch_inst_per_search); + aval_max = attr_vtbl_rational(__smt2_globals.avtbl, &q); + smt2_set_option(":yices-ematch-inst-per-search", aval_max); + q_clear(&q); + } + + if (ef_ematch_inst_total >= 0) { + aval_t aval_max; + rational_t q; + q_init(&q); + q_set32(&q, ef_ematch_inst_total); + aval_max = attr_vtbl_rational(__smt2_globals.avtbl, &q); + smt2_set_option(":yices-ematch-inst-total", aval_max); + q_clear(&q); + } + + if (ef_ematch_rounds_per_search >= 0) { + aval_t aval_max; + rational_t q; + q_init(&q); + q_set32(&q, ef_ematch_rounds_per_search); + aval_max = attr_vtbl_rational(__smt2_globals.avtbl, &q); + smt2_set_option(":yices-ematch-rounds-per-search", aval_max); + q_clear(&q); + } + + if (ef_ematch_search_total >= 0) { + aval_t aval_max; + rational_t q; + q_init(&q); + q_set32(&q, ef_ematch_search_total); + aval_max = attr_vtbl_rational(__smt2_globals.avtbl, &q); + smt2_set_option(":yices-ematch-search-total", aval_max); + q_clear(&q); + } + + if (ef_ematch_trial_fdepth >= 0) { + aval_t aval_max; + rational_t q; + q_init(&q); + q_set32(&q, ef_ematch_trial_fdepth); + aval_max = attr_vtbl_rational(__smt2_globals.avtbl, &q); + smt2_set_option(":yices-ematch-trial-fdepth", aval_max); + q_clear(&q); + } + + if (ef_ematch_trial_vdepth >= 0) { + aval_t aval_max; + rational_t q; + q_init(&q); + q_set32(&q, ef_ematch_trial_vdepth); + aval_max = attr_vtbl_rational(__smt2_globals.avtbl, &q); + smt2_set_option(":yices-ematch-trial-vdepth", aval_max); + q_clear(&q); + } + + if (ef_ematch_trial_fapps >= 0) { + aval_t aval_max; + rational_t q; + q_init(&q); + q_set32(&q, ef_ematch_trial_fapps); + aval_max = attr_vtbl_rational(__smt2_globals.avtbl, &q); + smt2_set_option(":yices-ematch-trial-fapps", aval_max); + q_clear(&q); + } + + if (ef_ematch_trial_matches >= 0) { + aval_t aval_max; + rational_t q; + q_init(&q); + q_set32(&q, ef_ematch_trial_matches); + aval_max = attr_vtbl_rational(__smt2_globals.avtbl, &q); + smt2_set_option(":yices-ematch-trial-matches", aval_max); + q_clear(&q); + } + + if (ef_ematch_cnstr_epsilon >= 0) { + aval_t aval_max; + rational_t q; + q_init(&q); + q_set32(&q, ef_ematch_cnstr_epsilon); + aval_max = attr_vtbl_rational(__smt2_globals.avtbl, &q); + smt2_set_option(":yices-ematch-cnstr-epsilon", aval_max); + q_clear(&q); + } + + if (ef_ematch_cnstr_alpha >= 0) { + aval_t aval_max; + rational_t q; + q_init(&q); + // accurate upto 3 decimal places + q_set_int32(&q, (int32_t)(ef_ematch_cnstr_alpha*1000), 1000); + aval_max = attr_vtbl_rational(__smt2_globals.avtbl, &q); + smt2_set_option(":yices-ematch-cnstr-alpha", aval_max); + q_clear(&q); + } + + if (ef_ematch_term_epsilon >= 0) { + aval_t aval_max; + rational_t q; + q_init(&q); + q_set32(&q, ef_ematch_term_epsilon); + aval_max = attr_vtbl_rational(__smt2_globals.avtbl, &q); + smt2_set_option(":yices-ematch-term-epsilon", aval_max); + q_clear(&q); + } + + if (ef_ematch_term_alpha >= 0) { + aval_t aval_max; + rational_t q; + q_init(&q); + // accurate upto 3 decimal places + q_set_int32(&q, (int32_t)(ef_ematch_term_alpha*1000), 1000); + aval_max = attr_vtbl_rational(__smt2_globals.avtbl, &q); + smt2_set_option(":yices-ematch-term-alpha", aval_max); + q_clear(&q); + } + + if (ef_ematch_cnstr_mode >= 0) { + aval_t aval_mode = attr_vtbl_symbol(__smt2_globals.avtbl, ematchmode2string[ef_ematch_cnstr_mode]); + smt2_set_option(":yices-ematch-cnstr-mode", aval_mode); + } + + if (ef_ematch_term_mode >= 0) { + aval_t aval_mode = attr_vtbl_symbol(__smt2_globals.avtbl, ematchmode2string[ef_ematch_term_mode]); + smt2_set_option(":yices-ematch-term-mode", aval_mode); + } + +} + + +/******************** + * SIGNAL HANDLER * + *******************/ + +static const char *signum_msg = "\nInterrupted by signal "; + +/* + * Write signal number of file 2 (assumed to be stderr): we can't use + * fprintf because it's not safe in a signal handler. + */ +static void write_signum(int signum) { + print_buffer_t b; + + reset_print_buffer(&b); + print_buffer_append_string(&b, signum_msg); + print_buffer_append_int32(&b, (int32_t) signum); + print_buffer_append_char(&b, '\n'); + (void) write_buffer(2, &b); +} + +/* + * We call exit on SIGINT/ABORT and XCPU + * - we could try to handle SIGINT more gracefully in interactive mode + * - this will do for now. + */ +static void default_handler(int signum) { + if (verbosity > 0) { + write_signum(signum); + } + if (show_stats) { + smt2_show_stats(); + } + _exit(YICES_EXIT_INTERRUPTED); +} + + +/* + * Initialize the signal handlers + */ +static void init_handlers(void) { + signal(SIGINT, default_handler); + signal(SIGABRT, default_handler); +#ifndef MINGW + signal(SIGXCPU, default_handler); +#endif +} + + +/* + * Reset the default handlers + */ +static void reset_handlers(void) { + signal(SIGINT, SIG_DFL); + signal(SIGABRT, SIG_DFL); +#ifndef MINGW + signal(SIGXCPU, SIG_DFL); +#endif +} + + + +/********** + * MAIN * + *********/ + +#define HACK_FOR_UTF 0 + +#if HACK_FOR_UTF + +/* + * List of locales to try + */ +#define NUM_LOCALES 3 + +static const char *const locales[NUM_LOCALES] = { + "C.UTF-8", "en_US.utf8", "en_US.UTF-8", +}; + +// HACK TO FORCE UTF8 +static void force_utf8(void) { + uint32_t i; + + for (i=0; i 1) { + fprintf(stderr, "Switched to locale '%s'\n", setlocale(LC_CTYPE, NULL)); + fflush(stderr); + } + return; + } + } + + fprintf(stderr, "Failed to switch locale to UTF-8. Current locale is '%s'\n", setlocale(LC_CTYPE, NULL)); + fflush(stderr); +} + +#else + +static void force_utf8(void) { + // Do nothing +} + +#endif + + +int main(int argc, char *argv[]) { + int32_t code; + uint32_t i; + bool prompt; + + prompt = false; + parse_command_line(argc, argv); + force_utf8(); + + if (filename != NULL) { + // read from file + if (init_smt2_file_lexer(&lexer, filename) < 0) { + perror(filename); + exit(YICES_EXIT_FILE_NOT_FOUND); + } + } else { + // read from stdin + init_smt2_stdin_lexer(&lexer); + prompt = interactive && isatty(STDIN_FILENO); + } + + init_handlers(); + + yices_init(); + init_smt2(!incremental, timeout, interactive); + if (smt2_model_format) smt2_force_smt2_model_format(); + if (bvdecimal) smt2_force_bvdecimal_format(); + if (dimacsfile != NULL && delegate == NULL) smt2_export_to_dimacs(dimacsfile); + if (delegate != NULL) { + smt2_set_delegate(delegate); + if (dimacsfile != NULL) smt2_set_dimacs_file(dimacsfile); + } + + init_smt2_tstack(&stack); + init_parser(&parser, &lexer, &stack); + + init_parameter_name_table(); + + if (verbosity > 0) { + smt2_set_verbosity(verbosity); + } + if (trace_tags.size > 0) { + for (i = 0; i < trace_tags.size; ++ i) { + smt2_enable_trace_tag(trace_tags.data[i]); + } + } + + setup_mcsat(); + setup_ef(); + + while (smt2_active()) { + if (prompt) { + // prompt + fputs("yices> ", stdout); + fflush(stdout); + } + code = parse_smt2_command(&parser); + if (code < 0) { + // syntax error + if (interactive) { + flush_lexer(&lexer); + } else { + break; // exit + } + } + } + + if (show_stats) { + smt2_show_stats(); + } + + if (dimacsfile != NULL) { + safe_free(dimacsfile); + dimacsfile = NULL; + } + if (delegate != NULL) { + safe_free(delegate); + delegate = NULL; + } + + delete_pvector(&trace_tags); + delete_parser(&parser); + close_lexer(&lexer); + delete_tstack(&stack); + delete_smt2(); + yices_exit(); + + reset_handlers(); + + return YICES_EXIT_SUCCESS; +} + diff --git a/src/mcsat/nra/nra_plugin.c b/src/mcsat/nra/nra_plugin.c index 801ca0e25..61bbc3c6a 100644 --- a/src/mcsat/nra/nra_plugin.c +++ b/src/mcsat/nra/nra_plugin.c @@ -44,7 +44,7 @@ #include "mcsat/nra/poly_constraint.h" #include "mcsat/nra/nra_plugin_explain.h" -#include "terms/terms.h" +#include "terms/rba_buffer_terms.h" #include "utils/int_array_sort2.h" #include "terms/term_explorer.h" #include "utils/refcount_strings.h" @@ -428,12 +428,105 @@ void nra_plugin_process_fully_assigned_constraint(nra_plugin_t* nra, trail_token } } +static +term_t mk_one(term_manager_t* tm) { + rational_t r0; + q_init(&r0); + q_set32(&r0, 1); + term_t r = mk_arith_constant(tm, &r0); + q_clear(&r0); + return r; +} + +static +term_t mk_add(term_manager_t* tm, term_t t1, term_t t2) { + rba_buffer_t *b; + term_table_t *tbl; + + b = term_manager_get_arith_buffer(tm); + tbl = tm->terms; + reset_rba_buffer(b); + rba_buffer_add_term(b, tbl, t1); + rba_buffer_add_term(b, tbl, t2); + + return mk_arith_term(tm, b); +} + +static +term_t mk_sub(term_manager_t* tm, term_t t1, term_t t2) { + rba_buffer_t *b; + term_table_t *tbl; + + b = term_manager_get_arith_buffer(tm); + tbl = tm->terms; + reset_rba_buffer(b); + rba_buffer_add_term(b, tbl, t1); + rba_buffer_sub_term(b, tbl, t2); + + return mk_arith_term(tm, b); +} + +static +term_t mk_neg(term_manager_t* tm, term_t t1) { + rba_buffer_t *b; + term_table_t *tbl; + + b = term_manager_get_arith_buffer(tm); + tbl = tm->terms; + reset_rba_buffer(b); + rba_buffer_sub_term(b, tbl, t1); + + return mk_arith_term(tm, b); +} + +static +term_t mk_mul(term_manager_t* tm, term_t t1, term_t t2) { + rba_buffer_t *b; + term_table_t *tbl; + + b = term_manager_get_arith_buffer(tm); + tbl = tm->terms; + reset_rba_buffer(b); + rba_buffer_add_term(b, tbl, t1); + rba_buffer_mul_term(b, tbl, t2); + + return mk_arith_term(tm, b); +} + +static +term_t mk_ite_with_supertype(term_manager_t* tm, term_t cond, term_t then_term, term_t else_term) { + term_table_t *tbl; + type_t tau; + + // Check whether then/else are compatible and get the supertype + tbl = tm->terms; + tau = super_type(tm->types, term_type(tbl, then_term), term_type(tbl, else_term)); + assert (tau != NULL_TYPE); + + return mk_ite(tm, cond, then_term, else_term, tau); +} + +static +term_t mk_simp_or(term_manager_t* tm, uint32_t n, term_t arg[]) { + switch (n) { + case 0: + return false_term; + case 1: + return arg[0]; + case 2: + return mk_binary_or(tm, arg[0], arg[1]); + default: + return mk_or(tm, n, arg); + } +} + static void nra_plugin_new_term_notify(plugin_t* plugin, term_t t, trail_token_t* prop) { uint32_t i; nra_plugin_t* nra = (nra_plugin_t*) plugin; term_table_t* terms = nra->ctx->terms; + term_manager_t* tm = nra->ctx->tm; if (ctx_trace_enabled(nra->ctx, "mcsat::new_term")) { ctx_trace_printf(nra->ctx, "nra_plugin_new_term_notify: "); @@ -476,16 +569,16 @@ void nra_plugin_new_term_notify(plugin_t* plugin, term_t t, trail_token_t* prop) // Add a lemma (assuming non-zero): // (div m n) // (and (= m (+ (* n q) r)) (<= 0 r (- (abs n) 1)))))) - term_t guard = opposite_term(_o_yices_arith_eq0_atom(n)); - term_t c1 = _o_yices_eq(m, _o_yices_add(_o_yices_mul(n, q), r)); + term_t guard = opposite_term(mk_arith_term_eq0(tm, n)); + term_t c1 = mk_eq(tm, m, mk_add(tm, mk_mul(tm, n, q), r)); term_t c2 = arith_geq_atom(terms, r); // r < (abs n) same as not (r - abs) >= 0 - term_t abs_n = _o_yices_ite(_o_yices_arith_geq0_atom(n), n, _o_yices_neg(n)); - term_t c3 = opposite_term(arith_geq_atom(terms, _o_yices_sub(r, abs_n))); + term_t abs_n = mk_ite_with_supertype(tm, mk_arith_term_geq0(tm, n), n, mk_neg(tm, n)); + term_t c3 = opposite_term(arith_geq_atom(terms, mk_sub(tm, r, abs_n))); - prop->definition_lemma(prop, _o_yices_implies(guard, c1), t); - prop->definition_lemma(prop, _o_yices_implies(guard, c2), t); - prop->definition_lemma(prop, _o_yices_implies(guard, c3), t); + prop->definition_lemma(prop, mk_implies(tm, guard, c1), t); + prop->definition_lemma(prop, mk_implies(tm, guard, c2), t); + prop->definition_lemma(prop, mk_implies(tm, guard, c3), t); break; } case ARITH_RDIV: { @@ -497,18 +590,18 @@ void nra_plugin_new_term_notify(plugin_t* plugin, term_t t, trail_token_t* prop) // Add a lemma (assuming non-zero): // (n != 0) => m = n*q // (and (= m (+ (* n q) r)) (<= 0 r (- (abs n) 1)))))) - term_t guard = opposite_term(_o_yices_arith_eq0_atom(n)); - term_t c = _o_yices_eq(m, _o_yices_mul(n, q)); - prop->definition_lemma(prop, _o_yices_implies(guard, c), t); + term_t guard = opposite_term(mk_arith_term_eq0(tm, n)); + term_t c = mk_eq(tm, m, mk_mul(tm, n, q)); + prop->definition_lemma(prop, mk_implies(tm, guard, c), t); break; } case ARITH_FLOOR: { term_t arg = arith_floor_arg(terms, t); // t <= arg < t+1: t is int so it should be fine - term_t ineq1 = _o_yices_arith_geq_atom(arg, t); - term_t t_1 = _o_yices_add(t, _o_yices_rational32(1, 1)); - term_t ineq2 = _o_yices_arith_gt_atom(t_1, arg); + term_t ineq1 = mk_arith_geq(tm, arg, t); + term_t t_1 = mk_add(tm, t, mk_one(tm)); + term_t ineq2 = mk_arith_gt(tm, t_1, arg); prop->lemma(prop, ineq1); prop->lemma(prop, ineq2); @@ -518,9 +611,9 @@ void nra_plugin_new_term_notify(plugin_t* plugin, term_t t, trail_token_t* prop) term_t arg = arith_ceil_arg(terms, t); // t-1 < arg <= t: t is int so it should be fine - term_t t_1 = _o_yices_sub(t, _o_yices_rational32(1, 1)); - term_t ineq1 = _o_yices_arith_gt_atom(arg, t_1); - term_t ineq2 = _o_yices_arith_geq_atom(t, arg); + term_t t_1 = mk_sub(tm, t, mk_one(tm)); + term_t ineq1 = mk_arith_gt(tm, arg, t_1); + term_t ineq2 = mk_arith_geq(tm, t, arg); prop->lemma(prop, ineq1); prop->lemma(prop, ineq2); @@ -536,10 +629,10 @@ void nra_plugin_new_term_notify(plugin_t* plugin, term_t t, trail_token_t* prop) ivector_t disjuncts; init_ivector(&disjuncts, type_size); for (i=0; i < type_size; i++) { - term_t disjunct = _o_yices_eq(t, _o_yices_constant(type, i)); + term_t disjunct = mk_eq(tm, t, mk_constant(tm, type, i)); ivector_push(&disjuncts, disjunct); } - term_t tcc = _o_yices_or(type_size, disjuncts.data); + term_t tcc = mk_simp_or(tm, type_size, disjuncts.data); prop->lemma(prop, tcc); delete_ivector(&disjuncts); } @@ -655,7 +748,8 @@ void nra_plugin_new_term_notify(plugin_t* plugin, term_t t, trail_token_t* prop) case CONSTANT_TERM: { // Propagate constant value int32_t int_value; - _o_yices_scalar_const_value(t, &int_value); + int_value = generic_const_value(terms, t); + lp_rational_t rat_value; lp_rational_construct_from_int(&rat_value, int_value, 1); lp_value_t lp_value; @@ -683,10 +777,10 @@ void nra_plugin_new_term_notify(plugin_t* plugin, term_t t, trail_token_t* prop) } // Add bound lemma b - t >= 0 && t + b >= 0 - term_t ub_term = _o_yices_sub(nra->global_bound_term, t); - term_t lb_term = _o_yices_add(nra->global_bound_term, t); - term_t ub = _o_yices_arith_geq0_atom(ub_term); - term_t lb = _o_yices_arith_geq0_atom(lb_term); + term_t ub_term = mk_sub(tm, nra->global_bound_term, t); + term_t lb_term = mk_add(tm, nra->global_bound_term, t); + term_t ub = mk_arith_term_geq0(tm, ub_term); + term_t lb = mk_arith_term_geq0(tm, lb_term); prop->lemma(prop, ub); prop->lemma(prop, lb); @@ -698,7 +792,7 @@ void nra_plugin_new_term_notify(plugin_t* plugin, term_t t, trail_token_t* prop) q_init(&q); q_set32(&q, nra->ctx->options->nra_bound_min); term_t min = mk_arith_constant(nra->ctx->tm, &q); - term_t min_bound = _o_yices_arith_geq_atom(nra->global_bound_term, min); + term_t min_bound = mk_arith_geq(tm, nra->global_bound_term, min); prop->lemma(prop, min_bound); q_clear(&q); } @@ -707,7 +801,7 @@ void nra_plugin_new_term_notify(plugin_t* plugin, term_t t, trail_token_t* prop) q_init(&q); q_set32(&q, nra->ctx->options->nra_bound_max); term_t max = mk_arith_constant(nra->ctx->tm, &q); - term_t max_bound = _o_yices_arith_leq_atom(nra->global_bound_term, max); + term_t max_bound = mk_arith_leq(tm, nra->global_bound_term, max); prop->lemma(prop, max_bound); q_clear(&q); } diff --git a/src/mcsat/nra/nra_plugin_internal.c b/src/mcsat/nra/nra_plugin_internal.c index 7cd67d384..c7ce607da 100644 --- a/src/mcsat/nra/nra_plugin_internal.c +++ b/src/mcsat/nra/nra_plugin_internal.c @@ -90,6 +90,8 @@ void nra_plugin_get_term_variables(nra_plugin_t* nra, term_t t, int_mset_t* vars } } } else { + // product inside polynomial cannot be another polynormial. + assert(term_kind(terms, product) != ARITH_POLY); // Variable, or foreign term var = variable_db_get_variable(var_db, product); int_mset_add(vars_out, var); diff --git a/src/solvers/floyd_warshall/idl_floyd_warshall.c b/src/solvers/floyd_warshall/idl_floyd_warshall.c index 3bf4df6a9..2442138f5 100644 --- a/src/solvers/floyd_warshall/idl_floyd_warshall.c +++ b/src/solvers/floyd_warshall/idl_floyd_warshall.c @@ -2227,7 +2227,12 @@ thvar_t idl_create_pprod(idl_solver_t *solver, pprod_t *p, thvar_t *map) { idl_exception(solver, FORMULA_NOT_IDL); } - +/* + * Internalization for a division: always fails with NOT_RDL exception + */ +static thvar_t idl_create_rdiv(idl_solver_t *solver, thvar_t num, thvar_t den) { + idl_exception(solver, FORMULA_NOT_RDL); +} /* * ATOM CONSTRUCTORS @@ -2670,7 +2675,7 @@ void idl_free_model(idl_solver_t *solver) { * Value of variable x in the model * - copy the value in v and return true */ -bool idl_value_in_model(idl_solver_t *solver, thvar_t x, rational_t *v) { +bool idl_value_in_model(idl_solver_t *solver, thvar_t x, arithval_in_model_t* res) { dl_triple_t *d; int32_t aux; @@ -2686,8 +2691,9 @@ bool idl_value_in_model(idl_solver_t *solver, thvar_t x, rational_t *v) { aux -= idl_vertex_value(solver, d->source); } - q_set32(v, aux); // aux is the value of (target - source) in the model - q_add(v, &d->constant); + assert(res->tag == ARITHVAL_RATIONAL); + q_set32(&res->val.q, aux); // aux is the value of (target - source) in the model + q_add(&res->val.q, &d->constant); return true; } @@ -2744,6 +2750,7 @@ static arith_interface_t idl_intern = { (create_arith_const_fun_t) idl_create_const, (create_arith_poly_fun_t) idl_create_poly, (create_arith_pprod_fun_t) idl_create_pprod, + (create_arith_rdiv_fun_t) idl_create_rdiv, (create_arith_atom_fun_t) idl_create_eq_atom, (create_arith_atom_fun_t) idl_create_ge_atom, diff --git a/src/solvers/floyd_warshall/idl_floyd_warshall.h b/src/solvers/floyd_warshall/idl_floyd_warshall.h index bb873e4e9..04cb2f988 100644 --- a/src/solvers/floyd_warshall/idl_floyd_warshall.h +++ b/src/solvers/floyd_warshall/idl_floyd_warshall.h @@ -763,7 +763,7 @@ static inline int32_t idl_vertex_value(idl_solver_t *solver, int32_t x) { * Value of variable v in the model * - copy the value in rational q and return true */ -extern bool idl_value_in_model(idl_solver_t *solver, thvar_t v, rational_t *q); +extern bool idl_value_in_model(idl_solver_t *solver, thvar_t v, arithval_in_model_t* res); /* diff --git a/src/solvers/floyd_warshall/rdl_floyd_warshall.c b/src/solvers/floyd_warshall/rdl_floyd_warshall.c index 3f87522ce..c32c4c2b6 100644 --- a/src/solvers/floyd_warshall/rdl_floyd_warshall.c +++ b/src/solvers/floyd_warshall/rdl_floyd_warshall.c @@ -2489,7 +2489,12 @@ thvar_t rdl_create_pprod(rdl_solver_t *solver, pprod_t *p, thvar_t *map) { rdl_exception(solver, FORMULA_NOT_RDL); } - +/* + * Internalization for a division: always fails with NOT_RDL exception + */ +static thvar_t rdl_create_rdiv(rdl_solver_t *solver, thvar_t num, thvar_t den) { + rdl_exception(solver, FORMULA_NOT_RDL); +} /* * ATOM CONSTRUCTORS @@ -3225,8 +3230,12 @@ void rdl_free_model(rdl_solver_t *solver) { * Value of variable x in the model * - copy the value in v and return true */ -bool rdl_value_in_model(rdl_solver_t *solver, thvar_t x, rational_t *v) { +bool rdl_value_in_model(rdl_solver_t *solver, thvar_t x, arithval_in_model_t* res) { dl_triple_t *d; + rational_t* v; + + assert(res->tag == ARITHVAL_RATIONAL); + v = &res->val.q; assert(solver->value != NULL && 0 <= x && x < solver->vtbl.nvars); d = dl_var_triple(&solver->vtbl, x); @@ -3299,6 +3308,7 @@ static arith_interface_t rdl_intern = { (create_arith_const_fun_t) rdl_create_const, (create_arith_poly_fun_t) rdl_create_poly, (create_arith_pprod_fun_t) rdl_create_pprod, + (create_arith_rdiv_fun_t) rdl_create_rdiv, (create_arith_atom_fun_t) rdl_create_eq_atom, (create_arith_atom_fun_t) rdl_create_ge_atom, diff --git a/src/solvers/floyd_warshall/rdl_floyd_warshall.h b/src/solvers/floyd_warshall/rdl_floyd_warshall.h index b3678fcf5..7e01df732 100644 --- a/src/solvers/floyd_warshall/rdl_floyd_warshall.h +++ b/src/solvers/floyd_warshall/rdl_floyd_warshall.h @@ -803,7 +803,7 @@ static inline rational_t *rdl_vertex_value(rdl_solver_t *solver, int32_t x) { * Value of variable v in the model * - copy the value into q and return true */ -extern bool rdl_value_in_model(rdl_solver_t *solver, thvar_t v, rational_t *q); +extern bool rdl_value_in_model(rdl_solver_t *solver, thvar_t v, arithval_in_model_t* res); diff --git a/src/solvers/mcarith/mcarith.c b/src/solvers/mcarith/mcarith.c new file mode 100644 index 000000000..4b8c6f85b --- /dev/null +++ b/src/solvers/mcarith/mcarith.c @@ -0,0 +1,1566 @@ +/* + * 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 . + */ + +/* + * MCARITH SOLVER + * + * Uses MCSAT to implement a non-linear arithmetic solver. + */ +#ifdef HAVE_MCSAT + +#include "context/context.h" +#include "solvers/mcarith/mcarith.h" +#include "solvers/simplex/simplex.h" + +#include "mcsat/trail.h" +#include "mcsat/variable_db.h" + +#include "model/models.h" +#include "model/model_queries.h" + +#include "yices.h" + +void simplex_attach_eterm(simplex_solver_t *solver, thvar_t v, eterm_t t); +thvar_t simplex_create_const(simplex_solver_t *solver, rational_t *q); +eterm_t simplex_eterm_of_var(simplex_solver_t *solver, thvar_t v); +void simplex_start_internalization(simplex_solver_t *solver); +void simplex_assert_clause_vareq_axiom(simplex_solver_t *solver, uint32_t n, literal_t *c, thvar_t x, thvar_t y); +void simplex_assert_cond_vareq_axiom(simplex_solver_t *solver, literal_t c, thvar_t x, thvar_t y); + +/** + * Allocate a polynomial from an existing polynomial, but mapping variables. + */ +static +polynomial_t* alloc_polynomial_from_map(polynomial_t* p, thvar_t* map, int32_t var_count) { + uint32_t n = p->nterms; + polynomial_t* pv = alloc_raw_polynomial(n); + if (n == 0) return pv; + + q_set(&pv->mono[0].coeff, &p->mono[0].coeff); + if (p->mono[0].var == const_idx) { + pv->mono[0].var = 0; + } else { + assert(0 <= map[0] && map[0] < var_count); + pv->mono[0].var = map[0]; + } + for (uint32_t i = 1; i < n; ++i) { + q_set(&pv->mono[i].coeff, &p->mono[i].coeff); + assert(0 <= map[i] && map[i] < var_count); + pv->mono[i].var = map[i]; + } + return pv; +} + +// Indicates if the variable is free or a poly. +enum mcarith_var_type { VAR_FREE, VAR_CONST, VAR_POLY }; + +struct mcarith_var_s { + enum mcarith_var_type type; + union { + rational_t *rat; + pprod_t* prod; + } def; +}; + +typedef struct mcarith_var_s mcarith_var_t; + +enum mcarith_assertion_type { VAR_EQ, VAR_EQ0, VAR_GE0, POLY_EQ0, POLY_GE0, ATOM_ASSERT }; + +/** + * Assertion for mcarith. + * + * type and def value determine the assertion. + * tt indicates if the assertion is true or false. + * lit indicates the literal associated with the assetion (or null_literal if none). + * + * + * VAR_EQ: An equality between two theory variables. + * def.eq contains the left-hand and right hand side theory variables. + * VAR_EQ0: A theory variable is equal to 0. + * def.var contains the variable + * VAR_GE0: A theory variable is greater than or equal to 0. + * def.var contains the variable + * POLY_EQ0: A polynomial is equal to 0. + * def.poly contains the polynomial over theory variables. + * POLY_GE0: A polynomial is greater than or equal to 0. + * def.poly contains the polynomial over theory variables. + * ATOM_ASSERT: An atom is asserted to be true. + */ +typedef struct mcarith_assertion_s { + // Indicates the type of the assertion. + enum mcarith_assertion_type type; + // A polynomial over theory variables. + union { + thvar_t var; + polynomial_t* poly; + struct { thvar_t lhs; thvar_t rhs; } eq; + int32_t atom; + } def; + // tt is true if the poly should be non-negative and false if negative. + bool tt; + // Literal associated with assertion (or null_literal if none). + literal_t lit; +} mcarith_assertion_t; + +void free_mcarith_assertion(const mcarith_assertion_t* a) { + switch (a->type) { + case POLY_EQ0: + case POLY_GE0: + free_polynomial(a->def.poly); + break; + default: + break; + } +} + +/* + * On entry to each decision level k we store: + * - the number of asserted bounds (i.e., arith_stack.top) + * - the number of asserted atoms (i.e., arith_queue.top) + * + * At level 0: n_bounds = 0, n_assertions = 0 + */ +typedef struct mcarith_undo_record_s { + uint32_t n_assertions; +} mcarith_undo_record_t; + +typedef struct mcarith_undo_stack_s { + uint32_t size; + uint32_t top; + mcarith_undo_record_t *data; +} mcarith_undo_stack_t; + +/* + * Initialize: n = initial size + */ +static void init_mcarith_undo_stack(mcarith_undo_stack_t *stack, uint32_t n) { + assert(0 < n); + + stack->size = n; + stack->top = 0; + stack->data = safe_malloc(n * sizeof(mcarith_undo_record_t)); +} + +/* + * Double the undo stack size + */ +static void extend_mcarith_undo_stack(mcarith_undo_stack_t* stack) { + stack->size = 2 * stack->size; + // Check for overflow. + if (stack->size == 0) + out_of_memory(); + stack->data = safe_realloc(stack->data, stack->size * sizeof(mcarith_undo_record_t)); +} + +/* + * Push an undo record to the stack. + */ +static void mcarith_undo_push_record(mcarith_undo_stack_t* stack, uint32_t n_a) { + uint32_t i = stack->top; + assert (stack->size > 0); + // Double stack size if needed + if (i == stack->size) { + extend_mcarith_undo_stack(stack); + } + assert(i < stack->size); + stack->data[i].n_assertions = n_a; + stack->top = i+1; +} + +/* + * Pop an undo record to the stack. + */ +static mcarith_undo_record_t* mcarith_undo_pop_record(mcarith_undo_stack_t* stack) { + assert(stack->top > 0); + return stack->data + --stack->top; +} + +/* + * Reset to given undo level (which should be greater than current one. + */ +static +mcarith_undo_record_t* mcarith_undo_backtrack(mcarith_undo_stack_t* stack, uint32_t back_level) { + assert(stack->top > back_level); + stack->top = back_level; + return stack->data + back_level; +} + +// Reset undo stack. +static +void mcarith_undo_reset(mcarith_undo_stack_t* stack) { + stack->top = 0; +} + +// Variables kinds specific to mcsat +typedef enum { + MCVAR_SIMPLEX = 0, // Defined in simplex variable table + MCVAR_PPROD = 1, // A power product + MCVAR_RDIV = 2 // A real division +} mcsatvar_kind_t; + +typedef struct { + mcsatvar_kind_t kind; + union { + pprod_t* pprod; + struct { + thvar_t num; + thvar_t den; + } rdiv; + } def; +} mcsatvar_def_t; + +// Note. +// This conditional causes MCSAT to create new tables for types products and terms. +// Disabling it causes mcsat to share those tables with yices. +#define MCSAT_STANDALONE_TERMS + +struct mcarith_solver_s { + // Simple solver + simplex_solver_t simplex; + // Context for mcsat solver + context_t mcsat_ctx; + // MCSat solver + mcsat_solver_t* mcsat; + // Model returned by mcsat + model_t* model; + +#ifdef MCSAT_STANDALONE_TERMS + // Type table for mcsat + type_table_t types; + // Power product table for mcsat + pprod_table_t pprods; + // Term Table for mcsat + term_table_t terms; +#else + // Type table for mcsat + type_table_t* types; + // Power product table for mcsat + pprod_table_t* pprods; + // Term Table for mcsat + term_table_t* terms; +#endif + ivector_t var_terms; + + // Size of atom term array + uint32_t atom_terms_size; + // Map atom indices to term (or NULL_TERM if unassigned). + term_t* atom_terms; + + // Assertion array + mcarith_assertion_t* assertions; + // Number of entries in the array + uint32_t assertion_capacity; + // Number of assertions so far. + uint32_t assertion_count; + + // Vector for storing assertions mcsat sees. + // Each element is a term formed + ivector_t mcsat_assertions; + + mcarith_undo_stack_t undo_stack; +}; + +void mcarith_enable_row_saving(mcarith_solver_t *solver) { + simplex_enable_row_saving(&solver->simplex); +} + +#ifdef MCSAT_STANDALONE_TERMS +static +pprod_table_t* mcarith_solver_pprods(mcarith_solver_t* s) { + return &s->pprods; +} + +static +type_table_t* mcarith_solver_types(mcarith_solver_t* s) { + return &s->types; +} + +static +term_table_t* mcarith_solver_terms(mcarith_solver_t* s) { + return &s->terms; +} +#else +static +pprod_table_t* mcarith_solver_pprods(mcarith_solver_t* s) { + return s->pprods; +} + +static +type_table_t* mcarith_solver_types(mcarith_solver_t* s) { + return s->types; +} + +static +term_table_t* mcarith_solver_terms(mcarith_solver_t* s) { + return s->terms; +} +#endif + +#define DEF_MCSAT_VAR_VECTOR_SIZE 64 +#define DEF_MCSAT_UNDO_STACK_SIZE 16 +#define DEF_MCSAT_ASSERTION_VECTOR_SIZE 32 + +/* + * Initialize a mcarith solver + */ +void init_mcarith_solver(mcarith_solver_t **solver, context_t* ctx) { + printf("init_mcarith_solver\n"); + const uint32_t init_assertion_capacity = 64; + + mcarith_solver_t* s = safe_malloc(sizeof(mcarith_solver_t)); + init_simplex_solver(&s->simplex, ctx->core, &ctx->gate_manager, ctx->egraph); + + s->mcsat = 0; + s->model = 0; + +#ifdef MCSAT_STANDALONE_TERMS + // Initialize mcsat type table + init_type_table(&s->types, 64); + // Initialize mcsat power product table. + init_pprod_table(&s->pprods, 0); // Use default size + // Initialize term table + const uint32_t init_termtable_size = 1024; + init_term_table(&s->terms, init_termtable_size, &s->types, &s->pprods); +#else + s->types = ctx->types; + s->pprods = ctx->terms->pprods; + s->terms = ctx->terms; + assert(ctx->types == ctx->terms->types); +#endif + + // Create array for mapping theory variables to initial term. + assert(s->simplex.vtbl.nvars == 1); + init_ivector(&s->var_terms, s->simplex.vtbl.size); + rational_t one; + q_init(&one); + q_set_one(&one); + ivector_push(&s->var_terms, arith_constant(mcarith_solver_terms(s), &one)); + + s->atom_terms = 0; + s->atom_terms_size = 0; + + // Initialize assertion table + s->assertions = safe_malloc(init_assertion_capacity * sizeof(mcarith_assertion_t)); + s->assertion_capacity = init_assertion_capacity; + s->assertion_count = 0; + + // Create undo stack + init_mcarith_undo_stack(&s->undo_stack, DEF_MCSAT_UNDO_STACK_SIZE); + + // Initialize storage of assertions to pass to mcsat. + init_ivector(&s->mcsat_assertions, DEF_MCSAT_ASSERTION_VECTOR_SIZE); + + *solver = s; +} + +static +void mcarith_free_mcsat(mcarith_solver_t* s) { + if (s->mcsat) { + mcsat_destruct(s->mcsat); + safe_free(s->mcsat); + delete_context(&s->mcsat_ctx); + s->mcsat = 0; + } +} + +/* + * Free the model generated by build_model after a SAT result. + */ +static void mcarith_free_model(void* s) { + mcarith_solver_t* solver; + + solver = s; + if (solver->model != 0) { + delete_model(solver->model); + free(solver->model); + solver->model = 0; + } +} + +void destroy_mcarith_solver(mcarith_solver_t* s) { + mcarith_free_mcsat(s); + mcarith_free_model(s); + // Free assertions + for (uint32_t i = 0; i != s->assertion_count; ++i) { + free_mcarith_assertion(s->assertions + i); + } + safe_free(s->assertions); + // Free MCSat terms + delete_ivector(&s->var_terms); + safe_free(s->atom_terms); + delete_ivector(&s->mcsat_assertions); + +#ifdef MCSAT_STANDALONE_TERMS + delete_term_table(&s->terms); + delete_pprod_table(&s->pprods); + delete_type_table(&s->types); +#endif + // Free solver + delete_simplex_solver(&s->simplex); + // Free solver itself + safe_free(s); +} + +/* + * This resizes a size_ptr and term array so that it can accomodate the new_size entries. + */ +static inline +void realloc_term_array(uint32_t* size_ptr, term_t** term_array, uint32_t new_size) { + if (new_size > *size_ptr) { + *term_array = safe_realloc(*term_array, sizeof(term_t) * new_size); + for (int i = *size_ptr; i < new_size; ++i) { + (*term_array)[i] = NULL_TERM; + } + *size_ptr = new_size; + } +} + +/* + * This resizes var_terms to make sure it is large enough + * to reference all vtbl entries. + */ +static inline +void mcarith_check_var_size(mcarith_solver_t *solver) { + uint32_t size; + uint32_t new_size; + ivector_t* a; + + a = &solver->var_terms; + resize_ivector(a, solver->simplex.vtbl.size); + + size = a->size; + new_size = solver->simplex.vtbl.nvars; + assert(new_size < solver->simplex.vtbl.size); + for (int32_t* p = a->data + size; p < a->data + new_size; ++p) { + *p = NULL_TERM; + } + a->size = new_size; +} + +/* + * This resizes the atom_terms to make sure it is large enough + * to reference all atbl entries. + */ +static inline +void mcarith_check_atom_size(mcarith_solver_t *solver) { + uint32_t new_size = solver->simplex.atbl.size; + realloc_term_array(&solver->atom_terms_size, &solver->atom_terms, new_size); +} + +static +void rba_buffer_add_mono_mcarithvar(mcarith_solver_t* solver, rba_buffer_t* b, rational_t *a, thvar_t v); + +/** + * This creates a term from a polynomial while taking care not to + * introduce a polynomial from a constant. + */ +static +term_t mcarith_poly(term_table_t* terms, rba_buffer_t* b) { + + if (b->nterms == 0) { + rational_t q; + q_init(&q); + return arith_constant(terms, &q); + } + + if (b->nterms == 1) { + mono_t* m = b->mono + b->root; + if (m->prod == empty_pp) { + return arith_constant(terms, &m->coeff); + } + } + + return arith_poly(terms, b); +} + +/** + * This sets the value of an index in the array to a value while growing the + * array if needed (new elements are initialized to zero). + */ +static +void term_ivector_grow_set(ivector_t* a, uint32_t idx, int32_t val) { + uint32_t size; + size = a->size; + if (size < idx+1) { + for (int32_t* p = a->data + size; p != a->data + idx; ++p) { + *p = NULL_TERM; + } + a->size = idx+1; + } + a->data[idx] = val; +} + +/* +Return term associated with theory variable. +*/ +static +term_t get_term(mcarith_solver_t* solver, thvar_t v) { + arith_vartable_t* table; + term_table_t* terms; + + table = &solver->simplex.vtbl; + assert(0 <= v && v < table->nvars); + + terms = mcarith_solver_terms(solver); + + assert(v < solver->var_terms.size); + term_t t = solver->var_terms.data[v]; + if (t != NULL_TERM) { + assert(good_term(terms, t)); + return t; + } + + uint8_t tag = table->tag[v]; + bool is_int = (tag & AVARTAG_INT_MASK) != 0; + switch (tag & AVARTAG_KIND_MASK) { + // Uninterpreted + case AVARTAG_KIND_FREE: + { + type_t tp = is_int ? int_type(mcarith_solver_types(solver)) : real_type(mcarith_solver_types(solver)); + t = new_uninterpreted_term(terms, tp); + assert(good_term(terms, t)); + } + break; + case AVARTAG_KIND_POLY: + { + rba_buffer_t b; + polynomial_t* p = table->def[v]; + init_rba_buffer(&b, mcarith_solver_pprods(solver)); + uint32_t n = p->nterms; + for (uint32_t j = 0; j < n; ++j) { + rational_t* r = &p->mono[j].coeff; + if (j == 0 && p->mono[j].var == const_idx) { + rba_buffer_add_const(&b, r); + } else { + thvar_t v = p->mono[j].var; + rba_buffer_add_mono_mcarithvar(solver, &b, r, v); + } + } + t = mcarith_poly(terms, &b); + assert(good_term(terms, t)); + } + break; + case AVARTAG_KIND_PPROD: + //pprod_t* p = table->def[v]; + longjmp(*solver->simplex.env, INTERNAL_ERROR); + break; + case AVARTAG_KIND_CONST: + t = arith_constant(terms, table->def[v]); + assert(good_term(terms, t)); + break; + default: + longjmp(*solver->simplex.env, INTERNAL_ERROR); + } + term_ivector_grow_set(&solver->var_terms, v, t); + return t; +} + +/* This adds the theory var value to the buffer while ensuring a nested polynomial term is not created. */ +static +void rba_buffer_add_mono_mcarithvar(mcarith_solver_t* solver, rba_buffer_t* b, rational_t *a, thvar_t v) { + arith_vartable_t* table; + term_table_t* terms; + polynomial_t* p; + rational_t* c; + rational_t aux; + term_t t; + + q_init(&aux); + + table = &solver->simplex.vtbl; + terms = mcarith_solver_terms(solver); + + assert(0 <= v && v < table->nvars); + + uint8_t tag = table->tag[v]; + switch (tag & AVARTAG_KIND_MASK) { + case AVARTAG_KIND_POLY: { + p = table->def[v]; + uint32_t n = p->nterms; + for (uint32_t j = 0; j < n; ++j) { + c = &p->mono[j].coeff; + q_set(&aux, a); + q_mul(&aux, c); + if (j == 0 && p->mono[j].var == const_idx) { + rba_buffer_add_const(b, &aux); + } else { + t = get_term(solver, p->mono[j].var); + assert(term_kind(terms, t) != ARITH_POLY); + rba_buffer_add_mono(b, &aux, var_pp(t)); + } + } + break; + } + case AVARTAG_KIND_PPROD: + //pprod_t* p = table->def[v]; + longjmp(*solver->simplex.env, INTERNAL_ERROR); + break; + case AVARTAG_KIND_CONST: + q_set(&aux, a); + q_mul(&aux, table->def[v]); + rba_buffer_add_const(b, &aux); + break; + default: + t = get_term(solver, v); + assert(term_kind(terms, t) != ARITH_POLY); + rba_buffer_add_mono(b, a, var_pp(t)); + } + q_clear(&aux); +} + +/* This adds the theory var value to the buffer while ensuring a nested polynomial term is not created. */ +static +void rba_buffer_add_mcarithvar(mcarith_solver_t* solver, rba_buffer_t* b, thvar_t v) { + arith_vartable_t* table; + term_table_t* terms; + polynomial_t* p; + rational_t* c; + term_t t; + thvar_t mv; + + table = &solver->simplex.vtbl; + terms = mcarith_solver_terms(solver); + + assert(0 <= v && v < table->nvars); + + uint8_t tag = table->tag[v]; + switch (tag & AVARTAG_KIND_MASK) { + case AVARTAG_KIND_POLY: { + p = table->def[v]; + uint32_t n = p->nterms; + for (uint32_t j = 0; j < n; ++j) { + c = &p->mono[j].coeff; + mv = p->mono[j].var; + if (j == 0 && mv == const_idx) { + rba_buffer_add_const(b, c); + } else { + rba_buffer_add_mono_mcarithvar(solver, b, c, mv); + } + } + break; + } + case AVARTAG_KIND_PPROD: + //pprod_t* p = table->def[v]; + longjmp(*solver->simplex.env, INTERNAL_ERROR); + break; + case AVARTAG_KIND_CONST: + rba_buffer_add_const(b, table->def[v]); + break; + default: + t = get_term(solver, v); + assert(term_kind(terms, t) != ARITH_POLY); + rba_buffer_add_pp(b, var_pp(t)); + } +} + +/* This subtracts the theory var value from the buffer while ensuring a nested polynomial term is not created. */ +static +void rba_buffer_sub_mcarithvar(mcarith_solver_t* solver, rba_buffer_t* b, thvar_t v) { + arith_vartable_t* table; + term_table_t* terms; + uint32_t j; + uint32_t n; + polynomial_t* p; + rational_t* c; + term_t t; + thvar_t mv; + rational_t aux; + + table = &solver->simplex.vtbl; + terms = mcarith_solver_terms(solver); + + assert(0 <= v && v < table->nvars); + + uint8_t tag = table->tag[v]; + switch (tag & AVARTAG_KIND_MASK) { + case AVARTAG_KIND_POLY: { + p = table->def[v]; + n = p->nterms; + for (j = 0; j < n; ++j) { + c = &p->mono[j].coeff; + mv = p->mono[j].var; + if (j == 0 && mv == const_idx) { + rba_buffer_sub_const(b, c); + } else { + q_init(&aux); + q_set(&aux, c); + q_neg(&aux); + rba_buffer_add_mono_mcarithvar(solver, b, &aux, mv); + q_clear(&aux); + } + } + break; + } + case AVARTAG_KIND_PPROD: + //pprod_t* p = table->def[v]; + longjmp(*solver->simplex.env, INTERNAL_ERROR); + break; + case AVARTAG_KIND_CONST: + rba_buffer_sub_const(b, table->def[v]); + break; + default: + t = get_term(solver, v); + assert(term_kind(terms, t) != ARITH_POLY); + rba_buffer_sub_pp(b, var_pp(t)); + } +} + +/* + * Return the term associated with the given atom index. + */ +static +term_t get_atom(mcarith_solver_t* solver, int32_t atom_index) { + arith_atomtable_t *atbl; + term_t result; + term_table_t* terms; + arith_atom_t* ap; + term_t v; + rational_t* bnd; + rba_buffer_t b; + + mcarith_check_atom_size(solver); + + atbl = &solver->simplex.atbl; + assert(0 <= atom_index && atom_index < atbl->natoms); + + result = solver->atom_terms[atom_index]; + if (result != NULL_TERM) return result; + + terms = mcarith_solver_terms(solver); + + ap = atbl->atoms + atom_index; + // Get variable in ap + v = var_of_atom(ap); + // Get bound + bnd = bound_of_atom(ap); + + switch (tag_of_atom(ap)) { + // Assert v-b >= 0 + case GE_ATM: { + if (q_is_zero(bnd)) { + term_t polyTerm; + polyTerm = get_term(solver, v); + result = arith_geq_atom(terms, polyTerm); + } else { + term_t polyTerm; + // Create buffer b = v - bnd + init_rba_buffer(&b, mcarith_solver_pprods(solver)); + rba_buffer_add_mcarithvar(solver, &b, v); + rba_buffer_sub_const(&b, bnd); + // Create term and free buffer. + polyTerm = mcarith_poly(terms, &b); + delete_rba_buffer(&b); + result = arith_geq_atom(terms, polyTerm); + } + break; + } + // Assert v <= b by asserting b-v >= 0 + case LE_ATM: { + term_t polyTerm; + + // Create buffer b = bnd - v + init_rba_buffer(&b, mcarith_solver_pprods(solver)); + rba_buffer_sub_mcarithvar(solver, &b, v); + rba_buffer_add_const(&b, bnd); + polyTerm = mcarith_poly(terms, &b); + delete_rba_buffer(&b); + result = arith_geq_atom(terms, polyTerm); + break; + } + // Assert v == bnd + case EQ_ATM: { + result = arith_bineq_atom(terms, get_term(solver, v), arith_constant(terms, bnd)); + break; + } + default: + longjmp(*solver->simplex.env, INTERNAL_ERROR); + } + solver->atom_terms[atom_index] = result; + return result; +} + +/* + * Create a power of products. + */ +static +thvar_t mcarith_create_pprod(void *s, pprod_t *p, thvar_t *map) { + mcarith_solver_t *solver = s; + term_table_t* terms = mcarith_solver_terms(solver); + + assert(pprod_degree(p) > 1); + assert(!pp_is_empty(p)); + assert(!pp_is_var(p)); + // Create theory variable + thvar_t v = simplex_create_var(&solver->simplex, false); + // Remap variables in powerproduct + mcarith_check_var_size(solver); + pp_buffer_t b; + init_pp_buffer(&b, p->len); + uint32_t n = p->len; + int32_t* vars = safe_malloc(sizeof(int32_t) * n); + uint32_t* exps = safe_malloc(sizeof(uint32_t) * n); + + for (uint32_t i = 0; i < n; ++i) { + thvar_t mv = map[i]; + term_t t; + assert(mv < v); + t = get_term(solver, mv); + vars[i] = t; + exps[i] = p->prod[i].exp; + } + pp_buffer_set_varexps(&b, n, vars, exps); + free(vars); + free(exps); + + assert(solver->var_terms.capacity > v); + + term_t t = pprod_term_from_buffer(terms, &b); + term_ivector_grow_set(&solver->var_terms, v, t); + // Free buffer and return + delete_pp_buffer(&b); + return v; +} + +/* + * Create a divison + */ +static +thvar_t mcarith_create_rdiv(void *s, thvar_t num, thvar_t den) { + mcarith_solver_t *solver; + thvar_t v; + term_t nt; + term_t dt; + + solver = s; + // Create theory variable + v = simplex_create_var(&solver->simplex, false); + + // Assign term + mcarith_check_var_size(solver); + nt = get_term(solver, num); + dt = get_term(solver, den); + term_ivector_grow_set(&solver->var_terms, v, arith_rdiv(mcarith_solver_terms(solver), nt, dt)); + + return v; +} + +/** + * Allocate an assertion for storing on array. + */ +static +mcarith_assertion_t* alloc_top_assertion(mcarith_solver_t* s) { + size_t cnt = s->assertion_count; + if (cnt >= s->assertion_capacity) { + assert(cnt == s->assertion_capacity); + s->assertion_capacity = 2 * s->assertion_capacity; + if (s->assertion_capacity == 0) + out_of_memory(); + s->assertions = safe_realloc(s->assertions, s->assertion_capacity * sizeof(mcarith_assertion_t)); + } + s->assertion_count = cnt + 1; + return s->assertions + cnt; +} + +/******************************** + * SMT AND CONTROL INTERFACES * + *******************************/ + +/* + * This is called before any new atom/variable is created + * (before start_search). + * - we reset the tableau and restore the matrix if needed + */ +void mcarith_start_internalization(mcarith_solver_t *solver) { + simplex_start_internalization(&solver->simplex); +} + +/* + * Start search: + * - simplify the matrix + * - initialize the tableau + * - compute the initial assignment + */ +static void mcarith_start_search(mcarith_solver_t *solver) { + simplex_start_search(&solver->simplex); +} + +/* + * Process all assertions + * - this function may be called before start_search + * - if it's called before start_search, the tableau is not ready + * return true if no conflict is found. + */ +bool mcarith_propagate(mcarith_solver_t *solver) { + return simplex_propagate(&solver->simplex); +} + +/* + * Initializes an rba buffer from a polynomial while translating polynomial variables + * using the var_terms array. + * + * @param pprods Power product table for rba buffer. + * @param b Buffer to initialize + * @param p Polynomial to initialize + * @param var_terms Variable term array used to map from polynomial variables to terms. + * @param var_count Size of var_terms array + */ +static +void init_rba_buffer_from_poly(mcarith_solver_t* solver, + rba_buffer_t* b, + polynomial_t* p) { + init_rba_buffer(b, mcarith_solver_pprods(solver)); + uint32_t n = p->nterms; + for (uint32_t j = 0; j < n; ++j) { + if (j == 0 && p->mono[j].var == const_idx) { + rba_buffer_add_const(b, &p->mono[j].coeff); + } else { + rational_t* c = &p->mono[j].coeff; + thvar_t v = p->mono[j].var; + rba_buffer_add_mono_mcarithvar(solver, b, c, v); + } + } +} + +static +bool rba_buffer_get_const(rba_buffer_t* b, rational_t* r) { + if (b->nterms == 0) { + q_init(r); + return true; + } else if (b->nterms == 1) { + mono_t* m = b->mono + b->root; + if (m->prod == empty_pp) { + q_init(r); + q_set(r, &m->coeff); + return true; + } + } + return false; +} + +/** + * Create term equivalent to mcarith_assertion for MCSAT. + */ +static +term_t mk_assertion_pred(mcarith_solver_t *solver, mcarith_assertion_t* a) { + term_t t; + term_table_t* terms; + rba_buffer_t b; + rational_t br; + term_t p; + terms = mcarith_solver_terms(solver); + switch (a->type) { + case VAR_EQ: + return arith_bineq_atom(terms, + get_term(solver, a->def.eq.lhs), + get_term(solver, a->def.eq.rhs)); + case VAR_EQ0: + return arith_eq_atom(terms, get_term(solver, a->def.var)); + case VAR_GE0: + t = get_term(solver, a->def.var); + assert(term_kind(terms, t) != ARITH_CONSTANT); + return arith_geq_atom(terms, t); + case POLY_EQ0: + init_rba_buffer_from_poly(solver, &b, a->def.poly); + if (rba_buffer_get_const(&b, &br)) { + p = bool2term(q_is_zero(&br)); + q_clear(&br); + } else { + t = arith_poly(terms, &b); + assert(term_kind(terms, t) != ARITH_CONSTANT); + p = arith_eq_atom(terms, t); + } + delete_rba_buffer(&b); + return p; + case POLY_GE0: + init_rba_buffer_from_poly(solver, &b, a->def.poly); + if (rba_buffer_get_const(&b, &br)) { + p = bool2term(q_is_nonneg(&br)); + q_clear(&br); + } else { + t = arith_poly(terms, &b); + assert(term_kind(terms, t) != ARITH_CONSTANT); + p = arith_geq_atom(terms, t); + } + delete_rba_buffer(&b); + return p; + case ATOM_ASSERT: + return get_atom(solver, a->def.atom); + default: + longjmp(*solver->simplex.env, INTERNAL_ERROR); + } +} + +/* + * Cleanup and return final check conflict + * + * Note. This should be updated to derive conflict clause from mcsat information. + */ +static +fcheck_code_t final_check_conflict(mcarith_solver_t* solver) { + ivector_t* conflict = &solver->simplex.expl_vector; + uint32_t acnt = solver->assertion_count; + // Add negation of all clauses with literal set. + for (size_t i = 0; i < acnt; ++i) { + mcarith_assertion_t* a = solver->assertions + i; + if (a->lit != null_literal) { + assert(literal_value(solver->simplex.core, a->lit) == VAL_TRUE); + ivector_push(conflict, not(a->lit)); + } + } + ivector_push(conflict, end_clause); + // Record conflict data with solver. + record_theory_conflict(solver->simplex.core, conflict->data); + // Free mcsat solver + mcarith_free_mcsat(solver); + return FCHECK_CONTINUE; +} + +/* + * Check for integer feasibility + */ +static +fcheck_code_t mcarith_final_check(void* s) { + mcarith_solver_t *solver; + term_table_t* terms; + fcheck_code_t simplex_result; + + // Conflict clause + ivector_t* conflict; + + // Initialize variables + solver = s; + terms = mcarith_solver_terms(solver); + + assert(!solver->simplex.unsat_before_search); + + + simplex_result = simplex_final_check(&solver->simplex); + if (simplex_result == FCHECK_CONTINUE) return FCHECK_CONTINUE; + + mcarith_free_mcsat(solver); + + const bool qflag = false; // Quantifiers not allowed + init_context(&solver->mcsat_ctx, terms, QF_NRA, CTX_MODE_ONECHECK, CTX_ARCH_MCSAT, qflag); + solver->mcsat = mcsat_new(&solver->mcsat_ctx); + + ivector_reset(&solver->mcsat_assertions); + + mcarith_check_var_size(solver); + for (size_t i = 0; i < solver->assertion_count; ++i) { + mcarith_assertion_t* a = solver->assertions + i; + + term_t p = mk_assertion_pred(solver, a); + ivector_push(&solver->mcsat_assertions, a->tt ? p : not_term(terms, p)); + } + + int32_t r = mcsat_assert_formulas(solver->mcsat, solver->mcsat_assertions.size, solver->mcsat_assertions.data); + if (r == TRIVIALLY_UNSAT) { + return final_check_conflict(solver); + } else if (r == CTX_NO_ERROR) { + mcsat_solve(solver->mcsat, 0, 0, 0, 0); + switch (mcsat_status(solver->mcsat)) { + case STATUS_UNKNOWN: + mcarith_free_mcsat(solver); + return FCHECK_UNKNOWN; + case STATUS_SAT: + return FCHECK_SAT; + case STATUS_UNSAT: + return final_check_conflict(solver); + case STATUS_IDLE: + case STATUS_SEARCHING: + case STATUS_INTERRUPTED: + case STATUS_ERROR: + default: + mcarith_free_mcsat(solver); + longjmp(*solver->simplex.env, INTERNAL_ERROR); + } + } else { + mcarith_free_mcsat(solver); + longjmp(*solver->simplex.env, INTERNAL_ERROR); + } + +} + +/* + * Free assertions added since undo record was created. + */ +static +void mcarith_backtrack_assertions(mcarith_solver_t* solver, uint32_t assertion_count) { + assert(assertion_count <= solver->assertion_count); + for (uint32_t i = assertion_count; i != solver->assertion_count; ++i) { + free_mcarith_assertion(solver->assertions + i); + } + solver->assertion_count = assertion_count; +} + +/* + * Increase dlevel in simplex and eqprop + */ +void mcarith_increase_decision_level(mcarith_solver_t *solver) { + simplex_increase_decision_level(&solver->simplex); + mcarith_undo_push_record(&solver->undo_stack, solver->assertion_count); +} + +/* + * Full backtrack + */ +void mcarith_backtrack(mcarith_solver_t *solver, uint32_t back_level) { + mcarith_undo_record_t* r = mcarith_undo_backtrack(&solver->undo_stack, back_level); + mcarith_backtrack_assertions(solver, r->n_assertions); + uint32_t vc = solver->simplex.vtbl.nvars; + simplex_backtrack(&solver->simplex, back_level); + (void)vc; // SUPPRESS unused variable warning in release builds. + assert(vc == solver->simplex.vtbl.nvars); +} + +/* + * Start a new base level + */ +static void mcarith_push(mcarith_solver_t *solver) { + simplex_push(&solver->simplex); + mcarith_undo_push_record(&solver->undo_stack, solver->assertion_count); +} + +/* + * Return to the previous base level + */ +void mcarith_pop(mcarith_solver_t *solver) { + uint32_t vc; + mcarith_undo_record_t* r; + // Reset assertions + r = mcarith_undo_pop_record(&solver->undo_stack); + mcarith_backtrack_assertions(solver, r->n_assertions); + // Pop simplex state + vc = solver->simplex.vtbl.nvars; + simplex_pop(&solver->simplex); + ivector_shrink(&solver->var_terms, solver->simplex.vtbl.nvars); +} + +/* + * Reset to the empty solver + */ +void mcarith_reset(mcarith_solver_t *solver) { + uint32_t vc = solver->simplex.vtbl.nvars; + simplex_reset(&solver->simplex); + assert(vc == solver->simplex.vtbl.nvars); // FIXME + + mcarith_undo_reset(&solver->undo_stack); + mcarith_backtrack_assertions(solver, 0); +} + +/* + * Clear: nothing to clear. + */ +void mcarith_clear(mcarith_solver_t *solver) { +} + +static th_ctrl_interface_t mcarith_control = { + .start_internalization = (start_intern_fun_t) mcarith_start_internalization, + .start_search = (start_fun_t) mcarith_start_search, + .propagate = (propagate_fun_t) mcarith_propagate, + .final_check = mcarith_final_check, + .increase_decision_level = (increase_level_fun_t) mcarith_increase_decision_level, + .backtrack = (backtrack_fun_t) mcarith_backtrack, + .push = (push_fun_t) mcarith_push, + .pop = (pop_fun_t) mcarith_pop, + .reset = (reset_fun_t) mcarith_reset, + .clear = (clear_fun_t) mcarith_clear, +}; + +/* + * Assert atom attached to literal l + * This function is called when l is assigned to true by the core + * - atom is the atom attached to a boolean variable v = var_of(l) + * - if l is positive (i.e., pos_lit(v)), assert the atom + * - if l is negative (i.e., neg_lit(v)), assert its negation + * Return false if that causes a conflict, true otherwise. + * + * Do nothing (although we could try more simplification if + * this is called before start_search). + */ +bool mcarith_assert_atom(mcarith_solver_t *solver, void *atom_pointer, literal_t l) { + bool r = simplex_assert_atom(&solver->simplex, atom_pointer, l); + if (!r) return false; + + simplex_solver_t* simplex = &solver->simplex; + arith_atomtable_t *atbl = &simplex->atbl; + + // Get atom index from pointer + int32_t atom_index = arithatom_tagged_ptr2idx(atom_pointer); + assert(0 <= atom_index && atom_index < atbl->natoms); + + assert(boolvar_of_atom(atbl->atoms + atom_index) == var_of(l)); + + mcarith_assertion_t* assert = alloc_top_assertion(solver); + assert->type = ATOM_ASSERT; + assert->def.atom = atom_index; + assert->tt = is_pos(l); + assert->lit = l; + return true; +} + +/* + * Expand a propagation object into a conjunction of literals + * - expl is a pointer to a propagation object in solver->arena + */ +void mcarith_expand_explanation(mcarith_solver_t *solver, literal_t l, void *expl, ivector_t *v) { + simplex_expand_explanation(&solver->simplex, l, expl, v); +} + +/* + * Return l or (not l) + * - a = atom attached to l = mcarith atom index packed in a void* pointer + */ +literal_t mcarith_select_polarity(mcarith_solver_t *solver, void *a, literal_t l) { + return simplex_select_polarity(&solver->simplex, a, l); +} + +static th_smt_interface_t mcarith_smt = { + .assert_atom = (assert_fun_t) mcarith_assert_atom, + .expand_explanation = (expand_expl_fun_t) mcarith_expand_explanation, + .select_polarity = (select_pol_fun_t) mcarith_select_polarity, + .delete_atom = NULL, + .end_atom_deletion = NULL, +}; + +static const uint32_t theory_var_verb = 5; + +static +thvar_t mcarith_create_const(void* s, rational_t *q) { + mcarith_solver_t *solver; + + solver = s; + return simplex_create_const(&solver->simplex, q); +} + +/* + * Create a theory variable equal to p + * - arith_map maps variables of p to corresponding theory variables + * in the solver + */ +static +thvar_t mcarith_create_poly(void* s, polynomial_t *p, thvar_t *map) { + mcarith_solver_t *solver; + + solver = s; + return simplex_create_poly(&solver->simplex, p, map); +} + +typedef struct{ + uint32_t bstack_top; + uint32_t matrix_nrows; +} simplex_assertion_count_t; + +static simplex_assertion_count_t simplex_assertion_count(simplex_solver_t* simplex) { + simplex_assertion_count_t r; + r.bstack_top = simplex->bstack.top; + r.matrix_nrows = simplex->matrix.nrows; + return r; +} + +/** + * Returns true if the simplex solver concluded the assertion just added did not + * need to get recorded as it was true or false from previous assertions. + */ +static bool simplex_handled_assertion(simplex_solver_t* simplex, simplex_assertion_count_t c) { + return simplex->unsat_before_search + || (simplex->matrix.nrows == c.matrix_nrows && simplex->bstack.top == c.bstack_top); +} + +/* + * Assert a top-level equality constraint (either x == 0 or x != 0) + * - tt indicates whether the constraint or its negation must be asserted + * tt == true --> assert x == 0 + * tt == false --> assert x != 0 + */ +static void mcarith_assert_eq_axiom(void* s, thvar_t x, bool tt) { + mcarith_solver_t *solver; + mcarith_assertion_t* assert; + + solver = s; + // Get number of assertions + simplex_assertion_count_t cinit = simplex_assertion_count(&solver->simplex); + simplex_assert_eq_axiom(&solver->simplex, x, tt); + if (simplex_handled_assertion(&solver->simplex, cinit)) + return; + + // Record assertion for sending to mcarith solver. + assert = alloc_top_assertion(solver); + assert->type = VAR_EQ0; + assert->def.var = x; + assert->tt = tt; + assert->lit = null_literal; +} + +/* + * Assert a top-level inequality (either x >= 0 or x < 0) + * - tt indicates whether the constraint or its negation must be asserted + * tt == true --> assert x >= 0 + * tt == false --> assert x < 0 + */ +static void mcarith_assert_ge_axiom(void* s, thvar_t x, bool tt){ + mcarith_solver_t *solver; + mcarith_assertion_t* assert; + + solver = s; + // Get number of assertions + simplex_assertion_count_t cinit = simplex_assertion_count(&solver->simplex); + simplex_assert_ge_axiom(&solver->simplex, x, tt); + if (simplex_handled_assertion(&solver->simplex, cinit)) + return; + + assert = alloc_top_assertion(solver); + assert->type = VAR_GE0; + assert->def.var = x; + assert->tt = tt; + assert->lit = null_literal; +} + +/* + * Assert top-level equality or disequality (either p == 0 or p != 0) + * - map: convert p's variables to mcarith variables + * - if tt is true ---> assert p == 0 + * - if tt is false ---> assert p != 0 + */ +static void mcarith_assert_poly_eq_axiom(void * s, polynomial_t *p, thvar_t *map, bool tt) { + mcarith_solver_t *solver; + mcarith_assertion_t* assert; + + solver = s; + assert(p->nterms > 0); + + simplex_assertion_count_t cinit = simplex_assertion_count(&solver->simplex); + simplex_assert_poly_eq_axiom(&solver->simplex, p, map, tt); + if (simplex_handled_assertion(&solver->simplex, cinit)) + return; + + assert = alloc_top_assertion(solver); + assert->type = POLY_EQ0; + assert(p->nterms > 0); + assert(p->nterms > 1 || p->mono[0].var != const_idx); + assert->def.poly = alloc_polynomial_from_map(p, map, solver->simplex.vtbl.nvars); + assert->tt = tt; + assert->lit = null_literal; +} + +/* + * Assert a top-level inequality that p >= 0 is true or false. + * - map: an array that maps the `i`th variable in `p` to the mcarith theory variable. + * - tt indicates if `p >= 0` is asserted be true or false. + */ +static void mcarith_assert_poly_ge_axiom(void *s, polynomial_t *p, thvar_t *map, bool tt) { + mcarith_solver_t *solver; + mcarith_assertion_t* assert; + + solver = s; + assert(p->nterms > 0); + + simplex_assertion_count_t cinit = simplex_assertion_count(&solver->simplex); + simplex_assert_poly_ge_axiom(&solver->simplex, p, map, tt); + if (simplex_handled_assertion(&solver->simplex, cinit)) + return; + + assert = alloc_top_assertion(solver); + assert->type = POLY_GE0; + assert(p->nterms > 0); + assert(p->nterms > 1 || p->mono[0].var != const_idx); + assert->def.poly = alloc_polynomial_from_map(p, map, solver->simplex.vtbl.nvars); + assert->tt = tt; + assert->lit = null_literal; +} + +/* + * If tt == true --> assert (x - y == 0) + * If tt == false --> assert (x - y != 0) + */ +static +void mcarith_assert_vareq_axiom(void* s, thvar_t x, thvar_t y, bool tt) { + mcarith_solver_t *solver; + mcarith_assertion_t* assert; + + solver = s; + simplex_assertion_count_t cinit = simplex_assertion_count(&solver->simplex); + simplex_assert_vareq_axiom(&solver->simplex, x, y, tt); + if (simplex_handled_assertion(&solver->simplex, cinit)) + return; + + assert = alloc_top_assertion(solver); + assert->type = VAR_EQ; + assert->def.eq.lhs = x; + assert->def.eq.rhs = y; + assert->tt = tt; + assert->lit = null_literal; +} + +/* + * Assert (c ==> x == y) + */ +static +void mcarith_assert_cond_vareq_axiom(void* s, literal_t c, thvar_t x, thvar_t y) { + mcarith_solver_t *solver; + solver = s; + simplex_assertion_count_t cinit = simplex_assertion_count(&solver->simplex); + simplex_assert_cond_vareq_axiom(&solver->simplex, c, x, y); + if (simplex_handled_assertion(&solver->simplex, cinit)) + return; + + assert(false); +} + +/* + * Assert (c[0] \/ ... \/ c[n-1] \/ x == y) + */ +static +void mcarith_assert_clause_vareq_axiom(void* s, uint32_t n, literal_t *c, thvar_t x, thvar_t y) { + mcarith_solver_t *solver = s; + simplex_assertion_count_t cinit = simplex_assertion_count(&solver->simplex); + simplex_assert_clause_vareq_axiom(&solver->simplex, n, c, x, y); + if (simplex_handled_assertion(&solver->simplex, cinit)) + return; + + assert(false); +} + +/* + * Get the type of variable x + */ +static +bool mcarith_var_is_integer(void* s, thvar_t x) { + mcarith_solver_t *solver = s; + return arith_var_is_int(&solver->simplex.vtbl, x); +} + +#pragma region Models + +/* + * Model construction + */ +static void mcarith_build_model(void* s) { + mcarith_solver_t* solver = s; + + model_t *model; + assert(solver->mcsat); + assert(!solver->model); + // Create model + model = safe_malloc(sizeof(model_t)); + init_model(model, mcarith_solver_terms(solver), true); + mcsat_build_model(solver->mcsat, model); + solver->model = model; + + mcarith_free_mcsat(solver); +} + +/* + * This tries to return the value associated with the variable x in the model. + * If x has a value, then this returns true and sets v. If not, then it returns + * false. + */ +static +bool mcarith_value_in_model(void* s, thvar_t x, arithval_in_model_t* res) { + mcarith_solver_t* solver; + term_t t; + model_t* mdl; + value_t v; + value_table_t* vtbl; + + assert(res->tag == ARITHVAL_RATIONAL); + + solver = s; + t = solver->var_terms.data[x]; + if (t == NULL_TERM) + return false; + + mdl = solver->model; + assert(mdl); + + v = model_get_term_value(mdl, t); + if (v < 0) { + return false; + } + + vtbl = model_get_vtbl(mdl); + if (object_is_rational(vtbl, v)) { + q_set(&res->val.q, vtbl_rational(vtbl, v)); + return true; + } else if (object_is_algebraic(vtbl, v)) { + lp_algebraic_number_t* n = vtbl_algebraic_number(vtbl, v); + q_clear(&res->val.q); + res->tag = ARITHVAL_ALGEBRAIC; + lp_algebraic_number_construct_copy(&res->val.alg_number, n); + return true; + } + + // Should not happen. + return false; +} + +#pragma endregion Models + +/****************************** + * INTERFACE TO THE CONTEXT * + *****************************/ + +static arith_interface_t mcarith_context = { + .create_var = (create_arith_var_fun_t) simplex_create_var, + .create_const = mcarith_create_const, + .create_poly = mcarith_create_poly, + .create_pprod = mcarith_create_pprod, + .create_rdiv = mcarith_create_rdiv, + + .create_eq_atom = (create_arith_atom_fun_t) simplex_create_eq_atom, + .create_ge_atom = (create_arith_atom_fun_t) simplex_create_ge_atom, + .create_poly_eq_atom = (create_arith_patom_fun_t) simplex_create_poly_eq_atom, + .create_poly_ge_atom = (create_arith_patom_fun_t) simplex_create_poly_ge_atom, + .create_vareq_atom = (create_arith_vareq_atom_fun_t) simplex_create_vareq_atom, + + .assert_eq_axiom = mcarith_assert_eq_axiom, + .assert_ge_axiom = mcarith_assert_ge_axiom, + .assert_poly_eq_axiom = mcarith_assert_poly_eq_axiom, + .assert_poly_ge_axiom = mcarith_assert_poly_ge_axiom, + .assert_vareq_axiom = mcarith_assert_vareq_axiom, + .assert_cond_vareq_axiom = mcarith_assert_cond_vareq_axiom, + .assert_clause_vareq_axiom = mcarith_assert_clause_vareq_axiom, + + .attach_eterm = (attach_eterm_fun_t) simplex_attach_eterm, + .eterm_of_var = (eterm_of_var_fun_t) simplex_eterm_of_var, + + .build_model = mcarith_build_model, + .free_model = mcarith_free_model, + .value_in_model = mcarith_value_in_model, + + .arith_var_is_int = mcarith_var_is_integer, +}; + +/* + * Return the interface descriptor + */ +arith_interface_t *mcarith_arith_interface(mcarith_solver_t *solver) { + return &mcarith_context; +} + +/* + * Get the control and smt interfaces + */ +th_ctrl_interface_t *mcarith_ctrl_interface(mcarith_solver_t *solver) { + return &mcarith_control; +} + +th_smt_interface_t *mcarith_smt_interface(mcarith_solver_t *solver) { + return &mcarith_smt; +} +#endif \ No newline at end of file diff --git a/src/solvers/mcarith/mcarith.h b/src/solvers/mcarith/mcarith.h new file mode 100644 index 000000000..040eb1d7e --- /dev/null +++ b/src/solvers/mcarith/mcarith.h @@ -0,0 +1,69 @@ +/* + * 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 . + */ +#ifdef HAVE_MCSAT +#ifndef __MCARITH_H +#define __MCARITH_H + +#include +//#include +//#include +//#include + +typedef struct mcarith_solver_s mcarith_solver_t; + +/* + * Initialize the mcarith solver. + * - core = the attached smt-core object + * - gates = the gate manager for core + * - egraph = the attached egraph (or NULL) + * + * Default settings: + * - no row saving, no jump buffer (exceptions cause abort) + */ +extern void init_mcarith_solver(mcarith_solver_t **solver, context_t* ctx); + +/* + * Enable row saving (to support push/pop/multiple checks) + * - must be done before any assertions + */ +void mcarith_enable_row_saving(mcarith_solver_t *solver); + +/** + * + */ +extern void destroy_mcarith_solver(mcarith_solver_t* solver); + +/* + * Get the internalization interface descriptor + */ +extern arith_interface_t *mcarith_arith_interface(mcarith_solver_t *solver); + +/* + * Get the solver descriptors + */ +extern th_ctrl_interface_t *mcarith_ctrl_interface(mcarith_solver_t *solver); +extern th_smt_interface_t *mcarith_smt_interface(mcarith_solver_t *solver); + +/* + * Get the egraph interface descriptors + */ +extern th_egraph_interface_t *mcarith_egraph_interface(mcarith_solver_t *solver); +extern arith_egraph_interface_t *mcarith_arith_egraph_interface(mcarith_solver_t *solver); + +#endif +#endif \ No newline at end of file diff --git a/src/solvers/simplex/simplex.c b/src/solvers/simplex/simplex.c index 32a17a522..d974b3b45 100644 --- a/src/solvers/simplex/simplex.c +++ b/src/solvers/simplex/simplex.c @@ -2854,6 +2854,15 @@ thvar_t simplex_create_pprod(simplex_solver_t *solver, pprod_t *p, thvar_t *map) abort(); } +/* + * Placeholder for a division. + */ +thvar_t simplex_create_rdiv(simplex_solver_t *solver, thvar_t num, thvar_t den) { + if (solver->env != NULL) { + longjmp(*solver->env, FORMULA_NOT_LINEAR); + } + abort(); +} /* * Attach egraph term t to a variable v @@ -10122,7 +10131,7 @@ fcheck_code_t simplex_final_check(simplex_solver_t *solver) { /* - * Clear: nothing to to + * Clear: nothing to clear. */ void simplex_clear(simplex_solver_t *solver) { } @@ -12665,9 +12674,10 @@ void simplex_free_model(simplex_solver_t *solver) { /* * Value of variable x in the model */ -bool simplex_value_in_model(simplex_solver_t *solver, int32_t x, rational_t *v) { +bool simplex_value_in_model(simplex_solver_t *solver, int32_t x, arithval_in_model_t* res) { assert(solver->value != NULL && 0 <= x && x < solver->vtbl.nvars); - q_set(v, solver->value + x); + assert(res->tag == ARITHVAL_RATIONAL); + q_set(&res->val.q, solver->value + x); return true; } @@ -12706,6 +12716,7 @@ static arith_interface_t simplex_context = { (create_arith_const_fun_t) simplex_create_const, (create_arith_poly_fun_t) simplex_create_poly, (create_arith_pprod_fun_t) simplex_create_pprod, + (create_arith_rdiv_fun_t) simplex_create_rdiv, (create_arith_atom_fun_t) simplex_create_eq_atom, (create_arith_atom_fun_t) simplex_create_ge_atom, diff --git a/src/solvers/simplex/simplex.h b/src/solvers/simplex/simplex.h index 9a9d4be81..d5bb5b801 100644 --- a/src/solvers/simplex/simplex.h +++ b/src/solvers/simplex/simplex.h @@ -312,7 +312,7 @@ extern void simplex_assert_cond_vareq_axiom(simplex_solver_t *solver, literal_t extern void simplex_start_search(simplex_solver_t *solver); /* - * Stop the search: sets flag solver->interrupted to true and + * Stop the search: sets flag solver->interrupted to true and * stops the diophantine solver if it's active. * - the solver->interrupted flag is set to false by start_search * - currently, the interrupted flag is checked in every iteration @@ -395,7 +395,7 @@ extern void simplex_reset(simplex_solver_t *solver); * Model construction */ extern void simplex_build_model(simplex_solver_t *solver); -extern bool simplex_value_in_model(simplex_solver_t *solver, int32_t x, rational_t *v); +extern bool simplex_value_in_model(simplex_solver_t *solver, int32_t x, arithval_in_model_t* res); extern void simplex_free_model(simplex_solver_t *solver);