diff --git a/Data/Presburger/Omega/Expr.hs b/Data/Presburger/Omega/Expr.hs --- a/Data/Presburger/Omega/Expr.hs +++ b/Data/Presburger/Omega/Expr.hs @@ -37,6 +37,9 @@ (|==|), (|/=|), (|>|), (|>=|), (|<|), (|<=|), forallE, existsE, + -- ** Destruction + foldIntExp, foldBoolExp, + -- ** Internal data structures -- -- | These are exported to allow other modules to build the low-level @@ -44,6 +47,7 @@ -- expressions. Normally, the 'Exp' functions are sufficient. Expr, IntExpr, BoolExpr, PredOp(..), + Quantifier(..), wrapExpr, wrapSimplifiedExpr, varExpr, sumOfProductsExpr, conjExpr, disjExpr, testExpr, existsExpr, @@ -263,19 +267,89 @@ e |<=| f = f |>=| e -- | Build a universally quantified formula. -forallE :: (Var -> Exp t) -> Exp t +forallE :: (Var -> BoolExp) -> BoolExp forallE f = wrapExpr $ QuantE Forall $ getExpr $ withFreshVariable f -- | Build an existentially quantified formula. -existsE :: (Var -> Exp t) -> Exp t +existsE :: (Var -> BoolExp) -> BoolExp existsE f = wrapExpr $ QuantE Exists $ getExpr $ withFreshVariable f +-- | Reduce an integer expression to a value. Values for free variables +-- are provided explicitly in an environment. +foldIntExp :: forall a. + (Int -> [a] -> a) -- ^ summation + -> (Int -> [a] -> a) -- ^ multiplication + -> (Int -> a) -- ^ integer literal + -> [a] -- ^ environment + -> (IntExp -> a) +foldIntExp sumE prodE litE env expression = + foldIntExp' sumE prodE litE env (getSimplifiedExpr expression) + +foldIntExp' :: forall a. + (Int -> [a] -> a) -- ^ summation + -> (Int -> [a] -> a) -- ^ multiplication + -> (Int -> a) -- ^ integer literal + -> [a] -- ^ environment + -> (Expr Int -> a) +foldIntExp' sumE prodE litE env expression = rec env expression + where + rec :: forall. [a] -> Expr Int -> a + rec env expression = + case expression + of CAUE Sum lit es -> sumE lit $ map (rec env) es + CAUE Prod lit es -> prodE lit $ map (rec env) es + LitE n -> litE n + VarE (Bound i) -> env `index` i + VarE _ -> error "Expr.fold: unexpected variable" + + -- Like (!!), but throws a useful error message + index (x:_) 0 = x + index (_:xs) n = index xs (n-1) + index [] _ = error "Expr.fold: variable index out of range" + +-- | Reduce a boolean expression to a value. Values for free variables +-- are provided explicitly in an environment. +foldBoolExp :: forall a b. + (Int -> [b] -> b) -- ^ summation + -> (Int -> [b] -> b) -- ^ multiplication + -> (Int -> b) -- ^ integer literal + -> ([a] -> a) -- ^ disjunction + -> ([a] -> a) -- ^ conjunction + -> (a -> a) -- ^ negation + -> (Quantifier -> (b -> a) -> a) -- ^ quantification + -> (PredOp -> b -> a) -- ^ an integer predicate + -> a -- ^ true + -> a -- ^ false + -> [b] -- ^ environment + -> (BoolExp -> a) +foldBoolExp sumE prodE litE orE andE notE quantE predE trueE falseE + env expression = rec env (getSimplifiedExpr expression) + where + rec :: forall. [b] -> Expr Bool -> a + rec env expression = + case expression + of CAUE Disj True es -> trueE + CAUE Disj False es -> orE $ map (rec env) es + CAUE Conj True es -> andE $ map (rec env) es + CAUE Conj False es -> falseE + PredE pred e -> predE pred (integral env e) + NotE e -> notE (rec env e) + LitE True -> trueE + LitE False -> falseE + QuantE q e -> quantE q (quantifier env e) + + -- Handle a quantifier: the variable gets the specified value + quantifier env e value = rec (value:env) e + + -- Call foldIntExp for integer expressions + integral env e = foldIntExp' sumE prodE litE env e + -- | Use a fresh variable in an expression. After the expression is -- constructed, rename/adjust variable indices so that the fresh variable -- has index 0 and all other free variables' indices are incremented -- by 1. withFreshVariable :: (Var -> Exp t) -> Exp t -withFreshVariable f =unsafePerformIO $ do +withFreshVariable f = unsafePerformIO $ do v <- newQuantified return $ rename v (Bound 0) $ adjustBindings 0 1 $ f v @@ -304,7 +378,7 @@ VarE :: !Var -> Expr Int -- An expression quantified over an integer variable - QuantE :: !Quantifier -> Expr t -> Expr t + QuantE :: !Quantifier -> Expr Bool -> Expr Bool type IntExpr = Expr Int type BoolExpr = Expr Bool @@ -374,22 +448,24 @@ isLitE (LitE _) = True isLitE _ = False -deconstructProduct :: IntExpr -> Term Int -deconstructProduct (CAUE Prod n xs) = (n, xs) -deconstructProduct e = (unit Prod, [e]) +data Term = Term {-# UNPACK #-} !Int [IntExpr] -rebuildProduct :: Term Int -> Expr Int -rebuildProduct (1, [e]) = e -rebuildProduct (n, es) = CAUE Prod n es +deconstructProduct :: IntExpr -> Term +deconstructProduct (CAUE Prod n xs) = Term n xs +deconstructProduct e = Term (unit Prod) [e] -deconstructSum :: Expr Int -> Term Int -deconstructSum (CAUE Sum n xs) = (n, xs) -deconstructSum e = (unit Sum, [e]) +rebuildProduct :: Term -> IntExpr +rebuildProduct (Term 1 [e]) = e +rebuildProduct (Term n es) = CAUE Prod n es -rebuildSum :: Term Int -> Expr Int -rebuildSum (1, [e]) = e -rebuildSum (n, es) = CAUE Sum n es +deconstructSum :: IntExpr -> Term +deconstructSum (CAUE Sum n xs) = Term n xs +deconstructSum e = Term (unit Sum) [e] +rebuildSum :: Term -> IntExpr +rebuildSum (Term 1 [e]) = e +rebuildSum (Term n es) = CAUE Sum n es + -- Get the 'equality' operator for type t. cauEq :: CAUOp t -> t -> t -> Bool cauEq Sum = (==) @@ -397,13 +473,6 @@ cauEq Conj = (==) cauEq Disj = (==) --- Get the 'shows' operator for type t. -cauShows :: CAUOp t -> t -> ShowS -cauShows Sum = shows -cauShows Prod = shows -cauShows Conj = shows -cauShows Disj = shows - -- Get the zero for a CAU op (if one exists) zero :: CAUOp t -> Maybe t zero Sum = Nothing @@ -446,7 +515,7 @@ appPrec = 10 mulPrec = 7 addPrec = 6 -relPrec = 4 +cmpPrec = 5 -- Less-than, equal lamPrec = 0 -- An environment for showing expressions. @@ -457,7 +526,7 @@ data ShowsEnv = ShowsEnv { -- How to show the n_th bound variable, given a precedence context - showNthVar :: [Int -> ShowS] + showNthVar :: ![Int -> ShowS] -- Number of bound variables we know about. -- numBound e == length (showNthVar e) , numBound :: !Int @@ -519,8 +588,6 @@ LitE l -> showParen (n >= appPrec) $ showsInt l VarE v -> showsVarPrec env n v - QuantE q e -> showParen (n >= appPrec) $ - showQuantifier showsIntExprPrec env q e showsBoolExprPrec :: ShowsEnv -> Int -> BoolExpr -> ShowS showsBoolExprPrec env n expression = @@ -534,6 +601,7 @@ | otherwise -> let texts = map (showsBoolExprPrec env 0) es in showParen (n >= appPrec) $ showString "disjE " . showsList texts + PredE IsGEZ e -> showParen (n >= appPrec) $ showGEZ env e PredE p e -> let operator = case p of IsZero -> showString "isZeroE " @@ -546,6 +614,69 @@ QuantE q e -> showParen (n >= appPrec) $ showQuantifier showsBoolExprPrec env q e +-- Show an inequality prettily. +-- First, eliminate minus-signs. +-- Then, choose between the ">", ">=", or "<" for displaying a term. +-- +-- If one side of the inequality is a literal, it +-- Use ">" if it gets rid of a term, otherwise use ">=". +-- If the left side of the inequality is an integer literal, +-- then move it to the right +showGEZ :: ShowsEnv -> IntExpr -> ShowS +showGEZ env (CAUE Sum lit es) = + -- Partition into terms that will go on the left (positive) and right + -- (negative) sides of the inequality. Try to get rid of a '1' by + -- using a greater-than sign. + case partitionSumBySign lit es + of (-1, neg, pos) -> balanceInequality False 0 neg pos + (n, neg, pos) -> balanceInequality True n neg pos + where + -- If the left side is empty, flip the direction of the inequality + balanceInequality True n neg [] = + showInequality le (negate n) [] neg + + balanceInequality False n neg [] = + showInequality lt (negate n) [] neg + + balanceInequality True n neg pos = + showInequality ge n neg pos + + balanceInequality False n neg pos = + showInequality gt n neg pos + + -- Show the inequality. Put the literal on whichever side makes it + -- positive. + showInequality symbol lit neg pos = + let (pos', neg') = + if lit >= 0 + then (CAUE Sum lit pos, CAUE Sum 0 neg) + else (CAUE Sum 0 pos, CAUE Sum (negate lit) neg) + in showsIntExprPrec env cmpPrec pos' . + symbol . + showsIntExprPrec env cmpPrec neg' + + ge = showString " |>=| " + gt = showString " |>| " + le = showString " |<=| " + lt = showString " |<| " + +-- Partition a sum term based on the sign it is displayed with. +-- Negative-signed terms are multiplied by -1 to make them positive. +partitionSumBySign n es = + case partition hasNegativeMultiplier es + of (neg, pos) -> let neg' = map negateMultiplier neg + in (n, neg', pos) + where + hasNegativeMultiplier :: IntExpr -> Bool + hasNegativeMultiplier (CAUE Prod n es) = n < 0 + hasNegativeMultiplier (LitE n) = n < 0 + hasNegativeMultiplier _ = False + + negateMultiplier :: IntExpr -> IntExpr + negateMultiplier (CAUE Prod n es) = CAUE Prod (negate n) es + negateMultiplier (LitE n) = LitE (negate n) + negateMultiplier _ = error "partitionSumBySign: unexpected term" + -- Show a sum term showSum env lit es = -- The first element of the summation gets shown a little differently. @@ -562,10 +693,10 @@ showSumTailElement e = case deconstructProduct e - of (1, es) -> add . showProd env 1 es - (-1, es) -> sub . showProd env 1 es - (n, es) | n >= 0 -> add . showProd env n es - | otherwise -> sub . showProd env (negate n) es + of Term 1 es -> add . showProd env 1 es + Term (-1) es -> sub . showProd env 1 es + Term n es | n >= 0 -> add . showProd env n es + | otherwise -> sub . showProd env (negate n) es add = showString " |+| " sub = showString " |-| " @@ -577,20 +708,17 @@ then id else showsPrec mulPrec lit . showString " *| " in textLit . (text `showSepBy` showString " |*| ") - where - showMulOperator = showString " |*| " -- Show a list in [,,] syntax showsList :: [ShowS] -> ShowS -showsList ss z = - showChar '[' $ - foldr ($) (showChar ']' $ z) (intersperse (showString ", ") ss) +showsList ss = + showChar '[' . (ss `showSepBy` showString ", ") . showChar ']' -- Show a list with a separator interspersed showSepBy :: [ShowS] -> ShowS -> ShowS xs `showSepBy` sep = foldr (.) id (intersperse sep xs) --- Show a quantified expression, e.g. (forallE. (x + 1)) +-- Show a quantified expression, e.g. (forallE $ \x -> varE x |+| intE 1) showQuantifier :: (ShowsEnv -> Int -> Expr t -> ShowS) -> ShowsEnv -> Quantifier -> Expr t -> ShowS showQuantifier showExpr env q e = @@ -690,7 +818,7 @@ posToSop :: Expr Int -> Expr Int posToSop expr@(CAUE Prod n es) - | all (isSingletonList . snd) terms = + | all isSingletonTerm terms = -- If no terms are sums, then the expression is unchanged expr @@ -700,30 +828,36 @@ -- product (map sum terms') terms' = [LitE n] : map mkTermList terms - -- The cartesian product converts this to a sum of products. - sop = sequence terms' - expr' = CAUE Sum 0 (map (CAUE Prod 1) sop) + -- 'sequence' converts terms' to sum of products from. + expr' = CAUE Sum 0 [CAUE Prod 1 t | t <- sequence terms'] in simplify expr' where terms = map deconstructSum es - mkTermList (n, es) = LitE n : es - isSingletonList [_] = True - isSingletonList _ = False + mkTermList (Term n es) = LitE n : es + -- True if we've deconstructed something that's not really a sum. + -- Compare with eliminations in 'zus'. + isSingletonTerm (Term 0 [_]) = True + isSingletonTerm (Term _ []) = True + isSingletonTerm (Term _ _ ) = False + posToSop expr = expr -- Terms other than products are not modified -- Flatten nested CA expressions flatten :: forall t. Expr t -> Expr t -flatten (CAUE op lit es) = CAUE op lit (flat es) +flatten (CAUE op lit es) = + case flat lit id es of (lit', es') -> CAUE op lit' es' where -- Wherever a nested CA expression with the same operator appears, -- include its terms in the list - flat :: [Expr t] -> [Expr t] - flat (e:es) = case e - of CAUE op2 lit2 es2 - | op == op2 -> LitE lit2 : es2 ++ flat es - _ -> e:flat es - flat [] = [] + flat lit hd (e:es) = + case e + of CAUE op2 lit2 es2 + | op == op2 -> let lit' = evalCAUOp op [lit, lit2] + in flat lit' hd (es2 ++ es) + _ -> flat lit (hd . (e:)) es + flat lit hd [] = (lit, hd []) + flatten e = e -- Partially evaluate an expression @@ -771,8 +905,6 @@ -- collect (2xy + 3x - 3xy) -- becomes (-1)xy + 3x -type Term t = (t, [Expr t]) - collect :: Expr Int -> Expr Int collect (CAUE Sum literal es) = let es' = map simplify $ @@ -782,7 +914,7 @@ in CAUE Sum literal es' where - collectTerms :: [Term Int] -> [Term Int] + collectTerms :: [Term] -> [Term] collectTerms (t:ts) = case collectTerm t ts of (t', ts') -> t':collectTerms ts' collectTerms [] = [] @@ -791,14 +923,14 @@ -- the first term only in their multiplier. The collected terms' -- multipliers are summed. The result is the collected term -- and the unused terms from the list. - collectTerm :: Term Int -> [Term Int] -> (Term Int, [Term Int]) - collectTerm (factor, t) terms = + collectTerm :: Term -> [Term] -> (Term, [Term]) + collectTerm (Term factor t) terms = let (equalTerms, terms') = partition (sameTerms t) terms - factor' = factor + sum (map fst equalTerms) - in ((factor', t), terms') + factor' = factor + sum [n | Term n _ <- equalTerms] + in (Term factor' t, terms') - -- Decide whether the expression lists are equal. - sameTerms t (_, t') = expListsEqual t t' + -- True if the terms are the same modulo a constant factor. + sameTerms t (Term _ t') = expListsEqual t t' collect e = e -- Terms other than sums do not change @@ -823,9 +955,6 @@ -- internally simplifies expressions to sum-of-products form, so complex -- expressions are valid as long as each simplified product has at most -- one variable. --- The library currently cannot create a set or relation if any --- integer expressions contain quantifiers, but this restriction could be --- lifted in the future. expToFormula :: [VarHandle] -- ^ Free variables -> BoolExp -- ^ Expression to convert @@ -871,12 +1000,12 @@ -> ([Coefficient], Int) sumToConstraint freeVars expr = case deconstructSum expr - of (constant, terms) -> (map deconstructTerm terms, constant) + of Term constant terms -> (map deconstructTerm terms, constant) where deconstructTerm :: IntExpr -> Coefficient deconstructTerm expr = case deconstructProduct expr - of (n, [VarE (Bound i)]) -> Coefficient (lookupVar i freeVars) n + of Term n [VarE (Bound i)] -> Coefficient (lookupVar i freeVars) n _ -> expToFormulaError "expression is non-affine" expToFormulaError :: String -> a @@ -955,4 +1084,4 @@ check' (VarE (Quantified _)) = quantifiedVar check' (QuantE _ e) = check (n+1) e - quantifiedVar = error "Unexpected quantified variable" + quantifiedVar = error "variablesWithinRange: unexpected variable" diff --git a/Omega.cabal b/Omega.cabal --- a/Omega.cabal +++ b/Omega.cabal @@ -1,6 +1,6 @@ Cabal-Version: >= 1.2.3 && < 1.8 Name: Omega -Version: 0.1.3 +Version: 0.2.0 Build-Type: Custom License: BSD3 License-File: LICENSE @@ -19,6 +19,8 @@ aclocal.m4 configure.ac Makefile.in + src/C_omega.cc + src/C_omega.h src/the-omega-project.tar.gz Extra-Tmp-Files: build/C_omega.o diff --git a/Setup.hs b/Setup.hs --- a/Setup.hs +++ b/Setup.hs @@ -31,6 +31,7 @@ writeUseInstalledOmegaFlag :: Bool -> IO () writeUseInstalledOmegaFlag b = do + createDirectoryIfMissing False "build" writeFile useInstalledOmegaFlagPath (show b) readUseInstalledOmegaFlag :: IO Bool diff --git a/src/C_omega.cc b/src/C_omega.cc new file mode 100644 --- /dev/null +++ b/src/C_omega.cc @@ -0,0 +1,535 @@ + +#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 new file mode 100644 --- /dev/null +++ b/src/C_omega.h @@ -0,0 +1,115 @@ + +#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