diff options
Diffstat (limited to 'src/theory/quantifiers/sygus/transition_inference.cpp')
| -rw-r--r-- | src/theory/quantifiers/sygus/transition_inference.cpp | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/src/theory/quantifiers/sygus/transition_inference.cpp b/src/theory/quantifiers/sygus/transition_inference.cpp index 7ee2f2ec6..eb2f0f739 100644 --- a/src/theory/quantifiers/sygus/transition_inference.cpp +++ b/src/theory/quantifiers/sygus/transition_inference.cpp @@ -16,6 +16,7 @@ #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" @@ -197,6 +198,7 @@ void TransitionInference::process(Node n, Node f) void TransitionInference::process(Node n) { NodeManager* nm = NodeManager::currentNM(); + SkolemManager* sm = nm->getSkolemManager(); d_complete = true; d_trivial = true; std::vector<Node> n_check; @@ -276,7 +278,7 @@ void TransitionInference::process(Node n) { 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); } @@ -426,9 +428,11 @@ bool TransitionInference::processDisjunct( 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 << " "; } |