PathUtils { public static Valuation extractValuation(final Valuation model, final VarIndexing indexing) { final ImmutableValuation.Builder builder = ImmutableValuation.builder(); for (final Decl<?> decl : model.getDecls()) { if (decl instanceof IndexedConstDecl) { final IndexedConstDecl<?> indexedConstDecl = (IndexedConstDecl<?>) decl; final VarDecl<?> varDecl = indexedConstDecl.getVarDecl(); if (indexedConstDecl.getIndex() == indexing.get(varDecl)) { final LitExpr<?> value = model.eval(indexedConstDecl).get(); builder.put(varDecl, value); } } } return builder.build(); } private  PathUtils(); static VarIndexing countPrimes(final Expr<?> expr); static Expr<T> unfold(final Expr<T> expr, final VarIndexing indexing); static Expr<T> unfold(final Expr<T> expr, final int i); static Expr<T> foldin(final Expr<T> expr, final VarIndexing indexing); static Expr<T> foldin(final Expr<T> expr, final int i); static Valuation extractValuation(final Valuation model, final VarIndexing indexing); static Valuation extractValuation(final Valuation model, final int i); static Valuation extractValuation(final Valuation model, final VarIndexing indexing,
											 final Collection<? extends VarDecl<?>> varDecls); static Valuation extractValuation(final Valuation model, final int i,
											 final Collection<? extends VarDecl<?>> varDecls);  }
@Test public void testExtractValuation() { final Valuation valuation = ImmutableValuation.builder().put(x1, Int(1)).put(x2, Int(2)).put(y1, Int(3)) .build(); final Valuation extr0 = PathUtils.extractValuation(valuation, 1); Assert.assertEquals(2, extr0.getDecls().size()); Assert.assertEquals(Int(1), extr0.eval(vx).get()); Assert.assertEquals(Int(3), extr0.eval(vy).get()); final Valuation extr1 = PathUtils.extractValuation(valuation, 1, ImmutableSet.of(vx, vz)); Assert.assertEquals(1, extr1.getDecls().size()); Assert.assertEquals(Int(1), extr1.eval(vx).get()); }