<commit_before>package perseus.abstractions;

import manticore.dl.*;

public class SolverResult {
    
    public final String satisfiability;
    public final String validity;
    public final Valuation valuation;

    public SolverResult( String satisfiability, String validity, Valuation valuation ) 
    		throws SolverResultIntegrityException {
	this.satisfiability = satisfiability;
	this.validity = validity;
	this.valuation = valuation;

	checkIntegrity();
    }

    public String toString() {
    	    return "(Solver result:\n\tsatisfiability: " + satisfiability 
    	    		+ "\n\tvaluation: " 
    	    		+ valuation.toString() +"\n)\n";
    }

    public void checkIntegrity() throws SolverResultIntegrityException {

	// Check that validity contains a validity string
	if ( !validity.equals("valid")
		&& !validity.equals("notvalid")
		&& !validity.equals("unknown") ) {
		throw new SolverResultIntegrityException( "Incorrect validity string:\n" + this.toString() );
	}

	// Check that satisfiability contains a satisfiability string
	if ( !satisfiability.equals("sat")
		&& !satisfiability.equals("unsat")
		&& !satisfiability.equals("delta-sat")
		&& !satisfiability.equals("unknown") ) {
		throw new SolverResultIntegrityException( "Incorrect satisfiability string:\n" + this.toString() );

	}

	// Check that it is not both unsat and valid
	if ( satisfiability.equals("unsat")
		&& validity.equals("valid") ) {
		throw new SolverResultIntegrityException("Result cannot be unsat and valid:\n" + this.toString() );
	}

	// If it's unsat, you better not be giving me a valuation
	if ( satisfiability.equals("unsat") && !valuation.isEmpty() ) {
		throw new SolverResultIntegrityException("Valuation given for purportedly unsat formula\n" 
								+ this.toString() );
	}

	// Make sure I get a valuation when you tell me there is one
//	if ( satisfiability.equals("sat") && valuation == null ) {
//		throw new SolverResultIntegrityException("Formula is allegedly sat, but no valuation is given\n" 
//								+ this.toString() );
//	}

//	if ( validity.equals("valid") && valuation == null ) {
//		throw new SolverResultIntegrityException("Formula is allegedly valid, but no valuation is given\n" 
//								+ this.toString() );
//	}

	if ( satisfiability.equals("unsat") && !validity.equals("notvalid") ) {
		throw new SolverResultIntegrityException("If formula is unsat, it can't be valid\n" 
								+ this.toString() );

	}
   }


}


    
    
<commit_msg>another detail<commit_after>package perseus.abstractions;

import manticore.dl.*;

public class SolverResult {
    
    public final String satisfiability;
    public final String validity;
    public final Valuation valuation;

    public SolverResult( String satisfiability, String validity, Valuation valuation ) 
    		throws SolverResultIntegrityException {
	this.satisfiability = satisfiability;
	this.validity = validity;
	this.valuation = valuation;

	checkIntegrity();
    }

    public String toString() {
    	    return "(Solver result:\n\tsatisfiability: " + satisfiability 
    	    		+ "\n\tvaluation: " 
    	    		+ valuation.toString() +"\n)\n";
    }

    public void checkIntegrity() throws SolverResultIntegrityException {

	// Check that validity contains a validity string
	if ( !validity.equals("valid")
		&& !validity.equals("notvalid")
		&& !validity.equals("unknown") ) {
		throw new SolverResultIntegrityException( "Incorrect validity string:\n" + this.toString() );
	}

	// Check that satisfiability contains a satisfiability string
	if ( !satisfiability.equals("sat")
		&& !satisfiability.equals("unsat")
		&& !satisfiability.equals("delta-sat")
		&& !satisfiability.equals("unknown") ) {
		throw new SolverResultIntegrityException( "Incorrect satisfiability string:\n" + this.toString() );

	}

	// Check that it is not both unsat and valid
	if ( satisfiability.equals("unsat")
		&& validity.equals("valid") ) {
		throw new SolverResultIntegrityException("Result cannot be unsat and valid:\n" + this.toString() );
	}

	// If it's unsat, you better not be giving me a valuation
	if ( satisfiability.equals("unsat") && !valuation.isEmpty() ) {
		throw new SolverResultIntegrityException("Valuation given for purportedly unsat formula\n" 
								+ this.toString() );
	}

	// Make sure I get a valuation when you tell me there is one
//	if ( satisfiability.equals("sat") && valuation == null ) {
//		throw new SolverResultIntegrityException("Formula is allegedly sat, but no valuation is given\n" 
//								+ this.toString() );
//	}

//	if ( validity.equals("valid") && valuation == null ) {
//		throw new SolverResultIntegrityException("Formula is allegedly valid, but no valuation is given\n" 
//								+ this.toString() );
//	}

   }


}


    
    

{'fraction_non_alphanumeric': 0.12211013030685162, 'fraction_numerical': 0.0, 'mean_word_length': 3.652003910068426, 'pattern_counts': {'":': 0, '<': 3, '<?xml version=': 0, '>': 3, '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': '5197373', 'n_tokens_mistral': 1565, 'n_tokens_neox': 1423, 'n_words': 371}