diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-01-14 14:42:44 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-01-14 14:42:44 -0600 |
commit | 9e94e0bfcf55cf4f11afaacfc2d9e03f2a259236 (patch) | |
tree | d5ec8956dc69c010b9614f89a01b8ccff0f693a3 /test | |
parent | 32c3001c293f50f53cc7a4ae35bd28966dfdd412 (diff) |
Generalize example-based sym breaking to conjectures with constant function apps (#3605)
Diffstat (limited to 'test')
-rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
-rw-r--r-- | test/regress/regress1/sygus/pLTL_5_trace.sy | 90 |
2 files changed, 91 insertions, 0 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 03d38df5e..a04619342 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1804,6 +1804,7 @@ set(regress_1_tests regress1/sygus/phone-1-long.sy regress1/sygus/planning-unif.sy regress1/sygus/process-10-vars.sy + regress1/sygus/pLTL_5_trace.sy regress1/sygus/qe.sy regress1/sygus/qf_abv.smt2 regress1/sygus/real-any-const.sy diff --git a/test/regress/regress1/sygus/pLTL_5_trace.sy b/test/regress/regress1/sygus/pLTL_5_trace.sy new file mode 100644 index 000000000..532a8f3a8 --- /dev/null +++ b/test/regress/regress1/sygus/pLTL_5_trace.sy @@ -0,0 +1,90 @@ +; EXPECT: unsat +; COMMAND-LINE: --sygus-out=status --lang=sygus2 +(set-logic BV) + +;Trace length +(define-sort Stream () (_ BitVec 48)) +(define-fun ZERO () Stream (_ bv0 48)) +(define-fun ONE () Stream (_ bv1 48)) + + +(define-fun S_FALSE () Stream ZERO) +(define-fun S_TRUE () Stream (bvnot S_FALSE)) + +; Yesterday: X << 1 +(define-fun + Y ( (X Stream) ) Stream + (bvshl X ONE) +) + +; Once: X|-X +(define-fun + O ( (X Stream) ) Stream + (bvor X (bvneg X)) +) + +; Historically: X & ~(1 + X) +(define-fun + H ( (X Stream) ) Stream + (bvand X (bvnot (bvadd ONE X))) +) + +; Since: Z | (X & ~((X | Z) + Z)) +(define-fun +S ( (X Stream) (Z Stream) ) Stream + (bvor Z + (bvand X + (bvnot (bvadd (bvor X Z) Z )) + ) + ) +) + +(define-fun + bvimpl ( (X Stream) (Z Stream) ) Stream + (bvor (bvnot X) Z) +) + +(synth-fun phi ((ulInformationTransfer Stream) (dlInformationTransfer Stream) (rrcConnectionReconfiguration Stream) (measurementReport Stream) (systemInformationBlockType1 Stream) (securityModeComplete Stream) (systemInformation Stream) (rrcConnectionReestablishmentReject Stream) (rrcConnectionRequest Stream) (rrcConnectionSetupComplete Stream) (rrcConnectionRelease Stream) (ueCapabilityInformation Stream) (rrcConnectionSetup Stream) (securityModeCommand Stream) (ueCapabilityEnquiry Stream) (rrcConnectionReconfigurationComplete Stream) (rrcConnectionReestablishmentRequest Stream)) Stream + ((<F> Stream)) + ((<F> Stream ( + S_TRUE + S_FALSE + ( Variable Stream ) + (bvnot <F>) + (bvand <F> <F>) + (bvor <F> <F>) + (bvimpl <F> <F>) + (Y <F>) + (O <F>) + (H <F>) + (S <F> <F>) + ))) +) + +;; Positive examples +;Positive Trace Data +(constraint + (and + (= ((_ extract 8 0) (phi #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000100000 #b000000000000000000000000000000000000000011000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000010000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000001 #b000000000000000000000000000000000000000000000100 #b000000000000000000000000000000000000000100000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000010 #b000000000000000000000000000000000000000000001000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000000)) ((_ extract 8 0) S_TRUE)) + (= (phi #b000000000000000000000100000000100000000000000000 #b000000000000000000000010000000000000000000000000 #b000000101000000001010000000100000100001000100000 #b000000000100000000001000000000000010100000000000 #b000010000001000100000001000000010000000000000000 #b000000000000000000000000000000000000000000010000 #b001100000010111000000000110011000001000000000000 #b100000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000001 #b000000000000000000000000000000000000000000000100 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000100000000 #b000000000000000000000000000000000000000000000010 #b000000000000000000000000000000000000000000001000 #b000000000000000000000000000000000000000010000000 #b000001010000000010100000001000001000010001000000 #b010000000000000000000000000000000000000000000000) S_TRUE) + (= ((_ extract 15 0) (phi #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000010000010100000 #b000000000000000000000000000000000001100000000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000010000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000001 #b000000000000000000000000000000000000000000000100 #b000000000000000000000000000000001000000000000000 #b000000000000000000000000000000000000010000000000 #b000000000000000000000000000000000000000000000010 #b000000000000000000000000000000000000000000001000 #b000000000000000000000000000000000000001000000000 #b000000000000000000000000000000000100000101000000 #b000000000000000000000000000000000000000000000000)) ((_ extract 15 0) S_TRUE)) + (= ((_ extract 15 0) (phi #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000010001000000 #b000000000000000000000000000000000111000000000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000100000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000001 #b000000000000000000000000000000000000000000000100 #b000000000000000000000000000000001000000000000000 #b000000000000000000000000000000000000001000000000 #b000000000000000000000000000000000000000000001010 #b000000000000000000000000000000000000000000010000 #b000000000000000000000000000000000000000100000000 #b000000000000000000000000000000000000100010000000 #b000000000000000000000000000000000000000000000000)) ((_ extract 15 0) S_TRUE)) + (= ((_ extract 20 0) (phi #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000001001001010100000 #b000000000000000000000000000000000000100000000000 #b000000000000000000000000000010000100000000000000 #b000000000000000000000000000000000000000000010000 #b000000000000000000000000000001100000000000000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000001 #b000000000000000000000000000000000000000000000100 #b000000000000000000000000000100000000000000000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000010 #b000000000000000000000000000000000000000000001000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000010010010101000000 #b000000000000000000000000000000000000000000000000)) ((_ extract 20 0) S_TRUE)) + ) +) + +;; Negative examples + +;Negative Trace Data +(constraint + (and + (not (= ((_ extract 6 0) (phi #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000001000 #b000000000000000000000000000000000000000000110000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000001 #b000000000000000000000000000000000000000000000100 #b000000000000000000000000000000000000000001000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000010 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000000)) ((_ extract 6 0) S_TRUE))) + (not (= ((_ extract 45 0) (phi #b000000000000000000000001000000001000000000000000 #b000000000000000000000000100000000000000000000000 #b000000001010000000010100000001000001000010001000 #b000000000001000000000010000000000000101000000000 #b000000100000010001000000010000000100000000000000 #b000000000000000000000000000000000000000000000000 #b000011000000101110000000001100110000010000000000 #b001000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000001 #b000000000000000000000000000000000000000000000100 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000001000000 #b000000000000000000000000000000000000000000000010 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000100000 #b000000010100000000101000000010000010000100010000 #b000100000000000000000000000000000000000000000000)) ((_ extract 45 0) S_TRUE))) + (not (= ((_ extract 13 0) (phi #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000100000101000 #b000000000000000000000000000000000000011000000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000001 #b000000000000000000000000000000000000000000000100 #b000000000000000000000000000000000010000000000000 #b000000000000000000000000000000000000000100000000 #b000000000000000000000000000000000000000000000010 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000010000000 #b000000000000000000000000000000000001000001010000 #b000000000000000000000000000000000000000000000000)) ((_ extract 13 0) S_TRUE))) + (not (= ((_ extract 13 0) (phi #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000100010000 #b000000000000000000000000000000000001110000000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000001 #b000000000000000000000000000000000000000000000100 #b000000000000000000000000000000000010000000000000 #b000000000000000000000000000000000000000010000000 #b000000000000000000000000000000000000000000001010 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000001000000 #b000000000000000000000000000000000000001000100000 #b000000000000000000000000000000000000000000000000)) ((_ extract 13 0) S_TRUE))) + (not (= ((_ extract 18 0) (phi #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000010010010101000 #b000000000000000000000000000000000000001000000000 #b000000000000000000000000000000100001000000000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000011000000000000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000001 #b000000000000000000000000000000000000000000000100 #b000000000000000000000000000001000000000000000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000010 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000000000000000000 #b000000000000000000000000000000000100100101010000 #b000000000000000000000000000000000000000000000000)) ((_ extract 18 0) S_TRUE))) + ) +) + +; Solution: G (p -> O f) +(check-synth) |