Z3: SMT solver

00001 /*++
00002 Copyright (c) 2007 Microsoft Corporation
00003 
00004 Module Name:
00005 
00006     Microsoft.Z3.h
00007 
00008 Abstract:
00009 
00010     Z3 Managed API.
00011 
00012 Author:
00013 
00014     Nikolaj Bjorner (nbjorner)
00015     Leonardo de Moura (leonardo) 2007-06-8
00016 
00017 Notes:
00018     
00019 --*/
00020 
00021 #ifndef _MICROSOFT_Z3_H__
00022 #define _MICROSOFT_Z3_H__
00023 
00024 struct _Z3_model {};
00025 struct _Z3_config {};
00026 struct _Z3_context {};
00027 struct _Z3_func_decl {};
00028 struct _Z3_app {};
00029 struct _Z3_sort {};
00030 struct _Z3_symbol {};
00031 struct _Z3_ast {};
00032 struct _Z3_literals {};
00033 struct _Z3_pattern {};
00034 struct _Z3_constructor {};
00035 struct _Z3_constructor_list {};
00036 typedef _Z3_literals *Z3_literals;
00037 
00038 using namespace System;
00039 using namespace System::Collections::Generic;
00040 
00041 
00042 #include "..\lib\z3.h"
00043 #include "..\lib\z3_private.h"
00044 
00045 namespace Microsoft {
00046 namespace Z3 {
00047 
00052 
00058     public ref class Symbol {
00059         Z3_symbol m_symbol;
00060     internal:
00061         Symbol(Z3_symbol s) : m_symbol(s) {}
00062         Z3_symbol get() { return m_symbol; }      
00063     };
00064 
00073     public enum class LBool
00074     {
00075         True,
00076         False,
00077         Undef
00078     };
00079 
00104     public enum class ErrorCode 
00105     {
00106         Ok,
00107         TypeError,
00108         IndexOutOfBounds,
00109         InvalidArgument,
00110         ParserError,
00111         NoParser,
00112         InvalidPattern,
00113         InternalFatal,
00114         FileAccessError,
00115         NonDisposedConfig,
00116         NonDisposedContext,
00117         NonDisposedLiterals,
00118         NonDisposedModel
00119     };
00120 
00127     public enum class PrintMode 
00128     {
00129         SmtlibFull,
00130         LowLevel
00131     };
00132 
00139     public ref class Z3Error : Exception {
00140     public:
00141         Z3Error(ErrorCode c) { Code = c; InternalCode = 0; }
00142         Z3Error(int i) { Code = ErrorCode::Ok; InternalCode = i; }
00143         ErrorCode Code;
00144         int       InternalCode;
00145     };
00146 
00147     
00149     typedef IntPtr AstPtr;
00150     typedef IntPtr SortPtr;
00151     typedef IntPtr FuncDeclPtr;
00152     typedef IntPtr TermPtr;
00153     typedef IntPtr PatternPtr;
00154     typedef IntPtr AppPtr;
00155 
00156 
00157     Z3_sort get_sort_ast(SortPtr t) { 
00158         if (t == IntPtr::Zero) {
00159             throw gcnew Z3Error(ErrorCode::InvalidArgument);
00160         }
00161         return static_cast<Z3_sort>(t.ToPointer()); 
00162     }
00163     Z3_func_decl get_func_decl(FuncDeclPtr t) { 
00164         if (t == IntPtr::Zero) {
00165             throw gcnew Z3Error(ErrorCode::InvalidArgument);
00166         }
00167         return static_cast<Z3_func_decl>(t.ToPointer()); 
00168     }
00169     Z3_ast get_ast(TermPtr t) { 
00170         if (t == IntPtr::Zero) {
00171             throw gcnew Z3Error(ErrorCode::InvalidArgument);
00172         }
00173         return static_cast<Z3_ast>(t.ToPointer()); 
00174     }
00175     Z3_app get_const_ast(AppPtr c) { 
00176         if (c == IntPtr::Zero) {
00177             throw gcnew Z3Error(ErrorCode::InvalidArgument);
00178         }
00179         return static_cast<Z3_app>(c.ToPointer()); 
00180     }
00181     Z3_pattern_ast get_pattern_ast(PatternPtr p) { 
00182         if (p == IntPtr::Zero) {
00183             throw gcnew Z3Error(ErrorCode::InvalidArgument);
00184         }
00185         return static_cast<Z3_pattern_ast>(p.ToPointer()); 
00186     }
00187 
00189 
00190 
00191     
00198     public enum class SymbolKind 
00199     {
00200         Int, 
00201         String
00202     };
00203 
00207     public enum class SortKind 
00208     {
00209         Uninterpreted,
00210         Bool,
00211         Int,
00212         Real,
00213         BitVector,
00214         Array,
00215         Datatype,
00216         Unknown
00217     };
00218 
00232     public enum class SearchFailureExplanation
00233     {
00234         NoFailure,
00235         Unknown,
00236         TimeOut,
00237         MemOut,
00238         UserCanceled,
00239         MaxConflicts,
00240         Theory,
00241         Quantifiers
00242     };
00243 
00253     public enum class TermKind 
00254     {
00255         Numeral,
00256         App,
00257         Var,
00258         Quantifier,
00259         Unknown
00260     };
00261     
00262 
00266     public enum class DeclKind 
00267     {
00268         // Basic operators
00269         True,
00270         False,
00271         Eq,
00272         Distinct,
00273         Ite,
00274         And,
00275         Or,
00276         Iff,
00277         Xor,
00278         Not,
00279         Implies,
00280         // Arithmetic
00281         ArithNum,
00282         Le,
00283         Ge,
00284         Lt,
00285         Gt,
00286         Add,
00287         Sub,
00288         Uminus,
00289         Mul,
00290         Div,
00291         IDiv,
00292         Rem,
00293         Mod,
00294         // Arrays
00295         Store,
00296         Select,
00297         ConstArray,
00298         DefaultArray,
00299         MapArray,
00300         Union,
00301         Intersect,
00302         Difference,
00303         Complement,
00304         Subset,
00305         // Bit-vectors.            
00306 
00307         BitNum,
00308         Bit1,
00309         Bit0,
00310         BNeg,
00311         BAdd,
00312         BSub,
00313         BMul,
00314         BSDiv,
00315         BUDiv,
00316         BSRem,
00317         BURem,
00318         BSMod,
00319 
00320         BSDiv0,
00321         BUDiv0,
00322         BSRem0,
00323         BURem0,
00324         BSMod0,
00325         BULeq,
00326         BSLeq,
00327         BUGeq,
00328         BSGeq,
00329         BULt,
00330         BSLt,
00331         BUGt,
00332         BSGt,
00333         BAnd,
00334         BOr,
00335         BNot,
00336         BXor,
00337         BNand,
00338         BNor,
00339         BXnor,
00340         BConcat,
00341         BSignExt,
00342         BZeroExt,
00343         BExtract,
00344         BRepeat,
00345         BRedOr,
00346         BRedAnd,
00347         BComp,
00348 
00349         BShl,
00350         BLShr,
00351         BAShr,
00352         BRotateLeft,
00353         BRotateRight,
00354         BInt2Bv,
00355         BBv2Int,
00356 
00357         PrAsserted,
00358         PrGoal,
00359         PrModusPonens,
00360         PrReflexivity,
00361         PrTransitivity,
00362         PrTransitivityStar,
00363         PrSymmetry,
00364         PrMonotonicity,
00365         PrQuantIntro,
00366         PrDistributivity,
00367         PrAndElim,
00368         PrNotOrElim,
00369         PrRewrite,
00370         PrRewriteStar,
00371         PrPullQuant,
00372         PrPullQuantStar,
00373         PrPushQuant,
00374         PrElimUnusedVars,
00375         PrDer,
00376         PrQuantInst,
00377         PrHypothesis,
00378         PrLemma,
00379         PrUnitResolution,
00380         PrIffTrue,
00381         PrIffFalse,
00382         PrCommutativity,
00383         PrDefAxiom,
00384         PrDefIntro,
00385         PrApplyDef,
00386         PrIffOeq,            
00387         PrNnfPos,
00388         PrNnfNeg,
00389         PrNnfStar,
00390         PrSkolemize,
00391         PrCnfStar,
00392         PrModusPonensOeq,
00393         PrThLemma,
00394         Uninterpreted            
00395     };
00396 
00397 
00405     public interface class IErrorHandler 
00406     {
00407     public:
00408         virtual void Handler(ErrorCode code) = 0;
00409     };
00410 
00412     LBool ToLBool(Z3_lbool b) {
00413         switch(b) {
00414         case Z3_L_FALSE: return LBool::False; 
00415         case Z3_L_TRUE:  return LBool::True; 
00416         default:         return LBool::Undef; 
00417         }
00418     }
00420 
00428     public ref class LabeledLiterals {
00429         Z3_context m_context;
00430         Z3_literals  m_labels;
00431     internal:
00432         LabeledLiterals(Z3_context ctx, Z3_literals lbls): m_context(ctx), m_labels(lbls) {}
00433         Z3_literals Get() { return m_labels; }
00434         TermPtr GetLiteral(unsigned idx) { return TermPtr(Z3_get_literal(m_context, m_labels, idx)); }
00435     protected:
00436         !LabeledLiterals(); 
00437     public:
00438         ~LabeledLiterals() { if (m_labels) { Z3_del_literals(m_context, m_labels); } m_labels = 0; }
00439         unsigned GetNumLabels() { return Z3_get_num_literals(m_context, m_labels); }
00440         void Disable(unsigned idx) { Z3_disable_literal(m_context, m_labels, idx); }
00441         Symbol^ GetLabel(unsigned idx) { return gcnew Symbol(Z3_get_label_symbol(m_context, m_labels, idx)); }
00442     };
00443 
00444 
00450     public ref class Constructor {
00451         Z3_context          m_context;
00452         Z3_constructor      m_constructor;
00453         FuncDeclPtr         m_constructor_decl;
00454         FuncDeclPtr         m_tester;
00455         array<FuncDeclPtr>^ m_accessors;
00456 
00457         !Constructor();
00458 
00459     internal:
00460         String^          m_name;
00461         String^          m_tester_name;
00462         array<String^>^  m_field_names;
00463         array<SortPtr>^  m_field_sorts;
00464         array<unsigned>^ m_field_refs;
00465 
00466         Constructor(
00467             Z3_context       context,
00468             String^          name,
00469             String^          tester,
00470             array<String^>^  field_names,
00471             array<SortPtr>^  field_sorts,
00472             array<unsigned>^ field_refs
00473             );
00474 
00475         void Query();
00476         Z3_constructor Get();
00477         FuncDeclPtr GetConstructor();
00478         FuncDeclPtr GetTester();
00479         array<FuncDeclPtr>^ GetAccessors();
00480     public:    
00481         ~Constructor();   
00482     };
00483 
00484     
00485 
00497     public ref class Config
00498     {
00500         Z3_config m_config;
00502     internal:
00504         Z3_config get() { return m_config; }
00506 
00507     protected:
00508         !Config();
00509 
00510     public:
00518         Config();
00519 
00521         ~Config();
00522         
00532         void SetParamValue(String^ name, String^ value);
00533     };
00534 
00535 
00539     public interface class IRawParameter {  };
00540     public interface class IParameter {  };
00541 
00542     public ref class IntParameter : public IRawParameter, public IParameter { 
00543         int m_value;
00544     internal:
00545         IntParameter(int i) : m_value(i) {}
00546     public:
00547         property int Int { int get() { return m_value; } }
00548         virtual String^ ToString() override { return m_value.ToString(); }
00549     };
00550 
00551     public ref class DoubleParameter : public IRawParameter, public IParameter  { 
00552         double m_value;
00553     internal:
00554         DoubleParameter(double i) : m_value(i) {}
00555     public:
00556         property double Double { double get() { return m_value; } }
00557         virtual String^ ToString() override { return m_value.ToString(); }
00558     };
00559 
00560     public ref class RationalParameter : public IRawParameter, public IParameter  { 
00561         String^ m_value;
00562     internal:
00563         RationalParameter(String^ s): m_value(s) {}
00564     public:
00565         property  String^ GetRational {  String^ get() { return m_value; } }
00566         virtual String^ ToString() override { return m_value; }
00567     };
00568 
00569     public ref class SymbolParameter : public IRawParameter, public IParameter  { 
00570         Symbol^ m_value;
00571     internal:
00572         SymbolParameter(Symbol^ s): m_value(s) {}
00573     public:
00574         property  Symbol^ GetSymbol {  Symbol^ get() { return m_value; } }
00575     };
00576 
00577     public ref class TermPtrParameter : public IRawParameter  { 
00578         TermPtr m_value;
00579     internal:
00580         TermPtrParameter(TermPtr t) : m_value(t) {}
00581     public:
00582         property TermPtr GetTerm {  TermPtr get() { return m_value; } }
00583     };
00584 
00585     public ref class SortPtrParameter : public IRawParameter  { 
00586         SortPtr m_value;
00587     internal:
00588         SortPtrParameter(SortPtr t) : m_value(t) {}
00589     public:
00590         property  SortPtr GetSort {  SortPtr get() { return m_value; } }
00591     };
00592 
00593     public ref class FuncDeclPtrParameter : public IRawParameter  { 
00594         FuncDeclPtr m_value;
00595     internal:
00596         FuncDeclPtrParameter(FuncDeclPtr t) : m_value(t) {}
00597     public:
00598         property  FuncDeclPtr GetFuncDecl {  FuncDeclPtr get() { return m_value; } }
00599     };
00600 
00601 
00602 
00603 
00607     public ref class RawArrayValue {
00608     public:
00609         array<TermPtr>^   Domain; 
00610         array<TermPtr>^   Range;
00611         TermPtr           ElseCase;
00612     };
00613 
00620     public ref class RawFunctionEntry {
00621     public:
00622         array<TermPtr>^ Arguments;
00623         TermPtr         Result;
00624     };
00625 
00640     public ref class RawFunctionGraph {
00641     public:
00642         FuncDeclPtr        Declaration;
00643         array<RawFunctionEntry^>^ Entries;
00644         TermPtr               Else;
00645     };
00646 
00647     public ref class RawQuantifier {
00648     public:
00649         bool               IsForall;
00650         unsigned           Weight;
00651         array<PatternPtr>^ Patterns;
00652         array<SortPtr>^    Sorts;
00653         array<Symbol^>^    Names;
00654         TermPtr            Body;
00655     };
00656 
00657     ref class RawModel;
00658 
00662     public ref class RawModel {
00663         Z3_context m_context;
00664         Z3_model   m_model;
00665         Dictionary<FuncDeclPtr, RawFunctionGraph^>^ m_graphs;
00666     internal:           
00667         RawModel(Z3_context c, Z3_model m) : m_context(c), m_model(m), m_graphs(nullptr) {}
00668 
00669         void Reset();
00670     protected:
00671         !RawModel();
00672     public:
00673         ~RawModel();
00674 
00675 
00679         array<FuncDeclPtr>^ GetModelConstants();
00680            
00687         Dictionary<FuncDeclPtr, RawFunctionGraph^>^ GetFunctionGraphs();
00688 
00711         TermPtr Eval(TermPtr);
00712 
00713         TermPtr Eval(FuncDeclPtr, array<TermPtr>^ args);
00714 
00718         virtual String^ ToString() override;
00719 
00723         void Display(System::IO::TextWriter^ w);
00724 
00725     };
00726 
00727 
00731     public ref class RawContext : public MarshalByRefObject
00732     {        
00733         Z3_context m_context;
00734     internal:
00735         static IErrorHandler^ m_error_handler = nullptr;
00736 
00737         Z3_context GetContext() { return m_context; }
00738 
00739     protected:
00740         !RawContext();
00741     public: 
00753         RawContext(Config^ config); 
00754 
00755         void Reset();
00756 
00757         ~RawContext();
00758 
00763         
00775         bool TraceToFile(String^ trace_file);
00776         
00782         void TraceToStdErr();
00783 
00789         void TraceToStdOut();
00790 
00798         void TraceOff();
00799 
00803         void EnableDebugTrace(String^ tag);
00804 
00812         bool OpenLog(String^ filename);
00813 
00820         void AppendLog(String^ string);
00821 
00827         void CloseLog();
00828 
00835         void ToggleWarningMessages(bool enabled);
00849         Symbol^ MkSymbol(int i);
00850 
00851         Symbol^ MkSymbol(String^ s);
00858         
00864         SortPtr MkSort(Symbol^ s);
00865 
00866         SortPtr MkSort(String^ s); 
00867 
00868         SortPtr MkSort(int i);
00869 
00870 
00876         SortPtr MkBoolSort();
00877 
00887         SortPtr MkIntSort();
00888 
00895         SortPtr MkRealSort();
00896 
00897 
00905         SortPtr MkBvSort(unsigned sz);
00906 
00919         SortPtr MkArraySort(SortPtr domain, SortPtr range);
00920 
00921 
00936         SortPtr MkTupleSort(
00937             Symbol^               mk_tuple_name, 
00938             array<Symbol^>^       field_names,
00939             array<SortPtr>^       field_types,
00940             [Runtime::InteropServices::Out] FuncDeclPtr%         mk_tuple_decl,
00941             [Runtime::InteropServices::In] [Runtime::InteropServices::Out] array<FuncDeclPtr>^  proj_decl
00942             );
00943 
00944         SortPtr MkTupleSort(
00945             String^               mk_tuple_name, 
00946             array<String^>^       field_names,
00947             array<SortPtr>^       field_types,
00948             [Runtime::InteropServices::Out] FuncDeclPtr%         mk_tuple_decl,
00949             [Runtime::InteropServices::In] [Runtime::InteropServices::Out] array<FuncDeclPtr>^  proj_decl
00950             );
00951 
00961         SortPtr MkEnumerationSort(
00962             String^             name,
00963             array<String^>^     enum_names,
00964             array<FuncDeclPtr>^ enum_consts,
00965             array<FuncDeclPtr>^ enum_testers);
00966 
00980         SortPtr MkListSort(
00981             String^ name,
00982             SortPtr elem_sort,
00983             [Runtime::InteropServices::Out] FuncDeclPtr% nil_decl,
00984             [Runtime::InteropServices::Out] FuncDeclPtr% is_nil_decl,
00985             [Runtime::InteropServices::Out] FuncDeclPtr% cons_decl,
00986             [Runtime::InteropServices::Out] FuncDeclPtr% is_cons_decl,
00987             [Runtime::InteropServices::Out] FuncDeclPtr% head_decl,
00988             [Runtime::InteropServices::Out] FuncDeclPtr% tail_decl
00989             );
00990         
00991 
01008         Constructor^ MkConstructor(
01009             String^ name,
01010             String^ tester,
01011             array<String^>^ field_names,
01012             array<SortPtr>^ field_sorts,
01013             array<unsigned>^ field_refs
01014             );
01015 
01019         FuncDeclPtr GetConstructor(Constructor^ c) { return c->GetConstructor(); }
01020 
01024         FuncDeclPtr GetTester(Constructor^ c) { return c->GetTester(); }
01025 
01029         array<FuncDeclPtr>^ GetAccessors(Constructor^ c) { return c->GetAccessors(); }
01030 
01034         SortPtr MkDataType(
01035             String^ name,
01036             array<Constructor^>^ constructors
01037             );
01038 
01039         
01046         array<SortPtr>^ MkDataTypes(
01047             array<String^>^ names,
01048             array<array<Constructor^>^>^ constructors
01049             );
01050 
01058 
01073         FuncDeclPtr MkFuncDecl(Symbol^ s, array<SortPtr>^ domain, SortPtr range);
01074 
01075         FuncDeclPtr MkFuncDecl(String^ s, array<SortPtr>^ domain, SortPtr range);
01076 
01077         FuncDeclPtr MkConstDecl(Symbol^ s, SortPtr ty) {
01078             return MkFuncDecl(s, gcnew array<SortPtr>(0), ty);
01079         }
01080         FuncDeclPtr MkFuncDecl(Symbol^ s, SortPtr domain, SortPtr range);
01081 
01082         FuncDeclPtr MkFuncDecl(Symbol^ s, SortPtr d1, SortPtr d2, SortPtr range);
01083 
01084         FuncDeclPtr MkConstDecl(String^ s, SortPtr ty) {
01085             return MkFuncDecl(s, gcnew array<SortPtr>(0), ty);
01086         }
01087         FuncDeclPtr MkFuncDecl(String^ s, SortPtr domain, SortPtr range);
01088 
01089         FuncDeclPtr MkFuncDecl(String^ s, SortPtr d1, SortPtr d2, SortPtr range);
01090 
01091     
01097         AppPtr MkApp(FuncDeclPtr d, array<TermPtr>^ args);
01098         AppPtr MkApp(FuncDeclPtr d, TermPtr arg);
01099         AppPtr MkApp(FuncDeclPtr d, TermPtr arg1, TermPtr arg2);
01100         AppPtr MkApp(FuncDeclPtr d, TermPtr arg1, TermPtr arg2, TermPtr arg3);
01101 
01108         AppPtr MkConst(FuncDeclPtr d);
01109         AppPtr MkConst(String^ s, SortPtr ty);
01110         AppPtr MkConst(Symbol^ s, SortPtr ty);
01111 
01112 
01120         FuncDeclPtr MkFreshFuncDecl(String^ prefix, array<SortPtr>^ domain, SortPtr range);
01121     
01128         TermPtr MkFreshConst(String^ prefix, SortPtr ty);
01129 
01134         TermPtr MkLabel(Symbol^ name, bool pos, TermPtr fml);
01135     
01139         TermPtr MkTrue() { return TermPtr(Z3_mk_true(m_context)); }
01140 
01141 
01145         TermPtr MkFalse() { return TermPtr(Z3_mk_false(m_context)); }
01146 
01147     
01153         TermPtr MkEq(TermPtr l, TermPtr r);
01154 
01155 
01166         TermPtr MkDistinct(array<TermPtr>^ args);
01167 
01168 
01174         virtual TermPtr MkNot(TermPtr arg);
01175     
01183         TermPtr MkIte(TermPtr t1, TermPtr t2, TermPtr t3);
01184 
01190         TermPtr MkIff(TermPtr t1, TermPtr t2);
01191 
01197         TermPtr MkImplies(TermPtr t1, TermPtr t2);
01198     
01204         TermPtr MkXor(TermPtr t1, TermPtr t2);
01205     
01213         TermPtr MkAnd(array<TermPtr>^ args);
01214         TermPtr MkAnd(TermPtr arg1, TermPtr arg2);
01215     
01223         TermPtr MkOr(array<TermPtr>^ args);
01224         TermPtr MkOr(TermPtr arg1, TermPtr arg2);
01225 
01233         TermPtr MkAdd(array<TermPtr>^ args);
01234         TermPtr MkAdd(TermPtr arg1, TermPtr arg2);
01235 
01244         TermPtr MkMul(array<TermPtr>^ args);
01245         TermPtr MkMul(TermPtr arg1, TermPtr arg2);
01246     
01254         TermPtr MkSub(array<TermPtr>^ args);
01255         TermPtr MkSub(TermPtr arg1, TermPtr arg2);
01256 
01262         TermPtr MkUnaryMinus(TermPtr arg);
01263 
01269         TermPtr MkDiv(TermPtr arg1, TermPtr arg2);
01270 
01276         TermPtr MkMod(TermPtr arg1, TermPtr arg2);
01277 
01283         TermPtr MkRem(TermPtr arg1, TermPtr arg2);
01284 
01285 
01291         TermPtr MkLt(TermPtr arg1, TermPtr arg2);
01292 
01298         TermPtr MkLe(TermPtr arg1, TermPtr arg2);
01299 
01305         TermPtr MkGt(TermPtr arg1, TermPtr arg2);
01306 
01312         TermPtr MkGe(TermPtr arg1, TermPtr arg2);
01313 
01324         TermPtr MkInt2Real(TermPtr arg);
01325 
01331         TermPtr MkBvNot(TermPtr t1);
01332 
01338         TermPtr MkBvAnd(TermPtr t1, TermPtr t2);
01339 
01345         TermPtr MkBvOr(TermPtr t1, TermPtr t2);
01346 
01352         TermPtr MkBvXor(TermPtr t1, TermPtr t2);
01353 
01359         TermPtr MkBvNand(TermPtr t1, TermPtr t2);
01360 
01366         TermPtr MkBvNor(TermPtr t1, TermPtr t2);
01367 
01373         TermPtr MkBvXnor(TermPtr t1, TermPtr t2);
01374 
01380         TermPtr MkBvNeg(TermPtr t1);
01381     
01387         TermPtr MkBvAdd(TermPtr t1, TermPtr t2);
01388 
01394         TermPtr MkBvSub(TermPtr t1, TermPtr t2);
01395     
01401         TermPtr MkBvMul(TermPtr t1, TermPtr t2);
01402 
01412         TermPtr MkBvUdiv(TermPtr t1, TermPtr t2);
01413 
01427         TermPtr MkBvSdiv(TermPtr t1, TermPtr t2);
01428 
01438         TermPtr MkBvUrem(TermPtr t1, TermPtr t2);
01439 
01452         TermPtr MkBvSrem(TermPtr t1, TermPtr t2);
01453 
01463         TermPtr MkBvSmod(TermPtr t1, TermPtr t2);
01464 
01470         TermPtr MkBvUlt(TermPtr t1, TermPtr t2);
01471     
01485         TermPtr MkBvSlt(TermPtr t1, TermPtr t2);
01486 
01492         TermPtr MkBvUle(TermPtr t1, TermPtr t2);
01493 
01499         TermPtr MkBvSle(TermPtr t1, TermPtr t2);
01500 
01506         TermPtr MkBvUge(TermPtr t1, TermPtr t2);
01507 
01513         TermPtr MkBvSge(TermPtr t1, TermPtr t2);
01514 
01520         TermPtr MkBvUgt(TermPtr t1, TermPtr t2);
01521 
01527         TermPtr MkBvSgt(TermPtr t1, TermPtr t2);
01528 
01537         TermPtr MkBvConcat(TermPtr t1, TermPtr t2);
01538     
01546         TermPtr MkBvExtract(unsigned high, unsigned low, TermPtr t);
01547 
01555         TermPtr MkBvSignExt(unsigned i, TermPtr t);
01556 
01564         TermPtr MkBvZeroExt(unsigned i, TermPtr t);
01565 
01574         TermPtr MkBvShl(TermPtr t1, TermPtr t2);
01575 
01584         TermPtr MkBvLshr(TermPtr t1, TermPtr t2);
01585 
01595         TermPtr MkBvAshr(TermPtr t1, TermPtr t2);
01596     
01602         TermPtr MkBvRotateLeft(unsigned i, TermPtr t1);
01603     
01609         TermPtr MkBvRotateRight(unsigned i, TermPtr t1);
01610 
01616         TermPtr MkBv2Int(TermPtr t1, bool is_signed);
01617 
01623         TermPtr MkInt2Bv(unsigned size, TermPtr t1);
01624 
01630         TermPtr MkBvAddNoOverflow(TermPtr t1, TermPtr t2, bool is_signed);
01631 
01637         TermPtr MkBvAddNoUnderflow(TermPtr t1, TermPtr t2);
01638 
01644         TermPtr MkBvSubNoOverflow(TermPtr t1, TermPtr t2);
01645 
01651         TermPtr MkBvSubNoUnderflow(TermPtr t1, TermPtr t2, bool is_signed);
01652 
01658         TermPtr MkBvSDivNoOverflow(TermPtr t1, TermPtr t2);
01659 
01663         TermPtr MkBvNegNoOverflow(TermPtr t1);
01664 
01670         TermPtr MkBvMulNoOverflow(TermPtr t1, TermPtr t2, bool is_signed);
01671 
01677         TermPtr MkBvMulNoUnderflow(TermPtr t1, TermPtr t2);
01678 
01688         TermPtr MkArraySelect(TermPtr a, TermPtr i);
01689     
01699         TermPtr MkArrayStore(TermPtr a, TermPtr i, TermPtr v);
01700 
01712         TermPtr MkArrayMap(FuncDeclPtr d, array<TermPtr>^ args);
01713 
01725         TermPtr MkArrayConst(SortPtr domain, TermPtr v);
01726 
01741         TermPtr MkArrayDefault(TermPtr a);
01742 
01750 
01754         SortPtr MkSetSort(SortPtr ty) { return SortPtr(Z3_mk_set_sort(m_context, get_sort_ast(ty))); }
01755 
01759         TermPtr MkEmptySet(SortPtr ty) { return TermPtr(Z3_mk_empty_set(m_context, get_sort_ast(ty))); }
01760 
01764         TermPtr MkFullSet(SortPtr ty) { return TermPtr(Z3_mk_full_set(m_context, get_sort_ast(ty))); }
01765 
01771         TermPtr MkSetAdd(TermPtr set, TermPtr elem) {
01772             return TermPtr(Z3_mk_set_add(m_context, get_ast(set), get_ast(elem)));
01773         }
01774 
01780         TermPtr MkSetDel(TermPtr set, TermPtr elem) {
01781             return TermPtr(Z3_mk_set_del(m_context, get_ast(set), get_ast(elem)));
01782         }
01783 
01789         TermPtr MkSetUnion(array<TermPtr>^ sets);
01790         TermPtr MkSetUnion(TermPtr set1, TermPtr set2);
01791 
01795         TermPtr MkSetIntersect(array<TermPtr>^ sets);
01796         TermPtr MkSetIntersect(TermPtr set1, TermPtr set2);
01797 
01801         TermPtr MkSetDifference(TermPtr arg1, TermPtr arg2) {
01802             return TermPtr(Z3_mk_set_difference(m_context, get_ast(arg1), get_ast(arg2)));
01803         }
01807         TermPtr MkSetComplement(TermPtr arg) {
01808             return TermPtr(Z3_mk_set_complement(m_context, get_ast(arg)));
01809         }
01810 
01816         TermPtr MkSetMember(TermPtr elem, TermPtr set) {
01817             return TermPtr(Z3_mk_set_member(m_context, get_ast(elem), get_ast(set)));
01818         }
01819 
01823         TermPtr MkSetSubset(TermPtr arg1, TermPtr arg2) {
01824             return TermPtr(Z3_mk_set_subset(m_context, get_ast(arg1), get_ast(arg2)));
01825         }
01833 
01838         FuncDeclPtr MkInjectiveFunction(String^ name, array<SortPtr>^ domain, SortPtr range);
01839 
01840         FuncDeclPtr MkInjectiveFunction(Symbol^ name, array<SortPtr>^ domain, SortPtr range);
01841 
01850         
01859         TermPtr MkNumeral(String^ numeral, SortPtr ty);
01860         TermPtr MkNumeral(int n, SortPtr ty);
01861         TermPtr MkNumeral(unsigned n, SortPtr ty);
01862         TermPtr MkNumeral(__int64 n, SortPtr ty);
01863         TermPtr MkNumeral(unsigned __int64 n, SortPtr ty);
01864 
01871         
01930         PatternPtr MkPattern(array<TermPtr>^ terms);
01931 
01958         TermPtr MkBound(unsigned index, SortPtr ty);
01959     
01974         TermPtr MkForall(
01975             unsigned weight,
01976             array<PatternPtr>^ patterns,
01977             array<SortPtr>^ types,
01978             array<Symbol^>^ names,
01979             TermPtr body
01980             );
01981 
01996         TermPtr MkForall(
01997             unsigned weight,
01998             array<PatternPtr>^ patterns,
01999             array<SortPtr>^ types,
02000             array<String^>^ names,
02001             TermPtr body
02002             );
02003 
02023         TermPtr MkForall(
02024             unsigned           weight,
02025             array<AppPtr>^   bound,
02026             array<PatternPtr>^ patterns,
02027             TermPtr body
02028             );
02029 
02037         TermPtr MkExists(
02038             unsigned weight,
02039             array<PatternPtr>^ patterns,
02040             array<SortPtr>^ types,
02041             array<Symbol^>^ names,
02042             TermPtr body
02043             );
02044 
02045         TermPtr MkExists(
02046             unsigned weight,
02047             array<PatternPtr>^ patterns,
02048             array<SortPtr>^ types,
02049             array<String^>^ names,
02050             TermPtr body
02051             );
02052 
02053         TermPtr MkExists(
02054             unsigned           weight,
02055             array<AppPtr>^   bound,
02056             array<PatternPtr>^ patterns,
02057             TermPtr            body
02058             );
02059 
02069         TermPtr MkQuantifier(
02070             bool                  is_forall,
02071             unsigned              weight,
02072             array<PatternPtr>^ patterns,
02073             array<TermPtr>^    no_patterns,
02074             array<SortPtr>^    types,
02075             array<Symbol^>^       names,
02076             TermPtr            body
02077             );
02078 
02079 
02087         
02093         SymbolKind GetSymbolKind(Symbol^ s);
02094 
02102         int GetSymbolInt(Symbol^ s);
02103     
02111         String^ GetSymbolString(Symbol^ s);
02112 
02116         bool IsEq(TermPtr t1, TermPtr t2);
02117     
02121         TermKind GetTermKind(TermPtr a);
02122 
02128         DeclKind GetDeclKind(FuncDeclPtr d);
02129 
02135         array<IRawParameter^>^ GetDeclParameters(FuncDeclPtr d);
02136     
02142         FuncDeclPtr GetAppDecl(AppPtr a);
02143         
02148         array<TermPtr>^ GetAppArgs(AppPtr a);
02149 
02155         String^ GetNumeralString(TermPtr a);
02156 
02165         int GetNumeralInt(TermPtr v);
02166 
02167         bool TryGetNumeralInt(TermPtr v, [Runtime::InteropServices::Out] int% i);
02168 
02177         unsigned int GetNumeralUInt(TermPtr v);
02178 
02179         bool TryGetNumeralUInt(TermPtr v, [Runtime::InteropServices::Out] unsigned int% u);
02180 
02181 
02190         unsigned __int64 GetNumeralUInt64(TermPtr v);
02191 
02192         bool TryGetNumeralUInt64(TermPtr v, [Runtime::InteropServices::Out] unsigned __int64% u);
02193 
02194 
02203         __int64 GetNumeralInt64(TermPtr v);
02204 
02205         bool TryGetNumeralInt64(TermPtr v, [Runtime::InteropServices::Out] __int64% i);
02206 
02212         LBool GetBoolValue(TermPtr a);
02213 
02217         bool TryGetArrayValue(TermPtr a,[Runtime::InteropServices::Out] RawArrayValue^% av);
02218 
02219 
02225         unsigned GetVarIndex(TermPtr a) {
02226             return Z3_get_index_value(m_context, get_ast(a));
02227         }
02228 
02234         RawQuantifier^ GetQuantifier(TermPtr a);
02235 
02236 
02242         array<TermPtr>^ GetPatternTerms(PatternPtr p);
02243 
02247         Symbol^ GetDeclName(FuncDeclPtr d);
02248 
02252         Symbol^ GetSortName(SortPtr ty);
02253 
02259         SortPtr GetSort(TermPtr a);
02260 
02265         array<SortPtr>^ GetDomain(FuncDeclPtr d);
02266 
02267 
02274         SortPtr GetRange(FuncDeclPtr d);
02275 
02281         SortKind GetSortKind(SortPtr t);
02282 
02291         unsigned GetBvSortSize(SortPtr t);
02292 
02301         SortPtr GetArraySortDomain(SortPtr t);
02302 
02311         SortPtr GetArraySortRange(SortPtr t);
02312 
02322         FuncDeclPtr GetTupleConstructor(SortPtr t);
02323     
02333         array<FuncDeclPtr>^ GetTupleFields(SortPtr t);
02334 
02342         
02353         void Push();
02354     
02369         void Pop(unsigned num_scopes);
02370 
02371         void Pop() { Pop(1); }
02372 
02373 
02400         void PersistTerm(TermPtr t, unsigned num_scopes);
02401         
02402 
02415         void AssertCnstr(TermPtr a);
02416     
02430         LBool CheckAndGetModel([Runtime::InteropServices::Out] RawModel^% m);
02431     
02439         LBool Check();
02440 
02463         LBool CheckAssumptions([Runtime::InteropServices::Out] RawModel^% m, 
02464                                [Runtime::InteropServices::In]  array<TermPtr>^ assumptions, 
02465                                [Runtime::InteropServices::Out] TermPtr% proof, 
02466                                [Runtime::InteropServices::Out] array<TermPtr>^% core);
02467 
02468 
02488         LBool GetImpliedEqualities(
02489             [Runtime::InteropServices::In]  array<TermPtr>^ terms,
02490             [Runtime::InteropServices::Out] array<unsigned>^% class_ids
02491             );
02492 
02493 
02499         SearchFailureExplanation GetSearchFailureExplanation();
02500 
02501 
02505         TermPtr GetAssignments();
02506 
02510         LabeledLiterals^ GetRelevantLabels();
02511 
02515         LabeledLiterals^ GetRelevantLiterals();
02516 
02520         LabeledLiterals^ GetGuessedLiterals();
02521 
02528         void BlockLiterals(LabeledLiterals^ labels);
02529 
02533         TermPtr GetLiteral(LabeledLiterals^ labels, unsigned idx) {
02534             return labels->GetLiteral(idx);
02535         }
02536 
02544         TermPtr Simplify(TermPtr a);
02545         
02546     
02553 
02554 
02565         void SetPrintMode(PrintMode mode);
02566 
02570         String^ ToString(AstPtr a);
02571         
02572         void Display(System::IO::TextWriter^ w, AstPtr a);
02573     
02580         virtual String^ ToString() override;
02581 
02582         void Display(System::IO::TextWriter^ w);
02583 
02590         String^ StatisticsToString() {
02591             return gcnew String(Z3_statistics_to_string(m_context));
02592         }
02593 
02594         void DisplayStatistics(System::IO::TextWriter^ w) {
02595             w->Write(StatisticsToString());
02596         }
02597 
02601         String^ BenchmarkToSmtlib(String^ name,
02602                                   String^ logic,
02603                                   String^ status,
02604                                   String^ attributes,
02605                                   array<TermPtr>^ assumptions,
02606                                   TermPtr formula);
02607 
02633         void ParseSmtlibString(
02634             String^ string,
02635             [Runtime::InteropServices::In]  array<SortPtr>^     sorts,
02636             [Runtime::InteropServices::In]  array<FuncDeclPtr>^ decls,
02637             [Runtime::InteropServices::Out] array<TermPtr>^%    assumptions,            
02638             [Runtime::InteropServices::Out] array<TermPtr>^%    formulas,
02639             [Runtime::InteropServices::Out] array<FuncDeclPtr>^% new_decls,
02640             [Runtime::InteropServices::Out] array<SortPtr>^%    new_sorts,
02641             [Runtime::InteropServices::Out] String^% parser_out
02642             );
02643     
02647         void ParseSmtlibFile(
02648             String^             file,
02649             [Runtime::InteropServices::In]  array<SortPtr>^     sorts,
02650             [Runtime::InteropServices::In]  array<FuncDeclPtr>^ decls,
02651             [Runtime::InteropServices::Out] array<TermPtr>^%    assumptions,            
02652             [Runtime::InteropServices::Out] array<TermPtr>^%    formulas,
02653             [Runtime::InteropServices::Out] array<FuncDeclPtr>^% new_decls,
02654             [Runtime::InteropServices::Out] array<SortPtr>^%    new_sorts,
02655             [Runtime::InteropServices::Out] String^% parser_out
02656             );
02657 
02658 
02664         TermPtr ParseZ3String(String^ s);
02665 
02671         TermPtr ParseZ3File(String^ filename);
02672 
02678         TermPtr ParseSimplifyString(
02679             String^ s, 
02680             [Runtime::InteropServices::Out] String^% parser_out);
02681 
02687         TermPtr ParseSimplifyFile(
02688             String^ filename, 
02689             [Runtime::InteropServices::Out] String^% parser_out);
02690 
02696         /*{@*/
02697 
02705         static void SetErrorHandler(IErrorHandler^ h);
02706 
02710         static String^ GetErrorMessage(ErrorCode err);
02711 
02715         static void ResetMemory();
02716         
02724     
02728         void GetVersion(
02729             [Runtime::InteropServices::Out] unsigned % major, 
02730             [Runtime::InteropServices::Out] unsigned % minor, 
02731             [Runtime::InteropServices::Out] unsigned % build_number, 
02732             [Runtime::InteropServices::Out] unsigned % revision_number);
02733 
02734         
02738         /*
02739           TBD: obsolete?
02740           bool TypeCheck(TermPtr t) {
02741           return Z3_TRUE == Z3_type_check(m_context, get_ast(t));
02742         }
02743         */
02746     };
02747 
02748     ref class Context;
02749     ref class Model;
02750 
02751     public ref class Ast : public System::IComparable {
02752     protected:
02753         AstPtr m_ast;
02754         RawContext^ m_ctx;
02755     internal:
02756         Ast(RawContext^ c, AstPtr a);
02757         AstPtr GetPtr() { return m_ast; }
02758         AstPtr operator()() { return m_ast; }
02759     public:
02763         virtual bool Equals(Object^ obj) override;
02764 
02768         virtual int GetHashCode() override;
02769 
02773         virtual String^ ToString() override;
02774 
02778         virtual int CompareTo(Object^ other);
02779     };
02780 
02781     public ref class Sort : public Ast{
02782     internal:
02783         Sort(RawContext^ c, SortPtr a) : Ast(c,a) {}
02784     public:
02785         String^ GetName();
02786     };
02787 
02788     public ref class FuncDecl : public Ast {
02789     internal:
02790         FuncDecl(RawContext^ c, FuncDeclPtr a) : Ast(c,a) {}
02791     public:
02792         String^ GetDeclName();
02793         DeclKind GetKind();
02794     };
02795 
02796     public ref class Term : public Ast {
02797     internal:
02798         Term(RawContext^ c, TermPtr a) : Ast(c,a) {}
02799     public:
02805         static Term^ operator!(Term^ t1);
02806         static Term^ operator&(Term^ t1, Term^ t2);
02807         static Term^ operator|(Term^ t1, Term^ t2);
02808         static Term^ operator^(Term^ t1, Term^ t2);
02814         static Term^ operator+(Term^ t1, Term^ t2);
02815         static Term^ operator*(Term^ t1, Term^ t2);
02816         static Term^ operator/(Term^ t1, Term^ t2);
02817         static Term^ operator-(Term^ t1, Term^ t2);
02818         static Term^ operator>(Term^ t1, Term^ t2);
02819         static Term^ operator<(Term^ t1, Term^ t2);
02820         static Term^ operator>=(Term^ t1, Term^ t2);
02821         static Term^ operator<=(Term^ t1, Term^ t2);
02822 
02828         Term^ operator[](Term^ index);
02829 
02830         TermKind GetKind();
02831         FuncDecl^ GetAppDecl();
02832         array<Term^>^ GetAppArgs();
02833         Sort^ GetSort();
02834         String^ GetNumeralString();
02835         unsigned GetVarIndex();
02836         ref class Quantifier^ GetQuantifier();
02837 
02838     };
02839     
02840     public ref class Pattern : public Ast {
02841     internal:
02842         Pattern(RawContext^ c, PatternPtr a) : Ast(c,a) {}
02843     };
02844 
02845     public ref class Quantifier {
02846     public:
02847         bool                  IsForall;
02848         unsigned              Weight;
02849         array<Pattern^>^   Patterns;
02850         array<Sort^>^         Sorts;
02851         array<Symbol^>^       Names;
02852         Term^                 Body;
02853     };
02854 
02855     public ref class ArrayValue {
02856     public:
02857         array<Term^>^   Domain; 
02858         array<Term^>^   Range;
02859         Term^           ElseCase;
02860     };
02861 
02862     public ref class TermParameter : public IParameter  { 
02863         Term^ m_value;
02864     internal:
02865         TermParameter(Term^ t) : m_value(t) {}
02866     public:
02867         virtual String^ ToString() override { return m_value->ToString(); }
02868         property  Term^ GetTerm {  Term^ get() { return m_value; } }
02869     };
02870 
02871     public ref class SortParameter : public IParameter  { 
02872         Sort^ m_value;
02873     internal:
02874         SortParameter(Sort^ s): m_value(s) {}
02875     public:
02876         property  Sort^ GetSort {  Sort^ get() { return m_value; } }
02877         virtual String^ ToString() override { return m_value->ToString(); }
02878     };
02879 
02880     public ref class FuncDeclParameter : public IParameter  { 
02881         FuncDecl^ m_value;
02882     internal:
02883         FuncDeclParameter(FuncDecl^ d): m_value(d) {}
02884     public:
02885         property  FuncDecl^ GetFuncDecl { FuncDecl^ get() { return m_value; } }
02886         virtual String^ ToString() override { return m_value->ToString(); } 
02887     };
02888 
02889 
02893     public ref class Context  {
02894         
02896         RawContext^ m_ctx;
02897 
02898     internal:
02899         template<class Tptr, class T>
02900         array<Tptr>^ CopyArray(array<T^>^ a) {
02901             if (a == nullptr) {
02902                 return gcnew array<Tptr>(0);
02903             }
02904             int len = a->Length;
02905             array<Tptr>^ result = gcnew array<Tptr>(len);
02906             for (int i = 0; i < len; ++i) {
02907                 if (a[i] == nullptr) {
02908                     result[i] = IntPtr(0);
02909                 }
02910                 else {
02911                     result[i] = a[i]();
02912                 }
02913             }
02914             return result;
02915         }
02916 
02917         array<SortPtr>^ CopyArray(array<Sort^>^ a) {
02918             return CopyArray<SortPtr, Sort>(a);
02919         }
02920 
02921         array<FuncDeclPtr>^ CopyArray(array<FuncDecl^>^ a) {
02922             return CopyArray<FuncDeclPtr, FuncDecl>(a);
02923         }
02924 
02925         array<TermPtr>^ CopyArray(array<Term^>^ a) {
02926             return CopyArray<TermPtr,Term>(a);
02927         }
02928 
02929         array<PatternPtr>^ CopyArray(array<Pattern^>^ a) {
02930             return CopyArray<PatternPtr,Pattern>(a);
02931         }
02932 
02933         template<class T, class TPtr>
02934         static array<T^>^ CopyAstArray(RawContext^ ctx, array<TPtr>^ a) {
02935             if (a == nullptr) return nullptr;
02936             int len = a->Length;
02937             array<T^>^ result = gcnew array<T^>(len);
02938 
02939             for (int i = 0; i < len; ++i) {
02940                 if (a[i] != IntPtr(0)) {
02941                     result[i] = gcnew T(ctx,a[i]);
02942                 }
02943                 else {
02944                     result[i] = nullptr;
02945                 }
02946             }
02947             return result;
02948         }
02949 
02950         template<class T, class TPtr>
02951         array<T^>^ CopyAstArray(array<TPtr>^ a) {
02952             return CopyAstArray<T,TPtr>(m_ctx, a);
02953         }
02954 
02955 
02956         array<Sort^>^ CopySortArray(array<SortPtr>^ a) {
02957             return CopyAstArray<Sort, SortPtr>(a);
02958         }
02959 
02960         array<Term^>^ CopyTermArray(array<TermPtr>^ a) {
02961             return CopyAstArray<Term, TermPtr>(a);
02962         }
02963 
02964         array<FuncDecl^>^ CopyFuncDeclArray(array<FuncDeclPtr>^ a) {
02965             return CopyAstArray<FuncDecl, FuncDeclPtr>(a);
02966         }
02967 
02968         static array<Term^>^ CopyTermArray(RawContext^ ctx, array<TermPtr>^ a) {
02969             return CopyAstArray<Term, TermPtr>(ctx, a);
02970         }
02971 
02972         static array<Sort^>^ CopySortArray(RawContext^ ctx, array<SortPtr>^ a) {
02973             return CopyAstArray<Sort, SortPtr>(ctx, a);
02974         }
02975         static Quantifier^ GetQuantifier(RawContext^ ctx, Term^ term);
02976 
02977     internal:
02978         property RawContext^ GetContext { RawContext^ get() { return m_ctx; } }
02979 
02981 
02982 
02983     public:
02995         Context(Config^ config) : m_ctx(gcnew RawContext(config)) {}
02996 
02997 
03001         ~Context() { m_ctx->Reset(); }
03002 
03008         bool TraceToFile(String^ trace_file) { return m_ctx->TraceToFile(trace_file); }
03009 
03010         
03016         void TraceToStdErr() { m_ctx->TraceToStdErr(); }
03017 
03023         void TraceToStdOut() { m_ctx->TraceToStdOut(); }
03024 
03032         void TraceOff() { m_ctx->TraceOff(); }
03033 
03041         bool OpenLog(String^ filename) { return m_ctx->OpenLog(filename); }
03042 
03049         void AppendLog(String^ s) { m_ctx->AppendLog(s); }
03050 
03056         void CloseLog() { m_ctx->CloseLog(); }
03057 
03064         void EnableDebugTrace(String^ tag) { m_ctx->EnableDebugTrace(tag); }
03065 
03066         void ToggleWarningMessages(bool enabled) { m_ctx->ToggleWarningMessages(enabled); }
03067 
03072         Symbol^ MkSymbol(int i) { return m_ctx->MkSymbol(i); }
03073 
03074         Symbol^ MkSymbol(String^ s) { return m_ctx->MkSymbol(s); }
03081         void Push() { m_ctx->Push(); }
03082         void Pop(unsigned num_scopes) { m_ctx->Pop(num_scopes); }
03083         void Pop() { Pop(1); }
03084         void PersistTerm(Term^ t, unsigned num_scopes) { 
03085             m_ctx->PersistTerm(t(), num_scopes); 
03086         }
03087         LBool Check() { return m_ctx->Check(); }
03088         LBool CheckAndGetModel([Runtime::InteropServices::Out] Model^% m);
03089         LBool CheckAssumptions([Runtime::InteropServices::Out] Model^% m, 
03090                                [Runtime::InteropServices::In]  array<Term^>^ assumptions, 
03091                                [Runtime::InteropServices::Out] Term^% proof, 
03092                                [Runtime::InteropServices::Out] array<Term^>^% core);
03093         LBool GetImpliedEqualities(
03094             [Runtime::InteropServices::In]  array<Term^>^ terms,
03095             [Runtime::InteropServices::Out] array<unsigned>^% class_ids);
03096 
03097         SearchFailureExplanation GetSearchFailureExplanation() { return m_ctx->GetSearchFailureExplanation(); }
03098         LabeledLiterals^ GetRelevantLabels() { return m_ctx->GetRelevantLabels(); }
03099         LabeledLiterals^ GetRelevantLiterals() { return m_ctx->GetRelevantLiterals(); }
03100         LabeledLiterals^ GetGuessedLiterals() { return m_ctx->GetGuessedLiterals(); }
03101         void BlockLiterals(LabeledLiterals^ lbls) { m_ctx->BlockLiterals(lbls); }
03102         Term^ GetLiteral(LabeledLiterals^ lbls, unsigned idx) { return gcnew Term(m_ctx, m_ctx->GetLiteral(lbls, idx)); }
03103         Term^ Simplify(Term^ a) { return gcnew Term(m_ctx,m_ctx->Simplify(a())); }
03104         void AssertCnstr(Term^ a) { m_ctx->AssertCnstr(a()); }
03107         virtual String^ ToString() override { return m_ctx->ToString(); }
03108 
03109         void Display(System::IO::TextWriter^ w) { m_ctx->Display(w); }
03110         Term^ GetAssignments() { return gcnew Term(m_ctx, m_ctx->GetAssignments()); }
03111         String^ StatisticsToString() { return m_ctx->StatisticsToString(); }
03112         void DisplayStatistics(System::IO::TextWriter^ w) { m_ctx->DisplayStatistics(w); }
03113 
03117         String^ BenchmarkToSmtlib(String^ name,
03118                                   String^ logic,
03119                                   String^ status,
03120                                   String^ attributes,
03121                                   array<Term^>^ assumptions,
03122                                   Term^ formula);
03123 
03124         void ParseSmtlibString(
03125             String^            string,
03126             [Runtime::InteropServices::In]  array<Sort^>^     sorts,
03127             [Runtime::InteropServices::In]  array<FuncDecl^>^ decls,
03128             [Runtime::InteropServices::Out] array<Term^>^%    assumptions,            
03129             [Runtime::InteropServices::Out] array<Term^>^%    formulas,
03130             [Runtime::InteropServices::Out] array<FuncDecl^>^% new_decls,
03131             [Runtime::InteropServices::Out] array<Sort^>^%    new_sorts,
03132             [Runtime::InteropServices::Out] String^% parser_out
03133             );
03134                                          
03135 
03136         void ParseSmtlibFile(
03137             String^ file,
03138             [Runtime::InteropServices::In]  array<Sort^>^     sorts,
03139             [Runtime::InteropServices::In]  array<FuncDecl^>^ decls,
03140             [Runtime::InteropServices::Out] array<Term^>^%    assumptions,            
03141             [Runtime::InteropServices::Out] array<Term^>^%    formulas,
03142             [Runtime::InteropServices::Out] array<FuncDecl^>^% new_decls,
03143             [Runtime::InteropServices::Out] array<Sort^>^%    new_sorts,
03144             [Runtime::InteropServices::Out] String^% parser_out
03145             );
03146 
03147 
03148         Term^ ParseZ3String(String^ s) {
03149             return gcnew Term(m_ctx,m_ctx->ParseZ3String(s));
03150         }
03151 
03152         Term^ ParseZ3File(String^ s) {
03153             return gcnew Term(m_ctx,m_ctx->ParseZ3File(s));
03154         }
03155 
03156         Term^ ParseSimplifyString(String^ s, String^% parser_out) {
03157             return gcnew Term(m_ctx,m_ctx->ParseSimplifyString(s, parser_out));
03158         }
03159 
03160         Term^ ParseSimplifyFile(String^ s, String^% parser_out) {
03161             return gcnew Term(m_ctx,m_ctx->ParseSimplifyFile(s, parser_out));
03162         }
03163 
03164         static void SetErrorHandler(IErrorHandler^ h) {
03165             RawContext::SetErrorHandler(h);
03166         }
03167 
03168         static String^ GetErrorMessage(ErrorCode err) {
03169             return RawContext::GetErrorMessage(err);
03170         }
03171 
03172         static void ResetMemory() {
03173             RawContext::ResetMemory();
03174         }
03175 
03176         
03177         void SetPrintMode(PrintMode mode) { m_ctx->SetPrintMode(mode); }
03178 
03179         String^ ToString(Ast^ a) { return m_ctx->ToString(a()); }
03180         
03181         void Display(System::IO::TextWriter^ w, Ast^ a) { m_ctx->Display(w, a()); }
03182 
03183 
03184         Sort^ MkIntSort() { return gcnew Sort(m_ctx,m_ctx->MkIntSort()); }
03185         Sort^ MkBoolSort() { return gcnew Sort(m_ctx,m_ctx->MkBoolSort()); }
03186         Sort^ MkSort(Symbol^ s) { return gcnew Sort(m_ctx,m_ctx->MkSort(s)); }
03187         Sort^ MkSort(String^ s) { return gcnew Sort(m_ctx,m_ctx->MkSort(s)); }
03188         Sort^ MkSort(int i) { return gcnew Sort(m_ctx,m_ctx->MkSort(i)); }   
03189         Sort^ MkRealSort() { return gcnew Sort(m_ctx,m_ctx->MkRealSort()); } 
03190         Sort^ MkBvSort(unsigned sz) { return gcnew Sort(m_ctx,m_ctx->MkBvSort(sz)); }
03191         Sort^ MkArraySort(Sort^ domain, Sort^ range) { return gcnew Sort(m_ctx,m_ctx->MkArraySort(domain(), range())); }
03192 
03193         Sort^ MkTupleSort(
03194             Symbol^               mk_tuple_name, 
03195             array<Symbol^>^       field_names,
03196             array<Sort^>^       field_types,
03197             [Runtime::InteropServices::Out] FuncDecl^%         mk_tuple_decl,
03198             [Runtime::InteropServices::In, Runtime::InteropServices::Out] array<FuncDecl^>^  proj_decl
03199             );
03200 
03201         Sort^ MkTupleSort(
03202             String^               mk_tuple_name, 
03203             array<String^>^       field_names,
03204             array<Sort^>^       field_types,
03205             [Runtime::InteropServices::Out] FuncDecl^%         mk_tuple_decl,
03206             [Runtime::InteropServices::In, Runtime::InteropServices::Out] array<FuncDecl^>^  proj_decl
03207             );
03208         
03209         Sort^ MkEnumerationSort(
03210             String^             name,
03211             array<String^>^     enum_names,
03212             array<FuncDecl^>^ enum_consts,
03213             array<FuncDecl^>^ enum_testers);
03214 
03215         Sort^ MkListSort(
03216             String^ name,
03217             Sort^ elem_sort,
03218             [Runtime::InteropServices::Out] FuncDecl^% nil_decl,
03219             [Runtime::InteropServices::Out] FuncDecl^% is_nil_decl,
03220             [Runtime::InteropServices::Out] FuncDecl^% cons_decl,
03221             [Runtime::InteropServices::Out] FuncDecl^% is_cons_decl,
03222             [Runtime::InteropServices::Out] FuncDecl^% head_decl,
03223             [Runtime::InteropServices::Out] FuncDecl^% tail_decl
03224             );
03225         
03226         Constructor^ MkConstructor(
03227             String^ name,
03228             String^ tester,
03229             array<String^>^ field_names,
03230             array<Sort^>^ field_sorts,
03231             array<unsigned>^ field_refs
03232             );
03233 
03234         
03235         FuncDecl^ GetConstructor(Constructor^ c);
03236 
03237         FuncDecl^ GetTester(Constructor^ c);
03238 
03239         array<FuncDecl^>^ GetAccessors(Constructor^ c);
03240 
03245         Sort^ MkDataType(
03246             String^ name,
03247             array<Constructor^>^ constructors
03248             ) {
03249             return gcnew Sort(m_ctx, m_ctx->MkDataType(name, constructors));
03250         }
03251 
03256         array<Sort^>^ MkDataTypes(
03257             array<String^>^ names,
03258             array<array<Constructor^>^>^ constructors
03259             ) {
03260             return CopySortArray(m_ctx->MkDataTypes(names, constructors));
03261         }
03262 
03263 
03264         FuncDecl^ MkFuncDecl(Symbol^ s, array<Sort^>^ domain, Sort^ range) {
03265             return gcnew FuncDecl(m_ctx,m_ctx->MkFuncDecl(s, CopyArray(domain), range()));
03266         }
03267 
03268         FuncDecl^ MkFuncDecl(String^ s, array<Sort^>^ domain, Sort^ range) {
03269             return gcnew FuncDecl(m_ctx,m_ctx->MkFuncDecl(s, CopyArray(domain), range()));
03270         }
03271 
03272         FuncDecl^ MkConstDecl(Symbol^ s, Sort^ ty) {
03273             return MkFuncDecl(s, gcnew array<Sort^>(0), ty);
03274         }
03275         FuncDecl^ MkFuncDecl(Symbol^ s, Sort^ domain, Sort^ range) {
03276             return gcnew FuncDecl(m_ctx,m_ctx->MkFuncDecl(s, domain(), range()));
03277         }
03278         FuncDecl^ MkFuncDecl(Symbol^ s, Sort^ d1, Sort^ d2, Sort^ range) {
03279             return gcnew FuncDecl(m_ctx,m_ctx->MkFuncDecl(s, d1(), d2(), range()));            
03280         }
03281         FuncDecl^ MkConstDecl(String^ s, Sort^ ty) {
03282             return MkFuncDecl(s, gcnew array<Sort^>(0), ty);
03283         }
03284         FuncDecl^ MkFuncDecl(String^ s, Sort^ domain, Sort^ range) {
03285             return gcnew FuncDecl(m_ctx,m_ctx->MkFuncDecl(s, domain(), range()));
03286         }
03287         FuncDecl^ MkFuncDecl(String^ s, Sort^ d1, Sort^ d2, Sort^ range) {
03288             return gcnew FuncDecl(m_ctx,m_ctx->MkFuncDecl(s, d1(), d2(), range()));            
03289         }
03290         Term^ MkApp(FuncDecl^ d, array<Term^>^ args) {
03291             return gcnew Term(m_ctx,m_ctx->MkApp(d(), CopyArray(args)));
03292         }
03293         Term^ MkApp(FuncDecl^ d, Term^ arg) {
03294             return gcnew Term(m_ctx,m_ctx->MkApp(d(), arg()));
03295         }
03296         Term^ MkApp(FuncDecl^ d, Term^ arg1, Term^ arg2) {
03297             return gcnew Term(m_ctx,m_ctx->MkApp(d(), arg1(), arg2()));
03298         }
03299         Term^ MkApp(FuncDecl^ d, Term^ arg1, Term^ arg2, Term^ arg3) {
03300             return gcnew Term(m_ctx,m_ctx->MkApp(d(), arg1(), arg2(), arg3()));
03301         }
03302         Term^ MkConst(FuncDecl^ d) {
03303             return gcnew Term(m_ctx,m_ctx->MkConst(d()));
03304         }
03305         Term^ MkConst(String^ s, Sort^ ty) {
03306             return gcnew  Term(m_ctx,m_ctx->MkConst(s,ty()));
03307         }
03308         Term^ MkConst(Symbol^ s, Sort^ ty) {
03309             return gcnew Term(m_ctx,m_ctx->MkConst(s, ty()));
03310         }
03311         FuncDecl^ MkFreshFuncDecl(String^ prefix, array<Sort^>^ domain, Sort^ range) {
03312             return gcnew FuncDecl(m_ctx,m_ctx->MkFreshFuncDecl(prefix, CopyArray(domain), range()));
03313         }
03314         Term^ MkFreshConst(String^ prefix, Sort^ ty) {
03315             return gcnew Term(m_ctx,m_ctx->MkFreshConst(prefix, ty()));
03316         }
03317         Term^ MkTrue() { return gcnew Term(m_ctx,m_ctx->MkTrue()); }
03318         Term^ MkFalse() { return gcnew Term(m_ctx,m_ctx->MkFalse()); }
03319         Term^ MkLabel(Symbol^ name, bool pos, Term^ fml) { return gcnew Term(m_ctx,m_ctx->MkLabel(name, pos, fml())); }
03320 
03321         Term^ MkEq(Term^ l, Term^ r) { return gcnew Term(m_ctx,m_ctx->MkEq(l(), r())); }
03322         Term^ MkDistinct(array<Term^>^ args) {
03323             return gcnew Term(m_ctx,m_ctx->MkDistinct(CopyArray(args))); 
03324         }
03325         Term^ MkNot(Term^ arg) { return gcnew Term(m_ctx,m_ctx->MkNot(arg())); }
03326         Term^ MkIte(Term^ t1, Term^ t2, Term^ t3) {
03327             return gcnew Term(m_ctx,m_ctx->MkIte(t1(), t2(), t3()));
03328         }
03329         Term^ MkIff(Term^ t1, Term^ t2) { return gcnew Term(m_ctx,m_ctx->MkIff(t1(), t2()));  }
03330         Term^ MkImplies(Term^ t1, Term^ t2) {return gcnew Term(m_ctx,m_ctx->MkImplies(t1(), t2()));}
03331         Term^ MkXor(Term^ t1, Term^ t2) { return gcnew Term(m_ctx,m_ctx->MkXor(t1(), t2())); }
03332         Term^ MkAnd(array<Term^>^ args) { return gcnew Term(m_ctx,m_ctx->MkAnd(CopyArray(args))); }
03333         Term^ MkAnd(Term^ t1, Term^ t2) { return gcnew Term(m_ctx,m_ctx->MkAnd(t1(), t2())); }
03334         Term^ MkOr(array<Term^>^ args) { return gcnew Term(m_ctx,m_ctx->MkOr(CopyArray(args))); }
03335         Term^ MkOr(Term^ t1, Term^ t2) { return gcnew Term(m_ctx,m_ctx->MkOr(t1(), t2())); }
03336         Term^ MkAdd(array<Term^>^ args) { return gcnew Term(m_ctx,m_ctx->MkAdd(CopyArray(args))); }
03337         Term^ MkAdd(Term^ t1, Term^ t2) { return gcnew Term(m_ctx,m_ctx->MkAdd(t1(), t2())); }
03338         Term^ MkMul(array<Term^>^ args) { return gcnew Term(m_ctx,m_ctx->MkMul(CopyArray(args))); }
03339         Term^ MkMul(Term^ t1, Term^ t2) { return gcnew Term(m_ctx,m_ctx->MkMul(t1(), t2())); }
03340         Term^ MkSub(array<Term^>^ args) { return gcnew Term(m_ctx,m_ctx->MkSub(CopyArray(args))); }
03341         Term^ MkSub(Term^ t1, Term^ t2) { return gcnew Term(m_ctx,m_ctx->MkSub(t1(), t2())); }
03342         Term^ MkUnaryMinus(Term^ arg) { return gcnew Term(m_ctx,m_ctx->MkUnaryMinus(arg())); }
03343         Term^ MkDiv(Term^ t1, Term^ t2) { return gcnew Term(m_ctx,m_ctx->MkDiv(t1(), t2())); }
03344         Term^ MkMod(Term^ t1, Term^ t2) { return gcnew Term(m_ctx,m_ctx->MkMod(t1(), t2())); }
03345         Term^ MkRem(Term^ t1, Term^ t2) { return gcnew Term(m_ctx,m_ctx->MkRem(t1(), t2())); }
03346         Term^ MkLt(Term^ t1, Term^ t2) { return gcnew Term(m_ctx,m_ctx->MkLt(t1(), t2())); }
03347         Term^ MkLe(Term^ t1, Term^ t2) { return gcnew Term(m_ctx,m_ctx->MkLe(t1(), t2())); }
03348         Term^ MkGt(Term^ t1, Term^ t2) { return gcnew Term(m_ctx,m_ctx->MkGt(t1(), t2())); }
03349         Term^ MkGe(Term^ t1, Term^ t2) { return gcnew Term(m_ctx,m_ctx->MkGe(t1(), t2())); }
03350         Term^ MkInt2Real(Term^ t1) { return gcnew Term(m_ctx,m_ctx->MkInt2Real(t1())); }
03351         Term^ MkBvNot(Term^ t1) { return gcnew Term(m_ctx,m_ctx->MkBvNot(t1())); }
03352         Term^ MkBvAnd(Term^ t1, Term^ t2) { return gcnew Term(m_ctx,m_ctx->MkBvAnd(t1(), t2())); }
03353         Term^ MkBvOr(Term^ t1, Term^ t2) { return gcnew Term(m_ctx,m_ctx->MkBvOr(t1(), t2())); }
03354         Term^ MkBvXor(Term^ t1, Term^ t2) { return gcnew Term(m_ctx,m_ctx->MkBvXor(t1(), t2())); }
03355         Term^ MkBvNand(Term^ t1, Term^ t2) { return gcnew Term(m_ctx,m_ctx->MkBvNand(t1(), t2())); }
03356         Term^ MkBvNor(Term^ t1, Term^ t2) { return gcnew Term(m_ctx,m_ctx->MkBvNor(t1(), t2())); }
03357         Term^ MkBvXnor(Term^ t1, Term^ t2) { return gcnew Term(m_ctx,m_ctx->MkBvXnor(t1(), t2())); }
03358         Term^ MkBvNeg(Term^ t1) { return gcnew Term(m_ctx,m_ctx->MkBvNeg(t1())); }
03359         Term^ MkBvAdd(Term^ t1, Term^ t2) { return gcnew Term(m_ctx,m_ctx->MkBvAdd(t1(), t2())); }
03360         Term^ MkBvSub(Term^ t1, Term^ t2) { return gcnew Term(m_ctx,m_ctx->MkBvSub(t1(), t2())); }
03361         Term^ MkBvMul(Term^ t1, Term^ t2) { return gcnew Term(m_ctx,m_ctx->MkBvMul(t1(), t2())); }
03362         Term^ MkBvUdiv(Term^ t1, Term^ t2) { return gcnew Term(m_ctx,m_ctx->MkBvUdiv(t1(), t2())); }
03363         Term^ MkBvSdiv(Term^ t1, Term^ t2) { return gcnew Term(m_ctx,m_ctx->MkBvSdiv(t1(), t2())); }
03364         Term^ MkBvUrem(Term^ t1, Term^ t2) { return gcnew Term(m_ctx,m_ctx->MkBvUrem(t1(), t2())); }
03365         Term^ MkBvSrem(Term^ t1, Term^ t2) { return gcnew Term(m_ctx,m_ctx->MkBvSrem(t1(), t2())); }
03366         Term^ MkBvSmod(Term^ t1, Term^ t2) { return gcnew Term(m_ctx,m_ctx->MkBvSmod(t1(), t2())); }
03367         Term^ MkBvUlt(Term^ t1, Term^ t2) { return gcnew Term(m_ctx,m_ctx->MkBvUlt(t1(), t2())); }
03368         Term^ MkBvSlt(Term^ t1, Term^ t2) { return gcnew Term(m_ctx,m_ctx->MkBvSlt(t1(), t2())); }
03369         Term^ MkBvUle(Term^ t1, Term^ t2) { return gcnew Term(m_ctx,m_ctx->MkBvUle(t1(), t2())); }
03370         Term^ MkBvSle(Term^ t1, Term^ t2) { return gcnew Term(m_ctx,m_ctx->MkBvSle(t1(), t2())); }
03371         Term^ MkBvUge(Term^ t1, Term^ t2) { return gcnew Term(m_ctx,m_ctx->MkBvUge(t1(), t2())); }
03372         Term^ MkBvSge(Term^ t1, Term^ t2) { return gcnew Term(m_ctx,m_ctx->MkBvSge(t1(), t2())); }
03373         Term^ MkBvUgt(Term^ t1, Term^ t2) { return gcnew Term(m_ctx,m_ctx->MkBvUgt(t1(), t2())); }
03374         Term^ MkBvSgt(Term^ t1, Term^ t2) { return gcnew Term(m_ctx,m_ctx->MkBvSgt(t1(), t2())); }
03375         Term^ MkBvConcat(Term^ t1, Term^ t2) { return gcnew Term(m_ctx,m_ctx->MkBvConcat(t1(), t2())); }
03376         Term^ MkBvExtract(unsigned high, unsigned low, Term^ t) {
03377             return gcnew Term(m_ctx,m_ctx->MkBvExtract(high, low, t()));
03378         }
03379         Term^ MkBvSignExt(unsigned i, Term^ t) {
03380             return gcnew Term(m_ctx,m_ctx->MkBvSignExt(i, t()));
03381         }
03382         Term^ MkBvZeroExt(unsigned i, Term^ t) {
03383             return gcnew Term(m_ctx,m_ctx->MkBvZeroExt(i, t()));
03384         }
03385         Term^ MkBvShl(Term^ t1, Term^ t2) { return gcnew Term(m_ctx,m_ctx->MkBvShl(t1(), t2())); }
03386         Term^ MkBvLshr(Term^ t1, Term^ t2) { return gcnew Term(m_ctx,m_ctx->MkBvLshr(t1(), t2())); }
03387         Term^ MkBvAshr(Term^ t1, Term^ t2) { return gcnew Term(m_ctx,m_ctx->MkBvAshr(t1(), t2())); }
03388         Term^ MkBvRotateLeft(unsigned i, Term^ t1) {
03389             return gcnew Term(m_ctx,m_ctx->MkBvRotateLeft(i,t1()));
03390         }
03391         Term^ MkBvRotateRight(unsigned i, Term^ t1) { return gcnew Term(m_ctx,m_ctx->MkBvRotateRight(i,t1()));  }
03392         Term^ MkBv2Int(Term^ t1, bool is_signed) { return gcnew Term(m_ctx, m_ctx->MkBv2Int(t1(), is_signed)); }
03393         Term^ MkInt2Bv(unsigned n, Term^ t1) { return gcnew Term(m_ctx, m_ctx->MkInt2Bv(n, t1())); }
03394         Term^ MkBvAddNoOverflow(Term^ t1, Term^ t2, bool is_signed) { 
03395             return gcnew Term(m_ctx,m_ctx->MkBvAddNoOverflow(t1(), t2(), is_signed)); 
03396         }
03397         Term^ MkBvAddNoUnderflow(Term^ t1, Term^ t2) { 
03398             return gcnew Term(m_ctx,m_ctx->MkBvAddNoUnderflow(t1(), t2())); 
03399         }
03400         Term^ MkBvSubNoOverflow(Term^ t1, Term^ t2) { 
03401             return gcnew Term(m_ctx,m_ctx->MkBvSubNoOverflow(t1(), t2())); 
03402         }
03403         Term^ MkBvSubNoUnderflow(Term^ t1, Term^ t2, bool is_signed) { 
03404             return gcnew Term(m_ctx,m_ctx->MkBvSubNoUnderflow(t1(), t2(), is_signed)); 
03405         }
03406         Term^ MkBvSDivNoOverflow(Term^ t1, Term^ t2) { 
03407             return gcnew Term(m_ctx,m_ctx->MkBvSDivNoOverflow(t1(), t2())); 
03408         }
03409         Term^ MkBvNegNoOverflow(Term^ t1) { 
03410             return gcnew Term(m_ctx,m_ctx->MkBvNegNoOverflow(t1())); 
03411         }
03412         Term^ MkBvMulNoOverflow(Term^ t1, Term^ t2, bool is_signed) { 
03413             return gcnew Term(m_ctx,m_ctx->MkBvMulNoOverflow(t1(), t2(), is_signed)); 
03414         }
03415         Term^ MkBvMulNoUnderflow(Term^ t1, Term^ t2) { 
03416             return gcnew Term(m_ctx,m_ctx->MkBvMulNoUnderflow(t1(), t2())); 
03417         }
03418         Term^ MkArraySelect(Term^ a, Term^ i) { return gcnew Term(m_ctx,m_ctx->MkArraySelect(a(), i()));  }
03419         Term^ MkArrayStore(Term^ a, Term^ i, Term^ v) {
03420             return gcnew Term(m_ctx,m_ctx->MkArrayStore(a(), i(), v()));
03421         }
03422         Term^ MkArrayMap(FuncDecl^ f, array<Term^>^ args) {
03423             return gcnew Term(m_ctx, m_ctx->MkArrayMap(f(), CopyArray(args)));
03424         }
03425         Term^ MkArrayConst(Sort^ domain, Term^ v) { return gcnew Term(m_ctx,m_ctx->MkArrayConst(domain(), v())); }
03426         Term^ MkArrayDefault(Term^ a) { return gcnew Term(m_ctx,m_ctx->MkArrayDefault(a())); }
03427         Sort^ MkSetSort(Sort^ ty) { return gcnew Sort(m_ctx,m_ctx->MkSetSort(ty())); }
03428         Term^ MkEmptySet(Sort^ ty) { return gcnew Term(m_ctx,m_ctx->MkEmptySet(ty())); }
03429         Term^ MkFullSet(Sort^ ty) { return gcnew Term(m_ctx,m_ctx->MkFullSet(ty())); }
03430         Term^ MkSetAdd(Term^ set, Term^ elem) { return gcnew Term(m_ctx,m_ctx->MkSetAdd(set(), elem())); }
03431         Term^ MkSetDel(Term^ set, Term^ elem) { return gcnew Term(m_ctx,m_ctx->MkSetDel(set(), elem())); }
03432         Term^ MkSetUnion(array<Term^>^ sets) {
03433             return gcnew Term(m_ctx,m_ctx->MkSetUnion(CopyArray(sets)));
03434         }
03435         Term^ MkSetUnion(Term^ set1, Term^ set2) {
03436             return gcnew Term(m_ctx,m_ctx->MkSetUnion(set1(), set2()));
03437         }
03438         Term^ MkSetIntersect(array<Term^>^ sets) {
03439             return gcnew Term(m_ctx,m_ctx->MkSetIntersect(CopyArray(sets)));
03440         }
03441         Term^ MkSetIntersect(Term^ set1, Term^ set2) {
03442             return gcnew Term(m_ctx,m_ctx->MkSetIntersect(set1(), set2()));
03443         }
03444         Term^ MkSetDifference(Term^ t1, Term^ t2) {
03445             return gcnew Term(m_ctx,m_ctx->MkSetDifference(t1(), t2()));
03446         }
03447         Term^ MkSetComplement(Term^ arg) {
03448             return gcnew Term(m_ctx,m_ctx->MkSetComplement(arg()));
03449         }
03450         Term^ MkSetMember(Term^ elem, Term^ set) {
03451             return gcnew Term(m_ctx,m_ctx->MkSetMember(elem(), set()));
03452         }
03453         Term^ MkSetSubset(Term^ t1, Term^ t2) {
03454             return gcnew Term(m_ctx,m_ctx->MkSetSubset(t1(), t2()));
03455         }
03456         
03457         FuncDecl^ MkInjectiveFunction(String^ name, array<Sort^>^ domain, Sort^ range) {
03458             return gcnew FuncDecl(m_ctx,m_ctx->MkInjectiveFunction(name, CopyArray(domain), range()));
03459         }
03460         FuncDecl^ MkInjectiveFunction(Symbol^ name, array<Sort^>^ domain, Sort^ range) {
03461             return gcnew FuncDecl(m_ctx,m_ctx->MkInjectiveFunction(name, CopyArray(domain), range()));
03462         }
03463 
03464         Term^ MkNumeral(String^ numeral, Sort^ ty) {
03465             return gcnew Term(m_ctx,m_ctx->MkNumeral(numeral, ty()));
03466         }
03467         Term^ MkNumeral(int n, Sort^ ty) { return gcnew Term(m_ctx,m_ctx->MkNumeral(n, ty()));  }
03468         Term^ MkNumeral(unsigned n, Sort^ ty) { return gcnew Term(m_ctx,m_ctx->MkNumeral(n, ty())); }
03469         Term^ MkNumeral(__int64 n, Sort^ ty) { return gcnew Term(m_ctx,m_ctx->MkNumeral(n, ty())); }
03470         Term^ MkNumeral(unsigned __int64 n, Sort^ ty) { return gcnew Term(m_ctx,m_ctx->MkNumeral(n, ty())); }
03471         Pattern^ MkPattern(array<Term^>^ terms) { return gcnew Pattern(m_ctx,m_ctx->MkPattern(CopyArray(terms))); }
03472         Term^ MkBound(unsigned index, Sort^ ty) { return gcnew Term(m_ctx,m_ctx->MkBound(index, ty())); }
03473 
03474         Term^ MkForall(
03475             unsigned weight,
03476             array<Pattern^>^ patterns,
03477             array<Sort^>^ types,
03478             array<Symbol^>^ names,
03479             Term^ body
03480             ) {
03481             return gcnew Term(m_ctx,m_ctx->MkForall(weight, CopyArray(patterns), CopyArray(types), names, body()));
03482         }
03483 
03484         Term^ MkForall(
03485             unsigned weight,
03486             array<Pattern^>^ patterns,
03487             array<Sort^>^ types,
03488             array<String^>^ names,
03489             Term^ body
03490             ) {
03491             return gcnew Term(m_ctx,m_ctx->MkForall(weight, CopyArray(patterns), CopyArray(types), names, body()));
03492         }
03493 
03494         Term^ MkForall(
03495             unsigned           weight,
03496             array<Term^>^   bound,
03497             array<Pattern^>^ patterns,
03498             Term^ body
03499             ) {
03500             return gcnew Term(m_ctx,m_ctx->MkForall(weight, CopyArray(bound), CopyArray(patterns), body()));
03501         }
03502 
03503 
03504         Term^ MkExists(
03505             unsigned weight,
03506             array<Pattern^>^ patterns,
03507             array<Sort^>^ types,
03508             array<Symbol^>^ names,
03509             Term^ body
03510             ) {
03511             return gcnew Term(m_ctx,m_ctx->MkExists(weight, CopyArray(patterns), CopyArray(types), names, body()));
03512         }
03513 
03514         Term^ MkExists(
03515             unsigned weight,
03516             array<Pattern^>^ patterns,
03517             array<Sort^>^ types,
03518             array<String^>^ names,
03519             Term^ body
03520             ) {
03521             return gcnew Term(m_ctx,m_ctx->MkExists(weight, CopyArray(patterns), CopyArray(types), names, body()));
03522         }
03523 
03524         Term^ MkExists(
03525             unsigned           weight,
03526             array<Term^>^   bound,
03527             array<Pattern^>^ patterns,
03528             Term^            body
03529             ) {
03530             return gcnew Term(m_ctx,m_ctx->MkExists(weight, CopyArray(bound), CopyArray(patterns), body()));
03531         }
03532 
03533         Term^ MkQuantifier(
03534             bool                is_forall,
03535             unsigned            weight,
03536             array<Pattern^>^ patterns,
03537             array<Term^>^    no_patterns,
03538             array<Sort^>^    types,
03539             array<Symbol^>^     names,
03540             Term^            body
03541             ) {
03542             return gcnew Term(m_ctx,m_ctx->MkQuantifier(
03543                                      is_forall, weight, 
03544                                      CopyArray(patterns),
03545                                      CopyArray(no_patterns),
03546                                      CopyArray(types),
03547                                      names,
03548                                      body()));
03549         }
03550 
03551         SymbolKind GetSymbolKind(Symbol^ s) { return m_ctx->GetSymbolKind(s); }
03552         int GetSymbolInt(Symbol^ s) { return m_ctx->GetSymbolInt(s); }
03553         String^ GetSymbolString(Symbol^ s) { return m_ctx->GetSymbolString(s); }
03554         bool IsEq(Term^ t1, Term^ t2) { return m_ctx->IsEq(t1(), t2()); }
03555         TermKind GetTermKind(Term^ a) { return m_ctx->GetTermKind(a()); }
03556         DeclKind GetDeclKind(FuncDecl^ d) { return m_ctx->GetDeclKind(d()); }
03557         array<IParameter^>^ GetDeclParameters(FuncDecl^ d);
03558         FuncDecl^ GetAppDecl(Term^ a) { return gcnew FuncDecl(m_ctx,m_ctx->GetAppDecl(a())); }
03559         array<Term^>^ GetAppArgs(Term^ a) { return CopyTermArray(m_ctx->GetAppArgs(a())); }
03560         String^ GetNumeralString(Term^ a) { return m_ctx->GetNumeralString(a()); }
03561         int GetNumeralInt(Term^ v) { return m_ctx->GetNumeralInt(v()); }
03562         bool TryGetNumeralInt(Term^ v, [Runtime::InteropServices::Out] int% i) { return m_ctx->TryGetNumeralInt(v(), i); }
03563         unsigned int GetNumeralUInt(Term^ v) { return m_ctx->GetNumeralUInt(v()); }
03564         bool TryGetNumeralUInt(Term^ v, [Runtime::InteropServices::Out] unsigned int% u) { return m_ctx->TryGetNumeralUInt(v(), u); }
03565         __int64 GetNumeralInt64(Term^ v) { return m_ctx->GetNumeralInt64(v()); }
03566         bool TryGetNumeralInt64(Term^ v, [Runtime::InteropServices::Out] __int64% i) { return m_ctx->TryGetNumeralInt64(v(), i); }
03567         unsigned __int64 GetNumeralUInt64(Term^ v) { return m_ctx->GetNumeralUInt64(v()); }
03568         bool TryGetNumeralUInt64(Term^ v, [Runtime::InteropServices::Out] unsigned __int64% u) { return m_ctx->TryGetNumeralUInt64(v(), u); }
03569 
03570 
03571         LBool GetBoolValue(Term^ v) { return m_ctx->GetBoolValue(v()); }
03572         bool TryGetArrayValue(Term^ a,[Runtime::InteropServices::Out] ArrayValue^% av);
03573 
03574         unsigned GetVarIndex(Term^ a) { return m_ctx->GetVarIndex(a()); }
03575         Quantifier^ GetQuantifier(Term^ a) { return GetQuantifier(m_ctx, a); }
03576 
03577         array<Term^>^ GetPatternTerms(Pattern^ p) { return CopyTermArray(m_ctx->GetPatternTerms(p())); }
03578         Symbol^ GetDeclName(FuncDecl^ d) { return m_ctx->GetDeclName(d()); }
03579         Symbol^ GetSortName(Sort^ ty) { return m_ctx->GetSortName(ty()); }
03580         Sort^ GetSort(Term^ a) { return gcnew Sort(m_ctx,m_ctx->GetSort(a())); }
03581         array<Sort^>^ GetDomain(FuncDecl^ d) { return CopySortArray(m_ctx->GetDomain(d())); }
03582         Sort^ GetRange(FuncDecl^ d) { return gcnew Sort(m_ctx,m_ctx->GetRange(d())); }
03583         SortKind GetSortKind(Sort^ t) { return m_ctx->GetSortKind(t()); }
03584         unsigned GetBvSortSize(Sort^ t) { return m_ctx->GetBvSortSize(t()); }
03585         Sort^ GetArraySortDomain(Sort^ t) { return gcnew Sort(m_ctx,m_ctx->GetArraySortDomain(t())); }
03586         Sort^ GetArraySortRange(Sort^ t) { return gcnew Sort(m_ctx,m_ctx->GetArraySortRange(t())); }
03587         FuncDecl^ GetTupleConstructor(Sort^ t) { return gcnew FuncDecl(m_ctx,m_ctx->GetTupleConstructor(t())); }
03588         array<FuncDecl^>^ GetTupleFields(Sort^ t) { return CopyFuncDeclArray(m_ctx->GetTupleFields(t())); }
03589 
03590     };
03591 
03592 
03593     public ref class FunctionEntry {
03594     public:
03595         array<Term^>^ Arguments;
03596         Term^         Result;
03597     };
03598 
03599     public ref class FunctionGraph {
03600     public:
03601         FuncDecl^        Declaration;
03602         array<FunctionEntry^>^ Entries;
03603         Term^               Else;
03604     };
03605 
03606 
03607     public ref class Model {
03608         RawModel^ m_model;
03609         Context^ m_ctx;
03610 
03611         ArrayValue^ Mk(RawArrayValue^ av);
03612         FunctionEntry^ Mk(RawFunctionEntry^ fe);
03613         FunctionGraph^ Mk(RawFunctionGraph^ fg);
03614         Dictionary<FuncDecl^, FunctionGraph^>^ Mk(Dictionary<FuncDeclPtr, RawFunctionGraph^>^ fgs);
03615 
03616     internal:
03617         property Context^ GetContext { Context^ get() { return m_ctx; }}
03618         property RawModel^ GetModel { RawModel^ get() { return m_model; }}
03619 
03620         Model(RawModel^ m, Context^ c) : m_model(m), m_ctx(c) {}
03621 
03622     public:
03623         ~Model() { m_model->Reset(); }
03624 
03625         array<FuncDecl^>^ GetModelConstants() {
03626             return m_ctx->CopyFuncDeclArray(m_model->GetModelConstants());
03627         }
03628 
03629         Dictionary<FuncDecl^, FunctionGraph^>^ GetFunctionGraphs() { return Mk(m_model->GetFunctionGraphs()); }
03630 
03631         Term^ Eval(Term^ t) { return gcnew Term(m_ctx->GetContext, m_model->Eval(t())); }
03632 
03633         Term^ Eval(FuncDecl^ d, array<Term^>^ args) {
03634             return gcnew Term(m_ctx->GetContext, m_model->Eval(d(), m_ctx->CopyArray(args)));
03635         }
03636 
03637         void Display(System::IO::TextWriter^ w) { m_model->Display(w); }
03638 
03639     };
03640 
03643 };
03644 };
03645 
03646 #endif
managed/Microsoft.Z3.h
