mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 17:44:08 +00:00
Code Activity

fix issues found in parsing examples

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-12-01 14:43:52 -08:00
parent 274279b251
commit 0bfea99cff
4 changed files with 10 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
examples/c++/example.cpp
View file

@ -1139,7 +1139,7 @@ static void parse_example() {
expr a = c.parse_string("(assert a)", sorts, decls); expr a = c.parse_string("(assert a)", sorts, decls);
std::cout << a << "\n"; std::cout << a << "\n";
expr b = c.parse_string("(benchmark tst :extrafuns ((x Int) (y Int)) :formula (> x y) :formula (> x 0))"); // expr b = c.parse_string("(benchmark tst :extrafuns ((x Int) (y Int)) :formula (> x y) :formula (> x 0))");
} }

4
examples/dotnet/Program.cs
View file

@ -1383,7 +1383,7 @@ namespace test_mapi
{ {
Console.WriteLine("ParserExample1"); Console.WriteLine("ParserExample1");
var fml = ctx.ParseSMTLIB2String("(benchmark tst :extrafuns ((x Int) (y Int)) :formula (> x y) :formula (> x 0))"); var fml = ctx.ParseSMTLIB2String("(declare-const x Int) (declare-const y Int) (assert (> x y)) (assert (> x 0))");
Console.WriteLine("formula {0}", fml); Console.WriteLine("formula {0}", fml);
Model m = Check(ctx, fml, Status.SATISFIABLE); Model m = Check(ctx, fml, Status.SATISFIABLE);
@ -1417,7 +1417,7 @@ namespace test_mapi
BoolExpr ca = CommAxiom(ctx, g); BoolExpr ca = CommAxiom(ctx, g);
BoolExpr thm = ctx.ParseSMTLIB2String("(assert (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, null, null,
new Symbol[] { ctx.MkSymbol("gg") }, new Symbol[] { ctx.MkSymbol("gg") },
new FuncDecl[] { g }); new FuncDecl[] { g });

8
src/api/api_parsers.cpp
View file

@ -52,8 +52,12 @@ extern "C" {
ctx->insert(to_symbol(decl_names[i]), to_func_decl(decls[i])); ctx->insert(to_symbol(decl_names[i]), to_func_decl(decls[i]));
} }
for (unsigned i = 0; i < num_sorts; ++i) { for (unsigned i = 0; i < num_sorts; ++i) {
psort* ps = ctx->pm().mk_psort_cnst(to_sort(sorts[i])); sort* srt = to_sort(sorts[i]);
ctx->insert(ctx->pm().mk_psort_user_decl(0, to_symbol(sort_names[i]), ps)); 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));
}
} }
std::stringstream errstrm; std::stringstream errstrm;
ctx->set_regular_stream(errstrm); ctx->set_regular_stream(errstrm);

1
src/cmd_context/pdecl.cpp
View file

@ -853,6 +853,7 @@ pdecl_manager::~pdecl_manager() {
dec_ref(m_list); dec_ref(m_list);
reset_sort_info(); reset_sort_info();
SASSERT(m_sort2psort.empty()); SASSERT(m_sort2psort.empty());
SASSERT(m_table.empty());
} }
psort * pdecl_manager::mk_psort_cnst(sort * s) { psort * pdecl_manager::mk_psort_cnst(sort * s) {