blob: ed1d5c8625f4301d4d60ff5bc9c6d2b846c19fe4 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
|
; REQUIRES: proof
; COMMAND-LINE: --produce-abducts
; COMMAND-LINE: --produce-abducts --sygus-core-connective
; SCRUBBER: grep -v -E '(\(define-fun)'
; EXIT: 0
(set-logic QF_UFLIRA)
(set-option :produce-abducts true)
(declare-fun n () Int)
(declare-fun m () Int)
(declare-fun x () Int)
(declare-fun y () Int)
(assert (>= n 1))
(assert (and (<= n x)(<= x (+ n 5))))
(assert (and (<= 1 y)(<= y m)))
; Generate a predicate A that is consistent with the above axioms (i.e.
; their conjunction is SAT), and is such that the conjunction of the above
; axioms, A and the negation of the conjecture below are UNSAT.
; The signature of A is below grammar.
(get-abduct A (not (< x y))
; the grammar for the abduct-to-synthesize
; notice it does not permit the sygus-core-connective algorithm; this regression
; tests that we ignore this option properly.
((Start Bool) (StartInt Int))
(
(Start Bool ((< StartInt StartInt)))
(StartInt Int (n m (+ StartInt StartInt) 0 1))
)
)
|
