diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-11-25 17:59:51 -0600 |
---|---|---|
committer | Haniel Barbosa <hanielbbarbosa@gmail.com> | 2019-11-25 20:59:51 -0300 |
commit | 89e00fbfffdbf3f7acde46623bf7a54f455614b5 (patch) | |
tree | 701cf4218158c294e7cc5e499865a033abc8d5c4 /test/regress/regress0/sygus | |
parent | eff8e6a30d348e2418f805602d3dd41ac2bc795b (diff) |
Better front-end type checking for SyGuS (#3496)
Diffstat (limited to 'test/regress/regress0/sygus')
-rw-r--r-- | test/regress/regress0/sygus/pLTL-sygus-syntax-err.sy | 92 |
1 files changed, 92 insertions, 0 deletions
diff --git a/test/regress/regress0/sygus/pLTL-sygus-syntax-err.sy b/test/regress/regress0/sygus/pLTL-sygus-syntax-err.sy new file mode 100644 index 000000000..7a90d7427 --- /dev/null +++ b/test/regress/regress0/sygus/pLTL-sygus-syntax-err.sy @@ -0,0 +1,92 @@ +; COMMAND-LINE: --sygus-out=status --sygus-rec-fun --lang=sygus2 +; EXPECT-ERROR: CVC4 Error: +; EXPECT-ERROR: Parse Error: pLTL-sygus-syntax-err.sy:79.19: number of arguments does not match the constructor type +; EXPECT-ERROR: +; EXPECT-ERROR: (Op2 <O2> <F>) +; EXPECT-ERROR: ^ +; EXIT: 1 +(set-logic 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) + +(declare-datatype Var ( (X0) (X1) )) + +; Declare Unary Operators. +(declare-datatype UNARY_OP ( (NOT) (Y) (G) (H) )) + +; Declare Binary Operators. +(declare-datatype BINARY_OP ( (AND) (OR) (IMPLIES) )) ; (S) )) + +; Formula Declaration. +(declare-datatype Formula ( + (P (Id Var)) + (Op1 (op1 UNARY_OP) (f Formula)) + (Op2 (op2 BINARY_OP) (f1 Formula) (f2 Formula)) + ) +) + +; Trace Length. +(declare-const tn Int) +(assert (= tn 2)) + +;cTrace Declaration (trace_index, variable_index) +(define-fun val ((i Int) (x Var)) Bool + (or (and (= i 0) (= x X0)) + (and (= i 0) (= x X1)) + (and (= i 1) (= x X1)) + ) +) + +;cpLTL Semantics +(define-fun-rec holds ((f Formula) (t Time)) Bool + (and (<= 0 t tn) + (match f ( + ((P i) (val t i)) + + ((Op1 op g) + (match op ( + (NOT (not (holds g t))) + + (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) + (match op ( + (AND (and (holds f t) (holds g t))) + + (OR (or (holds f t) (holds g t))) + + (IMPLIES (or (not (holds f t)) (holds g t))) + ))))) + ) +) + +(synth-fun phi ((x0 Var) (x1 Var)) Formula + ((<F> Formula) (<O1> UNARY_OP) (<O2> BINARY_OP)) + ( + (<F> Formula ( + (P x0) + (P x1) + (Op1 <O1> <F>) + (Op2 <O2> <F>) + ) + ) + (<O1> UNARY_OP (NOT Y G H)) + (<O2> BINARY_OP (AND OR IMPLIES)) + ) +) + +(constraint (holds (Op1 G (phi X0 X1)) 0)) + +(check-synth) + + + |