diff --git a/cmake/Z3Config.cmake.in b/cmake/Z3Config.cmake.in index dbd63b103..05570fcf9 100644 --- a/cmake/Z3Config.cmake.in +++ b/cmake/Z3Config.cmake.in @@ -10,6 +10,21 @@ # This file was built for the @CONFIG_FILE_TYPE@. ################################################################################ + +# Handle dependencies (necessary when compiling the static library) +if(NOT @Z3_BUILD_LIBZ3_SHARED@) + include(CMakeFindDependencyMacro) + + # Threads::Threads + set(THREADS_PREFER_PTHREAD_FLAG TRUE) + find_dependency(Threads) + + # GMP::GMP + if(@Z3_USE_LIB_GMP@) + find_dependency(GMP) + endif() +endif() + # Exported targets include("${CMAKE_CURRENT_LIST_DIR}/Z3Targets.cmake") diff --git a/examples/c++/example.cpp b/examples/c++/example.cpp index d49fc45b3..9ae621dbe 100644 --- a/examples/c++/example.cpp +++ b/examples/c++/example.cpp @@ -1286,6 +1286,20 @@ static void string_issue_2298() { s.pop(); } +void iterate_args() { + std::cout << "iterate arguments\n"; + context c; + expr x = c.int_const("x"); + expr y = c.int_const("y"); + sort I = c.int_sort(); + func_decl g = function("g", I, I, I); + expr e = g(x, y); + std::cout << "expression " << e << "\n"; + for (expr arg : e) + std::cout << "arg " << arg << "\n"; + +} + int main() { try { @@ -1339,6 +1353,7 @@ int main() { recfun_example(); std::cout << "\n"; string_values(); std::cout << "\n"; string_issue_2298(); std::cout << "\n"; + iterate_args(); std::cout << "\n"; std::cout << "done\n"; } catch (exception & ex) { diff --git a/src/api/api_ast.cpp b/src/api/api_ast.cpp index 4b4574b65..10a98c477 100644 --- a/src/api/api_ast.cpp +++ b/src/api/api_ast.cpp @@ -719,7 +719,7 @@ extern "C" { else if (fid == mk_c(c)->get_seq_fid() && k == RE_SORT) { return Z3_RE_SORT; } - else if (fid == mk_c(c)->get_char_fid() && k == CHAR_SORT) { + else if (fid == mk_c(c)->get_char_fid() && k == CHAR_SORT) { return Z3_CHAR_SORT; } else { @@ -1230,6 +1230,18 @@ extern "C" { } } + if (mk_c(c)->get_char_fid() == _d->get_family_id()) { + switch (_d->get_decl_kind()) { + case OP_CHAR_LE: return Z3_OP_CHAR_LE; + case OP_CHAR_TO_INT: return Z3_OP_CHAR_TO_INT; + case OP_CHAR_TO_BV: return Z3_OP_CHAR_TO_BV; + case OP_CHAR_FROM_BV: return Z3_OP_CHAR_FROM_BV; + case OP_CHAR_IS_DIGIT: return Z3_OP_CHAR_IS_DIGIT; + default: + return Z3_OP_INTERNAL; + } + } + if (mk_c(c)->get_fpa_fid() == _d->get_family_id()) { switch (_d->get_decl_kind()) { case OP_FPA_RM_NEAREST_TIES_TO_EVEN: return Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN; diff --git a/src/api/api_seq.cpp b/src/api/api_seq.cpp index d2b677330..f0f1d903e 100644 --- a/src/api/api_seq.cpp +++ b/src/api/api_seq.cpp @@ -187,14 +187,18 @@ extern "C" { svector buff; for (unsigned i = 0; i < str.length(); ++i) { unsigned ch = str[i]; - if (ch >= 256) { + if (ch <= 32 || ch >= 127) { buff.reset(); buffer.push_back('\\'); - buffer.push_back('\\'); // possibly replace by native non-escaped version? +// buffer.push_back('\\'); // possibly replace by native non-escaped version? buffer.push_back('u'); buffer.push_back('{'); while (ch > 0) { - buff.push_back('0' + (ch & 0xF)); + unsigned d = ch & 0xF; + if (d < 10) + buff.push_back('0' + d); + else + buff.push_back('a' + (d - 10)); ch /= 16; } for (unsigned j = buff.size(); j-- > 0; ) { @@ -271,6 +275,11 @@ extern "C" { MK_SORTED(Z3_mk_re_empty, mk_c(c)->sutil().re.mk_empty); MK_SORTED(Z3_mk_re_full, mk_c(c)->sutil().re.mk_full_seq); + MK_BINARY(Z3_mk_char_le, mk_c(c)->get_char_fid(), OP_CHAR_LE, SKIP); + MK_UNARY(Z3_mk_char_to_int, mk_c(c)->get_char_fid(), OP_CHAR_TO_INT, SKIP); + MK_UNARY(Z3_mk_char_to_bv, mk_c(c)->get_char_fid(), OP_CHAR_TO_BV, SKIP); + MK_UNARY(Z3_mk_char_from_bv, mk_c(c)->get_char_fid(), OP_CHAR_FROM_BV, SKIP); + MK_UNARY(Z3_mk_char_is_digit, mk_c(c)->get_char_fid(), OP_CHAR_IS_DIGIT, SKIP); }; diff --git a/src/api/api_solver.cpp b/src/api/api_solver.cpp index 2b590c070..2837d6a36 100644 --- a/src/api/api_solver.cpp +++ b/src/api/api_solver.cpp @@ -42,6 +42,7 @@ Revision History: #include "sat/dimacs.h" #include "sat/sat_solver.h" #include "sat/tactic/goal2sat.h" +#include "sat/tactic/sat2goal.h" extern "C" { diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index 97413ae54..754f78857 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -599,6 +599,7 @@ namespace z3 { iterator begin() const noexcept { return iterator(this, 0); } iterator end() const { return iterator(this, size()); } friend std::ostream & operator<<(std::ostream & out, ast_vector_tpl const & v) { out << Z3_ast_vector_to_string(v.ctx(), v); return out; } + std::string to_string() const { return std::string(Z3_ast_vector_to_string(ctx(), m_vector)); } }; @@ -1444,6 +1445,26 @@ namespace z3 { check_error(); return expr(ctx(), r); } + expr char_to_int() const { + Z3_ast r = Z3_mk_char_to_int(ctx(), *this); + check_error(); + return expr(ctx(), r); + } + expr char_to_bv() const { + Z3_ast r = Z3_mk_char_to_bv(ctx(), *this); + check_error(); + return expr(ctx(), r); + } + expr char_from_bv() const { + Z3_ast r = Z3_mk_char_from_bv(ctx(), *this); + check_error(); + return expr(ctx(), r); + } + expr is_digit() const { + Z3_ast r = Z3_mk_char_is_digit(ctx(), *this); + check_error(); + return expr(ctx(), r); + } friend expr range(expr const& lo, expr const& hi); /** @@ -1494,6 +1515,26 @@ namespace z3 { */ expr substitute(expr_vector const& dst); + + class iterator { + expr& e; + unsigned i; + public: + iterator(expr& e, unsigned i): e(e), i(i) {} + bool operator==(iterator const& other) noexcept { + return i == other.i; + } + bool operator!=(iterator const& other) noexcept { + return i != other.i; + } + expr operator*() const { return e.arg(i); } + iterator& operator++() { ++i; return *this; } + iterator operator++(int) { assert(false); return *this; } + }; + + iterator begin() { return iterator(*this, 0); } + iterator end() { return iterator(*this, is_app() ? num_args() : 0); } + }; #define _Z3_MK_BIN_(a, b, binop) \ diff --git a/src/api/dotnet/Context.cs b/src/api/dotnet/Context.cs index 7279fe847..07759b1fa 100644 --- a/src/api/dotnet/Context.cs +++ b/src/api/dotnet/Context.cs @@ -567,7 +567,7 @@ namespace Microsoft.Z3 CheckContextMatch(body); IntPtr[] argsNative = AST.ArrayToNative(args); Native.Z3_add_rec_def(nCtx, f.NativeObject, (uint)args.Length, argsNative, body.NativeObject); - } + } /// /// Creates a new function declaration. @@ -2693,7 +2693,53 @@ namespace Microsoft.Z3 CheckContextMatch(lo, hi); return new ReExpr(this, Native.Z3_mk_re_range(nCtx, lo.NativeObject, hi.NativeObject)); } - + + /// + /// Create less than or equal to between two characters. + /// + public BoolExpr MkCharLe(Expr ch1, Expr ch2) + { + Debug.Assert(ch1 != null); + Debug.Assert(ch2 != null); + return new BoolExpr(this, Native.Z3_mk_char_le(nCtx, ch1.NativeObject, ch2.NativeObject)); + } + + /// + /// Create an integer (code point) from character. + /// + public IntExpr CharToInt(Expr ch) + { + Debug.Assert(ch != null); + return new IntExpr(this, Native.Z3_mk_char_to_int(nCtx, ch.NativeObject)); + } + + /// + /// Create a bit-vector (code point) from character. + /// + public BitVecExpr CharToBV(Expr ch) + { + Debug.Assert(ch != null); + return new BitVecExpr(this, Native.Z3_mk_char_to_bv(nCtx, ch.NativeObject)); + } + + /// + /// Create a character from a bit-vector (code point). + /// + public Expr CharFromBV(BitVecExpr bv) + { + Debug.Assert(bv != null); + return new Expr(this, Native.Z3_mk_char_from_bv(nCtx, bv.NativeObject)); + } + + /// + /// Create a check if the character is a digit. + /// + public BoolExpr MkIsDigit(Expr ch) + { + Debug.Assert(ch != null); + return new BoolExpr(this, Native.Z3_mk_char_is_digit(nCtx, ch.NativeObject)); + } + #endregion #region Pseudo-Boolean constraints diff --git a/src/api/java/Context.java b/src/api/java/Context.java index 1e581c482..6b49e9e27 100644 --- a/src/api/java/Context.java +++ b/src/api/java/Context.java @@ -508,11 +508,11 @@ public class Context implements AutoCloseable { */ public void AddRecDef(FuncDecl f, Expr[] args, Expr body) { - checkContextMatch(f); - checkContextMatch(args); - checkContextMatch(body); - long[] argsNative = AST.arrayToNative(args); - Native.addRecDef(nCtx(), f.getNativeObject(), args.length, argsNative, body.getNativeObject()); + checkContextMatch(f); + checkContextMatch(args); + checkContextMatch(body); + long[] argsNative = AST.arrayToNative(args); + Native.addRecDef(nCtx(), f.getNativeObject(), args.length, argsNative, body.getNativeObject()); } /** @@ -2025,7 +2025,7 @@ public class Context implements AutoCloseable { */ public SeqExpr intToString(Expr e) { - return (SeqExpr) Expr.create(this, Native.mkIntToStr(nCtx(), e.getNativeObject())); + return (SeqExpr) Expr.create(this, Native.mkIntToStr(nCtx(), e.getNativeObject())); } /** @@ -2033,7 +2033,7 @@ public class Context implements AutoCloseable { */ public SeqExpr ubvToString(Expr e) { - return (SeqExpr) Expr.create(this, Native.mkUbvToStr(nCtx(), e.getNativeObject())); + return (SeqExpr) Expr.create(this, Native.mkUbvToStr(nCtx(), e.getNativeObject())); } /** @@ -2041,7 +2041,7 @@ public class Context implements AutoCloseable { */ public SeqExpr sbvToString(Expr e) { - return (SeqExpr) Expr.create(this, Native.mkSbvToStr(nCtx(), e.getNativeObject())); + return (SeqExpr) Expr.create(this, Native.mkSbvToStr(nCtx(), e.getNativeObject())); } /** @@ -2049,7 +2049,7 @@ public class Context implements AutoCloseable { */ public IntExpr stringToInt(Expr> e) { - return (IntExpr) Expr.create(this, Native.mkStrToInt(nCtx(), e.getNativeObject())); + return (IntExpr) Expr.create(this, Native.mkStrToInt(nCtx(), e.getNativeObject())); } /** @@ -2111,7 +2111,7 @@ public class Context implements AutoCloseable { /** * Retrieve element at index. */ - public Expr MkNth(Expr> s, Expr index) + public Expr mkNth(Expr> s, Expr index) { checkContextMatch(s, index); return (Expr) Expr.create(this, Native.mkSeqNth(nCtx(), s.getNativeObject(), index.getNativeObject())); @@ -2252,7 +2252,7 @@ public class Context implements AutoCloseable { */ public ReExpr mkEmptyRe(R s) { - return (ReExpr) Expr.create(this, Native.mkReEmpty(nCtx(), s.getNativeObject())); + return (ReExpr) Expr.create(this, Native.mkReEmpty(nCtx(), s.getNativeObject())); } /** @@ -2260,7 +2260,7 @@ public class Context implements AutoCloseable { */ public ReExpr mkFullRe(R s) { - return (ReExpr) Expr.create(this, Native.mkReFull(nCtx(), s.getNativeObject())); + return (ReExpr) Expr.create(this, Native.mkReFull(nCtx(), s.getNativeObject())); } /** @@ -2272,6 +2272,50 @@ public class Context implements AutoCloseable { return (ReExpr) Expr.create(this, Native.mkReRange(nCtx(), lo.getNativeObject(), hi.getNativeObject())); } + /** + * Create less than or equal to between two characters. + */ + public BoolExpr mkCharLe(Expr ch1, Expr ch2) + { + checkContextMatch(ch1, ch2); + return (BoolExpr) Expr.create(this, Native.mkCharLe(nCtx(), ch1.getNativeObject(), ch2.getNativeObject())); + } + + /** + * Create an integer (code point) from character. + */ + public IntExpr charToInt(Expr ch) + { + checkContextMatch(ch); + return (IntExpr) Expr.create(this, Native.mkCharToInt(nCtx(), ch.getNativeObject())); + } + + /** + * Create a bit-vector (code point) from character. + */ + public BitVecExpr charToBv(Expr ch) + { + checkContextMatch(ch); + return (BitVecExpr) Expr.create(this, Native.mkCharToBv(nCtx(), ch.getNativeObject())); + } + + /** + * Create a character from a bit-vector (code point). + */ + public Expr charFromBv(BitVecExpr bv) + { + checkContextMatch(bv); + return (Expr) Expr.create(this, Native.mkCharFromBv(nCtx(), bv.getNativeObject())); + } + + /** + * Create a check if the character is a digit. + */ + public BoolExpr mkIsDigit(Expr ch) + { + checkContextMatch(ch); + return (BoolExpr) Expr.create(this, Native.mkCharIsDigit(nCtx(), ch.getNativeObject())); + } /** * Create an at-most-k constraint. diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index 3f6dbd2e0..5c0d5765a 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -3206,7 +3206,7 @@ def Q(a, b, ctx=None): >>> Q(3,5).sort() Real """ - return simplify(RatVal(a, b)) + return simplify(RatVal(a, b, ctx=ctx)) def Int(name, ctx=None): @@ -10578,7 +10578,7 @@ class SeqSortRef(SortRef): class CharSortRef(SortRef): """Character sort.""" - + def StringSort(ctx=None): @@ -10706,12 +10706,11 @@ def is_string_value(a): """ return isinstance(a, SeqRef) and a.is_string_value() - def StringVal(s, ctx=None): """create a string expression""" - s = "".join(str(ch) if ord(ch) < 128 else "\\u{%x}" % (ord(ch)) for ch in s) + s = "".join(str(ch) if 32 <= ord(ch) and ord(ch) < 127 else "\\u{%x}" % (ord(ch)) for ch in s) ctx = _get_ctx(ctx) - return SeqRef(Z3_mk_lstring(ctx.ref(), len(s), s), ctx) + return SeqRef(Z3_mk_string(ctx.ref(), s), ctx) def String(name, ctx=None): diff --git a/src/api/z3_api.h b/src/api/z3_api.h index ac7a23a6e..a15e77788 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -1221,6 +1221,13 @@ typedef enum { Z3_OP_RE_FULL_SET, Z3_OP_RE_COMPLEMENT, + // char + Z3_OP_CHAR_LE, + Z3_OP_CHAR_TO_INT, + Z3_OP_CHAR_TO_BV, + Z3_OP_CHAR_FROM_BV, + Z3_OP_CHAR_IS_DIGIT, + // Auxiliary Z3_OP_LABEL = 0x700, Z3_OP_LABEL_LIT, @@ -1533,6 +1540,7 @@ extern "C" { - model model generation for solvers, this parameter can be overwritten when creating a solver - model_validate validate models produced by solvers - unsat_core unsat-core generation for solvers, this parameter can be overwritten when creating a solver + - encoding the string encoding used internally (must be either "unicode" - 18 bit, "bmp" - 16 bit or "ascii" - 8 bit) \sa Z3_set_param_value \sa Z3_del_config @@ -3442,7 +3450,7 @@ extern "C" { /** \brief Create a sort for unicode strings. - def_API('Z3_mk_string_sort', SORT ,(_in(CONTEXT), )) + def_API('Z3_mk_string_sort', SORT, (_in(CONTEXT), )) */ Z3_sort Z3_API Z3_mk_string_sort(Z3_context c); @@ -3452,7 +3460,7 @@ extern "C" { The sort for characters can be changed to ASCII by setting the global parameter \c unicode to \c false. - def_API('Z3_mk_char_sort', SORT ,(_in(CONTEXT), )) + def_API('Z3_mk_char_sort', SORT, (_in(CONTEXT), )) */ Z3_sort Z3_API Z3_mk_char_sort(Z3_context c); @@ -3472,7 +3480,7 @@ extern "C" { /** \brief Create a string constant out of the string that is passed in - def_API('Z3_mk_string' ,AST ,(_in(CONTEXT), _in(STRING))) + def_API('Z3_mk_string', AST, (_in(CONTEXT), _in(STRING))) */ Z3_ast Z3_API Z3_mk_string(Z3_context c, Z3_string s); @@ -3481,7 +3489,7 @@ extern "C" { It takes the length of the string as well to take into account 0 characters. The string is unescaped. - def_API('Z3_mk_lstring' ,AST ,(_in(CONTEXT), _in(UINT), _in(STRING))) + def_API('Z3_mk_lstring', AST, (_in(CONTEXT), _in(UINT), _in(STRING))) */ Z3_ast Z3_API Z3_mk_lstring(Z3_context c, unsigned len, Z3_string s); @@ -3497,7 +3505,7 @@ extern "C" { \pre Z3_is_string(c, s) - def_API('Z3_get_string' ,STRING ,(_in(CONTEXT), _in(AST))) + def_API('Z3_get_string', STRING, (_in(CONTEXT), _in(AST))) */ Z3_string Z3_API Z3_get_string(Z3_context c, Z3_ast s); @@ -3506,7 +3514,7 @@ extern "C" { \pre Z3_is_string(c, s) - def_API('Z3_get_lstring' ,CHAR_PTR ,(_in(CONTEXT), _in(AST), _out(UINT))) + def_API('Z3_get_lstring', CHAR_PTR, (_in(CONTEXT), _in(AST), _out(UINT))) */ Z3_char_ptr Z3_API Z3_get_lstring(Z3_context c, Z3_ast s, unsigned* length); @@ -3515,14 +3523,14 @@ extern "C" { \pre s is a sequence sort. - def_API('Z3_mk_seq_empty' ,AST ,(_in(CONTEXT), _in(SORT))) + def_API('Z3_mk_seq_empty', AST ,(_in(CONTEXT), _in(SORT))) */ Z3_ast Z3_API Z3_mk_seq_empty(Z3_context c, Z3_sort seq); /** \brief Create a unit sequence of \c a. - def_API('Z3_mk_seq_unit' ,AST ,(_in(CONTEXT), _in(AST))) + def_API('Z3_mk_seq_unit', AST ,(_in(CONTEXT), _in(AST))) */ Z3_ast Z3_API Z3_mk_seq_unit(Z3_context c, Z3_ast a); @@ -3531,7 +3539,7 @@ extern "C" { \pre n > 0 - def_API('Z3_mk_seq_concat' ,AST ,(_in(CONTEXT), _in(UINT), _in_array(1, AST))) + def_API('Z3_mk_seq_concat', AST ,(_in(CONTEXT), _in(UINT), _in_array(1, AST))) */ Z3_ast Z3_API Z3_mk_seq_concat(Z3_context c, unsigned n, Z3_ast const args[]); @@ -3540,7 +3548,7 @@ extern "C" { \pre prefix and s are the same sequence sorts. - def_API('Z3_mk_seq_prefix' ,AST ,(_in(CONTEXT), _in(AST), _in(AST))) + def_API('Z3_mk_seq_prefix', AST ,(_in(CONTEXT), _in(AST), _in(AST))) */ Z3_ast Z3_API Z3_mk_seq_prefix(Z3_context c, Z3_ast prefix, Z3_ast s); @@ -3549,7 +3557,7 @@ extern "C" { \pre \c suffix and \c s are the same sequence sorts. - def_API('Z3_mk_seq_suffix' ,AST ,(_in(CONTEXT), _in(AST), _in(AST))) + def_API('Z3_mk_seq_suffix', AST ,(_in(CONTEXT), _in(AST), _in(AST))) */ Z3_ast Z3_API Z3_mk_seq_suffix(Z3_context c, Z3_ast suffix, Z3_ast s); @@ -3558,7 +3566,7 @@ extern "C" { \pre \c container and \c containee are the same sequence sorts. - def_API('Z3_mk_seq_contains' ,AST ,(_in(CONTEXT), _in(AST), _in(AST))) + def_API('Z3_mk_seq_contains', AST ,(_in(CONTEXT), _in(AST), _in(AST))) */ Z3_ast Z3_API Z3_mk_seq_contains(Z3_context c, Z3_ast container, Z3_ast containee); @@ -3568,7 +3576,7 @@ extern "C" { \pre \c s1 and \c s2 are strings - def_API('Z3_mk_str_lt' ,AST ,(_in(CONTEXT), _in(AST), _in(AST))) + def_API('Z3_mk_str_lt', AST ,(_in(CONTEXT), _in(AST), _in(AST))) */ Z3_ast Z3_API Z3_mk_str_lt(Z3_context c, Z3_ast prefix, Z3_ast s); @@ -3577,21 +3585,21 @@ extern "C" { \pre \c s1 and \c s2 are strings - def_API('Z3_mk_str_le' ,AST ,(_in(CONTEXT), _in(AST), _in(AST))) + def_API('Z3_mk_str_le', AST ,(_in(CONTEXT), _in(AST), _in(AST))) */ Z3_ast Z3_API Z3_mk_str_le(Z3_context c, Z3_ast prefix, Z3_ast s); /** \brief Extract subsequence starting at \c offset of \c length. - def_API('Z3_mk_seq_extract' ,AST ,(_in(CONTEXT), _in(AST), _in(AST), _in(AST))) + def_API('Z3_mk_seq_extract', AST ,(_in(CONTEXT), _in(AST), _in(AST), _in(AST))) */ Z3_ast Z3_API Z3_mk_seq_extract(Z3_context c, Z3_ast s, Z3_ast offset, Z3_ast length); /** \brief Replace the first occurrence of \c src with \c dst in \c s. - def_API('Z3_mk_seq_replace' ,AST ,(_in(CONTEXT), _in(AST), _in(AST), _in(AST))) + def_API('Z3_mk_seq_replace', AST ,(_in(CONTEXT), _in(AST), _in(AST), _in(AST))) */ Z3_ast Z3_API Z3_mk_seq_replace(Z3_context c, Z3_ast s, Z3_ast src, Z3_ast dst); @@ -3599,7 +3607,7 @@ extern "C" { \brief Retrieve from \c s the unit sequence positioned at position \c index. The sequence is empty if the index is out of bounds. - def_API('Z3_mk_seq_at' ,AST ,(_in(CONTEXT), _in(AST), _in(AST))) + def_API('Z3_mk_seq_at', AST ,(_in(CONTEXT), _in(AST), _in(AST))) */ Z3_ast Z3_API Z3_mk_seq_at(Z3_context c, Z3_ast s, Z3_ast index); @@ -3607,14 +3615,14 @@ extern "C" { \brief Retrieve from \c s the element positioned at position \c index. The function is under-specified if the index is out of bounds. - def_API('Z3_mk_seq_nth' ,AST ,(_in(CONTEXT), _in(AST), _in(AST))) + def_API('Z3_mk_seq_nth', AST ,(_in(CONTEXT), _in(AST), _in(AST))) */ Z3_ast Z3_API Z3_mk_seq_nth(Z3_context c, Z3_ast s, Z3_ast index); /** \brief Return the length of the sequence \c s. - def_API('Z3_mk_seq_length' ,AST ,(_in(CONTEXT), _in(AST))) + def_API('Z3_mk_seq_length', AST ,(_in(CONTEXT), _in(AST))) */ Z3_ast Z3_API Z3_mk_seq_length(Z3_context c, Z3_ast s); @@ -3624,7 +3632,7 @@ extern "C" { If \c s does not contain \c substr, then the value is -1, if \c offset is the length of \c s, then the value is -1 as well. The value is -1 if \c offset is negative or larger than the length of \c s. - def_API('Z3_mk_seq_index' ,AST ,(_in(CONTEXT), _in(AST), _in(AST), _in(AST))) + def_API('Z3_mk_seq_index', AST ,(_in(CONTEXT), _in(AST), _in(AST), _in(AST))) */ Z3_ast Z3_API Z3_mk_seq_index(Z3_context c, Z3_ast s, Z3_ast substr, Z3_ast offset); @@ -3638,7 +3646,7 @@ extern "C" { /** \brief Convert string to integer. - def_API('Z3_mk_str_to_int' ,AST ,(_in(CONTEXT), _in(AST))) + def_API('Z3_mk_str_to_int', AST ,(_in(CONTEXT), _in(AST))) */ Z3_ast Z3_API Z3_mk_str_to_int(Z3_context c, Z3_ast s); @@ -3646,56 +3654,56 @@ extern "C" { /** \brief Integer to string conversion. - def_API('Z3_mk_int_to_str' ,AST ,(_in(CONTEXT), _in(AST))) + def_API('Z3_mk_int_to_str', AST ,(_in(CONTEXT), _in(AST))) */ Z3_ast Z3_API Z3_mk_int_to_str(Z3_context c, Z3_ast s); /** \brief Unsigned bit-vector to string conversion. - def_API('Z3_mk_ubv_to_str' ,AST ,(_in(CONTEXT), _in(AST))) + def_API('Z3_mk_ubv_to_str', AST ,(_in(CONTEXT), _in(AST))) */ Z3_ast Z3_API Z3_mk_ubv_to_str(Z3_context c, Z3_ast s); /** \brief Signed bit-vector to string conversion. - def_API('Z3_mk_sbv_to_str' ,AST ,(_in(CONTEXT), _in(AST))) + def_API('Z3_mk_sbv_to_str', AST ,(_in(CONTEXT), _in(AST))) */ Z3_ast Z3_API Z3_mk_sbv_to_str(Z3_context c, Z3_ast s); /** \brief Create a regular expression that accepts the sequence \c seq. - def_API('Z3_mk_seq_to_re' ,AST ,(_in(CONTEXT), _in(AST))) + def_API('Z3_mk_seq_to_re', AST ,(_in(CONTEXT), _in(AST))) */ Z3_ast Z3_API Z3_mk_seq_to_re(Z3_context c, Z3_ast seq); /** \brief Check if \c seq is in the language generated by the regular expression \c re. - def_API('Z3_mk_seq_in_re' ,AST ,(_in(CONTEXT), _in(AST), _in(AST))) + def_API('Z3_mk_seq_in_re', AST ,(_in(CONTEXT), _in(AST), _in(AST))) */ Z3_ast Z3_API Z3_mk_seq_in_re(Z3_context c, Z3_ast seq, Z3_ast re); /** \brief Create the regular language \c re+. - def_API('Z3_mk_re_plus' ,AST ,(_in(CONTEXT), _in(AST))) + def_API('Z3_mk_re_plus', AST ,(_in(CONTEXT), _in(AST))) */ Z3_ast Z3_API Z3_mk_re_plus(Z3_context c, Z3_ast re); /** \brief Create the regular language \c re*. - def_API('Z3_mk_re_star' ,AST ,(_in(CONTEXT), _in(AST))) + def_API('Z3_mk_re_star', AST ,(_in(CONTEXT), _in(AST))) */ Z3_ast Z3_API Z3_mk_re_star(Z3_context c, Z3_ast re); /** \brief Create the regular language \c [re]. - def_API('Z3_mk_re_option' ,AST ,(_in(CONTEXT), _in(AST))) + def_API('Z3_mk_re_option', AST ,(_in(CONTEXT), _in(AST))) */ Z3_ast Z3_API Z3_mk_re_option(Z3_context c, Z3_ast re); @@ -3704,7 +3712,7 @@ extern "C" { \pre n > 0 - def_API('Z3_mk_re_union' ,AST ,(_in(CONTEXT), _in(UINT), _in_array(1, AST))) + def_API('Z3_mk_re_union', AST ,(_in(CONTEXT), _in(UINT), _in_array(1, AST))) */ Z3_ast Z3_API Z3_mk_re_union(Z3_context c, unsigned n, Z3_ast const args[]); @@ -3713,7 +3721,7 @@ extern "C" { \pre n > 0 - def_API('Z3_mk_re_concat' ,AST ,(_in(CONTEXT), _in(UINT), _in_array(1, AST))) + def_API('Z3_mk_re_concat', AST ,(_in(CONTEXT), _in(UINT), _in_array(1, AST))) */ Z3_ast Z3_API Z3_mk_re_concat(Z3_context c, unsigned n, Z3_ast const args[]); @@ -3721,7 +3729,7 @@ extern "C" { /** \brief Create the range regular expression over two sequences of length 1. - def_API('Z3_mk_re_range' ,AST ,(_in(CONTEXT), _in(AST), _in(AST))) + def_API('Z3_mk_re_range', AST ,(_in(CONTEXT), _in(AST), _in(AST))) */ Z3_ast Z3_API Z3_mk_re_range(Z3_context c, Z3_ast lo, Z3_ast hi); @@ -3748,14 +3756,14 @@ extern "C" { \pre n > 0 - def_API('Z3_mk_re_intersect' ,AST ,(_in(CONTEXT), _in(UINT), _in_array(1, AST))) + def_API('Z3_mk_re_intersect', AST ,(_in(CONTEXT), _in(UINT), _in_array(1, AST))) */ Z3_ast Z3_API Z3_mk_re_intersect(Z3_context c, unsigned n, Z3_ast const args[]); /** \brief Create the complement of the regular language \c re. - def_API('Z3_mk_re_complement' ,AST ,(_in(CONTEXT), _in(AST))) + def_API('Z3_mk_re_complement', AST ,(_in(CONTEXT), _in(AST))) */ Z3_ast Z3_API Z3_mk_re_complement(Z3_context c, Z3_ast re); @@ -3764,7 +3772,7 @@ extern "C" { \pre re is a regular expression sort. - def_API('Z3_mk_re_empty' ,AST ,(_in(CONTEXT), _in(SORT))) + def_API('Z3_mk_re_empty', AST ,(_in(CONTEXT), _in(SORT))) */ Z3_ast Z3_API Z3_mk_re_empty(Z3_context c, Z3_sort re); @@ -3774,10 +3782,45 @@ extern "C" { \pre re is a regular expression sort. - def_API('Z3_mk_re_full' ,AST ,(_in(CONTEXT), _in(SORT))) + def_API('Z3_mk_re_full', AST ,(_in(CONTEXT), _in(SORT))) */ Z3_ast Z3_API Z3_mk_re_full(Z3_context c, Z3_sort re); + /** + \brief Create less than or equal to between two characters. + + def_API('Z3_mk_char_le', AST, (_in(CONTEXT), _in(AST), _in(AST))) + */ + Z3_ast Z3_API Z3_mk_char_le(Z3_context c, Z3_ast ch1, Z3_ast ch2); + + /** + \brief Create an integer (code point) from character. + + def_API('Z3_mk_char_to_int', AST, (_in(CONTEXT), _in(AST))) + */ + Z3_ast Z3_API Z3_mk_char_to_int(Z3_context c, Z3_ast ch); + + /** + \brief Create a bit-vector (code point) from character. + + def_API('Z3_mk_char_to_bv', AST, (_in(CONTEXT), _in(AST))) + */ + Z3_ast Z3_API Z3_mk_char_to_bv(Z3_context c, Z3_ast ch); + + /** + \brief Create a character from a bit-vector (code point). + + def_API('Z3_mk_char_from_bv', AST, (_in(CONTEXT), _in(AST))) + */ + Z3_ast Z3_API Z3_mk_char_from_bv(Z3_context c, Z3_ast bv); + + /** + \brief Create a check if the character is a digit. + + def_API('Z3_mk_char_is_digit', AST, (_in(CONTEXT), _in(AST))) + */ + Z3_ast Z3_API Z3_mk_char_is_digit(Z3_context c, Z3_ast ch); + /*@}*/ diff --git a/src/ast/ast_ll_pp.cpp b/src/ast/ast_ll_pp.cpp index de6efe020..4c48bc7e7 100644 --- a/src/ast/ast_ll_pp.cpp +++ b/src/ast/ast_ll_pp.cpp @@ -80,6 +80,9 @@ class ll_printer { display_child_ref(n); } break; + case AST_FUNC_DECL: + m_out << to_func_decl(n)->get_name(); + break; default: display_child_ref(n); } diff --git a/src/ast/ast_util.cpp b/src/ast/ast_util.cpp index 7148b427e..993831d64 100644 --- a/src/ast/ast_util.cpp +++ b/src/ast/ast_util.cpp @@ -379,7 +379,7 @@ bool has_uninterpreted(ast_manager& m, expr* _e) { expr_ref e(_e, m); arith_util au(m); func_decl_ref f_out(m); - for (expr* arg : subterms(e)) { + for (expr* arg : subterms::all(e)) { if (!is_app(arg)) continue; app* a = to_app(arg); diff --git a/src/ast/char_decl_plugin.cpp b/src/ast/char_decl_plugin.cpp index 7e0f6d4af..2ab4def9a 100644 --- a/src/ast/char_decl_plugin.cpp +++ b/src/ast/char_decl_plugin.cpp @@ -22,7 +22,6 @@ Author: char_decl_plugin::char_decl_plugin(): m_charc_sym("Char") { - m_unicode = gparams::get_value("unicode") != "false"; } char_decl_plugin::~char_decl_plugin() { @@ -49,7 +48,7 @@ func_decl* char_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, if (num_parameters != 1) msg << "incorrect number of parameters passed. Expected 1, received " << num_parameters; else if (arity != 0) - msg << "incorrect number of arguments passed. Expected 1, received " << arity; + msg << "incorrect number of arguments passed. Expected 0, received " << arity; else if (!parameters[0].is_int()) msg << "integer parameter expected"; else if (parameters[0].get_int() < 0) @@ -69,6 +68,32 @@ func_decl* char_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, return m.mk_func_decl(symbol("char.to_int"), arity, domain, a.mk_int(), func_decl_info(m_family_id, k, 0, nullptr)); } m.raise_exception(msg.str()); + case OP_CHAR_TO_BV: + if (num_parameters != 0) + msg << "incorrect number of parameters passed. Expected 0, received " << num_parameters; + else if (arity != 1) + msg << "incorrect number of arguments passed. Expected one character, received " << arity; + else if (m_char != domain[0]) + msg << "expected character sort argument"; + else { + bv_util b(m); + unsigned sz = num_bits(); + return m.mk_func_decl(symbol("char.to_bv"), arity, domain, b.mk_sort(sz), func_decl_info(m_family_id, k, 0, nullptr)); + } + m.raise_exception(msg.str()); + case OP_CHAR_FROM_BV: { + bv_util b(m); + if (num_parameters != 0) + msg << "incorrect number of parameters passed. Expected 0, received " << num_parameters; + else if (arity != 1) + msg << "incorrect number of arguments passed. Expected one character, received " << arity; + else if (!b.is_bv_sort(domain[0]) || b.get_bv_size(domain[0]) != num_bits()) + msg << "expected bit-vector sort argument with " << num_bits(); + else { + return m.mk_func_decl(symbol("char.from_bv"), arity, domain, m_char, func_decl_info(m_family_id, k, 0, nullptr)); + } + m.raise_exception(msg.str()); + } case OP_CHAR_IS_DIGIT: if (num_parameters != 0) msg << "incorrect number of parameters passed. Expected 0, received " << num_parameters; @@ -78,6 +103,7 @@ func_decl* char_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, return m.mk_func_decl(symbol("char.is_digit"), arity, domain, m.mk_bool_sort(), func_decl_info(m_family_id, k, 0, nullptr)); } m.raise_exception(msg.str()); + default: UNREACHABLE(); } @@ -95,6 +121,8 @@ void char_decl_plugin::get_op_names(svector& op_names, symbol cons op_names.push_back(builtin_name("Char", OP_CHAR_CONST)); op_names.push_back(builtin_name("char.to_int", OP_CHAR_TO_INT)); op_names.push_back(builtin_name("char.is_digit", OP_CHAR_IS_DIGIT)); + op_names.push_back(builtin_name("char.to_bv", OP_CHAR_TO_BV)); + op_names.push_back(builtin_name("char.from_bv", OP_CHAR_FROM_BV)); } void char_decl_plugin::get_sort_names(svector& sort_names, symbol const& logic) { diff --git a/src/ast/char_decl_plugin.h b/src/ast/char_decl_plugin.h index 50b89306e..3d934ffe4 100644 --- a/src/ast/char_decl_plugin.h +++ b/src/ast/char_decl_plugin.h @@ -34,13 +34,14 @@ enum char_op_kind { OP_CHAR_CONST, OP_CHAR_LE, OP_CHAR_TO_INT, + OP_CHAR_TO_BV, + OP_CHAR_FROM_BV, OP_CHAR_IS_DIGIT }; class char_decl_plugin : public decl_plugin { sort* m_char { nullptr }; symbol m_charc_sym; - bool m_unicode { true }; void set_manager(ast_manager * m, family_id id) override; @@ -92,12 +93,17 @@ public: bool is_is_digit(expr const* e) const { return is_app_of(e, m_family_id, OP_CHAR_IS_DIGIT); } + bool is_char2bv(expr const* e) const { return is_app_of(e, m_family_id, OP_CHAR_TO_BV); } + + bool is_bv2char(expr const* e) const { return is_app_of(e, m_family_id, OP_CHAR_FROM_BV); } + MATCH_UNARY(is_is_digit); MATCH_UNARY(is_to_int); + MATCH_UNARY(is_char2bv); + MATCH_UNARY(is_bv2char); MATCH_BINARY(is_le); - bool unicode() const { return m_unicode; } - unsigned max_char() const { return m_unicode ? zstring::unicode_max_char() : zstring::ascii_max_char(); } - unsigned num_bits() const { return m_unicode ? zstring::unicode_num_bits() : zstring::ascii_num_bits(); } + static unsigned max_char() { return zstring::max_char(); } + static unsigned num_bits() { return zstring::num_bits(); } }; diff --git a/src/ast/euf/euf_egraph.cpp b/src/ast/euf/euf_egraph.cpp index 79426202b..fd93ce943 100644 --- a/src/ast/euf/euf_egraph.cpp +++ b/src/ast/euf/euf_egraph.cpp @@ -422,6 +422,11 @@ namespace euf { set_conflict(n1, n2, j); return; } + if (r1->value() != r2->value() && r1->value() != l_undef && r2->value() != l_undef) { + SASSERT(m.is_bool(r1->get_expr())); + set_conflict(n1, n2, j); + return; + } if (!r2->interpreted() && (r1->class_size() > r2->class_size() || r1->interpreted() || r1->value() != l_undef)) { std::swap(r1, r2); diff --git a/src/ast/euf/euf_etable.cpp b/src/ast/euf/euf_etable.cpp index 43ad52726..cfc99e4a0 100644 --- a/src/ast/euf/euf_etable.cpp +++ b/src/ast/euf/euf_etable.cpp @@ -72,7 +72,7 @@ namespace euf { void * etable::mk_table_for(unsigned arity, func_decl * d) { void * r; SASSERT(d->get_arity() >= 1); - SASSERT(arity >= d->get_arity() || d->is_associative()); + SASSERT(arity >= d->get_arity() || d->is_associative() || d->is_left_associative()); switch (arity) { case 1: r = TAG(void*, alloc(unary_table), UNARY); diff --git a/src/ast/for_each_expr.cpp b/src/ast/for_each_expr.cpp index 480a66d82..2762fda38 100644 --- a/src/ast/for_each_expr.cpp +++ b/src/ast/for_each_expr.cpp @@ -64,11 +64,11 @@ bool has_skolem_functions(expr * n) { return false; } -subterms::subterms(expr_ref_vector const& es): m_es(es) {} -subterms::subterms(expr_ref const& e) : m_es(e.m()) { m_es.push_back(e); } +subterms::subterms(expr_ref_vector const& es, bool include_bound): m_include_bound(include_bound), m_es(es) {} +subterms::subterms(expr_ref const& e, bool include_bound) : m_include_bound(include_bound), m_es(e.m()) { m_es.push_back(e); } subterms::iterator subterms::begin() { return iterator(*this, true); } subterms::iterator subterms::end() { return iterator(*this, false); } -subterms::iterator::iterator(subterms& f, bool start): m_es(f.m_es) { +subterms::iterator::iterator(subterms& f, bool start): m_include_bound(f.m_include_bound), m_es(f.m_es) { if (!start) m_es.reset(); } expr* subterms::iterator::operator*() { @@ -82,14 +82,15 @@ subterms::iterator subterms::iterator::operator++(int) { subterms::iterator& subterms::iterator::operator++() { expr* e = m_es.back(); m_visited.mark(e, true); - if (is_app(e)) { - for (expr* arg : *to_app(e)) { - m_es.push_back(arg); - } - } - while (!m_es.empty() && m_visited.is_marked(m_es.back())) { + if (is_app(e)) + for (expr* arg : *to_app(e)) + m_es.push_back(arg); + else if (is_quantifier(e) && m_include_bound) + m_es.push_back(to_quantifier(e)->get_expr()); + + while (!m_es.empty() && m_visited.is_marked(m_es.back())) m_es.pop_back(); - } + return *this; } diff --git a/src/ast/for_each_expr.h b/src/ast/for_each_expr.h index d58dcccfd..b724bed86 100644 --- a/src/ast/for_each_expr.h +++ b/src/ast/for_each_expr.h @@ -168,9 +168,13 @@ bool has_skolem_functions(expr * n); // pre-order traversal of subterms class subterms { + bool m_include_bound = false; expr_ref_vector m_es; + subterms(expr_ref const& e, bool include_bound); + subterms(expr_ref_vector const& es, bool include_bound); public: class iterator { + bool m_include_bound = false; expr_ref_vector m_es; expr_mark m_visited; public: @@ -181,8 +185,12 @@ public: bool operator==(iterator const& other) const; bool operator!=(iterator const& other) const; }; - subterms(expr_ref_vector const& es); - subterms(expr_ref const& e); + + + static subterms all(expr_ref const& e) { return subterms(e, true); } + static subterms ground(expr_ref const& e) { return subterms(e, false); } + static subterms all(expr_ref_vector const& e) { return subterms(e, true); } + static subterms ground(expr_ref_vector const& e) { return subterms(e, false); } iterator begin(); iterator end(); }; diff --git a/src/ast/fpa/bv2fpa_converter.cpp b/src/ast/fpa/bv2fpa_converter.cpp index 764344f1d..49f9abacd 100644 --- a/src/ast/fpa/bv2fpa_converter.cpp +++ b/src/ast/fpa/bv2fpa_converter.cpp @@ -19,6 +19,7 @@ Notes: #include #include "ast/ast_smt2_pp.h" +#include "ast/ast_pp.h" #include "ast/well_sorted.h" #include "ast/rewriter/th_rewriter.h" #include "ast/rewriter/fpa_rewriter.h" @@ -311,10 +312,19 @@ func_interp * bv2fpa_converter::convert_func_interp(model_core * mc, func_decl * } } - expr_ref bv_els(m); - bv_els = bv_fi->get_else(); - if (bv_els) { - expr_ref ft_els = rebuild_floats(mc, rng, bv_els); + if (m_fpa_util.is_to_sbv(f) || m_fpa_util.is_to_ubv(f)) { + auto fid = m_fpa_util.get_family_id(); + auto k = m_fpa_util.is_to_sbv(f) ? OP_FPA_TO_SBV_I : OP_FPA_TO_UBV_I; + expr_ref_vector dom(m); + for (unsigned i = 0; i < f->get_arity(); ++i) + dom.push_back(m.mk_var(i, f->get_domain(i))); + parameter param = f->get_parameter(0); + func_decl_ref to_bv_i(m.mk_func_decl(fid, k, 1, ¶m, dom.size(), dom.data()), m); + expr_ref else_value(m.mk_app(to_bv_i, dom.size(), dom.data()), m); + result->set_else(else_value); + } + else if (bv_fi->get_else()) { + expr_ref ft_els = rebuild_floats(mc, rng, bv_fi->get_else()); m_th_rw(ft_els); TRACE("bv2fpa", tout << "else=" << mk_ismt2_pp(ft_els, m) << std::endl;); result->set_else(ft_els); @@ -412,24 +422,32 @@ void bv2fpa_converter::convert_min_max_specials(model_core * mc, model_core * ta app * np_cnst = kv.m_value.second; expr_ref pzero(m), nzero(m); - pzero = m_fpa_util.mk_pzero(f->get_range()); - nzero = m_fpa_util.mk_nzero(f->get_range()); + sort* srt = f->get_range(); + pzero = m_fpa_util.mk_pzero(srt); + nzero = m_fpa_util.mk_nzero(srt); expr_ref pn(m), np(m); - if (!mc->eval(pn_cnst->get_decl(), pn)) pn = pzero; - if (!mc->eval(np_cnst->get_decl(), np)) np = pzero; + if (!mc->eval(pn_cnst->get_decl(), pn)) pn = m_bv_util.mk_numeral(0, 1); + if (!mc->eval(np_cnst->get_decl(), np)) np = m_bv_util.mk_numeral(0, 1); seen.insert(pn_cnst->get_decl()); seen.insert(np_cnst->get_decl()); rational pn_num, np_num; unsigned bv_sz; - m_bv_util.is_numeral(pn, pn_num, bv_sz); - m_bv_util.is_numeral(np, np_num, bv_sz); + VERIFY(m_bv_util.is_numeral(pn, pn_num, bv_sz)); + VERIFY(m_bv_util.is_numeral(np, np_num, bv_sz)); func_interp * flt_fi = alloc(func_interp, m, f->get_arity()); expr * pn_args[2] = { pzero, nzero }; - if (pn != np) flt_fi->insert_new_entry(pn_args, (pn_num.is_one() ? nzero : pzero)); - flt_fi->set_else(np_num.is_one() ? nzero : pzero); + expr * np_args[2] = { nzero, pzero }; + flt_fi->insert_new_entry(pn_args, (pn_num.is_one() ? nzero : pzero)); + flt_fi->insert_new_entry(np_args, (np_num.is_one() ? nzero : pzero)); + + auto fid = m_fpa_util.get_family_id(); + auto k = is_decl_of(f, fid, OP_FPA_MIN) ? OP_FPA_MIN_I : OP_FPA_MAX_I; + func_decl_ref min_max_i(m.mk_func_decl(fid, k, 0, nullptr, 2, pn_args), m); + expr_ref else_value(m.mk_app(min_max_i, m.mk_var(0, srt), m.mk_var(1, srt)), m); + flt_fi->set_else(else_value); target_model->register_decl(f, flt_fi); TRACE("bv2fpa", tout << "fp.min/fp.max special: " << std::endl << diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp index 3167f2305..de0b69946 100644 --- a/src/ast/fpa/fpa2bv_converter.cpp +++ b/src/ast/fpa/fpa2bv_converter.cpp @@ -1267,6 +1267,16 @@ void fpa2bv_converter::mk_abs(sort * s, expr_ref & x, expr_ref & result) { result = m_util.mk_fp(m_bv_util.mk_numeral(0, 1), exp, sig); } +void fpa2bv_converter::mk_min_i(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { + func_decl_ref fu(m.mk_func_decl(f->get_family_id(), OP_FPA_MIN, 0, nullptr, num, args), m); + mk_min(fu, num, args, result); +} + +void fpa2bv_converter::mk_max_i(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { + func_decl_ref fu(m.mk_func_decl(f->get_family_id(), OP_FPA_MAX, 0, nullptr, num, args), m); + mk_max(fu, num, args, result); +} + void fpa2bv_converter::mk_min(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { SASSERT(num == 2); @@ -3419,6 +3429,16 @@ void fpa2bv_converter::mk_to_sbv(func_decl * f, unsigned num, expr * const * arg mk_to_bv(f, num, args, true, result); } +void fpa2bv_converter::mk_to_ubv_i(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { + func_decl_ref fu(m.mk_func_decl(f->get_family_id(), OP_FPA_TO_UBV, 0, nullptr, num, args), m); + mk_to_bv(f, num, args, false, result); +} + +void fpa2bv_converter::mk_to_sbv_i(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { + func_decl_ref fu(m.mk_func_decl(f->get_family_id(), OP_FPA_TO_SBV, 0, nullptr, num, args), m); + mk_to_bv(f, num, args, true, result); +} + expr_ref fpa2bv_converter::nan_wrap(expr * n) { expr_ref n_bv(m), arg_is_nan(m), nan(m), nan_bv(m), res(m); mk_is_nan(n, arg_is_nan); diff --git a/src/ast/fpa/fpa2bv_converter.h b/src/ast/fpa/fpa2bv_converter.h index 31a5f7f40..3a1f2ec50 100644 --- a/src/ast/fpa/fpa2bv_converter.h +++ b/src/ast/fpa/fpa2bv_converter.h @@ -141,6 +141,8 @@ public: void mk_to_ubv(func_decl * f, unsigned num, expr * const * args, expr_ref & result); void mk_to_sbv(func_decl * f, unsigned num, expr * const * args, expr_ref & result); + void mk_to_ubv_i(func_decl * f, unsigned num, expr * const * args, expr_ref & result); + void mk_to_sbv_i(func_decl * f, unsigned num, expr * const * args, expr_ref & result); void mk_to_bv_unspecified(func_decl * f, unsigned num, expr * const * args, expr_ref & result); void mk_to_real(func_decl * f, unsigned num, expr * const * args, expr_ref & result); void mk_to_real_unspecified(func_decl * f, unsigned num, expr * const * args, expr_ref & result); @@ -149,6 +151,8 @@ public: void mk_min(func_decl * f, unsigned num, expr * const * args, expr_ref & result); void mk_max(func_decl * f, unsigned num, expr * const * args, expr_ref & result); + void mk_min_i(func_decl * f, unsigned num, expr * const * args, expr_ref & result); + void mk_max_i(func_decl * f, unsigned num, expr * const * args, expr_ref & result); expr_ref mk_min_max_unspecified(func_decl * f, expr * x, expr * y); void reset(); diff --git a/src/ast/fpa/fpa2bv_rewriter.cpp b/src/ast/fpa/fpa2bv_rewriter.cpp index df9505354..68a5cd784 100644 --- a/src/ast/fpa/fpa2bv_rewriter.cpp +++ b/src/ast/fpa/fpa2bv_rewriter.cpp @@ -124,6 +124,8 @@ br_status fpa2bv_rewriter_cfg::reduce_app(func_decl * f, unsigned num, expr * co case OP_FPA_ABS: m_conv.mk_abs(f, num, args, result); return BR_DONE; case OP_FPA_MIN: m_conv.mk_min(f, num, args, result); return BR_DONE; case OP_FPA_MAX: m_conv.mk_max(f, num, args, result); return BR_DONE; + case OP_FPA_MIN_I: m_conv.mk_min_i(f, num, args, result); return BR_DONE; + case OP_FPA_MAX_I: m_conv.mk_max_i(f, num, args, result); return BR_DONE; case OP_FPA_FMA: m_conv.mk_fma(f, num, args, result); return BR_DONE; case OP_FPA_SQRT: m_conv.mk_sqrt(f, num, args, result); return BR_DONE; case OP_FPA_ROUND_TO_INTEGRAL: m_conv.mk_round_to_integral(f, num, args, result); return BR_DONE; @@ -144,6 +146,8 @@ br_status fpa2bv_rewriter_cfg::reduce_app(func_decl * f, unsigned num, expr * co case OP_FPA_FP: m_conv.mk_fp(f, num, args, result); return BR_DONE; case OP_FPA_TO_UBV: m_conv.mk_to_ubv(f, num, args, result); return BR_DONE; case OP_FPA_TO_SBV: m_conv.mk_to_sbv(f, num, args, result); return BR_DONE; + case OP_FPA_TO_UBV_I: m_conv.mk_to_ubv_i(f, num, args, result); return BR_DONE; + case OP_FPA_TO_SBV_I: m_conv.mk_to_sbv_i(f, num, args, result); return BR_DONE; case OP_FPA_TO_REAL: m_conv.mk_to_real(f, num, args, result); return BR_DONE; case OP_FPA_TO_IEEE_BV: m_conv.mk_to_ieee_bv(f, num, args, result); return BR_DONE; diff --git a/src/ast/fpa_decl_plugin.cpp b/src/ast/fpa_decl_plugin.cpp index 941140a82..2dca61a39 100644 --- a/src/ast/fpa_decl_plugin.cpp +++ b/src/ast/fpa_decl_plugin.cpp @@ -375,6 +375,8 @@ func_decl * fpa_decl_plugin::mk_binary_decl(decl_kind k, unsigned num_parameters case OP_FPA_REM: name = "fp.rem"; break; case OP_FPA_MIN: name = "fp.min"; break; case OP_FPA_MAX: name = "fp.max"; break; + case OP_FPA_MIN_I: name = "fp.min_i"; break; + case OP_FPA_MAX_I: name = "fp.max_i"; break; default: UNREACHABLE(); break; @@ -756,6 +758,8 @@ func_decl * fpa_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, case OP_FPA_REM: case OP_FPA_MIN: case OP_FPA_MAX: + case OP_FPA_MIN_I: + case OP_FPA_MAX_I: return mk_binary_decl(k, num_parameters, parameters, arity, domain, range); case OP_FPA_ADD: case OP_FPA_MUL: @@ -774,8 +778,10 @@ func_decl * fpa_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, case OP_FPA_FP: return mk_fp(k, num_parameters, parameters, arity, domain, range); case OP_FPA_TO_UBV: + case OP_FPA_TO_UBV_I: return mk_to_ubv(k, num_parameters, parameters, arity, domain, range); case OP_FPA_TO_SBV: + case OP_FPA_TO_SBV_I: return mk_to_sbv(k, num_parameters, parameters, arity, domain, range); case OP_FPA_TO_REAL: return mk_to_real(k, num_parameters, parameters, arity, domain, range); @@ -829,6 +835,8 @@ void fpa_decl_plugin::get_op_names(svector & op_names, symbol cons op_names.push_back(builtin_name("fp.roundToIntegral", OP_FPA_ROUND_TO_INTEGRAL)); op_names.push_back(builtin_name("fp.min", OP_FPA_MIN)); op_names.push_back(builtin_name("fp.max", OP_FPA_MAX)); + op_names.push_back(builtin_name("fp.min_i", OP_FPA_MIN_I)); + op_names.push_back(builtin_name("fp.max_i", OP_FPA_MAX_I)); op_names.push_back(builtin_name("fp.leq", OP_FPA_LE)); op_names.push_back(builtin_name("fp.lt", OP_FPA_LT)); op_names.push_back(builtin_name("fp.geq", OP_FPA_GE)); @@ -846,6 +854,8 @@ void fpa_decl_plugin::get_op_names(svector & op_names, symbol cons op_names.push_back(builtin_name("fp", OP_FPA_FP)); op_names.push_back(builtin_name("fp.to_ubv", OP_FPA_TO_UBV)); op_names.push_back(builtin_name("fp.to_sbv", OP_FPA_TO_SBV)); + op_names.push_back(builtin_name("fp.to_ubv_I", OP_FPA_TO_UBV_I)); + op_names.push_back(builtin_name("fp.to_sbv_I", OP_FPA_TO_SBV_I)); op_names.push_back(builtin_name("fp.to_real", OP_FPA_TO_REAL)); op_names.push_back(builtin_name("to_fp", OP_FPA_TO_FP)); @@ -927,9 +937,8 @@ bool fpa_decl_plugin::is_unique_value(app* e) const { case OP_FPA_NUM: /* see NaN */ return false; case OP_FPA_FP: - return m_manager->is_unique_value(e->get_arg(0)) && - m_manager->is_unique_value(e->get_arg(1)) && - m_manager->is_unique_value(e->get_arg(2)); + return false; /*No; generally not because of clashes with +oo, -oo, +zero, -zero, NaN */ + // a refinement would require to return true only if there is no clash with these cases. default: return false; } @@ -1065,10 +1074,12 @@ bool fpa_util::is_considered_uninterpreted(func_decl * f, unsigned n, expr* cons return is_nan(x); } else if (is_decl_of(f, ffid, OP_FPA_TO_SBV) || - is_decl_of(f, ffid, OP_FPA_TO_UBV)) { + is_decl_of(f, ffid, OP_FPA_TO_UBV) || + is_decl_of(f, ffid, OP_FPA_TO_SBV_I) || + is_decl_of(f, ffid, OP_FPA_TO_UBV_I)) { SASSERT(n == 2); SASSERT(f->get_num_parameters() == 1); - bool is_signed = f->get_decl_kind() == OP_FPA_TO_SBV; + bool is_signed = f->get_decl_kind() == OP_FPA_TO_SBV || f->get_decl_kind() == OP_FPA_TO_SBV_I; expr* rm = args[0]; expr* x = args[1]; unsigned bv_sz = f->get_parameter(0).get_int(); diff --git a/src/ast/fpa_decl_plugin.h b/src/ast/fpa_decl_plugin.h index 1cbe9fc4b..ef0a1882c 100644 --- a/src/ast/fpa_decl_plugin.h +++ b/src/ast/fpa_decl_plugin.h @@ -58,6 +58,8 @@ enum fpa_op_kind { OP_FPA_ABS, OP_FPA_MIN, OP_FPA_MAX, + OP_FPA_MIN_I, + OP_FPA_MAX_I, OP_FPA_FMA, // x*y + z OP_FPA_SQRT, OP_FPA_ROUND_TO_INTEGRAL, @@ -82,6 +84,9 @@ enum fpa_op_kind { OP_FPA_TO_SBV, OP_FPA_TO_REAL, + OP_FPA_TO_SBV_I, + OP_FPA_TO_UBV_I, + /* Extensions */ OP_FPA_TO_IEEE_BV, diff --git a/src/ast/normal_forms/defined_names.cpp b/src/ast/normal_forms/defined_names.cpp index 5aef5c075..ad5f83486 100644 --- a/src/ast/normal_forms/defined_names.cpp +++ b/src/ast/normal_forms/defined_names.cpp @@ -114,6 +114,8 @@ app * defined_names::impl::gen_name(expr * e, sort_ref_buffer & var_sorts, buffe var_sorts.push_back(s); } else { + domain.push_back(m.mk_bool_sort()); + new_args.push_back(m.mk_true()); var_sorts.push_back(m.mk_bool_sort()); // could be any sort. } var_names.push_back(symbol(i)); diff --git a/src/ast/recfun_decl_plugin.cpp b/src/ast/recfun_decl_plugin.cpp index a702b4bfd..96ddc7162 100644 --- a/src/ast/recfun_decl_plugin.cpp +++ b/src/ast/recfun_decl_plugin.cpp @@ -466,7 +466,7 @@ namespace recfun { obj_map> parents; expr_ref tmp(e, m()); parents.insert(e, ptr_vector()); - for (expr* t : subterms(tmp)) { + for (expr* t : subterms::ground(tmp)) { if (is_app(t)) { for (expr* arg : *to_app(t)) { parents.insert_if_not_there(arg, ptr_vector()).push_back(t); diff --git a/src/ast/rewriter/array_rewriter.cpp b/src/ast/rewriter/array_rewriter.cpp index b464a33f8..c25ae1156 100644 --- a/src/ast/rewriter/array_rewriter.cpp +++ b/src/ast/rewriter/array_rewriter.cpp @@ -31,7 +31,7 @@ void array_rewriter::updt_params(params_ref const & _p) { m_expand_store_eq = p.expand_store_eq(); m_expand_nested_stores = p.expand_nested_stores(); m_blast_select_store = p.blast_select_store(); - m_expand_select_ite = false; + m_expand_select_ite = p.expand_select_ite(); } void array_rewriter::get_param_descrs(param_descrs & r) { @@ -226,8 +226,7 @@ br_status array_rewriter::mk_select_core(unsigned num_args, expr * const * args, result = subst(q->get_expr(), _args.size(), _args.data()); inv_var_shifter invsh(m()); invsh(result, _args.size(), result); - return BR_REWRITE_FULL; - + return BR_REWRITE_FULL; } if (m_util.is_map(args[0])) { @@ -248,7 +247,6 @@ br_status array_rewriter::mk_select_core(unsigned num_args, expr * const * args, // select(as-array[f], I) --> f(I) func_decl * f = m_util.get_as_array_func_decl(to_app(args[0])); result = m().mk_app(f, num_args - 1, args + 1); - TRACE("array", tout << mk_pp(args[0], m()) << " " << result << "\n";); return BR_REWRITE1; } @@ -695,12 +693,6 @@ br_status array_rewriter::mk_eq_core(expr * lhs, expr * rhs, expr_ref & result) if (m_util.is_const(rhs) && m_util.is_store(lhs)) { std::swap(lhs, rhs); } - if (m_util.is_const(lhs, v) && m_util.is_store(rhs)) { - unsigned n = to_app(rhs)->get_num_args(); - result = m().mk_and(m().mk_eq(lhs, to_app(rhs)->get_arg(0)), - m().mk_eq(v, to_app(rhs)->get_arg(n - 1))); - return BR_REWRITE2; - } if (m_util.is_const(lhs, v) && m_util.is_const(rhs, w)) { result = m().mk_eq(v, w); return BR_REWRITE1; diff --git a/src/ast/rewriter/fpa_rewriter.cpp b/src/ast/rewriter/fpa_rewriter.cpp index 15aaa7672..e135268d6 100644 --- a/src/ast/rewriter/fpa_rewriter.cpp +++ b/src/ast/rewriter/fpa_rewriter.cpp @@ -66,6 +66,8 @@ br_status fpa_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con case OP_FPA_ABS: SASSERT(num_args == 1); st = mk_abs(args[0], result); break; case OP_FPA_MIN: SASSERT(num_args == 2); st = mk_min(args[0], args[1], result); break; case OP_FPA_MAX: SASSERT(num_args == 2); st = mk_max(args[0], args[1], result); break; + case OP_FPA_MIN_I: SASSERT(num_args == 2); st = mk_min(args[0], args[1], result); break; + case OP_FPA_MAX_I: SASSERT(num_args == 2); st = mk_max(args[0], args[1], result); break; case OP_FPA_FMA: SASSERT(num_args == 4); st = mk_fma(args[0], args[1], args[2], args[3], result); break; case OP_FPA_SQRT: SASSERT(num_args == 2); st = mk_sqrt(args[0], args[1], result); break; case OP_FPA_ROUND_TO_INTEGRAL: SASSERT(num_args == 2); st = mk_round_to_integral(args[0], args[1], result); break; @@ -86,8 +88,10 @@ br_status fpa_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con case OP_FPA_FP: SASSERT(num_args == 3); st = mk_fp(args[0], args[1], args[2], result); break; case OP_FPA_TO_FP: st = mk_to_fp(f, num_args, args, result); break; case OP_FPA_TO_FP_UNSIGNED: SASSERT(num_args == 2); st = mk_to_fp_unsigned(f, args[0], args[1], result); break; - case OP_FPA_TO_UBV: SASSERT(num_args == 2); st = mk_to_ubv(f, args[0], args[1], result); break; - case OP_FPA_TO_SBV: SASSERT(num_args == 2); st = mk_to_sbv(f, args[0], args[1], result); break; + case OP_FPA_TO_UBV: SASSERT(num_args == 2); st = mk_to_ubv(f, args[0], args[1], result); break; + case OP_FPA_TO_SBV: SASSERT(num_args == 2); st = mk_to_sbv(f, args[0], args[1], result); break; + case OP_FPA_TO_UBV_I: SASSERT(num_args == 2); st = mk_to_ubv(f, args[0], args[1], result); break; + case OP_FPA_TO_SBV_I: SASSERT(num_args == 2); st = mk_to_sbv(f, args[0], args[1], result); break; case OP_FPA_TO_IEEE_BV: SASSERT(num_args == 1); st = mk_to_ieee_bv(f, args[0], result); break; case OP_FPA_TO_REAL: SASSERT(num_args == 1); st = mk_to_real(args[0], result); break; diff --git a/src/ast/rewriter/rewriter.h b/src/ast/rewriter/rewriter.h index b9b3a7f85..a04c96f4f 100644 --- a/src/ast/rewriter/rewriter.h +++ b/src/ast/rewriter/rewriter.h @@ -21,6 +21,7 @@ Notes: #include "ast/ast.h" #include "ast/rewriter/rewriter_types.h" #include "ast/act_cache.h" +#include "util/obj_hashtable.h" /** \brief Common infrastructure for AST rewriters. @@ -60,6 +61,7 @@ protected: proof_ref_vector m_result_pr_stack; // -------------------------- + obj_hashtable m_blocked; expr * m_root; unsigned m_num_qvars; struct scope { @@ -112,6 +114,8 @@ protected: void set_new_child_flag(expr * old_t, expr * new_t) { if (old_t != new_t) set_new_child_flag(old_t); } void elim_reflex_prs(unsigned spos); + void block(expr* t) { m_blocked.insert(t); } + bool is_blocked(expr* t) const { return m_blocked.contains(t); } public: rewriter_core(ast_manager & m, bool proof_gen); virtual ~rewriter_core(); diff --git a/src/ast/rewriter/rewriter_def.h b/src/ast/rewriter/rewriter_def.h index 7cf62eb83..4bf829be6 100644 --- a/src/ast/rewriter/rewriter_def.h +++ b/src/ast/rewriter/rewriter_def.h @@ -192,10 +192,21 @@ bool rewriter_tpl::visit(expr * t, unsigned max_depth) { switch (t->get_kind()) { case AST_APP: if (to_app(t)->get_num_args() == 0) { - if (process_const(to_app(t))) - return true; - TRACE("rewriter", tout << "process const: " << mk_bounded_pp(t, m()) << " -> " << mk_bounded_pp(m_r,m()) << "\n";); - t = m_r; + if (process_const(to_app(t))) + return true; + TRACE("rewriter_const", tout << "process const: " << mk_bounded_pp(t, m()) << " -> " << mk_bounded_pp(m_r, m()) << "\n";); + if (!is_blocked(t)) { + rewriter_tpl rw(m(), false, m_cfg); + for (auto* s : m_blocked) + rw.block(s); + rw.block(t); + expr_ref result(m()); + rw(m_r, result, m_pr); + m_r = result; + } + set_new_child_flag(t, m_r); + result_stack().push_back(m_r); + return true; } if (max_depth != RW_UNBOUNDED_DEPTH) max_depth--; diff --git a/src/ast/rewriter/value_sweep.cpp b/src/ast/rewriter/value_sweep.cpp index e7dff58cb..11cbb16b3 100644 --- a/src/ast/rewriter/value_sweep.cpp +++ b/src/ast/rewriter/value_sweep.cpp @@ -124,14 +124,14 @@ void value_sweep::init(expr_ref_vector const& terms) { m_vars.reset(); m_qhead = 0; m_vhead = 0; - for (expr* t : subterms(terms)) { + for (expr* t : subterms::ground(terms)) { m_parents.reserve(t->get_id() + 1); if (get_value(t)) m_queue.push_back(t); else if (!is_reducible(t)) m_vars.push_back(t); } - for (expr* t : subterms(terms)) { + for (expr* t : subterms::ground(terms)) { if (!is_app(t)) continue; for (expr* arg : *to_app(t)) { diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp index 82ab83681..69ec244d5 100644 --- a/src/ast/seq_decl_plugin.cpp +++ b/src/ast/seq_decl_plugin.cpp @@ -798,6 +798,15 @@ bool seq_util::is_char2int(expr const* e) const { return ch.is_to_int(e); } +bool seq_util::is_bv2char(expr const* e) const { + return ch.is_bv2char(e); +} + +bool seq_util::is_char2bv(expr const* e) const { + return ch.is_char2bv(e); +} + + app* seq_util::mk_char(unsigned ch) const { return seq.mk_char(ch); } diff --git a/src/ast/seq_decl_plugin.h b/src/ast/seq_decl_plugin.h index 3c0f28ca6..f9589fee6 100644 --- a/src/ast/seq_decl_plugin.h +++ b/src/ast/seq_decl_plugin.h @@ -166,8 +166,6 @@ public: void finalize() override; - bool unicode() const { return get_char_plugin().unicode(); } - decl_plugin * mk_fresh() override { return alloc(seq_decl_plugin); } sort * mk_sort(decl_kind k, unsigned num_parameters, parameter const * parameters) override; @@ -241,6 +239,8 @@ public: bool is_char_is_digit(expr const* e, expr*& d) const { return ch.is_is_digit(e, d); } bool is_char_is_digit(expr const* e) const { return ch.is_is_digit(e); } bool is_char2int(expr const* e) const; + bool is_bv2char(expr const* e) const; + bool is_char2bv(expr const* e) const; app* mk_char_bit(expr* e, unsigned i); app* mk_char(unsigned ch) const; app* mk_char_is_digit(expr* e) { return ch.mk_is_digit(e); } @@ -255,6 +255,8 @@ public: MATCH_BINARY(is_char_le); MATCH_UNARY(is_char2int); + MATCH_UNARY(is_char2bv); + MATCH_UNARY(is_bv2char); bool has_re() const { return seq.has_re(); } bool has_seq() const { return seq.has_seq(); } diff --git a/src/ast/static_features.cpp b/src/ast/static_features.cpp index 5e43a0273..f6c0a59ae 100644 --- a/src/ast/static_features.cpp +++ b/src/ast/static_features.cpp @@ -406,7 +406,7 @@ void static_features::process(expr * e, bool form_ctx, bool or_and_ctx, bool ite } if (stack_depth > m_max_stack_depth) { - for (expr* arg : subterms(expr_ref(e, m))) + for (expr* arg : subterms::ground(expr_ref(e, m))) if (get_depth(arg) <= 3 || is_quantifier(arg)) process(arg, form_ctx, or_and_ctx, ite_ctx, stack_depth - 10); return; diff --git a/src/math/lp/core_solver_pretty_printer.h b/src/math/lp/core_solver_pretty_printer.h index 75e3c5ca8..3c0563c32 100644 --- a/src/math/lp/core_solver_pretty_printer.h +++ b/src/math/lp/core_solver_pretty_printer.h @@ -118,10 +118,6 @@ public: void print_basis_heading(); - void print_bottom_line() { - m_out << "----------------------" << std::endl; - } - void print_cost(); void print_given_row(vector & row, vector & signs, X rst); diff --git a/src/math/lp/core_solver_pretty_printer_def.h b/src/math/lp/core_solver_pretty_printer_def.h index 8980c1c28..2f54b175a 100644 --- a/src/math/lp/core_solver_pretty_printer_def.h +++ b/src/math/lp/core_solver_pretty_printer_def.h @@ -345,12 +345,6 @@ template void core_solver_pretty_printer::print() for (unsigned i = 0; i < nrows(); i++) { print_row(i); } - print_bottom_line(); - print_cost(); - print_x(); - print_basis_heading(); - print_lows(); - print_upps(); print_exact_norms(); if (!m_core_solver.m_column_norms.empty()) print_approx_norms(); diff --git a/src/model/model_core.cpp b/src/model/model_core.cpp index 81ec4c654..da0cfb883 100644 --- a/src/model/model_core.cpp +++ b/src/model/model_core.cpp @@ -82,6 +82,7 @@ void model_core::register_decl(func_decl * d, func_interp * fi) { func_interp* model_core::update_func_interp(func_decl* d, func_interp* fi) { TRACE("model", tout << "register " << d->get_name() << "\n";); + SASSERT(d->get_arity() > 0); SASSERT(&fi->m() == &m); func_interp* old_fi = nullptr; diff --git a/src/model/model_evaluator.cpp b/src/model/model_evaluator.cpp index fc620d757..617cfe85f 100644 --- a/src/model/model_evaluator.cpp +++ b/src/model/model_evaluator.cpp @@ -18,6 +18,7 @@ Revision History: --*/ #include "ast/ast_pp.h" #include "ast/ast_util.h" +#include "ast/for_each_expr.h" #include "ast/recfun_decl_plugin.h" #include "ast/rewriter/rewriter_types.h" #include "ast/rewriter/bool_rewriter.h" @@ -150,7 +151,7 @@ struct evaluator_cfg : public default_rewriter_cfg { br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) { auto st = reduce_app_core(f, num, args, result, result_pr); CTRACE("model_evaluator", st != BR_FAILED, - tout << f->get_name() << " "; + tout << st << " " << mk_pp(f, m) << " "; for (unsigned i = 0; i < num; ++i) tout << mk_pp(args[i], m) << " "; tout << "\n--> " << result << "\n";); @@ -161,6 +162,7 @@ struct evaluator_cfg : public default_rewriter_cfg { result_pr = nullptr; family_id fid = f->get_family_id(); bool _is_uninterp = fid != null_family_id && m.get_plugin(fid)->is_considered_uninterpreted(f); + func_decl* g = nullptr; br_status st = BR_FAILED; #if 0 struct pp { @@ -171,6 +173,8 @@ struct evaluator_cfg : public default_rewriter_cfg { }; pp _pp(f, result); #endif + + if (num == 0 && (fid == null_family_id || _is_uninterp || m_ar.is_as_array(f))) { expr * val = m_model.get_const_interp(f); if (val != nullptr) { @@ -243,42 +247,58 @@ struct evaluator_cfg : public default_rewriter_cfg { result = args[0]; st = BR_DONE; } - else if (evaluate(f, num, args, result)) { - st = BR_REWRITE1; - } - if (st == BR_FAILED && !m.is_builtin_family_id(fid)) { - st = evaluate_partial_theory_func(f, num, args, result, result_pr); - } + else if (evaluate(f, num, args, result)) + st = BR_REWRITE1; + if (st == BR_FAILED && !m.is_builtin_family_id(fid)) + st = evaluate_partial_theory_func(f, num, args, result, result_pr); if (st == BR_DONE && is_app(result)) { app* a = to_app(result); - if (evaluate(a->get_decl(), a->get_num_args(), a->get_args(), result)) { - st = BR_REWRITE1; - } - } - if (st == BR_FAILED && num == 0 && m_ar.is_as_array(f) && m_model_completion) { - func_decl* g = nullptr; - VERIFY(m_ar.is_as_array(f, g)); - expr* def = nullptr; - if (m_def_cache.find(g, def)) { - result = def; - TRACE("model_evaluator", tout << result << "\n";); - return BR_DONE; - } - func_interp * fi = m_model.get_func_interp(g); - if (fi && (result = fi->get_array_interp(g))) { - model_evaluator ev(m_model, m_params); - ev.set_model_completion(false); - result = ev(result); - m_pinned.push_back(result); - m_def_cache.insert(g, result); - TRACE("model_evaluator", tout << mk_pp(g, m) << " " << result << "\n";); - return BR_DONE; - } + if (evaluate(a->get_decl(), a->get_num_args(), a->get_args(), result)) + st = BR_REWRITE1; } + if (st == BR_DONE && is_app(result) && expand_as_array(to_app(result)->get_decl(), result)) + return BR_REWRITE_FULL; + + if (st == BR_FAILED && expand_as_array(f, result)) + return BR_REWRITE_FULL; return st; } + bool expand_as_array(func_decl* f, expr_ref& result) { + if (!m_model_completion) + return false; + func_decl* g = nullptr; + if (!m_ar.is_as_array(f, g)) + return false; + expr* def = nullptr; + if (m_def_cache.find(g, def)) { + result = def; + TRACE("model_evaluator", tout << result << "\n";); + return true; + } + expr_ref tmp(m); + func_interp* fi = m_model.get_func_interp(g); + if (fi && !fi->get_else()) { + fi->set_else(m_model.get_some_value(g->get_range())); + } + if (fi && (tmp = fi->get_array_interp(g))) { + model_evaluator ev(m_model, m_params); + ev.set_model_completion(false); + result = ev(tmp); + m_pinned.push_back(result); + m_def_cache.insert(g, result); + TRACE("model_evaluator", tout << mk_pp(g, m) << " " << result << "\n";); + return true; + } + + TRACE("model_evaluator", + tout << "could not get array interpretation " << mk_pp(g, m) << " " << fi << "\n"; + tout << m_model << "\n";); + + return false; + } + void expand_stores(expr_ref& val) { TRACE("model_evaluator", tout << val << "\n";); vector stores; @@ -391,8 +411,7 @@ struct evaluator_cfg : public default_rewriter_cfg { } br_status mk_array_eq(expr* a, expr* b, expr_ref& result) { - TRACE("model_evaluator", tout << "mk_array_eq " << m_array_equalities << " " - << mk_pp(a, m) << " " << mk_pp(b, m) << "\n";); + if (a == b) { result = m.mk_true(); return BR_DONE; @@ -400,6 +419,8 @@ struct evaluator_cfg : public default_rewriter_cfg { if (!m_array_equalities) { return m_ar_rw.mk_eq_core(a, b, result); } + TRACE("model_evaluator", tout << "mk_array_eq " << m_array_equalities << " " + << mk_pp(a, m) << " " << mk_pp(b, m) << "\n";); vector stores1, stores2; bool args_are_unique1, args_are_unique2; @@ -689,11 +710,10 @@ void model_evaluator::operator()(expr * t, expr_ref & result) { TRACE("model_evaluator", tout << mk_ismt2_pp(t, m()) << "\n";); m_imp->operator()(t, result); m_imp->expand_stores(result); - TRACE("model_evaluator", tout << result << "\n";); + TRACE("model_evaluator", tout << "eval: " << mk_ismt2_pp(t, m()) << " --> " << result << "\n";); } expr_ref model_evaluator::operator()(expr * t) { - TRACE("model_evaluator", tout << mk_ismt2_pp(t, m()) << "\n";); expr_ref result(m()); this->operator()(t, result); return result; diff --git a/src/model/model_v2_pp.cpp b/src/model/model_v2_pp.cpp index 556ecb35d..e50d70079 100644 --- a/src/model/model_v2_pp.cpp +++ b/src/model/model_v2_pp.cpp @@ -40,7 +40,7 @@ static void display_function(std::ostream & out, model_core const & md, func_dec out << "\n"; } if (partial) { - out << else_str << "#unspecified\n"; + out << else_str << "...\n"; } else { expr * else_val = g->get_else(); diff --git a/src/params/array_rewriter_params.pyg b/src/params/array_rewriter_params.pyg index ba178f40d..26444440f 100644 --- a/src/params/array_rewriter_params.pyg +++ b/src/params/array_rewriter_params.pyg @@ -4,5 +4,6 @@ def_module_params(module_name='rewriter', params=(("expand_select_store", BOOL, False, "conservatively replace a (select (store ...) ...) term by an if-then-else term"), ("blast_select_store", BOOL, False, "eagerly replace all (select (store ..) ..) term by an if-then-else term"), ("expand_nested_stores", BOOL, False, "replace nested stores by a lambda expression"), + ("expand_select_ite", BOOL, False, "expand select over ite expressions"), ("expand_store_eq", BOOL, False, "reduce (store ...) = (store ...) with a common base into selects"), ("sort_store", BOOL, False, "sort nested stores when the indices are known to be different"))) diff --git a/src/params/context_params.cpp b/src/params/context_params.cpp index 03f49c028..4bc37b86b 100644 --- a/src/params/context_params.cpp +++ b/src/params/context_params.cpp @@ -106,8 +106,15 @@ void context_params::set(char const * param, char const * value) { else if (p == "smtlib2_compliant") { set_bool(m_smtlib2_compliant, param, value); } - else if (p == "unicode") { - set_bool(m_unicode, param, value); + else if (p == "encoding") { + if (strcmp(value, "unicode") == 0 || strcmp(value, "bmp") == 0 || strcmp(value, "ascii") == 0) { + m_encoding = value; + } + else { + std::stringstream strm; + strm << "invalid value '" << value << "' for parameter '" << param << "' (supported: unicode, bmp, ascii)"; + throw default_exception(strm.str()); + } } else { param_descrs d; @@ -140,7 +147,7 @@ void context_params::updt_params(params_ref const & p) { m_debug_ref_count = p.get_bool("debug_ref_count", m_debug_ref_count); m_smtlib2_compliant = p.get_bool("smtlib2_compliant", m_smtlib2_compliant); m_statistics = p.get_bool("stats", m_statistics); - m_unicode = p.get_bool("unicode", m_unicode); + m_encoding = p.get_str("encoding", m_encoding.c_str()); } void context_params::collect_param_descrs(param_descrs & d) { @@ -157,7 +164,7 @@ void context_params::collect_param_descrs(param_descrs & d) { d.insert("debug_ref_count", CPK_BOOL, "debug support for AST reference counting", "false"); d.insert("smtlib2_compliant", CPK_BOOL, "enable/disable SMT-LIB 2.0 compliance", "false"); d.insert("stats", CPK_BOOL, "enable/disable statistics", "false"); - d.insert("unicode", CPK_BOOL, "use unicode strings instead of ASCII strings"); + d.insert("encoding", CPK_STRING, "string encoding used internally: unicode|bmp|ascii", "unicode"); // statistics are hidden as they are controlled by the /st option. collect_solver_param_descrs(d); } diff --git a/src/params/context_params.h b/src/params/context_params.h index b4c6e914c..ad4cee31d 100644 --- a/src/params/context_params.h +++ b/src/params/context_params.h @@ -20,6 +20,7 @@ Notes: #pragma once #include "util/params.h" +#include "util/zstring.h" class context_params { void set_bool(bool & opt, char const * param, char const * value); @@ -28,21 +29,21 @@ class context_params { unsigned m_rlimit { 0 }; public: - unsigned m_timeout { UINT_MAX } ; - std::string m_dot_proof_file; - std::string m_trace_file_name; - bool m_auto_config { true }; - bool m_proof { false }; - bool m_debug_ref_count { false }; - bool m_trace { false }; - bool m_well_sorted_check { false }; - bool m_model { true }; - bool m_model_validate { false }; - bool m_dump_models { false }; - bool m_unsat_core { false }; - bool m_smtlib2_compliant { false }; // it must be here because it enable/disable the use of coercions in the ast_manager. - bool m_statistics { false }; - bool m_unicode { true }; + unsigned m_timeout { UINT_MAX } ; + std::string m_dot_proof_file; + std::string m_trace_file_name; + bool m_auto_config { true }; + bool m_proof { false }; + bool m_debug_ref_count { false }; + bool m_trace { false }; + bool m_well_sorted_check { false }; + bool m_model { true }; + bool m_model_validate { false }; + bool m_dump_models { false }; + bool m_unsat_core { false }; + bool m_smtlib2_compliant { false }; // it must be here because it enable/disable the use of coercions in the ast_manager. + bool m_statistics { false }; + std::string m_encoding { "unicode" }; unsigned rlimit() const { return m_rlimit; } context_params(); diff --git a/src/qe/qe_mbi.cpp b/src/qe/qe_mbi.cpp index bae670394..1dcbb178f 100644 --- a/src/qe/qe_mbi.cpp +++ b/src/qe/qe_mbi.cpp @@ -246,7 +246,7 @@ namespace qe { app_ref_vector avars(m); bool_vector seen; arith_util a(m); - for (expr* e : subterms(lits)) { + for (expr* e : subterms::ground(lits)) { if ((m.is_eq(e) && a.is_int_real(to_app(e)->get_arg(0))) || a.is_arith_expr(e)) { for (expr* arg : *to_app(e)) { unsigned id = arg->get_id(); @@ -368,7 +368,7 @@ namespace qe { void uflia_mbi::add_arith_dcert(model& mdl, expr_ref_vector& lits) { obj_map> apps; arith_util a(m); - for (expr* e : subterms(lits)) { + for (expr* e : subterms::ground(lits)) { if (a.is_int_real(e) && is_uninterp(e) && to_app(e)->get_num_args() > 0) { func_decl* f = to_app(e)->get_decl(); apps.insert_if_not_there(f, ptr_vector()).push_back(to_app(e)); diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h index a5d83f273..b6affe4ee 100644 --- a/src/sat/sat_solver.h +++ b/src/sat/sat_solver.h @@ -244,12 +244,13 @@ namespace sat { // Misc // // ----------------------- - void updt_params(params_ref const & p) override; + void updt_params(params_ref const & p); static void collect_param_descrs(param_descrs & d); - void collect_statistics(statistics & st) const override; + // collect statistics from sat solver + void collect_statistics(statistics & st) const; void reset_statistics(); - void display_status(std::ostream & out) const override; + void display_status(std::ostream & out) const; /** \brief Copy (non learned) clauses from src to this solver. @@ -351,14 +352,19 @@ namespace sat { // // ----------------------- public: - bool inconsistent() const override { return m_inconsistent; } - unsigned num_vars() const override { return m_justification.size(); } - unsigned num_clauses() const override; + // is the state inconsistent? + bool inconsistent() const { return m_inconsistent; } + + // number of variables and clauses + unsigned num_vars() const { return m_justification.size(); } + unsigned num_clauses() const; + void num_binary(unsigned& given, unsigned& learned) const; unsigned num_restarts() const { return m_restarts; } - bool is_external(bool_var v) const override { return m_external[v]; } + bool is_external(bool_var v) const { return m_external[v]; } + bool is_external(literal l) const { return is_external(l.var()); } void set_external(bool_var v) override; - void set_non_external(bool_var v) override; + void set_non_external(bool_var v); bool was_eliminated(bool_var v) const { return m_eliminated[v]; } void set_eliminated(bool_var v, bool f) override; bool was_eliminated(literal l) const { return was_eliminated(l.var()); } @@ -368,16 +374,14 @@ namespace sat { unsigned scope_lvl() const { return m_scope_lvl; } unsigned search_lvl() const { return m_search_lvl; } bool at_search_lvl() const { return m_scope_lvl == m_search_lvl; } - bool at_base_lvl() const override { return m_scope_lvl == 0; } + bool at_base_lvl() const { return m_scope_lvl == 0; } lbool value(literal l) const { return m_assignment[l.index()]; } lbool value(bool_var v) const { return m_assignment[literal(v, false).index()]; } justification get_justification(literal l) const { return m_justification[l.var()]; } justification get_justification(bool_var v) const { return m_justification[v]; } unsigned lvl(bool_var v) const { return m_justification[v].level(); } unsigned lvl(literal l) const { return m_justification[l.var()].level(); } - unsigned init_trail_size() const override { return at_base_lvl() ? m_trail.size() : m_scopes[0].m_trail_lim; } unsigned trail_size() const { return m_trail.size(); } - literal trail_literal(unsigned i) const override { return m_trail[i]; } literal scope_literal(unsigned n) const { return m_trail[m_scopes[n].m_trail_lim]; } void assign(literal l, justification j) { TRACE("sat_assign", tout << l << " previous value: " << value(l) << " j: " << j << "\n";); @@ -430,7 +434,7 @@ namespace sat { bool canceled() { return !m_rlimit.inc(); } config const& get_config() const { return m_config; } drat& get_drat() { return m_drat; } - drat* get_drat_ptr() override { return &m_drat; } + drat* get_drat_ptr() { return &m_drat; } void set_incremental(bool b) { m_config.m_incremental = b; } bool is_incremental() const { return m_config.m_incremental; } extension* get_extension() const override { return m_ext.get(); } @@ -472,15 +476,37 @@ namespace sat { // // ----------------------- public: - lbool check(unsigned num_lits = 0, literal const* lits = nullptr) override; + lbool check(unsigned num_lits = 0, literal const* lits = nullptr); - model const & get_model() const override { return m_model; } + // retrieve model if solver return sat + model const & get_model() const { return m_model; } bool model_is_current() const { return m_model_is_current; } - literal_vector const& get_core() const override { return m_core; } + + // retrieve core from assumptions + literal_vector const& get_core() const { return m_core; } + model_converter const & get_model_converter() const { return m_mc; } - void flush(model_converter& mc) override { mc.flush(m_mc); } + + // The following methods are used when converting the state from the SAT solver back + // to a set of assertions. + + // retrieve model converter that handles variable elimination and other transformations + void flush(model_converter& mc) { mc.flush(m_mc); } + + // size of initial trail containing unit clauses + unsigned init_trail_size() const { return at_base_lvl() ? m_trail.size() : m_scopes[0].m_trail_lim; } + + // literal at trail index i + literal trail_literal(unsigned i) const { return m_trail[i]; } + + // collect n-ary clauses + clause_vector const& clauses() const { return m_clauses; } + + // collect binary clauses + void collect_bin_clauses(svector & r, bool learned, bool learned_only) const; + void set_model(model const& mdl, bool is_current); - char const* get_reason_unknown() const override { return m_reason_unknown.c_str(); } + char const* get_reason_unknown() const { return m_reason_unknown.c_str(); } bool check_clauses(model const& m) const; bool is_assumption(bool_var v) const; void set_activity(bool_var v, unsigned act); @@ -688,7 +714,7 @@ namespace sat { public: void user_push() override; void user_pop(unsigned num_scopes) override; - void pop_to_base_level() override; + void pop_to_base_level(); unsigned num_user_scopes() const override { return m_user_scope_literals.size(); } unsigned num_scopes() const override { return m_scopes.size(); } reslimit& rlimit() { return m_rlimit; } @@ -788,8 +814,6 @@ namespace sat { clause * const * begin_learned() const { return m_learned.begin(); } clause * const * end_learned() const { return m_learned.end(); } clause_vector const& learned() const { return m_learned; } - clause_vector const& clauses() const override { return m_clauses; } - void collect_bin_clauses(svector & r, bool learned, bool learned_only) const override; // ----------------------- @@ -798,11 +822,11 @@ namespace sat { // // ----------------------- public: - bool check_invariant() const override; + bool check_invariant() const; void display(std::ostream & out) const; void display_watches(std::ostream & out) const; void display_watches(std::ostream & out, literal lit) const; - void display_dimacs(std::ostream & out) const override; + void display_dimacs(std::ostream & out) const; std::ostream& display_model(std::ostream& out) const; void display_wcnf(std::ostream & out, unsigned sz, literal const* lits, unsigned const* weights) const; void display_assignment(std::ostream & out) const; diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp index 7999676d6..e2ce43637 100644 --- a/src/sat/sat_solver/inc_sat_solver.cpp +++ b/src/sat/sat_solver/inc_sat_solver.cpp @@ -42,6 +42,7 @@ Notes: #include "sat/sat_params.hpp" #include "sat/smt/euf_solver.h" #include "sat/tactic/goal2sat.h" +#include "sat/tactic/sat2goal.h" #include "sat/tactic/sat_tactic.h" #include "sat/sat_simplifier_params.hpp" @@ -1050,6 +1051,8 @@ private: eval.set_model_completion(true); bool all_true = true; for (expr * f : m_fmls) { + if (has_quantifiers(f)) + continue; expr_ref tmp(m); eval(f, tmp); if (m.limit().is_canceled()) diff --git a/src/sat/sat_solver_core.h b/src/sat/sat_solver_core.h index 40ac4cbc4..ca66003cb 100644 --- a/src/sat/sat_solver_core.h +++ b/src/sat/sat_solver_core.h @@ -18,14 +18,13 @@ Revision History: --*/ #pragma once - +#include "sat/sat_model_converter.h" #include "sat/sat_types.h" namespace sat { class cut_simplifier; class extension; - class drat; class solver_core { protected: @@ -34,27 +33,6 @@ namespace sat { solver_core(reslimit& l) : m_rlimit(l) {} virtual ~solver_core() {} - virtual void pop_to_base_level() {} - virtual bool at_base_lvl() const { return true; } - - // retrieve model if solver return sat - virtual model const & get_model() const = 0; - - // retrieve core from assumptions - virtual literal_vector const& get_core() const = 0; - - // is the state inconsistent? - virtual bool inconsistent() const = 0; - - // number of variables and clauses - virtual unsigned num_vars() const = 0; - virtual unsigned num_clauses() const = 0; - - // check satisfiability - virtual lbool check(unsigned num_lits = 0, literal const* lits = nullptr) = 0; - - virtual char const* get_reason_unknown() const { return "reason unavailable"; } - // add clauses virtual void add_clause(unsigned n, literal* lits, status st) = 0; void add_clause(literal l1, literal l2, status st) { @@ -68,18 +46,7 @@ namespace sat { // create boolean variable, tagged as external (= true) or internal (can be eliminated). virtual bool_var add_var(bool ext) = 0; - // update parameters - virtual void updt_params(params_ref const& p) {} - - - virtual bool check_invariant() const { return true; } - virtual void display_status(std::ostream& out) const {} - virtual void display_dimacs(std::ostream& out) const {} - - virtual bool is_external(bool_var v) const { return true; } - bool is_external(literal l) const { return is_external(l.var()); } virtual void set_external(bool_var v) {} - virtual void set_non_external(bool_var v) {} virtual void set_eliminated(bool_var v, bool f) {} virtual void set_phase(literal l) { } @@ -96,32 +63,6 @@ namespace sat { virtual void set_extension(extension* e) { if (e) throw default_exception("optional API not supported"); } virtual cut_simplifier* get_cut_simplifier() { return nullptr; } - - virtual drat* get_drat_ptr() { return nullptr; } - - - // The following methods are used when converting the state from the SAT solver back - // to a set of assertions. - - // retrieve model converter that handles variable elimination and other transformations - virtual void flush(model_converter& mc) {} - - // size of initial trail containing unit clauses - virtual unsigned init_trail_size() const = 0; - - // literal at trail index i - virtual literal trail_literal(unsigned i) const = 0; - - // collect n-ary clauses - virtual clause_vector const& clauses() const = 0; - - // collect binary clauses - typedef std::pair bin_clause; - virtual void collect_bin_clauses(svector & r, bool learned, bool learned_only) const = 0; - - // collect statistics from sat solver - virtual void collect_statistics(statistics & st) const {} - }; }; diff --git a/src/sat/smt/arith_diagnostics.cpp b/src/sat/smt/arith_diagnostics.cpp index b639c183f..2dfd508d1 100644 --- a/src/sat/smt/arith_diagnostics.cpp +++ b/src/sat/smt/arith_diagnostics.cpp @@ -57,7 +57,11 @@ namespace arith { if (ctx.is_shared(var2enode(v))) out << ", shared"; } - out << " := " << mk_bounded_pp(var2expr(v), m) << "\n"; + expr* e = var2expr(v); + out << " := "; + if (e) + out << "#" << e->get_id() << ": "; + out << mk_bounded_pp(var2expr(v), m) << "\n"; } return out; } diff --git a/src/sat/smt/arith_internalize.cpp b/src/sat/smt/arith_internalize.cpp index e59d3f4d7..f28948868 100644 --- a/src/sat/smt/arith_internalize.cpp +++ b/src/sat/smt/arith_internalize.cpp @@ -42,6 +42,7 @@ namespace arith { void solver::init_internalize() { force_push(); // initialize 0, 1 variables: + if (!m_internalize_initialized) { get_one(true); get_one(false); @@ -276,7 +277,7 @@ namespace arith { if (is_app(n)) { internalize_args(to_app(n)); for (expr* arg : *to_app(n)) - if (a.is_arith_expr(arg)) + if (a.is_arith_expr(arg) && !m.is_bool(arg)) internalize_term(arg); } theory_var v = mk_evar(n); @@ -335,21 +336,18 @@ namespace arith { } else if (a.is_le(atom, n1, n2)) { expr_ref n3(a.mk_sub(n1, n2), m); - rewrite(n3); v = internalize_def(n3); k = lp_api::upper_t; r = 0; } else if (a.is_ge(atom, n1, n2)) { expr_ref n3(a.mk_sub(n1, n2), m); - rewrite(n3); v = internalize_def(n3); k = lp_api::lower_t; r = 0; } else if (a.is_lt(atom, n1, n2)) { expr_ref n3(a.mk_sub(n1, n2), m); - rewrite(n3); v = internalize_def(n3); k = lp_api::lower_t; r = 0; @@ -357,7 +355,6 @@ namespace arith { } else if (a.is_gt(atom, n1, n2)) { expr_ref n3(a.mk_sub(n1, n2), m); - rewrite(n3); v = internalize_def(n3); k = lp_api::upper_t; r = 0; @@ -484,10 +481,10 @@ namespace arith { return st.vars()[0]; } else if (is_one(st) && a.is_numeral(term)) { - return get_one(a.is_int(term)); + return lp().local_to_external(get_one(a.is_int(term))); } else if (is_zero(st) && a.is_numeral(term)) { - return get_zero(a.is_int(term)); + return lp().local_to_external(get_zero(a.is_int(term))); } else { init_left_side(st); diff --git a/src/sat/smt/arith_solver.cpp b/src/sat/smt/arith_solver.cpp index 6ceea42f2..89b778672 100644 --- a/src/sat/smt/arith_solver.cpp +++ b/src/sat/smt/arith_solver.cpp @@ -581,6 +581,27 @@ namespace arith { value = ~value; if (!found_bad && value == get_phase(n->bool_var())) continue; + + TRACE("arith", + ptr_vector nodes; + expr_mark marks; + nodes.push_back(n->get_expr()); + for (unsigned i = 0; i < nodes.size(); ++i) { + expr* r = nodes[i]; + if (marks.is_marked(r)) + continue; + marks.mark(r); + if (is_app(r)) + for (expr* arg : *to_app(r)) + nodes.push_back(arg); + expr_ref rval(m); + expr_ref mval = mdl(r); + if (ctx.get_egraph().find(r)) + rval = mdl(ctx.get_egraph().find(r)->get_root()->get_expr()); + tout << r->get_id() << ": " << mk_bounded_pp(r, m, 1) << " := " << mval; + if (rval != mval) tout << " " << rval; + tout << "\n"; + }); TRACE("arith", tout << eval << " " << value << " " << ctx.bpp(n) << "\n"; tout << mdl << "\n"; @@ -605,8 +626,7 @@ namespace arith { else if (use_nra_model() && lp().external_to_local(v) != lp::null_lpvar) { anum const& an = nl_value(v, *m_a1); if (a.is_int(o) && !m_nla->am().is_int(an)) - value = a.mk_numeral(rational::zero(), a.is_int(o)); - else + value = a.mk_numeral(rational::zero(), a.is_int(o)); value = a.mk_numeral(m_nla->am(), nl_value(v, *m_a1), a.is_int(o)); } else if (v != euf::null_theory_var) { @@ -617,7 +637,7 @@ namespace arith { r = floor(r); value = a.mk_numeral(r, o->get_sort()); } - else if (a.is_arith_expr(o)) { + else if (a.is_arith_expr(o) && reflect(o)) { expr_ref_vector args(m); for (auto* arg : *to_app(o)) { if (m.is_value(arg)) diff --git a/src/sat/smt/array_axioms.cpp b/src/sat/smt/array_axioms.cpp index cd0b241fb..015c4a0c1 100644 --- a/src/sat/smt/array_axioms.cpp +++ b/src/sat/smt/array_axioms.cpp @@ -451,6 +451,7 @@ namespace array { expr_ref alpha(a.mk_select(args), m); expr_ref beta(alpha); rewrite(beta); + TRACE("array", tout << alpha << " == " << beta << "\n";); return ctx.propagate(e_internalize(alpha), e_internalize(beta), array_axiom()); } @@ -531,19 +532,22 @@ namespace array { if (!get_config().m_array_delay_exp_axiom) return false; unsigned num_vars = get_num_vars(); + bool change = false; for (unsigned v = 0; v < num_vars; v++) { propagate_parent_select_axioms(v); auto& d = get_var_data(v); if (!d.m_prop_upward) continue; euf::enode* n = var2enode(v); + if (add_as_array_eqs(n)) + change = true; bool has_default = false; for (euf::enode* p : euf::enode_parents(n)) has_default |= a.is_default(p->get_expr()); if (has_default) propagate_parent_default(v); } - bool change = false; + unsigned sz = m_axiom_trail.size(); m_delay_qhead = 0; @@ -556,8 +560,30 @@ namespace array { return change; } + bool solver::add_as_array_eqs(euf::enode* n) { + func_decl* f = nullptr; + bool change = false; + if (!a.is_as_array(n->get_expr(), f)) + return false; + for (unsigned i = 0; i < ctx.get_egraph().enodes_of(f).size(); ++i) { + euf::enode* p = ctx.get_egraph().enodes_of(f)[i]; + expr_ref_vector select(m); + select.push_back(n->get_expr()); + for (expr* arg : *to_app(p->get_expr())) + select.push_back(arg); + expr_ref _e(a.mk_select(select.size(), select.data()), m); + euf::enode* e = e_internalize(_e); + if (e->get_root() != p->get_root()) { + add_unit(eq_internalize(_e, p->get_expr())); + change = true; + } + } + return change; + } + bool solver::add_interface_equalities() { sbuffer roots; + collect_defaults(); collect_shared_vars(roots); bool prop = false; for (unsigned i = roots.size(); i-- > 0; ) { @@ -568,10 +594,12 @@ namespace array { expr* e2 = var2expr(v2); if (e1->get_sort() != e2->get_sort()) continue; - if (have_different_model_values(v1, v2)) + if (must_have_different_model_values(v1, v2)) { continue; - if (ctx.get_egraph().are_diseq(var2enode(v1), var2enode(v2))) - continue; + } + if (ctx.get_egraph().are_diseq(var2enode(v1), var2enode(v2))) { + continue; + } sat::literal lit = eq_internalize(e1, e2); if (s().value(lit) == l_undef) prop = true; @@ -592,24 +620,29 @@ namespace array { if (r->is_marked1()) continue; // arrays used as indices in other arrays have to be treated as shared issue #3532, #3529 - if (ctx.is_shared(r) || is_select_arg(r)) + if (ctx.is_shared(r) || is_shared_arg(r)) roots.push_back(r->get_th_var(get_id())); r->mark1(); to_unmark.push_back(r); } - TRACE("array", tout << "collecting shared vars...\n" << unsigned_vector(roots.size(), (unsigned*)roots.data()) << "\n";); + TRACE("array", tout << "collecting shared vars...\n"; for (auto v : roots) tout << ctx.bpp(var2enode(v)) << "\n";); for (auto* n : to_unmark) n->unmark1(); } - bool solver::is_select_arg(euf::enode* r) { + bool solver::is_shared_arg(euf::enode* r) { SASSERT(r->is_root()); - for (euf::enode* n : euf::enode_parents(r)) - if (a.is_select(n->get_expr())) - for (unsigned i = 1; i < n->num_args(); ++i) - if (r == n->get_arg(i)->get_root()) + for (euf::enode* n : euf::enode_parents(r)) { + expr* e = n->get_expr(); + if (a.is_select(e)) + for (unsigned i = 1; i < n->num_args(); ++i) + if (r == n->get_arg(i)->get_root()) return true; + if (a.is_const(e)) + return true; + } + return false; } diff --git a/src/sat/smt/array_diagnostics.cpp b/src/sat/smt/array_diagnostics.cpp index f28cc47b4..c1230ea7f 100644 --- a/src/sat/smt/array_diagnostics.cpp +++ b/src/sat/smt/array_diagnostics.cpp @@ -24,7 +24,7 @@ namespace array { out << "array\n"; for (unsigned i = 0; i < get_num_vars(); ++i) { auto& d = get_var_data(i); - out << var2enode(i)->get_expr_id() << " " << (d.m_prop_upward?"up":"fx") << " " << mk_bounded_pp(var2expr(i), m, 2) << "\n"; + out << "v" << i << ": " << var2enode(i)->get_expr_id() << " " << (d.m_prop_upward?"up":"fx") << " " << mk_bounded_pp(var2expr(i), m, 2) << "\n"; display_info(out, "parent lambdas", d.m_parent_lambdas); display_info(out, "parent select", d.m_parent_selects); display_info(out, "lambdas", d.m_lambdas); diff --git a/src/sat/smt/array_internalize.cpp b/src/sat/smt/array_internalize.cpp index 55496a729..7e3f94b84 100644 --- a/src/sat/smt/array_internalize.cpp +++ b/src/sat/smt/array_internalize.cpp @@ -75,10 +75,11 @@ namespace array { } void solver::internalize_lambda(euf::enode* n) { - set_prop_upward(n); - if (!a.is_store(n->get_expr())) - push_axiom(default_axiom(n)); - add_lambda(n->get_th_var(get_id()), n); + SASSERT(is_lambda(n->get_expr()) || a.is_const(n->get_expr()) || a.is_as_array(n->get_expr())); + theory_var v = n->get_th_var(get_id()); + push_axiom(default_axiom(n)); + add_lambda(v, n); + set_prop_upward(v); } void solver::internalize_select(euf::enode* n) { diff --git a/src/sat/smt/array_model.cpp b/src/sat/smt/array_model.cpp index ecaedd97b..0fbc4364a 100644 --- a/src/sat/smt/array_model.cpp +++ b/src/sat/smt/array_model.cpp @@ -72,20 +72,6 @@ namespace array { if (!fi->get_else() && get_else(v)) fi->set_else(get_else(v)); - -#if 0 - // this functionality is already taken care of by model_init. - - if (!fi->get_else()) - for (euf::enode* k : euf::enode_class(n)) - if (a.is_const(k->get_expr())) - fi->set_else(values.get(k->get_arg(0)->get_root_id())); - - if (!fi->get_else()) - for (euf::enode* p : euf::enode_parents(n)) - if (a.is_default(p->get_expr())) - fi->set_else(values.get(p->get_root_id())); -#endif if (!fi->get_else()) { expr* else_value = nullptr; @@ -125,34 +111,27 @@ namespace array { } } + TRACE("array", tout << "array-as-function " << ctx.bpp(n) << " := " << mk_pp(f, m) << "\n" << "default " << mk_pp(fi->get_else(), m) << "\n";); parameter p(f); values.set(n->get_expr_id(), m.mk_app(get_id(), OP_AS_ARRAY, 1, &p)); } - bool solver::have_different_model_values(theory_var v1, theory_var v2) { + bool solver::must_have_different_model_values(theory_var v1, theory_var v2) { euf::enode* else1 = nullptr, * else2 = nullptr; euf::enode* n1 = var2enode(v1), *n2 = var2enode(v2); euf::enode* r1 = n1->get_root(), * r2 = n2->get_root(); expr* e1 = n1->get_expr(); - expr* e; if (!a.is_array(e1)) return true; - auto find_else = [&](theory_var v, euf::enode* r) { - var_data& d = get_var_data(find(v)); - for (euf::enode* c : d.m_lambdas) - if (a.is_const(c->get_expr(), e)) - return expr2enode(e)->get_root(); - for (euf::enode* p : euf::enode_parents(r)) - for (euf::enode* pe : euf::enode_class(p)) - if (a.is_default(pe->get_expr())) - return pe->get_root(); - return (euf::enode*)nullptr; - }; - else1 = find_else(v1, r1); - else2 = find_else(v2, r2); + + else1 = get_default(v1); + else2 = get_default(v2); if (else1 && else2 && else1->get_root() != else2->get_root() && has_large_domain(e1)) return true; + + return false; +#if 0 struct eq { solver& s; eq(solver& s) :s(s) {} @@ -196,6 +175,8 @@ namespace array { }; return table_diff(r1, r2, else1) || table_diff(r2, r1, else2); + +#endif } void solver::collect_defaults() { @@ -235,8 +216,8 @@ namespace array { } void solver::set_default(theory_var v, euf::enode* n) { - TRACE("array", tout << "set default: " << v << " " << ctx.bpp(n) << "\n";); v = mg_find(v); + CTRACE("array", !m_defaults[v], tout << "set default: " << v << " " << ctx.bpp(n) << "\n";); if (!m_defaults[v]) m_defaults[v] = n; } diff --git a/src/sat/smt/array_solver.h b/src/sat/smt/array_solver.h index b64dbfff5..0c0fc82d6 100644 --- a/src/sat/smt/array_solver.h +++ b/src/sat/smt/array_solver.h @@ -184,13 +184,14 @@ namespace array { bool assert_default_store_axiom(app* store); bool assert_congruent_axiom(expr* e1, expr* e2); bool add_delayed_axioms(); + bool add_as_array_eqs(euf::enode* n); bool has_unitary_domain(app* array_term); bool has_large_domain(expr* array_term); std::pair mk_epsilon(sort* s); void collect_shared_vars(sbuffer& roots); bool add_interface_equalities(); - bool is_select_arg(euf::enode* r); + bool is_shared_arg(euf::enode* r); bool is_array(euf::enode* n) const { return a.is_array(n->get_expr()); } // solving @@ -222,7 +223,7 @@ namespace array { euf::enode_vector m_defaults; // temporary field for model construction ptr_vector m_else_values; // svector m_parents; // temporary field for model construction - bool have_different_model_values(theory_var v1, theory_var v2); + bool must_have_different_model_values(theory_var v1, theory_var v2); void collect_defaults(); void mg_merge(theory_var u, theory_var v); theory_var mg_find(theory_var n); @@ -262,11 +263,12 @@ namespace array { euf::theory_var mk_var(euf::enode* n) override; void apply_sort_cnstr(euf::enode* n, sort* s) override; bool is_shared(theory_var v) const override; + bool enable_self_propagate() const override { return true; } void merge_eh(theory_var, theory_var, theory_var v1, theory_var v2); void after_merge_eh(theory_var r1, theory_var r2, theory_var v1, theory_var v2) {} void unmerge_eh(theory_var v1, theory_var v2) {} - euf::enode_vector const& parent_selects(euf::enode* n) const { return m_var_data[n->get_th_var(get_id())]->m_parent_selects; } + euf::enode_vector const& parent_selects(euf::enode* n) { return m_var_data[find(n->get_th_var(get_id()))]->m_parent_selects; } }; } diff --git a/src/sat/smt/bv_internalize.cpp b/src/sat/smt/bv_internalize.cpp index 8c16d6052..439764515 100644 --- a/src/sat/smt/bv_internalize.cpp +++ b/src/sat/smt/bv_internalize.cpp @@ -244,8 +244,9 @@ namespace bv { expr_ref b2b(bv.mk_bit2bool(e, i), m); m_bits[v].push_back(sat::null_literal); sat::literal lit = ctx.internalize(b2b, false, false, m_is_redundant); - (void)lit; TRACE("bv", tout << "add-bit: " << lit << " " << literal2expr(lit) << "\n";); + if (m_bits[v].back() == sat::null_literal) + m_bits[v].back() = lit; SASSERT(m_bits[v].back() == lit); } } diff --git a/src/sat/smt/bv_solver.cpp b/src/sat/smt/bv_solver.cpp index d030394a8..fe6d7e0f7 100644 --- a/src/sat/smt/bv_solver.cpp +++ b/src/sat/smt/bv_solver.cpp @@ -673,25 +673,33 @@ namespace bv { for (theory_var i = 0; i < static_cast(get_num_vars()); ++i) if (find(i) != i) result->m_find.set_root(i, find(i)); - result->m_prop_queue.append(m_prop_queue); - for (unsigned i = 0; i < m_bool_var2atom.size(); ++i) { - atom* a = m_bool_var2atom[i]; - if (!a) - continue; - atom* new_a = new (result->get_region()) atom(i); - result->m_bool_var2atom.setx(i, new_a, nullptr); - for (auto vp : *a) - new_a->m_occs = new (result->get_region()) var_pos_occ(vp.first, vp.second, new_a->m_occs); - for (eq_occurs const& occ : a->eqs()) { + auto clone_atom = [&](atom const& a) { + atom* new_a = new (result->get_region()) atom(a.m_bv); + result->m_bool_var2atom.setx(a.m_bv, new_a, nullptr); + for (auto [v, p] : a) + new_a->m_occs = new (result->get_region()) var_pos_occ(v, p, new_a->m_occs); + for (eq_occurs const& occ : a.eqs()) { expr* e = occ.m_node->get_expr(); expr_ref e2(tr(e), tr.to()); euf::enode* n = ctx.get_enode(e2); + SASSERT(tr.to().contains(e2)); new_a->m_eqs = new (result->get_region()) eq_occurs(occ.m_bv1, occ.m_bv2, occ.m_idx, occ.m_v1, occ.m_v2, occ.m_literal, n, new_a->m_eqs); } - new_a->m_def = a->m_def; - new_a->m_var = a->m_var; - // validate_atoms(); + new_a->m_def = a.m_def; + new_a->m_var = a.m_var; + }; + + for (atom* a : m_bool_var2atom) + if (a) + clone_atom(*a); + // validate_atoms(); + + for (auto p : m_prop_queue) { + propagation_item q = p; + if (p.is_atom()) + q = propagation_item(result->get_bv2a(p.m_atom->m_bv)); + result->m_prop_queue.push_back(q); } return result; } diff --git a/src/sat/smt/bv_solver.h b/src/sat/smt/bv_solver.h index 3d15c2cf1..f699a8030 100644 --- a/src/sat/smt/bv_solver.h +++ b/src/sat/smt/bv_solver.h @@ -161,11 +161,11 @@ namespace bv { struct atom { bool_var m_bv; - eq_occurs* m_eqs; - var_pos_occ * m_occs; + eq_occurs* m_eqs = nullptr; + var_pos_occ * m_occs = nullptr; svector> m_bit2occ; - literal m_var { sat::null_literal }; - literal m_def { sat::null_literal }; + literal m_var = sat::null_literal; + literal m_def = sat::null_literal; atom(bool_var b) :m_bv(b), m_eqs(nullptr), m_occs(nullptr) {} ~atom() { m_bit2occ.clear(); } var_pos_it begin() const { return var_pos_it(m_occs); } @@ -174,11 +174,12 @@ namespace bv { }; struct propagation_item { - var_pos m_vp { var_pos(0, 0) }; - atom* m_atom{ nullptr }; + var_pos m_vp = var_pos(0, 0) ; + atom* m_atom = nullptr; explicit propagation_item(atom* a) : m_atom(a) {} explicit propagation_item(var_pos const& vp) : m_vp(vp) {} bool operator==(propagation_item const& other) const { if (m_atom) return m_atom == other.m_atom; return false; } + bool is_atom() const { return m_atom != nullptr; } }; diff --git a/src/sat/smt/euf_internalize.cpp b/src/sat/smt/euf_internalize.cpp index 020d29baa..2302a8935 100644 --- a/src/sat/smt/euf_internalize.cpp +++ b/src/sat/smt/euf_internalize.cpp @@ -85,7 +85,7 @@ namespace euf { if (auto* s = expr2solver(e)) s->internalize(e, m_is_redundant); else - attach_node(m_egraph.mk(e, m_generation, 0, nullptr)); + attach_node(mk_enode(e, 0, nullptr)); return true; } @@ -100,7 +100,7 @@ namespace euf { if (auto* s = expr2solver(e)) s->internalize(e, m_is_redundant); else - attach_node(m_egraph.mk(e, m_generation, num, m_args.data())); + attach_node(mk_enode(e, num, m_args.data())); return true; } @@ -158,8 +158,9 @@ namespace euf { m_bool_var2expr[v] = e; m_var_trail.push_back(v); enode* n = m_egraph.find(e); - if (!n) - n = m_egraph.mk(e, m_generation, 0, nullptr); + if (!n) { + n = mk_enode(e, 0, nullptr); + } SASSERT(n->bool_var() == sat::null_bool_var || n->bool_var() == v); m_egraph.set_bool_var(n, v); if (m.is_eq(e) || m.is_or(e) || m.is_and(e) || m.is_not(e)) @@ -262,7 +263,7 @@ namespace euf { for (unsigned i = 0; i < sz; ++i) { expr_ref fapp(m.mk_app(f, e->get_arg(i)), m); expr_ref fresh(m.mk_fresh_const("dist-value", u), m); - enode* n = m_egraph.mk(fresh, m_generation, 0, nullptr); + enode* n = mk_enode(fresh, 0, nullptr); n->mark_interpreted(); expr_ref eq = mk_eq(fapp, fresh); sat::literal lit = mk_literal(eq); @@ -334,15 +335,19 @@ namespace euf { // the variable is shared if the equivalence class of n // contains a parent application. - + family_id th_id = m.get_basic_family_id(); for (auto p : euf::enode_th_vars(n)) { - if (m.get_basic_family_id() != p.get_id()) { - th_id = p.get_id(); - break; + family_id id = p.get_id(); + if (m.get_basic_family_id() != id) { + if (th_id != m.get_basic_family_id()) + return true; + th_id = id; } } - + if (m.is_bool(n->get_expr()) && th_id != m.get_basic_family_id()) + return true; + for (enode* parent : euf::enode_parents(n)) { app* p = to_app(parent->get_expr()); family_id fid = p->get_family_id(); @@ -417,4 +422,35 @@ namespace euf { return g; } + euf::enode* solver::e_internalize(expr* e) { + euf::enode* n = m_egraph.find(e); + if (!n) { + internalize(e, m_is_redundant); + n = m_egraph.find(e); + } + return n; + } + + euf::enode* solver::mk_enode(expr* e, unsigned n, enode* const* args) { + euf::enode* r = m_egraph.mk(e, m_generation, n, args); + for (unsigned i = 0; i < n; ++i) + ensure_merged_tf(args[i]); + return r; + } + + void solver::ensure_merged_tf(euf::enode* n) { + switch (n->value()) { + case l_undef: + break; + case l_true: + if (n->get_root() != mk_true()) + m_egraph.merge(n, mk_true(), to_ptr(sat::literal(n->bool_var()))); + break; + case l_false: + if (n->get_root() != mk_false()) + m_egraph.merge(n, mk_false(), to_ptr(~sat::literal(n->bool_var()))); + break; + } + } + } diff --git a/src/sat/smt/euf_model.cpp b/src/sat/smt/euf_model.cpp index 930ca4fed..f0f455f6c 100644 --- a/src/sat/smt/euf_model.cpp +++ b/src/sat/smt/euf_model.cpp @@ -63,6 +63,7 @@ namespace euf { }; void solver::update_model(model_ref& mdl) { + TRACE("model", tout << "create model\n";); mdl->reset_eval_cache(); for (auto* mb : m_solvers) mb->init_model(); @@ -117,7 +118,7 @@ namespace euf { for (enode* n : fresh_values) n->unmark1(); - TRACE("euf", + TRACE("model", for (auto const& d : deps.deps()) if (d.m_value) { tout << bpp(d.m_key) << ":\n"; @@ -188,7 +189,7 @@ namespace euf { else { IF_VERBOSE(1, verbose_stream() << "no model values created for " << mk_pp(e, m) << "\n"); } - } + } } void solver::values2model(deps_t const& deps, model_ref& mdl) { @@ -227,9 +228,12 @@ namespace euf { SASSERT(args.size() == arity); if (!fi->get_entry(args.data())) fi->insert_new_entry(args.data(), v); - TRACE("euf", tout << f->get_name() << "\n"; + TRACE("euf", tout << bpp(n) << " " << f->get_name() << "\n"; for (expr* arg : args) tout << mk_pp(arg, m) << " "; - tout << "\n -> " << mk_pp(v, m) << "\n";); + tout << "\n -> " << mk_pp(v, m) << "\n"; + for (euf::enode* arg : euf::enode_args(n)) tout << bpp(arg) << " "; + tout << "\n"; + ); } } @@ -254,7 +258,7 @@ namespace euf { m_values2root.insert(m_values.get(n->get_expr_id()), n); TRACE("model", for (auto kv : m_values2root) - tout << mk_pp(kv.m_key, m) << " -> " << bpp(kv.m_value) << "\n";); + tout << mk_bounded_pp(kv.m_key, m) << "\n -> " << bpp(kv.m_value) << "\n";); return m_values2root; } @@ -265,17 +269,40 @@ namespace euf { void solver::display_validation_failure(std::ostream& out, model& mdl, enode* n) { out << "Failed to validate " << n->bool_var() << " " << bpp(n) << " " << mdl(n->get_expr()) << "\n"; - for (auto* arg : euf::enode_args(n)) { - expr_ref val = mdl(arg->get_expr()); + euf::enode_vector nodes; + nodes.push_back(n); + for (unsigned i = 0; i < nodes.size(); ++i) { + euf::enode* r = nodes[i]; + if (r->is_marked1()) + continue; + r->mark1(); + for (auto* arg : euf::enode_args(r)) + nodes.push_back(arg); + expr_ref val = mdl(r->get_expr()); expr_ref sval(m); th_rewriter rw(m); rw(val, sval); - out << bpp(arg) << "\n" << sval << "\n"; + out << bpp(r) << " := " << sval << " " << mdl(r->get_root()->get_expr()) << "\n"; } + for (euf::enode* r : nodes) + r->unmark1(); out << mdl << "\n"; + s().display(out); } void solver::validate_model(model& mdl) { + model_evaluator ev(mdl); + ev.set_model_completion(true); + TRACE("model", + for (enode* n : m_egraph.nodes()) { + unsigned id = n->get_root_id(); + expr* val = m_values.get(id, nullptr); + if (!val) + continue; + expr_ref mval = ev(n->get_expr()); + if (m.is_value(mval) && val != mval) + tout << "#" << bpp(n) << " := " << mk_pp(val, m) << " ~ " << mval << "\n"; + }); bool first = true; for (enode* n : m_egraph.nodes()) { expr* e = n->get_expr(); diff --git a/src/sat/smt/euf_solver.cpp b/src/sat/smt/euf_solver.cpp index 5d9b96958..e10225c9c 100644 --- a/src/sat/smt/euf_solver.cpp +++ b/src/sat/smt/euf_solver.cpp @@ -300,7 +300,7 @@ namespace euf { size_t* c = to_ptr(l); SASSERT(is_literal(c)); SASSERT(l == get_literal(c)); - if (n->value_conflict()) { + if (n->value_conflict()) { euf::enode* nb = sign ? mk_false() : mk_true(); euf::enode* r = n->get_root(); euf::enode* rb = sign ? mk_true() : mk_false(); @@ -454,37 +454,67 @@ namespace euf { bool give_up = false; bool cont = false; + if (unit_propagate()) + return sat::check_result::CR_CONTINUE; + if (!init_relevancy()) give_up = true; unsigned num_nodes = m_egraph.num_nodes(); - for (auto* e : m_solvers) { - if (!m.inc()) - return sat::check_result::CR_GIVEUP; - if (e == m_qsolver) - continue; + auto apply_solver = [&](th_solver* e) { switch (e->check()) { case sat::check_result::CR_CONTINUE: cont = true; break; case sat::check_result::CR_GIVEUP: give_up = true; break; default: break; } + }; + if (merge_shared_bools()) + cont = true; + for (auto* e : m_solvers) { + if (!m.inc()) + return sat::check_result::CR_GIVEUP; + if (e == m_qsolver) + continue; + apply_solver(e); if (s().inconsistent()) return sat::check_result::CR_CONTINUE; } + + + if (s().inconsistent()) + return sat::check_result::CR_CONTINUE; if (cont) return sat::check_result::CR_CONTINUE; - if (give_up) - return sat::check_result::CR_GIVEUP; + if (m_qsolver) + apply_solver(m_qsolver); if (num_nodes < m_egraph.num_nodes()) { IF_VERBOSE(1, verbose_stream() << "new nodes created, but not detected\n"); - return sat::check_result::CR_CONTINUE; + return sat::check_result::CR_CONTINUE; } - if (m_qsolver) - return m_qsolver->check(); TRACE("after_search", s().display(tout);); + if (give_up) + return sat::check_result::CR_GIVEUP; return sat::check_result::CR_DONE; } + bool solver::merge_shared_bools() { + bool merged = false; + for (unsigned i = m_egraph.nodes().size(); i-- > 0; ) { + euf::enode* n = m_egraph.nodes()[i]; + if (!is_shared(n) || !m.is_bool(n->get_expr())) + continue; + if (n->value() == l_true && !m.is_true(n->get_root()->get_expr())) { + m_egraph.merge(n, mk_true(), to_ptr(sat::literal(n->bool_var()))); + merged = true; + } + if (n->value() == l_false && !m.is_false(n->get_root()->get_expr())) { + m_egraph.merge(n, mk_false(), to_ptr(~sat::literal(n->bool_var()))); + merged = true; + } + } + return merged; + } + void solver::push() { si.push(); scope s; @@ -564,13 +594,21 @@ namespace euf { TRACE("euf", for (auto const& kv : replay.m) tout << kv.m_value << "\n";); for (auto const& [e, generation, v] : m_reinit) { scoped_generation _sg(*this, generation); - TRACE("euf", tout << "replay: " << v << " " << mk_bounded_pp(e, m) << "\n";); + TRACE("euf", tout << "replay: " << v << " " << e->get_id() << " " << mk_bounded_pp(e, m) << " " << si.is_bool_op(e) << "\n";); sat::literal lit; if (si.is_bool_op(e)) lit = literal(replay.m[e], false); else lit = si.internalize(e, true); - VERIFY(lit.var() == v); + VERIFY(lit.var() == v); + if (!m_egraph.find(e) && (!m.is_iff(e) && !m.is_or(e) && !m.is_and(e) && !m.is_not(e))) { + ptr_buffer args; + if (is_app(e)) + for (expr* arg : *to_app(e)) + args.push_back(e_internalize(arg)); + if (!m_egraph.find(e)) + mk_enode(e, args.size(), args.data()); + } attach_lit(lit, e); } @@ -634,10 +672,10 @@ namespace euf { break; } case OP_TRUE: - add_root(lit); + add_aux(lit); break; case OP_FALSE: - add_root(~lit); + add_aux(~lit); break; case OP_ITE: { auto lit1 = si.internalize(to_app(e)->get_arg(0), true); @@ -826,6 +864,14 @@ namespace euf { }; r->m_egraph.copy_from(m_egraph, copy_justification); r->set_solver(s); + for (euf::enode* n : r->m_egraph.nodes()) { + auto b = n->bool_var(); + if (b != sat::null_bool_var) { + m_bool_var2expr.setx(b, n->get_expr(), nullptr); + SASSERT(r->m.is_bool(n->get_sort())); + IF_VERBOSE(11, verbose_stream() << "set bool_var " << r->bpp(n) << "\n"); + } + } for (auto* s_orig : m_id2solver) { if (s_orig) { auto* s_clone = s_orig->clone(*r); diff --git a/src/sat/smt/euf_solver.h b/src/sat/smt/euf_solver.h index 9a8ab3687..6d08ba512 100644 --- a/src/sat/smt/euf_solver.h +++ b/src/sat/smt/euf_solver.h @@ -127,6 +127,7 @@ namespace euf { void add_not_distinct_axiom(app* e, euf::enode* const* args); void axiomatize_basic(enode* n); bool internalize_root(app* e, bool sign, ptr_vector const& args); + void ensure_merged_tf(euf::enode* n); euf::enode* mk_true(); euf::enode* mk_false(); @@ -165,6 +166,7 @@ namespace euf { bool is_self_propagated(th_eq const& e); void get_antecedents(literal l, constraint& j, literal_vector& r, bool probing); void new_diseq(enode* a, enode* b, literal lit); + bool merge_shared_bools(); // proofs void log_antecedents(std::ostream& out, literal l, literal_vector const& r); @@ -286,6 +288,7 @@ namespace euf { void propagate(literal lit, th_explain* p) { propagate(lit, p->to_index()); } bool propagate(enode* a, enode* b, th_explain* p) { return propagate(a, b, p->to_index()); } + size_t* to_justification(sat::literal l) { return to_ptr(l); } void set_conflict(th_explain* p) { set_conflict(p->to_index()); } bool set_root(literal l, literal r) override; @@ -310,7 +313,7 @@ namespace euf { std::ostream& display(std::ostream& out) const override; std::ostream& display_justification(std::ostream& out, ext_justification_idx idx) const override; std::ostream& display_constraint(std::ostream& out, ext_constraint_idx idx) const override; - euf::egraph::b_pp bpp(enode* n) { return m_egraph.bpp(n); } + euf::egraph::b_pp bpp(enode* n) const { return m_egraph.bpp(n); } clause_pp pp(literal_vector const& lits) { return clause_pp(*this, lits); } void collect_statistics(statistics& st) const override; extension* copy(sat::solver* s) override; @@ -346,9 +349,10 @@ namespace euf { void attach_node(euf::enode* n); expr_ref mk_eq(expr* e1, expr* e2); expr_ref mk_eq(euf::enode* n1, euf::enode* n2) { return mk_eq(n1->get_expr(), n2->get_expr()); } - euf::enode* mk_enode(expr* e, unsigned n, enode* const* args) { return m_egraph.mk(e, m_generation, n, args); } + euf::enode* e_internalize(expr* e); + euf::enode* mk_enode(expr* e, unsigned n, enode* const* args); expr* bool_var2expr(sat::bool_var v) const { return m_bool_var2expr.get(v, nullptr); } - expr_ref literal2expr(sat::literal lit) const { expr* e = bool_var2expr(lit.var()); return lit.sign() ? expr_ref(m.mk_not(e), m) : expr_ref(e, m); } + expr_ref literal2expr(sat::literal lit) const { expr* e = bool_var2expr(lit.var()); return (e && lit.sign()) ? expr_ref(m.mk_not(e), m) : expr_ref(e, m); } unsigned generation() const { return m_generation; } sat::literal attach_lit(sat::literal lit, expr* e); @@ -367,6 +371,7 @@ namespace euf { void add_root(sat::literal a, sat::literal b) { sat::literal lits[2] = {a, b}; add_root(2, lits); } void add_aux(sat::literal_vector const& lits) { add_aux(lits.size(), lits.data()); } void add_aux(unsigned n, sat::literal const* lits); + void add_aux(sat::literal a) { sat::literal lits[1] = { a }; add_aux(1, lits); } void add_aux(sat::literal a, sat::literal b) { sat::literal lits[2] = {a, b}; add_aux(2, lits); } void add_aux(sat::literal a, sat::literal b, sat::literal c) { sat::literal lits[3] = { a, b, c }; add_aux(3, lits); } void track_relevancy(sat::bool_var v); diff --git a/src/sat/smt/q_ematch.cpp b/src/sat/smt/q_ematch.cpp index a2c27fd60..2e779cb80 100644 --- a/src/sat/smt/q_ematch.cpp +++ b/src/sat/smt/q_ematch.cpp @@ -359,17 +359,21 @@ namespace q { for (unsigned i = 0; i < c.num_decls(); ++i) _binding.push_back(binding[i]->get_expr()); var_subst subst(m); + auto sub = [&](expr* e) { + expr_ref r = subst(e, _binding); + //ctx.rewrite(r); + return l.sign ? ~ctx.mk_literal(r) : ctx.mk_literal(r); + }; if (m.is_true(l.rhs)) { SASSERT(!l.sign); - return ctx.mk_literal(subst(l.lhs, _binding)); + return sub(l.lhs); } else if (m.is_false(l.rhs)) { SASSERT(!l.sign); - return ~ctx.mk_literal(subst(l.lhs, _binding)); + return ~sub(l.lhs); } expr_ref fml(m.mk_eq(l.lhs, l.rhs), m); - fml = subst(fml, _binding); - return l.sign ? ~ctx.mk_literal(fml) : ctx.mk_literal(fml); + return sub(fml); } struct ematch::reset_in_queue : public trail { diff --git a/src/sat/smt/q_eval.cpp b/src/sat/smt/q_eval.cpp index b7c07424f..600dcd2c5 100644 --- a/src/sat/smt/q_eval.cpp +++ b/src/sat/smt/q_eval.cpp @@ -181,21 +181,25 @@ namespace q { while (!todo.empty()) { expr* t = todo.back(); SASSERT(!is_ground(t) || ctx.get_egraph().find(t)); - if (is_ground(t) || (has_quantifiers(t) && !has_free_vars(t))) { - m_mark.mark(t); - m_eval.setx(t->get_id(), ctx.get_egraph().find(t), nullptr); - if (!m_eval[t->get_id()]) - return nullptr; - todo.pop_back(); - continue; - } if (m_mark.is_marked(t)) { todo.pop_back(); continue; } - if (is_var(t)) { + if (is_ground(t) || (has_quantifiers(t) && !has_free_vars(t))) { + m_eval.setx(t->get_id(), ctx.get_egraph().find(t), nullptr); + if (!m_eval[t->get_id()]) + return nullptr; m_mark.mark(t); + todo.pop_back(); + continue; + } + if (is_var(t)) { + if (to_var(t)->get_idx() >= n) + return nullptr; m_eval.setx(t->get_id(), binding[n - 1 - to_var(t)->get_idx()], nullptr); + if (!m_eval[t->get_id()]) + return nullptr; + m_mark.mark(t); todo.pop_back(); continue; } diff --git a/src/sat/smt/q_mam.cpp b/src/sat/smt/q_mam.cpp index bd8859575..b1432a5ee 100644 --- a/src/sat/smt/q_mam.cpp +++ b/src/sat/smt/q_mam.cpp @@ -2082,11 +2082,9 @@ namespace q { p = p->get_root(); for (enode* p2 : euf::enode_parents(p)) { if (p2->get_decl() == f && - num_args == n->num_args() && - num_args == p2->num_args() && ctx.is_relevant(p2) && p2->is_cgr() && - i < num_args && + i < p2->num_args() && p2->get_arg(i)->get_root() == p) { v->push_back(p2); } @@ -3333,6 +3331,8 @@ namespace q { } void update_vars(unsigned short var_id, path * p, quantifier * qa, app * mp) { + if (var_id >= qa->get_num_decls()) + return; paths & var_paths = m_var_paths[var_id]; bool found = false; for (path* curr_path : var_paths) { @@ -3558,12 +3558,14 @@ namespace q { // For every application f(x_1, ..., x_n) of a function symbol f, n = f->get_arity(). // Starting at Z3 3.0, this is only true if !f->is_flat_associative(). // Thus, we need the extra checks. - (!is_flat_assoc || (curr_tree->m_arg_idx < curr_parent->num_args() && - curr_tree->m_ground_arg_idx < curr_parent->num_args()))) { + curr_tree->m_arg_idx < curr_parent->num_args() && + (!is_flat_assoc || curr_tree->m_ground_arg_idx < curr_parent->num_args())) { enode * curr_parent_child = curr_parent->get_arg(curr_tree->m_arg_idx)->get_root(); if (// Filter 1. the curr_child is equal to child of the current parent. curr_child == curr_parent_child && - // Filter 2. + // Filter 2. m_ground_arg_idx is a valid argument + curr_tree->m_ground_arg_idx < curr_parent->num_args() && + // Filter 3. ( // curr_tree has no support for the filter based on a ground argument. curr_tree->m_ground_arg == nullptr || @@ -3745,7 +3747,7 @@ namespace q { // However, the simplifier may turn a non-ground pattern into a ground one. // So, we should check it again here. for (expr* arg : *mp) - if (is_ground(arg)) + if (is_ground(arg) || has_quantifiers(arg)) return; // ignore multi-pattern containing ground pattern. update_filters(qa, mp); m_new_patterns.push_back(qp_pair(qa, mp)); diff --git a/src/sat/smt/q_mbi.cpp b/src/sat/smt/q_mbi.cpp index 84859781f..a7a2d67d7 100644 --- a/src/sat/smt/q_mbi.cpp +++ b/src/sat/smt/q_mbi.cpp @@ -448,7 +448,7 @@ namespace q { */ void mbqi::extract_var_args(expr* _t, q_body& qb) { expr_ref t(_t, m); - for (expr* s : subterms(t)) { + for (expr* s : subterms::ground(t)) { if (is_ground(s)) continue; if (is_uninterp(s) && to_app(s)->get_num_args() > 0) { diff --git a/src/sat/smt/q_model_fixer.cpp b/src/sat/smt/q_model_fixer.cpp index 41b6f31fb..3339daf2d 100644 --- a/src/sat/smt/q_model_fixer.cpp +++ b/src/sat/smt/q_model_fixer.cpp @@ -90,6 +90,14 @@ namespace q { univ.append(residue); add_projection_functions(mdl, univ); + for (unsigned i = mdl.get_num_functions(); i-- > 0; ) { + func_decl* f = mdl.get_function(i); + func_interp* fi = mdl.get_func_interp(f); + if (fi->is_partial()) + fi->set_else(fi->get_max_occ_result()); + if (fi->is_partial()) + fi->set_else(mdl.get_some_value(f->get_range())); + } TRACE("q", tout << "end: " << mdl << "\n";); } @@ -235,7 +243,7 @@ namespace q { auto* info = (*this)(q); quantifier* flat_q = info->get_flat_q(); expr_ref body(flat_q->get_expr(), m); - for (expr* t : subterms(body)) + for (expr* t : subterms::ground(body)) if (is_uninterp(t) && !to_app(t)->is_ground()) fns.insert(to_app(t)->get_decl()); } diff --git a/src/sat/smt/recfun_solver.cpp b/src/sat/smt/recfun_solver.cpp index 7bf1d5bc2..be7322a75 100644 --- a/src/sat/smt/recfun_solver.cpp +++ b/src/sat/smt/recfun_solver.cpp @@ -40,7 +40,6 @@ namespace recfun { } void solver::reset() { - m_propagation_queue.reset(); m_stats.reset(); m_disabled_guards.reset(); m_enabled_guards.reset(); @@ -229,7 +228,7 @@ namespace recfun { } void solver::push_prop(propagation_item* p) { - m_propagation_queue.push_back(p); + m_propagation_queue.push_back(p); ctx.push(push_back_vector>(m_propagation_queue)); } @@ -273,7 +272,8 @@ namespace recfun { if (!n) n = mk_enode(e, false); SASSERT(!n->is_attached_to(get_id())); - mk_var(n); + euf::theory_var w = mk_var(n); + ctx.attach_th_var(n, this, w); if (u().is_defined(e) && u().has_defs()) push_case_expand(e); return true; @@ -292,6 +292,8 @@ namespace recfun { s().assign_scoped(assumption); } } + for (expr* g : m_enabled_guards) + push_guard(g); } bool solver::should_research(sat::literal_vector const& core) { @@ -322,14 +324,11 @@ namespace recfun { if (to_delete) { m_disabled_guards.erase(to_delete); m_enabled_guards.push_back(to_delete); - push_guard(to_delete); IF_VERBOSE(2, verbose_stream() << "(smt.recfun :enable-guard " << mk_pp(to_delete, m) << ")\n"); } else { IF_VERBOSE(2, verbose_stream() << "(smt.recfun :increment-round)\n"); } - for (expr* g : m_enabled_guards) - push_guard(g); } return found; } diff --git a/src/sat/smt/sat_dual_solver.cpp b/src/sat/smt/sat_dual_solver.cpp index dcc90ddb0..599caf6e5 100644 --- a/src/sat/smt/sat_dual_solver.cpp +++ b/src/sat/smt/sat_dual_solver.cpp @@ -67,6 +67,7 @@ namespace sat { bool_var w = m_ext2var.get(v, null_bool_var); if (null_bool_var == w) { w = m_solver.mk_var(); + m_solver.set_external(w); m_ext2var.setx(v, w, null_bool_var); m_var2ext.setx(w, v, null_bool_var); m_vars.push_back(v); @@ -103,6 +104,7 @@ namespace sat { root = ext2lit(clause[0]); else { root = literal(m_solver.mk_var(), false); + m_solver.set_external(root.var()); for (unsigned i = 0; i < sz; ++i) m_solver.mk_clause(root, ~ext2lit(clause[i]), status::input()); } diff --git a/src/sat/smt/sat_internalizer.h b/src/sat/smt/sat_internalizer.h new file mode 100644 index 000000000..43413a893 --- /dev/null +++ b/src/sat/smt/sat_internalizer.h @@ -0,0 +1,35 @@ +/*++ +Copyright (c) 2020 Microsoft Corporation + +Module Name: + + sat_internalizer.h + +Abstract: + + Header for SMT theories over SAT solver + +Author: + + Nikolaj Bjorner (nbjorner) 2020-08-25 + +--*/ +#pragma once + +#include "util/sat_literal.h" + +namespace sat { + class sat_internalizer { + public: + virtual ~sat_internalizer() {} + virtual bool is_bool_op(expr* e) const = 0; + virtual literal internalize(expr* e, bool learned) = 0; + virtual bool_var to_bool_var(expr* e) = 0; + virtual bool_var add_bool_var(expr* e) = 0; + virtual void cache(app* t, literal l) = 0; + virtual void uncache(literal l) = 0; + virtual void push() = 0; + virtual void pop(unsigned n) = 0; + virtual void set_expr2var_replay(obj_map* r) = 0; + }; +} diff --git a/src/sat/smt/sat_smt.h b/src/sat/smt/sat_smt.h index 0ba632f63..b509f0a9e 100644 --- a/src/sat/smt/sat_smt.h +++ b/src/sat/smt/sat_smt.h @@ -19,6 +19,7 @@ Author: #include "ast/ast_pp.h" #include "ast/ast_ll_pp.h" #include "sat/sat_solver.h" +#include "sat/smt/sat_internalizer.h" namespace sat { @@ -28,20 +29,6 @@ namespace sat { eframe(expr* e) : m_e(e), m_idx(0) {} }; - class sat_internalizer { - public: - virtual ~sat_internalizer() {} - virtual bool is_bool_op(expr* e) const = 0; - virtual literal internalize(expr* e, bool learned) = 0; - virtual bool_var to_bool_var(expr* e) = 0; - virtual bool_var add_bool_var(expr* e) = 0; - virtual void cache(app* t, literal l) = 0; - virtual void uncache(literal l) = 0; - virtual void push() = 0; - virtual void pop(unsigned n) = 0; - virtual void set_expr2var_replay(obj_map* r) = 0; - }; - class constraint_base { extension* m_ex; unsigned m_mem[0]; diff --git a/src/sat/smt/sat_th.cpp b/src/sat/smt/sat_th.cpp index 1538f9a3b..06efccaf0 100644 --- a/src/sat/smt/sat_th.cpp +++ b/src/sat/smt/sat_th.cpp @@ -218,12 +218,7 @@ namespace euf { } euf::enode* th_euf_solver::e_internalize(expr* e) { - euf::enode* n = expr2enode(e); - if (!n) { - ctx.internalize(e, m_is_redundant); - n = expr2enode(e); - } - return n; + return ctx.e_internalize(e); } unsigned th_euf_solver::random() { diff --git a/src/sat/smt/user_solver.cpp b/src/sat/smt/user_solver.cpp index 8190e3bf7..e9d8a54cb 100644 --- a/src/sat/smt/user_solver.cpp +++ b/src/sat/smt/user_solver.cpp @@ -44,6 +44,7 @@ namespace user { unsigned num_eqs, unsigned const* eq_lhs, unsigned const* eq_rhs, expr* conseq) { m_prop.push_back(prop_info(num_fixed, fixed_ids, num_eqs, eq_lhs, eq_rhs, expr_ref(conseq, m))); + DEBUG_CODE(validate_propagation();); } sat::check_result solver::check() { @@ -95,7 +96,7 @@ namespace user { ctx.push(value_trail(m_qhead)); unsigned np = m_stats.m_num_propagations; for (; m_qhead < m_prop.size() && !s().inconsistent(); ++m_qhead) { - auto const& prop = m_prop[m_qhead]; + auto const& prop = m_prop[m_qhead]; sat::literal lit = ctx.internalize(prop.m_conseq, false, false, true); if (s().value(lit) != l_true) { s().assign(lit, mk_justification(m_qhead)); @@ -126,6 +127,19 @@ namespace user { ctx.add_antecedent(var2enode(p.first), var2enode(p.second)); } + /* + * All assumptions and equalities have to be true in the current scope. + * A caller could mistakingly supply some assumption that isn't set. + */ + void solver::validate_propagation() { + auto const& prop = m_prop.back(); + for (unsigned id : prop.m_ids) + for (auto lit: m_id2justification[id]) + VERIFY(s().value(lit) == l_true); + for (auto const& p : prop.m_eqs) + VERIFY(var2enode(p.first)->get_root() == var2enode(p.second)->get_root()); + } + std::ostream& solver::display(std::ostream& out) const { for (unsigned i = 0; i < get_num_vars(); ++i) out << i << ": " << mk_pp(var2expr(i), m) << "\n"; diff --git a/src/sat/smt/user_solver.h b/src/sat/smt/user_solver.h index 24f4604d1..e16eb5b5e 100644 --- a/src/sat/smt/user_solver.h +++ b/src/sat/smt/user_solver.h @@ -79,6 +79,8 @@ namespace user { sat::justification mk_justification(unsigned propagation_index); + void validate_propagation(); + public: solver(euf::solver& ctx); diff --git a/src/sat/tactic/CMakeLists.txt b/src/sat/tactic/CMakeLists.txt index d1924d679..59e7db1ab 100644 --- a/src/sat/tactic/CMakeLists.txt +++ b/src/sat/tactic/CMakeLists.txt @@ -1,6 +1,7 @@ z3_add_component(sat_tactic SOURCES goal2sat.cpp + sat2goal.cpp sat_tactic.cpp COMPONENT_DEPENDENCIES sat diff --git a/src/sat/tactic/goal2sat.cpp b/src/sat/tactic/goal2sat.cpp index 9be810e9d..bdb37bc79 100644 --- a/src/sat/tactic/goal2sat.cpp +++ b/src/sat/tactic/goal2sat.cpp @@ -251,7 +251,7 @@ struct goal2sat::imp : public sat::sat_internalizer { return; } n -= m_num_scopes; - m_num_scopes = 0; + m_num_scopes = 0; m_map.pop(n); unsigned k = m_cache_lim[m_cache_lim.size() - n]; for (unsigned i = m_cache_trail.size(); i-- > k; ) { @@ -284,7 +284,7 @@ struct goal2sat::imp : public sat::sat_internalizer { m_cache_trail.push_back(t); } - void convert_atom(expr * t, bool root, bool sign) { + void convert_atom(expr * t, bool root, bool sign) { SASSERT(m.is_bool(t)); sat::literal l; sat::bool_var v = m_map.to_bool_var(t); @@ -954,9 +954,11 @@ struct goal2sat::imp : public sat::sat_internalizer { } void user_push() { + push(); } void user_pop(unsigned n) { + pop(n); } }; @@ -1010,15 +1012,7 @@ void goal2sat::operator()(goal const & g, params_ref const & p, sat::solver_core for (unsigned i = 0; i < m_scopes; ++i) m_imp->user_push(); } - (*m_imp)(g); - - if (!t.get_extension() && m_imp->interpreted_funs().empty()) { - dealloc(m_imp); - m_imp = nullptr; - } - else - m_scopes = 0; - + (*m_imp)(g); } void goal2sat::get_interpreted_funs(func_decl_ref_vector& funs) { @@ -1059,290 +1053,3 @@ sat::sat_internalizer& goal2sat::si(ast_manager& m, params_ref const& p, sat::so m_imp = alloc(imp, m, p, t, a2b, dep2asm, default_external); return *m_imp; } - - - -sat2goal::mc::mc(ast_manager& m): m(m), m_var2expr(m) {} - -void sat2goal::mc::flush_smc(sat::solver_core& s, atom2bool_var const& map) { - s.flush(m_smc); - m_var2expr.resize(s.num_vars()); - map.mk_var_inv(m_var2expr); - flush_gmc(); -} - -void sat2goal::mc::flush_gmc() { - sat::literal_vector updates; - m_smc.expand(updates); - if (!m_gmc) m_gmc = alloc(generic_model_converter, m, "sat2goal"); - // now gmc owns the model converter - sat::literal_vector clause; - expr_ref_vector tail(m); - expr_ref def(m); - auto is_literal = [&](expr* e) { expr* r; return is_uninterp_const(e) || (m.is_not(e, r) && is_uninterp_const(r)); }; - - for (unsigned i = 0; i < updates.size(); ++i) { - sat::literal l = updates[i]; - if (l == sat::null_literal) { - sat::literal lit0 = clause[0]; - for (unsigned i = 1; i < clause.size(); ++i) { - tail.push_back(lit2expr(~clause[i])); - } - def = m.mk_or(lit2expr(lit0), mk_and(tail)); - if (lit0.sign()) { - lit0.neg(); - def = m.mk_not(def); - } - expr_ref e = lit2expr(lit0); - if (is_literal(e)) - m_gmc->add(e, def); - clause.reset(); - tail.reset(); - } - // short circuit for equivalences: - else if (clause.empty() && tail.empty() && - i + 5 < updates.size() && - updates[i] == ~updates[i + 3] && - updates[i + 1] == ~updates[i + 4] && - updates[i + 2] == sat::null_literal && - updates[i + 5] == sat::null_literal) { - sat::literal r = ~updates[i+1]; - if (l.sign()) { - l.neg(); - r.neg(); - } - - expr* a = lit2expr(l); - if (is_literal(a)) - m_gmc->add(a, lit2expr(r)); - i += 5; - } - else { - clause.push_back(l); - } - } -} - -model_converter* sat2goal::mc::translate(ast_translation& translator) { - mc* result = alloc(mc, translator.to()); - result->m_smc.copy(m_smc); - result->m_gmc = m_gmc ? dynamic_cast(m_gmc->translate(translator)) : nullptr; - for (expr* e : m_var2expr) { - result->m_var2expr.push_back(translator(e)); - } - return result; -} - -void sat2goal::mc::set_env(ast_pp_util* visitor) { - flush_gmc(); - if (m_gmc) m_gmc->set_env(visitor); -} - -void sat2goal::mc::display(std::ostream& out) { - flush_gmc(); - if (m_gmc) m_gmc->display(out); -} - -void sat2goal::mc::get_units(obj_map& units) { - flush_gmc(); - if (m_gmc) m_gmc->get_units(units); -} - - -void sat2goal::mc::operator()(sat::model& md) { - m_smc(md); -} - -void sat2goal::mc::operator()(model_ref & md) { - // apply externalized model converter - CTRACE("sat_mc", m_gmc, m_gmc->display(tout << "before sat_mc\n"); model_v2_pp(tout, *md);); - if (m_gmc) (*m_gmc)(md); - CTRACE("sat_mc", m_gmc, m_gmc->display(tout << "after sat_mc\n"); model_v2_pp(tout, *md);); -} - - -void sat2goal::mc::operator()(expr_ref& fml) { - flush_gmc(); - if (m_gmc) (*m_gmc)(fml); -} - -void sat2goal::mc::insert(sat::bool_var v, expr * atom, bool aux) { - SASSERT(!m_var2expr.get(v, nullptr)); - m_var2expr.reserve(v + 1); - m_var2expr.set(v, atom); - if (aux) { - SASSERT(m.is_bool(atom)); - if (!m_gmc) m_gmc = alloc(generic_model_converter, m, "sat2goal"); - if (is_uninterp_const(atom)) - m_gmc->hide(to_app(atom)->get_decl()); - } - TRACE("sat_mc", tout << "insert " << v << "\n";); -} - -expr_ref sat2goal::mc::lit2expr(sat::literal l) { - sat::bool_var v = l.var(); - if (!m_var2expr.get(v)) { - app* aux = m.mk_fresh_const(nullptr, m.mk_bool_sort()); - m_var2expr.set(v, aux); - if (!m_gmc) m_gmc = alloc(generic_model_converter, m, "sat2goal"); - m_gmc->hide(aux->get_decl()); - } - VERIFY(m_var2expr.get(v)); - expr_ref result(m_var2expr.get(v), m); - if (l.sign()) { - result = m.mk_not(result); - } - return result; -} - - -struct sat2goal::imp { - - typedef mc sat_model_converter; - - ast_manager & m; - expr_ref_vector m_lit2expr; - unsigned long long m_max_memory; - bool m_learned; - - imp(ast_manager & _m, params_ref const & p):m(_m), m_lit2expr(m) { - updt_params(p); - } - - void updt_params(params_ref const & p) { - m_learned = p.get_bool("learned", false); - m_max_memory = megabytes_to_bytes(p.get_uint("max_memory", UINT_MAX)); - } - - void checkpoint() { - if (!m.inc()) - throw tactic_exception(m.limit().get_cancel_msg()); - if (memory::get_allocation_size() > m_max_memory) - throw tactic_exception(TACTIC_MAX_MEMORY_MSG); - } - - expr * lit2expr(ref& mc, sat::literal l) { - if (!m_lit2expr.get(l.index())) { - SASSERT(m_lit2expr.get((~l).index()) == 0); - expr* aux = mc ? mc->var2expr(l.var()) : nullptr; - if (!aux) { - aux = m.mk_fresh_const(nullptr, m.mk_bool_sort()); - if (mc) { - mc->insert(l.var(), aux, true); - } - } - sat::literal lit(l.var(), false); - m_lit2expr.set(lit.index(), aux); - m_lit2expr.set((~lit).index(), m.mk_not(aux)); - } - return m_lit2expr.get(l.index()); - } - - void assert_clauses(ref& mc, sat::solver_core const & s, sat::clause_vector const& clauses, goal & r, bool asserted) { - ptr_buffer lits; - unsigned small_lbd = 3; // s.get_config().m_gc_small_lbd; - for (sat::clause* cp : clauses) { - checkpoint(); - lits.reset(); - sat::clause const & c = *cp; - if (asserted || m_learned || c.glue() <= small_lbd) { - for (sat::literal l : c) { - lits.push_back(lit2expr(mc, l)); - } - r.assert_expr(m.mk_or(lits)); - } - } - } - - void operator()(sat::solver_core & s, atom2bool_var const & map, goal & r, ref & mc) { - if (s.at_base_lvl() && s.inconsistent()) { - r.assert_expr(m.mk_false()); - return; - } - if (r.models_enabled() && !mc) { - mc = alloc(sat_model_converter, m); - } - if (mc) mc->flush_smc(s, map); - m_lit2expr.resize(s.num_vars() * 2); - map.mk_inv(m_lit2expr); - // collect units - unsigned trail_sz = s.init_trail_size(); - for (unsigned i = 0; i < trail_sz; ++i) { - checkpoint(); - r.assert_expr(lit2expr(mc, s.trail_literal(i))); - } - // collect binary clauses - svector bin_clauses; - s.collect_bin_clauses(bin_clauses, m_learned, false); - for (sat::solver::bin_clause const& bc : bin_clauses) { - checkpoint(); - r.assert_expr(m.mk_or(lit2expr(mc, bc.first), lit2expr(mc, bc.second))); - } - // collect clauses - assert_clauses(mc, s, s.clauses(), r, true); - - auto* ext = s.get_extension(); - if (ext) { - std::function l2e = [&](sat::literal lit) { - return expr_ref(lit2expr(mc, lit), m); - }; - expr_ref_vector fmls(m); - pb::solver* ba = dynamic_cast(ext); - if (ba) { - ba->to_formulas(l2e, fmls); - } - else - dynamic_cast(ext)->to_formulas(l2e, fmls); - for (expr* f : fmls) - r.assert_expr(f); - } - } - - void add_clause(ref& mc, sat::literal_vector const& lits, expr_ref_vector& lemmas) { - expr_ref_vector lemma(m); - for (sat::literal l : lits) { - expr* e = lit2expr(mc, l); - if (!e) return; - lemma.push_back(e); - } - lemmas.push_back(mk_or(lemma)); - } - - void add_clause(ref& mc, sat::clause const& c, expr_ref_vector& lemmas) { - expr_ref_vector lemma(m); - for (sat::literal l : c) { - expr* e = lit2expr(mc, l); - if (!e) return; - lemma.push_back(e); - } - lemmas.push_back(mk_or(lemma)); - } - -}; - -sat2goal::sat2goal():m_imp(nullptr) { -} - -void sat2goal::collect_param_descrs(param_descrs & r) { - insert_max_memory(r); - r.insert("learned", CPK_BOOL, "(default: false) collect also learned clauses."); -} - -struct sat2goal::scoped_set_imp { - sat2goal * m_owner; - scoped_set_imp(sat2goal * o, sat2goal::imp * i):m_owner(o) { - m_owner->m_imp = i; - } - ~scoped_set_imp() { - m_owner->m_imp = nullptr; - } -}; - -void sat2goal::operator()(sat::solver_core & t, atom2bool_var const & m, params_ref const & p, - goal & g, ref & mc) { - imp proc(g.m(), p); - scoped_set_imp set(this, &proc); - proc(t, m, g, mc); -} - - diff --git a/src/sat/tactic/goal2sat.h b/src/sat/tactic/goal2sat.h index bc6b8dcb1..8b344c9c3 100644 --- a/src/sat/tactic/goal2sat.h +++ b/src/sat/tactic/goal2sat.h @@ -29,11 +29,9 @@ Notes: #pragma once #include "tactic/goal.h" -#include "sat/sat_solver.h" -#include "tactic/model_converter.h" -#include "tactic/generic_model_converter.h" +#include "sat/sat_solver_core.h" #include "sat/smt/atom2bool_var.h" -#include "sat/smt/sat_smt.h" +#include "sat/smt/sat_internalizer.h" class goal2sat { struct imp; @@ -77,54 +75,3 @@ public: void user_pop(unsigned n); }; - - -class sat2goal { - struct imp; - imp * m_imp; - struct scoped_set_imp; -public: - - class mc : public model_converter { - ast_manager& m; - sat::model_converter m_smc; - generic_model_converter_ref m_gmc; - expr_ref_vector m_var2expr; - - // flushes from m_smc to m_gmc; - void flush_gmc(); - - public: - mc(ast_manager& m); - ~mc() override {} - // flush model converter from SAT solver to this structure. - void flush_smc(sat::solver_core& s, atom2bool_var const& map); - void operator()(sat::model& m); - void operator()(model_ref& md) override; - void operator()(expr_ref& fml) override; - model_converter* translate(ast_translation& translator) override; - void set_env(ast_pp_util* visitor) override; - void display(std::ostream& out) override; - void get_units(obj_map& units) override; - expr* var2expr(sat::bool_var v) const { return m_var2expr.get(v, nullptr); } - expr_ref lit2expr(sat::literal l); - void insert(sat::bool_var v, expr * atom, bool aux); - }; - - sat2goal(); - - - static void collect_param_descrs(param_descrs & r); - - /** - \brief Translate the state of the SAT engine back into a goal. - The SAT solver may use variables that are not in \c m. The translator - creates fresh boolean AST variables for them. They are stored in fvars. - - \warning conversion throws a tactic_exception, if it is interrupted (by set_cancel), - or memory consumption limit is reached (set with param :max-memory). - */ - void operator()(sat::solver_core & t, atom2bool_var const & m, params_ref const & p, goal & s, ref & mc); - -}; - diff --git a/src/sat/tactic/sat2goal.cpp b/src/sat/tactic/sat2goal.cpp new file mode 100644 index 000000000..482e441ef --- /dev/null +++ b/src/sat/tactic/sat2goal.cpp @@ -0,0 +1,331 @@ +/*++ +Copyright (c) 2011 Microsoft Corporation + +Module Name: + + sat2goal.cpp + +Abstract: + + "Compile" a goal into the SAT engine. + Atoms are "abstracted" into boolean variables. + The mapping between boolean variables and atoms + can be used to convert back the state of the + SAT engine into a goal. + + The idea is to support scenarios such as: + 1) simplify, blast, convert into SAT, and solve + 2) convert into SAT, apply SAT for a while, learn new units, and translate back into a goal. + 3) convert into SAT, apply SAT preprocessor (failed literal propagation, resolution, etc) and translate back into a goal. + 4) Convert boolean structure into SAT, convert atoms into another engine, combine engines using lazy combination, solve. + +Author: + + Leonardo (leonardo) 2011-10-26 + +Notes: + +--*/ +#include "util/ref_util.h" +#include "ast/ast_smt2_pp.h" +#include "ast/ast_pp.h" +#include "ast/ast_smt2_pp.h" +#include "ast/ast_ll_pp.h" +#include "ast/pb_decl_plugin.h" +#include "ast/ast_util.h" +#include "ast/for_each_expr.h" +#include "model/model_evaluator.h" +#include "model/model_v2_pp.h" +#include "tactic/tactic.h" +#include "tactic/generic_model_converter.h" +#include "sat/sat_cut_simplifier.h" +#include "sat/sat_drat.h" +#include "sat/tactic/sat2goal.h" +#include "sat/smt/pb_solver.h" +#include "sat/smt/euf_solver.h" +#include "sat/smt/sat_th.h" +#include "sat/sat_params.hpp" +#include + +sat2goal::mc::mc(ast_manager& m): m(m), m_var2expr(m) {} + +void sat2goal::mc::flush_smc(sat::solver& s, atom2bool_var const& map) { + s.flush(m_smc); + m_var2expr.resize(s.num_vars()); + map.mk_var_inv(m_var2expr); + flush_gmc(); +} + +void sat2goal::mc::flush_gmc() { + sat::literal_vector updates; + m_smc.expand(updates); + if (!m_gmc) m_gmc = alloc(generic_model_converter, m, "sat2goal"); + // now gmc owns the model converter + sat::literal_vector clause; + expr_ref_vector tail(m); + expr_ref def(m); + auto is_literal = [&](expr* e) { expr* r; return is_uninterp_const(e) || (m.is_not(e, r) && is_uninterp_const(r)); }; + + for (unsigned i = 0; i < updates.size(); ++i) { + sat::literal l = updates[i]; + if (l == sat::null_literal) { + sat::literal lit0 = clause[0]; + for (unsigned i = 1; i < clause.size(); ++i) { + tail.push_back(lit2expr(~clause[i])); + } + def = m.mk_or(lit2expr(lit0), mk_and(tail)); + if (lit0.sign()) { + lit0.neg(); + def = m.mk_not(def); + } + expr_ref e = lit2expr(lit0); + if (is_literal(e)) + m_gmc->add(e, def); + clause.reset(); + tail.reset(); + } + // short circuit for equivalences: + else if (clause.empty() && tail.empty() && + i + 5 < updates.size() && + updates[i] == ~updates[i + 3] && + updates[i + 1] == ~updates[i + 4] && + updates[i + 2] == sat::null_literal && + updates[i + 5] == sat::null_literal) { + sat::literal r = ~updates[i+1]; + if (l.sign()) { + l.neg(); + r.neg(); + } + + expr* a = lit2expr(l); + if (is_literal(a)) + m_gmc->add(a, lit2expr(r)); + i += 5; + } + else { + clause.push_back(l); + } + } +} + +model_converter* sat2goal::mc::translate(ast_translation& translator) { + mc* result = alloc(mc, translator.to()); + result->m_smc.copy(m_smc); + result->m_gmc = m_gmc ? dynamic_cast(m_gmc->translate(translator)) : nullptr; + for (expr* e : m_var2expr) { + result->m_var2expr.push_back(translator(e)); + } + return result; +} + +void sat2goal::mc::set_env(ast_pp_util* visitor) { + flush_gmc(); + if (m_gmc) m_gmc->set_env(visitor); +} + +void sat2goal::mc::display(std::ostream& out) { + flush_gmc(); + if (m_gmc) m_gmc->display(out); +} + +void sat2goal::mc::get_units(obj_map& units) { + flush_gmc(); + if (m_gmc) m_gmc->get_units(units); +} + + +void sat2goal::mc::operator()(sat::model& md) { + m_smc(md); +} + +void sat2goal::mc::operator()(model_ref & md) { + // apply externalized model converter + CTRACE("sat_mc", m_gmc, m_gmc->display(tout << "before sat_mc\n"); model_v2_pp(tout, *md);); + if (m_gmc) (*m_gmc)(md); + CTRACE("sat_mc", m_gmc, m_gmc->display(tout << "after sat_mc\n"); model_v2_pp(tout, *md);); +} + + +void sat2goal::mc::operator()(expr_ref& fml) { + flush_gmc(); + if (m_gmc) (*m_gmc)(fml); +} + +void sat2goal::mc::insert(sat::bool_var v, expr * atom, bool aux) { + SASSERT(!m_var2expr.get(v, nullptr)); + m_var2expr.reserve(v + 1); + m_var2expr.set(v, atom); + if (aux) { + SASSERT(m.is_bool(atom)); + if (!m_gmc) m_gmc = alloc(generic_model_converter, m, "sat2goal"); + if (is_uninterp_const(atom)) + m_gmc->hide(to_app(atom)->get_decl()); + } + TRACE("sat_mc", tout << "insert " << v << "\n";); +} + +expr_ref sat2goal::mc::lit2expr(sat::literal l) { + sat::bool_var v = l.var(); + if (!m_var2expr.get(v)) { + app* aux = m.mk_fresh_const(nullptr, m.mk_bool_sort()); + m_var2expr.set(v, aux); + if (!m_gmc) m_gmc = alloc(generic_model_converter, m, "sat2goal"); + m_gmc->hide(aux->get_decl()); + } + VERIFY(m_var2expr.get(v)); + expr_ref result(m_var2expr.get(v), m); + if (l.sign()) { + result = m.mk_not(result); + } + return result; +} + + +struct sat2goal::imp { + + typedef mc sat_model_converter; + + ast_manager & m; + expr_ref_vector m_lit2expr; + unsigned long long m_max_memory; + bool m_learned; + + imp(ast_manager & _m, params_ref const & p):m(_m), m_lit2expr(m) { + updt_params(p); + } + + void updt_params(params_ref const & p) { + m_learned = p.get_bool("learned", false); + m_max_memory = megabytes_to_bytes(p.get_uint("max_memory", UINT_MAX)); + } + + void checkpoint() { + if (!m.inc()) + throw tactic_exception(m.limit().get_cancel_msg()); + if (memory::get_allocation_size() > m_max_memory) + throw tactic_exception(TACTIC_MAX_MEMORY_MSG); + } + + expr * lit2expr(ref& mc, sat::literal l) { + if (!m_lit2expr.get(l.index())) { + SASSERT(m_lit2expr.get((~l).index()) == 0); + expr* aux = mc ? mc->var2expr(l.var()) : nullptr; + if (!aux) { + aux = m.mk_fresh_const(nullptr, m.mk_bool_sort()); + if (mc) { + mc->insert(l.var(), aux, true); + } + } + sat::literal lit(l.var(), false); + m_lit2expr.set(lit.index(), aux); + m_lit2expr.set((~lit).index(), m.mk_not(aux)); + } + return m_lit2expr.get(l.index()); + } + + void assert_clauses(ref& mc, sat::solver const & s, sat::clause_vector const& clauses, goal & r, bool asserted) { + ptr_buffer lits; + unsigned small_lbd = 3; // s.get_config().m_gc_small_lbd; + for (sat::clause* cp : clauses) { + checkpoint(); + lits.reset(); + sat::clause const & c = *cp; + if (asserted || m_learned || c.glue() <= small_lbd) { + for (sat::literal l : c) { + lits.push_back(lit2expr(mc, l)); + } + r.assert_expr(m.mk_or(lits)); + } + } + } + + void operator()(sat::solver & s, atom2bool_var const & map, goal & r, ref & mc) { + if (s.at_base_lvl() && s.inconsistent()) { + r.assert_expr(m.mk_false()); + return; + } + if (r.models_enabled() && !mc) { + mc = alloc(sat_model_converter, m); + } + if (mc) mc->flush_smc(s, map); + m_lit2expr.resize(s.num_vars() * 2); + map.mk_inv(m_lit2expr); + // collect units + unsigned trail_sz = s.init_trail_size(); + for (unsigned i = 0; i < trail_sz; ++i) { + checkpoint(); + r.assert_expr(lit2expr(mc, s.trail_literal(i))); + } + // collect binary clauses + svector bin_clauses; + s.collect_bin_clauses(bin_clauses, m_learned, false); + for (sat::solver::bin_clause const& bc : bin_clauses) { + checkpoint(); + r.assert_expr(m.mk_or(lit2expr(mc, bc.first), lit2expr(mc, bc.second))); + } + // collect clauses + assert_clauses(mc, s, s.clauses(), r, true); + + auto* ext = s.get_extension(); + if (ext) { + std::function l2e = [&](sat::literal lit) { + return expr_ref(lit2expr(mc, lit), m); + }; + expr_ref_vector fmls(m); + pb::solver* ba = dynamic_cast(ext); + if (ba) { + ba->to_formulas(l2e, fmls); + } + else + dynamic_cast(ext)->to_formulas(l2e, fmls); + for (expr* f : fmls) + r.assert_expr(f); + } + } + + void add_clause(ref& mc, sat::literal_vector const& lits, expr_ref_vector& lemmas) { + expr_ref_vector lemma(m); + for (sat::literal l : lits) { + expr* e = lit2expr(mc, l); + if (!e) return; + lemma.push_back(e); + } + lemmas.push_back(mk_or(lemma)); + } + + void add_clause(ref& mc, sat::clause const& c, expr_ref_vector& lemmas) { + expr_ref_vector lemma(m); + for (sat::literal l : c) { + expr* e = lit2expr(mc, l); + if (!e) return; + lemma.push_back(e); + } + lemmas.push_back(mk_or(lemma)); + } + +}; + +sat2goal::sat2goal():m_imp(nullptr) { +} + +void sat2goal::collect_param_descrs(param_descrs & r) { + insert_max_memory(r); + r.insert("learned", CPK_BOOL, "(default: false) collect also learned clauses."); +} + +struct sat2goal::scoped_set_imp { + sat2goal * m_owner; + scoped_set_imp(sat2goal * o, sat2goal::imp * i):m_owner(o) { + m_owner->m_imp = i; + } + ~scoped_set_imp() { + m_owner->m_imp = nullptr; + } +}; + +void sat2goal::operator()(sat::solver & t, atom2bool_var const & m, params_ref const & p, + goal & g, ref & mc) { + imp proc(g.m(), p); + scoped_set_imp set(this, &proc); + proc(t, m, g, mc); +} diff --git a/src/sat/tactic/sat2goal.h b/src/sat/tactic/sat2goal.h new file mode 100644 index 000000000..b911f7b47 --- /dev/null +++ b/src/sat/tactic/sat2goal.h @@ -0,0 +1,84 @@ +/*++ +Copyright (c) 2011 Microsoft Corporation + +Module Name: + + sat2goal.h + +Abstract: + + "Compile" a goal into the SAT engine. + Atoms are "abstracted" into boolean variables. + The mapping between boolean variables and atoms + can be used to convert back the state of the + SAT engine into a goal. + + The idea is to support scenarios such as: + 1) simplify, blast, convert into SAT, and solve + 2) convert into SAT, apply SAT for a while, learn new units, and translate back into a goal. + 3) convert into SAT, apply SAT preprocessor (failed literal propagation, resolution, etc) and translate back into a goal. + 4) Convert boolean structure into SAT, convert atoms into another engine, combine engines using lazy combination, solve. + +Author: + + Leonardo (leonardo) 2011-10-26 + +Notes: + +--*/ +#pragma once + +#include "tactic/goal.h" +#include "sat/sat_model_converter.h" +#include "sat/sat_solver.h" +#include "tactic/generic_model_converter.h" +#include "sat/smt/atom2bool_var.h" + +class sat2goal { + struct imp; + imp * m_imp; + struct scoped_set_imp; +public: + + class mc : public model_converter { + ast_manager& m; + sat::model_converter m_smc; + generic_model_converter_ref m_gmc; + expr_ref_vector m_var2expr; + + // flushes from m_smc to m_gmc; + void flush_gmc(); + + public: + mc(ast_manager& m); + ~mc() override {} + // flush model converter from SAT solver to this structure. + void flush_smc(sat::solver& s, atom2bool_var const& map); + void operator()(sat::model& m); + void operator()(model_ref& md) override; + void operator()(expr_ref& fml) override; + model_converter* translate(ast_translation& translator) override; + void set_env(ast_pp_util* visitor) override; + void display(std::ostream& out) override; + void get_units(obj_map& units) override; + expr* var2expr(sat::bool_var v) const { return m_var2expr.get(v, nullptr); } + expr_ref lit2expr(sat::literal l); + void insert(sat::bool_var v, expr * atom, bool aux); + }; + + sat2goal(); + + + static void collect_param_descrs(param_descrs & r); + + /** + \brief Translate the state of the SAT engine back into a goal. + The SAT solver may use variables that are not in \c m. The translator + creates fresh boolean AST variables for them. They are stored in fvars. + + \warning conversion throws a tactic_exception, if it is interrupted (by set_cancel), + or memory consumption limit is reached (set with param :max-memory). + */ + void operator()(sat::solver & t, atom2bool_var const & m, params_ref const & p, goal & s, ref & mc); + +}; diff --git a/src/sat/tactic/sat_tactic.cpp b/src/sat/tactic/sat_tactic.cpp index c8c009bbf..521a70fb7 100644 --- a/src/sat/tactic/sat_tactic.cpp +++ b/src/sat/tactic/sat_tactic.cpp @@ -20,6 +20,7 @@ Notes: #include "model/model_v2_pp.h" #include "tactic/tactical.h" #include "sat/tactic/goal2sat.h" +#include "sat/tactic/sat2goal.h" #include "sat/sat_solver.h" #include "sat/sat_params.hpp" @@ -29,7 +30,7 @@ class sat_tactic : public tactic { ast_manager & m; goal2sat m_goal2sat; sat2goal m_sat2goal; - scoped_ptr m_solver; + scoped_ptr m_solver; params_ref m_params; imp(ast_manager & _m, params_ref const & p): diff --git a/src/shell/dimacs_frontend.cpp b/src/shell/dimacs_frontend.cpp index ec157a291..a5d562440 100644 --- a/src/shell/dimacs_frontend.cpp +++ b/src/shell/dimacs_frontend.cpp @@ -26,6 +26,7 @@ Revision History: #include "sat/sat_params.hpp" #include "sat/sat_solver.h" #include "sat/tactic/goal2sat.h" +#include "sat/tactic/sat2goal.h" #include "ast/reg_decl_plugins.h" #include "tactic/tactic.h" #include "tactic/fd_solver/fd_solver.h" diff --git a/src/smt/mam.cpp b/src/smt/mam.cpp index 0d09f07ea..bc97daed2 100644 --- a/src/smt/mam.cpp +++ b/src/smt/mam.cpp @@ -2109,11 +2109,9 @@ namespace { for (; it2 != end2; ++it2) { enode * p2 = *it2; if (p2->get_decl() == f && - num_args == n->get_num_args() && - num_args == p2->get_num_args() && m_context.is_relevant(p2) && p2->is_cgr() && - i < num_args && + i < p2->get_num_args() && p2->get_arg(i)->get_root() == p) { v->push_back(p2); } diff --git a/src/smt/params/dyn_ack_params.h b/src/smt/params/dyn_ack_params.h index ce5a685bf..81211e9cd 100644 --- a/src/smt/params/dyn_ack_params.h +++ b/src/smt/params/dyn_ack_params.h @@ -27,21 +27,15 @@ enum class dyn_ack_strategy { }; struct dyn_ack_params { - dyn_ack_strategy m_dack; - bool m_dack_eq; - double m_dack_factor; - unsigned m_dack_threshold; - unsigned m_dack_gc; - double m_dack_gc_inv_decay; + dyn_ack_strategy m_dack = dyn_ack_strategy::DACK_ROOT; + bool m_dack_eq = false; + double m_dack_factor = 0.1; + unsigned m_dack_threshold = 10; + unsigned m_dack_gc = 2000; + double m_dack_gc_inv_decay = 0.8; public: - dyn_ack_params(params_ref const & p = params_ref()) : - m_dack(dyn_ack_strategy::DACK_ROOT), - m_dack_eq(false), - m_dack_factor(0.1), - m_dack_threshold(10), - m_dack_gc(2000), - m_dack_gc_inv_decay(0.8) { + dyn_ack_params(params_ref const & p = params_ref()) { updt_params(p); } diff --git a/src/smt/params/smt_params_helper.pyg b/src/smt/params/smt_params_helper.pyg index f0a715e96..20839ea8a 100644 --- a/src/smt/params/smt_params_helper.pyg +++ b/src/smt/params/smt_params_helper.pyg @@ -74,7 +74,6 @@ def_module_params(module_name='smt', ('arith.nl.delay', UINT, 500, 'number of calls to final check before invoking bounded nlsat check'), ('arith.propagate_eqs', BOOL, True, 'propagate (cheap) equalities'), ('arith.propagation_mode', UINT, 1, '0 - no propagation, 1 - propagate existing literals, 2 - refine finite bounds'), - ('arith.reflect', BOOL, True, 'reflect arithmetical operators to the congruence closure'), ('arith.branch_cut_ratio', UINT, 2, 'branch/cut ratio for linear integer arithmetic'), ('arith.int_eq_branch', BOOL, False, 'branching using derived integer equations'), ('arith.ignore_int', BOOL, False, 'treat integer variables as real'), diff --git a/src/smt/params/theory_arith_params.cpp b/src/smt/params/theory_arith_params.cpp index 6906c5940..deec4e4da 100644 --- a/src/smt/params/theory_arith_params.cpp +++ b/src/smt/params/theory_arith_params.cpp @@ -35,7 +35,6 @@ void theory_arith_params::updt_params(params_ref const & _p) { m_arith_ignore_int = p.arith_ignore_int(); m_arith_bound_prop = static_cast(p.arith_propagation_mode()); m_arith_dump_lemmas = p.arith_dump_lemmas(); - m_arith_reflect = p.arith_reflect(); m_arith_eager_eq_axioms = p.arith_eager_eq_axioms(); m_arith_auto_config_simplex = p.arith_auto_config_simplex(); diff --git a/src/smt/params/theory_arith_params.h b/src/smt/params/theory_arith_params.h index 623f91fd0..d45a902db 100644 --- a/src/smt/params/theory_arith_params.h +++ b/src/smt/params/theory_arith_params.h @@ -51,110 +51,64 @@ enum class arith_pivot_strategy { inline std::ostream& operator<<(std::ostream& out, arith_pivot_strategy st) { return out << (int)st; } struct theory_arith_params { - bool m_arith_eq2ineq; - bool m_arith_process_all_eqs; - arith_solver_id m_arith_mode; - bool m_arith_auto_config_simplex; //!< force simplex solver in auto_config - unsigned m_arith_blands_rule_threshold; - bool m_arith_propagate_eqs; - bound_prop_mode m_arith_bound_prop; - bool m_arith_stronger_lemmas; - bool m_arith_skip_rows_with_big_coeffs; - unsigned m_arith_max_lemma_size; - unsigned m_arith_small_lemma_size; - bool m_arith_reflect; - bool m_arith_ignore_int; - unsigned m_arith_lazy_pivoting_lvl; - unsigned m_arith_random_seed; - bool m_arith_random_initial_value; - int m_arith_random_lower; - int m_arith_random_upper; - bool m_arith_adaptive; - double m_arith_adaptive_assertion_threshold; - double m_arith_adaptive_propagation_threshold; - bool m_arith_dump_lemmas; - bool m_arith_eager_eq_axioms; - unsigned m_arith_branch_cut_ratio; - bool m_arith_int_eq_branching; - bool m_arith_enum_const_mod; + bool m_arith_eq2ineq = false; + bool m_arith_process_all_eqs = false; + arith_solver_id m_arith_mode = arith_solver_id::AS_NEW_ARITH; + bool m_arith_auto_config_simplex = false; //!< force simplex solver in auto_config + unsigned m_arith_blands_rule_threshold = 1000; + bool m_arith_propagate_eqs = true; + bound_prop_mode m_arith_bound_prop = bound_prop_mode::BP_REFINE; + bool m_arith_stronger_lemmas = true; + bool m_arith_skip_rows_with_big_coeffs = true; + unsigned m_arith_max_lemma_size = 128; + unsigned m_arith_small_lemma_size = 16; + bool m_arith_reflect = true; + bool m_arith_ignore_int = false; + unsigned m_arith_lazy_pivoting_lvl = 0; + unsigned m_arith_random_seed = 0; + bool m_arith_random_initial_value = false; + int m_arith_random_lower = -1000; + int m_arith_random_upper = 1000; + bool m_arith_adaptive = false; + double m_arith_adaptive_assertion_threshold = 0.2; + double m_arith_adaptive_propagation_threshold = 0.4; + bool m_arith_dump_lemmas = false; + bool m_arith_eager_eq_axioms = true; + unsigned m_arith_branch_cut_ratio = 2; + bool m_arith_int_eq_branching = false; + bool m_arith_enum_const_mod = false; - bool m_arith_gcd_test; - bool m_arith_eager_gcd; - bool m_arith_adaptive_gcd; - unsigned m_arith_propagation_threshold; + bool m_arith_gcd_test = true; + bool m_arith_eager_gcd = false; + bool m_arith_adaptive_gcd = false; + unsigned m_arith_propagation_threshold = UINT_MAX; - arith_pivot_strategy m_arith_pivot_strategy; + arith_pivot_strategy m_arith_pivot_strategy = arith_pivot_strategy::ARITH_PIVOT_SMALLEST; // used in diff-logic - bool m_arith_add_binary_bounds; - arith_prop_strategy m_arith_propagation_strategy; + bool m_arith_add_binary_bounds = false; + arith_prop_strategy m_arith_propagation_strategy = arith_prop_strategy::ARITH_PROP_PROPORTIONAL; // used arith_eq_adapter - bool m_arith_eq_bounds; - bool m_arith_lazy_adapter; + bool m_arith_eq_bounds = false; + bool m_arith_lazy_adapter = false; // performance debugging flags - bool m_arith_fixnum; - bool m_arith_int_only; + bool m_arith_fixnum = false; + bool m_arith_int_only = false; // non linear support - bool m_nl_arith; - bool m_nl_arith_gb; - unsigned m_nl_arith_gb_threshold; - bool m_nl_arith_gb_eqs; - bool m_nl_arith_gb_perturbate; - unsigned m_nl_arith_max_degree; - bool m_nl_arith_branching; - unsigned m_nl_arith_rounds; + bool m_nl_arith = true; + bool m_nl_arith_gb = true; + unsigned m_nl_arith_gb_threshold = 512; + bool m_nl_arith_gb_eqs = false; + bool m_nl_arith_gb_perturbate = true; + unsigned m_nl_arith_max_degree = 6; + bool m_nl_arith_branching = true; + unsigned m_nl_arith_rounds = 1024; - - theory_arith_params(params_ref const & p = params_ref()): - m_arith_eq2ineq(false), - m_arith_process_all_eqs(false), - m_arith_mode(arith_solver_id::AS_NEW_ARITH), - m_arith_auto_config_simplex(false), - m_arith_blands_rule_threshold(1000), - m_arith_propagate_eqs(true), - m_arith_bound_prop(bound_prop_mode::BP_REFINE), - m_arith_stronger_lemmas(true), - m_arith_skip_rows_with_big_coeffs(true), - m_arith_max_lemma_size(128), - m_arith_small_lemma_size(16), - m_arith_reflect(true), - m_arith_ignore_int(false), - m_arith_lazy_pivoting_lvl(0), - m_arith_random_seed(0), - m_arith_random_initial_value(false), - m_arith_random_lower(-1000), - m_arith_random_upper(1000), - m_arith_adaptive(false), - m_arith_adaptive_assertion_threshold(0.2), - m_arith_adaptive_propagation_threshold(0.4), - m_arith_dump_lemmas(false), - m_arith_eager_eq_axioms(true), - m_arith_branch_cut_ratio(2), - m_arith_int_eq_branching(false), - m_arith_enum_const_mod(false), - m_arith_gcd_test(true), - m_arith_eager_gcd(false), - m_arith_adaptive_gcd(false), - m_arith_propagation_threshold(UINT_MAX), - m_arith_pivot_strategy(arith_pivot_strategy::ARITH_PIVOT_SMALLEST), - m_arith_add_binary_bounds(false), - m_arith_propagation_strategy(arith_prop_strategy::ARITH_PROP_PROPORTIONAL), - m_arith_eq_bounds(false), - m_arith_lazy_adapter(false), - m_arith_fixnum(false), - m_arith_int_only(false), - m_nl_arith(true), - m_nl_arith_gb(true), - m_nl_arith_gb_threshold(512), - m_nl_arith_gb_eqs(false), - m_nl_arith_gb_perturbate(true), - m_nl_arith_max_degree(6), - m_nl_arith_branching(true), - m_nl_arith_rounds(1024) { + theory_arith_params(params_ref const & p = params_ref()) { updt_params(p); } diff --git a/src/smt/params/theory_array_params.h b/src/smt/params/theory_array_params.h index 250d17ffb..b6da32ba5 100644 --- a/src/smt/params/theory_array_params.h +++ b/src/smt/params/theory_array_params.h @@ -28,34 +28,20 @@ enum array_solver_id { }; struct theory_array_params { - bool m_array_canonize_simplify; - bool m_array_simplify; // temporary hack for disabling array simplifier plugin. - array_solver_id m_array_mode; - bool m_array_weak; - bool m_array_extensional; - unsigned m_array_laziness; - bool m_array_delay_exp_axiom; - bool m_array_cg; - bool m_array_always_prop_upward; - bool m_array_lazy_ieq; - unsigned m_array_lazy_ieq_delay; - bool m_array_fake_support; // fake support for all array operations to pretend they are satisfiable. - - theory_array_params(): - m_array_canonize_simplify(false), - m_array_simplify(true), - m_array_mode(array_solver_id::AR_FULL), - m_array_weak(false), - m_array_extensional(true), - m_array_laziness(1), - m_array_delay_exp_axiom(true), - m_array_cg(false), - m_array_always_prop_upward(true), // UPWARDs filter is broken... TODO: fix it - m_array_lazy_ieq(false), - m_array_lazy_ieq_delay(10), - m_array_fake_support(false) { - } + bool m_array_canonize_simplify = false; + bool m_array_simplify = true; // temporary hack for disabling array simplifier plugin. + array_solver_id m_array_mode = array_solver_id::AR_FULL; + bool m_array_weak = false; + bool m_array_extensional = true; + unsigned m_array_laziness = 1; + bool m_array_delay_exp_axiom = true; + bool m_array_cg = false; + bool m_array_always_prop_upward = true; + bool m_array_lazy_ieq = false; + unsigned m_array_lazy_ieq_delay = 10; + bool m_array_fake_support = false; // fake support for all array operations to pretend they are satisfiable. + theory_array_params() {} void updt_params(params_ref const & _p); diff --git a/src/smt/params/theory_bv_params.h b/src/smt/params/theory_bv_params.h index 1fc477c79..57ec16b6a 100644 --- a/src/smt/params/theory_bv_params.h +++ b/src/smt/params/theory_bv_params.h @@ -26,27 +26,17 @@ enum bv_solver_id { }; struct theory_bv_params { - bv_solver_id m_bv_mode; - bool m_hi_div0; //!< if true, uses the hardware interpretation for div0, mod0, ... if false, div0, mod0, ... are considered uninterpreted. - bool m_bv_reflect; - bool m_bv_lazy_le; - bool m_bv_cc; - bool m_bv_eq_axioms; - unsigned m_bv_blast_max_size; - bool m_bv_enable_int2bv2int; - bool m_bv_watch_diseq; - bool m_bv_delay; - theory_bv_params(params_ref const & p = params_ref()): - m_bv_mode(bv_solver_id::BS_BLASTER), - m_hi_div0(false), - m_bv_reflect(true), - m_bv_lazy_le(false), - m_bv_cc(false), - m_bv_eq_axioms(true), - m_bv_blast_max_size(INT_MAX), - m_bv_enable_int2bv2int(true), - m_bv_watch_diseq(false), - m_bv_delay(true) { + bv_solver_id m_bv_mode = bv_solver_id::BS_BLASTER; + bool m_hi_div0 = false; //!< if true, uses the hardware interpretation for div0, mod0, ... if false, div0, mod0, ... are considered uninterpreted. + bool m_bv_reflect = true; + bool m_bv_lazy_le = false; + bool m_bv_cc = false; + bool m_bv_eq_axioms = true; + unsigned m_bv_blast_max_size = INT_MAX; + bool m_bv_enable_int2bv2int = true; + bool m_bv_watch_diseq = false; + bool m_bv_delay = true; + theory_bv_params(params_ref const & p = params_ref()) { updt_params(p); } diff --git a/src/smt/params/theory_pb_params.h b/src/smt/params/theory_pb_params.h index a706f844b..2922ca5ef 100644 --- a/src/smt/params/theory_pb_params.h +++ b/src/smt/params/theory_pb_params.h @@ -22,12 +22,11 @@ Revision History: struct theory_pb_params { - unsigned m_pb_conflict_frequency; - bool m_pb_learn_complements; - theory_pb_params(params_ref const & p = params_ref()): - m_pb_conflict_frequency(1000), - m_pb_learn_complements(true) - {} + unsigned m_pb_conflict_frequency = 1000; + bool m_pb_learn_complements = true; + theory_pb_params(params_ref const & p = params_ref()) { + updt_params(p); + } void updt_params(params_ref const & p); diff --git a/src/smt/params/theory_seq_params.h b/src/smt/params/theory_seq_params.h index 002d6c9e6..84437fa15 100644 --- a/src/smt/params/theory_seq_params.h +++ b/src/smt/params/theory_seq_params.h @@ -22,14 +22,10 @@ struct theory_seq_params { /* * Enable splitting guided by length constraints */ - bool m_split_w_len; - bool m_seq_validate; + bool m_split_w_len = false; + bool m_seq_validate = false; - - theory_seq_params(params_ref const & p = params_ref()): - m_split_w_len(false), - m_seq_validate(false) - { + theory_seq_params(params_ref const & p = params_ref()) { updt_params(p); } diff --git a/src/smt/params/theory_str_params.h b/src/smt/params/theory_str_params.h index 971f4ba18..0dd5e51f6 100644 --- a/src/smt/params/theory_str_params.h +++ b/src/smt/params/theory_str_params.h @@ -27,108 +27,92 @@ struct theory_str_params { * This is a stronger version of the standard axiom. * The Z3str2 axioms can be simulated by setting this to false. */ - bool m_StrongArrangements; + bool m_StrongArrangements = true; /* * If AggressiveLengthTesting is true, we manipulate the phase of length tester equalities * to prioritize trying concrete length options over choosing the "more" option. */ - bool m_AggressiveLengthTesting; + bool m_AggressiveLengthTesting = false; /* * Similarly, if AggressiveValueTesting is true, we manipulate the phase of value tester equalities * to prioritize trying concrete value options over choosing the "more" option. */ - bool m_AggressiveValueTesting; + bool m_AggressiveValueTesting = false; /* * If AggressiveUnrollTesting is true, we manipulate the phase of regex unroll tester equalities * to prioritize trying concrete unroll counts over choosing the "more" option. */ - bool m_AggressiveUnrollTesting; + bool m_AggressiveUnrollTesting = true; /* * If UseFastLengthTesterCache is set to true, * length tester terms will not be generated from scratch each time they are needed, * but will be saved in a map and looked up. */ - bool m_UseFastLengthTesterCache; + bool m_UseFastLengthTesterCache = false; /* * If UseFastValueTesterCache is set to true, * value tester terms will not be generated from scratch each time they are needed, * but will be saved in a map and looked up. */ - bool m_UseFastValueTesterCache; + bool m_UseFastValueTesterCache = true; /* * If StringConstantCache is set to true, * all string constants in theory_str generated from anywhere will be cached and saved. */ - bool m_StringConstantCache; + bool m_StringConstantCache = true; - double m_OverlapTheoryAwarePriority; + double m_OverlapTheoryAwarePriority = -0.1; /* * RegexAutomata_DifficultyThreshold is the lowest difficulty above which Z3str3 * will not eagerly construct an automaton for a regular expression term. */ - unsigned m_RegexAutomata_DifficultyThreshold; + unsigned m_RegexAutomata_DifficultyThreshold = 1000; /* * RegexAutomata_IntersectionDifficultyThreshold is the lowest difficulty above which Z3str3 * will not eagerly intersect automata to check unsatisfiability. */ - unsigned m_RegexAutomata_IntersectionDifficultyThreshold; + unsigned m_RegexAutomata_IntersectionDifficultyThreshold = 1000; /* * RegexAutomata_FailedAutomatonThreshold is the number of failed attempts to build an automaton * after which a full automaton (i.e. with no length information) will be built regardless of difficulty. */ - unsigned m_RegexAutomata_FailedAutomatonThreshold; + unsigned m_RegexAutomata_FailedAutomatonThreshold = 10; /* * RegexAutomaton_FailedIntersectionThreshold is the number of failed attempts to perform automaton * intersection after which intersection will always be performed regardless of difficulty. */ - unsigned m_RegexAutomata_FailedIntersectionThreshold; + unsigned m_RegexAutomata_FailedIntersectionThreshold = 10; /* * RegexAutomaton_LengthAttemptThreshold is the number of attempts to satisfy length/path constraints * before which we begin checking unsatisfiability of a regex term. */ - unsigned m_RegexAutomata_LengthAttemptThreshold; + unsigned m_RegexAutomata_LengthAttemptThreshold = 10; /* * If FixedLengthRefinement is true and the fixed-length equation solver is enabled, * Z3str3 will use abstraction refinement to handle formulas that would result in disjunctions or expensive * reductions to fixed-length formulas. */ - bool m_FixedLengthRefinement; + bool m_FixedLengthRefinement = false; /* * If FixedLengthNaiveCounterexamples is true and the fixed-length equation solver is enabled, * Z3str3 will only construct simple counterexamples to block unsatisfiable length assignments * instead of attempting to learn more complex lessons. */ - bool m_FixedLengthNaiveCounterexamples; + bool m_FixedLengthNaiveCounterexamples = true; - theory_str_params(params_ref const & p = params_ref()): - m_StrongArrangements(true), - m_AggressiveLengthTesting(false), - m_AggressiveValueTesting(false), - m_AggressiveUnrollTesting(true), - m_UseFastLengthTesterCache(false), - m_UseFastValueTesterCache(true), - m_StringConstantCache(true), - m_OverlapTheoryAwarePriority(-0.1), - m_RegexAutomata_DifficultyThreshold(1000), - m_RegexAutomata_IntersectionDifficultyThreshold(1000), - m_RegexAutomata_FailedAutomatonThreshold(10), - m_RegexAutomata_FailedIntersectionThreshold(10), - m_RegexAutomata_LengthAttemptThreshold(10), - m_FixedLengthRefinement(false), - m_FixedLengthNaiveCounterexamples(true) - { + theory_str_params(params_ref const & p = params_ref()) { updt_params(p); } diff --git a/src/smt/smt_context_inv.cpp b/src/smt/smt_context_inv.cpp index bc994f0b3..f0e8fb59b 100644 --- a/src/smt/smt_context_inv.cpp +++ b/src/smt/smt_context_inv.cpp @@ -371,7 +371,7 @@ namespace smt { case l_true: if (!m_proto_model->eval(n, res, false)) return true; - CTRACE("model", !m.is_true(res), tout << n << " evaluates to " << res << "\n";); + CTRACE("model", !m.is_true(res), tout << n << " evaluates to " << res << "\n" << *m_proto_model << "\n";); if (m.is_false(res)) { return false; } @@ -379,7 +379,7 @@ namespace smt { case l_false: if (!m_proto_model->eval(n, res, false)) return true; - CTRACE("model", !m.is_false(res), tout << n << " evaluates to " << res << "\n";); + CTRACE("model", !m.is_false(res), tout << n << " evaluates to " << res << "\n" << *m_proto_model << "\n";); if (m.is_true(res)) { return false; } diff --git a/src/smt/theory_array_base.cpp b/src/smt/theory_array_base.cpp index ab3570872..79b380671 100644 --- a/src/smt/theory_array_base.cpp +++ b/src/smt/theory_array_base.cpp @@ -389,19 +389,7 @@ namespace smt { if (q) { // the variables in q are maybe not consecutive. var_subst sub(m, false); - expr_free_vars fv; - fv(q); - expr_ref_vector es(m); - es.resize(fv.size()); - for (unsigned i = 0, j = 0; i < e->get_num_args(); ++i) { - SASSERT(j < es.size()); - while (!fv[j]) { - ++j; - SASSERT(j < es.size()); - } - es[j++] = e->get_arg(i); - } - f = sub(q, es.size(), es.data()); + f = sub(q, e->get_num_args(), e->get_args()); } return f; } diff --git a/src/smt/theory_char.cpp b/src/smt/theory_char.cpp index a89693476..772438986 100644 --- a/src/smt/theory_char.cpp +++ b/src/smt/theory_char.cpp @@ -16,6 +16,7 @@ Author: --*/ #include "ast/ast_ll_pp.h" +#include "ast/bv_decl_plugin.h" #include "smt/theory_char.h" #include "smt/smt_context.h" #include "smt/smt_model_generator.h" @@ -84,6 +85,11 @@ namespace smt { expr* n = nullptr; if (seq.is_char2int(term, n)) new_char2int(v, n); + else if (seq.is_char2bv(term, n)) + new_char2bv(term, n); + else if (seq.is_bv2char(term, n)) + new_bv2char(v, n); + return true; } @@ -265,6 +271,34 @@ namespace smt { ctx.assign_eq(n1, n2, eq_justification(j)); } + void theory_char::new_char2bv(expr* b, expr* c) { + theory_var w = ctx.get_enode(c)->get_th_var(get_id()); + init_bits(w); + auto const& bits = get_bits(w); + bv_util bv(m); + SASSERT(bits.size() == bv.get_bv_size(b)); + unsigned i = 0; + for (auto bit1 : bits) { + auto bit2 = mk_literal(bv.mk_bit2bool(b, i++)); + ctx.mk_th_axiom(get_id(), ~bit1, bit2); + ctx.mk_th_axiom(get_id(), bit1, ~bit2); + } + } + + void theory_char::new_bv2char(theory_var v, expr* b) { + init_bits(v); + auto const& bits = get_bits(v); + bv_util bv(m); + SASSERT(bits.size() == bv.get_bv_size(b)); + unsigned i = 0; + for (auto bit1 : bits) { + auto bit2 = mk_literal(bv.mk_bit2bool(b, i++)); + ctx.mk_th_axiom(get_id(), ~bit1, bit2); + ctx.mk_th_axiom(get_id(), bit1, ~bit2); + } + } + + /** * 1. Check that values of classes are unique. diff --git a/src/smt/theory_char.h b/src/smt/theory_char.h index 511bcbd10..8be817cda 100644 --- a/src/smt/theory_char.h +++ b/src/smt/theory_char.h @@ -57,6 +57,8 @@ namespace smt { bool final_check(); void new_const_char(theory_var v, unsigned c); void new_char2int(theory_var v, expr* c); + void new_bv2char(theory_var v, expr* b); + void new_char2bv(expr* n, expr* c); unsigned get_char_value(theory_var v); void internalize_le(literal lit, app* term); void internalize_is_digit(literal lit, app* term); diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index abe10d0f3..124461189 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -807,10 +807,10 @@ class theory_lra::imp { return st.vars()[0]; } else if (is_one(st) && a.is_numeral(term)) { - return get_one(a.is_int(term)); + return lp().local_to_external(get_one(a.is_int(term))); } else if (is_zero(st) && a.is_numeral(term)) { - return get_zero(a.is_int(term)); + return lp().local_to_external(get_zero(a.is_int(term))); } else { init_left_side(st); diff --git a/src/smt/user_propagator.cpp b/src/smt/user_propagator.cpp index 5769a34e5..7fbfd567f 100644 --- a/src/smt/user_propagator.cpp +++ b/src/smt/user_propagator.cpp @@ -52,6 +52,8 @@ void user_propagator::propagate_cb( unsigned num_fixed, unsigned const* fixed_ids, unsigned num_eqs, unsigned const* eq_lhs, unsigned const* eq_rhs, expr* conseq) { + if (ctx.lit_internalized(conseq) && ctx.get_assignment(ctx.get_literal(conseq)) == l_true) + return; m_prop.push_back(prop_info(num_fixed, fixed_ids, num_eqs, eq_lhs, eq_rhs, expr_ref(conseq, m))); } @@ -125,7 +127,10 @@ void user_propagator::propagate() { for (auto const& p : prop.m_eqs) m_eqs.push_back(enode_pair(get_enode(p.first), get_enode(p.second))); DEBUG_CODE(for (auto const& p : m_eqs) VERIFY(p.first->get_root() == p.second->get_root());); + DEBUG_CODE(for (unsigned id : prop.m_ids) VERIFY(m_fixed.contains(id));); + DEBUG_CODE(for (literal lit : m_lits) VERIFY(ctx.get_assignment(lit) == l_true);); + if (m.is_false(prop.m_conseq)) { js = ctx.mk_justification( ext_theory_conflict_justification( diff --git a/src/solver/assertions/asserted_formulas.cpp b/src/solver/assertions/asserted_formulas.cpp index be931ccd6..9e9b54140 100644 --- a/src/solver/assertions/asserted_formulas.cpp +++ b/src/solver/assertions/asserted_formulas.cpp @@ -532,14 +532,14 @@ void asserted_formulas::propagate_values() { flush_cache(); unsigned num_prop = 0; - unsigned delta_prop = m_formulas.size(); - while (!inconsistent() && m_formulas.size()/20 < delta_prop) { + unsigned sz = m_formulas.size(); + unsigned delta_prop = sz; + while (!inconsistent() && sz/20 < delta_prop) { m_expr2depth.reset(); m_scoped_substitution.push(); unsigned prop = num_prop; TRACE("propagate_values", display(tout << "before:\n");); unsigned i = m_qhead; - unsigned sz = m_formulas.size(); for (; i < sz; i++) { prop += propagate_values(i); } @@ -558,6 +558,9 @@ void asserted_formulas::propagate_values() { TRACE("propagate_values", tout << "after:\n"; display(tout);); delta_prop = prop - num_prop; num_prop = prop; + if (sz <= m_formulas.size()) + break; + sz = m_formulas.size(); } TRACE("asserted_formulas", tout << num_prop << "\n";); if (num_prop > 0) diff --git a/src/solver/parallel_tactic.cpp b/src/solver/parallel_tactic.cpp index c0bf63b23..8336f0050 100644 --- a/src/solver/parallel_tactic.cpp +++ b/src/solver/parallel_tactic.cpp @@ -503,7 +503,10 @@ private: cube.append(s.split_cubes(1)); SASSERT(cube.size() <= 1); IF_VERBOSE(2, verbose_stream() << "(tactic.parallel :split-cube " << cube.size() << ")\n";); - if (!s.cubes().empty()) m_queue.add_task(s.clone()); + { + // std::lock_guard lock(m_mutex); + if (!s.cubes().empty()) m_queue.add_task(s.clone()); + } if (!cube.empty()) { s.assert_cube(cube.get(0).cube()); vars.reset(); @@ -611,8 +614,12 @@ private: void spawn_cubes(solver_state& s, unsigned width, vector& cubes) { if (cubes.empty()) return; add_branches(cubes.size()); - s.set_cubes(cubes); - solver_state* s1 = s.clone(); + s.set_cubes(cubes); + solver_state* s1 = nullptr; + { + // std::lock_guard lock(m_mutex); + s1 = s.clone(); + } s1->inc_width(width); m_queue.add_task(s1); } diff --git a/src/tactic/core/solve_eqs_tactic.cpp b/src/tactic/core/solve_eqs_tactic.cpp index 5196b1df1..b9feaf949 100644 --- a/src/tactic/core/solve_eqs_tactic.cpp +++ b/src/tactic/core/solve_eqs_tactic.cpp @@ -21,6 +21,7 @@ Revision History: #include "ast/ast_util.h" #include "ast/ast_pp.h" #include "ast/pb_decl_plugin.h" +#include "ast/recfun_decl_plugin.h" #include "ast/rewriter/th_rewriter.h" #include "ast/rewriter/rewriter_def.h" #include "ast/rewriter/hoist_rewriter.h" @@ -407,6 +408,9 @@ class solve_eqs_tactic : public tactic { } void insert_solution(goal const& g, unsigned idx, expr* f, app* var, expr* def, proof* pr) { + + if (!is_safe(var)) + return; m_vars.push_back(var); m_candidates.push_back(f); m_candidate_set.mark(f); @@ -707,8 +711,21 @@ class solve_eqs_tactic : public tactic { pr1 = m().mk_transitivity(pr1, pr2); if (!pr1) pr1 = g.pr(idx); else pr1 = m().mk_modus_ponens(g.pr(idx), pr1); g.update(idx, tmp2, pr1, g.dep(idx)); - } - + } + } + + expr_mark m_unsafe_vars; + + void filter_unsafe_vars() { + m_unsafe_vars.reset(); + recfun::util rec(m()); + for (func_decl* f : rec.get_rec_funs()) + for (expr* term : subterms::all(expr_ref(rec.get_def(f).get_rhs(), m()))) + m_unsafe_vars.mark(term); + } + + bool is_safe(expr* f) { + return !m_unsafe_vars.is_marked(f); } void sort_vars() { @@ -1020,6 +1037,8 @@ class solve_eqs_tactic : public tactic { m_subst = alloc(expr_substitution, m(), m_produce_unsat_cores, m_produce_proofs); m_norm_subst = alloc(expr_substitution, m(), m_produce_unsat_cores, m_produce_proofs); unsigned rounds = 0; + + filter_unsafe_vars(); while (rounds < 20) { ++rounds; if (!m_produce_proofs && m_context_solve && rounds < 3) { diff --git a/src/tactic/fd_solver/smtfd_solver.cpp b/src/tactic/fd_solver/smtfd_solver.cpp index 4ebb07898..3e23175ff 100644 --- a/src/tactic/fd_solver/smtfd_solver.cpp +++ b/src/tactic/fd_solver/smtfd_solver.cpp @@ -619,7 +619,7 @@ namespace smtfd { return false; } else if (round < max_rounds) { - for (expr* t : subterms(core)) { + for (expr* t : subterms::ground(core)) { for (theory_plugin* p : m_plugins) { p->check_term(t, round); } @@ -863,7 +863,7 @@ namespace smtfd { } mdl->register_decl(fn, fi); } - for (expr* t : subterms(terms)) { + for (expr* t : subterms::ground(terms)) { if (is_uninterp_const(t) && sort_covered(t->get_sort())) { expr_ref val = model_value(t); mdl->register_decl(to_app(t)->get_decl(), val); @@ -1305,7 +1305,7 @@ namespace smtfd { void populate_model(model_ref& mdl, expr_ref_vector const& terms) override { - for (expr* t : subterms(terms)) { + for (expr* t : subterms::ground(terms)) { if (is_uninterp_const(t) && m_autil.is_array(t)) { mdl->register_decl(to_app(t)->get_decl(), model_value_core(t)); } @@ -1317,7 +1317,7 @@ namespace smtfd { void global_check(expr_ref_vector const& core) override { expr_mark seen; expr_ref_vector shared(m), sharedvals(m); - for (expr* t : subterms(core)) { + for (expr* t : subterms::ground(core)) { if (!is_app(t)) continue; app* a = to_app(t); unsigned offset = 0; @@ -1463,7 +1463,7 @@ namespace smtfd { if (r == l_true) { expr_ref qq(q->get_expr(), m); - for (expr* t : subterms(qq)) { + for (expr* t : subterms::ground(qq)) { init_term(t); } m_solver->get_model(mdl); @@ -1558,10 +1558,10 @@ namespace smtfd { void init_val2term(expr_ref_vector const& fmls, expr_ref_vector const& core) { m_val2term_trail.reset(); m_val2term.reset(); - for (expr* t : subterms(core)) { + for (expr* t : subterms::ground(core)) { init_term(t); } - for (expr* t : subterms(fmls)) { + for (expr* t : subterms::ground(fmls)) { init_term(t); } } @@ -1719,12 +1719,12 @@ namespace smtfd { m_context.reset(m_model); expr_ref_vector terms(core); terms.append(m_axioms); - for (expr* t : subterms(core)) { + for (expr* t : subterms::ground(core)) { if (is_forall(t) || is_exists(t)) { has_q = true; } } - for (expr* t : subterms(terms)) { + for (expr* t : subterms::ground(terms)) { if (!is_forall(t) && !is_exists(t) && (!m_context.term_covered(t) || !m_context.sort_covered(t->get_sort()))) { is_decided = l_false; } @@ -1733,7 +1733,7 @@ namespace smtfd { TRACE("smtfd", tout << "axioms: " << m_axioms << "\n"; - for (expr* a : subterms(terms)) { + for (expr* a : subterms::ground(terms)) { expr_ref val0 = (*m_model)(a); expr_ref val1 = (*m_model)(abs(a)); if (is_ground(a) && val0 != val1 && val0->get_sort() == val1->get_sort()) { @@ -1750,7 +1750,7 @@ namespace smtfd { DEBUG_CODE( bool found_bad = false; - for (expr* a : subterms(core)) { + for (expr* a : subterms::ground(core)) { expr_ref val0 = (*m_model)(a); expr_ref val1 = (*m_model)(abs(a)); if (is_ground(a) && val0 != val1 && val0->get_sort() == val1->get_sort()) { diff --git a/src/tactic/portfolio/solver_subsumption_tactic.h b/src/tactic/portfolio/solver_subsumption_tactic.h index c088aa0b0..73dfb562c 100644 --- a/src/tactic/portfolio/solver_subsumption_tactic.h +++ b/src/tactic/portfolio/solver_subsumption_tactic.h @@ -19,7 +19,7 @@ class tactic; tactic * mk_solver_subsumption_tactic(ast_manager & m, params_ref const & p = params_ref()); /* - ADD_TACTIC("solver_subsumption", "remove assertions that are subsumed.", "mk_solver_subsumption_tactic(m, p)") + ADD_TACTIC("solver-subsumption", "remove assertions that are subsumed.", "mk_solver_subsumption_tactic(m, p)") */ diff --git a/src/test/pdd_solver.cpp b/src/test/pdd_solver.cpp index 170e887a7..7a1c07131 100644 --- a/src/test/pdd_solver.cpp +++ b/src/test/pdd_solver.cpp @@ -182,7 +182,7 @@ namespace dd { void collect_id2var(unsigned_vector& id2var, expr_ref_vector const& fmls) { svector> ds; unsigned maxid = 0; - for (expr* e : subterms(fmls)) { + for (expr* e : subterms::ground(fmls)) { ds.push_back(std::make_pair(to_app(e)->get_depth(), e->get_id())); maxid = std::max(maxid, e->get_id()); } @@ -202,11 +202,11 @@ namespace dd { pdd_manager p(id2var.size(), use_mod2 ? pdd_manager::mod2_e : pdd_manager::zero_one_vars_e); solver g(m.limit(), p); - for (expr* e : subterms(fmls)) { + for (expr* e : subterms::ground(fmls)) { add_def(id2var, to_app(e), m, p, g); } if (!use_mod2) { // should be built-in - for (expr* e : subterms(fmls)) { + for (expr* e : subterms::ground(fmls)) { pdd v = p.mk_var(id2var[e->get_id()]); g.add(v*v - v); } diff --git a/src/util/zstring.cpp b/src/util/zstring.cpp index 46c9d9fce..534999606 100644 --- a/src/util/zstring.cpp +++ b/src/util/zstring.cpp @@ -42,10 +42,8 @@ bool zstring::is_escape_char(char const *& s, unsigned& result) { result = 16*result + d; } else if (*(s+3+i) == '}') { - if (result > 255 && !uses_unicode()) - throw default_exception("unicode characters outside of byte range are not supported"); - if (result > unicode_max_char()) - throw default_exception("unicode characters outside of byte range are not supported"); + if (result > max_char()) + return false; s += 4 + i; return true; } @@ -65,8 +63,8 @@ bool zstring::is_escape_char(char const *& s, unsigned& result) { result = 16*result + d2; result = 16*result + d3; result = 16*result + d4; - if (result > unicode_max_char()) - throw default_exception("unicode characters outside of byte range are not supported"); + if (result > max_char()) + return false; s += 6; return true; } @@ -87,14 +85,19 @@ zstring::zstring(char const* s) { SASSERT(well_formed()); } - -bool zstring::uses_unicode() const { - return gparams::get_value("unicode") != "false"; +string_encoding zstring::get_encoding() { + if (gparams::get_value("encoding") == "unicode") + return unicode; + if (gparams::get_value("encoding") == "bmp") + return bmp; + if (gparams::get_value("encoding") == "ascii") + return ascii; + return unicode; } bool zstring::well_formed() const { for (unsigned ch : m_buffer) { - if (ch > unicode_max_char()) { + if (ch > max_char()) { IF_VERBOSE(0, verbose_stream() << "large character: " << ch << "\n";); return false; } @@ -147,7 +150,7 @@ std::string zstring::encode() const { #define _flush() if (offset > 0) { buffer[offset] = 0; strm << buffer; offset = 0; } for (unsigned i = 0; i < m_buffer.size(); ++i) { unsigned ch = m_buffer[i]; - if (ch < 32 || ch >= 128) { + if (ch < 32 || ch >= 128 || ('\\' == ch && i + 1 < m_buffer.size() && 'u' == m_buffer[i+1])) { _flush(); strm << "\\u{" << std::hex << ch << std::dec << "}"; } diff --git a/src/util/zstring.h b/src/util/zstring.h index a15d1b03d..c5606b267 100644 --- a/src/util/zstring.h +++ b/src/util/zstring.h @@ -21,17 +21,47 @@ Author: #include "util/buffer.h" #include "util/rational.h" +enum string_encoding { + ascii, // exactly 8 bits + unicode, + bmp // basic multilingual plane; exactly 16 bits +}; + class zstring { private: buffer m_buffer; bool well_formed() const; - bool uses_unicode() const; bool is_escape_char(char const *& s, unsigned& result); public: static unsigned unicode_max_char() { return 196607; } static unsigned unicode_num_bits() { return 18; } + static unsigned bmp_max_char() { return 65535; } + static unsigned bmp_num_bits() { return 16; } static unsigned ascii_max_char() { return 255; } static unsigned ascii_num_bits() { return 8; } + static unsigned max_char() { + switch (get_encoding()) { + case unicode: + return unicode_max_char(); + case bmp: + return bmp_max_char(); + case ascii: + return ascii_max_char(); + } + return unicode_max_char(); + } + static unsigned num_bits() { + switch (get_encoding()) { + case unicode: + return unicode_num_bits(); + case bmp: + return bmp_num_bits(); + case ascii: + return ascii_num_bits(); + } + return unicode_num_bits(); + } + static string_encoding get_encoding(); zstring() = default; zstring(char const* s); zstring(const std::string &str) : zstring(str.c_str()) {}