Merge branch 'master' of https://github.com/z3prover/z3

scripts/mk_util.py

@@ -2393,7 +2393,50 @@ class DotNetExampleComponent(ExampleComponent):
             out.write('\n')
             out.write('_ex_%s: %s\n\n' % (self.name, exefile))
         if is_dotnet_core_enabled():
-            print("TBD: build script for dotnet_example on core")
+            proj_name = 'dotnet_example.csproj'
+            out.write('_ex_%s:' % self.name)
+            for csfile in get_cs_files(self.ex_dir):
+                out.write(' ')
+                out.write(os.path.join(self.to_ex_dir, csfile))
+
+            def mk_echo(msg, first = False):
+                echo_ex_qu = '' if IS_WINDOWS else '"'
+                echo_in_qu = '"' if IS_WINDOWS else '\\"'
+                echo_esc = '^' if IS_WINDOWS else ''
+                echo_dir = '>' if first else '>>'
+
+                msg = msg.replace('"', echo_in_qu).replace('<', echo_esc + '<').replace('>', echo_esc + '>')
+                out.write('\t@echo %s%s%s %s %s\n' % (echo_ex_qu, msg, echo_ex_qu, echo_dir, proj_name))
+
+            out.write('\n')
+            mk_echo('<Project Sdk="Microsoft.NET.Sdk">', True)
+            mk_echo('  <PropertyGroup>')
+            mk_echo('    <OutputType>Exe</OutputType>')
+            mk_echo('    <TargetFramework>netcoreapp2.0</TargetFramework>')
+            if VS_X64:
+                platform = 'x64'
+            elif VS_ARM:
+                platform = 'ARM'
+            else:
+                platform = 'x86'
+            mk_echo('    <PlatformTarget>%s</PlatformTarget>' % platform)
+            mk_echo('  </PropertyGroup>')
+            mk_echo('  <ItemGroup>')
+            mk_echo('    <Compile Include="%s/*.cs" />' % self.to_ex_dir)
+            mk_echo('    <Reference Include="Microsoft.Z3">')
+            mk_echo('      <HintPath>Microsoft.Z3.dll</HintPath>')
+            mk_echo('    </Reference>')
+            mk_echo('  </ItemGroup>')
+            mk_echo('</Project>')
+
+            dotnetCmdLine = [DOTNET, "build", proj_name]
+            dotnetCmdLine.extend(['-c'])
+            if DEBUG_MODE:
+                dotnetCmdLine.extend(['Debug'])
+            else:
+                dotnetCmdLine.extend(['Release'])
+            MakeRuleCmd.write_cmd(out, ' '.join(dotnetCmdLine))
+            out.write('\n')
 
 class JavaExampleComponent(ExampleComponent):
     def __init__(self, name, path):

src/api/api_solver.cpp

@@ -183,8 +183,12 @@ extern "C" {
         }
         else if (ext && std::string("dimacs") == ext) {
             ast_manager& m = to_solver_ref(s)->get_manager();
+            std::stringstream err;
             sat::solver solver(to_solver_ref(s)->get_params(), m.limit());
-            parse_dimacs(is, solver);
+            if (!parse_dimacs(is, err, solver)) {
+                SET_ERROR_CODE(Z3_PARSER_ERROR, err.str().c_str());
+                return;
+            }
             sat2goal s2g;
             ref<sat2goal::mc> mc;
             atom2bool_var a2b(m);

src/ast/rewriter/seq_rewriter.cpp

@@ -561,6 +561,7 @@ br_status seq_rewriter::mk_seq_extract(expr* a, expr* b, expr* c, expr_ref& resu
     zstring s;
     rational pos, len;
 
+    TRACE("seq", tout << mk_pp(a, m()) << " " << mk_pp(b, m()) << " " << mk_pp(c, m()) << "\n";);
     bool constantBase = m_util.str.is_string(a, s);
     bool constantPos = m_autil.is_numeral(b, pos);
     bool constantLen = m_autil.is_numeral(c, len);
@@ -599,6 +600,10 @@ br_status seq_rewriter::mk_seq_extract(expr* a, expr* b, expr* c, expr_ref& resu
         SASSERT(_len > 0);
         expr_ref_vector as(m()), bs(m());
         m_util.str.get_concat(a, as);
+        if (as.empty()) {
+            result = a;
+            return BR_DONE;
+        }
         for (unsigned i = 0; i < as.size() && _len > 0; ++i) {
             if (m_util.str.is_unit(as[i].get())) {
                 if (_pos == 0) {
@@ -613,7 +618,12 @@ br_status seq_rewriter::mk_seq_extract(expr* a, expr* b, expr* c, expr_ref& resu
                 return BR_FAILED;
             }
         }
-        result = m_util.str.mk_concat(bs);
+        if (bs.empty()) {
+            result = m_util.str.mk_empty(m().get_sort(a));
+        }
+        else {
+            result = m_util.str.mk_concat(bs);
+        }
         return BR_DONE;
     }
 

src/parsers/smt2/smt2parser.cpp

@@ -346,7 +346,8 @@ namespace smt2 {
         // consume garbage
         // return true if managed to recover from the error...
         bool sync_after_error() {
-            while (true) {
+            unsigned num_errors = 0;
+            while (num_errors < 100) {
                 try {
                     while (curr_is_rparen())
                         next();
@@ -374,8 +375,10 @@ namespace smt2 {
                 catch (scanner_exception & ex) {
                     SASSERT(ex.has_pos());
                     error(ex.line(), ex.pos(), ex.msg());
+                    ++num_errors;
                 }
             }
+            return false;
         }
 
         void check_next(scanner::token t, char const * msg) {
@@ -3117,7 +3120,7 @@ namespace smt2 {
 
         bool operator()() {
             m_num_bindings    = 0;
-            bool found_errors = false;
+            unsigned found_errors = 0;
 
             try {
                 scan_core();
@@ -3126,7 +3129,7 @@ namespace smt2 {
                 error(ex.msg());
                 if (!sync_after_error())
                     return false;
-                found_errors = true;
+                found_errors++;
             }
 
             while (true) {
@@ -3138,7 +3141,7 @@ namespace smt2 {
                             parse_cmd();
                             break;
                         case scanner::EOF_TOKEN:
-                            return !found_errors;
+                            return found_errors == 0;
                         default:
                             throw parser_exception("invalid command, '(' expected");
                             break;

src/sat/dimacs.cpp

@@ -21,6 +21,8 @@ Revision History:
 #undef min
 #include "sat/sat_solver.h"
 
+struct lex_error {};
+
 class stream_buffer {
     std::istream & m_stream;
     int            m_val;
@@ -67,7 +69,7 @@ void skip_line(Buffer & in) {
 }
 
 template<typename Buffer>
-int parse_int(Buffer & in) {
+int parse_int(Buffer & in, std::ostream& err) {
     int     val = 0;
     bool    neg = false;
     skip_whitespace(in);
@@ -81,9 +83,8 @@ int parse_int(Buffer & in) {
     }
 
     if (*in < '0' || *in > '9') {
-        std::cerr << "(error, \"unexpected char: " << *in << " line: " << in.line() << "\")\n";
+        err << "(error, \"unexpected char: " << *in << " line: " << in.line() << "\")\n";
-        exit(3);
+        throw lex_error();
-        exit(ERR_PARSER);
     }
 
     while (*in >= '0' && *in <= '9') {
@@ -95,14 +96,14 @@ int parse_int(Buffer & in) {
 }
 
 template<typename Buffer>
-void read_clause(Buffer & in, sat::solver & solver, sat::literal_vector & lits) {
+void read_clause(Buffer & in, std::ostream& err, sat::solver & solver, sat::literal_vector & lits) {
     int     parsed_lit;
     int     var;
     
     lits.reset();
 
     while (true) { 
-        parsed_lit = parse_int(in);
+        parsed_lit = parse_int(in, err);
         if (parsed_lit == 0)
             break;
         var = abs(parsed_lit);
@@ -114,24 +115,30 @@ void read_clause(Buffer & in, sat::solver & solver, sat::literal_vector & lits)
 }
 
 template<typename Buffer>
-void parse_dimacs_core(Buffer & in, sat::solver & solver) {
+bool parse_dimacs_core(Buffer & in, std::ostream& err, sat::solver & solver) {
     sat::literal_vector lits;
-    while (true) {
+    try {
-        skip_whitespace(in);
+        while (true) {
-        if (*in == EOF) {
+            skip_whitespace(in);
-            break;
+            if (*in == EOF) {
-        }
+                break;
-        else if (*in == 'c' || *in == 'p') {
+            }
-            skip_line(in);
+            else if (*in == 'c' || *in == 'p') {
-        }
+                skip_line(in);
-        else {
+            }
-            read_clause(in, solver, lits);
+            else {
-            solver.mk_clause(lits.size(), lits.c_ptr());
+                read_clause(in, err, solver, lits);
+                solver.mk_clause(lits.size(), lits.c_ptr());
+            }
         }
     }
+    catch (lex_error) {
+        return false;
+    }
+    return true;
 }
 
-void parse_dimacs(std::istream & in, sat::solver & solver) {
+bool parse_dimacs(std::istream & in, std::ostream& err, sat::solver & solver) {
     stream_buffer _in(in);
-    parse_dimacs_core(_in, solver);
+    return parse_dimacs_core(_in, err, solver);
 }

src/sat/dimacs.h

@@ -21,7 +21,7 @@ Revision History:
 
 #include "sat/sat_types.h"
 
-void parse_dimacs(std::istream & s, sat::solver & solver);
+bool parse_dimacs(std::istream & s, std::ostream& err, sat::solver & solver);
 
 #endif /* DIMACS_PARSER_H_ */
 

src/shell/dimacs_frontend.cpp

@@ -136,7 +136,7 @@ void verify_solution(char const * file_name) {
         std::cerr << "(error \"failed to open file '" << file_name << "'\")" << std::endl;
         exit(ERR_OPEN_FILE);
     }
-    parse_dimacs(in, solver);
+    parse_dimacs(in, std::cerr, solver);
     
     sat::model const & m = g_solver->get_model();
     for (unsigned i = 1; i < m.size(); i++) {
@@ -178,10 +178,10 @@ unsigned read_dimacs(char const * file_name) {
             std::cerr << "(error \"failed to open file '" << file_name << "'\")" << std::endl;
             exit(ERR_OPEN_FILE);
         }
-        parse_dimacs(in, solver);
+        parse_dimacs(in, std::cerr, solver);
     }
     else {
-        parse_dimacs(std::cin, solver);
+        parse_dimacs(std::cin, std::cerr, solver);
     }
     IF_VERBOSE(20, solver.display_status(verbose_stream()););