fi
fi
+AC_ARG_VAR(PYTHON, [PYTHON interpreter (used for building legacy Java library interface)])
+
+if test -z "$PYTHON"; then
+ AC_CHECK_PROGS(PYTHON, python, python, [])
+else
+ AC_CHECK_PROG(PYTHON, "$PYTHON", "$PYTHON", [])
+fi
+
+if test -z "$PYTHON"; then
+ AC_MSG_WARN([python not found, cannot build libcvc4compat_java (the legacy Java interface).])
+ CXXTESTGEN=
+ CXXTEST=
+fi
+
# Checks for libraries.
AC_CHECK_LIB(z, gzread, , [AC_MSG_ERROR([zlib required, install your distro's zlib-dev package or see www.zlib.net])])
AC_CHECK_HEADER(zlib.h, , [AC_MSG_ERROR([zlib required, install your distro's zlib-dev package or see www.zlib.net])])
# Java
AC_ARG_VAR(JAVA, [Java interpreter (used when testing Java interface)])
AC_ARG_VAR(JAVAC, [Java compiler (used when building and testing Java interface)])
+AC_ARG_VAR(JAVAH, [Java compiler (used when building and testing Java interface)])
AC_ARG_VAR(JAR, [Jar archiver (used when building Java interface)])
AC_ARG_VAR(JAVA_INCLUDES, [flags to pass to C compiler when building JNI libraries])
if test "$cvc4_build_java_bindings"; then
else
AC_CHECK_PROG(JAVAC, "$JAVAC", "$JAVAC", [])
fi
+ if test -z "$JAVAH"; then
+ AC_CHECK_PROGS(JAVAH, javah gcjh, javah, [])
+ else
+ AC_CHECK_PROG(JAVAH, "$JAVAH", "$JAVAH", [])
+ fi
if test -z "$JAR"; then
AC_CHECK_PROGS(JAR, jar, jar, [])
else
-I@srcdir@/../include -I@srcdir@/.. -I@builddir@/..
AM_CXXFLAGS = -Wall $(FLAG_VISIBILITY_HIDDEN)
+SUBDIRS = . compat
+
lib_LTLIBRARIES =
data_DATA =
if CVC4_LANGUAGE_BINDING_JAVA
--- /dev/null
+topdir = ../../..
+srcdir = src/bindings/compat
+
+include $(topdir)/Makefile.subdir
--- /dev/null
+AM_CPPFLAGS = \
+ -D__BUILDING_CVC4BINDINGSLIB \
+ -I@srcdir@/../../include -I@srcdir@/../.. -I@builddir@/../..
+AM_CXXFLAGS = -Wall $(FLAG_VISIBILITY_HIDDEN)
+
+if CVC4_BUILD_LIBCOMPAT
+SUBDIRS = java
+endif
+
--- /dev/null
+Main-Class: cvc3/Cvc3
+Class-Path: libcvc3.jar
--- /dev/null
+topdir = ../../../..
+srcdir = src/bindings/compat/java
+
+include $(topdir)/Makefile.subdir
--- /dev/null
+# LIBCVC4BINDINGS_VERSION (-version-info) is in the form current:revision:age
+#
+# current -
+# increment if interfaces have been added, removed or changed
+# revision -
+# increment if source code has changed
+# set to zero if current is incremented
+# age -
+# increment if interfaces have been added
+# set to zero if interfaces have been removed
+# or changed
+#
+LIBCVC4BINDINGS_VERSION = @CVC4_BINDINGS_LIBRARY_VERSION@
+
+AM_CPPFLAGS = \
+ -D__BUILDING_CVC4BINDINGSLIB \
+ -I@srcdir@/../../../include -I@srcdir@/../../.. -I@builddir@/../../.. -I@builddir@/cvc3
+AM_CXXFLAGS = -Wall $(FLAG_VISIBILITY_HIDDEN)
+
+lib_LTLIBRARIES =
+data_DATA =
+
+if CVC4_LANGUAGE_BINDING_JAVA
+
+lib_LTLIBRARIES += libcvc4bindings_java_compat.la
+data_DATA += cvc4compat.jar
+libcvc4bindings_java_compat_la_LDFLAGS = \
+ -version-info $(LIBCVC4BINDINGS_VERSION)
+libcvc4bindings_java_compat_la_LIBADD = \
+ -L@builddir@/../compat -lcvc4compat
+
+endif
+
+# source files
+# java files of the library wrapper
+LIB_FILES = \
+ JniUtils \
+ Cvc3Exception TypecheckException SoundException EvalException \
+ CLException ParserException SmtlibException DebugException \
+ Embedded EmbeddedManager \
+ InputLanguage QueryResult SatResult FormulaValue \
+ Expr ExprMut ExprManager ExprManagerMut \
+ Type TypeMut Op OpMut Rational RationalMut \
+ Theorem TheoremMut Proof ProofMut Context ContextMut \
+ Flag Flags FlagsMut \
+ Statistics StatisticsMut ValidityChecker
+# java files of the test program
+TEST_FILES = Test
+# java files of the stand alone program
+PROG_FILES = TimeoutHandler Cvc3
+# all java files, library and stand alone
+JAVA_FILES = $(LIB_FILES) $(TEST_FILES) $(PROG_FILES)
+# jni files of the library wrapper
+JNI_FILES = \
+ EmbeddedManager \
+ Expr ExprMut ExprManager \
+ Type TypeMut Op OpMut Rational RationalMut \
+ Theorem TheoremMut Proof ProofMut Context ContextMut \
+ Flag Flags FlagsMut \
+ Statistics StatisticsMut ValidityChecker
+
+# stub files
+IMPL_FILES = $(addsuffix _impl.cpp,$(JNI_FILES))
+# generated files
+JNI_CPP_FILES = $(patsubst %,%.cpp,$(JNI_FILES))
+# non-generated files
+SRC_CPP_FILES = JniUtils.cpp
+# all cpp files (to compile)
+CPP_FILES = $(SRC_CPP_FILES) $(JNI_CPP_FILES)
+
+nodist_libcvc4bindings_java_compat_la_SOURCES = $(CPP_FILES)
+
+HEADER_FILES = JniUtils.h
+PYTHON_FILES = run_all.py run_tests.py create_impl.py
+MANIFEST_FILES = Cvc3_manifest Test_manifest
+
+# compile each cpp file
+$(JNI_CPP_FILES): %.cpp: %_impl.cpp $(builddir)%.h JniUtils.h
+ $(AM_V_GEN)$(PYTHON) ./create_impl.py \
+ $(HEADER_PATH)/$(PACKAGE)/$*.h \
+ $(SOURCE_PATH)/$(PACKAGE)/$*_impl.cpp \
+ $(SOURCE_PATH)/$(PACKAGE)/$*.cpp
+
+$(SRC_CPP_FILES:.cpp=.lo): %.lo: src/cvc3/%.cpp .headers
+ $(AM_V_CXX)$(LTCXXCOMPILE) -c $(JAVA_INCLUDES) -I . -o $@ $<
+
+$(LIB_FILES:%=classes/cvc3/%.class): .classes
+.classes:
+ $(AM_V_GEN)mkdir -p classes && $(JAVAC) -source 1.4 -sourcepath $(srcdir)/src -d classes $(LIB_FILES:%=$(srcdir)/src/cvc3/%.java)
+ @touch .classes
+.headers: $(LIB_FILES:%=cvc3/%.h)
+ @touch .headers
+$(LIB_FILES:%=cvc3/%.h): %.h: classes/%.class .cvc3dir
+ $(AM_V_GEN)$(JAVAH) -jni -force -classpath classes -o $@ cvc3.$(@:cvc3/%.h=%)
+.cvc3dir:
+ @mkdir -p cvc3 && touch $@
+cvc4compat.jar: $(LIB_FILES:%=classes/cvc3/%.class)
+ $(AM_V_GEN)$(JAR) cf $@ -C classes .
+
+clean-local:
+ rm -fr classes cvc3
+CLEANFILES = .cvc3dir .classes .headers cvc4compat.jar
--- /dev/null
+#!/usr/bin/env python
+
+import sys
+import os
+import re
+
+
+### output cpp file
+
+# qualifiers:
+# c : embedded constant
+# m : embedded mutable
+# n : native
+# plus:
+# v : vector
+# vv : vector vector
+# vvv : vector vector vector
+
+# types:
+# - native: void, bool, int, string
+# - objects: the rest
+
+def is_native(arg_qual):
+ return (arg_qual[0] == 'n')
+
+def is_mutable(arg_qual):
+ return (arg_qual[0] == 'm')
+
+def is_const(arg_qual):
+ return (arg_qual[0] == 'c')
+
+def forall(p, s):
+ for x in s:
+ if not p(s):
+ return False
+
+ return True
+
+def check_arg_qual(arg_qual):
+ return \
+ (is_native(arg_qual) or is_mutable(arg_qual) or is_const(arg_qual)) \
+ and \
+ forall(lambda q: q == 'v', arg_qual[1:])
+
+def is_vector(arg_qual):
+ return (len(arg_qual) > 1 and arg_qual[1] == 'v')
+
+def is_vector2(arg_qual):
+ return (is_vector(arg_qual) and len(arg_qual) > 2 and arg_qual[2] == 'v')
+
+def is_vector3(arg_qual):
+ return (is_vector2(arg_qual) and len(arg_qual) > 3 and arg_qual[3] == 'v')
+
+
+# returns the jni type corresponding to the pseudo type signature
+def arg_type_to_java((arg_qual, arg_type, arg_name)):
+ check_arg_qual(arg_qual);
+ if arg_type == "jobject":
+ if (not is_native(arg_qual)) or is_vector(arg_qual):
+ print("Error: native defined in implementation with qualifier: " + arg_qual)
+ sys.exit(1)
+ return "jobject"
+ elif arg_type == "bool":
+ if not is_native(arg_qual):
+ print("Error: bool defined in implementation with qualifier: " + arg_qual)
+ sys.exit(1)
+ if is_vector(arg_qual):
+ return "jbooleanArray"
+ else:
+ return "jboolean"
+ elif arg_type == "int":
+ if not is_native(arg_qual):
+ print("Error: int defined in implementation with qualifier: " + arg_qual)
+ sys.exit(1)
+ if is_vector(arg_qual):
+ return "jintArray"
+ else:
+ return "jint"
+ elif arg_type == "string":
+ if not is_native(arg_qual):
+ print("Error: string defined in implementation with qualifier: " + arg_qual)
+ sys.exit(1)
+ if is_vector(arg_qual):
+ return "jobjectArray"
+ else:
+ return "jstring"
+ else:
+ if is_vector(arg_qual):
+ return "jobjectArray"
+ else:
+ return "jobject"
+
+def print_unembed_arg(cpp_file, (arg_qual, arg_type, arg_name)):
+ check_arg_qual(arg_qual);
+ if arg_type == "jobject":
+ ()
+ elif arg_type == "bool":
+ if is_vector3(arg_qual):
+ cpp_file.write(" vector<vector<vector<bool> > > " + arg_name \
+ + "(toCppVVV(env, j" + arg_name + "));\n");
+ elif is_vector2(arg_qual):
+ cpp_file.write(" vector<vector<bool> > " + arg_name \
+ + "(toCppVV(env, j" + arg_name + "));\n");
+ elif is_vector(arg_qual):
+ cpp_file.write(" vector<bool> " + arg_name \
+ + "(toCppV(env, j" + arg_name + "));\n");
+ else:
+ cpp_file.write(" bool " + arg_name + "(j" + arg_name + ");\n");
+ elif arg_type == "int":
+ if is_vector3(arg_qual):
+ cpp_file.write(" vector<vector<vector<int> > > " + arg_name \
+ + "(toCppVVV(env, j" + arg_name + "));\n");
+ elif is_vector2(arg_qual):
+ cpp_file.write(" vector<vector<int> > " + arg_name \
+ + "(toCppVV(env, j" + arg_name + "));\n");
+ elif is_vector(arg_qual):
+ cpp_file.write(" vector<int> " + arg_name \
+ + "(toCppV(env, j" + arg_name + "));\n");
+ else:
+ cpp_file.write(" int " + arg_name + "(j" + arg_name + ");\n");
+ elif arg_type == "string":
+ if is_vector3(arg_qual):
+ cpp_file.write(" vector<vector<vector<string> > > " + arg_name \
+ + "(toCppVVV(env, j" + arg_name + "));\n");
+ elif is_vector2(arg_qual):
+ cpp_file.write(" vector<vector<string> > " + arg_name \
+ + "(toCppVV(env, j" + arg_name + "));\n");
+ elif is_vector(arg_qual):
+ cpp_file.write(" vector<string> " + arg_name \
+ + "(toCppV(env, j" + arg_name + "));\n");
+ else:
+ cpp_file.write(" string " + arg_name + "(toCpp(env, j" + arg_name + "));\n");
+ else:
+ if is_vector3(arg_qual):
+ cpp_file.write(" vector<vector<vector<" + arg_type + "> > > " + arg_name \
+ + "(toCppVVV<" + arg_type + ">(env, j" + arg_name + "));\n");
+ elif is_vector2(arg_qual):
+ cpp_file.write(" vector<vector<" + arg_type + "> > " + arg_name \
+ + "(toCppVV<" + arg_type + ">(env, j" + arg_name + "));\n");
+ elif is_vector(arg_qual):
+ cpp_file.write(" vector<" + arg_type + "> " + arg_name \
+ + "(toCppV<" + arg_type + ">(env, j" + arg_name + "));\n");
+ elif is_const(arg_qual):
+ cpp_file.write(" const " + arg_type + "* " + arg_name \
+ + " = unembed_const<" + arg_type + ">(env, j" + arg_name + ");\n");
+ else:
+ cpp_file.write(" " + arg_type + "* " + arg_name \
+ + " = unembed_mut<" + arg_type + ">(env, j" + arg_name + ");\n");
+
+def print_unembed_args(cpp_file, args):
+ for arg in args:
+ print_unembed_arg(cpp_file, arg)
+
+
+# check hat declaration and definition signatures match
+def match_signatures((decl_result, decl_args), (def_result, def_args, _)):
+ if decl_result != def_result or len(decl_args) != len(def_args):
+ return False
+ for i in xrange(0, len(decl_args)):
+ java_type = arg_type_to_java(def_args[i])
+ #print java_type
+ if decl_args[i] != java_type:
+ return False
+ return True
+
+def print_header(cpp_file, includes):
+ cpp_file.writelines(map(lambda name: "#include " + name + "\n", includes))
+
+ cpp_file.writelines(
+ [
+ "#include \"JniUtils.h\"\n",
+ "\n",
+ "using namespace std;\n",
+ "using namespace Java_cvc3_JniUtils;\n",
+ "using namespace CVC3;\n",
+ "\n"
+ ])
+
+def print_signature(cpp_file, name, result, args):
+ arg_strings = ["JNIEnv* env", "jclass"]
+ arg_strings.extend( \
+ map(lambda (argQual, argType, argName): \
+ arg_type_to_java((argQual, argType, argName)) \
+ + " j" + argName, args))
+ cpp_file.writelines([
+ "JNIEXPORT " + result + " JNICALL " + name + "\n",
+ "(" + ", ".join(arg_strings) + ")\n"])
+
+def print_definition(cpp_file, name, (result, args, body)):
+ cpp_file.writelines(["extern \"C\"\n"])
+ print_signature(cpp_file, name, result, args)
+ cpp_file.writelines([
+ "{\n",
+ " try {\n"])
+ print_unembed_args(cpp_file, args)
+ cpp_file.writelines([
+ " " + " ".join(body),
+ " } catch (const Exception& e) {\n",
+ " toJava(env, e);\n"])
+ if result in [ "jobject", "jobjectArray", "jstring" ]:
+ cpp_file.writelines([" return NULL;\n"])
+ elif result == "jboolean":
+ cpp_file.writelines([" return false;\n"])
+ elif result == "jint":
+ cpp_file.writelines([" return -1;\n"])
+ elif result <> "void":
+ print("BUG: return type " + result + " is not handled in print_definition")
+ sys.exit(1)
+ cpp_file.writelines([" };\n",
+ "}\n\n"])
+
+def print_cpp(cpp_name, declarations, definitions, includes):
+ try:
+ cpp_file = open(cpp_name, 'w')
+
+ print_header(cpp_file, includes)
+
+ #names = declarations.keys()
+ #names.sort()
+ for name in declarations[0]:
+ if not definitions.has_key(name):
+ #continue
+ print("Error: " + name + " is declared in header" \
+ + " but not defined in implementation.")
+ sys.exit(1)
+
+ declaration = declarations[1][name]
+ definition = definitions[name]
+ definitions.pop(name)
+ if not match_signatures(declaration, definition):
+ print("Error: signature for " + name \
+ + " in definition and implementation do not match:")
+ print declaration
+ print (definition[0], definition[1])
+ sys.exit(1)
+
+ print_definition(cpp_file, name, definition)
+
+ if not len(definitions) == 0:
+ print("Error: found definitions in implementation" \
+ " without declaration in header file:")
+ print definitions
+ sys.exit(1)
+
+
+ except IOError, (error_nr, error_string):
+ print ("Couldn't open " + cpp_name + ": " + error_string)
+ sys.exit(0)
+
+
+### header file function declarations
+
+# header file function declaration:
+# - name: function name
+# - result: result type
+# - args: list of argument types, except for the first two (JNIEnv*, jclass)
+def register_declaration(declarations, name, result, args):
+ assert(not declarations[1].has_key(name));
+ declarations[0].append(name)
+ declarations[1][name] = (result, args)
+
+# extract function signatures from generated JNI header file
+def read_header(header_name):
+ # 0.: names of declared functions in same order as in input
+ # 1.: map from names to signature
+ declarations = ([], {})
+ try:
+ header_file = open(header_name)
+
+ line = header_file.readline()
+ while (line):
+ # look for start of signature
+ # declaration will look like:
+ # JNIEXPORT <result> JNICALL <name> (JNIENV *env, jclass, jobject);
+ # with an optional linebreak before the parameter list, and
+ # perhaps missing the "env"
+ if re.search("^JNIEXPORT", line):
+ # extract name and return type
+ elements = re.sub('[,();]+',' ',line).split();
+ assert(elements[0] == "JNIEXPORT");
+ assert(elements[2] == "JNICALL");
+ name = elements[3]
+ result = elements[1]
+
+ # If there are no more elements on this line,
+ # read and tokenize the next line
+ if len(elements) > 4:
+ elements = elements[4:]
+ else:
+ line = header_file.readline ()
+ elements = re.sub('[,();]+',' ',line).split();
+
+ # extract argument types
+ assert(elements[0] == "JNIEnv");
+ assert(elements[1] == "*" or elements[1] == "*env");
+ assert(elements[2] == "jclass")
+ args = elements[3:]
+
+ register_declaration(declarations, name, result, args)
+
+ line = header_file.readline ()
+
+ header_file.close()
+
+
+ except IOError, (error_nr, error_string):
+ print ("Couldn't open " + header_name + ": " + error_string)
+ sys.exit(0)
+
+ return declarations
+
+
+
+
+# function definitions:
+
+# cpp file function definition:
+# - name: function name
+# - result: result type
+# - args: list of pairs of argument types and argument names,
+# except for the first two (JNIEnv*, jclass)
+def register_definition(definitions, name, result, args, body):
+ if definitions.has_key(name):
+ print("Error: redefinition of " + name + " in implementation.")
+ sys.exit(1)
+
+ definitions[name] = (result, args, body)
+ #print_definition(name, declarations[name])
+
+# extract function definition from implementation file
+def read_impl(impl_name):
+ definitions = {}
+ includes = []
+ try:
+ impl_file = open(impl_name)
+
+ line = impl_file.readline()
+ while (line):
+ # look for include
+ if re.search("^INCLUDE:", line):
+ elements = line.split();
+ assert(len(elements) == 2);
+ assert(elements[0] == "INCLUDE:")
+ includes.append(elements[1])
+ line = impl_file.readline()
+
+ #print line
+ # look for start of definition
+ elif re.search("^DEFINITION:", line):
+ #print line,
+ # get name
+ elements = line.split();
+ if not (len(elements) == 2):
+ print("Error: misformed signature: " + line)
+ sys.exit(1)
+
+ assert(elements[0] == "DEFINITION:")
+ name = elements[1]
+
+ # get signature
+ line = impl_file.readline ()
+ elements = line.split();
+ assert(len(elements) > 0);
+ if not (len(elements) % 3 == 1):
+ print("Error: misformed signature for: " + name)
+ print(line)
+ sys.exit(1)
+ result = elements.pop(0)
+ args = []
+ while len(elements) > 0:
+ argQual = elements.pop(0)
+ argType = elements.pop(0)
+ argName = elements.pop(0)
+ args.append((argQual, argType, argName))
+
+ # get body
+ body = []
+ line = impl_file.readline ()
+ while line and not re.search("^DEFINITION:", line):
+ body.append(line)
+ line = impl_file.readline()
+
+ while body and body[len(body) - 1] == "\n":
+ body.pop(len(body) - 1)
+ assert(len(body) > 0)
+
+ register_definition(definitions, name, result, args, body)
+
+ else:
+ line = impl_file.readline()
+
+ impl_file.close()
+
+ except IOError, (error_nr, error_string):
+ print ("Couldn't open " + impl_name + ": " + error_string)
+ sys.exit(0)
+
+ return definitions, includes
+
+
+# read name of input file
+if (len(sys.argv) != 4):
+ print("Expected path to header, implementation, and target file.")
+ print("")
+ print("./create_impl.py <H_FILE> <IMPL_FILE> <CPP_FILE>")
+
+ sys.exit(0)
+
+else:
+ #print(sys.argv)
+ header_name = sys.argv[1]
+ impl_name = sys.argv[2]
+ cpp_file = sys.argv[3]
+
+ # extract information from header
+ declarations = read_header(header_name)
+ #print declarations
+
+ # extract information from template
+ definitions, includes = read_impl(impl_name)
+ #print definitions
+
+ # create implementation
+ print_cpp(cpp_file, declarations, definitions, includes)
--- /dev/null
+/*****************************************************************************/
+/*!
+ *\file formulavalue.h
+ *\brief enumerated type for value of formulas
+ *
+ * Author: Alexander Fuchs
+ *
+ * Created: Fri Dec 07 08:00:00 2007
+ *
+ * <hr>
+ *
+ * License to use, copy, modify, sell and/or distribute this software
+ * and its documentation for any purpose is hereby granted without
+ * royalty, subject to the terms and conditions defined in the \ref
+ * LICENSE file provided with this distribution.
+ *
+ * <hr>
+ */
+/*****************************************************************************/
+
+#ifndef _cvc3__include__formulavalue_h_
+#define _cvc3__include__formulavalue_h_
+
+namespace CVC3 {
+
+/*****************************************************************************/
+/*
+ * Type for truth value of formulas.
+ */
+/*****************************************************************************/
+typedef enum FormulaValue {
+ TRUE_VAL,
+ FALSE_VAL,
+ UNKNOWN_VAL
+} FormulaValue;
+
+}
+
+#endif
--- /dev/null
+#ifndef _java__cvc3__jni_utils_h_
+#define _java__cvc3__jni_utils_h_
+
+#include <cassert>
+#include <string>
+#include <jni.h>
+#include <typeinfo>
+#include "vcl.h"
+#include "hash_map.h"
+#include "exception.h"
+
+namespace Java_cvc3_JniUtils {
+
+ /// Embedding of c++ objects in java objects
+
+ // generic delete function for any type T
+ template <class T> class DeleteEmbedded {
+ public:
+ static void deleteEmbedded(void* cobj) {
+ delete (T*) cobj;
+ }
+ };
+
+ typedef void (*TDeleteEmbedded)(void*);
+
+
+ // Encapsulates a c++ object so that:
+ // - (un)embedding casting is type safe
+ // - deallocation is automatic (if needed)
+ // This has probably quit a bit of overhead, because now for each
+ // wrapper object (even if only a temporary reference) an instance
+ // of Embedded is created.
+ // But considering the above two benefits it should be worth it
+ // because it should simplify maintenance quite a bit,
+ // as changes in the cvc API should lead to assertion failures
+ // instead of strange bugs.
+ class Embedded {
+ private:
+ // the actual embedded c++ object,
+ // as void* to make Embedded independent of its type
+ void* d_cobj;
+
+ // the type info of d_cobj,
+ // to make sure that later unembeddings are type safe
+ // actually only needed in debugging, so might be guarded with IF_DEBUG
+ const std::type_info& d_typeInfo;
+
+ // the type correct delete function for d_cobj,
+ // or NULL if this embedding is merely a reference
+ // and not responsible for its deallocation
+ TDeleteEmbedded d_delete;
+
+ public:
+ Embedded(void* cobj, const std::type_info& ti, TDeleteEmbedded del) :
+ d_cobj(cobj), d_typeInfo(ti), d_delete(del) {
+ assert(d_cobj != NULL);
+ }
+
+ ~Embedded() {
+ assert(d_cobj != NULL);
+ if (d_delete != NULL) d_delete(d_cobj);
+ }
+
+ const void* getCObj() const {
+ return d_cobj;
+ }
+
+ const std::type_info& getType() const {
+ return d_typeInfo;
+ }
+ };
+
+
+
+ // embed functions
+
+ // embeds a c++ object of type T into a jobject
+ // by first wrapping it into an Embedded object.
+ template <class T> jobject embed(JNIEnv* env, T* cobj, const std::type_info& ti,
+ TDeleteEmbedded del) {
+ DebugAssert(cobj != NULL, "JniUtils::embed: null object given");
+ Embedded* embedded = new Embedded((void*)cobj, ti, del);
+ return (jobject)env->NewDirectByteBuffer(embedded, sizeof(Embedded));
+ }
+
+ // embeds a constant reference to a c++ object into a jobject
+ template <class T> jobject embed_const_ref(JNIEnv* env, const T* cobj) {
+ DebugAssert(cobj != NULL, "JniUtils::embed_const: null object given");
+ return embed<T>(env, (T*) cobj, typeid(cobj), NULL);
+ }
+
+ // embeds a mutable reference to a c++ object into a jobject
+ template <class T> jobject embed_mut_ref(JNIEnv* env, T* cobj) {
+ DebugAssert(cobj != NULL, "JniUtils::embed_mut_ref: null object given");
+ return embed<T>(env, (T*) cobj, typeid(cobj), NULL);
+ }
+
+ // embeds a fresh copy of a (probably temporary) c++ object into a jobject
+ template <class T> jobject embed_copy(JNIEnv* env, const T& cobj) {
+ DebugAssert(&cobj != NULL, "JniUtils::embed_copy: null object given");
+ T* copy = new T(cobj);
+ assert(copy != NULL);
+ return embed<T>(env, copy, typeid(copy), &DeleteEmbedded<T>::deleteEmbedded);
+ }
+
+ // embeds a c++ object into a jobject,
+ // and takes over the responsibility to deallocate it
+ template <class T> jobject embed_own(JNIEnv* env, T* cobj) {
+ DebugAssert(&cobj != NULL, "JniUtils::embed_own: null object given");
+ return embed<T>(env, cobj, typeid(cobj), &DeleteEmbedded<T>::deleteEmbedded);
+ }
+
+
+ // unembed functions
+
+ // extract Embedded* from a jobject
+ Embedded* unembed(JNIEnv* env, jobject jobj);
+
+ // extract a constant c++ object of type T from a jobject
+ template <class T> const T* unembed_const(JNIEnv* env, jobject jobj) {
+ Embedded* embedded = unembed(env, jobj);
+ return (const T*) embedded->getCObj();
+ }
+
+ // extract a mutable c++ object of type T from a jobject
+ template <class T> T* unembed_mut(JNIEnv* env, jobject jobj) {
+ Embedded* embedded = unembed(env, jobj);
+ // check that the wrapped object is not const
+ DebugAssert(embedded->getType() == typeid(T*),
+ "JniUtils::unembed_mut: type mismatch");
+ return (T*) embedded->getCObj();
+ }
+
+
+ // delete embedded
+
+ // delete the Embedded object contained in a jobject,
+ // and also destruct the wrapped c++ object if necessary.
+ void deleteEmbedded(JNIEnv* env, jobject jobj);
+
+
+
+
+ /// Conversions between c++ and java
+
+ // bool
+ bool toCpp(jboolean j);
+
+ // string
+ jstring toJava(JNIEnv* env, const std::string& cstring);
+ jstring toJava(JNIEnv* env, const char* cstring);
+ std::string toCpp(JNIEnv* env, const jstring& string);
+
+ // enums
+ jstring toJava(JNIEnv* env, CVC3::QueryResult result);
+ jstring toJava(JNIEnv* env, CVC3::FormulaValue result);
+ jstring toJava(JNIEnv* env, CVC3::InputLanguage result);
+ CVC3::InputLanguage toCppInputLanguage(JNIEnv* env, const std::string& lang);
+
+ // exceptions
+ void toJava(JNIEnv* env, const CVC3::Exception& e);
+
+ // vectors
+ template <class T> jobjectArray toJavaVCopy(JNIEnv* env, const std::vector<T>& v) {
+ jobjectArray jarray = (jobjectArray)
+ env->NewObjectArray(
+ v.size(),
+ env->FindClass("java/lang/Object"),
+ NULL);
+
+ for (int i = 0; i < v.size(); ++i) {
+ env->SetObjectArrayElement(jarray, i, embed_copy<T>(env, v[i]));
+ }
+
+ return jarray;
+ }
+
+ template <class T> jobjectArray toJavaVConstRef(JNIEnv* env, const std::vector<T>& v) {
+ jobjectArray jarray = (jobjectArray)
+ env->NewObjectArray(
+ v.size(),
+ env->FindClass("java/lang/Object"),
+ NULL);
+
+ for (int i = 0; i < v.size(); ++i) {
+ env->SetObjectArrayElement(jarray, i, embed_const_ref<T>(env, &v[i]));
+ }
+
+ return jarray;
+ }
+
+ template<class T>
+ jobjectArray
+ toJavaVVConstRef(JNIEnv* env, const std::vector<std::vector<T> >& v)
+ {
+ jobjectArray jarray = (jobjectArray) env->NewObjectArray(v.size(),
+ env->FindClass("[Ljava/lang/Object;"), NULL);
+ for (int i = 0; i < v.size(); ++i)
+ {
+ env->SetObjectArrayElement(jarray, i, toJavaVConstRef(env, v[i]));
+ }
+ return jarray;
+ }
+
+ template <class T> std::vector<T> toCppV(JNIEnv* env, const jobjectArray& jarray) {
+ std::vector<T> v;
+ int length = env->GetArrayLength(jarray);
+ for (int i = 0; i < length; ++i) {
+ v.push_back(*unembed_const<T>(env, env->GetObjectArrayElement(jarray, i)));
+ }
+ return v;
+ }
+
+ template <class T> std::vector<std::vector<T> > toCppVV(JNIEnv* env, const jobjectArray& jarray) {
+ std::vector<std::vector<T> > v;
+ int length = env->GetArrayLength(jarray);
+ for (int i = 0; i < length; ++i) {
+ jobjectArray jsub = static_cast<jobjectArray>(env->GetObjectArrayElement(jarray, i));
+ v.push_back(toCppV<T>(env, jsub));
+ }
+ return v;
+ }
+
+ template <class T> std::vector<std::vector<std::vector<T> > >
+ toCppVVV(JNIEnv* env, const jobjectArray& jarray) {
+ std::vector<std::vector<std::vector<T> > > v;
+ int length = env->GetArrayLength(jarray);
+ for (int i = 0; i < length; ++i) {
+ jobjectArray jsub = static_cast<jobjectArray>(env->GetObjectArrayElement(jarray, i));
+ v.push_back(toCppVV<T>(env, jsub));
+ }
+ return v;
+ }
+
+ // string vectors
+ std::vector<std::string> toCppV(JNIEnv* env, const jobjectArray& jarray);
+ std::vector<std::vector<std::string> > toCppVV(JNIEnv* env, const jobjectArray& jarray);
+ std::vector<std::vector<std::vector<std::string> > > toCppVVV(JNIEnv* env, const jobjectArray& jarray);
+ jobjectArray toJavaV(JNIEnv* env, const std::vector<std::string>& v);
+
+ // primitive vectors
+ std::vector<bool> toCppV(JNIEnv* env, const jbooleanArray& jarray);
+
+
+ // hash map
+ template <class K, class V> jobjectArray toJavaHCopy(JNIEnv* env, const Hash::hash_map<K, V>& hm) {
+ jobjectArray jarray = (jobjectArray)
+ env->NewObjectArray(
+ hm.size() * 2,
+ env->FindClass("java/lang/Object"),
+ NULL);
+
+ int i = 0;
+ typename Hash::hash_map<K, V>::const_iterator it;
+ for (it = hm.begin(); it != hm.end(); ++it) {
+ assert(i < env->GetArrayLength(jarray));
+ env->SetObjectArrayElement(jarray, i, embed_copy<K>(env, it->first));
+ ++i;
+ assert(i < env->GetArrayLength(jarray));
+ env->SetObjectArrayElement(jarray, i, embed_copy<V>(env, it->second));
+ ++i;
+ }
+ return jarray;
+ }
+
+ template <class V> jobjectArray toJavaHCopy(JNIEnv* env, const CVC3::ExprMap<V>& hm) {
+ jobjectArray jarray = (jobjectArray)
+ env->NewObjectArray(
+ hm.size() * 2,
+ env->FindClass("java/lang/Object"),
+ NULL);
+
+ int i = 0;
+ typename CVC3::ExprMap<V>::const_iterator it;
+ for (it = hm.begin(); it != hm.end(); ++it) {
+ assert(i < env->GetArrayLength(jarray));
+ env->SetObjectArrayElement(jarray, i, embed_copy<CVC3::Expr>(env, it->first));
+ ++i;
+ assert(i < env->GetArrayLength(jarray));
+ env->SetObjectArrayElement(jarray, i, embed_copy<V>(env, it->second));
+ ++i;
+ }
+ return jarray;
+ }
+
+}
+
+
+#endif
--- /dev/null
+package cvc3;
+
+import java.util.*;
+
+/** mirrors CVC3::CLException */
+class CLException extends Cvc3Exception {
+
+ private final static long serialVersionUID = 1L;
+
+ public CLException(String message) {
+ super(message);
+ }
+}
--- /dev/null
+package cvc3;
+
+import java.util.*;
+
+public class Context extends Embedded {
+ // jni methods
+
+ /// Constructor
+
+ public Context(Object Context, EmbeddedManager embeddedManager) {
+ super(Context, embeddedManager);
+ }
+
+
+ /// API (immutable)
+
+}
--- /dev/null
+package cvc3;
+
+import java.util.*;
+
+public class ContextMut extends Context {
+ // jni methods
+
+
+ /// Constructor
+
+ // create embedded object
+ public ContextMut(Object ContextMut, EmbeddedManager embeddedManager) {
+ super(ContextMut, embeddedManager);
+ }
+
+
+ /// API (mutable)
+}
--- /dev/null
+package cvc3;
+
+import java.util.*;
+
+class Cvc3 {
+ static boolean useObjManager = false;
+
+ static void timeoutHandler(Object o) {
+ System.out.println("self-timeout.");
+ System.exit(1);
+ }
+
+ public static void main(String args[]) throws Cvc3Exception {
+
+ ValidityChecker vc = null;
+ FlagsMut flags = null;
+ try {
+ flags = ValidityChecker.createFlags(null);
+
+ // parse input
+ String fileName = "";
+ try {
+ fileName = parse_args(args, flags);
+ } catch(CLException e) {
+ System.err.print("*** " + e);
+ System.err.println("\n\nRun with -help option for usage information.");
+ System.exit(1);
+ }
+
+ // Set the timeout, if given in the command line options
+ int timeout = flags.getFlag("timeout").getInt();
+ if (timeout > 0) {
+ new Timer().schedule(new TimeoutHandler(), timeout * 1000);
+ }
+
+ /*
+ * Create and run the validity checker
+ */
+
+ // Debugging code may throw an exception
+ vc = ValidityChecker.create(flags);
+ flags.delete();
+
+ // -h flag sets "help" to false (+h would make it true, but that's
+ // not what the user normally types in).
+ if(!vc.getFlags().getFlag("help").getBool()) {
+ String programName = "cvc3"; //:TODO:
+ printUsage(vc.getFlags(), programName);
+ System.exit(0);
+ }
+
+ // Similarly, -version sets the flag "version" to false
+ if(!vc.getFlags().getFlag("version").getBool()) {
+ System.out.println("This is CVC3 version " + "UNKNOWN"); //:TODO:
+ System.out.println("Copyright (C) 2003-2006 by the Board of Trustees of Leland Stanford Junior");
+ System.out.println("University, New York University, and the University of Iowa.");
+ System.out.println();
+ System.out.print("THIS SOFTWARE PROVIDED AS-IS, WITHOUT ANY WARRANTIES. ");
+ System.out.println("USE IT AT YOUR OWN RISK.");
+ System.out.println();
+ System.exit(0);
+ }
+
+ // Test if the output language is correctly specified; if not, an
+ // exception will be thrown
+ vc.getExprManager().getOutputLanguage();
+ // Read the input file
+ vc.loadFile(fileName, vc.getExprManager().getInputLanguage());
+
+ // Print statistics
+ if (vc.getFlags().getFlag("stats").getBool()) {
+ vc.printStatistics();
+ }
+ } catch (Cvc3Exception e) {
+ System.err.println("*** Fatal exception: " + e);
+ System.exit(1);
+ } finally {
+ if (flags != null) flags.delete();
+ if (vc != null) vc.delete();
+ }
+
+ // to avoid waiting for timer to finish
+ System.exit(0);
+ }
+
+
+
+ // evaluates command line flags, returns problem file name
+ public static String parse_args(String[] args, FlagsMut flags) throws Cvc3Exception {
+ // keep track that exactly one file name is given
+ String fileName = "";
+ boolean seenFileName = false;
+
+ // iterate over the arguments
+ for (int i = 0; i < args.length; ++i) {
+ String arg = args[i];
+
+ // A command-line option
+ if (arg.startsWith("-") || arg.startsWith("+")) {
+ List names = flags.getFlags(arg.substring(1));
+
+ // no match
+ if (names.size() == 0)
+ throw new CLException(arg + " does not match any known option");
+
+ // ambiguous
+ else if (names.size() > 1) {
+ StringBuffer s = new StringBuffer();
+ s.append(arg + " is ambiguous. Possible matches are:\n");
+ for (Iterator name = names.iterator(); name.hasNext(); ) {
+ s.append(" " + name.next() + "\n");
+ }
+ throw new CLException(s.toString());
+ }
+
+ // Single match; process the option by name, type, and parameters
+ else {
+ String name = (String) names.iterator().next();
+ boolean val = arg.startsWith("+");
+ Flag flag = flags.getFlag(name);
+
+ if (flag.isBool()) {
+ flags.setFlag(name, val);
+ }
+
+ else if (flag.isInt()) {
+ ++i;
+ if (i >= args.length)
+ throw new CLException (arg + " (-" + name + ") expects an integer argument.");
+ int parameter = Integer.parseInt(args[i]);
+ flags.setFlag(name, parameter);
+ }
+
+ else if (flag.isString()) {
+ ++i;
+ if (i >= args.length)
+ throw new CLException (arg + " (-" + name + ") expects a string argument.");
+ flags.setFlag(name, args[i]);
+ }
+
+ // else if (flag.isStringVec())
+ // {
+ // bool hasMore = iter.MoveNext();
+ // if (!hasMore)
+ // {
+ // throw new CLException
+ // (arg + " (-" + name + ") expects a string argument.");
+ // }
+ // flags.setFlag(name, (string)iter.Current, val);
+ // }
+
+ else {
+ throw new CLException("parse_args: Bad flag : " + name);
+ }
+ }
+ }
+
+ // no flag, so should be a file name
+ // second no flag argument
+ else if(seenFileName) {
+ throw new CLException("More than one file name given: " + fileName + " and " + arg);
+ }
+
+ // first no flag argument
+ else {
+ fileName = arg;
+ seenFileName = true;
+ }
+ }
+
+ return fileName;
+ }
+
+
+ public static void printUsage(Flags flags, String programName) throws Cvc3Exception {
+ System.out.println("Usage: " + programName + " [options]");
+ System.out.println(programName + " will read the input from STDIN and ");
+ System.out.println("print the result on STDOUT.");
+ System.out.println("Boolean (b) options are set 'on' by +option and 'off' by -option");
+ System.out.println("(for instance, +sat or -sat).");
+ System.out.println("Integer (i), string (s) and vector (v) options ");
+ System.out.println("require a parameter, e.g. -width 80");
+ System.out.println("Also, (v) options can appear multiple times setting args on and off,");
+ System.out.println("as in +trace \"enable this\" -trace \"disable that\".");
+ System.out.println("Option names can be abbreviated to the shortest unambiguous prefix.");
+ System.out.println();
+ System.out.println("The options are:");
+
+ // Get all the names of options (they all match the empty string)
+ List names = flags.getFlags("");
+ for (Iterator i = names.iterator(); i.hasNext(); ) {
+ String name = (String) i.next();
+ Flag flag = flags.getFlag(name);
+ String prefix = "";
+ if (flag.isNull()) {
+ prefix = " (null)";
+ }
+ else if (flag.isBool()) {
+ String enabled = flag.getBool() ? "+" : "-";
+ prefix = " (b) " + enabled + name;
+ }
+ else if (flag.isInt()) {
+ prefix = " (i) -" + name + " " + flag.getInt();
+ }
+ else if (flag.isString()) {
+ prefix = " (s) -" + name + " " + flag.getString();
+ }
+ else if (flag.isStringVec()) {
+ prefix = " (s) -" + name;
+ }
+ else {
+ assert(false);
+ }
+
+ while (prefix.length() < 21) {
+ prefix += " ";
+ }
+ System.out.println(prefix + " " + flag.getHelp());
+ }
+ System.out.println();
+ }
+}
--- /dev/null
+package cvc3;
+
+
+/** mirrors CVC3::Exception */
+public class Cvc3Exception extends RuntimeException {
+
+ private final static long serialVersionUID = 1L;
+
+ public Cvc3Exception(String message) {
+ super(message);
+ }
+}
--- /dev/null
+package cvc3;
+
+import java.util.*;
+
+/** mirrors CVC3::DebugException */
+public class DebugException extends Cvc3Exception {
+
+ private final static long serialVersionUID = 1L;
+
+ public DebugException(String message) {
+ super(message);
+ }
+}
--- /dev/null
+package cvc3;
+
+import java.util.*;
+import java.io.*;
+
+/** Wrapper for a c++ object as a java Object.
+
+ see README for details on garbage collection,
+ i.e. interplay of delete, finalize, and EmbeddedManager to destruct
+ the embedded c++ object. */
+public abstract class Embedded {
+
+ // load jni c++ library
+ static {
+ System.loadLibrary("cvc3jni");
+
+ /*
+ // for debugging: stop here by waiting for a key press,
+ // and attach c++ debugger
+ System.out.println("Loadded cvc3jni");
+
+ try {
+ BufferedReader br = new BufferedReader(new InputStreamReader(System.in));
+ br.readLine();
+ } catch (IOException ioe) {
+ }
+ */
+ }
+
+
+ /// Attributes
+
+
+ // embedded object
+ protected Object d_embedded;
+
+ // embedded object manager
+ private final EmbeddedManager d_embeddedManager;
+
+
+ /// Constructor
+
+
+ // initialize with embedded object and EmbeddedManager
+ // if EmbeddedManager is null then delete must be called before
+ // Embedded is garbage collected
+ protected Embedded(Object Embedded, EmbeddedManager embeddedManager) {
+ //System.out.println("Create: Embedded");
+ assert(Embedded != null);
+ d_embedded = Embedded;
+ d_embeddedManager = embeddedManager;
+ }
+
+ // access to embedded c++ object
+ public synchronized Object embedded() {
+ return d_embedded;
+ }
+
+ // access to EmbeddedManager (might be null if none used)
+ public EmbeddedManager embeddedManager() {
+ return d_embeddedManager;
+ }
+
+ // check if already destructed
+ // (or queued for destruction in embeddedManager)
+ public synchronized boolean isDeleted() {
+ return (d_embedded == null);
+ }
+
+ // delete embedded object or enqueue it for deletion
+ public synchronized void delete() throws Cvc3Exception {
+ if (isDeleted()) return;
+
+ // no embedded manager, so should be in main thread:
+ // destruct right away
+ if (d_embeddedManager == null) {
+ EmbeddedManager.jniDelete(d_embedded);
+ }
+ // could be in finalizer, so queue in embeddedManager;
+ // unless the embeddedManager is already deleted,
+ // then its (and this') ValidityChecker has been delete.
+ // assuming this is an Expr or a Theorem it's embedded object
+ // has then already been deleted as well.
+ else {
+ synchronized(d_embeddedManager) {
+ if (!d_embeddedManager.isDeleted()) {
+ d_embeddedManager.register(this);
+ }
+ }
+ }
+ d_embedded = null;
+ }
+
+ // ensure that delete is called if finalization occurs
+ public void finalize() throws Throwable {
+ try {
+ // no embeddedManager, so deleted should have been called
+ if (d_embeddedManager == null) {
+ if (d_embedded != null) {
+ assert(false);
+// System.out.println("Embedded.Finalizer: should never be called");
+ throw new Error("Embedded.Finalizer: should never be called");
+ }
+ }
+ else if (!d_embeddedManager.isDeleted()) {
+ delete();
+ }
+ } finally {
+ super.finalize();
+ }
+ }
+}
--- /dev/null
+package cvc3;
+
+import java.util.*;
+
+/** Helps to enforce deallocation of a set of embedded objects
+
+ See also Embedded.java
+
+ Cvc3 requires on the C++ level that the ValidityChecker is destructed
+ last, after all other Cvc3 objects (i.e. subclasses of Embedded).
+
+ A 'simple' (but not too cheap) way to achieve this effect of deterministic
+ deallocation in Java without introducing much error prone code is to
+ register all embedded objects (except for the ValidityChecker)
+ with an EmbeddedManager.
+
+ When the ValidityChecker is deleted/finalized it uses the EmbeddedManager
+ to destruct all other Cvc3 objects first.
+*/
+public class EmbeddedManager {
+ // jni methods
+
+ // call the destructor of the c++ object
+ public static native void jniDelete(Object Embedded) throws Cvc3Exception;
+
+
+ // c++ objects which have been registered for deletion
+ private List d_deleted;
+
+
+ /// Constructor
+
+ // delete must be called before EmbeddedManager is garbage collected
+ public EmbeddedManager() {
+ d_deleted = new ArrayList();
+ }
+
+
+ /// Methods
+
+ // true iff delete has been called
+ public synchronized boolean isDeleted() {
+ return (d_deleted == null);
+ }
+
+ // signals that the ValidityChecker destructs itself
+ public synchronized void delete() throws Cvc3Exception {
+ d_deleted = null;
+ }
+
+ // registers a c++ object for deletion
+ public synchronized void register(Embedded embedded) {
+ d_deleted.add(embedded.embedded());
+ }
+
+ // destruct all registered objects
+ public synchronized void cleanUp() throws Cvc3Exception {
+ assert(!isDeleted());
+ Iterator i = d_deleted.iterator();
+ while (i.hasNext()) {
+ jniDelete(i.next());
+ }
+ d_deleted.clear();
+ }
+
+ // ensure that all embedded objects are deallocated eventually
+ public void finalize() throws Throwable {
+ try {
+ if (!isDeleted()) {
+ assert(false);
+// System.out.println("EmbeddedManager.Finalizer: should never be called");
+ throw new Error("EmbeddedManager.Finalizer: should never be called");
+ }
+ } finally {
+ super.finalize();
+ }
+ }
+}
--- /dev/null
+DEFINITION: Java_cvc3_EmbeddedManager_jniDelete
+void n jobject obj
+deleteEmbedded(env, jobj);
--- /dev/null
+package cvc3;
+
+import java.util.*;
+
+/** mirrors CVC3::EvalException */
+public class EvalException extends Cvc3Exception {
+
+ private final static long serialVersionUID = 1L;
+
+ public EvalException(String message) {
+ super(message);
+ }
+}
--- /dev/null
+package cvc3;
+
+import java.util.*;
+
+public class Expr extends Embedded {
+ // jni methods
+ private static native boolean
+ jniEquals(Object Expr1, Object Expr2) throws Cvc3Exception;
+ private static native String
+ jniToString(Object Expr) throws Cvc3Exception;
+ private static native void
+ jniPrint(Object Expr, String InputLanguage, boolean dagify) throws Cvc3Exception;
+ private static native int
+ jniHash(Object Expr) throws Cvc3Exception;
+
+ private static native String
+ jniGetKind(Object Expr) throws Cvc3Exception;
+
+ private static native boolean
+ jniIsFalse(Object Expr) throws Cvc3Exception;
+ private static native boolean
+ jniIsTrue(Object Expr) throws Cvc3Exception;
+ private static native boolean
+ jniIsBoolConst(Object Expr) throws Cvc3Exception;
+ private static native boolean
+ jniIsVar(Object Expr) throws Cvc3Exception;
+ private static native boolean
+ jniIsBoundVar(Object Expr) throws Cvc3Exception;
+ private static native boolean
+ jniIsString(Object Expr) throws Cvc3Exception;
+ private static native boolean
+ jniIsClosure(Object Expr) throws Cvc3Exception;
+ private static native boolean
+ jniIsQuantifier(Object Expr) throws Cvc3Exception;
+ private static native boolean
+ jniIsLambda(Object Expr) throws Cvc3Exception;
+ private static native boolean
+ jniIsApply(Object Expr) throws Cvc3Exception;
+ private static native boolean
+ jniIsSymbol(Object Expr) throws Cvc3Exception;
+ private static native boolean
+ jniIsTheorem(Object Expr) throws Cvc3Exception;
+ private static native boolean
+ jniIsType(Object Expr) throws Cvc3Exception;
+ private static native boolean
+ jniIsTerm(Object Expr) throws Cvc3Exception;
+ private static native boolean
+ jniIsAtomic(Object Expr) throws Cvc3Exception;
+ private static native boolean
+ jniIsAtomicFormula(Object Expr) throws Cvc3Exception;
+ private static native boolean
+ jniIsAbsAtomicFormula(Object Expr) throws Cvc3Exception;
+ private static native boolean
+ jniIsLiteral(Object Expr) throws Cvc3Exception;
+ private static native boolean
+ jniIsAbsLiteral(Object Expr) throws Cvc3Exception;
+ private static native boolean
+ jniIsBoolConnective(Object Expr) throws Cvc3Exception;
+ private static native boolean
+ jniIsPropAtom(Object Expr) throws Cvc3Exception;
+ private static native boolean
+ jniIsPropLiteral(Object Expr) throws Cvc3Exception;
+ private static native boolean
+ jniIsArrayLiteral(Object Expr) throws Cvc3Exception;
+ private static native boolean
+ jniIsEq(Object Expr) throws Cvc3Exception;
+ private static native boolean
+ jniIsNot(Object Expr) throws Cvc3Exception;
+ private static native boolean
+ jniIsAnd(Object Expr) throws Cvc3Exception;
+ private static native boolean
+ jniIsOr(Object Expr) throws Cvc3Exception;
+ private static native boolean
+ jniIsITE(Object Expr) throws Cvc3Exception;
+ private static native boolean
+ jniIsIff(Object Expr) throws Cvc3Exception;
+ private static native boolean
+ jniIsImpl(Object Expr) throws Cvc3Exception;
+ private static native boolean
+ jniIsXor(Object Expr) throws Cvc3Exception;
+ private static native boolean
+ jniIsForall(Object Expr) throws Cvc3Exception;
+ private static native boolean
+ jniIsExists(Object Expr) throws Cvc3Exception;
+ private static native boolean
+ jniIsRational(Object Expr) throws Cvc3Exception;
+ private static native boolean
+ jniIsUminus(Object Expr) throws Cvc3Exception;
+ private static native boolean
+ jniIsPlus(Object Expr) throws Cvc3Exception;
+ private static native boolean
+ jniIsMinus(Object Expr) throws Cvc3Exception;
+ private static native boolean
+ jniIsMult(Object Expr) throws Cvc3Exception;
+ private static native boolean
+ jniIsPow(Object Expr) throws Cvc3Exception;
+ private static native boolean
+ jniIsDivide(Object Expr) throws Cvc3Exception;
+ private static native boolean
+ jniIsLt(Object Expr) throws Cvc3Exception;
+ private static native boolean
+ jniIsLe(Object Expr) throws Cvc3Exception;
+ private static native boolean
+ jniIsGt(Object Expr) throws Cvc3Exception;
+ private static native boolean
+ jniIsGe(Object Expr) throws Cvc3Exception;
+ private static native boolean
+ jniIsSkolem(Object Expr) throws Cvc3Exception;
+ private static native boolean
+ jniIsRead(Object Expr) throws Cvc3Exception;
+ private static native boolean
+ jniIsWrite(Object Expr) throws Cvc3Exception;
+
+ private static native String
+ jniGetName(Object Expr) throws Cvc3Exception;
+ private static native String
+ jniGetUid(Object Expr) throws Cvc3Exception;
+ private static native String
+ jniGetString(Object Expr) throws Cvc3Exception;
+ private static native Object[]
+ jniGetVars(Object Expr) throws Cvc3Exception;
+ private static native Object
+ jniGetExistential(Object Expr) throws Cvc3Exception;
+ private static native int
+ jniGetBoundIndex(Object Expr) throws Cvc3Exception;
+ private static native Object
+ jniGetBody(Object Expr) throws Cvc3Exception;
+ private static native Object
+ jniGetRational(Object Expr) throws Cvc3Exception;
+ private static native Object[][]
+ jniGetTriggers(Object Expr) throws Cvc3Exception;
+ private static native Object
+ jniGetTheorem(Object Expr) throws Cvc3Exception;
+ private static native Object
+ jniGetType(Object Expr) throws Cvc3Exception;
+ private static native Object
+ jniMkOp(Object Expr) throws Cvc3Exception;
+ private static native Object
+ jniGetOp(Object Expr) throws Cvc3Exception;
+ private static native Object
+ jniGetOpExpr(Object Expr) throws Cvc3Exception;
+
+ private static native boolean
+ jniIsNull(Object Expr) throws Cvc3Exception;
+ private static native int
+ jniArity(Object Expr) throws Cvc3Exception;
+ private static native Object
+ jniGetKid(Object Expr, int i) throws Cvc3Exception;
+ private static native Object[]
+ jniGetKids(Object Expr) throws Cvc3Exception;
+
+ private static native Object
+ jniSubstExpr(Object Expr, Object[] oldExprs, Object[] newExprs) throws Cvc3Exception;
+
+ private static native boolean
+ jniIsBvLt(Object Expr) throws Cvc3Exception;
+ private static native boolean
+ jniIsBvLe(Object Expr) throws Cvc3Exception;
+ private static native boolean
+ jniIsBvGt(Object Expr) throws Cvc3Exception;
+ private static native boolean
+ jniIsBvGe(Object Expr) throws Cvc3Exception;
+ private static native boolean
+ jniIsBvPlus(Object Expr) throws Cvc3Exception;
+ private static native boolean
+ jniIsBvSub(Object Expr) throws Cvc3Exception;
+ private static native boolean
+ jniIsBvConst(Object Expr) throws Cvc3Exception;
+ private static native boolean
+ jniIsBvExtract(Object Expr) throws Cvc3Exception;
+ private static native boolean
+ jniIsBvConcat(Object Expr) throws Cvc3Exception;
+
+
+ /// Constructor
+
+ public Expr(Object Expr, EmbeddedManager embeddedManager) {
+ super(Expr, embeddedManager);
+ }
+
+
+ /// API (immutable)
+
+
+ // 'Problem' with equals/hashCode:
+ // this is based on the wrapped c++ expressions.
+ // as a consequence two Expr objects are equal iff
+ // the wrapped expression is equal,
+ // and are indistinguishable for example in a HashMap.
+
+ public boolean equals(Object o) {
+ if (this == o) return true;
+
+ if (!(o instanceof Expr)) return false;
+ boolean result = false;
+ try {
+ result = jniEquals(embedded(), ((Embedded)o).embedded());
+ } catch (Cvc3Exception e) {
+ assert(false);
+ }
+ return result;
+ }
+
+ // must return the same hash code for two objects if equals returns true
+ public int hashCode() {
+ try {
+ if (!jniIsNull(embedded())) {
+ return jniHash(embedded());
+ }
+ } catch (Cvc3Exception e) {
+ assert(false);
+ }
+ assert(false);
+ return 0;
+ }
+
+ public Expr subst(List oldExprs, List newExprs) throws Cvc3Exception {
+ assert(JniUtils.listInstanceof(oldExprs, Expr.class));
+ assert(JniUtils.listInstanceof(newExprs, Expr.class));
+ return new Expr(jniSubstExpr(embedded(), JniUtils.unembedList(oldExprs),
+ JniUtils.unembedList(newExprs)), embeddedManager());
+ }
+
+ public String toString() {
+ String result = "";
+ try {
+ result = jniToString(embedded());
+ } catch (Cvc3Exception e) {
+ assert(false);
+ }
+ return result;
+ }
+
+ public void print(InputLanguage lang, boolean dagify) throws Cvc3Exception {
+ jniPrint(embedded(), lang.toString(), dagify);
+ }
+
+ public void print(boolean dagify) throws Cvc3Exception {
+ print(InputLanguage.PRESENTATION, dagify);
+ }
+
+ public void print() throws Cvc3Exception {
+ print(false);
+ }
+
+ public String getKind() throws Cvc3Exception {
+ return jniGetKind(embedded());
+ }
+
+ // Core expression testers
+
+
+ public boolean isFalse() throws Cvc3Exception {
+ return jniIsFalse(embedded());
+ }
+
+ public boolean isTrue() throws Cvc3Exception {
+ return jniIsTrue(embedded());
+ }
+
+ public boolean isBooleanConst() throws Cvc3Exception {
+ return jniIsBoolConst(embedded());
+ }
+
+ public boolean isVar() throws Cvc3Exception {
+ return jniIsVar(embedded());
+ }
+
+ public boolean isBoundVar() throws Cvc3Exception {
+ return jniIsBoundVar(embedded());
+ }
+
+ public boolean isString() throws Cvc3Exception {
+ return jniIsString(embedded());
+ }
+
+ public boolean isClosure() throws Cvc3Exception {
+ return jniIsClosure(embedded());
+ }
+
+ public boolean isQuantifier() throws Cvc3Exception {
+ return jniIsQuantifier(embedded());
+ }
+
+ public boolean isLambda() throws Cvc3Exception {
+ return jniIsLambda(embedded());
+ }
+
+ public boolean isApply() throws Cvc3Exception {
+ return jniIsApply(embedded());
+ }
+
+ public boolean isSymbol() throws Cvc3Exception {
+ return jniIsSymbol(embedded());
+ }
+
+ public boolean isTheorem() throws Cvc3Exception {
+ return jniIsTheorem(embedded());
+ }
+
+ public boolean isType() throws Cvc3Exception {
+ return jniIsType(embedded());
+ }
+
+
+
+
+ public boolean isTerm() throws Cvc3Exception {
+ return jniIsTerm(embedded());
+ }
+
+ public boolean isAtomic() throws Cvc3Exception {
+ return jniIsAtomic(embedded());
+ }
+
+ public boolean isAtomicFormula() throws Cvc3Exception {
+ return jniIsAtomicFormula(embedded());
+ }
+
+ public boolean isAbsAtomicFormula() throws Cvc3Exception {
+ return jniIsAbsAtomicFormula(embedded());
+ }
+
+ public boolean isLiteral() throws Cvc3Exception {
+ return jniIsLiteral(embedded());
+ }
+
+ public boolean isAbsLiteral() throws Cvc3Exception {
+ return jniIsAbsLiteral(embedded());
+ }
+
+ public boolean isBoolConnective() throws Cvc3Exception {
+ return jniIsBoolConnective(embedded());
+ }
+
+ public boolean isPropAtom() throws Cvc3Exception {
+ return jniIsPropAtom(embedded());
+ }
+
+ public boolean isPropLiteral() throws Cvc3Exception {
+ return jniIsPropLiteral(embedded());
+ }
+
+ public boolean isArrayLiteral() throws Cvc3Exception {
+ return jniIsArrayLiteral(embedded());
+ }
+
+ public boolean isEq() throws Cvc3Exception {
+ return jniIsEq(embedded());
+ }
+
+ public boolean isNot() throws Cvc3Exception {
+ return jniIsNot(embedded());
+ }
+
+
+ public boolean isAnd() throws Cvc3Exception {
+ return jniIsAnd(embedded());
+ }
+
+
+ public boolean isOr() throws Cvc3Exception {
+ return jniIsOr(embedded());
+ }
+
+
+ public boolean isITE() throws Cvc3Exception {
+ return jniIsITE(embedded());
+ }
+
+
+ public boolean isIff() throws Cvc3Exception {
+ return jniIsIff(embedded());
+ }
+
+
+ public boolean isImpl() throws Cvc3Exception {
+ return jniIsImpl(embedded());
+ }
+
+
+ public boolean isXor() throws Cvc3Exception {
+ return jniIsXor(embedded());
+ }
+
+
+ public boolean isForall() throws Cvc3Exception {
+ return jniIsForall(embedded());
+ }
+
+
+ public boolean isExists() throws Cvc3Exception {
+ return jniIsExists(embedded());
+ }
+
+
+ public boolean isRational() throws Cvc3Exception {
+ return jniIsRational(embedded());
+ }
+
+ public boolean isUminus() throws Cvc3Exception {
+ return jniIsUminus(embedded());
+ }
+
+ public boolean isPlus() throws Cvc3Exception {
+ return jniIsPlus(embedded());
+ }
+
+ public boolean isMinus() throws Cvc3Exception {
+ return jniIsMinus(embedded());
+ }
+
+ public boolean isMult() throws Cvc3Exception {
+ return jniIsMult(embedded());
+ }
+
+ public boolean isPow() throws Cvc3Exception {
+ return jniIsPow(embedded());
+ }
+
+ public boolean isDivide() throws Cvc3Exception {
+ return jniIsDivide(embedded());
+ }
+
+ public boolean isLt() throws Cvc3Exception {
+ return jniIsLt(embedded());
+ }
+
+ public boolean isLe() throws Cvc3Exception {
+ return jniIsLe(embedded());
+ }
+
+ public boolean isGt() throws Cvc3Exception {
+ return jniIsGt(embedded());
+ }
+
+ public boolean isGe() throws Cvc3Exception {
+ return jniIsGe(embedded());
+ }
+
+ public boolean isSkolem() throws Cvc3Exception {
+ return jniIsSkolem(embedded());
+ }
+
+ public boolean isRead() throws Cvc3Exception {
+ return jniIsRead(embedded());
+ }
+
+ public boolean isWrite() throws Cvc3Exception {
+ return jniIsWrite(embedded());
+ }
+
+ public boolean isBvLe() throws Cvc3Exception {
+ return jniIsBvLe(embedded());
+ }
+
+ public boolean isBvLt() throws Cvc3Exception {
+ return jniIsBvLt(embedded());
+ }
+
+ public boolean isBvGe() throws Cvc3Exception {
+ return jniIsBvGe(embedded());
+ }
+
+ public boolean isBvGt() throws Cvc3Exception {
+ return jniIsBvGt(embedded());
+ }
+
+ public boolean isBvPlus() throws Cvc3Exception {
+ return jniIsBvPlus(embedded());
+ }
+
+ public boolean isBvSub() throws Cvc3Exception {
+ return jniIsBvSub(embedded());
+ }
+
+ public boolean isBvConstant() throws Cvc3Exception {
+ return jniIsBvConst(embedded());
+ }
+
+ public boolean isBvConcat() throws Cvc3Exception {
+ return jniIsBvConcat(embedded());
+ }
+
+ public boolean isBvExtract() throws Cvc3Exception {
+ return jniIsBvExtract(embedded());
+ }
+
+
+ public String getName() throws Cvc3Exception {
+ assert(!jniIsNull(embedded()));
+ return jniGetName(embedded());
+ }
+
+ public String getUid() throws Cvc3Exception {
+ assert(jniIsBoundVar(embedded()));
+ return jniGetUid(embedded());
+ }
+
+ public String getString() throws Cvc3Exception {
+ assert(jniIsString(embedded()));
+ return jniGetString(embedded());
+ }
+
+ public List getVars() throws Cvc3Exception {
+ assert(jniIsClosure(embedded()));
+ Object[] vars = jniGetVars(embedded());
+ return JniUtils.embedList(vars, Expr.class, embeddedManager());
+ }
+
+ public List getTriggers() throws Cvc3Exception {
+ assert (jniIsClosure(embedded()));
+ return JniUtils.embedListList(jniGetTriggers(embedded()), Expr.class, embeddedManager());
+ }
+
+ public Expr getExistential() throws Cvc3Exception {
+ assert(jniIsSkolem(embedded()));
+ return new Expr(jniGetExistential(embedded()), embeddedManager());
+ }
+
+ public int getBoundIndex() throws Cvc3Exception {
+ assert(jniIsSkolem(embedded()));
+ return jniGetBoundIndex(embedded());
+ }
+
+ public Expr getBody() throws Cvc3Exception {
+ assert(jniIsClosure(embedded()));
+ return new Expr(jniGetBody(embedded()), embeddedManager());
+ }
+
+ public Rational getRational() throws Cvc3Exception {
+ assert(isRational());
+ return new Rational(jniGetRational(embedded()), embeddedManager());
+ }
+
+ public Theorem getTheorem() throws Cvc3Exception {
+ assert(jniIsTheorem(embedded()));
+ return new Theorem(jniGetTheorem(embedded()), embeddedManager());
+ }
+
+ public TypeMut getType() throws Cvc3Exception {
+ return new TypeMut(jniGetType(embedded()), embeddedManager());
+ }
+
+ public OpMut mkOp() throws Cvc3Exception {
+ return new OpMut(jniMkOp(embedded()), embeddedManager());
+ }
+
+ public OpMut getOp() throws Cvc3Exception {
+ return new OpMut(jniGetOp(embedded()), embeddedManager());
+ }
+
+ public ExprMut getOpExpr() throws Cvc3Exception {
+ return new ExprMut(jniGetOpExpr(embedded()), embeddedManager());
+ }
+
+ public boolean isNull() throws Cvc3Exception {
+ return jniIsNull(embedded());
+ }
+
+ public int arity() throws Cvc3Exception {
+ return jniArity(embedded());
+ }
+
+ public Expr getChild(int i) throws Cvc3Exception {
+ assert(i >= 0 && i < arity());
+ return new Expr(jniGetKid(embedded(), i), embeddedManager());
+ }
+
+ public List getChildren() throws Cvc3Exception {
+ return JniUtils.embedList(jniGetKids(embedded()), Expr.class, embeddedManager());
+ }
+}
--- /dev/null
+package cvc3;
+
+import java.util.*;
+
+public class ExprManager extends Embedded {
+ // jni methods
+ private static native String jniGetInputLanguage(Object ExprManager) throws Cvc3Exception;
+ private static native String jniGetOutputLanguage(Object ExprManager) throws Cvc3Exception;
+
+ /// Constructor
+
+ public ExprManager(Object ExprManager, EmbeddedManager embeddedManager) {
+ super(ExprManager, embeddedManager);
+ }
+
+
+ /// API (immutable)
+
+ public InputLanguage getInputLanguage() throws Cvc3Exception {
+ return InputLanguage.get(jniGetInputLanguage(embedded()));
+ }
+
+ public InputLanguage getOutputLanguage() throws Cvc3Exception {
+ return InputLanguage.get(jniGetOutputLanguage(embedded()));
+ }
+}
--- /dev/null
+package cvc3;
+
+import java.util.*;
+
+public class ExprManagerMut extends ExprManager {
+ // jni methods
+
+ /// Constructor
+
+ public ExprManagerMut(Object ExprManagerMut, EmbeddedManager embeddedManager) {
+ super(ExprManagerMut, embeddedManager);
+ }
+
+
+ /// API (mutable)
+}
--- /dev/null
+DEFINITION: Java_cvc3_ExprManager_jniGetInputLanguage
+jstring c ExprManager exprManager
+return toJava(env, exprManager->getInputLang());
+
+DEFINITION: Java_cvc3_ExprManager_jniGetOutputLanguage
+jstring c ExprManager exprManager
+return toJava(env, exprManager->getOutputLang());
--- /dev/null
+package cvc3;
+
+import java.util.*;
+
+public class ExprMut extends Expr {
+ // jni methods
+
+
+ /// Constructor
+
+ // create embedded object
+ public ExprMut(Object ExprMut, EmbeddedManager embeddedManager) {
+ super(ExprMut, embeddedManager);
+ }
+
+
+ /// API (mutable)
+}
--- /dev/null
+INCLUDE: <expr.h>
+INCLUDE: <theory_array.h>
+INCLUDE: <theory_arith.h>
+INCLUDE: <theory_bitvector.h>
+
+DEFINITION: Java_cvc3_Expr_jniEquals
+jboolean c Expr expr1 c Expr expr2
+return *expr1 == *expr2;
+
+DEFINITION: Java_cvc3_Expr_jniToString
+jstring c Expr expr
+return toJava(env, expr->toString());
+
+DEFINITION: Java_cvc3_Expr_jniPrint
+void c Expr expr n string lang n bool dagify
+dagify ? expr->pprint() : expr->pprintnodag();
+
+DEFINITION: Java_cvc3_Expr_jniHash
+jint c Expr expr
+return expr->hash();
+
+DEFINITION: Java_cvc3_Expr_jniGetKind
+jstring c Expr expr
+return toJava(env, expr->getEM()->getKindName( expr->getKind() ));
+
+DEFINITION: Java_cvc3_Expr_jniIsFalse
+jboolean c Expr expr
+return expr->isFalse();
+
+DEFINITION: Java_cvc3_Expr_jniIsTrue
+jboolean c Expr expr
+return expr->isTrue();
+
+DEFINITION: Java_cvc3_Expr_jniIsBoolConst
+jboolean c Expr expr
+return expr->isBoolConst();
+
+DEFINITION: Java_cvc3_Expr_jniIsVar
+jboolean c Expr expr
+return expr->isVar();
+
+DEFINITION: Java_cvc3_Expr_jniIsBoundVar
+jboolean c Expr expr
+return expr->isBoundVar();
+
+DEFINITION: Java_cvc3_Expr_jniIsString
+jboolean c Expr expr
+return expr->isString();
+
+DEFINITION: Java_cvc3_Expr_jniIsClosure
+jboolean c Expr expr
+return expr->isClosure();
+
+DEFINITION: Java_cvc3_Expr_jniIsQuantifier
+jboolean c Expr expr
+return expr->isQuantifier();
+
+DEFINITION: Java_cvc3_Expr_jniIsLambda
+jboolean c Expr expr
+return expr->isLambda();
+
+DEFINITION: Java_cvc3_Expr_jniIsApply
+jboolean c Expr expr
+return expr->isApply();
+
+DEFINITION: Java_cvc3_Expr_jniIsSymbol
+jboolean c Expr expr
+return expr->isSymbol();
+
+DEFINITION: Java_cvc3_Expr_jniIsTheorem
+jboolean c Expr expr
+return expr->isTheorem();
+
+DEFINITION: Java_cvc3_Expr_jniIsType
+jboolean c Expr expr
+return expr->isType();
+
+
+
+DEFINITION: Java_cvc3_Expr_jniIsTerm
+jboolean c Expr expr
+return expr->isTerm();
+
+DEFINITION: Java_cvc3_Expr_jniIsAtomic
+jboolean c Expr expr
+return expr->isAtomic();
+
+DEFINITION: Java_cvc3_Expr_jniIsAtomicFormula
+jboolean c Expr expr
+return expr->isAtomicFormula();
+
+DEFINITION: Java_cvc3_Expr_jniIsAbsAtomicFormula
+jboolean c Expr expr
+return expr->isAbsAtomicFormula();
+
+DEFINITION: Java_cvc3_Expr_jniIsLiteral
+jboolean c Expr expr
+return expr->isLiteral();
+
+DEFINITION: Java_cvc3_Expr_jniIsAbsLiteral
+jboolean c Expr expr
+return expr->isAbsLiteral();
+
+DEFINITION: Java_cvc3_Expr_jniIsBoolConnective
+jboolean c Expr expr
+return expr->isBoolConnective();
+
+DEFINITION: Java_cvc3_Expr_jniIsPropAtom
+jboolean c Expr expr
+return expr->isPropAtom();
+
+DEFINITION: Java_cvc3_Expr_jniIsPropLiteral
+jboolean c Expr expr
+return expr->isPropLiteral();
+
+DEFINITION: Java_cvc3_Expr_jniIsArrayLiteral
+jboolean c Expr expr
+return CVC3::isArrayLiteral(*expr);
+
+
+DEFINITION: Java_cvc3_Expr_jniIsEq
+jboolean c Expr expr
+return expr->isEq();
+
+DEFINITION: Java_cvc3_Expr_jniIsNot
+jboolean c Expr expr
+return expr->isNot();
+
+DEFINITION: Java_cvc3_Expr_jniIsAnd
+jboolean c Expr expr
+return expr->isAnd();
+
+DEFINITION: Java_cvc3_Expr_jniIsOr
+jboolean c Expr expr
+return expr->isOr();
+
+DEFINITION: Java_cvc3_Expr_jniIsITE
+jboolean c Expr expr
+return expr->isITE();
+
+DEFINITION: Java_cvc3_Expr_jniIsIff
+jboolean c Expr expr
+return expr->isIff();
+
+DEFINITION: Java_cvc3_Expr_jniIsImpl
+jboolean c Expr expr
+return expr->isImpl();
+
+DEFINITION: Java_cvc3_Expr_jniIsXor
+jboolean c Expr expr
+return expr->isXor();
+
+DEFINITION: Java_cvc3_Expr_jniIsForall
+jboolean c Expr expr
+return expr->isForall();
+
+DEFINITION: Java_cvc3_Expr_jniIsExists
+jboolean c Expr expr
+return expr->isExists();
+
+DEFINITION: Java_cvc3_Expr_jniIsRational
+jboolean c Expr expr
+return expr->isRational();
+
+DEFINITION: Java_cvc3_Expr_jniIsUminus
+jboolean c Expr expr
+return expr->getKind() == UMINUS;
+
+DEFINITION: Java_cvc3_Expr_jniIsPlus
+jboolean c Expr expr
+return expr->getKind() == PLUS;
+
+DEFINITION: Java_cvc3_Expr_jniIsMinus
+jboolean c Expr expr
+return expr->getKind() == MINUS;
+
+DEFINITION: Java_cvc3_Expr_jniIsMult
+jboolean c Expr expr
+return expr->getKind() == MULT;
+
+DEFINITION: Java_cvc3_Expr_jniIsPow
+jboolean c Expr expr
+return expr->getKind() == POW;
+
+DEFINITION: Java_cvc3_Expr_jniIsDivide
+jboolean c Expr expr
+return expr->getKind() == DIVIDE;
+
+DEFINITION: Java_cvc3_Expr_jniIsLt
+jboolean c Expr expr
+return expr->getKind() == LT;
+
+DEFINITION: Java_cvc3_Expr_jniIsLe
+jboolean c Expr expr
+return expr->getKind() == LE;
+
+DEFINITION: Java_cvc3_Expr_jniIsGt
+jboolean c Expr expr
+return expr->getKind() == GT;
+
+DEFINITION: Java_cvc3_Expr_jniIsGe
+jboolean c Expr expr
+return expr->getKind() == GE;
+
+DEFINITION: Java_cvc3_Expr_jniIsSkolem
+jboolean c Expr expr
+return expr->isSkolem();
+
+
+DEFINITION: Java_cvc3_Expr_jniIsRead
+jboolean c Expr expr
+return expr->getKind() == READ;
+
+DEFINITION: Java_cvc3_Expr_jniIsWrite
+jboolean c Expr expr
+return expr->getKind() == WRITE;
+
+
+DEFINITION: Java_cvc3_Expr_jniGetName
+jstring c Expr expr
+return toJava(env, expr->getName());
+
+DEFINITION: Java_cvc3_Expr_jniGetUid
+jstring c Expr expr
+return toJava(env, expr->getUid());
+
+DEFINITION: Java_cvc3_Expr_jniGetString
+jstring c Expr expr
+return toJava(env, expr->getString());
+
+DEFINITION: Java_cvc3_Expr_jniGetVars
+jobjectArray c Expr expr
+return toJavaVConstRef(env, expr->getVars());
+
+DEFINITION: Java_cvc3_Expr_jniGetExistential
+jobject c Expr expr
+return embed_const_ref<Expr>(env, &expr->getExistential());
+
+DEFINITION: Java_cvc3_Expr_jniGetBoundIndex
+jint c Expr expr
+return expr->getBoundIndex();
+
+DEFINITION: Java_cvc3_Expr_jniGetBody
+jobject c Expr expr
+return embed_const_ref<Expr>(env, &expr->getBody());
+
+DEFINITION: Java_cvc3_Expr_jniGetRational
+jobject c Expr expr
+return embed_const_ref<Rational>(env, &expr->getRational());
+
+DEFINITION: Java_cvc3_Expr_jniGetTriggers
+jobjectArray c Expr expr
+return toJavaVVConstRef(env, expr->getTriggers());
+
+DEFINITION: Java_cvc3_Expr_jniGetTheorem
+jobject c Expr expr
+return embed_const_ref<Theorem>(env, &expr->getTheorem());
+
+DEFINITION: Java_cvc3_Expr_jniGetType
+jobject c Expr expr
+return embed_copy<Type>(env, expr->getType());
+
+DEFINITION: Java_cvc3_Expr_jniMkOp
+jobject c Expr expr
+return embed_copy<Op>(env, expr->mkOp());
+
+DEFINITION: Java_cvc3_Expr_jniGetOp
+jobject c Expr expr
+return embed_copy<Op>(env, expr->getOp());
+
+DEFINITION: Java_cvc3_Expr_jniGetOpExpr
+jobject c Expr expr
+return embed_copy<Expr>(env, expr->getOpExpr());
+
+DEFINITION: Java_cvc3_Expr_jniIsNull
+jboolean c Expr expr
+return expr->isNull();
+
+DEFINITION: Java_cvc3_Expr_jniArity
+jint c Expr expr
+return expr->arity();
+
+DEFINITION: Java_cvc3_Expr_jniGetKid
+jobject c Expr expr n int i
+return embed_const_ref<Expr>(env, &((*expr)[ji]));
+
+DEFINITION: Java_cvc3_Expr_jniGetKids
+jobjectArray c Expr expr
+return toJavaVConstRef(env, expr->getKids());
+
+DEFINITION: Java_cvc3_Expr_jniSubstExpr
+jobject c Expr e cv Expr oldExprs cv Expr newExprs
+return embed_copy(env, e->substExpr(oldExprs,newExprs));
+
+DEFINITION: Java_cvc3_Expr_jniIsBvLt
+jboolean c Expr expr
+return expr->getKind() == BVLT;
+
+DEFINITION: Java_cvc3_Expr_jniIsBvLe
+jboolean c Expr expr
+return expr->getKind() == BVLE;
+
+DEFINITION: Java_cvc3_Expr_jniIsBvGt
+jboolean c Expr expr
+return expr->getKind() == BVGT;
+
+DEFINITION: Java_cvc3_Expr_jniIsBvGe
+jboolean c Expr expr
+return expr->getKind() == BVGE;
+
+DEFINITION: Java_cvc3_Expr_jniIsBvPlus
+jboolean c Expr expr
+return expr->getKind() == BVPLUS;
+
+DEFINITION: Java_cvc3_Expr_jniIsBvSub
+jboolean c Expr expr
+return expr->getKind() == BVSUB;
+
+DEFINITION: Java_cvc3_Expr_jniIsBvConst
+jboolean c Expr expr
+return expr->getKind() == BVCONST;
+
+DEFINITION: Java_cvc3_Expr_jniIsBvExtract
+jboolean c Expr expr
+return expr->getKind() == EXTRACT;
+
+DEFINITION: Java_cvc3_Expr_jniIsBvConcat
+jboolean c Expr expr
+return expr->getKind() == CONCAT;
--- /dev/null
+package cvc3;
+
+import java.util.*;
+
+public class Flag extends Embedded {
+ // jni methods
+ private static native boolean jniIsNull(Object Flag) throws Cvc3Exception;
+ private static native boolean jniIsBool(Object Flag) throws Cvc3Exception;
+ private static native boolean jniIsInt(Object Flag) throws Cvc3Exception;
+ private static native boolean jniIsString(Object Flag) throws Cvc3Exception;
+ private static native boolean jniIsStringVec(Object Flag) throws Cvc3Exception;
+ private static native boolean jniGetBool(Object Flag) throws Cvc3Exception;
+ private static native int jniGetInt(Object Flag) throws Cvc3Exception;
+ private static native String jniGetString(Object Flag) throws Cvc3Exception;
+ private static native String jniGetHelp(Object Flag) throws Cvc3Exception;
+
+
+ /// Constructor
+
+ // create embedded object
+ public Flag(Object Flag, EmbeddedManager embeddedManager) {
+ super(Flag, embeddedManager);
+ }
+
+
+ /// API immutable
+
+ boolean isNull() throws Cvc3Exception {
+ return jniIsNull(embedded());
+ }
+
+ boolean isBool() throws Cvc3Exception {
+ return jniIsBool(embedded());
+ }
+
+ boolean isInt() throws Cvc3Exception {
+ return jniIsInt(embedded());
+ }
+
+ boolean isString() throws Cvc3Exception {
+ return jniIsString(embedded());
+ }
+
+ boolean isStringVec() throws Cvc3Exception {
+ return jniIsStringVec(embedded());
+ }
+
+ boolean getBool() throws Cvc3Exception {
+ return jniGetBool(embedded());
+ }
+
+ int getInt() throws Cvc3Exception {
+ return jniGetInt(embedded());
+ }
+
+ String getString() throws Cvc3Exception {
+ return jniGetString(embedded());
+ }
+
+ String getHelp() throws Cvc3Exception {
+ return jniGetHelp(embedded());
+ }
+}
--- /dev/null
+package cvc3;
+
+import java.util.*;
+
+public class FlagException extends Cvc3Exception {
+
+ private final static long serialVersionUID = 1L;
+
+ public FlagException(String message) {
+ super(message);
+ }
+}
--- /dev/null
+DEFINITION: Java_cvc3_Flag_jniIsNull
+jboolean c CLFlag flag
+return (flag->getType() == CLFLAG_NULL);
+
+DEFINITION: Java_cvc3_Flag_jniIsBool
+jboolean c CLFlag flag
+return (flag->getType() == CLFLAG_BOOL);
+
+DEFINITION: Java_cvc3_Flag_jniIsInt
+jboolean c CLFlag flag
+return (flag->getType() == CLFLAG_INT);
+
+DEFINITION: Java_cvc3_Flag_jniIsString
+jboolean c CLFlag flag
+return (flag->getType() == CLFLAG_STRING);
+
+DEFINITION: Java_cvc3_Flag_jniIsStringVec
+jboolean c CLFlag flag
+return (flag->getType() == CLFLAG_STRVEC);
+
+
+DEFINITION: Java_cvc3_Flag_jniGetBool
+jboolean c CLFlag flag
+return flag->getBool();
+
+DEFINITION: Java_cvc3_Flag_jniGetInt
+jint c CLFlag flag
+return flag->getInt();
+
+DEFINITION: Java_cvc3_Flag_jniGetString
+jstring c CLFlag flag
+return toJava(env, flag->getString());
+
+DEFINITION: Java_cvc3_Flag_jniGetHelp
+jstring c CLFlag flag
+return toJava(env, flag->getHelp());
--- /dev/null
+package cvc3;
+
+import java.util.*;
+
+public abstract class Flags extends Embedded {
+ // jni methods
+ private static native Object[] jniGetFlags(Object Flags, String prefix) throws Cvc3Exception;
+ private static native Object jniGetFlag(Object Flags, String name) throws Cvc3Exception;
+
+
+ /// Constructor
+
+ // create embedded object
+ public Flags(Object Flags, EmbeddedManager embeddedManager) {
+ super(Flags, embeddedManager);
+ }
+
+ /// API (immutable)
+
+
+ // get names of all flags starting with prefix
+ public List getFlags(String prefix) throws Cvc3Exception {
+ Object[] flags = jniGetFlags(embedded(), prefix);
+ assert(flags instanceof String[]);
+ return Arrays.asList(flags);
+ }
+
+ // get the value of a flag by name (without prefix -/+)
+ public Flag getFlag(String name) throws Cvc3Exception {
+ return new Flag(jniGetFlag(embedded(), name), embeddedManager());
+ }
+}
--- /dev/null
+package cvc3;
+
+import java.util.*;
+
+public class FlagsMut extends Flags {
+ // jni methods
+ private static native void jniSetFlag1(Object Flags, String name, boolean value) throws Cvc3Exception;
+ private static native void jniSetFlag2(Object Flags, String name, int value) throws Cvc3Exception;
+ private static native void jniSetFlag3(Object Flags, String name, String value) throws Cvc3Exception;
+ private static native void jniSetFlag4(Object Flags, String map, String name, boolean value) throws Cvc3Exception;
+
+
+ /// Constructor
+
+ // create embedded object
+ public FlagsMut(Object FlagsMut, EmbeddedManager embeddedManager) {
+ super(FlagsMut, embeddedManager);
+ }
+
+
+ /// API (mutable)
+
+ public void setFlag(String name, boolean value) throws Cvc3Exception {
+ jniSetFlag1(embedded(), name, value);
+ }
+
+ public void setFlag(String name, int value) throws Cvc3Exception {
+ jniSetFlag2(embedded(), name, value);
+ }
+
+ public void setFlag(String name, String value) throws Cvc3Exception {
+ jniSetFlag3(embedded(), name, value);
+ }
+
+ // flag representing set of options, e.g. trace
+ public void setFlag(String map, String name, boolean value) throws Cvc3Exception {
+ jniSetFlag4(embedded(), map, name, value);
+ }
+}
--- /dev/null
+DEFINITION: Java_cvc3_FlagsMut_jniSetFlag1
+void m CLFlags flags n string name n bool value
+flags->setFlag(name, value);
+
+DEFINITION: Java_cvc3_FlagsMut_jniSetFlag2
+void m CLFlags flags n string name n int value
+flags->setFlag(name, value);
+
+DEFINITION: Java_cvc3_FlagsMut_jniSetFlag3
+void m CLFlags flags n string name n string value
+flags->setFlag(name, value);
+
+DEFINITION: Java_cvc3_FlagsMut_jniSetFlag4
+void m CLFlags flags n string map n string name n bool value
+flags->setFlag(map, std::make_pair(name, value));
--- /dev/null
+DEFINITION: Java_cvc3_Flags_jniGetFlags
+jobjectArray c CLFlags flags n string prefix
+
+// get flag names
+vector<string> names;
+flags->countFlags(prefix, names);
+return toJavaV(env, names);
+
+
+DEFINITION: Java_cvc3_Flags_jniGetFlag
+jobject c CLFlags flags n string name
+const CLFlag& flag = flags->getFlag(name);
+return embed_const_ref(env, &flag);
--- /dev/null
+package cvc3;
+
+import java.util.*;
+
+/** A truth value of a formula. */
+public class FormulaValue {
+ private final String d_result;
+
+ protected FormulaValue(String result) {
+ d_result = result;
+ }
+
+
+ // names of c++ enum values
+ public static final FormulaValue TRUE = new FormulaValue("TRUE_VAL");
+ public static final FormulaValue FALSE = new FormulaValue("FALSE_VAL");
+ public static final FormulaValue UNKNOWN = new FormulaValue("UNKNOWN_VAL");
+
+ // the FormulaValue corresponding to a c++ enum value by name
+ public static FormulaValue get(String value) throws DebugException {
+ if (value.equals(TRUE.toString())) {
+ return TRUE;
+ } else if (value.equals(FALSE.toString())) {
+ return FALSE;
+ } else if (value.equals(UNKNOWN.toString())) {
+ return UNKNOWN;
+ } else {
+ throw new DebugException("FormulaValue.constructor: unknown enum value: " + value);
+ }
+ }
+
+ // the FormulaValue's c++ enum value
+ public String toString() {
+ return d_result;
+ }
+}
--- /dev/null
+package cvc3;
+
+import java.util.*;
+
+/** See comments about mapping c++ enums to java in QueryResult */
+public class InputLanguage {
+ private final String d_lang;
+
+ private InputLanguage(String lang) {
+ d_lang = lang;
+ }
+
+
+ // names of c++ enum values
+ public static final InputLanguage PRESENTATION = new InputLanguage("PRESENTATION");
+ public static final InputLanguage SMTLIB = new InputLanguage("SMTLIB");
+ public static final InputLanguage LISP = new InputLanguage("LISP");
+
+ // the InputLanguage corresponding to a c++ enum value by name
+ public static InputLanguage get(String value) throws DebugException {
+ if (value.equals(PRESENTATION.toString())) {
+ return PRESENTATION;
+ } else if (value.equals(SMTLIB.toString())) {
+ return SMTLIB;
+ } else if (value.equals(LISP.toString())) {
+ return LISP;
+ } else {
+ throw new DebugException("InputLanguage.constructor: unknown enum value: " + value);
+ }
+ }
+
+ // the InputLanguage's c++ enum value
+ public String toString() {
+ return d_lang;
+ }
+}
--- /dev/null
+#include "JniUtils.h"
+
+// for CVC4: removed; don't need these
+//#include <typecheck_exception.h>
+//#include <sound_exception.h>
+//#include <eval_exception.h>
+//#include <command_line_exception.h>
+//#include <parser_exception.h>
+//#include <smtlib_exception.h>
+
+// for CVC4: need these for compatibility layer
+#include "compat/cvc3_compat.h"
+#include "Embedded.h"
+
+using namespace std;
+using namespace CVC3;
+
+namespace Java_cvc3_JniUtils {
+
+ /// Embedding of c++ objects in java objects
+
+ Embedded* unembed(JNIEnv* env, jobject jobj) {
+ Embedded* embedded = (Embedded*) env->GetDirectBufferAddress(jobj);
+ DebugAssert(embedded != NULL, "JniUtils::unembed: embedded object is NULL");
+ return embedded;
+ }
+
+ void deleteEmbedded(JNIEnv* env, jobject jobj) {
+ Embedded* embedded = unembed(env, jobj);
+ DebugAssert(embedded != NULL, "JniUtils::deleteEmbedded: embedded object is NULL");
+ delete embedded;
+ }
+
+
+
+ /// Conversions between c++ and java
+
+ bool toCpp(jboolean j) {
+ return (bool)j;
+ }
+
+ jstring toJava(JNIEnv* env, const string& cstring) {
+ return env->NewStringUTF(cstring.c_str());
+ }
+
+ jstring toJava(JNIEnv* env, const char* cstring) {
+ return env->NewStringUTF(cstring);
+ }
+
+ string toCpp(JNIEnv* env, const jstring& jstring) {
+ const char* cstring = env->GetStringUTFChars(jstring, NULL);
+ string string(cstring);
+ env->ReleaseStringUTFChars(jstring, cstring);
+ return string;
+ }
+
+ jstring toJava(JNIEnv* env, CVC3::QueryResult result) {
+ switch (result) {
+ case SATISFIABLE: return toJava(env, "SATISFIABLE");
+ case UNSATISFIABLE: return toJava(env, "UNSATISFIABLE");
+ case ABORT: return toJava(env, "ABORT");
+ case UNKNOWN: return toJava(env, "UNKNOWN");
+ }
+
+ DebugAssert(false, "JniUtils::toJava(QueryResult): unreachable");
+ }
+
+ jstring toJava(JNIEnv* env, CVC3::FormulaValue result) {
+ switch (result) {
+ case TRUE_VAL: return toJava(env, "TRUE_VAL");
+ case FALSE_VAL: return toJava(env, "FALSE_VAL");
+ case UNKNOWN_VAL: return toJava(env, "UNKNOWN_VAL");
+ }
+
+ DebugAssert(false, "JniUtils::toJava(FormulaValue): unreachable");
+ }
+
+ jstring toJava(JNIEnv* env, CVC3::InputLanguage lang) {
+ switch (lang) {
+ case PRESENTATION_LANG: return toJava(env, "PRESENTATION");
+ case SMTLIB_LANG: return toJava(env, "SMTLIB");
+ case LISP_LANG: return toJava(env, "LISP");
+ }
+
+ DebugAssert(false, "JniUtils::toJava(InputLanguage): unreachable");
+ }
+
+ InputLanguage toCppInputLanguage(JNIEnv* env, const string& lang) {
+ if (lang.compare("PRESENTATION") == 0) {
+ return PRESENTATION_LANG;
+ } else if (lang.compare("SMTLIB") == 0) {
+ return SMTLIB_LANG;
+ } else if (lang.compare("LISP") == 0) {
+ return LISP_LANG;
+ }
+
+ DebugAssert(false, "JniUtils::toCpp(InputLanguage): unreachable");
+ }
+
+ void toJava(JNIEnv* env, const Exception& e) {
+ /* for CVC4: don't worry about legacy exception mapping
+ string exceptionName("cvc3/");
+ if (dynamic_cast<const TypecheckException*>(&e) != NULL) {
+ exceptionName += "TypecheckException";
+ } else if (dynamic_cast<const CVC3::SoundException*>(&e) != NULL) {
+ exceptionName += "SoundException";
+ } else if (dynamic_cast<const CVC3::EvalException*>(&e) != NULL) {
+ exceptionName += "EvalException";
+ } else if (dynamic_cast<const CVC3::CLException*>(&e) != NULL) {
+ exceptionName += "CLException";
+ } else if (dynamic_cast<const CVC3::ParserException*>(&e) != NULL) {
+ exceptionName += "ParserException";
+ } else if (dynamic_cast<const CVC3::SmtlibException*>(&e) != NULL) {
+ exceptionName += "SmtlibException";
+ } else if (dynamic_cast<const CVC3::DebugException*>(&e) != NULL) {
+ exceptionName += "DebugException";
+ } else {
+ exceptionName += "Cvc3Exception";
+ }
+ */
+
+ jclass exceptionClass = env->FindClass("java/lang/RuntimeException");
+ // queues up the exception in the Java layer
+ env->ThrowNew(exceptionClass, e.toString().c_str());
+ }
+
+
+ vector<string> toCppV(JNIEnv* env, const jobjectArray& jarray) {
+ vector<string> v;
+ int length = env->GetArrayLength(jarray);
+ for (int i = 0; i < length; ++i) {
+ v.push_back(toCpp(env, (jstring)env->GetObjectArrayElement(jarray, i)));
+ }
+ return v;
+ }
+
+ vector<vector<string> > toCppVV(JNIEnv* env, const jobjectArray& jarray) {
+ vector<vector<string> > v;
+ int length = env->GetArrayLength(jarray);
+ for (int i = 0; i < length; ++i) {
+ jobjectArray jsub = static_cast<jobjectArray>(env->GetObjectArrayElement(jarray, i));
+ v.push_back(toCppV(env, jsub));
+ }
+ return v;
+ }
+
+ vector<vector<vector<string> > > toCppVVV(JNIEnv* env, const jobjectArray& jarray) {
+ vector<vector<vector<string> > > v;
+ int length = env->GetArrayLength(jarray);
+ for (int i = 0; i < length; ++i) {
+ jobjectArray jsub = static_cast<jobjectArray>(env->GetObjectArrayElement(jarray, i));
+ v.push_back(toCppVV(env, jsub));
+ }
+ return v;
+ }
+
+ jobjectArray toJavaV(JNIEnv* env, const vector<string>& v) {
+ jobjectArray jarray = (jobjectArray)
+ env->NewObjectArray(
+ v.size(),
+ env->FindClass("java/lang/String"),
+ env->NewStringUTF(""));
+
+ for(int i = 0; i < v.size(); ++i) {
+ env->SetObjectArrayElement(jarray, i, toJava(env, v[i]));
+ }
+
+ return jarray;
+ }
+
+
+ vector<bool> toCppV(JNIEnv* env, const jbooleanArray& jarray) {
+ int length = env->GetArrayLength(jarray);
+ jboolean* jboolean = env->GetBooleanArrayElements(jarray, NULL);
+
+ vector<bool> v;
+ for (int i = 0; i < length; ++i) {
+ v.push_back(jboolean[i]);
+ }
+ env->ReleaseBooleanArrayElements(jarray, jboolean, JNI_ABORT);
+
+ return v;
+ }
+}
--- /dev/null
+package cvc3;
+
+import java.util.*;
+import java.lang.reflect.Constructor;
+
+public class JniUtils {
+
+ // check that list is an instance of a class -
+ // generics would avoid that
+ public static boolean listInstanceof(List list, Class c) {
+ Iterator i = list.iterator();
+ while (i.hasNext()) {
+ if (!(c.isInstance(i.next()))) return false;
+ }
+ return true;
+ }
+
+ public static boolean listListInstanceof(List listList, Class c) {
+ Iterator i = listList.iterator();
+ while (i.hasNext()) {
+ Object list = i.next();
+ assert(list instanceof List);
+ if (!(listInstanceof((List)list, c))) return false;
+ }
+ return true;
+ }
+
+ public static boolean listListListInstanceof(List listListList, Class c) {
+ Iterator i = listListList.iterator();
+ while (i.hasNext()) {
+ Object list = i.next();
+ assert(list instanceof List);
+ if (!(listListInstanceof((List)list, c))) return false;
+ }
+ return true;
+ }
+
+
+ // embed an array of c++ objects in a list
+ public static List embedList(Object[] cobjects, Class c, EmbeddedManager embeddedManager) {
+ List embedded = new ArrayList();
+
+ try {
+ Class[] argsC = new Class[2];
+ argsC[0] = Object.class;
+ argsC[1] = EmbeddedManager.class;
+ Constructor constr = c.getConstructor(argsC);
+
+ Object[] args = new Object[2];
+ for (int i = 0; i < cobjects.length; ++i) {
+ args[0] = cobjects[i];
+ args[1] = embeddedManager;
+ embedded.add(constr.newInstance(args));
+ }
+ } catch (NoSuchMethodException e) {
+ System.out.println(e);
+ assert(false);
+ } catch (InstantiationException e) {
+ System.out.println(e);
+ assert(false);
+ } catch (IllegalAccessException e) {
+ System.out.println(e);
+ assert(false);
+ } catch (java.lang.reflect.InvocationTargetException e) {
+ System.out.println(e);
+ assert(false);
+ }
+ return embedded;
+ }
+
+ public static List embedListList(Object[][] cobjects, Class c, EmbeddedManager embeddedManager) {
+ List embedded = new ArrayList(cobjects.length);
+ for (int i = 0; i < cobjects.length; ++i) {
+ Object[] cobject = cobjects[i];
+ embedded.add( embedList(cobject,c,embeddedManager) );
+ }
+ return embedded;
+ }
+
+ // embed an array of c++ objects in a hash map
+ public static HashMap embedHashMap(Object[] cobjects, Class ck, Class cv,
+ EmbeddedManager embeddedManager) {
+ HashMap embedded = new HashMap(cobjects.length / 2);
+
+ try {
+ Class[] argsCK = new Class[2];
+ argsCK[0] = Object.class;
+ argsCK[1] = EmbeddedManager.class;
+ Constructor constrK = ck.getConstructor(argsCK);
+
+ Class[] argsCV = new Class[2];
+ argsCV[0] = Object.class;
+ argsCV[1] = EmbeddedManager.class;
+ Constructor constrV = cv.getConstructor(argsCV);
+
+ Object[] argsK = new Object[2];
+ Object[] argsV = new Object[2];
+ for (int i = 0; i < cobjects.length; ++i) {
+ argsK[0] = cobjects[i];
+ argsK[1] = embeddedManager;
+
+ ++i;
+ assert(i < cobjects.length);
+ argsV[0] = cobjects[i];
+ argsV[1] = embeddedManager;
+
+ embedded.put(constrK.newInstance(argsK), constrV.newInstance(argsV));
+ }
+ } catch (NoSuchMethodException e) {
+ System.out.println(e);
+ assert(false);
+ } catch (InstantiationException e) {
+ System.out.println(e);
+ assert(false);
+ } catch (IllegalAccessException e) {
+ System.out.println(e);
+ assert(false);
+ } catch (java.lang.reflect.InvocationTargetException e) {
+ System.out.println(e);
+ assert(false);
+ }
+ return embedded;
+ }
+
+
+ // unembed a list of Embedded objects to a list
+ public static Object[] unembedList(List embedded) {
+ Object[] unembedded = new Object[embedded.size()];
+
+ for (int i = 0; i < embedded.size(); ++i) {
+ assert(embedded.get(i) instanceof Embedded);
+ unembedded[i] = ((Embedded)embedded.get(i)).embedded();
+ }
+
+ return unembedded;
+ }
+
+ public static Object[][] unembedListList(List embedded) {
+ Object[][] unembedded = new Object[embedded.size()][];
+
+ for (int i = 0; i < embedded.size(); ++i) {
+ Object list = embedded.get(i);
+ assert(list instanceof List);
+ unembedded[i] = unembedList((List)list);
+ }
+
+ return unembedded;
+ }
+
+ public static Object[][][] unembedListListList(List embedded) {
+ Object[][][] unembedded = new Object[embedded.size()][][];
+
+ for (int i = 0; i < embedded.size(); ++i) {
+ Object list = embedded.get(i);
+ assert(list instanceof List);
+ unembedded[i] = unembedListList((List)list);
+ }
+
+ return unembedded;
+ }
+
+
+ // unembed a list of Embedded objects to a list
+ public static Object[] unembedArray(Object[] embedded) {
+ Object[] unembedded = new Object[embedded.length];
+
+ for (int i = 0; i < embedded.length; ++i) {
+ assert(embedded[i] instanceof Embedded);
+ unembedded[i] = ((Embedded)embedded[i]).embedded();
+ }
+
+ return unembedded;
+ }
+
+ public static Object[] unembedArrayArray(Object[][] embedded) {
+ Object[] unembedded = new Object[embedded.length];
+
+ for (int i = 0; i < embedded.length; ++i) {
+ unembedded[i] = unembedArray(embedded[i]);
+ }
+
+ return unembedded;
+ }
+
+ public static Object[] unembedArrayArrayArray(Object[][][] embedded) {
+ Object[] unembedded = new Object[embedded.length];
+
+ for (int i = 0; i < embedded.length; ++i) {
+ unembedded[i] = unembedArrayArray(embedded[i]);
+ }
+
+ return unembedded;
+ }
+
+
+ // copy a list of strings to a list
+ public static Object[] toArray(List list) {
+ assert(listInstanceof(list, String.class));
+ assert(list.isEmpty() || !listInstanceof(list, Embedded.class));
+ return list.toArray();
+ }
+
+ public static Object[] toArrayArray(List listList) {
+ Object[] arrayArray = new Object[listList.size()];
+
+ for (int i = 0; i < listList.size(); ++i) {
+ Object list = listList.get(i);
+ assert(list instanceof List);
+ arrayArray[i] = toArray(((List)list));
+ }
+
+ return arrayArray;
+ }
+
+ public static Object[] toArrayArrayArray(List listListList) {
+ Object[] arrayArrayArray = new Object[listListList.size()];
+
+ for (int i = 0; i < listListList.size(); ++i) {
+ Object list = listListList.get(i);
+ assert(list instanceof List);
+ arrayArrayArray[i] = toArrayArray((List)list);
+ }
+
+ return arrayArrayArray;
+ }
+}
+
--- /dev/null
+package cvc3;
+
+import java.util.*;
+
+public class Op extends Embedded {
+ // jni methods
+ private static native boolean
+ jniEquals(Object Expr1, Object Expr2) throws Cvc3Exception;
+ private static native String
+ jniToString(Object Expr) throws Cvc3Exception;
+
+ private static native Object
+ jniGetExpr(Object op) throws Cvc3Exception;
+ private static native boolean
+ jniIsNull(Object Op) throws Cvc3Exception;
+
+ /// Constructor
+
+ public Op(Object Op, EmbeddedManager embeddedManager) {
+ super(Op, embeddedManager);
+ }
+
+
+ /// API (immutable)
+
+ public boolean equals(Object o) {
+ if (this == o) return true;
+
+ if (!(o instanceof Op)) return false;
+ boolean result = false;
+ try {
+ result = jniEquals(embedded(), ((Embedded)o).embedded());
+ } catch (Cvc3Exception e) {
+ assert(false);
+ }
+ return result;
+ }
+
+ // must return the same hash code for two objects if equals returns true
+ public int hashCode() {
+ try {
+ return getExpr().hashCode();
+ } catch (Cvc3Exception e) {
+ assert(false);
+ }
+ return 0;
+ }
+
+ public String toString() {
+ String result = "";
+ try {
+ result = jniToString(embedded());
+ } catch (Cvc3Exception e) {
+ assert(false);
+ }
+ return result;
+ }
+
+ public ExprMut getExpr() throws Cvc3Exception {
+ return new ExprMut(jniGetExpr(embedded()), embeddedManager());
+ }
+
+ public boolean isNull() throws Cvc3Exception {
+ return jniIsNull(embedded());
+ }
+}
--- /dev/null
+package cvc3;
+
+import java.util.*;
+
+public class OpMut extends Op {
+ // jni methods
+
+
+ /// Constructor
+
+ // create embedded object
+ public OpMut(Object OpMut, EmbeddedManager embeddedManager) {
+ super(OpMut, embeddedManager);
+ }
+
+
+ /// API (mutable)
+}
--- /dev/null
+INCLUDE: <expr_op.h>
+
+DEFINITION: Java_cvc3_Op_jniEquals
+jboolean c Op op1 c Op op2
+return *op1 == *op2;
+
+DEFINITION: Java_cvc3_Op_jniToString
+jstring c Op op
+return toJava(env, op->toString());
+
+
+DEFINITION: Java_cvc3_Op_jniGetExpr
+jobject c Op op
+return embed_const_ref<Expr>(env, &op->getExpr());
+
+DEFINITION: Java_cvc3_Op_jniIsNull
+jboolean c Op op
+return op->isNull();
--- /dev/null
+package cvc3;
+
+import java.util.*;
+
+/** mirrors CVC3::ParserException */
+public class ParserException extends Cvc3Exception {
+
+ private final static long serialVersionUID = 1L;
+
+ public ParserException(String message) {
+ super(message);
+ }
+}
--- /dev/null
+package cvc3;
+
+import java.util.*;
+
+public class Proof extends Embedded {
+ // jni methods
+
+ /// Constructor
+
+ public Proof(Object Proof, EmbeddedManager embeddedManager) {
+ super(Proof, embeddedManager);
+ }
+
+
+ /// API (immutable)
+
+}
--- /dev/null
+package cvc3;
+
+import java.util.*;
+
+public class ProofMut extends Proof {
+ // jni methods
+
+
+ /// Constructor
+
+ // create embedded object
+ public ProofMut(Object ProofMut, EmbeddedManager embeddedManager) {
+ super(ProofMut, embeddedManager);
+ }
+
+
+ /// API (mutable)
+}
--- /dev/null
+package cvc3;
+
+import java.util.*;
+
+/**
+ * QueryResult is an enum in Cvc3, but as we have to use java 1.4 we have to
+ * use one of the usual tricks instead of java's Enum.
+ *
+ * To be independent of changes of the actual values of the c++ enum elements
+ * they are passed by name from the JNI interface, so that changing them will
+ * violently break the code (though unfortunately only at runtime).
+ */
+public class QueryResult {
+ private final String d_result;
+
+ private QueryResult(String result) {
+ d_result = result;
+ }
+
+ // value constants
+ public static final QueryResult INVALID = new QueryResult("INVALID");
+ public static final QueryResult VALID = new QueryResult("VALID");
+ public static final QueryResult ABORT = new QueryResult("ABORT");
+ public static final QueryResult UNKNOWN = new QueryResult("UNKNOWN");
+
+ // names of c++ enum values, CVC3 maps INVALID->SAT and VALID->UNSAT
+ private static Map valueMap = new HashMap() {
+ {
+ put("SATISFIABLE", INVALID);
+ put("UNSATISFIABLE", VALID);
+ put("UNKNOWN", UNKNOWN);
+ put("ABORT", ABORT);
+ }
+
+ public static final long serialVersionUID = 1L;
+ };
+
+ // the QueryResult corresponding to a c++ enum value by name
+ public static QueryResult get(String value) throws DebugException {
+ QueryResult queryResult = (QueryResult) valueMap.get(value);
+ if (queryResult == null) {
+ throw new DebugException("QueryResult.constructor: unknown enum value: "
+ + value);
+ }
+ return queryResult;
+ }
+
+ public String toString() {
+ return d_result;
+ }
+}
--- /dev/null
+package cvc3;
+
+import java.util.*;
+
+public class Rational extends Embedded {
+ // jni methods
+ private static native Object
+ jniRational1(int n, int d) throws Cvc3Exception;
+ private static native Object
+ jniRational2(String n, int base) throws Cvc3Exception;
+ private static native Object
+ jniRational3(String n, String d, int base) throws Cvc3Exception;
+
+ private static native boolean
+ jniEquals(Object Rational1, Object Rational2) throws Cvc3Exception;
+ private static native String
+ jniToString(Object Rational) throws Cvc3Exception;
+ private static native int
+ jniHash(Object Rational) throws Cvc3Exception;
+
+ private static native boolean
+ jniIsLe(Object Rational1, Object Rational2) throws Cvc3Exception;
+ private static native boolean
+ jniIsLt(Object Rational1, Object Rational2) throws Cvc3Exception;
+ private static native boolean
+ jniIsGe(Object Rational1, Object Rational2) throws Cvc3Exception;
+ private static native boolean
+ jniIsGt(Object Rational1, Object Rational2) throws Cvc3Exception;
+
+ private static native Object
+ jniPlus(Object Rational1, Object Rational2) throws Cvc3Exception;
+ private static native Object
+ jniMinus(Object Rational1, Object Rational2) throws Cvc3Exception;
+ private static native Object
+ jniMult(Object Rational1, Object Rational2) throws Cvc3Exception;
+ private static native Object
+ jniDivide(Object Rational1, Object Rational2) throws Cvc3Exception;
+ private static native Object
+ jniMod(Object Rational1, Object Rational2) throws Cvc3Exception;
+
+
+ private static native Object
+ jniGetNumerator(Object Rational) throws Cvc3Exception;
+ private static native Object
+ jniGetDenominator(Object Rational) throws Cvc3Exception;
+ private static native boolean
+ jniIsInteger(Object Rational) throws Cvc3Exception;
+ private static native int
+ jniGetInteger(Object Rational) throws Cvc3Exception;
+
+
+ private static native Object
+ jniGcd(Object Rational1, Object Rational2) throws Cvc3Exception;
+ private static native Object
+ jniLcm(Object Rational1, Object Rational2) throws Cvc3Exception;
+ private static native Object
+ jniAbs(Object Rational) throws Cvc3Exception;
+ private static native Object
+ jniFloor(Object Rational) throws Cvc3Exception;
+ private static native Object
+ jniCeil(Object Rational) throws Cvc3Exception;
+
+ /// Constructor
+
+ public Rational(Object Rational, EmbeddedManager embeddedManager) {
+ super(Rational, embeddedManager);
+ }
+
+
+ public Rational(int n, EmbeddedManager embeddedManager) throws Cvc3Exception {
+ this(jniRational1(n, 10), embeddedManager);
+ }
+
+ public Rational(int n, int d, EmbeddedManager embeddedManager) throws Cvc3Exception {
+ this(jniRational1(n, d), embeddedManager);
+ }
+
+ public Rational(String n, EmbeddedManager embeddedManager) throws Cvc3Exception {
+ this(jniRational2(n, 10), embeddedManager);
+ }
+
+ public Rational(String n, int base, EmbeddedManager embeddedManager) throws Cvc3Exception {
+ this(jniRational2(n, base), embeddedManager);
+ }
+
+ public Rational(String n, String d, EmbeddedManager embeddedManager) throws Cvc3Exception {
+ this(jniRational3(n, d, 10), embeddedManager);
+ }
+
+ public Rational(String n, String d, int base, EmbeddedManager embeddedManager) throws Cvc3Exception {
+ this(jniRational3(n, d, base), embeddedManager);
+ }
+
+
+
+ /// API (immutable)
+
+ // 'Problem' with equals/hashCode:
+ // this is based on the wrapped c++ expressions.
+ // as a consequence two Expr objects are equal iff
+ // the wrapped expression is equal,
+ // and are indistinguishable for example in a HashMap.
+
+ public boolean equals(Object o) {
+ if (this == o) return true;
+
+ if (!(o instanceof Rational)) return false;
+ boolean result = false;
+ try {
+ result = jniEquals(embedded(), ((Embedded)o).embedded());
+ } catch (Cvc3Exception e) {
+ assert(false);
+ }
+ return result;
+ }
+
+ // must return the same hash code for two objects if equals returns true
+ public int hashCode() {
+ try {
+ return jniHash(embedded());
+ } catch (Cvc3Exception e) {
+ assert(false);
+ }
+ assert(false);
+ return 0;
+ }
+
+
+ public String toString() {
+ String result = "";
+ try {
+ result = jniToString(embedded());
+ } catch (Cvc3Exception e) {
+ assert(false);
+ }
+ return result;
+ }
+
+
+ public boolean isLt(Rational r) throws Cvc3Exception {
+ return jniIsLt(embedded(), r.embedded());
+ }
+
+ public boolean isLe(Rational r) throws Cvc3Exception {
+ return jniIsLe(embedded(), r.embedded());
+ }
+
+ public boolean isGt(Rational r) throws Cvc3Exception {
+ return jniIsGt(embedded(), r.embedded());
+ }
+
+ public boolean isGe(Rational r) throws Cvc3Exception {
+ return jniIsGe(embedded(), r.embedded());
+ }
+
+
+
+ public Rational plus(Rational r) throws Cvc3Exception {
+ return new Rational(jniPlus(embedded(), r.embedded()), embeddedManager());
+ }
+
+ public Rational minus(Rational r) throws Cvc3Exception {
+ return new Rational(jniPlus(embedded(), r.embedded()), embeddedManager());
+ }
+
+ public Rational mult(Rational r) throws Cvc3Exception {
+ return new Rational(jniPlus(embedded(), r.embedded()), embeddedManager());
+ }
+
+ public Rational divide(Rational r) throws Cvc3Exception {
+ return new Rational(jniPlus(embedded(), r.embedded()), embeddedManager());
+ }
+
+ public Rational mod(Rational r) throws Cvc3Exception {
+ return new Rational(jniPlus(embedded(), r.embedded()), embeddedManager());
+ }
+
+
+
+ public Rational getNumerator() throws Cvc3Exception {
+ return new Rational(jniGetNumerator(embedded()), embeddedManager());
+ }
+
+ public Rational getDenominator() throws Cvc3Exception {
+ return new Rational(jniGetDenominator(embedded()), embeddedManager());
+ }
+
+ public boolean isInteger() throws Cvc3Exception {
+ return jniIsInteger(embedded());
+ }
+
+ public int getInteger() throws Cvc3Exception {
+ assert(isInteger());
+ return jniGetInteger(embedded());
+ }
+
+
+
+ public Rational gcd(Rational r) throws Cvc3Exception {
+ return new Rational(jniGcd(embedded(), r.embedded()), embeddedManager());
+ }
+
+ public Rational lcm(Rational r) throws Cvc3Exception {
+ return new Rational(jniLcm(embedded(), r.embedded()), embeddedManager());
+ }
+
+ public Rational abs() throws Cvc3Exception {
+ return new Rational(jniAbs(embedded()), embeddedManager());
+ }
+
+ public Rational floor() throws Cvc3Exception {
+ return new Rational(jniFloor(embedded()), embeddedManager());
+ }
+
+ public Rational ceil() throws Cvc3Exception {
+ return new Rational(jniCeil(embedded()), embeddedManager());
+ }
+}
--- /dev/null
+package cvc3;
+
+import java.util.*;
+
+public class RationalMut extends Rational {
+ // jni methods
+
+
+ /// Constructor
+
+ // create embedded object
+ public RationalMut(Object RationalMut, EmbeddedManager embeddedManager) {
+ super(RationalMut, embeddedManager);
+ }
+
+
+ /// API (mutable)
+}
--- /dev/null
+INCLUDE: <rational.h>
+
+DEFINITION: Java_cvc3_Rational_jniRational1
+jobject n int n n int d
+return embed_copy(env, Rational(n, d));
+
+DEFINITION: Java_cvc3_Rational_jniRational2
+jobject n string n n int d
+return embed_copy(env, Rational(n, d));
+
+DEFINITION: Java_cvc3_Rational_jniRational3
+jobject n string n n string d n int base
+return embed_copy(env, Rational(n, d, base));
+
+
+
+DEFINITION: Java_cvc3_Rational_jniEquals
+jboolean c Rational r1 c Rational r2
+return *r1 == *r2;
+
+DEFINITION: Java_cvc3_Rational_jniToString
+jstring c Rational r
+return toJava(env, r->toString());
+
+DEFINITION: Java_cvc3_Rational_jniHash
+jint c Rational r
+return r->hash();
+
+
+
+DEFINITION: Java_cvc3_Rational_jniIsLt
+jboolean c Rational r1 c Rational r2
+return *r1 < *r2;
+
+DEFINITION: Java_cvc3_Rational_jniIsLe
+jboolean c Rational r1 c Rational r2
+return *r1 <= *r2;
+
+DEFINITION: Java_cvc3_Rational_jniIsGt
+jboolean c Rational r1 c Rational r2
+return *r1 > *r2;
+
+DEFINITION: Java_cvc3_Rational_jniIsGe
+jboolean c Rational r1 c Rational r2
+return *r1 >= *r2;
+
+
+
+DEFINITION: Java_cvc3_Rational_jniPlus
+jobject c Rational r1 c Rational r2
+return embed_copy(env, *r1 + *r2);
+
+DEFINITION: Java_cvc3_Rational_jniMinus
+jobject c Rational r1 c Rational r2
+return embed_copy(env, *r1 + *r2);
+
+DEFINITION: Java_cvc3_Rational_jniMult
+jobject c Rational r1 c Rational r2
+return embed_copy(env, *r1 + *r2);
+
+DEFINITION: Java_cvc3_Rational_jniDivide
+jobject c Rational r1 c Rational r2
+return embed_copy(env, *r1 + *r2);
+
+DEFINITION: Java_cvc3_Rational_jniMod
+jobject c Rational r1 c Rational r2
+return embed_copy(env, *r1 % *r2);
+
+
+
+DEFINITION: Java_cvc3_Rational_jniGetNumerator
+jobject c Rational r
+return embed_copy(env, r->getNumerator());
+
+DEFINITION: Java_cvc3_Rational_jniGetDenominator
+jobject c Rational r
+return embed_copy(env, r->getDenominator());
+
+DEFINITION: Java_cvc3_Rational_jniIsInteger
+jboolean c Rational r
+return r->isInteger();
+
+DEFINITION: Java_cvc3_Rational_jniGetInteger
+jint c Rational r
+return r->getInt();
+
+DEFINITION: Java_cvc3_Rational_jniGcd
+jobject c Rational r1 c Rational r2
+return embed_copy(env, gcd(*r1, *r2));
+
+DEFINITION: Java_cvc3_Rational_jniLcm
+jobject c Rational r1 c Rational r2
+return embed_copy(env, lcm(*r1, *r2));
+
+DEFINITION: Java_cvc3_Rational_jniAbs
+jobject c Rational r
+return embed_copy(env, abs(*r));
+
+DEFINITION: Java_cvc3_Rational_jniFloor
+jobject c Rational r
+return embed_copy(env, floor(*r));
+
+DEFINITION: Java_cvc3_Rational_jniCeil
+jobject c Rational r
+return embed_copy(env, ceil(*r));
--- /dev/null
+package cvc3;
+
+import java.util.*;
+
+/**
+ * SatResult is derived from the QueryResult enum in Cvc3, but as we have to
+ * use java 1.4 we have to use one of the usual tricks instead of java's Enum.
+ *
+ * To be independent of changes of the actual values of the c++ enum elements
+ * they are passed by name from the JNI interface, so that changing them will
+ * violently break the code (though unfortunately only at runtime).
+ */
+public class SatResult {
+ private final String d_result;
+
+ private SatResult(String result) {
+ d_result = result;
+ }
+
+ // names of c++ enum values
+ public static final SatResult SATISFIABLE = new SatResult("SATISFIABLE");
+ public static final SatResult UNSATISFIABLE = new SatResult("UNSATISFIABLE");
+ public static final SatResult ABORT = new SatResult("ABORT");
+ public static final SatResult UNKNOWN = new SatResult("UNKNOWN");
+
+ // the SatResult corresponding to a c++ enum value by name
+ public static SatResult get(String value) throws DebugException {
+ if (value.equals(SATISFIABLE.toString())) {
+ return SATISFIABLE;
+ } else if (value.equals(UNSATISFIABLE.toString())) {
+ return UNSATISFIABLE;
+ } else if (value.equals(ABORT.toString())) {
+ return ABORT;
+ } else if (value.equals(UNKNOWN.toString())) {
+ return UNKNOWN;
+ } else {
+ throw new DebugException("SatResult.constructor: unknown enum value: "
+ + value);
+ }
+ }
+
+ // the SatResult's c++ enum value
+ public String toString() {
+ return d_result;
+ }
+}
--- /dev/null
+package cvc3;
+
+import java.util.*;
+
+/** mirrors CVC3::SmtlibException */
+public class SmtlibException extends Cvc3Exception {
+
+ private final static long serialVersionUID = 1L;
+
+ public SmtlibException(String message) {
+ super(message);
+ }
+}
--- /dev/null
+package cvc3;
+
+import java.util.*;
+
+/** mirrors CVC3::SoundException */
+public class SoundException extends Cvc3Exception {
+
+ private final static long serialVersionUID = 1L;
+
+ public SoundException(String message) {
+ super(message);
+ }
+}
--- /dev/null
+package cvc3;
+
+import java.util.*;
+
+public class Statistics extends Embedded {
+ // jni methods
+
+ /// Constructor
+
+ public Statistics(Object Statistics, EmbeddedManager embeddedManager) {
+ super(Statistics, embeddedManager);
+ }
+
+
+ /// API (immutable)
+
+}
--- /dev/null
+package cvc3;
+
+import java.util.*;
+
+public class StatisticsMut extends Statistics {
+ // jni methods
+
+
+ /// Constructor
+
+ // create embedded object
+ public StatisticsMut(Object StatisticsMut, EmbeddedManager embeddedManager) {
+ super(StatisticsMut, embeddedManager);
+ }
+
+
+ /// API (mutable)
+}
--- /dev/null
+package cvc3;
+
+import java.util.*;
+
+class Test {
+
+ public static void main(String args[]) {
+ int regressLevel = 3;
+ if (args.length > 1) {
+ regressLevel = Integer.parseInt(args[0]);
+ }
+
+ boolean allPassed = true;
+ System.out.println("Running API test, regress level = " + regressLevel);
+ try {
+ System.out.println("\ntest():");
+ allPassed = test() && allPassed;
+ System.out.println("\n}\ntest1():");
+ allPassed = test1() && allPassed;
+ System.out.println("\n}\ntest2():");
+ allPassed = test2() && allPassed;
+ System.out.println("\n}\ntest3():");
+ allPassed = test3() && allPassed;
+ System.out.println("\n}\ntest4():");
+ allPassed = test4() && allPassed;
+ if (regressLevel > 0) {
+ System.out.println("\n}\n\ntest5():");
+ allPassed = test5() && allPassed;
+ }
+ System.out.println("\n}\ntest6():");
+ allPassed = test6() && allPassed;
+ System.out.println("\n}\ntest7():");
+ allPassed = test7() && allPassed;
+ System.out.println("\n}\ntest8():");
+ allPassed = test8() && allPassed;
+ System.out.println("\n}\ntest9():");
+ allPassed = test9(10 * regressLevel + 10) && allPassed;
+ System.out.println("\n}\nbvtest9():");
+ allPassed = bvtest9(regressLevel*3+2) && allPassed;
+
+ // Test for obvious memory leaks
+ int limit = 100 * regressLevel + 10;
+ for (int i = 0; i < limit; ++i) {
+ if (i % 100 == 0) System.out.println("test10[" + i + "]");
+ allPassed = test10() && allPassed;
+ }
+
+ System.out.println("\n}\ntest11():");
+ allPassed = test11() && allPassed;
+ System.out.println("\n}\ntest12():");
+ allPassed = test12() && allPassed;
+ System.out.println("\n}\ntest13():");
+ allPassed = test13() && allPassed;
+ System.out.println("\n}\ntest14():");
+ allPassed = test14() && allPassed;
+ System.out.println("\n}\ntest15():");
+ allPassed = test15() && allPassed;
+ System.out.println("\n}\ntest16():");
+ allPassed = test16() && allPassed;
+ System.out.println("\n}\ntest17():");
+ allPassed = test17() && allPassed;
+ System.out.println("\n}\ntest18():");
+ allPassed = test18() && allPassed;
+ System.out.println("\n}\ntest19():");
+ allPassed = test19() && allPassed;
+ System.out.println("\n}\ntest22():");
+ allPassed = test22() && allPassed;
+ System.out.println("\n}\ntest23():");
+ allPassed = test23() && allPassed;
+ /* :TODO:
+ if (regressLevel > 1) {
+ System.out.println("\n}\ntestgeorge1():");
+ George.testgeorge1();
+ System.out.println("\n}\ntestgeorge2():");
+ George.testgeorge2();
+ System.out.println("\n}\ntestgeorge3():");
+ George.testgeorge3();
+ System.out.println("\n}\ntestgeorge4():");
+ George.testgeorge4();
+ System.out.println("\n}\ntestgeorge5():");
+ George.testgeorge5();
+ }
+ */
+ System.out.println("\n}\ntestNonlinearBV():");
+ allPassed = testNonlinearBV() && allPassed;
+ System.out.println("\n}\ntestDistinct():");
+ allPassed = testDistinct() && allPassed;
+ System.out.println("\n}");
+ } catch (Exception e) {
+ System.out.println("*** Exception caught: \n" + e);
+ e.printStackTrace(System.out);
+ allPassed = false;
+ }
+
+ if (allPassed) {
+ System.out.println("Program exits successfully.");
+ }
+ else {
+ System.out.println("Program exits with error status = " + allPassed + ".");
+ }
+ System.exit(allPassed ? 0 : 1);
+ }
+
+
+ public static void DebugAssert(boolean condition, String message) throws Cvc3Exception {
+ if (!condition) {
+ throw new DebugException(message);
+ }
+ }
+
+ // Check whether e is valid
+ public static boolean check(ValidityChecker vc, Expr e) throws Cvc3Exception {
+ return check(vc, e, true);
+ }
+
+ public static boolean check(ValidityChecker vc, Expr e, boolean verbose) throws Cvc3Exception {
+ if(verbose) {
+ System.out.println("Query: " + e.toString());
+ }
+ QueryResult result = vc.query(e);
+ if (result == QueryResult.VALID) {
+ if (verbose) System.out.println("Valid\n");
+ return true;
+ }
+ else if (result == QueryResult.INVALID) {
+ if (verbose) System.out.println("Invalid\n");
+ return false;
+ }
+ if (verbose) System.out.println("Returned neither valid nor invalid\n");
+ return false;
+ }
+
+ public static void printResult(QueryResult result) throws Cvc3Exception {
+ if (result == QueryResult.VALID) {
+ System.out.println("Result Valid");
+ }
+ else if (result == QueryResult.INVALID) {
+ System.out.println("Result Invalid");
+ }
+ else if (result == QueryResult.UNKNOWN) {
+ System.out.println("Result Unknown");
+ }
+ else if (result == QueryResult.ABORT) {
+ System.out.println("Aborted");
+ } else {
+ assert(false);
+ }
+ }
+
+ // Make a new assertion - disposes expression
+ public static void newAssertion(ValidityChecker vc, Expr e) throws Cvc3Exception {
+ System.out.println("Assert: " + e);
+ vc.assertFormula(e);
+ }
+
+
+
+ public static boolean test() throws Cvc3Exception {
+ ValidityChecker vc = null;
+ try {
+ vc = ValidityChecker.create();
+
+ Type it = vc.intType(); //int
+ Op f = vc.createOp("f", vc.funType(it, it));
+ Expr z = vc.varExpr("z", it);
+ Expr e = vc.funExpr(f, vc.funExpr(f, z));
+ e = e.getChild(0);
+ Expr f2 = vc.funExpr(f, e);
+ Expr f3 = vc.funExpr(f, f2);
+
+ DebugAssert(!e.equals(f2) && !e.equals(f3), "Refcount problems");
+
+ Expr x = vc.boundVarExpr("x", "0", it); //x0:int
+ List xs = new ArrayList();
+ xs.add(x); //<x0:int>
+ Op lxsx = vc.lambdaExpr(xs, x); //\<x0:int>. x0:int
+ Expr y = vc.ratExpr(1, 1); //1
+ List ys = new ArrayList();
+ ys.add(y); //<1>
+ Expr lxsxy = vc.funExpr(lxsx, y); //(\<x0:int>. x0:int)1
+ Expr lxsxys = vc.funExpr(lxsx, ys); //(\<x0:int>. x0:int)<1>
+ System.out.println("Lambda application: " + lxsxy);
+ System.out.println("Simplified: " + vc.simplify(lxsxy));
+ return true;
+ } catch (Exception e) {
+ System.out.println("*** Exception caught in test(): \n" + e);
+ e.printStackTrace(System.out);
+ return false;
+ } finally {
+ if (vc != null) vc.delete();
+ }
+ }
+
+ public static boolean test1() throws Cvc3Exception {
+ // It is important that all Expr objects are deleted before vc is
+ // deleted. Therefore, we enclose them in a scope of try{ }catch
+ // block.
+ //
+ // Also, vc methods may throw an Exception, and we want to delete vc
+ // even in those exceptional cases.
+ ValidityChecker vc = null;
+ FlagsMut flags = null;
+ try {
+ flags = ValidityChecker.createFlags(null);
+ flags.setFlag("dagify-exprs",false);
+ flags.setFlag("dump-log", ".test1.cvc");
+ vc = ValidityChecker.create(flags);
+
+ boolean b = check(vc, vc.trueExpr());
+ DebugAssert(b, "Should be valid");
+
+ vc.push();
+ b = check(vc, vc.falseExpr());
+ DebugAssert(!b, "Should be invalid");
+ vc.pop();
+
+ // Check p OR ~p
+
+ Expr p = vc.varExpr("p", vc.boolType());
+ Expr e = vc.orExpr(p, vc.notExpr(p));
+
+ b = check(vc, e);
+ DebugAssert(b, "Should be valid");
+
+ // Check x = y . f(x) = f(y)
+
+ Expr x = vc.varExpr("x", vc.realType());
+ Expr y = vc.varExpr("y", vc.realType());
+
+ Type real2real = vc.funType(vc.realType(), vc.realType());
+ Op f = vc.createOp("f", real2real);
+ Expr fx = vc.funExpr(f, x);
+ Expr fy = vc.funExpr(f, y);
+
+ e = vc.impliesExpr(vc.eqExpr(x,y),vc.eqExpr(fx, fy));
+ b = check(vc, e);
+ DebugAssert(b, "Should be valid");
+
+ // Check f(x) = f(y) . x = y
+
+ e = vc.impliesExpr(vc.eqExpr(fx,fy),vc.eqExpr(x, y));
+ int scopeLevel = vc.scopeLevel();
+ vc.push();
+ b = check(vc, e);
+ DebugAssert(!b, "Should be invalid");
+
+ // Get counter-example
+
+ System.out.println("Scope level: " + vc.scopeLevel());
+ System.out.println("Counter-example:");
+ List assertions = vc.getCounterExample();
+ for (int i = 0; i < assertions.size(); ++i) {
+ System.out.println((Expr)assertions.get(i));
+ }
+ System.out.println("End of counter-example");
+ System.out.println();
+
+ // Reset to initial scope
+ System.out.println("Resetting");
+ vc.pop();
+ DebugAssert(scopeLevel == vc.scopeLevel(), "scope error");
+ System.out.println("Scope level: " + vc.scopeLevel());
+ System.out.println();
+
+ // Check w = x & x = y & y = z & f(x) = f(y) & x = 1 & z = 2
+
+ Expr w = vc.varExpr("w", vc.realType());
+ Expr z = vc.varExpr("z", vc.realType());
+
+ System.out.println("Push Scope");
+ System.out.println();
+ vc.push();
+
+ newAssertion(vc, vc.eqExpr(w, x));
+ newAssertion(vc, vc.eqExpr(x, y));
+ newAssertion(vc, vc.eqExpr(y, z));
+ newAssertion(vc, vc.eqExpr(fx, fy));
+ newAssertion(vc, vc.eqExpr(x, vc.ratExpr(1)));
+
+ System.out.println("simplify(w) = " + vc.simplify(w));
+ DebugAssert(vc.simplify(w).equals(vc.ratExpr(1)), "Expected simplify(w) = 1");
+
+ newAssertion(vc, vc.eqExpr(z, vc.ratExpr(2)));
+ System.out.println("Inconsistent?: " + vc.inconsistent());
+
+ System.out.println("Assumptions Used:");
+ assertions = vc.inconsistentReasons();
+ for (int i = 0; i < assertions.size(); ++i) {
+ System.out.println((Expr)assertions.get(i));
+ }
+
+ System.out.println("Pop Scope");
+ System.out.println();
+ vc.pop();
+
+ System.out.println("simplify(w) = " + vc.simplify(w));
+ DebugAssert(vc.simplify(w).equals(w), "Expected simplify(w) = w");
+
+ System.out.println("Inconsistent?: " + vc.inconsistent());
+
+ return true;
+ } catch (Exception e) {
+ System.out.println("*** Exception caught in test1(): \n" + e);
+ e.printStackTrace(System.out);
+ return false;
+ } finally {
+ if (vc != null) vc.delete();
+ if (flags != null) flags.delete();
+ }
+ }
+
+
+ public static boolean test2() throws Cvc3Exception {
+ ValidityChecker vc = null;
+ FlagsMut flags = null;
+ try {
+ flags = ValidityChecker.createFlags(null);
+ flags.setFlag("dagify-exprs",false);
+ vc = ValidityChecker.create(flags);
+
+ Expr bexpr = vc.varExpr("b", vc.intType());
+ vc.assertFormula(vc.ltExpr(bexpr, vc.ratExpr(10)));
+
+ Expr c = vc.varExpr("c", vc.intType());
+ vc.assertFormula(vc.orExpr(vc.eqExpr(c, vc.ratExpr(0)), vc.eqExpr(c, vc.ratExpr(1))));
+
+ boolean b = check(vc, vc.leExpr(bexpr, vc.ratExpr(10)));
+ DebugAssert(b, "Should be valid");
+
+ b = check(vc, vc.falseExpr());
+ DebugAssert(!b, "Should be invalid");
+ vc.returnFromCheck();
+
+ // Check x = y . g(x,y) = g(y,x)
+
+ Expr x = vc.varExpr("x", vc.realType());
+ Expr y = vc.varExpr("y", vc.realType());
+
+ Type real = vc.realType();
+ List RxR = new ArrayList();
+ RxR.add(real);
+ RxR.add(real);
+
+ Type realxreal2real = vc.funType(RxR, real);
+ Op g = vc.createOp("g", realxreal2real);
+
+ Expr gxy = vc.funExpr(g, x, y);
+ Expr gyx = vc.funExpr(g, y, x);
+
+ Expr e = vc.impliesExpr(vc.eqExpr(x,y),vc.eqExpr(gxy, gyx));
+ b = check(vc, e);
+ DebugAssert(b, "Should be valid");
+
+ Op h = vc.createOp("h", realxreal2real);
+
+ Expr hxy = vc.funExpr(h, x, y);
+ Expr hyx = vc.funExpr(h, y, x);
+
+ e = vc.impliesExpr(vc.eqExpr(x,y),vc.eqExpr(hxy, hyx));
+ b = check(vc, e);
+ DebugAssert(b, "Should be valid");
+
+ return true;
+ } catch (Exception e) {
+ System.out.println("*** Exception caught in test2(): \n" + e);
+ e.printStackTrace(System.out);
+ return false;
+ } finally {
+ if (vc != null) vc.delete();
+ if (flags != null) flags.delete();
+ }
+ }
+
+
+ public static ExprMut ltLex(ValidityChecker vc, Expr i1, Expr i2, Expr j1, Expr j2) throws Cvc3Exception {
+ Expr res = vc.ltExpr(i1, j1);
+ return vc.orExpr(res, vc.andExpr(vc.eqExpr(i1, j1), vc.ltExpr(i2, j2)));
+ }
+
+ public static ExprMut createTestFormula(ValidityChecker vc, Expr i1, Expr i2, Expr r1, Expr r2)
+ throws Cvc3Exception {
+ Expr lt1 = ltLex(vc, r1, r2, i1, i2);
+ Expr lt2 = ltLex(vc, i2, i1, r2, r1);
+ return vc.andExpr(lt1, lt2);
+ }
+
+ public static boolean test3() throws Cvc3Exception {
+ ValidityChecker vc = null;
+ FlagsMut flags = null;
+ try {
+ flags = ValidityChecker.createFlags(null);
+ flags.setFlag("dagify-exprs",false);
+ vc = ValidityChecker.create(flags);
+
+ Expr i = vc.varExpr("i", vc.realType());
+ Expr j = vc.varExpr("j", vc.realType());
+ Expr k = vc.varExpr("k", vc.realType());
+
+ Expr one = vc.ratExpr(1);
+
+ Expr test = createTestFormula(vc, i, j,
+ vc.minusExpr(i, one), vc.minusExpr(j, k));
+
+ System.out.println("Trying test: " + test);
+
+ vc.push();
+ QueryResult result = vc.query(test);
+ if (result == QueryResult.VALID) {
+ System.out.println("Test Valid");
+ vc.pop();
+ }
+ else {
+ List assertions = vc.getCounterExample();
+ System.out.println("Test Invalid Under Conditions:");
+ for (int index = 0; index < assertions.size(); ++index) {
+ System.out.println(assertions.get(index));
+ }
+
+ // Try assertions one by one
+ for (int index = 0; index < assertions.size(); ++index) {
+ Expr condition = vc.notExpr((Expr)assertions.get(index));
+ System.out.println("Trying test under condition: " + condition);
+ vc.pop();
+ vc.push();
+ printResult(vc.query(vc.impliesExpr(condition, test)));
+ }
+ }
+
+ return true;
+ } catch (Exception e) {
+ System.out.println("*** Exception caught in test3(): \n" + e);
+ e.printStackTrace(System.out);
+ return false;
+ } finally {
+ if (vc != null) vc.delete();
+ if (flags != null) flags.delete();
+ }
+ }
+
+
+ public static boolean test4() throws Cvc3Exception {
+ ValidityChecker vc = null;
+ FlagsMut flags = null;
+ try {
+ flags = ValidityChecker.createFlags(null);
+ flags.setFlag("dagify-exprs",false);
+ vc = ValidityChecker.create(flags);
+
+ Expr i = vc.varExpr("i", vc.realType());
+ Expr j = vc.varExpr("j", vc.realType());
+ Expr k = vc.varExpr("k", vc.realType());
+
+ Expr one = vc.ratExpr(1);
+
+ Expr test = createTestFormula(vc, i, j,
+ vc.minusExpr(i, one), vc.minusExpr(j, k));
+
+ System.out.println("Trying test: " + test);
+
+ vc.push();
+ QueryResult result = vc.query(test);
+ if (result == QueryResult.VALID) {
+ System.out.println("Test Valid");
+ }
+ else {
+ List assertions = vc.getCounterExample();
+ System.out.println("Test Invalid Under Conditions:");
+ for (int index = 0; index < assertions.size(); ++index) {
+ System.out.println(assertions.get(index));
+ }
+
+ // Try assertions one by one
+ for (int index = 0; index < assertions.size(); ++index) {
+ Expr condition = vc.notExpr((Expr)assertions.get(index));
+ System.out.println("Trying test under condition: " + condition);
+ vc.pop();
+ vc.push();
+ printResult(vc.query(vc.impliesExpr(condition, test)));
+ }
+ }
+
+ return true;
+ } catch (Exception e) {
+ System.out.println("*** Exception caught in test4(): \n" + e);
+ e.printStackTrace(System.out);
+ return false;
+ } finally {
+ if (vc != null) vc.delete();
+ if (flags != null) flags.delete();
+ }
+ }
+
+
+ public static void findLeaves(Expr e, List l) throws Cvc3Exception {
+ int ar = e.arity();
+ if (ar > 0) {
+ for (int i = 0; i < ar; ++i) {
+ findLeaves(e.getChild(i), l);
+ }
+ return;
+ }
+ l.add(e);
+ }
+
+ public static boolean hasij(Expr e, Expr i, Expr j) throws Cvc3Exception {
+ int ar = e.arity();
+ if (ar > 0) {
+ for (int k = 0; k < ar; ++k)
+ if (hasij(e.getChild(k), i, j)) return true;
+ return false;
+ }
+ if (e.equals(i) || e.equals(j)) return true;
+ return false;
+ }
+
+ public static Expr plusExpr(ValidityChecker vc, List kids) throws Cvc3Exception {
+ if (kids.size() == 0) return vc.ratExpr(0);
+ else if (kids.size() == 1) return (Expr)kids.get(0);
+ else if (kids.size() == 2) return vc.plusExpr((Expr)kids.get(0), (Expr)kids.get(1));
+ else {
+ Expr r = (Expr)kids.get(kids.size() - 1);
+ kids.remove(kids.size() - 1);
+ return vc.plusExpr(plusExpr(vc, kids), r);
+ }
+ }
+
+ public static boolean test5() throws Cvc3Exception {
+ ValidityChecker vc = null;
+ FlagsMut flags = null;
+ try {
+ flags = ValidityChecker.createFlags(null);
+ flags.setFlag("dagify-exprs",false);
+ vc = ValidityChecker.create(flags);
+
+ Expr i = vc.varExpr("i1", vc.realType());
+ Expr j = vc.varExpr("i2", vc.realType());
+ Expr p = vc.varExpr("p", vc.realType());
+ Expr q = vc.varExpr("q", vc.realType());
+ Expr r = vc.varExpr("r", vc.realType());
+ Expr a = vc.varExpr("arb_addr", vc.realType());
+ Expr N = vc.varExpr("N", vc.realType());
+
+ Expr M = vc.varExpr("M", vc.arrayType(vc.realType(), vc.realType()));
+
+ Expr M2 = vc.writeExpr(M, vc.plusExpr(q, i), vc.readExpr(M, vc.plusExpr(r, i)));
+
+ Expr M1 = vc.writeExpr(M, vc.plusExpr(p, j), vc.readExpr(M, vc.plusExpr(r, j)));
+
+ Expr e = vc.eqExpr(vc.readExpr(vc.writeExpr(M2, vc.plusExpr(p, j),
+ vc.readExpr(M2, vc.plusExpr(r, j))), a),
+ vc.readExpr(vc.writeExpr(M1, vc.plusExpr(q, i),
+ vc.readExpr(M1, vc.plusExpr(r, i))), a));
+
+ Expr one = vc.ratExpr(1);
+ Expr zero = vc.ratExpr(0);
+
+ Expr qmp = vc.minusExpr(q, p);
+ Expr qmr = vc.minusExpr(q, r);
+
+ List hyp = new ArrayList();
+ hyp.add(vc.ltExpr(i, j));
+ // hyp.add(vc.orExpr(vc.geExpr(qmp, N), vc.leExpr(qmp, zero)));
+ // hyp.add(vc.orExpr(vc.geExpr(qmr, N), vc.leExpr(qmr, zero)));
+
+ Expr test = vc.impliesExpr(vc.andExpr(hyp), e);
+ Expr query;
+
+ System.out.println("Checking verification condition:" + test);
+
+ vc.push();
+ QueryResult result = vc.query(test);
+ if (result == QueryResult.VALID) {
+ System.out.println("Test Valid");
+ }
+ else {
+ List conditions = new ArrayList();
+ int req;
+
+ List assertions = vc.getCounterExample();
+
+ System.out.println("Invalid Under Conditions:");
+ for (int index = 0; index < assertions.size(); ++index) {
+ if (((Expr)assertions.get(index)).equals(vc.notExpr(test))) {
+ for (; index < assertions.size()-1; ++index) {
+ assertions.set(index, assertions.get(index+1));
+ }
+ assertions.remove(assertions.size() - 1);
+ break;
+ }
+ }
+ for (int index = 0; index < assertions.size(); ++index) {
+ System.out.println(assertions.get(index));
+ }
+
+ System.out.println();
+
+ // Try assertions one by one
+ for (int index = 0; index < assertions.size(); ++index) {
+ e = (Expr)assertions.get(index);
+
+ // Check condition for eligibility
+ if (e.isNot()) {
+ System.out.println("Condition ineligible: negation: " + e);
+ System.out.println();
+ continue;
+ }
+ if (e.isEq()) {
+ req = 2;
+ }
+ else req = 1;
+
+ List leaves = new ArrayList();
+ findLeaves(e, leaves);
+ for (int index2 = 0; index2 < leaves.size(); ++index2) {
+ if (!((Expr)leaves.get(index2)).isVar() ||
+ ((Expr)leaves.get(index2)).equals(i) ||
+ ((Expr)leaves.get(index2)).equals(j) ||
+ ((Expr)leaves.get(index2)).equals(a))
+ continue;
+ req--;
+ }
+ if (req > 0) {
+ System.out.println("Condition ineligible: not enough non-loop variables: " + e);
+ System.out.println();
+ continue;
+ }
+
+ System.out.println("Condition selected: " + e);
+ System.out.println();
+
+ conditions.add(vc.notExpr(e));
+ System.out.println("Trying verification condition with hypothesis: "
+ + vc.andExpr(conditions));
+ vc.pop();
+ vc.push();
+ query = vc.impliesExpr(vc.andExpr(conditions), test);
+ result = vc.query(test);
+ if (result == QueryResult.VALID) {
+ System.out.println("Result Valid");
+ break;
+ }
+ else {
+ assertions = vc.getCounterExample();
+
+ System.out.println("Invalid Under Conditions:");
+ for (int index2 = 0; index2 < assertions.size(); ++index2) {
+ if (((Expr)assertions.get(index2)).equals(vc.notExpr(query))) {
+ for (; index2 < assertions.size()-1; ++index2) {
+ assertions.set(index2, assertions.get(index2+1));
+ }
+ assertions.remove(assertions.size() - 1);
+ break;
+ }
+ }
+
+ for (int index2 = 0; index2 < assertions.size(); ++index2) {
+ System.out.println(assertions.get(index2));
+ }
+ System.out.println();
+ index = assertions.size();
+ }
+ }
+
+ System.out.println();
+ System.out.println("Attempting to remove loop variables");
+ // replace loop variables in conditions
+ List newConditions = new ArrayList();
+ List newPlus = new ArrayList();
+ boolean foundi, foundj, negi, negj;
+ Expr minusone = vc.ratExpr(-1);
+ int index;
+ for (index = 0; index < conditions.size(); ++index) {
+ if (((Expr)conditions.get(index)).getChild(0).isEq()) {
+ e = vc.simplify(
+ vc.minusExpr(((Expr)conditions.get(index)).getChild(0).getChild(0),
+ ((Expr)conditions.get(index)).getChild(0).getChild(1)));
+ if (hasij(e, i, j)) {
+ if (e.isPlus()) {
+ newPlus.clear();
+ newPlus.add(e.getChild(0));
+ foundi = foundj = negi = negj = false;
+ for (int index2 = 1; index2 < e.arity(); index2++) {
+ Expr term = e.getChild(index2);
+ if (term.equals(i) && !foundi) foundi = true;
+ else if (term.equals(j) && !foundj) {
+ foundj = true;
+ negj = true;
+ }
+ else if (term.isMult()
+ && term.getChild(0).equals(minusone)
+ && term.getChild(1).equals(i)
+ && !foundi) {
+ foundi = true;
+ negi = true;
+ }
+ else if (term.isMult()
+ && term.getChild(0).equals(minusone)
+ && term.getChild(1).equals(j)
+ && !foundj)
+ foundj = true;
+ else newPlus.add(term);
+ }
+ if (foundi && foundj && (negi && negj || (!negi && !negj))) {
+ e = plusExpr(vc, newPlus);
+ if (negi && negj) e = vc.uminusExpr(e);
+ e = vc.simplify(e);
+ if (!hasij(e, i, j)) {
+ newConditions.add(vc.orExpr(vc.geExpr(e, N), vc.leExpr(e, zero)));
+ continue;
+ }
+ }
+ }
+ System.out.println("Unable to remove loop variables:" + e);
+ break;
+ }
+ }
+ newConditions.add(conditions.get(index));
+ }
+ if (index == conditions.size()) {
+ System.out.println("Loop variables successfully removed:");
+ Expr cond = (newConditions.size()>0)?
+ vc.andExpr(newConditions) : vc.trueExpr();
+ System.out.println(cond);
+
+ List loopConditions = new ArrayList();
+ loopConditions.add(cond);
+ loopConditions.add(vc.geExpr(i, one));
+ loopConditions.add(vc.geExpr(j, one));
+ loopConditions.add(vc.leExpr(i, N));
+ loopConditions.add(vc.leExpr(j, N));
+ vc.pop();
+ vc.push();
+ System.out.println("Final query");
+ printResult(vc.query(vc.impliesExpr(vc.andExpr(loopConditions), test)));
+ }
+ }
+
+ return true;
+ } catch (Exception e) {
+ System.out.println("*** Exception caught in test5(): \n" + e);
+ e.printStackTrace(System.out);
+ return false;
+ } finally {
+ if (vc != null) vc.delete();
+ if (flags != null) flags.delete();
+ }
+ }
+
+
+
+ public static boolean test6() throws Cvc3Exception {
+ ValidityChecker vc1 = null;
+ ValidityChecker vc2 = null;
+ try {
+ vc1 = ValidityChecker.create();
+ vc2 = ValidityChecker.create();
+
+ Type real1 = vc1.realType();
+
+ Expr x1 = vc1.varExpr("x", real1);
+ Expr y1 = vc1.boundVarExpr("y", "0", real1);
+
+ System.out.println("vc1 variables: " + x1 + ", " + y1);
+
+ Expr x2 = vc2.varExpr("x", vc2.importType(real1));
+ Expr y2 = vc2.boundVarExpr("y", "0", vc2.realType());
+
+ System.out.println("vc2 variables: " + x2 + ", " + y2);
+ System.out.println("vars imported to vc2 from vc1: "
+ + vc2.importExpr(x1) + ", " + vc2.importExpr(y1));
+ Expr t1 = vc1.trueExpr();
+ Expr and1 = vc1.andExpr(t1, vc1.falseExpr());
+ Op f1 = vc1.createOp("f", vc1.funType(real1, real1));
+ Expr fx1 = vc1.funExpr(f1, x1);
+ Expr f5_1 = vc1.funExpr(f1, vc1.ratExpr(5,1));
+ Type rt1 = vc1.recordType("foo", real1, "bar", real1);
+ Expr r1 = vc1.recordExpr("foo", fx1, "bar", f5_1);
+ Expr r1_eq = vc1.eqExpr(r1, vc1.recUpdateExpr(r1, "foo", f5_1));
+ Type art1 = vc1.arrayType(real1, rt1);
+ Expr ar1 = vc1.varExpr("ar", art1);
+ Expr ar_eq1 = vc1.eqExpr(vc1.writeExpr(ar1, x1, r1), ar1);
+ Expr query1 = vc1.eqExpr(vc1.recSelectExpr(vc1.readExpr(ar1, x1), "foo"),
+ vc1.recSelectExpr(r1, "bar"));
+
+ System.out.println("*** VC #1:");
+ newAssertion(vc1, r1_eq);
+ newAssertion(vc1, ar_eq1);
+ check(vc1, query1);
+
+ System.out.println("*** VC #2:");
+ newAssertion(vc2, vc2.importExpr(r1_eq));
+ newAssertion(vc2, vc2.importExpr(ar_eq1));
+ check(vc2, vc2.importExpr(query1));
+
+ return true;
+ } catch (Exception e) {
+ System.out.println("*** Exception caught in test6(): \n" + e);
+ e.printStackTrace(System.out);
+ return false;
+ } finally {
+ if (vc1 != null) vc1.delete();
+ if (vc2 != null) vc2.delete();
+ }
+ }
+
+
+
+ public static boolean test7() throws Cvc3Exception {
+ ValidityChecker vc1 = null;
+ ValidityChecker vc2 = null;
+ try {
+ vc1 = ValidityChecker.create();
+ vc2 = ValidityChecker.create();
+
+ Expr e1 = vc1.varExpr("e1", vc1.realType());
+ Expr e2 = vc2.varExpr("e2", vc2.realType());
+ newAssertion(vc2, vc2.eqExpr(vc2.importExpr(e1), e2));
+
+ return true;
+ } catch (Exception e) {
+ System.out.println("*** Exception caught in test7(): \n" + e);
+ e.printStackTrace(System.out);
+ return false;
+ } finally {
+ if (vc1 != null) vc1.delete();
+ if (vc2 != null) vc2.delete();
+ }
+ }
+
+
+
+ public static boolean test8() throws Cvc3Exception {
+ ValidityChecker vc = null;
+ try {
+ vc = ValidityChecker.create();
+
+ List vec = new ArrayList();
+ vec.add(vc.boundVarExpr("x", "x", vc.realType()));
+ Expr lambda = vc.lambdaExpr(vec, vc.falseExpr()).getExpr();
+ try {
+ Type t = vc.subtypeType(lambda, vc.nullExpr());
+ DebugAssert(false, "Typechecking exception expected");
+ } catch(TypecheckException e) {
+ // fall through
+ }
+
+ return true;
+ } catch (Exception e) {
+ System.out.println("*** Exception caught in test5(): \n" + e);
+ e.printStackTrace(System.out);
+ return false;
+ } finally {
+ if (vc != null) vc.delete();
+ }
+ }
+
+
+
+ public static ExprMut adder(ValidityChecker vc, Expr a, Expr b, Expr c) throws Cvc3Exception {
+ return vc.notExpr(vc.iffExpr(vc.notExpr(vc.iffExpr(a,b)),c));
+ }
+
+ public static ExprMut carry(ValidityChecker vc, Expr a, Expr b, Expr c) throws Cvc3Exception {
+ return vc.orExpr(vc.andExpr(a,b), vc.orExpr(vc.andExpr(b,c),vc.andExpr(a,c)));
+ }
+
+ public static List add(ValidityChecker vc, List a, List b) throws Cvc3Exception {
+ int N = a.size();
+ Expr c = vc.falseExpr();
+
+ List sum = new ArrayList();
+ for (int i = 0; i < N; i++) {
+ sum.add(adder(vc,(Expr)a.get(i),(Expr)b.get(i),c));
+ c = carry(vc,(Expr)a.get(i),(Expr)b.get(i),c);
+ }
+ return sum;
+ }
+
+ public static ExprMut vectorEq(ValidityChecker vc, List a, List b) throws Cvc3Exception {
+ int N = a.size();
+ ExprMut result = vc.trueExpr();
+
+ for (int i = 0; i < N; i++) {
+ result = vc.andExpr(result, vc.iffExpr((Expr)a.get(i), (Expr)b.get(i)));
+ }
+ return result;
+ }
+
+
+ public static boolean test9(int N) throws Cvc3Exception {
+ ValidityChecker vc = null;
+ try {
+ vc = ValidityChecker.create();
+
+ int i;
+ List a = new ArrayList();
+ List b = new ArrayList();
+
+ for (i=0; i < N; i++) {
+ a.add(vc.varExpr("a" + Integer.toString(i), vc.boolType()));
+ b.add(vc.varExpr("b" + Integer.toString(i), vc.boolType()));
+ }
+
+ List sum1 = add(vc,a,b);
+ List sum2 = add(vc,b,a);
+
+ Expr q = vectorEq(vc,sum1,sum2);
+
+ check(vc, q);
+
+ // Proof p = vc.getProof();
+
+ return true;
+ } catch (Exception e) {
+ System.out.println("*** Exception caught in test9(): \n" + e);
+ e.printStackTrace(System.out);
+ return false;
+ } finally {
+ if (vc != null) vc.delete();
+ }
+ }
+
+
+ public static boolean test22() throws Cvc3Exception {
+ ValidityChecker vc = null;
+
+ try {
+ vc = ValidityChecker.create();
+ Type intType = vc.intType();
+ Type fType = vc.funType(intType, intType);
+
+ Op f = vc.createOp("f", fType);
+ Expr x = vc.varExpr("x", intType);
+ Expr fx = vc.exprFromString("f(x)");
+
+ Expr p = vc.exprFromString("FORALL (x:INT) : x < f(x)");
+
+ List patternvv = new ArrayList();
+ List patternv = new ArrayList();
+ patternv.add(fx);
+ patternvv.add(patternv);
+
+ vc.setTriggers(p, patternv);
+ DebugAssert(patternvv.equals(p.getTriggers()),
+ "Expected p.getTriggers() == patternvv: " + p.toString());
+
+ vc.setMultiTriggers(p, patternvv);
+
+ DebugAssert(patternvv.equals(p.getTriggers()),
+ "Expected p.getTriggers() == patternvv: " + p.toString());
+
+ List vars = new ArrayList();
+ vars.add(x);
+ Expr r = vc.forallExpr(vars, vc.ltExpr(x, fx), patternv);
+
+ DebugAssert(patternvv.equals(r.getTriggers()),
+ "Expected r.getTriggers() == patternvv: " + r.toString());
+
+ Expr s = vc.exprFromString("FORALL (x:INT) : x > f(x)");
+ vc.setTrigger(s, fx);
+
+ List trigsvv = s.getTriggers();
+ DebugAssert(trigsvv.size() == 1, "Expected s.getTriggers().size() == 1: "
+ + trigsvv.size());
+
+ List trigsv = (List)trigsvv.get(0);
+ DebugAssert(trigsv.size() == 1, "Expected s.getTriggers()[0].size() == 1: "
+ + trigsv.size());
+
+ DebugAssert(fx.equals(trigsv.get(0)),
+ "Expected s.getTriggers()[0][0] == fx: " + (trigsv.get(0)));
+
+ Expr t = vc.exprFromString("FORALL (x:INT) : x > f(x)");
+ vc.setMultiTrigger(t, patternv);
+ trigsvv = t.getTriggers();
+ DebugAssert(trigsvv.size() == 1, "Expected t.getTriggers().size() == 1: "
+ + trigsvv.size());
+
+ trigsv = (List)trigsvv.get(0);
+ DebugAssert(trigsv.size() == 1, "Expected t.getTriggers()[0].size() == 1: "
+ + trigsv.size());
+
+ DebugAssert(fx.equals(trigsv.get(0)),
+ "Expected t.getTriggers()[0][0] == fx: " + (trigsv.get(0)));
+
+ Expr u = vc.forallExprMultiTriggers(vars, vc.ltExpr(x, fx), patternvv);
+
+ DebugAssert(patternvv.equals(u.getTriggers()),
+ "Expected u.getTriggers() == patternvv: " + u.toString());
+
+ } catch (Exception e) {
+ System.out.println("*** Exception caught in test22(): \n" + e);
+ e.printStackTrace(System.out);
+ return false;
+ } finally {
+ if (vc != null)
+ vc.delete();
+ }
+ return true;
+ }
+
+ private static boolean test23() throws Cvc3Exception {
+ ValidityChecker vc = null;
+
+ try {
+ vc = ValidityChecker.create();
+ Type intType = vc.intType();
+
+ Expr x = vc.varExpr("x",intType);
+ Expr y= vc.varExpr("y",intType);
+ Expr a = vc.varExpr("a",intType);
+ Expr b = vc.varExpr("b",intType);
+
+ Expr s = vc.exprFromString("x < y");
+ Expr t = vc.exprFromString("a < b");
+
+ System.out.println( "s=" + s + "\nt=" + t );
+
+ List oldExprs = new ArrayList(), newExprs = new ArrayList();
+ oldExprs.add(x);
+ oldExprs.add(y);
+ newExprs.add(a);
+ newExprs.add(b);
+
+ Expr u = s.subst(oldExprs,newExprs);
+ System.out.println( "u=" + u );
+
+ DebugAssert( t.equals(u), "Expected t==u" );
+ } catch(Throwable e) {
+ System.out.println( "*** Exception caught in test23(): ");
+ e.printStackTrace(System.out);
+ return false;
+ } finally {
+ if (vc != null)
+ vc.delete();
+ }
+ return true;
+ }
+
+ public static ExprMut bvadder(ValidityChecker vc, Expr a, Expr b, Expr c) throws Cvc3Exception {
+ return vc.newBVXorExpr(a, vc.newBVXorExpr(b, c));
+ }
+
+
+ public static ExprMut bvcarry(ValidityChecker vc, Expr a, Expr b, Expr c) throws Cvc3Exception {
+ return vc.newBVOrExpr(vc.newBVAndExpr(a,b), vc.newBVOrExpr(vc.newBVAndExpr(b,c),vc.newBVAndExpr(a,c)));
+ }
+
+ public static List bvadd(ValidityChecker vc, List a, List b) throws Cvc3Exception {
+ int N=a.size();
+ Expr c = vc.newBVConstExpr(new Rational(0, vc.embeddedManager()), 1);
+
+ List sum = new ArrayList();
+ for (int i = 0; i < N; i++) {
+ sum.add(bvadder(vc,(Expr)a.get(i),(Expr)b.get(i),c));
+ c = bvcarry(vc,(Expr)a.get(i),(Expr)b.get(i),c);
+ }
+ return sum;
+ }
+
+
+ public static ExprMut bvvectorEq(ValidityChecker vc, List a, List b) throws Cvc3Exception {
+ int N = a.size();
+ ExprMut result = vc.newBVConstExpr("1");
+
+ for (int i = 0; i < N; i++) {
+ result = vc.newBVAndExpr(result, vc.newBVXnorExpr((Expr)a.get(i), (Expr)b.get(i)));
+ }
+ return result;
+ }
+
+
+ public static boolean bvtest9(int N) throws Cvc3Exception {
+ ValidityChecker vc = null;
+ try {
+ vc = ValidityChecker.create();
+
+ Expr a, b, sum1;
+ a = vc.varExpr("a", vc.bitvecType(N));
+ b = vc.varExpr("b", vc.bitvecType(N));
+ List kids = new ArrayList();
+ kids.add(a);
+ kids.add(b);
+ sum1 = vc.newBVPlusExpr(N, kids);
+
+ List avec = new ArrayList();
+ List bvec = new ArrayList();
+ List sum1vec = new ArrayList();
+ for (int i = 0; i < N; i++) {
+ avec.add(vc.newBVExtractExpr(a, i, i));
+ bvec.add(vc.newBVExtractExpr(b, i, i));
+ sum1vec.add(vc.newBVExtractExpr(sum1, i, i));
+ }
+
+ List sum2 = bvadd(vc,avec,bvec);
+
+ Expr q = bvvectorEq(vc,sum1vec,sum2);
+
+ check(vc, vc.eqExpr(q,vc.newBVConstExpr("1")));
+
+ return true;
+ } catch (Exception e) {
+ System.out.println("*** Exception caught in bvtest9(): \n" + e);
+ e.printStackTrace(System.out);
+ return false;
+ } finally {
+ if (vc != null) vc.delete();
+ }
+ }
+
+
+ public static boolean test10() throws Cvc3Exception {
+ ValidityChecker vc = null;
+ try {
+ vc = ValidityChecker.create();
+
+ Expr x = vc.varExpr("x", vc.realType());
+ Expr y = vc.varExpr("y", vc.realType());
+
+ Type real = vc.realType();
+ List RxR = new ArrayList();
+ RxR.add(real);
+ RxR.add(real);
+
+ Type realxreal2real = vc.funType(RxR, real);
+ Op g = vc.createOp("g", realxreal2real);
+
+ Expr gxy = vc.funExpr(g, x, y);
+ Expr gyx = vc.funExpr(g, y, x);
+
+ Expr ia = vc.eqExpr(x,y);
+ Expr ib = vc.eqExpr(gxy, gyx);
+
+ Expr e = vc.impliesExpr(vc.eqExpr(x,y),vc.eqExpr(gxy, gyx));
+ check(vc, e, false);
+
+ Op h = vc.createOp("h", realxreal2real);
+
+ Expr hxy = vc.funExpr(h, x, y);
+ Expr hyx = vc.funExpr(h, y, x);
+
+ e = vc.impliesExpr(vc.eqExpr(x,y),vc.eqExpr(hxy, hyx));
+ check(vc, e, false);
+
+ return true;
+ } catch (Exception e) {
+ System.out.println("*** Exception caught in test10(): \n" + e);
+ e.printStackTrace(System.out);
+ return false;
+ } finally {
+ if (vc != null) vc.delete();
+ }
+ }
+
+
+
+ public static int printImpliedLiterals(ValidityChecker vc) throws Cvc3Exception {
+ int count = 0;
+ System.out.println("Implied Literals:");
+ Expr impLit = vc.getImpliedLiteral();
+ while (!impLit.isNull()) {
+ ++count;
+ System.out.println(impLit);
+ impLit = vc.getImpliedLiteral();
+ }
+ return count;
+ }
+
+ public static boolean test11() throws Cvc3Exception {
+ ValidityChecker vc = null;
+ try {
+ vc = ValidityChecker.create();
+
+ Expr x = vc.varExpr("x", vc.realType());
+ Expr y = vc.varExpr("y", vc.realType());
+ Expr z = vc.varExpr("z", vc.realType());
+
+ Type real = vc.realType();
+ Type real2real = vc.funType(real, real);
+ Type real2bool = vc.funType(real, vc.boolType());
+ Op f = vc.createOp("f", real2real);
+ Op p = vc.createOp("p", real2bool);
+
+ Expr fx = vc.funExpr(f, x);
+ Expr fy = vc.funExpr(f, y);
+
+ Expr px = vc.funExpr(p, x);
+ Expr py = vc.funExpr(p, y);
+
+ Expr xeqy = vc.eqExpr(x, y);
+ Expr yeqx = vc.eqExpr(y, x);
+ Expr xeqz = vc.eqExpr(x, z);
+ Expr zeqx = vc.eqExpr(z, x);
+ Expr yeqz = vc.eqExpr(y, z);
+ Expr zeqy = vc.eqExpr(z, y);
+
+ int c;
+
+ vc.registerAtom(vc.eqExpr(x,vc.ratExpr(0,1)));
+ vc.registerAtom(xeqy);
+ vc.registerAtom(yeqx);
+ vc.registerAtom(xeqz);
+ vc.registerAtom(zeqx);
+ vc.registerAtom(yeqz);
+ vc.registerAtom(zeqy);
+ vc.registerAtom(px);
+ vc.registerAtom(py);
+ vc.registerAtom(vc.eqExpr(fx, fy));
+
+ System.out.println("Push");
+ vc.push();
+
+ System.out.println("Assert x = y");
+ vc.assertFormula(xeqy);
+ c = printImpliedLiterals(vc);
+ DebugAssert(c==3,"Implied literal error 0");
+
+ System.out.println("Push");
+ vc.push();
+ System.out.println("Assert x /= z");
+ vc.assertFormula(vc.notExpr(xeqz));
+ c = printImpliedLiterals(vc);
+ DebugAssert(c==4,"Implied literal error 1");
+ System.out.println("Pop");
+ vc.pop();
+
+ System.out.println("Push");
+ vc.push();
+ System.out.println("Assert y /= z");
+ vc.assertFormula(vc.notExpr(yeqz));
+ c = printImpliedLiterals(vc);
+ DebugAssert(c==4,"Implied literal error 2");
+ System.out.println("Pop");
+ vc.pop();
+
+ System.out.println("Push");
+ vc.push();
+ System.out.println("Assert p(x)");
+ vc.assertFormula(px);
+ c = printImpliedLiterals(vc);
+ DebugAssert(c==2,"Implied literal error 3");
+ System.out.println("Pop");
+ vc.pop();
+
+ System.out.println("Push");
+ vc.push();
+ System.out.println("Assert p(y)");
+ vc.assertFormula(py);
+ c = printImpliedLiterals(vc);
+ DebugAssert(c==2,"Implied literal error 4");
+ System.out.println("Pop");
+ vc.pop();
+
+ System.out.println("Pop");
+ vc.pop();
+
+ System.out.println("Push");
+ vc.push();
+ System.out.println("Assert y = x");
+ vc.assertFormula(yeqx);
+ c = printImpliedLiterals(vc);
+ DebugAssert(c==3,"Implied literal error 5");
+ System.out.println("Pop");
+ vc.pop();
+
+ System.out.println("Push");
+ vc.push();
+ System.out.println("Assert p(x)");
+ vc.assertFormula(px);
+ c = printImpliedLiterals(vc);
+ DebugAssert(c==1,"Implied literal error 6");
+ System.out.println("Assert x = y");
+ vc.assertFormula(xeqy);
+ c = printImpliedLiterals(vc);
+ DebugAssert(c==4,"Implied literal error 7");
+ System.out.println("Pop");
+ vc.pop();
+
+ System.out.println("Push");
+ vc.push();
+ System.out.println("Assert NOT p(x)");
+ vc.assertFormula(vc.notExpr(px));
+ c = printImpliedLiterals(vc);
+ DebugAssert(c==1,"Implied literal error 8");
+ System.out.println("Assert x = y");
+ vc.assertFormula(xeqy);
+ c = printImpliedLiterals(vc);
+ DebugAssert(c==4,"Implied literal error 9");
+ System.out.println("Pop");
+ vc.pop();
+
+ return true;
+ } catch (Exception e) {
+ System.out.println("*** Exception caught in test11(): \n" + e);
+ e.printStackTrace(System.out);
+ return false;
+ } finally {
+ if (vc != null) vc.delete();
+ }
+ }
+
+
+ public static boolean test12() throws Cvc3Exception {
+ ValidityChecker vc = null;
+ try {
+ vc = ValidityChecker.create();
+
+ Type realType = vc.realType();
+ Type intType = vc.intType();
+ Type boolType = vc.boolType();
+ vc.push();
+ int initial_layer = vc.stackLevel();
+ int initial_scope = vc.scopeLevel();
+ Expr exprObj_trueID = vc.trueExpr();
+ Expr exprObj_falseID = vc.notExpr(vc.trueExpr());
+ vc.popTo(initial_layer);
+ DebugAssert(vc.scopeLevel() == initial_scope, "Expected no change");
+ DebugAssert(vc.stackLevel() == initial_layer, "Expected no change");
+ // TODO: what happens if we push and then popscope?
+
+ return true;
+ } catch (Exception e) {
+ System.out.println("*** Exception caught in test12(): \n" + e);
+ e.printStackTrace(System.out);
+ return false;
+ } finally {
+ if (vc != null) vc.delete();
+ }
+ }
+
+
+ public static boolean test13() throws Cvc3Exception {
+ ValidityChecker vc = null;
+ FlagsMut flags = null;
+ try {
+ flags = ValidityChecker.createFlags(null);
+ flags.setFlag("dagify-exprs",false);
+ flags.setFlag("dump-log", ".test13.cvc");
+ vc = ValidityChecker.create(flags);
+
+ Expr rat_one = vc.ratExpr(1);
+ Expr rat_two = vc.ratExpr(2);
+ Expr rat_minus_one = vc.ratExpr(-1);
+
+ QueryResult query_result;
+ query_result = vc.query(vc.eqExpr(rat_two,rat_one));
+ System.out.println("2=1 " + query_result);
+ query_result = vc.query(vc.eqExpr(rat_two,rat_minus_one));
+ System.out.println("2=-1 " + query_result);
+
+ return true;
+ } catch (Exception e) {
+ System.out.println("*** Exception caught in test13(): \n" + e);
+ e.printStackTrace(System.out);
+ return false;
+ } finally {
+ if (vc != null) vc.delete();
+ if (flags != null) flags.delete();
+ }
+ }
+
+
+ public static Expr func1(ValidityChecker vc) throws Cvc3Exception {
+ // local Expr 'tmp'
+ Expr tmp = vc.varExpr("tmp", vc.boolType());
+ return vc.trueExpr();
+ }
+
+
+ public static boolean test14() throws Cvc3Exception {
+ ValidityChecker vc = null;
+ try {
+ vc = ValidityChecker.create();
+
+ // func call: ok
+ Expr test1 = func1(vc);
+
+ // func call: fail
+ Expr test2 = func1(vc);
+
+ return true;
+ } catch (Exception e) {
+ System.out.println("*** Exception caught in test13(): \n" + e);
+ e.printStackTrace(System.out);
+ return false;
+ } finally {
+ if (vc != null) vc.delete();
+ }
+ }
+
+
+ public static boolean test15() throws Cvc3Exception {
+ ValidityChecker vc = null;
+ FlagsMut flags = null;
+ try {
+ flags = ValidityChecker.createFlags(null);
+ flags.setFlag("dagify-exprs",false);
+ vc = ValidityChecker.create(flags);
+
+ /*****************************************************
+ * array declaration *
+ *****************************************************/
+
+ // array: index type
+ Type index_type = vc.subrangeType(vc.ratExpr(0),
+ vc.ratExpr(3));
+ // array: data type
+ Type data_type = vc.subrangeType(vc.ratExpr(0),
+ vc.ratExpr(3));
+ // array type: [0 .. 3] of 0 .. 3
+ Type array_type = vc.arrayType(index_type, data_type);
+ Expr arr = vc.varExpr("array", array_type);
+
+ // array: [1,1,0,0]
+ arr = vc.writeExpr(arr, vc.ratExpr(0), vc.ratExpr(1));
+ arr = vc.writeExpr(arr, vc.ratExpr(1), vc.ratExpr(1));
+ arr = vc.writeExpr(arr, vc.ratExpr(2), vc.ratExpr(0));
+ arr = vc.writeExpr(arr, vc.ratExpr(3), vc.ratExpr(0));
+
+
+
+ /*****************************************************
+ * forall Expr *
+ *****************************************************/
+
+ // for loop: index
+ Expr id = vc.boundVarExpr("id", "0", vc.subrangeType(vc.ratExpr(0),
+ vc.ratExpr(2)));
+ List vars = new ArrayList();
+ vars.add(id);
+
+ // for loop: body
+ Expr for_body = vc.leExpr(vc.readExpr(arr, id),
+ vc.readExpr(arr, vc.plusExpr(id, vc.ratExpr(1))));
+ // forall expr
+ Expr forall_expr = vc.forallExpr(vars, for_body);
+
+ vc.push();
+ check(vc, forall_expr);
+
+ System.out.println("Scope level: " + vc.scopeLevel());
+ System.out.println("Counter-example:");
+ List assertions = vc.getCounterExample();
+ for (int i = 0; i < assertions.size(); ++i) {
+ System.out.println(assertions.get(i));
+ }
+ System.out.println("End of counter-example");
+ System.out.println("");
+ vc.pop();
+
+ /*****************************************************
+ * manual expansion *
+ *****************************************************/
+
+ Expr e1 = vc.leExpr(vc.readExpr(arr, vc.ratExpr(0)),
+ vc.readExpr(arr, vc.ratExpr(1)));
+ Expr e2 = vc.leExpr(vc.readExpr(arr, vc.ratExpr(1)),
+ vc.readExpr(arr, vc.ratExpr(2)));
+ Expr e3 = vc.leExpr(vc.readExpr(arr, vc.ratExpr(2)),
+ vc.readExpr(arr, vc.ratExpr(3)));
+ Expr manual_expr = vc.andExpr(e1, vc.andExpr(e2, e3));
+
+
+
+ /*****************************************************
+ * exists Expr *
+ *****************************************************/
+
+ // exists: index
+ Expr id_ex = vc.varExpr("id_ex", vc.subrangeType(vc.ratExpr(0),
+ vc.ratExpr(2)));
+ List vars_ex = new ArrayList();
+ vars_ex.add(id_ex);
+
+ // exists: body
+ Expr ex_body = vc.gtExpr(vc.readExpr(arr, id_ex),
+ vc.readExpr(arr, vc.plusExpr(id_ex, vc.ratExpr(1))));
+ // exists expr
+ Expr ex_expr = vc.existsExpr(vars_ex, ex_body);
+
+
+
+
+ /*****************************************************
+ * ??? forall <==> manual expansion *
+ *****************************************************/
+ System.out.println("Checking forallExpr <==> manual expansion ...");
+ if (vc.query(vc.iffExpr(forall_expr, manual_expr)) == QueryResult.VALID)
+ System.out.println(" -- yes.");
+ else {
+ System.out.println(" -- no, with counter examples as ");
+
+ List assert1 = vc.getCounterExample();
+ for (int i = 0; i < assert1.size(); i ++)
+ System.out.println(assert1.get(i));
+ }
+ System.out.println();
+
+
+
+ /*****************************************************
+ * ??? !forall <==> existsExpr *
+ *****************************************************/
+ System.out.println();
+ System.out.println("Checking !forallExpr <==> existsExpr ...");
+ if (vc.query(vc.iffExpr(vc.notExpr(forall_expr), ex_expr)) == QueryResult.VALID)
+ System.out.println(" -- yes.");
+ else if (vc.incomplete()) {
+ System.out.println(" -- incomplete:");
+ List reasons = vc.incompleteReasons();
+ for (int i = 0; i < reasons.size(); ++i)
+ System.out.println(reasons.get(i));
+ }
+ else {
+ System.out.println(" -- no, with counter examples as ");
+
+ List assert2 = vc.getCounterExample();
+ for (int i = 0; i < assert2.size(); i ++)
+ System.out.println(assert2.get(i));
+ }
+
+ System.out.println();
+ System.out.println("End of testcases.");
+ System.out.println();
+
+ return true;
+ } catch (Exception e) {
+ System.out.println("*** Exception caught in test15(): \n" + e);
+ e.printStackTrace(System.out);
+ return false;
+ } finally {
+ if (vc != null) vc.delete();
+ if (flags != null) flags.delete();
+ }
+ }
+
+
+ public static boolean test16() throws Cvc3Exception {
+ ValidityChecker vc = null;
+ try {
+ vc = ValidityChecker.create();
+
+ Type zto100 = vc.subrangeType(vc.ratExpr(0), vc.ratExpr(100));
+ Expr mem = vc.varExpr("mem", vc.arrayType(zto100, vc.intType()));
+ Expr a = vc.varExpr("a", zto100);
+ Expr b = vc.varExpr("b", zto100);
+
+ Expr lhs = vc.readExpr(vc.writeExpr(mem, a, vc.ratExpr(30)), b);
+ Expr rhs = vc.readExpr(vc.writeExpr(mem, b, vc.ratExpr(40)), a);
+
+ Expr q = vc.impliesExpr(vc.notExpr(vc.eqExpr(a, b)), vc.eqExpr(lhs, rhs));
+
+ check(vc, q);
+
+ System.out.println("Scope level: " + vc.scopeLevel());
+ System.out.println("Counter-example:");
+ List assertions = vc.getCounterExample();
+ DebugAssert(assertions.size() > 0, "Expected non-empty counter-example");
+ for (int i = 0; i < assertions.size(); ++i) {
+ System.out.println(assertions.get(i));
+ }
+ System.out.println("End of counter-example");
+ System.out.println();
+
+ HashMap m = vc.getConcreteModel();
+ if(m.isEmpty())
+ System.out.println(" Did not find concrete model for any vars");
+ else {
+ System.out.println("%Satisfiable Variable Assignment: %");
+ Iterator it = m.entrySet().iterator();
+ while(it.hasNext()) {
+ Map.Entry next = (Map.Entry)it.next();
+ Expr eq;
+ Expr key = (Expr)next.getKey();
+ Expr value = (Expr)next.getValue();
+ if (key.getType().isBoolean()) {
+ DebugAssert(value.isBooleanConst(),
+ "Bad variable assignement: e = "+ key
+ +"\n\n val = "+ value);
+ if(value.isTrue())
+ eq = key;
+ else
+ eq = vc.notExpr(key);
+ }
+ else
+ eq = vc.eqExpr(key, value);
+ //:TODO:System.out.println(Expr(ASSERT, eq));
+ System.out.println(eq);
+ }
+ }
+
+ return true;
+ } catch (Exception e) {
+ System.out.println("*** Exception caught in test16(): \n" + e);
+ e.printStackTrace(System.out);
+ return false;
+ } finally {
+ if (vc != null) vc.delete();
+ }
+ }
+
+
+ public static boolean test17() throws Cvc3Exception {
+ ValidityChecker vc = null;
+ try {
+ vc = ValidityChecker.create();
+ try {
+ List selectors = new ArrayList();
+ List types = new ArrayList();
+
+ selectors.add("car");
+ types.add(vc.intType().getExpr());
+ selectors.add("cdr");
+ types.add(vc.stringExpr("list"));
+
+ Type badList = vc.dataType("list", "cons", selectors, types);
+ DebugAssert(false, "Typechecking exception expected");
+ } catch(TypecheckException e) {
+ // fall through
+ }
+
+ vc.delete();
+
+ vc = ValidityChecker.create();
+ {
+ List constructors = new ArrayList();
+ List selectors = new ArrayList();
+ List selectors0 = new ArrayList();
+ List selectors1 = new ArrayList();
+ selectors.add(selectors0);
+ selectors.add(selectors1);
+ List types = new ArrayList();
+ List types0 = new ArrayList();
+ List types1 = new ArrayList();
+ types.add(types0);
+ types.add(types1);
+
+ constructors.add("cons");
+ selectors0.add("car");
+ types0.add(vc.intType().getExpr());
+ selectors0.add("cdr");
+ types0.add(vc.stringExpr("list"));
+ constructors.add("null");
+
+ Type list = vc.dataType("list", constructors, selectors, types);
+
+ Expr x = vc.varExpr("x", vc.intType());
+ Expr y = vc.varExpr("y", list);
+
+ List args = new ArrayList();
+ args.add(x);
+ args.add(y);
+ Expr cons = vc.datatypeConsExpr("cons", args);
+
+ Expr sel = vc.datatypeSelExpr("car", cons);
+ boolean b = check(vc, vc.eqExpr(sel, x));
+ DebugAssert(b, "Should be valid");
+ }
+ vc.delete();
+
+ vc = ValidityChecker.create();
+ try {
+ List names = new ArrayList();
+ List constructors = new ArrayList();
+ List constructors0 = new ArrayList();
+ List constructors1 = new ArrayList();
+ constructors.add(constructors0);
+ constructors.add(constructors1);
+ List selectors = new ArrayList();
+ List selectors0 = new ArrayList();
+ List selectors1 = new ArrayList();
+ List selectors00 = new ArrayList();
+ List selectors10 = new ArrayList();
+ selectors.add(selectors0);
+ selectors0.add(selectors00);
+ selectors.add(selectors1);
+ selectors1.add(selectors10);
+ List types = new ArrayList();
+ List types0 = new ArrayList();
+ List types1 = new ArrayList();
+ List types00 = new ArrayList();
+ List types10 = new ArrayList();
+ types.add(types0);
+ types0.add(types00);
+ types.add(types1);
+ types1.add(types10);
+
+ names.add("list1");
+
+ constructors0.add("cons1");
+ selectors00.add("car1");
+ types00.add(vc.intType().getExpr());
+ selectors00.add("cdr1");
+ types00.add(vc.stringExpr("list2"));
+
+ names.add("list2");
+
+ constructors1.add("cons2");
+ selectors10.add("car2");
+ types10.add(vc.intType().getExpr());
+ selectors10.add("cdr2");
+ types10.add(vc.stringExpr("list1"));
+ constructors1.add("null");
+
+ List returnTypes = vc.dataType(names, constructors, selectors, types);
+
+ Type list1 = (Type)returnTypes.get(0);
+ Type list2 = (Type)returnTypes.get(1);
+
+ Expr x = vc.varExpr("x", vc.intType());
+ Expr y = vc.varExpr("y", list2);
+ Expr z = vc.varExpr("z", list1);
+
+ List args = new ArrayList();
+ args.add(x);
+ args.add(y);
+ Expr cons1 = vc.datatypeConsExpr("cons1", args);
+
+ Expr isnull = vc.datatypeTestExpr("null", y);
+ Expr hyp = vc.andExpr(vc.eqExpr(z, cons1), isnull);
+
+ Expr nullE = vc.datatypeConsExpr("null", new ArrayList());
+
+ args = new ArrayList();
+ args.add(x);
+ args.add(nullE);
+ Expr cons1_2 = vc.datatypeConsExpr("cons1", args);
+
+ boolean b = check(vc, vc.impliesExpr(hyp, vc.eqExpr(z, cons1_2)));
+ DebugAssert(b, "Should be valid");
+ } catch(TypecheckException e) {
+ // fall through
+ }
+
+ vc.delete();
+
+ vc = ValidityChecker.create();
+ {
+ List constructors = new ArrayList();
+ List selectors = new ArrayList();
+ selectors.add(new ArrayList());
+ selectors.add(new ArrayList());
+ List types = new ArrayList();
+ types.add(new ArrayList());
+ types.add(new ArrayList());
+
+ constructors.add("A");
+ constructors.add("B");
+
+ Type two = vc.dataType("two", constructors, selectors, types);
+
+ Expr x = vc.varExpr("x", two);
+ Expr y = vc.varExpr("y", two);
+ Expr z = vc.varExpr("z", two);
+
+ List args = new ArrayList();
+ args.add(vc.notExpr(vc.eqExpr(x,y)));
+ args.add(vc.notExpr(vc.eqExpr(y,z)));
+ args.add(vc.notExpr(vc.eqExpr(x,z)));
+
+ boolean b = check(vc, vc.notExpr(vc.andExpr(args)));
+ DebugAssert(b, "Should be valid");
+ }
+ return true;
+ } catch (Exception e) {
+ System.out.println("*** Exception caught in test17(): \n" + e);
+ e.printStackTrace(System.out);
+ return false;
+ } finally {
+ if (vc != null) vc.delete();
+ }
+ }
+
+
+ public static boolean test18() throws Cvc3Exception {
+ ValidityChecker vc = null;
+ FlagsMut flags = null;
+ try {
+ flags = ValidityChecker.createFlags(null);
+ flags.setFlag("tcc", true);
+ vc = ValidityChecker.create(flags);
+
+ List names = new ArrayList();
+ List constructors = new ArrayList();
+ List constructors0 = new ArrayList();
+ List constructors1 = new ArrayList();
+ List constructors2 = new ArrayList();
+ constructors.add(constructors0);
+ constructors.add(constructors1);
+ constructors.add(constructors2);
+ List selectors = new ArrayList();
+ List selectors0 = new ArrayList();
+ List selectors1 = new ArrayList();
+ List selectors2 = new ArrayList();
+ List selectors00 = new ArrayList();
+ List selectors01 = new ArrayList();
+ List selectors10 = new ArrayList();
+ List selectors11 = new ArrayList();
+ List selectors20 = new ArrayList();
+ List selectors21 = new ArrayList();
+ selectors.add(selectors0);
+ selectors0.add(selectors00);
+ selectors0.add(selectors01);
+ selectors.add(selectors1);
+ selectors1.add(selectors10);
+ selectors1.add(selectors11);
+ selectors.add(selectors2);
+ selectors2.add(selectors20);
+ selectors2.add(selectors21);
+ List types = new ArrayList();
+ List types0 = new ArrayList();
+ List types1 = new ArrayList();
+ List types2 = new ArrayList();
+ List types00 = new ArrayList();
+ List types01 = new ArrayList();
+ List types10 = new ArrayList();
+ List types11 = new ArrayList();
+ List types20 = new ArrayList();
+ List types21 = new ArrayList();
+ types.add(types0);
+ types0.add(types00);
+ types0.add(types01);
+ types.add(types1);
+ types1.add(types10);
+ types1.add(types11);
+ types.add(types2);
+ types2.add(types20);
+ types2.add(types21);
+
+ names.add("nat");
+
+ constructors0.add("zero");
+ constructors0.add("succ");
+ selectors01.add("pred");
+ types01.add(vc.stringExpr("nat"));
+
+ names.add("list");
+
+ constructors1.add("cons");
+ selectors10.add("car");
+ types10.add(vc.stringExpr("tree"));
+ selectors10.add("cdr");
+ types10.add(vc.stringExpr("list"));
+ constructors1.add("null");
+
+ names.add("tree");
+
+ constructors2.add("leaf");
+ constructors2.add("node");
+ selectors21.add("data");
+ types21.add(vc.stringExpr("nat"));
+ selectors21.add("children");
+ types21.add(vc.stringExpr("list"));
+
+ List returnTypes = vc.dataType(names, constructors, selectors, types);
+
+ Type nat = (Type)returnTypes.get(0);
+ Type listType = (Type)returnTypes.get(1);
+ Type tree = (Type)returnTypes.get(2);
+
+ Expr x = vc.varExpr("x", nat);
+
+ List args = new ArrayList();
+ Expr zero = vc.datatypeConsExpr("zero", args);
+ Expr nullE = vc.datatypeConsExpr("null", args);
+ Expr leaf = vc.datatypeConsExpr("leaf", args);
+
+ vc.push();
+ try {
+ check(vc, vc.notExpr(vc.eqExpr(zero, nullE)));
+ DebugAssert(false, "Should have caught tcc exception");
+ } catch (TypecheckException e) { }
+
+ vc.pop();
+ args.add(vc.datatypeSelExpr("pred",x));
+ Expr spx = vc.datatypeConsExpr("succ", args);
+ Expr spxeqx = vc.eqExpr(spx, x);
+ vc.push();
+ try {
+ check(vc, spxeqx);
+ DebugAssert(false, "Should have caught tcc exception");
+ } catch(TypecheckException e) { }
+
+ vc.pop();
+ boolean b = check(vc, vc.impliesExpr(vc.datatypeTestExpr("succ", x), spxeqx));
+ DebugAssert(b, "Should be valid");
+
+ b = check(vc, vc.orExpr(vc.datatypeTestExpr("zero", x),
+ vc.datatypeTestExpr("succ", x)));
+ DebugAssert(b, "Should be valid");
+
+ Expr y = vc.varExpr("y", nat);
+ Expr xeqy = vc.eqExpr(x, y);
+ args.clear();
+ args.add(x);
+ Expr sx = vc.datatypeConsExpr("succ", args);
+ args.clear();
+ args.add(y);
+ Expr sy = vc.datatypeConsExpr("succ", args);
+ Expr sxeqsy = vc.eqExpr(sx,sy);
+ b = check(vc, vc.impliesExpr(xeqy, sxeqsy));
+ DebugAssert(b, "Should be valid");
+
+ b = check(vc, vc.notExpr(vc.eqExpr(sx, zero)));
+ DebugAssert(b, "Should be valid");
+
+ b = check(vc, vc.impliesExpr(sxeqsy, xeqy));
+ DebugAssert(b, "Should be valid");
+
+ b = check(vc, vc.notExpr(vc.eqExpr(sx, x)));
+ DebugAssert(b, "Should be valid");
+
+ return true;
+ } catch (Exception e) {
+ System.out.println("*** Exception caught in test18(): \n" + e);
+ e.printStackTrace(System.out);
+ return false;
+ } finally {
+ if (vc != null) vc.delete();
+ if (flags != null) flags.delete();
+ }
+ }
+
+
+ public static boolean test19() throws Cvc3Exception {
+ ValidityChecker vc = null;
+ FlagsMut flags = null;
+ try {
+ flags = ValidityChecker.createFlags(null);
+ flags.setFlag("dagify-exprs",false);
+ vc = ValidityChecker.create(flags);
+
+ Type RealType= vc.realType();
+ Type IntType= vc.intType();
+ Type BoolType= vc.boolType();
+ Type PtrType = RealType;
+ Type HeapType = vc.arrayType(PtrType, RealType);
+
+ // -----------------
+ //ASSERT(FORALL (CVCi: REAL): (Hs[CVCi] = Ht[CVCi]));
+ //QUERY(Hs[(t6 + (3 * 1))] = Ht[(t6 + (3 * 1))]);
+ Expr Ad = vc.boundVarExpr("CVCi", "CVCi", RealType);
+ Expr Hs = vc.varExpr("Hs", HeapType);
+ Expr Ht = vc.varExpr("Ht", HeapType);
+ Expr t6 = vc.varExpr("t6", RealType);
+
+ List Vars = new ArrayList();
+ Vars.add(Ad);
+ // Body = (Hs[Ad] = Ht[Ad])
+ Expr Body = vc.eqExpr(vc.readExpr(Hs, Ad), vc.readExpr(Ht, Ad));
+
+ //A = forall (~i:REAL): Body
+ Expr A = vc.forallExpr(Vars, Body);
+
+ // Q = (Hs[t6] = Ht[t6])
+ Expr Q = vc.eqExpr(vc.readExpr(Hs, t6), vc.readExpr(Ht, t6));
+
+ // ----------- CHECK A . Q
+ vc.push();
+
+ vc.assertFormula(A);
+
+ System.out.println("Checking formula " + Q);
+ System.out.println(" in context " + A);
+
+ QueryResult Succ = vc.query(Q);
+
+ DebugAssert(Succ == QueryResult.VALID, "Expected valid formula");
+
+ return true;
+ } catch (Exception e) {
+ System.out.println("*** Exception caught in test19(): \n" + e);
+ e.printStackTrace(System.out);
+ return false;
+ } finally {
+ if (vc != null) vc.delete();
+ if (flags != null) flags.delete();
+ }
+ }
+
+ public static boolean testNonlinearBV() throws Cvc3Exception {
+ ValidityChecker vc = null;
+ FlagsMut flags = null;
+ try {
+ flags = ValidityChecker.createFlags(null);
+ flags.setFlag("dagify-exprs",false);
+ vc = ValidityChecker.create(flags);
+
+ int bvLength = 8;
+
+ Rational zero = new Rational(0, vc.embeddedManager());
+
+ Expr x = vc.varExpr("x", vc.bitvecType(bvLength));
+ Expr y = vc.varExpr("y", vc.bitvecType(bvLength));
+ Expr bv0 = vc.newBVConstExpr(zero, bvLength);
+
+ // BVUDIV
+ vc.push();
+ System.out.println("Checking BVUDIV:");
+ Expr udiv = vc.newBVUDivExpr(x, y);
+ Expr umult = vc.newBVMultExpr(bvLength, udiv, y);
+ Expr test = vc.eqExpr(bv0, y);
+ boolean result = check(vc, vc.impliesExpr(vc.notExpr(test), vc.newBVLEExpr(umult, x)), true);
+ DebugAssert(result, "Expected valid formula");
+ vc.pop();
+
+ // BVUREM
+ vc.push();
+ System.out.println("Checking BVUREM:");
+ Expr urem = vc.newBVURemExpr(x, y);
+ result = check(vc, vc.impliesExpr(vc.notExpr(test), vc.newBVLTExpr(urem, y)), true);
+ DebugAssert(result, "Expected valid formula");
+ vc.pop();
+
+ // BVSDIV
+ vc.push();
+ System.out.println("Checking BVSDIV:");
+ Expr sdiv = vc.newBVSDivExpr(x, y);
+ Expr smult = vc.newBVMultExpr(bvLength, sdiv, y);
+ Expr signed_test = vc.newBVSLEExpr(bv0, x);
+ signed_test = vc.andExpr(signed_test, vc.newBVSLTExpr(bv0, y));
+ result = check(vc, vc.impliesExpr(signed_test, vc.newBVSLEExpr(smult, x)), true);
+ DebugAssert(result, "Expected valid formula");
+ vc.pop();
+
+ // BVSREM
+ vc.push();
+ System.out.println("Checking BVSREM:");
+ Expr srem = vc.newBVSRemExpr(x, y);
+ result = check(vc, vc.impliesExpr(signed_test, vc.newBVLTExpr(srem, y)), true);
+ DebugAssert(result, "Expected valid formula");
+ vc.pop();
+
+ // BVSMOD
+ vc.push();
+ System.out.println("Checking BVSMOD:");
+ Expr smod = vc.newBVSModExpr(x, y);
+ result = check(vc, vc.impliesExpr(signed_test, vc.newBVLTExpr(smod, y)), true);
+ DebugAssert(result, "Expected valid formula");
+ vc.pop();
+
+ return true;
+ } catch (Exception e) {
+ System.out.println("*** Exception caught in test19(): \n" + e);
+ e.printStackTrace(System.out);
+ return false;
+ } finally {
+ if (vc != null) vc.delete();
+ if (flags != null) flags.delete();
+ }
+ }
+
+ public static boolean testDistinct() throws Cvc3Exception {
+ ValidityChecker vc = null;
+ FlagsMut flags = null;
+ try {
+ flags = ValidityChecker.createFlags(null);
+ vc = ValidityChecker.create(flags);
+
+ int bvLength = 2;
+ int elements_count = bvLength*bvLength + 1;
+
+ List elements = new ArrayList();
+ for (int i = 0; i < elements_count; i ++)
+ elements.add(vc.varExpr("x" + i, vc.bitvecType(bvLength)));
+ Expr distinct = vc.distinctExpr(elements);
+ boolean result = check(vc, vc.notExpr(distinct), true);
+ DebugAssert(result, "Expected valid formula");
+
+ return true;
+ } catch (Exception e) {
+ System.out.println("*** Exception caught in test19(): \n" + e);
+ e.printStackTrace(System.out);
+ return false;
+ } finally {
+ if (vc != null) vc.delete();
+ if (flags != null) flags.delete();
+ }
+ }
+
+}
+
--- /dev/null
+package cvc3;
+
+import java.util.*;
+
+public class Theorem extends Embedded {
+ // jni methods
+
+ /// Constructor
+
+ public Theorem(Object Theorem, EmbeddedManager embeddedManager) {
+ super(Theorem, embeddedManager);
+ }
+
+
+ /// API (immutable)
+
+}
--- /dev/null
+package cvc3;
+
+import java.util.*;
+
+public class TheoremMut extends Theorem {
+ // jni methods
+
+
+ /// Constructor
+
+ // create embedded object
+ public TheoremMut(Object TheoremMut, EmbeddedManager embeddedManager) {
+ super(TheoremMut, embeddedManager);
+ }
+
+
+ /// API (mutable)
+}
--- /dev/null
+package cvc3;
+
+import java.util.*;
+
+// used to enforce timeout in class Cvc3
+class TimeoutHandler extends TimerTask {
+ public void run() {
+ System.out.println("self-timeout.");
+ System.exit(1);
+ }
+}
--- /dev/null
+package cvc3;
+
+public class Type extends Embedded {
+ // jni methods
+ private static native boolean
+ jniIsAny(Object Type) throws Cvc3Exception;
+ private static native boolean
+ jniIsArray(Object Type) throws Cvc3Exception;
+ private static native boolean
+ jniIsBitvector(Object Type) throws Cvc3Exception;
+ private static native boolean
+ jniIsBool(Object Type) throws Cvc3Exception;
+ private static native boolean
+ jniIsDatatype(Object Type) throws Cvc3Exception;
+ private static native boolean
+ jniIsFunction(Object Type) throws Cvc3Exception;
+ private static native boolean
+ jniIsNull(Object Type) throws Cvc3Exception;
+ private static native boolean
+ jniIsSubtype(Object Type) throws Cvc3Exception;
+
+ private static native Object
+ jniGetExpr(Object Type) throws Cvc3Exception;
+ private static native int
+ jniArity(Object Type) throws Cvc3Exception;
+ private static native Type
+ jniGetChild(Object Type, int i) throws Cvc3Exception;
+
+ private static native boolean
+ jniEquals(Object Type1, Object Type2) throws Cvc3Exception;
+ private static native String
+ jniToString(Object Type) throws Cvc3Exception;
+
+ private static native Object jniConstr(Object expr) throws Cvc3Exception;
+
+ public static Type valueOf(Expr expr) throws Cvc3Exception {
+ return new Type(jniConstr(expr.embedded()), expr.embeddedManager());
+ }
+
+ /// Constructor
+
+ public Type(Object Type, EmbeddedManager embeddedManager) {
+ super(Type, embeddedManager);
+ }
+
+
+ /// API (immutable)
+
+ public boolean isAny() throws Cvc3Exception {
+ return jniIsAny(embedded());
+ }
+
+ public boolean isArray() throws Cvc3Exception {
+ return jniIsArray(embedded());
+ }
+
+ public boolean isBitvector() throws Cvc3Exception {
+ return jniIsBitvector(embedded());
+ }
+
+ public boolean isBoolean() throws Cvc3Exception {
+ return jniIsBool(embedded());
+ }
+
+ public boolean isDatatype() throws Cvc3Exception {
+ return jniIsDatatype(embedded());
+ }
+
+ public boolean isFunction() throws Cvc3Exception {
+ return jniIsFunction(embedded());
+ }
+
+ public boolean isNull() throws Cvc3Exception {
+ return jniIsNull(embedded());
+ }
+
+ public boolean isSubtype() throws Cvc3Exception {
+ return jniIsSubtype(embedded());
+ }
+
+
+
+
+
+ public Expr getExpr() throws Cvc3Exception {
+ return new Expr(jniGetExpr(embedded()), embeddedManager());
+ }
+
+ public int arity() throws Cvc3Exception {
+ return jniArity(embedded());
+ }
+
+ public Type getChild(int i) throws Cvc3Exception {
+ assert(i >= 0 && i < arity());
+ return new Type(jniGetChild(embedded(), i), embeddedManager());
+ }
+
+
+ // Printing
+ public String toString() {
+ String result = "";
+ try {
+ result = jniToString(embedded());
+ } catch (Cvc3Exception e) {
+ System.out.println(e);
+ assert(false);
+ }
+ return result;
+ }
+
+ public boolean equals(Object o) {
+ if (this == o) return true;
+
+ if (!(o instanceof Type)) return false;
+ boolean result = false;
+ try {
+ result = jniEquals(embedded(), ((Embedded)o).embedded());
+ } catch (Cvc3Exception e) {
+ assert(false);
+ }
+ return result;
+ }
+
+ // must return the same hash code for two exprs if equals returns true
+
+ public int hashCode() {
+ try {
+ return getExpr().hashCode();
+ } catch (Cvc3Exception e) {
+ assert(false);
+ }
+ assert(false);
+ return 0;
+ }
+}
--- /dev/null
+package cvc3;
+
+import java.util.*;
+
+public class TypeMut extends Type {
+ // jni methods
+
+
+ /// Constructor
+
+ // create embedded object
+ public TypeMut(Object TypeMut, EmbeddedManager embeddedManager) {
+ super(TypeMut, embeddedManager);
+ }
+
+
+ /// API (mutable)
+}
--- /dev/null
+INCLUDE: "kinds.h"
+INCLUDE: "type.h"
+INCLUDE: "theory_array.h"
+INCLUDE: "theory_bitvector.h"
+INCLUDE: "theory_datatype.h"
+
+DEFINITION: Java_cvc3_Type_jniConstr
+jobject c Expr expr
+return embed_copy<Type>(env, Type(*expr));
+
+DEFINITION: Java_cvc3_Type_jniIsAny
+jboolean c Type type
+return type->getExpr().getKind() == ANY_TYPE;
+
+DEFINITION: Java_cvc3_Type_jniIsArray
+jboolean c Type type
+return type->getExpr().getKind() == ARRAY;
+
+DEFINITION: Java_cvc3_Type_jniIsBitvector
+jboolean c Type type
+return type->getExpr().getKind() == BITVECTOR;
+
+DEFINITION: Java_cvc3_Type_jniIsBool
+jboolean c Type type
+return type->isBool();
+
+DEFINITION: Java_cvc3_Type_jniIsDatatype
+jboolean c Type type
+return ::isDatatype(*type);
+
+DEFINITION: Java_cvc3_Type_jniIsFunction
+jboolean c Type type
+return type->isFunction();
+
+DEFINITION: Java_cvc3_Type_jniIsNull
+jboolean c Type type
+return type->isNull();
+
+DEFINITION: Java_cvc3_Type_jniIsSubtype
+jboolean c Type type
+return type->isSubtype();
+
+
+
+DEFINITION: Java_cvc3_Type_jniGetExpr
+jobject c Type type
+return embed_const_ref<Expr>(env, &type->getExpr());
+
+DEFINITION: Java_cvc3_Type_jniArity
+jint c Type type
+return type->arity();
+
+DEFINITION: Java_cvc3_Type_jniGetChild
+jobject c Type type n int i
+return embed_copy<Type>(env, (*type)[i]);
+
+
+
+
+DEFINITION: Java_cvc3_Type_jniEquals
+jboolean c Type type1 c Type type2
+return *type1 == *type2;
+
+DEFINITION: Java_cvc3_Type_jniToString
+jstring c Type type
+return toJava(env, type->toString());
+
--- /dev/null
+package cvc3;
+
+import java.util.*;
+
+/** mirrors CVC3::TypecheckException */
+public class TypecheckException extends Cvc3Exception {
+
+ private final static long serialVersionUID = 1L;
+
+ public TypecheckException(String message) {
+ super(message);
+ }
+}
--- /dev/null
+package cvc3;
+
+import java.util.*;
+
+import cvc3.Expr;
+import cvc3.JniUtils;
+
+public class ValidityChecker extends Embedded {
+ // jni methods
+ private static native Object
+ jniCreate1() throws Cvc3Exception;
+ private static native Object
+ jniCreate2(Object Flags) throws Cvc3Exception;
+ private static native Object
+ jniCreateFlags() throws Cvc3Exception;
+ private static native Object
+ jniGetFlags(Object ValidityChecker) throws Cvc3Exception;
+
+
+ private static native Object
+ jniBoolType(Object ValidityChecker) throws Cvc3Exception;
+ private static native Object
+ jniRealType(Object ValidityChecker) throws Cvc3Exception;
+ private static native Object
+ jniIntType(Object ValidityChecker) throws Cvc3Exception;
+ private static native Object
+ jniSubrangeType(Object ValidityChecker, Object lExpr, Object rExpr) throws Cvc3Exception;
+ private static native Object
+ jniSubtypeType(Object ValidityChecker, Object predExpr, Object witnessExpr) throws Cvc3Exception;
+ private static native Object
+ jniTupleType1(Object ValidityChecker, Object Type0, Object Type1) throws Cvc3Exception;
+ private static native Object
+ jniTupleType2(Object ValidityChecker, Object Type0, Object Type1, Object Type2) throws Cvc3Exception;
+ private static native Object
+ jniTupleType3(Object ValidityChecker, Object[] Types) throws Cvc3Exception;
+ private static native Object
+ jniRecordType1(Object ValidityChecker, String field, Object Type) throws Cvc3Exception;
+ private static native Object
+ jniRecordType2(Object ValidityChecker, String field0, Object Type0,
+ String field1, Object Type1) throws Cvc3Exception;
+ private static native Object
+ jniRecordType3(Object ValidityChecker, String field0, Object Type0,
+ String field1, Object Type1, String field2, Object Type2) throws Cvc3Exception;
+ private static native Object
+ jniRecordType4(Object ValidityChecker, Object[] fields, Object[] types) throws Cvc3Exception;
+ private static native Object
+ jniDataType1(Object ValidityChecker, String name, String constructor,
+ Object[] selectors, Object[] types) throws Cvc3Exception;
+ private static native Object
+ jniDataType2(Object ValidityChecker, String name, Object[] constructors,
+ Object[] selectors, Object[] types) throws Cvc3Exception;
+ private static native Object[]
+ jniDataType3(Object ValidityChecker, Object[] names, Object[] constructors,
+ Object[] selectors, Object[] types) throws Cvc3Exception;
+ private static native Object
+ jniAnyType(Object ValidityChecker) throws Cvc3Exception;
+ private static native Object
+ jniArrayLiteral(Object ValidityChecker, Object indexVar, Object bodyExpr) throws Cvc3Exception;
+ private static native Object
+ jniArrayType(Object ValidityChecker, Object TypeIndex, Object TypeData) throws Cvc3Exception;
+ private static native Object
+ jniBitvecType(Object ValidityChecker, int n) throws Cvc3Exception;
+ private static native Object
+ jniFunType1(Object ValidityChecker, Object typeDom, Object TypeRan) throws Cvc3Exception;
+ private static native Object
+ jniFunType2(Object ValidityChecker, Object[] typeDom, Object TypeRan) throws Cvc3Exception;
+ private static native Object
+ jniCreateType1(Object ValidityChecker, String typeName) throws Cvc3Exception;
+ private static native Object
+ jniCreateType2(Object ValidityChecker, String typeName, Object TypeDef) throws Cvc3Exception;
+ private static native Object
+ jniLookupType(Object ValidityChecker, String typeName) throws Cvc3Exception;
+
+
+ private static native Object
+ jniGetExprManager(Object ValidityChecker) throws Cvc3Exception;
+ private static native Object
+ jniNullExpr(Object ValidityChecker) throws Cvc3Exception;
+ private static native Object
+ jniVarExpr1(Object ValidityChecker, String name, Object Type) throws Cvc3Exception;
+ private static native Object
+ jniVarExpr2(Object ValidityChecker, String name, Object Type, Object defExpr) throws Cvc3Exception;
+ private static native Object
+ jniBoundVarExpr(Object ValidityChecker, String name, String uid, Object Type) throws Cvc3Exception;
+ /*private static native Object
+ jniBoundVarExpr2(Object ValidityChecker, Object Type) throws Cvc3Exception;
+ */
+ private static native Object
+ jniLookupVar(Object ValidityChecker, String name) throws Cvc3Exception;
+ private static native Object
+ jniLookupOp(Object ValidityChecker, String name) throws Cvc3Exception;
+ private static native Object
+ jniGetType(Object ValidityChecker, Object Expr) throws Cvc3Exception;
+ private static native Object
+ jniGetBaseType1(Object ValidityChecker, Object Expr) throws Cvc3Exception;
+ private static native Object
+ jniGetBaseType2(Object ValidityChecker, Object Type) throws Cvc3Exception;
+ private static native Object
+ jniGetTypePred(Object ValidityChecker, Object Type, Object Expr) throws Cvc3Exception;
+ private static native Object
+ jniStringExpr(Object ValidityChecker, String str) throws Cvc3Exception;
+ private static native Object
+ jniIdExpr(Object ValidityChecker, String name) throws Cvc3Exception;
+ private static native Object
+ jniListExpr1(Object ValidityChecker, Object[] kids) throws Cvc3Exception;
+ private static native Object
+ jniListExpr2(Object ValidityChecker, Object Expr1) throws Cvc3Exception;
+ private static native Object
+ jniListExpr3(Object ValidityChecker, Object Expr1, Object Expr2) throws Cvc3Exception;
+ private static native Object
+ jniListExpr4(Object ValidityChecker, Object Expr1, Object Expr2, Object Expr3) throws Cvc3Exception;
+ private static native Object
+ jniListExpr5(Object ValidityChecker, String op, Object[] kids) throws Cvc3Exception;
+ private static native Object
+ jniListExpr6(Object ValidityChecker, String op, Object Expr1) throws Cvc3Exception;
+ private static native Object
+ jniListExpr7(Object ValidityChecker, String op, Object Expr1, Object Expr2) throws Cvc3Exception;
+ private static native Object
+ jniListExpr8(Object ValidityChecker, String op, Object Expr1, Object Expr2, Object Expr3) throws Cvc3Exception;
+ private static native void
+ jniPrintExpr(Object ValidityChecker, Object Expr) throws Cvc3Exception;
+ private static native Object
+ jniParseExpr(Object ValidityChecker, Object Expr) throws Cvc3Exception;
+ private static native Object
+ jniParseType(Object ValidityChecker, Object Expr) throws Cvc3Exception;
+ private static native Object
+ jniImportExpr(Object ValidityChecker, Object Expr) throws Cvc3Exception;
+ private static native Object
+ jniImportType(Object ValidityChecker, Object Type) throws Cvc3Exception;
+ private static native void
+ jniCmdsFromString(Object ValidityChecker, String s) throws Cvc3Exception;
+ private static native Object
+ jniExprFromString(Object ValidityChecker, String s) throws Cvc3Exception;
+ private static native Object
+ jniTrueExpr(Object ValidityChecker) throws Cvc3Exception;
+ private static native Object
+ jniFalseExpr(Object ValidityChecker) throws Cvc3Exception;
+ private static native Object
+ jniNotExpr(Object ValidityChecker, Object Expr) throws Cvc3Exception;
+ private static native Object
+ jniAndExpr1(Object ValidityChecker, Object ExprLeft, Object ExprRight) throws Cvc3Exception;
+ private static native Object
+ jniAndExpr2(Object ValidityChecker, Object[] ExprChildren) throws Cvc3Exception;
+ private static native Object
+ jniOrExpr1(Object ValidityChecker, Object ExprLeft, Object ExprRight) throws Cvc3Exception;
+ private static native Object
+ jniOrExpr2(Object ValidityChecker, Object[] Exprchildren) throws Cvc3Exception;
+ private static native Object
+ jniImpliesExpr(Object ValidityChecker, Object ExprHyp, Object ExprConc) throws Cvc3Exception;
+ private static native Object
+ jniIffExpr(Object ValidityChecker, Object ExprLeft, Object ExprRight) throws Cvc3Exception;
+ private static native Object
+ jniEqExpr(Object ValidityChecker, Object Expr1, Object Expr2) throws Cvc3Exception;
+ private static native Object
+ jniDistinctExpr(Object ValidityChecker, Object[] ExprChildren) throws Cvc3Exception;
+ private static native Object
+ jniIteExpr(Object ValidityChecker, Object ExprIf, Object ExprThen, Object ExprElse) throws Cvc3Exception;
+ private static native Object
+ jniCreateOp1(Object ValidityChecker, String name, Object Type) throws Cvc3Exception;
+ private static native Object
+ jniCreateOp2(Object ValidityChecker, String name, Object Type, Object ExprDef) throws Cvc3Exception;
+ private static native Object
+ jniEqOp() throws Cvc3Exception;
+ private static native Object
+ jniLtOp() throws Cvc3Exception;
+ private static native Object
+ jniLeOp() throws Cvc3Exception;
+ private static native Object
+ jniGtOp() throws Cvc3Exception;
+ private static native Object
+ jniGeOp() throws Cvc3Exception;
+ private static native Object
+ jniPlusOp() throws Cvc3Exception;
+ private static native Object
+ jniMinusOp() throws Cvc3Exception;
+ private static native Object
+ jniMultOp() throws Cvc3Exception;
+ private static native Object
+ jniDivideOp() throws Cvc3Exception;
+ private static native Object
+ jniFunExpr1(Object ValidityChecker, Object Op, Object Expr) throws Cvc3Exception;
+ private static native Object
+ jniFunExpr2(Object ValidityChecker, Object Op, Object ExprLeft, Object ExprRight) throws Cvc3Exception;
+ private static native Object
+ jniFunExpr3(Object ValidityChecker, Object Op, Object Expr1, Object Expr2, Object Expr3) throws Cvc3Exception;
+ private static native Object
+ jniFunExpr4(Object ValidityChecker, Object Op, Object[] ExprChildren) throws Cvc3Exception;
+ private static native Object
+ jniRatExpr1(Object ValidityChecker, int n, int d) throws Cvc3Exception;
+ private static native Object
+ jniRatExpr2(Object ValidityChecker, String n, String d, int base) throws Cvc3Exception;
+ private static native Object
+ jniRatExpr3(Object ValidityChecker, String n, int base) throws Cvc3Exception;
+ private static native Object
+ jniUminusExpr(Object ValidityChecker, Object Expr) throws Cvc3Exception;
+ private static native Object
+ jniPlusExpr1(Object ValidityChecker, Object Exprleft, Object ExprRight) throws Cvc3Exception;
+ private static native Object
+ jniPlusExpr2(Object ValidityChecker, Object[] kids) throws Cvc3Exception;
+ private static native Object
+ jniMinusExpr(Object ValidityChecker, Object ExprLeft, Object ExprRight) throws Cvc3Exception;
+ private static native Object
+ jniMultExpr(Object ValidityChecker, Object ExprLeft, Object ExprRight) throws Cvc3Exception;
+ private static native Object
+ jniPowExpr(Object ValidityChecker, Object ExprX, Object ExprN) throws Cvc3Exception;
+ private static native Object
+ jniDivideExpr(Object ValidityChecker, Object ExprNumerator, Object ExprDenominator) throws Cvc3Exception;
+ private static native Object
+ jniLtExpr(Object ValidityChecker, Object ExprLeft, Object ExprRight) throws Cvc3Exception;
+ private static native Object
+ jniLeExpr(Object ValidityChecker, Object ExprLeft, Object ExprRight) throws Cvc3Exception;
+ private static native Object
+ jniGtExpr(Object ValidityChecker, Object ExprLeft, Object ExprRight) throws Cvc3Exception;
+ private static native Object
+ jniGeExpr(Object ValidityChecker, Object ExprLeft, Object ExprRight) throws Cvc3Exception;
+ private static native Object
+ jniRecordExpr1(Object ValidityChecker, String field, Object Expr) throws Cvc3Exception;
+ private static native Object
+ jniRecordExpr2(Object ValidityChecker, String field1, Object Expr1,
+ String field2, Object Expr2) throws Cvc3Exception;
+ private static native Object
+ jniRecordExpr3(Object ValidityChecker, String field1, Object Expr1, String field2, Object Expr2,
+ String field3, Object Expr3) throws Cvc3Exception;
+ private static native Object
+ jniRecordExpr4(Object ValidityChecker, Object[] StringFields, Object[] Exprs) throws Cvc3Exception;
+ private static native Object
+ jniRecSelectExpr(Object ValidityChecker, Object ExprRecord, String field) throws Cvc3Exception;
+ private static native Object
+ jniRecUpdateExpr(Object ValidityChecker, Object ExprRecord, String field,
+ Object ExprNewValue) throws Cvc3Exception;
+ private static native Object
+ jniReadExpr(Object ValidityChecker, Object ExprArray, Object ExprIndex) throws Cvc3Exception;
+ private static native Object
+ jniWriteExpr(Object ValidityChecker, Object ExprArray, Object ExprIndex,
+ Object ExprNewValue) throws Cvc3Exception;
+ private static native Object
+ jniNewBVConstExpr1(Object ValidityChecker, String s, int base) throws Cvc3Exception;
+ private static native Object
+ jniNewBVConstExpr2(Object ValidityChecker, boolean[] bits) throws Cvc3Exception;
+ private static native Object
+ jniNewBVConstExpr3(Object ValidityChecker, Object RationalR, int len) throws Cvc3Exception;
+ private static native Object
+ jniNewConcatExpr1(Object ValidityChecker, Object Expr1, Object Expr2) throws Cvc3Exception;
+ private static native Object
+ jniNewConcatExpr2(Object ValidityChecker, Object[] Exprkids) throws Cvc3Exception;
+ private static native Object
+ jniNewBVExtractExpr(Object ValidityChecker, Object ExprE, int hi, int low) throws Cvc3Exception;
+ private static native Object
+ jniNewBVNegExpr(Object ValidityChecker, Object Expr1) throws Cvc3Exception;
+ private static native Object
+ jniNewBVAndExpr1(Object ValidityChecker, Object Expr1, Object Expr2) throws Cvc3Exception;
+ private static native Object
+ jniNewBVAndExpr2(Object ValidityChecker, Object[] ExprKids) throws Cvc3Exception;
+ private static native Object
+ jniNewBVOrExpr1(Object ValidityChecker, Object Expr1, Object Expr2) throws Cvc3Exception;
+ private static native Object
+ jniNewBVOrExpr2(Object ValidityChecker, Object[] ExprKids) throws Cvc3Exception;
+ private static native Object
+ jniNewBVXorExpr1(Object ValidityChecker, Object Expr1, Object Expr2) throws Cvc3Exception;
+ private static native Object
+ jniNewBVXorExpr2(Object ValidityChecker, Object[] ExprKids) throws Cvc3Exception;
+ private static native Object
+ jniNewBVXnorExpr1(Object ValidityChecker, Object Expr1, Object Expr2) throws Cvc3Exception;
+ private static native Object
+ jniNewBVXnorExpr2(Object ValidityChecker, Object[] ExprKids) throws Cvc3Exception;
+ private static native Object
+ jniNewBVNandExpr(Object ValidityChecker, Object Expr1, Object Expr2) throws Cvc3Exception;
+ private static native Object
+ jniNewBVNorExpr(Object ValidityChecker, Object Expr1, Object Expr2) throws Cvc3Exception;
+ private static native Object
+ jniNewBVLTExpr(Object ValidityChecker, Object Expr1, Object Expr2) throws Cvc3Exception;
+ private static native Object
+ jniNewBVLEExpr(Object ValidityChecker, Object Expr1, Object Expr2) throws Cvc3Exception;
+ private static native Object
+ jniNewBVSLTExpr(Object ValidityChecker, Object Expr1, Object Expr2) throws Cvc3Exception;
+ private static native Object
+ jniNewBVSLEExpr(Object ValidityChecker, Object Expr1, Object Expr2) throws Cvc3Exception;
+ private static native Object
+ jniNewSXExpr(Object ValidityChecker, Object Expr1, int len) throws Cvc3Exception;
+ private static native Object
+ jniNewBVUminusExpr(Object ValidityChecker, Object Expr) throws Cvc3Exception;
+ private static native Object
+ jniNewBVSubExpr(Object ValidityChecker, Object Expr1, Object Expr2) throws Cvc3Exception;
+ private static native Object
+ jniNewBVPlusExpr(Object ValidityChecker, int numbits, Object[] ExprK) throws Cvc3Exception;
+ private static native Object
+ jniNewBVMultExpr(Object ValidityChecker, int numbits, Object Expr1, Object Expr2) throws Cvc3Exception;
+ private static native Object
+ jniNewBVUDivExpr(Object ValidityChecker, Object left, Object right) throws Cvc3Exception;
+ private static native Object
+ jniNewBVURemExpr(Object ValidityChecker, Object left, Object right) throws Cvc3Exception;
+ private static native Object
+ jniNewBVSDivExpr(Object ValidityChecker, Object left, Object right) throws Cvc3Exception;
+ private static native Object
+ jniNewBVSRemExpr(Object ValidityChecker, Object left, Object right) throws Cvc3Exception;
+ private static native Object
+ jniNewBVSModExpr(Object ValidityChecker, Object left, Object right) throws Cvc3Exception;
+ private static native Object
+ jniNewBVSHL(Object ValidityChecker, Object left, Object right) throws Cvc3Exception;
+ private static native Object
+ jniNewBVLSHR(Object ValidityChecker, Object left, Object right) throws Cvc3Exception;
+ private static native Object
+ jniNewBVASHR(Object ValidityChecker, Object left, Object right) throws Cvc3Exception;
+ private static native Object
+ jniNewFixedLeftShiftExpr(Object ValidityChecker, Object Expr1, int r) throws Cvc3Exception;
+ private static native Object
+ jniNewFixedConstWidthLeftShiftExpr(Object ValidityChecker, Object Expr1, int r) throws Cvc3Exception;
+ private static native Object
+ jniNewFixedRightShiftExpr(Object ValidityChecker, Object Expr1, int r) throws Cvc3Exception;
+ private static native Object
+ jniComputeBVConst(Object ValidityChecker, Object Expr) throws Cvc3Exception;
+ private static native Object
+ jniTupleExpr(Object ValidityChecker, Object[] Exprs) throws Cvc3Exception;
+ private static native Object
+ jniTupleSelectExpr(Object ValidityChecker, Object ExprTuple, int index) throws Cvc3Exception;
+ private static native Object
+ jniTupleUpdateExpr(Object ValidityChecker, Object ExprTuple, int index,
+ Object ExprNewValue) throws Cvc3Exception;
+ private static native Object
+ jniDatatypeConsExpr(Object ValidityChecker, String constructor, Object[] ExprArgs) throws Cvc3Exception;
+ private static native Object
+ jniDatatypeSelExpr(Object ValidityChecker, String selector, Object ExprArg) throws Cvc3Exception;
+ private static native Object
+ jniDatatypeTestExpr(Object ValidityChecker, String constructor, Object ExprArg) throws Cvc3Exception;
+ private static native Object
+ jniForallExpr1(Object ValidityChecker, Object[] ExprVars, Object ExprBody) throws Cvc3Exception;
+ private static native Object
+ jniForallExpr2(Object ValidityChecker, Object[] ExprVars, Object ExprBody,
+ Object ExprTrigger) throws Cvc3Exception;
+ private static native Object
+ jniForallExpr3(Object ValidityChecker, Object[] ExprVars, Object ExprBody,
+ Object[] ExprTriggers) throws Cvc3Exception;
+ private static native Object
+ jniForallExpr4(Object ValidityChecker, Object[] ExprVars, Object ExprBody,
+ Object[][] ExprTriggers) throws Cvc3Exception;
+ private static native void
+ jniSetTrigger(Object ValidityChecker, Object ExprClosure, Object ExprTrigger) throws Cvc3Exception;
+ private static native void
+ jniSetTriggers(Object ValidityChecker, Object ExprClosure, Object[] ExprTriggers) throws Cvc3Exception;
+ private static native void
+ jniSetTriggers2(Object ValidityChecker, Object ExprClosure, Object[][] ExprTriggers) throws Cvc3Exception;
+ private static native void
+ jniSetMultiTrigger(Object ValidityChecker, Object ExprClosure, Object[] ExprMultiTrigger) throws Cvc3Exception;
+ private static native Object
+ jniExistsExpr(Object ValidityChecker, Object[] ExprVars, Object ExprBody) throws Cvc3Exception;
+ private static native Object
+ jniLambdaExpr(Object ValidityChecker, Object[] ExprVars, Object ExprBody) throws Cvc3Exception;
+ private static native Object
+ jniTransClosure(Object ValidityChecker, Object Op) throws Cvc3Exception;
+ private static native Object
+ jniSimulateExpr(Object ValidityChecker, Object ExprF, Object ExprS,
+ Object[] ExprInputs, Object ExprN) throws Cvc3Exception;
+
+ private static native void
+ jniSetResourceLimit(Object ValidityChecker, int limit) throws Cvc3Exception;
+ private static native void
+ jniAssertFormula(Object ValidityChecker, Object Expr) throws Cvc3Exception;
+ private static native void
+ jniRegisterAtom(Object ValidityChecker, Object Expr) throws Cvc3Exception;
+ private static native Object
+ jniGetImpliedLiteral(Object ValidityChecker) throws Cvc3Exception;
+ private static native Object
+ jniSimplify(Object ValidityChecker, Object Expr) throws Cvc3Exception;
+ private static native String
+ jniQuery(Object ValidityChecker, Object Expr) throws Cvc3Exception;
+ private static native String
+ jniCheckUnsat(Object ValidityChecker, Object Expr) throws Cvc3Exception;
+ private static native String
+ jniCheckContinue(Object ValidityChecker) throws Cvc3Exception;
+ private static native String
+ jniRestart(Object ValidityChecker, Object Expr) throws Cvc3Exception;
+ private static native void
+ jniReturnFromCheck(Object ValidityChecker) throws Cvc3Exception;
+ private static native Object[]
+ jniGetUserAssumptions(Object ValidityChecker) throws Cvc3Exception;
+ private static native Object[]
+ jniGetInternalAssumptions(Object ValidityChecker) throws Cvc3Exception;
+ private static native Object[]
+ jniGetAssumptions(Object ValidityChecker) throws Cvc3Exception;
+ private static native Object[]
+ jniGetAssumptionsUsed(Object ValidityChecker) throws Cvc3Exception;
+ private static native Object[]
+ jniGetCounterExample(Object ValidityChecker, boolean inOrder) throws Cvc3Exception;
+ private static native Object[]
+ jniGetConcreteModel(Object ValidityChecker) throws Cvc3Exception;
+ private static native String
+ jniGetValue(Object ValidityChecker, Object Expr) throws Cvc3Exception;
+ private static native boolean
+ jniInconsistent1(Object ValidityChecker) throws Cvc3Exception;
+ private static native Object[]
+ jniInconsistent2(Object ValidityChecker) throws Cvc3Exception;
+ private static native boolean
+ jniIncomplete1(Object ValidityChecker) throws Cvc3Exception;
+ private static native Object[]
+ jniIncomplete2(Object ValidityChecker) throws Cvc3Exception;
+ private static native Object
+ jniGetProof(Object ValidityChecker) throws Cvc3Exception;
+ private static native Object
+ jniGetTCC(Object ValidityChecker) throws Cvc3Exception;
+ private static native Object[]
+ jniGetAssumptionsTCC(Object ValidityChecker) throws Cvc3Exception;
+ private static native Object
+ jniGetProofTCC(Object ValidityChecker) throws Cvc3Exception;
+ private static native Object
+ jniGetClosure(Object ValidityChecker) throws Cvc3Exception;
+ private static native Object
+ jniGetProofClosure(Object ValidityChecker) throws Cvc3Exception;
+
+ private static native int
+ jniStackLevel(Object ValidityChecker) throws Cvc3Exception;
+ private static native void
+ jniPush(Object ValidityChecker) throws Cvc3Exception;
+ private static native void
+ jniPop(Object ValidityChecker) throws Cvc3Exception;
+ private static native void
+ jniPopTo(Object ValidityChecker, int stackLevel) throws Cvc3Exception;
+ private static native int
+ jniScopeLevel(Object ValidityChecker) throws Cvc3Exception;
+ private static native void
+ jniPushScope(Object ValidityChecker) throws Cvc3Exception;
+ private static native void
+ jniPopScope(Object ValidityChecker) throws Cvc3Exception;
+ private static native void
+ jniPopToScope(Object ValidityChecker, int scopeLevel) throws Cvc3Exception;
+ private static native Object
+ jniGetCurrentContext(Object ValidityChecker) throws Cvc3Exception;
+
+ private static native void
+ jniLoadFile1(Object ValidityChecker, String fileName, String lang) throws Cvc3Exception;
+
+ private static native Object
+ jniGetStatistics(Object ValidityChecker) throws Cvc3Exception;
+ private static native void
+ jniPrintStatistics(Object ValidityChecker) throws Cvc3Exception;
+
+ private static native void
+ jniSetTimeLimit(Object ValidityChecker, int limit) throws Cvc3Exception;
+
+
+
+ // delete ValidityChecker, all expressions created using it,
+ // and all embedded objects registered with its embeddedManager
+ public synchronized void delete() throws Cvc3Exception {
+ if (isDeleted()) return;
+
+ //:TEST:
+ embeddedManager().cleanUp();
+
+ embeddedManager().delete();
+ EmbeddedManager.jniDelete(embedded());
+ d_embedded = null;
+ }
+
+ // ensure that all embedded objects are deallocated eventually
+ public void finalize() throws Throwable {
+ try {
+ if (!isDeleted()) {
+ assert(false);
+// System.out.println("ValidityChecker.Finalizer: should never be called");
+ throw new Error("ValidityChecker.Finalizer: should never be called");
+ }
+ } finally {
+ super.finalize();
+ }
+ }
+
+ /// Constructor
+
+ // create embedded object
+ protected ValidityChecker(Object ValidityChecker) {
+ super(ValidityChecker, new EmbeddedManager());
+ }
+
+
+ /// API: ValidityChecker
+
+
+ // Creation
+
+ // delete must be called before ValidityChecker is garbage collected
+ public static ValidityChecker create() throws Cvc3Exception {
+ return new ValidityChecker(jniCreate1());
+ }
+
+ // delete must be called before ValidityChecker is garbage collected
+ public static ValidityChecker create(Flags flags) throws Cvc3Exception {
+ return new ValidityChecker(jniCreate2(flags.embedded()));
+ }
+
+
+ // Flags
+
+ // if embeddedManger is null then delete must be called before
+ // the returned Flags is garbage collected
+ public static FlagsMut createFlags(EmbeddedManager embeddedManager) throws Cvc3Exception {
+ return new FlagsMut(jniCreateFlags(), embeddedManager);
+ }
+
+ public FlagsMut getFlags() throws Cvc3Exception {
+ return new FlagsMut(jniGetFlags(embedded()), embeddedManager());
+ }
+
+
+
+ // Type-related methods
+
+ public TypeMut boolType() throws Cvc3Exception {
+ return new TypeMut(jniBoolType(embedded()), embeddedManager());
+ }
+
+ public TypeMut realType() throws Cvc3Exception {
+ return new TypeMut(jniRealType(embedded()), embeddedManager());
+ }
+
+ public TypeMut intType() throws Cvc3Exception {
+ return new TypeMut(jniIntType(embedded()), embeddedManager());
+ }
+
+ public TypeMut subrangeType(Expr l, Expr r) throws Cvc3Exception {
+ return new TypeMut(
+ jniSubrangeType(embedded(), l.embedded(), r.embedded()),
+ embeddedManager());
+ }
+
+ public TypeMut subtypeType(Expr pred, Expr witness) throws Cvc3Exception {
+ return new TypeMut(
+ jniSubtypeType(embedded(), pred.embedded(), witness.embedded()),
+ embeddedManager());
+ }
+
+ public TypeMut tupleType(Type type0, Type type1) throws Cvc3Exception {
+ return new TypeMut(
+ jniTupleType1(embedded(), type0.embedded(), type1.embedded()),
+ embeddedManager());
+ }
+
+ public TypeMut tupleType(Type type0, Type type1, Type type2) throws Cvc3Exception {
+ return new TypeMut(
+ jniTupleType2(embedded(), type0.embedded(), type1.embedded(), type2.embedded()),
+ embeddedManager());
+ }
+
+ public TypeMut tupleType(List types) throws Cvc3Exception {
+ return new TypeMut(
+ jniTupleType3(embedded(), JniUtils.unembedList(types)),
+ embeddedManager());
+ }
+
+ public TypeMut recordType(String field, Type type) throws Cvc3Exception {
+ return new TypeMut(
+ jniRecordType1(embedded(), field, type.embedded()),
+ embeddedManager());
+ }
+
+ public TypeMut recordType(String field0, Type type0, String field1, Type type1) throws Cvc3Exception {
+ return new TypeMut(
+ jniRecordType2(embedded(), field0, type0.embedded(), field1, type1.embedded()),
+ embeddedManager());
+ }
+
+ public TypeMut recordType(String field0, Type type0, String field1, Type type1,
+ String field2, Type type2) throws Cvc3Exception {
+ return new TypeMut(
+ jniRecordType3(embedded(), field0, type0.embedded(), field1, type1.embedded(),
+ field2, type2.embedded()),
+ embeddedManager());
+ }
+
+ public TypeMut recordType(List fields, List types) throws Cvc3Exception {
+ assert(JniUtils.listInstanceof(fields, String.class));
+ return new TypeMut(
+ jniRecordType4(embedded(), JniUtils.toArray(fields), JniUtils.unembedList(types)),
+ embeddedManager());
+ }
+
+ public TypeMut dataType(String name, String constructor,
+ List selectors, List types) throws Cvc3Exception {
+ assert(JniUtils.listInstanceof(selectors, String.class));
+ assert(JniUtils.listInstanceof(types, Expr.class));
+ return new TypeMut(
+ jniDataType1(embedded(), name, constructor,
+ JniUtils.toArray(selectors), JniUtils.unembedList(types)),
+ embeddedManager());
+ }
+
+ public TypeMut dataType(String name, String[] constructors,
+ String[][] selectors, Expr[][] types) throws Cvc3Exception {
+ return new TypeMut(
+ jniDataType2(embedded(), name, constructors, selectors, JniUtils.unembedArrayArray(types)),
+ embeddedManager());
+ }
+
+ public TypeMut dataType(String name, List constructors,
+ List selectors, List types) throws Cvc3Exception {
+ assert(JniUtils.listInstanceof(constructors, String.class));
+ assert(JniUtils.listListInstanceof(selectors, String.class));
+ assert(JniUtils.listListInstanceof(types, Expr.class));
+ return new TypeMut(
+ jniDataType2(embedded(), name, JniUtils.toArray(constructors),
+ JniUtils.toArrayArray(selectors), JniUtils.unembedListList(types)),
+ embeddedManager());
+ }
+
+ public List dataType(List names, List constructors,
+ List selectors, List types) throws Cvc3Exception {
+ assert(JniUtils.listInstanceof(names, String.class));
+ assert(JniUtils.listListInstanceof(constructors, String.class));
+ assert(JniUtils.listListListInstanceof(selectors, String.class));
+ assert(JniUtils.listListListInstanceof(types, Expr.class));
+ Object[] dataTypes =
+ jniDataType3(embedded(), JniUtils.toArray(names), JniUtils.toArrayArray(constructors),
+ JniUtils.toArrayArrayArray(selectors), JniUtils.unembedListListList(types));
+ return JniUtils.embedList(dataTypes, TypeMut.class, embeddedManager());
+ }
+
+ public ExprMut arrayLiteral(Expr var, Expr body) throws Cvc3Exception {
+ return new ExprMut(jniArrayLiteral(embedded(), var.embedded(), body.embedded()),embeddedManager());
+ }
+
+ public TypeMut anyType() throws Cvc3Exception {
+ return new TypeMut(jniAnyType(embedded()),embeddedManager());
+ }
+
+ public TypeMut arrayType(Type typeIndex, Type typeData) throws Cvc3Exception {
+ return new TypeMut(
+ jniArrayType(embedded(), typeIndex.embedded(), typeData.embedded()),
+ embeddedManager());
+ }
+
+ public TypeMut bitvecType(int n) throws Cvc3Exception {
+ return new TypeMut(
+ jniBitvecType(embedded(), n),
+ embeddedManager());
+ }
+
+ public TypeMut funType(Type typeDom, Type typeRange) throws Cvc3Exception {
+ return new TypeMut(
+ jniFunType1(embedded(), typeDom.embedded(), typeRange.embedded()),
+ embeddedManager());
+ }
+
+ public TypeMut funType(List typeDom, Type typeRange) throws Cvc3Exception {
+ assert(JniUtils.listInstanceof(typeDom, Type.class));
+ return new TypeMut(
+ jniFunType2(embedded(), JniUtils.unembedList(typeDom), typeRange.embedded()),
+ embeddedManager());
+ }
+
+ public TypeMut createType(String typeName) throws Cvc3Exception {
+ return new TypeMut(
+ jniCreateType1(embedded(), typeName),
+ embeddedManager());
+ }
+
+ public TypeMut createType(String typeName, Type typeDef) throws Cvc3Exception {
+ return new TypeMut(
+ jniCreateType2(embedded(), typeName, typeDef.embedded()),
+ embeddedManager());
+ }
+
+ public TypeMut lookupType(String typeName) throws Cvc3Exception {
+ return new TypeMut(
+ jniLookupType(embedded(), typeName),
+ embeddedManager());
+ }
+
+
+
+ // Expressions
+
+ public ExprManagerMut getExprManager() throws Cvc3Exception {
+ return new ExprManagerMut(jniGetExprManager(embedded()), embeddedManager());
+ }
+
+ public Expr nullExpr() throws Cvc3Exception {
+ return new Expr(jniNullExpr(embedded()), embeddedManager());
+ }
+
+ public ExprMut varExpr(String name, Type type) throws Cvc3Exception {
+ return new ExprMut(
+ jniVarExpr1(embedded(), name, type.embedded()),
+ embeddedManager());
+ }
+
+ public ExprMut varExpr(String name, Type type, Expr def) throws Cvc3Exception {
+ return new ExprMut(
+ jniVarExpr2(embedded(), name, type.embedded(), def.embedded()),
+ embeddedManager());
+ }
+
+ public ExprMut boundVarExpr(String name, String uid, Type type) throws Cvc3Exception {
+ return new ExprMut(
+ jniBoundVarExpr(embedded(), name, uid, type.embedded()),
+ embeddedManager());
+ }
+
+/* public ExprMut boundVarExpr(Type type) throws Cvc3Exception {
+ return new ExprMut(
+ jniBoundVarExpr(embedded(), type.embedded()),
+ embeddedManager());
+ }*/
+
+ public ExprMut lookupVar(String name) throws Cvc3Exception {
+ return new ExprMut(
+ jniLookupVar(embedded(), name),
+ embeddedManager());
+ }
+
+ public OpMut lookupOp(String name) throws Cvc3Exception {
+ return new OpMut(
+ jniLookupOp(embedded(), name),
+ embeddedManager());
+ }
+
+ public TypeMut getType(Expr expr) throws Cvc3Exception {
+ return new TypeMut(
+ jniGetType(embedded(), expr.embedded()),
+ embeddedManager());
+ }
+
+ public TypeMut getBaseType(Expr expr) throws Cvc3Exception {
+ return new TypeMut(
+ jniGetBaseType1(embedded(), expr.embedded()),
+ embeddedManager());
+ }
+
+ public TypeMut getBaseType(Type type) throws Cvc3Exception {
+ return new TypeMut(
+ jniGetBaseType2(embedded(), type.embedded()),
+ embeddedManager());
+ }
+
+ public ExprMut getTypePred(Type type, Expr expr) throws Cvc3Exception {
+ return new ExprMut(
+ jniGetTypePred(embedded(), type.embedded(), expr.embedded()),
+ embeddedManager());
+ }
+
+ public ExprMut stringExpr(String str) throws Cvc3Exception {
+ return new ExprMut(
+ jniStringExpr(embedded(), str),
+ embeddedManager());
+ }
+
+ public ExprMut idExpr(String name) throws Cvc3Exception {
+ return new ExprMut(
+ jniIdExpr(embedded(), name),
+ embeddedManager());
+ }
+
+ public ExprMut listExpr(List kids) throws Cvc3Exception {
+ assert(JniUtils.listInstanceof(kids, Expr.class));
+ return new ExprMut(
+ jniListExpr1(embedded(), JniUtils.unembedList(kids)),
+ embeddedManager());
+ }
+
+ public ExprMut listExpr(Expr expr1) throws Cvc3Exception {
+ return new ExprMut(
+ jniListExpr2(embedded(), expr1.embedded()),
+ embeddedManager());
+ }
+
+ public ExprMut listExpr(Expr expr1, Expr expr2) throws Cvc3Exception {
+ return new ExprMut(
+ jniListExpr3(embedded(), expr1.embedded(), expr2.embedded()),
+ embeddedManager());
+ }
+
+ public ExprMut listExpr(Expr expr1, Expr expr2, Expr expr3) throws Cvc3Exception {
+ return new ExprMut(
+ jniListExpr4(embedded(), expr1.embedded(), expr2.embedded(), expr3.embedded()),
+ embeddedManager());
+ }
+
+ public ExprMut listExpr(String op, List kids) throws Cvc3Exception {
+ assert(JniUtils.listInstanceof(kids, Expr.class));
+ return new ExprMut(
+ jniListExpr5(embedded(), op, JniUtils.unembedList(kids)),
+ embeddedManager());
+ }
+
+ public ExprMut listExpr(String op, Expr expr1) throws Cvc3Exception {
+ return new ExprMut(
+ jniListExpr6(embedded(), op, expr1.embedded()),
+ embeddedManager());
+ }
+
+ public ExprMut listExpr(String op, Expr expr1, Expr expr2) throws Cvc3Exception {
+ return new ExprMut(
+ jniListExpr7(embedded(), op, expr1.embedded(), expr2.embedded()),
+ embeddedManager());
+ }
+
+ public ExprMut listExpr(String op, Expr expr1, Expr expr2, Expr expr3) throws Cvc3Exception {
+ return new ExprMut(
+ jniListExpr8(embedded(), op, expr1.embedded(), expr2.embedded(), expr3.embedded()),
+ embeddedManager());
+ }
+
+ public void printExpr(Expr expr) throws Cvc3Exception {
+ jniPrintExpr(embedded(), expr.embedded());
+ }
+
+ public ExprMut parseExpr(Expr expr) throws Cvc3Exception {
+ return new ExprMut(
+ jniParseExpr(embedded(), expr.embedded()),
+ embeddedManager());
+ }
+
+ public TypeMut parseType(Expr expr) throws Cvc3Exception {
+ return new TypeMut(
+ jniParseType(embedded(), expr.embedded()),
+ embeddedManager());
+ }
+
+ public ExprMut importExpr(Expr expr) throws Cvc3Exception {
+ return new ExprMut(
+ jniImportExpr(embedded(), expr.embedded()),
+ embeddedManager());
+ }
+
+ public TypeMut importType(Type type) throws Cvc3Exception {
+ return new TypeMut(
+ jniImportType(embedded(), type.embedded()),
+ embeddedManager());
+ }
+
+ public void cmdsFromString(String s) throws Cvc3Exception {
+ jniCmdsFromString(embedded(), s);
+ }
+
+ public ExprMut exprFromString(String s) throws Cvc3Exception {
+ return new ExprMut( jniExprFromString(embedded(), s), embeddedManager() );
+ }
+
+
+ public ExprMut trueExpr() throws Cvc3Exception {
+ return new ExprMut(jniTrueExpr(embedded()), embeddedManager());
+ }
+
+ public ExprMut falseExpr() throws Cvc3Exception {
+ return new ExprMut(jniFalseExpr(embedded()), embeddedManager());
+ }
+
+ public ExprMut notExpr(Expr expr) throws Cvc3Exception {
+ return new ExprMut(
+ jniNotExpr(embedded(), expr.embedded()),
+ embeddedManager());
+ }
+
+ public ExprMut andExpr(Expr expr1, Expr expr2) throws Cvc3Exception {
+ return new ExprMut(
+ jniAndExpr1(embedded(), expr1.embedded(), expr2.embedded()),
+ embeddedManager());
+ }
+
+ public ExprMut andExpr(List children) throws Cvc3Exception {
+ assert(JniUtils.listInstanceof(children, Expr.class));
+ return new ExprMut(
+ jniAndExpr2(embedded(), JniUtils.unembedList(children)),
+ embeddedManager());
+ }
+
+ public ExprMut orExpr(Expr expr1, Expr expr2) throws Cvc3Exception {
+ return new ExprMut(
+ jniOrExpr1(embedded(), expr1.embedded(), expr2.embedded()),
+ embeddedManager());
+ }
+
+ public ExprMut orExpr(List children) throws Cvc3Exception {
+ assert(JniUtils.listInstanceof(children, Expr.class));
+ return new ExprMut(
+ jniOrExpr2(embedded(), JniUtils.unembedList(children)),
+ embeddedManager());
+ }
+
+ public ExprMut impliesExpr(Expr hyp, Expr conc) throws Cvc3Exception {
+ return new ExprMut(
+ jniImpliesExpr(embedded(), hyp.embedded(), conc.embedded()),
+ embeddedManager());
+ }
+
+ public ExprMut iffExpr(Expr left, Expr right) throws Cvc3Exception {
+ return new ExprMut(
+ jniIffExpr(embedded(), left.embedded(), right.embedded()),
+ embeddedManager());
+ }
+
+ public ExprMut eqExpr(Expr left, Expr right) throws Cvc3Exception {
+ return new ExprMut(
+ jniEqExpr(embedded(), left.embedded(), right.embedded()),
+ embeddedManager());
+ }
+
+ public ExprMut distinctExpr(List children) throws Cvc3Exception {
+ assert(JniUtils.listInstanceof(children, Expr.class));
+ return new ExprMut(
+ jniDistinctExpr(embedded(), JniUtils.unembedList(children)), embeddedManager());
+ }
+
+ public ExprMut iteExpr(Expr ifPart, Expr thenPart, Expr elsePart) throws Cvc3Exception {
+ return new ExprMut(
+ jniIteExpr(embedded(), ifPart.embedded(), thenPart.embedded(), elsePart.embedded()),
+ embeddedManager());
+ }
+
+ public OpMut createOp(String name, Type type) throws Cvc3Exception {
+ return new OpMut(
+ jniCreateOp1(embedded(), name, type.embedded()),
+ embeddedManager());
+ }
+
+ public OpMut createOp(String name, Type type, Expr expr) throws Cvc3Exception {
+ return new OpMut(
+ jniCreateOp2(embedded(), name, type.embedded(), expr.embedded()),
+ embeddedManager());
+ }
+
+ // '='
+ public OpMut eqOp() throws Cvc3Exception {
+ return new OpMut(jniEqOp(), embeddedManager());
+ }
+
+ // '<'
+ public OpMut ltOp() throws Cvc3Exception {
+ return new OpMut(jniLtOp(), embeddedManager());
+ }
+
+ // '<='
+ public OpMut leOp() throws Cvc3Exception {
+ return new OpMut(jniLeOp(), embeddedManager());
+ }
+
+ // '>'
+ public OpMut gtOp() throws Cvc3Exception {
+ return new OpMut(jniGtOp(), embeddedManager());
+ }
+
+ // '>='
+ public OpMut geOp() throws Cvc3Exception {
+ return new OpMut(jniGeOp(), embeddedManager());
+ }
+
+ // '+'
+ public OpMut plusOp() throws Cvc3Exception {
+ return new OpMut(jniPlusOp(), embeddedManager());
+ }
+
+ // '-'
+ public OpMut minusOp() throws Cvc3Exception {
+ return new OpMut(jniMinusOp(), embeddedManager());
+ }
+
+ // '*'
+ public OpMut multOp() throws Cvc3Exception {
+ return new OpMut(jniMultOp(), embeddedManager());
+ }
+
+ // '/' for rationals
+ public OpMut divideOp() throws Cvc3Exception {
+ return new OpMut(jniDivideOp(), embeddedManager());
+ }
+
+ public ExprMut funExpr(Op op, Expr expr1) throws Cvc3Exception {
+ return new ExprMut(
+ jniFunExpr1(embedded(), op.embedded(), expr1.embedded()),
+ embeddedManager());
+ }
+
+ public ExprMut funExpr(Op op, Expr expr1, Expr expr2) throws Cvc3Exception {
+ return new ExprMut(
+ jniFunExpr2(embedded(), op.embedded(), expr1.embedded(), expr2.embedded()),
+ embeddedManager());
+ }
+
+ public ExprMut funExpr(Op op, Expr expr1, Expr expr2, Expr expr3) throws Cvc3Exception {
+ return new ExprMut(
+ jniFunExpr3(embedded(), op.embedded(), expr1.embedded(), expr2.embedded(), expr3.embedded()),
+ embeddedManager());
+ }
+
+ public ExprMut funExpr(Op op, List children) throws Cvc3Exception {
+ assert(JniUtils.listInstanceof(children, Expr.class));
+ return new ExprMut(
+ jniFunExpr4(embedded(), op.embedded(), JniUtils.unembedList(children)),
+ embeddedManager());
+ }
+
+ public ExprMut ratExpr(int n) throws Cvc3Exception {
+ return ratExpr(n, 1);
+ }
+
+ public ExprMut ratExpr(int n, int d) throws Cvc3Exception {
+ return new ExprMut(
+ jniRatExpr1(embedded(), n, d),
+ embeddedManager());
+ }
+
+ public ExprMut ratExpr(String n, String d, int base) throws Cvc3Exception {
+ return new ExprMut(
+ jniRatExpr2(embedded(), n, d, base),
+ embeddedManager());
+ }
+
+ public ExprMut ratExpr(String n) throws Cvc3Exception {
+ return ratExpr(n, 10);
+ }
+
+ public ExprMut ratExpr(String n, int base) throws Cvc3Exception {
+ return new ExprMut(
+ jniRatExpr3(embedded(), n, base),
+ embeddedManager());
+ }
+
+ public ExprMut uminusExpr(Expr expr) throws Cvc3Exception {
+ return new ExprMut(
+ jniUminusExpr(embedded(), expr.embedded()),
+ embeddedManager());
+ }
+
+ public ExprMut plusExpr(Expr left, Expr right) throws Cvc3Exception {
+ return new ExprMut(
+ jniPlusExpr1(embedded(), left.embedded(), right.embedded()),
+ embeddedManager());
+ }
+
+ public ExprMut plusExpr(List kids) throws Cvc3Exception {
+ return new ExprMut(
+ jniPlusExpr2(embedded(), JniUtils.unembedList(kids)),
+ embeddedManager());
+ }
+
+ public ExprMut minusExpr(Expr left, Expr right) throws Cvc3Exception {
+ return new ExprMut(
+ jniMinusExpr(embedded(), left.embedded(), right.embedded()),
+ embeddedManager());
+ }
+
+ public ExprMut multExpr(Expr left, Expr right) throws Cvc3Exception {
+ return new ExprMut(
+ jniMultExpr(embedded(), left.embedded(), right.embedded()),
+ embeddedManager());
+ }
+
+ public ExprMut powExpr(Expr x, Expr n) throws Cvc3Exception {
+ return new ExprMut(
+ jniPowExpr(embedded(), x.embedded(), n.embedded()),
+ embeddedManager());
+ }
+
+ public ExprMut divideExpr(Expr numerator, Expr denominator) throws Cvc3Exception {
+ return new ExprMut(
+ jniDivideExpr(embedded(), numerator.embedded(), denominator.embedded()),
+ embeddedManager());
+ }
+
+ public ExprMut ltExpr(Expr left, Expr right) throws Cvc3Exception {
+ return new ExprMut(
+ jniLtExpr(embedded(), left.embedded(), right.embedded()),
+ embeddedManager());
+ }
+
+ public ExprMut leExpr(Expr left, Expr right) throws Cvc3Exception {
+ return new ExprMut(
+ jniLeExpr(embedded(), left.embedded(), right.embedded()),
+ embeddedManager());
+ }
+
+ public ExprMut gtExpr(Expr left, Expr right) throws Cvc3Exception {
+ return new ExprMut(
+ jniGtExpr(embedded(), left.embedded(), right.embedded()),
+ embeddedManager());
+ }
+
+ public ExprMut geExpr(Expr left, Expr right) throws Cvc3Exception {
+ return new ExprMut(
+ jniGeExpr(embedded(), left.embedded(), right.embedded()),
+ embeddedManager());
+ }
+
+ public ExprMut recordExpr(String field, Expr expr) throws Cvc3Exception {
+ return new ExprMut(
+ jniRecordExpr1(embedded(), field, expr.embedded()),
+ embeddedManager());
+ }
+
+ public ExprMut recordExpr(String field1, Expr expr1, String field2, Expr expr2) throws Cvc3Exception {
+ return new ExprMut(
+ jniRecordExpr2(embedded(), field1, expr1.embedded(), field2, expr2.embedded()),
+ embeddedManager());
+ }
+
+ public ExprMut recordExpr(String field1, Expr expr1, String field2, Expr expr2,
+ String field3, Expr expr3) throws Cvc3Exception {
+ return new ExprMut(
+ jniRecordExpr3(embedded(), field1, expr1.embedded(), field2, expr2.embedded(),
+ field3, expr3.embedded()),
+ embeddedManager());
+ }
+
+ public ExprMut recordExpr(List fields, List exprs) throws Cvc3Exception {
+ assert(JniUtils.listInstanceof(fields, String.class));
+ assert(JniUtils.listInstanceof(exprs, Expr.class));
+ return new ExprMut(
+ jniRecordExpr4(embedded(), JniUtils.toArray(fields), JniUtils.unembedList(exprs)),
+ embeddedManager());
+ }
+
+ public ExprMut recSelectExpr(Expr record, String field) throws Cvc3Exception {
+ return new ExprMut(
+ jniRecSelectExpr(embedded(), record.embedded(), field),
+ embeddedManager());
+ }
+
+ public ExprMut recUpdateExpr(Expr record, String field, Expr newValue) throws Cvc3Exception {
+ return new ExprMut(
+ jniRecUpdateExpr(embedded(), record.embedded(), field, newValue.embedded()),
+ embeddedManager());
+ }
+
+ public ExprMut readExpr(Expr array, Expr index) throws Cvc3Exception {
+ return new ExprMut(
+ jniReadExpr(embedded(), array.embedded(), index.embedded()),
+ embeddedManager());
+ }
+
+ public ExprMut writeExpr(Expr array, Expr index, Expr newValue) throws Cvc3Exception {
+ return new ExprMut(
+ jniWriteExpr(embedded(), array.embedded(), index.embedded(), newValue.embedded()),
+ embeddedManager());
+ }
+
+ public ExprMut newBVConstExpr(String s) throws Cvc3Exception {
+ return newBVConstExpr(s, 2);
+ }
+
+ public ExprMut newBVConstExpr(String s, int base) throws Cvc3Exception {
+ return new ExprMut(
+ jniNewBVConstExpr1(embedded(), s, base),
+ embeddedManager());
+ }
+
+ public ExprMut newBVConstExpr(boolean[] bits) throws Cvc3Exception {
+ return new ExprMut(
+ jniNewBVConstExpr2(embedded(), bits),
+ embeddedManager());
+ }
+
+ public ExprMut newBVConstExpr(Rational r, int len) throws Cvc3Exception {
+ return new ExprMut(
+ jniNewBVConstExpr3(embedded(), r.embedded(), len),
+ embeddedManager());
+ }
+
+ public ExprMut newConcatExpr(Expr expr1, Expr expr2) throws Cvc3Exception {
+ return new ExprMut(
+ jniNewConcatExpr1(embedded(), expr1.embedded(), expr2.embedded()),
+ embeddedManager());
+ }
+
+ public ExprMut newConcatExpr(List kids) throws Cvc3Exception {
+ assert(JniUtils.listInstanceof(kids, Expr.class));
+ return new ExprMut(
+ jniNewConcatExpr2(embedded(), JniUtils.unembedList(kids)),
+ embeddedManager());
+ }
+
+ public ExprMut newBVExtractExpr(Expr e, int hi, int low) throws Cvc3Exception {
+ return new ExprMut(
+ jniNewBVExtractExpr(embedded(), e.embedded(), hi, low),
+ embeddedManager());
+ }
+
+ public ExprMut newBVNegExpr(Expr expr) throws Cvc3Exception {
+ return new ExprMut(
+ jniNewBVNegExpr(embedded(), expr.embedded()),
+ embeddedManager());
+ }
+
+ public ExprMut newBVAndExpr(Expr expr1, Expr expr2) throws Cvc3Exception {
+ return new ExprMut(
+ jniNewBVAndExpr1(embedded(), expr1.embedded(), expr2.embedded()),
+ embeddedManager());
+ }
+
+ public ExprMut newBVAndExpr(List kids) throws Cvc3Exception {
+ assert(JniUtils.listInstanceof(kids, Expr.class));
+ return new ExprMut(
+ jniNewBVAndExpr2(embedded(), JniUtils.unembedList(kids)),
+ embeddedManager());
+ }
+
+ public ExprMut newBVOrExpr(Expr expr1, Expr expr2) throws Cvc3Exception {
+ return new ExprMut(
+ jniNewBVOrExpr1(embedded(), expr1.embedded(), expr2.embedded()),
+ embeddedManager());
+ }
+
+ public ExprMut newBVOrExpr(List kids) throws Cvc3Exception {
+ assert(JniUtils.listInstanceof(kids, Expr.class));
+ return new ExprMut(
+ jniNewBVOrExpr2(embedded(), JniUtils.unembedList(kids)),
+ embeddedManager());
+ }
+
+ public ExprMut newBVXorExpr(Expr expr1, Expr expr2) throws Cvc3Exception {
+ return new ExprMut(
+ jniNewBVXorExpr1(embedded(), expr1.embedded(), expr2.embedded()),
+ embeddedManager());
+ }
+
+ public ExprMut newBVXorExpr(List kids) throws Cvc3Exception {
+ assert(JniUtils.listInstanceof(kids, Expr.class));
+ return new ExprMut(
+ jniNewBVXorExpr2(embedded(), JniUtils.unembedList(kids)),
+ embeddedManager());
+ }
+
+ public ExprMut newBVXnorExpr(Expr expr1, Expr expr2) throws Cvc3Exception {
+ return new ExprMut(
+ jniNewBVXnorExpr1(embedded(), expr1.embedded(), expr2.embedded()),
+ embeddedManager());
+ }
+
+ public ExprMut newBVXnorExpr(List kids) throws Cvc3Exception {
+ assert(JniUtils.listInstanceof(kids, Expr.class));
+ return new ExprMut(
+ jniNewBVXnorExpr2(embedded(), JniUtils.unembedList(kids)),
+ embeddedManager());
+ }
+
+ public ExprMut newBVNandExpr(Expr expr1, Expr expr2) throws Cvc3Exception {
+ return new ExprMut(
+ jniNewBVNandExpr(embedded(), expr1.embedded(), expr2.embedded()),
+ embeddedManager());
+ }
+
+ public ExprMut newBVNorExpr(Expr expr1, Expr expr2) throws Cvc3Exception {
+ return new ExprMut(
+ jniNewBVNorExpr(embedded(), expr1.embedded(), expr2.embedded()),
+ embeddedManager());
+ }
+
+ public ExprMut newBVLTExpr(Expr expr1, Expr expr2) throws Cvc3Exception {
+ return new ExprMut(
+ jniNewBVLTExpr(embedded(), expr1.embedded(), expr2.embedded()),
+ embeddedManager());
+ }
+
+ public ExprMut newBVLEExpr(Expr expr1, Expr expr2) throws Cvc3Exception {
+ return new ExprMut(
+ jniNewBVLEExpr(embedded(), expr1.embedded(), expr2.embedded()),
+ embeddedManager());
+ }
+
+ public ExprMut newBVSLTExpr(Expr expr1, Expr expr2) throws Cvc3Exception {
+ return new ExprMut(
+ jniNewBVSLTExpr(embedded(), expr1.embedded(), expr2.embedded()),
+ embeddedManager());
+ }
+
+ public ExprMut newBVSLEExpr(Expr expr1, Expr expr2) throws Cvc3Exception {
+ return new ExprMut(
+ jniNewBVSLEExpr(embedded(), expr1.embedded(), expr2.embedded()),
+ embeddedManager());
+ }
+
+ public ExprMut newSXExpr(Expr expr, int len) throws Cvc3Exception {
+ return new ExprMut(
+ jniNewSXExpr(embedded(), expr.embedded(), len),
+ embeddedManager());
+ }
+
+ public ExprMut newBVUminusExpr(Expr expr) throws Cvc3Exception {
+ return new ExprMut(
+ jniNewBVUminusExpr(embedded(), expr.embedded()),
+ embeddedManager());
+ }
+
+ public ExprMut newBVSubExpr(Expr expr1, Expr expr2) throws Cvc3Exception {
+ return new ExprMut(
+ jniNewBVSubExpr(embedded(), expr1.embedded(), expr2.embedded()),
+ embeddedManager());
+ }
+
+ public ExprMut newBVPlusExpr(int numbits, List exprs) throws Cvc3Exception {
+ assert(JniUtils.listInstanceof(exprs, Expr.class));
+ return new ExprMut(
+ jniNewBVPlusExpr(embedded(), numbits, JniUtils.unembedList(exprs)),
+ embeddedManager());
+ }
+
+ public ExprMut newBVMultExpr(int numbits, Expr expr1, Expr expr2) throws Cvc3Exception {
+ return new ExprMut(
+ jniNewBVMultExpr(embedded(), numbits, expr1.embedded(), expr2.embedded()),
+ embeddedManager());
+ }
+
+ public ExprMut newBVUDivExpr(Expr left, Expr right) throws Cvc3Exception {
+ return new ExprMut(
+ jniNewBVUDivExpr(embedded(), left.embedded(), right.embedded()),
+ embeddedManager());
+ }
+
+ public ExprMut newBVURemExpr(Expr left, Expr right) throws Cvc3Exception {
+ return new ExprMut(
+ jniNewBVURemExpr(embedded(), left.embedded(), right.embedded()),
+ embeddedManager());
+ }
+
+ public ExprMut newBVSDivExpr(Expr left, Expr right) throws Cvc3Exception {
+ return new ExprMut(
+ jniNewBVSDivExpr(embedded(), left.embedded(), right.embedded()),
+ embeddedManager());
+ }
+
+ public ExprMut newBVSRemExpr(Expr left, Expr right) throws Cvc3Exception {
+ return new ExprMut(
+ jniNewBVSRemExpr(embedded(), left.embedded(), right.embedded()),
+ embeddedManager());
+ }
+
+ public ExprMut newBVSModExpr(Expr left, Expr right) throws Cvc3Exception {
+ return new ExprMut(
+ jniNewBVSModExpr(embedded(), left.embedded(), right.embedded()),
+ embeddedManager());
+ }
+
+ public ExprMut newBVSHL(Expr left, Expr right) throws Cvc3Exception {
+ return new ExprMut(
+ jniNewBVSHL(embedded(), left.embedded(), right.embedded()),
+ embeddedManager());
+ }
+
+ public ExprMut newBVLSHR(Expr left, Expr right) throws Cvc3Exception {
+ return new ExprMut(
+ jniNewBVLSHR(embedded(), left.embedded(), right.embedded()),
+ embeddedManager());
+ }
+
+ public ExprMut newBVASHR(Expr left, Expr right) throws Cvc3Exception {
+ return new ExprMut(
+ jniNewBVASHR(embedded(), left.embedded(), right.embedded()),
+ embeddedManager());
+ }
+
+ public ExprMut newFixedLeftShiftExpr(Expr expr, int r) throws Cvc3Exception {
+ return new ExprMut(
+ jniNewFixedLeftShiftExpr(embedded(), expr.embedded(), r),
+ embeddedManager());
+ }
+
+ public ExprMut newFixedConstWidthLeftShiftExpr(Expr expr, int r) throws Cvc3Exception {
+ return new ExprMut(
+ jniNewFixedConstWidthLeftShiftExpr(embedded(), expr.embedded(), r),
+ embeddedManager());
+ }
+
+ public ExprMut newFixedRightShiftExpr(Expr expr, int r) throws Cvc3Exception {
+ return new ExprMut(
+ jniNewFixedRightShiftExpr(embedded(), expr.embedded(), r),
+ embeddedManager());
+ }
+
+ public Rational computeBVConst(Expr expr) {
+ Rational rat = new Rational(
+ jniComputeBVConst(embedded(),expr.embedded()),
+ embeddedManager());
+ assert( rat.isInteger() );
+ return rat;
+ }
+
+ public ExprMut tupleExpr(List exprs) throws Cvc3Exception {
+ assert(JniUtils.listInstanceof(exprs, Expr.class));
+ return new ExprMut(
+ jniTupleExpr(embedded(), JniUtils.unembedList(exprs)),
+ embeddedManager());
+ }
+
+ public ExprMut tupleSelectExpr(Expr tuple, int index) throws Cvc3Exception {
+ return new ExprMut(
+ jniTupleSelectExpr(embedded(), tuple.embedded(), index),
+ embeddedManager());
+ }
+
+ public ExprMut tupleUpdateExpr(Expr tuple, int index, Expr newValue) throws Cvc3Exception {
+ return new ExprMut(
+ jniTupleUpdateExpr(embedded(), tuple.embedded(), index, newValue.embedded()),
+ embeddedManager());
+ }
+
+ public ExprMut datatypeConsExpr(String constructor, List exprs) throws Cvc3Exception {
+ assert(JniUtils.listInstanceof(exprs, Expr.class));
+ return new ExprMut(
+ jniDatatypeConsExpr(embedded(), constructor, JniUtils.unembedList(exprs)),
+ embeddedManager());
+ }
+
+ public ExprMut datatypeSelExpr(String selector, Expr arg) throws Cvc3Exception {
+ return new ExprMut(
+ jniDatatypeSelExpr(embedded(), selector, arg.embedded()),
+ embeddedManager());
+ }
+
+ public ExprMut datatypeTestExpr(String constructor, Expr arg) throws Cvc3Exception {
+ return new ExprMut(
+ jniDatatypeTestExpr(embedded(), constructor, arg.embedded()),
+ embeddedManager());
+ }
+
+ public ExprMut forallExpr(List vars, Expr body) throws Cvc3Exception {
+ assert(JniUtils.listInstanceof(vars, Expr.class));
+ return new ExprMut(
+ jniForallExpr1(embedded(), JniUtils.unembedList(vars), body.embedded()),
+ embeddedManager());
+ }
+
+ public ExprMut forallExpr(List vars, Expr body, Expr trigger) throws Cvc3Exception {
+ assert(JniUtils.listInstanceof(vars, Expr.class));
+ return new ExprMut(
+ jniForallExpr2(embedded(), JniUtils.unembedList(vars), body.embedded(),
+ trigger.embedded()),
+ embeddedManager());
+ }
+
+ public ExprMut forallExpr(List vars, Expr body, List triggers) throws Cvc3Exception {
+ assert(JniUtils.listInstanceof(vars, Expr.class));
+ assert(JniUtils.listInstanceof(triggers, Expr.class));
+ return new ExprMut(
+ jniForallExpr3(embedded(), JniUtils.unembedList(vars), body.embedded(),
+ JniUtils.unembedList(triggers)),
+ embeddedManager());
+ }
+
+ public ExprMut forallExprMultiTriggers(List vars, Expr body, List multiTriggers)
+ throws Cvc3Exception {
+ assert (JniUtils.listInstanceof(vars, Expr.class));
+ assert (JniUtils.listListInstanceof(multiTriggers, Expr.class));
+ return new ExprMut(jniForallExpr4(embedded(), JniUtils.unembedList(vars),
+ body.embedded(), JniUtils.unembedListList(multiTriggers)),
+ embeddedManager());
+ }
+
+ public void setTrigger(Expr closure, Expr trigger) throws Cvc3Exception {
+ jniSetTrigger(embedded(), closure.embedded(), trigger.embedded());
+ }
+
+ public void setTriggers(Expr closure, List triggers) throws Cvc3Exception {
+ jniSetTriggers(embedded(), closure.embedded(), JniUtils.unembedList(triggers));
+ }
+
+ public void setMultiTrigger(Expr closure, List multiTrigger) throws Cvc3Exception {
+ jniSetMultiTrigger(embedded(), closure.embedded(), JniUtils.unembedList(multiTrigger));
+ }
+
+ public void setMultiTriggers(Expr closure, List triggers) throws Cvc3Exception {
+ jniSetTriggers2(embedded(), closure.embedded(), JniUtils.unembedListList(triggers));
+ }
+
+ public ExprMut existsExpr(List vars, Expr body) throws Cvc3Exception {
+ assert(JniUtils.listInstanceof(vars, Expr.class));
+ return new ExprMut(
+ jniExistsExpr(embedded(), JniUtils.unembedList(vars), body.embedded()),
+ embeddedManager());
+ }
+
+ public OpMut lambdaExpr(List vars, Expr body) throws Cvc3Exception {
+ assert(JniUtils.listInstanceof(vars, Expr.class));
+ return new OpMut(
+ jniLambdaExpr(embedded(), JniUtils.unembedList(vars), body.embedded()),
+ embeddedManager());
+ }
+
+ public OpMut transClosure(Op p) throws Cvc3Exception {
+ return new OpMut(
+ jniTransClosure(embedded(), p.embedded()),
+ embeddedManager());
+ }
+
+ public ExprMut simulateExpr(Expr f, Expr s, List inputs, Expr n) throws Cvc3Exception {
+ assert(JniUtils.listInstanceof(inputs, Expr.class));
+ return new ExprMut(
+ jniSimulateExpr(embedded(), f.embedded(), s.embedded(), JniUtils.unembedList(inputs), n.embedded()),
+ embeddedManager());
+ }
+
+
+ public void setResourceLimit(int limit) throws Cvc3Exception {
+ jniSetResourceLimit(embedded(), limit);
+ }
+
+ // Validity checking methods
+
+ public void assertFormula(Expr expr) throws Cvc3Exception {
+ embeddedManager().cleanUp();
+ jniAssertFormula(embedded(), expr.embedded());
+ embeddedManager().cleanUp();
+ }
+
+ public void registerAtom(Expr expr) throws Cvc3Exception {
+ jniRegisterAtom(embedded(), expr.embedded());
+ }
+
+ public ExprMut getImpliedLiteral() throws Cvc3Exception {
+ return new ExprMut(
+ jniGetImpliedLiteral(embedded()),
+ embeddedManager());
+ }
+
+ public ExprMut simplify(Expr expr) throws Cvc3Exception {
+ return new ExprMut(
+ jniSimplify(embedded(), expr.embedded()),
+ embeddedManager());
+ }
+
+ public QueryResult query(Expr expr) throws Cvc3Exception {
+ embeddedManager().cleanUp();
+ QueryResult result = QueryResult.get(jniQuery(embedded(), expr.embedded()));
+
+ //:TEST:
+ embeddedManager().cleanUp();
+ return result;
+ }
+
+ public SatResult checkUnsat(Expr expr) throws Cvc3Exception {
+ embeddedManager().cleanUp();
+ SatResult result = SatResult.get(jniCheckUnsat(embedded(), expr.embedded()));
+
+ //:TEST:
+ embeddedManager().cleanUp();
+ return result;
+ }
+
+ public QueryResult checkContinue() throws Cvc3Exception {
+ embeddedManager().cleanUp();
+ QueryResult result = QueryResult.get(jniCheckContinue(embedded()));
+
+ //:TEST:
+ embeddedManager().cleanUp();
+ return result;
+ }
+
+ public QueryResult restart(Expr expr) throws Cvc3Exception {
+ embeddedManager().cleanUp();
+ QueryResult result = QueryResult.get(jniRestart(embedded(), expr.embedded()));
+
+ //:TEST:
+ embeddedManager().cleanUp();
+ return result;
+ }
+
+ public void returnFromCheck() throws Cvc3Exception {
+ jniReturnFromCheck(embedded());
+
+ //:TEST:
+ embeddedManager().cleanUp();
+ }
+
+ public List getUserAssumptions() throws Cvc3Exception {
+ Object[] assumptions = jniGetUserAssumptions(embedded());
+ return JniUtils.embedList(assumptions, ExprMut.class, embeddedManager());
+ }
+
+ public List getInternalAssumptions() throws Cvc3Exception {
+ Object[] assumptions = jniGetInternalAssumptions(embedded());
+ return JniUtils.embedList(assumptions, ExprMut.class, embeddedManager());
+ }
+
+ public List getAssumptions() throws Cvc3Exception {
+ Object[] assumptions = jniGetAssumptions(embedded());
+ return JniUtils.embedList(assumptions, ExprMut.class, embeddedManager());
+ }
+
+ public List getAssumptionsUsed() throws Cvc3Exception {
+ Object[] assumptions = jniGetAssumptionsUsed(embedded());
+ return JniUtils.embedList(assumptions, ExprMut.class, embeddedManager());
+ }
+
+ public List getCounterExample() throws Cvc3Exception {
+ return getCounterExample(true);
+ }
+
+ public List getCounterExample(boolean inOrder) throws Cvc3Exception {
+ Object[] assumptions = jniGetCounterExample(embedded(), inOrder);
+ return JniUtils.embedList(assumptions, ExprMut.class, embeddedManager());
+ }
+
+ public HashMap getConcreteModel() throws Cvc3Exception {
+ Object[] model = jniGetConcreteModel(embedded());
+ return JniUtils.embedHashMap(model, Expr.class, Expr.class, embeddedManager());
+ }
+
+ public FormulaValue getValue(Expr expr) throws Cvc3Exception {
+ return FormulaValue.get(jniGetValue(embedded(), expr.embedded()));
+ }
+
+ public boolean inconsistent() throws Cvc3Exception {
+ return jniInconsistent1(embedded());
+ }
+
+ // makes only sense if inconsistent is true
+ public List inconsistentReasons() throws Cvc3Exception {
+ Object[] assumptions = jniInconsistent2(embedded());
+ return JniUtils.embedList(assumptions, ExprMut.class, embeddedManager());
+ }
+
+ public boolean incomplete() throws Cvc3Exception {
+ return jniIncomplete1(embedded());
+ }
+
+ // makes only sense if incomplete is true
+ public List incompleteReasons() throws Cvc3Exception {
+ Object[] assumptions = jniIncomplete2(embedded());
+ return JniUtils.embedList(assumptions, String.class, embeddedManager());
+ }
+
+ public ProofMut getProof() throws Cvc3Exception {
+ return new ProofMut(
+ jniGetProof(embedded()),
+ embeddedManager());
+ }
+
+ public ExprMut getTCC() throws Cvc3Exception {
+ return new ExprMut(
+ jniGetTCC(embedded()),
+ embeddedManager());
+ }
+
+ public List getAssumptionsTCC() throws Cvc3Exception {
+ Object[] assumptions = jniGetAssumptionsTCC(embedded());
+ return JniUtils.embedList(assumptions, ExprMut.class, embeddedManager());
+ }
+
+ public ProofMut getProofTCC() throws Cvc3Exception {
+ return new ProofMut(
+ jniGetProofTCC(embedded()),
+ embeddedManager());
+ }
+
+ public ExprMut getClosure() throws Cvc3Exception {
+ return new ExprMut(
+ jniGetClosure(embedded()),
+ embeddedManager());
+ }
+
+ public ProofMut getProofClosure() throws Cvc3Exception {
+ return new ProofMut(
+ jniGetProofClosure(embedded()),
+ embeddedManager());
+ }
+
+
+
+
+ // Context Methods
+
+ public int stackLevel() throws Cvc3Exception {
+ return jniStackLevel(embedded());
+ }
+
+ public void push() throws Cvc3Exception {
+ jniPush(embedded());
+ }
+
+ public void pop() throws Cvc3Exception {
+ jniPop(embedded());
+ //:TEST:
+ embeddedManager().cleanUp();
+ }
+
+ public void popTo(int stackLevel) throws Cvc3Exception {
+ jniPopTo(embedded(), stackLevel);
+ //:TEST:
+ embeddedManager().cleanUp();
+ }
+
+ public int scopeLevel() throws Cvc3Exception {
+ return jniScopeLevel(embedded());
+ }
+
+ public void pushScope() throws Cvc3Exception {
+ jniPushScope(embedded());
+ }
+
+ public void popScope() throws Cvc3Exception {
+ jniPopScope(embedded());
+ }
+
+ public void popToScope(int scopeLevel) throws Cvc3Exception {
+ jniPopToScope(embedded(), scopeLevel);
+ }
+
+ public ContextMut getCurrentContext() throws Cvc3Exception {
+ return new ContextMut(
+ jniGetCurrentContext(embedded()),
+ embeddedManager());
+ }
+
+
+
+
+ // Reading Files
+
+ public void loadFile(String fileName) throws Cvc3Exception {
+ loadFile(fileName, InputLanguage.PRESENTATION);
+ }
+
+ public void loadFile(String fileName, InputLanguage lang) throws Cvc3Exception {
+ jniLoadFile1(embedded(), fileName, lang.toString());
+ }
+
+ // Reporting Statistics
+
+ public void printStatistics() throws Cvc3Exception {
+ jniPrintStatistics(embedded());
+ }
+
+ public StatisticsMut getStatistics() throws Cvc3Exception {
+ return new StatisticsMut(
+ jniGetStatistics(embedded()),
+ embeddedManager());
+ }
+
+ public void setTimeLimit(int limit) throws Cvc3Exception {
+ jniSetTimeLimit(embedded(), limit);
+ }
+}
--- /dev/null
+INCLUDE: <sstream>
+INCLUDE: <theory_arith.h>
+INCLUDE: <theory_array.h>
+
+DEFINITION: Java_cvc3_ValidityChecker_jniCreate1
+jobject
+return embed_own<ValidityChecker>(env, VCL::create());
+
+DEFINITION: Java_cvc3_ValidityChecker_jniCreate2
+jobject c CLFlags flags
+return embed_own<ValidityChecker>(env, VCL::create(*flags));
+
+
+
+DEFINITION: Java_cvc3_ValidityChecker_jniCreateFlags
+jobject
+return embed_copy(env, ValidityChecker::createFlags());
+
+DEFINITION: Java_cvc3_ValidityChecker_jniGetFlags
+jobject c ValidityChecker vc
+return embed_mut_ref(env, &vc->getFlags());
+
+
+
+DEFINITION: Java_cvc3_ValidityChecker_jniBoolType
+jobject m ValidityChecker vc
+return embed_copy(env, vc->boolType());
+
+DEFINITION: Java_cvc3_ValidityChecker_jniRealType
+jobject m ValidityChecker vc
+return embed_copy(env, vc->realType());
+
+DEFINITION: Java_cvc3_ValidityChecker_jniIntType
+jobject m ValidityChecker vc
+return embed_copy(env, vc->intType());
+
+DEFINITION: Java_cvc3_ValidityChecker_jniSubrangeType
+jobject m ValidityChecker vc c Expr l c Expr r
+return embed_copy(env, vc->subrangeType(*l, *r));
+
+DEFINITION: Java_cvc3_ValidityChecker_jniSubtypeType
+jobject m ValidityChecker vc c Expr pred c Expr witness
+return embed_copy(env, vc->subtypeType(*pred, *witness));
+
+DEFINITION: Java_cvc3_ValidityChecker_jniTupleType1
+jobject m ValidityChecker vc c Type type0 c Type type1
+return embed_copy(env, vc->tupleType(*type0, *type1));
+
+DEFINITION: Java_cvc3_ValidityChecker_jniTupleType2
+jobject m ValidityChecker vc c Type type0 c Type type1 c Type type2
+return embed_copy(env, vc->tupleType(*type0, *type1, *type2));
+
+DEFINITION: Java_cvc3_ValidityChecker_jniTupleType3
+jobject m ValidityChecker vc cv Type types
+return embed_copy(env, vc->tupleType(types));
+
+DEFINITION: Java_cvc3_ValidityChecker_jniRecordType1
+jobject m ValidityChecker vc n string field c Type type
+return embed_copy(env, vc->recordType(field, *type));
+
+DEFINITION: Java_cvc3_ValidityChecker_jniRecordType2
+jobject m ValidityChecker vc n string field0 c Type type0 n string field1 c Type type1
+return embed_copy(env, vc->recordType(field0, *type0, field1, *type1));
+
+DEFINITION: Java_cvc3_ValidityChecker_jniRecordType3
+jobject m ValidityChecker vc n string field0 c Type type0 n string field1 c Type type1 n string field2 c Type type2
+return embed_copy(env, vc->recordType(field0, *type0, field1, *type1, field2, *type2));
+
+DEFINITION: Java_cvc3_ValidityChecker_jniRecordType4
+jobject m ValidityChecker vc nv string fields cv Type types
+return embed_copy(env, vc->recordType(fields, types));
+
+DEFINITION: Java_cvc3_ValidityChecker_jniDataType1
+jobject m ValidityChecker vc n string name n string constructor nv string selectors cv Expr types
+return embed_copy(env, vc->dataType(name, constructor, selectors, types));
+
+DEFINITION: Java_cvc3_ValidityChecker_jniDataType2
+jobject m ValidityChecker vc n string name nv string constructors nvv string selectors cvv Expr types
+return embed_copy(env, vc->dataType(name, constructors, selectors, types));
+
+DEFINITION: Java_cvc3_ValidityChecker_jniDataType3
+jobjectArray m ValidityChecker vc nv string names nvv string constructors nvvv string selectors cvvv Expr types
+vector<Type> result;
+vc->dataType(names, constructors, selectors, types, result);
+return toJavaVCopy(env, result);
+
+DEFINITION: Java_cvc3_ValidityChecker_jniAnyType
+jobject m ValidityChecker vc
+return embed_copy(env, Type::anyType(vc->getEM()));
+
+DEFINITION: Java_cvc3_ValidityChecker_jniArrayLiteral
+jobject m ValidityChecker vc c Expr indexVar c Expr bodyExpr
+return embed_copy(env, CVC3::arrayLiteral(*indexVar, *bodyExpr));
+
+DEFINITION: Java_cvc3_ValidityChecker_jniArrayType
+jobject m ValidityChecker vc c Type typeIndex c Type typeData
+return embed_copy(env, vc->arrayType(*typeIndex, *typeData));
+
+DEFINITION: Java_cvc3_ValidityChecker_jniBitvecType
+jobject m ValidityChecker vc n int n
+return embed_copy(env, vc->bitvecType(n));
+
+DEFINITION: Java_cvc3_ValidityChecker_jniFunType1
+jobject m ValidityChecker vc c Type typeDom c Type typeRange
+return embed_copy(env, vc->funType(*typeDom, *typeRange));
+
+DEFINITION: Java_cvc3_ValidityChecker_jniFunType2
+jobject m ValidityChecker vc cv Type typeDom c Type typeRange
+return embed_copy(env, vc->funType(typeDom, *typeRange));
+
+DEFINITION: Java_cvc3_ValidityChecker_jniCreateType1
+jobject m ValidityChecker vc n string typeName
+return embed_copy(env, vc->createType(typeName));
+
+DEFINITION: Java_cvc3_ValidityChecker_jniCreateType2
+jobject m ValidityChecker vc n string typeName c Type typeDef
+return embed_copy(env, vc->createType(typeName, *typeDef));
+
+DEFINITION: Java_cvc3_ValidityChecker_jniLookupType
+jobject m ValidityChecker vc n string typeName
+return embed_copy(env, vc->lookupType(typeName));
+
+
+
+DEFINITION: Java_cvc3_ValidityChecker_jniGetExprManager
+jobject m ValidityChecker vc
+return embed_mut_ref(env, vc->getEM());
+
+DEFINITION: Java_cvc3_ValidityChecker_jniNullExpr
+jobject m ValidityChecker vc
+return embed_copy(env, Expr());
+
+DEFINITION: Java_cvc3_ValidityChecker_jniVarExpr1
+jobject m ValidityChecker vc n string name c Type type
+return embed_copy(env, vc->varExpr(name, *type));
+
+DEFINITION: Java_cvc3_ValidityChecker_jniVarExpr2
+jobject m ValidityChecker vc n string name c Type type c Expr def
+return embed_copy(env, vc->varExpr(name, *type, *def));
+
+DEFINITION: Java_cvc3_ValidityChecker_jniBoundVarExpr
+jobject m ValidityChecker vc n string name n string uid c Type type
+return embed_copy(env, vc->boundVarExpr(name, uid, *type));
+
+DEFINITION: Java_cvc3_ValidityChecker_jniLookupVar
+jobject m ValidityChecker vc n string name
+Type* type = new Type;
+jobject result = embed_copy(env, vc->lookupVar(name, type));
+delete type;
+return result;
+
+DEFINITION: Java_cvc3_ValidityChecker_jniLookupOp
+jobject m ValidityChecker vc n string name
+Type* type = new Type;
+jobject result = embed_copy(env, vc->lookupOp(name, type));
+delete type;
+return result;
+
+DEFINITION: Java_cvc3_ValidityChecker_jniGetType
+jobject m ValidityChecker vc c Expr expr
+return embed_copy(env, vc->getType(*expr));
+
+DEFINITION: Java_cvc3_ValidityChecker_jniGetBaseType1
+jobject m ValidityChecker vc c Expr expr
+return embed_copy(env, vc->getBaseType(*expr));
+
+DEFINITION: Java_cvc3_ValidityChecker_jniGetBaseType2
+jobject m ValidityChecker vc c Type type
+return embed_copy(env, vc->getBaseType(*type));
+
+DEFINITION: Java_cvc3_ValidityChecker_jniGetTypePred
+jobject m ValidityChecker vc c Type type c Expr expr
+return embed_copy(env, vc->getTypePred(*type, *expr));
+
+DEFINITION: Java_cvc3_ValidityChecker_jniStringExpr
+jobject m ValidityChecker vc n string str
+return embed_copy(env, vc->stringExpr(str));
+
+DEFINITION: Java_cvc3_ValidityChecker_jniIdExpr
+jobject m ValidityChecker vc n string name
+return embed_copy(env, vc->idExpr(name));
+
+DEFINITION: Java_cvc3_ValidityChecker_jniListExpr1
+jobject m ValidityChecker vc cv Expr kids
+return embed_copy(env, vc->listExpr(kids));
+
+DEFINITION: Java_cvc3_ValidityChecker_jniListExpr2
+jobject m ValidityChecker vc c Expr expr1
+return embed_copy(env, vc->listExpr(*expr1));
+
+DEFINITION: Java_cvc3_ValidityChecker_jniListExpr3
+jobject m ValidityChecker vc c Expr expr1 c Expr expr2
+return embed_copy(env, vc->listExpr(*expr1, *expr2));
+
+DEFINITION: Java_cvc3_ValidityChecker_jniListExpr4
+jobject m ValidityChecker vc c Expr expr1 c Expr expr2 c Expr expr3
+return embed_copy(env, vc->listExpr(*expr1, *expr2, *expr3));
+
+DEFINITION: Java_cvc3_ValidityChecker_jniListExpr5
+jobject m ValidityChecker vc n string op cv Expr kids
+return embed_copy(env, vc->listExpr(op, kids));
+
+DEFINITION: Java_cvc3_ValidityChecker_jniListExpr6
+jobject m ValidityChecker vc n string op c Expr expr1
+return embed_copy(env, vc->listExpr(op, *expr1));
+
+DEFINITION: Java_cvc3_ValidityChecker_jniListExpr7
+jobject m ValidityChecker vc n string op c Expr expr1 c Expr expr2
+return embed_copy(env, vc->listExpr(op, *expr1, *expr2));
+
+DEFINITION: Java_cvc3_ValidityChecker_jniListExpr8
+jobject m ValidityChecker vc n string op c Expr expr1 c Expr expr2 c Expr expr3
+return embed_copy(env, vc->listExpr(op, *expr1, *expr2, *expr3));
+
+
+DEFINITION: Java_cvc3_ValidityChecker_jniPrintExpr
+void m ValidityChecker vc c Expr expr
+vc->printExpr(*expr);
+
+DEFINITION: Java_cvc3_ValidityChecker_jniParseExpr
+jobject m ValidityChecker vc c Expr expr
+return embed_copy(env, vc->parseExpr(*expr));
+
+DEFINITION: Java_cvc3_ValidityChecker_jniParseType
+jobject m ValidityChecker vc c Expr expr
+return embed_copy(env, vc->parseType(*expr));
+
+DEFINITION: Java_cvc3_ValidityChecker_jniImportExpr
+jobject m ValidityChecker vc c Expr expr
+return embed_copy(env, vc->importExpr(*expr));
+
+DEFINITION: Java_cvc3_ValidityChecker_jniImportType
+jobject m ValidityChecker vc c Type type
+return embed_copy(env, vc->importType(*type));
+
+DEFINITION: Java_cvc3_ValidityChecker_jniCmdsFromString
+void m ValidityChecker vc n string s
+vc->cmdsFromString(s);
+
+DEFINITION: Java_cvc3_ValidityChecker_jniExprFromString
+jobject m ValidityChecker vc n string s
+return embed_copy<Expr>(env, vc->exprFromString(s));
+
+DEFINITION: Java_cvc3_ValidityChecker_jniTrueExpr
+jobject m ValidityChecker vc
+return embed_copy<Expr>(env, vc->trueExpr());
+
+DEFINITION: Java_cvc3_ValidityChecker_jniFalseExpr
+jobject m ValidityChecker vc
+return embed_copy<Expr>(env, vc->falseExpr());
+
+DEFINITION: Java_cvc3_ValidityChecker_jniNotExpr
+jobject m ValidityChecker vc c Expr expr
+return embed_copy(env, vc->notExpr(*expr));
+
+DEFINITION: Java_cvc3_ValidityChecker_jniAndExpr1
+jobject m ValidityChecker vc c Expr expr1 c Expr expr2
+return embed_copy(env, vc->andExpr(*expr1, *expr2));
+
+DEFINITION: Java_cvc3_ValidityChecker_jniAndExpr2
+jobject m ValidityChecker vc cv Expr children
+return embed_copy(env, vc->andExpr(children));
+
+DEFINITION: Java_cvc3_ValidityChecker_jniOrExpr1
+jobject m ValidityChecker vc c Expr expr1 c Expr expr2
+return embed_copy(env, vc->orExpr(*expr1, *expr2));
+
+DEFINITION: Java_cvc3_ValidityChecker_jniOrExpr2
+jobject m ValidityChecker vc cv Expr children
+return embed_copy(env, vc->orExpr(children));
+
+DEFINITION: Java_cvc3_ValidityChecker_jniImpliesExpr
+jobject m ValidityChecker vc c Expr expr1 c Expr expr2
+return embed_copy(env, vc->impliesExpr(*expr1, *expr2));
+
+DEFINITION: Java_cvc3_ValidityChecker_jniIffExpr
+jobject m ValidityChecker vc c Expr expr1 c Expr expr2
+return embed_copy(env, vc->iffExpr(*expr1, *expr2));
+
+DEFINITION: Java_cvc3_ValidityChecker_jniEqExpr
+jobject m ValidityChecker vc c Expr expr1 c Expr expr2
+return embed_copy(env, vc->eqExpr(*expr1, *expr2));
+
+DEFINITION: Java_cvc3_ValidityChecker_jniDistinctExpr
+jobject m ValidityChecker vc cv Expr children
+return embed_copy(env, vc->distinctExpr(children));
+
+DEFINITION: Java_cvc3_ValidityChecker_jniIteExpr
+jobject m ValidityChecker vc c Expr expr1 c Expr expr2 c Expr expr3
+return embed_copy(env, vc->iteExpr(*expr1, *expr2, *expr3));
+
+DEFINITION: Java_cvc3_ValidityChecker_jniCreateOp1
+jobject m ValidityChecker vc n string name c Type type
+return embed_copy(env, vc->createOp(name, *type));
+
+DEFINITION: Java_cvc3_ValidityChecker_jniCreateOp2
+jobject m ValidityChecker vc n string name c Type type c Expr expr
+return embed_copy(env, vc->createOp(name, *type, *expr));
+
+DEFINITION: Java_cvc3_ValidityChecker_jniEqOp
+jobject
+return embed_copy<Op>(env, Op(EQ));
+
+DEFINITION: Java_cvc3_ValidityChecker_jniLtOp
+jobject
+return embed_copy<Op>(env, Op(LT));
+
+DEFINITION: Java_cvc3_ValidityChecker_jniLeOp
+jobject
+return embed_copy<Op>(env, Op(LE));
+
+DEFINITION: Java_cvc3_ValidityChecker_jniGtOp
+jobject
+return embed_copy<Op>(env, Op(GT));
+
+DEFINITION: Java_cvc3_ValidityChecker_jniGeOp
+jobject
+return embed_copy<Op>(env, Op(GE));
+
+DEFINITION: Java_cvc3_ValidityChecker_jniPlusOp
+jobject
+return embed_copy<Op>(env, Op(PLUS));
+
+DEFINITION: Java_cvc3_ValidityChecker_jniMinusOp
+jobject
+return embed_copy<Op>(env, Op(MINUS));
+
+DEFINITION: Java_cvc3_ValidityChecker_jniMultOp
+jobject
+return embed_copy<Op>(env, Op(MULT));
+
+DEFINITION: Java_cvc3_ValidityChecker_jniDivideOp
+jobject
+return embed_copy<Op>(env, Op(DIVIDE));
+
+
+DEFINITION: Java_cvc3_ValidityChecker_jniFunExpr1
+jobject m ValidityChecker vc c Op op c Expr expr1
+return embed_copy(env, vc->funExpr(*op, *expr1));
+
+DEFINITION: Java_cvc3_ValidityChecker_jniFunExpr2
+jobject m ValidityChecker vc c Op op c Expr expr1 c Expr expr2
+return embed_copy(env, vc->funExpr(*op, *expr1, *expr2));
+
+DEFINITION: Java_cvc3_ValidityChecker_jniFunExpr3
+jobject m ValidityChecker vc c Op op c Expr expr1 c Expr expr2 c Expr expr3
+return embed_copy(env, vc->funExpr(*op, *expr1, *expr2, *expr3));
+
+DEFINITION: Java_cvc3_ValidityChecker_jniFunExpr4
+jobject m ValidityChecker vc c Op op cv Expr children
+return embed_copy(env, vc->funExpr(*op, children));
+
+DEFINITION: Java_cvc3_ValidityChecker_jniRatExpr1
+jobject m ValidityChecker vc n int n n int d
+return embed_copy(env, vc->ratExpr(n, d));
+
+DEFINITION: Java_cvc3_ValidityChecker_jniRatExpr2
+jobject m ValidityChecker vc n string n n string d n int base
+return embed_copy(env, vc->ratExpr(n, d, base));
+
+DEFINITION: Java_cvc3_ValidityChecker_jniRatExpr3
+jobject m ValidityChecker vc n string n n int base
+return embed_copy(env, vc->ratExpr(n, base));
+
+DEFINITION: Java_cvc3_ValidityChecker_jniUminusExpr
+jobject m ValidityChecker vc c Expr expr
+return embed_copy(env, vc->uminusExpr(*expr));
+
+DEFINITION: Java_cvc3_ValidityChecker_jniPlusExpr1
+jobject m ValidityChecker vc c Expr expr1 c Expr expr2
+return embed_copy(env, vc->plusExpr(*expr1, *expr2));
+
+DEFINITION: Java_cvc3_ValidityChecker_jniPlusExpr2
+jobject m ValidityChecker vc cv Expr kids
+return embed_copy(env, vc->plusExpr(kids));
+
+DEFINITION: Java_cvc3_ValidityChecker_jniMinusExpr
+jobject m ValidityChecker vc c Expr expr1 c Expr expr2
+return embed_copy(env, vc->minusExpr(*expr1, *expr2));
+
+DEFINITION: Java_cvc3_ValidityChecker_jniMultExpr
+jobject m ValidityChecker vc c Expr expr1 c Expr expr2
+return embed_copy(env, vc->multExpr(*expr1, *expr2));
+
+DEFINITION: Java_cvc3_ValidityChecker_jniPowExpr
+jobject m ValidityChecker vc c Expr expr1 c Expr expr2
+return embed_copy(env, vc->powExpr(*expr1, *expr2));
+
+DEFINITION: Java_cvc3_ValidityChecker_jniDivideExpr
+jobject m ValidityChecker vc c Expr expr1 c Expr expr2
+return embed_copy(env, vc->divideExpr(*expr1, *expr2));
+
+DEFINITION: Java_cvc3_ValidityChecker_jniLtExpr
+jobject m ValidityChecker vc c Expr expr1 c Expr expr2
+return embed_copy(env, vc->ltExpr(*expr1, *expr2));
+
+DEFINITION: Java_cvc3_ValidityChecker_jniLeExpr
+jobject m ValidityChecker vc c Expr expr1 c Expr expr2
+return embed_copy(env, vc->leExpr(*expr1, *expr2));
+
+DEFINITION: Java_cvc3_ValidityChecker_jniGtExpr
+jobject m ValidityChecker vc c Expr expr1 c Expr expr2
+return embed_copy(env, vc->gtExpr(*expr1, *expr2));
+
+DEFINITION: Java_cvc3_ValidityChecker_jniGeExpr
+jobject m ValidityChecker vc c Expr expr1 c Expr expr2
+return embed_copy(env, vc->geExpr(*expr1, *expr2));
+
+DEFINITION: Java_cvc3_ValidityChecker_jniRecordExpr1
+jobject m ValidityChecker vc n string field c Expr expr
+return embed_copy(env, vc->recordExpr(field, *expr));
+
+DEFINITION: Java_cvc3_ValidityChecker_jniRecordExpr2
+jobject m ValidityChecker vc n string field1 c Expr expr1 n string field2 c Expr expr2
+return embed_copy(env, vc->recordExpr(field1, *expr1, field2, *expr2));
+
+DEFINITION: Java_cvc3_ValidityChecker_jniRecordExpr3
+jobject m ValidityChecker vc n string field1 c Expr expr1 n string field2 c Expr expr2 n string field3 c Expr expr3
+return embed_copy(env, vc->recordExpr(field1, *expr1, field2, *expr2, field2, *expr2));
+
+DEFINITION: Java_cvc3_ValidityChecker_jniRecordExpr4
+jobject m ValidityChecker vc nv string fields cv Expr exprs
+return embed_copy(env, vc->recordExpr(fields, exprs));
+
+DEFINITION: Java_cvc3_ValidityChecker_jniRecSelectExpr
+jobject m ValidityChecker vc c Expr record n string field
+return embed_copy(env, vc->recSelectExpr(*record, field));
+
+DEFINITION: Java_cvc3_ValidityChecker_jniRecUpdateExpr
+jobject m ValidityChecker vc c Expr record n string field c Expr update
+return embed_copy(env, vc->recUpdateExpr(*record, field, *update));
+
+DEFINITION: Java_cvc3_ValidityChecker_jniReadExpr
+jobject m ValidityChecker vc c Expr array c Expr index
+return embed_copy(env, vc->readExpr(*array, *index));
+
+DEFINITION: Java_cvc3_ValidityChecker_jniWriteExpr
+jobject m ValidityChecker vc c Expr array c Expr index c Expr value
+return embed_copy(env, vc->writeExpr(*array, *index, *value));
+
+DEFINITION: Java_cvc3_ValidityChecker_jniNewBVConstExpr1
+jobject m ValidityChecker vc n string s n int base
+return embed_copy(env, vc->newBVConstExpr(s, jbase));
+
+DEFINITION: Java_cvc3_ValidityChecker_jniNewBVConstExpr2
+jobject m ValidityChecker vc nv bool bits
+return embed_copy(env, vc->newBVConstExpr(bits));
+
+DEFINITION: Java_cvc3_ValidityChecker_jniNewBVConstExpr3
+jobject m ValidityChecker vc c Rational rational n int len
+return embed_copy(env, vc->newBVConstExpr(*rational, len));
+
+DEFINITION: Java_cvc3_ValidityChecker_jniNewConcatExpr1
+jobject m ValidityChecker vc c Expr expr1 c Expr expr2
+return embed_copy(env, vc->newConcatExpr(*expr1, *expr2));
+
+DEFINITION: Java_cvc3_ValidityChecker_jniNewConcatExpr2
+jobject m ValidityChecker vc cv Expr kids
+return embed_copy(env, vc->newConcatExpr(kids));
+
+DEFINITION: Java_cvc3_ValidityChecker_jniNewBVExtractExpr
+jobject m ValidityChecker vc c Expr expr n int hi n int low
+return embed_copy(env, vc->newBVExtractExpr(*expr, hi, low));
+
+DEFINITION: Java_cvc3_ValidityChecker_jniNewBVNegExpr
+jobject m ValidityChecker vc c Expr expr
+return embed_copy(env, vc->newBVNegExpr(*expr));
+
+DEFINITION: Java_cvc3_ValidityChecker_jniNewBVAndExpr1
+jobject m ValidityChecker vc c Expr expr1 c Expr expr2
+return embed_copy(env, vc->newBVAndExpr(*expr1, *expr2));
+
+DEFINITION: Java_cvc3_ValidityChecker_jniNewBVAndExpr2
+jobject m ValidityChecker vc cv Expr kids
+return embed_copy(env, vc->newBVAndExpr(kids));
+
+DEFINITION: Java_cvc3_ValidityChecker_jniNewBVOrExpr1
+jobject m ValidityChecker vc c Expr expr1 c Expr expr2
+return embed_copy(env, vc->newBVOrExpr(*expr1, *expr2));
+
+DEFINITION: Java_cvc3_ValidityChecker_jniNewBVOrExpr2
+jobject m ValidityChecker vc cv Expr kids
+return embed_copy(env, vc->newBVOrExpr(kids));
+
+DEFINITION: Java_cvc3_ValidityChecker_jniNewBVXorExpr1
+jobject m ValidityChecker vc c Expr expr1 c Expr expr2
+return embed_copy(env, vc->newBVXorExpr(*expr1, *expr2));
+
+DEFINITION: Java_cvc3_ValidityChecker_jniNewBVXorExpr2
+jobject m ValidityChecker vc cv Expr kids
+return embed_copy(env, vc->newBVXorExpr(kids));
+
+DEFINITION: Java_cvc3_ValidityChecker_jniNewBVXnorExpr1
+jobject m ValidityChecker vc c Expr expr1 c Expr expr2
+return embed_copy(env, vc->newBVXnorExpr(*expr1, *expr2));
+
+DEFINITION: Java_cvc3_ValidityChecker_jniNewBVXnorExpr2
+jobject m ValidityChecker vc cv Expr kids
+return embed_copy(env, vc->newBVXnorExpr(kids));
+
+DEFINITION: Java_cvc3_ValidityChecker_jniNewBVNandExpr
+jobject m ValidityChecker vc c Expr expr1 c Expr expr2
+return embed_copy(env, vc->newBVNandExpr(*expr1, *expr2));
+
+DEFINITION: Java_cvc3_ValidityChecker_jniNewBVNorExpr
+jobject m ValidityChecker vc c Expr expr1 c Expr expr2
+return embed_copy(env, vc->newBVNorExpr(*expr1, *expr2));
+
+DEFINITION: Java_cvc3_ValidityChecker_jniNewBVLTExpr
+jobject m ValidityChecker vc c Expr expr1 c Expr expr2
+return embed_copy(env, vc->newBVLTExpr(*expr1, *expr2));
+
+DEFINITION: Java_cvc3_ValidityChecker_jniNewBVLEExpr
+jobject m ValidityChecker vc c Expr expr1 c Expr expr2
+return embed_copy(env, vc->newBVLEExpr(*expr1, *expr2));
+
+DEFINITION: Java_cvc3_ValidityChecker_jniNewBVSLTExpr
+jobject m ValidityChecker vc c Expr expr1 c Expr expr2
+return embed_copy(env, vc->newBVSLTExpr(*expr1, *expr2));
+
+DEFINITION: Java_cvc3_ValidityChecker_jniNewBVSLEExpr
+jobject m ValidityChecker vc c Expr expr1 c Expr expr2
+return embed_copy(env, vc->newBVSLEExpr(*expr1, *expr2));
+
+DEFINITION: Java_cvc3_ValidityChecker_jniNewSXExpr
+jobject m ValidityChecker vc c Expr expr n int len
+return embed_copy(env, vc->newSXExpr(*expr, len));
+
+DEFINITION: Java_cvc3_ValidityChecker_jniNewBVUminusExpr
+jobject m ValidityChecker vc c Expr expr
+return embed_copy(env, vc->newBVUminusExpr(*expr));
+
+DEFINITION: Java_cvc3_ValidityChecker_jniNewBVSubExpr
+jobject m ValidityChecker vc c Expr expr1 c Expr expr2
+return embed_copy(env, vc->newBVSubExpr(*expr1, *expr2));
+
+DEFINITION: Java_cvc3_ValidityChecker_jniNewBVPlusExpr
+jobject m ValidityChecker vc n int numbits cv Expr exprs
+return embed_copy(env, vc->newBVPlusExpr(numbits, exprs));
+
+DEFINITION: Java_cvc3_ValidityChecker_jniNewBVMultExpr
+jobject m ValidityChecker vc n int numbits c Expr expr1 c Expr expr2
+return embed_copy(env, vc->newBVMultExpr(numbits, *expr1, *expr2));
+
+DEFINITION: Java_cvc3_ValidityChecker_jniNewBVUDivExpr
+jobject m ValidityChecker vc c Expr expr1 c Expr expr2
+return embed_copy(env, vc->newBVUDivExpr(*expr1, *expr2));
+
+DEFINITION: Java_cvc3_ValidityChecker_jniNewBVURemExpr
+jobject m ValidityChecker vc c Expr expr1 c Expr expr2
+return embed_copy(env, vc->newBVURemExpr(*expr1, *expr2));
+
+DEFINITION: Java_cvc3_ValidityChecker_jniNewBVSDivExpr
+jobject m ValidityChecker vc c Expr expr1 c Expr expr2
+return embed_copy(env, vc->newBVSDivExpr(*expr1, *expr2));
+
+DEFINITION: Java_cvc3_ValidityChecker_jniNewBVSRemExpr
+jobject m ValidityChecker vc c Expr expr1 c Expr expr2
+return embed_copy(env, vc->newBVSRemExpr(*expr1, *expr2));
+
+DEFINITION: Java_cvc3_ValidityChecker_jniNewBVSModExpr
+jobject m ValidityChecker vc c Expr expr1 c Expr expr2
+return embed_copy(env, vc->newBVSModExpr(*expr1, *expr2));
+
+DEFINITION: Java_cvc3_ValidityChecker_jniNewBVSHL
+jobject m ValidityChecker vc c Expr expr1 c Expr expr2
+return embed_copy(env, vc->newBVSHL(*expr1, *expr2));
+
+DEFINITION: Java_cvc3_ValidityChecker_jniNewBVLSHR
+jobject m ValidityChecker vc c Expr expr1 c Expr expr2
+return embed_copy(env, vc->newBVLSHR(*expr1, *expr2));
+
+DEFINITION: Java_cvc3_ValidityChecker_jniNewBVASHR
+jobject m ValidityChecker vc c Expr expr1 c Expr expr2
+return embed_copy(env, vc->newBVASHR(*expr1, *expr2));
+
+DEFINITION: Java_cvc3_ValidityChecker_jniNewFixedLeftShiftExpr
+jobject m ValidityChecker vc c Expr expr n int r
+return embed_copy(env, vc->newFixedLeftShiftExpr(*expr, r));
+
+DEFINITION: Java_cvc3_ValidityChecker_jniNewFixedConstWidthLeftShiftExpr
+jobject m ValidityChecker vc c Expr expr n int r
+return embed_copy(env, vc->newFixedConstWidthLeftShiftExpr(*expr, r));
+
+DEFINITION: Java_cvc3_ValidityChecker_jniNewFixedRightShiftExpr
+jobject m ValidityChecker vc c Expr expr n int r
+return embed_copy(env, vc->newFixedRightShiftExpr(*expr, r));
+
+DEFINITION: Java_cvc3_ValidityChecker_jniComputeBVConst
+jobject m ValidityChecker vc c Expr expr
+return embed_copy(env, vc->computeBVConst(*expr));
+
+DEFINITION: Java_cvc3_ValidityChecker_jniTupleExpr
+jobject m ValidityChecker vc cv Expr exprs
+return embed_copy(env, vc->tupleExpr(exprs));
+
+DEFINITION: Java_cvc3_ValidityChecker_jniTupleSelectExpr
+jobject m ValidityChecker vc c Expr tuple n int index
+return embed_copy(env, vc->tupleSelectExpr(*tuple, index));
+
+DEFINITION: Java_cvc3_ValidityChecker_jniTupleUpdateExpr
+jobject m ValidityChecker vc c Expr tuple n int index c Expr value
+return embed_copy(env, vc->tupleUpdateExpr(*tuple, index, *value));
+
+DEFINITION: Java_cvc3_ValidityChecker_jniDatatypeConsExpr
+jobject m ValidityChecker vc n string constructor cv Expr exprs
+return embed_copy(env, vc->datatypeConsExpr(constructor, exprs));
+
+DEFINITION: Java_cvc3_ValidityChecker_jniDatatypeSelExpr
+jobject m ValidityChecker vc n string selector c Expr expr
+return embed_copy(env, vc->datatypeSelExpr(selector, *expr));
+
+DEFINITION: Java_cvc3_ValidityChecker_jniDatatypeTestExpr
+jobject m ValidityChecker vc n string constructor c Expr expr
+return embed_copy(env, vc->datatypeTestExpr(constructor, *expr));
+
+DEFINITION: Java_cvc3_ValidityChecker_jniForallExpr1
+jobject m ValidityChecker vc cv Expr vars c Expr body
+return embed_copy(env, vc->forallExpr(vars, *body));
+
+DEFINITION: Java_cvc3_ValidityChecker_jniForallExpr2
+jobject m ValidityChecker vc cv Expr vars c Expr body c Expr trigger
+return embed_copy(env, vc->forallExpr(vars, *body, *trigger));
+
+DEFINITION: Java_cvc3_ValidityChecker_jniForallExpr3
+jobject m ValidityChecker vc cv Expr vars c Expr body cv Expr triggers
+return embed_copy(env, vc->forallExpr(vars, *body, triggers));
+
+DEFINITION: Java_cvc3_ValidityChecker_jniForallExpr4
+jobject m ValidityChecker vc cv Expr vars c Expr body cvv Expr triggers
+return embed_copy(env, vc->forallExpr(vars, *body, triggers));
+
+DEFINITION: Java_cvc3_ValidityChecker_jniSetTrigger
+void m ValidityChecker vc c Expr closure c Expr trigger
+vc->setTrigger(*closure, *trigger);
+
+DEFINITION: Java_cvc3_ValidityChecker_jniSetTriggers
+void m ValidityChecker vc c Expr closure cv Expr triggers
+vc->setTriggers(*closure, triggers);
+
+DEFINITION: Java_cvc3_ValidityChecker_jniSetTriggers2
+void m ValidityChecker vc c Expr closure cvv Expr triggers
+vc->setTriggers(*closure, triggers);
+
+DEFINITION: Java_cvc3_ValidityChecker_jniSetMultiTrigger
+void m ValidityChecker vc c Expr closure cv Expr multiTrigger
+vc->setMultiTrigger(*closure, multiTrigger);
+
+DEFINITION: Java_cvc3_ValidityChecker_jniExistsExpr
+jobject m ValidityChecker vc cv Expr vars c Expr body
+return embed_copy(env, vc->existsExpr(vars, *body));
+
+DEFINITION: Java_cvc3_ValidityChecker_jniLambdaExpr
+jobject m ValidityChecker vc cv Expr vars c Expr body
+return embed_copy(env, vc->lambdaExpr(vars, *body));
+
+DEFINITION: Java_cvc3_ValidityChecker_jniTransClosure
+jobject m ValidityChecker vc c Op p
+return embed_copy(env, vc->transClosure(*p));
+
+DEFINITION: Java_cvc3_ValidityChecker_jniSimulateExpr
+jobject m ValidityChecker vc c Expr f c Expr s cv Expr inputs c Expr n
+return embed_copy(env, vc->simulateExpr(*f, *s, inputs, *n));
+
+
+DEFINITION: Java_cvc3_ValidityChecker_jniSetResourceLimit
+void m ValidityChecker vc n int limit
+vc->setResourceLimit(limit);
+
+DEFINITION: Java_cvc3_ValidityChecker_jniAssertFormula
+void m ValidityChecker vc c Expr expr
+vc->assertFormula(*expr);
+
+DEFINITION: Java_cvc3_ValidityChecker_jniRegisterAtom
+void m ValidityChecker vc c Expr expr
+vc->registerAtom(*expr);
+
+DEFINITION: Java_cvc3_ValidityChecker_jniGetImpliedLiteral
+jobject m ValidityChecker vc
+return embed_copy(env, vc->getImpliedLiteral());
+
+DEFINITION: Java_cvc3_ValidityChecker_jniSimplify
+jobject m ValidityChecker vc c Expr expr
+return embed_copy(env, vc->simplify(*expr));
+
+DEFINITION: Java_cvc3_ValidityChecker_jniQuery
+jstring m ValidityChecker vc c Expr expr
+return toJava(env, vc->query(*expr));
+
+DEFINITION: Java_cvc3_ValidityChecker_jniCheckUnsat
+jstring m ValidityChecker vc c Expr expr
+return toJava(env, vc->checkUnsat(*expr));
+
+DEFINITION: Java_cvc3_ValidityChecker_jniCheckContinue
+jstring m ValidityChecker vc
+return toJava(env, vc->checkContinue());
+
+DEFINITION: Java_cvc3_ValidityChecker_jniRestart
+jstring m ValidityChecker vc c Expr expr
+return toJava(env, vc->restart(*expr));
+
+DEFINITION: Java_cvc3_ValidityChecker_jniReturnFromCheck
+void m ValidityChecker vc
+vc->returnFromCheck();
+
+DEFINITION: Java_cvc3_ValidityChecker_jniGetUserAssumptions
+jobjectArray m ValidityChecker vc
+vector<Expr> result;
+vc->getUserAssumptions(result);
+return toJavaVCopy(env, result);
+
+DEFINITION: Java_cvc3_ValidityChecker_jniGetInternalAssumptions
+jobjectArray m ValidityChecker vc
+vector<Expr> result;
+vc->getInternalAssumptions(result);
+return toJavaVCopy(env, result);
+
+DEFINITION: Java_cvc3_ValidityChecker_jniGetAssumptions
+jobjectArray m ValidityChecker vc
+vector<Expr> result;
+vc->getAssumptions(result);
+return toJavaVCopy(env, result);
+
+DEFINITION: Java_cvc3_ValidityChecker_jniGetAssumptionsUsed
+jobjectArray m ValidityChecker vc
+vector<Expr> result;
+vc->getAssumptionsUsed(result);
+return toJavaVCopy(env, result);
+
+DEFINITION: Java_cvc3_ValidityChecker_jniGetCounterExample
+jobjectArray m ValidityChecker vc n bool inOrder
+vector<Expr> result;
+vc->getCounterExample(result, inOrder);
+return toJavaVCopy(env, result);
+
+DEFINITION: Java_cvc3_ValidityChecker_jniGetValue
+jstring m ValidityChecker vc c Expr expr
+return toJava(env, vc->value(*expr));
+
+DEFINITION: Java_cvc3_ValidityChecker_jniGetConcreteModel
+jobjectArray m ValidityChecker vc
+ExprMap<Expr> result;
+vc->getConcreteModel(result);
+return toJavaHCopy(env, result);
+
+DEFINITION: Java_cvc3_ValidityChecker_jniInconsistent1
+jboolean m ValidityChecker vc
+return vc->inconsistent();
+
+DEFINITION: Java_cvc3_ValidityChecker_jniInconsistent2
+jobjectArray m ValidityChecker vc
+vector<Expr> result;
+bool inconsistent = vc->inconsistent(result);
+assert(inconsistent);
+return toJavaVCopy(env, result);
+
+DEFINITION: Java_cvc3_ValidityChecker_jniIncomplete1
+jboolean m ValidityChecker vc
+return vc->incomplete();
+
+DEFINITION: Java_cvc3_ValidityChecker_jniIncomplete2
+jobjectArray m ValidityChecker vc
+vector<std::string> result;
+bool incomplete = vc->incomplete(result);
+assert(incomplete);
+return toJavaVCopy(env, result);
+
+DEFINITION: Java_cvc3_ValidityChecker_jniGetProof
+jobject m ValidityChecker vc
+return embed_copy(env, vc->getProof());
+
+DEFINITION: Java_cvc3_ValidityChecker_jniGetTCC
+jobject m ValidityChecker vc
+return embed_copy(env, vc->getTCC());
+
+DEFINITION: Java_cvc3_ValidityChecker_jniGetAssumptionsTCC
+jobjectArray m ValidityChecker vc
+vector<Expr> result;
+vc->getAssumptionsTCC(result);
+return toJavaVCopy(env, result);
+
+DEFINITION: Java_cvc3_ValidityChecker_jniGetProofTCC
+jobject m ValidityChecker vc
+return embed_copy(env, vc->getProofTCC());
+
+DEFINITION: Java_cvc3_ValidityChecker_jniGetClosure
+jobject m ValidityChecker vc
+return embed_copy(env, vc->getClosure());
+
+DEFINITION: Java_cvc3_ValidityChecker_jniGetProofClosure
+jobject m ValidityChecker vc
+return embed_copy(env, vc->getProofClosure());
+
+
+
+
+
+
+DEFINITION: Java_cvc3_ValidityChecker_jniStackLevel
+jint m ValidityChecker vc
+return vc->stackLevel();
+
+DEFINITION: Java_cvc3_ValidityChecker_jniPush
+void m ValidityChecker vc
+vc->push();
+
+DEFINITION: Java_cvc3_ValidityChecker_jniPop
+void m ValidityChecker vc
+vc->pop();
+
+DEFINITION: Java_cvc3_ValidityChecker_jniPopTo
+void m ValidityChecker vc n int stackLevel
+vc->popto(stackLevel);
+
+DEFINITION: Java_cvc3_ValidityChecker_jniScopeLevel
+jint m ValidityChecker vc
+return vc->scopeLevel();
+
+DEFINITION: Java_cvc3_ValidityChecker_jniPushScope
+void m ValidityChecker vc
+vc->pushScope();
+
+DEFINITION: Java_cvc3_ValidityChecker_jniPopScope
+void m ValidityChecker vc
+vc->popScope();
+
+DEFINITION: Java_cvc3_ValidityChecker_jniPopToScope
+void m ValidityChecker vc n int stackLevel
+vc->poptoScope(stackLevel);
+
+DEFINITION: Java_cvc3_ValidityChecker_jniGetCurrentContext
+jobject m ValidityChecker vc
+return embed_mut_ref(env, vc->getCurrentContext());
+
+
+
+
+
+DEFINITION: Java_cvc3_ValidityChecker_jniLoadFile1
+void m ValidityChecker vc n string fileName n string lang
+vc->loadFile(fileName, toCppInputLanguage(env, lang), false);
+
+
+DEFINITION: Java_cvc3_ValidityChecker_jniGetStatistics
+jobject m ValidityChecker vc
+return embed_mut_ref(env, &vc->getStatistics());
+
+DEFINITION: Java_cvc3_ValidityChecker_jniPrintStatistics
+void m ValidityChecker vc
+vc->printStatistics();
+
+
+DEFINITION: Java_cvc3_ValidityChecker_jniSetTimeLimit
+void m ValidityChecker vc n int n
+vc->setTimeLimit((unsigned int)n);
projects / cvc5.git / commitdiff