diff --git a/src/duality/duality.h b/src/duality/duality.h index a37896af1..fc70ffa70 100755 --- a/src/duality/duality.h +++ b/src/duality/duality.h @@ -1,1319 +1,1321 @@ -/*++ -Copyright (c) 2012 Microsoft Corporation - -Module Name: - - duality.h - -Abstract: - - main header for duality - -Author: - - Ken McMillan (kenmcmil) - -Revision History: - - ---*/ - -#pragma once - -#include "duality_wrapper.h" -#include -#include - -// make hash_map and hash_set available -using namespace stl_ext; - -namespace Duality { - - class implicant_solver; - - /* Generic operations on Z3 formulas */ - - struct Z3User { - - context &ctx; - - typedef func_decl FuncDecl; - 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); - - Term CloneQuantifier(const Term &t, const Term &new_body); - - Term SubstRec(hash_map &memo, const Term &t); - - Term SubstRec(hash_map &memo, hash_map &map, const Term &t); - - void Strengthen(Term &x, const Term &y); - - // return the func_del of an app if it is uninterpreted - - bool get_relation(const Term &t, func_decl &R); - - // return true if term is an individual variable - // TODO: have to check that it is not a background symbol - - bool is_variable(const Term &t); - - FuncDecl SuffixFuncDecl(Term t, int n); - - - Term SubstRecHide(hash_map &memo, const Term &t, int number); - - void CollectConjuncts(const Term &f, std::vector &lits, bool pos = true); - - void SortTerms(std::vector &terms); - - Term SortSum(const Term &t); - - void Summarize(const Term &t); - - int CountOperators(const Term &t); - - Term SubstAtom(hash_map &memo, const expr &t, const expr &atom, const expr &val); - - Term CloneQuantAndSimp(const expr &t, const expr &body); - - Term RemoveRedundancy(const Term &t); - - Term IneqToEq(const Term &t); - - bool IsLiteral(const expr &lit, expr &atom, expr &val); - - expr Negate(const expr &f); - - expr SimplifyAndOr(const std::vector &args, bool is_and); - - expr ReallySimplifyAndOr(const std::vector &args, bool is_and); - - int MaxIndex(hash_map &memo, const Term &t); - - bool IsClosedFormula(const Term &t); - - Term AdjustQuantifiers(const Term &t); - - FuncDecl RenumberPred(const FuncDecl &f, int n); - - Term ExtractStores(hash_map &memo, const Term &t, std::vector &cnstrs, hash_map &renaming); - - -protected: - - void SummarizeRec(hash_set &memo, std::vector &lits, int &ops, const Term &t); - int CountOperatorsRec(hash_set &memo, const Term &t); - void RemoveRedundancyOp(bool pol, std::vector &args, hash_map &smemo); - Term RemoveRedundancyRec(hash_map &memo, hash_map &smemo, const Term &t); - Term SubstAtomTriv(const expr &foo, const expr &atom, const expr &val); - expr ReduceAndOr(const std::vector &args, bool is_and, std::vector &res); - expr FinishAndOr(const std::vector &args, bool is_and); - expr PullCommonFactors(std::vector &args, bool is_and); - Term IneqToEqRec(hash_map &memo, const Term &t); - Term CloneQuantAndSimp(const expr &t, const expr &body, bool is_forall); - Term PushQuantifier(const expr &t, const expr &body, bool is_forall); - - -}; - - /** 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. - * - * */ - 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? */ - solver aux_solver; /** For temporary use -- don't leave assertions here. */ - - /** Tree interpolation. This method assumes the formulas in TermTree - "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. - */ - - virtual - lbool interpolate_tree(TermTree *assumptions, - TermTree *&interpolants, - model &_model, - TermTree *goals = 0, - bool weak = false - ) = 0; - - /** Declare a constant in the background theory. */ - virtual void declare_constant(const func_decl &f) = 0; - - /** Is this a background constant? */ - virtual bool is_constant(const func_decl &f) = 0; - - /** Get the constants in the background vocabulary */ - virtual hash_set &get_constants() = 0; - - /** Assert a background axiom. */ - virtual void assert_axiom(const expr &axiom) = 0; - - /** Get the background axioms. */ - virtual const std::vector &get_axioms() = 0; - - /** Return a string describing performance. */ - virtual std::string profile() = 0; - - virtual void write_interpolation_problem(const std::string &file_name, - const std::vector &assumptions, - const std::vector &theory - ){} - - /** Cancel, throw Canceled object if possible. */ - virtual void cancel(){ } - - /* Note: aux solver uses extensional array theory, since it - needs to be able to produce counter-models for - interpolants the have array equalities in them. - */ - LogicSolver(context &c) : aux_solver(c,true){} - - virtual ~LogicSolver(){} - }; - - /** This solver uses iZ3. */ - class iZ3LogicSolver : public LogicSolver { - public: - interpolating_context *ictx; /** iZ3 context for formulas */ - interpolating_solver *islvr; /** iZ3 solver */ - - lbool interpolate_tree(TermTree *assumptions, - TermTree *&interpolants, - model &_model, - TermTree *goals = 0, - bool weak = false) - { - literals _labels; - islvr->SetWeakInterpolants(weak); - return islvr->interpolate_tree(assumptions,interpolants,_model,_labels,true); - } - - void assert_axiom(const expr &axiom){ - islvr->AssertInterpolationAxiom(axiom); - } - - const std::vector &get_axioms() { - return islvr->GetInterpolationAxioms(); - } - - std::string profile(){ - return islvr->profile(); - } - -#if 0 - iZ3LogicSolver(config &_config){ - ctx = ictx = new interpolating_context(_config); - slvr = islvr = new interpolating_solver(*ictx); - need_goals = false; - islvr->SetWeakInterpolants(true); - } -#endif - - iZ3LogicSolver(context &c, bool models = true) : LogicSolver(c) { - ctx = ictx = &c; - slvr = islvr = new interpolating_solver(*ictx, models); - need_goals = false; - islvr->SetWeakInterpolants(true); - } - - void write_interpolation_problem(const std::string &file_name, - const std::vector &assumptions, - const std::vector &theory - ){ -#if 0 - islvr->write_interpolation_problem(file_name,assumptions,theory); -#endif - - } - - void cancel(){islvr->cancel();} - - /** Declare a constant in the background theory. */ - 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(); - } - - /** Get the constants in the background vocabulary */ - virtual hash_set &get_constants(){ - return bckg; - } - - ~iZ3LogicSolver(){ - // delete ictx; - delete islvr; - } - private: - hash_set bckg; - - }; - -#if 0 - /** Create a logic solver from a Z3 configuration. */ - static iZ3LogicSolver *CreateLogicSolver(config &_config){ - return new iZ3LogicSolver(_config); - } -#endif - - /** 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); - } - - LogicSolver *ls; - - protected: - int nodeCount; - int edgeCount; - - class stack_entry - { - public: - std::list edges; - std::list nodes; - std::list > constraints; - }; - - - public: - model dualModel; - protected: - literals dualLabels; - std::list stack; - 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. - */ - - RPFP(LogicSolver *_ls) : Z3User(*(_ls->ctx)), dualModel(*(_ls->ctx)), aux_solver(_ls->aux_solver) - { - ls = _ls; - nodeCount = 0; - edgeCount = 0; - stack.push_back(stack_entry()); - HornClauses = false; - proof_core = 0; - } - - virtual ~RPFP(); - - /** Symbolic representation of a relational transformer */ - class Transformer - { - public: - std::vector RelParams; - std::vector IndParams; - Term Formula; - RPFP *owner; - hash_map labels; - - Transformer *Clone() - { - return new Transformer(*this); - } - - void SetEmpty(){ - Formula = owner->ctx.bool_val(false); - } - - void SetFull(){ - Formula = owner->ctx.bool_val(true); - } - - bool IsEmpty(){ - return eq(Formula,owner->ctx.bool_val(false)); - } - - bool IsFull(){ - return eq(Formula,owner->ctx.bool_val(true)); - } - - void UnionWith(const Transformer &other){ - Term t = owner->SubstParams(other.IndParams,IndParams,other.Formula); - Formula = Formula || t; - } - - void IntersectWith(const Transformer &other){ - Term t = owner->SubstParams(other.IndParams,IndParams,other.Formula); - Formula = Formula && t; - } - - bool SubsetEq(const Transformer &other){ - Term t = owner->SubstParams(other.IndParams,IndParams,other.Formula); - expr test = Formula && !t; - owner->aux_solver.push(); - owner->aux_solver.add(test); - check_result res = owner->aux_solver.check(); - owner->aux_solver.pop(1); - return res == unsat; - } - - void Complement(){ - Formula = !Formula; - } - - void Simplify(){ - Formula = Formula.simplify(); - } - - 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) - { - // var ops = new Util.ContextOps(ctx); - // var foo = ops.simplify_lhs(_Formula); - // t.Formula = foo.Item1; - // 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 - { - public: - FuncDecl Name; - Transformer Annotation; - Transformer Bound; - Transformer Underapprox; - RPFP *owner; - int number; - Edge *Outgoing; - std::vector Incoming; - Term dual; - Node *map; - - 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;} - }; - - /** 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; - int nargs = t.num_args(); - for(int i = 0; i < nargs; i++) - _IndParams.push_back(t.arg(i)); - Node *n = new Node(t.decl(), - CreateRelation(_IndParams,ctx.bool_val(true)), - CreateRelation(_IndParams,ctx.bool_val(true)), - CreateRelation(_IndParams,ctx.bool_val(false)), - expr(ctx), this, ++nodeCount - ); - nodes.push_back(n); - return n; - } - - /** Clone a node (can be from another graph). */ - - Node *CloneNode(Node *old) - { - Node *n = new Node(old->Name, - old->Annotation, - old->Bound, - old->Underapprox, - expr(ctx), - this, - ++nodeCount - ); - nodes.push_back(n); - 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()) - throw "cannot delete RPFP node"; - for(std::vector::iterator it = nodes.end(), en = nodes.begin(); it != en;){ - if(*(--it) == node){ - nodes.erase(it); - break; - } - } - delete node; - } - - /** This class represents a hyper-edge in the RPFP graph */ - - class Edge - { - public: - Transformer F; - Node *Parent; - std::vector Children; - RPFP *owner; - int number; - // these should be internal... - Term dual; - hash_map relMap; - hash_map varMap; - 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) - { - Edge *e = new Edge(_Parent,_F,_Children,this,++edgeCount); - _Parent->Outgoing = e; - for(unsigned i = 0; i < _Children.size(); i++) - _Children[i]->Incoming.push_back(e); - edges.push_back(e); - return e; - } - - - /** Delete a hyper-edge and unlink it from any nodes. */ - void DeleteEdge(Edge *edge){ - if(edge->Parent) - edge->Parent->Outgoing = 0; - for(unsigned int i = 0; i < edge->Children.size(); i++){ - std::vector &ic = edge->Children[i]->Incoming; - for(std::vector::iterator it = ic.begin(), en = ic.end(); it != en; ++it){ - if(*it == edge){ - ic.erase(it); - break; - } - } - } - for(std::vector::iterator it = edges.end(), en = edges.begin(); it != en;){ - if(*(--it) == edge){ - edges.erase(it); - break; - } - } - 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. */ - - void ConstrainParent(Edge *parent, Node *child); - - /** 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. - */ - 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. */ - - void DeclareConstant(const FuncDecl &f); - - /** Assert a background axiom. Background axioms can be used to provide the - * theory of auxilliary functions or relations. All symbols appearing in - * background axioms are considered global, and may appear in both transformer - * and relational solutions. Semantically, a solution to the RPFP gives - * an interpretation of the unknown relations for each interpretation of the - * auxilliary symbols that is consistent with the axioms. Axioms should be - * asserted before any calls to Push. They cannot be de-asserted by Pop. */ - - void AssertAxiom(const Term &t); - -#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). - * - * 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. - * - * 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 - * - * - */ - - 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(), - 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", - based on a previously computed counterexample. */ - - Term ComputeUnderapprox(Node *root, int persist); - - /** Try to strengthen the annotation of a node by removing disjuncts. */ - void Generalize(Node *root, Node *node); - - - /** Compute disjunctive interpolant for node by case splitting */ - 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; - bad_clause(const std::string &_msg, int _i){ - msg = _msg; - i = _i; - } - }; - - struct parse_error { - std::string msg; - parse_error(const std::string &_msg){ - msg = _msg; - } - }; - - struct file_not_found { - }; - - struct bad_format { - }; - - // thrown on internal error - struct Bad { - }; - - /** 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 - - 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) {} - }; - - -#ifdef _WINDOWS - __declspec(dllexport) -#endif - void FromClauses(const std::vector &clauses); - - void FromFixpointContext(fixedpoint fp, std::vector &queries); - - void WriteSolution(std::ostream &s); - - void WriteCounterexample(std::ostream &s, Node *node); - - 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); - - /** Read the RPFP from a file (in specificed format) */ - void ReadProblemFromFile(std::string filename, FileFormat format = DualityFormat); - - /** Translate problem to Horn clause form */ - void ToClauses(std::vector &cnsts, FileFormat format = DualityFormat); - - /** Translate the RPFP to a fixed point context, with queries */ - fixedpoint ToFixedPointProblem(std::vector &queries); - - /** Nodes of the graph. */ - std::vector nodes; - - /** Edges of the graph. */ - std::vector edges; - - /** 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_1(r_11,...,r_iN(1)) U ... U T_M(r_M1,...,r_MN(M)) - */ - - Transformer Fuse(const std::vector &trs); - - /** Fuse edges so that each node is the output of at most one edge. This - transformation is solution-preserving, but changes the numbering of edges in - counterexamples. - */ - void FuseEdges(); - - void RemoveDeadNodes(); - - Term SubstParams(const std::vector &from, - const std::vector &to, const Term &t); - - Term SubstParamsNoCapture(const std::vector &from, - const std::vector &to, const Term &t); - - Term Localize(Edge *e, const Term &t); - - void EvalNodeAsConstraint(Node *p, Transformer &res); - - TermTree *GetGoalTree(Node *root); - - int EvalTruth(hash_map &memo, Edge *e, const Term &f); - - void GetLabels(Edge *e, std::vector &labels); - - // int GetLabelsRec(hash_map *memo, const Term &f, std::vector &labels, bool labpos); - - /** Compute and save the proof core for future calls to - EdgeUsedInProof. You only need to call this if you will pop - the solver before calling EdgeUsedInProof. - */ - void ComputeProofCore(); - - int CumulativeDecisions(); - - solver &slvr(){ - return *ls->slvr; - } - - protected: - - void ClearProofCore(){ - if(proof_core) - delete proof_core; - proof_core = 0; - } - - Term SuffixVariable(const Term &t, int n); - - Term HideVariable(const Term &t, int n); - - void RedVars(Node *node, Term &b, std::vector &v); - - Term RedDualRela(Edge *e, std::vector &args, int idx); - - Term LocalizeRec(Edge *e, hash_map &memo, const Term &t); - - void SetEdgeMaps(Edge *e); - - Term ReducedDualEdge(Edge *e); - - TermTree *ToTermTree(Node *root, Node *skip_descendant = 0); - - TermTree *ToGoalTree(Node *root); - - void CollapseTermTreeRec(TermTree *root, TermTree *node); - - TermTree *CollapseTermTree(TermTree *node); - - void DecodeTree(Node *root, TermTree *interp, int persist); - - Term GetUpperBound(Node *n); - - TermTree *AddUpperBound(Node *root, TermTree *t); - -#if 0 - void WriteInterps(System.IO.StreamWriter f, TermTree t); -#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, - const Term &t, - hash_map &pmap, - std::vector &res, - std::vector &nodes); - - Term RemoveLabelsRec(hash_map &memo, const Term &t, std::vector &lbls); - - Term RemoveLabels(const Term &t, std::vector &lbls); - - Term GetAnnotation(Node *n); - - - Term GetUnderapprox(Node *n); - - Term UnderapproxFlag(Node *n); - - hash_map underapprox_flag_rev; - - Node *UnderapproxFlagRev(const Term &flag); - - Term ProjectFormula(std::vector &keep_vec, const Term &f); - - int SubtermTruth(hash_map &memo, const Term &); - - void ImplicantRed(hash_map &memo, const Term &f, std::vector &lits, - hash_set *done, bool truth, hash_set &dont_cares); - - void Implicant(hash_map &memo, const Term &f, std::vector &lits, hash_set &dont_cares); - - Term UnderapproxFormula(const Term &f, hash_set &dont_cares); - - void ImplicantFullRed(hash_map &memo, const Term &f, std::vector &lits, - hash_set &done, hash_set &dont_cares, bool extensional = true); - - public: - Term UnderapproxFullFormula(const Term &f, bool extensional = true); - - protected: - Term ToRuleRec(Edge *e, hash_map &memo, const Term &t, std::vector &quants); - - hash_map resolve_ite_memo; - - Term ResolveIte(hash_map &memo, const Term &t, std::vector &lits, - hash_set *done, hash_set &dont_cares); - - struct ArrayValue { - bool defined; - std::map entries; - expr def_val; - }; - - void EvalArrayTerm(const Term &t, ArrayValue &res); - - Term EvalArrayEquality(const Term &f); - - Term ModelValueAsConstraint(const Term &t); - - void GetLabelsRec(hash_map &memo, const Term &f, std::vector &labels, - hash_set *done, bool truth); - - Term SubstBoundRec(hash_map > &memo, hash_map &subst, int level, const Term &t); - - Term SubstBound(hash_map &subst, const Term &t); - - void ConstrainEdgeLocalized(Edge *e, const Term &t); - - void GreedyReduce(solver &s, std::vector &conjuncts); - - void NegateLits(std::vector &lits); - - expr SimplifyOr(std::vector &lits); - - expr SimplifyAnd(std::vector &lits); - - void SetAnnotation(Node *root, const expr &t); - - void AddEdgeToSolver(Edge *edge); - - void AddEdgeToSolver(implicant_solver &aux_solver, Edge *edge); - - void AddToProofCore(hash_set &core); - - 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); - - bool IsVar(const expr &t); - - void GetVarsRec(hash_set &memo, const expr &cnst, std::vector &vars); - - 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); - - expr GetRel(Edge *edge, int child_idx); - - void GetDefs(const expr &cnst, hash_map &defs); - - void GetDefsRec(const expr &cnst, hash_map &defs); - - void AddParamsToNode(Node *node, const std::vector ¶ms); - - 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); - - 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, - TermTree *&interpolants, - model &_model, - TermTree *goals = 0, - bool weak = false); - - virtual bool proof_core_contains(const expr &e); - - }; - - - /** RPFP solver base class. */ - - class Solver { - - public: - - class Counterexample { - private: - RPFP *tree; - RPFP::Node *root; - public: - Counterexample(){ - tree = 0; - root = 0; - } - Counterexample(RPFP *_tree, RPFP::Node *_root){ - tree = _tree; - root = _root; - } - ~Counterexample(){ - if(tree) delete tree; - } - void swap(Counterexample &other){ - std::swap(tree,other.tree); - std::swap(root,other.root); - } - void set(RPFP *_tree, RPFP::Node *_root){ - if(tree) delete tree; - tree = _tree; - root = _root; - } - void clear(){ - if(tree) delete tree; - tree = 0; - } - RPFP *get_tree() const {return tree;} - RPFP::Node *get_root() const {return root;} - private: - 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. */ - - virtual void LearnFrom(Solver *old_solver) = 0; - - virtual ~Solver(){} - - static Solver *Create(const std::string &solver_class, RPFP *rpfp); - - /** This can be called asynchrnously to cause Solve to throw a - Canceled exception at some time in the future. - */ - virtual void Cancel() = 0; - - /** Object thrown on cancellation */ - struct Canceled {}; - - /** Object thrown on incompleteness */ - struct Incompleteness {}; - }; -} - - -// Allow to hash on nodes and edges in deterministic way - -namespace hash_space { - template <> - class hash { - public: - size_t operator()(const Duality::RPFP::Node *p) const { - return p->number; - } - }; -} - -namespace hash_space { - template <> - class hash { - public: - size_t operator()(const Duality::RPFP::Edge *p) const { - return p->number; - } - }; -} - -// allow to walk sets of nodes without address dependency - -namespace std { - template <> - class less { - public: - bool operator()(Duality::RPFP::Node * const &s, Duality::RPFP::Node * const &t) const { - return s->number < t->number; // s.raw()->get_id() < t.raw()->get_id(); - } - }; -} - -// #define LIMIT_STACK_WEIGHT 5 - - -namespace Duality { - /** Caching version of RPFP. Instead of asserting constraints, returns assumption literals */ - - class RPFP_caching : public RPFP { - public: - - /** appends assumption literals for edge to lits. if with_children is true, - 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); - - /** Get the clone of a node */ - Node *GetNodeClone(Node *other_node); - - /** Get the clone of an edge */ - Edge *GetEdgeClone(Edge *other_edge); - - /** Try to strengthen the parent of an edge */ - void GeneralizeCache(Edge *edge); - - /** Try to propagate some facts from children to parents of edge. - Return true if success. */ - bool PropagateCache(Edge *edge); - - /** Construct a caching RPFP using a LogicSolver */ - RPFP_caching(LogicSolver *_ls) : RPFP(_ls) {} - - /** Constraint an edge by its child's annotation. Return - assumption lits. */ - void ConstrainParentCache(Edge *parent, Node *child, std::vector &lits); - -#ifdef LIMIT_STACK_WEIGHT - virtual void AssertEdge(Edge *e, int persist = 0, bool with_children = false, bool underapprox = false); -#endif - - virtual ~RPFP_caching(){} - - protected: - hash_map AssumptionLits; - hash_map NodeCloneMap; - hash_map EdgeCloneMap; - std::vector alit_stack; - std::vector alit_stack_sizes; - - // to let us use one solver per edge - struct edge_solver { - hash_map AssumptionLits; - uptr slvr; - }; - hash_map edge_solvers; - -#ifdef LIMIT_STACK_WEIGHT - struct weight_counter { - int val; - weight_counter(){val = 0;} - void swap(weight_counter &other){ - std::swap(val,other.val); - } - }; - - struct big_stack_entry { - weight_counter weight_added; - std::vector new_alits; - std::vector alit_stack; - std::vector alit_stack_sizes; - }; - - std::vector new_alits; - weight_counter weight_added; - std::vector big_stack; -#endif - - - - void GetAssumptionLits(const expr &fmla, std::vector &lits, hash_map *opt_map = 0); - - void GreedyReduceCache(std::vector &assumps, std::vector &core); - - void FilterCore(std::vector &core, std::vector &full_core); - 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, - TermTree *&interpolants, - model &_model, - TermTree *goals = 0, - bool weak = false); - - virtual bool proof_core_contains(const expr &e); - - void GetTermTreeAssertionLiterals(TermTree *assumptions); - - void GetTermTreeAssertionLiteralsRec(TermTree *assumptions); - - edge_solver &SolverForEdge(Edge *edge, bool models, bool axioms); - - public: - struct scoped_solver_for_edge { - solver *orig_slvr; - RPFP_caching *rpfp; - edge_solver *es; - 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)); - rpfp->ls->slvr = es->slvr.get(); - rpfp->AssumptionLits.swap(es->AssumptionLits); - } - ~scoped_solver_for_edge(){ - rpfp->ls->slvr = orig_slvr; - rpfp->AssumptionLits.swap(es->AssumptionLits); - } - }; - - }; - -} +/*++ +Copyright (c) 2012 Microsoft Corporation + +Module Name: + + duality.h + +Abstract: + + main header for duality + +Author: + + Ken McMillan (kenmcmil) + +Revision History: + + +--*/ + +#pragma once + +#include "duality_wrapper.h" +#include +#include + +// make hash_map and hash_set available +using namespace stl_ext; + +namespace Duality { + + class implicant_solver; + + /* Generic operations on Z3 formulas */ + + struct Z3User { + + context &ctx; + + typedef func_decl FuncDecl; + 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); + + Term CloneQuantifier(const Term &t, const Term &new_body); + + Term SubstRec(hash_map &memo, const Term &t); + + Term SubstRec(hash_map &memo, hash_map &map, const Term &t); + + void Strengthen(Term &x, const Term &y); + + // return the func_del of an app if it is uninterpreted + + bool get_relation(const Term &t, func_decl &R); + + // return true if term is an individual variable + // TODO: have to check that it is not a background symbol + + bool is_variable(const Term &t); + + FuncDecl SuffixFuncDecl(Term t, int n); + + + Term SubstRecHide(hash_map &memo, const Term &t, int number); + + void CollectConjuncts(const Term &f, std::vector &lits, bool pos = true); + + void SortTerms(std::vector &terms); + + Term SortSum(const Term &t); + + void Summarize(const Term &t); + + int CountOperators(const Term &t); + + Term SubstAtom(hash_map &memo, const expr &t, const expr &atom, const expr &val); + + Term CloneQuantAndSimp(const expr &t, const expr &body); + + Term RemoveRedundancy(const Term &t); + + Term IneqToEq(const Term &t); + + bool IsLiteral(const expr &lit, expr &atom, expr &val); + + expr Negate(const expr &f); + + expr SimplifyAndOr(const std::vector &args, bool is_and); + + expr ReallySimplifyAndOr(const std::vector &args, bool is_and); + + int MaxIndex(hash_map &memo, const Term &t); + + bool IsClosedFormula(const Term &t); + + Term AdjustQuantifiers(const Term &t); + + FuncDecl RenumberPred(const FuncDecl &f, int n); + + Term ExtractStores(hash_map &memo, const Term &t, std::vector &cnstrs, hash_map &renaming); + + +protected: + + void SummarizeRec(hash_set &memo, std::vector &lits, int &ops, const Term &t); + int CountOperatorsRec(hash_set &memo, const Term &t); + void RemoveRedundancyOp(bool pol, std::vector &args, hash_map &smemo); + Term RemoveRedundancyRec(hash_map &memo, hash_map &smemo, const Term &t); + Term SubstAtomTriv(const expr &foo, const expr &atom, const expr &val); + expr ReduceAndOr(const std::vector &args, bool is_and, std::vector &res); + expr FinishAndOr(const std::vector &args, bool is_and); + expr PullCommonFactors(std::vector &args, bool is_and); + Term IneqToEqRec(hash_map &memo, const Term &t); + Term CloneQuantAndSimp(const expr &t, const expr &body, bool is_forall); + Term PushQuantifier(const expr &t, const expr &body, bool is_forall); + void CollectJuncts(const Term &f, std::vector &lits, decl_kind op, bool negate); + Term DeleteBoundRec(hash_map > &memo, int level, int num, const Term &t); + Term DeleteBound(int level, int num, const Term &t); + +}; + + /** 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. + * + * */ + 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? */ + solver aux_solver; /** For temporary use -- don't leave assertions here. */ + + /** Tree interpolation. This method assumes the formulas in TermTree + "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. + */ + + virtual + lbool interpolate_tree(TermTree *assumptions, + TermTree *&interpolants, + model &_model, + TermTree *goals = 0, + bool weak = false + ) = 0; + + /** Declare a constant in the background theory. */ + virtual void declare_constant(const func_decl &f) = 0; + + /** Is this a background constant? */ + virtual bool is_constant(const func_decl &f) = 0; + + /** Get the constants in the background vocabulary */ + virtual hash_set &get_constants() = 0; + + /** Assert a background axiom. */ + virtual void assert_axiom(const expr &axiom) = 0; + + /** Get the background axioms. */ + virtual const std::vector &get_axioms() = 0; + + /** Return a string describing performance. */ + virtual std::string profile() = 0; + + virtual void write_interpolation_problem(const std::string &file_name, + const std::vector &assumptions, + const std::vector &theory + ){} + + /** Cancel, throw Canceled object if possible. */ + virtual void cancel(){ } + + /* Note: aux solver uses extensional array theory, since it + needs to be able to produce counter-models for + interpolants the have array equalities in them. + */ + LogicSolver(context &c) : aux_solver(c,true){} + + virtual ~LogicSolver(){} + }; + + /** This solver uses iZ3. */ + class iZ3LogicSolver : public LogicSolver { + public: + interpolating_context *ictx; /** iZ3 context for formulas */ + interpolating_solver *islvr; /** iZ3 solver */ + + lbool interpolate_tree(TermTree *assumptions, + TermTree *&interpolants, + model &_model, + TermTree *goals = 0, + bool weak = false) + { + literals _labels; + islvr->SetWeakInterpolants(weak); + return islvr->interpolate_tree(assumptions,interpolants,_model,_labels,true); + } + + void assert_axiom(const expr &axiom){ + islvr->AssertInterpolationAxiom(axiom); + } + + const std::vector &get_axioms() { + return islvr->GetInterpolationAxioms(); + } + + std::string profile(){ + return islvr->profile(); + } + +#if 0 + iZ3LogicSolver(config &_config){ + ctx = ictx = new interpolating_context(_config); + slvr = islvr = new interpolating_solver(*ictx); + need_goals = false; + islvr->SetWeakInterpolants(true); + } +#endif + + iZ3LogicSolver(context &c, bool models = true) : LogicSolver(c) { + ctx = ictx = &c; + slvr = islvr = new interpolating_solver(*ictx, models); + need_goals = false; + islvr->SetWeakInterpolants(true); + } + + void write_interpolation_problem(const std::string &file_name, + const std::vector &assumptions, + const std::vector &theory + ){ +#if 0 + islvr->write_interpolation_problem(file_name,assumptions,theory); +#endif + + } + + void cancel(){islvr->cancel();} + + /** Declare a constant in the background theory. */ + 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(); + } + + /** Get the constants in the background vocabulary */ + virtual hash_set &get_constants(){ + return bckg; + } + + ~iZ3LogicSolver(){ + // delete ictx; + delete islvr; + } + private: + hash_set bckg; + + }; + +#if 0 + /** Create a logic solver from a Z3 configuration. */ + static iZ3LogicSolver *CreateLogicSolver(config &_config){ + return new iZ3LogicSolver(_config); + } +#endif + + /** 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); + } + + LogicSolver *ls; + + protected: + int nodeCount; + int edgeCount; + + class stack_entry + { + public: + std::list edges; + std::list nodes; + std::list > constraints; + }; + + + public: + model dualModel; + protected: + literals dualLabels; + std::list stack; + 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. + */ + + RPFP(LogicSolver *_ls) : Z3User(*(_ls->ctx)), dualModel(*(_ls->ctx)), aux_solver(_ls->aux_solver) + { + ls = _ls; + nodeCount = 0; + edgeCount = 0; + stack.push_back(stack_entry()); + HornClauses = false; + proof_core = 0; + } + + virtual ~RPFP(); + + /** Symbolic representation of a relational transformer */ + class Transformer + { + public: + std::vector RelParams; + std::vector IndParams; + Term Formula; + RPFP *owner; + hash_map labels; + + Transformer *Clone() + { + return new Transformer(*this); + } + + void SetEmpty(){ + Formula = owner->ctx.bool_val(false); + } + + void SetFull(){ + Formula = owner->ctx.bool_val(true); + } + + bool IsEmpty(){ + return eq(Formula,owner->ctx.bool_val(false)); + } + + bool IsFull(){ + return eq(Formula,owner->ctx.bool_val(true)); + } + + void UnionWith(const Transformer &other){ + Term t = owner->SubstParams(other.IndParams,IndParams,other.Formula); + Formula = Formula || t; + } + + void IntersectWith(const Transformer &other){ + Term t = owner->SubstParams(other.IndParams,IndParams,other.Formula); + Formula = Formula && t; + } + + bool SubsetEq(const Transformer &other){ + Term t = owner->SubstParams(other.IndParams,IndParams,other.Formula); + expr test = Formula && !t; + owner->aux_solver.push(); + owner->aux_solver.add(test); + check_result res = owner->aux_solver.check(); + owner->aux_solver.pop(1); + return res == unsat; + } + + void Complement(){ + Formula = !Formula; + } + + void Simplify(){ + Formula = Formula.simplify(); + } + + 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) + { + // var ops = new Util.ContextOps(ctx); + // var foo = ops.simplify_lhs(_Formula); + // t.Formula = foo.Item1; + // 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 + { + public: + FuncDecl Name; + Transformer Annotation; + Transformer Bound; + Transformer Underapprox; + RPFP *owner; + int number; + Edge *Outgoing; + std::vector Incoming; + Term dual; + Node *map; + + 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;} + }; + + /** 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; + int nargs = t.num_args(); + for(int i = 0; i < nargs; i++) + _IndParams.push_back(t.arg(i)); + Node *n = new Node(t.decl(), + CreateRelation(_IndParams,ctx.bool_val(true)), + CreateRelation(_IndParams,ctx.bool_val(true)), + CreateRelation(_IndParams,ctx.bool_val(false)), + expr(ctx), this, ++nodeCount + ); + nodes.push_back(n); + return n; + } + + /** Clone a node (can be from another graph). */ + + Node *CloneNode(Node *old) + { + Node *n = new Node(old->Name, + old->Annotation, + old->Bound, + old->Underapprox, + expr(ctx), + this, + ++nodeCount + ); + nodes.push_back(n); + 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()) + throw "cannot delete RPFP node"; + for(std::vector::iterator it = nodes.end(), en = nodes.begin(); it != en;){ + if(*(--it) == node){ + nodes.erase(it); + break; + } + } + delete node; + } + + /** This class represents a hyper-edge in the RPFP graph */ + + class Edge + { + public: + Transformer F; + Node *Parent; + std::vector Children; + RPFP *owner; + int number; + // these should be internal... + Term dual; + hash_map relMap; + hash_map varMap; + 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) + { + Edge *e = new Edge(_Parent,_F,_Children,this,++edgeCount); + _Parent->Outgoing = e; + for(unsigned i = 0; i < _Children.size(); i++) + _Children[i]->Incoming.push_back(e); + edges.push_back(e); + return e; + } + + + /** Delete a hyper-edge and unlink it from any nodes. */ + void DeleteEdge(Edge *edge){ + if(edge->Parent) + edge->Parent->Outgoing = 0; + for(unsigned int i = 0; i < edge->Children.size(); i++){ + std::vector &ic = edge->Children[i]->Incoming; + for(std::vector::iterator it = ic.begin(), en = ic.end(); it != en; ++it){ + if(*it == edge){ + ic.erase(it); + break; + } + } + } + for(std::vector::iterator it = edges.end(), en = edges.begin(); it != en;){ + if(*(--it) == edge){ + edges.erase(it); + break; + } + } + 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. */ + + void ConstrainParent(Edge *parent, Node *child); + + /** 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. + */ + 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. */ + + void DeclareConstant(const FuncDecl &f); + + /** Assert a background axiom. Background axioms can be used to provide the + * theory of auxilliary functions or relations. All symbols appearing in + * background axioms are considered global, and may appear in both transformer + * and relational solutions. Semantically, a solution to the RPFP gives + * an interpretation of the unknown relations for each interpretation of the + * auxilliary symbols that is consistent with the axioms. Axioms should be + * asserted before any calls to Push. They cannot be de-asserted by Pop. */ + + void AssertAxiom(const Term &t); + +#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). + * + * 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. + * + * 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 + * + * + */ + + 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(), + 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", + based on a previously computed counterexample. */ + + Term ComputeUnderapprox(Node *root, int persist); + + /** Try to strengthen the annotation of a node by removing disjuncts. */ + void Generalize(Node *root, Node *node); + + + /** Compute disjunctive interpolant for node by case splitting */ + 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; + bad_clause(const std::string &_msg, int _i){ + msg = _msg; + i = _i; + } + }; + + struct parse_error { + std::string msg; + parse_error(const std::string &_msg){ + msg = _msg; + } + }; + + struct file_not_found { + }; + + struct bad_format { + }; + + // thrown on internal error + struct Bad { + }; + + /** 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 + + 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) {} + }; + + +#ifdef _WINDOWS + __declspec(dllexport) +#endif + void FromClauses(const std::vector &clauses); + + void FromFixpointContext(fixedpoint fp, std::vector &queries); + + void WriteSolution(std::ostream &s); + + void WriteCounterexample(std::ostream &s, Node *node); + + 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); + + /** Read the RPFP from a file (in specificed format) */ + void ReadProblemFromFile(std::string filename, FileFormat format = DualityFormat); + + /** Translate problem to Horn clause form */ + void ToClauses(std::vector &cnsts, FileFormat format = DualityFormat); + + /** Translate the RPFP to a fixed point context, with queries */ + fixedpoint ToFixedPointProblem(std::vector &queries); + + /** Nodes of the graph. */ + std::vector nodes; + + /** Edges of the graph. */ + std::vector edges; + + /** 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_1(r_11,...,r_iN(1)) U ... U T_M(r_M1,...,r_MN(M)) + */ + + Transformer Fuse(const std::vector &trs); + + /** Fuse edges so that each node is the output of at most one edge. This + transformation is solution-preserving, but changes the numbering of edges in + counterexamples. + */ + void FuseEdges(); + + void RemoveDeadNodes(); + + Term SubstParams(const std::vector &from, + const std::vector &to, const Term &t); + + Term SubstParamsNoCapture(const std::vector &from, + const std::vector &to, const Term &t); + + Term Localize(Edge *e, const Term &t); + + void EvalNodeAsConstraint(Node *p, Transformer &res); + + TermTree *GetGoalTree(Node *root); + + int EvalTruth(hash_map &memo, Edge *e, const Term &f); + + void GetLabels(Edge *e, std::vector &labels); + + // int GetLabelsRec(hash_map *memo, const Term &f, std::vector &labels, bool labpos); + + /** Compute and save the proof core for future calls to + EdgeUsedInProof. You only need to call this if you will pop + the solver before calling EdgeUsedInProof. + */ + void ComputeProofCore(); + + int CumulativeDecisions(); + + solver &slvr(){ + return *ls->slvr; + } + + protected: + + void ClearProofCore(){ + if(proof_core) + delete proof_core; + proof_core = 0; + } + + Term SuffixVariable(const Term &t, int n); + + Term HideVariable(const Term &t, int n); + + void RedVars(Node *node, Term &b, std::vector &v); + + Term RedDualRela(Edge *e, std::vector &args, int idx); + + Term LocalizeRec(Edge *e, hash_map &memo, const Term &t); + + void SetEdgeMaps(Edge *e); + + Term ReducedDualEdge(Edge *e); + + TermTree *ToTermTree(Node *root, Node *skip_descendant = 0); + + TermTree *ToGoalTree(Node *root); + + void CollapseTermTreeRec(TermTree *root, TermTree *node); + + TermTree *CollapseTermTree(TermTree *node); + + void DecodeTree(Node *root, TermTree *interp, int persist); + + Term GetUpperBound(Node *n); + + TermTree *AddUpperBound(Node *root, TermTree *t); + +#if 0 + void WriteInterps(System.IO.StreamWriter f, TermTree t); +#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, + const Term &t, + hash_map &pmap, + std::vector &res, + std::vector &nodes); + + Term RemoveLabelsRec(hash_map &memo, const Term &t, std::vector &lbls); + + Term RemoveLabels(const Term &t, std::vector &lbls); + + Term GetAnnotation(Node *n); + + + Term GetUnderapprox(Node *n); + + Term UnderapproxFlag(Node *n); + + hash_map underapprox_flag_rev; + + Node *UnderapproxFlagRev(const Term &flag); + + Term ProjectFormula(std::vector &keep_vec, const Term &f); + + int SubtermTruth(hash_map &memo, const Term &); + + void ImplicantRed(hash_map &memo, const Term &f, std::vector &lits, + hash_set *done, bool truth, hash_set &dont_cares); + + void Implicant(hash_map &memo, const Term &f, std::vector &lits, hash_set &dont_cares); + + Term UnderapproxFormula(const Term &f, hash_set &dont_cares); + + void ImplicantFullRed(hash_map &memo, const Term &f, std::vector &lits, + hash_set &done, hash_set &dont_cares, bool extensional = true); + + public: + Term UnderapproxFullFormula(const Term &f, bool extensional = true); + + protected: + Term ToRuleRec(Edge *e, hash_map &memo, const Term &t, std::vector &quants); + + hash_map resolve_ite_memo; + + Term ResolveIte(hash_map &memo, const Term &t, std::vector &lits, + hash_set *done, hash_set &dont_cares); + + struct ArrayValue { + bool defined; + std::map entries; + expr def_val; + }; + + void EvalArrayTerm(const Term &t, ArrayValue &res); + + Term EvalArrayEquality(const Term &f); + + Term ModelValueAsConstraint(const Term &t); + + void GetLabelsRec(hash_map &memo, const Term &f, std::vector &labels, + hash_set *done, bool truth); + + Term SubstBoundRec(hash_map > &memo, hash_map &subst, int level, const Term &t); + + Term SubstBound(hash_map &subst, const Term &t); + + void ConstrainEdgeLocalized(Edge *e, const Term &t); + + void GreedyReduce(solver &s, std::vector &conjuncts); + + void NegateLits(std::vector &lits); + + expr SimplifyOr(std::vector &lits); + + expr SimplifyAnd(std::vector &lits); + + void SetAnnotation(Node *root, const expr &t); + + void AddEdgeToSolver(Edge *edge); + + void AddEdgeToSolver(implicant_solver &aux_solver, Edge *edge); + + void AddToProofCore(hash_set &core); + + 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); + + bool IsVar(const expr &t); + + void GetVarsRec(hash_set &memo, const expr &cnst, std::vector &vars); + + 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); + + expr GetRel(Edge *edge, int child_idx); + + void GetDefs(const expr &cnst, hash_map &defs); + + void GetDefsRec(const expr &cnst, hash_map &defs); + + void AddParamsToNode(Node *node, const std::vector ¶ms); + + 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); + + 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, + TermTree *&interpolants, + model &_model, + TermTree *goals = 0, + bool weak = false); + + virtual bool proof_core_contains(const expr &e); + + }; + + + /** RPFP solver base class. */ + + class Solver { + + public: + + class Counterexample { + private: + RPFP *tree; + RPFP::Node *root; + public: + Counterexample(){ + tree = 0; + root = 0; + } + Counterexample(RPFP *_tree, RPFP::Node *_root){ + tree = _tree; + root = _root; + } + ~Counterexample(){ + if(tree) delete tree; + } + void swap(Counterexample &other){ + std::swap(tree,other.tree); + std::swap(root,other.root); + } + void set(RPFP *_tree, RPFP::Node *_root){ + if(tree) delete tree; + tree = _tree; + root = _root; + } + void clear(){ + if(tree) delete tree; + tree = 0; + } + RPFP *get_tree() const {return tree;} + RPFP::Node *get_root() const {return root;} + private: + 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. */ + + virtual void LearnFrom(Solver *old_solver) = 0; + + virtual ~Solver(){} + + static Solver *Create(const std::string &solver_class, RPFP *rpfp); + + /** This can be called asynchrnously to cause Solve to throw a + Canceled exception at some time in the future. + */ + virtual void Cancel() = 0; + + /** Object thrown on cancellation */ + struct Canceled {}; + + /** Object thrown on incompleteness */ + struct Incompleteness {}; + }; +} + + +// Allow to hash on nodes and edges in deterministic way + +namespace hash_space { + template <> + class hash { + public: + size_t operator()(const Duality::RPFP::Node *p) const { + return p->number; + } + }; +} + +namespace hash_space { + template <> + class hash { + public: + size_t operator()(const Duality::RPFP::Edge *p) const { + return p->number; + } + }; +} + +// allow to walk sets of nodes without address dependency + +namespace std { + template <> + class less { + public: + bool operator()(Duality::RPFP::Node * const &s, Duality::RPFP::Node * const &t) const { + return s->number < t->number; // s.raw()->get_id() < t.raw()->get_id(); + } + }; +} + +// #define LIMIT_STACK_WEIGHT 5 + + +namespace Duality { + /** Caching version of RPFP. Instead of asserting constraints, returns assumption literals */ + + class RPFP_caching : public RPFP { + public: + + /** appends assumption literals for edge to lits. if with_children is true, + 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); + + /** Get the clone of a node */ + Node *GetNodeClone(Node *other_node); + + /** Get the clone of an edge */ + Edge *GetEdgeClone(Edge *other_edge); + + /** Try to strengthen the parent of an edge */ + void GeneralizeCache(Edge *edge); + + /** Try to propagate some facts from children to parents of edge. + Return true if success. */ + bool PropagateCache(Edge *edge); + + /** Construct a caching RPFP using a LogicSolver */ + RPFP_caching(LogicSolver *_ls) : RPFP(_ls) {} + + /** Constraint an edge by its child's annotation. Return + assumption lits. */ + void ConstrainParentCache(Edge *parent, Node *child, std::vector &lits); + +#ifdef LIMIT_STACK_WEIGHT + virtual void AssertEdge(Edge *e, int persist = 0, bool with_children = false, bool underapprox = false); +#endif + + virtual ~RPFP_caching(){} + + protected: + hash_map AssumptionLits; + hash_map NodeCloneMap; + hash_map EdgeCloneMap; + std::vector alit_stack; + std::vector alit_stack_sizes; + + // to let us use one solver per edge + struct edge_solver { + hash_map AssumptionLits; + uptr slvr; + }; + hash_map edge_solvers; + +#ifdef LIMIT_STACK_WEIGHT + struct weight_counter { + int val; + weight_counter(){val = 0;} + void swap(weight_counter &other){ + std::swap(val,other.val); + } + }; + + struct big_stack_entry { + weight_counter weight_added; + std::vector new_alits; + std::vector alit_stack; + std::vector alit_stack_sizes; + }; + + std::vector new_alits; + weight_counter weight_added; + std::vector big_stack; +#endif + + + + void GetAssumptionLits(const expr &fmla, std::vector &lits, hash_map *opt_map = 0); + + void GreedyReduceCache(std::vector &assumps, std::vector &core); + + void FilterCore(std::vector &core, std::vector &full_core); + 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, + TermTree *&interpolants, + model &_model, + TermTree *goals = 0, + bool weak = false); + + virtual bool proof_core_contains(const expr &e); + + void GetTermTreeAssertionLiterals(TermTree *assumptions); + + void GetTermTreeAssertionLiteralsRec(TermTree *assumptions); + + edge_solver &SolverForEdge(Edge *edge, bool models, bool axioms); + + public: + struct scoped_solver_for_edge { + solver *orig_slvr; + RPFP_caching *rpfp; + edge_solver *es; + 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)); + rpfp->ls->slvr = es->slvr.get(); + rpfp->AssumptionLits.swap(es->AssumptionLits); + } + ~scoped_solver_for_edge(){ + rpfp->ls->slvr = orig_slvr; + rpfp->AssumptionLits.swap(es->AssumptionLits); + } + }; + + }; + +} diff --git a/src/duality/duality_rpfp.cpp b/src/duality/duality_rpfp.cpp index accbec81a..8040310ec 100755 --- a/src/duality/duality_rpfp.cpp +++ b/src/duality/duality_rpfp.cpp @@ -551,7 +551,7 @@ namespace Duality { Z3User::Term Z3User::PushQuantifier(const expr &t, const expr &body, bool is_forall){ if(t.get_quantifier_num_bound() == 1){ std::vector fmlas,free,not_free; - CollectConjuncts(body,fmlas, !is_forall); + CollectJuncts(body,fmlas, is_forall ? Or : And, false); for(unsigned i = 0; i < fmlas.size(); i++){ const expr &fmla = fmlas[i]; if(fmla.has_free(0)) @@ -564,7 +564,7 @@ namespace Duality { return SimplifyAndOr(not_free,op == And); expr q = clone_quantifier(is_forall ? Forall : Exists,t, SimplifyAndOr(free, op == And)); if(!not_free.empty()) - q = ctx.make(op,q,SimplifyAndOr(not_free, op == And)); + q = ctx.make(op,q,DeleteBound(0,1,SimplifyAndOr(not_free, op == And))); return q; } return clone_quantifier(is_forall ? Forall : Exists,t,body); @@ -579,14 +579,16 @@ namespace Duality { args[i] = CloneQuantAndSimp(t, body.arg(i), is_forall); return SimplifyAndOr(args, body.decl().get_decl_kind() == And); } - else if(body.decl().get_decl_kind() == (is_forall ? And : Or)){ // quantifier distributes + else if(body.decl().get_decl_kind() == (is_forall ? Or : And)){ // quantifier distributes return PushQuantifier(t,body,is_forall); // may distribute partially } else if(body.decl().get_decl_kind() == Not){ - return CloneQuantAndSimp(t,body.arg(0),!is_forall); + return ctx.make(Not,CloneQuantAndSimp(t,body.arg(0),!is_forall)); } } - return clone_quantifier(t,body); + if(t.get_quantifier_num_bound() == 1 && !body.has_free(0)) + return DeleteBound(0,1,body); // drop the quantifier + return clone_quantifier(is_forall ? Forall : Exists,t,body); } Z3User::Term Z3User::CloneQuantAndSimp(const expr &t, const expr &body){ @@ -2494,6 +2496,20 @@ namespace Duality { } } + void Z3User::CollectJuncts(const Term &f, std::vector &lits, decl_kind op, bool negate){ + if(f.is_app() && f.decl().get_decl_kind() == Not) + CollectJuncts(f.arg(0), lits, (op == And) ? Or : And, !negate); + else if(f.is_app() && f.decl().get_decl_kind() == op){ + int num_args = f.num_args(); + for(int i = 0; i < num_args; i++) + CollectJuncts(f.arg(i),lits,op,negate); + } + else { + expr junct = negate ? Negate(f) : f; + lits.push_back(junct); + } + } + struct TermLt { bool operator()(const expr &x, const expr &y){ unsigned xid = x.get_id(); @@ -3444,6 +3460,46 @@ namespace Duality { return SubstBoundRec(memo, subst, 0, t); } + // Eliminate the deBruijn indices from level to level+num-1 + Z3User::Term Z3User::DeleteBoundRec(hash_map > &memo, int level, int num, const Term &t) + { + std::pair foo(t,expr(ctx)); + std::pair::iterator, bool> bar = memo[level].insert(foo); + Term &res = bar.first->second; + if(!bar.second) return res; + if (t.is_app()) + { + func_decl f = t.decl(); + std::vector args; + int nargs = t.num_args(); + for(int i = 0; i < nargs; i++) + args.push_back(DeleteBoundRec(memo, level, num, t.arg(i))); + res = f(args.size(),&args[0]); + } + else if (t.is_quantifier()){ + int bound = t.get_quantifier_num_bound(); + std::vector pats; + t.get_patterns(pats); + for(unsigned i = 0; i < pats.size(); i++) + pats[i] = DeleteBoundRec(memo, level + bound, num, pats[i]); + res = clone_quantifier(t, DeleteBoundRec(memo, level + bound, num, t.body()), pats); + } + else if (t.is_var()) { + int idx = t.get_index_value(); + if(idx >= level){ + res = ctx.make_var(idx-num,t.get_sort()); + } + else res = t; + } + else res = t; + return res; + } + + Z3User::Term Z3User::DeleteBound(int level, int num, const Term &t){ + hash_map > memo; + return DeleteBoundRec(memo, level, num, t); + } + int Z3User::MaxIndex(hash_map &memo, const Term &t) { std::pair foo(t,-1); diff --git a/src/duality/duality_wrapper.cpp b/src/duality/duality_wrapper.cpp index d5c9a9575..604192ebc 100755 --- a/src/duality/duality_wrapper.cpp +++ b/src/duality/duality_wrapper.cpp @@ -340,6 +340,12 @@ expr context::make_quant(decl_kind op, const std::vector &_sorts, const st params p; return simplify(p); } + + expr context::make_var(int idx, const sort &s){ + ::sort * a = to_sort(s.raw()); + return cook(m().mk_var(idx,a)); + } + expr expr::qe_lite() const { ::qe_lite qe(m()); diff --git a/src/duality/duality_wrapper.h b/src/duality/duality_wrapper.h index a85b3981d..3ee7c3882 100755 --- a/src/duality/duality_wrapper.h +++ b/src/duality/duality_wrapper.h @@ -1,1482 +1,1487 @@ -/*++ -Copyright (c) 2012 Microsoft Corporation - -Module Name: - - duality_wrapper.h - -Abstract: - - wrap various Z3 classes in the style expected by duality - -Author: - - Ken McMillan (kenmcmil) - -Revision History: - - ---*/ -#ifndef __DUALITY_WRAPPER_H_ -#define __DUALITY_WRAPPER_H_ - -#include -#include -#include -#include -#include -#include -#include -#include"version.h" -#include - -#include "iz3hash.h" -#include "model.h" -#include "solver.h" - -#include"well_sorted.h" -#include"arith_decl_plugin.h" -#include"bv_decl_plugin.h" -#include"datatype_decl_plugin.h" -#include"array_decl_plugin.h" -#include"ast_translation.h" -#include"ast_pp.h" -#include"ast_ll_pp.h" -#include"ast_smt_pp.h" -#include"ast_smt2_pp.h" -#include"th_rewriter.h" -#include"var_subst.h" -#include"expr_substitution.h" -#include"pp.h" -#include"scoped_ctrl_c.h" -#include"cancel_eh.h" -#include"scoped_timer.h" -#include"scoped_proof.h" - -namespace Duality { - - class exception; - class config; - class context; - class symbol; - class params; - class ast; - class sort; - class func_decl; - class expr; - class solver; - class goal; - class tactic; - class probe; - class model; - class func_interp; - class func_entry; - class statistics; - class apply_result; - class fixedpoint; - class literals; - - /** - Duality global configuration object. - */ - - class config { - params_ref m_params; - config & operator=(config const & s); - public: - config(config const & s) : m_params(s.m_params) {} - config(const params_ref &_params) : m_params(_params) {} - config() { } // TODO: create a new params object here - ~config() { } - void set(char const * param, char const * value) { m_params.set_str(param,value); } - void set(char const * param, bool value) { m_params.set_bool(param,value); } - void set(char const * param, int value) { m_params.set_uint(param,value); } - params_ref &get() {return m_params;} - const params_ref &get() const {return m_params;} - }; - - enum decl_kind { - True, - False, - And, - Or, - Not, - Iff, - Ite, - Equal, - Implies, - Distinct, - Xor, - Oeq, - Interp, - Leq, - Geq, - Lt, - Gt, - Plus, - Sub, - Uminus, - Times, - Div, - Idiv, - Rem, - Mod, - Power, - ToReal, - ToInt, - IsInt, - Select, - Store, - ConstArray, - ArrayDefault, - ArrayMap, - SetUnion, - SetIntersect, - SetDifference, - SetComplement, - SetSubSet, - AsArray, - Numeral, - Forall, - Exists, - Variable, - Uninterpreted, - OtherBasic, - OtherArith, - OtherArray, - Other - }; - - enum sort_kind {BoolSort,IntSort,RealSort,ArraySort,UninterpretedSort,UnknownSort}; - - /** - A context has an ast manager global configuration options, etc. - */ - - class context { - protected: - ast_manager &mgr; - config m_config; - - family_id m_basic_fid; - family_id m_array_fid; - family_id m_arith_fid; - family_id m_bv_fid; - family_id m_dt_fid; - family_id m_datalog_fid; - arith_util m_arith_util; - - public: - context(ast_manager &_manager, const config &_config) : mgr(_manager), m_config(_config), m_arith_util(_manager) { - m_basic_fid = m().get_basic_family_id(); - m_arith_fid = m().mk_family_id("arith"); - m_bv_fid = m().mk_family_id("bv"); - m_array_fid = m().mk_family_id("array"); - m_dt_fid = m().mk_family_id("datatype"); - 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); } - void set(char const * param, bool value) { m_config.set(param,value); } - void set(char const * param, int value) { m_config.set(param,value); } - config &get_config() {return m_config;} - - 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); - func_decl function(char const * name, sort const & d1, sort const & d2, sort const & range); - func_decl function(char const * name, sort const & d1, sort const & d2, sort const & d3, sort const & range); - func_decl function(char const * name, sort const & d1, sort const & d2, sort const & d3, sort const & d4, sort const & range); - func_decl function(char const * name, sort const & d1, sort const & d2, sort const & d3, sort const & d4, sort const & d5, sort const & range); - func_decl fresh_func_decl(char const * name, const std::vector &domain, sort const & range); - func_decl fresh_func_decl(char const * name, sort const & range); - - expr constant(symbol const & name, sort const & s); - expr constant(char const * name, sort const & s); - expr constant(const std::string &name, sort const & s); - expr bool_const(char const * name); - 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); - expr make(decl_kind op, int n, ::expr **args); - expr make(decl_kind op, const std::vector &args); - expr make(decl_kind op); - expr make(decl_kind op, const expr &arg0); - expr make(decl_kind op, const expr &arg0, const expr &arg1); - expr make(decl_kind op, const expr &arg0, const expr &arg1, const expr &arg2); - - expr make_quant(decl_kind op, const std::vector &bvs, const expr &body); - expr make_quant(decl_kind op, const std::vector &_sorts, const std::vector &_names, const expr &body); - - - decl_kind get_decl_kind(const func_decl &t); - - sort_kind get_sort_kind(const sort &s); - - expr translate(const expr &e); - func_decl translate(const func_decl &); - - void print_expr(std::ostream &s, const ast &e); - - fixedpoint mk_fixedpoint(); - - expr cook(::expr *a); - std::vector cook(ptr_vector< ::expr> v); - ::expr *uncook(const expr &a); - }; - - template - class z3array { - T * m_array; - unsigned m_size; - z3array(z3array const & s); - z3array & operator=(z3array const & s); - public: - z3array(unsigned sz):m_size(sz) { m_array = new T[sz]; } - ~z3array() { delete[] m_array; } - unsigned size() const { return m_size; } - T & operator[](unsigned i) { assert(i < m_size); return m_array[i]; } - T const & operator[](unsigned i) const { assert(i < m_size); return m_array[i]; } - T const * ptr() const { return m_array; } - T * ptr() { return m_array; } - }; - - class object { - protected: - context * m_ctx; - public: - object(): m_ctx((context *)0) {} - object(context & c):m_ctx(&c) {} - 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();} - }; - - 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 & 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 { - if (m_sym.is_numerical()) { - std::ostringstream buffer; - buffer << m_sym.get_num(); - return buffer.str(); - } - else { - return m_sym.bare_str(); - } - } - friend std::ostream & operator<<(std::ostream & out, symbol const & s){ - return out << s.str(); - } - friend bool operator==(const symbol &x, const symbol &y){ - return x.m_sym == y.m_sym; - } - }; - - class params : public config {}; - - /** Wrapper around an ast pointer */ - class ast_i : public object { - protected: - ::ast *_ast; - 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; - } - bool lt(const ast_i &other) const { - return _ast < other._ast; - } - friend bool operator==(const ast_i &x, const ast_i&y){ - return x.eq(y); - } - friend bool operator!=(const ast_i &x, const ast_i&y){ - return !x.eq(y); - } - friend bool operator<(const ast_i &x, const ast_i&y){ - return x.lt(y); - } - size_t hash() const {return (size_t)_ast;} - bool null() const {return !_ast;} - }; - - /** Reference counting verison of above */ - class ast : public ast_i { - public: - 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); - _ast = other._ast; - m_ctx = other.m_ctx; - if(_ast) - m().inc_ref(_ast); - return *this; - } - - ~ast(){ - if(_ast) - m().dec_ref(_ast); - } - - void show() const; - - }; - - class sort : public ast { - public: - sort(context & c):ast(c) {} - sort(context & c, ::sort *s):ast(c, s) {} - sort(sort const & s):ast(s) {} - operator ::sort*() const { return to_sort(raw()); } - 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_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; - - - sort array_domain() const; - sort array_range() const; - }; - - - class func_decl : public ast { - public: - func_decl() : ast() {} - func_decl(context & c):ast(c) {} - func_decl(context & c, ::func_decl *n):ast(c, n) {} - 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; - symbol name() const {return symbol(ctx(),to_func_decl(raw())->get_name());} - decl_kind get_decl_kind() const; - - bool is_const() const { return arity() == 0; } - - expr operator()(unsigned n, expr const * args) const; - expr operator()(const std::vector &args) const; - expr operator()() const; - expr operator()(expr const & a) const; - expr operator()(int a) const; - expr operator()(expr const & a1, expr const & a2) const; - expr operator()(expr const & a1, int a2) const; - expr operator()(int a1, expr const & a2) const; - expr operator()(expr const & a1, expr const & a2, expr const & a3) const; - 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){ - return func_decl(ctx(),to_func_decl(to_func_decl(raw())->get_parameters()[idx].get_ast())); - } - - }; - - class expr : public ast { - public: - expr() : ast() {} - expr(context & c):ast(c) {} - 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();} - - sort get_sort() const { return sort(ctx(),m().get_sort(to_expr(raw()))); } - - bool is_bool() const { return get_sort().is_bool(); } - bool is_int() const { return get_sort().is_int(); } - bool is_real() const { return get_sort().is_real(); } - bool is_arith() const { return get_sort().is_arith(); } - bool is_array() const { return get_sort().is_array(); } - 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_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_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 { - used_vars proc; - proc.process(to_expr(raw())); - return proc.contains(idx); - } - - // 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());} - unsigned num_args() const { - ast_kind dk = raw()->get_kind(); - switch(dk){ - case AST_APP: - return to_app(raw())->get_num_args(); - case AST_QUANTIFIER: - return 1; - case AST_VAR: - return 0; - default:; - } - SASSERT(0); - return 0; - } - expr arg(unsigned i) const { - ast_kind dk = raw()->get_kind(); - switch(dk){ - case AST_APP: - return ctx().cook(to_app(raw())->get_arg(i)); - case AST_QUANTIFIER: - return ctx().cook(to_quantifier(raw())->get_expr()); - default:; - } - 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)); - } - - friend expr operator==(expr const & a, expr const & b) { - return expr(a.ctx(),a.m().mk_app(a.m().get_basic_family_id(),OP_EQ,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_DISTINCT,a,b)); - } - - friend expr operator+(expr const & a, expr const & b) { - return a.ctx().make(Plus,a,b); // expr(a.ctx(),a.m().mk_app(a.m().get_basic_family_id(),OP_ADD,a,b)); - } - - 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)); - } - - friend expr operator-(expr const & a, expr const & b) { - return a.ctx().make(Sub,a,b); // expr(a.ctx(),a.m().mk_app(a.ctx().m_arith_fid,OP_SUB,a,b)); - } - - 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; - - 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 std::ostream & operator<<(std::ostream & out, expr const & m){ - m.ctx().print_expr(out,m); - return out; - } - - void get_patterns(std::vector &pats) const ; - - unsigned get_quantifier_num_bound() const { - return to_quantifier(raw())->get_num_decls(); - } - - 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 { - return sort(ctx(),to_quantifier(raw())->get_decl_sort(n)); - } - - 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 exists(const std::vector &quants, const expr &body); - - }; - - - typedef ::decl_kind pfrule; - - class proof : public ast { - public: - proof(context & c):ast(c) {} - proof(context & c, ::proof *s):ast(c, s) {} - proof(proof const & s):ast(s) {} - operator ::proof*() const { return to_app(raw()); } - proof & operator=(proof const & s) { return static_cast(ast::operator=(s)); } - - pfrule rule() const { - ::func_decl *d = to_app(raw())->get_decl(); - return d->get_decl_kind(); - } - - 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); - }; - -#if 0 - -#if Z3_MAJOR_VERSION > 4 || Z3_MAJOR_VERSION == 4 && Z3_MINOR_VERSION >= 3 - template - class ast_vector_tpl : public object { - Z3_ast_vector m_vector; - void init(Z3_ast_vector v) { Z3_ast_vector_inc_ref(ctx(), v); m_vector = v; } - public: - ast_vector_tpl(context & c):object(c) { init(Z3_mk_ast_vector(c)); } - ast_vector_tpl(context & c, Z3_ast_vector v):object(c) { init(v); } - ast_vector_tpl(ast_vector_tpl const & s):object(s), m_vector(s.m_vector) { Z3_ast_vector_inc_ref(ctx(), m_vector); } - ~ast_vector_tpl() { /* Z3_ast_vector_dec_ref(ctx(), m_vector); */ } - operator Z3_ast_vector() const { return m_vector; } - unsigned size() const { return Z3_ast_vector_size(ctx(), m_vector); } - T operator[](unsigned i) const { Z3_ast r = Z3_ast_vector_get(ctx(), m_vector, i); check_error(); return cast_ast()(ctx(), r); } - void push_back(T const & e) { Z3_ast_vector_push(ctx(), m_vector, e); check_error(); } - void resize(unsigned sz) { Z3_ast_vector_resize(ctx(), m_vector, sz); check_error(); } - 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); - // Z3_ast_vector_dec_ref(ctx(), m_vector); - m_ctx = s.m_ctx; - m_vector = s.m_vector; - 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; } - }; - - typedef ast_vector_tpl ast_vector; - typedef ast_vector_tpl expr_vector; - typedef ast_vector_tpl sort_vector; - typedef ast_vector_tpl func_decl_vector; - -#endif - -#endif - - class func_interp : public object { - ::func_interp * m_interp; - void init(::func_interp * e) { - m_interp = e; - } - public: - func_interp(context & c, ::func_interp * e):object(c) { init(e); } - func_interp(func_interp const & s):object(s) { init(s.m_interp); } - ~func_interp() { } - operator ::func_interp *() const { return m_interp; } - func_interp & operator=(func_interp const & s) { - m_ctx = s.m_ctx; - m_interp = s.m_interp; - return *this; - } - unsigned num_entries() const { return m_interp->num_entries(); } - expr get_arg(unsigned ent, unsigned arg) const { - return expr(ctx(),m_interp->get_entry(ent)->get_arg(arg)); - } - expr get_value(unsigned ent) const { - return expr(ctx(),m_interp->get_entry(ent)->get_result()); - } - expr else_value() const { - return expr(ctx(),m_interp->get_else()); - } - }; - - - - class model : public object { - model_ref m_model; - void init(::model *m) { - 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() { } - 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_model = s.m_model.get(); - return *this; - } - model & operator=(::model *s) { - m_model = s; - return *this; - } - 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; - - unsigned num_consts() const {return m_model.get()->get_num_constants();} - unsigned num_funcs() const {return m_model.get()->get_num_functions();} - func_decl get_const_decl(unsigned i) const {return func_decl(ctx(),m_model.get()->get_constant(i));} - func_decl get_func_decl(unsigned i) const {return func_decl(ctx(),m_model.get()->get_function(i));} - unsigned size() const; - func_decl operator[](unsigned i) const; - - 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; } -#endif - }; - -#if 0 - class stats : public object { - Z3_stats m_stats; - void init(Z3_stats e) { - m_stats = e; - Z3_stats_inc_ref(ctx(), m_stats); - } - public: - stats(context & c):object(c), m_stats(0) {} - stats(context & c, Z3_stats e):object(c) { init(e); } - stats(stats const & s):object(s) { init(s.m_stats); } - ~stats() { if (m_stats) Z3_stats_dec_ref(ctx(), m_stats); } - operator Z3_stats() const { return m_stats; } - 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_stats = s.m_stats; - 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; } - bool is_uint(unsigned i) const { Z3_bool r = Z3_stats_is_uint(ctx(), m_stats, i); check_error(); return r != 0; } - bool is_double(unsigned i) const { Z3_bool r = Z3_stats_is_double(ctx(), m_stats, i); check_error(); return r != 0; } - unsigned uint_value(unsigned i) const { unsigned r = Z3_stats_get_uint_value(ctx(), m_stats, i); check_error(); return r; } - double double_value(unsigned i) const { double r = Z3_stats_get_double_value(ctx(), m_stats, i); check_error(); return r; } - friend std::ostream & operator<<(std::ostream & out, stats const & s) { out << Z3_stats_to_string(s.ctx(), s); return out; } - }; -#endif - - enum check_result { - unsat, sat, unknown - }; - - class fixedpoint : public object { - - public: - void get_rules(std::vector &rules); - void get_assertions(std::vector &rules); - void register_relation(const func_decl &rela); - void add_rule(const expr &clause, const symbol &name); - void assert_cnst(const expr &cnst); - }; - - inline std::ostream & operator<<(std::ostream & out, check_result r) { - if (r == unsat) out << "unsat"; - else if (r == sat) out << "sat"; - else out << "unknown"; - return out; - } - - inline check_result to_check_result(lbool l) { - if (l == l_true) return sat; - else if (l == l_false) return unsat; - return unknown; - } - - class solver : public object { - protected: - ::solver *m_solver; - model the_model; - 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() { - 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(){ - 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); - 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); - 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); - checkpoint(); - std::vector< ::expr *> _assumptions(n); - for (unsigned i = 0; i < n; i++) { - _assumptions[i] = to_expr(assumptions[i]); - } - the_model = 0; - lbool r = m_solver->check_sat(n,&_assumptions[0]); - - if(core_size && core){ - ptr_vector< ::expr> _core; - m_solver->get_unsat_core(_core); - *core_size = _core.size(); - for(unsigned i = 0; i < *core_size; i++) - core[i] = expr(ctx(),_core[i]); - } - - model_ref m; - m_solver->get_model(m); - the_model = m.get(); - - return to_check_result(r); - } -#if 0 - 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); - } -#endif - model get_model() const { return model(ctx(), the_model); } - // std::string reason_unknown() const { Z3_string r = Z3_solver_get_reason_unknown(ctx(), m_solver); check_error(); return r; } - // stats statistics() const { Z3_stats r = Z3_solver_get_statistics(ctx(), m_solver); check_error(); return stats(ctx(), r); } -#if 0 - expr_vector unsat_core() const { Z3_ast_vector r = Z3_solver_get_unsat_core(ctx(), m_solver); check_error(); return expr_vector(ctx(), r); } - expr_vector assertions() const { Z3_ast_vector r = Z3_solver_get_assertions(ctx(), m_solver); check_error(); return expr_vector(ctx(), r); } -#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(); - - void cancel(){ - scoped_proof_mode spm(m(),m_mode); - canceled = true; - if(m_solver) - m_solver->cancel(); - } - - 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(); - - proof get_proof(){ - scoped_proof_mode spm(m(),m_mode); - return proof(ctx(),m_solver->get_proof()); - } - - bool extensional_array_theory() {return extensional;} - }; - -#if 0 - class goal : public object { - Z3_goal m_goal; - void init(Z3_goal s) { - m_goal = s; - Z3_goal_inc_ref(ctx(), s); - } - public: - goal(context & c, bool models=true, bool unsat_cores=false, bool proofs=false):object(c) { init(Z3_mk_goal(c, models, unsat_cores, proofs)); } - goal(context & c, Z3_goal s):object(c) { init(s); } - goal(goal const & s):object(s) { init(s.m_goal); } - ~goal() { Z3_goal_dec_ref(ctx(), m_goal); } - operator Z3_goal() const { return m_goal; } - 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_goal = s.m_goal; - 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); } - 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; } - friend std::ostream & operator<<(std::ostream & out, goal const & g) { out << Z3_goal_to_string(g.ctx(), g); return out; } - }; - - class apply_result : public object { - Z3_apply_result m_apply_result; - void init(Z3_apply_result s) { - m_apply_result = s; - Z3_apply_result_inc_ref(ctx(), s); - } - public: - apply_result(context & c, Z3_apply_result s):object(c) { init(s); } - apply_result(apply_result const & s):object(s) { init(s.m_apply_result); } - ~apply_result() { Z3_apply_result_dec_ref(ctx(), m_apply_result); } - operator Z3_apply_result() const { return m_apply_result; } - 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_apply_result = s.m_apply_result; - 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); - Z3_model new_m = Z3_apply_result_convert_model(ctx(), m_apply_result, i, m); - check_error(); - return model(ctx(), new_m); - } - friend std::ostream & operator<<(std::ostream & out, apply_result const & r) { out << Z3_apply_result_to_string(r.ctx(), r); return out; } - }; - - class tactic : public object { - Z3_tactic m_tactic; - void init(Z3_tactic s) { - m_tactic = s; - Z3_tactic_inc_ref(ctx(), s); - } - public: - tactic(context & c, char const * name):object(c) { Z3_tactic r = Z3_mk_tactic(c, name); check_error(); init(r); } - tactic(context & c, Z3_tactic s):object(c) { init(s); } - tactic(tactic const & s):object(s) { init(s.m_tactic); } - ~tactic() { Z3_tactic_dec_ref(ctx(), m_tactic); } - operator Z3_tactic() const { return m_tactic; } - 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_tactic = s.m_tactic; - 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 { - check_context(*this, g); - 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); - } - std::string help() const { char const * r = Z3_tactic_get_help(ctx(), m_tactic); check_error(); return r; } - friend tactic operator&(tactic const & t1, tactic const & t2) { - check_context(t1, t2); - Z3_tactic r = Z3_tactic_and_then(t1.ctx(), t1, t2); - t1.check_error(); - return tactic(t1.ctx(), r); - } - friend tactic operator|(tactic const & t1, tactic const & t2) { - check_context(t1, t2); - Z3_tactic r = Z3_tactic_or_else(t1.ctx(), t1, t2); - t1.check_error(); - return tactic(t1.ctx(), r); - } - friend tactic repeat(tactic const & t, unsigned max=UINT_MAX) { - Z3_tactic r = Z3_tactic_repeat(t.ctx(), t, max); - t.check_error(); - return tactic(t.ctx(), r); - } - friend tactic with(tactic const & t, params const & p) { - Z3_tactic r = Z3_tactic_using_params(t.ctx(), t, p); - t.check_error(); - return tactic(t.ctx(), r); - } - friend tactic try_for(tactic const & t, unsigned ms) { - Z3_tactic r = Z3_tactic_try_for(t.ctx(), t, ms); - t.check_error(); - return tactic(t.ctx(), r); - } - }; - - class probe : public object { - Z3_probe m_probe; - void init(Z3_probe s) { - m_probe = s; - Z3_probe_inc_ref(ctx(), s); - } - public: - probe(context & c, char const * name):object(c) { Z3_probe r = Z3_mk_probe(c, name); check_error(); init(r); } - probe(context & c, double val):object(c) { Z3_probe r = Z3_probe_const(c, val); check_error(); init(r); } - probe(context & c, Z3_probe s):object(c) { init(s); } - probe(probe const & s):object(s) { init(s.m_probe); } - ~probe() { Z3_probe_dec_ref(ctx(), m_probe); } - operator Z3_probe() const { return m_probe; } - 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_probe = s.m_probe; - 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, 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, 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, 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, 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, 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_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); - } - }; - - inline tactic fail_if(probe const & p) { - Z3_tactic r = Z3_tactic_fail_if(p.ctx(), p); - p.check_error(); - return tactic(p.ctx(), r); - } - inline tactic when(probe const & p, tactic const & t) { - check_context(p, t); - Z3_tactic r = Z3_tactic_when(t.ctx(), p, t); - t.check_error(); - return tactic(t.ctx(), r); - } - inline tactic cond(probe const & p, tactic const & t1, tactic const & t2) { - check_context(p, t1); check_context(p, t2); - Z3_tactic r = Z3_tactic_cond(t1.ctx(), p, t1, t2); - t1.check_error(); - return tactic(t1.ctx(), r); - } - -#endif - - inline expr context::bool_val(bool b){return b ? make(True) : make(False);} - - inline symbol context::str_symbol(char const * s) { ::symbol r = ::symbol(s); return symbol(*this, r); } - 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); - return sort(*this, s); - } - inline sort context::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); - return sort(*this, s); - } - inline sort context::array_sort(sort d, sort r) { - parameter params[2] = { parameter(d), parameter(to_sort(r)) }; - ::sort * s = m().mk_sort(m_array_fid, ARRAY_SORT, 2, params); - return sort(*this, s); - } - - - inline func_decl context::function(symbol const & name, unsigned arity, sort const * domain, sort const & range) { - std::vector< ::sort *> sv(arity); - for(unsigned i = 0; i < arity; i++) - sv[i] = domain[i]; - ::func_decl* d = m().mk_func_decl(name,arity,&sv[0],range); - return func_decl(*this,d); - } - - 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); - } - - 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); - } - - inline func_decl context::function(char const * name, sort const & d1, sort const & d2, sort const & d3, sort const & range) { - sort args[3] = { d1, d2, d3 }; - return function(name, 3, args, range); - } - - inline func_decl context::function(char const * name, sort const & d1, sort const & d2, sort const & d3, sort const & d4, sort const & range) { - 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); - } - - - 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); - } - 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()); } - inline expr context::int_const(char const * name) { return constant(name, int_sort()); } - inline expr context::real_const(char const * name) { return constant(name, real_sort()); } - inline expr context::bv_const(char const * name, unsigned sz) { return constant(name, bv_sort(sz)); } - - inline expr func_decl::operator()(const std::vector &args) const { - return operator()(args.size(),&args[0]); - } - inline expr func_decl::operator()() const { - return operator()(0,0); - } - inline expr func_decl::operator()(expr const & a) const { - return operator()(1,&a); - } - inline expr func_decl::operator()(expr const & a1, expr const & a2) const { - expr args[2] = {a1,a2}; - return operator()(2,args); - } - inline expr func_decl::operator()(expr const & a1, expr const & a2, expr const & a3) const { - expr args[3] = {a1,a2,a3}; - return operator()(3,args); - } - inline expr func_decl::operator()(expr const & a1, expr const & a2, expr const & a3, expr const & a4) const { - expr args[4] = {a1,a2,a3,a4}; - return operator()(4,args); - } - inline expr func_decl::operator()(expr const & a1, expr const & a2, expr const & a3, expr const & a4, expr const & a5) const { - 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); - } - - inline expr exists(const std::vector &quants, const expr &body){ - return body.ctx().make_quant(Exists,quants,body); - } - - inline expr context::int_val(int n){ - :: sort *r = m().mk_sort(m_arith_fid, INT_SORT); - return cook(m_arith_util.mk_numeral(rational(n),r)); - } - - - class literals : public object { - }; - - class TermTree { - public: - - TermTree(expr _term){ - term = _term; - } - - TermTree(expr _term, const std::vector &_children){ - term = _term; - children = _children; - } - - inline expr getTerm(){return term;} - - inline std::vector &getTerms(){return terms;} - - inline std::vector &getChildren(){ - return children; - } - - inline int number(int from){ - for(unsigned i = 0; i < children.size(); i++) - from = children[i]->number(from); - num = from; - return from + 1; - } - - inline int getNumber(){ - return num; - } - - inline void setTerm(expr t){term = t;} - - inline void addTerm(expr t){terms.push_back(t);} - - inline void setChildren(const std::vector & _children){ - children = _children; - } - - inline void setNumber(int _num){ - num = _num; - } - - ~TermTree(){ - for(unsigned i = 0; i < children.size(); i++) - delete children[i]; - } - - private: - expr term; - std::vector terms; - std::vector children; - int num; - }; - - typedef context interpolating_context; - - class interpolating_solver : public solver { - public: - interpolating_solver(context &ctx, bool models = true) - : solver(ctx, true, models) - { - weak_mode = false; - } - - public: - lbool interpolate(const std::vector &assumptions, - std::vector &interpolants, - model &_model, - 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) { - std::vector _v(v.size()); - for(unsigned i = 0; i < v.size(); i++) - _v[i] = cook(v[i]); - return _v; - } - - inline ::expr *context::uncook(const expr &a) { - m().inc_ref(a.raw()); - return to_expr(a.raw()); - } - - inline expr context::translate(const expr &e) { - ::expr *f = to_expr(e.raw()); - if(&e.ctx().m() != &m()) // same ast manager -> no translation - throw "ast manager mismatch"; - return cook(f); - } - - inline func_decl context::translate(const func_decl &e) { - ::func_decl *f = to_func_decl(e.raw()); - if(&e.ctx().m() != &m()) // same ast manager -> no translation - throw "ast manager mismatch"; - return func_decl(*this,f); - } - - typedef double clock_t; - clock_t current_time(); - inline void output_time(std::ostream &os, clock_t time){os << time;} - - template class uptr { - public: - X *ptr; - uptr(){ptr = 0;} - void set(X *_ptr){ - if(ptr) delete ptr; - ptr = _ptr; - } - X *get(){ return ptr;} - ~uptr(){ - if(ptr) delete ptr; - } - }; - -}; - -// to make Duality::ast hashable -namespace hash_space { - template <> - class hash { - public: - size_t operator()(const Duality::ast &s) const { - return s.raw()->get_id(); - } - }; -} - - -// to make Duality::ast usable in ordered collections -namespace std { - template <> - class less { - public: - bool operator()(const Duality::ast &s, const Duality::ast &t) const { - // return s.raw() < t.raw(); - return s.raw()->get_id() < t.raw()->get_id(); - } - }; -} - -// to make Duality::ast usable in ordered collections -namespace std { - template <> - class less { - public: - bool operator()(const Duality::expr &s, const Duality::expr &t) const { - // return s.raw() < t.raw(); - return s.raw()->get_id() < t.raw()->get_id(); - } - }; -} - -// to make Duality::func_decl hashable -namespace hash_space { - template <> - class hash { - public: - size_t operator()(const Duality::func_decl &s) const { - return s.raw()->get_id(); - } - }; -} - - -// to make Duality::func_decl usable in ordered collections -namespace std { - template <> - class less { - public: - bool operator()(const Duality::func_decl &s, const Duality::func_decl &t) const { - // return s.raw() < t.raw(); - return s.raw()->get_id() < t.raw()->get_id(); - } - }; -} - -#endif - +/*++ +Copyright (c) 2012 Microsoft Corporation + +Module Name: + + duality_wrapper.h + +Abstract: + + wrap various Z3 classes in the style expected by duality + +Author: + + Ken McMillan (kenmcmil) + +Revision History: + + +--*/ +#ifndef __DUALITY_WRAPPER_H_ +#define __DUALITY_WRAPPER_H_ + +#include +#include +#include +#include +#include +#include +#include +#include"version.h" +#include + +#include "iz3hash.h" +#include "model.h" +#include "solver.h" + +#include"well_sorted.h" +#include"arith_decl_plugin.h" +#include"bv_decl_plugin.h" +#include"datatype_decl_plugin.h" +#include"array_decl_plugin.h" +#include"ast_translation.h" +#include"ast_pp.h" +#include"ast_ll_pp.h" +#include"ast_smt_pp.h" +#include"ast_smt2_pp.h" +#include"th_rewriter.h" +#include"var_subst.h" +#include"expr_substitution.h" +#include"pp.h" +#include"scoped_ctrl_c.h" +#include"cancel_eh.h" +#include"scoped_timer.h" +#include"scoped_proof.h" + +namespace Duality { + + class exception; + class config; + class context; + class symbol; + class params; + class ast; + class sort; + class func_decl; + class expr; + class solver; + class goal; + class tactic; + class probe; + class model; + class func_interp; + class func_entry; + class statistics; + class apply_result; + class fixedpoint; + class literals; + + /** + Duality global configuration object. + */ + + class config { + params_ref m_params; + config & operator=(config const & s); + public: + config(config const & s) : m_params(s.m_params) {} + config(const params_ref &_params) : m_params(_params) {} + config() { } // TODO: create a new params object here + ~config() { } + void set(char const * param, char const * value) { m_params.set_str(param,value); } + void set(char const * param, bool value) { m_params.set_bool(param,value); } + void set(char const * param, int value) { m_params.set_uint(param,value); } + params_ref &get() {return m_params;} + const params_ref &get() const {return m_params;} + }; + + enum decl_kind { + True, + False, + And, + Or, + Not, + Iff, + Ite, + Equal, + Implies, + Distinct, + Xor, + Oeq, + Interp, + Leq, + Geq, + Lt, + Gt, + Plus, + Sub, + Uminus, + Times, + Div, + Idiv, + Rem, + Mod, + Power, + ToReal, + ToInt, + IsInt, + Select, + Store, + ConstArray, + ArrayDefault, + ArrayMap, + SetUnion, + SetIntersect, + SetDifference, + SetComplement, + SetSubSet, + AsArray, + Numeral, + Forall, + Exists, + Variable, + Uninterpreted, + OtherBasic, + OtherArith, + OtherArray, + Other + }; + + enum sort_kind {BoolSort,IntSort,RealSort,ArraySort,UninterpretedSort,UnknownSort}; + + /** + A context has an ast manager global configuration options, etc. + */ + + class context { + protected: + ast_manager &mgr; + config m_config; + + family_id m_basic_fid; + family_id m_array_fid; + family_id m_arith_fid; + family_id m_bv_fid; + family_id m_dt_fid; + family_id m_datalog_fid; + arith_util m_arith_util; + + public: + context(ast_manager &_manager, const config &_config) : mgr(_manager), m_config(_config), m_arith_util(_manager) { + m_basic_fid = m().get_basic_family_id(); + m_arith_fid = m().mk_family_id("arith"); + m_bv_fid = m().mk_family_id("bv"); + m_array_fid = m().mk_family_id("array"); + m_dt_fid = m().mk_family_id("datatype"); + 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); } + void set(char const * param, bool value) { m_config.set(param,value); } + void set(char const * param, int value) { m_config.set(param,value); } + config &get_config() {return m_config;} + + 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); + func_decl function(char const * name, sort const & d1, sort const & d2, sort const & range); + func_decl function(char const * name, sort const & d1, sort const & d2, sort const & d3, sort const & range); + func_decl function(char const * name, sort const & d1, sort const & d2, sort const & d3, sort const & d4, sort const & range); + func_decl function(char const * name, sort const & d1, sort const & d2, sort const & d3, sort const & d4, sort const & d5, sort const & range); + func_decl fresh_func_decl(char const * name, const std::vector &domain, sort const & range); + func_decl fresh_func_decl(char const * name, sort const & range); + + expr constant(symbol const & name, sort const & s); + expr constant(char const * name, sort const & s); + expr constant(const std::string &name, sort const & s); + expr bool_const(char const * name); + 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); + expr make(decl_kind op, int n, ::expr **args); + expr make(decl_kind op, const std::vector &args); + expr make(decl_kind op); + expr make(decl_kind op, const expr &arg0); + expr make(decl_kind op, const expr &arg0, const expr &arg1); + expr make(decl_kind op, const expr &arg0, const expr &arg1, const expr &arg2); + + expr make_quant(decl_kind op, const std::vector &bvs, const expr &body); + expr make_quant(decl_kind op, const std::vector &_sorts, const std::vector &_names, const expr &body); + expr make_var(int idx, const sort &s); + + decl_kind get_decl_kind(const func_decl &t); + + sort_kind get_sort_kind(const sort &s); + + expr translate(const expr &e); + func_decl translate(const func_decl &); + + void print_expr(std::ostream &s, const ast &e); + + fixedpoint mk_fixedpoint(); + + expr cook(::expr *a); + std::vector cook(ptr_vector< ::expr> v); + ::expr *uncook(const expr &a); + }; + + template + class z3array { + T * m_array; + unsigned m_size; + z3array(z3array const & s); + z3array & operator=(z3array const & s); + public: + z3array(unsigned sz):m_size(sz) { m_array = new T[sz]; } + ~z3array() { delete[] m_array; } + unsigned size() const { return m_size; } + T & operator[](unsigned i) { assert(i < m_size); return m_array[i]; } + T const & operator[](unsigned i) const { assert(i < m_size); return m_array[i]; } + T const * ptr() const { return m_array; } + T * ptr() { return m_array; } + }; + + class object { + protected: + context * m_ctx; + public: + object(): m_ctx((context *)0) {} + object(context & c):m_ctx(&c) {} + 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();} + }; + + 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 & 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 { + if (m_sym.is_numerical()) { + std::ostringstream buffer; + buffer << m_sym.get_num(); + return buffer.str(); + } + else { + return m_sym.bare_str(); + } + } + friend std::ostream & operator<<(std::ostream & out, symbol const & s){ + return out << s.str(); + } + friend bool operator==(const symbol &x, const symbol &y){ + return x.m_sym == y.m_sym; + } + }; + + class params : public config {}; + + /** Wrapper around an ast pointer */ + class ast_i : public object { + protected: + ::ast *_ast; + 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; + } + bool lt(const ast_i &other) const { + return _ast < other._ast; + } + friend bool operator==(const ast_i &x, const ast_i&y){ + return x.eq(y); + } + friend bool operator!=(const ast_i &x, const ast_i&y){ + return !x.eq(y); + } + friend bool operator<(const ast_i &x, const ast_i&y){ + return x.lt(y); + } + size_t hash() const {return (size_t)_ast;} + bool null() const {return !_ast;} + }; + + /** Reference counting verison of above */ + class ast : public ast_i { + public: + 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); + _ast = other._ast; + m_ctx = other.m_ctx; + if(_ast) + m().inc_ref(_ast); + return *this; + } + + ~ast(){ + if(_ast) + m().dec_ref(_ast); + } + + void show() const; + + }; + + class sort : public ast { + public: + sort(context & c):ast(c) {} + sort(context & c, ::sort *s):ast(c, s) {} + sort(sort const & s):ast(s) {} + operator ::sort*() const { return to_sort(raw()); } + 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_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; + + + sort array_domain() const; + sort array_range() const; + }; + + + class func_decl : public ast { + public: + func_decl() : ast() {} + func_decl(context & c):ast(c) {} + func_decl(context & c, ::func_decl *n):ast(c, n) {} + 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; + symbol name() const {return symbol(ctx(),to_func_decl(raw())->get_name());} + decl_kind get_decl_kind() const; + + bool is_const() const { return arity() == 0; } + + expr operator()(unsigned n, expr const * args) const; + expr operator()(const std::vector &args) const; + expr operator()() const; + expr operator()(expr const & a) const; + expr operator()(int a) const; + expr operator()(expr const & a1, expr const & a2) const; + expr operator()(expr const & a1, int a2) const; + expr operator()(int a1, expr const & a2) const; + expr operator()(expr const & a1, expr const & a2, expr const & a3) const; + 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){ + return func_decl(ctx(),to_func_decl(to_func_decl(raw())->get_parameters()[idx].get_ast())); + } + + }; + + class expr : public ast { + public: + expr() : ast() {} + expr(context & c):ast(c) {} + 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();} + + sort get_sort() const { return sort(ctx(),m().get_sort(to_expr(raw()))); } + + bool is_bool() const { return get_sort().is_bool(); } + bool is_int() const { return get_sort().is_int(); } + bool is_real() const { return get_sort().is_real(); } + bool is_arith() const { return get_sort().is_arith(); } + bool is_array() const { return get_sort().is_array(); } + 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_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_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 { + used_vars proc; + proc.process(to_expr(raw())); + return proc.contains(idx); + } + 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());} + unsigned num_args() const { + ast_kind dk = raw()->get_kind(); + switch(dk){ + case AST_APP: + return to_app(raw())->get_num_args(); + case AST_QUANTIFIER: + return 1; + case AST_VAR: + return 0; + default:; + } + SASSERT(0); + return 0; + } + expr arg(unsigned i) const { + ast_kind dk = raw()->get_kind(); + switch(dk){ + case AST_APP: + return ctx().cook(to_app(raw())->get_arg(i)); + case AST_QUANTIFIER: + return ctx().cook(to_quantifier(raw())->get_expr()); + default:; + } + 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)); + } + + friend expr operator==(expr const & a, expr const & b) { + return expr(a.ctx(),a.m().mk_app(a.m().get_basic_family_id(),OP_EQ,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_DISTINCT,a,b)); + } + + friend expr operator+(expr const & a, expr const & b) { + return a.ctx().make(Plus,a,b); // expr(a.ctx(),a.m().mk_app(a.m().get_basic_family_id(),OP_ADD,a,b)); + } + + 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)); + } + + friend expr operator-(expr const & a, expr const & b) { + return a.ctx().make(Sub,a,b); // expr(a.ctx(),a.m().mk_app(a.ctx().m_arith_fid,OP_SUB,a,b)); + } + + 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; + + 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 std::ostream & operator<<(std::ostream & out, expr const & m){ + m.ctx().print_expr(out,m); + return out; + } + + void get_patterns(std::vector &pats) const ; + + unsigned get_quantifier_num_bound() const { + return to_quantifier(raw())->get_num_decls(); + } + + 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 { + return sort(ctx(),to_quantifier(raw())->get_decl_sort(n)); + } + + 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 exists(const std::vector &quants, const expr &body); + + }; + + + typedef ::decl_kind pfrule; + + class proof : public ast { + public: + proof(context & c):ast(c) {} + proof(context & c, ::proof *s):ast(c, s) {} + proof(proof const & s):ast(s) {} + operator ::proof*() const { return to_app(raw()); } + proof & operator=(proof const & s) { return static_cast(ast::operator=(s)); } + + pfrule rule() const { + ::func_decl *d = to_app(raw())->get_decl(); + return d->get_decl_kind(); + } + + 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); + }; + +#if 0 + +#if Z3_MAJOR_VERSION > 4 || Z3_MAJOR_VERSION == 4 && Z3_MINOR_VERSION >= 3 + template + class ast_vector_tpl : public object { + Z3_ast_vector m_vector; + void init(Z3_ast_vector v) { Z3_ast_vector_inc_ref(ctx(), v); m_vector = v; } + public: + ast_vector_tpl(context & c):object(c) { init(Z3_mk_ast_vector(c)); } + ast_vector_tpl(context & c, Z3_ast_vector v):object(c) { init(v); } + ast_vector_tpl(ast_vector_tpl const & s):object(s), m_vector(s.m_vector) { Z3_ast_vector_inc_ref(ctx(), m_vector); } + ~ast_vector_tpl() { /* Z3_ast_vector_dec_ref(ctx(), m_vector); */ } + operator Z3_ast_vector() const { return m_vector; } + unsigned size() const { return Z3_ast_vector_size(ctx(), m_vector); } + T operator[](unsigned i) const { Z3_ast r = Z3_ast_vector_get(ctx(), m_vector, i); check_error(); return cast_ast()(ctx(), r); } + void push_back(T const & e) { Z3_ast_vector_push(ctx(), m_vector, e); check_error(); } + void resize(unsigned sz) { Z3_ast_vector_resize(ctx(), m_vector, sz); check_error(); } + 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); + // Z3_ast_vector_dec_ref(ctx(), m_vector); + m_ctx = s.m_ctx; + m_vector = s.m_vector; + 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; } + }; + + typedef ast_vector_tpl ast_vector; + typedef ast_vector_tpl expr_vector; + typedef ast_vector_tpl sort_vector; + typedef ast_vector_tpl func_decl_vector; + +#endif + +#endif + + class func_interp : public object { + ::func_interp * m_interp; + void init(::func_interp * e) { + m_interp = e; + } + public: + func_interp(context & c, ::func_interp * e):object(c) { init(e); } + func_interp(func_interp const & s):object(s) { init(s.m_interp); } + ~func_interp() { } + operator ::func_interp *() const { return m_interp; } + func_interp & operator=(func_interp const & s) { + m_ctx = s.m_ctx; + m_interp = s.m_interp; + return *this; + } + unsigned num_entries() const { return m_interp->num_entries(); } + expr get_arg(unsigned ent, unsigned arg) const { + return expr(ctx(),m_interp->get_entry(ent)->get_arg(arg)); + } + expr get_value(unsigned ent) const { + return expr(ctx(),m_interp->get_entry(ent)->get_result()); + } + expr else_value() const { + return expr(ctx(),m_interp->get_else()); + } + }; + + + + class model : public object { + model_ref m_model; + void init(::model *m) { + 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() { } + 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_model = s.m_model.get(); + return *this; + } + model & operator=(::model *s) { + m_model = s; + return *this; + } + 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; + + unsigned num_consts() const {return m_model.get()->get_num_constants();} + unsigned num_funcs() const {return m_model.get()->get_num_functions();} + func_decl get_const_decl(unsigned i) const {return func_decl(ctx(),m_model.get()->get_constant(i));} + func_decl get_func_decl(unsigned i) const {return func_decl(ctx(),m_model.get()->get_function(i));} + unsigned size() const; + func_decl operator[](unsigned i) const; + + 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; } +#endif + }; + +#if 0 + class stats : public object { + Z3_stats m_stats; + void init(Z3_stats e) { + m_stats = e; + Z3_stats_inc_ref(ctx(), m_stats); + } + public: + stats(context & c):object(c), m_stats(0) {} + stats(context & c, Z3_stats e):object(c) { init(e); } + stats(stats const & s):object(s) { init(s.m_stats); } + ~stats() { if (m_stats) Z3_stats_dec_ref(ctx(), m_stats); } + operator Z3_stats() const { return m_stats; } + 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_stats = s.m_stats; + 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; } + bool is_uint(unsigned i) const { Z3_bool r = Z3_stats_is_uint(ctx(), m_stats, i); check_error(); return r != 0; } + bool is_double(unsigned i) const { Z3_bool r = Z3_stats_is_double(ctx(), m_stats, i); check_error(); return r != 0; } + unsigned uint_value(unsigned i) const { unsigned r = Z3_stats_get_uint_value(ctx(), m_stats, i); check_error(); return r; } + double double_value(unsigned i) const { double r = Z3_stats_get_double_value(ctx(), m_stats, i); check_error(); return r; } + friend std::ostream & operator<<(std::ostream & out, stats const & s) { out << Z3_stats_to_string(s.ctx(), s); return out; } + }; +#endif + + enum check_result { + unsat, sat, unknown + }; + + class fixedpoint : public object { + + public: + void get_rules(std::vector &rules); + void get_assertions(std::vector &rules); + void register_relation(const func_decl &rela); + void add_rule(const expr &clause, const symbol &name); + void assert_cnst(const expr &cnst); + }; + + inline std::ostream & operator<<(std::ostream & out, check_result r) { + if (r == unsat) out << "unsat"; + else if (r == sat) out << "sat"; + else out << "unknown"; + return out; + } + + inline check_result to_check_result(lbool l) { + if (l == l_true) return sat; + else if (l == l_false) return unsat; + return unknown; + } + + class solver : public object { + protected: + ::solver *m_solver; + model the_model; + 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() { + 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(){ + 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); + 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); + 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); + checkpoint(); + std::vector< ::expr *> _assumptions(n); + for (unsigned i = 0; i < n; i++) { + _assumptions[i] = to_expr(assumptions[i]); + } + the_model = 0; + lbool r = m_solver->check_sat(n,&_assumptions[0]); + + if(core_size && core){ + ptr_vector< ::expr> _core; + m_solver->get_unsat_core(_core); + *core_size = _core.size(); + for(unsigned i = 0; i < *core_size; i++) + core[i] = expr(ctx(),_core[i]); + } + + model_ref m; + m_solver->get_model(m); + the_model = m.get(); + + return to_check_result(r); + } +#if 0 + 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); + } +#endif + model get_model() const { return model(ctx(), the_model); } + // std::string reason_unknown() const { Z3_string r = Z3_solver_get_reason_unknown(ctx(), m_solver); check_error(); return r; } + // stats statistics() const { Z3_stats r = Z3_solver_get_statistics(ctx(), m_solver); check_error(); return stats(ctx(), r); } +#if 0 + expr_vector unsat_core() const { Z3_ast_vector r = Z3_solver_get_unsat_core(ctx(), m_solver); check_error(); return expr_vector(ctx(), r); } + expr_vector assertions() const { Z3_ast_vector r = Z3_solver_get_assertions(ctx(), m_solver); check_error(); return expr_vector(ctx(), r); } +#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(); + + void cancel(){ + scoped_proof_mode spm(m(),m_mode); + canceled = true; + if(m_solver) + m_solver->cancel(); + } + + 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(); + + proof get_proof(){ + scoped_proof_mode spm(m(),m_mode); + return proof(ctx(),m_solver->get_proof()); + } + + bool extensional_array_theory() {return extensional;} + }; + +#if 0 + class goal : public object { + Z3_goal m_goal; + void init(Z3_goal s) { + m_goal = s; + Z3_goal_inc_ref(ctx(), s); + } + public: + goal(context & c, bool models=true, bool unsat_cores=false, bool proofs=false):object(c) { init(Z3_mk_goal(c, models, unsat_cores, proofs)); } + goal(context & c, Z3_goal s):object(c) { init(s); } + goal(goal const & s):object(s) { init(s.m_goal); } + ~goal() { Z3_goal_dec_ref(ctx(), m_goal); } + operator Z3_goal() const { return m_goal; } + 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_goal = s.m_goal; + 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); } + 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; } + friend std::ostream & operator<<(std::ostream & out, goal const & g) { out << Z3_goal_to_string(g.ctx(), g); return out; } + }; + + class apply_result : public object { + Z3_apply_result m_apply_result; + void init(Z3_apply_result s) { + m_apply_result = s; + Z3_apply_result_inc_ref(ctx(), s); + } + public: + apply_result(context & c, Z3_apply_result s):object(c) { init(s); } + apply_result(apply_result const & s):object(s) { init(s.m_apply_result); } + ~apply_result() { Z3_apply_result_dec_ref(ctx(), m_apply_result); } + operator Z3_apply_result() const { return m_apply_result; } + 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_apply_result = s.m_apply_result; + 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); + Z3_model new_m = Z3_apply_result_convert_model(ctx(), m_apply_result, i, m); + check_error(); + return model(ctx(), new_m); + } + friend std::ostream & operator<<(std::ostream & out, apply_result const & r) { out << Z3_apply_result_to_string(r.ctx(), r); return out; } + }; + + class tactic : public object { + Z3_tactic m_tactic; + void init(Z3_tactic s) { + m_tactic = s; + Z3_tactic_inc_ref(ctx(), s); + } + public: + tactic(context & c, char const * name):object(c) { Z3_tactic r = Z3_mk_tactic(c, name); check_error(); init(r); } + tactic(context & c, Z3_tactic s):object(c) { init(s); } + tactic(tactic const & s):object(s) { init(s.m_tactic); } + ~tactic() { Z3_tactic_dec_ref(ctx(), m_tactic); } + operator Z3_tactic() const { return m_tactic; } + 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_tactic = s.m_tactic; + 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 { + check_context(*this, g); + 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); + } + std::string help() const { char const * r = Z3_tactic_get_help(ctx(), m_tactic); check_error(); return r; } + friend tactic operator&(tactic const & t1, tactic const & t2) { + check_context(t1, t2); + Z3_tactic r = Z3_tactic_and_then(t1.ctx(), t1, t2); + t1.check_error(); + return tactic(t1.ctx(), r); + } + friend tactic operator|(tactic const & t1, tactic const & t2) { + check_context(t1, t2); + Z3_tactic r = Z3_tactic_or_else(t1.ctx(), t1, t2); + t1.check_error(); + return tactic(t1.ctx(), r); + } + friend tactic repeat(tactic const & t, unsigned max=UINT_MAX) { + Z3_tactic r = Z3_tactic_repeat(t.ctx(), t, max); + t.check_error(); + return tactic(t.ctx(), r); + } + friend tactic with(tactic const & t, params const & p) { + Z3_tactic r = Z3_tactic_using_params(t.ctx(), t, p); + t.check_error(); + return tactic(t.ctx(), r); + } + friend tactic try_for(tactic const & t, unsigned ms) { + Z3_tactic r = Z3_tactic_try_for(t.ctx(), t, ms); + t.check_error(); + return tactic(t.ctx(), r); + } + }; + + class probe : public object { + Z3_probe m_probe; + void init(Z3_probe s) { + m_probe = s; + Z3_probe_inc_ref(ctx(), s); + } + public: + probe(context & c, char const * name):object(c) { Z3_probe r = Z3_mk_probe(c, name); check_error(); init(r); } + probe(context & c, double val):object(c) { Z3_probe r = Z3_probe_const(c, val); check_error(); init(r); } + probe(context & c, Z3_probe s):object(c) { init(s); } + probe(probe const & s):object(s) { init(s.m_probe); } + ~probe() { Z3_probe_dec_ref(ctx(), m_probe); } + operator Z3_probe() const { return m_probe; } + 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_probe = s.m_probe; + 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, 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, 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, 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, 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, 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_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); + } + }; + + inline tactic fail_if(probe const & p) { + Z3_tactic r = Z3_tactic_fail_if(p.ctx(), p); + p.check_error(); + return tactic(p.ctx(), r); + } + inline tactic when(probe const & p, tactic const & t) { + check_context(p, t); + Z3_tactic r = Z3_tactic_when(t.ctx(), p, t); + t.check_error(); + return tactic(t.ctx(), r); + } + inline tactic cond(probe const & p, tactic const & t1, tactic const & t2) { + check_context(p, t1); check_context(p, t2); + Z3_tactic r = Z3_tactic_cond(t1.ctx(), p, t1, t2); + t1.check_error(); + return tactic(t1.ctx(), r); + } + +#endif + + inline expr context::bool_val(bool b){return b ? make(True) : make(False);} + + inline symbol context::str_symbol(char const * s) { ::symbol r = ::symbol(s); return symbol(*this, r); } + 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); + return sort(*this, s); + } + inline sort context::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); + return sort(*this, s); + } + inline sort context::array_sort(sort d, sort r) { + parameter params[2] = { parameter(d), parameter(to_sort(r)) }; + ::sort * s = m().mk_sort(m_array_fid, ARRAY_SORT, 2, params); + return sort(*this, s); + } + + + inline func_decl context::function(symbol const & name, unsigned arity, sort const * domain, sort const & range) { + std::vector< ::sort *> sv(arity); + for(unsigned i = 0; i < arity; i++) + sv[i] = domain[i]; + ::func_decl* d = m().mk_func_decl(name,arity,&sv[0],range); + return func_decl(*this,d); + } + + 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); + } + + 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); + } + + inline func_decl context::function(char const * name, sort const & d1, sort const & d2, sort const & d3, sort const & range) { + sort args[3] = { d1, d2, d3 }; + return function(name, 3, args, range); + } + + inline func_decl context::function(char const * name, sort const & d1, sort const & d2, sort const & d3, sort const & d4, sort const & range) { + 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); + } + + + 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); + } + 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()); } + inline expr context::int_const(char const * name) { return constant(name, int_sort()); } + inline expr context::real_const(char const * name) { return constant(name, real_sort()); } + inline expr context::bv_const(char const * name, unsigned sz) { return constant(name, bv_sort(sz)); } + + inline expr func_decl::operator()(const std::vector &args) const { + return operator()(args.size(),&args[0]); + } + inline expr func_decl::operator()() const { + return operator()(0,0); + } + inline expr func_decl::operator()(expr const & a) const { + return operator()(1,&a); + } + inline expr func_decl::operator()(expr const & a1, expr const & a2) const { + expr args[2] = {a1,a2}; + return operator()(2,args); + } + inline expr func_decl::operator()(expr const & a1, expr const & a2, expr const & a3) const { + expr args[3] = {a1,a2,a3}; + return operator()(3,args); + } + inline expr func_decl::operator()(expr const & a1, expr const & a2, expr const & a3, expr const & a4) const { + expr args[4] = {a1,a2,a3,a4}; + return operator()(4,args); + } + inline expr func_decl::operator()(expr const & a1, expr const & a2, expr const & a3, expr const & a4, expr const & a5) const { + 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); + } + + inline expr exists(const std::vector &quants, const expr &body){ + return body.ctx().make_quant(Exists,quants,body); + } + + inline expr context::int_val(int n){ + :: sort *r = m().mk_sort(m_arith_fid, INT_SORT); + return cook(m_arith_util.mk_numeral(rational(n),r)); + } + + + class literals : public object { + }; + + class TermTree { + public: + + TermTree(expr _term){ + term = _term; + } + + TermTree(expr _term, const std::vector &_children){ + term = _term; + children = _children; + } + + inline expr getTerm(){return term;} + + inline std::vector &getTerms(){return terms;} + + inline std::vector &getChildren(){ + return children; + } + + inline int number(int from){ + for(unsigned i = 0; i < children.size(); i++) + from = children[i]->number(from); + num = from; + return from + 1; + } + + inline int getNumber(){ + return num; + } + + inline void setTerm(expr t){term = t;} + + inline void addTerm(expr t){terms.push_back(t);} + + inline void setChildren(const std::vector & _children){ + children = _children; + } + + inline void setNumber(int _num){ + num = _num; + } + + ~TermTree(){ + for(unsigned i = 0; i < children.size(); i++) + delete children[i]; + } + + private: + expr term; + std::vector terms; + std::vector children; + int num; + }; + + typedef context interpolating_context; + + class interpolating_solver : public solver { + public: + interpolating_solver(context &ctx, bool models = true) + : solver(ctx, true, models) + { + weak_mode = false; + } + + public: + lbool interpolate(const std::vector &assumptions, + std::vector &interpolants, + model &_model, + 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) { + std::vector _v(v.size()); + for(unsigned i = 0; i < v.size(); i++) + _v[i] = cook(v[i]); + return _v; + } + + inline ::expr *context::uncook(const expr &a) { + m().inc_ref(a.raw()); + return to_expr(a.raw()); + } + + inline expr context::translate(const expr &e) { + ::expr *f = to_expr(e.raw()); + if(&e.ctx().m() != &m()) // same ast manager -> no translation + throw "ast manager mismatch"; + return cook(f); + } + + inline func_decl context::translate(const func_decl &e) { + ::func_decl *f = to_func_decl(e.raw()); + if(&e.ctx().m() != &m()) // same ast manager -> no translation + throw "ast manager mismatch"; + return func_decl(*this,f); + } + + typedef double clock_t; + clock_t current_time(); + inline void output_time(std::ostream &os, clock_t time){os << time;} + + template class uptr { + public: + X *ptr; + uptr(){ptr = 0;} + void set(X *_ptr){ + if(ptr) delete ptr; + ptr = _ptr; + } + X *get(){ return ptr;} + ~uptr(){ + if(ptr) delete ptr; + } + }; + +}; + +// to make Duality::ast hashable +namespace hash_space { + template <> + class hash { + public: + size_t operator()(const Duality::ast &s) const { + return s.raw()->get_id(); + } + }; +} + + +// to make Duality::ast usable in ordered collections +namespace std { + template <> + class less { + public: + bool operator()(const Duality::ast &s, const Duality::ast &t) const { + // return s.raw() < t.raw(); + return s.raw()->get_id() < t.raw()->get_id(); + } + }; +} + +// to make Duality::ast usable in ordered collections +namespace std { + template <> + class less { + public: + bool operator()(const Duality::expr &s, const Duality::expr &t) const { + // return s.raw() < t.raw(); + return s.raw()->get_id() < t.raw()->get_id(); + } + }; +} + +// to make Duality::func_decl hashable +namespace hash_space { + template <> + class hash { + public: + size_t operator()(const Duality::func_decl &s) const { + return s.raw()->get_id(); + } + }; +} + + +// to make Duality::func_decl usable in ordered collections +namespace std { + template <> + class less { + public: + bool operator()(const Duality::func_decl &s, const Duality::func_decl &t) const { + // return s.raw() < t.raw(); + return s.raw()->get_id() < t.raw()->get_id(); + } + }; +} + +#endif + diff --git a/src/interp/iz3proof_itp.cpp b/src/interp/iz3proof_itp.cpp index c880d60aa..5fe3338dc 100755 --- a/src/interp/iz3proof_itp.cpp +++ b/src/interp/iz3proof_itp.cpp @@ -2682,9 +2682,11 @@ class iz3proof_itp_impl : public iz3proof_itp { pf = make_refl(e); // proof that e = e prover::range erng = pv->ast_scope(e); +#if 0 if(!(erng.lo > erng.hi) && pv->ranges_intersect(pv->ast_scope(e),rng)){ return e; // this term occurs in range, so it's O.K. } +#endif hash_map::iterator it = localization_map.find(e);