From 352034696fdce868452d097d155f195ea1fa949c Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 6 Aug 2018 17:33:23 -0500 Subject: [PATCH] Fixes and improvements for single invocation inference (#2261) --- .../quantifiers/single_inv_partition.cpp | 54 +++++++++++++++---- src/theory/quantifiers/single_inv_partition.h | 2 + test/regress/Makefile.tests | 1 + .../regress1/sygus/constant-bool-si-all.sy | 14 +++++ 4 files changed, 60 insertions(+), 11 deletions(-) create mode 100644 test/regress/regress1/sygus/constant-bool-si-all.sy 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& 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 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& 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& 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 conj; @@ -187,7 +205,21 @@ bool SingleInvocationPartition::init(std::vector& funcs, std::vector 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 d_input_funcs; /** all input functions */ std::vector d_all_funcs; + /** skolem of the same type as input functions */ + std::vector d_input_func_sks; /** infer the argument types of uninterpreted function applications * diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests index b8479475f..34855e81d 100644 --- a/test/regress/Makefile.tests +++ b/test/regress/Makefile.tests @@ -1508,6 +1508,7 @@ REG1_TESTS = \ regress1/sygus/clock-inc-tuple.sy \ regress1/sygus/commutative.sy \ regress1/sygus/constant.sy \ + regress1/sygus/constant-bool-si-all.sy \ regress1/sygus/constant-dec-tree-bug.sy \ regress1/sygus/constant-ite-bv.sy \ regress1/sygus/crci-ssb-unk.sy \ diff --git a/test/regress/regress1/sygus/constant-bool-si-all.sy b/test/regress/regress1/sygus/constant-bool-si-all.sy new file mode 100644 index 000000000..eee7956f4 --- /dev/null +++ b/test/regress/regress1/sygus/constant-bool-si-all.sy @@ -0,0 +1,14 @@ +; EXPECT: unsat +; COMMAND-LINE: --sygus-out=status +(set-logic SAT) +(synth-fun f () Bool) +(synth-fun g () Bool) +(synth-fun h () Bool) +(synth-fun w () Int) + +(constraint (not (= w 0))) +(constraint f) +(constraint (not g)) +(constraint h) + +(check-synth) -- 2.30.2