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/regress0/ho/simple-matching.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/regress0/ho/simple-matching.smt2')
| -rw-r--r-- | test/regress/regress0/ho/simple-matching.smt2 | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/test/regress/regress0/ho/simple-matching.smt2 b/test/regress/regress0/ho/simple-matching.smt2 index 8e2315b2f..cbd70f072 100644 --- a/test/regress/regress0/ho/simple-matching.smt2 +++ b/test/regress/regress0/ho/simple-matching.smt2 @@ -1,6 +1,5 @@ -; COMMAND-LINE: --uf-ho ; EXPECT: unsat -(set-logic ALL) +(set-logic HO_ALL) (set-info :status unsat) (declare-sort U 0) (declare-fun f (U) U) |