diff --git a/Makefile.in b/Makefile.in
new file mode 100644
index 000000000..e3e3ccfa9
--- /dev/null
+++ b/Makefile.in
@@ -0,0 +1,466 @@
+
+SHELL=/bin/sh
+SED=sed
+AWK=awk
+DOS2UNIX=@D2U@
+
+@SET_MAKE@
+
+##### Configuration #####
+CPPFLAGS_CORE=@CPPFLAGS@ -I lib -fopenmp -msse -msse2 -mfpmath=sse
+CXXFLAGS_CORE=@CXXFLAGS@
+ifeq ($(MODE),)
+Z3_BUILD_MODE=external
+else
+Z3_BUILD_MODE=$(MODE)
+endif
+LIBS=@LIBS@
+## -lrt is for timer_create and timer_settime
+LDFLAGS=@LDFLAGS@ -lpthread -fopenmp
+LDFLAGS_EXTRA=
+#########################
+
+Z3=z3
+TEST_CAPI=test_capi
+EPR=epr
+GROBNER=grobner
+TEST=test
+
+BIN_DIR=bin/$(Z3_BUILD_MODE)
+OBJ_DIR=obj/$(Z3_BUILD_MODE)
+SED_OBJ_DIR=obj\/$(Z3_BUILD_MODE)
+OBJ_TEST_DIR=obj-test/$(Z3_BUILD_MODE)
+SED_OBJ_TEST_DIR=obj-test\/$(Z3_BUILD_MODE)
+
+MAJ=$(shell grep 'Z3_MAJOR_VERSION' lib/version.h | cut -d ' ' -f 4)
+MIN=$(shell grep 'Z3_MINOR_VERSION' lib/version.h | cut -d ' ' -f 4)
+Z3_VERSION=$(MAJ).$(MIN)
+
+PLATFORM=@PLATFORM@
+
+
+ifeq ($(Z3_BUILD_MODE),release)
+CPPFLAGS=$(CPPFLAGS_CORE) -DNDEBUG
+CXXFLAGS=-O3 -fomit-frame-pointer $(CXXFLAGS_CORE)
+else
+ifeq ($(Z3_BUILD_MODE),smtcomp07)
+CPPFLAGS=$(CPPFLAGS_CORE) -DNDEBUG -DSMTCOMP
+CXXFLAGS=-O3 -fomit-frame-pointer $(CXXFLAGS_CORE)
+# doesn't work on cygwin
+LDFLAGS_EXTRA=@STATIC_FLAGS@
+else
+ifeq ($(Z3_BUILD_MODE),external)
+CPPFLAGS=$(CPPFLAGS_CORE) -DNDEBUG -D_EXTERNAL_RELEASE
+CXXFLAGS=-O3 -fomit-frame-pointer $(CXXFLAGS_CORE)
+# doesn't work on cygwin
+LDFLAGS_EXTRA=@STATIC_FLAGS@
+else
+ifeq ($(Z3_BUILD_MODE),debug)
+CPPFLAGS=$(CPPFLAGS_CORE) -DZ3DEBUG -D_TRACE
+CXXFLAGS=-g -Wall $(CXXFLAGS_CORE)
+else
+ifeq ($(Z3_BUILD_MODE),debugopt)
+CPPFLAGS=$(CPPFLAGS_CORE) -DNDEBUG -DZ3DEBUG -D_TRACE
+CXXFLAGS=-g -O1 $(CXXFLAGS_CORE)
+else
+ifeq ($(Z3_BUILD_MODE),trace)
+CPPFLAGS=$(CPPFLAGS_CORE) -DNDEBUG -D_TRACE
+CXXFLAGS=-g -O1 $(CXXFLAGS_CORE)
+else
+ifeq ($(Z3_BUILD_MODE),profile)
+CPPFLAGS=$(CPPFLAGS_CORE) -DNDEBUG
+CXXFLAGS=-g -pg -O2 $(CXXFLAGS_CORE)
+LDFLAGS_EXTRA=-pg
+else
+ifeq ($(Z3_BUILD_MODE),gcov)
+CPPFLAGS=$(CPPFLAGS_CORE) -DNDEBUG
+CXXFLAGS=-g -fprofile-arcs -ftest-coverage -O2 $(CXXFLAGS_CORE)
+LDFLAGS_EXTRA=-fprofile-arcs -ftest-coverage
+else
+ifeq ($(Z3_BUILD_MODE),external_parallel)
+CPPFLAGS=$(CPPFLAGS_CORE) -DNDEBUG -D_EXTERNAL_RELEASE -D_Z3_BUILD_PARALLEL_SMT
+CXXFLAGS=-O3 -fomit-frame-pointer $(CXXFLAGS_CORE)
+# doesn't work on cygwin
+LDFLAGS_EXTRA=@STATIC_FLAGS@
+else
+ifeq ($(Z3_BUILD_MODE),debug_parallel)
+CPPFLAGS=$(CPPFLAGS_CORE) -DZ3DEBUG -D_TRACE -D_Z3_BUILD_PARALLEL_SMT
+CXXFLAGS=-g -Wall $(CXXFLAGS_CORE)
+else
+$(error INVALID BUILD MODE = $(Z3_BUILD_MODE))
+endif
+endif
+endif
+endif
+endif
+endif
+endif
+endif
+endif
+endif
+
+LIBFLAGS=@SLIBFLAGS@
+
+################################
+#
+# Extract the source files from
+# the MSVC++ project files.
+#
+# lib.vcproj ===> lib.srcs
+# shell.vcproj ===> shell.srcs
+#
+################################
+
+main: $(BIN_DIR)/$(Z3)
+
+lib.srcs: lib/lib.vcxproj
+ @echo Making 'lib.srcs'...
+ @cp $< lib0.srcs
+ @chmod +rw lib0.srcs
+ @$(DOS2UNIX) lib0.srcs
+ @$(AWK) '/cpp\"/{ print $$0 }' lib0.srcs > lib1.srcs
+ @$(SED) 's|\"||g;s|||g;s|Include=|lib/|g' lib1.srcs > lib2.srcs
+ @$(AWK) 'BEGIN { printf ("LIB_SRCS= "); } { printf($$1 " ") } END { print ""; }' lib2.srcs > $@
+ @rm -f lib0.srcs
+ @rm -f lib1.srcs
+ @rm -f lib2.srcs
+
+shell.srcs: shell/shell.vcxproj
+ @echo Making 'shell.srcs'...
+ @cp $< shell0.srcs
+ @chmod +rw shell0.srcs
+ @$(DOS2UNIX) shell0.srcs
+ @$(AWK) '/cpp\"/{ print $$0 }' shell0.srcs > shell1.srcs
+ @$(SED) 's|\"||g;s|||g;s|Include=|shell/|g' shell1.srcs > shell2.srcs
+ @$(AWK) 'BEGIN { printf ("SHELL_SRCS= "); } { printf($$1 " ") } END { print ""; }' shell2.srcs > $@
+ @rm -f shell0.srcs
+ @rm -f shell1.srcs
+ @rm -f shell2.srcs
+
+epr.srcs: epr/epr.vcxproj
+ @echo Making 'epr.srcs'...
+ @cp $< epr0.srcs
+ @chmod +rw epr0.srcs
+ @$(DOS2UNIX) epr0.srcs
+ @$(AWK) '/cpp\"/{ print $$0 }' epr0.srcs > epr1.srcs
+ @$(SED) 's|\"||g;s|||g;s|Include=|epr/|g' epr1.srcs > epr2.srcs
+ @$(AWK) 'BEGIN { printf ("EPR_SRCS= "); } { printf($$1 " ") } END { print ""; }' epr2.srcs > $@
+ @rm -f epr0.srcs
+ @rm -f epr1.srcs
+ @rm -f epr2.srcs
+
+test.srcs: test/test.vcxproj
+ @echo Making 'test.srcs'...
+ @cp $< test0.srcs
+ @chmod +rw test0.srcs
+ @$(DOS2UNIX) test0.srcs
+ @$(AWK) '/cpp\"/{ print $$0 }' test0.srcs > test1.srcs
+ @$(SED) 's|\"||g;s|||g;s|Include=|test/|g' test1.srcs > test2.srcs
+ @$(AWK) 'BEGIN { printf ("TEST_SRCS= "); } { printf($$1 " ") } END { print ""; }' test2.srcs > $@
+ @rm -f test0.srcs
+ @rm -f test1.srcs
+ @rm -f test2.srcs
+
+
+include lib.srcs
+include shell.srcs
+include epr.srcs
+include test.srcs
+
+LIB_SRCS+=@EXTRA_LIB_SRCS@
+LIB_OBJS=$(LIB_SRCS:lib/%.cpp=$(OBJ_DIR)/%.o)
+SHELL_OBJS=$(SHELL_SRCS:shell/%.cpp=$(OBJ_DIR)/%.o)
+
+OBJS=$(LIB_OBJS) $(SHELL_OBJS)
+TEST_CAPI_OBJS=$(OBJ_DIR)/test_capi.o $(LIB_OBJS)
+EPR_OBJS=$(EPR_SRCS:epr/%.cpp=$(OBJ_DIR)/%.o) $(LIB_OBJS)
+GROBNER_OBJS=$(OBJ_DIR)/grobner_main.o $(LIB_OBJS)
+TEST_OBJS=$(TEST_SRCS:test/%.cpp=$(OBJ_TEST_DIR)/%.o)
+
+$(BIN_DIR)/$(Z3): $(OBJ_DIR) $(BIN_DIR) $(OBJS)
+ @mkdir -p $(BIN_DIR)
+ $(CXX) -o $(BIN_DIR)/$(Z3) $(OBJS) $(LDFLAGS) $(LDFLAGS_EXTRA) $(LIBS)
+
+$(BIN_DIR)/$(TEST): $(OBJ_DIR) $(BIN_DIR) $(LIB_OBJS) $(TEST_OBJS)
+ @mkdir -p $(BIN_DIR)
+ $(CXX) -o $(BIN_DIR)/$(TEST) $(LIB_OBJS) $(TEST_OBJS) $(LDFLAGS) $(LDFLAGS_EXTRA) $(LIBS)
+
+$(BIN_DIR)/$(TEST_CAPI): $(OBJ_DIR) $(BIN_DIR) $(TEST_CAPI_OBJS)
+ @mkdir -p $(BIN_DIR)
+ $(CXX) -o $(BIN_DIR)/$(TEST_CAPI) $(TEST_CAPI_OBJS) $(LDFLAGS) $(LDFLAGS_EXTRA) $(LIBS)
+
+$(BIN_DIR)/$(EPR): $(OBJ_DIR) $(BIN_DIR) $(EPR_OBJS)
+ @mkdir -p $(BIN_DIR)
+ $(CXX) -o $(BIN_DIR)/$(EPR) $(EPR_OBJS) $(LDFLAGS) $(LDFLAGS_EXTRA) $(LIBS)
+
+$(BIN_DIR)/lib$(Z3).@SO_EXT@: $(OBJ_DIR) $(BIN_DIR) $(LIB_OBJS)
+ @mkdir -p $(BIN_DIR)
+ $(CXX) -o $(BIN_DIR)/lib$(Z3).@SO_EXT@ $(LIB_OBJS) $(LIBFLAGS) $(LIBS) @COMP_VERSIONS@
+
+$(BIN_DIR)/lib$(Z3).a: $(OBJ_DIR) $(BIN_DIR) $(LIB_OBJS)
+ @mkdir -p $(BIN_DIR)
+ ar -cvr $(BIN_DIR)/lib$(Z3).a $(LIB_OBJS)
+
+$(BIN_DIR)/$(GROBNER): $(OBJ_DIR) $(BIN_DIR) $(GROBNER_OBJS)
+ @mkdir -p $(BIN_DIR)
+ $(CXX) -o $(BIN_DIR)/$(GROBNER) $(GROBNER_OBJS) $(LDFLAGS) $(LDFLAGS_EXTRA) $(LIBS)
+
+$(BIN_DIR):
+ mkdir -p $(BIN_DIR)
+
+$(OBJ_DIR):
+ mkdir -p $(OBJ_DIR)
+
+$(OBJ_TEST_DIR):
+ mkdir -p $(OBJ_TEST_DIR)
+
+smtcomp07: $(BIN_DIR)/$(Z3)
+ rm -r -f z3
+ mkdir z3
+ cp $(BIN_DIR)/$(Z3) z3/run
+ strip z3/run
+ cp doc/MAGIC_NUMBER z3/
+ cp doc/README-SMTCOMP07 z3/README
+ cp doc/NOTICES-SMTCOMP07 z3/NOTICES
+ cp doc/z3.pdf z3/
+ tar -czf z3.tar.gz z3
+
+test_capi: $(BIN_DIR)/$(TEST_CAPI)
+
+epr: $(BIN_DIR)/$(EPR)
+
+@SO_EXT@: $(BIN_DIR)/lib$(Z3).@SO_EXT@
+
+a: $(BIN_DIR)/lib$(Z3).a
+
+grobner: $(BIN_DIR)/$(GROBNER)
+
+test: $(BIN_DIR)/$(TEST)
+
+################################
+#
+# Grobner
+#
+################################
+lib/grobner_main.cpp: test/igrobner.cpp
+ cp test/igrobner.cpp lib/grobner_main.cpp
+ chmod +rw lib/grobner_main.cpp
+
+$(OBJ_DIR)/grobner_main.o: lib/grobner_main.cpp
+ @mkdir -p $(OBJ_DIR)
+ $(CXX) $(CPPFLAGS) $(CXXFLAGS) -DGB_APP -c -o $@ $<
+
+################################
+#
+# .cpp ===> .o
+#
+################################
+
+$(OBJ_DIR)/%.o : lib/%.cpp
+ @mkdir -p $(OBJ_DIR)
+ $(CXX) $(CPPFLAGS) $(CXXFLAGS) -c -o $@ $<
+
+$(OBJ_TEST_DIR)/%.o : test/%.cpp
+ @mkdir -p $(OBJ_TEST_DIR)
+ $(CXX) $(CPPFLAGS) $(CXXFLAGS) -c -o $@ $<
+
+$(OBJ_DIR)/%.o : shell/%.cpp
+ @mkdir -p $(OBJ_DIR)
+ $(CXX) $(CPPFLAGS) $(CXXFLAGS) -c -o $@ $<
+
+$(OBJ_DIR)/%.o : test_capi/%.c
+ @mkdir -p $(OBJ_DIR)
+ $(CXX) $(CPPFLAGS) $(CXXFLAGS) -I ../lib -c -o $@ $<
+
+$(OBJ_DIR)/%.o : epr/%.cpp
+ @mkdir -p $(OBJ_DIR)
+ $(CXX) $(CPPFLAGS) $(CXXFLAGS) -c -o $@ $<
+
+################################
+#
+# Dependency files
+#
+# .cpp ===> .d
+#
+################################
+
+$(OBJ_DIR)/%.d: lib/%.cpp
+ @echo Making dependency file \'$@\' ...
+ @mkdir -p $(OBJ_DIR)
+ @$(SHELL) -ec '$(CXX) -MM $(CPPFLAGS) $< | $(SED) '\''s/\($*\)\.o[ :]*/$(SED_OBJ_DIR)\/\1.o $(SED_OBJ_DIR)\/\1.d : /g'\'' > $@; [ -s $@ ] || rm -f $@'
+
+$(OBJ_DIR)/%.d: shell/%.cpp
+ @echo Making dependency file \'$@\' ...
+ @mkdir -p $(OBJ_DIR)
+ @$(SHELL) -ec '$(CXX) -MM $(CPPFLAGS) $< | $(SED) '\''s/\($*\)\.o[ :]*/$(SED_OBJ_DIR)\/\1.o $(SED_OBJ_DIR)\/\1.d : /g'\'' > $@; [ -s $@ ] || rm -f $@'
+
+$(OBJ_TEST_DIR)/%.d: test/%.cpp
+ @echo Making dependency file \'$@\' ...
+ @mkdir -p $(OBJ_TEST_DIR)
+ @$(SHELL) -ec '$(CXX) -MM $(CPPFLAGS) $< | $(SED) '\''s/\($*\)\.o[ :]*/$(SED_OBJ_TEST_DIR)\/\1.o $(SED_OBJ_TEST_DIR)\/\1.d : /g'\'' > $@; [ -s $@ ] || rm -f $@'
+
+
+include $(LIB_SRCS:lib/%.cpp=$(OBJ_DIR)/%.d)
+include $(SHELL_SRCS:shell/%.cpp=$(OBJ_DIR)/%.d)
+include $(TEST_SRCS:test/%.cpp=$(OBJ_TEST_DIR)/%.d)
+
+################################
+#
+# Cleanup
+#
+################################
+.PHONY: clean
+
+clean:
+ rm -f $(BIN_DIR)/$(Z3)
+ rm -f $(OBJ_DIR)/*
+ rm -f lib.srcs
+ rm -f shell.srcs
+ find . -name '*.bb' -exec rm -f '{}' ';'
+ find . -name '*.bbg' -exec rm -f '{}' ';'
+ find . -name '*.da' -exec rm -f '{}' ';'
+ find . -name '*.gcov' -exec rm -f '{}' ';'
+ find . -name 'cachegrind*' -exec rm -f '{}' ';'
+ find . -name 'a.out' -exec rm -f '{}' ';'
+ find . -name 'a.exe' -exec rm -f '{}' ';'
+ find . -name 'core' -exec rm -f '{}' ';'
+
+################################
+#
+# Release
+#
+# NOTE: In 64-bit systems it is not possible to build a dynamic library using static gmp.
+# So, EXTRA_LIBS="" in 64-bit systems.
+# EXTRA_LIBS="$(BIN_DIR)/lib$(Z3)-gmp.so" in 32-bit systems.
+################################
+release: $(BIN_DIR)/$(Z3) $(BIN_DIR)/lib$(Z3).@SO_EXT@ @EXTRA_LIBS@ $(BIN_DIR)/lib$(Z3).a
+ @rm -f -r z3
+ @mkdir -p z3
+ @mkdir -p z3/bin
+ @mkdir -p z3/lib
+ @mkdir -p z3/include
+ @mkdir -p z3/examples
+ @mkdir -p z3/ocaml
+ @mkdir -p z3/python
+ @mkdir -p z3/examples/c
+ @mkdir -p z3/examples/c++
+ @mkdir -p z3/examples/python
+ @mkdir -p z3/examples/maxsat
+ @mkdir -p z3/examples/theory
+ @mkdir -p z3/examples/ocaml
+ @cp lib/z3.h z3/include
+ @cp lib/z3_v1.h z3/include
+ @cp lib/z3_api.h z3/include
+ @cp lib/z3_macros.h z3/include
+ @cp ml/z3_stubs.c z3/ocaml
+ @cp ml/z3_theory_stubs.c z3/ocaml
+ @cp ml/z3.mli z3/ocaml
+ @cp ml/z3.ml z3/ocaml
+ @cp ml_release/build-lib.sh z3/ocaml
+ @$(DOS2UNIX) z3/ocaml/build-lib.sh
+ @chmod +rwx z3/ocaml/build-lib.sh
+ @cp ml_release/README_$(PLATFORM) z3/ocaml/README
+ @$(DOS2UNIX) z3/ocaml/README
+ @cp ml_release/build-test.sh z3/examples/ocaml
+ @$(DOS2UNIX) z3/examples/ocaml/build-test.sh
+ @chmod +rwx z3/examples/ocaml/build-test.sh
+ @cp ml_release/README_test_$(PLATFORM) z3/examples/ocaml/README
+ @$(DOS2UNIX) z3/examples/ocaml/README
+ @$(DOS2UNIX) z3/include/*
+ @cp $(BIN_DIR)/$(Z3) z3/bin
+ @cp $(BIN_DIR)/lib$(Z3).@SO_EXT@ z3/lib
+ @cp $(BIN_DIR)/lib$(Z3).a z3/lib
+ @cp test_capi/test_capi.c z3/examples/c
+ @$(DOS2UNIX) z3/examples/c/test_capi.c
+ @cp test_capi/README-$(PLATFORM).txt z3/examples/c/README
+ @$(DOS2UNIX) z3/examples/c/README
+ @cp test_capi/build-external-$(PLATFORM).sh z3/examples/c/build.sh
+ @cp test_capi/build-static-$(PLATFORM).sh z3/examples/c/build-static.sh
+ @$(DOS2UNIX) z3/examples/c/build.sh
+ @chmod +rwx z3/examples/c/build.sh
+ @$(DOS2UNIX) z3/examples/c/build-static.sh
+ @chmod +rwx z3/examples/c/build-static.sh
+ @cp test_capi/exec-external-$(PLATFORM).sh z3/examples/c/exec.sh
+ @$(DOS2UNIX) z3/examples/c/exec.sh
+ @chmod +rwx z3/examples/c/exec.sh
+ @cp maxsat/maxsat.c z3/examples/maxsat
+ @$(DOS2UNIX) z3/examples/maxsat/maxsat.c
+ @cp maxsat/README-$(PLATFORM).txt z3/examples/maxsat/README
+ @$(DOS2UNIX) z3/examples/maxsat/README
+ @cp maxsat/build-external-$(PLATFORM).sh z3/examples/maxsat/build.sh
+ @cp maxsat/build-static-$(PLATFORM).sh z3/examples/maxsat/build-static.sh
+ @$(DOS2UNIX) z3/examples/maxsat/build.sh
+ @chmod +rwx z3/examples/maxsat/build.sh
+ @$(DOS2UNIX) z3/examples/maxsat/build-static.sh
+ @chmod +rwx z3/examples/maxsat/build-static.sh
+ @cp maxsat/exec-external-$(PLATFORM).sh z3/examples/maxsat/exec.sh
+ @$(DOS2UNIX) z3/examples/maxsat/exec.sh
+ @chmod +rwx z3/examples/maxsat/exec.sh
+ @cp test_user_theory/test_user_theory.c z3/examples/theory
+ @$(DOS2UNIX) z3/examples/theory/test_user_theory.c
+ @cp test_user_theory/README-$(PLATFORM).txt z3/examples/theory/README
+ @$(DOS2UNIX) z3/examples/theory/README
+ @cp test_user_theory/build-external-$(PLATFORM).sh z3/examples/theory/build.sh
+ @cp test_user_theory/build-static-$(PLATFORM).sh z3/examples/theory/build-static.sh
+ @$(DOS2UNIX) z3/examples/theory/build.sh
+ @chmod +rwx z3/examples/theory/build.sh
+ @$(DOS2UNIX) z3/examples/theory/build-static.sh
+ @chmod +rwx z3/examples/theory/build-static.sh
+ @cp test_user_theory/exec-external-$(PLATFORM).sh z3/examples/theory/exec.sh
+ @$(DOS2UNIX) z3/examples/theory/exec.sh
+ @chmod +rwx z3/examples/theory/exec.sh
+ @cp ml_release/exec-$(PLATFORM).sh z3/examples/ocaml/exec.sh
+ @$(DOS2UNIX) z3/examples/ocaml/exec.sh
+ @chmod +rwx z3/examples/ocaml/exec.sh
+ @cp ml/test_mlapi.ml z3/examples/ocaml
+ @$(DOS2UNIX) z3/examples/ocaml/test_mlapi.ml
+ @cp c++/z3++.h z3/include
+ @cp c++/example.cpp z3/examples/c++
+ @cp c++/build-external-$(PLATFORM).sh z3/examples/c++/build.sh
+ @$(DOS2UNIX) z3/examples/c++/build.sh
+ @chmod +rwx z3/examples/c++/build.sh
+ @cp c++/exec-external-$(PLATFORM).sh z3/examples/c++/exec.sh
+ @$(DOS2UNIX) z3/examples/c++/exec.sh
+ @chmod +rwx z3/examples/c++/exec.sh
+ @cp python/z3.py z3/python
+ @cp python/z3core.py z3/python
+ @cp python/z3types.py z3/python
+ @cp python/z3consts.py z3/python
+ @cp python/z3tactics.py z3/python
+ @cp python/z3printer.py z3/python
+ @cp python/README-$(PLATFORM).txt z3/examples/python/README
+ @cp python/exec-$(PLATFORM).sh z3/examples/python/exec.sh
+ @cp python/example.py z3/examples/python
+ @$(DOS2UNIX) z3/python/*.py
+ @$(DOS2UNIX) z3/examples/python/*.py
+ @$(DOS2UNIX) z3/examples/python/*.sh
+ @chmod +rwx z3/examples/python/*.sh
+ @$(DOS2UNIX) iZ3/pack-iz3-$(PLATFORM).sh
+ @chmod +rwx iZ3/pack-iz3-$(PLATFORM).sh
+ @iZ3/pack-iz3-$(PLATFORM).sh
+ @tar -cvzf z3.tar.gz z3
+
+################################
+#
+# Support
+#
+################################
+
+Makefile: Makefile.in config.status
+ ./config.status
+ make
+
+config.status: configure
+ ./config.status --recheck
+
+################################
+#
+# checkgmake
+#
+################################
+.PHONY: checkgmake
+
+checkgmake:
+ @ ./gmaketest --make=$(MAKE) || \
+ (echo "Z3 needs GNU-Make to be built"; exit 1)
+
diff --git a/Microsoft.Z3/AST.cs b/Microsoft.Z3/AST.cs
new file mode 100644
index 000000000..e3b8fc3ec
--- /dev/null
+++ b/Microsoft.Z3/AST.cs
@@ -0,0 +1,260 @@
+/*++
+Copyright (c) 2012 Microsoft Corporation
+
+Module Name:
+
+ AST.cs
+
+Abstract:
+
+ Z3 Managed API: ASTs
+
+Author:
+
+ Christoph Wintersteiger (cwinter) 2012-03-16
+
+Notes:
+
+--*/
+
+using System;
+using System.Collections;
+using System.Collections.Generic;
+using System.Diagnostics.Contracts;
+
+namespace Microsoft.Z3
+{
+ ///
+ /// The abstract syntax tree (AST) class.
+ ///
+ [ContractVerification(true)]
+ public class AST : Z3Object, IComparable
+ {
+ ///
+ /// Comparison operator.
+ ///
+ /// An AST
+ /// An AST
+ /// True if and are from the same context
+ /// and represent the same sort; false otherwise.
+ public static bool operator ==(AST a, AST b)
+ {
+ return Object.ReferenceEquals(a, b) ||
+ (!Object.ReferenceEquals(a, null) &&
+ !Object.ReferenceEquals(b, null) &&
+ a.Context.nCtx == b.Context.nCtx &&
+ Native.Z3_is_eq_ast(a.Context.nCtx, a.NativeObject, b.NativeObject) != 0);
+ }
+
+ ///
+ /// Comparison operator.
+ ///
+ /// An AST
+ /// An AST
+ /// True if and are not from the same context
+ /// or represent different sorts; false otherwise.
+ public static bool operator !=(AST a, AST b)
+ {
+ return !(a == b);
+ }
+
+ ///
+ /// Object comparison.
+ ///
+ public override bool Equals(object o)
+ {
+ AST casted = o as AST;
+ if (casted == null) return false;
+ return this == casted;
+ }
+
+ ///
+ /// Object Comparison.
+ ///
+ /// Another AST
+ /// Negative if the object should be sorted before , positive if after else zero.
+ public virtual int CompareTo(object other)
+ {
+ if (other == null) return 1;
+ AST oAST = other as AST;
+ if (oAST == null)
+ return 1;
+ else
+ {
+ if (Id < oAST.Id)
+ return -1;
+ else if (Id > oAST.Id)
+ return +1;
+ else
+ return 0;
+ }
+ }
+
+ ///
+ /// The AST's hash code.
+ ///
+ /// A hash code
+ public override int GetHashCode()
+ {
+ return (int)Native.Z3_get_ast_hash(Context.nCtx, NativeObject);
+ }
+
+ ///
+ /// A unique identifier for the AST (unique among all ASTs).
+ ///
+ public uint Id
+ {
+ get { return Native.Z3_get_ast_id(Context.nCtx, NativeObject); }
+ }
+
+ ///
+ /// Translates (copies) the AST to the Context .
+ ///
+ /// A context
+ /// A copy of the AST which is associated with
+ public AST Translate(Context ctx)
+ {
+ Contract.Requires(ctx != null);
+ Contract.Ensures(Contract.Result() != null);
+
+ if (ReferenceEquals(Context, ctx))
+ return this;
+ else
+ return new AST(ctx, Native.Z3_translate(Context.nCtx, NativeObject, ctx.nCtx));
+ }
+
+ ///
+ /// The kind of the AST.
+ ///
+ public Z3_ast_kind ASTKind
+ {
+ get { return (Z3_ast_kind)Native.Z3_get_ast_kind(Context.nCtx, NativeObject); }
+ }
+
+ ///
+ /// Indicates whether the AST is an Expr
+ ///
+ public bool IsExpr
+ {
+ get
+ {
+ switch (ASTKind)
+ {
+ case Z3_ast_kind.Z3_APP_AST:
+ case Z3_ast_kind.Z3_NUMERAL_AST:
+ case Z3_ast_kind.Z3_QUANTIFIER_AST:
+ case Z3_ast_kind.Z3_VAR_AST: return true;
+ default: return false;
+ }
+ }
+ }
+
+ ///
+ /// Indicates whether the AST is a BoundVariable
+ ///
+ public bool IsVar
+ {
+ get { return this.ASTKind == Z3_ast_kind.Z3_VAR_AST; }
+ }
+
+ ///
+ /// Indicates whether the AST is a Quantifier
+ ///
+ public bool IsQuantifier
+ {
+ get { return this.ASTKind == Z3_ast_kind.Z3_QUANTIFIER_AST; }
+ }
+
+ ///
+ /// Indicates whether the AST is a Sort
+ ///
+ public bool IsSort
+ {
+ get { return this.ASTKind == Z3_ast_kind.Z3_SORT_AST; }
+ }
+
+ ///
+ /// Indicates whether the AST is a FunctionDeclaration
+ ///
+ public bool IsFuncDecl
+ {
+ get { return this.ASTKind == Z3_ast_kind.Z3_FUNC_DECL_AST; }
+ }
+
+ ///
+ /// A string representation of the AST.
+ ///
+ public override string ToString()
+ {
+ return Native.Z3_ast_to_string(Context.nCtx, NativeObject);
+ }
+
+ ///
+ /// A string representation of the AST in s-expression notation.
+ ///
+ public string SExpr()
+ {
+ Contract.Ensures(Contract.Result() != null);
+
+ return Native.Z3_ast_to_string(Context.nCtx, NativeObject);
+ }
+
+ #region Internal
+ internal AST(Context ctx) : base(ctx) { Contract.Requires(ctx != null); }
+ internal AST(Context ctx, IntPtr obj) : base(ctx, obj) { Contract.Requires(ctx != null); }
+
+ internal class DecRefQueue : Z3.DecRefQueue
+ {
+ public override void IncRef(Context ctx, IntPtr obj)
+ {
+ Native.Z3_inc_ref(ctx.nCtx, obj);
+ }
+
+ public override void DecRef(Context ctx, IntPtr obj)
+ {
+ Native.Z3_dec_ref(ctx.nCtx, obj);
+ }
+ };
+
+ internal override void IncRef(IntPtr o)
+ {
+ // Console.WriteLine("AST IncRef()");
+ if (Context == null)
+ throw new Z3Exception("inc() called on null context");
+ if (o == IntPtr.Zero)
+ throw new Z3Exception("inc() called on null AST");
+ Context.AST_DRQ.IncAndClear(Context, o);
+ base.IncRef(o);
+ }
+
+ internal override void DecRef(IntPtr o)
+ {
+ // Console.WriteLine("AST DecRef()");
+ if (Context == null)
+ throw new Z3Exception("dec() called on null context");
+ if (o == IntPtr.Zero)
+ throw new Z3Exception("dec() called on null AST");
+ Context.AST_DRQ.Add(o);
+ base.DecRef(o);
+ }
+
+ internal static AST Create(Context ctx, IntPtr obj)
+ {
+ Contract.Requires(ctx != null);
+ Contract.Ensures(Contract.Result() != null);
+
+ switch ((Z3_ast_kind)Native.Z3_get_ast_kind(ctx.nCtx, obj))
+ {
+ case Z3_ast_kind.Z3_FUNC_DECL_AST: return new FuncDecl(ctx, obj);
+ case Z3_ast_kind.Z3_QUANTIFIER_AST: return new Quantifier(ctx, obj);
+ case Z3_ast_kind.Z3_SORT_AST: return Sort.Create(ctx, obj);
+ case Z3_ast_kind.Z3_APP_AST:
+ case Z3_ast_kind.Z3_NUMERAL_AST:
+ case Z3_ast_kind.Z3_VAR_AST: return Expr.Create(ctx, obj);
+ default:
+ throw new Z3Exception("Unknown AST kind");
+ }
+ }
+ #endregion
+ }
+}
diff --git a/Microsoft.Z3/ASTMap.cs b/Microsoft.Z3/ASTMap.cs
new file mode 100644
index 000000000..d945b3d44
--- /dev/null
+++ b/Microsoft.Z3/ASTMap.cs
@@ -0,0 +1,155 @@
+/*++
+Copyright (c) 2012 Microsoft Corporation
+
+Module Name:
+
+ ASTMap.cs
+
+Abstract:
+
+ Z3 Managed API: AST Maps
+
+Author:
+
+ Christoph Wintersteiger (cwinter) 2012-03-21
+
+Notes:
+
+--*/
+
+using System;
+using System.Diagnostics.Contracts;
+
+namespace Microsoft.Z3
+{
+ ///
+ /// Map from AST to AST
+ ///
+ [ContractVerification(true)]
+ internal class ASTMap : Z3Object
+ {
+ ///
+ /// Checks whether the map contains the key .
+ ///
+ /// An AST
+ /// True if is a key in the map, false otherwise.
+ public bool Contains(AST k)
+ {
+ Contract.Requires(k != null);
+
+ return Native.Z3_ast_map_contains(Context.nCtx, NativeObject, k.NativeObject) != 0;
+ }
+
+ ///
+ /// Finds the value associated with the key .
+ ///
+ ///
+ /// This function signs an error when is not a key in the map.
+ ///
+ /// An AST
+ public AST Find(AST k)
+ {
+ Contract.Requires(k != null);
+ Contract.Ensures(Contract.Result() != null);
+
+ return new AST(Context, Native.Z3_ast_map_find(Context.nCtx, NativeObject, k.NativeObject));
+ }
+
+ ///
+ /// Stores or replaces a new key/value pair in the map.
+ ///
+ /// The key AST
+ /// The value AST
+ public void Insert(AST k, AST v)
+ {
+ Contract.Requires(k != null);
+ Contract.Requires(v != null);
+
+ Native.Z3_ast_map_insert(Context.nCtx, NativeObject, k.NativeObject, v.NativeObject);
+ }
+
+ ///
+ /// Erases the key from the map.
+ ///
+ /// An AST
+ public void Erase(AST k)
+ {
+ Contract.Requires(k != null);
+
+ Native.Z3_ast_map_erase(Context.nCtx, NativeObject, k.NativeObject);
+ }
+
+ ///
+ /// Removes all keys from the map.
+ ///
+ public void Reset()
+ {
+ Native.Z3_ast_map_reset(Context.nCtx, NativeObject);
+ }
+
+ ///
+ /// The size of the map
+ ///
+ public uint Size
+ {
+ get { return Native.Z3_ast_map_size(Context.nCtx, NativeObject); }
+ }
+
+ ///
+ /// The keys stored in the map.
+ ///
+ public ASTVector Keys
+ {
+ get
+ {
+ return new ASTVector(Context, Native.Z3_ast_map_keys(Context.nCtx, NativeObject));
+ }
+ }
+
+ ///
+ /// Retrieves a string representation of the map.
+ ///
+ public override string ToString()
+ {
+ return Native.Z3_ast_map_to_string(Context.nCtx, NativeObject);
+ }
+
+ #region Internal
+ internal ASTMap(Context ctx, IntPtr obj)
+ : base(ctx, obj)
+ {
+ Contract.Requires(ctx != null);
+ }
+ internal ASTMap(Context ctx)
+ : base(ctx, Native.Z3_mk_ast_map(ctx.nCtx))
+ {
+ Contract.Requires(ctx != null);
+ }
+
+ internal class DecRefQueue : Z3.DecRefQueue
+ {
+ public override void IncRef(Context ctx, IntPtr obj)
+ {
+ Native.Z3_ast_map_inc_ref(ctx.nCtx, obj);
+ }
+
+ public override void DecRef(Context ctx, IntPtr obj)
+ {
+ Native.Z3_ast_map_dec_ref(ctx.nCtx, obj);
+ }
+ };
+
+ internal override void IncRef(IntPtr o)
+ {
+ Context.ASTMap_DRQ.IncAndClear(Context, o);
+ base.IncRef(o);
+ }
+
+ internal override void DecRef(IntPtr o)
+ {
+ Context.ASTMap_DRQ.Add(o);
+ base.DecRef(o);
+ }
+ #endregion
+ }
+}
diff --git a/Microsoft.Z3/ASTVector.cs b/Microsoft.Z3/ASTVector.cs
new file mode 100644
index 000000000..1e66c4b21
--- /dev/null
+++ b/Microsoft.Z3/ASTVector.cs
@@ -0,0 +1,132 @@
+/*++
+Copyright (c) 2012 Microsoft Corporation
+
+Module Name:
+
+ ASTVector.cs
+
+Abstract:
+
+ Z3 Managed API: AST Vectors
+
+Author:
+
+ Christoph Wintersteiger (cwinter) 2012-03-21
+
+Notes:
+
+--*/
+
+using System;
+using System.Diagnostics.Contracts;
+
+namespace Microsoft.Z3
+{
+ ///
+ /// Vectors of ASTs.
+ ///
+ internal class ASTVector : Z3Object
+ {
+ ///
+ /// The size of the vector
+ ///
+ public uint Size
+ {
+ get { return Native.Z3_ast_vector_size(Context.nCtx, NativeObject); }
+ }
+
+ ///
+ /// Retrieves the i-th object in the vector.
+ ///
+ /// May throw an IndexOutOfBoundsException when is out of range.
+ /// Index
+ /// An AST
+ public AST this[uint i]
+ {
+ get
+ {
+ Contract.Ensures(Contract.Result() != null);
+
+ return new AST(Context, Native.Z3_ast_vector_get(Context.nCtx, NativeObject, i));
+ }
+ set
+ {
+ Contract.Requires(value!= null);
+
+ Native.Z3_ast_vector_set(Context.nCtx, NativeObject, i, value.NativeObject);
+ }
+ }
+
+ ///
+ /// Resize the vector to .
+ ///
+ /// The new size of the vector.
+ public void Resize(uint newSize)
+ {
+ Native.Z3_ast_vector_resize(Context.nCtx, NativeObject, newSize);
+ }
+
+ ///
+ /// Add the AST to the back of the vector. The size
+ /// is increased by 1.
+ ///
+ /// An AST
+ public void Push(AST a)
+ {
+ Contract.Requires(a != null);
+
+ Native.Z3_ast_vector_push(Context.nCtx, NativeObject, a.NativeObject);
+ }
+
+ ///
+ /// Translates all ASTs in the vector to .
+ ///
+ /// A context
+ /// A new ASTVector
+ public ASTVector Translate(Context ctx)
+ {
+ Contract.Requires(ctx != null);
+ Contract.Ensures(Contract.Result() != null);
+
+ return new ASTVector(Context, Native.Z3_ast_vector_translate(Context.nCtx, NativeObject, ctx.nCtx));
+ }
+
+ ///
+ /// Retrieves a string representation of the vector.
+ ///
+ public override string ToString()
+ {
+ return Native.Z3_ast_vector_to_string(Context.nCtx, NativeObject);
+ }
+
+ #region Internal
+ internal ASTVector(Context ctx, IntPtr obj) : base(ctx, obj) { Contract.Requires(ctx != null); }
+ internal ASTVector(Context ctx) : base(ctx, Native.Z3_mk_ast_vector(ctx.nCtx)) { Contract.Requires(ctx != null); }
+
+ internal class DecRefQueue : Z3.DecRefQueue
+ {
+ public override void IncRef(Context ctx, IntPtr obj)
+ {
+ Native.Z3_ast_vector_inc_ref(ctx.nCtx, obj);
+ }
+
+ public override void DecRef(Context ctx, IntPtr obj)
+ {
+ Native.Z3_ast_vector_dec_ref(ctx.nCtx, obj);
+ }
+ };
+
+ internal override void IncRef(IntPtr o)
+ {
+ Context.ASTVector_DRQ.IncAndClear(Context, o);
+ base.IncRef(o);
+ }
+
+ internal override void DecRef(IntPtr o)
+ {
+ Context.ASTVector_DRQ.Add(o);
+ base.DecRef(o);
+ }
+ #endregion
+ }
+}
diff --git a/Microsoft.Z3/ApplyResult.cs b/Microsoft.Z3/ApplyResult.cs
new file mode 100644
index 000000000..21a515643
--- /dev/null
+++ b/Microsoft.Z3/ApplyResult.cs
@@ -0,0 +1,111 @@
+/*++
+Copyright (c) 2012 Microsoft Corporation
+
+Module Name:
+
+ ApplyResult.cs
+
+Abstract:
+
+ Z3 Managed API: Result object for tactic applications
+
+Author:
+
+ Christoph Wintersteiger (cwinter) 2012-03-21
+
+Notes:
+
+--*/
+
+using System;
+using System.Diagnostics.Contracts;
+
+namespace Microsoft.Z3
+{
+ ///
+ /// ApplyResult objects represent the result of an application of a
+ /// tactic to a goal. It contains the subgoals that were produced.
+ ///
+ [ContractVerification(true)]
+ public class ApplyResult : Z3Object
+ {
+ ///
+ /// The number of Subgoals.
+ ///
+ public uint NumSubgoals
+ {
+ get { return Native.Z3_apply_result_get_num_subgoals(Context.nCtx, NativeObject); }
+ }
+
+ ///
+ /// Retrieves the subgoals from the ApplyResult.
+ ///
+ public Goal[] Subgoals
+ {
+ get
+ {
+ Contract.Ensures(Contract.Result() != null);
+ Contract.Ensures(Contract.Result().Length == this.NumSubgoals);
+
+ uint n = NumSubgoals;
+ Goal[] res = new Goal[n];
+ for (uint i = 0; i < n; i++)
+ res[i] = new Goal(Context, Native.Z3_apply_result_get_subgoal(Context.nCtx, NativeObject, i));
+ return res;
+ }
+ }
+
+ ///
+ /// Convert a model for the subgoal into a model for the original
+ /// goal g, that the ApplyResult was obtained from.
+ ///
+ /// A model for g
+ public Model ConvertModel(uint i, Model m)
+ {
+ Contract.Requires(m != null);
+ Contract.Ensures(Contract.Result() != null);
+
+ return new Model(Context, Native.Z3_apply_result_convert_model(Context.nCtx, NativeObject, i, m.NativeObject));
+ }
+
+ ///
+ /// A string representation of the ApplyResult.
+ ///
+ public override string ToString()
+ {
+ return Native.Z3_apply_result_to_string(Context.nCtx, NativeObject);
+ }
+
+ #region Internal
+ internal ApplyResult(Context ctx, IntPtr obj) : base(ctx, obj)
+ {
+ Contract.Requires(ctx != null);
+ }
+
+ internal class DecRefQueue : Z3.DecRefQueue
+ {
+ public override void IncRef(Context ctx, IntPtr obj)
+ {
+ Native.Z3_apply_result_inc_ref(ctx.nCtx, obj);
+ }
+
+ public override void DecRef(Context ctx, IntPtr obj)
+ {
+ Native.Z3_apply_result_dec_ref(ctx.nCtx, obj);
+ }
+ };
+
+ internal override void IncRef(IntPtr o)
+ {
+ Context.ApplyResult_DRQ.IncAndClear(Context, o);
+ base.IncRef(o);
+ }
+
+ internal override void DecRef(IntPtr o)
+ {
+ Context.ApplyResult_DRQ.Add(o);
+ base.DecRef(o);
+ }
+ #endregion
+ }
+}
diff --git a/Microsoft.Z3/Constructor.cs b/Microsoft.Z3/Constructor.cs
new file mode 100644
index 000000000..403d18736
--- /dev/null
+++ b/Microsoft.Z3/Constructor.cs
@@ -0,0 +1,170 @@
+/*++
+Copyright (c) 2012 Microsoft Corporation
+
+Module Name:
+
+ Constructor.cs
+
+Abstract:
+
+ Z3 Managed API: Constructors
+
+Author:
+
+ Christoph Wintersteiger (cwinter) 2012-03-22
+
+Notes:
+
+--*/
+
+using System;
+using System.Diagnostics.Contracts;
+
+namespace Microsoft.Z3
+{
+ ///
+ /// Constructors are used for datatype sorts.
+ ///
+ [ContractVerification(true)]
+ public class Constructor : Z3Object
+ {
+ ///
+ /// The number of fields of the constructor.
+ ///
+ public uint NumFields
+ {
+ get { init(); return n; }
+ }
+
+ ///
+ /// The function declaration of the constructor.
+ ///
+ public FuncDecl ConstructorDecl
+ {
+ get {
+ Contract.Ensures(Contract.Result() != null);
+ init(); return m_constructorDecl; }
+ }
+
+ ///
+ /// The function declaration of the tester.
+ ///
+ public FuncDecl TesterDecl
+ {
+ get {
+ Contract.Ensures(Contract.Result() != null);
+ init(); return m_testerDecl; }
+ }
+
+ ///
+ /// The function declarations of the accessors
+ ///
+ public FuncDecl[] AccessorDecls
+ {
+ get {
+ Contract.Ensures(Contract.Result() != null);
+ init(); return m_accessorDecls; }
+ }
+
+ ///
+ /// Destructor.
+ ///
+ ~Constructor()
+ {
+ Native.Z3_del_constructor(Context.nCtx, NativeObject);
+ }
+
+ #region Object invariant
+
+ [ContractInvariantMethod]
+ private void ObjectInvariant()
+ {
+ Contract.Invariant(m_testerDecl == null || m_constructorDecl != null);
+ Contract.Invariant(m_testerDecl == null || m_accessorDecls != null);
+ }
+
+ #endregion
+
+ #region Internal
+ readonly private uint n = 0;
+ private FuncDecl m_testerDecl = null;
+ private FuncDecl m_constructorDecl = null;
+ private FuncDecl[] m_accessorDecls = null;
+
+ internal Constructor(Context ctx, Symbol name, Symbol recognizer, Symbol[] fieldNames,
+ Sort[] sorts, uint[] sortRefs)
+ : base(ctx)
+ {
+ Contract.Requires(ctx != null);
+ Contract.Requires(name != null);
+ Contract.Requires(recognizer != null);
+
+ n = AST.ArrayLength(fieldNames);
+
+ if (n != AST.ArrayLength(sorts))
+ throw new Z3Exception("Number of field names does not match number of sorts");
+ if (sortRefs != null && sortRefs.Length != n)
+ throw new Z3Exception("Number of field names does not match number of sort refs");
+
+ if (sortRefs == null) sortRefs = new uint[n];
+
+ NativeObject = Native.Z3_mk_constructor(ctx.nCtx, name.NativeObject, recognizer.NativeObject,
+ n,
+ Symbol.ArrayToNative(fieldNames),
+ Sort.ArrayToNative(sorts),
+ sortRefs);
+
+ }
+
+ private void init()
+ {
+ Contract.Ensures(m_constructorDecl != null);
+ Contract.Ensures(m_testerDecl != null);
+ Contract.Ensures(m_accessorDecls != null);
+
+ if (m_testerDecl != null) return;
+ IntPtr constructor = IntPtr.Zero;
+ IntPtr tester = IntPtr.Zero;
+ IntPtr[] accessors = new IntPtr[n];
+ Native.Z3_query_constructor(Context.nCtx, NativeObject, n, ref constructor, ref tester, accessors);
+ m_constructorDecl = new FuncDecl(Context, constructor);
+ m_testerDecl = new FuncDecl(Context, tester);
+ m_accessorDecls = new FuncDecl[n];
+ for (uint i = 0; i < n; i++)
+ m_accessorDecls[i] = new FuncDecl(Context, accessors[i]);
+ }
+
+ #endregion
+ }
+
+ ///
+ /// Lists of constructors
+ ///
+ public class ConstructorList : Z3Object
+ {
+ ///
+ /// Destructor.
+ ///
+ ~ConstructorList()
+ {
+ Native.Z3_del_constructor_list(Context.nCtx, NativeObject);
+ }
+
+ #region Internal
+ internal ConstructorList(Context ctx, IntPtr obj)
+ : base(ctx, obj)
+ {
+ Contract.Requires(ctx != null);
+ }
+
+ internal ConstructorList(Context ctx, Constructor[] constructors)
+ : base(ctx)
+ {
+ Contract.Requires(ctx != null);
+ Contract.Requires(constructors != null);
+
+ NativeObject = Native.Z3_mk_constructor_list(Context.nCtx, (uint)constructors.Length, Constructor.ArrayToNative(constructors));
+ }
+ #endregion
+ }
+}
diff --git a/Microsoft.Z3/Context.cs b/Microsoft.Z3/Context.cs
new file mode 100644
index 000000000..597b9b7c6
--- /dev/null
+++ b/Microsoft.Z3/Context.cs
@@ -0,0 +1,3694 @@
+/*++
+Copyright (c) 2012 Microsoft Corporation
+
+Module Name:
+
+ Context.cs
+
+Abstract:
+
+ Z3 Managed API: Context
+
+Author:
+
+ Christoph Wintersteiger (cwinter) 2012-03-15
+
+Notes:
+
+--*/
+
+using System;
+using System.Collections.Generic;
+using System.Runtime.InteropServices;
+using System.Diagnostics.Contracts;
+
+namespace Microsoft.Z3
+{
+ ///
+ /// The main interaction with Z3 happens via the Context.
+ ///
+ [ContractVerification(true)]
+ public class Context : IDisposable
+ {
+ #region Constructors
+ ///
+ /// Constructor.
+ ///
+ public Context()
+ : base()
+ {
+ m_ctx = Native.Z3_mk_context_rc(IntPtr.Zero);
+ InitContext();
+ }
+
+ ///
+ /// Constructor.
+ ///
+ public Context(Dictionary settings)
+ : base()
+ {
+ Contract.Requires(settings != null);
+
+ IntPtr cfg = Native.Z3_mk_config();
+ foreach(KeyValuePair kv in settings)
+ Native.Z3_set_param_value(cfg, kv.Key, kv.Value);
+ m_ctx = Native.Z3_mk_context_rc(cfg);
+ Native.Z3_del_config(cfg);
+ InitContext();
+ }
+ #endregion
+
+ #region Symbols
+ ///
+ /// Creates a new symbol using an integer.
+ ///
+ ///
+ /// Not all integers can be passed to this function.
+ /// The legal range of unsigned integers is 0 to 2^30-1.
+ ///
+ public IntSymbol MkSymbol(int i)
+ {
+ Contract.Ensures(Contract.Result() != null);
+
+ return new IntSymbol(this, i);
+ }
+
+ ///
+ /// Create a symbol using a string.
+ ///
+ public StringSymbol MkSymbol(string name)
+ {
+ Contract.Ensures(Contract.Result() != null);
+
+ return new StringSymbol(this, name);
+ }
+
+ ///
+ /// Create an array of symbols.
+ ///
+ internal Symbol[] MkSymbols(string[] names)
+ {
+ Contract.Ensures(names == null || Contract.Result() != null);
+ Contract.Ensures(names != null || Contract.Result() == null);
+ Contract.Ensures(Contract.Result() == null || Contract.Result().Length == names.Length);
+ Contract.Ensures(Contract.Result() == null || Contract.ForAll(Contract.Result(), s => s != null));
+
+ if (names == null) return null;
+ Symbol[] result = new Symbol[names.Length];
+ for (int i = 0; i < names.Length; ++i) result[i] = MkSymbol(names[i]);
+ return result;
+ }
+ #endregion
+
+ #region Sorts
+ private BoolSort m_boolSort = null;
+ private IntSort m_intSort = null;
+ private RealSort m_realSort = null;
+
+ ///
+ /// Retrieves the Boolean sort of the context.
+ ///
+ public BoolSort BoolSort
+ {
+ get
+ {
+ Contract.Ensures(Contract.Result() != null);
+
+ if (m_boolSort == null) m_boolSort = new BoolSort(this); return m_boolSort;
+ }
+ }
+
+ ///
+ /// Retrieves the Integer sort of the context.
+ ///
+ public IntSort IntSort
+ {
+ get
+ {
+ Contract.Ensures(Contract.Result() != null);
+ if (m_intSort == null) m_intSort = new IntSort(this); return m_intSort;
+ }
+ }
+
+
+ ///
+ /// Retrieves the Real sort of the context.
+ ///
+ public RealSort RealSort { get { Contract.Ensures(Contract.Result() != null); if (m_realSort == null) m_realSort = new RealSort(this); return m_realSort; } }
+
+ ///
+ /// Create a new Boolean sort.
+ ///
+ public BoolSort MkBoolSort()
+ {
+ Contract.Ensures(Contract.Result() != null);
+ return new BoolSort(this);
+ }
+
+ ///
+ /// Create a new uninterpreted sort.
+ ///
+ public UninterpretedSort MkUninterpretedSort(Symbol s)
+ {
+ Contract.Requires(s != null);
+ Contract.Ensures(Contract.Result() != null);
+
+ CheckContextMatch(s);
+ return new UninterpretedSort(this, s);
+ }
+
+ ///
+ /// Create a new uninterpreted sort.
+ ///
+ public UninterpretedSort MkUninterpretedSort(string str)
+ {
+ Contract.Ensures(Contract.Result() != null);
+
+ return MkUninterpretedSort(MkSymbol(str));
+ }
+
+ ///
+ /// Create a new integer sort.
+ ///
+ public IntSort MkIntSort()
+ {
+ Contract.Ensures(Contract.Result() != null);
+
+ return new IntSort(this);
+ }
+
+ ///
+ /// Create a real sort.
+ ///
+ public RealSort MkRealSort()
+ {
+ Contract.Ensures(Contract.Result() != null);
+ return new RealSort(this);
+ }
+
+ ///
+ /// Create a new bit-vector sort.
+ ///
+ public BitVecSort MkBitVecSort(uint size)
+ {
+ Contract.Ensures(Contract.Result() != null);
+
+ return new BitVecSort(this, size);
+ }
+
+ ///
+ /// Create a new array sort.
+ ///
+ public ArraySort MkArraySort(Sort domain, Sort range)
+ {
+ Contract.Requires(domain != null);
+ Contract.Requires(range != null);
+ Contract.Ensures(Contract.Result() != null);
+
+ CheckContextMatch(domain);
+ CheckContextMatch(range);
+ return new ArraySort(this, domain, range);
+ }
+
+ ///
+ /// Create a new tuple sort.
+ ///
+ public TupleSort MkTupleSort(Symbol name, Symbol[] fieldNames, Sort[] fieldSorts)
+ {
+ Contract.Requires(name != null);
+ Contract.Requires(fieldNames != null);
+ Contract.Requires(Contract.ForAll(fieldNames, fn => fn != null));
+ Contract.Requires(fieldSorts == null || Contract.ForAll(fieldSorts, fs => fs != null));
+ Contract.Ensures(Contract.Result() != null);
+
+ CheckContextMatch(name);
+ CheckContextMatch(fieldNames);
+ CheckContextMatch(fieldSorts);
+ return new TupleSort(this, name, (uint)fieldNames.Length, fieldNames, fieldSorts);
+ }
+
+ ///
+ /// Create a new enumeration sort.
+ ///
+ public EnumSort MkEnumSort(Symbol name, Symbol[] enumNames)
+ {
+ Contract.Requires(name != null);
+ Contract.Requires(enumNames != null);
+ Contract.Requires(Contract.ForAll(enumNames, f => f != null));
+
+ Contract.Ensures(Contract.Result() != null);
+
+ CheckContextMatch(name);
+ CheckContextMatch(enumNames);
+ return new EnumSort(this, name, enumNames);
+ }
+
+ ///
+ /// Create a new enumeration sort.
+ ///
+ public EnumSort MkEnumSort(string name, string[] enumNames)
+ {
+ Contract.Requires(enumNames != null);
+ Contract.Ensures(Contract.Result() != null);
+
+ return new EnumSort(this, MkSymbol(name), MkSymbols(enumNames));
+ }
+
+ ///
+ /// Create a new list sort.
+ ///
+ public ListSort MkListSort(Symbol name, Sort elemSort)
+ {
+ Contract.Requires(name != null);
+ Contract.Requires(elemSort != null);
+ Contract.Ensures(Contract.Result() != null);
+
+ CheckContextMatch(name);
+ CheckContextMatch(elemSort);
+ return new ListSort(this, name, elemSort);
+ }
+
+ ///
+ /// Create a new list sort.
+ ///
+ public ListSort MkListSort(string name, Sort elemSort)
+ {
+ Contract.Requires(elemSort != null);
+ Contract.Ensures(Contract.Result() != null);
+
+ CheckContextMatch(elemSort);
+ return new ListSort(this, MkSymbol(name), elemSort);
+ }
+
+ ///
+ /// Create a new finite domain sort.
+ ///
+ public FiniteDomainSort MkFiniteDomainSort(Symbol name, ulong size)
+ {
+ Contract.Requires(name != null);
+ Contract.Ensures(Contract.Result() != null);
+
+ CheckContextMatch(name);
+ return new FiniteDomainSort(this, name, size);
+ }
+
+ ///
+ /// Create a new finite domain sort.
+ ///
+ public FiniteDomainSort MkFiniteDomainSort(string name, ulong size)
+ {
+ Contract.Ensures(Contract.Result() != null);
+
+ return new FiniteDomainSort(this, MkSymbol(name), size);
+ }
+
+
+ #region Datatypes
+ ///
+ /// Create a datatype constructor.
+ ///
+ /// constructor name
+ /// name of recognizer function.
+ /// names of the constructor fields.
+ /// field sorts, 0 if the field sort refers to a recursive sort.
+ /// reference to datatype sort that is an argument to the constructor;
+ /// if the corresponding sort reference is 0, then the value in sort_refs should be an index
+ /// referring to one of the recursive datatypes that is declared.
+ public Constructor MkConstructor(Symbol name, Symbol recognizer, Symbol[] fieldNames = null, Sort[] sorts = null, uint[] sortRefs = null)
+ {
+ Contract.Requires(name != null);
+ Contract.Requires(recognizer != null);
+ Contract.Ensures(Contract.Result() != null);
+
+ return new Constructor(this, name, recognizer, fieldNames, sorts, sortRefs);
+ }
+
+ ///
+ /// Create a datatype constructor.
+ ///
+ ///
+ ///
+ ///
+ ///
+ ///
+ ///
+ public Constructor MkConstructor(string name, string recognizer, string[] fieldNames = null, Sort[] sorts = null, uint[] sortRefs = null)
+ {
+ Contract.Ensures(Contract.Result() != null);
+
+ return new Constructor(this, MkSymbol(name), MkSymbol(recognizer), MkSymbols(fieldNames), sorts, sortRefs);
+ }
+
+ ///
+ /// Create a new datatype sort.
+ ///
+ public DatatypeSort MkDatatypeSort(Symbol name, Constructor[] constructors)
+ {
+ Contract.Requires(name != null);
+ Contract.Requires(constructors != null);
+ Contract.Requires(Contract.ForAll(constructors, c => c != null));
+
+ Contract.Ensures(Contract.Result() != null);
+
+ CheckContextMatch(name);
+ CheckContextMatch(constructors);
+ return new DatatypeSort(this, name, constructors);
+ }
+
+ ///
+ /// Create a new datatype sort.
+ ///
+ public DatatypeSort MkDatatypeSort(string name, Constructor[] constructors)
+ {
+ Contract.Requires(constructors != null);
+ Contract.Requires(Contract.ForAll(constructors, c => c != null));
+ Contract.Ensures(Contract.Result() != null);
+
+ CheckContextMatch(constructors);
+ return new DatatypeSort(this, MkSymbol(name), constructors);
+ }
+
+ ///
+ /// Create mutually recursive datatypes.
+ ///
+ /// names of datatype sorts
+ /// list of constructors, one list per sort.
+ public DatatypeSort[] MkDatatypeSorts(Symbol[] names, Constructor[][] c)
+ {
+ Contract.Requires(names != null);
+ Contract.Requires(c != null);
+ Contract.Requires(names.Length == c.Length);
+ Contract.Requires(Contract.ForAll(0, c.Length, j => c[j] != null));
+ Contract.Requires(Contract.ForAll(names, name => name != null));
+ Contract.Ensures(Contract.Result() != null);
+
+ CheckContextMatch(names);
+ uint n = (uint)names.Length;
+ ConstructorList[] cla = new ConstructorList[n];
+ IntPtr[] n_constr = new IntPtr[n];
+ for (uint i = 0; i < n; i++)
+ {
+ var constructor = c[i];
+ Contract.Assume(Contract.ForAll(constructor, arr => arr != null), "Clousot does not support yet quantified formula on multidimensional arrays");
+ CheckContextMatch(constructor);
+ cla[i] = new ConstructorList(this, constructor);
+ n_constr[i] = cla[i].NativeObject;
+ }
+ IntPtr[] n_res = new IntPtr[n];
+ Native.Z3_mk_datatypes(nCtx, n, Symbol.ArrayToNative(names), n_res, n_constr);
+ DatatypeSort[] res = new DatatypeSort[n];
+ for (uint i = 0; i < n; i++)
+ res[i] = new DatatypeSort(this, n_res[i]);
+ return res;
+ }
+
+ ///
+ /// Create mutually recursive data-types.
+ ///
+ ///
+ ///
+ ///
+ public DatatypeSort[] MkDatatypeSorts(string[] names, Constructor[][] c)
+ {
+ Contract.Requires(names != null);
+ Contract.Requires(c != null);
+ Contract.Requires(names.Length == c.Length);
+ Contract.Requires(Contract.ForAll(0, c.Length, j => c[j] != null));
+ Contract.Requires(Contract.ForAll(names, name => name != null));
+ Contract.Ensures(Contract.Result() != null);
+
+ return MkDatatypeSorts(MkSymbols(names), c);
+ }
+
+ #endregion
+ #endregion
+
+ #region Function Declarations
+ ///
+ /// Creates a new function declaration.
+ ///
+ public FuncDecl MkFuncDecl(Symbol name, Sort[] domain, Sort range)
+ {
+ Contract.Requires(name != null);
+ Contract.Requires(range != null);
+ Contract.Requires(Contract.ForAll(domain, d => d != null));
+ Contract.Ensures(Contract.Result() != null);
+
+ CheckContextMatch(name);
+ CheckContextMatch(domain);
+ CheckContextMatch(range);
+ return new FuncDecl(this, name, domain, range);
+ }
+
+ ///
+ /// Creates a new function declaration.
+ ///
+ public FuncDecl MkFuncDecl(Symbol name, Sort domain, Sort range)
+ {
+ Contract.Requires(name != null);
+ Contract.Requires(domain != null);
+ Contract.Requires(range != null);
+ Contract.Ensures(Contract.Result() != null);
+
+ CheckContextMatch(name);
+ CheckContextMatch(domain);
+ CheckContextMatch(range);
+ Sort[] q = new Sort[] { domain };
+ return new FuncDecl(this, name, q, range);
+ }
+
+ ///
+ /// Creates a new function declaration.
+ ///
+ public FuncDecl MkFuncDecl(string name, Sort[] domain, Sort range)
+ {
+ Contract.Requires(range != null);
+ Contract.Requires(Contract.ForAll(domain, d => d != null));
+ Contract.Ensures(Contract.Result() != null);
+
+ CheckContextMatch(domain);
+ CheckContextMatch(range);
+ return new FuncDecl(this, MkSymbol(name), domain, range);
+ }
+
+ ///
+ /// Creates a new function declaration.
+ ///
+ public FuncDecl MkFuncDecl(string name, Sort domain, Sort range)
+ {
+ Contract.Requires(range != null);
+ Contract.Requires(domain != null);
+ Contract.Ensures(Contract.Result() != null);
+
+ CheckContextMatch(domain);
+ CheckContextMatch(range);
+ Sort[] q = new Sort[] { domain };
+ return new FuncDecl(this, MkSymbol(name), q, range);
+ }
+
+ ///
+ /// Creates a fresh function declaration with a name prefixed with .
+ ///
+ ///
+ ///
+ public FuncDecl MkFreshFuncDecl(string prefix, Sort[] domain, Sort range)
+ {
+ Contract.Requires(range != null);
+ Contract.Requires(Contract.ForAll(domain, d => d != null));
+ Contract.Ensures(Contract.Result() != null);
+
+ CheckContextMatch(domain);
+ CheckContextMatch(range);
+ return new FuncDecl(this, prefix, domain, range);
+ }
+
+ ///
+ /// Creates a new constant function declaration.
+ ///
+ public FuncDecl MkConstDecl(Symbol name, Sort range)
+ {
+ Contract.Requires(name != null);
+ Contract.Requires(range != null);
+ Contract.Ensures(Contract.Result() != null);
+
+ CheckContextMatch(name);
+ CheckContextMatch(range);
+ return new FuncDecl(this, name, null, range);
+ }
+
+ ///
+ /// Creates a new constant function declaration.
+ ///
+ public FuncDecl MkConstDecl(string name, Sort range)
+ {
+ Contract.Requires(range != null);
+ Contract.Ensures(Contract.Result() != null);
+
+ CheckContextMatch(range);
+ return new FuncDecl(this, MkSymbol(name), null, range);
+ }
+
+ ///
+ /// Creates a fresh constant function declaration with a name prefixed with .
+ ///
+ ///
+ ///
+ public FuncDecl MkFreshConstDecl(string prefix, Sort range)
+ {
+ Contract.Requires(range != null);
+ Contract.Ensures(Contract.Result() != null);
+
+ CheckContextMatch(range);
+ return new FuncDecl(this, prefix, null, range);
+ }
+ #endregion
+
+ #region Bound Variables
+ ///
+ /// Creates a new bound variable.
+ ///
+ /// The de-Bruijn index of the variable
+ /// The sort of the variable
+ public Expr MkBound(uint index, Sort ty)
+ {
+ Contract.Requires(ty != null);
+ Contract.Ensures(Contract.Result() != null);
+
+ return Expr.Create(this, Native.Z3_mk_bound(nCtx, index, ty.NativeObject));
+ }
+ #endregion
+
+ #region Quantifier Patterns
+ ///
+ /// Create a quantifier pattern.
+ ///
+ public Pattern MkPattern(params Expr[] terms)
+ {
+ Contract.Requires(terms != null);
+ if (terms.Length == 0)
+ throw new Z3Exception("Cannot create a pattern from zero terms");
+
+ Contract.Ensures(Contract.Result() != null);
+
+ Contract.EndContractBlock();
+
+ IntPtr[] termsNative = AST.ArrayToNative(terms);
+ return new Pattern(this, Native.Z3_mk_pattern(nCtx, (uint)terms.Length, termsNative));
+ }
+ #endregion
+
+ #region Constants
+ ///
+ /// Creates a new Constant of sort and named .
+ ///
+ public Expr MkConst(Symbol name, Sort range)
+ {
+ Contract.Requires(name != null);
+ Contract.Requires(range != null);
+ Contract.Ensures(Contract.Result() != null);
+
+ CheckContextMatch(name);
+ CheckContextMatch(range);
+
+ return Expr.Create(this, Native.Z3_mk_const(nCtx, name.NativeObject, range.NativeObject));
+ }
+
+ ///
+ /// Creates a new Constant of sort and named .
+ ///
+ public Expr MkConst(string name, Sort range)
+ {
+ Contract.Requires(range != null);
+ Contract.Ensures(Contract.Result() != null);
+
+ return MkConst(MkSymbol(name), range);
+ }
+
+ ///
+ /// Creates a fresh Constant of sort and a
+ /// name prefixed with .
+ ///
+ public Expr MkFreshConst(string prefix, Sort range)
+ {
+ Contract.Requires(range != null);
+ Contract.Ensures(Contract.Result() != null);
+
+ CheckContextMatch(range);
+ return Expr.Create(this, Native.Z3_mk_fresh_const(nCtx, prefix, range.NativeObject));
+ }
+
+ ///
+ /// Creates a fresh constant from the FuncDecl .
+ ///
+ /// A decl of a 0-arity function
+ public Expr MkConst(FuncDecl f)
+ {
+ Contract.Requires(f != null);
+ Contract.Ensures(Contract.Result() != null);
+
+ return MkApp(f);
+ }
+
+ ///
+ /// Create a Boolean constant.
+ ///
+ public BoolExpr MkBoolConst(Symbol name)
+ {
+ Contract.Requires(name != null);
+ Contract.Ensures(Contract.Result() != null);
+
+ return (BoolExpr)MkConst(name, BoolSort);
+ }
+
+ ///
+ /// Create a Boolean constant.
+ ///
+ public BoolExpr MkBoolConst(string name)
+ {
+ Contract.Ensures(Contract.Result() != null);
+
+ return (BoolExpr)MkConst(MkSymbol(name), BoolSort);
+ }
+
+ ///
+ /// Creates an integer constant.
+ ///
+ public IntExpr MkIntConst(Symbol name)
+ {
+ Contract.Requires(name != null);
+ Contract.Ensures(Contract.Result() != null);
+
+ return (IntExpr)MkConst(name, IntSort);
+ }
+
+ ///
+ /// Creates an integer constant.
+ ///
+ public IntExpr MkIntConst(string name)
+ {
+ Contract.Requires(name != null);
+ Contract.Ensures(Contract.Result() != null);
+
+ return (IntExpr)MkConst(name, IntSort);
+ }
+
+ ///
+ /// Creates a real constant.
+ ///
+ public RealExpr MkRealConst(Symbol name)
+ {
+ Contract.Requires(name != null);
+ Contract.Ensures(Contract.Result() != null);
+
+ return (RealExpr)MkConst(name, RealSort);
+ }
+
+ ///
+ /// Creates a real constant.
+ ///
+ public RealExpr MkRealConst(string name)
+ {
+ Contract.Ensures(Contract.Result() != null);
+
+ return (RealExpr)MkConst(name, RealSort);
+ }
+
+ ///
+ /// Creates a bit-vector constant.
+ ///
+ public BitVecExpr MkBVConst(Symbol name, uint size)
+ {
+ Contract.Requires(name != null);
+ Contract.Ensures(Contract.Result() != null);
+
+ return (BitVecExpr)MkConst(name, MkBitVecSort(size));
+ }
+
+ ///
+ /// Creates a bit-vector constant.
+ ///
+ public BitVecExpr MkBVConst(string name, uint size)
+ {
+ Contract.Ensures(Contract.Result() != null);
+
+ return (BitVecExpr)MkConst(name, MkBitVecSort(size));
+ }
+ #endregion
+
+ #region Terms
+ ///
+ /// Create a new function application.
+ ///
+ public Expr MkApp(FuncDecl f, params Expr[] args)
+ {
+ Contract.Requires(f != null);
+ Contract.Requires(args == null || Contract.ForAll(args, a => a != null));
+ Contract.Ensures(Contract.Result() != null);
+
+ CheckContextMatch(f);
+ CheckContextMatch(args);
+ return Expr.Create(this, f, args);
+ }
+
+ #region Propositional
+ ///
+ /// The true Term.
+ ///
+ public BoolExpr MkTrue()
+ {
+ Contract.Ensures(Contract.Result() != null);
+
+ return new BoolExpr(this, Native.Z3_mk_true(nCtx));
+ }
+
+ ///
+ /// The false Term.
+ ///
+ public BoolExpr MkFalse()
+ {
+ Contract.Ensures(Contract.Result() != null);
+
+ return new BoolExpr(this, Native.Z3_mk_false(nCtx));
+ }
+
+ ///
+ /// Creates a Boolean value.
+ ///
+ public BoolExpr MkBool(bool value)
+ {
+ Contract.Ensures(Contract.Result() != null);
+
+ return value ? MkTrue() : MkFalse();
+ }
+
+ ///
+ /// Creates the equality = .
+ ///
+ public BoolExpr MkEq(Expr x, Expr y)
+ {
+ Contract.Requires(x != null);
+ Contract.Requires(y != null);
+ Contract.Ensures(Contract.Result() != null);
+
+ CheckContextMatch(x);
+ CheckContextMatch(y);
+ return new BoolExpr(this, Native.Z3_mk_eq(nCtx, x.NativeObject, y.NativeObject));
+ }
+
+ ///
+ /// Creates a distinct term.
+ ///
+ public BoolExpr MkDistinct(params Expr[] args)
+ {
+ Contract.Requires(args != null);
+ Contract.Requires(Contract.ForAll(args, a => a != null));
+
+ Contract.Ensures(Contract.Result() != null);
+
+ CheckContextMatch(args);
+ return new BoolExpr(this, Native.Z3_mk_distinct(nCtx, (uint)args.Length, AST.ArrayToNative(args)));
+ }
+
+ ///
+ /// Mk an expression representing not(a).
+ ///
+ public BoolExpr MkNot(BoolExpr a)
+ {
+ Contract.Requires(a != null);
+ Contract.Ensures(Contract.Result() != null);
+
+ CheckContextMatch(a);
+ return new BoolExpr(this, Native.Z3_mk_not(nCtx, a.NativeObject));
+ }
+
+ ///
+ /// Create an expression representing an if-then-else: ite(t1, t2, t3).
+ ///
+ /// An expression with Boolean sort
+ /// An expression
+ /// An expression with the same sort as
+ public Expr MkITE(BoolExpr t1, Expr t2, Expr t3)
+ {
+ Contract.Requires(t1 != null);
+ Contract.Requires(t2 != null);
+ Contract.Requires(t3 != null);
+ Contract.Ensures(Contract.Result() != null);
+
+ CheckContextMatch(t1);
+ CheckContextMatch(t2);
+ CheckContextMatch(t3);
+ return Expr.Create(this, Native.Z3_mk_ite(nCtx, t1.NativeObject, t2.NativeObject, t3.NativeObject));
+ }
+
+ ///
+ /// Create an expression representing t1 iff t2.
+ ///
+ public BoolExpr MkIff(BoolExpr t1, BoolExpr t2)
+ {
+ Contract.Requires(t1 != null);
+ Contract.Requires(t2 != null);
+ Contract.Ensures(Contract.Result() != null);
+
+ CheckContextMatch(t1);
+ CheckContextMatch(t2);
+ return new BoolExpr(this, Native.Z3_mk_iff(nCtx, t1.NativeObject, t2.NativeObject));
+ }
+
+ ///
+ /// Create an expression representing t1 -> t2.
+ ///
+ public BoolExpr MkImplies(BoolExpr t1, BoolExpr t2)
+ {
+ Contract.Requires(t1 != null);
+ Contract.Requires(t2 != null);
+ Contract.Ensures(Contract.Result() != null);
+
+ CheckContextMatch(t1);
+ CheckContextMatch(t2);
+ return new BoolExpr(this, Native.Z3_mk_implies(nCtx, t1.NativeObject, t2.NativeObject));
+ }
+
+ ///
+ /// Create an expression representing t1 xor t2.
+ ///
+ public BoolExpr MkXor(BoolExpr t1, BoolExpr t2)
+ {
+ Contract.Requires(t1 != null);
+ Contract.Requires(t2 != null);
+ Contract.Ensures(Contract.Result() != null);
+
+ CheckContextMatch(t1);
+ CheckContextMatch(t2);
+ return new BoolExpr(this, Native.Z3_mk_xor(nCtx, t1.NativeObject, t2.NativeObject));
+ }
+
+ ///
+ /// Create an expression representing t[0] and t[1] and ....
+ ///
+ public BoolExpr MkAnd(params BoolExpr[] t)
+ {
+ Contract.Requires(t != null);
+ Contract.Requires(Contract.ForAll(t, a => a != null));
+ Contract.Ensures(Contract.Result() != null);
+
+ CheckContextMatch(t);
+ return new BoolExpr(this, Native.Z3_mk_and(nCtx, (uint)t.Length, AST.ArrayToNative(t)));
+ }
+
+ ///
+ /// Create an expression representing t[0] or t[1] or ....
+ ///
+ public BoolExpr MkOr(params BoolExpr[] t)
+ {
+ Contract.Requires(t != null);
+ Contract.Requires(Contract.ForAll(t, a => a != null));
+ Contract.Ensures(Contract.Result() != null);
+
+ CheckContextMatch(t);
+ return new BoolExpr(this, Native.Z3_mk_or(nCtx, (uint)t.Length, AST.ArrayToNative(t)));
+ }
+ #endregion
+
+ #region Arithmetic
+ ///
+ /// Create an expression representing t[0] + t[1] + ....
+ ///
+ public ArithExpr MkAdd(params ArithExpr[] t)
+ {
+ Contract.Requires(t != null);
+ Contract.Requires(Contract.ForAll(t, a => a != null));
+ Contract.Ensures(Contract.Result() != null);
+
+ CheckContextMatch(t);
+ return (ArithExpr)Expr.Create(this, Native.Z3_mk_add(nCtx, (uint)t.Length, AST.ArrayToNative(t)));
+ }
+
+ ///
+ /// Create an expression representing t[0] * t[1] * ....
+ ///
+ public ArithExpr MkMul(params ArithExpr[] t)
+ {
+ Contract.Requires(t != null);
+ Contract.Requires(Contract.ForAll(t, a => a != null));
+ Contract.Ensures(Contract.Result() != null);
+
+ CheckContextMatch(t);
+ return (ArithExpr)Expr.Create(this, Native.Z3_mk_mul(nCtx, (uint)t.Length, AST.ArrayToNative(t)));
+ }
+
+ ///
+ /// Create an expression representing t[0] - t[1] - ....
+ ///
+ public ArithExpr MkSub(params ArithExpr[] t)
+ {
+ Contract.Requires(t != null);
+ Contract.Requires(Contract.ForAll(t, a => a != null));
+ Contract.Ensures(Contract.Result() != null);
+
+ CheckContextMatch(t);
+ return (ArithExpr)Expr.Create(this, Native.Z3_mk_sub(nCtx, (uint)t.Length, AST.ArrayToNative(t)));
+ }
+
+ ///
+ /// Create an expression representing -t.
+ ///
+ public ArithExpr MkUnaryMinus(ArithExpr t)
+ {
+ Contract.Requires(t != null);
+ Contract.Ensures(Contract.Result() != null);
+
+ CheckContextMatch(t);
+ return (ArithExpr)Expr.Create(this, Native.Z3_mk_unary_minus(nCtx, t.NativeObject));
+ }
+
+ ///
+ /// Create an expression representing t1 / t2.
+ ///
+ public ArithExpr MkDiv(ArithExpr t1, ArithExpr t2)
+ {
+ Contract.Requires(t1 != null);
+ Contract.Requires(t2 != null);
+ Contract.Ensures(Contract.Result() != null);
+
+ CheckContextMatch(t1);
+ CheckContextMatch(t2);
+ return (ArithExpr)Expr.Create(this, Native.Z3_mk_div(nCtx, t1.NativeObject, t2.NativeObject));
+ }
+
+ ///
+ /// Create an expression representing t1 mod t2.
+ ///
+ /// The arguments must have int type.
+ public IntExpr MkMod(IntExpr t1, IntExpr t2)
+ {
+ Contract.Requires(t1 != null);
+ Contract.Requires(t2 != null);
+ Contract.Ensures(Contract.Result() != null);
+
+ CheckContextMatch(t1);
+ CheckContextMatch(t2);
+ return new IntExpr(this, Native.Z3_mk_mod(nCtx, t1.NativeObject, t2.NativeObject));
+ }
+
+ ///
+ /// Create an expression representing t1 rem t2.
+ ///
+ /// The arguments must have int type.
+ public IntExpr MkRem(IntExpr t1, IntExpr t2)
+ {
+ Contract.Requires(t1 != null);
+ Contract.Requires(t2 != null);
+ Contract.Ensures(Contract.Result() != null);
+
+ CheckContextMatch(t1);
+ CheckContextMatch(t2);
+ return new IntExpr(this, Native.Z3_mk_rem(nCtx, t1.NativeObject, t2.NativeObject));
+ }
+
+ ///
+ /// Create an expression representing t1 ^ t2.
+ ///
+ public ArithExpr MkPower(ArithExpr t1, ArithExpr t2)
+ {
+ Contract.Requires(t1 != null);
+ Contract.Requires(t2 != null);
+ Contract.Ensures(Contract.Result() != null);
+
+ CheckContextMatch(t1);
+ CheckContextMatch(t2);
+ return (ArithExpr)Expr.Create(this, Native.Z3_mk_power(nCtx, t1.NativeObject, t2.NativeObject));
+ }
+
+ ///
+ /// Create an expression representing t1 < t2
+ ///
+ public BoolExpr MkLt(ArithExpr t1, ArithExpr t2)
+ {
+ Contract.Requires(t1 != null);
+ Contract.Requires(t2 != null);
+ Contract.Ensures(Contract.Result() != null);
+
+ CheckContextMatch(t1);
+ CheckContextMatch(t2);
+ return new BoolExpr(this, Native.Z3_mk_lt(nCtx, t1.NativeObject, t2.NativeObject));
+ }
+
+ ///
+ /// Create an expression representing t1 <= t2
+ ///
+ public BoolExpr MkLe(ArithExpr t1, ArithExpr t2)
+ {
+ Contract.Requires(t1 != null);
+ Contract.Requires(t2 != null);
+ Contract.Ensures(Contract.Result() != null);
+
+ CheckContextMatch(t1);
+ CheckContextMatch(t2);
+ return new BoolExpr(this, Native.Z3_mk_le(nCtx, t1.NativeObject, t2.NativeObject));
+ }
+
+ ///
+ /// Create an expression representing t1 > t2
+ ///
+ public BoolExpr MkGt(ArithExpr t1, ArithExpr t2)
+ {
+ Contract.Requires(t1 != null);
+ Contract.Requires(t2 != null);
+ Contract.Ensures(Contract.Result() != null);
+
+ CheckContextMatch(t1);
+ CheckContextMatch(t2);
+ return new BoolExpr(this, Native.Z3_mk_gt(nCtx, t1.NativeObject, t2.NativeObject));
+ }
+
+ ///
+ /// Create an expression representing t1 >= t2
+ ///
+ public BoolExpr MkGe(ArithExpr t1, ArithExpr t2)
+ {
+ Contract.Requires(t1 != null);
+ Contract.Requires(t2 != null);
+ Contract.Ensures(Contract.Result() != null);
+
+ CheckContextMatch(t1);
+ CheckContextMatch(t2);
+ return new BoolExpr(this, Native.Z3_mk_ge(nCtx, t1.NativeObject, t2.NativeObject));
+ }
+
+ ///
+ /// Coerce an integer to a real.
+ ///
+ ///
+ /// There is also a converse operation exposed. It follows the semantics prescribed by the SMT-LIB standard.
+ ///
+ /// You can take the floor of a real by creating an auxiliary integer Term k and
+ /// and asserting MakeInt2Real(k) <= t1 < MkInt2Real(k)+1.
+ /// The argument must be of integer sort.
+ ///
+ public RealExpr MkInt2Real(IntExpr t)
+ {
+ Contract.Requires(t != null);
+ Contract.Ensures(Contract.Result() != null);
+
+ CheckContextMatch(t);
+ return new RealExpr(this, Native.Z3_mk_int2real(nCtx, t.NativeObject));
+ }
+
+ ///
+ /// Coerce a real to an integer.
+ ///
+ ///
+ /// The semantics of this function follows the SMT-LIB standard for the function to_int.
+ /// The argument must be of real sort.
+ ///
+ public IntExpr MkReal2Int(RealExpr t)
+ {
+ Contract.Requires(t != null);
+ Contract.Ensures(Contract.Result() != null);
+
+ CheckContextMatch(t);
+ return new IntExpr(this, Native.Z3_mk_real2int(nCtx, t.NativeObject));
+ }
+
+ ///
+ /// Creates an expression that checks whether a real number is an integer.
+ ///
+ public BoolExpr MkIsInteger(RealExpr t)
+ {
+ Contract.Requires(t != null);
+ Contract.Ensures(Contract.Result() != null);
+
+ CheckContextMatch(t);
+ return new BoolExpr(this, Native.Z3_mk_is_int(nCtx, t.NativeObject));
+ }
+ #endregion
+
+ #region Bit-vectors
+ ///
+ /// Bitwise negation.
+ ///
+ /// The argument must have a bit-vector sort.
+ public BitVecExpr MkBVNot(BitVecExpr t)
+ {
+ Contract.Requires(t != null);
+ Contract.Ensures(Contract.Result() != null);
+
+ CheckContextMatch(t);
+ return new BitVecExpr(this, Native.Z3_mk_bvnot(nCtx, t.NativeObject));
+ }
+
+ ///
+ /// Take conjunction of bits in a vector, return vector of length 1.
+ ///
+ /// The argument must have a bit-vector sort.
+ public BitVecExpr MkBVRedAND(BitVecExpr t)
+ {
+ Contract.Requires(t != null);
+ Contract.Ensures(Contract.Result() != null);
+
+ CheckContextMatch(t);
+ return new BitVecExpr(this, Native.Z3_mk_bvredand(nCtx, t.NativeObject));
+ }
+
+ ///
+ /// Take disjunction of bits in a vector, return vector of length 1.
+ ///
+ /// The argument must have a bit-vector sort.
+ public BitVecExpr MkBVRedOR(BitVecExpr t)
+ {
+ Contract.Requires(t != null);
+ Contract.Ensures(Contract.Result() != null);
+
+ CheckContextMatch(t);
+ return new BitVecExpr(this, Native.Z3_mk_bvredor(nCtx, t.NativeObject));
+ }
+
+ ///
+ /// Bitwise conjunction.
+ ///
+ /// The arguments must have a bit-vector sort.
+ public BitVecExpr MkBVAND(BitVecExpr t1, BitVecExpr t2)
+ {
+ Contract.Requires(t1 != null);
+ Contract.Requires(t2 != null);
+ Contract.Ensures(Contract.Result() != null);
+
+ CheckContextMatch(t1);
+ CheckContextMatch(t2);
+ return new BitVecExpr(this, Native.Z3_mk_bvand(nCtx, t1.NativeObject, t2.NativeObject));
+ }
+
+ ///
+ /// Bitwise disjunction.
+ ///
+ /// The arguments must have a bit-vector sort.
+ public BitVecExpr MkBVOR(BitVecExpr t1, BitVecExpr t2)
+ {
+ Contract.Requires(t1 != null);
+ Contract.Requires(t2 != null);
+ Contract.Ensures(Contract.Result() != null);
+
+ CheckContextMatch(t1);
+ CheckContextMatch(t2);
+ return new BitVecExpr(this, Native.Z3_mk_bvor(nCtx, t1.NativeObject, t2.NativeObject));
+ }
+
+ ///
+ /// Bitwise XOR.
+ ///
+ /// The arguments must have a bit-vector sort.
+ public BitVecExpr MkBVXOR(BitVecExpr t1, BitVecExpr t2)
+ {
+ Contract.Requires(t1 != null);
+ Contract.Requires(t2 != null);
+ Contract.Ensures(Contract.Result() != null);
+
+ CheckContextMatch(t1);
+ CheckContextMatch(t2);
+ return new BitVecExpr(this, Native.Z3_mk_bvxor(nCtx, t1.NativeObject, t2.NativeObject));
+ }
+
+ ///
+ /// Bitwise NAND.
+ ///
+ /// The arguments must have a bit-vector sort.
+ public BitVecExpr MkBVNAND(BitVecExpr t1, BitVecExpr t2)
+ {
+ Contract.Requires(t1 != null);
+ Contract.Requires(t2 != null);
+ Contract.Ensures(Contract.Result() != null);
+
+ CheckContextMatch(t1);
+ CheckContextMatch(t2);
+ return new BitVecExpr(this, Native.Z3_mk_bvnand(nCtx, t1.NativeObject, t2.NativeObject));
+ }
+
+ ///
+ /// Bitwise NOR.
+ ///
+ /// The arguments must have a bit-vector sort.
+ public BitVecExpr MkBVNOR(BitVecExpr t1, BitVecExpr t2)
+ {
+ Contract.Requires(t1 != null);
+ Contract.Requires(t2 != null);
+ Contract.Ensures(Contract.Result() != null);
+
+ CheckContextMatch(t1);
+ CheckContextMatch(t2);
+ return new BitVecExpr(this, Native.Z3_mk_bvnor(nCtx, t1.NativeObject, t2.NativeObject));
+ }
+
+ ///
+ /// Bitwise XNOR.
+ ///
+ /// The arguments must have a bit-vector sort.
+ public BitVecExpr MkBVXNOR(BitVecExpr t1, BitVecExpr t2)
+ {
+ Contract.Requires(t1 != null);
+ Contract.Requires(t2 != null);
+ Contract.Ensures(Contract.Result() != null);
+
+ CheckContextMatch(t1);
+ CheckContextMatch(t2);
+ return new BitVecExpr(this, Native.Z3_mk_bvxnor(nCtx, t1.NativeObject, t2.NativeObject));
+ }
+
+ ///
+ /// Standard two's complement unary minus.
+ ///
+ /// The arguments must have a bit-vector sort.
+ public BitVecExpr MkBVNeg(BitVecExpr t)
+ {
+ Contract.Requires(t != null);
+ Contract.Ensures(Contract.Result() != null);
+
+ CheckContextMatch(t);
+ return new BitVecExpr(this, Native.Z3_mk_bvneg(nCtx, t.NativeObject));
+ }
+
+ ///
+ /// Two's complement addition.
+ ///
+ /// The arguments must have the same bit-vector sort.
+ public BitVecExpr MkBVAdd(BitVecExpr t1, BitVecExpr t2)
+ {
+ Contract.Requires(t1 != null);
+ Contract.Requires(t2 != null);
+ Contract.Ensures(Contract.Result() != null);
+
+ CheckContextMatch(t1);
+ CheckContextMatch(t2);
+ return new BitVecExpr(this, Native.Z3_mk_bvadd(nCtx, t1.NativeObject, t2.NativeObject));
+ }
+
+ ///
+ /// Two's complement subtraction.
+ ///
+ /// The arguments must have the same bit-vector sort.
+ public BitVecExpr MkBVSub(BitVecExpr t1, BitVecExpr t2)
+ {
+ Contract.Requires(t1 != null);
+ Contract.Requires(t2 != null);
+ Contract.Ensures(Contract.Result() != null);
+
+ CheckContextMatch(t1);
+ CheckContextMatch(t2);
+ return new BitVecExpr(this, Native.Z3_mk_bvsub(nCtx, t1.NativeObject, t2.NativeObject));
+ }
+
+ ///
+ /// Two's complement multiplication.
+ ///
+ /// The arguments must have the same bit-vector sort.
+ public BitVecExpr MkBVMul(BitVecExpr t1, BitVecExpr t2)
+ {
+ Contract.Requires(t1 != null);
+ Contract.Requires(t2 != null);
+ Contract.Ensures(Contract.Result() != null);
+
+ CheckContextMatch(t1);
+ CheckContextMatch(t2);
+ return new BitVecExpr(this, Native.Z3_mk_bvmul(nCtx, t1.NativeObject, t2.NativeObject));
+ }
+
+ ///
+ /// Unsigned division.
+ ///
+ ///
+ /// It is defined as the floor of t1/t2 if \c t2 is
+ /// different from zero. If t2 is zero, then the result
+ /// is undefined.
+ /// The arguments must have the same bit-vector sort.
+ ///
+ public BitVecExpr MkBVUDiv(BitVecExpr t1, BitVecExpr t2)
+ {
+ Contract.Requires(t1 != null);
+ Contract.Requires(t2 != null);
+ Contract.Ensures(Contract.Result() != null);
+
+ CheckContextMatch(t1);
+ CheckContextMatch(t2);
+ return new BitVecExpr(this, Native.Z3_mk_bvudiv(nCtx, t1.NativeObject, t2.NativeObject));
+ }
+
+ ///
+ /// Signed division.
+ ///
+ ///
+ /// It is defined in the following way:
+ ///
+ /// - The \c floor of t1/t2 if \c t2 is different from zero, and t1*t2 >= 0.
+ ///
+ /// - The \c ceiling of t1/t2 if \c t2 is different from zero, and t1*t2 < 0.
+ ///
+ /// If t2 is zero, then the result is undefined.
+ /// The arguments must have the same bit-vector sort.
+ ///
+ public BitVecExpr MkBVSDiv(BitVecExpr t1, BitVecExpr t2)
+ {
+ Contract.Requires(t1 != null);
+ Contract.Requires(t2 != null);
+ Contract.Ensures(Contract.Result() != null);
+
+ CheckContextMatch(t1);
+ CheckContextMatch(t2);
+ return new BitVecExpr(this, Native.Z3_mk_bvsdiv(nCtx, t1.NativeObject, t2.NativeObject));
+ }
+
+ ///
+ /// Unsigned remainder.
+ ///
+ ///
+ /// It is defined as t1 - (t1 /u t2) * t2, where /u represents unsigned division.
+ /// If t2 is zero, then the result is undefined.
+ /// The arguments must have the same bit-vector sort.
+ ///
+ public BitVecExpr MkBVURem(BitVecExpr t1, BitVecExpr t2)
+ {
+ Contract.Requires(t1 != null);
+ Contract.Requires(t2 != null);
+ Contract.Ensures(Contract.Result() != null);
+
+ CheckContextMatch(t1);
+ CheckContextMatch(t2);
+ return new BitVecExpr(this, Native.Z3_mk_bvurem(nCtx, t1.NativeObject, t2.NativeObject));
+ }
+
+ ///
+ /// Signed remainder.
+ ///
+ ///
+ /// It is defined as t1 - (t1 /s t2) * t2, where /s represents signed division.
+ /// The most significant bit (sign) of the result is equal to the most significant bit of \c t1.
+ ///
+ /// If t2 is zero, then the result is undefined.
+ /// The arguments must have the same bit-vector sort.
+ ///
+ public BitVecExpr MkBVSRem(BitVecExpr t1, BitVecExpr t2)
+ {
+ Contract.Requires(t1 != null);
+ Contract.Requires(t2 != null);
+ Contract.Ensures(Contract.Result() != null);
+
+ CheckContextMatch(t1);
+ CheckContextMatch(t2);
+ return new BitVecExpr(this, Native.Z3_mk_bvsrem(nCtx, t1.NativeObject, t2.NativeObject));
+ }
+
+ ///
+ /// Two's complement signed remainder (sign follows divisor).
+ ///
+ ///
+ /// If t2 is zero, then the result is undefined.
+ /// The arguments must have the same bit-vector sort.
+ ///
+ public BitVecExpr MkBVSMod(BitVecExpr t1, BitVecExpr t2)
+ {
+ Contract.Requires(t1 != null);
+ Contract.Requires(t2 != null);
+ Contract.Ensures(Contract.Result() != null);
+
+ CheckContextMatch(t1);
+ CheckContextMatch(t2);
+ return new BitVecExpr(this, Native.Z3_mk_bvsmod(nCtx, t1.NativeObject, t2.NativeObject));
+ }
+
+ ///
+ /// Unsigned less-than
+ ///
+ ///
+ /// The arguments must have the same bit-vector sort.
+ ///
+ public BoolExpr MkBVULT(BitVecExpr t1, BitVecExpr t2)
+ {
+ Contract.Requires(t1 != null);
+ Contract.Requires(t2 != null);
+ Contract.Ensures(Contract.Result() != null);
+
+ CheckContextMatch(t1);
+ CheckContextMatch(t2);
+ return new BoolExpr(this, Native.Z3_mk_bvult(nCtx, t1.NativeObject, t2.NativeObject));
+ }
+
+ ///
+ /// Two's complement signed less-than
+ ///
+ ///
+ /// The arguments must have the same bit-vector sort.
+ ///
+ public BoolExpr MkBVSLT(BitVecExpr t1, BitVecExpr t2)
+ {
+ Contract.Requires(t1 != null);
+ Contract.Requires(t2 != null);
+ Contract.Ensures(Contract.Result() != null);
+
+ CheckContextMatch(t1);
+ CheckContextMatch(t2);
+ return new BoolExpr(this, Native.Z3_mk_bvslt(nCtx, t1.NativeObject, t2.NativeObject));
+ }
+
+ ///
+ /// Unsigned less-than or equal to.
+ ///
+ ///
+ /// The arguments must have the same bit-vector sort.
+ ///
+ public BoolExpr MkBVULE(BitVecExpr t1, BitVecExpr t2)
+ {
+ Contract.Requires(t1 != null);
+ Contract.Requires(t2 != null);
+ Contract.Ensures(Contract.Result() != null);
+
+ CheckContextMatch(t1);
+ CheckContextMatch(t2);
+ return new BoolExpr(this, Native.Z3_mk_bvule(nCtx, t1.NativeObject, t2.NativeObject));
+ }
+
+ ///
+ /// Two's complement signed less-than or equal to.
+ ///
+ ///
+ /// The arguments must have the same bit-vector sort.
+ ///
+ public BoolExpr MkBVSLE(BitVecExpr t1, BitVecExpr t2)
+ {
+ Contract.Requires(t1 != null);
+ Contract.Requires(t2 != null);
+ Contract.Ensures(Contract.Result() != null);
+
+ CheckContextMatch(t1);
+ CheckContextMatch(t2);
+ return new BoolExpr(this, Native.Z3_mk_bvsle(nCtx, t1.NativeObject, t2.NativeObject));
+ }
+
+ ///
+ /// Unsigned greater than or equal to.
+ ///
+ ///
+ /// The arguments must have the same bit-vector sort.
+ ///
+ public BoolExpr MkBVUGE(BitVecExpr t1, BitVecExpr t2)
+ {
+ Contract.Requires(t1 != null);
+ Contract.Requires(t2 != null);
+ Contract.Ensures(Contract.Result() != null);
+
+ CheckContextMatch(t1);
+ CheckContextMatch(t2);
+ return new BoolExpr(this, Native.Z3_mk_bvuge(nCtx, t1.NativeObject, t2.NativeObject));
+ }
+
+ ///
+ /// Two's complement signed greater than or equal to.
+ ///
+ ///
+ /// The arguments must have the same bit-vector sort.
+ ///
+ public BoolExpr MkBVSGE(BitVecExpr t1, BitVecExpr t2)
+ {
+ Contract.Requires(t1 != null);
+ Contract.Requires(t2 != null);
+ Contract.Ensures(Contract.Result() != null);
+
+ CheckContextMatch(t1);
+ CheckContextMatch(t2);
+ return new BoolExpr(this, Native.Z3_mk_bvsge(nCtx, t1.NativeObject, t2.NativeObject));
+ }
+
+ ///
+ /// Unsigned greater-than.
+ ///
+ ///
+ /// The arguments must have the same bit-vector sort.
+ ///
+ public BoolExpr MkBVUGT(BitVecExpr t1, BitVecExpr t2)
+ {
+ Contract.Requires(t1 != null);
+ Contract.Requires(t2 != null);
+ Contract.Ensures(Contract.Result() != null);
+
+ CheckContextMatch(t1);
+ CheckContextMatch(t2);
+ return new BoolExpr(this, Native.Z3_mk_bvugt(nCtx, t1.NativeObject, t2.NativeObject));
+ }
+
+ ///
+ /// Two's complement signed greater-than.
+ ///
+ ///
+ /// The arguments must have the same bit-vector sort.
+ ///
+ public BoolExpr MkBVSGT(BitVecExpr t1, BitVecExpr t2)
+ {
+ Contract.Requires(t1 != null);
+ Contract.Requires(t2 != null);
+ Contract.Ensures(Contract.Result() != null);
+
+ CheckContextMatch(t1);
+ CheckContextMatch(t2);
+ return new BoolExpr(this, Native.Z3_mk_bvsgt(nCtx, t1.NativeObject, t2.NativeObject));
+ }
+
+ ///
+ /// Bit-vector concatenation.
+ ///
+ ///
+ /// The arguments must have a bit-vector sort.
+ ///
+ ///
+ /// The result is a bit-vector of size n1+n2, where n1 (n2)
+ /// is the size of t1 (t2).
+ ///
+ public BitVecExpr MkConcat(BitVecExpr t1, BitVecExpr t2)
+ {
+ Contract.Requires(t1 != null);
+ Contract.Requires(t2 != null);
+ Contract.Ensures(Contract.Result() != null);
+
+ CheckContextMatch(t1);
+ CheckContextMatch(t2);
+ return new BitVecExpr(this, Native.Z3_mk_concat(nCtx, t1.NativeObject, t2.NativeObject));
+ }
+
+ ///
+ /// Bit-vector extraction.
+ ///
+ ///
+ /// Extract the bits down to from a bitvector of
+ /// size m to yield a new bitvector of size n, where
+ /// n = high - low + 1.
+ /// The argument must have a bit-vector sort.
+ ///
+ public BitVecExpr MkExtract(uint high, uint low, BitVecExpr t)
+ {
+ Contract.Requires(t != null);
+ Contract.Ensures(Contract.Result() != null);
+
+ CheckContextMatch(t);
+ return new BitVecExpr(this, Native.Z3_mk_extract(nCtx, high, low, t.NativeObject));
+ }
+
+ ///
+ /// Bit-vector sign extension.
+ ///
+ ///
+ /// Sign-extends the given bit-vector to the (signed) equivalent bitvector of
+ /// size m+i, where \c m is the size of the given bit-vector.
+ /// The argument must have a bit-vector sort.
+ ///
+ public BitVecExpr MkSignExt(uint i, BitVecExpr t)
+ {
+ Contract.Requires(t != null);
+ Contract.Ensures(Contract.Result() != null);
+
+ CheckContextMatch(t);
+ return new BitVecExpr(this, Native.Z3_mk_sign_ext(nCtx, i, t.NativeObject));
+ }
+
+ ///
+ /// Bit-vector zero extension.
+ ///
+ ///
+ /// Extend the given bit-vector with zeros to the (unsigned) equivalent
+ /// bitvector of size m+i, where \c m is the size of the
+ /// given bit-vector.
+ /// The argument must have a bit-vector sort.
+ ///
+ public BitVecExpr MkZeroExt(uint i, BitVecExpr t)
+ {
+ Contract.Requires(t != null);
+ Contract.Ensures(Contract.Result() != null);
+
+ CheckContextMatch(t);
+ return new BitVecExpr(this, Native.Z3_mk_zero_ext(nCtx, i, t.NativeObject));
+ }
+
+ ///
+ /// Bit-vector repetition.
+ ///
+ ///
+ /// The argument must have a bit-vector sort.
+ ///
+ public BitVecExpr MkRepeat(uint i, BitVecExpr t)
+ {
+ Contract.Requires(t != null);
+ Contract.Ensures(Contract.Result() != null);
+
+ CheckContextMatch(t);
+ return new BitVecExpr(this, Native.Z3_mk_repeat(nCtx, i, t.NativeObject));
+ }
+
+ ///
+ /// Shift left.
+ ///
+ ///
+ /// It is equivalent to multiplication by 2^x where \c x is the value of .
+ ///
+ /// NB. The semantics of shift operations varies between environments. This
+ /// definition does not necessarily capture directly the semantics of the
+ /// programming language or assembly architecture you are modeling.
+ ///
+ /// The arguments must have a bit-vector sort.
+ ///
+ public BitVecExpr MkBVSHL(BitVecExpr t1, BitVecExpr t2)
+ {
+ Contract.Requires(t1 != null);
+ Contract.Requires(t2 != null);
+ Contract.Ensures(Contract.Result() != null);
+
+ CheckContextMatch(t1);
+ CheckContextMatch(t2);
+ return new BitVecExpr(this, Native.Z3_mk_bvshl(nCtx, t1.NativeObject, t2.NativeObject));
+ }
+
+ ///
+ /// Logical shift right
+ ///
+ ///
+ /// It is equivalent to unsigned division by 2^x where \c x is the value of .
+ ///
+ /// NB. The semantics of shift operations varies between environments. This
+ /// definition does not necessarily capture directly the semantics of the
+ /// programming language or assembly architecture you are modeling.
+ ///
+ /// The arguments must have a bit-vector sort.
+ ///
+ public BitVecExpr MkBVLSHR(BitVecExpr t1, BitVecExpr t2)
+ {
+ Contract.Requires(t1 != null);
+ Contract.Requires(t2 != null);
+ Contract.Ensures(Contract.Result() != null);
+
+ CheckContextMatch(t1);
+ CheckContextMatch(t2);
+ return new BitVecExpr(this, Native.Z3_mk_bvlshr(nCtx, t1.NativeObject, t2.NativeObject));
+ }
+
+ ///
+ /// Arithmetic shift right
+ ///
+ ///
+ /// It is like logical shift right except that the most significant
+ /// bits of the result always copy the most significant bit of the
+ /// second argument.
+ ///
+ /// NB. The semantics of shift operations varies between environments. This
+ /// definition does not necessarily capture directly the semantics of the
+ /// programming language or assembly architecture you are modeling.
+ ///
+ /// The arguments must have a bit-vector sort.
+ ///
+ public BitVecExpr MkBVASHR(BitVecExpr t1, BitVecExpr t2)
+ {
+ Contract.Requires(t1 != null);
+ Contract.Requires(t2 != null);
+ Contract.Ensures(Contract.Result() != null);
+
+ CheckContextMatch(t1);
+ CheckContextMatch(t2);
+ return new BitVecExpr(this, Native.Z3_mk_bvashr(nCtx, t1.NativeObject, t2.NativeObject));
+ }
+
+ ///
+ /// Rotate Left.
+ ///
+ ///
+ /// Rotate bits of \c t to the left \c i times.
+ /// The argument must have a bit-vector sort.
+ ///
+ public BitVecExpr MkBVRotateLeft(uint i, BitVecExpr t)
+ {
+ Contract.Requires(t != null);
+ Contract.Ensures(Contract.Result() != null);
+
+ CheckContextMatch(t);
+ return new BitVecExpr(this, Native.Z3_mk_rotate_left(nCtx, i, t.NativeObject));
+ }
+
+ ///
+ /// Rotate Right.
+ ///
+ ///
+ /// Rotate bits of \c t to the right \c i times.
+ /// The argument must have a bit-vector sort.
+ ///
+ public BitVecExpr MkBVRotateRight(uint i, BitVecExpr t)
+ {
+ Contract.Requires(t != null);
+ Contract.Ensures(Contract.Result() != null);
+
+ CheckContextMatch(t);
+ return new BitVecExpr(this, Native.Z3_mk_rotate_right(nCtx, i, t.NativeObject));
+ }
+
+ ///
+ /// Rotate Left.
+ ///
+ ///
+ /// Rotate bits of to the left times.
+ /// The arguments must have the same bit-vector sort.
+ ///
+ public BitVecExpr MkBVRotateLeft(BitVecExpr t1, BitVecExpr t2)
+ {
+ Contract.Requires(t1 != null);
+ Contract.Requires(t2 != null);
+ Contract.Ensures(Contract.Result() != null);
+
+ CheckContextMatch(t1);
+ CheckContextMatch(t2);
+ return new BitVecExpr(this, Native.Z3_mk_ext_rotate_left(nCtx, t1.NativeObject, t2.NativeObject));
+ }
+
+ ///
+ /// Rotate Right.
+ ///
+ ///
+ /// Rotate bits of to the right times.
+ /// The arguments must have the same bit-vector sort.
+ ///
+ public BitVecExpr MkBVRotateRight(BitVecExpr t1, BitVecExpr t2)
+ {
+ Contract.Requires(t1 != null);
+ Contract.Requires(t2 != null);
+ Contract.Ensures(Contract.Result() != null);
+
+ CheckContextMatch(t1);
+ CheckContextMatch(t2);
+ return new BitVecExpr(this, Native.Z3_mk_ext_rotate_right(nCtx, t1.NativeObject, t2.NativeObject));
+ }
+
+ ///
+ /// Create an bit bit-vector from the integer argument .
+ ///
+ ///
+ /// NB. This function is essentially treated as uninterpreted.
+ /// So you cannot expect Z3 to precisely reflect the semantics of this function
+ /// when solving constraints with this function.
+ ///
+ /// The argument must be of integer sort.
+ ///
+ public BitVecExpr MkInt2BV(uint n, IntExpr t)
+ {
+ Contract.Requires(t != null);
+ Contract.Ensures(Contract.Result() != null);
+
+ CheckContextMatch(t);
+ return new BitVecExpr(this, Native.Z3_mk_int2bv(nCtx, n, t.NativeObject));
+ }
+
+ ///
+ /// Create an integer from the bit-vector argument .
+ ///
+ ///
+ /// If \c is_signed is false, then the bit-vector \c t1 is treated as unsigned.
+ /// So the result is non-negative and in the range [0..2^N-1], where
+ /// N are the number of bits in .
+ /// If \c is_signed is true, \c t1 is treated as a signed bit-vector.
+ ///
+ /// NB. This function is essentially treated as uninterpreted.
+ /// So you cannot expect Z3 to precisely reflect the semantics of this function
+ /// when solving constraints with this function.
+ ///
+ /// The argument must be of bit-vector sort.
+ ///
+ public IntExpr MkBV2Int(BitVecExpr t, bool signed)
+ {
+ Contract.Requires(t != null);
+ Contract.Ensures(Contract.Result() != null);
+
+ CheckContextMatch(t);
+ return new IntExpr(this, Native.Z3_mk_bv2int(nCtx, t.NativeObject, (signed) ? 1 : 0));
+ }
+
+ ///
+ /// Create a predicate that checks that the bit-wise addition does not overflow.
+ ///
+ ///
+ /// The arguments must be of bit-vector sort.
+ ///
+ public BoolExpr MkBVAddNoOverflow(BitVecExpr t1, BitVecExpr t2, bool isSigned)
+ {
+ Contract.Requires(t1 != null);
+ Contract.Requires(t2 != null);
+ Contract.Ensures(Contract.Result() != null);
+
+ CheckContextMatch(t1);
+ CheckContextMatch(t2);
+ return new BoolExpr(this, Native.Z3_mk_bvadd_no_overflow(nCtx, t1.NativeObject, t2.NativeObject, (isSigned) ? 1 : 0));
+ }
+
+ ///
+ /// Create a predicate that checks that the bit-wise addition does not underflow.
+ ///
+ ///
+ /// The arguments must be of bit-vector sort.
+ ///
+ public BoolExpr MkBVAddNoUnderflow(BitVecExpr t1, BitVecExpr t2)
+ {
+ Contract.Requires(t1 != null);
+ Contract.Requires(t2 != null);
+ Contract.Ensures(Contract.Result() != null);
+
+ CheckContextMatch(t1);
+ CheckContextMatch(t2);
+ return new BoolExpr(this, Native.Z3_mk_bvadd_no_underflow(nCtx, t1.NativeObject, t2.NativeObject));
+ }
+
+ ///
+ /// Create a predicate that checks that the bit-wise subtraction does not overflow.
+ ///
+ ///
+ /// The arguments must be of bit-vector sort.
+ ///
+ public BoolExpr MkBVSubNoOverflow(BitVecExpr t1, BitVecExpr t2)
+ {
+ Contract.Requires(t1 != null);
+ Contract.Requires(t2 != null);
+ Contract.Ensures(Contract.Result() != null);
+
+ CheckContextMatch(t1);
+ CheckContextMatch(t2);
+ return new BoolExpr(this, Native.Z3_mk_bvsub_no_overflow(nCtx, t1.NativeObject, t2.NativeObject));
+ }
+
+ ///
+ /// Create a predicate that checks that the bit-wise subtraction does not underflow.
+ ///
+ ///
+ /// The arguments must be of bit-vector sort.
+ ///
+ public BoolExpr MkBVSubNoUnderflow(BitVecExpr t1, BitVecExpr t2, bool isSigned)
+ {
+ Contract.Requires(t1 != null);
+ Contract.Requires(t2 != null);
+ Contract.Ensures(Contract.Result() != null);
+
+ CheckContextMatch(t1);
+ CheckContextMatch(t2);
+ return new BoolExpr(this, Native.Z3_mk_bvsub_no_underflow(nCtx, t1.NativeObject, t2.NativeObject, (isSigned) ? 1 : 0));
+ }
+
+ ///
+ /// Create a predicate that checks that the bit-wise signed division does not overflow.
+ ///
+ ///
+ /// The arguments must be of bit-vector sort.
+ ///
+ public BoolExpr MkBVSDivNoOverflow(BitVecExpr t1, BitVecExpr t2)
+ {
+ Contract.Requires(t1 != null);
+ Contract.Requires(t2 != null);
+ Contract.Ensures(Contract.Result() != null);
+
+ CheckContextMatch(t1);
+ CheckContextMatch(t2);
+ return new BoolExpr(this, Native.Z3_mk_bvsdiv_no_overflow(nCtx, t1.NativeObject, t2.NativeObject));
+ }
+
+ ///
+ /// Create a predicate that checks that the bit-wise negation does not overflow.
+ ///
+ ///
+ /// The arguments must be of bit-vector sort.
+ ///
+ public BoolExpr MkBVNegNoOverflow(BitVecExpr t)
+ {
+ Contract.Requires(t != null);
+ Contract.Ensures(Contract.Result() != null);
+
+ CheckContextMatch(t);
+ return new BoolExpr(this, Native.Z3_mk_bvneg_no_overflow(nCtx, t.NativeObject));
+ }
+
+ ///
+ /// Create a predicate that checks that the bit-wise multiplication does not overflow.
+ ///
+ ///
+ /// The arguments must be of bit-vector sort.
+ ///
+ public BoolExpr MkBVMulNoOverflow(BitVecExpr t1, BitVecExpr t2, bool isSigned)
+ {
+ Contract.Requires(t1 != null);
+ Contract.Requires(t2 != null);
+ Contract.Ensures(Contract.Result() != null);
+
+ CheckContextMatch(t1);
+ CheckContextMatch(t2);
+ return new BoolExpr(this, Native.Z3_mk_bvmul_no_overflow(nCtx, t1.NativeObject, t2.NativeObject, (isSigned) ? 1 : 0));
+ }
+
+ ///
+ /// Create a predicate that checks that the bit-wise multiplication does not underflow.
+ ///
+ ///
+ /// The arguments must be of bit-vector sort.
+ ///
+ public BoolExpr MkBVMulNoUnderflow(BitVecExpr t1, BitVecExpr t2)
+ {
+ Contract.Requires(t1 != null);
+ Contract.Requires(t2 != null);
+ Contract.Ensures(Contract.Result() != null);
+
+ CheckContextMatch(t1);
+ CheckContextMatch(t2);
+ return new BoolExpr(this, Native.Z3_mk_bvmul_no_underflow(nCtx, t1.NativeObject, t2.NativeObject));
+ }
+ #endregion
+
+ #region Arrays
+ ///
+ /// Create an array constant.
+ ///
+ public ArrayExpr MkArrayConst(Symbol name, Sort domain, Sort range)
+ {
+ Contract.Requires(name != null);
+ Contract.Requires(domain != null);
+ Contract.Requires(range != null);
+ Contract.Ensures(Contract.Result() != null);
+
+ return (ArrayExpr)MkConst(name, MkArraySort(domain, range));
+ }
+
+ ///
+ /// Create an array constant.
+ ///
+ public ArrayExpr MkArrayConst(string name, Sort domain, Sort range)
+ {
+ Contract.Requires(domain != null);
+ Contract.Requires(range != null);
+ Contract.Ensures(Contract.Result() != null);
+
+ return (ArrayExpr)MkConst(MkSymbol(name), MkArraySort(domain, range));
+ }
+
+ ///
+ /// Array read.
+ ///
+ ///
+ /// The argument a is the array and i is the index
+ /// of the array that gets read.
+ ///
+ /// The node a must have an array sort [domain -> range],
+ /// and i must have the sort domain.
+ /// The sort of the result is range.
+ ///
+ ///
+ ///
+ public Expr MkSelect(ArrayExpr a, Expr i)
+ {
+ Contract.Requires(a != null);
+ Contract.Requires(i != null);
+ Contract.Ensures(Contract.Result() != null);
+
+ CheckContextMatch(a);
+ CheckContextMatch(i);
+ return Expr.Create(this, Native.Z3_mk_select(nCtx, a.NativeObject, i.NativeObject));
+ }
+
+ ///
+ /// Array update.
+ ///
+ ///
+ /// The node a must have an array sort [domain -> range],
+ /// i must have sort domain,
+ /// v must have sort range. The sort of the result is [domain -> range].
+ /// The semantics of this function is given by the theory of arrays described in the SMT-LIB
+ /// standard. See http://smtlib.org for more details.
+ /// The result of this function is an array that is equal to a
+ /// (with respect to select)
+ /// on all indices except for i, where it maps to v
+ /// (and the select of a with
+ /// respect to i may be a different value).
+ ///
+ ///
+ ///
+ public ArrayExpr MkStore(ArrayExpr a, Expr i, Expr v)
+ {
+ Contract.Requires(a != null);
+ Contract.Requires(i != null);
+ Contract.Requires(v != null);
+ Contract.Ensures(Contract.Result() != null);
+
+ CheckContextMatch(a);
+ CheckContextMatch(i);
+ CheckContextMatch(v);
+ return new ArrayExpr(this, Native.Z3_mk_store(nCtx, a.NativeObject, i.NativeObject, v.NativeObject));
+ }
+
+ ///
+ /// Create a constant array.
+ ///
+ ///
+ /// The resulting term is an array, such that a selecton an arbitrary index
+ /// produces the value v.
+ ///
+ ///
+ ///
+ public ArrayExpr MkConstArray(Sort domain, Expr v)
+ {
+ Contract.Requires(domain != null);
+ Contract.Requires(v != null);
+ Contract.Ensures(Contract.Result() != null);
+
+ CheckContextMatch(domain);
+ CheckContextMatch(v);
+ return new ArrayExpr(this, Native.Z3_mk_const_array(nCtx, domain.NativeObject, v.NativeObject));
+ }
+
+ ///
+ /// Maps f on the argument arrays.
+ ///
+ ///
+ /// Eeach element of args must be of an array sort [domain_i -> range_i].
+ /// The function declaration f must have type range_1 .. range_n -> range.
+ /// v must have sort range. The sort of the result is [domain_i -> range].
+ ///
+ ///
+ ///
+ ///
+ public ArrayExpr MkMap(FuncDecl f, params ArrayExpr[] args)
+ {
+ Contract.Requires(f != null);
+ Contract.Requires(args == null || Contract.ForAll(args, a => a != null));
+ Contract.Ensures(Contract.Result() != null);
+
+ CheckContextMatch(f);
+ CheckContextMatch(args);
+ return (ArrayExpr)Expr.Create(this, Native.Z3_mk_map(nCtx, f.NativeObject, AST.ArrayLength(args), AST.ArrayToNative(args)));
+ }
+
+ ///
+ /// Access the array default value.
+ ///
+ ///
+ /// Produces the default range value, for arrays that can be represented as
+ /// finite maps with a default range value.
+ ///
+ public Expr MkTermArray(ArrayExpr array)
+ {
+ Contract.Requires(array != null);
+ Contract.Ensures(Contract.Result() != null);
+
+ CheckContextMatch(array);
+ return Expr.Create(this, Native.Z3_mk_array_default(nCtx, array.NativeObject));
+ }
+ #endregion
+
+ #region Sets
+ ///
+ /// Create a set type.
+ ///
+ public SetSort MkSetSort(Sort ty)
+ {
+ Contract.Requires(ty != null);
+ Contract.Ensures(Contract.Result() != null);
+
+ CheckContextMatch(ty);
+ return new SetSort(this, ty);
+ }
+
+ ///
+ /// Create an empty set.
+ ///
+ public Expr MkEmptySet(Sort domain)
+ {
+ Contract.Requires(domain != null);
+ Contract.Ensures(Contract.Result() != null);
+
+ CheckContextMatch(domain);
+ return Expr.Create(this, Native.Z3_mk_empty_set(nCtx, domain.NativeObject));
+ }
+
+ ///
+ /// Create the full set.
+ ///
+ public Expr MkFullSet(Sort domain)
+ {
+ Contract.Requires(domain != null);
+ Contract.Ensures(Contract.Result() != null);
+
+ CheckContextMatch(domain);
+ return Expr.Create(this, Native.Z3_mk_full_set(nCtx, domain.NativeObject));
+ }
+
+ ///
+ /// Add an element to the set.
+ ///
+ public Expr MkSetAdd(Expr set, Expr element)
+ {
+ Contract.Requires(set != null);
+ Contract.Requires(element != null);
+ Contract.Ensures(Contract.Result() != null);
+
+ CheckContextMatch(set);
+ CheckContextMatch(element);
+ return Expr.Create(this, Native.Z3_mk_set_add(nCtx, set.NativeObject, element.NativeObject));
+ }
+
+
+ ///
+ /// Remove an element from a set.
+ ///
+ public Expr MkSetDel(Expr set, Expr element)
+ {
+ Contract.Requires(set != null);
+ Contract.Requires(element != null);
+ Contract.Ensures(Contract.Result() != null);
+
+ CheckContextMatch(set);
+ CheckContextMatch(element);
+ return Expr.Create(this, Native.Z3_mk_set_del(nCtx, set.NativeObject, element.NativeObject));
+ }
+
+ ///
+ /// Take the union of a list of sets.
+ ///
+ public Expr MkSetUnion(params Expr[] args)
+ {
+ Contract.Requires(args != null);
+ Contract.Requires(Contract.ForAll(args, a => a != null));
+
+ CheckContextMatch(args);
+ return Expr.Create(this, Native.Z3_mk_set_union(nCtx, (uint)args.Length, AST.ArrayToNative(args)));
+ }
+
+ ///
+ /// Take the intersection of a list of sets.
+ ///
+ public Expr MkSetIntersection(params Expr[] args)
+ {
+ Contract.Requires(args != null);
+ Contract.Requires(Contract.ForAll(args, a => a != null));
+ Contract.Ensures(Contract.Result() != null);
+
+ CheckContextMatch(args);
+ return Expr.Create(this, Native.Z3_mk_set_intersect(nCtx, (uint)args.Length, AST.ArrayToNative(args)));
+ }
+
+ ///
+ /// Take the difference between two sets.
+ ///
+ public Expr MkSetDifference(Expr arg1, Expr arg2)
+ {
+ Contract.Requires(arg1 != null);
+ Contract.Requires(arg2 != null);
+ Contract.Ensures(Contract.Result() != null);
+
+ CheckContextMatch(arg1);
+ CheckContextMatch(arg2);
+ return Expr.Create(this, Native.Z3_mk_set_difference(nCtx, arg1.NativeObject, arg2.NativeObject));
+ }
+
+ ///
+ /// Take the complement of a set.
+ ///
+ public Expr MkSetComplement(Expr arg)
+ {
+ Contract.Requires(arg != null);
+ Contract.Ensures(Contract.Result() != null);
+
+ CheckContextMatch(arg);
+ return Expr.Create(this, Native.Z3_mk_set_complement(nCtx, arg.NativeObject));
+ }
+
+ ///
+ /// Check for set membership.
+ ///
+ public Expr MkSetMembership(Expr elem, Expr set)
+ {
+ Contract.Requires(elem != null);
+ Contract.Requires(set != null);
+ Contract.Ensures(Contract.Result() != null);
+
+ CheckContextMatch(elem);
+ CheckContextMatch(set);
+ return Expr.Create(this, Native.Z3_mk_set_member(nCtx, elem.NativeObject, set.NativeObject));
+ }
+
+ ///
+ /// Check for subsetness of sets.
+ ///
+ public Expr MkSetSubset(Expr arg1, Expr arg2)
+ {
+ Contract.Requires(arg1 != null);
+ Contract.Requires(arg2 != null);
+ Contract.Ensures(Contract.Result() != null);
+
+ CheckContextMatch(arg1);
+ CheckContextMatch(arg2);
+ return Expr.Create(this, Native.Z3_mk_set_subset(nCtx, arg1.NativeObject, arg2.NativeObject));
+ }
+ #endregion
+
+ #region Numerals
+
+ #region General Numerals
+ ///
+ /// Create a Term of a given sort.
+ ///
+ /// A string representing the Term value in decimal notation. If the given sort is a real, then the Term can be a rational, that is, a string of the form [num]* / [num]*.
+ /// The sort of the numeral. In the current implementation, the given sort can be an int, real, or bit-vectors of arbitrary size.
+ /// A Term with value and sort
+ public Expr MkNumeral(string v, Sort ty)
+ {
+ Contract.Requires(ty != null);
+ Contract.Ensures(Contract.Result() != null);
+
+ CheckContextMatch(ty);
+ return Expr.Create(this, Native.Z3_mk_numeral(nCtx, v, ty.NativeObject));
+ }
+
+ ///
+ /// Create a Term of a given sort. This function can be use to create numerals that fit in a machine integer.
+ /// It is slightly faster than MakeNumeral since it is not necessary to parse a string.
+ ///
+ /// Value of the numeral
+ /// Sort of the numeral
+ /// A Term with value and type
+ public Expr MkNumeral(int v, Sort ty)
+ {
+ Contract.Requires(ty != null);
+ Contract.Ensures(Contract.Result() != null);
+
+ CheckContextMatch(ty);
+ return Expr.Create(this, Native.Z3_mk_int(nCtx, v, ty.NativeObject));
+ }
+
+ ///
+ /// Create a Term of a given sort. This function can be use to create numerals that fit in a machine integer.
+ /// It is slightly faster than MakeNumeral since it is not necessary to parse a string.
+ ///
+ /// Value of the numeral
+ /// Sort of the numeral
+ /// A Term with value and type
+ public Expr MkNumeral(uint v, Sort ty)
+ {
+ Contract.Requires(ty != null);
+ Contract.Ensures(Contract.Result() != null);
+
+ CheckContextMatch(ty);
+ return Expr.Create(this, Native.Z3_mk_unsigned_int(nCtx, v, ty.NativeObject));
+ }
+
+ ///
+ /// Create a Term of a given sort. This function can be use to create numerals that fit in a machine integer.
+ /// It is slightly faster than MakeNumeral since it is not necessary to parse a string.
+ ///
+ /// Value of the numeral
+ /// Sort of the numeral
+ /// A Term with value and type
+ public Expr MkNumeral(long v, Sort ty)
+ {
+ Contract.Requires(ty != null);
+ Contract.Ensures(Contract.Result() != null);
+
+ CheckContextMatch(ty);
+ return Expr.Create(this, Native.Z3_mk_int64(nCtx, v, ty.NativeObject));
+ }
+
+ ///
+ /// Create a Term of a given sort. This function can be use to create numerals that fit in a machine integer.
+ /// It is slightly faster than MakeNumeral since it is not necessary to parse a string.
+ ///
+ /// Value of the numeral
+ /// Sort of the numeral
+ /// A Term with value and type
+ public Expr MkNumeral(ulong v, Sort ty)
+ {
+ Contract.Requires(ty != null);
+ Contract.Ensures(Contract.Result() != null);
+
+ CheckContextMatch(ty);
+ return Expr.Create(this, Native.Z3_mk_unsigned_int64(nCtx, v, ty.NativeObject));
+ }
+ #endregion
+
+ #region Reals
+ ///
+ /// Create a real from a fraction.
+ ///
+ /// numerator of rational.
+ /// denominator of rational.
+ /// A Term with value / and sort Real
+ ///
+ public RatNum MkReal(int num, int den)
+ {
+ if (den == 0)
+ throw new Z3Exception("Denominator is zero");
+
+ Contract.Ensures(Contract.Result() != null);
+ Contract.EndContractBlock();
+
+ return new RatNum(this, Native.Z3_mk_real(nCtx, num, den));
+ }
+
+ ///
+ /// Create a real numeral.
+ ///
+ /// A string representing the Term value in decimal notation.
+ /// A Term with value and sort Real
+ public RatNum MkReal(string v)
+ {
+ Contract.Ensures(Contract.Result() != null);
+
+ return new RatNum(this, Native.Z3_mk_numeral(nCtx, v, RealSort.NativeObject));
+ }
+
+ ///
+ /// Create a real numeral.
+ ///
+ /// value of the numeral.
+ /// A Term with value and sort Real
+ public RatNum MkReal(int v)
+ {
+ Contract.Ensures(Contract.Result() != null);
+
+ return new RatNum(this, Native.Z3_mk_int(nCtx, v, RealSort.NativeObject));
+ }
+
+ ///
+ /// Create a real numeral.
+ ///
+ /// value of the numeral.
+ /// A Term with value and sort Real
+ public RatNum MkReal(uint v)
+ {
+ Contract.Ensures(Contract.Result() != null);
+
+ return new RatNum(this, Native.Z3_mk_unsigned_int(nCtx, v, RealSort.NativeObject));
+ }
+
+ ///
+ /// Create a real numeral.
+ ///
+ /// value of the numeral.
+ /// A Term with value and sort Real
+ public RatNum MkReal(long v)
+ {
+ Contract.Ensures(Contract.Result() != null);
+
+ return new RatNum(this, Native.Z3_mk_int64(nCtx, v, RealSort.NativeObject));
+ }
+
+ ///
+ /// Create a real numeral.
+ ///
+ /// value of the numeral.
+ /// A Term with value and sort Real
+ public RatNum MkReal(ulong v)
+ {
+ Contract.Ensures(Contract.Result() != null);
+
+ return new RatNum(this, Native.Z3_mk_unsigned_int64(nCtx, v, RealSort.NativeObject));
+ }
+ #endregion
+
+ #region Integers
+ ///
+ /// Create an integer numeral.
+ ///
+ /// A string representing the Term value in decimal notation.
+ public IntNum MkInt(string v)
+ {
+ Contract.Ensures(Contract.Result() != null);
+
+ return new IntNum(this, Native.Z3_mk_numeral(nCtx, v, IntSort.NativeObject));
+ }
+
+ ///
+ /// Create an integer numeral.
+ ///
+ /// value of the numeral.
+ /// A Term with value and sort Integer
+ public IntNum MkInt(int v)
+ {
+ Contract.Ensures(Contract.Result() != null);
+
+ return new IntNum(this, Native.Z3_mk_int(nCtx, v, IntSort.NativeObject));
+ }
+
+ ///
+ /// Create an integer numeral.
+ ///
+ /// value of the numeral.
+ /// A Term with value and sort Integer
+ public IntNum MkInt(uint v)
+ {
+ Contract.Ensures(Contract.Result() != null);
+
+ return new IntNum(this, Native.Z3_mk_unsigned_int(nCtx, v, IntSort.NativeObject));
+ }
+
+ ///
+ /// Create an integer numeral.
+ ///
+ /// value of the numeral.
+ /// A Term with value and sort Integer
+ public IntNum MkInt(long v)
+ {
+ Contract.Ensures(Contract.Result() != null);
+
+ return new IntNum(this, Native.Z3_mk_int64(nCtx, v, IntSort.NativeObject));
+ }
+
+ ///
+ /// Create an integer numeral.
+ ///
+ /// value of the numeral.
+ /// A Term with value and sort Integer
+ public IntNum MkInt(ulong v)
+ {
+ Contract.Ensures(Contract.Result() != null);
+
+ return new IntNum(this, Native.Z3_mk_unsigned_int64(nCtx, v, IntSort.NativeObject));
+ }
+ #endregion
+
+ #region Bit-vectors
+ ///
+ /// Create a bit-vector numeral.
+ ///
+ /// A string representing the value in decimal notation.
+ /// the size of the bit-vector
+ public BitVecNum MkBV(string v, uint size)
+ {
+ Contract.Ensures(Contract.Result() != null);
+
+ return (BitVecNum)MkNumeral(v, MkBitVecSort(size));
+ }
+
+ ///
+ /// Create a bit-vector numeral.
+ ///
+ /// value of the numeral.
+ /// the size of the bit-vector
+ public BitVecNum MkBV(int v, uint size)
+ {
+ Contract.Ensures(Contract.Result() != null);
+
+ return (BitVecNum)MkNumeral(v, MkBitVecSort(size));
+ }
+
+ ///
+ /// Create a bit-vector numeral.
+ ///
+ /// value of the numeral.
+ /// the size of the bit-vector
+ public BitVecNum MkBV(uint v, uint size)
+ {
+ Contract.Ensures(Contract.Result() != null);
+
+ return (BitVecNum)MkNumeral(v, MkBitVecSort(size));
+ }
+
+ ///
+ /// Create a bit-vector numeral.
+ ///
+ /// value of the numeral.
+ /// /// the size of the bit-vector
+ public BitVecNum MkBV(long v, uint size)
+ {
+ Contract.Ensures(Contract.Result() != null);
+
+ return (BitVecNum)MkNumeral(v, MkBitVecSort(size));
+ }
+
+ ///
+ /// Create a bit-vector numeral.
+ ///
+ /// value of the numeral.
+ /// the size of the bit-vector
+ public BitVecNum MkBV(ulong v, uint size)
+ {
+ Contract.Ensures(Contract.Result() != null);
+
+ return (BitVecNum)MkNumeral(v, MkBitVecSort(size));
+ }
+ #endregion
+
+ #endregion // Numerals
+
+ #region Quantifiers
+ ///
+ /// Create a universal Quantifier.
+ ///
+ ///
+ /// Creates a forall formula, where is the weight,
+ /// is an array of patterns, is an array
+ /// with the sorts of the bound variables, is an array with the
+ /// 'names' of the bound variables, and is the body of the
+ /// quantifier. Quantifiers are associated with weights indicating
+ /// the importance of using the quantifier during instantiation.
+ ///
+ /// the sorts of the bound variables.
+ /// names of the bound variables
+ /// the body of the quantifier.
+ /// quantifiers are associated with weights indicating the importance of using the quantifier during instantiation. By default, pass the weight 0.
+ /// array containing the patterns created using MkPattern.
+ /// array containing the anti-patterns created using MkPattern.
+ /// optional symbol to track quantifier.
+ /// optional symbol to track skolem constants.
+ public Quantifier MkForall(Sort[] sorts, Symbol[] names, Expr body, uint weight = 1, Pattern[] patterns = null, Expr[] noPatterns = null, Symbol quantifierID = null, Symbol skolemID = null)
+ {
+ Contract.Requires(sorts != null);
+ Contract.Requires(names != null);
+ Contract.Requires(body != null);
+ Contract.Requires(sorts.Length == names.Length);
+ Contract.Requires(Contract.ForAll(sorts, s => s != null));
+ Contract.Requires(Contract.ForAll(names, n => n != null));
+ Contract.Requires(patterns == null || Contract.ForAll(patterns, p => p != null));
+ Contract.Requires(noPatterns == null || Contract.ForAll(noPatterns, np => np != null));
+
+ Contract.Ensures(Contract.Result() != null);
+
+ return new Quantifier(this, true, sorts, names, body, weight, patterns, noPatterns, quantifierID, skolemID);
+ }
+
+
+ ///
+ /// Create a universal Quantifier.
+ ///
+ public Quantifier MkForall(Expr[] boundConstants, Expr body, uint weight = 1, Pattern[] patterns = null, Expr[] noPatterns = null, Symbol quantifierID = null, Symbol skolemID = null)
+ {
+ Contract.Requires(body != null);
+ Contract.Requires(boundConstants == null || Contract.ForAll(boundConstants, b => b != null));
+ Contract.Requires(patterns == null || Contract.ForAll(patterns, p => p != null));
+ Contract.Requires(noPatterns == null || Contract.ForAll(noPatterns, np => np != null));
+
+ Contract.Ensures(Contract.Result() != null);
+
+ return new Quantifier(this, true, boundConstants, body, weight, patterns, noPatterns, quantifierID, skolemID);
+ }
+
+ ///
+ /// Create an existential Quantifier.
+ ///
+ ///
+ public Quantifier MkExists(Sort[] sorts, Symbol[] names, Expr body, uint weight = 1, Pattern[] patterns = null, Expr[] noPatterns = null, Symbol quantifierID = null, Symbol skolemID = null)
+ {
+ Contract.Requires(sorts != null);
+ Contract.Requires(names != null);
+ Contract.Requires(body != null);
+ Contract.Requires(sorts.Length == names.Length);
+ Contract.Requires(Contract.ForAll(sorts, s => s != null));
+ Contract.Requires(Contract.ForAll(names, n => n != null));
+ Contract.Requires(patterns == null || Contract.ForAll(patterns, p => p != null));
+ Contract.Requires(noPatterns == null || Contract.ForAll(noPatterns, np => np != null));
+ Contract.Ensures(Contract.Result() != null);
+
+ return new Quantifier(this, false, sorts, names, body, weight, patterns, noPatterns, quantifierID, skolemID);
+ }
+
+ ///
+ /// Create an existential Quantifier.
+ ///
+ public Quantifier MkExists(Expr[] boundConstants, Expr body, uint weight = 1, Pattern[] patterns = null, Expr[] noPatterns = null, Symbol quantifierID = null, Symbol skolemID = null)
+ {
+ Contract.Requires(body != null);
+ Contract.Requires(boundConstants == null || Contract.ForAll(boundConstants, n => n != null));
+ Contract.Requires(patterns == null || Contract.ForAll(patterns, p => p != null));
+ Contract.Requires(noPatterns == null || Contract.ForAll(noPatterns, np => np != null));
+ Contract.Ensures(Contract.Result() != null);
+
+ return new Quantifier(this, false, boundConstants, body, weight, patterns, noPatterns, quantifierID, skolemID);
+ }
+
+
+ ///
+ /// Create a Quantifier.
+ ///
+ public Quantifier MkQuantifier(bool universal, Sort[] sorts, Symbol[] names, Expr body, uint weight = 1, Pattern[] patterns = null, Expr[] noPatterns = null, Symbol quantifierID = null, Symbol skolemID = null)
+ {
+ Contract.Requires(body != null);
+ Contract.Requires(names != null);
+ Contract.Requires(sorts != null);
+ Contract.Requires(sorts.Length == names.Length);
+ Contract.Requires(Contract.ForAll(sorts, s => s != null));
+ Contract.Requires(Contract.ForAll(names, n => n != null));
+ Contract.Requires(patterns == null || Contract.ForAll(patterns, p => p != null));
+ Contract.Requires(noPatterns == null || Contract.ForAll(noPatterns, np => np != null));
+
+ Contract.Ensures(Contract.Result() != null);
+
+ if (universal)
+ return MkForall(sorts, names, body, weight, patterns, noPatterns, quantifierID, skolemID);
+ else
+ return MkExists(sorts, names, body, weight, patterns, noPatterns, quantifierID, skolemID);
+ }
+
+
+ ///
+ /// Create a Quantifier.
+ ///
+ public Quantifier MkQuantifier(bool universal, Expr[] boundConstants, Expr body, uint weight = 1, Pattern[] patterns = null, Expr[] noPatterns = null, Symbol quantifierID = null, Symbol skolemID = null)
+ {
+ Contract.Requires(body != null);
+ Contract.Requires(boundConstants == null || Contract.ForAll(boundConstants, n => n != null));
+ Contract.Requires(patterns == null || Contract.ForAll(patterns, p => p != null));
+ Contract.Requires(noPatterns == null || Contract.ForAll(noPatterns, np => np != null));
+
+ Contract.Ensures(Contract.Result() != null);
+
+ if (universal)
+ return MkForall(boundConstants, body, weight, patterns, noPatterns, quantifierID, skolemID);
+ else
+ return MkExists(boundConstants, body, weight, patterns, noPatterns, quantifierID, skolemID);
+ }
+
+ #endregion
+
+ #endregion // Expr
+
+ #region Options
+ ///
+ /// Selects the format used for pretty-printing expressions.
+ ///
+ ///
+ /// The default mode for pretty printing expressions is to produce
+ /// SMT-LIB style output where common subexpressions are printed
+ /// at each occurrence. The mode is called Z3_PRINT_SMTLIB_FULL.
+ /// To print shared common subexpressions only once,
+ /// use the Z3_PRINT_LOW_LEVEL mode.
+ /// To print in way that conforms to SMT-LIB standards and uses let
+ /// expressions to share common sub-expressions use Z3_PRINT_SMTLIB_COMPLIANT.
+ ///
+ ///
+ ///
+ ///
+ ///
+ public Z3_ast_print_mode PrintMode
+ {
+ set { Native.Z3_set_ast_print_mode(nCtx, (uint)value); }
+ }
+ #endregion
+
+ #region SMT Files & Strings
+ ///
+ /// Convert a benchmark into an SMT-LIB formatted string.
+ ///
+ /// Name of the benchmark. The argument is optional.
+ /// The benchmark logic.
+ /// The status string (sat, unsat, or unknown)
+ /// Other attributes, such as source, difficulty or category.
+ /// Auxiliary assumptions.
+ /// Formula to be checked for consistency in conjunction with assumptions.
+ /// A string representation of the benchmark.
+ public string BenchmarkToSMTString(string name, string logic, string status, string attributes,
+ BoolExpr[] assumptions, BoolExpr formula)
+ {
+ Contract.Requires(assumptions != null);
+ Contract.Requires(formula != null);
+ Contract.Ensures(Contract.Result() != null);
+
+ return Native.Z3_benchmark_to_smtlib_string(nCtx, name, logic, status, attributes,
+ (uint)assumptions.Length, AST.ArrayToNative(assumptions),
+ formula.NativeObject);
+ }
+
+ ///
+ /// Parse the given string using the SMT-LIB parser.
+ ///
+ ///
+ /// The symbol table of the parser can be initialized using the given sorts and declarations.
+ /// The symbols in the arrays and
+ /// don't need to match the names of the sorts and declarations in the arrays
+ /// and . This is a useful feature since we can use arbitrary names to
+ /// reference sorts and declarations.
+ ///
+ public void ParseSMTLIBString(string str, Symbol[] sortNames = null, Sort[] sorts = null, Symbol[] declNames = null, FuncDecl[] decls = null)
+ {
+ uint csn = Symbol.ArrayLength(sortNames);
+ uint cs = Sort.ArrayLength(sorts);
+ uint cdn = Symbol.ArrayLength(declNames);
+ uint cd = AST.ArrayLength(decls);
+ if (csn != cs || cdn != cd)
+ throw new Z3Exception("Argument size mismatch");
+ Native.Z3_parse_smtlib_string(nCtx, str,
+ AST.ArrayLength(sorts), Symbol.ArrayToNative(sortNames), AST.ArrayToNative(sorts),
+ AST.ArrayLength(decls), Symbol.ArrayToNative(declNames), AST.ArrayToNative(decls));
+ }
+
+ ///
+ /// Parse the given file using the SMT-LIB parser.
+ ///
+ ///
+ public void ParseSMTLIBFile(string fileName, Symbol[] sortNames = null, Sort[] sorts = null, Symbol[] declNames = null, FuncDecl[] decls = null)
+ {
+ uint csn = Symbol.ArrayLength(sortNames);
+ uint cs = Sort.ArrayLength(sorts);
+ uint cdn = Symbol.ArrayLength(declNames);
+ uint cd = AST.ArrayLength(decls);
+ if (csn != cs || cdn != cd)
+ throw new Z3Exception("Argument size mismatch");
+ Native.Z3_parse_smtlib_file(nCtx, fileName,
+ AST.ArrayLength(sorts), Symbol.ArrayToNative(sortNames), AST.ArrayToNative(sorts),
+ AST.ArrayLength(decls), Symbol.ArrayToNative(declNames), AST.ArrayToNative(decls));
+ }
+
+ ///
+ /// The number of SMTLIB formulas parsed by the last call to ParseSMTLIBString or ParseSMTLIBFile.
+ ///
+ public uint NumSMTLIBFormulas { get { return Native.Z3_get_smtlib_num_formulas(nCtx); } }
+
+ ///
+ /// The formulas parsed by the last call to ParseSMTLIBString or ParseSMTLIBFile.
+ ///
+ public BoolExpr[] SMTLIBFormulas
+ {
+ get
+ {
+ Contract.Ensures(Contract.Result() != null);
+
+ uint n = NumSMTLIBFormulas;
+ BoolExpr[] res = new BoolExpr[n];
+ for (uint i = 0; i < n; i++)
+ res[i] = (BoolExpr)Expr.Create(this, Native.Z3_get_smtlib_formula(nCtx, i));
+ return res;
+ }
+ }
+
+ ///
+ /// The number of SMTLIB assumptions parsed by the last call to ParseSMTLIBString or ParseSMTLIBFile.
+ ///
+ public uint NumSMTLIBAssumptions { get { return Native.Z3_get_smtlib_num_assumptions(nCtx); } }
+
+ ///
+ /// The assumptions parsed by the last call to ParseSMTLIBString or ParseSMTLIBFile.
+ ///
+ public BoolExpr[] SMTLIBAssumptions
+ {
+ get
+ {
+ Contract.Ensures(Contract.Result() != null);
+
+ uint n = NumSMTLIBAssumptions;
+ BoolExpr[] res = new BoolExpr[n];
+ for (uint i = 0; i < n; i++)
+ res[i] = (BoolExpr)Expr.Create(this, Native.Z3_get_smtlib_assumption(nCtx, i));
+ return res;
+ }
+ }
+
+ ///
+ /// The number of SMTLIB declarations parsed by the last call to ParseSMTLIBString or ParseSMTLIBFile.
+ ///
+ public uint NumSMTLIBDecls { get { return Native.Z3_get_smtlib_num_decls(nCtx); } }
+
+ ///
+ /// The declarations parsed by the last call to ParseSMTLIBString or ParseSMTLIBFile.
+ ///
+ public FuncDecl[] SMTLIBDecls
+ {
+ get
+ {
+ Contract.Ensures(Contract.Result() != null);
+
+ uint n = NumSMTLIBDecls;
+ FuncDecl[] res = new FuncDecl[n];
+ for (uint i = 0; i < n; i++)
+ res[i] = new FuncDecl(this, Native.Z3_get_smtlib_decl(nCtx, i));
+ return res;
+ }
+ }
+
+ ///
+ /// The number of SMTLIB sorts parsed by the last call to ParseSMTLIBString or ParseSMTLIBFile.
+ ///
+ public uint NumSMTLIBSorts { get { return Native.Z3_get_smtlib_num_sorts(nCtx); } }
+
+ ///
+ /// The declarations parsed by the last call to ParseSMTLIBString or ParseSMTLIBFile.
+ ///
+ public Sort[] SMTLIBSorts
+ {
+ get
+ {
+ Contract.Ensures(Contract.Result() != null);
+
+ uint n = NumSMTLIBSorts;
+ Sort[] res = new Sort[n];
+ for (uint i = 0; i < n; i++)
+ res[i] = Sort.Create(this, Native.Z3_get_smtlib_sort(nCtx, i));
+ return res;
+ }
+ }
+
+ ///
+ /// Parse the given string using the SMT-LIB2 parser.
+ ///
+ ///
+ /// A conjunction of assertions in the scope (up to push/pop) at the end of the string.
+ public BoolExpr ParseSMTLIB2String(string str, Symbol[] sortNames = null, Sort[] sorts = null, Symbol[] declNames = null, FuncDecl[] decls = null)
+ {
+ Contract.Ensures(Contract.Result() != null);
+
+ uint csn = Symbol.ArrayLength(sortNames);
+ uint cs = Sort.ArrayLength(sorts);
+ uint cdn = Symbol.ArrayLength(declNames);
+ uint cd = AST.ArrayLength(decls);
+ if (csn != cs || cdn != cd)
+ throw new Z3Exception("Argument size mismatch");
+ return (BoolExpr)Expr.Create(this, Native.Z3_parse_smtlib2_string(nCtx, str,
+ AST.ArrayLength(sorts), Symbol.ArrayToNative(sortNames), AST.ArrayToNative(sorts),
+ AST.ArrayLength(decls), Symbol.ArrayToNative(declNames), AST.ArrayToNative(decls)));
+ }
+
+ ///
+ /// Parse the given file using the SMT-LIB2 parser.
+ ///
+ ///
+ public BoolExpr ParseSMTLIB2File(string fileName, Symbol[] sortNames = null, Sort[] sorts = null, Symbol[] declNames = null, FuncDecl[] decls = null)
+ {
+ Contract.Ensures(Contract.Result() != null);
+
+ uint csn = Symbol.ArrayLength(sortNames);
+ uint cs = Sort.ArrayLength(sorts);
+ uint cdn = Symbol.ArrayLength(declNames);
+ uint cd = AST.ArrayLength(decls);
+ if (csn != cs || cdn != cd)
+ throw new Z3Exception("Argument size mismatch");
+ return (BoolExpr)Expr.Create(this, Native.Z3_parse_smtlib2_file(nCtx, fileName,
+ AST.ArrayLength(sorts), Symbol.ArrayToNative(sortNames), AST.ArrayToNative(sorts),
+ AST.ArrayLength(decls), Symbol.ArrayToNative(declNames), AST.ArrayToNative(decls)));
+ }
+ #endregion
+
+ #region Native Parser
+ ///
+ /// Parse the given string using the Z3 native parser.
+ ///
+ /// A conjunction of asserts made in .
+ public Expr ParseZ3String(string str)
+ {
+ Contract.Ensures(Contract.Result() != null);
+
+ return Expr.Create(this, Native.Z3_parse_z3_string(nCtx, str));
+ }
+
+ ///
+ /// Parse the given file using the Z3 native parser.
+ ///
+ /// A conjunction of asserts made in the file.
+ public Expr ParseZ3File(string fileName)
+ {
+ Contract.Ensures(Contract.Result() != null);
+
+ return Expr.Create(this, Native.Z3_parse_z3_file(nCtx, fileName));
+ }
+ #endregion
+
+ #region Goals
+ ///
+ /// Creates a new Goal.
+ ///
+ ///
+ /// Note that the Context must have been created with proof generation support if
+ /// is set to true here.
+ ///
+ /// Indicates whether model generation should be enabled.
+ /// Indicates whether unsat core generation should be enabled.
+ /// Indicates whether proof generation should be enabled.
+ public Goal MkGoal(bool models = true, bool unsatCores = false, bool proofs = false)
+ {
+ Contract.Ensures(Contract.Result() != null);
+
+ return new Goal(this, models, unsatCores, proofs);
+ }
+ #endregion
+
+ #region ParameterSets
+ ///
+ /// Creates a new ParameterSet.
+ ///
+ public Params MkParams()
+ {
+ Contract.Ensures(Contract.Result() != null);
+
+ return new Params(this);
+ }
+ #endregion
+
+ #region Tactics
+ ///
+ /// The number of supported tactics.
+ ///
+ public uint NumTactics
+ {
+ get { return Native.Z3_get_num_tactics(nCtx); }
+ }
+
+ ///
+ /// The names of all supported tactics.
+ ///
+ public string[] TacticNames
+ {
+ get
+ {
+ Contract.Ensures(Contract.Result() != null);
+
+ uint n = NumTactics;
+ string[] res = new string[n];
+ for (uint i = 0; i < n; i++)
+ res[i] = Native.Z3_get_tactic_name(nCtx, i);
+ return res;
+ }
+ }
+
+ ///
+ /// Returns a string containing a description of the tactic with the given name.
+ ///
+ public string TacticDescription(string name)
+ {
+ Contract.Ensures(Contract.Result() != null);
+
+ return Native.Z3_tactic_get_descr(nCtx, name);
+ }
+
+ ///
+ /// Creates a new Tactic.
+ ///
+ public Tactic MkTactic(string name)
+ {
+ Contract.Ensures(Contract.Result() != null);
+
+ return new Tactic(this, name);
+ }
+
+ ///
+ /// Create a tactic that applies to a Goal and
+ /// then to every subgoal produced by .
+ ///
+ public Tactic AndThen(Tactic t1, Tactic t2, params Tactic[] ts)
+ {
+ Contract.Requires(t1 != null);
+ Contract.Requires(t2 != null);
+ Contract.Requires(ts == null || Contract.ForAll(0, ts.Length, j => ts[j] != null));
+ Contract.Ensures(Contract.Result() != null);
+
+
+ CheckContextMatch(t1);
+ CheckContextMatch(t2);
+ CheckContextMatch(ts);
+
+ IntPtr last = IntPtr.Zero;
+ if (ts != null && ts.Length > 0)
+ {
+ last = ts[ts.Length - 1].NativeObject;
+ for (int i = ts.Length - 2; i >= 0; i--)
+ last = Native.Z3_tactic_and_then(nCtx, ts[i].NativeObject, last);
+ }
+ if (last != IntPtr.Zero)
+ {
+ last = Native.Z3_tactic_and_then(nCtx, t2.NativeObject, last);
+ return new Tactic(this, Native.Z3_tactic_and_then(nCtx, t1.NativeObject, last));
+ }
+ else
+ return new Tactic(this, Native.Z3_tactic_and_then(nCtx, t1.NativeObject, t2.NativeObject));
+ }
+
+ ///
+ /// Create a tactic that applies to a Goal and
+ /// then to every subgoal produced by .
+ ///
+ ///
+ /// Shorthand for AndThen.
+ ///
+ public Tactic Then(Tactic t1, Tactic t2, params Tactic[] ts)
+ {
+ Contract.Requires(t1 != null);
+ Contract.Requires(t2 != null);
+ Contract.Requires(ts == null || Contract.ForAll(0, ts.Length, j => ts[j] != null));
+ Contract.Ensures(Contract.Result() != null);
+
+ return AndThen(t1, t2, ts);
+ }
+
+ ///
+ /// Create a tactic that first applies to a Goal and
+ /// if it fails then returns the result of applied to the Goal.
+ ///
+ public Tactic OrElse(Tactic t1, Tactic t2)
+ {
+ Contract.Requires(t1 != null);
+ Contract.Requires(t2 != null);
+ Contract.Ensures(Contract.Result() != null);
+
+ CheckContextMatch(t1);
+ CheckContextMatch(t2);
+ return new Tactic(this, Native.Z3_tactic_or_else(nCtx, t1.NativeObject, t2.NativeObject));
+ }
+
+ ///
+ /// Create a tactic that applies to a goal for milliseconds.
+ ///
+ ///
+ /// If does not terminate within milliseconds, then it fails.
+ ///
+ public Tactic TryFor(Tactic t, uint ms)
+ {
+ Contract.Requires(t != null);
+ Contract.Ensures(Contract.Result() != null);
+
+ CheckContextMatch(t);
+ return new Tactic(this, Native.Z3_tactic_try_for(nCtx, t.NativeObject, ms));
+ }
+
+ ///
+ /// Create a tactic that applies to a given goal if the probe
+ /// evaluates to true.
+ ///
+ ///
+ /// If evaluates to false, then the new tactic behaves like the skip tactic.
+ ///
+ public Tactic When(Probe p, Tactic t)
+ {
+ Contract.Requires(p != null);
+ Contract.Requires(t != null);
+ Contract.Ensures(Contract.Result() != null);
+
+ CheckContextMatch(t);
+ CheckContextMatch(p);
+ return new Tactic(this, Native.Z3_tactic_when(nCtx, p.NativeObject, t.NativeObject));
+ }
+
+ ///
+ /// Create a tactic that applies to a given goal if the probe
+ /// evaluates to true and otherwise.
+ ///
+ public Tactic Cond(Probe p, Tactic t1, Tactic t2)
+ {
+ Contract.Requires(p != null);
+ Contract.Requires(t1 != null);
+ Contract.Requires(t2 != null);
+ Contract.Ensures(Contract.Result() != null);
+
+ CheckContextMatch(p);
+ CheckContextMatch(t1);
+ CheckContextMatch(t2);
+ return new Tactic(this, Native.Z3_tactic_cond(nCtx, p.NativeObject, t1.NativeObject, t2.NativeObject));
+ }
+
+ ///
+ /// Create a tactic that keeps applying until the goal is not
+ /// modified anymore or the maximum number of iterations is reached.
+ ///
+ public Tactic Repeat(Tactic t, uint max = uint.MaxValue)
+ {
+ Contract.Requires(t != null);
+ Contract.Ensures(Contract.Result() != null);
+
+ CheckContextMatch(t);
+ return new Tactic(this, Native.Z3_tactic_repeat(nCtx, t.NativeObject, max));
+ }
+
+ ///
+ /// Create a tactic that just returns the given goal.
+ ///
+ public Tactic Skip()
+ {
+ Contract.Ensures(Contract.Result() != null);
+
+ return new Tactic(this, Native.Z3_tactic_skip(nCtx));
+ }
+
+ ///
+ /// Create a tactic always fails.
+ ///
+ public Tactic Fail()
+ {
+ Contract.Ensures(Contract.Result() != null);
+
+ return new Tactic(this, Native.Z3_tactic_fail(nCtx));
+ }
+
+ ///
+ /// Create a tactic that fails if the probe evaluates to false.
+ ///
+ public Tactic FailIf(Probe p)
+ {
+ Contract.Requires(p != null);
+ Contract.Ensures(Contract.Result() != null);
+
+ CheckContextMatch(p);
+ return new Tactic(this, Native.Z3_tactic_fail_if(nCtx, p.NativeObject));
+ }
+
+ ///
+ /// Create a tactic that fails if the goal is not triviall satisfiable (i.e., empty)
+ /// or trivially unsatisfiable (i.e., contains `false').
+ ///
+ public Tactic FailIfNotDecided()
+ {
+ Contract.Ensures(Contract.Result() != null);
+
+ return new Tactic(this, Native.Z3_tactic_fail_if_not_decided(nCtx));
+ }
+
+ ///
+ /// Create a tactic that applies using the given set of parameters .
+ ///
+ public Tactic UsingParams(Tactic t, Params p)
+ {
+ Contract.Requires(t != null);
+ Contract.Requires(p != null);
+ Contract.Ensures(Contract.Result() != null);
+
+ CheckContextMatch(t);
+ CheckContextMatch(p);
+ return new Tactic(this, Native.Z3_tactic_using_params(nCtx, t.NativeObject, p.NativeObject));
+ }
+
+ ///
+ /// Create a tactic that applies using the given set of parameters .
+ ///
+ /// Alias for UsingParams
+ public Tactic With(Tactic t, Params p)
+ {
+ Contract.Requires(t != null);
+ Contract.Requires(p != null);
+ Contract.Ensures(Contract.Result() != null);
+
+ return UsingParams(t, p);
+ }
+
+ ///
+ /// Create a tactic that applies the given tactics in parallel.
+ ///
+ public Tactic ParOr(params Tactic[] t)
+ {
+ Contract.Requires(t == null || Contract.ForAll(t, tactic => tactic != null));
+ Contract.Ensures(Contract.Result() != null);
+
+ CheckContextMatch(t);
+ return new Tactic(this, Native.Z3_tactic_par_or(nCtx, Tactic.ArrayLength(t), Tactic.ArrayToNative(t)));
+ }
+
+ ///
+ /// Create a tactic that applies to a given goal and then
+ /// to every subgoal produced by . The subgoals are processed in parallel.
+ ///
+ public Tactic ParAndThen(Tactic t1, Tactic t2)
+ {
+ Contract.Requires(t1 != null);
+ Contract.Requires(t2 != null);
+ Contract.Ensures(Contract.Result() != null);
+
+ CheckContextMatch(t1);
+ CheckContextMatch(t2);
+ return new Tactic(this, Native.Z3_tactic_par_and_then(nCtx, t1.NativeObject, t2.NativeObject));
+ }
+
+ ///
+ /// Interrupt the execution of a Z3 procedure.
+ ///
+ /// This procedure can be used to interrupt: solvers, simplifiers and tactics.
+ public void Interrupt()
+ {
+ Native.Z3_interrupt(nCtx);
+ }
+ #endregion
+
+ #region Probes
+ ///
+ /// The number of supported Probes.
+ ///
+ public uint NumProbes
+ {
+ get { return Native.Z3_get_num_probes(nCtx); }
+ }
+
+ ///
+ /// The names of all supported Probes.
+ ///
+ public string[] ProbeNames
+ {
+ get
+ {
+ Contract.Ensures(Contract.Result() != null);
+
+ uint n = NumProbes;
+ string[] res = new string[n];
+ for (uint i = 0; i < n; i++)
+ res[i] = Native.Z3_get_probe_name(nCtx, i);
+ return res;
+ }
+ }
+
+ ///
+ /// Returns a string containing a description of the probe with the given name.
+ ///
+ public string ProbeDescription(string name)
+ {
+ Contract.Ensures(Contract.Result() != null);
+
+ return Native.Z3_probe_get_descr(nCtx, name);
+ }
+
+ ///
+ /// Creates a new Probe.
+ ///
+ public Probe MkProbe(string name)
+ {
+ Contract.Ensures(Contract.Result() != null);
+
+ return new Probe(this, name);
+ }
+
+ ///
+ /// Create a probe that always evaluates to .
+ ///
+ public Probe Const(double val)
+ {
+ Contract.Ensures(Contract.Result() != null);
+
+ return new Probe(this, Native.Z3_probe_const(nCtx, val));
+ }
+
+ ///
+ /// Create a probe that evaluates to "true" when the value returned by
+ /// is less than the value returned by
+ ///
+ public Probe Lt(Probe p1, Probe p2)
+ {
+ Contract.Requires(p1 != null);
+ Contract.Requires(p2 != null);
+ Contract.Ensures(Contract.Result() != null);
+
+ CheckContextMatch(p1);
+ CheckContextMatch(p2);
+ return new Probe(this, Native.Z3_probe_lt(nCtx, p1.NativeObject, p2.NativeObject));
+ }
+
+ ///
+ /// Create a probe that evaluates to "true" when the value returned by
+ /// is greater than the value returned by
+ ///
+ public Probe Gt(Probe p1, Probe p2)
+ {
+ Contract.Requires(p1 != null);
+ Contract.Requires(p2 != null);
+ Contract.Ensures(Contract.Result() != null);
+
+ CheckContextMatch(p1);
+ CheckContextMatch(p2);
+ return new Probe(this, Native.Z3_probe_gt(nCtx, p1.NativeObject, p2.NativeObject));
+ }
+
+ ///
+ /// Create a probe that evaluates to "true" when the value returned by
+ /// is less than or equal the value returned by
+ ///
+ public Probe Le(Probe p1, Probe p2)
+ {
+ Contract.Requires(p1 != null);
+ Contract.Requires(p2 != null);
+ Contract.Ensures(Contract.Result() != null);
+
+ CheckContextMatch(p1);
+ CheckContextMatch(p2);
+ return new Probe(this, Native.Z3_probe_le(nCtx, p1.NativeObject, p2.NativeObject));
+ }
+
+ ///
+ /// Create a probe that evaluates to "true" when the value returned by
+ /// is greater than or equal the value returned by
+ ///
+ public Probe Ge(Probe p1, Probe p2)
+ {
+ Contract.Requires(p1 != null);
+ Contract.Requires(p2 != null);
+ Contract.Ensures(Contract.Result() != null);
+
+ CheckContextMatch(p1);
+ CheckContextMatch(p2);
+ return new Probe(this, Native.Z3_probe_ge(nCtx, p1.NativeObject, p2.NativeObject));
+ }
+
+ ///
+ /// Create a probe that evaluates to "true" when the value returned by
+ /// is equal to the value returned by
+ ///
+ public Probe Eq(Probe p1, Probe p2)
+ {
+ Contract.Requires(p1 != null);
+ Contract.Requires(p2 != null);
+ Contract.Ensures(Contract.Result() != null);
+
+ CheckContextMatch(p1);
+ CheckContextMatch(p2);
+ return new Probe(this, Native.Z3_probe_eq(nCtx, p1.NativeObject, p2.NativeObject));
+ }
+
+ ///
+ /// Create a probe that evaluates to "true" when the value
+ /// and evaluate to "true".
+ ///
+ public Probe And(Probe p1, Probe p2)
+ {
+ Contract.Requires(p1 != null);
+ Contract.Requires(p2 != null);
+ Contract.Ensures(Contract.Result() != null);
+
+ CheckContextMatch(p1);
+ CheckContextMatch(p2);
+ return new Probe(this, Native.Z3_probe_and(nCtx, p1.NativeObject, p2.NativeObject));
+ }
+
+ ///
+ /// Create a probe that evaluates to "true" when the value
+ /// or evaluate to "true".
+ ///
+ public Probe Or(Probe p1, Probe p2)
+ {
+ Contract.Requires(p1 != null);
+ Contract.Requires(p2 != null);
+ Contract.Ensures(Contract.Result() != null);
+
+ CheckContextMatch(p1);
+ CheckContextMatch(p2);
+ return new Probe(this, Native.Z3_probe_or(nCtx, p1.NativeObject, p2.NativeObject));
+ }
+
+ ///
+ /// Create a probe that evaluates to "true" when the value
+ /// does not evaluate to "true".
+ ///
+ public Probe Not(Probe p)
+ {
+ Contract.Requires(p != null);
+ Contract.Ensures(Contract.Result() != null);
+
+ CheckContextMatch(p);
+ return new Probe(this, Native.Z3_probe_not(nCtx, p.NativeObject));
+ }
+ #endregion
+
+ #region Solvers
+ ///
+ /// Creates a new (incremental) solver.
+ ///
+ ///
+ /// This solver also uses a set of builtin tactics for handling the first
+ /// check-sat command, and check-sat commands that take more than a given
+ /// number of milliseconds to be solved.
+ ///
+ public Solver MkSolver(Symbol logic = null)
+ {
+ Contract.Ensures(Contract.Result() != null);
+
+ if (logic == null)
+ return new Solver(this, Native.Z3_mk_solver(nCtx));
+ else
+ return new Solver(this, Native.Z3_mk_solver_for_logic(nCtx, logic.NativeObject));
+ }
+
+ ///
+ /// Creates a new (incremental) solver.
+ ///
+ ///
+ public Solver MkSolver(string logic)
+ {
+ Contract.Ensures(Contract.Result() != null);
+
+ return MkSolver(MkSymbol(logic));
+ }
+
+ ///
+ /// Creates a new (incremental) solver.
+ ///
+ public Solver MkSimpleSolver()
+ {
+ Contract.Ensures(Contract.Result() != null);
+
+ return new Solver(this, Native.Z3_mk_simple_solver(nCtx));
+ }
+
+ ///
+ /// Creates a solver that is implemented using the given tactic.
+ ///
+ ///
+ /// The solver supports the commands Push and Pop, but it
+ /// will always solve each check from scratch.
+ ///
+ public Solver MkSolver(Tactic t)
+ {
+ Contract.Requires(t != null);
+ Contract.Ensures(Contract.Result() != null);
+
+ return new Solver(this, Native.Z3_mk_solver_from_tactic(nCtx, t.NativeObject));
+ }
+ #endregion
+
+ #region Fixedpoints
+ ///
+ /// Create a Fixedpoint context.
+ ///
+ public Fixedpoint MkFixedpoint()
+ {
+ Contract.Ensures(Contract.Result() != null);
+
+ return new Fixedpoint(this);
+ }
+ #endregion
+
+
+ #region Miscellaneous
+ ///
+ /// Wraps an AST.
+ ///
+ /// This function is used for transitions between native and
+ /// managed objects. Note that must be a
+ /// native object obtained from Z3 (e.g., through )
+ /// and that it must have a correct reference count (see e.g.,
+ /// .
+ ///
+ /// The native pointer to wrap.
+ public AST WrapAST(IntPtr nativeObject)
+ {
+ Contract.Ensures(Contract.Result() != null);
+ return AST.Create(this, nativeObject);
+ }
+
+ ///
+ /// Unwraps an AST.
+ ///
+ /// This function is used for transitions between native and
+ /// managed objects. It returns the native pointer to the AST. Note that
+ /// AST objects are reference counted and unwrapping an AST disables automatic
+ /// reference counting, i.e., all references to the IntPtr that is returned
+ /// must be handled externally and through native calls (see e.g.,
+ /// ).
+ ///
+ /// The AST to unwrap.
+ public IntPtr UnwrapAST(AST a)
+ {
+ return a.NativeObject;
+ }
+
+ ///
+ /// Return a string describing all available parameters to Expr.Simplify.
+ ///
+ public string SimplifyHelp()
+ {
+ Contract.Ensures(Contract.Result() != null);
+
+ return Native.Z3_simplify_get_help(nCtx);
+ }
+
+ ///
+ /// Retrieves parameter descriptions for simplifier.
+ ///
+ public ParamDescrs SimplifyParameterDescriptions
+ {
+ get
+ {
+ return new ParamDescrs(this, Native.Z3_simplify_get_param_descrs(nCtx));
+ }
+ }
+
+
+ ///
+ /// Enable/disable printing of warning messages to the console.
+ ///
+ /// Note that this function is static and effects the behaviour of
+ /// all contexts globally.
+ public static void ToggleWarningMessages(bool enabled)
+ {
+ Native.Z3_toggle_warning_messages((enabled) ? 1 : 0);
+ }
+ #endregion
+
+ #region Error Handling
+ /////
+ ///// A delegate which is executed when an error is raised.
+ /////
+ /////
+ ///// Note that it is possible for memory leaks to occur if error handlers
+ ///// throw exceptions.
+ /////
+ //public delegate void ErrorHandler(Context ctx, Z3_error_code errorCode, string errorString);
+
+ /////
+ ///// The OnError event.
+ /////
+ //public event ErrorHandler OnError = null;
+ #endregion
+
+ #region Parameters
+ ///
+ /// Update a mutable configuration parameter.
+ ///
+ ///
+ /// The list of all configuration parameters can be obtained using the Z3 executable:
+ /// z3.exe -ini?
+ /// Only a few configuration parameters are mutable once the context is created.
+ /// An exception is thrown when trying to modify an immutable parameter.
+ ///
+ ///
+ public void UpdateParamValue(string id, string value)
+ {
+ Native.Z3_update_param_value(nCtx, id, value);
+ }
+
+ ///
+ /// Get a configuration parameter.
+ ///
+ ///
+ /// Returns null if the parameter value does not exist.
+ ///
+ ///
+ public string GetParamValue(string id)
+ {
+ IntPtr res = IntPtr.Zero;
+ int r = Native.Z3_get_param_value(nCtx, id, out res);
+ if (r == (int)Z3_lbool.Z3_L_FALSE)
+ return null;
+ else
+ return Marshal.PtrToStringAnsi(res);
+ }
+
+ #endregion
+
+ #region Internal
+ internal IntPtr m_ctx = IntPtr.Zero;
+ internal Native.Z3_error_handler m_n_err_handler = null;
+ internal IntPtr nCtx { get { return m_ctx; } }
+
+ internal void NativeErrorHandler(IntPtr ctx, Z3_error_code errorCode)
+ {
+ // Do-nothing error handler. The wrappers in Z3.Native will throw exceptions upon errors.
+ }
+
+ internal void InitContext()
+ {
+ PrintMode = Z3_ast_print_mode.Z3_PRINT_SMTLIB2_COMPLIANT;
+ m_n_err_handler = new Native.Z3_error_handler(NativeErrorHandler); // keep reference so it doesn't get collected.
+ Native.Z3_set_error_handler(m_ctx, m_n_err_handler);
+ GC.SuppressFinalize(this);
+ }
+
+ [Pure]
+ internal void CheckContextMatch(Z3Object other)
+ {
+ Contract.Requires(other != null);
+
+ if (!ReferenceEquals(this, other.Context))
+ throw new Z3Exception("Context mismatch");
+ }
+
+ [Pure]
+ internal void CheckContextMatch(Z3Object[] arr)
+ {
+ Contract.Requires(arr == null || Contract.ForAll(arr, a => a != null));
+
+ if (arr != null)
+ {
+ foreach (Z3Object a in arr)
+ {
+ Contract.Assert(a != null); // It was an assume, now we added the precondition, and we made it into an assert
+ CheckContextMatch(a);
+ }
+ }
+ }
+
+ [ContractInvariantMethod]
+ private void ObjectInvariant()
+ {
+ Contract.Invariant(m_AST_DRQ != null);
+ Contract.Invariant(m_ASTMap_DRQ != null);
+ Contract.Invariant(m_ASTVector_DRQ != null);
+ Contract.Invariant(m_ApplyResult_DRQ != null);
+ Contract.Invariant(m_FuncEntry_DRQ != null);
+ Contract.Invariant(m_FuncInterp_DRQ != null);
+ Contract.Invariant(m_Goal_DRQ != null);
+ Contract.Invariant(m_Model_DRQ != null);
+ Contract.Invariant(m_Params_DRQ != null);
+ Contract.Invariant(m_ParamDescrs_DRQ != null);
+ Contract.Invariant(m_Probe_DRQ != null);
+ Contract.Invariant(m_Solver_DRQ != null);
+ Contract.Invariant(m_Statistics_DRQ != null);
+ Contract.Invariant(m_Tactic_DRQ != null);
+ Contract.Invariant(m_Fixedpoint_DRQ != null);
+ }
+
+ readonly private AST.DecRefQueue m_AST_DRQ = new AST.DecRefQueue();
+ readonly private ASTMap.DecRefQueue m_ASTMap_DRQ = new ASTMap.DecRefQueue();
+ readonly private ASTVector.DecRefQueue m_ASTVector_DRQ = new ASTVector.DecRefQueue();
+ readonly private ApplyResult.DecRefQueue m_ApplyResult_DRQ = new ApplyResult.DecRefQueue();
+ readonly private FuncInterp.Entry.DecRefQueue m_FuncEntry_DRQ = new FuncInterp.Entry.DecRefQueue();
+ readonly private FuncInterp.DecRefQueue m_FuncInterp_DRQ = new FuncInterp.DecRefQueue();
+ readonly private Goal.DecRefQueue m_Goal_DRQ = new Goal.DecRefQueue();
+ readonly private Model.DecRefQueue m_Model_DRQ = new Model.DecRefQueue();
+ readonly private Params.DecRefQueue m_Params_DRQ = new Params.DecRefQueue();
+ readonly private ParamDescrs.DecRefQueue m_ParamDescrs_DRQ = new ParamDescrs.DecRefQueue();
+ readonly private Probe.DecRefQueue m_Probe_DRQ = new Probe.DecRefQueue();
+ readonly private Solver.DecRefQueue m_Solver_DRQ = new Solver.DecRefQueue();
+ readonly private Statistics.DecRefQueue m_Statistics_DRQ = new Statistics.DecRefQueue();
+ readonly private Tactic.DecRefQueue m_Tactic_DRQ = new Tactic.DecRefQueue();
+ readonly private Fixedpoint.DecRefQueue m_Fixedpoint_DRQ = new Fixedpoint.DecRefQueue();
+
+ internal AST.DecRefQueue AST_DRQ { get { Contract.Ensures(Contract.Result() != null); return m_AST_DRQ; } }
+ internal ASTMap.DecRefQueue ASTMap_DRQ { get { Contract.Ensures(Contract.Result() != null); return m_ASTMap_DRQ; } }
+ internal ASTVector.DecRefQueue ASTVector_DRQ { get { Contract.Ensures(Contract.Result() != null); return m_ASTVector_DRQ; } }
+ internal ApplyResult.DecRefQueue ApplyResult_DRQ { get { Contract.Ensures(Contract.Result() != null); return m_ApplyResult_DRQ; } }
+ internal FuncInterp.Entry.DecRefQueue FuncEntry_DRQ { get { Contract.Ensures(Contract.Result() != null); return m_FuncEntry_DRQ; } }
+ internal FuncInterp.DecRefQueue FuncInterp_DRQ { get { Contract.Ensures(Contract.Result() != null); return m_FuncInterp_DRQ; } }
+ internal Goal.DecRefQueue Goal_DRQ { get { Contract.Ensures(Contract.Result() != null); return m_Goal_DRQ; } }
+ internal Model.DecRefQueue Model_DRQ { get { Contract.Ensures(Contract.Result() != null); return m_Model_DRQ; } }
+ internal Params.DecRefQueue Params_DRQ { get { Contract.Ensures(Contract.Result() != null); return m_Params_DRQ; } }
+ internal ParamDescrs.DecRefQueue ParamDescrs_DRQ { get { Contract.Ensures(Contract.Result() != null); return m_ParamDescrs_DRQ; } }
+ internal Probe.DecRefQueue Probe_DRQ { get { Contract.Ensures(Contract.Result() != null); return m_Probe_DRQ; } }
+ internal Solver.DecRefQueue Solver_DRQ { get { Contract.Ensures(Contract.Result() != null); return m_Solver_DRQ; } }
+ internal Statistics.DecRefQueue Statistics_DRQ { get { Contract.Ensures(Contract.Result() != null); return m_Statistics_DRQ; } }
+ internal Tactic.DecRefQueue Tactic_DRQ { get { Contract.Ensures(Contract.Result() != null); return m_Tactic_DRQ; } }
+ internal Fixedpoint.DecRefQueue Fixedpoint_DRQ { get { Contract.Ensures(Contract.Result() != null); return m_Fixedpoint_DRQ; } }
+
+
+ internal uint refCount = 0;
+
+ ///
+ /// Finalizer.
+ ///
+ ~Context()
+ {
+ // Console.WriteLine("Context Finalizer from " + System.Threading.Thread.CurrentThread.ManagedThreadId);
+ Dispose();
+
+ if (refCount == 0)
+ {
+ m_n_err_handler = null;
+ Native.Z3_del_context(m_ctx);
+ m_ctx = IntPtr.Zero;
+ }
+ else
+ GC.ReRegisterForFinalize(this);
+ }
+
+ ///
+ /// Disposes of the context.
+ ///
+ public void Dispose()
+ {
+ // Console.WriteLine("Context Dispose from " + System.Threading.Thread.CurrentThread.ManagedThreadId);
+ AST_DRQ.Clear(this);
+ ASTMap_DRQ.Clear(this);
+ ASTVector_DRQ.Clear(this);
+ ApplyResult_DRQ.Clear(this);
+ FuncEntry_DRQ.Clear(this);
+ FuncInterp_DRQ.Clear(this);
+ Goal_DRQ.Clear(this);
+ Model_DRQ.Clear(this);
+ Params_DRQ.Clear(this);
+ Probe_DRQ.Clear(this);
+ Solver_DRQ.Clear(this);
+ Statistics_DRQ.Clear(this);
+ Tactic_DRQ.Clear(this);
+ Fixedpoint_DRQ.Clear(this);
+
+ m_boolSort = null;
+ m_intSort = null;
+ m_realSort = null;
+ }
+ #endregion
+ }
+}
diff --git a/Microsoft.Z3/DecRefQUeue.cs b/Microsoft.Z3/DecRefQUeue.cs
new file mode 100644
index 000000000..777a5d5af
--- /dev/null
+++ b/Microsoft.Z3/DecRefQUeue.cs
@@ -0,0 +1,92 @@
+/*++
+Copyright (c) 2012 Microsoft Corporation
+
+Module Name:
+
+ DecRefQueue.cs
+
+Abstract:
+
+ Z3 Managed API: DecRef Queues
+
+Author:
+
+ Christoph Wintersteiger (cwinter) 2012-03-16
+
+Notes:
+
+--*/
+
+using System;
+using System.Collections;
+using System.Collections.Generic;
+using System.Threading;
+using System.Diagnostics.Contracts;
+
+namespace Microsoft.Z3
+{
+ [ContractClass(typeof(DecRefQueueContracts))]
+ internal abstract class DecRefQueue
+ {
+ #region Object invariant
+
+ [ContractInvariantMethod]
+ private void ObjectInvariant()
+ {
+ Contract.Invariant(this.m_queue != null);
+ }
+
+ #endregion
+
+ readonly internal protected Object m_lock = new Object();
+ readonly internal protected List m_queue = new List();
+ internal const uint m_move_limit = 1024;
+
+ public abstract void IncRef(Context ctx, IntPtr obj);
+ public abstract void DecRef(Context ctx, IntPtr obj);
+
+ public void IncAndClear(Context ctx, IntPtr o)
+ {
+ Contract.Requires(ctx != null);
+
+ IncRef(ctx, o);
+ if (m_queue.Count >= m_move_limit) Clear(ctx);
+ }
+
+ public void Add(IntPtr o)
+ {
+ if (o == IntPtr.Zero) return;
+
+ lock (m_lock)
+ {
+ m_queue.Add(o);
+ }
+ }
+
+ public void Clear(Context ctx)
+ {
+ Contract.Requires(ctx != null);
+
+ lock (m_lock)
+ {
+ foreach (IntPtr o in m_queue)
+ DecRef(ctx, o);
+ m_queue.Clear();
+ }
+ }
+ }
+
+ [ContractClassFor(typeof(DecRefQueue))]
+ abstract class DecRefQueueContracts : DecRefQueue
+ {
+ public override void IncRef(Context ctx, IntPtr obj)
+ {
+ Contract.Requires(ctx != null);
+ }
+
+ public override void DecRef(Context ctx, IntPtr obj)
+ {
+ Contract.Requires(ctx != null);
+ }
+ }
+}
diff --git a/Microsoft.Z3/Enumerations.cs b/Microsoft.Z3/Enumerations.cs
new file mode 100644
index 000000000..8e041ef41
--- /dev/null
+++ b/Microsoft.Z3/Enumerations.cs
@@ -0,0 +1,257 @@
+// Automatically generated file, generator: mk_z3consts.py
+
+using System;
+
+#pragma warning disable 1591
+
+namespace Microsoft.Z3
+{
+ /// Z3_lbool
+ public enum Z3_lbool {
+ Z3_L_TRUE = 1,
+ Z3_L_UNDEF = 0,
+ Z3_L_FALSE = -1,
+ }
+
+ /// Z3_symbol_kind
+ public enum Z3_symbol_kind {
+ Z3_INT_SYMBOL = 0,
+ Z3_STRING_SYMBOL = 1,
+ }
+
+ /// Z3_parameter_kind
+ public enum Z3_parameter_kind {
+ Z3_PARAMETER_FUNC_DECL = 6,
+ Z3_PARAMETER_DOUBLE = 1,
+ Z3_PARAMETER_SYMBOL = 3,
+ Z3_PARAMETER_INT = 0,
+ Z3_PARAMETER_AST = 5,
+ Z3_PARAMETER_SORT = 4,
+ Z3_PARAMETER_RATIONAL = 2,
+ }
+
+ /// Z3_sort_kind
+ public enum Z3_sort_kind {
+ Z3_BV_SORT = 4,
+ Z3_FINITE_DOMAIN_SORT = 8,
+ Z3_ARRAY_SORT = 5,
+ Z3_UNKNOWN_SORT = 1000,
+ Z3_RELATION_SORT = 7,
+ Z3_REAL_SORT = 3,
+ Z3_INT_SORT = 2,
+ Z3_UNINTERPRETED_SORT = 0,
+ Z3_BOOL_SORT = 1,
+ Z3_DATATYPE_SORT = 6,
+ }
+
+ /// Z3_ast_kind
+ public enum Z3_ast_kind {
+ Z3_VAR_AST = 2,
+ Z3_SORT_AST = 4,
+ Z3_QUANTIFIER_AST = 3,
+ Z3_UNKNOWN_AST = 1000,
+ Z3_FUNC_DECL_AST = 5,
+ Z3_NUMERAL_AST = 0,
+ Z3_APP_AST = 1,
+ }
+
+ /// Z3_decl_kind
+ public enum Z3_decl_kind {
+ Z3_OP_LABEL = 1792,
+ Z3_OP_PR_REWRITE = 1294,
+ Z3_OP_UNINTERPRETED = 2051,
+ Z3_OP_SUB = 519,
+ Z3_OP_ZERO_EXT = 1058,
+ Z3_OP_ADD = 518,
+ Z3_OP_IS_INT = 528,
+ Z3_OP_BREDOR = 1061,
+ Z3_OP_BNOT = 1051,
+ Z3_OP_BNOR = 1054,
+ Z3_OP_PR_CNF_STAR = 1315,
+ Z3_OP_RA_JOIN = 1539,
+ Z3_OP_LE = 514,
+ Z3_OP_SET_UNION = 773,
+ Z3_OP_PR_UNDEF = 1280,
+ Z3_OP_BREDAND = 1062,
+ Z3_OP_LT = 516,
+ Z3_OP_RA_UNION = 1540,
+ Z3_OP_BADD = 1028,
+ Z3_OP_BUREM0 = 1039,
+ Z3_OP_OEQ = 267,
+ Z3_OP_PR_MODUS_PONENS = 1284,
+ Z3_OP_RA_CLONE = 1548,
+ Z3_OP_REPEAT = 1060,
+ Z3_OP_RA_NEGATION_FILTER = 1544,
+ Z3_OP_BSMOD0 = 1040,
+ Z3_OP_BLSHR = 1065,
+ Z3_OP_BASHR = 1066,
+ Z3_OP_PR_UNIT_RESOLUTION = 1304,
+ Z3_OP_ROTATE_RIGHT = 1068,
+ Z3_OP_ARRAY_DEFAULT = 772,
+ Z3_OP_PR_PULL_QUANT = 1296,
+ Z3_OP_PR_APPLY_DEF = 1310,
+ Z3_OP_PR_REWRITE_STAR = 1295,
+ Z3_OP_IDIV = 523,
+ Z3_OP_PR_GOAL = 1283,
+ Z3_OP_PR_IFF_TRUE = 1305,
+ Z3_OP_LABEL_LIT = 1793,
+ Z3_OP_BOR = 1050,
+ Z3_OP_PR_SYMMETRY = 1286,
+ Z3_OP_TRUE = 256,
+ Z3_OP_SET_COMPLEMENT = 776,
+ Z3_OP_CONCAT = 1056,
+ Z3_OP_PR_NOT_OR_ELIM = 1293,
+ Z3_OP_IFF = 263,
+ Z3_OP_BSHL = 1064,
+ Z3_OP_PR_TRANSITIVITY = 1287,
+ Z3_OP_SGT = 1048,
+ Z3_OP_RA_WIDEN = 1541,
+ Z3_OP_PR_DEF_INTRO = 1309,
+ Z3_OP_NOT = 265,
+ Z3_OP_PR_QUANT_INTRO = 1290,
+ Z3_OP_UGT = 1047,
+ Z3_OP_DT_RECOGNISER = 2049,
+ Z3_OP_SET_INTERSECT = 774,
+ Z3_OP_BSREM = 1033,
+ Z3_OP_RA_STORE = 1536,
+ Z3_OP_SLT = 1046,
+ Z3_OP_ROTATE_LEFT = 1067,
+ Z3_OP_PR_NNF_NEG = 1313,
+ Z3_OP_PR_REFLEXIVITY = 1285,
+ Z3_OP_ULEQ = 1041,
+ Z3_OP_BIT1 = 1025,
+ Z3_OP_BIT0 = 1026,
+ Z3_OP_EQ = 258,
+ Z3_OP_BMUL = 1030,
+ Z3_OP_ARRAY_MAP = 771,
+ Z3_OP_STORE = 768,
+ Z3_OP_PR_HYPOTHESIS = 1302,
+ Z3_OP_RA_RENAME = 1545,
+ Z3_OP_AND = 261,
+ Z3_OP_TO_REAL = 526,
+ Z3_OP_PR_NNF_POS = 1312,
+ Z3_OP_PR_AND_ELIM = 1292,
+ Z3_OP_MOD = 525,
+ Z3_OP_BUDIV0 = 1037,
+ Z3_OP_PR_TRUE = 1281,
+ Z3_OP_BNAND = 1053,
+ Z3_OP_PR_ELIM_UNUSED_VARS = 1299,
+ Z3_OP_RA_FILTER = 1543,
+ Z3_OP_FD_LT = 1549,
+ Z3_OP_RA_EMPTY = 1537,
+ Z3_OP_DIV = 522,
+ Z3_OP_ANUM = 512,
+ Z3_OP_MUL = 521,
+ Z3_OP_UGEQ = 1043,
+ Z3_OP_BSREM0 = 1038,
+ Z3_OP_PR_TH_LEMMA = 1318,
+ Z3_OP_BXOR = 1052,
+ Z3_OP_DISTINCT = 259,
+ Z3_OP_PR_IFF_FALSE = 1306,
+ Z3_OP_BV2INT = 1072,
+ Z3_OP_EXT_ROTATE_LEFT = 1069,
+ Z3_OP_PR_PULL_QUANT_STAR = 1297,
+ Z3_OP_BSUB = 1029,
+ Z3_OP_PR_ASSERTED = 1282,
+ Z3_OP_BXNOR = 1055,
+ Z3_OP_EXTRACT = 1059,
+ Z3_OP_PR_DER = 1300,
+ Z3_OP_DT_CONSTRUCTOR = 2048,
+ Z3_OP_GT = 517,
+ Z3_OP_BUREM = 1034,
+ Z3_OP_IMPLIES = 266,
+ Z3_OP_SLEQ = 1042,
+ Z3_OP_GE = 515,
+ Z3_OP_BAND = 1049,
+ Z3_OP_ITE = 260,
+ Z3_OP_AS_ARRAY = 778,
+ Z3_OP_RA_SELECT = 1547,
+ Z3_OP_CONST_ARRAY = 770,
+ Z3_OP_BSDIV = 1031,
+ Z3_OP_OR = 262,
+ Z3_OP_AGNUM = 513,
+ Z3_OP_PR_PUSH_QUANT = 1298,
+ Z3_OP_BSMOD = 1035,
+ Z3_OP_PR_IFF_OEQ = 1311,
+ Z3_OP_PR_LEMMA = 1303,
+ Z3_OP_SET_SUBSET = 777,
+ Z3_OP_SELECT = 769,
+ Z3_OP_RA_PROJECT = 1542,
+ Z3_OP_BNEG = 1027,
+ Z3_OP_UMINUS = 520,
+ Z3_OP_REM = 524,
+ Z3_OP_TO_INT = 527,
+ Z3_OP_PR_QUANT_INST = 1301,
+ Z3_OP_SGEQ = 1044,
+ Z3_OP_POWER = 529,
+ Z3_OP_XOR3 = 1074,
+ Z3_OP_RA_IS_EMPTY = 1538,
+ Z3_OP_CARRY = 1073,
+ Z3_OP_DT_ACCESSOR = 2050,
+ Z3_OP_PR_TRANSITIVITY_STAR = 1288,
+ Z3_OP_PR_NNF_STAR = 1314,
+ Z3_OP_PR_COMMUTATIVITY = 1307,
+ Z3_OP_ULT = 1045,
+ Z3_OP_BSDIV0 = 1036,
+ Z3_OP_SET_DIFFERENCE = 775,
+ Z3_OP_INT2BV = 1071,
+ Z3_OP_XOR = 264,
+ Z3_OP_PR_MODUS_PONENS_OEQ = 1317,
+ Z3_OP_BNUM = 1024,
+ Z3_OP_BUDIV = 1032,
+ Z3_OP_PR_MONOTONICITY = 1289,
+ Z3_OP_PR_DEF_AXIOM = 1308,
+ Z3_OP_FALSE = 257,
+ Z3_OP_EXT_ROTATE_RIGHT = 1070,
+ Z3_OP_PR_DISTRIBUTIVITY = 1291,
+ Z3_OP_SIGN_EXT = 1057,
+ Z3_OP_PR_SKOLEMIZE = 1316,
+ Z3_OP_BCOMP = 1063,
+ Z3_OP_RA_COMPLEMENT = 1546,
+ }
+
+ /// Z3_param_kind
+ public enum Z3_param_kind {
+ Z3_PK_BOOL = 1,
+ Z3_PK_SYMBOL = 3,
+ Z3_PK_OTHER = 5,
+ Z3_PK_INVALID = 6,
+ Z3_PK_UINT = 0,
+ Z3_PK_STRING = 4,
+ Z3_PK_DOUBLE = 2,
+ }
+
+ /// Z3_ast_print_mode
+ public enum Z3_ast_print_mode {
+ Z3_PRINT_SMTLIB2_COMPLIANT = 3,
+ Z3_PRINT_SMTLIB_COMPLIANT = 2,
+ Z3_PRINT_SMTLIB_FULL = 0,
+ Z3_PRINT_LOW_LEVEL = 1,
+ }
+
+ /// Z3_error_code
+ public enum Z3_error_code {
+ Z3_INVALID_PATTERN = 6,
+ Z3_MEMOUT_FAIL = 7,
+ Z3_NO_PARSER = 5,
+ Z3_OK = 0,
+ Z3_INVALID_ARG = 3,
+ Z3_EXCEPTION = 12,
+ Z3_IOB = 2,
+ Z3_INTERNAL_FATAL = 9,
+ Z3_INVALID_USAGE = 10,
+ Z3_FILE_ACCESS_ERROR = 8,
+ Z3_SORT_ERROR = 1,
+ Z3_PARSER_ERROR = 4,
+ Z3_DEC_REF_ERROR = 11,
+ }
+
+ /// Z3_goal_prec
+ public enum Z3_goal_prec {
+ Z3_GOAL_UNDER = 1,
+ Z3_GOAL_PRECISE = 0,
+ Z3_GOAL_UNDER_OVER = 3,
+ Z3_GOAL_OVER = 2,
+ }
+
+}
diff --git a/Microsoft.Z3/Expr.cs b/Microsoft.Z3/Expr.cs
new file mode 100644
index 000000000..428381ae8
--- /dev/null
+++ b/Microsoft.Z3/Expr.cs
@@ -0,0 +1,1677 @@
+/*++
+Copyright () 2012 Microsoft Corporation
+
+Module Name:
+
+ Expr.cs
+
+Abstract:
+
+ Z3 Managed API: Expressions
+
+Author:
+
+ Christoph Wintersteiger (cwinter) 2012-03-20
+
+Notes:
+
+--*/
+
+using System;
+using System.Diagnostics.Contracts;
+
+namespace Microsoft.Z3
+{
+ ///