Synthesis for channels, inputs/outputs, T-junctions

examples/tjunction.smt2

@@ -0,0 +1,31 @@
+(set-logic QF_NRA)
+
+(declare-fun rho () Real)
+(declare-fun pressure_Cin () Real)
+(declare-fun flow_Cin () Real)
+(declare-fun res_Cin () Real)
+(declare-fun pressure_J () Real)
+(declare-fun flow_D () Real)
+(declare-fun flow_Ef () Real)
+(declare-fun res_Ef () Real)
+(declare-fun pressure_G () Real)
+(declare-fun flow_Eb () Real)
+(declare-fun res_Eb () Real)
+(declare-fun pressure_W () Real)
+
+(assert (= rho 0.013503)) ; rho = resistance per micrometer = 8.1016 * 10e-6 * 10000/60
+(assert (= res_Cin (* rho 100000)))
+(assert (= res_Ef (* rho 50000)))
+(assert (= res_Eb (* rho 50000)))
+;(assert (= pressure_Cin 1500.0)) ; input pressure = 1500 millibars
+(assert (= flow_Cin 7.0)) ; input flow rate = 7 uL/min
+(assert (= (- pressure_Cin pressure_J) (* res_Cin flow_Cin))) ; Pin - Pj = Rin * Qin
+(assert (= flow_D 7.0)) ; disperse flow rate = 7 uL/min
+(assert (= flow_Ef (+ flow_Cin flow_D))) ; Qin + Qd = Qef
+(assert (= (- pressure_J pressure_G) (* res_Ef flow_Ef))) ; Pj - Pg = Ref * Qef
+(assert (= flow_Ef flow_Eb)) ; Qef = Qeb
+(assert (= (- pressure_G pressure_W) (* res_Eb flow_Eb))) ; Pg - Pw = Reb * Qeb
+(assert (= pressure_W 1013.0)) ; output pressure = 1013 millibars
+
+(check-sat)
+(exit)

src/main/java/org/manifold/compiler/back/microfluidics/MicrofluidicsBackend.java

@@ -1,6 +1,10 @@
 package org.manifold.compiler.back.microfluidics;
 
+import java.io.BufferedWriter;
+import java.io.FileWriter;
 import java.io.IOException;
+import java.util.LinkedList;
+import java.util.List;
 
 import org.apache.commons.cli.CommandLine;
 import org.apache.commons.cli.Option;
@@ -9,6 +13,15 @@
 import org.apache.log4j.LogManager;
 import org.apache.log4j.Logger;
 import org.manifold.compiler.Backend;
+import org.manifold.compiler.back.microfluidics.smt2.Decimal;
+import org.manifold.compiler.back.microfluidics.smt2.ParenList;
+import org.manifold.compiler.back.microfluidics.smt2.QFNRA;
+import org.manifold.compiler.back.microfluidics.smt2.SExpression;
+import org.manifold.compiler.back.microfluidics.smt2.Symbol;
+import org.manifold.compiler.back.microfluidics.smt2.SymbolNameGenerator;
+import org.manifold.compiler.back.microfluidics.strategies.MultiPhaseStrategySet;
+import org.manifold.compiler.back.microfluidics.strategies.PlacementTranslationStrategySet;
+import org.manifold.compiler.back.microfluidics.strategies.PressureFlowStrategySet;
 import org.manifold.compiler.middle.Schematic;
 
 public class MicrofluidicsBackend implements Backend {
@@ -113,8 +126,84 @@ private static void checkTypeHierarchy(PrimitiveTypeTable typeTable) {
     }
   }
 
-  public void run(Schematic schematic) {
+  // Sort a list of unsorted expressions so that all declarations (declare-fun)
+  // come before all assertions (assert).
+  public List<SExpression> sortExprs(List<SExpression> unsorted) {
+    List<SExpression> retval = new LinkedList<>();
+    List<SExpression> decls = new LinkedList<>();
+    List<SExpression> asserts = new LinkedList<>();
+    List<SExpression> others = new LinkedList<>();
+
+    for (SExpression expr : unsorted) {
+      if (expr instanceof ParenList) {
+        ParenList list = (ParenList) expr;
+        SExpression head = list.getExprs().get(0);
+        if (head instanceof Symbol) {
+          Symbol s = (Symbol) head;
+          if (s.getName().equals("declare-fun")) {
+            decls.add(expr);
+          } else if (s.getName().equals("assert")) {
+            asserts.add(expr);
+          } else {
+            others.add(expr);
+          }
+        } else {
+          others.add(expr);
+        }
+      } else {
+        others.add(expr);
+      }
+    }
+
+    retval.addAll(decls);
+    retval.addAll(asserts);
+    retval.addAll(others);
+    return retval;
+  }
+
+  public void run(Schematic schematic) throws IOException {
     primitiveTypes = constructTypeTable(schematic);
+    // translation step
+    // for now: one pass
+    List<SExpression> exprs = new LinkedList<>();
+    exprs.add(QFNRA.useQFNRA());
+
+    List<SExpression> unsortedExprs = new LinkedList<>();
+    // define constant pi
+    unsortedExprs.add(QFNRA.declareRealVariable(
+        SymbolNameGenerator.getsym_constant_pi()));
+    unsortedExprs.add(QFNRA.assertEqual(
+        SymbolNameGenerator.getsym_constant_pi(), 
+        new Decimal(Math.PI)));
+
+    PlacementTranslationStrategySet placeSet = 
+        new PlacementTranslationStrategySet();
+    unsortedExprs.addAll(placeSet.translate(
+        schematic, processParams, primitiveTypes));
+    MultiPhaseStrategySet multiPhase = new MultiPhaseStrategySet();
+    unsortedExprs.addAll(multiPhase.translate(
+        schematic, processParams, primitiveTypes));
+    PressureFlowStrategySet pressureFlow = new PressureFlowStrategySet();
+    unsortedExprs.addAll(pressureFlow.translate(
+        schematic, processParams, primitiveTypes));
+
+    exprs.addAll(sortExprs(unsortedExprs));
+
+    // (check-sat) (exit)
+    exprs.add(new ParenList(new SExpression[] {
+      new Symbol("check-sat")
+    }));
+    exprs.add(new ParenList(new SExpression[] {
+      new Symbol("exit")
+    }));
+    // write to "schematic-name.smt2"
+    String filename = schematic.getName() + ".smt2";
+    try (BufferedWriter writer = new BufferedWriter(new FileWriter(filename))) {
+      for (SExpression expr : exprs) {
+        expr.write(writer);
+        writer.newLine();
+      }
+    }
   }
 
 }

src/main/java/org/manifold/compiler/back/microfluidics/PrimitiveTypeTable.java

@@ -15,7 +15,25 @@ public class PrimitiveTypeTable {
   public PortTypeValue getMicrofluidPortType() {
     return microfluidPortType;
   }
+
+  // multi-phase stuff
+
+  private NodeTypeValue fluidEntryNodeType = null;
+  public NodeTypeValue getFluidEntryNodeType() {
+    return fluidEntryNodeType;
+  }
+
+  private NodeTypeValue fluidExitNodeType = null;
+  public NodeTypeValue getFluidExitNodeType() {
+    return fluidExitNodeType;
+  }
 
+  private NodeTypeValue tJunctionNodeType = null;
+  public NodeTypeValue getTJunctionNodeType() {
+    return tJunctionNodeType;
+  }
+
+  // single-phase stuff, probably out of date
   private NodeTypeValue controlPointNodeType = null;
   public NodeTypeValue getControlPointNodeType() {
     return controlPointNodeType;
@@ -53,24 +71,27 @@ public void addDerivedVoltageControlPointNodeTypes(
   public NodeTypeValue getChannelCrossingNodeType() {
     return channelCrossingNodeType;
   }
-
-  private NodeTypeValue tJunctionNodeType = null;
-  public NodeTypeValue getTJunctionNodetype() {
-    return tJunctionNodeType;
-  }
 
   public void retrieveBaseTypes(Schematic schematic) {
     try {
       microfluidPortType = schematic.getPortType("microfluidPort");
+
+      // multi-phase
+      fluidEntryNodeType = 
+          schematic.getNodeType("fluidEntry");
+      fluidExitNodeType = 
+          schematic.getNodeType("fluidExit");
+      tJunctionNodeType = 
+          schematic.getNodeType("tJunction");
+
+      // single-phase
       controlPointNodeType = schematic.getNodeType("controlPoint");
       pressureControlPointNodeType = 
           schematic.getNodeType("pressureControlPoint");
       voltageControlPointNodeType = 
           schematic.getNodeType("voltageControlPoint");
       channelCrossingNodeType =
           schematic.getNodeType("channelCrossing");
-      tJunctionNodeType = 
-          schematic.getNodeType("tJunction");
     } catch (UndeclaredIdentifierException e) {
       throw new CodeGenerationError(
           "could not find required microfluidic schematic type '"
@@ -100,12 +121,19 @@ public ConstraintType getChannelPlacementConstraintType() {
     return channelPlacementConstraintType;
   }
 
+  private ConstraintType channelDropletVolumeConstraintType = null;
+  public ConstraintType getchannelDropletVolumeConstraintType() {
+    return channelDropletVolumeConstraintType;
+  }
+
   public void retrieveConstraintTypes(Schematic schematic) {
     try {
       controlPointPlacementConstraintType =
           schematic.getConstraintType("controlPointPlacementConstraint");
       channelPlacementConstraintType =
           schematic.getConstraintType("channelPlacementConstraint");
+      channelDropletVolumeConstraintType =
+          schematic.getConstraintType("channelDropletVolumeConstraint");
     } catch (UndeclaredIdentifierException e) {
       throw new CodeGenerationError(
           "could not find required microfluidic schematic constraint type '"

src/main/java/org/manifold/compiler/back/microfluidics/smt2/Macros.java

@@ -0,0 +1,70 @@
+package org.manifold.compiler.back.microfluidics.smt2;
+
+import java.util.LinkedList;
+import java.util.List;
+
+import org.manifold.compiler.ConnectionValue;
+import org.manifold.compiler.PortValue;
+import org.manifold.compiler.back.microfluidics.CodeGenerationError;
+import org.manifold.compiler.middle.Schematic;
+
+public class Macros {
+
+  //get the connection associated with this port
+  // TODO this is VERY EXPENSIVE, find an optimization
+  protected static ConnectionValue getConnection(
+     Schematic schematic, PortValue port) {
+    for (ConnectionValue conn : schematic.getConnections().values()) {
+      if (conn.getFrom().equals(port) || conn.getTo().equals(port)) {
+        return conn;
+      }
+    }
+    return null;
+  }
+
+  // generate an expression that describes the constraint
+  // "total flow in = total flow out"
+  // this is difficult because the actual flow direction may be backwards
+  // with respect to the expected direction
+  public static List<SExpression> generateConservationOfFlow(Schematic schematic,
+      List<PortValue> connectedPorts) {
+    List<SExpression> flowRatesIn = new LinkedList<SExpression>();
+    List<SExpression> flowRatesOut = new LinkedList<SExpression>();
+
+    List<SExpression> flowRatesIn_WorstCase = new LinkedList<SExpression>();
+    List<SExpression> flowRatesOut_WorstCase = new LinkedList<SExpression>();
+
+    for (PortValue port : connectedPorts) {
+      ConnectionValue channel = getConnection(schematic, port);
+      boolean connectedIntoJunction;
+      // check which way the channel is connected
+      if (channel.getFrom().equals(port)) {
+        connectedIntoJunction = false;
+      } else if (channel.getTo().equals(port)) {
+        connectedIntoJunction = true;
+      } else {
+        throw new CodeGenerationError("attempt to generate flow direction "
+            + "constraint for a channel that is disconnected from the "
+            + "target port");
+      }
+      Symbol flowRate = SymbolNameGenerator
+          .getsym_ChannelFlowRate(schematic, channel);
+      Symbol flowRate_WorstCase = SymbolNameGenerator
+          .getsym_ChannelFlowRate_WorstCase(schematic, channel);
+      if (connectedIntoJunction) {
+        // flow rate is positive into the junction
+        flowRatesIn.add(flowRate);
+        flowRatesIn_WorstCase.add(flowRate_WorstCase);
+      } else {
+        // flow rate is positive out of the junction
+        flowRatesOut.add(flowRate);
+        flowRatesOut_WorstCase.add(flowRate_WorstCase);
+      }
+    }
+    List<SExpression> exprs = new LinkedList<>();
+    exprs.add(QFNRA.assertEqual(QFNRA.add(flowRatesIn), QFNRA.add(flowRatesOut)));
+    exprs.add(QFNRA.assertEqual(QFNRA.add(flowRatesIn_WorstCase), QFNRA.add(flowRatesOut_WorstCase)));
+    return exprs;
+  }
+
+}

src/main/java/org/manifold/compiler/back/microfluidics/smt2/QFNRA.java

@@ -1,5 +1,8 @@
 package org.manifold.compiler.back.microfluidics.smt2;
 
+import java.util.LinkedList;
+import java.util.List;
+
 // Helper class for generating valid QF_NRA S-expressions.
 public class QFNRA {
 
@@ -12,10 +15,35 @@ private static SExpression infix(SExpression e1, String op, SExpression e2) {
     return new ParenList(exprs);
   }
 
+  public static SExpression useQFNRA() {
+    SExpression exprs[] = new SExpression[] {
+      new Symbol("set-logic"),
+      new Symbol("QF_NRA")
+    };
+    return new ParenList(exprs);
+  }
+
+  public static SExpression declareRealVariable(Symbol var) {
+    SExpression exprs[] = new SExpression[] {
+      new Symbol("declare-fun"),
+      var,
+      new ParenList(),
+      new Symbol("Real")
+    };
+    return new ParenList(exprs);
+  }
+
   public static SExpression add(SExpression e1, SExpression e2) {
     return infix(e1, "+", e2);
   }
 
+  public static SExpression add(List<SExpression> terms) {
+    List<SExpression> exprs = new LinkedList<SExpression>();
+    exprs.add(new Symbol("+"));
+    exprs.addAll(terms);
+    return new ParenList(exprs);
+  }
+
   public static SExpression subtract(SExpression e1, SExpression e2) {
     return infix(e1, "-", e2);
   }