diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-05-05 18:44:47 -0500 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-05-05 18:44:56 -0500 |
commit | c87ee73ad3d51c238700f236c18e425b80e8e7ac (patch) | |
tree | aa4214b0fa7d6ef275605253fee88899fa3ce230 /test/regress/regress0/sygus/strings-small.sy | |
parent | a2923ec61b601b0e3f4f78f22fffc1c2421f0d81 (diff) |
Compute term indices lazily in TermDb. Optimization for qcf to recognize irrelevant quantifiers based on irrelevant functions. Fix rewriter for prefix merges. Minor optimizations for LFSC. Work on --literal-matching. Updates to inst propagate, move instantiation filtering within qe. Enable sygus for string inputs.
Diffstat (limited to 'test/regress/regress0/sygus/strings-small.sy')
-rw-r--r-- | test/regress/regress0/sygus/strings-small.sy | 35 |
1 files changed, 35 insertions, 0 deletions
diff --git a/test/regress/regress0/sygus/strings-small.sy b/test/regress/regress0/sygus/strings-small.sy new file mode 100644 index 000000000..bc559f94a --- /dev/null +++ b/test/regress/regress0/sygus/strings-small.sy @@ -0,0 +1,35 @@ +; EXPECT: unsat +; COMMAND-LINE: --cegqi-si --no-dump-synth +(set-logic SLIA) +(synth-fun f ((firstname String) (lastname String)) String +((Start String (ntString)) + +(ntString String ( +firstname +lastname +" " +(str.++ ntString ntString))) + +(ntInt Int ( +0 +1 +2 +(+ ntInt ntInt) +(- ntInt ntInt) +(str.len ntString) +(str.to.int ntString) +(str.indexof ntString ntString ntInt))) + +(ntBool Bool ( +true +false +(str.prefixof ntString ntString) +(str.suffixof ntString ntString) +(str.contains ntString ntString))) + +)) + +(constraint (= (f "Nancy" "FreeHafer") "Nancy FreeHafer")) + +(check-synth) + |