From: Haniel Barbosa <hanielbbarbosa@gmail.com>
Date: Tue, 10 Dec 2019 20:17:00 +0000 (-0300)
Subject: Fix ufho issues (#3551)
X-Git-Tag: cvc5-1.0.0~3778
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d19c52821bb911413ff3dd4494c08a42a1db1e22;p=cvc5.git

Fix ufho issues (#3551)
---

diff --git a/src/options/options.h b/src/options/options.h
index 3f758e392..c321b3499 100644
--- a/src/options/options.h
+++ b/src/options/options.h
@@ -197,6 +197,7 @@ public:
   InputLanguage getInputLanguage() const;
   InstFormatMode getInstFormatMode() const;
   OutputLanguage getOutputLanguage() const;
+  bool getUfHo() const;
   bool getCheckProofs() const;
   bool getDumpInstantiations() const;
   bool getDumpModels() const;
diff --git a/src/options/options_public_functions.cpp b/src/options/options_public_functions.cpp
index a753c08de..d3906e24d 100644
--- a/src/options/options_public_functions.cpp
+++ b/src/options/options_public_functions.cpp
@@ -28,12 +28,13 @@
 #include "options/base_options.h"
 #include "options/language.h"
 #include "options/main_options.h"
+#include "options/option_exception.h"
 #include "options/parser_options.h"
 #include "options/printer_modes.h"
 #include "options/printer_options.h"
-#include "options/option_exception.h"
-#include "options/smt_options.h"
 #include "options/quantifiers_options.h"
+#include "options/smt_options.h"
+#include "options/uf_options.h"
 
 namespace CVC4 {
 
@@ -50,6 +51,8 @@ OutputLanguage Options::getOutputLanguage() const {
   return (*this)[options::outputLanguage];
 }
 
+bool Options::getUfHo() const { return (*this)[options::ufHo]; }
+
 bool Options::getCheckProofs() const{
   return (*this)[options::checkProofs];
 }
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 73dea766a..151ecbfb4 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -1763,7 +1763,6 @@ Expr Smt2::applyParseOp(ParseOp& p, std::vector<Expr>& args)
       }
     }
   }
-
   // Second phase: apply the arguments to the parse op
   ExprManager* em = getExprManager();
   // handle special cases
@@ -1833,6 +1832,19 @@ Expr Smt2::applyParseOp(ParseOp& p, std::vector<Expr>& args)
   }
   else if (isBuiltinOperator)
   {
+    if (!em->getOptions().getUfHo()
+        && (kind == kind::EQUAL || kind == kind::DISTINCT))
+    {
+      // need --uf-ho if these operators are applied over function args
+      for (std::vector<Expr>::iterator i = args.begin(); i != args.end(); ++i)
+      {
+        if ((*i).getType().isFunction())
+        {
+          parseError(
+              "Cannot apply equalty to functions unless --uf-ho is set.");
+        }
+      }
+    }
     if (args.size() > 2)
     {
       if (kind == kind::INTS_DIVISION || kind == kind::XOR
diff --git a/test/regress/regress0/declare-fun-is-match.smt2 b/test/regress/regress0/declare-fun-is-match.smt2
index d9387208f..f3877edca 100644
--- a/test/regress/regress0/declare-fun-is-match.smt2
+++ b/test/regress/regress0/declare-fun-is-match.smt2
@@ -1,4 +1,5 @@
 ; EXPECT: sat
+; COMMAND-LINE: --uf-ho
 (set-info :smt-lib-version 2.6)
 (set-logic UFIDL)
 (set-info :status sat)