diff options
| author | Haniel Barbosa <hanielbbarbosa@gmail.com> | 2019-12-10 17:17:00 -0300 |
|---|---|---|
| committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-12-10 14:17:00 -0600 |
| commit | d19c52821bb911413ff3dd4494c08a42a1db1e22 (patch) | |
| tree | aa91cb7bbc7aa66521b7bbfc528ab67394944616 | |
| parent | ee5fed52332ec6baddc8ecd8f8e04a644990bf29 (diff) | |
Fix ufho issues (#3551)
| -rw-r--r-- | src/options/options.h | 1 | ||||
| -rw-r--r-- | src/options/options_public_functions.cpp | 7 | ||||
| -rw-r--r-- | src/parser/smt2/smt2.cpp | 14 | ||||
| -rw-r--r-- | test/regress/regress0/declare-fun-is-match.smt2 | 1 |
4 files changed, 20 insertions, 3 deletions
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) |