diff --git a/src/main/java/org/polystat/far/Expr.java b/src/main/java/org/polystat/far/Expr.java index c3d07f0..1ab9211 100644 --- a/src/main/java/org/polystat/far/Expr.java +++ b/src/main/java/org/polystat/far/Expr.java @@ -88,8 +88,18 @@ public Directives find() { final Solver slv = CTX.mkSolver(); final List list = new ArrayList<>(0); for (final XML obj : this.xml.nodes("o/o")) { - final BoolExpr cur = opts(obj); - list.add(cur); + final String name = obj.xpath("@name").get(0); + BoolExpr equation = CTX.mkNot( + CTX.mkEq( + CTX.mkConst(name, CTX.getStringSort()), + CTX.mkString("NONE") + ) + ); + final BoolExpr cur = opts(obj, name); + if (!cur.isFalse()) { + equation = CTX.mkAnd(cur, equation); + } + list.add(equation); } list.add(this.mkVariables()); slv.add(list.toArray(new BoolExpr[0])); @@ -113,11 +123,11 @@ public Directives find() { /** * Parse opts tags. * @param xml Current XML block + * @param name Attr name of current XML block * @return BoolExpr of current block */ - private static BoolExpr opts(final XML xml) { + private static BoolExpr opts(final XML xml, final String name) { BoolExpr result = CTX.mkFalse(); - final String name = xml.xpath("@name").get(0); final List> obj = new ArrayList<>(0); for (final XML opts : xml.nodes("opts")) { obj.add(opt(opts)); @@ -136,15 +146,6 @@ private static BoolExpr opts(final XML xml) { ); result = CTX.mkOr(result, cur); } - result = CTX.mkAnd( - result, - CTX.mkNot( - CTX.mkEq( - CTX.mkConst(name, CTX.getStringSort()), - CTX.mkString("NONE") - ) - ) - ); return result; } @@ -157,9 +158,8 @@ private static Map opt(final XML xml) { final Map result = new HashMap<>(); for (final XML opt : xml.nodes("opt")) { final String val = opt.xpath("@x").get(0); - final BoolExpr cur = taus(opt); final BoolExpr old = result.getOrDefault(val, CTX.mkFalse()); - result.put(val, CTX.mkOr(cur, old)); + result.put(val, CTX.mkOr(taus(opt), old)); } return result; } @@ -220,7 +220,7 @@ private BoolExpr mkVariables() { final String path = String.format("/o/o/opts/opt/tau[@i='%s']/text()", var); variables.get(name).addAll(this.xml.xpath(path)); } - BoolExpr result = CTX.mkAnd(); + BoolExpr result = CTX.mkTrue(); for (final String var : variables.keySet()) { BoolExpr cur = CTX.mkFalse(); for (final String val : variables.get(var)) {