This is in preparation for refactoring skolem creation throughout the code base to improve proofs and migrate Theory::expandDefinitions to Rewriter::expandDefinitions.
This PR also eliminates some unused code in TheoryArithPrivate.
Followup PRs will start formalizing/eliminating calls to mkDummySkolem.
#include "expr/dtype_cons.h"
#include "expr/node_algorithm.h"
+#include "expr/skolem_manager.h"
#include "expr/type_matcher.h"
using namespace cvc5::kind;
NodeManager* nm = NodeManager::currentNM();
std::stringstream ss;
ss << "sel_" << index;
- s = nm->mkSkolem(ss.str(),
- nm->mkSelectorType(dtt, t),
- "is a shared selector",
- NodeManager::SKOLEM_NO_NOTIFY);
+ SkolemManager* sm = nm->getSkolemManager();
+ s = sm->mkDummySkolem(ss.str(),
+ nm->mkSelectorType(dtt, t),
+ "is a shared selector",
+ NodeManager::SKOLEM_NO_NOTIFY);
d_sharedSel[dtt][t][index] = s;
Trace("dt-shared-sel") << "Made " << s << " of type " << dtt << " -> " << t
<< std::endl;
#include "expr/dtype.h"
#include "expr/node_manager.h"
+#include "expr/skolem_manager.h"
#include "expr/type_matcher.h"
#include "options/datatypes_options.h"
// create the proper selector type)
Assert(!isResolved());
Assert(!selectorType.isNull());
-
- Node type = NodeManager::currentNM()->mkSkolem(
+ SkolemManager* sm = NodeManager::currentNM()->getSkolemManager();
+ Node type = sm->mkDummySkolem(
"unresolved_" + selectorName,
selectorType,
"is an unresolved selector type placeholder",
<< std::endl;
NodeManager* nm = NodeManager::currentNM();
+ SkolemManager* sm = nm->getSkolemManager();
size_t index = 0;
std::vector<TypeNode> argTypes;
Trace("datatypes-init") << "Initialize constructor " << d_name << std::endl;
{
Trace("datatypes-init") << " ...self selector" << std::endl;
range = self;
- arg->d_selector = nm->mkSkolem(
+ arg->d_selector = sm->mkDummySkolem(
argName,
nm->mkSelectorType(self, self),
"is a selector",
{
Trace("datatypes-init") << " ...resolved selector" << std::endl;
range = (*j).second;
- arg->d_selector = nm->mkSkolem(
+ arg->d_selector = sm->mkDummySkolem(
argName,
nm->mkSelectorType(self, range),
"is a selector",
}
Trace("datatypes-init")
<< " ...range after parametric substitution " << range << std::endl;
- arg->d_selector = nm->mkSkolem(
+ arg->d_selector = sm->mkDummySkolem(
argName,
nm->mkSelectorType(self, range),
"is a selector",
// The name of the tester variable does not matter, it is only used
// internally.
std::string testerName("is_" + d_name);
- d_tester = nm->mkSkolem(
+ d_tester = sm->mkDummySkolem(
testerName,
nm->mkTesterType(self),
"is a tester",
NodeManager::SKOLEM_EXACT_NAME | NodeManager::SKOLEM_NO_NOTIFY);
- d_constructor = nm->mkSkolem(
+ d_constructor = sm->mkDummySkolem(
getName(),
nm->mkConstructorType(argTypes, self),
"is a constructor",
friend class api::Solver;
friend class expr::NodeValue;
friend class expr::TypeChecker;
+ friend class SkolemManager;
friend class NodeBuilder;
friend class NodeManagerScope;
* lookup is done on the name. If you mkVar("a", type) and then
* mkVar("a", type) again, you have two variables. The NodeManager
* version of this is private to avoid internal uses of mkVar() from
- * within CVC4. Such uses should employ mkSkolem() instead.
+ * within CVC4. Such uses should employ SkolemManager::mkSkolem() instead.
*/
Node mkVar(const std::string& name, const TypeNode& type);
Node* mkVarPtr(const std::string& name, const TypeNode& type);
Node mkVar(const TypeNode& type);
Node* mkVarPtr(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:
explicit NodeManager();
~NodeManager();
SKOLEM_BOOL_TERM_VAR = 8 /**< vars requiring kind BOOLEAN_TERM_VARIABLE */
}; /* enum SkolemFlags */
- /**
- * Create a skolem constant with the given name, type, and comment.
- *
- * @param prefix the name of the new skolem variable is the prefix
- * appended with a unique ID. This way a family of skolem variables
- * can be made with unique identifiers, used in dump, tracing, and
- * debugging output. Use SKOLEM_EXECT_NAME flag if you don't want
- * a unique ID appended and use prefix as the name.
- *
- * @param type the type of the skolem variable to create
- *
- * @param comment a comment for dumping output; if declarations are
- * 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
- */
- Node mkSkolem(const std::string& prefix, const TypeNode& type,
- const std::string& comment = "", int flags = SKOLEM_DEFAULT);
-
/** Create a instantiation constant with the given type. */
Node mkInstConstant(const TypeNode& type);
return it->second;
}
+Node SkolemManager::mkDummySkolem(const std::string& prefix,
+ const TypeNode& type,
+ const std::string& comment,
+ int flags)
+{
+ return NodeManager::currentNM()->mkSkolem(prefix, type, comment, flags);
+}
+
Node SkolemManager::mkBooleanTermVariable(Node t)
{
return mkPurifySkolem(t, "", "", NodeManager::SKOLEM_BOOL_TERM_VAR);
Node mkSkolemFunction(SkolemFunId id,
TypeNode tn,
Node cacheVal = Node::null());
+ /**
+ * Create a skolem constant with the given name, type, and comment. This
+ * should only be used if the definition of the skolem does not matter.
+ * The definition of a skolem matters e.g. when the skolem is used in a
+ * proof.
+ *
+ * @param prefix the name of the new skolem variable is the prefix
+ * appended with a unique ID. This way a family of skolem variables
+ * can be made with unique identifiers, used in dump, tracing, and
+ * debugging output. Use SKOLEM_EXACT_NAME flag if you don't want
+ * a unique ID appended and use prefix as the name.
+ * @param type the type of the skolem variable to create
+ * @param comment a comment for dumping output; if declarations are
+ * 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
+ */
+ Node mkDummySkolem(const std::string& prefix,
+ const TypeNode& type,
+ const std::string& comment = "",
+ int flags = NodeManager::SKOLEM_DEFAULT);
/**
* Make Boolean term variable for term t. This is a special case of
* mkPurifySkolem above, where the returned term has kind
#include <sstream>
+#include "expr/skolem_manager.h"
#include "theory/rewriter.h"
namespace cvc5 {
void Subs::add(Node v)
{
+ SkolemManager* sm = NodeManager::currentNM()->getSkolemManager();
// default, use a fresh skolem of the same type
- Node s = NodeManager::currentNM()->mkSkolem("sk", v.getType());
+ Node s = sm->mkDummySkolem("sk", v.getType());
add(v, s);
}
#include "expr/sygus_datatype.h"
#include <sstream>
+#include "expr/skolem_manager.h"
using namespace cvc5::kind;
void SygusDatatype::addAnyConstantConstructor(TypeNode tn)
{
+ SkolemManager* sm = NodeManager::currentNM()->getSkolemManager();
// add an "any constant" proxy variable
- Node av = NodeManager::currentNM()->mkSkolem("_any_constant", tn);
+ Node av = sm->mkDummySkolem("_any_constant", tn);
// mark that it represents any constant
SygusAnyConstAttribute saca;
av.setAttribute(saca, true);
#include "base/check.h"
#include "expr/node_algorithm.h"
+#include "expr/skolem_manager.h"
#include "options/options.h"
#include "options/smt_options.h"
#include "preprocessing/assertion_pipeline.h"
if (set.find(term) == set.end())
{
TypeNode tn = term.getType();
- Node skolem = nm->mkSkolem("SKOLEM$$",
- tn,
- "is a variable created by the ackermannization "
- "preprocessing pass");
+ SkolemManager* sm = nm->getSkolemManager();
+ Node skolem =
+ sm->mkDummySkolem("SKOLEM$$",
+ tn,
+ "is a variable created by the ackermannization "
+ "preprocessing pass");
for (const auto& t : set)
{
addLemmaForPair(t, term, func, assertions, nm);
SubstitutionMap& usVarsToBVVars)
{
NodeManager* nm = NodeManager::currentNM();
+ SkolemManager* sm = nm->getSkolemManager();
for (TNode var : vars)
{
TypeNode type = var.getType();
size_t size = getBVSkolemSize(usortCardinality.at(type));
- Node skolem = nm->mkSkolem(
+ Node skolem = sm->mkDummySkolem(
"BVSKOLEM$$",
nm->mkBitVectorType(size),
"a variable created by the ackermannization "
#include "expr/node.h"
#include "expr/node_traversal.h"
+#include "expr/skolem_manager.h"
#include "options/smt_options.h"
#include "options/uf_options.h"
#include "preprocessing/assertion_pipeline.h"
Node BVToInt::translateNoChildren(Node original)
{
+ SkolemManager* sm = d_nm->getSkolemManager();
Node translation;
Assert(original.isVar() || original.isConst());
if (original.isVar())
// New integer variables that are not bound (symbolic constants)
// are added together with range constraints induced by the
// bit-width of the original bit-vector variables.
- Node newVar = d_nm->mkSkolem("__bvToInt_var",
- d_nm->integerType(),
- "Variable introduced in bvToInt "
- "pass instead of original variable "
- + original.toString());
+ Node newVar = sm->mkDummySkolem("__bvToInt_var",
+ d_nm->integerType(),
+ "Variable introduced in bvToInt "
+ "pass instead of original variable "
+ + original.toString());
uint64_t bvsize = original.getType().getBitVectorSize();
translation = newVar;
d_rangeAssertions.insert(mkRangeConstraint(newVar, bvsize));
{
intDomain.push_back(d.isBitVector() ? d_nm->integerType() : d);
}
+ SkolemManager* sm = d_nm->getSkolemManager();
ostringstream os;
os << "__bvToInt_fun_" << bvUF << "_int";
- intUF = d_nm->mkSkolem(
+ intUF = sm->mkDummySkolem(
os.str(), d_nm->mkFunctionType(intDomain, intRange), "bv2int function");
// introduce a `define-fun` in the smt-engine to keep
// the correspondence between the original
#include <sstream>
+#include "expr/skolem_manager.h"
#include "options/smt_options.h"
#include "preprocessing/assertion_pipeline.h"
#include "preprocessing/preprocessing_pass_context.h"
std::map<int, Node> subs_head;
// first pass : find defined functions, transform quantifiers
NodeManager* nm = NodeManager::currentNM();
+ SkolemManager* sm = nm->getSkolemManager();
for (size_t i = 0, asize = assertions.size(); i < asize; i++)
{
Node n = QuantAttributes::getFunDefHead(assertions[i]);
TypeNode typ = nm->mkFunctionType(iType, n[j].getType());
std::stringstream ssf;
ssf << f << "_arg_" << j;
- d_input_arg_inj[f].push_back(
- nm->mkSkolem(ssf.str(), typ, "op created during fun def fmf"));
+ d_input_arg_inj[f].push_back(sm->mkDummySkolem(
+ ssf.str(), typ, "op created during fun def fmf"));
}
// construct new quantifier forall S. F[f1(S)/x1....fn(S)/xn]
#include <sstream>
#include "expr/node_algorithm.h"
+#include "expr/skolem_manager.h"
#include "options/quantifiers_options.h"
#include "preprocessing/assertion_pipeline.h"
#include "theory/rewriter.h"
Node HoElim::eliminateLambdaComplete(Node n, std::map<Node, Node>& newLambda)
{
NodeManager* nm = NodeManager::currentNM();
+ SkolemManager* sm = nm->getSkolemManager();
std::unordered_map<Node, Node, TNodeHashFunction>::iterator it;
std::vector<Node> visit;
TNode cur;
}
TypeNode rangeType = cur.getType().getRangeType();
TypeNode nft = nm->mkFunctionType(ftypes, rangeType);
- Node nf = nm->mkSkolem("ll", nft);
+ Node nf = sm->mkDummySkolem("ll", nft);
Trace("ho-elim-ll")
<< "...introduce: " << nf << " of type " << nft << std::endl;
newLambda[nf] = nlambda;
{
Trace("ho-elim-assert") << "Ho-elim assertion: " << n << std::endl;
NodeManager* nm = NodeManager::currentNM();
+ SkolemManager* sm = nm->getSkolemManager();
std::unordered_map<Node, Node, NodeHashFunction>::iterator it;
std::map<Node, Node> preReplace;
std::map<Node, Node>::iterator itr;
}
else
{
- ret = nm->mkSkolem("k", ut);
+ ret = sm->mkDummySkolem("k", ut);
}
// must get the ho apply to ensure extensionality is applied
Node hoa = getHoApplyUf(tn);
{
Assert(!childrent.empty());
TypeNode newFType = nm->mkFunctionType(childrent, cur.getType());
- retOp = nm->mkSkolem("rf", newFType);
+ retOp = sm->mkDummySkolem("rf", newFType);
d_visited_op[op] = retOp;
}
else
if (it == d_hoApplyUf.end())
{
NodeManager* nm = NodeManager::currentNM();
+ SkolemManager* sm = nm->getSkolemManager();
std::vector<TypeNode> hoTypeArgs;
hoTypeArgs.push_back(tnf);
hoTypeArgs.push_back(tna);
TypeNode tnh = nm->mkFunctionType(hoTypeArgs, tnr);
- Node k = NodeManager::currentNM()->mkSkolem("ho", tnh);
+ Node k = sm->mkDummySkolem("ho", tnh);
d_hoApplyUf[tnf] = k;
return k;
}
#include "expr/node.h"
#include "expr/node_traversal.h"
+#include "expr/skolem_manager.h"
#include "options/smt_options.h"
#include "preprocessing/assertion_pipeline.h"
#include "theory/rewriter.h"
AlwaysAssert(size > 0);
AlwaysAssert(!options::incrementalSolving());
+ NodeManager* nm = NodeManager::currentNM();
+ SkolemManager* sm = nm->getSkolemManager();
NodeMap binaryCache;
Node n_binary = intToBVMakeBinary(n, binaryCache);
for (TNode current : NodeDfsIterable(n_binary, VisitOrder::POSTORDER,
[&cache](TNode nn) { return cache.count(nn) > 0; }))
{
- NodeManager* nm = NodeManager::currentNM();
if (current.getNumChildren() > 0)
{
// Not a leaf
{
if (current.getType() == nm->integerType())
{
- result = nm->mkSkolem("__intToBV_var",
- nm->mkBitVectorType(size),
- "Variable introduced in intToBV pass");
+ result = sm->mkDummySkolem("__intToBV_var",
+ nm->mkBitVectorType(size),
+ "Variable introduced in intToBV pass");
}
}
else if (current.isConst())
#include <vector>
#include "expr/node_self_iterator.h"
+#include "expr/skolem_manager.h"
#include "options/arith_options.h"
#include "options/smt_options.h"
#include "preprocessing/assertion_pipeline.h"
SubstitutionMap& top_level_substs = tlsm.get();
NodeManager* nm = NodeManager::currentNM();
+ SkolemManager* sm = nm->getSkolemManager();
Node zero = nm->mkConst(Rational(0)), one = nm->mkConst(Rational(1));
Node trueNode = nm->mkConst(true);
{
stringstream ss;
ss << "mipvar_" << *ii;
- Node newVar = nm->mkSkolem(
+ Node newVar = sm->mkDummySkolem(
ss.str(),
nm->integerType(),
"a variable introduced due to scrubbing a miplib encoding",
#include "preprocessing/passes/nl_ext_purify.h"
+#include "expr/skolem_manager.h"
#include "preprocessing/assertion_pipeline.h"
#include "theory/rewriter.h"
std::vector<Node>& var_eq,
bool beneathMult)
{
+ NodeManager* nm = NodeManager::currentNM();
+ SkolemManager* sm = nm->getSkolemManager();
if (beneathMult)
{
NodeMap::iterator find = bcache.find(n);
else
{
// new variable
- ret = NodeManager::currentNM()->mkSkolem(
- "__purifyNl_var",
- n.getType(),
- "Variable introduced in purifyNl pass");
+ ret = sm->mkDummySkolem("__purifyNl_var",
+ n.getType(),
+ "Variable introduced in purifyNl pass");
Node np = purifyNlTerms(n, cache, bcache, var_eq, false);
var_eq.push_back(np.eqNode(ret));
Trace("nl-ext-purify") << "Purify : " << ret << " -> " << np
}
if (childChanged)
{
- ret = NodeManager::currentNM()->mkNode(n.getKind(), children);
+ ret = nm->mkNode(n.getKind(), children);
}
}
}
#include <vector>
+#include "expr/skolem_manager.h"
#include "options/quantifiers_options.h"
#include "options/smt_options.h"
#include "preprocessing/assertion_pipeline.h"
bool QuantifierMacros::process( Node n, bool pol, std::vector< Node >& args, Node f ){
Trace("macros-debug") << " process " << n << std::endl;
+ NodeManager* nm = NodeManager::currentNM();
+ SkolemManager* sm = nm->getSkolemManager();
if( n.getKind()==NOT ){
return process( n[0], !pol, args, f );
}else if( n.getKind()==AND || n.getKind()==OR ){
if( isBoundVarApplyUf( n ) ){
Node op = n.getOperator();
if( d_macro_defs.find( op )==d_macro_defs.end() ){
- Node n_def = NodeManager::currentNM()->mkConst( pol );
+ Node n_def = nm->mkConst(pol);
for( unsigned i=0; i<n.getNumChildren(); i++ ){
std::stringstream ss;
ss << "mda_" << op << "";
- Node v = NodeManager::currentNM()->mkSkolem( ss.str(), n[i].getType(), "created during macro definition recognition" );
+ Node v =
+ sm->mkDummySkolem(ss.str(),
+ n[i].getType(),
+ "created during macro definition recognition");
d_macro_basis[op].push_back( v );
}
//contains no ops
for( size_t a=0; a<m.getNumChildren(); a++ ){
std::stringstream ss;
ss << "mda_" << op << "";
- Node v = NodeManager::currentNM()->mkSkolem( ss.str(), m[a].getType(), "created during macro definition recognition" );
+ Node v = sm->mkDummySkolem(
+ ss.str(),
+ m[a].getType(),
+ "created during macro definition recognition");
d_macro_basis[op].push_back( v );
}
}
#include <string>
+#include "expr/skolem_manager.h"
#include "preprocessing/assertion_pipeline.h"
#include "preprocessing/preprocessing_pass_context.h"
#include "theory/arith/arith_msum.h"
else
{
NodeManager* nm = NodeManager::currentNM();
+ SkolemManager* sm = nm->getSkolemManager();
Node ret = n;
if (n.getNumChildren() > 0)
{
}
else if (n.isVar())
{
- ret = nm->mkSkolem("__realToIntInternal_var",
- nm->integerType(),
- "Variable introduced in realToIntInternal pass");
+ ret = sm->mkDummySkolem(
+ "__realToIntInternal_var",
+ nm->integerType(),
+ "Variable introduced in realToIntInternal pass");
var_eq.push_back(n.eqNode(ret));
// ensure that the original variable is defined to be the returned
// one, which is important for models and for incremental solving.
#include <vector>
#include "expr/node.h"
+#include "expr/skolem_manager.h"
#include "preprocessing/assertion_pipeline.h"
#include "theory/quantifiers/quant_util.h"
#include "theory/rewriter.h"
std::map<Node, Node>::iterator it = visited[pol].find(n);
if (it == visited[pol].end())
{
+ NodeManager* nm = NodeManager::currentNM();
+ SkolemManager* sm = nm->getSkolemManager();
Trace("sep-preprocess") << "Pre-skolem emp " << n << " with pol " << pol
<< std::endl;
Node ret = n;
{
TypeNode tnx = n[0].getType();
TypeNode tny = n[1].getType();
- Node x = NodeManager::currentNM()->mkSkolem(
- "ex", tnx, "skolem location for negated emp");
- Node y = NodeManager::currentNM()->mkSkolem(
- "ey", tny, "skolem data for negated emp");
- return NodeManager::currentNM()
+ Node x =
+ sm->mkDummySkolem("ex", tnx, "skolem location for negated emp");
+ Node y = sm->mkDummySkolem("ey", tny, "skolem data for negated emp");
+ return nm
->mkNode(kind::SEP_STAR,
- NodeManager::currentNM()->mkNode(kind::SEP_PTO, x, y),
- NodeManager::currentNM()->mkConst(true))
+ nm->mkNode(kind::SEP_PTO, x, y),
+ nm->mkConst(true))
.negate();
}
}
}
if (childChanged)
{
- return NodeManager::currentNM()->mkNode(n.getKind(), children);
+ return nm->mkNode(n.getKind(), children);
}
}
visited[pol][n] = ret;
#include "preprocessing/passes/unconstrained_simplifier.h"
#include "expr/dtype.h"
+#include "expr/skolem_manager.h"
#include "preprocessing/assertion_pipeline.h"
#include "preprocessing/preprocessing_pass_context.h"
#include "smt/logic_exception.h"
Node UnconstrainedSimplifier::newUnconstrainedVar(TypeNode t, TNode var)
{
- Node n = NodeManager::currentNM()->mkSkolem(
+ SkolemManager* sm = NodeManager::currentNM()->getSkolemManager();
+ Node n = sm->mkDummySkolem(
"unconstrained",
t,
"a new var introduced because of unconstrained variable "
#include <utility>
+#include "expr/skolem_manager.h"
#include "preprocessing/assertion_pipeline.h"
#include "preprocessing/passes/rewrite.h"
#include "smt/smt_statistics_registry.h"
else
{
NodeManager* nm = NodeManager::currentNM();
- Node skolem = nm->mkSkolem("compress", nm->booleanType());
+ SkolemManager* sm = nm->getSkolemManager();
+ Node skolem = sm->mkDummySkolem("compress", nm->booleanType());
d_compressed[rewritten] = skolem;
d_compressed[original] = skolem;
d_compressed[compressed] = skolem;
{
return (*it).second;
}
- else
- {
- Node var = NodeManager::currentNM()->mkSkolem(
- "iteSimp", t, "is a variable resulting from ITE simplification");
- d_simpVars[t] = var;
- return var;
- }
+ SkolemManager* sm = NodeManager::currentNM()->getSkolemManager();
+ Node var = sm->mkDummySkolem(
+ "iteSimp", t, "is a variable resulting from ITE simplification");
+ d_simpVars[t] = var;
+ return var;
}
Node ITESimplifier::createSimpContext(TNode c, Node& iteNode, Node& simpVar)
"Expecting a quantified formula as argument to get-qe.");
}
NodeManager* nm = NodeManager::currentNM();
+ SkolemManager* sm = nm->getSkolemManager();
// ensure the body is rewritten
q = nm->mkNode(q.getKind(), q[0], Rewriter::rewrite(q[1]));
// do nested quantifier elimination if necessary
<< q << std::endl;
// tag the quantified formula with the quant-elim attribute
TypeNode t = nm->booleanType();
- Node n_attr = nm->mkSkolem("qe", t, "Auxiliary variable for qe attr.");
+ Node n_attr = sm->mkDummySkolem("qe", t, "Auxiliary variable for qe attr.");
std::vector<Node> node_values;
TheoryEngine* te = d_smtSolver.getTheoryEngine();
Assert(te != nullptr);
#include <sstream>
#include "expr/dtype.h"
+#include "expr/skolem_manager.h"
#include "options/quantifiers_options.h"
#include "options/smt_options.h"
#include "printer/printer.h"
void SygusSolver::checkSynthSolution(Assertions& as)
{
NodeManager* nm = NodeManager::currentNM();
+ SkolemManager* sm = nm->getSkolemManager();
Notice() << "SygusSolver::checkSynthSolution(): checking synthesis solution"
<< std::endl;
std::map<Node, std::map<Node, Node>> sol_map;
vars.push_back(conj[1][0][j]);
std::stringstream ss;
ss << "sk_" << j;
- skos.push_back(nm->mkSkolem(ss.str(), conj[1][0][j].getType()));
+ skos.push_back(sm->mkDummySkolem(ss.str(), conj[1][0][j].getType()));
Trace("check-synth-sol") << "\tSkolemizing " << conj[1][0][j] << " to "
<< skos.back() << "\n";
}
#include <ostream>
#include "base/output.h"
+#include "expr/skolem_manager.h"
#include "options/smt_options.h"
#include "preprocessing/util/ite_utilities.h"
#include "theory/arith/arith_utilities.h"
// a: (sel = otherL) or (sel = otherR), otherL-otherR = c
NodeManager* nm = NodeManager::currentNM();
+ SkolemManager* sm = nm->getSkolemManager();
Node cnd = findIteCnd(binor[0], binor[1]);
- Node sk = nm->mkSkolem("deor", nm->booleanType());
+ Node sk = sm->mkDummySkolem("deor", nm->booleanType());
Node ite = sk.iteNode(otherL, otherR);
d_skolems.insert(sk, cnd);
addSubstitution(sel, ite);
return NodeManager::currentNM()->mkConst<bool>(b);
}
-inline Node mkIntSkolem(const std::string& name){
- return NodeManager::currentNM()->mkSkolem(name, NodeManager::currentNM()->integerType());
-}
-
-inline Node mkRealSkolem(const std::string& name){
- return NodeManager::currentNM()->mkSkolem(name, NodeManager::currentNM()->realType());
-}
-
-inline Node skolemFunction(const std::string& name, TypeNode dom, TypeNode range){
- NodeManager* currNM = NodeManager::currentNM();
- TypeNode functionType = currNM->mkFunctionType(dom, range);
- return currNM->mkSkolem(name, functionType);
-}
-
/** \f$ k \in {LT, LEQ, EQ, GEQ, GT} \f$ */
inline bool isRelationOperator(Kind k){
using namespace kind;
#include "theory/arith/callbacks.h"
#include "expr/proof_node.h"
+#include "expr/skolem_manager.h"
#include "theory/arith/proof_macros.h"
#include "theory/arith/theory_arith_private.h"
: d_ta(ta)
{}
ArithVar TempVarMalloc::request(){
- Node skolem = mkRealSkolem("tmpVar");
+ NodeManager* nm = NodeManager::currentNM();
+ SkolemManager* sm = nm->getSkolemManager();
+ Node skolem = sm->mkDummySkolem("tmpVar", nm->realType());
return d_ta.requestArithVar(skolem, false, true);
}
void TempVarMalloc::release(ArithVar v){
#include <iostream>
#include "base/output.h"
+#include "expr/skolem_manager.h"
#include "options/arith_options.h"
#include "smt/smt_statistics_registry.h"
#include "theory/arith/partial_model.h"
namespace arith {
inline Node makeIntegerVariable(){
- NodeManager* curr = NodeManager::currentNM();
- return curr->mkSkolem("intvar", curr->integerType(), "is an integer variable created by the dio solver");
+ NodeManager* nm = NodeManager::currentNM();
+ SkolemManager* sm = nm->getSkolemManager();
+ return sm->mkDummySkolem("intvar",
+ nm->integerType(),
+ "is an integer variable created by the dio solver");
}
DioSolver::DioSolver(context::Context* ctxt)
#include "theory/arith/nl/cad_solver.h"
-#include "theory/inference_id.h"
+#include "expr/skolem_manager.h"
#include "theory/arith/inference_manager.h"
#include "theory/arith/nl/cad/cdcac.h"
#include "theory/arith/nl/nl_model.h"
#include "theory/arith/nl/poly_conversion.h"
+#include "theory/inference_id.h"
namespace cvc5 {
namespace theory {
d_im(im),
d_model(model)
{
- d_ranVariable =
- NodeManager::currentNM()->mkSkolem("__z",
- NodeManager::currentNM()->realType(),
- "",
- NodeManager::SKOLEM_EXACT_NAME);
+ NodeManager* nm = NodeManager::currentNM();
+ SkolemManager* sm = nm->getSkolemManager();
+ d_ranVariable = sm->mkDummySkolem(
+ "__z", nm->realType(), "", NodeManager::SKOLEM_EXACT_NAME);
#ifdef CVC4_POLY_IMP
ProofChecker* pc = pnm != nullptr ? pnm->getChecker() : nullptr;
if (pc != nullptr)
#include "expr/node_algorithm.h"
#include "expr/node_builder.h"
#include "expr/proof.h"
+#include "expr/skolem_manager.h"
#include "options/arith_options.h"
#include "theory/arith/arith_msum.h"
#include "theory/arith/arith_utilities.h"
void SineSolver::doPhaseShift(TNode a, TNode new_a, TNode y)
{
NodeManager* nm = NodeManager::currentNM();
+ SkolemManager* sm = nm->getSkolemManager();
Assert(a.getKind() == Kind::SINE);
Trace("nl-ext-tf") << "Basis sine : " << new_a << " for " << a << std::endl;
Assert(!d_data->d_pi.isNull());
- Node shift = nm->mkSkolem("s", nm->integerType(), "number of shifts");
+ Node shift = sm->mkDummySkolem("s", nm->integerType(), "number of shifts");
// TODO (cvc4-projects #47) : do not introduce shift here, instead needs model-based
// refinement for constant shifts (cvc4-projects #1284)
Node lem = nm->mkNode(
#include "expr/node_algorithm.h"
#include "expr/node_builder.h"
+#include "expr/skolem_manager.h"
#include "options/arith_options.h"
#include "theory/arith/arith_msum.h"
#include "theory/arith/arith_utilities.h"
}
NodeManager* nm = NodeManager::currentNM();
+ SkolemManager* sm = nm->getSkolemManager();
for (const Node& a : needsMaster)
{
// should not have processed this already
Assert(d_tstate.d_trMaster.find(a) == d_tstate.d_trMaster.end());
Kind k = a.getKind();
Assert(k == Kind::SINE || k == Kind::EXPONENTIAL);
- Node y =
- nm->mkSkolem("y", nm->realType(), "phase shifted trigonometric arg");
+ Node y = sm->mkDummySkolem(
+ "y", nm->realType(), "phase shifted trigonometric arg");
Node new_a = nm->mkNode(k, y);
d_tstate.d_trSlaves[new_a].insert(new_a);
d_tstate.d_trSlaves[new_a].insert(a);
setToMin(secDir * dm.sgn(), bestSecDiff, tmp);
}
break;
- case inferbounds::Simplex:
- {
- // primDir * diffm * diff < c or primDir * diffm * diff > c
- tmp = entailmentCheckSimplex(primDir * dm.sgn(), dp, ibalg, out.getSimplexSideEffects());
- setToMin(primDir * dm.sgn(), bestPrimDiff, tmp);
-
- tmp = entailmentCheckSimplex(secDir * dm.sgn(), dp, ibalg, out.getSimplexSideEffects());
- setToMin(secDir * dm.sgn(), bestSecDiff, tmp);
- }
- break;
default:
Unhandled();
}
tmp.first = nb;
}
-std::pair<Node, DeltaRational> TheoryArithPrivate::entailmentCheckSimplex(int sgn, TNode tp, const inferbounds::InferBoundAlgorithm& param, InferBoundsResult& result){
-
- if((sgn == 0) || !(d_qflraStatus == Result::SAT && d_errorSet.noSignals()) || tp.getKind() == CONST_RATIONAL){
- return make_pair(Node::null(), DeltaRational());
- }
-
- Assert(d_qflraStatus == Result::SAT);
- Assert(d_errorSet.noSignals());
- Assert(param.getAlgorithm() == inferbounds::Simplex);
-
- // TODO Move me into a new file
-
- enum ResultState {Unset, Inferred, NoBound, ReachedThreshold, ExhaustedRounds};
- ResultState finalState = Unset;
-
- const int maxRounds =
- param.getSimplexRounds().just() ? param.getSimplexRounds().value() : -1;
-
- Maybe<DeltaRational> threshold;
- // TODO: get this from the parameters
-
- // setup term
- Polynomial p = Polynomial::parsePolynomial(tp);
- vector<ArithVar> variables;
- vector<Rational> coefficients;
- asVectors(p, coefficients, variables);
- if(sgn < 0){
- for(size_t i=0, N=coefficients.size(); i < N; ++i){
- coefficients[i] = -coefficients[i];
- }
- }
- // implicitly an upperbound
- Node skolem = mkRealSkolem("tmpVar$$");
- ArithVar optVar = requestArithVar(skolem, false, true);
- d_tableau.addRow(optVar, coefficients, variables);
- RowIndex ridx = d_tableau.basicToRowIndex(optVar);
-
- DeltaRational newAssignment = d_linEq.computeRowValue(optVar, false);
- d_partialModel.setAssignment(optVar, newAssignment);
- d_linEq.trackRowIndex(d_tableau.basicToRowIndex(optVar));
-
- // Setup simplex
- d_partialModel.stopQueueingBoundCounts();
- UpdateTrackingCallback utcb(&d_linEq);
- d_partialModel.processBoundsQueue(utcb);
- d_linEq.startTrackingBoundCounts();
-
- // maximize optVar via primal Simplex
- int rounds = 0;
- while(finalState == Unset){
- ++rounds;
- if(maxRounds >= 0 && rounds > maxRounds){
- finalState = ExhaustedRounds;
- break;
- }
-
- // select entering by bland's rule
- // TODO improve upon bland's
- ArithVar entering = ARITHVAR_SENTINEL;
- const Tableau::Entry* enteringEntry = NULL;
- for(Tableau::RowIterator ri = d_tableau.ridRowIterator(ridx); !ri.atEnd(); ++ri){
- const Tableau::Entry& entry = *ri;
- ArithVar v = entry.getColVar();
- if(v != optVar){
- int sgn1 = entry.getCoefficient().sgn();
- Assert(sgn1 != 0);
- bool candidate = (sgn1 > 0)
- ? (d_partialModel.cmpAssignmentUpperBound(v) != 0)
- : (d_partialModel.cmpAssignmentLowerBound(v) != 0);
- if(candidate && (entering == ARITHVAR_SENTINEL || entering > v)){
- entering = v;
- enteringEntry = &entry;
- }
- }
- }
- if(entering == ARITHVAR_SENTINEL){
- finalState = Inferred;
- break;
- }
- Assert(entering != ARITHVAR_SENTINEL);
- Assert(enteringEntry != NULL);
-
- int esgn = enteringEntry->getCoefficient().sgn();
- Assert(esgn != 0);
-
- // select leaving and ratio
- ArithVar leaving = ARITHVAR_SENTINEL;
- DeltaRational minRatio;
- const Tableau::Entry* pivotEntry = NULL;
-
- // Special case check the upper/lowerbound on entering
- ConstraintP cOnEntering = (esgn > 0)
- ? d_partialModel.getUpperBoundConstraint(entering)
- : d_partialModel.getLowerBoundConstraint(entering);
- if(cOnEntering != NullConstraint){
- leaving = entering;
- minRatio = d_partialModel.getAssignment(entering) - cOnEntering->getValue();
- }
- for(Tableau::ColIterator ci = d_tableau.colIterator(entering); !ci.atEnd(); ++ci){
- const Tableau::Entry& centry = *ci;
- ArithVar basic = d_tableau.rowIndexToBasic(centry.getRowIndex());
- int csgn = centry.getCoefficient().sgn();
- int basicDir = csgn * esgn;
-
- ConstraintP bound = (basicDir > 0)
- ? d_partialModel.getUpperBoundConstraint(basic)
- : d_partialModel.getLowerBoundConstraint(basic);
- if(bound != NullConstraint){
- DeltaRational diff = d_partialModel.getAssignment(basic) - bound->getValue();
- DeltaRational ratio = diff/(centry.getCoefficient());
- bool selected = false;
- if(leaving == ARITHVAR_SENTINEL){
- selected = true;
- }else{
- int cmp = ratio.compare(minRatio);
- if((csgn > 0) ? (cmp <= 0) : (cmp >= 0)){
- selected = (cmp != 0) ||
- ((leaving != entering) && (basic < leaving));
- }
- }
- if(selected){
- leaving = basic;
- minRatio = ratio;
- pivotEntry = ¢ry;
- }
- }
- }
-
-
- if(leaving == ARITHVAR_SENTINEL){
- finalState = NoBound;
- break;
- }else if(leaving == entering){
- d_linEq.update(entering, minRatio);
- }else{
- DeltaRational newLeaving = minRatio * (pivotEntry->getCoefficient());
- d_linEq.pivotAndUpdate(leaving, entering, newLeaving);
- // no conflicts clear signals
- Assert(d_errorSet.noSignals());
- }
-
- if(threshold.just()){
- if (d_partialModel.getAssignment(optVar) >= threshold.value())
- {
- finalState = ReachedThreshold;
- break;
- }
- }
- };
-
- result = InferBoundsResult(tp, sgn > 0);
-
- // tear down term
- switch(finalState){
- case Inferred:
- {
- NodeBuilder nb(kind::AND);
- for(Tableau::RowIterator ri = d_tableau.ridRowIterator(ridx); !ri.atEnd(); ++ri){
- const Tableau::Entry& e =*ri;
- ArithVar colVar = e.getColVar();
- if(colVar != optVar){
- const Rational& q = e.getCoefficient();
- Assert(q.sgn() != 0);
- ConstraintP c = (q.sgn() > 0)
- ? d_partialModel.getUpperBoundConstraint(colVar)
- : d_partialModel.getLowerBoundConstraint(colVar);
- c->externalExplainByAssertions(nb);
- }
- }
- Assert(nb.getNumChildren() >= 1);
- Node exp = (nb.getNumChildren() >= 2) ? (Node) nb : nb[0];
- result.setBound(d_partialModel.getAssignment(optVar), exp);
- result.setIsOptimal();
- break;
- }
- case NoBound:
- break;
- case ReachedThreshold:
- result.setReachedThreshold();
- break;
- case ExhaustedRounds:
- result.setBudgetExhausted();
- break;
- case Unset:
- default:
- Unreachable();
- break;
- };
-
- d_linEq.stopTrackingRowIndex(ridx);
- d_tableau.removeBasicRow(optVar);
- releaseArithVar(optVar);
-
- d_linEq.stopTrackingBoundCounts();
- d_partialModel.startQueueingBoundCounts();
-
- if(result.foundBound()){
- return make_pair(result.getExplanation(), result.getValue());
- }else{
- return make_pair(Node::null(), DeltaRational());
- }
-}
-
ArithProofRuleChecker* TheoryArithPrivate::getProofChecker()
{
return &d_checker;
}
-// InferBoundsResult TheoryArithPrivate::inferUpperBoundSimplex(TNode t, const
-// inferbounds::InferBoundAlgorithm& param){
-// Assert(param.findUpperBound());
-
-// if(!(d_qflraStatus == Result::SAT && d_errorSet.noSignals())){
-// InferBoundsResult inconsistent;
-// inconsistent.setInconsistent();
-// return inconsistent;
-// }
-
-// Assert(d_qflraStatus == Result::SAT);
-// Assert(d_errorSet.noSignals());
-
-// // TODO Move me into a new file
-
-// enum ResultState {Unset, Inferred, NoBound, ReachedThreshold, ExhaustedRounds};
-// ResultState finalState = Unset;
-
-// int maxRounds = 0;
-// switch(param.getParamKind()){
-// case InferBoundsParameters::Unbounded:
-// maxRounds = -1;
-// break;
-// case InferBoundsParameters::NumVars:
-// maxRounds = d_partialModel.getNumberOfVariables() * param.getSimplexRoundParameter();
-// break;
-// case InferBoundsParameters::Direct:
-// maxRounds = param.getSimplexRoundParameter();
-// break;
-// default: maxRounds = 0; break;
-// }
-
-// // setup term
-// Polynomial p = Polynomial::parsePolynomial(t);
-// vector<ArithVar> variables;
-// vector<Rational> coefficients;
-// asVectors(p, coefficients, variables);
-
-// Node skolem = mkRealSkolem("tmpVar$$");
-// ArithVar optVar = requestArithVar(skolem, false, true);
-// d_tableau.addRow(optVar, coefficients, variables);
-// RowIndex ridx = d_tableau.basicToRowIndex(optVar);
-
-// DeltaRational newAssignment = d_linEq.computeRowValue(optVar, false);
-// d_partialModel.setAssignment(optVar, newAssignment);
-// d_linEq.trackRowIndex(d_tableau.basicToRowIndex(optVar));
-
-// // Setup simplex
-// d_partialModel.stopQueueingBoundCounts();
-// UpdateTrackingCallback utcb(&d_linEq);
-// d_partialModel.processBoundsQueue(utcb);
-// d_linEq.startTrackingBoundCounts();
-
-// // maximize optVar via primal Simplex
-// int rounds = 0;
-// while(finalState == Unset){
-// ++rounds;
-// if(maxRounds >= 0 && rounds > maxRounds){
-// finalState = ExhaustedRounds;
-// break;
-// }
-
-// // select entering by bland's rule
-// // TODO improve upon bland's
-// ArithVar entering = ARITHVAR_SENTINEL;
-// const Tableau::Entry* enteringEntry = NULL;
-// for(Tableau::RowIterator ri = d_tableau.ridRowIterator(ridx);
-// !ri.atEnd(); ++ri){
-// const Tableau::Entry& entry = *ri;
-// ArithVar v = entry.getColVar();
-// if(v != optVar){
-// int sgn = entry.getCoefficient().sgn();
-// Assert(sgn != 0);
-// bool candidate = (sgn > 0)
-// ? (d_partialModel.cmpAssignmentUpperBound(v) != 0)
-// : (d_partialModel.cmpAssignmentLowerBound(v) != 0);
-// if(candidate && (entering == ARITHVAR_SENTINEL || entering > v)){
-// entering = v;
-// enteringEntry = &entry;
-// }
-// }
-// }
-// if(entering == ARITHVAR_SENTINEL){
-// finalState = Inferred;
-// break;
-// }
-// Assert(entering != ARITHVAR_SENTINEL);
-// Assert(enteringEntry != NULL);
-
-// int esgn = enteringEntry->getCoefficient().sgn();
-// Assert(esgn != 0);
-
-// // select leaving and ratio
-// ArithVar leaving = ARITHVAR_SENTINEL;
-// DeltaRational minRatio;
-// const Tableau::Entry* pivotEntry = NULL;
-
-// // Special case check the upper/lowerbound on entering
-// ConstraintP cOnEntering = (esgn > 0)
-// ? d_partialModel.getUpperBoundConstraint(entering)
-// : d_partialModel.getLowerBoundConstraint(entering);
-// if(cOnEntering != NullConstraint){
-// leaving = entering;
-// minRatio = d_partialModel.getAssignment(entering) - cOnEntering->getValue();
-// }
-// for(Tableau::ColIterator ci = d_tableau.colIterator(entering); !ci.atEnd(); ++ci){
-// const Tableau::Entry& centry = *ci;
-// ArithVar basic = d_tableau.rowIndexToBasic(centry.getRowIndex());
-// int csgn = centry.getCoefficient().sgn();
-// int basicDir = csgn * esgn;
-
-// ConstraintP bound = (basicDir > 0)
-// ? d_partialModel.getUpperBoundConstraint(basic)
-// : d_partialModel.getLowerBoundConstraint(basic);
-// if(bound != NullConstraint){
-// DeltaRational diff = d_partialModel.getAssignment(basic) - bound->getValue();
-// DeltaRational ratio = diff/(centry.getCoefficient());
-// bool selected = false;
-// if(leaving == ARITHVAR_SENTINEL){
-// selected = true;
-// }else{
-// int cmp = ratio.compare(minRatio);
-// if((csgn > 0) ? (cmp <= 0) : (cmp >= 0)){
-// selected = (cmp != 0) ||
-// ((leaving != entering) && (basic < leaving));
-// }
-// }
-// if(selected){
-// leaving = basic;
-// minRatio = ratio;
-// pivotEntry = ¢ry;
-// }
-// }
-// }
-
-// if(leaving == ARITHVAR_SENTINEL){
-// finalState = NoBound;
-// break;
-// }else if(leaving == entering){
-// d_linEq.update(entering, minRatio);
-// }else{
-// DeltaRational newLeaving = minRatio * (pivotEntry->getCoefficient());
-// d_linEq.pivotAndUpdate(leaving, entering, newLeaving);
-// // no conflicts clear signals
-// Assert(d_errorSet.noSignals());
-// }
-
-// if(param.useThreshold()){
-// if(d_partialModel.getAssignment(optVar) >= param.getThreshold()){
-// finalState = ReachedThreshold;
-// break;
-// }
-// }
-// };
-
-// InferBoundsResult result(t, param.findUpperBound());
-
-// // tear down term
-// switch(finalState){
-// case Inferred:
-// {
-// NodeBuilder nb(kind::AND);
-// for(Tableau::RowIterator ri = d_tableau.ridRowIterator(ridx);
-// !ri.atEnd(); ++ri){
-// const Tableau::Entry& e =*ri;
-// ArithVar colVar = e.getColVar();
-// if(colVar != optVar){
-// const Rational& q = e.getCoefficient();
-// Assert(q.sgn() != 0);
-// ConstraintP c = (q.sgn() > 0)
-// ? d_partialModel.getUpperBoundConstraint(colVar)
-// : d_partialModel.getLowerBoundConstraint(colVar);
-// c->externalExplainByAssertions(nb);
-// }
-// }
-// Assert(nb.getNumChildren() >= 1);
-// Node exp = (nb.getNumChildren() >= 2) ? (Node) nb : nb[0];
-// result.setBound(d_partialModel.getAssignment(optVar), exp);
-// result.setIsOptimal();
-// break;
-// }
-// case NoBound:
-// break;
-// case ReachedThreshold:
-// result.setReachedThreshold();
-// break;
-// case ExhaustedRounds:
-// result.setBudgetExhausted();
-// break;
-// case Unset:
-// default:
-// Unreachable();
-// break;
-// };
-
-// d_linEq.stopTrackingRowIndex(ridx);
-// d_tableau.removeBasicRow(optVar);
-// releaseArithVar(optVar);
-
-// d_linEq.stopTrackingBoundCounts();
-// d_partialModel.startQueueingBoundCounts();
-
-// return result;
-// }
-
} // namespace arith
} // namespace theory
} // namespace cvc5
void entailmentCheckBoundLookup(std::pair<Node, DeltaRational>& tmp, int sgn, TNode tp) const;
void entailmentCheckRowSum(std::pair<Node, DeltaRational>& tmp, int sgn, TNode tp) const;
- std::pair<Node, DeltaRational> entailmentCheckSimplex(int sgn, TNode tp, const inferbounds::InferBoundAlgorithm& p, InferBoundsResult& out);
-
- //InferBoundsResult inferBound(TNode term, const InferBoundsParameters& p);
- //InferBoundsResult inferUpperBoundLookup(TNode t, const InferBoundsParameters& p);
- //InferBoundsResult inferUpperBoundSimplex(TNode t, const SimplexInferBoundsParameters& p);
-
/**
* Infers either a new upper/lower bound on term in the real relaxation.
* Either:
#include "theory/builtin/theory_builtin_type_rules.h"
#include "expr/attribute.h"
+#include "expr/skolem_manager.h"
namespace cvc5 {
namespace theory {
{
return type.getAttribute(gta);
}
- Node k = NodeManager::currentNM()->mkSkolem(
+ SkolemManager* sm = NodeManager::currentNM()->getSkolemManager();
+ Node k = sm->mkDummySkolem(
"groundTerm", type, "a ground term created for type " + type.toString());
type.setAttribute(gta, k);
return k;
**/
#include "theory/bv/abstraction.h"
+#include "expr/skolem_manager.h"
#include "options/bv_options.h"
#include "printer/printer.h"
#include "smt/dump.h"
{
Assert(node.getMetaKind() == kind::metakind::VARIABLE);
NodeManager* nm = NodeManager::currentNM();
+ SkolemManager* sm = nm->getSkolemManager();
unsigned bitwidth = utils::getSize(node);
if (d_signatureSkolems.find(bitwidth) == d_signatureSkolems.end())
{
{
ostringstream os;
os << "sig_" << bitwidth << "_" << index;
- skolems.push_back(nm->mkSkolem(os.str(),
- nm->mkBitVectorType(bitwidth),
- "skolem for computing signatures"));
+ skolems.push_back(sm->mkDummySkolem(os.str(),
+ nm->mkBitVectorType(bitwidth),
+ "skolem for computing signatures"));
}
++(d_signatureIndices[bitwidth]);
return skolems[index];
void AbstractionModule::finalizeSignatures()
{
NodeManager* nm = NodeManager::currentNM();
+ SkolemManager* sm = nm->getSkolemManager();
Debug("bv-abstraction")
<< "AbstractionModule::finalizeSignatures num signatures = "
<< d_signatures.size() << "\n";
TypeNode range = nm->mkBitVectorType(1);
TypeNode abs_type = nm->mkFunctionType(arg_types, range);
- Node abs_func =
- nm->mkSkolem("abs_$$", abs_type, "abstraction function for bv theory");
+ Node abs_func = sm->mkDummySkolem(
+ "abs_$$", abs_type, "abstraction function for bv theory");
Debug("bv-abstraction") << " abstracted by function " << abs_func << "\n";
// NOTE: signature expression type is BOOLEAN
#include "theory/bv/bv_subtheory_core.h"
+#include "expr/skolem_manager.h"
#include "options/bv_options.h"
#include "options/smt_options.h"
#include "smt/smt_statistics_registry.h"
bool CoreSolver::doExtfInferences(std::vector<Node>& terms)
{
NodeManager* nm = NodeManager::currentNM();
+ SkolemManager* sm = nm->getSkolemManager();
bool sentLemma = false;
eq::EqualityEngine* ee = d_equalityEngine;
std::map<Node, Node> op_map;
// congruent modulo 2^( bv width )
unsigned bvs = n.getType().getBitVectorSize();
Node coeff = nm->mkConst(Rational(Integer(1).multiplyByPow2(bvs)));
- Node k = nm->mkSkolem(
+ Node k = sm->mkDummySkolem(
"int_bv_cong", t.getType(), "for int2bv/bv2nat congruence");
t = nm->mkNode(kind::PLUS, t, nm->mkNode(kind::MULT, coeff, k));
}
#include <vector>
+#include "expr/skolem_manager.h"
#include "options/theory_options.h"
#include "theory/theory.h"
Node mkVar(unsigned size)
{
NodeManager* nm = NodeManager::currentNM();
-
- return nm->mkSkolem("BVSKOLEM$$",
- nm->mkBitVectorType(size),
- "is a variable created by the theory of bitvectors");
+ SkolemManager* sm = nm->getSkolemManager();
+ return sm->mkDummySkolem("BVSKOLEM$$",
+ nm->mkBitVectorType(size),
+ "is a variable created by the theory of bitvectors");
}
/* ------------------------------------------------------------------------- */
#include "expr/dtype.h"
#include "expr/dtype_cons.h"
#include "expr/node_manager.h"
+#include "expr/skolem_manager.h"
#include "expr/sygus_datatype.h"
#include "options/base_options.h"
#include "options/datatypes_options.h"
return itt->second;
}
NodeManager* nm = NodeManager::currentNM();
+ SkolemManager* sm = nm->getSkolemManager();
std::vector<TypeNode> types;
types.push_back(tn);
TypeNode ptn = nm->mkPredicateType(types);
- Node pred = nm->mkSkolem(isPre ? "pre" : "post", ptn);
+ Node pred = sm->mkDummySkolem(isPre ? "pre" : "post", ptn);
d_traversal_pred[index][tn][n] = pred;
return pred;
}
Node SygusExtension::eliminateTraversalPredicates(Node n)
{
NodeManager* nm = NodeManager::currentNM();
+ SkolemManager* sm = nm->getSkolemManager();
std::unordered_map<TNode, Node, TNodeHashFunction> visited;
std::unordered_map<TNode, Node, TNodeHashFunction>::iterator it;
std::map<Node, Node>::iterator ittb;
{
std::stringstream ss;
ss << "v_" << cur;
- ret = nm->mkSkolem(ss.str(), cur.getType());
+ ret = sm->mkDummySkolem(ss.str(), cur.getType());
d_traversal_bool[cur] = ret;
}
else
slem = nm->mkNode(LEQ, ds, d_szinfo[m]->getOrMkMeasureValue());
}else{
Node mt = d_szinfo[m]->getOrMkActiveMeasureValue();
- Node new_mt = d_szinfo[m]->getOrMkActiveMeasureValue(true);
+ Node newMt = d_szinfo[m]->getOrMkActiveMeasureValue(true);
Node ds = nm->mkNode(DT_SIZE, e);
- slem = mt.eqNode(nm->mkNode(PLUS, new_mt, ds));
+ slem = mt.eqNode(nm->mkNode(PLUS, newMt, ds));
}
Trace("sygus-sb") << "...size lemma : " << slem << std::endl;
d_im.lemma(slem, InferenceId::DATATYPES_SYGUS_MT_BOUND);
if (d_measure_value.isNull())
{
NodeManager* nm = NodeManager::currentNM();
- d_measure_value = nm->mkSkolem("mt", nm->integerType());
+ SkolemManager* sm = nm->getSkolemManager();
+ d_measure_value = sm->mkDummySkolem("mt", nm->integerType());
Node mtlem =
nm->mkNode(kind::GEQ, d_measure_value, nm->mkConst(Rational(0)));
d_im.lemma(mtlem, InferenceId::DATATYPES_SYGUS_MT_POS);
if (mkNew)
{
NodeManager* nm = NodeManager::currentNM();
- Node new_mt = nm->mkSkolem("mt", nm->integerType());
+ SkolemManager* sm = nm->getSkolemManager();
+ Node new_mt = sm->mkDummySkolem("mt", nm->integerType());
Node mtlem = nm->mkNode(kind::GEQ, new_mt, nm->mkConst(Rational(0)));
d_measure_value_active = new_mt;
d_im.lemma(mtlem, InferenceId::DATATYPES_SYGUS_MT_POS);
#include "expr/dtype_cons.h"
#include "expr/kind.h"
#include "expr/proof_node_manager.h"
+#include "expr/skolem_manager.h"
#include "options/datatypes_options.h"
#include "options/quantifiers_options.h"
#include "options/smt_options.h"
void TheoryDatatypes::mkExpDefSkolem( Node sel, TypeNode dt, TypeNode rt ) {
if( d_exp_def_skolem[dt].find( sel )==d_exp_def_skolem[dt].end() ){
+ NodeManager* nm = NodeManager::currentNM();
+ SkolemManager* sm = nm->getSkolemManager();
std::stringstream ss;
ss << sel << "_uf";
- d_exp_def_skolem[dt][ sel ] = NodeManager::currentNM()->mkSkolem( ss.str().c_str(),
- NodeManager::currentNM()->mkFunctionType( dt, rt ) );
+ d_exp_def_skolem[dt][sel] =
+ sm->mkDummySkolem(ss.str().c_str(), nm->mkFunctionType(dt, rt));
}
}
if( n.getKind()==APPLY_CONSTRUCTOR ){
NodeMap::const_iterator it = d_term_sk.find( n );
if( it==d_term_sk.end() ){
+ NodeManager* nm = NodeManager::currentNM();
+ SkolemManager* sm = nm->getSkolemManager();
//add purification unit lemma ( k = n )
- Node k = NodeManager::currentNM()->mkSkolem( "k", n.getType(), "reference skolem for datatypes" );
+ Node k =
+ sm->mkDummySkolem("k", n.getType(), "reference skolem for datatypes");
d_term_sk[n] = k;
Node eq = k.eqNode( n );
Trace("datatypes-infer") << "DtInfer : ref : " << eq << std::endl;
}
Node TheoryDatatypes::getSingletonLemma( TypeNode tn, bool pol ) {
+ NodeManager* nm = NodeManager::currentNM();
+ SkolemManager* sm = nm->getSkolemManager();
int index = pol ? 0 : 1;
std::map< TypeNode, Node >::iterator it = d_singleton_lemma[index].find( tn );
if( it==d_singleton_lemma[index].end() ){
Node a;
if( pol ){
- Node v1 = NodeManager::currentNM()->mkBoundVar( tn );
- Node v2 = NodeManager::currentNM()->mkBoundVar( tn );
- a = NodeManager::currentNM()->mkNode( FORALL, NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, v1, v2 ), v1.eqNode( v2 ) );
+ Node v1 = nm->mkBoundVar(tn);
+ Node v2 = nm->mkBoundVar(tn);
+ a = nm->mkNode(FORALL, nm->mkNode(BOUND_VAR_LIST, v1, v2), v1.eqNode(v2));
}else{
- Node v1 = NodeManager::currentNM()->mkSkolem( "k1", tn );
- Node v2 = NodeManager::currentNM()->mkSkolem( "k2", tn );
+ Node v1 = sm->mkDummySkolem("k1", tn);
+ Node v2 = sm->mkDummySkolem("k2", tn);
a = v1.eqNode( v2 ).negate();
//send out immediately as lemma
d_im.lemma(a, InferenceId::DATATYPES_REC_SINGLETON_FORCE_DEQ);
#include "theory/engine_output_channel.h"
+#include "expr/skolem_manager.h"
#include "prop/prop_engine.h"
#include "smt/smt_statistics_registry.h"
#include "theory/theory_engine.h"
void EngineOutputChannel::demandRestart()
{
- NodeManager* curr = NodeManager::currentNM();
- Node restartVar = curr->mkSkolem(
+ NodeManager* nm = NodeManager::currentNM();
+ SkolemManager* sm = nm->getSkolemManager();
+ Node restartVar = sm->mkDummySkolem(
"restartVar",
- curr->booleanType(),
+ nm->booleanType(),
"A boolean variable asserted to be true to force a restart");
Trace("theory::restart") << "EngineOutputChannel<" << d_theory
<< ">::restart(" << restartVar << ")" << std::endl;
#include <vector>
#include "base/configuration.h"
+#include "expr/skolem_manager.h"
#include "options/fp_options.h"
#include "smt/logic_exception.h"
#include "theory/fp/fp_converter.h"
Assert(t.getKind() == kind::FLOATINGPOINT_TYPE);
NodeManager *nm = NodeManager::currentNM();
+ SkolemManager* sm = nm->getSkolemManager();
ComparisonUFMap::const_iterator i(d_minMap.find(t));
Node fun;
std::vector<TypeNode> args(2);
args[0] = t;
args[1] = t;
- fun = nm->mkSkolem("floatingpoint_min_zero_case",
- nm->mkFunctionType(args,
+ fun = sm->mkDummySkolem("floatingpoint_min_zero_case",
+ nm->mkFunctionType(args,
#ifdef SYMFPUPROPISBOOL
- nm->booleanType()
+ nm->booleanType()
#else
- nm->mkBitVectorType(1U)
+ nm->mkBitVectorType(1U)
#endif
- ),
- "floatingpoint_min_zero_case",
- NodeManager::SKOLEM_EXACT_NAME);
+ ),
+ "floatingpoint_min_zero_case",
+ NodeManager::SKOLEM_EXACT_NAME);
d_minMap.insert(t, fun);
} else {
fun = (*i).second;
Assert(t.getKind() == kind::FLOATINGPOINT_TYPE);
NodeManager *nm = NodeManager::currentNM();
+ SkolemManager* sm = nm->getSkolemManager();
ComparisonUFMap::const_iterator i(d_maxMap.find(t));
Node fun;
std::vector<TypeNode> args(2);
args[0] = t;
args[1] = t;
- fun = nm->mkSkolem("floatingpoint_max_zero_case",
- nm->mkFunctionType(args,
+ fun = sm->mkDummySkolem("floatingpoint_max_zero_case",
+ nm->mkFunctionType(args,
#ifdef SYMFPUPROPISBOOL
- nm->booleanType()
+ nm->booleanType()
#else
- nm->mkBitVectorType(1U)
+ nm->mkBitVectorType(1U)
#endif
- ),
- "floatingpoint_max_zero_case",
- NodeManager::SKOLEM_EXACT_NAME);
+ ),
+ "floatingpoint_max_zero_case",
+ NodeManager::SKOLEM_EXACT_NAME);
d_maxMap.insert(t, fun);
} else {
fun = (*i).second;
std::pair<TypeNode, TypeNode> p(source, target);
NodeManager *nm = NodeManager::currentNM();
+ SkolemManager* sm = nm->getSkolemManager();
ConversionUFMap::const_iterator i(d_toUBVMap.find(p));
Node fun;
std::vector<TypeNode> args(2);
args[0] = nm->roundingModeType();
args[1] = source;
- fun = nm->mkSkolem("floatingpoint_to_ubv_out_of_range_case",
- nm->mkFunctionType(args, target),
- "floatingpoint_to_ubv_out_of_range_case",
- NodeManager::SKOLEM_EXACT_NAME);
+ 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);
d_toUBVMap.insert(p, fun);
} else {
fun = (*i).second;
std::pair<TypeNode, TypeNode> p(source, target);
NodeManager *nm = NodeManager::currentNM();
+ SkolemManager* sm = nm->getSkolemManager();
ConversionUFMap::const_iterator i(d_toSBVMap.find(p));
Node fun;
std::vector<TypeNode> args(2);
args[0] = nm->roundingModeType();
args[1] = source;
- fun = nm->mkSkolem("floatingpoint_to_sbv_out_of_range_case",
- nm->mkFunctionType(args, target),
- "floatingpoint_to_sbv_out_of_range_case",
- NodeManager::SKOLEM_EXACT_NAME);
+ 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);
d_toSBVMap.insert(p, fun);
} else {
fun = (*i).second;
Assert(t.getKind() == kind::FLOATINGPOINT_TYPE);
NodeManager *nm = NodeManager::currentNM();
+ SkolemManager* sm = nm->getSkolemManager();
ComparisonUFMap::const_iterator i(d_toRealMap.find(t));
Node fun;
if (i == d_toRealMap.end()) {
std::vector<TypeNode> args(1);
args[0] = t;
- fun = nm->mkSkolem("floatingpoint_to_real_infinity_and_NaN_case",
- nm->mkFunctionType(args, nm->realType()),
- "floatingpoint_to_real_infinity_and_NaN_case",
- NodeManager::SKOLEM_EXACT_NAME);
+ 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);
d_toRealMap.insert(t, fun);
} else {
fun = (*i).second;
Assert(t.getKind() == kind::FLOATINGPOINT_TYPE);
NodeManager *nm = NodeManager::currentNM();
+ SkolemManager* sm = nm->getSkolemManager();
ComparisonUFMap::const_iterator i(d_realToFloatMap.find(t));
Node fun;
std::vector<TypeNode> args(2);
args[0] = node[0].getType();
args[1] = node[1].getType();
- fun = nm->mkSkolem("floatingpoint_abstract_real_to_float",
- nm->mkFunctionType(args, node.getType()),
- "floatingpoint_abstract_real_to_float",
- NodeManager::SKOLEM_EXACT_NAME);
+ fun = sm->mkDummySkolem("floatingpoint_abstract_real_to_float",
+ nm->mkFunctionType(args, node.getType()),
+ "floatingpoint_abstract_real_to_float",
+ NodeManager::SKOLEM_EXACT_NAME);
d_realToFloatMap.insert(t, fun);
}
else
Assert(t.getKind() == kind::FLOATINGPOINT_TYPE);
NodeManager *nm = NodeManager::currentNM();
+ SkolemManager* sm = nm->getSkolemManager();
ComparisonUFMap::const_iterator i(d_floatToRealMap.find(t));
Node fun;
std::vector<TypeNode> args(2);
args[0] = t;
args[1] = nm->realType();
- fun = nm->mkSkolem("floatingpoint_abstract_float_to_real",
- nm->mkFunctionType(args, nm->realType()),
- "floatingpoint_abstract_float_to_real",
- NodeManager::SKOLEM_EXACT_NAME);
+ fun = sm->mkDummySkolem("floatingpoint_abstract_float_to_real",
+ nm->mkFunctionType(args, nm->realType()),
+ "floatingpoint_abstract_float_to_real",
+ NodeManager::SKOLEM_EXACT_NAME);
d_floatToRealMap.insert(t, fun);
}
else
#include <algorithm>
+#include "expr/skolem_manager.h"
#include "options/quantifiers_options.h"
#include "theory/bv/theory_bv_utils.h"
#include "theory/quantifiers/bv_inverter_utils.h"
std::map<TypeNode, Node>::iterator its = d_solve_var.find(tn);
if (its == d_solve_var.end())
{
- Node k = NodeManager::currentNM()->mkSkolem("slv", tn);
+ SkolemManager* sm = NodeManager::currentNM()->getSkolemManager();
+ Node k = sm->mkDummySkolem("slv", tn);
d_solve_var[tn] = k;
return k;
}
- else
- {
- return its->second;
- }
+ return its->second;
}
/*---------------------------------------------------------------------------*/
#include "theory/quantifiers/cegqi/ceg_bv_instantiator.h"
#include <stack>
+#include "expr/skolem_manager.h"
#include "options/quantifiers_options.h"
#include "theory/bv/theory_bv_utils.h"
#include "theory/quantifiers/cegqi/ceg_bv_instantiator_utils.h"
if (options::cegqiBvRmExtract())
{
NodeManager* nm = NodeManager::currentNM();
+ SkolemManager* sm = nm->getSkolemManager();
Trace("cegqi-bv-pp") << "-----remove extracts..." << std::endl;
// map from terms to bitvector extracts applied to that term
std::map<Node, std::vector<Node> > extract_map;
Node ex = bv::utils::mkExtract(
es.first, boundaries[i - 1] - 1, boundaries[i]);
Node var =
- nm->mkSkolem("ek",
- ex.getType(),
- "variable to represent disjoint extract region");
+ sm->mkDummySkolem("ek",
+ ex.getType(),
+ "variable to represent disjoint extract region");
children.push_back(var);
vars.push_back(var);
}
#include "theory/quantifiers/cegqi/inst_strategy_cegqi.h"
#include "expr/node_algorithm.h"
+#include "expr/skolem_manager.h"
#include "options/quantifiers_options.h"
#include "theory/quantifiers/first_order_model.h"
#include "theory/quantifiers/instantiate.h"
return it->second;
}
NodeManager * nm = NodeManager::currentNM();
- Node g = nm->mkSkolem("g", nm->booleanType());
+ SkolemManager* sm = nm->getSkolemManager();
+ Node g = sm->mkDummySkolem("g", nm->booleanType());
// ensure that it is a SAT literal
Node ceLit = d_qstate.getValuation().ensureLiteral(g);
d_ce_lit[q] = ceLit;
#include "theory/quantifiers/cegqi/vts_term_cache.h"
#include "expr/node_algorithm.h"
+#include "expr/skolem_manager.h"
#include "theory/arith/arith_msum.h"
#include "theory/quantifiers/quantifiers_inference_manager.h"
#include "theory/rewriter.h"
if (create)
{
NodeManager* nm = NodeManager::currentNM();
+ SkolemManager* sm = nm->getSkolemManager();
if (d_vts_delta_free.isNull())
{
d_vts_delta_free =
- nm->mkSkolem("delta_free",
- nm->realType(),
- "free delta for virtual term substitution");
+ sm->mkDummySkolem("delta_free",
+ nm->realType(),
+ "free delta for virtual term substitution");
Node delta_lem = nm->mkNode(GT, d_vts_delta_free, d_zero);
d_qim.lemma(delta_lem, InferenceId::QUANTIFIERS_CEGQI_VTS_LB_DELTA);
}
if (d_vts_delta.isNull())
{
- d_vts_delta = nm->mkSkolem(
+ d_vts_delta = sm->mkDummySkolem(
"delta", nm->realType(), "delta for virtual term substitution");
// mark as a virtual term
VirtualTermSkolemAttribute vtsa;
if (create)
{
NodeManager* nm = NodeManager::currentNM();
+ SkolemManager* sm = nm->getSkolemManager();
if (d_vts_inf_free[tn].isNull())
{
- d_vts_inf_free[tn] = nm->mkSkolem(
+ d_vts_inf_free[tn] = sm->mkDummySkolem(
"inf_free", tn, "free infinity for virtual term substitution");
}
if (d_vts_inf[tn].isNull())
{
- d_vts_inf[tn] =
- nm->mkSkolem("inf", tn, "infinity for virtual term substitution");
+ d_vts_inf[tn] = sm->mkDummySkolem(
+ "inf", tn, "infinity for virtual term substitution");
// mark as a virtual term
VirtualTermSkolemAttribute vtsa;
d_vts_inf[tn].setAttribute(vtsa, true);
#include "theory/quantifiers/conjecture_generator.h"
+#include "expr/skolem_manager.h"
#include "expr/term_canonize.h"
#include "options/quantifiers_options.h"
#include "theory/quantifiers/ematching/trigger_term_info.h"
Node ConjectureGenerator::getPredicateForType( TypeNode tn ) {
std::map< TypeNode, Node >::iterator it = d_typ_pred.find( tn );
if( it==d_typ_pred.end() ){
- TypeNode op_tn = NodeManager::currentNM()->mkFunctionType( tn, NodeManager::currentNM()->booleanType() );
- Node op = NodeManager::currentNM()->mkSkolem( "PE", op_tn, "was created by conjecture ground term enumerator." );
+ NodeManager* nm = NodeManager::currentNM();
+ SkolemManager* sm = nm->getSkolemManager();
+ TypeNode op_tn = nm->mkFunctionType(tn, nm->booleanType());
+ Node op = sm->mkDummySkolem(
+ "PE", op_tn, "was created by conjecture ground term enumerator.");
d_typ_pred[tn] = op;
return op;
}else{
#include "theory/quantifiers/dynamic_rewrite.h"
+#include "expr/skolem_manager.h"
#include "theory/rewriter.h"
using namespace std;
Node DynamicRewriter::OpInternalSymTrie::getSymbol(Node n)
{
+ NodeManager* nm = NodeManager::currentNM();
+ SkolemManager* sm = nm->getSkolemManager();
std::vector<TypeNode> ctypes;
for (const Node& cn : n)
{
}
else
{
- utype = NodeManager::currentNM()->mkFunctionType(ctypes);
+ utype = nm->mkFunctionType(ctypes);
}
- Node f = NodeManager::currentNM()->mkSkolem(
- "ufd", utype, "internal op for dynamic_rewriter");
+ Node f = sm->mkDummySkolem("ufd", utype, "internal op for dynamic_rewriter");
curr->d_sym = f;
return f;
}
#include "theory/quantifiers/expr_miner.h"
+#include "expr/skolem_manager.h"
#include "options/quantifiers_options.h"
#include "smt/smt_engine.h"
#include "smt/smt_engine_scope.h"
std::vector<Node> sks;
// map to skolems
NodeManager* nm = NodeManager::currentNM();
+ SkolemManager* sm = nm->getSkolemManager();
for (unsigned i = 0, size = fvs.size(); i < size; i++)
{
Node v = fvs[i];
std::map<Node, Node>::iterator itf = d_fv_to_skolem.find(v);
if (itf == d_fv_to_skolem.end())
{
- Node sk = nm->mkSkolem("rrck", v.getType());
+ Node sk = sm->mkDummySkolem("rrck", v.getType());
d_fv_to_skolem[v] = sk;
sks.push_back(sk);
}
#include "expr/dtype_cons.h"
#include "expr/node_algorithm.h"
+#include "expr/skolem_manager.h"
#include "options/quantifiers_options.h"
#include "theory/arith/arith_msum.h"
#include "theory/datatypes/theory_datatypes_utils.h"
: DecisionStrategyFmf(c, valuation), d_range(r), d_ranges_proxied(u)
{
if( options::fmfBoundLazy() ){
- d_proxy_range = isProxy ? r : NodeManager::currentNM()->mkSkolem( "pbir", r.getType() );
+ SkolemManager* sm = NodeManager::currentNM()->getSkolemManager();
+ d_proxy_range = isProxy ? r : sm->mkDummySkolem("pbir", r.getType());
}else{
d_proxy_range = r;
}
//this needs to be done at preregister since it affects e.g. QuantDSplit's preregister
Trace("bound-int") << "check ownership quantifier " << f << std::endl;
NodeManager* nm = NodeManager::currentNM();
+ SkolemManager* sm = nm->getSkolemManager();
bool success;
do{
if (expr::hasBoundVar(r))
{
// introduce a new bound
- Node new_range = NodeManager::currentNM()->mkSkolem(
- "bir", r.getType(), "bound for term");
+ Node new_range =
+ sm->mkDummySkolem("bir", r.getType(), "bound for term");
d_nground_range[f][v] = r;
d_range[f][v] = new_range;
r = new_range;
#include "theory/quantifiers/fmf/first_order_model_fmc.h"
#include "expr/attribute.h"
+#include "expr/skolem_manager.h"
#include "theory/quantifiers/fmf/full_model_check.h"
#include "theory/rewriter.h"
{
return it->second;
}
- Node st = NodeManager::currentNM()->mkSkolem(
- "star", tn, "skolem created for full-model checking");
+ SkolemManager* sm = NodeManager::currentNM()->getSkolemManager();
+ Node st =
+ sm->mkDummySkolem("star", tn, "skolem created for full-model checking");
d_type_star[tn] = st;
st.setAttribute(IsStarAttribute(), true);
return st;
#include "theory/quantifiers/fmf/full_model_check.h"
+#include "expr/skolem_manager.h"
#include "options/quantifiers_options.h"
#include "options/theory_options.h"
#include "options/uf_options.h"
return;
}
NodeManager* nm = NodeManager::currentNM();
+ SkolemManager* sm = nm->getSkolemManager();
std::vector<TypeNode> types;
for (const Node& v : q[0])
{
types.push_back(tn);
}
TypeNode typ = nm->mkFunctionType(types, nm->booleanType());
- Node op = nm->mkSkolem("qfmc", typ, "op for full-model checking");
+ Node op = sm->mkDummySkolem("qfmc", typ, "op for full-model checking");
d_quant_cond[q] = op;
}
#include "expr/dtype.h"
#include "expr/dtype_cons.h"
#include "expr/node_algorithm.h"
+#include "expr/skolem_manager.h"
#include "options/quantifiers_options.h"
#include "theory/arith/arith_msum.h"
#include "theory/datatypes/theory_datatypes_utils.h"
children.push_back(body);
if (marked)
{
- Node avar = nm->mkSkolem("id", nm->booleanType());
+ SkolemManager* sm = nm->getSkolemManager();
+ Node avar = sm->mkDummySkolem("id", nm->booleanType());
QuantIdNumAttribute ida;
avar.setAttribute(ida, 0);
iplc.push_back(nm->mkNode(kind::INST_ATTRIBUTE, avar));
#include <sstream>
#include "expr/node_algorithm.h"
+#include "expr/skolem_manager.h"
#include "theory/quantifiers/term_util.h"
#include "theory/rewriter.h"
Assert(d_input_funcs.empty());
Assert(d_si_vars.empty());
NodeManager* nm = NodeManager::currentNM();
+ SkolemManager* sm = nm->getSkolemManager();
d_has_input_funcs = has_funcs;
d_arg_types.insert(d_arg_types.end(), typs.begin(), typs.end());
d_input_funcs.insert(d_input_funcs.end(), funcs.begin(), funcs.end());
Assert(d_si_vars.size() == d_arg_types.size());
for (const Node& inf : d_input_funcs)
{
- Node sk = nm->mkSkolem("_sik", inf.getType());
+ Node sk = sm->mkDummySkolem("_sik", inf.getType());
d_input_func_sks.push_back(sk);
}
Trace("si-prt") << "SingleInvocationPartition::process " << n << std::endl;
std::vector<unsigned>& sub_vars)
{
NodeManager* nm = NodeManager::currentNM();
+ SkolemManager* sm = nm->getSkolemManager();
Assert(sk.empty() || sk.size() == f[0].getNumChildren());
// calculate the variables and substitution
std::vector<TNode> ind_vars;
{
if (argTypes.empty())
{
- s = NodeManager::currentNM()->mkSkolem(
+ s = sm->mkDummySkolem(
"skv", f[0][i].getType(), "created during skolemization");
}
else
{
- TypeNode typ = NodeManager::currentNM()->mkFunctionType(
- argTypes, f[0][i].getType());
- Node op = NodeManager::currentNM()->mkSkolem(
+ TypeNode typ = nm->mkFunctionType(argTypes, f[0][i].getType());
+ Node op = sm->mkDummySkolem(
"skop", typ, "op created during pre-skolemization");
// DOTHIS: set attribute on op, marking that it should not be selected
// as trigger
std::vector<Node> funcArgs;
funcArgs.push_back(op);
funcArgs.insert(funcArgs.end(), fvs.begin(), fvs.end());
- s = NodeManager::currentNM()->mkNode(kind::APPLY_UF, funcArgs);
+ s = nm->mkNode(kind::APPLY_UF, funcArgs);
}
sk.push_back(s);
}
{
conj.push_back(ret.substitute(ind_vars[0], selfSel[j]).negate());
}
- disj.push_back(conj.size() == 1
- ? conj[0]
- : NodeManager::currentNM()->mkNode(OR, conj));
+ disj.push_back(conj.size() == 1 ? conj[0] : nm->mkNode(OR, conj));
}
Assert(!disj.empty());
- n_str_ind = disj.size() == 1
- ? disj[0]
- : NodeManager::currentNM()->mkNode(AND, disj);
+ n_str_ind = disj.size() == 1 ? disj[0] : nm->mkNode(AND, disj);
}
else if (options::intWfInduction() && tn.isInteger())
{
- Node icond = NodeManager::currentNM()->mkNode(
- GEQ, k, NodeManager::currentNM()->mkConst(Rational(0)));
- Node iret =
- ret.substitute(
- ind_vars[0],
- NodeManager::currentNM()->mkNode(
- MINUS, k, NodeManager::currentNM()->mkConst(Rational(1))))
- .negate();
- n_str_ind = NodeManager::currentNM()->mkNode(OR, icond.negate(), iret);
- n_str_ind = NodeManager::currentNM()->mkNode(AND, icond, n_str_ind);
+ Node icond = nm->mkNode(GEQ, k, nm->mkConst(Rational(0)));
+ Node iret = ret.substitute(ind_vars[0],
+ nm->mkNode(MINUS, k, nm->mkConst(Rational(1))))
+ .negate();
+ n_str_ind = nm->mkNode(OR, icond.negate(), iret);
+ n_str_ind = nm->mkNode(AND, icond, n_str_ind);
}
else
{
rem_ind_vars.end(), ind_vars.begin() + 1, ind_vars.end());
if (!rem_ind_vars.empty())
{
- Node bvl = NodeManager::currentNM()->mkNode(BOUND_VAR_LIST, rem_ind_vars);
- nret = NodeManager::currentNM()->mkNode(FORALL, bvl, nret);
+ Node bvl = nm->mkNode(BOUND_VAR_LIST, rem_ind_vars);
+ nret = nm->mkNode(FORALL, bvl, nret);
nret = Rewriter::rewrite(nret);
sub = nret;
sub_vars.insert(
sub_vars.end(), ind_var_indicies.begin() + 1, ind_var_indicies.end());
- n_str_ind = NodeManager::currentNM()
- ->mkNode(FORALL, bvl, n_str_ind.negate())
- .negate();
+ n_str_ind = nm->mkNode(FORALL, bvl, n_str_ind.negate()).negate();
}
- ret = NodeManager::currentNM()->mkNode(OR, nret, n_str_ind);
+ ret = nm->mkNode(OR, nret, n_str_ind);
}
Trace("quantifiers-sk-debug") << "mkSkolem body for " << f
<< " returns : " << ret << std::endl;
**/
#include "theory/quantifiers/sygus/ce_guided_single_inv.h"
+#include "expr/skolem_manager.h"
#include "options/quantifiers_options.h"
#include "smt/logic_exception.h"
#include "smt/smt_engine.h"
return;
}
NodeManager* nm = NodeManager::currentNM();
+ SkolemManager* sm = nm->getSkolemManager();
d_single_inv = d_sip->getSingleInvocation();
d_single_inv = TermUtil::simpleNegate(d_single_inv);
std::vector<Node> func_vars;
d_sip->getSingleInvocationVariables(sivars);
for (unsigned i = 0, size = sivars.size(); i < size; i++)
{
- Node v = NodeManager::currentNM()->mkSkolem(
- "a", sivars[i].getType(), "single invocation arg");
+ Node v =
+ sm->mkDummySkolem("a", sivars[i].getType(), "single invocation arg");
d_single_inv_arg_sk.push_back(v);
}
d_single_inv = d_single_inv.substitute(sivars.begin(),
}
Trace("sygus-si") << "Solve using single invocation..." << std::endl;
NodeManager* nm = NodeManager::currentNM();
+ SkolemManager* sm = nm->getSkolemManager();
// Mark the quantified formula with the quantifier elimination attribute to
// ensure its structure is preserved in the query below.
Node siq = d_single_inv;
if (siq.getKind() == FORALL)
{
- Node n_attr =
- nm->mkSkolem("qe_si",
- nm->booleanType(),
- "Auxiliary variable for qe attr for single invocation.");
+ Node n_attr = sm->mkDummySkolem(
+ "qe_si",
+ nm->booleanType(),
+ "Auxiliary variable for qe attr for single invocation.");
QuantElimAttribute qea;
n_attr.setAttribute(qea, true);
n_attr = nm->mkNode(INST_ATTRIBUTE, n_attr);
#include "theory/quantifiers/sygus/cegis_unif.h"
+#include "expr/skolem_manager.h"
#include "expr/sygus_datatype.h"
#include "options/quantifiers_options.h"
#include "printer/printer.h"
Node CegisUnifEnumDecisionStrategy::mkLiteral(unsigned n)
{
NodeManager* nm = NodeManager::currentNM();
- Node new_lit = nm->mkSkolem("G_cost", nm->booleanType());
+ SkolemManager* sm = nm->getSkolemManager();
+ Node newLit = sm->mkDummySkolem("G_cost", nm->booleanType());
unsigned new_size = n + 1;
// allocate an enumerator for each candidate
{
Node c = ci.first;
TypeNode ct = c.getType();
- Node eu = nm->mkSkolem("eu", ct);
+ Node eu = sm->mkDummySkolem("eu", ct);
Node ceu;
if (!d_useCondPool && !ci.second.d_enums[0].empty())
{
// make a new conditional enumerator as well, starting the
// second type around
- ceu = nm->mkSkolem("cu", ci.second.d_ce_type);
+ ceu = sm->mkDummySkolem("cu", ci.second.d_ce_type);
}
// register the new enumerators
for (unsigned index = 0; index < 2; index++)
{
Trace("cegis-unif-enum") << "...increasing enum number for hd " << ei
<< " to new size " << new_size << "\n";
- registerEvalPtAtSize(c, ei, new_lit, new_size);
+ registerEvalPtAtSize(c, ei, newLit, new_size);
}
}
// enforce fairness between number of enumerators and enumerator size
datatypes.push_back(sdt.getDatatype());
std::vector<TypeNode> dtypes = nm->mkMutualDatatypeTypes(
datatypes, unresolvedTypes, NodeManager::DATATYPE_FLAG_PLACEHOLDER);
- d_virtual_enum = nm->mkSkolem("_ve", dtypes[0]);
+ d_virtual_enum = sm->mkDummySkolem("_ve", dtypes[0]);
d_tds->registerEnumerator(
d_virtual_enum, Node::null(), d_parent, ROLE_ENUM_CONSTRAINED);
}
Node size_ve = nm->mkNode(DT_SIZE, d_virtual_enum);
Node fair_lemma =
nm->mkNode(GEQ, size_ve, nm->mkConst(Rational(pow_two - 1)));
- fair_lemma = nm->mkNode(OR, new_lit, fair_lemma);
+ fair_lemma = nm->mkNode(OR, newLit, fair_lemma);
Trace("cegis-unif-enum-lemma")
<< "CegisUnifEnum::lemma, fairness size:" << fair_lemma << "\n";
// this lemma relates the number of conditions we enumerate and the
}
}
- return new_lit;
+ return newLit;
}
void CegisUnifEnumDecisionStrategy::initialize(
}
// initialize type information for candidates
NodeManager* nm = NodeManager::currentNM();
+ SkolemManager* sm = nm->getSkolemManager();
for (const Node& e : es)
{
Trace("cegis-unif-enum-debug") << "...adding strategy point " << e << "\n";
// allocate a condition enumerator for each candidate
for (std::pair<const Node, StrategyPtInfo>& ci : d_ce_info)
{
- Node ceu = nm->mkSkolem("cu", ci.second.d_ce_type);
+ Node ceu = sm->mkDummySkolem("cu", ci.second.d_ce_type);
setUpEnumerator(ceu, ci.second, 1);
}
}
#include "theory/quantifiers/sygus/rcons_type_info.h"
+#include "expr/skolem_manager.h"
#include "theory/datatypes/sygus_datatype_utils.h"
namespace cvc5 {
const std::vector<Node>& builtinVars)
{
NodeManager* nm = NodeManager::currentNM();
+ SkolemManager* sm = nm->getSkolemManager();
d_enumerator.reset(new SygusEnumerator(tds, nullptr, s, true));
- d_enumerator->initialize(nm->mkSkolem("sygus_rcons", stn));
+ d_enumerator->initialize(sm->mkDummySkolem("sygus_rcons", stn));
d_crd.reset(new CandidateRewriteDatabase(true, false, true, false));
// since initial samples are not always useful for equivalence checks, set
// their number to 0
#include "expr/dtype.h"
#include "expr/node_algorithm.h"
+#include "expr/skolem_manager.h"
#include "expr/sygus_datatype.h"
#include "theory/datatypes/sygus_datatype_utils.h"
#include "theory/quantifiers/quantifiers_attributes.h"
TypeNode abdGType)
{
NodeManager* nm = NodeManager::currentNM();
+ SkolemManager* sm = nm->getSkolemManager();
std::unordered_set<Node, NodeHashFunction> symset;
for (size_t i = 0, size = asserts.size(); i < size; i++)
{
Node sc = nm->mkNode(AND, aconj, abdApp);
Node vbvl = nm->mkNode(BOUND_VAR_LIST, vars);
sc = nm->mkNode(EXISTS, vbvl, sc);
- Node sygusScVar = nm->mkSkolem("sygus_sc", nm->booleanType());
+ Node sygusScVar = sm->mkDummySkolem("sygus_sc", nm->booleanType());
sygusScVar.setAttribute(theory::SygusSideConditionAttribute(), sc);
Node instAttr = nm->mkNode(INST_ATTRIBUTE, sygusScVar);
// build in the side condition
#include "theory/quantifiers/sygus/sygus_qe_preproc.h"
#include "expr/node_algorithm.h"
+#include "expr/skolem_manager.h"
#include "theory/quantifiers/single_inv_partition.h"
#include "theory/rewriter.h"
#include "theory/smt_engine_subsolver.h"
body = body[0][1];
}
NodeManager* nm = NodeManager::currentNM();
+ SkolemManager* sm = nm->getSkolemManager();
Trace("cegqi-qep") << "Compute single invocation for " << q << "..."
<< std::endl;
quantifiers::SingleInvocationPartition sip;
// skolemize non-qe variables
for (unsigned i = 0, size = nqe_vars.size(); i < size; i++)
{
- Node k = nm->mkSkolem(
+ Node k = sm->mkDummySkolem(
"k", nqe_vars[i].getType(), "qe for non-ground single invocation");
orig.push_back(nqe_vars[i]);
subs.push_back(k);
Node fv = sip.getFirstOrderVariableForFunction(f);
Assert(!fi.isNull());
orig.push_back(fi);
- Node k = nm->mkSkolem(
+ Node k = sm->mkDummySkolem(
"k", fv.getType(), "qe for function in non-ground single invocation");
subs.push_back(k);
Trace("cegqi-qep") << " subs : " << fi << " -> " << k << std::endl;
#include "theory/quantifiers/sygus/sygus_reconstruct.h"
#include "expr/node_algorithm.h"
+#include "expr/skolem_manager.h"
#include "smt/command.h"
#include "theory/datatypes/sygus_datatype_utils.h"
#include "theory/rewriter.h"
initialize(stn);
NodeManager* nm = NodeManager::currentNM();
+ SkolemManager* sm = nm->getSkolemManager();
/** a set of obligations that are not yet satisfied for each sygus datatype */
TypeObligationSetMap unsolvedObs;
// paramaters sol and stn constitute the main obligation to satisfy
- Node mainOb = nm->mkSkolem("sygus_rcons", stn);
+ Node mainOb = sm->mkDummySkolem("sygus_rcons", stn);
// add the main obligation to the set of obligations that are not yet
// satisfied
{
// if not, create an "artifical" obligation whose solution would be
// the enumerated term
- k = nm->mkSkolem("sygus_rcons", pair.first);
+ k = sm->mkDummySkolem("sygus_rcons", pair.first);
d_obInfo.emplace(k, RConsObligationInfo(builtin));
d_stnInfo[pair.first].setBuiltinToOb(builtin, k);
}
TypeObligationSetMap SygusReconstruct::matchNewObs(Node k, Node sz)
{
NodeManager* nm = NodeManager::currentNM();
+ SkolemManager* sm = nm->getSkolemManager();
TypeObligationSetMap obsPrime;
// obligations generated by match. Note that we might have already seen (and
else
{
// otherwise, create a new obligation of the corresponding sygus type
- newVar = nm->mkSkolem("sygus_rcons", stn);
+ newVar = sm->mkDummySkolem("sygus_rcons", stn);
d_obInfo.emplace(newVar, candOb.second);
d_stnInfo[stn].setBuiltinToOb(candOb.second, newVar);
// if the candidate obligation is a constant and the grammar allows
#include "expr/dtype_cons.h"
#include "expr/node_algorithm.h"
+#include "expr/skolem_manager.h"
#include "options/base_options.h"
#include "options/quantifiers_options.h"
#include "printer/printer.h"
const std::vector<Node>& sk_vars)
{
NodeManager* nm = NodeManager::currentNM();
+ SkolemManager* sm = nm->getSkolemManager();
Trace("sygus-repair-const") << " Substitute skeletons..." << std::endl;
body = body.substitute(candidates.begin(),
candidates.end(),
if (itf == d_sk_to_fo.end())
{
TypeNode builtinType = d_tds->sygusToBuiltinType(v.getType());
- Node sk_fov = nm->mkSkolem("k", builtinType);
+ Node sk_fov = sm->mkDummySkolem("k", builtinType);
d_sk_to_fo[v] = sk_fov;
d_fo_to_sk[sk_fov] = v;
Trace("sygus-repair-const-debug")
#include "theory/quantifiers/sygus/sygus_unif_rl.h"
+#include "expr/skolem_manager.h"
#include "options/base_options.h"
#include "options/quantifiers_options.h"
#include "printer/printer.h"
bool childChanged = false;
std::vector<Node> children;
NodeManager* nm = NodeManager::currentNM();
+ SkolemManager* sm = nm->getSkolemManager();
for (unsigned i = 0; i < size; ++i)
{
if (i == 0 && fapp)
// 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 = nm->mkSkolem(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",
+ NodeManager::SKOLEM_EXACT_NAME);
// Adds new enumerator to map from candidate
Trace("sygus-unif-rl-purify")
<< "...new enum " << new_f << " for candidate " << nb[0] << "\n";
#include "expr/dtype.h"
#include "expr/dtype_cons.h"
+#include "expr/skolem_manager.h"
#include "theory/datatypes/theory_datatypes_utils.h"
#include "theory/quantifiers/sygus/sygus_eval_unfold.h"
#include "theory/quantifiers/sygus/sygus_unif.h"
void SygusUnifStrategy::buildStrategyGraph(TypeNode tn, NodeRole nrole)
{
NodeManager* nm = NodeManager::currentNM();
+ SkolemManager* sm = nm->getSkolemManager();
if (d_tinfo.find(tn) == d_tinfo.end())
{
// register type
std::map<EnumRole, Node>::iterator iten = eti.d_enum.find(erole);
if (iten == eti.d_enum.end())
{
- ee = nm->mkSkolem("ee", tn);
+ ee = sm->mkDummySkolem("ee", tn);
eti.d_enum[erole] = ee;
Trace("sygus-unif-debug")
<< "...enumerator " << ee << " for " << tn.getDType().getName()
for (unsigned k = 0, nargs = dt[j].getNumArgs(); k < nargs; k++)
{
TypeNode ttn = dt[j][k].getRangeType();
- Node kv = nm->mkSkolem("ut", ttn);
+ Node kv = sm->mkDummySkolem("ut", ttn);
sks.push_back(kv);
cop_to_sks[cop].push_back(kv);
sktns.push_back(ttn);
<< std::endl;
Node esk = nm->mkNode(DT_SYGUS_EVAL, echildren);
vs.push_back(esk);
- Node tvar = nm->mkSkolem("templ", esk.getType());
+ Node tvar = sm->mkDummySkolem("templ", esk.getType());
templ_var_index[tvar] = k;
Trace("sygus-unif-debug2") << "* template inference : looking for "
<< tvar << " for arg " << k << std::endl;
if (cop_to_child_templ[cop].find(j) != cop_to_child_templ[cop].end())
{
// it is templated, allocate a fresh variable
- et = nm->mkSkolem("et", ct);
+ et = sm->mkDummySkolem("et", ct);
Trace("sygus-unif-debug") << "...enumerate " << et << " of type "
<< ct.getDType().getName();
Trace("sygus-unif-debug") << " for arg " << j << " of "
#include <sstream>
#include "expr/node_algorithm.h"
+#include "expr/skolem_manager.h"
#include "theory/quantifiers/quantifiers_attributes.h"
#include "theory/quantifiers/sygus/sygus_grammar_cons.h"
{
Assert(!fs.empty());
NodeManager* nm = NodeManager::currentNM();
+ SkolemManager* sm = nm->getSkolemManager();
SygusAttribute ca;
- Node sygusVar = nm->mkSkolem("sygus", nm->booleanType());
+ Node sygusVar = sm->mkDummySkolem("sygus", nm->booleanType());
sygusVar.setAttribute(ca, true);
std::vector<Node> ipls{nm->mkNode(INST_ATTRIBUTE, sygusVar)};
// insert the remaining instantiation attributes
{
Assert(!fs.empty());
NodeManager* nm = NodeManager::currentNM();
+ SkolemManager* sm = nm->getSkolemManager();
std::vector<Node> iattrs;
// take existing properties, without the previous solves
SygusSolutionAttribute ssa;
for (size_t i = 0, nsolved = solvedf.size(); i < nsolved; i++)
{
Node eq = solvedf.getEquality(i);
- Node var = nm->mkSkolem("solved", nm->booleanType());
+ Node var = sm->mkDummySkolem("solved", nm->booleanType());
var.setAttribute(ssa, eq);
Node ipv = nm->mkNode(INST_ATTRIBUTE, var);
iattrs.push_back(ipv);
#include "theory/quantifiers/sygus/synth_conjecture.h"
#include "base/configuration.h"
+#include "expr/skolem_manager.h"
#include "options/base_options.h"
#include "options/datatypes_options.h"
#include "options/quantifiers_options.h"
#include "theory/quantifiers/sygus/enum_stream_substitution.h"
#include "theory/quantifiers/sygus/sygus_enumerator.h"
#include "theory/quantifiers/sygus/sygus_enumerator_basic.h"
-#include "theory/quantifiers/sygus/synth_engine.h"
#include "theory/quantifiers/sygus/sygus_grammar_cons.h"
#include "theory/quantifiers/sygus/sygus_pbe.h"
+#include "theory/quantifiers/sygus/synth_engine.h"
#include "theory/quantifiers/sygus/term_database_sygus.h"
#include "theory/quantifiers/term_util.h"
#include "theory/rewriter.h"
Trace("cegqi") << "SynthConjecture : assign : " << q << std::endl;
d_quant = q;
NodeManager* nm = NodeManager::currentNM();
+ SkolemManager* sm = nm->getSkolemManager();
// initialize the guard
- d_feasible_guard = nm->mkSkolem("G", nm->booleanType());
+ d_feasible_guard = sm->mkDummySkolem("G", nm->booleanType());
d_feasible_guard = Rewriter::rewrite(d_feasible_guard);
d_feasible_guard = d_qstate.getValuation().ensureLiteral(d_feasible_guard);
AlwaysAssert(!d_feasible_guard.isNull());
for (unsigned i = 0; i < d_embed_quant[0].getNumChildren(); i++)
{
vars.push_back(d_embed_quant[0][i]);
- Node e =
- NodeManager::currentNM()->mkSkolem("e", d_embed_quant[0][i].getType());
+ Node e = sm->mkDummySkolem("e", d_embed_quant[0][i].getType());
d_candidates.push_back(e);
}
Trace("cegqi") << "Base quantified formula is : " << d_embed_quant
}
NodeManager* nm = NodeManager::currentNM();
+ SkolemManager* sm = nm->getSkolemManager();
// check the side condition if we constructed a candidate
if (constructed_cand)
{
for (const Node& v : inst[0][0])
{
- Node sk = nm->mkSkolem("rsk", v.getType());
+ Node sk = sm->mkDummySkolem("rsk", v.getType());
sks.push_back(sk);
vars.push_back(v);
Trace("cegqi-check-debug")
**/
#include "theory/quantifiers/sygus/template_infer.h"
+#include "expr/skolem_manager.h"
#include "options/quantifiers_options.h"
#include "theory/quantifiers/sygus/sygus_grammar_cons.h"
#include "theory/quantifiers/sygus/sygus_utils.h"
}
Assert(prog == q[0][0]);
NodeManager* nm = NodeManager::currentNM();
+ SkolemManager* sm = nm->getSkolemManager();
// map the program back via non-single invocation map
std::vector<Node> prog_templ_vars;
d_ti.getVariables(prog_templ_vars);
{
atn = atn.getRangeType();
}
- d_templ_arg[prog] = nm->mkSkolem("I", atn);
+ d_templ_arg[prog] = sm->mkDummySkolem("I", atn);
// construct template
Node templ;
#include "base/check.h"
#include "expr/dtype_cons.h"
+#include "expr/skolem_manager.h"
#include "expr/sygus_datatype.h"
#include "options/base_options.h"
#include "options/datatypes_options.h"
{
SygusTypeInfo& ti = getTypeInfo(tn);
int anyC = ti.getAnyConstantConsNum();
+ NodeManager* nm = NodeManager::currentNM();
Node k;
if (anyC == -1)
{
- k = NodeManager::currentNM()->mkSkolem("sy", tn, "sygus proxy");
+ SkolemManager* sm = nm->getSkolemManager();
+ k = sm->mkDummySkolem("sy", tn, "sygus proxy");
SygusPrintProxyAttribute spa;
k.setAttribute(spa, c);
}
else
{
const DType& dt = tn.getDType();
- k = NodeManager::currentNM()->mkNode(
- APPLY_CONSTRUCTOR, dt[anyC].getConstructor(), c);
+ k = nm->mkNode(APPLY_CONSTRUCTOR, dt[anyC].getConstructor(), c);
}
d_proxy_vars[tn][c] = k;
return k;
// populate a pool of terms, or (some cases) of when it is actively generated.
if (isActiveGen || erole == ROLE_ENUM_POOL)
{
+ SkolemManager* sm = nm->getSkolemManager();
// make the guard
- Node ag = nm->mkSkolem("eG", nm->booleanType());
+ Node ag = sm->mkDummySkolem("eG", nm->booleanType());
// must ensure it is a literal immediately here
ag = d_qstate.getValuation().ensureLiteral(ag);
// must ensure that it is asserted as a literal before we begin solving
#include "theory/quantifiers/sygus/transition_inference.h"
#include "expr/node_algorithm.h"
+#include "expr/skolem_manager.h"
#include "theory/arith/arith_msum.h"
#include "theory/quantifiers/term_util.h"
#include "theory/rewriter.h"
void TransitionInference::process(Node n)
{
NodeManager* nm = NodeManager::currentNM();
+ SkolemManager* sm = nm->getSkolemManager();
d_complete = true;
d_trivial = true;
std::vector<Node> n_check;
{
for (unsigned j = 0, nchild = next.getNumChildren(); j < nchild; j++)
{
- Node v = nm->mkSkolem(
+ Node v = sm->mkDummySkolem(
"ir", next[j].getType(), "template inference rev argument");
d_prime_vars.push_back(v);
}
d_func = op;
Trace("cegqi-inv-debug") << "Use " << op << " with args ";
NodeManager* nm = NodeManager::currentNM();
+ SkolemManager* sm = nm->getSkolemManager();
for (const Node& l : lit)
{
- Node v = nm->mkSkolem("i", l.getType(), "template inference argument");
+ Node v =
+ sm->mkDummySkolem("i", l.getType(), "template inference argument");
d_vars.push_back(v);
Trace("cegqi-inv-debug") << v << " ";
}
#include <unordered_set>
#include "expr/node_algorithm.h"
+#include "expr/skolem_manager.h"
#include "options/quantifiers_options.h"
#include "theory/bv/theory_bv_utils.h"
#include "theory/datatypes/sygus_datatype_utils.h"
}
NodeManager* nm = NodeManager::currentNM();
- Node sk = nm->mkSkolem("CeLiteral", nm->booleanType());
+ SkolemManager* sm = nm->getSkolemManager();
+ Node sk = sm->mkDummySkolem("CeLiteral", nm->booleanType());
Node lit = d_qstate.getValuation().ensureLiteral(sk);
d_ce_lits[q] = lit;
return lit;
#include "theory/quantifiers/term_database.h"
+#include "expr/skolem_manager.h"
#include "options/base_options.h"
#include "options/quantifiers_options.h"
#include "options/smt_options.h"
d_type_fv.find(tn);
if (it == d_type_fv.end())
{
+ SkolemManager* sm = NodeManager::currentNM()->getSkolemManager();
std::stringstream ss;
ss << language::SetLanguage(options::outputLanguage());
ss << "e_" << tn;
- Node k = NodeManager::currentNM()->mkSkolem(
- ss.str(), tn, "is a termDb fresh variable");
+ Node k = sm->mkDummySkolem(ss.str(), tn, "is a termDb fresh variable");
Trace("mkVar") << "TermDb:: Make variable " << k << " : " << tn
<< std::endl;
if (options::instMaxLevel() != -1)
d_type_fv[tn] = k;
return k;
}
- else
- {
- return it->second;
- }
+ return it->second;
}
Node TermDb::getMatchOperator( Node n ) {
return;
}
NodeManager* nm = NodeManager::currentNM();
+ SkolemManager* sm = nm->getSkolemManager();
Node curr = n;
std::vector<Node> args;
while (curr.getKind() == HO_APPLY)
Node psk;
if (itp == d_ho_fun_op_purify.end())
{
- psk = nm->mkSkolem("pfun",
- curr.getType(),
- "purify for function operator term indexing");
+ psk = sm->mkDummySkolem("pfun",
+ curr.getType(),
+ "purify for function operator term indexing");
d_ho_fun_op_purify[curr] = psk;
// we do not add it to d_ops since it is an internal operator
}
return ithp->second;
}
NodeManager* nm = NodeManager::currentNM();
+ SkolemManager* sm = nm->getSkolemManager();
TypeNode ptn = nm->mkFunctionType(tn, nm->booleanType());
- Node k = nm->mkSkolem("U", ptn, "predicate to force higher-order types");
+ Node k = sm->mkDummySkolem("U", ptn, "predicate to force higher-order types");
d_ho_type_match_pred[tn] = k;
return k;
}
#include "base/map_util.h"
#include "expr/kind.h"
+#include "expr/skolem_manager.h"
#include "options/quantifiers_options.h"
#include "options/sep_options.h"
#include "options/smt_options.h"
TNode satom = atom.getKind() == SEP_LABEL ? atom[0] : atom;
TNode slbl = atom.getKind() == SEP_LABEL ? atom[1] : TNode::null();
NodeManager* nm = NodeManager::currentNM();
+ SkolemManager* sm = nm->getSkolemManager();
if (slbl.isNull())
{
Trace("sep-lemma-debug")
}
else
{
- Node kl = nm->mkSkolem("loc", getReferenceType(satom));
- Node kd = nm->mkSkolem("data", getDataType(satom));
+ Node kl = sm->mkDummySkolem("loc", getReferenceType(satom));
+ Node kd = sm->mkDummySkolem("data", getDataType(satom));
Node econc = nm->mkNode(
SEP_LABEL,
nm->mkNode(SEP_STAR, nm->mkNode(SEP_PTO, kl, kd), d_true),
Trace("sep-lemma-debug")
<< "Negated spatial constraint asserted to sep theory: " << fact
<< std::endl;
- Node g = nm->mkSkolem("G", nm->booleanType());
+ Node g = sm->mkDummySkolem("G", nm->booleanType());
d_neg_guard_strategy[g].reset(new DecisionStrategySingleton(
"sep_neg_guard", g, getSatContext(), getValuation()));
DecisionStrategySingleton* ds = d_neg_guard_strategy[g].get();
return;
}
NodeManager* nm = NodeManager::currentNM();
+ SkolemManager* sm = nm->getSkolemManager();
Trace("sep-process") << "Checking heap at full effort..." << std::endl;
d_label_model.clear();
d_tmodel.clear();
{
Trace("sep-process") << "Must witness label : " << ll
<< ", data type is " << data_type << std::endl;
- Node dsk =
- nm->mkSkolem("dsk", data_type, "pto-data for implicit location");
+ Node dsk = sm->mkDummySkolem(
+ "dsk", data_type, "pto-data for implicit location");
// if location is in the heap, then something must point to it
Node lem = nm->mkNode(
IMPLIES,
if( !d_bounds_init ){
Trace("sep-bound") << "Initialize sep bounds..." << std::endl;
d_bounds_init = true;
+ NodeManager* nm = NodeManager::currentNM();
+ SkolemManager* sm = nm->getSkolemManager();
for( std::map< TypeNode, TypeNode >::iterator it = d_loc_to_data_type.begin(); it != d_loc_to_data_type.end(); ++it ){
TypeNode tn = it->first;
Trace("sep-bound") << "Initialize bounds for " << tn << "..." << std::endl;
Trace("sep-bound") << "Type reference size : " << d_type_references[tn].size() << std::endl;
Trace("sep-bound") << "Constructing " << n_emp << " cardinality constants." << std::endl;
for( unsigned r=0; r<n_emp; r++ ){
- Node e = NodeManager::currentNM()->mkSkolem( "e", tn, "cardinality bound element for seplog" );
+ Node e =
+ sm->mkDummySkolem("e", tn, "cardinality bound element for seplog");
d_type_references_card[tn].push_back( e );
d_type_ref_card_id[e] = r;
}
Node TheorySep::getBaseLabel( TypeNode tn ) {
std::map< TypeNode, Node >::iterator it = d_base_label.find( tn );
if( it==d_base_label.end() ){
+ NodeManager* nm = NodeManager::currentNM();
+ SkolemManager* sm = nm->getSkolemManager();
initializeBounds();
Trace("sep") << "Make base label for " << tn << std::endl;
std::stringstream ss;
ss << "__Lb";
- TypeNode ltn = NodeManager::currentNM()->mkSetType(tn);
- //TypeNode ltn = NodeManager::currentNM()->mkSetType(NodeManager::currentNM()->mkRefType(tn));
- Node n_lbl = NodeManager::currentNM()->mkSkolem( ss.str(), ltn, "base label" );
+ TypeNode ltn = nm->mkSetType(tn);
+ Node n_lbl = sm->mkDummySkolem(ss.str(), ltn, "base label");
d_base_label[tn] = n_lbl;
//make reference bound
Trace("sep") << "Make reference bound label for " << tn << std::endl;
std::stringstream ss2;
ss2 << "__Lu";
- d_reference_bound[tn] = NodeManager::currentNM()->mkSkolem( ss2.str(), ltn, "" );
+ d_reference_bound[tn] = sm->mkDummySkolem(ss2.str(), ltn, "");
d_type_references_all[tn].insert( d_type_references_all[tn].end(), d_type_references[tn].begin(), d_type_references[tn].end() );
//check whether monotonic (elements can be added to tn without effecting satisfiability)
Node TheorySep::getLabel( Node atom, int child, Node lbl ) {
std::map< int, Node >::iterator it = d_label_map[atom][lbl].find( child );
if( it==d_label_map[atom][lbl].end() ){
+ NodeManager* nm = NodeManager::currentNM();
+ SkolemManager* sm = nm->getSkolemManager();
TypeNode refType = getReferenceType( atom );
std::stringstream ss;
ss << "__Lc" << child;
TypeNode ltn = NodeManager::currentNM()->mkSetType(refType);
//TypeNode ltn = NodeManager::currentNM()->mkSetType(NodeManager::currentNM()->mkRefType(refType));
- Node n_lbl = NodeManager::currentNM()->mkSkolem( ss.str(), ltn, "sep label" );
+ Node n_lbl = sm->mkDummySkolem(ss.str(), ltn, "sep label");
d_label_map[atom][lbl][child] = n_lbl;
d_label_map_parent[n_lbl] = lbl;
return n_lbl;
#include "expr/emptyset.h"
#include "expr/node_algorithm.h"
+#include "expr/skolem_manager.h"
#include "options/sets_options.h"
#include "smt/logic_exception.h"
#include "theory/rewriter.h"
std::uint32_t vu = v.getConst<Rational>().getNumerator().toUnsignedInt();
Assert(els.size() <= vu);
NodeManager* nm = NodeManager::currentNM();
+ SkolemManager* sm = nm->getSkolemManager();
if (elementType.isInterpretedFinite())
{
// get all members of this finite type
// slack elements for the leaves without worrying about conflicts with
// the current members of this finite type.
- Node slack = nm->mkSkolem("slack", elementType);
+ Node slack = sm->mkDummySkolem("slack", elementType);
Node singleton = nm->mkSingleton(elementType, slack);
els.push_back(singleton);
d_finite_type_slack_elements[elementType].push_back(slack);
}
else
{
- els.push_back(
- nm->mkSingleton(elementType, nm->mkSkolem("msde", elementType)));
+ els.push_back(nm->mkSingleton(
+ elementType, sm->mkDummySkolem("msde", elementType)));
}
}
}
#include "theory/sets/skolem_cache.h"
+#include "expr/skolem_manager.h"
#include "theory/rewriter.h"
using namespace cvc5::kind;
Node SkolemCache::mkTypedSkolem(TypeNode tn, const char* c)
{
- Node n = NodeManager::currentNM()->mkSkolem(c, tn, "sets skolem");
+ SkolemManager* sm = NodeManager::currentNM()->getSkolemManager();
+ Node n = sm->mkDummySkolem(c, tn, "sets skolem");
d_allSkolems.insert(n);
return n;
}
#include "theory/sets/term_registry.h"
#include "expr/emptyset.h"
+#include "expr/skolem_manager.h"
using namespace std;
using namespace cvc5::kind;
std::map<TypeNode, Node>::iterator it = d_tc_skolem[n].find(tn);
if (it == d_tc_skolem[n].end())
{
- Node k = NodeManager::currentNM()->mkSkolem("tc_k", tn);
+ SkolemManager* sm = NodeManager::currentNM()->getSkolemManager();
+ Node k = sm->mkDummySkolem("tc_k", tn);
d_tc_skolem[n][tn] = k;
return k;
}
}
NodeManager* nm = NodeManager::currentNM();
+ SkolemManager* sm = nm->getSkolemManager();
TypeNode chooseUf = nm->mkFunctionType(setType, setType.getSetElementType());
stringstream stream;
stream << "chooseUf" << setType.getId();
string name = stream.str();
- Node chooseSkolem = nm->mkSkolem(
+ Node chooseSkolem = sm->mkDummySkolem(
name, chooseUf, "choose function", NodeManager::SKOLEM_EXACT_NAME);
d_chooseFunctions[setType] = chooseSkolem;
return chooseSkolem;
**/
#include "theory/sets/theory_sets_rels.h"
-#include "theory/sets/theory_sets_private.h"
+
+#include "expr/skolem_manager.h"
#include "theory/sets/theory_sets.h"
+#include "theory/sets/theory_sets_private.h"
using namespace std;
using namespace cvc5::kind;
}
/* JOIN-IMAGE DOWN : (x) IS_IN (R JOIN_IMAGE n)
- * -------------------------------------------------------
- * (x, x1) IS_IN R .... (x, xn) IS_IN R DISTINCT(x1, ... , xn)
- *
- */
-
+ * -------------------------------------------------------
+ * (x, x1) IS_IN R .... (x, xn) IS_IN R DISTINCT(x1, ...
+ * , xn)
+ *
+ */
void TheorySetsRels::applyJoinImageRule( Node mem_rep, Node join_image_term, Node exp ) {
Trace("rels-debug") << "\n[Theory::Rels] *********** applyJoinImageRule on " << join_image_term
<< " with mem_rep = " << mem_rep << " and exp = " << exp << std::endl;
}
}
}
-
+ NodeManager* nm = NodeManager::currentNM();
+ SkolemManager* sm = nm->getSkolemManager();
Node reason = exp;
Node conclusion = d_trueNode;
std::vector< Node > distinct_skolems;
Node fst_mem_element = RelsUtils::nthElementOfTuple( exp[0], 0 );
if( exp[1] != join_image_term ) {
- reason = NodeManager::currentNM()->mkNode( kind::AND, reason, NodeManager::currentNM()->mkNode( kind::EQUAL, exp[1], join_image_term ) );
+ reason =
+ nm->mkNode(AND, reason, nm->mkNode(EQUAL, exp[1], join_image_term));
}
for( unsigned int i = 0; i < min_card; i++ ) {
- Node skolem = NodeManager::currentNM()->mkSkolem( "jig", join_image_rel.getType()[0].getTupleTypes()[0] );
+ Node skolem = sm->mkDummySkolem(
+ "jig", join_image_rel.getType()[0].getTupleTypes()[0]);
distinct_skolems.push_back( skolem );
- conclusion = NodeManager::currentNM()->mkNode( kind::AND, conclusion, NodeManager::currentNM()->mkNode( kind::MEMBER, RelsUtils::constructPair( join_image_rel, fst_mem_element, skolem ), join_image_rel ) );
+ conclusion = nm->mkNode(
+ AND,
+ conclusion,
+ nm->mkNode(
+ MEMBER,
+ RelsUtils::constructPair(join_image_rel, fst_mem_element, skolem),
+ join_image_rel));
}
if( distinct_skolems.size() >= 2 ) {
- conclusion = NodeManager::currentNM()->mkNode( kind::AND, conclusion, NodeManager::currentNM()->mkNode( kind::DISTINCT, distinct_skolems ) );
+ conclusion =
+ nm->mkNode(AND, conclusion, nm->mkNode(DISTINCT, distinct_skolems));
}
sendInfer(conclusion, InferenceId::SETS_RELS_JOIN_IMAGE_DOWN, reason);
Trace("rels-debug") << "\n[Theory::Rels] *********** Done with applyJoinImageRule ***********" << std::endl;
-
}
-
/* IDENTITY-DOWN : (x, y) IS_IN IDEN(R)
* -------------------------------------------------------
* x = y, (x IS_IN R)
#include <sstream>
#include <vector>
+#include "expr/skolem_manager.h"
#include "options/quantifiers_options.h"
#include "options/smt_options.h"
#include "options/uf_options.h"
-#include "theory/rewriter.h"
#include "theory/quantifiers/quant_util.h"
+#include "theory/rewriter.h"
using namespace cvc5;
using namespace cvc5::kind;
//must create new type
std::stringstream ss;
ss << "it_" << t << "_" << pref;
- retType = NodeManager::currentNM()->mkSort( ss.str() );
+ retType = NodeManager::currentNM()->mkSort(ss.str());
}
Trace("sort-inference") << "-> Make type " << retType << " to correspond to ";
printSort("sort-inference", t );
}
Node SortInference::getNewSymbol( Node old, TypeNode tn ){
+ NodeManager* nm = NodeManager::currentNM();
+ SkolemManager* sm = nm->getSkolemManager();
// if no sort was inferred for this node, return original
if( tn.isNull() || tn.isComparableTo( old.getType() ) ){
return old;
if( d_const_map[tn].find( old )==d_const_map[tn].end() ){
std::stringstream ss;
ss << "ic_" << tn << "_" << old;
- d_const_map[tn][ old ] = NodeManager::currentNM()->mkSkolem( ss.str(), tn, "constant created during sort inference" ); //use mkConst???
+ d_const_map[tn][old] = sm->mkDummySkolem(
+ ss.str(),
+ tn,
+ "constant created during sort inference"); // use mkConst???
}
return d_const_map[tn][ old ];
}else if( old.getKind()==kind::BOUND_VARIABLE ){
std::stringstream ss;
ss << "b_" << old;
- return NodeManager::currentNM()->mkBoundVar( ss.str(), tn );
- }else{
- std::stringstream ss;
- ss << "i_" << old;
- return NodeManager::currentNM()->mkSkolem( ss.str(), tn, "created during sort inference" );
+ return nm->mkBoundVar(ss.str(), tn);
}
+ std::stringstream ss;
+ ss << "i_" << old;
+ return sm->mkDummySkolem(ss.str(), tn, "created during sort inference");
}
Node SortInference::simplifyNode(
if( itv!=visited[n].end() ){
return itv->second;
}else{
+ NodeManager* nm = NodeManager::currentNM();
+ SkolemManager* sm = nm->getSkolemManager();
Trace("sort-inference-debug2") << "Simplify " << n << ", type context=" << tnn << std::endl;
std::vector< Node > children;
std::map< Node, std::map< TypeNode, Node > > new_visited;
new_children.push_back( v );
var_bound[ n[0][i] ] = v;
}
- children.push_back( NodeManager::currentNM()->mkNode( n[0].getKind(), new_children ) );
+ children.push_back(nm->mkNode(n[0].getKind(), new_children));
use_new_visited = true;
}
Trace("sort-inference-debug2") << "Remove bound for " << n[0][i] << std::endl;
var_bound.erase( n[0][i] );
}
- ret = NodeManager::currentNM()->mkNode( n.getKind(), children );
+ ret = nm->mkNode(n.getKind(), children);
}else if( n.getKind()==kind::EQUAL ){
TypeNode tn1 = children[0].getType();
TypeNode tn2 = children[1].getType();
Trace("sort-inference-warn") << " Types : " << children[0].getType() << " " << children[1].getType() << std::endl;
Assert(false);
}
- ret = NodeManager::currentNM()->mkNode( kind::EQUAL, children );
+ ret = nm->mkNode(kind::EQUAL, children);
}
else if (isHandledApplyUf(n.getKind()))
{
if( opChanged ){
std::stringstream ss;
ss << "io_" << op;
- TypeNode typ = NodeManager::currentNM()->mkFunctionType( argTypes, retType );
- d_symbol_map[op] = NodeManager::currentNM()->mkSkolem( ss.str(), typ, "op created during sort inference" );
+ TypeNode typ = nm->mkFunctionType(argTypes, retType);
+ d_symbol_map[op] = sm->mkDummySkolem(
+ ss.str(), typ, "op created during sort inference");
Trace("setp-model") << "Function " << op << " is replaced with " << d_symbol_map[op] << std::endl;
model_replace_f[op] = d_symbol_map[op];
}else{
Assert(false);
}
}
- ret = NodeManager::currentNM()->mkNode( kind::APPLY_UF, children );
+ ret = nm->mkNode(kind::APPLY_UF, children);
}else{
std::map< Node, Node >::iterator it = var_bound.find( n );
if( it!=var_bound.end() ){
//type is determined by context
ret = getNewSymbol( n, tnn );
}else if( childChanged ){
- ret = NodeManager::currentNM()->mkNode( n.getKind(), children );
+ ret = nm->mkNode(n.getKind(), children);
}else{
ret = n;
}
}
Node SortInference::mkInjection( TypeNode tn1, TypeNode tn2 ) {
+ NodeManager* nm = NodeManager::currentNM();
+ SkolemManager* sm = nm->getSkolemManager();
std::vector< TypeNode > tns;
tns.push_back( tn1 );
- TypeNode typ = NodeManager::currentNM()->mkFunctionType( tns, tn2 );
- Node f = NodeManager::currentNM()->mkSkolem( "inj", typ, "injection for monotonicity constraint" );
+ TypeNode typ = nm->mkFunctionType(tns, tn2);
+ Node f =
+ sm->mkDummySkolem("inj", typ, "injection for monotonicity constraint");
Trace("sort-inference") << "-> Make injection " << f << " from " << tn1 << " to " << tn2 << std::endl;
- Node v1 = NodeManager::currentNM()->mkBoundVar( "?x", tn1 );
- Node v2 = NodeManager::currentNM()->mkBoundVar( "?y", tn1 );
- Node ret = NodeManager::currentNM()->mkNode( kind::FORALL,
- NodeManager::currentNM()->mkNode( kind::BOUND_VAR_LIST, v1, v2 ),
- NodeManager::currentNM()->mkNode( kind::OR,
- NodeManager::currentNM()->mkNode( kind::APPLY_UF, f, v1 ).eqNode( NodeManager::currentNM()->mkNode( kind::APPLY_UF, f, v2 ) ).negate(),
- v1.eqNode( v2 ) ) );
+ Node v1 = nm->mkBoundVar("?x", tn1);
+ Node v2 = nm->mkBoundVar("?y", tn1);
+ Node ret =
+ nm->mkNode(kind::FORALL,
+ nm->mkNode(kind::BOUND_VAR_LIST, v1, v2),
+ nm->mkNode(kind::OR,
+ nm->mkNode(kind::APPLY_UF, f, v1)
+ .eqNode(nm->mkNode(kind::APPLY_UF, f, v2))
+ .negate(),
+ v1.eqNode(v2)));
ret = theory::Rewriter::rewrite( ret );
return ret;
}
int ret = 1;
retNode = d_emptyRegexp;
NodeManager* nm = NodeManager::currentNM();
+ SkolemManager* sm = nm->getSkolemManager();
PairNodeStr dv = std::make_pair( r, c );
if( d_deriv_cache.find( dv ) != d_deriv_cache.end() ) {
}
}
if(ret == 0) {
- Node sk = NodeManager::currentNM()->mkSkolem( "rsp", NodeManager::currentNM()->stringType(), "Split RegExp" );
+ Node sk =
+ sm->mkDummySkolem("rsp", nm->stringType(), "Split RegExp");
retNode = NodeManager::currentNM()->mkNode(kind::STRING_TO_REGEXP, sk);
if(!rest.isNull()) {
retNode = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::REGEXP_CONCAT, retNode, rest));
Node SkolemCache::mkSkolem(const char* c)
{
// TODO: eliminate this
- Node n = NodeManager::currentNM()->mkSkolem(c, d_strType, "string skolem");
+ SkolemManager* sm = NodeManager::currentNM()->getSkolemManager();
+ Node n = sm->mkDummySkolem(c, d_strType, "string skolem");
d_allSkolems.insert(n);
return n;
}
#include "theory/strings/theory_strings_preprocess.h"
#include "expr/kind.h"
+#include "expr/skolem_manager.h"
#include "options/smt_options.h"
#include "options/strings_options.h"
#include "proof/proof_manager.h"
<< "StringsPreprocess::reduce: " << t << std::endl;
Node retNode = t;
NodeManager* nm = NodeManager::currentNM();
+ SkolemManager* sm = nm->getSkolemManager();
Node zero = nm->mkConst(Rational(0));
Node one = nm->mkConst(Rational(1));
Node negOne = nm->mkConst(Rational(-1));
std::vector<Node> conc;
std::vector< TypeNode > argTypes;
argTypes.push_back(nm->integerType());
- Node u = nm->mkSkolem("U", nm->mkFunctionType(argTypes, nm->integerType()));
+ Node u =
+ sm->mkDummySkolem("U", nm->mkFunctionType(argTypes, nm->integerType()));
Node lem = nm->mkNode(GEQ, leni, one);
conc.push_back(lem);
Node emp = Word::mkEmptyWord(s.getType());
Node sEmpty = s.eqNode(emp);
- Node k = nm->mkSkolem("k", nm->integerType());
+ Node k = sm->mkDummySkolem("k", nm->integerType());
Node kc1 = nm->mkNode(GEQ, k, zero);
Node kc2 = nm->mkNode(LT, k, lens);
Node c0 = nm->mkNode(STRING_TO_CODE, nm->mkConst(String("0")));
std::vector<Node> conc2;
std::vector< TypeNode > argTypes;
argTypes.push_back(nm->integerType());
- Node u = nm->mkSkolem("U", nm->mkFunctionType(argTypes, nm->integerType()));
+ Node u =
+ sm->mkDummySkolem("U", nm->mkFunctionType(argTypes, nm->integerType()));
lem = stoit.eqNode(nm->mkNode(APPLY_UF, u, lens));
conc2.push_back(lem);
std::vector<TypeNode> argTypes;
argTypes.push_back(nm->integerType());
Node us =
- nm->mkSkolem("Us", nm->mkFunctionType(argTypes, nm->stringType()));
+ sm->mkDummySkolem("Us", nm->mkFunctionType(argTypes, nm->stringType()));
TypeNode ufType = nm->mkFunctionType(argTypes, nm->integerType());
Node uf = sc->mkTypedSkolemCached(
ufType, x, y, SkolemCache::SK_OCCUR_INDEX, "Uf");
nm->integerType(), x, y, SkolemCache::SK_NUM_OCCUR, "numOcc");
std::vector<TypeNode> argTypes;
argTypes.push_back(nm->integerType());
- Node us = nm->mkSkolem("Us", nm->mkFunctionType(argTypes, t.getType()));
+ Node us =
+ sm->mkDummySkolem("Us", nm->mkFunctionType(argTypes, t.getType()));
TypeNode ufType = nm->mkFunctionType(argTypes, nm->integerType());
Node uf = sc->mkTypedSkolemCached(
ufType, x, y, SkolemCache::SK_OCCUR_INDEX, "Uf");
}
else
{
- qvar = nm->mkSkolem("qinternal", nm->booleanType());
+ SkolemManager* sm = nm->getSkolemManager();
+ qvar = sm->mkDummySkolem("qinternal", nm->booleanType());
// this dummy variable marks that the quantified formula is internal
qvar.setAttribute(InternalQuantAttribute(), true);
// remember the dummy variable
#include <sstream>
+#include "expr/skolem_manager.h"
#include "options/smt_options.h"
#include "options/uf_options.h"
#include "smt/logic_exception.h"
bool SortModel::checkLastCall()
{
+ NodeManager* nm = NodeManager::currentNM();
+ SkolemManager* sm = nm->getSkolemManager();
TheoryModel* m = d_state.getModel();
if( Trace.isOn("uf-ss-warn") ){
std::vector< Node > eqcs;
{
std::stringstream ss;
ss << "r_" << d_type << "_";
- Node nn = NodeManager::currentNM()->mkSkolem(
+ Node nn = sm->mkDummySkolem(
ss.str(), d_type, "enumeration to meet negative card constraint");
d_fresh_aloc_reps.push_back( nn );
}
}
}
Node cl = getCardinalityLiteral( d_maxNegCard );
- Node lem = NodeManager::currentNM()->mkNode(
- OR, cl, NodeManager::currentNM()->mkAnd(force_cl));
+ Node lem = nm->mkNode(OR, cl, nm->mkAnd(force_cl));
Trace("uf-ss-lemma") << "*** Enforce negative cardinality constraint lemma : " << lem << std::endl;
d_im.lemma(lem, InferenceId::UF_CARD_ENFORCE_NEGATIVE);
return false;
#include "theory/uf/ho_extension.h"
#include "expr/node_algorithm.h"
+#include "expr/skolem_manager.h"
#include "options/uf_options.h"
#include "theory/theory_model.h"
#include "theory/uf/theory_uf_rewriter.h"
std::vector<TypeNode> argTypes = tn.getArgTypes();
std::vector<Node> skolems;
NodeManager* nm = NodeManager::currentNM();
+ SkolemManager* sm = nm->getSkolemManager();
for (unsigned i = 0, nargs = argTypes.size(); i < nargs; i++)
{
- Node k =
- nm->mkSkolem("k", argTypes[i], "skolem created for extensionality.");
+ Node k = sm->mkDummySkolem(
+ "k", argTypes[i], "skolem created for extensionality.");
skolems.push_back(k);
}
Node t[2];
Node f = TheoryUfRewriter::decomposeHoApply(node, args, true);
Node new_f = f;
NodeManager* nm = NodeManager::currentNM();
+ SkolemManager* sm = nm->getSkolemManager();
if (!TheoryUfRewriter::canUseAsApplyUfOperator(f))
{
NodeNodeMap::const_iterator itus = d_uf_std_skolem.find(f);
newTypes.insert(newTypes.end(), argTypes.begin(), argTypes.end());
TypeNode nft = nm->mkFunctionType(newTypes, rangeType);
- new_f = nm->mkSkolem("app_uf", nft);
+ new_f = sm->mkDummySkolem("app_uf", nft);
for (const Node& v : vs)
{
new_f = nm->mkNode(HO_APPLY, new_f, v);
else
{
// introduce skolem to make a standard APPLY_UF
- new_f = nm->mkSkolem("app_uf", f.getType());
+ new_f = sm->mkDummySkolem("app_uf", f.getType());
lem = new_f.eqNode(f);
}
Trace("uf-ho-lemma")
TEST_F(TestNodeBlackAttribute, ints)
{
TypeNode booleanType = d_nodeManager->booleanType();
- Node* node = new Node(d_nodeManager->mkSkolem("b", booleanType));
+ Node* node = new Node(d_skolemManager->mkDummySkolem("b", booleanType));
const uint64_t val = 63489;
uint64_t data0 = 0;
uint64_t data1 = 0;
TEST_F(TestNodeBlackAttribute, tnodes)
{
TypeNode booleanType = d_nodeManager->booleanType();
- Node* node = new Node(d_nodeManager->mkSkolem("b", booleanType));
+ Node* node = new Node(d_skolemManager->mkDummySkolem("b", booleanType));
- Node val(d_nodeManager->mkSkolem("b", booleanType));
+ Node val(d_skolemManager->mkDummySkolem("b", booleanType));
TNode data0;
TNode data1;
TEST_F(TestNodeBlackAttribute, strings)
{
TypeNode booleanType = d_nodeManager->booleanType();
- Node* node = new Node(d_nodeManager->mkSkolem("b", booleanType));
+ Node* node = new Node(d_skolemManager->mkDummySkolem("b", booleanType));
std::string val("63489");
std::string data0;
TEST_F(TestNodeBlackAttribute, bools)
{
TypeNode booleanType = d_nodeManager->booleanType();
- Node* node = new Node(d_nodeManager->mkSkolem("b", booleanType));
+ Node* node = new Node(d_skolemManager->mkDummySkolem("b", booleanType));
bool val = true;
bool data0 = false;
TEST_F(TestNodeBlackNodeAlgorithm, get_symbols1)
{
// The only symbol in ~x (x is a boolean varible) should be x
- Node x = d_nodeManager->mkSkolem("x", d_nodeManager->booleanType());
+ Node x = d_skolemManager->mkDummySkolem("x", d_nodeManager->booleanType());
Node n = d_nodeManager->mkNode(NOT, x);
std::unordered_set<Node, NodeHashFunction> syms;
getSymbols(n, syms);
// "var" is bound.
// left conjunct
- Node x = d_nodeManager->mkSkolem("x", d_nodeManager->integerType());
- Node y = d_nodeManager->mkSkolem("y", d_nodeManager->integerType());
+ Node x = d_skolemManager->mkDummySkolem("x", d_nodeManager->integerType());
+ Node y = d_skolemManager->mkDummySkolem("y", d_nodeManager->integerType());
Node left = d_nodeManager->mkNode(EQUAL, x, y);
// right conjunct
std::map<TypeNode, std::unordered_set<Node, NodeHashFunction> >();
// create test formula
- Node x = d_nodeManager->mkSkolem("x", d_nodeManager->integerType());
+ Node x = d_skolemManager->mkDummySkolem("x", d_nodeManager->integerType());
Node plus = d_nodeManager->mkNode(PLUS, x, x);
Node mul = d_nodeManager->mkNode(MULT, x, x);
Node eq1 = d_nodeManager->mkNode(EQUAL, plus, mul);
- Node y = d_nodeManager->mkSkolem("y", d_nodeManager->mkBitVectorType(4));
+ Node y =
+ d_skolemManager->mkDummySkolem("y", d_nodeManager->mkBitVectorType(4));
Node ext1 = theory::bv::utils::mkExtract(y, 1, 0);
Node ext2 = theory::bv::utils::mkExtract(y, 3, 2);
Node eq2 = d_nodeManager->mkNode(EQUAL, ext1, ext2);
Node two = d_nodeManager->mkConst(Rational(2));
Node x = d_nodeManager->mkBoundVar(integer);
- Node a = d_nodeManager->mkSkolem("a", integer);
+ Node a = d_skolemManager->mkDummySkolem("a", integer);
Node n1 = d_nodeManager->mkNode(MULT, two, x);
std::unordered_map<Node, Node, NodeHashFunction> subs;
#include "expr/node_builder.h"
#include "expr/node_manager.h"
#include "expr/node_value.h"
+#include "expr/skolem_manager.h"
#include "smt/smt_engine.h"
#include "test_node.h"
#include "theory/rewriter.h"
TypeNode type)
{
std::vector<Node> skolems;
+ SkolemManager* sm = nodeManager->getSkolemManager();
for (uint32_t i = 0; i < n; i++)
{
- skolems.push_back(nodeManager->mkSkolem(
- "skolem_", type, "Created by makeNSkolemNodes()"));
+ skolems.push_back(
+ sm->mkDummySkolem("skolem_", type, "Created by makeNSkolemNodes()"));
}
return skolems;
}
{
Node a, b, c;
- b = d_nodeManager->mkSkolem("b", d_nodeManager->booleanType());
+ b = d_skolemManager->mkDummySkolem("b", d_nodeManager->booleanType());
a = b;
c = a;
- Node d = d_nodeManager->mkSkolem("d", d_nodeManager->booleanType());
+ Node d = d_skolemManager->mkDummySkolem("d", d_nodeManager->booleanType());
ASSERT_TRUE(a == a);
ASSERT_TRUE(a == b);
{
Node a, b, c;
- b = d_nodeManager->mkSkolem("b", d_nodeManager->booleanType());
+ b = d_skolemManager->mkDummySkolem("b", d_nodeManager->booleanType());
a = b;
c = a;
- Node d = d_nodeManager->mkSkolem("d", d_nodeManager->booleanType());
+ Node d = d_skolemManager->mkDummySkolem("d", d_nodeManager->booleanType());
/*structed assuming operator == works */
ASSERT_TRUE(iff(a != a, !(a == a)));
{
Node a, b;
Node c = d_nodeManager->mkNode(
- NOT, d_nodeManager->mkSkolem("c", d_nodeManager->booleanType()));
+ NOT, d_skolemManager->mkDummySkolem("c", d_nodeManager->booleanType()));
b = c;
ASSERT_EQ(b, c);
// We don't have access to the ids so we can't test the implementation
// in the black box tests.
- Node a = d_nodeManager->mkSkolem("a", d_nodeManager->booleanType());
- Node b = d_nodeManager->mkSkolem("b", d_nodeManager->booleanType());
+ Node a = d_skolemManager->mkDummySkolem("a", d_nodeManager->booleanType());
+ Node b = d_skolemManager->mkDummySkolem("b", d_nodeManager->booleanType());
ASSERT_TRUE(a < b || b < a);
ASSERT_TRUE(!(a < b && b < a));
TEST_F(TestNodeBlackNode, eqNode)
{
TypeNode t = d_nodeManager->mkSort();
- Node left = d_nodeManager->mkSkolem("left", t);
- Node right = d_nodeManager->mkSkolem("right", t);
+ Node left = d_skolemManager->mkDummySkolem("left", t);
+ Node right = d_skolemManager->mkDummySkolem("right", t);
Node eq = left.eqNode(right);
ASSERT_EQ(EQUAL, eq.getKind());
TEST_F(TestNodeBlackNode, iteNode)
{
- Node a = d_nodeManager->mkSkolem("a", d_nodeManager->booleanType());
- Node b = d_nodeManager->mkSkolem("b", d_nodeManager->booleanType());
+ Node a = d_skolemManager->mkDummySkolem("a", d_nodeManager->booleanType());
+ Node b = d_skolemManager->mkDummySkolem("b", d_nodeManager->booleanType());
Node cnd = d_nodeManager->mkNode(OR, a, b);
Node thenBranch = d_nodeManager->mkConst(true);
TEST_F(TestNodeBlackNode, getKind)
{
- Node a = d_nodeManager->mkSkolem("a", d_nodeManager->booleanType());
- Node b = d_nodeManager->mkSkolem("b", d_nodeManager->booleanType());
+ Node a = d_skolemManager->mkDummySkolem("a", d_nodeManager->booleanType());
+ Node b = d_skolemManager->mkDummySkolem("b", d_nodeManager->booleanType());
Node n = d_nodeManager->mkNode(NOT, a);
ASSERT_EQ(NOT, n.getKind());
n = d_nodeManager->mkNode(EQUAL, a, b);
ASSERT_EQ(EQUAL, n.getKind());
- Node x = d_nodeManager->mkSkolem("x", d_nodeManager->realType());
- Node y = d_nodeManager->mkSkolem("y", d_nodeManager->realType());
+ Node x = d_skolemManager->mkDummySkolem("x", d_nodeManager->realType());
+ Node y = d_skolemManager->mkDummySkolem("y", d_nodeManager->realType());
n = d_nodeManager->mkNode(PLUS, x, y);
ASSERT_EQ(PLUS, n.getKind());
TypeNode booleanType = d_nodeManager->booleanType();
TypeNode predType = d_nodeManager->mkFunctionType(sort, booleanType);
- Node f = d_nodeManager->mkSkolem("f", predType);
- Node a = d_nodeManager->mkSkolem("a", sort);
+ Node f = d_skolemManager->mkDummySkolem("f", predType);
+ Node a = d_skolemManager->mkDummySkolem("a", sort);
Node fa = d_nodeManager->mkNode(kind::APPLY_UF, f, a);
ASSERT_TRUE(fa.hasOperator());
TEST_F(TestNodeBlackNode, iterator)
{
NodeBuilder b;
- Node x = d_nodeManager->mkSkolem("x", d_nodeManager->booleanType());
- Node y = d_nodeManager->mkSkolem("y", d_nodeManager->booleanType());
- Node z = d_nodeManager->mkSkolem("z", d_nodeManager->booleanType());
+ Node x = d_skolemManager->mkDummySkolem("x", d_nodeManager->booleanType());
+ Node y = d_skolemManager->mkDummySkolem("y", d_nodeManager->booleanType());
+ Node z = d_skolemManager->mkDummySkolem("z", d_nodeManager->booleanType());
Node n = b << x << y << z << kind::AND;
{ // iterator
{
TypeNode integerType = d_nodeManager->integerType();
- Node x = d_nodeManager->mkSkolem("x", integerType);
- Node y = d_nodeManager->mkSkolem("y", integerType);
- Node z = d_nodeManager->mkSkolem("z", integerType);
+ Node x = d_skolemManager->mkDummySkolem("x", integerType);
+ Node y = d_skolemManager->mkDummySkolem("y", integerType);
+ Node z = d_skolemManager->mkDummySkolem("z", integerType);
Node plus_x_y_z = d_nodeManager->mkNode(kind::PLUS, x, y, z);
Node x_minus_y = d_nodeManager->mkNode(kind::MINUS, x, y);
{
TypeNode booleanType = d_nodeManager->booleanType();
- Node w = d_nodeManager->mkSkolem(
+ Node w = d_skolemManager->mkDummySkolem(
"w", booleanType, "", NodeManager::SKOLEM_EXACT_NAME);
- Node x = d_nodeManager->mkSkolem(
+ Node x = d_skolemManager->mkDummySkolem(
"x", booleanType, "", NodeManager::SKOLEM_EXACT_NAME);
- Node y = d_nodeManager->mkSkolem(
+ Node y = d_skolemManager->mkDummySkolem(
"y", booleanType, "", NodeManager::SKOLEM_EXACT_NAME);
- Node z = d_nodeManager->mkSkolem(
+ Node z = d_skolemManager->mkDummySkolem(
"z", booleanType, "", NodeManager::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_nodeManager->mkSkolem(
+ Node w = d_skolemManager->mkDummySkolem(
"w", booleanType, "", NodeManager::SKOLEM_EXACT_NAME);
- Node x = d_nodeManager->mkSkolem(
+ Node x = d_skolemManager->mkDummySkolem(
"x", booleanType, "", NodeManager::SKOLEM_EXACT_NAME);
- Node y = d_nodeManager->mkSkolem(
+ Node y = d_skolemManager->mkDummySkolem(
"y", booleanType, "", NodeManager::SKOLEM_EXACT_NAME);
- Node z = d_nodeManager->mkSkolem(
+ Node z = d_skolemManager->mkDummySkolem(
"z", booleanType, "", NodeManager::SKOLEM_EXACT_NAME);
Node m = NodeBuilder() << x << y << kind::OR;
Node n = NodeBuilder() << w << m << z << kind::AND;
TypeNode intType = d_nodeManager->integerType();
TypeNode fnType = d_nodeManager->mkFunctionType(intType, intType);
- Node x =
- d_nodeManager->mkSkolem("x", intType, "", NodeManager::SKOLEM_EXACT_NAME);
- Node y =
- d_nodeManager->mkSkolem("y", intType, "", NodeManager::SKOLEM_EXACT_NAME);
- Node f =
- d_nodeManager->mkSkolem("f", fnType, "", NodeManager::SKOLEM_EXACT_NAME);
- Node g =
- d_nodeManager->mkSkolem("g", fnType, "", NodeManager::SKOLEM_EXACT_NAME);
+ Node x = d_skolemManager->mkDummySkolem(
+ "x", intType, "", NodeManager::SKOLEM_EXACT_NAME);
+ Node y = d_skolemManager->mkDummySkolem(
+ "y", intType, "", NodeManager::SKOLEM_EXACT_NAME);
+ Node f = d_skolemManager->mkDummySkolem(
+ "f", fnType, "", NodeManager::SKOLEM_EXACT_NAME);
+ Node g = d_skolemManager->mkDummySkolem(
+ "g", fnType, "", NodeManager::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);
listType.getDType().getConstructors();
Node cons = lcons[0]->getConstructor();
Node nil = lcons[1]->getConstructor();
- Node x = d_nodeManager->mkSkolem("x", d_nodeManager->integerType());
+ Node x = d_skolemManager->mkDummySkolem("x", d_nodeManager->integerType());
Node cons_x_nil =
d_nodeManager->mkNode(APPLY_CONSTRUCTOR,
cons,
namespace {
Node level0(NodeManager* nm)
{
+ SkolemManager* sm = nm->getSkolemManager();
NodeBuilder nb(kind::AND);
- Node x = nm->mkSkolem("x", nm->booleanType());
+ Node x = sm->mkDummySkolem("x", nm->booleanType());
nb << x;
nb << x;
return Node(nb.constructNode());
NodeBuilder noKind;
ASSERT_EQ(noKind.getKind(), UNDEFINED_KIND);
- Node x(d_nodeManager->mkSkolem("x", *d_intTypeNode));
+ Node x(d_skolemManager->mkDummySkolem("x", *d_intTypeNode));
noKind << x << x;
ASSERT_EQ(noKind.getKind(), UNDEFINED_KIND);
TEST_F(TestNodeBlackNodeBuilder, getNumChildren)
{
- Node x(d_nodeManager->mkSkolem("x", *d_intTypeNode));
+ Node x(d_skolemManager->mkDummySkolem("x", *d_intTypeNode));
NodeBuilder nb;
#ifdef CVC4_ASSERTIONS
TEST_F(TestNodeBlackNodeBuilder, append)
{
- Node x = d_nodeManager->mkSkolem("x", *d_boolTypeNode);
- Node y = d_nodeManager->mkSkolem("y", *d_boolTypeNode);
- Node z = d_nodeManager->mkSkolem("z", *d_boolTypeNode);
+ Node x = d_skolemManager->mkDummySkolem("x", *d_boolTypeNode);
+ Node y = d_skolemManager->mkDummySkolem("y", *d_boolTypeNode);
+ Node z = d_skolemManager->mkDummySkolem("z", *d_boolTypeNode);
Node m = d_nodeManager->mkNode(AND, y, z, x);
Node n = d_nodeManager->mkNode(OR, d_nodeManager->mkNode(NOT, x), y, z);
Node o = d_nodeManager->mkNode(XOR, y, x);
- Node r = d_nodeManager->mkSkolem("r", *d_realTypeNode);
- Node s = d_nodeManager->mkSkolem("s", *d_realTypeNode);
- Node t = d_nodeManager->mkSkolem("t", *d_realTypeNode);
+ Node r = d_skolemManager->mkDummySkolem("r", *d_realTypeNode);
+ Node s = d_skolemManager->mkDummySkolem("s", *d_realTypeNode);
+ Node t = d_skolemManager->mkDummySkolem("t", *d_realTypeNode);
Node p = d_nodeManager->mkNode(
EQUAL,
{
NodeBuilder nb;
- Node a = d_nodeManager->mkSkolem("a", *d_boolTypeNode);
+ Node a = d_skolemManager->mkDummySkolem("a", *d_boolTypeNode);
- Node b = d_nodeManager->mkSkolem("b", *d_boolTypeNode);
- Node c = d_nodeManager->mkSkolem("c", *d_boolTypeNode);
+ Node b = d_skolemManager->mkDummySkolem("b", *d_boolTypeNode);
+ Node c = d_skolemManager->mkDummySkolem("c", *d_boolTypeNode);
- Node d = d_nodeManager->mkSkolem("d", *d_realTypeNode);
- Node e = d_nodeManager->mkSkolem("e", *d_realTypeNode);
+ Node d = d_skolemManager->mkDummySkolem("d", *d_realTypeNode);
+ Node e = d_skolemManager->mkDummySkolem("e", *d_realTypeNode);
nb << a << NOT << b << c << OR << c << a << AND << d << e << ITE;
TEST_F(TestNodeBlackNodeManager, mkNode_not)
{
- Node x = d_nodeManager->mkSkolem("x", d_nodeManager->booleanType());
+ Node x = d_skolemManager->mkDummySkolem("x", d_nodeManager->booleanType());
Node n = d_nodeManager->mkNode(NOT, x);
ASSERT_EQ(n.getNumChildren(), 1u);
ASSERT_EQ(n.getKind(), NOT);
TEST_F(TestNodeBlackNodeManager, mkNode_binary)
{
- Node x = d_nodeManager->mkSkolem("x", d_nodeManager->booleanType());
- Node y = d_nodeManager->mkSkolem("y", d_nodeManager->booleanType());
+ Node x = d_skolemManager->mkDummySkolem("x", d_nodeManager->booleanType());
+ Node y = d_skolemManager->mkDummySkolem("y", d_nodeManager->booleanType());
Node n = d_nodeManager->mkNode(IMPLIES, x, y);
ASSERT_EQ(n.getNumChildren(), 2u);
ASSERT_EQ(n.getKind(), IMPLIES);
TEST_F(TestNodeBlackNodeManager, mkNode_three_children)
{
- Node x = d_nodeManager->mkSkolem("x", d_nodeManager->booleanType());
- Node y = d_nodeManager->mkSkolem("y", d_nodeManager->booleanType());
- Node z = d_nodeManager->mkSkolem("z", d_nodeManager->booleanType());
+ Node x = d_skolemManager->mkDummySkolem("x", d_nodeManager->booleanType());
+ Node y = d_skolemManager->mkDummySkolem("y", d_nodeManager->booleanType());
+ Node z = d_skolemManager->mkDummySkolem("z", d_nodeManager->booleanType());
Node n = d_nodeManager->mkNode(AND, x, y, z);
ASSERT_EQ(n.getNumChildren(), 3u);
ASSERT_EQ(n.getKind(), AND);
TEST_F(TestNodeBlackNodeManager, mkNode_four_children)
{
- Node x1 = d_nodeManager->mkSkolem("x1", d_nodeManager->booleanType());
- Node x2 = d_nodeManager->mkSkolem("x2", d_nodeManager->booleanType());
- Node x3 = d_nodeManager->mkSkolem("x3", d_nodeManager->booleanType());
- Node x4 = d_nodeManager->mkSkolem("x4", d_nodeManager->booleanType());
+ Node x1 = d_skolemManager->mkDummySkolem("x1", d_nodeManager->booleanType());
+ Node x2 = d_skolemManager->mkDummySkolem("x2", d_nodeManager->booleanType());
+ Node x3 = d_skolemManager->mkDummySkolem("x3", d_nodeManager->booleanType());
+ Node x4 = d_skolemManager->mkDummySkolem("x4", d_nodeManager->booleanType());
Node n = d_nodeManager->mkNode(AND, x1, x2, x3, x4);
ASSERT_EQ(n.getNumChildren(), 4u);
ASSERT_EQ(n.getKind(), AND);
TEST_F(TestNodeBlackNodeManager, mkNode_five_children)
{
- Node x1 = d_nodeManager->mkSkolem("x1", d_nodeManager->booleanType());
- Node x2 = d_nodeManager->mkSkolem("x2", d_nodeManager->booleanType());
- Node x3 = d_nodeManager->mkSkolem("x3", d_nodeManager->booleanType());
- Node x4 = d_nodeManager->mkSkolem("x4", d_nodeManager->booleanType());
- Node x5 = d_nodeManager->mkSkolem("x5", d_nodeManager->booleanType());
+ Node x1 = d_skolemManager->mkDummySkolem("x1", d_nodeManager->booleanType());
+ Node x2 = d_skolemManager->mkDummySkolem("x2", d_nodeManager->booleanType());
+ Node x3 = d_skolemManager->mkDummySkolem("x3", d_nodeManager->booleanType());
+ Node x4 = d_skolemManager->mkDummySkolem("x4", d_nodeManager->booleanType());
+ Node x5 = d_skolemManager->mkDummySkolem("x5", d_nodeManager->booleanType());
Node n = d_nodeManager->mkNode(AND, x1, x2, x3, x4, x5);
ASSERT_EQ(n.getNumChildren(), 5u);
ASSERT_EQ(n.getKind(), AND);
TEST_F(TestNodeBlackNodeManager, mkNode_vector_of_node)
{
- Node x1 = d_nodeManager->mkSkolem("x1", d_nodeManager->booleanType());
- Node x2 = d_nodeManager->mkSkolem("x2", d_nodeManager->booleanType());
- Node x3 = d_nodeManager->mkSkolem("x3", d_nodeManager->booleanType());
+ Node x1 = d_skolemManager->mkDummySkolem("x1", d_nodeManager->booleanType());
+ Node x2 = d_skolemManager->mkDummySkolem("x2", d_nodeManager->booleanType());
+ Node x3 = d_skolemManager->mkDummySkolem("x3", d_nodeManager->booleanType());
std::vector<Node> args;
args.push_back(x1);
args.push_back(x2);
TEST_F(TestNodeBlackNodeManager, mkNode_vector_of_tnode)
{
- Node x1 = d_nodeManager->mkSkolem("x1", d_nodeManager->booleanType());
- Node x2 = d_nodeManager->mkSkolem("x2", d_nodeManager->booleanType());
- Node x3 = d_nodeManager->mkSkolem("x3", d_nodeManager->booleanType());
+ Node x1 = d_skolemManager->mkDummySkolem("x1", d_nodeManager->booleanType());
+ Node x2 = d_skolemManager->mkDummySkolem("x2", d_nodeManager->booleanType());
+ Node x3 = d_skolemManager->mkDummySkolem("x3", d_nodeManager->booleanType());
std::vector<TNode> args;
args.push_back(x1);
args.push_back(x2);
TEST_F(TestNodeBlackNodeManager, mkSkolem_with_name)
{
- Node x = d_nodeManager->mkSkolem(
+ Node x = d_skolemManager->mkDummySkolem(
"x", *d_boolTypeNode, "", NodeManager::SKOLEM_EXACT_NAME);
ASSERT_EQ(x.getKind(), SKOLEM);
ASSERT_EQ(x.getNumChildren(), 0u);
TEST_F(TestNodeBlackNodeManager, mkNode_too_few_children)
{
#ifdef CVC4_ASSERTIONS
- Node x = d_nodeManager->mkSkolem("x", d_nodeManager->booleanType());
+ Node x = d_skolemManager->mkDummySkolem("x", d_nodeManager->booleanType());
ASSERT_DEATH(d_nodeManager->mkNode(AND, x),
"Nodes with kind AND must have at least 2 children");
#endif
std::vector<Node> vars;
const uint32_t max = metakind::getMaxArityForKind(AND);
TypeNode boolType = d_nodeManager->booleanType();
- Node skolem_i = d_nodeManager->mkSkolem("i", boolType);
- Node skolem_j = d_nodeManager->mkSkolem("j", boolType);
+ Node skolem_i = d_skolemManager->mkDummySkolem("i", boolType);
+ Node skolem_j = d_skolemManager->mkDummySkolem("j", boolType);
Node andNode = skolem_i.andNode(skolem_j);
Node orNode = skolem_i.orNode(skolem_j);
while (vars.size() <= max)
TEST_F(TestNodeWhiteNodeManager, topological_sort)
{
TypeNode boolType = d_nodeManager->booleanType();
- Node i = d_nodeManager->mkSkolem("i", boolType);
- Node j = d_nodeManager->mkSkolem("j", boolType);
+ Node i = d_skolemManager->mkDummySkolem("i", boolType);
+ Node j = d_skolemManager->mkDummySkolem("j", boolType);
Node n1 = d_nodeManager->mkNode(kind::AND, j, j);
Node n2 = d_nodeManager->mkNode(kind::AND, i, n1);
TEST_F(TestNodeBlackNodeSelfIterator, iteration)
{
- Node x = d_nodeManager->mkSkolem("x", *d_boolTypeNode);
- Node y = d_nodeManager->mkSkolem("y", *d_boolTypeNode);
+ Node x = d_skolemManager->mkDummySkolem("x", *d_boolTypeNode);
+ Node y = d_skolemManager->mkDummySkolem("y", *d_boolTypeNode);
Node x_and_y = x.andNode(y);
NodeSelfIterator i = x_and_y, j = NodeSelfIterator::self(x_and_y);
ASSERT_NE(i, x_and_y.end());
#define CVC4__TEST__UNIT__TEST_NODE_H
#include "expr/node_manager.h"
+#include "expr/skolem_manager.h"
#include "smt/smt_engine.h"
#include "smt/smt_engine_scope.h"
#include "test.h"
void SetUp() override
{
d_nodeManager.reset(new NodeManager());
+ d_skolemManager = d_nodeManager->getSkolemManager();
d_scope.reset(new NodeManagerScope(d_nodeManager.get()));
d_boolTypeNode.reset(new TypeNode(d_nodeManager->booleanType()));
d_bvTypeNode.reset(new TypeNode(d_nodeManager->mkBitVectorType(2)));
std::unique_ptr<NodeManagerScope> d_scope;
std::unique_ptr<NodeManager> d_nodeManager;
+ SkolemManager* d_skolemManager;
std::unique_ptr<TypeNode> d_boolTypeNode;
std::unique_ptr<TypeNode> d_bvTypeNode;
std::unique_ptr<TypeNode> d_intTypeNode;
#include "expr/node.h"
#include "expr/node_manager.h"
#include "expr/proof_checker.h"
+#include "expr/skolem_manager.h"
#include "smt/smt_engine.h"
#include "smt/smt_engine_scope.h"
#include "test.h"
void SetUp() override
{
d_nodeManager.reset(new NodeManager());
+ d_skolemManager = d_nodeManager->getSkolemManager();
d_nmScope.reset(new NodeManagerScope(d_nodeManager.get()));
d_smtEngine.reset(new SmtEngine(d_nodeManager.get()));
d_smtEngine->finishInit();
std::unique_ptr<NodeManagerScope> d_nmScope;
std::unique_ptr<NodeManager> d_nodeManager;
+ SkolemManager* d_skolemManager;
std::unique_ptr<SmtEngine> d_smtEngine;
};
void SetUp() override
{
d_nodeManager.reset(new NodeManager());
+ d_skolemManager = d_nodeManager->getSkolemManager();
d_nmScope.reset(new NodeManagerScope(d_nodeManager.get()));
d_smtEngine.reset(new SmtEngine(d_nodeManager.get()));
}
std::unique_ptr<NodeManagerScope> d_nmScope;
std::unique_ptr<NodeManager> d_nodeManager;
+ SkolemManager* d_skolemManager;
std::unique_ptr<SmtEngine> d_smtEngine;
};
std::vector<Node> elements(n);
for (size_t i = 0; i < n; i++)
{
- elements[i] = d_nodeManager->mkSkolem("x", d_nodeManager->stringType());
+ elements[i] =
+ d_skolemManager->mkDummySkolem("x", d_nodeManager->stringType());
}
return elements;
}
std::vector<Node> elements = getNStrings(2);
Node x = elements[0];
Node y = elements[1];
- Node c = d_nodeManager->mkSkolem("c", d_nodeManager->integerType());
- Node d = d_nodeManager->mkSkolem("d", d_nodeManager->integerType());
+ Node c = d_skolemManager->mkDummySkolem("c", d_nodeManager->integerType());
+ Node d = d_skolemManager->mkDummySkolem("d", d_nodeManager->integerType());
Node A = d_nodeManager->mkBag(d_nodeManager->stringType(), x, c);
Node B = d_nodeManager->mkBag(d_nodeManager->stringType(), y, d);
Node emptyBag = d_nodeManager->mkConst(
TEST_F(TestTheoryWhiteBagsRewriter, mkBag_variable_element)
{
- Node skolem = d_nodeManager->mkSkolem("x", d_nodeManager->stringType());
+ Node skolem =
+ d_skolemManager->mkDummySkolem("x", d_nodeManager->stringType());
Node variable = d_nodeManager->mkBag(d_nodeManager->stringType(),
skolem,
d_nodeManager->mkConst(Rational(-1)));
TEST_F(TestTheoryWhiteBagsRewriter, bag_count)
{
int n = 3;
- Node skolem = d_nodeManager->mkSkolem("x", d_nodeManager->stringType());
+ Node skolem =
+ d_skolemManager->mkDummySkolem("x", d_nodeManager->stringType());
Node emptyBag = d_nodeManager->mkConst(
EmptyBag(d_nodeManager->mkBagType(skolem.getType())));
Node bag = d_nodeManager->mkBag(
TEST_F(TestTheoryWhiteBagsRewriter, duplicate_removal)
{
- Node x = d_nodeManager->mkSkolem("x", d_nodeManager->stringType());
+ Node x = d_skolemManager->mkDummySkolem("x", d_nodeManager->stringType());
Node bag = d_nodeManager->mkBag(
d_nodeManager->stringType(), x, d_nodeManager->mkConst(Rational(5)));
TEST_F(TestTheoryWhiteBagsRewriter, choose)
{
- Node x = d_nodeManager->mkSkolem("x", d_nodeManager->stringType());
+ Node x = d_skolemManager->mkDummySkolem("x", d_nodeManager->stringType());
Node c = d_nodeManager->mkConst(Rational(3));
Node bag = d_nodeManager->mkBag(d_nodeManager->stringType(), x, c);
TEST_F(TestTheoryWhiteBagsRewriter, bag_card)
{
- Node x = d_nodeManager->mkSkolem("x", d_nodeManager->stringType());
+ Node x = d_skolemManager->mkDummySkolem("x", d_nodeManager->stringType());
Node emptyBag = d_nodeManager->mkConst(
EmptyBag(d_nodeManager->mkBagType(d_nodeManager->stringType())));
Node zero = d_nodeManager->mkConst(Rational(0));
{
Node emptybag = d_nodeManager->mkConst(
EmptyBag(d_nodeManager->mkBagType(d_nodeManager->stringType())));
- Node x = d_nodeManager->mkSkolem("x", d_nodeManager->stringType());
- Node c = d_nodeManager->mkSkolem("c", d_nodeManager->integerType());
+ Node x = d_skolemManager->mkDummySkolem("x", d_nodeManager->stringType());
+ Node c = d_skolemManager->mkDummySkolem("c", d_nodeManager->integerType());
Node bag = d_nodeManager->mkBag(d_nodeManager->stringType(), x, c);
// TODO(projects#223): complete this function
TEST_F(TestTheoryWhiteBagsRewriter, from_set)
{
- Node x = d_nodeManager->mkSkolem("x", d_nodeManager->stringType());
+ Node x = d_skolemManager->mkDummySkolem("x", d_nodeManager->stringType());
Node singleton = d_nodeManager->mkSingleton(d_nodeManager->stringType(), x);
// (bag.from_set (singleton (singleton_op Int) x)) = (mkBag x 1)
TEST_F(TestTheoryWhiteBagsRewriter, to_set)
{
- Node x = d_nodeManager->mkSkolem("x", d_nodeManager->stringType());
+ Node x = d_skolemManager->mkDummySkolem("x", d_nodeManager->stringType());
Node bag = d_nodeManager->mkBag(
d_nodeManager->stringType(), x, d_nodeManager->mkConst(Rational(5)));
d_s = d_nodeManager->mkVar("s", d_nodeManager->mkBitVectorType(4));
d_t = d_nodeManager->mkVar("t", d_nodeManager->mkBitVectorType(4));
- d_sk = d_nodeManager->mkSkolem("sk", d_t.getType());
+ d_sk = d_skolemManager->mkDummySkolem("sk", d_t.getType());
d_x = d_nodeManager->mkBoundVar(d_t.getType());
d_bvarlist = d_nodeManager->mkNode(BOUND_VAR_LIST, {d_x});
}
{
s2 = d_nodeManager->mkVar("s2", d_nodeManager->mkBitVectorType(4));
x = d_nodeManager->mkBoundVar(s2.getType());
- sk = d_nodeManager->mkSkolem("sk", s2.getType());
+ sk = d_skolemManager->mkDummySkolem("sk", s2.getType());
t = d_nodeManager->mkVar("t", d_nodeManager->mkBitVectorType(8));
sv_t = d_nodeManager->mkNode(BITVECTOR_CONCAT, x, s2);
sc = getICBvConcat(pol, litk, 0, sk, sv_t, t);
{
s1 = d_nodeManager->mkVar("s1", d_nodeManager->mkBitVectorType(4));
x = d_nodeManager->mkBoundVar(s1.getType());
- sk = d_nodeManager->mkSkolem("sk", s1.getType());
+ sk = d_skolemManager->mkDummySkolem("sk", s1.getType());
t = d_nodeManager->mkVar("t", d_nodeManager->mkBitVectorType(8));
sv_t = d_nodeManager->mkNode(BITVECTOR_CONCAT, s1, x);
sc = getICBvConcat(pol, litk, 1, sk, sv_t, t);
s1 = d_nodeManager->mkVar("s1", d_nodeManager->mkBitVectorType(4));
s2 = d_nodeManager->mkVar("s2", d_nodeManager->mkBitVectorType(4));
x = d_nodeManager->mkBoundVar(s2.getType());
- sk = d_nodeManager->mkSkolem("sk", s1.getType());
+ sk = d_skolemManager->mkDummySkolem("sk", s1.getType());
t = d_nodeManager->mkVar("t", d_nodeManager->mkBitVectorType(12));
sv_t = d_nodeManager->mkNode(BITVECTOR_CONCAT, s1, x, s2);
sc = getICBvConcat(pol, litk, 1, sk, sv_t, t);
unsigned w = 8;
Node x = d_nodeManager->mkVar("x", d_nodeManager->mkBitVectorType(wx));
- Node sk = d_nodeManager->mkSkolem("sk", x.getType());
+ Node sk = d_skolemManager->mkDummySkolem("sk", x.getType());
x = d_nodeManager->mkBoundVar(x.getType());
Node t = d_nodeManager->mkVar("t", d_nodeManager->mkBitVectorType(w));
TEST_F(TestTheoryBlackStringsSkolemCache, mkSkolemCached)
{
Node zero = d_nodeManager->mkConst(Rational(0));
- Node n = d_nodeManager->mkSkolem("n", d_nodeManager->integerType());
- Node a = d_nodeManager->mkSkolem("a", d_nodeManager->stringType());
- Node b = d_nodeManager->mkSkolem("b", d_nodeManager->stringType());
- Node c = d_nodeManager->mkSkolem("c", d_nodeManager->stringType());
- Node d = d_nodeManager->mkSkolem("d", d_nodeManager->stringType());
+ Node n = d_skolemManager->mkDummySkolem("n", d_nodeManager->integerType());
+ Node a = d_skolemManager->mkDummySkolem("a", d_nodeManager->stringType());
+ Node b = d_skolemManager->mkDummySkolem("b", d_nodeManager->stringType());
+ Node c = d_skolemManager->mkDummySkolem("c", d_nodeManager->stringType());
+ Node d = d_skolemManager->mkDummySkolem("d", d_nodeManager->stringType());
Node sa = d_nodeManager->mkNode(
kind::STRING_SUBSTR,
a,
{
TestNode::SetUp();
- d_a = d_nodeManager->mkSkolem("a", d_nodeManager->booleanType());
- d_b = d_nodeManager->mkSkolem("b", d_nodeManager->booleanType());
- d_c = d_nodeManager->mkSkolem("c", d_nodeManager->booleanType());
- d_d = d_nodeManager->mkSkolem("d", d_nodeManager->booleanType());
- d_e = d_nodeManager->mkSkolem("e", d_nodeManager->booleanType());
- d_f = d_nodeManager->mkSkolem(
+ d_a = d_skolemManager->mkDummySkolem("a", d_nodeManager->booleanType());
+ d_b = d_skolemManager->mkDummySkolem("b", d_nodeManager->booleanType());
+ d_c = d_skolemManager->mkDummySkolem("c", d_nodeManager->booleanType());
+ d_d = d_skolemManager->mkDummySkolem("d", d_nodeManager->booleanType());
+ d_e = d_skolemManager->mkDummySkolem("e", d_nodeManager->booleanType());
+ d_f = d_skolemManager->mkDummySkolem(
"f",
d_nodeManager->mkFunctionType(d_nodeManager->booleanType(),
d_nodeManager->booleanType()));
- d_g = d_nodeManager->mkSkolem(
+ d_g = d_skolemManager->mkDummySkolem(
"g",
d_nodeManager->mkFunctionType(d_nodeManager->booleanType(),
d_nodeManager->booleanType()));
- d_h = d_nodeManager->mkSkolem(
+ d_h = d_skolemManager->mkDummySkolem(
"h",
d_nodeManager->mkFunctionType(d_nodeManager->booleanType(),
d_nodeManager->booleanType()));
projects / cvc5.git / commitdiff