/** */ package hu.bme.mit.inf.dslreasoner.smtLanguage; import org.eclipse.emf.ecore.EFactory; /** * * The Factory for the model. * It provides a create method for each non-abstract class of the model. * * @see hu.bme.mit.inf.dslreasoner.smtLanguage.SmtLanguagePackage * @generated */ public interface SmtLanguageFactory extends EFactory { /** * The singleton instance of the factory. * * * @generated */ SmtLanguageFactory eINSTANCE = hu.bme.mit.inf.dslreasoner.smtLanguage.impl.SmtLanguageFactoryImpl.init(); /** * Returns a new object of class 'SMT Document'. * * * @return a new object of class 'SMT Document'. * @generated */ SMTDocument createSMTDocument(); /** * Returns a new object of class 'SMT Input'. * * * @return a new object of class 'SMT Input'. * @generated */ SMTInput createSMTInput(); /** * Returns a new object of class 'SMT Output'. * * * @return a new object of class 'SMT Output'. * @generated */ SMTOutput createSMTOutput(); /** * Returns a new object of class 'SMT Option'. * * * @return a new object of class 'SMT Option'. * @generated */ SMTOption createSMTOption(); /** * Returns a new object of class 'SMT Type'. * * * @return a new object of class 'SMT Type'. * @generated */ SMTType createSMTType(); /** * Returns a new object of class 'SMT Enum Literal'. * * * @return a new object of class 'SMT Enum Literal'. * @generated */ SMTEnumLiteral createSMTEnumLiteral(); /** * Returns a new object of class 'SMT Enumerated Type Declaration'. * * * @return a new object of class 'SMT Enumerated Type Declaration'. * @generated */ SMTEnumeratedTypeDeclaration createSMTEnumeratedTypeDeclaration(); /** * Returns a new object of class 'SMT Set Type Declaration'. * * * @return a new object of class 'SMT Set Type Declaration'. * @generated */ SMTSetTypeDeclaration createSMTSetTypeDeclaration(); /** * Returns a new object of class 'SMT Type Reference'. * * * @return a new object of class 'SMT Type Reference'. * @generated */ SMTTypeReference createSMTTypeReference(); /** * Returns a new object of class 'SMT Complex Type Reference'. * * * @return a new object of class 'SMT Complex Type Reference'. * @generated */ SMTComplexTypeReference createSMTComplexTypeReference(); /** * Returns a new object of class 'SMT Primitive Type Reference'. * * * @return a new object of class 'SMT Primitive Type Reference'. * @generated */ SMTPrimitiveTypeReference createSMTPrimitiveTypeReference(); /** * Returns a new object of class 'SMT Int Type Reference'. * * * @return a new object of class 'SMT Int Type Reference'. * @generated */ SMTIntTypeReference createSMTIntTypeReference(); /** * Returns a new object of class 'SMT Bool Type Reference'. * * * @return a new object of class 'SMT Bool Type Reference'. * @generated */ SMTBoolTypeReference createSMTBoolTypeReference(); /** * Returns a new object of class 'SMT Real Type Reference'. * * * @return a new object of class 'SMT Real Type Reference'. * @generated */ SMTRealTypeReference createSMTRealTypeReference(); /** * Returns a new object of class 'SMT Function Declaration'. * * * @return a new object of class 'SMT Function Declaration'. * @generated */ SMTFunctionDeclaration createSMTFunctionDeclaration(); /** * Returns a new object of class 'SMT Function Definition'. * * * @return a new object of class 'SMT Function Definition'. * @generated */ SMTFunctionDefinition createSMTFunctionDefinition(); /** * Returns a new object of class 'SMT Term'. * * * @return a new object of class 'SMT Term'. * @generated */ SMTTerm createSMTTerm(); /** * Returns a new object of class 'SMT Symbolic Declaration'. * * * @return a new object of class 'SMT Symbolic Declaration'. * @generated */ SMTSymbolicDeclaration createSMTSymbolicDeclaration(); /** * Returns a new object of class 'SMT Symbolic Value'. * * * @return a new object of class 'SMT Symbolic Value'. * @generated */ SMTSymbolicValue createSMTSymbolicValue(); /** * Returns a new object of class 'SMT Atomic Term'. * * * @return a new object of class 'SMT Atomic Term'. * @generated */ SMTAtomicTerm createSMTAtomicTerm(); /** * Returns a new object of class 'SMT Int Literal'. * * * @return a new object of class 'SMT Int Literal'. * @generated */ SMTIntLiteral createSMTIntLiteral(); /** * Returns a new object of class 'SMT Bool Literal'. * * * @return a new object of class 'SMT Bool Literal'. * @generated */ SMTBoolLiteral createSMTBoolLiteral(); /** * Returns a new object of class 'SMT Real Literal'. * * * @return a new object of class 'SMT Real Literal'. * @generated */ SMTRealLiteral createSMTRealLiteral(); /** * Returns a new object of class 'SMT Sorted Variable'. * * * @return a new object of class 'SMT Sorted Variable'. * @generated */ SMTSortedVariable createSMTSortedVariable(); /** * Returns a new object of class 'SMT Quantified Expression'. * * * @return a new object of class 'SMT Quantified Expression'. * @generated */ SMTQuantifiedExpression createSMTQuantifiedExpression(); /** * Returns a new object of class 'SMT Exists'. * * * @return a new object of class 'SMT Exists'. * @generated */ SMTExists createSMTExists(); /** * Returns a new object of class 'SMT Forall'. * * * @return a new object of class 'SMT Forall'. * @generated */ SMTForall createSMTForall(); /** * Returns a new object of class 'SMT Bool Operation'. * * * @return a new object of class 'SMT Bool Operation'. * @generated */ SMTBoolOperation createSMTBoolOperation(); /** * Returns a new object of class 'SMT And'. * * * @return a new object of class 'SMT And'. * @generated */ SMTAnd createSMTAnd(); /** * Returns a new object of class 'SMT Or'. * * * @return a new object of class 'SMT Or'. * @generated */ SMTOr createSMTOr(); /** * Returns a new object of class 'SMT Impl'. * * * @return a new object of class 'SMT Impl'. * @generated */ SMTImpl createSMTImpl(); /** * Returns a new object of class 'SMT Not'. * * * @return a new object of class 'SMT Not'. * @generated */ SMTNot createSMTNot(); /** * Returns a new object of class 'SMT Iff'. * * * @return a new object of class 'SMT Iff'. * @generated */ SMTIff createSMTIff(); /** * Returns a new object of class 'SMTITE'. * * * @return a new object of class 'SMTITE'. * @generated */ SMTITE createSMTITE(); /** * Returns a new object of class 'SMT Let'. * * * @return a new object of class 'SMT Let'. * @generated */ SMTLet createSMTLet(); /** * Returns a new object of class 'SMT Inline Constant Definition'. * * * @return a new object of class 'SMT Inline Constant Definition'. * @generated */ SMTInlineConstantDefinition createSMTInlineConstantDefinition(); /** * Returns a new object of class 'SMT Relation'. * * * @return a new object of class 'SMT Relation'. * @generated */ SMTRelation createSMTRelation(); /** * Returns a new object of class 'SMT Equals'. * * * @return a new object of class 'SMT Equals'. * @generated */ SMTEquals createSMTEquals(); /** * Returns a new object of class 'SMT Distinct'. * * * @return a new object of class 'SMT Distinct'. * @generated */ SMTDistinct createSMTDistinct(); /** * Returns a new object of class 'SMTLT'. * * * @return a new object of class 'SMTLT'. * @generated */ SMTLT createSMTLT(); /** * Returns a new object of class 'SMTMT'. * * * @return a new object of class 'SMTMT'. * @generated */ SMTMT createSMTMT(); /** * Returns a new object of class 'SMTLEQ'. * * * @return a new object of class 'SMTLEQ'. * @generated */ SMTLEQ createSMTLEQ(); /** * Returns a new object of class 'SMTMEQ'. * * * @return a new object of class 'SMTMEQ'. * @generated */ SMTMEQ createSMTMEQ(); /** * Returns a new object of class 'SMT Int Operation'. * * * @return a new object of class 'SMT Int Operation'. * @generated */ SMTIntOperation createSMTIntOperation(); /** * Returns a new object of class 'SMT Plus'. * * * @return a new object of class 'SMT Plus'. * @generated */ SMTPlus createSMTPlus(); /** * Returns a new object of class 'SMT Minus'. * * * @return a new object of class 'SMT Minus'. * @generated */ SMTMinus createSMTMinus(); /** * Returns a new object of class 'SMT Multiply'. * * * @return a new object of class 'SMT Multiply'. * @generated */ SMTMultiply createSMTMultiply(); /** * Returns a new object of class 'SMT Divison'. * * * @return a new object of class 'SMT Divison'. * @generated */ SMTDivison createSMTDivison(); /** * Returns a new object of class 'SMT Div'. * * * @return a new object of class 'SMT Div'. * @generated */ SMTDiv createSMTDiv(); /** * Returns a new object of class 'SMT Mod'. * * * @return a new object of class 'SMT Mod'. * @generated */ SMTMod createSMTMod(); /** * Returns a new object of class 'SMT Assertion'. * * * @return a new object of class 'SMT Assertion'. * @generated */ SMTAssertion createSMTAssertion(); /** * Returns a new object of class 'SMT Cardinality Constraint'. * * * @return a new object of class 'SMT Cardinality Constraint'. * @generated */ SMTCardinalityConstraint createSMTCardinalityConstraint(); /** * Returns a new object of class 'SMT Sat Command'. * * * @return a new object of class 'SMT Sat Command'. * @generated */ SMTSatCommand createSMTSatCommand(); /** * Returns a new object of class 'SMT Simple Sat Command'. * * * @return a new object of class 'SMT Simple Sat Command'. * @generated */ SMTSimpleSatCommand createSMTSimpleSatCommand(); /** * Returns a new object of class 'SMT Complex Sat Command'. * * * @return a new object of class 'SMT Complex Sat Command'. * @generated */ SMTComplexSatCommand createSMTComplexSatCommand(); /** * Returns a new object of class 'SMT Get Model Command'. * * * @return a new object of class 'SMT Get Model Command'. * @generated */ SMTGetModelCommand createSMTGetModelCommand(); /** * Returns a new object of class 'SMT Reasoning Tactic'. * * * @return a new object of class 'SMT Reasoning Tactic'. * @generated */ SMTReasoningTactic createSMTReasoningTactic(); /** * Returns a new object of class 'SMT Builtin Tactic'. * * * @return a new object of class 'SMT Builtin Tactic'. * @generated */ SMTBuiltinTactic createSMTBuiltinTactic(); /** * Returns a new object of class 'SMT Reasoning Combinator'. * * * @return a new object of class 'SMT Reasoning Combinator'. * @generated */ SMTReasoningCombinator createSMTReasoningCombinator(); /** * Returns a new object of class 'SMT And Then Combinator'. * * * @return a new object of class 'SMT And Then Combinator'. * @generated */ SMTAndThenCombinator createSMTAndThenCombinator(); /** * Returns a new object of class 'SMT Or Else Combinator'. * * * @return a new object of class 'SMT Or Else Combinator'. * @generated */ SMTOrElseCombinator createSMTOrElseCombinator(); /** * Returns a new object of class 'SMT Par Or Combinator'. * * * @return a new object of class 'SMT Par Or Combinator'. * @generated */ SMTParOrCombinator createSMTParOrCombinator(); /** * Returns a new object of class 'SMT Par Then Combinator'. * * * @return a new object of class 'SMT Par Then Combinator'. * @generated */ SMTParThenCombinator createSMTParThenCombinator(); /** * Returns a new object of class 'SMT Try For Combinator'. * * * @return a new object of class 'SMT Try For Combinator'. * @generated */ SMTTryForCombinator createSMTTryForCombinator(); /** * Returns a new object of class 'SMT If Combinator'. * * * @return a new object of class 'SMT If Combinator'. * @generated */ SMTIfCombinator createSMTIfCombinator(); /** * Returns a new object of class 'SMT When Combinator'. * * * @return a new object of class 'SMT When Combinator'. * @generated */ SMTWhenCombinator createSMTWhenCombinator(); /** * Returns a new object of class 'SMT Fail If Combinator'. * * * @return a new object of class 'SMT Fail If Combinator'. * @generated */ SMTFailIfCombinator createSMTFailIfCombinator(); /** * Returns a new object of class 'SMT Using Param Combinator'. * * * @return a new object of class 'SMT Using Param Combinator'. * @generated */ SMTUsingParamCombinator createSMTUsingParamCombinator(); /** * Returns a new object of class 'Reasoning Probe'. * * * @return a new object of class 'Reasoning Probe'. * @generated */ ReasoningProbe createReasoningProbe(); /** * Returns a new object of class 'Reasoning Tactic Parameter'. * * * @return a new object of class 'Reasoning Tactic Parameter'. * @generated */ ReasoningTacticParameter createReasoningTacticParameter(); /** * Returns a new object of class 'SMT Result'. * * * @return a new object of class 'SMT Result'. * @generated */ SMTResult createSMTResult(); /** * Returns a new object of class 'SMT Error Result'. * * * @return a new object of class 'SMT Error Result'. * @generated */ SMTErrorResult createSMTErrorResult(); /** * Returns a new object of class 'SMT Unsupported Result'. * * * @return a new object of class 'SMT Unsupported Result'. * @generated */ SMTUnsupportedResult createSMTUnsupportedResult(); /** * Returns a new object of class 'SMT Sat Result'. * * * @return a new object of class 'SMT Sat Result'. * @generated */ SMTSatResult createSMTSatResult(); /** * Returns a new object of class 'SMT Model Result'. * * * @return a new object of class 'SMT Model Result'. * @generated */ SMTModelResult createSMTModelResult(); /** * Returns a new object of class 'SMT Statistic Value'. * * * @return a new object of class 'SMT Statistic Value'. * @generated */ SMTStatisticValue createSMTStatisticValue(); /** * Returns a new object of class 'SMT Statistic Int Value'. * * * @return a new object of class 'SMT Statistic Int Value'. * @generated */ SMTStatisticIntValue createSMTStatisticIntValue(); /** * Returns a new object of class 'SMT Statistic Double Value'. * * * @return a new object of class 'SMT Statistic Double Value'. * @generated */ SMTStatisticDoubleValue createSMTStatisticDoubleValue(); /** * Returns a new object of class 'SMT Statistics Section'. * * * @return a new object of class 'SMT Statistics Section'. * @generated */ SMTStatisticsSection createSMTStatisticsSection(); /** * Returns the package supported by this factory. * * * @return the package supported by this factory. * @generated */ SmtLanguagePackage getSmtLanguagePackage(); } //SmtLanguageFactory