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
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
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 \
#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"
}
}
+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\
#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"
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);
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;
+++ /dev/null
-/********************* */
-/*! \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 <iostream>
-
-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 */
+++ /dev/null
-/********************* */
-/*! \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 <iosfwd>
-
-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 */
--- /dev/null
+/********************* */
+/*! \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 <iostream>
+
+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
--- /dev/null
+/********************* */
+/*! \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 <iosfwd>
+
+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 */
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]]
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"
namespace CVC4 {
bool ModelCoreBuilder::setModelCore(const std::vector<Expr>& assertions,
- Model* m)
+ Model* m,
+ ModelCoresMode mode)
{
if (Trace.isOn("model-core"))
{
Trace("model-core") << "Minimizing substitution..." << std::endl;
std::vector<Node> coreVars;
- bool minimized =
- theory::SubstitutionMinimize::find(formula, truen, vars, subs, coreVars);
+ std::vector<Node> 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)
#include <vector>
#include "expr/expr.h"
+#include "options/smt_options.h"
#include "smt/model.h"
namespace CVC4 {
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<Expr>& assertions, Model* m);
+ static bool setModelCore(const std::vector<Expr>& assertions,
+ Model* m,
+ ModelCoresMode mode);
}; /* class TheoryModelCoreBuilder */
} // namespace CVC4
}
if ((options::checkModels() || options::checkSynthSol()
- || options::produceModelCores())
+ || options::modelCoresMode() != MODEL_CORES_NONE)
&& !options::produceAssertions())
{
Notice() << "SmtEngine: turning on produce-assertions to support "
// 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"));
}
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<Expr> easserts = getAssertions();
- ModelCoreBuilder::setModelCore(easserts, m);
+ ModelCoreBuilder::setModelCore(easserts, m, options::modelCoresMode());
}
m->d_inputName = d_filename;
return m;
#include "theory/subs_minimize.h"
+#include "expr/node_algorithm.h"
#include "theory/bv/theory_bv_utils.h"
#include "theory/rewriter.h"
SubstitutionMinimize::SubstitutionMinimize() {}
-bool SubstitutionMinimize::find(Node n,
+bool SubstitutionMinimize::find(Node t,
Node target,
const std::vector<Node>& vars,
const std::vector<Node>& subs,
std::vector<Node>& reqVars)
+{
+ return findInternal(t, target, vars, subs, reqVars);
+}
+
+void getConjuncts(Node n, std::vector<Node>& 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<Node>& vars,
+ const std::vector<Node>& subs,
+ std::vector<Node>& reqVars,
+ std::vector<Node>& 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<Node> tconj;
+ getConjuncts(t, tconj);
+ // map from conjuncts to their free symbols
+ std::map<Node, std::unordered_set<Node, NodeHashFunction> > tcFv;
+
+ std::unordered_set<Node, NodeHashFunction> reqSet;
+ std::vector<Node> reqSubs;
+ std::map<Node, unsigned> reqVarToIndex;
+ for (const Node& v : reqVars)
+ {
+ reqVarToIndex[v] = reqSubs.size();
+ const std::vector<Node>::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<Node> 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<Node, std::unordered_set<Node, NodeHashFunction> >::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<Node> 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<Node>& vars,
+ const std::vector<Node>& subs,
+ std::vector<Node>& reqVars)
{
Trace("subs-min") << "Substitution minimize : " << std::endl;
Trace("subs-min") << " substitution : " << vars << " -> " << subs
Trace("subs-min") << " node : " << n << std::endl;
Trace("subs-min") << " target : " << target << std::endl;
- std::map<Node, std::unordered_set<Node, NodeHashFunction> > fvDepend;
-
Trace("subs-min") << "--- Compute values for subterms..." << std::endl;
// the value of each subterm in n under the substitution
std::unordered_map<TNode, Node, TNodeHashFunction> value;
Trace("subs-min") << "--- Compute relevant variables..." << std::endl;
std::unordered_set<Node, NodeHashFunction> rlvFv;
// only variables that occur in assertions are relevant
- std::map<Node, unsigned> iteBranch;
- std::map<Node, std::vector<unsigned> > justifyArgs;
visit.push_back(n);
std::unordered_set<TNode, TNodeHashFunction> visited;
~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<Node>& vars,
const std::vector<Node>& subs,
std::vector<Node>& 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<Node>& vars,
+ const std::vector<Node>& subs,
+ std::vector<Node>& reqVars,
+ std::vector<Node>& impliedVars);
private:
+ /** Common helper function for the above functions. */
+ static bool findInternal(Node t,
+ Node target,
+ const std::vector<Node>& vars,
+ const std::vector<Node>& subs,
+ std::vector<Node>& reqVars);
/** is singular arg
*
* Returns true if
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
-; 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)
--- /dev/null
+; 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)
projects / cvc5.git / commitdiff