From c5000befcf95c03a42a2f73a40c3dac6dc3492be Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Mon, 3 Oct 2011 22:07:38 +0000 Subject: [PATCH] user push/pop support in minisat and simplification; also bindings work --- config/bindings.m4 | 79 +++++--- configure.ac | 3 +- examples/SimpleVCCompat.java | 2 + src/bindings/Makefile.am | 78 +++++++- src/cvc4.i | 14 +- src/parser/parser.i | 17 ++ src/prop/minisat/core/Solver.cc | 68 +++++-- src/prop/minisat/core/Solver.h | 2 + src/prop/minisat/simp/SimpSolver.cc | 2 +- src/smt/smt_engine.cpp | 6 + src/util/datatype.i | 218 ++++++++++++++++++++- test/regress/regress0/push-pop/Makefile.am | 5 +- test/system/Makefile.am | 6 - 13 files changed, 438 insertions(+), 62 deletions(-) diff --git a/config/bindings.m4 b/config/bindings.m4 index f47490fec..e328810fb 100644 --- a/config/bindings.m4 +++ b/config/bindings.m4 @@ -21,8 +21,8 @@ AC_ARG_WITH([swig], [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 @@ -44,12 +44,18 @@ else 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]) @@ -60,35 +66,58 @@ else 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 diff --git a/configure.ac b/configure.ac index b2badafbb..930a5685c 100644 --- a/configure.ac +++ b/configure.ac @@ -784,7 +784,7 @@ AC_LIB_ANTLR # 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]) @@ -857,7 +857,6 @@ 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 dnl AM_PROG_GCJ if test -z "$JAVA"; then diff --git a/examples/SimpleVCCompat.java b/examples/SimpleVCCompat.java index 107b5504e..aa28a423b 100644 --- a/examples/SimpleVCCompat.java +++ b/examples/SimpleVCCompat.java @@ -39,6 +39,8 @@ import cvc3.*; 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: 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& 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& 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 decision; // Declares if a variable is eligible for selection in the decision heuristic. vec trail; // Assignment stack; stores all assigments made in the order they were made. vec trail_lim; // Separator indices for different decision levels in 'trail'. + vec trail_user; // Stack of assignments to UNdo on user pop. + vec trail_ok; // Stack of "whether we're in conflict" flags. vec 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(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(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(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::iterator iterator; + /** The (const) type for iterators over constructor arguments. */ + typedef std::vector::const_iterator const_iterator; + + private: + + std::string d_name; + Expr d_constructor; + Expr d_tester; + std::vector d_args; + + void resolve(ExprManager* em, DatatypeType self, + const std::map& resolutions, + const std::vector& placeholders, + const std::vector& 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; +} +%} + diff --git a/test/regress/regress0/push-pop/Makefile.am b/test/regress/regress0/push-pop/Makefile.am index 85c3cb9c9..86eeae902 100644 --- a/test/regress/regress0/push-pop/Makefile.am +++ b/test/regress/regress0/push-pop/Makefile.am @@ -8,7 +8,10 @@ MAKEFLAGS = -k # 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) diff --git a/test/system/Makefile.am b/test/system/Makefile.am index cc0d63aee..6f8094410 100644 --- a/test/system/Makefile.am +++ b/test/system/Makefile.am @@ -71,12 +71,6 @@ cvc3_main: cvc3_george.lo $(LIBADD) $(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)) -- 2.30.2