From 8488ca24d28536a2b9f24ee6efbb99de40dd3f82 Mon Sep 17 00:00:00 2001 From: Ken McMillan Date: Sat, 20 Apr 2013 18:18:45 -0700 Subject: [PATCH] first commit of duality --- scripts/mk_project.py | 3 +- src/api/dotnet/Properties/AssemblyInfo.cs | 4 +- src/duality/duality.h | 792 ++++++++ src/duality/duality_hash.h | 169 ++ src/duality/duality_profiling.cpp | 201 ++ src/duality/duality_profiling.h | 38 + src/duality/duality_rpfp.cpp | 1991 +++++++++++++++++++ src/duality/duality_solver.cpp | 2200 +++++++++++++++++++++ src/duality/duality_wrapper.cpp | 523 +++++ src/duality/duality_wrapper.h | 1343 +++++++++++++ src/interp/iz3mgr.h | 1 + src/muz_qe/dl_context.cpp | 32 + src/muz_qe/dl_context.h | 12 +- src/muz_qe/dl_util.h | 1 + 14 files changed, 7305 insertions(+), 5 deletions(-) create mode 100644 src/duality/duality.h create mode 100755 src/duality/duality_hash.h create mode 100755 src/duality/duality_profiling.cpp create mode 100755 src/duality/duality_profiling.h create mode 100644 src/duality/duality_rpfp.cpp create mode 100644 src/duality/duality_solver.cpp create mode 100644 src/duality/duality_wrapper.cpp create mode 100755 src/duality/duality_wrapper.h diff --git a/scripts/mk_project.py b/scripts/mk_project.py index f23c4fe80..5682cc5d7 100644 --- a/scripts/mk_project.py +++ b/scripts/mk_project.py @@ -54,8 +54,9 @@ def init_project_def(): add_lib('fpa', ['core_tactics', 'bv_tactics', 'sat_tactic'], 'tactic/fpa') add_lib('smt_tactic', ['smt'], 'smt/tactic') add_lib('sls_tactic', ['tactic', 'normal_forms', 'core_tactics', 'bv_tactics'], 'tactic/sls') + add_lib('duality', ['smt', 'interp']) # TODO: split muz_qe inbto muz, qe. Perhaps, we should also consider breaking muz into muz and pdr. - add_lib('muz_qe', ['smt', 'sat', 'smt2parser']) + add_lib('muz_qe', ['smt', 'sat', 'smt2parser', 'duality']) add_lib('smtlogic_tactics', ['arith_tactics', 'bv_tactics', 'nlsat_tactic', 'smt_tactic', 'aig_tactic', 'muz_qe'], 'tactic/smtlogics') add_lib('ufbv_tactic', ['normal_forms', 'core_tactics', 'macros', 'smt_tactic', 'rewriter'], 'tactic/ufbv') add_lib('portfolio', ['smtlogic_tactics', 'ufbv_tactic', 'fpa', 'aig_tactic', 'muz_qe', 'sls_tactic', 'subpaving_tactic'], 'tactic/portfolio') diff --git a/src/api/dotnet/Properties/AssemblyInfo.cs b/src/api/dotnet/Properties/AssemblyInfo.cs index 517349177..1cd0fe7b8 100644 --- a/src/api/dotnet/Properties/AssemblyInfo.cs +++ b/src/api/dotnet/Properties/AssemblyInfo.cs @@ -34,6 +34,6 @@ using System.Security.Permissions; // You can specify all the values or you can default the Build and Revision Numbers // by using the '*' as shown below: // [assembly: AssemblyVersion("4.2.0.0")] -[assembly: AssemblyVersion("4.3.2.0")] -[assembly: AssemblyFileVersion("4.3.2.0")] +[assembly: AssemblyVersion("4.3.2.0")] +[assembly: AssemblyFileVersion("4.3.2.0")] diff --git a/src/duality/duality.h b/src/duality/duality.h new file mode 100644 index 000000000..c75ecfa61 --- /dev/null +++ b/src/duality/duality.h @@ -0,0 +1,792 @@ +/*++ +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 +#ifndef WIN32 +using namespace stl_ext; +#endif + +namespace Duality { + + /* Generic operations on Z3 formulas */ + + struct Z3User { + + context &ctx; + solver &slvr; + + typedef func_decl FuncDecl; + typedef expr Term; + + Z3User(context &_ctx, solver &_slvr) : ctx(_ctx), slvr(_slvr){} + + 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); + + 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 CumulativeDecisions(); + + Term SubstBoundRec(hash_map > &memo, hash_map &subst, int level, const Term &t); + + Term SubstBound(hash_map &subst, const Term &t); + + private: + + void SummarizeRec(hash_set &memo, std::vector &lits, int &ops, 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? */ + + /** 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 + ) = 0; + + /** Assert a background axiom. */ + virtual void assert_axiom(const expr &axiom) = 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 + ){} + }; + + /** 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) + { + literals _labels; + return islvr->interpolate_tree(assumptions,interpolants,_model,_labels,true); + } + + void assert_axiom(const expr &axiom){ + islvr->AssertInterpolationAxiom(axiom); + } + + 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){ + ctx = ictx = new interpolating_context(c); + slvr = islvr = new interpolating_solver(*ictx); + 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 + } + ~iZ3LogicSolver(){ + delete ictx; + delete islvr; + } + }; + +#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; + + private: + int nodeCount; + int edgeCount; + + class stack_entry + { + public: + std::list edges; + std::list nodes; + }; + + + model dualModel; + literals dualLabels; + std::list stack; + std::vector axioms; // only saved here for printing purposes + + 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), *(_ls->slvr)), dualModel(*(_ls->ctx)) + { + ls = _ls; + nodeCount = 0; + edgeCount = 0; + stack.push_back(stack_entry()); + HornClauses = false; + } + + ~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->slvr.push(); + owner->slvr.add(test); + check_result res = owner->slvr.check(); + owner->slvr.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; + } + + /** 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; + + 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; + } + + /** 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. */ + + void AssertEdge(Edge *e, int persist = 0, bool with_children = false, bool underapprox = false); + + + /** For incremental solving, asserts the negation of the upper bound associated + * with a node. + * */ + + void AssertNode(Node *n); + + /** 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); + + /** Get the constraint tree (but don't solve it) */ + + TermTree *GetConstraintTree(Node *root); + + /** 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); + + /** 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 { + }; + + /** Pop a scope (see Push). Note, you cannot pop axioms. */ + + void Pop(int num_scopes); + + /** 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. + + */ + + +#ifdef WIN32 + __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; + + Term SubstParams(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); + + private: + + + 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); + + TermTree *ToGoalTree(Node *root); + + 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); + + Term RemoveLabels(const Term &t); + + 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); + + 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); + + }; + + /** RPFP solver base class. */ + + class Solver { + + public: + + struct Counterexample { + RPFP *tree; + RPFP::Node *root; + Counterexample(){ + tree = 0; + root = 0; + } + }; + + /** 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); + + + }; +} diff --git a/src/duality/duality_hash.h b/src/duality/duality_hash.h new file mode 100755 index 000000000..f6767c037 --- /dev/null +++ b/src/duality/duality_hash.h @@ -0,0 +1,169 @@ +/*++ +Copyright (c) 2011 Microsoft Corporation + +Module Name: + + iz3hash.h + +Abstract: + + Wrapper for stl hash tables + +Author: + + Ken McMillan (kenmcmil) + +Revision History: + +--*/ + +// pull in the headers for has_map and hash_set +// these live in non-standard places + +#ifndef IZ3_HASH_H +#define IZ3_HASH_H + +//#define USE_UNORDERED_MAP +#ifdef USE_UNORDERED_MAP + +#define stl_ext std +#define hash_space std +#include +#include +#define hash_map unordered_map +#define hash_set unordered_set + +#else + +#if __GNUC__ >= 3 +#undef __DEPRECATED +#define stl_ext __gnu_cxx +#define hash_space stl_ext +#include +#include +#else +#ifdef WIN32 +#define stl_ext stdext +#define hash_space std +#include +#include +#else +#define stl_ext std +#define hash_space std +#include +#include +#endif +#endif + +#endif + +#include + +// stupid STL doesn't include hash function for class string + +#ifndef WIN32 + +namespace stl_ext { + template <> + class hash { + stl_ext::hash H; + public: + size_t operator()(const std::string &s) const { + return H(s.c_str()); + } + }; +} + +#endif + +namespace hash_space { + template <> + class hash > { + public: + size_t operator()(const std::pair &p) const { + return p.first + p.second; + } + }; +} + +#ifdef WIN32 +template <> inline +size_t stdext::hash_value >(const std::pair& p) +{ // hash _Keyval to size_t value one-to-one + return p.first + p.second; +} +#endif + +namespace hash_space { + template + class hash > { + public: + size_t operator()(const std::pair &p) const { + return (size_t)p.first + (size_t)p.second; + } + }; +} + +#if 0 +template inline +size_t stdext::hash_value >(const std::pair& p) +{ // hash _Keyval to size_t value one-to-one + return (size_t)p.first + (size_t)p.second; +} +#endif + +#ifdef WIN32 + +namespace std { + template <> + class less > { + public: + bool operator()(const pair &x, const pair &y) const { + return x.first < y.first || x.first == y.first && x.second < y.second; + } + }; + +} + +namespace std { + template + class less > { + public: + bool operator()(const pair &x, const pair &y) const { + return (size_t)x.first < (size_t)y.first || (size_t)x.first == (size_t)y.first && (size_t)x.second < (size_t)y.second; + } + }; + +} + +#endif + + +#ifndef WIN32 + +namespace stl_ext { + template + class hash { + public: + size_t operator()(const T *p) const { + return (size_t) p; + } + }; +} + +#endif + +#ifdef WIN32 + + + + +template +class hash_map : public stl_ext::hash_map > > {}; + +template +class hash_set : public stl_ext::hash_set > > {}; + +#endif + +#endif diff --git a/src/duality/duality_profiling.cpp b/src/duality/duality_profiling.cpp new file mode 100755 index 000000000..b516e03ca --- /dev/null +++ b/src/duality/duality_profiling.cpp @@ -0,0 +1,201 @@ +/*++ +Copyright (c) 2011 Microsoft Corporation + +Module Name: + + duality_profiling.cpp + +Abstract: + + collection performance information for duality + +Author: + + Ken McMillan (kenmcmil) + +Revision History: + + +--*/ + + +#include +#include +#include +#include +#include + +#ifdef WIN32 + +// include "Windows.h" + + +#if 0 +typedef __int64 clock_t; + +static clock_t current_time(){ + LARGE_INTEGER lpPerformanceCount; + lpPerformanceCount.QuadPart = 0; + QueryPerformanceCounter(&lpPerformanceCount); + return lpPerformanceCount.QuadPart; +} + +static void output_time(std::ostream &os, clock_t time){ + LARGE_INTEGER lpFrequency; + lpFrequency.QuadPart = 1; + QueryPerformanceFrequency(&lpFrequency); + os << ((double)time)/lpFrequency.QuadPart; +} +#else + +typedef double clock_t; + +static clock_t current_time(){ + FILETIME lpCreationTime; + FILETIME lpExitTime; + FILETIME lpKernelTime; + FILETIME lpUserTime; + + GetProcessTimes( GetCurrentProcess(), + &lpCreationTime, &lpExitTime, &lpKernelTime, &lpUserTime ); + + + double usr_time = ((double) lpUserTime.dwLowDateTime)/10000000. + + ((double) lpUserTime.dwHighDateTime)/(10000000. * pow(2.0,32.0)); + return usr_time; +} + +static void output_time(std::ostream &os, clock_t time){ + os << time; +} + +#endif + +#else + +#include +#include +#include +#include + +static clock_t current_time(){ +#if 0 + struct tms buf; + times(&buf); + return buf.tms_utime; +#else + struct rusage r; + getrusage(RUSAGE_SELF, &r); + return 1000 * r.ru_utime.tv_sec + r.ru_utime.tv_usec / 1000; +#endif +} + +static void output_time(std::ostream &os, clock_t time){ +#if 0 + os << ((double)time)/sysconf(_SC_CLK_TCK); +#else + os << ((double)time)/1000; +#endif +} + +#endif + + + +namespace Duality { + + void show_time(){ + output_time(std::cout,current_time()); + std::cout << "\n"; + } + + typedef std::map nmap; + + struct node { + std::string name; + clock_t time; + clock_t start_time; + nmap sub; + struct node *parent; + + node(); + } top; + + node::node(){ + time = 0; + parent = 0; + } + + struct node *current; + + struct init { + init(){ + top.name = "TOTAL"; + current = ⊤ + } + } initializer; + + struct time_entry { + clock_t t; + time_entry(){t = 0;}; + void add(clock_t incr){t += incr;} + }; + + struct ltstr + { + bool operator()(const char* s1, const char* s2) const + { + return strcmp(s1, s2) < 0; + } + }; + + typedef std::map tmap; + + static std::ostream *pfs; + + void print_node(node &top, int indent, tmap &totals){ + for(int i = 0; i < indent; i++) (*pfs) << " "; + (*pfs) << top.name; + int dots = 70 - 2 * indent - top.name.size(); + for(int i = 0; i second,indent+1,totals); + } + + void print_profile(std::ostream &os) { + pfs = &os; + top.time = 0; + for(nmap::iterator it = top.sub.begin(); it != top.sub.end(); it++) + top.time += it->second.time; + tmap totals; + print_node(top,0,totals); + (*pfs) << "TOTALS:" << std::endl; + for(tmap::iterator it = totals.begin(); it != totals.end(); it++){ + (*pfs) << (it->first) << " "; + output_time(*pfs, it->second.t); + (*pfs) << std::endl; + } + } + + void timer_start(const char *name){ + node &child = current->sub[name]; + if(child.name.empty()){ // a new node + child.parent = current; + child.name = name; + } + child.start_time = current_time(); + current = &child; + } + + void timer_stop(const char *name){ + if(current->name != name || !current->parent){ + std::cerr << "imbalanced timer_start and timer_stop"; + exit(1); + } + current->time += (current_time() - current->start_time); + current = current->parent; + } +} diff --git a/src/duality/duality_profiling.h b/src/duality/duality_profiling.h new file mode 100755 index 000000000..ff70fae23 --- /dev/null +++ b/src/duality/duality_profiling.h @@ -0,0 +1,38 @@ +/*++ +Copyright (c) 2011 Microsoft Corporation + +Module Name: + + duality_profiling.h + +Abstract: + + collection performance information for duality + +Author: + + Ken McMillan (kenmcmil) + +Revision History: + + +--*/ + +#ifndef DUALITYPROFILING_H +#define DUALITYPROFILING_H + +#include + +namespace Duality { + /** Start a timer with given name */ + void timer_start(const char *); + /** Stop a timer with given name */ + void timer_stop(const char *); + /** Print out timings */ + void print_profile(std::ostream &s); + /** Show the current time. */ + void show_time(); +} + +#endif + diff --git a/src/duality/duality_rpfp.cpp b/src/duality/duality_rpfp.cpp new file mode 100644 index 000000000..6b176a574 --- /dev/null +++ b/src/duality/duality_rpfp.cpp @@ -0,0 +1,1991 @@ +/*++ +Copyright (c) 2012 Microsoft Corporation + +Module Name: + + duality_rpfp.h + +Abstract: + + implements relational post-fixedpoint problem + (RPFP) data structure. + +Author: + + Ken McMillan (kenmcmil) + +Revision History: + + +--*/ + + + +#include "duality.h" +#include "duality_profiling.h" +#include +#include + +#ifndef WIN32 +// #define Z3OPS +#endif + +// TODO: do we need these? +#ifdef Z3OPS + +class Z3_subterm_truth { + public: + virtual bool eval(Z3_ast f) = 0; + ~Z3_subterm_truth(){} +}; + +Z3_subterm_truth *Z3_mk_subterm_truth(Z3_context ctx, Z3_model model); + +#endif + +#include + +// TODO: use something official for this +int debug_gauss = 0; + +namespace Duality { + + static char string_of_int_buffer[20]; + + const char *Z3User::string_of_int(int n){ + sprintf(string_of_int_buffer,"%d",n); + return string_of_int_buffer; + } + + RPFP::Term RPFP::SuffixVariable(const Term &t, int n) + { + std::string name = t.decl().name().str() + "_" + string_of_int(n); + return ctx.constant(name.c_str(), t.get_sort()); + } + + RPFP::Term RPFP::HideVariable(const Term &t, int n) + { + std::string name = std::string("@p_") + t.decl().name().str() + "_" + string_of_int(n); + return ctx.constant(name.c_str(), t.get_sort()); + } + + void RPFP::RedVars(Node *node, Term &b, std::vector &v) + { + int idx = node->number; + if(HornClauses) + b = ctx.bool_val(true); + else { + std::string name = std::string("@b_") + string_of_int(idx); + symbol sym = ctx.str_symbol(name.c_str()); + b = ctx.constant(sym,ctx.bool_sort()); + } + // ctx.constant(name.c_str(), ctx.bool_sort()); + v = node->Annotation.IndParams; + for(unsigned i = 0; i < v.size(); i++) + v[i] = SuffixVariable(v[i],idx); + } + + void Z3User::SummarizeRec(hash_set &memo, std::vector &lits, int &ops, const Term &t){ + if(memo.find(t) != memo.end()) + return; + memo.insert(t); + decl_kind k = t.decl().get_decl_kind(); + if(k == And || k == Or || k == Not || k == Implies || k == Iff){ + ops++; + int nargs = t.num_args(); + for(int i = 0; i < nargs; i++) + SummarizeRec(memo,lits,ops,t.arg(i)); + } + else + lits.push_back(t); + } + + int Z3User::CumulativeDecisions(){ +#if 0 + std::string stats = Z3_statistics_to_string(ctx); + int pos = stats.find("decisions:"); + pos += 10; + int end = stats.find('\n',pos); + std::string val = stats.substr(pos,end-pos); + return atoi(val.c_str()); +#endif + return slvr.get_num_decisions(); + } + + + void Z3User::Summarize(const Term &t){ + hash_set memo; std::vector lits; int ops = 0; + SummarizeRec(memo, lits, ops, t); + std::cout << ops << ": "; + for(unsigned i = 0; i < lits.size(); i++){ + if(i > 0) std::cout << ", "; + std::cout << lits[i]; + } + } + + Z3User::Term Z3User::conjoin(const std::vector &args){ + return ctx.make(And,args); + } + + Z3User::Term Z3User::sum(const std::vector &args){ + return ctx.make(Plus,args); + } + + RPFP::Term RPFP::RedDualRela(Edge *e, std::vector &args, int idx){ + Node *child = e->Children[idx]; + Term b(ctx); + std::vector v; + RedVars(child, b, v); + for (unsigned i = 0; i < args.size(); i++) + { + if (eq(args[i].get_sort(),ctx.bool_sort())) + args[i] = ctx.make(Iff,args[i], v[i]); + else + args[i] = args[i] == v[i]; + } + return args.size() > 0 ? (b && conjoin(args)) : b; + } + + Z3User::Term Z3User::CloneQuantifier(const Term &t, const Term &new_body){ +#if 0 + Z3_context c = ctx; + Z3_ast a = t; + std::vector pats; + int num_pats = Z3_get_quantifier_num_patterns(c,a); + for(int i = 0; i < num_pats; i++) + pats.push_back(Z3_get_quantifier_pattern_ast(c,a,i)); + std::vector no_pats; + int num_no_pats = Z3_get_quantifier_num_patterns(c,a); + for(int i = 0; i < num_no_pats; i++) + no_pats.push_back(Z3_get_quantifier_no_pattern_ast(c,a,i)); + int bound = Z3_get_quantifier_num_bound(c,a); + std::vector sorts; + std::vector names; + for(int i = 0; i < bound; i++){ + sorts.push_back(Z3_get_quantifier_bound_sort(c,a,i)); + names.push_back(Z3_get_quantifier_bound_name(c,a,i)); + } + Z3_ast foo = Z3_mk_quantifier_ex(c, + Z3_is_quantifier_forall(c,a), + Z3_get_quantifier_weight(c,a), + 0, + 0, + num_pats, + &pats[0], + num_no_pats, + &no_pats[0], + bound, + &sorts[0], + &names[0], + new_body); + return expr(ctx,foo); +#endif + return clone_quantifier(t,new_body); + } + + RPFP::Term RPFP::LocalizeRec(Edge *e, hash_map &memo, const Term &t) + { + std::pair foo(t,expr(ctx)); + std::pair::iterator, bool> bar = memo.insert(foo); + Term &res = bar.first->second; + if(!bar.second) return res; + hash_map::iterator it = e->varMap.find(t); + if (it != e->varMap.end()){ + res = it->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(LocalizeRec(e, memo, t.arg(i))); + hash_map::iterator rit = e->relMap.find(f); + if(rit != e->relMap.end()) + res = RedDualRela(e,args,(rit->second)); + else { + if (args.size() == 0 && f.get_decl_kind() == Uninterpreted) + { + res = HideVariable(t,e->number); + } + else + { + res = f(args.size(),&args[0]); + } + } + } + else if (t.is_quantifier()) + { + Term body = LocalizeRec(e,memo,t.body()); + res = CloneQuantifier(t,body); + } + else res = t; + return res; + } + + void RPFP::SetEdgeMaps(Edge *e){ + timer_start("SetEdgeMaps"); + e->relMap.clear(); + e->varMap.clear(); + for(unsigned i = 0; i < e->F.RelParams.size(); i++){ + e->relMap[e->F.RelParams[i]] = i; + } + Term b(ctx); + std::vector v; + RedVars(e->Parent, b, v); + for(unsigned i = 0; i < e->F.IndParams.size(); i++){ + // func_decl parentParam = e->Parent.Annotation.IndParams[i]; + expr oldname = e->F.IndParams[i]; + expr newname = v[i]; + e->varMap[oldname] = newname; + } + timer_stop("SetEdgeMaps"); + + } + + + RPFP::Term RPFP::Localize(Edge *e, const Term &t){ + timer_start("Localize"); + hash_map memo; + Term res = LocalizeRec(e,memo,t); + timer_stop("Localize"); + return res; + } + + + RPFP::Term RPFP::ReducedDualEdge(Edge *e) + { + SetEdgeMaps(e); + timer_start("RedVars"); + Term b(ctx); + std::vector v; + RedVars(e->Parent, b, v); + timer_stop("RedVars"); + // ast_to_track = (ast)b; + return implies(b, Localize(e, e->F.Formula)); + } + + TermTree *RPFP::ToTermTree(Node *root) + { + Edge *e = root->Outgoing; + if(!e) return new TermTree(ctx.bool_val(true), std::vector()); + std::vector children(e->Children.size()); + for(unsigned i = 0; i < children.size(); i++) + children[i] = ToTermTree(e->Children[i]); + // Term top = ReducedDualEdge(e); + Term top = e->dual.null() ? ctx.bool_val(true) : e->dual; + return new TermTree(top, children); + } + + TermTree *RPFP::GetGoalTree(Node *root){ + std::vector children(1); + children[0] = ToGoalTree(root); + return new TermTree(ctx.bool_val(false),children); + } + + TermTree *RPFP::ToGoalTree(Node *root) + { + Term b(ctx); + std::vector v; + RedVars(root, b, v); + Term goal = root->Name(v); + Edge *e = root->Outgoing; + if(!e) return new TermTree(goal, std::vector()); + std::vector children(e->Children.size()); + for(unsigned i = 0; i < children.size(); i++) + children[i] = ToGoalTree(e->Children[i]); + // Term top = ReducedDualEdge(e); + return new TermTree(goal, children); + } + + Z3User::Term Z3User::SubstRec(hash_map &memo, const Term &t) + { + std::pair foo(t,expr(ctx)); + std::pair::iterator, bool> bar = memo.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(SubstRec(memo, t.arg(i))); + res = f(args.size(),&args[0]); + } + else if (t.is_quantifier()) + res = CloneQuantifier(t,SubstRec(memo, t.body())); + else res = t; + return res; + } + + Z3User::Term Z3User::SubstRecHide(hash_map &memo, const Term &t, int number) + { + std::pair foo(t,expr(ctx)); + std::pair::iterator, bool> bar = memo.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(); + if (nargs == 0 && f.get_decl_kind() == Uninterpreted){ + std::string name = std::string("@q_") + t.decl().name().str() + "_" + string_of_int(number); + res = ctx.constant(name.c_str(), t.get_sort()); + return res; + } + for(int i = 0; i < nargs; i++) + args.push_back(SubstRec(memo, t.arg(i))); + res = f(args.size(),&args[0]); + } + else if (t.is_quantifier()) + res = CloneQuantifier(t,SubstRec(memo, t.body())); + else res = t; + return res; + } + + RPFP::Term RPFP::SubstParams(const std::vector &from, + const std::vector &to, const Term &t){ + hash_map memo; + bool some_diff = false; + for(unsigned i = 0; i < from.size(); i++) + if(i < to.size() && !eq(from[i],to[i])){ + memo[from[i]] = to[i]; + some_diff = true; + } + return some_diff ? SubstRec(memo,t) : t; + } + + + void Z3User::Strengthen(Term &x, const Term &y) + { + if (eq(x,ctx.bool_val(true))) + x = y; + else + x = x && y; + } + + void RPFP::DecodeTree(Node *root, TermTree *interp, int persist) + { + std::vector &ic = interp->getChildren(); + if (ic.size() > 0) + { + std::vector &nc = root->Outgoing->Children; + for (unsigned i = 0; i < nc.size(); i++) + DecodeTree(nc[i], ic[i], persist); + } + hash_map memo; + Term b; + std::vector v; + RedVars(root, b, v); + memo[b] = ctx.bool_val(true); + for (unsigned i = 0; i < v.size(); i++) + memo[v[i]] = root->Annotation.IndParams[i]; + Term annot = SubstRec(memo, interp->getTerm()); + // Strengthen(ref root.Annotation.Formula, annot); + root->Annotation.Formula = annot; +#if 0 + if(persist != 0) + Z3_persist_ast(ctx,root->Annotation.Formula,persist); +#endif + } + + RPFP::Term RPFP::GetUpperBound(Node *n) + { + // TODO: cache this + Term b(ctx); std::vector v; + RedVars(n, b, v); + hash_map memo; + for (unsigned int i = 0; i < v.size(); i++) + memo[n->Bound.IndParams[i]] = v[i]; + Term cnst = SubstRec(memo, n->Bound.Formula); + return b && !cnst; + } + + RPFP::Term RPFP::GetAnnotation(Node *n) + { + if(eq(n->Annotation.Formula,ctx.bool_val(true))) + return n->Annotation.Formula; + // TODO: cache this + Term b(ctx); std::vector v; + RedVars(n, b, v); + hash_map memo; + for (unsigned i = 0; i < v.size(); i++) + memo[n->Annotation.IndParams[i]] = v[i]; + Term cnst = SubstRec(memo, n->Annotation.Formula); + return !b || cnst; + } + + RPFP::Term RPFP::GetUnderapprox(Node *n) + { + // TODO: cache this + Term b(ctx); std::vector v; + RedVars(n, b, v); + hash_map memo; + for (unsigned i = 0; i < v.size(); i++) + memo[n->Underapprox.IndParams[i]] = v[i]; + Term cnst = SubstRecHide(memo, n->Underapprox.Formula, n->number); + return !b || cnst; + } + + TermTree *RPFP::AddUpperBound(Node *root, TermTree *t) + { + Term f = !((ast)(root->dual)) ? ctx.bool_val(true) : root->dual; + std::vector c(1); c[0] = t; + return new TermTree(f, c); + } + +#if 0 + void RPFP::WriteInterps(System.IO.StreamWriter f, TermTree t) + { + foreach (var c in t.getChildren()) + WriteInterps(f, c); + f.WriteLine(t.getTerm()); + } +#endif + + + /** 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. The constraint formula + * will survive "persist" pops of the context. If you plan + * to reassert the edge after popping the context once, + * you can save time re-constructing the formula by setting + * "persist" to one. If you set "persist" too high, however, + * you could have a memory leak. + * + * The flag "with children" causes the annotations of the children + * to be asserted. The flag underapprox causes the underapproximations + * of the children to be asserted *conditionally*. See Check() on + * how to actually enforce these constraints. + * + */ + + void RPFP::AssertEdge(Edge *e, int persist, bool with_children, bool underapprox) + { + if(eq(e->F.Formula,ctx.bool_val(true)) && (!with_children || e->Children.empty())) + return; + if (e->dual.null()) + { + timer_start("ReducedDualEdge"); + e->dual = ReducedDualEdge(e); + timer_stop("ReducedDualEdge"); + timer_start("getting children"); + if(with_children) + for(unsigned i = 0; i < e->Children.size(); i++) + e->dual = e->dual && GetAnnotation(e->Children[i]); + if(underapprox){ + std::vector cus(e->Children.size()); + for(unsigned i = 0; i < e->Children.size(); i++) + cus[i] = !UnderapproxFlag(e->Children[i]) || GetUnderapprox(e->Children[i]); + expr cnst = conjoin(cus); + e->dual = e->dual && cnst; + } + timer_stop("getting children"); + timer_start("Persisting"); + std::list::reverse_iterator it = stack.rbegin(); + for(int i = 0; i < persist && it != stack.rend(); i++) + it++; + if(it != stack.rend()) + it->edges.push_back(e); +#if 0 + if(persist != 0) + Z3_persist_ast(ctx,e->dual,persist); +#endif + timer_stop("Persisting"); + //Console.WriteLine("{0}", cnst); + } + timer_start("solver add"); + slvr.add(e->dual); + timer_stop("solver add"); + } + + + /** For incremental solving, asserts the negation of the upper bound associated + * with a node. + * */ + + void RPFP::AssertNode(Node *n) + { + if (n->dual.null()) + { + n->dual = GetUpperBound(n); + stack.back().nodes.push_back(n); + slvr.add(n->dual); + } + } + + /** 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 RPFP::AssertAxiom(const Term &t) + { + ls->assert_axiom(t); + axioms.push_back(t); // for printing only + } + +#if 0 + /** Do not call this. */ + + void RPFP::RemoveAxiom(const Term &t) + { + slvr.RemoveInterpolationAxiom(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 RPFP::Solve(Node *root, int persist) + { + timer_start("Solve"); + TermTree *tree = GetConstraintTree(root); + TermTree *interpolant = NULL; + TermTree *goals = NULL; + if(ls->need_goals) + goals = GetGoalTree(root); + + // if (dualModel != null) dualModel.Dispose(); + // if (dualLabels != null) dualLabels.Dispose(); + + timer_start("interpolate_tree"); + lbool res = ls->interpolate_tree(tree, interpolant, dualModel,goals); + timer_stop("interpolate_tree"); + if (res == l_false) + { + DecodeTree(root, interpolant->getChildren()[0], persist); + } + + timer_stop("Solve"); + return res; + } + + /** Get the constraint tree (but don't solve it) */ + + TermTree *RPFP::GetConstraintTree(Node *root) + { + return AddUpperBound(root, ToTermTree(root)); + } + + /** Dispose of the dual model (counterexample) if there is one. */ + + void RPFP::DisposeDualModel() + { + dualModel = model(ctx,NULL); + } + + RPFP::Term RPFP::UnderapproxFlag(Node *n){ + expr flag = ctx.constant((std::string("@under") + string_of_int(n->number)).c_str(), ctx.bool_sort()); + underapprox_flag_rev[flag] = n; + return flag; + } + + RPFP::Node *RPFP::UnderapproxFlagRev(const Term &flag){ + return underapprox_flag_rev[flag]; + } + + /** Check satisfiability of asserted edges and nodes. Same functionality as + * Solve, except no primal solution (interpolant) is generated in the unsat case. + * The vector underapproxes gives the set of node underapproximations to be enforced + * (assuming these were conditionally asserted by AssertEdge). + * + */ + + check_result RPFP::Check(Node *root, std::vector underapproxes, std::vector *underapprox_core ) + { + // if (dualModel != null) dualModel.Dispose(); + check_result res; + if(!underapproxes.size()) + res = slvr.check(); + else { + std::vector us(underapproxes.size()); + for(unsigned i = 0; i < underapproxes.size(); i++) + us[i] = UnderapproxFlag(underapproxes[i]); + slvr.check(); // TODO: no idea why I need to do this + if(underapprox_core){ + std::vector unsat_core(us.size()); + unsigned core_size = 0; + res = slvr.check(us.size(),&us[0],&core_size,&unsat_core[0]); + underapprox_core->resize(core_size); + for(unsigned i = 0; i < core_size; i++) + (*underapprox_core)[i] = UnderapproxFlagRev(unsat_core[i]); + } + else { + res = slvr.check(us.size(),&us[0]); + bool dump = false; + if(dump){ + std::vector cnsts; + // cnsts.push_back(axioms[0]); + cnsts.push_back(root->dual); + cnsts.push_back(root->Outgoing->dual); + ls->write_interpolation_problem("temp.smt",cnsts,std::vector()); + } + } + // check_result temp = slvr.check(); + } + dualModel = slvr.get_model(); + return res; + } + + check_result RPFP::CheckUpdateModel(Node *root, std::vector assumps){ + // check_result temp1 = slvr.check(); // no idea why I need to do this + check_result res = slvr.check_keep_model(assumps.size(),&assumps[0]); + dualModel = slvr.get_model(); + return res; + } + + /** Determines the value in the counterexample of a symbol occuring in the transformer formula of + * a given edge. */ + + RPFP::Term RPFP::Eval(Edge *e, Term t) + { + Term tl = Localize(e, t); + return dualModel.eval(tl); + } + + + + /** 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 RPFP::Empty(Node *p) + { + Term b; std::vector v; + RedVars(p, b, v); + // dualModel.show_internals(); + // std::cout << "b: " << b << std::endl; + expr bv = dualModel.eval(b); + // std::cout << "bv: " << bv << std::endl; + bool res = !eq(bv,ctx.bool_val(true)); + return res; + } + + RPFP::Term RPFP::EvalNode(Node *p) + { + Term b; std::vector v; + RedVars(p, b, v); + std::vector args; + for(unsigned i = 0; i < v.size(); i++) + args.push_back(dualModel.eval(v[i])); + return (p->Name)(args); + } + + void RPFP::EvalArrayTerm(const RPFP::Term &t, ArrayValue &res){ + if(t.is_app()){ + decl_kind k = t.decl().get_decl_kind(); + if(k == AsArray){ + func_decl fd = t.decl().get_func_decl_parameter(0); + func_interp r = dualModel.get_func_interp(fd); + int num = r.num_entries(); + res.defined = true; + for(int i = 0; i < num; i++){ + expr arg = r.get_arg(i,0); + expr value = r.get_value(i); + res.entries[arg] = value; + } + res.def_val = r.else_value(); + return; + } + else if(k == Store){ + EvalArrayTerm(t.arg(0),res); + if(!res.defined)return; + expr addr = t.arg(1); + expr val = t.arg(2); + if(addr.is_numeral() && val.is_numeral()){ + if(eq(val,res.def_val)) + res.entries.erase(addr); + else + res.entries[addr] = val; + } + else + res.defined = false; + return; + } + } + res.defined = false; + } + + int eae_count = 0; + + RPFP::Term RPFP::EvalArrayEquality(const RPFP::Term &f){ + ArrayValue lhs,rhs; + eae_count++; + EvalArrayTerm(f.arg(0),lhs); + EvalArrayTerm(f.arg(1),rhs); + if(lhs.defined && rhs.defined){ + if(eq(lhs.def_val,rhs.def_val)) + if(lhs.entries == rhs.entries) + return ctx.bool_val(true); + return ctx.bool_val(false); + } + return f; + } + + /** Compute truth values of all boolean subterms in current model. + Assumes formulas has been simplified by Z3, so only boolean ops + ands and, or, not. Returns result in memo. + */ + + int RPFP::SubtermTruth(hash_map &memo, const Term &f){ + if(memo.find(f) != memo.end()){ + return memo[f]; + } + int res; + if(f.is_app()){ + int nargs = f.num_args(); + decl_kind k = f.decl().get_decl_kind(); + if(k == Implies){ + res = SubtermTruth(memo,!f.arg(0) || f.arg(1)); + goto done; + } + if(k == And) { + res = 1; + for(int i = 0; i < nargs; i++){ + int ar = SubtermTruth(memo,f.arg(i)); + if(ar == 0){ + res = 0; + goto done; + } + if(ar == 2)res = 2; + } + goto done; + } + else if(k == Or) { + res = 0; + for(int i = 0; i < nargs; i++){ + int ar = SubtermTruth(memo,f.arg(i)); + if(ar == 1){ + res = 1; + goto done; + } + if(ar == 2)res = 2; + } + goto done; + } + else if(k == Not) { + int ar = SubtermTruth(memo,f.arg(0)); + res = (ar == 0) ? 1 : ((ar == 1) ? 0 : 2); + goto done; + } + } + { + expr bv = dualModel.eval(f); + if(bv.is_app() && bv.decl().get_decl_kind() == Equal && + bv.arg(0).is_array()){ + bv = EvalArrayEquality(bv); + } + // Hack!!!! array equalities can occur negatively! + if(bv.is_app() && bv.decl().get_decl_kind() == Not && + bv.arg(0).decl().get_decl_kind() == Equal && + bv.arg(0).arg(0).is_array()){ + bv = dualModel.eval(!EvalArrayEquality(bv.arg(0))); + } + if(eq(bv,ctx.bool_val(true))) + res = 1; + else if(eq(bv,ctx.bool_val(false))) + res = 0; + else + res = 2; + } + done: + memo[f] = res; + return res; + } + +#ifdef Z3OPS + static Z3_subterm_truth *stt; +#endif + + int ir_count = 0; + + void RPFP::ImplicantRed(hash_map &memo, const Term &f, std::vector &lits, + hash_set *done, bool truth, hash_set &dont_cares){ + if(done[truth].find(f) != done[truth].end()) + return; /* already processed */ +#if 0 + int this_count = ir_count++; + if(this_count == 50092) + std::cout << "foo!\n"; +#endif + if(f.is_app()){ + int nargs = f.num_args(); + decl_kind k = f.decl().get_decl_kind(); + if(k == Implies){ + ImplicantRed(memo,!f.arg(0) || f.arg(1),lits,done,truth,dont_cares); + goto done; + } + if(k == Iff){ + int b = SubtermTruth(memo,f.arg(0)); + if(b == 2) + throw "disaster in ImplicantRed"; + ImplicantRed(memo,f.arg(1),lits,done,truth ? b : !b,dont_cares); + goto done; + } + if(truth ? k == And : k == Or) { + for(int i = 0; i < nargs; i++) + ImplicantRed(memo,f.arg(i),lits,done,truth,dont_cares); + goto done; + } + if(truth ? k == Or : k == And) { + for(int i = 0; i < nargs; i++){ + Term a = f.arg(i); +#if 0 + if(i == nargs - 1){ // last chance! + ImplicantRed(memo,a,lits,done,truth,dont_cares); + goto done; + } +#endif + timer_start("SubtermTruth"); +#ifdef Z3OPS + bool b = stt->eval(a); +#else + int b = SubtermTruth(memo,a); +#endif + timer_stop("SubtermTruth"); + if(truth ? (b == 1) : (b == 0)){ + ImplicantRed(memo,a,lits,done,truth,dont_cares); + goto done; + } + } + /* Unreachable! */ + throw "error in RPFP::ImplicantRed"; + goto done; + } + else if(k == Not) { + ImplicantRed(memo,f.arg(0),lits,done,!truth,dont_cares); + goto done; + } + } + { + if(dont_cares.find(f) == dont_cares.end()){ + expr rf = ResolveIte(memo,f,lits,done,dont_cares); + expr bv = truth ? rf : !rf; + lits.push_back(bv); + } + } + done: + done[truth].insert(f); + } + + RPFP::Term RPFP::ResolveIte(hash_map &memo, const Term &t, std::vector &lits, + hash_set *done, hash_set &dont_cares){ + if(resolve_ite_memo.find(t) != resolve_ite_memo.end()) + return resolve_ite_memo[t]; + Term res; + if (t.is_app()) + { + func_decl f = t.decl(); + std::vector args; + int nargs = t.num_args(); + if(f.get_decl_kind() == Ite){ + timer_start("SubtermTruth"); +#ifdef Z3OPS + bool sel = stt->eval(t.arg(0)); +#else + int xval = SubtermTruth(memo,t.arg(0)); + bool sel; + if(xval == 0)sel = false; + else if(xval == 1)sel = true; + else + throw "unresolved ite in model"; +#endif + timer_stop("SubtermTruth"); + ImplicantRed(memo,t.arg(0),lits,done,sel,dont_cares); + res = ResolveIte(memo,t.arg(sel?1:2),lits,done,dont_cares); + } + else { + for(int i = 0; i < nargs; i++) + args.push_back(ResolveIte(memo,t.arg(i),lits,done,dont_cares)); + res = f(args.size(),&args[0]); + } + } + else res = t; + resolve_ite_memo[t] = res; + return res; + } + + void RPFP::Implicant(hash_map &memo, const Term &f, std::vector &lits, hash_set &dont_cares){ + hash_set done[2]; + ImplicantRed(memo,f,lits,done,true, dont_cares); + } + + + /** Underapproximate a formula using current counterexample. */ + + RPFP::Term RPFP::UnderapproxFormula(const Term &f, hash_set &dont_cares){ + /* first compute truth values of subterms */ + hash_map memo; + #ifdef Z3OPS + stt = Z3_mk_subterm_truth(ctx,dualModel); + #endif + // SubtermTruth(memo,f); + /* now compute an implicant */ + std::vector lits; + Implicant(memo,f,lits, dont_cares); +#ifdef Z3OPS + delete stt; stt = 0; +#endif + /* return conjunction of literals */ + return conjoin(lits); + } + + struct VariableProjector : Z3User { + + struct elim_cand { + Term var; + int sup; + Term val; + }; + + typedef expr Term; + + hash_set keep; + hash_map var_ord; + int num_vars; + std::vector elim_cands; + hash_map > sup_map; + hash_map elim_map; + std::vector ready_cands; + hash_map cand_map; + params simp_params; + + VariableProjector(Z3User &_user, std::vector &keep_vec) : + Z3User(_user), simp_params() + { + num_vars = 0; + for(unsigned i = 0; i < keep_vec.size(); i++){ + keep.insert(keep_vec[i]); + var_ord[keep_vec[i]] = num_vars++; + } + } + + int VarNum(const Term &v){ + if(var_ord.find(v) == var_ord.end()) + var_ord[v] = num_vars++; + return var_ord[v]; + } + + bool IsVar(const Term &t){ + return t.is_app() && t.num_args() == 0 && t.decl().get_decl_kind() == Uninterpreted; + } + + bool IsPropLit(const Term &t, Term &a){ + if(IsVar(t)){ + a = t; + return true; + } + else if(t.is_app() && t.decl().get_decl_kind() == Not) + return IsPropLit(t.arg(0),a); + return false; + } + + void CountOtherVarsRec(hash_map &memo, + const Term &t, + int id, + int &count){ + std::pair foo(t,0); + std::pair::iterator, bool> bar = memo.insert(foo); + // int &res = bar.first->second; + if(!bar.second) return; + if (t.is_app()) + { + func_decl f = t.decl(); + std::vector args; + int nargs = t.num_args(); + if (nargs == 0 && f.get_decl_kind() == Uninterpreted){ + if(cand_map.find(t) != cand_map.end()){ + count++; + sup_map[t].push_back(id); + } + } + for(int i = 0; i < nargs; i++) + CountOtherVarsRec(memo, t.arg(i), id, count); + } + else if (t.is_quantifier()) + CountOtherVarsRec(memo, t.body(), id, count); + } + + void NewElimCand(const Term &lhs, const Term &rhs){ + if(debug_gauss){ + std::cout << "mapping " << lhs << " to " << rhs << std::endl; + } + elim_cand cand; + cand.var = lhs; + cand.sup = 0; + cand.val = rhs; + elim_cands.push_back(cand); + cand_map[lhs] = elim_cands.size()-1; + } + + void MakeElimCand(const Term &lhs, const Term &rhs){ + if(eq(lhs,rhs)) + return; + if(!IsVar(lhs)){ + if(IsVar(rhs)){ + MakeElimCand(rhs,lhs); + return; + } + else{ + std::cout << "would have mapped a non-var\n"; + return; + } + } + if(IsVar(rhs) && VarNum(rhs) > VarNum(lhs)){ + MakeElimCand(rhs,lhs); + return; + } + if(keep.find(lhs) != keep.end()) + return; + if(cand_map.find(lhs) == cand_map.end()) + NewElimCand(lhs,rhs); + else { + int cand_idx = cand_map[lhs]; + if(IsVar(rhs) && cand_map.find(rhs) == cand_map.end() + && keep.find(rhs) == keep.end()) + NewElimCand(rhs,elim_cands[cand_idx].val); + elim_cands[cand_idx].val = rhs; + } + } + + Term FindRep(const Term &t){ + if(cand_map.find(t) == cand_map.end()) + return t; + Term &res = elim_cands[cand_map[t]].val; + if(IsVar(res)){ + assert(VarNum(res) < VarNum(t)); + res = FindRep(res); + return res; + } + return t; + } + + void GaussElimCheap(const std::vector &lits_in, + std::vector &lits_out){ + for(unsigned i = 0; i < lits_in.size(); i++){ + Term lit = lits_in[i]; + if(lit.is_app()){ + decl_kind k = lit.decl().get_decl_kind(); + if(k == Equal || k == Iff) + MakeElimCand(FindRep(lit.arg(0)),FindRep(lit.arg(1))); + } + } + + for(unsigned i = 0; i < elim_cands.size(); i++){ + elim_cand &cand = elim_cands[i]; + hash_map memo; + CountOtherVarsRec(memo,cand.val,i,cand.sup); + if(cand.sup == 0) + ready_cands.push_back(i); + } + + while(!ready_cands.empty()){ + elim_cand &cand = elim_cands[ready_cands.back()]; + ready_cands.pop_back(); + Term rep = FindRep(cand.var); + if(!eq(rep,cand.var)) + if(cand_map.find(rep) != cand_map.end()){ + int rep_pos = cand_map[rep]; + cand.val = elim_cands[rep_pos].val; + } + Term val = SubstRec(elim_map,cand.val); + if(debug_gauss){ + std::cout << "subbing " << cand.var << " --> " << val << std::endl; + } + elim_map[cand.var] = val; + std::vector &sup = sup_map[cand.var]; + for(unsigned i = 0; i < sup.size(); i++){ + int c = sup[i]; + if((--elim_cands[c].sup) == 0) + ready_cands.push_back(c); + } + } + + for(unsigned i = 0; i < lits_in.size(); i++){ + Term lit = lits_in[i]; + lit = SubstRec(elim_map,lit); + lit = lit.simplify(); + if(eq(lit,ctx.bool_val(true))) + continue; + Term a; + if(IsPropLit(lit,a)) + if(keep.find(lit) == keep.end()) + continue; + lits_out.push_back(lit); + } + } + + // maps variables to constrains in which the occur pos, neg + hash_map la_index[2]; + hash_map la_coeffs[2]; + std::vector la_pos_vars; + bool fixing; + + void IndexLAcoeff(const Term &coeff1, const Term &coeff2, Term t, int id){ + Term coeff = coeff1 * coeff2; + coeff = coeff.simplify(); + Term is_pos = (coeff >= ctx.int_val(0)); + is_pos = is_pos.simplify(); + if(eq(is_pos,ctx.bool_val(true))) + IndexLA(true,coeff,t, id); + else + IndexLA(false,coeff,t, id); + } + + void IndexLAremove(const Term &t){ + if(IsVar(t)){ + la_index[0][t] = -1; // means ineligible to be eliminated + la_index[1][t] = -1; // (more that one occurrence, or occurs not in linear comb) + } + else if(t.is_app()){ + int nargs = t.num_args(); + for(int i = 0; i < nargs; i++) + IndexLAremove(t.arg(i)); + } + // TODO: quantifiers? + } + + + void IndexLA(bool pos, const Term &coeff, const Term &t, int id){ + if(t.is_numeral()) + return; + if(t.is_app()){ + int nargs = t.num_args(); + switch(t.decl().get_decl_kind()){ + case Plus: + for(int i = 0; i < nargs; i++) + IndexLA(pos,coeff,t.arg(i), id); + break; + case Sub: + IndexLA(pos,coeff,t.arg(0), id); + IndexLA(!pos,coeff,t.arg(1), id); + break; + case Times: + if(t.arg(0).is_numeral()) + IndexLAcoeff(coeff,t.arg(0),t.arg(1), id); + else if(t.arg(1).is_numeral()) + IndexLAcoeff(coeff,t.arg(1),t.arg(0), id); + break; + default: + if(IsVar(t) && (fixing || la_index[pos].find(t) == la_index[pos].end())){ + la_index[pos][t] = id; + la_coeffs[pos][t] = coeff; + if(pos && !fixing) + la_pos_vars.push_back(t); // this means we only add a var once + } + else + IndexLAremove(t); + } + } + } + + void IndexLAstart(bool pos, const Term &t, int id){ + IndexLA(pos,(pos ? ctx.int_val(1) : ctx.int_val(-1)), t, id); + } + + void IndexLApred(bool pos, const Term &p, int id){ + if(p.is_app()){ + switch(p.decl().get_decl_kind()){ + case Not: + IndexLApred(!pos, p.arg(0),id); + break; + case Leq: + case Lt: + IndexLAstart(!pos, p.arg(0), id); + IndexLAstart(pos, p.arg(1), id); + break; + case Geq: + case Gt: + IndexLAstart(pos,p.arg(0), id); + IndexLAstart(!pos,p.arg(1), id); + break; + default: + IndexLAremove(p); + } + } + } + + void IndexLAfix(const Term &p, int id){ + fixing = true; + IndexLApred(true,p,id); + fixing = false; + } + + bool IsCanonIneq(const Term &lit, Term &term, Term &bound){ + // std::cout << Z3_simplify_get_help(ctx) << std::endl; + bool pos = lit.decl().get_decl_kind() != Not; + Term atom = pos ? lit : lit.arg(0); + if(atom.decl().get_decl_kind() == Leq){ + if(pos){ + bound = atom.arg(0); + term = atom.arg(1).simplify(simp_params); +#if Z3_MAJOR_VERSION < 4 + term = SortSum(term); +#endif + } + else { + bound = (atom.arg(1) + ctx.int_val(1)); + term = atom.arg(0); + // std::cout << "simplifying bound: " << bound << std::endl; + bound = bound.simplify(); + term = term.simplify(simp_params); +#if Z3_MAJOR_VERSION < 4 + term = SortSum(term); +#endif + } + return true; + } + else if(atom.decl().get_decl_kind() == Geq){ + if(pos){ + bound = atom.arg(1); // integer axiom + term = atom.arg(0).simplify(simp_params); +#if Z3_MAJOR_VERSION < 4 + term = SortSum(term); +#endif + return true; + } + else{ + bound = -(atom.arg(1) - ctx.int_val(1)); // integer axiom + term = -atom.arg(0); + bound = bound.simplify(); + term = term.simplify(simp_params); +#if Z3_MAJOR_VERSION < 4 + term = SortSum(term); +#endif + } + return true; + } + return false; + } + + Term CanonIneqTerm(const Term &p){ + Term term,bound; + Term ps = p.simplify(); + bool ok = IsCanonIneq(ps,term,bound); + assert(ok); + return term - bound; + } + + void ElimRedundantBounds(std::vector &lits){ + hash_map best_bound; + for(unsigned i = 0; i < lits.size(); i++){ + lits[i] = lits[i].simplify(simp_params); + Term term,bound; + if(IsCanonIneq(lits[i],term,bound)){ + if(best_bound.find(term) == best_bound.end()) + best_bound[term] = i; + else { + int best = best_bound[term]; + Term bterm,bbound; + IsCanonIneq(lits[best],bterm,bbound); + Term comp = bound > bbound; + comp = comp.simplify(); + if(eq(comp,ctx.bool_val(true))){ + lits[best] = ctx.bool_val(true); + best_bound[term] = i; + } + else { + lits[i] = ctx.bool_val(true); + } + } + } + } + } + + void FourierMotzkinCheap(const std::vector &lits_in, + std::vector &lits_out){ + simp_params.set(":som",true); + simp_params.set(":sort-sums",true); + fixing = false; lits_out = lits_in; + ElimRedundantBounds(lits_out); + for(unsigned i = 0; i < lits_out.size(); i++) + IndexLApred(true,lits_out[i],i); + + for(unsigned i = 0; i < la_pos_vars.size(); i++){ + Term var = la_pos_vars[i]; + if(la_index[false].find(var) != la_index[false].end()){ + int pos_idx = la_index[true][var]; + int neg_idx = la_index[false][var]; + if(pos_idx >= 0 && neg_idx >= 0){ + if(keep.find(var) != keep.end()){ + std::cout << "would have eliminated keep var\n"; + continue; + } + Term tpos = CanonIneqTerm(lits_out[pos_idx]); + Term tneg = CanonIneqTerm(lits_out[neg_idx]); + Term pos_coeff = la_coeffs[true][var]; + Term neg_coeff = -la_coeffs[false][var]; + Term comb = neg_coeff * tpos + pos_coeff * tneg; + Term ineq = ctx.int_val(0) <= comb; + ineq = ineq.simplify(); + lits_out[pos_idx] = ineq; + lits_out[neg_idx] = ctx.bool_val(true); + IndexLAfix(ineq,pos_idx); + } + } + } + } + + Term ProjectFormula(const Term &f){ + std::vector lits, new_lits1, new_lits2; + CollectConjuncts(f,lits); + timer_start("GaussElimCheap"); + GaussElimCheap(lits,new_lits1); + timer_stop("GaussElimCheap"); + timer_start("FourierMotzkinCheap"); + FourierMotzkinCheap(new_lits1,new_lits2); + timer_stop("FourierMotzkinCheap"); + return conjoin(new_lits2); + } + }; + + void Z3User::CollectConjuncts(const Term &f, std::vector &lits, bool pos){ + if(f.is_app() && f.decl().get_decl_kind() == Not) + CollectConjuncts(f.arg(0), lits, !pos); + else if(pos && f.is_app() && f.decl().get_decl_kind() == And){ + int num_args = f.num_args(); + for(int i = 0; i < num_args; i++) + CollectConjuncts(f.arg(i),lits,true); + } + else if(!pos && f.is_app() && f.decl().get_decl_kind() == Or){ + int num_args = f.num_args(); + for(int i = 0; i < num_args; i++) + CollectConjuncts(f.arg(i),lits,false); + } + else if(pos) + lits.push_back(f); + else + lits.push_back(!f); + } + + struct TermLt { + bool operator()(const expr &x, const expr &y){ + unsigned xid = x.get_id(); + unsigned yid = y.get_id(); + return xid < yid; + } + }; + + void Z3User::SortTerms(std::vector &terms){ + TermLt foo; + std::sort(terms.begin(),terms.end(),foo); + } + + Z3User::Term Z3User::SortSum(const Term &t){ + if(!(t.is_app() && t.decl().get_decl_kind() == Plus)) + return t; + int nargs = t.num_args(); + if(nargs < 2) return t; + std::vector args(nargs); + for(int i = 0; i < nargs; i++) + args[i] = t.arg(i); + SortTerms(args); + if(nargs == 2) + return args[0] + args[1]; + return sum(args); + } + + + RPFP::Term RPFP::ProjectFormula(std::vector &keep_vec, const Term &f){ + VariableProjector vp(*this,keep_vec); + return vp.ProjectFormula(f); + } + + /** Compute an underapproximation of every node in a tree rooted at "root", + based on a previously computed counterexample. The underapproximation + may contain free variables that are implicitly existentially quantified. + */ + + RPFP::Term RPFP::ComputeUnderapprox(Node *root, int persist){ + /* if terminated underapprox is empty set (false) */ + bool show_model = false; + if(show_model) + std::cout << dualModel << std::endl; + if(!root->Outgoing){ + root->Underapprox.SetEmpty(); + return ctx.bool_val(true); + } + /* if not used in cex, underapprox is empty set (false) */ + if(Empty(root)){ + root->Underapprox.SetEmpty(); + return ctx.bool_val(true); + } + /* compute underapprox of children first */ + std::vector &chs = root->Outgoing->Children; + std::vector chu(chs.size()); + for(unsigned i = 0; i < chs.size(); i++) + chu[i] = ComputeUnderapprox(chs[i],persist); + + Term b; std::vector v; + RedVars(root, b, v); + /* underapproximate the edge formula */ + hash_set dont_cares; + dont_cares.insert(b); + resolve_ite_memo.clear(); + timer_start("UnderapproxFormula"); + Term eu = UnderapproxFormula(root->Outgoing->dual,dont_cares); + timer_stop("UnderapproxFormula"); + /* combine with children */ + chu.push_back(eu); + eu = conjoin(chu); + /* project onto appropriate variables */ + eu = ProjectFormula(v,eu); + eu = eu.simplify(); + +#if 0 + /* check the result is consistent */ + { + hash_map memo; + int res = SubtermTruth(memo, eu); + if(res != 1) + throw "inconsistent projection"; + } +#endif + + /* rename to appropriate variable names */ + hash_map memo; + for (unsigned i = 0; i < v.size(); i++) + memo[v[i]] = root->Annotation.IndParams[i]; /* copy names from annotation */ + Term funder = SubstRec(memo, eu); + root->Underapprox = CreateRelation(root->Annotation.IndParams,funder); +#if 0 + if(persist) + Z3_persist_ast(ctx,root->Underapprox.Formula,persist); +#endif + return eu; + } + + + RPFP::Term RPFP::ModelValueAsConstraint(const Term &t){ + if(t.is_array()){ + ArrayValue arr; + Term e = dualModel.eval(t); + EvalArrayTerm(e, arr); + if(arr.defined){ + std::vector cs; + for(std::map::iterator it = arr.entries.begin(), en = arr.entries.end(); it != en; ++it){ + expr foo = select(t,expr(ctx,it->first)) == expr(ctx,it->second); + cs.push_back(foo); + } + return conjoin(cs); + } + } + else { + expr r = dualModel.get_const_interp(t.decl()); + if(!r.null()){ + expr res = t == expr(ctx,r); + return res; + } + } + return ctx.bool_val(true); + } + + void RPFP::EvalNodeAsConstraint(Node *p, Transformer &res) + { + Term b; std::vector v; + RedVars(p, b, v); + std::vector args; + for(unsigned i = 0; i < v.size(); i++){ + expr val = ModelValueAsConstraint(v[i]); + if(!eq(val,ctx.bool_val(true))) + args.push_back(val); + } + expr cnst = conjoin(args); + hash_map memo; + for (unsigned i = 0; i < v.size(); i++) + memo[v[i]] = p->Annotation.IndParams[i]; /* copy names from annotation */ + Term funder = SubstRec(memo, cnst); + res = CreateRelation(p->Annotation.IndParams,funder); + } + + + /** Push a scope. Assertions made after Push can be undone by Pop. */ + + void RPFP::Push() + { + stack.push_back(stack_entry()); + slvr.push(); + } + + /** Pop a scope (see Push). Note, you cannot pop axioms. */ + + void RPFP::Pop(int num_scopes) + { + slvr.pop(num_scopes); + for (int i = 0; i < num_scopes; i++) + { + stack_entry &back = stack.back(); + for(std::list::iterator it = back.edges.begin(), en = back.edges.end(); it != en; ++it) + (*it)->dual = expr(ctx,NULL); + for(std::list::iterator it = back.nodes.begin(), en = back.nodes.end(); it != en; ++it) + (*it)->dual = expr(ctx,NULL); + stack.pop_back(); + } + } + + + + + // This returns a new FuncDel with same sort as top-level function + // of term t, but with numeric suffix appended to name. + + Z3User::FuncDecl Z3User::SuffixFuncDecl(Term t, int n) + { + std::string name = t.decl().name().str() + "_" + string_of_int(n); + std::vector sorts; + int nargs = t.num_args(); + for(int i = 0; i < nargs; i++) + sorts.push_back(t.arg(i).get_sort()); + return ctx.function(name.c_str(), nargs, &sorts[0], t.get_sort()); + } + + // Scan the clause body for occurrences of the predicate unknowns + + RPFP::Term RPFP::ScanBody(hash_map &memo, + const Term &t, + hash_map &pmap, + std::vector &parms, + std::vector &nodes) + { + if(memo.find(t) != memo.end()) + return memo[t]; + Term res(ctx); + if (t.is_app()) { + func_decl f = t.decl(); + if(pmap.find(f) != pmap.end()){ + nodes.push_back(pmap[f]); + f = SuffixFuncDecl(t,parms.size()); + parms.push_back(f); + } + int nargs = t.num_args(); + std::vector args; + for(int i = 0; i < nargs; i++) + args.push_back(ScanBody(memo,t.arg(i),pmap,parms,nodes)); + res = f(nargs,&args[0]); + } + else if (t.is_quantifier()) + res = CloneQuantifier(t,ScanBody(memo,t.body(),pmap,parms,nodes)); + else + res = t; + memo[t] = res; + return res; + } + + // return the func_del of an app if it is uninterpreted + + bool Z3User::get_relation(const Term &t, func_decl &R){ + if(!t.is_app()) + return false; + R = t.decl(); + return R.get_decl_kind() == Uninterpreted; + } + + // return true if term is an individual variable + // TODO: have to check that it is not a background symbol + + bool Z3User::is_variable(const Term &t){ + if(!t.is_app()) + return false; + return t.decl().get_decl_kind() == Uninterpreted + && t.num_args() == 0; + } + + RPFP::Term RPFP::RemoveLabelsRec(hash_map &memo, const Term &t){ + if(memo.find(t) != memo.end()) + return memo[t]; + Term res(ctx); + if (t.is_app()){ + func_decl f = t.decl(); + if(t.num_args() == 1 && f.name().str().substr(0,3) == "lbl"){ + res = RemoveLabelsRec(memo,t.arg(0)); + } + else { + int nargs = t.num_args(); + std::vector args; + for(int i = 0; i < nargs; i++) + args.push_back(RemoveLabelsRec(memo,t.arg(i))); + res = f(nargs,&args[0]); + } + } + else if (t.is_quantifier()) + res = CloneQuantifier(t,RemoveLabelsRec(memo,t.body())); + else + res = t; + memo[t] = res; + return res; + } + + RPFP::Term RPFP::RemoveLabels(const Term &t){ + hash_map memo ; + return RemoveLabelsRec(memo,t); + } + + Z3User::Term Z3User::SubstBoundRec(hash_map > &memo, hash_map &subst, int level, 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(SubstBoundRec(memo, subst, level, t.arg(i))); + res = f(args.size(),&args[0]); + } + else if (t.is_quantifier()){ + int bound = t.get_quantifier_num_bound(); + res = CloneQuantifier(t,SubstBoundRec(memo, subst, level + bound, t.body())); + } + else if (t.is_var()) { + int idx = t.get_index_value(); + if(idx >= level && subst.find(idx-level) != subst.end()){ + res = subst[idx-level]; + } + else res = t; + } + else res = t; + return res; + } + + Z3User::Term Z3User::SubstBound(hash_map &subst, const Term &t){ + hash_map > memo; + return SubstBoundRec(memo, subst, 0, t); + } + + /** 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. + + */ + + + static bool canonical_clause(const expr &clause){ + if(clause.decl().get_decl_kind() != Implies) + return false; + expr arg = clause.arg(1); + return arg.is_app() && (arg.decl().get_decl_kind() == False || + arg.decl().get_decl_kind() == Uninterpreted); + } + + void RPFP::FromClauses(const std::vector &unskolemized_clauses){ + hash_map pmap; + func_decl fail_pred = ctx.fresh_func_decl("@Fail", ctx.bool_sort()); + + std::vector clauses(unskolemized_clauses); + // first, skolemize the clauses + + for(unsigned i = 0; i < clauses.size(); i++){ + expr &t = clauses[i]; + if (t.is_quantifier() && t.is_quantifier_forall()) { + int bound = t.get_quantifier_num_bound(); + std::vector sorts; + std::vector names; + hash_map subst; + for(int j = 0; j < bound; j++){ + sort the_sort = t.get_quantifier_bound_sort(j); + symbol name = t.get_quantifier_bound_name(j); + expr skolem = ctx.constant(symbol(ctx,name),sort(ctx,the_sort)); + subst[bound-1-j] = skolem; + } + t = SubstBound(subst,t.body()); + } + } + + // create the nodes from the heads of the clauses + + for(unsigned i = 0; i < clauses.size(); i++){ + Term &clause = clauses[i]; + if(!canonical_clause(clause)) + clause = implies((!clause).simplify(),ctx.bool_val(false)); + Term head = clause.arg(1); + func_decl R(ctx); + bool is_query = false; + if (eq(head,ctx.bool_val(false))){ + R = fail_pred; + // R = ctx.constant("@Fail", ctx.bool_sort()).decl(); + is_query = true; + } + else if(!get_relation(head,R)) + throw bad_clause("rhs must be a predicate application",i); + if(pmap.find(R) == pmap.end()){ + + // If the node doesn't exitst, create it. The Indparams + // are arbitrary, but we use the rhs arguments if they + // are variables for mnomonic value. + + hash_set seen; + std::vector Indparams; + for(unsigned j = 0; j < head.num_args(); j++){ + Term arg = head.arg(j); + if(!is_variable(arg) || seen.find(arg) != seen.end()){ + std::string name = std::string("@a_") + string_of_int(j); + arg = ctx.constant(name.c_str(),arg.get_sort()); + } + seen.insert(arg); + Indparams.push_back(arg); + } + Node *node = CreateNode(R(Indparams.size(),&Indparams[0])); + //nodes.push_back(node); + pmap[R] = node; + if (is_query) + node->Bound = CreateRelation(std::vector(), ctx.bool_val(false)); + } + } + + // create the edges + + for(unsigned i = 0; i < clauses.size(); i++){ + Term clause = clauses[i]; + Term body = clause.arg(0); + Term head = clause.arg(1); + func_decl R(ctx); + if (eq(head,ctx.bool_val(false))) + R = fail_pred; + //R = ctx.constant("@Fail", ctx.bool_sort()).decl(); + else get_relation(head,R); + Node *Parent = pmap[R]; + std::vector Indparams; + hash_set seen; + for(unsigned j = 0; j < head.num_args(); j++){ + Term arg = head.arg(j); + if(!is_variable(arg) || seen.find(arg) != seen.end()){ + std::string name = std::string("@a_") + string_of_int(j); + Term var = ctx.constant(name.c_str(),arg.get_sort()); + body = body && (arg == var); + arg = var; + } + seen.insert(arg); + Indparams.push_back(arg); + } + + // We extract the relparams positionally + + std::vector Relparams; + hash_map scan_memo; + std::vector Children; + body = ScanBody(scan_memo,body,pmap,Relparams,Children); + body = RemoveLabels(body); + body = body.simplify(); + + // Create the edge + Transformer T = CreateTransformer(Relparams,Indparams,body); + // Edge *edge = + CreateEdge(Parent,T,Children); + // edges.push_back(edge); + } + } + + + + void RPFP::WriteSolution(std::ostream &s){ + for(unsigned i = 0; i < nodes.size(); i++){ + Node *node = nodes[i]; + Term asgn = (node->Name)(node->Annotation.IndParams) == node->Annotation.Formula; + s << asgn << std::endl; + } + } + + void RPFP::WriteEdgeVars(Edge *e, hash_map &memo, const Term &t, std::ostream &s) + { + std::pair foo(t,0); + std::pair::iterator, bool> bar = memo.insert(foo); + // int &res = bar.first->second; + if(!bar.second) return; + hash_map::iterator it = e->varMap.find(t); + if (it != e->varMap.end()){ + return; + } + if (t.is_app()) + { + func_decl f = t.decl(); + // int idx; + int nargs = t.num_args(); + for(int i = 0; i < nargs; i++) + WriteEdgeVars(e, memo, t.arg(i),s); + if (nargs == 0 && f.get_decl_kind() == Uninterpreted){ + Term rename = HideVariable(t,e->number); + Term value = dualModel.eval(rename); + s << " (= " << t << " " << value << ")\n"; + } + } + else if (t.is_quantifier()) + WriteEdgeVars(e,memo,t.body(),s); + return; + } + + void RPFP::WriteEdgeAssignment(std::ostream &s, Edge *e){ + s << "(\n"; + hash_map memo; + WriteEdgeVars(e, memo, e->F.Formula ,s); + s << ")\n"; + } + + void RPFP::WriteCounterexample(std::ostream &s, Node *node){ + for(unsigned i = 0; i < node->Outgoing->Children.size(); i++){ + Node *child = node->Outgoing->Children[i]; + if(!Empty(child)) + WriteCounterexample(s,child); + } + s << "(" << node->number << " : " << EvalNode(node) << " <- "; + for(unsigned i = 0; i < node->Outgoing->Children.size(); i++){ + Node *child = node->Outgoing->Children[i]; + if(!Empty(child)) + s << " " << node->Outgoing->Children[i]->number; + } + s << ")" << std::endl; + WriteEdgeAssignment(s,node->Outgoing); + } + + RPFP::Term RPFP::ToRuleRec(Edge *e, hash_map &memo, const Term &t, std::vector &quants) + { + std::pair foo(t,expr(ctx)); + std::pair::iterator, bool> bar = memo.insert(foo); + Term &res = bar.first->second; + if(!bar.second) return res; + if (t.is_app()) + { + func_decl f = t.decl(); + // int idx; + std::vector args; + int nargs = t.num_args(); + for(int i = 0; i < nargs; i++) + args.push_back(ToRuleRec(e, memo, t.arg(i),quants)); + hash_map::iterator rit = e->relMap.find(f); + if(rit != e->relMap.end()){ + Node* child = e->Children[rit->second]; + FuncDecl op = child->Name; + res = op(args.size(),&args[0]); + } + else { + res = f(args.size(),&args[0]); + if(nargs == 0 && t.decl().get_decl_kind() == Uninterpreted) + quants.push_back(t); + } + } + else if (t.is_quantifier()) + { + Term body = ToRuleRec(e,memo,t.body(),quants); + res = CloneQuantifier(t,body); + } + else res = t; + return res; + } + + + void RPFP::ToClauses(std::vector &cnsts, FileFormat format){ + cnsts.resize(edges.size()); + for(unsigned i = 0; i < edges.size(); i++){ + Edge *edge = edges[i]; + SetEdgeMaps(edge); + std::vector quants; + hash_map memo; + Term lhs = ToRuleRec(edge, memo, edge->F.Formula,quants); + Term rhs = (edge->Parent->Name)(edge->F.IndParams.size(),&edge->F.IndParams[0]); + for(unsigned j = 0; j < edge->F.IndParams.size(); j++) + ToRuleRec(edge,memo,edge->F.IndParams[j],quants); // just to get quants + Term cnst = implies(lhs,rhs); +#if 0 + for(unsigned i = 0; i < quants.size(); i++){ + std::cout << expr(ctx,(Z3_ast)quants[i]) << " : " << sort(ctx,Z3_get_sort(ctx,(Z3_ast)quants[i])) << std::endl; + } +#endif + if(format != DualityFormat) + cnst= forall(quants,cnst); + cnsts[i] = cnst; + } + // int num_rules = cnsts.size(); + + for(unsigned i = 0; i < nodes.size(); i++){ + Node *node = nodes[i]; + if(!node->Bound.IsFull()){ + Term lhs = (node->Name)(node->Bound.IndParams) && !node->Bound.Formula; + Term cnst = implies(lhs,ctx.bool_val(false)); + if(format != DualityFormat){ + std::vector quants; + for(unsigned j = 0; j < node->Bound.IndParams.size(); j++) + quants.push_back(node->Bound.IndParams[j]); + if(format == HornFormat) + cnst= exists(quants,!cnst); + else + cnst= forall(quants, cnst); + } + cnsts.push_back(cnst); + } + } + + } + + +RPFP::~RPFP(){ + for(unsigned i = 0; i < nodes.size(); i++) + delete nodes[i]; + for(unsigned i = 0; i < edges.size(); i++) + delete edges[i]; + } +} + +#if 0 +void show_ast(expr *a){ + std::cout << *a; +} +#endif diff --git a/src/duality/duality_solver.cpp b/src/duality/duality_solver.cpp new file mode 100644 index 000000000..d5c6579d1 --- /dev/null +++ b/src/duality/duality_solver.cpp @@ -0,0 +1,2200 @@ +/*++ +Copyright (c) 2012 Microsoft Corporation + +Module Name: + + duality_solver.h + +Abstract: + + implements relational post-fixedpoint problem + (RPFP) solver + +Author: + + Ken McMillan (kenmcmil) + +Revision History: + + +--*/ + +#include "duality.h" +#include "duality_profiling.h" + +#include +#include +#include +#include + +// TODO: make these official options or get rid of them + +#define NEW_CAND_SEL +// #define LOCALIZE_CONJECTURES +// #define CANDS_FROM_UPDATES +#define CANDS_FROM_COVER_FAIL +#define DEPTH_FIRST_EXPAND +#define MINIMIZE_CANDIDATES +// #define MINIMIZE_CANDIDATES_HARDER +#define BOUNDED +#define CHECK_CANDS_FROM_IND_SET +#define UNDERAPPROX_NODES +#define NEW_EXPAND +#define EARLY_EXPAND +// #define TOP_DOWN +#define EFFORT_BOUNDED_STRAT +#define SKIP_UNDERAPPROX_NODES + + +namespace Duality { + + // TODO: must be a better place for this... + static char string_of_int_buffer[20]; + + static const char *string_of_int(int n){ + sprintf(string_of_int_buffer,"%d",n); + return string_of_int_buffer; + } + + /** Generic object for producing diagnostic output. */ + + class Reporter { + protected: + RPFP *rpfp; + public: + Reporter(RPFP *_rpfp){ + rpfp = _rpfp; + } + virtual void Extend(RPFP::Node *node){} + virtual void Update(RPFP::Node *node, const RPFP::Transformer &update){} + virtual void Bound(RPFP::Node *node){} + virtual void Expand(RPFP::Edge *edge){} + virtual void AddCover(RPFP::Node *covered, std::vector &covering){} + virtual void RemoveCover(RPFP::Node *covered, RPFP::Node *covering){} + virtual void Conjecture(RPFP::Node *node, const RPFP::Transformer &t){} + virtual void Forcing(RPFP::Node *covered, RPFP::Node *covering){} + virtual void Dominates(RPFP::Node *node, RPFP::Node *other){} + virtual void InductionFailure(RPFP::Edge *edge, const std::vector &children){} + virtual void UpdateUnderapprox(RPFP::Node *node, const RPFP::Transformer &update){} + virtual void Reject(RPFP::Edge *edge, const std::vector &Children){} + virtual ~Reporter(){} + }; + + Reporter *CreateStdoutReporter(RPFP *rpfp); + + /** Object we throw in case of catastrophe. */ + + struct InternalError { + std::string msg; + InternalError(const std::string _msg) + : msg(_msg) {} + }; + + + /** This is the main solver. It takes anarbitrary (possibly cyclic) + RPFP and either annotates it with a solution, or returns a + counterexample derivation in the form of an embedd RPFP tree. */ + + class Duality : public Solver { + + public: + Duality(RPFP *_rpfp) + : ctx(_rpfp->ctx), + slvr(_rpfp->slvr), + nodes(_rpfp->nodes), + edges(_rpfp->edges) + { + rpfp = _rpfp; + reporter = 0; + heuristic = 0; + FullExpand = false; + NoConj = false; + FeasibleEdges = true; + UseUnderapprox = true; + Report = false; + StratifiedInlining = false; + RecursionBound = -1; + } + + typedef RPFP::Node Node; + typedef RPFP::Edge Edge; + + /** This struct represents a candidate for extending the + unwinding. It consists of an edge to instantiate + and a vector of children for the new instance. */ + + struct Candidate { + Edge *edge; std::vector + Children; + }; + + /** Comparison operator, allowing us to sort Nodes + by their number field. */ + + struct lnode + { + bool operator()(const Node* s1, const Node* s2) const + { + return s1->number < s2->number; + } + }; + + typedef std::set Unexpanded; // sorted set of Nodes + + /** This class provides a heuristic for expanding a derivation + tree. */ + + class Heuristic { + RPFP *rpfp; + + /** Heuristic score for unwinding nodes. Currently this + counts the number of updates. */ + struct score { + int updates; + score() : updates(0) {} + }; + hash_map scores; + + public: + Heuristic(RPFP *_rpfp){ + rpfp = _rpfp; + } + virtual void Update(RPFP::Node *node){ + scores[node].updates++; + } + + /** Heuristic choice of nodes to expand. Takes a set "choices" + and returns a subset "best". We currently choose the + nodes with the fewest updates. + */ +#if 0 + virtual void ChooseExpand(const std::set &choices, std::set &best){ + int best_score = INT_MAX; + for(std::set::iterator it = choices.begin(), en = choices.end(); it != en; ++it){ + Node *node = (*it)->map; + int score = scores[node].updates; + best_score = std::min(best_score,score); + } + for(std::set::iterator it = choices.begin(), en = choices.end(); it != en; ++it) + if(scores[(*it)->map].updates == best_score) + best.insert(*it); + } +#else + virtual void ChooseExpand(const std::set &choices, std::set &best, bool high_priority=false){ + if(high_priority) return; + int best_score = INT_MAX; + int worst_score = 0; + for(std::set::iterator it = choices.begin(), en = choices.end(); it != en; ++it){ + Node *node = (*it)->map; + int score = scores[node].updates; + best_score = std::min(best_score,score); + worst_score = std::max(worst_score,score); + } + int cutoff = best_score + (worst_score-best_score)/2; + for(std::set::iterator it = choices.begin(), en = choices.end(); it != en; ++it) + if(scores[(*it)->map].updates <= cutoff) + best.insert(*it); + } +#endif + }; + + + class Covering; // see below + + // These members represent the state of the algorithm. + + RPFP *rpfp; // the input RPFP + Reporter *reporter; // object for logging + Heuristic *heuristic; // expansion heuristic + context &ctx; // Z3 context + solver &slvr; // Z3 solver + std::vector &nodes; // Nodes of input RPFP + std::vector &edges; // Edges of input RPFP + std::vector leaves; // leaf nodes of unwinding (unused) + Unexpanded unexpanded; // unexpanded nodes + std::list candidates; // candidates for expansion + // maps children to edges in input RPFP + hash_map > edges_by_child; + // maps each node in input RPFP to its expanded instances + hash_map > insts_of_node; + // maps each node in input RPFP to all its instances + hash_map > all_of_node; + RPFP *unwinding; // the unwinding + Covering *indset; // proposed inductive subset + Counterexample cex; // counterexample + std::list to_expand; + hash_set updated_nodes; + hash_map underapprox_map; // maps underapprox nodes to the nodes they approximate + int last_decisions; + hash_set overapproxes; + +#ifdef BOUNDED + struct Counter { + int val; + Counter(){val = 0;} + }; + typedef std::map NodeToCounter; + hash_map back_edges; // counts of back edges +#endif + + /** Solve the problem. */ + virtual bool Solve(){ + reporter = Report ? CreateStdoutReporter(rpfp) : new Reporter(rpfp); +#ifndef LOCALIZE_CONJECTURES + heuristic = !cex.tree ? new Heuristic(rpfp) : new ReplayHeuristic(rpfp,cex); +#else + heuristic = !cex.tree ? (Heuristic *)(new LocalHeuristic(rpfp)) + : (Heuristic *)(new ReplayHeuristic(rpfp,cex)); +#endif + unwinding = new RPFP(rpfp->ls); + unwinding->HornClauses = rpfp->HornClauses; + indset = new Covering(this); + last_decisions = 0; + CreateEdgesByChildMap(); + CreateLeaves(); +#ifndef TOP_DOWN + if(FeasibleEdges)NullaryCandidates(); + else InstantiateAllEdges(); +#else + for(unsigned i = 0; i < leaves.size(); i++) + if(!SatisfyUpperBound(leaves[i])) + return false; +#endif + StratifiedLeafCount = -1; + timer_start("SolveMain"); + bool res = SolveMain(); // does the actual work + timer_stop("SolveMain"); + // print_profile(std::cout); + delete indset; + delete heuristic; + return res; + } + +#if 0 + virtual void Restart(RPFP *_rpfp){ + rpfp = _rpfp; + delete unwinding; + nodes = _rpfp->nodes; + edges = _rpfp->edges; + leaves.clear(); + unexpanded.clear(); // unexpanded nodes + candidates.clear(); // candidates for expansion + edges_by_child.clear(); + insts_of_node.clear(); + all_of_node.clear(); + to_expand.clear(); + } +#endif + + virtual void LearnFrom(Solver *old_solver){ + cex = old_solver->GetCounterexample(); + } + + /** Return the counterexample */ + virtual Counterexample GetCounterexample(){ + return cex; + } + + // options + bool FullExpand; // do not use partial expansion of derivation tree + bool NoConj; // do not use conjectures (no forced covering) + bool FeasibleEdges; // use only feasible edges in unwinding + bool UseUnderapprox; // use underapproximations + bool Report; // spew on stdout + bool StratifiedInlining; // Do stratified inlining as preprocessing step + int RecursionBound; // Recursion bound for bounded verification + + bool SetBoolOption(bool &opt, const std::string &value){ + if(value == "0") { + opt = false; + return true; + } + if(value == "1") { + opt = true; + return true; + } + return false; + } + + bool SetIntOption(int &opt, const std::string &value){ + opt = atoi(value.c_str()); + return true; + } + + /** Set options (not currently used) */ + virtual bool SetOption(const std::string &option, const std::string &value){ + if(option == "full_expand"){ + return SetBoolOption(FullExpand,value); + } + if(option == "no_conj"){ + return SetBoolOption(NoConj,value); + } + if(option == "feasible_edges"){ + return SetBoolOption(FeasibleEdges,value); + } + if(option == "use_underapprox"){ + return SetBoolOption(UseUnderapprox,value); + } + if(option == "report"){ + return SetBoolOption(Report,value); + } + if(option == "stratified_inlining"){ + return SetBoolOption(StratifiedInlining,value); + } + if(option == "recursion_bound"){ + return SetIntOption(RecursionBound,value); + } + return false; + } + + /** Create an instance of a node in the unwinding. Set its + annotation to true, and mark it unexpanded. */ + Node* CreateNodeInstance(Node *node, int number = 0){ + RPFP::Node *inst = unwinding->CloneNode(node); + inst->Annotation.SetFull(); + if(number < 0) inst->number = number; + unexpanded.insert(inst); + all_of_node[node].push_back(inst); + return inst; + } + + /** Create an instance of an edge in the unwinding, with given + parent and children. */ + void CreateEdgeInstance(Edge *edge, Node *parent, const std::vector &children){ + RPFP::Edge *inst = unwinding->CreateEdge(parent,edge->F,children); + inst->map = edge; + } + + void MakeLeaf(Node *node, bool do_not_expand = false){ + node->Annotation.SetEmpty(); + Edge *e = unwinding->CreateLowerBoundEdge(node); +#ifdef TOP_DOWN + node->Annotation.SetFull(); // allow this node to cover others +#endif + if(StratifiedInlining) + node->Annotation.SetFull(); // allow this node to cover others + else + updated_nodes.insert(node); + e->map = 0; + reporter->Extend(node); +#ifdef EARLY_EXPAND + if(!do_not_expand) + TryExpandNode(node); +#endif + // e->F.SetEmpty(); + } + + void MakeOverapprox(Node *node){ + node->Annotation.SetFull(); + Edge *e = unwinding->CreateLowerBoundEdge(node); + overapproxes.insert(node); + e->map = 0; + } + + /** We start the unwinding with leaves that under-approximate + each relation with false. */ + void CreateLeaves(){ + unexpanded.clear(); + leaves.clear(); + for(unsigned i = 0; i < nodes.size(); i++){ + RPFP::Node *node = CreateNodeInstance(nodes[i]); + if(0 && nodes[i]->Outgoing->Children.size() == 0) + CreateEdgeInstance(nodes[i]->Outgoing,node,std::vector()); + else { + if(!StratifiedInlining) + MakeLeaf(node); + else { + MakeOverapprox(node); + LeafMap[nodes[i]] = node; + } + } + leaves.push_back(node); + } + } + + /** Create the map from children to edges in the input RPFP. This + is used to generate candidates for expansion. */ + void CreateEdgesByChildMap(){ + edges_by_child.clear(); + for(unsigned i = 0; i < edges.size(); i++){ + Edge *e = edges[i]; + std::set done; + for(unsigned j = 0; j < e->Children.size(); j++){ + Node *c = e->Children[j]; + if(done.find(c) == done.end()) // avoid duplicates + edges_by_child[c].push_back(e); + done.insert(c); + } + } + } + + void NullaryCandidates(){ + for(unsigned i = 0; i < edges.size(); i++){ + RPFP::Edge *edge = edges[i]; + if(edge->Children.size() == 0){ + Candidate cand; + cand.edge = edge; + candidates.push_back(cand); + } + } + } + + void InstantiateAllEdges(){ + hash_map leaf_map; + for(unsigned i = 0; i < leaves.size(); i++){ + leaf_map[leaves[i]->map] = leaves[i]; + insts_of_node[leaves[i]->map].push_back(leaves[i]); + } + unexpanded.clear(); + for(unsigned i = 0; i < edges.size(); i++){ + Edge *edge = edges[i]; + Candidate c; c.edge = edge; + c.Children.resize(edge->Children.size()); + for(unsigned j = 0; j < c.Children.size(); j++) + c.Children[j] = leaf_map[edge->Children[j]]; + Extend(c); + } + for(Unexpanded::iterator it = unexpanded.begin(), en = unexpanded.end(); it != en; ++it) + indset->Add(*it); + for(unsigned i = 0; i < leaves.size(); i++){ + std::vector &foo = insts_of_node[leaves[i]->map]; + foo.erase(foo.begin()); + } + } + + bool ProducedBySI(Edge *edge, std::vector &children){ + if(LeafMap.find(edge->Parent) == LeafMap.end()) return false; + Node *other = LeafMap[edge->Parent]; + if(other->Outgoing->map != edge) return false; + std::vector &ochs = other->Outgoing->Children; + for(unsigned i = 0; i < children.size(); i++) + if(ochs[i] != children[i]) return false; + return true; + } + + /** Add a candidate for expansion, but not if Stratified inlining has already + produced it */ + + void AddCandidate(Edge *edge, std::vector &children){ + if(StratifiedInlining && ProducedBySI(edge,children)) + return; + candidates.push_back(Candidate()); + candidates.back().edge = edge; + candidates.back().Children = children; + } + + /** Generate candidates for expansion, given a vector of candidate + sets for each argument position. This recursively produces + the cross product. + */ + void GenCandidatesRec(int pos, Edge *edge, + const std::vector > &vec, + std::vector &children){ + if(pos == (int)vec.size()){ + AddCandidate(edge,children); + } + else { + for(unsigned i = 0; i < vec[pos].size(); i++){ + children[pos] = vec[pos][i]; + GenCandidatesRec(pos+1,edge,vec,children); + } + } + } + + /** Setup for above recursion. */ + void GenCandidates(int pos, Edge *edge, + const std::vector > &vec){ + std::vector children(vec.size()); + GenCandidatesRec(0,edge,vec,children); + } + + /** Expand a node. We find all the candidates for expansion using + this node and other already expanded nodes. This is a little + tricky, since a node may be used for multiple argument + positions of an edge, and we don't want to produce duplicates. + */ + +#ifndef NEW_EXPAND + void ExpandNode(Node *node){ + std::vector &nedges = edges_by_child[node->map]; + for(unsigned i = 0; i < nedges.size(); i++){ + Edge *edge = nedges[i]; + for(unsigned npos = 0; npos < edge->Children.size(); ++npos){ + if(edge->Children[npos] == node->map){ + std::vector > vec(edge->Children.size()); + vec[npos].push_back(node); + for(unsigned j = 0; j < edge->Children.size(); j++){ + if(j != npos){ + std::vector &insts = insts_of_node[edge->Children[j]]; + for(unsigned k = 0; k < insts.size(); k++) + if(indset->Candidate(insts[k])) + vec[j].push_back(insts[k]); + } + if(j < npos && edge->Children[j] == node->map) + vec[j].push_back(node); + } + GenCandidates(0,edge,vec); + } + } + } + unexpanded.erase(node); + insts_of_node[node->map].push_back(node); + } +#else + /** If the current proposed solution is not inductive, + use the induction failure to generate candidates for extension. */ + void ExpandNode(Node *node){ + unexpanded.erase(node); + insts_of_node[node->map].push_back(node); + timer_start("GenCandIndFailUsing"); + std::vector &nedges = edges_by_child[node->map]; + for(unsigned i = 0; i < nedges.size(); i++){ + Edge *edge = nedges[i]; + slvr.push(); + RPFP *checker = new RPFP(rpfp->ls); + Node *root = CheckerJustForEdge(edge,checker,true); + if(root){ + expr using_cond = ctx.bool_val(false); + for(unsigned npos = 0; npos < edge->Children.size(); ++npos) + if(edge->Children[npos] == node->map) + using_cond = using_cond || checker->Localize(root->Outgoing->Children[npos]->Outgoing,NodeMarker(node)); + slvr.add(using_cond); + if(checker->Check(root) != unsat){ + Candidate candidate; + ExtractCandidateFromCex(edge,checker,root,candidate); + reporter->InductionFailure(edge,candidate.Children); + candidates.push_back(candidate); + } + } + slvr.pop(1); + delete checker; + } + timer_stop("GenCandIndFailUsing"); + } +#endif + + void ExpandNodeFromOther(Node *node, Node *other){ + std::vector &in = other->Incoming; + for(unsigned i = 0; i < in.size(); i++){ + Edge *edge = in[i]; + Candidate cand; + cand.edge = edge->map; + cand.Children = edge->Children; + for(unsigned j = 0; j < cand.Children.size(); j++) + if(cand.Children[j] == other) + cand.Children[j] = node; + candidates.push_front(cand); + } + // unexpanded.erase(node); + // insts_of_node[node->map].push_back(node); + } + + /** Expand a node based on some uncovered node it dominates. + This pushes cahdidates onto the *front* of the candidate + queue, so these expansions are done depth-first. */ + bool ExpandNodeFromCoverFail(Node *node){ + if(!node->Outgoing || node->Outgoing->Children.size() == 0) + return false; + Node *other = indset->GetSimilarNode(node); + if(!other) + return false; +#ifdef UNDERAPPROX_NODES + Node *under_node = CreateUnderapproxNode(node); + underapprox_map[under_node] = node; + indset->CoverByNode(node,under_node); + ExpandNodeFromOther(under_node,other); + ExpandNode(under_node); +#else + ExpandNodeFromOther(node,other); + unexpanded.erase(node); + insts_of_node[node->map].push_back(node); +#endif + return true; + } + + + /** Make a boolean variable to act as a "marker" for a node. */ + expr NodeMarker(Node *node){ + std::string name = std::string("@m_") + string_of_int(node->number); + return ctx.constant(name.c_str(),ctx.bool_sort()); + } + + /** Union the annotation of dst into src. If with_markers is + true, we conjoin the annotation formula of dst with its + marker. This allows us to discover which disjunct is + true in a satisfying assignment. */ + void UnionAnnotations(RPFP::Transformer &dst, Node *src, bool with_markers = false){ + if(!with_markers) + dst.UnionWith(src->Annotation); + else { + RPFP::Transformer t = src->Annotation; + t.Formula = t.Formula && NodeMarker(src); + dst.UnionWith(t); + } + } + + void GenNodeSolutionFromIndSet(Node *node, RPFP::Transformer &annot, bool with_markers = false){ + annot.SetEmpty(); + std::vector &insts = insts_of_node[node]; + for(unsigned j = 0; j < insts.size(); j++) + if(indset->Contains(insts[j])) + UnionAnnotations(annot,insts[j],with_markers); + annot.Simplify(); + } + + /** Generate a proposed solution of the input RPFP from + the unwinding, by unioning the instances of each node. */ + void GenSolutionFromIndSet(bool with_markers = false){ + for(unsigned i = 0; i < nodes.size(); i++){ + Node *node = nodes[i]; + GenNodeSolutionFromIndSet(node,node->Annotation,with_markers); + } + } + +#ifdef BOUNDED + bool NodePastRecursionBound(Node *node){ + if(RecursionBound < 0) return false; + NodeToCounter &backs = back_edges[node]; + for(NodeToCounter::iterator it = backs.begin(), en = backs.end(); it != en; ++it){ + if(it->second.val > RecursionBound) + return true; + } + return false; + } +#endif + + /** Test whether a given extension candidate actually represents + an induction failure. Right now we approximate this: if + the resulting node in the unwinding could be labeled false, + it clearly is not an induction failure. */ + + bool CandidateFeasible(const Candidate &cand){ + if(!FeasibleEdges) return true; + RPFP *checker = new RPFP(rpfp->ls); + // std::cout << "Checking feasibility of extension " << cand.edge->Parent->number << std::endl; + checker->Push(); + std::vector chs(cand.Children.size()); + Node *root = checker->CloneNode(cand.edge->Parent); +#ifdef BOUNDED + for(unsigned i = 0; i < cand.Children.size(); i++) + if(NodePastRecursionBound(cand.Children[i])) + return false; +#endif +#ifdef NEW_CAND_SEL + GenNodeSolutionFromIndSet(cand.edge->Parent,root->Bound); +#else + root->Bound.SetEmpty(); +#endif + checker->AssertNode(root); + for(unsigned i = 0; i < cand.Children.size(); i++) + chs[i] = checker->CloneNode(cand.Children[i]); + Edge *e = checker->CreateEdge(root,cand.edge->F,chs); + checker->AssertEdge(e,0,true); + // std::cout << "Checking SAT: " << e->dual << std::endl; + bool res = checker->Check(root) != unsat; + // std::cout << "Result: " << res << std::endl; + if(!res)reporter->Reject(cand.edge,cand.Children); + checker->Pop(1); + delete checker; + return res; + } + + + /* For stratified inlining, we need a topological sort of the + nodes. */ + + hash_map TopoSort; + int TopoSortCounter; + + void DoTopoSortRec(Node *node){ + if(TopoSort.find(node) != TopoSort.end()) + return; + TopoSort[node] = TopoSortCounter++; // just to break cycles + Edge *edge = node->Outgoing; // note, this is just *one* outgoing edge + if(edge){ + std::vector &chs = edge->Children; + for(unsigned i = 0; i < chs.size(); i++) + DoTopoSortRec(chs[i]); + } + TopoSort[node] = TopoSortCounter++; + } + + void DoTopoSort(){ + TopoSort.clear(); + TopoSortCounter = 0; + for(unsigned i = 0; i < nodes.size(); i++) + DoTopoSortRec(nodes[i]); + } + + /** In stratified inlining, we build the unwinding from the bottom + down, trying to satisfy the node bounds. We do this as a pre-pass, + limiting the expansion. If we get a counterexample, we are done, + else we continue as usual expanding the unwinding upward. + */ + + int StratifiedLeafCount; + + bool DoStratifiedInlining(){ + DoTopoSort(); + for(unsigned i = 0; i < leaves.size(); i++){ + Node *node = leaves[i]; + if(!SatisfyUpperBound(node)) + return false; + } + // don't leave any dangling nodes! +#ifndef EFFORT_BOUNDED_STRAT + for(unsigned i = 0; i < leaves.size(); i++) + if(!leaves[i]->Outgoing) + MakeLeaf(leaves[i],true); +#endif + return true; + } + + /** Here, we do the downward expansion for stratified inlining */ + + hash_map LeafMap, StratifiedLeafMap; + + Edge *GetNodeOutgoing(Node *node, int last_decs = 0){ + if(overapproxes.find(node) == overapproxes.end()) return node->Outgoing; /* already expanded */ + overapproxes.erase(node); +#ifdef EFFORT_BOUNDED_STRAT + if(last_decs > 5000){ + // RPFP::Transformer save = node->Annotation; + node->Annotation.SetEmpty(); + Edge *e = unwinding->CreateLowerBoundEdge(node); + // node->Annotation = save; + insts_of_node[node->map].push_back(node); + std::cout << "made leaf: " << node->number << std::endl; + return e; + } +#endif + Edge *edge = node->map->Outgoing; + std::vector &chs = edge->Children; + std::vector nchs(chs.size()); + for(unsigned i = 0; i < chs.size(); i++){ + Node *child = chs[i]; + if(TopoSort[child] < TopoSort[node->map]) + nchs[i] = LeafMap[child]; + else { + if(StratifiedLeafMap.find(child) == StratifiedLeafMap.end()){ + RPFP::Node *nchild = CreateNodeInstance(child,StratifiedLeafCount--); + MakeLeaf(nchild); + StratifiedLeafMap[child] = nchild; + indset->SetDominated(nchild); + } + nchs[i] = StratifiedLeafMap[child]; + } + } + CreateEdgeInstance(edge,node,nchs); + reporter->Extend(node); + return node->Outgoing; + } + + void SetHeuristicOldNode(Node *node){ + LocalHeuristic *h = dynamic_cast(heuristic); + if(h) + h->SetOldNode(node); + } + + /** This does the actual solving work. We try to generate + candidates for extension. If we succed, we extend the + unwinding. If we fail, we have a solution. */ + bool SolveMain(){ + if(StratifiedInlining && !DoStratifiedInlining()) + return false; +#ifdef BOUNDED + DoTopoSort(); +#endif + while(true){ + timer_start("ProduceCandidatesForExtension"); + ProduceCandidatesForExtension(); + timer_stop("ProduceCandidatesForExtension"); + if(candidates.empty()){ + GenSolutionFromIndSet(); + return true; + } + Candidate cand = candidates.front(); + candidates.pop_front(); + if(CandidateFeasible(cand)) + if(!Extend(cand)) + return false; + } + } + + // hack: put something local into the underapproximation formula + // without this, interpolants can be pretty bad + void AddThing(expr &conj){ + std::string name = "@thing"; + expr thing = ctx.constant(name.c_str(),ctx.bool_sort()); + if(conj.is_app() && conj.decl().get_decl_kind() == And){ + std::vector conjs(conj.num_args()+1); + for(unsigned i = 0; i+1 < conjs.size(); i++) + conjs[i] = conj.arg(i); + conjs[conjs.size()-1] = thing; + conj = rpfp->conjoin(conjs); + } + } + + + Node *CreateUnderapproxNode(Node *node){ + // cex.tree->ComputeUnderapprox(cex.root,0); + RPFP::Node *under_node = CreateNodeInstance(node->map /* ,StratifiedLeafCount-- */); + under_node->Annotation.IntersectWith(cex.root->Underapprox); + AddThing(under_node->Annotation.Formula); + Edge *e = unwinding->CreateLowerBoundEdge(under_node); + under_node->Annotation.SetFull(); // allow this node to cover others + back_edges[under_node] = back_edges[node]; + e->map = 0; + reporter->Extend(under_node); + return under_node; + } + + /** Try to prove a conjecture about a node. If successful + update the unwinding annotation appropriately. */ + bool ProveConjecture(Node *node, const RPFP::Transformer &t,Node *other = 0, Counterexample *_cex = 0){ + reporter->Conjecture(node,t); + timer_start("ProveConjecture"); + RPFP::Transformer save = node->Bound; + node->Bound.IntersectWith(t); + +#ifndef LOCALIZE_CONJECTURES + bool ok = SatisfyUpperBound(node); +#else + SetHeuristicOldNode(other); + bool ok = SatisfyUpperBound(node); + SetHeuristicOldNode(0); +#endif + + if(ok){ + timer_stop("ProveConjecture"); + return true; + } +#ifdef UNDERAPPROX_NODES + if(0 && last_decisions > 5000){ + std::cout << "making an underapprox\n"; + ExpandNodeFromCoverFail(node); + } +#endif + if(_cex) *_cex = cex; + else delete cex.tree; // delete the cex if not required + node->Bound = save; // put back original bound + timer_stop("ProveConjecture"); + return false; + } + + /** If a node is part of the inductive subset, expand it. + We ask the inductive subset to exclude the node if possible. + */ + void TryExpandNode(RPFP::Node *node){ + if(indset->Close(node)) return; + if(!NoConj && indset->Conjecture(node)){ +#ifdef UNDERAPPROX_NODES + /* TODO: temporary fix. this prevents an infinite loop in case + the node is covered by multiple others. This should be + removed when covering by a set is implemented. + */ + if(indset->Contains(node)){ + unexpanded.erase(node); + insts_of_node[node->map].push_back(node); + } +#endif + return; + } +#ifdef UNDERAPPROX_NODES + if(!indset->Contains(node)) + return; // could be covered by an underapprox node +#endif + indset->Add(node); +#if defined(CANDS_FROM_COVER_FAIL) && !defined(UNDERAPPROX_NODES) + if(ExpandNodeFromCoverFail(node)) + return; +#endif + ExpandNode(node); + } + + /** Make the conjunction of markers for all (expanded) instances of + a node in the input RPFP. */ + expr AllNodeMarkers(Node *node){ + expr res = ctx.bool_val(true); + std::vector &insts = insts_of_node[node]; + for(int k = insts.size()-1; k >= 0; k--) + res = res && NodeMarker(insts[k]); + return res; + } + + void RuleOutNodesPastBound(Node *node, RPFP::Transformer &t){ +#ifdef BOUNDED + if(RecursionBound < 0)return; + std::vector &insts = insts_of_node[node]; + for(unsigned i = 0; i < insts.size(); i++) + if(NodePastRecursionBound(insts[i])) + t.Formula = t.Formula && !NodeMarker(insts[i]); +#endif + } + + + void GenNodeSolutionWithMarkersAux(Node *node, RPFP::Transformer &annot, expr &marker_disjunction){ +#ifdef BOUNDED + if(RecursionBound >= 0 && NodePastRecursionBound(node)) + return; +#endif + RPFP::Transformer temp = node->Annotation; + expr marker = NodeMarker(node); + temp.Formula = (!marker || temp.Formula); + annot.IntersectWith(temp); + marker_disjunction = marker_disjunction || marker; + } + + bool GenNodeSolutionWithMarkers(Node *node, RPFP::Transformer &annot, bool expanded_only = false){ + bool res = false; + annot.SetFull(); + expr marker_disjunction = ctx.bool_val(false); + std::vector &insts = expanded_only ? insts_of_node[node] : all_of_node[node]; + for(unsigned j = 0; j < insts.size(); j++){ + Node *node = insts[j]; + if(indset->Contains(insts[j])){ + GenNodeSolutionWithMarkersAux(node, annot, marker_disjunction); res = true; + } + } + annot.Formula = annot.Formula && marker_disjunction; + annot.Simplify(); + return res; + } + + /** Make a checker to determine if an edge in the input RPFP + is satisfied. */ + Node *CheckerJustForEdge(Edge *edge, RPFP *checker, bool expanded_only = false){ + Node *root = checker->CloneNode(edge->Parent); + GenNodeSolutionFromIndSet(edge->Parent, root->Bound); + if(root->Bound.IsFull()) + return 0; + checker->AssertNode(root); + std::vector cs; + for(unsigned j = 0; j < edge->Children.size(); j++){ + Node *oc = edge->Children[j]; + Node *nc = checker->CloneNode(oc); + if(!GenNodeSolutionWithMarkers(oc,nc->Annotation,expanded_only)) + return 0; + Edge *e = checker->CreateLowerBoundEdge(nc); + checker->AssertEdge(e); + cs.push_back(nc); + } + checker->AssertEdge(checker->CreateEdge(root,edge->F,cs)); + return root; + } + +#ifndef MINIMIZE_CANDIDATES_HARDER + +#if 0 + /** Make a checker to detheermine if an edge in the input RPFP + is satisfied. */ + Node *CheckerForEdge(Edge *edge, RPFP *checker){ + Node *root = checker->CloneNode(edge->Parent); + root->Bound = edge->Parent->Annotation; + root->Bound.Formula = (!AllNodeMarkers(edge->Parent)) || root->Bound.Formula; + checker->AssertNode(root); + std::vector cs; + for(unsigned j = 0; j < edge->Children.size(); j++){ + Node *oc = edge->Children[j]; + Node *nc = checker->CloneNode(oc); + nc->Annotation = oc->Annotation; + RuleOutNodesPastBound(oc,nc->Annotation); + Edge *e = checker->CreateLowerBoundEdge(nc); + checker->AssertEdge(e); + cs.push_back(nc); + } + checker->AssertEdge(checker->CreateEdge(root,edge->F,cs)); + return root; + } + +#else + /** Make a checker to determine if an edge in the input RPFP + is satisfied. */ + Node *CheckerForEdge(Edge *edge, RPFP *checker){ + Node *root = checker->CloneNode(edge->Parent); + GenNodeSolutionFromIndSet(edge->Parent, root->Bound); +#if 0 + if(root->Bound.IsFull()) + return = 0; +#endif + checker->AssertNode(root); + std::vector cs; + for(unsigned j = 0; j < edge->Children.size(); j++){ + Node *oc = edge->Children[j]; + Node *nc = checker->CloneNode(oc); + GenNodeSolutionWithMarkers(oc,nc->Annotation,true); + Edge *e = checker->CreateLowerBoundEdge(nc); + checker->AssertEdge(e); + cs.push_back(nc); + } + checker->AssertEdge(checker->CreateEdge(root,edge->F,cs)); + return root; + } +#endif + + /** If an edge is not satisfied, produce an extension candidate + using instances of its children that violate the parent annotation. + We find these using the marker predicates. */ + void ExtractCandidateFromCex(Edge *edge, RPFP *checker, Node *root, Candidate &candidate){ + candidate.edge = edge; + for(unsigned j = 0; j < edge->Children.size(); j++){ + Edge *lb = root->Outgoing->Children[j]->Outgoing; + std::vector &insts = insts_of_node[edge->Children[j]]; +#ifndef MINIMIZE_CANDIDATES + for(int k = insts.size()-1; k >= 0; k--) +#else + for(unsigned k = 0; k < insts.size(); k++) +#endif + { + Node *inst = insts[k]; + if(indset->Contains(inst)){ + if(checker->Empty(lb->Parent) || + eq(checker->Eval(lb,NodeMarker(inst)),ctx.bool_val(true))){ + candidate.Children.push_back(inst); + goto next_child; + } + } + } + throw InternalError("No candidate from induction failure"); + next_child:; + } + } +#else + + + /** Make a checker to determine if an edge in the input RPFP + is satisfied. */ + Node *CheckerForEdge(Edge *edge, RPFP *checker){ + Node *root = checker->CloneNode(edge->Parent); + GenNodeSolutionFromIndSet(edge->Parent, root->Bound); + if(root->Bound.IsFull()) + return = 0; + checker->AssertNode(root); + std::vector cs; + for(unsigned j = 0; j < edge->Children.size(); j++){ + Node *oc = edge->Children[j]; + Node *nc = checker->CloneNode(oc); + GenNodeSolutionWithMarkers(oc,nc->Annotation,true); + Edge *e = checker->CreateLowerBoundEdge(nc); + checker->AssertEdge(e); + cs.push_back(nc); + } + checker->AssertEdge(checker->CreateEdge(root,edge->F,cs)); + return root; + } + + /** If an edge is not satisfied, produce an extension candidate + using instances of its children that violate the parent annotation. + We find these using the marker predicates. */ + void ExtractCandidateFromCex(Edge *edge, RPFP *checker, Node *root, Candidate &candidate){ + candidate.edge = edge; + std::vector assumps; + for(unsigned j = 0; j < edge->Children.size(); j++){ + Edge *lb = root->Outgoing->Children[j]->Outgoing; + std::vector &insts = insts_of_node[edge->Children[j]]; + for(unsigned k = 0; k < insts.size(); k++) + { + Node *inst = insts[k]; + expr marker = NodeMarker(inst); + if(indset->Contains(inst)){ + if(checker->Empty(lb->Parent) || + eq(checker->Eval(lb,marker),ctx.bool_val(true))){ + candidate.Children.push_back(inst); + assumps.push_back(checker->Localize(lb,marker)); + goto next_child; + } + assumps.push_back(checker->Localize(lb,marker)); + if(checker->CheckUpdateModel(root,assumps) != unsat){ + candidate.Children.push_back(inst); + goto next_child; + } + assumps.pop_back(); + } + } + throw InternalError("No candidate from induction failure"); + next_child:; + } + } + +#endif + + + /** If the current proposed solution is not inductive, + use the induction failure to generate candidates for extension. */ + void GenCandidatesFromInductionFailure(bool full_scan = false){ + timer_start("GenCandIndFail"); + GenSolutionFromIndSet(true /* add markers */); + for(unsigned i = 0; i < edges.size(); i++){ + Edge *edge = edges[i]; + if(!full_scan && updated_nodes.find(edge->Parent) == updated_nodes.end()) + continue; + slvr.push(); + RPFP *checker = new RPFP(rpfp->ls); + Node *root = CheckerForEdge(edge,checker); + if(checker->Check(root) != unsat){ + Candidate candidate; + ExtractCandidateFromCex(edge,checker,root,candidate); + reporter->InductionFailure(edge,candidate.Children); + candidates.push_back(candidate); + } + slvr.pop(1); + delete checker; + } + updated_nodes.clear(); + timer_stop("GenCandIndFail"); +#ifdef CHECK_CANDS_FROM_IND_SET + for(std::list::iterator it = candidates.begin(), en = candidates.end(); it != en; ++it){ + if(!CandidateFeasible(*it)) + throw "produced infeasible candidate"; + } +#endif + if(!full_scan && candidates.empty()){ + std::cout << "No candidates from updates. Trying full scan.\n"; + GenCandidatesFromInductionFailure(true); + } + } + +#ifdef CANDS_FROM_UPDATES + /** If the given edge is not inductive in the current proposed solution, + use the induction failure to generate candidates for extension. */ + void GenCandidatesFromEdgeInductionFailure(RPFP::Edge *edge){ + GenSolutionFromIndSet(true /* add markers */); + for(unsigned i = 0; i < edges.size(); i++){ + slvr.push(); + Edge *edge = edges[i]; + RPFP *checker = new RPFP(rpfp->ls); + Node *root = CheckerForEdge(edge,checker); + if(checker->Check(root) != unsat){ + Candidate candidate; + ExtractCandidateFromCex(edge,checker,root,candidate); + reporter->InductionFailure(edge,candidate.Children); + candidates.push_back(candidate); + } + slvr.pop(1); + delete checker; + } + } +#endif + + /** Find the unexpanded nodes in the inductive subset. */ + void FindNodesToExpand(){ + for(Unexpanded::iterator it = unexpanded.begin(), en = unexpanded.end(); it != en; ++it){ + Node *node = *it; + if(indset->Candidate(node)) + to_expand.push_back(node); + } + } + + /** Try to create some extension candidates from the unexpanded + nodes. */ + void ProduceSomeCandidates(){ + while(candidates.empty() && !to_expand.empty()){ + Node *node = to_expand.front(); + to_expand.pop_front(); + TryExpandNode(node); + } + } + + std::list postponed_candidates; + + /** Try to produce some extension candidates, first from unexpanded + nides, and if this fails, from induction failure. */ + void ProduceCandidatesForExtension(){ + if(candidates.empty()) + ProduceSomeCandidates(); + while(candidates.empty()){ + FindNodesToExpand(); + if(to_expand.empty()) break; + ProduceSomeCandidates(); + } + if(candidates.empty()){ +#ifdef DEPTH_FIRST_EXPAND + if(postponed_candidates.empty()){ + GenCandidatesFromInductionFailure(); + postponed_candidates.swap(candidates); + } + if(!postponed_candidates.empty()){ + candidates.push_back(postponed_candidates.front()); + postponed_candidates.pop_front(); + } +#else + GenCandidatesFromInductionFailure(); +#endif + } + } + + /** Update the unwinding solution, using an interpolant for the + derivation tree. */ + void UpdateWithInterpolant(Node *node, RPFP *tree, Node *top){ + if(top->Outgoing) + for(unsigned i = 0; i < top->Outgoing->Children.size(); i++) + UpdateWithInterpolant(node->Outgoing->Children[i],tree,top->Outgoing->Children[i]); + if(!node->Annotation.SubsetEq(top->Annotation)){ + reporter->Update(node,top->Annotation); + indset->Update(node,top->Annotation); + updated_nodes.insert(node->map); + node->Annotation.IntersectWith(top->Annotation); + } + heuristic->Update(node); + } + + /** Update unwinding lower bounds, using a counterexample. */ + + void UpdateWithCounterexample(Node *node, RPFP *tree, Node *top){ + if(top->Outgoing) + for(unsigned i = 0; i < top->Outgoing->Children.size(); i++) + UpdateWithCounterexample(node->Outgoing->Children[i],tree,top->Outgoing->Children[i]); + if(!top->Underapprox.SubsetEq(node->Underapprox)){ + reporter->UpdateUnderapprox(node,top->Underapprox); + // indset->Update(node,top->Annotation); + node->Underapprox.UnionWith(top->Underapprox); + heuristic->Update(node); + } + } + + /** Try to update the unwinding to satisfy the upper bound of a + node. */ + bool SatisfyUpperBound(Node *node){ + if(node->Bound.IsFull()) return true; + reporter->Bound(node); + int start_decs = rpfp->CumulativeDecisions(); + DerivationTree dt(this,unwinding,reporter,heuristic,FullExpand); + bool res = dt.Derive(unwinding,node,UseUnderapprox); + int end_decs = rpfp->CumulativeDecisions(); + std::cout << "decisions: " << (end_decs - start_decs) << std::endl; + last_decisions = end_decs - start_decs; + if(res){ + cex.tree = dt.tree; + cex.root = dt.top; + if(UseUnderapprox){ + UpdateWithCounterexample(node,dt.tree,dt.top); + } + } + else { + UpdateWithInterpolant(node,dt.tree,dt.top); + delete dt.tree; + } + return !res; + } + + /* If the counterexample derivation is partial due to + use of underapproximations, complete it. */ + + void BuildFullCex(Node *node){ + DerivationTree dt(this,unwinding,reporter,heuristic,FullExpand); + bool res = dt.Derive(unwinding,node,UseUnderapprox,true); // build full tree + if(!res) throw "Duality internal error in BuildFullCex"; + cex.tree = dt.tree; + cex.root = dt.top; + } + + void UpdateBackEdges(Node *node){ +#ifdef BOUNDED + std::vector &chs = node->Outgoing->Children; + for(unsigned i = 0; i < chs.size(); i++){ + Node *child = chs[i]; + bool is_back = TopoSort[child->map] >= TopoSort[node->map]; + NodeToCounter &nov = back_edges[node]; + NodeToCounter chv = back_edges[child]; + if(is_back) + chv[child->map].val++; + for(NodeToCounter::iterator it = chv.begin(), en = chv.end(); it != en; ++it){ + Node *back = it->first; + Counter &c = nov[back]; + c.val = std::max(c.val,it->second.val); + } + } +#endif + } + + /** Extend the unwinding, keeping it solved. */ + bool Extend(Candidate &cand){ + Node *node = CreateNodeInstance(cand.edge->Parent); + CreateEdgeInstance(cand.edge,node,cand.Children); + UpdateBackEdges(node); + reporter->Extend(node); + bool res = SatisfyUpperBound(node); + if(res) indset->CloseDescendants(node); + else { +#ifdef UNDERAPPROX_NODES + ExpandUnderapproxNodes(cex.tree, cex.root); +#endif + if(UseUnderapprox) BuildFullCex(node); + return res; + } +#ifdef EARLY_EXPAND + TryExpandNode(node); +#endif + return res; + } + + void ExpandUnderapproxNodes(RPFP *tree, Node *root){ + Node *node = root->map; + if(underapprox_map.find(node) != underapprox_map.end()){ + RPFP::Transformer cnst = root->Annotation; + tree->EvalNodeAsConstraint(root, cnst); + cnst.Complement(); + Node *orig = underapprox_map[node]; + RPFP::Transformer save = orig->Bound; + orig->Bound = cnst; + DerivationTree dt(this,unwinding,reporter,heuristic,FullExpand); + bool res = dt.Derive(unwinding,orig,UseUnderapprox,true,tree); + if(!res){ + UpdateWithInterpolant(orig,dt.tree,dt.top); + throw "bogus underapprox!"; + } + ExpandUnderapproxNodes(tree,dt.top); + } + else if(root->Outgoing){ + std::vector &chs = root->Outgoing->Children; + for(unsigned i = 0; i < chs.size(); i++) + ExpandUnderapproxNodes(tree,chs[i]); + } + } + + + /** This class represents a derivation tree. */ + class DerivationTree { + public: + + DerivationTree(Duality *_duality, RPFP *rpfp, Reporter *_reporter, Heuristic *_heuristic, bool _full_expand) + : slvr(rpfp->slvr), + ctx(rpfp->ctx) + { + duality = _duality; + reporter = _reporter; + heuristic = _heuristic; + full_expand = _full_expand; + } + + Duality *duality; + Reporter *reporter; + Heuristic *heuristic; + solver &slvr; + context &ctx; + RPFP *tree; + RPFP::Node *top; + std::list leaves; + bool full_expand; + bool underapprox; + bool constrained; + bool false_approx; + std::vector underapprox_core; + int start_decs, last_decs; + + /* We build derivation trees in one of three modes: + + 1) In normal mode, we build the full tree without considering + underapproximations. + + 2) In underapprox mode, we use underapproximations to cut off + the tree construction. THis means the resulting tree may not + be complete. + + 3) In constrained mode, we build the full tree but use + underapproximations as upper bounds. This mode is used to + complete the partial derivation constructed in underapprox + mode. + */ + + bool Derive(RPFP *rpfp, RPFP::Node *root, bool _underapprox, bool _constrained = false, RPFP *_tree = 0){ + underapprox = _underapprox; + constrained = _constrained; + false_approx = true; + timer_start("Derive"); + tree = _tree ? _tree : new RPFP(rpfp->ls); + tree->HornClauses = rpfp->HornClauses; + tree->Push(); // so we can clear out the solver later when finished + top = CreateApproximatedInstance(root); + tree->AssertNode(top); // assert the negation of the top-level spec + timer_start("Build"); + bool res = Build(); + timer_stop("Build"); + timer_start("Pop"); + tree->Pop(1); + timer_stop("Pop"); + timer_stop("Derive"); + return res; + } + +#define WITH_CHILDREN + + Node *CreateApproximatedInstance(RPFP::Node *from){ + Node *to = tree->CloneNode(from); + to->Annotation = from->Annotation; +#ifndef WITH_CHILDREN + tree->CreateLowerBoundEdge(to); +#endif + leaves.push_back(to); + return to; + } + + bool CheckWithUnderapprox(){ + timer_start("CheckWithUnderapprox"); + std::vector leaves_vector(leaves.size()); + std::copy(leaves.begin(),leaves.end(),leaves_vector.begin()); + check_result res = tree->Check(top,leaves_vector); + timer_stop("CheckWithUnderapprox"); + return res != unsat; + } + + bool Build(){ +#ifdef EFFORT_BOUNDED_STRAT + start_decs = tree->CumulativeDecisions(); +#endif + // while(ExpandSomeNodes(true)); // do high-priority expansions + while (true) + { +#ifndef WITH_CHILDREN + timer_start("asserting leaves"); + timer_start("pushing"); + tree->Push(); + timer_stop("pushing"); + for(std::list::iterator it = leaves.begin(), en = leaves.end(); it != en; ++it) + tree->AssertEdge((*it)->Outgoing,1); // assert the overapproximation, and keep it past pop + timer_stop("asserting leaves"); + lbool res = tree->Solve(top, 2); // incremental solve, keep interpolants for two pops + timer_start("popping leaves"); + tree->Pop(1); + timer_stop("popping leaves"); +#else + lbool res; + if((underapprox || false_approx) && top->Outgoing && CheckWithUnderapprox()){ + if(constrained) goto expand_some_nodes; // in constrained mode, keep expanding + goto we_are_sat; // else if underapprox is sat, we stop + } + // tree->Check(top); + res = tree->Solve(top, 1); // incremental solve, keep interpolants for one pop +#endif + if (res == l_false) + return false; + + expand_some_nodes: + if(ExpandSomeNodes()) + continue; + + we_are_sat: + if(underapprox && !constrained){ + timer_start("ComputeUnderapprox"); + tree->ComputeUnderapprox(top,1); + timer_stop("ComputeUnderapprox"); + } + else { +#ifdef UNDERAPPROX_NODES +#ifndef SKIP_UNDERAPPROX_NODES + timer_start("ComputeUnderapprox"); + tree->ComputeUnderapprox(top,1); + timer_stop("ComputeUnderapprox"); +#endif +#endif + } + return true; + } + } + + void ExpandNode(RPFP::Node *p){ + // tree->RemoveEdge(p->Outgoing); + Edge *edge = duality->GetNodeOutgoing(p->map,last_decs); + std::vector &cs = edge->Children; + std::vector children(cs.size()); + for(unsigned i = 0; i < cs.size(); i++) + children[i] = CreateApproximatedInstance(cs[i]); + Edge *ne = tree->CreateEdge(p, p->map->Outgoing->F, children); + ne->map = p->map->Outgoing->map; +#ifndef WITH_CHILDREN + tree->AssertEdge(ne); // assert the edge in the solver +#else + tree->AssertEdge(ne,0,!full_expand,(underapprox || false_approx)); // assert the edge in the solver +#endif + reporter->Expand(ne); + } + +#define UNDERAPPROXCORE +#ifndef UNDERAPPROXCORE + void ExpansionChoices(std::set &best){ + std::set choices; + for(std::list::iterator it = leaves.begin(), en = leaves.end(); it != en; ++it) + if (!tree->Empty(*it)) // if used in the counter-model + choices.insert(*it); + heuristic->ChooseExpand(choices, best); + } +#else +#if 0 + void ExpansionChoices(std::set &best){ + std::vector unused_set, used_set; + std::set choices; + for(std::list::iterator it = leaves.begin(), en = leaves.end(); it != en; ++it){ + Node *n = *it; + if (!tree->Empty(n)) + used_set.push_back(n); + else + unused_set.push_back(n); + } + if(tree->Check(top,unused_set) == unsat) + throw "error in ExpansionChoices"; + for(unsigned i = 0; i < used_set.size(); i++){ + Node *n = used_set[i]; + unused_set.push_back(n); + if(!top->Outgoing || tree->Check(top,unused_set) == unsat){ + unused_set.pop_back(); + choices.insert(n); + } + else + std::cout << "Using underapprox of " << n->number << std::endl; + } + heuristic->ChooseExpand(choices, best); + } +#else + void ExpansionChoicesFull(std::set &best, bool high_priority){ + std::set choices; + for(std::list::iterator it = leaves.begin(), en = leaves.end(); it != en; ++it) + if (high_priority || !tree->Empty(*it)) // if used in the counter-model + choices.insert(*it); + heuristic->ChooseExpand(choices, best, high_priority); + } + + void ExpansionChoicesRec(std::vector &unused_set, std::vector &used_set, + std::set &choices, int from, int to){ + if(from == to) return; + int orig_unused = unused_set.size(); + unused_set.resize(orig_unused + (to - from)); + std::copy(used_set.begin()+from,used_set.begin()+to,unused_set.begin()+orig_unused); + if(!top->Outgoing || tree->Check(top,unused_set) == unsat){ + unused_set.resize(orig_unused); + if(to - from == 1){ +#if 1 + std::cout << "Not using underapprox of " << used_set[from] ->number << std::endl; +#endif + choices.insert(used_set[from]); + } + else { + int mid = from + (to - from)/2; + ExpansionChoicesRec(unused_set, used_set, choices, from, mid); + ExpansionChoicesRec(unused_set, used_set, choices, mid, to); + } + } + else { +#if 1 + std::cout << "Using underapprox of "; + for(int i = from; i < to; i++){ + std::cout << used_set[i]->number << " "; + if(used_set[i]->map->Underapprox.IsEmpty()) + std::cout << "(false!) "; + } + std::cout << std::endl; +#endif + } + } + + std::set old_choices; + + void ExpansionChoices(std::set &best, bool high_priority){ + if(!underapprox || constrained){ + ExpansionChoicesFull(best, high_priority); + return; + } + std::vector unused_set, used_set; + std::set choices; + for(std::list::iterator it = leaves.begin(), en = leaves.end(); it != en; ++it){ + Node *n = *it; + if (!tree->Empty(n)){ + if(old_choices.find(n) != old_choices.end() || n->map->Underapprox.IsEmpty()) + choices.insert(n); + else + used_set.push_back(n); + } + else + unused_set.push_back(n); + } + if(tree->Check(top,unused_set) == unsat) + throw "error in ExpansionChoices"; + ExpansionChoicesRec(unused_set, used_set, choices, 0, used_set.size()); + old_choices = choices; + heuristic->ChooseExpand(choices, best, high_priority); + } +#endif +#endif + + bool ExpandSomeNodes(bool high_priority = false){ +#ifdef EFFORT_BOUNDED_STRAT + last_decs = tree->CumulativeDecisions() - start_decs; +#endif + timer_start("ExpandSomeNodes"); + timer_start("ExpansionChoices"); + std::set choices; + ExpansionChoices(choices,high_priority); + timer_stop("ExpansionChoices"); + std::list leaves_copy = leaves; // copy so can modify orig + leaves.clear(); + for(std::list::iterator it = leaves_copy.begin(), en = leaves_copy.end(); it != en; ++it){ + if(choices.find(*it) != choices.end()) + ExpandNode(*it); + else leaves.push_back(*it); + } + timer_stop("ExpandSomeNodes"); + return !choices.empty(); + } + + }; + + class Covering { + + struct cover_info { + Node *covered_by; + std::list covers; + bool dominated; + std::set dominates; + cover_info(){ + covered_by = 0; + dominated = false; + } + }; + + typedef hash_map cover_map; + cover_map cm; + Duality *parent; + bool some_updates; + + Node *&covered_by(Node *node){ + return cm[node].covered_by; + } + + std::list &covers(Node *node){ + return cm[node].covers; + } + + std::vector &insts_of_node(Node *node){ + return parent->insts_of_node[node]; + } + + Reporter *reporter(){ + return parent->reporter; + } + + std::set &dominates(Node *x){ + return cm[x].dominates; + } + + bool dominates(Node *x, Node *y){ + std::set &d = cm[x].dominates; + return d.find(y) != d.end(); + } + + bool &dominated(Node *x){ + return cm[x].dominated; + } + + public: + + Covering(Duality *_parent){ + parent = _parent; + some_updates = false; + } + + bool IsCoveredRec(hash_set &memo, Node *node){ + if(memo.find(node) != memo.end()) + return false; + memo.insert(node); + if(covered_by(node)) return true; + for(unsigned i = 0; i < node->Outgoing->Children.size(); i++) + if(IsCoveredRec(memo,node->Outgoing->Children[i])) + return true; + return false; + } + + bool IsCovered(Node *node){ + hash_set memo; + return IsCoveredRec(memo,node); + } + +#ifndef UNDERAPPROX_NODES + void RemoveCoveringsBy(Node *node){ + std::list &cs = covers(node); + for(std::list::iterator it = cs.begin(), en = cs.end(); it != en; it++){ + covered_by(*it) = 0; + reporter()->RemoveCover(*it,node); + } + cs.clear(); + } +#else + void RemoveCoveringsBy(Node *node){ + std::vector &cs = parent->all_of_node[node->map]; + for(std::vector::iterator it = cs.begin(), en = cs.end(); it != en; it++){ + Node *other = *it; + if(covered_by(other) && CoverOrder(node,other)){ + covered_by(other) = 0; + reporter()->RemoveCover(*it,node); + } + } + } +#endif + + void RemoveAscendantCoveringsRec(hash_set &memo, Node *node){ + if(memo.find(node) != memo.end()) + return; + memo.insert(node); + RemoveCoveringsBy(node); + for(std::vector::iterator it = node->Incoming.begin(), en = node->Incoming.end(); it != en; ++it) + RemoveAscendantCoveringsRec(memo,(*it)->Parent); + } + + void RemoveAscendantCoverings(Node *node){ + hash_set memo; + RemoveAscendantCoveringsRec(memo,node); + } + + bool CoverOrder(Node *covering, Node *covered){ +#ifdef UNDERAPPROX_NODES + if(parent->underapprox_map.find(covered) != parent->underapprox_map.end()) + return false; + if(parent->underapprox_map.find(covering) != parent->underapprox_map.end()) + return covering->number < covered->number || parent->underapprox_map[covering] == covered; +#endif + return covering->number < covered->number; + } + + bool CheckCover(Node *covered, Node *covering){ + return + CoverOrder(covering,covered) + && covered->Annotation.SubsetEq(covering->Annotation) + && !IsCovered(covering); + } + + bool CoverByNode(Node *covered, Node *covering){ + if(CheckCover(covered,covering)){ + covered_by(covered) = covering; + covers(covering).push_back(covered); + std::vector others; others.push_back(covering); + reporter()->AddCover(covered,others); + RemoveAscendantCoverings(covered); + return true; + } + else + return false; + } + +#ifdef UNDERAPPROX_NODES + bool CoverByAll(Node *covered){ + RPFP::Transformer all = covered->Annotation; + all.SetEmpty(); + std::vector &insts = parent->insts_of_node[covered->map]; + std::vector others; + for(unsigned i = 0; i < insts.size(); i++){ + Node *covering = insts[i]; + if(CoverOrder(covering,covered) && !IsCovered(covering)){ + others.push_back(covering); + all.UnionWith(covering->Annotation); + } + } + if(others.size() && covered->Annotation.SubsetEq(all)){ + covered_by(covered) = covered; // anything non-null will do + reporter()->AddCover(covered,others); + RemoveAscendantCoverings(covered); + return true; + } + else + return false; + } +#endif + + bool Close(Node *node){ + if(covered_by(node)) + return true; +#ifndef UNDERAPPROX_NODES + std::vector &insts = insts_of_node(node->map); + for(unsigned i = 0; i < insts.size(); i++) + if(CoverByNode(node,insts[i])) + return true; +#else + if(CoverByAll(node)) + return true; +#endif + return false; + } + + bool CloseDescendantsRec(hash_set &memo, Node *node){ + if(memo.find(node) != memo.end()) + return false; + for(unsigned i = 0; i < node->Outgoing->Children.size(); i++) + if(CloseDescendantsRec(memo,node->Outgoing->Children[i])) + return true; + if(Close(node)) + return true; + memo.insert(node); + return false; + } + + bool CloseDescendants(Node *node){ + timer_start("CloseDescendants"); + hash_set memo; + bool res = CloseDescendantsRec(memo,node); + timer_stop("CloseDescendants"); + return res; + } + + bool Contains(Node *node){ + timer_start("Contains"); + bool res = !IsCovered(node); + timer_stop("Contains"); + return res; + } + + bool Candidate(Node *node){ + timer_start("Candidate"); + bool res = !IsCovered(node) && !dominated(node); + timer_stop("Candidate"); + return res; + } + + void SetDominated(Node *node){ + dominated(node) = true; + } + + bool CouldCover(Node *covered, Node *covering){ +#ifdef UNDERAPPROX_NODES + // if(parent->underapprox_map.find(covering) != parent->underapprox_map.end()) + // return parent->underapprox_map[covering] == covered; +#endif + if(CoverOrder(covering,covered) + && !IsCovered(covering)){ + RPFP::Transformer f(covering->Annotation); f.SetEmpty(); +#if defined(TOP_DOWN) || defined(EFFORT_BOUNDED_STRAT) + if(parent->StratifiedInlining) + return true; +#endif + return !covering->Annotation.SubsetEq(f); + } + return false; + } + + bool ContainsCex(Node *node, Counterexample &cex){ + expr val = cex.tree->Eval(cex.root->Outgoing,node->Annotation.Formula); + return eq(val,parent->ctx.bool_val(true)); + } + + /** We conjecture that the annotations of similar nodes may be + true of this one. We start with later nodes, on the + principle that their annotations are likely weaker. We save + a counterexample -- if annotations of other nodes are true + in this counterexample, we don't need to check them. + */ + +#ifndef UNDERAPPROX_NODES + bool Conjecture(Node *node){ + std::vector &insts = insts_of_node(node->map); + Counterexample cex; + for(int i = insts.size() - 1; i >= 0; i--){ + Node *other = insts[i]; + if(CouldCover(node,other)){ + reporter()->Forcing(node,other); + if(cex.tree && !ContainsCex(other,cex)) + continue; + if(cex.tree) {delete cex.tree; cex.tree = 0;} + if(parent->ProveConjecture(node,other->Annotation,other,&cex)) + if(CloseDescendants(node)) + return true; + } + } + if(cex.tree) {delete cex.tree; cex.tree = 0;} + return false; + } +#else + bool Conjecture(Node *node){ + std::vector &insts = insts_of_node(node->map); + Counterexample cex; + RPFP::Transformer Bound = node->Annotation; + Bound.SetEmpty(); + bool some_other = false; + for(int i = insts.size() - 1; i >= 0; i--){ + Node *other = insts[i]; + if(CouldCover(node,other)){ + reporter()->Forcing(node,other); + Bound.UnionWith(other->Annotation); + some_other = true; + } + } + if(some_other && parent->ProveConjecture(node,Bound)){ + CloseDescendants(node); + return true; + } + return false; + } +#endif + + void Update(Node *node, const RPFP::Transformer &update){ + RemoveCoveringsBy(node); + some_updates = true; + } + +#ifndef UNDERAPPROX_NODES + Node *GetSimilarNode(Node *node){ + if(!some_updates) + return 0; + std::vector &insts = insts_of_node(node->map); + for(int i = insts.size()-1; i >= 0; i--){ + Node *other = insts[i]; + if(dominates(node,other)) + if(CoverOrder(other,node) + && !IsCovered(other)) + return other; + } + return 0; + } +#else + Node *GetSimilarNode(Node *node){ + if(!some_updates) + return 0; + std::vector &insts = insts_of_node(node->map); + for(int i = insts.size() - 1; i >= 0; i--){ + Node *other = insts[i]; + if(CoverOrder(other,node) + && !IsCovered(other)) + return other; + } + return 0; + } +#endif + + bool Dominates(Node * node, Node *other){ + if(node == other) return false; + if(other->Outgoing->map == 0) return true; + if(node->Outgoing->map == other->Outgoing->map){ + assert(node->Outgoing->Children.size() == other->Outgoing->Children.size()); + for(unsigned i = 0; i < node->Outgoing->Children.size(); i++){ + Node *nc = node->Outgoing->Children[i]; + Node *oc = other->Outgoing->Children[i]; + if(!(nc == oc || oc->Outgoing->map ==0 || dominates(nc,oc))) + return false; + } + return true; + } + return false; + } + + void Add(Node *node){ + std::vector &insts = insts_of_node(node->map); + for(unsigned i = 0; i < insts.size(); i++){ + Node *other = insts[i]; + if(Dominates(node,other)){ + cm[node].dominates.insert(other); + cm[other].dominated = true; + reporter()->Dominates(node, other); + } + } + } + + }; + + /* This expansion heuristic makes use of a previuosly obtained + counterexample as a guide. This is for use in abstraction + refinement schemes.*/ + + class ReplayHeuristic : public Heuristic { + + Counterexample &old_cex; + public: + ReplayHeuristic(RPFP *_rpfp, Counterexample &_old_cex) + : Heuristic(_rpfp), old_cex(_old_cex) + { + } + + // Maps nodes of derivation tree into old cex + hash_map cex_map; + + void ShowNodeAndChildren(Node *n){ + std::cout << n->Name.name() << ": "; + std::vector &chs = n->Outgoing->Children; + for(unsigned i = 0; i < chs.size(); i++) + std::cout << chs[i]->Name.name() << " " ; + std::cout << std::endl; + } + + virtual void ChooseExpand(const std::set &choices, std::set &best, bool high_priority){ + if(!high_priority){ + Heuristic::ChooseExpand(choices,best,false); + return; + } + // first, try to match the derivatino tree nodes to the old cex + std::set matched, unmatched; + for(std::set::iterator it = choices.begin(), en = choices.end(); it != en; ++it){ + Node *node = (*it); + if(cex_map.empty()) + cex_map[node] = old_cex.root; // match the root nodes + if(cex_map.find(node) == cex_map.end()){ // try to match an unmatched node + Node *parent = node->Incoming[0]->Parent; // assumes we are a tree! + if(cex_map.find(parent) == cex_map.end()) + throw "catastrophe in ReplayHeuristic::ChooseExpand"; + Node *old_parent = cex_map[parent]; + std::vector &chs = parent->Outgoing->Children; + if(old_parent && old_parent->Outgoing){ + std::vector &old_chs = old_parent->Outgoing->Children; + for(unsigned i = 0, j=0; i < chs.size(); i++){ + if(j < old_chs.size() && chs[i]->Name.name() == old_chs[j]->Name.name()) + cex_map[chs[i]] = old_chs[j++]; + else { + std::cout << "unmatched child: " << chs[i]->Name.name() << std::endl; + cex_map[chs[i]] = 0; + } + } + goto matching_done; + } + for(unsigned i = 0; i < chs.size(); i++) + cex_map[chs[i]] = 0; + } + matching_done: + Node *old_node = cex_map[node]; + if(!old_node) + unmatched.insert(node); + else if(old_cex.tree->Empty(old_node)) + unmatched.insert(node); + else + matched.insert(node); + } + if (matched.empty() && !high_priority) + Heuristic::ChooseExpand(unmatched,best,false); + else + Heuristic::ChooseExpand(matched,best,false); + } + }; + + + class LocalHeuristic : public Heuristic { + + RPFP::Node *old_node; + public: + LocalHeuristic(RPFP *_rpfp) + : Heuristic(_rpfp) + { + old_node = 0; + } + + void SetOldNode(RPFP::Node *_old_node){ + old_node = _old_node; + cex_map.clear(); + } + + // Maps nodes of derivation tree into old subtree + hash_map cex_map; + + virtual void ChooseExpand(const std::set &choices, std::set &best){ + if(old_node == 0){ + Heuristic::ChooseExpand(choices,best); + return; + } + // first, try to match the derivatino tree nodes to the old cex + std::set matched, unmatched; + for(std::set::iterator it = choices.begin(), en = choices.end(); it != en; ++it){ + Node *node = (*it); + if(cex_map.empty()) + cex_map[node] = old_node; // match the root nodes + if(cex_map.find(node) == cex_map.end()){ // try to match an unmatched node + Node *parent = node->Incoming[0]->Parent; // assumes we are a tree! + if(cex_map.find(parent) == cex_map.end()) + throw "catastrophe in ReplayHeuristic::ChooseExpand"; + Node *old_parent = cex_map[parent]; + std::vector &chs = parent->Outgoing->Children; + if(old_parent && old_parent->Outgoing){ + std::vector &old_chs = old_parent->Outgoing->Children; + if(chs.size() == old_chs.size()){ + for(unsigned i = 0; i < chs.size(); i++) + cex_map[chs[i]] = old_chs[i]; + goto matching_done; + } + else + std::cout << "derivation tree does not match old cex" << std::endl; + } + for(unsigned i = 0; i < chs.size(); i++) + cex_map[chs[i]] = 0; + } + matching_done: + Node *old_node = cex_map[node]; + if(!old_node) + unmatched.insert(node); + else if(old_node != node->map) + unmatched.insert(node); + else + matched.insert(node); + } + Heuristic::ChooseExpand(unmatched,best); + } + }; + + + }; + + + class StreamReporter : public Reporter { + std::ostream &s; + public: + StreamReporter(RPFP *_rpfp, std::ostream &_s) + : Reporter(_rpfp), s(_s) {event = 0;} + int event; + void ev(){ + s << "[" << event++ << "]" ; + } + virtual void Extend(RPFP::Node *node){ + ev(); s << "node " << node->number << ": " << node->Name.name(); + std::vector &rps = node->Outgoing->Children; + for(unsigned i = 0; i < rps.size(); i++) + s << " " << rps[i]->number; + s << std::endl; + } + virtual void Update(RPFP::Node *node, const RPFP::Transformer &update){ + ev(); s << "update " << node->number << " " << node->Name.name() << ": "; + rpfp->Summarize(update.Formula); + std::cout << std::endl; + } + virtual void Bound(RPFP::Node *node){ + ev(); s << "check " << node->number << std::endl; + } + virtual void Expand(RPFP::Edge *edge){ + RPFP::Node *node = edge->Parent; + ev(); s << "expand " << node->map->number << " " << node->Name.name() << std::endl; + } + virtual void AddCover(RPFP::Node *covered, std::vector &covering){ + ev(); s << "cover " << covered->Name.name() << ": " << covered->number << " by "; + for(unsigned i = 0; i < covering.size(); i++) + std::cout << covering[i]->number << " "; + std::cout << std::endl; + } + virtual void RemoveCover(RPFP::Node *covered, RPFP::Node *covering){ + ev(); s << "uncover " << covered->Name.name() << ": " << covered->number << " by " << covering->number << std::endl; + } + virtual void Forcing(RPFP::Node *covered, RPFP::Node *covering){ + ev(); s << "forcing " << covered->Name.name() << ": " << covered->number << " by " << covering->number << std::endl; + } + virtual void Conjecture(RPFP::Node *node, const RPFP::Transformer &t){ + ev(); s << "conjecture " << node->number << " " << node->Name.name() << ": "; + rpfp->Summarize(t.Formula); + std::cout << std::endl; + } + virtual void Dominates(RPFP::Node *node, RPFP::Node *other){ + ev(); s << "dominates " << node->Name.name() << ": " << node->number << " > " << other->number << std::endl; + } + virtual void InductionFailure(RPFP::Edge *edge, const std::vector &children){ + ev(); s << "induction failure: " << edge->Parent->Name.name() << ", children ="; + for(unsigned i = 0; i < children.size(); i++) + s << " " << children[i]->number; + s << std::endl; + } + virtual void UpdateUnderapprox(RPFP::Node *node, const RPFP::Transformer &update){ + ev(); s << "underapprox " << node->number << " " << node->Name.name() << ": " << update.Formula << std::endl; + } + virtual void Reject(RPFP::Edge *edge, const std::vector &children){ + ev(); s << "reject " << edge->Parent->number << " " << edge->Parent->Name.name() << ": "; + for(unsigned i = 0; i < children.size(); i++) + s << " " << children[i]->number; + s << std::endl; + } + + }; + + Solver *Solver::Create(const std::string &solver_class, RPFP *rpfp){ + Duality *s = alloc(Duality,rpfp); + return s; + } + + Reporter *CreateStdoutReporter(RPFP *rpfp){ + return new StreamReporter(rpfp, std::cout); + } +} diff --git a/src/duality/duality_wrapper.cpp b/src/duality/duality_wrapper.cpp new file mode 100644 index 000000000..e5a8e31f4 --- /dev/null +++ b/src/duality/duality_wrapper.cpp @@ -0,0 +1,523 @@ +/*++ +Copyright (c) 2012 Microsoft Corporation + +Module Name: + + wrapper.cpp + +Abstract: + + wrap various objects in the style expected by duality + +Author: + + Ken McMillan (kenmcmil) + +Revision History: + + +--*/ + +#include "duality_wrapper.h" +#include +#include "smt_solver.h" +#include "iz3interp.h" +#include "statistics.h" +#include "expr_abstract.h" + +namespace Duality { + + solver::solver(Duality::context& c) : object(c), the_model(c) { + // TODO: the following is a HACK to enable proofs in the old smt solver + // When we stop using that solver, this hack can be removed + m().toggle_proof_mode(PGM_FINE); + params_ref p; + p.set_bool("proof", true); // this is currently useless + p.set_bool("model", true); + p.set_bool("unsat_core", true); + scoped_ptr sf = mk_smt_solver_factory(); + m_solver = (*sf)(m(), p, true, true, true, ::symbol::null); + } + +expr context::constant(const std::string &name, const sort &ty){ + symbol s = str_symbol(name.c_str()); + return cook(m().mk_const(m().mk_const_decl(s, ty))); +} + +expr context::make(decl_kind op, int n, ::expr **args){ + switch(op) { + case True: return mki(m_basic_fid,OP_TRUE,n,args); + case False: return mki(m_basic_fid,OP_FALSE,n,args); + case Equal: return mki(m_basic_fid,OP_EQ,n,args); + case Distinct: return mki(m_basic_fid,OP_DISTINCT,n,args); + case Ite: return mki(m_basic_fid,OP_ITE,n,args); + case And: return mki(m_basic_fid,OP_AND,n,args); + case Or: return mki(m_basic_fid,OP_OR,n,args); + case Iff: return mki(m_basic_fid,OP_IFF,n,args); + case Xor: return mki(m_basic_fid,OP_XOR,n,args); + case Not: return mki(m_basic_fid,OP_NOT,n,args); + case Implies: return mki(m_basic_fid,OP_IMPLIES,n,args); + case Oeq: return mki(m_basic_fid,OP_OEQ,n,args); + case Interp: return mki(m_basic_fid,OP_INTERP,n,args); + case Leq: return mki(m_arith_fid,OP_LE,n,args); + case Geq: return mki(m_arith_fid,OP_GE,n,args); + case Lt: return mki(m_arith_fid,OP_LT,n,args); + case Gt: return mki(m_arith_fid,OP_GT,n,args); + case Plus: return mki(m_arith_fid,OP_ADD,n,args); + case Sub: return mki(m_arith_fid,OP_SUB,n,args); + case Uminus: return mki(m_arith_fid,OP_UMINUS,n,args); + case Times: return mki(m_arith_fid,OP_MUL,n,args); + case Div: return mki(m_arith_fid,OP_DIV,n,args); + case Idiv: return mki(m_arith_fid,OP_IDIV,n,args); + case Rem: return mki(m_arith_fid,OP_REM,n,args); + case Mod: return mki(m_arith_fid,OP_MOD,n,args); + case Power: return mki(m_arith_fid,OP_POWER,n,args); + case ToReal: return mki(m_arith_fid,OP_TO_REAL,n,args); + case ToInt: return mki(m_arith_fid,OP_TO_INT,n,args); + case IsInt: return mki(m_arith_fid,OP_IS_INT,n,args); + case Store: return mki(m_array_fid,OP_STORE,n,args); + case Select: return mki(m_array_fid,OP_SELECT,n,args); + case ConstArray: return mki(m_array_fid,OP_CONST_ARRAY,n,args); + case ArrayDefault: return mki(m_array_fid,OP_ARRAY_DEFAULT,n,args); + case ArrayMap: return mki(m_array_fid,OP_ARRAY_MAP,n,args); + case SetUnion: return mki(m_array_fid,OP_SET_UNION,n,args); + case SetIntersect: return mki(m_array_fid,OP_SET_INTERSECT,n,args); + case SetDifference: return mki(m_array_fid,OP_SET_DIFFERENCE,n,args); + case SetComplement: return mki(m_array_fid,OP_SET_COMPLEMENT,n,args); + case SetSubSet: return mki(m_array_fid,OP_SET_SUBSET,n,args); + case AsArray: return mki(m_array_fid,OP_AS_ARRAY,n,args); + default: + assert(0); + return expr(*this); + } +} + + expr context::mki(family_id fid, ::decl_kind dk, int n, ::expr **args){ + return cook(m().mk_app(fid, dk, 0, 0, n, (::expr **)args)); +} + +expr context::make(decl_kind op, const std::vector &args){ + static std::vector< ::expr*> a(10); + if(a.size() < args.size()) + a.resize(args.size()); + for(unsigned i = 0; i < args.size(); i++) + a[i] = to_expr(args[i].raw()); + return make(op,args.size(), args.size() ? &a[0] : 0); +} + +expr context::make(decl_kind op){ + return make(op,0,0); +} + +expr context::make(decl_kind op, const expr &arg0){ + ::expr *a = to_expr(arg0.raw()); + return make(op,1,&a); +} + +expr context::make(decl_kind op, const expr &arg0, const expr &arg1){ + ::expr *args[2]; + args[0] = to_expr(arg0.raw()); + args[1] = to_expr(arg1.raw()); + return make(op,2,args); +} + +expr context::make(decl_kind op, const expr &arg0, const expr &arg1, const expr &arg2){ + ::expr *args[3]; + args[0] = to_expr(arg0.raw()); + args[1] = to_expr(arg1.raw()); + args[2] = to_expr(arg2.raw()); + return make(op,3,args); +} + +expr context::make_quant(decl_kind op, const std::vector &bvs, const expr &body){ + if(bvs.size() == 0) return body; + std::vector< ::expr *> foo(bvs.size()); + + + std::vector< ::symbol> names; + std::vector< ::sort *> types; + std::vector< ::expr *> bound_asts; + unsigned num_bound = bvs.size(); + + for (unsigned i = 0; i < num_bound; ++i) { + app* a = to_app(bvs[i].raw()); + ::symbol s(to_app(a)->get_decl()->get_name()); + names.push_back(s); + types.push_back(m().get_sort(a)); + bound_asts.push_back(a); + } + expr_ref abs_body(m()); + expr_abstract(m(), 0, num_bound, &bound_asts[0], to_expr(body.raw()), abs_body); + expr_ref result(m()); + result = m().mk_quantifier( + op == Forall, + names.size(), &types[0], &names[0], abs_body.get(), + 0, + ::symbol(), + ::symbol(), + 0, 0, + 0, 0 + ); + return cook(result.get()); +} + + decl_kind func_decl::get_decl_kind() const { + return ctx().get_decl_kind(*this); + } + + decl_kind context::get_decl_kind(const func_decl &t){ + ::func_decl *d = to_func_decl(t.raw()); + if (null_family_id == d->get_family_id()) + return Uninterpreted; + // return (opr)d->get_decl_kind(); + if (m_basic_fid == d->get_family_id()) { + switch(d->get_decl_kind()) { + case OP_TRUE: return True; + case OP_FALSE: return False; + case OP_EQ: return Equal; + case OP_DISTINCT: return Distinct; + case OP_ITE: return Ite; + case OP_AND: return And; + case OP_OR: return Or; + case OP_IFF: return Iff; + case OP_XOR: return Xor; + case OP_NOT: return Not; + case OP_IMPLIES: return Implies; + case OP_OEQ: return Oeq; + case OP_INTERP: return Interp; + default: + return OtherBasic; + } + } + if (m_arith_fid == d->get_family_id()) { + switch(d->get_decl_kind()) { + case OP_LE: return Leq; + case OP_GE: return Geq; + case OP_LT: return Lt; + case OP_GT: return Gt; + case OP_ADD: return Plus; + case OP_SUB: return Sub; + case OP_UMINUS: return Uminus; + case OP_MUL: return Times; + case OP_DIV: return Div; + case OP_IDIV: return Idiv; + case OP_REM: return Rem; + case OP_MOD: return Mod; + case OP_POWER: return Power; + case OP_TO_REAL: return ToReal; + case OP_TO_INT: return ToInt; + case OP_IS_INT: return IsInt; + default: + return OtherArith; + } + } + if (m_array_fid == d->get_family_id()) { + switch(d->get_decl_kind()) { + case OP_STORE: return Store; + case OP_SELECT: return Select; + case OP_CONST_ARRAY: return ConstArray; + case OP_ARRAY_DEFAULT: return ArrayDefault; + case OP_ARRAY_MAP: return ArrayMap; + case OP_SET_UNION: return SetUnion; + case OP_SET_INTERSECT: return SetIntersect; + case OP_SET_DIFFERENCE: return SetDifference; + case OP_SET_COMPLEMENT: return SetComplement; + case OP_SET_SUBSET: return SetSubSet; + case OP_AS_ARRAY: return AsArray; + default: + return OtherArray; + } + } + + return Other; + } + + + sort_kind context::get_sort_kind(const sort &s){ + family_id fid = to_sort(s.raw())->get_family_id(); + ::decl_kind k = to_sort(s.raw())->get_decl_kind(); + if (m().is_uninterp(to_sort(s.raw()))) { + return UninterpretedSort; + } + else if (fid == m_basic_fid && k == BOOL_SORT) { + return BoolSort; + } + else if (fid == m_arith_fid && k == INT_SORT) { + return IntSort; + } + else if (fid == m_arith_fid && k == REAL_SORT) { + return RealSort; + } + else if (fid == m_array_fid && k == ARRAY_SORT) { + return ArraySort; + } + else { + return UnknownSort; + } + } + + expr func_decl::operator()(unsigned n, expr const * args) const { + std::vector< ::expr *> _args(n); + for(unsigned i = 0; i < n; i++) + _args[i] = to_expr(args[i].raw()); + return ctx().cook(m().mk_app(to_func_decl(raw()),n,&_args[0])); + } + + int solver::get_num_decisions(){ + ::statistics st; + m_solver->collect_statistics(st); + std::ostringstream ss; + st.display(ss); + std::string stats = ss.str(); + int pos = stats.find("decisions:"); + pos += 10; + int end = stats.find('\n',pos); + std::string val = stats.substr(pos,end-pos); + return atoi(val.c_str()); + } + + void context::print_expr(std::ostream &s, const ast &e){ + s << mk_pp(e.raw(), m()); + } + + + expr expr::simplify(const params &_p) const { + ::expr * a = to_expr(raw()); + params_ref p = _p.get(); + th_rewriter m_rw(m(), p); + expr_ref result(m()); + m_rw(a, result); + return ctx().cook(result); + } + + expr expr::simplify() const { + params p; + return simplify(p); + } + + expr clone_quantifier(const expr &q, const expr &b){ + return q.ctx().cook(q.m().update_quantifier(to_quantifier(q.raw()), to_expr(b.raw()))); + } + + func_decl context::fresh_func_decl(char const * prefix, const std::vector &domain, sort const & range){ + std::vector < ::sort * > _domain(domain.size()); + for(unsigned i = 0; i < domain.size(); i++) + _domain[i] = to_sort(domain[i].raw()); + ::func_decl* d = m().mk_fresh_func_decl(prefix, + _domain.size(), + &_domain[0], + to_sort(range.raw())); + return func_decl(*this,d); + } + + func_decl context::fresh_func_decl(char const * prefix, sort const & range){ + ::func_decl* d = m().mk_fresh_func_decl(prefix, + 0, + 0, + to_sort(range.raw())); + return func_decl(*this,d); + } + + + +#if 0 + + + lbool interpolating_solver::interpolate( + const std::vector &assumptions, + std::vector &interpolants, + model &model, + Z3_literals &labels, + bool incremental) + { + Z3_model _model = 0; + Z3_literals _labels = 0; + Z3_lbool lb; + std::vector _assumptions(assumptions.size()); + std::vector _interpolants(assumptions.size()-1); + for(unsigned i = 0; i < assumptions.size(); i++) + _assumptions[i] = assumptions[i]; + std::vector _theory(theory.size()); + for(unsigned i = 0; i < theory.size(); i++) + _theory[i] = theory[i]; + + lb = Z3_interpolate( + ctx(), + _assumptions.size(), + &_assumptions[0], + 0, + 0, + &_interpolants[0], + &_model, + &_labels, + incremental, + _theory.size(), + &_theory[0] + ); + + if(lb == Z3_L_FALSE){ + interpolants.resize(_interpolants.size()); + for (unsigned i = 0; i < _interpolants.size(); ++i) { + interpolants[i] = expr(ctx(),_interpolants[i]); + } + } + + if (_model) { + model = iz3wrapper::model(ctx(), _model); + } + + if(_labels){ + labels = _labels; + } + + return lb; + } + +#endif + + static int linearize_assumptions(int num, + TermTree *assumptions, + std::vector &linear_assumptions, + std::vector &parents){ + for(unsigned i = 0; i < assumptions->getChildren().size(); i++) + num = linearize_assumptions(num, assumptions->getChildren()[i], linear_assumptions, parents); + linear_assumptions[num] = assumptions->getTerm(); + for(unsigned i = 0; i < assumptions->getChildren().size(); i++) + parents[assumptions->getChildren()[i]->getNumber()] = num; + parents[num] = SHRT_MAX; // in case we have no parent + linear_assumptions[num] = assumptions->getTerm(); + return num + 1; + } + + static int unlinearize_interpolants(int num, + TermTree* assumptions, + const std::vector &interpolant, + TermTree * &tree_interpolant) + { + std::vector chs(assumptions->getChildren().size()); + for(unsigned i = 0; i < assumptions->getChildren().size(); i++) + num = unlinearize_interpolants(num, assumptions->getChildren()[i], interpolant,chs[i]); + expr f; + if(num < (int)interpolant.size()) // last interpolant is missing, presumed false + f = interpolant[num]; + tree_interpolant = new TermTree(f,chs); + return num + 1; + } + + + lbool interpolating_solver::interpolate_tree(TermTree *assumptions, + TermTree *&interpolant, + model &model, + literals &labels, + bool incremental + ) + + { + int size = assumptions->number(0); + std::vector linear_assumptions(size); + std::vector parents(size); + linearize_assumptions(0,assumptions,linear_assumptions,parents); + + ptr_vector< ::ast> _interpolants(size-1); + ptr_vector< ::ast>_assumptions(size); + for(int i = 0; i < size; i++) + _assumptions[i] = linear_assumptions[i]; + ::vector _parents(parents.size()); + for(unsigned i = 0; i < parents.size(); i++) + _parents[i] = parents[i]; + ptr_vector< ::ast> _theory(theory.size()); + for(unsigned i = 0; i < theory.size(); i++) + _theory[i] = theory[i]; + + push(); + + if(!incremental){ + for(unsigned i = 0; i < linear_assumptions.size(); i++) + add(linear_assumptions[i]); + } + + check_result res = check(); + + if(res == unsat){ + + // TODO +#if 0 + if(weak_mode) + Z3_set_interpolation_option(options,"weak","1"); +#endif + + ::ast *proof = m_solver->get_proof(); + iz3interpolate(m(),proof,_assumptions,_parents,_interpolants,_theory,0); + + std::vector linearized_interpolants(_interpolants.size()); + for(unsigned i = 0; i < _interpolants.size(); i++) + linearized_interpolants[i] = expr(ctx(),_interpolants[i]); + + unlinearize_interpolants(0,assumptions,linearized_interpolants,interpolant); + interpolant->setTerm(ctx().bool_val(false)); + } + + model_ref _m; + m_solver->get_model(_m); + model = Duality::model(ctx(),_m.get()); + +#if 0 + if(_labels){ + labels = _labels; + } +#endif + + pop(); + + return (res == unsat) ? l_false : ((res == sat) ? l_true : l_undef); + + } + + + void interpolating_solver::SetWeakInterpolants(bool weak){ + weak_mode = weak; + } + + + void interpolating_solver::SetPrintToFile(const std::string &filename){ + print_filename = filename; + } + + void interpolating_solver::AssertInterpolationAxiom(const expr & t){ + add(t); + theory.push_back(t); + } + + + void interpolating_solver::RemoveInterpolationAxiom(const expr & t){ + // theory.remove(t); + } + + + const char *interpolating_solver::profile(){ + // return Z3_interpolation_profile(ctx()); + return ""; + } + + + void ast::show() const{ + std::cout << mk_pp(raw(), m()) << std::endl; + } + +#if 0 + void model::show() const { + std::cout << Z3_model_to_string(ctx(), m_model) << std::endl; + } + + Z3_ast ast_to_track = 0; +#endif + + void include_ast_show(ast &a){ + a.show(); + } + +} + + + + diff --git a/src/duality/duality_wrapper.h b/src/duality/duality_wrapper.h new file mode 100755 index 000000000..0afad2df9 --- /dev/null +++ b/src/duality/duality_wrapper.h @@ -0,0 +1,1343 @@ +/*++ +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"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" + +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); } + + 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); + + + decl_kind get_decl_kind(const func_decl &t); + + sort_kind get_sort_kind(const sort &s); + + 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()(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_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;} + + // 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 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 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 expr(a.ctx(),a.m().mk_app(a.m().get_basic_family_id(),OP_DIV,a,b)); + } + + friend expr operator-(expr const & a) { + return 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 expr(a.ctx(),a.m().mk_app(a.m().get_basic_family_id(),OP_SUB,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_LE,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_GE,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_LT,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_GT,a,b)); + } + + expr simplify() const; + + expr simplify(params const & p) const; + + friend expr clone_quantifier(const expr &, const expr &); + + friend std::ostream & operator<<(std::ostream & out, expr const & m){ + m.ctx().print_expr(out,m); + return out; + } + + 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); + + }; + + +#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; + } + + expr eval(expr const & n, bool model_completion=false) const { + ::model * _m = m_model.get(); + expr_ref result(ctx().m()); + _m->eval(n, result, model_completion); + return expr(ctx(), result); + } + + void show() const; + + unsigned num_consts() const; + unsigned num_funcs() const; + func_decl get_const_decl(unsigned i) const; + func_decl get_func_decl(unsigned i) const; + 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; + public: + solver(context & c); + solver(context & c, ::solver *s):object(c),the_model(c) { m_solver = s; } + solver(solver const & s):object(s), the_model(s.the_model) { m_solver = s.m_solver;} + ~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; + return *this; + } + // void set(params const & p) { Z3_solver_set_params(ctx(), m_solver, p); check_error(); } + void push() { m_solver->push(); } + void pop(unsigned n = 1) { m_solver->pop(n); } + // void reset() { Z3_solver_reset(ctx(), m_solver); check_error(); } + void add(expr const & e) { m_solver->assert_expr(e); } + check_result check() { + 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) { + 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) { + 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) { + 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(); + + }; + +#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()(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 &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 setChildren(const std::vector & _children){ + children = _children; + } + + inline void setNumber(int _num){ + num = _num; + } + + private: + expr term; + std::vector children; + int num; + }; + + typedef context interpolating_context; + + class interpolating_solver : public solver { + public: + interpolating_solver(context &ctx) + : solver(ctx) + { + 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 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()); + } + + +}; + +// 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 hashable in windows +#ifdef WIN32 +template <> inline +size_t stdext::hash_value(const Duality::ast& s) +{ + return s.raw()->get_id(); +} +#endif + +// 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(); // 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 hashable in windows +#ifdef WIN32 +template <> inline +size_t stdext::hash_value(const Duality::func_decl& s) +{ + return s.raw()->get_id(); +} +#endif + +// 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(); // s.raw()->get_id() < t.raw()->get_id(); + } + }; +} + + +#endif + diff --git a/src/interp/iz3mgr.h b/src/interp/iz3mgr.h index e948e9ceb..4ae345319 100644 --- a/src/interp/iz3mgr.h +++ b/src/interp/iz3mgr.h @@ -110,6 +110,7 @@ class ast_r : public ast_i { _m->dec_ref(_ast); } + ast_manager *mgr() const {return _m;} }; diff --git a/src/muz_qe/dl_context.cpp b/src/muz_qe/dl_context.cpp index 7c9d2c965..931a96ced 100644 --- a/src/muz_qe/dl_context.cpp +++ b/src/muz_qe/dl_context.cpp @@ -731,6 +731,10 @@ namespace datalog { check_existential_tail(r); check_positive_predicates(r); break; + case DUALITY_ENGINE: + check_existential_tail(r); + check_positive_predicates(r); + break; default: UNREACHABLE(); break; @@ -989,6 +993,9 @@ namespace datalog { else if (e == symbol("tab")) { m_engine = TAB_ENGINE; } + else if (e == symbol("duality")) { + m_engine = DUALITY_ENGINE; + } if (m_engine == LAST_ENGINE) { expr_fast_mark1 mark; @@ -1024,6 +1031,8 @@ namespace datalog { return bmc_query(query); case TAB_ENGINE: return tab_query(query); + case DUALITY_ENGINE: + return duality_query(query); default: UNREACHABLE(); return rel_query(query); @@ -1042,6 +1051,9 @@ namespace datalog { case QPDR_ENGINE: ensure_pdr(); return m_pdr->get_model(); + case DUALITY_ENGINE: + ensure_duality(); + return m_duality->get_model(); default: return model_ref(alloc(model, m)); } @@ -1053,6 +1065,9 @@ namespace datalog { case QPDR_ENGINE: ensure_pdr(); return m_pdr->get_proof(); + case DUALITY_ENGINE: + ensure_duality(); + return m_duality->get_proof(); default: return proof_ref(m.mk_asserted(m.mk_true()), m); } @@ -1064,11 +1079,22 @@ namespace datalog { } } + void context::ensure_duality() { + if (!m_duality.get()) { + m_duality = alloc(Duality::dl_interface, *this); + } + } + lbool context::pdr_query(expr* query) { ensure_pdr(); return m_pdr->query(query); } + lbool context::duality_query(expr* query) { + ensure_duality(); + return m_duality->query(query); + } + void context::ensure_bmc() { if (!m_bmc.get()) { m_bmc = alloc(bmc, *this); @@ -1131,6 +1157,10 @@ namespace datalog { ensure_tab(); m_last_answer = m_tab->get_answer(); return m_last_answer.get(); + case DUALITY_ENGINE: + ensure_duality(); + m_last_answer = m_duality->get_answer(); + return m_last_answer.get(); default: UNREACHABLE(); } @@ -1155,6 +1185,8 @@ namespace datalog { ensure_tab(); m_tab->display_certificate(out); return true; + case DUALITY_ENGINE: + return false; default: return false; } diff --git a/src/muz_qe/dl_context.h b/src/muz_qe/dl_context.h index 98380c9c8..c9d0bec77 100644 --- a/src/muz_qe/dl_context.h +++ b/src/muz_qe/dl_context.h @@ -36,6 +36,7 @@ Revision History: #include"pdr_dl_interface.h" #include"dl_bmc_engine.h" #include"tab_context.h" +#include"duality_dl_interface.h" #include"rel_context.h" #include"lbool.h" #include"statistics.h" @@ -102,6 +103,7 @@ namespace datalog { scoped_ptr m_bmc; scoped_ptr m_rel; scoped_ptr m_tab; + scoped_ptr m_duality; bool m_closed; bool m_saturation_was_run; @@ -373,14 +375,16 @@ namespace datalog { /** \brief retrieve model from inductive invariant that shows query is unsat. - \pre engine == 'pdr' - this option is only supported for PDR mode. + \pre engine == 'pdr' || engine == 'duality' - this option is only supported + for PDR mode and Duality mode. */ model_ref get_model(); /** \brief retrieve proof from derivation of the query. - \pre engine == 'pdr' - this option is only supported for PDR mode. + \pre engine == 'pdr' || engine == 'duality'- this option is only supported + for PDR mode and Duality mode. */ proof_ref get_proof(); @@ -438,6 +442,8 @@ namespace datalog { void ensure_tab(); + void ensure_duality(); + void ensure_rel(); void new_query(); @@ -450,6 +456,8 @@ namespace datalog { lbool tab_query(expr* query); + lbool duality_query(expr* query); + void check_quantifier_free(rule_ref& r); void check_uninterpreted_free(rule_ref& r); void check_existential_tail(rule_ref& r); diff --git a/src/muz_qe/dl_util.h b/src/muz_qe/dl_util.h index 69be7e9ac..61f85a691 100644 --- a/src/muz_qe/dl_util.h +++ b/src/muz_qe/dl_util.h @@ -53,6 +53,7 @@ namespace datalog { BMC_ENGINE, QBMC_ENGINE, TAB_ENGINE, + DUALITY_ENGINE, LAST_ENGINE };