packages feed

Omega 0.1.1 → 0.1.2

raw patch · 13 files changed

+257/−737 lines, 13 filessetup-changedbinary-added

Files

Data/Presburger/Omega/LowLevel.hsc view
@@ -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.
Data/Presburger/Omega/Rel.hs view
@@ -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
Data/Presburger/Omega/Set.hs view
@@ -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
LICENSE view
@@ -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:
Makefile.in view
@@ -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)
Omega.cabal view
@@ -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-        (<http://github.com/davewathaverford/the-omega-project>) 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++
README view
@@ -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 <FLAGS> 	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.
Setup.hs view
@@ -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
+ aclocal.m4 view
@@ -0,0 +1,9 @@++m4_define([AC_OMEGA_IFELSE],+[if test "$ac_with_omega" == "yes" ; then+$1+:+else+$2+:+fi])
configure.ac view
@@ -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 <basic/bool.h>-		]])],-	[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 <basic/bool.h>+			]])],+		[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 <omega.h>-		]])],-	[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 <omega.h>+			]])],+		[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.h>]],-		[[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.h>+			]],+			[[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
− src/C_omega.cc 
@@ -1,535 +0,0 @@--#include <omega.h>-#include <string.h>--#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<F_And *>(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<void *> *ti =-    reinterpret_cast<Tuple_Iterator<void *> *>-    (new Tuple_Iterator<Variable_ID>(*conj->variables()));-  return (struct Tuple_Iter *)ti;-}--extern "C"-void *-hsw_tuple_iterator_next(struct Tuple_Iter *iter)-{-  Tuple_Iterator<void *> *ti = (Tuple_Iterator<void *> *)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<void *> *)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
− src/C_omega.h 
@@ -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
+ src/the-omega-project.tar.gz view

binary file changed (absent → 728537 bytes)