3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-05 09:04:07 +00:00

Added utility to compare quantifier instantiation profiles generated via smt.qi.profile=true

This commit is contained in:
Christoph M. Wintersteiger 2017-04-06 18:37:29 +01:00
parent 7d35fcb17e
commit d390885757
4 changed files with 404 additions and 0 deletions

View file

@ -0,0 +1,7 @@
qprofdiff: main.cpp
$(CXX) $(CXXFLAGS) main.cpp -o qprofdiff
all: qprofdiff
clean:
rm -f qprofdiff

238
contrib/qprofdiff/main.cpp Normal file
View file

@ -0,0 +1,238 @@
/*++
Copyright (c) 2017 Microsoft Corporation
Module Name:
main.cpp
Abstract:
Main file for qprofdiff.
Author:
Christoph M. Wintersteiger (cwinter)
Revision History:
--*/
#include<errno.h>
#include<string>
#include<iostream>
#include<fstream>
#include<map>
#include<vector>
#include<set>
#include<algorithm>
using namespace std;
set<string> options;
// Profile format:
// [quantifier_instances] qname : num_instances : max_generation : max_cost_s
const string prefix = "[quantifier_instances]";
unsigned prefix_len = prefix.length();
typedef struct { unsigned num_instances, max_generation, max_cost; } map_entry;
string trim(string str) {
size_t linx = str.find_first_not_of(' ');
size_t rinx = str.find_last_not_of(' ');
return str.substr(linx, rinx-linx+1);
}
int parse(string const & filename, map<string, map_entry> & data) {
ifstream fs(filename.c_str());
if (!fs.is_open()) {
cout << "Can't open file '" << filename << "'" << endl;
return ENOENT;
}
string qid;
string tokens[4];
unsigned cur_token = 0;
while (!fs.eof()) {
string line;
getline(fs, line);
if (line.substr(0, prefix_len) == prefix) {
line = trim(line.substr(prefix_len));
size_t from = 0, ti = 0;
for (size_t inx = line.find(':', from);
inx != string::npos;
inx = line.find(':', from)) {
tokens[ti] = trim(line.substr(from, inx-from));
from = inx+1;
ti++;
}
if (from != line.length() && ti < 4)
tokens[ti] = trim(line.substr(from));
qid = tokens[0];
if (data.find(qid) == data.end()) {
map_entry & entry = data[qid];
entry.num_instances = entry.max_generation = entry.max_cost = 0;
}
map_entry & entry = data[qid];
entry.num_instances += atoi(tokens[1].c_str());
entry.max_generation = std::max(entry.max_generation, (unsigned)atoi(tokens[2].c_str()));
entry.max_cost = max(entry.max_cost, (unsigned)atoi(tokens[3].c_str()));
}
}
fs.close();
return 0;
}
void display_data(map<string, map_entry> & data) {
for (map<string, map_entry>::iterator it = data.begin();
it != data.end();
it++)
cout << it->first << ": " << it->second.num_instances <<
", " << it->second.max_generation <<
", " << it->second.max_cost << endl;
}
typedef struct { int d_num_instances, d_max_generation, d_max_cost; } diff_entry;
typedef struct { string qid; diff_entry e; } diff_item;
bool diff_item_lt_inst(diff_item const & l, diff_item const & r) {
return l.e.d_num_instances < r.e.d_num_instances;
}
bool diff_item_lt_gen(diff_item const & l, diff_item const & r) {
return l.e.d_max_generation< r.e.d_max_generation;
}
bool diff_item_lt_cost(diff_item const & l, diff_item const & r) {
return l.e.d_max_cost < r.e.d_max_cost;
}
void display_indicator(int const & delta, bool suppress_unchanged) {
if (delta < 0)
cout << "+ ";
else if (delta > 0)
cout << "- ";
else if (delta == 0 && !suppress_unchanged)
cout << "= ";
}
void diff(map<string, map_entry> & left, map<string, map_entry> & right) {
map<string, diff_entry> diff_data;
for (map<string, map_entry>::const_iterator lit = left.begin();
lit != left.end();
lit++) {
string const & qid = lit->first;
map_entry const & lentry = lit->second;
map<string, map_entry>::const_iterator rit = right.find(qid);
if (rit != right.end()) {
map_entry const & rentry = rit->second;
diff_entry & de = diff_data[qid];
de.d_num_instances = lentry.num_instances - rentry.num_instances;
de.d_max_generation = lentry.max_generation - rentry.max_generation;
de.d_max_cost = lentry.max_cost - rentry.max_cost;
}
}
vector<diff_item> flat_data;
for (map<string, diff_entry>::const_iterator it = diff_data.begin();
it != diff_data.end();
it++) {
flat_data.push_back(diff_item());
flat_data.back().qid = it->first;
flat_data.back().e = it->second;
}
stable_sort(flat_data.begin(), flat_data.end(),
options.find("-si") != options.end() ? diff_item_lt_inst :
options.find("-sg") != options.end() ? diff_item_lt_gen :
options.find("-sc") != options.end() ? diff_item_lt_cost :
diff_item_lt_inst);
bool suppress_unchanged = options.find("-n") != options.end();
for (vector<diff_item>::const_iterator it = flat_data.begin();
it != flat_data.end();
it++) {
diff_item const & d = *it;
string const & qid = d.qid;
diff_entry const & e = d.e;
int const & delta =
(options.find("-si") != options.end()) ? e.d_num_instances :
(options.find("-sg") != options.end()) ? e.d_max_generation :
(options.find("-sc") != options.end()) ? e.d_max_cost :
e.d_num_instances;
display_indicator(delta, suppress_unchanged);
if (delta != 0 || !suppress_unchanged)
cout << qid << " (" <<
(e.d_num_instances > 0 ? "" : "+") << -e.d_num_instances << " inst., " <<
(e.d_max_generation > 0 ? "" : "+") << -e.d_max_generation << " max. gen., " <<
(e.d_max_cost > 0 ? "" : "+") << -e.d_max_cost << " max. cost)" <<
endl;
}
}
void display_usage() {
cout << "Usage: qprofdiff [options] <filename> <filename>" << endl;
cout << "Options:" << endl;
cout << " -n Suppress unchanged items" << endl;
cout << " -si Sort by difference in number of instances" << endl;
cout << " -sg Sort by difference in max. generation" << endl;
cout << " -sc Sort by difference in max. cost" << endl;
}
int main(int argc, char ** argv) {
char * filename1 = 0;
char * filename2 = 0;
for (int i = 1; i < argc; i++) {
int len = string(argv[i]).length();
if (len > 1 && argv[i][0] == '-') {
options.insert(string(argv[i]));
}
else if (filename1 == 0)
filename1 = argv[i];
else if (filename2 == 0)
filename2 = argv[i];
else {
cout << "Invalid argument: " << argv[i] << endl << endl;
display_usage();
return EINVAL;
}
}
if (filename1 == 0 || filename2 == 0) {
cout << "Two filenames required." << endl << endl;
display_usage();
return EINVAL;
}
cout << "Comparing " << filename1 << " to " << filename2 << endl;
map<string, map_entry> data1, data2;
int r = parse(filename1, data1);
if (r != 0) return r;
r = parse(filename2, data2);
if (r != 0) return r;
// display_data(data1);
// display_data(data2);
diff(data1, data2);
return 0;
}

View file

@ -0,0 +1,137 @@
<?xml version="1.0" encoding="utf-8"?>
<Project DefaultTargets="Build" ToolsVersion="15.0" xmlns="http://schemas.microsoft.com/developer/msbuild/2003">
<ItemGroup Label="ProjectConfigurations">
<ProjectConfiguration Include="Debug|Win32">
<Configuration>Debug</Configuration>
<Platform>Win32</Platform>
</ProjectConfiguration>
<ProjectConfiguration Include="Release|Win32">
<Configuration>Release</Configuration>
<Platform>Win32</Platform>
</ProjectConfiguration>
<ProjectConfiguration Include="Debug|x64">
<Configuration>Debug</Configuration>
<Platform>x64</Platform>
</ProjectConfiguration>
<ProjectConfiguration Include="Release|x64">
<Configuration>Release</Configuration>
<Platform>x64</Platform>
</ProjectConfiguration>
</ItemGroup>
<PropertyGroup Label="Globals">
<VCProjectVersion>15.0</VCProjectVersion>
<ProjectGuid>{96E7E3EF-4162-474D-BD32-C702632AAF2B}</ProjectGuid>
<RootNamespace>qprofdiff</RootNamespace>
<WindowsTargetPlatformVersion>8.1</WindowsTargetPlatformVersion>
</PropertyGroup>
<Import Project="$(VCTargetsPath)\Microsoft.Cpp.Default.props" />
<PropertyGroup Condition="'$(Configuration)|$(Platform)'=='Debug|Win32'" Label="Configuration">
<ConfigurationType>Application</ConfigurationType>
<UseDebugLibraries>true</UseDebugLibraries>
<PlatformToolset>v141</PlatformToolset>
<CharacterSet>NotSet</CharacterSet>
</PropertyGroup>
<PropertyGroup Condition="'$(Configuration)|$(Platform)'=='Release|Win32'" Label="Configuration">
<ConfigurationType>Application</ConfigurationType>
<UseDebugLibraries>false</UseDebugLibraries>
<PlatformToolset>v141</PlatformToolset>
<WholeProgramOptimization>true</WholeProgramOptimization>
<CharacterSet>MultiByte</CharacterSet>
</PropertyGroup>
<PropertyGroup Condition="'$(Configuration)|$(Platform)'=='Debug|x64'" Label="Configuration">
<ConfigurationType>Application</ConfigurationType>
<UseDebugLibraries>true</UseDebugLibraries>
<PlatformToolset>v141</PlatformToolset>
<CharacterSet>MultiByte</CharacterSet>
</PropertyGroup>
<PropertyGroup Condition="'$(Configuration)|$(Platform)'=='Release|x64'" Label="Configuration">
<ConfigurationType>Application</ConfigurationType>
<UseDebugLibraries>false</UseDebugLibraries>
<PlatformToolset>v141</PlatformToolset>
<WholeProgramOptimization>true</WholeProgramOptimization>
<CharacterSet>MultiByte</CharacterSet>
</PropertyGroup>
<Import Project="$(VCTargetsPath)\Microsoft.Cpp.props" />
<ImportGroup Label="ExtensionSettings">
</ImportGroup>
<ImportGroup Label="Shared">
</ImportGroup>
<ImportGroup Label="PropertySheets" Condition="'$(Configuration)|$(Platform)'=='Debug|Win32'">
<Import Project="$(UserRootDir)\Microsoft.Cpp.$(Platform).user.props" Condition="exists('$(UserRootDir)\Microsoft.Cpp.$(Platform).user.props')" Label="LocalAppDataPlatform" />
</ImportGroup>
<ImportGroup Label="PropertySheets" Condition="'$(Configuration)|$(Platform)'=='Release|Win32'">
<Import Project="$(UserRootDir)\Microsoft.Cpp.$(Platform).user.props" Condition="exists('$(UserRootDir)\Microsoft.Cpp.$(Platform).user.props')" Label="LocalAppDataPlatform" />
</ImportGroup>
<ImportGroup Label="PropertySheets" Condition="'$(Configuration)|$(Platform)'=='Debug|x64'">
<Import Project="$(UserRootDir)\Microsoft.Cpp.$(Platform).user.props" Condition="exists('$(UserRootDir)\Microsoft.Cpp.$(Platform).user.props')" Label="LocalAppDataPlatform" />
</ImportGroup>
<ImportGroup Label="PropertySheets" Condition="'$(Configuration)|$(Platform)'=='Release|x64'">
<Import Project="$(UserRootDir)\Microsoft.Cpp.$(Platform).user.props" Condition="exists('$(UserRootDir)\Microsoft.Cpp.$(Platform).user.props')" Label="LocalAppDataPlatform" />
</ImportGroup>
<PropertyGroup Label="UserMacros" />
<PropertyGroup Condition="'$(Configuration)|$(Platform)'=='Debug|Win32'">
<IncludePath>$(IncludePath)</IncludePath>
<LibraryPath>$(LibraryPath)</LibraryPath>
</PropertyGroup>
<PropertyGroup Condition="'$(Configuration)|$(Platform)'=='Release|Win32'">
<IncludePath>$(IncludePath)</IncludePath>
<LibraryPath>$(LibraryPath)</LibraryPath>
</PropertyGroup>
<ItemDefinitionGroup Condition="'$(Configuration)|$(Platform)'=='Debug|Win32'">
<ClCompile>
<WarningLevel>Level3</WarningLevel>
<Optimization>Disabled</Optimization>
<SDLCheck>true</SDLCheck>
<RuntimeLibrary>MultiThreadedDebugDLL</RuntimeLibrary>
<AdditionalIncludeDirectories>..\..\src\util;%(AdditionalIncludeDirectories)</AdditionalIncludeDirectories>
<MultiProcessorCompilation>
</MultiProcessorCompilation>
<DebugInformationFormat>ProgramDatabase</DebugInformationFormat>
</ClCompile>
<Link>
<AdditionalLibraryDirectories>$(LibraryPath);%(AdditionalLibraryDirectories)</AdditionalLibraryDirectories>
</Link>
</ItemDefinitionGroup>
<ItemDefinitionGroup Condition="'$(Configuration)|$(Platform)'=='Debug|x64'">
<ClCompile>
<WarningLevel>Level3</WarningLevel>
<Optimization>Disabled</Optimization>
<SDLCheck>true</SDLCheck>
<AdditionalIncludeDirectories>..\..\src\util;%(AdditionalIncludeDirectories)</AdditionalIncludeDirectories>
</ClCompile>
</ItemDefinitionGroup>
<ItemDefinitionGroup Condition="'$(Configuration)|$(Platform)'=='Release|Win32'">
<ClCompile>
<WarningLevel>Level3</WarningLevel>
<Optimization>MaxSpeed</Optimization>
<FunctionLevelLinking>true</FunctionLevelLinking>
<IntrinsicFunctions>true</IntrinsicFunctions>
<SDLCheck>true</SDLCheck>
<AdditionalIncludeDirectories>..\..\src\util;%(AdditionalIncludeDirectories)</AdditionalIncludeDirectories>
</ClCompile>
<Link>
<EnableCOMDATFolding>true</EnableCOMDATFolding>
<OptimizeReferences>true</OptimizeReferences>
</Link>
</ItemDefinitionGroup>
<ItemDefinitionGroup Condition="'$(Configuration)|$(Platform)'=='Release|x64'">
<ClCompile>
<WarningLevel>Level3</WarningLevel>
<Optimization>MaxSpeed</Optimization>
<FunctionLevelLinking>true</FunctionLevelLinking>
<IntrinsicFunctions>true</IntrinsicFunctions>
<SDLCheck>true</SDLCheck>
<AdditionalIncludeDirectories>..\..\src\util;%(AdditionalIncludeDirectories)</AdditionalIncludeDirectories>
</ClCompile>
<Link>
<EnableCOMDATFolding>true</EnableCOMDATFolding>
<OptimizeReferences>true</OptimizeReferences>
</Link>
</ItemDefinitionGroup>
<ItemGroup>
<ClCompile Include="main.cpp" />
</ItemGroup>
<Import Project="$(VCTargetsPath)\Microsoft.Cpp.targets" />
<ImportGroup Label="ExtensionTargets">
</ImportGroup>
</Project>

View file

@ -0,0 +1,22 @@
<?xml version="1.0" encoding="utf-8"?>
<Project ToolsVersion="4.0" xmlns="http://schemas.microsoft.com/developer/msbuild/2003">
<ItemGroup>
<Filter Include="Source Files">
<UniqueIdentifier>{4FC737F1-C7A5-4376-A066-2A32D752A2FF}</UniqueIdentifier>
<Extensions>cpp;c;cc;cxx;def;odl;idl;hpj;bat;asm;asmx</Extensions>
</Filter>
<Filter Include="Header Files">
<UniqueIdentifier>{93995380-89BD-4b04-88EB-625FBE52EBFB}</UniqueIdentifier>
<Extensions>h;hh;hpp;hxx;hm;inl;inc;xsd</Extensions>
</Filter>
<Filter Include="Resource Files">
<UniqueIdentifier>{67DA6AB6-F800-4c08-8B7A-83BB121AAD01}</UniqueIdentifier>
<Extensions>rc;ico;cur;bmp;dlg;rc2;rct;bin;rgs;gif;jpg;jpeg;jpe;resx;tiff;tif;png;wav;mfcribbon-ms</Extensions>
</Filter>
</ItemGroup>
<ItemGroup>
<ClCompile Include="main.cpp">
<Filter>Source Files</Filter>
</ClCompile>
</ItemGroup>
</Project>