Mercurial > hg > Applications > JavaLite
changeset 64:80db395eeb30 quantifier-worked
*** empty log message ***
author | kono |
---|---|
date | Thu, 10 Jan 2008 18:16:00 +0900 |
parents | d6a300cdd18e |
children | 48db54d3129b |
files | Changes src/lite/BDDSolver.java src/lite/ChopSolver.java src/lite/ExistsSolver.java src/lite/ITLNodeParser.java src/lite/ITLSatisfier.java src/sbdd/BDDSatisfier.java src/sbdd/SBDDTest.java |
diffstat | 8 files changed, 52 insertions(+), 38 deletions(-) [+] |
line wrap: on
line diff
--- a/Changes Thu Jan 10 02:29:46 2008 +0900 +++ b/Changes Thu Jan 10 18:16:00 2008 +0900 @@ -1,3 +1,9 @@ +Thu Jan 10 13:28:26 JST 2008 + +hasChoicePoint は、variable 毎にフラグで持っても良い。 +その方が linear search しなくて良いので少し速い。 +けど、exists との相性は悪い。(かな?) + Wed Jan 9 20:42:17 JST 2008 あぁ、そうか。
--- a/src/lite/BDDSolver.java Thu Jan 10 02:29:46 2008 +0900 +++ b/src/lite/BDDSolver.java Thu Jan 10 18:16:00 2008 +0900 @@ -121,9 +121,11 @@ if (low==null) low = sat.lf.falseNode(); if (high==null) high = sat.lf.falseNode(); // if (cond==null) cond = sat.lf.falseNode(); - return next.sat(sat.lf.orNode( + ITLSolver value = sat.lf.orNode( sat.lf.andNode(cond, high), - sat.lf.andNode(sat.lf.notNode(cond), low))); + sat.lf.andNode(sat.lf.notNode(cond), low)); + if (value==sat.false_) value = null; + return next.sat(value); } } }
--- a/src/lite/ChopSolver.java Thu Jan 10 02:29:46 2008 +0900 +++ b/src/lite/ChopSolver.java Thu Jan 10 18:16:00 2008 +0900 @@ -123,7 +123,9 @@ // we don't have to execute later case now, do it on next clock ITLSolver former1 = sat.lf.chopNode(value,later); // return disjunction with other choice - return next.sat(sat.lf.orNode(later1,former1)); + ITLSolver v = sat.lf.orNode(later1,former1); + if (v==sat.false_) v = null; + return next.sat(v); } } }
--- a/src/lite/ExistsSolver.java Thu Jan 10 02:29:46 2008 +0900 +++ b/src/lite/ExistsSolver.java Thu Jan 10 18:16:00 2008 +0900 @@ -1,7 +1,5 @@ package lite; -import java.util.LinkedList; - import logicNode.parser.TokenID; import sbdd.SBDDFactoryInterface; @@ -11,13 +9,12 @@ ITLSolver node; VariableSolver var; - LinkedList<Boolean> oldVarList; + Boolean old; ITLSolver residue; public ExistsSolver(VariableSolver var, ITLSolver node) { this.node = node; this.var = var; - oldVarList = new LinkedList<Boolean>(); } @@ -27,9 +24,8 @@ @Override public ITLSolver sat(ITLSatisfier sat, Continuation next) throws Backtrack { - boolean old = var.value; - makeLocal(sat); - var.setValue(true); + old = var.value; + makeLocal(sat,true); try { return node.sat(sat, new Continuation(sat,next,this)); } catch (Backtrack e) { @@ -41,20 +37,13 @@ private void restoreLocal(ITLSatisfier sat) { - if (oldVarList.size()>0) { - var.value = oldVarList.getLast(); - oldVarList.removeLast(); - } else { - sat.deleteChoicePoint(var); - } + sat.deleteChoicePoint(var); + var.setValue(old); } - private void makeLocal(ITLSatisfier sat) { - if (sat.hasChoicePoint(var)) { - oldVarList.add(var.value); - } else { - sat.addChoicePoint(var); - } + private void makeLocal(ITLSatisfier sat,boolean newv) { + sat.addChoicePoint(var); + var.setValue(newv); } private ITLSolver restoreLocal(ITLSatisfier sat,boolean now,ITLSolver value,Continuation next) throws Backtrack { @@ -62,8 +51,7 @@ try { return next.sat(value); } catch (Backtrack e) { - makeLocal(sat); - var.setValue(now); + makeLocal(sat,now); throw sat.backtrack; } } @@ -72,14 +60,24 @@ public ITLSolver next(ITLSatisfier sat,Continuation next, ITLSolver value) throws Backtrack { if (value==null) { var.setValue(false); - return node.sat(sat, new Continuation(sat,next ,new ExistsSolver3())); + try { + return node.sat(sat, new Continuation(sat,next ,new ExistsSolver3())); + } catch (Backtrack e) { + var.setValue(true); + throw e; + } } else if (value==sat.true_) { - return restoreLocal(sat,var.value,value,next); + return restoreLocal(sat,true,value,next); } else { var.setValue(false); residue = value; - return node.sat(sat, new Continuation(sat,next, + try { + return node.sat(sat, new Continuation(sat,next, new ExistsSolver2())); + } catch (Backtrack e) { + var.setValue(true); + throw e; + } } } @@ -91,23 +89,24 @@ } else { value = sat.lf.orNode(residue,value); if (value==sat.true_) { + } else if (value==sat.false_) { + value = null; } else { value = sat.lf.existsNode(var,value); } } - return restoreLocal(sat,var.value,value,next); + return restoreLocal(sat,false,value,next); } } class ExistsSolver3 implements Next { - public ITLSolver next(ITLSatisfier sat, Continuation next, ITLSolver value) throws Backtrack { if (value==null) { } else if (value==sat.true_) { } else { value = sat.lf.existsNode(var, value); } - return restoreLocal(sat,var.value,value,next); + return restoreLocal(sat,false,value,next); } }
--- a/src/lite/ITLNodeParser.java Thu Jan 10 02:29:46 2008 +0900 +++ b/src/lite/ITLNodeParser.java Thu Jan 10 18:16:00 2008 +0900 @@ -147,6 +147,7 @@ Node n; LinkedList<Node> arg = new LinkedList<Node>(); while(nextToken.type!=TokenID.CloseParen) { + if (nextToken.type==TokenID.NULL) break; n = exprI2(); arg.add(n); if (nextToken.type == TokenID.And)
--- a/src/lite/ITLSatisfier.java Thu Jan 10 02:29:46 2008 +0900 +++ b/src/lite/ITLSatisfier.java Thu Jan 10 18:16:00 2008 +0900 @@ -12,6 +12,7 @@ */ private static final long serialVersionUID = 1L; public ITLSolver true_; + public ITLSolver false_; public SBDDFactoryInterface lf; public Backtrack backtrack; @@ -20,7 +21,8 @@ public ITLSatisfier() { backtrack = new Backtrack(); - true_ = ITLNodeFactory.trueSolver; + true_ = ITLNodeFactory.trueSolver; + false_ = ITLNodeFactory.falseSolver; } public ITLSatisfier(ITLSolver p) {
--- a/src/sbdd/BDDSatisfier.java Thu Jan 10 02:29:46 2008 +0900 +++ b/src/sbdd/BDDSatisfier.java Thu Jan 10 18:16:00 2008 +0900 @@ -41,6 +41,7 @@ init(); lf = new SBDDFactory(); true_ = SBDDFactory.trueSolver; + false_ = SBDDFactory.falseSolver; state = sf.set(); state.getEntry(SBDDFactory.trueSolver).expanded = true; state.getEntry(SBDDFactory.falseSolver).expanded = true; @@ -95,7 +96,6 @@ queue = new LinkedList<SBDDEntry>(); AllNext allNext = new AllNext(); SBDDEntry b = state.getEntry(n); - this.clear(); // if not empty something wrong if (b.expanded) { // already checked System.out.println(" already checked."); @@ -107,6 +107,10 @@ e.expanded = true; System.out.println(e.key+"->"); develop(e.key, allNext); + if (this.size()>0) { + System.err.println("cb remains "+this); + this.clear(); + } } }
--- a/src/sbdd/SBDDTest.java Thu Jan 10 02:29:46 2008 +0900 +++ b/src/sbdd/SBDDTest.java Thu Jan 10 18:16:00 2008 +0900 @@ -65,15 +65,13 @@ sat.showVerify("exists(x,@@x = ~x)"); sat.showVerify("all(x,@@x)"); sat.showVerify("even(p)"); - sat.showVerify("Q, keep( @Q = ~Q),'[]'((Q->P))"); + sat.showVerify("Q, keep( @Q = ~Q)"); } - sat.showVerify("Q, keep( @Q = ~Q)"); - //sat.showVerify("evenp(p)"); - //at.showVerify("keep(@q = ~q)"); - //sat.showVerify("keep(q)"); + sat.showVerify("even(p)"); + sat.showVerify("evenp(p)"); //sat.showVerify("even(p)<->evenp(p)"); //System.out.println(sat.state); - // sat.p.parse("include('data/example')."); + //sat.p.parse("include('data/example')."); // System.out.println(p.parseCommand.sat.state); }