diff --git a/CMakeLists.txt b/CMakeLists.txt index 715679957..871852c04 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -33,8 +33,8 @@ endif() # Project version ################################################################################ set(Z3_VERSION_MAJOR 4) -set(Z3_VERSION_MINOR 5) -set(Z3_VERSION_PATCH 1) +set(Z3_VERSION_MINOR 6) +set(Z3_VERSION_PATCH 0) set(Z3_VERSION_TWEAK 0) set(Z3_VERSION "${Z3_VERSION_MAJOR}.${Z3_VERSION_MINOR}.${Z3_VERSION_PATCH}.${Z3_VERSION_TWEAK}") set(Z3_FULL_VERSION_STR "${Z3_VERSION}") # Note this might be modified diff --git a/examples/c++/example.cpp b/examples/c++/example.cpp index 035d032bc..df977268a 100644 --- a/examples/c++/example.cpp +++ b/examples/c++/example.cpp @@ -1138,8 +1138,11 @@ static void parse_example() { decls.push_back(c.function("a", 0, 0, B)); expr a = c.parse_string("(assert a)", sorts, decls); std::cout << a << "\n"; + + // expr b = c.parse_string("(benchmark tst :extrafuns ((x Int) (y Int)) :formula (> x y) :formula (> x 0))"); } + int main() { try { diff --git a/examples/c/test_capi.c b/examples/c/test_capi.c index f6d515389..d71771f98 100644 --- a/examples/c/test_capi.c +++ b/examples/c/test_capi.c @@ -395,11 +395,10 @@ void assert_comm_axiom(Z3_context ctx, Z3_solver s, Z3_func_decl f) t_name = Z3_mk_string_symbol(ctx, "T"); - Z3_parse_smtlib_string(ctx, - "(benchmark comm :formula (forall (x T) (y T) (= (f x y) (f y x))))", + q = Z3_parse_smtlib2_string(ctx, + "(assert (forall ((x T) (y T)) (= (f x y) (f y x))))", 1, &t_name, &t, 1, &f_name, &f); - q = Z3_get_smtlib_formula(ctx, 0); printf("assert axiom:\n%s\n", Z3_ast_to_string(ctx, q)); Z3_solver_assert(ctx, s, q); } @@ -1632,35 +1631,6 @@ void error_code_example2() { } } -/** - \brief Demonstrates how to use the SMTLIB parser. - */ -void parser_example1() -{ - Z3_context ctx = mk_context(); - Z3_solver s = mk_solver(ctx); - unsigned i, num_formulas; - - printf("\nparser_example1\n"); - LOG_MSG("parser_example1"); - - - Z3_parse_smtlib_string(ctx, - "(benchmark tst :extrafuns ((x Int) (y Int)) :formula (> x y) :formula (> x 0))", - 0, 0, 0, - 0, 0, 0); - num_formulas = Z3_get_smtlib_num_formulas(ctx); - for (i = 0; i < num_formulas; i++) { - Z3_ast f = Z3_get_smtlib_formula(ctx, i); - printf("formula %d: %s\n", i, Z3_ast_to_string(ctx, f)); - Z3_solver_assert(ctx, s, f); - } - - check(ctx, s, Z3_L_TRUE); - - del_solver(ctx, s); - Z3_del_context(ctx); -} /** \brief Demonstrates how to initialize the parser symbol table. @@ -1690,12 +1660,11 @@ void parser_example2() names[0] = Z3_mk_string_symbol(ctx, "a"); names[1] = Z3_mk_string_symbol(ctx, "b"); - Z3_parse_smtlib_string(ctx, - "(benchmark tst :formula (> a b))", + f = Z3_parse_smtlib2_string(ctx, + "(assert (> a b))", 0, 0, 0, /* 'x' and 'y' declarations are inserted as 'a' and 'b' into the parser symbol table. */ 2, names, decls); - f = Z3_get_smtlib_formula(ctx, 0); printf("formula: %s\n", Z3_ast_to_string(ctx, f)); Z3_solver_assert(ctx, s, f); check(ctx, s, Z3_L_TRUE); @@ -1737,11 +1706,10 @@ void parser_example3() assert_comm_axiom(ctx, s, g); - Z3_parse_smtlib_string(ctx, - "(benchmark tst :formula (forall (x Int) (y Int) (implies (= x y) (= (g x 0) (g 0 y)))))", + thm = Z3_parse_smtlib2_string(ctx, + "(assert (forall ((x Int) (y Int)) (=> (= x y) (= (g x 0) (g 0 y)))))", 0, 0, 0, 1, &g_name, &g); - thm = Z3_get_smtlib_formula(ctx, 0); printf("formula: %s\n", Z3_ast_to_string(ctx, thm)); prove(ctx, s, thm, Z3_TRUE); @@ -1749,41 +1717,6 @@ void parser_example3() Z3_del_context(ctx); } -/** - \brief Display the declarations, assumptions and formulas in a SMT-LIB string. -*/ -void parser_example4() -{ - Z3_context ctx; - unsigned i, num_decls, num_assumptions, num_formulas; - - printf("\nparser_example4\n"); - LOG_MSG("parser_example4"); - - ctx = mk_context(); - - Z3_parse_smtlib_string(ctx, - "(benchmark tst :extrafuns ((x Int) (y Int)) :assumption (= x 20) :formula (> x y) :formula (> x 0))", - 0, 0, 0, - 0, 0, 0); - num_decls = Z3_get_smtlib_num_decls(ctx); - for (i = 0; i < num_decls; i++) { - Z3_func_decl d = Z3_get_smtlib_decl(ctx, i); - printf("declaration %d: %s\n", i, Z3_func_decl_to_string(ctx, d)); - } - num_assumptions = Z3_get_smtlib_num_assumptions(ctx); - for (i = 0; i < num_assumptions; i++) { - Z3_ast a = Z3_get_smtlib_assumption(ctx, i); - printf("assumption %d: %s\n", i, Z3_ast_to_string(ctx, a)); - } - num_formulas = Z3_get_smtlib_num_formulas(ctx); - for (i = 0; i < num_formulas; i++) { - Z3_ast f = Z3_get_smtlib_formula(ctx, i); - printf("formula %d: %s\n", i, Z3_ast_to_string(ctx, f)); - } - Z3_del_context(ctx); -} - /** \brief Demonstrates how to handle parser errors using Z3 error handling support. */ @@ -1802,9 +1735,9 @@ void parser_example5() { s = mk_solver(ctx); Z3_del_config(cfg); - Z3_parse_smtlib_string(ctx, + Z3_parse_smtlib2_string(ctx, /* the following string has a parsing error: missing parenthesis */ - "(benchmark tst :extrafuns ((x Int (y Int)) :formula (> x y) :formula (> x 0))", + "(declare-const x Int) declare-const y Int) (assert (and (> x y) (> x 0)))", 0, 0, 0, 0, 0, 0); e = Z3_get_error_code(ctx); @@ -1817,7 +1750,7 @@ void parser_example5() { err: printf("Z3 error: %s.\n", Z3_get_error_msg(ctx, e)); if (ctx != NULL) { - printf("Error message: '%s'.\n",Z3_get_smtlib_error(ctx)); + printf("Error message: '%s'.\n",Z3_get_parser_error(ctx)); del_solver(ctx, s); Z3_del_context(ctx); } @@ -3065,10 +2998,8 @@ int main() { two_contexts_example1(); error_code_example1(); error_code_example2(); - parser_example1(); parser_example2(); parser_example3(); - parser_example4(); parser_example5(); numeral_example(); ite_example(); diff --git a/examples/dotnet/Program.cs b/examples/dotnet/Program.cs index 64149a553..af3c59099 100644 --- a/examples/dotnet/Program.cs +++ b/examples/dotnet/Program.cs @@ -173,10 +173,9 @@ namespace test_mapi throw new Exception("function must be binary, and argument types must be equal to return type"); } - string bench = string.Format("(benchmark comm :formula (forall (x {0}) (y {1}) (= ({2} x y) ({3} y x))))", + string bench = string.Format("(assert (forall ((x {0}) (y {1})) (= ({2} x y) ({3} y x))))", t.Name, t.Name, f.Name, f.Name); - ctx.ParseSMTLIBString(bench, new Symbol[] { t.Name }, new Sort[] { t }, new Symbol[] { f.Name }, new FuncDecl[] { f }); - return ctx.SMTLIBFormulas[0]; + return ctx.ParseSMTLIB2String(bench, new Symbol[] { t.Name }, new Sort[] { t }, new Symbol[] { f.Name }, new FuncDecl[] { f }); } /// @@ -965,21 +964,6 @@ namespace test_mapi } } - /// - /// Shows how to read an SMT1 file. - /// - static void SMT1FileTest(string filename) - { - Console.Write("SMT File test "); - - using (Context ctx = new Context(new Dictionary() { { "MODEL", "true" } })) - { - ctx.ParseSMTLIBFile(filename); - - BoolExpr a = ctx.MkAnd(ctx.SMTLIBFormulas); - Console.WriteLine("read formula: " + a); - } - } /// /// Shows how to read an SMT2 file. @@ -1399,11 +1383,10 @@ namespace test_mapi { Console.WriteLine("ParserExample1"); - ctx.ParseSMTLIBString("(benchmark tst :extrafuns ((x Int) (y Int)) :formula (> x y) :formula (> x 0))"); - foreach (BoolExpr f in ctx.SMTLIBFormulas) - Console.WriteLine("formula {0}", f); + var fml = ctx.ParseSMTLIB2String("(declare-const x Int) (declare-const y Int) (assert (> x y)) (assert (> x 0))"); + Console.WriteLine("formula {0}", fml); - Model m = Check(ctx, ctx.MkAnd(ctx.SMTLIBFormulas), Status.SATISFIABLE); + Model m = Check(ctx, fml, Status.SATISFIABLE); } /// @@ -1412,15 +1395,11 @@ namespace test_mapi public static void ParserExample2(Context ctx) { Console.WriteLine("ParserExample2"); - Symbol[] declNames = { ctx.MkSymbol("a"), ctx.MkSymbol("b") }; FuncDecl a = ctx.MkConstDecl(declNames[0], ctx.MkIntSort()); FuncDecl b = ctx.MkConstDecl(declNames[1], ctx.MkIntSort()); FuncDecl[] decls = new FuncDecl[] { a, b }; - - ctx.ParseSMTLIBString("(benchmark tst :formula (> a b))", - null, null, declNames, decls); - BoolExpr f = ctx.SMTLIBFormulas[0]; + BoolExpr f = ctx.ParseSMTLIB2String("(assert (> a b))", null, null, declNames, decls); Console.WriteLine("formula: {0}", f); Check(ctx, f, Status.SATISFIABLE); } @@ -1438,39 +1417,15 @@ namespace test_mapi BoolExpr ca = CommAxiom(ctx, g); - ctx.ParseSMTLIBString("(benchmark tst :formula (forall (x Int) (y Int) (implies (= x y) (= (gg x 0) (gg 0 y)))))", + BoolExpr thm = ctx.ParseSMTLIB2String("(assert (forall ((x Int) (y Int)) (=> (= x y) (= (gg x 0) (gg 0 y)))))", null, null, new Symbol[] { ctx.MkSymbol("gg") }, new FuncDecl[] { g }); - BoolExpr thm = ctx.SMTLIBFormulas[0]; Console.WriteLine("formula: {0}", thm); Prove(ctx, thm, false, ca); } - /// - /// Display the declarations, assumptions and formulas in a SMT-LIB string. - /// - public static void ParserExample4(Context ctx) - { - Console.WriteLine("ParserExample4"); - - ctx.ParseSMTLIBString - ("(benchmark tst :extrafuns ((x Int) (y Int)) :assumption (= x 20) :formula (> x y) :formula (> x 0))"); - foreach (var decl in ctx.SMTLIBDecls) - { - Console.WriteLine("Declaration: {0}", decl); - } - foreach (var f in ctx.SMTLIBAssumptions) - { - Console.WriteLine("Assumption: {0}", f); - } - foreach (var f in ctx.SMTLIBFormulas) - { - Console.WriteLine("Formula: {0}", f); - } - } - /// /// Demonstrates how to handle parser errors using Z3 error handling support. /// @@ -1481,9 +1436,9 @@ namespace test_mapi try { - ctx.ParseSMTLIBString( + ctx.ParseSMTLIB2String( /* the following string has a parsing error: missing parenthesis */ - "(benchmark tst :extrafuns ((x Int (y Int)) :formula (> x y) :formula (> x 0))"); + "(declare-const x Int (declare-const y Int)) (assert (> x y))"); } catch (Z3Exception e) { @@ -2213,7 +2168,6 @@ namespace test_mapi BitvectorExample2(ctx); ParserExample1(ctx); ParserExample2(ctx); - ParserExample4(ctx); ParserExample5(ctx); ITEExample(ctx); EvalExample1(ctx); diff --git a/examples/java/JavaExample.java b/examples/java/JavaExample.java index 25076e27c..40fb25a92 100644 --- a/examples/java/JavaExample.java +++ b/examples/java/JavaExample.java @@ -170,10 +170,9 @@ class JavaExample String bench = "(benchmark comm :formula (forall (x " + t.getName() + ") (y " + t.getName() + ") (= (" + f.getName() + " x y) (" + f.getName() + " y x))))"; - ctx.parseSMTLIBString(bench, new Symbol[] { t.getName() }, + return ctx.parseSMTLIB2String(bench, new Symbol[] { t.getName() }, new Sort[] { t }, new Symbol[] { f.getName() }, new FuncDecl[] { f }); - return ctx.getSMTLIBFormulas()[0]; } // / "Hello world" example: create a Z3 logical context, and delete it. @@ -1028,21 +1027,6 @@ class JavaExample } } - // / Shows how to read an SMT1 file. - - void smt1FileTest(String filename) - { - System.out.print("SMT File test "); - - { - HashMap cfg = new HashMap(); - Context ctx = new Context(cfg); - ctx.parseSMTLIBFile(filename, null, null, null, null); - - BoolExpr a = ctx.mkAnd(ctx.getSMTLIBFormulas()); - System.out.println("read formula: " + a); - } - } // / Shows how to read an SMT2 file. @@ -1459,15 +1443,13 @@ class JavaExample System.out.println("ParserExample1"); Log.append("ParserExample1"); - ctx.parseSMTLIBString( - "(benchmark tst :extrafuns ((x Int) (y Int)) :formula (> x y) :formula (> x 0))", + BoolExpr f = ctx.parseSMTLIB2String( + "(declare-const x Int) (declare-const y Int) (assert (and (> x y) (> x 0)))", null, null, null, null); - for (BoolExpr f : ctx.getSMTLIBFormulas()) - System.out.println("formula " + f); + System.out.println("formula " + f); @SuppressWarnings("unused") - Model m = check(ctx, ctx.mkAnd(ctx.getSMTLIBFormulas()), - Status.SATISFIABLE); + Model m = check(ctx, f, Status.SATISFIABLE); } // / Demonstrates how to initialize the parser symbol table. @@ -1482,9 +1464,8 @@ class JavaExample FuncDecl b = ctx.mkConstDecl(declNames[1], ctx.mkIntSort()); FuncDecl[] decls = new FuncDecl[] { a, b }; - ctx.parseSMTLIBString("(benchmark tst :formula (> a b))", null, null, + BoolExpr f = ctx.parseSMTLIB2String("(assert (> a b))", null, null, declNames, decls); - BoolExpr f = ctx.getSMTLIBFormulas()[0]; System.out.println("formula: " + f); check(ctx, f, Status.SATISFIABLE); } @@ -1502,39 +1483,14 @@ class JavaExample BoolExpr ca = commAxiom(ctx, g); - ctx.parseSMTLIBString( - "(benchmark tst :formula (forall (x Int) (y Int) (implies (= x y) (= (gg x 0) (gg 0 y)))))", + BoolExpr thm = ctx.parseSMTLIB2String( + "(assert (forall ((x Int) (y Int)) (=> (= x y) (= (gg x 0) (gg 0 y)))))", null, null, new Symbol[] { ctx.mkSymbol("gg") }, new FuncDecl[] { g }); - - BoolExpr thm = ctx.getSMTLIBFormulas()[0]; System.out.println("formula: " + thm); prove(ctx, thm, false, ca); } - // / Display the declarations, assumptions and formulas in a SMT-LIB string. - - public void parserExample4(Context ctx) - { - System.out.println("ParserExample4"); - Log.append("ParserExample4"); - - ctx.parseSMTLIBString( - "(benchmark tst :extrafuns ((x Int) (y Int)) :assumption (= x 20) :formula (> x y) :formula (> x 0))", - null, null, null, null); - for (FuncDecl decl : ctx.getSMTLIBDecls()) - { - System.out.println("Declaration: " + decl); - } - for (BoolExpr f : ctx.getSMTLIBAssumptions()) - { - System.out.println("Assumption: " + f); - } - for (BoolExpr f : ctx.getSMTLIBFormulas()) - { - System.out.println("Formula: " + f); - } - } // / Demonstrates how to handle parser errors using Z3 error handling // support. @@ -1546,12 +1502,12 @@ class JavaExample try { - ctx.parseSMTLIBString( + ctx.parseSMTLIB2String( /* * the following string has a parsing error: missing * parenthesis */ - "(benchmark tst :extrafuns ((x Int (y Int)) :formula (> x y) :formula (> x 0))", + "(declare-const x Int (declare-const y Int)) (assert (> x y))", null, null, null, null); } catch (Z3Exception e) { @@ -2341,7 +2297,6 @@ class JavaExample p.bitvectorExample2(ctx); p.parserExample1(ctx); p.parserExample2(ctx); - p.parserExample4(ctx); p.parserExample5(ctx); p.iteExample(ctx); p.evalExample1(ctx); diff --git a/examples/maxsat/ex.smt b/examples/maxsat/ex.smt index 14ac0db89..d28b27c80 100644 --- a/examples/maxsat/ex.smt +++ b/examples/maxsat/ex.smt @@ -1,11 +1,11 @@ -(benchmark ex - :logic AUFLIA - :extrafuns ((x Int) (y Int) (z Int)) - :assumption (> x 0) - :assumption (<= x -1) - :assumption (or (> x 0) (< y 1)) - :assumption (> y 2) - :assumption (> y 3) - :assumption (<= y -1) - :formula (= z (+ x y))) +(declare-const x Int) +(declare-const y Int) +(declare-const z Int) +(assert-soft (> x 0)) +(assert-soft (<= x -1)) +(assert-soft (or (> x 0) (< y 1))) +(assert-soft (> y 2)) +(assert-soft (> y 3)) +(assert-soft (<= y -1)) +(assert (= z (+ x y))) \ No newline at end of file diff --git a/examples/maxsat/maxsat.c b/examples/maxsat/maxsat.c index a312e79ad..5696f5b89 100644 --- a/examples/maxsat/maxsat.c +++ b/examples/maxsat/maxsat.c @@ -116,41 +116,6 @@ Z3_ast mk_binary_and(Z3_context ctx, Z3_ast in_1, Z3_ast in_2) } -/** - \brief Get hard constraints from a SMT-LIB file. We assume hard constraints - are formulas preceeded with the keyword :formula. - Return an array containing all formulas read by the last Z3_parse_smtlib_file invocation. - It will store the number of formulas in num_cnstrs. -*/ -Z3_ast * get_hard_constraints(Z3_context ctx, unsigned * num_cnstrs) -{ - Z3_ast * result; - unsigned i; - *num_cnstrs = Z3_get_smtlib_num_formulas(ctx); - result = (Z3_ast *) malloc(sizeof(Z3_ast) * (*num_cnstrs)); - for (i = 0; i < *num_cnstrs; i++) { - result[i] = Z3_get_smtlib_formula(ctx, i); - } - return result; -} - -/** - \brief Get soft constraints from a SMT-LIB file. We assume soft constraints - are formulas preceeded with the keyword :assumption. - Return an array containing all assumptions read by the last Z3_parse_smtlib_file invocation. - It will store the number of formulas in num_cnstrs. -*/ -Z3_ast * get_soft_constraints(Z3_context ctx, unsigned * num_cnstrs) -{ - Z3_ast * result; - unsigned i; - *num_cnstrs = Z3_get_smtlib_num_assumptions(ctx); - result = (Z3_ast *) malloc(sizeof(Z3_ast) * (*num_cnstrs)); - for (i = 0; i < *num_cnstrs; i++) { - result[i] = Z3_get_smtlib_assumption(ctx, i); - } - return result; -} /** \brief Free the given array of cnstrs that was allocated using get_hard_constraints or get_soft_constraints. @@ -610,14 +575,37 @@ int smtlib_maxsat(char * file_name, int approach) { Z3_context ctx; Z3_solver s; + unsigned i; + Z3_optimize opt; unsigned num_hard_cnstrs, num_soft_cnstrs; Z3_ast * hard_cnstrs, * soft_cnstrs; + Z3_ast_vector hard, objs; + Z3_app soft; unsigned result = 0; ctx = mk_context(); s = mk_solver(ctx); - Z3_parse_smtlib_file(ctx, file_name, 0, 0, 0, 0, 0, 0); - hard_cnstrs = get_hard_constraints(ctx, &num_hard_cnstrs); - soft_cnstrs = get_soft_constraints(ctx, &num_soft_cnstrs); + opt = Z3_mk_optimize(ctx); + Z3_optimize_inc_ref(ctx, opt); + Z3_optimize_from_file(ctx, opt, file_name); + hard = Z3_optimize_get_assertions(ctx, opt); + Z3_ast_vector_inc_ref(ctx, hard); + num_hard_cnstrs = Z3_ast_vector_size(ctx, hard); + hard_cnstrs = (Z3_ast *) malloc(sizeof(Z3_ast) * (num_hard_cnstrs)); + for (i = 0; i < num_hard_cnstrs; i++) { + hard_cnstrs[i] = Z3_ast_vector_get(ctx, hard, i); + } + objs = Z3_optimize_get_objectives(ctx, opt); + Z3_ast_vector_inc_ref(ctx, objs); + + // soft constraints are stored in a single objective which is a sum + // of if-then-else expressions. + soft = Z3_to_app(ctx, Z3_ast_vector_get(ctx, objs, 0)); + num_soft_cnstrs = Z3_get_app_num_args(ctx, soft); + soft_cnstrs = (Z3_ast *) malloc(sizeof(Z3_ast) * (num_soft_cnstrs)); + for (i = 0; i < num_soft_cnstrs; ++i) { + soft_cnstrs[i] = Z3_get_app_arg(ctx, Z3_to_app(ctx, Z3_get_app_arg(ctx, soft, i)), 0); + } + switch (approach) { case NAIVE_MAXSAT: result = naive_maxsat(ctx, s, num_hard_cnstrs, hard_cnstrs, num_soft_cnstrs, soft_cnstrs); @@ -633,6 +621,7 @@ int smtlib_maxsat(char * file_name, int approach) free_cnstr_array(hard_cnstrs); free_cnstr_array(soft_cnstrs); Z3_solver_dec_ref(ctx, s); + Z3_optimize_dec_ref(ctx, opt); return result; } diff --git a/scripts/mk_project.py b/scripts/mk_project.py index 05190f217..60b3b7756 100644 --- a/scripts/mk_project.py +++ b/scripts/mk_project.py @@ -9,7 +9,7 @@ from mk_util import * # Z3 Project definition def init_project_def(): - set_version(4, 5, 1, 0) + set_version(4, 6, 0, 0) add_lib('util', []) add_lib('lp', ['util'], 'util/lp') add_lib('polynomial', ['util'], 'math/polynomial') @@ -75,10 +75,9 @@ def init_project_def(): add_lib('smtlogic_tactics', ['ackermannization', 'sat_solver', 'arith_tactics', 'bv_tactics', 'nlsat_tactic', 'smt_tactic', 'aig_tactic', 'fp', 'muz','qe','nlsat_smt_tactic'], 'tactic/smtlogics') add_lib('fpa_tactics', ['fpa', 'core_tactics', 'bv_tactics', 'sat_tactic', 'smt_tactic', 'arith_tactics', 'smtlogic_tactics'], 'tactic/fpa') add_lib('portfolio', ['smtlogic_tactics', 'sat_solver', 'ufbv_tactic', 'fpa_tactics', 'aig_tactic', 'fp', 'qe','sls_tactic', 'subpaving_tactic'], 'tactic/portfolio') - add_lib('smtparser', ['portfolio'], 'parsers/smt') add_lib('opt', ['smt', 'smtlogic_tactics', 'sls_tactic', 'sat_solver'], 'opt') API_files = ['z3_api.h', 'z3_ast_containers.h', 'z3_algebraic.h', 'z3_polynomial.h', 'z3_rcf.h', 'z3_fixedpoint.h', 'z3_optimization.h', 'z3_interp.h', 'z3_fpa.h', 'z3_spacer.h'] - add_lib('api', ['portfolio', 'smtparser', 'realclosure', 'interp', 'opt'], + add_lib('api', ['portfolio', 'realclosure', 'interp', 'opt'], includes2install=['z3.h', 'z3_v1.h', 'z3_macros.h'] + API_files) add_exe('shell', ['api', 'sat', 'extra_cmds','opt'], exe_name='z3') add_exe('test', ['api', 'fuzzing', 'simplex'], exe_name='test-z3', install=False) diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index cfe6e5265..7cde89ae2 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -98,7 +98,6 @@ add_subdirectory(sat/sat_solver) add_subdirectory(tactic/smtlogics) add_subdirectory(tactic/fpa) add_subdirectory(tactic/portfolio) -add_subdirectory(parsers/smt) add_subdirectory(opt) add_subdirectory(api) add_subdirectory(api/dll) diff --git a/src/api/CMakeLists.txt b/src/api/CMakeLists.txt index a413376ac..fcdbb1651 100644 --- a/src/api/CMakeLists.txt +++ b/src/api/CMakeLists.txt @@ -71,5 +71,4 @@ z3_add_component(api opt portfolio realclosure - smtparser ) diff --git a/src/api/api_ast.cpp b/src/api/api_ast.cpp index e22603225..ae23ca100 100644 --- a/src/api/api_ast.cpp +++ b/src/api/api_ast.cpp @@ -832,30 +832,9 @@ extern "C" { case Z3_PRINT_LOW_LEVEL: buffer << mk_ll_pp(to_ast(a), mk_c(c)->m()); break; - case Z3_PRINT_SMTLIB_COMPLIANT: { - ast_smt_pp pp(mk_c(c)->m()); - pp_params params; - pp.set_simplify_implies(params.simplify_implies()); - ast* a1 = to_ast(a); - pp.set_logic(mk_c(c)->fparams().m_logic); - if (!is_expr(a1)) { - buffer << mk_pp(a1, mk_c(c)->m()); - break; - } - if (mk_c(c)->get_print_mode() == Z3_PRINT_SMTLIB_COMPLIANT) { - pp.display_expr(buffer, to_expr(a1)); - break; - } - if (mk_c(c)->get_print_mode() == Z3_PRINT_SMTLIB2_COMPLIANT) { - pp.display_expr_smt2(buffer, to_expr(a1)); - break; - } - break; - } - case Z3_PRINT_SMTLIB2_COMPLIANT: { + case Z3_PRINT_SMTLIB2_COMPLIANT: buffer << mk_ismt2_pp(to_ast(a), mk_c(c)->m()); break; - } default: UNREACHABLE(); } @@ -893,12 +872,7 @@ extern "C" { for (unsigned i = 0; i < num_assumptions; ++i) { pp.add_assumption(to_expr(assumptions[i])); } - if (mk_c(c)->get_print_mode() == Z3_PRINT_SMTLIB2_COMPLIANT) { - pp.display_smt2(buffer, to_expr(formula)); - } - else { - pp.display(buffer, to_expr(formula)); - } + pp.display_smt2(buffer, to_expr(formula)); return mk_c(c)->mk_external_string(buffer.str()); Z3_CATCH_RETURN(""); } diff --git a/src/api/api_context.cpp b/src/api/api_context.cpp index 1e3f7a0a4..73fb2c212 100644 --- a/src/api/api_context.cpp +++ b/src/api/api_context.cpp @@ -19,7 +19,6 @@ Revision History: --*/ #include #include "api/api_context.h" -#include "parsers/smt/smtparser.h" #include "util/version.h" #include "ast/ast_pp.h" #include "ast/ast_ll_pp.h" @@ -89,8 +88,6 @@ namespace api { m_print_mode = Z3_PRINT_SMTLIB_FULL; m_searching = false; - m_smtlib_parser = 0; - m_smtlib_parser_has_decls = false; m_interruptable = 0; m_error_handler = &default_error_handler; @@ -111,7 +108,6 @@ namespace api { context::~context() { - reset_parser(); m_last_obj = 0; u_map::iterator it = m_allocated_objects.begin(); while (it != m_allocated_objects.end()) { @@ -304,39 +300,6 @@ namespace api { } } - - // ------------------------ - // - // Parser interface for backward compatibility - // - // ------------------------ - - void context::reset_parser() { - if (m_smtlib_parser) { - dealloc(m_smtlib_parser); - m_smtlib_parser = 0; - m_smtlib_parser_has_decls = false; - m_smtlib_parser_decls.reset(); - m_smtlib_parser_sorts.reset(); - } - SASSERT(!m_smtlib_parser_has_decls); - } - - void context::extract_smtlib_parser_decls() { - if (m_smtlib_parser) { - if (!m_smtlib_parser_has_decls) { - smtlib::symtable * table = m_smtlib_parser->get_benchmark()->get_symtable(); - table->get_func_decls(m_smtlib_parser_decls); - table->get_sorts(m_smtlib_parser_sorts); - m_smtlib_parser_has_decls = true; - } - } - else { - m_smtlib_parser_decls.reset(); - m_smtlib_parser_sorts.reset(); - } - } - // ------------------------ // // RCF manager diff --git a/src/api/api_context.h b/src/api/api_context.h index 6f8dc43f6..58893d1c1 100644 --- a/src/api/api_context.h +++ b/src/api/api_context.h @@ -220,19 +220,11 @@ namespace api { // ------------------------ // - // Parser interface for backward compatibility + // Parser interface // // ------------------------ - // TODO: move to a "parser" object visible to the external world. - std::string m_smtlib_error_buffer; - smtlib::parser * m_smtlib_parser; - bool m_smtlib_parser_has_decls; - ptr_vector m_smtlib_parser_decls; - ptr_vector m_smtlib_parser_sorts; - - void reset_parser(); - void extract_smtlib_parser_decls(); + std::string m_parser_error_buffer; }; diff --git a/src/api/api_interp.cpp b/src/api/api_interp.cpp index 416c71adf..d6f4e1128 100644 --- a/src/api/api_interp.cpp +++ b/src/api/api_interp.cpp @@ -510,31 +510,15 @@ extern "C" { read_error.clear(); try { std::string foo(filename); - if (foo.size() >= 5 && foo.substr(foo.size() - 5) == ".smt2"){ - Z3_ast assrts = Z3_parse_smtlib2_file(ctx, filename, 0, 0, 0, 0, 0, 0); - Z3_app app = Z3_to_app(ctx, assrts); - int nconjs = Z3_get_app_num_args(ctx, app); - assertions.resize(nconjs); - for (int k = 0; k < nconjs; k++) - assertions[k] = Z3_get_app_arg(ctx, app, k); - } - else { - Z3_parse_smtlib_file(ctx, filename, 0, 0, 0, 0, 0, 0); - int numa = Z3_get_smtlib_num_assumptions(ctx); - int numf = Z3_get_smtlib_num_formulas(ctx); - int num = numa + numf; - - assertions.resize(num); - for (int j = 0; j < num; j++){ - if (j < numa) - assertions[j] = Z3_get_smtlib_assumption(ctx, j); - else - assertions[j] = Z3_get_smtlib_formula(ctx, j - numa); - } - } + Z3_ast assrts = Z3_parse_smtlib2_file(ctx, filename, 0, 0, 0, 0, 0, 0); + Z3_app app = Z3_to_app(ctx, assrts); + int nconjs = Z3_get_app_num_args(ctx, app); + assertions.resize(nconjs); + for (int k = 0; k < nconjs; k++) + assertions[k] = Z3_get_app_arg(ctx, app, k); } catch (...) { - read_error << "SMTLIB parse error: " << Z3_get_smtlib_error(ctx); + read_error << "SMTLIB parse error: " << Z3_get_parser_error(ctx); read_msg = read_error.str(); *error = read_msg.c_str(); return false; diff --git a/src/api/api_opt.cpp b/src/api/api_opt.cpp index 9f5f7dd5d..ac11e1a33 100644 --- a/src/api/api_opt.cpp +++ b/src/api/api_opt.cpp @@ -286,11 +286,23 @@ extern "C" { scoped_ptr ctx = alloc(cmd_context, false, &m); install_opt_cmds(*ctx.get(), to_optimize_ptr(opt)); ctx->set_ignore_check(true); - if (!parse_smt2_commands(*ctx.get(), s)) { + std::stringstream errstrm; + ctx->set_regular_stream(errstrm); + try { + if (!parse_smt2_commands(*ctx.get(), s)) { + mk_c(c)->m_parser_error_buffer = errstrm.str(); + ctx = nullptr; + SET_ERROR_CODE(Z3_PARSER_ERROR); + return; + } + } + catch (z3_exception& e) { + errstrm << e.msg(); + mk_c(c)->m_parser_error_buffer = errstrm.str(); ctx = nullptr; SET_ERROR_CODE(Z3_PARSER_ERROR); return; - } + } ptr_vector::const_iterator it = ctx->begin_assertions(); ptr_vector::const_iterator end = ctx->end_assertions(); for (; it != end; ++it) { diff --git a/src/api/api_parsers.cpp b/src/api/api_parsers.cpp index b3252281b..d5a98672b 100644 --- a/src/api/api_parsers.cpp +++ b/src/api/api_parsers.cpp @@ -22,232 +22,16 @@ Revision History: #include "api/api_util.h" #include "cmd_context/cmd_context.h" #include "parsers/smt2/smt2parser.h" -#include "parsers/smt/smtparser.h" #include "solver/solver_na2as.h" extern "C" { - void init_smtlib_parser(Z3_context c, - unsigned num_sorts, - Z3_symbol const sort_names[], - Z3_sort const types[], - unsigned num_decls, - Z3_symbol const decl_names[], - Z3_func_decl const decls[]) { - mk_c(c)->reset_parser(); - mk_c(c)->m_smtlib_parser = smtlib::parser::create(mk_c(c)->m()); - mk_c(c)->m_smtlib_parser->initialize_smtlib(); - smtlib::symtable * table = mk_c(c)->m_smtlib_parser->get_benchmark()->get_symtable(); - for (unsigned i = 0; i < num_sorts; i++) { - table->insert(to_symbol(sort_names[i]), to_sort(types[i])); - } - for (unsigned i = 0; i < num_decls; i++) { - table->insert(to_symbol(decl_names[i]), to_func_decl(decls[i])); - } - } - - void Z3_API Z3_parse_smtlib_string(Z3_context c, - const char * str, - unsigned num_sorts, - Z3_symbol const sort_names[], - Z3_sort const sorts[], - unsigned num_decls, - Z3_symbol const decl_names[], - Z3_func_decl const decls[]) { - Z3_TRY; - LOG_Z3_parse_smtlib_string(c, str, num_sorts, sort_names, sorts, num_decls, decl_names, decls); - scoped_ptr outs = alloc(std::ostringstream); - bool ok = false; - RESET_ERROR_CODE(); - init_smtlib_parser(c, num_sorts, sort_names, sorts, num_decls, decl_names, decls); - mk_c(c)->m_smtlib_parser->set_error_stream(*outs); - try { - ok = mk_c(c)->m_smtlib_parser->parse_string(str); - } - catch (...) { - ok = false; - } - mk_c(c)->m_smtlib_error_buffer = outs->str(); - outs = nullptr; - if (!ok) { - mk_c(c)->reset_parser(); - SET_ERROR_CODE(Z3_PARSER_ERROR); - } - Z3_CATCH; - } - - void Z3_API Z3_parse_smtlib_file(Z3_context c, - const char * file_name, - unsigned num_sorts, - Z3_symbol const sort_names[], - Z3_sort const types[], - unsigned num_decls, - Z3_symbol const decl_names[], - Z3_func_decl const decls[]) { + Z3_string Z3_API Z3_get_parser_error(Z3_context c) { Z3_TRY; - LOG_Z3_parse_smtlib_file(c, file_name, num_sorts, sort_names, types, num_decls, decl_names, decls); - bool ok = false; - RESET_ERROR_CODE(); - scoped_ptr outs = alloc(std::ostringstream); - init_smtlib_parser(c, num_sorts, sort_names, types, num_decls, decl_names, decls); - mk_c(c)->m_smtlib_parser->set_error_stream(*outs); - try { - ok = mk_c(c)->m_smtlib_parser->parse_file(file_name); - } - catch(...) { - ok = false; - } - mk_c(c)->m_smtlib_error_buffer = outs->str(); - outs = nullptr; - if (!ok) { - mk_c(c)->reset_parser(); - SET_ERROR_CODE(Z3_PARSER_ERROR); - } - Z3_CATCH; - } - - unsigned Z3_API Z3_get_smtlib_num_formulas(Z3_context c) { - Z3_TRY; - LOG_Z3_get_smtlib_num_formulas(c); - RESET_ERROR_CODE(); - if (mk_c(c)->m_smtlib_parser) { - return mk_c(c)->m_smtlib_parser->get_benchmark()->get_num_formulas(); - } - SET_ERROR_CODE(Z3_NO_PARSER); - return 0; - Z3_CATCH_RETURN(0); - } - - Z3_ast Z3_API Z3_get_smtlib_formula(Z3_context c, unsigned i) { - Z3_TRY; - LOG_Z3_get_smtlib_formula(c, i); - RESET_ERROR_CODE(); - if (mk_c(c)->m_smtlib_parser) { - if (i < mk_c(c)->m_smtlib_parser->get_benchmark()->get_num_formulas()) { - ast * f = mk_c(c)->m_smtlib_parser->get_benchmark()->begin_formulas()[i]; - mk_c(c)->save_ast_trail(f); - RETURN_Z3(of_ast(f)); - } - else { - SET_ERROR_CODE(Z3_IOB); - } - } - else { - SET_ERROR_CODE(Z3_NO_PARSER); - } - RETURN_Z3(0); - Z3_CATCH_RETURN(0); - } - - unsigned Z3_API Z3_get_smtlib_num_assumptions(Z3_context c) { - Z3_TRY; - LOG_Z3_get_smtlib_num_assumptions(c); - RESET_ERROR_CODE(); - if (mk_c(c)->m_smtlib_parser) { - return mk_c(c)->m_smtlib_parser->get_benchmark()->get_num_axioms(); - } - SET_ERROR_CODE(Z3_NO_PARSER); - return 0; - Z3_CATCH_RETURN(0); - } - - Z3_ast Z3_API Z3_get_smtlib_assumption(Z3_context c, unsigned i) { - Z3_TRY; - LOG_Z3_get_smtlib_assumption(c, i); - RESET_ERROR_CODE(); - if (mk_c(c)->m_smtlib_parser) { - if (i < mk_c(c)->m_smtlib_parser->get_benchmark()->get_num_axioms()) { - ast * a = mk_c(c)->m_smtlib_parser->get_benchmark()->begin_axioms()[i]; - mk_c(c)->save_ast_trail(a); - RETURN_Z3(of_ast(a)); - } - else { - SET_ERROR_CODE(Z3_IOB); - } - } - else { - SET_ERROR_CODE(Z3_NO_PARSER); - } - RETURN_Z3(0); - Z3_CATCH_RETURN(0); - } - - unsigned Z3_API Z3_get_smtlib_num_decls(Z3_context c) { - Z3_TRY; - LOG_Z3_get_smtlib_num_decls(c); - RESET_ERROR_CODE(); - if (mk_c(c)->m_smtlib_parser) { - mk_c(c)->extract_smtlib_parser_decls(); - return mk_c(c)->m_smtlib_parser_decls.size(); - } - SET_ERROR_CODE(Z3_NO_PARSER); - return 0; - Z3_CATCH_RETURN(0); - } - - Z3_func_decl Z3_API Z3_get_smtlib_decl(Z3_context c, unsigned i) { - Z3_TRY; - LOG_Z3_get_smtlib_decl(c, i); + LOG_Z3_get_parser_error(c); RESET_ERROR_CODE(); - mk_c(c)->extract_smtlib_parser_decls(); - if (mk_c(c)->m_smtlib_parser) { - if (i < mk_c(c)->m_smtlib_parser_decls.size()) { - func_decl * d = mk_c(c)->m_smtlib_parser_decls[i]; - mk_c(c)->save_ast_trail(d); - RETURN_Z3(of_func_decl(d)); - } - else { - SET_ERROR_CODE(Z3_IOB); - } - } - else { - SET_ERROR_CODE(Z3_NO_PARSER); - } - RETURN_Z3(0); - Z3_CATCH_RETURN(0); - } - - unsigned Z3_API Z3_get_smtlib_num_sorts(Z3_context c) { - Z3_TRY; - LOG_Z3_get_smtlib_num_sorts(c); - RESET_ERROR_CODE(); - if (mk_c(c)->m_smtlib_parser) { - mk_c(c)->extract_smtlib_parser_decls(); - return mk_c(c)->m_smtlib_parser_sorts.size(); - } - SET_ERROR_CODE(Z3_NO_PARSER); - return 0; - Z3_CATCH_RETURN(0); - } - - Z3_sort Z3_API Z3_get_smtlib_sort(Z3_context c, unsigned i) { - Z3_TRY; - LOG_Z3_get_smtlib_sort(c, i); - RESET_ERROR_CODE(); - if (mk_c(c)->m_smtlib_parser) { - mk_c(c)->extract_smtlib_parser_decls(); - if (i < mk_c(c)->m_smtlib_parser_sorts.size()) { - sort* s = mk_c(c)->m_smtlib_parser_sorts[i]; - mk_c(c)->save_ast_trail(s); - RETURN_Z3(of_sort(s)); - } - else { - SET_ERROR_CODE(Z3_IOB); - } - } - else { - SET_ERROR_CODE(Z3_NO_PARSER); - } - RETURN_Z3(0); - Z3_CATCH_RETURN(0); - } - - Z3_string Z3_API Z3_get_smtlib_error(Z3_context c) { - Z3_TRY; - LOG_Z3_get_smtlib_error(c); - RESET_ERROR_CODE(); - return mk_c(c)->m_smtlib_error_buffer.c_str(); + return mk_c(c)->m_parser_error_buffer.c_str(); Z3_CATCH_RETURN(""); } @@ -268,10 +52,26 @@ extern "C" { ctx->insert(to_symbol(decl_names[i]), to_func_decl(decls[i])); } for (unsigned i = 0; i < num_sorts; ++i) { - psort* ps = ctx->pm().mk_psort_cnst(to_sort(sorts[i])); - ctx->insert(ctx->pm().mk_psort_user_decl(0, to_symbol(sort_names[i]), ps)); + sort* srt = to_sort(sorts[i]); + symbol name(to_symbol(sort_names[i])); + if (!ctx->find_psort_decl(name)) { + psort* ps = ctx->pm().mk_psort_cnst(srt); + ctx->insert(ctx->pm().mk_psort_user_decl(0, name, ps)); + } } - if (!parse_smt2_commands(*ctx.get(), is)) { + std::stringstream errstrm; + ctx->set_regular_stream(errstrm); + try { + if (!parse_smt2_commands(*ctx.get(), is)) { + ctx = nullptr; + mk_c(c)->m_parser_error_buffer = errstrm.str(); + SET_ERROR_CODE(Z3_PARSER_ERROR); + return of_ast(mk_c(c)->m().mk_true()); + } + } + catch (z3_exception& e) { + errstrm << e.msg(); + mk_c(c)->m_parser_error_buffer = errstrm.str(); ctx = nullptr; SET_ERROR_CODE(Z3_PARSER_ERROR); return of_ast(mk_c(c)->m().mk_true()); diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index 4b5e9d04e..236750bdf 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -174,6 +174,15 @@ namespace z3 { return e; } + void check_parser_error() const { + Z3_error_code e = Z3_get_error_code(*this); + if (e != Z3_OK && enable_exceptions()) { + Z3_string s = Z3_get_parser_error(*this); + if (s && *s) Z3_THROW(exception(s)); + } + check_error(); + } + /** \brief The C++ API uses by defaults exceptions on errors. For applications that don't work well with exceptions (there should be only few) @@ -2774,13 +2783,12 @@ namespace z3 { inline expr context::parse_string(char const* s) { Z3_ast r = Z3_parse_smtlib2_string(*this, s, 0, 0, 0, 0, 0, 0); - check_error(); - return expr(*this, r); - + check_parser_error(); + return expr(*this, r); } inline expr context::parse_file(char const* s) { Z3_ast r = Z3_parse_smtlib2_file(*this, s, 0, 0, 0, 0, 0, 0); - check_error(); + check_parser_error(); return expr(*this, r); } @@ -2796,7 +2804,7 @@ namespace z3 { decl_names[i] = decls[i].name(); } Z3_ast r = Z3_parse_smtlib2_string(*this, s, sorts.size(), sort_names.ptr(), sorts1.ptr(), decls.size(), decl_names.ptr(), decls1.ptr()); - check_error(); + check_parser_error(); return expr(*this, r); } @@ -2812,7 +2820,7 @@ namespace z3 { decl_names[i] = decls[i].name(); } Z3_ast r = Z3_parse_smtlib2_file(*this, s, sorts.size(), sort_names.ptr(), sorts1.ptr(), decls.size(), decl_names.ptr(), decls1.ptr()); - check_error(); + check_parser_error(); return expr(*this, r); } diff --git a/src/api/dotnet/Context.cs b/src/api/dotnet/Context.cs index 914cee615..ac23d1dbc 100644 --- a/src/api/dotnet/Context.cs +++ b/src/api/dotnet/Context.cs @@ -3320,160 +3320,10 @@ namespace Microsoft.Z3 #endregion #region SMT Files & Strings - /// - /// Convert a benchmark into an SMT-LIB formatted string. - /// - /// Name of the benchmark. The argument is optional. - /// The benchmark logic. - /// The status string (sat, unsat, or unknown) - /// Other attributes, such as source, difficulty or category. - /// Auxiliary assumptions. - /// Formula to be checked for consistency in conjunction with assumptions. - /// A string representation of the benchmark. - public string BenchmarkToSMTString(string name, string logic, string status, string attributes, - BoolExpr[] assumptions, BoolExpr formula) - { - Contract.Requires(assumptions != null); - Contract.Requires(formula != null); - Contract.Ensures(Contract.Result() != null); - - return Native.Z3_benchmark_to_smtlib_string(nCtx, name, logic, status, attributes, - (uint)assumptions.Length, AST.ArrayToNative(assumptions), - formula.NativeObject); - } - - /// - /// Parse the given string using the SMT-LIB parser. - /// - /// - /// The symbol table of the parser can be initialized using the given sorts and declarations. - /// The symbols in the arrays and - /// don't need to match the names of the sorts and declarations in the arrays - /// and . This is a useful feature since we can use arbitrary names to - /// reference sorts and declarations. - /// - public void ParseSMTLIBString(string str, Symbol[] sortNames = null, Sort[] sorts = null, Symbol[] declNames = null, FuncDecl[] decls = null) - { - uint csn = Symbol.ArrayLength(sortNames); - uint cs = Sort.ArrayLength(sorts); - uint cdn = Symbol.ArrayLength(declNames); - uint cd = AST.ArrayLength(decls); - if (csn != cs || cdn != cd) - throw new Z3Exception("Argument size mismatch"); - Native.Z3_parse_smtlib_string(nCtx, str, - AST.ArrayLength(sorts), Symbol.ArrayToNative(sortNames), AST.ArrayToNative(sorts), - AST.ArrayLength(decls), Symbol.ArrayToNative(declNames), AST.ArrayToNative(decls)); - } - - /// - /// Parse the given file using the SMT-LIB parser. - /// - /// - public void ParseSMTLIBFile(string fileName, Symbol[] sortNames = null, Sort[] sorts = null, Symbol[] declNames = null, FuncDecl[] decls = null) - { - uint csn = Symbol.ArrayLength(sortNames); - uint cs = Sort.ArrayLength(sorts); - uint cdn = Symbol.ArrayLength(declNames); - uint cd = AST.ArrayLength(decls); - if (csn != cs || cdn != cd) - throw new Z3Exception("Argument size mismatch"); - Native.Z3_parse_smtlib_file(nCtx, fileName, - AST.ArrayLength(sorts), Symbol.ArrayToNative(sortNames), AST.ArrayToNative(sorts), - AST.ArrayLength(decls), Symbol.ArrayToNative(declNames), AST.ArrayToNative(decls)); - } - - /// - /// The number of SMTLIB formulas parsed by the last call to ParseSMTLIBString or ParseSMTLIBFile. - /// - public uint NumSMTLIBFormulas { get { return Native.Z3_get_smtlib_num_formulas(nCtx); } } - - /// - /// The formulas parsed by the last call to ParseSMTLIBString or ParseSMTLIBFile. - /// - public BoolExpr[] SMTLIBFormulas - { - get - { - Contract.Ensures(Contract.Result() != null); - - uint n = NumSMTLIBFormulas; - BoolExpr[] res = new BoolExpr[n]; - for (uint i = 0; i < n; i++) - res[i] = (BoolExpr)Expr.Create(this, Native.Z3_get_smtlib_formula(nCtx, i)); - return res; - } - } - - /// - /// The number of SMTLIB assumptions parsed by the last call to ParseSMTLIBString or ParseSMTLIBFile. - /// - public uint NumSMTLIBAssumptions { get { return Native.Z3_get_smtlib_num_assumptions(nCtx); } } - - /// - /// The assumptions parsed by the last call to ParseSMTLIBString or ParseSMTLIBFile. - /// - public BoolExpr[] SMTLIBAssumptions - { - get - { - Contract.Ensures(Contract.Result() != null); - - uint n = NumSMTLIBAssumptions; - BoolExpr[] res = new BoolExpr[n]; - for (uint i = 0; i < n; i++) - res[i] = (BoolExpr)Expr.Create(this, Native.Z3_get_smtlib_assumption(nCtx, i)); - return res; - } - } - - /// - /// The number of SMTLIB declarations parsed by the last call to ParseSMTLIBString or ParseSMTLIBFile. - /// - public uint NumSMTLIBDecls { get { return Native.Z3_get_smtlib_num_decls(nCtx); } } - - /// - /// The declarations parsed by the last call to ParseSMTLIBString or ParseSMTLIBFile. - /// - public FuncDecl[] SMTLIBDecls - { - get - { - Contract.Ensures(Contract.Result() != null); - - uint n = NumSMTLIBDecls; - FuncDecl[] res = new FuncDecl[n]; - for (uint i = 0; i < n; i++) - res[i] = new FuncDecl(this, Native.Z3_get_smtlib_decl(nCtx, i)); - return res; - } - } - - /// - /// The number of SMTLIB sorts parsed by the last call to ParseSMTLIBString or ParseSMTLIBFile. - /// - public uint NumSMTLIBSorts { get { return Native.Z3_get_smtlib_num_sorts(nCtx); } } - - /// - /// The declarations parsed by the last call to ParseSMTLIBString or ParseSMTLIBFile. - /// - public Sort[] SMTLIBSorts - { - get - { - Contract.Ensures(Contract.Result() != null); - - uint n = NumSMTLIBSorts; - Sort[] res = new Sort[n]; - for (uint i = 0; i < n; i++) - res[i] = Sort.Create(this, Native.Z3_get_smtlib_sort(nCtx, i)); - return res; - } - } /// /// Parse the given string using the SMT-LIB2 parser. /// - /// /// A conjunction of assertions in the scope (up to push/pop) at the end of the string. public BoolExpr ParseSMTLIB2String(string str, Symbol[] sortNames = null, Sort[] sorts = null, Symbol[] declNames = null, FuncDecl[] decls = null) { diff --git a/src/api/java/Context.java b/src/api/java/Context.java index 76303d670..3458f4d97 100644 --- a/src/api/java/Context.java +++ b/src/api/java/Context.java @@ -2540,147 +2540,8 @@ public class Context implements AutoCloseable { AST.arrayToNative(assumptions), formula.getNativeObject()); } - /** - * Parse the given string using the SMT-LIB parser. - * Remarks: The symbol - * table of the parser can be initialized using the given sorts and - * declarations. The symbols in the arrays {@code sortNames} and - * {@code declNames} don't need to match the names of the sorts - * and declarations in the arrays {@code sorts} and {@code decls}. This is a useful feature since we can use arbitrary names - * to reference sorts and declarations. - **/ - public void parseSMTLIBString(String str, Symbol[] sortNames, Sort[] sorts, - Symbol[] declNames, FuncDecl[] decls) - { - int csn = Symbol.arrayLength(sortNames); - int cs = Sort.arrayLength(sorts); - int cdn = Symbol.arrayLength(declNames); - int cd = AST.arrayLength(decls); - if (csn != cs || cdn != cd) - throw new Z3Exception("Argument size mismatch"); - Native.parseSmtlibString(nCtx(), str, AST.arrayLength(sorts), - Symbol.arrayToNative(sortNames), AST.arrayToNative(sorts), - AST.arrayLength(decls), Symbol.arrayToNative(declNames), - AST.arrayToNative(decls)); - } - - /** - * Parse the given file using the SMT-LIB parser. - * @see #parseSMTLIBString - **/ - public void parseSMTLIBFile(String fileName, Symbol[] sortNames, - Sort[] sorts, Symbol[] declNames, FuncDecl[] decls) - - { - int csn = Symbol.arrayLength(sortNames); - int cs = Sort.arrayLength(sorts); - int cdn = Symbol.arrayLength(declNames); - int cd = AST.arrayLength(decls); - if (csn != cs || cdn != cd) - throw new Z3Exception("Argument size mismatch"); - Native.parseSmtlibFile(nCtx(), fileName, AST.arrayLength(sorts), - Symbol.arrayToNative(sortNames), AST.arrayToNative(sorts), - AST.arrayLength(decls), Symbol.arrayToNative(declNames), - AST.arrayToNative(decls)); - } - - /** - * The number of SMTLIB formulas parsed by the last call to - * {@code ParseSMTLIBString} or {@code ParseSMTLIBFile}. - **/ - public int getNumSMTLIBFormulas() - { - return Native.getSmtlibNumFormulas(nCtx()); - } - - /** - * The formulas parsed by the last call to {@code ParseSMTLIBString} or - * {@code ParseSMTLIBFile}. - **/ - public BoolExpr[] getSMTLIBFormulas() - { - - int n = getNumSMTLIBFormulas(); - BoolExpr[] res = new BoolExpr[n]; - for (int i = 0; i < n; i++) - res[i] = (BoolExpr) Expr.create(this, - Native.getSmtlibFormula(nCtx(), i)); - return res; - } - - /** - * The number of SMTLIB assumptions parsed by the last call to - * {@code ParseSMTLIBString} or {@code ParseSMTLIBFile}. - **/ - public int getNumSMTLIBAssumptions() - { - return Native.getSmtlibNumAssumptions(nCtx()); - } - - /** - * The assumptions parsed by the last call to {@code ParseSMTLIBString} - * or {@code ParseSMTLIBFile}. - **/ - public BoolExpr[] getSMTLIBAssumptions() - { - - int n = getNumSMTLIBAssumptions(); - BoolExpr[] res = new BoolExpr[n]; - for (int i = 0; i < n; i++) - res[i] = (BoolExpr) Expr.create(this, - Native.getSmtlibAssumption(nCtx(), i)); - return res; - } - - /** - * The number of SMTLIB declarations parsed by the last call to - * {@code ParseSMTLIBString} or {@code ParseSMTLIBFile}. - **/ - public int getNumSMTLIBDecls() - { - return Native.getSmtlibNumDecls(nCtx()); - } - - /** - * The declarations parsed by the last call to - * {@code ParseSMTLIBString} or {@code ParseSMTLIBFile}. - **/ - public FuncDecl[] getSMTLIBDecls() - { - - int n = getNumSMTLIBDecls(); - FuncDecl[] res = new FuncDecl[n]; - for (int i = 0; i < n; i++) - res[i] = new FuncDecl(this, Native.getSmtlibDecl(nCtx(), i)); - return res; - } - - /** - * The number of SMTLIB sorts parsed by the last call to - * {@code ParseSMTLIBString} or {@code ParseSMTLIBFile}. - **/ - public int getNumSMTLIBSorts() - { - return Native.getSmtlibNumSorts(nCtx()); - } - - /** - * The declarations parsed by the last call to - * {@code ParseSMTLIBString} or {@code ParseSMTLIBFile}. - **/ - public Sort[] getSMTLIBSorts() - { - - int n = getNumSMTLIBSorts(); - Sort[] res = new Sort[n]; - for (int i = 0; i < n; i++) - res[i] = Sort.create(this, Native.getSmtlibSort(nCtx(), i)); - return res; - } - /** * Parse the given string using the SMT-LIB2 parser. - * @see #parseSMTLIBString * * @return A conjunction of assertions in the scope (up to push/pop) at the * end of the string. diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index 1f050d3bd..2304491c8 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -6668,11 +6668,17 @@ class Fixedpoint(Z3PPObject): def parse_string(self, s): """Parse rules and queries from a string""" - return AstVector(Z3_fixedpoint_from_string(self.ctx.ref(), self.fixedpoint, s), self.ctx) + try: + return AstVector(Z3_fixedpoint_from_string(self.ctx.ref(), self.fixedpoint, s), self.ctx) + except Z3Exception as e: + _handle_parse_error(e, self.ctx) def parse_file(self, f): """Parse rules and queries from a file""" - return AstVector(Z3_fixedpoint_from_file(self.ctx.ref(), self.fixedpoint, f), self.ctx) + try: + return AstVector(Z3_fixedpoint_from_file(self.ctx.ref(), self.fixedpoint, f), self.ctx) + except Z3Exception as e: + _handle_parse_error(e, self.ctx) def get_rules(self): """retrieve rules that have been added to fixedpoint context""" @@ -6995,15 +7001,21 @@ class Optimize(Z3PPObject): def upper_values(self, obj): if not isinstance(obj, OptimizeObjective): raise Z3Exception("Expecting objective handle returned by maximize/minimize") - return obj.upper_values() + return obj.upper_values() def from_file(self, filename): """Parse assertions and objectives from a file""" - Z3_optimize_from_file(self.ctx.ref(), self.optimize, filename) + try: + Z3_optimize_from_file(self.ctx.ref(), self.optimize, filename) + except Z3Exception as e: + _handle_parse_error(e, self.ctx) def from_string(self, s): """Parse assertions and objectives from a string""" - Z3_optimize_from_string(self.ctx.ref(), self.optimize, s) + try: + Z3_optimize_from_string(self.ctx.ref(), self.optimize, s) + except Z3Exception as e: + _handle_parse_error(e, self.ctx) def assertions(self): """Return an AST vector containing all added constraints.""" @@ -8071,6 +8083,12 @@ def _dict2darray(decls, ctx): i = i + 1 return sz, _names, _decls +def _handle_parse_error(ex, ctx): + msg = Z3_get_parser_error(ctx.ref()) + if msg != "": + raise Z3Exception(msg) + raise ex + def parse_smt2_string(s, sorts={}, decls={}, ctx=None): """Parse a string in SMT 2.0 format using the given sorts and decls. @@ -8089,7 +8107,10 @@ def parse_smt2_string(s, sorts={}, decls={}, ctx=None): ctx = _get_ctx(ctx) ssz, snames, ssorts = _dict2sarray(sorts, ctx) dsz, dnames, ddecls = _dict2darray(decls, ctx) - return _to_expr_ref(Z3_parse_smtlib2_string(ctx.ref(), s, ssz, snames, ssorts, dsz, dnames, ddecls), ctx) + try: + return _to_expr_ref(Z3_parse_smtlib2_string(ctx.ref(), s, ssz, snames, ssorts, dsz, dnames, ddecls), ctx) + except Z3Exception as e: + _handle_parse_error(e, ctx) def parse_smt2_file(f, sorts={}, decls={}, ctx=None): """Parse a file in SMT 2.0 format using the given sorts and decls. @@ -8099,7 +8120,10 @@ def parse_smt2_file(f, sorts={}, decls={}, ctx=None): ctx = _get_ctx(ctx) ssz, snames, ssorts = _dict2sarray(sorts, ctx) dsz, dnames, ddecls = _dict2darray(decls, ctx) - return _to_expr_ref(Z3_parse_smtlib2_file(ctx.ref(), f, ssz, snames, ssorts, dsz, dnames, ddecls), ctx) + try: + return _to_expr_ref(Z3_parse_smtlib2_file(ctx.ref(), f, ssz, snames, ssorts, dsz, dnames, ddecls), ctx) + except Z3Exception as e: + _handle_parse_error(e, ctx) def Interpolant(a,ctx=None): """Create an interpolation operator. diff --git a/src/api/z3_api.h b/src/api/z3_api.h index cf1c8fca7..d620254d1 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -1314,13 +1314,11 @@ typedef enum { - Z3_PRINT_SMTLIB_FULL: Print AST nodes in SMTLIB verbose format. - Z3_PRINT_LOW_LEVEL: Print AST nodes using a low-level format. - - Z3_PRINT_SMTLIB_COMPLIANT: Print AST nodes in SMTLIB 1.x compliant format. - Z3_PRINT_SMTLIB2_COMPLIANT: Print AST nodes in SMTLIB 2.x compliant format. */ typedef enum { Z3_PRINT_SMTLIB_FULL, Z3_PRINT_LOW_LEVEL, - Z3_PRINT_SMTLIB_COMPLIANT, Z3_PRINT_SMTLIB2_COMPLIANT } Z3_ast_print_mode; @@ -4301,7 +4299,7 @@ extern "C" { /** \brief Return the i-th argument of the given application. - \pre i < Z3_get_num_args(c, a) + \pre i < Z3_get_app_num_args(c, a) def_API('Z3_get_app_arg', AST, (_in(CONTEXT), _in(APP), _in(UINT))) */ @@ -5116,7 +5114,7 @@ extern "C" { To print shared common subexpressions only once, use the Z3_PRINT_LOW_LEVEL mode. To print in way that conforms to SMT-LIB standards and uses let - expressions to share common sub-expressions use Z3_PRINT_SMTLIB_COMPLIANT. + expressions to share common sub-expressions use Z3_PRINT_SMTLIB2_COMPLIANT. \sa Z3_ast_to_string \sa Z3_pattern_to_string @@ -5228,115 +5226,13 @@ extern "C" { Z3_symbol const decl_names[], Z3_func_decl const decls[]); - /** - \brief Parse the given string using the SMT-LIB parser. - - The symbol table of the parser can be initialized using the given sorts and declarations. - The symbols in the arrays \c sort_names and \c decl_names don't need to match the names - of the sorts and declarations in the arrays \c sorts and \c decls. This is an useful feature - since we can use arbitrary names to reference sorts and declarations defined using the C API. - - The formulas, assumptions and declarations defined in \c str can be extracted using the functions: - #Z3_get_smtlib_num_formulas, #Z3_get_smtlib_formula, #Z3_get_smtlib_num_assumptions, #Z3_get_smtlib_assumption, - #Z3_get_smtlib_num_decls, and #Z3_get_smtlib_decl. - - def_API('Z3_parse_smtlib_string', VOID, (_in(CONTEXT), _in(STRING), _in(UINT), _in_array(2, SYMBOL), _in_array(2, SORT), _in(UINT), _in_array(5, SYMBOL), _in_array(5, FUNC_DECL))) - */ - void Z3_API Z3_parse_smtlib_string(Z3_context c, - Z3_string str, - unsigned num_sorts, - Z3_symbol const sort_names[], - Z3_sort const sorts[], - unsigned num_decls, - Z3_symbol const decl_names[], - Z3_func_decl const decls[] - ); - - /** - \brief Similar to #Z3_parse_smtlib_string, but reads the benchmark from a file. - - def_API('Z3_parse_smtlib_file', VOID, (_in(CONTEXT), _in(STRING), _in(UINT), _in_array(2, SYMBOL), _in_array(2, SORT), _in(UINT), _in_array(5, SYMBOL), _in_array(5, FUNC_DECL))) - */ - void Z3_API Z3_parse_smtlib_file(Z3_context c, - Z3_string file_name, - unsigned num_sorts, - Z3_symbol const sort_names[], - Z3_sort const sorts[], - unsigned num_decls, - Z3_symbol const decl_names[], - Z3_func_decl const decls[] - ); - - /** - \brief Return the number of SMTLIB formulas parsed by the last call to #Z3_parse_smtlib_string or #Z3_parse_smtlib_file. - - def_API('Z3_get_smtlib_num_formulas', UINT, (_in(CONTEXT), )) - */ - unsigned Z3_API Z3_get_smtlib_num_formulas(Z3_context c); - - /** - \brief Return the i-th formula parsed by the last call to #Z3_parse_smtlib_string or #Z3_parse_smtlib_file. - - \pre i < Z3_get_smtlib_num_formulas(c) - - def_API('Z3_get_smtlib_formula', AST, (_in(CONTEXT), _in(UINT))) - */ - Z3_ast Z3_API Z3_get_smtlib_formula(Z3_context c, unsigned i); - - /** - \brief Return the number of SMTLIB assumptions parsed by #Z3_parse_smtlib_string or #Z3_parse_smtlib_file. - - def_API('Z3_get_smtlib_num_assumptions', UINT, (_in(CONTEXT), )) - */ - unsigned Z3_API Z3_get_smtlib_num_assumptions(Z3_context c); - - /** - \brief Return the i-th assumption parsed by the last call to #Z3_parse_smtlib_string or #Z3_parse_smtlib_file. - - \pre i < Z3_get_smtlib_num_assumptions(c) - - def_API('Z3_get_smtlib_assumption', AST, (_in(CONTEXT), _in(UINT))) - */ - Z3_ast Z3_API Z3_get_smtlib_assumption(Z3_context c, unsigned i); - - /** - \brief Return the number of declarations parsed by #Z3_parse_smtlib_string or #Z3_parse_smtlib_file. - - def_API('Z3_get_smtlib_num_decls', UINT, (_in(CONTEXT), )) - */ - unsigned Z3_API Z3_get_smtlib_num_decls(Z3_context c); - - /** - \brief Return the i-th declaration parsed by the last call to #Z3_parse_smtlib_string or #Z3_parse_smtlib_file. - - \pre i < Z3_get_smtlib_num_decls(c) - - def_API('Z3_get_smtlib_decl', FUNC_DECL, (_in(CONTEXT), _in(UINT))) - */ - Z3_func_decl Z3_API Z3_get_smtlib_decl(Z3_context c, unsigned i); - - /** - \brief Return the number of sorts parsed by #Z3_parse_smtlib_string or #Z3_parse_smtlib_file. - - def_API('Z3_get_smtlib_num_sorts', UINT, (_in(CONTEXT), )) - */ - unsigned Z3_API Z3_get_smtlib_num_sorts(Z3_context c); - - /** - \brief Return the i-th sort parsed by the last call to #Z3_parse_smtlib_string or #Z3_parse_smtlib_file. - - \pre i < Z3_get_smtlib_num_sorts(c) - - def_API('Z3_get_smtlib_sort', SORT, (_in(CONTEXT), _in(UINT))) - */ - Z3_sort Z3_API Z3_get_smtlib_sort(Z3_context c, unsigned i); /** \brief Retrieve that last error message information generated from parsing. - def_API('Z3_get_smtlib_error', STRING, (_in(CONTEXT), )) + def_API('Z3_get_parser_error', STRING, (_in(CONTEXT), )) */ - Z3_string Z3_API Z3_get_smtlib_error(Z3_context c); + Z3_string Z3_API Z3_get_parser_error(Z3_context c); /*@}*/ /** @name Error Handling */ diff --git a/src/ast/ast_smt_pp.cpp b/src/ast/ast_smt_pp.cpp index 906fd054b..bad4b1984 100644 --- a/src/ast/ast_smt_pp.cpp +++ b/src/ast/ast_smt_pp.cpp @@ -340,8 +340,7 @@ class smt_printer { } - void pp_arg(expr *arg, app *parent) - { + void pp_arg(expr *arg, app *parent) { pp_marked_expr(arg); } @@ -417,7 +416,7 @@ class smt_printer { else if (m_simplify_implies && m_manager.is_implies(decl) && m_manager.is_implies(n->get_arg(1))) { expr *curr = n; expr *arg; - m_out << "(implies (and"; + m_out << "(=> (and"; while (m_manager.is_implies(curr)) { arg = to_app(curr)->get_arg(0); @@ -476,9 +475,8 @@ class smt_printer { } } - void print_no_lets(expr *e) - { - smt_printer p(m_out, m_manager, m_qlists, m_renaming, m_logic, true, m_simplify_implies, true, m_indent, m_num_var_names, m_var_names); + void print_no_lets(expr *e) { + smt_printer p(m_out, m_manager, m_qlists, m_renaming, m_logic, true, m_simplify_implies, m_indent, m_num_var_names, m_var_names); p(e); } @@ -511,7 +509,7 @@ class smt_printer { m_out << "(! "; } { - smt_printer p(m_out, m_manager, m_qlists, m_renaming, m_logic, false, true, m_simplify_implies, m_indent, m_num_var_names, m_var_names); + smt_printer p(m_out, m_manager, m_qlists, m_renaming, m_logic, false, m_simplify_implies, m_indent, m_num_var_names, m_var_names); p(q->get_expr()); } @@ -704,7 +702,7 @@ class smt_printer { public: smt_printer(std::ostream& out, ast_manager& m, ptr_vector& ql, smt_renaming& rn, - symbol logic, bool no_lets, bool is_smt2, bool simplify_implies, unsigned indent, unsigned num_var_names = 0, char const* const* var_names = 0) : + symbol logic, bool no_lets, bool simplify_implies, unsigned indent, unsigned num_var_names = 0, char const* const* var_names = 0) : m_out(out), m_manager(m), m_qlists(ql), @@ -894,25 +892,17 @@ ast_smt_pp::ast_smt_pp(ast_manager& m): m_simplify_implies(true) {} - -void ast_smt_pp::display_expr(std::ostream& strm, expr* n) { - ptr_vector ql; - smt_renaming rn; - smt_printer p(strm, m_manager, ql, rn, m_logic, false, false, m_simplify_implies, 0); - p(n); -} - void ast_smt_pp::display_expr_smt2(std::ostream& strm, expr* n, unsigned indent, unsigned num_var_names, char const* const* var_names) { ptr_vector ql; smt_renaming rn; - smt_printer p(strm, m_manager, ql, rn, m_logic, false, true, m_simplify_implies, indent, num_var_names, var_names); + smt_printer p(strm, m_manager, ql, rn, m_logic, false, m_simplify_implies, indent, num_var_names, var_names); p(n); } void ast_smt_pp::display_ast_smt2(std::ostream& strm, ast* a, unsigned indent, unsigned num_var_names, char const* const* var_names) { ptr_vector ql; smt_renaming rn; - smt_printer p(strm, m_manager, ql, rn, m_logic, false, true, m_simplify_implies, indent, num_var_names, var_names); + smt_printer p(strm, m_manager, ql, rn, m_logic, false, m_simplify_implies, indent, num_var_names, var_names); if (is_expr(a)) { p(to_expr(a)); } @@ -1021,92 +1011,3 @@ void ast_smt_pp::display_smt2(std::ostream& strm, expr* n) { p(n); } } - -void ast_smt_pp::display(std::ostream& strm, expr* n) { - ptr_vector ql; - decl_collector decls(m_manager); - smt_renaming rn; - - for (unsigned i = 0; i < m_assumptions.size(); ++i) { - decls.visit(m_assumptions[i].get()); - } - for (unsigned i = 0; i < m_assumptions_star.size(); ++i) { - decls.visit(m_assumptions_star[i].get()); - } - decls.visit(n); - - strm << "(benchmark "; - - if (m_benchmark_name != symbol::null) { - strm << m_benchmark_name << "\n"; - } - else { - strm << "unnamed\n"; - } - if (m_source_info != symbol::null && m_source_info != symbol("")) { - strm << ":source { " << m_source_info << " }\n"; - } - strm << ":status " << m_status << "\n"; - if (m_category != symbol::null && m_category != symbol("")) { - strm << ":category { " << m_category << " }\n"; - } - if (m_logic != symbol::null && m_logic != symbol("")) { - strm << ":logic " << m_logic << "\n"; - } - - if (m_attributes.size() > 0) { - strm << m_attributes.c_str(); - } - - ast_mark sort_mark; - for (unsigned i = 0; i < decls.get_num_sorts(); ++i) { - sort* s = decls.get_sorts()[i]; - if (!(*m_is_declared)(s)) { - smt_printer p(strm, m_manager, ql, rn, m_logic, true, false, m_simplify_implies, 0); - p.pp_sort_decl(sort_mark, s); - } - } - - for (unsigned i = 0; i < decls.get_num_decls(); ++i) { - func_decl* d = decls.get_func_decls()[i]; - if (!(*m_is_declared)(d)) { - strm << ":extrafuns ("; - smt_printer p(strm, m_manager, ql, rn, m_logic, true, false, m_simplify_implies, 0); - p(d); - strm << ")\n"; - } - } - - for (unsigned i = 0; i < decls.get_num_preds(); ++i) { - func_decl* d = decls.get_pred_decls()[i]; - if (!(*m_is_declared)(d)) { - strm << ":extrapreds ("; - smt_printer p(strm, m_manager, ql, rn, m_logic, true, false, m_simplify_implies, 0); - p.visit_pred(d); - strm << ")\n"; - } - } - - for (unsigned i = 0; i < m_assumptions.size(); ++i) { - expr * e = m_assumptions[i].get(); - strm << ":assumption\n"; - smt_printer p(strm, m_manager, ql, rn, m_logic, false, false, m_simplify_implies, 0); - p(e); - strm << "\n"; - } - - for (unsigned i = 0; i < m_assumptions_star.size(); ++i) { - strm << ":assumption-core\n"; - smt_printer p(strm, m_manager, ql, rn, m_logic, false, false, m_simplify_implies, 0); - p(m_assumptions_star[i].get()); - strm << "\n"; - } - - { - strm << ":formula\n"; - smt_printer p(strm, m_manager, ql, rn, m_logic, false, false, m_simplify_implies, 0); - p(n); - strm << "\n"; - } - strm << ")\n"; -} diff --git a/src/ast/ast_smt_pp.h b/src/ast/ast_smt_pp.h index dd2a6d753..ac2e33140 100644 --- a/src/ast/ast_smt_pp.h +++ b/src/ast/ast_smt_pp.h @@ -75,9 +75,7 @@ public: void set_is_declared(is_declared* id) { m_is_declared = id; } - void display(std::ostream& strm, expr* n); void display_smt2(std::ostream& strm, expr* n); - void display_expr(std::ostream& strm, expr* n); void display_expr_smt2(std::ostream& strm, expr* n, unsigned indent = 0, unsigned num_var_names = 0, char const* const* var_names = 0); void display_ast_smt2(std::ostream& strm, ast* n, unsigned indent = 0, unsigned num_var_names = 0, char const* const* var_names = 0); diff --git a/src/ast/proofs/proof_checker.cpp b/src/ast/proofs/proof_checker.cpp index 3f9438229..6fd876efc 100644 --- a/src/ast/proofs/proof_checker.cpp +++ b/src/ast/proofs/proof_checker.cpp @@ -1284,7 +1284,7 @@ void proof_checker::dump_proof(unsigned num_antecedents, expr * const * antecede pp.add_assumption(antecedents[i]); expr_ref n(m); n = m.mk_not(consequent); - pp.display(out, n); + pp.display_smt2(out, n); out.close(); m_proof_lemma_id++; } diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index a1e7a4745..ec2eea032 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -339,6 +339,13 @@ void ast_object_ref::finalize(cmd_context & ctx) { ctx.m().dec_ref(m_ast); } +void stream_ref::set(std::ostream& out) { + reset(); + m_owner = false; + m_name = "caller-owned"; + m_stream = &out; +} + void stream_ref::set(char const * name) { if (!name) { throw cmd_exception("invalid stream name"); diff --git a/src/cmd_context/cmd_context.h b/src/cmd_context/cmd_context.h index b60f590a9..99d6c8284 100644 --- a/src/cmd_context/cmd_context.h +++ b/src/cmd_context/cmd_context.h @@ -128,6 +128,7 @@ public: stream_ref(std::string n, std::ostream & d):m_default_name(n), m_default(d), m_name(n), m_stream(&d), m_owner(false) {} ~stream_ref() { reset(); } void set(char const * name); + void set(std::ostream& strm); void reset(); std::ostream & operator*() { return *m_stream; } char const * name() const { return m_name.c_str(); } @@ -404,6 +405,7 @@ public: void reset_object_refs(); void reset_user_tactics(); void set_regular_stream(char const * name) { m_regular.set(name); } + void set_regular_stream(std::ostream& out) { m_regular.set(out); } void set_diagnostic_stream(char const * name); virtual std::ostream & regular_stream() { return *m_regular; } virtual std::ostream & diagnostic_stream() { return *m_diagnostic; } diff --git a/src/cmd_context/pdecl.cpp b/src/cmd_context/pdecl.cpp index 7eac1f347..d1185544a 100644 --- a/src/cmd_context/pdecl.cpp +++ b/src/cmd_context/pdecl.cpp @@ -852,7 +852,7 @@ pdecl_manager::pdecl_manager(ast_manager & m): pdecl_manager::~pdecl_manager() { dec_ref(m_list); reset_sort_info(); - SASSERT(m_sort2psort.empty()); + SASSERT(m_sort2psort.empty()); SASSERT(m_table.empty()); } @@ -865,6 +865,8 @@ psort * pdecl_manager::mk_psort_cnst(sort * s) { return r; } +static unsigned r_count = 0; + psort * pdecl_manager::register_psort(psort * n) { TRACE("register_psort", tout << "registering psort...\n"; n->display(tout); tout << "\n";); psort * r = m_table.insert_if_not_there(n); diff --git a/src/parsers/smt/CMakeLists.txt b/src/parsers/smt/CMakeLists.txt deleted file mode 100644 index 2edf7b679..000000000 --- a/src/parsers/smt/CMakeLists.txt +++ /dev/null @@ -1,8 +0,0 @@ -z3_add_component(smtparser - SOURCES - smtlib.cpp - smtlib_solver.cpp - smtparser.cpp - COMPONENT_DEPENDENCIES - portfolio -) diff --git a/src/parsers/smt/smtlib.cpp b/src/parsers/smt/smtlib.cpp deleted file mode 100644 index 71dd48156..000000000 --- a/src/parsers/smt/smtlib.cpp +++ /dev/null @@ -1,258 +0,0 @@ - -/*++ -Copyright (c) 2015 Microsoft Corporation - ---*/ - - -#include "parsers/smt/smtlib.h" -#include "ast/ast_pp.h" -#include "ast/ast_smt2_pp.h" - -#ifdef _WINDOWS -#ifdef ARRAYSIZE -#undef ARRAYSIZE -#endif -#include -#include -#endif - -#include - - -using namespace smtlib; - -// -------------------------------------------------------------------------- -// symtable - -symtable::~symtable() { - reset(); -} - -void symtable::reset() { - svector*> range; - m_ids.get_range(range); - for (unsigned i = 0; i < range.size(); ++i) { - ptr_vector const & v = *range[i]; - for (unsigned j = 0; j < v.size(); ++j) { - m_manager.dec_ref(v[j]); - } - dealloc(range[i]); - } - m_ids.reset(); - ptr_vector sorts; - m_sorts1.get_range(sorts); - for (unsigned i = 0; i < sorts.size(); ++i) { - m_manager.dec_ref(sorts[i]); - } - m_sorts1.reset(); - ptr_vector sort_builders; - m_sorts.get_range(sort_builders); - for (unsigned i = 0; i < sort_builders.size(); ++i) { - dealloc(sort_builders[i]); - } - m_sorts.reset(); -} - - -void symtable::insert(symbol s, func_decl * d) { - ptr_vector* decls = 0; - m_manager.inc_ref(d); - if (!m_ids.find(s, decls)) { - SASSERT(!decls); - decls = alloc(ptr_vector); - decls->push_back(d); - m_ids.insert(s, decls); - } - else { - SASSERT(decls); - if ((*decls)[0] != d) { - decls->push_back(d); - } - else { - m_manager.dec_ref(d); - } - } -} - -bool symtable::find1(symbol s, func_decl*& d) { - ptr_vector* decls = 0; - - if (!m_ids.find(s, decls)) { - SASSERT(!decls); - return false; - } - SASSERT(decls && !decls->empty()); - d = (*decls)[0]; - return true; -} - -bool symtable::find_overload(symbol s, ptr_vector const & dom, func_decl * & d) { - ptr_vector* decls = 0; - d = 0; - if (!m_ids.find(s, decls)) { - SASSERT(!decls); - return false; - } - SASSERT(decls); - for (unsigned i = 0; i < decls->size(); ++i) { - func_decl* decl = (*decls)[i]; - if (decl->is_associative() && decl->get_arity() > 0) { - for (unsigned j = 0; j < dom.size(); ++j) { - if (dom[j] != decl->get_domain(0)) { - goto try_next; - } - } - d = decl; - return true; - } - - if (decl->get_arity() != dom.size()) { - goto try_next; - } - for (unsigned j = 0; j < decl->get_arity(); ++j) { - if (decl->get_domain(j) != dom[j]) { - goto try_next; - } - } - d = decl; - return true; - - try_next: - if (decl->get_family_id() == m_manager.get_basic_family_id() && decl->get_decl_kind() == OP_DISTINCT) { - // we skip type checking for 'distinct' - d = decl; - return true; - } - } - return false; -} - -// Store in result the func_decl that are not attached to any family id. -// That is, the uninterpreted constants and function declarations. -void symtable::get_func_decls(ptr_vector & result) const { - svector*> tmp; - m_ids.get_range(tmp); - svector*>::const_iterator it = tmp.begin(); - svector*>::const_iterator end = tmp.end(); - for (; it != end; ++it) { - ptr_vector * curr = *it; - if (curr) { - ptr_vector::const_iterator it2 = curr->begin(); - ptr_vector::const_iterator end2 = curr->end(); - for (; it2 != end2; ++it2) { - func_decl * d = *it2; - if (d && d->get_family_id() == null_family_id) { - result.push_back(d); - } - } - } - } -} - -void symtable::insert(symbol s, sort_builder* sb) { - m_sorts.insert(s, sb); -} - -bool symtable::lookup(symbol s, sort_builder*& sb) { - return m_sorts.find(s, sb); -} - -void symtable::push_sort(symbol name, sort* srt) { - m_sorts.begin_scope(); - sort_builder* sb = alloc(basic_sort_builder,srt); - m_sorts.insert(name, sb); - m_sorts_trail.push_back(sb); -} - -void symtable::pop_sorts(unsigned num_sorts) { - while (num_sorts > 0) { - dealloc(m_sorts_trail.back()); - m_sorts_trail.pop_back(); - m_sorts.end_scope(); - } -} - -void symtable::get_sorts(ptr_vector& result) const { - vector tmp; - m_sorts1.get_range(tmp); - for (unsigned i = 0; i < tmp.size(); ++i) { - if (tmp[i]->get_family_id() == null_family_id) { - result.push_back(tmp[i]); - } - } -} - - -// -------------------------------------------------------------------------- -// theory - -func_decl * theory::declare_func(symbol const & id, sort_ref_buffer & domain, sort * range, - bool is_assoc, bool is_comm, bool is_inj) { - func_decl * decl = m_ast_manager.mk_func_decl(id, domain.size(), domain.c_ptr(), range, - is_assoc, is_comm, is_inj); - - m_symtable.insert(id, decl); - m_asts.push_back(decl); - return decl; -} - - -sort * theory::declare_sort(symbol const & id) { - sort * decl = m_ast_manager.mk_uninterpreted_sort(id); - m_symtable.insert(id, decl); - m_asts.push_back(decl); - return decl; -} - - -bool theory::get_func_decl(symbol id, func_decl * & decl) { - return m_symtable.find1(id, decl); -} - -bool theory::get_sort(symbol id, sort* & s) { - return m_symtable.find(id, s); -} - -bool theory::get_const(symbol id, expr * & term) { - func_decl* decl = 0; - if (!get_func_decl(id,decl)) { - return false; - } - if (decl->get_arity() != 0) { - return false; - } - term = m_ast_manager.mk_const(decl); - m_asts.push_back(term); - return true; -} - -void benchmark::display_as_smt2(std::ostream & out) const { - if (m_logic != symbol::null) - out << "(set-logic " << m_logic << ")\n"; - out << "(set-info :smt-lib-version 2.0)\n"; - out << "(set-info :status "; - switch (m_status) { - case SAT: out << "sat"; break; - case UNSAT: out << "unsat"; break; - default: out << "unknown"; break; - } - out << ")\n"; -#if 0 - ast_manager & m = m_ast_manager; - ptr_vector decls; - m_symtable.get_func_decls(decls); - ptr_vector::const_iterator it = decls.begin(); - ptr_vector::const_iterator end = decls.end(); - for (; it != end; ++it) { - func_decl * f = *it; - out << "(declare-fun " << f->get_name() << " ("; - for (unsigned i = 0; i < f->get_arity(); i++) { - if (i > 0) out << " "; - out << mk_ismt2_pp(f->get_domain(i), m); - } - out << ") " << mk_ismt2_pp(f->get_range(), m); - out << ")\n"; - } -#endif -} diff --git a/src/parsers/smt/smtlib.h b/src/parsers/smt/smtlib.h deleted file mode 100644 index f037e3d74..000000000 --- a/src/parsers/smt/smtlib.h +++ /dev/null @@ -1,232 +0,0 @@ -/*++ -Copyright (c) 2006 Microsoft Corporation - -Module Name: - - smtlib.h - -Abstract: - - SMT library utilities - -Author: - - Nikolaj Bjorner (nbjorner) 2006-09-29 - -Revision History: - ---*/ -#ifndef SMTLIB_H_ -#define SMTLIB_H_ - -#include "ast/ast.h" -#include "util/symbol_table.h" -#include "util/map.h" -#include "ast/arith_decl_plugin.h" - -namespace smtlib { - - class sort_builder { - public: - virtual ~sort_builder() {} - virtual bool apply(unsigned num_params, parameter const* params, sort_ref& result) = 0; - virtual char const* error_message() { return ""; } - }; - - class basic_sort_builder : public sort_builder { - sort* m_sort; - public: - basic_sort_builder(sort* s) : m_sort(s) {} - - virtual bool apply(unsigned np, parameter const*, sort_ref& result) { - result = m_sort; - return m_sort && np != 0; - } - }; - - - class symtable { - ast_manager& m_manager; - symbol_table m_sorts1; - symbol_table m_sorts; - ptr_vector m_sorts_trail; - symbol_table* > m_ids; - - public: - - symtable(ast_manager& m): m_manager(m) {} - - ~symtable(); - - void reset(); - - void insert(symbol s, func_decl * d); - - bool find(symbol s, ptr_vector * & decls) { - return m_ids.find(s, decls); - } - - bool find1(symbol s, func_decl * & d); - - bool find_overload(symbol s, ptr_vector const & dom, func_decl * & d); - - void insert(symbol s, sort * d) { - sort * d2; - if (m_sorts1.find(s, d2)) { - m_manager.dec_ref(d2); - } - m_manager.inc_ref(d); - m_sorts1.insert(s, d); - } - - bool find(symbol s, sort * & d) { - return m_sorts1.find(s, d); - } - - void insert(symbol s, sort_builder* sb); - - bool lookup(symbol s, sort_builder*& sb); - - void push_sort(symbol s, sort*); - - void pop_sorts(unsigned num_sorts); - - void get_func_decls(ptr_vector & result) const; - - void get_sorts(ptr_vector& result) const; - }; - - class theory { - public: - typedef ptr_vector::const_iterator expr_iterator; - - theory(ast_manager & ast_manager, symbol const& name): - m_name(name), - m_ast_manager(ast_manager), - m_symtable(ast_manager), - m_asts(ast_manager) - {} - - virtual ~theory() {} - - symtable * get_symtable() { return &m_symtable; } - - void insert(sort * s) { m_symtable.insert(s->get_name(), s); } - - void insert(func_decl * c) { m_symtable.insert(c->get_name(), c); } - - func_decl * declare_func(symbol const & id, sort_ref_buffer & domain, sort * range, - bool is_assoc, bool is_comm, bool is_inj); - - sort * declare_sort(symbol const & id); - - void add_axiom(expr * axiom) { - m_asts.push_back(axiom); - m_axioms.push_back(axiom); - } - - expr_iterator begin_axioms() const { - return m_axioms.begin(); - } - - unsigned get_num_axioms() const { - return m_axioms.size(); - } - - expr * const * get_axioms() const { - return m_axioms.c_ptr(); - } - - expr_iterator end_axioms() const { - return m_axioms.end(); - } - - void add_assumption(expr * axiom) { - m_asts.push_back(axiom); - m_assumptions.push_back(axiom); - } - - unsigned get_num_assumptions() const { - return m_assumptions.size(); - } - - expr * const * get_assumptions() const { - return m_assumptions.c_ptr(); - } - - bool get_func_decl(symbol, func_decl*&); - - bool get_sort(symbol, sort*&); - - bool get_const(symbol, expr*&); - - void set_name(symbol const& name) { m_name = name; } - - symbol const get_name() const { return m_name; } - protected: - symbol m_name; - ast_manager& m_ast_manager; - ptr_vector m_axioms; - ptr_vector m_assumptions; - symtable m_symtable; - ast_ref_vector m_asts; - - private: - theory& operator=(theory const&); - - theory(theory const&); - }; - - class benchmark : public theory { - public: - enum status { - UNKNOWN, - SAT, - UNSAT - }; - - benchmark(ast_manager & ast_manager, symbol const & name) : - theory(ast_manager, name), - m_status(UNKNOWN) {} - - virtual ~benchmark() {} - - status get_status() const { return m_status; } - void set_status(status status) { m_status = status; } - - symbol get_logic() const { - if (m_logic == symbol::null) { - return symbol("ALL"); - } - return m_logic; - } - - void set_logic(symbol const & s) { m_logic = s; } - - unsigned get_num_formulas() const { - return m_formulas.size(); - } - - expr_iterator begin_formulas() const { - return m_formulas.begin(); - } - - expr_iterator end_formulas() const { - return m_formulas.end(); - } - - void add_formula(expr * formula) { - m_asts.push_back(formula); - m_formulas.push_back(formula); - } - - void display_as_smt2(std::ostream & out) const; - - private: - status m_status; - symbol m_logic; - ptr_vector m_formulas; - }; -}; - -#endif diff --git a/src/parsers/smt/smtlib_solver.cpp b/src/parsers/smt/smtlib_solver.cpp deleted file mode 100644 index 339be2ddd..000000000 --- a/src/parsers/smt/smtlib_solver.cpp +++ /dev/null @@ -1,119 +0,0 @@ -/*++ -Copyright (c) 2006 Microsoft Corporation - -Module Name: - - smtlib_solver.cpp - -Abstract: - - SMT based solver. - -Author: - - Nikolaj Bjorner (nbjorner) 2006-11-3. - -Revision History: - ---*/ - -#include "parsers/smt/smtparser.h" -#include "parsers/smt/smtlib_solver.h" -#include "util/warning.h" -#include "ast/ast_pp.h" -#include "ast/ast_ll_pp.h" -#include "ast/well_sorted.h" -#include "model/model.h" -#include "model/model_v2_pp.h" -#include "solver/solver.h" -#include "tactic/portfolio/smt_strategic_solver.h" -#include "cmd_context/cmd_context.h" -#include "model/model_params.hpp" -#include "parsers/util/parser_params.hpp" - -namespace smtlib { - - solver::solver(): - m_ast_manager(m_params.m_proof ? PGM_ENABLED : PGM_DISABLED, - m_params.m_trace ? m_params.m_trace_file_name.c_str() : 0), - m_ctx(0), - m_error_code(0) { - parser_params ps; - m_parser = parser::create(m_ast_manager, ps.ignore_user_patterns()); - m_parser->initialize_smtlib(); - } - - solver::~solver() { - if (m_ctx) - dealloc(m_ctx); - } - - bool solver::solve_smt(char const * benchmark_file) { - IF_VERBOSE(100, verbose_stream() << "parsing...\n";); - if (!m_parser->parse_file(benchmark_file)) { - if (benchmark_file) { - warning_msg("could not parse file '%s'.", benchmark_file); - } - else { - warning_msg("could not parse input stream."); - } - m_error_code = ERR_PARSER; - return false; - } - benchmark * benchmark = m_parser->get_benchmark(); - solve_benchmark(*benchmark); - return true; - } - - bool solver::solve_smt_string(char const * benchmark_string) { - if (!m_parser->parse_string(benchmark_string)) { - warning_msg("could not parse string '%s'.", benchmark_string); - return false; - } - benchmark * benchmark = m_parser->get_benchmark(); - solve_benchmark(*benchmark); - return true; - } - - void solver::display_statistics() { - if (m_ctx) - m_ctx->display_statistics(); - } - - void solver::solve_benchmark(benchmark & benchmark) { - if (benchmark.get_num_formulas() == 0) { - // Hack: it seems SMT-LIB allow benchmarks without any :formula - benchmark.add_formula(m_ast_manager.mk_true()); - } - m_ctx = alloc(cmd_context, true, &m_ast_manager, benchmark.get_logic()); - m_ctx->set_solver_factory(mk_smt_strategic_solver_factory()); - theory::expr_iterator fit = benchmark.begin_formulas(); - theory::expr_iterator fend = benchmark.end_formulas(); - for (; fit != fend; ++fit) - solve_formula(benchmark, *fit); - } - - void solver::solve_formula(benchmark const & benchmark, expr * f) { - IF_VERBOSE(100, verbose_stream() << "starting...\n";); - m_ctx->reset(); - for (unsigned i = 0; i < benchmark.get_num_axioms(); i++) - m_ctx->assert_expr(benchmark.get_axioms()[i]); - m_ctx->assert_expr(f); - m_ctx->check_sat(benchmark.get_num_assumptions(), benchmark.get_assumptions()); - check_sat_result * r = m_ctx->get_check_sat_result(); - if (r != 0) { - proof * pr = r->get_proof(); - if (pr != 0 && m_params.m_proof) - std::cout << mk_ll_pp(pr, m_ast_manager, false, false); - model_ref md; - if (r->status() != l_false) r->get_model(md); - if (md.get() != 0 && m_params.m_model) { - model_params p; - model_v2_pp(std::cout, *(md.get()), p.partial()); - } - } - else { - m_error_code = ERR_UNKNOWN_RESULT; - } - } -}; diff --git a/src/parsers/smt/smtlib_solver.h b/src/parsers/smt/smtlib_solver.h deleted file mode 100644 index 6288c360b..000000000 --- a/src/parsers/smt/smtlib_solver.h +++ /dev/null @@ -1,48 +0,0 @@ -/*++ -Copyright (c) 2006 Microsoft Corporation - -Module Name: - - smtlib_solver.h - -Abstract: - - SMT based solver. - -Author: - - Nikolaj Bjorner (nbjorner) 2006-11-3. - -Revision History: - ---*/ -#ifndef SMTLIB_SOLVER_H_ -#define SMTLIB_SOLVER_H_ - -#include "parsers/smt/smtparser.h" -#include "cmd_context/context_params.h" -#include "util/lbool.h" - -class cmd_context; - -namespace smtlib { - class solver { - context_params m_params; - ast_manager m_ast_manager; - cmd_context * m_ctx; - scoped_ptr m_parser; - unsigned m_error_code; - public: - solver(); - ~solver(); - bool solve_smt(char const * benchmark_file); - bool solve_smt_string(char const * benchmark_string); - void display_statistics(); - unsigned get_error_code() const { return m_error_code; } - private: - void solve_benchmark(benchmark & benchmark); - void solve_formula(benchmark const & benchmark, expr * f); - }; -}; - -#endif diff --git a/src/parsers/smt/smtparser.cpp b/src/parsers/smt/smtparser.cpp deleted file mode 100644 index 15f094e33..000000000 --- a/src/parsers/smt/smtparser.cpp +++ /dev/null @@ -1,2760 +0,0 @@ -/*++ -Copyright (c) 2006 Microsoft Corporation - -Module Name: - - smtparser.cpp - -Abstract: - - SMT parser into ast. - -Author: - - Nikolaj Bjorner (nbjorner) 2006-10-4. - Leonardo de Moura (leonardo) - -Revision History: ---*/ -#include -#include -#include -#include -#include -#include "util/region.h" -#include "parsers/util/scanner.h" -#include "util/symbol.h" -#include "util/vector.h" -#include "util/symbol_table.h" -#include "parsers/smt/smtlib.h" -#include "parsers/smt/smtparser.h" -#include "ast/ast_pp.h" -#include "ast/bv_decl_plugin.h" -#include "ast/array_decl_plugin.h" -#include "util/warning.h" -#include "util/error_codes.h" -#include "parsers/util/pattern_validation.h" -#include "ast/rewriter/var_subst.h" -#include "ast/well_sorted.h" -#include "util/str_hashtable.h" -#include "util/stopwatch.h" - -class id_param_info { - symbol m_string; - unsigned m_num_params; - parameter m_params[0]; -public: - id_param_info(symbol const& s, unsigned n, parameter const* p) : m_string(s), m_num_params(n) { - for (unsigned i = 0; i < n; ++i) { - new (&(m_params[i])) parameter(); - m_params[i] = p[i]; - } - } - symbol string() const { return m_string; } - parameter * params() { return m_params; } - unsigned num_params() const { return m_num_params; } -}; - -class proto_region { - ptr_vector m_rationals; - ptr_vector m_id_infos; - region m_region; -public: - proto_region() { } - - ~proto_region() { reset(); } - - rational* allocate(rational const & n) { - rational* r = alloc(rational, n); - m_rationals.push_back(r); - return r; - } - - id_param_info* allocate(vector const& params, symbol const & s) { - unsigned size = sizeof(id_param_info) + sizeof(parameter)*(params.size()); - id_param_info* r = static_cast(m_region.allocate(size)); - new (r) id_param_info(s, params.size(), params.c_ptr()); - m_id_infos.push_back(r); - return r; - } - - void* allocate(size_t s) { return m_region.allocate(s); } - - void reset() { - for (unsigned i = 0; i < m_rationals.size(); ++i) { - dealloc(m_rationals[i]); - } - for (unsigned i = 0; i < m_id_infos.size(); ++i) { - unsigned n = m_id_infos[i]->num_params(); - for (unsigned j = 0; j < n; ++j) { - m_id_infos[i]->params()[j].~parameter(); - } - } - m_rationals.reset(); - m_id_infos.reset(); - m_region.reset(); - } - -private: - -}; - -inline void * operator new(size_t s, proto_region& r) { return r.allocate(s); } -inline void * operator new[](size_t s, proto_region & r) { return r.allocate(s); } -inline void operator delete(void*, proto_region& r) {} -inline void operator delete[](void *, proto_region& r) {} - -class proto_expr { -public: - - enum kind_t { - ID, - STRING, - COMMENT, - ANNOTATION, - INT, - FLOAT, - CONS - }; -private: - - int m_kind:8; - int m_line:24; - int m_pos; - union { - id_param_info* m_id_info; - rational* m_number; - proto_expr** m_children; - }; - -public: - - symbol string() { - if (m_kind == INT || m_kind == FLOAT) { - std::string s = m_number->to_string(); - return symbol(s.c_str()); - } - if (m_kind == CONS) { - return symbol(""); - } - SASSERT(m_kind == STRING || m_kind == COMMENT || m_kind == ID || m_kind == ANNOTATION); - return m_id_info->string(); - } - - rational const& number() { - SASSERT(m_kind == INT || m_kind == FLOAT); - return *m_number; - } - - proto_expr* const* children() const { - if (m_kind == CONS) { - return m_children; - } - else { - return 0; - } - } - - int line() { return m_line; } - int pos() { return m_pos; } - kind_t kind() { return static_cast(m_kind); } - - unsigned num_params() const { - SASSERT(m_kind == ID); - return m_id_info->num_params(); - } - - parameter * params() { - SASSERT(m_kind == ID); - return m_id_info->params(); - } - - proto_expr(proto_region & region, kind_t kind, symbol const & s, vector const & params, int line, int pos): - m_kind(kind), - m_line(line), - m_pos(pos), - m_id_info(region.allocate(params, s)) { - SASSERT(kind != CONS); - SASSERT(kind != INT); - SASSERT(kind != FLOAT); - } - - proto_expr(proto_region& region, bool is_int, rational const & n, int line, int pos): - m_kind(is_int?INT:FLOAT), - m_line(line), - m_pos(pos), - m_number(region.allocate(n)) - {} - - proto_expr(proto_region& region, ptr_vector& proto_exprs, int line, int pos): - m_kind(CONS), - m_line(line), - m_pos(pos) { - // - // null terminated list of proto_expression pointers. - // - unsigned num_children = proto_exprs.size(); - m_children = new (region) proto_expr*[num_children+1]; - for (unsigned i = 0; i < num_children; ++i) { - m_children[i] = proto_exprs[i]; - } - m_children[num_children] = 0; - } - - ~proto_expr() {} - - - static proto_expr* copy(proto_region& r, proto_expr* e) { - switch(e->kind()) { - case proto_expr::CONS: { - ptr_vector args; - proto_expr* const* children = e->children(); - while (children && *children) { - args.push_back(copy(r, *children)); - ++children; - } - return new (r) proto_expr(r, args, e->line(), e->pos()); - } - case proto_expr::INT: { - return new (r) proto_expr(r, true, e->number(), e->line(), e->pos()); - } - case proto_expr::FLOAT: { - return new (r) proto_expr(r, false, e->number(), e->line(), e->pos()); - } - case proto_expr::ID: { - vector params; - for (unsigned i = 0; i < e->num_params(); ++i) { - params.push_back(e->params()[i]); - } - return new (r) proto_expr(r, e->kind(), e->string(), params, e->line(), e->pos()); - } - default: { - vector params; - return new (r) proto_expr(r, e->kind(), e->string(), params, e->line(), e->pos()); - } - } - } - -private: - - proto_expr(proto_expr const & other); - proto_expr& operator=(proto_expr const & other); -}; - - -// -// build up proto_expr tree from token stream. -// - -class proto_expr_parser { - proto_region& m_region; - scanner& m_scanner; - std::ostream& m_err; - bool m_at_eof; -public: - proto_expr_parser(proto_region& region, scanner& scanner, std::ostream& err): - m_region(region), - m_scanner(scanner), - m_err(err), - m_at_eof(false) { - } - - ~proto_expr_parser() {} - - bool parse(ptr_vector & proto_exprs, bool parse_single_expr = false) { - scanner::token token; - vector stack; - proto_expr* result = 0; - - stack.push_back(frame(PROTO_EXPRS_PRE)); - - token = m_scanner.scan(); - - if (token == scanner::EOF_TOKEN) { - proto_exprs.reset(); - return true; - } - - while (!stack.empty()) { - - if (token == scanner::EOF_TOKEN) { - break; - } - - if (token == scanner::ERROR_TOKEN) { - print_error("unexpected token"); - goto done; - } - - switch(stack.back().m_state) { - - case PROTO_EXPR: - switch (token) { - case scanner::LEFT_PAREN: - stack.back().m_state = PROTO_EXPRS_PRE; - token = m_scanner.scan(); - break; - default: - stack.back().m_state = ATOM; - break; - } - break; - - case ATOM: - SASSERT(!result); - switch(token) { - case scanner::ID_TOKEN: - result = new (m_region) proto_expr(m_region, proto_expr::ID, m_scanner.get_id(), m_scanner.get_params(), - m_scanner.get_line(), m_scanner.get_pos()); - break; - case scanner::INT_TOKEN: - result = new (m_region) proto_expr(m_region, true, m_scanner.get_number(), m_scanner.get_line(), - m_scanner.get_pos()); - break; - case scanner::FLOAT_TOKEN: - result = new (m_region) proto_expr(m_region, false, m_scanner.get_number(), m_scanner.get_line(), - m_scanner.get_pos()); - break; - case scanner::STRING_TOKEN: - result = new (m_region) proto_expr(m_region, proto_expr::STRING, m_scanner.get_id(), m_scanner.get_params(), - m_scanner.get_line(), m_scanner.get_pos()); - break; - case scanner::COMMENT_TOKEN: - result = new (m_region) proto_expr(m_region, proto_expr::COMMENT, m_scanner.get_id(), m_scanner.get_params(), - m_scanner.get_line(), m_scanner.get_pos()); - break; - case scanner::COLON: - token = m_scanner.scan(); - if (token == scanner::ID_TOKEN) { - result = new (m_region) proto_expr(m_region, proto_expr::ANNOTATION, m_scanner.get_id(), - m_scanner.get_params(), m_scanner.get_line(), m_scanner.get_pos()); - } - else { - print_error("unexpected identifier ':'"); - token = scanner::ERROR_TOKEN; - goto done; - } - break; - default: - print_error("unexpected token"); - token = scanner::ERROR_TOKEN; - goto done; - } - stack.pop_back(); - SASSERT(!stack.empty()); - stack.back().m_proto_exprs.push_back(result); - result = 0; - if (parse_single_expr && stack.size() == 1) { - goto done; - } - token = m_scanner.scan(); - break; - - case PROTO_EXPRS_PRE: - SASSERT(!result); - switch(token) { - case scanner::RIGHT_PAREN: - result = new (m_region) proto_expr(m_region, stack.back().m_proto_exprs, m_scanner.get_line(), - m_scanner.get_pos()); - stack.pop_back(); - - if (stack.empty()) { - print_error("unexpected right parenthesis"); - token = scanner::ERROR_TOKEN; - result = 0; - goto done; - } - stack.back().m_proto_exprs.push_back(result); - if (parse_single_expr && stack.size() == 1) { - goto done; - } - result = 0; - token = m_scanner.scan(); - break; - - case scanner::EOF_TOKEN: - m_at_eof = true; - break; - - case scanner::ERROR_TOKEN: - print_error("could not parse expression"); - goto done; - - default: - stack.back().m_state = PROTO_EXPRS_POST; - stack.push_back(frame(PROTO_EXPR)); - break; - } - break; - - case PROTO_EXPRS_POST: - stack.back().m_state = PROTO_EXPRS_PRE; - break; - } - } - - done: - - if (stack.size() == 1) { - for (unsigned i = 0; i < stack.back().m_proto_exprs.size(); ++i) { - proto_exprs.push_back(stack.back().m_proto_exprs[i]); - } - return true; - } - - if (stack.size() == 2) { - proto_exprs.push_back(new (m_region) proto_expr(m_region, stack.back().m_proto_exprs, m_scanner.get_line(), - m_scanner.get_pos())); - return true; - } - - print_error("unexpected nesting of parenthesis: ", stack.size()); - return false; - } - - int get_line() { - return m_scanner.get_line(); - } - - bool at_eof() const { - return m_at_eof; - } - -private: - - template - void print_error(char const* msg1, T msg2) { - m_err << "ERROR: line " << m_scanner.get_line() - << " column " << m_scanner.get_pos() << ": " - << msg1 << msg2 << "\n"; - } - - void print_error(char const* msg) { - print_error(msg, ""); - } - - // stack frame: - enum frame_state { - PROTO_EXPR, - PROTO_EXPRS_PRE, - PROTO_EXPRS_POST, - ATOM - }; - - class frame { - public: - frame_state m_state; - ptr_vector m_proto_exprs; - frame(frame_state state): - m_state(state){ - } - frame(frame const & other): - m_state(other.m_state), - m_proto_exprs(other.m_proto_exprs) { - } - private: - frame& operator=(frame const &); - }; - -}; - -using namespace smtlib; - -class idbuilder { -public: - virtual ~idbuilder() {} - virtual bool apply(expr_ref_vector const & args, expr_ref & result) = 0; -}; - -class builtin_sort_builder : public sort_builder { - ast_manager& m_manager; - family_id m_fid; - decl_kind m_kind; -public: - builtin_sort_builder(ast_manager& m, family_id fid, decl_kind k) : - m_manager(m), m_fid(fid), m_kind(k) {} - - virtual bool apply(unsigned num_params, parameter const* params, sort_ref & result) { - result = m_manager.mk_sort(m_fid, m_kind, num_params, params); - return result.get() != 0; - } -}; - -class array_sort : public builtin_sort_builder { -public: - array_sort(ast_manager& m) : - builtin_sort_builder(m, m.mk_family_id("array"), ARRAY_SORT) {} -}; - -class bv_sort : public builtin_sort_builder { -public: - bv_sort(ast_manager& m) : - builtin_sort_builder(m, m.mk_family_id("bv"), BV_SORT) {} -}; - -class user_sort : public sort_builder { - user_sort_plugin * m_plugin; - decl_kind m_kind; - symbol m_name; - unsigned m_num_args; - std::string m_error_message; -public: - user_sort(ast_manager& m, unsigned num_args, symbol name): - m_name(name), - m_num_args(num_args) { - m_plugin = m.get_user_sort_plugin(); - m_kind = m_plugin->register_name(name); - } - - ~user_sort() {} - - virtual bool apply(unsigned num_params, parameter const* params, sort_ref & result) { - if (num_params != m_num_args) { - std::ostringstream strm; - strm << "wrong number of arguments passed to " << m_name << " " - << m_num_args << " expected, but " << num_params << " given"; - m_error_message = strm.str(); - return false; - } - result = m_plugin->mk_sort(m_kind, num_params, params); - return true; - } - - virtual char const* error_message() { - return m_error_message.c_str(); - } -}; - -class smtparser : public parser { - 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) {} - }; - - class add_plugins { - - public: - add_plugins(ast_manager& m) { -#define REGISTER_PLUGIN(NAME, MK) { \ - family_id fid = m.mk_family_id(symbol(NAME)); \ - if (!m.has_plugin(fid)) { \ - m.register_plugin(fid, MK); \ - } \ - } ((void) 0) - - REGISTER_PLUGIN("arith", alloc(arith_decl_plugin)); - REGISTER_PLUGIN("bv", alloc(bv_decl_plugin)); - REGISTER_PLUGIN("array", alloc(array_decl_plugin)); - - }; - }; - - ast_manager& m_manager; - add_plugins m_plugins; - arith_util m_anum_util; - bv_util m_bvnum_util; - pattern_validator m_pattern_validator; - bool m_ignore_user_patterns; - unsigned m_binding_level; // scope level for bound vars - benchmark m_benchmark; // currently parsed benchmark - - typedef map op_map; - op_map m_builtin_ops; - op_map m_builtin_sorts; - - symbol m_let; // commonly used symbols. - symbol m_flet; - symbol m_forall; - symbol m_exists; - symbol m_lblneg; - symbol m_lblpos; - symbol m_associative; - symbol m_commutative; - symbol m_injective; - symbol m_sorts; - symbol m_funs; - symbol m_preds; - symbol m_axioms; - symbol m_notes; - symbol m_array; - symbol m_bang; - symbol m_underscore; - sort* m_int_sort; - sort* m_real_sort; - family_id m_bv_fid; - family_id m_arith_fid; - family_id m_array_fid; - family_id m_rel_fid; - func_decl * m_sk_hack; - std::ostream* m_err; - bool m_display_error_for_vs; - - -public: - - smtparser(ast_manager& m, bool ignore_user_patterns): - m_manager(m), - m_plugins(m), - m_anum_util(m), - m_bvnum_util(m), - m_pattern_validator(m), - m_ignore_user_patterns(ignore_user_patterns), - m_binding_level(0), - m_benchmark(m_manager, symbol("")), - m_let("let"), - m_flet("flet"), - m_forall("forall"), - m_exists("exists"), - m_lblneg("lblneg"), - m_lblpos("lblpos"), - m_associative("assoc"), - m_commutative("comm"), - m_injective("injective"), - m_sorts("sorts"), - m_funs("funs"), - m_preds("preds"), - m_axioms("axioms"), - m_notes("notes"), - m_array("array"), - m_bang("!"), - m_underscore("_"), - m_err(0), - m_display_error_for_vs(false) - { - family_id bfid = m_manager.get_basic_family_id(); - - add_builtin_type("bool", bfid, BOOL_SORT); - m_benchmark.get_symtable()->insert(symbol("Array"), alloc(array_sort, m)); - m_benchmark.get_symtable()->insert(symbol("BitVec"), alloc(bv_sort, m)); - - - add_builtins(bfid); - } - - ~smtparser() { - } - - void set_error_stream(std::ostream& strm) { m_err = &strm; } - - std::ostream& get_err() { return m_err?(*m_err):std::cerr; } - - bool ignore_user_patterns() const { return m_ignore_user_patterns; } - - bool parse_stream(std::istream& stream) { - proto_region region; - scanner scanner(stream, get_err(), false); - proto_expr_parser parser(region, scanner, get_err()); - return parse(parser); - } - - bool parse_file(char const * filename) { - if (filename != 0) { - std::ifstream stream(filename); - if (!stream) { - get_err() << "ERROR: could not open file '" << filename << "'.\n"; - return false; - } - return parse_stream(stream); - } - else { - return parse_stream(std::cin); - } - } - - bool parse_string(char const * str) { - std::string s = str; - std::istringstream is(s); - return parse_stream(is); - } - - void add_builtin_op(char const * s, family_id fid, decl_kind k) { - m_builtin_ops.insert(symbol(s), builtin_op(fid, k)); - } - - void add_builtin_type(char const * s, family_id fid, decl_kind k) { - m_builtin_sorts.insert(symbol(s), builtin_op(fid, k)); - } - - void initialize_smtlib() { - smtlib::symtable* table = m_benchmark.get_symtable(); - - symbol arith("arith"); - family_id afid = m_manager.mk_family_id(arith); - m_arith_fid = afid; - - add_builtin_type("Int", afid, INT_SORT); - add_builtin_type("Real", afid, REAL_SORT); - add_builtin_type("Bool", m_manager.get_basic_family_id(), BOOL_SORT); - - m_int_sort = m_manager.mk_sort(m_arith_fid, INT_SORT); - m_real_sort = m_manager.mk_sort(m_arith_fid, REAL_SORT); - - add_builtins(afid); - - symbol bv("bv"); - family_id bfid = m_manager.mk_family_id(bv); - m_bv_fid = bfid; - - add_builtins(bfid); - - add_builtin_type("BitVec", bfid, BV_SORT); - - symbol array("array"); - afid = m_manager.mk_family_id(array); - m_array_fid = afid; - - add_builtins(afid); - - sort* a1, *a2; - func_decl* store1, *sel1, *store2, *sel2; - - // Array - parameter params0[2] = { parameter(m_int_sort), parameter(m_int_sort) }; - a1 = m_manager.mk_sort(afid, ARRAY_SORT, 2, params0); - table->insert(symbol("Array"), a1); - parameter param0(a1); - sort * args0[3] = { a1, m_int_sort, m_int_sort }; - store1 = m_manager.mk_func_decl(afid, OP_STORE, 0, 0, 3, args0); - table->insert(symbol("store"), store1); - sel1 = m_manager.mk_func_decl(afid, OP_SELECT, 0, 0, 2, args0); - table->insert(symbol("select"), sel1); - - // Array1 - parameter params1[2] = { parameter(m_int_sort), parameter(m_real_sort) }; - a1 = m_manager.mk_sort(afid, ARRAY_SORT, 2, params1); - table->insert(symbol("Array1"), a1); - parameter param1(a1); - sort * args1[3] = { a1, m_int_sort, m_real_sort }; - store1 = m_manager.mk_func_decl(afid, OP_STORE, 0, 0, 3, args1); - table->insert(symbol("store"), store1); - sel1 = m_manager.mk_func_decl(afid, OP_SELECT, 0, 0, 2, args1); - table->insert(symbol("select"), sel1); - - // Array2 - parameter params2[2] = { parameter(m_int_sort), parameter(a1) }; - a2 = m_manager.mk_sort(afid, ARRAY_SORT, 2, params2); - table->insert(symbol("Array2"), a2); - parameter param2(a2); - sort * args2[3] = { a2, m_int_sort, a1 }; - store2 = m_manager.mk_func_decl(afid, OP_STORE, 0, 0, 3, args2); - table->insert(symbol("store"), store2); - sel2 = m_manager.mk_func_decl(afid, OP_SELECT, 0, 0, 2, args2); - table->insert(symbol("select"), sel2); - - m_benchmark.declare_sort(symbol("U")); - - sort * bool_sort = m_manager.mk_bool_sort(); - m_sk_hack = m_manager.mk_func_decl(symbol("sk_hack"), 1, &bool_sort, bool_sort); - table->insert(symbol("sk_hack"), m_sk_hack); - } - - - void add_builtins(family_id fid) { - decl_plugin * plugin = m_manager.get_plugin(fid); - SASSERT(plugin); - svector op_names; - plugin->get_op_names(op_names); - for (unsigned i = 0; i < op_names.size(); ++i) { - add_builtin_op(op_names[i].m_name.bare_str(), fid, op_names[i].m_kind); - } - } - - smtlib::benchmark* get_benchmark() { return &m_benchmark; } - -private: - - - bool parse(proto_expr_parser& parser) { - symbol benchmark("benchmark"); - symbol name(""); - proto_expr* const* rest = 0; - ptr_vector proto_exprs; - bool result = parser.parse(proto_exprs); - proto_expr* proto_expr = 0; - - if (!result) { - get_err() << "ERROR: parse error at line " << parser.get_line() << ".\n"; - } - - for (unsigned i = 0; result && i < proto_exprs.size(); ++i) { - - proto_expr = proto_exprs[i]; - - if (match_cons(proto_expr, benchmark, name, rest)) { - result = make_benchmark(name, rest); - } - else if (proto_expr && proto_expr->kind() != proto_expr::COMMENT) { - set_error("could not match expression to benchmark ", proto_expr); - } - else { - // proto_expr->kind() == proto_expr::COMMENT. - } - } - return result; - } - - void error_prefix(proto_expr* e) { - if (m_display_error_for_vs) { - if (e) { - get_err() << "Z3(" << e->line() << "," << e->pos() << "): ERROR: "; - } - } - else { - get_err() << "ERROR: "; - if (e) { - get_err() << "line " << e->line() << " column " << e->pos() << ": "; - } - } - } - - void set_error(char const * str, proto_expr* e) { - error_prefix(e); - if (e->kind() == proto_expr::ID) { - get_err() << str << " '" << e->string() << "'.\n"; - } - else { - get_err() << str << ".\n"; - } - } - - template - void set_error(T1 str1, T2 str2, proto_expr* e) { - error_prefix(e); - get_err() << str1 << " " << str2 << ".\n"; - } - - template - void set_error(T1 str1, T2 str2, T3 str3, proto_expr* e) { - error_prefix(e); - get_err() << str1 << str2 << str3 << ".\n"; - } - - bool match_cons(proto_expr * e, symbol const & sym, symbol & name, proto_expr* const*& proto_exprs) { - if (e && - e->kind() == proto_expr::CONS && - e->children() && - e->children()[0] && - e->children()[0]->string() == sym && - e->children()[1]) { - proto_exprs = e->children() + 2; - name = e->children()[1]->string(); - return true; - } - - return false; - } - - bool make_benchmark(symbol & name, proto_expr * const* proto_exprs) { - symbol extrasorts("extrasorts"); - symbol extrafuns("extrafuns"); - symbol extrapreds("extrapreds"); - symbol assumption("assumption"); - symbol assumption_core("assumption-core"); - symbol define_sorts_sym("define_sorts"); - symbol logic("logic"); - symbol formula("formula"); - symbol status("status"); - symbol sat("sat"); - symbol unsat("unsat"); - symbol unknown("unknown"); - symbol empty(""); - symbol source("source"); - symbol difficulty("difficulty"); - symbol category("category"); - bool success = true; - - push_benchmark(name); - - while (proto_exprs && *proto_exprs) { - proto_expr* e = *proto_exprs; - ++proto_exprs; - proto_expr* e1 = *proto_exprs; - - if (logic == e->string() && e1) { - name = e1->string(); - m_benchmark.set_logic(name); - - set_default_num_sort(name); - - if (name == symbol("QF_AX")) { - // Hack for supporting new QF_AX theory... - sort * index = m_manager.mk_uninterpreted_sort(symbol("Index")); - sort * element = m_manager.mk_uninterpreted_sort(symbol("Element")); - parameter params[2] = { parameter(index), parameter(element) }; - sort * array = m_manager.mk_sort(m_array_fid, ARRAY_SORT, 2, params); - smtlib::symtable* table = m_benchmark.get_symtable(); - table->insert(symbol("Index"), index); - table->insert(symbol("Element"), element); - // overwrite Array definition... - table->insert(symbol("Array"), array); - sort * args[3] = { array, index, element }; - func_decl * store = m_manager.mk_func_decl(m_array_fid, OP_STORE, 0, 0, 3, args); - table->insert(symbol("store"), store); - func_decl * sel = m_manager.mk_func_decl(m_array_fid, OP_SELECT, 0, 0, 2, args); - table->insert(symbol("select"), sel); - } - - ++proto_exprs; - continue; - } - - if (assumption == e->string() && e1) { - expr_ref t(m_manager); - if (!make_expression(e1, t) || - !push_assumption(t.get())) { - return false; - } - ++proto_exprs; - continue; - } - - if (assumption_core == e->string() && e1) { - expr_ref t(m_manager); - if (!make_expression(e1, t)) - return false; - m_benchmark.add_assumption(t.get()); - ++proto_exprs; - continue; - } - - if (define_sorts_sym == e->string() && e1) { - if (!define_sorts(e1)) { - return false; - } - ++proto_exprs; - continue; - } - - if (formula == e->string() && e1) { - expr_ref t(m_manager); - if (!make_expression(e1, t) || - !push_formula(t.get())) { - return false; - } - ++proto_exprs; - continue; - } - - if (status == e->string() && e1) { - if (sat == e1->string()) { - if (!push_status(smtlib::benchmark::SAT)) { - set_error("could not push status ", e1->string(),e1); - return false; - } - } - else if (unsat == e1->string()) { - if (!push_status(smtlib::benchmark::UNSAT)) { - set_error("could not push status ", e1->string(),e1); - return false; - } - } - else if (unknown == e1->string()) { - if (!push_status(smtlib::benchmark::UNKNOWN)) { - set_error("could not push status ", e1->string(),e1); - return false; - } - } - else { - set_error("could not recognize status ", e1->string(),e1); - return false; - } - ++proto_exprs; - continue; - } - - if (extrasorts == e->string() && e1) { - if (!declare_sorts(e1)) { - return false; - } - ++proto_exprs; - continue; - } - if (extrafuns == e->string() && e1) { - if (!declare_funs(e1)) { - return false; - } - ++proto_exprs; - continue; - } - if (extrapreds == e->string() && e1) { - if (!declare_preds(e1)) { - return false; - } - ++proto_exprs; - continue; - } - if (m_notes == e->string() && e1) { - ++proto_exprs; - continue; - } - - if ((source == e->string() || difficulty == e->string() || category == e->string()) && e1) { - ++proto_exprs; - continue; - } - - if (e->string() != empty) { - set_error("ignoring unknown attribute '", e->string().bare_str(), "'", e); - if (e1) { - ++proto_exprs; - } - // do not fail. - // success = false; - continue; - } - - TRACE("smtparser", - tout << "skipping: " << e->string() << " " << - e->line() << " " << - e->pos() << ".\n";); - continue; - } - return success; - } - - bool is_id_token(proto_expr* expr) { - return - expr && - (expr->kind() == proto_expr::ID || - expr->kind() == proto_expr::STRING || - expr->kind() == proto_expr::ANNOTATION); - } - - bool check_id(proto_expr* e) { - return is_id_token(e); - } - - bool make_expression(proto_expr * e, expr_ref & result) { - m_binding_level = 0; - symbol_table local_scope; - return make_expression(local_scope, e, result); - } - - bool make_func_decl(proto_expr* e, func_decl_ref& result) { - func_decl* f; - if (m_benchmark.get_symtable()->find1(e->string(), f)) { - result = f; - return true; - } - else { - return false; - } - } - - bool make_bool_expression(symbol_table& local_scope, proto_expr * e, expr_ref & result) { - if (!make_expression(local_scope, e, result)) { - return false; - } - if (!m_manager.is_bool(result)) { - set_error("expecting Boolean expression", e); - return false; - } - return true; - } - - bool make_bool_expressions(symbol_table& local_scope, proto_expr * const* chs, expr_ref_vector & exprs) { - while (chs && *chs) { - expr_ref result(m_manager); - m_binding_level = 0; - if (!make_bool_expression(local_scope, *chs, result)) { - return false; - } - exprs.push_back(result); - ++chs; - } - return true; - } - - bool make_expression(symbol_table& local_scope, proto_expr * e, expr_ref & result) { - // - // Walk proto_expr by using the zipper. - // That is, maintain a stack of what's - // . left - already processed. - // . right - to be processed. - // . up - above the processed node. - // - - region region; - - expr_ref_vector * left = alloc(expr_ref_vector, m_manager); - proto_expr* const* right = 0; - ptr_vector up; - proto_expr* current = e; - bool success = false; - idbuilder* builder = 0; - - while (true) { - - if (!current && right && *right) { - // - // pull the current from right. - // - current = *right; - ++right; - } - - if (!current && up.empty()) { - // - // we are done. - // - if (left->size() == 0) { - // set_error(); - set_error("there are no expressions to return", e); - goto cleanup; - } - if (left->size() != 1) { - set_error("there are too many expressions to return", e); - goto cleanup; - } - result = left->back(); - success = true; - goto cleanup; - } - - if (!current && !up.empty()) { - // - // There is nothing more to process at this level. - // - // Apply the operator on the stack to the - // current 'left' vector. - // Adjust the stack by popping the left and right - // work-lists. - // - expr_ref term(m_manager); - parse_frame* above = up.back(); - // symbol sym = above->get_proto_expr()->string(); - - if (above->make_term()) { - if (!above->make_term()->apply(*left, term)) { - set_error("Could not create application", - above->get_proto_expr()); - success = false; - goto cleanup; - } - } - else if (!make_app(above->get_proto_expr(), *left, term)) { - success = false; - goto cleanup; - } - dealloc(left); - left = above->detach_left(); - left->push_back(term.get()); - right = above->right(); - m_binding_level = above->binding_level(); - up.pop_back(); - continue; - } - - while (current && - current->kind() == proto_expr::CONS && - current->children() && - current->children()[0] && - !current->children()[1]) { - current = current->children()[0]; - } - - switch(current->kind()) { - - case proto_expr::ANNOTATION: - // ignore - current = 0; - break; - - case proto_expr::ID: { - symbol const& id = current->string(); - expr_ref term(m_manager); - expr * const_term = 0; - bool ok = true; - - if (local_scope.find(id, builder)) { - expr_ref_vector tmp(m_manager); - if (!builder->apply(tmp, term)) { - set_error("identifier supplied with the wrong number of arguments ", id, current); - goto cleanup; - - } - } - else if (m_benchmark.get_const(id, const_term)) { - // found. - term = const_term; - } - else if (is_builtin_const(id, current, current->num_params(), current->params(), ok, term)) { - if (!ok) goto cleanup; - } - else if (is_bvconst(id, current->num_params(), current->params(), term)) { - // found - } - else { - set_error("could not locate id ", id, current); - goto cleanup; - } - - left->push_back(term.get()); - current = 0; - break; - } - - case proto_expr::STRING: - // - // Ignore strings. - // - current = 0; - break; - - case proto_expr::COMMENT: - // - // Ignore comments. - // - current = 0; - break; - - case proto_expr::INT: - - left->push_back(mk_number(current->number(), true)); - current = 0; - break; - - case proto_expr::FLOAT: - left->push_back(mk_number(current->number(), false)); - current = 0; - break; - - case proto_expr::CONS: - - if (!current->children() || - !current->children()[0]) { - set_error("cons does not have children", current); - current = 0; - goto cleanup; - } - - // - // expect the head to be a symbol - // which can be used to build a term of - // the subterms. - // - - symbol const& head_symbol = current->children()[0]->string(); - - if (head_symbol == m_underscore) { - - expr_ref term(m_manager); - - proto_expr * const* chs = current->children() + 1; - symbol const& id = chs[0]->string(); - sort_ref_vector sorts(m_manager); - vector params; - bool ok = true; - if (!parse_params(chs+1, params, sorts)) { - goto cleanup; - } - if (is_builtin_const(id, current, params.size(), params.c_ptr(), ok, term)) { - if (!ok) goto cleanup; - } - else if (is_bvconst(id, params.size(), params.c_ptr(), term)) { - // ok - } - else { - set_error("Could not parse _ term", current); - goto cleanup; - } - left->push_back(term.get()); - current = 0; - break; - } - - if ((head_symbol == m_let) || - (head_symbol == m_flet)) { - - if (!current->children()[1] || - !current->children()[2]) { - set_error("let does not have two arguments", current); - goto cleanup; - } - - proto_expr * let_binding = current->children()[1]; - proto_expr * const* let_body = current->children()+2; - - // - // Collect bound variables and definitions for the bound variables - // into vectors 'vars' and 'bound'. - // - svector vars; - ptr_vector bound_vec; - if (is_binary_let_binding(let_binding)) { - vars.push_back(let_binding->children()[0]->string()); - bound_vec.push_back(let_binding->children()[1]); - } - else { - proto_expr* const* children = let_binding->children(); - if (!children) { - set_error("let binding does not have two arguments", let_binding); - goto cleanup; - } - while (*children) { - proto_expr* ch = *children; - if (!is_binary_let_binding(ch)) { - set_error("let binding does not have two arguments", ch); - goto cleanup; - } - vars.push_back(ch->children()[0]->string()); - bound_vec.push_back(ch->children()[1]); - ++children; - } - } - bound_vec.push_back(0); - - proto_expr** bound = new (region) proto_expr*[bound_vec.size()]; - for (unsigned i = 0; i < bound_vec.size(); ++i) { - bound[i] = bound_vec[i]; - } - - // - // Let's justify the transformation that - // pushes push_let and pop_let on the stack. - // and how it processes the let declaration. - // - // walk up left ((let ((v1 x1) (v2 x2)) z)::right) - // - // = - // - // walk (up::(pop_let(),left,right)::(bind(v1,v2),[],[z])) [] [x1;x2] - // - // = (* assume x1 -> y1, x2 -> y2 *) - // - // walk (up::(pop_let(),left,right)::(bind(v1,v2),[],[z])) [y1;y2] [] - // - // = (* apply binding *) - // - // walk (up::(pop_let(),left,right)) [] [z] - // - // = (* assume z -> u *) - // - // walk up {left::u] right - // - // so if pop_let(v) [a,b] has the effect of removing v from the environment - // and projecting the second element "b", we obtain the effect of a let-binding. - // - - expr_ref_vector * pinned = alloc(expr_ref_vector, m_manager); - pop_let * popl = new (region) pop_let(local_scope, pinned); - up.push_back(new (region) parse_frame(let_binding, popl, left, right, m_binding_level)); - - - push_let_and * pushl = new (region) push_let_and(this, region, local_scope, pinned, vars.size(), vars.c_ptr()); - expr_ref_vector * tmp = alloc(expr_ref_vector, m_manager); - up.push_back(new (region) parse_frame(let_binding, pushl, tmp, let_body, m_binding_level)); - - - left = alloc(expr_ref_vector, m_manager); - right = bound; - current = 0; - break; - } - - if (head_symbol == m_lblneg || - head_symbol == m_lblpos) { - if (!current->children()[1] || - !current->children()[2]) { - set_error("labels require two arguments", current); - goto cleanup; - } - - bool is_pos = head_symbol == m_lblpos; - idbuilder* lbl = new (region) build_label(this, is_pos, current->children()[1]); - - up.push_back(new (region) parse_frame(current, lbl, left, right, m_binding_level)); - - // - // process the body. - // - left = alloc(expr_ref_vector, m_manager); - right = 0; - current = current->children()[2]; - break; - } - - if (head_symbol == m_bang) { - proto_expr* const* children = current->children(); - proto_expr* body = children[1]; - proto_expr* lblname = 0; - bool is_pos = false; - - children += 2; - - while (children[0] && - children[0]->kind() == proto_expr::ANNOTATION && - children[1]) { - symbol id = children[0]->string(); - - if ((id == m_lblneg) || - (id == m_lblpos)) { - is_pos = id == m_lblpos; - lblname = children[1]; - } - - children += 2; - } - - if (lblname) { - idbuilder* lbl = new (region) build_label(this, is_pos, lblname); - up.push_back(new (region) parse_frame(current, lbl, left, right, m_binding_level)); - left = alloc(expr_ref_vector, m_manager); - right = 0; - } - - // - // process the body. - // - current = body; - break; - } - - if ((head_symbol == m_forall) || - (head_symbol == m_exists)) { - - expr_ref_buffer patterns(m_manager); - expr_ref_buffer no_patterns(m_manager); - sort_ref_buffer sorts(m_manager); - svector vars; - int weight = 1; - - proto_expr* const* children = current->children(); - proto_expr* body = 0; - - ++children; - - if (!children[0] || !children[1]) { - set_error("quantifier should have at least two arguments", current); - goto cleanup; - } - - // - // restore 'left' and 'right' working set and m_binding_level. - // - up.push_back(new (region) parse_frame(current, new (region) identity(), left, right, m_binding_level)); - left = alloc(expr_ref_vector, m_manager); - - // - // declare the bound variables. - // - - local_scope.begin_scope(); - - while (children[0] && children[1] && - (children[1]->kind() != proto_expr::ANNOTATION)) { - - if (!parse_bound(local_scope, region, *children, vars, sorts)) { - goto cleanup; - } - ++children; - } - - body = children[0]; - - if (is_annotated_cons(body)) { - children = body->children()+1; - body = body->children()[1]; - } - - ++children; - - symbol qid = symbol(current->line()); - symbol skid = symbol(); - - read_patterns(vars.size(), local_scope, children, patterns, no_patterns, weight, qid, skid); - - // - // push a parse_frame to undo the scope of the quantifier. - // - - SASSERT(sorts.size() > 0); - - idbuilder* pop_q = new (region) pop_quantifier(this, (head_symbol == m_forall), weight, qid, skid, patterns, no_patterns, sorts, vars, local_scope); - - expr_ref_vector * empty_v = alloc(expr_ref_vector, m_manager); - up.push_back(new (region) parse_frame(current, pop_q, empty_v, 0, m_binding_level)); - - // - // process the body. - // - right = 0; - current = body; - break; - } - - if (is_underscore_op(region, current->children()[0], builder)) { - up.push_back(new (region) parse_frame(current, builder, left, right, m_binding_level)); - } - else if (local_scope.find(head_symbol, builder)) { - up.push_back(new (region) parse_frame(current, builder, left, right, m_binding_level)); - } - else { - up.push_back(new (region) parse_frame(current->children()[0], left, right, m_binding_level)); - } - left = alloc(expr_ref_vector, m_manager); - right = current->children() + 1; - current = 0; - break; - } - } - - cleanup: - - if (success && !is_well_sorted(m_manager, result)) { - set_error("expression is not well sorted", e); - success = false; - } - - dealloc(left); - while (!up.empty()) { - dealloc(up.back()->detach_left()); - up.pop_back(); - } - return success; - } - - bool read_patterns(unsigned num_bindings, symbol_table & local_scope, proto_expr * const * & children, - expr_ref_buffer & patterns, expr_ref_buffer & no_patterns, int& weight, symbol& qid, symbol& skid) { - proto_region region; - while (children[0] && - children[0]->kind() == proto_expr::ANNOTATION && - children[1]) { - - if (children[0]->string() == symbol("qid") || - children[0]->string() == symbol("named")) { - qid = children[1]->string(); - children += 2; - continue; - } - - if (children[0]->string() == symbol("skolemid")) { - skid = children[1]->string(); - children += 2; - continue; - } - - ptr_vector proto_exprs; - - if (children[1]->kind() == proto_expr::COMMENT) { - std::string s = children[1]->string().str(); - std::istringstream stream(s); - scanner scanner(stream, get_err(), false); - proto_expr_parser parser(region, scanner, get_err()); - - if (!parser.parse(proto_exprs)) { - set_error("could not parse expression", children[1]); - return false; - } - } else if (children[1]->kind() == proto_expr::CONS) { - for (proto_expr* const* pexpr = children[1]->children(); *pexpr; pexpr++) - proto_exprs.push_back(*pexpr); - } else { - proto_exprs.push_back(children[1]); - } - - expr_ref_buffer ts(m_manager); - for (unsigned i = 0; i < proto_exprs.size(); ++i) { - expr_ref t(m_manager); - if (!make_expression(local_scope, proto_exprs[i], t)) { - return false; - } - ts.push_back(t.get()); - } - - if (children[0]->string() == symbol("pat") || - children[0]->string() == symbol("pats") || - children[0]->string() == symbol("pattern")) { - for (unsigned i = 0; i < ts.size(); ++i) { - if (!is_app(ts[i])) { - set_error("invalid pattern", children[0]); - return false; - } - } - expr_ref p(m_manager); - p = m_manager.mk_pattern(ts.size(), (app*const*)(ts.c_ptr())); - if (!p || (!ignore_user_patterns() && !m_pattern_validator(num_bindings, p, children[0]->line(), children[0]->pos()))) { - set_error("invalid pattern", children[0]); - return false; - } - patterns.push_back(p); - } - else if (children[0]->string() == symbol("ex_act") && ts.size() == 1) { - app_ref sk_hack(m_manager); - sk_hack = m_manager.mk_app(m_sk_hack, 1, ts.c_ptr()); - app * sk_hackp = sk_hack.get(); - expr_ref p(m_manager); - p = m_manager.mk_pattern(1, &sk_hackp); - if (!p || (!ignore_user_patterns() && !m_pattern_validator(num_bindings, p, children[0]->line(), children[0]->pos()))) { - set_error("invalid pattern", children[0]); - return false; - } - patterns.push_back(p); - } - else if ((children[0]->string() == symbol("nopat") || - children[0]->string() == symbol("no-pattern")) - && ts.size() == 1) { - no_patterns.push_back(ts[0]); - } - else if (children[0]->string() == symbol("weight") && ts.size() == 1 && - proto_exprs[0]->kind() == proto_expr::INT && - proto_exprs[0]->number().is_unsigned()) { - weight = proto_exprs[0]->number().get_unsigned(); - } - else { - // TODO: this should be a warning, perferably once per unknown kind of annotation - set_error("could not understand annotation '", - children[0]->string().bare_str(), "'", children[0]); - } - - children += 2; - } - return true; - } - - void set_default_num_sort(symbol const& name) { - if (name == symbol("QF_RDL") || - name == symbol("QF_LRA") || - name == symbol("LRA") || - name == symbol("RDL") || - name == symbol("QF_NRA") || - name == symbol("QF_UFNRA") || - name == symbol("QF_UFLRA")) { - m_int_sort = m_real_sort; - } - } - - bool get_sort(theory* th, char const * s, sort_ref& sort) { - return make_sort(symbol(s), 0, 0, sort); - } - - - bool make_sort(symbol const & id, unsigned num_params, parameter const* params, sort_ref& s) { - builtin_op info; - if (m_builtin_sorts.find(id, info)) { - s = m_manager.mk_sort(info.m_family_id, info.m_kind, num_params, params); - return true; - } - - if (num_params == 2 && symbol("Array") == id) { - // Old HACK to accomodate bit-vector arrays. - - if (!params[0].is_int()) { - throw default_exception("Non-integer parameter to array"); - return false; - } - if (!params[1].is_int()) { - throw default_exception("Non-integer parameter to array"); - return false; - } - parameter bv_params0[1] = { parameter(params[0].get_int()) }; - parameter bv_params1[1] = { parameter(params[1].get_int()) }; - - sort * t1 = m_manager.mk_sort(m_bv_fid, BV_SORT, 1, bv_params0); - sort * t2 = m_manager.mk_sort(m_bv_fid, BV_SORT, 1, bv_params1); - parameter params[2] = { parameter(t1), parameter(t2) }; - s = m_manager.mk_sort(m_array_fid, ARRAY_SORT, 2, params); - return true; - } - - sort* srt = 0; - if (m_benchmark.get_sort(id, srt)) { - s = srt; - return true; - } - return false; - } - - bool make_sort(proto_expr * e, sort_ref& s) { - SASSERT(can_be_sort(e)); - symtable& env = *m_benchmark.get_symtable(); - sort_builder* mk_sort; - switch(e->kind()) { - case proto_expr::ID: { - if (make_sort(e->string(), e->num_params(), e->params(), s)) { - return true; - } - if (env.lookup(e->string(), mk_sort)) { - if (!mk_sort->apply(e->num_params(), e->params(), s)) { - set_error(mk_sort->error_message(), e); - return false; - } - return true; - } - set_error("could not find sort ", e); - return false; - } - case proto_expr::CONS: { - if (!can_be_sort(e)) { - set_error("expression cannot be a sort", e); - return false; - } - proto_expr *const* chs = e->children(); - if (is_underscore(e)) { - ++chs; - } - symbol name = (*chs)->string(); - if (!env.lookup(name, mk_sort)) { - set_error("could not find sort symbol '", name.str(), "'", e); - return false; - } - sort_ref_vector sorts(m_manager); - vector params; - if (!parse_params(chs+1, params, sorts)) { - return false; - } - - if (!mk_sort->apply(params.size(), params.c_ptr(), s)) { - set_error(mk_sort->error_message(), e); - return false; - } - return true; - } - default: - set_error("could not create sort ", e); - return false; - } - } - - bool parse_params(proto_expr* const* chs,vector& params, sort_ref_vector& sorts) { - while (*chs) { - if ((*chs)->kind() == proto_expr::INT) { - rational const& num = (*chs)->number(); - if (num.is_unsigned()) { - params.push_back(parameter(num.get_unsigned())); - } - else { - params.push_back(parameter(num)); - } - } - else { - sort_ref s1(m_manager); - if (!make_sort(*chs, s1)) { - return false; - } - sorts.push_back(s1); - params.push_back(parameter((ast*)s1.get())); - } - ++chs; - } - return true; - } - - bool parse_bound( - symbol_table& local_scope, - region& region, - proto_expr* bound, - svector& vars, - sort_ref_buffer& sorts - ) - { - if (is_cons_list(bound)) { - proto_expr *const* children = bound->children(); - while (*children) { - if (!parse_bound(local_scope, region, *children, vars, sorts)) { - return false; - } - ++children; - } - return true; - } - if (!can_be_sorted_var(bound)) { - set_error("bound variable should contain a list of pairs", bound); - return false; - } - proto_expr* var = bound->children()[0]; - proto_expr* sort_proto_expr = bound->children()[1]; - - sort_ref sort(m_manager); - if (!make_sort(sort_proto_expr, sort)) { - return false; - } - sorts.push_back(sort); - vars.push_back(var->string()); - - local_scope.insert( - var->string(), - new (region) bound_var(this, sort) - ); - - ++m_binding_level; - - return true; - } - - bool can_be_sort(proto_expr* e) { - if (e && e->kind() == proto_expr::ID) { - return true; - } - if (is_underscore(e)) { - return true; - } - - if (e && - e->kind() == proto_expr::CONS && - e->children() && - e->children()[0] && - e->children()[1]) { - proto_expr* const* ch = e->children(); - while(*ch) { - if (!can_be_sort(*ch)) { - return false; - } - ++ch; - } - return true; - } - return false; - } - - bool declare_sorts(proto_expr* e) { - proto_expr* const * children = e->children(); - - while (children && *children) { - proto_expr* ch = *children; - switch(ch->kind()) { - - case proto_expr::ID: - m_benchmark.declare_sort(ch->string()); - break; - - case proto_expr::CONS: - // - // The declaration of type constructors - // consists of an identifier together with - // a number indicating the arity of the - // constructor. - // - if (ch->children() && - ch->children()[0] && - ch->children()[0]->kind() == proto_expr::ID && - ch->children()[1] && - ch->children()[1]->kind() == proto_expr::INT) { - - // unsigned num = (unsigned) ch->children()[1]->number().get_uint64(); - m_benchmark.declare_sort(ch->children()[0]->string()); - } - break; - - case proto_expr::ANNOTATION: - break; - - default: - set_error("unexpected argument to sorts",ch); - return false; - } - ++children; - } - return true; - } - - bool define_sorts(proto_expr* e) { - proto_expr* const * children = e->children(); - - while (children && *children) { - if (!define_sort(*children)) { - return false; - } - ++children; - } - return true; - } - - bool define_sort(proto_expr* e) { - proto_expr* const * children = e->children(); - sort_ref_buffer domain(m_manager); - - // - // First element in list must be an identifier. - // there should be just two elements. - // - if (!children || - !children[0] || - !(children[0]->kind() == proto_expr::ID) || - !children[1] || - children[2]) { - set_error("unexpected arguments to function declaration", e); - return false; - } - symbol name = children[0]->string(); - sort_ref s(m_manager); - if (!can_be_sort(children[1]) || - !make_sort(children[1], s)) { - set_error("unexpected arguments to function declaration", e); - return false; - } - - m_benchmark.get_symtable()->insert(name, s); - - return true; - } - - bool declare_funs(proto_expr* e) { - proto_expr* const * children = e->children(); - - while (children && *children) { - if (!declare_fun(*children)) { - return false; - } - ++children; - } - return true; - } - class define_sort_cls : public sort_builder { - smtparser& m_parser; - proto_region m_region; - proto_expr* m_expr; - svector m_params; - symbol m_name; - std::string m_error_message; - - public: - define_sort_cls(smtparser& p, symbol const& name, proto_expr* e, unsigned num_params, symbol* params) : - m_parser(p), - m_name(name) { - for (unsigned i = 0; i < num_params; ++i) { - m_params.push_back(params[i]); - } - m_expr = proto_expr::copy(m_region, e); - } - - virtual bool apply(unsigned num_params, parameter const* params, sort_ref & result) { - smtlib::symtable * symtable = m_parser.m_benchmark.get_symtable(); - if (m_params.size() != num_params) { - std::ostringstream strm; - strm << "wrong number of arguments passed to " << m_name << " " - << m_params.size() << " expected, but " << num_params << " given"; - m_error_message = strm.str(); - return false; - } - for (unsigned i = 0; i < num_params; ++i) { - parameter p(params[i]); - if (!p.is_ast() || !is_sort(p.get_ast())) { - symtable->pop_sorts(i); - std::ostringstream strm; - strm << "argument " << i << " is not a sort"; - m_error_message = strm.str(); - return false; - } - symtable->push_sort(m_params[i], to_sort(p.get_ast())); - } - bool success = m_parser.make_sort(m_expr, result); - - symtable->pop_sorts(num_params); - return success; - } - - virtual char const* error_message() { - return m_error_message.c_str(); - } - - }; - - // (define-sort name (*) ) - bool define_sort(proto_expr* id, proto_expr* sorts, proto_expr* srt) { - symbol name = id->string(); - proto_expr* const * children = sorts->children(); - svector names; - - if (!children) { - set_error("Sort definition expects a list of sort symbols",id); - return false; - } - - while (children[0]) { - id = children[0]; - if(id->kind() != proto_expr::ID) { - set_error("unexpected argument, expected ID", id); - return false; - } - names.push_back(id->string()); - ++children; - } - - m_benchmark.get_symtable()->insert(name, alloc(define_sort_cls, *this, name, srt, names.size(), names.c_ptr())); - return true; - } - - bool declare_fun(proto_expr* id, proto_expr* sorts, proto_expr* srt) { - proto_expr* const * children = sorts?sorts->children():0; - sort_ref_buffer domain(m_manager); - symbol name = id->string(); - - if (sorts && !children) { - set_error("Function declaration expects a list of sorts", id); - return false; - } - // - // parse domain. - // - while (sorts && children[0]) { - sort_ref s(m_manager); - if (!make_sort(children[0], s)) { - return false; - } - domain.push_back(s); - ++children; - } - - sort_ref range(m_manager); - if (!make_sort(srt, range)) { - return false; - } - bool is_associative = false; - bool is_commutative = false; - bool is_injective = false; - m_benchmark.declare_func(name, domain, range, is_associative, is_commutative, is_injective); - return true; - } - - bool declare_fun(proto_expr* e) { - proto_expr* const * children = e->children(); - sort_ref_buffer domain(m_manager); - // - // Skip declaration of numbers. - // - if (children && - children[0] && - children[0]->kind() == proto_expr::INT) { - return true; - } - - // - // First element in list must be an identifier. - // - if (!children || - !children[0] || - !(children[0]->kind() == proto_expr::ID)) { - set_error("unexpected arguments to function declaration", e); - return false; - } - - symbol name = children[0]->string(); - - ++children; - - - if (!can_be_sort(children[0])) { - set_error("unexpected arguments to function declaration", e); - return false; - } - - // - // parse domain. - // - while (can_be_sort(children[1])) { - sort_ref s(m_manager); - if (!make_sort(children[0], s)) { - return false; - } - domain.push_back(s); - ++children; - } - - // - // parse range. - // - SASSERT(can_be_sort(children[0])); - - sort_ref range(m_manager); - if (!make_sort(children[0], range)) { - return false; - } - ++children; - - // - // parse attributes. - // - bool is_associative = false; - bool is_commutative = false; - bool is_injective = false; - - while(children[0] && children[0]->kind() == proto_expr::ANNOTATION) { - - if (m_associative == children[0]->string()) { - is_associative = true; - } - else if (m_commutative == children[0]->string()) { - is_commutative = true; - } - else if (m_injective == children[0]->string()) { - is_injective = true; - } - ++children; - } - - m_benchmark.declare_func(name, domain, range, is_associative, is_commutative, is_injective); - - return true; - } - - bool declare_preds(proto_expr* e) { - proto_expr* const * children = e->children(); - - while (children && *children) { - if (!declare_pred(*children)) { - return false; - } - ++children; - } - return true; - } - - - bool declare_pred(proto_expr* e) { - proto_expr* const * children = e->children(); - if (!children || !children[0] || !(children[0]->kind() == proto_expr::ID)) { - set_error("unexpected arguments to predicate declaration", e); - return false; - } - symbol const & name = children[0]->string(); - sort_ref_buffer domain(m_manager); - sort * bool_sort = m_manager.mk_bool_sort(); - - ++children; - - while (can_be_sort(children[0])) { - sort_ref s(m_manager); - if (!make_sort(children[0], s)) { - return false; - } - domain.push_back(s); - ++children; - } - - m_benchmark.declare_func(name, domain, bool_sort, false, false, false); - - return true; - } - - bool can_be_sorted_var(proto_expr* e) { - return - e && - (e->kind() == proto_expr::CONS) && - e->children() && - e->children()[0] && - (e->children()[0]->kind() == proto_expr::ID) && - can_be_sort(e->children()[1]); - } - - bool is_cons_list(proto_expr* e) { - return - e && - (e->kind() == proto_expr::CONS) && - e->children() && - e->children()[0] && - e->children()[0]->kind() == proto_expr::CONS; - } - - bool is_prefixed(proto_expr* e, symbol const& s) { - return - e && - (e->kind() == proto_expr::CONS) && - e->children() && - e->children()[0] && - e->children()[1] && - e->children()[0]->string() == s; - - } - - bool is_underscore(proto_expr* e) { - return - is_prefixed(e, m_underscore) && - e->children()[1]->kind() == proto_expr::ID; - } - - bool is_annotated_cons(proto_expr* e) { - return is_prefixed(e, m_bang); - } - - bool is_builtin_const(symbol const& id, proto_expr* current, unsigned num_params, parameter * params, bool& ok, expr_ref& term) { - builtin_op info; - ok = true; - if (!m_builtin_ops.find(id, info)) { - return false; - } - fix_parameters(num_params, params); - func_decl* d = m_manager.mk_func_decl(info.m_family_id, info.m_kind, num_params, params, 0, (expr * const *)0); - if (!d) { - set_error("could not create a term from constant ", id, current); - ok = false; - } - else if (d->get_arity() != 0) { - set_error("identifier expects arguments ", id, current); - ok = false; - } - else { - term = m_manager.mk_const(d); - } - return true; - } - - bool is_underscore_op(region& r, proto_expr* e, idbuilder*& builder) { - if (!is_underscore(e)) { - return false; - } - builtin_op info; - proto_expr *const* chs = e->children()+1; - symbol const& id = (*chs)->string(); - sort_ref_vector sorts(m_manager); - vector params; - - if (!m_builtin_ops.find(id, info)) { - return false; - } - if (!parse_params(chs+1, params, sorts)) { - return false; - } - - builder = new (r) builtin_builder(this, info.m_family_id, info.m_kind, params); - return true; - } - - void fix_parameters(unsigned num_params, parameter* params) { - for (unsigned i = 0; i < num_params; ++i) { - func_decl* d = 0; - sort* s = 0; - builtin_op info; - if (params[i].is_symbol() && m_benchmark.get_symtable()->find1(params[i].get_symbol(), d)) { - params[i] = parameter(d); - } - else if (params[i].is_symbol() && m_benchmark.get_symtable()->find(params[i].get_symbol(), s)) { - params[i] = parameter(s); - } - else if (params[i].is_symbol() && m_builtin_sorts.find(params[i].get_symbol(), info)) { - params[i] = parameter(m_manager.mk_sort(info.m_family_id, info.m_kind, 0, 0)); - } - } - } - - bool make_app(proto_expr * proto_expr, expr_ref_vector const & args, expr_ref & result) { - symbol const& name = proto_expr->string(); - ptr_vector sorts; - func_decl * d = 0; - smtlib::symtable * symtable = m_benchmark.get_symtable(); - - for (unsigned i = 0; i < args.size(); ++i) { - sorts.push_back(m_manager.get_sort(args.get(i))); - } - - if (symtable->find_overload(name, sorts, d)) { - result = m_manager.mk_app(d, args.size(), args.c_ptr()); - return true; - } - - builtin_op info; - if (m_builtin_ops.find(name, info)) { - unsigned num_params = proto_expr->num_params(); - parameter * params = proto_expr->params(); - fix_parameters(num_params, params); - d = m_manager.mk_func_decl(info.m_family_id, info.m_kind, num_params, params, args.size(), args.c_ptr()); - if (d) { - result = m_manager.mk_app(d, args.size(), args.c_ptr()); - return true; - } - } - - rational arg2_value; - bool arg2_is_int; - - if (name == symbol("store") && - args.size() == 3 && - m_anum_util.is_numeral(args.get(2), arg2_value, arg2_is_int) && - arg2_is_int) { - expr_ref_vector new_args(m_manager); - new_args.push_back(args.get(0)); - new_args.push_back(args.get(1)); - new_args.push_back(m_anum_util.mk_numeral(arg2_value, false)); - sorts.reset(); - for (unsigned i = 0; i < args.size(); ++i) { - sorts.push_back(m_manager.get_sort(new_args.get(i))); - } - if (symtable->find_overload(name, sorts, d)) { - result = m_manager.mk_app(d, new_args.size(), new_args.c_ptr()); - return true; - } - } - - error_prefix(proto_expr); - get_err() << "could not find overload for '" << name << "' "; - for (unsigned i = 0; i < sorts.size(); ++i) { - get_err() << "Argument: " - << mk_pp(args.get(i), m_manager) - << " has type " - << mk_pp(sorts[i], m_manager) - << ".\n"; - } - return false; - } - - class nullary : public idbuilder { - expr* m_expr; - smtparser* m_parser; - unsigned m_decl_level_save; - public: - nullary(expr* e, smtparser* p) : m_expr(e), m_parser(p), m_decl_level_save(p->m_binding_level) {} - - virtual bool apply(expr_ref_vector const& args, expr_ref & result) { - unsigned decl_level = m_parser->m_binding_level; - SASSERT(decl_level >= m_decl_level_save); - shift_vars shifty(m_parser->m_manager); - shifty(m_expr, decl_level - m_decl_level_save, result); - return (args.size() == 0); - } - }; - - class identity : public idbuilder { - public: - identity() {} - - virtual bool apply(expr_ref_vector const & args, expr_ref & result) { - if (args.size() == 1) { - result = args.back(); - return true; - } - else { - return false; - } - } - }; - - class parse_frame { - public: - - parse_frame(proto_expr * e, idbuilder * make, expr_ref_vector * left, proto_expr * const* right, unsigned binding_level): - m_proto_expr(e), - m_make_term(make), - m_left(left), - m_right(right), - m_binding_level(binding_level) { - } - - parse_frame(proto_expr * e, expr_ref_vector * left, proto_expr * const* right, unsigned binding_level): - m_proto_expr(e), - m_make_term(0), - m_left(left), - m_right(right), - m_binding_level(binding_level) { - } - - expr_ref_vector * detach_left() { - expr_ref_vector * result = m_left; - SASSERT(m_left); - m_left = 0; - return result; - } - - unsigned binding_level() const { return m_binding_level; } - - proto_expr* const * right() const { return m_right; } - - idbuilder* make_term() { return m_make_term; } - - proto_expr* get_proto_expr() const { return m_proto_expr; } - - ~parse_frame() { dealloc(m_left); } - - private: - - proto_expr* m_proto_expr; - idbuilder* m_make_term; - expr_ref_vector * m_left; - proto_expr* const * m_right; - unsigned m_binding_level; - - parse_frame & operator=(parse_frame const & other); - - parse_frame(parse_frame const & other); - - }; - - class build_label : public idbuilder { - bool m_pos; - symbol m_sym; - smtparser * m_smt; - public: - build_label(smtparser * smt, bool is_pos, proto_expr * sym): m_pos(is_pos), m_smt(smt) { - switch(sym->kind()) { - case proto_expr::ID: - case proto_expr::STRING: - m_sym = sym->string(); - break; - case proto_expr::INT: - m_sym = symbol(sym->number().to_string().c_str()); - break; - default: - UNREACHABLE(); - break; - } - } - - virtual bool apply(expr_ref_vector const & args, expr_ref & result) { - if (args.size() >= 1) { - result = m_smt->m_manager.mk_label(m_pos, m_sym, args.get(0)); - return true; - } - else { - return false; - } - } - }; - - class pop_let : public idbuilder { - public: - pop_let(symbol_table & local_scope, expr_ref_vector* pinned = 0): - m_local_scope(local_scope), - m_pinned(pinned) { - } - - virtual ~pop_let() {} - - virtual bool apply(expr_ref_vector const & args, expr_ref & result) { - dealloc(m_pinned); - if (args.size() == 2) { - m_local_scope.end_scope(); - result = args.get(1); - return true; - } - else { - return false; - } - } - private: - symbol_table & m_local_scope; - expr_ref_vector* m_pinned; - }; - - class push_let : public idbuilder { - smtparser* m_parser; - region & m_region; - symbol_table & m_local_scope; - symbol m_let_var; - - public: - push_let(smtparser* p, region & region, symbol_table & local_scope, symbol const & let_var): - m_parser(p), - m_region(region), - m_local_scope(local_scope), - m_let_var(let_var) { - } - - virtual bool apply(expr_ref_vector const & args, expr_ref & result) { - // - // . push a scope, - // . create a nullary function using the variable/term association. - // . return the (first) argument. - // - // - if (args.size() == 1) { - m_local_scope.begin_scope(); - m_local_scope.insert(m_let_var, new (m_region) nullary(args.back(), m_parser)); - result = args.back(); - return true; - } - else { - return false; - } - } - }; - - // push multiple let bound variables. - class push_let_and : public idbuilder { - smtparser* m_parser; - region & m_region; - symbol_table & m_local_scope; - unsigned m_num_vars; - symbol* m_vars; - expr_ref_vector* m_pinned; - - public: - push_let_and(smtparser* p, region & region, symbol_table & local_scope, expr_ref_vector* pinned, unsigned num_vars, symbol const* vars): - m_parser(p), - m_region(region), - m_local_scope(local_scope), - m_num_vars(num_vars), - m_vars(new (region) symbol[num_vars]), - m_pinned(pinned) { - for (unsigned i = 0; i < num_vars; ++i) { - m_vars[i] = vars[i]; - } - } - - virtual bool apply(expr_ref_vector const & args, expr_ref & result) { - if (args.size() != m_num_vars) { - return false; - } - - // - // . push a scope, - // . create a nullary function using the variable/term association. - // . return the last argument (arbitrary). - // - - m_local_scope.begin_scope(); - for (unsigned i = 0; i < m_num_vars; ++i) { - m_local_scope.insert(m_vars[i], new (m_region) nullary(args[i], m_parser)); - m_pinned->push_back(args[i]); - } - result = args.back(); - return true; - } - }; - - class bound_var : public idbuilder { - public: - bound_var(smtparser * smt, sort * sort): - m_smt(smt), - m_decl_level(smt->m_binding_level), - m_sort(sort) { - } - - virtual bool apply(expr_ref_vector const & args, expr_ref & result) { - SASSERT(m_smt->m_binding_level > m_decl_level); - unsigned idx = m_smt->m_binding_level - m_decl_level - 1; - result = m_smt->m_manager.mk_var(idx, m_sort); - return args.empty(); - } - - private: - smtparser * m_smt; - unsigned m_decl_level; - sort * m_sort; - }; - - class pop_quantifier : public idbuilder { - public: - pop_quantifier(smtparser * smt, bool is_forall, int weight, symbol const& qid, symbol const& skid, expr_ref_buffer & patterns, expr_ref_buffer & no_patterns, sort_ref_buffer & sorts, - svector& vars, symbol_table & local_scope): - m_smt(smt), - m_is_forall(is_forall), - m_weight(weight), - m_qid(qid), - m_skid(skid), - m_patterns(m_smt->m_manager), - m_no_patterns(m_smt->m_manager), - m_sorts(m_smt->m_manager), - m_local_scope(local_scope) { - SASSERT(sorts.size() == vars.size()); - - m_vars.append(vars); - m_sorts.append(sorts); - m_patterns.append(patterns); - m_no_patterns.append(no_patterns); - } - - virtual bool apply(expr_ref_vector const & args, expr_ref & result) { - if (args.size() != 1) { - return false; - } - - m_local_scope.end_scope(); - - expr * body = args.back(); - - if (m_smt->ignore_user_patterns()) { - TRACE("pat_bug", tout << "ignoring user patterns...: " << m_patterns.size() << "\n";); - result = m_smt->m_manager.mk_quantifier(m_is_forall, - m_sorts.size(), // num_decls - m_sorts.c_ptr(), // decl_sorts - m_vars.begin(), // decl_names - body, - m_weight, - m_qid, - m_skid, - 0, - 0, - 0, - 0); - } - else if (!m_patterns.empty()) { - if (!m_no_patterns.empty()) { - m_smt->set_error("patterns were provided, ignoring :nopat attribute.", ((proto_expr*)0)); - } - result = m_smt->m_manager.mk_quantifier(m_is_forall, - m_sorts.size(), // num_decls - m_sorts.c_ptr(), // decl_sorts - m_vars.begin(), // decl_names - body, - m_weight, - m_qid, - m_skid, - m_patterns.size(), - m_patterns.c_ptr(), - 0, - 0); - } - else { - result = m_smt->m_manager.mk_quantifier(m_is_forall, - m_sorts.size(), // num_decls - m_sorts.c_ptr(), // decl_sorts - m_vars.begin(), // decl_names - body, - m_weight, - m_qid, - m_skid, - 0, - 0, - m_no_patterns.size(), - m_no_patterns.c_ptr()); - } - - // - // reclaim memory resources on application. - // - - m_vars.finalize(); - m_sorts.finalize(); - m_patterns.finalize(); - m_no_patterns.finalize(); - return true; - } - - private: - smtparser* m_smt; - bool m_is_forall; - int m_weight; - symbol m_qid; - symbol m_skid; - expr_ref_buffer m_patterns; - expr_ref_buffer m_no_patterns; - sort_ref_buffer m_sorts; - svector m_vars; - symbol_table& m_local_scope; - }; - - class builtin_builder : public idbuilder { - smtparser* m_smt; - family_id m_fid; - decl_kind m_kind; - vector m_params; - - public: - builtin_builder(smtparser* smt, family_id fid, decl_kind k,vector const& p): - m_smt(smt), - m_fid(fid), - m_kind(k), - m_params(p) - { - } - - virtual bool apply(expr_ref_vector const& args, expr_ref& result) { - ast_manager& m = m_smt->m_manager; - func_decl* d = m.mk_func_decl(m_fid, m_kind, m_params.size(), m_params.c_ptr(), args.size(), args.c_ptr()); - if (d) { - result = m.mk_app(d, args.size(), args.c_ptr()); - } - m_params.finalize(); - return d != 0; - } - }; - - bool push_status(smtlib::benchmark::status status) { - m_benchmark.set_status( status); - return true; - } - - expr * mk_number(rational const & r, bool is_int){ - if (m_int_sort == m_real_sort) // integer constants should be mapped to real - is_int = false; - return m_anum_util.mk_numeral(r, is_int); - } - - void push_benchmark(symbol const & name) { - m_benchmark.set_name(name); - } - - bool push_assumption(expr * t) { - m_benchmark.add_axiom(t); - return true; - } - - bool push_formula(expr * t) { - m_benchmark.add_formula(t); - return true; - } - - bool is_binary_let_binding(proto_expr* let_binding) { - return - let_binding && - let_binding->children() && - let_binding->children()[0] && - (let_binding->children()[0]->kind() == proto_expr::ID) && - let_binding->children()[1] && - !let_binding->children()[2]; - } - - bool is_bvconst(symbol const & fname, unsigned num_params, parameter const* params, expr_ref & term) { - rational n; - char const * str = fname.bare_str(); - unsigned sz = 0; - - if (strncmp(str, "bvbin", 5) == 0) { - str += 5; - n = rational(0); - while (*str == '1' || *str == '0') { - n *= rational(2); - n += rational(*str - '0'); - ++sz; - ++str; - } - if (sz == 0) { - return false; - } - } - else if (strncmp(str, "bvhex", 5) == 0) { - n = rational(0); - str += 5; - while (('0' <= *str && *str <= '9') || - ('a' <= *str && *str <= 'f') || - ('A' <= *str && *str <= 'F')) { - n *= rational(16); - if ('0' <= *str && *str <= '9') { - n += rational(*str - '0'); - } - else if ('a' <= *str && *str <= 'f') { - n += rational(10); - n += rational(*str - 'a'); - } - else { - SASSERT('A' <= *str && *str <= 'F'); - n += rational(10); - n += rational(*str - 'A'); - } - sz += 4; - ++str; - } - if (sz == 0) { - return false; - } - } - else if (strncmp(str, "bv", 2) == 0 && '0' <= *(str + 2) && *(str + 2) <= '9') { - n = rational(0); - str += 2; - while ('0' <= *str && *str <= '9') { - n *= rational(10); - n += rational(*str - '0'); - ++str; - } - if (num_params == 1) { - sz = params[0].get_int(); - } - else { - sz = 32; - } - } - else { - return false; - } - - term = m_bvnum_util.mk_numeral(n, sz); - - return true; - } -}; - - -parser * parser::create(ast_manager& ast_manager, bool ignore_user_patterns) { - return alloc(smtparser, ast_manager, ignore_user_patterns); -} diff --git a/src/parsers/smt/smtparser.h b/src/parsers/smt/smtparser.h deleted file mode 100644 index d8999e8ab..000000000 --- a/src/parsers/smt/smtparser.h +++ /dev/null @@ -1,48 +0,0 @@ -/*++ -Copyright (c) 2006 Microsoft Corporation - -Module Name: - - smtparser.h - -Abstract: - - SMT parsing utilities - -Author: - - Nikolaj Bjorner (nbjorner) 2006-09-25 - -Revision History: - ---*/ -#ifndef SMT_PARSER_H_ -#define SMT_PARSER_H_ - -#include -#include "ast/ast.h" -#include "util/vector.h" -#include "parsers/smt/smtlib.h" - -namespace smtlib { - class parser { - public: - static parser * create(ast_manager & ast_manager, bool ignore_user_patterns = false); - - virtual ~parser() {} - - virtual void add_builtin_op(char const *, family_id fid, decl_kind kind) = 0; - virtual void add_builtin_type(char const *, family_id fid, decl_kind kind) = 0; - - virtual void initialize_smtlib() = 0; - - virtual void set_error_stream(std::ostream& strm) = 0; - - virtual bool parse_file(char const * path) = 0; - virtual bool parse_string(char const * string) = 0; - - virtual benchmark * get_benchmark() = 0; - }; -}; - -#endif diff --git a/src/shell/main.cpp b/src/shell/main.cpp index 3d2609c4f..8b719681c 100644 --- a/src/shell/main.cpp +++ b/src/shell/main.cpp @@ -37,7 +37,7 @@ Revision History: #include "util/env_params.h" #include "shell/lp_frontend.h" -typedef enum { IN_UNSPECIFIED, IN_SMTLIB, IN_SMTLIB_2, IN_DATALOG, IN_DIMACS, IN_WCNF, IN_OPB, IN_Z3_LOG, IN_MPS } input_kind; +typedef enum { IN_UNSPECIFIED, IN_SMTLIB_2, IN_DATALOG, IN_DIMACS, IN_WCNF, IN_OPB, IN_Z3_LOG, IN_MPS } input_kind; std::string g_aux_input_file; char const * g_input_file = 0; @@ -169,9 +169,6 @@ void parse_cmd_line_args(int argc, char ** argv) { std::cout << "\n"; exit(0); } - else if (strcmp(opt_name, "smt") == 0) { - g_input_kind = IN_SMTLIB; - } else if (strcmp(opt_name, "smt2") == 0) { g_input_kind = IN_SMTLIB_2; } @@ -340,9 +337,6 @@ int STD_CALL main(int argc, char ** argv) { else if (strcmp(ext, "smt2") == 0) { g_input_kind = IN_SMTLIB_2; } - else if (strcmp(ext, "smt") == 0) { - g_input_kind = IN_SMTLIB; - } else if (strcmp(ext, "mps") == 0 || strcmp(ext, "sif") == 0 || strcmp(ext, "MPS") == 0 || strcmp(ext, "SIF") == 0) { g_input_kind = IN_MPS; @@ -350,9 +344,6 @@ int STD_CALL main(int argc, char ** argv) { } } switch (g_input_kind) { - case IN_SMTLIB: - return_value = read_smtlib_file(g_input_file); - break; case IN_SMTLIB_2: memory::exit_when_out_of_memory(true, "(error \"out of memory\")"); return_value = read_smtlib2_commands(g_input_file); diff --git a/src/shell/smtlib_frontend.cpp b/src/shell/smtlib_frontend.cpp index 666a1e1fe..8c716a81a 100644 --- a/src/shell/smtlib_frontend.cpp +++ b/src/shell/smtlib_frontend.cpp @@ -21,7 +21,6 @@ Revision History: #include #include #include -#include "parsers/smt/smtlib_solver.h" #include "util/timeout.h" #include "parsers/smt2/smt2parser.h" #include "muz/fp/dl_cmds.h" @@ -35,20 +34,14 @@ Revision History: extern bool g_display_statistics; static clock_t g_start_time; -static smtlib::solver* g_solver = 0; static cmd_context * g_cmd_context = 0; static void display_statistics() { clock_t end_time = clock(); - if ((g_solver || g_cmd_context) && g_display_statistics) { + if (g_cmd_context && g_display_statistics) { std::cout.flush(); std::cerr.flush(); - if (g_solver) { - g_solver->display_statistics(); - memory::display_max_usage(std::cout); - std::cout << "time: " << ((static_cast(end_time) - static_cast(g_start_time)) / CLOCKS_PER_SEC) << " secs\n"; - } - else if (g_cmd_context) { + if (g_cmd_context) { g_cmd_context->set_regular_stream("stdout"); g_cmd_context->display_statistics(true, ((static_cast(end_time) - static_cast(g_start_time)) / CLOCKS_PER_SEC)); } @@ -72,33 +65,6 @@ static void STD_CALL on_ctrl_c(int) { raise(SIGINT); } -unsigned read_smtlib_file(char const * benchmark_file) { - g_start_time = clock(); - register_on_timeout_proc(on_timeout); - signal(SIGINT, on_ctrl_c); - smtlib::solver solver; - g_solver = &solver; - - bool ok = true; - - ok = solver.solve_smt(benchmark_file); - if (!ok) { - if (benchmark_file) { - std::cerr << "ERROR: solving '" << benchmark_file << "'.\n"; - } - else { - std::cerr << "ERROR: solving input stream.\n"; - } - } - - #pragma omp critical (g_display_stats) - { - display_statistics(); - register_on_timeout_proc(0); - g_solver = 0; - } - return solver.get_error_code(); -} unsigned read_smtlib2_commands(char const * file_name) { g_start_time = clock(); diff --git a/src/smt/theory_arith_pp.h b/src/smt/theory_arith_pp.h index 67fe5a572..997698411 100644 --- a/src/smt/theory_arith_pp.h +++ b/src/smt/theory_arith_pp.h @@ -526,7 +526,7 @@ namespace smt { } } } - pp.display(out, m.mk_true()); + pp.display_smt2(out, m.mk_true()); } template diff --git a/src/test/expr_rand.cpp b/src/test/expr_rand.cpp index f1b20ba8e..e52bfbc1a 100644 --- a/src/test/expr_rand.cpp +++ b/src/test/expr_rand.cpp @@ -40,10 +40,10 @@ void tst_expr_arith(unsigned num_files) { pp.set_logic(symbol("QF_AUFLIA")); std::ostringstream buffer; - buffer << "random_arith_" << i << ".smt"; + buffer << "random_arith_" << i << ".smt2"; std::cout << buffer.str() << "\n"; std::ofstream file(buffer.str().c_str()); - pp.display(file, e.get()); + pp.display_smt2(file, e.get()); file.close(); } @@ -83,10 +83,10 @@ void tst_expr_rand(unsigned num_files) { pp.set_logic(symbol("QF_AUFBV")); std::ostringstream buffer; - buffer << "random_bv_" << i << ".smt"; + buffer << "random_bv_" << i << ".smt2"; std::cout << buffer.str() << "\n"; std::ofstream file(buffer.str().c_str()); - pp.display(file, e.get()); + pp.display_smt2(file, e.get()); file.close(); } diff --git a/src/test/quant_elim.cpp b/src/test/quant_elim.cpp index 3674e6b70..12fca706d 100644 --- a/src/test/quant_elim.cpp +++ b/src/test/quant_elim.cpp @@ -8,8 +8,6 @@ Copyright (c) 2015 Microsoft Corporation #include "smt/params/smt_params.h" #include "qe/qe.h" #include "ast/ast_pp.h" -#include "parsers/smt/smtlib.h" -#include "parsers/smt/smtparser.h" #include "util/lbool.h" #include #include "ast/reg_decl_plugins.h" @@ -54,6 +52,9 @@ static void test_qe(ast_manager& m, lbool expected_outcome, expr* fml, char cons static void test_formula(lbool expected_outcome, char const* fml) { ast_manager m; reg_decl_plugins(m); + // No-op requires SMTLIB2 + +#if 0 scoped_ptr parser = smtlib::parser::create(m); parser->initialize_smtlib(); @@ -73,8 +74,10 @@ static void test_formula(lbool expected_outcome, char const* fml) { for (; it != end; ++it) { test_qe(m, expected_outcome, *it, 0); } +#endif } + void tst_quant_elim() { disable_debug("heap");