Minor cleanup improvements + fix an answer literal bug in URR

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; i<activeLen; i++) {
-    if (!(*c)[i]->isAnswerLiteral()) handleLiteral((*c)[i], c, adding);
+    handleLiteral((*c)[i], c, adding);
   }
 }
 

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

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())) {

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>(_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);
       }
     }
 

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<TermList> _dividesNvalues;
   DHMap<Term*, int> _formulaCounts;
@@ -981,9 +971,6 @@ class Signature
    */ 
   DHMap<unsigned, Shell::TermAlgebra*> _termAlgebras;
 
-  // Map from functions to predicates they represent in answer literal conditions used in synthesis
-  DHMap<unsigned, unsigned> _synthesisFnToPred;
-
   //TODO Why are these here? They are not used anywhere. AYB
   //void defineOptionTermAlgebra(unsigned optionSort);
   //void defineEitherTermAlgebra(unsigned eitherSort);

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<TermList> 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<TermList> 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.
  */

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<TermList> 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);
 

Shell/AnswerExtractor.cpp

@@ -593,13 +593,13 @@ Literal* SynthesisManager::makeITEAnswerLiteral(Literal* condition, Literal* the
 
   Signature::Symbol* predSym = env.signature->getPredicate(thenLit->functor());
   Stack<TermList> 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<TermList> 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<TermList> 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<TermList> args;
         for (unsigned i = 0; i < tcond->arity(); ++i) args.push(transform(*(tcond->nthArgument(i))));
         Literal* newCond;

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<Term*, unsigned> _skolemToVar;
+    // Map from functions to predicates they represent in answer literal conditions
+    DHMap<unsigned, unsigned> _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<std::pair<unsigned,std::pair<Clause*, Literal*>>>* _answerPairs = nullptr;