(no commit message)
authorDejan Jovanović <dejan.jovanovic@gmail.com>
Tue, 9 Mar 2010 05:19:22 +0000 (05:19 +0000)
committerDejan Jovanović <dejan.jovanovic@gmail.com>
Tue, 9 Mar 2010 05:19:22 +0000 (05:19 +0000)
src/prop/minisat/core/Solver.C
src/prop/minisat/simp/SimpSolver.C
src/prop/prop_engine.cpp
test/regress/regress0/Makefile.am
test/regress/regress0/uf/Makefile [new file with mode: 0644]
test/regress/regress0/uf/Makefile.am [new file with mode: 0644]
test/regress/regress0/uf/Makefile.in [new file with mode: 0644]
test/regress/regress0/uf/simple.01.cvc [new file with mode: 0644]
test/regress/regress0/uf/simple.02.cvc [new file with mode: 0644]
test/regress/regress0/uf/simple.03.cvc [new file with mode: 0644]

index 5ad647baa776d263a0727df53dd3442333f69a75..e54884925e163eab03d57750f4268a882981d262 100644 (file)
@@ -141,6 +141,7 @@ void Solver::attachClause(Clause& c) {
 
 
 void Solver::detachClause(Clause& c) {
+    Debug("minisat") << "Solver::detachClause(" << c << ")" << std::endl;
     assert(c.size() > 1);
     assert(find(watches[toInt(~c[0])], &c));
     assert(find(watches[toInt(~c[1])], &c));
@@ -151,8 +152,10 @@ void Solver::detachClause(Clause& c) {
 
 
 void Solver::removeClause(Clause& c) {
+    Debug("minisat") << "Solver::removeClause(" << c << ")" << std::endl;
     detachClause(c);
-    free(&c); }
+    free(&c);
+}
 
 
 bool Solver::satisfied(const Clause& c) const {
@@ -440,8 +443,8 @@ Clause* Solver::propagateTheory()
   SatClause clause;
   proxy->theoryCheck(clause);
   if (clause.size() > 0) {
-    Clause* c = Clause_new(clause, false);
-    clauses.push(c);
+    c = Clause_new(clause, true);
+    learnts.push(c);
     attachClause(*c);
   }
   return c;
index a2e46e2e4ae72d119295ac6850d512c3616e094f..057dfdbe291b21627d6d23399c6bbcce112a2e4f 100644 (file)
@@ -65,7 +65,7 @@ Var SimpSolver::newVar(bool sign, bool dvar, bool theoryAtom) {
         n_occ    .push(0);
         n_occ    .push(0);
         occurs   .push();
-        frozen   .push((char)false);
+        frozen   .push((char)theoryAtom);
         touched  .push(0);
         elim_heap.insert(v);
         elimtable.push();
@@ -156,6 +156,7 @@ bool SimpSolver::addClause(vec<Lit>& ps)
 
 void SimpSolver::removeClause(Clause& c)
 {
+    Debug("minisat") << "SimpSolver::removeClause(" << c << ")" << std::endl;
     assert(!c.learnt());
 
     if (use_simplification)
index 96154063d573c470eea3112a86ca66dd3bd81cbf..ef28a4ac6a68d4ab0d5d15db19d85085950dcadd 100644 (file)
@@ -66,14 +66,14 @@ void PropEngine::assertLemma(TNode node) {
 
 Result PropEngine::checkSat() {
   Assert(!d_inCheckSat, "Sat solver in solve()!");
-  Debug("prop") << "solve()" << endl;
+  Debug("prop") << "PropEngine::checkSat()" << endl;
   // Mark that we are in the checkSat
   d_inCheckSat = true;
   // Check the problem
   bool result = d_satSolver->solve();
   // Not in checkSat any more
   d_inCheckSat = false;
-  Debug("prop") << "solve() => " << (result ? "true" : "false") << endl;
+  Debug("prop") << "PropEngine::checkSat() => " << (result ? "true" : "false") << endl;
   return Result(result ? Result::SAT : Result::UNSAT);
 }
 
index 987a2dfe2bb1a03265d31d5110b40f18dc9c94cb..a8786b4ff58eb18796009e4e89be7728f077309a 100644 (file)
@@ -1,4 +1,4 @@
-SUBDIRS = precedence
+SUBDIRS = precedence uf
 
 TESTS_ENVIRONMENT = @srcdir@/../run_regression @top_builddir@/../../bin/cvc4
 TESTS =        bug32.cvc \
@@ -11,7 +11,7 @@ TESTS =       bug32.cvc \
        simple2.smt \
        simple.cvc \
        simple.smt \
-  simple-uf.smt \
+       simple-uf.smt \
        smallcnf.cvc \
        test11.cvc \
        test9.cvc \
diff --git a/test/regress/regress0/uf/Makefile b/test/regress/regress0/uf/Makefile
new file mode 100644 (file)
index 0000000..d3d4267
--- /dev/null
@@ -0,0 +1,8 @@
+topdir = ../../../..
+srcdir = test/regress/regress0/uf
+
+include $(topdir)/Makefile.subdir
+
+# synonyms for "check"
+.PHONY: test
+test: check
diff --git a/test/regress/regress0/uf/Makefile.am b/test/regress/regress0/uf/Makefile.am
new file mode 100644 (file)
index 0000000..3fcf179
--- /dev/null
@@ -0,0 +1,12 @@
+TESTS_ENVIRONMENT = @srcdir@/../../run_regression @top_builddir@/../../bin/cvc4
+TESTS =        simple.01.cvc \
+       simple.02.cvc \
+       simple.03.cvc
+
+# synonyms for "check"
+.PHONY: regress regress0 test
+regress regress0 test: check
+
+# do nothing in this subdir
+.PHONY: regress1 regress2 regress3
+regress1 regress2 regress3:
diff --git a/test/regress/regress0/uf/Makefile.in b/test/regress/regress0/uf/Makefile.in
new file mode 100644 (file)
index 0000000..22aeeff
--- /dev/null
@@ -0,0 +1,520 @@
+# Makefile.in generated by automake 1.11 from Makefile.am.
+# @configure_input@
+
+# Copyright (C) 1994, 1995, 1996, 1997, 1998, 1999, 2000, 2001, 2002,
+# 2003, 2004, 2005, 2006, 2007, 2008, 2009  Free Software Foundation,
+# Inc.
+# This Makefile.in is free software; the Free Software Foundation
+# gives unlimited permission to copy and/or distribute it,
+# with or without modifications, as long as this notice is preserved.
+
+# This program is distributed in the hope that it will be useful,
+# but WITHOUT ANY WARRANTY, to the extent permitted by law; without
+# even the implied warranty of MERCHANTABILITY or FITNESS FOR A
+# PARTICULAR PURPOSE.
+
+@SET_MAKE@
+VPATH = @srcdir@
+pkgdatadir = $(datadir)/@PACKAGE@
+pkgincludedir = $(includedir)/@PACKAGE@
+pkglibdir = $(libdir)/@PACKAGE@
+pkglibexecdir = $(libexecdir)/@PACKAGE@
+am__cd = CDPATH="$${ZSH_VERSION+.}$(PATH_SEPARATOR)" && cd
+install_sh_DATA = $(install_sh) -c -m 644
+install_sh_PROGRAM = $(install_sh) -c
+install_sh_SCRIPT = $(install_sh) -c
+INSTALL_HEADER = $(INSTALL_DATA)
+transform = $(program_transform_name)
+NORMAL_INSTALL = :
+PRE_INSTALL = :
+POST_INSTALL = :
+NORMAL_UNINSTALL = :
+PRE_UNINSTALL = :
+POST_UNINSTALL = :
+build_triplet = @build@
+host_triplet = @host@
+target_triplet = @target@
+subdir = test/regress/regress0/uf
+DIST_COMMON = $(srcdir)/Makefile.am $(srcdir)/Makefile.in
+ACLOCAL_M4 = $(top_srcdir)/aclocal.m4
+am__aclocal_m4_deps = $(top_srcdir)/config/antlr.m4 \
+       $(top_srcdir)/config/ax_prog_doxygen.m4 \
+       $(top_srcdir)/config/cvc4.m4 $(top_srcdir)/config/libtool.m4 \
+       $(top_srcdir)/config/ltoptions.m4 \
+       $(top_srcdir)/config/ltsugar.m4 \
+       $(top_srcdir)/config/ltversion.m4 \
+       $(top_srcdir)/config/lt~obsolete.m4 $(top_srcdir)/configure.ac
+am__configure_deps = $(am__aclocal_m4_deps) $(CONFIGURE_DEPENDENCIES) \
+       $(ACLOCAL_M4)
+mkinstalldirs = $(install_sh) -d
+CONFIG_HEADER = $(top_builddir)/config.h
+CONFIG_CLEAN_FILES =
+CONFIG_CLEAN_VPATH_FILES =
+AM_V_GEN = $(am__v_GEN_$(V))
+am__v_GEN_ = $(am__v_GEN_$(AM_DEFAULT_VERBOSITY))
+am__v_GEN_0 = @echo "  GEN   " $@;
+AM_V_at = $(am__v_at_$(V))
+am__v_at_ = $(am__v_at_$(AM_DEFAULT_VERBOSITY))
+am__v_at_0 = @
+SOURCES =
+DIST_SOURCES =
+am__tty_colors = \
+red=; grn=; lgn=; blu=; std=
+DISTFILES = $(DIST_COMMON) $(DIST_SOURCES) $(TEXINFOS) $(EXTRA_DIST)
+ACLOCAL = @ACLOCAL@
+AMTAR = @AMTAR@
+AM_DEFAULT_VERBOSITY = @AM_DEFAULT_VERBOSITY@
+ANTLR = @ANTLR@
+ANTLR_INCLUDES = @ANTLR_INCLUDES@
+ANTLR_LDFLAGS = @ANTLR_LDFLAGS@
+AR = @AR@
+AS = @AS@
+AUTOCONF = @AUTOCONF@
+AUTOHEADER = @AUTOHEADER@
+AUTOMAKE = @AUTOMAKE@
+AWK = @AWK@
+BUILDING_SHARED = @BUILDING_SHARED@
+BUILDING_STATIC = @BUILDING_STATIC@
+CC = @CC@
+CCDEPMODE = @CCDEPMODE@
+CFLAGS = @CFLAGS@
+CPP = @CPP@
+CPPFLAGS = @CPPFLAGS@
+CVC4_LIBRARY_VERSION = @CVC4_LIBRARY_VERSION@
+CVC4_PARSER_LIBRARY_VERSION = @CVC4_PARSER_LIBRARY_VERSION@
+CXX = @CXX@
+CXXCPP = @CXXCPP@
+CXXDEPMODE = @CXXDEPMODE@
+CXXFLAGS = @CXXFLAGS@
+CXXTEST = @CXXTEST@
+CXXTESTGEN = @CXXTESTGEN@
+CYGPATH_W = @CYGPATH_W@
+DEFS = @DEFS@
+DEPDIR = @DEPDIR@
+DLLTOOL = @DLLTOOL@
+DOXYGEN_PAPER_SIZE = @DOXYGEN_PAPER_SIZE@
+DSYMUTIL = @DSYMUTIL@
+DUMPBIN = @DUMPBIN@
+DX_CONFIG = @DX_CONFIG@
+DX_DOCDIR = @DX_DOCDIR@
+DX_DOT = @DX_DOT@
+DX_DOXYGEN = @DX_DOXYGEN@
+DX_DVIPS = @DX_DVIPS@
+DX_EGREP = @DX_EGREP@
+DX_ENV = @DX_ENV@
+DX_FLAG_DX_CURRENT_FEATURE = @DX_FLAG_DX_CURRENT_FEATURE@
+DX_FLAG_chi = @DX_FLAG_chi@
+DX_FLAG_chm = @DX_FLAG_chm@
+DX_FLAG_doc = @DX_FLAG_doc@
+DX_FLAG_dot = @DX_FLAG_dot@
+DX_FLAG_html = @DX_FLAG_html@
+DX_FLAG_man = @DX_FLAG_man@
+DX_FLAG_pdf = @DX_FLAG_pdf@
+DX_FLAG_ps = @DX_FLAG_ps@
+DX_FLAG_rtf = @DX_FLAG_rtf@
+DX_FLAG_xml = @DX_FLAG_xml@
+DX_HHC = @DX_HHC@
+DX_LATEX = @DX_LATEX@
+DX_MAKEINDEX = @DX_MAKEINDEX@
+DX_PDFLATEX = @DX_PDFLATEX@
+DX_PERL = @DX_PERL@
+DX_PROJECT = @DX_PROJECT@
+ECHO_C = @ECHO_C@
+ECHO_N = @ECHO_N@
+ECHO_T = @ECHO_T@
+EGREP = @EGREP@
+EXEEXT = @EXEEXT@
+FGREP = @FGREP@
+GREP = @GREP@
+INSTALL = @INSTALL@
+INSTALL_DATA = @INSTALL_DATA@
+INSTALL_PROGRAM = @INSTALL_PROGRAM@
+INSTALL_SCRIPT = @INSTALL_SCRIPT@
+INSTALL_STRIP_PROGRAM = @INSTALL_STRIP_PROGRAM@
+LD = @LD@
+LDFLAGS = @LDFLAGS@
+LIBOBJS = @LIBOBJS@
+LIBS = @LIBS@
+LIBTOOL = @LIBTOOL@
+LIPO = @LIPO@
+LN_S = @LN_S@
+LTLIBOBJS = @LTLIBOBJS@
+MAKEINFO = @MAKEINFO@
+MKDIR_P = @MKDIR_P@
+NM = @NM@
+NMEDIT = @NMEDIT@
+OBJDUMP = @OBJDUMP@
+OBJEXT = @OBJEXT@
+OTOOL = @OTOOL@
+OTOOL64 = @OTOOL64@
+PACKAGE = @PACKAGE@
+PACKAGE_BUGREPORT = @PACKAGE_BUGREPORT@
+PACKAGE_NAME = @PACKAGE_NAME@
+PACKAGE_STRING = @PACKAGE_STRING@
+PACKAGE_TARNAME = @PACKAGE_TARNAME@
+PACKAGE_URL = @PACKAGE_URL@
+PACKAGE_VERSION = @PACKAGE_VERSION@
+PATH_SEPARATOR = @PATH_SEPARATOR@
+PERL = @PERL@
+RANLIB = @RANLIB@
+SED = @SED@
+SET_MAKE = @SET_MAKE@
+SHELL = @SHELL@
+STRIP = @STRIP@
+TEST_CPPFLAGS = @TEST_CPPFLAGS@
+TEST_CXXFLAGS = @TEST_CXXFLAGS@
+TEST_LDFLAGS = @TEST_LDFLAGS@
+VERSION = @VERSION@
+abs_builddir = @abs_builddir@
+abs_srcdir = @abs_srcdir@
+abs_top_builddir = @abs_top_builddir@
+abs_top_srcdir = @abs_top_srcdir@
+ac_ct_CC = @ac_ct_CC@
+ac_ct_CXX = @ac_ct_CXX@
+ac_ct_DUMPBIN = @ac_ct_DUMPBIN@
+am__include = @am__include@
+am__leading_dot = @am__leading_dot@
+am__quote = @am__quote@
+am__tar = @am__tar@
+am__untar = @am__untar@
+bindir = @bindir@
+build = @build@
+build_alias = @build_alias@
+build_cpu = @build_cpu@
+build_os = @build_os@
+build_vendor = @build_vendor@
+builddir = @builddir@
+datadir = @datadir@
+datarootdir = @datarootdir@
+docdir = @docdir@
+dvidir = @dvidir@
+exec_prefix = @exec_prefix@
+host = @host@
+host_alias = @host_alias@
+host_cpu = @host_cpu@
+host_os = @host_os@
+host_vendor = @host_vendor@
+htmldir = @htmldir@
+includedir = @includedir@
+infodir = @infodir@
+install_sh = @install_sh@
+libdir = @libdir@
+libexecdir = @libexecdir@
+localedir = @localedir@
+localstatedir = @localstatedir@
+lt_ECHO = @lt_ECHO@
+mandir = @mandir@
+mk_include = @mk_include@
+mkdir_p = @mkdir_p@
+oldincludedir = @oldincludedir@
+pdfdir = @pdfdir@
+prefix = @prefix@
+program_transform_name = @program_transform_name@
+psdir = @psdir@
+sbindir = @sbindir@
+sharedstatedir = @sharedstatedir@
+srcdir = @srcdir@
+sysconfdir = @sysconfdir@
+target = @target@
+target_alias = @target_alias@
+target_cpu = @target_cpu@
+target_os = @target_os@
+target_vendor = @target_vendor@
+top_build_prefix = @top_build_prefix@
+top_builddir = @top_builddir@
+top_srcdir = @top_srcdir@
+TESTS_ENVIRONMENT = @srcdir@/../../run_regression @top_builddir@/../../bin/cvc4
+TESTS = simple.01.cvc \
+       simple.02.cvc \
+       simple.03.cvc
+
+all: all-am
+
+.SUFFIXES:
+$(srcdir)/Makefile.in:  $(srcdir)/Makefile.am  $(am__configure_deps)
+       @for dep in $?; do \
+         case '$(am__configure_deps)' in \
+           *$$dep*) \
+             ( cd $(top_builddir) && $(MAKE) $(AM_MAKEFLAGS) am--refresh ) \
+               && { if test -f $@; then exit 0; else break; fi; }; \
+             exit 1;; \
+         esac; \
+       done; \
+       echo ' cd $(top_srcdir) && $(AUTOMAKE) --gnu test/regress/regress0/uf/Makefile'; \
+       $(am__cd) $(top_srcdir) && \
+         $(AUTOMAKE) --gnu test/regress/regress0/uf/Makefile
+.PRECIOUS: Makefile
+Makefile: $(srcdir)/Makefile.in $(top_builddir)/config.status
+       @case '$?' in \
+         *config.status*) \
+           cd $(top_builddir) && $(MAKE) $(AM_MAKEFLAGS) am--refresh;; \
+         *) \
+           echo ' cd $(top_builddir) && $(SHELL) ./config.status $(subdir)/$@ $(am__depfiles_maybe)'; \
+           cd $(top_builddir) && $(SHELL) ./config.status $(subdir)/$@ $(am__depfiles_maybe);; \
+       esac;
+
+$(top_builddir)/config.status: $(top_srcdir)/configure $(CONFIG_STATUS_DEPENDENCIES)
+       cd $(top_builddir) && $(MAKE) $(AM_MAKEFLAGS) am--refresh
+
+$(top_srcdir)/configure:  $(am__configure_deps)
+       cd $(top_builddir) && $(MAKE) $(AM_MAKEFLAGS) am--refresh
+$(ACLOCAL_M4):  $(am__aclocal_m4_deps)
+       cd $(top_builddir) && $(MAKE) $(AM_MAKEFLAGS) am--refresh
+$(am__aclocal_m4_deps):
+
+mostlyclean-libtool:
+       -rm -f *.lo
+
+clean-libtool:
+       -rm -rf .libs _libs
+tags: TAGS
+TAGS:
+
+ctags: CTAGS
+CTAGS:
+
+
+check-TESTS: $(TESTS)
+       @failed=0; all=0; xfail=0; xpass=0; skip=0; \
+       srcdir=$(srcdir); export srcdir; \
+       list=' $(TESTS) '; \
+       $(am__tty_colors); \
+       if test -n "$$list"; then \
+         for tst in $$list; do \
+           if test -f ./$$tst; then dir=./; \
+           elif test -f $$tst; then dir=; \
+           else dir="$(srcdir)/"; fi; \
+           if $(TESTS_ENVIRONMENT) $${dir}$$tst; then \
+             all=`expr $$all + 1`; \
+             case " $(XFAIL_TESTS) " in \
+             *[\ \     ]$$tst[\ \      ]*) \
+               xpass=`expr $$xpass + 1`; \
+               failed=`expr $$failed + 1`; \
+               col=$$red; res=XPASS; \
+             ;; \
+             *) \
+               col=$$grn; res=PASS; \
+             ;; \
+             esac; \
+           elif test $$? -ne 77; then \
+             all=`expr $$all + 1`; \
+             case " $(XFAIL_TESTS) " in \
+             *[\ \     ]$$tst[\ \      ]*) \
+               xfail=`expr $$xfail + 1`; \
+               col=$$lgn; res=XFAIL; \
+             ;; \
+             *) \
+               failed=`expr $$failed + 1`; \
+               col=$$red; res=FAIL; \
+             ;; \
+             esac; \
+           else \
+             skip=`expr $$skip + 1`; \
+             col=$$blu; res=SKIP; \
+           fi; \
+           echo "$${col}$$res$${std}: $$tst"; \
+         done; \
+         if test "$$all" -eq 1; then \
+           tests="test"; \
+           All=""; \
+         else \
+           tests="tests"; \
+           All="All "; \
+         fi; \
+         if test "$$failed" -eq 0; then \
+           if test "$$xfail" -eq 0; then \
+             banner="$$All$$all $$tests passed"; \
+           else \
+             if test "$$xfail" -eq 1; then failures=failure; else failures=failures; fi; \
+             banner="$$All$$all $$tests behaved as expected ($$xfail expected $$failures)"; \
+           fi; \
+         else \
+           if test "$$xpass" -eq 0; then \
+             banner="$$failed of $$all $$tests failed"; \
+           else \
+             if test "$$xpass" -eq 1; then passes=pass; else passes=passes; fi; \
+             banner="$$failed of $$all $$tests did not behave as expected ($$xpass unexpected $$passes)"; \
+           fi; \
+         fi; \
+         dashes="$$banner"; \
+         skipped=""; \
+         if test "$$skip" -ne 0; then \
+           if test "$$skip" -eq 1; then \
+             skipped="($$skip test was not run)"; \
+           else \
+             skipped="($$skip tests were not run)"; \
+           fi; \
+           test `echo "$$skipped" | wc -c` -le `echo "$$banner" | wc -c` || \
+             dashes="$$skipped"; \
+         fi; \
+         report=""; \
+         if test "$$failed" -ne 0 && test -n "$(PACKAGE_BUGREPORT)"; then \
+           report="Please report to $(PACKAGE_BUGREPORT)"; \
+           test `echo "$$report" | wc -c` -le `echo "$$banner" | wc -c` || \
+             dashes="$$report"; \
+         fi; \
+         dashes=`echo "$$dashes" | sed s/./=/g`; \
+         if test "$$failed" -eq 0; then \
+           echo "$$grn$$dashes"; \
+         else \
+           echo "$$red$$dashes"; \
+         fi; \
+         echo "$$banner"; \
+         test -z "$$skipped" || echo "$$skipped"; \
+         test -z "$$report" || echo "$$report"; \
+         echo "$$dashes$$std"; \
+         test "$$failed" -eq 0; \
+       else :; fi
+
+distdir: $(DISTFILES)
+       @srcdirstrip=`echo "$(srcdir)" | sed 's/[].[^$$\\*]/\\\\&/g'`; \
+       topsrcdirstrip=`echo "$(top_srcdir)" | sed 's/[].[^$$\\*]/\\\\&/g'`; \
+       list='$(DISTFILES)'; \
+         dist_files=`for file in $$list; do echo $$file; done | \
+         sed -e "s|^$$srcdirstrip/||;t" \
+             -e "s|^$$topsrcdirstrip/|$(top_builddir)/|;t"`; \
+       case $$dist_files in \
+         */*) $(MKDIR_P) `echo "$$dist_files" | \
+                          sed '/\//!d;s|^|$(distdir)/|;s,/[^/]*$$,,' | \
+                          sort -u` ;; \
+       esac; \
+       for file in $$dist_files; do \
+         if test -f $$file || test -d $$file; then d=.; else d=$(srcdir); fi; \
+         if test -d $$d/$$file; then \
+           dir=`echo "/$$file" | sed -e 's,/[^/]*$$,,'`; \
+           if test -d "$(distdir)/$$file"; then \
+             find "$(distdir)/$$file" -type d ! -perm -700 -exec chmod u+rwx {} \;; \
+           fi; \
+           if test -d $(srcdir)/$$file && test $$d != $(srcdir); then \
+             cp -fpR $(srcdir)/$$file "$(distdir)$$dir" || exit 1; \
+             find "$(distdir)/$$file" -type d ! -perm -700 -exec chmod u+rwx {} \;; \
+           fi; \
+           cp -fpR $$d/$$file "$(distdir)$$dir" || exit 1; \
+         else \
+           test -f "$(distdir)/$$file" \
+           || cp -p $$d/$$file "$(distdir)/$$file" \
+           || exit 1; \
+         fi; \
+       done
+check-am: all-am
+       $(MAKE) $(AM_MAKEFLAGS) check-TESTS
+check: check-am
+all-am: Makefile
+installdirs:
+install: install-am
+install-exec: install-exec-am
+install-data: install-data-am
+uninstall: uninstall-am
+
+install-am: all-am
+       @$(MAKE) $(AM_MAKEFLAGS) install-exec-am install-data-am
+
+installcheck: installcheck-am
+install-strip:
+       $(MAKE) $(AM_MAKEFLAGS) INSTALL_PROGRAM="$(INSTALL_STRIP_PROGRAM)" \
+         install_sh_PROGRAM="$(INSTALL_STRIP_PROGRAM)" INSTALL_STRIP_FLAG=-s \
+         `test -z '$(STRIP)' || \
+           echo "INSTALL_PROGRAM_ENV=STRIPPROG='$(STRIP)'"` install
+mostlyclean-generic:
+
+clean-generic:
+
+distclean-generic:
+       -test -z "$(CONFIG_CLEAN_FILES)" || rm -f $(CONFIG_CLEAN_FILES)
+       -test . = "$(srcdir)" || test -z "$(CONFIG_CLEAN_VPATH_FILES)" || rm -f $(CONFIG_CLEAN_VPATH_FILES)
+
+maintainer-clean-generic:
+       @echo "This command is intended for maintainers to use"
+       @echo "it deletes files that may require special tools to rebuild."
+clean: clean-am
+
+clean-am: clean-generic clean-libtool mostlyclean-am
+
+distclean: distclean-am
+       -rm -f Makefile
+distclean-am: clean-am distclean-generic
+
+dvi: dvi-am
+
+dvi-am:
+
+html: html-am
+
+html-am:
+
+info: info-am
+
+info-am:
+
+install-data-am:
+
+install-dvi: install-dvi-am
+
+install-dvi-am:
+
+install-exec-am:
+
+install-html: install-html-am
+
+install-html-am:
+
+install-info: install-info-am
+
+install-info-am:
+
+install-man:
+
+install-pdf: install-pdf-am
+
+install-pdf-am:
+
+install-ps: install-ps-am
+
+install-ps-am:
+
+installcheck-am:
+
+maintainer-clean: maintainer-clean-am
+       -rm -f Makefile
+maintainer-clean-am: distclean-am maintainer-clean-generic
+
+mostlyclean: mostlyclean-am
+
+mostlyclean-am: mostlyclean-generic mostlyclean-libtool
+
+pdf: pdf-am
+
+pdf-am:
+
+ps: ps-am
+
+ps-am:
+
+uninstall-am:
+
+.MAKE: check-am install-am install-strip
+
+.PHONY: all all-am check check-TESTS check-am clean clean-generic \
+       clean-libtool distclean distclean-generic distclean-libtool \
+       distdir dvi dvi-am html html-am info info-am install \
+       install-am install-data install-data-am install-dvi \
+       install-dvi-am install-exec install-exec-am install-html \
+       install-html-am install-info install-info-am install-man \
+       install-pdf install-pdf-am install-ps install-ps-am \
+       install-strip installcheck installcheck-am installdirs \
+       maintainer-clean maintainer-clean-generic mostlyclean \
+       mostlyclean-generic mostlyclean-libtool pdf pdf-am ps ps-am \
+       uninstall uninstall-am
+
+
+# synonyms for "check"
+.PHONY: regress regress0 test
+regress regress0 test: check
+
+# do nothing in this subdir
+.PHONY: regress1 regress2 regress3
+regress1 regress2 regress3:
+
+# Tell versions [3.59,3.63) of GNU make to not export all variables.
+# Otherwise a system limit (for SysV at least) may be exceeded.
+.NOEXPORT:
diff --git a/test/regress/regress0/uf/simple.01.cvc b/test/regress/regress0/uf/simple.01.cvc
new file mode 100644 (file)
index 0000000..f5d8c10
--- /dev/null
@@ -0,0 +1,7 @@
+% EXPECT: VALID
+A: TYPE;
+B: TYPE;
+x, y: A;
+f: A -> B;
+QUERY (x = y => f(x) = f(y));
+
diff --git a/test/regress/regress0/uf/simple.02.cvc b/test/regress/regress0/uf/simple.02.cvc
new file mode 100644 (file)
index 0000000..0ebc319
--- /dev/null
@@ -0,0 +1,7 @@
+% EXPECT: INVALID
+A: TYPE;
+B: TYPE;
+x, y: A;
+f: A -> B;
+QUERY (f(x) = f(y));
+
diff --git a/test/regress/regress0/uf/simple.03.cvc b/test/regress/regress0/uf/simple.03.cvc
new file mode 100644 (file)
index 0000000..54948ed
--- /dev/null
@@ -0,0 +1,11 @@
+% EXPECT: VALID
+A: TYPE;
+B: TYPE;
+x, y: A;
+a, b: A;
+
+f: A -> B;
+
+ASSERT (x = a AND y = a) OR (x = b AND y = b);
+QUERY (f(x) = f(y));
+