Login or Register to Ask a Question and Join Our Community

Sponsored Content
Full Discussion: how to split this file into blocks and then send these blocks as input to the tool called Yices?
Top Forums Shell Programming and Scripting how to split this file into blocks and then send these blocks as input to the tool called Yices? Post 302481187 by R0H0N on Friday 17th of December 2010 01:05:07 AM
Old 12-17-2010
Code:
$ split -l 5 FILE.TXT spl

This will split FILE.TXT in spla and splb as below.
Code:
$ cat spla
(define argc :: int)
(assert ( > argc 1))
(assert ( = argc 1))
<check>
#
$ cat splb
(define c :: float)
(assert ( > c 0))
(assert ( = c 0))
<check>
#

Now u can use this files as input to yices tool.
Code:
yices < `ls spl* | xargs`

This User Gave Thanks to For This Post:
paramad
R0H0N
 

10 More Discussions You Might Find Interesting

1. Shell Programming and Scripting

Delete blocks of lines from text file

Hello, Hello Firends, I have file like below. I want to remove selected blocks say abc,pqr,lst. how can i remove those blocks from file. zone abc { blah blah blah } zone xyz { blah blah blah } zone pqr { blah blah blah } (4 Replies)
Discussion started by: nrbhole
4 Replies

2. Solaris

Why does the # of blocks change for a file on a ZFS filesystem?

I created a zpool and zfs filesystem in OpenSolaris. I made two NFS mount points: > zpool history History for 'raidpool': 2009-01-15.17:12:48 zpool create -f raidpool raidz1 c4t1d0 c4t2d0 c4t3d0 c4t4d0 c4t5d0 2009-01-15.17:15:54 zfs create -o mountpoint=/vol01 -o sharenfs=on -o... (0 Replies)
Discussion started by: sqa777
0 Replies

3. Shell Programming and Scripting

extract blocks of text from a file

Hi, This is part of a large text file I need to separate out. I'd like some help to build a shell script that will extract the text between sets of dashed lines, write that to a new file using the whole or part of the first text string as the new file name, then move on to the next one and... (7 Replies)
Discussion started by: cajunfries
7 Replies

4. Shell Programming and Scripting

Removing blocks from a file

I have a file like the one below. Each record is separated with > In between I have lines consisting of 3 numeric values separated by a space. I need to take each block between the > sign and read the first number in the line. Then take the first after the > sign and the last before the >... (7 Replies)
Discussion started by: kristinu
7 Replies

5. UNIX for Dummies Questions & Answers

Convert 512-blocks to 4k blocks

I'm Unix. I'm looking at "df" on Unix now and below is an example. It's lists the filesystems out in 512-blocks, I need this in 4k blocks. Is there a way to do this in Unix or do I manually convert and how? So for container 1 there is 7,340,032 in size in 512-blocks. What would the 4k block be... (2 Replies)
Discussion started by: rockycj
2 Replies

6. Shell Programming and Scripting

Extracting data blocks from file

Hi all, I want to extract blocks of data from a file depending on the contents of that block. The input file(table) has several blocks each starting with 'gene' in the first column. I want to extract only those blocks which do not have the expression '_T02' in the second column. Input file ... (3 Replies)
Discussion started by: newbie83
3 Replies

7. Shell Programming and Scripting

Row blocks to column blocks

Hello, Searched for a while and found some "line-to-column" script. My case is similar but with multiple fields each row: S02 Length Per S02 7043 3.864 S02 54477 29.89 S02 104841 57.52 S03 Length Per S03 1150 0.835 S03 1321 0.96 S03 ... (9 Replies)
Discussion started by: yifangt
9 Replies

8. Shell Programming and Scripting

Adding and removing blocks of text from file

Hello all, short story: I'm writing a script to add and remove dns records in dns files. Its on a RHEL 5.5 So far i've locked up the basic operations in a couple of functions: - validate the parameters - search for existant ip in file when adding - search for existant name records in... (6 Replies)
Discussion started by: maverick72
6 Replies

9. Shell Programming and Scripting

How to remove duplicate text blocks from a file?

Hi All I have a list of files which will have duplicate list of blocks of text. Following is a sample of the file, I have removed the sensitive information from the file. All the code samples starts from <TR BGCOLOR="white"> and Ends with IP address and two html tags like this. 10.14.22.22... (3 Replies)
Discussion started by: mahasona
3 Replies

10. Shell Programming and Scripting

How to Split a file -- so that each file has N number of Blocks?

Using Linux ,trying to come up with a shell script to automate below but not able to I have a input XML file (XML.txt) with over 200,00 XML blocks, I need to inject this XML file into an application queue for processing, but due to resource contraints I will need to split them up so that each... (5 Replies)
Discussion started by: alldbest
5 Replies

LEARN ABOUT MOJAVE

locale::codes::langfam5.18

Locale::Codes::LangFam(3pm)				 Perl Programmers Reference Guide			       Locale::Codes::LangFam(3pm)

NAME

       Locale::Codes::LangFam - standard codes for language extension identification

SYNOPSIS

	  use Locale::Codes::LangFam;

	  $lext = code2langfam('apa');		       # $lext gets 'Apache languages'
	  $code = langfam2code('Apache languages');    # $code gets 'apa'

	  @codes   = all_langfam_codes();
	  @names   = all_langfam_names();

DESCRIPTION

       The "Locale::Codes::LangFam" module provides access to standard codes used for identifying language families, such as those as defined in
       ISO 639-5.

       Most of the routines take an optional additional argument which specifies the code set to use. If not specified, the default ISO 639-5
       language family codes will be used.

SUPPORTED CODE SETS

       There are several different code sets you can use for identifying language families. A code set may be specified using either a name, or a
       constant that is automatically exported by this module.

       For example, the two are equivalent:

	  $lext = code2langfam('apa','alpha');
	  $lext = code2langfam('apa',LOCALE_LANGFAM_ALPHA);

       The codesets currently supported are:

       alpha
	   This is the set of three-letter (lowercase) codes from ISO 639-5 such as 'apa' for Apache languages.

	   This is the default code set.

ROUTINES

       code2langfam ( CODE [,CODESET] )
       langfam2code ( NAME [,CODESET] )
       langfam_code2code ( CODE ,CODESET ,CODESET2 )
       all_langfam_codes ( [CODESET] )
       all_langfam_names ( [CODESET] )
       Locale::Codes::LangFam::rename_langfam  ( CODE ,NEW_NAME [,CODESET] )
       Locale::Codes::LangFam::add_langfam  ( CODE ,NAME [,CODESET] )
       Locale::Codes::LangFam::delete_langfam  ( CODE [,CODESET] )
       Locale::Codes::LangFam::add_langfam_alias  ( NAME ,NEW_NAME )
       Locale::Codes::LangFam::delete_langfam_alias  ( NAME )
       Locale::Codes::LangFam::rename_langfam_code  ( CODE ,NEW_CODE [,CODESET] )
       Locale::Codes::LangFam::add_langfam_code_alias  ( CODE ,NEW_CODE [,CODESET] )
       Locale::Codes::LangFam::delete_langfam_code_alias  ( CODE [,CODESET] )
	   These routines are all documented in the Locale::Codes::API man page.

SEE ALSO

       Locale::Codes
	   The Locale-Codes distribution.

       Locale::Codes::API
	   The list of functions supported by this module.

       http://www.loc.gov/standards/iso639-5/id.php
	   ISO 639-5 .

AUTHOR

       See Locale::Codes for full author history.

       Currently maintained by Sullivan Beck (sbeck@cpan.org).

COPYRIGHT

	  Copyright (c) 2011-2013 Sullivan Beck

       This module is free software; you can redistribute it and/or modify it under the same terms as Perl itself.

perl v5.18.2							    2013-11-04					       Locale::Codes::LangFam(3pm)
All times are GMT -4. The time now is 11:55 AM.
Unix & Linux Forums Content Copyright 1993-2022. All Rights Reserved.
Privacy Policy