3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 20:18:18 +00:00

Merge branch 'master' of /home/leo/projects-bare/z3

This commit is contained in:
Leonardo de Moura 2012-10-05 15:38:06 -07:00
commit 06a08da81b
8 changed files with 933 additions and 953 deletions

View file

@ -1,3 +0,0 @@
<?xml version="1.0" encoding="utf-8"?>
<Project ToolsVersion="4.0" xmlns="http://schemas.microsoft.com/developer/msbuild/2003">
</Project>

View file

@ -1,3 +0,0 @@
<?xml version="1.0" encoding="utf-8"?>
<Project ToolsVersion="4.0" xmlns="http://schemas.microsoft.com/developer/msbuild/2003">
</Project>

View file

@ -1,3 +0,0 @@
<?xml version="1.0" encoding="utf-8"?>
<Project ToolsVersion="4.0" xmlns="http://schemas.microsoft.com/developer/msbuild/2003">
</Project>

View file

@ -581,10 +581,11 @@ br_status poly_rewriter<Config>::mk_nflat_add_core(unsigned num_args, expr * con
hoist_cmul(new_args); hoist_cmul(new_args);
} }
else if (m_sort_sums) { else if (m_sort_sums) {
TRACE("sort_sums_bug", tout << "new_args.size(): " << new_args.size() << "\n";);
if (c.is_zero()) if (c.is_zero())
std::sort(new_args.c_ptr(), new_args.c_ptr() + new_args.size(), ast_to_lt()); std::sort(new_args.c_ptr(), new_args.c_ptr() + new_args.size(), ast_to_lt());
else else
std::sort(new_args.c_ptr() + 1, new_args.c_ptr() + new_args.size() - 1, ast_to_lt()); std::sort(new_args.c_ptr() + 1, new_args.c_ptr() + new_args.size(), ast_to_lt());
} }
result = mk_add_app(new_args.size(), new_args.c_ptr()); result = mk_add_app(new_args.size(), new_args.c_ptr());
if (hoist_multiplication(result)) { if (hoist_multiplication(result)) {
@ -616,7 +617,7 @@ br_status poly_rewriter<Config>::mk_nflat_add_core(unsigned num_args, expr * con
if (c.is_zero()) if (c.is_zero())
std::sort(new_args.c_ptr(), new_args.c_ptr() + new_args.size(), ast_to_lt()); std::sort(new_args.c_ptr(), new_args.c_ptr() + new_args.size(), ast_to_lt());
else else
std::sort(new_args.c_ptr() + 1, new_args.c_ptr() + new_args.size() - 1, ast_to_lt()); std::sort(new_args.c_ptr() + 1, new_args.c_ptr() + new_args.size(), ast_to_lt());
} }
result = mk_add_app(new_args.size(), new_args.c_ptr()); result = mk_add_app(new_args.size(), new_args.c_ptr());
if (hoist_multiplication(result)) { if (hoist_multiplication(result)) {

View file

@ -1,3 +0,0 @@
<?xml version="1.0" encoding="utf-8"?>
<Project ToolsVersion="4.0" xmlns="http://schemas.microsoft.com/developer/msbuild/2003">
</Project>

View file

@ -1,3 +0,0 @@
<?xml version="1.0" encoding="utf-8"?>
<Project ToolsVersion="4.0" xmlns="http://schemas.microsoft.com/developer/msbuild/2003">
</Project>

View file

@ -1,3 +0,0 @@
<?xml version="1.0" encoding="utf-8"?>
<Project ToolsVersion="4.0" xmlns="http://schemas.microsoft.com/developer/msbuild/2003">
</Project>

View file

@ -1,3 +0,0 @@
<?xml version="1.0" encoding="utf-8"?>
<Project ToolsVersion="4.0" xmlns="http://schemas.microsoft.com/developer/msbuild/2003">
</Project>