diff --git a/src/api/dll/dll.cpp b/src/api/dll/dll.cpp index a0bd25d2e..74dc48153 100644 --- a/src/api/dll/dll.cpp +++ b/src/api/dll/dll.cpp @@ -15,16 +15,16 @@ Copyright (c) 2015 Microsoft Corporation BOOL APIENTRY DllMain( HMODULE hModule, DWORD ul_reason_for_call, LPVOID lpReserved - ) + ) { - switch (ul_reason_for_call) - { - case DLL_PROCESS_ATTACH: - case DLL_THREAD_ATTACH: - case DLL_THREAD_DETACH: - case DLL_PROCESS_DETACH: - break; - } + switch (ul_reason_for_call) + { + case DLL_PROCESS_ATTACH: + case DLL_THREAD_ATTACH: + case DLL_THREAD_DETACH: + case DLL_PROCESS_DETACH: + break; + } return TRUE; } diff --git a/src/api/ml/z3native_stubs.h b/src/api/ml/z3native_stubs.h index ef81ac239..ec498dafe 100644 --- a/src/api/ml/z3native_stubs.h +++ b/src/api/ml/z3native_stubs.h @@ -36,5 +36,5 @@ Notes: #define DLL_LOCAL #endif #endif - + #endif diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp index cae357a32..bc0364994 100644 --- a/src/ast/fpa/fpa2bv_converter.cpp +++ b/src/ast/fpa/fpa2bv_converter.cpp @@ -3332,18 +3332,18 @@ void fpa2bv_converter::mk_to_bv(func_decl * f, unsigned num, expr * const * args dbg_decouple("fpa2bv_to_bv_inc", inc); dbg_decouple("fpa2bv_to_bv_pre_rounded", pre_rounded); - pre_rounded = m.mk_ite(x_is_neg, m_bv_util.mk_bv_neg(pre_rounded), pre_rounded); + pre_rounded = m.mk_ite(x_is_neg, m_bv_util.mk_bv_neg(pre_rounded), pre_rounded); - expr_ref ll(m), ul(m), in_range(m); + expr_ref ll(m), ul(m), in_range(m); if (!is_signed) { - ll = m_bv_util.mk_numeral(0, bv_sz+3); + ll = m_bv_util.mk_numeral(0, bv_sz+3); ul = m_bv_util.mk_zero_extend(3, m_bv_util.mk_numeral(-1, bv_sz)); } else { ll = m_bv_util.mk_sign_extend(3, m_bv_util.mk_concat(bv1, m_bv_util.mk_numeral(0, bv_sz-1))); ul = m_bv_util.mk_zero_extend(4, m_bv_util.mk_numeral(-1, bv_sz-1)); } - in_range = m.mk_and(m_bv_util.mk_sle(ll, pre_rounded), m_bv_util.mk_sle(pre_rounded, ul)); + in_range = m.mk_and(m_bv_util.mk_sle(ll, pre_rounded), m_bv_util.mk_sle(pre_rounded, ul)); dbg_decouple("fpa2bv_to_bv_in_range", in_range); expr_ref rounded(m); diff --git a/src/ast/rewriter/bit2int.h b/src/ast/rewriter/bit2int.h index fe15d1ec5..fbbf2e6d1 100644 --- a/src/ast/rewriter/bit2int.h +++ b/src/ast/rewriter/bit2int.h @@ -75,7 +75,7 @@ protected: bool mk_mul(expr* a, expr* b, expr_ref& result); bool mk_comp(eq_type ty, expr* e1, expr* e2, expr_ref& result); bool mk_add(expr* e1, expr* e2, expr_ref& result); - + expr * get_cached(expr * n) const; bool is_cached(expr * n) const { return get_cached(n) != 0; } void cache_result(expr * n, expr * r); diff --git a/src/ast/rewriter/bv_bounds.h b/src/ast/rewriter/bv_bounds.h index 3d8ec9ebb..4a7226fa7 100644 --- a/src/ast/rewriter/bv_bounds.h +++ b/src/ast/rewriter/bv_bounds.h @@ -38,7 +38,7 @@ public: bv_bounds(ast_manager& m) : m_m(m), m_bv_util(m), m_okay(true) {}; ~bv_bounds(); public: // bounds addition methods - br_status rewrite(unsigned limit, func_decl * f, unsigned num, expr * const * args, expr_ref& result); + br_status rewrite(unsigned limit, func_decl * f, unsigned num, expr * const * args, expr_ref& result); /** \brief Add a constraint to the system. @@ -82,7 +82,7 @@ protected: bv_util m_bv_util; bool m_okay; bool is_sat(app * v); - bool is_sat_core(app * v); +bool is_sat_core(app * v); inline bool in_range(app *v, numeral l); inline bool is_constant_add(unsigned bv_sz, expr * e, app*& v, numeral& val); void record_singleton(app * v, numeral& singleton_value); @@ -94,7 +94,7 @@ protected: inline bool bv_bounds::is_okay() { return m_okay; } inline bool bv_bounds::to_bound(const expr * e) const { - return is_app(e) && m_bv_util.is_bv(e) + return is_app(e) && m_bv_util.is_bv(e) && !m_bv_util.is_bv_add(e) && !m_bv_util.is_numeral(e); } diff --git a/src/duality/duality.h b/src/duality/duality.h index 0ef6be30e..657fa18b4 100644 --- a/src/duality/duality.h +++ b/src/duality/duality.h @@ -21,6 +21,7 @@ #pragma once #include "duality/duality_wrapper.h" +#include #include #include @@ -41,9 +42,9 @@ namespace Duality { typedef expr Term; Z3User(context &_ctx) : ctx(_ctx){} - + const char *string_of_int(int n); - + Term conjoin(const std::vector &args); Term sum(const std::vector &args); @@ -130,58 +131,58 @@ namespace Duality { /** This class represents a relation post-fixed point (RPFP) problem as * a "problem graph". The graph consists of Nodes and hyper-edges. - * + * * A node consists of * - Annotation, a symbolic relation * - Bound, a symbolic relation giving an upper bound on Annotation - * + * * * A hyper-edge consists of: * - Children, a sequence of children Nodes, * - F, a symbolic relational transformer, * - Parent, a single parent Node. - * + * * The graph is "solved" when: * - For every Node n, n.Annotation subseteq n.Bound * - For every hyperedge e, e.F(e.Children.Annotation) subseteq e.Parent.Annotation - * + * * where, if x is a sequence of Nodes, x.Annotation is the sequences * of Annotations of the nodes in the sequence. - * + * * A symbolic Transformer consists of * - RelParams, a sequence of relational symbols * - IndParams, a sequence of individual symbols * - Formula, a formula over RelParams and IndParams - * + * * A Transformer t represents a function that takes sequence R of relations * and yields the relation lambda (t.Indparams). Formula(R/RelParams). - * + * * As a special case, a nullary Transformer (where RelParams is the empty sequence) * represents a fixed relation. - * + * * An RPFP consists of * - Nodes, a set of Nodes * - Edges, a set of hyper-edges * - Context, a prover context that contains formula AST's - * + * * Multiple RPFP's can use the same Context, but you should be careful - * that only one RPFP asserts constraints in the context at any time. - * + * that only one RPFP asserts constraints in the context at any time. + * * */ class RPFP : public Z3User { public: - + class Edge; class Node; bool HornClauses; - + /** Interface class for interpolating solver. */ class LogicSolver { public: - + context *ctx; /** Z3 context for formulas */ solver *slvr; /** Z3 solver */ bool need_goals; /** Can the solver use the goal tree to optimize interpolants? */ @@ -191,7 +192,7 @@ namespace Duality { "assumptions" are currently asserted in the solver. The return value indicates whether the assertions are satisfiable. In the UNSAT case, a tree interpolant is returned in "interpolants". - In the SAT case, a model is returned. + In the SAT case, a model is returned. */ virtual @@ -201,7 +202,7 @@ namespace Duality { TermTree *goals = 0, bool weak = false ) = 0; - + /** Declare a constant in the background theory. */ virtual void declare_constant(const func_decl &f) = 0; @@ -319,7 +320,7 @@ namespace Duality { virtual void declare_constant(const func_decl &f){ bckg.insert(f); } - + /** Is this a background constant? */ virtual bool is_constant(const func_decl &f){ return bckg.find(f) != bckg.end(); @@ -344,9 +345,9 @@ namespace Duality { static iZ3LogicSolver *CreateLogicSolver(config &_config){ return new iZ3LogicSolver(_config); } -#endif +#endif - /** Create a logic solver from a low-level Z3 context. + /** Create a logic solver from a low-level Z3 context. Only use this if you know what you're doing. */ static iZ3LogicSolver *CreateLogicSolver(context c){ return new iZ3LogicSolver(c); @@ -357,7 +358,7 @@ namespace Duality { protected: int nodeCount; int edgeCount; - + class stack_entry { public: @@ -365,8 +366,8 @@ namespace Duality { std::list nodes; std::list > constraints; }; - - + + public: model dualModel; protected: @@ -375,14 +376,14 @@ namespace Duality { std::vector axioms; // only saved here for printing purposes solver &aux_solver; hash_set *proof_core; - + public: /** Construct an RPFP graph with a given interpolating prover context. It is allowed to have multiple RPFP's use the same context, but you should never have teo RPFP's with the same conext asserting nodes or edges at the same time. Note, if you create axioms in one RPFP, them create a second RPFP with the same context, the second will - inherit the axioms. + inherit the axioms. */ RPFP(LogicSolver *_ls) : Z3User(*(_ls->ctx)), dualModel(*(_ls->ctx)), aux_solver(_ls->aux_solver) @@ -396,7 +397,7 @@ namespace Duality { } virtual ~RPFP(); - + /** Symbolic representation of a relational transformer */ class Transformer { @@ -406,12 +407,12 @@ namespace Duality { Term Formula; RPFP *owner; hash_map labels; - + Transformer *Clone() { return new Transformer(*this); } - + void SetEmpty(){ Formula = owner->ctx.bool_val(false); } @@ -451,7 +452,7 @@ namespace Duality { void Complement(){ Formula = !Formula; } - + void Simplify(){ Formula = Formula.simplify(); } @@ -459,7 +460,7 @@ namespace Duality { Transformer(const std::vector &_RelParams, const std::vector &_IndParams, const Term &_Formula, RPFP *_owner) : RelParams(_RelParams), IndParams(_IndParams), Formula(_Formula) {owner = _owner;} }; - + /** Create a symbolic transformer. */ Transformer CreateTransformer(const std::vector &_RelParams, const std::vector &_IndParams, const Term &_Formula) { @@ -469,13 +470,13 @@ namespace Duality { // t.labels = foo.Item2; return Transformer(_RelParams,_IndParams,_Formula,this); } - + /** Create a relation (nullary relational transformer) */ Transformer CreateRelation(const std::vector &_IndParams, const Term &_Formula) { return CreateTransformer(std::vector(), _IndParams, _Formula); } - + /** A node in the RPFP graph */ class Node { @@ -491,17 +492,17 @@ namespace Duality { Term dual; Node *map; unsigned recursion_bound; - + Node(const FuncDecl &_Name, const Transformer &_Annotation, const Transformer &_Bound, const Transformer &_Underapprox, const Term &_dual, RPFP *_owner, int _number) : Name(_Name), Annotation(_Annotation), Bound(_Bound), Underapprox(_Underapprox), dual(_dual) {owner = _owner; number = _number; Outgoing = 0; recursion_bound = UINT_MAX;} }; - + /** Create a node in the graph. The input is a term R(v_1...v_n) * where R is an arbitrary relational symbol and v_1...v_n are * arbitary distinct variables. The names are only of mnemonic value, * however, the number and type of arguments determine the type * of the relation at this node. */ - + Node *CreateNode(const Term &t) { std::vector _IndParams; @@ -517,9 +518,9 @@ namespace Duality { nodes.push_back(n); return n; } - + /** Clone a node (can be from another graph). */ - + Node *CloneNode(Node *old) { Node *n = new Node(old->Name, @@ -534,7 +535,7 @@ namespace Duality { n->map = old; return n; } - + /** Delete a node. You can only do this if not connected to any edges.*/ void DeleteNode(Node *node){ if(node->Outgoing || !node->Incoming.empty()) @@ -549,7 +550,7 @@ namespace Duality { } /** This class represents a hyper-edge in the RPFP graph */ - + class Edge { public: @@ -565,15 +566,15 @@ namespace Duality { Edge *map; Term labeled; std::vector constraints; - + Edge(Node *_Parent, const Transformer &_F, const std::vector &_Children, RPFP *_owner, int _number) : F(_F), Parent(_Parent), Children(_Children), dual(expr(_owner->ctx)) { owner = _owner; number = _number; } }; - - + + /** Create a hyper-edge. */ Edge *CreateEdge(Node *_Parent, const Transformer &_F, const std::vector &_Children) { @@ -584,8 +585,8 @@ namespace Duality { edges.push_back(e); return e; } - - + + /** Delete a hyper-edge and unlink it from any nodes. */ void DeleteEdge(Edge *edge){ if(edge->Parent) @@ -607,19 +608,19 @@ namespace Duality { } delete edge; } - + /** Create an edge that lower-bounds its parent. */ Edge *CreateLowerBoundEdge(Node *_Parent) { return CreateEdge(_Parent, _Parent->Annotation, std::vector()); } - + /** For incremental solving, asserts the constraint associated * with this edge in the SMT context. If this edge is removed, * you must pop the context accordingly. The second argument is * the number of pushes we are inside. */ - + virtual void AssertEdge(Edge *e, int persist = 0, bool with_children = false, bool underapprox = false); /* Constrain an edge by the annotation of one of its children. */ @@ -629,19 +630,19 @@ namespace Duality { /** For incremental solving, asserts the negation of the upper bound associated * with a node. * */ - + void AssertNode(Node *n); - /** Assert a constraint on an edge in the SMT context. + /** Assert a constraint on an edge in the SMT context. */ void ConstrainEdge(Edge *e, const Term &t); - + /** Fix the truth values of atomic propositions in the given edge to their values in the current assignment. */ void FixCurrentState(Edge *root); - + void FixCurrentStateFull(Edge *edge, const expr &extra); - + void FixCurrentStateFull(Edge *edge, const std::vector &assumps, const hash_map &renaming); /** Declare a constant in the background theory. */ @@ -660,78 +661,78 @@ namespace Duality { #if 0 /** Do not call this. */ - + void RemoveAxiom(const Term &t); #endif /** Solve an RPFP graph. This means either strengthen the annotation * so that the bound at the given root node is satisfied, or - * show that this cannot be done by giving a dual solution - * (i.e., a counterexample). - * + * show that this cannot be done by giving a dual solution + * (i.e., a counterexample). + * * In the current implementation, this only works for graphs that * are: * - tree-like - * + * * - closed. - * + * * In a tree-like graph, every nod has out most one incoming and one out-going edge, * and there are no cycles. In a closed graph, every node has exactly one out-going * edge. This means that the leaves of the tree are all hyper-edges with no * children. Such an edge represents a relation (nullary transformer) and thus * a lower bound on its parent. The parameter root must be the root of this tree. - * + * * If Solve returns LBool.False, this indicates success. The annotation of the tree - * has been updated to satisfy the upper bound at the root. - * + * has been updated to satisfy the upper bound at the root. + * * If Solve returns LBool.True, this indicates a counterexample. For each edge, * you can then call Eval to determine the values of symbols in the transformer formula. * You can also call Empty on a node to determine if its value in the counterexample * is the empty relation. - * + * * \param root The root of the tree - * \param persist Number of context pops through which result should persist - * - * + * \param persist Number of context pops through which result should persist + * + * */ lbool Solve(Node *root, int persist); - + /** Same as Solve, but annotates only a single node. */ lbool SolveSingleNode(Node *root, Node *node); /** Get the constraint tree (but don't solve it) */ - + TermTree *GetConstraintTree(Node *root, Node *skip_descendant = 0); - + /** Dispose of the dual model (counterexample) if there is one. */ - + void DisposeDualModel(); /** Check satisfiability of asserted edges and nodes. Same functionality as - * Solve, except no primal solution (interpolant) is generated in the unsat case. */ - - check_result Check(Node *root, std::vector underapproxes = std::vector(), + * Solve, except no primal solution (interpolant) is generated in the unsat case. */ + + check_result Check(Node *root, std::vector underapproxes = std::vector(), std::vector *underapprox_core = 0); /** Update the model, attempting to make the propositional literals in assumps true. If possible, return sat, else return unsat and keep the old model. */ - + check_result CheckUpdateModel(Node *root, std::vector assumps); /** Determines the value in the counterexample of a symbol occuring in the transformer formula of * a given edge. */ - + Term Eval(Edge *e, Term t); - + /** Return the fact derived at node p in a counterexample. */ Term EvalNode(Node *p); - + /** Returns true if the given node is empty in the primal solution. For proecudure summaries, this means that the procedure is not called in the current counter-model. */ - + bool Empty(Node *p); /** Compute an underapproximation of every node in a tree rooted at "root", @@ -747,11 +748,11 @@ namespace Duality { void InterpolateByCases(Node *root, Node *node); /** Push a scope. Assertions made after Push can be undone by Pop. */ - + void Push(); /** Exception thrown when bad clause is encountered */ - + struct bad_clause { std::string msg; int i; @@ -777,7 +778,7 @@ namespace Duality { // thrown on internal error struct Bad { }; - + // thrown on more serious internal error struct ReallyBad { }; @@ -786,56 +787,56 @@ namespace Duality { struct greedy_reduce_failed {}; /** Pop a scope (see Push). Note, you cannot pop axioms. */ - + void Pop(int num_scopes); - + /** Erase the proof by performing a Pop, Push and re-assertion of all the popped constraints */ void PopPush(); /** Return true if the given edge is used in the proof of unsat. Can be called only after Solve or Check returns an unsat result. */ - + bool EdgeUsedInProof(Edge *edge); /** Convert a collection of clauses to Nodes and Edges in the RPFP. - + Predicate unknowns are uninterpreted predicates not occurring in the background theory. - - Clauses are of the form - + + Clauses are of the form + B => P(t_1,...,t_k) - + where P is a predicate unknown and predicate unknowns occur only positivey in H and only under existential quantifiers in prenex form. - + Each predicate unknown maps to a node. Each clause maps to an edge. Let C be a clause B => P(t_1,...,t_k) where the sequence of predicate unknowns occurring in B (in order of occurrence) is P_1..P_n. The clause maps to a transformer T where: - + T.Relparams = P_1..P_n T.Indparams = x_1...x+k T.Formula = B /\ t_1 = x_1 /\ ... /\ t_k = x_k - + Throws exception bad_clause(msg,i) if a clause i is in the wrong form. - + */ - + struct label_struct { symbol name; expr value; bool pos; - label_struct(const symbol &s, const expr &e, bool b) - : name(s), value(e), pos(b) {} + label_struct(const symbol &s, const expr &e, bool b) + : name(s), value(e), pos(b) {} }; - + #ifdef _WINDOWS __declspec(dllexport) #endif @@ -847,7 +848,7 @@ namespace Duality { void WriteCounterexample(std::ostream &s, Node *node); - enum FileFormat {DualityFormat, SMT2Format, HornFormat}; + enum FileFormat {DualityFormat, SMT2Format, HornFormat}; /** Write the RPFP to a file (currently in SMTLIB 1.2 format) */ void WriteProblemToFile(std::string filename, FileFormat format = DualityFormat); @@ -870,9 +871,9 @@ namespace Duality { /** Fuse a vector of transformers. If the total number of inputs of the transformers is N, then the result is an N-ary transfomer whose output is the union of the outputs of the given transformers. The is, suppose we have a vetor of transfoermers - {T_i(r_i1,...,r_iN(i) : i=1..M}. The the result is a transformer - - F(r_11,...,r_iN(1),...,r_M1,...,r_MN(M)) = + {T_i(r_i1,...,r_iN(i) : i=1..M}. The the result is a transformer + + F(r_11,...,r_iN(1),...,r_M1,...,r_MN(M)) = T_1(r_11,...,r_iN(1)) U ... U T_M(r_M1,...,r_MN(M)) */ @@ -921,7 +922,7 @@ namespace Duality { } protected: - + void ClearProofCore(){ if(proof_core) delete proof_core; @@ -929,7 +930,7 @@ namespace Duality { } Term SuffixVariable(const Term &t, int n); - + Term HideVariable(const Term &t, int n); void RedVars(Node *node, Term &b, std::vector &v); @@ -958,16 +959,16 @@ namespace Duality { #if 0 void WriteInterps(System.IO.StreamWriter f, TermTree t); -#endif +#endif void WriteEdgeVars(Edge *e, hash_map &memo, const Term &t, std::ostream &s); void WriteEdgeAssignment(std::ostream &s, Edge *e); - + // Scan the clause body for occurrences of the predicate unknowns - - Term ScanBody(hash_map &memo, + + Term ScanBody(hash_map &memo, const Term &t, hash_map &pmap, std::vector &res, @@ -1035,7 +1036,7 @@ namespace Duality { void ConstrainEdgeLocalized(Edge *e, const Term &t); void GreedyReduce(solver &s, std::vector &conjuncts); - + void NegateLits(std::vector &lits); expr SimplifyOr(std::vector &lits); @@ -1053,7 +1054,7 @@ namespace Duality { void GetGroundLitsUnderQuants(hash_set *memo, const Term &f, std::vector &res, int under); Term StrengthenFormulaByCaseSplitting(const Term &f, std::vector &case_lits); - + expr NegateLit(const expr &f); expr GetEdgeFormula(Edge *e, int persist, bool with_children, bool underapprox); @@ -1065,7 +1066,7 @@ namespace Duality { expr UnhoistPullRec(hash_map & memo, const expr &w, hash_map & init_defs, hash_map & const_params, hash_map &const_params_inv, std::vector &new_params); void AddParamsToTransformer(Transformer &trans, const std::vector ¶ms); - + expr AddParamsToApp(const expr &app, const func_decl &new_decl, const std::vector ¶ms); expr GetRelRec(hash_set &memo, const expr &t, const func_decl &rel); @@ -1081,7 +1082,7 @@ namespace Duality { void UnhoistLoop(Edge *loop_edge, Edge *init_edge); void Unhoist(); - + Term ElimIteRec(hash_map &memo, const Term &t, std::vector &cnsts); Term ElimIte(const Term &t); @@ -1089,11 +1090,11 @@ namespace Duality { void MarkLiveNodes(hash_map > &outgoing, hash_set &live_nodes, Node *node); virtual void slvr_add(const expr &e); - + virtual void slvr_pop(int i); virtual void slvr_push(); - + virtual check_result slvr_check(unsigned n = 0, expr * const assumptions = 0, unsigned *core_size = 0, expr *core = 0); virtual lbool ls_interpolate_tree(TermTree *assumptions, @@ -1105,14 +1106,14 @@ namespace Duality { virtual bool proof_core_contains(const expr &e); }; - + /** RPFP solver base class. */ class Solver { - + public: - + class Counterexample { private: RPFP *tree; @@ -1148,18 +1149,18 @@ namespace Duality { Counterexample &operator=(const Counterexample &); Counterexample(const Counterexample &); }; - + /** Solve the problem. You can optionally give an old counterexample to use as a guide. This is chiefly useful for abstraction refinement metholdologies, and is only used as a heuristic. */ - + virtual bool Solve() = 0; - + virtual Counterexample &GetCounterexample() = 0; - + virtual bool SetOption(const std::string &option, const std::string &value) = 0; - + /** Learn heuristic information from another solver. This is chiefly useful for abstraction refinement, when we want to solve a series of similar problems. */ @@ -1184,7 +1185,7 @@ namespace Duality { /** Object thrown on cancellation */ struct Canceled {}; - + /** Object thrown on incompleteness */ struct Incompleteness {}; }; @@ -1235,16 +1236,16 @@ namespace Duality { public: /** appends assumption literals for edge to lits. if with_children is true, - includes that annotation of the edge's children. - */ + includes that annotation of the edge's children. + */ void AssertEdgeCache(Edge *e, std::vector &lits, bool with_children = false); - + /** appends assumption literals for node to lits */ void AssertNodeCache(Node *, std::vector lits); /** check assumption lits, and return core */ check_result CheckCore(const std::vector &assumps, std::vector &core); - + /** Clone another RPFP into this one, keeping a map */ void Clone(RPFP *other); @@ -1287,7 +1288,7 @@ namespace Duality { uptr slvr; }; hash_map edge_solvers; - + #ifdef LIMIT_STACK_WEIGHT struct weight_counter { int val; @@ -1296,7 +1297,7 @@ namespace Duality { std::swap(val,other.val); } }; - + struct big_stack_entry { weight_counter weight_added; std::vector new_alits; @@ -1319,11 +1320,11 @@ namespace Duality { void ConstrainEdgeLocalizedCache(Edge *e, const Term &tl, std::vector &lits); virtual void slvr_add(const expr &e); - + virtual void slvr_pop(int i); virtual void slvr_push(); - + virtual check_result slvr_check(unsigned n = 0, expr * const assumptions = 0, unsigned *core_size = 0, expr *core = 0); virtual lbool ls_interpolate_tree(TermTree *assumptions, @@ -1348,7 +1349,7 @@ namespace Duality { scoped_solver_for_edge(RPFP_caching *_rpfp, Edge *edge, bool models = false, bool axioms = false){ rpfp = _rpfp; orig_slvr = rpfp->ls->slvr; - es = &(rpfp->SolverForEdge(edge,models,axioms)); + es = &(rpfp->SolverForEdge(edge,models,axioms)); rpfp->ls->slvr = es->slvr.get(); rpfp->AssumptionLits.swap(es->AssumptionLits); } diff --git a/src/duality/duality_wrapper.h b/src/duality/duality_wrapper.h index 8ea8017a2..96c49b36b 100644 --- a/src/duality/duality_wrapper.h +++ b/src/duality/duality_wrapper.h @@ -176,7 +176,7 @@ namespace Duality { m_datalog_fid = m().mk_family_id("datalog_relation"); } ~context() { } - + ast_manager &m() const {return *(ast_manager *)&mgr;} void set(char const * param, char const * value) { m_config.set(param,value); } @@ -186,13 +186,13 @@ namespace Duality { symbol str_symbol(char const * s); symbol int_symbol(int n); - + sort bool_sort(); sort int_sort(); sort real_sort(); sort bv_sort(unsigned sz); sort array_sort(sort d, sort r); - + func_decl function(symbol const & name, unsigned arity, sort const * domain, sort const & range); func_decl function(char const * name, unsigned arity, sort const * domain, sort const & range); func_decl function(char const * name, sort const & domain, sort const & range); @@ -210,22 +210,22 @@ namespace Duality { expr int_const(char const * name); expr real_const(char const * name); expr bv_const(char const * name, unsigned sz); - + expr bool_val(bool b); - + expr int_val(int n); expr int_val(unsigned n); expr int_val(char const * n); - + expr real_val(int n, int d); expr real_val(int n); expr real_val(unsigned n); expr real_val(char const * n); - + expr bv_val(int n, unsigned sz); expr bv_val(unsigned n, unsigned sz); expr bv_val(char const * n, unsigned sz); - + expr num_val(int n, sort const & s); expr mki(family_id fid, ::decl_kind dk, int n, ::expr **args); @@ -281,17 +281,17 @@ namespace Duality { object(object const & s):m_ctx(s.m_ctx) {} context & ctx() const { return *m_ctx; } friend void check_context(object const & a, object const & b) { assert(a.m_ctx == b.m_ctx); } - ast_manager &m() const {return m_ctx->m();} + ast_manager &m() const {return m_ctx->m();} }; class symbol : public object { ::symbol m_sym; public: - symbol(context & c, ::symbol s):object(c), m_sym(s) {} - symbol(symbol const & s):object(s), m_sym(s.m_sym) {} + symbol(context & c, ::symbol s):object(c), m_sym(s) {} + symbol(symbol const & s):object(s), m_sym(s.m_sym) {} symbol & operator=(symbol const & s) { m_ctx = s.m_ctx; m_sym = s.m_sym; return *this; } - operator ::symbol() const {return m_sym;} - std::string str() const { + operator ::symbol() const {return m_sym;} + std::string str() const { if (m_sym.is_numerical()) { std::ostringstream buffer; buffer << m_sym.get_num(); @@ -300,13 +300,13 @@ namespace Duality { else { return m_sym.bare_str(); } - } - friend std::ostream & operator<<(std::ostream & out, symbol const & s){ + } + friend std::ostream & operator<<(std::ostream & out, symbol const & s) { return out << s.str(); - } - friend bool operator==(const symbol &x, const symbol &y){ + } + friend bool operator==(const symbol &x, const symbol &y) { return x.m_sym == y.m_sym; - } + } }; class params : public config {}; @@ -318,7 +318,7 @@ namespace Duality { public: ::ast * const &raw() const {return _ast;} ast_i(context & c, ::ast *a = 0) : object(c) {_ast = a;} - + ast_i(){_ast = 0;} bool eq(const ast_i &other) const { return _ast == other._ast; @@ -345,19 +345,19 @@ namespace Duality { operator ::ast*() const { return raw(); } friend bool eq(ast const & a, ast const & b) { return a.raw() == b.raw(); } - + ast(context &c, ::ast *a = 0) : ast_i(c,a) { if(_ast) m().inc_ref(a); } - + ast() {} - + ast(const ast &other) : ast_i(other) { if(_ast) m().inc_ref(_ast); } - + ast &operator=(const ast &other) { if(_ast) m().dec_ref(_ast); @@ -367,7 +367,7 @@ namespace Duality { m().inc_ref(_ast); return *this; } - + ~ast(){ if(_ast) m().dec_ref(_ast); @@ -386,15 +386,15 @@ namespace Duality { sort & operator=(sort const & s) { return static_cast(ast::operator=(s)); } bool is_bool() const { return m().is_bool(*this); } - bool is_int() const { return ctx().get_sort_kind(*this) == IntSort; } - bool is_real() const { return ctx().get_sort_kind(*this) == RealSort; } + bool is_int() const { return ctx().get_sort_kind(*this) == IntSort; } + bool is_real() const { return ctx().get_sort_kind(*this) == RealSort; } bool is_arith() const; - bool is_array() const { return ctx().get_sort_kind(*this) == ArraySort; } - bool is_datatype() const; - bool is_relation() const; - bool is_finite_domain() const; + bool is_array() const { return ctx().get_sort_kind(*this) == ArraySort; } + bool is_datatype() const; + bool is_relation() const; + bool is_finite_domain() const; + - sort array_domain() const; sort array_range() const; @@ -404,7 +404,7 @@ namespace Duality { } }; - + class func_decl : public ast { public: func_decl() : ast() {} @@ -413,7 +413,7 @@ namespace Duality { func_decl(func_decl const & s):ast(s) {} operator ::func_decl*() const { return to_func_decl(*this); } func_decl & operator=(func_decl const & s) { return static_cast(ast::operator=(s)); } - + unsigned arity() const; sort domain(unsigned i) const; sort range() const; @@ -434,9 +434,9 @@ namespace Duality { expr operator()(expr const & a1, expr const & a2, expr const & a3, expr const & a4) const; expr operator()(expr const & a1, expr const & a2, expr const & a3, expr const & a4, expr const & a5) const; - func_decl get_func_decl_parameter(unsigned idx){ + func_decl get_func_decl_parameter(unsigned idx){ return func_decl(ctx(),to_func_decl(to_func_decl(raw())->get_parameters()[idx].get_ast())); - } + } }; @@ -447,8 +447,8 @@ namespace Duality { expr(context & c, ::ast *n):ast(c, n) {} expr(expr const & n):ast(n) {} expr & operator=(expr const & n) { return static_cast(ast::operator=(n)); } - operator ::expr*() const { return to_expr(raw()); } - unsigned get_id() const {return to_expr(raw())->get_id();} + operator ::expr*() const { return to_expr(raw()); } + unsigned get_id() const {return to_expr(raw())->get_id();} sort get_sort() const { return sort(ctx(),m().get_sort(to_expr(raw()))); } @@ -460,27 +460,27 @@ namespace Duality { bool is_datatype() const { return get_sort().is_datatype(); } bool is_relation() const { return get_sort().is_relation(); } bool is_finite_domain() const { return get_sort().is_finite_domain(); } - bool is_true() const {return is_app() && decl().get_decl_kind() == True; } + bool is_true() const {return is_app() && decl().get_decl_kind() == True; } bool is_numeral() const { return is_app() && decl().get_decl_kind() == OtherArith && m().is_unique_value(to_expr(raw())); - } - bool is_app() const {return raw()->get_kind() == AST_APP;} + } + bool is_app() const {return raw()->get_kind() == AST_APP;} bool is_quantifier() const {return raw()->get_kind() == AST_QUANTIFIER;} bool is_var() const {return raw()->get_kind() == AST_VAR;} - bool is_label (bool &pos,std::vector &names) const ; - bool is_ground() const {return to_app(raw())->is_ground();} - bool has_quantifiers() const {return to_app(raw())->has_quantifiers();} - bool has_free(int idx) const { + bool is_label (bool &pos,std::vector &names) const ; + bool is_ground() const {return to_app(raw())->is_ground();} + bool has_quantifiers() const {return to_app(raw())->has_quantifiers();} + bool has_free(int idx) const { used_vars proc; proc.process(to_expr(raw())); return proc.contains(idx); - } - unsigned get_max_var_idx_plus_1() const { + } + unsigned get_max_var_idx_plus_1() const { used_vars proc; proc.process(to_expr(raw())); return proc.get_max_found_var_idx_plus_1(); - } + } // operator Z3_app() const { assert(is_app()); return reinterpret_cast(m_ast); } func_decl decl() const {return func_decl(ctx(),to_app(raw())->get_decl());} @@ -493,11 +493,11 @@ namespace Duality { return 1; case AST_VAR: return 0; - default:; + default:; } SASSERT(0); return 0; - } + } expr arg(unsigned i) const { ast_kind dk = raw()->get_kind(); switch(dk){ @@ -509,25 +509,25 @@ namespace Duality { } assert(0); return expr(); - } + } expr body() const { return ctx().cook(to_quantifier(raw())->get_expr()); - } + } friend expr operator!(expr const & a) { // ::expr *e = a; return expr(a.ctx(),a.m().mk_app(a.m().get_basic_family_id(),OP_NOT,a)); - } + } friend expr operator&&(expr const & a, expr const & b) { return expr(a.ctx(),a.m().mk_app(a.m().get_basic_family_id(),OP_AND,a,b)); - } + } friend expr operator||(expr const & a, expr const & b) { return expr(a.ctx(),a.m().mk_app(a.m().get_basic_family_id(),OP_OR,a,b)); } - + friend expr implies(expr const & a, expr const & b) { return expr(a.ctx(),a.m().mk_app(a.m().get_basic_family_id(),OP_IMPLIES,a,b)); } @@ -546,12 +546,12 @@ namespace Duality { friend expr operator*(expr const & a, expr const & b) { return a.ctx().make(Times,a,b); // expr(a.ctx(),a.m().mk_app(a.m().get_basic_family_id(),OP_MUL,a,b)); - } + } friend expr operator/(expr const & a, expr const & b) { return a.ctx().make(Div,a,b); // expr(a.ctx(),a.m().mk_app(a.m().get_basic_family_id(),OP_DIV,a,b)); } - + friend expr operator-(expr const & a) { return a.ctx().make(Uminus,a); // expr(a.ctx(),a.m().mk_app(a.m().get_basic_family_id(),OP_UMINUS,a)); } @@ -562,71 +562,71 @@ namespace Duality { friend expr operator<=(expr const & a, expr const & b) { return a.ctx().make(Leq,a,b); // expr(a.ctx(),a.m().mk_app(a.m().get_basic_family_id(),OP_LE,a,b)); - } + } friend expr operator>=(expr const & a, expr const & b) { return a.ctx().make(Geq,a,b); //expr(a.ctx(),a.m().mk_app(a.m().get_basic_family_id(),OP_GE,a,b)); } - + friend expr operator<(expr const & a, expr const & b) { return a.ctx().make(Lt,a,b); expr(a.ctx(),a.m().mk_app(a.m().get_basic_family_id(),OP_LT,a,b)); } - + friend expr operator>(expr const & a, expr const & b) { return a.ctx().make(Gt,a,b); expr(a.ctx(),a.m().mk_app(a.m().get_basic_family_id(),OP_GT,a,b)); - } + } expr simplify() const; expr simplify(params const & p) const; - + expr qe_lite() const; - expr qe_lite(const std::set &idxs, bool index_of_bound) const; + expr qe_lite(const std::set &idxs, bool index_of_bound) const; - friend expr clone_quantifier(const expr &, const expr &); + friend expr clone_quantifier(const expr &, const expr &); friend expr clone_quantifier(const expr &q, const expr &b, const std::vector &patterns); - friend expr clone_quantifier(decl_kind, const expr &, const expr &); + friend expr clone_quantifier(decl_kind, const expr &, const expr &); friend std::ostream & operator<<(std::ostream & out, expr const & m){ m.ctx().print_expr(out,m); return out; - } + } - void get_patterns(std::vector &pats) const ; + void get_patterns(std::vector &pats) const ; - unsigned get_quantifier_num_bound() const { + unsigned get_quantifier_num_bound() const { return to_quantifier(raw())->get_num_decls(); - } + } - unsigned get_index_value() const { + unsigned get_index_value() const { var* va = to_var(raw()); return va->get_idx(); - } + } bool is_quantifier_forall() const { return to_quantifier(raw())->is_forall(); - } + } - sort get_quantifier_bound_sort(unsigned n) const { + sort get_quantifier_bound_sort(unsigned n) const { return sort(ctx(),to_quantifier(raw())->get_decl_sort(n)); - } + } - symbol get_quantifier_bound_name(unsigned n) const { + symbol get_quantifier_bound_name(unsigned n) const { return symbol(ctx(),to_quantifier(raw())->get_decl_names()[n]); - } + } - friend expr forall(const std::vector &quants, const expr &body); + friend expr forall(const std::vector &quants, const expr &body); - friend expr exists(const std::vector &quants, const expr &body); + friend expr exists(const std::vector &quants, const expr &body); }; - + typedef ::decl_kind pfrule; - + class proof : public ast { public: proof(context & c):ast(c) {} @@ -643,15 +643,15 @@ namespace Duality { unsigned num_prems() const { return to_app(raw())->get_num_args() - 1; } - + expr conc() const { return ctx().cook(to_app(raw())->get_arg(num_prems())); } - + proof prem(unsigned i) const { return proof(ctx(),to_app(to_app(raw())->get_arg(i))); } - + void get_assumptions(std::vector &assumps); }; @@ -675,12 +675,12 @@ namespace Duality { T back() const { return operator[](size() - 1); } void pop_back() { assert(size() > 0); resize(size() - 1); } bool empty() const { return size() == 0; } - ast_vector_tpl & operator=(ast_vector_tpl const & s) { - Z3_ast_vector_inc_ref(s.ctx(), s.m_vector); + ast_vector_tpl & operator=(ast_vector_tpl const & s) { + Z3_ast_vector_inc_ref(s.ctx(), s.m_vector); // Z3_ast_vector_dec_ref(ctx(), m_vector); - m_ctx = s.m_ctx; + m_ctx = s.m_ctx; m_vector = s.m_vector; - return *this; + return *this; } friend std::ostream & operator<<(std::ostream & out, ast_vector_tpl const & v) { out << Z3_ast_vector_to_string(v.ctx(), v); return out; } }; @@ -705,9 +705,9 @@ namespace Duality { ~func_interp() { } operator ::func_interp *() const { return m_interp; } func_interp & operator=(func_interp const & s) { - m_ctx = s.m_ctx; + m_ctx = s.m_ctx; m_interp = s.m_interp; - return *this; + return *this; } unsigned num_entries() const { return m_interp->num_entries(); } expr get_arg(unsigned ent, unsigned arg) const { @@ -729,32 +729,32 @@ namespace Duality { m_model = m; } public: - model(context & c, ::model * m = 0):object(c), m_model(m) { } - model(model const & s):object(s), m_model(s.m_model) { } - ~model() { } + model(context & c, ::model * m = 0):object(c), m_model(m) { } + model(model const & s):object(s), m_model(s.m_model) { } + ~model() { } operator ::model *() const { return m_model.get(); } model & operator=(model const & s) { // ::model *_inc_ref(s.ctx(), s.m_model); // ::model *_dec_ref(ctx(), m_model); - m_ctx = s.m_ctx; + m_ctx = s.m_ctx; m_model = s.m_model.get(); - return *this; + return *this; } model & operator=(::model *s) { - m_model = s; - return *this; + m_model = s; + return *this; } - bool null() const {return !m_model;} - + bool null() const {return !m_model;} + expr eval(expr const & n, bool model_completion=true) const { ::model * _m = m_model.get(); expr_ref result(ctx().m()); _m->eval(n, result, model_completion); return expr(ctx(), result); } - + void show() const; - void show_hash() const; + void show_hash() const; unsigned num_consts() const {return m_model.get()->get_num_constants();} unsigned num_funcs() const {return m_model.get()->get_num_functions();} @@ -765,11 +765,11 @@ namespace Duality { expr get_const_interp(func_decl f) const { return ctx().cook(m_model->get_const_interp(to_func_decl(f.raw()))); - } + } func_interp get_func_interp(func_decl f) const { return func_interp(ctx(),m_model->get_func_interp(to_func_decl(f.raw()))); - } + } #if 0 friend std::ostream & operator<<(std::ostream & out, model const & m) { out << Z3_model_to_string(m.ctx(), m); return out; } @@ -792,9 +792,9 @@ namespace Duality { stats & operator=(stats const & s) { Z3_stats_inc_ref(s.ctx(), s.m_stats); if (m_stats) Z3_stats_dec_ref(ctx(), m_stats); - m_ctx = s.m_ctx; + m_ctx = s.m_ctx; m_stats = s.m_stats; - return *this; + return *this; } unsigned size() const { return Z3_stats_size(ctx(), m_stats); } std::string key(unsigned i) const { Z3_string s = Z3_stats_get_key(ctx(), m_stats, i); check_error(); return s; } @@ -820,7 +820,7 @@ namespace Duality { void assert_cnst(const expr &cnst); }; - inline std::ostream & operator<<(std::ostream & out, check_result r) { + inline std::ostream & operator<<(std::ostream & out, check_result r) { if (r == unsat) out << "unsat"; else if (r == sat) out << "sat"; else out << "unknown"; @@ -837,54 +837,54 @@ namespace Duality { protected: ::solver *m_solver; model the_model; - bool canceled; - proof_gen_mode m_mode; - bool extensional; + bool canceled; + proof_gen_mode m_mode; + bool extensional; public: solver(context & c, bool extensional = false, bool models = true); - solver(context & c, ::solver *s):object(c),the_model(c) { m_solver = s; canceled = false;} - solver(solver const & s):object(s), the_model(s.the_model) { m_solver = s.m_solver; canceled = false;} + solver(context & c, ::solver *s):object(c),the_model(c) { m_solver = s; canceled = false;} + solver(solver const & s):object(s), the_model(s.the_model) { m_solver = s.m_solver; canceled = false;} ~solver() { if(m_solver) dealloc(m_solver); - } - operator ::solver*() const { return m_solver; } - solver & operator=(solver const & s) { - m_ctx = s.m_ctx; - m_solver = s.m_solver; - the_model = s.the_model; - m_mode = s.m_mode; - return *this; } - struct cancel_exception {}; - void checkpoint(){ + operator ::solver*() const { return m_solver; } + solver & operator=(solver const & s) { + m_ctx = s.m_ctx; + m_solver = s.m_solver; + the_model = s.the_model; + m_mode = s.m_mode; + return *this; + } + struct cancel_exception {}; + void checkpoint(){ if(canceled) throw(cancel_exception()); - } + } // void set(params const & p) { Z3_solver_set_params(ctx(), m_solver, p); check_error(); } void push() { scoped_proof_mode spm(m(),m_mode); m_solver->push(); } void pop(unsigned n = 1) { scoped_proof_mode spm(m(),m_mode); m_solver->pop(n); } // void reset() { Z3_solver_reset(ctx(), m_solver); check_error(); } void add(expr const & e) { scoped_proof_mode spm(m(),m_mode); m_solver->assert_expr(e); } - check_result check() { - scoped_proof_mode spm(m(),m_mode); + check_result check() { + scoped_proof_mode spm(m(),m_mode); checkpoint(); lbool r = m_solver->check_sat(0,0); model_ref m; m_solver->get_model(m); the_model = m.get(); return to_check_result(r); - } - check_result check_keep_model(unsigned n, expr * const assumptions, unsigned *core_size = 0, expr *core = 0) { - scoped_proof_mode spm(m(),m_mode); + } + check_result check_keep_model(unsigned n, expr * const assumptions, unsigned *core_size = 0, expr *core = 0) { + scoped_proof_mode spm(m(),m_mode); model old_model(the_model); check_result res = check(n,assumptions,core_size,core); if(the_model == 0) the_model = old_model; return res; - } + } check_result check(unsigned n, expr * const assumptions, unsigned *core_size = 0, expr *core = 0) { - scoped_proof_mode spm(m(),m_mode); + scoped_proof_mode spm(m(),m_mode); checkpoint(); std::vector< ::expr *> _assumptions(n); for (unsigned i = 0; i < n; i++) { @@ -892,7 +892,7 @@ namespace Duality { } the_model = 0; lbool r = m_solver->check_sat(n, VEC2PTR(_assumptions)); - + if(core_size && core){ ptr_vector< ::expr> _core; m_solver->get_unsat_core(_core); @@ -905,20 +905,20 @@ namespace Duality { m_solver->get_model(m); the_model = m.get(); - return to_check_result(r); + return to_check_result(r); } #if 0 - check_result check(expr_vector assumptions) { - scoped_proof_mode spm(m(),m_mode); + check_result check(expr_vector assumptions) { + scoped_proof_mode spm(m(),m_mode); unsigned n = assumptions.size(); z3array _assumptions(n); for (unsigned i = 0; i < n; i++) { check_context(*this, assumptions[i]); _assumptions[i] = assumptions[i]; } - Z3_lbool r = Z3_check_assumptions(ctx(), m_solver, n, _assumptions.ptr()); - check_error(); - return to_check_result(r); + Z3_lbool r = Z3_check_assumptions(ctx(), m_solver, n, _assumptions.ptr()); + check_error(); + return to_check_result(r); } #endif model get_model() const { return model(ctx(), the_model); } @@ -930,27 +930,26 @@ namespace Duality { #endif // expr proof() const { Z3_ast r = Z3_solver_proof(ctx(), m_solver); check_error(); return expr(ctx(), r); } // friend std::ostream & operator<<(std::ostream & out, solver const & s) { out << Z3_solver_to_string(s.ctx(), s); return out; } - - int get_num_decisions(); + int get_num_decisions(); - void cancel(){ - scoped_proof_mode spm(m(),m_mode); + void cancel(){ + scoped_proof_mode spm(m(),m_mode); canceled = true; m().limit().cancel(); - } + } - unsigned get_scope_level(){ scoped_proof_mode spm(m(),m_mode); return m_solver->get_scope_level();} + unsigned get_scope_level(){ scoped_proof_mode spm(m(),m_mode); return m_solver->get_scope_level();} - void show(); - void print(const char *filename); - void show_assertion_ids(); + void show(); + void print(const char *filename); + void show_assertion_ids(); - proof get_proof(){ - scoped_proof_mode spm(m(),m_mode); + proof get_proof(){ + scoped_proof_mode spm(m(),m_mode); return proof(ctx(),m_solver->get_proof()); - } + } - bool extensional_array_theory() {return extensional;} + bool extensional_array_theory() {return extensional;} }; #if 0 @@ -969,20 +968,20 @@ namespace Duality { goal & operator=(goal const & s) { Z3_goal_inc_ref(s.ctx(), s.m_goal); Z3_goal_dec_ref(ctx(), m_goal); - m_ctx = s.m_ctx; + m_ctx = s.m_ctx; m_goal = s.m_goal; - return *this; + return *this; } void add(expr const & f) { check_context(*this, f); Z3_goal_assert(ctx(), m_goal, f); check_error(); } unsigned size() const { return Z3_goal_size(ctx(), m_goal); } expr operator[](unsigned i) const { Z3_ast r = Z3_goal_formula(ctx(), m_goal, i); check_error(); return expr(ctx(), r); } Z3_goal_prec precision() const { return Z3_goal_precision(ctx(), m_goal); } bool inconsistent() const { return Z3_goal_inconsistent(ctx(), m_goal) != 0; } - unsigned depth() const { return Z3_goal_depth(ctx(), m_goal); } + unsigned depth() const { return Z3_goal_depth(ctx(), m_goal); } void reset() { Z3_goal_reset(ctx(), m_goal); } unsigned num_exprs() const { Z3_goal_num_exprs(ctx(), m_goal); } - bool is_decided_sat() const { return Z3_goal_is_decided_sat(ctx(), m_goal) != 0; } - bool is_decided_unsat() const { return Z3_goal_is_decided_unsat(ctx(), m_goal) != 0; } + bool is_decided_sat() const { return Z3_goal_is_decided_sat(ctx(), m_goal) != 0; } + bool is_decided_unsat() const { return Z3_goal_is_decided_unsat(ctx(), m_goal) != 0; } friend std::ostream & operator<<(std::ostream & out, goal const & g) { out << Z3_goal_to_string(g.ctx(), g); return out; } }; @@ -1000,15 +999,15 @@ namespace Duality { apply_result & operator=(apply_result const & s) { Z3_apply_result_inc_ref(s.ctx(), s.m_apply_result); Z3_apply_result_dec_ref(ctx(), m_apply_result); - m_ctx = s.m_ctx; + m_ctx = s.m_ctx; m_apply_result = s.m_apply_result; - return *this; + return *this; } unsigned size() const { return Z3_apply_result_get_num_subgoals(ctx(), m_apply_result); } goal operator[](unsigned i) const { Z3_goal r = Z3_apply_result_get_subgoal(ctx(), m_apply_result, i); check_error(); return goal(ctx(), r); } goal operator[](int i) const { assert(i >= 0); return this->operator[](static_cast(i)); } - model convert_model(model const & m, unsigned i = 0) const { - check_context(*this, m); + model convert_model(model const & m, unsigned i = 0) const { + check_context(*this, m); Z3_model new_m = Z3_apply_result_convert_model(ctx(), m_apply_result, i, m); check_error(); return model(ctx(), new_m); @@ -1031,16 +1030,16 @@ namespace Duality { tactic & operator=(tactic const & s) { Z3_tactic_inc_ref(s.ctx(), s.m_tactic); Z3_tactic_dec_ref(ctx(), m_tactic); - m_ctx = s.m_ctx; + m_ctx = s.m_ctx; m_tactic = s.m_tactic; - return *this; + return *this; } solver mk_solver() const { Z3_solver r = Z3_mk_solver_from_tactic(ctx(), m_tactic); check_error(); return solver(ctx(), r); } - apply_result apply(goal const & g) const { + apply_result apply(goal const & g) const { check_context(*this, g); - Z3_apply_result r = Z3_tactic_apply(ctx(), m_tactic, g); - check_error(); - return apply_result(ctx(), r); + Z3_apply_result r = Z3_tactic_apply(ctx(), m_tactic, g); + check_error(); + return apply_result(ctx(), r); } apply_result operator()(goal const & g) const { return apply(g); @@ -1091,45 +1090,45 @@ namespace Duality { probe & operator=(probe const & s) { Z3_probe_inc_ref(s.ctx(), s.m_probe); Z3_probe_dec_ref(ctx(), m_probe); - m_ctx = s.m_ctx; + m_ctx = s.m_ctx; m_probe = s.m_probe; - return *this; + return *this; } double apply(goal const & g) const { double r = Z3_probe_apply(ctx(), m_probe, g); check_error(); return r; } double operator()(goal const & g) const { return apply(g); } - friend probe operator<=(probe const & p1, probe const & p2) { - check_context(p1, p2); Z3_probe r = Z3_probe_le(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r); + friend probe operator<=(probe const & p1, probe const & p2) { + check_context(p1, p2); Z3_probe r = Z3_probe_le(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r); } friend probe operator<=(probe const & p1, double p2) { return p1 <= probe(p1.ctx(), p2); } friend probe operator<=(double p1, probe const & p2) { return probe(p2.ctx(), p1) <= p2; } - friend probe operator>=(probe const & p1, probe const & p2) { - check_context(p1, p2); Z3_probe r = Z3_probe_ge(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r); + friend probe operator>=(probe const & p1, probe const & p2) { + check_context(p1, p2); Z3_probe r = Z3_probe_ge(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r); } friend probe operator>=(probe const & p1, double p2) { return p1 >= probe(p1.ctx(), p2); } friend probe operator>=(double p1, probe const & p2) { return probe(p2.ctx(), p1) >= p2; } - friend probe operator<(probe const & p1, probe const & p2) { - check_context(p1, p2); Z3_probe r = Z3_probe_lt(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r); + friend probe operator<(probe const & p1, probe const & p2) { + check_context(p1, p2); Z3_probe r = Z3_probe_lt(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r); } friend probe operator<(probe const & p1, double p2) { return p1 < probe(p1.ctx(), p2); } friend probe operator<(double p1, probe const & p2) { return probe(p2.ctx(), p1) < p2; } - friend probe operator>(probe const & p1, probe const & p2) { - check_context(p1, p2); Z3_probe r = Z3_probe_gt(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r); + friend probe operator>(probe const & p1, probe const & p2) { + check_context(p1, p2); Z3_probe r = Z3_probe_gt(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r); } friend probe operator>(probe const & p1, double p2) { return p1 > probe(p1.ctx(), p2); } friend probe operator>(double p1, probe const & p2) { return probe(p2.ctx(), p1) > p2; } - friend probe operator==(probe const & p1, probe const & p2) { - check_context(p1, p2); Z3_probe r = Z3_probe_eq(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r); + friend probe operator==(probe const & p1, probe const & p2) { + check_context(p1, p2); Z3_probe r = Z3_probe_eq(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r); } friend probe operator==(probe const & p1, double p2) { return p1 == probe(p1.ctx(), p2); } friend probe operator==(double p1, probe const & p2) { return probe(p2.ctx(), p1) == p2; } - friend probe operator&&(probe const & p1, probe const & p2) { - check_context(p1, p2); Z3_probe r = Z3_probe_and(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r); + friend probe operator&&(probe const & p1, probe const & p2) { + check_context(p1, p2); Z3_probe r = Z3_probe_and(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r); } - friend probe operator||(probe const & p1, probe const & p2) { - check_context(p1, p2); Z3_probe r = Z3_probe_or(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r); + friend probe operator||(probe const & p1, probe const & p2) { + check_context(p1, p2); Z3_probe r = Z3_probe_or(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r); } friend probe operator!(probe const & p) { - Z3_probe r = Z3_probe_not(p.ctx(), p); p.check_error(); return probe(p.ctx(), r); + Z3_probe r = Z3_probe_not(p.ctx(), p); p.check_error(); return probe(p.ctx(), r); } }; @@ -1159,15 +1158,15 @@ namespace Duality { inline symbol context::int_symbol(int n) { ::symbol r = ::symbol(n); return symbol(*this, r); } inline sort context::bool_sort() { - ::sort *s = m().mk_sort(m_basic_fid, BOOL_SORT); + ::sort *s = m().mk_sort(m_basic_fid, BOOL_SORT); return sort(*this, s); } inline sort context::int_sort() { - ::sort *s = m().mk_sort(m_arith_fid, INT_SORT); + ::sort *s = m().mk_sort(m_arith_fid, INT_SORT); return sort(*this, s); } inline sort context::real_sort() { - ::sort *s = m().mk_sort(m_arith_fid, REAL_SORT); + ::sort *s = m().mk_sort(m_arith_fid, REAL_SORT); return sort(*this, s); } inline sort context::array_sort(sort d, sort r) { @@ -1188,7 +1187,7 @@ namespace Duality { inline func_decl context::function(char const * name, unsigned arity, sort const * domain, sort const & range) { return function(str_symbol(name), arity, domain, range); } - + inline func_decl context::function(char const * name, sort const & domain, sort const & range) { sort args[1] = { domain }; return function(name, 1, args, range); @@ -1196,7 +1195,7 @@ namespace Duality { inline func_decl context::function(char const * name, sort const & d1, sort const & d2, sort const & range) { sort args[2] = { d1, d2 }; - return function(name, 2, args, range); + return function(name, 2, args, range); } inline func_decl context::function(char const * name, sort const & d1, sort const & d2, sort const & d3, sort const & range) { @@ -1208,7 +1207,7 @@ namespace Duality { sort args[4] = { d1, d2, d3, d4 }; return function(name, 4, args, range); } - + inline func_decl context::function(char const * name, sort const & d1, sort const & d2, sort const & d3, sort const & d4, sort const & d5, sort const & range) { sort args[5] = { d1, d2, d3, d4, d5 }; return function(name, 5, args, range); @@ -1217,7 +1216,7 @@ namespace Duality { inline expr context::constant(symbol const & name, sort const & s) { ::expr *r = m().mk_const(m().mk_const_decl(name, s)); - return expr(*this, r); + return expr(*this, r); } inline expr context::constant(char const * name, sort const & s) { return constant(str_symbol(name), s); } inline expr context::bool_const(char const * name) { return constant(name, bool_sort()); } @@ -1250,11 +1249,11 @@ namespace Duality { expr args[5] = {a1,a2,a3,a4,a5}; return operator()(5,args); } - - + + inline expr select(expr const & a, expr const & i) { return a.ctx().make(Select,a,i); } inline expr store(expr const & a, expr const & i, expr const & v) { return a.ctx().make(Store,a,i,v); } - + inline expr forall(const std::vector &quants, const expr &body){ return body.ctx().make_quant(Forall,quants,body); } @@ -1304,7 +1303,7 @@ namespace Duality { } inline void setTerm(expr t){term = t;} - + inline void addTerm(expr t){terms.push_back(t);} inline void setChildren(const std::vector & _children){ @@ -1326,7 +1325,7 @@ namespace Duality { std::vector children; int num; }; - + typedef context interpolating_context; class interpolating_solver : public solver { @@ -1336,7 +1335,7 @@ namespace Duality { { weak_mode = false; } - + public: lbool interpolate(const std::vector &assumptions, std::vector &interpolants, @@ -1344,41 +1343,41 @@ namespace Duality { literals &lits, bool incremental ); - + lbool interpolate_tree(TermTree *assumptions, TermTree *&interpolants, model &_model, literals &lits, bool incremental ); - + bool read_interpolation_problem(const std::string &file_name, std::vector &assumptions, std::vector &theory, std::string &error_message ); - + void write_interpolation_problem(const std::string &file_name, const std::vector &assumptions, const std::vector &theory ); - + void AssertInterpolationAxiom(const expr &expr); void RemoveInterpolationAxiom(const expr &expr); - + void SetWeakInterpolants(bool weak); void SetPrintToFile(const std::string &file_name); - + const std::vector &GetInterpolationAxioms() {return theory;} const char *profile(); - + private: bool weak_mode; std::string print_filename; std::vector theory; }; - - + + inline expr context::cook(::expr *a) {return expr(*this,a);} inline std::vector context::cook(ptr_vector< ::expr> v) { diff --git a/src/interp/iz3base.h b/src/interp/iz3base.h index ac171aa9e..15f613730 100755 --- a/src/interp/iz3base.h +++ b/src/interp/iz3base.h @@ -66,35 +66,35 @@ class iz3base : public iz3mgr, public scopes { /** Constructor */ - iz3base(ast_manager &_m_manager, - const std::vector &_cnsts, - const std::vector &_parents, - const std::vector &_theory) - : iz3mgr(_m_manager), scopes(_parents) { + iz3base(ast_manager &_m_manager, + const std::vector &_cnsts, + const std::vector &_parents, + const std::vector &_theory) + : iz3mgr(_m_manager), scopes(_parents) { initialize(_cnsts,_parents,_theory); weak = false; } - iz3base(const iz3mgr& other, - const std::vector &_cnsts, - const std::vector &_parents, - const std::vector &_theory) - : iz3mgr(other), scopes(_parents) { + iz3base(const iz3mgr& other, + const std::vector &_cnsts, + const std::vector &_parents, + const std::vector &_theory) + : iz3mgr(other), scopes(_parents) { initialize(_cnsts,_parents,_theory); weak = false; } - iz3base(const iz3mgr& other, - const std::vector > &_cnsts, - const std::vector &_parents, - const std::vector &_theory) - : iz3mgr(other), scopes(_parents) { + iz3base(const iz3mgr& other, + const std::vector > &_cnsts, + const std::vector &_parents, + const std::vector &_theory) + : iz3mgr(other), scopes(_parents) { initialize(_cnsts,_parents,_theory); weak = false; } - iz3base(const iz3mgr& other) - : iz3mgr(other), scopes() { + iz3base(const iz3mgr& other) + : iz3mgr(other), scopes() { weak = false; } diff --git a/src/interp/iz3checker.h b/src/interp/iz3checker.h index 175b5a43a..d89db3011 100644 --- a/src/interp/iz3checker.h +++ b/src/interp/iz3checker.h @@ -24,26 +24,26 @@ #include "solver/solver.h" bool iz3check(ast_manager &_m_manager, - solver *s, - std::ostream &err, - const ptr_vector &cnsts, - const ::vector &parents, - const ptr_vector &interps, - const ptr_vector &theory); + solver *s, + std::ostream &err, + const ptr_vector &cnsts, + const ::vector &parents, + const ptr_vector &interps, + const ptr_vector &theory); bool iz3check(ast_manager &_m_manager, - solver *s, - std::ostream &err, - const ptr_vector &cnsts, - ast *tree, - const ptr_vector &interps); + solver *s, + std::ostream &err, + const ptr_vector &cnsts, + ast *tree, + const ptr_vector &interps); bool iz3check(iz3mgr &mgr, - solver *s, - std::ostream &err, - const std::vector &cnsts, - const std::vector &parents, - const std::vector &interps, - const ptr_vector &theory); + solver *s, + std::ostream &err, + const std::vector &cnsts, + const std::vector &parents, + const std::vector &interps, + const ptr_vector &theory); #endif diff --git a/src/interp/iz3hash.h b/src/interp/iz3hash.h index 483c7ca49..c796a247b 100644 --- a/src/interp/iz3hash.h +++ b/src/interp/iz3hash.h @@ -468,10 +468,10 @@ namespace hash_space { : hashtable,Key,HashFun,proj1,EqFun>(7) {} Value &operator[](const Key& key) { - std::pair kvp(key,Value()); - return - hashtable,Key,HashFun,proj1,EqFun>:: - lookup(kvp,true)->val.second; + std::pair kvp(key,Value()); + return + hashtable,Key,HashFun,proj1,EqFun>:: + lookup(kvp,true)->val.second; } }; diff --git a/src/interp/iz3interp.h b/src/interp/iz3interp.h index 9763208f1..a4e1024a9 100644 --- a/src/interp/iz3interp.h +++ b/src/interp/iz3interp.h @@ -73,22 +73,22 @@ typedef interpolation_options_struct *interpolation_options; representation, for compatibility with the old API. */ void iz3interpolate(ast_manager &_m_manager, - ast *proof, - const ptr_vector &cnsts, - const ::vector &parents, - ptr_vector &interps, - const ptr_vector &theory, - interpolation_options_struct * options = 0); + ast *proof, + const ptr_vector &cnsts, + const ::vector &parents, + ptr_vector &interps, + const ptr_vector &theory, + interpolation_options_struct * options = 0); /* Same as above, but each constraint is a vector of formulas. */ void iz3interpolate(ast_manager &_m_manager, - ast *proof, - const vector > &cnsts, - const ::vector &parents, - ptr_vector &interps, - const ptr_vector &theory, - interpolation_options_struct * options = 0); + ast *proof, + const vector > &cnsts, + const ::vector &parents, + ptr_vector &interps, + const ptr_vector &theory, + interpolation_options_struct * options = 0); /* Compute an interpolant from a proof. This version uses the ast representation, for compatibility with the new API. Here, cnsts is @@ -98,11 +98,11 @@ void iz3interpolate(ast_manager &_m_manager, proof, so it can be considered a hint. */ void iz3interpolate(ast_manager &_m_manager, - ast *proof, - const ptr_vector &cnsts, - ast *tree, - ptr_vector &interps, - interpolation_options_struct * options); + ast *proof, + const ptr_vector &cnsts, + ast *tree, + ptr_vector &interps, + interpolation_options_struct * options); /* Compute an interpolant from an ast representing an interpolation @@ -112,12 +112,12 @@ void iz3interpolate(ast_manager &_m_manager, */ lbool iz3interpolate(ast_manager &_m_manager, - solver &s, - ast *tree, - ptr_vector &cnsts, - ptr_vector &interps, - model_ref &m, - interpolation_options_struct * options); + solver &s, + ast *tree, + ptr_vector &cnsts, + ptr_vector &interps, + model_ref &m, + interpolation_options_struct * options); #endif diff --git a/src/interp/iz3pp.h b/src/interp/iz3pp.h index eec88d35e..7b3405f9b 100644 --- a/src/interp/iz3pp.h +++ b/src/interp/iz3pp.h @@ -30,7 +30,7 @@ struct iz3pp_bad_tree: public iz3_exception { }; void iz3pp(ast_manager &m, - const ptr_vector &cnsts_vec, - expr *tree, - std::ostream& out); + const ptr_vector &cnsts_vec, + expr *tree, + std::ostream& out); #endif diff --git a/src/interp/iz3scopes.h b/src/interp/iz3scopes.h index 745256e57..ece30dc25 100755 --- a/src/interp/iz3scopes.h +++ b/src/interp/iz3scopes.h @@ -105,7 +105,7 @@ class scopes { void range_add(int i, range &n){ #if 0 - if(i < n.lo) n.lo = i; + if(i < n.lo) n.lo = i; if(i > n.hi) n.hi = i; #else range rng; rng.lo = i; rng.hi = i; @@ -119,7 +119,7 @@ class scopes { int thing = tree_lca(rng1.lo,rng2.hi); if(thing == rng1.lo) frame = rng1.lo; else frame = tree_gcd(thing,rng1.hi); - return frame; + return frame; } #else diff --git a/src/interp/iz3translate.h b/src/interp/iz3translate.h index 3430d11b3..519a252e0 100755 --- a/src/interp/iz3translate.h +++ b/src/interp/iz3translate.h @@ -47,9 +47,9 @@ class iz3translation : public iz3base { protected: iz3translation(iz3mgr &mgr, - const std::vector > &_cnsts, - const std::vector &_parents, - const std::vector &_theory) + const std::vector > &_cnsts, + const std::vector &_parents, + const std::vector &_theory) : iz3base(mgr,_cnsts,_parents,_theory) {} }; diff --git a/src/math/automata/automaton.h b/src/math/automata/automaton.h index 07d6d31ec..41fc19907 100644 --- a/src/math/automata/automaton.h +++ b/src/math/automata/automaton.h @@ -478,7 +478,7 @@ public: unsigned out_degree(unsigned state) const { return m_delta[state].size(); } move const& get_move_from(unsigned state) const { SASSERT(m_delta[state].size() == 1); return m_delta[state][0]; } move const& get_move_to(unsigned state) const { SASSERT(m_delta_inv[state].size() == 1); return m_delta_inv[state][0]; } - moves const& get_moves_from(unsigned state) const { return m_delta[state]; } + moves const& get_moves_from(unsigned state) const { return m_delta[state]; } moves const& get_moves_to(unsigned state) const { return m_delta_inv[state]; } bool initial_state_is_source() const { return m_delta_inv[m_init].empty(); } bool is_final_state(unsigned s) const { return m_final_set.contains(s); } diff --git a/src/math/automata/boolean_algebra.h b/src/math/automata/boolean_algebra.h index e49d414c4..d54ff5d1a 100644 --- a/src/math/automata/boolean_algebra.h +++ b/src/math/automata/boolean_algebra.h @@ -40,9 +40,7 @@ template class boolean_algebra : public positive_boolean_algebra { public: virtual ~boolean_algebra() {} - virtual T mk_not(T x) = 0; - //virtual lbool are_equivalent(T x, T y) = 0; - //virtual T simplify(T x) = 0; + virtual T mk_not(T x) = 0; }; #endif diff --git a/src/math/polynomial/polynomial.h b/src/math/polynomial/polynomial.h index 138331ef3..43b3c1138 100644 --- a/src/math/polynomial/polynomial.h +++ b/src/math/polynomial/polynomial.h @@ -63,8 +63,8 @@ namespace polynomial { public: void set_degree(var x, unsigned d) { m_var2degree.setx(x, d, 0); } unsigned degree(var x) const { return m_var2degree.get(x, 0); } - void display(std::ostream & out) const; - friend std::ostream & operator<<(std::ostream & out, var2degree const & ideal) { ideal.display(out); return out; } + void display(std::ostream & out) const; + friend std::ostream & operator<<(std::ostream & out, var2degree const & ideal) { ideal.display(out); return out; } }; template diff --git a/src/math/polynomial/upolynomial.h b/src/math/polynomial/upolynomial.h index e0df0dd31..f8efae465 100644 --- a/src/math/polynomial/upolynomial.h +++ b/src/math/polynomial/upolynomial.h @@ -434,11 +434,11 @@ namespace upolynomial { m().reset(r[i]); } for (unsigned i = 0; i < sz; i++) { - typename polynomial::monomial * mon = pm.get_monomial(p, i); - if (pm.size(mon) == 0) { + typename polynomial::monomial * mon = pm.get_monomial(p, i); + if (pm.size(mon) == 0) { m().set(r[0], pm.coeff(p, i)); - } else if (pm.size(mon) == 1 && pm.get_var(mon, 0) == x) { - unsigned m_deg_x = pm.degree(mon, 0); + } else if (pm.size(mon) == 1 && pm.get_var(mon, 0) == x) { + unsigned m_deg_x = pm.degree(mon, 0); m().set(r[m_deg_x], pm.coeff(p, i)); } } diff --git a/src/model/model_core.cpp b/src/model/model_core.cpp index 2fd2d8746..f94558097 100644 --- a/src/model/model_core.cpp +++ b/src/model/model_core.cpp @@ -86,13 +86,13 @@ void model_core::register_decl(func_decl * d, func_interp * fi) { void model_core::unregister_decl(func_decl * d) { decl2expr::obj_map_entry * ec = m_interp.find_core(d); if (ec && ec->get_data().m_value != 0) { - m_manager.dec_ref(ec->get_data().m_key); - m_manager.dec_ref(ec->get_data().m_value); + m_manager.dec_ref(ec->get_data().m_key); + m_manager.dec_ref(ec->get_data().m_value); m_interp.remove(d); m_const_decls.erase(d); return; } - + decl2finterp::obj_map_entry * ef = m_finterp.find_core(d); if (ef && ef->get_data().m_value != 0) { m_manager.dec_ref(ef->get_data().m_key); diff --git a/src/muz/base/dl_context.h b/src/muz/base/dl_context.h index 738c2559e..129277514 100644 --- a/src/muz/base/dl_context.h +++ b/src/muz/base/dl_context.h @@ -54,7 +54,7 @@ namespace datalog { MEMOUT, INPUT_ERROR, APPROX, - BOUNDED, + BOUNDED, CANCELED }; @@ -318,7 +318,7 @@ namespace datalog { \brief Retrieve predicates */ func_decl_set const& get_predicates() const { return m_preds; } - ast_ref_vector const &get_pinned() const {return m_pinned; } + ast_ref_vector const &get_pinned() const {return m_pinned; } bool is_predicate(func_decl* pred) const { return m_preds.contains(pred); } bool is_predicate(expr * e) const { return is_app(e) && is_predicate(to_app(e)->get_decl()); } @@ -534,7 +534,7 @@ namespace datalog { \brief retrieve proof from derivation of the query. \pre engine == 'pdr' || engine == 'duality'- this option is only supported - for PDR mode and Duality mode. + for PDR mode and Duality mode. */ proof_ref get_proof(); diff --git a/src/muz/base/dl_engine_base.h b/src/muz/base/dl_engine_base.h index 9c20c712d..576ed7f6b 100644 --- a/src/muz/base/dl_engine_base.h +++ b/src/muz/base/dl_engine_base.h @@ -32,7 +32,7 @@ namespace datalog { QBMC_ENGINE, TAB_ENGINE, CLP_ENGINE, - DUALITY_ENGINE, + DUALITY_ENGINE, DDNF_ENGINE, LAST_ENGINE }; diff --git a/src/muz/duality/duality_dl_interface.h b/src/muz/duality/duality_dl_interface.h index 21291a45b..506642217 100644 --- a/src/muz/duality/duality_dl_interface.h +++ b/src/muz/duality/duality_dl_interface.h @@ -37,7 +37,7 @@ namespace Duality { class dl_interface : public datalog::engine_base { duality_data *_d; - datalog::context &m_ctx; + datalog::context &m_ctx; public: dl_interface(datalog::context& ctx); @@ -69,7 +69,7 @@ namespace Duality { proof_ref get_proof(); - duality_data *dd(){return _d;} + duality_data *dd(){return _d;} private: void display_certificate_non_const(std::ostream& out); diff --git a/src/muz/pdr/pdr_generalizers.h b/src/muz/pdr/pdr_generalizers.h index 3d0fe6ccd..e0feda310 100644 --- a/src/muz/pdr/pdr_generalizers.h +++ b/src/muz/pdr/pdr_generalizers.h @@ -88,7 +88,7 @@ namespace pdr { virtual ~core_convex_hull_generalizer() {} virtual void operator()(model_node& n, expr_ref_vector const& core, bool uses_level, cores& new_cores); virtual void operator()(model_node& n, expr_ref_vector& core, bool& uses_level); - }; + }; class core_multi_generalizer : public core_generalizer { core_bool_inductive_generalizer m_gen; diff --git a/src/muz/rel/dl_mk_similarity_compressor.h b/src/muz/rel/dl_mk_similarity_compressor.h index 68410831c..096305c59 100644 --- a/src/muz/rel/dl_mk_similarity_compressor.h +++ b/src/muz/rel/dl_mk_similarity_compressor.h @@ -53,7 +53,7 @@ namespace datalog { */ class mk_similarity_compressor : public rule_transformer::plugin { - context & m_context; + context & m_context; ast_manager & m_manager; /** number of similar rules necessary for a group to be introduced */ unsigned m_threshold_count; diff --git a/src/muz/rel/dl_mk_simple_joins.h b/src/muz/rel/dl_mk_simple_joins.h index 4d422e651..cf4522c22 100644 --- a/src/muz/rel/dl_mk_simple_joins.h +++ b/src/muz/rel/dl_mk_simple_joins.h @@ -49,7 +49,7 @@ namespace datalog { We say that a rule containing C_i's is a rule with a "big tail". */ class mk_simple_joins : public rule_transformer::plugin { - context & m_context; + context & m_context; rule_manager & rm; public: mk_simple_joins(context & ctx); diff --git a/src/muz/spacer/spacer_qe_project.cpp b/src/muz/spacer/spacer_qe_project.cpp index 8dbf87ca5..dd6472224 100644 --- a/src/muz/spacer/spacer_qe_project.cpp +++ b/src/muz/spacer/spacer_qe_project.cpp @@ -1209,7 +1209,7 @@ namespace qe { void operator()(model& mdl, app_ref_vector& vars, expr_ref& fml) { expr_map map (m); - operator()(mdl, vars, fml, map); + operator()(mdl, vars, fml, map); } void operator()(model& mdl, app_ref_vector& vars, expr_ref& fml, expr_map& map) { diff --git a/src/muz/transforms/dl_mk_magic_sets.h b/src/muz/transforms/dl_mk_magic_sets.h index eef40fd71..73b5e94f6 100644 --- a/src/muz/transforms/dl_mk_magic_sets.h +++ b/src/muz/transforms/dl_mk_magic_sets.h @@ -93,7 +93,7 @@ namespace datalog { typedef obj_map pred_adornment_map; typedef obj_map pred2pred; - context & m_context; + context & m_context; ast_manager & m; rule_manager& rm; ast_ref_vector m_pinned; diff --git a/src/muz/transforms/dl_mk_unbound_compressor.h b/src/muz/transforms/dl_mk_unbound_compressor.h index febb4bd46..6f53e0707 100644 --- a/src/muz/transforms/dl_mk_unbound_compressor.h +++ b/src/muz/transforms/dl_mk_unbound_compressor.h @@ -50,7 +50,7 @@ namespace datalog { typedef hashtable > in_progress_table; typedef svector todo_stack; - context & m_context; + context & m_context; ast_manager & m; rule_manager & rm; rule_ref_vector m_rules; diff --git a/src/smt/diff_logic.h b/src/smt/diff_logic.h index 67d1f045d..44e858219 100644 --- a/src/smt/diff_logic.h +++ b/src/smt/diff_logic.h @@ -956,8 +956,8 @@ public: } void get_neighbours_undirected(dl_var current, svector & neighbours) { - neighbours.reset(); - edge_id_vector & out_edges = m_out_edges[current]; + neighbours.reset(); + edge_id_vector & out_edges = m_out_edges[current]; typename edge_id_vector::iterator it = out_edges.begin(), end = out_edges.end(); for (; it != end; ++it) { edge_id e_id = *it; @@ -968,7 +968,7 @@ public: } edge_id_vector & in_edges = m_in_edges[current]; typename edge_id_vector::iterator it2 = in_edges.begin(), end2 = in_edges.end(); - for (; it2 != end2; ++it2) { + for (; it2 != end2; ++it2) { edge_id e_id = *it2; edge & e = m_edges[e_id]; SASSERT(e.get_target() == current); @@ -980,19 +980,19 @@ public: void dfs_undirected(dl_var start, svector & threads) { threads.reset(); threads.resize(get_num_nodes()); - uint_set discovered, explored; - svector nodes; + uint_set discovered, explored; + svector nodes; discovered.insert(start); - nodes.push_back(start); - dl_var prev = start; - while(!nodes.empty()) { - dl_var current = nodes.back(); + nodes.push_back(start); + dl_var prev = start; + while(!nodes.empty()) { + dl_var current = nodes.back(); SASSERT(discovered.contains(current) && !explored.contains(current)); - svector neighbours; - get_neighbours_undirected(current, neighbours); + svector neighbours; + get_neighbours_undirected(current, neighbours); SASSERT(!neighbours.empty()); bool found = false; - for (unsigned i = 0; i < neighbours.size(); ++i) { + for (unsigned i = 0; i < neighbours.size(); ++i) { dl_var next = neighbours[i]; DEBUG_CODE( edge_id id; @@ -1002,18 +1002,18 @@ public: threads[prev] = next; prev = next; discovered.insert(next); - nodes.push_back(next); + nodes.push_back(next); found = true; break; } - } + } SASSERT(!nodes.empty()); if (!found) { explored.insert(current); nodes.pop_back(); } - } - threads[prev] = start; + } + threads[prev] = start; } void bfs_undirected(dl_var start, svector & parents, svector & depths) { @@ -1022,31 +1022,31 @@ public: parents[start] = -1; depths.reset(); depths.resize(get_num_nodes()); - uint_set visited; - std::deque nodes; - visited.insert(start); - nodes.push_front(start); - while(!nodes.empty()) { + uint_set visited; + std::deque nodes; + visited.insert(start); + nodes.push_front(start); + while(!nodes.empty()) { dl_var current = nodes.back(); nodes.pop_back(); - SASSERT(visited.contains(current)); + SASSERT(visited.contains(current)); svector neighbours; - get_neighbours_undirected(current, neighbours); + get_neighbours_undirected(current, neighbours); SASSERT(!neighbours.empty()); - for (unsigned i = 0; i < neighbours.size(); ++i) { - dl_var next = neighbours[i]; + for (unsigned i = 0; i < neighbours.size(); ++i) { + dl_var next = neighbours[i]; DEBUG_CODE( edge_id id; SASSERT(get_edge_id(current, next, id) || get_edge_id(next, current, id));); if (!visited.contains(next)) { TRACE("diff_logic", tout << "parents[" << next << "] --> " << current << std::endl;); - parents[next] = current; - depths[next] = depths[current] + 1; - visited.insert(next); - nodes.push_front(next); + parents[next] = current; + depths[next] = depths[current] + 1; + visited.insert(next); + nodes.push_front(next); } - } - } + } + } } template diff --git a/src/smt/smt_enode.h b/src/smt/smt_enode.h index 4b3a64d90..f471314fa 100644 --- a/src/smt/smt_enode.h +++ b/src/smt/smt_enode.h @@ -40,10 +40,10 @@ namespace smt { /** \ brief Use sparse maps in SMT solver. - Define this to use hash maps rather than vectors over ast - nodes. This is useful in the case there are many solvers, each - referencing few nodes from a large ast manager. There is some - unknown performance penalty for this. */ + Define this to use hash maps rather than vectors over ast + nodes. This is useful in the case there are many solvers, each + referencing few nodes from a large ast manager. There is some + unknown performance penalty for this. */ // #define SPARSE_MAP diff --git a/src/smt/smt_quantifier.h b/src/smt/smt_quantifier.h index a55c895e6..d89f3f6a4 100644 --- a/src/smt/smt_quantifier.h +++ b/src/smt/smt_quantifier.h @@ -149,7 +149,7 @@ namespace smt { /** \brief Is "model based" instantiate allowed to instantiate this quantifier? */ - virtual bool mbqi_enabled(quantifier *q) const {return true;} + virtual bool mbqi_enabled(quantifier *q) const {return true;} /** \brief Give a change to the plugin to adjust the interpretation of unintepreted functions. diff --git a/src/smt/smt_theory.h b/src/smt/smt_theory.h index 71eedc1a7..2ee0db322 100644 --- a/src/smt/smt_theory.h +++ b/src/smt/smt_theory.h @@ -192,7 +192,7 @@ namespace smt { virtual lbool validate_unsat_core(expr_ref_vector & unsat_core) { return l_false; } - + /** \brief This method is invoked before the search starts. */ diff --git a/src/smt/theory_seq.h b/src/smt/theory_seq.h index 1f97697c2..2ad257fd7 100644 --- a/src/smt/theory_seq.h +++ b/src/smt/theory_seq.h @@ -45,7 +45,7 @@ namespace smt { typedef trail_stack th_trail_stack; typedef std::pair expr_dep; typedef obj_map eqdep_map_t; - typedef union_find th_union_find; + typedef union_find th_union_find; class seq_value_proc; @@ -298,8 +298,8 @@ namespace smt { scoped_vector m_eqs; // set of current equations. scoped_vector m_nqs; // set of current disequalities. scoped_vector m_ncs; // set of non-contains constraints. - unsigned m_eq_id; - th_union_find m_find; + unsigned m_eq_id; + th_union_find m_find; seq_factory* m_factory; // value factory exclusion_table m_exclude; // set of asserted disequalities. @@ -584,7 +584,7 @@ namespace smt { // model building app* mk_value(app* a); - th_trail_stack& get_trail_stack() { return m_trail_stack; } + th_trail_stack& get_trail_stack() { return m_trail_stack; } 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) {} diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index 88b044a90..8a141665c 100644 --- a/src/smt/theory_str.cpp +++ b/src/smt/theory_str.cpp @@ -4748,11 +4748,11 @@ namespace smt { context& ctx = get_context(); ast_manager & m = get_manager(); - // safety - if (!ctx.e_internalized(e)) { + // safety + if (!ctx.e_internalized(e)) { return false; - } - + } + // if an integer constant exists in the eqc, it should be the root enode * en_e = ctx.get_enode(e); enode * root_e = en_e->get_root(); @@ -7028,7 +7028,7 @@ namespace smt { ast_manager & m = get_manager(); if (lenTester_fvar_map.contains(lenTester)) { expr * fVar = lenTester_fvar_map[lenTester]; - expr_ref toAssert(gen_len_val_options_for_free_var(fVar, lenTester, lenTesterValue), m); + expr_ref toAssert(gen_len_val_options_for_free_var(fVar, lenTester, lenTesterValue), m); TRACE("str", tout << "asserting more length tests for free variable " << mk_ismt2_pp(fVar, m) << std::endl;); if (toAssert) { assert_axiom(toAssert); diff --git a/src/smt/watch_list.cpp b/src/smt/watch_list.cpp index 2ff75c418..edd6923d7 100644 --- a/src/smt/watch_list.cpp +++ b/src/smt/watch_list.cpp @@ -36,10 +36,10 @@ namespace smt { void watch_list::expand() { if (m_data == 0) { - unsigned size = DEFAULT_WATCH_LIST_SIZE + HEADER_SIZE; + unsigned size = DEFAULT_WATCH_LIST_SIZE + HEADER_SIZE; unsigned * mem = reinterpret_cast(alloc_svect(char, size)); #ifdef _AMD64_ - ++mem; // make sure data is aligned in 64 bit machines + ++mem; // make sure data is aligned in 64 bit machines #endif *mem = 0; ++mem; @@ -62,9 +62,9 @@ namespace smt { unsigned * mem = reinterpret_cast(alloc_svect(char, new_capacity + HEADER_SIZE)); unsigned curr_end_cls = end_cls_core(); #ifdef _AMD64_ - ++mem; // make sure data is aligned in 64 bit machines + ++mem; // make sure data is aligned in 64 bit machines #endif - *mem = curr_end_cls; + *mem = curr_end_cls; ++mem; SASSERT(bin_bytes <= new_capacity); unsigned new_begin_bin = new_capacity - bin_bytes; diff --git a/src/tactic/sls/sls_tracker.h b/src/tactic/sls/sls_tracker.h index 651e4ef14..4ad5c65f4 100644 --- a/src/tactic/sls/sls_tracker.h +++ b/src/tactic/sls/sls_tracker.h @@ -68,7 +68,7 @@ private: typedef obj_map scores_type; typedef obj_map > uplinks_type; typedef obj_map > occ_type; - obj_hashtable m_top_expr; + obj_hashtable m_top_expr; scores_type m_scores; uplinks_type m_uplinks; entry_point_type m_entry_points; @@ -85,11 +85,11 @@ private: unsigned m_touched; double m_scale_unsat; unsigned m_paws_init; - obj_map m_where_false; - expr** m_list_false; + obj_map m_where_false; + expr** m_list_false; unsigned m_track_unsat; obj_map m_weights; - double m_top_sum; + double m_top_sum; obj_hashtable m_temp_seen; public: @@ -450,7 +450,7 @@ public: m_list_false = new expr*[sz]; for (unsigned i = 0; i < sz; i++) { - if (m_mpz_manager.eq(get_value(as[i]), m_zero)) + if (m_mpz_manager.eq(get_value(as[i]), m_zero)) break_assertion(as[i]); } } @@ -462,7 +462,7 @@ public: // initialize weights if (!m_weights.contains(e)) - m_weights.insert(e, m_paws_init); + m_weights.insert(e, m_paws_init); // positive/negative occurrences used for early pruning setup_occs(as[i]); @@ -1075,7 +1075,7 @@ public: unsigned cnt_unsat = 0; for (unsigned i = 0; i < sz; i++) - if (m_mpz_manager.neq(get_value(as[i]), m_one) && (get_random_uint(16) % ++cnt_unsat == 0)) pos = i; + if (m_mpz_manager.neq(get_value(as[i]), m_one) && (get_random_uint(16) % ++cnt_unsat == 0)) pos = i; if (pos == static_cast(-1)) return 0; } @@ -1092,7 +1092,7 @@ public: unsigned cnt_unsat = 0, pos = -1; for (unsigned i = 0; i < sz; i++) - if ((i != m_last_pos) && m_mpz_manager.neq(get_value(as[i]), m_one) && (get_random_uint(16) % ++cnt_unsat == 0)) pos = i; + if ((i != m_last_pos) && m_mpz_manager.neq(get_value(as[i]), m_one) && (get_random_uint(16) % ++cnt_unsat == 0)) pos = i; if (pos == static_cast(-1)) return 0; diff --git a/src/test/bit_vector.cpp b/src/test/bit_vector.cpp index e920fadee..487f6cdd0 100644 --- a/src/test/bit_vector.cpp +++ b/src/test/bit_vector.cpp @@ -27,36 +27,36 @@ static void tst1() { unsigned n = rand()%10000; for (unsigned i = 0; i < n; i++) { int op = rand()%6; - if (op <= 1) { - bool val = (rand()%2) != 0; - v1.push_back(val); - v2.push_back(val); - ENSURE(v1.size() == v2.size()); - } - else if (op <= 3) { - ENSURE(v1.size() == v2.size()); - if (v1.size() > 0) { - bool val = (rand()%2) != 0; - unsigned idx = rand()%v1.size(); - ENSURE(v1.get(idx) == v2[idx]); - v1.set(idx, val); - v2[idx] = val; - ENSURE(v1.get(idx) == v2[idx]); - } - } - else if (op <= 4) { - ENSURE(v1.size() == v2.size()); - if (v1.size() > 0) { - unsigned idx = rand()%v1.size(); - VERIFY(v1.get(idx) == v2[idx]); - } - } - else if (op <= 5) { - ENSURE(v1.size() == v2.size()); - for (unsigned j = 0; j < v1.size(); j++) { - ENSURE(v1.get(j) == v2[j]); - } - } + if (op <= 1) { + bool val = (rand()%2) != 0; + v1.push_back(val); + v2.push_back(val); + ENSURE(v1.size() == v2.size()); + } + else if (op <= 3) { + ENSURE(v1.size() == v2.size()); + if (v1.size() > 0) { + bool val = (rand()%2) != 0; + unsigned idx = rand()%v1.size(); + ENSURE(v1.get(idx) == v2[idx]); + v1.set(idx, val); + v2[idx] = val; + ENSURE(v1.get(idx) == v2[idx]); + } + } + else if (op <= 4) { + ENSURE(v1.size() == v2.size()); + if (v1.size() > 0) { + unsigned idx = rand()%v1.size(); + VERIFY(v1.get(idx) == v2[idx]); + } + } + else if (op <= 5) { + ENSURE(v1.size() == v2.size()); + for (unsigned j = 0; j < v1.size(); j++) { + ENSURE(v1.get(j) == v2[j]); + } + } } } @@ -309,6 +309,6 @@ void tst_bit_vector() { tst2(); for (unsigned i = 0; i < 20; i++) { std::cerr << i << std::endl; - tst1(); + tst1(); } } diff --git a/src/test/diff_logic.cpp b/src/test/diff_logic.cpp index e79c93cf2..0564fbfbe 100644 --- a/src/test/diff_logic.cpp +++ b/src/test/diff_logic.cpp @@ -33,7 +33,7 @@ template class dl_graph; typedef dl_graph dlg; struct tst_dl_functor { - smt::literal_vector m_literals; + smt::literal_vector m_literals; void operator()(smt::literal l) { m_literals.push_back(l); } diff --git a/src/test/expr_rand.cpp b/src/test/expr_rand.cpp index 388a178f4..f1b20ba8e 100644 --- a/src/test/expr_rand.cpp +++ b/src/test/expr_rand.cpp @@ -98,8 +98,8 @@ void tst_expr_rand(char** argv, int argc, int& i) { i += 1; if (i + 1 < argc && 0 == strncmp(argv[i+1],"/rs:",3)) { rand_seed = atol(argv[i+1]+4); - std::cout << "random seed:" << rand_seed << "\n"; - i += 1; + std::cout << "random seed:" << rand_seed << "\n"; + i += 1; } if (i + 1 < argc && 0 == strcmp(argv[i+1],"/arith")) { diff --git a/src/test/main.cpp b/src/test/main.cpp index 2c51df601..d0d0aac5b 100644 --- a/src/test/main.cpp +++ b/src/test/main.cpp @@ -16,20 +16,20 @@ // and print "PASS" to indicate success. // -#define TST(MODULE) { \ - std::string s("test "); \ - s += #MODULE; \ - void tst_##MODULE(); \ +#define TST(MODULE) { \ + std::string s("test "); \ + s += #MODULE; \ + void tst_##MODULE(); \ if (do_display_usage) \ std::cout << #MODULE << "\n"; \ - for (int i = 0; i < argc; i++) \ - if (test_all || strcmp(argv[i], #MODULE) == 0) { \ + for (int i = 0; i < argc; i++) \ + if (test_all || strcmp(argv[i], #MODULE) == 0) { \ enable_trace(#MODULE); \ - enable_debug(#MODULE); \ - timeit timeit(true, s.c_str()); \ - tst_##MODULE(); \ + enable_debug(#MODULE); \ + timeit timeit(true, s.c_str()); \ + tst_##MODULE(); \ std::cout << "PASS" << std::endl; \ - } \ + } \ } #define TST_ARGV(MODULE) { \ @@ -39,13 +39,13 @@ if (do_display_usage) \ std::cout << #MODULE << "\n"; \ for (int i = 0; i < argc; i++) \ - if (strcmp(argv[i], #MODULE) == 0) { \ + if (strcmp(argv[i], #MODULE) == 0) { \ enable_trace(#MODULE); \ - enable_debug(#MODULE); \ - timeit timeit(true, s.c_str()); \ - tst_##MODULE(argv, argc, i); \ + enable_debug(#MODULE); \ + timeit timeit(true, s.c_str()); \ + tst_##MODULE(argv, argc, i); \ std::cout << "PASS" << std::endl; \ - } \ + } \ } void error(const char * msg) { @@ -76,49 +76,49 @@ void display_usage() { void parse_cmd_line_args(int argc, char ** argv, bool& do_display_usage, bool& test_all) { int i = 1; while (i < argc) { - char * arg = argv[i], *eq_pos = 0; + char * arg = argv[i], *eq_pos = 0; - if (arg[0] == '-' || arg[0] == '/') { - char * opt_name = arg + 1; - char * opt_arg = 0; - char * colon = strchr(arg, ':'); - if (colon) { - opt_arg = colon + 1; - *colon = 0; - } - if (strcmp(opt_name, "h") == 0 || + if (arg[0] == '-' || arg[0] == '/') { + char * opt_name = arg + 1; + char * opt_arg = 0; + char * colon = strchr(arg, ':'); + if (colon) { + opt_arg = colon + 1; + *colon = 0; + } + if (strcmp(opt_name, "h") == 0 || strcmp(opt_name, "?") == 0) { - display_usage(); + display_usage(); do_display_usage = true; return; - } - else if (strcmp(opt_name, "v") == 0) { - if (!opt_arg) - error("option argument (/v:level) is missing."); - long lvl = strtol(opt_arg, 0, 10); - set_verbosity_level(lvl); - } - else if (strcmp(opt_name, "w") == 0) { + } + else if (strcmp(opt_name, "v") == 0) { + if (!opt_arg) + error("option argument (/v:level) is missing."); + long lvl = strtol(opt_arg, 0, 10); + set_verbosity_level(lvl); + } + else if (strcmp(opt_name, "w") == 0) { enable_warning_messages(true); - } - else if (strcmp(opt_name, "a") == 0) { + } + else if (strcmp(opt_name, "a") == 0) { test_all = true; - } + } #ifdef _TRACE - else if (strcmp(opt_name, "tr") == 0) { - if (!opt_arg) - error("option argument (/tr:tag) is missing."); - enable_trace(opt_arg); - } + else if (strcmp(opt_name, "tr") == 0) { + if (!opt_arg) + error("option argument (/tr:tag) is missing."); + enable_trace(opt_arg); + } #endif #ifdef Z3DEBUG - else if (strcmp(opt_name, "dbg") == 0) { - if (!opt_arg) - error("option argument (/dbg:tag) is missing."); - enable_debug(opt_arg); - } + else if (strcmp(opt_name, "dbg") == 0) { + if (!opt_arg) + error("option argument (/dbg:tag) is missing."); + enable_debug(opt_arg); + } #endif - } + } else if (arg[0] != '"' && (eq_pos = strchr(arg, '='))) { char * key = arg; *eq_pos = 0; @@ -130,7 +130,7 @@ void parse_cmd_line_args(int argc, char ** argv, bool& do_display_usage, bool& t std::cerr << ex.msg() << "\n"; } } - i++; + i++; } } diff --git a/src/test/model_based_opt.cpp b/src/test/model_based_opt.cpp index 2f8cf9941..7b3b95afd 100644 --- a/src/test/model_based_opt.cpp +++ b/src/test/model_based_opt.cpp @@ -54,7 +54,7 @@ static void add_random_ineq(opt::model_based_opt& mbo, continue; } unsigned sign = r(2); - coeff = sign == 0 ? coeff : -coeff; + coeff = sign == 0 ? coeff : -coeff; vars.push_back(var(x, rational(coeff))); value += coeff*values[x]; } diff --git a/src/test/optional.cpp b/src/test/optional.cpp index 2ef922444..d698f7289 100644 --- a/src/test/optional.cpp +++ b/src/test/optional.cpp @@ -36,11 +36,11 @@ struct OptFoo { int m_y; OptFoo(int x, int y):m_x(x), m_y(y) { - TRACE("optional", tout << "OptFoo created: " << m_x << " : " << m_y << "\n";); + TRACE("optional", tout << "OptFoo created: " << m_x << " : " << m_y << "\n";); } ~OptFoo() { - TRACE("optional", tout << "OptFoo deleted: " << m_x << " : " << m_y << "\n";); + TRACE("optional", tout << "OptFoo deleted: " << m_x << " : " << m_y << "\n";); } }; diff --git a/src/util/dependency.h b/src/util/dependency.h index d6df6d7bf..5055399bc 100644 --- a/src/util/dependency.h +++ b/src/util/dependency.h @@ -201,7 +201,7 @@ public: m_todo.push_back(d); unsigned qhead = 0; while (qhead < m_todo.size()) { - d = m_todo[qhead]; + d = m_todo[qhead]; qhead++; if (d->is_leaf()) { vs.push_back(to_leaf(d)->m_value); diff --git a/src/util/hash.h b/src/util/hash.h index 7fce04ca8..bc6117cac 100644 --- a/src/util/hash.h +++ b/src/util/hash.h @@ -236,7 +236,7 @@ template struct ptr_hash { typedef T * data; unsigned operator()(T * ptr) const { - return get_ptr_hash(ptr); + return get_ptr_hash(ptr); } }; diff --git a/src/util/inf_eps_rational.h b/src/util/inf_eps_rational.h index 72212d33c..c184623ca 100644 --- a/src/util/inf_eps_rational.h +++ b/src/util/inf_eps_rational.h @@ -119,12 +119,12 @@ class inf_eps_rational { bool is_rational() const { return m_infty.is_zero() && m_r.is_rational(); } int64 get_int64() const { - SASSERT(is_int64()); + SASSERT(is_int64()); return m_r.get_int64(); } uint64 get_uint64() const { - SASSERT(is_uint64()); + SASSERT(is_uint64()); return m_r.get_uint64(); } @@ -168,45 +168,45 @@ class inf_eps_rational { inf_eps_rational & operator=(const inf_eps_rational & r) { m_infty = r.m_infty; m_r = r.m_r; - return *this; + return *this; } inf_eps_rational & operator=(const Numeral & r) { m_infty.reset(); m_r = r; - return *this; + return *this; } inf_eps_rational & operator+=(const inf_eps_rational & r) { m_infty += r.m_infty; m_r += r.m_r; - return *this; + return *this; } inf_eps_rational & operator-=(const inf_eps_rational & r) { m_infty -= r.m_infty; m_r -= r.m_r; - return *this; + return *this; } inf_eps_rational & operator-=(const inf_rational & r) { m_r -= r; - return *this; + return *this; } inf_eps_rational & operator+=(const inf_rational & r) { m_r += r; - return *this; + return *this; } inf_eps_rational & operator+=(const rational & r) { m_r += r; - return *this; + return *this; } inf_eps_rational & operator-=(const rational & r) { m_r -= r; - return *this; + return *this; } inf_eps_rational & operator*=(const rational & r1) { diff --git a/src/util/inf_int_rational.h b/src/util/inf_int_rational.h index ce871b0d5..c9c82052e 100644 --- a/src/util/inf_int_rational.h +++ b/src/util/inf_int_rational.h @@ -110,12 +110,12 @@ class inf_int_rational { bool is_rational() const { return m_second == 0; } int64 get_int64() const { - SASSERT(is_int64()); + SASSERT(is_int64()); return m_first.get_int64(); } uint64 get_uint64() const { - SASSERT(is_uint64()); + SASSERT(is_uint64()); return m_first.get_uint64(); } @@ -132,7 +132,7 @@ class inf_int_rational { inf_int_rational & operator=(const inf_int_rational & r) { m_first = r.m_first; m_second = r.m_second; - return *this; + return *this; } inf_int_rational & operator=(const rational & r) { @@ -154,7 +154,7 @@ class inf_int_rational { inf_int_rational & operator+=(const inf_int_rational & r) { m_first += r.m_first; m_second += r.m_second; - return *this; + return *this; } inf_int_rational & operator*=(const rational & r) { @@ -163,7 +163,7 @@ class inf_int_rational { } m_first *= r; m_second *= r.get_int32(); - return *this; + return *this; } @@ -171,17 +171,17 @@ class inf_int_rational { inf_int_rational & operator-=(const inf_int_rational & r) { m_first -= r.m_first; m_second -= r.m_second; - return *this; + return *this; } inf_int_rational & operator+=(const rational & r) { m_first += r; - return *this; + return *this; } inf_int_rational & operator-=(const rational & r) { m_first -= r; - return *this; + return *this; } inf_int_rational & operator++() { diff --git a/src/util/inf_rational.h b/src/util/inf_rational.h index c17c4312b..d49e45f50 100644 --- a/src/util/inf_rational.h +++ b/src/util/inf_rational.h @@ -123,12 +123,12 @@ class inf_rational { bool is_rational() const { return m_second.is_zero(); } int64 get_int64() const { - SASSERT(is_int64()); + SASSERT(is_int64()); return m_first.get_int64(); } uint64 get_uint64() const { - SASSERT(is_uint64()); + SASSERT(is_uint64()); return m_first.get_uint64(); } @@ -145,7 +145,7 @@ class inf_rational { inf_rational & operator=(const inf_rational & r) { m_first = r.m_first; m_second = r.m_second; - return *this; + return *this; } inf_rational & operator=(const rational & r) { @@ -167,23 +167,23 @@ class inf_rational { inf_rational & operator+=(const inf_rational & r) { m_first += r.m_first; m_second += r.m_second; - return *this; + return *this; } inf_rational & operator-=(const inf_rational & r) { m_first -= r.m_first; m_second -= r.m_second; - return *this; + return *this; } inf_rational & operator+=(const rational & r) { m_first += r; - return *this; + return *this; } inf_rational & operator-=(const rational & r) { m_first -= r; - return *this; + return *this; } inf_rational & operator*=(const rational & r1) { diff --git a/src/util/inf_s_integer.h b/src/util/inf_s_integer.h index 6cf1d4225..067000202 100644 --- a/src/util/inf_s_integer.h +++ b/src/util/inf_s_integer.h @@ -67,7 +67,7 @@ class inf_s_integer { inf_s_integer & operator=(const inf_s_integer & r) { m_first = r.m_first; m_second = r.m_second; - return *this; + return *this; } inf_s_integer & operator=(const rational & r) { m_first = static_cast(r.get_int64()); @@ -90,20 +90,20 @@ class inf_s_integer { inf_s_integer & operator+=(const inf_s_integer & r) { m_first += r.m_first; m_second += r.m_second; - return *this; + return *this; } inf_s_integer & operator-=(const inf_s_integer & r) { m_first -= r.m_first; m_second -= r.m_second; - return *this; + return *this; } inf_s_integer & operator+=(const s_integer & r) { m_first += r.get_int(); - return *this; + return *this; } inf_s_integer & operator-=(const s_integer & r) { m_first -= r.get_int(); - return *this; + return *this; } inf_s_integer & operator*=(const s_integer & r1) { m_first *= r1.get_int(); diff --git a/src/util/lp/bound_analyzer_on_row.h b/src/util/lp/bound_analyzer_on_row.h index 4c6c43464..914835a3c 100644 --- a/src/util/lp/bound_analyzer_on_row.h +++ b/src/util/lp/bound_analyzer_on_row.h @@ -114,22 +114,22 @@ public : } return a * lb(j).x; } - mpq monoid_max(const mpq & a, unsigned j, bool & strict) const { - if (is_pos(a)) { - strict = !is_zero(ub(j).y); - return a * ub(j).x; - } - strict = !is_zero(lb(j).y); - return a * lb(j).x; - } - const mpq & monoid_min_no_mult(bool a_is_pos, unsigned j, bool & strict) const { - if (!a_is_pos) { - strict = !is_zero(ub(j).y); - return ub(j).x; - } - strict = !is_zero(lb(j).y); - return lb(j).x; - } + mpq monoid_max(const mpq & a, unsigned j, bool & strict) const { + if (is_pos(a)) { + strict = !is_zero(ub(j).y); + return a * ub(j).x; + } + strict = !is_zero(lb(j).y); + return a * lb(j).x; + } + const mpq & monoid_min_no_mult(bool a_is_pos, unsigned j, bool & strict) const { + if (!a_is_pos) { + strict = !is_zero(ub(j).y); + return ub(j).x; + } + strict = !is_zero(lb(j).y); + return lb(j).x; + } mpq monoid_min(const mpq & a, unsigned j, bool& strict) const { if (is_neg(a)) { @@ -166,7 +166,7 @@ public : m_it.reset(); while (m_it.next(a, j)) { bool str; - bool a_is_pos = is_pos(a); + bool a_is_pos = is_pos(a); mpq bound = total / a + monoid_min_no_mult(a_is_pos, j, str); if (a_is_pos) { limit_j(j, bound, true, false, strict - static_cast(str) > 0); @@ -192,8 +192,8 @@ public : m_it.reset(); while (m_it.next(a, j)) { bool str; - bool a_is_pos = is_pos(a); - mpq bound = total / a + monoid_max_no_mult(a_is_pos, j, str); + bool a_is_pos = is_pos(a); + mpq bound = total / a + monoid_max_no_mult(a_is_pos, j, str); bool astrict = strict - static_cast(str) > 0; if (a_is_pos) { limit_j(j, bound, true, true, astrict); diff --git a/src/util/lp/init_lar_solver.h b/src/util/lp/init_lar_solver.h index 3fc29f25b..db5a6ed4c 100644 --- a/src/util/lp/init_lar_solver.h +++ b/src/util/lp/init_lar_solver.h @@ -123,7 +123,7 @@ void add_row_for_term(const lar_term * term, unsigned term_ext_index) { void add_row_from_term_no_constraint(const lar_term * term, unsigned term_ext_index) { register_new_ext_var_index(term_ext_index); // j will be a new variable - unsigned j = A_r().column_count(); + unsigned j = A_r().column_count(); ul_pair ul(j); m_vars_to_ul_pairs.push_back(ul); add_basic_var_to_core_fields(); @@ -152,7 +152,7 @@ void add_basic_var_to_core_fields() { } constraint_index add_var_bound(var_index j, lconstraint_kind kind, const mpq & right_side) { - constraint_index ci = m_constraints.size(); + constraint_index ci = m_constraints.size(); if (!is_term(j)) { // j is a var auto vc = new lar_var_constraint(j, kind, right_side); m_constraints.push_back(vc); @@ -212,8 +212,8 @@ void add_constraint_from_term_and_create_new_column_row(unsigned term_j, const l } void decide_on_strategy_and_adjust_initial_state() { - lean_assert(strategy_is_undecided()); - if (m_vars_to_ul_pairs.size() > m_settings.column_number_threshold_for_using_lu_in_lar_solver) { + lean_assert(strategy_is_undecided()); + if (m_vars_to_ul_pairs.size() > m_settings.column_number_threshold_for_using_lu_in_lar_solver) { m_settings.simplex_strategy() = simplex_strategy_enum::lu; } else { m_settings.simplex_strategy() = simplex_strategy_enum::tableau_rows; // todo: when to switch to tableau_costs? @@ -239,14 +239,14 @@ void adjust_initial_state() { void adjust_initial_state_for_lu() { copy_from_mpq_matrix(A_d()); - unsigned n = A_d().column_count(); - m_mpq_lar_core_solver.m_d_x.resize(n); - m_mpq_lar_core_solver.m_d_low_bounds.resize(n); - m_mpq_lar_core_solver.m_d_upper_bounds.resize(n); - m_mpq_lar_core_solver.m_d_heading = m_mpq_lar_core_solver.m_r_heading; - m_mpq_lar_core_solver.m_d_basis = m_mpq_lar_core_solver.m_r_basis; + unsigned n = A_d().column_count(); + m_mpq_lar_core_solver.m_d_x.resize(n); + m_mpq_lar_core_solver.m_d_low_bounds.resize(n); + m_mpq_lar_core_solver.m_d_upper_bounds.resize(n); + m_mpq_lar_core_solver.m_d_heading = m_mpq_lar_core_solver.m_r_heading; + m_mpq_lar_core_solver.m_d_basis = m_mpq_lar_core_solver.m_r_basis; - /* + /* unsigned j = A_d().column_count(); A_d().add_column(); lean_assert(m_mpq_lar_core_solver.m_d_x.size() == j); diff --git a/src/util/lp/lar_core_solver.h b/src/util/lp/lar_core_solver.h index 71d69c3a4..7e402d726 100644 --- a/src/util/lp/lar_core_solver.h +++ b/src/util/lp/lar_core_solver.h @@ -550,7 +550,7 @@ public: lean_assert(m_r_solver.m_basis_heading[leaving] >= 0); m_r_solver.change_basis_unconditionally(entering, leaving); if(!m_r_solver.pivot_column_tableau(entering, m_r_solver.m_basis_heading[entering])) { - // unroll the last step + // unroll the last step m_r_solver.change_basis_unconditionally(leaving, entering); #ifdef LEAN_DEBUG bool t = diff --git a/src/util/lp/lar_solver.h b/src/util/lp/lar_solver.h index c8048a550..d4b591154 100644 --- a/src/util/lp/lar_solver.h +++ b/src/util/lp/lar_solver.h @@ -380,8 +380,8 @@ public: bool term_is_used_as_row(unsigned term) const { - lean_assert(is_term(term)); - return contains(m_ext_vars_to_columns, term); + lean_assert(is_term(term)); + return contains(m_ext_vars_to_columns, term); } void propagate_bounds_on_terms(lp_bound_propagator & bp) { @@ -484,16 +484,16 @@ public: void pop(unsigned k) { int n_was = static_cast(m_ext_vars_to_columns.size()); - m_status.pop(k); - m_infeasible_column_index.pop(k); + m_status.pop(k); + m_infeasible_column_index.pop(k); unsigned n = m_vars_to_ul_pairs.peek_size(k); - for (unsigned j = n_was; j-- > n;) - m_ext_vars_to_columns.erase(m_columns_to_ext_vars_or_term_indices[j]); - m_columns_to_ext_vars_or_term_indices.resize(n); - if (m_settings.use_tableau()) { + for (unsigned j = n_was; j-- > n;) + m_ext_vars_to_columns.erase(m_columns_to_ext_vars_or_term_indices[j]); + m_columns_to_ext_vars_or_term_indices.resize(n); + if (m_settings.use_tableau()) { pop_tableau(); } - m_vars_to_ul_pairs.pop(k); + m_vars_to_ul_pairs.pop(k); m_mpq_lar_core_solver.pop(k); clean_large_elements_after_pop(n, m_columns_with_changed_bound); @@ -501,7 +501,7 @@ public: clean_large_elements_after_pop(m, m_rows_with_changed_bounds); clean_inf_set_of_r_solver_after_pop(); lean_assert(m_settings.simplex_strategy() == simplex_strategy_enum::undecided || - (!use_tableau()) || m_mpq_lar_core_solver.m_r_solver.reduced_costs_are_correct_tableau()); + (!use_tableau()) || m_mpq_lar_core_solver.m_r_solver.reduced_costs_are_correct_tableau()); lean_assert(ax_is_correct()); @@ -518,9 +518,9 @@ public: } m_terms.resize(m_term_count); m_orig_terms.resize(m_term_count); - m_simplex_strategy.pop(k); - m_settings.simplex_strategy() = m_simplex_strategy; - lean_assert(sizes_are_correct()); + m_simplex_strategy.pop(k); + m_settings.simplex_strategy() = m_simplex_strategy; + lean_assert(sizes_are_correct()); lean_assert((!m_settings.use_tableau()) || m_mpq_lar_core_solver.m_r_solver.reduced_costs_are_correct_tableau()); } @@ -967,8 +967,8 @@ public: template void copy_from_mpq_matrix(static_matrix & matr) { - matr.m_rows.resize(A_r().row_count()); - matr.m_columns.resize(A_r().column_count()); + matr.m_rows.resize(A_r().row_count()); + matr.m_columns.resize(A_r().column_count()); for (unsigned i = 0; i < matr.row_count(); i++) { for (auto & it : A_r().m_rows[i]) { matr.set(i, it.m_j, convert_struct::convert(it.get_val())); diff --git a/src/util/lp/lp_bound_propagator.cpp b/src/util/lp/lp_bound_propagator.cpp index 8b42f24a0..506ba138b 100644 --- a/src/util/lp/lp_bound_propagator.cpp +++ b/src/util/lp/lp_bound_propagator.cpp @@ -17,11 +17,11 @@ const impq & lp_bound_propagator::get_upper_bound(unsigned j) const { } void lp_bound_propagator::try_add_bound(const mpq & v, unsigned j, bool is_low, bool coeff_before_j_is_pos, unsigned row_or_term_index, bool strict) { unsigned term_j = m_lar_solver.adjust_column_index_to_term_index(j); - mpq w = v; - if (term_j != j) { - j = term_j; - w += m_lar_solver.get_term(term_j).m_v; // when terms are turned into the columns they "lose" the right side, at this moment they aquire it back - } + mpq w = v; + if (term_j != j) { + j = term_j; + w += m_lar_solver.get_term(term_j).m_v; // when terms are turned into the columns they "lose" the right side, at this moment they aquire it back + } lconstraint_kind kind = is_low? GE : LE; if (strict) kind = static_cast(kind / 2); diff --git a/src/util/lp/lp_settings.h b/src/util/lp/lp_settings.h index aac3692f9..ad40ad69d 100644 --- a/src/util/lp/lp_settings.h +++ b/src/util/lp/lp_settings.h @@ -278,13 +278,13 @@ public: return m_simplex_strategy; } - bool use_lu() const { - return m_simplex_strategy == simplex_strategy_enum::lu; - } + bool use_lu() const { + return m_simplex_strategy == simplex_strategy_enum::lu; + } bool use_tableau() const { - return m_simplex_strategy == simplex_strategy_enum::tableau_rows || - m_simplex_strategy == simplex_strategy_enum::tableau_costs; + return m_simplex_strategy == simplex_strategy_enum::tableau_rows || + m_simplex_strategy == simplex_strategy_enum::tableau_costs; } bool use_tableau_rows() const { diff --git a/src/util/lp/lp_utils.h b/src/util/lp/lp_utils.h index 2be15d79a..34cf4f6b9 100644 --- a/src/util/lp/lp_utils.h +++ b/src/util/lp/lp_utils.h @@ -18,7 +18,7 @@ bool try_get_val(const std::unordered_map & map, const A& key, B & val) { template bool contains(const std::unordered_map & map, const A& key) { - return map.find(key) != map.end(); + return map.find(key) != map.end(); } #ifdef lp_for_z3 diff --git a/src/util/lp/stacked_vector.h b/src/util/lp/stacked_vector.h index 3f39dd346..21202b7b8 100644 --- a/src/util/lp/stacked_vector.h +++ b/src/util/lp/stacked_vector.h @@ -51,10 +51,10 @@ public: private: void emplace_replace(unsigned i,const B & b) { - if (m_vector[i] != b) { - m_changes.push_back(std::make_pair(i, m_vector[i])); - m_vector[i] = b; - } + if (m_vector[i] != b) { + m_changes.push_back(std::make_pair(i, m_vector[i])); + m_vector[i] = b; + } } public: @@ -87,14 +87,14 @@ public: } template - void pop_tail(vector & v, unsigned k) { - lean_assert(v.size() >= k); - v.resize(v.size() - k); - } + void pop_tail(vector & v, unsigned k) { + lean_assert(v.size() >= k); + v.resize(v.size() - k); + } template void resize(vector & v, unsigned new_size) { - v.resize(new_size); + v.resize(new_size); } void pop(unsigned k) { @@ -156,10 +156,10 @@ public: m_vector.resize(m_vector.size() + 1); } - unsigned peek_size(unsigned k) const { - lean_assert(k > 0 && k <= m_stack_of_vector_sizes.size()); - return m_stack_of_vector_sizes[m_stack_of_vector_sizes.size() - k]; - } + unsigned peek_size(unsigned k) const { + lean_assert(k > 0 && k <= m_stack_of_vector_sizes.size()); + return m_stack_of_vector_sizes[m_stack_of_vector_sizes.size() - k]; + } const vector& operator()() const { return m_vector; } }; diff --git a/src/util/lp/static_matrix.h b/src/util/lp/static_matrix.h index 5ef4b449f..d027c105f 100644 --- a/src/util/lp/static_matrix.h +++ b/src/util/lp/static_matrix.h @@ -47,7 +47,7 @@ class static_matrix dim(unsigned m, unsigned n) :m_m(m), m_n(n) {} }; std::stack m_stack; - vector m_became_zeros; // the row indices that became zeroes during the pivoting + vector m_became_zeros; // the row indices that became zeroes during the pivoting public: typedef vector> row_strip; typedef vector column_strip; diff --git a/src/util/lp/ul_pair.h b/src/util/lp/ul_pair.h index 2e77a7db0..6331d17b5 100644 --- a/src/util/lp/ul_pair.h +++ b/src/util/lp/ul_pair.h @@ -49,8 +49,8 @@ public: && m_upper_bound_witness == p.m_upper_bound_witness && m_i == p.m_i; } - // empty constructor - ul_pair() : + // empty constructor + ul_pair() : m_low_bound_witness(static_cast(-1)), m_upper_bound_witness(static_cast(-1)), m_i(static_cast(-1)) diff --git a/src/util/map.h b/src/util/map.h index 0d2acf11b..3a59c8975 100644 --- a/src/util/map.h +++ b/src/util/map.h @@ -135,7 +135,7 @@ public: value const& get(key const& k, value const& default_value) const { entry* e = find_core(k); if (e) { - return e->get_data().m_value; + return e->get_data().m_value; } else { return default_value; diff --git a/src/util/max_cliques.h b/src/util/max_cliques.h index 09e40dee1..340d3fee7 100644 --- a/src/util/max_cliques.h +++ b/src/util/max_cliques.h @@ -92,7 +92,7 @@ public: m_next.reserve(std::max(src, dst) + 1); m_next.reserve(std::max(negate(src), negate(dst)) + 1); m_next[src].push_back(dst); - m_next[dst].push_back(src); + m_next[dst].push_back(src); } void cliques(unsigned_vector const& ps, vector& cliques) { @@ -104,7 +104,7 @@ public: max = std::max(max, std::max(np, p) + 1); } m_next.reserve(max); - m_tc.reserve(m_next.size()); + m_tc.reserve(m_next.size()); unsigned_vector clique; uint_set vars; for (unsigned i = 0; i < num_ps; ++i) { diff --git a/src/util/rational.h b/src/util/rational.h index ca294e234..803c562ad 100644 --- a/src/util/rational.h +++ b/src/util/rational.h @@ -422,7 +422,7 @@ inline bool operator>(rational const & r1, rational const & r2) { } inline bool operator<(rational const & r1, int r2) { - return r1 < rational(r2); + return r1 < rational(r2); } inline bool operator<=(rational const & r1, rational const & r2) { @@ -450,11 +450,11 @@ inline rational operator+(rational const & r1, rational const & r2) { } inline rational operator+(int r1, rational const & r2) { - return rational(r1) + r2; + return rational(r1) + r2; } inline rational operator+(rational const & r1, int r2) { - return r1 + rational(r2); + return r1 + rational(r2); } @@ -463,11 +463,11 @@ inline rational operator-(rational const & r1, rational const & r2) { } inline rational operator-(rational const & r1, int r2) { - return r1 - rational(r2); + return r1 - rational(r2); } inline rational operator-(int r1, rational const & r2) { - return rational(r1) - r2; + return rational(r1) - r2; } inline rational operator-(rational const & r) { @@ -492,11 +492,11 @@ inline rational operator/(rational const & r1, rational const & r2) { } inline rational operator/(rational const & r1, int r2) { - return r1 / rational(r2); + return r1 / rational(r2); } -inline rational operator/(int r1, rational const & r2) { - return rational(r1) / r2; +inline rational operator/(int r1, rational const & r2) { + return rational(r1) / r2; } inline rational power(rational const & r, unsigned p) { diff --git a/src/util/stopwatch.h b/src/util/stopwatch.h index 7a9066030..7f2ed3245 100644 --- a/src/util/stopwatch.h +++ b/src/util/stopwatch.h @@ -110,7 +110,7 @@ public: mach_timespec_t _stop; clock_get_time(m_host_clock, &_stop); m_time += (_stop.tv_sec - m_start.tv_sec) * 1000000000ull; - m_time += (_stop.tv_nsec - m_start.tv_nsec); + m_time += (_stop.tv_nsec - m_start.tv_nsec); m_running = false; } } @@ -163,8 +163,8 @@ public: struct timespec _stop; clock_gettime(CLOCK_PROCESS_CPUTIME_ID, &_stop); m_time += (_stop.tv_sec - m_start.tv_sec) * 1000000000ull; - if (m_time != 0 || _stop.tv_nsec >= m_start.tv_nsec) - m_time += (_stop.tv_nsec - m_start.tv_nsec); + if (m_time != 0 || _stop.tv_nsec >= m_start.tv_nsec) + m_time += (_stop.tv_nsec - m_start.tv_nsec); m_running = false; } } diff --git a/src/util/util.h b/src/util/util.h index 440877619..23c2c1657 100644 --- a/src/util/util.h +++ b/src/util/util.h @@ -153,13 +153,13 @@ template char (*ArraySizer(T (&)[N]))[N]; template void display(std::ostream & out, const IT & begin, const IT & end, const char * sep, bool & first) { for(IT it = begin; it != end; ++it) { - if (first) { - first = false; - } - else { - out << sep; - } - out << *it; + if (first) { + first = false; + } + else { + out << sep; + } + out << *it; } } @@ -172,9 +172,9 @@ void display(std::ostream & out, const IT & begin, const IT & end, const char * template struct delete_proc { void operator()(T * ptr) { - if (ptr) { - dealloc(ptr); - } + if (ptr) { + dealloc(ptr); + } } };