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

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

Browse source
This commit is contained in:
Nikolaj Bjorner 2017-04-25 10:30:16 -07:00
parent bd8b0186d6 049cb957ea
commit dedc130e98
54 changed files with 1755 additions and 915 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
README.md
View file

@ -53,8 +53,8 @@ make
sudo make install
```
Note by default ``gcc`` is used as the C++ compiler if it is available. If you
would prefer to use Clang change the ``mk_make.py`` line to
Note by default ``g++`` is used as the C++ compiler if it is available. If you
would prefer to use Clang change the ``mk_make.py`` invocation to:
```bash
CXX=clang++ CC=clang python scripts/mk_make.py

7
contrib/qprofdiff/Makefile Normal file
View file

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

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

@ -0,0 +1,284 @@
/*++
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<limits.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 = (unsigned)atoi(tokens[2].c_str());
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;
bool left_only, right_only;
} diff_entry;
typedef struct { string qid; diff_entry e; } diff_item;
#define DIFF_LT(X) bool diff_item_lt_ ## X (diff_item const & l, diff_item const & r) { \
int l_lt_r = l.e.d_ ## X < r.e.d_ ## X; \
int l_eq_r = l.e.d_ ## X == r.e.d_ ## X; \
return \
l.e.left_only ? (r.e.left_only ? ((l_eq_r) ? l.qid < r.qid : l_lt_r) : false) : \
l.e.right_only ? (r.e.right_only ? ((l_eq_r) ? l.qid < r.qid : l_lt_r) : true) : \
r.e.right_only ? false : \
r.e.left_only ? true : \
l_lt_r; \
}
DIFF_LT(num_instances)
DIFF_LT(max_generation)
DIFF_LT(max_cost)
int indicate(diff_entry const & e, bool suppress_unchanged) {
if (e.left_only) {
cout << "< ";
return INT_MIN;
}
else if (e.right_only) {
cout << "> ";
return INT_MAX;
}
else {
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;
if (delta < 0)
cout << "+ ";
else if (delta > 0)
cout << "- ";
else if (delta == 0 && !suppress_unchanged)
cout << "= ";
return delta;
}
}
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.left_only = de.right_only = false;
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;
}
else {
diff_entry & de = diff_data[qid];
de.left_only = true;
de.right_only = false;
de.d_num_instances = lentry.num_instances;
de.d_max_generation = lentry.max_generation;
de.d_max_cost = lentry.max_cost;
}
}
for (map<string, map_entry>::const_iterator rit = right.begin();
rit != right.end();
rit++) {
string const & qid = rit->first;
map_entry const & rentry = rit->second;
map<string, map_entry>::const_iterator lit = left.find(qid);
if (lit == left.end()) {
diff_entry & de = diff_data[qid];
de.left_only = false;
de.right_only = true;
de.d_num_instances = -(int)rentry.num_instances;
de.d_max_generation = -(int)rentry.max_generation;
de.d_max_cost = -(int)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_num_instances:
options.find("-sg") != options.end() ? diff_item_lt_max_generation :
options.find("-sc") != options.end() ? diff_item_lt_max_cost :
diff_item_lt_num_instances);
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 delta = indicate(e, 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;
}

3
contrib/qprofdiff/maintainers.txt Normal file
View file

@ -0,0 +1,3 @@
# Maintainers
- Christoph M. Wintersteiger (@wintersteiger, cwinter@microsoft.com)

137
contrib/qprofdiff/qprofdiff.vcxproj Normal file
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>

22
contrib/qprofdiff/qprofdiff.vcxproj.filters Normal file
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>

2
src/api/api_opt.cpp
View file

@ -128,7 +128,7 @@ extern "C" {
lbool r = l_undef;
cancel_eh<reslimit> eh(mk_c(c)->m().limit());
unsigned timeout = to_optimize_ptr(o)->get_params().get_uint("timeout", mk_c(c)->get_timeout());
unsigned rlimit = mk_c(c)->get_rlimit();
unsigned rlimit = to_optimize_ptr(o)->get_params().get_uint("rlimit", mk_c(c)->get_rlimit());
api::context::set_interruptable si(*(mk_c(c)), eh);
{
scoped_timer timer(timeout, &eh);

2
src/api/c++/z3++.h
View file

@ -2244,7 +2244,7 @@ namespace z3 {
void from_file(char const* s) { Z3_fixedpoint_from_file(ctx(), m_fp, s); check_error(); }
void add_rule(expr& rule, symbol const& name) { Z3_fixedpoint_add_rule(ctx(), m_fp, rule, name); check_error(); }
void add_fact(func_decl& f, unsigned * args) { Z3_fixedpoint_add_fact(ctx(), m_fp, f, f.arity(), args); check_error(); }
check_result query(expr& q) { Z3_lbool r = Z3_fixedpoint_query(ctx(), m_fp, q); check_error(); to_check_result(r); }
check_result query(expr& q) { Z3_lbool r = Z3_fixedpoint_query(ctx(), m_fp, q); check_error(); return to_check_result(r); }
check_result query(func_decl_vector& relations) {
array<Z3_func_decl> rs(relations);
Z3_lbool r = Z3_fixedpoint_query_relations(ctx(), m_fp, rs.size(), rs.ptr());

165
src/api/java/Context.java
View file

@ -1890,43 +1890,43 @@ public class Context implements AutoCloseable {
/**
* Create the empty sequence.
*/
public SeqExpr MkEmptySeq(Sort s)
public SeqExpr mkEmptySeq(Sort s)
{
checkContextMatch(s);
return new SeqExpr(this, Native.mkSeqEmpty(nCtx(), s.getNativeObject()));
return (SeqExpr) Expr.create(this, Native.mkSeqEmpty(nCtx(), s.getNativeObject()));
}
/**
* Create the singleton sequence.
*/
public SeqExpr MkUnit(Expr elem)
public SeqExpr mkUnit(Expr elem)
{
checkContextMatch(elem);
return new SeqExpr(this, Native.mkSeqUnit(nCtx(), elem.getNativeObject()));
return (SeqExpr) Expr.create(this, Native.mkSeqUnit(nCtx(), elem.getNativeObject()));
}
/**
* Create a string constant.
*/
public SeqExpr MkString(String s)
public SeqExpr mkString(String s)
{
return new SeqExpr(this, Native.mkString(nCtx(), s));
return (SeqExpr) Expr.create(this, Native.mkString(nCtx(), s));
}
/**
* Concatentate sequences.
*/
public SeqExpr MkConcat(SeqExpr... t)
public SeqExpr mkConcat(SeqExpr... t)
{
checkContextMatch(t);
return new SeqExpr(this, Native.mkSeqConcat(nCtx(), t.length, AST.arrayToNative(t)));
return (SeqExpr) Expr.create(this, Native.mkSeqConcat(nCtx(), t.length, AST.arrayToNative(t)));
}
/**
* Retrieve the length of a given sequence.
*/
public IntExpr MkLength(SeqExpr s)
public IntExpr mkLength(SeqExpr s)
{
checkContextMatch(s);
return (IntExpr) Expr.create(this, Native.mkSeqLength(nCtx(), s.getNativeObject()));
@ -1935,130 +1935,221 @@ public class Context implements AutoCloseable {
/**
* Check for sequence prefix.
*/
public BoolExpr MkPrefixOf(SeqExpr s1, SeqExpr s2)
public BoolExpr mkPrefixOf(SeqExpr s1, SeqExpr s2)
{
checkContextMatch(s1, s2);
return new BoolExpr(this, Native.mkSeqPrefix(nCtx(), s1.getNativeObject(), s2.getNativeObject()));
return (BoolExpr) Expr.create(this, Native.mkSeqPrefix(nCtx(), s1.getNativeObject(), s2.getNativeObject()));
}
/**
* Check for sequence suffix.
*/
public BoolExpr MkSuffixOf(SeqExpr s1, SeqExpr s2)
public BoolExpr mkSuffixOf(SeqExpr s1, SeqExpr s2)
{
checkContextMatch(s1, s2);
return new BoolExpr(this, Native.mkSeqSuffix(nCtx(), s1.getNativeObject(), s2.getNativeObject()));
return (BoolExpr)Expr.create(this, Native.mkSeqSuffix(nCtx(), s1.getNativeObject(), s2.getNativeObject()));
}
/**
* Check for sequence containment of s2 in s1.
*/
public BoolExpr MkContains(SeqExpr s1, SeqExpr s2)
public BoolExpr mkContains(SeqExpr s1, SeqExpr s2)
{
checkContextMatch(s1, s2);
return new BoolExpr(this, Native.mkSeqContains(nCtx(), s1.getNativeObject(), s2.getNativeObject()));
return (BoolExpr) Expr.create(this, Native.mkSeqContains(nCtx(), s1.getNativeObject(), s2.getNativeObject()));
}
/**
* Retrieve sequence of length one at index.
*/
public SeqExpr MkAt(SeqExpr s, IntExpr index)
public SeqExpr mkAt(SeqExpr s, IntExpr index)
{
checkContextMatch(s, index);
return new SeqExpr(this, Native.mkSeqAt(nCtx(), s.getNativeObject(), index.getNativeObject()));
return (SeqExpr) Expr.create(this, Native.mkSeqAt(nCtx(), s.getNativeObject(), index.getNativeObject()));
}
/**
* Extract subsequence.
*/
public SeqExpr MkExtract(SeqExpr s, IntExpr offset, IntExpr length)
public SeqExpr mkExtract(SeqExpr s, IntExpr offset, IntExpr length)
{
checkContextMatch(s, offset, length);
return new SeqExpr(this, Native.mkSeqExtract(nCtx(), s.getNativeObject(), offset.getNativeObject(), length.getNativeObject()));
return (SeqExpr) Expr.create(this, Native.mkSeqExtract(nCtx(), s.getNativeObject(), offset.getNativeObject(), length.getNativeObject()));
}
/**
* Extract index of sub-string starting at offset.
*/
public IntExpr MkIndexOf(SeqExpr s, SeqExpr substr, ArithExpr offset)
public IntExpr mkIndexOf(SeqExpr s, SeqExpr substr, ArithExpr offset)
{
checkContextMatch(s, substr, offset);
return new IntExpr(this, Native.mkSeqIndex(nCtx(), s.getNativeObject(), substr.getNativeObject(), offset.getNativeObject()));
return (IntExpr)Expr.create(this, Native.mkSeqIndex(nCtx(), s.getNativeObject(), substr.getNativeObject(), offset.getNativeObject()));
}
/**
* Replace the first occurrence of src by dst in s.
*/
public SeqExpr MkReplace(SeqExpr s, SeqExpr src, SeqExpr dst)
public SeqExpr mkReplace(SeqExpr s, SeqExpr src, SeqExpr dst)
{
checkContextMatch(s, src, dst);
return new SeqExpr(this, Native.mkSeqReplace(nCtx(), s.getNativeObject(), src.getNativeObject(), dst.getNativeObject()));
return (SeqExpr) Expr.create(this, Native.mkSeqReplace(nCtx(), s.getNativeObject(), src.getNativeObject(), dst.getNativeObject()));
}
/**
* Convert a regular expression that accepts sequence s.
*/
public ReExpr MkToRe(SeqExpr s)
public ReExpr mkToRe(SeqExpr s)
{
checkContextMatch(s);
return new ReExpr(this, Native.mkSeqToRe(nCtx(), s.getNativeObject()));
return (ReExpr) Expr.create(this, Native.mkSeqToRe(nCtx(), s.getNativeObject()));
}
/**
* Check for regular expression membership.
*/
public BoolExpr MkInRe(SeqExpr s, ReExpr re)
public BoolExpr mkInRe(SeqExpr s, ReExpr re)
{
checkContextMatch(s, re);
return new BoolExpr(this, Native.mkSeqInRe(nCtx(), s.getNativeObject(), re.getNativeObject()));
return (BoolExpr) Expr.create(this, Native.mkSeqInRe(nCtx(), s.getNativeObject(), re.getNativeObject()));
}
/**
* Take the Kleene star of a regular expression.
*/
public ReExpr MkStar(ReExpr re)
public ReExpr mkStar(ReExpr re)
{
checkContextMatch(re);
return new ReExpr(this, Native.mkReStar(nCtx(), re.getNativeObject()));
return (ReExpr) Expr.create(this, Native.mkReStar(nCtx(), re.getNativeObject()));
}
/**
* Take the lower and upper-bounded Kleene star of a regular expression.
*/
public ReExpr mkLoop(ReExpr re, int lo, int hi)
{
return (ReExpr) Expr.create(this, Native.mkReLoop(nCtx(), re.getNativeObject(), lo, hi));
}
/**
* Take the lower-bounded Kleene star of a regular expression.
*/
public ReExpr mkLoop(ReExpr re, int lo)
{
return (ReExpr) Expr.create(this, Native.mkReLoop(nCtx(), re.getNativeObject(), lo, 0));
}
/**
* Take the Kleene plus of a regular expression.
*/
public ReExpr MPlus(ReExpr re)
public ReExpr mkPlus(ReExpr re)
{
checkContextMatch(re);
return new ReExpr(this, Native.mkRePlus(nCtx(), re.getNativeObject()));
return (ReExpr) Expr.create(this, Native.mkRePlus(nCtx(), re.getNativeObject()));
}
/**
* Create the optional regular expression.
*/
public ReExpr MOption(ReExpr re)
public ReExpr mkOption(ReExpr re)
{
checkContextMatch(re);
return new ReExpr(this, Native.mkReOption(nCtx(), re.getNativeObject()));
return (ReExpr) Expr.create(this, Native.mkReOption(nCtx(), re.getNativeObject()));
}
/**
* Create the complement regular expression.
*/
public ReExpr mkComplement(ReExpr re)
{
checkContextMatch(re);
return (ReExpr) Expr.create(this, Native.mkReComplement(nCtx(), re.getNativeObject()));
}
/**
* Create the concatenation of regular languages.
*/
public ReExpr MkConcat(ReExpr... t)
public ReExpr mkConcat(ReExpr... t)
{
checkContextMatch(t);
return new ReExpr(this, Native.mkReConcat(nCtx(), t.length, AST.arrayToNative(t)));
return (ReExpr) Expr.create(this, Native.mkReConcat(nCtx(), t.length, AST.arrayToNative(t)));
}
/**
* Create the union of regular languages.
*/
public ReExpr MkUnion(ReExpr... t)
public ReExpr mkUnion(ReExpr... t)
{
checkContextMatch(t);
return new ReExpr(this, Native.mkReUnion(nCtx(), t.length, AST.arrayToNative(t)));
return (ReExpr) Expr.create(this, Native.mkReUnion(nCtx(), t.length, AST.arrayToNative(t)));
}
/**
* Create the intersection of regular languages.
*/
public ReExpr mkIntersect(ReExpr... t)
{
checkContextMatch(t);
return (ReExpr) Expr.create(this, Native.mkReIntersect(nCtx(), t.length, AST.arrayToNative(t)));
}
/**
* Create a range expression.
*/
public ReExpr MkRange(SeqExpr lo, SeqExpr hi)
{
checkContextMatch(lo, hi);
return (ReExpr) Expr.create(this, Native.mkReRange(nCtx(), lo.getNativeObject(), hi.getNativeObject()));
}
/**
* Create an at-most-k constraint.
*/
public BoolExpr mkAtMost(BoolExpr[] args, int k)
{
checkContextMatch(args);
return (BoolExpr) Expr.create(this, Native.mkAtmost(nCtx(), args.length, AST.arrayToNative(args), k));
}
/**
* Create an at-least-k constraint.
*/
public BoolExpr mkAtLeast(BoolExpr[] args, int k)
{
checkContextMatch(args);
return (BoolExpr) Expr.create(this, Native.mkAtleast(nCtx(), args.length, AST.arrayToNative(args), k));
}
/**
* Create a pseudo-Boolean less-or-equal constraint.
*/
public BoolExpr mkPBLe(int[] coeffs, BoolExpr[] args, int k)
{
checkContextMatch(args);
return (BoolExpr) Expr.create(this, Native.mkPble(nCtx(), args.length, AST.arrayToNative(args), coeffs, k));
}
/**
* Create a pseudo-Boolean greater-or-equal constraint.
*/
public BoolExpr mkPBGe(int[] coeffs, BoolExpr[] args, int k)
{
checkContextMatch(args);
return (BoolExpr) Expr.create(this, Native.mkPbge(nCtx(), args.length, AST.arrayToNative(args), coeffs, k));
}
/**
* Create a pseudo-Boolean equal constraint.
*/
public BoolExpr mkPBEq(int[] coeffs, BoolExpr[] args, int k)
{
checkContextMatch(args);
return (BoolExpr) Expr.create(this, Native.mkPbeq(nCtx(), args.length, AST.arrayToNative(args), coeffs, k));
}
/**
* Create a Term of a given sort.

36
src/ast/normal_forms/defined_names.cpp
View file

@ -28,7 +28,7 @@ struct defined_names::impl {
typedef obj_map<expr, proof *> expr2proof;
ast_manager & m_manager;
symbol m_z3name;
/**
\brief Mapping from expressions to their names. A name is an application.
If the expression does not have free variables, then the name is just a constant.
@ -38,25 +38,25 @@ struct defined_names::impl {
\brief Mapping from expressions to the apply-def proof.
That is, for each expression e, m_expr2proof[e] is the
proof e and m_expr2name[2] are observ. equivalent.
This mapping is not used if proof production is disabled.
*/
expr2proof m_expr2proof;
/**
\brief Domain of m_expr2name. It is used to keep the expressions
alive and for backtracking
*/
expr_ref_vector m_exprs;
expr_ref_vector m_exprs;
expr_ref_vector m_names; //!< Range of m_expr2name. It is used to keep the names alive.
proof_ref_vector m_apply_proofs; //!< Range of m_expr2proof. It is used to keep the def-intro proofs alive.
unsigned_vector m_lims; //!< Backtracking support.
impl(ast_manager & m, char const * prefix);
virtual ~impl();
app * gen_name(expr * e, sort_ref_buffer & var_sorts, buffer<symbol> & var_names);
void cache_new_name(expr * e, app * name);
void cache_new_name_intro_proof(expr * e, proof * pr);
@ -106,7 +106,7 @@ app * defined_names::impl::gen_name(expr * e, sort_ref_buffer & var_sorts, buffe
for (unsigned i = 0; i < num_vars; i++) {
sort * s = uv.get(i);
if (s) {
domain.push_back(s);
domain.push_back(s);
new_args.push_back(m_manager.mk_var(i, s));
var_sorts.push_back(s);
}
@ -162,7 +162,7 @@ void defined_names::impl::bound_vars(sort_ref_buffer const & sorts, buffer<symbo
1, symbol::null, symbol::null,
1, patterns);
TRACE("mk_definition_bug", tout << "before elim_unused_vars:\n" << mk_ismt2_pp(q, m_manager) << "\n";);
elim_unused_vars(m_manager, q, result);
elim_unused_vars(m_manager, q, params_ref(), result);
TRACE("mk_definition_bug", tout << "after elim_unused_vars:\n" << mk_ismt2_pp(result, m_manager) << "\n";);
}
}
@ -207,7 +207,7 @@ bool defined_names::impl::mk_name(expr * e, expr_ref & new_def, proof_ref & new_
app * n_ptr;
if (m_expr2name.find(e, n_ptr)) {
TRACE("mk_definition_bug", tout << "name for expression is already cached..., returning false...\n";);
TRACE("mk_definition_bug", tout << "name for expression is already cached..., returning false...\n";);
n = n_ptr;
if (m_manager.proofs_enabled()) {
proof * pr_ptr = 0;
@ -220,19 +220,19 @@ bool defined_names::impl::mk_name(expr * e, expr_ref & new_def, proof_ref & new_
else {
sort_ref_buffer var_sorts(m_manager);
buffer<symbol> var_names;
n = gen_name(e, var_sorts, var_names);
cache_new_name(e, n);
TRACE("mk_definition_bug", tout << "name: " << mk_ismt2_pp(n, m_manager) << "\n";);
// variables are in reverse order in quantifiers
std::reverse(var_sorts.c_ptr(), var_sorts.c_ptr() + var_sorts.size());
std::reverse(var_names.c_ptr(), var_names.c_ptr() + var_names.size());
mk_definition(e, n, var_sorts, var_names, new_def);
TRACE("mk_definition_bug", tout << "new_def:\n" << mk_ismt2_pp(new_def, m_manager) << "\n";);
if (m_manager.proofs_enabled()) {
new_def_pr = m_manager.mk_def_intro(new_def);
pr = m_manager.mk_apply_def(e, n, new_def_pr);
@ -311,11 +311,11 @@ void defined_names::reset() {
m_pos_impl->reset();
}
unsigned defined_names::get_num_names() const {
unsigned defined_names::get_num_names() const {
return m_impl->get_num_names() + m_pos_impl->get_num_names();
}
func_decl * defined_names::get_name_decl(unsigned i) const {
func_decl * defined_names::get_name_decl(unsigned i) const {
SASSERT(i < get_num_names());
unsigned n1 = m_impl->get_num_names();
return i < n1 ? m_impl->get_name_decl(i) : m_pos_impl->get_name_decl(i - n1);

2
src/ast/rewriter/arith_rewriter.cpp
View file

@ -194,7 +194,7 @@ bool arith_rewriter::is_bound(expr * arg1, expr * arg2, op_kind kind, expr_ref &
}
}
expr* t1, *t2;
bool is_int;
bool is_int = false;
if (m_util.is_mod(arg2)) {
std::swap(arg1, arg2);
switch (kind) {

62
src/ast/rewriter/der.cpp
View file

@ -36,7 +36,7 @@ static bool is_neg_var(ast_manager & m, expr * e, unsigned num_decls) {
/**
\brief Return true if \c e is of the form (not (= VAR t)) or (not (iff VAR t)) or (iff VAR t) or (iff (not VAR) t) or (VAR IDX) or (not (VAR IDX)).
The last case can be viewed
The last case can be viewed
*/
bool der::is_var_diseq(expr * e, unsigned num_decls, var * & v, expr_ref & t) {
// (not (= VAR t)) and (not (iff VAR t)) cases
@ -49,7 +49,7 @@ bool der::is_var_diseq(expr * e, unsigned num_decls, var * & v, expr_ref & t) {
return false;
if (!is_var(lhs, num_decls))
std::swap(lhs, rhs);
SASSERT(is_var(lhs, num_decls));
SASSERT(is_var(lhs, num_decls));
// Remark: Occurs check is not necessary here... the top-sort procedure will check for cycles...
// if (occurs(lhs, rhs)) {
// return false;
@ -67,7 +67,7 @@ bool der::is_var_diseq(expr * e, unsigned num_decls, var * & v, expr_ref & t) {
if (is_var(lhs, num_decls) || is_var(rhs, num_decls)) {
if (!is_var(lhs, num_decls))
std::swap(lhs, rhs);
SASSERT(is_var(lhs, num_decls));
SASSERT(is_var(lhs, num_decls));
// Remark: Occurs check is not necessary here... the top-sort procedure will check for cycles...
// if (occurs(lhs, rhs)) {
// return false;
@ -83,11 +83,11 @@ bool der::is_var_diseq(expr * e, unsigned num_decls, var * & v, expr_ref & t) {
if (!is_neg_var(m_manager, lhs, num_decls))
std::swap(lhs, rhs);
SASSERT(is_neg_var(m_manager, lhs, num_decls));
expr * lhs_var = to_app(lhs)->get_arg(0);
expr * lhs_var = to_app(lhs)->get_arg(0);
// Remark: Occurs check is not necessary here... the top-sort procedure will check for cycles...
// if (occurs(lhs_var, rhs)) {
// return false;
// }
// }
v = to_var(lhs_var);
t = rhs;
TRACE("der", tout << mk_pp(e, m_manager) << "\n";);
@ -134,11 +134,11 @@ void der::operator()(quantifier * q, expr_ref & r, proof_ref & pr) {
pr = m_manager.mk_transitivity(pr, curr_pr);
}
} while (q != r && is_quantifier(r));
// Eliminate variables that have become unused
if (reduced && is_forall(r)) {
quantifier * q = to_quantifier(r);
elim_unused_vars(m_manager, q, r);
elim_unused_vars(m_manager, q, params_ref(), r);
if (m_manager.proofs_enabled()) {
proof * p1 = m_manager.mk_elim_unused_vars(q, r);
pr = m_manager.mk_transitivity(pr, p1);
@ -153,24 +153,24 @@ void der::reduce1(quantifier * q, expr_ref & r, proof_ref & pr) {
r = q;
return;
}
expr * e = q->get_expr();
unsigned num_decls = q->get_num_decls();
var * v = 0;
expr_ref t(m_manager);
expr_ref t(m_manager);
if (m_manager.is_or(e)) {
unsigned num_args = to_app(e)->get_num_args();
unsigned i = 0;
unsigned diseq_count = 0;
unsigned largest_vinx = 0;
m_map.reset();
m_pos2var.reset();
m_inx2var.reset();
m_pos2var.reserve(num_args, -1);
// Find all disequalities
for (; i < num_args; i++) {
if (is_var_diseq(to_app(e)->get_arg(i), num_decls, v, t)) {
@ -192,7 +192,7 @@ void der::reduce1(quantifier * q, expr_ref & r, proof_ref & pr) {
get_elimination_order();
SASSERT(m_order.size() <= diseq_count); // some might be missing because of cycles
if (!m_order.empty()) {
if (!m_order.empty()) {
create_substitution(largest_vinx + 1);
apply_substitution(q, r);
}
@ -202,22 +202,22 @@ void der::reduce1(quantifier * q, expr_ref & r, proof_ref & pr) {
r = q;
}
}
// Remark: get_elimination_order/top-sort checks for cycles, but it is not invoked for unit clauses.
// Remark: get_elimination_order/top-sort checks for cycles, but it is not invoked for unit clauses.
// So, we must perform a occurs check here.
else if (is_var_diseq(e, num_decls, v, t) && !occurs(v, t)) {
r = m_manager.mk_false();
}
else
else
r = q;
if (m_manager.proofs_enabled()) {
pr = r == q ? 0 : m_manager.mk_der(q, r);
}
}
}
void der_sort_vars(ptr_vector<var> & vars, ptr_vector<expr> & definitions, unsigned_vector & order) {
order.reset();
// eliminate self loops, and definitions containing quantifiers.
bool found = false;
for (unsigned i = 0; i < definitions.size(); i++) {
@ -228,7 +228,7 @@ void der_sort_vars(ptr_vector<var> & vars, ptr_vector<expr> & definitions, unsig
else
found = true; // found at least one candidate
}
if (!found)
return;
@ -329,14 +329,14 @@ void der::get_elimination_order() {
// der::top_sort ts(m_manager);
der_sort_vars(m_inx2var, m_map, m_order);
TRACE("der",
TRACE("der",
tout << "Elimination m_order:" << std::endl;
for(unsigned i=0; i<m_order.size(); i++)
{
if (i != 0) tout << ",";
tout << m_order[i];
}
tout << std::endl;
tout << std::endl;
);
}
@ -359,24 +359,24 @@ void der::create_substitution(unsigned sz) {
void der::apply_substitution(quantifier * q, expr_ref & r) {
expr * e = q->get_expr();
unsigned num_args=to_app(e)->get_num_args();
unsigned num_args=to_app(e)->get_num_args();
// get a new expression
m_new_args.reset();
for(unsigned i = 0; i < num_args; i++) {
int x = m_pos2var[i];
if (x != -1 && m_map[x] != 0)
if (x != -1 && m_map[x] != 0)
continue; // this is a disequality with definition (vanishes)
m_new_args.push_back(to_app(e)->get_arg(i));
}
unsigned sz = m_new_args.size();
expr_ref t(m_manager);
t = (sz == 1) ? m_new_args[0] : m_manager.mk_or(sz, m_new_args.c_ptr());
expr_ref new_e(m_manager);
expr_ref new_e(m_manager);
m_subst(t, m_subst_map.size(), m_subst_map.c_ptr(), new_e);
// don't forget to update the quantifier patterns
expr_ref_buffer new_patterns(m_manager);
expr_ref_buffer new_no_patterns(m_manager);
@ -392,7 +392,7 @@ void der::apply_substitution(quantifier * q, expr_ref & r) {
new_no_patterns.push_back(new_nopat);
}
r = m_manager.update_quantifier(q, new_patterns.size(), new_patterns.c_ptr(),
r = m_manager.update_quantifier(q, new_patterns.size(), new_patterns.c_ptr(),
new_no_patterns.size(), new_no_patterns.c_ptr(), new_e);
}
@ -404,9 +404,9 @@ struct der_rewriter_cfg : public default_rewriter_cfg {
ast_manager & m() const { return m_der.m(); }
bool reduce_quantifier(quantifier * old_q,
expr * new_body,
expr * const * new_patterns,
bool reduce_quantifier(quantifier * old_q,
expr * new_body,
expr * const * new_patterns,
expr * const * new_no_patterns,
expr_ref & result,
proof_ref & result_pr) {

3
src/ast/rewriter/rewriter_params.pyg
View file

@ -8,5 +8,6 @@ def_module_params('rewriter',
("push_ite_bv", BOOL, False, "push if-then-else over bit-vector terms."),
("pull_cheap_ite", BOOL, False, "pull if-then-else terms when cheap."),
("bv_ineq_consistency_test_max", UINT, 0, "max size of conjunctions on which to perform consistency test based on inequalities on bitvectors."),
("cache_all", BOOL, False, "cache all intermediate results.")))
("cache_all", BOOL, False, "cache all intermediate results."),
("ignore_patterns_on_ground_qbody", BOOL, True, "ignores patterns on quantifiers that don't mention their bound variables.")))

34
src/ast/rewriter/seq_rewriter.cpp
View file

@ -60,7 +60,12 @@ expr_ref sym_expr::accept(expr* e) {
}
std::ostream& sym_expr::display(std::ostream& out) const {
return out << m_t;
switch (m_ty) {
case t_char: return out << m_t;
case t_range: return out << m_t << ":" << m_s;
case t_pred: return out << m_t;
}
return out << "expression type not recognized";
}
struct display_expr1 {
@ -237,6 +242,7 @@ eautomaton* re2automaton::re2aut(expr* e) {
unsigned nb = s1.num_bits();
expr_ref _start(bv.mk_numeral(start, nb), m);
expr_ref _stop(bv.mk_numeral(stop, nb), m);
TRACE("seq", tout << "Range: " << start << " " << stop << "\n";);
a = alloc(eautomaton, sm, sym_expr::mk_range(_start, _stop));
return a.detach();
}
@ -646,6 +652,29 @@ br_status seq_rewriter::mk_seq_contains(expr* a, expr* b, expr_ref& result) {
result = m().mk_true();
return BR_DONE;
}
bool all_units = true;
for (unsigned i = 0; i < bs.size(); ++i) {
all_units = m_util.str.is_unit(bs[i].get());
}
for (unsigned i = 0; i < as.size(); ++i) {
all_units = m_util.str.is_unit(as[i].get());
}
if (all_units) {
if (as.size() < bs.size()) {
result = m().mk_false();
return BR_DONE;
}
expr_ref_vector ors(m());
for (unsigned i = 0; i < as.size() - bs.size() + 1; ++i) {
expr_ref_vector ands(m());
for (unsigned j = 0; j < bs.size(); ++j) {
ands.push_back(m().mk_eq(as[i + j].get(), bs[j].get()));
}
ors.push_back(::mk_and(ands));
}
result = ::mk_or(ors);
return BR_REWRITE_FULL;
}
return BR_FAILED;
}
@ -1435,6 +1464,7 @@ bool seq_rewriter::reduce_eq(expr_ref_vector& ls, expr_ref_vector& rs, expr_ref_
zstring s;
bool lchange = false;
SASSERT(lhs.empty());
TRACE("seq", tout << ls << "\n"; tout << rs << "\n";);
// solve from back
while (true) {
while (!rs.empty() && m_util.str.is_empty(rs.back())) {
@ -1552,9 +1582,11 @@ bool seq_rewriter::reduce_eq(expr_ref_vector& ls, expr_ref_vector& rs, expr_ref_
head2 < rs.size() &&
m_util.str.is_string(ls[head1].get(), s1) &&
m_util.str.is_string(rs[head2].get(), s2)) {
TRACE("seq", tout << s1 << " - " << s2 << " " << s1.length() << " " << s2.length() << "\n";);
unsigned l = std::min(s1.length(), s2.length());
for (unsigned i = 0; i < l; ++i) {
if (s1[i] != s2[i]) {
TRACE("seq", tout << "different at position " << i << " " << s1[i] << " " << s2[i] << "\n";);
return false;
}
}

72
src/ast/rewriter/th_rewriter.cpp
View file

@ -54,6 +54,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
bool m_cache_all;
bool m_push_ite_arith;
bool m_push_ite_bv;
bool m_ignore_patterns_on_ground_qbody;
// substitution support
expr_dependency_ref m_used_dependencies; // set of dependencies of used substitutions
@ -70,8 +71,9 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
m_cache_all = p.cache_all();
m_push_ite_arith = p.push_ite_arith();
m_push_ite_bv = p.push_ite_bv();
m_ignore_patterns_on_ground_qbody = p.ignore_patterns_on_ground_qbody();
}
void updt_params(params_ref const & p) {
m_b_rw.updt_params(p);
m_a_rw.updt_params(p);
@ -82,7 +84,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
updt_local_params(p);
}
bool flat_assoc(func_decl * f) const {
bool flat_assoc(func_decl * f) const {
if (!m_flat) return false;
family_id fid = f->get_family_id();
if (fid == null_family_id)
@ -98,10 +100,10 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
}
bool rewrite_patterns() const { return false; }
bool cache_all_results() const { return m_cache_all; }
bool max_steps_exceeded(unsigned num_steps) const {
bool max_steps_exceeded(unsigned num_steps) const {
cooperate("simplifier");
if (memory::get_allocation_size() > m_max_memory)
throw rewriter_exception(Z3_MAX_MEMORY_MSG);
@ -179,13 +181,13 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
st = m_ar_rw.mk_eq_core(args[0], args[1], result);
else if (s_fid == m_seq_rw.get_fid())
st = m_seq_rw.mk_eq_core(args[0], args[1], result);
if (st != BR_FAILED)
return st;
}
if (k == OP_EQ || k == OP_IFF) {
SASSERT(num == 2);
st = apply_tamagotchi(args[0], args[1], result);
st = apply_tamagotchi(args[0], args[1], result);
if (st != BR_FAILED)
return st;
}
@ -239,13 +241,13 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
}
else {
if (SWAP) {
result = m().mk_ite(ite->get_arg(0),
result = m().mk_ite(ite->get_arg(0),
m().mk_app(p, value, ite->get_arg(1)),
m().mk_app(p, value, ite->get_arg(2)));
return BR_REWRITE2;
}
else {
result = m().mk_ite(ite->get_arg(0),
result = m().mk_ite(ite->get_arg(0),
m().mk_app(p, ite->get_arg(1), value),
m().mk_app(p, ite->get_arg(2), value));
return BR_REWRITE2;
@ -257,7 +259,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
// ite-value-tree := (ite c <subtree> <subtree>)
// subtree := value
// | (ite c <subtree> <subtree>)
//
//
bool is_ite_value_tree(expr * t) {
if (!m().is_ite(t))
return false;
@ -281,7 +283,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
}
return true;
}
br_status pull_ite(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
if (num == 2 && m().is_bool(f->get_range()) && !m().is_bool(args[0])) {
if (m().is_ite(args[0])) {
@ -325,7 +327,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
if (!is_app(t))
return false;
family_id fid = to_app(t)->get_family_id();
return ((fid == m_a_rw.get_fid() && m_push_ite_arith) ||
return ((fid == m_a_rw.get_fid() && m_push_ite_arith) ||
(fid == m_bv_rw.get_fid() && m_push_ite_bv));
}
@ -349,7 +351,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
}
return false;
}
/**
\brief Try to "unify" t1 and t2
Examples
@ -463,7 +465,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
}
// terms matched...
bool is_int = m_a_util.is_int(t1);
if (!new_t1)
if (!new_t1)
new_t1 = m_a_util.mk_numeral(rational(0), is_int);
if (!new_t2)
new_t2 = m_a_util.mk_numeral(rational(0), is_int);
@ -476,7 +478,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
args.push_back(arg);
}
SASSERT(!args.empty());
if (args.size() == 1)
if (args.size() == 1)
c = args[0];
else
c = m_a_util.mk_add(args.size(), args.c_ptr());
@ -518,7 +520,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
// Apply transformations of the form
//
// (ite c (+ k1 a) (+ k2 a)) --> (+ (ite c k1 k2) a)
// (ite c (+ k1 a) (+ k2 a)) --> (+ (ite c k1 k2) a)
// (ite c (* k1 a) (* k2 a)) --> (* (ite c k1 k2) a)
//
// These transformations are useful for bit-vector problems, since
@ -536,7 +538,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
if (unify(t, e, f_prime, new_t, new_e, common, first)) {
if (first)
result = m().mk_app(f_prime, common, m().mk_ite(c, new_t, new_e));
else
else
result = m().mk_app(f_prime, m().mk_ite(c, new_t, new_e), common);
return BR_DONE;
}
@ -558,7 +560,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
result_pr = 0;
br_status st = reduce_app_core(f, num, args, result);
if (st != BR_DONE && st != BR_FAILED) {
CTRACE("th_rewriter_step", st != BR_FAILED,
CTRACE("th_rewriter_step", st != BR_FAILED,
tout << f->get_name() << "\n";
for (unsigned i = 0; i < num; i++) tout << mk_ismt2_pp(args[i], m()) << "\n";
tout << "---------->\n" << mk_ismt2_pp(result, m()) << "\n";);
@ -576,7 +578,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
else
st = pull_ite(result);
}
CTRACE("th_rewriter_step", st != BR_FAILED,
CTRACE("th_rewriter_step", st != BR_FAILED,
tout << f->get_name() << "\n";
for (unsigned i = 0; i < num; i++) tout << mk_ismt2_pp(args[i], m()) << "\n";
tout << "---------->\n" << mk_ismt2_pp(result, m()) << "\n";);
@ -593,28 +595,28 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
}
bool reduce_quantifier(quantifier * old_q,
expr * new_body,
expr * const * new_patterns,
bool reduce_quantifier(quantifier * old_q,
expr * new_body,
expr * const * new_patterns,
expr * const * new_no_patterns,
expr_ref & result,
proof_ref & result_pr) {
quantifier_ref q1(m());
proof * p1 = 0;
if (is_quantifier(new_body) &&
if (is_quantifier(new_body) &&
to_quantifier(new_body)->is_forall() == old_q->is_forall() &&
!old_q->has_patterns() &&
!to_quantifier(new_body)->has_patterns()) {
quantifier * nested_q = to_quantifier(new_body);
ptr_buffer<sort> sorts;
buffer<symbol> names;
buffer<symbol> names;
sorts.append(old_q->get_num_decls(), old_q->get_decl_sorts());
names.append(old_q->get_num_decls(), old_q->get_decl_names());
sorts.append(nested_q->get_num_decls(), nested_q->get_decl_sorts());
names.append(nested_q->get_num_decls(), nested_q->get_decl_names());
q1 = m().mk_quantifier(old_q->is_forall(),
sorts.size(),
sorts.c_ptr(),
@ -624,9 +626,9 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
old_q->get_qid(),
old_q->get_skid(),
0, 0, 0, 0);
SASSERT(is_well_sorted(m(), q1));
if (m().proofs_enabled()) {
SASSERT(old_q->get_expr() == new_body);
p1 = m().mk_pull_quant(old_q, q1);
@ -635,24 +637,24 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
else {
ptr_buffer<expr> new_patterns_buf;
ptr_buffer<expr> new_no_patterns_buf;
new_patterns_buf.append(old_q->get_num_patterns(), new_patterns);
new_no_patterns_buf.append(old_q->get_num_no_patterns(), new_no_patterns);
remove_duplicates(new_patterns_buf);
remove_duplicates(new_no_patterns_buf);
q1 = m().update_quantifier(old_q,
q1 = m().update_quantifier(old_q,
new_patterns_buf.size(), new_patterns_buf.c_ptr(), new_no_patterns_buf.size(), new_no_patterns_buf.c_ptr(),
new_body);
TRACE("reduce_quantifier", tout << mk_ismt2_pp(old_q, m()) << "\n----->\n" << mk_ismt2_pp(q1, m()) << "\n";);
SASSERT(is_well_sorted(m(), q1));
}
elim_unused_vars(m(), q1, result);
elim_unused_vars(m(), q1, params_ref(), result);
TRACE("reduce_quantifier", tout << "after elim_unused_vars:\n" << mk_ismt2_pp(result, m()) << "\n";);
result_pr = 0;
if (m().proofs_enabled()) {
proof * p2 = 0;
@ -758,7 +760,7 @@ unsigned th_rewriter::get_num_steps() const {
void th_rewriter::cleanup() {
ast_manager & m = m_imp->m();
dealloc(m_imp);
m_imp = alloc(imp, m, m_params);
m_imp = alloc(imp, m, m_params);
}
void th_rewriter::reset() {

14
src/ast/rewriter/var_subst.cpp
View file

@ -39,10 +39,16 @@ void var_subst::operator()(expr * n, unsigned num_args, expr * const * args, exp
tout << mk_ismt2_pp(result, m_reducer.m()) << "\n";);
}
unused_vars_eliminator::unused_vars_eliminator(ast_manager & m, params_ref const & params) :
m(m), m_subst(m), m_params(params)
{
m_ignore_patterns_on_ground_qbody = m_params.get_bool("ignore_patterns_on_ground_qbody", true);
}
void unused_vars_eliminator::operator()(quantifier* q, expr_ref & result) {
SASSERT(is_well_sorted(m, q));
if (is_ground(q->get_expr())) {
// ignore patterns if the body is a ground formula.
if (m_ignore_patterns_on_ground_qbody && is_ground(q->get_expr())) {
// Ignore patterns if the body is a ground formula.
result = q->get_expr();
return;
}
@ -146,8 +152,8 @@ void unused_vars_eliminator::operator()(quantifier* q, expr_ref & result) {
SASSERT(is_well_sorted(m, result));
}
void elim_unused_vars(ast_manager & m, quantifier * q, expr_ref & result) {
unused_vars_eliminator el(m);
void elim_unused_vars(ast_manager & m, quantifier * q, params_ref const & params, expr_ref & result) {
unused_vars_eliminator el(m, params);
el(q, result);
}

21
src/ast/rewriter/var_subst.h
View file

@ -21,6 +21,7 @@ Notes:
#include"rewriter.h"
#include"used_vars.h"
#include"params.h"
/**
\brief Alias for var_shifter class.
@ -31,7 +32,7 @@ typedef var_shifter shift_vars;
\brief Variable substitution functor. It substitutes variables by expressions.
The expressions may contain variables.
*/
class var_subst {
class var_subst {
beta_reducer m_reducer;
bool m_std_order;
public:
@ -39,7 +40,7 @@ public:
bool std_order() const { return m_std_order; }
/**
When std_order() == true,
When std_order() == true,
I'm using the same standard used in quantifier instantiation.
(VAR 0) is stored in the last position of the array.
...
@ -55,15 +56,17 @@ public:
\brief Eliminate the unused variables from \c q. Store the result in \c r.
*/
class unused_vars_eliminator {
ast_manager& m;
var_subst m_subst;
used_vars m_used;
ast_manager & m;
var_subst m_subst;
used_vars m_used;
params_ref m_params;
bool m_ignore_patterns_on_ground_qbody;
public:
unused_vars_eliminator(ast_manager& m): m(m), m_subst(m) {}
unused_vars_eliminator(ast_manager & m, params_ref const & params);
void operator()(quantifier* q, expr_ref& r);
};
void elim_unused_vars(ast_manager & m, quantifier * q, expr_ref & r);
void elim_unused_vars(ast_manager & m, quantifier * q, params_ref const & params, expr_ref & r);
/**
\brief Instantiate quantifier q using the given exprs.
@ -86,7 +89,7 @@ class expr_free_vars {
expr_sparse_mark m_mark;
ptr_vector<sort> m_sorts;
ptr_vector<expr> m_todo;
public:
public:
void reset();
void operator()(expr* e);
void accumulate(expr* e);
@ -96,7 +99,7 @@ public:
bool contains(unsigned idx) const { return idx < m_sorts.size() && m_sorts[idx] != 0; }
void set_default_sort(sort* s);
void reverse() { m_sorts.reverse(); }
sort*const* c_ptr() const { return m_sorts.c_ptr(); }
sort*const* c_ptr() const { return m_sorts.c_ptr(); }
};
#endif

5
src/ast/seq_decl_plugin.cpp
View file

@ -126,13 +126,14 @@ static bool is_escape_char(char const *& s, unsigned& result) {
zstring::zstring(encoding enc): m_encoding(enc) {}
zstring::zstring(char const* s, encoding enc): m_encoding(enc) {
unsigned mask = 0xFF; // TBD for UTF
while (*s) {
unsigned ch;
if (is_escape_char(s, ch)) {
m_buffer.push_back(ch);
m_buffer.push_back(ch & mask);
}
else {
m_buffer.push_back(*s);
m_buffer.push_back(*s & mask);
++s;
}
}

1
src/ast/seq_decl_plugin.h
View file

@ -304,6 +304,7 @@ public:
app* mk_to_re(expr* s) { return m.mk_app(m_fid, OP_SEQ_TO_RE, 1, &s); }
app* mk_in_re(expr* s, expr* r) { return m.mk_app(m_fid, OP_SEQ_IN_RE, s, r); }
app* mk_range(expr* s1, expr* s2) { return m.mk_app(m_fid, OP_RE_RANGE, s1, s2); }
app* mk_concat(expr* r1, expr* r2) { return m.mk_app(m_fid, OP_RE_CONCAT, r1, r2); }
app* mk_union(expr* r1, expr* r2) { return m.mk_app(m_fid, OP_RE_UNION, r1, r2); }
app* mk_inter(expr* r1, expr* r2) { return m.mk_app(m_fid, OP_RE_INTERSECT, r1, r2); }

22
src/ast/simplifier/distribute_forall.cpp
View file

@ -14,7 +14,7 @@ Author:
Leonardo de Moura (leonardo) 2010-04-02.
Revision History:
Christoph Wintersteiger 2010-04-06: Added implementation.
--*/
@ -40,7 +40,7 @@ bool distribute_forall::visit_children(expr * n) {
bool visited = true;
unsigned j;
switch(n->get_kind()) {
case AST_VAR:
case AST_VAR:
break;
case AST_APP:
j = to_app(n)->get_num_args();
@ -86,15 +86,15 @@ void distribute_forall::reduce1_app(app * a) {
SASSERT(is_cached(a->get_arg(j)));
expr * c = get_cached(a->get_arg(j));
SASSERT(c!=0);
if (c != a->get_arg(j))
if (c != a->get_arg(j))
reduced = true;
m_new_args[j] = c;
}
}
if (reduced) {
na = m_manager.mk_app(a->get_decl(), num_args, m_new_args.c_ptr());
}
cache_result(a, na);
}
@ -126,11 +126,11 @@ void distribute_forall::reduce1_quantifier(quantifier * q) {
quantifier_ref tmp_q(m_manager);
tmp_q = m_manager.update_quantifier(q, not_arg);
expr_ref new_q(m_manager);
elim_unused_vars(m_manager, tmp_q, new_q);
elim_unused_vars(m_manager, tmp_q, params_ref(), new_q);
new_args.push_back(new_q);
}
expr_ref result(m_manager);
// m_bsimp.mk_and actually constructs a (not (or ...)) formula,
// m_bsimp.mk_and actually constructs a (not (or ...)) formula,
// it will also apply basic simplifications.
m_bsimp.mk_and(new_args.size(), new_args.c_ptr(), result);
cache_result(q, result);
@ -148,15 +148,15 @@ void distribute_forall::operator()(expr * f, expr_ref & result) {
while (!m_todo.empty()) {
expr * e = m_todo.back();
if (visit_children(e)) {
if (visit_children(e)) {
m_todo.pop_back();
reduce1(e);
}
}
}
result = get_cached(f);
SASSERT(result!=0);
TRACE("distribute_forall", tout << mk_ll_pp(f, m_manager) << "======>\n"
TRACE("distribute_forall", tout << mk_ll_pp(f, m_manager) << "======>\n"
<< mk_ll_pp(result, m_manager););
}
@ -166,5 +166,5 @@ expr * distribute_forall::get_cached(expr * n) const {
void distribute_forall::cache_result(expr * n, expr * r) {
SASSERT(r != 0);
m_cache.insert(n, r);
m_cache.insert(n, r);
}

14
src/ast/simplifier/elim_bounds.cpp
View file

@ -32,7 +32,7 @@ elim_bounds::elim_bounds(ast_manager & m):
(<= x k)
(<= (+ x (* -1 y)) k)
(<= (+ x (* -1 t)) k)
(<= (+ x (* -1 t)) k)
(<= (+ t (* -1 x)) k)
x and y are a bound variables, t is a ground term and k is a numeral
@ -65,14 +65,14 @@ bool elim_bounds::is_bound(expr * n, var * & lower, var * & upper) {
if (neg)
le = !le;
if (is_var(n)) {
upper = to_var(n);
}
else if (m_util.is_add(n) && to_app(n)->get_num_args() == 2) {
expr * arg1 = to_app(n)->get_arg(0);
expr * arg2 = to_app(n)->get_arg(1);
if (is_var(arg1))
if (is_var(arg1))
upper = to_var(arg1);
else if (!is_ground(arg1))
return false;
@ -95,7 +95,7 @@ bool elim_bounds::is_bound(expr * n, var * & lower, var * & upper) {
if (!le)
std::swap(upper, lower);
return true;
}
@ -188,7 +188,7 @@ void elim_bounds::operator()(quantifier * q, expr_ref & r) {
}
quantifier_ref new_q(m_manager);
new_q = m_manager.update_quantifier(q, new_body);
elim_unused_vars(m_manager, new_q, r);
elim_unused_vars(m_manager, new_q, params_ref(), r);
TRACE("elim_bounds", tout << mk_pp(q, m_manager) << "\n" << mk_pp(r, m_manager) << "\n";);
}
@ -199,10 +199,10 @@ bool elim_bounds_star::visit_quantifier(quantifier * q) {
visit(q->get_expr(), visited);
return visited;
}
void elim_bounds_star::reduce1_quantifier(quantifier * q) {
if (!q->is_forall() || q->get_num_patterns() != 0) {
cache_result(q, q, 0);
cache_result(q, q, 0);
return;
}
quantifier_ref new_q(m);

94
src/ast/simplifier/simplifier.cpp
View file

@ -33,8 +33,8 @@ simplifier::simplifier(ast_manager & m):
m_ac_support(true) {
}
void simplifier::register_plugin(plugin * p) {
m_plugins.register_plugin(p);
void simplifier::register_plugin(plugin * p) {
m_plugins.register_plugin(p);
}
simplifier::~simplifier() {
@ -46,13 +46,13 @@ void simplifier::enable_ac_support(bool flag) {
ptr_vector<plugin>::const_iterator it = m_plugins.begin();
ptr_vector<plugin>::const_iterator end = m_plugins.end();
for (; it != end; ++it) {
if (*it != 0)
if (*it != 0)
(*it)->enable_ac_support(flag);
}
}
/**
\brief External interface for the simplifier.
\brief External interface for the simplifier.
A client will invoke operator()(s, r, p) to simplify s.
The result is stored in r.
When proof generation is enabled, a proof for the equivalence (or equisatisfiability)
@ -69,14 +69,14 @@ void simplifier::operator()(expr * s, expr_ref & r, proof_ref & p) {
proof * result_proof;
switch (m.proof_mode()) {
case PGM_DISABLED: // proof generation is disabled.
reduce_core(s);
reduce_core(s);
// after executing reduce_core, the result of the simplification is in the cache
get_cached(s, result, result_proof);
r = result;
p = m.mk_undef_proof();
break;
case PGM_COARSE: // coarse proofs... in this case, we do not produce a step by step (fine grain) proof to show the equivalence (or equisatisfiability) of s an r.
m_subst_proofs.reset(); // m_subst_proofs is an auxiliary vector that is used to justify substitutions. See comment on method get_subst.
m_subst_proofs.reset(); // m_subst_proofs is an auxiliary vector that is used to justify substitutions. See comment on method get_subst.
reduce_core(s);
get_cached(s, result, result_proof);
r = result;
@ -163,7 +163,7 @@ bool simplifier::visit_children(expr * n) {
// The method ast_manager::mk_app is used to create the flat version of an AC operator.
// In Z3 1.x, we used multi-ary operators. This creates problems for the superposition engine.
// So, starting at Z3 2.x, only boolean operators can be multi-ary.
// Example:
// Example:
// (and (and a b) (and c d)) --> (and a b c d)
// (+ (+ a b) (+ c d)) --> (+ a (+ b (+ c d)))
// Remark: The flattening is only applied if m_ac_support is true.
@ -178,7 +178,7 @@ bool simplifier::visit_children(expr * n) {
}
return visited;
}
case AST_QUANTIFIER:
case AST_QUANTIFIER:
return visit_quantifier(to_quantifier(n));
default:
UNREACHABLE();
@ -188,7 +188,7 @@ bool simplifier::visit_children(expr * n) {
/**
\brief Visit the children of n assuming it is an AC (associative-commutative) operator.
For example, if n is of the form (+ (+ a b) (+ c d)), this method
will return true if the nodes a, b, c and d have been already simplified.
The nodes (+ a b) and (+ c d) are not really checked.
@ -216,7 +216,7 @@ bool simplifier::visit_ac(app * n) {
expr * arg = n->get_arg(i);
if (is_app_of(arg, decl))
todo.push_back(to_app(arg));
else
else
visit(arg, visited);
}
}
@ -319,7 +319,7 @@ void simplifier::reduce1_app_core(app * n) {
proof * p;
if (n == r)
p = 0;
else if (r != s)
else if (r != s)
// we use a "theory rewrite generic proof" to justify the step
// s = (decl arg_0' ... arg_{n-1}') --> r
p = m.mk_transitivity(p1, m.mk_rewrite(s, r));
@ -368,7 +368,7 @@ void simplifier::reduce1_ac_app_core(app * n) {
proof_ref p1(m);
mk_ac_congruent_term(n, n_c, p1);
TRACE("ac", tout << "expr:\n" << mk_pp(n, m) << "\ncongruent term:\n" << mk_pp(n_c, m) << "\n";);
expr_ref r(m);
expr_ref r(m);
func_decl * decl = n->get_decl();
family_id fid = decl->get_family_id();
plugin * p = get_plugin(fid);
@ -415,7 +415,7 @@ void simplifier::reduce1_ac_app_core(app * n) {
proof * p;
if (n == r.get())
p = 0;
else if (r.get() != n_c.get())
else if (r.get() != n_c.get())
p = m.mk_transitivity(p1, m.mk_rewrite(n_c, r));
else
p = p1;
@ -434,7 +434,7 @@ void simplifier::dump_rewrite_lemma(func_decl * decl, unsigned num_args, expr *
sprintf_s(buffer, ARRAYSIZE(buffer), "lemma_%d.smt", g_rewrite_lemma_id);
#else
sprintf(buffer, "rewrite_lemma_%d.smt", g_rewrite_lemma_id);
#endif
#endif
ast_smt_pp pp(m);
pp.set_benchmark_name("rewrite_lemma");
pp.set_status("unsat");
@ -450,7 +450,7 @@ void simplifier::dump_rewrite_lemma(func_decl * decl, unsigned num_args, expr *
/**
\brief Return in \c result an expression \c e equivalent to <tt>(f args[0] ... args[num_args - 1])</tt>, and
store in \c pr a proof for <tt>(= (f args[0] ... args[num_args - 1]) e)</tt>
If e is identical to (f args[0] ... args[num_args - 1]), then pr is set to 0.
*/
void simplifier::mk_app(func_decl * decl, unsigned num_args, expr * const * args, expr_ref & result) {
@ -474,7 +474,7 @@ void simplifier::mk_app(func_decl * decl, unsigned num_args, expr * const * args
//dump_rewrite_lemma(decl, num_args, args, result.get());
return;
}
result = m.mk_app(decl, num_args, args);
}
@ -494,17 +494,17 @@ void simplifier::mk_congruent_term(app * n, app_ref & r, proof_ref & p) {
proof * arg_proof;
get_cached(arg, new_arg, arg_proof);
CTRACE("simplifier_bug", (arg != new_arg) != (arg_proof != 0),
CTRACE("simplifier_bug", (arg != new_arg) != (arg_proof != 0),
tout << mk_ll_pp(arg, m) << "\n---->\n" << mk_ll_pp(new_arg, m) << "\n";
tout << "#" << arg->get_id() << " #" << new_arg->get_id() << "\n";
tout << arg << " " << new_arg << "\n";);
if (arg != new_arg) {
has_new_args = true;
proofs.push_back(arg_proof);
SASSERT(arg_proof);
}
}
else {
SASSERT(arg_proof == 0);
}
@ -526,10 +526,10 @@ void simplifier::mk_congruent_term(app * n, app_ref & r, proof_ref & p) {
/**
\brief Store the new arguments of \c n in result. Store in p a proof for
(= n (f result[0] ... result[num_args - 1])), where f is the function symbol of n.
If there are no new arguments or fine grain proofs are disabled, then p is set to 0.
Return true there are new arguments.
Return true there are new arguments.
*/
bool simplifier::get_args(app * n, ptr_vector<expr> & result, proof_ref & p) {
bool has_new_args = false;
@ -565,10 +565,10 @@ bool simplifier::get_args(app * n, ptr_vector<expr> & result, proof_ref & p) {
void simplifier::mk_ac_congruent_term(app * n, app_ref & r, proof_ref & p) {
SASSERT(m_ac_support);
func_decl * f = n->get_decl();
m_ac_cache.reset();
m_ac_pr_cache.reset();
ptr_buffer<app> todo;
ptr_buffer<expr> new_args;
ptr_buffer<proof> new_arg_prs;
@ -621,7 +621,7 @@ void simplifier::mk_ac_congruent_term(app * n, app_ref & r, proof_ref & p) {
todo.pop_back();
if (!has_new_arg) {
m_ac_cache.insert(curr, curr);
if (m.fine_grain_proofs())
if (m.fine_grain_proofs())
m_ac_pr_cache.insert(curr, 0);
}
else {
@ -634,7 +634,7 @@ void simplifier::mk_ac_congruent_term(app * n, app_ref & r, proof_ref & p) {
}
}
}
SASSERT(m_ac_cache.contains(n));
app * new_n = 0;
m_ac_cache.find(n, new_n);
@ -646,7 +646,7 @@ void simplifier::mk_ac_congruent_term(app * n, app_ref & r, proof_ref & p) {
}
}
#define White 0
#define White 0
#define Grey 1
#define Black 2
@ -688,7 +688,7 @@ void simplifier::ac_top_sort(app * n, ptr_buffer<expr> & result) {
while (!todo.empty()) {
expr * curr = todo.back();
int color;
obj_map<expr, int>::obj_map_entry * entry = colors.insert_if_not_there2(curr, White);
obj_map<expr, int>::obj_map_entry * entry = colors.insert_if_not_there2(curr, White);
SASSERT(entry);
color = entry->get_data().m_value;
switch (color) {
@ -731,7 +731,7 @@ void simplifier::get_ac_args(app * n, ptr_vector<expr> & args, vector<rational>
ac_top_sort(n, sorted_exprs);
SASSERT(!sorted_exprs.empty());
SASSERT(sorted_exprs[sorted_exprs.size()-1] == n);
TRACE("ac", tout << mk_ll_pp(n, m, true, false) << "#" << n->get_id() << "\nsorted expressions...\n";
for (unsigned i = 0; i < sorted_exprs.size(); i++) {
tout << "#" << sorted_exprs[i]->get_id() << " ";
@ -747,7 +747,7 @@ void simplifier::get_ac_args(app * n, ptr_vector<expr> & args, vector<rational>
expr * curr = sorted_exprs[j];
rational mult;
m_ac_mults.find(curr, mult);
SASSERT(!mult.is_zero());
SASSERT(!mult.is_zero());
if (is_app_of(curr, decl)) {
unsigned num_args = to_app(curr)->get_num_args();
for (unsigned i = 0; i < num_args; i++) {
@ -772,16 +772,16 @@ void simplifier::reduce1_quantifier(quantifier * q) {
quantifier_ref q1(m);
proof * p1 = 0;
if (is_quantifier(new_body) &&
if (is_quantifier(new_body) &&
to_quantifier(new_body)->is_forall() == q->is_forall() &&
!to_quantifier(q)->has_patterns() &&
!to_quantifier(new_body)->has_patterns()) {
quantifier * nested_q = to_quantifier(new_body);
ptr_buffer<sort> sorts;
buffer<symbol> names;
buffer<symbol> names;
sorts.append(q->get_num_decls(), q->get_decl_sorts());
names.append(q->get_num_decls(), q->get_decl_names());
sorts.append(nested_q->get_num_decls(), nested_q->get_decl_sorts());
@ -797,7 +797,7 @@ void simplifier::reduce1_quantifier(quantifier * q) {
q->get_skid(),
0, 0, 0, 0);
SASSERT(is_well_sorted(m, q1));
if (m.fine_grain_proofs()) {
quantifier * q0 = m.update_quantifier(q, new_body);
proof * p0 = q == q0 ? 0 : m.mk_quant_intro(q, q0, new_body_pr);
@ -817,13 +817,13 @@ void simplifier::reduce1_quantifier(quantifier * q) {
get_cached(q->get_pattern(i), new_pattern, new_pattern_pr);
if (m.is_pattern(new_pattern)) {
new_patterns.push_back(new_pattern);
}
}
}
num = q->get_num_no_patterns();
for (unsigned i = 0; i < num; i++) {
get_cached(q->get_no_pattern(i), new_pattern, new_pattern_pr);
new_no_patterns.push_back(new_pattern);
}
}
remove_duplicates(new_patterns);
remove_duplicates(new_no_patterns);
@ -833,7 +833,7 @@ void simplifier::reduce1_quantifier(quantifier * q) {
q->get_decl_sorts(),
q->get_decl_names(),
new_body,
q->get_weight(),
q->get_weight(),
q->get_qid(),
q->get_skid(),
new_patterns.size(),
@ -850,10 +850,10 @@ void simplifier::reduce1_quantifier(quantifier * q) {
p1 = q == q1 ? 0 : m.mk_quant_intro(q, q1, new_body_pr);
}
}
expr_ref r(m);
elim_unused_vars(m, q1, r);
elim_unused_vars(m, q1, params_ref(), r);
proof * pr = 0;
if (m.fine_grain_proofs()) {
proof * p2 = 0;
@ -871,7 +871,7 @@ void simplifier::reduce1_quantifier(quantifier * q) {
void simplifier::borrow_plugins(simplifier const & s) {
ptr_vector<plugin>::const_iterator it = s.begin_plugins();
ptr_vector<plugin>::const_iterator end = s.end_plugins();
for (; it != end; ++it)
for (; it != end; ++it)
register_plugin(*it);
}
@ -882,7 +882,7 @@ void simplifier::enable_presimp() {
enable_ac_support(false);
ptr_vector<plugin>::const_iterator it = begin_plugins();
ptr_vector<plugin>::const_iterator end = end_plugins();
for (; it != end; ++it)
for (; it != end; ++it)
(*it)->enable_presimp(true);
}
@ -905,7 +905,7 @@ bool subst_simplifier::get_subst(expr * n, expr_ref & r, proof_ref & p) {
m_subst_map->get(n, _r, _p);
r = _r;
p = _p;
if (m.coarse_grain_proofs())
if (m.coarse_grain_proofs())
m_subst_proofs.push_back(p);
return true;
}
@ -917,7 +917,7 @@ static void push_core(ast_manager & m, expr * e, proof * pr, expr_ref_vector & r
TRACE("preprocessor",
tout << mk_pp(e, m) << "\n";
if (pr) tout << mk_ll_pp(pr, m) << "\n\n";);
if (m.is_true(e))
if (m.is_true(e))
return;
result.push_back(e);
if (m.proofs_enabled())
@ -952,9 +952,9 @@ void push_assertion(ast_manager & m, expr * e, proof * pr, expr_ref_vector & res
CTRACE("push_assertion", !(pr == 0 || m.is_undef_proof(pr) || m.get_fact(pr) == e),
tout << mk_pp(e, m) << "\n" << mk_pp(m.get_fact(pr), m) << "\n";);
SASSERT(pr == 0 || m.is_undef_proof(pr) || m.get_fact(pr) == e);
if (m.is_and(e))
if (m.is_and(e))
push_and(m, to_app(e), pr, result, result_prs);
else if (m.is_not(e) && m.is_or(to_app(e)->get_arg(0)))
else if (m.is_not(e) && m.is_or(to_app(e)->get_arg(0)))
push_not_or(m, to_app(to_app(e)->get_arg(0)), pr, result, result_prs);
else
push_core(m, e, pr, result, result_prs);

43
src/cmd_context/extra_cmds/dbg_cmds.cpp
View file

@ -29,11 +29,12 @@ Notes:
#include"bound_manager.h"
#include"used_vars.h"
#include"var_subst.h"
#include"gparams.h"
#ifndef _EXTERNAL_RELEASE
BINARY_SYM_CMD(get_quantifier_body_cmd,
"dbg-get-qbody",
BINARY_SYM_CMD(get_quantifier_body_cmd,
"dbg-get-qbody",
"<symbol> <quantifier>",
"store the body of the quantifier in the global variable <symbol>",
CPK_EXPR,
@ -43,8 +44,8 @@ BINARY_SYM_CMD(get_quantifier_body_cmd,
store_expr_ref(ctx, m_sym, to_quantifier(arg)->get_expr());
});
BINARY_SYM_CMD(set_cmd,
"dbg-set",
BINARY_SYM_CMD(set_cmd,
"dbg-set",
"<symbol> <term>",
"store <term> in the global variable <symbol>",
CPK_EXPR,
@ -57,7 +58,7 @@ UNARY_CMD(pp_var_cmd, "dbg-pp-var", "<symbol>", "pretty print a global variable
expr * t = get_expr_ref(ctx, arg);
SASSERT(t != 0);
ctx.display(ctx.regular_stream(), t);
ctx.regular_stream() << std::endl;
ctx.regular_stream() << std::endl;
});
BINARY_SYM_CMD(shift_vars_cmd,
@ -71,7 +72,7 @@ BINARY_SYM_CMD(shift_vars_cmd,
var_shifter s(ctx.m());
s(t, arg, r);
store_expr_ref(ctx, m_sym, r.get());
});
});
UNARY_CMD(pp_shared_cmd, "dbg-pp-shared", "<term>", "display shared subterms of the given term", CPK_EXPR, expr *, {
shared_occs s(ctx.m());
@ -81,7 +82,7 @@ UNARY_CMD(pp_shared_cmd, "dbg-pp-shared", "<term>", "display shared subterms of
shared_occs::iterator end = s.end_shared();
for (; it != end; ++it) {
expr * curr = *it;
ctx.regular_stream() << std::endl << " ";
ctx.regular_stream() << std::endl << " ";
ctx.display(ctx.regular_stream(), curr, 2);
}
ctx.regular_stream() << ")" << std::endl;
@ -112,7 +113,7 @@ public:
if (m_idx == 1) return CPK_SYMBOL_LIST;
return CPK_SYMBOL;
}
virtual void set_next_arg(cmd_context & ctx, symbol const & s) {
virtual void set_next_arg(cmd_context & ctx, symbol const & s) {
if (m_idx == 0) {
m_source = get_expr_ref(ctx, s);
}
@ -146,24 +147,24 @@ UNARY_CMD(bool_rewriter_cmd, "dbg-bool-rewriter", "<term>", "apply the Boolean r
bool_rewriter_star r(ctx.m(), p);
r(arg, t);
ctx.display(ctx.regular_stream(), t);
ctx.regular_stream() << std::endl;
ctx.regular_stream() << std::endl;
});
UNARY_CMD(bool_frewriter_cmd, "dbg-bool-flat-rewriter", "<term>", "apply the Boolean (flattening) rewriter to the given term", CPK_EXPR, expr *, {
expr_ref t(ctx.m());
{
{
params_ref p;
p.set_bool("flat", true);
bool_rewriter_star r(ctx.m(), p);
r(arg, t);
}
ctx.display(ctx.regular_stream(), t);
ctx.regular_stream() << std::endl;
ctx.regular_stream() << std::endl;
});
UNARY_CMD(elim_and_cmd, "dbg-elim-and", "<term>", "apply the Boolean rewriter (eliminating AND operator and flattening) to the given term", CPK_EXPR, expr *, {
expr_ref t(ctx.m());
{
{
params_ref p;
p.set_bool("flat", true);
p.set_bool("elim_and", true);
@ -171,7 +172,7 @@ UNARY_CMD(elim_and_cmd, "dbg-elim-and", "<term>", "apply the Boolean rewriter (e
r(arg, t);
}
ctx.display(ctx.regular_stream(), t);
ctx.regular_stream() << std::endl;
ctx.regular_stream() << std::endl;
});
class lt_cmd : public cmd {
@ -192,7 +193,7 @@ public:
}
virtual void execute(cmd_context & ctx) {
bool r = lt(m_t1, m_t2);
ctx.regular_stream() << (r ? "true" : "false") << std::endl;
ctx.regular_stream() << (r ? "true" : "false") << std::endl;
}
};
@ -249,7 +250,7 @@ UNARY_CMD(set_next_id, "dbg-set-next-id", "<unsigned>", "set the next expression
UNARY_CMD(used_vars_cmd, "dbg-used-vars", "<expr>", "test used_vars functor", CPK_EXPR, expr *, {
used_vars proc;
if (is_quantifier(arg))
if (is_quantifier(arg))
arg = to_quantifier(arg)->get_expr();
proc(arg);
ctx.regular_stream() << "(vars";
@ -258,7 +259,7 @@ UNARY_CMD(used_vars_cmd, "dbg-used-vars", "<expr>", "test used_vars functor", CP
ctx.regular_stream() << "\n (" << std::left << std::setw(6) << i << " ";
if (s != 0)
ctx.display(ctx.regular_stream(), s, 10);
else
else
ctx.regular_stream() << "<not-used>";
ctx.regular_stream() << ")";
}
@ -271,7 +272,7 @@ UNARY_CMD(elim_unused_vars_cmd, "dbg-elim-unused-vars", "<expr>", "eliminate unu
return;
}
expr_ref r(ctx.m());
elim_unused_vars(ctx.m(), to_quantifier(arg), r);
elim_unused_vars(ctx.m(), to_quantifier(arg), gparams::get(), r);
SASSERT(!is_quantifier(r) || !to_quantifier(r)->may_have_unused_vars());
ctx.display(ctx.regular_stream(), r);
ctx.regular_stream() << std::endl;
@ -287,18 +288,18 @@ public:
virtual char const * get_descr() const { return "instantiate the quantifier using the given expressions."; }
virtual unsigned get_arity() const { return 2; }
virtual void prepare(cmd_context & ctx) { m_q = 0; m_args.reset(); }
virtual cmd_arg_kind next_arg_kind(cmd_context & ctx) const {
if (m_q == 0) return CPK_EXPR;
else return CPK_EXPR_LIST;
}
virtual void set_next_arg(cmd_context & ctx, expr * s) {
if (!is_quantifier(s))
throw cmd_exception("invalid command, quantifier expected.");
m_q = to_quantifier(s);
}
virtual void set_next_arg(cmd_context & ctx, unsigned num, expr * const * ts) {
if (num != m_q->get_num_decls())
throw cmd_exception("invalid command, mismatch between the number of quantified variables and the number of arguments.");
@ -331,7 +332,7 @@ public:
class instantiate_nested_cmd : public instantiate_cmd_core {
public:
instantiate_nested_cmd():instantiate_cmd_core("dbg-instantiate-nested") {}
virtual char const * get_descr() const { return "instantiate the quantifier nested in the outermost quantifier, this command is used to test the instantiation procedure with quantifiers that contain free variables."; }
virtual void set_next_arg(cmd_context & ctx, expr * s) {

82
src/duality/duality_wrapper.cpp
View file

@ -41,8 +41,8 @@ namespace Duality {
params_ref p;
p.set_bool("proof", true); // this is currently useless
if(models)
p.set_bool("model", true);
p.set_bool("unsat_core", true);
p.set_bool("model", true);
p.set_bool("unsat_core", true);
bool mbqi = c.get_config().get().get_bool("mbqi",true);
p.set_bool("mbqi",mbqi); // just to test
p.set_str("mbqi.id","itp"); // use mbqi for quantifiers in interpolants
@ -57,7 +57,7 @@ namespace Duality {
m_mode = m().proof_mode();
}
expr context::constant(const std::string &name, const sort &ty){
expr context::constant(const std::string &name, const sort &ty){
symbol s = str_symbol(name.c_str());
return cook(m().mk_const(m().mk_const_decl(s, ty)));
}
@ -111,7 +111,7 @@ namespace Duality {
}
expr context::mki(family_id fid, ::decl_kind dk, int n, ::expr **args){
return cook(m().mk_app(fid, dk, 0, 0, n, (::expr **)args));
return cook(m().mk_app(fid, dk, 0, 0, n, (::expr **)args));
}
expr context::make(decl_kind op, const std::vector<expr> &args){
@ -168,9 +168,9 @@ namespace Duality {
expr_abstract(m(), 0, num_bound, VEC2PTR(bound_asts), to_expr(body.raw()), abs_body);
expr_ref result(m());
result = m().mk_quantifier(
op == Forall,
names.size(), VEC2PTR(types), VEC2PTR(names), abs_body.get(),
0,
op == Forall,
names.size(), VEC2PTR(types), VEC2PTR(names), abs_body.get(),
0,
::symbol(),
::symbol(),
0, 0,
@ -194,9 +194,9 @@ namespace Duality {
}
expr_ref result(m());
result = m().mk_quantifier(
op == Forall,
names.size(), VEC2PTR(types), VEC2PTR(names), to_expr(body.raw()),
0,
op == Forall,
names.size(), VEC2PTR(types), VEC2PTR(names), to_expr(body.raw()),
0,
::symbol(),
::symbol(),
0, 0,
@ -273,7 +273,7 @@ namespace Duality {
return OtherArray;
}
}
return Other;
}
@ -340,7 +340,7 @@ namespace Duality {
params p;
return simplify(p);
}
expr context::make_var(int idx, const sort &s){
::sort * a = to_sort(s.raw());
return cook(m().mk_var(idx,a));
@ -348,7 +348,7 @@ namespace Duality {
expr expr::qe_lite() const {
::qe_lite qe(m());
::qe_lite qe(m(), params_ref());
expr_ref result(to_expr(raw()),m());
proof_ref pf(m());
qe(result,pf);
@ -356,7 +356,7 @@ namespace Duality {
}
expr expr::qe_lite(const std::set<int> &idxs, bool index_of_bound) const {
::qe_lite qe(m());
::qe_lite qe(m(), params_ref());
expr_ref result(to_expr(raw()),m());
proof_ref pf(m());
uint_set uis;
@ -412,16 +412,16 @@ namespace Duality {
std::vector < ::sort * > _domain(domain.size());
for(unsigned i = 0; i < domain.size(); i++)
_domain[i] = to_sort(domain[i].raw());
::func_decl* d = m().mk_fresh_func_decl(prefix,
_domain.size(),
::func_decl* d = m().mk_fresh_func_decl(prefix,
_domain.size(),
VEC2PTR(_domain),
to_sort(range.raw()));
return func_decl(*this,d);
}
func_decl context::fresh_func_decl(char const * prefix, sort const & range){
::func_decl* d = m().mk_fresh_func_decl(prefix,
0,
::func_decl* d = m().mk_fresh_func_decl(prefix,
0,
0,
to_sort(range.raw()));
return func_decl(*this,d);
@ -462,30 +462,30 @@ namespace Duality {
incremental,
_theory.size(),
VEC2PTR(_theory));
if(lb == Z3_L_FALSE){
interpolants.resize(_interpolants.size());
for (unsigned i = 0; i < _interpolants.size(); ++i) {
interpolants[i] = expr(ctx(),_interpolants[i]);
}
}
}
if (_model) {
model = iz3wrapper::model(ctx(), _model);
}
if(_labels){
labels = _labels;
}
return lb;
}
#endif
static int linearize_assumptions(int num,
TermTree *assumptions,
std::vector<std::vector <expr> > &linear_assumptions,
std::vector<std::vector <expr> > &linear_assumptions,
std::vector<int> &parents){
for(unsigned i = 0; i < assumptions->getChildren().size(); i++)
num = linearize_assumptions(num, assumptions->getChildren()[i], linear_assumptions, parents);
@ -501,7 +501,7 @@ namespace Duality {
}
static int unlinearize_interpolants(int num,
TermTree* assumptions,
TermTree* assumptions,
const std::vector<expr> &interpolant,
TermTree * &tree_interpolant)
{
@ -522,7 +522,7 @@ namespace Duality {
literals &labels,
bool incremental
)
{
int size = assumptions->number(0);
std::vector<std::vector<expr> > linear_assumptions(size);
@ -540,36 +540,36 @@ namespace Duality {
ptr_vector< ::ast> _theory(theory.size());
for(unsigned i = 0; i < theory.size(); i++)
_theory[i] = theory[i];
if(!incremental){
push();
for(unsigned i = 0; i < linear_assumptions.size(); i++)
for(unsigned j = 0; j < linear_assumptions[i].size(); j++)
add(linear_assumptions[i][j]);
}
check_result res = unsat;
if(!m_solver->get_proof())
res = check();
if(res == unsat){
interpolation_options_struct opts;
if(weak_mode)
opts.set("weak","1");
opts.set("weak","1");
::ast *proof = m_solver->get_proof();
try {
iz3interpolate(m(),proof,_assumptions,_parents,_interpolants,_theory,&opts);
}
// If there's an interpolation bug, throw a char *
// exception so duality can catch it and restart.
// exception so duality can catch it and restart.
catch (const interpolation_failure &f) {
throw f.msg();
}
std::vector<expr> linearized_interpolants(_interpolants.size());
for(unsigned i = 0; i < _interpolants.size(); i++)
linearized_interpolants[i] = expr(ctx(),_interpolants[i]);
@ -585,13 +585,13 @@ namespace Duality {
model_ref _m;
m_solver->get_model(_m);
model = Duality::model(ctx(),_m.get());
#if 0
if(_labels){
labels = _labels;
}
#endif
if(!incremental)
pop();
@ -603,7 +603,7 @@ namespace Duality {
void interpolating_solver::SetWeakInterpolants(bool weak){
weak_mode = weak;
}
void interpolating_solver::SetPrintToFile(const std::string &filename){
print_filename = filename;
@ -618,14 +618,14 @@ namespace Duality {
void interpolating_solver::RemoveInterpolationAxiom(const expr & t){
// theory.remove(t);
}
const char *interpolating_solver::profile(){
// return Z3_interpolation_profile(ctx());
return "";
}
static void get_assumptions_rec(stl_ext::hash_set<ast> &memo, const proof &pf, std::vector<expr> &assumps){
if(memo.find(pf) != memo.end())return;
memo.insert(pf);
@ -657,7 +657,7 @@ namespace Duality {
model_smt2_pp(std::cout, m(), *m_model, 0);
std::cout << std::endl;
}
void model::show_hash() const {
std::ostringstream ss;
model_smt2_pp(ss, m(), *m_model, 0);

82
src/muz/base/dl_rule.cpp
View file

@ -47,14 +47,14 @@ Revision History:
namespace datalog {
rule_manager::rule_manager(context& ctx)
rule_manager::rule_manager(context& ctx)
: m(ctx.get_manager()),
m_ctx(ctx),
m_body(m),
m_head(m),
m_args(m),
m_hnf(m),
m_qe(m),
m_qe(m, params_ref()),
m_rwr(m),
m_ufproc(m) {}
@ -98,7 +98,7 @@ namespace datalog {
var_idx_set& rule_manager::finalize_collect_vars() {
unsigned sz = m_free_vars.size();
for (unsigned i = 0; i < sz; ++i) {
if (m_free_vars[i]) m_var_idx.insert(i);
if (m_free_vars[i]) m_var_idx.insert(i);
}
return m_var_idx;
}
@ -139,7 +139,7 @@ namespace datalog {
}
void rule_manager::mk_rule(expr* fml, proof* p, rule_set& rules, symbol const& name) {
void rule_manager::mk_rule(expr* fml, proof* p, rule_set& rules, symbol const& name) {
scoped_proof_mode _sc(m, m_ctx.generate_proof_trace()?PGM_FINE:PGM_DISABLED);
proof_ref pr(p, m);
expr_ref fml1(m);
@ -147,7 +147,7 @@ namespace datalog {
if (fml1 != fml && pr) {
pr = m.mk_asserted(fml1);
}
remove_labels(fml1, pr);
remove_labels(fml1, pr);
mk_rule_core(fml1, pr, rules, name);
}
@ -162,7 +162,7 @@ namespace datalog {
else {
is_negated.push_back(false);
}
}
}
}
void rule_manager::mk_rule_core(expr* fml, proof* p, rule_set& rules, symbol const& name) {
@ -170,7 +170,7 @@ namespace datalog {
proof_ref_vector prs(m);
m_hnf.reset();
m_hnf.set_name(name);
m_hnf(fml, p, fmls, prs);
for (unsigned i = 0; i < m_hnf.get_fresh_predicates().size(); ++i) {
m_ctx.register_predicate(m_hnf.get_fresh_predicates()[i], false);
@ -181,7 +181,7 @@ namespace datalog {
}
void rule_manager::mk_horn_rule(expr* fml, proof* p, rule_set& rules, symbol const& name) {
m_body.reset();
m_neg.reset();
unsigned index = extract_horn(fml, m_body, m_head);
@ -208,13 +208,13 @@ namespace datalog {
}
else if (is_quantifier(fml1)) {
p = m.mk_modus_ponens(p, m.mk_symmetry(m.mk_der(to_quantifier(fml1), fml)));
}
}
else {
p = m.mk_modus_ponens(p, m.mk_rewrite(fml, fml1));
}
}
if (m_ctx.fix_unbound_vars()) {
if (m_ctx.fix_unbound_vars()) {
fix_unbound_vars(r, true);
}
@ -242,10 +242,10 @@ namespace datalog {
for (unsigned i = 0; i < m_args.size(); ++i) {
body.push_back(ensure_app(m_args[i].get()));
}
}
}
else {
head = ensure_app(fml);
}
}
return index;
}
@ -262,12 +262,12 @@ namespace datalog {
func_decl* rule_manager::mk_query(expr* query, rule_set& rules) {
TRACE("dl", tout << mk_pp(query, m) << "\n";);
ptr_vector<sort> vars;
svector<symbol> names;
app_ref_vector body(m);
expr_ref q(m);
// Add implicit variables.
// Remove existential prefix.
bind_variables(query, false, q);
@ -278,7 +278,7 @@ namespace datalog {
m_free_vars(q);
vars.append(m_free_vars.size(), m_free_vars.c_ptr());
if (vars.contains(static_cast<sort*>(0))) {
var_subst sub(m, false);
var_subst sub(m, false);
expr_ref_vector args(m);
// [s0, 0, s2, ..]
// [0 -> 0, 1 -> x, 2 -> 1, ..]
@ -313,7 +313,7 @@ namespace datalog {
}
}
// we want outermost declared variable first to
// we want outermost declared variable first to
// follow order of quantified variables so we reverse vars.
while (vars.size() > names.size()) {
names.push_back(symbol(names.size()));
@ -321,9 +321,9 @@ namespace datalog {
vars.reverse();
names.reverse();
func_decl* qpred = m_ctx.mk_fresh_head_predicate(symbol("query"), symbol(), vars.size(), vars.c_ptr(), body_pred);
m_ctx.register_predicate(qpred, false);
m_ctx.register_predicate(qpred, false);
rules.set_output_predicate(qpred);
if (m_ctx.get_model_converter()) {
filter_model_converter* mc = alloc(filter_model_converter, m);
mc->insert(qpred);
@ -366,7 +366,7 @@ namespace datalog {
for (unsigned i = 0; i < r.size(); ++i) {
body.push_back(ensure_app(r[i].get()));
}
}
}
void rule_manager::hoist_compound(unsigned& num_bound, app_ref& fml, app_ref_vector& body) {
@ -440,7 +440,7 @@ namespace datalog {
if (is_quantifier(e)) {
q = to_quantifier(e);
return q->is_forall();
}
}
return false;
}
@ -454,7 +454,7 @@ namespace datalog {
return app_ref(m.mk_eq(e, m.mk_true()), m);
}
}
void rule_manager::check_app(expr* e) {
if (!is_app(e)) {
std::ostringstream out;
@ -481,7 +481,7 @@ namespace datalog {
bool has_neg = false;
for (unsigned i = 0; i < n; i++) {
bool is_neg = (is_negated != 0 && is_negated[i]);
bool is_neg = (is_negated != 0 && is_negated[i]);
app * curr = tail[i];
if (is_neg && !m_ctx.is_predicate(curr)) {
@ -571,7 +571,7 @@ namespace datalog {
case 1: fml = m.mk_implies(body[0].get(), fml); break;
default: fml = m.mk_implies(m.mk_and(body.size(), body.c_ptr()), fml); break;
}
m_free_vars(fml);
if (m_free_vars.empty()) {
return;
@ -579,7 +579,7 @@ namespace datalog {
svector<symbol> names;
used_symbols<> us;
m_free_vars.set_default_sort(m.mk_bool_sort());
us(fml);
m_free_vars.reverse();
for (unsigned j = 0, i = 0; i < m_free_vars.size(); ++j) {
@ -594,8 +594,8 @@ namespace datalog {
++i;
}
}
}
fml = m.mk_forall(m_free_vars.size(), m_free_vars.c_ptr(), names.c_ptr(), fml);
}
fml = m.mk_forall(m_free_vars.size(), m_free_vars.c_ptr(), names.c_ptr(), fml);
}
std::ostream& rule_manager::display_smt2(rule const& r, std::ostream & out) {
@ -749,7 +749,7 @@ namespace datalog {
quant_tail = m.mk_exists(q_var_cnt, qsorts.c_ptr(), qnames.c_ptr(), unbound_tail_pre_quant);
if (try_quantifier_elimination) {
TRACE("dl_rule_unbound_fix_pre_qe",
TRACE("dl_rule_unbound_fix_pre_qe",
tout<<"rule: ";
r->display(m_ctx, tout);
tout<<"tail with unbound vars: "<<mk_pp(unbound_tail, m)<<"\n";
@ -764,7 +764,7 @@ namespace datalog {
fixed_tail = quant_tail;
}
TRACE("dl_rule_unbound_fix",
TRACE("dl_rule_unbound_fix",
tout<<"rule: ";
r->display(m_ctx, tout);
tout<<"tail with unbound vars: "<<mk_pp(unbound_tail, m)<<"\n";
@ -796,7 +796,7 @@ namespace datalog {
to_formula(new_rule, fml);
scoped_proof _sc(m);
proof* p = m.mk_rewrite(m.get_fact(old_rule.get_proof()), fml);
new_rule.set_proof(m, m.mk_modus_ponens(old_rule.get_proof(), p));
new_rule.set_proof(m, m.mk_modus_ponens(old_rule.get_proof(), p));
}
}
@ -824,7 +824,7 @@ namespace datalog {
}
r = mk(new_head.get(), new_tail.size(), new_tail.c_ptr(), tail_neg.c_ptr(), r->name(), false);
// keep old variable indices around so we can compose with substitutions.
// keep old variable indices around so we can compose with substitutions.
// r->norm_vars(*this);
}
@ -835,7 +835,7 @@ namespace datalog {
void rule_manager::check_valid_head(expr * head) const {
SASSERT(head);
if (!m_ctx.is_predicate(head)) {
std::ostringstream out;
out << "Illegal head. The head predicate needs to be uninterpreted and registered (as recursive) " << mk_pp(head, m);
@ -874,14 +874,14 @@ namespace datalog {
m.get_allocator().deallocate(get_obj_size(n), this);
}
void rule::set_proof(ast_manager& m, proof* p) {
void rule::set_proof(ast_manager& m, proof* p) {
if (p) {
m.inc_ref(p);
m.inc_ref(p);
}
if (m_proof) {
m.dec_ref(m_proof);
m.dec_ref(m_proof);
}
m_proof = p;
m_proof = p;
}
bool rule::is_in_tail(const func_decl * p, bool only_positive) const {
@ -896,7 +896,7 @@ namespace datalog {
//
// non-predicates may appear only in the interpreted tail, it is therefore
// non-predicates may appear only in the interpreted tail, it is therefore
// sufficient only to check the tail.
//
bool rule_manager::has_uninterpreted_non_predicates(rule const& r, func_decl*& f) const {
@ -911,7 +911,7 @@ namespace datalog {
//
// Quantifiers may appear only in the interpreted tail, it is therefore
// Quantifiers may appear only in the interpreted tail, it is therefore
// sufficient only to check the interpreted tail.
//
void rule_manager::has_quantifiers(rule const& r, bool& existential, bool& universal) const {
@ -945,7 +945,7 @@ namespace datalog {
unsigned sz = get_tail_size();
for (unsigned i = 0; i < sz; ++i) {
used.process(get_tail(i));
}
}
}
void rule::get_vars(ast_manager& m, ptr_vector<sort>& sorts) const {
@ -994,13 +994,13 @@ namespace datalog {
app * old_tail = get_tail(i);
expr_ref new_tail_e(m);
vs(old_tail, subst_vals.size(), subst_vals.c_ptr(), new_tail_e);
bool sign = is_neg_tail(i);
bool sign = is_neg_tail(i);
m.inc_ref(new_tail_e);
m.dec_ref(old_tail);
m_tail[i] = TAG(app *, to_app(new_tail_e), sign);
}
}
void rule::display(context & ctx, std::ostream & out) const {
ast_manager & m = ctx.get_manager();
//out << mk_pp(m_head, m);
@ -1068,7 +1068,7 @@ namespace datalog {
}
};

4
src/muz/pdr/pdr_context.cpp
View file

@ -1007,7 +1007,7 @@ namespace pdr {
return m_cache[l];
}
void model_search::erase_children(model_node& n, bool backtrack) {
void model_search::erase_children(model_node& n, bool backtrack) {
ptr_vector<model_node> todo, nodes;
todo.append(n.children());
remove_goal(n);
@ -2241,7 +2241,7 @@ namespace pdr {
vars.append(aux_vars.size(), aux_vars.c_ptr());
scoped_ptr<expr_replacer> rep;
qe_lite qe(m);
qe_lite qe(m, m_params.p);
expr_ref phi1 = m_pm.mk_and(Phi);
qe(vars, phi1);
TRACE("pdr", tout << "Eliminated\n" << mk_pp(phi1, m) << "\n";);

206
src/muz/tab/tab_context.cpp
View file

@ -53,10 +53,10 @@ namespace tb {
app* t = to_app(_t);
if (m.is_value(s) && m.is_value(t)) {
IF_VERBOSE(2, verbose_stream() << "different:" << mk_pp(s, m) << " " << mk_pp(t, m) << "\n";);
IF_VERBOSE(2, verbose_stream() << "different:" << mk_pp(s, m) << " " << mk_pp(t, m) << "\n";);
return l_false;
}
if (m_dt.is_constructor(s) && m_dt.is_constructor(t)) {
if (s->get_decl() == t->get_decl()) {
lbool state = l_true;
@ -75,7 +75,7 @@ namespace tb {
return state;
}
else {
IF_VERBOSE(2, verbose_stream() << "different constructors:" << mk_pp(s, m) << " " << mk_pp(t, m) << "\n";);
IF_VERBOSE(2, verbose_stream() << "different constructors:" << mk_pp(s, m) << " " << mk_pp(t, m) << "\n";);
return l_false;
}
}
@ -109,7 +109,7 @@ namespace tb {
case l_false:
return false;
default:
conds.push_back(m.mk_eq(p, t));
conds.push_back(m.mk_eq(p, t));
return true;
}
}
@ -117,7 +117,7 @@ namespace tb {
public:
matcher(ast_manager& m): m(m), m_dt(m) {}
bool operator()(app* pat, app* term, substitution& s, expr_ref_vector& conds) {
// top-most term to match is a predicate. The predicates should be the same.
if (pat->get_decl() != term->get_decl() ||
@ -149,7 +149,7 @@ namespace tb {
}
}
return true;
}
}
};
class clause {
@ -165,22 +165,22 @@ namespace tb {
unsigned m_next_rule; // next rule to expand goal on
unsigned m_ref; // reference count
public:
public:
clause(ast_manager& m):
m_head(m),
m_predicates(m),
m_constraint(m),
m_seqno(0),
m_index(0),
m_index(0),
m_num_vars(0),
m_predicate_index(0),
m_predicate_index(0),
m_parent_rule(0),
m_parent_index(0),
m_next_rule(static_cast<unsigned>(-1)),
m_ref(0) {
}
void set_seqno(unsigned seqno) { m_seqno = seqno; }
unsigned get_seqno() const { return m_seqno; }
unsigned get_next_rule() const { return m_next_rule; }
@ -198,10 +198,10 @@ namespace tb {
void set_head(app* h) { m_head = h; }
unsigned get_parent_index() const { return m_parent_index; }
unsigned get_parent_rule() const { return m_parent_rule; }
void set_parent(ref<tb::clause>& parent) {
void set_parent(ref<tb::clause>& parent) {
m_parent_index = parent->get_index();
m_parent_rule = parent->get_next_rule();
}
}
expr_ref get_body() const {
ast_manager& m = get_manager();
@ -247,7 +247,7 @@ namespace tb {
}
if (!vars.empty()) {
body = m.mk_forall(vars.size(), vars.c_ptr(), names.c_ptr(), body);
}
}
return body;
}
@ -273,18 +273,18 @@ namespace tb {
reduce_equalities();
// IF_VERBOSE(1, display(verbose_stream()););
}
void inc_ref() {
m_ref++;
}
void dec_ref() {
--m_ref;
if (m_ref == 0) {
dealloc(this);
}
}
void display(std::ostream& out) const {
ast_manager& m = m_head.get_manager();
expr_ref_vector fmls(m);
@ -304,7 +304,7 @@ namespace tb {
}
out << mk_pp(fml, m) << "\n";
}
private:
ast_manager& get_manager() const { return m_head.get_manager(); }
@ -314,7 +314,7 @@ namespace tb {
// - m_head - head predicate
// - m_predicates - auxiliary predicates in body.
// - m_constraint - side constraint
//
//
void init_from_rule(datalog::rule_ref const& r) {
ast_manager& m = get_manager();
expr_ref_vector fmls(m);
@ -328,7 +328,7 @@ namespace tb {
m_predicates.reset();
for (unsigned i = 0; i < utsz; ++i) {
m_predicates.push_back(r->get_tail(i));
}
}
bool_rewriter(m).mk_and(fmls.size(), fmls.c_ptr(), m_constraint);
}
@ -348,13 +348,13 @@ namespace tb {
if (get_subst(rw, subst, i, fmls)) {
fmls[i] = m.mk_true();
}
}
}
subst.apply(1, delta, expr_offset(m_head, 0), tmp);
m_head = to_app(tmp);
for (unsigned i = 0; i < m_predicates.size(); ++i) {
subst.apply(1, delta, expr_offset(m_predicates[i].get(), 0), tmp);
m_predicates[i] = to_app(tmp);
}
}
bool_rewriter(m).mk_and(fmls.size(), fmls.c_ptr(), m_constraint);
subst.apply(1, delta, expr_offset(m_constraint, 0), m_constraint);
rw(m_constraint);
@ -404,7 +404,7 @@ namespace tb {
throw non_constructor();
}
}
void operator()(var* v) { }
void operator()(var* v) { }
void operator()(quantifier* ) {
throw non_constructor();
}
@ -421,7 +421,7 @@ namespace tb {
return true;
}
};
};
// rules
class rules {
@ -456,7 +456,7 @@ namespace tb {
func_decl* f = g->get_decl();
map::obj_map_entry* e = m_index.insert_if_not_there2(f, unsigned_vector());
SASSERT(e);
e->get_data().m_value.push_back(idx);
e->get_data().m_value.push_back(idx);
}
unsigned get_num_rules(func_decl* p) const {
@ -475,14 +475,14 @@ namespace tb {
for (; it != end; ++it) {
decls.push_back(it->m_key);
}
}
}
ref<clause> get_rule(func_decl* p, unsigned idx) const {
map::obj_map_entry* e = m_index.find_core(p);
SASSERT(p);
unsigned rule_id = e->get_data().get_value()[idx];
return m_rules[rule_id];
}
}
private:
void reset() {
m_rules.reset();
@ -509,7 +509,7 @@ namespace tb {
bool_rewriter m_rw;
smt_params m_fparams;
smt::kernel m_solver;
public:
index(ast_manager& m):
m(m),
@ -520,7 +520,7 @@ namespace tb {
m_matcher(m),
m_refs(m),
m_subst(m),
m_qe(m),
m_qe(m, params_ref()),
m_rw(m),
m_solver(m, m_fparams) {}
@ -544,7 +544,7 @@ namespace tb {
}
private:
void setup(clause const& g) {
m_preds.reset();
m_refs.reset();
@ -569,8 +569,8 @@ namespace tb {
}
vs(g.get_constraint(), vars.size(), vars.c_ptr(), fml);
fmls.push_back(fml);
m_precond = m.mk_and(fmls.size(), fmls.c_ptr());
IF_VERBOSE(2,
m_precond = m.mk_and(fmls.size(), fmls.c_ptr());
IF_VERBOSE(2,
verbose_stream() << "setup-match: ";
for (unsigned i = 0; i < m_preds.size(); ++i) {
verbose_stream() << mk_pp(m_preds[i].get(), m) << " ";
@ -587,18 +587,18 @@ namespace tb {
return true;
}
}
return false;
return false;
}
//
// check that each predicate in r is matched by some predicate in premise.
// for now: skip multiple matches within the same rule (incomplete).
//
bool match_rule(unsigned rule_index) {
clause const& g = *m_index[rule_index];
clause const& g = *m_index[rule_index];
m_sideconds.reset();
m_subst.reset();
m_subst.reserve(2, g.get_num_vars());
IF_VERBOSE(2, g.display(verbose_stream() << "try-match\n"););
return match_head(g);
@ -628,9 +628,9 @@ namespace tb {
}
verbose_stream() << mk_pp(q, m) << " = " << mk_pp(p, m) << "\n";
);
if (q->get_decl() == p->get_decl() &&
if (q->get_decl() == p->get_decl() &&
m_matcher(q, p, m_subst, m_sideconds) &&
match_predicates(predicate_index + 1, g)) {
return true;
@ -646,7 +646,7 @@ namespace tb {
expr_ref q(m), postcond(m);
expr_ref_vector fmls(m_sideconds);
m_subst.reset_cache();
for (unsigned i = 0; !m.canceled() && i < fmls.size(); ++i) {
m_subst.apply(2, deltas, expr_offset(fmls[i].get(), 0), q);
fmls[i] = q;
@ -680,7 +680,7 @@ namespace tb {
verbose_stream() << "check: " << mk_pp(postcond, m, 7 + g.get_num_predicates()) << "\n";);
if (!is_ground(postcond)) {
IF_VERBOSE(1, verbose_stream() << "TBD: non-ground\n"
IF_VERBOSE(1, verbose_stream() << "TBD: non-ground\n"
<< mk_pp(postcond, m) << "\n";
m_clause->display(verbose_stream());
verbose_stream() << "\n=>\n";
@ -743,7 +743,7 @@ namespace tb {
double m_weight_multiply;
unsigned m_update_frequency;
unsigned m_next_update;
public:
selection(datalog::context& ctx):
@ -766,7 +766,7 @@ namespace tb {
scores.reset();
basic_score_predicate(p, scores);
insert_score(p->get_decl(), scores);
}
}
normalize_scores(rs);
}
@ -783,7 +783,7 @@ namespace tb {
default:
return weight_select(g);
}
}
}
void reset() {
@ -867,8 +867,8 @@ namespace tb {
}
}
IF_VERBOSE(1, verbose_stream() << "select:" << result << "\n";);
return result;
return result;
}
unsigned basic_weight_select(clause const& g) {
@ -957,7 +957,7 @@ namespace tb {
}
}
double score_predicate(app* p) {
double score = 1;
if (find_score(p, score)) {
@ -1031,7 +1031,7 @@ namespace tb {
}
else {
m_score_map.insert(f, scores);
}
}
}
};
@ -1044,15 +1044,15 @@ namespace tb {
expr_ref_vector m_sub1;
expr_ref_vector m_sub2;
public:
unifier(ast_manager& m):
m(m),
unifier(ast_manager& m):
m(m),
m_unifier(m),
m_S1(m),
m_S2(m, false),
m_rename(m),
m_sub1(m),
m_sub1(m),
m_sub2(m) {}
bool operator()(ref<clause>& tgt, unsigned idx, ref<clause>& src, bool compute_subst, ref<clause>& result) {
return unify(*tgt, idx, *src, compute_subst, result);
}
@ -1066,12 +1066,12 @@ namespace tb {
}
}
bool unify(clause const& tgt, unsigned idx, clause const& src, bool compute_subst, ref<clause>& result) {
qe_lite qe(m);
bool unify(clause const& tgt, unsigned idx, clause const& src, bool compute_subst, ref<clause>& result) {
qe_lite qe(m, params_ref());
reset();
SASSERT(tgt.get_predicate(idx)->get_decl() == src.get_decl());
unsigned var_cnt = std::max(tgt.get_num_vars(), src.get_num_vars());
m_S1.reserve(2, var_cnt);
m_S1.reserve(2, var_cnt);
if (!m_unifier(tgt.get_predicate(idx), src.get_head(), m_S1)) {
return false;
}
@ -1080,7 +1080,7 @@ namespace tb {
app_ref head(m);
result = alloc(clause, m);
unsigned delta[2] = { 0, var_cnt };
m_S1.apply(2, delta, expr_offset(tgt.get_head(), 0), tmp);
m_S1.apply(2, delta, expr_offset(tgt.get_head(), 0), tmp);
head = to_app(tmp);
for (unsigned i = 0; i < tgt.get_num_predicates(); ++i) {
if (i != idx) {
@ -1096,7 +1096,7 @@ namespace tb {
}
m_S1.apply(2, delta, expr_offset(tgt.get_constraint(), 0), tmp);
m_S1.apply(2, delta, expr_offset(src.get_constraint(), 1), tmp2);
constraint = m.mk_and(tmp, tmp2);
constraint = m.mk_and(tmp, tmp2);
// perform trival quantifier-elimination:
uint_set index_set;
@ -1114,7 +1114,7 @@ namespace tb {
if (m.is_false(constraint)) {
return false;
}
// initialize rule.
result->init(head, predicates, constraint);
ptr_vector<sort> vars;
@ -1147,10 +1147,10 @@ namespace tb {
extract_subst(delta, src, 1);
}
// init result using head, predicates, constraint
return true;
return true;
}
private:
void reset() {
m_S1.reset();
@ -1175,9 +1175,9 @@ namespace tb {
else {
insert_subst(offset, m.mk_true());
}
}
}
}
void insert_subst(unsigned offset, expr* e) {
if (offset == 0) {
m_sub1.push_back(e);
@ -1201,7 +1201,7 @@ namespace tb {
//
// Given a clause
// Given a clause
// P(s) :- P(t), Phi(x).
// Compute the clauses:
// acc: P(s) :- Delta(z,t), P(z), Phi(x).
@ -1237,7 +1237,7 @@ namespace tb {
head = m.mk_app(delta, zszs.size(), zszs.c_ptr());
for (unsigned i = 0; i < zs.size(); ++i) {
zszs[i+zs.size()] = q->get_arg(i);
}
}
pred = m.mk_app(delta, zszs.size(), zszs.c_ptr());
preds.push_back(pred);
for (unsigned i = 1; i < g.get_num_predicates(); ++i) {
@ -1247,28 +1247,28 @@ namespace tb {
preds.push_back(m.mk_app(q->get_decl(), zs.size(), zs.c_ptr()));
acc->init(p, preds, g.get_constraint());
IF_VERBOSE(1,
IF_VERBOSE(1,
delta1->display(verbose_stream() << "delta1:\n");
delta2->display(verbose_stream() << "delta2:\n");
acc->display(verbose_stream() << "acc:\n"););
}
//
//
// Given a sequence of clauses and inference rules
// compute a super-predicate and auxiliary clauses.
//
//
// P1(x) :- P2(y), R(z)
// P2(y) :- P3(z), T(u)
// P3(z) :- P1(x), U(v)
// =>
// P1(x) :- P1(x), R(z), T(u), U(v)
//
//
ref<clause> resolve_rules(unsigned num_clauses, clause*const* clauses, unsigned const* positions) {
ref<clause> result = clauses[0];
ref<clause> tmp;
unsigned offset = 0;
for (unsigned i = 0; i + 1 < num_clauses; ++i) {
for (unsigned i = 0; i + 1 < num_clauses; ++i) {
clause const& cl = *clauses[i+1];
offset += positions[i];
VERIFY (m_unifier.unify(*result, offset, cl, false, tmp));
@ -1276,7 +1276,7 @@ namespace tb {
}
return result;
}
private:
@ -1286,7 +1286,7 @@ namespace tb {
unsigned num_vars = g.get_num_vars();
for (unsigned i = 0; i < p->get_num_args(); ++i) {
result.push_back(m.mk_var(num_vars+i, m.get_sort(p->get_arg(i))));
}
}
return result;
}
};
@ -1341,7 +1341,7 @@ namespace datalog {
uint_set m_displayed_rules;
public:
imp(context& ctx):
m_ctx(ctx),
m_ctx(ctx),
m(ctx.get_manager()),
rm(ctx.get_rule_manager()),
m_index(m),
@ -1358,7 +1358,7 @@ namespace datalog {
m_fparams.m_timeout = 1000;
}
~imp() {}
~imp() {}
lbool query(expr* query) {
m_ctx.ensure_opened();
@ -1378,7 +1378,7 @@ namespace datalog {
IF_VERBOSE(1, display_clause(*get_clause(), verbose_stream() << "g" << get_clause()->get_seqno() << " "););
return run();
}
void cleanup() {
m_clauses.reset();
}
@ -1400,7 +1400,7 @@ namespace datalog {
expr_ref get_answer() const {
switch(m_status) {
case l_undef:
case l_undef:
UNREACHABLE();
return expr_ref(m.mk_false(), m);
case l_true: {
@ -1415,7 +1415,7 @@ namespace datalog {
return expr_ref(m.mk_true(), m);
}
private:
void select_predicate() {
tb::clause & g = *get_clause();
unsigned num_predicates = g.get_num_predicates();
@ -1430,17 +1430,17 @@ namespace datalog {
IF_VERBOSE(2, verbose_stream() << mk_pp(g.get_predicate(pi), m) << "\n";);
}
}
void apply_rule(ref<tb::clause>& r) {
ref<tb::clause> clause = get_clause();
ref<tb::clause> next_clause;
ref<tb::clause> next_clause;
if (m_unifier(clause, clause->get_predicate_index(), r, false, next_clause) &&
!query_is_tautology(*next_clause)) {
init_clause(next_clause);
unsigned subsumer = 0;
IF_VERBOSE(1,
IF_VERBOSE(1,
display_rule(*clause, verbose_stream());
display_premise(*clause,
display_premise(*clause,
verbose_stream() << "g" << next_clause->get_seqno() << " ");
display_clause(*next_clause, verbose_stream());
);
@ -1462,8 +1462,8 @@ namespace datalog {
m_instruction = tb::SELECT_RULE;
}
}
void select_rule() {
void select_rule() {
tb::clause& g = *get_clause();
g.inc_next_rule();
unsigned pi = g.get_predicate_index();
@ -1481,7 +1481,7 @@ namespace datalog {
void backtrack() {
SASSERT(!m_clauses.empty());
m_clauses.pop_back();
m_clauses.pop_back();
if (m_clauses.empty()) {
m_instruction = tb::SATISFIABLE;
}
@ -1500,16 +1500,16 @@ namespace datalog {
return l_undef;
}
switch(m_instruction) {
case tb::SELECT_PREDICATE:
select_predicate();
case tb::SELECT_PREDICATE:
select_predicate();
break;
case tb::SELECT_RULE:
select_rule();
case tb::SELECT_RULE:
select_rule();
break;
case tb::BACKTRACK:
backtrack();
break;
case tb::SATISFIABLE:
case tb::SATISFIABLE:
m_status = l_false;
return l_false;
case tb::UNSATISFIABLE:
@ -1522,18 +1522,18 @@ namespace datalog {
return l_undef;
}
}
}
}
bool query_is_tautology(tb::clause const& g) {
expr_ref fml = g.to_formula();
fml = m.mk_not(fml);
m_solver.push();
m_solver.assert_expr(fml);
lbool is_sat = m_solver.check();
lbool is_sat = m_solver.check();
m_solver.pop(1);
TRACE("dl", tout << is_sat << ":\n" << mk_pp(fml, m) << "\n";);
return l_false == is_sat;
}
@ -1560,7 +1560,7 @@ namespace datalog {
void display_premise(tb::clause& p, std::ostream& out) {
func_decl* f = p.get_predicate(p.get_predicate_index())->get_decl();
out << "{g" << p.get_seqno() << " " << f->get_name() << " pos: "
out << "{g" << p.get_seqno() << " " << f->get_name() << " pos: "
<< p.get_predicate_index() << " rule: " << p.get_next_rule() << "}\n";
}
@ -1576,21 +1576,21 @@ namespace datalog {
ref<tb::clause> replayed_clause;
replace_proof_converter pc(m);
// clause is a empty clause.
// clause is a empty clause.
// Pretend it is asserted.
// It gets replaced by premises.
SASSERT(clause->get_num_predicates() == 0);
SASSERT(clause->get_num_predicates() == 0);
expr_ref root = clause->to_formula();
vector<expr_ref_vector> substs;
while (0 != clause->get_index()) {
SASSERT(clause->get_parent_index() < clause->get_index());
while (0 != clause->get_index()) {
SASSERT(clause->get_parent_index() < clause->get_index());
unsigned p_index = clause->get_parent_index();
unsigned p_rule = clause->get_parent_rule();
ref<tb::clause> parent = m_clauses[p_index];
unsigned pi = parent->get_predicate_index();
func_decl* pred = parent->get_predicate(pi)->get_decl();
ref<tb::clause> rl = m_rules.get_rule(pred, p_rule);
ref<tb::clause> rl = m_rules.get_rule(pred, p_rule);
VERIFY(m_unifier(parent, parent->get_predicate_index(), rl, true, replayed_clause));
expr_ref_vector s1(m_unifier.get_rule_subst(true));
expr_ref_vector s2(m_unifier.get_rule_subst(false));
@ -1614,36 +1614,36 @@ namespace datalog {
}
expr_ref body = clause.get_body();
var_subst vs(m, false);
vs(body, subst.size(), subst.c_ptr(), body);
vs(body, subst.size(), subst.c_ptr(), body);
out << mk_pp(body, m) << "\n";
}
void resolve_rule(replace_proof_converter& pc, tb::clause const& r1, tb::clause const& r2,
void resolve_rule(replace_proof_converter& pc, tb::clause const& r1, tb::clause const& r2,
expr_ref_vector const& s1, expr_ref_vector const& s2, tb::clause const& res) const {
unsigned idx = r1.get_predicate_index();
expr_ref fml = res.to_formula();
vector<expr_ref_vector> substs;
svector<std::pair<unsigned, unsigned> > positions;
substs.push_back(s1);
substs.push_back(s2);
substs.push_back(s2);
scoped_proof _sc(m);
proof_ref pr(m);
proof_ref_vector premises(m);
premises.push_back(m.mk_asserted(r1.to_formula()));
premises.push_back(m.mk_asserted(r2.to_formula()));
positions.push_back(std::make_pair(idx+1, 0));
positions.push_back(std::make_pair(idx+1, 0));
pr = m.mk_hyper_resolve(2, premises.c_ptr(), fml, positions, substs);
pc.insert(pr);
}
}
};
tab::tab(context& ctx):
datalog::engine_base(ctx.get_manager(),"tabulation"),
m_imp(alloc(imp, ctx)) {
m_imp(alloc(imp, ctx)) {
}
tab::~tab() {
dealloc(m_imp);
}
}
lbool tab::query(expr* query) {
return m_imp->query(query);
}

2
src/opt/opt_params.pyg
View file

@ -5,6 +5,8 @@ def_module_params('opt',
('maxsat_engine', SYMBOL, 'maxres', "select engine for maxsat: 'core_maxsat', 'wmax', 'maxres', 'pd-maxres'"),
('priority', SYMBOL, 'lex', "select how to priortize objectives: 'lex' (lexicographic), 'pareto', or 'box'"),
('dump_benchmarks', BOOL, False, 'dump benchmarks for profiling'),
('timeout', UINT, UINT_MAX, 'timeout (in milliseconds) (UINT_MAX and 0 mean no timeout)'),
('rlimit', UINT, 0, 'resource limit (0 means no limit)'),
('print_model', BOOL, False, 'display model for satisfiable constraints'),
('enable_sls', BOOL, False, 'enable SLS tuning during weighted maxsast'),
('enable_sat', BOOL, True, 'enable the new SAT core for propositional constraints'),

575
src/qe/qe_lite.cpp
View file

File diff suppressed because it is too large Load diff

10
src/qe/qe_lite.h
View file

@ -7,7 +7,7 @@ Module Name:
Abstract:
Light weight partial quantifier-elimination procedures
Light weight partial quantifier-elimination procedures
Author:
@ -31,14 +31,14 @@ class qe_lite {
class impl;
impl * m_impl;
public:
qe_lite(ast_manager& m);
qe_lite(ast_manager & m, params_ref const & p);
~qe_lite();
/**
\brief
Apply light-weight quantifier elimination
on constants provided as vector of variables.
Apply light-weight quantifier elimination
on constants provided as vector of variables.
Return the updated formula and updated set of variables that were not eliminated.
*/
@ -66,4 +66,4 @@ tactic * mk_qe_lite_tactic(ast_manager & m, params_ref const & p = params_ref())
ADD_TACTIC("qe-light", "apply light-weight quantifier elimination.", "mk_qe_lite_tactic(m, p)")
*/
#endif
#endif

3
src/sat/sat_simplifier.cpp
View file

@ -154,6 +154,8 @@ namespace sat {
if (!m_subsumption && !m_elim_blocked_clauses && !m_resolution)
return;
// solver::scoped_disable_checkpoint _scoped_disable_checkpoint(s);
initialize();
CASSERT("sat_solver", s.check_invariant());
@ -167,7 +169,6 @@ namespace sat {
CASSERT("sat_solver", s.check_invariant());
m_need_cleanup = false;
m_use_list.init(s.num_vars());
init_visited();
m_learned_in_use_lists = false;
if (learned) {
register_clauses(s.m_learned);

1
src/sat/sat_solver.cpp
View file

@ -33,6 +33,7 @@ namespace sat {
solver::solver(params_ref const & p, reslimit& l, extension * ext):
m_rlimit(l),
m_checkpoint_enabled(true),
m_config(p),
m_ext(ext),
m_par(0),

12
src/sat/sat_solver.h
View file

@ -72,6 +72,7 @@ namespace sat {
struct abort_solver {};
protected:
reslimit& m_rlimit;
bool m_checkpoint_enabled;
config m_config;
stats m_stats;
extension * m_ext;
@ -214,6 +215,16 @@ namespace sat {
}
}
};
class scoped_disable_checkpoint {
solver& s;
public:
scoped_disable_checkpoint(solver& s): s(s) {
s.m_checkpoint_enabled = false;
}
~scoped_disable_checkpoint() {
s.m_checkpoint_enabled = true;
}
};
unsigned select_watch_lit(clause const & cls, unsigned starting_at) const;
unsigned select_learned_watch_lit(clause const & cls) const;
bool simplify_clause(unsigned & num_lits, literal * lits) const;
@ -257,6 +268,7 @@ namespace sat {
lbool status(clause const & c) const;
clause_offset get_offset(clause const & c) const { return m_cls_allocator.get_offset(&c); }
void checkpoint() {
if (!m_checkpoint_enabled) return;
if (!m_rlimit.inc()) {
m_mc.reset();
m_model_is_current = false;

22
src/smt/old_interval.cpp
View file

@ -81,7 +81,7 @@ ext_numeral & ext_numeral::operator*=(ext_numeral const & other) {
m_value.reset();
return *this;
}
if (is_infinite() || other.is_infinite()) {
if (sign() == other.sign())
m_kind = PLUS_INFINITY;
@ -203,7 +203,7 @@ interval::interval(v_dependency_manager & m, rational const & val, v_dependency
m_lower_dep(l_dep),
m_upper_dep(u_dep) {
}
/**
\brief Create intervals (-oo, val], (-oo, val), [val, oo), (val, oo)
*/
@ -271,8 +271,8 @@ interval & interval::operator-=(interval const & other) {
return operator+=(tmp);
}
v_dependency * interval::join(v_dependency * d1, v_dependency * d2, v_dependency * d3, v_dependency * d4) {
return m_manager.mk_join(m_manager.mk_join(d1, d2), m_manager.mk_join(d3,d4));
v_dependency * interval::join(v_dependency * d1, v_dependency * d2, v_dependency * d3, v_dependency * d4) {
return m_manager.mk_join(m_manager.mk_join(d1, d2), m_manager.mk_join(d3,d4));
}
/**
@ -318,7 +318,7 @@ interval & interval::operator*=(interval const & other) {
v_dependency * d_d = other.m_upper_dep;
TRACE("interval_bug", tout << "operator*= " << *this << " " << other << "\n";);
if (is_N()) {
if (other.is_N()) {
// x <= b <= 0, y <= d <= 0 --> b*d <= x*y
@ -452,7 +452,7 @@ interval & interval::operator*=(interval const & other) {
m_upper_dep = m_upper.is_infinite() ? 0 : join(b_d, d_d, a_d);
}
else {
// 0 <= a <= x, 0 <= c <= y --> a*c <= x*y
// 0 <= a <= x, 0 <= c <= y --> a*c <= x*y
// x <= b, y <= d --> x*y <= b*d (uses the fact that x is pos (a is not negative) or y is pos (c is not negative))
TRACE("interval_bug", tout << "(P, P)\n";);
SASSERT(other.is_P());
@ -467,7 +467,7 @@ interval & interval::operator*=(interval const & other) {
}
}
TRACE("interval_bug", tout << "operator*= result: " << *this << "\n";);
CTRACE("interval", !(!(contains_zero1 || contains_zero2) || contains_zero()),
CTRACE("interval", !(!(contains_zero1 || contains_zero2) || contains_zero()),
tout << "contains_zero1: " << contains_zero1 << ", contains_zero2: " << contains_zero2 << ", contains_zero(): " << contains_zero() << "\n";);
SASSERT(!(contains_zero1 || contains_zero2) || contains_zero());
return *this;
@ -482,7 +482,7 @@ bool interval::contains_zero() const {
tout << "m_upper.is_zero: " << m_upper.is_zero() << "\n";
tout << "m_upper_open: " << m_upper_open << "\n";
tout << "result: " << ((m_lower.is_neg() || (m_lower.is_zero() && !m_lower_open)) && (m_upper.is_pos() || (m_upper.is_zero() && !m_upper_open))) << "\n";);
return
return
(m_lower.is_neg() || (m_lower.is_zero() && !m_lower_open)) &&
(m_upper.is_pos() || (m_upper.is_zero() && !m_upper_open));
}
@ -510,7 +510,7 @@ interval & interval::inv() {
ext_numeral new_upper;
if (m_lower.is_zero()) {
SASSERT(m_lower_open);
ext_numeral plus_infinity(true);
ext_numeral plus_infinity(true);
new_upper = plus_infinity;
}
else {
@ -595,7 +595,7 @@ void interval::expt(unsigned n) {
else if (m_upper.is_neg()) {
// [l, u]^n = [u^n, l^n] if u < 0
// a <= x <= b < 0 --> x^n <= a^n (use lower and upper bound -- need the fact that x is negative)
// x <= b < 0 --> b^n <= x^n
// x <= b < 0 --> b^n <= x^n
std::swap(m_lower, m_upper);
std::swap(m_lower_open, m_upper_open);
std::swap(m_lower_dep, m_upper_dep);
@ -614,7 +614,7 @@ void interval::expt(unsigned n) {
m_upper = m_lower;
m_upper_open = m_lower_open;
}
m_upper_dep = m_upper.is_infinite() ? 0 : m_manager.mk_join(m_lower_dep, m_upper_dep);
m_upper_dep = m_upper.is_infinite() ? 0 : m_manager.mk_join(m_lower_dep, m_upper_dep);
m_lower = ext_numeral(0);
m_lower_open = false;
m_lower_dep = 0;

3
src/smt/params/smt_params_helper.pyg
View file

@ -64,5 +64,6 @@ def_module_params(module_name='smt',
('core.validate', BOOL, False, 'validate unsat core produced by SMT context'),
('core.minimize', BOOL, False, 'minimize unsat core produced by SMT context'),
('core.extend_patterns', BOOL, False, 'extend unsat core with literals that trigger (potential) quantifier instances'),
('core.extend_patterns.max_distance', UINT, UINT_MAX, 'limits the distance of a pattern-extended unsat core')
('core.extend_patterns.max_distance', UINT, UINT_MAX, 'limits the distance of a pattern-extended unsat core'),
('core.extend_nonlocal_patterns', BOOL, False, 'extend unsat cores with literals that have quantifiers with patterns that contain symbols which are not in the quantifier\'s body')
))

59
src/smt/smt_context.cpp
View file

@ -3072,11 +3072,11 @@ namespace smt {
m_assumptions.reset();
}
void context::mk_unsat_core() {
lbool context::mk_unsat_core() {
SASSERT(inconsistent());
if (!tracking_assumptions()) {
SASSERT(m_assumptions.empty());
return;
return l_false;
}
uint_set already_found_assumptions;
literal_vector::const_iterator it = m_conflict_resolution->begin_unsat_core();
@ -3101,7 +3101,17 @@ namespace smt {
for (unsigned i = 0; i < sz; i++) {
tout << mk_pp(m_unsat_core.get(i), m_manager) << "\n";
});
validate_unsat_core();
validate_unsat_core();
// theory validation of unsat core
ptr_vector<theory>::iterator th_it = m_theory_set.begin();
ptr_vector<theory>::iterator th_end = m_theory_set.end();
for (; th_it != th_end; ++th_it) {
lbool theory_result = (*th_it)->validate_unsat_core(m_unsat_core);
if (theory_result == l_undef) {
return l_undef;
}
}
return l_false;
}
/**
@ -3144,6 +3154,14 @@ namespace smt {
SASSERT(m_scope_lvl == 0);
SASSERT(!m_setup.already_configured());
setup_context(m_fparams.m_auto_config);
expr_ref_vector theory_assumptions(m_manager);
add_theory_assumptions(theory_assumptions);
if (!theory_assumptions.empty()) {
TRACE("search", tout << "Adding theory assumptions to context" << std::endl;);
return check(theory_assumptions.size(), theory_assumptions.c_ptr(), reset_cancel, true);
}
internalize_assertions();
lbool r = l_undef;
if (m_asserted_formulas.inconsistent()) {
@ -3205,7 +3223,15 @@ namespace smt {
(*it)->setup();
}
lbool context::check(unsigned num_assumptions, expr * const * assumptions, bool reset_cancel) {
void context::add_theory_assumptions(expr_ref_vector & theory_assumptions) {
ptr_vector<theory>::iterator it = m_theory_set.begin();
ptr_vector<theory>::iterator end = m_theory_set.end();
for (; it != end; ++it) {
(*it)->add_theory_assumptions(theory_assumptions);
}
}
lbool context::check(unsigned ext_num_assumptions, expr * const * ext_assumptions, bool reset_cancel, bool already_did_theory_assumptions) {
m_stats.m_num_checks++;
TRACE("check_bug", tout << "STARTING check(num_assumptions, assumptions)\n";
tout << "inconsistent: " << inconsistent() << ", m_unsat_core.empty(): " << m_unsat_core.empty() << "\n";
@ -3216,6 +3242,15 @@ namespace smt {
m_unsat_core.reset();
if (!check_preamble(reset_cancel))
return l_undef;
expr_ref_vector all_assumptions(m_manager, ext_num_assumptions, ext_assumptions);
if (!already_did_theory_assumptions) {
add_theory_assumptions(all_assumptions);
}
unsigned num_assumptions = all_assumptions.size();
expr * const * assumptions = all_assumptions.c_ptr();
if (!validate_assumptions(num_assumptions, assumptions))
return l_undef;
TRACE("check_bug", tout << "inconsistent: " << inconsistent() << ", m_unsat_core.empty(): " << m_unsat_core.empty() << "\n";);
@ -3239,13 +3274,21 @@ namespace smt {
TRACE("after_internalization", display(tout););
if (inconsistent()) {
VERIFY(!resolve_conflict()); // build the proof
mk_unsat_core();
r = l_false;
lbool result = mk_unsat_core();
if (result == l_undef) {
r = l_undef;
} else {
r = l_false;
}
}
else {
r = search();
if (r == l_false)
mk_unsat_core();
if (r == l_false) {
lbool result = mk_unsat_core();
if (result == l_undef) {
r = l_undef;
}
}
}
}
}

6
src/smt/smt_context.h
View file

@ -1059,7 +1059,9 @@ namespace smt {
void reset_assumptions();
void mk_unsat_core();
void add_theory_assumptions(expr_ref_vector & theory_assumptions);
lbool mk_unsat_core();
void validate_unsat_core();
@ -1444,7 +1446,7 @@ namespace smt {
void pop(unsigned num_scopes);
lbool check(unsigned num_assumptions = 0, expr * const * assumptions = 0, bool reset_cancel = true);
lbool check(unsigned num_assumptions = 0, expr * const * assumptions = 0, bool reset_cancel = true, bool already_did_theory_assumptions = false);
lbool get_consequences(expr_ref_vector const& assumptions, expr_ref_vector const& vars, expr_ref_vector& conseq, expr_ref_vector& unfixed);

3
src/smt/smt_context_inv.cpp
View file

@ -433,6 +433,9 @@ namespace smt {
if (!is_ground(n)) {
continue;
}
if (is_quantifier(n) && m.is_rec_fun_def(to_quantifier(n))) {
continue;
}
switch (get_assignment(*it)) {
case l_undef:
break;

12
src/smt/smt_justification.cpp
View file

@ -246,13 +246,15 @@ namespace smt {
simple_justification::simple_justification(region & r, unsigned num_lits, literal const * lits):
m_num_literals(num_lits) {
m_literals = new (r) literal[num_lits];
memcpy(m_literals, lits, sizeof(literal) * num_lits);
if (num_lits != 0) {
m_literals = new (r) literal[num_lits];
memcpy(m_literals, lits, sizeof(literal) * num_lits);
#ifdef Z3DEBUG
for (unsigned i = 0; i < num_lits; i++) {
SASSERT(lits[i] != null_literal);
}
for (unsigned i = 0; i < num_lits; i++) {
SASSERT(lits[i] != null_literal);
}
#endif
}
}
void simple_justification::get_antecedents(conflict_resolution & cr) {

62
src/smt/smt_model_checker.cpp
View file

@ -316,7 +316,7 @@ namespace smt {
return false;
}
bool model_checker::check_rec_fun(quantifier* q) {
bool model_checker::check_rec_fun(quantifier* q, bool strict_rec_fun) {
TRACE("model_checker", tout << mk_pp(q, m) << "\n";);
SASSERT(q->get_num_patterns() == 2); // first pattern is the function, second is the body.
expr* fn = to_app(q->get_pattern(0))->get_arg(0);
@ -340,7 +340,7 @@ namespace smt {
}
sub(q->get_expr(), num_decls, args.c_ptr(), tmp);
m_curr_model->eval(tmp, result, true);
if (m.is_false(result)) {
if (strict_rec_fun ? !m.is_true(result) : m.is_false(result)) {
add_instance(q, args, 0);
return false;
}
@ -365,10 +365,10 @@ namespace smt {
bool model_checker::check(proto_model * md, obj_map<enode, app *> const & root2value) {
SASSERT(md != 0);
m_root2value = &root2value;
ptr_vector<quantifier>::const_iterator it = m_qm->begin_quantifiers();
ptr_vector<quantifier>::const_iterator end = m_qm->end_quantifiers();
if (it == end)
if (m_qm->num_quantifiers() == 0)
return true;
if (m_iteration_idx >= m_params.m_mbqi_max_iterations) {
@ -393,6 +393,36 @@ namespace smt {
bool found_relevant = false;
unsigned num_failures = 0;
check_quantifiers(false, found_relevant, num_failures);
if (found_relevant)
m_iteration_idx++;
TRACE("model_checker", tout << "model after check:\n"; model_pp(tout, *md););
TRACE("model_checker", tout << "model checker result: " << (num_failures == 0) << "\n";);
m_max_cexs += m_params.m_mbqi_max_cexs;
if (num_failures == 0 && !m_context->validate_model()) {
num_failures = 1;
// this time force expanding recursive function definitions
// that are not forced true in the current model.
check_quantifiers(true, found_relevant, num_failures);
}
if (num_failures == 0)
m_curr_model->cleanup();
if (m_params.m_mbqi_trace) {
if (num_failures == 0)
verbose_stream() << "(smt.mbqi :succeeded true)\n";
else
verbose_stream() << "(smt.mbqi :num-failures " << num_failures << ")\n";
}
return num_failures == 0;
}
void model_checker::check_quantifiers(bool strict_rec_fun, bool& found_relevant, unsigned& num_failures) {
ptr_vector<quantifier>::const_iterator it = m_qm->begin_quantifiers();
ptr_vector<quantifier>::const_iterator end = m_qm->end_quantifiers();
for (; it != end; ++it) {
quantifier * q = *it;
if(!m_qm->mbqi_enabled(q)) continue;
@ -406,7 +436,7 @@ namespace smt {
}
found_relevant = true;
if (m.is_rec_fun_def(q)) {
if (!check_rec_fun(q)) {
if (!check_rec_fun(q, strict_rec_fun)) {
TRACE("model_checker", tout << "checking recursive function failed\n";);
num_failures++;
}
@ -420,26 +450,6 @@ namespace smt {
}
}
}
if (found_relevant)
m_iteration_idx++;
TRACE("model_checker", tout << "model after check:\n"; model_pp(tout, *md););
TRACE("model_checker", tout << "model checker result: " << (num_failures == 0) << "\n";);
m_max_cexs += m_params.m_mbqi_max_cexs;
if (num_failures == 0 && !m_context->validate_model()) {
num_failures = 1;
}
if (num_failures == 0)
m_curr_model->cleanup();
if (m_params.m_mbqi_trace) {
if (num_failures == 0)
verbose_stream() << "(smt.mbqi :succeeded true)\n";
else
verbose_stream() << "(smt.mbqi :num-failures " << num_failures << ")\n";
}
return num_failures == 0;
}
void model_checker::init_search_eh() {

3
src/smt/smt_model_checker.h
View file

@ -59,7 +59,8 @@ namespace smt {
void assert_neg_q_m(quantifier * q, expr_ref_vector & sks);
bool add_blocking_clause(model * cex, expr_ref_vector & sks);
bool check(quantifier * q);
bool check_rec_fun(quantifier* q);
bool check_rec_fun(quantifier* q, bool strict_rec_fun);
void check_quantifiers(bool strict_rec_fun, bool& found_relevant, unsigned& num_failures);
struct instance {
quantifier * m_q;

4
src/smt/smt_quantifier.cpp
View file

@ -397,6 +397,10 @@ namespace smt {
return m_imp->m_quantifiers.end();
}
unsigned quantifier_manager::num_quantifiers() const {
return m_imp->m_quantifiers.size();
}
// The default plugin uses E-matching, MBQI and quick-checker
class default_qm_plugin : public quantifier_manager_plugin {
quantifier_manager * m_qm;

2
src/smt/smt_quantifier.h
View file

@ -91,6 +91,8 @@ namespace smt {
ptr_vector<quantifier>::const_iterator begin_quantifiers() const;
ptr_vector<quantifier>::const_iterator end_quantifiers() const;
unsigned num_quantifiers() const;
};
class quantifier_manager_plugin {

62
src/smt/smt_solver.cpp
View file

@ -38,6 +38,7 @@ namespace smt {
bool m_minimizing_core;
bool m_core_extend_patterns;
unsigned m_core_extend_patterns_max_distance;
bool m_core_extend_nonlocal_patterns;
obj_map<expr, expr*> m_name2assertion;
public:
@ -48,13 +49,15 @@ namespace smt {
m_context(m, m_smt_params),
m_minimizing_core(false),
m_core_extend_patterns(false),
m_core_extend_patterns_max_distance(UINT_MAX) {
m_core_extend_patterns_max_distance(UINT_MAX),
m_core_extend_nonlocal_patterns(false) {
m_logic = l;
if (m_logic != symbol::null)
m_context.set_logic(m_logic);
smt_params_helper smth(p);
m_core_extend_patterns = smth.core_extend_patterns();
m_core_extend_patterns_max_distance = smth.core_extend_patterns_max_distance();
m_core_extend_nonlocal_patterns = smth.core_extend_nonlocal_patterns();
}
virtual solver * translate(ast_manager & m, params_ref const & p) {
@ -81,6 +84,8 @@ namespace smt {
m_context.updt_params(p);
smt_params_helper smth(p);
m_core_extend_patterns = smth.core_extend_patterns();
m_core_extend_patterns_max_distance = smth.core_extend_patterns_max_distance();
m_core_extend_nonlocal_patterns = smth.core_extend_nonlocal_patterns();
}
virtual void collect_param_descrs(param_descrs & r) {
@ -172,6 +177,8 @@ namespace smt {
if (m_core_extend_patterns)
add_pattern_literals_to_core(r);
if (m_core_extend_nonlocal_patterns)
add_nonlocal_pattern_literals_to_core(r);
}
virtual void get_model(model_ref & m) {
@ -250,7 +257,7 @@ namespace smt {
}
};
void collect_pattern_func_decls(expr_ref & e, func_decl_set & fds) {
void collect_pattern_fds(expr_ref & e, func_decl_set & fds) {
collect_pattern_fds_proc p(get_manager(), fds);
expr_mark visited;
for_each_expr(p, visited, e);
@ -295,7 +302,7 @@ namespace smt {
expr_ref name(core[i], m);
SASSERT(m_name2assertion.contains(name));
expr_ref assrtn(m_name2assertion.find(name), m);
collect_pattern_func_decls(assrtn, pattern_fds);
collect_pattern_fds(assrtn, pattern_fds);
}
if (!pattern_fds.empty()) {
@ -317,6 +324,55 @@ namespace smt {
break;
}
}
struct collect_body_fds_proc {
ast_manager & m;
func_decl_set & m_fds;
collect_body_fds_proc(ast_manager & m, func_decl_set & fds) :
m(m), m_fds(fds) {
}
void operator()(var * n) {}
void operator()(app * n) {}
void operator()(quantifier * n) {
collect_fds_proc p(m, m_fds);
expr_fast_mark1 visited;
quick_for_each_expr(p, visited, n->get_expr());
}
};
void collect_body_func_decls(expr_ref & e, func_decl_set & fds) {
ast_manager & m = get_manager();
collect_body_fds_proc p(m, fds);
expr_mark visited;
for_each_expr(p, visited, e);
}
void add_nonlocal_pattern_literals_to_core(ptr_vector<expr> & core) {
ast_manager & m = get_manager();
obj_map<expr, expr*>::iterator it = m_name2assertion.begin();
obj_map<expr, expr*>::iterator end = m_name2assertion.end();
for (unsigned i = 0; it != end; it++, i++) {
expr_ref name(it->m_key, m);
expr_ref assrtn(it->m_value, m);
if (!core.contains(name)) {
func_decl_set pattern_fds, body_fds;
collect_pattern_fds(assrtn, pattern_fds);
collect_body_func_decls(assrtn, body_fds);
func_decl_set::iterator pit = pattern_fds.begin();
func_decl_set::iterator pend= pattern_fds.end();
for (; pit != pend; pit++) {
func_decl * fd = *pit;
if (!body_fds.contains(fd)) {
core.insert(name);
break;
}
}
}
}
}
};
};

16
src/smt/smt_theory.h
View file

@ -177,6 +177,22 @@ namespace smt {
virtual void restart_eh() {
}
/**
\brief This method is called by smt_context before the search starts
to get any extra assumptions the theory wants to use.
(See theory_str for an example)
*/
virtual void add_theory_assumptions(expr_ref_vector & assumptions) {
}
/**
\brief This method is called from smt_context when an unsat core is generated.
The theory may change the answer to UNKNOWN by returning l_undef from this method.
*/
virtual lbool validate_unsat_core(expr_ref_vector & unsat_core) {
return l_false;
}
/**
\brief This method is invoked before the search starts.
*/

5
src/smt/theory_arith_nl.h
View file

@ -339,8 +339,13 @@ namespace smt {
tout << mk_pp(var, get_manager()) << "\n";
tout << "power " << power << ": " << expt(i, power) << "\n";
display_interval(tout << "target before: ", target); tout << "\n";);
i.expt(power);
target *= i;
get_manager().limit().inc((target.is_lower_open() || target.minus_infinity()) ? 1 : target.get_lower_value().bitsize());
get_manager().limit().inc((target.is_upper_open() || target.plus_infinity()) ? 1 : target.get_upper_value().bitsize());
TRACE("non_linear", display_interval(tout << "target after: ", target); tout << "\n";);
}

52
src/smt/theory_seq.cpp
View file

@ -255,6 +255,11 @@ final_check_status theory_seq::final_check_eh() {
TRACE("seq", tout << ">>solve_eqs\n";);
return FC_CONTINUE;
}
if (check_contains()) {
++m_stats.m_propagate_contains;
TRACE("seq", tout << ">>propagate_contains\n";);
return FC_CONTINUE;
}
if (solve_nqs(0)) {
++m_stats.m_solve_nqs;
TRACE("seq", tout << ">>solve_nqs\n";);
@ -290,11 +295,6 @@ final_check_status theory_seq::final_check_eh() {
TRACE("seq", tout << ">>propagate_automata\n";);
return FC_CONTINUE;
}
if (check_contains()) {
++m_stats.m_propagate_contains;
TRACE("seq", tout << ">>propagate_contains\n";);
return FC_CONTINUE;
}
if (is_solved()) {
TRACE("seq", tout << ">>is_solved\n";);
return FC_DONE;
@ -1159,7 +1159,7 @@ bool theory_seq::check_extensionality() {
}
/*
\brief check negated contains constriants.
\brief check negated contains constraints.
*/
bool theory_seq::check_contains() {
context & ctx = get_context();
@ -1199,6 +1199,11 @@ bool theory_seq::is_solved() {
IF_VERBOSE(10, display_disequation(verbose_stream() << "(seq.giveup ", m_nqs[0]); verbose_stream() << " is unsolved)\n";);
return false;
}
if (!m_ncs.empty()) {
TRACE("seq", display_nc(tout << "(seq.giveup ", m_ncs[0]); tout << " is unsolved)\n";);
IF_VERBOSE(10, display_nc(verbose_stream() << "(seq.giveup ", m_ncs[0]); verbose_stream() << " is unsolved)\n";);
return false;
}
return true;
}
@ -1984,6 +1989,22 @@ bool theory_seq::solve_nc(unsigned idx) {
m_new_propagation = true;
return true;
}
expr* e1, *e2;
if (m.is_eq(c, e1, e2)) {
literal eq = mk_eq(e1, e2, false);
propagate_lit(deps, 0, 0, ~eq);
return true;
}
if (m.is_or(c)) {
for (unsigned i = 0; i < to_app(c)->get_num_args(); ++i) {
expr_ref ci(to_app(c)->get_arg(i), m);
m_ncs.push_back(nc(ci, deps));
}
m_new_propagation = true;
return true;
}
return false;
}
@ -2345,6 +2366,17 @@ bool theory_seq::add_itos_axiom(expr* e) {
return false;
}
add_axiom(mk_eq(e2, n, false));
#if 1
expr_ref num_re(m), opt_re(m);
num_re = m_util.re.mk_range(m_util.str.mk_string(symbol("0")), m_util.str.mk_string(symbol("9")));
num_re = m_util.re.mk_plus(num_re);
opt_re = m_util.re.mk_opt(m_util.re.mk_to_re(m_util.str.mk_string(symbol("-"))));
num_re = m_util.re.mk_concat(opt_re, num_re);
app_ref in_re(m_util.re.mk_in_re(e, num_re), m);
internalize_term(in_re);
propagate_in_re(in_re, true);
#endif
m_trail_stack.push(push_replay(alloc(replay_axiom, m, e)));
return true;
}
@ -2407,13 +2439,17 @@ void theory_seq::display(std::ostream & out) const {
if (!m_ncs.empty()) {
out << "Non contains:\n";
for (unsigned i = 0; i < m_ncs.size(); ++i) {
out << "not " << mk_pp(m_ncs[i].contains(), m) << "\n";
display_deps(out << " <- ", m_ncs[i].deps()); out << "\n";
display_nc(out, m_ncs[i]);
}
}
}
void theory_seq::display_nc(std::ostream& out, nc const& nc) const {
out << "not " << mk_pp(nc.contains(), m) << "\n";
display_deps(out << " <- ", nc.deps()); out << "\n";
}
void theory_seq::display_equations(std::ostream& out) const {
for (unsigned i = 0; i < m_eqs.size(); ++i) {
display_equation(out, m_eqs[i]);

1
src/smt/theory_seq.h
View file

@ -570,6 +570,7 @@ namespace smt {
void display_disequation(std::ostream& out, ne const& e) const;
void display_deps(std::ostream& out, dependency* deps) const;
void display_deps(std::ostream& out, literal_vector const& lits, enode_pair_vector const& eqs) const;
void display_nc(std::ostream& out, nc const& nc) const;
public:
theory_seq(ast_manager& m);
virtual ~theory_seq();

9
src/tactic/bv/elim_small_bv_tactic.cpp
View file

@ -34,6 +34,7 @@ class elim_small_bv_tactic : public tactic {
struct rw_cfg : public default_rewriter_cfg {
ast_manager & m;
params_ref m_params;
bv_util m_util;
simplifier m_simp;
ref<filter_model_converter> m_mc;
@ -47,6 +48,7 @@ class elim_small_bv_tactic : public tactic {
rw_cfg(ast_manager & _m, params_ref const & p) :
m(_m),
m_params(p),
m_util(_m),
m_simp(_m),
m_bindings(_m),
@ -119,7 +121,7 @@ class elim_small_bv_tactic : public tactic {
return res;
}
br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) {
br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) {
TRACE("elim_small_bv_app", expr_ref tmp(m.mk_app(f, num, args), m); tout << "reduce " << tmp << std::endl; );
return BR_FAILED;
}
@ -178,7 +180,7 @@ class elim_small_bv_tactic : public tactic {
quantifier_ref new_q(m);
new_q = m.update_quantifier(q, body);
unused_vars_eliminator el(m);
unused_vars_eliminator el(m, m_params);
el(new_q, result);
TRACE("elim_small_bv", tout << "elimination result: " << mk_ismt2_pp(result, m) << std::endl; );
@ -203,6 +205,7 @@ class elim_small_bv_tactic : public tactic {
}
void updt_params(params_ref const & p) {
m_params = p;
m_max_memory = megabytes_to_bytes(p.get_uint("max_memory", UINT_MAX));
m_max_steps = p.get_uint("max_steps", UINT_MAX);
m_max_bits = p.get_uint("max_bits", 4);
@ -305,7 +308,7 @@ public:
virtual void cleanup() {
ast_manager & m = m_imp->m;
imp * d = alloc(imp, m, m_params);
std::swap(d, m_imp);
std::swap(d, m_imp);
dealloc(d);
}

32
src/tactic/core/distribute_forall_tactic.cpp
View file

@ -24,9 +24,9 @@ class distribute_forall_tactic : public tactic {
ast_manager & m;
rw_cfg(ast_manager & _m):m(_m) {}
bool reduce_quantifier(quantifier * old_q,
expr * new_body,
expr * const * new_patterns,
bool reduce_quantifier(quantifier * old_q,
expr * new_body,
expr * const * new_patterns,
expr * const * new_no_patterns,
expr_ref & result,
proof_ref & result_pr) {
@ -34,7 +34,7 @@ class distribute_forall_tactic : public tactic {
if (!old_q->is_forall()) {
return false;
}
if (m.is_not(new_body) && m.is_or(to_app(new_body)->get_arg(0))) {
// (forall X (not (or F1 ... Fn)))
// -->
@ -50,13 +50,13 @@ class distribute_forall_tactic : public tactic {
quantifier_ref tmp_q(m);
tmp_q = m.update_quantifier(old_q, not_arg);
expr_ref new_q(m);
elim_unused_vars(m, tmp_q, new_q);
elim_unused_vars(m, tmp_q, params_ref(), new_q);
new_args.push_back(new_q);
}
result = m.mk_and(new_args.size(), new_args.c_ptr());
return true;
}
if (m.is_and(new_body)) {
// (forall X (and F1 ... Fn))
// -->
@ -70,20 +70,20 @@ class distribute_forall_tactic : public tactic {
quantifier_ref tmp_q(m);
tmp_q = m.update_quantifier(old_q, arg);
expr_ref new_q(m);
elim_unused_vars(m, tmp_q, new_q);
elim_unused_vars(m, tmp_q, params_ref(), new_q);
new_args.push_back(new_q);
}
result = m.mk_and(new_args.size(), new_args.c_ptr());
return true;
}
return false;
}
};
struct rw : public rewriter_tpl<rw_cfg> {
rw_cfg m_cfg;
rw(ast_manager & m, bool proofs_enabled):
rewriter_tpl<rw_cfg>(m, proofs_enabled, m_cfg),
m_cfg(m) {
@ -99,19 +99,19 @@ public:
return alloc(distribute_forall_tactic);
}
virtual void operator()(goal_ref const & g,
goal_ref_buffer & result,
model_converter_ref & mc,
virtual void operator()(goal_ref const & g,
goal_ref_buffer & result,
model_converter_ref & mc,
proof_converter_ref & pc,
expr_dependency_ref & core) {
SASSERT(g->is_well_sorted());
ast_manager & m = g->m();
bool produce_proofs = g->proofs_enabled();
rw r(m, produce_proofs);
m_rw = &r;
m_rw = &r;
mc = 0; pc = 0; core = 0; result.reset();
tactic_report report("distribute-forall", *g);
expr_ref new_curr(m);
proof_ref new_pr(m);
unsigned size = g->size();
@ -126,12 +126,12 @@ public:
}
g->update(idx, new_curr, new_pr, g->dep(idx));
}
g->inc_depth();
result.push_back(g.get());
TRACE("distribute-forall", g->display(tout););
SASSERT(g->is_well_sorted());
m_rw = 0;
m_rw = 0;
}
virtual void cleanup() {}

74
src/tactic/portfolio/bounded_int2bv_solver.cpp
View file

@ -34,19 +34,19 @@ Notes:
class bounded_int2bv_solver : public solver_na2as {
ast_manager& m;
params_ref m_params;
bv_util m_bv;
arith_util m_arith;
expr_ref_vector m_assertions;
mutable bv_util m_bv;
mutable arith_util m_arith;
mutable expr_ref_vector m_assertions;
ref<solver> m_solver;
ptr_vector<bound_manager> m_bounds;
func_decl_ref_vector m_bv_fns;
func_decl_ref_vector m_int_fns;
mutable ptr_vector<bound_manager> m_bounds;
mutable func_decl_ref_vector m_bv_fns;
mutable func_decl_ref_vector m_int_fns;
unsigned_vector m_bv_fns_lim;
obj_map<func_decl, func_decl*> m_int2bv;
obj_map<func_decl, func_decl*> m_bv2int;
obj_map<func_decl, rational> m_bv2offset;
bv2int_rewriter_ctx m_rewriter_ctx;
bv2int_rewriter_star m_rewriter;
mutable obj_map<func_decl, func_decl*> m_int2bv;
mutable obj_map<func_decl, func_decl*> m_bv2int;
mutable obj_map<func_decl, rational> m_bv2offset;
mutable bv2int_rewriter_ctx m_rewriter_ctx;
mutable bv2int_rewriter_star m_rewriter;
public:
@ -78,7 +78,19 @@ public:
}
virtual void assert_expr(expr * t) {
unsigned i = m_assertions.size();
m_assertions.push_back(t);
while (i < m_assertions.size()) {
t = m_assertions[i].get();
if (m.is_and(t)) {
m_assertions.append(to_app(t)->get_num_args(), to_app(t)->get_args());
m_assertions[i] = m_assertions.back();
m_assertions.pop_back();
}
else {
++i;
}
}
}
virtual void push_core() {
@ -184,7 +196,7 @@ private:
}
filter_model_converter filter(m);
for (unsigned i = 0; i < m_bv_fns.size(); ++i) {
filter.insert(m_bv_fns[i]);
filter.insert(m_bv_fns[i].get());
}
filter(mdl, 0);
}
@ -205,13 +217,13 @@ private:
ext(mdl, 0);
}
void accumulate_sub(expr_safe_replace& sub) {
void accumulate_sub(expr_safe_replace& sub) const {
for (unsigned i = 0; i < m_bounds.size(); ++i) {
accumulate_sub(sub, *m_bounds[i]);
}
}
void accumulate_sub(expr_safe_replace& sub, bound_manager& bm) {
void accumulate_sub(expr_safe_replace& sub, bound_manager& bm) const {
bound_manager::iterator it = bm.begin(), end = bm.end();
for (; it != end; ++it) {
expr* e = *it;
@ -252,19 +264,20 @@ private:
sub.insert(e, t);
}
else {
IF_VERBOSE(1,
verbose_stream() << "unprocessed entry: " << mk_pp(e, m) << "\n";
if (bm.has_lower(e, lo, s1)) {
verbose_stream() << "lower: " << lo << " " << s1 << "\n";
}
if (bm.has_upper(e, hi, s2)) {
verbose_stream() << "upper: " << hi << " " << s2 << "\n";
});
TRACE("pb",
tout << "unprocessed entry: " << mk_pp(e, m) << "\n";
if (bm.has_lower(e, lo, s1)) {
tout << "lower: " << lo << " " << s1 << "\n";
}
if (bm.has_upper(e, hi, s2)) {
tout << "upper: " << hi << " " << s2 << "\n";
});
}
}
}
unsigned get_num_bits(rational const& k) {
unsigned get_num_bits(rational const& k) const {
SASSERT(!k.is_neg());
SASSERT(k.is_int());
rational two(2);
@ -277,11 +290,13 @@ private:
return num_bits;
}
void flush_assertions() {
void flush_assertions() const {
if (m_assertions.empty()) return;
bound_manager& bm = *m_bounds.back();
for (unsigned i = 0; i < m_assertions.size(); ++i) {
bm(m_assertions[i].get());
}
TRACE("int2bv", bm.display(tout););
expr_safe_replace sub(m);
accumulate_sub(sub);
proof_ref proof(m);
@ -304,6 +319,17 @@ private:
m_assertions.reset();
m_rewriter.reset();
}
virtual unsigned get_num_assertions() const {
flush_assertions();
return m_solver->get_num_assertions();
}
virtual expr * get_assertion(unsigned idx) const {
flush_assertions();
return m_solver->get_assertion(idx);
}
};
solver * mk_bounded_int2bv_solver(ast_manager & m, params_ref const & p, solver* s) {

8
src/tactic/portfolio/enum2bv_solver.cpp
View file

@ -163,6 +163,14 @@ public:
ext(mdl, 0);
}
virtual unsigned get_num_assertions() const {
return m_solver->get_num_assertions();
}
virtual expr * get_assertion(unsigned idx) const {
return m_solver->get_assertion(idx);
}
};
solver * mk_enum2bv_solver(ast_manager & m, params_ref const & p, solver* s) {

19
src/tactic/portfolio/pb2bv_solver.cpp
View file

@ -27,9 +27,9 @@ Notes:
class pb2bv_solver : public solver_na2as {
ast_manager& m;
params_ref m_params;
expr_ref_vector m_assertions;
ref<solver> m_solver;
pb2bv_rewriter m_rewriter;
mutable expr_ref_vector m_assertions;
mutable ref<solver> m_solver;
mutable pb2bv_rewriter m_rewriter;
public:
@ -107,8 +107,19 @@ public:
filter(mdl, 0);
}
virtual unsigned get_num_assertions() const {
flush_assertions();
return m_solver->get_num_assertions();
}
virtual expr * get_assertion(unsigned idx) const {
flush_assertions();
return m_solver->get_assertion(idx);
}
private:
void flush_assertions() {
void flush_assertions() const {
proof_ref proof(m);
expr_ref fml(m);
expr_ref_vector fmls(m);

190
src/tactic/ufbv/ufbv_rewriter.cpp
View file

@ -49,7 +49,7 @@ ufbv_rewriter::~ufbv_rewriter() {
bool ufbv_rewriter::is_demodulator(expr * e, expr_ref & large, expr_ref & small) const {
if (e->get_kind() == AST_QUANTIFIER) {
quantifier * q = to_quantifier(e);
if (q->is_forall()) {
if (q->is_forall()) {
expr * qe = q->get_expr();
if ((m_manager.is_eq(qe) || m_manager.is_iff(qe))) {
app * eq = to_app(q->get_expr());
@ -61,7 +61,7 @@ bool ufbv_rewriter::is_demodulator(expr * e, expr_ref & large, expr_ref & small)
<< mk_pp(lhs, m_manager) << "\n"
<< mk_pp(rhs, m_manager) << "\n"
<< "subset: " << subset << ", smaller: " << smaller << "\n";);
// We only track uninterpreted functions, everything else is likely too expensive.
// We only track uninterpreted functions, everything else is likely too expensive.
if ((subset == +1 || subset == +2) && smaller == +1) {
if (is_uninterp(rhs)) {
large = rhs;
@ -78,7 +78,7 @@ bool ufbv_rewriter::is_demodulator(expr * e, expr_ref & large, expr_ref & small)
}
#endif
}
if ((subset == -1 || subset == +2) && smaller == -1) {
if (is_uninterp(lhs)) {
large = lhs;
@ -113,13 +113,13 @@ bool ufbv_rewriter::is_demodulator(expr * e, expr_ref & large, expr_ref & small)
return false;
}
class var_set_proc {
class var_set_proc {
uint_set & m_set;
public:
var_set_proc(uint_set &s):m_set(s) {}
void operator()(var * n) { m_set.insert(n->get_idx()); }
void operator()(quantifier * n) {}
void operator()(app * n) {}
void operator()(app * n) {}
};
int ufbv_rewriter::is_subset(expr * e1, expr * e2) const {
@ -132,10 +132,10 @@ int ufbv_rewriter::is_subset(expr * e1, expr * e2) const {
for_each_expr(proc1, e1);
var_set_proc proc2(ev2);
for_each_expr(proc2, e2);
return (ev1==ev2 ) ? +2 : // We return +2 if the sets are equal.
(ev1.subset_of(ev2)) ? +1 :
(ev2.subset_of(ev1)) ? -1 :
return (ev1==ev2 ) ? +2 : // We return +2 if the sets are equal.
(ev1.subset_of(ev2)) ? +1 :
(ev2.subset_of(ev1)) ? -1 :
0 ;
}
@ -154,8 +154,8 @@ int ufbv_rewriter::is_smaller(expr * e1, expr * e2) const {
else if (is_uninterp(e1) && !is_uninterp(e2))
return -1;
// two uninterpreted functions are ordered first by the number of
// arguments, then by their id.
// two uninterpreted functions are ordered first by the number of
// arguments, then by their id.
if (is_uninterp(e1) && is_uninterp(e2)) {
if (to_app(e1)->get_num_args() < to_app(e2)->get_num_args())
return +1;
@ -163,10 +163,10 @@ int ufbv_rewriter::is_smaller(expr * e1, expr * e2) const {
return -1;
else {
unsigned a = to_app(e1)->get_decl()->get_id();
unsigned b = to_app(e2)->get_decl()->get_id();
if (a < b)
unsigned b = to_app(e2)->get_decl()->get_id();
if (a < b)
return +1;
else if (a > b)
else if (a > b)
return -1;
}
}
@ -185,8 +185,8 @@ int ufbv_rewriter::is_smaller(expr * e1, expr * e2) const {
default: UNREACHABLE();
}
return (sz1 == sz2) ? 0 :
(sz1 < sz2) ? +1 :
return (sz1 == sz2) ? 0 :
(sz1 < sz2) ? +1 :
-1 ;
}
@ -194,9 +194,9 @@ class max_var_id_proc {
unsigned m_max_var_id;
public:
max_var_id_proc(void):m_max_var_id(0) {}
void operator()(var * n) {
if(n->get_idx() > m_max_var_id)
m_max_var_id = n->get_idx();
void operator()(var * n) {
if(n->get_idx() > m_max_var_id)
m_max_var_id = n->get_idx();
}
void operator()(quantifier * n) {}
void operator()(app * n) {}
@ -206,7 +206,7 @@ public:
unsigned ufbv_rewriter::max_var_id(expr * e)
{
max_var_id_proc proc;
for_each_expr(proc, e);
for_each_expr(proc, e);
return proc.get_max();
}
@ -219,14 +219,14 @@ void ufbv_rewriter::insert_fwd_idx(expr * large, expr * small, quantifier * demo
func_decl * fd = to_app(large)->get_decl();
fwd_idx_map::iterator it = m_fwd_idx.find_iterator(fd);
if (it == m_fwd_idx.end()) {
quantifier_set * qs = alloc(quantifier_set, 1);
if (it == m_fwd_idx.end()) {
quantifier_set * qs = alloc(quantifier_set, 1);
m_fwd_idx.insert(fd, qs);
it = m_fwd_idx.find_iterator(fd);
}
SASSERT(it->m_value);
it->m_value->insert(demodulator);
it->m_value->insert(demodulator);
m_manager.inc_ref(demodulator);
m_manager.inc_ref(large);
@ -238,13 +238,13 @@ void ufbv_rewriter::remove_fwd_idx(func_decl * f, quantifier * demodulator) {
TRACE("demodulator_fwd", tout << "REMOVE: " << std::hex << (size_t)demodulator << std::endl; );
fwd_idx_map::iterator it = m_fwd_idx.find_iterator(f);
if (it != m_fwd_idx.end()) {
if (it != m_fwd_idx.end()) {
demodulator2lhs_rhs::iterator fit = m_demodulator2lhs_rhs.find_iterator(demodulator);
m_manager.dec_ref(fit->m_value.first);
m_manager.dec_ref(fit->m_value.second);
m_manager.dec_ref(demodulator);
m_demodulator2lhs_rhs.erase(demodulator);
it->m_value->erase(demodulator);
it->m_value->erase(demodulator);
} else {
SASSERT(m_demodulator2lhs_rhs.contains(demodulator));
}
@ -281,13 +281,13 @@ void ufbv_rewriter::show_fwd_idx(std::ostream & out) {
}
}
bool ufbv_rewriter::rewrite1(func_decl * f, ptr_vector<expr> & m_new_args, expr_ref & np) {
bool ufbv_rewriter::rewrite1(func_decl * f, ptr_vector<expr> & m_new_args, expr_ref & np) {
fwd_idx_map::iterator it = m_fwd_idx.find_iterator(f);
if (it != m_fwd_idx.end()) {
TRACE("demodulator_bug", tout << "trying to rewrite: " << f->get_name() << " args:\n";
for (unsigned i = 0; i < m_new_args.size(); i++) { tout << mk_pp(m_new_args[i], m_manager) << "\n"; });
quantifier_set::iterator dit = it->m_value->begin();
quantifier_set::iterator dend = it->m_value->end();
quantifier_set::iterator dend = it->m_value->end();
for ( ; dit != dend ; dit++ ) {
quantifier * d = *dit;
@ -302,7 +302,7 @@ bool ufbv_rewriter::rewrite1(func_decl * f, ptr_vector<expr> & m_new_args, expr_
TRACE("demodulator_bug", tout << "Matching with demodulator: " << mk_pp(d, m_manager) << std::endl; );
SASSERT(large->get_decl() == f);
if (m_match_subst(large, l_s.second, m_new_args.c_ptr(), np)) {
TRACE("demodulator_bug", tout << "succeeded...\n" << mk_pp(l_s.second, m_manager) << "\n===>\n" << mk_pp(np, m_manager) << "\n";);
return true;
@ -331,22 +331,22 @@ void ufbv_rewriter::rewrite_cache(expr * e, expr * new_e, bool done) {
}
expr * ufbv_rewriter::rewrite(expr * n) {
if (m_fwd_idx.empty())
if (m_fwd_idx.empty())
return n;
TRACE("demodulator", tout << "rewrite: " << mk_pp(n, m_manager) << std::endl; );
app * a;
SASSERT(m_rewrite_todo.empty());
m_rewrite_cache.reset();
m_rewrite_todo.push_back(n);
while (!m_rewrite_todo.empty()) {
TRACE("demodulator_stack", tout << "STACK: " << std::endl;
for ( unsigned i = 0; i<m_rewrite_todo.size(); i++)
for ( unsigned i = 0; i<m_rewrite_todo.size(); i++)
tout << std::dec << i << ": " << std::hex << (size_t)m_rewrite_todo[i] << std::endl;
);
);
expr * e = m_rewrite_todo.back();
expr * actual = e;
@ -355,7 +355,7 @@ expr * ufbv_rewriter::rewrite(expr * n) {
if (ebp.second) {
m_rewrite_todo.pop_back();
continue;
}
}
else {
actual = ebp.first;
}
@ -366,8 +366,8 @@ expr * ufbv_rewriter::rewrite(expr * n) {
rewrite_cache(e, actual, true);
m_rewrite_todo.pop_back();
break;
case AST_APP:
a = to_app(actual);
case AST_APP:
a = to_app(actual);
if (rewrite_visit_children(a)) {
func_decl * f = a->get_decl();
m_new_args.reset();
@ -389,12 +389,12 @@ expr * ufbv_rewriter::rewrite(expr * n) {
// No pop.
} else {
if(all_untouched) {
rewrite_cache(e, actual, true);
}
rewrite_cache(e, actual, true);
}
else {
expr_ref na(m_manager);
if (f->get_family_id() != m_manager.get_basic_family_id())
na = m_manager.mk_app(f, m_new_args.size(), m_new_args.c_ptr());
na = m_manager.mk_app(f, m_new_args.size(), m_new_args.c_ptr());
else
m_bsimp.reduce(f, m_new_args.size(), m_new_args.c_ptr(), na);
TRACE("demodulator_bug", tout << "e:\n" << mk_pp(e, m_manager) << "\nnew_args: \n";
@ -405,9 +405,9 @@ expr * ufbv_rewriter::rewrite(expr * n) {
}
m_rewrite_todo.pop_back();
}
}
}
break;
case AST_QUANTIFIER: {
case AST_QUANTIFIER: {
expr * body = to_quantifier(actual)->get_expr();
if (m_rewrite_cache.contains(body)) {
const expr_bool_pair ebp = m_rewrite_cache.get(body);
@ -417,13 +417,13 @@ expr * ufbv_rewriter::rewrite(expr * n) {
q = m_manager.update_quantifier(to_quantifier(actual), new_body);
m_new_exprs.push_back(q);
expr_ref new_q(m_manager);
elim_unused_vars(m_manager, q, new_q);
elim_unused_vars(m_manager, q, params_ref(), new_q);
m_new_exprs.push_back(new_q);
rewrite_cache(e, new_q, true);
rewrite_cache(e, new_q, true);
m_rewrite_todo.pop_back();
} else {
m_rewrite_todo.push_back(body);
}
}
break;
}
default:
@ -437,7 +437,7 @@ expr * ufbv_rewriter::rewrite(expr * n) {
expr * r = ebp.first;
TRACE("demodulator", tout << "rewrite result: " << mk_pp(r, m_manager) << std::endl; );
return r;
}
@ -448,7 +448,7 @@ public:
add_back_idx_proc(back_idx_map & bi, expr * e):m_back_idx(bi),m_expr(e) {}
void operator()(var * n) {}
void operator()(quantifier * n) {}
void operator()(app * n) {
void operator()(app * n) {
// We track only uninterpreted and constant functions.
if (n->get_num_args()==0) return;
SASSERT(m_expr && m_expr != (expr*) 0x00000003);
@ -464,7 +464,7 @@ public:
m_back_idx.insert(d, e);
}
}
}
}
};
class ufbv_rewriter::remove_back_idx_proc {
@ -473,15 +473,15 @@ class ufbv_rewriter::remove_back_idx_proc {
public:
remove_back_idx_proc(back_idx_map & bi, expr * e):m_back_idx(bi),m_expr(e) {}
void operator()(var * n) {}
void operator()(quantifier * n) {}
void operator()(app * n) {
void operator()(quantifier * n) {}
void operator()(app * n) {
// We track only uninterpreted and constant functions.
if (n->get_num_args()==0) return;
func_decl * d=n->get_decl();
if (d->get_family_id() == null_family_id) {
if (d->get_family_id() == null_family_id) {
back_idx_map::iterator it = m_back_idx.find_iterator(d);
if (it != m_back_idx.end()) {
SASSERT(it->m_value);
SASSERT(it->m_value);
it->m_value->remove(m_expr);
}
}
@ -489,12 +489,12 @@ public:
};
void ufbv_rewriter::reschedule_processed(func_decl * f) {
//use m_back_idx to find all formulas p in m_processed that contains f {
//use m_back_idx to find all formulas p in m_processed that contains f {
back_idx_map::iterator it = m_back_idx.find_iterator(f);
if (it != m_back_idx.end()) {
SASSERT(it->m_value);
expr_set temp;
expr_set::iterator sit = it->m_value->begin();
expr_set::iterator send = it->m_value->end();
for ( ; sit != send ; sit++ ) {
@ -502,7 +502,7 @@ void ufbv_rewriter::reschedule_processed(func_decl * f) {
if (m_processed.contains(p))
temp.insert(p);
}
sit = temp.begin();
send = temp.end();
for ( ; sit != send; sit++) {
@ -511,7 +511,7 @@ void ufbv_rewriter::reschedule_processed(func_decl * f) {
m_processed.remove(p);
remove_back_idx_proc proc(m_back_idx, p); // this could change it->m_value, thus we need the `temp' set.
for_each_expr(proc, p);
// insert p into m_todo
// insert p into m_todo
m_todo.push_back(p);
}
}
@ -529,40 +529,40 @@ bool ufbv_rewriter::can_rewrite(expr * n, expr * lhs) {
while (!stack.empty()) {
curr = stack.back();
if (visited.is_marked(curr)) {
stack.pop_back();
continue;
}
switch(curr->get_kind()) {
case AST_VAR:
case AST_VAR:
visited.mark(curr, true);
stack.pop_back();
break;
case AST_APP:
if (for_each_expr_args(stack, visited, to_app(curr)->get_num_args(), to_app(curr)->get_args())) {
if (for_each_expr_args(stack, visited, to_app(curr)->get_num_args(), to_app(curr)->get_args())) {
if (m_match_subst(lhs, curr))
return true;
visited.mark(curr, true);
stack.pop_back();
}
break;
case AST_QUANTIFIER:
if (!for_each_expr_args(stack, visited, to_quantifier(curr)->get_num_patterns(),
if (!for_each_expr_args(stack, visited, to_quantifier(curr)->get_num_patterns(),
to_quantifier(curr)->get_patterns())) {
break;
}
if (!for_each_expr_args(stack, visited, to_quantifier(curr)->get_num_no_patterns(),
if (!for_each_expr_args(stack, visited, to_quantifier(curr)->get_num_no_patterns(),
to_quantifier(curr)->get_no_patterns())) {
break;
}
if (!visited.is_marked(to_quantifier(curr)->get_expr())) {
stack.push_back(to_quantifier(curr)->get_expr());
break;
}
}
stack.pop_back();
break;
@ -597,7 +597,7 @@ void ufbv_rewriter::reschedule_demodulators(func_decl * f, expr * lhs) {
expr * occ = *esit;
if (!is_quantifier(occ))
continue;
continue;
// Use the fwd idx to find out whether this is a demodulator.
demodulator2lhs_rhs::iterator d2lr_it = m_demodulator2lhs_rhs.find_iterator(to_quantifier(occ));
@ -605,22 +605,22 @@ void ufbv_rewriter::reschedule_demodulators(func_decl * f, expr * lhs) {
l = d2lr_it->m_value.first;
quantifier_ref d(m_manager);
func_decl_ref df(m_manager);
d = to_quantifier(occ);
d = to_quantifier(occ);
df = to_app(l)->get_decl();
// Now we know there is an occurrence of f in d
// if n' can rewrite d {
// if n' can rewrite d {
if (can_rewrite(d, lhs)) {
TRACE("demodulator", tout << "Rescheduling: " << std::endl << mk_pp(d, m_manager) << std::endl; );
// remove d from m_fwd_idx
remove_fwd_idx(df, d);
// remove d from m_back_idx
// remove d from m_back_idx
// just remember it here, because otherwise it and/or esit might become invalid?
// to_remove.insert(d);
// to_remove.insert(d);
remove_back_idx_proc proc(m_back_idx, d);
for_each_expr(proc, d);
// insert d into m_todo
m_todo.push_back(d);
m_todo.push_back(d);
}
}
}
@ -629,10 +629,10 @@ void ufbv_rewriter::reschedule_demodulators(func_decl * f, expr * lhs) {
//for (ptr_vector<expr>::iterator it = to_remove.begin(); it != to_remove.end(); it++) {
// expr * d = *it;
// remove_back_idx_proc proc(m_manager, m_back_idx, d);
// for_each_expr(proc, d);
// for_each_expr(proc, d);
//}
}
void ufbv_rewriter::operator()(unsigned n, expr * const * exprs, proof * const * prs, expr_ref_vector & new_exprs, proof_ref_vector & new_prs) {
if (m_manager.proofs_enabled()) {
// Let us not waste time with proof production
@ -655,7 +655,7 @@ void ufbv_rewriter::operator()(unsigned n, expr * const * exprs, proof * const *
m_match_subst.reserve(max_vid);
while (!m_todo.empty()) {
while (!m_todo.empty()) {
// let n be the next formula in m_todo.
expr_ref cur(m_manager);
cur = m_todo.back();
@ -670,21 +670,21 @@ void ufbv_rewriter::operator()(unsigned n, expr * const * exprs, proof * const *
expr_ref large(m_manager), small(m_manager);
if (!is_demodulator(np, large, small)) {
// insert n' into m_processed
m_processed.insert(np);
// update m_back_idx (traverse n' and for each uninterpreted function declaration f in n' add the entry f->n' to m_back_idx)
m_processed.insert(np);
// update m_back_idx (traverse n' and for each uninterpreted function declaration f in n' add the entry f->n' to m_back_idx)
add_back_idx_proc proc(m_back_idx, np);
for_each_expr(proc, np);
} else {
} else {
// np is a demodulator that allows us to replace 'large' with 'small'.
TRACE("demodulator", tout << "Found demodulator: " << std::endl;
tout << mk_pp(large.get(), m_manager) << std::endl << " ---> " <<
tout << mk_pp(large.get(), m_manager) << std::endl << " ---> " <<
std::endl << mk_pp(small.get(), m_manager) << std::endl; );
TRACE("demodulator_s", tout << "Found demodulator: " << std::endl;
tout << to_app(large)->get_decl()->get_name() <<
tout << to_app(large)->get_decl()->get_name() <<
"[" << to_app(large)->get_depth() << "]" << " ---> ";
if (is_app(small))
tout << to_app(small)->get_decl()->get_name() <<
tout << to_app(small)->get_decl()->get_name() <<
"[" << to_app(small)->get_depth() << "]" << std::endl;
else
tout << mk_pp(small.get(), m_manager) << std::endl; );
@ -695,14 +695,14 @@ void ufbv_rewriter::operator()(unsigned n, expr * const * exprs, proof * const *
reschedule_processed(f);
reschedule_demodulators(f, large);
// insert n' into m_fwd_idx
insert_fwd_idx(large, small, to_quantifier(np));
// update m_back_idx
add_back_idx_proc proc(m_back_idx, np);
for_each_expr(proc, np);
}
}
}
// the result is the contents of m_processed + all demodulators in m_fwd_idx.
@ -743,10 +743,10 @@ ufbv_rewriter::match_subst::match_subst(ast_manager & m):
*/
struct match_args_aux_proc {
substitution & m_subst;
struct no_match {};
struct no_match {};
match_args_aux_proc(substitution & s):m_subst(s) {}
void operator()(var * n) {
expr_offset r;
if (m_subst.find(n, 0, r)) {
@ -766,7 +766,7 @@ struct match_args_aux_proc {
bool ufbv_rewriter::match_subst::match_args(app * lhs, expr * const * args) {
m_cache.reset();
m_todo.reset();
// fill todo-list, and perform quick success/failure tests
m_all_args_eq = true;
unsigned num_args = lhs->get_num_args();
@ -777,21 +777,21 @@ bool ufbv_rewriter::match_subst::match_args(app * lhs, expr * const * args) {
m_all_args_eq = false;
if (is_app(t_arg) && is_app(i_arg) && to_app(t_arg)->get_decl() != to_app(i_arg)->get_decl()) {
// quick failure...
return false;
return false;
}
m_todo.push_back(expr_pair(t_arg, i_arg));
}
if (m_all_args_eq) {
if (m_all_args_eq) {
// quick success worked...
return true;
}
m_subst.reset();
while (!m_todo.empty()) {
expr_pair const & p = m_todo.back();
if (is_var(p.first)) {
expr_offset r;
if (m_subst.find(to_var(p.first), 0, r)) {
@ -814,7 +814,7 @@ bool ufbv_rewriter::match_subst::match_args(app * lhs, expr * const * args) {
SASSERT(is_app(p.first) && is_app(p.second));
if (to_app(p.first)->is_ground() && !to_app(p.second)->is_ground())
if (to_app(p.first)->is_ground() && !to_app(p.second)->is_ground())
return false;
if (p.first == p.second && to_app(p.first)->is_ground()) {
@ -827,7 +827,7 @@ bool ufbv_rewriter::match_subst::match_args(app * lhs, expr * const * args) {
m_todo.pop_back();
continue;
}
if (p.first == p.second) {
// p.first and p.second is not ground...
@ -855,10 +855,10 @@ bool ufbv_rewriter::match_subst::match_args(app * lhs, expr * const * args) {
app * n1 = to_app(p.first);
app * n2 = to_app(p.second);
if (n1->get_decl() != n2->get_decl())
return false;
unsigned num_args1 = n1->get_num_args();
if (num_args1 != n2->get_num_args())
return false;
@ -867,7 +867,7 @@ bool ufbv_rewriter::match_subst::match_args(app * lhs, expr * const * args) {
if (num_args1 == 0)
continue;
m_cache.insert(p);
unsigned j = num_args1;
while (j > 0) {
@ -886,7 +886,7 @@ bool ufbv_rewriter::match_subst::operator()(app * lhs, expr * rhs, expr * const
new_rhs = rhs;
return true;
}
unsigned deltas[2] = { 0, 0 };
unsigned deltas[2] = { 0, 0 };
m_subst.apply(2, deltas, expr_offset(rhs, 0), new_rhs);
return true;
}