diff options
author | Haniel Barbosa <hanielbbarbosa@gmail.com> | 2021-06-11 18:29:19 -0300 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-06-11 21:29:19 +0000 |
commit | 8ddd5e82c8e896977d5573b639524264c7207d85 (patch) | |
tree | ee6a94468288397e290cb3db60db76dbdf69e978 /test/regress/regress3/issue4170.smt2 | |
parent | f10087c3b347da6ef625a2ad92846551ad324d73 (diff) |
Better support for HOL parsing and set up (#6697)
This commit adds a new parser option, --hol, which marks that HOL is being used. This option has the effect of prepending the problem's logic with "HO_", which teels the solver that the logic is higher order. The parser builder, base parser, and SMT2 and TPTP parsers are all updated to work with this new setting, as is the logic info class.
For now this parser option is enabling the --uf-ho option for internal use, since for now higher-order solving relies it. In a future PR this dependency will be removed (since this information is already given to the SMT solver via the logic).
Diffstat (limited to 'test/regress/regress3/issue4170.smt2')
-rw-r--r-- | test/regress/regress3/issue4170.smt2 | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/test/regress/regress3/issue4170.smt2 b/test/regress/regress3/issue4170.smt2 index 0dee146c0..25e0c7f8d 100644 --- a/test/regress/regress3/issue4170.smt2 +++ b/test/regress/regress3/issue4170.smt2 @@ -1,6 +1,5 @@ -(set-logic ALL) +(set-logic HO_ALL) (set-option :sygus-inference true) -(set-option :uf-ho true) (set-option :sygus-ext-rew false) (set-info :status sat) (declare-fun a (Int) Int) |