import { Decider , Decision , ImplicationProofItem , Property , PropertyFactory , Quantifier , QuantifierResult , } from '../../types' ; import { CannotDecideError } from './utils' ; export interface ForAllSuchThatInput { quantifier : Quantifier ; quantifierParameters : any ; propertyFactory : PropertyFactory ; } /**
 * Decider that decides true iff the provided quantifier quantifies all results and they all evaluate to true.
 * If any evaluates to false, it will decide false. Otherwise, it is undecidable.
 */ export class ForAllSuchThatDecider implements Decider { private static _instance : ForAllSuchThatDecider ; public static instance ( ) { if ( ! ForAllSuchThatDecider . _instance ) { ForAllSuchThatDecider . _instance = new ForAllSuchThatDecider ( ) ; } return ForAllSuchThatDecider . _instance ; } public async decide ( input , noCache ? ) { const quantifierResult = await input . quantifier . getAllQuantified ( input . quantifierParameters ) ; let anyUndecided = false ; let falseDecision ; const trueDecisions = [ ] ; for ( const res of quantifierResult . results ) { const prop = input . propertyFactory ( res ) ; try { const decision = await prop . decider . decide ( prop . input , noCache ) ; if ( ! decision . outcome ) { falseDecision = decision ; break ; } trueDecisions . push ( decision ) ; } catch ( e ) { if ( e instanceof CannotDecideError ) { anyUndecided = true ; } else { throw e ; } } } return this . getDecision ( input , falseDecision , trueDecisions , anyUndecided || ! quantifierResult . allResultsQuantified ) ; } param input param falseDecision param trueDecisions param undecided returns private getDecision ( input , falseDecision , trueDecisions , undecided ) { if ( ! falseDecision && undecided ) { throw new CannotDecideError ( 'Cannot decide ForAllSuchThat due to undecided Decision or not all results being quantified.' ) ; } const justification = [ { implication : { decider : this , input , } , implicationWitness : undefined , } , ] ; if ( ! ! falseDecision ) { justification . push ( ... falseDecision . justification ) ; } else { for ( const decision of trueDecisions ) { justification . push ( ... decision . justification ) ; } } return { outcome : ! falseDecision , justification , } ; } }