diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/bindings/Makefile.am | 78 | ||||
| -rw-r--r-- | src/cvc4.i | 14 | ||||
| -rw-r--r-- | src/parser/parser.i | 17 | ||||
| -rw-r--r-- | src/prop/minisat/core/Solver.cc | 68 | ||||
| -rw-r--r-- | src/prop/minisat/core/Solver.h | 2 | ||||
| -rw-r--r-- | src/prop/minisat/simp/SimpSolver.cc | 2 | ||||
| -rw-r--r-- | src/smt/smt_engine.cpp | 6 | ||||
| -rw-r--r-- | src/util/datatype.i | 218 |
8 files changed, 377 insertions, 28 deletions
diff --git a/src/bindings/Makefile.am b/src/bindings/Makefile.am index f9420dbdb..e35ec5e67 100644 --- a/src/bindings/Makefile.am +++ b/src/bindings/Makefile.am @@ -30,13 +30,62 @@ libcvc4bindings_java_la_LIBADD = \ -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 @@ -66,7 +115,7 @@ MOSTLYCLEANFILES = \ 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; \ @@ -77,15 +126,26 @@ cvc4.jar: java.cpp $(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,$@) $< diff --git a/src/cvc4.i b/src/cvc4.i index 7f7926bfd..0e2f48dba 100644 --- a/src/cvc4.i +++ b/src/cvc4.i @@ -40,6 +40,13 @@ using namespace CVC4; %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 @@ -50,16 +57,13 @@ using namespace CVC4; } } -// 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" diff --git a/src/parser/parser.i b/src/parser/parser.i index 55119be9a..dd52bfcda 100644 --- a/src/parser/parser.i +++ b/src/parser/parser.i @@ -8,7 +8,24 @@ namespace CVC4 { 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; + } +} +%} diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc index 7b5ba9286..c1795a12c 100644 --- a/src/prop/minisat/core/Solver.cc +++ b/src/prop/minisat/core/Solver.cc @@ -221,7 +221,6 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable) // Fit to size ps.shrink(i - j); - // If we are in solve or decision level > 0 if (minisat_busy || decisionLevel() > 0) { lemmas.push(); @@ -232,8 +231,15 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable) 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); @@ -307,10 +313,13 @@ void Solver::cancelUntil(int level) { } 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]); @@ -581,8 +590,16 @@ void Solver::uncheckedEnqueue(Lit p, CRef from) 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); @@ -1050,6 +1067,8 @@ lbool Solver::solve_() ScopedBool scoped_bool(minisat_busy, true); + popTrail(); + model.clear(); conflict.clear(); if (!ok){ @@ -1231,14 +1250,19 @@ void Solver::push() { 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; @@ -1247,8 +1271,26 @@ void Solver::pop() 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); @@ -1357,9 +1399,11 @@ CRef Solver::updateLemmas() { // } 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]); } } } diff --git a/src/prop/minisat/core/Solver.h b/src/prop/minisat/core/Solver.h index 345a00e52..c5220997b 100644 --- a/src/prop/minisat/core/Solver.h +++ b/src/prop/minisat/core/Solver.h @@ -278,6 +278,8 @@ protected: 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()'. diff --git a/src/prop/minisat/simp/SimpSolver.cc b/src/prop/minisat/simp/SimpSolver.cc index f8292c072..8c31dd377 100644 --- a/src/prop/minisat/simp/SimpSolver.cc +++ b/src/prop/minisat/simp/SimpSolver.cc @@ -57,7 +57,7 @@ SimpSolver::SimpSolver(CVC4::prop::SatSolver* proxy, CVC4::context::Context* con , 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) diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 42b21b79a..f80d9a135 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -574,14 +574,17 @@ void SmtEnginePrivate::nonClausalSimplify() { 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]); } @@ -591,6 +594,7 @@ void SmtEnginePrivate::nonClausalSimplify() { // 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 { @@ -610,6 +614,7 @@ void SmtEnginePrivate::nonClausalSimplify() { Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): " << "conflict with " << d_nonClausalLearnedLiterals[i] << endl; + d_assertionsToPreprocess.clear(); d_assertionsToCheck.push_back(NodeManager::currentNM()->mkConst<bool>(false)); return; } @@ -625,6 +630,7 @@ void SmtEnginePrivate::nonClausalSimplify() { 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: diff --git a/src/util/datatype.i b/src/util/datatype.i index f306d7682..b62033e17 100644 --- a/src/util/datatype.i +++ b/src/util/datatype.i @@ -7,7 +7,7 @@ namespace CVC4 { namespace CVC4 { %rename(DatatypeConstructor) CVC4::Datatype::Constructor; -//%rename(DatatypeConstructor) CVC4::Constructor; +%rename(DatatypeConstructor) CVC4::Constructor; } %extend std::vector< CVC4::Datatype > { @@ -37,5 +37,221 @@ namespace CVC4 { %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; +} +%} + |