Disable definition introduction if not needed

vprover · Feb 29, 2024 · 7565a92 · 7565a92
1 parent 9380fdd
commit 7565a92
Show file tree

Hide file tree

Showing 3 changed files with 46 additions and 17 deletions.
diff --git a/Kernel/Signature.cpp b/Kernel/Signature.cpp
@@ -699,14 +699,14 @@ unsigned Signature::getDiff(){
 
 unsigned Signature::getFnDef(unsigned fn)
 {
-  auto sort = getFunction(fn)->fnType()->result();
-  ASS(sort.isTerm() && sort.term()->ground());
+  auto type = getFunction(fn)->fnType();
+  auto sort = type->result();
   bool added = false;
   auto name = "$def_"+sort.toString();
   unsigned p = addPredicate(name, 2, added);
   if (added) {
     ALWAYS(_fnDefPreds.insert(p));
-    OperatorType* ot = OperatorType::getPredicateType({sort, sort});
+    OperatorType* ot = OperatorType::getPredicateType({sort, sort}, type->numTypeArguments());
     Symbol* sym = getPredicate(p);
     sym->markProtected();
     sym->setType(ot);

diff --git a/Parse/SMTLIB2.cpp b/Parse/SMTLIB2.cpp
@@ -772,6 +772,11 @@ SMTLIB2::DeclaredSymbol SMTLIB2::declareFunctionOrPredicate(const vstring& name,
 
 //  ----------------------------------------------------------------------
 
+bool shouldCreateFunctionDefinition(unsigned fn)
+{
+  return env.options->functionDefinitionRewriting() || env.options->structInduction()==Options::StructuralInductionKind::RECURSION;
+}
+
 void SMTLIB2::readDefineFun(const vstring& name, LExprList* iArgs, LExpr* oSort, LExpr* body, const TermStack& typeArgs, bool recursive)
 {
   if (isAlreadyKnownSymbol(name)) {
@@ -838,12 +843,23 @@ void SMTLIB2::readDefineFun(const vstring& name, LExprList* iArgs, LExpr* oSort,
   Literal* lit;
   if (isTrueFun) {
     TermList lhs(Term::create(symbIdx,args.size(),args.begin()));
-    auto p = env.signature->getFnDef(symbIdx);
-    lit = Literal::create(p, true, { lhs, rhs });
+    if (shouldCreateFunctionDefinition(symbIdx)) {
+      auto p = env.signature->getFnDef(symbIdx);
+      auto defArgs = typeArgs;
+      defArgs.push(lhs);
+      defArgs.push(rhs);
+      lit = Literal::create(p,defArgs.size(),true,false,defArgs.begin());
+    } else {
+      lit = Literal::createEquality(true,lhs,rhs,rangeSort);
+    }
   } else {
-    auto p = env.signature->getBoolDef(symbIdx);
-    Formula* frm = new AtomicFormula(Literal::create(p,args.size(),true,false,args.begin()));
-    TermList lhs(Term::createFormula(frm));
+    if (shouldCreateFunctionDefinition(symbIdx)) {
+      auto p = env.signature->getBoolDef(symbIdx);
+      lit = Literal::create(p,args.size(),true,false,args.begin());
+    } else {
+      lit = Literal::create(symbIdx,args.size(),true,false,args.begin());
+    }
+    TermList lhs(Term::createFormula(new AtomicFormula(lit)));
     lit = Literal::createEquality(true, lhs, rhs, rangeSort);
   }
   Formula* fla = new AtomicFormula(lit);
@@ -932,13 +948,24 @@ void SMTLIB2::readDefineFunsRec(LExprList* declsExpr, LExprList* defsExpr)
     Literal* lit;
     if (isTrueFun) {
       TermList lhs(Term::create(symbIdx,decl.args.size(),decl.args.begin()));
-      auto p = env.signature->getFnDef(symbIdx);
-      lit = Literal::create(p, true, { lhs, rhs });
+      if (shouldCreateFunctionDefinition(symbIdx)) {
+        auto p = env.signature->getFnDef(symbIdx);
+        TermStack defArgs; // no type arguments (yet) in this case
+        defArgs.push(lhs);
+        defArgs.push(rhs);
+        lit = Literal::create(p,defArgs.size(),true,false,defArgs.begin());
+      } else {
+        lit = Literal::createEquality(true,lhs,rhs,decl.rangeSort);
+      }
     } else {
-      auto p = env.signature->getBoolDef(symbIdx);
-      Formula* frm = new AtomicFormula(Literal::create(p,decl.args.size(),true,false,decl.args.begin()));
-      TermList lhs(Term::createFormula(frm));
-      lit = Literal::createEquality(true,lhs,rhs,decl.rangeSort);
+      if (shouldCreateFunctionDefinition(symbIdx)) {
+        auto p = env.signature->getBoolDef(symbIdx);
+        lit = Literal::create(p,decl.args.size(),true,false,decl.args.begin());
+      } else {
+        lit = Literal::create(symbIdx,decl.args.size(),true,false,decl.args.begin());
+      }
+      TermList lhs(Term::createFormula(new AtomicFormula(lit)));
+      lit = Literal::createEquality(true, lhs, rhs, decl.rangeSort);
     }
     Formula* fla = new AtomicFormula(lit);
 

diff --git a/Shell/Preprocess.cpp b/Shell/Preprocess.cpp
@@ -367,9 +367,11 @@ void Preprocess::preprocess(Problem& prb)
      resolver.apply(prb);
    }
 
-  auto fnDefHandler = new FunctionDefinitionHandler();
-  fnDefHandler->preprocess(prb);
-  prb.addFunctionDefinitionHandler(fnDefHandler);
+  if (_options.functionDefinitionRewriting() || _options.structInduction()==Options::StructuralInductionKind::RECURSION) {
+    auto fnDefHandler = new FunctionDefinitionHandler();
+    fnDefHandler->preprocess(prb);
+    prb.addFunctionDefinitionHandler(fnDefHandler);
+  }
 
    if (_options.generalSplitting()) {
      if (prb.isHigherOrder() || prb.hasPolymorphicSym()) {  // TODO: extend GeneralSplitting to support polymorphism (would higher-order make sense?)