summaryrefslogtreecommitdiff
path: root/Source/VCGeneration/RPFP.cs
diff options
context:
space:
mode:
Diffstat (limited to 'Source/VCGeneration/RPFP.cs')
-rw-r--r--Source/VCGeneration/RPFP.cs1218
1 files changed, 609 insertions, 609 deletions
diff --git a/Source/VCGeneration/RPFP.cs b/Source/VCGeneration/RPFP.cs
index ed3842d5..9d38eb47 100644
--- a/Source/VCGeneration/RPFP.cs
+++ b/Source/VCGeneration/RPFP.cs
@@ -1,609 +1,609 @@
-//-----------------------------------------------------------------------------
-//
-// Copyright (C) 2012 Microsoft Corporation. All Rights Reserved.
-//
-//-----------------------------------------------------------------------------
-
-using System;
-using System.Collections.Generic;
-using System.Linq;
-using System.Text;
-
-using Term = Microsoft.Boogie.VCExprAST.VCExpr;
-using FuncDecl = Microsoft.Boogie.VCExprAST.VCExprOp;
-using Sort = Microsoft.Boogie.Type;
-using Microsoft.Boogie.VCExprAST;
-
-
-using Microsoft.Boogie.ExprExtensions;
-
-
-namespace Microsoft.Boogie
-{
-
-
-
-
- /** 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.
- *
- * */
- public class RPFP
- {
- /** Symbolic representation of a relational transformer */
- public class Transformer
- {
- public FuncDecl[] RelParams;
- public Term[] IndParams;
- public Term Formula;
- public RPFP owner;
-
- public Transformer Clone()
- {
- return (Transformer)this.MemberwiseClone();
- }
- }
-
- /** Create a symbolic transformer. */
- public Transformer CreateTransformer(FuncDecl[] _RelParams, Term[] _IndParams, Term _Formula)
- {
- Transformer t = new Transformer();
- t.RelParams = _RelParams;
- t.IndParams = _IndParams;
- t.Formula = _Formula;
- t.owner = this;
- return t;
- }
-
- /** Create a relation (nullary relational transformer) */
- public Transformer CreateRelation(Term[] _IndParams, Term _Formula)
- {
- return CreateTransformer(new FuncDecl[0], _IndParams, _Formula);
- }
-
- /** A node in the RPFP graph */
- public class Node
- {
- public FuncDecl Name;
- public Transformer Annotation;
- public Transformer Bound;
- public RPFP owner;
- public int number;
- public Edge Outgoing;
- public List<Edge> Incoming;
- public Term dual;
- public Node map;
- }
-
- /** 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. */
-
- public Node CreateNode(Term t)
- {
- Node n = new Node();
- // Microsoft.Boogie.VCExprAST.VCExprNAry tn = t as Microsoft.Boogie.VCExprAST.VCExprNAry;
- // Term[] _IndParams = tn.ToArray();
- Term[] _IndParams = t.GetAppArgs();
- FuncDecl Name = t.GetAppDecl();
- n.Annotation = CreateRelation(_IndParams,ctx.MkTrue());
- n.Bound = CreateRelation(_IndParams, ctx.MkTrue());
- n.owner = this;
- n.number = ++nodeCount;
- n.Name = Name; // just to have a unique name
- n.Incoming = new List<Edge>();
- return n;
- }
-
- /** Clone a node (can be from another graph). */
-
- public Node CloneNode(Node old)
- {
- Node n = new Node();
- n.Annotation = old.Annotation.Clone();
- n.Bound = old.Bound.Clone();
- n.owner = this;
- n.number = ++nodeCount;
- n.Name = old.Name; // just to have a unique name
- n.Incoming = new List<Edge>();
- return n;
- }
-
- /** This class represents a hyper-edge in the RPFP graph */
-
- public class Edge
- {
- public Transformer F;
- public Node Parent;
- public Node[] Children;
- public RPFP owner;
- public int number;
- public Edge map;
- public HashSet<string> labels;
- internal Term dual;
- internal TermDict<Term> valuation;
- }
-
-
- /** Create a hyper-edge. */
- public Edge CreateEdge(Node _Parent, Transformer _F, Node[] _Children)
- {
- Edge e = new Edge();
- e.Parent = _Parent;
- e.F = _F;
- e.Children = _Children;
- e.owner = this;
- e.number = ++edgeCount;
- _Parent.Outgoing = e;
- foreach (var c in _Children)
- if(c != null)
- c.Incoming.Add(e);
- return e;
- }
-
- /** Create an edge that lower-bounds its parent. */
- public Edge CreateLowerBoundEdge(Node _Parent)
- {
- return CreateEdge(_Parent, _Parent.Annotation, new RPFP.Node[0]);
- }
-
-
-
-
- /** 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. */
-
- public void AssertAxiom(Term t)
- {
- ctx.AddAxiom(t);
- }
-
- /** Do not call this. */
-
- public void RemoveAxiom(Term t)
- {
- ctx.RemoveAxiom(t);
- }
-
- /** Type of solve results */
- public enum LBool { False, True, Undef };
-
-
- /** 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
- *
- *
- */
-
- public LBool Solve(Node root, int persist)
- {
- return LBool.False; // TODO
- }
-
-
- /** Dispose of the dual model (counterexample) if there is one. */
-
- public void DisposeDualModel()
- {
- // TODO dualModel = null;
- }
-
-
- /** Determines the value in the counterexample of a symbol occuring in the transformer formula of
- * a given edge. */
-
- public Term Eval(Edge e, Term t)
- {
- if (e.valuation == null)
- e.valuation = new TermDict< Term>();
- if (e.valuation.ContainsKey(t))
- return e.valuation[t];
- return null; // TODO
- }
-
- /** Sets the value in the counterexample of a symbol occuring in the transformer formula of
- * a given edge. */
-
- public void SetValue(Edge e, Term variable, Term value)
- {
- if (e.valuation == null)
- e.valuation = new TermDict< Term>();
- e.valuation.Add(variable, value);
- }
-
-
- /** 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. */
-
- public bool Empty(Node p)
- {
- return false; // TODO
- }
-
- /** Push a scope. Assertions made after Push can be undone by Pop. */
-
- public void Push()
- {
- stack.Push(new stack_entry());
- // TODO: do we need push/pop?
- }
-
- /** Pop a scope (see Push). Note, you cannot pop axioms. */
-
- public void Pop(int num_scopes)
- {
- //TODO ctx.Pop((uint)num_scopes);
- for (uint i = 0; i < num_scopes; i++)
- {
- stack_entry back = stack.Pop();
- foreach (var e in back.edges)
- e.dual = null;
- foreach (var n in back.nodes)
- n.dual = null;
- }
- }
-
- public Context ctx;
-
- public class LogicSolver {
- public Context ctx;
- };
-
- public LogicSolver solver;
-
- static public LogicSolver CreateLogicSolver(Context _ctx){
- LogicSolver res = new LogicSolver();
- res.ctx = _ctx;
- return res;
- }
-
- /** This represents a conjecture that a given node is upper-boudned
- by bound. */
- public class Conjecture
- {
- public Node node;
- public Transformer bound;
- }
-
- /** This is a list of conjectures generated during solving. */
-
- public List<Conjecture> conjectures = new List<Conjecture>();
-
- /** 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.
- */
-
- public RPFP(LogicSolver slvr)
- {
- solver = slvr;
- ctx = slvr.ctx;
- stack = new Stack<stack_entry>();
- stack.Push(new stack_entry());
- }
-
-
- /** Convert an array of clauses to an RPFP.
- */
-
- public void FromClauses(Term[] clauses){
- FuncDecl failName = ctx.MkFuncDecl("@Fail", ctx.MkBoolSort());
- foreach(var clause in clauses){
- Node foo = GetNodeFromClause(clause,failName);
- if(foo != null)
- nodes.Add(foo);
- }
- foreach (var clause in clauses)
- edges.Add(GetEdgeFromClause(clause,failName));
- }
-
-
- // This returns a new FuncDel with same sort as top-level function
- // of term t, but with numeric suffix appended to name.
-
- private FuncDecl SuffixFuncDecl(Term t, int n)
- {
- var name = t.GetAppDecl().GetDeclName() + "_" + n.ToString();
- return ctx.MkFuncDecl(name, t.GetAppDecl());
- }
-
- // Collect the relational paremeters
-
- Dictionary<FuncDecl, Node> relationToNode = new Dictionary<FuncDecl, Node>();
-
- private Term CollectParamsRec(TermDict<Term> memo, Term t, List<FuncDecl> parms, List<RPFP.Node> nodes, Dictionary<Term, Term> done)
- {
- Term res;
- if (memo.TryGetValue(t, out res))
- return res;
- if (t.GetKind() == TermKind.App)
- {
- var f = t.GetAppDecl();
- Node node;
- if (relationToNode.TryGetValue(f, out node))
- {
- if (done.ContainsKey(t))
- res = done[t];
- else
- {
- f = SuffixFuncDecl(t, parms.Count);
- parms.Add(f);
- nodes.Add(node);
- done.Add(t,res); // don't count same expression twice!
- }
- }
- var args = t.GetAppArgs();
- args = args.Select(x => CollectParamsRec(memo, x, parms, nodes, done)).ToArray();
- res = ctx.CloneApp(t, args);
- } // TODO: handle quantifiers
- else
- res = t;
- memo.Add(t, res);
- return res;
- }
-
- private bool IsVariable(Term t)
- {
- // TODO: is this right?
- // return t.IsFunctionApp() && t.GetAppArgs().Length == 0;
- return t is VCExprVar && !(t is VCExprConstant);
- }
-
- private Edge GetEdgeFromClause(Term t, FuncDecl failName)
- {
- Term[] args = t.GetAppArgs();
- Term body = args[0];
- Term head = args[1];
- Term[] _IndParams;
- FuncDecl Name;
- if (head.IsFalse())
- {
- Name = failName;
- _IndParams = new Term[0];
- }
- else
- {
- _IndParams = head.GetAppArgs();
- Name = head.GetAppDecl();
- }
- for(int i = 0; i < _IndParams.Length; i++)
- if (!IsVariable(_IndParams[i]))
- {
- Term v = ctx.MkConst("@a" + i.ToString(), _IndParams[i].GetSort());
- body = ctx.MkAnd(body, ctx.MkEq(v, _IndParams[i]));
- _IndParams[i] = v;
- }
- var relParams = new List<FuncDecl>();
- var nodeParams = new List<RPFP.Node>();
- var memo = new TermDict< Term>();
- var done = new Dictionary<Term, Term>(); // note this hashes on equality, not reference!
- body = CollectParamsRec(memo, body, relParams, nodeParams,done);
- Transformer F = CreateTransformer(relParams.ToArray(), _IndParams, body);
- Node parent = relationToNode[Name];
- return CreateEdge(parent, F, nodeParams.ToArray());
- }
-
- private Node GetNodeFromClause(Term t, FuncDecl failName)
- {
- Term[] args = t.GetAppArgs();
- Term body = args[0];
- Term head = args[1];
- FuncDecl Name;
- Term[] _IndParams;
- bool is_query = false;
- if (head.Equals(ctx.MkFalse()))
- {
- Name = failName;
- is_query = true;
- _IndParams = new Term[0];
- }
- else
- {
- Name = head.GetAppDecl();
- _IndParams = head.GetAppArgs();
- }
- if (relationToNode.ContainsKey(Name))
- return null;
- for (int i = 0; i < _IndParams.Length; i++)
- if (!IsVariable(_IndParams[i]))
- {
- Term v = ctx.MkConst("@a" + i.ToString(), _IndParams[i].GetSort());
- _IndParams[i] = v;
- }
- Term foo = ctx.MkApp(Name, _IndParams);
- Node node = CreateNode(foo);
- relationToNode[Name] = node;
- if (is_query)
- node.Bound = CreateRelation(new Term[0], ctx.MkFalse());
- return node;
- }
-
- /////////////////////////////////////////////////////////////////////////////////////////
- // Convert RPFP to Z3 rules
- /////////////////////////////////////////////////////////////////////////////////////////
-
- /** Get the Z3 rule corresponding to an edge */
-
- public Term GetRule(Edge edge)
- {
- Dictionary<FuncDecl, FuncDecl> predSubst = new Dictionary<FuncDecl, FuncDecl>();
- for (int i = 0; i < edge.Children.Length; i++)
- predSubst.Add(edge.F.RelParams[i], edge.Children[i].Name);
- Term body = SubstPreds(predSubst, edge.F.Formula);
- Term head = ctx.MkApp(edge.Parent.Name, edge.F.IndParams);
- var rule = BindVariables(ctx.MkImplies(body, head));
- rule = ctx.Letify(rule); // put in let bindings for theorem prover
- return rule;
- }
-
- /** Get the Z3 query corresponding to the conjunction of the node bounds. */
-
- public Term GetQuery()
- {
- List<Term> conjuncts = new List<Term>();
- foreach (var node in nodes)
- {
- if (node.Bound.Formula != ctx.MkTrue())
- conjuncts.Add(ctx.MkImplies(ctx.MkApp(node.Name, node.Bound.IndParams), node.Bound.Formula));
- }
- Term query = ctx.MkNot(ctx.MkAnd(conjuncts.ToArray()));
- query = BindVariables(query,false); // bind variables existentially
- query = ctx.Letify(query); // put in let bindings for theorem prover
- return query;
- }
-
- private void CollectVariables(TermDict< bool> memo, Term t, List<Term> vars)
- {
- if (memo.ContainsKey(t))
- return;
- if (IsVariable(t))
- vars.Add(t);
- if (t.GetKind() == TermKind.App)
- {
- foreach (var s in t.GetAppArgs())
- CollectVariables(memo, s, vars);
- }
- memo.Add(t, true);
- }
-
- private Term BindVariables(Term t, bool universal = true)
- {
- TermDict< bool> memo = new TermDict<bool>();
- List<Term> vars = new List<Term>();
- CollectVariables(memo,t,vars);
- return universal ? ctx.MkForall(vars.ToArray(), t) : ctx.MkExists(vars.ToArray(), t);
- }
-
- private Term SubstPredsRec(TermDict< Term> memo, Dictionary<FuncDecl,FuncDecl> subst, Term t)
- {
- Term res;
- if (memo.TryGetValue(t, out res))
- return res;
- if (t.GetKind() == TermKind.App)
- {
- var args = t.GetAppArgs();
- args = args.Select(x => SubstPredsRec(memo,subst,x)).ToArray();
- FuncDecl nf = null;
- var f = t.GetAppDecl();
- if (subst.TryGetValue(f, out nf))
- {
- res = ctx.MkApp(nf, args);
- }
- else
- {
- res = ctx.CloneApp(t, args);
- }
- } // TODO: handle quantifiers
- else
- res = t;
- memo.Add(t, res);
- return res;
- }
-
- private Term SubstPreds(Dictionary<FuncDecl, FuncDecl> subst, Term t)
- {
- TermDict< Term> memo = new TermDict< Term>();
- return SubstPredsRec(memo, subst, t);
- }
-
- /* Everything after here is private. */
-
- private class stack_entry
- {
- public List<Edge> edges = new List<Edge>();
- public List<Node> nodes = new List<Node>();
- };
-
- /** Set the model of the background theory used in a counterexample. */
- public void SetBackgroundModel(Model m)
- {
- dualModel = m;
- }
-
- /** Set the model of the background theory used in a counterexample. */
- public Model GetBackgroundModel()
- {
- return dualModel;
- }
-
- private int nodeCount = 0;
- private int edgeCount = 0;
- private Model dualModel;
- // private LabeledLiterals dualLabels;
- private Stack<stack_entry> stack;
- public List<Node> nodes = new List<Node>();
- public List<Edge> edges = new List<Edge>();
-
-
- }
-}
+//-----------------------------------------------------------------------------
+//
+// Copyright (C) 2012 Microsoft Corporation. All Rights Reserved.
+//
+//-----------------------------------------------------------------------------
+
+using System;
+using System.Collections.Generic;
+using System.Linq;
+using System.Text;
+
+using Term = Microsoft.Boogie.VCExprAST.VCExpr;
+using FuncDecl = Microsoft.Boogie.VCExprAST.VCExprOp;
+using Sort = Microsoft.Boogie.Type;
+using Microsoft.Boogie.VCExprAST;
+
+
+using Microsoft.Boogie.ExprExtensions;
+
+
+namespace Microsoft.Boogie
+{
+
+
+
+
+ /** 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.
+ *
+ * */
+ public class RPFP
+ {
+ /** Symbolic representation of a relational transformer */
+ public class Transformer
+ {
+ public FuncDecl[] RelParams;
+ public Term[] IndParams;
+ public Term Formula;
+ public RPFP owner;
+
+ public Transformer Clone()
+ {
+ return (Transformer)this.MemberwiseClone();
+ }
+ }
+
+ /** Create a symbolic transformer. */
+ public Transformer CreateTransformer(FuncDecl[] _RelParams, Term[] _IndParams, Term _Formula)
+ {
+ Transformer t = new Transformer();
+ t.RelParams = _RelParams;
+ t.IndParams = _IndParams;
+ t.Formula = _Formula;
+ t.owner = this;
+ return t;
+ }
+
+ /** Create a relation (nullary relational transformer) */
+ public Transformer CreateRelation(Term[] _IndParams, Term _Formula)
+ {
+ return CreateTransformer(new FuncDecl[0], _IndParams, _Formula);
+ }
+
+ /** A node in the RPFP graph */
+ public class Node
+ {
+ public FuncDecl Name;
+ public Transformer Annotation;
+ public Transformer Bound;
+ public RPFP owner;
+ public int number;
+ public Edge Outgoing;
+ public List<Edge> Incoming;
+ public Term dual;
+ public Node map;
+ }
+
+ /** 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. */
+
+ public Node CreateNode(Term t)
+ {
+ Node n = new Node();
+ // Microsoft.Boogie.VCExprAST.VCExprNAry tn = t as Microsoft.Boogie.VCExprAST.VCExprNAry;
+ // Term[] _IndParams = tn.ToArray();
+ Term[] _IndParams = t.GetAppArgs();
+ FuncDecl Name = t.GetAppDecl();
+ n.Annotation = CreateRelation(_IndParams,ctx.MkTrue());
+ n.Bound = CreateRelation(_IndParams, ctx.MkTrue());
+ n.owner = this;
+ n.number = ++nodeCount;
+ n.Name = Name; // just to have a unique name
+ n.Incoming = new List<Edge>();
+ return n;
+ }
+
+ /** Clone a node (can be from another graph). */
+
+ public Node CloneNode(Node old)
+ {
+ Node n = new Node();
+ n.Annotation = old.Annotation.Clone();
+ n.Bound = old.Bound.Clone();
+ n.owner = this;
+ n.number = ++nodeCount;
+ n.Name = old.Name; // just to have a unique name
+ n.Incoming = new List<Edge>();
+ return n;
+ }
+
+ /** This class represents a hyper-edge in the RPFP graph */
+
+ public class Edge
+ {
+ public Transformer F;
+ public Node Parent;
+ public Node[] Children;
+ public RPFP owner;
+ public int number;
+ public Edge map;
+ public HashSet<string> labels;
+ internal Term dual;
+ internal TermDict<Term> valuation;
+ }
+
+
+ /** Create a hyper-edge. */
+ public Edge CreateEdge(Node _Parent, Transformer _F, Node[] _Children)
+ {
+ Edge e = new Edge();
+ e.Parent = _Parent;
+ e.F = _F;
+ e.Children = _Children;
+ e.owner = this;
+ e.number = ++edgeCount;
+ _Parent.Outgoing = e;
+ foreach (var c in _Children)
+ if(c != null)
+ c.Incoming.Add(e);
+ return e;
+ }
+
+ /** Create an edge that lower-bounds its parent. */
+ public Edge CreateLowerBoundEdge(Node _Parent)
+ {
+ return CreateEdge(_Parent, _Parent.Annotation, new RPFP.Node[0]);
+ }
+
+
+
+
+ /** 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. */
+
+ public void AssertAxiom(Term t)
+ {
+ ctx.AddAxiom(t);
+ }
+
+ /** Do not call this. */
+
+ public void RemoveAxiom(Term t)
+ {
+ ctx.RemoveAxiom(t);
+ }
+
+ /** Type of solve results */
+ public enum LBool { False, True, Undef };
+
+
+ /** 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
+ *
+ *
+ */
+
+ public LBool Solve(Node root, int persist)
+ {
+ return LBool.False; // TODO
+ }
+
+
+ /** Dispose of the dual model (counterexample) if there is one. */
+
+ public void DisposeDualModel()
+ {
+ // TODO dualModel = null;
+ }
+
+
+ /** Determines the value in the counterexample of a symbol occuring in the transformer formula of
+ * a given edge. */
+
+ public Term Eval(Edge e, Term t)
+ {
+ if (e.valuation == null)
+ e.valuation = new TermDict< Term>();
+ if (e.valuation.ContainsKey(t))
+ return e.valuation[t];
+ return null; // TODO
+ }
+
+ /** Sets the value in the counterexample of a symbol occuring in the transformer formula of
+ * a given edge. */
+
+ public void SetValue(Edge e, Term variable, Term value)
+ {
+ if (e.valuation == null)
+ e.valuation = new TermDict< Term>();
+ e.valuation.Add(variable, value);
+ }
+
+
+ /** 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. */
+
+ public bool Empty(Node p)
+ {
+ return false; // TODO
+ }
+
+ /** Push a scope. Assertions made after Push can be undone by Pop. */
+
+ public void Push()
+ {
+ stack.Push(new stack_entry());
+ // TODO: do we need push/pop?
+ }
+
+ /** Pop a scope (see Push). Note, you cannot pop axioms. */
+
+ public void Pop(int num_scopes)
+ {
+ //TODO ctx.Pop((uint)num_scopes);
+ for (uint i = 0; i < num_scopes; i++)
+ {
+ stack_entry back = stack.Pop();
+ foreach (var e in back.edges)
+ e.dual = null;
+ foreach (var n in back.nodes)
+ n.dual = null;
+ }
+ }
+
+ public Context ctx;
+
+ public class LogicSolver {
+ public Context ctx;
+ };
+
+ public LogicSolver solver;
+
+ static public LogicSolver CreateLogicSolver(Context _ctx){
+ LogicSolver res = new LogicSolver();
+ res.ctx = _ctx;
+ return res;
+ }
+
+ /** This represents a conjecture that a given node is upper-boudned
+ by bound. */
+ public class Conjecture
+ {
+ public Node node;
+ public Transformer bound;
+ }
+
+ /** This is a list of conjectures generated during solving. */
+
+ public List<Conjecture> conjectures = new List<Conjecture>();
+
+ /** 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.
+ */
+
+ public RPFP(LogicSolver slvr)
+ {
+ solver = slvr;
+ ctx = slvr.ctx;
+ stack = new Stack<stack_entry>();
+ stack.Push(new stack_entry());
+ }
+
+
+ /** Convert an array of clauses to an RPFP.
+ */
+
+ public void FromClauses(Term[] clauses){
+ FuncDecl failName = ctx.MkFuncDecl("@Fail", ctx.MkBoolSort());
+ foreach(var clause in clauses){
+ Node foo = GetNodeFromClause(clause,failName);
+ if(foo != null)
+ nodes.Add(foo);
+ }
+ foreach (var clause in clauses)
+ edges.Add(GetEdgeFromClause(clause,failName));
+ }
+
+
+ // This returns a new FuncDel with same sort as top-level function
+ // of term t, but with numeric suffix appended to name.
+
+ private FuncDecl SuffixFuncDecl(Term t, int n)
+ {
+ var name = t.GetAppDecl().GetDeclName() + "_" + n.ToString();
+ return ctx.MkFuncDecl(name, t.GetAppDecl());
+ }
+
+ // Collect the relational paremeters
+
+ Dictionary<FuncDecl, Node> relationToNode = new Dictionary<FuncDecl, Node>();
+
+ private Term CollectParamsRec(TermDict<Term> memo, Term t, List<FuncDecl> parms, List<RPFP.Node> nodes, Dictionary<Term, Term> done)
+ {
+ Term res;
+ if (memo.TryGetValue(t, out res))
+ return res;
+ if (t.GetKind() == TermKind.App)
+ {
+ var f = t.GetAppDecl();
+ Node node;
+ if (relationToNode.TryGetValue(f, out node))
+ {
+ if (done.ContainsKey(t))
+ res = done[t];
+ else
+ {
+ f = SuffixFuncDecl(t, parms.Count);
+ parms.Add(f);
+ nodes.Add(node);
+ done.Add(t,res); // don't count same expression twice!
+ }
+ }
+ var args = t.GetAppArgs();
+ args = args.Select(x => CollectParamsRec(memo, x, parms, nodes, done)).ToArray();
+ res = ctx.CloneApp(t, args);
+ } // TODO: handle quantifiers
+ else
+ res = t;
+ memo.Add(t, res);
+ return res;
+ }
+
+ private bool IsVariable(Term t)
+ {
+ // TODO: is this right?
+ // return t.IsFunctionApp() && t.GetAppArgs().Length == 0;
+ return t is VCExprVar && !(t is VCExprConstant);
+ }
+
+ private Edge GetEdgeFromClause(Term t, FuncDecl failName)
+ {
+ Term[] args = t.GetAppArgs();
+ Term body = args[0];
+ Term head = args[1];
+ Term[] _IndParams;
+ FuncDecl Name;
+ if (head.IsFalse())
+ {
+ Name = failName;
+ _IndParams = new Term[0];
+ }
+ else
+ {
+ _IndParams = head.GetAppArgs();
+ Name = head.GetAppDecl();
+ }
+ for(int i = 0; i < _IndParams.Length; i++)
+ if (!IsVariable(_IndParams[i]))
+ {
+ Term v = ctx.MkConst("@a" + i.ToString(), _IndParams[i].GetSort());
+ body = ctx.MkAnd(body, ctx.MkEq(v, _IndParams[i]));
+ _IndParams[i] = v;
+ }
+ var relParams = new List<FuncDecl>();
+ var nodeParams = new List<RPFP.Node>();
+ var memo = new TermDict< Term>();
+ var done = new Dictionary<Term, Term>(); // note this hashes on equality, not reference!
+ body = CollectParamsRec(memo, body, relParams, nodeParams,done);
+ Transformer F = CreateTransformer(relParams.ToArray(), _IndParams, body);
+ Node parent = relationToNode[Name];
+ return CreateEdge(parent, F, nodeParams.ToArray());
+ }
+
+ private Node GetNodeFromClause(Term t, FuncDecl failName)
+ {
+ Term[] args = t.GetAppArgs();
+ Term body = args[0];
+ Term head = args[1];
+ FuncDecl Name;
+ Term[] _IndParams;
+ bool is_query = false;
+ if (head.Equals(ctx.MkFalse()))
+ {
+ Name = failName;
+ is_query = true;
+ _IndParams = new Term[0];
+ }
+ else
+ {
+ Name = head.GetAppDecl();
+ _IndParams = head.GetAppArgs();
+ }
+ if (relationToNode.ContainsKey(Name))
+ return null;
+ for (int i = 0; i < _IndParams.Length; i++)
+ if (!IsVariable(_IndParams[i]))
+ {
+ Term v = ctx.MkConst("@a" + i.ToString(), _IndParams[i].GetSort());
+ _IndParams[i] = v;
+ }
+ Term foo = ctx.MkApp(Name, _IndParams);
+ Node node = CreateNode(foo);
+ relationToNode[Name] = node;
+ if (is_query)
+ node.Bound = CreateRelation(new Term[0], ctx.MkFalse());
+ return node;
+ }
+
+ /////////////////////////////////////////////////////////////////////////////////////////
+ // Convert RPFP to Z3 rules
+ /////////////////////////////////////////////////////////////////////////////////////////
+
+ /** Get the Z3 rule corresponding to an edge */
+
+ public Term GetRule(Edge edge)
+ {
+ Dictionary<FuncDecl, FuncDecl> predSubst = new Dictionary<FuncDecl, FuncDecl>();
+ for (int i = 0; i < edge.Children.Length; i++)
+ predSubst.Add(edge.F.RelParams[i], edge.Children[i].Name);
+ Term body = SubstPreds(predSubst, edge.F.Formula);
+ Term head = ctx.MkApp(edge.Parent.Name, edge.F.IndParams);
+ var rule = BindVariables(ctx.MkImplies(body, head));
+ rule = ctx.Letify(rule); // put in let bindings for theorem prover
+ return rule;
+ }
+
+ /** Get the Z3 query corresponding to the conjunction of the node bounds. */
+
+ public Term GetQuery()
+ {
+ List<Term> conjuncts = new List<Term>();
+ foreach (var node in nodes)
+ {
+ if (node.Bound.Formula != ctx.MkTrue())
+ conjuncts.Add(ctx.MkImplies(ctx.MkApp(node.Name, node.Bound.IndParams), node.Bound.Formula));
+ }
+ Term query = ctx.MkNot(ctx.MkAnd(conjuncts.ToArray()));
+ query = BindVariables(query,false); // bind variables existentially
+ query = ctx.Letify(query); // put in let bindings for theorem prover
+ return query;
+ }
+
+ private void CollectVariables(TermDict< bool> memo, Term t, List<Term> vars)
+ {
+ if (memo.ContainsKey(t))
+ return;
+ if (IsVariable(t))
+ vars.Add(t);
+ if (t.GetKind() == TermKind.App)
+ {
+ foreach (var s in t.GetAppArgs())
+ CollectVariables(memo, s, vars);
+ }
+ memo.Add(t, true);
+ }
+
+ private Term BindVariables(Term t, bool universal = true)
+ {
+ TermDict< bool> memo = new TermDict<bool>();
+ List<Term> vars = new List<Term>();
+ CollectVariables(memo,t,vars);
+ return universal ? ctx.MkForall(vars.ToArray(), t) : ctx.MkExists(vars.ToArray(), t);
+ }
+
+ private Term SubstPredsRec(TermDict< Term> memo, Dictionary<FuncDecl,FuncDecl> subst, Term t)
+ {
+ Term res;
+ if (memo.TryGetValue(t, out res))
+ return res;
+ if (t.GetKind() == TermKind.App)
+ {
+ var args = t.GetAppArgs();
+ args = args.Select(x => SubstPredsRec(memo,subst,x)).ToArray();
+ FuncDecl nf = null;
+ var f = t.GetAppDecl();
+ if (subst.TryGetValue(f, out nf))
+ {
+ res = ctx.MkApp(nf, args);
+ }
+ else
+ {
+ res = ctx.CloneApp(t, args);
+ }
+ } // TODO: handle quantifiers
+ else
+ res = t;
+ memo.Add(t, res);
+ return res;
+ }
+
+ private Term SubstPreds(Dictionary<FuncDecl, FuncDecl> subst, Term t)
+ {
+ TermDict< Term> memo = new TermDict< Term>();
+ return SubstPredsRec(memo, subst, t);
+ }
+
+ /* Everything after here is private. */
+
+ private class stack_entry
+ {
+ public List<Edge> edges = new List<Edge>();
+ public List<Node> nodes = new List<Node>();
+ };
+
+ /** Set the model of the background theory used in a counterexample. */
+ public void SetBackgroundModel(Model m)
+ {
+ dualModel = m;
+ }
+
+ /** Set the model of the background theory used in a counterexample. */
+ public Model GetBackgroundModel()
+ {
+ return dualModel;
+ }
+
+ private int nodeCount = 0;
+ private int edgeCount = 0;
+ private Model dualModel;
+ // private LabeledLiterals dualLabels;
+ private Stack<stack_entry> stack;
+ public List<Node> nodes = new List<Node>();
+ public List<Edge> edges = new List<Edge>();
+
+
+ }
+}
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-02 02:01:20 +0000