This makes all methods for constructing skolems local to SkolemManager.
It removes infrastructure for node manager listeners being notified when skolems are constructed. This was used for 2 things:
(1) The old dumping infrastructure, where skolems could contribute in part to traces to print benchmarks. This code will be deleted soon.
(2) The miplib preprocessing pass, which used this functionality to listen to what skolems were constructed, and subsequently assumed these skolems coincided with what Boolean variables appeared in assertions. This is highly error prone, and has been replaced by a simple traversal to collect Boolean variables in assertions.
This is in preparation for a lazy lambda lifting technique, which will require more infrastructure in SkolemManager.
SkolemManager* sm = nm->getSkolemManager();
TypeNode stype = nm->mkSelectorType(dtt, t);
Node nindex = nm->mkConst(Rational(index));
- s = sm->mkSkolemFunction(SkolemFunId::SHARED_SELECTOR,
- stype,
- nindex,
- NodeManager::SKOLEM_NO_NOTIFY);
+ s = sm->mkSkolemFunction(SkolemFunId::SHARED_SELECTOR, stype, nindex);
d_sharedSel[dtt][t][index] = s;
Trace("dt-shared-sel") << "Made " << s << " of type " << dtt << " -> " << t
<< std::endl;
Assert(!isResolved());
Assert(!selectorType.isNull());
SkolemManager* sm = NodeManager::currentNM()->getSkolemManager();
- Node sel = sm->mkDummySkolem(
- "unresolved_" + selectorName,
- selectorType,
- "is an unresolved selector type placeholder",
- NodeManager::SKOLEM_EXACT_NAME | NodeManager::SKOLEM_NO_NOTIFY);
+ Node sel = sm->mkDummySkolem("unresolved_" + selectorName,
+ selectorType,
+ "is an unresolved selector type placeholder",
+ SkolemManager::SKOLEM_EXACT_NAME);
// can use null updater for now
Node nullNode;
Trace("datatypes") << "DTypeConstructor::addArg: " << sel << std::endl;
}
// Internally, selectors (and updaters) are fresh internal skolems which
// we constructor via mkDummySkolem.
- arg->d_selector = sm->mkDummySkolem(
- argName,
- nm->mkSelectorType(self, range),
- "is a selector",
- NodeManager::SKOLEM_EXACT_NAME | NodeManager::SKOLEM_NO_NOTIFY);
+ arg->d_selector = sm->mkDummySkolem(argName,
+ nm->mkSelectorType(self, range),
+ "is a selector",
+ SkolemManager::SKOLEM_EXACT_NAME);
std::string updateName("update_" + argName);
- arg->d_updater = sm->mkDummySkolem(
- updateName,
- nm->mkDatatypeUpdateType(self, range),
- "is a selector",
- NodeManager::SKOLEM_EXACT_NAME | NodeManager::SKOLEM_NO_NOTIFY);
+ arg->d_updater = sm->mkDummySkolem(updateName,
+ nm->mkDatatypeUpdateType(self, range),
+ "is a selector",
+ SkolemManager::SKOLEM_EXACT_NAME);
// must set indices to ensure datatypes::utils::indexOf works
arg->d_selector.setAttribute(DTypeConsIndexAttr(), cindex);
arg->d_selector.setAttribute(DTypeIndexAttr(), index);
// The name of the tester variable does not matter, it is only used
// internally.
std::string testerName("is_" + d_name);
- d_tester = sm->mkDummySkolem(
- testerName,
- nm->mkTesterType(self),
- "is a tester",
- NodeManager::SKOLEM_EXACT_NAME | NodeManager::SKOLEM_NO_NOTIFY);
- d_constructor = sm->mkDummySkolem(
- getName(),
- nm->mkConstructorType(argTypes, self),
- "is a constructor",
- NodeManager::SKOLEM_EXACT_NAME | NodeManager::SKOLEM_NO_NOTIFY);
+ d_tester = sm->mkDummySkolem(testerName,
+ nm->mkTesterType(self),
+ "is a tester",
+ SkolemManager::SKOLEM_EXACT_NAME);
+ d_constructor = sm->mkDummySkolem(getName(),
+ nm->mkConstructorType(argTypes, self),
+ "is a constructor",
+ SkolemManager::SKOLEM_EXACT_NAME);
Assert(d_constructor.getType().isConstructor());
// associate constructor with all selectors
for (std::shared_ptr<DTypeSelector> sel : d_args)
d_attrManager(new expr::attr::AttributeManager()),
d_nodeUnderDeletion(nullptr),
d_inReclaimZombies(false),
- d_abstractValueCount(0),
- d_skolemCounter(0)
+ d_abstractValueCount(0)
{
}
return typeNode;
}
-Node NodeManager::mkSkolem(const std::string& prefix, const TypeNode& type, const std::string& comment, int flags) {
- Node n = NodeBuilder(this, kind::SKOLEM);
- setAttribute(n, TypeAttr(), type);
- setAttribute(n, TypeCheckedAttr(), true);
- if((flags & SKOLEM_EXACT_NAME) == 0) {
- stringstream name;
- name << prefix << '_' << ++d_skolemCounter;
- setAttribute(n, expr::VarNameAttr(), name.str());
- } else {
- setAttribute(n, expr::VarNameAttr(), prefix);
- }
- if((flags & SKOLEM_NO_NOTIFY) == 0) {
- for(vector<NodeManagerListener*>::iterator i = d_listeners.begin(); i != d_listeners.end(); ++i) {
- (*i)->nmNotifyNewSkolem(n, comment, (flags & SKOLEM_IS_GLOBAL) == SKOLEM_IS_GLOBAL);
- }
- }
- return n;
-}
-
TypeNode NodeManager::mkBagType(TypeNode elementType)
{
CheckArgument(
return n;
}
-Node NodeManager::mkBooleanTermVariable() {
- Node n = NodeBuilder(this, kind::BOOLEAN_TERM_VARIABLE);
- n.setAttribute(TypeAttr(), booleanType());
- n.setAttribute(TypeCheckedAttr(), true);
- return n;
-}
-
Node NodeManager::mkNullaryOperator(const TypeNode& type, Kind k) {
std::map< TypeNode, Node >::iterator it = d_unique_vars[k].find( type );
if( it==d_unique_vars[k].end() ){
{
}
virtual void nmNotifyNewVar(TNode n) {}
- virtual void nmNotifyNewSkolem(TNode n, const std::string& comment,
- uint32_t flags) {}
/**
* Notify a listener of a Node that's being GCed. If this function stores a
* reference
*/
unsigned d_abstractValueCount;
- /**
- * A counter used to produce unique skolem names.
- *
- * Note that it is NOT incremented when skolems are created using
- * SKOLEM_EXACT_NAME, so it is NOT a count of the skolems produced
- * by this node manager.
- */
- unsigned d_skolemCounter;
-
/**
* Look up a NodeValue in the pool associated to this NodeManager.
* The NodeValue argument need not be a "completely-constructed"
/** Create a variable with the given type. */
Node mkVar(const TypeNode& type);
- /**
- * Create a skolem constant with the given name, type, and comment. For
- * details, see SkolemManager::mkDummySkolem, which calls this method.
- *
- * This method is intentionally private. To create skolems, one should
- * call a method from SkolemManager for allocating a skolem in a standard
- * way, or otherwise use SkolemManager::mkDummySkolem.
- */
- Node mkSkolem(const std::string& prefix,
- const TypeNode& type,
- const std::string& comment = "",
- int flags = SKOLEM_DEFAULT);
-
public:
/**
* Initialize the node manager by adding a null node to the pool and filling
*/
Node mkChain(Kind kind, const std::vector<Node>& children);
- /**
- * Optional flags used to control behavior of NodeManager::mkSkolem().
- * They should be composed with a bitwise OR (e.g.,
- * "SKOLEM_NO_NOTIFY | SKOLEM_EXACT_NAME"). Of course, SKOLEM_DEFAULT
- * cannot be composed in such a manner.
- */
- enum SkolemFlags
- {
- SKOLEM_DEFAULT = 0, /**< default behavior */
- SKOLEM_NO_NOTIFY = 1, /**< do not notify subscribers */
- SKOLEM_EXACT_NAME = 2, /**< do not make the name unique by adding the id */
- SKOLEM_IS_GLOBAL = 4, /**< global vars appear in models even after a pop */
- SKOLEM_BOOL_TERM_VAR = 8 /**< vars requiring kind BOOLEAN_TERM_VARIABLE */
- }; /* enum SkolemFlags */
-
/** Create a instantiation constant with the given type. */
Node mkInstConstant(const TypeNode& type);
- /** Create a boolean term variable. */
- Node mkBooleanTermVariable();
-
/** Make a new abstract value with the given type. */
Node mkAbstractValue(const TypeNode& type);
#include "expr/attribute.h"
#include "expr/bound_var_manager.h"
#include "expr/node_algorithm.h"
+#include "expr/node_manager_attributes.h"
using namespace cvc5::kind;
return out;
}
+SkolemManager::SkolemManager() : d_skolemCounter(0) {}
+
Node SkolemManager::mkSkolem(Node v,
Node pred,
const std::string& prefix,
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", flags);
+ Node k = mkSkolemNode(ss.str(), tn, "an internal skolem function", flags);
d_skolemFuns[key] = k;
d_skolemFunMap[k] = key;
return k;
const std::string& comment,
int flags)
{
- return NodeManager::currentNM()->mkSkolem(prefix, type, comment, flags);
+ return mkSkolemNode(prefix, type, comment, flags);
}
ProofGenerator* SkolemManager::getProofGenerator(Node t) const
int flags)
{
// note that witness, original forms are independent, but share skolems
- NodeManager* nm = NodeManager::currentNM();
// w is not necessarily a witness term
SkolemFormAttribute sfa;
- Node k;
// could already have a skolem if we used w already
if (w.hasAttribute(sfa))
{
return w.getAttribute(sfa);
}
// make the new skolem
- if (flags & NodeManager::SKOLEM_BOOL_TERM_VAR)
- {
- Assert (w.getType().isBoolean());
- k = nm->mkBooleanTermVariable();
- }
- else
- {
- k = nm->mkSkolem(prefix, w.getType(), comment, flags);
- }
+ Node k = mkSkolemNode(prefix, w.getType(), comment, flags);
// set skolem form attribute for w
w.setAttribute(sfa, k);
Trace("sk-manager") << "SkolemManager::mkSkolem: " << k << " : " << w
return k;
}
+Node SkolemManager::mkSkolemNode(const std::string& prefix,
+ const TypeNode& type,
+ const std::string& comment,
+ int flags)
+{
+ NodeManager* nm = NodeManager::currentNM();
+ Node n;
+ if (flags & SKOLEM_BOOL_TERM_VAR)
+ {
+ Assert(type.isBoolean());
+ n = NodeBuilder(nm, BOOLEAN_TERM_VARIABLE);
+ }
+ else
+ {
+ n = NodeBuilder(nm, SKOLEM);
+ if ((flags & SKOLEM_EXACT_NAME) == 0)
+ {
+ std::stringstream name;
+ name << prefix << '_' << ++d_skolemCounter;
+ n.setAttribute(expr::VarNameAttr(), name.str());
+ }
+ else
+ {
+ n.setAttribute(expr::VarNameAttr(), prefix);
+ }
+ }
+ n.setAttribute(expr::TypeAttr(), type);
+ n.setAttribute(expr::TypeCheckedAttr(), true);
+ return n;
+}
+
} // namespace cvc5
class SkolemManager
{
public:
- SkolemManager() {}
+ SkolemManager();
~SkolemManager() {}
+
+ /**
+ * Optional flags used to control behavior of skolem creation.
+ * They should be composed with a bitwise OR (e.g.,
+ * "SKOLEM_BOOL_TERM_VAR | SKOLEM_EXACT_NAME"). Of course, SKOLEM_DEFAULT
+ * cannot be composed in such a manner.
+ */
+ enum SkolemFlags
+ {
+ SKOLEM_DEFAULT = 0, /**< default behavior */
+ SKOLEM_EXACT_NAME = 1, /**< do not make the name unique by adding the id */
+ SKOLEM_BOOL_TERM_VAR = 2 /**< vars requiring kind BOOLEAN_TERM_VARIABLE */
+ };
/**
* This makes a skolem of same type as bound variable v, (say its type is T),
* whose definition is (witness ((v T)) pred). This definition is maintained
* variable v.
* @param prefix The prefix of the name of the Skolem
* @param comment Debug information about the Skolem
- * @param flags The flags for the Skolem (see NodeManager::mkSkolem)
+ * @param flags The flags for the Skolem (see SkolemFlags)
* @param pg The proof generator for this skolem. If non-null, this proof
* generator must respond to a call to getProofFor(exists v. pred) during
* the lifetime of the current node manager.
Node pred,
const std::string& prefix,
const std::string& comment = "",
- int flags = NodeManager::SKOLEM_DEFAULT,
+ int flags = SKOLEM_DEFAULT,
ProofGenerator* pg = nullptr);
/**
* Make skolemized form of existentially quantified formula q, and store its
* @param skolems Vector to add Skolems of q to,
* @param prefix The prefix of the name of each of the Skolems
* @param comment Debug information about each of the Skolems
- * @param flags The flags for the Skolem (see NodeManager::mkSkolem)
+ * @param flags The flags for the Skolem (see SkolemFlags)
* @param pg The proof generator for this skolem. If non-null, this proof
* generator must respond to a call to getProofFor(q) during
* the lifetime of the current node manager.
std::vector<Node>& skolems,
const std::string& prefix,
const std::string& comment = "",
- int flags = NodeManager::SKOLEM_DEFAULT,
+ int flags = SKOLEM_DEFAULT,
ProofGenerator* pg = nullptr);
/**
* Same as above, but for special case of (witness ((x T)) (= x t))
Node mkPurifySkolem(Node t,
const std::string& prefix,
const std::string& comment = "",
- int flags = NodeManager::SKOLEM_DEFAULT);
+ int flags = 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
Node mkSkolemFunction(SkolemFunId id,
TypeNode tn,
Node cacheVal = Node::null(),
- int flags = NodeManager::SKOLEM_DEFAULT);
+ int flags = SKOLEM_DEFAULT);
/** Same as above, with multiple cache values */
Node mkSkolemFunction(SkolemFunId id,
TypeNode tn,
const std::vector<Node>& cacheVals,
- int flags = NodeManager::SKOLEM_DEFAULT);
+ int flags = SKOLEM_DEFAULT);
/**
* Is k a skolem function? Returns true if k was generated by the above call.
* Updates the arguments to the values used when constructing it.
* being dumped, this is included in a comment before the declaration
* and can be quite useful for debugging
* @param flags an optional mask of bits from SkolemFlags to control
- * mkSkolem() behavior
+ * skolem behavior
*/
Node mkDummySkolem(const std::string& prefix,
const TypeNode& type,
const std::string& comment = "",
- int flags = NodeManager::SKOLEM_DEFAULT);
+ int flags = SKOLEM_DEFAULT);
/**
* Get proof generator for existentially quantified formula q. This returns
* the proof generator that was provided in a call to mkSkolem above.
* Mapping from witness terms to proof generators.
*/
std::map<Node, ProofGenerator*> d_gens;
+
+ /**
+ * A counter used to produce unique skolem names.
+ *
+ * Note that it is NOT incremented when skolems are created using
+ * SKOLEM_EXACT_NAME, so it is NOT a count of the skolems produced
+ * by this node manager.
+ */
+ size_t d_skolemCounter;
/** Get or make skolem attribute for term w, which may be a witness term */
- static Node mkSkolemInternal(Node w,
- const std::string& prefix,
- const std::string& comment,
- int flags);
+ Node mkSkolemInternal(Node w,
+ const std::string& prefix,
+ const std::string& comment,
+ int flags);
/**
* Skolemize the first variable of existentially quantified formula q.
* For example, calling this method on:
Node& qskolem,
const std::string& prefix,
const std::string& comment = "",
- int flags = NodeManager::SKOLEM_DEFAULT);
+ int flags = SKOLEM_DEFAULT);
+ /**
+ * Create a skolem constant with the given name, type, and comment.
+ *
+ * This method is intentionally private. To create skolems, one should
+ * call a public method from SkolemManager for allocating a skolem in a
+ * proper way, or otherwise use SkolemManager::mkDummySkolem.
+ */
+ Node mkSkolemNode(const std::string& prefix,
+ const TypeNode& type,
+ const std::string& comment = "",
+ int flags = SKOLEM_DEFAULT);
};
} // namespace cvc5
: PreprocessingPass(preprocContext, "miplib-trick"),
d_statistics(statisticsRegistry())
{
- if (!options().base.incrementalSolving)
- {
- NodeManager::currentNM()->subscribeEvents(this);
- }
}
MipLibTrick::~MipLibTrick()
{
- if (!options().base.incrementalSolving)
- {
- NodeManager::currentNM()->unsubscribeEvents(this);
- }
}
/**
return 0;
}
-void MipLibTrick::nmNotifyNewVar(TNode n)
+void MipLibTrick::collectBooleanVariables(
+ AssertionPipeline* assertionsToPreprocess)
{
- if (n.getType().isBoolean())
+ d_boolVars.clear();
+ std::unordered_set<TNode> visited;
+ std::unordered_set<TNode>::iterator it;
+ std::vector<TNode> visit;
+ TNode cur;
+ for (size_t i = 0, size = assertionsToPreprocess->size(); i < size; ++i)
{
- d_boolVars.push_back(n);
+ visit.push_back((*assertionsToPreprocess)[i]);
}
-}
-
-void MipLibTrick::nmNotifyNewSkolem(TNode n,
- const std::string& comment,
- uint32_t flags)
-{
- if (n.getType().isBoolean())
+ do
{
- d_boolVars.push_back(n);
- }
+ cur = visit.back();
+ visit.pop_back();
+ it = visited.find(cur);
+
+ if (it == visited.end())
+ {
+ visited.insert(cur);
+ if (cur.isVar() && cur.getType().isBoolean())
+ {
+ d_boolVars.push_back(cur);
+ }
+ visit.insert(visit.end(), cur.begin(), cur.end());
+ }
+ } while (!visit.empty());
}
PreprocessingPassResult MipLibTrick::applyInternal(
== assertionsToPreprocess->size());
Assert(!options().base.incrementalSolving);
+ // collect Boolean variables
+ collectBooleanVariables(assertionsToPreprocess);
+
context::Context fakeContext;
TheoryEngine* te = d_preprocContext->getTheoryEngine();
booleans::CircuitPropagator* propagator =
Node newVar = sm->mkDummySkolem(
ss.str(),
nm->integerType(),
- "a variable introduced due to scrubbing a miplib encoding",
- NodeManager::SKOLEM_EXACT_NAME);
+ "a variable introduced due to scrubbing a miplib encoding");
Node geq = rewrite(nm->mkNode(kind::GEQ, newVar, zero));
Node leq = rewrite(nm->mkNode(kind::LEQ, newVar, one));
TrustNode tgeq = TrustNode::mkTrustLemma(geq, nullptr);
namespace preprocessing {
namespace passes {
-class MipLibTrick : public PreprocessingPass, public NodeManagerListener
+class MipLibTrick : public PreprocessingPass
{
public:
MipLibTrick(PreprocessingPassContext* preprocContext);
~MipLibTrick();
- // NodeManagerListener callbacks to collect d_boolVars.
- void nmNotifyNewVar(TNode n) override;
- void nmNotifyNewSkolem(TNode n,
- const std::string& comment,
- uint32_t flags) override;
-
protected:
PreprocessingPassResult applyInternal(
AssertionPipeline* assertionsToPreprocess) override;
size_t removeFromConjunction(
Node& n, const std::unordered_set<unsigned long>& toRemove);
+ /**
+ * Collect Boolean variables in the given pipeline, store them in d_boolVars.
+ */
+ void collectBooleanVariables(AssertionPipeline* assertionsToPreprocess);
Statistics d_statistics;
d_dm.addToDump(c);
}
-void SmtNodeManagerListener::nmNotifyNewSkolem(TNode n,
- const std::string& comment,
- uint32_t flags)
-{
- std::string id = n.getAttribute(expr::VarNameAttr());
- DeclareFunctionNodeCommand c(id, n, n.getType());
- if (Dump.isOn("skolems") && comment != "")
- {
- d_outMgr.getPrinter().toStreamCmdSetInfo(
- d_outMgr.getDumpOut(), "notes", id + " is " + comment);
- }
- d_dm.addToDump(c, "skolems");
-}
-
} // namespace smt
} // namespace cvc5
uint32_t flags) override;
/** Notify when new variable is created */
void nmNotifyNewVar(TNode n) override;
- /** Notify when new skolem is created */
- void nmNotifyNewSkolem(TNode n,
- const std::string& comment,
- uint32_t flags) override;
/** Notify when a term is deleted */
void nmNotifyDeleteNode(TNode n) override {}
node,
"btvK",
"a Boolean term variable introduced during term formula removal",
- NodeManager::SKOLEM_BOOL_TERM_VAR);
+ SkolemManager::SKOLEM_BOOL_TERM_VAR);
d_skolem_cache.insert(node, skolem);
// The new assertion
{
NodeManager* nm = NodeManager::currentNM();
SkolemManager* sm = nm->getSkolemManager();
- d_ranVariable = sm->mkDummySkolem(
- "__z", nm->realType(), "", NodeManager::SKOLEM_EXACT_NAME);
+ d_ranVariable = sm->mkDummySkolem("__z", nm->realType(), "");
#ifdef CVC5_POLY_IMP
if (env.isTheoryProofProducing())
{
NodeManager* nm = NodeManager::currentNM();
SkolemManager* sm = nm->getSkolemManager();
// we mark that we should send a lemma
- Node k =
- sm->mkSkolem(v, pred, prefix, comment, NodeManager::SKOLEM_DEFAULT, this);
+ Node k = sm->mkSkolem(
+ v, pred, prefix, comment, SkolemManager::SKOLEM_DEFAULT, this);
if (d_pnm != nullptr)
{
Node lem = SkolemLemma::getSkolemLemmaFor(k);
args[0] = t;
args[1] = t;
fun = sm->mkDummySkolem("floatingpoint_min_zero_case",
- nm->mkFunctionType(args,
- nm->mkBitVectorType(1U)
- ),
- "floatingpoint_min_zero_case",
- NodeManager::SKOLEM_EXACT_NAME);
+ nm->mkFunctionType(args, nm->mkBitVectorType(1U)),
+ "floatingpoint_min_zero_case");
d_minMap.insert(t, fun);
}
else
args[0] = t;
args[1] = t;
fun = sm->mkDummySkolem("floatingpoint_max_zero_case",
- nm->mkFunctionType(args,
- nm->mkBitVectorType(1U)
- ),
- "floatingpoint_max_zero_case",
- NodeManager::SKOLEM_EXACT_NAME);
+ nm->mkFunctionType(args, nm->mkBitVectorType(1U)),
+ "floatingpoint_max_zero_case");
d_maxMap.insert(t, fun);
}
else
args[1] = source;
fun = sm->mkDummySkolem("floatingpoint_to_ubv_out_of_range_case",
nm->mkFunctionType(args, target),
- "floatingpoint_to_ubv_out_of_range_case",
- NodeManager::SKOLEM_EXACT_NAME);
+ "floatingpoint_to_ubv_out_of_range_case");
d_toUBVMap.insert(p, fun);
}
else
args[1] = source;
fun = sm->mkDummySkolem("floatingpoint_to_sbv_out_of_range_case",
nm->mkFunctionType(args, target),
- "floatingpoint_to_sbv_out_of_range_case",
- NodeManager::SKOLEM_EXACT_NAME);
+ "floatingpoint_to_sbv_out_of_range_case");
d_toSBVMap.insert(p, fun);
}
else
args[0] = t;
fun = sm->mkDummySkolem("floatingpoint_to_real_infinity_and_NaN_case",
nm->mkFunctionType(args, nm->realType()),
- "floatingpoint_to_real_infinity_and_NaN_case",
- NodeManager::SKOLEM_EXACT_NAME);
+ "floatingpoint_to_real_infinity_and_NaN_case");
d_toRealMap.insert(t, fun);
}
else
// Build purified head with fresh skolem and recreate node
std::stringstream ss;
ss << nb[0] << "_" << d_cand_to_hd_count[nb[0]]++;
- Node new_f = sm->mkDummySkolem(ss.str(),
- nb[0].getType(),
- "head of unif evaluation point",
- NodeManager::SKOLEM_EXACT_NAME);
+ Node new_f = sm->mkDummySkolem(
+ ss.str(), nb[0].getType(), "head of unif evaluation point");
// Adds new enumerator to map from candidate
Trace("sygus-unif-rl-purify")
<< "...new enum " << new_f << " for candidate " << nb[0] << "\n";
stringstream stream;
stream << "chooseUf" << setType.getId();
string name = stream.str();
- Node chooseSkolem = sm->mkDummySkolem(
- name, chooseUf, "choose function", NodeManager::SKOLEM_EXACT_NAME);
+ Node chooseSkolem = sm->mkDummySkolem(name, chooseUf, "choose function");
d_chooseFunctions[setType] = chooseSkolem;
return chooseSkolem;
}
{
// for sequences of Booleans, we may purify Boolean terms, in which case
// they must be Boolean term variables.
- int flags = a.getType().isBoolean() ? NodeManager::SKOLEM_BOOL_TERM_VAR
- : NodeManager::SKOLEM_DEFAULT;
+ int flags = a.getType().isBoolean() ? SkolemManager::SKOLEM_BOOL_TERM_VAR
+ : SkolemManager::SKOLEM_DEFAULT;
sk = sm->mkPurifySkolem(a, c, "string purify skolem", flags);
}
break;
TypeNode booleanType = d_nodeManager->booleanType();
Node w = d_skolemManager->mkDummySkolem(
- "w", booleanType, "", NodeManager::SKOLEM_EXACT_NAME);
+ "w", booleanType, "", SkolemManager::SKOLEM_EXACT_NAME);
Node x = d_skolemManager->mkDummySkolem(
- "x", booleanType, "", NodeManager::SKOLEM_EXACT_NAME);
+ "x", booleanType, "", SkolemManager::SKOLEM_EXACT_NAME);
Node y = d_skolemManager->mkDummySkolem(
- "y", booleanType, "", NodeManager::SKOLEM_EXACT_NAME);
+ "y", booleanType, "", SkolemManager::SKOLEM_EXACT_NAME);
Node z = d_skolemManager->mkDummySkolem(
- "z", booleanType, "", NodeManager::SKOLEM_EXACT_NAME);
+ "z", booleanType, "", SkolemManager::SKOLEM_EXACT_NAME);
Node m = NodeBuilder() << w << x << kind::OR;
Node n = NodeBuilder() << m << y << z << kind::AND;
TypeNode booleanType = d_nodeManager->booleanType();
Node w = d_skolemManager->mkDummySkolem(
- "w", booleanType, "", NodeManager::SKOLEM_EXACT_NAME);
+ "w", booleanType, "", SkolemManager::SKOLEM_EXACT_NAME);
Node x = d_skolemManager->mkDummySkolem(
- "x", booleanType, "", NodeManager::SKOLEM_EXACT_NAME);
+ "x", booleanType, "", SkolemManager::SKOLEM_EXACT_NAME);
Node y = d_skolemManager->mkDummySkolem(
- "y", booleanType, "", NodeManager::SKOLEM_EXACT_NAME);
+ "y", booleanType, "", SkolemManager::SKOLEM_EXACT_NAME);
Node z = d_skolemManager->mkDummySkolem(
- "z", booleanType, "", NodeManager::SKOLEM_EXACT_NAME);
+ "z", booleanType, "", SkolemManager::SKOLEM_EXACT_NAME);
Node m = NodeBuilder() << x << y << kind::OR;
Node n = NodeBuilder() << w << m << z << kind::AND;
Node o = NodeBuilder() << n << n << kind::XOR;
TypeNode fnType = d_nodeManager->mkFunctionType(intType, intType);
Node x = d_skolemManager->mkDummySkolem(
- "x", intType, "", NodeManager::SKOLEM_EXACT_NAME);
+ "x", intType, "", SkolemManager::SKOLEM_EXACT_NAME);
Node y = d_skolemManager->mkDummySkolem(
- "y", intType, "", NodeManager::SKOLEM_EXACT_NAME);
+ "y", intType, "", SkolemManager::SKOLEM_EXACT_NAME);
Node f = d_skolemManager->mkDummySkolem(
- "f", fnType, "", NodeManager::SKOLEM_EXACT_NAME);
+ "f", fnType, "", SkolemManager::SKOLEM_EXACT_NAME);
Node g = d_skolemManager->mkDummySkolem(
- "g", fnType, "", NodeManager::SKOLEM_EXACT_NAME);
+ "g", fnType, "", SkolemManager::SKOLEM_EXACT_NAME);
Node fx = d_nodeManager->mkNode(APPLY_UF, f, x);
Node fy = d_nodeManager->mkNode(APPLY_UF, f, y);
Node gx = d_nodeManager->mkNode(APPLY_UF, g, x);
TEST_F(TestNodeBlackNodeManager, mkSkolem_with_name)
{
Node x = d_skolemManager->mkDummySkolem(
- "x", *d_boolTypeNode, "", NodeManager::SKOLEM_EXACT_NAME);
+ "x", *d_boolTypeNode, "", SkolemManager::SKOLEM_EXACT_NAME);
ASSERT_EQ(x.getKind(), SKOLEM);
ASSERT_EQ(x.getNumChildren(), 0u);
ASSERT_EQ(x.getAttribute(VarNameAttr()), "x");
Node operator!(const Node& a) { return nodeManager->mkNode(Kind::NOT, a); }
Node make_real_variable(const std::string& s)
{
- return nodeManager->mkSkolem(
- s, nodeManager->realType(), "", NodeManager::SKOLEM_EXACT_NAME);
+ SkolemManager* sm = nodeManager->getSkolemManager();
+ return sm->mkDummySkolem(
+ s, nodeManager->realType(), "", SkolemManager::SKOLEM_EXACT_NAME);
}
Node make_int_variable(const std::string& s)
{
- return nodeManager->mkSkolem(
- s, nodeManager->integerType(), "", NodeManager::SKOLEM_EXACT_NAME);
+ SkolemManager* sm = nodeManager->getSkolemManager();
+ return sm->mkDummySkolem(
+ s, nodeManager->integerType(), "", SkolemManager::SKOLEM_EXACT_NAME);
}
TEST_F(TestTheoryWhiteArithCAD, test_univariate_isolation)
projects / cvc5.git / commitdiff