⚙ D54974 [analyzer] Cleanup constructors in the Z3 backend (original) (raw)

Show First 20 Lines • Show All 71 Lines • ▼ Show 20 Lines

class Z3Sort : public SMTSort {

friend class Z3Solver;

Z3Context &Context;

Z3_sort Sort;

public:

/// Default constructor, mainly used by make_shared

Z3Sort(Z3Context &C, Z3_sort ZS) : SMTSort(), Context(C), Sort(ZS) {

Z3Sort(Z3Context &C, Z3_sort ZS) : Context(C), Sort(ZS) {

Z3_inc_ref(Context.Context, reinterpret_cast<Z3_ast>(Sort));

}

/// Override implicit copy constructor for correct reference counting.

Z3Sort(const Z3Sort &Copy)

Z3Sort(const Z3Sort &Other) : Context(Other.Context), Sort(Other.Sort) {

: SMTSort(), Context(Copy.Context), Sort(Copy.Sort) {

Z3_inc_ref(Context.Context, reinterpret_cast<Z3_ast>(Sort));

}

/// Provide move constructor

/// Override implicit copy assignment constructor for correct reference

Z3Sort(Z3Sort &&Move) : SMTSort(), Context(Move.Context), Sort(nullptr) {

/// counting.

*this = std::move(Move);

Z3Sort &operator=(const Z3Sort &Other) {

}

Z3_inc_ref(Context.Context, reinterpret_cast<Z3_ast>(Other.Sort));

/// Provide move assignment constructor

Z3Sort &operator=(Z3Sort &&Move) {

if (this != &Move) {

if (Sort)

Z3_dec_ref(Context.Context, reinterpret_cast<Z3_ast>(Sort));

Sort = Move.Sort;

Sort = Other.Sort;

Move.Sort = nullptr;

}

return *this;

}

Z3Sort(Z3Sort &&Other) = delete;

Z3Sort &operator=(Z3Sort &&Other) = delete;

~Z3Sort() {

if (Sort)

Z3_dec_ref(Context.Context, reinterpret_cast<Z3_ast>(Sort));

}

bool isBitvectorSortImpl() const override {

return (Z3_get_sort_kind(Context.Context, Sort) == Z3_BV_SORT);

}

Show All 15 Lines

return Z3_fpa_get_ebits(Context.Context, Sort) +

Z3_fpa_get_sbits(Context.Context, Sort);

}

bool equal_to(SMTSort const &Other) const override {

return Z3_is_eq_sort(Context.Context, Sort,

static_cast<const Z3Sort &>(Other).Sort);

}

Z3Sort &operator=(const Z3Sort &Move) {

Z3_inc_ref(Context.Context, reinterpret_cast<Z3_ast>(Move.Sort));

Z3_dec_ref(Context.Context, reinterpret_cast<Z3_ast>(Sort));

Sort = Move.Sort;

return *this;

}

void print(raw_ostream &OS) const override {

OS << Z3_sort_to_string(Context.Context, Sort);

}

}; // end class Z3Sort

static const Z3Sort &toZ3Sort(const SMTSort &S) {

return static_cast<const Z3Sort &>(S);

}

Show All 10 Lines

Z3Expr(Z3Context &C, Z3_ast ZA) : SMTExpr(), Context(C), AST(ZA) {

Z3_inc_ref(Context.Context, AST);

}

/// Override implicit copy constructor for correct reference counting.

Z3Expr(const Z3Expr &Copy) : SMTExpr(), Context(Copy.Context), AST(Copy.AST) {

Z3_inc_ref(Context.Context, AST);

}

/// Provide move constructor

/// Override implicit copy assignment constructor for correct reference

Z3Expr(Z3Expr &&Move) : SMTExpr(), Context(Move.Context), AST(nullptr) {

/// counting.

*this = std::move(Move);

Z3Expr &operator=(const Z3Expr &Other) {

}

Z3_inc_ref(Context.Context, Other.AST);

/// Provide move assignment constructor

Z3Expr &operator=(Z3Expr &&Move) {

if (this != &Move) {

if (AST)

Z3_dec_ref(Context.Context, AST);

AST = Move.AST;

AST = Other.AST;

Move.AST = nullptr;

}

return *this;

}

Z3Expr(Z3Expr &&Other) = delete;

Z3Expr &operator=(Z3Expr &&Other) = delete;

~Z3Expr() {

if (AST)

Z3_dec_ref(Context.Context, AST);

}

void Profile(llvm::FoldingSetNodeID &ID) const override {

ID.AddInteger(Z3_get_ast_hash(Context.Context, AST));

}

/// Comparison of AST equality, not model equivalence.

bool equal_to(SMTExpr const &Other) const override {

assert(Z3_is_eq_sort(Context.Context, Z3_get_sort(Context.Context, AST),

Z3_get_sort(Context.Context,

static_cast<const Z3Expr &>(Other).AST)) &&

"AST's must have the same sort");

return Z3_is_eq_ast(Context.Context, AST,

static_cast<const Z3Expr &>(Other).AST);

}

/// Override implicit move constructor for correct reference counting.

Z3Expr &operator=(const Z3Expr &Move) {

Z3_inc_ref(Context.Context, Move.AST);

Z3_dec_ref(Context.Context, AST);

AST = Move.AST;

return *this;

}

void print(raw_ostream &OS) const override {

OS << Z3_ast_to_string(Context.Context, AST);

}

}; // end class Z3Expr

static const Z3Expr &toZ3Expr(const SMTExpr &E) {

return static_cast<const Z3Expr &>(E);

}

class Z3Model {

friend class Z3Solver;

Z3Context &Context;

Z3_model Model;

public:

Z3Model(Z3Context &C, Z3_model ZM) : Context(C), Model(ZM) {

assert(C.Context != nullptr);

Z3_model_inc_ref(Context.Context, Model);

}

/// Override implicit copy constructor for correct reference counting.

Z3Model(const Z3Model &Copy) : Context(Copy.Context), Model(Copy.Model) {

Z3_model_inc_ref(Context.Context, Model);

}

/// Provide move constructor

Z3Model(const Z3Model &Other) = delete;

Z3Model(Z3Model &&Move) : Context(Move.Context), Model(nullptr) {

Z3Model(Z3Model &&Other) = delete;

*this = std::move(Move);

Z3Model &operator=(Z3Model &Other) = delete;

}

Z3Model &operator=(Z3Model &&Other) = delete;

/// Provide move assignment constructor

Z3Model &operator=(Z3Model &&Move) {

if (this != &Move) {

if (Model)

Z3_model_dec_ref(Context.Context, Model);

Model = Move.Model;

Move.Model = nullptr;

}

return *this;

}

~Z3Model() {

if (Model)

Z3_model_dec_ref(Context.Context, Model);

}

void print(raw_ostream &OS) const {

OS << Z3_model_to_string(Context.Context, Model);

▲ Show 20 Lines • Show All 42 Lines • ▼ Show 20 Lines

class Z3Solver : public SMTSolver {

friend class Z3ConstraintManager;

Z3Context Context;

Z3_solver Solver;

public:

Z3Solver() : SMTSolver(), Solver(Z3_mk_simple_solver(Context.Context)) {

Z3Solver() : Solver(Z3_mk_simple_solver(Context.Context)) {

Z3_solver_inc_ref(Context.Context, Solver);

}

/// Override implicit copy constructor for correct reference counting.

Z3Solver(const Z3Solver &Other) = delete;

Z3Solver(const Z3Solver &Copy)

Z3Solver(Z3Solver &&Other) = delete;

: SMTSolver(), Context(Copy.Context), Solver(Copy.Solver) {

Z3Solver &operator=(Z3Solver &Other) = delete;

Z3_solver_inc_ref(Context.Context, Solver);

Z3Solver &operator=(Z3Solver &&Other) = delete;

}

/// Provide move constructor

Z3Solver(Z3Solver &&Move)

: SMTSolver(), Context(Move.Context), Solver(nullptr) {

*this = std::move(Move);

}

/// Provide move assignment constructor

Z3Solver &operator=(Z3Solver &&Move) {

if (this != &Move) {

if (Solver)

Z3_solver_dec_ref(Context.Context, Solver);

Solver = Move.Solver;

Move.Solver = nullptr;

}

return *this;

}

~Z3Solver() {

if (Solver)

Z3_solver_dec_ref(Context.Context, Solver);

}

void addConstraint(const SMTExprRef &Exp) const override {

Z3_solver_assert(Context.Context, Solver, toZ3Expr(*Exp).AST);

▲ Show 20 Lines • Show All 457 Lines • ▼ Show 20 Lines

if (Sort->isBooleanSort()) {

Int.isUnsigned());

return true;

}

llvm_unreachable("Unsupported sort to integer!");

}

bool getInterpretation(const SMTExprRef &Exp, llvm::APSInt &Int) override {

Z3Model Model = getModel();

Z3Model Model(Context, Z3_solver_get_model(Context.Context, Solver));

Z3_func_decl Func = Z3_get_app_decl(

Context.Context, Z3_to_app(Context.Context, toZ3Expr(*Exp).AST));

if (Z3_model_has_interp(Context.Context, Model.Model, Func) != Z3_L_TRUE)

return false;

SMTExprRef Assign = newExprRef(

Z3Expr(Context,

Z3_model_get_const_interp(Context.Context, Model.Model, Func)));

SMTSortRef Sort = getSort(Assign);

return toAPSInt(Sort, Assign, Int, true);

}

bool getInterpretation(const SMTExprRef &Exp, llvm::APFloat &Float) override {

Z3Model Model = getModel();

Z3Model Model(Context, Z3_solver_get_model(Context.Context, Solver));

Z3_func_decl Func = Z3_get_app_decl(

Context.Context, Z3_to_app(Context.Context, toZ3Expr(*Exp).AST));

if (Z3_model_has_interp(Context.Context, Model.Model, Func) != Z3_L_TRUE)

return false;

SMTExprRef Assign = newExprRef(

Z3Expr(Context,

Z3_model_get_const_interp(Context.Context, Model.Model, Func)));

Show All 14 Lines

public:

void push() override { return Z3_solver_push(Context.Context, Solver); }

void pop(unsigned NumStates = 1) override {

assert(Z3_solver_get_num_scopes(Context.Context, Solver) >= NumStates);

return Z3_solver_pop(Context.Context, Solver, NumStates);

}

/// Get a model from the solver. Caller should check the model is

/// satisfiable.

Z3Model getModel() {

return Z3Model(Context, Z3_solver_get_model(Context.Context, Solver));

}

bool isFPSupported() override { return true; }

/// Reset the solver and remove all constraints.

void reset() override { Z3_solver_reset(Context.Context, Solver); }

void print(raw_ostream &OS) const override {

OS << Z3_solver_to_string(Context.Context, Solver);

}

Show All 36 Lines