summaryrefslogtreecommitdiff
path: root/src/preprocessing/passes
diff options
context:
space:
mode:
Diffstat (limited to 'src/preprocessing/passes')
-rw-r--r--src/preprocessing/passes/ackermann.cpp14
-rw-r--r--src/preprocessing/passes/bv_to_int.cpp15
-rw-r--r--src/preprocessing/passes/fun_def_fmf.cpp6
-rw-r--r--src/preprocessing/passes/ho_elim.cpp12
-rw-r--r--src/preprocessing/passes/int_to_bv.cpp10
-rw-r--r--src/preprocessing/passes/miplib_trick.cpp4
-rw-r--r--src/preprocessing/passes/nl_ext_purify.cpp12
-rw-r--r--src/preprocessing/passes/quantifier_macros.cpp15
-rw-r--r--src/preprocessing/passes/real_to_int.cpp9
-rw-r--r--src/preprocessing/passes/sep_skolem_emp.cpp18
-rw-r--r--src/preprocessing/passes/unconstrained_simplifier.cpp4
11 files changed, 77 insertions, 42 deletions
diff --git a/src/preprocessing/passes/ackermann.cpp b/src/preprocessing/passes/ackermann.cpp
index a19994ad9..525d0b243 100644
--- a/src/preprocessing/passes/ackermann.cpp
+++ b/src/preprocessing/passes/ackermann.cpp
@@ -27,6 +27,7 @@
#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"
@@ -105,10 +106,12 @@ void storeFunctionAndAddLemmas(TNode func,
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);
@@ -206,12 +209,13 @@ void collectUSortsToBV(const std::unordered_set<TNode, TNodeHashFunction>& vars,
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 "
diff --git a/src/preprocessing/passes/bv_to_int.cpp b/src/preprocessing/passes/bv_to_int.cpp
index c5f24c15c..28dcc1949 100644
--- a/src/preprocessing/passes/bv_to_int.cpp
+++ b/src/preprocessing/passes/bv_to_int.cpp
@@ -25,6 +25,7 @@
#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"
@@ -702,6 +703,7 @@ Node BVToInt::translateWithChildren(Node original,
Node BVToInt::translateNoChildren(Node original)
{
+ SkolemManager* sm = d_nm->getSkolemManager();
Node translation;
Assert(original.isVar() || original.isConst());
if (original.isVar())
@@ -722,11 +724,11 @@ Node BVToInt::translateNoChildren(Node original)
// 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));
@@ -783,9 +785,10 @@ Node BVToInt::translateFunctionSymbol(Node bvUF)
{
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
diff --git a/src/preprocessing/passes/fun_def_fmf.cpp b/src/preprocessing/passes/fun_def_fmf.cpp
index c6ea0ee27..8d1fed4a3 100644
--- a/src/preprocessing/passes/fun_def_fmf.cpp
+++ b/src/preprocessing/passes/fun_def_fmf.cpp
@@ -16,6 +16,7 @@
#include <sstream>
+#include "expr/skolem_manager.h"
#include "options/smt_options.h"
#include "preprocessing/assertion_pipeline.h"
#include "preprocessing/preprocessing_pass_context.h"
@@ -92,6 +93,7 @@ void FunDefFmf::process(AssertionPipeline* assertionsToPreprocess)
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]);
@@ -129,8 +131,8 @@ void FunDefFmf::process(AssertionPipeline* assertionsToPreprocess)
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]
diff --git a/src/preprocessing/passes/ho_elim.cpp b/src/preprocessing/passes/ho_elim.cpp
index 1bf980c49..619f3cfe2 100644
--- a/src/preprocessing/passes/ho_elim.cpp
+++ b/src/preprocessing/passes/ho_elim.cpp
@@ -19,6 +19,7 @@
#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"
@@ -36,6 +37,7 @@ HoElim::HoElim(PreprocessingPassContext* preprocContext)
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;
@@ -90,7 +92,7 @@ Node HoElim::eliminateLambdaComplete(Node n, std::map<Node, Node>& newLambda)
}
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;
@@ -151,6 +153,7 @@ Node HoElim::eliminateHo(Node n)
{
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;
@@ -187,7 +190,7 @@ Node HoElim::eliminateHo(Node n)
}
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);
@@ -260,7 +263,7 @@ Node HoElim::eliminateHo(Node n)
{
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
@@ -485,12 +488,13 @@ Node HoElim::getHoApplyUf(TypeNode tnf, TypeNode tna, TypeNode tnr)
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;
}
diff --git a/src/preprocessing/passes/int_to_bv.cpp b/src/preprocessing/passes/int_to_bv.cpp
index ef9b261b0..1f223ad4f 100644
--- a/src/preprocessing/passes/int_to_bv.cpp
+++ b/src/preprocessing/passes/int_to_bv.cpp
@@ -24,6 +24,7 @@
#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"
@@ -102,13 +103,14 @@ Node intToBV(TNode n, NodeMap& cache)
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
@@ -208,9 +210,9 @@ Node intToBV(TNode n, NodeMap& cache)
{
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())
diff --git a/src/preprocessing/passes/miplib_trick.cpp b/src/preprocessing/passes/miplib_trick.cpp
index f3c4d2e12..9ca58c334 100644
--- a/src/preprocessing/passes/miplib_trick.cpp
+++ b/src/preprocessing/passes/miplib_trick.cpp
@@ -19,6 +19,7 @@
#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"
@@ -201,6 +202,7 @@ PreprocessingPassResult MipLibTrick::applyInternal(
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);
@@ -522,7 +524,7 @@ PreprocessingPassResult MipLibTrick::applyInternal(
{
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",
diff --git a/src/preprocessing/passes/nl_ext_purify.cpp b/src/preprocessing/passes/nl_ext_purify.cpp
index 838a2a767..f07c5419f 100644
--- a/src/preprocessing/passes/nl_ext_purify.cpp
+++ b/src/preprocessing/passes/nl_ext_purify.cpp
@@ -16,6 +16,7 @@
#include "preprocessing/passes/nl_ext_purify.h"
+#include "expr/skolem_manager.h"
#include "preprocessing/assertion_pipeline.h"
#include "theory/rewriter.h"
@@ -32,6 +33,8 @@ Node NlExtPurify::purifyNlTerms(TNode n,
std::vector<Node>& var_eq,
bool beneathMult)
{
+ NodeManager* nm = NodeManager::currentNM();
+ SkolemManager* sm = nm->getSkolemManager();
if (beneathMult)
{
NodeMap::iterator find = bcache.find(n);
@@ -69,10 +72,9 @@ Node NlExtPurify::purifyNlTerms(TNode 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
@@ -92,7 +94,7 @@ Node NlExtPurify::purifyNlTerms(TNode n,
}
if (childChanged)
{
- ret = NodeManager::currentNM()->mkNode(n.getKind(), children);
+ ret = nm->mkNode(n.getKind(), children);
}
}
}
diff --git a/src/preprocessing/passes/quantifier_macros.cpp b/src/preprocessing/passes/quantifier_macros.cpp
index 8251183dd..6c97936b0 100644
--- a/src/preprocessing/passes/quantifier_macros.cpp
+++ b/src/preprocessing/passes/quantifier_macros.cpp
@@ -18,6 +18,7 @@
#include <vector>
+#include "expr/skolem_manager.h"
#include "options/quantifiers_options.h"
#include "options/smt_options.h"
#include "preprocessing/assertion_pipeline.h"
@@ -323,6 +324,8 @@ bool QuantifierMacros::getSubstitution( std::vector< Node >& v_quant, std::map<
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 ){
@@ -335,11 +338,14 @@ bool QuantifierMacros::process( Node n, bool pol, std::vector< Node >& args, Nod
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
@@ -392,7 +398,10 @@ bool QuantifierMacros::process( Node n, bool pol, std::vector< Node >& args, Nod
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 );
}
}
diff --git a/src/preprocessing/passes/real_to_int.cpp b/src/preprocessing/passes/real_to_int.cpp
index c80d55d3d..d8993ff1b 100644
--- a/src/preprocessing/passes/real_to_int.cpp
+++ b/src/preprocessing/passes/real_to_int.cpp
@@ -18,6 +18,7 @@
#include <string>
+#include "expr/skolem_manager.h"
#include "preprocessing/assertion_pipeline.h"
#include "preprocessing/preprocessing_pass_context.h"
#include "theory/arith/arith_msum.h"
@@ -42,6 +43,7 @@ Node RealToInt::realToIntInternal(TNode n, NodeMap& cache, std::vector<Node>& va
else
{
NodeManager* nm = NodeManager::currentNM();
+ SkolemManager* sm = nm->getSkolemManager();
Node ret = n;
if (n.getNumChildren() > 0)
{
@@ -178,9 +180,10 @@ Node RealToInt::realToIntInternal(TNode n, NodeMap& cache, std::vector<Node>& va
}
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.
diff --git a/src/preprocessing/passes/sep_skolem_emp.cpp b/src/preprocessing/passes/sep_skolem_emp.cpp
index 8c130768d..0c5ca9af9 100644
--- a/src/preprocessing/passes/sep_skolem_emp.cpp
+++ b/src/preprocessing/passes/sep_skolem_emp.cpp
@@ -20,6 +20,7 @@
#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"
@@ -41,6 +42,8 @@ Node preSkolemEmp(Node n,
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;
@@ -50,14 +53,13 @@ Node preSkolemEmp(Node 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();
}
}
@@ -83,7 +85,7 @@ Node preSkolemEmp(Node n,
}
if (childChanged)
{
- return NodeManager::currentNM()->mkNode(n.getKind(), children);
+ return nm->mkNode(n.getKind(), children);
}
}
visited[pol][n] = ret;
diff --git a/src/preprocessing/passes/unconstrained_simplifier.cpp b/src/preprocessing/passes/unconstrained_simplifier.cpp
index 9a9aaa366..2c01bd6d2 100644
--- a/src/preprocessing/passes/unconstrained_simplifier.cpp
+++ b/src/preprocessing/passes/unconstrained_simplifier.cpp
@@ -19,6 +19,7 @@
#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"
@@ -126,7 +127,8 @@ void UnconstrainedSimplifier::visitAll(TNode assertion)
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 "
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback