diff --git a/Data/Presburger/Omega/LowLevel.hsc b/Data/Presburger/Omega/LowLevel.hsc --- a/Data/Presburger/Omega/LowLevel.hsc +++ b/Data/Presburger/Omega/LowLevel.hsc @@ -729,7 +729,7 @@ lowerBoundSatisfiable :: Presburger a => a -> IO Bool -- | Determine an upper bound on whether the formula is satisfiable. --- The lower bound is based on treating all UNKNOWN constraints as false. +-- The upper bound is based on treating all UNKNOWN constraints as true. upperBoundSatisfiable :: Presburger a => a -> IO Bool -- | Use simple, fast tests to decide whether the formula is a tautology. diff --git a/Data/Presburger/Omega/Rel.hs b/Data/Presburger/Omega/Rel.hs --- a/Data/Presburger/Omega/Rel.hs +++ b/Data/Presburger/Omega/Rel.hs @@ -325,11 +325,9 @@ -- re-introducing the background truth. The relations must have the -- same input dimensions and the same output dimensions. -- --- Given @x@ computed by --- --- > x <- intersection given =<< gist effort r given +-- The gist satisfies the property -- --- we have @x == r@. +-- > x === gist effort x given `intersection` given gist :: Effort -> Rel -> Rel -> Rel gist effort r1 r2 = useRel2Rel (L.gist effort) (relInpDim r1) (relOutDim r1) r1 r2 diff --git a/Data/Presburger/Omega/Set.hs b/Data/Presburger/Omega/Set.hs --- a/Data/Presburger/Omega/Set.hs +++ b/Data/Presburger/Omega/Set.hs @@ -210,11 +210,9 @@ -- re-introducing the background truth. The sets must have the -- same dimension. -- --- Given @x@ computed by --- --- > x <- intersection given =<< gist effort r given +-- The gist satisfies the property -- --- we have @x == r@. +-- > x === gist effort x given `intersection` given gist :: Effort -> Set -> Set -> Set gist effort s1 s2 = useSet2Set (L.gist effort) (setDim s1) s1 s2 diff --git a/LICENSE b/LICENSE --- a/LICENSE +++ b/LICENSE @@ -1,4 +1,10 @@ -Copyright (c) 2009 Christopher Rodrigues +Copyright (c) 2009 by Christopher Rodrigues +All rights reserved. + +Except for 'src/the-omega-project.tar.gz', which is +Copyright (c) 1994-2008 by the Omega Project and others +All rights reserved. + Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met: diff --git a/Makefile.in b/Makefile.in --- a/Makefile.in +++ b/Makefile.in @@ -1,21 +1,71 @@ +# Programs CXX=@CXX@ +TAR=tar +# Program parameters CPPFLAGS=@CPPFLAGS@ CXXFLAGS=@CXXFLAGS@ LDFLAGS=@LDFLAGS@ - LIBS=@LIBS@ +# Configure flags +USE_INSTALLED_OMEGA=@ac_with_omega@ + INCLUDES=src/C_omega.h +OMEGA_DIR=src/the-omega-project +OMEGA_LIB=$(OMEGA_DIR)/omega_lib/obj/libomega.a +OMEGA_MAKE_FLAGS= \ + CONFIGURE_CXXFLAGS="$(CPPFLAGS) $(CXXFLAGS)" \ + CONFIGURE_LDFLAGS="$(LDFLAGS)" \ + CONFIGURE_LIBS="$(LIBS)" \ + CONFIGURE_CXX="$(CXX)" +# If we're building the Omega library, then include its headers +ifeq ($(USE_INSTALLED_OMEGA),yes) +OMEGA_INCLUDE= +else +OMEGA_INCLUDE=-I$(OMEGA_DIR)/basic/include -I$(OMEGA_DIR)/omega_lib/include +endif + +# If we're building the Omega library, then add it as a target +# our interface file +ifeq ($(USE_INSTALLED_OMEGA),yes) +BUILD_OMEGA_TARGET= +BUILD_OMEGA_DEP= +else +BUILD_OMEGA_TARGET=$(OMEGA_DIR) $(OMEGA_LIB) +BUILD_OMEGA_DEP=$(OMEGA_DIR) +endif + +## +## RULES +## + .PHONY: all clean -all : build/C_omega.o +all : $(BUILD_OMEGA_TARGET) build/C_omega.o +clean : + @echo Making clean... +ifeq ($(USE_INSTALLED_OMEGA),no) + rm -rf $(OMEGA_DIR) +endif + +# The above is a more drastic way to clean than +# cd src && $(MAKE) veryclean $(OMEGA_MAKE_FLAGS) + build : mkdir $@ -build/C_omega.o : src/C_omega.cc build $(INCLUDES) - $(CXX) $(CPPFLAGS) $(CXXFLAGS) -c $< -o $@ +build/C_omega.o : src/C_omega.cc build $(INCLUDES) $(BUILD_OMEGA_DEP) + $(CXX) $(CPPFLAGS) $(CXXFLAGS) $(OMEGA_INCLUDE) -c $< -o $@ +$(OMEGA_DIR) : + cd src && \ + $(TAR) -xzf the-omega-project.tar.gz + +$(OMEGA_LIB) : $(OMEGA_DIR) + cd $(OMEGA_DIR) && \ + $(MAKE) depend $(OMEGA_MAKE_FLAGS) && \ + $(MAKE) libomega.a $(OMEGA_MAKE_FLAGS) diff --git a/Omega.cabal b/Omega.cabal --- a/Omega.cabal +++ b/Omega.cabal @@ -1,5 +1,5 @@ Name: Omega -Version: 0.1.1 +Version: 0.1.2 Cabal-Version: >= 1.2.3 Build-Type: Custom License: BSD3 @@ -13,19 +13,19 @@ whose members can be represented compactly as a Presburger arithmetic formula. The primary interface can be found in "Data.Presburger.Omega.Set" and "Data.Presburger.Omega.Rel". - - The Omega library - () must - be installed to build this package. Category: Data Extra-Source-Files: README + aclocal.m4 configure.ac Makefile.in - src/C_omega.h - src/C_omega.cc + src/the-omega-project.tar.gz Extra-Tmp-Files: build/C_omega.o +Flag UseInstalledOmega + Description: Link to a preinstalled version of the Omega library + Default: False + Library Build-Depends: base >= 3 && < 4, containers Exposed-Modules: @@ -38,4 +38,8 @@ Extensions: GADTs ScopedTypeVariables Build-Tools: hsc2hs Include-Dirs: src - Extra-Libraries: omega stdc++ + + if flag(UseInstalledOmega) + Extra-Libraries: omega stdc++ + else + Extra-Libraries: stdc++ diff --git a/README b/README --- a/README +++ b/README @@ -1,38 +1,41 @@ Omega -- Operations on Presburger arithmetic formulae +This package contains a reduced copy of the Omega library. +The Omega library's home page is http://www.cs.umd.edu/projects/omega/, and +its full sources are at http://github.com/davewathaverford/the-omega-project/. + BUILDING INSTRUCTIONS --------------------- This is a Cabal package. The typical build process is: - runhaskell Setup.hs configure + runhaskell Setup.hs configure runhaskell Setup.hs build runhaskell Setup.hs install -This package requires the C++ Omega library to be installed -(http://github.com/davewathaverford/the-omega-project). Because this package -contains C++ source code, Cabal will probably need help finding the required -headers and libraries. +Configure with -fUseInstalledOmega if you have already installed the C++ +Omega library. Otherwise, the library will be built and linked into this +package. -You will probably need to provide the paths to the C++ include directory -(contains STL headers such as "vector") and library directory (contains the -C runtime library, called "libstdc++.so" on GNU Linux systems). If the C++ -Omega library is not installed in a standard place, you will also need to -provide paths to it. +GHCi is not supported due to dynamic loading problems. +Because this package contains C++ source code, Cabal may need help +finding the required headers and libraries. You may need to provide the paths +to the C++ include directory (contains STL headers such as "vector") and +library directory (contains the C runtime library, called "libstdc++.so" on +GNU Linux systems). If the C++ Omega library is not installed in a standard +place, you will also need to provide paths to it. + A configuration might look something like this: - runhaskell Setup.hs configure \ + runhaskell Setup.hs configure --disable-library-for-ghci -p \ --extra-include-dirs=$(YOUR_CXX_INCLUDE_PATH) \ - --extra-lib-dirs=$(YOUR_CXX_LIB_PATH) \ - --extra-include-dirs=$(YOUR_OMEGA_PATH)/basic/include \ - --extra-include-dirs=$(YOUR_OMEGA_PATH)/omega_lib/include \ - --extra-lib-dirs=$(YOUR_OMEGA_PATH)/omega_lib/obj + --extra-lib-dirs=$(YOUR_CXX_LIB_PATH) DOCUMENTATION ------------- -The C++ Omega library includes documentation of its exported interface. -You may wish to look there if the Haddock documentation for a set operation -or relation operation is lacking. +The C++ Omega library includes documentation of its exported interface in +'interface.dvi'. You may wish to look there if the Haddock documentation for +a set operation or relation operation is lacking. diff --git a/Setup.hs b/Setup.hs --- a/Setup.hs +++ b/Setup.hs @@ -1,5 +1,6 @@ import Control.Applicative +import Control.Exception(bracket) import Control.Monad import Data.Char import Data.Maybe @@ -15,27 +16,52 @@ import System.Directory import System.Exit(ExitCode(..)) import System.IO -import System.FilePath(()) +import System.FilePath((), (<.>), takeExtension) import System.Process -- Mimic the && command of 'sh' (>&&>) :: IO ExitCode -> IO ExitCode -> IO ExitCode -cmd1 >&&> cmd2 = do - rc <- cmd1 - case rc of - ExitSuccess -> cmd2 - ExitFailure _ -> return rc +cmd1 >&&> cmd2 = cmd1 >>= continue + where + continue ExitSuccess = cmd2 + continue returnCode = return returnCode +-- Record whether we're building the Omega library here +useInstalledOmegaFlagPath = "build" "UseInstalledOmega" + +writeUseInstalledOmegaFlag :: Bool -> IO () +writeUseInstalledOmegaFlag b = do + createDirectoryIfMissing False "build" + writeFile useInstalledOmegaFlagPath (show b) + +readUseInstalledOmegaFlag :: IO Bool +readUseInstalledOmegaFlag = do + text <- readFile useInstalledOmegaFlagPath `catch` + \_ -> die "Configuration file missing; try reconfiguring" + return $! read text + -- We will call 'autoconf' and 'make' autoconfProgram = simpleProgram "autoconf" makeProgram = simpleProgram "make" --- Our single C++ source file is here +-- Our single C++ source file and corresponding object file are here cppSourceName = "src" "C_omega.cc" - --- It becomes this object file cppObjectName = "build" "C_omega.o" +-- If we're building the Omega library, it's here +omegaLibPath = "src" "the-omega-project" "omega_lib" "obj" "libomega.a" + +-- Unpack the Omega library into this directory +omegaUnpackPath = "build" "unpack_omega" + +noGHCiLib = + die "Sorry, this package does not support GHCi.\n\ + \Please configure with --disable-library-for-ghci to disable." + +noSharedLib = + die "Sorry, this package does not support shared library output.\n\ + \Please configure with --disable-shared to disable." + ------------------------------------------------------------------------------- -- Configuration @@ -43,32 +69,49 @@ -- Run Cabal configure lbi <- confHook simpleUserHooks pkgDesc flags - let verb = fromFlagOrDefault Verbosity.normal $ configVerbosity flags - cfg = withPrograms lbi + -- Detect and report error on unsupported configurations + when (withGHCiLib lbi) noGHCiLib + when (withSharedLib lbi) noSharedLib + + let verb = fromFlagOrDefault Verbosity.normal $ configVerbosity flags + cfg = withPrograms lbi runAutoconf = do rawSystemProgramConf verb autoconfProgram cfg [] return ExitSuccess -- Run autoconf configure runAutoconf >&&> runConfigure lbi + -- Save this flag for later use + writeUseInstalledOmegaFlag useInstalledOmega + return lbi where + -- Will build the Omega library? + useInstalledOmega = fromMaybe False $ + lookup (FlagName "useinstalledomega") $ + configConfigurationsFlags flags + -- Run 'configure' with the extra arguments that were passed to -- Setup.hs runConfigure lbi = do currentDir <- getCurrentDirectory - let opts = autoConfigureOptions lbi + let opts = autoConfigureOptions lbi useInstalledOmega configProgramName = currentDir "configure" rawSystem configProgramName opts -- Configuration: extract options to pass to 'configure' -autoConfigureOptions :: LocalBuildInfo -> [String] -autoConfigureOptions localBuildInfo = [libdirs, includedirs] +autoConfigureOptions :: LocalBuildInfo -> Bool -> [String] +autoConfigureOptions localBuildInfo useInstalledOmega = + withOmega ++ [libdirs, includedirs] where + withOmega = if useInstalledOmega + then ["--with-omega"] + else [] + libraryDescr = case library $ localPkgDescr localBuildInfo of Nothing -> error "Library description is missing" Just l -> l @@ -91,41 +134,85 @@ -- Building buildOmega pkgDesc lbi userhooks flags = do + + useInstalledOmega <- readUseInstalledOmegaFlag + -- Do default build procedure for hs files buildHook simpleUserHooks pkgDesc lbi userhooks flags - -- Get 'ar' program + -- Get 'ar' and 'ld' programs let verb = fromFlagOrDefault Verbosity.normal $ buildVerbosity flags (arPgm, _) <- requireProgram verb arProgram AnyVersion (withPrograms lbi) + let runAr = rawSystemProgram verb arPgm - -- Build the C++ source file + -- Build the C++ source file (and Omega library, if configured) + -- Makefile's behavior is controlled by output of 'configure' rawSystemProgramConf verb makeProgram (withPrograms lbi) ["all"] - -- Add the object file to libraries + -- Add other object files to libraries let pkgId = package $ localPkgDescr lbi - let addStaticObjectFile objName libName = - rawSystemProgram verb arPgm ["r", libName, objName] + let -- Add extra files into an archive file + addStaticObjectFiles libName = do + -- Add the C++ interface file + addStaticObjectFile cppObjectName libName + -- Add contents of libomega.a + unless useInstalledOmega $ + transferArFiles verb runAr omegaLibPath libName + + where + addStaticObjectFile objName libName = + runAr ["r", libName, objName] + when (withVanillaLib lbi) $ let libName = buildDir lbi mkLibName pkgId - in addStaticObjectFile cppObjectName libName + in addStaticObjectFiles libName when (withProfLib lbi) $ let libName = buildDir lbi mkProfLibName pkgId - in addStaticObjectFile cppObjectName libName + in addStaticObjectFiles libName - when (withSharedLib lbi) $ - die "Sorry, this package is not set up to build shared libraries" + when (withGHCiLib lbi) noGHCiLib + when (withSharedLib lbi) noSharedLib return () +-- Transfer the contents of one archive to another +transferArFiles verb runAr src dst = do + srcCan <- canonicalizePath src + dstCan <- canonicalizePath dst + withTempDirectory verb omegaUnpackPath $ + + -- Save/restore the current working directory + bracket getCurrentDirectory setCurrentDirectory $ \_ -> do + + -- Go to temporary directory + setCurrentDirectory omegaUnpackPath + + -- Unpack source archive + runAr ["x", srcCan] + + -- Find object files + objs <- liftM (filter isObjectFile) $ getDirectoryContents "." + when (null objs) $ warn verb "No object files found in Omega library; build may be incomplete" + + -- Insert into destination archive + runAr (["r", dstCan] ++ objs) + where + isObjectFile f = takeExtension f == ".o" + ------------------------------------------------------------------------------- -- Cleaning cleanOmega pkgDesc mlbi userhooks flags = do let verb = fromFlagOrDefault Verbosity.normal $ cleanVerbosity flags + -- run 'make clean', which will clean the Omega library if appropriate + case mlbi of + Just lbi -> rawSystemProgramConf verb makeProgram (withPrograms lbi) ["clean"] + Nothing -> return () + -- Clean extra files if we don't need to save configuration -- (Other temp files are automatically cleaned) unless (fromFlag $ cleanSaveConf flags) $ do @@ -146,11 +233,12 @@ -- (one level of recursion only), ignoring errors lenientRemoveDirectory f = do b <- doesDirectoryExist f - when b $ do lenientRemoveFiles =<< getDirectoryContents f + when b $ do lenientRemoveFiles . map (f ) =<< getDirectoryContents f removeDirectory f `catch` \_ -> return () -- Extra files produced by configuration - configFiles = ["configure", "config.log", "config.status", "Makefile"] + configFiles = ["configure", "config.log", "config.status", "Makefile", + useInstalledOmegaFlagPath] ------------------------------------------------------------------------------- -- Hooks diff --git a/aclocal.m4 b/aclocal.m4 new file mode 100644 --- /dev/null +++ b/aclocal.m4 @@ -0,0 +1,9 @@ + +m4_define([AC_OMEGA_IFELSE], +[if test "$ac_with_omega" == "yes" ; then +$1 +: +else +$2 +: +fi]) diff --git a/configure.ac b/configure.ac --- a/configure.ac +++ b/configure.ac @@ -3,37 +3,51 @@ AC_INIT(Omega, 0.1) AC_LANG(C++) +# Compile with pre-installed Omega? +AC_ARG_WITH(omega,[[Use preinstalled Omega library]], + [ac_with_omega=yes], + [ac_with_omega=no]) # Check for programs AC_PROG_CXX +AC_OMEGA_IFELSE([],[AC_MSG_NOTICE([will build the Omega library from source])]) + # Check the omega library -AC_MSG_CHECKING([whether we can include basic/bool.h]) -AC_COMPILE_IFELSE( - [AC_LANG_SOURCE([[#include - ]])], - [AC_MSG_RESULT([ok])], - [AC_MSG_FAILURE([cannot include basic/bool.h])]) +AC_OMEGA_IFELSE([ + AC_MSG_CHECKING([whether we can include basic/bool.h]) + AC_COMPILE_IFELSE( + [AC_LANG_SOURCE([[#include + ]])], + [AC_MSG_RESULT([ok])], + [AC_MSG_FAILURE([cannot include basic/bool.h])]) +]) -AC_MSG_CHECKING([whether we can include omega.h]) -AC_COMPILE_IFELSE( - [AC_LANG_SOURCE([[#include - ]])], - [AC_MSG_RESULT([ok])], - [AC_MSG_FAILURE([cannot include omega.h])]) +AC_OMEGA_IFELSE([ + AC_MSG_CHECKING([whether we can include omega.h]) + AC_COMPILE_IFELSE( + [AC_LANG_SOURCE([[#include + ]])], + [AC_MSG_RESULT([ok])], + [AC_MSG_FAILURE([cannot include omega.h])]) +]) -AC_MSG_CHECKING([whether we can link with omega library]) -{ - LIBS="${LIBS} -lomega" - AC_LINK_IFELSE( - [AC_LANG_PROGRAM( - [[#include ]], - [[omega::Relation::Null();]])], - [AC_MSG_RESULT([yes])], - [AC_MSG_FAILURE([cannot link with the omega library])]) -} +AC_OMEGA_IFELSE([ + AC_MSG_CHECKING([whether we can link with omega library]) + { + LIBS="${LIBS} -lomega" + AC_LINK_IFELSE( + [AC_LANG_PROGRAM( + [[#include + ]], + [[omega::Relation::Null();]])], + [AC_MSG_RESULT([yes])], + [AC_MSG_FAILURE([cannot link with the omega library])]) + } +]) # Output +AC_SUBST(ac_with_omega) AC_CONFIG_FILES([Makefile]) AC_OUTPUT diff --git a/src/C_omega.cc b/src/C_omega.cc deleted file mode 100644 --- a/src/C_omega.cc +++ /dev/null @@ -1,535 +0,0 @@ - -#include -#include - -#include "C_omega.h" - -extern "C" -Relation *hsw_new_relation(int n_input, int n_output) -{ - return new Relation(n_input, n_output); -} - -extern "C" -Relation *hsw_new_set(int n) -{ - return new Relation(n); -} - -extern "C" -void hsw_free_relation(Relation *rel) -{ - delete rel; -} - -extern "C" -char *hsw_relation_show(Relation *rel) -{ - return strdup((const char *)rel->print_with_subs_to_string()); -} - -extern "C" -int hsw_num_input_vars(Relation *rel) -{ - return rel->n_inp(); -} - -extern "C" -int hsw_num_output_vars(Relation *rel) -{ - return rel->n_out(); -} - -extern "C" -int hsw_num_set_vars(Relation *rel) -{ - return rel->n_set(); -} - -extern "C" -Var_Decl *hsw_input_var(Relation *rel, int n) -{ - return rel->input_var(n); -} - -extern "C" -Var_Decl *hsw_output_var(Relation *rel, int n) -{ - return rel->output_var(n); -} -extern "C" -Var_Decl *hsw_set_var(Relation *rel, int n) -{ - return rel->set_var(n); -} - -extern "C" -int hsw_is_lower_bound_satisfiable(Relation *rel) -{ - return rel->is_lower_bound_satisfiable(); -} - -extern "C" -int hsw_is_upper_bound_satisfiable(Relation *rel) -{ - return rel->is_upper_bound_satisfiable(); -} - -extern "C" -int hsw_is_obvious_tautology(Relation *rel) -{ - return rel->is_obvious_tautology(); -} -extern "C" -int hsw_is_definite_tautology(Relation *rel) -{ - return rel->is_tautology(); -} - -extern "C" -int hsw_is_exact(Relation *rel) -{ - return rel->is_exact(); -} - -extern "C" -int hsw_is_inexact(Relation *rel) -{ - return rel->is_inexact(); -} - -extern "C" -int hsw_is_unknown(Relation *rel) -{ - return rel->is_unknown(); -} - -extern "C" -Relation *hsw_upper_bound(Relation *rel) -{ - return new Relation(Upper_Bound(copy(*rel))); -} - -extern "C" -Relation *hsw_lower_bound(Relation *rel) -{ - return new Relation(Lower_Bound(copy(*rel))); -} - -extern "C" -int hsw_equal(Relation *r, Relation *s) -{ - /* r == s - * iff - * r `intersection` not s == False - * && r `union` not s == True - */ - Relation com_s = Complement(copy(*s)); - - /* If intersection is satisfiable, unequal */ - if (Intersection(copy(*r), copy(com_s)).is_upper_bound_satisfiable()) - return 0; - - /* If union is tautology, equal; else unequal */ - return Union(copy(*r), com_s).is_tautology(); -} - -extern "C" -Relation *hsw_union(Relation *r, Relation *s) -{ - return new Relation(Union(copy(*r), copy(*s))); -} - -extern "C" -Relation *hsw_intersection(Relation *r, Relation *s) -{ - return new Relation(Intersection(copy(*r), copy(*s))); -} - -extern "C" -Relation *hsw_composition(Relation *r, Relation *s) -{ - return new Relation(Composition(copy(*r), copy(*s))); -} - -extern "C" -Relation *hsw_restrict_domain(Relation *r, Relation *s) -{ - return new Relation(Restrict_Domain(copy(*r), copy(*s))); -} - -extern "C" -Relation *hsw_restrict_range(Relation *r, Relation *s) -{ - return new Relation(Restrict_Range(copy(*r), copy(*s))); -} - -extern "C" -Relation *hsw_difference(Relation *r, Relation *s) -{ - return new Relation(Difference(copy(*r), copy(*s))); -} - -extern "C" -Relation *hsw_cross_product(Relation *r, Relation *s) -{ - return new Relation(Cross_Product(copy(*r), copy(*s))); -} - -extern "C" -Relation *hsw_gist(Relation *r, Relation *s, int effort) -{ - return new Relation(Gist(copy(*r), copy(*s), effort)); -} - -extern "C" -Relation *hsw_transitive_closure(Relation *rel) -{ - return new Relation(TransitiveClosure(copy(*rel))); -} - -extern "C" -Relation *hsw_domain(Relation *rel) -{ - return new Relation(Domain(copy(*rel))); -} - -extern "C" -Relation *hsw_range(Relation *rel) -{ - return new Relation(Range(copy(*rel))); -} - -extern "C" -Relation *hsw_inverse(Relation *rel) -{ - return new Relation(Inverse(copy(*rel))); -} - -extern "C" -Relation *hsw_complement(Relation *rel) -{ - return new Relation(Complement(copy(*rel))); -} - -extern "C" -Relation *hsw_deltas(Relation *rel) -{ - return new Relation(Deltas(copy(*rel))); -} - -extern "C" -Relation *hsw_approximate(Relation *rel) -{ - return new Relation(Approximate(copy(*rel))); -} - -extern "C" -F_And *hsw_relation_add_and(Relation *rel) -{ - return rel->add_and(); -} - -extern "C" -Formula *hsw_relation_add_or(Relation *rel) -{ - return rel->add_or(); -} - -extern "C" -Formula *hsw_relation_add_not(Relation *rel) -{ - return rel->add_not(); -} - -extern "C" -F_Declaration *hsw_relation_add_forall(Relation *rel) -{ - return rel->add_forall(); -} - -extern "C" -F_Declaration *hsw_relation_add_exists(Relation *rel) -{ - return rel->add_exists(); -} - -extern "C" -void hsw_relation_finalize(Relation *rel) -{ - rel->finalize(); -} - -extern "C" -Var_Decl *hsw_declaration_declare(F_Declaration *rel) -{ - return rel->declare(); -} - -extern "C" -F_And *hsw_formula_to_and(Formula *rel) -{ - F_And *and_formula = dynamic_cast(rel); - - /* If the parameter is already an 'and', return it */ - if (and_formula) return and_formula; - - /* Otherwise add an 'and' */ - return rel->add_and(); -} - -extern "C" -F_And *hsw_formula_add_and(Formula *rel) -{ - return rel->add_and(); -} - -extern "C" -Formula *hsw_formula_add_or(Formula *rel) -{ - return rel->add_or(); -} - -extern "C" -Formula *hsw_formula_add_not(Formula *rel) -{ - return rel->add_not(); -} - -extern "C" -F_Declaration *hsw_formula_add_forall(Formula *rel) -{ - return rel->add_forall(); -} - -extern "C" -F_Declaration *hsw_formula_add_exists(Formula *rel) -{ - return rel->add_exists(); -} - -extern "C" -void hsw_formula_finalize(Formula *rel) -{ - rel->finalize(); -} - -/* hsw_add_constraint creates an equality or inequality constraint, - * fills in the coefficients for each variable, and fills in the - * constant term. */ -extern "C" -void hsw_add_constraint(F_And *formula, - int is_eq, - int num_vars, - int *coefficients, - Var_Decl **vars, - int constant) -{ - Constraint_Handle *hdl = is_eq - ? (Constraint_Handle *)new EQ_Handle(formula->add_EQ()) - : (Constraint_Handle *)new GEQ_Handle(formula->add_GEQ()); - - /* Update each coefficient in the array */ - for (; num_vars; num_vars--) - { - int index = num_vars - 1; - hdl->update_coef(vars[index], coefficients[index]); - } - - /* Update the constant part of the constraint */ - hdl->update_const(constant); - - hdl->finalize(); - free(hdl); -} - -/* These are all for inspecting a DNF formula */ - -extern "C" -DNF_Iterator *hsw_query_dnf(Relation *rel) -{ - return new DNF_Iterator(rel->query_DNF()); -} - -extern "C" -Conjunct *hsw_dnf_iterator_next(DNF_Iterator *iter) -{ - if (!iter->live()) return NULL; - - Conjunct *c = **iter; - ++*iter; - return c; -} - -extern "C" -void hsw_dnf_iterator_free(DNF_Iterator *iter) -{ - delete iter; -} - -/* Use to iterate over the tuple of the variables that are used in the - * conjunct. The variables obtained should not be freed. */ -extern "C" -struct Tuple_Iter *hsw_get_conjunct_variables(Conjunct *conj) -{ - Tuple_Iterator *ti = - reinterpret_cast *> - (new Tuple_Iterator(*conj->variables())); - return (struct Tuple_Iter *)ti; -} - -extern "C" -void * -hsw_tuple_iterator_next(struct Tuple_Iter *iter) -{ - Tuple_Iterator *ti = (Tuple_Iterator *)iter; - - if (!ti->live()) return NULL; // Exhausted? - - void *ret = (void *)**ti; - ++*ti; - return ret; -} - -extern "C" -void -hsw_tuple_iterator_free(struct Tuple_Iter *iter) -{ - delete (Tuple_Iterator *)iter; -} - -/* Use to iterate over the EQ constraints in a conjunct. The constraints - * obtained should be freed once you're done with them. */ -extern "C" -struct EQ_Iterator * -hsw_get_eqs(Conjunct *conj) -{ - return new EQ_Iterator(conj->EQs()); -} - -extern "C" -struct EQ_Handle * -hsw_eqs_next(struct EQ_Iterator *g) -{ - if (!g->live()) return NULL; // Exhausted? - - EQ_Handle *hdl = new EQ_Handle(**g); - ++*g; - return hdl; -} - -extern "C" -void -hsw_eqs_free(struct EQ_Iterator *g) -{ - delete g; -} - -extern "C" -void -hsw_eq_handle_free(struct EQ_Handle *hdl) -{ - delete hdl; -} - -/* Use to iterate over the GEQ constraints in a conjunct. Works like - * hsw_get_eqs. */ -extern "C" -struct GEQ_Iterator *hsw_get_geqs(Conjunct *conj) -{ - return new GEQ_Iterator(conj->GEQs()); -} - -extern "C" -struct GEQ_Handle * -hsw_geqs_next(struct GEQ_Iterator *g) -{ - if (!g->live()) return NULL; // Exhausted? - - GEQ_Handle *hdl = new GEQ_Handle(**g); - ++*g; - return hdl; -} - -extern "C" -void -hsw_geqs_free(struct GEQ_Iterator *g) -{ - delete g; -} - -extern "C" -void -hsw_geq_handle_free(struct GEQ_Handle *hdl) -{ - delete hdl; -} - -extern "C" -coefficient_t -hsw_constraint_get_const(struct Constraint_Handle_ *hdl) -{ - return ((struct Constraint_Handle *)hdl)->get_const(); -} - -extern "C" -Constr_Vars_Iter * -hsw_constraint_get_coefficients(struct Constraint_Handle_ *hdl) -{ - return new Constr_Vars_Iter(*(Constraint_Handle *)hdl); -} - -extern "C" -int -hsw_constr_vars_next(Variable_Info_struct *out, Constr_Vars_Iter *iter) -{ - if (!iter->live()) return 0; - - Variable_Info info(**iter); - ++*iter; - - out->var = info.var; - out->coef = info.coef; - - return 1; -} - -extern "C" -void -hsw_constr_vars_free(Constr_Vars_Iter *iter) -{ - delete iter; -} - -/* For debugging */ - -extern "C" -void -hsw_debug_print_eq(struct EQ_Handle *hdl) -{ - String s(hdl->print_to_string()); - puts(s); -} - -extern "C" -void -hsw_debug_print_geq(struct GEQ_Handle *hdl) -{ - String s(hdl->print_to_string()); - puts(s); -} - -#if 0 /* Not used? */ - -/* Find an array element equal to v. Return the element index, - * or -1 if no element matches. */ -static int -find_variable_index(Var_Decl *v, int num_vars, Var_Decl **vars) -{ - int n; - for (n = 0; n < num_vars; n++) { - if (v == vars[n]) return n; - } - return -1; -} -#endif diff --git a/src/C_omega.h b/src/C_omega.h deleted file mode 100644 --- a/src/C_omega.h +++ /dev/null @@ -1,115 +0,0 @@ - -#ifndef C_OMEGA_H -#define C_OMEGA_H - -#ifdef __cplusplus -extern "C" { -#endif - -/* This is a copy of 'coef_t'. Can't use the original because it's in - * a C++ header file. */ -typedef long long coefficient_t; - -/* This is a copy of struct Variable_Info. Can't use the original because - * it's in a C++ header file. */ -typedef struct Variable_Info_struct { - struct Var_Decl *var; - coefficient_t coef; -} Variable_Info_struct; - -struct Relation *hsw_new_relation(int n_input, int n_output); -struct Relation *hsw_new_set(int n); -void hsw_free_relation(struct Relation *rel); -char *hsw_relation_show(struct Relation *rel); -int hsw_num_input_vars(struct Relation *rel); -int hsw_num_output_vars(struct Relation *rel); -int hsw_num_set_vars(struct Relation *rel); -struct Var_Decl *hsw_input_var(struct Relation *rel, int n); -struct Var_Decl *hsw_output_var(struct Relation *rel, int n); -struct Var_Decl *hsw_set_var(struct Relation *rel, int n); -int hsw_is_lower_bound_satisfiable(struct Relation *rel); -int hsw_is_upper_bound_satisfiable(struct Relation *rel); -int hsw_is_obvious_tautology(struct Relation *rel); -int hsw_is_definite_tautology(struct Relation *rel); -int hsw_is_exact(struct Relation *rel); -int hsw_is_inexact(struct Relation *rel); -int hsw_is_unknown(struct Relation *rel); -struct Relation *hsw_upper_bound(struct Relation *); -struct Relation *hsw_lower_bound(struct Relation *); -int hsw_equal(struct Relation *, struct Relation *); -struct Relation *hsw_union(struct Relation *, struct Relation *); -struct Relation *hsw_intersection(struct Relation *, struct Relation *); -struct Relation *hsw_composition(struct Relation *, struct Relation *); -struct Relation *hsw_restrict_domain(struct Relation *, struct Relation *); -struct Relation *hsw_restrict_range(struct Relation *, struct Relation *); -struct Relation *hsw_difference(struct Relation *, struct Relation *); -struct Relation *hsw_cross_product(struct Relation *, struct Relation *); -struct Relation *hsw_gist(struct Relation *, struct Relation *, int); -struct Relation *hsw_transitive_closure(struct Relation *); -struct Relation *hsw_domain(struct Relation *); -struct Relation *hsw_range(struct Relation *); -struct Relation *hsw_inverse(struct Relation *); -struct Relation *hsw_complement(struct Relation *); -struct Relation *hsw_deltas(struct Relation *); -struct Relation *hsw_approximate(struct Relation *); - -struct F_And *hsw_relation_add_and(struct Relation *rel); -struct Formula *hsw_relation_add_or(struct Relation *rel); -struct Formula *hsw_relation_add_not(struct Relation *rel); -struct F_Declaration *hsw_relation_add_forall(struct Relation *rel); -struct F_Declaration *hsw_relation_add_exists(struct Relation *rel); -void hsw_relation_finalize(struct Relation *rel); - -struct F_And *hsw_formula_add_and(struct Formula *rel); -struct Formula *hsw_formula_add_or(struct Formula *rel); -struct Formula *hsw_formula_add_not(struct Formula *rel); -struct F_Declaration *hsw_formula_add_forall(struct Formula *rel); -struct F_Declaration *hsw_formula_add_exists(struct Formula *rel); -void hsw_formula_finalize(struct Formula *rel); - -struct Var_Decl *hsw_declaration_declare(struct F_Declaration *rel); - -struct F_And *hsw_formula_to_and(struct Formula *rel); - -void hsw_add_constraint(struct F_And *formula, - int is_eq, - int num_vars, - int *coefficients, - struct Var_Decl **vars, - int constant); - -struct DNF_Iterator *hsw_query_dnf(struct Relation *rel); -struct Conjunct *hsw_dnf_iterator_next(struct DNF_Iterator *iter); -void hsw_dnf_iterator_free(struct DNF_Iterator *iter); - -struct Tuple_Iter *hsw_get_conjunct_variables(struct Conjunct *conj); -void *hsw_tuple_iterator_next(struct Tuple_Iter *iter); -void hsw_tuple_iterator_free(struct Tuple_Iter *iter); - -struct EQ_Iterator *hsw_get_eqs(struct Conjunct *conj); -struct EQ_Handle *hsw_eqs_next(struct EQ_Iterator *g); -void hsw_eqs_free(struct EQ_Iterator *g); -void hsw_eq_handle_free(struct EQ_Handle *hdl); - -struct GEQ_Iterator *hsw_get_geqs(struct Conjunct *conj); -struct GEQ_Handle *hsw_geqs_next(struct GEQ_Iterator *g); -void hsw_geqs_free(struct GEQ_Iterator *g); -void hsw_geq_handle_free(struct GEQ_Handle *hdl); - -struct Constraint_Handle_; /* Use a different name to get rid of C++ warning */ -coefficient_t hsw_constraint_get_const(struct Constraint_Handle_ *hdl); -struct Constr_Vars_Iter *hsw_constraint_get_coefficients(struct Constraint_Handle_ *hdl); -int hsw_constr_vars_next(Variable_Info_struct *out, struct Constr_Vars_Iter *iter); -void hsw_constr_vars_free(struct Constr_Vars_Iter *iter); - - - -void hsw_debug_print_eq(struct EQ_Handle *hdl); -void hsw_debug_print_geq(struct GEQ_Handle *hdl); - - -#ifdef __cplusplus -} -#endif - -#endif diff --git a/src/the-omega-project.tar.gz b/src/the-omega-project.tar.gz new file mode 100644 Binary files /dev/null and b/src/the-omega-project.tar.gz differ