From da8152339ca0429a8066c2c160859797d079bd64 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Petra=20Hozzov=C3=A1?= Date: Thu, 5 Oct 2023 15:10:27 +0200 Subject: [PATCH] Minor cleanup improvements + fix an answer literal bug in URR --- Indexing/LiteralIndex.cpp | 2 +- Inferences/BinaryResolution.cpp | 2 +- Inferences/Superposition.cpp | 2 +- Inferences/URResolution.cpp | 4 +-- Kernel/Signature.hpp | 13 -------- Kernel/Term.cpp | 51 ----------------------------- Kernel/Term.hpp | 2 -- Shell/AnswerExtractor.cpp | 57 +++++++++++++++++++++++++++++++-- Shell/AnswerExtractor.hpp | 31 +++++++++++------- 9 files changed, 78 insertions(+), 86 deletions(-) diff --git a/Indexing/LiteralIndex.cpp b/Indexing/LiteralIndex.cpp index f91c8cb3e9..3f71869336 100644 --- a/Indexing/LiteralIndex.cpp +++ b/Indexing/LiteralIndex.cpp @@ -192,7 +192,7 @@ void NonUnitClauseWithALLiteralIndex::handleClause(Clause* c, bool adding) TIME_TRACE("non unit clause with answer literals index maintenance"); unsigned activeLen = _selectedOnly ? c->numSelected() : clen; for(unsigned i=0; iisAnswerLiteral()) handleLiteral((*c)[i], c, adding); + handleLiteral((*c)[i], c, adding); } } diff --git a/Inferences/BinaryResolution.cpp b/Inferences/BinaryResolution.cpp index 92e3f2733e..16b022ed59 100644 --- a/Inferences/BinaryResolution.cpp +++ b/Inferences/BinaryResolution.cpp @@ -313,7 +313,7 @@ Clause* BinaryResolution::generateClause(Clause* queryCl, Literal* queryLit, SLQ Literal* newLitD = qr.substitution->applyToResult(dAnsLit); bool cNeg = queryLit->isNegative(); Literal* condLit = cNeg ? qr.substitution->applyToResult(qr.literal) : qr.substitution->applyToQuery(queryLit); - (*res)[next] = SynthesisManager::makeITEAnswerLiteral(condLit, cNeg ? newLitC : newLitD, cNeg ? newLitD : newLitC); + (*res)[next] = SynthesisManager::getInstance()->makeITEAnswerLiteral(condLit, cNeg ? newLitC : newLitD, cNeg ? newLitD : newLitC); } if(withConstraints){ diff --git a/Inferences/Superposition.cpp b/Inferences/Superposition.cpp index 253d86b602..f45c9253c6 100644 --- a/Inferences/Superposition.cpp +++ b/Inferences/Superposition.cpp @@ -560,7 +560,7 @@ Clause* Superposition::performSuperposition( Literal* newLitC = subst->apply(rwAnsLit, !eqIsResult); Literal* newLitD = subst->apply(eqAnsLit, eqIsResult); Literal* condLit = subst->apply(eqLit, eqIsResult); - (*res)[next] = SynthesisManager::makeITEAnswerLiteral(condLit, newLitC, newLitD); + (*res)[next] = SynthesisManager::getInstance()->makeITEAnswerLiteral(condLit, newLitC, newLitD); } if(needsToFulfilWeightLimit && !passiveClauseContainer->fulfilsWeightLimit(weight, numPositiveLiteralsLowerBound, res->inference())) { diff --git a/Inferences/URResolution.cpp b/Inferences/URResolution.cpp index 801210d5ed..468e232a96 100644 --- a/Inferences/URResolution.cpp +++ b/Inferences/URResolution.cpp @@ -133,6 +133,7 @@ struct URResolution::Item */ void resolveLiteral(unsigned idx, SLQueryResult& unif, Clause* premise, bool useQuerySubstitution) { + Literal* rlit = _lits[idx]; _lits[idx] = 0; _premises[idx] = premise; _color = static_cast(_color | premise->color()); @@ -144,11 +145,10 @@ struct URResolution::Item if (!premAnsLit->ground()) premAnsLit = unif.substitution->apply(premAnsLit, useQuerySubstitution); if (!_ansLit) _ansLit = premAnsLit; else if (_ansLit != premAnsLit) { - Literal* rlit = _lits[idx]; bool neg = rlit->isNegative(); Literal* resolved = unif.substitution->apply(rlit, !useQuerySubstitution); if (neg) resolved = Literal::complementaryLiteral(resolved); - _ansLit = SynthesisManager::makeITEAnswerLiteral(resolved, neg ? _ansLit : premAnsLit, neg ? premAnsLit : _ansLit); + _ansLit = SynthesisManager::getInstance()->makeITEAnswerLiteral(resolved, neg ? _ansLit : premAnsLit, neg ? premAnsLit : _ansLit); } } diff --git a/Kernel/Signature.hpp b/Kernel/Signature.hpp index 8a4cda71a8..952746069c 100644 --- a/Kernel/Signature.hpp +++ b/Kernel/Signature.hpp @@ -893,16 +893,6 @@ class Signature static bool symbolNeedsQuoting(vstring name, bool interpreted, unsigned arity); - void addSynthesisPair(unsigned fn, unsigned pred) { - ASS(fn < _funs.length()); - ASS(pred < _preds.length()); - _synthesisFnToPred.insert(fn, pred); - } - - unsigned getPredForSynthesisFn(unsigned fn) { - return _synthesisFnToPred.get(fn); - } - private: Stack _dividesNvalues; DHMap _formulaCounts; @@ -981,9 +971,6 @@ class Signature */ DHMap _termAlgebras; - // Map from functions to predicates they represent in answer literal conditions used in synthesis - DHMap _synthesisFnToPred; - //TODO Why are these here? They are not used anywhere. AYB //void defineOptionTermAlgebra(unsigned optionSort); //void defineEitherTermAlgebra(unsigned eitherSort); diff --git a/Kernel/Term.cpp b/Kernel/Term.cpp index 0684e70d1d..7896f98ceb 100644 --- a/Kernel/Term.cpp +++ b/Kernel/Term.cpp @@ -860,47 +860,6 @@ Term* Term::create(Term* t,TermList* args) return s; } -/** Create a new complex term, with its top-level function symbol - * created as a dummy symbol representing the predicate of @b l, and copy - * from the array @b args its arguments. Insert it into the sharing - * structure if all arguments are shared. - */ -Term* Term::translateToSynthesisConditionTerm(Literal* l) -{ - ASS_EQ(l->getPreDataSize(), 0); - ASS(!l->isSpecial()); - - unsigned arity = l->arity(); - vstring fnName = "cond_"; - if (l->isNegative()) fnName.append("not_"); - fnName.append(l->predicateName()); - if (l->isEquality()) fnName.append(SortHelper::getEqualityArgumentSort(l).toString()); - bool added = false; - unsigned fn = env.signature->addFunction(fnName, arity, added); - // Store the mapping between the function and predicate symbols - env.signature->addSynthesisPair(fn, l->functor()); - if (added) { - Signature::Symbol* sym = env.signature->getFunction(fn); - Stack argSorts; - if (l->isEquality()) { - TermList as = SortHelper::getEqualityArgumentSort(l); - argSorts.push(as); - argSorts.push(as); - } else { - OperatorType* ot = env.signature->getPredicate(l->functor())->predType(); - for (unsigned i = 0; i < arity; ++i) { - argSorts.push(ot->arg(i)); - } - if (!env.signature->getPredicate(l->functor())->computable()) sym->markUncomputable(); - } - sym->setType(OperatorType::getFunctionType(arity, argSorts.begin(), AtomicSort::defaultSort())); - } - - Stack args; - for (unsigned i = 0; i < arity; ++i) args.push(*(l->nthArgument(i))); - return Term::create(fn, arity, args.begin()); -} - /** Create a new complex term, and insert it into the sharing * structure if all arguments are shared. */ @@ -1138,16 +1097,6 @@ Term *Term::createMatch(TermList sort, TermList matchedSort, unsigned int arity, return s; } -/** - * Create a (condition ? thenBranch : elseBranch) expression - * and return the resulting term - */ -Term* Term::createRegularITE(Term* condition, TermList thenBranch, TermList elseBranch, TermList branchSort) -{ - unsigned itefn = SynthesisManager::getITEFunctionSymbol(branchSort); - return Term::create(itefn, {TermList(condition), thenBranch, elseBranch}); -} - /** Create a new complex term, copy from @b t its function symbol and arity. * Initialize its arguments by a dummy special variable. */ diff --git a/Kernel/Term.hpp b/Kernel/Term.hpp index b09b1ac44a..775975e310 100644 --- a/Kernel/Term.hpp +++ b/Kernel/Term.hpp @@ -378,7 +378,6 @@ class Term static Term* create(unsigned function, unsigned arity, const TermList* args); static Term* create(unsigned fn, std::initializer_list args); static Term* create(Term* t,TermList* args); - static Term* translateToSynthesisConditionTerm(Literal* l); static Term* createNonShared(unsigned function, unsigned arity, TermList* arg); static Term* createNonShared(Term* t,TermList* args); static Term* createNonShared(Term* t); @@ -395,7 +394,6 @@ class Term static Term* createTuple(unsigned arity, TermList* sorts, TermList* elements); static Term* createTuple(Term* tupleTerm); static Term* createMatch(TermList sort, TermList matchedSort, unsigned int arity, TermList* elements); - static Term* createRegularITE(Term* condition, TermList thenBranch, TermList elseBranch, TermList branchSort); static Term* create1(unsigned fn, TermList arg); static Term* create2(unsigned fn, TermList arg1, TermList arg2); diff --git a/Shell/AnswerExtractor.cpp b/Shell/AnswerExtractor.cpp index e1ea4c5cd6..dff728d386 100644 --- a/Shell/AnswerExtractor.cpp +++ b/Shell/AnswerExtractor.cpp @@ -593,13 +593,13 @@ Literal* SynthesisManager::makeITEAnswerLiteral(Literal* condition, Literal* the Signature::Symbol* predSym = env.signature->getPredicate(thenLit->functor()); Stack litArgs; - Term* condTerm = Term::translateToSynthesisConditionTerm(condition); + Term* condTerm = translateToSynthesisConditionTerm(condition); for (unsigned i = 0; i < thenLit->arity(); ++i) { TermList* ttl = thenLit->nthArgument(i); TermList* etl = elseLit->nthArgument(i); if (ttl == etl) litArgs.push(*ttl); else { - litArgs.push(TermList(Term::createRegularITE(condTerm, *ttl, *etl, predSym->predType()->arg(i)))); + litArgs.push(TermList(createRegularITE(condTerm, *ttl, *etl, predSym->predType()->arg(i)))); } } return Literal::create(thenLit->functor(), thenLit->arity(), thenLit->polarity(), /*commutative=*/false, litArgs.begin()); @@ -658,6 +658,57 @@ Formula* SynthesisManager::getConditionFromClause(Clause* cl) { return JunctionFormula::generalJunction(Connective::AND, fl); } +/** Create a new complex term, with its top-level function symbol + * created as a dummy symbol representing the predicate of @b l, and copy + * from the array @b args its arguments. Insert it into the sharing + * structure if all arguments are shared. + */ +Term* SynthesisManager::translateToSynthesisConditionTerm(Literal* l) +{ + ASS_EQ(l->getPreDataSize(), 0); + ASS(!l->isSpecial()); + + unsigned arity = l->arity(); + vstring fnName = "cond_"; + if (l->isNegative()) fnName.append("not_"); + fnName.append(l->predicateName()); + if (l->isEquality()) fnName.append(SortHelper::getEqualityArgumentSort(l).toString()); + bool added = false; + unsigned fn = env.signature->addFunction(fnName, arity, added); + // Store the mapping between the function and predicate symbols + _skolemReplacement.addCondPair(fn, l->functor()); + if (added) { + Signature::Symbol* sym = env.signature->getFunction(fn); + Stack argSorts; + if (l->isEquality()) { + TermList as = SortHelper::getEqualityArgumentSort(l); + argSorts.push(as); + argSorts.push(as); + } else { + OperatorType* ot = env.signature->getPredicate(l->functor())->predType(); + for (unsigned i = 0; i < arity; ++i) { + argSorts.push(ot->arg(i)); + } + if (!env.signature->getPredicate(l->functor())->computable()) sym->markUncomputable(); + } + sym->setType(OperatorType::getFunctionType(arity, argSorts.begin(), AtomicSort::defaultSort())); + } + + Stack args; + for (unsigned i = 0; i < arity; ++i) args.push(*(l->nthArgument(i))); + return Term::create(fn, arity, args.begin()); +} + +/** + * Create a (condition ? thenBranch : elseBranch) expression + * and return the resulting term + */ +Term* SynthesisManager::createRegularITE(Term* condition, TermList thenBranch, TermList elseBranch, TermList branchSort) +{ + unsigned itefn = getITEFunctionSymbol(branchSort); + return Term::create(itefn, {TermList(condition), thenBranch, elseBranch}); +} + void SynthesisManager::ConjectureSkolemReplacement::bindSkolemToVar(Term* t, unsigned v) { ASS(_skolemToVar.count(t) == 0); _skolemToVar[t] = v; @@ -726,7 +777,7 @@ TermList SynthesisManager::ConjectureSkolemReplacement::transformSubterm(TermLis // Build condition Term* tcond = t->nthArgument(0)->term(); vstring condName = tcond->functionName(); - unsigned pred = env.signature->getPredForSynthesisFn(tcond->functor()); + unsigned pred = _condFnToPred.get(tcond->functor()); Stack args; for (unsigned i = 0; i < tcond->arity(); ++i) args.push(transform(*(tcond->nthArgument(i)))); Literal* newCond; diff --git a/Shell/AnswerExtractor.hpp b/Shell/AnswerExtractor.hpp index 58309a878b..efd4991d43 100644 --- a/Shell/AnswerExtractor.hpp +++ b/Shell/AnswerExtractor.hpp @@ -102,18 +102,7 @@ class SynthesisManager : public AnswerLiteralManager virtual Clause* recordAnswerAndReduce(Clause* cl) override; - static unsigned getITEFunctionSymbol(TermList sort) { - vstring name = "$ite_" + sort.toString(); - bool added = false; - unsigned fn = env.signature->addFunction(name, 3, added); - if (added) { - Signature::Symbol* sym = env.signature->getFunction(fn); - sym->setType(OperatorType::getFunctionType({AtomicSort::defaultSort(), sort, sort}, sort)); - } - return fn; - } - - static Literal* makeITEAnswerLiteral(Literal* condition, Literal* thenLit, Literal* elseLit); + Literal* makeITEAnswerLiteral(Literal* condition, Literal* thenLit, Literal* elseLit); private: class ConjectureSkolemReplacement : public TermTransformer { @@ -122,11 +111,14 @@ class SynthesisManager : public AnswerLiteralManager void bindSkolemToVar(Term* t, unsigned v); TermList transformTermList(TermList tl, TermList sort); virtual Literal* transform(Literal* lit) { return TermTransformer::transform(lit); } + void addCondPair(unsigned fn, unsigned pred) { _condFnToPred.insert(fn, pred); } protected: virtual TermList transformSubterm(TermList trm); virtual TermList transform(TermList ts); private: vmap _skolemToVar; + // Map from functions to predicates they represent in answer literal conditions + DHMap _condFnToPred; }; virtual Formula* tryGetQuantifiedFormulaForAnswerLiteral(Unit* unit) override; @@ -135,6 +127,21 @@ class SynthesisManager : public AnswerLiteralManager Formula* getConditionFromClause(Clause* cl); + Term* translateToSynthesisConditionTerm(Literal* l); + + static Term* createRegularITE(Term* condition, TermList thenBranch, TermList elseBranch, TermList branchSort); + + static unsigned getITEFunctionSymbol(TermList sort) { + vstring name = "$ite_" + sort.toString(); + bool added = false; + unsigned fn = env.signature->addFunction(name, 3, added); + if (added) { + Signature::Symbol* sym = env.signature->getFunction(fn); + sym->setType(OperatorType::getFunctionType({AtomicSort::defaultSort(), sort, sort}, sort)); + } + return fn; + } + ConjectureSkolemReplacement _skolemReplacement; List>>* _answerPairs = nullptr;