From 517ad92922ae05b00a84c4bbb189a9197bba63cf Mon Sep 17 00:00:00 2001 From: Joe Hendrix Date: Wed, 10 Nov 2021 12:23:13 -0800 Subject: [PATCH 01/10] Initial mcarith work-in-progress theory solver. --- Makefile.build | 3 +- src/Makefile | 2 + src/api/context_config.c | 2 +- src/context/context.c | 54 +- src/context/context_types.h | 5 +- src/frontend/yices_smt2_lc.c | 1128 +++++++++++++++++++++++++++++++++ src/solvers/mcarith/mcarith.c | 824 ++++++++++++++++++++++++ src/solvers/mcarith/mcarith.h | 63 ++ 8 files changed, 2072 insertions(+), 9 deletions(-) create mode 100644 src/frontend/yices_smt2_lc.c create mode 100644 src/solvers/mcarith/mcarith.c create mode 100644 src/solvers/mcarith/mcarith.h 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..fab69210b 100644 --- a/src/api/context_config.c +++ b/src/api/context_config.c @@ -181,7 +181,7 @@ 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_MCSATARITH, // QF_NRA CTX_ARCH_MCSAT, // QF_NIRA CTX_ARCH_SPLX, // QF_RDL CTX_ARCH_EG, // QF_UF diff --git a/src/context/context.c b/src/context/context.c index 7b7ec2d20..a89f5a8d0 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" @@ -4961,7 +4962,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 +4981,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 +5002,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 +5174,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 +5335,44 @@ 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. + */ +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) { + longjmp(ctx->env, INTERNAL_ERROR); + +// simplex_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); +} + /* * Create IDL/SIMPLEX solver based on ctx->dl_profile @@ -5511,7 +5553,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 +5650,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 diff --git a/src/context/context_types.h b/src/context/context_types.h index b1e5775ea..667e923cd 100644 --- a/src/context/context_types.h +++ b/src/context/context_types.h @@ -190,11 +190,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) /* 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/solvers/mcarith/mcarith.c b/src/solvers/mcarith/mcarith.c new file mode 100644 index 000000000..ba95780af --- /dev/null +++ b/src/solvers/mcarith/mcarith.c @@ -0,0 +1,824 @@ +/* + * 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. + */ + +#include "context/context.h" +#include "solvers/mcarith/mcarith.h" +#include "solvers/simplex/simplex.h" + +#include "mcsat/trail.h" +#include "mcsat/variable_db.h" + +/** + * Initialize b from a power product with variables translated by map. + */ +static +void init_pp_buffer_from_pprod_map(pp_buffer_t* b, pprod_t* p, int32_t* map, size_t map_size) { + init_pp_buffer(b, p->len); + for (uint32_t i = 0; i < p->len; ++i) { + varexp_t* v = p->prod + i; + assert(v->var < map_size); + pp_buffer_set_varexp(b, map[v->var], v->exp); + } + pp_buffer_normalize(b); +} + +/** + * Initialize b from a power product with variables translated by map. + */ +static +void init_pp_buffer_from_index_pprod_map(pp_buffer_t* b, pprod_t* p, int32_t* map, size_t map_size) { + init_pp_buffer(b, p->len); + for (uint32_t i = 0; i < p->len; ++i) { + varexp_t* v = p->prod + i; + assert(v->var < map_size); + pp_buffer_set_varexp(b, map[v->var], v->exp); + } + pp_buffer_normalize(b); +} + +/** + * 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_POLY }; + +struct mcarith_var_s { + enum mcarith_var_type type; + union { + pprod_t* prod; + } def; +}; + +typedef struct mcarith_var_s mcarith_var_t; + + +enum mcarith_assertion_type { VAR_EQ, POLY_EQ, POLY_GE }; + +struct mcarith_assertion_s { + // Indicates the type of the assertion. + enum mcarith_assertion_type type; + // A polynomial over theory variables. + union { + polynomial_t* poly; + struct { thvar_t lhs; thvar_t rhs } eq; + } 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; +}; + +typedef struct mcarith_assertion_s mcarith_assertion_t; + +struct mcarith_solver_s { + simplex_solver_t simplex; + // const context_t* ctx; + + // Variable definitions + + // Information about theory variables. + mcarith_var_t* vars; + + // Assertion array + mcarith_assertion_t* assertions; + size_t assertion_capacity; + size_t assertion_count; +}; + +/* + * Initialize a mcarith solver + */ +void init_mcarith_solver(mcarith_solver_t **solver, context_t* ctx) { + const size_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->assertions = safe_malloc(init_assertion_capacity * sizeof(mcarith_assertion_t)); + s->assertion_capacity = init_assertion_capacity; + s->assertion_count = 0; + s->vars = safe_malloc(sizeof(mcarith_var_t) * s->simplex.vtbl.size); + *solver = s; +} + +void destroy_mcarith_solver(mcarith_solver_t* s) { + // Free vars + uint32_t vc = s->simplex.vtbl.nvars; + for (uint32_t i = 0; i != vc; ++i) { + switch (s->vars[i].type) { + case VAR_POLY: + free_pprod(s->vars[i].def.prod); + break; + default: + break; + } + } + safe_free(s->vars); + // Free assertions + safe_free(s->assertions); + // Free solver + delete_simplex_solver(&s->simplex); + // Free solver itself + safe_free(s); +} + +/* + * Create a new theory variable + * - is_int indicates whether the variable should be an integer. + */ +static +thvar_t mcarith_create_var_internal(mcarith_solver_t *solver, bool is_int) { + uint32_t init_size = solver->simplex.vtbl.size; + + thvar_t v = simplex_create_var(&solver->simplex, is_int); + + uint32_t new_size = solver->simplex.vtbl.size; + if (new_size > init_size) { + solver->vars = safe_realloc(solver->vars, sizeof(mcarith_var_t) * new_size); + } + assert(v < new_size); + return v; +} + +/* + * Create a new theory variable + * - is_int indicates whether the variable should be an integer + * - also add a matrix column + */ +static +thvar_t mcarith_create_var(mcarith_solver_t *solver, bool is_int) { + thvar_t v = mcarith_create_var_internal(solver, is_int); + solver->vars[v].type = VAR_FREE; + return v; +} + +/** + * Allocate an assertion for storing on array. + */ +static +mcarith_assertion_t* alloc_assertion(mcarith_solver_t* s) { + size_t cnt = s->assertion_count; + if (cnt < s->assertion_capacity) { + ++s->assertion_count; + return s->assertions + cnt; + } else { + assert(cnt == s->assertion_capacity); + assert(s->assertion_capacity > 0); + s->assertion_capacity = 2 * s->assertion_capacity; + s->assertions = safe_realloc(s->assertions, s->assertion_capacity * sizeof(mcarith_assertion_t)); + 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_reset_tableau(solver); +// simplex_restore_matrix(solver); +// assert(solver->matrix_ready && ! solver->tableau_ready); +} + +/* + * Start search: + * - simplify the matrix + * - initialize the tableau + * - compute the initial assignment + */ +void mcarith_start_search(mcarith_solver_t *solver) { +// assert(0); //FIXME + +} + +/* + * 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 true; +} + +static +void init_rba_buffer_from_poly(rba_buffer_t* b, pprod_table_t* pprods, + polynomial_t* p, + term_t* var_terms, int32_t var_count) { + init_rba_buffer(b, pprods); + 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 { + assert(0 <= p->mono[j].var && p->mono[j].var < var_count); + pprod_t* pp = var_pp(var_terms[p->mono[j].var]); + rba_buffer_add_mono(b, &p->mono[j].coeff, pp); + } + } +} + +/* + * Check for integer feasibility + */ +static +fcheck_code_t mcarith_final_check(mcarith_solver_t *solver) { + type_table_t types; + init_type_table(&types, 64); + type_t itype = int_type(&types); + type_t rtype = real_type(&types); + + // Initialize power product table. + pprod_table_t pprods; + init_pprod_table(&pprods, 0); // Use default size + + // Initialize term table + term_table_t terms; + const uint32_t init_termtable_size = 1024; + + // Var table for arithmetic + arith_vartable_t* vtbl = &solver->simplex.vtbl; + + uint32_t vc = num_arith_vars(vtbl); + init_term_table(&terms, init_termtable_size, &types, &pprods); + + context_t ctx; + const bool qflag = false; // Quantifiers not allowed + init_context(&ctx, &terms, QF_NRA, CTX_MODE_ONECHECK, CTX_ARCH_MCSAT, qflag); + + // Create array for mapping theory variables to initial term. + term_t* var_terms = safe_malloc(vc * sizeof(term_t)); + // The variable denotes the constant one. + rational_t one; + q_set_one(&one); + var_terms[0] = arith_constant(&terms, &one); + // Allow variables/terms for later variables. + for (uint32_t i = 1; i < vc; ++i) { + bool is_int; + pp_buffer_t b; + + switch (solver->vars[i].type) { + case VAR_FREE: + is_int = arith_var_is_int(vtbl, i); + var_terms[i] = new_uninterpreted_term(&terms, is_int ? itype : rtype); + break; + case VAR_POLY: + init_pp_buffer_from_pprod_map(&b, solver->vars[i].def.prod, var_terms, i); + var_terms[i] = pprod_term_from_buffer(&terms, &b); + break; + default: + assert(false); + } + } + + mcsat_solver_t* mcsat = mcsat_new(&ctx); + + term_t* assertions = safe_malloc(sizeof(term_t) * solver->assertion_count); + literal_t* literals = safe_malloc(sizeof(literal_t) * solver->assertion_count + 1); + size_t literal_count = 0; + for (size_t i = 0; i < solver->assertion_count; ++i) { + mcarith_assertion_t* a = solver->assertions + i; + + + rba_buffer_t b; + term_t p; + switch (a->type) { + case VAR_EQ: + p = eq_term(&terms, var_terms[a->def.eq.lhs], var_terms[a->def.eq.rhs]); + break; + case POLY_EQ: + init_rba_buffer_from_poly(&b, &pprods, a->def.poly, var_terms, vc); + p = arith_eq_atom(&terms, arith_poly(&terms, &b)); + delete_rba_buffer(&b); + break; + case POLY_GE: + init_rba_buffer_from_poly(&b, &pprods, a->def.poly, var_terms, vc); + p = arith_geq_atom(&terms, arith_poly(&terms, &b)); + delete_rba_buffer(&b); + break; + default: + longjmp(*solver->simplex.env, INTERNAL_ERROR); + } + if (a->lit != null_literal) { + literals[literal_count++] = a->lit; + } + assertions[i] = a->tt ? p : not_term(&terms, p); + } + literals[literal_count] = end_clause; + + + int32_t r = mcsat_assert_formulas(mcsat, solver->assertion_count, assertions); + fcheck_code_t result; + if (r == TRIVIALLY_UNSAT) { + record_theory_conflict(solver->simplex.core, literals); + result = FCHECK_CONTINUE; + } else if (r == CTX_NO_ERROR) { + result = FCHECK_SAT; + mcsat_solve(mcsat, 0, 0, 0, 0); + switch (mcsat_status(mcsat)) { + case STATUS_UNKNOWN: + safe_free(literals); + result = FCHECK_UNKNOWN; + break; + case STATUS_SAT: + safe_free(literals); + result = FCHECK_SAT; + break; + case STATUS_UNSAT: + // TODO: + // - record a conflict (by calling record_theory_conflict) + // - create lemmas or atoms in the core + record_theory_conflict(solver->simplex.core, literals); + result = FCHECK_CONTINUE; + break; + case STATUS_IDLE: + case STATUS_SEARCHING: + case STATUS_INTERRUPTED: + case STATUS_ERROR: + default: + safe_free(literals); + longjmp(solver->simplex.env, INTERNAL_ERROR); + break; + } + } else { + safe_free(literals); + longjmp(solver->simplex.env, INTERNAL_ERROR); + } + + mcsat_destruct(mcsat); + safe_free(mcsat); + delete_context(&ctx); + delete_term_table(&terms); + delete_pprod_table(&pprods); + delete_type_table(&types); + return result; +} + +/* + * Increase dlevel in simplex and eqprop + */ +void mcarith_increase_decision_level(mcarith_solver_t *solver) { + assert(0); //FIXME +} + + +/* + * Full backtrack + */ +void mcarith_backtrack(mcarith_solver_t *solver, uint32_t back_level) { +#if TRACE + printf("---> Mcarith: backtracking to level %"PRIu32"\n", back_level); +#endif + assert(0); //FIXME +} + +/* + * Start a new base level + */ +void mcarith_push(mcarith_solver_t *solver) { + assert(0); //FIXME + //mcsat_push(solver->mcsat); +} + +/* + * Return to the previous base level + */ +void mcarith_pop(mcarith_solver_t *solver) { + assert(0); //FIXME + //mcsat_pop(solver->mcsat); +} + +/* + * Reset to the empty solver + */ +void mcarith_reset(mcarith_solver_t *solver) { + assert(0); //FIXME + //mcsat_reset(solver->mcsat); +} + +/* + * Clear: nothing to clear. + */ +void mcarith_clear(mcarith_solver_t *solver) { + assert(0); //FIXME + //mcsat_clear(solver->mcsat); +} + +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 = (final_check_fun_t) 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 *a, literal_t l) { + assert(0); //FIXME + 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) { + assert(false); // This function should not be called. +} + +/* + * 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) { + assert(0); //FIXME + return l; // Do nothing +} + +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, +}; + +/* + * Create a new variable that represents constant q + * - add a matrix column if that's a new variable + */ +thvar_t mcarith_create_const(mcarith_solver_t *solver, rational_t *q) { + assert(0); //FIXME + return 0; // FIXME +} + +/* + * Create a theory variable equal to p + * - arith_map maps variables of p to corresponding theory variables + * in the solver + */ +thvar_t mcarith_create_poly(mcarith_solver_t *solver, polynomial_t *p, thvar_t *map) { + assert(0); //FIXME + return 0; // FIXME +} + + +/* + * Create a power of products. + */ +static +thvar_t mcarith_create_pprod(mcarith_solver_t *solver, pprod_t *p, thvar_t *map) { + assert(pprod_degree(p) > 1); //FIXME + assert(!pp_is_empty(p)); + assert(!pp_is_var(p)); + + // Remap variables in powerproduct + pp_buffer_t b; + init_pp_buffer(&b, p->len); + for (uint32_t i = 0; i < p->len; ++i) { + pp_buffer_set_varexp(&b, map[i], p->prod[i].exp); + } + pp_buffer_normalize(&b); + + // Assign power product + thvar_t v = mcarith_create_var_internal(solver, false); + solver->vars[v].type = VAR_POLY; + solver->vars[v].def.prod = pp_buffer_getprod(&b); + + delete_pp_buffer(&b); + return v; +} + +/* + * Create the atom x == 0 + * - this attach the atom to the smt_core + */ +literal_t mcarith_create_eq_atom(mcarith_solver_t *solver, thvar_t x) { + assert(0); //FIXME + return 0; // FIXME +} + +/* + * Create the atom x >= 0 + * - this attach the atom to the smt_core + */ +literal_t mcarith_create_ge_atom(mcarith_solver_t *solver, thvar_t x) { + assert(0); //FIXME + return 0; // FIXME +} + +/* + * Create the atom p == 0 + * - apply the renaming defined by map + */ +literal_t mcarith_create_poly_eq_atom(mcarith_solver_t *solver, polynomial_t *p, thvar_t *map) { + assert(0); //FIXME + return 0; // FIXME +} + +/* + * Create the atom p >= 0 and return the corresponding literal + * - replace the variables of p as defined by map + */ +literal_t mcarith_create_poly_ge_atom(mcarith_solver_t *solver, polynomial_t *p, thvar_t *map) { + assert(0); //FIXME + return 0; // FIXME +} + +/* + * Create the atom x - y == 0 + * - x and y are two theory variables + */ +literal_t mcarith_create_vareq_atom(mcarith_solver_t *solver, thvar_t x, thvar_t y) { + assert(0); //FIXME + return 0; // FIXME +} + +/* + * 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 + */ +void mcarith_assert_eq_axiom(mcarith_solver_t *solver, thvar_t x, bool tt) { + assert(0); //FIXME + //FIXME +} + +/* + * 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 + */ +void mcarith_assert_ge_axiom(mcarith_solver_t *solver, thvar_t x, bool tt){ + assert(0); //FIXME + //FIXME +} + +/* + * 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 + */ +void mcarith_assert_poly_eq_axiom(mcarith_solver_t *solver, polynomial_t *p, thvar_t *map, bool tt) { + assert(p->nterms > 0); + mcarith_assertion_t* assert = alloc_assertion(solver); + assert->type = POLY_EQ; + 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. + */ +void mcarith_assert_poly_ge_axiom(mcarith_solver_t *solver, polynomial_t *p, thvar_t *map, bool tt) { + assert(p->nterms > 0); + mcarith_assertion_t* assert = alloc_assertion(solver); + assert->type = POLY_GE; + 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) + */ +void mcarith_assert_vareq_axiom(mcarith_solver_t *solver, thvar_t x, thvar_t y, bool tt) { + mcarith_assertion_t* assert = alloc_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) + */ +void mcarith_assert_cond_vareq_axiom(mcarith_solver_t *solver, literal_t c, thvar_t x, thvar_t y) { + assert(0); //FIXME + //FIXME +} + +/* + * Assert (c[0] \/ ... \/ c[n-1] \/ x == y) + */ +void mcarith_assert_clause_vareq_axiom(mcarith_solver_t *solver, uint32_t n, literal_t *c, thvar_t x, thvar_t y) { + assert(0); //FIXME + //FIXME +} + +/* + * Get the type of variable x + */ +bool mcarith_var_is_integer(mcarith_solver_t *solver, thvar_t x) { + return arith_var_is_int(&solver->simplex.vtbl, x); +} + + +extern void simplex_attach_eterm(simplex_solver_t *solver, thvar_t v, eterm_t t); + +/* + * Attach egraph term t to a variable v + * - v must not have an eterm attached already + */ +static void mcarith_attach_eterm(mcarith_solver_t *solver, thvar_t v, eterm_t t) { + simplex_attach_eterm(&solver->simplex, v, t); +} + +extern eterm_t simplex_eterm_of_var(simplex_solver_t *solver, thvar_t v); + +/* + * Get the egraph term t attached to v + * - return null_eterm if v has no eterm attached + */ +static eterm_t mcarith_eterm_of_var(mcarith_solver_t *solver, thvar_t v) { + return simplex_eterm_of_var(&solver->simplex, v); +} + +#pragma region Models + +/* + * Model construction + */ +void mcarith_build_model(mcarith_solver_t *solver) { + // FIXME + printf("mcarith_build_model\n"); +} + +/* + * Free the model + */ +void mcarith_free_model(mcarith_solver_t *solver) { + //FIXME + printf("mcarith_free_model\n"); +} + +/* + * 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. + */ +bool mcarith_value_in_model(mcarith_solver_t *solver, thvar_t x, rational_t *v) { + printf("mcarith_value_in_model\n"); + return false; // FIXME +} + +#pragma endregion Models + +/****************************** + * INTERFACE TO THE CONTEXT * + *****************************/ + +static arith_interface_t mcarith_context = { + .create_var = (create_arith_var_fun_t) mcarith_create_var, + .create_const = (create_arith_const_fun_t) mcarith_create_const, + .create_poly = (create_arith_poly_fun_t) mcarith_create_poly, + .create_pprod = (create_arith_pprod_fun_t) mcarith_create_pprod, + + .create_eq_atom = (create_arith_atom_fun_t) mcarith_create_eq_atom, + .create_ge_atom = (create_arith_atom_fun_t) mcarith_create_ge_atom, + .create_poly_eq_atom = (create_arith_patom_fun_t) mcarith_create_poly_eq_atom, + .create_poly_ge_atom = (create_arith_patom_fun_t) mcarith_create_poly_ge_atom, + .create_vareq_atom = (create_arith_vareq_atom_fun_t) mcarith_create_vareq_atom, + + .assert_eq_axiom = (assert_arith_axiom_fun_t) mcarith_assert_eq_axiom, + .assert_ge_axiom = (assert_arith_axiom_fun_t) mcarith_assert_ge_axiom, + .assert_poly_eq_axiom = (assert_arith_paxiom_fun_t) mcarith_assert_poly_eq_axiom, + .assert_poly_ge_axiom = (assert_arith_paxiom_fun_t) mcarith_assert_poly_ge_axiom, + .assert_vareq_axiom = (assert_arith_vareq_axiom_fun_t) mcarith_assert_vareq_axiom, + .assert_cond_vareq_axiom = (assert_arith_cond_vareq_axiom_fun_t) mcarith_assert_cond_vareq_axiom, + .assert_clause_vareq_axiom = (assert_arith_clause_vareq_axiom_fun_t) mcarith_assert_clause_vareq_axiom, + + .attach_eterm = (attach_eterm_fun_t) mcarith_attach_eterm, + .eterm_of_var = (eterm_of_var_fun_t) mcarith_eterm_of_var, + + .build_model = (build_model_fun_t) mcarith_build_model, + .free_model = (free_model_fun_t) mcarith_free_model, + .value_in_model = (arith_val_in_model_fun_t) mcarith_value_in_model, + + .arith_var_is_int = (arith_var_is_int_fun_t) 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; +} + +/* +static th_egraph_interface_t simplex_egraph = { + (assert_eq_fun_t) simplex_assert_var_eq, + (assert_diseq_fun_t) simplex_assert_var_diseq, + (assert_distinct_fun_t) simplex_assert_var_distinct, + (check_diseq_fun_t) simplex_check_disequality, + (is_constant_fun_t) simplex_var_is_constant, + (expand_eq_exp_fun_t) simplex_expand_th_explanation, + (reconcile_model_fun_t) simplex_reconcile_model, + (prepare_model_fun_t) simplex_prep_model, + (equal_in_model_fun_t) simplex_var_equal_in_model, + (gen_inter_lemma_fun_t) simplex_gen_interface_lemma, + (release_model_fun_t) simplex_release_model, + (build_partition_fun_t) simplex_build_model_partition, + (free_partition_fun_t) simplex_release_model_partition, + (attach_to_var_fun_t) simplex_attach_eterm, + (get_eterm_fun_t) simplex_eterm_of_var, + (select_eq_polarity_fun_t) simplex_select_eq_polarity, +}; + + +static arith_egraph_interface_t simplex_arith_egraph = { + (make_arith_var_fun_t) simplex_create_var, + (arith_val_fun_t) simplex_value_in_model, +}; + + +th_egraph_interface_t *simplex_egraph_interface(simplex_solver_t *solver) { + return &simplex_egraph; +} + +arith_egraph_interface_t *simplex_arith_egraph_interface(simplex_solver_t *solver) { + return &simplex_arith_egraph; +} +*/ \ 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..cd5b3934d --- /dev/null +++ b/src/solvers/mcarith/mcarith.h @@ -0,0 +1,63 @@ +/* + * 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 . + */ + +#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); + +/** + * + */ +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 \ No newline at end of file From 1b2cca997df02935707398579edfc0624574c05f Mon Sep 17 00:00:00 2001 From: Joe Hendrix Date: Wed, 10 Nov 2021 12:23:35 -0800 Subject: [PATCH 02/10] Fix comment typo --- src/solvers/simplex/simplex.c | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/solvers/simplex/simplex.c b/src/solvers/simplex/simplex.c index 32a17a522..db9b54fe9 100644 --- a/src/solvers/simplex/simplex.c +++ b/src/solvers/simplex/simplex.c @@ -10122,7 +10122,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) { } From e405f25ad3a4ccedd745e4af951db98f8e11ffa8 Mon Sep 17 00:00:00 2001 From: Joe Hendrix Date: Wed, 15 Dec 2021 11:17:58 -0800 Subject: [PATCH 03/10] Support conflicts in mcarith --- src/api/context_config.c | 1 + src/mcsat/nra/nra_plugin_internal.c | 2 + src/solvers/mcarith/mcarith.c | 754 +++++++++++++++++++++------- 3 files changed, 574 insertions(+), 183 deletions(-) diff --git a/src/api/context_config.c b/src/api/context_config.c index fab69210b..f9bfe0ae6 100644 --- a/src/api/context_config.c +++ b/src/api/context_config.c @@ -181,6 +181,7 @@ 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_MCSATARITH, // QF_NRA CTX_ARCH_MCSAT, // QF_NIRA CTX_ARCH_SPLX, // QF_RDL 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/mcarith/mcarith.c b/src/solvers/mcarith/mcarith.c index ba95780af..4e1166663 100644 --- a/src/solvers/mcarith/mcarith.c +++ b/src/solvers/mcarith/mcarith.c @@ -29,6 +29,11 @@ #include "mcsat/trail.h" #include "mcsat/variable_db.h" +extern void simplex_attach_eterm(simplex_solver_t *solver, thvar_t v, eterm_t t); +extern thvar_t simplex_create_const(simplex_solver_t *solver, rational_t *q); +extern eterm_t simplex_eterm_of_var(simplex_solver_t *solver, thvar_t v); +extern void simplex_start_internalization(simplex_solver_t *solver); + /** * Initialize b from a power product with variables translated by map. */ @@ -82,81 +87,272 @@ polynomial_t* alloc_polynomial_from_map(polynomial_t* p, thvar_t* map, int32_t v } // Indicates if the variable is free or a poly. -enum mcarith_var_type { VAR_FREE, VAR_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 }; -enum mcarith_assertion_type { VAR_EQ, POLY_EQ, POLY_GE }; - -struct mcarith_assertion_s { +/** + * 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; + 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)); +} -typedef struct mcarith_assertion_s mcarith_assertion_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_push_undo_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; +} + +/* + * Push an undo record to the stack. + */ +static mcarith_undo_record_t* mcarith_pop_undo_record(mcarith_undo_stack_t* stack) { + assert(stack->top > 0); + return stack->data + --stack->top; +} + +// 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; - // const context_t* ctx; - // Variable definitions +#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 + + // Size of var_terms array + uint32_t var_terms_size; + // Map theory variables to term. + term_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; // Information about theory variables. - mcarith_var_t* vars; + //mcarith_var_t* vars; // Assertion array mcarith_assertion_t* assertions; - size_t assertion_capacity; - size_t assertion_count; + // Number of entries in the array + uint32_t assertion_capacity; + // Number of assertions so far. + uint32_t assertion_count; + + mcarith_undo_stack_t undo_stack; }; +#ifdef MCSAT_STANDALONE_TERMS +static +pprod_table_t* mcarith_solver_pprods(const mcarith_solver_t* s) { + return &s->pprods; +} + +static +type_table_t* mcarith_solver_types(const mcarith_solver_t* s) { + return &s->types; +} + +static +term_table_t* mcarith_solver_terms(const mcarith_solver_t* s) { + return &s->terms; +} +#else +static +pprod_table_t* mcarith_solver_pprods(const mcarith_solver_t* s) { + return s->pprods; +} + +static +type_table_t* mcarith_solver_types(const mcarith_solver_t* s) { + return s->types; +} + +static +term_table_t* mcarith_solver_terms(const mcarith_solver_t* s) { + return s->terms; +} +#endif + /* * Initialize a mcarith solver */ void init_mcarith_solver(mcarith_solver_t **solver, context_t* ctx) { - const size_t init_assertion_capacity = 64; + 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); + +#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); + s->var_terms = safe_malloc(sizeof(term_t)); + s->var_terms_size = 1; + rational_t one; + q_set_one(&one); + s->var_terms[0] = 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; - s->vars = safe_malloc(sizeof(mcarith_var_t) * s->simplex.vtbl.size); + + // Create undo stack + const uint32_t init_undo_stack_size = 32; + init_mcarith_undo_stack(&s->undo_stack, init_undo_stack_size); + *solver = s; } void destroy_mcarith_solver(mcarith_solver_t* s) { - // Free vars - uint32_t vc = s->simplex.vtbl.nvars; - for (uint32_t i = 0; i != vc; ++i) { - switch (s->vars[i].type) { - case VAR_POLY: - free_pprod(s->vars[i].def.prod); - break; - default: - break; - } - } - safe_free(s->vars); // 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 + safe_free(s->var_terms); + safe_free(s->atom_terms); + +#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 @@ -164,32 +360,255 @@ void destroy_mcarith_solver(mcarith_solver_t* s) { } /* - * Create a new theory variable - * - is_int indicates whether the variable should be an integer. + * 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 new_size = solver->simplex.vtbl.size; + realloc_term_array(&solver->var_terms_size, &solver->var_terms, 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 +term_t get_term(mcarith_solver_t* solver, thvar_t v) { + arith_vartable_t* table = &solver->simplex.vtbl; + assert(0 <= v && v < table->nvars); + + term_t t = solver->var_terms[v]; + if (t != NULL_TERM) 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(mcarith_solver_terms(solver), tp); + } + 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 { + term_t t = get_term(solver, p->mono[j].var); + rba_buffer_add_mono(&b, r, var_pp(t)); + } + } + t = arith_poly(mcarith_solver_terms(solver), &b); + } + 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(mcarith_solver_terms(solver), table->def[v]); + break; + default: + longjmp(*solver->simplex.env, INTERNAL_ERROR); + } + solver->var_terms[v] = t; + return t; +} + +/* This addsthe 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 = &solver->simplex.vtbl; + assert(0 <= v && v < table->nvars); + + uint8_t tag = table->tag[v]; + switch (tag & AVARTAG_KIND_MASK) { + case AVARTAG_KIND_POLY: { + polynomial_t* p = table->def[v]; + 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 { + term_t t = get_term(solver, p->mono[j].var); + rba_buffer_add_mono(b, r, 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: + rba_buffer_add_const(b, table->def[v]); + break; + default: + rba_buffer_add_pp(b, var_pp(get_term(solver, v))); + } +} + +/* 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 = &solver->simplex.vtbl; + assert(0 <= v && v < table->nvars); + + uint8_t tag = table->tag[v]; + switch (tag & AVARTAG_KIND_MASK) { + case AVARTAG_KIND_POLY: { + polynomial_t* p = table->def[v]; + 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_sub_const(b, r); + } else { + term_t t = get_term(solver, p->mono[j].var); + rba_buffer_sub_mono(b, r, 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: + rba_buffer_sub_const(b, table->def[v]); + break; + default: + rba_buffer_sub_pp(b, var_pp(get_term(solver, v))); + } +} + +/* + * Return the term associated with the given atom index. */ static -thvar_t mcarith_create_var_internal(mcarith_solver_t *solver, bool is_int) { - uint32_t init_size = solver->simplex.vtbl.size; +term_t get_atom(mcarith_solver_t* solver, int32_t atom_index) { + mcarith_check_atom_size(solver); - thvar_t v = simplex_create_var(&solver->simplex, is_int); + arith_atomtable_t *atbl = &solver->simplex.atbl; + assert(0 <= atom_index && atom_index < atbl->natoms); - uint32_t new_size = solver->simplex.vtbl.size; - if (new_size > init_size) { - solver->vars = safe_realloc(solver->vars, sizeof(mcarith_var_t) * new_size); + term_t p = solver->atom_terms[atom_index]; + if (p != NULL_TERM) return p; + + arith_atom_t* ap = atbl->atoms + atom_index; + rational_t* bnd = bound_of_atom(ap); + term_table_t* terms = mcarith_solver_terms(solver); + + switch (tag_of_atom(ap)) { + // Assert v-b >= 0 + case GE_ATM: { + term_t polyTerm; + if (q_is_zero(bnd)) { + polyTerm = get_term(solver, var_of_atom(ap)); + } else { + rba_buffer_t b; + init_rba_buffer(&b, mcarith_solver_pprods(solver)); + rba_buffer_add_mcarithvar(solver, &b, var_of_atom(ap)); + rba_buffer_sub_const(&b, bnd); + polyTerm = arith_poly(terms, &b); + delete_rba_buffer(&b); + } + p = arith_geq_atom(terms, polyTerm); + break; } - assert(v < new_size); + // Assert v <= b by asserting b-v >= 0 + case LE_ATM: { + rba_buffer_t b; + init_rba_buffer(&b, mcarith_solver_pprods(solver)); + rba_buffer_sub_mcarithvar(solver, &b, var_of_atom(ap)); + rba_buffer_add_const(&b, bnd); + term_t polyTerm = arith_poly(terms, &b); + delete_rba_buffer(&b); + p = arith_geq_atom(terms, polyTerm); + break; + } + // Assert v == bnd + case EQ_ATM: { + term_t t = get_term(solver, var_of_atom(ap)); + p = arith_bineq_atom(terms, t, arith_constant(terms, bnd)); + break; + } + default: + longjmp(*solver->simplex.env, INTERNAL_ERROR); + } + solver->atom_terms[atom_index] = p; + return p; +} + +/* + * Create a new variable that represents constant q + * - add a matrix column if that's a new variable + */ +thvar_t mcarith_create_const(mcarith_solver_t *solver, rational_t *q) { + thvar_t v = simplex_create_const(&solver->simplex, q); + uint8_t tag = solver->simplex.vtbl.tag[v]; + assert((tag & AVARTAG_KIND_MASK) == AVARTAG_KIND_CONST); return v; } /* - * Create a new theory variable - * - is_int indicates whether the variable should be an integer - * - also add a matrix column + * Create a power of products. */ static -thvar_t mcarith_create_var(mcarith_solver_t *solver, bool is_int) { - thvar_t v = mcarith_create_var_internal(solver, is_int); - solver->vars[v].type = VAR_FREE; +thvar_t mcarith_create_pprod(mcarith_solver_t *solver, pprod_t *p, thvar_t *map) { + 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); + for (uint32_t i = 0; i < p->len; ++i) { + thvar_t mv = map[i]; + assert(mv < v); + term_t t = get_term(solver, mv); + pp_buffer_set_varexp(&b, t, p->prod[i].exp); + } + pp_buffer_normalize(&b); + + + // Create term + solver->var_terms[v] = pprod_term_from_buffer(mcarith_solver_terms(solver), &b); + + // Free buffer and return + delete_pp_buffer(&b); return v; } @@ -197,15 +616,16 @@ thvar_t mcarith_create_var(mcarith_solver_t *solver, bool is_int) { * Allocate an assertion for storing on array. */ static -mcarith_assertion_t* alloc_assertion(mcarith_solver_t* s) { +mcarith_assertion_t* alloc_top_assertion(mcarith_solver_t* s) { size_t cnt = s->assertion_count; if (cnt < s->assertion_capacity) { ++s->assertion_count; return s->assertions + cnt; } else { assert(cnt == s->assertion_capacity); - assert(s->assertion_capacity > 0); 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)); return s->assertions + cnt; } @@ -222,9 +642,7 @@ mcarith_assertion_t* alloc_assertion(mcarith_solver_t* s) { * - we reset the tableau and restore the matrix if needed */ void mcarith_start_internalization(mcarith_solver_t *solver) { -// simplex_reset_tableau(solver); -// simplex_restore_matrix(solver); -// assert(solver->matrix_ready && ! solver->tableau_ready); + simplex_start_internalization(&solver->simplex); } /* @@ -233,9 +651,8 @@ void mcarith_start_internalization(mcarith_solver_t *solver) { * - initialize the tableau * - compute the initial assignment */ -void mcarith_start_search(mcarith_solver_t *solver) { -// assert(0); //FIXME - +static void mcarith_start_search(mcarith_solver_t *solver) { + simplex_start_search(&solver->simplex); } /* @@ -245,21 +662,30 @@ void mcarith_start_search(mcarith_solver_t *solver) { * return true if no conflict is found. */ bool mcarith_propagate(mcarith_solver_t *solver) { - return true; + 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(rba_buffer_t* b, pprod_table_t* pprods, - polynomial_t* p, - term_t* var_terms, int32_t var_count) { - init_rba_buffer(b, pprods); +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 { - assert(0 <= p->mono[j].var && p->mono[j].var < var_count); - pprod_t* pp = var_pp(var_terms[p->mono[j].var]); + pprod_t* pp = var_pp(get_term(solver, p->mono[j].var)); rba_buffer_add_mono(b, &p->mono[j].coeff, pp); } } @@ -270,90 +696,58 @@ void init_rba_buffer_from_poly(rba_buffer_t* b, pprod_table_t* pprods, */ static fcheck_code_t mcarith_final_check(mcarith_solver_t *solver) { - type_table_t types; - init_type_table(&types, 64); - type_t itype = int_type(&types); - type_t rtype = real_type(&types); - - // Initialize power product table. - pprod_table_t pprods; - init_pprod_table(&pprods, 0); // Use default size - - // Initialize term table - term_table_t terms; - const uint32_t init_termtable_size = 1024; - - // Var table for arithmetic - arith_vartable_t* vtbl = &solver->simplex.vtbl; - - uint32_t vc = num_arith_vars(vtbl); - init_term_table(&terms, init_termtable_size, &types, &pprods); context_t ctx; const bool qflag = false; // Quantifiers not allowed - init_context(&ctx, &terms, QF_NRA, CTX_MODE_ONECHECK, CTX_ARCH_MCSAT, qflag); - - // Create array for mapping theory variables to initial term. - term_t* var_terms = safe_malloc(vc * sizeof(term_t)); - // The variable denotes the constant one. - rational_t one; - q_set_one(&one); - var_terms[0] = arith_constant(&terms, &one); - // Allow variables/terms for later variables. - for (uint32_t i = 1; i < vc; ++i) { - bool is_int; - pp_buffer_t b; - - switch (solver->vars[i].type) { - case VAR_FREE: - is_int = arith_var_is_int(vtbl, i); - var_terms[i] = new_uninterpreted_term(&terms, is_int ? itype : rtype); - break; - case VAR_POLY: - init_pp_buffer_from_pprod_map(&b, solver->vars[i].def.prod, var_terms, i); - var_terms[i] = pprod_term_from_buffer(&terms, &b); - break; - default: - assert(false); - } - } + term_table_t* terms = mcarith_solver_terms(solver); + init_context(&ctx, terms, QF_NRA, CTX_MODE_ONECHECK, CTX_ARCH_MCSAT, qflag); mcsat_solver_t* mcsat = mcsat_new(&ctx); term_t* assertions = safe_malloc(sizeof(term_t) * solver->assertion_count); literal_t* literals = safe_malloc(sizeof(literal_t) * solver->assertion_count + 1); size_t literal_count = 0; + mcarith_check_var_size(solver); for (size_t i = 0; i < solver->assertion_count; ++i) { mcarith_assertion_t* a = solver->assertions + i; - rba_buffer_t b; term_t p; switch (a->type) { case VAR_EQ: - p = eq_term(&terms, var_terms[a->def.eq.lhs], var_terms[a->def.eq.rhs]); + p = arith_bineq_atom(terms, get_term(solver, a->def.eq.lhs), get_term(solver, a->def.eq.rhs)); break; - case POLY_EQ: - init_rba_buffer_from_poly(&b, &pprods, a->def.poly, var_terms, vc); - p = arith_eq_atom(&terms, arith_poly(&terms, &b)); + case VAR_EQ0: + p = arith_eq_atom(terms, get_term(solver, a->def.var)); + break; + case VAR_GE0: + p = arith_geq_atom(terms, get_term(solver, a->def.var)); + break; + case POLY_EQ0: + init_rba_buffer_from_poly(solver, &b, a->def.poly); + p = arith_eq_atom(terms, arith_poly(terms, &b)); delete_rba_buffer(&b); break; - case POLY_GE: - init_rba_buffer_from_poly(&b, &pprods, a->def.poly, var_terms, vc); - p = arith_geq_atom(&terms, arith_poly(&terms, &b)); + case POLY_GE0: + init_rba_buffer_from_poly(solver, &b, a->def.poly); + p = arith_geq_atom(terms, arith_poly(terms, &b)); delete_rba_buffer(&b); break; + case ATOM_ASSERT: + p = get_atom(solver, a->def.atom); + break; default: longjmp(*solver->simplex.env, INTERNAL_ERROR); } if (a->lit != null_literal) { - literals[literal_count++] = a->lit; + smt_core_t* c = solver->simplex.core; + assert(literal_value(c, a->lit) == VAL_TRUE); + literals[literal_count++] = not(a->lit); } - assertions[i] = a->tt ? p : not_term(&terms, p); + assertions[i] = a->tt ? p : not_term(terms, p); } literals[literal_count] = end_clause; - int32_t r = mcsat_assert_formulas(mcsat, solver->assertion_count, assertions); fcheck_code_t result; if (r == TRIVIALLY_UNSAT) { @@ -384,20 +778,17 @@ fcheck_code_t mcarith_final_check(mcarith_solver_t *solver) { case STATUS_ERROR: default: safe_free(literals); - longjmp(solver->simplex.env, INTERNAL_ERROR); + longjmp(*solver->simplex.env, INTERNAL_ERROR); break; } } else { safe_free(literals); - longjmp(solver->simplex.env, INTERNAL_ERROR); + longjmp(*solver->simplex.env, INTERNAL_ERROR); } mcsat_destruct(mcsat); safe_free(mcsat); delete_context(&ctx); - delete_term_table(&terms); - delete_pprod_table(&pprods); - delete_type_table(&types); return result; } @@ -405,6 +796,7 @@ fcheck_code_t mcarith_final_check(mcarith_solver_t *solver) { * Increase dlevel in simplex and eqprop */ void mcarith_increase_decision_level(mcarith_solver_t *solver) { + simplex_increase_decision_level(&solver->simplex); assert(0); //FIXME } @@ -423,16 +815,22 @@ void mcarith_backtrack(mcarith_solver_t *solver, uint32_t back_level) { * Start a new base level */ void mcarith_push(mcarith_solver_t *solver) { - assert(0); //FIXME - //mcsat_push(solver->mcsat); + simplex_push(&solver->simplex); + mcarith_push_undo_record(&solver->undo_stack, solver->assertion_count); } /* * Return to the previous base level */ void mcarith_pop(mcarith_solver_t *solver) { - assert(0); //FIXME - //mcsat_pop(solver->mcsat); + // Reset assertions + mcarith_undo_record_t* r = mcarith_pop_undo_record(&solver->undo_stack); + for (uint32_t i = r->n_assertions; i != solver->assertion_count; ++i) { + free_mcarith_assertion(solver->assertions + i); + } + solver->assertion_count = r->n_assertions; + // Pop simplex state + simplex_pop(&solver->simplex); } /* @@ -476,8 +874,25 @@ static th_ctrl_interface_t mcarith_control = { * Do nothing (although we could try more simplification if * this is called before start_search). */ -bool mcarith_assert_atom(mcarith_solver_t *solver, void *a, literal_t l) { - assert(0); //FIXME +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); + + arith_atom_t* ap = atbl->atoms + atom_index; + assert(boolvar_of_atom(ap) == 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; } @@ -486,7 +901,7 @@ bool mcarith_assert_atom(mcarith_solver_t *solver, void *a, literal_t l) { * - 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) { - assert(false); // This function should not be called. + assert(0); // This function should not be called. } /* @@ -506,15 +921,6 @@ static th_smt_interface_t mcarith_smt = { .end_atom_deletion = NULL, }; -/* - * Create a new variable that represents constant q - * - add a matrix column if that's a new variable - */ -thvar_t mcarith_create_const(mcarith_solver_t *solver, rational_t *q) { - assert(0); //FIXME - return 0; // FIXME -} - /* * Create a theory variable equal to p * - arith_map maps variables of p to corresponding theory variables @@ -525,33 +931,6 @@ thvar_t mcarith_create_poly(mcarith_solver_t *solver, polynomial_t *p, thvar_t * return 0; // FIXME } - -/* - * Create a power of products. - */ -static -thvar_t mcarith_create_pprod(mcarith_solver_t *solver, pprod_t *p, thvar_t *map) { - assert(pprod_degree(p) > 1); //FIXME - assert(!pp_is_empty(p)); - assert(!pp_is_var(p)); - - // Remap variables in powerproduct - pp_buffer_t b; - init_pp_buffer(&b, p->len); - for (uint32_t i = 0; i < p->len; ++i) { - pp_buffer_set_varexp(&b, map[i], p->prod[i].exp); - } - pp_buffer_normalize(&b); - - // Assign power product - thvar_t v = mcarith_create_var_internal(solver, false); - solver->vars[v].type = VAR_POLY; - solver->vars[v].def.prod = pp_buffer_getprod(&b); - - delete_pp_buffer(&b); - return v; -} - /* * Create the atom x == 0 * - this attach the atom to the smt_core @@ -588,15 +967,6 @@ literal_t mcarith_create_poly_ge_atom(mcarith_solver_t *solver, polynomial_t *p, return 0; // FIXME } -/* - * Create the atom x - y == 0 - * - x and y are two theory variables - */ -literal_t mcarith_create_vareq_atom(mcarith_solver_t *solver, thvar_t x, thvar_t y) { - assert(0); //FIXME - return 0; // FIXME -} - /* * Assert a top-level equality constraint (either x == 0 or x != 0) * - tt indicates whether the constraint or its negation must be asserted @@ -604,8 +974,14 @@ literal_t mcarith_create_vareq_atom(mcarith_solver_t *solver, thvar_t x, thvar_t * tt == false --> assert x != 0 */ void mcarith_assert_eq_axiom(mcarith_solver_t *solver, thvar_t x, bool tt) { - assert(0); //FIXME - //FIXME + simplex_assert_eq_axiom(&solver->simplex, x, tt); + + // Record assertion for sending to mcarith solver. + mcarith_assertion_t* assert = alloc_top_assertion(solver); + assert->type = VAR_EQ0; + assert->def.var = x; + assert->tt = tt; + assert->lit = null_literal; } /* @@ -615,8 +991,13 @@ void mcarith_assert_eq_axiom(mcarith_solver_t *solver, thvar_t x, bool tt) { * tt == false --> assert x < 0 */ void mcarith_assert_ge_axiom(mcarith_solver_t *solver, thvar_t x, bool tt){ - assert(0); //FIXME - //FIXME + simplex_assert_ge_axiom(&solver->simplex, x, tt); + + mcarith_assertion_t* assert = alloc_top_assertion(solver); + assert->type = VAR_GE0; + assert->def.var = x; + assert->tt = tt; + assert->lit = null_literal; } /* @@ -627,8 +1008,11 @@ void mcarith_assert_ge_axiom(mcarith_solver_t *solver, thvar_t x, bool tt){ */ void mcarith_assert_poly_eq_axiom(mcarith_solver_t *solver, polynomial_t *p, thvar_t *map, bool tt) { assert(p->nterms > 0); - mcarith_assertion_t* assert = alloc_assertion(solver); - assert->type = POLY_EQ; + + simplex_assert_poly_eq_axiom(&solver->simplex, p, map, tt); + + mcarith_assertion_t* assert = alloc_top_assertion(solver); + assert->type = POLY_EQ0; assert->def.poly = alloc_polynomial_from_map(p, map, solver->simplex.vtbl.nvars); assert->tt = tt; assert->lit = null_literal; @@ -641,8 +1025,11 @@ void mcarith_assert_poly_eq_axiom(mcarith_solver_t *solver, polynomial_t *p, thv */ void mcarith_assert_poly_ge_axiom(mcarith_solver_t *solver, polynomial_t *p, thvar_t *map, bool tt) { assert(p->nterms > 0); - mcarith_assertion_t* assert = alloc_assertion(solver); - assert->type = POLY_GE; + + simplex_assert_poly_ge_axiom(&solver->simplex, p, map, tt); + + mcarith_assertion_t* assert = alloc_top_assertion(solver); + assert->type = POLY_GE0; assert->def.poly = alloc_polynomial_from_map(p, map, solver->simplex.vtbl.nvars); assert->tt = tt; assert->lit = null_literal; @@ -653,7 +1040,10 @@ void mcarith_assert_poly_ge_axiom(mcarith_solver_t *solver, polynomial_t *p, thv * If tt == false --> assert (x - y != 0) */ void mcarith_assert_vareq_axiom(mcarith_solver_t *solver, thvar_t x, thvar_t y, bool tt) { - mcarith_assertion_t* assert = alloc_assertion(solver); + simplex_assert_vareq_axiom(&solver->simplex, x, y, tt); + + mcarith_assertion_t* assert = alloc_top_assertion(solver); + assert->type = VAR_EQ; assert->def.eq.lhs = x; assert->def.eq.rhs = y; @@ -685,7 +1075,6 @@ bool mcarith_var_is_integer(mcarith_solver_t *solver, thvar_t x) { } -extern void simplex_attach_eterm(simplex_solver_t *solver, thvar_t v, eterm_t t); /* * Attach egraph term t to a variable v @@ -695,8 +1084,6 @@ static void mcarith_attach_eterm(mcarith_solver_t *solver, thvar_t v, eterm_t t) simplex_attach_eterm(&solver->simplex, v, t); } -extern eterm_t simplex_eterm_of_var(simplex_solver_t *solver, thvar_t v); - /* * Get the egraph term t attached to v * - return null_eterm if v has no eterm attached @@ -712,6 +1099,7 @@ static eterm_t mcarith_eterm_of_var(mcarith_solver_t *solver, thvar_t v) { */ void mcarith_build_model(mcarith_solver_t *solver) { // FIXME + assert(0); printf("mcarith_build_model\n"); } @@ -740,8 +1128,8 @@ bool mcarith_value_in_model(mcarith_solver_t *solver, thvar_t x, rational_t *v) *****************************/ static arith_interface_t mcarith_context = { - .create_var = (create_arith_var_fun_t) mcarith_create_var, - .create_const = (create_arith_const_fun_t) mcarith_create_const, + .create_var = (create_arith_var_fun_t) simplex_create_var, + .create_const = (create_arith_const_fun_t) simplex_create_const, .create_poly = (create_arith_poly_fun_t) mcarith_create_poly, .create_pprod = (create_arith_pprod_fun_t) mcarith_create_pprod, @@ -749,7 +1137,7 @@ static arith_interface_t mcarith_context = { .create_ge_atom = (create_arith_atom_fun_t) mcarith_create_ge_atom, .create_poly_eq_atom = (create_arith_patom_fun_t) mcarith_create_poly_eq_atom, .create_poly_ge_atom = (create_arith_patom_fun_t) mcarith_create_poly_ge_atom, - .create_vareq_atom = (create_arith_vareq_atom_fun_t) mcarith_create_vareq_atom, + .create_vareq_atom = (create_arith_vareq_atom_fun_t) simplex_create_vareq_atom, .assert_eq_axiom = (assert_arith_axiom_fun_t) mcarith_assert_eq_axiom, .assert_ge_axiom = (assert_arith_axiom_fun_t) mcarith_assert_ge_axiom, From f24450c037738202d8d18530c3775f7bc75a684f Mon Sep 17 00:00:00 2001 From: Joe Hendrix Date: Mon, 10 Jan 2022 23:36:50 -0800 Subject: [PATCH 04/10] Add model and rdiv support to mcarith. --- src/api/yices_api.c | 6 - src/context/context.c | 67 ++- src/context/context_solver.c | 21 +- src/context/context_types.h | 40 +- .../floyd_warshall/idl_floyd_warshall.c | 15 +- .../floyd_warshall/idl_floyd_warshall.h | 2 +- .../floyd_warshall/rdl_floyd_warshall.c | 14 +- .../floyd_warshall/rdl_floyd_warshall.h | 2 +- src/solvers/mcarith/mcarith.c | 409 ++++++++++-------- src/solvers/simplex/simplex.c | 15 +- src/solvers/simplex/simplex.h | 4 +- 11 files changed, 379 insertions(+), 216 deletions(-) diff --git a/src/api/yices_api.c b/src/api/yices_api.c index faed13510..787fdcced 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 diff --git a/src/context/context.c b/src/context/context.c index a89f5a8d0..881b214f9 100644 --- a/src/context/context.c +++ b/src/context/context.c @@ -1487,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; } @@ -2653,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)); @@ -4963,7 +4973,7 @@ static const uint32_t arch2theories[NUM_ARCH] = { RDL_MASK, // CTX_ARCH_AUTO_RDL UF_MASK|ARITH_MASK|FUN_MASK, // CTX_ARCH_MCSAT - ARITH_MASK // CTX_ARCH_MCSATARITH + ARITH_MASK // CTX_ARCH_MCSATARITH }; @@ -5347,7 +5357,7 @@ static void create_mcarith_solver(context_t *ctx) { 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) { longjmp(ctx->env, INTERNAL_ERROR); @@ -5751,7 +5761,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; @@ -5769,6 +5780,42 @@ void init_context(context_t *ctx, term_table_t *terms, smt_logic_t logic, } +void arithval_in_model_delete(arithval_in_model_t* v); + +void arithval_in_model_delete(arithval_in_model_t* v) { + switch (v->tag) { + case ARITHVAL_RATIONAL: + 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; + } +} /* @@ -5851,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); } @@ -5905,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..5ea55ed8f 100644 --- a/src/context/context_solver.c +++ b/src/context/context_solver.c @@ -892,14 +892,29 @@ static value_t bool_value(context_t *ctx, value_table_t *vtbl, literal_t l) { * 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 667e923cd..8302d6ba6 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 * **********************/ @@ -248,6 +252,30 @@ enum { }; +/** + * Tag for representing a value returned by arithmetic solver. + */ +typedef enum arithval_tag { + ARITHVAL_ERROR, + ARITHVAL_RATIONAL, +#ifdef HAVE_MCSAT + ARITHVAL_ALGEBRAIC, +#endif +} arithval_tag_t; + +/* + * Tagged union to represent pointers to either rational or algebraic numbers. + * The flag can ERROR/RATIONAL/ALGEBRAIC + */ +typedef struct { + arithval_tag_t tag; + union { + rational_t q; +#ifdef HAVE_MCSAT + lp_algebraic_number_t alg_number; +#endif + } val; +} arithval_in_model_t; /************************** @@ -382,7 +410,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 @@ -402,6 +430,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); @@ -418,7 +447,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); @@ -427,6 +456,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; @@ -717,7 +747,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 @@ -760,7 +792,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/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 index 4e1166663..23dba4bf3 100644 --- a/src/solvers/mcarith/mcarith.c +++ b/src/solvers/mcarith/mcarith.c @@ -29,38 +29,17 @@ #include "mcsat/trail.h" #include "mcsat/variable_db.h" +#include "model/models.h" +#include "model/model_queries.h" + +#include "yices.h" + extern void simplex_attach_eterm(simplex_solver_t *solver, thvar_t v, eterm_t t); extern thvar_t simplex_create_const(simplex_solver_t *solver, rational_t *q); extern eterm_t simplex_eterm_of_var(simplex_solver_t *solver, thvar_t v); extern void simplex_start_internalization(simplex_solver_t *solver); - -/** - * Initialize b from a power product with variables translated by map. - */ -static -void init_pp_buffer_from_pprod_map(pp_buffer_t* b, pprod_t* p, int32_t* map, size_t map_size) { - init_pp_buffer(b, p->len); - for (uint32_t i = 0; i < p->len; ++i) { - varexp_t* v = p->prod + i; - assert(v->var < map_size); - pp_buffer_set_varexp(b, map[v->var], v->exp); - } - pp_buffer_normalize(b); -} - -/** - * Initialize b from a power product with variables translated by map. - */ -static -void init_pp_buffer_from_index_pprod_map(pp_buffer_t* b, pprod_t* p, int32_t* map, size_t map_size) { - init_pp_buffer(b, p->len); - for (uint32_t i = 0; i < p->len; ++i) { - varexp_t* v = p->prod + i; - assert(v->var < map_size); - pp_buffer_set_varexp(b, map[v->var], v->exp); - } - pp_buffer_normalize(b); -} +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. @@ -71,7 +50,7 @@ polynomial_t* alloc_polynomial_from_map(polynomial_t* p, thvar_t* map, int32_t v polynomial_t* pv = alloc_raw_polynomial(n); if (n == 0) return pv; - q_set(&pv->mono[0].coeff, &p->mono[0].coeff); + q_set(&pv->mono[0].coeff, &p->mono[0].coeff); if (p->mono[0].var == const_idx) { pv->mono[0].var = 0; } else { @@ -79,7 +58,7 @@ polynomial_t* alloc_polynomial_from_map(polynomial_t* p, thvar_t* map, int32_t v pv->mono[0].var = map[0]; } for (uint32_t i = 1; i < n; ++i) { - q_set(&pv->mono[i].coeff, &p->mono[i].coeff); + q_set(&pv->mono[i].coeff, &p->mono[i].coeff); assert(0 <= map[i] && map[i] < var_count); pv->mono[i].var = map[i]; } @@ -103,12 +82,12 @@ enum mcarith_assertion_type { VAR_EQ, VAR_EQ0, VAR_GE0, POLY_EQ0, POLY_GE0, ATOM /** * 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. @@ -170,13 +149,13 @@ typedef struct mcarith_undo_stack_s { */ 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) { @@ -190,7 +169,7 @@ static void extend_mcarith_undo_stack(mcarith_undo_stack_t* stack) { /* * Push an undo record to the stack. */ -static void mcarith_push_undo_record(mcarith_undo_stack_t* stack, uint32_t n_a) { +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 @@ -205,11 +184,45 @@ static void mcarith_push_undo_record(mcarith_undo_stack_t* stack, uint32_t n_a) /* * Push an undo record to the stack. */ -static mcarith_undo_record_t* mcarith_pop_undo_record(mcarith_undo_stack_t* 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. @@ -218,6 +231,12 @@ static mcarith_undo_record_t* mcarith_pop_undo_record(mcarith_undo_stack_t* stac 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 @@ -234,20 +253,16 @@ struct mcarith_solver_s { // Term Table for mcsat term_table_t* terms; #endif - // Size of var_terms array uint32_t var_terms_size; - // Map theory variables to term. + // Map theory variables to term so we can send them to MCSat term_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; - // Information about theory variables. - //mcarith_var_t* vars; - // Assertion array mcarith_assertion_t* assertions; // Number of entries in the array @@ -259,33 +274,33 @@ struct mcarith_solver_s { }; #ifdef MCSAT_STANDALONE_TERMS -static -pprod_table_t* mcarith_solver_pprods(const mcarith_solver_t* s) { +static +pprod_table_t* mcarith_solver_pprods(mcarith_solver_t* s) { return &s->pprods; } static -type_table_t* mcarith_solver_types(const mcarith_solver_t* s) { +type_table_t* mcarith_solver_types(mcarith_solver_t* s) { return &s->types; } static -term_table_t* mcarith_solver_terms(const mcarith_solver_t* s) { +term_table_t* mcarith_solver_terms(mcarith_solver_t* s) { return &s->terms; } #else -static -pprod_table_t* mcarith_solver_pprods(const mcarith_solver_t* s) { +static +pprod_table_t* mcarith_solver_pprods(mcarith_solver_t* s) { return s->pprods; } static -type_table_t* mcarith_solver_types(const mcarith_solver_t* s) { +type_table_t* mcarith_solver_types(mcarith_solver_t* s) { return s->types; } static -term_table_t* mcarith_solver_terms(const mcarith_solver_t* s) { +term_table_t* mcarith_solver_terms(mcarith_solver_t* s) { return s->terms; } #endif @@ -299,18 +314,21 @@ void init_mcarith_solver(mcarith_solver_t **solver, context_t* ctx) { 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 + 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; + s->terms = ctx->terms; assert(ctx->types == ctx->terms->types); #endif @@ -338,7 +356,18 @@ void init_mcarith_solver(mcarith_solver_t **solver, context_t* ctx) { *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; + } +} + void destroy_mcarith_solver(mcarith_solver_t* s) { + mcarith_free_mcsat(s); // Free assertions for (uint32_t i = 0; i != s->assertion_count; ++i) { free_mcarith_assertion(s->assertions + i); @@ -356,7 +385,7 @@ void destroy_mcarith_solver(mcarith_solver_t* s) { // Free solver delete_simplex_solver(&s->simplex); // Free solver itself - safe_free(s); + safe_free(s); } /* @@ -374,7 +403,7 @@ void realloc_term_array(uint32_t* size_ptr, term_t** term_array, uint32_t new_si } /* - * This resizes var_Terms to make sure it is large enough + * This resizes var_terms to make sure it is large enough * to reference all vtbl entries. */ static inline @@ -397,8 +426,8 @@ static term_t get_term(mcarith_solver_t* solver, thvar_t v) { arith_vartable_t* table = &solver->simplex.vtbl; assert(0 <= v && v < table->nvars); - - term_t t = solver->var_terms[v]; + + term_t t = solver->var_terms[v]; if (t != NULL_TERM) return t; uint8_t tag = table->tag[v]; @@ -448,7 +477,7 @@ static void rba_buffer_add_mcarithvar(mcarith_solver_t* solver, rba_buffer_t* b, thvar_t v) { arith_vartable_t* table = &solver->simplex.vtbl; assert(0 <= v && v < table->nvars); - + uint8_t tag = table->tag[v]; switch (tag & AVARTAG_KIND_MASK) { case AVARTAG_KIND_POLY: { @@ -482,7 +511,7 @@ static void rba_buffer_sub_mcarithvar(mcarith_solver_t* solver, rba_buffer_t* b, thvar_t v) { arith_vartable_t* table = &solver->simplex.vtbl; assert(0 <= v && v < table->nvars); - + uint8_t tag = table->tag[v]; switch (tag & AVARTAG_KIND_MASK) { case AVARTAG_KIND_POLY: { @@ -511,7 +540,7 @@ void rba_buffer_sub_mcarithvar(mcarith_solver_t* solver, rba_buffer_t* b, thvar_ } } -/* +/* * Return the term associated with the given atom index. */ static @@ -569,22 +598,12 @@ term_t get_atom(mcarith_solver_t* solver, int32_t atom_index) { return p; } -/* - * Create a new variable that represents constant q - * - add a matrix column if that's a new variable - */ -thvar_t mcarith_create_const(mcarith_solver_t *solver, rational_t *q) { - thvar_t v = simplex_create_const(&solver->simplex, q); - uint8_t tag = solver->simplex.vtbl.tag[v]; - assert((tag & AVARTAG_KIND_MASK) == AVARTAG_KIND_CONST); - return v; -} - /* * Create a power of products. */ static -thvar_t mcarith_create_pprod(mcarith_solver_t *solver, pprod_t *p, thvar_t *map) { +thvar_t mcarith_create_pprod(void *s, pprod_t *p, thvar_t *map) { + mcarith_solver_t *solver = s; assert(pprod_degree(p) > 1); assert(!pp_is_empty(p)); assert(!pp_is_var(p)); @@ -603,15 +622,37 @@ thvar_t mcarith_create_pprod(mcarith_solver_t *solver, pprod_t *p, thvar_t *map) } pp_buffer_normalize(&b); - // Create term + assert(solver->var_terms_size > v); solver->var_terms[v] = pprod_term_from_buffer(mcarith_solver_terms(solver), &b); - // 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); + solver->var_terms[v] = arith_rdiv(mcarith_solver_terms(solver), nt, dt); + + return v; +} + /** * Allocate an assertion for storing on array. */ @@ -631,7 +672,6 @@ mcarith_assertion_t* alloc_top_assertion(mcarith_solver_t* s) { } } - /******************************** * SMT AND CONTROL INTERFACES * *******************************/ @@ -668,16 +708,16 @@ bool mcarith_propagate(mcarith_solver_t *solver) { /* * 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 +static void init_rba_buffer_from_poly(mcarith_solver_t* solver, - rba_buffer_t* b, + rba_buffer_t* b, polynomial_t* p) { init_rba_buffer(b, mcarith_solver_pprods(solver)); uint32_t n = p->nterms; @@ -696,16 +736,15 @@ void init_rba_buffer_from_poly(mcarith_solver_t* solver, */ static fcheck_code_t mcarith_final_check(mcarith_solver_t *solver) { + mcarith_free_mcsat(solver); - context_t ctx; const bool qflag = false; // Quantifiers not allowed term_table_t* terms = mcarith_solver_terms(solver); - init_context(&ctx, terms, QF_NRA, CTX_MODE_ONECHECK, CTX_ARCH_MCSAT, qflag); - - mcsat_solver_t* mcsat = mcsat_new(&ctx); + init_context(&solver->mcsat_ctx, terms, QF_NRA, CTX_MODE_ONECHECK, CTX_ARCH_MCSAT, qflag); + solver->mcsat = mcsat_new(&solver->mcsat_ctx); - term_t* assertions = safe_malloc(sizeof(term_t) * solver->assertion_count); - literal_t* literals = safe_malloc(sizeof(literal_t) * solver->assertion_count + 1); + term_t* assertions = safe_malloc(sizeof(term_t) * (solver->assertion_count + 1)); + literal_t* literals = safe_malloc(sizeof(literal_t) * (solver->assertion_count + 1)); size_t literal_count = 0; mcarith_check_var_size(solver); for (size_t i = 0; i < solver->assertion_count; ++i) { @@ -734,7 +773,7 @@ fcheck_code_t mcarith_final_check(mcarith_solver_t *solver) { delete_rba_buffer(&b); break; case ATOM_ASSERT: - p = get_atom(solver, a->def.atom); + p = get_atom(solver, a->def.atom); break; default: longjmp(*solver->simplex.env, INTERNAL_ERROR); @@ -746,18 +785,21 @@ fcheck_code_t mcarith_final_check(mcarith_solver_t *solver) { } assertions[i] = a->tt ? p : not_term(terms, p); } + assertions[solver->assertion_count] = assertions[solver->assertion_count-1]; literals[literal_count] = end_clause; - int32_t r = mcsat_assert_formulas(mcsat, solver->assertion_count, assertions); - fcheck_code_t result; + int32_t r = mcsat_assert_formulas(solver->mcsat, solver->assertion_count+1, assertions); + fcheck_code_t result; if (r == TRIVIALLY_UNSAT) { record_theory_conflict(solver->simplex.core, literals); + mcarith_free_mcsat(solver); result = FCHECK_CONTINUE; } else if (r == CTX_NO_ERROR) { result = FCHECK_SAT; - mcsat_solve(mcsat, 0, 0, 0, 0); - switch (mcsat_status(mcsat)) { + mcsat_solve(solver->mcsat, 0, 0, 0, 0); + switch (mcsat_status(solver->mcsat)) { case STATUS_UNKNOWN: + mcarith_free_mcsat(solver); safe_free(literals); result = FCHECK_UNKNOWN; break; @@ -766,7 +808,7 @@ fcheck_code_t mcarith_final_check(mcarith_solver_t *solver) { result = FCHECK_SAT; break; case STATUS_UNSAT: - // TODO: + mcarith_free_mcsat(solver); // - record a conflict (by calling record_theory_conflict) // - create lemmas or atoms in the core record_theory_conflict(solver->simplex.core, literals); @@ -777,46 +819,56 @@ fcheck_code_t mcarith_final_check(mcarith_solver_t *solver) { case STATUS_INTERRUPTED: case STATUS_ERROR: default: + mcarith_free_mcsat(solver); safe_free(literals); longjmp(*solver->simplex.env, INTERNAL_ERROR); break; } } else { + mcarith_free_mcsat(solver); safe_free(literals); longjmp(*solver->simplex.env, INTERNAL_ERROR); } - mcsat_destruct(mcsat); - safe_free(mcsat); - delete_context(&ctx); return result; } +/* + * 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); - assert(0); //FIXME + mcarith_undo_push_record(&solver->undo_stack, solver->assertion_count); } - /* * Full backtrack */ void mcarith_backtrack(mcarith_solver_t *solver, uint32_t back_level) { -#if TRACE - printf("---> Mcarith: backtracking to level %"PRIu32"\n", back_level); -#endif - assert(0); //FIXME + mcarith_undo_record_t* r = mcarith_undo_backtrack(&solver->undo_stack, back_level); + mcarith_backtrack_assertions(solver, r->n_assertions); + simplex_backtrack(&solver->simplex, back_level); } /* * Start a new base level */ -void mcarith_push(mcarith_solver_t *solver) { +static void mcarith_push(mcarith_solver_t *solver) { + assert(0); simplex_push(&solver->simplex); - mcarith_push_undo_record(&solver->undo_stack, solver->assertion_count); + mcarith_undo_push_record(&solver->undo_stack, solver->assertion_count); } /* @@ -824,11 +876,8 @@ void mcarith_push(mcarith_solver_t *solver) { */ void mcarith_pop(mcarith_solver_t *solver) { // Reset assertions - mcarith_undo_record_t* r = mcarith_pop_undo_record(&solver->undo_stack); - for (uint32_t i = r->n_assertions; i != solver->assertion_count; ++i) { - free_mcarith_assertion(solver->assertions + i); - } - solver->assertion_count = r->n_assertions; + mcarith_undo_record_t* r = mcarith_undo_pop_record(&solver->undo_stack); + mcarith_backtrack_assertions(solver, r->n_assertions); // Pop simplex state simplex_pop(&solver->simplex); } @@ -837,16 +886,16 @@ void mcarith_pop(mcarith_solver_t *solver) { * Reset to the empty solver */ void mcarith_reset(mcarith_solver_t *solver) { - assert(0); //FIXME - //mcsat_reset(solver->mcsat); + simplex_reset(&solver->simplex); + + mcarith_undo_reset(&solver->undo_stack); + mcarith_backtrack_assertions(solver, 0); } /* * Clear: nothing to clear. */ void mcarith_clear(mcarith_solver_t *solver) { - assert(0); //FIXME - //mcsat_clear(solver->mcsat); } static th_ctrl_interface_t mcarith_control = { @@ -901,7 +950,7 @@ bool mcarith_assert_atom(mcarith_solver_t *solver, void *atom_pointer, literal_t * - 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) { - assert(0); // This function should not be called. + simplex_expand_explanation(&solver->simplex, l, expl, v); } /* @@ -909,8 +958,7 @@ void mcarith_expand_explanation(mcarith_solver_t *solver, literal_t l, void *exp * - 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) { - assert(0); //FIXME - return l; // Do nothing + return simplex_select_polarity(&solver->simplex, a, l); } static th_smt_interface_t mcarith_smt = { @@ -927,8 +975,7 @@ static th_smt_interface_t mcarith_smt = { * in the solver */ thvar_t mcarith_create_poly(mcarith_solver_t *solver, polynomial_t *p, thvar_t *map) { - assert(0); //FIXME - return 0; // FIXME + return simplex_create_poly(&solver->simplex, p, map); } /* @@ -936,8 +983,7 @@ thvar_t mcarith_create_poly(mcarith_solver_t *solver, polynomial_t *p, thvar_t * * - this attach the atom to the smt_core */ literal_t mcarith_create_eq_atom(mcarith_solver_t *solver, thvar_t x) { - assert(0); //FIXME - return 0; // FIXME + return simplex_create_eq_atom(&solver->simplex, x); } /* @@ -945,8 +991,7 @@ literal_t mcarith_create_eq_atom(mcarith_solver_t *solver, thvar_t x) { * - this attach the atom to the smt_core */ literal_t mcarith_create_ge_atom(mcarith_solver_t *solver, thvar_t x) { - assert(0); //FIXME - return 0; // FIXME + return simplex_create_ge_atom(&solver->simplex, x); } /* @@ -954,8 +999,7 @@ literal_t mcarith_create_ge_atom(mcarith_solver_t *solver, thvar_t x) { * - apply the renaming defined by map */ literal_t mcarith_create_poly_eq_atom(mcarith_solver_t *solver, polynomial_t *p, thvar_t *map) { - assert(0); //FIXME - return 0; // FIXME + return simplex_create_poly_eq_atom(&solver->simplex, p, map); } /* @@ -963,8 +1007,7 @@ literal_t mcarith_create_poly_eq_atom(mcarith_solver_t *solver, polynomial_t *p, * - replace the variables of p as defined by map */ literal_t mcarith_create_poly_ge_atom(mcarith_solver_t *solver, polynomial_t *p, thvar_t *map) { - assert(0); //FIXME - return 0; // FIXME + return simplex_create_poly_ge_atom(&solver->simplex, p, map); } /* @@ -1043,7 +1086,6 @@ void mcarith_assert_vareq_axiom(mcarith_solver_t *solver, thvar_t x, thvar_t y, simplex_assert_vareq_axiom(&solver->simplex, x, y, tt); mcarith_assertion_t* assert = alloc_top_assertion(solver); - assert->type = VAR_EQ; assert->def.eq.lhs = x; assert->def.eq.rhs = y; @@ -1055,16 +1097,14 @@ void mcarith_assert_vareq_axiom(mcarith_solver_t *solver, thvar_t x, thvar_t y, * Assert (c ==> x == y) */ void mcarith_assert_cond_vareq_axiom(mcarith_solver_t *solver, literal_t c, thvar_t x, thvar_t y) { - assert(0); //FIXME - //FIXME + simplex_assert_cond_vareq_axiom(&solver->simplex, c, x, y); } /* * Assert (c[0] \/ ... \/ c[n-1] \/ x == y) */ void mcarith_assert_clause_vareq_axiom(mcarith_solver_t *solver, uint32_t n, literal_t *c, thvar_t x, thvar_t y) { - assert(0); //FIXME - //FIXME + simplex_assert_clause_vareq_axiom(&solver->simplex, n, c, x, y); } /* @@ -1074,8 +1114,6 @@ bool mcarith_var_is_integer(mcarith_solver_t *solver, thvar_t x) { return arith_var_is_int(&solver->simplex.vtbl, x); } - - /* * Attach egraph term t to a variable v * - v must not have an eterm attached already @@ -1097,18 +1135,29 @@ static eterm_t mcarith_eterm_of_var(mcarith_solver_t *solver, thvar_t v) { /* * Model construction */ -void mcarith_build_model(mcarith_solver_t *solver) { - // FIXME - assert(0); - printf("mcarith_build_model\n"); +static void mcarith_build_model(void* s) { + mcarith_solver_t* solver = s; + + model_t *model; + assert(solver->mcsat); + assert(!solver->model); + // Create model + model = yices_new_model(); + mcsat_build_model(solver->mcsat, model); + solver->model = model; + + mcarith_free_mcsat(solver); } /* * Free the model */ -void mcarith_free_model(mcarith_solver_t *solver) { - //FIXME - printf("mcarith_free_model\n"); +static void mcarith_free_model(void* s) { + mcarith_solver_t* solver = s; + assert(solver->model); + + yices_free_model(solver->model); + solver->model = 0; } /* @@ -1116,9 +1165,42 @@ void mcarith_free_model(mcarith_solver_t *solver) { * If x has a value, then this returns true and sets v. If not, then it returns * false. */ -bool mcarith_value_in_model(mcarith_solver_t *solver, thvar_t x, rational_t *v) { - printf("mcarith_value_in_model\n"); - return false; // FIXME +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[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)); + } 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 @@ -1131,7 +1213,8 @@ static arith_interface_t mcarith_context = { .create_var = (create_arith_var_fun_t) simplex_create_var, .create_const = (create_arith_const_fun_t) simplex_create_const, .create_poly = (create_arith_poly_fun_t) mcarith_create_poly, - .create_pprod = (create_arith_pprod_fun_t) mcarith_create_pprod, + .create_pprod = mcarith_create_pprod, + .create_rdiv = mcarith_create_rdiv, .create_eq_atom = (create_arith_atom_fun_t) mcarith_create_eq_atom, .create_ge_atom = (create_arith_atom_fun_t) mcarith_create_ge_atom, @@ -1150,9 +1233,9 @@ static arith_interface_t mcarith_context = { .attach_eterm = (attach_eterm_fun_t) mcarith_attach_eterm, .eterm_of_var = (eterm_of_var_fun_t) mcarith_eterm_of_var, - .build_model = (build_model_fun_t) mcarith_build_model, - .free_model = (free_model_fun_t) mcarith_free_model, - .value_in_model = (arith_val_in_model_fun_t) mcarith_value_in_model, + .build_model = mcarith_build_model, + .free_model = mcarith_free_model, + .value_in_model = mcarith_value_in_model, .arith_var_is_int = (arith_var_is_int_fun_t) mcarith_var_is_integer, }; @@ -1173,40 +1256,4 @@ th_ctrl_interface_t *mcarith_ctrl_interface(mcarith_solver_t *solver) { th_smt_interface_t *mcarith_smt_interface(mcarith_solver_t *solver) { return &mcarith_smt; -} - -/* -static th_egraph_interface_t simplex_egraph = { - (assert_eq_fun_t) simplex_assert_var_eq, - (assert_diseq_fun_t) simplex_assert_var_diseq, - (assert_distinct_fun_t) simplex_assert_var_distinct, - (check_diseq_fun_t) simplex_check_disequality, - (is_constant_fun_t) simplex_var_is_constant, - (expand_eq_exp_fun_t) simplex_expand_th_explanation, - (reconcile_model_fun_t) simplex_reconcile_model, - (prepare_model_fun_t) simplex_prep_model, - (equal_in_model_fun_t) simplex_var_equal_in_model, - (gen_inter_lemma_fun_t) simplex_gen_interface_lemma, - (release_model_fun_t) simplex_release_model, - (build_partition_fun_t) simplex_build_model_partition, - (free_partition_fun_t) simplex_release_model_partition, - (attach_to_var_fun_t) simplex_attach_eterm, - (get_eterm_fun_t) simplex_eterm_of_var, - (select_eq_polarity_fun_t) simplex_select_eq_polarity, -}; - - -static arith_egraph_interface_t simplex_arith_egraph = { - (make_arith_var_fun_t) simplex_create_var, - (arith_val_fun_t) simplex_value_in_model, -}; - - -th_egraph_interface_t *simplex_egraph_interface(simplex_solver_t *solver) { - return &simplex_egraph; -} - -arith_egraph_interface_t *simplex_arith_egraph_interface(simplex_solver_t *solver) { - return &simplex_arith_egraph; -} -*/ \ No newline at end of file +} \ No newline at end of file diff --git a/src/solvers/simplex/simplex.c b/src/solvers/simplex/simplex.c index db9b54fe9..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 @@ -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); From 0680c3103a0ddc8230a23349c12e68a0382df0ed Mon Sep 17 00:00:00 2001 From: Joe Hendrix Date: Tue, 11 Jan 2022 12:46:12 -0800 Subject: [PATCH 05/10] Reduce use of global term manager in mcsat. --- src/mcsat/nra/nra_plugin.c | 146 ++++++++++++++++++++++++++++++------- 1 file changed, 120 insertions(+), 26 deletions(-) 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); } From 18de466c62b707761b411662ce82707fa243271d Mon Sep 17 00:00:00 2001 From: Joe Hendrix Date: Tue, 11 Jan 2022 12:55:59 -0800 Subject: [PATCH 06/10] Cleanups; flatten mcsat poly terms. --- src/solvers/mcarith/mcarith.c | 333 +++++++++++++++++++++------------- 1 file changed, 211 insertions(+), 122 deletions(-) diff --git a/src/solvers/mcarith/mcarith.c b/src/solvers/mcarith/mcarith.c index 23dba4bf3..f899b6874 100644 --- a/src/solvers/mcarith/mcarith.c +++ b/src/solvers/mcarith/mcarith.c @@ -422,14 +422,23 @@ void mcarith_check_atom_size(mcarith_solver_t *solver) { 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); + static term_t get_term(mcarith_solver_t* solver, thvar_t v) { - arith_vartable_t* table = &solver->simplex.vtbl; + arith_vartable_t* table; + term_table_t* terms; + + terms = mcarith_solver_terms(solver); + + table = &solver->simplex.vtbl; assert(0 <= v && v < table->nvars); term_t t = solver->var_terms[v]; if (t != NULL_TERM) return t; + uint8_t tag = table->tag[v]; bool is_int = (tag & AVARTAG_INT_MASK) != 0; switch (tag & AVARTAG_KIND_MASK) { @@ -437,7 +446,7 @@ term_t get_term(mcarith_solver_t* solver, thvar_t v) { 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(mcarith_solver_terms(solver), tp); + t = new_uninterpreted_term(terms, tp); } break; case AVARTAG_KIND_POLY: @@ -451,11 +460,11 @@ term_t get_term(mcarith_solver_t* solver, thvar_t v) { if (j == 0 && p->mono[j].var == const_idx) { rba_buffer_add_const(&b, r); } else { - term_t t = get_term(solver, p->mono[j].var); - rba_buffer_add_mono(&b, r, var_pp(t)); + thvar_t v = p->mono[j].var; + rba_buffer_add_mono_mcarithvar(solver, &b, r, v); } } - t = arith_poly(mcarith_solver_terms(solver), &b); + t = arith_poly(terms, &b); } break; case AVARTAG_KIND_PPROD: @@ -463,7 +472,7 @@ term_t get_term(mcarith_solver_t* solver, thvar_t v) { longjmp(*solver->simplex.env, INTERNAL_ERROR); break; case AVARTAG_KIND_CONST: - t = arith_constant(mcarith_solver_terms(solver), table->def[v]); + t = arith_constant(terms, table->def[v]); break; default: longjmp(*solver->simplex.env, INTERNAL_ERROR); @@ -472,24 +481,86 @@ term_t get_term(mcarith_solver_t* solver, thvar_t v) { return t; } -/* This addsthe theory var value to the buffer while ensuring a nested polynomial term is not created. */ +/* 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 = &solver->simplex.vtbl; +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: { - polynomial_t* p = table->def[v]; + p = table->def[v]; uint32_t n = p->nterms; for (uint32_t j = 0; j < n; ++j) { - rational_t* r = &p->mono[j].coeff; + 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, r); + 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 { - term_t t = get_term(solver, p->mono[j].var); - rba_buffer_add_mono(b, r, var_pp(t)); + rba_buffer_add_mono_mcarithvar(solver, b, c, mv); } } break; @@ -502,28 +573,46 @@ void rba_buffer_add_mcarithvar(mcarith_solver_t* solver, rba_buffer_t* b, thvar_ rba_buffer_add_const(b, table->def[v]); break; default: - rba_buffer_add_pp(b, var_pp(get_term(solver, v))); + 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 = &solver->simplex.vtbl; + 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: { - polynomial_t* p = table->def[v]; - 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_sub_const(b, r); + 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 { - term_t t = get_term(solver, p->mono[j].var); - rba_buffer_sub_mono(b, r, var_pp(t)); + q_init(&aux); + q_set(&aux, c); + q_neg(&aux); + rba_buffer_add_mono_mcarithvar(solver, b, &aux, mv); + q_clear(&aux); } } break; @@ -536,7 +625,9 @@ void rba_buffer_sub_mcarithvar(mcarith_solver_t* solver, rba_buffer_t* b, thvar_ rba_buffer_sub_const(b, table->def[v]); break; default: - rba_buffer_sub_pp(b, var_pp(get_term(solver, v))); + t = get_term(solver, v); + assert(term_kind(terms, t) != ARITH_POLY); + rba_buffer_sub_pp(b, var_pp(t)); } } @@ -545,57 +636,70 @@ void rba_buffer_sub_mcarithvar(mcarith_solver_t* solver, rba_buffer_t* b, thvar_ */ 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; + term_t polyTerm; + + mcarith_check_atom_size(solver); - arith_atomtable_t *atbl = &solver->simplex.atbl; + atbl = &solver->simplex.atbl; assert(0 <= atom_index && atom_index < atbl->natoms); - term_t p = solver->atom_terms[atom_index]; - if (p != NULL_TERM) return p; + result = solver->atom_terms[atom_index]; + if (result != NULL_TERM) return result; - arith_atom_t* ap = atbl->atoms + atom_index; - rational_t* bnd = bound_of_atom(ap); - term_table_t* terms = mcarith_solver_terms(solver); + 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: { - term_t polyTerm; if (q_is_zero(bnd)) { polyTerm = get_term(solver, var_of_atom(ap)); } else { - rba_buffer_t b; + // Create buffer b = v - bnd init_rba_buffer(&b, mcarith_solver_pprods(solver)); - rba_buffer_add_mcarithvar(solver, &b, var_of_atom(ap)); + rba_buffer_add_mcarithvar(solver, &b, v); rba_buffer_sub_const(&b, bnd); + // Create term and free buffer. polyTerm = arith_poly(terms, &b); delete_rba_buffer(&b); } - p = arith_geq_atom(terms, polyTerm); + result = arith_geq_atom(terms, polyTerm); break; } // Assert v <= b by asserting b-v >= 0 case LE_ATM: { - rba_buffer_t b; + // Create buffer b = bnd - v init_rba_buffer(&b, mcarith_solver_pprods(solver)); - rba_buffer_sub_mcarithvar(solver, &b, var_of_atom(ap)); + rba_buffer_sub_mcarithvar(solver, &b, v); rba_buffer_add_const(&b, bnd); - term_t polyTerm = arith_poly(terms, &b); + polyTerm = arith_poly(terms, &b); delete_rba_buffer(&b); - p = arith_geq_atom(terms, polyTerm); + result = arith_geq_atom(terms, polyTerm); break; } // Assert v == bnd case EQ_ATM: { - term_t t = get_term(solver, var_of_atom(ap)); - p = arith_bineq_atom(terms, t, arith_constant(terms, bnd)); + 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] = p; - return p; + solver->atom_terms[atom_index] = result; + return result; } /* @@ -725,8 +829,9 @@ void init_rba_buffer_from_poly(mcarith_solver_t* solver, if (j == 0 && p->mono[j].var == const_idx) { rba_buffer_add_const(b, &p->mono[j].coeff); } else { - pprod_t* pp = var_pp(get_term(solver, p->mono[j].var)); - rba_buffer_add_mono(b, &p->mono[j].coeff, pp); + rational_t* c = &p->mono[j].coeff; + thvar_t v = p->mono[j].var; + rba_buffer_add_mono_mcarithvar(solver, b, c, v); } } } @@ -974,40 +1079,12 @@ static th_smt_interface_t mcarith_smt = { * - arith_map maps variables of p to corresponding theory variables * in the solver */ -thvar_t mcarith_create_poly(mcarith_solver_t *solver, polynomial_t *p, thvar_t *map) { - return simplex_create_poly(&solver->simplex, p, map); -} - -/* - * Create the atom x == 0 - * - this attach the atom to the smt_core - */ -literal_t mcarith_create_eq_atom(mcarith_solver_t *solver, thvar_t x) { - return simplex_create_eq_atom(&solver->simplex, x); -} - -/* - * Create the atom x >= 0 - * - this attach the atom to the smt_core - */ -literal_t mcarith_create_ge_atom(mcarith_solver_t *solver, thvar_t x) { - return simplex_create_ge_atom(&solver->simplex, x); -} - -/* - * Create the atom p == 0 - * - apply the renaming defined by map - */ -literal_t mcarith_create_poly_eq_atom(mcarith_solver_t *solver, polynomial_t *p, thvar_t *map) { - return simplex_create_poly_eq_atom(&solver->simplex, p, map); -} +static +thvar_t mcarith_create_poly(void* s, polynomial_t *p, thvar_t *map) { + mcarith_solver_t *solver; -/* - * Create the atom p >= 0 and return the corresponding literal - * - replace the variables of p as defined by map - */ -literal_t mcarith_create_poly_ge_atom(mcarith_solver_t *solver, polynomial_t *p, thvar_t *map) { - return simplex_create_poly_ge_atom(&solver->simplex, p, map); + solver = s; + return simplex_create_poly(&solver->simplex, p, map); } /* @@ -1016,11 +1093,15 @@ literal_t mcarith_create_poly_ge_atom(mcarith_solver_t *solver, polynomial_t *p, * tt == true --> assert x == 0 * tt == false --> assert x != 0 */ -void mcarith_assert_eq_axiom(mcarith_solver_t *solver, thvar_t x, bool tt) { +static void mcarith_assert_eq_axiom(void* s, thvar_t x, bool tt) { + mcarith_solver_t *solver; + mcarith_assertion_t* assert; + + solver = s; simplex_assert_eq_axiom(&solver->simplex, x, tt); // Record assertion for sending to mcarith solver. - mcarith_assertion_t* assert = alloc_top_assertion(solver); + assert = alloc_top_assertion(solver); assert->type = VAR_EQ0; assert->def.var = x; assert->tt = tt; @@ -1033,10 +1114,14 @@ void mcarith_assert_eq_axiom(mcarith_solver_t *solver, thvar_t x, bool tt) { * tt == true --> assert x >= 0 * tt == false --> assert x < 0 */ -void mcarith_assert_ge_axiom(mcarith_solver_t *solver, thvar_t x, bool tt){ +static void mcarith_assert_ge_axiom(void* s, thvar_t x, bool tt){ + mcarith_solver_t *solver; + mcarith_assertion_t* assert; + + solver = s; simplex_assert_ge_axiom(&solver->simplex, x, tt); - mcarith_assertion_t* assert = alloc_top_assertion(solver); + assert = alloc_top_assertion(solver); assert->type = VAR_GE0; assert->def.var = x; assert->tt = tt; @@ -1049,12 +1134,16 @@ void mcarith_assert_ge_axiom(mcarith_solver_t *solver, thvar_t x, bool tt){ * - if tt is true ---> assert p == 0 * - if tt is false ---> assert p != 0 */ -void mcarith_assert_poly_eq_axiom(mcarith_solver_t *solver, polynomial_t *p, thvar_t *map, bool tt) { +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_assert_poly_eq_axiom(&solver->simplex, p, map, tt); - mcarith_assertion_t* assert = alloc_top_assertion(solver); + assert = alloc_top_assertion(solver); assert->type = POLY_EQ0; assert->def.poly = alloc_polynomial_from_map(p, map, solver->simplex.vtbl.nvars); assert->tt = tt; @@ -1066,12 +1155,16 @@ void mcarith_assert_poly_eq_axiom(mcarith_solver_t *solver, polynomial_t *p, thv * - 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. */ -void mcarith_assert_poly_ge_axiom(mcarith_solver_t *solver, polynomial_t *p, thvar_t *map, bool tt) { +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_assert_poly_ge_axiom(&solver->simplex, p, map, tt); - mcarith_assertion_t* assert = alloc_top_assertion(solver); + assert = alloc_top_assertion(solver); assert->type = POLY_GE0; assert->def.poly = alloc_polynomial_from_map(p, map, solver->simplex.vtbl.nvars); assert->tt = tt; @@ -1082,10 +1175,15 @@ void mcarith_assert_poly_ge_axiom(mcarith_solver_t *solver, polynomial_t *p, thv * If tt == true --> assert (x - y == 0) * If tt == false --> assert (x - y != 0) */ -void mcarith_assert_vareq_axiom(mcarith_solver_t *solver, thvar_t x, thvar_t y, bool tt) { +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_assert_vareq_axiom(&solver->simplex, x, y, tt); - mcarith_assertion_t* assert = alloc_top_assertion(solver); + assert = alloc_top_assertion(solver); assert->type = VAR_EQ; assert->def.eq.lhs = x; assert->def.eq.rhs = y; @@ -1096,40 +1194,31 @@ void mcarith_assert_vareq_axiom(mcarith_solver_t *solver, thvar_t x, thvar_t y, /* * Assert (c ==> x == y) */ -void mcarith_assert_cond_vareq_axiom(mcarith_solver_t *solver, literal_t c, thvar_t x, thvar_t 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_assert_cond_vareq_axiom(&solver->simplex, c, x, y); } /* * Assert (c[0] \/ ... \/ c[n-1] \/ x == y) */ -void mcarith_assert_clause_vareq_axiom(mcarith_solver_t *solver, uint32_t n, literal_t *c, thvar_t x, thvar_t 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_assert_clause_vareq_axiom(&solver->simplex, n, c, x, y); } /* * Get the type of variable x */ -bool mcarith_var_is_integer(mcarith_solver_t *solver, thvar_t 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); } -/* - * Attach egraph term t to a variable v - * - v must not have an eterm attached already - */ -static void mcarith_attach_eterm(mcarith_solver_t *solver, thvar_t v, eterm_t t) { - simplex_attach_eterm(&solver->simplex, v, t); -} - -/* - * Get the egraph term t attached to v - * - return null_eterm if v has no eterm attached - */ -static eterm_t mcarith_eterm_of_var(mcarith_solver_t *solver, thvar_t v) { - return simplex_eterm_of_var(&solver->simplex, v); -} - #pragma region Models /* @@ -1212,32 +1301,32 @@ bool mcarith_value_in_model(void* s, thvar_t x, arithval_in_model_t* res) { static arith_interface_t mcarith_context = { .create_var = (create_arith_var_fun_t) simplex_create_var, .create_const = (create_arith_const_fun_t) simplex_create_const, - .create_poly = (create_arith_poly_fun_t) mcarith_create_poly, + .create_poly = mcarith_create_poly, .create_pprod = mcarith_create_pprod, .create_rdiv = mcarith_create_rdiv, - .create_eq_atom = (create_arith_atom_fun_t) mcarith_create_eq_atom, - .create_ge_atom = (create_arith_atom_fun_t) mcarith_create_ge_atom, - .create_poly_eq_atom = (create_arith_patom_fun_t) mcarith_create_poly_eq_atom, - .create_poly_ge_atom = (create_arith_patom_fun_t) mcarith_create_poly_ge_atom, + .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 = (assert_arith_axiom_fun_t) mcarith_assert_eq_axiom, - .assert_ge_axiom = (assert_arith_axiom_fun_t) mcarith_assert_ge_axiom, - .assert_poly_eq_axiom = (assert_arith_paxiom_fun_t) mcarith_assert_poly_eq_axiom, - .assert_poly_ge_axiom = (assert_arith_paxiom_fun_t) mcarith_assert_poly_ge_axiom, - .assert_vareq_axiom = (assert_arith_vareq_axiom_fun_t) mcarith_assert_vareq_axiom, - .assert_cond_vareq_axiom = (assert_arith_cond_vareq_axiom_fun_t) mcarith_assert_cond_vareq_axiom, - .assert_clause_vareq_axiom = (assert_arith_clause_vareq_axiom_fun_t) mcarith_assert_clause_vareq_axiom, + .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) mcarith_attach_eterm, - .eterm_of_var = (eterm_of_var_fun_t) mcarith_eterm_of_var, + .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 = (arith_var_is_int_fun_t) mcarith_var_is_integer, + .arith_var_is_int = mcarith_var_is_integer, }; /* From c49758c169ab4e5777bb3bd760e7a619a9b00f8b Mon Sep 17 00:00:00 2001 From: Joe Hendrix Date: Wed, 12 Jan 2022 10:51:53 -0800 Subject: [PATCH 07/10] mcarith push/pop support. --- src/context/context.c | 4 +- src/solvers/mcarith/mcarith.c | 107 +++++++++++++++++++++++++--------- src/solvers/mcarith/mcarith.h | 8 ++- 3 files changed, 87 insertions(+), 32 deletions(-) diff --git a/src/context/context.c b/src/context/context.c index 881b214f9..849ae8a9c 100644 --- a/src/context/context.c +++ b/src/context/context.c @@ -5360,9 +5360,7 @@ static void create_mcarith_solver(context_t *ctx) { // row saving must be enabled unless we're in ONECHECK mode if (ctx->mode != CTX_MODE_ONECHECK) { - longjmp(ctx->env, INTERNAL_ERROR); - -// simplex_enable_row_saving(solver); + simplex_enable_row_saving(solver); } if (ctx->egraph != NULL) { diff --git a/src/solvers/mcarith/mcarith.c b/src/solvers/mcarith/mcarith.c index f899b6874..77d5eb8d3 100644 --- a/src/solvers/mcarith/mcarith.c +++ b/src/solvers/mcarith/mcarith.c @@ -34,10 +34,10 @@ #include "yices.h" -extern void simplex_attach_eterm(simplex_solver_t *solver, thvar_t v, eterm_t t); -extern thvar_t simplex_create_const(simplex_solver_t *solver, rational_t *q); -extern eterm_t simplex_eterm_of_var(simplex_solver_t *solver, thvar_t v); -extern void simplex_start_internalization(simplex_solver_t *solver); +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); @@ -182,7 +182,7 @@ static void mcarith_undo_push_record(mcarith_undo_stack_t* stack, uint32_t n_a) } /* - * Push an undo record to the stack. + * 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); @@ -273,6 +273,10 @@ struct mcarith_solver_s { 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) { @@ -430,11 +434,12 @@ term_t get_term(mcarith_solver_t* solver, thvar_t v) { arith_vartable_t* table; term_table_t* terms; - terms = mcarith_solver_terms(solver); table = &solver->simplex.vtbl; assert(0 <= v && v < table->nvars); + terms = mcarith_solver_terms(solver); + term_t t = solver->var_terms[v]; if (t != NULL_TERM) return t; @@ -763,17 +768,15 @@ thvar_t mcarith_create_rdiv(void *s, thvar_t num, thvar_t den) { static mcarith_assertion_t* alloc_top_assertion(mcarith_solver_t* s) { size_t cnt = s->assertion_count; - if (cnt < s->assertion_capacity) { - ++s->assertion_count; - return s->assertions + cnt; - } else { + 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)); - return s->assertions + cnt; } + s->assertion_count = cnt + 1; + return s->assertions + cnt; } /******************************** @@ -840,27 +843,51 @@ void init_rba_buffer_from_poly(mcarith_solver_t* solver, * Check for integer feasibility */ static -fcheck_code_t mcarith_final_check(mcarith_solver_t *solver) { +fcheck_code_t mcarith_final_check(void* s) { + mcarith_solver_t *solver; + term_table_t* terms; + uint32_t acnt; + + + solver = s; + terms = mcarith_solver_terms(solver); + + yices_pp_t printer; + pp_area_t area; + + area.width = 72; + area.height = 8; + area.offset = 2; + area.stretch = false; + area.truncate = true; + + init_default_yices_pp(&printer, stdout, &area); + mcarith_free_mcsat(solver); const bool qflag = false; // Quantifiers not allowed - term_table_t* terms = mcarith_solver_terms(solver); init_context(&solver->mcsat_ctx, terms, QF_NRA, CTX_MODE_ONECHECK, CTX_ARCH_MCSAT, qflag); solver->mcsat = mcsat_new(&solver->mcsat_ctx); - term_t* assertions = safe_malloc(sizeof(term_t) * (solver->assertion_count + 1)); - literal_t* literals = safe_malloc(sizeof(literal_t) * (solver->assertion_count + 1)); + acnt = solver->assertion_count; + term_t* assertions = safe_malloc(sizeof(term_t) * (acnt + 1)); + literal_t* literals = safe_malloc(sizeof(literal_t) * acnt); size_t literal_count = 0; mcarith_check_var_size(solver); - for (size_t i = 0; i < solver->assertion_count; ++i) { + for (size_t i = 0; i < acnt; ++i) { mcarith_assertion_t* a = solver->assertions + i; rba_buffer_t b; term_t p; switch (a->type) { - case VAR_EQ: - p = arith_bineq_atom(terms, get_term(solver, a->def.eq.lhs), get_term(solver, a->def.eq.rhs)); + case VAR_EQ: { + term_t lhs; + term_t rhs; + lhs = get_term(solver, a->def.eq.lhs); + rhs = get_term(solver, a->def.eq.rhs); + p = arith_bineq_atom(terms, lhs, rhs); break; + } case VAR_EQ0: p = arith_eq_atom(terms, get_term(solver, a->def.var)); break; @@ -890,10 +917,9 @@ fcheck_code_t mcarith_final_check(mcarith_solver_t *solver) { } assertions[i] = a->tt ? p : not_term(terms, p); } - assertions[solver->assertion_count] = assertions[solver->assertion_count-1]; literals[literal_count] = end_clause; - int32_t r = mcsat_assert_formulas(solver->mcsat, solver->assertion_count+1, assertions); + int32_t r = mcsat_assert_formulas(solver->mcsat, acnt, assertions); fcheck_code_t result; if (r == TRIVIALLY_UNSAT) { record_theory_conflict(solver->simplex.core, literals); @@ -971,7 +997,6 @@ void mcarith_backtrack(mcarith_solver_t *solver, uint32_t back_level) { * Start a new base level */ static void mcarith_push(mcarith_solver_t *solver) { - assert(0); simplex_push(&solver->simplex); mcarith_undo_push_record(&solver->undo_stack, solver->assertion_count); } @@ -980,11 +1005,23 @@ static void mcarith_push(mcarith_solver_t *solver) { * Return to the previous base level */ void mcarith_pop(mcarith_solver_t *solver) { + uint32_t vc; + uint32_t vc0; + term_t* t; + term_t* end; + mcarith_undo_record_t* r; // Reset assertions - mcarith_undo_record_t* r = mcarith_undo_pop_record(&solver->undo_stack); + 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); + vc0 = solver->simplex.vtbl.nvars; + + end = solver->var_terms + vc; + for (t = solver->var_terms + vc0; t != end; ++t) { + *t = NULL_TERM; + } } /* @@ -1007,7 +1044,7 @@ 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 = (final_check_fun_t) mcarith_final_check, + .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, @@ -1074,6 +1111,16 @@ static th_smt_interface_t mcarith_smt = { .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 @@ -1231,7 +1278,8 @@ static void mcarith_build_model(void* s) { assert(solver->mcsat); assert(!solver->model); // Create model - model = yices_new_model(); + model = safe_malloc(sizeof(model_t)); + init_model(model, mcarith_solver_terms(solver), true); mcsat_build_model(solver->mcsat, model); solver->model = model; @@ -1242,10 +1290,12 @@ static void mcarith_build_model(void* s) { * Free the model */ static void mcarith_free_model(void* s) { - mcarith_solver_t* solver = s; - assert(solver->model); + mcarith_solver_t* solver; - yices_free_model(solver->model); + solver = s; + assert(solver->model); + delete_model(solver->model); + free(solver->model); solver->model = 0; } @@ -1280,6 +1330,7 @@ bool mcarith_value_in_model(void* s, thvar_t x, arithval_in_model_t* res) { 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); @@ -1300,7 +1351,7 @@ bool mcarith_value_in_model(void* s, thvar_t x, arithval_in_model_t* res) { static arith_interface_t mcarith_context = { .create_var = (create_arith_var_fun_t) simplex_create_var, - .create_const = (create_arith_const_fun_t) simplex_create_const, + .create_const = mcarith_create_const, .create_poly = mcarith_create_poly, .create_pprod = mcarith_create_pprod, .create_rdiv = mcarith_create_rdiv, diff --git a/src/solvers/mcarith/mcarith.h b/src/solvers/mcarith/mcarith.h index cd5b3934d..3b9a5ed65 100644 --- a/src/solvers/mcarith/mcarith.h +++ b/src/solvers/mcarith/mcarith.h @@ -37,8 +37,14 @@ typedef struct mcarith_solver_s mcarith_solver_t; */ 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); From c017ba4990edf9e776ba3f41d4dfefe91146991a Mon Sep 17 00:00:00 2001 From: Joe Hendrix Date: Wed, 12 Jan 2022 22:50:47 -0800 Subject: [PATCH 08/10] Bugfixes to mcarith --- src/context/context.c | 2 +- src/solvers/mcarith/mcarith.c | 185 ++++++++++++++++++++++++++++------ 2 files changed, 156 insertions(+), 31 deletions(-) diff --git a/src/context/context.c b/src/context/context.c index 849ae8a9c..ffac2458c 100644 --- a/src/context/context.c +++ b/src/context/context.c @@ -5360,7 +5360,7 @@ static void create_mcarith_solver(context_t *ctx) { // row saving must be enabled unless we're in ONECHECK mode if (ctx->mode != CTX_MODE_ONECHECK) { - simplex_enable_row_saving(solver); + mcarith_enable_row_saving(solver); } if (ctx->egraph != NULL) { diff --git a/src/solvers/mcarith/mcarith.c b/src/solvers/mcarith/mcarith.c index 77d5eb8d3..8e344b5eb 100644 --- a/src/solvers/mcarith/mcarith.c +++ b/src/solvers/mcarith/mcarith.c @@ -429,6 +429,29 @@ void mcarith_check_atom_size(mcarith_solver_t *solver) { 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); +} + static term_t get_term(mcarith_solver_t* solver, thvar_t v) { arith_vartable_t* table; @@ -469,7 +492,7 @@ term_t get_term(mcarith_solver_t* solver, thvar_t v) { rba_buffer_add_mono_mcarithvar(solver, &b, r, v); } } - t = arith_poly(terms, &b); + t = mcarith_poly(terms, &b); } break; case AVARTAG_KIND_PPROD: @@ -648,8 +671,6 @@ term_t get_atom(mcarith_solver_t* solver, int32_t atom_index) { term_t v; rational_t* bnd; rba_buffer_t b; - term_t polyTerm; - mcarith_check_atom_size(solver); @@ -671,26 +692,31 @@ term_t get_atom(mcarith_solver_t* solver, int32_t atom_index) { // Assert v-b >= 0 case GE_ATM: { if (q_is_zero(bnd)) { - polyTerm = get_term(solver, var_of_atom(ap)); + 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 = arith_poly(terms, &b); + polyTerm = mcarith_poly(terms, &b); delete_rba_buffer(&b); + result = arith_geq_atom(terms, polyTerm); } - 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 = arith_poly(terms, &b); + polyTerm = mcarith_poly(terms, &b); delete_rba_buffer(&b); result = arith_geq_atom(terms, polyTerm); break; @@ -716,24 +742,30 @@ thvar_t mcarith_create_pprod(void *s, pprod_t *p, thvar_t *map) { 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 < p->len; ++i) { thvar_t mv = map[i]; assert(mv < v); - term_t t = get_term(solver, mv); - pp_buffer_set_varexp(&b, t, p->prod[i].exp); + vars[i] = get_term(solver, mv); + exps[i] = p->prod[i].exp; } - pp_buffer_normalize(&b); + pp_buffer_set_varexps(&b, n, vars, exps); + free(vars); + free(exps); - // Create term assert(solver->var_terms_size > v); - solver->var_terms[v] = pprod_term_from_buffer(mcarith_solver_terms(solver), &b); + + term_t t = pprod_term_from_buffer(mcarith_solver_terms(solver), &b); + solver->var_terms[v] = t; // Free buffer and return delete_pp_buffer(&b); return v; @@ -839,6 +871,23 @@ void init_rba_buffer_from_poly(mcarith_solver_t* solver, } } +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; +} + + /* * Check for integer feasibility */ @@ -847,21 +896,18 @@ fcheck_code_t mcarith_final_check(void* s) { mcarith_solver_t *solver; term_table_t* terms; uint32_t acnt; - + term_t t; solver = s; terms = mcarith_solver_terms(solver); + assert(!solver->simplex.unsat_before_search); - yices_pp_t printer; - pp_area_t area; - - area.width = 72; - area.height = 8; - area.offset = 2; - area.stretch = false; - area.truncate = true; + fcheck_code_t result; - init_default_yices_pp(&printer, stdout, &area); + result = simplex_final_check(&solver->simplex); + if (result == FCHECK_CONTINUE) { + return result; + } mcarith_free_mcsat(solver); @@ -892,18 +938,40 @@ fcheck_code_t mcarith_final_check(void* s) { p = arith_eq_atom(terms, get_term(solver, a->def.var)); break; case VAR_GE0: - p = arith_geq_atom(terms, get_term(solver, a->def.var)); + t = get_term(solver, a->def.var); + assert(term_kind(terms, t) != ARITH_CONSTANT); + p = arith_geq_atom(terms, t); break; - case POLY_EQ0: + case POLY_EQ0: { + rational_t br; + init_rba_buffer_from_poly(solver, &b, a->def.poly); - p = arith_eq_atom(terms, arith_poly(terms, &b)); + 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); break; - case POLY_GE0: + } + case POLY_GE0: { + rational_t br; + init_rba_buffer_from_poly(solver, &b, a->def.poly); - p = arith_geq_atom(terms, arith_poly(terms, &b)); + 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); break; + } case ATOM_ASSERT: p = get_atom(solver, a->def.atom); break; @@ -920,10 +988,9 @@ fcheck_code_t mcarith_final_check(void* s) { literals[literal_count] = end_clause; int32_t r = mcsat_assert_formulas(solver->mcsat, acnt, assertions); - fcheck_code_t result; if (r == TRIVIALLY_UNSAT) { record_theory_conflict(solver->simplex.core, literals); - mcarith_free_mcsat(solver); + mcarith_free_mcsat(solver); result = FCHECK_CONTINUE; } else if (r == CTX_NO_ERROR) { result = FCHECK_SAT; @@ -990,7 +1057,10 @@ void mcarith_increase_decision_level(mcarith_solver_t *solver) { 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); + uint32_t vc0 = solver->simplex.vtbl.nvars; + assert(vc == vc0); } /* @@ -1028,7 +1098,10 @@ void mcarith_pop(mcarith_solver_t *solver) { * Reset to the empty solver */ void mcarith_reset(mcarith_solver_t *solver) { + uint32_t vc = solver->simplex.vtbl.nvars; simplex_reset(&solver->simplex); + uint32_t vc0 = solver->simplex.vtbl.nvars; + assert(vc == vc0); // FIXME mcarith_undo_reset(&solver->undo_stack); mcarith_backtrack_assertions(solver, 0); @@ -1134,6 +1207,27 @@ thvar_t mcarith_create_poly(void* s, polynomial_t *p, thvar_t *map) { 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 @@ -1145,7 +1239,11 @@ static void mcarith_assert_eq_axiom(void* s, thvar_t x, bool tt) { 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); @@ -1166,7 +1264,11 @@ static void mcarith_assert_ge_axiom(void* s, thvar_t x, bool tt){ 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; @@ -1188,10 +1290,15 @@ static void mcarith_assert_poly_eq_axiom(void * s, polynomial_t *p, thvar_t *map 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; @@ -1209,10 +1316,15 @@ static void mcarith_assert_poly_ge_axiom(void *s, polynomial_t *p, thvar_t *map, 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; @@ -1228,7 +1340,10 @@ void mcarith_assert_vareq_axiom(void* s, thvar_t x, thvar_t y, bool tt) { 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; @@ -1245,7 +1360,12 @@ 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); } /* @@ -1254,7 +1374,12 @@ void mcarith_assert_cond_vareq_axiom(void* s, literal_t c, thvar_t x, thvar_t 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); } /* From b2eb4fc902c75608b52d7ea1bd17108febc59d7a Mon Sep 17 00:00:00 2001 From: Joe Hendrix Date: Tue, 26 Sep 2023 12:00:53 -0700 Subject: [PATCH 09/10] Bugfixes and cleanups to support backtracing in mcarith. --- src/api/yices_api.c | 2 + src/context/context.c | 14 +- src/context/context_solver.c | 1 - src/context/context_types.h | 23 ++- src/solvers/mcarith/mcarith.c | 301 ++++++++++++++++++++-------------- src/solvers/mcarith/mcarith.h | 4 +- 6 files changed, 197 insertions(+), 148 deletions(-) diff --git a/src/api/yices_api.c b/src/api/yices_api.c index 787fdcced..ff4f915c1 100644 --- a/src/api/yices_api.c +++ b/src/api/yices_api.c @@ -10772,9 +10772,11 @@ static void yices_get_arith_value(model_t *mdl, term_t t, arithval_struct_t *r) if (object_is_rational(vtbl, v)) { r->tag = ARITHVAL_RATIONAL; r->val.q = vtbl_rational(vtbl, v); +#ifdef HAVE_MCSAT } else if (object_is_algebraic(vtbl, v)) { r->tag = ARITHVAL_ALGEBRAIC; r->val.p = vtbl_algebraic_number(vtbl, v); +#endif } else { // should not happen since t is an arithmetic term set_error_code(INTERNAL_EXCEPTION); diff --git a/src/context/context.c b/src/context/context.c index ffac2458c..f4c08b1d0 100644 --- a/src/context/context.c +++ b/src/context/context.c @@ -5349,6 +5349,7 @@ static void create_simplex_solver(context_t *ctx, bool automatic) { * Create an initialize the simplex solver and attach it to the core * or to the egraph if the egraph exists. */ +#ifdef HAVE_MCSAT static void create_mcarith_solver(context_t *ctx) { mcarith_solver_t *solver; smt_mode_t cmode; @@ -5380,7 +5381,12 @@ static void create_mcarith_solver(context_t *ctx) { ctx->arith_solver = solver; ctx->arith = *mcarith_arith_interface(solver); } - +#else +static void create_mcarith_solver(context_t *ctx) { + fprintf(stderr, "mcarithmetic solver not supported.\n"); + exit(-1); +} +#endif /* * Create IDL/SIMPLEX solver based on ctx->dl_profile @@ -5777,9 +5783,6 @@ void init_context(context_t *ctx, term_table_t *terms, smt_logic_t logic, ctx->en_quant = false; } - -void arithval_in_model_delete(arithval_in_model_t* v); - void arithval_in_model_delete(arithval_in_model_t* v) { switch (v->tag) { case ARITHVAL_RATIONAL: @@ -5802,8 +5805,7 @@ void arithval_in_model_reset(arithval_in_model_t* v) { break; #ifdef HAVE_MCSAT case ARITHVAL_ALGEBRAIC: - lp_algebraic_number_destruct(&v-> - val.alg_number); + lp_algebraic_number_destruct(&v->val.alg_number); v->tag = ARITHVAL_RATIONAL; q_init(&v->val.q); break; diff --git a/src/context/context_solver.c b/src/context/context_solver.c index 5ea55ed8f..17ce6f0da 100644 --- a/src/context/context_solver.c +++ b/src/context/context_solver.c @@ -887,7 +887,6 @@ static value_t bool_value(context_t *ctx, value_table_t *vtbl, literal_t l) { return v; } - /* * Value of arithmetic variable x in ctx->arith_solver */ diff --git a/src/context/context_types.h b/src/context/context_types.h index 8302d6ba6..5b130b8b1 100644 --- a/src/context/context_types.h +++ b/src/context/context_types.h @@ -258,25 +258,14 @@ enum { typedef enum arithval_tag { ARITHVAL_ERROR, ARITHVAL_RATIONAL, -#ifdef HAVE_MCSAT ARITHVAL_ALGEBRAIC, -#endif } arithval_tag_t; /* * Tagged union to represent pointers to either rational or algebraic numbers. * The flag can ERROR/RATIONAL/ALGEBRAIC */ -typedef struct { - arithval_tag_t tag; - union { - rational_t q; -#ifdef HAVE_MCSAT - lp_algebraic_number_t alg_number; -#endif - } val; -} arithval_in_model_t; - +typedef struct arithval_in_model_s arithval_in_model_t; /************************** * ARITHMETIC INTERFACE * @@ -662,6 +651,16 @@ typedef struct dl_data_s { * CONTEXT * *************/ +struct arithval_in_model_s { + arithval_tag_t tag; + union { + rational_t q; +#ifdef HAVE_MCSAT + lp_algebraic_number_t alg_number; +#endif + } val; +}; + struct context_s { // mode + architecture + logic code context_mode_t mode; diff --git a/src/solvers/mcarith/mcarith.c b/src/solvers/mcarith/mcarith.c index 8e344b5eb..af674bd42 100644 --- a/src/solvers/mcarith/mcarith.c +++ b/src/solvers/mcarith/mcarith.c @@ -21,6 +21,7 @@ * * Uses MCSAT to implement a non-linear arithmetic solver. */ +#ifdef HAVE_MCSAT #include "context/context.h" #include "solvers/mcarith/mcarith.h" @@ -253,10 +254,7 @@ struct mcarith_solver_s { // Term Table for mcsat term_table_t* terms; #endif - // Size of var_terms array - uint32_t var_terms_size; - // Map theory variables to term so we can send them to MCSat - term_t* var_terms; + ivector_t var_terms; // Size of atom term array uint32_t atom_terms_size; @@ -270,6 +268,10 @@ struct mcarith_solver_s { // 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; }; @@ -309,6 +311,10 @@ term_table_t* mcarith_solver_terms(mcarith_solver_t* s) { } #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 */ @@ -338,12 +344,11 @@ void init_mcarith_solver(mcarith_solver_t **solver, context_t* ctx) { // Create array for mapping theory variables to initial term. assert(s->simplex.vtbl.nvars == 1); - s->var_terms = safe_malloc(sizeof(term_t)); - s->var_terms_size = 1; + init_ivector(&s->var_terms, s->simplex.vtbl.size); rational_t one; + q_init(&one); q_set_one(&one); - s->var_terms[0] = arith_constant(mcarith_solver_terms(s), &one); - + ivector_push(&s->var_terms, arith_constant(mcarith_solver_terms(s), &one)); s->atom_terms = 0; s->atom_terms_size = 0; @@ -354,8 +359,10 @@ void init_mcarith_solver(mcarith_solver_t **solver, context_t* ctx) { s->assertion_count = 0; // Create undo stack - const uint32_t init_undo_stack_size = 32; - init_mcarith_undo_stack(&s->undo_stack, init_undo_stack_size); + 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; } @@ -370,16 +377,32 @@ void mcarith_free_mcsat(mcarith_solver_t* s) { } } +/* + * 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 - safe_free(s->var_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); @@ -412,8 +435,20 @@ void realloc_term_array(uint32_t* size_ptr, term_t** term_array, uint32_t new_si */ static inline void mcarith_check_var_size(mcarith_solver_t *solver) { - uint32_t new_size = solver->simplex.vtbl.size; - realloc_term_array(&solver->var_terms_size, &solver->var_terms, new_size); + 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; } /* @@ -452,20 +487,42 @@ term_t mcarith_poly(term_table_t* terms, rba_buffer_t* b) { 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); - term_t t = solver->var_terms[v]; - if (t != NULL_TERM) return t; - + 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; @@ -475,6 +532,7 @@ term_t get_term(mcarith_solver_t* solver, thvar_t v) { { 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: @@ -493,6 +551,7 @@ term_t get_term(mcarith_solver_t* solver, thvar_t v) { } } t = mcarith_poly(terms, &b); + assert(good_term(terms, t)); } break; case AVARTAG_KIND_PPROD: @@ -501,11 +560,12 @@ term_t get_term(mcarith_solver_t* solver, thvar_t v) { 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); } - solver->var_terms[v] = t; + term_ivector_grow_set(&solver->var_terms, v, t); return t; } @@ -739,6 +799,8 @@ term_t get_atom(mcarith_solver_t* solver, int32_t atom_index) { 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)); @@ -752,20 +814,22 @@ thvar_t mcarith_create_pprod(void *s, pprod_t *p, thvar_t *map) { int32_t* vars = safe_malloc(sizeof(int32_t) * n); uint32_t* exps = safe_malloc(sizeof(uint32_t) * n); - for (uint32_t i = 0; i < p->len; ++i) { + for (uint32_t i = 0; i < n; ++i) { thvar_t mv = map[i]; + term_t t; assert(mv < v); - vars[i] = get_term(solver, mv); + 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_size > v); + assert(solver->var_terms.capacity > v); - term_t t = pprod_term_from_buffer(mcarith_solver_terms(solver), &b); - solver->var_terms[v] = t; + 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; @@ -789,7 +853,7 @@ thvar_t mcarith_create_rdiv(void *s, thvar_t num, thvar_t den) { mcarith_check_var_size(solver); nt = get_term(solver, num); dt = get_term(solver, den); - solver->var_terms[v] = arith_rdiv(mcarith_solver_terms(solver), nt, dt); + term_ivector_grow_set(&solver->var_terms, v, arith_rdiv(mcarith_solver_terms(solver), nt, dt)); return v; } @@ -887,6 +951,72 @@ bool rba_buffer_get_const(rba_buffer_t* b, rational_t* r) { 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); + } +} + +static +void init_conflict(ivector_t* conflict, mcarith_solver_t *solver) { + ivector_reset(conflict); + uint32_t acnt = solver->assertion_count; + 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); +} /* * Check for integer feasibility @@ -916,81 +1046,23 @@ fcheck_code_t mcarith_final_check(void* s) { solver->mcsat = mcsat_new(&solver->mcsat_ctx); acnt = solver->assertion_count; - term_t* assertions = safe_malloc(sizeof(term_t) * (acnt + 1)); - literal_t* literals = safe_malloc(sizeof(literal_t) * acnt); - size_t literal_count = 0; +// ivector_t* assertions = &solver->mcsat_assertions; + ivector_reset(&solver->mcsat_assertions); + mcarith_check_var_size(solver); for (size_t i = 0; i < acnt; ++i) { mcarith_assertion_t* a = solver->assertions + i; - rba_buffer_t b; - term_t p; - switch (a->type) { - case VAR_EQ: { - term_t lhs; - term_t rhs; - lhs = get_term(solver, a->def.eq.lhs); - rhs = get_term(solver, a->def.eq.rhs); - p = arith_bineq_atom(terms, lhs, rhs); - break; - } - case VAR_EQ0: - p = arith_eq_atom(terms, get_term(solver, a->def.var)); - break; - case VAR_GE0: - t = get_term(solver, a->def.var); - assert(term_kind(terms, t) != ARITH_CONSTANT); - p = arith_geq_atom(terms, t); - break; - case POLY_EQ0: { - rational_t br; - - 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); - break; - } - case POLY_GE0: { - rational_t br; - - 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); - break; - } - case ATOM_ASSERT: - p = get_atom(solver, a->def.atom); - break; - default: - longjmp(*solver->simplex.env, INTERNAL_ERROR); - } - if (a->lit != null_literal) { - smt_core_t* c = solver->simplex.core; - assert(literal_value(c, a->lit) == VAL_TRUE); - literals[literal_count++] = not(a->lit); - } - assertions[i] = a->tt ? p : not_term(terms, p); + term_t p = mk_assertion_pred(solver, a); + ivector_push(&solver->mcsat_assertions, a->tt ? p : not_term(terms, p)); } - literals[literal_count] = end_clause; - int32_t r = mcsat_assert_formulas(solver->mcsat, acnt, assertions); + int32_t r = mcsat_assert_formulas(solver->mcsat, solver->mcsat_assertions.size, solver->mcsat_assertions.data); if (r == TRIVIALLY_UNSAT) { - record_theory_conflict(solver->simplex.core, literals); mcarith_free_mcsat(solver); + ivector_t* conflict = &solver->simplex.expl_vector; + init_conflict(conflict, solver); + record_theory_conflict(solver->simplex.core, conflict->data); result = FCHECK_CONTINUE; } else if (r == CTX_NO_ERROR) { result = FCHECK_SAT; @@ -998,18 +1070,18 @@ fcheck_code_t mcarith_final_check(void* s) { switch (mcsat_status(solver->mcsat)) { case STATUS_UNKNOWN: mcarith_free_mcsat(solver); - safe_free(literals); result = FCHECK_UNKNOWN; break; case STATUS_SAT: - safe_free(literals); result = FCHECK_SAT; break; case STATUS_UNSAT: mcarith_free_mcsat(solver); // - record a conflict (by calling record_theory_conflict) // - create lemmas or atoms in the core - record_theory_conflict(solver->simplex.core, literals); + ivector_t* conflict = &solver->simplex.expl_vector; + init_conflict(conflict, solver); + record_theory_conflict(solver->simplex.core, conflict->data); result = FCHECK_CONTINUE; break; case STATUS_IDLE: @@ -1018,13 +1090,11 @@ fcheck_code_t mcarith_final_check(void* s) { case STATUS_ERROR: default: mcarith_free_mcsat(solver); - safe_free(literals); longjmp(*solver->simplex.env, INTERNAL_ERROR); break; } } else { mcarith_free_mcsat(solver); - safe_free(literals); longjmp(*solver->simplex.env, INTERNAL_ERROR); } @@ -1059,8 +1129,8 @@ void mcarith_backtrack(mcarith_solver_t *solver, uint32_t back_level) { mcarith_backtrack_assertions(solver, r->n_assertions); uint32_t vc = solver->simplex.vtbl.nvars; simplex_backtrack(&solver->simplex, back_level); - uint32_t vc0 = solver->simplex.vtbl.nvars; - assert(vc == vc0); + (void)vc; // SUPPRESS unused variable warning in release builds. + assert(vc == solver->simplex.vtbl.nvars); } /* @@ -1076,9 +1146,6 @@ static void mcarith_push(mcarith_solver_t *solver) { */ void mcarith_pop(mcarith_solver_t *solver) { uint32_t vc; - uint32_t vc0; - term_t* t; - term_t* end; mcarith_undo_record_t* r; // Reset assertions r = mcarith_undo_pop_record(&solver->undo_stack); @@ -1086,12 +1153,7 @@ void mcarith_pop(mcarith_solver_t *solver) { // Pop simplex state vc = solver->simplex.vtbl.nvars; simplex_pop(&solver->simplex); - vc0 = solver->simplex.vtbl.nvars; - - end = solver->var_terms + vc; - for (t = solver->var_terms + vc0; t != end; ++t) { - *t = NULL_TERM; - } + ivector_shrink(&solver->var_terms, solver->simplex.vtbl.nvars); } /* @@ -1100,8 +1162,7 @@ void mcarith_pop(mcarith_solver_t *solver) { void mcarith_reset(mcarith_solver_t *solver) { uint32_t vc = solver->simplex.vtbl.nvars; simplex_reset(&solver->simplex); - uint32_t vc0 = solver->simplex.vtbl.nvars; - assert(vc == vc0); // FIXME + assert(vc == solver->simplex.vtbl.nvars); // FIXME mcarith_undo_reset(&solver->undo_stack); mcarith_backtrack_assertions(solver, 0); @@ -1126,7 +1187,6 @@ static th_ctrl_interface_t mcarith_control = { .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 @@ -1149,8 +1209,7 @@ bool mcarith_assert_atom(mcarith_solver_t *solver, void *atom_pointer, literal_t int32_t atom_index = arithatom_tagged_ptr2idx(atom_pointer); assert(0 <= atom_index && atom_index < atbl->natoms); - arith_atom_t* ap = atbl->atoms + atom_index; - assert(boolvar_of_atom(ap) == var_of(l)); + assert(boolvar_of_atom(atbl->atoms + atom_index) == var_of(l)); mcarith_assertion_t* assert = alloc_top_assertion(solver); assert->type = ATOM_ASSERT; @@ -1411,19 +1470,6 @@ static void mcarith_build_model(void* s) { mcarith_free_mcsat(solver); } -/* - * Free the model - */ -static void mcarith_free_model(void* s) { - mcarith_solver_t* solver; - - solver = s; - assert(solver->model); - delete_model(solver->model); - free(solver->model); - solver->model = 0; -} - /* * 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 @@ -1440,7 +1486,7 @@ bool mcarith_value_in_model(void* s, thvar_t x, arithval_in_model_t* res) { assert(res->tag == ARITHVAL_RATIONAL); solver = s; - t = solver->var_terms[x]; + t = solver->var_terms.data[x]; if (t == NULL_TERM) return false; @@ -1521,4 +1567,5 @@ th_ctrl_interface_t *mcarith_ctrl_interface(mcarith_solver_t *solver) { th_smt_interface_t *mcarith_smt_interface(mcarith_solver_t *solver) { return &mcarith_smt; -} \ No newline at end of file +} +#endif \ No newline at end of file diff --git a/src/solvers/mcarith/mcarith.h b/src/solvers/mcarith/mcarith.h index 3b9a5ed65..040eb1d7e 100644 --- a/src/solvers/mcarith/mcarith.h +++ b/src/solvers/mcarith/mcarith.h @@ -15,7 +15,7 @@ * 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 @@ -65,5 +65,5 @@ extern th_smt_interface_t *mcarith_smt_interface(mcarith_solver_t *solver); 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 From 6aaea1e0785f424a5aabd649cd48e62e55a6815e Mon Sep 17 00:00:00 2001 From: Joe Hendrix Date: Thu, 28 Sep 2023 15:44:42 -0700 Subject: [PATCH 10/10] Add extra logging and force command. --- src/frontend/smt2/smt2_commands.c | 5 +++ src/solvers/mcarith/mcarith.c | 65 ++++++++++++++----------------- 2 files changed, 35 insertions(+), 35 deletions(-) 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/solvers/mcarith/mcarith.c b/src/solvers/mcarith/mcarith.c index af674bd42..4b8c6f85b 100644 --- a/src/solvers/mcarith/mcarith.c +++ b/src/solvers/mcarith/mcarith.c @@ -319,6 +319,7 @@ term_table_t* mcarith_solver_terms(mcarith_solver_t* s) { * 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)); @@ -1004,10 +1005,16 @@ term_t mk_assertion_pred(mcarith_solver_t *solver, mcarith_assertion_t* a) { } } +/* + * Cleanup and return final check conflict + * + * Note. This should be updated to derive conflict clause from mcsat information. + */ static -void init_conflict(ivector_t* conflict, mcarith_solver_t *solver) { - ivector_reset(conflict); - uint32_t acnt = solver->assertion_count; +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) { @@ -1016,6 +1023,11 @@ void init_conflict(ivector_t* conflict, mcarith_solver_t *solver) { } } 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; } /* @@ -1025,32 +1037,31 @@ static fcheck_code_t mcarith_final_check(void* s) { mcarith_solver_t *solver; term_table_t* terms; - uint32_t acnt; - term_t t; + 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); - fcheck_code_t result; - - result = simplex_final_check(&solver->simplex); - if (result == FCHECK_CONTINUE) { - return result; - } + 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); - acnt = solver->assertion_count; -// ivector_t* assertions = &solver->mcsat_assertions; ivector_reset(&solver->mcsat_assertions); mcarith_check_var_size(solver); - for (size_t i = 0; i < acnt; ++i) { + 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); @@ -1059,31 +1070,17 @@ fcheck_code_t mcarith_final_check(void* s) { int32_t r = mcsat_assert_formulas(solver->mcsat, solver->mcsat_assertions.size, solver->mcsat_assertions.data); if (r == TRIVIALLY_UNSAT) { - mcarith_free_mcsat(solver); - ivector_t* conflict = &solver->simplex.expl_vector; - init_conflict(conflict, solver); - record_theory_conflict(solver->simplex.core, conflict->data); - result = FCHECK_CONTINUE; + return final_check_conflict(solver); } else if (r == CTX_NO_ERROR) { - result = FCHECK_SAT; mcsat_solve(solver->mcsat, 0, 0, 0, 0); switch (mcsat_status(solver->mcsat)) { case STATUS_UNKNOWN: mcarith_free_mcsat(solver); - result = FCHECK_UNKNOWN; - break; + return FCHECK_UNKNOWN; case STATUS_SAT: - result = FCHECK_SAT; - break; + return FCHECK_SAT; case STATUS_UNSAT: - mcarith_free_mcsat(solver); - // - record a conflict (by calling record_theory_conflict) - // - create lemmas or atoms in the core - ivector_t* conflict = &solver->simplex.expl_vector; - init_conflict(conflict, solver); - record_theory_conflict(solver->simplex.core, conflict->data); - result = FCHECK_CONTINUE; - break; + return final_check_conflict(solver); case STATUS_IDLE: case STATUS_SEARCHING: case STATUS_INTERRUPTED: @@ -1091,14 +1088,12 @@ fcheck_code_t mcarith_final_check(void* s) { default: mcarith_free_mcsat(solver); longjmp(*solver->simplex.env, INTERNAL_ERROR); - break; } } else { mcarith_free_mcsat(solver); longjmp(*solver->simplex.env, INTERNAL_ERROR); } - return result; } /*