[AS_HELP_STRING([--with-swig=BINARY], [path to swig binary])],
[if test "$withval" = no; then noswig=yes; else SWIG="$withval"; fi])
AC_ARG_ENABLE([language-bindings],
- [AS_HELP_STRING([--enable-language-bindings=][CVC4_SUPPORTED_BINDINGS], [specify language bindings to build])],
- [cvc4_check_for_bindings=no; if test "$enableval" = no; then try_bindings=; else try_bindings="$enableval"; fi],
+ [AS_HELP_STRING([--enable-language-bindings=][CVC4_SUPPORTED_BINDINGS][ | all], [specify language bindings to build])],
+ [if test "$enableval" = yes; then cvc4_check_for_bindings=yes; try_bindings='$1'; else cvc4_check_for_bindings=no; if test "$enableval" = no; then try_bindings=; else try_bindings="$enableval"; fi; fi],
[cvc4_check_for_bindings=yes; try_bindings=])
CVC4_LANGUAGE_BINDINGS=
if test "$noswig" = yes; then
fi
else
AC_MSG_CHECKING([for requested user language bindings])
- if test "$cvc4_check_for_bindings" = yes; then
- try_bindings='$1'
+ if test "$try_bindings" = all; then
+ try_bindings='CVC4_SUPPORTED_BINDINGS'
+ fi
+ try_bindings=$(echo "$try_bindings" | sed 's/,/ /g')
+ if test -z "$try_bindings"; then
+ AC_MSG_RESULT([none])
else
- try_bindings=$(echo "$try_bindings" | sed 's/,/ /g')
+ AC_MSG_RESULT([$try_bindings])
fi
- AC_MSG_RESULT([$try_bindings])
+ cvc4_save_CPPFLAGS="$CPPFLAGS"
+ cvc4_save_CXXFLAGS="$CXXFLAGS"
+ AC_LANG_PUSH([C++])
for binding in $try_bindings; do
binding_error=no
AC_MSG_CHECKING([for availability of $binding binding])
cvc4_build_c_bindings=yes
AC_MSG_RESULT([C support will be built]);;
java)
- cvc4_build_java_bindings=yes
- AC_MSG_RESULT([Java support will be built]);;
+ AC_MSG_RESULT([Java support will be built])
+ AC_ARG_VAR(JAVA_CPPFLAGS, [flags to pass to compiler when building Java bindings])
+ CPPFLAGS="$CPPFLAGS $JAVA_CPPFLAGS"
+ AC_CHECK_HEADER([jni.h], [cvc4_build_java_bindings=yes], [binding_error=yes])
+ ;;
csharp)
- binding_error=yes
- AC_MSG_RESULT([$binding not supported yet]);;
+ cvc4_build_csharp_bindings=yes
+ AC_MSG_RESULT([[C# support will be built]]);;
perl)
- binding_error=yes
- AC_MSG_RESULT([$binding not supported yet]);;
+ AC_MSG_RESULT([perl support will be built])
+ AC_ARG_VAR(PERL_CPPFLAGS, [flags to pass to compiler when building perl bindings])
+ CPPFLAGS="$CPPFLAGS $PERL_CPPFLAGS"
+ AC_CHECK_HEADER([EXTERN.h], [cvc4_build_perl_bindings=yes], [binding_error=yes])
+ ;;
php)
- binding_error=yes
- AC_MSG_RESULT([$binding not supported yet]);;
+ AC_MSG_RESULT([php support will be built])
+ AC_ARG_VAR(PHP_CPPFLAGS, [flags to pass to compiler when building PHP bindings])
+ CPPFLAGS="$CPPFLAGS $PHP_CPPFLAGS"
+ AC_CHECK_HEADER([zend.h], [cvc4_build_php_bindings=yes], [binding_error=yes])
+ ;;
python)
- binding_error=yes
- AC_MSG_RESULT([$binding not supported yet]);;
+ AC_MSG_RESULT([python support will be built])
+ AC_ARG_VAR(PYTHON_CPPFLAGS, [flags to pass to compiler when building Python bindings])
+ CPPFLAGS="$CPPFLAGS $PYTHON_CPPFLAGS"
+ AC_CHECK_HEADER([Python.h], [cvc4_build_python_bindings=yes], [binding_error=yes])
+ ;;
ruby)
- binding_error=yes
- AC_MSG_RESULT([$binding not supported yet]);;
+ AC_MSG_RESULT([ruby support will be built])
+ AC_ARG_VAR(RUBY_CPPFLAGS, [flags to pass to compiler when building ruby bindings])
+ CPPFLAGS="$CPPFLAGS $RUBY_CPPFLAGS"
+ AC_CHECK_HEADER([ruby.h], [cvc4_build_ruby_bindings=yes], [binding_error=yes])
+ ;;
tcl)
- binding_error=yes
- AC_MSG_RESULT([$binding not supported yet]);;
+ cvc4_build_tcl_bindings=yes
+ AC_MSG_RESULT([tcl support will be built]);;
ocaml)
- binding_error=yes
- AC_MSG_RESULT([$binding not supported yet]);;
+ cvc4_build_ocaml_bindings=yes
+ AC_MSG_RESULT([OCaml support will be built]);;
*) AC_MSG_RESULT([unknown binding]); binding_error=yes;;
esac
- if test "$binding_error" = yes -a "$cvc4_check_for_bindings" = no; then
- AC_MSG_ERROR([Language binding \`$binding' requested by user, but it cannot be built.])
+ if test "$binding_error" = yes; then
+ if test "$cvc4_check_for_bindings" = no; then
+ AC_MSG_ERROR([Language binding \`$binding' requested by user, but it cannot be built.])
+ else
+ AC_MSG_WARN([Language binding \`$binding' cannot be built.])
+ fi
+ else
+ CVC4_LANGUAGE_BINDINGS="${CVC4_LANGUAGE_BINDINGS:+$CVC4_LANGUAGE_BINDINGS }$binding"
fi
- CVC4_LANGUAGE_BINDINGS="${CVC4_LANGUAGE_BINDINGS:+$CVC4_LANGUAGE_BINDINGS }$binding"
+ AC_LANG_POP([C++])
+ CXXFLAGS="$cvc4_save_CXXFLAGS"
+ CPPFLAGS="$cvc4_save_CPPFLAGS"
done
fi
fi
# build support. The arg list is the default set if unspecified by
# the user (the actual built set is the subset that appears to be
# supported by the build host).
-CVC4_CHECK_BINDINGS dnl ([java csharp perl php python ruby tcl ocaml])
+CVC4_CHECK_BINDINGS([c java])dnl csharp perl php python ruby tcl ocaml])
# Checks for header files.
AC_CHECK_HEADERS([getopt.h unistd.h])
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
dnl AM_PROG_GCJ
if test -z "$JAVA"; then
public class SimpleVCCompat {
public static void main(String[] args) {
+ //System.loadLibrary("cvc4bindings_java_compat");
+
ValidityChecker vc = ValidityChecker.create();
// Prove that for integers x and y:
-L@builddir@/.. -lcvc4 \
-L@builddir@/../parser -lcvc4parser
endif
-# cvc4bindings_csharp.so \
-# cvc4bindings_perl.so \
-# cvc4bindings_php.so \
-# cvc4bindings_python.so \
-# cvc4bindings_ocaml.so \
-# cvc4bindings_ruby.so \
-# cvc4bindings_tcl.so
+if CVC4_LANGUAGE_BINDING_CSHARP
+lib_LTLIBRARIES += libcvc4bindings_csharp.la
+libcvc4bindings_csharp_la_LDFLAGS = \
+ -version-info $(LIBCVC4BINDINGS_VERSION)
+libcvc4bindings_csharp_la_LIBADD = \
+ -L@builddir@/.. -lcvc4 \
+ -L@builddir@/../parser -lcvc4parser
+endif
+if CVC4_LANGUAGE_BINDING_PERL
+lib_LTLIBRARIES += libcvc4bindings_perl.la
+libcvc4bindings_perl_la_LDFLAGS = \
+ -version-info $(LIBCVC4BINDINGS_VERSION)
+libcvc4bindings_perl_la_LIBADD = \
+ -L@builddir@/.. -lcvc4 \
+ -L@builddir@/../parser -lcvc4parser
+endif
+if CVC4_LANGUAGE_BINDING_PHP
+lib_LTLIBRARIES += libcvc4bindings_php.la
+libcvc4bindings_php_la_LDFLAGS = \
+ -version-info $(LIBCVC4BINDINGS_VERSION)
+libcvc4bindings_php_la_LIBADD = \
+ -L@builddir@/.. -lcvc4 \
+ -L@builddir@/../parser -lcvc4parser
+endif
+if CVC4_LANGUAGE_BINDING_PYTHON
+lib_LTLIBRARIES += libcvc4bindings_python.la
+libcvc4bindings_python_la_LDFLAGS = \
+ -version-info $(LIBCVC4BINDINGS_VERSION)
+libcvc4bindings_python_la_LIBADD = \
+ -L@builddir@/.. -lcvc4 \
+ -L@builddir@/../parser -lcvc4parser
+endif
+if CVC4_LANGUAGE_BINDING_OCAML
+lib_LTLIBRARIES += libcvc4bindings_ocaml.la
+libcvc4bindings_ocaml_la_LDFLAGS = \
+ -version-info $(LIBCVC4BINDINGS_VERSION)
+libcvc4bindings_ocaml_la_LIBADD = \
+ -L@builddir@/.. -lcvc4 \
+ -L@builddir@/../parser -lcvc4parser
+endif
+if CVC4_LANGUAGE_BINDING_RUBY
+lib_LTLIBRARIES += libcvc4bindings_ruby.la
+libcvc4bindings_ruby_la_LDFLAGS = \
+ -version-info $(LIBCVC4BINDINGS_VERSION)
+libcvc4bindings_ruby_la_LIBADD = \
+ -L@builddir@/.. -lcvc4 \
+ -L@builddir@/../parser -lcvc4parser
+endif
+if CVC4_LANGUAGE_BINDING_TCL
+lib_LTLIBRARIES += libcvc4bindings_tcl.la
+libcvc4bindings_tcl_la_LDFLAGS = \
+ -version-info $(LIBCVC4BINDINGS_VERSION)
+libcvc4bindings_tcl_la_LIBADD = \
+ -L@builddir@/.. -lcvc4 \
+ -L@builddir@/../parser -lcvc4parser
+endif
nodist_libcvc4bindings_java_la_SOURCES = java.cpp
libcvc4bindings_java_la_CXXFLAGS = -fno-strict-aliasing
cvc4.jar
java.lo: java.cpp
- $(AM_V_CXX)$(LTCXXCOMPILE) -c $(JAVA_INCLUDES) -o $@ $<
+ $(AM_V_CXX)$(LTCXXCOMPILE) -c $(JAVA_CPPFLAGS) -o $@ $<
cvc4.jar: java.cpp
$(AM_V_GEN) \
(cd java; \
$(JAR) cf $@ -C java/classes .
java.cpp:
csharp.cpp:
+perl.lo: perl.cpp
+ $(AM_V_CXX)$(LTCXXCOMPILE) -c $(PERL_CPPFLAGS) -o $@ $<
perl.cpp:
+php.lo: php.cpp
+ $(AM_V_CXX)$(LTCXXCOMPILE) -c $(PHP_CPPFLAGS) -Iphp -o $@ $<
php.cpp:
+python.lo: python.cpp
+ $(AM_V_CXX)$(LTCXXCOMPILE) -c $(PYTHON_CPPFLAGS) -o $@ $<
python.cpp:
ocaml.cpp:
+python.lo: ruby.cpp
+ $(AM_V_CXX)$(LTCXXCOMPILE) -c $(RUBY_CPPFLAGS) -o $@ $<
ruby.cpp:
tcl.cpp:
-$(patsubst %,%.cpp,$(filter-out c c++,$(CVC4_LANGUAGE_BINDINGS))): %.cpp: @srcdir@/../cvc4.i
+java.cpp: @srcdir@/../cvc4.i
$(AM_V_at)mkdir -p $(patsubst %.cpp,%,$@)
$(AM_V_GEN)$(SWIG) -Wall -I@srcdir@/../include -I@srcdir@/.. -I@builddir@/.. -c++ -$(patsubst %.cpp,%,$@) -outdir $(patsubst %.cpp,%,$@) -package edu.nyu.acsys.CVC4 -o $@ $<
+$(patsubst %,%.cpp,$(filter-out c c++ java,$(CVC4_LANGUAGE_BINDINGS))): %.cpp: @srcdir@/../cvc4.i
+ $(AM_V_at)mkdir -p $(patsubst %.cpp,%,$@)
+ $(AM_V_GEN)$(SWIG) -Wall -I@srcdir@/../include -I@srcdir@/.. -I@builddir@/.. -c++ -$(patsubst %.cpp,%,$@) -outdir $(patsubst %.cpp,%,$@) -o $@ $<
$(patsubst %,%.d,$(filter-out c c++,$(CVC4_LANGUAGE_BINDINGS))): %.d: @srcdir@/../cvc4.i
$(AM_V_GEN)$(SWIG) -I@srcdir@/../include -I@srcdir@/.. -I@builddir@/.. -c++ -MM -o $(patsubst %.d,%.cpp,$@) $<
%template(setType) std::set< CVC4::Type >;
%template(hashmapExpr) std::hash_map< CVC4::Expr, CVC4::Expr, CVC4::ExprHashFunction >;
+// This is unfortunate, but seems to be necessary; if we leave NULL
+// defined, swig will expand it to "(void*) 0", and some of swig's
+// helper functions won't compile properly.
+#undef NULL
+
+#ifdef SWIGJAVA
+
%exception {
try {
$action
}
}
-// This is unfortunate, but seems to be necessary; if we leave NULL
-// defined, swig will expand it to "(void*) 0", and some of swig's
-// helper functions won't compile properly.
-#undef NULL
-
%include "java/typemaps.i" // primitive pointers and references
%include "java/std_string.i" // map std::string to java.lang.String
%include "java/arrays_java.i" // C arrays to Java arrays
%include "java/various.i" // map char** to java.lang.String[]
+#endif /* SWIGJAVA */
+
%include "util/integer.i"
%include "util/rational.i"
%include "util/stats.i"
enum SymbolType;
%ignore operator<<(std::ostream&, DeclarationCheck);
%ignore operator<<(std::ostream&, SymbolType);
+
+ class ParserExprStream : public CVC4::ExprStream {
+ Parser* d_parser;
+ public:
+ ExprStream(Parser* parser) : d_parser(parser) {}
+ ~ExprStream() { delete d_parser; }
+ Expr nextExpr() { return d_parser->nextExpression(); }
+ };/* class Parser::ExprStream */
+
}/* namespace CVC4::parser */
}/* namespace CVC4 */
%include "parser/parser.h"
+
+%{
+namespace CVC4 {
+ namespace parser {
+ typedef CVC4::parser::Parser::ExprStream ParserExprStream;
+ }
+}
+%}
// Fit to size
ps.shrink(i - j);
-
// If we are in solve or decision level > 0
if (minisat_busy || decisionLevel() > 0) {
lemmas.push();
if (ps.size() == 0) {
return ok = false;
} else if (ps.size() == 1) {
- uncheckedEnqueue(ps[0]);
- return ok = (propagate(CHECK_WITHOUTH_PROPAGATION_QUICK) == CRef_Undef);
+ if(assigns[var(ps[0])] == l_Undef) {
+ uncheckedEnqueue(ps[0]);
+ if(assertionLevel > 0) {
+ // remember to unset it on user pop
+ Debug("minisat") << "got new unit " << ps[0] << " at assertion level " << assertionLevel << std::endl;
+ trail_user.push(ps[0]);
+ }
+ return ok = (propagate(CHECK_WITHOUTH_PROPAGATION_QUICK) == CRef_Undef);
+ } else return ok;
} else {
CRef cr = ca.alloc(assertionLevel, ps, false);
clauses_persistent.push(cr);
}
for (int c = trail.size()-1; c >= trail_lim[level]; c--){
Var x = var(trail[c]);
- assigns [x] = l_Undef;
- if (phase_saving > 1 || (phase_saving == 1) && c > trail_lim.last())
+ if(intro_level(x) != -1) {// might be unregistered
+ assigns [x] = l_Undef;
+ vardata[x].trail_index = -1;
+ if (phase_saving > 1 || (phase_saving == 1) && c > trail_lim.last())
polarity[x] = sign(trail[c]);
- insertVarOrder(x);
+ insertVarOrder(x);
+ }
}
qhead = trail_lim[level];
trail.shrink(trail.size() - trail_lim[level]);
Debug("minisat") << "unchecked enqueue of " << p << " (" << trail_index(var(p)) << ") trail size is " << trail.size() << " cap is " << trail.capacity() << std::endl;
assert(value(p) == l_Undef);
assigns[var(p)] = lbool(!sign(p));
- vardata[var(p)] = mkVarData(from, decisionLevel(), intro_level(var(p)), trail.size());
- trail.push_(p);
+ if(trail_index(var(p)) != -1) {
+ // This var is already represented in the trail, presumably from
+ // an earlier incarnation as a unit clause (it has been
+ // unregistered and renewed since then)
+ vardata[var(p)] = mkVarData(from, decisionLevel(), intro_level(var(p)), trail_index(var(p)));
+ trail[trail_index(var(p))] = p;
+ } else {
+ vardata[var(p)] = mkVarData(from, decisionLevel(), intro_level(var(p)), trail.size());
+ trail.push_(p);
+ }
if (theory[var(p)]) {
// Enqueue to the theory
proxy->enqueueTheoryLiteral(p);
ScopedBool scoped_bool(minisat_busy, true);
+ popTrail();
+
model.clear();
conflict.clear();
if (!ok){
{
assert(enable_incremental);
- Debug("minisat") << "in user push, increasing assertion level to " << assertionLevel << std::endl;
+ popTrail();
++assertionLevel;
+ Debug("minisat") << "in user push, increasing assertion level to " << assertionLevel << std::endl;
+ trail_user.push(lit_Undef);
+ trail_ok.push(ok);
}
void Solver::pop()
{
assert(enable_incremental);
+ popTrail();
+
--assertionLevel;
Debug("minisat") << "in user pop, reducing assertion level to " << assertionLevel << " and removing clauses above this from db" << std::endl;
removeClausesAboveLevel(clauses_removable, assertionLevel);
removeClausesAboveLevel(clauses_persistent, assertionLevel);
- // Pop the user trail size
- popTrail();
+ Debug("minisat") << "in user pop, at " << trail_lim.size() << " : " << assertionLevel << std::endl;
+
+ // Unset any units learned or added at this level
+ Debug("minisat") << "in user pop, unsetting level units for level " << assertionLevel << std::endl;
+ while(trail_user.last() != lit_Undef) {
+ Lit l = trail_user.last();
+ Debug("minisat") << "== unassigning " << l << std::endl;
+ Var x = var(l);
+ assigns [x] = l_Undef;
+ if (phase_saving >= 1)
+ polarity[x] = sign(l);
+ insertVarOrder(x);
+ trail_user.pop();
+ }
+ trail_user.pop();
+ ok = trail_ok.last();
+ trail_ok.pop();
+ Debug("minisat") << "in user pop, done unsetting level units" << std::endl;
+
+ Debug("minisat") << "about to removeClausesAboveLevel(" << assertionLevel << ") in CNF" << std::endl;
// Notify the cnf
proxy->removeClausesAboveLevel(assertionLevel);
// }
Debug("minisat::lemmas") << "lemma size is " << lemma.size() << std::endl;
uncheckedEnqueue(lemma[0], lemma_ref);
- if(assertionLevel > 0) {
+ if(lemma.size() == 1 && assertionLevel > 0) {
+ assert(decisionLevel() == 0);
// remember to unset it on user pop
Debug("minisat") << "got new unit (survived downward during updateLemmas()) " << lemma[0] << " at assertion level " << assertionLevel << std::endl;
+ trail_user.push(lemma[0]);
}
}
}
vec<char> decision; // Declares if a variable is eligible for selection in the decision heuristic.
vec<Lit> trail; // Assignment stack; stores all assigments made in the order they were made.
vec<int> trail_lim; // Separator indices for different decision levels in 'trail'.
+ vec<Lit> trail_user; // Stack of assignments to UNdo on user pop.
+ vec<bool> trail_ok; // Stack of "whether we're in conflict" flags.
vec<VarData> vardata; // Stores reason and level for each variable.
int qhead; // Head of queue (as index into the trail -- no more explicit propagation queue in MiniSat).
int simpDB_assigns; // Number of top-level assignments since last execution of 'simplify()'.
, asymm_lits (0)
, eliminated_vars (0)
, elimorder (1)
- , use_simplification (true)
+ , use_simplification (!enableIncremental)
, occurs (ClauseDeleted(ca))
, elim_heap (ElimLt(n_occ))
, bwdsub_assigns (0)
Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
<< "applying substitutions" << endl;
for (unsigned i = 0; i < d_assertionsToPreprocess.size(); ++ i) {
+ Trace("simplify") << "applying to " << d_assertionsToPreprocess[i] << std::endl;
d_assertionsToPreprocess[i] =
theory::Rewriter::rewrite(d_topLevelSubstitutions.apply(d_assertionsToPreprocess[i]));
+ Trace("simplify") << " got " << d_assertionsToPreprocess[i] << std::endl;
}
// Assert all the assertions to the propagator
Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
<< "asserting to propagator" << endl;
for (unsigned i = 0; i < d_assertionsToPreprocess.size(); ++ i) {
+ Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): asserting " << d_assertionsToPreprocess[i] << std::endl;
d_propagator.assert(d_assertionsToPreprocess[i]);
}
// If in conflict, just return false
Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
<< "conflict in non-clausal propagation" << endl;
+ d_assertionsToPreprocess.clear();
d_assertionsToCheck.push_back(NodeManager::currentNM()->mkConst<bool>(false));
return;
} else {
Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
<< "conflict with "
<< d_nonClausalLearnedLiterals[i] << endl;
+ d_assertionsToPreprocess.clear();
d_assertionsToCheck.push_back(NodeManager::currentNM()->mkConst<bool>(false));
return;
}
Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
<< "conflict while solving "
<< learnedLiteral << endl;
+ d_assertionsToPreprocess.clear();
d_assertionsToCheck.push_back(NodeManager::currentNM()->mkConst<bool>(false));
return;
case Theory::SOLVE_STATUS_SOLVED:
namespace CVC4 {
%rename(DatatypeConstructor) CVC4::Datatype::Constructor;
-//%rename(DatatypeConstructor) CVC4::Constructor;
+%rename(DatatypeConstructor) CVC4::Constructor;
}
%extend std::vector< CVC4::Datatype > {
%ignore CVC4::operator<<(std::ostream&, const Datatype::Constructor&);
%ignore CVC4::operator<<(std::ostream&, const Datatype::Constructor::Arg&);
+%feature("valuewrapper") CVC4::Datatype::UnresolvedType;
%include "util/datatype.h"
+
+namespace CVC4 {
+ class CVC4_PUBLIC Arg {
+
+ std::string d_name;
+ Expr d_selector;
+ /** the constructor associated with this selector */
+ Expr d_constructor;
+ bool d_resolved;
+
+ explicit Arg(std::string name, Expr selector);
+ friend class Constructor;
+ friend class Datatype;
+
+ bool isUnresolvedSelf() const throw();
+
+ public:
+
+ /** Get the name of this constructor argument. */
+ std::string getName() const throw();
+
+ /**
+ * Get the selector for this constructor argument; this call is
+ * only permitted after resolution.
+ */
+ Expr getSelector() const;
+
+ /**
+ * Get the associated constructor for this constructor argument;
+ * this call is only permitted after resolution.
+ */
+ Expr getConstructor() const;
+
+ /**
+ * Get the selector for this constructor argument; this call is
+ * only permitted after resolution.
+ */
+ Type getSelectorType() const;
+
+ /**
+ * Get the name of the type of this constructor argument
+ * (Datatype field). Can be used for not-yet-resolved Datatypes
+ * (in which case the name of the unresolved type, or "[self]"
+ * for a self-referential type is returned).
+ */
+ std::string getSelectorTypeName() const;
+
+ /**
+ * Returns true iff this constructor argument has been resolved.
+ */
+ bool isResolved() const throw();
+
+ };/* class Datatype::Constructor::Arg */
+
+ class Constructor {
+ public:
+
+ /** The type for iterators over constructor arguments. */
+ typedef std::vector<Arg>::iterator iterator;
+ /** The (const) type for iterators over constructor arguments. */
+ typedef std::vector<Arg>::const_iterator const_iterator;
+
+ private:
+
+ std::string d_name;
+ Expr d_constructor;
+ Expr d_tester;
+ std::vector<Arg> d_args;
+
+ void resolve(ExprManager* em, DatatypeType self,
+ const std::map<std::string, DatatypeType>& resolutions,
+ const std::vector<Type>& placeholders,
+ const std::vector<Type>& replacements,
+ const std::vector< SortConstructorType >& paramTypes,
+ const std::vector< DatatypeType >& paramReplacements)
+ throw(AssertionException, DatatypeResolutionException);
+ friend class Datatype;
+
+ /** @FIXME document this! */
+ Type doParametricSubstitution(Type range,
+ const std::vector< SortConstructorType >& paramTypes,
+ const std::vector< DatatypeType >& paramReplacements);
+ public:
+ /**
+ * Create a new Datatype constructor with the given name for the
+ * constructor and the given name for the tester. The actual
+ * constructor and tester aren't created until resolution time.
+ */
+ explicit Constructor(std::string name, std::string tester);
+
+ /**
+ * Add an argument (i.e., a data field) of the given name and type
+ * to this Datatype constructor.
+ */
+ void addArg(std::string selectorName, Type selectorType);
+
+ /**
+ * Add an argument (i.e., a data field) of the given name to this
+ * Datatype constructor that refers to an as-yet-unresolved
+ * Datatype (which may be mutually-recursive).
+ */
+ void addArg(std::string selectorName, Datatype::UnresolvedType selectorType);
+
+ /**
+ * Add a self-referential (i.e., a data field) of the given name
+ * to this Datatype constructor that refers to the enclosing
+ * Datatype. For example, using the familiar "nat" Datatype, to
+ * create the "pred" field for "succ" constructor, one uses
+ * succ::addArg("pred", Datatype::SelfType())---the actual Type
+ * cannot be passed because the Datatype is still under
+ * construction.
+ *
+ * This is a special case of
+ * Constructor::addArg(std::string, Datatype::UnresolvedType).
+ */
+ void addArg(std::string selectorName, Datatype::SelfType);
+
+ /** Get the name of this Datatype constructor. */
+ std::string getName() const throw();
+ /**
+ * Get the constructor operator of this Datatype constructor. The
+ * Datatype must be resolved.
+ */
+ Expr getConstructor() const;
+ /**
+ * Get the tester operator of this Datatype constructor. The
+ * Datatype must be resolved.
+ */
+ Expr getTester() const;
+ /**
+ * Get the number of arguments (so far) of this Datatype constructor.
+ */
+ inline size_t getNumArgs() const throw();
+
+ /**
+ * Get the specialized constructor type for a parametric
+ * constructor; this call is only permitted after resolution.
+ */
+ Type getSpecializedConstructorType(Type returnType) const;
+
+ /**
+ * Return the cardinality of this constructor (the product of the
+ * cardinalities of its arguments).
+ */
+ Cardinality getCardinality() const throw(AssertionException);
+
+ /**
+ * Return true iff this constructor is finite (it is nullary or
+ * each of its argument types are finite). This function can
+ * only be called for resolved constructors.
+ */
+ bool isFinite() const throw(AssertionException);
+
+ /**
+ * Return true iff this constructor is well-founded (there exist
+ * ground terms). The constructor must be resolved or an
+ * exception is thrown.
+ */
+ bool isWellFounded() const throw(AssertionException);
+
+ /**
+ * Construct and return a ground term of this constructor. The
+ * constructor must be both resolved and well-founded, or else an
+ * exception is thrown.
+ */
+ Expr mkGroundTerm( Type t ) const throw(AssertionException);
+
+ /**
+ * Returns true iff this Datatype constructor has already been
+ * resolved.
+ */
+ inline bool isResolved() const throw();
+
+ /** Get the beginning iterator over Constructor args. */
+ inline iterator begin() throw();
+ /** Get the ending iterator over Constructor args. */
+ inline iterator end() throw();
+ /** Get the beginning const_iterator over Constructor args. */
+ inline const_iterator begin() const throw();
+ /** Get the ending const_iterator over Constructor args. */
+ inline const_iterator end() const throw();
+
+ /** Get the ith Constructor arg. */
+ const Arg& operator[](size_t index) const;
+
+ };/* class Datatype::Constructor */
+}
+
+ class SelfType {
+ };/* class Datatype::SelfType */
+
+ /**
+ * An unresolved type (used in calls to
+ * Datatype::Constructor::addArg()) to allow a Datatype to refer to
+ * itself or to other mutually-recursive Datatypes. Unresolved-type
+ * fields of Datatypes will be properly typed when a Type is created
+ * for the Datatype by the ExprManager (which calls
+ * Datatype::resolve()).
+ */
+ class UnresolvedType {
+ std::string d_name;
+ public:
+ inline UnresolvedType(std::string name);
+ inline std::string getName() const throw();
+ };/* class Datatype::UnresolvedType */
+
+%{
+namespace CVC4 {
+typedef Datatype::Constructor Constructor;
+typedef Datatype::Constructor::Arg Arg;
+typedef Datatype::SelfType SelfType;
+typedef Datatype::UnresolvedType UnresolvedType;
+}
+%}
+
# put it below in "TESTS +="
# Regression tests for SMT inputs
-CVC_TESTS =
+CVC_TESTS = \
+ test.00.cvc \
+ test.01.cvc \
+ units.cvc
TESTS = $(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(BUG_TESTS)
$(AM_V_CXXLD)$(system_LINK) $(LIBADD) $(AM_LDFLAGS) $+
CVC4JavaTest.class: CVC4JavaTest.java @abs_top_builddir@/src/bindings/cvc4.jar @abs_top_builddir@/src/bindings/libcvc4bindings_java.la
$(AM_V_JAVAC)$(JAVAC) -classpath @abs_top_builddir@/src/bindings/cvc4.jar -d $(builddir) $<
-#CVC4JavaTest: CVC4JavaTest.class
-# $(AM_V_GEN)( \
-# echo "#!/bin/bash"; \
-# echo "exec $(JAVA) -classpath @abs_top_builddir@/src/bindings/cvc4.jar -Djava.library.path=@abs_top_builddir@/src/bindings/.libs CVC4JavaTest"; \
-# ) >$@; \
-# chmod +x $@
# for silent automake rules
AM_V_JAVAC = $(am__v_JAVAC_$(V))
projects / cvc5.git / commitdiff