Omega 0.1.3 → 0.2.0
raw patch · 5 files changed
+849/−67 lines, 5 filessetup-changed
Files
- Data/Presburger/Omega/Expr.hs +195/−66
- Omega.cabal +3/−1
- Setup.hs +1/−0
- src/C_omega.cc +535/−0
- src/C_omega.h +115/−0
Data/Presburger/Omega/Expr.hs view
@@ -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"
Omega.cabal view
@@ -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
Setup.hs view
@@ -31,6 +31,7 @@ writeUseInstalledOmegaFlag :: Bool -> IO () writeUseInstalledOmegaFlag b = do+ createDirectoryIfMissing False "build" writeFile useInstalledOmegaFlagPath (show b) readUseInstalledOmegaFlag :: IO Bool
+ src/C_omega.cc view
@@ -0,0 +1,535 @@++#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 view
@@ -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