Package kodkod.ast

Examples of kodkod.ast.Decl.variable()

393
394
395
396
397
398
399
400
401
402
403
      final List<Formula> domConstraints = new LinkedList<Formula>();
     
      for(Decl decl : decls) { 
        final Decl skolemDecl = visit(decl);
       
        final Relation skolem = Relation.nary("$"+ skolemDecl.variable().name(), nonSkolems.size() + skolemDecl.variable().arity());
        reporter.skolemizing(decl, skolem, nonSkolemsView);
       
        final Expression skolemExpr = skolemExpr(skolemDecl, skolem);
       
        final Multiplicity mult = decl.multiplicity();
View Full Code Here
393
394
395
396
397
398
399
400
401
402
403
      final List<Formula> domConstraints = new LinkedList<Formula>();
     
      for(Decl decl : decls) { 
        final Decl skolemDecl = visit(decl);
       
        final Relation skolem = Relation.nary("$"+ skolemDecl.variable().name(), nonSkolems.size() + skolemDecl.variable().arity());
        reporter.skolemizing(decl, skolem, nonSkolemsView);
       
        final Expression skolemExpr = skolemExpr(skolemDecl, skolem);
       
        final Multiplicity mult = decl.multiplicity();
View Full Code Here
420
421
422
423
424
425
426
427
428
429
430
    final Decl decl = decls.get(currentDecl);
    final BooleanMatrix declTransl = visit(decl);
    final int position = (int)StrictMath.pow(interpreter.universe().size(), decls.size()-currentDecl-1);
    final BooleanMatrix groundValue = factory.matrix(declTransl.dimensions());
    env = env.extend(decl.variable(), groundValue);
    for(IndexedEntry<BooleanValue> entry : declTransl) {
      groundValue.set(entry.index(), BooleanConstant.TRUE);
      comprehension(decls, formula, currentDecl+1, factory.and(entry.value(), declConstraints),
          partialIndex + entry.index()*position, matrix);
      groundValue.set(entry.index(), BooleanConstant.FALSE); 
View Full Code Here
519
520
521
522
523
524
525
526
527
528
529
    }

    final Decl decl = decls.get(currentDecl);
    final BooleanMatrix declTransl = visit(decl);
    final BooleanMatrix groundValue = factory.matrix(declTransl.dimensions());
    env = env.extend(decl.variable(), groundValue);
    for(IndexedEntry<BooleanValue> entry : declTransl) {
      groundValue.set(entry.index(), BooleanConstant.TRUE);
      all(decls, formula, currentDecl+1, factory.or(factory.not(entry.value()), declConstraints), acc);
      groundValue.set(entry.index(), BooleanConstant.FALSE); 
    }
View Full Code Here
555
556
557
558
559
560
561
562
563
564
565
    }

    final Decl decl = decls.get(currentDecl);
    final BooleanMatrix declTransl = visit(decl);
    final BooleanMatrix groundValue = factory.matrix(declTransl.dimensions());
    env = env.extend(decl.variable(), groundValue);
    for(IndexedEntry<BooleanValue> entry : declTransl) {
      groundValue.set(entry.index(), BooleanConstant.TRUE);
      some(decls, formula, currentDecl+1, factory.and(entry.value(), declConstraints), acc);
      groundValue.set(entry.index(), BooleanConstant.FALSE); 
    }
View Full Code Here
950
951
952
953
954
955
956
957
958
959
960
    }

    final Decl decl = decls.get(currentDecl);
    final BooleanMatrix declTransl = visit(decl);
    final BooleanMatrix groundValue = factory.matrix(declTransl.dimensions());
    env = env.extend(decl.variable(), groundValue);
    for(IndexedEntry<BooleanValue> entry : declTransl) {
      groundValue.set(entry.index(), BooleanConstant.TRUE);
      sum(decls, expr, currentDecl+1, factory.and(entry.value(), declConstraints), values);
      groundValue.set(entry.index(), BooleanConstant.FALSE); 
    }
View Full Code Here
TOP
Copyright © 2018 www.massapi.com. All rights reserved.
All source code are property of their respective owners. Java is a trademark of Sun Microsystems, Inc and owned by ORACLE Inc. Contact coftware#gmail.com.