Polymorphism and Z3 not playing nicely about vampire HOT 5 CLOSED

Defaulting to minisat sounds like a good step whilst we find a more long-term solution.

The alternative is the sat_fallback_for_smt option, which runs minisat alongside z3 and falls back to minisat if z3 ever fails... but if we know it's definitely going to fail then that doesn't sound very useful.

from vampire.

I looked at this code not so long ago in #300 - there we partially handle it if the "polymorphism" is actually just an indexed family of monomorphic functions. This looks like it's more involved though.

Seems to me that the thing to do would be to keep the mechanism in #300 and either:

1. Ground all sort variables before handing to Z3.
2. Skip asserting clauses with sort variables to Z3. Then it's an under-approximation, but it is anyway.

from vampire.

Just to note, that even with the fix #455 in place, we still receive an error when carrying out the above run command. However, the error is totally different (see below). It is linked to the interaction between polymorphism and UWA. As the UWA implementation is set to totally change, I am not going to fix this now.

Version : Vampire 4.7 (commit 340dc86bd on 2023-06-23 14:21:36 +0100)
Control points passed: 2214116
last control point:
                        -AtomicSort::isArraySort (2214116)
main
 vampireMode()
  doProving()
   ProvingHelper::runVampireSaturation
    ProvingHelper::runVampireSaturationImpl
     MainLoop::run
      SaturationAlgorithm::init
       SaturationAlgorithm::addInputClause
        SaturationAlgorithm::addInputSOSClause
         ActiveClauseContainer::add
          SingleParamEvent::fire
           SuperpositionSubtermIndex::handleClause
            SubstitutionTree::insert
             SubstitutionTree::UArrIntermediateNode::childByTop
              SubstitutionTree::ChildBySortHelper::mightExistAsTop
               tryGetResultSort(TermList,unsigned&)
                tryGetResultSort(Term*,unsigned&)
                 SortHelper::getResultSortOrMasterVariable
                  SortHelper::getResultSort(Term*)
                   SubstHelper::apply(TermList...)
                    SubstHelper::applyImpl(TermList...)
                     SubstHelper::applyImpl(Term*...)
                      AtomicSort::create/2
                       TermSharing::insert(AtomicSort*)

from vampire.

To clarify #455 has nothing to do with this issue. On further investigation, this issue is caused by current UWA implementation incorrectly creating constraints between sorts. As UWA implementation is set to change, I don't propose to fix now, but will leave this issue open so that we can revisit once new UWA implementation goes in.

from vampire.

No longer reproduces on master, I guess because the UWA changes came through. Good job!

from vampire.