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

disable dotnet in ci script. It seems to get turned on even if dotnet bindings are not requested

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-09-11 03:14:31 -07:00
parent 1e11b62bc6
commit 36a14a354a
4 changed files with 34 additions and 14 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

22
contrib/ci/scripts/build_z3_cmake.sh
View file

@ -78,17 +78,17 @@ else
fi
# .NET bindings?
if [ "X${DOTNET_BINDINGS}" = "X1" ]; then
ADDITIONAL_Z3_OPTS+=( \
'-DBUILD_DOTNET_BINDINGS=ON' \
'-DINSTALL_DOTNET_BINDINGS=ON' \
)
else
ADDITIONAL_Z3_OPTS+=( \
'-DBUILD_DOTNET_BINDINGS=OFF' \
'-DINSTALL_DOTNET_BINDINGS=OFF' \
)
fi
#if [ "X${DOTNET_BINDINGS}" = "X1" ]; then
# ADDITIONAL_Z3_OPTS+=( \
# '-DBUILD_DOTNET_BINDINGS=ON' \
# '-DINSTALL_DOTNET_BINDINGS=ON' \
# )
#else
# ADDITIONAL_Z3_OPTS+=( \
# '-DBUILD_DOTNET_BINDINGS=OFF' \
# '-DINSTALL_DOTNET_BINDINGS=OFF' \
# )
#fi
# Java bindings?
if [ "X${JAVA_BINDINGS}" = "X1" ]; then

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

@ -2176,6 +2176,8 @@ class ArithRef(ExprRef):
>>> (x * y).sort()
Real
"""
if isinstance(other, BoolRef):
return If(other, self, 0)
a, b = _coerce_exprs(self, other)
return ArithRef(_mk_bin(Z3_mk_mul, a, b), self.ctx)

12
src/smt/smt_farkas_util.cpp
View file

@ -312,6 +312,13 @@ namespace smt {
}
expr_ref farkas_util::get() {
TRACE("arith",
for (unsigned i = 0; i < m_coeffs.size(); ++i) {
tout << m_coeffs[i] << " * (" << mk_pp(m_ineqs[i].get(), m) << ") ";
}
tout << "\n";
);
m_normalize_factor = rational::one();
expr_ref res(m);
if (m_coeffs.empty()) {
@ -330,13 +337,12 @@ namespace smt {
partition_ineqs();
expr_ref_vector lits(m);
unsigned lo = 0;
for (unsigned i = 0; i < m_his.size(); ++i) {
unsigned hi = m_his[i];
for (unsigned hi : m_his) {
lits.push_back(extract_consequence(lo, hi));
lo = hi;
}
bool_rewriter(m).mk_or(lits.size(), lits.c_ptr(), res);
IF_VERBOSE(2, { if (lits.size() > 1) { verbose_stream() << "combined lemma: " << mk_pp(res, m) << "\n"; } });
IF_VERBOSE(2, { if (lits.size() > 1) { verbose_stream() << "combined lemma: " << res << "\n"; } });
}
else {
res = extract_consequence(0, m_coeffs.size());

12
src/test/pb2bv.cpp
View file

@ -18,6 +18,7 @@ Copyright (c) 2015 Microsoft Corporation
#include "ast/rewriter/th_rewriter.h"
#include "tactic/fd_solver/fd_solver.h"
#include "solver/solver.h"
#include "ast/arith_decl_plugin.h"
static void test1() {
ast_manager m;
@ -194,9 +195,20 @@ static void test3() {
}
}
static void test4() {
ast_manager m;
reg_decl_plugins(m);
arith_util arith(m);
expr_ref a(m.mk_const(symbol("a"), arith.mk_int()), m);
expr_ref b(m.mk_const(symbol("b"), arith.mk_int()), m);
expr_ref eq(m.mk_eq(a,b), m);
std::cout << "is_atom: " << is_atom(m, eq) << "\n";
}
void tst_pb2bv() {
test1();
test2();
test3();
test4();
}