/**
*/
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