mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
Merge branch 'master' of https://github.com/z3prover/z3
This commit is contained in:
commit
b632c08fe0
15
scripts/authorization.json
Normal file
15
scripts/authorization.json
Normal file
|
@ -0,0 +1,15 @@
|
|||
{
|
||||
"Version": "1.0.0",
|
||||
"AuthenticationType": "AAD_CERT",
|
||||
"ClientId": "1c614a83-2dbe-4d3c-853b-effaefd4fb20",
|
||||
"AuthCert": {
|
||||
"SubjectName": "1c614a83-2dbe-4d3c-853b-effaefd4fb20.microsoft.com",
|
||||
"StoreLocation": "LocalMachine",
|
||||
"StoreName": "My"
|
||||
},
|
||||
"RequestSigningCert": {
|
||||
"SubjectName": "1c614a83-2dbe-4d3c-853b-effaefd4fb20",
|
||||
"StoreLocation": "LocalMachine",
|
||||
"StoreName": "My"
|
||||
}
|
||||
}
|
|
@ -7,6 +7,7 @@
|
|||
# 3. copy over Microsoft.Z3.dll from suitable distribution
|
||||
# 4. copy nuspec file from packages
|
||||
# 5. call nuget pack
|
||||
# 6. sign package
|
||||
|
||||
import json
|
||||
import os
|
||||
|
@ -22,6 +23,7 @@ import mk_project
|
|||
data = json.loads(urllib.request.urlopen("https://api.github.com/repos/Z3Prover/z3/releases/latest").read().decode())
|
||||
|
||||
version_str = data['tag_name']
|
||||
version_num = version_str[3:]
|
||||
|
||||
print(version_str)
|
||||
|
||||
|
@ -50,7 +52,8 @@ def classify_package(f):
|
|||
ext, dst = os_info[os_name]
|
||||
return os_name, f[:-4], ext, dst
|
||||
return None
|
||||
|
||||
|
||||
|
||||
def unpack():
|
||||
shutil.rmtree("out", ignore_errors=True)
|
||||
# unzip files in packages
|
||||
|
@ -103,17 +106,67 @@ Linux Dependencies:
|
|||
</package>"""
|
||||
|
||||
with open("out/Microsoft.Z3.nuspec", 'w') as f:
|
||||
f.write(contents % version_str[3:])
|
||||
f.write(contents % version_num)
|
||||
|
||||
def create_nuget_package():
|
||||
subprocess.call(["nuget", "pack"], cwd="out")
|
||||
|
||||
nuget_sign_input = """
|
||||
{
|
||||
"Version": "1.0.0",
|
||||
"SignBatches"
|
||||
:
|
||||
[
|
||||
{
|
||||
"SourceLocationType": "UNC",
|
||||
"SourceRootDirectory": "%s",
|
||||
"DestinationLocationType": "UNC",
|
||||
"DestinationRootDirectory": "%s",
|
||||
"SignRequestFiles": [
|
||||
{
|
||||
"CustomerCorrelationId": "42fc9577-af9e-4ac9-995d-1788d8721d17",
|
||||
"SourceLocation": "Microsoft.Z3.%s.nupkg",
|
||||
"DestinationLocation": "Microsoft.Z3.%s.nupkg"
|
||||
}
|
||||
],
|
||||
"SigningInfo": {
|
||||
"Operations": [
|
||||
{
|
||||
"KeyCode" : "CP-401405",
|
||||
"OperationCode" : "NuGetSign",
|
||||
"Parameters" : {},
|
||||
"ToolName" : "sign",
|
||||
"ToolVersion" : "1.0"
|
||||
},
|
||||
{
|
||||
"KeyCode" : "CP-401405",
|
||||
"OperationCode" : "NuGetVerify",
|
||||
"Parameters" : {},
|
||||
"ToolName" : "sign",
|
||||
"ToolVersion" : "1.0"
|
||||
}
|
||||
]
|
||||
}
|
||||
}
|
||||
]
|
||||
}"""
|
||||
|
||||
def sign_nuget_package():
|
||||
package_name = "Microsoft.Z3.%s.nupkg" % version_num
|
||||
input_file = "out/nuget_sign_input.json"
|
||||
output_path = os.path.abspath("out").replace("\\","\\\\")
|
||||
with open(input_file, 'w') as f:
|
||||
f.write(nuget_sign_input % (output_path, output_path, version_num, version_num))
|
||||
subprocess.call(["EsrpClient.exe", "sign", "-a", "authorization.json", "-p", "policy.json", "-i", input_file, "-o", "out\\diagnostics.json"])
|
||||
|
||||
|
||||
def main():
|
||||
mk_dir("packages")
|
||||
download_installs()
|
||||
unpack()
|
||||
create_nuget_spec()
|
||||
create_nuget_package()
|
||||
sign_nuget_package()
|
||||
|
||||
|
||||
main()
|
||||
|
|
8
scripts/policy.json
Normal file
8
scripts/policy.json
Normal file
|
@ -0,0 +1,8 @@
|
|||
{
|
||||
"Version": "1.0.0",
|
||||
"Intent": "ProductRelease",
|
||||
"ContentType": "Binaries",
|
||||
"ContentOrigin": "1stParty",
|
||||
"ProductState": "Next",
|
||||
"Audience": "ExternalBroad"
|
||||
}
|
|
@ -89,7 +89,14 @@ app * arith_decl_plugin::mk_numeral(algebraic_numbers::anum const & val, bool is
|
|||
parameter p(idx, true);
|
||||
SASSERT(p.is_external());
|
||||
func_decl * decl = m_manager->mk_const_decl(m_rootv_sym, m_real_decl, func_decl_info(m_family_id, OP_IRRATIONAL_ALGEBRAIC_NUM, 1, &p));
|
||||
return m_manager->mk_const(decl);
|
||||
app * r = m_manager->mk_const(decl);
|
||||
|
||||
if (log_constant_meaning_prelude(r)) {
|
||||
am().display_root_smt2(m_manager->trace_stream(), val);
|
||||
m_manager->trace_stream() << "\n";
|
||||
}
|
||||
|
||||
return r;
|
||||
}
|
||||
}
|
||||
|
||||
|
@ -415,6 +422,10 @@ app * arith_decl_plugin::mk_numeral(rational const & val, bool is_int) {
|
|||
r = m_manager->mk_const(m_manager->mk_const_decl(m_intv_sym, m_int_decl, func_decl_info(m_family_id, OP_NUM, 2, p)));
|
||||
m_manager->inc_ref(r);
|
||||
m_small_ints.setx(u_val, r, 0);
|
||||
|
||||
if (log_constant_meaning_prelude(r)) {
|
||||
m_manager->trace_stream() << u_val << "\n";
|
||||
}
|
||||
}
|
||||
return r;
|
||||
}
|
||||
|
@ -425,6 +436,10 @@ app * arith_decl_plugin::mk_numeral(rational const & val, bool is_int) {
|
|||
r = m_manager->mk_const(m_manager->mk_const_decl(m_realv_sym, m_real_decl, func_decl_info(m_family_id, OP_NUM, 2, p)));
|
||||
m_manager->inc_ref(r);
|
||||
m_small_reals.setx(u_val, r, 0);
|
||||
|
||||
if (log_constant_meaning_prelude(r)) {
|
||||
m_manager->trace_stream() << u_val << "\n";
|
||||
}
|
||||
}
|
||||
return r;
|
||||
}
|
||||
|
@ -436,7 +451,14 @@ app * arith_decl_plugin::mk_numeral(rational const & val, bool is_int) {
|
|||
decl = m_manager->mk_const_decl(m_intv_sym, m_int_decl, func_decl_info(m_family_id, OP_NUM, 2, p));
|
||||
else
|
||||
decl = m_manager->mk_const_decl(m_realv_sym, m_real_decl, func_decl_info(m_family_id, OP_NUM, 2, p));
|
||||
return m_manager->mk_const(decl);
|
||||
app * r = m_manager->mk_const(decl);
|
||||
|
||||
if (log_constant_meaning_prelude(r)) {
|
||||
val.display_smt2(m_manager->trace_stream());
|
||||
m_manager->trace_stream() << "\n";
|
||||
}
|
||||
|
||||
return r;
|
||||
}
|
||||
|
||||
func_decl * arith_decl_plugin::mk_num_decl(unsigned num_parameters, parameter const * parameters, unsigned arity) {
|
||||
|
|
|
@ -141,7 +141,7 @@ func_decl * array_decl_plugin::mk_map(func_decl* f, unsigned arity, sort* const*
|
|||
std::ostringstream buffer;
|
||||
buffer << "map expects to take as many arguments as the function being mapped, "
|
||||
<< "it was given " << arity << " but expects " << f->get_arity();
|
||||
m_manager->raise_exception(buffer.str().c_str());
|
||||
m_manager->raise_exception(buffer.str());
|
||||
return nullptr;
|
||||
}
|
||||
if (arity == 0) {
|
||||
|
@ -158,14 +158,14 @@ func_decl * array_decl_plugin::mk_map(func_decl* f, unsigned arity, sort* const*
|
|||
if (!is_array_sort(domain[i])) {
|
||||
std::ostringstream buffer;
|
||||
buffer << "map expects an array sort as argument at position " << i;
|
||||
m_manager->raise_exception(buffer.str().c_str());
|
||||
m_manager->raise_exception(buffer.str());
|
||||
return nullptr;
|
||||
}
|
||||
if (get_array_arity(domain[i]) != dom_arity) {
|
||||
std::ostringstream buffer;
|
||||
buffer << "map expects all arguments to have the same array domain, "
|
||||
<< "this is not the case for argument " << i;
|
||||
m_manager->raise_exception(buffer.str().c_str());
|
||||
m_manager->raise_exception(buffer.str());
|
||||
return nullptr;
|
||||
}
|
||||
for (unsigned j = 0; j < dom_arity; ++j) {
|
||||
|
@ -173,7 +173,7 @@ func_decl * array_decl_plugin::mk_map(func_decl* f, unsigned arity, sort* const*
|
|||
std::ostringstream buffer;
|
||||
buffer << "map expects all arguments to have the same array domain, "
|
||||
<< "this is not the case for argument " << i;
|
||||
m_manager->raise_exception(buffer.str().c_str());
|
||||
m_manager->raise_exception(buffer.str());
|
||||
return nullptr;
|
||||
}
|
||||
}
|
||||
|
@ -181,7 +181,7 @@ func_decl * array_decl_plugin::mk_map(func_decl* f, unsigned arity, sort* const*
|
|||
std::ostringstream buffer;
|
||||
buffer << "map expects the argument at position " << i
|
||||
<< " to have the array range the same as the function";
|
||||
m_manager->raise_exception(buffer.str().c_str());
|
||||
m_manager->raise_exception(buffer.str());
|
||||
return nullptr;
|
||||
}
|
||||
}
|
||||
|
@ -244,7 +244,7 @@ func_decl* array_decl_plugin::mk_select(unsigned arity, sort * const * domain) {
|
|||
if (num_parameters != arity) {
|
||||
std::stringstream strm;
|
||||
strm << "select requires " << num_parameters << " arguments, but was provided with " << arity << " arguments";
|
||||
m_manager->raise_exception(strm.str().c_str());
|
||||
m_manager->raise_exception(strm.str());
|
||||
return nullptr;
|
||||
}
|
||||
ptr_buffer<sort> new_domain; // we need this because of coercions.
|
||||
|
@ -256,7 +256,7 @@ func_decl* array_decl_plugin::mk_select(unsigned arity, sort * const * domain) {
|
|||
std::stringstream strm;
|
||||
strm << "domain sort " << sort_ref(domain[i+1], *m_manager) << " and parameter ";
|
||||
strm << parameter_pp(parameters[i], *m_manager) << " do not match";
|
||||
m_manager->raise_exception(strm.str().c_str());
|
||||
m_manager->raise_exception(strm.str());
|
||||
UNREACHABLE();
|
||||
return nullptr;
|
||||
}
|
||||
|
@ -284,7 +284,7 @@ func_decl * array_decl_plugin::mk_store(unsigned arity, sort * const * domain) {
|
|||
std::ostringstream buffer;
|
||||
buffer << "store expects the first argument to be an array taking " << num_parameters+1
|
||||
<< ", instead it was passed " << (arity - 1) << "arguments";
|
||||
m_manager->raise_exception(buffer.str().c_str());
|
||||
m_manager->raise_exception(buffer.str());
|
||||
UNREACHABLE();
|
||||
return nullptr;
|
||||
}
|
||||
|
|
|
@ -28,6 +28,7 @@ Revision History:
|
|||
#include "ast/ast_smt2_pp.h"
|
||||
#include "ast/array_decl_plugin.h"
|
||||
#include "ast/ast_translation.h"
|
||||
#include "util/z3_version.h"
|
||||
|
||||
|
||||
// -----------------------------------
|
||||
|
@ -662,6 +663,23 @@ ast* ast_table::pop_erase() {
|
|||
//
|
||||
// -----------------------------------
|
||||
|
||||
/**
|
||||
\brief Checks wether a log is being generated and, if necessary, adds the beginning of an "[attach-meaning]" line
|
||||
to that log. The theory solver should add some description of the meaning of the term in terms of the theory's
|
||||
internal reasoning to the end of the line and insert a line break.
|
||||
|
||||
\param a the term that should be described.
|
||||
|
||||
\return true if a log is being generated, false otherwise.
|
||||
*/
|
||||
bool decl_plugin::log_constant_meaning_prelude(app * a) {
|
||||
if (m_manager->has_trace_stream()) {
|
||||
m_manager->trace_stream() << "[attach-meaning] #" << a->get_id() << " " << m_manager->get_family_name(m_family_id).str() << " ";
|
||||
return true;
|
||||
}
|
||||
return false;
|
||||
}
|
||||
|
||||
func_decl * decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters,
|
||||
unsigned num_args, expr * const * args, sort * range) {
|
||||
ptr_buffer<sort> sorts;
|
||||
|
@ -1347,6 +1365,7 @@ ast_manager::ast_manager(proof_gen_mode m, char const * trace_file, bool is_form
|
|||
if (trace_file) {
|
||||
m_trace_stream = alloc(std::fstream, trace_file, std::ios_base::out);
|
||||
m_trace_stream_owner = true;
|
||||
*m_trace_stream << "[tool-version] Z3 " << Z3_MAJOR_VERSION << "." << Z3_MINOR_VERSION << "." << Z3_BUILD_NUMBER << "\n";
|
||||
}
|
||||
|
||||
if (!is_format_manager)
|
||||
|
@ -1565,8 +1584,8 @@ void ast_manager::raise_exception(char const * msg) {
|
|||
throw ast_exception(msg);
|
||||
}
|
||||
|
||||
void ast_manager::raise_exception(std::string const& msg) {
|
||||
throw ast_exception(msg.c_str());
|
||||
void ast_manager::raise_exception(std::string && msg) {
|
||||
throw ast_exception(std::move(msg));
|
||||
}
|
||||
|
||||
|
||||
|
@ -2183,7 +2202,14 @@ app * ast_manager::mk_app_core(func_decl * decl, unsigned num_args, expr * const
|
|||
}
|
||||
|
||||
if (m_trace_stream && r == new_node) {
|
||||
*m_trace_stream << "[mk-app] #" << r->get_id() << " ";
|
||||
if (is_proof(r)) {
|
||||
if (decl == mk_func_decl(m_basic_family_id, PR_UNDEF, 0, nullptr, 0, static_cast<expr * const *>(nullptr)))
|
||||
return r;
|
||||
*m_trace_stream << "[mk-proof] #";
|
||||
} else {
|
||||
*m_trace_stream << "[mk-app] #";
|
||||
}
|
||||
*m_trace_stream << r->get_id() << " ";
|
||||
if (r->get_num_args() == 0 && r->get_decl()->get_name() == "int") {
|
||||
ast_ll_pp(*m_trace_stream, *this, r);
|
||||
}
|
||||
|
@ -2329,7 +2355,7 @@ var * ast_manager::mk_var(unsigned idx, sort * s) {
|
|||
var * r = register_node(new_node);
|
||||
|
||||
if (m_trace_stream && r == new_node) {
|
||||
*m_trace_stream << "[mk-var] #" << r->get_id() << "\n";
|
||||
*m_trace_stream << "[mk-var] #" << r->get_id() << " " << idx << "\n";
|
||||
}
|
||||
return r;
|
||||
}
|
||||
|
@ -2458,6 +2484,11 @@ quantifier * ast_manager::mk_quantifier(quantifier_kind k, unsigned num_decls, s
|
|||
|
||||
if (m_trace_stream && r == new_node) {
|
||||
trace_quant(*m_trace_stream, r);
|
||||
*m_trace_stream << "[attach-var-names] #" << r->get_id();
|
||||
for (unsigned i = 0; i < num_decls; ++i) {
|
||||
*m_trace_stream << " (|" << decl_names[num_decls - i - 1].str() << "| ; |" << decl_sorts[num_decls - i -1]->get_name().str() << "|)";
|
||||
}
|
||||
*m_trace_stream << "\n";
|
||||
}
|
||||
|
||||
return r;
|
||||
|
|
|
@ -998,6 +998,17 @@ protected:
|
|||
|
||||
virtual void inherit(decl_plugin* other_p, ast_translation& ) { }
|
||||
|
||||
/**
|
||||
\brief Checks wether a log is being generated and, if necessary, adds the beginning of an "[attach-meaning]" line
|
||||
to that log. The theory solver should add some description of the meaning of the term in terms of the theory's
|
||||
internal reasoning to the end of the line and insert a line break.
|
||||
|
||||
\param a the term that should be described.
|
||||
|
||||
\return true if a log is being generated, false otherwise.
|
||||
*/
|
||||
bool log_constant_meaning_prelude(app * a);
|
||||
|
||||
friend class ast_manager;
|
||||
|
||||
public:
|
||||
|
@ -1563,7 +1574,7 @@ public:
|
|||
|
||||
// Equivalent to throw ast_exception(msg)
|
||||
Z3_NORETURN void raise_exception(char const * msg);
|
||||
Z3_NORETURN void raise_exception(std::string const& s);
|
||||
Z3_NORETURN void raise_exception(std::string && s);
|
||||
|
||||
std::ostream& display(std::ostream& out, parameter const& p);
|
||||
|
||||
|
|
|
@ -951,7 +951,7 @@ void ast_smt_pp::display_smt2(std::ostream& strm, expr* n) {
|
|||
strm << "(set-logic " << m_logic << ")\n";
|
||||
}
|
||||
if (!m_attributes.empty()) {
|
||||
strm << "; " << m_attributes.c_str();
|
||||
strm << "; " << m_attributes;
|
||||
}
|
||||
|
||||
#if 0
|
||||
|
|
|
@ -624,7 +624,7 @@ func_decl * bv_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, p
|
|||
if (m.get_sort(args[i]) != r->get_domain(i)) {
|
||||
std::ostringstream buffer;
|
||||
buffer << "Argument " << mk_pp(args[i], m) << " at position " << i << " does not match declaration " << mk_pp(r, m);
|
||||
m.raise_exception(buffer.str().c_str());
|
||||
m.raise_exception(buffer.str());
|
||||
return nullptr;
|
||||
}
|
||||
}
|
||||
|
@ -868,7 +868,21 @@ app * bv_util::mk_numeral(rational const & val, sort* s) const {
|
|||
|
||||
app * bv_util::mk_numeral(rational const & val, unsigned bv_size) const {
|
||||
parameter p[2] = { parameter(val), parameter(static_cast<int>(bv_size)) };
|
||||
return m_manager.mk_app(get_fid(), OP_BV_NUM, 2, p, 0, nullptr);
|
||||
app * r = m_manager.mk_app(get_fid(), OP_BV_NUM, 2, p, 0, nullptr);
|
||||
|
||||
if (m_plugin->log_constant_meaning_prelude(r)) {
|
||||
if (bv_size % 4 == 0) {
|
||||
m_manager.trace_stream() << "#x";
|
||||
val.display_hex(m_manager.trace_stream(), bv_size);
|
||||
m_manager.trace_stream() << "\n";
|
||||
} else {
|
||||
m_manager.trace_stream() << "#b";
|
||||
val.display_bin(m_manager.trace_stream(), bv_size);
|
||||
m_manager.trace_stream() << "\n";
|
||||
}
|
||||
}
|
||||
|
||||
return r;
|
||||
}
|
||||
|
||||
sort * bv_util::mk_sort(unsigned bv_size) {
|
||||
|
|
|
@ -126,6 +126,7 @@ inline func_decl * get_div0_decl(ast_manager & m, func_decl * decl) {
|
|||
}
|
||||
|
||||
class bv_decl_plugin : public decl_plugin {
|
||||
friend class bv_util;
|
||||
protected:
|
||||
symbol m_bv_sym;
|
||||
symbol m_concat_sym;
|
||||
|
@ -432,7 +433,53 @@ public:
|
|||
app * mk_bvsmul_no_udfl(expr* m, expr* n) { return m_manager.mk_app(get_fid(), OP_BSMUL_NO_UDFL, n, m); }
|
||||
app * mk_bvumul_no_ovfl(expr* m, expr* n) { return m_manager.mk_app(get_fid(), OP_BUMUL_NO_OVFL, n, m); }
|
||||
|
||||
app * mk_bv(unsigned n, expr* const* es) { return m_manager.mk_app(get_fid(), OP_MKBV, n, es); }
|
||||
private:
|
||||
void log_bv_from_exprs(app * r, unsigned n, expr* const* es) {
|
||||
if (m_manager.has_trace_stream()) {
|
||||
for (unsigned i = 0; i < n; ++i) {
|
||||
if (!m_manager.is_true(es[i]) && !m_manager.is_false(es[i]))
|
||||
return;
|
||||
}
|
||||
|
||||
if (m_plugin->log_constant_meaning_prelude(r)) {
|
||||
if (n % 4 == 0) {
|
||||
m_manager.trace_stream() << " #x";
|
||||
|
||||
m_manager.trace_stream() << std::hex;
|
||||
uint8_t hexDigit = 0;
|
||||
unsigned curLength = (4 - n % 4) % 4;
|
||||
for (unsigned i = 0; i < n; ++i) {
|
||||
hexDigit <<= 1;
|
||||
++curLength;
|
||||
if (m_manager.is_true(es[i])) {
|
||||
hexDigit |= 1;
|
||||
}
|
||||
if (curLength == 4) {
|
||||
m_manager.trace_stream() << hexDigit;
|
||||
hexDigit = 0;
|
||||
}
|
||||
}
|
||||
m_manager.trace_stream() << std::dec;
|
||||
} else {
|
||||
m_manager.trace_stream() << " #b";
|
||||
for (unsigned i = 0; i < n; ++i) {
|
||||
m_manager.trace_stream() << (m_manager.is_true(es[i]) ? 1 : 0);
|
||||
}
|
||||
}
|
||||
|
||||
m_manager.trace_stream() << ")\n";
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
public:
|
||||
app * mk_bv(unsigned n, expr* const* es) {
|
||||
app * r = m_manager.mk_app(get_fid(), OP_MKBV, n, es);
|
||||
|
||||
log_bv_from_exprs(r, n, es);
|
||||
|
||||
return r;
|
||||
}
|
||||
|
||||
};
|
||||
|
||||
|
|
|
@ -342,7 +342,7 @@ namespace datatype {
|
|||
std::ostringstream buffer;
|
||||
buffer << "second argument to field update should be " << mk_ismt2_pp(rng, m)
|
||||
<< " instead of " << mk_ismt2_pp(domain[1], m);
|
||||
m.raise_exception(buffer.str().c_str());
|
||||
m.raise_exception(buffer.str());
|
||||
return nullptr;
|
||||
}
|
||||
range = domain[0];
|
||||
|
@ -453,6 +453,48 @@ namespace datatype {
|
|||
}
|
||||
}
|
||||
|
||||
void plugin::log_axiom_definitions(symbol const& s, sort * new_sort) {
|
||||
symbol const& family_name = m_manager->get_family_name(get_family_id());
|
||||
for (constructor const* c : *m_defs[s]) {
|
||||
func_decl_ref f = c->instantiate(new_sort);
|
||||
const unsigned num_args = f->get_arity();
|
||||
if (num_args == 0) continue;
|
||||
for (unsigned i = 0; i < num_args; ++i) {
|
||||
m_manager->trace_stream() << "[mk-var] " << family_name << "#" << m_id_counter << " " << i << "\n";
|
||||
++m_id_counter;
|
||||
}
|
||||
const unsigned constructor_id = m_id_counter;
|
||||
m_manager->trace_stream() << "[mk-app] " << family_name << "#" << constructor_id << " " << f->get_name();
|
||||
for (unsigned i = 0; i < num_args; ++i) {
|
||||
m_manager->trace_stream() << " " << family_name << "#" << constructor_id - num_args + i;
|
||||
}
|
||||
m_manager->trace_stream() << "\n";
|
||||
++m_id_counter;
|
||||
m_manager->trace_stream() << "[mk-app] " << family_name << "#" << m_id_counter << " pattern " << family_name << "#" << constructor_id << "\n";
|
||||
++m_id_counter;
|
||||
m_axiom_bases.insert(f->get_name(), constructor_id + 4);
|
||||
std::ostringstream var_sorts;
|
||||
for (accessor const* a : *c) {
|
||||
var_sorts << " (;" << a->range()->get_name() << ")";
|
||||
}
|
||||
std::string var_description = var_sorts.str();
|
||||
unsigned i = 0;
|
||||
for (accessor const* a : *c) {
|
||||
func_decl_ref acc = a->instantiate(new_sort);
|
||||
m_manager->trace_stream() << "[mk-app] " << family_name << "#" << m_id_counter << " " << acc->get_name() << " " << family_name << "#" << constructor_id << "\n";
|
||||
++m_id_counter;
|
||||
m_manager->trace_stream() << "[mk-app] " << family_name << "#" << m_id_counter << " = " << family_name << "#" << constructor_id - num_args + i
|
||||
<< " " << family_name << "#" << m_id_counter - 1 << "\n";
|
||||
++m_id_counter;
|
||||
m_manager->trace_stream() << "[mk-quant] " << family_name << "#" << m_id_counter << " constructor_accessor_axiom " << family_name << "#" << constructor_id + 1
|
||||
<< " " << family_name << "#" << m_id_counter - 1 << "\n";
|
||||
m_manager->trace_stream() << "[attach-var-names] " << family_name << "#" << m_id_counter << var_description << "\n";
|
||||
++m_id_counter;
|
||||
++i;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
bool plugin::mk_datatypes(unsigned num_datatypes, def * const * datatypes, unsigned num_params, sort* const* sort_params, sort_ref_vector & new_sorts) {
|
||||
begin_def_block();
|
||||
for (unsigned i = 0; i < num_datatypes; ++i) {
|
||||
|
@ -470,6 +512,9 @@ namespace datatype {
|
|||
sort_ref_vector ps(*m_manager);
|
||||
for (symbol const& s : m_def_block) {
|
||||
new_sorts.push_back(m_defs[s]->instantiate(ps));
|
||||
if (m_manager->has_trace_stream()) {
|
||||
log_axiom_definitions(s, new_sorts.back());
|
||||
}
|
||||
}
|
||||
return true;
|
||||
}
|
||||
|
|
|
@ -206,13 +206,17 @@ namespace datatype {
|
|||
class plugin : public decl_plugin {
|
||||
mutable scoped_ptr<util> m_util;
|
||||
map<symbol, def*, symbol_hash_proc, symbol_eq_proc> m_defs;
|
||||
map<symbol, unsigned, symbol_hash_proc, symbol_eq_proc> m_axiom_bases;
|
||||
unsigned m_id_counter;
|
||||
svector<symbol> m_def_block;
|
||||
unsigned m_class_id;
|
||||
|
||||
void inherit(decl_plugin* other_p, ast_translation& tr) override;
|
||||
|
||||
void log_axiom_definitions(symbol const& s, sort * new_sort);
|
||||
|
||||
public:
|
||||
plugin(): m_class_id(0) {}
|
||||
plugin(): m_id_counter(0), m_class_id(0) {}
|
||||
~plugin() override;
|
||||
|
||||
void finalize() override;
|
||||
|
@ -247,6 +251,7 @@ namespace datatype {
|
|||
def const& get_def(sort* s) const { return *(m_defs[datatype_name(s)]); }
|
||||
def& get_def(symbol const& s) { return *(m_defs[s]); }
|
||||
bool is_declared(sort* s) const { return m_defs.contains(datatype_name(s)); }
|
||||
unsigned get_axiom_base_id(symbol const& s) { return m_axiom_bases[s]; }
|
||||
util & u() const;
|
||||
|
||||
private:
|
||||
|
|
|
@ -54,7 +54,7 @@ namespace datalog {
|
|||
}
|
||||
std::ostringstream buffer;
|
||||
buffer << msg << ", value is not within bound " << low << " <= " << val << " <= " << up;
|
||||
m_manager->raise_exception(buffer.str().c_str());
|
||||
m_manager->raise_exception(buffer.str());
|
||||
return false;
|
||||
}
|
||||
|
||||
|
@ -676,7 +676,7 @@ namespace datalog {
|
|||
}
|
||||
std::stringstream strm;
|
||||
strm << "sort '" << mk_pp(s, m) << "' is not recognized as a sort that contains numeric values.\nUse Bool, BitVec, Int, Real, or a Finite domain sort";
|
||||
m.raise_exception(strm.str().c_str());
|
||||
m.raise_exception(strm.str());
|
||||
return nullptr;
|
||||
}
|
||||
|
||||
|
|
|
@ -92,7 +92,14 @@ func_decl * fpa_decl_plugin::mk_numeral_decl(mpf const & v) {
|
|||
}
|
||||
|
||||
app * fpa_decl_plugin::mk_numeral(mpf const & v) {
|
||||
return m_manager->mk_const(mk_numeral_decl(v));
|
||||
app * r = m_manager->mk_const(mk_numeral_decl(v));
|
||||
|
||||
if (log_constant_meaning_prelude(r)) {
|
||||
m_fm.display_smt2(m_manager->trace_stream(), v, false);
|
||||
m_manager->trace_stream() << "\n";
|
||||
}
|
||||
|
||||
return r;
|
||||
}
|
||||
|
||||
bool fpa_decl_plugin::is_numeral(expr * n, mpf & val) {
|
||||
|
|
|
@ -86,7 +86,7 @@ struct enum2bv_rewriter::imp {
|
|||
void throw_non_fd(expr* e) {
|
||||
std::stringstream strm;
|
||||
strm << "unable to handle nested data-type expression " << mk_pp(e, m);
|
||||
throw rewriter_exception(strm.str().c_str());
|
||||
throw rewriter_exception(strm.str());
|
||||
}
|
||||
|
||||
void check_for_fd(unsigned n, expr* const* args) {
|
||||
|
|
|
@ -46,7 +46,7 @@ inline br_status unsigned2br_status(unsigned u) {
|
|||
|
||||
class rewriter_exception : public default_exception {
|
||||
public:
|
||||
rewriter_exception(char const * msg):default_exception(msg) {}
|
||||
rewriter_exception(std::string && msg) : default_exception(std::move(msg)) {}
|
||||
};
|
||||
|
||||
#endif
|
||||
|
|
|
@ -562,6 +562,29 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
|
|||
br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) {
|
||||
result_pr = nullptr;
|
||||
br_status st = reduce_app_core(f, num, args, result);
|
||||
|
||||
if (st != BR_FAILED && m().has_trace_stream()) {
|
||||
family_id fid = f->get_family_id();
|
||||
if (fid == m_b_rw.get_fid()) {
|
||||
decl_kind k = f->get_decl_kind();
|
||||
if (k == OP_EQ) {
|
||||
SASSERT(num == 2);
|
||||
fid = m().get_sort(args[0])->get_family_id();
|
||||
}
|
||||
else if (k == OP_ITE) {
|
||||
SASSERT(num == 3);
|
||||
fid = m().get_sort(args[1])->get_family_id();
|
||||
}
|
||||
}
|
||||
app_ref tmp(m());
|
||||
tmp = m().mk_app(f, num, args);
|
||||
m().trace_stream() << "[inst-discovered] theory-solving " << static_cast<void *>(nullptr) << " " << m().get_family_name(fid) << "# ; #" << tmp->get_id() << "\n";
|
||||
tmp = m().mk_eq(tmp, result);
|
||||
m().trace_stream() << "[instance] " << static_cast<void *>(nullptr) << " #" << tmp->get_id() << "\n";
|
||||
m().trace_stream() << "[attach-enode] #" << tmp->get_id() << " 0\n";
|
||||
m().trace_stream() << "[end-of-instance]\n";
|
||||
}
|
||||
|
||||
if (st != BR_DONE && st != BR_FAILED) {
|
||||
CTRACE("th_rewriter_step", st != BR_FAILED,
|
||||
tout << f->get_name() << "\n";
|
||||
|
|
|
@ -400,7 +400,7 @@ void seq_decl_plugin::match_right_assoc(psig& sig, unsigned dsz, sort *const* do
|
|||
std::ostringstream strm;
|
||||
strm << "Unexpected number of arguments to '" << sig.m_name << "' ";
|
||||
strm << "at least one argument expected " << dsz << " given";
|
||||
m.raise_exception(strm.str().c_str());
|
||||
m.raise_exception(strm.str());
|
||||
}
|
||||
bool is_match = true;
|
||||
for (unsigned i = 0; is_match && i < dsz; ++i) {
|
||||
|
@ -420,7 +420,7 @@ void seq_decl_plugin::match_right_assoc(psig& sig, unsigned dsz, sort *const* do
|
|||
if (range) {
|
||||
strm << " and range: " << mk_pp(range, m);
|
||||
}
|
||||
m.raise_exception(strm.str().c_str());
|
||||
m.raise_exception(strm.str());
|
||||
}
|
||||
range_out = apply_binding(binding, sig.m_range);
|
||||
SASSERT(range_out);
|
||||
|
@ -434,7 +434,7 @@ void seq_decl_plugin::match(psig& sig, unsigned dsz, sort *const* dom, sort* ran
|
|||
std::ostringstream strm;
|
||||
strm << "Unexpected number of arguments to '" << sig.m_name << "' ";
|
||||
strm << sig.m_dom.size() << " arguments expected " << dsz << " given";
|
||||
m.raise_exception(strm.str().c_str());
|
||||
m.raise_exception(strm.str());
|
||||
}
|
||||
bool is_match = true;
|
||||
for (unsigned i = 0; is_match && i < dsz; ++i) {
|
||||
|
@ -459,13 +459,13 @@ void seq_decl_plugin::match(psig& sig, unsigned dsz, sort *const* dom, sort* ran
|
|||
strm << mk_pp(sig.m_dom[i].get(), m) << " ";
|
||||
}
|
||||
|
||||
m.raise_exception(strm.str().c_str());
|
||||
m.raise_exception(strm.str());
|
||||
}
|
||||
if (!range && dsz == 0) {
|
||||
std::ostringstream strm;
|
||||
strm << "Sort of polymorphic function '" << sig.m_name << "' ";
|
||||
strm << "is ambiguous. Function takes no arguments and sort of range has not been constrained";
|
||||
m.raise_exception(strm.str().c_str());
|
||||
m.raise_exception(strm.str());
|
||||
}
|
||||
range_out = apply_binding(m_binding, sig.m_range);
|
||||
SASSERT(range_out);
|
||||
|
|
|
@ -797,7 +797,7 @@ void cmd_context::insert(symbol const & s, func_decl * f) {
|
|||
msg += " '";
|
||||
msg += s.str();
|
||||
msg += "' (with the given signature) already declared";
|
||||
throw cmd_exception(msg.c_str());
|
||||
throw cmd_exception(std::move(msg));
|
||||
}
|
||||
if (s != f->get_name()) {
|
||||
TRACE("func_decl_alias", tout << "adding alias for: " << f->get_name() << ", alias: " << s << "\n";);
|
||||
|
@ -1142,7 +1142,7 @@ void cmd_context::mk_app(symbol const & s, unsigned num_args, expr * const * arg
|
|||
for (unsigned i = 0; i < fs.get_num_entries(); ++i) {
|
||||
buffer << "\ndeclared: " << mk_pp(fs.get_entry(i), m()) << " ";
|
||||
}
|
||||
throw cmd_exception(buffer.str().c_str());
|
||||
throw cmd_exception(buffer.str());
|
||||
}
|
||||
if (well_sorted_check_enabled())
|
||||
m().check_sort(f, num_args, args);
|
||||
|
|
|
@ -482,7 +482,7 @@ namespace smt2 {
|
|||
if (context[0]) msg += ": ";
|
||||
msg += "unknown sort '";
|
||||
msg += id.str() + "'";
|
||||
throw parser_exception(msg.c_str());
|
||||
throw parser_exception(std::move(msg));
|
||||
}
|
||||
|
||||
void consume_sexpr() {
|
||||
|
@ -1633,7 +1633,7 @@ namespace smt2 {
|
|||
void unknown_var_const_name(symbol id) {
|
||||
std::string msg = "unknown constant/variable '";
|
||||
msg += id.str() + "'";
|
||||
throw parser_exception(msg.c_str());
|
||||
throw parser_exception(std::move(msg));
|
||||
}
|
||||
|
||||
rational m_last_bv_numeral; // for bv, bvbin, bvhex
|
||||
|
@ -2431,7 +2431,7 @@ namespace smt2 {
|
|||
buffer << "invalid function definition, sort mismatch. Expcected "
|
||||
<< mk_pp(f->get_range(), m()) << " but function body has sort "
|
||||
<< mk_pp(m().get_sort(body), m());
|
||||
throw parser_exception(buffer.str().c_str());
|
||||
throw parser_exception(buffer.str());
|
||||
}
|
||||
m_ctx.insert_rec_fun(f, bindings, ids, body);
|
||||
}
|
||||
|
|
|
@ -694,7 +694,8 @@ namespace eq {
|
|||
if (m.proofs_enabled() && r != q) {
|
||||
pr = m.mk_transitivity(pr, curr_pr);
|
||||
}
|
||||
} while (q != r && is_quantifier(r));
|
||||
}
|
||||
while (q != r && is_quantifier(r));
|
||||
|
||||
m_new_exprs.reset();
|
||||
}
|
||||
|
@ -2441,7 +2442,7 @@ class qe_lite_tactic : public tactic {
|
|||
continue;
|
||||
new_f = f;
|
||||
m_qe(new_f, new_pr);
|
||||
if (produce_proofs) {
|
||||
if (new_pr) {
|
||||
expr* fact = m.get_fact(new_pr);
|
||||
if (to_app(fact)->get_arg(0) != to_app(fact)->get_arg(1)) {
|
||||
new_pr = m.mk_modus_ponens(g->pr(i), new_pr);
|
||||
|
|
|
@ -59,6 +59,7 @@ namespace smt {
|
|||
m_b_internalized_stack(m),
|
||||
m_e_internalized_stack(m),
|
||||
m_final_check_idx(0),
|
||||
m_is_auxiliary(false),
|
||||
m_cg_table(m),
|
||||
m_dyn_ack_manager(*this, p),
|
||||
m_is_diseq_tmp(nullptr),
|
||||
|
@ -238,6 +239,7 @@ namespace smt {
|
|||
|
||||
context * context::mk_fresh(symbol const * l, smt_params * p, params_ref const& pa) {
|
||||
context * new_ctx = alloc(context, m_manager, p ? *p : m_fparams, pa);
|
||||
new_ctx->m_is_auxiliary = true;
|
||||
new_ctx->set_logic(l == nullptr ? m_setup.get_logic() : *l);
|
||||
copy_plugins(*this, *new_ctx);
|
||||
return new_ctx;
|
||||
|
@ -1941,7 +1943,7 @@ namespace smt {
|
|||
*/
|
||||
void context::push_scope() {
|
||||
|
||||
if (m_manager.has_trace_stream())
|
||||
if (m_manager.has_trace_stream() && !m_is_auxiliary)
|
||||
m_manager.trace_stream() << "[push] " << m_scope_lvl << "\n";
|
||||
|
||||
m_scope_lvl++;
|
||||
|
@ -2392,7 +2394,7 @@ namespace smt {
|
|||
unsigned context::pop_scope_core(unsigned num_scopes) {
|
||||
|
||||
try {
|
||||
if (m_manager.has_trace_stream())
|
||||
if (m_manager.has_trace_stream() && !m_is_auxiliary)
|
||||
m_manager.trace_stream() << "[pop] " << num_scopes << " " << m_scope_lvl << "\n";
|
||||
|
||||
TRACE("context", tout << "backtracking: " << num_scopes << " from " << m_scope_lvl << "\n";);
|
||||
|
@ -3331,7 +3333,7 @@ namespace smt {
|
|||
Return true if succeeded.
|
||||
*/
|
||||
bool context::check_preamble(bool reset_cancel) {
|
||||
if (m_manager.has_trace_stream())
|
||||
if (m_manager.has_trace_stream() && !m_is_auxiliary)
|
||||
m_manager.trace_stream() << "[begin-check] " << m_scope_lvl << "\n";
|
||||
|
||||
if (memory::above_high_watermark()) {
|
||||
|
@ -3946,7 +3948,7 @@ namespace smt {
|
|||
<< mk_pp(bool_var2expr(l.var()), m_manager) << "\n";
|
||||
});
|
||||
|
||||
if (m_manager.has_trace_stream()) {
|
||||
if (m_manager.has_trace_stream() && !m_is_auxiliary) {
|
||||
m_manager.trace_stream() << "[conflict] ";
|
||||
display_literals(m_manager.trace_stream(), num_lits, lits);
|
||||
m_manager.trace_stream() << "\n";
|
||||
|
|
|
@ -106,6 +106,8 @@ namespace smt {
|
|||
|
||||
unsigned m_final_check_idx; // circular counter used for implementing fairness
|
||||
|
||||
bool m_is_auxiliary; // used to prevent unwanted information from being logged.
|
||||
|
||||
// -----------------------------------
|
||||
//
|
||||
// Equality & Uninterpreted functions
|
||||
|
|
|
@ -1019,15 +1019,7 @@ namespace smt {
|
|||
sort * s = term->get_decl()->get_range();
|
||||
theory * th = m_theories.get_plugin(s->get_family_id());
|
||||
if (th) {
|
||||
if (m_manager.has_trace_stream()) {
|
||||
m_manager.trace_stream() << "[theory-constraints] " << m_manager.get_family_name(s->get_family_id()) << "\n";
|
||||
}
|
||||
|
||||
th->apply_sort_cnstr(e, s);
|
||||
|
||||
if (m_manager.has_trace_stream()) {
|
||||
m_manager.trace_stream() << "[end-theory-constraints]\n";
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
|
|
|
@ -32,6 +32,98 @@ namespace smt {
|
|||
|
||||
quantifier_manager_plugin * mk_default_plugin();
|
||||
|
||||
void log_single_justification(std::ostream & out, enode *en, obj_hashtable<enode> &visited, context &ctx, ast_manager &m);
|
||||
|
||||
/**
|
||||
\brief Ensures that all relevant proof steps to explain why the enode is equal to the root of its
|
||||
equivalence class are in the log and up-to-date.
|
||||
*/
|
||||
void quantifier_manager::log_justification_to_root(std::ostream & out, enode *en, obj_hashtable<enode> &visited, context &ctx, ast_manager &m) {
|
||||
enode *root = en->get_root();
|
||||
for (enode *it = en; it != root; it = it->get_trans_justification().m_target) {
|
||||
if (visited.find(it) == visited.end()) visited.insert(it);
|
||||
else break;
|
||||
|
||||
if (!it->m_proof_is_logged) {
|
||||
log_single_justification(out, it, visited, ctx, m);
|
||||
it->m_proof_is_logged = true;
|
||||
} else if (it->get_trans_justification().m_justification.get_kind() == smt::eq_justification::kind::CONGRUENCE) {
|
||||
|
||||
// When the justification of an argument changes m_proof_is_logged is not reset => We need to check if the proofs of all arguments are logged.
|
||||
const unsigned num_args = it->get_num_args();
|
||||
enode *target = it->get_trans_justification().m_target;
|
||||
|
||||
for (unsigned i = 0; i < num_args; ++i) {
|
||||
log_justification_to_root(out, it->get_arg(i), visited, ctx, m);
|
||||
log_justification_to_root(out, target->get_arg(i), visited, ctx, m);
|
||||
}
|
||||
it->m_proof_is_logged = true;
|
||||
}
|
||||
}
|
||||
if (!root->m_proof_is_logged) {
|
||||
out << "[eq-expl] #" << root->get_owner_id() << " root\n";
|
||||
root->m_proof_is_logged = true;
|
||||
}
|
||||
}
|
||||
|
||||
/**
|
||||
\brief Logs a single equality explanation step and, if necessary, recursively calls log_justification_to_root to log
|
||||
equalities needed by the step (e.g. argument equalities for congruence steps).
|
||||
*/
|
||||
void log_single_justification(std::ostream & out, enode *en, obj_hashtable<enode> &visited, context &ctx, ast_manager &m) {
|
||||
smt::literal lit;
|
||||
unsigned num_args;
|
||||
enode *target = en->get_trans_justification().m_target;
|
||||
theory_id th_id;
|
||||
|
||||
switch (en->get_trans_justification().m_justification.get_kind()) {
|
||||
case smt::eq_justification::kind::EQUATION:
|
||||
lit = en->get_trans_justification().m_justification.get_literal();
|
||||
out << "[eq-expl] #" << en->get_owner_id() << " lit #" << ctx.bool_var2expr(lit.var())->get_id() << " ; #" << target->get_owner_id() << "\n";
|
||||
break;
|
||||
case smt::eq_justification::kind::AXIOM:
|
||||
out << "[eq-expl] #" << en->get_owner_id() << " ax ; #" << target->get_owner_id() << "\n";
|
||||
break;
|
||||
case smt::eq_justification::kind::CONGRUENCE:
|
||||
if (!en->get_trans_justification().m_justification.used_commutativity()) {
|
||||
num_args = en->get_num_args();
|
||||
|
||||
for (unsigned i = 0; i < num_args; ++i) {
|
||||
quantifier_manager::log_justification_to_root(out, en->get_arg(i), visited, ctx, m);
|
||||
quantifier_manager::log_justification_to_root(out, target->get_arg(i), visited, ctx, m);
|
||||
}
|
||||
|
||||
out << "[eq-expl] #" << en->get_owner_id() << " cg";
|
||||
for (unsigned i = 0; i < num_args; ++i) {
|
||||
out << " (#" << en->get_arg(i)->get_owner_id() << " #" << target->get_arg(i)->get_owner_id() << ")";
|
||||
}
|
||||
out << " ; #" << target->get_owner_id() << "\n";
|
||||
|
||||
break;
|
||||
} else {
|
||||
|
||||
// The e-graph only supports commutativity for binary functions
|
||||
out << "[eq-expl] #" << en->get_owner_id()
|
||||
<< " cg (#" << en->get_arg(0)->get_owner_id() << " #" << target->get_arg(1)->get_owner_id()
|
||||
<< ") (#" << en->get_arg(1)->get_owner_id() << " #" << target->get_arg(0)->get_owner_id()
|
||||
<< ") ; #" << target->get_owner_id() << "\n";
|
||||
break;
|
||||
}
|
||||
case smt::eq_justification::kind::JUSTIFICATION:
|
||||
th_id = en->get_trans_justification().m_justification.get_justification()->get_from_theory();
|
||||
if (th_id != null_theory_id) {
|
||||
symbol const theory = m.get_family_name(th_id);
|
||||
out << "[eq-expl] #" << en->get_owner_id() << " th " << theory.str() << " ; #" << target->get_owner_id() << "\n";
|
||||
} else {
|
||||
out << "[eq-expl] #" << en->get_owner_id() << " unknown ; #" << target->get_owner_id() << "\n";
|
||||
}
|
||||
break;
|
||||
default:
|
||||
out << "[eq-expl] #" << en->get_owner_id() << " unknown ; #" << target->get_owner_id() << "\n";
|
||||
break;
|
||||
}
|
||||
}
|
||||
|
||||
struct quantifier_manager::imp {
|
||||
quantifier_manager & m_wrapper;
|
||||
context & m_context;
|
||||
|
@ -81,7 +173,7 @@ namespace smt {
|
|||
if (num_instances > 0) {
|
||||
out << "[quantifier_instances] ";
|
||||
out.width(10);
|
||||
out << q->get_qid().str().c_str() << " : ";
|
||||
out << q->get_qid().str() << " : ";
|
||||
out.width(6);
|
||||
out << num_instances << " : ";
|
||||
out.width(3);
|
||||
|
@ -105,138 +197,58 @@ namespace smt {
|
|||
return m_plugin->is_shared(n);
|
||||
}
|
||||
|
||||
/**
|
||||
\brief Ensures that all relevant proof steps to explain why the enode is equal to the root of its
|
||||
equivalence class are in the log and up-to-date.
|
||||
*/
|
||||
void log_justification_to_root(std::ostream & out, enode *en, obj_hashtable<enode> &visited) {
|
||||
enode* root = en->get_root();
|
||||
for (enode *it = en; it != root && !visited.contains(it); it = it->get_trans_justification().m_target) {
|
||||
|
||||
visited.insert(it);
|
||||
|
||||
if (!it->m_proof_is_logged) {
|
||||
log_single_justification(out, it, visited);
|
||||
it->m_proof_is_logged = true;
|
||||
}
|
||||
else if (it->get_trans_justification().m_justification.get_kind() == smt::eq_justification::kind::CONGRUENCE) {
|
||||
|
||||
// When the justification of an argument changes m_proof_is_logged
|
||||
// is not reset => We need to check if the proofs of all arguments are logged.
|
||||
const unsigned num_args = it->get_num_args();
|
||||
enode *target = it->get_trans_justification().m_target;
|
||||
|
||||
for (unsigned i = 0; i < num_args; ++i) {
|
||||
log_justification_to_root(out, it->get_arg(i), visited);
|
||||
log_justification_to_root(out, target->get_arg(i), visited);
|
||||
}
|
||||
SASSERT(it->m_proof_is_logged);
|
||||
}
|
||||
}
|
||||
if (!root->m_proof_is_logged) {
|
||||
out << "[eq-expl] #" << root->get_owner_id() << " root\n";
|
||||
root->m_proof_is_logged = true;
|
||||
}
|
||||
}
|
||||
|
||||
/**
|
||||
\brief Logs a single equality explanation step and, if necessary, recursively calls log_justification_to_root to log
|
||||
equalities needed by the step (e.g. argument equalities for congruence steps).
|
||||
*/
|
||||
void log_single_justification(std::ostream & out, enode *en, obj_hashtable<enode> &visited) {
|
||||
smt::literal lit;
|
||||
unsigned num_args;
|
||||
enode *target = en->get_trans_justification().m_target;
|
||||
theory_id th_id;
|
||||
|
||||
switch (en->get_trans_justification().m_justification.get_kind()) {
|
||||
case smt::eq_justification::kind::EQUATION:
|
||||
lit = en->get_trans_justification().m_justification.get_literal();
|
||||
out << "[eq-expl] #" << en->get_owner_id() << " lit #" << m_context.bool_var2expr(lit.var())->get_id() << " ; #" << target->get_owner_id() << "\n";
|
||||
break;
|
||||
case smt::eq_justification::kind::AXIOM:
|
||||
out << "[eq-expl] #" << en->get_owner_id() << " ax ; #" << target->get_owner_id() << "\n";
|
||||
break;
|
||||
case smt::eq_justification::kind::CONGRUENCE:
|
||||
if (!en->get_trans_justification().m_justification.used_commutativity()) {
|
||||
num_args = en->get_num_args();
|
||||
|
||||
for (unsigned i = 0; i < num_args; ++i) {
|
||||
log_justification_to_root(out, en->get_arg(i), visited);
|
||||
log_justification_to_root(out, target->get_arg(i), visited);
|
||||
}
|
||||
|
||||
out << "[eq-expl] #" << en->get_owner_id() << " cg";
|
||||
for (unsigned i = 0; i < num_args; ++i) {
|
||||
out << " (#" << en->get_arg(i)->get_owner_id() << " #" << target->get_arg(i)->get_owner_id() << ")";
|
||||
}
|
||||
out << " ; #" << target->get_owner_id() << "\n";
|
||||
|
||||
break;
|
||||
} else {
|
||||
out << "[eq-expl] #" << en->get_owner_id() << " nyi ; #" << target->get_owner_id() << "\n";
|
||||
break;
|
||||
}
|
||||
case smt::eq_justification::kind::JUSTIFICATION:
|
||||
th_id = en->get_trans_justification().m_justification.get_justification()->get_from_theory();
|
||||
if (th_id != null_theory_id) {
|
||||
symbol const theory = m().get_family_name(th_id);
|
||||
out << "[eq-expl] #" << en->get_owner_id() << " th " << theory.str() << " ; #" << target->get_owner_id() << "\n";
|
||||
} else {
|
||||
out << "[eq-expl] #" << en->get_owner_id() << " unknown ; #" << target->get_owner_id() << "\n";
|
||||
}
|
||||
break;
|
||||
default:
|
||||
out << "[eq-expl] #" << en->get_owner_id() << " unknown ; #" << target->get_owner_id() << "\n";
|
||||
break;
|
||||
}
|
||||
}
|
||||
|
||||
void log_add_instance(
|
||||
fingerprint* f,
|
||||
quantifier * q, app * pat,
|
||||
unsigned num_bindings,
|
||||
enode * const * bindings,
|
||||
vector<std::tuple<enode *, enode *>> & used_enodes) {
|
||||
fingerprint* f,
|
||||
quantifier * q, app * pat,
|
||||
unsigned num_bindings,
|
||||
enode * const * bindings,
|
||||
vector<std::tuple<enode *, enode *>> & used_enodes) {
|
||||
|
||||
std::ostream & out = trace_stream();
|
||||
|
||||
obj_hashtable<enode> visited;
|
||||
|
||||
// In the term produced by the quantifier instantiation the root of
|
||||
// the equivalence class of the terms bound to the quantified variables
|
||||
// is used. We need to make sure that all of these equalities appear in the log.
|
||||
for (unsigned i = 0; i < num_bindings; ++i) {
|
||||
log_justification_to_root(out, bindings[i], visited);
|
||||
}
|
||||
|
||||
for (auto n : used_enodes) {
|
||||
enode *orig = std::get<0>(n);
|
||||
enode *substituted = std::get<1>(n);
|
||||
if (orig != nullptr) {
|
||||
log_justification_to_root(out, orig, visited);
|
||||
log_justification_to_root(out, substituted, visited);
|
||||
if (pat == nullptr) {
|
||||
trace_stream() << "[inst-discovered] MBQI " << static_cast<void*>(f) << " #" << q->get_id();
|
||||
for (unsigned i = 0; i < num_bindings; ++i) {
|
||||
trace_stream() << " #" << bindings[num_bindings - i - 1]->get_owner_id();
|
||||
}
|
||||
}
|
||||
|
||||
// At this point all relevant equalities for the match are logged.
|
||||
out << "[new-match] " << static_cast<void*>(f) << " #" << q->get_id() << " #" << pat->get_id();
|
||||
for (unsigned i = 0; i < num_bindings; i++) {
|
||||
// I don't want to use mk_pp because it creates expressions for pretty printing.
|
||||
// This nasty side-effect may change the behavior of Z3.
|
||||
out << " #" << bindings[i]->get_owner_id();
|
||||
}
|
||||
out << " ;";
|
||||
for (auto n : used_enodes) {
|
||||
enode *orig = std::get<0>(n);
|
||||
enode *substituted = std::get<1>(n);
|
||||
if (orig == nullptr)
|
||||
out << " #" << substituted->get_owner_id();
|
||||
else {
|
||||
out << " (#" << orig->get_owner_id() << " #" << substituted->get_owner_id() << ")";
|
||||
trace_stream() << "\n";
|
||||
} else {
|
||||
std::ostream & out = trace_stream();
|
||||
|
||||
obj_hashtable<enode> already_visited;
|
||||
|
||||
// In the term produced by the quantifier instantiation the root of the equivalence class of the terms bound to the quantified variables
|
||||
// is used. We need to make sure that all of these equalities appear in the log.
|
||||
for (unsigned i = 0; i < num_bindings; ++i) {
|
||||
log_justification_to_root(out, bindings[i], already_visited, m_context, m());
|
||||
}
|
||||
|
||||
for (auto n : used_enodes) {
|
||||
enode *orig = std::get<0>(n);
|
||||
enode *substituted = std::get<1>(n);
|
||||
if (orig != nullptr) {
|
||||
log_justification_to_root(out, orig, already_visited, m_context, m());
|
||||
log_justification_to_root(out, substituted, already_visited, m_context, m());
|
||||
}
|
||||
}
|
||||
|
||||
// At this point all relevant equalities for the match are logged.
|
||||
out << "[new-match] " << static_cast<void*>(f) << " #" << q->get_id() << " #" << pat->get_id();
|
||||
for (unsigned i = 0; i < num_bindings; i++) {
|
||||
// I don't want to use mk_pp because it creates expressions for pretty printing.
|
||||
// This nasty side-effect may change the behavior of Z3.
|
||||
out << " #" << bindings[num_bindings - i - 1]->get_owner_id();
|
||||
}
|
||||
out << " ;";
|
||||
for (auto n : used_enodes) {
|
||||
enode *orig = std::get<0>(n);
|
||||
enode *substituted = std::get<1>(n);
|
||||
if (orig == nullptr)
|
||||
out << " #" << substituted->get_owner_id();
|
||||
else {
|
||||
out << " (#" << orig->get_owner_id() << " #" << substituted->get_owner_id() << ")";
|
||||
}
|
||||
}
|
||||
out << "\n";
|
||||
}
|
||||
out << "\n";
|
||||
}
|
||||
|
||||
bool add_instance(quantifier * q, app * pat,
|
||||
|
|
|
@ -52,6 +52,8 @@ namespace smt {
|
|||
quantifier_stat * get_stat(quantifier * q) const;
|
||||
unsigned get_generation(quantifier * q) const;
|
||||
|
||||
static void log_justification_to_root(std::ostream & log, enode *en, obj_hashtable<enode> &already_visited, context &ctx, ast_manager &m);
|
||||
|
||||
bool add_instance(quantifier * q, app * pat,
|
||||
unsigned num_bindings,
|
||||
enode * const * bindings,
|
||||
|
|
|
@ -20,6 +20,7 @@ Revision History:
|
|||
#define SMT_THEORY_H_
|
||||
|
||||
#include "smt/smt_enode.h"
|
||||
#include "smt/smt_quantifier.h"
|
||||
#include "util/obj_hashtable.h"
|
||||
#include "util/statistics.h"
|
||||
#include<typeinfo>
|
||||
|
@ -358,6 +359,67 @@ namespace smt {
|
|||
|
||||
std::ostream& display_var_flat_def(std::ostream & out, theory_var v) const { return display_flat_app(out, get_enode(v)->get_owner()); }
|
||||
|
||||
protected:
|
||||
void log_axiom_instantiation(app * r, unsigned axiom_id = UINT_MAX, unsigned num_bindings = 0, app * const * bindings = nullptr, unsigned pattern_id = UINT_MAX, const vector<std::tuple<enode *, enode *>> & used_enodes = vector<std::tuple<enode *, enode*>>()) {
|
||||
ast_manager & m = get_manager();
|
||||
symbol const & family_name = m.get_family_name(get_family_id());
|
||||
if (pattern_id == UINT_MAX) {
|
||||
m.trace_stream() << "[inst-discovered] theory-solving " << static_cast<void *>(nullptr) << " " << family_name << "#";
|
||||
if (axiom_id != UINT_MAX)
|
||||
m.trace_stream() << axiom_id;
|
||||
for (unsigned i = 0; i < num_bindings; ++i) {
|
||||
m.trace_stream() << " #" << bindings[i]->get_id();
|
||||
}
|
||||
if (used_enodes.size() > 0) {
|
||||
m.trace_stream() << " ;";
|
||||
for (auto n : used_enodes) {
|
||||
enode *orig = std::get<0>(n);
|
||||
enode *substituted = std::get<1>(n);
|
||||
SASSERT(orig == nullptr);
|
||||
m.trace_stream() << " #" << substituted->get_owner_id();
|
||||
}
|
||||
}
|
||||
} else {
|
||||
SASSERT(axiom_id != UINT_MAX);
|
||||
obj_hashtable<enode> already_visited;
|
||||
for (auto n : used_enodes) {
|
||||
enode *orig = std::get<0>(n);
|
||||
enode *substituted = std::get<1>(n);
|
||||
if (orig != nullptr) {
|
||||
quantifier_manager::log_justification_to_root(m.trace_stream(), orig, already_visited, get_context(), get_manager());
|
||||
quantifier_manager::log_justification_to_root(m.trace_stream(), substituted, already_visited, get_context(), get_manager());
|
||||
}
|
||||
}
|
||||
m.trace_stream() << "[new-match] " << static_cast<void *>(nullptr) << " " << family_name << "#" << axiom_id << " " << family_name << "#" << pattern_id;
|
||||
for (unsigned i = 0; i < num_bindings; ++i) {
|
||||
m.trace_stream() << " #" << bindings[i]->get_id();
|
||||
}
|
||||
m.trace_stream() << " ;";
|
||||
for (auto n : used_enodes) {
|
||||
enode *orig = std::get<0>(n);
|
||||
enode *substituted = std::get<1>(n);
|
||||
if (orig == nullptr) {
|
||||
m.trace_stream() << " #" << substituted->get_owner_id();
|
||||
} else {
|
||||
m.trace_stream() << " (#" << orig->get_owner_id() << " #" << substituted->get_owner_id() << ")";
|
||||
}
|
||||
}
|
||||
}
|
||||
m.trace_stream() << "\n";
|
||||
m.trace_stream() << "[instance] " << static_cast<void *>(nullptr) << " #" << r->get_id() << "\n";
|
||||
}
|
||||
|
||||
void log_axiom_instantiation(expr * r, unsigned axiom_id = UINT_MAX, unsigned num_bindings = 0, app * const * bindings = nullptr, unsigned pattern_id = UINT_MAX, const vector<std::tuple<enode *, enode *>> & used_enodes = vector<std::tuple<enode *, enode*>>()) { log_axiom_instantiation(to_app(r), axiom_id, num_bindings, bindings, pattern_id, used_enodes); }
|
||||
|
||||
void log_axiom_instantiation(app * r, unsigned num_blamed_enodes, enode ** blamed_enodes) {
|
||||
vector<std::tuple<enode *, enode *>> used_enodes;
|
||||
for (unsigned i = 0; i < num_blamed_enodes; ++i) {
|
||||
used_enodes.push_back(std::make_tuple(nullptr, blamed_enodes[i]));
|
||||
}
|
||||
log_axiom_instantiation(r, UINT_MAX, 0, nullptr, UINT_MAX, used_enodes);
|
||||
}
|
||||
|
||||
public:
|
||||
/**
|
||||
\brief Assume eqs between variable that are equal with respect to the given table.
|
||||
Table is a hashtable indexed by the variable value.
|
||||
|
|
|
@ -1239,6 +1239,10 @@ namespace smt {
|
|||
farkas.add(abs(pa.get_rational()), to_app(tmp));
|
||||
}
|
||||
tmp = farkas.get();
|
||||
if (m.has_trace_stream()) {
|
||||
log_axiom_instantiation(tmp);
|
||||
m.trace_stream() << "[end-of-instance]\n";
|
||||
}
|
||||
// IF_VERBOSE(1, verbose_stream() << "Farkas result: " << tmp << "\n";);
|
||||
atom* a = get_bv2a(m_bound_watch);
|
||||
SASSERT(a);
|
||||
|
|
|
@ -447,7 +447,14 @@ namespace smt {
|
|||
tout << l_ante << "\n" << l_conseq << "\n";);
|
||||
|
||||
// literal lits[2] = {l_ante, l_conseq};
|
||||
if (m.has_trace_stream()) {
|
||||
app_ref body(m);
|
||||
body = m.mk_or(ante, conseq);
|
||||
log_axiom_instantiation(body);
|
||||
}
|
||||
mk_clause(l_ante, l_conseq, 0, nullptr);
|
||||
if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
|
||||
|
||||
if (ctx.relevancy()) {
|
||||
if (l_ante == false_literal) {
|
||||
ctx.mark_as_relevant(l_conseq);
|
||||
|
@ -528,7 +535,9 @@ namespace smt {
|
|||
expr_ref mod_j(m);
|
||||
while(j < k) {
|
||||
mod_j = m.mk_eq(mod, m_util.mk_numeral(j, true));
|
||||
if (m.has_trace_stream()) log_axiom_instantiation(mod_j);
|
||||
ctx.internalize(mod_j, false);
|
||||
if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
|
||||
literal lit(ctx.get_literal(mod_j));
|
||||
lits.push_back(lit);
|
||||
ctx.mark_as_relevant(lit);
|
||||
|
|
|
@ -199,6 +199,7 @@ namespace smt {
|
|||
void theory_arith<Ext>::branch_infeasible_int_var(theory_var v) {
|
||||
SASSERT(is_int(v));
|
||||
SASSERT(!get_value(v).is_int());
|
||||
ast_manager & m = get_manager();
|
||||
m_stats.m_branches++;
|
||||
numeral k = ceil(get_value(v));
|
||||
rational _k = k.to_rational();
|
||||
|
@ -206,13 +207,19 @@ namespace smt {
|
|||
display_var(tout, v);
|
||||
tout << "k = " << k << ", _k = "<< _k << std::endl;
|
||||
);
|
||||
expr_ref bound(get_manager());
|
||||
expr_ref bound(m);
|
||||
expr* e = get_enode(v)->get_owner();
|
||||
bound = m_util.mk_ge(e, m_util.mk_numeral(_k, m_util.is_int(e)));
|
||||
TRACE("arith_int", tout << mk_bounded_pp(bound, get_manager()) << "\n";);
|
||||
if (m.has_trace_stream()) {
|
||||
app_ref body(m);
|
||||
body = m.mk_or(to_app(bound), m.mk_not(to_app(bound)));
|
||||
log_axiom_instantiation(body);
|
||||
}
|
||||
TRACE("arith_int", tout << mk_bounded_pp(bound, m) << "\n";);
|
||||
context & ctx = get_context();
|
||||
ctx.internalize(bound, true);
|
||||
ctx.mark_as_relevant(bound.get());
|
||||
if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
|
||||
}
|
||||
|
||||
|
||||
|
@ -365,6 +372,11 @@ namespace smt {
|
|||
mk_polynomial_ge(pol.size(), pol.c_ptr(), unsat_row[0]+rational(1), p2);
|
||||
|
||||
context& ctx = get_context();
|
||||
if (get_manager().has_trace_stream()) {
|
||||
app_ref body(get_manager());
|
||||
body = get_manager().mk_or(p1, p2);
|
||||
log_axiom_instantiation(body);
|
||||
}
|
||||
ctx.internalize(p1, false);
|
||||
ctx.internalize(p2, false);
|
||||
literal l1(ctx.get_literal(p1)), l2(ctx.get_literal(p2));
|
||||
|
@ -372,6 +384,7 @@ namespace smt {
|
|||
ctx.mark_as_relevant(p2.get());
|
||||
|
||||
ctx.mk_th_axiom(get_id(), l1, l2);
|
||||
if (get_manager().has_trace_stream()) get_manager().trace_stream() << "[end-of-instance]\n";
|
||||
|
||||
TRACE("arith_int",
|
||||
tout << "cut: (or " << mk_pp(p1, get_manager()) << " " << mk_pp(p2, get_manager()) << ")\n";
|
||||
|
@ -400,7 +413,9 @@ namespace smt {
|
|||
bool _is_int = m_util.is_int(e);
|
||||
expr * bound = m_util.mk_ge(e, m_util.mk_numeral(rational::zero(), _is_int));
|
||||
context & ctx = get_context();
|
||||
if (get_manager().has_trace_stream()) log_axiom_instantiation(bound);
|
||||
ctx.internalize(bound, true);
|
||||
if (get_manager().has_trace_stream()) get_manager().trace_stream() << "[end-of-instance]\n";
|
||||
ctx.mark_as_relevant(bound);
|
||||
result = true;
|
||||
}
|
||||
|
@ -646,7 +661,9 @@ namespace smt {
|
|||
TRACE("gomory_cut", tout << "new cut:\n" << bound << "\n"; ante.display(tout););
|
||||
literal l = null_literal;
|
||||
context & ctx = get_context();
|
||||
if (get_manager().has_trace_stream()) log_axiom_instantiation(bound);
|
||||
ctx.internalize(bound, true);
|
||||
if (get_manager().has_trace_stream()) get_manager().trace_stream() << "[end-of-instance]\n";
|
||||
l = ctx.get_literal(bound);
|
||||
ctx.mark_as_relevant(l);
|
||||
dump_lemmas(l, ante);
|
||||
|
|
|
@ -789,7 +789,14 @@ namespace smt {
|
|||
bound = m_util.mk_eq(var2expr(v), m_util.mk_numeral(rational(0), true));
|
||||
TRACE("non_linear", tout << "new bound:\n" << mk_pp(bound, get_manager()) << "\n";);
|
||||
context & ctx = get_context();
|
||||
ast_manager & m = get_manager();
|
||||
if (m.has_trace_stream()) {
|
||||
app_ref body(m);
|
||||
body = m.mk_or(bound, m.mk_not(bound));
|
||||
log_axiom_instantiation(body);
|
||||
}
|
||||
ctx.internalize(bound, true);
|
||||
if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
|
||||
ctx.mark_as_relevant(bound);
|
||||
literal l = ctx.get_literal(bound);
|
||||
SASSERT(!l.sign());
|
||||
|
|
|
@ -111,7 +111,9 @@ namespace smt {
|
|||
if (m.proofs_enabled()) {
|
||||
literal l(mk_eq(sel, val, true));
|
||||
ctx.mark_as_relevant(l);
|
||||
if (m.has_trace_stream()) log_axiom_instantiation(ctx.bool_var2expr(l.var()));
|
||||
assert_axiom(l);
|
||||
if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
|
||||
}
|
||||
else {
|
||||
TRACE("mk_var_bug", tout << "mk_sel: " << sel->get_id() << "\n";);
|
||||
|
@ -189,7 +191,13 @@ namespace smt {
|
|||
TRACE("array_map_bug", tout << "axiom2:\n";
|
||||
tout << mk_ismt2_pp(idx1->get_owner(), m) << "\n=\n" << mk_ismt2_pp(idx2->get_owner(), m);
|
||||
tout << "\nimplies\n" << mk_ismt2_pp(conseq_expr, m) << "\n";);
|
||||
if (m.has_trace_stream()) {
|
||||
app_ref body(m);
|
||||
body = m.mk_or(ctx.bool_var2expr(ante.var()), conseq_expr);
|
||||
log_axiom_instantiation(body);
|
||||
}
|
||||
assert_axiom(ante, conseq);
|
||||
if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
|
||||
}
|
||||
}
|
||||
|
||||
|
@ -331,7 +339,13 @@ namespace smt {
|
|||
literal sel1_eq_sel2 = mk_eq(sel1, sel2, true);
|
||||
ctx.mark_as_relevant(n1_eq_n2);
|
||||
ctx.mark_as_relevant(sel1_eq_sel2);
|
||||
if (m.has_trace_stream()) {
|
||||
app_ref body(m);
|
||||
body = m.mk_implies(m.mk_not(ctx.bool_var2expr(n1_eq_n2.var())), m.mk_not(ctx.bool_var2expr(sel1_eq_sel2.var())));
|
||||
log_axiom_instantiation(body);
|
||||
}
|
||||
assert_axiom(n1_eq_n2, ~sel1_eq_sel2);
|
||||
if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
|
||||
}
|
||||
|
||||
bool theory_array_base::can_propagate() {
|
||||
|
|
|
@ -781,8 +781,10 @@ namespace smt {
|
|||
else {
|
||||
m_eqs.insert(v1, v2, true);
|
||||
literal eq(mk_eq(v1, v2, true));
|
||||
if (get_manager().has_trace_stream()) log_axiom_instantiation(get_context().bool_var2expr(eq.var()));
|
||||
get_context().mark_as_relevant(eq);
|
||||
assert_axiom(eq);
|
||||
if (get_manager().has_trace_stream()) get_manager().trace_stream() << "[end-of-instance]\n";
|
||||
|
||||
// m_eqsv.push_back(eq);
|
||||
return true;
|
||||
|
|
|
@ -253,9 +253,16 @@ namespace smt {
|
|||
enode * e2 = get_enode(v2);
|
||||
literal l = ~(mk_eq(e1->get_owner(), e2->get_owner(), true));
|
||||
context & ctx = get_context();
|
||||
ast_manager & m = get_manager();
|
||||
expr * eq = ctx.bool_var2expr(l.var());
|
||||
if (m.has_trace_stream()) {
|
||||
app_ref body(m);
|
||||
body = m.mk_implies(m.mk_eq(mk_bit2bool(get_enode(v1)->get_owner(), idx), m.mk_not(mk_bit2bool(get_enode(v2)->get_owner(), idx))), m.mk_not(eq));
|
||||
log_axiom_instantiation(body);
|
||||
}
|
||||
ctx.mk_th_axiom(get_id(), 1, &l);
|
||||
if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
|
||||
if (ctx.relevancy()) {
|
||||
expr * eq = ctx.bool_var2expr(l.var());
|
||||
relevancy_eh * eh = ctx.mk_relevancy_eh(pair_relevancy_eh(e1->get_owner(), e2->get_owner(), eq));
|
||||
ctx.add_relevancy_eh(e1->get_owner(), eh);
|
||||
ctx.add_relevancy_eh(e2->get_owner(), eh);
|
||||
|
@ -469,11 +476,17 @@ namespace smt {
|
|||
e1 = mk_bit2bool(o1, i);
|
||||
e2 = mk_bit2bool(o2, i);
|
||||
literal eq = mk_eq(e1, e2, true);
|
||||
if (m.has_trace_stream()) {
|
||||
app_ref body(m);
|
||||
body = m.mk_implies(m.mk_not(ctx.bool_var2expr(eq.var())), m.mk_not(ctx.bool_var2expr(oeq.var())));
|
||||
log_axiom_instantiation(body);
|
||||
}
|
||||
ctx.mk_th_axiom(get_id(), l1, ~l2, ~eq);
|
||||
ctx.mk_th_axiom(get_id(), ~l1, l2, ~eq);
|
||||
ctx.mk_th_axiom(get_id(), l1, l2, eq);
|
||||
ctx.mk_th_axiom(get_id(), ~l1, ~l2, eq);
|
||||
ctx.mk_th_axiom(get_id(), eq, ~oeq);
|
||||
if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
|
||||
eqs.push_back(~eq);
|
||||
}
|
||||
eqs.push_back(oeq);
|
||||
|
@ -641,7 +654,9 @@ namespace smt {
|
|||
);
|
||||
|
||||
ctx.mark_as_relevant(l);
|
||||
if (m.has_trace_stream()) log_axiom_instantiation(ctx.bool_var2expr(l.var()));
|
||||
ctx.mk_th_axiom(get_id(), 1, &l);
|
||||
if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
|
||||
}
|
||||
|
||||
void theory_bv::internalize_int2bv(app* n) {
|
||||
|
@ -684,7 +699,9 @@ namespace smt {
|
|||
|
||||
literal l(mk_eq(lhs, rhs, false));
|
||||
ctx.mark_as_relevant(l);
|
||||
if (m.has_trace_stream()) log_axiom_instantiation(ctx.bool_var2expr(l.var()));
|
||||
ctx.mk_th_axiom(get_id(), 1, &l);
|
||||
if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
|
||||
|
||||
TRACE("bv",
|
||||
tout << mk_pp(lhs, m) << " == \n";
|
||||
|
@ -705,7 +722,9 @@ namespace smt {
|
|||
TRACE("bv", tout << mk_pp(lhs, m) << " == " << mk_pp(rhs, m) << "\n";);
|
||||
l = literal(mk_eq(lhs, rhs, false));
|
||||
ctx.mark_as_relevant(l);
|
||||
if (m.has_trace_stream()) log_axiom_instantiation(ctx.bool_var2expr(l.var()));
|
||||
ctx.mk_th_axiom(get_id(), 1, &l);
|
||||
if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
|
||||
|
||||
}
|
||||
}
|
||||
|
@ -1200,8 +1219,10 @@ namespace smt {
|
|||
#endif
|
||||
|
||||
literal_vector & lits = m_tmp_literals;
|
||||
expr_ref_vector exprs(m);
|
||||
lits.reset();
|
||||
lits.push_back(mk_eq(get_enode(v1)->get_owner(), get_enode(v2)->get_owner(), true));
|
||||
literal eq = mk_eq(get_enode(v1)->get_owner(), get_enode(v2)->get_owner(), true);
|
||||
lits.push_back(eq);
|
||||
it1 = bits1.begin();
|
||||
it2 = bits2.begin();
|
||||
for (; it1 != end1; ++it1, ++it2) {
|
||||
|
@ -1212,9 +1233,16 @@ namespace smt {
|
|||
ctx.internalize(diff, true);
|
||||
literal arg = ctx.get_literal(diff);
|
||||
lits.push_back(arg);
|
||||
exprs.push_back(diff);
|
||||
}
|
||||
m_stats.m_num_diseq_dynamic++;
|
||||
if (m.has_trace_stream()) {
|
||||
app_ref body(m);
|
||||
body = m.mk_implies(m.mk_not(ctx.bool_var2expr(eq.var())), m.mk_or(exprs.size(), exprs.c_ptr()));
|
||||
log_axiom_instantiation(body);
|
||||
}
|
||||
ctx.mk_th_axiom(get_id(), lits.size(), lits.c_ptr());
|
||||
if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
|
||||
}
|
||||
|
||||
void theory_bv::assign_eh(bool_var v, bool is_true) {
|
||||
|
@ -1306,6 +1334,7 @@ namespace smt {
|
|||
|
||||
m_stats.m_num_bit2core++;
|
||||
context & ctx = get_context();
|
||||
ast_manager & m = get_manager();
|
||||
SASSERT(ctx.get_assignment(antecedent) == l_true);
|
||||
SASSERT(m_bits[v2][idx].var() == consequent.var());
|
||||
SASSERT(consequent.var() != antecedent.var());
|
||||
|
@ -1322,8 +1351,15 @@ namespace smt {
|
|||
literal_vector lits;
|
||||
lits.push_back(~consequent);
|
||||
lits.push_back(antecedent);
|
||||
lits.push_back(~mk_eq(get_enode(v1)->get_owner(), get_enode(v2)->get_owner(), false));
|
||||
literal eq = mk_eq(get_enode(v1)->get_owner(), get_enode(v2)->get_owner(), false);
|
||||
lits.push_back(~eq);
|
||||
if (m.has_trace_stream()) {
|
||||
app_ref body(m);
|
||||
body = m.mk_implies(ctx.bool_var2expr(eq.var()), m.mk_implies(ctx.bool_var2expr(consequent.var()), ctx.bool_var2expr(antecedent.var())));
|
||||
log_axiom_instantiation(body);
|
||||
}
|
||||
ctx.mk_th_axiom(get_id(), lits.size(), lits.c_ptr());
|
||||
if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
|
||||
|
||||
if (m_wpos[v2] == idx)
|
||||
find_wpos(v2);
|
||||
|
|
|
@ -140,7 +140,16 @@ namespace smt {
|
|||
args.push_back(acc);
|
||||
}
|
||||
expr * mk = m.mk_app(c, args.size(), args.c_ptr());
|
||||
if (m.has_trace_stream()) {
|
||||
app_ref body(m);
|
||||
body = m.mk_eq(n->get_owner(), mk);
|
||||
if (antecedent != null_literal) {
|
||||
body = m.mk_implies(get_context().bool_var2expr(antecedent.var()), body);
|
||||
}
|
||||
log_axiom_instantiation(body, 1, &n);
|
||||
}
|
||||
assert_eq_axiom(n, mk, antecedent);
|
||||
if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
|
||||
}
|
||||
|
||||
/**
|
||||
|
@ -157,11 +166,24 @@ namespace smt {
|
|||
func_decl * d = n->get_decl();
|
||||
ptr_vector<func_decl> const & accessors = *m_util.get_constructor_accessors(d);
|
||||
SASSERT(n->get_num_args() == accessors.size());
|
||||
app_ref_vector bindings(m);
|
||||
vector<std::tuple<enode *, enode *>> used_enodes;
|
||||
used_enodes.push_back(std::make_tuple(nullptr, n));
|
||||
for (unsigned i = 0; i < n->get_num_args(); ++i) {
|
||||
bindings.push_back(n->get_arg(i)->get_owner());
|
||||
}
|
||||
unsigned base_id = get_manager().has_trace_stream() && accessors.size() > 0 ? m_util.get_plugin()->get_axiom_base_id(d->get_name()) : 0;
|
||||
unsigned i = 0;
|
||||
for (func_decl * acc : accessors) {
|
||||
app * acc_app = m.mk_app(acc, n->get_owner());
|
||||
enode * arg = n->get_arg(i);
|
||||
if (m.has_trace_stream()) {
|
||||
app_ref body(m);
|
||||
body = m.mk_eq(arg->get_owner(), acc_app);
|
||||
log_axiom_instantiation(body, base_id + 3*i, bindings.size(), bindings.c_ptr(), base_id - 3, used_enodes);
|
||||
}
|
||||
assert_eq_axiom(arg, acc_app, null_literal);
|
||||
if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
|
||||
++i;
|
||||
}
|
||||
}
|
||||
|
@ -218,10 +240,20 @@ namespace smt {
|
|||
arg = ctx.get_enode(acc_app);
|
||||
}
|
||||
app * acc_own = m.mk_app(acc1, own);
|
||||
if (m.has_trace_stream()) {
|
||||
app_ref body(m);
|
||||
body = m.mk_implies(rec_app, m.mk_eq(arg->get_owner(), acc_own));
|
||||
log_axiom_instantiation(body, 1, &n);
|
||||
}
|
||||
assert_eq_axiom(arg, acc_own, is_con);
|
||||
if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
|
||||
}
|
||||
// update_field is identity if 'n' is not created by a matching constructor.
|
||||
app_ref imp(m);
|
||||
imp = m.mk_implies(m.mk_not(rec_app), m.mk_eq(n->get_owner(), arg1));
|
||||
if (m.has_trace_stream()) log_axiom_instantiation(imp, 1, &n);
|
||||
assert_eq_axiom(n, arg1, ~is_con);
|
||||
if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
|
||||
}
|
||||
|
||||
theory_var theory_datatype::mk_var(enode * n) {
|
||||
|
|
|
@ -598,7 +598,9 @@ void theory_diff_logic<Ext>::new_edge(dl_var src, dl_var dst, unsigned num_edges
|
|||
le = m_util.mk_le(m_util.mk_add(n2,n1), n3);
|
||||
le = get_manager().mk_not(le);
|
||||
}
|
||||
if (get_manager().has_trace_stream())log_axiom_instantiation(le);
|
||||
ctx.internalize(le, false);
|
||||
if (get_manager().has_trace_stream()) get_manager().trace_stream() << "[end-of-instance]\n";
|
||||
ctx.mark_as_relevant(le.get());
|
||||
literal lit(ctx.get_literal(le));
|
||||
bool_var bv = lit.var();
|
||||
|
@ -1007,6 +1009,11 @@ void theory_diff_logic<Ext>::new_eq_or_diseq(bool is_eq, theory_var v1, theory_v
|
|||
t2 = m_util.mk_numeral(k, m.get_sort(s2.get()));
|
||||
// t1 - s1 = k
|
||||
eq = m.mk_eq(s2.get(), t2.get());
|
||||
if (m.has_trace_stream()) {
|
||||
app_ref body(m);
|
||||
body = m.mk_eq(m.mk_eq(m_util.mk_add(s1, t2), t1), eq);
|
||||
log_axiom_instantiation(body);
|
||||
}
|
||||
|
||||
TRACE("diff_logic",
|
||||
tout << v1 << " .. " << v2 << "\n";
|
||||
|
@ -1015,6 +1022,8 @@ void theory_diff_logic<Ext>::new_eq_or_diseq(bool is_eq, theory_var v1, theory_v
|
|||
if (!internalize_atom(eq.get(), false)) {
|
||||
UNREACHABLE();
|
||||
}
|
||||
|
||||
if (m.has_trace_stream()) get_manager().trace_stream() << "[end-of-instance]\n";
|
||||
|
||||
literal l(ctx.get_literal(eq.get()));
|
||||
if (!is_eq) {
|
||||
|
|
|
@ -256,6 +256,11 @@ namespace smt {
|
|||
lt = u().mk_lt(x,y);
|
||||
le = b().mk_ule(m().mk_app(r,y),m().mk_app(r,x));
|
||||
context& ctx = get_context();
|
||||
if (m().has_trace_stream()) {
|
||||
app_ref body(m());
|
||||
body = m().mk_eq(lt, le);
|
||||
log_axiom_instantiation(body);
|
||||
}
|
||||
ctx.internalize(lt, false);
|
||||
ctx.internalize(le, false);
|
||||
literal lit1(ctx.get_literal(lt));
|
||||
|
@ -266,12 +271,15 @@ namespace smt {
|
|||
literal lits2[2] = { ~lit1, ~lit2 };
|
||||
ctx.mk_th_axiom(get_id(), 2, lits1);
|
||||
ctx.mk_th_axiom(get_id(), 2, lits2);
|
||||
if (m().has_trace_stream()) m().trace_stream() << "[end-of-instance]\n";
|
||||
}
|
||||
|
||||
void assert_cnstr(expr* e) {
|
||||
TRACE("theory_dl", tout << mk_pp(e, m()) << "\n";);
|
||||
context& ctx = get_context();
|
||||
if (m().has_trace_stream()) log_axiom_instantiation(e);
|
||||
ctx.internalize(e, false);
|
||||
if (m().has_trace_stream()) m().trace_stream() << "[end-of-instance]\n";
|
||||
literal lit(ctx.get_literal(e));
|
||||
ctx.mark_as_relevant(lit);
|
||||
ctx.mk_th_axiom(get_id(), 1, &lit);
|
||||
|
|
|
@ -409,7 +409,9 @@ namespace smt {
|
|||
if (get_manager().is_true(e)) return;
|
||||
TRACE("t_fpa_detail", tout << "asserting " << mk_ismt2_pp(e, get_manager()) << "\n";);
|
||||
context & ctx = get_context();
|
||||
if (get_manager().has_trace_stream()) log_axiom_instantiation(e);
|
||||
ctx.internalize(e, false);
|
||||
if (get_manager().has_trace_stream()) get_manager().trace_stream() << "[end-of-instance]\n";
|
||||
literal lit(ctx.get_literal(e));
|
||||
ctx.mark_as_relevant(lit);
|
||||
ctx.mk_th_axiom(get_id(), 1, &lit);
|
||||
|
|
|
@ -305,6 +305,13 @@ namespace smt {
|
|||
|
||||
literal end_ge_lo = mk_ge(ji.m_end, clb);
|
||||
// Initialization ensures that satisfiable states have completion time below end.
|
||||
ast_manager& m = get_manager();
|
||||
if (m.has_trace_stream()) {
|
||||
app_ref body(m);
|
||||
body = m.mk_implies(m.mk_and(m.mk_eq(eq.first->get_owner(), eq.second->get_owner()), ctx.bool_var2expr(start_ge_lo.var())), ctx.bool_var2expr(end_ge_lo.var()));
|
||||
log_axiom_instantiation(body);
|
||||
m.trace_stream() << "[end-of-instance]\n";
|
||||
}
|
||||
region& r = ctx.get_region();
|
||||
ctx.assign(end_ge_lo,
|
||||
ctx.mk_justification(
|
||||
|
@ -379,6 +386,13 @@ namespace smt {
|
|||
lits.push_back(mk_eq_lit(end_e->get_owner(), rhs));
|
||||
context& ctx = get_context();
|
||||
ctx.mk_clause(lits.size(), lits.c_ptr(), nullptr, CLS_AUX_LEMMA, nullptr);
|
||||
ast_manager& m = get_manager();
|
||||
if (m.has_trace_stream()) {
|
||||
app_ref body(m);
|
||||
body = m.mk_implies(m.mk_and(ctx.bool_var2expr(lits[0].var()), ctx.bool_var2expr(lits[1].var()), ctx.bool_var2expr(lits[2].var())), ctx.bool_var2expr(lits[3].var()));
|
||||
log_axiom_instantiation(body);
|
||||
m.trace_stream() << "[end-of-instance]\n";
|
||||
}
|
||||
return true;
|
||||
}
|
||||
|
||||
|
@ -736,7 +750,9 @@ namespace smt {
|
|||
|
||||
// start(j) <= end(j)
|
||||
lit = mk_le(ji.m_start, ji.m_end);
|
||||
if (m.has_trace_stream()) log_axiom_instantiation(ctx.bool_var2expr(lit.var()));
|
||||
ctx.mk_th_axiom(get_id(), 1, &lit);
|
||||
if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
|
||||
|
||||
time_t start_lb = std::numeric_limits<time_t>::max();
|
||||
time_t runtime_lb = std::numeric_limits<time_t>::max();
|
||||
|
@ -779,11 +795,15 @@ namespace smt {
|
|||
|
||||
// start(j) >= start_lb
|
||||
lit = mk_ge(ji.m_start, start_lb);
|
||||
if (m.has_trace_stream()) log_axiom_instantiation(ctx.bool_var2expr(lit.var()));
|
||||
ctx.mk_th_axiom(get_id(), 1, &lit);
|
||||
if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
|
||||
|
||||
// end(j) <= end_ub
|
||||
lit = mk_le(ji.m_end, end_ub);
|
||||
if (m.has_trace_stream()) log_axiom_instantiation(ctx.bool_var2expr(lit.var()));
|
||||
ctx.mk_th_axiom(get_id(), 1, &lit);
|
||||
if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
|
||||
|
||||
// start(j) + runtime_lb <= end(j)
|
||||
// end(j) <= start(j) + runtime_ub
|
||||
|
@ -799,7 +819,14 @@ namespace smt {
|
|||
#if 0
|
||||
job_info const& ji = m_jobs[j];
|
||||
literal l2 = mk_le(ji.m_end, jr.m_finite_capacity_end);
|
||||
get_context().mk_th_axiom(get_id(), ~eq, l2);
|
||||
context& ctx = get_context();
|
||||
if (m.has_trace_stream()) {
|
||||
app_ref body(m);
|
||||
body = m.mk_implies(ctx.bool_var2expr(eq.var()), ctx.bool_var2expr(l2.var()));
|
||||
log_axiom_instantiation(body);
|
||||
}
|
||||
ctx.mk_th_axiom(get_id(), ~eq, l2);
|
||||
if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
|
||||
#endif
|
||||
}
|
||||
|
||||
|
@ -808,11 +835,24 @@ namespace smt {
|
|||
context& ctx = get_context();
|
||||
time_t t;
|
||||
if (lst(j, r, t)) {
|
||||
ctx.mk_th_axiom(get_id(), ~eq, mk_le(m_jobs[j].m_start, t));
|
||||
literal le = mk_le(m_jobs[j].m_start, t);
|
||||
if (m.has_trace_stream()) {
|
||||
app_ref body(m);
|
||||
body = m.mk_implies(ctx.bool_var2expr(eq.var()), ctx.bool_var2expr(le.var()));
|
||||
log_axiom_instantiation(body);
|
||||
}
|
||||
ctx.mk_th_axiom(get_id(), ~eq, le);
|
||||
if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
|
||||
}
|
||||
else {
|
||||
eq.neg();
|
||||
if (m.has_trace_stream()) {
|
||||
app_ref body(m);
|
||||
body = m.mk_not(ctx.bool_var2expr(eq.var()));
|
||||
log_axiom_instantiation(body);
|
||||
}
|
||||
ctx.mk_th_axiom(get_id(), 1, &eq);
|
||||
if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
|
||||
}
|
||||
}
|
||||
|
||||
|
@ -823,7 +863,14 @@ namespace smt {
|
|||
if (!first_available(jr, m_resources[r], idx)) return;
|
||||
vector<res_available>& available = m_resources[r].m_available;
|
||||
literal l2 = mk_ge(m_jobs[j].m_start, available[idx].m_start);
|
||||
get_context().mk_th_axiom(get_id(), ~eq, l2);
|
||||
context& ctx = get_context();
|
||||
if (m.has_trace_stream()) {
|
||||
app_ref body(m);
|
||||
body = m.mk_implies(ctx.bool_var2expr(eq.var()), ctx.bool_var2expr(l2.var()));
|
||||
log_axiom_instantiation(body);
|
||||
}
|
||||
ctx.mk_th_axiom(get_id(), ~eq, l2);
|
||||
if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
|
||||
}
|
||||
|
||||
// resource(j) = r => start(j) <= end[idx] || start[idx+1] <= start(j);
|
||||
|
@ -834,7 +881,14 @@ namespace smt {
|
|||
SASSERT(resource_available(jr, available[idx]));
|
||||
literal l2 = mk_ge(m_jobs[j].m_start, available[idx1].m_start);
|
||||
literal l3 = mk_le(m_jobs[j].m_start, available[idx].m_end);
|
||||
get_context().mk_th_axiom(get_id(), ~eq, l2, l3);
|
||||
context& ctx = get_context();
|
||||
if (m.has_trace_stream()) {
|
||||
app_ref body(m);
|
||||
body = m.mk_implies(ctx.bool_var2expr(eq.var()), m.mk_or(ctx.bool_var2expr(l2.var()), ctx.bool_var2expr(l3.var())));
|
||||
log_axiom_instantiation(body);
|
||||
}
|
||||
ctx.mk_th_axiom(get_id(), ~eq, l2, l3);
|
||||
if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
|
||||
}
|
||||
|
||||
// resource(j) = r => end(j) <= end[idx] || start[idx+1] <= start(j);
|
||||
|
@ -845,7 +899,14 @@ namespace smt {
|
|||
SASSERT(resource_available(jr, available[idx]));
|
||||
literal l2 = mk_le(m_jobs[j].m_end, available[idx].m_end);
|
||||
literal l3 = mk_ge(m_jobs[j].m_start, available[idx1].m_start);
|
||||
get_context().mk_th_axiom(get_id(), ~eq, l2, l3);
|
||||
context& ctx = get_context();
|
||||
if (m.has_trace_stream()) {
|
||||
app_ref body(m);
|
||||
body = m.mk_implies(ctx.bool_var2expr(eq.var()), m.mk_or(ctx.bool_var2expr(l2.var()), ctx.bool_var2expr(l3.var())));
|
||||
log_axiom_instantiation(body);
|
||||
}
|
||||
ctx.mk_th_axiom(get_id(), ~eq, l2, l3);
|
||||
if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
|
||||
}
|
||||
|
||||
/**
|
||||
|
@ -864,6 +925,12 @@ namespace smt {
|
|||
if (ctx.is_diseq(e1, e2))
|
||||
continue;
|
||||
literal eq = mk_eq_lit(e1, e2);
|
||||
if (m.has_trace_stream()) {
|
||||
app_ref body(m);
|
||||
body = m.mk_or(ctx.bool_var2expr(eq.var()), m.mk_not(ctx.bool_var2expr(eq.var())));
|
||||
log_axiom_instantiation(body);
|
||||
m.trace_stream() << "[end-of-instance]\n";
|
||||
}
|
||||
if (ctx.get_assignment(eq) != l_false) {
|
||||
ctx.mark_as_relevant(eq);
|
||||
if (assume_eq(e1, e2)) {
|
||||
|
@ -872,14 +939,23 @@ namespace smt {
|
|||
}
|
||||
}
|
||||
literal_vector lits;
|
||||
expr_ref_vector exprs(m);
|
||||
for (job_resource const& jr : jrs) {
|
||||
unsigned r = jr.m_resource_id;
|
||||
res_info const& ri = m_resources[r];
|
||||
enode* e1 = ji.m_job2resource;
|
||||
enode* e2 = ri.m_resource;
|
||||
lits.push_back(mk_eq_lit(e1, e2));
|
||||
literal eq = mk_eq_lit(e1, e2);
|
||||
lits.push_back(eq);
|
||||
exprs.push_back(ctx.bool_var2expr(eq.var()));
|
||||
}
|
||||
if (m.has_trace_stream()) {
|
||||
app_ref body(m);
|
||||
body = m.mk_or(exprs.size(), exprs.c_ptr());
|
||||
log_axiom_instantiation(body);
|
||||
}
|
||||
ctx.mk_th_axiom(get_id(), lits.size(), lits.c_ptr());
|
||||
if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
|
||||
return true;
|
||||
}
|
||||
|
||||
|
|
|
@ -1026,9 +1026,18 @@ public:
|
|||
expr_ref rem(a.mk_rem(dividend, divisor), m);
|
||||
expr_ref mod(a.mk_mod(dividend, divisor), m);
|
||||
expr_ref mmod(a.mk_uminus(mod), m);
|
||||
literal dgez = mk_literal(a.mk_ge(divisor, zero));
|
||||
mk_axiom(~dgez, th.mk_eq(rem, mod, false));
|
||||
mk_axiom( dgez, th.mk_eq(rem, mmod, false));
|
||||
expr_ref degz_expr(a.mk_ge(divisor, zero), m);
|
||||
literal dgez = mk_literal(degz_expr);
|
||||
literal pos = th.mk_eq(rem, mod, false);
|
||||
literal neg = th.mk_eq(rem, mmod, false);
|
||||
if (m.has_trace_stream()) {
|
||||
app_ref body(m);
|
||||
body = m.mk_ite(degz_expr, ctx().bool_var2expr(pos.var()), ctx().bool_var2expr(neg.var()));
|
||||
th.log_axiom_instantiation(body);
|
||||
}
|
||||
mk_axiom(~dgez, pos);
|
||||
mk_axiom( dgez, neg);
|
||||
if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
|
||||
}
|
||||
|
||||
// q = 0 or q * (p div q) = p
|
||||
|
@ -1036,7 +1045,13 @@ public:
|
|||
if (a.is_zero(q)) return;
|
||||
literal eqz = th.mk_eq(q, a.mk_real(0), false);
|
||||
literal eq = th.mk_eq(a.mk_mul(q, a.mk_div(p, q)), p, false);
|
||||
if (m.has_trace_stream()) {
|
||||
app_ref body(m);
|
||||
body = m.mk_implies(m.mk_not(ctx().bool_var2expr(eqz.var())), ctx().bool_var2expr(eq.var()));
|
||||
th.log_axiom_instantiation(body);
|
||||
}
|
||||
mk_axiom(eqz, eq);
|
||||
if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
|
||||
}
|
||||
|
||||
// to_int (to_real x) = x
|
||||
|
@ -1045,14 +1060,28 @@ public:
|
|||
expr* x = nullptr, *y = nullptr;
|
||||
VERIFY (a.is_to_int(n, x));
|
||||
if (a.is_to_real(x, y)) {
|
||||
if (m.has_trace_stream()) {
|
||||
app_ref body(m);
|
||||
body = m.mk_eq(n, y);
|
||||
th.log_axiom_instantiation(body);
|
||||
}
|
||||
mk_axiom(th.mk_eq(y, n, false));
|
||||
if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
|
||||
}
|
||||
else {
|
||||
expr_ref to_r(a.mk_to_real(n), m);
|
||||
expr_ref lo(a.mk_le(a.mk_sub(to_r, x), a.mk_real(0)), m);
|
||||
expr_ref hi(a.mk_ge(a.mk_sub(x, to_r), a.mk_real(1)), m);
|
||||
if (m.has_trace_stream()) th.log_axiom_instantiation(lo);
|
||||
mk_axiom(mk_literal(lo));
|
||||
if (m.has_trace_stream()) {
|
||||
m.trace_stream() << "[end-of-instance]\n";
|
||||
expr_ref body(m);
|
||||
body = m.mk_not(hi);
|
||||
th.log_axiom_instantiation(body);
|
||||
}
|
||||
mk_axiom(~mk_literal(hi));
|
||||
if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
|
||||
}
|
||||
}
|
||||
|
||||
|
@ -1062,8 +1091,14 @@ public:
|
|||
VERIFY(a.is_is_int(n, x));
|
||||
literal eq = th.mk_eq(a.mk_to_real(a.mk_to_int(x)), x, false);
|
||||
literal is_int = ctx().get_literal(n);
|
||||
if (m.has_trace_stream()) {
|
||||
app_ref body(m);
|
||||
body = m.mk_iff(n, ctx().bool_var2expr(eq.var()));
|
||||
th.log_axiom_instantiation(body);
|
||||
}
|
||||
mk_axiom(~is_int, eq);
|
||||
mk_axiom(is_int, ~eq);
|
||||
if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
|
||||
}
|
||||
|
||||
// create axiom for
|
||||
|
@ -1115,17 +1150,60 @@ public:
|
|||
k = rational::zero();
|
||||
}
|
||||
|
||||
context& c = ctx();
|
||||
if (!k.is_zero()) {
|
||||
if (m.has_trace_stream()) {
|
||||
app_ref body(m);
|
||||
body = m.mk_implies(m.mk_not(m.mk_eq(q, zero)), c.bool_var2expr(eq.var()));
|
||||
th.log_axiom_instantiation(body);
|
||||
}
|
||||
mk_axiom(eq);
|
||||
if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
|
||||
if (m.has_trace_stream()) {
|
||||
app_ref body(m);
|
||||
body = m.mk_implies(m.mk_not(m.mk_eq(q, zero)), c.bool_var2expr(mod_ge_0.var()));
|
||||
th.log_axiom_instantiation(body);
|
||||
}
|
||||
mk_axiom(mod_ge_0);
|
||||
if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
|
||||
if (m.has_trace_stream()) {
|
||||
app_ref body(m);
|
||||
body = m.mk_implies(m.mk_not(m.mk_eq(q, zero)), a.mk_le(mod, upper));
|
||||
th.log_axiom_instantiation(body);
|
||||
}
|
||||
mk_axiom(mk_literal(a.mk_le(mod, upper)));
|
||||
if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
|
||||
if (k.is_pos()) {
|
||||
if (m.has_trace_stream()) {
|
||||
app_ref body(m);
|
||||
body = m.mk_implies(m.mk_and(a.mk_gt(q, zero), c.bool_var2expr(p_ge_0.var())), c.bool_var2expr(div_ge_0.var()));
|
||||
th.log_axiom_instantiation(body);
|
||||
}
|
||||
mk_axiom(~p_ge_0, div_ge_0);
|
||||
if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
|
||||
if (m.has_trace_stream()) {
|
||||
app_ref body(m);
|
||||
body = m.mk_implies(m.mk_and(a.mk_gt(q, zero), c.bool_var2expr(p_le_0.var())), c.bool_var2expr(div_le_0.var()));
|
||||
th.log_axiom_instantiation(body);
|
||||
}
|
||||
mk_axiom(~p_le_0, div_le_0);
|
||||
if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
|
||||
}
|
||||
else {
|
||||
if (m.has_trace_stream()) {
|
||||
app_ref body(m);
|
||||
body = m.mk_implies(m.mk_and(a.mk_lt(q, zero), c.bool_var2expr(p_ge_0.var())), c.bool_var2expr(div_le_0.var()));
|
||||
th.log_axiom_instantiation(body);
|
||||
}
|
||||
mk_axiom(~p_ge_0, div_le_0);
|
||||
if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
|
||||
if (m.has_trace_stream()) {
|
||||
app_ref body(m);
|
||||
body = m.mk_implies(m.mk_and(a.mk_lt(q, zero), c.bool_var2expr(p_le_0.var())), c.bool_var2expr(div_ge_0.var()));
|
||||
th.log_axiom_instantiation(body);
|
||||
}
|
||||
mk_axiom(~p_le_0, div_ge_0);
|
||||
if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
|
||||
}
|
||||
}
|
||||
else {
|
||||
|
@ -1137,26 +1215,82 @@ public:
|
|||
// q >= 0 or (p mod q) < -q
|
||||
literal q_ge_0 = mk_literal(a.mk_ge(q, zero));
|
||||
literal q_le_0 = mk_literal(a.mk_le(q, zero));
|
||||
if (m.has_trace_stream()) {
|
||||
app_ref body(m);
|
||||
body = m.mk_implies(m.mk_not(m.mk_eq(q, zero)), c.bool_var2expr(eq.var()));
|
||||
th.log_axiom_instantiation(body);
|
||||
}
|
||||
mk_axiom(q_ge_0, eq);
|
||||
mk_axiom(q_le_0, eq);
|
||||
if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
|
||||
if (m.has_trace_stream()) {
|
||||
app_ref body(m);
|
||||
body = m.mk_implies(m.mk_not(m.mk_eq(q, zero)), c.bool_var2expr(mod_ge_0.var()));
|
||||
th.log_axiom_instantiation(body);
|
||||
}
|
||||
mk_axiom(q_ge_0, mod_ge_0);
|
||||
mk_axiom(q_le_0, mod_ge_0);
|
||||
if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
|
||||
if (m.has_trace_stream()) {
|
||||
app_ref body(m);
|
||||
body = m.mk_implies(a.mk_lt(q, zero), a.mk_lt(a.mk_sub(mod, q), zero));
|
||||
th.log_axiom_instantiation(body);
|
||||
}
|
||||
mk_axiom(q_le_0, ~mk_literal(a.mk_ge(a.mk_sub(mod, q), zero)));
|
||||
if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
|
||||
if (m.has_trace_stream()) {
|
||||
app_ref body(m);
|
||||
body = m.mk_implies(a.mk_lt(q, zero), a.mk_lt(a.mk_add(mod, q), zero));
|
||||
th.log_axiom_instantiation(body);
|
||||
}
|
||||
mk_axiom(q_ge_0, ~mk_literal(a.mk_ge(a.mk_add(mod, q), zero)));
|
||||
if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
|
||||
if (m.has_trace_stream()) {
|
||||
app_ref body(m);
|
||||
body = m.mk_implies(m.mk_and(a.mk_gt(q, zero), c.bool_var2expr(p_ge_0.var())), c.bool_var2expr(div_ge_0.var()));
|
||||
th.log_axiom_instantiation(body);
|
||||
}
|
||||
mk_axiom(q_le_0, ~p_ge_0, div_ge_0);
|
||||
if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
|
||||
if (m.has_trace_stream()) {
|
||||
app_ref body(m);
|
||||
body = m.mk_implies(m.mk_and(a.mk_gt(q, zero), c.bool_var2expr(p_le_0.var())), c.bool_var2expr(div_le_0.var()));
|
||||
th.log_axiom_instantiation(body);
|
||||
}
|
||||
mk_axiom(q_le_0, ~p_le_0, div_le_0);
|
||||
if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
|
||||
if (m.has_trace_stream()) {
|
||||
app_ref body(m);
|
||||
body = m.mk_implies(m.mk_and(a.mk_lt(q, zero), c.bool_var2expr(p_ge_0.var())), c.bool_var2expr(div_le_0.var()));
|
||||
th.log_axiom_instantiation(body);
|
||||
}
|
||||
mk_axiom(q_ge_0, ~p_ge_0, div_le_0);
|
||||
if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
|
||||
if (m.has_trace_stream()) {
|
||||
app_ref body(m);
|
||||
body = m.mk_implies(m.mk_and(a.mk_lt(q, zero), c.bool_var2expr(p_le_0.var())), c.bool_var2expr(div_ge_0.var()));
|
||||
th.log_axiom_instantiation(body);
|
||||
}
|
||||
mk_axiom(q_ge_0, ~p_le_0, div_ge_0);
|
||||
if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
|
||||
}
|
||||
if (m_arith_params.m_arith_enum_const_mod && k.is_pos() && k < rational(8)) {
|
||||
unsigned _k = k.get_unsigned();
|
||||
literal_buffer lits;
|
||||
expr_ref_vector exprs(m);
|
||||
for (unsigned j = 0; j < _k; ++j) {
|
||||
literal mod_j = th.mk_eq(mod, a.mk_int(j), false);
|
||||
lits.push_back(mod_j);
|
||||
exprs.push_back(c.bool_var2expr(mod_j.var()));
|
||||
ctx().mark_as_relevant(mod_j);
|
||||
}
|
||||
if (m.has_trace_stream()) {
|
||||
app_ref body(m);
|
||||
body = m.mk_or(exprs.size(), exprs.c_ptr());
|
||||
th.log_axiom_instantiation(body);
|
||||
}
|
||||
ctx().mk_th_axiom(get_id(), lits.size(), lits.begin());
|
||||
if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
|
||||
}
|
||||
}
|
||||
|
||||
|
@ -1591,8 +1725,20 @@ public:
|
|||
literal p_ge_r1 = mk_literal(a.mk_ge(p, a.mk_numeral(lo, true)));
|
||||
literal n_le_div = mk_literal(a.mk_le(n, a.mk_numeral(div_r, true)));
|
||||
literal n_ge_div = mk_literal(a.mk_ge(n, a.mk_numeral(div_r, true)));
|
||||
if (m.has_trace_stream()) {
|
||||
app_ref body(m);
|
||||
body = m.mk_implies(ctx().bool_var2expr(p_le_r1.var()), ctx().bool_var2expr(n_le_div.var()));
|
||||
th.log_axiom_instantiation(body);
|
||||
}
|
||||
mk_axiom(~p_le_r1, n_le_div);
|
||||
if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
|
||||
if (m.has_trace_stream()) {
|
||||
app_ref body(m);
|
||||
body = m.mk_implies(ctx().bool_var2expr(p_ge_r1.var()), ctx().bool_var2expr(n_ge_div.var()));
|
||||
th.log_axiom_instantiation(body);
|
||||
}
|
||||
mk_axiom(~p_ge_r1, n_ge_div);
|
||||
if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
|
||||
|
||||
all_divs_valid = false;
|
||||
|
||||
|
@ -1631,8 +1777,20 @@ public:
|
|||
literal pq_rhs = ~mk_literal(a.mk_ge(pqr, zero));
|
||||
literal n_le_div = mk_literal(a.mk_le(n, divc));
|
||||
literal n_ge_div = mk_literal(a.mk_ge(n, divc));
|
||||
if (m.has_trace_stream()) {
|
||||
app_ref body(m);
|
||||
body = m.mk_implies(ctx().bool_var2expr(pq_lhs.var()), ctx().bool_var2expr(n_le_div.var()));
|
||||
th.log_axiom_instantiation(body);
|
||||
}
|
||||
mk_axiom(pq_lhs, n_le_div);
|
||||
if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
|
||||
if (m.has_trace_stream()) {
|
||||
app_ref body(m);
|
||||
body = m.mk_implies(ctx().bool_var2expr(pq_rhs.var()), ctx().bool_var2expr(n_ge_div.var()));
|
||||
th.log_axiom_instantiation(body);
|
||||
}
|
||||
mk_axiom(pq_rhs, n_ge_div);
|
||||
if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
|
||||
TRACE("arith",
|
||||
literal_vector lits;
|
||||
lits.push_back(pq_lhs);
|
||||
|
@ -1747,6 +1905,12 @@ public:
|
|||
case lp::lia_move::branch: {
|
||||
TRACE("arith", tout << "branch\n";);
|
||||
app_ref b = mk_bound(m_lia->get_term(), m_lia->get_offset(), !m_lia->is_upper());
|
||||
if (m.has_trace_stream()) {
|
||||
app_ref body(m);
|
||||
body = m.mk_or(b, m.mk_not(b));
|
||||
th.log_axiom_instantiation(body);
|
||||
m.trace_stream() << "[end-of-instance]\n";
|
||||
}
|
||||
IF_VERBOSE(2, verbose_stream() << "branch " << b << "\n";);
|
||||
// branch on term >= k + 1
|
||||
// branch on term <= k
|
||||
|
@ -1760,6 +1924,10 @@ public:
|
|||
++m_stats.m_gomory_cuts;
|
||||
// m_explanation implies term <= k
|
||||
app_ref b = mk_bound(m_lia->get_term(), m_lia->get_offset(), !m_lia->is_upper());
|
||||
if (m.has_trace_stream()) {
|
||||
th.log_axiom_instantiation(b);
|
||||
m.trace_stream() << "[end-of-instance]\n";
|
||||
}
|
||||
IF_VERBOSE(2, verbose_stream() << "cut " << b << "\n");
|
||||
TRACE("arith", dump_cut_lemma(tout, m_lia->get_term(), m_lia->get_offset(), m_lia->get_explanation(), m_lia->is_upper()););
|
||||
m_eqs.reset();
|
||||
|
|
|
@ -308,7 +308,9 @@ namespace smt {
|
|||
unsigned depth = get_depth(e.m_lhs);
|
||||
expr_ref rhs(apply_args(depth, vars, e.m_args, e.m_def->get_rhs()), m);
|
||||
literal lit = mk_eq_lit(lhs, rhs);
|
||||
if (m.has_trace_stream()) log_axiom_instantiation(ctx().bool_var2expr(lit.var()));
|
||||
ctx().mk_th_axiom(get_id(), 1, &lit);
|
||||
if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
|
||||
TRACEFN("macro expansion yields " << mk_pp(rhs, m) << "\n" <<
|
||||
"literal " << pp_lit(ctx(), lit));
|
||||
}
|
||||
|
@ -327,6 +329,7 @@ namespace smt {
|
|||
// add case-axioms for all case-paths
|
||||
auto & vars = e.m_def->get_vars();
|
||||
literal_vector preds;
|
||||
expr_ref_vector pred_exprs(m);
|
||||
for (recfun::case_def const & c : e.m_def->get_cases()) {
|
||||
// applied predicate to `args`
|
||||
app_ref pred_applied = c.apply_case_predicate(e.m_args);
|
||||
|
@ -337,6 +340,7 @@ namespace smt {
|
|||
SASSERT(u().owns_app(pred_applied));
|
||||
literal concl = mk_literal(pred_applied);
|
||||
preds.push_back(concl);
|
||||
pred_exprs.push_back(pred_applied);
|
||||
|
||||
if (c.is_immediate()) {
|
||||
body_expansion be(pred_applied, c, e.m_args);
|
||||
|
@ -348,20 +352,39 @@ namespace smt {
|
|||
}
|
||||
|
||||
literal_vector guards;
|
||||
expr_ref_vector exprs(m);
|
||||
guards.push_back(concl);
|
||||
for (auto & g : c.get_guards()) {
|
||||
expr_ref ga = apply_args(depth, vars, e.m_args, g);
|
||||
literal guard = mk_literal(ga);
|
||||
guards.push_back(~guard);
|
||||
exprs.push_back(m.mk_not(ga));
|
||||
literal c[2] = {~concl, guard};
|
||||
if (m.has_trace_stream()) {
|
||||
app_ref body(m);
|
||||
body = m.mk_implies(pred_applied, ga);
|
||||
log_axiom_instantiation(body);
|
||||
}
|
||||
ctx().mk_th_axiom(get_id(), 2, c);
|
||||
if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
|
||||
}
|
||||
if (m.has_trace_stream()) {
|
||||
app_ref body(m);
|
||||
body = m.mk_implies(m.mk_not(pred_applied), m.mk_or(exprs.size(), exprs.c_ptr()));
|
||||
log_axiom_instantiation(body);
|
||||
}
|
||||
ctx().mk_th_axiom(get_id(), guards);
|
||||
|
||||
if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
|
||||
}
|
||||
// the disjunction of branches is asserted
|
||||
// to close the available cases.
|
||||
if (m.has_trace_stream()) {
|
||||
app_ref body(m);
|
||||
body = m.mk_or(pred_exprs.size(), pred_exprs.c_ptr());
|
||||
log_axiom_instantiation(body);
|
||||
}
|
||||
ctx().mk_th_axiom(get_id(), preds);
|
||||
if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
|
||||
}
|
||||
|
||||
/**
|
||||
|
@ -382,9 +405,11 @@ namespace smt {
|
|||
expr_ref rhs = apply_args(depth, vars, args, e.m_cdef->get_rhs());
|
||||
|
||||
literal_vector clause;
|
||||
expr_ref_vector exprs(m);
|
||||
for (auto & g : e.m_cdef->get_guards()) {
|
||||
expr_ref guard = apply_args(depth, vars, args, g);
|
||||
clause.push_back(~mk_literal(guard));
|
||||
exprs.push_back(guard);
|
||||
if (clause.back() == true_literal) {
|
||||
TRACEFN("body " << pp_body_expansion(e,m) << "\n" << clause << "\n" << guard);
|
||||
return;
|
||||
|
@ -394,7 +419,13 @@ namespace smt {
|
|||
}
|
||||
}
|
||||
clause.push_back(mk_eq_lit(lhs, rhs));
|
||||
if (m.has_trace_stream()) {
|
||||
app_ref body(m);
|
||||
body = m.mk_implies(m.mk_and(exprs.size(), exprs.c_ptr()), m.mk_eq(lhs, rhs));
|
||||
log_axiom_instantiation(body);
|
||||
}
|
||||
ctx().mk_th_axiom(get_id(), clause);
|
||||
if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
|
||||
TRACEFN("body " << pp_body_expansion(e,m));
|
||||
TRACEFN(pp_lits(ctx(), clause));
|
||||
}
|
||||
|
|
|
@ -2166,6 +2166,13 @@ void theory_seq::propagate_lit(dependency* dep, unsigned n, literal const* _lits
|
|||
|
||||
m_new_propagation = true;
|
||||
ctx.assign(lit, js);
|
||||
if (m.has_trace_stream()) {
|
||||
expr_ref expr(m);
|
||||
expr = ctx.bool_var2expr(lit.var());
|
||||
if (lit.sign()) expr = m.mk_not(expr);
|
||||
log_axiom_instantiation(expr);
|
||||
m.trace_stream() << "[end-of-instance]\n";
|
||||
}
|
||||
}
|
||||
|
||||
void theory_seq::set_conflict(dependency* dep, literal_vector const& _lits) {
|
||||
|
@ -2199,7 +2206,13 @@ void theory_seq::propagate_eq(dependency* dep, enode* n1, enode* n2) {
|
|||
justification* js = ctx.mk_justification(
|
||||
ext_theory_eq_propagation_justification(
|
||||
get_id(), ctx.get_region(), lits.size(), lits.c_ptr(), eqs.size(), eqs.c_ptr(), n1, n2));
|
||||
if (m.has_trace_stream()) {
|
||||
app_ref body(m);
|
||||
body = m.mk_eq(n1->get_owner(), n2->get_owner());
|
||||
log_axiom_instantiation(body);
|
||||
}
|
||||
ctx.assign_eq(n1, n2, eq_justification(js));
|
||||
if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
|
||||
m_new_propagation = true;
|
||||
|
||||
enforce_length_coherence(n1, n2);
|
||||
|
@ -3172,6 +3185,18 @@ bool theory_seq::solve_nc(unsigned idx) {
|
|||
}
|
||||
TRACE("seq", ctx.display_literals_verbose(tout, lits.size(), lits.c_ptr()) << "\n";);
|
||||
ctx.mk_th_axiom(get_id(), lits.size(), lits.c_ptr());
|
||||
if (m.has_trace_stream()) {
|
||||
expr_ref_vector exprs(m);
|
||||
for (literal l : lits) {
|
||||
expr* e = ctx.bool_var2expr(l.var());
|
||||
if (l.sign()) e = m.mk_not(e);
|
||||
exprs.push_back(e);
|
||||
}
|
||||
app_ref body(m);
|
||||
body = m.mk_or(exprs.size(), exprs.c_ptr());
|
||||
log_axiom_instantiation(body);
|
||||
m.trace_stream() << "[end-of-instance]\n";
|
||||
}
|
||||
return true;
|
||||
}
|
||||
|
||||
|
@ -4617,16 +4642,25 @@ void theory_seq::propagate_in_re(expr* n, bool is_true) {
|
|||
unsigned_vector states;
|
||||
a->get_epsilon_closure(a->init(), states);
|
||||
lits.push_back(~lit);
|
||||
expr_ref_vector exprs(m);
|
||||
|
||||
for (unsigned st : states) {
|
||||
lits.push_back(mk_accept(s, zero, re, st));
|
||||
literal acc = mk_accept(s, zero, re, st);
|
||||
lits.push_back(acc);
|
||||
exprs.push_back(ctx.bool_var2expr(acc.var()));
|
||||
}
|
||||
if (lits.size() == 2) {
|
||||
propagate_lit(nullptr, 1, &lit, lits[1]);
|
||||
}
|
||||
else {
|
||||
TRACE("seq", ctx.display_literals_verbose(tout, lits) << "\n";);
|
||||
if (m.has_trace_stream()) {
|
||||
app_ref body(m);
|
||||
body = m.mk_implies(n, m.mk_or(exprs.size(), exprs.c_ptr()));
|
||||
log_axiom_instantiation(body);
|
||||
}
|
||||
ctx.mk_th_axiom(get_id(), lits.size(), lits.c_ptr());
|
||||
if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
|
||||
}
|
||||
}
|
||||
|
||||
|
@ -5071,19 +5105,32 @@ literal theory_seq::mk_eq_empty(expr* _e, bool phase) {
|
|||
return lit;
|
||||
}
|
||||
|
||||
void theory_seq::push_lit_as_expr(literal l, expr_ref_vector& buf) {
|
||||
expr* e = get_context().bool_var2expr(l.var());
|
||||
if (l.sign()) e = m.mk_not(e);
|
||||
buf.push_back(e);
|
||||
}
|
||||
|
||||
void theory_seq::add_axiom(literal l1, literal l2, literal l3, literal l4, literal l5) {
|
||||
context& ctx = get_context();
|
||||
literal_vector lits;
|
||||
expr_ref_vector exprs(m);
|
||||
if (l1 == true_literal || l2 == true_literal || l3 == true_literal || l4 == true_literal || l5 == true_literal) return;
|
||||
if (l1 != null_literal && l1 != false_literal) { ctx.mark_as_relevant(l1); lits.push_back(l1); }
|
||||
if (l2 != null_literal && l2 != false_literal) { ctx.mark_as_relevant(l2); lits.push_back(l2); }
|
||||
if (l3 != null_literal && l3 != false_literal) { ctx.mark_as_relevant(l3); lits.push_back(l3); }
|
||||
if (l4 != null_literal && l4 != false_literal) { ctx.mark_as_relevant(l4); lits.push_back(l4); }
|
||||
if (l5 != null_literal && l5 != false_literal) { ctx.mark_as_relevant(l5); lits.push_back(l5); }
|
||||
if (l1 != null_literal && l1 != false_literal) { ctx.mark_as_relevant(l1); lits.push_back(l1); push_lit_as_expr(l1, exprs); }
|
||||
if (l2 != null_literal && l2 != false_literal) { ctx.mark_as_relevant(l2); lits.push_back(l2); push_lit_as_expr(l2, exprs); }
|
||||
if (l3 != null_literal && l3 != false_literal) { ctx.mark_as_relevant(l3); lits.push_back(l3); push_lit_as_expr(l3, exprs); }
|
||||
if (l4 != null_literal && l4 != false_literal) { ctx.mark_as_relevant(l4); lits.push_back(l4); push_lit_as_expr(l4, exprs); }
|
||||
if (l5 != null_literal && l5 != false_literal) { ctx.mark_as_relevant(l5); lits.push_back(l5); push_lit_as_expr(l5, exprs); }
|
||||
TRACE("seq", ctx.display_literals_verbose(tout << "assert:\n", lits) << "\n";);
|
||||
m_new_propagation = true;
|
||||
++m_stats.m_add_axiom;
|
||||
if (m.has_trace_stream()) {
|
||||
app_ref body(m);
|
||||
body = m.mk_or(exprs.size(), exprs.c_ptr());
|
||||
log_axiom_instantiation(body);
|
||||
}
|
||||
ctx.mk_th_axiom(get_id(), lits.size(), lits.c_ptr());
|
||||
if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
|
||||
}
|
||||
|
||||
|
||||
|
@ -5208,7 +5255,13 @@ void theory_seq::propagate_eq(dependency* deps, literal_vector const& _lits, exp
|
|||
get_id(), ctx.get_region(), lits.size(), lits.c_ptr(), eqs.size(), eqs.c_ptr(), n1, n2));
|
||||
|
||||
m_new_propagation = true;
|
||||
if (m.has_trace_stream()) {
|
||||
app_ref body(m);
|
||||
body = m.mk_eq(e1, e2);
|
||||
log_axiom_instantiation(body);
|
||||
}
|
||||
ctx.assign_eq(n1, n2, eq_justification(js));
|
||||
if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
|
||||
}
|
||||
|
||||
|
||||
|
@ -5254,7 +5307,13 @@ void theory_seq::assign_eh(bool_var v, bool is_true) {
|
|||
lits.push_back(mk_literal(d));
|
||||
}
|
||||
++m_stats.m_add_axiom;
|
||||
if (m.has_trace_stream()) {
|
||||
app_ref body(m);
|
||||
body = m.mk_implies(e, m.mk_or(disj.size(), disj.c_ptr()));
|
||||
log_axiom_instantiation(body);
|
||||
}
|
||||
ctx.mk_th_axiom(get_id(), lits.size(), lits.c_ptr());
|
||||
if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
|
||||
for (expr* d : disj) {
|
||||
add_axiom(lit, ~mk_literal(d));
|
||||
}
|
||||
|
@ -5613,14 +5672,23 @@ void theory_seq::propagate_accept(literal lit, expr* acc) {
|
|||
eautomaton::moves mvs;
|
||||
aut->get_moves_from(src, mvs);
|
||||
TRACE("seq", tout << mk_pp(acc, m) << " #moves " << mvs.size() << "\n";);
|
||||
expr_ref_vector exprs(m);
|
||||
for (auto const& mv : mvs) {
|
||||
expr_ref nth = mk_nth(e, idx);
|
||||
expr_ref t = mv.t()->accept(nth);
|
||||
ctx.get_rewriter()(t);
|
||||
literal step = mk_literal(mk_step(e, idx, re, src, mv.dst(), t));
|
||||
get_context().get_rewriter()(t);
|
||||
expr_ref step_e(mk_step(e, idx, re, src, mv.dst(), t), m);
|
||||
literal step = mk_literal(step_e);
|
||||
lits.push_back(step);
|
||||
exprs.push_back(step_e);
|
||||
}
|
||||
if (m.has_trace_stream()) {
|
||||
app_ref body(m);
|
||||
body = m.mk_implies(acc, m.mk_or(exprs.size(), exprs.c_ptr()));
|
||||
log_axiom_instantiation(body);
|
||||
}
|
||||
ctx.mk_th_axiom(get_id(), lits.size(), lits.c_ptr());
|
||||
if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
|
||||
|
||||
if (_idx.get_unsigned() > m_max_unfolding_depth &&
|
||||
m_max_unfolding_lit != null_literal && ctx.get_scope_level() > 0) {
|
||||
|
|
|
@ -547,6 +547,7 @@ namespace smt {
|
|||
// terms whose meaning are encoded using axioms.
|
||||
void enque_axiom(expr* e);
|
||||
void deque_axiom(expr* e);
|
||||
void push_lit_as_expr(literal l, expr_ref_vector& buf);
|
||||
void add_axiom(literal l1, literal l2 = null_literal, literal l3 = null_literal, literal l4 = null_literal, literal l5 = null_literal);
|
||||
void add_indexof_axiom(expr* e);
|
||||
void add_replace_axiom(expr* e);
|
||||
|
|
|
@ -217,7 +217,9 @@ namespace smt {
|
|||
}
|
||||
literal lit(ctx.get_literal(e));
|
||||
ctx.mark_as_relevant(lit);
|
||||
if (m.has_trace_stream()) log_axiom_instantiation(e);
|
||||
ctx.mk_th_axiom(get_id(), 1, &lit);
|
||||
if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
|
||||
|
||||
// crash/error avoidance: add all axioms to the trail
|
||||
m_trail.push_back(e);
|
||||
|
@ -1084,7 +1086,9 @@ namespace smt {
|
|||
|
||||
literal lit(mk_eq(len_str, len, false));
|
||||
ctx.mark_as_relevant(lit);
|
||||
if (m.has_trace_stream()) log_axiom_instantiation(ctx.bool_var2expr(lit.var()));
|
||||
ctx.mk_th_axiom(get_id(), 1, &lit);
|
||||
if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
|
||||
} else {
|
||||
// build axiom 1: Length(a_str) >= 0
|
||||
{
|
||||
|
@ -1126,7 +1130,9 @@ namespace smt {
|
|||
TRACE("str", tout << "string axiom 2: " << mk_ismt2_pp(lhs, m) << " <=> " << mk_ismt2_pp(rhs, m) << std::endl;);
|
||||
literal l(mk_eq(lhs, rhs, true));
|
||||
ctx.mark_as_relevant(l);
|
||||
if (m.has_trace_stream()) log_axiom_instantiation(ctx.bool_var2expr(l.var()));
|
||||
ctx.mk_th_axiom(get_id(), 1, &l);
|
||||
if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
|
||||
}
|
||||
|
||||
}
|
||||
|
|
|
@ -172,7 +172,7 @@ public:
|
|||
}
|
||||
for (unsigned i = 0; i < n; i++) {
|
||||
if (tmp[i] == '.') {
|
||||
param_name = tmp.substr(i+1).c_str();
|
||||
param_name = tmp.c_str() + i + 1;
|
||||
tmp.resize(i);
|
||||
mod_name = tmp.c_str();
|
||||
return;
|
||||
|
|
|
@ -16,7 +16,8 @@ Author:
|
|||
Revision History:
|
||||
|
||||
--*/
|
||||
#include<sstream>
|
||||
#include <sstream>
|
||||
#include <iomanip>
|
||||
#include "util/mpz.h"
|
||||
#include "util/buffer.h"
|
||||
#include "util/trace.h"
|
||||
|
@ -1725,6 +1726,101 @@ void mpz_manager<SYNCH>::display_smt2(std::ostream & out, mpz const & a, bool de
|
|||
}
|
||||
}
|
||||
|
||||
template<bool SYNCH>
|
||||
void mpz_manager<SYNCH>::display_hex(std::ostream & out, mpz const & a, unsigned num_bits) const {
|
||||
SASSERT(num_bits % 4 == 0);
|
||||
std::ios fmt(nullptr);
|
||||
fmt.copyfmt(out);
|
||||
out << std::hex;
|
||||
if (is_small(a)) {
|
||||
out << std::setw(num_bits/4) << std::setfill('0') << get_uint64(a);
|
||||
} else {
|
||||
#ifndef _MP_GMP
|
||||
digit_t *ds = digits(a);
|
||||
unsigned sz = size(a);
|
||||
unsigned bitSize = sz * sizeof(digit_t) * 8;
|
||||
unsigned firstDigitSize;
|
||||
if (num_bits >= bitSize) {
|
||||
firstDigitSize = sizeof(digit_t) * 2;
|
||||
|
||||
for (unsigned i = 0; i < (num_bits - bitSize)/4; ++i) {
|
||||
out << "0";
|
||||
}
|
||||
} else {
|
||||
firstDigitSize = num_bits % (sizeof(digit_t) * 8) / 4;
|
||||
}
|
||||
|
||||
out << std::setfill('0') << std::setw(firstDigitSize) << ds[sz-1] << std::setw(sizeof(digit_t)*2);
|
||||
for (unsigned i = 1; i < sz; ++i) {
|
||||
out << ds[sz-i-1];
|
||||
}
|
||||
#else
|
||||
// GMP version
|
||||
size_t sz = mpz_sizeinbase(*(a.m_ptr), 16);
|
||||
unsigned requiredLength = num_bits / 4;
|
||||
unsigned padding = requiredLength > sz ? requiredLength - sz : 0;
|
||||
sbuffer<char, 1024> buffer(sz, 0);
|
||||
mpz_get_str(buffer.c_ptr(), 16, *(a.m_ptr));
|
||||
for (unsigned i = 0; i < padding; ++i) {
|
||||
out << "0";
|
||||
}
|
||||
out << buffer.c_ptr() + (sz > requiredLength ? sz - requiredLength : 0);
|
||||
#endif
|
||||
}
|
||||
out.copyfmt(fmt);
|
||||
}
|
||||
|
||||
void display_binary_data(std::ostream &out, unsigned val, unsigned numBits) {
|
||||
SASSERT(numBits <= sizeof(unsigned)*8);
|
||||
for (int shift = numBits-1; shift >= 0; --shift) {
|
||||
if (val & (1 << shift)) {
|
||||
out << "1";
|
||||
} else {
|
||||
out << "0";
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
template<bool SYNCH>
|
||||
void mpz_manager<SYNCH>::display_bin(std::ostream & out, mpz const & a, unsigned num_bits) const {
|
||||
if (is_small(a)) {
|
||||
display_binary_data(out, get_uint64(a), num_bits);
|
||||
} else {
|
||||
#ifndef _MP_GMP
|
||||
digit_t *ds = digits(a);
|
||||
unsigned sz = size(a);
|
||||
const unsigned digitBitSize = sizeof(digit_t) * 8;
|
||||
unsigned bitSize = sz * digitBitSize;
|
||||
unsigned firstDigitLength;
|
||||
if (num_bits > bitSize) {
|
||||
firstDigitLength = 0;
|
||||
for (unsigned i = 0; i < (num_bits - bitSize); ++i) {
|
||||
out << "0";
|
||||
}
|
||||
} else {
|
||||
firstDigitLength = num_bits % digitBitSize;
|
||||
}
|
||||
for (unsigned i = 0; i < sz; ++i) {
|
||||
if (i == 0 && firstDigitLength != 0) {
|
||||
display_binary_data(out, ds[sz-1], firstDigitLength);
|
||||
} else {
|
||||
display_binary_data(out, ds[sz-i-1], digitBitSize);
|
||||
}
|
||||
}
|
||||
#else
|
||||
// GMP version
|
||||
size_t sz = mpz_sizeinbase(*(a.m_ptr), 2);
|
||||
unsigned padding = num_bits > sz ? num_bits - sz : 0;
|
||||
sbuffer<char, 1024> buffer(sz, 0);
|
||||
mpz_get_str(buffer.c_ptr(), 2, *(a.m_ptr));
|
||||
for (unsigned i = 0; i < padding; ++i) {
|
||||
out << "0";
|
||||
}
|
||||
out << buffer.c_ptr() + (sz > num_bits ? sz - num_bits : 0);
|
||||
#endif
|
||||
}
|
||||
}
|
||||
|
||||
template<bool SYNCH>
|
||||
std::string mpz_manager<SYNCH>::to_string(mpz const & a) const {
|
||||
std::ostringstream buffer;
|
||||
|
|
|
@ -592,6 +592,17 @@ public:
|
|||
*/
|
||||
void display_smt2(std::ostream & out, mpz const & a, bool decimal) const;
|
||||
|
||||
/**
|
||||
\brief Displays the num_bits least significant bits of a mpz number in hexadecimal format.
|
||||
num_bits must be divisible by 4.
|
||||
*/
|
||||
void display_hex(std::ostream & out, mpz const & a, unsigned num_bits) const;
|
||||
|
||||
/**
|
||||
\brief Displays the num_bits least significant bits of a mpz number in binary format.
|
||||
*/
|
||||
void display_bin(std::ostream & out, mpz const & a, unsigned num_bits) const;
|
||||
|
||||
static unsigned hash(mpz const & a);
|
||||
|
||||
static bool is_one(mpz const & a) {
|
||||
|
|
|
@ -93,6 +93,12 @@ public:
|
|||
|
||||
void display_decimal(std::ostream & out, unsigned prec, bool truncate = false) const { return m().display_decimal(out, m_val, prec, truncate); }
|
||||
|
||||
void display_smt2(std::ostream & out) const { return m().display_smt2(out, m_val, false); }
|
||||
|
||||
void display_hex(std::ostream & out, unsigned num_bits) const { SASSERT(is_int()); return m().display_hex(out, m_val.numerator(), num_bits); }
|
||||
|
||||
void display_bin(std::ostream & out, unsigned num_bits) const { SASSERT(is_int()); return m().display_bin(out, m_val.numerator(), num_bits); }
|
||||
|
||||
bool is_uint64() const { return m().is_uint64(m_val); }
|
||||
|
||||
bool is_int64() const { return m().is_int64(m_val); }
|
||||
|
|
Loading…
Reference in a new issue