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

Merge branch 'master' of http://github.com/z3prover/z3 into polysat

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-09-20 17:39:04 -07:00
commit 959f150e4a
104 changed files with 1666 additions and 1040 deletions
Download patch file Download diff file Expand all files Collapse all files

14
src/api/api_ast.cpp
View file

@ -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;

15
src/api/api_seq.cpp
View file

@ -187,14 +187,18 @@ extern "C" {
svector<char> 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);
};

1
src/api/api_solver.cpp
View file

@ -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" {

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

@ -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) \

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

@ -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);
}
}
/// <summary>
/// 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));
}
/// <summary>
/// Create less than or equal to between two characters.
/// </summary>
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));
}
/// <summary>
/// Create an integer (code point) from character.
/// </summary>
public IntExpr CharToInt(Expr ch)
{
Debug.Assert(ch != null);
return new IntExpr(this, Native.Z3_mk_char_to_int(nCtx, ch.NativeObject));
}
/// <summary>
/// Create a bit-vector (code point) from character.
/// </summary>
public BitVecExpr CharToBV(Expr ch)
{
Debug.Assert(ch != null);
return new BitVecExpr(this, Native.Z3_mk_char_to_bv(nCtx, ch.NativeObject));
}
/// <summary>
/// Create a character from a bit-vector (code point).
/// </summary>
public Expr CharFromBV(BitVecExpr bv)
{
Debug.Assert(bv != null);
return new Expr(this, Native.Z3_mk_char_from_bv(nCtx, bv.NativeObject));
}
/// <summary>
/// Create a check if the character is a digit.
/// </summary>
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

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

@ -508,11 +508,11 @@ public class Context implements AutoCloseable {
*/
public <R extends Sort> void AddRecDef(FuncDecl<R> f, Expr<?>[] args, Expr<R> 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<CharSort> intToString(Expr<IntSort> e)
{
return (SeqExpr<CharSort>) Expr.create(this, Native.mkIntToStr(nCtx(), e.getNativeObject()));
return (SeqExpr<CharSort>) Expr.create(this, Native.mkIntToStr(nCtx(), e.getNativeObject()));
}
/**
@ -2033,7 +2033,7 @@ public class Context implements AutoCloseable {
*/
public SeqExpr<CharSort> ubvToString(Expr<BitVecSort> e)
{
return (SeqExpr<CharSort>) Expr.create(this, Native.mkUbvToStr(nCtx(), e.getNativeObject()));
return (SeqExpr<CharSort>) Expr.create(this, Native.mkUbvToStr(nCtx(), e.getNativeObject()));
}
/**
@ -2041,7 +2041,7 @@ public class Context implements AutoCloseable {
*/
public SeqExpr<CharSort> sbvToString(Expr<BitVecSort> e)
{
return (SeqExpr<CharSort>) Expr.create(this, Native.mkSbvToStr(nCtx(), e.getNativeObject()));
return (SeqExpr<CharSort>) Expr.create(this, Native.mkSbvToStr(nCtx(), e.getNativeObject()));
}
/**
@ -2049,7 +2049,7 @@ public class Context implements AutoCloseable {
*/
public IntExpr stringToInt(Expr<SeqSort<CharSort>> 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 <R extends Sort> Expr<R> MkNth(Expr<SeqSort<R>> s, Expr<IntSort> index)
public <R extends Sort> Expr<R> mkNth(Expr<SeqSort<R>> s, Expr<IntSort> index)
{
checkContextMatch(s, index);
return (Expr<R>) Expr.create(this, Native.mkSeqNth(nCtx(), s.getNativeObject(), index.getNativeObject()));
@ -2252,7 +2252,7 @@ public class Context implements AutoCloseable {
*/
public <R extends Sort> ReExpr<R> mkEmptyRe(R s)
{
return (ReExpr<R>) Expr.create(this, Native.mkReEmpty(nCtx(), s.getNativeObject()));
return (ReExpr<R>) Expr.create(this, Native.mkReEmpty(nCtx(), s.getNativeObject()));
}
/**
@ -2260,7 +2260,7 @@ public class Context implements AutoCloseable {
*/
public <R extends Sort> ReExpr<R> mkFullRe(R s)
{
return (ReExpr<R>) Expr.create(this, Native.mkReFull(nCtx(), s.getNativeObject()));
return (ReExpr<R>) Expr.create(this, Native.mkReFull(nCtx(), s.getNativeObject()));
}
/**
@ -2272,6 +2272,50 @@ public class Context implements AutoCloseable {
return (ReExpr<R>) Expr.create(this, Native.mkReRange(nCtx(), lo.getNativeObject(), hi.getNativeObject()));
}
/**
* Create less than or equal to between two characters.
*/
public BoolExpr mkCharLe(Expr<CharSort> ch1, Expr<CharSort> 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<CharSort> 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<CharSort> ch)
{
checkContextMatch(ch);
return (BitVecExpr) Expr.create(this, Native.mkCharToBv(nCtx(), ch.getNativeObject()));
}
/**
* Create a character from a bit-vector (code point).
*/
public Expr<CharSort> charFromBv(BitVecExpr bv)
{
checkContextMatch(bv);
return (Expr<CharSort>) Expr.create(this, Native.mkCharFromBv(nCtx(), bv.getNativeObject()));
}
/**
* Create a check if the character is a digit.
*/
public BoolExpr mkIsDigit(Expr<CharSort> ch)
{
checkContextMatch(ch);
return (BoolExpr) Expr.create(this, Native.mkCharIsDigit(nCtx(), ch.getNativeObject()));
}
/**
* Create an at-most-k constraint.

9
src/api/python/z3/z3.py
View file

@ -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):

115
src/api/z3_api.h
View file

@ -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);
/*@}*/

3
src/ast/ast_ll_pp.cpp
View file

@ -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);
}

2
src/ast/ast_util.cpp
View file

@ -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);

32
src/ast/char_decl_plugin.cpp
View file

@ -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<builtin_name>& 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<builtin_name>& sort_names, symbol const& logic) {

14
src/ast/char_decl_plugin.h
View file

@ -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(); }
};

5
src/ast/euf/euf_egraph.cpp
View file

@ -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);

2
src/ast/euf/euf_etable.cpp
View file

@ -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);

21
src/ast/for_each_expr.cpp
View file

@ -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;
}

12
src/ast/for_each_expr.h
View file

@ -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();
};

42
src/ast/fpa/bv2fpa_converter.cpp
View file

@ -19,6 +19,7 @@ Notes:
#include<math.h>
#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, &param, 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 <<

20
src/ast/fpa/fpa2bv_converter.cpp
View file

@ -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);

4
src/ast/fpa/fpa2bv_converter.h
View file

@ -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();

4
src/ast/fpa/fpa2bv_rewriter.cpp
View file

@ -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;

21
src/ast/fpa_decl_plugin.cpp
View file

@ -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<builtin_name> & 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<builtin_name> & 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();

5
src/ast/fpa_decl_plugin.h
View file

@ -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,

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

@ -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));

2
src/ast/recfun_decl_plugin.cpp
View file

@ -466,7 +466,7 @@ namespace recfun {
obj_map<expr, ptr_vector<expr>> parents;
expr_ref tmp(e, m());
parents.insert(e, ptr_vector<expr>());
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<expr>()).push_back(t);

12
src/ast/rewriter/array_rewriter.cpp
View file

@ -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;

8
src/ast/rewriter/fpa_rewriter.cpp
View file

@ -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;

4
src/ast/rewriter/rewriter.h
View file

@ -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<expr> 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();

19
src/ast/rewriter/rewriter_def.h
View file

@ -192,10 +192,21 @@ bool rewriter_tpl<Config>::visit(expr * t, unsigned max_depth) {
switch (t->get_kind()) {
case AST_APP:
if (to_app(t)->get_num_args() == 0) {
if (process_const<ProofGen>(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<ProofGen>(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--;

4
src/ast/rewriter/value_sweep.cpp
View file

@ -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)) {

9
src/ast/seq_decl_plugin.cpp
View file

@ -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);
}

6
src/ast/seq_decl_plugin.h
View file

@ -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(); }

2
src/ast/static_features.cpp
View file

@ -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;

4
src/math/lp/core_solver_pretty_printer.h
View file

@ -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<string> & row, vector<string> & signs, X rst);

6
src/math/lp/core_solver_pretty_printer_def.h
View file

@ -345,12 +345,6 @@ template <typename T, typename X> void core_solver_pretty_printer<T, X>::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();

1
src/model/model_core.cpp
View file

@ -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;

88
src/model/model_evaluator.cpp
View file

@ -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<expr_ref_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<expr_ref_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;

2
src/model/model_v2_pp.cpp
View file

@ -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();

1
src/params/array_rewriter_params.pyg
View file

@ -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")))

15
src/params/context_params.cpp
View file

@ -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);
}

31
src/params/context_params.h
View file

@ -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();

4
src/qe/qe_mbi.cpp
View file

@ -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<func_decl, ptr_vector<app>> 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<app>()).push_back(to_app(e));

68
src/sat/sat_solver.h
View file

@ -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<bin_clause> & 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<bin_clause> & 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;

3
src/sat/sat_solver/inc_sat_solver.cpp
View file

@ -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())

61
src/sat/sat_solver_core.h
View file

@ -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<literal, literal> bin_clause;
virtual void collect_bin_clauses(svector<bin_clause> & r, bool learned, bool learned_only) const = 0;
// collect statistics from sat solver
virtual void collect_statistics(statistics & st) const {}
};
};

6
src/sat/smt/arith_diagnostics.cpp
View file

@ -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;
}

11
src/sat/smt/arith_internalize.cpp
View file

@ -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);

26
src/sat/smt/arith_solver.cpp
View file

@ -581,6 +581,27 @@ namespace arith {
value = ~value;
if (!found_bad && value == get_phase(n->bool_var()))
continue;
TRACE("arith",
ptr_vector<expr> 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))

55
src/sat/smt/array_axioms.cpp
View file

@ -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<theory_var> 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;
}

2
src/sat/smt/array_diagnostics.cpp
View file

@ -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);

9
src/sat/smt/array_internalize.cpp
View file

@ -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) {

41
src/sat/smt/array_model.cpp
View file

@ -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;
}

8
src/sat/smt/array_solver.h
View file

@ -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<app*, func_decl*> mk_epsilon(sort* s);
void collect_shared_vars(sbuffer<theory_var>& 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<expr> m_else_values; //
svector<int> 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; }
};
}

3
src/sat/smt/bv_internalize.cpp
View file

@ -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);
}
}

34
src/sat/smt/bv_solver.cpp
View file

@ -673,25 +673,33 @@ namespace bv {
for (theory_var i = 0; i < static_cast<theory_var>(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;
}

13
src/sat/smt/bv_solver.h
View file

@ -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<std::pair<atom*, eq_occurs*>> 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; }
};

56
src/sat/smt/euf_internalize.cpp
View file

@ -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;
}
}
}

43
src/sat/smt/euf_model.cpp
View file

@ -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();

76
src/sat/smt/euf_solver.cpp
View file

@ -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<euf::enode> 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);

11
src/sat/smt/euf_solver.h
View file

@ -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<enode> 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);

12
src/sat/smt/q_ematch.cpp
View file

@ -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 {

22
src/sat/smt/q_eval.cpp
View file

@ -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;
}

16
src/sat/smt/q_mam.cpp
View file

@ -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));

2
src/sat/smt/q_mbi.cpp
View file

@ -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) {

10
src/sat/smt/q_model_fixer.cpp
View file

@ -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());
}

11
src/sat/smt/recfun_solver.cpp
View file

@ -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<scoped_ptr_vector<propagation_item>>(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;
}

2
src/sat/smt/sat_dual_solver.cpp
View file

@ -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());
}

35
src/sat/smt/sat_internalizer.h Normal file
View file

@ -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<expr, sat::bool_var>* r) = 0;
};
}

15
src/sat/smt/sat_smt.h
View file

@ -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<expr, sat::bool_var>* r) = 0;
};
class constraint_base {
extension* m_ex;
unsigned m_mem[0];

7
src/sat/smt/sat_th.cpp
View file

@ -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() {

16
src/sat/smt/user_solver.cpp
View file

@ -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<unsigned>(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";

2
src/sat/smt/user_solver.h
View file

@ -79,6 +79,8 @@ namespace user {
sat::justification mk_justification(unsigned propagation_index);
void validate_propagation();
public:
solver(euf::solver& ctx);

1
src/sat/tactic/CMakeLists.txt
View file

@ -1,6 +1,7 @@
z3_add_component(sat_tactic
SOURCES
goal2sat.cpp
sat2goal.cpp
sat_tactic.cpp
COMPONENT_DEPENDENCIES
sat

303
src/sat/tactic/goal2sat.cpp
View file

@ -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<generic_model_converter*>(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<expr, bool>& 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>& 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>& mc, sat::solver_core const & s, sat::clause_vector const& clauses, goal & r, bool asserted) {
ptr_buffer<expr> 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> & 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<sat::solver::bin_clause> 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<expr_ref(sat::literal)> l2e = [&](sat::literal lit) {
return expr_ref(lit2expr(mc, lit), m);
};
expr_ref_vector fmls(m);
pb::solver* ba = dynamic_cast<pb::solver*>(ext);
if (ba) {
ba->to_formulas(l2e, fmls);
}
else
dynamic_cast<euf::solver*>(ext)->to_formulas(l2e, fmls);
for (expr* f : fmls)
r.assert_expr(f);
}
}
void add_clause(ref<mc>& 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>& 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> & mc) {
imp proc(g.m(), p);
scoped_set_imp set(this, &proc);
proc(t, m, g, mc);
}

57
src/sat/tactic/goal2sat.h
View file

@ -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<expr, bool>& 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> & mc);
};

331
src/sat/tactic/sat2goal.cpp Normal file
View file

@ -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<sstream>
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<generic_model_converter*>(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<expr, bool>& 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>& 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>& mc, sat::solver const & s, sat::clause_vector const& clauses, goal & r, bool asserted) {
ptr_buffer<expr> 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> & 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<sat::solver::bin_clause> 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<expr_ref(sat::literal)> l2e = [&](sat::literal lit) {
return expr_ref(lit2expr(mc, lit), m);
};
expr_ref_vector fmls(m);
pb::solver* ba = dynamic_cast<pb::solver*>(ext);
if (ba) {
ba->to_formulas(l2e, fmls);
}
else
dynamic_cast<euf::solver*>(ext)->to_formulas(l2e, fmls);
for (expr* f : fmls)
r.assert_expr(f);
}
}
void add_clause(ref<mc>& 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>& 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> & mc) {
imp proc(g.m(), p);
scoped_set_imp set(this, &proc);
proc(t, m, g, mc);
}

84
src/sat/tactic/sat2goal.h Normal file
View file

@ -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<expr, bool>& 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> & mc);
};

3
src/sat/tactic/sat_tactic.cpp
View file

@ -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<sat::solver_core> m_solver;
scoped_ptr<sat::solver> m_solver;
params_ref m_params;
imp(ast_manager & _m, params_ref const & p):

1
src/shell/dimacs_frontend.cpp
View file

@ -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"

4
src/smt/mam.cpp
View file

@ -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);
}

20
src/smt/params/dyn_ack_params.h
View file

@ -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);
}

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

@ -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'),

1
src/smt/params/theory_arith_params.cpp
View file

@ -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<bound_prop_mode>(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();

138
src/smt/params/theory_arith_params.h
View file

@ -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);
}

40
src/smt/params/theory_array_params.h
View file

@ -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);

32
src/smt/params/theory_bv_params.h
View file

@ -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);
}

11
src/smt/params/theory_pb_params.h
View file

@ -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);

10
src/smt/params/theory_seq_params.h
View file

@ -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);
}

48
src/smt/params/theory_str_params.h
View file

@ -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);
}

4
src/smt/smt_context_inv.cpp
View file

@ -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;
}

14
src/smt/theory_array_base.cpp
View file

@ -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;
}

34
src/smt/theory_char.cpp
View file

@ -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.

2
src/smt/theory_char.h
View file

@ -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);

4
src/smt/theory_lra.cpp
View file

@ -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);

5
src/smt/user_propagator.cpp
View file

@ -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(

9
src/solver/assertions/asserted_formulas.cpp
View file

@ -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)

13
src/solver/parallel_tactic.cpp
View file

@ -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<std::mutex> 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<cube_var>& 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<std::mutex> lock(m_mutex);
s1 = s.clone();
}
s1->inc_width(width);
m_queue.add_task(s1);
}

23
src/tactic/core/solve_eqs_tactic.cpp
View file

@ -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) {

22
src/tactic/fd_solver/smtfd_solver.cpp
View file

@ -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()) {

2
src/tactic/portfolio/solver_subsumption_tactic.h
View file

@ -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)")
*/

6
src/test/pdd_solver.cpp
View file

@ -182,7 +182,7 @@ namespace dd {
void collect_id2var(unsigned_vector& id2var, expr_ref_vector const& fmls) {
svector<std::pair<unsigned, unsigned>> 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);
}

Some files were not shown because too many files have changed in this diff Show more