Polymorphism and Z3 not playing nicely

[ibnyusuf]

As pointed out by Andrei on slack:

vampire_rel -awr 28 -aac none -amm sco -anc none -bd preordered -bs on -bsr on -drc off -fsr off -gsp on -gs on -gsaa from_current -inw on -nwc 1.5 -sas z3 -s -1003 -sos all -sac on -sp frequency -tha off -t 90.0 -uwa all --mode spider --test_id 1980632213 --normalize on --memory_limit 16384 --include /home/voronkov/TPTP /home/voronkov/TPTP/Problems/LCL/LCL749_5.p
Z3 exception:
Sorts |fun(X0,fun(X0,X0))| and X0 are incompatible

I guess this is unsurprising, because Z3 has no support for polymorphism. We need to decide how best to handle the combination of AVATAR using Z3 as solver and polymorphism. Or should we only use minisat if we detect polymorphism?

[selig]

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.

[MichaelRawson]

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.

[ibnyusuf]

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*)

[ibnyusuf]

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.