From 64041ec680c39dac8487812d27141d921130aed5 Mon Sep 17 00:00:00 2001 From: Naveen Sundar Govindarajulu Date: Fri, 13 Jul 2018 12:38:47 -0700 Subject: [PATCH] add tai demo, snark builtins. --- pom.xml | 60 +++--- snark-20120808r02/snark-interface.lisp | 11 +- .../ccprovers/CognitiveCalculusProver.java | 78 +++++--- .../prover/core/ccprovers/ShadowProver.java | 181 ++++++++++++++++++ .../core/proof/AtomicJustification.java | 17 +- .../core/proof/CompoundJustification.java | 7 +- .../core/proof/TrivialJustification.java | 29 ++- .../shadow/prover/examples/Example.java | 79 ++++++++ .../shadow/prover/examples/TAI_AEGAP.java | 14 ++ .../prover/examples/VirtueLearning.java | 2 +- .../representations/formula/Formula.java | 1 + .../shadow/prover/sandboxes/Sandbox.java | 18 +- .../shadow/prover/utils/Reader.java | 32 +++- .../shadow/prover/examples/taiaegap.clj | 80 ++++++++ .../virtuelearning.clj | 0 15 files changed, 530 insertions(+), 79 deletions(-) create mode 100644 src/main/java/com/naveensundarg/shadow/prover/core/ccprovers/ShadowProver.java create mode 100644 src/main/java/com/naveensundarg/shadow/prover/examples/Example.java create mode 100644 src/main/java/com/naveensundarg/shadow/prover/examples/TAI_AEGAP.java create mode 100644 src/main/resources/com/naveensundarg/shadow/prover/examples/taiaegap.clj rename src/main/resources/com/naveensundarg/shadow/prover/{experiments => examples}/virtuelearning.clj (100%) diff --git a/pom.xml b/pom.xml index b378f1a..83f0d9d 100644 --- a/pom.xml +++ b/pom.xml @@ -6,7 +6,7 @@ com.naveensundarg prover - 0.998 + 1.02 jar @@ -31,38 +31,34 @@ HEAD - - - ossrh - https://oss.sonatype.org/content/repositories/snapshots - - - ossrh - https://oss.sonatype.org/service/local/staging/deploy/maven2/ - - + - - - - org.apache.maven.plugins - maven-gpg-plugin - 1.5 - - - org.apache.maven.plugins - maven-release-plugin - - - pom.xml - - - 2.4 - - - - - + + + org.apache.maven.plugins + maven-assembly-plugin + 2.2-beta-5 + + + jar-with-dependencies + + + + com.naveensundarg.shadow.prover.sandboxes.Sandbox + + + + + + make-assembly + package + + single + + + + + diff --git a/snark-20120808r02/snark-interface.lisp b/snark-20120808r02/snark-interface.lisp index 3099b81..ba7fd71 100644 --- a/snark-20120808r02/snark-interface.lisp +++ b/snark-20120808r02/snark-interface.lisp @@ -45,7 +45,7 @@ (assert `(= ,(+ i j) (+ ,j ,i )))))) (defun assert-domain (end) - (assert `(forall ((?p Number)) + (assert `(forall (?p) (implies (Prior ?p ,end) ,(cons 'or (loop for i from 0 to end collect `(= ,i ?p))))))) @@ -56,10 +56,10 @@ -(defun setup-snark (&key (time-limit 500) (verbose t)) +(defun setup-snark (&key (time-limit 500) (verbose nil)) (snark:initialize :verbose verbose) - ;(if (not verbose) (snark-deverbose) ) + (if (not verbose) (snark-deverbose) ) (snark:run-time-limit time-limit) (snark:assert-supported t) (snark:assume-supported t) @@ -69,9 +69,8 @@ (snark::declare-code-for-numbers) (snark:allow-skolem-symbols-in-answers nil) - ;(assert-domain 10) - ;(assert-add-table 10) - ) + (assert-domain 10) + (assert-add-table 10)) diff --git a/src/main/java/com/naveensundarg/shadow/prover/core/ccprovers/CognitiveCalculusProver.java b/src/main/java/com/naveensundarg/shadow/prover/core/ccprovers/CognitiveCalculusProver.java index 685a2a4..7c58749 100644 --- a/src/main/java/com/naveensundarg/shadow/prover/core/ccprovers/CognitiveCalculusProver.java +++ b/src/main/java/com/naveensundarg/shadow/prover/core/ccprovers/CognitiveCalculusProver.java @@ -3,6 +3,7 @@ import com.diogonunes.jcdp.color.ColoredPrinter; import com.diogonunes.jcdp.color.api.Ansi; import com.naveensundarg.shadow.prover.core.Logic; +import com.naveensundarg.shadow.prover.core.proof.AtomicJustification; import com.naveensundarg.shadow.prover.utils.*; import com.naveensundarg.shadow.prover.core.Prover; import com.naveensundarg.shadow.prover.core.SnarkWrapper; @@ -138,6 +139,13 @@ private static CognitiveCalculusProver root(CognitiveCalculusProver cognitiveCal @Override public Optional prove(Set assumptions, Formula formula) { + assumptions.forEach(x-> { + + if(x.getJustification() == null){ + + x.setJustification(new AtomicJustification("GIVEN")); + } + }); return prove(assumptions, formula, CollectionUtils.newEmptySet()); } @@ -169,19 +177,7 @@ private boolean alreadySeen(Set assumptions, Formula formula) { private synchronized Optional prove(Set assumptions, Formula formula, Set added) { - currentAssumptions = assumptions; - - - if (defeasible) { - Optional got = defeasible(formula); - - if (got != null) return got; - - } else { - - - } Prover folProver = SnarkWrapper.getInstance(); @@ -204,7 +200,7 @@ private synchronized Optional prove(Set assumptions, For int sizeAfterExpansion = base.size(); if (base.contains(formula)) { - return Optional.of(TrivialJustification.trivial(assumptions, formula)); + return Optional.of(TrivialJustification.trivial(base, formula)); } Optional andProofOpt = tryAND(base, formula, added); @@ -288,17 +284,10 @@ private synchronized Optional prove(Set assumptions, For // logFOLCall(true, shadow(base), shadowedGoal); return shadowedJustificationOpt; } - else{ - - // logFOLCall(false, shadow(base), shadowedGoal); + // logFOLCall(false, shadow(base), shadowedGoal); - } - if (agentClosureJustificationOpt.isPresent()) { - - return agentClosureJustificationOpt; - } + return agentClosureJustificationOpt; - return Optional.empty(); } protected Optional tryIfIntro(Set base, Formula formula, Set added) { @@ -729,6 +718,9 @@ protected Set expand(Set base, Set added, Formula goa expandR4(base, added); expandSelfBelief(base, added); expandPerceptionToKnowledge(base, added); + expandSaysToBelief(base, added); + expandIntentionToPerception(base, added); + expandModalConjunctions(base, added); expandModalImplications(base, added); expandDR1(base, added, goal); @@ -885,12 +877,52 @@ private void expandPerceptionToKnowledge(Set base, Set added) filter(f -> f instanceof Perception). map(f -> { Perception p = (Perception) f; - return new Knowledge(p.getAgent(), p.getTime(), p.getFormula()); + Knowledge k = new Knowledge(p.getAgent(), p.getTime(), p.getFormula()); + k.setJustification(new CompoundJustification("Perception to knowledge " + p, CollectionUtils.listOf(p.getJustification()))); + return k; }). collect(Collectors.toSet()); expansionLog(String.format("Perceives(P) ==> P", Constants.VDASH, Constants.PHI, Constants.NEC, Constants.PHI), derived); + base.addAll(derived); + added.addAll(derived); + } + + private void expandIntentionToPerception(Set base, Set added) { + + Set derived = base. + stream(). + filter(f -> f instanceof Intends). + map(f -> { + Intends i = (Intends) f; + Perception k = new Perception(i.getAgent(), i.getTime(), i.getFormula()); + k.setJustification(new CompoundJustification("Intention to Perception " + i, CollectionUtils.listOf(i.getJustification()))); + return k; + }). + collect(Collectors.toSet()); + + expansionLog(String.format("Intends(P) ==> Perceives(P)", Constants.VDASH, Constants.PHI, Constants.NEC, Constants.PHI), derived); + + base.addAll(derived); + added.addAll(derived); + } + + private void expandSaysToBelief(Set base, Set added) { + + Set derived = base. + stream(). + filter(f -> f instanceof Says). + map(f -> { + Says s = (Says) f; + Belief b = new Belief(s.getAgent(), s.getTime(), s.getFormula()); + b.setJustification(new CompoundJustification("Says to belief", CollectionUtils.listOf(s.getJustification()))); + return b; + }). + collect(Collectors.toSet()); + + expansionLog(String.format("Says(P) ==> Belief(P)", Constants.VDASH, Constants.PHI, Constants.NEC, Constants.PHI), derived); + base.addAll(derived); added.addAll(derived); diff --git a/src/main/java/com/naveensundarg/shadow/prover/core/ccprovers/ShadowProver.java b/src/main/java/com/naveensundarg/shadow/prover/core/ccprovers/ShadowProver.java new file mode 100644 index 0000000..f47c704 --- /dev/null +++ b/src/main/java/com/naveensundarg/shadow/prover/core/ccprovers/ShadowProver.java @@ -0,0 +1,181 @@ +package com.naveensundarg.shadow.prover.core.ccprovers; + +import com.diogonunes.jcdp.color.api.Ansi; +import com.naveensundarg.shadow.prover.core.Prover; +import com.naveensundarg.shadow.prover.core.SnarkWrapper; +import com.naveensundarg.shadow.prover.core.internals.AgentSnapShot; +import com.naveensundarg.shadow.prover.core.proof.Justification; +import com.naveensundarg.shadow.prover.core.proof.TrivialJustification; +import com.naveensundarg.shadow.prover.core.sortsystem.SortSystem; +import com.naveensundarg.shadow.prover.representations.formula.Belief; +import com.naveensundarg.shadow.prover.representations.formula.Formula; +import com.naveensundarg.shadow.prover.representations.formula.Intends; +import com.naveensundarg.shadow.prover.representations.formula.Knowledge; +import com.naveensundarg.shadow.prover.representations.value.Value; +import com.naveensundarg.shadow.prover.representations.value.Variable; +import com.naveensundarg.shadow.prover.utils.CollectionUtils; +import org.apache.commons.lang3.tuple.Pair; + +import java.util.List; +import java.util.Map; +import java.util.Optional; +import java.util.Set; +import java.util.stream.Collectors; + + +public class ShadowProver implements Prover { + + + Prover folProver; + + + public ShadowProver() { + + folProver = SnarkWrapper.getInstance(); + + + } + + @Override + public Optional prove(Set assumptions, Formula goal) { + Set base = CollectionUtils.setFrom(assumptions); + + Formula shadowedGoal = goal.shadow(1); + + Optional shadowedJustificationOpt = folProver.prove(shadow(base), shadowedGoal); + Optional agentClosureJustificationOpt = proveAgentClosure(base, goal); + + while (!shadowedJustificationOpt.isPresent() && !agentClosureJustificationOpt.isPresent()) { + + + int sizeBeforeExpansion = base.size(); + base = expand(base, goal); + int sizeAfterExpansion = base.size(); + + if(sizeAfterExpansion == sizeBeforeExpansion){ + + return Optional.empty(); + } + if (base.contains(goal)) { + return Optional.of(TrivialJustification.trivial(base, goal)); + } + + shadowedJustificationOpt = folProver.prove(shadow(base), shadowedGoal); + agentClosureJustificationOpt = proveAgentClosure(base, goal); + + } + + if (shadowedJustificationOpt.isPresent()) { + + return shadowedJustificationOpt; + } + + return agentClosureJustificationOpt; + + + } + + public Set expand(Set base, Formula goal) { + return base; + } + + @Override + public Optional prove(SortSystem sortSystem, Set assumptions, Formula formula) { + + return null; + } + + @Override + public Optional proveAndGetBinding(Set assumptions, Formula formula, Variable variable) { + return Optional.empty(); + } + + @Override + public Optional> proveAndGetBindings(Set assumptions, Formula formula, List variable) { + return Optional.empty(); + } + + @Override + public Optional>>> proveAndGetMultipleBindings(Set assumptions, Formula formula, List variable) { + return Optional.empty(); + } + + protected Set shadow(Set formulas) { + return formulas.stream().map(f -> f.shadow(1)).collect(Collectors.toSet()); + } + + + private Optional proveAgentClosure(Set base, Formula goal) { + + if (goal instanceof Belief) { + + Belief belief = (Belief) goal; + Value agent = belief.getAgent(); + Value time = belief.getTime(); + Formula goalBelief = belief.getFormula(); + + AgentSnapShot agentSnapShot = AgentSnapShot.from(base); + + Set allBelievedTillTime = agentSnapShot.allBelievedByAgentTillTime(agent, time); + + + ShadowProver shadowProver = new ShadowProver(); + Optional inner = shadowProver.prove(allBelievedTillTime, goalBelief); + if (inner.isPresent()) { + //TODO: Augment this + + return inner; + } + + } + + if (goal instanceof Intends) { + + + Intends intends = (Intends) goal; + Value agent = intends.getAgent(); + Value time = intends.getTime(); + Formula goalKnowledge = intends.getFormula(); + + AgentSnapShot agentSnapShot = AgentSnapShot.from(base); + + Set allIntendedByTillTime = agentSnapShot.allIntendedByAgentTillTime(agent, time); + + + ShadowProver shadowProver = new ShadowProver(); + Optional inner = shadowProver.prove(allIntendedByTillTime, goalKnowledge); + if (inner.isPresent()) { + //TODO: Augment this + + return inner; + } + } + + if (goal instanceof Knowledge) { + + + Knowledge knowledge = (Knowledge) goal; + Value agent = knowledge.getAgent(); + Value time = knowledge.getTime(); + Formula goalKnowledge = knowledge.getFormula(); + + AgentSnapShot agentSnapShot = AgentSnapShot.from(base); + + Set allKnownByTillTime = agentSnapShot.allKnownByAgentTillTime(agent, time); + + + ShadowProver shadowProver = new ShadowProver(); + Optional inner = shadowProver.prove(allKnownByTillTime, goalKnowledge); + if (inner.isPresent()) { + //TODO: Augment this + + return inner; + } + } + + return Optional.empty(); + + } + + +} diff --git a/src/main/java/com/naveensundarg/shadow/prover/core/proof/AtomicJustification.java b/src/main/java/com/naveensundarg/shadow/prover/core/proof/AtomicJustification.java index 833e7e8..2fc3328 100644 --- a/src/main/java/com/naveensundarg/shadow/prover/core/proof/AtomicJustification.java +++ b/src/main/java/com/naveensundarg/shadow/prover/core/proof/AtomicJustification.java @@ -19,11 +19,26 @@ public AtomicJustification(String name, Formula... inputs){ } + public AtomicJustification(String name){ + this.name = name; + + this.inputs = null; + } + public Formula[] getInputs() { + return inputs; + } @Override public String toString() { - return "(" + name + Arrays.toString(inputs) + ")"; + if(inputs!=null){ + + return "(" + name + Arrays.toString(inputs) + ")"; + + } else { + + return name; + } } } diff --git a/src/main/java/com/naveensundarg/shadow/prover/core/proof/CompoundJustification.java b/src/main/java/com/naveensundarg/shadow/prover/core/proof/CompoundJustification.java index 658347b..b7af270 100644 --- a/src/main/java/com/naveensundarg/shadow/prover/core/proof/CompoundJustification.java +++ b/src/main/java/com/naveensundarg/shadow/prover/core/proof/CompoundJustification.java @@ -15,12 +15,13 @@ public CompoundJustification(String name, List subs){ } - - + public List getSubs() { + return subs; + } @Override public String toString() { return "(" + name +"\n"+ - " "+ subs +")"; + " "+ subs +")"; } } diff --git a/src/main/java/com/naveensundarg/shadow/prover/core/proof/TrivialJustification.java b/src/main/java/com/naveensundarg/shadow/prover/core/proof/TrivialJustification.java index 790eaf3..c8e3746 100644 --- a/src/main/java/com/naveensundarg/shadow/prover/core/proof/TrivialJustification.java +++ b/src/main/java/com/naveensundarg/shadow/prover/core/proof/TrivialJustification.java @@ -29,11 +29,34 @@ public TrivialJustification(Set base, Formula formula, String message){ this.message = message; } + private String printFormula(Formula f){ + + if(f.getJustification()==null){ + + return f.toString(); + } + else { + + return "\n(" + f.toString() + "\n " + f.getJustification() + ")"; + } + } @Override public String toString() { - return "(" + message+ "\n\t\t Givens:\n\t\t(" - + base.stream().map(Formula::toString).reduce("\t\t", (x,y) -> x + "\n\t\t" + y).trim() + - ") \n\t\t Goals:\n\t\t" + return "(" + message+ "\n Givens:\n(" + + base.stream().map(this::printFormula).reduce("", (x, y) -> x + "\n" + y).trim() + + ") \n Goals:\n" + formula.toString() + ")"; } + + public Formula getFormula() { + return formula; + } + + public Set getBase() { + return base; + } + + public String getMessage() { + return message; + } } diff --git a/src/main/java/com/naveensundarg/shadow/prover/examples/Example.java b/src/main/java/com/naveensundarg/shadow/prover/examples/Example.java new file mode 100644 index 0000000..2ec2982 --- /dev/null +++ b/src/main/java/com/naveensundarg/shadow/prover/examples/Example.java @@ -0,0 +1,79 @@ +package com.naveensundarg.shadow.prover.examples; + +import com.diogonunes.jcdp.color.ColoredPrinter; +import com.diogonunes.jcdp.color.api.Ansi; +import com.naveensundarg.shadow.prover.core.Prover; +import com.naveensundarg.shadow.prover.core.SnarkWrapper; +import com.naveensundarg.shadow.prover.core.ccprovers.AxiologyProver; +import com.naveensundarg.shadow.prover.core.ccprovers.InductiveCognitiveCalculusProver; +import com.naveensundarg.shadow.prover.core.proof.Justification; +import com.naveensundarg.shadow.prover.representations.formula.Formula; +import com.naveensundarg.shadow.prover.utils.Problem; +import com.naveensundarg.shadow.prover.utils.ProblemReader; +import com.naveensundarg.shadow.prover.utils.Reader; +import com.naveensundarg.shadow.prover.utils.Sets; + +import java.util.Optional; + +/** + * Created by naveensundarg on 4/8/16. + */ +public class Example { + + + private static ColoredPrinter coloredPrinter = new ColoredPrinter.Builder(1, false) + .foreground(Ansi.FColor.WHITE).background(Ansi.BColor.BLACK) //setting format + .build(); + + + + public static void run(Prover prover, String path) throws Exception { + + + + + Problem problem = ProblemReader.readFrom(VirtueLearning.class.getResourceAsStream(path)).get(0); + + System.out.println(); + coloredPrinter.println("===================================" , Ansi.Attribute.NONE, Ansi.FColor.BLACK, Ansi.BColor.NONE); + + + coloredPrinter.println(" \t"+ "STARTING STATE", Ansi.Attribute.BOLD, Ansi.FColor.BLACK, Ansi.BColor.NONE); + + problem.getAssumptions().forEach(f-> { + + try { + Thread.sleep(1000); + } catch (InterruptedException e) { + e.printStackTrace(); + } + coloredPrinter.println(" \t"+ f, Ansi.Attribute.BOLD, Ansi.FColor.BLACK, Ansi.BColor.NONE); + }); + + coloredPrinter.println(" " , Ansi.Attribute.UNDERLINE, Ansi.FColor.BLACK, Ansi.BColor.NONE); + Thread.sleep(1000); + coloredPrinter.println(" \t Goal", Ansi.Attribute.BOLD, Ansi.FColor.MAGENTA, Ansi.BColor.NONE); + Thread.sleep(1000); + + coloredPrinter.println(" \t"+ problem.getGoal(), Ansi.Attribute.BOLD, Ansi.FColor.GREEN, Ansi.BColor.NONE); + coloredPrinter.println("===================================" , Ansi.Attribute.NONE, Ansi.FColor.BLACK, Ansi.BColor.NONE); + + Thread.sleep(1000); + + Optional proofOpt = (prover.prove(problem.getAssumptions(), problem.getGoal())); + + + if(proofOpt.isPresent()){ + + coloredPrinter.println(" " , Ansi.Attribute.UNDERLINE, Ansi.FColor.BLACK, Ansi.BColor.NONE); + Thread.sleep(500); + coloredPrinter.println(" \t INFERRED", Ansi.Attribute.BOLD, Ansi.FColor.MAGENTA, Ansi.BColor.NONE); + + coloredPrinter.println(" \t"+ problem.getGoal(), Ansi.Attribute.BOLD, Ansi.FColor.BLUE, Ansi.BColor.NONE); + coloredPrinter.println("===================================" , Ansi.Attribute.NONE, Ansi.FColor.BLACK, Ansi.BColor.NONE); + + } + + } + +} diff --git a/src/main/java/com/naveensundarg/shadow/prover/examples/TAI_AEGAP.java b/src/main/java/com/naveensundarg/shadow/prover/examples/TAI_AEGAP.java new file mode 100644 index 0000000..2e15e2c --- /dev/null +++ b/src/main/java/com/naveensundarg/shadow/prover/examples/TAI_AEGAP.java @@ -0,0 +1,14 @@ +package com.naveensundarg.shadow.prover.examples; + +import com.naveensundarg.shadow.prover.core.ccprovers.CognitiveCalculusProver; + +public class TAI_AEGAP { + + + public static void main(String[ ] args) throws Exception { + + + + Example.run(new CognitiveCalculusProver(), "taiaegap.clj"); + } +} diff --git a/src/main/java/com/naveensundarg/shadow/prover/examples/VirtueLearning.java b/src/main/java/com/naveensundarg/shadow/prover/examples/VirtueLearning.java index 6a45a61..9af1fa7 100644 --- a/src/main/java/com/naveensundarg/shadow/prover/examples/VirtueLearning.java +++ b/src/main/java/com/naveensundarg/shadow/prover/examples/VirtueLearning.java @@ -35,7 +35,7 @@ public static void main(String[] args) throws Exception { Prover prover = new InductiveCognitiveCalculusProver(); - Problem problem = ProblemReader.readFrom(VirtueLearning.class.getResourceAsStream("../experiments/virtuelearning.clj")).get(0); + Problem problem = ProblemReader.readFrom(VirtueLearning.class.getResourceAsStream("virtuelearning.clj")).get(0); System.out.println(); coloredPrinter.println("===================================" , Ansi.Attribute.NONE, Ansi.FColor.BLACK, Ansi.BColor.NONE); diff --git a/src/main/java/com/naveensundarg/shadow/prover/representations/formula/Formula.java b/src/main/java/com/naveensundarg/shadow/prover/representations/formula/Formula.java index 634958f..6b1a126 100644 --- a/src/main/java/com/naveensundarg/shadow/prover/representations/formula/Formula.java +++ b/src/main/java/com/naveensundarg/shadow/prover/representations/formula/Formula.java @@ -19,6 +19,7 @@ public abstract class Formula extends Expression { + private Justification justification; diff --git a/src/main/java/com/naveensundarg/shadow/prover/sandboxes/Sandbox.java b/src/main/java/com/naveensundarg/shadow/prover/sandboxes/Sandbox.java index 466feaa..feef44f 100644 --- a/src/main/java/com/naveensundarg/shadow/prover/sandboxes/Sandbox.java +++ b/src/main/java/com/naveensundarg/shadow/prover/sandboxes/Sandbox.java @@ -32,16 +32,30 @@ public class Sandbox { - public static void main1(String[] args) throws Exception { + public static void main(String[] args) throws Exception { + + + Formula f1 = Reader.readFormulaFromString("(forall (x y) (iff (= x y) (forall X (iff (X x) (X y)))))"); + Formula f2 = Reader.readFormulaFromString("(TwentyFive joan)"); + Formula f3 = Reader.readFormulaFromString("(Thirty John)"); + Formula f4 = Reader.readFormulaFromString("(forall x (if (TwentyFive x) (not (Thirty x))))"); + + Formula goal = Reader.readFormulaFromString("(= 5 (+ 2 3))"); + + + Prover prover = new CognitiveCalculusProver(); + + System.out.println(prover.prove(Sets.from(), goal).get()); } + private static ColoredPrinter coloredPrinter = new ColoredPrinter.Builder(1, false) .foreground(Ansi.FColor.WHITE).background(Ansi.BColor.BLACK) //setting format .build(); - public static void main(String[] args) throws Exception { + public static void main2(String[] args) throws Exception { diff --git a/src/main/java/com/naveensundarg/shadow/prover/utils/Reader.java b/src/main/java/com/naveensundarg/shadow/prover/utils/Reader.java index 62b0094..d1aaa2d 100644 --- a/src/main/java/com/naveensundarg/shadow/prover/utils/Reader.java +++ b/src/main/java/com/naveensundarg/shadow/prover/utils/Reader.java @@ -10,7 +10,6 @@ import com.naveensundarg.shadow.prover.representations.value.Constant; import com.naveensundarg.shadow.prover.representations.value.Value; import com.naveensundarg.shadow.prover.representations.value.Variable; -import com.sun.org.apache.xpath.internal.operations.Bool; import us.bpsm.edn.Symbol; import us.bpsm.edn.parser.Parseable; import us.bpsm.edn.parser.Parser; @@ -70,6 +69,9 @@ private enum QuantifierType { public static final Value NOW, I; + private static final Map SNARK_BUILTIN_RELATIONS = CollectionUtils.newMap(); + private static final Map SNARK_BUILTIN_FUNCTIONS = CollectionUtils.newMap(); + static { try { @@ -78,6 +80,17 @@ private enum QuantifierType { NOW = readLogicValue("NOW"); I = readLogicValueFromString("I"); + SNARK_BUILTIN_RELATIONS.put("<", "$$$less"); + SNARK_BUILTIN_RELATIONS.put("<=", "$$$lesseq"); + SNARK_BUILTIN_RELATIONS.put(">", "$$$greater"); + SNARK_BUILTIN_RELATIONS.put(">=", "$$$greatereq"); + + SNARK_BUILTIN_FUNCTIONS.put("+", "$$sum"); + SNARK_BUILTIN_FUNCTIONS.put("-", "$$difference"); + SNARK_BUILTIN_FUNCTIONS.put("*", "$$produce"); + SNARK_BUILTIN_FUNCTIONS.put("/", "$$quotient_r"); + + } catch (Exception e) { throw new AssertionError("Could not instantiate basic constant: now"); } @@ -137,7 +150,8 @@ public static Value readLogicValue(Object input, Set variableNames) thro arguments[i - 1] = readLogicValue(list.get(i), variableNames); } - return new Compound(name, arguments); + + return new Compound(SNARK_BUILTIN_FUNCTIONS.getOrDefault(name, name), arguments); } throw new ParsingException("name should be a string" + nameObject); @@ -263,7 +277,9 @@ private static Phrase readPhrase(Object input, Set variableNames) throws throw new ParsingException("Could not resolve the method " + name); } else { - return new Atom(((Symbol) input).getName()); + + String atomName = ((Symbol) input).getName(); + return new Atom(SNARK_BUILTIN_RELATIONS.getOrDefault(atomName, atomName)); } } @@ -359,7 +375,8 @@ private static Phrase readPhrase(Object input, Set variableNames) throws private static Formula readFormula(Object input, Set variableNames) throws ParsingException { if (input instanceof Symbol) { - return new Atom(((Symbol) input).getName()); + String name = ((Symbol) input).getName(); + return new Atom(SNARK_BUILTIN_RELATIONS.getOrDefault(name, name)); } if (input instanceof List) { @@ -964,9 +981,7 @@ private static Formula constructPredicate(List list, Set variableNames) String name = ((Symbol) nameObject).getName(); - if (name.startsWith("$")) { - throw new AssertionError("Atom and predicate names cannot start with a $: " + name); - } + Value[] values = new Value[list.size() - 1]; @@ -975,7 +990,8 @@ private static Formula constructPredicate(List list, Set variableNames) values[i - 1] = readLogicValue(list.get(i), variableNames); } - return new Predicate(name, values); + + return new Predicate(SNARK_BUILTIN_RELATIONS.getOrDefault(name, name), values); } else { throw new ParsingException("Name of predicate should be a string! " + nameObject); diff --git a/src/main/resources/com/naveensundarg/shadow/prover/examples/taiaegap.clj b/src/main/resources/com/naveensundarg/shadow/prover/examples/taiaegap.clj new file mode 100644 index 0000000..faedda2 --- /dev/null +++ b/src/main/resources/com/naveensundarg/shadow/prover/examples/taiaegap.clj @@ -0,0 +1,80 @@ +{ + :name "TAI AEGAP Example" + :assumptions + { + "Background 1 - Iff the battery is alive it is dead. " + (Knows! tai t0 + (forall [time] + (iff (not (holds battery_alive time)) + (holds battery_dead time)))) + + "Background 2 - Iff the alarm is on it is off." + (Knows! tai t0 + (forall [time] + (iff (not (holds alarm_on time)) + (holds alarm_off time)))) + + "Background 3 - If the battery is alive and the CO level is greater than 400, + the alarm will not be off." + (Believes! tai t0 + (forall [time] + (if (and (exists [level] (and (> level 400) (holds (COLevel level) time))) + (holds battery_alive time)) + (not (holds alarm_off time))))) + "Background 4" (Knows! tai t0 + (forall + [time] + (if + (and (exists [level] (and (> level 400) (holds (COLevel level) time))) + (not (holds battery_alive time))) + (holds dangerous time)))) + + + + "Background 5" (Believes! tai t1 + (Ought! tai t1 + (holds dangerous t1) + (Intends! tai t1 alert))) + + "Background 6" (Believes! tai t1 + (Ought! tai t1 + alert + (Desires! tai t1 alert))) + + "Background 7" (Believes! tai t0 + (forall [time] + (if (or (not (holds dangerous time)) + alert) + safe))) + + "Backgroung 8" (forall [time] (if (DangerouslyHighCOLevel time) + (not (happens (alert fire-station) time)))) + + "Background 9" (forall [time] + (iff (HighCOLevel time) + (exists [level] + (and (> level 400) + (holds (COLevel level) time))))) + + "Background 10" (forall [time] + (iff (DangerouslyHighCOLevel time) + (exists [level] + (and (> level 800) + (holds (COLevel level) time))))) + + + "Planning" (if (Desires! tai t1 alert) + (Intends! tai t1 + (or (happens (alert fire-station) t2) + (happens (switch-on speaker) t2)))) + + :Situation-1 (Perceives! tai t1 (holds (COLevel 500) t1)) + :Situation-2 (Perceives! tai t1 (holds alarm_off t1)) + :Situation-3 (Perceives! tai t2 (holds (COLevel 1000) t2)) + + } + + + + :goal (happens (switch-on speaker) t2) + } \ No newline at end of file diff --git a/src/main/resources/com/naveensundarg/shadow/prover/experiments/virtuelearning.clj b/src/main/resources/com/naveensundarg/shadow/prover/examples/virtuelearning.clj similarity index 100% rename from src/main/resources/com/naveensundarg/shadow/prover/experiments/virtuelearning.clj rename to src/main/resources/com/naveensundarg/shadow/prover/examples/virtuelearning.clj