Skip to content

improve Vampire's Prolog compliance #1017

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
MichaelRawson merged 1 commit into from
Oct 12, 2026
Merged

improve Vampire's Prolog compliance #1017

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
7 changes: 3 additions & 4 deletions Kernel/Formula.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -174,12 +174,11 @@ std::string Formula::toString (bool topLevel) const

case NOT:
{
res += toString(c);
// always separate with a space: "~$true", "~~p" or "~?[X] : p(X)" do not tokenise as intended,
// and "~(p & q)" is read by Prolog as functional notation, where the argument may not be an operator of high priority
res += toString(c) + " ";

const Formula* arg = f->uarg();
Connective subc = arg->connective();
if(subc == FORALL || subc == EXISTS || subc == NOT || subc == LITERAL)
res += " ";
stack.push({arg->parenthesesRequired(c),NOCONN,arg});

continue;
Expand Down
4 changes: 2 additions & 2 deletions Kernel/InferenceStore.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -741,7 +741,7 @@ std::string getSkolemizeMap(unsigned unitNumber, It symIt){
}

void printSATStep(SATClause *cl) override {
out << "cnf(s" << cl->number << ", plain, ";
out << "cnf(s" << cl->number << ", plain, (";
if(cl->isEmpty())
out << "$false";
else {
Expand All @@ -754,7 +754,7 @@ std::string getSkolemizeMap(unsigned unitNumber, It symIt){
}
}

out << ", inference(";
out << "), inference(";
auto inference = cl->inference();
switch(inference->getType()) {
case SAT::SATInference::PROP_INF: {
Expand Down
7 changes: 6 additions & 1 deletion Kernel/Term.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -917,7 +917,12 @@ std::string Literal::toString(bool reverseEquality) const
}
}

s += predicateName();
const std::string& name = predicateName();
// "~$less(X,Y)" is not valid Prolog: "~$" would be read as a single token
if (polarity() == 0 && name[0] == '$') {
s += ' ';
}
s += name;

//cerr << "predicate: "<< predicateName()<<endl;
if (_arity > 0) {
Expand Down
5 changes: 3 additions & 2 deletions Shell/TPTPPrinter.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -71,7 +71,7 @@ void TPTPPrinter::printWithRole(std::string name, std::string role, Unit* u, boo
std::string body = getBodyStr(u, includeSplitLevels);

ensureHeadersPrinted(u);
tgt() << "tff(" << name << ", " << role << ", " << body << ")." << endl;
tgt() << "tff(" << name << ", " << role << ", (" << body << "))." << endl;
}

/**
Expand Down Expand Up @@ -328,7 +328,7 @@ std::string TPTPPrinter::toString(const Formula* formula)
{
static std::string names [] =
{ "", " & ", " | ", " => ", " <=> ", " <~> ",
"~", "!", "?", "$term", "$false", "$true", "", ""};
"~ ", "!", "?", "$term", "$false", "$true", "", ""};
ASS_EQ(sizeof(names)/sizeof(std::string), NOCONN+1);

std::string res;
Expand Down Expand Up @@ -542,6 +542,7 @@ std::string TPTPPrinter::toString (const Unit* unit, bool typedClauses)
main = universalPrefix(unit) + "( " + main + " )";
} else {
prefix = "cnf";
main = "( " + main + " )";
}
}
else {
Expand Down
4 changes: 2 additions & 2 deletions checks/sanity
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -340,10 +340,10 @@ check_output_contains '(f @ (^[X0 : a] : (X0)) @ (^[X1 : b] : (X1)))' --mode out
check_output_contains '(^[X0 : a] : ((g @ X0))) @ y' --mode output parse/thf-lambda-in-app-chain.p
check_output_contains '(ev @ (^[X0 : a] : ((? [X1 : b] : (r @ X0 @ X1)))) @ q)' --mode output parse/thf-lambda-in-app-chain.p
check_output_contains '(((((^[X0 : b] : (y)) @ w)) = y))' --mode output parse/thf-lambda-in-app-chain.p
check_output_contains '(fl @ (^[X0 : a] : ((~(r @ X0 @ w)))) @ q)' --mode output parse/thf-lambda-in-app-chain.p
check_output_contains '(fl @ (^[X0 : a] : ((~ (r @ X0 @ w)))) @ q)' --mode output parse/thf-lambda-in-app-chain.p
check_rejected 'sort mismatch in the application x @ y' --input_syntax tptp --mode output parse/thf-ill-typed-app.p
check_rejected 'sort mismatch in the application r | q @ x' --input_syntax tptp --mode output parse/thf-app-to-formula.p
check_output_contains '(~((p = q)))' --mode output parse/thf-not-eq.p
check_output_contains '(~ ((p = q)))' --mode output parse/thf-not-eq.p
check_output_contains_once "'~' applied to an unparenthesized (in)equality" --mode output parse/thf-non-conformity-warnings.p
check_output_contains_once 'an unparenthesized application as a connective argument' --mode output parse/thf-non-conformity-warnings.p
check_output_contains_once 'as an unparenthesized equality argument' --mode output parse/thf-non-conformity-warnings.p
Expand Down