This PR introduces the notion of a "skolem function" to SkolemManager, which is implemented as a simple cache of canonical skolem functions/variables.
This is a prerequisite for two things:
(1) Making progress on the LFSC proof conversion, which currently is cumbersome for skolems corresponding to regular expression unfolding.
(2) Cleaning up singletons. Having the ability make canonical skolem functions in skolem manager will enable Theory::expandDefinitions to move to TheoryRewriter::expandDefinitions. This will then enable removal of calls to SmtEngine::expandDefinitions.
This PR also makes arithmetic make use of this functionality already.
The next steps will be to clean up all raw uses of NodeManager::mkSkolem, especially for other theories that manually track allocated skolem functions.
#include "expr/skolem_manager.h"
+#include <sstream>
+
#include "expr/attribute.h"
#include "expr/bound_var_manager.h"
#include "expr/node_algorithm.h"
};
typedef expr::Attribute<OriginalFormAttributeId, Node> OriginalFormAttribute;
+const char* toString(SkolemFunId id)
+{
+ switch (id)
+ {
+ case SkolemFunId::DIV_BY_ZERO: return "DIV_BY_ZERO";
+ case SkolemFunId::INT_DIV_BY_ZERO: return "INT_DIV_BY_ZERO";
+ case SkolemFunId::MOD_BY_ZERO: return "MOD_BY_ZERO";
+ case SkolemFunId::SQRT: return "SQRT";
+ default: return "?";
+ }
+}
+
+std::ostream& operator<<(std::ostream& out, SkolemFunId id)
+{
+ out << toString(id);
+ return out;
+}
+
Node SkolemManager::mkSkolem(Node v,
Node pred,
const std::string& prefix,
return k;
}
+Node SkolemManager::mkSkolemFunction(SkolemFunId id, TypeNode tn, Node cacheVal)
+{
+ std::pair<SkolemFunId, Node> key(id, cacheVal);
+ std::map<std::pair<SkolemFunId, Node>, Node>::iterator it =
+ d_skolemFuns.find(key);
+ if (it == d_skolemFuns.end())
+ {
+ NodeManager* nm = NodeManager::currentNM();
+ std::stringstream ss;
+ ss << "SKOLEM_FUN_" << id;
+ Node k = nm->mkSkolem(ss.str(), tn, "an internal skolem function");
+ d_skolemFuns[key] = k;
+ return k;
+ }
+ return it->second;
+}
+
Node SkolemManager::mkBooleanTermVariable(Node t)
{
return mkPurifySkolem(t, "", "", NodeManager::SKOLEM_BOOL_TERM_VAR);
class ProofGenerator;
+/** Skolem function identifier */
+enum class SkolemFunId
+{
+ /* an uninterpreted function f s.t. f(x) = x / 0.0 (real division) */
+ DIV_BY_ZERO,
+ /* an uninterpreted function f s.t. f(x) = x / 0 (integer division) */
+ INT_DIV_BY_ZERO,
+ /* an uninterpreted function f s.t. f(x) = x mod 0 */
+ MOD_BY_ZERO,
+ /* an uninterpreted function f s.t. f(x) = sqrt(x) */
+ SQRT,
+};
+/** Converts a skolem function name to a string. */
+const char* toString(SkolemFunId id);
+/** Writes a skolem function name to a stream. */
+std::ostream& operator<<(std::ostream& out, SkolemFunId id);
+
/**
* A manager for skolems that can be used in proofs. This is designed to be
* a trusted interface to NodeManager::mkSkolem, where one
* Furthermore, note that original form and witness form may share skolems
* in the rare case that a witness term is purified. This is currently only the
* case for algorithms that introduce witness, e.g. BV/set instantiation.
+ *
+ * Additionally, we consider a third class of skolems (mkSkolemFunction) which
+ * are for convenience associated with an identifier, and not a witness term.
*/
class SkolemManager
{
const std::string& prefix,
const std::string& comment = "",
int flags = NodeManager::SKOLEM_DEFAULT);
+ /**
+ * Make skolem function. This method should be used for creating fixed
+ * skolem functions of the forms described in SkolemFunId. The user of this
+ * method is responsible for providing a proper type for the identifier that
+ * matches the description of id. Skolem functions are useful for modelling
+ * the behavior of partial functions, or for theory-specific inferences that
+ * introduce fresh variables.
+ *
+ * A skolem function is not given a formal semantics in terms of a witness
+ * term, nor is it a purification skolem, thus it does not fall into the two
+ * categories of skolems above. This method is motivated by convenience, as
+ * the user of this method does not require constructing canonical variables
+ * for witness terms.
+ *
+ * The returned skolem is an ordinary skolem variable that can be used
+ * e.g. in APPLY_UF terms when tn is a function type.
+ *
+ * Notice that we do not insist that tn is a function type. A user of this
+ * method may construct a canonical (first-order) skolem using this method
+ * as well.
+ *
+ * @param id The identifier of the skolem function
+ * @param tn The type of the returned skolem function
+ * @param cacheVal A cache value. The returned skolem function will be
+ * unique to the pair (id, cacheVal). This value is required, for instance,
+ * for skolem functions that are in fact families of skolem functions,
+ * e.g. the wrongly applied case of selectors.
+ * @return The skolem function.
+ */
+ Node mkSkolemFunction(SkolemFunId id,
+ TypeNode tn,
+ Node cacheVal = Node::null());
/**
* Make Boolean term variable for term t. This is a special case of
* mkPurifySkolem above, where the returned term has kind
static Node getOriginalForm(Node n);
private:
+ /**
+ * Cached of skolem functions for mkSkolemFunction above.
+ */
+ std::map<std::pair<SkolemFunId, Node>, Node> d_skolemFuns;
/**
* Mapping from witness terms to proof generators.
*/
#include "expr/attribute.h"
#include "expr/bound_var_manager.h"
-#include "expr/skolem_manager.h"
#include "expr/term_conversion_proof_generator.h"
#include "options/arith_options.h"
#include "smt/logic_exception.h"
if (!den.isConst() || den.getConst<Rational>().sgn() == 0)
{
checkNonLinearLogic(node);
- Node divByZeroNum = getArithSkolemApp(num, ArithSkolemId::DIV_BY_ZERO);
+ Node divByZeroNum = getArithSkolemApp(num, SkolemFunId::DIV_BY_ZERO);
Node denEq0 = nm->mkNode(EQUAL, den, nm->mkConst(Rational(0)));
ret = nm->mkNode(ITE, denEq0, divByZeroNum, ret);
}
{
checkNonLinearLogic(node);
Node intDivByZeroNum =
- getArithSkolemApp(num, ArithSkolemId::INT_DIV_BY_ZERO);
+ getArithSkolemApp(num, SkolemFunId::INT_DIV_BY_ZERO);
Node denEq0 = nm->mkNode(EQUAL, den, nm->mkConst(Rational(0)));
ret = nm->mkNode(ITE, denEq0, intDivByZeroNum, ret);
}
if (!den.isConst() || den.getConst<Rational>().sgn() == 0)
{
checkNonLinearLogic(node);
- Node modZeroNum = getArithSkolemApp(num, ArithSkolemId::MOD_BY_ZERO);
+ Node modZeroNum = getArithSkolemApp(num, SkolemFunId::MOD_BY_ZERO);
Node denEq0 = nm->mkNode(EQUAL, den, nm->mkConst(Rational(0)));
ret = nm->mkNode(ITE, denEq0, modZeroNum, ret);
}
Node lem;
if (k == SQRT)
{
- Node skolemApp = getArithSkolemApp(node[0], ArithSkolemId::SQRT);
+ Node skolemApp = getArithSkolemApp(node[0], SkolemFunId::SQRT);
Node uf = skolemApp.eqNode(var);
Node nonNeg =
nm->mkNode(AND, nm->mkNode(MULT, var, var).eqNode(node[0]), uf);
Node OperatorElim::getAxiomFor(Node n) { return Node::null(); }
-Node OperatorElim::getArithSkolem(ArithSkolemId asi)
+Node OperatorElim::getArithSkolem(SkolemFunId id)
{
- std::map<ArithSkolemId, Node>::iterator it = d_arith_skolem.find(asi);
- if (it == d_arith_skolem.end())
+ std::map<SkolemFunId, Node>::iterator it = d_arithSkolem.find(id);
+ if (it == d_arithSkolem.end())
{
NodeManager* nm = NodeManager::currentNM();
-
TypeNode tn;
- std::string name;
- std::string desc;
- switch (asi)
+ if (id == SkolemFunId::DIV_BY_ZERO || id == SkolemFunId::SQRT)
{
- case ArithSkolemId::DIV_BY_ZERO:
- tn = nm->realType();
- name = std::string("divByZero");
- desc = std::string("partial real division");
- break;
- case ArithSkolemId::INT_DIV_BY_ZERO:
- tn = nm->integerType();
- name = std::string("intDivByZero");
- desc = std::string("partial int division");
- break;
- case ArithSkolemId::MOD_BY_ZERO:
- tn = nm->integerType();
- name = std::string("modZero");
- desc = std::string("partial modulus");
- break;
- case ArithSkolemId::SQRT:
- tn = nm->realType();
- name = std::string("sqrtUf");
- desc = std::string("partial sqrt");
- break;
- default: Unhandled();
+ tn = nm->realType();
+ }
+ else
+ {
+ tn = nm->integerType();
}
-
Node skolem;
+ SkolemManager* sm = nm->getSkolemManager();
if (options::arithNoPartialFun())
{
- // partial function: division
- skolem = nm->mkSkolem(name, tn, desc, NodeManager::SKOLEM_EXACT_NAME);
+ // partial function: division, where we treat the skolem function as
+ // a constant
+ skolem = sm->mkSkolemFunction(id, tn);
}
else
{
// partial function: division
- skolem = nm->mkSkolem(name,
- nm->mkFunctionType(tn, tn),
- desc,
- NodeManager::SKOLEM_EXACT_NAME);
+ skolem = sm->mkSkolemFunction(id, nm->mkFunctionType(tn, tn));
}
- d_arith_skolem[asi] = skolem;
+ // cache it
+ d_arithSkolem[id] = skolem;
return skolem;
}
return it->second;
}
-Node OperatorElim::getArithSkolemApp(Node n, ArithSkolemId asi)
+Node OperatorElim::getArithSkolemApp(Node n, SkolemFunId id)
{
- Node skolem = getArithSkolem(asi);
+ Node skolem = getArithSkolem(id);
if (!options::arithNoPartialFun())
{
skolem = NodeManager::currentNM()->mkNode(APPLY_UF, skolem, n);
#include <map>
#include "expr/node.h"
+#include "expr/skolem_manager.h"
#include "theory/eager_proof_generator.h"
#include "theory/logic_info.h"
#include "theory/skolem_lemma.h"
private:
/** Logic info of the owner of this class */
const LogicInfo& d_info;
-
- /** Arithmetic skolem identifier */
- enum class ArithSkolemId
- {
- /* an uninterpreted function f s.t. f(x) = x / 0.0 (real division) */
- DIV_BY_ZERO,
- /* an uninterpreted function f s.t. f(x) = x / 0 (integer division) */
- INT_DIV_BY_ZERO,
- /* an uninterpreted function f s.t. f(x) = x mod 0 */
- MOD_BY_ZERO,
- /* an uninterpreted function f s.t. f(x) = sqrt(x) */
- SQRT,
- };
-
/**
* Function symbols used to implement:
* (1) Uninterpreted division-by-zero semantics. Needed to deal with partial
* If the option arithNoPartialFun() is enabled, then the range of this map
* stores Skolem constants instead of Skolem functions, meaning that the
* function-ness of e.g. division by zero is ignored.
+ *
+ * Note that this cache is used only for performance reasons. Conceptually,
+ * these skolem functions actually live in SkolemManager.
*/
- std::map<ArithSkolemId, Node> d_arith_skolem;
+ std::map<SkolemFunId, Node> d_arithSkolem;
/**
* Eliminate operators in term n. If n has top symbol that is not a core
* one (including division, int division, mod, to_int, is_int, syntactic sugar
* Returns the Skolem in the above map for the given id, creating it if it
* does not already exist.
*/
- Node getArithSkolem(ArithSkolemId asi);
+ Node getArithSkolem(SkolemFunId asi);
/**
* Make the witness term, which creates a witness term based on the skolem
* manager with this class as a proof generator.
* If the option arithNoPartialFun is enabled, this returns f, where f is
* the Skolem constant for the identifier asi.
*/
- Node getArithSkolemApp(Node n, ArithSkolemId asi);
+ Node getArithSkolemApp(Node n, SkolemFunId asi);
/**
* Called when a non-linear term n is given to this class. Throw an exception
projects / cvc5.git / commitdiff