diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/theory/quantifiers/single_inv_partition.cpp | 54 | ||||
-rw-r--r-- | src/theory/quantifiers/single_inv_partition.h | 2 |
2 files changed, 45 insertions, 11 deletions
diff --git a/src/theory/quantifiers/single_inv_partition.cpp b/src/theory/quantifiers/single_inv_partition.cpp index 40c191ca2..851204a84 100644 --- a/src/theory/quantifiers/single_inv_partition.cpp +++ b/src/theory/quantifiers/single_inv_partition.cpp @@ -128,26 +128,38 @@ bool SingleInvocationPartition::inferArgTypes(Node n, bool SingleInvocationPartition::init(std::vector<Node>& funcs, Node n) { - Trace("si-prt") << "Initialize with " << funcs.size() << " input functions..." - << std::endl; + Trace("si-prt") << "Initialize with " << funcs.size() << " input functions (" + << funcs << ")..." << std::endl; std::vector<TypeNode> typs; if (!funcs.empty()) { TypeNode tn0 = funcs[0].getType(); - for (unsigned i = 1; i < funcs.size(); i++) + if (tn0.getNumChildren() > 0) { - if (funcs[i].getType() != tn0) + for (unsigned i = 0, nargs = tn0.getNumChildren() - 1; i < nargs; i++) + { + typs.push_back(tn0[i]); + } + } + for (unsigned i = 1, size = funcs.size(); i < size; i++) + { + TypeNode tni = funcs[i].getType(); + if (tni.getNumChildren() != tn0.getNumChildren()) { // can't anti-skolemize functions of different sort Trace("si-prt") << "...type mismatch" << std::endl; return false; } - } - if (tn0.getNumChildren() > 1) - { - for (unsigned j = 0; j < tn0.getNumChildren() - 1; j++) + else if (tni.getNumChildren() > 0) { - typs.push_back(tn0[j]); + for (unsigned j = 0, nargs = tni.getNumChildren() - 1; j < nargs; j++) + { + if (tni[j] != typs[j]) + { + Trace("si-prt") << "...argument type mismatch" << std::endl; + return false; + } + } } } } @@ -163,6 +175,7 @@ bool SingleInvocationPartition::init(std::vector<Node>& funcs, Assert(d_arg_types.empty()); Assert(d_input_funcs.empty()); Assert(d_si_vars.empty()); + NodeManager* nm = NodeManager::currentNM(); 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()); @@ -171,10 +184,15 @@ bool SingleInvocationPartition::init(std::vector<Node>& funcs, { std::stringstream ss; ss << "s_" << j; - Node si_v = NodeManager::currentNM()->mkBoundVar(ss.str(), d_arg_types[j]); + Node si_v = nm->mkBoundVar(ss.str(), d_arg_types[j]); d_si_vars.push_back(si_v); } Assert(d_si_vars.size() == d_arg_types.size()); + for (const Node& inf : d_input_funcs) + { + Node sk = nm->mkSkolem("_sik", inf.getType()); + d_input_func_sks.push_back(sk); + } Trace("si-prt") << "SingleInvocationPartition::process " << n << std::endl; Trace("si-prt") << "Get conjuncts..." << std::endl; std::vector<Node> conj; @@ -187,7 +205,21 @@ bool SingleInvocationPartition::init(std::vector<Node>& funcs, std::vector<Node> si_subs; Trace("si-prt") << "Process conjunct : " << conj[i] << std::endl; // do DER on conjunct - Node cr = TermUtil::getQuantSimplify(conj[i]); + // Must avoid eliminating the first-order input functions in the + // getQuantSimplify step below. We use a substitution to avoid this. + // This makes it so that e.g. the synthesis conjecture: + // exists f. f!=0 ^ P + // is not rewritten to exists f. (f=0 => false) ^ P and subsquently + // rewritten to exists f. false ^ P by the elimination f -> 0. + Node cr = conj[i].substitute(d_input_funcs.begin(), + d_input_funcs.end(), + d_input_func_sks.begin(), + d_input_func_sks.end()); + cr = TermUtil::getQuantSimplify(cr); + cr = cr.substitute(d_input_func_sks.begin(), + d_input_func_sks.end(), + d_input_funcs.begin(), + d_input_funcs.end()); if (cr != conj[i]) { Trace("si-prt-debug") << "...rewritten to " << cr << std::endl; diff --git a/src/theory/quantifiers/single_inv_partition.h b/src/theory/quantifiers/single_inv_partition.h index 588b1fde8..199ab29d4 100644 --- a/src/theory/quantifiers/single_inv_partition.h +++ b/src/theory/quantifiers/single_inv_partition.h @@ -228,6 +228,8 @@ class SingleInvocationPartition std::vector<Node> d_input_funcs; /** all input functions */ std::vector<Node> d_all_funcs; + /** skolem of the same type as input functions */ + std::vector<Node> d_input_func_sks; /** infer the argument types of uninterpreted function applications * |