CVC4
diff --git a/‎.github/ISSUE_TEMPLATE/bug_report.md‎
Lines changed: 38 additions & 0 deletions b/‎.github/ISSUE_TEMPLATE/bug_report.md‎
Lines changed: 38 additions & 0 deletions
diff --git a/‎.github/ISSUE_TEMPLATE/feature_request.md‎
Lines changed: 20 additions & 0 deletions b/‎.github/ISSUE_TEMPLATE/feature_request.md‎
Lines changed: 20 additions & 0 deletions
diff --git a/‎README.md‎
Lines changed: 5 additions & 1 deletion b/‎README.md‎
Lines changed: 5 additions & 1 deletion
diff --git a/‎SMT-Extension/.classpath‎
Lines changed: 11 additions & 0 deletions b/‎SMT-Extension/.classpath‎
Lines changed: 11 additions & 0 deletions
diff --git a/‎SMT-Extension/.project‎
Lines changed: 23 additions & 0 deletions b/‎SMT-Extension/.project‎
Lines changed: 23 additions & 0 deletions
diff --git a/‎SMT-Extension/bnd.bnd‎
Lines changed: 11 additions & 0 deletions b/‎SMT-Extension/bnd.bnd‎
Lines changed: 11 additions & 0 deletions
diff --git a/‎SMT-Extension/src/main/java/edu/uiowa/alloy2smt/Alloy2SmtLogger.java‎
Lines changed: 77 additions & 0 deletions b/‎SMT-Extension/src/main/java/edu/uiowa/alloy2smt/Alloy2SmtLogger.java‎
Lines changed: 77 additions & 0 deletions
diff --git a/‎SMT-Extension/src/main/java/edu/uiowa/alloy2smt/Main.java‎
Lines changed: 148 additions & 0 deletions b/‎SMT-Extension/src/main/java/edu/uiowa/alloy2smt/Main.java‎
Lines changed: 148 additions & 0 deletions
@@ -0,0 +1,38 @@
+---
+name: Bug report
+about: Create a report to help us improve
+title: ''
+labels: ''
+assignees: ''
+
+---
+
+**Describe the bug**
+A clear and concise description of what the bug is.
+
+**To Reproduce**
+Steps to reproduce the behavior:
+1. Go to '...'
+2. Click on '....'
+3. Scroll down to '....'
+4. See error
+
+**Expected behavior**
+A clear and concise description of what you expected to happen.
+
+**Screenshots**
+If applicable, add screenshots to help explain your problem.
+
+**Desktop (please complete the following information):**
+ - OS: [e.g. iOS]
+ - Browser [e.g. chrome, safari]
+ - Version [e.g. 22]
+
+**Smartphone (please complete the following information):**
+ - Device: [e.g. iPhone6]
+ - OS: [e.g. iOS8.1]
+ - Browser [e.g. stock browser, safari]
+ - Version [e.g. 22]
+
+**Additional context**
+Add any other context about the problem here.
@@ -0,0 +1,20 @@
+---
+name: Feature request
+about: Suggest an idea for this project
+title: ''
+labels: ''
+assignees: ''
+
+---
+
+**Is your feature request related to a problem? Please describe.**
+A clear and concise description of what the problem is. Ex. I'm always frustrated when [...]
+
+**Describe the solution you'd like**
+A clear and concise description of what you want to happen.
+
+**Describe alternatives you've considered**
+A clear and concise description of any alternative solutions or features you've considered.
+
+**Additional context**
+Add any other context or screenshots about the feature request here.
@@ -31,7 +31,11 @@ Checkout the project and type `./gradlew build`. You find the executable JAR in
      $ git clone --recursive https://github.com/AlloyTools/org.alloytools.alloy.git
      $ cd org.alloytools.alloy
      $ ./gradlew build
-     $ java -jar org.alloytools.alloy.dist/target/org.alloytools.alloy.dist.jar
+	 $ cd org.alloytools.alloy.dist
+	 $ chmod +x binaries/cvc4_linux
+	 $ cp binaries/* target
+	 $ cd target
+     $ java -jar org.alloytools.alloy.dist.jar
      # opens GUI
      
 Note: if you are behind a proxy, the call to `gradlew` is likely to fail, unless you pass it further options about the http and https proxies (and possibly your login and password on this proxy). There are several ways to pass these options, a simple one is to type (replace the `XXXXX`'s by the adequate settings):
 
@@ -0,0 +1,11 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<classpath>
+	<classpathentry kind="con" path="org.eclipse.jdt.launching.JRE_CONTAINER/org.eclipse.jdt.internal.debug.ui.launcher.StandardVMType/JavaSE-1.8">
+		<attributes>
+			<attribute name="module" value="true"/>
+		</attributes>
+	</classpathentry>
+	<classpathentry kind="con" path="aQute.bnd.classpath.container"/>
+	<classpathentry kind="src" output="target/classes" path="src/main/java"/>
+	<classpathentry kind="output" path="bin"/>
+</classpath>
@@ -0,0 +1,23 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<projectDescription>
+	<name>SMT-Extension</name>
+	<comment></comment>
+	<projects>
+	</projects>
+	<buildSpec>
+		<buildCommand>
+			<name>org.eclipse.jdt.core.javabuilder</name>
+			<arguments>
+			</arguments>
+		</buildCommand>
+		<buildCommand>
+			<name>bndtools.core.bndbuilder</name>
+			<arguments>
+			</arguments>
+		</buildCommand>
+	</buildSpec>
+	<natures>
+		<nature>org.eclipse.jdt.core.javanature</nature>
+		<nature>bndtools.core.bndnature</nature>
+	</natures>
+</projectDescription>
@@ -0,0 +1,11 @@
+-buildpath: \
+	org.apache.commons.cli,\
+	org.alloytools.alloy.core,\
+	com.fasterxml.jackson.core.jackson-annotations,\
+	com.fasterxml.jackson.core.jackson-databind,\
+	jaxb-api,\
+	com.fasterxml.jackson.core.jackson-core,\
+	org.antlr.antlr4-runtime,\
+
+-testpath:	
+	
@@ -0,0 +1,77 @@
+/*
+ * This file is part of alloy2smt.
+ * Copyright (C) 2018-2019  The University of Iowa
+ *
+ * @author Mudathir Mohamed, Paul Meng
+ *
+ */
+
+package edu.uiowa.alloy2smt;
+
+import java.util.logging.Filter;
+import java.util.logging.LogRecord;
+import java.util.logging.Logger;
+
+public class Alloy2SmtLogger implements Filter
+{
+  private final Logger LOGGER;
+
+  public Alloy2SmtLogger(String className)
+  {
+    LOGGER = Logger.getLogger(className);
+  }
+
+  public void printInfo(String info)
+  {
+    if (info != null)
+    {
+      LOGGER.info(info);
+    }
+  }
+
+  public void printWarning(String warning)
+  {
+    if (warning != null)
+    {
+      LOGGER.warning(warning);
+    }
+  }
+
+  public void printSevere(String severe)
+  {
+    if (severe != null)
+    {
+      LOGGER.warning(severe);
+    }
+  }
+
+  @Override
+  public boolean isLoggable(LogRecord record)
+  {
+    if (record == null)
+    {
+      return false;
+    }
+    return !record.getMessage().toLowerCase().startsWith("debug");
+  }
+
+  public enum LEVEL
+  {
+    INFO("info"),
+    WARNING("warning"),
+    SEVERE("severe");
+
+    private final String levelStr;
+
+    private LEVEL(String level)
+    {
+      this.levelStr = level;
+    }
+
+    @Override
+    public String toString()
+    {
+      return this.levelStr;
+    }
+  }
+}
@@ -0,0 +1,148 @@
+/*
+ * This file is part of alloy2smt.
+ * Copyright (C) 2018-2019  The University of Iowa
+ *
+ * @author Mudathir Mohamed, Paul Meng
+ *
+ */
+
+package edu.uiowa.alloy2smt;
+
+import edu.uiowa.alloy2smt.translators.Translation;
+import edu.uiowa.alloy2smt.utils.AlloySettings;
+import edu.uiowa.smt.printers.SmtLibPrinter;
+import org.apache.commons.cli.*;
+
+import java.io.File;
+import java.io.IOException;
+import java.nio.charset.StandardCharsets;
+import java.nio.file.Files;
+import java.nio.file.InvalidPathException;
+import java.nio.file.Paths;
+import java.util.Formatter;
+import java.util.Scanner;
+
+public class Main
+{
+  public static final String SEP = File.separator;
+  public static final String OUTPUT_DIR = System.getProperty("java.io.tmpdir");
+  public static final String DEFAULT_OUTPUT_FILE = "output.smt2";
+
+  public static boolean isValidInputFilePath(String path)
+  {
+    File inputFile = new File(path);
+
+    return inputFile.exists() && inputFile.canRead() && path.endsWith(".als");
+  }
+
+  public static boolean isValidOutputFilePath(String path) throws IOException
+  {
+    try
+    {
+      Paths.get(path);
+    }
+    catch (InvalidPathException | NullPointerException ex)
+    {
+      return false;
+    }
+
+    File outputFile = new File(path);
+
+    if (outputFile.getParentFile() != null)
+    {
+      outputFile.getParentFile().mkdirs();
+    }
+    outputFile.createNewFile();
+    return true;
+  }
+
+  public static void main(String[] args)
+  {
+    Options options = new Options();
+    CommandLineParser commandLineParser = new DefaultParser();
+
+    options.addOption(Option.builder("i").longOpt("input").desc("Input Alloy model").hasArg().build());
+    options.addOption(Option.builder("o").longOpt("output").desc("SMT-LIB model output").hasArg().build());
+
+    try
+    {
+      CommandLine command = commandLineParser.parse(options, args);
+
+      Translation translation;
+      String defaultOutputFile;
+
+      if (command.hasOption("i"))
+      {
+        String inputFile = command.getOptionValue("i").trim();
+
+        if (isValidInputFilePath(inputFile))
+        {
+          String alloy = new String(Files.readAllBytes(Paths.get(inputFile)), StandardCharsets.UTF_8);
+          translation = Utils.translate(alloy, AlloySettings.Default);
+          defaultOutputFile = OUTPUT_DIR + SEP + new File(inputFile).getName() + ".smt2";
+        }
+        else
+        {
+          throw new Exception("Can not open file " + inputFile);
+        }
+      }
+      else
+      {
+        StringBuilder stringBuilder = new StringBuilder();
+        Scanner scanner = new Scanner(System.in);
+
+        while (scanner.hasNextLine())
+        {
+          stringBuilder.append(scanner.nextLine()).append("\n");
+        }
+
+        translation = Utils.translate(stringBuilder.toString(), AlloySettings.Default);
+        defaultOutputFile = DEFAULT_OUTPUT_FILE + ".smt2";
+      }
+
+      File outputFile = null;
+
+      if (command.hasOption("o"))
+      {
+        if (isValidOutputFilePath(command.getOptionValue("o")))
+        {
+          outputFile = new File(command.getOptionValue("o").trim());
+        }
+      }
+      if (outputFile == null)
+      {
+        outputFile = new File(defaultOutputFile);
+      }
+      try (Formatter formatter = new Formatter(outputFile))
+      {
+        formatter.format("%s\n", translation.getOptimizedSmtScript());
+
+        System.out.println("\n");
+        System.out.println(translation.getOptimizedSmtScript());
+
+        // translate all alloy commands
+        for (int i = 0; i < translation.getCommands().size(); i++)
+        {
+          String commandTranslation = translation.getOptimizedSmtScript(i).toString();
+
+          commandTranslation = SmtLibPrinter.PUSH + "\n" + commandTranslation +
+              SmtLibPrinter.CHECK_SAT + "\n" + SmtLibPrinter.GET_MODEL + "\n" +
+              SmtLibPrinter.POP + "\n";
+
+          formatter.format("%s\n", commandTranslation);
+          System.out.println("\n" + commandTranslation);
+        }
+      }
+      System.out.println("\nThe SMT-LIB model was generated at: " + outputFile.getAbsolutePath());
+    }
+    catch (ParseException exception)
+    {
+      HelpFormatter formatter = new HelpFormatter();
+      formatter.printHelp("java -jar alloy2smt.jar ", options);
+    }
+    catch (Exception exception)
+    {
+      exception.printStackTrace();
+    }
+  }
+}