Skip to content

N
NIWO
Commit d362f152 authored by Christian Müller's avatar Christian Müller
Browse files
Options

add parser, add aalta, add main that transforms everything in examples to results

parent 08c66638
Expand all Hide whitespace changes
Inline Side-by-side
Showing with 6560 additions and 3368 deletions
aalta/Aalta_v2.0/Aalta_v2.0/aalta 100644 → 100755
View file @ d362f152
No preview for this file type
aalta/Aalta_v2.0/Aalta_v2.0/ltlparser/grammar/ltllexer.l
View file @ d362f152
......@@ -19,17 +19,17 @@
LPAREN "("
RPAREN ")"
EQUIV "<->"
IMPLIES "->"
OR \|\|?
AND &&?
EQUIV "<->"|"↔"
IMPLIES "->"|"→"
OR "∨"
AND "∧"
RELEASE R|V
UNTIL U
FUTURE F|\<>
GLOBALLY G|\[\]
NEXT X
WEAK_NEXT W
NOT !|~
NOT !|~|"¬"
TRUE 1|[tT]rue|TRUE
FALSE 0|[fF]alse|FALSE
......
aalta/Aalta_v2.0/Aalta_v2.0/ltlparser/grammar/ltllexer.l.bak 0 → 100644
View file @ d362f152
%{
/**
* lellexer.l file
* To generate the lexical analyzer run: "flex ltllexer.l"
*/
#include "ltl_formula.h"
#include "ltlparser.h"
#include <stdio.h>
%}
%option outfile="../ltllexer.c" header-file="../ltllexer.h"
%option warn nodefault
%option reentrant noyywrap never-interactive nounistd
%option bison-bridge
LPAREN "("
RPAREN ")"
EQUIV "<->"
IMPLIES "->"
OR \|\|?
AND &&?
RELEASE R|V
UNTIL U
FUTURE F|\<>
GLOBALLY G|\[\]
NEXT X
WEAK_NEXT W
NOT !|~
TRUE 1|[tT]rue|TRUE
FALSE 0|[fF]alse|FALSE
ID [a-zA-Z_][a-zA-Z0-9_]*
WS [ \r\n\t]*
%%
{LPAREN} { return TOKEN_LPAREN; }
{RPAREN} { return TOKEN_RPAREN; }
{EQUIV} { return TOKEN_EQUIV; }
{IMPLIES} { return TOKEN_IMPLIES; }
{OR} { return TOKEN_OR; }
{AND} { return TOKEN_AND; }
{RELEASE} { return TOKEN_RELEASE; }
{UNTIL} { return TOKEN_UNTIL; }
{FUTURE} { return TOKEN_FUTURE; }
{GLOBALLY} { return TOKEN_GLOBALLY; }
{NEXT} { return TOKEN_NEXT; }
{WEAK_NEXT} { return TOKEN_WEAK_NEXT; }
{NOT} { return TOKEN_NOT; }
{WS} { /* Skip blanks. */ }
{TRUE} { return TOKEN_TRUE; }
{FALSE} { return TOKEN_FALSE; }
{ID} { yylval->var_name = yytext; return TOKEN_VARIABLE; }
. { fprintf(stderr, "\033[31mERROR\033[0m: Unrecognized symbol: \033[34m%s\033[0m\n", yytext); exit(1); }
%%
/*
int yyerror(const char *msg) {
fprintf(stderr,"Error:%s\n",msg);
exit(1);
return 0;
}*/
aalta/Aalta_v2.0/Aalta_v2.0/ltlparser/ltllexer.h
View file @ d362f152
......@@ -12,8 +12,8 @@
#define FLEX_SCANNER
#define YY_FLEX_MAJOR_VERSION 2
#define YY_FLEX_MINOR_VERSION 5
#define YY_FLEX_SUBMINOR_VERSION 37
#define YY_FLEX_MINOR_VERSION 6
#define YY_FLEX_SUBMINOR_VERSION 1
#if YY_FLEX_SUBMINOR_VERSION > 0
#define FLEX_BETA
#endif
......@@ -92,25 +92,13 @@ typedef unsigned int flex_uint32_t;
#endif /* ! FLEXINT_H */
#ifdef __cplusplus
/* The "const" storage-class-modifier is valid. */
#define YY_USE_CONST
#else /* ! __cplusplus */
/* C99 requires __STDC__ to be defined as 1. */
#if defined (__STDC__)
#define YY_USE_CONST
#endif /* defined (__STDC__) */
#endif /* ! __cplusplus */
#ifdef YY_USE_CONST
/* TODO: this is always defined, so inline it */
#define yyconst const
#if defined(__GNUC__) && __GNUC__ >= 3
#define yynoreturn __attribute__((__noreturn__))
#else
#define yyconst
#define yynoreturn
#endif
/* An opaque pointer. */
......@@ -132,7 +120,15 @@ typedef void* yyscan_t;
/* Size of default input buffer. */
#ifndef YY_BUF_SIZE
#ifdef __ia64__
/* On IA-64, the buffer size is 16k, not 8k.
* Moreover, YY_BUF_SIZE is 2*YY_READ_BUF_SIZE in the general case.
* Ditto for the __ia64__ case accordingly.
*/
#define YY_BUF_SIZE 32768
#else
#define YY_BUF_SIZE 16384
#endif /* __ia64__ */
#endif
#ifndef YY_TYPEDEF_YY_BUFFER_STATE
......@@ -157,12 +153,12 @@ struct yy_buffer_state
/* Size of input buffer in bytes, not including room for EOB
* characters.
*/
yy_size_t yy_buf_size;
int yy_buf_size;
/* Number of characters read into yy_ch_buf, not including EOB
* characters.
*/
yy_size_t yy_n_chars;
int yy_n_chars;
/* Whether we "own" the buffer - i.e., we know we created it,
* and can realloc() it to grow it, and should free() it to
......@@ -185,7 +181,7 @@ struct yy_buffer_state
int yy_bs_lineno; /**< The line count. */
int yy_bs_column; /**< The column count. */
/* Whether to try to fill the input buffer when we reach the
* end of it.
*/
......@@ -206,7 +202,7 @@ void yypop_buffer_state (yyscan_t yyscanner );
YY_BUFFER_STATE yy_scan_buffer (char *base,yy_size_t size ,yyscan_t yyscanner );
YY_BUFFER_STATE yy_scan_string (yyconst char *yy_str ,yyscan_t yyscanner );
YY_BUFFER_STATE yy_scan_bytes (yyconst char *bytes,yy_size_t len ,yyscan_t yyscanner );
YY_BUFFER_STATE yy_scan_bytes (yyconst char *bytes,int len ,yyscan_t yyscanner );
void *yyalloc (yy_size_t ,yyscan_t yyscanner );
void *yyrealloc (void *,yy_size_t ,yyscan_t yyscanner );
......@@ -214,7 +210,7 @@ void yyfree (void * ,yyscan_t yyscanner );
/* Begin user sect3 */
#define yywrap(yyscanner) 1
#define yywrap(yyscanner) (/*CONSTCOND*/1)
#define YY_SKIP_YYWRAP
#define yytext_ptr yytext_r
......@@ -255,23 +251,23 @@ void yyset_extra (YY_EXTRA_TYPE user_defined ,yyscan_t yyscanner );
FILE *yyget_in (yyscan_t yyscanner );
void yyset_in (FILE * in_str ,yyscan_t yyscanner );
void yyset_in (FILE * _in_str ,yyscan_t yyscanner );
FILE *yyget_out (yyscan_t yyscanner );
void yyset_out (FILE * out_str ,yyscan_t yyscanner );
void yyset_out (FILE * _out_str ,yyscan_t yyscanner );
yy_size_t yyget_leng (yyscan_t yyscanner );
int yyget_leng (yyscan_t yyscanner );
char *yyget_text (yyscan_t yyscanner );
int yyget_lineno (yyscan_t yyscanner );
void yyset_lineno (int line_number ,yyscan_t yyscanner );
void yyset_lineno (int _line_number ,yyscan_t yyscanner );
int yyget_column (yyscan_t yyscanner );
void yyset_column (int column_no ,yyscan_t yyscanner );
void yyset_column (int _column_no ,yyscan_t yyscanner );
YYSTYPE * yyget_lval (yyscan_t yyscanner );
......@@ -303,7 +299,12 @@ static int yy_flex_strlen (yyconst char * ,yyscan_t yyscanner);
/* Amount of stuff to slurp up with each read. */
#ifndef YY_READ_BUF_SIZE
#ifdef __ia64__
/* On IA-64, the buffer size is 16k, not 8k */
#define YY_READ_BUF_SIZE 16384
#else
#define YY_READ_BUF_SIZE 8192
#endif /* __ia64__ */
#endif
/* Number of entries by which start-condition stack grows. */
......@@ -341,6 +342,6 @@ extern int yylex \
#line 61 "ltllexer.l"
#line 345 "../ltllexer.h"
#line 346 "../ltllexer.h"
#undef yyIN_HEADER
#endif /* yyHEADER_H */
aalta/Aalta_v2.0/Aalta_v2.0/ltlparser/ltlparser.h
View file @ d362f152
/* A Bison parser, made by GNU Bison 2.7. */
/* A Bison parser, made by GNU Bison 3.0.4. */
/* Bison interface for Yacc-like parsers in C
Copyright (C) 1984, 1989-1990, 2000-2012 Free Software Foundation, Inc.
Copyright (C) 1984, 1989-1990, 2000-2015 Free Software Foundation, Inc.
This program is free software: you can redistribute it and/or modify
it under the terms of the GNU General Public License as published by
the Free Software Foundation, either version 3 of the License, or
(at your option) any later version.
This program is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
GNU General Public License for more details.
You should have received a copy of the GNU General Public License
along with this program. If not, see <http://www.gnu.org/licenses/>. */
......@@ -26,13 +26,13 @@
special exception, which will cause the skeleton and the resulting
Bison output files to be licensed under the GNU General Public
License without this special exception.
This special exception was added by the Free Software Foundation in
version 2.2 of Bison. */
#ifndef YY_YY_LTLPARSER_H_INCLUDED
# define YY_YY_LTLPARSER_H_INCLUDED
/* Enabling traces. */
/* Debug traces. */
#ifndef YYDEBUG
# define YYDEBUG 0
#endif
......@@ -40,75 +40,59 @@
extern int yydebug;
#endif
/* "%code requires" blocks. */
/* Line 2058 of yacc.c */
#line 19 "ltlparser.y"
#line 19 "ltlparser.y" /* yacc.c:1909 */
#ifndef YY_TYPEDEF_YY_SCANNER_T
#define YY_TYPEDEF_YY_SCANNER_T
typedef void* yyscan_t;
#endif
#line 51 "../ltlparser.h" /* yacc.c:1909 */
/* Line 2058 of yacc.c */
#line 54 "../ltlparser.h"
/* Tokens. */
/* Token type. */
#ifndef YYTOKENTYPE
# define YYTOKENTYPE
/* Put the tokens into the symbol table, so that GDB and other debuggers
know about them. */
enum yytokentype {
TOKEN_EQUIV = 258,
TOKEN_IMPLIES = 259,
TOKEN_OR = 260,
TOKEN_AND = 261,
TOKEN_RELEASE = 262,
TOKEN_UNTIL = 263,
TOKEN_FUTURE = 264,
TOKEN_GLOBALLY = 265,
TOKEN_NEXT = 266,
TOKEN_WEAK_NEXT = 267,
TOKEN_NOT = 268,
TOKEN_TRUE = 269,
TOKEN_FALSE = 270,
TOKEN_LPAREN = 271,
TOKEN_RPAREN = 272,
TOKEN_VARIABLE = 273
};
enum yytokentype
{
TOKEN_EQUIV = 258,
TOKEN_IMPLIES = 259,
TOKEN_OR = 260,
TOKEN_AND = 261,
TOKEN_RELEASE = 262,
TOKEN_UNTIL = 263,
TOKEN_FUTURE = 264,
TOKEN_GLOBALLY = 265,
TOKEN_NEXT = 266,
TOKEN_WEAK_NEXT = 267,
TOKEN_NOT = 268,
TOKEN_TRUE = 269,
TOKEN_FALSE = 270,
TOKEN_LPAREN = 271,
TOKEN_RPAREN = 272,
TOKEN_VARIABLE = 273
};
#endif
/* Value type. */
#if ! defined YYSTYPE && ! defined YYSTYPE_IS_DECLARED
typedef union YYSTYPE
union YYSTYPE
{
/* Line 2058 of yacc.c */
#line 34 "ltlparser.y"
#line 34 "ltlparser.y" /* yacc.c:1909 */
char* var_name;
ltl_formula *formula;
#line 87 "../ltlparser.h" /* yacc.c:1909 */
};
/* Line 2058 of yacc.c */
#line 93 "../ltlparser.h"
} YYSTYPE;
typedef union YYSTYPE YYSTYPE;
# define YYSTYPE_IS_TRIVIAL 1
# define yystype YYSTYPE /* obsolescent; will be withdrawn */
# define YYSTYPE_IS_DECLARED 1
#endif
#ifdef YYPARSE_PARAM
#if defined __STDC__ || defined __cplusplus
int yyparse (void *YYPARSE_PARAM);
#else
int yyparse ();
#endif
#else /* ! YYPARSE_PARAM */
#if defined __STDC__ || defined __cplusplus
int yyparse (ltl_formula **formula, yyscan_t scanner);
#else
int yyparse ();
#endif
#endif /* ! YYPARSE_PARAM */
#endif /* !YY_YY_LTLPARSER_H_INCLUDED */
aalta/sat_v0.2/minisat/LICENSE
View file @ d362f152
MiniSat -- Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
Copyright (c) 2007-2010 Niklas Sorensson
Permission is hereby granted, free of charge, to any person obtaining a
copy of this software and associated documentation files (the
......
aalta/sat_v0.2/minisat/README
View file @ d362f152
Directory overview:
==================
================================================================================
DIRECTORY OVERVIEW:
mtl/ Mini Template Library
utils/ Generic helper code (I/O, Parsing, CPU-time, etc)
core/ A core version of the solver
simp/ An extended solver with simplification capabilities
README
LICENSE
To build (release version: without assertions, statically linked, etc):
======================================================================
================================================================================
BUILDING: (release version: without assertions, statically linked, etc)
export MROOT=<minisat-dir> (or setenv in cshell)
cd { core | simp }
gmake rs
cp minisat_static <install-dir>/minisat
Usage:
======
================================================================================
EXAMPLES:
TODO
Run minisat with same heuristics as version 2.0:
> minisat <cnf-file> -no-luby -rinc=1.5 -phase-saving=0 -rnd-freq=0.02
aalta/sat_v0.2/minisat/mtl/BasicHeap.h → aalta/sat_v0.2/minisat/core/Dimacs.h
View file @ d362f152
/******************************************************************************************[Heap.h]
MiniSat -- Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
/****************************************************************************************[Dimacs.h]
Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
Copyright (c) 2007-2010, Niklas Sorensson
Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
associated documentation files (the "Software"), to deal in the Software without restriction,
......@@ -17,82 +18,72 @@ DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE,
OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
**************************************************************************************************/
#ifndef BasicHeap_h
#define BasicHeap_h
#ifndef Minisat_Dimacs_h
#define Minisat_Dimacs_h
#include "Vec.h"
#include <stdio.h>
//=================================================================================================
// A heap implementation with support for decrease/increase key.
template<class Comp>
class BasicHeap {
Comp lt;
vec<int> heap; // heap of ints
// Index "traversal" functions
static inline int left (int i) { return i*2+1; }
static inline int right (int i) { return (i+1)*2; }
static inline int parent(int i) { return (i-1) >> 1; }
inline void percolateUp(int i)
{
int x = heap[i];
while (i != 0 && lt(x, heap[parent(i)])){
heap[i] = heap[parent(i)];
i = parent(i);
}
heap [i] = x;
}
#include "utils/ParseUtils.h"
#include "core/SolverTypes.h"
namespace Minisat {
inline void percolateDown(int i)
{
int x = heap[i];
while (left(i) < heap.size()){
int child = right(i) < heap.size() && lt(heap[right(i)], heap[left(i)]) ? right(i) : left(i);
if (!lt(heap[child], x)) break;
heap[i] = heap[child];
i = child;
}
heap[i] = x;
//=================================================================================================
// DIMACS Parser:
template<class B, class Solver>
static void readClause(B& in, Solver& S, vec<Lit>& lits) {
int parsed_lit, var;
lits.clear();
for (;;){
parsed_lit = parseInt(in);
if (parsed_lit == 0) break;
var = abs(parsed_lit)-1;
while (var >= S.nVars()) S.newVar();
lits.push( (parsed_lit > 0) ? mkLit(var) : ~mkLit(var) );
}
bool heapProperty(int i) {
return i >= heap.size()
|| ((i == 0 || !lt(heap[i], heap[parent(i)])) && heapProperty(left(i)) && heapProperty(right(i))); }
public:
BasicHeap(const C& c) : comp(c) { }
int size () const { return heap.size(); }
bool empty () const { return heap.size() == 0; }
int operator[](int index) const { return heap[index+1]; }
void clear (bool dealloc = false) { heap.clear(dealloc); }
void insert (int n) { heap.push(n); percolateUp(heap.size()-1); }
int removeMin() {
int r = heap[0];
heap[0] = heap.last();
heap.pop();
if (heap.size() > 1) percolateDown(0);
return r;
}
template<class B, class Solver>
static void parse_DIMACS_main(B& in, Solver& S) {
vec<Lit> lits;
int vars = 0;
int clauses = 0;
int cnt = 0;
for (;;){
skipWhitespace(in);
if (*in == EOF) break;
else if (*in == 'p'){
if (eagerMatch(in, "p cnf")){
vars = parseInt(in);
clauses = parseInt(in);
// SATRACE'06 hack
// if (clauses > 4000000)
// S.eliminate(true);
}else{
printf("PARSE ERROR! Unexpected char: %c\n", *in), exit(3);
}
} else if (*in == 'c' || *in == 'p')
skipLine(in);
else{
cnt++;
readClause(in, S, lits);
S.addClause_(lits); }
}
// DEBUG: consistency checking
bool heapProperty() {
return heapProperty(1); }
// COMPAT: should be removed
int getmin () { return removeMin(); }
};
if (vars != S.nVars())
fprintf(stderr, "WARNING! DIMACS header mismatch: wrong number of variables.\n");
if (cnt != clauses)
fprintf(stderr, "WARNING! DIMACS header mismatch: wrong number of clauses.\n");
}
// Inserts problem into solver.
//
template<class Solver>
static void parse_DIMACS(gzFile input_stream, Solver& S) {
StreamBuffer in(input_stream);
parse_DIMACS_main(in, S); }
//=================================================================================================
}
#endif
aalta/sat_v0.2/minisat/core/Main.C deleted 100644 → 0
View file @ 08c66638
This diff is collapsed.
aalta/sat_v0.2/minisat/core/Main.cc 0 → 100644
View file @ d362f152
/*****************************************************************************************[Main.cc]
Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
Copyright (c) 2007-2010, Niklas Sorensson
Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
associated documentation files (the "Software"), to deal in the Software without restriction,
including without limitation the rights to use, copy, modify, merge, publish, distribute,
sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
furnished to do so, subject to the following conditions:
The above copyright notice and this permission notice shall be included in all copies or
substantial portions of the Software.
THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT
NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT
OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
**************************************************************************************************/
#include <errno.h>
#include <signal.h>
#include <zlib.h>
#include "utils/System.h"
#include "utils/ParseUtils.h"
#include "utils/Options.h"
#include "core/Dimacs.h"
#include "core/Solver.h"
using namespace Minisat;
//=================================================================================================
void printStats(Solver& solver)
{
double cpu_time = cpuTime();
double mem_used = memUsedPeak();
printf("restarts : %"PRIu64"\n", solver.starts);
printf("conflicts : %-12"PRIu64" (%.0f /sec)\n", solver.conflicts , solver.conflicts /cpu_time);
printf("decisions : %-12"PRIu64" (%4.2f %% random) (%.0f /sec)\n", solver.decisions, (float)solver.rnd_decisions*100 / (float)solver.decisions, solver.decisions /cpu_time);
printf("propagations : %-12"PRIu64" (%.0f /sec)\n", solver.propagations, solver.propagations/cpu_time);
printf("conflict literals : %-12"PRIu64" (%4.2f %% deleted)\n", solver.tot_literals, (solver.max_literals - solver.tot_literals)*100 / (double)solver.max_literals);
if (mem_used != 0) printf("Memory used : %.2f MB\n", mem_used);
printf("CPU time : %g s\n", cpu_time);
}
static Solver* solver;
// Terminate by notifying the solver and back out gracefully. This is mainly to have a test-case
// for this feature of the Solver as it may take longer than an immediate call to '_exit()'.
static void SIGINT_interrupt(int signum) { solver->interrupt(); }
// Note that '_exit()' rather than 'exit()' has to be used. The reason is that 'exit()' calls
// destructors and may cause deadlocks if a malloc/free function happens to be running (these
// functions are guarded by locks for multithreaded use).
static void SIGINT_exit(int signum) {
printf("\n"); printf("*** INTERRUPTED ***\n");
if (solver->verbosity > 0){
printStats(*solver);
printf("\n"); printf("*** INTERRUPTED ***\n"); }
_exit(1); }
//=================================================================================================
// Main:
int main(int argc, char** argv)
{
try {
setUsageHelp("USAGE: %s [options] <input-file> <result-output-file>\n\n where input may be either in plain or gzipped DIMACS.\n");
// printf("This is MiniSat 2.0 beta\n");
#if defined(__linux__)
fpu_control_t oldcw, newcw;
_FPU_GETCW(oldcw); newcw = (oldcw & ~_FPU_EXTENDED) | _FPU_DOUBLE; _FPU_SETCW(newcw);
printf("WARNING: for repeatability, setting FPU to use double precision\n");
#endif
// Extra options:
//
IntOption verb ("MAIN", "verb", "Verbosity level (0=silent, 1=some, 2=more).", 1, IntRange(0, 2));
IntOption cpu_lim("MAIN", "cpu-lim","Limit on CPU time allowed in seconds.\n", INT32_MAX, IntRange(0, INT32_MAX));
IntOption mem_lim("MAIN", "mem-lim","Limit on memory usage in megabytes.\n", INT32_MAX, IntRange(0, INT32_MAX));
parseOptions(argc, argv, true);
Solver S;
double initial_time = cpuTime();
S.verbosity = verb;
solver = &S;
// Use signal handlers that forcibly quit until the solver will be able to respond to
// interrupts:
signal(SIGINT, SIGINT_exit);
signal(SIGXCPU,SIGINT_exit);
// Set limit on CPU-time:
if (cpu_lim != INT32_MAX){
rlimit rl;
getrlimit(RLIMIT_CPU, &rl);
if (rl.rlim_max == RLIM_INFINITY || (rlim_t)cpu_lim < rl.rlim_max){
rl.rlim_cur = cpu_lim;
if (setrlimit(RLIMIT_CPU, &rl) == -1)
printf("WARNING! Could not set resource limit: CPU-time.\n");
} }
// Set limit on virtual memory: