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/issue4990-care-graph.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/issue4990-care-graph.smt2')
-rw-r--r-- | test/regress/regress0/ho/issue4990-care-graph.smt2 | 4 |
1 files changed, 1 insertions, 3 deletions
diff --git a/test/regress/regress0/ho/issue4990-care-graph.smt2 b/test/regress/regress0/ho/issue4990-care-graph.smt2 index 6c44a94a8..93c87d3c9 100644 --- a/test/regress/regress0/ho/issue4990-care-graph.smt2 +++ b/test/regress/regress0/ho/issue4990-care-graph.smt2 @@ -1,7 +1,5 @@ -; COMMAND-LINE: --uf-ho ; EXPECT: sat -(set-logic QF_AUFBVLIA) -(set-option :uf-ho true) +(set-logic HO_QF_AUFBVLIA) (declare-fun a () Int) (declare-fun b () Int) (declare-fun c (Int) Int) |