From 8f1a235f006bb106ea8943f647b615aeff94ea78 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 27 Dec 2013 14:50:04 -0800
Subject: [PATCH] add app.config

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 .../msf/SolverFoundation.Plugin.Z3/App.config | 60 +++++++++++++
 src/smt/theory_pb.cpp                         | 87 +++++++++++++++++++
 2 files changed, 147 insertions(+)
 create mode 100644 examples/msf/SolverFoundation.Plugin.Z3/App.config

diff --git a/examples/msf/SolverFoundation.Plugin.Z3/App.config b/examples/msf/SolverFoundation.Plugin.Z3/App.config
new file mode 100644
index 000000000..75e2872f1
--- /dev/null
+++ b/examples/msf/SolverFoundation.Plugin.Z3/App.config
@@ -0,0 +1,60 @@
+<?xml version="1.0"?>
+<configuration>
+  <configSections>
+    <section name="MsfConfig" 
+             type="Microsoft.SolverFoundation.Services.MsfConfigSection, Microsoft.Solver.Foundation" 
+             allowLocation="true" 
+             allowDefinition="Everywhere" 
+             allowExeDefinition="MachineToApplication" 
+             restartOnExternalChanges="true" 
+             requirePermission="true"/>
+  </configSections>
+  <MsfConfig>
+    <MsfPluginSolvers>      
+      <MsfPluginSolver name="Microsoft Z3 MILP Solver" 
+                       capability="MILP" 
+                       assembly="SolverFoundation.Plugin.Z3.dll" 
+                       solverclass="Microsoft.SolverFoundation.Plugin.Z3.Z3MILPSolver" 
+                       directiveclass="Microsoft.SolverFoundation.Plugin.Z3.Z3MILPDirective" 
+                       parameterclass="Microsoft.SolverFoundation.Plugin.Z3.Z3MILPParams"/>
+      <MsfPluginSolver name="Microsoft Z3 MILP Solver" 
+                       capability="LP" 
+                       assembly="SolverFoundation.Plugin.Z3.dll" 
+                       solverclass="Microsoft.SolverFoundation.Plugin.Z3.Z3MILPSolver" 
+                       directiveclass="Microsoft.SolverFoundation.Plugin.Z3.Z3MILPDirective" 
+                       parameterclass="Microsoft.SolverFoundation.Plugin.Z3.Z3MILPParams"/>
+      
+      <MsfPluginSolver name="Microsoft Z3 Term Solver" 
+                       capability="MILP" 
+                       assembly="SolverFoundation.Plugin.Z3.dll" 
+                       interface="Microsoft.SolverFoundation.Services.ITermSolver"
+                       solverclass="Microsoft.SolverFoundation.Plugin.Z3.Z3TermSolver" 
+                       directiveclass="Microsoft.SolverFoundation.Plugin.Z3.Z3TermDirective" 
+                       parameterclass="Microsoft.SolverFoundation.Plugin.Z3.Z3TermParams"/>
+      <MsfPluginSolver name="Microsoft Z3 Term Solver" 
+                       capability="LP"                        
+                       assembly="SolverFoundation.Plugin.Z3.dll" 
+                       interface="Microsoft.SolverFoundation.Services.ITermSolver"
+                       solverclass="Microsoft.SolverFoundation.Plugin.Z3.Z3TermSolver"
+                       directiveclass="Microsoft.SolverFoundation.Plugin.Z3.Z3TermDirective"
+                       parameterclass="Microsoft.SolverFoundation.Plugin.Z3.Z3TermParams"/>
+      <MsfPluginSolver name="Microsoft Z3 Term Solver"
+                       capability="MINLP"
+                       assembly="SolverFoundation.Plugin.Z3.dll"
+                       interface="Microsoft.SolverFoundation.Services.ITermSolver"
+                       solverclass="Microsoft.SolverFoundation.Plugin.Z3.Z3TermSolver"
+                       directiveclass="Microsoft.SolverFoundation.Plugin.Z3.Z3TermDirective"
+                       parameterclass="Microsoft.SolverFoundation.Plugin.Z3.Z3TermParams"/>
+      <MsfPluginSolver name="Microsoft Z3 Term Solver"
+                       capability="NLP"
+                       assembly="SolverFoundation.Plugin.Z3.dll"
+                       interface="Microsoft.SolverFoundation.Services.ITermSolver"
+                       solverclass="Microsoft.SolverFoundation.Plugin.Z3.Z3TermSolver"
+                       directiveclass="Microsoft.SolverFoundation.Plugin.Z3.Z3TermDirective"
+                       parameterclass="Microsoft.SolverFoundation.Plugin.Z3.Z3TermParams"/>
+    </MsfPluginSolvers>
+  </MsfConfig>
+<startup>
+  <supportedRuntime version="v4.0" sku=".NETFramework,Version=v4.0"/>
+</startup>
+</configuration>
diff --git a/src/smt/theory_pb.cpp b/src/smt/theory_pb.cpp
index c04390ea8..992b7fc4e 100644
--- a/src/smt/theory_pb.cpp
+++ b/src/smt/theory_pb.cpp
@@ -28,6 +28,93 @@ Notes:
 
 namespace smt {
 
+#if 0
+    // parametric sorting network
+    class psort_nw {
+        ast_manager& m;
+        context&     ctx;
+        enum cmp_t { LE, GE, EQ };
+    public:
+        psort_nw(ast_manager& m, context& c): 
+            m(m), ctx(c) {}
+        
+        void cmp_ge(literal x1, literal x2, literal y1, literal y2) {
+            add_clause(~y2, x1);
+            add_clause(~y2, x2);
+            add_clause(x1, x2, ~y1);            
+        }
+
+        void cmp_le(literal x1, literal x2, literal y1, literal y2) {
+            add_clause(~x1, y1);
+            add_clause(~x2, y1);
+            add_clause(~x1, ~x2, y2);
+        }
+
+        void cmp_eq(literal x1, literal x2, literal y1, literal y2) {
+            cmp_ge(x1, x2, y1, y2);
+            cmp_le(x1, x2, y1, y2);
+        }
+
+        void cmp(cmp_t t, literal x1, literal x2, literal y1, literal y2) {
+            switch(t) {
+            case LE: cmp_le(x1, x2, y1, y2); break;
+            case GE: cmp_ge(x1, x2, y1, y2); break;
+            case EQ: cmp_eq(x1, x2, y1, y2); break;
+            }
+        }
+
+        void merge(cmp_t t,
+                   unsigned a, literal const* as, 
+                   unsigned b, literal const* bs,                    
+                   literal_vector& out) {
+            if (a == 1 && b == 1) {
+                y1 = fresh();
+                y2 = fresh();
+                out.push_back(y1);
+                out.push_back(y2);
+                cmp(t, as[0], bs[0], y1, y2);
+            }
+            else if (a == 0) {
+                out.append(b, bs);
+            }
+            else if (even(a) && even(b) && b > 0) {
+                
+            }
+            else if (even(a) && odd(b) && (a > 1 || b > 1)) {
+
+            }
+            else if (odd(a) && odd(b) && (a > 1 || b > 1)) {
+                
+            }
+            else {
+                merge(t, b, bs, a, as, out);
+            }
+        }
+
+        
+        void sorting(cmp_t t, unsigned n, literal const* xs, 
+                     literal_vector& out) {
+            if (n == 0) {
+                // no-op
+            }
+            else if (n == 1) {
+                out.push_back(xs[0]);
+            }
+            else {
+                literal_vector out1, out2;
+                unsigned l = n/2;  // TBD
+                sorting(t, l, xs, out1);
+                sorting(t, n-l, xs+l, out2);
+                merge(t, 
+                      out1.size(), out1.c_ptr(), 
+                      out2.size(), out2.c_ptr(),
+                      out);                
+            }
+        }
+
+        void smerge(cmp_t t, );
+    };
+#endif
     class pb_lit_rewriter_util {
     public:
         typedef std::pair<literal, rational> arg_t;