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/sygus | |
| 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/sygus')
| -rw-r--r-- | test/regress/regress0/sygus/pLTL-sygus-syntax-err.sy | 19 | ||||
| -rw-r--r-- | test/regress/regress0/sygus/sygus-uf.sy | 4 |
2 files changed, 10 insertions, 13 deletions
diff --git a/test/regress/regress0/sygus/pLTL-sygus-syntax-err.sy b/test/regress/regress0/sygus/pLTL-sygus-syntax-err.sy index 848ae0349..6a149cc71 100644 --- a/test/regress/regress0/sygus/pLTL-sygus-syntax-err.sy +++ b/test/regress/regress0/sygus/pLTL-sygus-syntax-err.sy @@ -1,16 +1,16 @@ ; REQUIRES: no-competition ; COMMAND-LINE: --sygus-out=status --sygus-rec-fun --lang=sygus2 ; EXPECT-ERROR: (error "Parse Error: pLTL-sygus-syntax-err.sy:80.19: number of arguments does not match the constructor type -; EXPECT-ERROR: +; EXPECT-ERROR: ; EXPECT-ERROR: (Op2 <O2> <F>) ; EXPECT-ERROR: ^ ; EXPECT-ERROR: ") ; EXIT: 1 -(set-logic ALL) +(set-logic HO_ALL) (set-option :lang sygus2) ;(set-option :sygus-out status) (set-option :sygus-rec-fun true) -(set-option :uf-ho true) + (define-sort Time () Int) @@ -47,19 +47,19 @@ (and (<= 0 t tn) (match f ( ((P i) (val t i)) - - ((Op1 op g) + + ((Op1 op g) (match op ( - (NOT (not (holds g t))) + (NOT (not (holds g t))) - (Y (and (< 0 t) (holds g (- t 1)))) + (Y (and (< 0 t) (holds g (- t 1)))) (G (and (holds g t) (or (= t tn) (holds f (+ t 1))))) (H (and (holds g t) (or (= t 0) (holds f (- t 1))))) ))) - ((Op2 op f g) + ((Op2 op f g) (match op ( (AND (and (holds f t) (holds g t))) @@ -88,6 +88,3 @@ (constraint (holds (Op1 G (phi X0 X1)) 0)) (check-synth) - - - diff --git a/test/regress/regress0/sygus/sygus-uf.sy b/test/regress/regress0/sygus/sygus-uf.sy index b08aa8929..2f59598ec 100644 --- a/test/regress/regress0/sygus/sygus-uf.sy +++ b/test/regress/regress0/sygus/sygus-uf.sy @@ -1,6 +1,6 @@ -; COMMAND-LINE: --lang=sygus2 --sygus-out=status --uf-ho +; COMMAND-LINE: --lang=sygus2 --sygus-out=status ; EXPECT: unsat -(set-logic ALL) +(set-logic HO_ALL) (declare-var uf (-> Int Int)) |