diff options
| -rw-r--r-- | src/theory/quantifiers/sygus/sygus_unif_io.cpp | 54 | ||||
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/regress/regress1/sygus/tester.sy | 37 |
3 files changed, 76 insertions, 16 deletions
diff --git a/src/theory/quantifiers/sygus/sygus_unif_io.cpp b/src/theory/quantifiers/sygus/sygus_unif_io.cpp index 8833c0cdf..7e999d3f5 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_io.cpp +++ b/src/theory/quantifiers/sygus/sygus_unif_io.cpp @@ -448,20 +448,33 @@ void SubsumeTrie::getLeavesInternal(const std::vector<Node>& vals, ++it) { int new_status = status; - // if the current value is true + bool success = true; + // if the current value is true, we must consider the value of this child if (curr_val_true) { if (status != 0) { - Assert(it->first.isConst() && it->first.getType().isBoolean()); - new_status = (it->first.getConst<bool>() ? 1 : -1); - if (status != -2 && new_status != status) + if (it->first.isNull()) + { + // The value of this child is unknown on this point, hence we + // ignore it. + success = false; + } + else { - new_status = 0; + Assert(it->first.getType().isBoolean()); + new_status = (it->first.getConst<bool>() ? 1 : -1); + if (status != -2 && new_status != status) + { + new_status = 0; + } } } } - it->second.getLeavesInternal(vals, pol, v, index + 1, new_status); + if (success) + { + it->second.getLeavesInternal(vals, pol, v, index + 1, new_status); + } } } } @@ -644,17 +657,25 @@ void SygusUnifIo::notifyEnumeration(Node e, Node v, std::vector<Node>& lemmas) // The value of this term for this example, or the truth value of // the I/O pair if the role of this enumerator is enum_io. Node resb; - // If the result is not constant, then we cannot determine its value - // on this point. In this case, resb remains null. - if (res.isConst()) + if (eiv.getRole() == enum_io) { - if (eiv.getRole() == enum_io) - { - Node out = d_examples_out[j]; - Assert(out.isConst()); - resb = res == out ? d_true : d_false; - } - else + Node out = d_examples_out[j]; + Assert(out.isConst()); + // If the result is not constant, then we assume that it does + // not satisfy the example. This is a safe underapproximation + // of the good behavior of the current term, that is, we only + // produce solutions whose values are fully evaluatable on all input + // points. Notice that terms may be used as leaves of decision + // trees that are fully evaluatable on points in that branch, but + // are not evaluatable on others, e.g. (head x) in the solution: + // (ite ((_ is cons) x) (head x) 5) + resb = (res.isConst() && res == out) ? d_true : d_false; + } + else + { + // We only set resb if it is constant, otherwise it remains null. + // This indicates its value cannot be determined. + if (res.isConst()) { resb = res; } @@ -687,6 +708,7 @@ void SygusUnifIo::notifyEnumeration(Node e, Node v, std::vector<Node>& lemmas) std::vector<Node> subsume; if (cond_vals.find(d_false) == cond_vals.end()) { + Assert(cond_vals.size() == 1); // it is the entire solution, we are done Trace("sygus-sui-enum") << " ...success, full solution added to PBE pool : " diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 083f8df75..b5bccae23 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1656,6 +1656,7 @@ set(regress_1_tests regress1/sygus/sygus-uf-ex.sy regress1/sygus/t8.sy regress1/sygus/temp_input_to_synth_ic-error-121418.sy + regress1/sygus/tester.sy regress1/sygus/tl-type-0.sy regress1/sygus/tl-type-4x.sy regress1/sygus/tl-type.sy diff --git a/test/regress/regress1/sygus/tester.sy b/test/regress/regress1/sygus/tester.sy new file mode 100644 index 000000000..261666dd4 --- /dev/null +++ b/test/regress/regress1/sygus/tester.sy @@ -0,0 +1,37 @@ +; EXPECT: unsat +; COMMAND-LINE: --sygus-out=status + +(set-logic SLIA) +(declare-datatype DT ((A (a Int)) (B (b String)) (JSBool (jsBool Bool)))) + +(define-fun isA ((i DT)) Bool ((_ is A) i) ) +(define-fun isB ((i DT)) Bool ((_ is B) i) ) + +(synth-fun add ((x1 DT)) DT + ( + (Start DT (ntDT)) + (ntDT DT + ( x1 x2 + (JSBool ntBool) + (A ntInt) + (ite ntBool ntDT ntDT) + ) + ) + (ntBool Bool + ( + (isA ntDT) + (isB ntDT) + (jsBool ntDT) + ) + ) + (ntInt Int + (1 + (a ntDT) + (+ ntInt ntInt) + ) + ) + ) +) +(constraint (= (add (A 6)) (A 7))) +(constraint (= (add (B "j")) (B "j"))) +(check-synth) |