diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-01-22 17:02:58 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-01-22 17:02:58 -0600 |
| commit | fd88b18c0db55eb63d0cd0454b19810a8abee789 (patch) | |
| tree | b87fed361d73f1f28b4bf8e51249e03dd7bc83b8 | |
| parent | 91538b206fd5da5be289cf2d6165a854e6e5bc07 (diff) | |
Fix subtyping for instantiations where internal representatives are chosen (#3641)
| -rw-r--r-- | src/theory/quantifiers/equality_query.cpp | 4 | ||||
| -rw-r--r-- | src/theory/quantifiers/instantiate.cpp | 9 | ||||
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/regress/regress1/fmf/issue3626.smt2 | 5 |
4 files changed, 13 insertions, 6 deletions
diff --git a/src/theory/quantifiers/equality_query.cpp b/src/theory/quantifiers/equality_query.cpp index f72a0d1b4..13e7b2eb7 100644 --- a/src/theory/quantifiers/equality_query.cpp +++ b/src/theory/quantifiers/equality_query.cpp @@ -167,7 +167,9 @@ Node EqualityQueryQuantifiersEngine::getInternalRepresentative(Node a, if( d_rep_score.find( r_best )==d_rep_score.end() ){ d_rep_score[ r_best ] = d_reset_count; } - Trace("internal-rep-select") << "...Choose " << r_best << " with score " << r_best_score << std::endl; + Trace("internal-rep-select") + << "...Choose " << r_best << " with score " << r_best_score + << " and type " << r_best.getType() << std::endl; Assert(r_best.getType().isSubtypeOf(v_tn)); v_int_rep[r] = r_best; if( r_best!=a ){ diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp index c6427a4c4..aec648037 100644 --- a/src/theory/quantifiers/instantiate.cpp +++ b/src/theory/quantifiers/instantiate.cpp @@ -126,17 +126,16 @@ bool Instantiate::addInstantiation( { terms[i] = getTermForType(tn); } + // Ensure the type is correct, this for instance ensures that real terms + // are cast to integers for { x -> t } where x has type Int and t has + // type Real. + terms[i] = quantifiers::TermUtil::ensureType(terms[i], tn); if (mkRep) { // pick the best possible representative for instantiation, based on past // use and simplicity of term terms[i] = d_qe->getInternalRepresentative(terms[i], q, i); } - else - { - // ensure the type is correct - terms[i] = quantifiers::TermUtil::ensureType(terms[i], tn); - } Trace("inst-add-debug") << " -> " << terms[i] << std::endl; if (terms[i].isNull()) { diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 5020fe6fd..65d7f2b31 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1225,6 +1225,7 @@ set(regress_1_tests regress1/fmf/german73.smt2 regress1/fmf/issue2034-preinit.smt2 regress1/fmf/issue3587.smt2 + regress1/fmf/issue3626.smt2 regress1/fmf/issue916-fmf-or.smt2 regress1/fmf/jasmin-cdt-crash.smt2 regress1/fmf/ko-bound-set.cvc diff --git a/test/regress/regress1/fmf/issue3626.smt2 b/test/regress/regress1/fmf/issue3626.smt2 new file mode 100644 index 000000000..9f27dee01 --- /dev/null +++ b/test/regress/regress1/fmf/issue3626.smt2 @@ -0,0 +1,5 @@ +; COMMAND-LINE: --fmf-bound +; EXPECT: sat +(set-logic ALL) +(assert (forall ((a Int)) (or (distinct (/ 0 0) a) (= (/ 0 a) 0)))) +(check-sat) |