diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-09-11 13:08:00 -0500 |
---|---|---|
committer | Andres Noetzli <andres.noetzli@gmail.com> | 2018-09-11 11:08:00 -0700 |
commit | 64c48c4d3b4c26b0ba28ab1ab11ef2314ca0cbee (patch) | |
tree | ece6319150e855d2b0850f7508d9e3ee080b7f03 /src/theory/subs_minimize.h | |
parent | 2fb903ed7309fd97c848b03f6587c9d0604efd24 (diff) |
Support model cores via option --produce-model-cores. (#2407)
This adds support for model cores, fixes #1233.
It includes some minor cleanup and additions to utility functions.
Diffstat (limited to 'src/theory/subs_minimize.h')
-rw-r--r-- | src/theory/subs_minimize.h | 66 |
1 files changed, 66 insertions, 0 deletions
diff --git a/src/theory/subs_minimize.h b/src/theory/subs_minimize.h new file mode 100644 index 000000000..55e57b921 --- /dev/null +++ b/src/theory/subs_minimize.h @@ -0,0 +1,66 @@ +/********************* */ +/*! \file subs_minimize.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** 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 Substitution minimization. + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY__SUBS_MINIMIZE_H +#define __CVC4__THEORY__SUBS_MINIMIZE_H + +#include <vector> + +#include "expr/node.h" + +namespace CVC4 { +namespace theory { + +/** SubstitutionMinimize + * + * This class is used for finding a minimal substitution under which an + * evaluation holds. + */ +class SubstitutionMinimize +{ + public: + 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 n { vars -> subs } does not rewrite to target, this method returns + * false. + */ + static bool find(Node n, + Node target, + const std::vector<Node>& vars, + const std::vector<Node>& subs, + std::vector<Node>& reqVars); + + private: + /** is singular arg + * + * Returns true if + * <k>( ... t_{arg-1}, n, t_{arg+1}...) = c + * always holds for some constant c. + */ + static bool isSingularArg(Node n, Kind k, unsigned arg); +}; + +} // namespace theory +} // namespace CVC4 + +#endif /* __CVC4__THEORY__SUBS_MINIMIZE_H */ |