<commit_before>package edu.kit.iti.formal.pse.worthwhile.prover;

import java.util.ArrayList;
import java.util.Collections;
import java.util.List;
import java.util.Stack;

import edu.kit.iti.formal.pse.worthwhile.model.ast.Assertion;
import edu.kit.iti.formal.pse.worthwhile.model.ast.Assignment;
import edu.kit.iti.formal.pse.worthwhile.model.ast.Assumption;
import edu.kit.iti.formal.pse.worthwhile.model.ast.Axiom;
import edu.kit.iti.formal.pse.worthwhile.model.ast.Block;
import edu.kit.iti.formal.pse.worthwhile.model.ast.Conditional;
import edu.kit.iti.formal.pse.worthwhile.model.ast.Conjunction;
import edu.kit.iti.formal.pse.worthwhile.model.ast.Expression;
import edu.kit.iti.formal.pse.worthwhile.model.ast.ForAllQuantifier;
import edu.kit.iti.formal.pse.worthwhile.model.ast.FunctionDeclaration;
import edu.kit.iti.formal.pse.worthwhile.model.ast.Implication;
import edu.kit.iti.formal.pse.worthwhile.model.ast.Invariant;
import edu.kit.iti.formal.pse.worthwhile.model.ast.Loop;
import edu.kit.iti.formal.pse.worthwhile.model.ast.Negation;
import edu.kit.iti.formal.pse.worthwhile.model.ast.Postcondition;
import edu.kit.iti.formal.pse.worthwhile.model.ast.Precondition;
import edu.kit.iti.formal.pse.worthwhile.model.ast.Program;
import edu.kit.iti.formal.pse.worthwhile.model.ast.QuantifiedExpression;
import edu.kit.iti.formal.pse.worthwhile.model.ast.ReturnStatement;
import edu.kit.iti.formal.pse.worthwhile.model.ast.Statement;
import edu.kit.iti.formal.pse.worthwhile.model.ast.VariableDeclaration;
import edu.kit.iti.formal.pse.worthwhile.model.ast.util.AstNodeCloneHelper;
import edu.kit.iti.formal.pse.worthwhile.model.ast.util.AstNodeCreatorHelper;
import edu.kit.iti.formal.pse.worthwhile.model.ast.visitor.HierarchialASTNodeVisitor;

/**
 * Applies the Weakest Precondition calculus to a {@link Program}.
 */
class WPStrategy extends HierarchialASTNodeVisitor implements FormulaGenerator {
	/**
	 * The stack of weakest preconditions that implies the correctness of the remainder {@link Block}.
	 */
	private Stack<List<Proof>> weakestPreconditionStack;

	/**
	 * The postcondition when visitor is inside an {@link FunctionDeclaration}. This is needed because the original
	 * postcondition may be needed again while proving a function, e.g. when a return statement occurs
	 */
	private List<Proof> currentFunctionPostcondition;

	/**
	 * Construct a new weakest precondition strategy object.
	 */
	public WPStrategy() {
		this.weakestPreconditionStack = new Stack<List<Proof>>();
	}

	/**
	 * @param program
	 *                the {@link Program} to calculate the weakest precondition for
	 * @return the weakest precondition that implies the correctness of <code>program</code>
	 * @see FormulaGenerator#transformProgram(Program program)
	 */
	@Override
	public List<Proof> transformProgram(final Program program) {
		// clear weakestPrecondition state from a previous transformation
		this.weakestPreconditionStack.clear();
		program.accept(this);
		return this.weakestPreconditionStack.pop();
	}

	/**
	 * Visit a {@link Assertion}.
	 * 
	 * @param assertion
	 *                the {@link Assertion} to visit
	 */
	@Override
	public void visit(final Assertion assertion) {
		// add this assertion to the list of things that have to be proven
		this.weakestPreconditionStack.peek().add(
		                new Proof(AstNodeCloneHelper.clone(assertion.getExpression()),
		                                ProofImplication.ASSERTION_VALID, assertion));
	}

	/**
	 * Visit a {@link Assignment} to generate the weakest precondition.
	 * 
	 * @param assignment
	 *                the {@link Assignment} to visit
	 */
	@Override
	public void visit(final Assignment assignment) {
		for (Proof condition : this.weakestPreconditionStack.peek()) {
			final Expression value = assignment.getValue();
			final VariableDeclaration variableDeclaration = assignment.getVariable().getVariable();
			// in every provable condition, substitute the variable declaration
			condition.setExpression(VariableReferenceSubstitution.substitute(condition.getExpression(),
			                variableDeclaration, value));
		}
	}

	/**
	 * Visit an {@link Assumption}.
	 * 
	 * <code><pre>
	 * _assume assumption
	 * </pre></code>
	 * 
	 * to
	 * 
	 * <code><pre>
	 * assumption => wp
	 * </pre></code>
	 * 
	 * @param assumption
	 *                the <code>Assumption</code> to visit
	 */
	@Override
	public void visit(final Assumption assumption) {
		for (Proof condition : this.weakestPreconditionStack.peek()) {
			// add the assumption to every provable expression
			Implication implication = AstNodeCreatorHelper
			                .createImplication(AstNodeCloneHelper.clone(assumption.getExpression()),
			                                condition.getExpression());
			condition.setExpression(implication);
		}
	}

	/**
	 * Visit an {@link Axiom}.
	 * 
	 * <code><pre>
	 * _axiom axiom
	 * </pre></code>
	 * 
	 * to
	 * 
	 * <code><pre>
	 * axiom => wp
	 * </pre></code>
	 * 
	 * @param axiom
	 *                the <code>Axiom</code> to visit
	 */
	@Override
	public void visit(final Axiom axiom) {
		for (Proof condition : this.weakestPreconditionStack.peek()) {
			// add the assumption to every provable expression
			Implication implication = AstNodeCreatorHelper.createImplication(
			                AstNodeCloneHelper.clone(axiom.getExpression()), condition.getExpression());
			condition.setExpression(implication);
		}
	}

	/**
	 * Visit a {@link Block} to generate the weakest precondition.
	 * 
	 * @param block
	 *                the {@link Block} to visit
	 */
	@Override
	public void visit(final Block block) {
		// visit all block statements in the order they were parsed reversed
		List<Statement> stmts = new ArrayList<Statement>(block.getStatements());
		Collections.reverse(stmts);
		for (Statement stmt : stmts) {
			stmt.accept(this);
		}
	}

	/**
	 * Visit a {@link Conditional} to generate the weakest precondition.
	 * 
	 * Transforms
	 * 
	 * <pre>
	 * if condition
	 *     if-block
	 * else
	 *     else-block
	 * </pre>
	 * 
	 * to
	 * 
	 * <pre>
	 * condition => wp(if-block, wp) && !condition => wp(else-block, wp)
	 * </pre>
	 * 
	 * If a <code>else-block</code> is missing <code>wp(else-block, wp)</code> is <code>true</code>.
	 * 
	 * @param conditional
	 *                the {@link Conditional} to visit
	 */
	@Override
	public void visit(final Conditional conditional) {
		List<Proof> preconditionList = new ArrayList<Proof>();
		List<Proof> postconditionList = this.weakestPreconditionStack.pop();

		// calculate weakest precondition so that the true block implies the postcondition
		this.weakestPreconditionStack.push(postconditionList);
		conditional.getTrueBlock().accept(this);
		List<Proof> trueBlockPreconditionList = this.weakestPreconditionStack.pop();

		for (Proof trueBlockPrecondition : trueBlockPreconditionList) {
			// build first implication: condition => wp(if-block, wp)
			Implication conditionImpliesBlockPrecondition = AstNodeCreatorHelper.createImplication(
			                AstNodeCloneHelper.clone(conditional.getCondition()),
			                trueBlockPrecondition.getExpression());
			Proof conditionalPrecondition = trueBlockPrecondition.clone();
			conditionalPrecondition.setExpression(AstNodeCloneHelper.clone(conditionImpliesBlockPrecondition));
			preconditionList.add(conditionalPrecondition);
		}

		// check if the false block even exists
		if (conditional.getFalseBlock() != null) {
			this.weakestPreconditionStack.push(postconditionList);
			// calculate weakest precondition so that false block implies postcondition
			conditional.getFalseBlock().accept(this);
			List<Proof> falseBlockPreconditionList = this.weakestPreconditionStack.pop();

			for (Proof falseBlockPrecondition : falseBlockPreconditionList) {
				// build second implication: !condition => wp(else-block, wp)
				Negation notCondition = AstNodeCreatorHelper.createNegation(AstNodeCloneHelper
				                .clone(conditional.getCondition()));
				Implication notConditionImpliesBlockPrecondition = AstNodeCreatorHelper
				                .createImplication(notCondition, falseBlockPrecondition.getExpression());
				Proof conditionalPrecondition = falseBlockPrecondition.clone();
				conditionalPrecondition.setExpression(notConditionImpliesBlockPrecondition);
				preconditionList.add(conditionalPrecondition);
			}
		} else {
			for (Proof falseBlockPostcondition : postconditionList) {
				// no else block exists, so not the condition should imply the postcondition directly
				Negation notCondition = AstNodeCreatorHelper.createNegation(AstNodeCloneHelper
				                .clone(conditional.getCondition()));
				Implication notConditionImpliesBlockPostcondition = AstNodeCreatorHelper
				                .createImplication(notCondition, AstNodeCloneHelper
				                                .clone(falseBlockPostcondition.getExpression()));
				Proof conditionalPrecondition = falseBlockPostcondition.clone();
				conditionalPrecondition.setExpression(notConditionImpliesBlockPostcondition);
				preconditionList.add(conditionalPrecondition);
			}
		}
		// put updated weakest preconditions for the conjunctions on top of stack
		this.weakestPreconditionStack.push(preconditionList);
	}

	/**
	 * Visit a {@link FunctionDeclaration}.
	 * 
	 * @param functionDeclaration
	 *                the {@link FunctionDeclaration} to visit
	 */
	@Override
	public void visit(final FunctionDeclaration functionDeclaration) {
		// create a single conjuction containing all the ensures
		Expression ensures = AstNodeCreatorHelper.createTrueLiteral();
		for (Precondition e : functionDeclaration.getPreconditions()) {
			ensures = AstNodeCreatorHelper.createConjunction(ensures,
			                AstNodeCloneHelper.clone(e.getExpression()));
		}

		List<Proof> preconditionList = new ArrayList<Proof>();

		// generate a list of Postcondition Proofs that have to be proven
		List<Proof> postconditionList = new ArrayList<Proof>();
		for (Postcondition functionPostcondition : functionDeclaration.getPostconditions()) {
			Proof postconditionProof = new Proof(AstNodeCloneHelper.clone(functionPostcondition
			                .getExpression()), ProofImplication.POSTCONDITION_VALID, functionPostcondition);
			postconditionList.add(postconditionProof);
		}
		// just to be sure that there is anything to prove, add true as a required postcondition
		postconditionList.add(new Proof(AstNodeCreatorHelper.createTrueLiteral(),
		                ProofImplication.POSTCONDITION_VALID, functionDeclaration));

		// calculate wp(loop block, postcondition) for each of the postconditions in the list
		for (Proof postcondition : postconditionList) {
			List<Proof> singlePostconditionList = new ArrayList<Proof>();
			singlePostconditionList.add(postcondition);
			this.currentFunctionPostcondition = singlePostconditionList;
			this.weakestPreconditionStack.add(singlePostconditionList);
			functionDeclaration.getBody().accept(this);
			preconditionList.addAll(this.weakestPreconditionStack.pop());
			this.currentFunctionPostcondition = null;
		}

		for (Proof precondition : preconditionList) {
			// build the weakest precondition for this function: preconditions => wp(body, postconditions)
			precondition.setExpression(AstNodeCreatorHelper.createImplication(
			                AstNodeCloneHelper.clone(ensures), precondition.getExpression()));

			// wrap all the preconditions in foralls because they have to be true for all parameters
			final FreshVariableSetVisitor freshVariableSet = new FreshVariableSetVisitor();
			precondition.getExpression().accept(freshVariableSet);
			for (final VariableDeclaration v : freshVariableSet.getVariableMap().values()) {
				ForAllQuantifier forall = AstNodeCreatorHelper.createForAllQuantifier(v,<commit_msg>[prover] Set related ASTNode to null when proving postcondition true<commit_after>package edu.kit.iti.formal.pse.worthwhile.prover;

import java.util.ArrayList;
import java.util.Collections;
import java.util.List;
import java.util.Stack;

import edu.kit.iti.formal.pse.worthwhile.model.ast.Assertion;
import edu.kit.iti.formal.pse.worthwhile.model.ast.Assignment;
import edu.kit.iti.formal.pse.worthwhile.model.ast.Assumption;
import edu.kit.iti.formal.pse.worthwhile.model.ast.Axiom;
import edu.kit.iti.formal.pse.worthwhile.model.ast.Block;
import edu.kit.iti.formal.pse.worthwhile.model.ast.Conditional;
import edu.kit.iti.formal.pse.worthwhile.model.ast.Conjunction;
import edu.kit.iti.formal.pse.worthwhile.model.ast.Expression;
import edu.kit.iti.formal.pse.worthwhile.model.ast.ForAllQuantifier;
import edu.kit.iti.formal.pse.worthwhile.model.ast.FunctionDeclaration;
import edu.kit.iti.formal.pse.worthwhile.model.ast.Implication;
import edu.kit.iti.formal.pse.worthwhile.model.ast.Invariant;
import edu.kit.iti.formal.pse.worthwhile.model.ast.Loop;
import edu.kit.iti.formal.pse.worthwhile.model.ast.Negation;
import edu.kit.iti.formal.pse.worthwhile.model.ast.Postcondition;
import edu.kit.iti.formal.pse.worthwhile.model.ast.Precondition;
import edu.kit.iti.formal.pse.worthwhile.model.ast.Program;
import edu.kit.iti.formal.pse.worthwhile.model.ast.QuantifiedExpression;
import edu.kit.iti.formal.pse.worthwhile.model.ast.ReturnStatement;
import edu.kit.iti.formal.pse.worthwhile.model.ast.Statement;
import edu.kit.iti.formal.pse.worthwhile.model.ast.VariableDeclaration;
import edu.kit.iti.formal.pse.worthwhile.model.ast.util.AstNodeCloneHelper;
import edu.kit.iti.formal.pse.worthwhile.model.ast.util.AstNodeCreatorHelper;
import edu.kit.iti.formal.pse.worthwhile.model.ast.visitor.HierarchialASTNodeVisitor;

/**
 * Applies the Weakest Precondition calculus to a {@link Program}.
 */
class WPStrategy extends HierarchialASTNodeVisitor implements FormulaGenerator {
	/**
	 * The stack of weakest preconditions that implies the correctness of the remainder {@link Block}.
	 */
	private Stack<List<Proof>> weakestPreconditionStack;

	/**
	 * The postcondition when visitor is inside an {@link FunctionDeclaration}. This is needed because the original
	 * postcondition may be needed again while proving a function, e.g. when a return statement occurs
	 */
	private List<Proof> currentFunctionPostcondition;

	/**
	 * Construct a new weakest precondition strategy object.
	 */
	public WPStrategy() {
		this.weakestPreconditionStack = new Stack<List<Proof>>();
	}

	/**
	 * @param program
	 *                the {@link Program} to calculate the weakest precondition for
	 * @return the weakest precondition that implies the correctness of <code>program</code>
	 * @see FormulaGenerator#transformProgram(Program program)
	 */
	@Override
	public List<Proof> transformProgram(final Program program) {
		// clear weakestPrecondition state from a previous transformation
		this.weakestPreconditionStack.clear();
		program.accept(this);
		return this.weakestPreconditionStack.pop();
	}

	/**
	 * Visit a {@link Assertion}.
	 * 
	 * @param assertion
	 *                the {@link Assertion} to visit
	 */
	@Override
	public void visit(final Assertion assertion) {
		// add this assertion to the list of things that have to be proven
		this.weakestPreconditionStack.peek().add(
		                new Proof(AstNodeCloneHelper.clone(assertion.getExpression()),
		                                ProofImplication.ASSERTION_VALID, assertion));
	}

	/**
	 * Visit a {@link Assignment} to generate the weakest precondition.
	 * 
	 * @param assignment
	 *                the {@link Assignment} to visit
	 */
	@Override
	public void visit(final Assignment assignment) {
		for (Proof condition : this.weakestPreconditionStack.peek()) {
			final Expression value = assignment.getValue();
			final VariableDeclaration variableDeclaration = assignment.getVariable().getVariable();
			// in every provable condition, substitute the variable declaration
			condition.setExpression(VariableReferenceSubstitution.substitute(condition.getExpression(),
			                variableDeclaration, value));
		}
	}

	/**
	 * Visit an {@link Assumption}.
	 * 
	 * <code><pre>
	 * _assume assumption
	 * </pre></code>
	 * 
	 * to
	 * 
	 * <code><pre>
	 * assumption => wp
	 * </pre></code>
	 * 
	 * @param assumption
	 *                the <code>Assumption</code> to visit
	 */
	@Override
	public void visit(final Assumption assumption) {
		for (Proof condition : this.weakestPreconditionStack.peek()) {
			// add the assumption to every provable expression
			Implication implication = AstNodeCreatorHelper
			                .createImplication(AstNodeCloneHelper.clone(assumption.getExpression()),
			                                condition.getExpression());
			condition.setExpression(implication);
		}
	}

	/**
	 * Visit an {@link Axiom}.
	 * 
	 * <code><pre>
	 * _axiom axiom
	 * </pre></code>
	 * 
	 * to
	 * 
	 * <code><pre>
	 * axiom => wp
	 * </pre></code>
	 * 
	 * @param axiom
	 *                the <code>Axiom</code> to visit
	 */
	@Override
	public void visit(final Axiom axiom) {
		for (Proof condition : this.weakestPreconditionStack.peek()) {
			// add the assumption to every provable expression
			Implication implication = AstNodeCreatorHelper.createImplication(
			                AstNodeCloneHelper.clone(axiom.getExpression()), condition.getExpression());
			condition.setExpression(implication);
		}
	}

	/**
	 * Visit a {@link Block} to generate the weakest precondition.
	 * 
	 * @param block
	 *                the {@link Block} to visit
	 */
	@Override
	public void visit(final Block block) {
		// visit all block statements in the order they were parsed reversed
		List<Statement> stmts = new ArrayList<Statement>(block.getStatements());
		Collections.reverse(stmts);
		for (Statement stmt : stmts) {
			stmt.accept(this);
		}
	}

	/**
	 * Visit a {@link Conditional} to generate the weakest precondition.
	 * 
	 * Transforms
	 * 
	 * <pre>
	 * if condition
	 *     if-block
	 * else
	 *     else-block
	 * </pre>
	 * 
	 * to
	 * 
	 * <pre>
	 * condition => wp(if-block, wp) && !condition => wp(else-block, wp)
	 * </pre>
	 * 
	 * If a <code>else-block</code> is missing <code>wp(else-block, wp)</code> is <code>true</code>.
	 * 
	 * @param conditional
	 *                the {@link Conditional} to visit
	 */
	@Override
	public void visit(final Conditional conditional) {
		List<Proof> preconditionList = new ArrayList<Proof>();
		List<Proof> postconditionList = this.weakestPreconditionStack.pop();

		// calculate weakest precondition so that the true block implies the postcondition
		this.weakestPreconditionStack.push(postconditionList);
		conditional.getTrueBlock().accept(this);
		List<Proof> trueBlockPreconditionList = this.weakestPreconditionStack.pop();

		for (Proof trueBlockPrecondition : trueBlockPreconditionList) {
			// build first implication: condition => wp(if-block, wp)
			Implication conditionImpliesBlockPrecondition = AstNodeCreatorHelper.createImplication(
			                AstNodeCloneHelper.clone(conditional.getCondition()),
			                trueBlockPrecondition.getExpression());
			Proof conditionalPrecondition = trueBlockPrecondition.clone();
			conditionalPrecondition.setExpression(AstNodeCloneHelper.clone(conditionImpliesBlockPrecondition));
			preconditionList.add(conditionalPrecondition);
		}

		// check if the false block even exists
		if (conditional.getFalseBlock() != null) {
			this.weakestPreconditionStack.push(postconditionList);
			// calculate weakest precondition so that false block implies postcondition
			conditional.getFalseBlock().accept(this);
			List<Proof> falseBlockPreconditionList = this.weakestPreconditionStack.pop();

			for (Proof falseBlockPrecondition : falseBlockPreconditionList) {
				// build second implication: !condition => wp(else-block, wp)
				Negation notCondition = AstNodeCreatorHelper.createNegation(AstNodeCloneHelper
				                .clone(conditional.getCondition()));
				Implication notConditionImpliesBlockPrecondition = AstNodeCreatorHelper
				                .createImplication(notCondition, falseBlockPrecondition.getExpression());
				Proof conditionalPrecondition = falseBlockPrecondition.clone();
				conditionalPrecondition.setExpression(notConditionImpliesBlockPrecondition);
				preconditionList.add(conditionalPrecondition);
			}
		} else {
			for (Proof falseBlockPostcondition : postconditionList) {
				// no else block exists, so not the condition should imply the postcondition directly
				Negation notCondition = AstNodeCreatorHelper.createNegation(AstNodeCloneHelper
				                .clone(conditional.getCondition()));
				Implication notConditionImpliesBlockPostcondition = AstNodeCreatorHelper
				                .createImplication(notCondition, AstNodeCloneHelper
				                                .clone(falseBlockPostcondition.getExpression()));
				Proof conditionalPrecondition = falseBlockPostcondition.clone();
				conditionalPrecondition.setExpression(notConditionImpliesBlockPostcondition);
				preconditionList.add(conditionalPrecondition);
			}
		}
		// put updated weakest preconditions for the conjunctions on top of stack
		this.weakestPreconditionStack.push(preconditionList);
	}

	/**
	 * Visit a {@link FunctionDeclaration}.
	 * 
	 * @param functionDeclaration
	 *                the {@link FunctionDeclaration} to visit
	 */
	@Override
	public void visit(final FunctionDeclaration functionDeclaration) {
		// create a single conjuction containing all the ensures
		Expression ensures = AstNodeCreatorHelper.createTrueLiteral();
		for (Precondition e : functionDeclaration.getPreconditions()) {
			ensures = AstNodeCreatorHelper.createConjunction(ensures,
			                AstNodeCloneHelper.clone(e.getExpression()));
		}

		List<Proof> preconditionList = new ArrayList<Proof>();

		// generate a list of Postcondition Proofs that have to be proven
		List<Proof> postconditionList = new ArrayList<Proof>();
		for (Postcondition functionPostcondition : functionDeclaration.getPostconditions()) {
			Proof postconditionProof = new Proof(AstNodeCloneHelper.clone(functionPostcondition
			                .getExpression()), ProofImplication.POSTCONDITION_VALID, functionPostcondition);
			postconditionList.add(postconditionProof);
		}
		// just to be sure that there is anything to prove, add true as a required postcondition
		postconditionList.add(new Proof(AstNodeCreatorHelper.createTrueLiteral(),
		                ProofImplication.POSTCONDITION_VALID, null));

		// calculate wp(loop block, postcondition) for each of the postconditions in the list
		for (Proof postcondition : postconditionList) {
			List<Proof> singlePostconditionList = new ArrayList<Proof>();
			singlePostconditionList.add(postcondition);
			this.currentFunctionPostcondition = singlePostconditionList;
			this.weakestPreconditionStack.add(singlePostconditionList);
			functionDeclaration.getBody().accept(this);
			preconditionList.addAll(this.weakestPreconditionStack.pop());
			this.currentFunctionPostcondition = null;
		}

		for (Proof precondition : preconditionList) {
			// build the weakest precondition for this function: preconditions => wp(body, postconditions)
			precondition.setExpression(AstNodeCreatorHelper.createImplication(
			                AstNodeCloneHelper.clone(ensures), precondition.getExpression()));

			// wrap all the preconditions in foralls because they have to be true for all parameters
			final FreshVariableSetVisitor freshVariableSet = new FreshVariableSetVisitor();
			precondition.getExpression().accept(freshVariableSet);
			for (final VariableDeclaration v : freshVariableSet.getVariableMap().values()) {
				ForAllQuantifier forall = AstNodeCreatorHelper.createForAllQuantifier(v,
{'fraction_non_alphanumeric': 0.10001689474573408, 'fraction_numerical': 0.0, 'mean_word_length': 3.98253367003367, 'pattern_counts': {'":': 0, '<': 105, '<?xml version=': 0, '>': 119, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '1121787', 'n_tokens_mistral': 7210, 'n_tokens_neox': 6372, 'n_words': 1462}