prepping measurement setup w/ dreal

13 files changed, 30 insertions, 4 deletions

diff --git a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericDrealProblemSolver.java b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericDrealProblemSolver.java
index c71bb53a..d7268bb9 100644
--- a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericDrealProblemSolver.java
+++ b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericDrealProblemSolver.java
@@ -74,7 +74,10 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{
                                                 containerName,

                                                 "dreal"));

                 if (getModel) {drealCmd.add("--model");}

-                drealCmd.add("mnt/" + tempFileName);

+                String tmpFileLoc = "mnt/" + tempFileName;

+                //REMOVE LINE BELOW IF USING WINDOWS

+                tmpFileLoc = "../" + tmpFileLoc;//ONLY IF USING LINUX

+                drealCmd.add(tmpFileLoc);               

                 return runProcess(drealCmd);

         }

         

@@ -288,7 +291,7 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{
                 //DEBUG - Print things

 //              printFileContent(System.getProperty("java.io.tmpdir") + tempFileName);

 //              printOutput(outputs.get(0));

-                System.out.println(result);

+//              System.out.println(result);

                 //END DEBUG

                 

                 return result;

diff --git a/Solvers/SMT-Solver/com.microsoft.z3/lib/libz3.dll b/Solvers/SMT-Solver/com.microsoft.z3/lib/libz3.dll
new file mode 100644
index 00000000..46b1e7c2
--- /dev/null
+++ b/Solvers/SMT-Solver/com.microsoft.z3/lib/libz3.dll
diff --git a/Solvers/SMT-Solver/com.microsoft.z3/lib/libz3.dylib b/Solvers/SMT-Solver/com.microsoft.z3/lib/libz3.dylib
new file mode 100755
index 00000000..6ca9aea8
--- /dev/null
+++ b/Solvers/SMT-Solver/com.microsoft.z3/lib/libz3.dylib
diff --git a/Solvers/SMT-Solver/com.microsoft.z3/lib/libz3java.dll b/Solvers/SMT-Solver/com.microsoft.z3/lib/libz3java.dll
new file mode 100644
index 00000000..615bf3b8
--- /dev/null
+++ b/Solvers/SMT-Solver/com.microsoft.z3/lib/libz3java.dll
diff --git a/Solvers/SMT-Solver/com.microsoft.z3/lib/libz3java.dylib b/Solvers/SMT-Solver/com.microsoft.z3/lib/libz3java.dylib
new file mode 100755
index 00000000..73e02b97
--- /dev/null
+++ b/Solvers/SMT-Solver/com.microsoft.z3/lib/libz3java.dylib
diff --git a/Tests/MODELS2020-CaseStudies/case.study.familyTree.run/plugin.xml b/Tests/MODELS2020-CaseStudies/case.study.familyTree.run/plugin.xml
index 4297ec89..f5cda378 100644
--- a/Tests/MODELS2020-CaseStudies/case.study.familyTree.run/plugin.xml
+++ b/Tests/MODELS2020-CaseStudies/case.study.familyTree.run/plugin.xml
@@ -5,6 +5,7 @@
       <query-specification fqn="queries.twoMembersHaveNoParent"/>
       <query-specification fqn="queries.memberHasParent"/>
       <query-specification fqn="queries.negativeAge"/>
+      <query-specification fqn="queries.realisticAge"/>
       <query-specification fqn="queries.parentTooYoung"/>
     </group>
   </extension>
diff --git a/Tests/MODELS2020-CaseStudies/case.study.familyTree.run/src/queries/familyTreeConstraints.vql b/Tests/MODELS2020-CaseStudies/case.study.familyTree.run/src/queries/familyTreeConstraints.vql
index fdbac640..f8650073 100644
--- a/Tests/MODELS2020-CaseStudies/case.study.familyTree.run/src/queries/familyTreeConstraints.vql
+++ b/Tests/MODELS2020-CaseStudies/case.study.familyTree.run/src/queries/familyTreeConstraints.vql
@@ -26,6 +26,12 @@ pattern negativeAge(m: Member) {
         check(mage<0);

 }

 

+@Constraint(message="realisticAge", severity="error",key={m})

+pattern realisticAge(m: Member) {

+        Member.age(m,mage);

+        check(mage>120);

+}

+

 @Constraint(message="parentTooYoung", severity="error", key={c, p})

 pattern parentTooYoung(c: Member, p: Member) = {

         FamilyTree.members(_, c);

diff --git a/Tests/MODELS2020-CaseStudies/case.study.pledge.run/config/genericFamilyTree.vsconfig b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/config/genericFamilyTree.vsconfig
index 2e653776..a5fd3189 100644
--- a/Tests/MODELS2020-CaseStudies/case.study.pledge.run/config/genericFamilyTree.vsconfig
+++ b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/config/genericFamilyTree.vsconfig
@@ -33,6 +33,7 @@ generate {
         

         config = {

                 runtime = 10000,

+                "numeric-solver" = "z3",

                 log-level = normal,

                 "fitness-punishSize" = "false",

                 "fitness-scope" = "3"

diff --git a/Tests/MODELS2020-CaseStudies/case.study.pledge.run/config/genericFamilyTreeSMTEnd.vsconfig b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/config/genericFamilyTreeSMTEnd.vsconfig
index 7a22f760..e833397f 100644
--- a/Tests/MODELS2020-CaseStudies/case.study.pledge.run/config/genericFamilyTreeSMTEnd.vsconfig
+++ b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/config/genericFamilyTreeSMTEnd.vsconfig
@@ -33,6 +33,7 @@ generate {
         
         config = {
                 runtime = 10000,
+                "numeric-solver" = "z3",
                 log-level = normal,
                 "fitness-punishSize" = "false",
                 "fitness-scope" = "3",
diff --git a/Tests/MODELS2020-CaseStudies/case.study.pledge.run/config/genericFamilyTreeSMTQual.vsconfig b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/config/genericFamilyTreeSMTQual.vsconfig
index fa9cd6e2..36df7eef 100644
--- a/Tests/MODELS2020-CaseStudies/case.study.pledge.run/config/genericFamilyTreeSMTQual.vsconfig
+++ b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/config/genericFamilyTreeSMTQual.vsconfig
@@ -33,6 +33,7 @@ generate {
         
         config = {
                 runtime = 10000,
+                "numeric-solver" = "z3",
                 log-level = normal,
                 "fitness-punishSize" = "false",
                 "fitness-scope" = "3",
diff --git a/Tests/MODELS2020-CaseStudies/case.study.pledge.run/config/genericSatellite.vsconfig b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/config/genericSatellite.vsconfig
index aad8f544..3ee164cd 100644
--- a/Tests/MODELS2020-CaseStudies/case.study.pledge.run/config/genericSatellite.vsconfig
+++ b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/config/genericSatellite.vsconfig
@@ -31,6 +31,7 @@ generate {
 

         config = {

                 runtime = 10000,

+                "numeric-solver" = "z3",

                 log-level = normal,

                 "fitness-scope" = "3",

                 "fitness-punishSize" = "true",

diff --git a/Tests/MODELS2020-CaseStudies/case.study.pledge.run/config/genericTaxation.vsconfig b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/config/genericTaxation.vsconfig
index a3f1cd07..0f2657c1 100644
--- a/Tests/MODELS2020-CaseStudies/case.study.pledge.run/config/genericTaxation.vsconfig
+++ b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/config/genericTaxation.vsconfig
@@ -34,6 +34,7 @@ generate {
         
         config = {
                 runtime = 10000,
+                "numeric-solver" = "z3",
                 log-level = normal,
                 "fitness-scope" = "1",
                 "fitness-punishSize" = "inverse",
diff --git a/Tests/MODELS2020-CaseStudies/case.study.pledge.run/src/run/RunGeneratorConfig.xtend b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/src/run/RunGeneratorConfig.xtend
index e4d6fe9f..e1d9b9d9 100644
--- a/Tests/MODELS2020-CaseStudies/case.study.pledge.run/src/run/RunGeneratorConfig.xtend
+++ b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/src/run/RunGeneratorConfig.xtend
@@ -25,6 +25,9 @@ import org.apache.commons.cli.Option
 import org.apache.commons.cli.Options

 import org.apache.commons.cli.ParseException

 import org.eclipse.core.runtime.NullProgressMonitor

+import hu.bme.mit.inf.dslreasoner.application.applicationConfiguration.ConfigEntry

+import hu.bme.mit.inf.dslreasoner.application.applicationConfiguration.impl.ConfigEntryImpl

+import hu.bme.mit.inf.dslreasoner.application.applicationConfiguration.CustomEntry

 

 class RunGeneratorConfig {

         static var SIZE_LB = 20

@@ -34,6 +37,7 @@ class RunGeneratorConfig {
         static var RUNS = 10

         static var MODELS = 10

         static var RUNTIME = 1500

+        static var NUM_SOLVER = "z3"

 

         static var DOMAIN = "FamilyTree" // "FamilyTree", "Satellite", "Taxation"

         static val QUERIES = true

@@ -62,6 +66,9 @@ class RunGeneratorConfig {
 

                 val rt = new Option("rt", "runtime", true, "runtime limit")

                 options.addOption(rt)

+                

+                val ns = new Option("ns", "numericSolver", true, "what numeric solver to use")

+                options.addOption(ns)

 

                 val d = new Option("d", "domain", true, "domain")

                 options.addOption(d)

@@ -91,6 +98,8 @@ class RunGeneratorConfig {
                 if(nmIn !== null) MODELS = Integer.parseInt(nmIn)

                 val rtIn = cmd.getOptionValue("runtime")

                 if(rtIn !== null) RUNTIME = Integer.parseInt(rtIn)

+                val nsIn = cmd.getOptionValue("numericSolver")

+                if(nsIn !== null && nsIn.equals("dreal")) NUM_SOLVER = "dreal"

                 val dIn = cmd.getOptionValue("domain")

                 if(dIn !== null) DOMAIN = dIn

                 val hhIn = cmd.getOptionValue("household")

@@ -109,7 +118,7 @@ class RunGeneratorConfig {
                 // /////////////////////////

                 // BEGIN RUN

                 println(

-                        "<<DOMAIN: " + DOMAIN + ", SIZE=" + SIZE_LB + "to" + SIZE_UB + ", Runs=" + RUNS + ", ModelsPerRun=" +

+                        "<<DOMAIN: " + DOMAIN + ", NumSolver=" + NUM_SOLVER + ", SIZE=" + SIZE_LB + "to" + SIZE_UB + ", Runs=" + RUNS + ", ModelsPerRun=" +

                                 MODELS + ", Runtime=" + RUNTIME + ">>")

                 if (isTaxation) println("<<Households: " + HOUSEHOLD + ">>")

 

@@ -173,10 +182,12 @@ class RunGeneratorConfig {
                         }

                 }

 //              workspace.writeModel(config, '''x.xmi''')

-                // Runtime

+                // Config

                 val configScope = genTask.config as ConfigSpecification

                 val runtimeEntry = configScope.entries.get(0) as RuntimeEntry

                 runtimeEntry.millisecLimit = RUNTIME

+                val numSolverEntry = configScope.entries.get(1) as CustomEntry

+                numSolverEntry.value = NUM_SOLVER

 

                 // Output locations

                 val debug = genTask.debugFolder as FileSpecification