From: Andrew Reynolds Date: Fri, 19 Oct 2018 00:37:11 +0000 (-0500) Subject: Non-implied mode for model cores (#2653) X-Git-Tag: cvc5-1.0.0~4405 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=547bd91e189b28da9950e12037d1e88079157479;p=cvc5.git Non-implied mode for model cores (#2653) --- diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 676943b11..4cf8412f0 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -823,7 +823,7 @@ install(FILES options/printer_modes.h options/quantifiers_modes.h options/set_language.h - options/simplification_mode.h + options/smt_modes.h options/sygus_out_mode.h options/theoryof_mode.h DESTINATION diff --git a/src/options/CMakeLists.txt b/src/options/CMakeLists.txt index 457fd23cd..dd0e34578 100644 --- a/src/options/CMakeLists.txt +++ b/src/options/CMakeLists.txt @@ -32,8 +32,8 @@ libcvc4_add_sources( quantifiers_modes.h set_language.cpp set_language.h - simplification_mode.cpp - simplification_mode.h + smt_modes.cpp + smt_modes.h sygus_out_mode.h theoryof_mode.cpp theoryof_mode.h diff --git a/src/options/Makefile.am b/src/options/Makefile.am index c311e04d8..54047efcc 100644 --- a/src/options/Makefile.am +++ b/src/options/Makefile.am @@ -96,8 +96,8 @@ liboptions_la_SOURCES = \ quantifiers_modes.h \ set_language.cpp \ set_language.h \ - simplification_mode.cpp \ - simplification_mode.h \ + smt_modes.cpp \ + smt_modes.h \ sygus_out_mode.h \ theoryof_mode.cpp \ theoryof_mode.h \ diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp index be2d7883d..46663ce7c 100644 --- a/src/options/options_handler.cpp +++ b/src/options/options_handler.cpp @@ -42,8 +42,6 @@ #include "options/language.h" #include "options/option_exception.h" #include "options/printer_modes.h" -#include "options/quantifiers_modes.h" -#include "options/simplification_mode.h" #include "options/smt_options.h" #include "options/theory_options.h" #include "options/theoryof_mode.h" @@ -1472,6 +1470,51 @@ SimplificationMode OptionsHandler::stringToSimplificationMode( } } +const std::string OptionsHandler::s_modelCoresHelp = + "\ +Model cores modes currently supported by the --simplification option:\n\ +\n\ +none (default) \n\ ++ do not compute model cores\n\ +\n\ +simple\n\ ++ only include a subset of variables whose values are sufficient to show the\n\ +input formula is satisfied by the given model\n\ +\n\ +non-implied\n\ ++ only include a subset of variables whose values, in addition to the values\n\ +of variables whose values are implied, are sufficient to show the input\n\ +formula is satisfied by the given model\n\ +\n\ +"; + +ModelCoresMode OptionsHandler::stringToModelCoresMode(std::string option, + std::string optarg) +{ + if (optarg == "none") + { + return MODEL_CORES_NONE; + } + else if (optarg == "simple") + { + return MODEL_CORES_SIMPLE; + } + else if (optarg == "non-implied") + { + return MODEL_CORES_NON_IMPLIED; + } + else if (optarg == "help") + { + puts(s_modelCoresHelp.c_str()); + exit(1); + } + else + { + throw OptionException(std::string("unknown option for --model-cores: `") + + optarg + "'. Try --model-cores help."); + } +} + const std::string OptionsHandler::s_sygusSolutionOutModeHelp = "\ Modes for finite model finding bound minimization, supported by --sygus-out:\n\ diff --git a/src/options/options_handler.h b/src/options/options_handler.h index 0205b0b73..3078db0f8 100644 --- a/src/options/options_handler.h +++ b/src/options/options_handler.h @@ -35,7 +35,7 @@ #include "options/options.h" #include "options/printer_modes.h" #include "options/quantifiers_modes.h" -#include "options/simplification_mode.h" +#include "options/smt_modes.h" #include "options/sygus_out_mode.h" #include "options/theoryof_mode.h" #include "options/ufss_mode.h" @@ -171,6 +171,7 @@ public: void notifyDumpMode(std::string option); SimplificationMode stringToSimplificationMode(std::string option, std::string optarg); + ModelCoresMode stringToModelCoresMode(std::string option, std::string optarg); SygusSolutionOutMode stringToSygusSolutionOutMode(std::string option, std::string optarg); void setProduceAssertions(std::string option, bool value); @@ -241,6 +242,7 @@ public: static const std::string s_qcfModeHelp; static const std::string s_qcfWhenModeHelp; static const std::string s_simplificationHelp; + static const std::string s_modelCoresHelp; static const std::string s_sygusSolutionOutModeHelp; static const std::string s_cbqiBvIneqModeHelp; static const std::string s_cegqiSingleInvHelp; diff --git a/src/options/simplification_mode.cpp b/src/options/simplification_mode.cpp deleted file mode 100644 index 6b6fc842d..000000000 --- a/src/options/simplification_mode.cpp +++ /dev/null @@ -1,39 +0,0 @@ -/********************* */ -/*! \file simplification_mode.cpp - ** \verbatim - ** Top contributors (to current version): - ** Morgan Deters, Tim King - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief [[ Add one-line brief description here ]] - ** - ** [[ Add lengthier description here ]] - ** \todo document this file - **/ - -#include "options/simplification_mode.h" - -#include - -namespace CVC4 { - -std::ostream& operator<<(std::ostream& out, SimplificationMode mode) { - switch(mode) { - case SIMPLIFICATION_MODE_BATCH: - out << "SIMPLIFICATION_MODE_BATCH"; - break; - case SIMPLIFICATION_MODE_NONE: - out << "SIMPLIFICATION_MODE_NONE"; - break; - default: - out << "SimplificationMode:UNKNOWN![" << unsigned(mode) << "]"; - } - - return out; -} - -}/* CVC4 namespace */ diff --git a/src/options/simplification_mode.h b/src/options/simplification_mode.h deleted file mode 100644 index 52bf25fa1..000000000 --- a/src/options/simplification_mode.h +++ /dev/null @@ -1,39 +0,0 @@ -/********************* */ -/*! \file simplification_mode.h - ** \verbatim - ** Top contributors (to current version): - ** Morgan Deters, Tim King - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief [[ Add one-line brief description here ]] - ** - ** [[ Add lengthier description here ]] - ** \todo document this file - **/ - -#include "cvc4_public.h" - -#ifndef __CVC4__SMT__SIMPLIFICATION_MODE_H -#define __CVC4__SMT__SIMPLIFICATION_MODE_H - -#include - -namespace CVC4 { - -/** Enumeration of simplification modes (when to simplify). */ -typedef enum { - /** Simplify the assertions all together once a check is requested */ - SIMPLIFICATION_MODE_BATCH, - /** Don't do simplification */ - SIMPLIFICATION_MODE_NONE -} SimplificationMode; - -std::ostream& operator<<(std::ostream& out, SimplificationMode mode) CVC4_PUBLIC; - -}/* CVC4 namespace */ - -#endif /* __CVC4__SMT__SIMPLIFICATION_MODE_H */ diff --git a/src/options/smt_modes.cpp b/src/options/smt_modes.cpp new file mode 100644 index 000000000..4a2fd404c --- /dev/null +++ b/src/options/smt_modes.cpp @@ -0,0 +1,36 @@ +/********************* */ +/*! \file smt_modes.cpp + ** \verbatim + ** Top contributors (to current version): + ** Morgan Deters, Tim King + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ + +#include "options/smt_modes.h" + +#include + +namespace CVC4 { + +std::ostream& operator<<(std::ostream& out, SimplificationMode mode) +{ + switch (mode) + { + case SIMPLIFICATION_MODE_BATCH: out << "SIMPLIFICATION_MODE_BATCH"; break; + case SIMPLIFICATION_MODE_NONE: out << "SIMPLIFICATION_MODE_NONE"; break; + default: out << "SimplificationMode:UNKNOWN![" << unsigned(mode) << "]"; + } + + return out; +} + +} // namespace CVC4 diff --git a/src/options/smt_modes.h b/src/options/smt_modes.h new file mode 100644 index 000000000..761f3be01 --- /dev/null +++ b/src/options/smt_modes.h @@ -0,0 +1,58 @@ +/********************* */ +/*! \file smt_modes.h + ** \verbatim + ** Top contributors (to current version): + ** Morgan Deters, Tim King + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ + +#include "cvc4_public.h" + +#ifndef __CVC4__SMT__MODES_H +#define __CVC4__SMT__MODES_H + +#include + +namespace CVC4 { + +/** Enumeration of simplification modes (when to simplify). */ +enum SimplificationMode +{ + /** Simplify the assertions all together once a check is requested */ + SIMPLIFICATION_MODE_BATCH, + /** Don't do simplification */ + SIMPLIFICATION_MODE_NONE +}; + +std::ostream& operator<<(std::ostream& out, + SimplificationMode mode) CVC4_PUBLIC; + +/** Enumeration of model core modes. */ +enum ModelCoresMode +{ + /** Do not compute model cores */ + MODEL_CORES_NONE, + /** + * Compute "simple" model cores that exclude variables that do not + * contribute to satisfying the input. + */ + MODEL_CORES_SIMPLE, + /** + * Compute model cores that also exclude variables whose variables are implied + * by others. + */ + MODEL_CORES_NON_IMPLIED +}; + +} // namespace CVC4 + +#endif /* __CVC4__SMT__MODES_H */ diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml index 8af1000ba..e0041774a 100644 --- a/src/options/smt_options.toml +++ b/src/options/smt_options.toml @@ -40,7 +40,7 @@ header = "options/smt_options.h" type = "SimplificationMode" default = "SIMPLIFICATION_MODE_BATCH" handler = "stringToSimplificationMode" - includes = ["options/simplification_mode.h"] + includes = ["options/smt_modes.h"] help = "choose simplification mode, see --simplification=help" [[alias]] @@ -99,13 +99,14 @@ header = "options/smt_options.h" help = "output models after every SAT/INVALID/UNKNOWN response" [[option]] - name = "produceModelCores" + name = "modelCoresMode" category = "regular" - long = "produce-model-cores" - type = "bool" - default = "false" - read_only = true - help = "when printing models, compute a minimal core of relevant definitions" + long = "model-cores=MODE" + type = "ModelCoresMode" + default = "MODEL_CORES_NONE" + handler = "stringToModelCoresMode" + includes = ["options/smt_modes.h"] + help = "mode for producing model cores" [[option]] name = "proof" diff --git a/src/smt/model_core_builder.cpp b/src/smt/model_core_builder.cpp index 1cbc18c1a..a077bb2fa 100644 --- a/src/smt/model_core_builder.cpp +++ b/src/smt/model_core_builder.cpp @@ -21,7 +21,8 @@ using namespace CVC4::kind; namespace CVC4 { bool ModelCoreBuilder::setModelCore(const std::vector& assertions, - Model* m) + Model* m, + ModelCoresMode mode) { if (Trace.isOn("model-core")) { @@ -74,8 +75,22 @@ bool ModelCoreBuilder::setModelCore(const std::vector& assertions, Trace("model-core") << "Minimizing substitution..." << std::endl; std::vector coreVars; - bool minimized = - theory::SubstitutionMinimize::find(formula, truen, vars, subs, coreVars); + std::vector impliedVars; + bool minimized = false; + if (mode == MODEL_CORES_NON_IMPLIED) + { + minimized = theory::SubstitutionMinimize::findWithImplied( + formula, vars, subs, coreVars, impliedVars); + } + else if (mode == MODEL_CORES_SIMPLE) + { + minimized = theory::SubstitutionMinimize::find( + formula, truen, vars, subs, coreVars); + } + else + { + Unreachable("Unknown model cores mode"); + } Assert(minimized, "cannot compute model core, since model does not satisfy input!"); if (minimized) diff --git a/src/smt/model_core_builder.h b/src/smt/model_core_builder.h index 29348a4f4..a60a3767c 100644 --- a/src/smt/model_core_builder.h +++ b/src/smt/model_core_builder.h @@ -20,6 +20,7 @@ #include #include "expr/expr.h" +#include "options/smt_options.h" #include "smt/model.h" namespace CVC4 { @@ -32,22 +33,30 @@ class ModelCoreBuilder public: /** set model core * - * This function updates the model m so that it is a minimal "core" of - * substitutions that satisfy the formulas in assertions, interpreted - * conjunctively. This is specified via calls to - * Model::setUsingModelCore, Model::recordModelCoreSymbol, - * for details see smt/model.h. + * This function updates model m so that it has information regarding its + * "model core". A model core for m is a substitution of the form + * { s1 -> m(s1), ..., sn -> m(sn) } * - * It returns true if m is a model for assertions. In this case, we set: + * The criteria for what consistutes a model core given by mode. For + * example, if mode is MODEL_CORES_SIMPLE, then a model core corresponds to a + * subset of assignments from the model that suffice to show that the set of + * assertions, interpreted conjunctively, evaluates to true under the + * substitution corresponding to the model core. + * + * The model core is recorded on the model object m via calls to + * m->setUsingModelCore, m->recordModelCoreSymbol, for details see + * smt/model.h. In particular, we call: * m->usingModelCore(); * m->recordModelCoreSymbol(s1); ... m->recordModelCoreSymbol(sn); - * such that each formula in assertions under the substitution - * { s1 -> m(s1), ..., sn -> m(sn) } rewrites to true. + * such that { s1 -> m(s1), ..., sn -> m(sn) } is the model core computed + * by this class. * * If m is not a model for assertions, this method returns false and m is * left unchanged. */ - static bool setModelCore(const std::vector& assertions, Model* m); + static bool setModelCore(const std::vector& assertions, + Model* m, + ModelCoresMode mode); }; /* class TheoryModelCoreBuilder */ } // namespace CVC4 diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index a2dd8276b..63c970920 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1235,7 +1235,7 @@ void SmtEngine::setDefaults() { } if ((options::checkModels() || options::checkSynthSol() - || options::produceModelCores()) + || options::modelCoresMode() != MODEL_CORES_NONE) && !options::produceAssertions()) { Notice() << "SmtEngine: turning on produce-assertions to support " @@ -1432,7 +1432,7 @@ void SmtEngine::setDefaults() { // cases where we need produce models if (!options::produceModels() && (options::produceAssignments() || options::sygusRewSynthCheck() - || options::produceModelCores() || is_sygus)) + || is_sygus)) { Notice() << "SmtEngine: turning on produce-models" << endl; setOption("produce-models", SExpr("true")); @@ -4263,12 +4263,12 @@ Model* SmtEngine::getModel() { } TheoryModel* m = d_theoryEngine->getModel(); - if (options::produceModelCores()) + if (options::modelCoresMode() != MODEL_CORES_NONE) { // If we enabled model cores, we compute a model core for m based on our // assertions using the model core builder utility std::vector easserts = getAssertions(); - ModelCoreBuilder::setModelCore(easserts, m); + ModelCoreBuilder::setModelCore(easserts, m, options::modelCoresMode()); } m->d_inputName = d_filename; return m; diff --git a/src/theory/subs_minimize.cpp b/src/theory/subs_minimize.cpp index 03a55b3a4..58daf5c75 100644 --- a/src/theory/subs_minimize.cpp +++ b/src/theory/subs_minimize.cpp @@ -14,6 +14,7 @@ #include "theory/subs_minimize.h" +#include "expr/node_algorithm.h" #include "theory/bv/theory_bv_utils.h" #include "theory/rewriter.h" @@ -25,11 +26,150 @@ namespace theory { SubstitutionMinimize::SubstitutionMinimize() {} -bool SubstitutionMinimize::find(Node n, +bool SubstitutionMinimize::find(Node t, Node target, const std::vector& vars, const std::vector& subs, std::vector& reqVars) +{ + return findInternal(t, target, vars, subs, reqVars); +} + +void getConjuncts(Node n, std::vector& conj) +{ + if (n.getKind() == AND) + { + for (const Node& nc : n) + { + conj.push_back(nc); + } + } + else + { + conj.push_back(n); + } +} + +bool SubstitutionMinimize::findWithImplied(Node t, + const std::vector& vars, + const std::vector& subs, + std::vector& reqVars, + std::vector& impliedVars) +{ + NodeManager* nm = NodeManager::currentNM(); + Node truen = nm->mkConst(true); + if (!findInternal(t, truen, vars, subs, reqVars)) + { + return false; + } + if (reqVars.empty()) + { + return true; + } + + // map from conjuncts of t to whether they may be used to show an implied var + std::vector tconj; + getConjuncts(t, tconj); + // map from conjuncts to their free symbols + std::map > tcFv; + + std::unordered_set reqSet; + std::vector reqSubs; + std::map reqVarToIndex; + for (const Node& v : reqVars) + { + reqVarToIndex[v] = reqSubs.size(); + const std::vector::const_iterator& it = + std::find(vars.begin(), vars.end(), v); + Assert(it != vars.end()); + ptrdiff_t pos = std::distance(vars.begin(), it); + reqSubs.push_back(subs[pos]); + } + std::vector finalReqVars; + for (const Node& v : vars) + { + if (reqVarToIndex.find(v) == reqVarToIndex.end()) + { + // not a required variable, nothing to do + continue; + } + unsigned vindex = reqVarToIndex[v]; + Node prev = reqSubs[vindex]; + // make identity substitution + reqSubs[vindex] = v; + bool madeImplied = false; + // it is a required variable, can we make an implied variable? + for (const Node& tc : tconj) + { + // ensure we've computed its free symbols + std::map >::iterator + itf = tcFv.find(tc); + if (itf == tcFv.end()) + { + expr::getSymbols(tc, tcFv[tc]); + itf = tcFv.find(tc); + } + // only have a chance if contains v + if (itf->second.find(v) == itf->second.end()) + { + continue; + } + // try the current substitution + Node tcs = tc.substitute( + reqVars.begin(), reqVars.end(), reqSubs.begin(), reqSubs.end()); + Node tcsr = Rewriter::rewrite(tcs); + std::vector tcsrConj; + getConjuncts(tcsr, tcsrConj); + for (const Node& tcc : tcsrConj) + { + if (tcc.getKind() == EQUAL) + { + for (unsigned r = 0; r < 2; r++) + { + if (tcc[r] == v) + { + Node res = tcc[1 - r]; + if (res.isConst()) + { + Assert(res == prev); + madeImplied = true; + break; + } + } + } + } + if (madeImplied) + { + break; + } + } + if (madeImplied) + { + break; + } + } + if (!madeImplied) + { + // revert the substitution + reqSubs[vindex] = prev; + finalReqVars.push_back(v); + } + else + { + impliedVars.push_back(v); + } + } + reqVars.clear(); + reqVars.insert(reqVars.end(), finalReqVars.begin(), finalReqVars.end()); + + return true; +} + +bool SubstitutionMinimize::findInternal(Node n, + Node target, + const std::vector& vars, + const std::vector& subs, + std::vector& reqVars) { Trace("subs-min") << "Substitution minimize : " << std::endl; Trace("subs-min") << " substitution : " << vars << " -> " << subs @@ -37,8 +177,6 @@ bool SubstitutionMinimize::find(Node n, Trace("subs-min") << " node : " << n << std::endl; Trace("subs-min") << " target : " << target << std::endl; - std::map > fvDepend; - Trace("subs-min") << "--- Compute values for subterms..." << std::endl; // the value of each subterm in n under the substitution std::unordered_map value; @@ -124,8 +262,6 @@ bool SubstitutionMinimize::find(Node n, Trace("subs-min") << "--- Compute relevant variables..." << std::endl; std::unordered_set rlvFv; // only variables that occur in assertions are relevant - std::map iteBranch; - std::map > justifyArgs; visit.push_back(n); std::unordered_set visited; diff --git a/src/theory/subs_minimize.h b/src/theory/subs_minimize.h index 55e57b921..bf6ccffae 100644 --- a/src/theory/subs_minimize.h +++ b/src/theory/subs_minimize.h @@ -36,21 +36,55 @@ class SubstitutionMinimize ~SubstitutionMinimize() {} /** find * - * If n { vars -> subs } rewrites to target, this method returns true, and - * vars[i1], ..., vars[in] are added to rewVars, such that - * n { vars[i_1] -> subs[i_1], ..., vars[i_n] -> subs[i_n] } also rewrites to - * target. + * If t { vars -> subs } rewrites to target, this method returns true, and + * vars[i_1], ..., vars[i_n] are added to reqVars, such that i_1, ..., i_n are + * distinct, and t { vars[i_1] -> subs[i_1], ..., vars[i_n] -> subs[i_n] } + * rewrites to target. * - * If n { vars -> subs } does not rewrite to target, this method returns + * If t { vars -> subs } does not rewrite to target, this method returns * false. */ - static bool find(Node n, + static bool find(Node t, Node target, const std::vector& vars, const std::vector& subs, std::vector& reqVars); + /** find with implied + * + * This method should be called on a formula t. + * + * If t { vars -> subs } rewrites to true, this method returns true, + * vars[i_1], ..., vars[i_n] are added to reqVars, and + * vars[i_{n+1}], ..., vars[i_{n+m}] are added to impliedVars such that + * i_1...i_{n+m} are distinct, i_{n+1} < ... < i_{n+m}, and: + * + * (1) t { vars[i_1]->subs[i_1], ..., vars[i_{n+k}]->subs[i_{n+k}] } implies + * vars[i_{n+k+1}] = subs[i_{n+k+1}] for k = 0, ..., m-1. + * + * (2) t { vars[i_1] -> subs[i_1], ..., vars[i_{n+m}] -> subs[i_{n+m}] } + * rewrites to true. + * + * For example, given (x>0 ^ x = y ^ y = z){ x -> 1, y -> 1, z -> 1, w -> 0 }, + * this method may add { x } to reqVars, and { y, z } to impliedVars. + * + * Notice that the order of variables in vars matters. By the semantics above, + * variables that appear earlier in the variable list vars are more likely + * to appear in reqVars, whereas those later in the vars are more likely to + * appear in impliedVars. + */ + static bool findWithImplied(Node t, + const std::vector& vars, + const std::vector& subs, + std::vector& reqVars, + std::vector& impliedVars); private: + /** Common helper function for the above functions. */ + static bool findInternal(Node t, + Node target, + const std::vector& vars, + const std::vector& subs, + std::vector& reqVars); /** is singular arg * * Returns true if diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index a41108a71..cd98a8917 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1183,6 +1183,7 @@ set(regress_1_tests regress1/nl/nl-unk-quant.smt2 regress1/nl/nl_uf_lalt.smt2 regress1/nl/ones.smt2 + regress1/nl/pinto-model-core-ni.smt2 regress1/nl/poly-1025.smt2 regress1/nl/quant-nl.smt2 regress1/nl/red-exp.smt2 diff --git a/test/regress/regress0/model-core.smt2 b/test/regress/regress0/model-core.smt2 index 6729cb5e0..fca80a960 100644 --- a/test/regress/regress0/model-core.smt2 +++ b/test/regress/regress0/model-core.smt2 @@ -1,4 +1,5 @@ -; COMMAND-LINE: --produce-model-cores +; COMMAND-LINE: --produce-models --model-cores=simple +; COMMAND-LINE: --produce-models --model-core=non-implied ; EXPECT: sat (set-logic QF_UFLIA) (declare-fun x () Int) diff --git a/test/regress/regress1/nl/pinto-model-core-ni.smt2 b/test/regress/regress1/nl/pinto-model-core-ni.smt2 new file mode 100644 index 000000000..1e09f8439 --- /dev/null +++ b/test/regress/regress1/nl/pinto-model-core-ni.smt2 @@ -0,0 +1,22 @@ +; COMMAND-LINE: --nl-ext-tplanes --produce-models --model-core=non-implied +; EXPECT: sat +(set-logic ALL) +(declare-fun i1 () Real) +(declare-fun i2 () Real) +(declare-fun n () Int) +(declare-fun x () Int) +(declare-fun y () Int) +(declare-fun i11 () Real) +(declare-fun i21 () Real) + +(assert (>= n 1)) +(assert (and (<= 1 x)(<= x n))) +(assert (and (<= 1 y)(<= y n))) +(assert (or (= (/ (* (- 1) x) n) i1)(= i1 (/ x n)))) +(assert (or (= (/ (* (- 1) y) n) i2)(= i2 (/ y n)))) + +(assert (and (= i1 i11) (= i2 i21) )) + +(assert (not (and (or (= (- 1) i11 )(= i11 1)) (or (= (- 1) i21)(= i21 1)) ))) + +(check-sat)