Reorganizing the code

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

src/assertion_set/st2tactic.cpp

@@ -0,0 +1,77 @@
+/*++
+Copyright (c) 2012 Microsoft Corporation
+
+Module Name:
+
+    st2tactic.h
+
+Abstract:
+
+    Temporary adapter that converts a assertion_set_strategy into a tactic.
+
+Author:
+
+    Leonardo (leonardo) 2012-02-19
+
+Notes:
+
+--*/
+#include"assertion_set_strategy.h"
+#include"tactic.h"
+
+class st2tactic_wrapper : public tactic {
+    assertion_set_strategy * m_st;
+    params_ref               m_params;
+public:
+    st2tactic_wrapper(assertion_set_strategy * st):m_st(st) {}
+    ~st2tactic_wrapper() { dealloc(m_st); }
+
+    virtual tactic * translate(ast_manager & m) {
+        // st2tactic_wrapper is a temporary hack to support the old strategy framework.
+        // This class will be deleted in the future.
+        UNREACHABLE();
+        NOT_IMPLEMENTED_YET();
+        return 0;
+    }
+
+    virtual void operator()(goal_ref const & g, goal_ref_buffer & result, model_converter_ref & mc, proof_converter_ref & pc, expr_dependency_ref & core) {
+        SASSERT(g->is_well_sorted());
+        pc = 0; mc = 0; core = 0;
+        fail_if_unsat_core_generation("st2tactic", g);
+        assertion_set s(g->m());
+        for (unsigned i = 0; i < g->size(); i++)
+            s.assert_expr(g->form(i), g->pr(i));
+        if (g->models_enabled()) {
+            params_ref mp = m_params;
+            mp.set_bool(":produce-models", true);
+            m_st->updt_params(mp);
+        }
+        try {
+            (*m_st)(s, mc);
+        }
+        catch (strategy_exception & ex) {
+            throw tactic_exception(ex.msg());
+        }
+        g->reset();
+        for (unsigned i = 0; i < s.size(); i++) {
+            g->assert_expr(s.form(i), s.pr(i), 0);
+        }
+        g->inc_depth();
+        result.push_back(g.get());
+        SASSERT(g->is_well_sorted());
+    }
+
+    virtual void updt_params(params_ref const & p) { m_params = p; m_st->updt_params(p); }
+    virtual void collect_param_descrs(param_descrs & r) { m_st->collect_param_descrs(r); }
+    virtual void cleanup() { m_st->cleanup(); }
+    virtual void set_cancel(bool f) { m_st->set_cancel(f); }
+    virtual void collect_statistics(statistics & st) const { m_st->collect_statistics(st); }
+    virtual void reset_statistics() { m_st->reset_statistics(); }
+    virtual void set_front_end_params(front_end_params & p) { m_st->set_front_end_params(p); }
+    virtual void set_logic(symbol const & l) { m_st->set_logic(l); }
+    virtual void set_progress_callback(progress_callback * callback) { m_st->set_progress_callback(callback); }
+};
+
+tactic * st2tactic(assertion_set_strategy * st) {
+    return alloc(st2tactic_wrapper, st);
+}

src/assertion_set/st2tactic.h

@@ -0,0 +1,27 @@
+/*++
+Copyright (c) 2012 Microsoft Corporation
+
+Module Name:
+
+    st2tactic.h
+
+Abstract:
+
+    Temporary adapter that converts a assertion_set_strategy into a tactic.
+
+Author:
+
+    Leonardo (leonardo) 2012-02-19
+
+Notes:
+
+--*/
+#ifndef _ST2TACTIC_H_
+#define _ST2TACTIC_H_
+
+class tactic;
+class assertion_set_strategy;
+
+tactic * st2tactic(assertion_set_strategy * st);
+
+#endif

src/parser_util/cost_parser.cpp

@@ -0,0 +1,70 @@
+/*++
+Copyright (c) 2006 Microsoft Corporation
+
+Module Name:
+
+    cost_parser.cpp
+
+Abstract:
+
+    <abstract>
+
+Author:
+
+    Leonardo de Moura (leonardo) 2008-06-14.
+
+Revision History:
+
+--*/
+#include"cost_parser.h"
+
+cost_parser::cost_parser(ast_manager & m):
+    simple_parser(m),
+    m_util(m),
+    m_vars(m) {
+    family_id fid;
+    fid = m.get_basic_family_id();
+    add_builtin_op("true",    fid, OP_TRUE);
+    add_builtin_op("false",   fid, OP_FALSE);
+    add_builtin_op("not",     fid, OP_NOT);
+    add_builtin_op("and",     fid, OP_AND);
+    add_builtin_op("implies", fid, OP_IMPLIES);
+    add_builtin_op("or",      fid, OP_OR);
+    add_builtin_op("ite",     fid, OP_ITE);
+    add_builtin_op("=",       fid, OP_EQ);
+    add_builtin_op("iff",     fid, OP_IFF);
+    add_builtin_op("xor",     fid, OP_XOR);
+
+    fid = m_util.get_family_id();
+    add_builtin_op("+",  fid, OP_ADD);
+    add_builtin_op("*",  fid, OP_MUL);
+    add_builtin_op("-",  fid, OP_SUB);
+    add_builtin_op("/",  fid, OP_DIV);
+    add_builtin_op("<=", fid, OP_LE);
+    add_builtin_op(">=", fid, OP_GE);
+    add_builtin_op("<",  fid, OP_LT);
+    add_builtin_op(">",  fid, OP_GT);
+}
+
+expr * cost_parser::parse_int(rational const & r) {
+    return m_util.mk_numeral(r, false);
+}
+
+expr * cost_parser::parse_float(rational const & r) {
+    return m_util.mk_numeral(r, false);
+}
+
+unsigned cost_parser::add_var(symbol name) {
+    sort * real = m_util.mk_real();
+    unsigned r  = m_vars.size();
+    var * v     = m_manager.mk_var(r, real);
+    simple_parser::add_var(name, v);
+    m_vars.push_back(v);
+    return r;
+}
+
+void cost_parser::reset_vars() { 
+    simple_parser::reset_vars(); 
+    m_vars.reset(); 
+}
+

src/parser_util/cost_parser.h

@@ -0,0 +1,39 @@
+/*++
+Copyright (c) 2006 Microsoft Corporation
+
+Module Name:
+
+    cost_parser.h
+
+Abstract:
+
+    <abstract>
+
+Author:
+
+    Leonardo de Moura (leonardo) 2008-06-14.
+
+Revision History:
+
+--*/
+#ifndef _COST_PARSER_H_
+#define _COST_PARSER_H_
+
+#include"simple_parser.h"
+#include"arith_decl_plugin.h"
+
+class cost_parser : public simple_parser {
+    arith_util     m_util;
+    var_ref_vector m_vars;
+public:
+    cost_parser(ast_manager & m);
+    virtual ~cost_parser() {}
+    virtual expr * parse_int(rational const & r);
+    virtual expr * parse_float(rational const & r);
+    unsigned add_var(symbol name);
+    unsigned add_var(char const * name) { return add_var(symbol(name)); }
+    void reset_vars();
+};
+
+#endif /* _COST_PARSER_H_ */
+

src/parser_util/scanner.cpp

@@ -0,0 +1,496 @@
+/*++
+Copyright (c) 2006 Microsoft Corporation
+
+Module Name:
+
+    scanner.cpp
+
+Abstract:
+
+    <abstract>
+
+Author:
+
+    Leonardo de Moura (leonardo) 2008-03-31.
+
+Revision History:
+
+--*/
+#include"scanner.h"
+
+inline char scanner::read_char() {
+    if (m_is_interactive) {
+        ++m_pos;
+        return m_stream.get();
+    }
+
+    if (m_bpos >= m_bend) {
+        m_buffer[0] = m_last_char;
+        m_stream.read(m_buffer.c_ptr()+1, m_buffer.size()-1);
+        m_bend = 1 + static_cast<unsigned>(m_stream.gcount());
+        m_bpos = 1;
+        m_last_char = m_buffer[m_bend-1];
+    }
+    ++m_pos;
+    if (m_bpos < m_bend) {        
+        return m_buffer[m_bpos++];
+    } else {
+        // increment m_bpos, so unread_char() will work properly
+        ++m_bpos;
+        return -1;
+    }    
+}
+
+inline void scanner::unread_char() {
+    --m_pos;
+    if (m_is_interactive) {
+        m_stream.unget();
+    } else {
+        // at most one character can be unread.
+        SASSERT(m_bpos > 0);
+        --m_bpos;
+    }
+}
+
+inline bool scanner::state_ok() {
+    return m_state != ERROR_TOKEN && m_state != EOF_TOKEN;
+}
+
+void scanner::comment(char delimiter) {
+    while(state_ok()) {
+        char ch = read_char();
+        if ('\n' == ch) {
+            ++m_line;
+        }
+        if (delimiter == ch || -1 == ch) {
+            return;
+        }
+    }        
+}
+
+scanner::token scanner::read_symbol(char ch) {
+    bool escape = false;
+    if (m_smt2)
+        m_string.pop_back(); // remove leading '|'
+    while (ch != '|' || escape) {
+        if (ch == EOF) {
+            // TODO: use error reporting
+            m_err << "ERROR: unexpected end of file.\n";
+            return EOF_TOKEN;
+        }
+        if (ch == '\n') {
+            ++m_line;
+        }
+        escape = (ch == '\\');
+        m_string.push_back(ch);
+        ch = read_char();                
+    }
+    if (!m_smt2)
+        m_string.push_back(ch); // don't add trailing '|'
+    m_string.push_back(0);
+    m_id = m_string.begin();
+    return ID_TOKEN;
+}
+
+
+scanner::token scanner::read_id(char first_char) {
+    char ch;
+    m_string.reset();
+    m_params.reset();
+    m_string.push_back(first_char);
+
+    bool is_arith = (m_normalized[(unsigned char) first_char] == '+');
+    bool is_alpha = (m_normalized[(unsigned char) first_char] == 'a');
+    
+    ch = read_char();        
+    // In SMT2 "-20" is an identifier.
+    if (!m_smt2 && state_ok() && first_char == '-' && m_normalized[(unsigned char) ch] == '0') {
+        return read_number(ch, false);
+    }
+
+    if (state_ok() && first_char == '|') {
+        return read_symbol(ch);
+    }
+    
+    while (state_ok()) {                        
+        switch(m_normalized[(unsigned char) ch]) {
+        case '+':
+            if (is_arith) {
+                m_string.push_back(ch);
+                break;
+            }
+            // strings can have hyphens.
+            if (!is_alpha || ch != '-') {
+                goto bail_out;  
+            }
+        case 'a':
+        case ':':
+        case '.':
+        case '0':
+            if (is_arith) {
+                goto bail_out;
+            }
+            m_string.push_back(ch);
+            break;
+        case '[':                
+            m_string.push_back(0);
+            m_id = m_string.begin();
+            if (read_params()) {
+                return ID_TOKEN;
+            }
+            else {
+                return m_state;
+            }
+        default:
+            goto bail_out;
+        }
+        ch = read_char();
+    }
+    return m_state;
+
+ bail_out:
+    m_string.push_back(0);
+    m_id = m_string.begin();
+    unread_char();
+    return ID_TOKEN;
+}
+
+bool scanner::read_params() {
+    unsigned param_num = 0;
+    
+    while (state_ok()) {
+        char ch = read_char();
+        switch (m_normalized[(unsigned char) ch]) {
+        case '0': 
+            param_num = 10*param_num + (ch - '0');
+            break;
+        case ']':
+            m_params.push_back(parameter(param_num));
+            return true;
+        case ':':               
+            m_params.push_back(parameter(param_num));
+            param_num = 0;
+            break;
+        default:
+            m_string.reset();
+            m_string.push_back(ch);
+            while (true) {
+                ch = read_char();
+                if (ch == ':' || ch == ']') {
+                    m_string.push_back(0);
+                    m_params.push_back(parameter(symbol(m_string.c_ptr())));
+                    param_num = 0;
+                    if (ch == ':') {
+                        unread_char();
+                    }
+                    else {
+                        return true;
+                    }
+                    break;
+                }
+                if (ch == EOF) {
+                    // TODO: use error reporting
+                    m_err << "ERROR: unexpected character: '" << ((int)ch) << " " << ch << "'.\n";
+                    m_state = ERROR_TOKEN;
+                    break;
+                }
+                m_string.push_back(ch);
+            }
+            break;
+        }
+    }
+    return false;
+}
+
+scanner::token scanner::read_number(char first_char, bool is_pos) {
+    unsigned divide_by = 0;
+    m_number = rational(first_char - '0');
+    m_state = INT_TOKEN;
+    
+    while (true) {
+        char ch = read_char();
+        if (m_normalized[(unsigned char) ch] == '0') {
+            m_number = rational(10)*m_number + rational(ch - '0');
+            if (m_state == FLOAT_TOKEN) {
+                ++divide_by;
+            }
+        }
+        else if (ch == '.') {
+            m_state = FLOAT_TOKEN;
+        }
+        else {
+            unread_char();
+            break;
+        }
+    }
+    if (!is_pos) {
+        m_number.neg();            
+    }
+    if (m_state == FLOAT_TOKEN) {
+        m_number /= power(rational(10), divide_by);
+    }
+    return m_state;
+}
+    
+scanner::token scanner::read_string(char delimiter, token result) {
+    m_string.reset();
+    m_params.reset();
+    while (true) {
+        char ch = read_char();
+        
+        if (!state_ok()) {
+            return m_state;
+        }
+        
+        if (ch == '\n') {
+            ++m_line;
+        }
+        
+        if (ch == delimiter || ch == EOF) {
+            m_string.push_back(0);
+            m_id = m_string.begin();
+            return result;
+        }
+        
+        if (ch == '\\') {
+            m_string.push_back('\\');
+            ch = read_char();
+        }
+        m_string.push_back(ch);
+    }
+    
+    return m_state;
+}
+
+scanner::token scanner::read_bv_literal() {
+    TRACE("scanner", tout << "read_bv_literal\n";);
+    if (m_bv_token) {
+        char ch     = read_char();
+        if (ch == 'x') {
+            ch = read_char();
+            m_number  = rational(0);
+            m_bv_size = 0;
+            while (true) {
+                if ('0' <= ch && ch <= '9') {
+                    m_number *= rational(16);
+                    m_number += rational(ch - '0');
+                }
+                else if ('a' <= ch && ch <= 'f') {
+                    m_number *= rational(16);
+                    m_number += rational(10 + (ch - 'a')); 
+                }
+                else if ('A' <= ch && ch <= 'F') {
+                    m_number *= rational(16);
+                    m_number += rational(10 + (ch - 'A'));
+                }
+                else {
+                    unread_char();
+                    m_state = m_bv_size == 0 ? ERROR_TOKEN : BV_TOKEN;
+                    TRACE("scanner", tout << m_state << ", bv-size: " << m_bv_size << ", INT_TOKEN: " << INT_TOKEN
+                          << ", BV_TOKEN: " << BV_TOKEN << "\n";);
+                    return m_state;
+                }
+                m_bv_size += 4;
+                ch = read_char();
+            }
+        }
+        else if (ch == 'b') {
+            ch = read_char();
+            m_number  = rational(0);
+            m_bv_size = 0;
+            while (ch == '0' || ch == '1') {
+                m_number *= rational(2);
+                m_number += rational(ch - '0');
+                m_bv_size++;
+                ch = read_char();
+            }
+            unread_char();
+            m_state = m_bv_size == 0 ? ERROR_TOKEN : BV_TOKEN;
+            return m_state;
+        }
+        else {
+            m_state = ERROR_TOKEN;
+            return m_state;
+        }
+    }
+    else {
+        // hack for the old parser
+        char ch     = read_char();
+        bool is_hex = false;
+        
+        m_state = ID_TOKEN;
+        m_string.reset();
+        m_params.reset();
+        
+        // convert to SMT1 format
+        m_string.push_back('b');
+        m_string.push_back('v');
+        if (ch == 'x') {
+            m_string.push_back('h');
+            m_string.push_back('e');
+            m_string.push_back('x');
+            is_hex = true;
+        } else if (ch == 'b') {
+            m_string.push_back('b');
+            m_string.push_back('i');
+            m_string.push_back('n');
+        } else {
+            // TODO: use error reporting
+            m_err << "ERROR: unexpected character after '#': '" << ((int)ch) << " " << ch << "'.\n";
+            m_state = ERROR_TOKEN;
+            return m_state;
+        }
+        
+        while (true) {
+            ch = read_char();
+            if (ch == '0' || ch == '1' ||
+                (is_hex &&
+                 (('0' <= ch && ch <= '9') ||
+                  ('a' <= ch && ch <= 'f') ||
+                  ('A' <= ch && ch <= 'F')))) {
+                m_string.push_back(ch);
+            } else {
+                unread_char();
+                break;
+            }
+        }
+        m_string.push_back(0);
+        m_id = m_string.begin();
+        
+        return m_state;
+    }
+}
+
+scanner::scanner(std::istream& stream, std::ostream& err, bool smt2, bool bv_token):
+    m_line(1),
+    m_pos(0),
+    m_id(""),
+    m_bv_size(UINT_MAX),
+    m_state(ID_TOKEN),
+    m_stream(stream),
+    m_err(err),
+    m_bpos(1 << 10),
+    m_bend(1 << 10),
+    m_last_char(0),
+    m_smt2(smt2),
+    m_bv_token(bv_token) {
+    char ch;
+
+    m_is_interactive = &stream == &std::cin;
+    m_buffer.resize(m_bpos);
+    
+    for (int i = 0; i < 256; ++i) {
+        m_normalized[i] = (char) i;
+    }
+    
+    m_normalized[static_cast<int>('\t')] = ' ';
+    m_normalized[static_cast<int>('\r')] = ' ';
+    
+    // assert ('a' < 'z');
+    for (ch = 'b'; ch <= 'z'; ++ch) {
+        m_normalized[static_cast<int>(ch)] = 'a';
+    }
+    for (ch = 'A'; ch <= 'Z'; ++ch) {
+        m_normalized[static_cast<int>(ch)] = 'a';
+    }
+    // assert ('0' < '9', '9' - '0' == 9);
+    for (ch = '1'; ch <= '9'; ++ch) {
+        m_normalized[static_cast<int>(ch)] = '0';
+    }
+
+    if (m_smt2) {
+        // SMT2 3.1, "Symbols": ~ ! @ $ % ^ & * _ - + = < > . ? /
+        m_normalized[static_cast<int>('~')] = 'a';
+        m_normalized[static_cast<int>('!')] = 'a';
+        m_normalized[static_cast<int>('@')] = 'a';
+        m_normalized[static_cast<int>('$')] = 'a';
+        m_normalized[static_cast<int>('%')] = 'a';
+        m_normalized[static_cast<int>('^')] = 'a';
+        m_normalized[static_cast<int>('&')] = 'a';
+        m_normalized[static_cast<int>('*')] = 'a';
+        m_normalized[static_cast<int>('_')] = 'a';
+        m_normalized[static_cast<int>('-')] = 'a';
+        m_normalized[static_cast<int>('+')] = 'a';
+        m_normalized[static_cast<int>('=')] = 'a';
+        m_normalized[static_cast<int>('<')] = 'a';
+        m_normalized[static_cast<int>('>')] = 'a';
+        m_normalized[static_cast<int>('.')] = 'a';
+        m_normalized[static_cast<int>('?')] = 'a';
+        m_normalized[static_cast<int>('/')] = 'a';
+
+        // SMT2 3.1, "Hexadecimals", "Binaries"
+        m_normalized[static_cast<int>('#')] = '#';
+
+        m_normalized[static_cast<int>('|')] = '+';
+    } else {
+        m_normalized[static_cast<int>('=')] = '+';
+        m_normalized[static_cast<int>('<')] = '+';
+        m_normalized[static_cast<int>('>')] = '+';
+        m_normalized[static_cast<int>('+')] = '+';
+        m_normalized[static_cast<int>('-')] = '+';
+        m_normalized[static_cast<int>('*')] = '+';
+        m_normalized[static_cast<int>('/')] = '+';
+        m_normalized[static_cast<int>('%')] = '+';
+        m_normalized[static_cast<int>('~')] = '+';
+        m_normalized[static_cast<int>('&')] = '+';
+        m_normalized[static_cast<int>('@')] = '+';
+        m_normalized[static_cast<int>('#')] = '+';
+        m_normalized[static_cast<int>('|')] = '+';
+        m_normalized[static_cast<int>('\\')] = '+';
+
+        m_normalized[static_cast<int>('.')]  = '.';
+
+        m_normalized[static_cast<int>('_')]  = 'a';
+        m_normalized[static_cast<int>('\'')] = 'a';
+        m_normalized[static_cast<int>('!')] = 'a';
+        m_normalized[static_cast<int>('?')] = 'a';
+    }
+}
+
+scanner::token scanner::scan() {
+    while (state_ok()) {
+        char ch = read_char();        
+        switch (m_normalized[(unsigned char) ch]) {
+        case ' ':
+            break;
+        case '\n':
+            m_pos = 0;
+            ++m_line;
+            break;
+        case ';':
+            comment('\n');
+            break;
+        case ':':
+            return COLON;
+        case '(':
+            return LEFT_PAREN;
+        case ')':
+            return RIGHT_PAREN;
+        case '?':
+        case '$':
+        case 'a':
+        case '+':
+        case '.':
+            return read_id(ch);
+        case '{':
+            return read_string('}',COMMENT_TOKEN);
+        case '"':
+            return read_string('"',STRING_TOKEN);
+        case '0':
+            return read_number(ch, true);
+        case '#':
+            return read_bv_literal();
+        case -1:
+            m_state = EOF_TOKEN;
+            break;
+        default:
+            // TODO: use error reporting 
+            m_err << "ERROR: unexpected character: '" << ((int)ch) << " " << ch << "'.\n";
+            m_state = ERROR_TOKEN;
+            break;
+        }
+    }
+    return m_state;
+}
+
+

src/parser_util/scanner.h

@@ -0,0 +1,92 @@
+/*++
+Copyright (c) 2006 Microsoft Corporation
+
+Module Name:
+
+    scanner.h
+
+Abstract:
+
+    <abstract>
+
+Author:
+
+    Leonardo de Moura (leonardo) 2008-03-31.
+
+Revision History:
+
+--*/
+#ifndef _SCANNER_H_
+#define _SCANNER_H_
+
+#include"ast.h"
+
+class scanner {
+public:
+
+    enum token {
+        LEFT_PAREN = 1,
+        RIGHT_PAREN,
+        COLON,
+        ID_TOKEN,        
+        STRING_TOKEN,
+        COMMENT_TOKEN,
+        INT_TOKEN,
+        BV_TOKEN,
+        FLOAT_TOKEN,
+        EOF_TOKEN,
+        ERROR_TOKEN
+    };    
+
+    scanner(std::istream& stream, std::ostream& err, bool smt2, bool bv_token=false);
+
+    ~scanner() {}    
+    
+    int get_line() const { return m_line; }
+
+    int get_pos() const { return m_pos; }
+
+    symbol const & get_id() const { return m_id; }
+
+    rational get_number() const { return m_number; }
+
+    unsigned get_bv_size() const { return m_bv_size; }
+
+    vector<parameter> const & get_params() const { return m_params; }
+    
+    token scan();
+    
+private:
+    int                m_line;
+    int                m_pos;
+    symbol             m_id;
+    rational           m_number;
+    unsigned           m_bv_size;
+    token              m_state;
+    char               m_normalized[256];
+    vector<char>       m_string;
+    std::istream&      m_stream;
+    std::ostream&      m_err;
+    vector<parameter>  m_params;
+    buffer<char>       m_buffer;
+    unsigned           m_bpos;
+    unsigned           m_bend;
+    char               m_last_char;
+    bool               m_is_interactive;
+    bool               m_smt2;
+    bool               m_bv_token;
+
+    char read_char();
+    token read_symbol(char ch);
+    void unread_char();
+    void comment(char delimiter);
+    token read_id(char first_char);
+    bool read_params();
+    token read_number(char first_char, bool is_pos);
+    token read_string(char delimiter, token result);
+    token read_bv_literal();
+    bool state_ok();
+};
+
+#endif /* _SCANNER_H_ */
+

src/parser_util/simple_parser.cpp

@@ -0,0 +1,149 @@
+/*++
+Copyright (c) 2006 Microsoft Corporation
+
+Module Name:
+
+    simple_parser.cpp
+
+Abstract:
+
+    <abstract>
+
+Author:
+
+    Leonardo de Moura (leonardo) 2008-03-31.
+
+Revision History:
+
+--*/
+#include<fstream>
+#include<sstream>
+#include"simple_parser.h"
+#include"warning.h"
+#include"scanner.h"
+
+simple_parser::simple_parser(ast_manager & m):
+    m_manager(m),
+    m_exprs(m) {
+}
+
+simple_parser::~simple_parser() {
+}
+
+void simple_parser::add_builtin_op(symbol const & s, family_id fid, decl_kind kind) {
+    SASSERT(!m_builtin.contains(s));
+    SASSERT(!m_vars.contains(s));
+    m_builtin.insert(s, builtin_op(fid, kind));
+}
+
+void simple_parser::add_builtin_op(char const * str, family_id fid, decl_kind kind) {
+    add_builtin_op(symbol(str), fid, kind);
+}
+
+void simple_parser::add_var(symbol const & s, var * v) {
+    SASSERT(!m_builtin.contains(s));
+    SASSERT(!m_vars.contains(s));
+    m_vars.insert(s, v);
+}
+
+void simple_parser::add_var(char const * str, var * v) {
+    add_var(symbol(str), v);
+}
+
+void simple_parser::reset() {
+    m_builtin.reset();
+    m_vars.reset();
+    m_exprs.reset();
+}
+
+void simple_parser::reset_vars() {
+    m_vars.reset();
+}
+
+expr * simple_parser::parse_expr(scanner & s) {
+    builtin_op op; 
+    var * v;
+    expr * r;
+    scanner::token token;
+    token = s.scan();
+    switch (token) {
+    case scanner::LEFT_PAREN:
+        token = s.scan();
+        if (token != scanner::ID_TOKEN)
+            throw parser_error();
+        if (m_builtin.find(s.get_id(), op)) {
+            ptr_vector<expr> args;
+            while (true) {
+                expr * arg = parse_expr(s);
+                if (arg) {
+                    args.push_back(arg);
+                }
+                else {
+                    expr * r = m_manager.mk_app(op.m_family_id, op.m_kind, args.size(), args.c_ptr());
+                    m_exprs.push_back(r);
+                    return r;
+                }
+            }
+        }
+        throw parser_error();
+    case scanner::RIGHT_PAREN:
+        return 0;
+    case scanner::ID_TOKEN:
+        if (m_builtin.find(s.get_id(), op)) {
+            expr * r = m_manager.mk_const(op.m_family_id, op.m_kind);
+            m_exprs.push_back(r);
+            return r;
+        }
+        else if (m_vars.find(s.get_id(), v)) {
+            return v;
+        }
+        throw parser_error();
+    case scanner::INT_TOKEN:
+        r = parse_int(s.get_number());
+        m_exprs.push_back(r);
+        return r;
+    case scanner::FLOAT_TOKEN:
+        r = parse_float(s.get_number());
+        m_exprs.push_back(r);
+        return r;
+    default:
+        throw parser_error();
+    }
+}
+
+bool simple_parser::parse(std::istream & in, expr_ref & result) {
+	scanner s(in, std::cerr, false);
+    try {
+        result = parse_expr(s);
+        if (!result)
+            throw parser_error();
+    }
+    catch (parser_error) {
+        warning_msg("parser error");
+        return false;
+    } 
+    m_exprs.reset();
+    return result.get() != 0;
+}
+
+bool simple_parser::parse_string(char const * str, expr_ref & result) {
+    std::string s = str;
+    std::istringstream is(s);
+    return parse(is, result);
+}
+ 
+bool simple_parser::parse_file(char const * file, expr_ref & result) {
+    if (file != 0) {
+        std::ifstream stream(file);
+        if (!stream) {
+            warning_msg("ERROR: could not open file '%s'.", file);
+            return false;
+        }
+        return parse(stream, result);
+    }
+    else {
+        return parse(std::cin, result);
+    }
+}
+
+

src/parser_util/simple_parser.h

@@ -0,0 +1,64 @@
+/*++
+Copyright (c) 2006 Microsoft Corporation
+
+Module Name:
+
+    simple_parser.h
+
+Abstract:
+
+    Simple sexpr parser
+
+Author:
+
+    Leonardo de Moura (leonardo) 2008-03-31.
+
+Revision History:
+
+--*/
+#ifndef _SIMPLE_PARSER_H_
+#define _SIMPLE_PARSER_H_
+
+#include"ast.h"
+#include"map.h"
+
+class scanner;
+
+/**
+   \brief Simple sexpr parser.
+   This class is used to parse small expressions used for configuring Z3.
+*/
+class simple_parser {
+protected:
+    struct parser_error {};
+    struct builtin_op {
+        family_id m_family_id;
+        decl_kind m_kind;
+        builtin_op() : m_family_id(null_family_id), m_kind(0) {}
+        builtin_op(family_id fid, decl_kind k) : m_family_id(fid), m_kind(k) {}
+    };
+    typedef map<symbol, builtin_op, symbol_hash_proc, symbol_eq_proc> op_map;
+    typedef map<symbol, var *, symbol_hash_proc, symbol_eq_proc>   var_map;
+    ast_manager &    m_manager;
+    op_map           m_builtin;
+    var_map          m_vars;
+    expr_ref_vector  m_exprs;
+    expr * parse_expr(scanner & s);
+public:
+    simple_parser(ast_manager & m);
+    virtual ~simple_parser();
+    void add_builtin_op(symbol const & s, family_id fid, decl_kind kind);
+    void add_builtin_op(char const * str, family_id fid, decl_kind kind);
+    void add_var(symbol const & s, var * v);
+    void add_var(char const * str, var * v);
+    void reset();
+    void reset_vars();
+    bool parse(std::istream & in, expr_ref & result);
+    bool parse_string(char const * str, expr_ref & result);
+    bool parse_file(char const * file, expr_ref & result);
+    virtual expr * parse_int(rational const & r) { throw parser_error(); }
+    virtual expr * parse_float(rational const & r) { throw parser_error(); }
+};
+
+#endif /* _SIMPLE_PARSER_H_ */
+