Fix ufho issues (#3551)

diff --git a/src/options/options.h b/src/options/options.h
index 3f758e39227376664c78da8f0d67a10dc2754bd5..c321b349921f761c21d0a73f646da054628fe611 100644 (file)
--- 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 a753c08dea45f885e0d38b89f9d440876a74343d..d3906e24dbafd1acfd488e2886fd524df1c43d86 100644 (file)
--- 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 73dea766a018b8ad11bb3e0e0ba0d081cbb66b7e..151ecbfb4885d90bddf64ddcffb57009948c21a3 100644 (file)
--- 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 d9387208f072036e225e74b5147ed86281a9212f..f3877edca23a8410d993505ad93e7a113f95e037 100644 (file)
--- 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)