mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-28 19:35:50 +00:00
Code Activity

merging duality/interp changes

Browse source
This commit is contained in:
Ken McMillan 2014-05-22 11:52:16 -07:00
commit aa35149700
30 changed files with 604 additions and 369 deletions
Download patch file Download diff file Expand all files Collapse all files

2
.gitignore vendored
View file

@ -55,6 +55,8 @@ src/api/api_log_macros.cpp
src/api/dll/api_dll.def
src/api/dotnet/Enumerations.cs
src/api/dotnet/Native.cs
src/api/dotnet/Properties/AssemblyInfo.cs
src/api/dotnet/Microsoft.Z3.xml
src/api/python/z3consts.py
src/api/python/z3core.py
src/ast/pattern/database.h

7
scripts/mk_project.py
View file

@ -42,17 +42,18 @@ def init_project_def():
# Simplifier module will be deleted in the future.
# It has been replaced with rewriter module.
add_lib('simplifier', ['rewriter'], 'ast/simplifier')
add_lib('fpa', ['ast', 'util', 'simplifier'], 'ast/fpa')
add_lib('macros', ['simplifier'], 'ast/macros')
add_lib('pattern', ['normal_forms', 'smt2parser', 'simplifier'], 'ast/pattern')
add_lib('bit_blaster', ['rewriter', 'simplifier'], 'ast/rewriter/bit_blaster')
add_lib('smt_params', ['ast', 'simplifier', 'pattern', 'bit_blaster'], 'smt/params')
add_lib('proto_model', ['model', 'simplifier', 'smt_params'], 'smt/proto_model')
add_lib('smt', ['bit_blaster', 'macros', 'normal_forms', 'cmd_context', 'proto_model',
'substitution', 'grobner', 'euclid', 'proof_checker', 'pattern', 'parser_util'])
'substitution', 'grobner', 'euclid', 'proof_checker', 'pattern', 'parser_util', 'fpa'])
add_lib('user_plugin', ['smt'], 'smt/user_plugin')
add_lib('bv_tactics', ['tactic', 'bit_blaster'], 'tactic/bv')
add_lib('fuzzing', ['ast'], 'test/fuzzing')
add_lib('fpa', ['core_tactics', 'bv_tactics', 'sat_tactic'], 'tactic/fpa')
add_lib('fpa_tactics', ['fpa', 'core_tactics', 'bv_tactics', 'sat_tactic'], 'tactic/fpa')
add_lib('smt_tactic', ['smt'], 'smt/tactic')
add_lib('sls_tactic', ['tactic', 'normal_forms', 'core_tactics', 'bv_tactics'], 'tactic/sls')
add_lib('qe', ['smt','sat'], 'qe')
@ -68,7 +69,7 @@ def init_project_def():
add_lib('fp', ['muz', 'pdr', 'clp', 'tab', 'rel', 'bmc', 'duality_intf'], 'muz/fp')
add_lib('smtlogic_tactics', ['arith_tactics', 'bv_tactics', 'nlsat_tactic', 'smt_tactic', 'aig_tactic', 'fp', 'muz','qe'], 'tactic/smtlogics')
add_lib('ufbv_tactic', ['normal_forms', 'core_tactics', 'macros', 'smt_tactic', 'rewriter'], 'tactic/ufbv')
add_lib('portfolio', ['smtlogic_tactics', 'ufbv_tactic', 'fpa', 'aig_tactic', 'fp', 'qe','sls_tactic', 'subpaving_tactic'], 'tactic/portfolio')
add_lib('portfolio', ['smtlogic_tactics', 'ufbv_tactic', 'fpa_tactics', 'aig_tactic', 'fp', 'qe','sls_tactic', 'subpaving_tactic'], 'tactic/portfolio')
add_lib('smtparser', ['portfolio'], 'parsers/smt')
# add_dll('foci2', ['util'], 'interp/foci2stub',
# dll_name='foci2',

8
scripts/mk_util.py
View file

@ -54,6 +54,7 @@ CPP_COMPONENT='cpp'
IS_WINDOWS=False
IS_LINUX=False
IS_OSX=False
IS_FREEBSD=False
VERBOSE=True
DEBUG_MODE=False
SHOW_CPPS = True
@ -98,6 +99,9 @@ def is_windows():
def is_linux():
return IS_LINUX
def is_freebsd():
return IS_FREEBSD
def is_osx():
return IS_OSX
@ -426,6 +430,8 @@ elif os.name == 'posix':
IS_OSX=True
elif os.uname()[0] == 'Linux':
IS_LINUX=True
elif os.uname()[0] == 'FreeBSD':
IS_FREEBSD=True
def display_help(exit_code):
print("mk_make.py: Z3 Makefile generator\n")
@ -1181,6 +1187,8 @@ class JavaDLLComponent(Component):
t = t.replace('PLATFORM', 'darwin')
elif IS_LINUX:
t = t.replace('PLATFORM', 'linux')
elif IS_FREEBSD:
t = t.replace('PLATFORM', 'freebsd')
else:
t = t.replace('PLATFORM', 'win32')
out.write(t)

20
src/api/dotnet/Context.cs
View file

@ -302,11 +302,11 @@ namespace Microsoft.Z3
}
/// <summary>
/// Create a new finite domain sort.
/// <param name="name">The name used to identify the sort</param>
/// <param size="size">The size of the sort</param>
/// <returns>The result is a sort</returns>
/// Create a new finite domain sort.
/// <returns>The result is a sort</returns>
/// </summary>
/// <param name="name">The name used to identify the sort</param>
/// <param name="size">The size of the sort</param>
public FiniteDomainSort MkFiniteDomainSort(Symbol name, ulong size)
{
Contract.Requires(name != null);
@ -317,13 +317,13 @@ namespace Microsoft.Z3
}
/// <summary>
/// Create a new finite domain sort.
/// <param name="name">The name used to identify the sort</param>
/// <param size="size">The size of the sort</param>
/// <returns>The result is a sort</returns>
/// Elements of the sort are created using <seealso cref="MkNumeral"/>,
/// and the elements range from 0 to <tt>size-1</tt>.
/// Create a new finite domain sort.
/// <returns>The result is a sort</returns>
/// Elements of the sort are created using <seealso cref="MkNumeral(ulong, Sort)"/>,
/// and the elements range from 0 to <tt>size-1</tt>.
/// </summary>
/// <param name="name">The name used to identify the sort</param>
/// <param name="size">The size of the sort</param>
public FiniteDomainSort MkFiniteDomainSort(string name, ulong size)
{
Contract.Ensures(Contract.Result<FiniteDomainSort>() != null);

2
src/api/dotnet/Global.cs
View file

@ -43,7 +43,7 @@ namespace Microsoft.Z3
/// The parameter names are case-insensitive. The character '-' should be viewed as an "alias" for '_'.
/// Thus, the following parameter names are considered equivalent: "pp.decimal-precision" and "PP.DECIMAL_PRECISION".
/// This function can be used to set parameters for a specific Z3 module.
/// This can be done by using <module-name>.<parameter-name>.
/// This can be done by using [module-name].[parameter-name].
/// For example:
/// Z3_global_param_set('pp.decimal', 'true')
/// will set the parameter "decimal" in the module "pp" to true.

19
src/api/dotnet/Microsoft.Z3.csproj
View file

@ -24,8 +24,7 @@
<ErrorReport>prompt</ErrorReport>
<WarningLevel>4</WarningLevel>
<AllowUnsafeBlocks>true</AllowUnsafeBlocks>
<DocumentationFile>
</DocumentationFile>
<DocumentationFile>..\Debug\Microsoft.Z3.XML</DocumentationFile>
<CodeContractsEnableRuntimeChecking>False</CodeContractsEnableRuntimeChecking>
<CodeContractsRuntimeOnlyPublicSurface>False</CodeContractsRuntimeOnlyPublicSurface>
<CodeContractsRuntimeThrowOnFailure>True</CodeContractsRuntimeThrowOnFailure>
@ -140,6 +139,7 @@
<CodeContractsRuntimeCheckingLevel>Full</CodeContractsRuntimeCheckingLevel>
<CodeContractsReferenceAssembly>%28none%29</CodeContractsReferenceAssembly>
<CodeContractsAnalysisWarningLevel>0</CodeContractsAnalysisWarningLevel>
<DocumentationFile>..\x64\Debug\Microsoft.Z3.XML</DocumentationFile>
</PropertyGroup>
<PropertyGroup Condition="'$(Configuration)|$(Platform)' == 'Release|x64'">
<OutputPath>..\x64\external_64\</OutputPath>
@ -193,7 +193,7 @@
<PropertyGroup Condition="'$(Configuration)|$(Platform)' == 'external|x64'">
<OutputPath>..\x64\external\</OutputPath>
<AllowUnsafeBlocks>true</AllowUnsafeBlocks>
<DocumentationFile>..\external\Microsoft.Z3.xml</DocumentationFile>
<DocumentationFile>..\x64\external\Microsoft.Z3.XML</DocumentationFile>
<Optimize>true</Optimize>
<DebugType>pdbonly</DebugType>
<PlatformTarget>x64</PlatformTarget>
@ -220,7 +220,7 @@
<PropertyGroup Condition="'$(Configuration)|$(Platform)' == 'Release_delaysign|AnyCPU'">
<OutputPath>..\Release_delaysign\</OutputPath>
<AllowUnsafeBlocks>true</AllowUnsafeBlocks>
<DocumentationFile>..\Release_delaysign\Microsoft.Z3.xml</DocumentationFile>
<DocumentationFile>..\Release_delaysign\Microsoft.Z3.XML</DocumentationFile>
<Optimize>true</Optimize>
<DebugType>pdbonly</DebugType>
<PlatformTarget>AnyCPU</PlatformTarget>
@ -238,7 +238,7 @@
<PropertyGroup Condition="'$(Configuration)|$(Platform)' == 'Release_delaysign|x64'">
<OutputPath>bin\x64\Release_delaysign\</OutputPath>
<AllowUnsafeBlocks>true</AllowUnsafeBlocks>
<DocumentationFile>..\x64\external_64\Microsoft.Z3.xml</DocumentationFile>
<DocumentationFile>bin\x64\Release_delaysign\Microsoft.Z3.XML</DocumentationFile>
<Optimize>true</Optimize>
<DebugType>pdbonly</DebugType>
<PlatformTarget>x64</PlatformTarget>
@ -266,11 +266,12 @@
<CodeAnalysisRuleSet>MinimumRecommendedRules.ruleset</CodeAnalysisRuleSet>
<CodeAnalysisRuleSetDirectories>;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets</CodeAnalysisRuleSetDirectories>
<CodeAnalysisRuleDirectories>;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules</CodeAnalysisRuleDirectories>
<DocumentationFile>bin\x86\Debug\Microsoft.Z3.XML</DocumentationFile>
</PropertyGroup>
<PropertyGroup Condition="'$(Configuration)|$(Platform)' == 'Release|x86'">
<OutputPath>bin\x86\Release\</OutputPath>
<AllowUnsafeBlocks>true</AllowUnsafeBlocks>
<DocumentationFile>..\external\Microsoft.Z3.xml</DocumentationFile>
<DocumentationFile>bin\x86\Release\Microsoft.Z3.xml</DocumentationFile>
<Optimize>true</Optimize>
<DebugType>pdbonly</DebugType>
<PlatformTarget>x86</PlatformTarget>
@ -285,7 +286,7 @@
<PropertyGroup Condition="'$(Configuration)|$(Platform)' == 'external|x86'">
<OutputPath>bin\x86\external\</OutputPath>
<AllowUnsafeBlocks>true</AllowUnsafeBlocks>
<DocumentationFile>..\external\Microsoft.Z3.xml</DocumentationFile>
<DocumentationFile>bin\x86\external\Microsoft.Z3.XML</DocumentationFile>
<Optimize>true</Optimize>
<DebugType>pdbonly</DebugType>
<PlatformTarget>x86</PlatformTarget>
@ -303,7 +304,7 @@
<OutputPath>bin\x86\Release_delaysign\</OutputPath>
<DefineConstants>DELAYSIGN</DefineConstants>
<AllowUnsafeBlocks>true</AllowUnsafeBlocks>
<DocumentationFile>..\Release_delaysign\Microsoft.Z3.xml</DocumentationFile>
<DocumentationFile>bin\x86\Release_delaysign\Microsoft.Z3.XML</DocumentationFile>
<Optimize>true</Optimize>
<DebugType>pdbonly</DebugType>
<PlatformTarget>x86</PlatformTarget>
@ -399,4 +400,4 @@
<Target Name="AfterBuild">
</Target>
-->
</Project>
</Project>

6
src/api/dotnet/Solver.cs
View file

@ -132,7 +132,8 @@ namespace Microsoft.Z3
/// <remarks>
/// This API is an alternative to <see cref="Check"/> with assumptions for extracting unsat cores.
/// Both APIs can be used in the same solver. The unsat core will contain a combination
/// of the Boolean variables provided using <see cref="AssertAndTrack"/> and the Boolean literals
/// of the Boolean variables provided using <see cref="AssertAndTrack(BoolExpr[],BoolExpr[])"/>
/// and the Boolean literals
/// provided using <see cref="Check"/> with assumptions.
/// </remarks>
public void AssertAndTrack(BoolExpr[] constraints, BoolExpr[] ps)
@ -156,7 +157,8 @@ namespace Microsoft.Z3
/// <remarks>
/// This API is an alternative to <see cref="Check"/> with assumptions for extracting unsat cores.
/// Both APIs can be used in the same solver. The unsat core will contain a combination
/// of the Boolean variables provided using <see cref="AssertAndTrack"/> and the Boolean literals
/// of the Boolean variables provided using <see cref="AssertAndTrack(BoolExpr[],BoolExpr[])"/>
/// and the Boolean literals
/// provided using <see cref="Check"/> with assumptions.
/// </remarks>
public void AssertAndTrack(BoolExpr constraint, BoolExpr p)

2
src/api/python/z3printer.py
View file

@ -386,7 +386,7 @@ def seq3(args, lp='(', rp=')'):
else:
return group(indent(len(lp), compose(to_format(lp), seq(args), to_format(rp))))
class StopPPException:
class StopPPException(Exception):
def __str__(self):
return 'pp-interrupted'

225
src/tactic/fpa/fpa2bv_converter.cpp → src/ast/fpa/fpa2bv_converter.cpp
View file

@ -872,8 +872,19 @@ void fpa2bv_converter::mk_div(func_decl * f, unsigned num, expr * const * args,
sticky = m.mk_app(m_bv_util.get_fid(), OP_BREDOR, m_bv_util.mk_extract(extra_bits-2, 0, quotient));
res_sig = m_bv_util.mk_concat(m_bv_util.mk_extract(extra_bits+sbits+1, extra_bits-1, quotient), sticky);
SASSERT(m_bv_util.get_bv_size(res_sig) == (sbits + 4));
SASSERT(m_bv_util.get_bv_size(res_sig) == (sbits + 4));
expr_ref res_sig_lz(m);
mk_leading_zeros(res_sig, sbits + 4, res_sig_lz);
dbg_decouple("fpa2bv_div_res_sig_lz", res_sig_lz);
expr_ref res_sig_shift_amount(m);
res_sig_shift_amount = m_bv_util.mk_bv_sub(res_sig_lz, m_bv_util.mk_numeral(1, sbits + 4));
dbg_decouple("fpa2bv_div_res_sig_shift_amount", res_sig_shift_amount);
expr_ref shift_cond(m);
shift_cond = m_bv_util.mk_ule(res_sig_lz, m_bv_util.mk_numeral(1, sbits + 4));
m_simp.mk_ite(shift_cond, res_sig, m_bv_util.mk_bv_shl(res_sig, res_sig_shift_amount), res_sig);
m_simp.mk_ite(shift_cond, res_exp, m_bv_util.mk_bv_sub(res_exp, m_bv_util.mk_extract(ebits+1, 0, res_sig_shift_amount)), res_exp);
round(f->get_range(), rm, res_sgn, res_sig, res_exp, v8);
// And finally, we tie them together.
@ -2743,215 +2754,3 @@ void fpa2bv_converter::round(sort * s, expr_ref & rm, expr_ref & sgn, expr_ref &
TRACE("fpa2bv_round", tout << "ROUND = " << mk_ismt2_pp(result, m) << std::endl; );
}
void fpa2bv_model_converter::display(std::ostream & out) {
out << "(fpa2bv-model-converter";
for (obj_map<func_decl, expr*>::iterator it = m_const2bv.begin();
it != m_const2bv.end();
it++) {
const symbol & n = it->m_key->get_name();
out << "\n (" << n << " ";
unsigned indent = n.size() + 4;
out << mk_ismt2_pp(it->m_value, m, indent) << ")";
}
for (obj_map<func_decl, expr*>::iterator it = m_rm_const2bv.begin();
it != m_rm_const2bv.end();
it++) {
const symbol & n = it->m_key->get_name();
out << "\n (" << n << " ";
unsigned indent = n.size() + 4;
out << mk_ismt2_pp(it->m_value, m, indent) << ")";
}
for (obj_map<func_decl, func_decl*>::iterator it = m_uf2bvuf.begin();
it != m_uf2bvuf.end();
it++) {
const symbol & n = it->m_key->get_name();
out << "\n (" << n << " ";
unsigned indent = n.size() + 4;
out << mk_ismt2_pp(it->m_value, m, indent) << ")";
}
for (obj_map<func_decl, func_decl_triple>::iterator it = m_uf23bvuf.begin();
it != m_uf23bvuf.end();
it++) {
const symbol & n = it->m_key->get_name();
out << "\n (" << n << " ";
unsigned indent = n.size() + 4;
out << mk_ismt2_pp(it->m_value.f_sgn, m, indent) << " ; " <<
mk_ismt2_pp(it->m_value.f_sig, m, indent) << " ; " <<
mk_ismt2_pp(it->m_value.f_exp, m, indent) << " ; " <<
")";
}
out << ")" << std::endl;
}
model_converter * fpa2bv_model_converter::translate(ast_translation & translator) {
fpa2bv_model_converter * res = alloc(fpa2bv_model_converter, translator.to());
for (obj_map<func_decl, expr*>::iterator it = m_const2bv.begin();
it != m_const2bv.end();
it++)
{
func_decl * k = translator(it->m_key);
expr * v = translator(it->m_value);
res->m_const2bv.insert(k, v);
translator.to().inc_ref(k);
translator.to().inc_ref(v);
}
for (obj_map<func_decl, expr*>::iterator it = m_rm_const2bv.begin();
it != m_rm_const2bv.end();
it++)
{
func_decl * k = translator(it->m_key);
expr * v = translator(it->m_value);
res->m_rm_const2bv.insert(k, v);
translator.to().inc_ref(k);
translator.to().inc_ref(v);
}
return res;
}
void fpa2bv_model_converter::convert(model * bv_mdl, model * float_mdl) {
float_util fu(m);
bv_util bu(m);
mpf fp_val;
unsynch_mpz_manager & mpzm = fu.fm().mpz_manager();
unsynch_mpq_manager & mpqm = fu.fm().mpq_manager();
TRACE("fpa2bv_mc", tout << "BV Model: " << std::endl;
for (unsigned i = 0 ; i < bv_mdl->get_num_constants(); i++)
tout << bv_mdl->get_constant(i)->get_name() << " --> " <<
mk_ismt2_pp(bv_mdl->get_const_interp(bv_mdl->get_constant(i)), m) << std::endl;
);
obj_hashtable<func_decl> seen;
for (obj_map<func_decl, expr*>::iterator it = m_const2bv.begin();
it != m_const2bv.end();
it++)
{
func_decl * var = it->m_key;
app * a = to_app(it->m_value);
SASSERT(fu.is_float(var->get_range()));
SASSERT(var->get_range()->get_num_parameters() == 2);
unsigned ebits = fu.get_ebits(var->get_range());
unsigned sbits = fu.get_sbits(var->get_range());
expr_ref sgn(m), sig(m), exp(m);
sgn = bv_mdl->get_const_interp(to_app(a->get_arg(0))->get_decl());
sig = bv_mdl->get_const_interp(to_app(a->get_arg(1))->get_decl());
exp = bv_mdl->get_const_interp(to_app(a->get_arg(2))->get_decl());
seen.insert(to_app(a->get_arg(0))->get_decl());
seen.insert(to_app(a->get_arg(1))->get_decl());
seen.insert(to_app(a->get_arg(2))->get_decl());
if (!sgn && !sig && !exp)
continue;
unsigned sgn_sz = bu.get_bv_size(m.get_sort(a->get_arg(0)));
unsigned sig_sz = bu.get_bv_size(m.get_sort(a->get_arg(1))) - 1;
unsigned exp_sz = bu.get_bv_size(m.get_sort(a->get_arg(2)));
rational sgn_q(0), sig_q(0), exp_q(0);
if (sgn) bu.is_numeral(sgn, sgn_q, sgn_sz);
if (sig) bu.is_numeral(sig, sig_q, sig_sz);
if (exp) bu.is_numeral(exp, exp_q, exp_sz);
// un-bias exponent
rational exp_unbiased_q;
exp_unbiased_q = exp_q - fu.fm().m_powers2.m1(ebits-1);
mpz sig_z; mpf_exp_t exp_z;
mpzm.set(sig_z, sig_q.to_mpq().numerator());
exp_z = mpzm.get_int64(exp_unbiased_q.to_mpq().numerator());
TRACE("fpa2bv_mc", tout << var->get_name() << " == [" << sgn_q.to_string() << " " <<
mpzm.to_string(sig_z) << " " << exp_z << "(" << exp_q.to_string() << ")]" << std::endl; );
fu.fm().set(fp_val, ebits, sbits, !mpqm.is_zero(sgn_q.to_mpq()), sig_z, exp_z);
float_mdl->register_decl(var, fu.mk_value(fp_val));
mpzm.del(sig_z);
}
for (obj_map<func_decl, expr*>::iterator it = m_rm_const2bv.begin();
it != m_rm_const2bv.end();
it++)
{
func_decl * var = it->m_key;
app * a = to_app(it->m_value);
SASSERT(fu.is_rm(var->get_range()));
rational val(0);
unsigned sz = 0;
if (a && bu.is_numeral(a, val, sz)) {
TRACE("fpa2bv_mc", tout << var->get_name() << " == " << val.to_string() << std::endl; );
SASSERT(val.is_uint64());
switch (val.get_uint64())
{
case BV_RM_TIES_TO_AWAY: float_mdl->register_decl(var, fu.mk_round_nearest_ties_to_away()); break;
case BV_RM_TIES_TO_EVEN: float_mdl->register_decl(var, fu.mk_round_nearest_ties_to_even()); break;
case BV_RM_TO_NEGATIVE: float_mdl->register_decl(var, fu.mk_round_toward_negative()); break;
case BV_RM_TO_POSITIVE: float_mdl->register_decl(var, fu.mk_round_toward_positive()); break;
case BV_RM_TO_ZERO:
default: float_mdl->register_decl(var, fu.mk_round_toward_zero());
}
seen.insert(var);
}
}
for (obj_map<func_decl, func_decl*>::iterator it = m_uf2bvuf.begin();
it != m_uf2bvuf.end();
it++)
seen.insert(it->m_value);
for (obj_map<func_decl, func_decl_triple>::iterator it = m_uf23bvuf.begin();
it != m_uf23bvuf.end();
it++)
{
seen.insert(it->m_value.f_sgn);
seen.insert(it->m_value.f_sig);
seen.insert(it->m_value.f_exp);
}
fu.fm().del(fp_val);
// Keep all the non-float constants.
unsigned sz = bv_mdl->get_num_constants();
for (unsigned i = 0; i < sz; i++)
{
func_decl * c = bv_mdl->get_constant(i);
if (!seen.contains(c))
float_mdl->register_decl(c, bv_mdl->get_const_interp(c));
}
// And keep everything else
sz = bv_mdl->get_num_functions();
for (unsigned i = 0; i < sz; i++)
{
func_decl * f = bv_mdl->get_function(i);
if (!seen.contains(f))
{
TRACE("fpa2bv_mc", tout << "Keeping: " << mk_ismt2_pp(f, m) << std::endl; );
func_interp * val = bv_mdl->get_func_interp(f);
float_mdl->register_decl(f, val);
}
}
sz = bv_mdl->get_num_uninterpreted_sorts();
for (unsigned i = 0; i < sz; i++)
{
sort * s = bv_mdl->get_uninterpreted_sort(i);
ptr_vector<expr> u = bv_mdl->get_universe(s);
float_mdl->register_usort(s, u.size(), u.c_ptr());
}
}
model_converter * mk_fpa2bv_model_converter(ast_manager & m,
obj_map<func_decl, expr*> const & const2bv,
obj_map<func_decl, expr*> const & rm_const2bv,
obj_map<func_decl, func_decl*> const & uf2bvuf,
obj_map<func_decl, func_decl_triple> const & uf23bvuf) {
return alloc(fpa2bv_model_converter, m, const2bv, rm_const2bv, uf2bvuf, uf23bvuf);
}

85
src/tactic/fpa/fpa2bv_converter.h → src/ast/fpa/fpa2bv_converter.h
View file

@ -24,13 +24,10 @@ Notes:
#include"ref_util.h"
#include"float_decl_plugin.h"
#include"bv_decl_plugin.h"
#include"model_converter.h"
#include"basic_simplifier_plugin.h"
typedef enum { BV_RM_TIES_TO_AWAY=0, BV_RM_TIES_TO_EVEN=1, BV_RM_TO_NEGATIVE=2, BV_RM_TO_POSITIVE=3, BV_RM_TO_ZERO=4 } BV_RM_VAL;
class fpa2bv_model_converter;
struct func_decl_triple {
func_decl_triple () { f_sgn = 0; f_sig = 0; f_exp = 0; }
func_decl_triple (func_decl * sgn, func_decl * sig, func_decl * exp)
@ -173,86 +170,4 @@ protected:
expr_ref & res_sgn, expr_ref & res_sig, expr_ref & res_exp);
};
class fpa2bv_model_converter : public model_converter {
ast_manager & m;
obj_map<func_decl, expr*> m_const2bv;
obj_map<func_decl, expr*> m_rm_const2bv;
obj_map<func_decl, func_decl*> m_uf2bvuf;
obj_map<func_decl, func_decl_triple> m_uf23bvuf;
public:
fpa2bv_model_converter(ast_manager & m, obj_map<func_decl, expr*> const & const2bv,
obj_map<func_decl, expr*> const & rm_const2bv,
obj_map<func_decl, func_decl*> const & uf2bvuf,
obj_map<func_decl, func_decl_triple> const & uf23bvuf) :
m(m) {
// Just create a copy?
for (obj_map<func_decl, expr*>::iterator it = const2bv.begin();
it != const2bv.end();
it++)
{
m_const2bv.insert(it->m_key, it->m_value);
m.inc_ref(it->m_key);
m.inc_ref(it->m_value);
}
for (obj_map<func_decl, expr*>::iterator it = rm_const2bv.begin();
it != rm_const2bv.end();
it++)
{
m_rm_const2bv.insert(it->m_key, it->m_value);
m.inc_ref(it->m_key);
m.inc_ref(it->m_value);
}
for (obj_map<func_decl, func_decl*>::iterator it = uf2bvuf.begin();
it != uf2bvuf.end();
it++)
{
m_uf2bvuf.insert(it->m_key, it->m_value);
m.inc_ref(it->m_key);
m.inc_ref(it->m_value);
}
for (obj_map<func_decl, func_decl_triple>::iterator it = uf23bvuf.begin();
it != uf23bvuf.end();
it++)
{
m_uf23bvuf.insert(it->m_key, it->m_value);
m.inc_ref(it->m_key);
}
}
virtual ~fpa2bv_model_converter() {
dec_ref_map_key_values(m, m_const2bv);
dec_ref_map_key_values(m, m_rm_const2bv);
}
virtual void operator()(model_ref & md, unsigned goal_idx) {
SASSERT(goal_idx == 0);
model * new_model = alloc(model, m);
obj_hashtable<func_decl> bits;
convert(md.get(), new_model);
md = new_model;
}
virtual void operator()(model_ref & md) {
operator()(md, 0);
}
void display(std::ostream & out);
virtual model_converter * translate(ast_translation & translator);
protected:
fpa2bv_model_converter(ast_manager & m) : m(m) { }
void convert(model * bv_mdl, model * float_mdl);
};
model_converter * mk_fpa2bv_model_converter(ast_manager & m,
obj_map<func_decl, expr*> const & const2bv,
obj_map<func_decl, expr*> const & rm_const2bv,
obj_map<func_decl, func_decl*> const & uf2bvuf,
obj_map<func_decl, func_decl_triple> const & uf23bvuf);
#endif

0
src/tactic/fpa/fpa2bv_rewriter.h → src/ast/fpa/fpa2bv_rewriter.h
View file

2
src/ast/scoped_proof.h
View file

@ -17,7 +17,7 @@ Revision History:
--*/
#ifndef _SCOPED_PROOF__H_
#define _SCOPED_PROOF_H_
#define _SCOPED_PROOF__H_
#include "ast.h"

2
src/cmd_context/pdecl.cpp
View file

@ -189,7 +189,7 @@ class psort_app : public psort {
m.inc_ref(d);
m.inc_ref(num_args, args);
SASSERT(num_args == m_decl->get_num_params() || m_decl->has_var_params());
DEBUG_CODE(for (unsigned i = 0; i < num_params; i++) args[i]->check_num_params(this););
DEBUG_CODE(if (num_args == num_params) { for (unsigned i = 0; i < num_params; i++) args[i]->check_num_params(this); });
}
virtual void finalize(pdecl_manager & m) {

2
src/duality/duality.h
View file

@ -29,7 +29,7 @@ using namespace stl_ext;
namespace Duality {
class implicant_solver;
struct implicant_solver;
/* Generic operations on Z3 formulas */

2
src/duality/duality_solver.cpp
View file

@ -2220,7 +2220,7 @@ namespace Duality {
#endif
int expand_max = 1;
if(0&&duality->BatchExpand){
int thing = stack.size() * 0.1;
int thing = stack.size() / 10; // * 0.1;
expand_max = std::max(1,thing);
if(expand_max > 1)
std::cout << "foo!\n";

2
src/math/polynomial/upolynomial_factorization.cpp
View file

@ -530,7 +530,7 @@ bool check_hansel_lift(z_manager & upm, numeral_vector const & C,
upm.mul(A_lifted.size(), A_lifted.c_ptr(), B_lifted.size(), B_lifted.c_ptr(), test1);
upm.sub(C.size(), C.c_ptr(), test1.size(), test1.c_ptr(), test1);
to_zp_manager(br_upm, test1);
if (!test1.size() == 0) {
if (test1.size() != 0) {
TRACE("polynomial::factorization::bughunt",
tout << "sage: R.<x> = ZZ['x']" << endl;
tout << "sage: A = "; upm.display(tout, A); tout << endl;

4
src/model/model.cpp
View file

@ -133,7 +133,9 @@ bool model::eval(expr * e, expr_ref & result, bool model_completion) {
ev(e, result);
return true;
}
catch (model_evaluator_exception &) {
catch (model_evaluator_exception & ex) {
(void)ex;
TRACE("model_evaluator", tout << ex.msg() << "\n";);
return false;
}
}

6
src/muz/base/dl_context.h
View file

@ -278,6 +278,12 @@ namespace datalog {
void register_variable(func_decl* var);
/*
Replace constants that have been registered as
variables by de-Bruijn indices and corresponding
universal (if is_forall is true) or existential
quantifier.
*/
expr_ref bind_variables(expr* fml, bool is_forall);
/**

18
src/muz/transforms/dl_mk_coi_filter.cpp
View file

@ -200,7 +200,23 @@ namespace datalog {
func_decl_set::iterator it = pruned_preds.begin();
extension_model_converter* mc0 = alloc(extension_model_converter, m);
for (; it != end; ++it) {
mc0->insert(*it, m.mk_true());
const rule_vector& rules = source.get_predicate_rules(*it);
expr_ref_vector fmls(m);
for (unsigned i = 0; i < rules.size(); ++i) {
app* head = rules[i]->get_head();
expr_ref_vector conj(m);
unsigned n = head->get_num_args()-1;
for (unsigned j = 0; j < head->get_num_args(); ++j) {
expr* arg = head->get_arg(j);
if (!is_var(arg)) {
conj.push_back(m.mk_eq(m.mk_var(j, m.get_sort(arg)), arg));
}
}
fmls.push_back(m.mk_and(conj.size(), conj.c_ptr()));
}
expr_ref fml(m);
fml = m.mk_or(fmls.size(), fmls.c_ptr());
mc0->insert(*it, fml);
}
m_context.add_model_converter(mc0);
}

2
src/qe/qe_sat_tactic.cpp
View file

@ -226,7 +226,7 @@ namespace qe {
return alloc(sat_tactic, m);
}
~sat_tactic() {
virtual ~sat_tactic() {
for (unsigned i = 0; i < m_solvers.size(); ++i) {
dealloc(m_solvers[i]);
}

37
src/smt/proto_model/datatype_factory.cpp
View file

@ -20,6 +20,7 @@ Revision History:
#include"proto_model.h"
#include"ast_pp.h"
#include"ast_ll_pp.h"
#include"expr_functors.h"
datatype_factory::datatype_factory(ast_manager & m, proto_model & md):
struct_factory(m, m.mk_family_id("datatype"), md),
@ -47,8 +48,10 @@ expr * datatype_factory::get_some_value(sort * s) {
*/
expr * datatype_factory::get_last_fresh_value(sort * s) {
expr * val = 0;
if (m_last_fresh_value.find(s, val))
if (m_last_fresh_value.find(s, val)) {
TRACE("datatype_factory", tout << "cached fresh value: " << mk_pp(val, m_manager) << "\n";);
return val;
}
value_set * set = get_value_set(s);
if (set->empty())
val = get_some_value(s);
@ -59,6 +62,17 @@ expr * datatype_factory::get_last_fresh_value(sort * s) {
return val;
}
bool datatype_factory::is_subterm_of_last_value(app* e) {
expr* last;
if (!m_last_fresh_value.find(m_manager.get_sort(e), last)) {
return false;
}
contains_app contains(m_manager, e);
bool result = contains(last);
TRACE("datatype_factory", tout << mk_pp(e, m_manager) << " in " << mk_pp(last, m_manager) << " " << result << "\n";);
return result;
}
/**
\brief Create an almost fresh value. If s is recursive, then the result is not 0.
It also updates m_last_fresh_value
@ -105,11 +119,18 @@ expr * datatype_factory::get_almost_fresh_value(sort * s) {
}
}
if (recursive || found_fresh_arg) {
expr * new_value = m_manager.mk_app(constructor, args.size(), args.c_ptr());
app * new_value = m_manager.mk_app(constructor, args.size(), args.c_ptr());
SASSERT(!found_fresh_arg || !set->contains(new_value));
register_value(new_value);
if (m_util.is_recursive(s))
m_last_fresh_value.insert(s, new_value);
if (m_util.is_recursive(s)) {
if (is_subterm_of_last_value(new_value)) {
new_value = static_cast<app*>(m_last_fresh_value.find(s));
}
else {
m_last_fresh_value.insert(s, new_value);
}
}
TRACE("datatype_factory", tout << "almost fresh: " << mk_pp(new_value, m_manager) << "\n";);
return new_value;
}
}
@ -181,12 +202,20 @@ expr * datatype_factory::get_fresh_value(sort * s) {
expr_ref_vector args(m_manager);
bool found_sibling = false;
unsigned num = constructor->get_arity();
TRACE("datatype_factory", tout << "checking constructor: " << constructor->get_name() << "\n";);
for (unsigned i = 0; i < num; i++) {
sort * s_arg = constructor->get_domain(i);
TRACE("datatype_factory", tout << mk_pp(s, m_manager) << " "
<< mk_pp(s_arg, m_manager) << " are_siblings "
<< m_util.are_siblings(s, s_arg) << " is_datatype "
<< m_util.is_datatype(s_arg) << " found_sibling "
<< found_sibling << "\n";);
if (!found_sibling && m_util.is_datatype(s_arg) && m_util.are_siblings(s, s_arg)) {
found_sibling = true;
expr * maybe_new_arg = get_almost_fresh_value(s_arg);
if (!maybe_new_arg) {
TRACE("datatype_factory",
tout << "no argument found for " << mk_pp(s_arg, m_manager) << "\n";);
maybe_new_arg = m_model.get_some_value(s_arg);
found_sibling = false;
}

2
src/smt/proto_model/datatype_factory.h
View file

@ -29,6 +29,8 @@ class datatype_factory : public struct_factory {
expr * get_last_fresh_value(sort * s);
expr * get_almost_fresh_value(sort * s);
bool is_subterm_of_last_value(app* e);
public:
datatype_factory(ast_manager & m, proto_model & md);
virtual ~datatype_factory() {}

3
src/smt/proto_model/proto_model.cpp
View file

@ -247,6 +247,7 @@ bool proto_model::eval(expr * e, expr_ref & result, bool model_completion) {
new_t = mk_some_interp_for(f);
}
else {
TRACE("model_eval", tout << f->get_name() << " is uninterpreted\n";);
is_ok = false;
}
}
@ -294,6 +295,7 @@ bool proto_model::eval(expr * e, expr_ref & result, bool model_completion) {
// f is an uninterpreted function, there is no need to use m_simplifier.mk_app
new_t = m_manager.mk_app(f, num_args, args.c_ptr());
trail.push_back(new_t);
TRACE("model_eval", tout << f->get_name() << " is uninterpreted\n";);
is_ok = false;
}
}
@ -326,6 +328,7 @@ bool proto_model::eval(expr * e, expr_ref & result, bool model_completion) {
todo.pop_back();
break;
case AST_QUANTIFIER:
TRACE("model_eval", tout << "found quantifier\n" << mk_pp(a, m_manager) << "\n";);
is_ok = false; // evaluator does not handle quantifiers.
SASSERT(a != 0);
eval_cache.insert(a, a);

21
src/smt/smt_model_finder.cpp
View file

@ -396,7 +396,7 @@ namespace smt {
// Support for evaluating expressions in the current model.
proto_model * m_model;
obj_map<expr, expr *> m_eval_cache;
obj_map<expr, expr *> m_eval_cache[2];
expr_ref_vector m_eval_cache_range;
ptr_vector<node> m_root_nodes;
@ -409,7 +409,8 @@ namespace smt {
}
void reset_eval_cache() {
m_eval_cache.reset();
m_eval_cache[0].reset();
m_eval_cache[1].reset();
m_eval_cache_range.reset();
}
@ -468,6 +469,7 @@ namespace smt {
~auf_solver() {
flush_nodes();
reset_eval_cache();
}
void set_context(context * ctx) {
@ -547,7 +549,7 @@ namespace smt {
for (obj_map<expr, unsigned>::iterator it = elems.begin(); it != elems.end(); it++) {
expr * n = it->m_key;
expr * n_val = eval(n, true);
if (!m_manager.is_value(n_val))
if (!n_val || !m_manager.is_value(n_val))
to_delete.push_back(n);
}
for (ptr_vector<expr>::iterator it = to_delete.begin(); it != to_delete.end(); it++) {
@ -569,16 +571,19 @@ namespace smt {
virtual expr * eval(expr * n, bool model_completion) {
expr * r = 0;
if (m_eval_cache.find(n, r)) {
if (m_eval_cache[model_completion].find(n, r)) {
return r;
}
expr_ref tmp(m_manager);
if (!m_model->eval(n, tmp, model_completion))
if (!m_model->eval(n, tmp, model_completion)) {
r = 0;
else
TRACE("model_finder", tout << "eval\n" << mk_pp(n, m_manager) << "\n-----> null\n";);
}
else {
r = tmp;
TRACE("model_finder", tout << "eval\n" << mk_pp(n, m_manager) << "\n----->\n" << mk_pp(r, m_manager) << "\n";);
m_eval_cache.insert(n, r);
TRACE("model_finder", tout << "eval\n" << mk_pp(n, m_manager) << "\n----->\n" << mk_pp(r, m_manager) << "\n";);
}
m_eval_cache[model_completion].insert(n, r);
m_eval_cache_range.push_back(r);
return r;
}

46
src/smt/theory_fpa.cpp Normal file
View file

@ -0,0 +1,46 @@
/*++
Copyright (c) 2014 Microsoft Corporation
Module Name:
theory_fpa.cpp
Abstract:
Floating-Point Theory Plugin
Author:
Christoph (cwinter) 2014-04-23
Revision History:
--*/
#include"ast_smt2_pp.h"
#include"theory_fpa.h"
namespace smt {
bool theory_fpa::internalize_atom(app * atom, bool gate_ctx) {
TRACE("bv", tout << "internalizing atom: " << mk_ismt2_pp(atom, get_manager()) << "\n";);
SASSERT(atom->get_family_id() == get_family_id());
NOT_IMPLEMENTED_YET();
return true;
}
void theory_fpa::new_eq_eh(theory_var, theory_var) {
NOT_IMPLEMENTED_YET();
}
void theory_fpa::new_diseq_eh(theory_var, theory_var) {
NOT_IMPLEMENTED_YET();
}
void theory_fpa::push_scope_eh() {
NOT_IMPLEMENTED_YET();
}
void theory_fpa::pop_scope_eh(unsigned num_scopes) {
NOT_IMPLEMENTED_YET();
}
};

45
src/smt/theory_fpa.h Normal file
View file

@ -0,0 +1,45 @@
/*++
Copyright (c) 2014 Microsoft Corporation
Module Name:
theory_fpa.h
Abstract:
Floating-Point Theory Plugin
Author:
Christoph (cwinter) 2014-04-23
Revision History:
--*/
#ifndef _THEORY_FPA_H_
#define _THEORY_FPA_H_
#include"smt_theory.h"
#include"fpa2bv_converter.h"
namespace smt {
class theory_fpa : public theory {
fpa2bv_converter m_converter;
virtual final_check_status final_check_eh() { return FC_DONE; }
virtual bool internalize_atom(app*, bool);
virtual bool internalize_term(app*) { return internalize_atom(0, false); }
virtual void new_eq_eh(theory_var, theory_var);
virtual void new_diseq_eh(theory_var, theory_var);
virtual void push_scope_eh();
virtual void pop_scope_eh(unsigned num_scopes);
virtual theory* mk_fresh(context*) { return alloc(theory_fpa, get_manager()); }
virtual char const * get_name() const { return "fpa"; }
public:
theory_fpa(ast_manager& m) : theory(m.mk_family_id("fpa")), m_converter(m) {}
};
};
#endif /* _THEORY_FPA_H_ */

232
src/tactic/fpa/fpa2bv_model_converter.cpp Normal file
View file

@ -0,0 +1,232 @@
/*++
Copyright (c) 2012 Microsoft Corporation
Module Name:
fpa2bv_model_converter.h
Abstract:
Model conversion for fpa2bv_converter
Author:
Christoph (cwinter) 2012-02-09
Notes:
--*/
#include"ast_smt2_pp.h"
#include"fpa2bv_model_converter.h"
void fpa2bv_model_converter::display(std::ostream & out) {
out << "(fpa2bv-model-converter";
for (obj_map<func_decl, expr*>::iterator it = m_const2bv.begin();
it != m_const2bv.end();
it++) {
const symbol & n = it->m_key->get_name();
out << "\n (" << n << " ";
unsigned indent = n.size() + 4;
out << mk_ismt2_pp(it->m_value, m, indent) << ")";
}
for (obj_map<func_decl, expr*>::iterator it = m_rm_const2bv.begin();
it != m_rm_const2bv.end();
it++) {
const symbol & n = it->m_key->get_name();
out << "\n (" << n << " ";
unsigned indent = n.size() + 4;
out << mk_ismt2_pp(it->m_value, m, indent) << ")";
}
for (obj_map<func_decl, func_decl*>::iterator it = m_uf2bvuf.begin();
it != m_uf2bvuf.end();
it++) {
const symbol & n = it->m_key->get_name();
out << "\n (" << n << " ";
unsigned indent = n.size() + 4;
out << mk_ismt2_pp(it->m_value, m, indent) << ")";
}
for (obj_map<func_decl, func_decl_triple>::iterator it = m_uf23bvuf.begin();
it != m_uf23bvuf.end();
it++) {
const symbol & n = it->m_key->get_name();
out << "\n (" << n << " ";
unsigned indent = n.size() + 4;
out << mk_ismt2_pp(it->m_value.f_sgn, m, indent) << " ; " <<
mk_ismt2_pp(it->m_value.f_sig, m, indent) << " ; " <<
mk_ismt2_pp(it->m_value.f_exp, m, indent) << " ; " <<
")";
}
out << ")" << std::endl;
}
model_converter * fpa2bv_model_converter::translate(ast_translation & translator) {
fpa2bv_model_converter * res = alloc(fpa2bv_model_converter, translator.to());
for (obj_map<func_decl, expr*>::iterator it = m_const2bv.begin();
it != m_const2bv.end();
it++)
{
func_decl * k = translator(it->m_key);
expr * v = translator(it->m_value);
res->m_const2bv.insert(k, v);
translator.to().inc_ref(k);
translator.to().inc_ref(v);
}
for (obj_map<func_decl, expr*>::iterator it = m_rm_const2bv.begin();
it != m_rm_const2bv.end();
it++)
{
func_decl * k = translator(it->m_key);
expr * v = translator(it->m_value);
res->m_rm_const2bv.insert(k, v);
translator.to().inc_ref(k);
translator.to().inc_ref(v);
}
return res;
}
void fpa2bv_model_converter::convert(model * bv_mdl, model * float_mdl) {
float_util fu(m);
bv_util bu(m);
mpf fp_val;
unsynch_mpz_manager & mpzm = fu.fm().mpz_manager();
unsynch_mpq_manager & mpqm = fu.fm().mpq_manager();
TRACE("fpa2bv_mc", tout << "BV Model: " << std::endl;
for (unsigned i = 0; i < bv_mdl->get_num_constants(); i++)
tout << bv_mdl->get_constant(i)->get_name() << " --> " <<
mk_ismt2_pp(bv_mdl->get_const_interp(bv_mdl->get_constant(i)), m) << std::endl;
);
obj_hashtable<func_decl> seen;
for (obj_map<func_decl, expr*>::iterator it = m_const2bv.begin();
it != m_const2bv.end();
it++)
{
func_decl * var = it->m_key;
app * a = to_app(it->m_value);
SASSERT(fu.is_float(var->get_range()));
SASSERT(var->get_range()->get_num_parameters() == 2);
unsigned ebits = fu.get_ebits(var->get_range());
unsigned sbits = fu.get_sbits(var->get_range());
expr_ref sgn(m), sig(m), exp(m);
sgn = bv_mdl->get_const_interp(to_app(a->get_arg(0))->get_decl());
sig = bv_mdl->get_const_interp(to_app(a->get_arg(1))->get_decl());
exp = bv_mdl->get_const_interp(to_app(a->get_arg(2))->get_decl());
seen.insert(to_app(a->get_arg(0))->get_decl());
seen.insert(to_app(a->get_arg(1))->get_decl());
seen.insert(to_app(a->get_arg(2))->get_decl());
if (!sgn && !sig && !exp)
continue;
unsigned sgn_sz = bu.get_bv_size(m.get_sort(a->get_arg(0)));
unsigned sig_sz = bu.get_bv_size(m.get_sort(a->get_arg(1))) - 1;
unsigned exp_sz = bu.get_bv_size(m.get_sort(a->get_arg(2)));
rational sgn_q(0), sig_q(0), exp_q(0);
if (sgn) bu.is_numeral(sgn, sgn_q, sgn_sz);
if (sig) bu.is_numeral(sig, sig_q, sig_sz);
if (exp) bu.is_numeral(exp, exp_q, exp_sz);
// un-bias exponent
rational exp_unbiased_q;
exp_unbiased_q = exp_q - fu.fm().m_powers2.m1(ebits - 1);
mpz sig_z; mpf_exp_t exp_z;
mpzm.set(sig_z, sig_q.to_mpq().numerator());
exp_z = mpzm.get_int64(exp_unbiased_q.to_mpq().numerator());
TRACE("fpa2bv_mc", tout << var->get_name() << " == [" << sgn_q.to_string() << " " <<
mpzm.to_string(sig_z) << " " << exp_z << "(" << exp_q.to_string() << ")]" << std::endl;);
fu.fm().set(fp_val, ebits, sbits, !mpqm.is_zero(sgn_q.to_mpq()), sig_z, exp_z);
float_mdl->register_decl(var, fu.mk_value(fp_val));
mpzm.del(sig_z);
}
for (obj_map<func_decl, expr*>::iterator it = m_rm_const2bv.begin();
it != m_rm_const2bv.end();
it++)
{
func_decl * var = it->m_key;
app * a = to_app(it->m_value);
SASSERT(fu.is_rm(var->get_range()));
rational val(0);
unsigned sz = 0;
if (a && bu.is_numeral(a, val, sz)) {
TRACE("fpa2bv_mc", tout << var->get_name() << " == " << val.to_string() << std::endl;);
SASSERT(val.is_uint64());
switch (val.get_uint64())
{
case BV_RM_TIES_TO_AWAY: float_mdl->register_decl(var, fu.mk_round_nearest_ties_to_away()); break;
case BV_RM_TIES_TO_EVEN: float_mdl->register_decl(var, fu.mk_round_nearest_ties_to_even()); break;
case BV_RM_TO_NEGATIVE: float_mdl->register_decl(var, fu.mk_round_toward_negative()); break;
case BV_RM_TO_POSITIVE: float_mdl->register_decl(var, fu.mk_round_toward_positive()); break;
case BV_RM_TO_ZERO:
default: float_mdl->register_decl(var, fu.mk_round_toward_zero());
}
seen.insert(var);
}
}
for (obj_map<func_decl, func_decl*>::iterator it = m_uf2bvuf.begin();
it != m_uf2bvuf.end();
it++)
seen.insert(it->m_value);
for (obj_map<func_decl, func_decl_triple>::iterator it = m_uf23bvuf.begin();
it != m_uf23bvuf.end();
it++)
{
seen.insert(it->m_value.f_sgn);
seen.insert(it->m_value.f_sig);
seen.insert(it->m_value.f_exp);
}
fu.fm().del(fp_val);
// Keep all the non-float constants.
unsigned sz = bv_mdl->get_num_constants();
for (unsigned i = 0; i < sz; i++)
{
func_decl * c = bv_mdl->get_constant(i);
if (!seen.contains(c))
float_mdl->register_decl(c, bv_mdl->get_const_interp(c));
}
// And keep everything else
sz = bv_mdl->get_num_functions();
for (unsigned i = 0; i < sz; i++)
{
func_decl * f = bv_mdl->get_function(i);
if (!seen.contains(f))
{
TRACE("fpa2bv_mc", tout << "Keeping: " << mk_ismt2_pp(f, m) << std::endl;);
func_interp * val = bv_mdl->get_func_interp(f);
float_mdl->register_decl(f, val);
}
}
sz = bv_mdl->get_num_uninterpreted_sorts();
for (unsigned i = 0; i < sz; i++)
{
sort * s = bv_mdl->get_uninterpreted_sort(i);
ptr_vector<expr> u = bv_mdl->get_universe(s);
float_mdl->register_usort(s, u.size(), u.c_ptr());
}
}
model_converter * mk_fpa2bv_model_converter(ast_manager & m,
obj_map<func_decl, expr*> const & const2bv,
obj_map<func_decl, expr*> const & rm_const2bv,
obj_map<func_decl, func_decl*> const & uf2bvuf,
obj_map<func_decl, func_decl_triple> const & uf23bvuf) {
return alloc(fpa2bv_model_converter, m, const2bv, rm_const2bv, uf2bvuf, uf23bvuf);
}

106
src/tactic/fpa/fpa2bv_model_converter.h Normal file
View file

@ -0,0 +1,106 @@
/*++
Copyright (c) 2012 Microsoft Corporation
Module Name:
fpa2bv_model_converter.h
Abstract:
Model conversion for fpa2bv_converter
Author:
Christoph (cwinter) 2012-02-09
Notes:
--*/
#ifndef _FPA2BV_MODEL_CONVERTER_H_
#define _FPA2BV_MODEL_CONVERTER_H_
#include"fpa2bv_converter.h"
#include"model_converter.h"
class fpa2bv_model_converter : public model_converter {
ast_manager & m;
obj_map<func_decl, expr*> m_const2bv;
obj_map<func_decl, expr*> m_rm_const2bv;
obj_map<func_decl, func_decl*> m_uf2bvuf;
obj_map<func_decl, func_decl_triple> m_uf23bvuf;
public:
fpa2bv_model_converter(ast_manager & m, obj_map<func_decl, expr*> const & const2bv,
obj_map<func_decl, expr*> const & rm_const2bv,
obj_map<func_decl, func_decl*> const & uf2bvuf,
obj_map<func_decl, func_decl_triple> const & uf23bvuf) :
m(m) {
// Just create a copy?
for (obj_map<func_decl, expr*>::iterator it = const2bv.begin();
it != const2bv.end();
it++)
{
m_const2bv.insert(it->m_key, it->m_value);
m.inc_ref(it->m_key);
m.inc_ref(it->m_value);
}
for (obj_map<func_decl, expr*>::iterator it = rm_const2bv.begin();
it != rm_const2bv.end();
it++)
{
m_rm_const2bv.insert(it->m_key, it->m_value);
m.inc_ref(it->m_key);
m.inc_ref(it->m_value);
}
for (obj_map<func_decl, func_decl*>::iterator it = uf2bvuf.begin();
it != uf2bvuf.end();
it++)
{
m_uf2bvuf.insert(it->m_key, it->m_value);
m.inc_ref(it->m_key);
m.inc_ref(it->m_value);
}
for (obj_map<func_decl, func_decl_triple>::iterator it = uf23bvuf.begin();
it != uf23bvuf.end();
it++)
{
m_uf23bvuf.insert(it->m_key, it->m_value);
m.inc_ref(it->m_key);
}
}
virtual ~fpa2bv_model_converter() {
dec_ref_map_key_values(m, m_const2bv);
dec_ref_map_key_values(m, m_rm_const2bv);
}
virtual void operator()(model_ref & md, unsigned goal_idx) {
SASSERT(goal_idx == 0);
model * new_model = alloc(model, m);
obj_hashtable<func_decl> bits;
convert(md.get(), new_model);
md = new_model;
}
virtual void operator()(model_ref & md) {
operator()(md, 0);
}
void display(std::ostream & out);
virtual model_converter * translate(ast_translation & translator);
protected:
fpa2bv_model_converter(ast_manager & m) : m(m) { }
void convert(model * bv_mdl, model * float_mdl);
};
model_converter * mk_fpa2bv_model_converter(ast_manager & m,
obj_map<func_decl, expr*> const & const2bv,
obj_map<func_decl, expr*> const & rm_const2bv,
obj_map<func_decl, func_decl*> const & uf2bvuf,
obj_map<func_decl, func_decl_triple> const & uf23bvuf);
#endif

1
src/tactic/fpa/fpa2bv_tactic.cpp
View file

@ -20,6 +20,7 @@ Notes:
#include"fpa2bv_rewriter.h"
#include"simplify_tactic.h"
#include"fpa2bv_tactic.h"
#include"fpa2bv_model_converter.h"
class fpa2bv_tactic : public tactic {
struct imp {

64
src/util/scoped_timer.cpp
View file

@ -70,7 +70,9 @@ struct scoped_timer::imp {
pthread_t m_thread_id;
pthread_attr_t m_attributes;
unsigned m_interval;
pthread_mutex_t m_mutex;
pthread_cond_t m_condition_var;
struct timespec m_end_time;
#elif defined(_LINUX_) || defined(_FREEBSD_)
// Linux & FreeBSD
timer_t m_timerid;
@ -93,35 +95,15 @@ struct scoped_timer::imp {
static void * thread_func(void * arg) {
scoped_timer::imp * st = static_cast<scoped_timer::imp*>(arg);
pthread_mutex_t mutex;
clock_serv_t host_clock;
struct timespec abstime;
mach_timespec_t now;
unsigned long long nano = static_cast<unsigned long long>(st->m_interval) * 1000000ull;
pthread_mutex_lock(&st->m_mutex);
host_get_clock_service(mach_host_self(), CALENDAR_CLOCK, &host_clock);
if (pthread_mutex_init(&mutex, NULL) != 0)
throw default_exception("failed to initialize timer mutex");
if (pthread_cond_init(&st->m_condition_var, NULL) != 0)
throw default_exception("failed to initialize timer condition variable");
abstime.tv_sec = nano / 1000000000ull;
abstime.tv_nsec = nano % 1000000000ull;
pthread_mutex_lock(&mutex);
clock_get_time(host_clock, &now);
ADD_MACH_TIMESPEC(&abstime, &now);
int e = pthread_cond_timedwait(&st->m_condition_var, &mutex, &abstime);
int e = pthread_cond_timedwait(&st->m_condition_var, &st->m_mutex, &st->m_end_time);
if (e != 0 && e != ETIMEDOUT)
throw default_exception("failed to start timed wait");
st->m_eh->operator()();
pthread_mutex_unlock(&mutex);
if (pthread_mutex_destroy(&mutex) != 0)
throw default_exception("failed to destroy pthread mutex");
if (pthread_cond_destroy(&st->m_condition_var) != 0)
throw default_exception("failed to destroy pthread condition variable");
pthread_mutex_unlock(&st->m_mutex);
return st;
}
#elif defined(_LINUX_) || defined(_FREEBSD_)
@ -150,6 +132,22 @@ struct scoped_timer::imp {
m_interval = ms;
if (pthread_attr_init(&m_attributes) != 0)
throw default_exception("failed to initialize timer thread attributes");
if (pthread_cond_init(&m_condition_var, NULL) != 0)
throw default_exception("failed to initialize timer condition variable");
if (pthread_mutex_init(&m_mutex, NULL) != 0)
throw default_exception("failed to initialize timer mutex");
clock_serv_t host_clock;
mach_timespec_t now;
unsigned long long nano = static_cast<unsigned long long>(m_interval) * 1000000ull;
host_get_clock_service(mach_host_self(), CALENDAR_CLOCK, &host_clock);
m_end_time.tv_sec = nano / 1000000000ull;
m_end_time.tv_nsec = nano % 1000000000ull;
clock_get_time(host_clock, &now);
ADD_MACH_TIMESPEC(&m_end_time, &now);
if (pthread_create(&m_thread_id, &m_attributes, &thread_func, this) != 0)
throw default_exception("failed to start timer thread");
#elif defined(_LINUX_) || defined(_FREEBSD_)
@ -183,9 +181,25 @@ struct scoped_timer::imp {
INVALID_HANDLE_VALUE);
#elif defined(__APPLE__) && defined(__MACH__)
// Mac OS X
pthread_cond_signal(&m_condition_var); // this is okay to fail
// If the waiting-thread is not up and waiting yet,
// we can make sure that it finishes quickly by
// setting the end-time to zero.
m_end_time.tv_sec = 0;
m_end_time.tv_nsec = 0;
// Otherwise it's already up and waiting, and
// we can send a signal on m_condition_var:
pthread_mutex_lock(&m_mutex);
pthread_cond_signal(&m_condition_var);
pthread_mutex_unlock(&m_mutex);
if (pthread_join(m_thread_id, NULL) != 0)
throw default_exception("failed to join thread");
if (pthread_mutex_destroy(&m_mutex) != 0)
throw default_exception("failed to destroy pthread mutex");
if (pthread_cond_destroy(&m_condition_var) != 0)
throw default_exception("failed to destroy pthread condition variable");
if (pthread_attr_destroy(&m_attributes) != 0)
throw default_exception("failed to destroy pthread attributes object");
#elif defined(_LINUX_) || defined(_FREEBSD_)