_*      !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNO P Q R S T U V W X Y Z [ \ ] ^ _ ` a b c d e f g h i j k l m n o p q r s t u v w x y z { | } ~        !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~ !!!"""#$$$$$$$$$$%%%%%%%%%%%%%&'''''''''''''''''''''''''''''''''''''''''''''''''''''''''''''''''''''''''''(((((( ( ) ) ) ))))))))))***+,---- -!-"-#.$/%0&0'0(0)0*0+0,0-0.0/000102030405060708090:0;0<0=0>0?0@0A0B0C0D1E1F1G1H1I1J1K1L1M2N2O2P2Q2R2S2T2U2V2W2X2Y3Z3[3\3]3^3_3`3a3b3c3d3e3f3g3h3i3j3k3l3m3n3o3p3q3r3s3t3u3v3w3x3y3z3{3|4}4~444444444555566777777777778888888888889:::;;;;;;;;;;;;;;;<<<<<<<<=========>>>>??????@@@@@@@@@@@@@@@AABCDEEEEEEFFFFFFFFFGGGGGGGGGGHHHIIIIIII I I I I IJJJJJJJJJJJJJJJJJJ J!J"J#J$K%K&K'K(K)K*K+K,K-K.K/K0K1K2K3K4K5K6K7K8K9K:K;K<K=K>K?K@KALBLCLDLELFLGLHLILJLKLLLMLNLOLPLQLRLSLTLUMVMWMXMYMZM[M\M]M^M_M`MaMbMcMdMeMfNgNhNiNjNkNlNmOnOoOpOqOrOsOtOuOvOwOxOyOzO{P|P}P~PQQQQQQQQQQQQQQQQQQQQQQRSSSTTTTTTTTTTTTTTTTUUVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVWWWWWWWWWWXXXXXXXXYYYYYYYYYZZZ[[[[[[[\]]^ ^ _ _ _ __________________` `!`"`#`$`%`&`'a(a)aib Safe-Inferred *+,-./012345012345 *+,-./012345 Safe-Inferred(c) Masahiro Sakai 2014 BSD-stylemasahiro.sakai@gmail.com provisionalnon-portable (FlexibleContexts)None366(c) Masahiro Sakai 2012 BSD-stylemasahiro.sakai@gmail.com provisionalportable Safe-Inferred (the block strcuture vector (bLOCKsTRUCT)Constant Vector Constraint Matrices!%the number of primal variables (mDim)"the number of blocks (nBLOCK)'"Parse a SDPA format (.dat) string.( Parse a SDPA format file (.dat).)+Parse a SDPA sparse format (.dat-s) string.*)Parse a SDPA sparse format file (.dat-s).& !"#$%&'()*789:;<=>?@AB+,CDEFG !"#$%&'()*+, !"#%$&+,'()*" !"#$%&'()*789:;<=>?@AB+,CDEFG Safe-Inferred-.-.-.-.(c) Masahiro Sakai 2012-2014 BSD-stylemasahiro.sakai@gmail.com provisionalnon-portable (BangPatterns) Safe-Inferred0H allocate too many intermediate I. Therefore we use this optimized implementation instead. Many intermediate values in this implementation will be optimized away by worker-wrapper transformation and unboxing./J0/0/0/J0(c) Masahiro Sakai 2014 BSD-stylemasahiro.sakai@gmail.com provisionalBnon-portable (BangPatterns, FlexibleContexts, ScopedTypeVariables)None3M6%Get the internal representation arrayB%Get the internal representation arrayC%Get the internal representation arrayD!Pre-allocate internal buffer for n elements.1234K56789:;<=>?@ABCDLM123456789:;<=>?@ABCD43215A6789:;<=>?@BCD1234K56789:;<=>?@ABCDLM(c) Masahiro Sakai 2012 BSD-stylemasahiro.sakai@gmail.com provisionalEnon-portable (MultiParamTypeClasses, FlexibleInstances, BangPatterns)None246 E6Priority queue implemented as array-based binary heap.G7Build a priority queue with default ordering ('(<)' of N class)H$Build a priority queue with a given  less than operator.ICReturn a list of all the elements of a priority queue. (not sorted)J*Remove all elements from a priority queue.K"Create a copy of a priority queue.L:Get the internal representation of a given priority queue.M:Get the internal representation of a given priority queue.N!Pre-allocate internal buffer for n elements.EOPQFGHIJKRSLMNTUVWXYZ EFGHIJKLMNEFGHIJK  LMNEOPQFGHIJKRSLMNTUVWXYZ (c) Masahiro Sakai 2012 BSD-stylemasahiro.sakai@gmail.com provisional7non-portable (FlexibleInstances, MultiParamTypeClasses) Safe-Inferred246O[P\]^_  OP O  PO[P\]^_ (c) Masahiro Sakai 2012 BSD-stylemasahiro.sakai@gmail.com provisional[non-portable (MultiParamTypeClasses, FlexibleInstances, BangPatterns, TypeSynonymInstances)None246; Q6Priority queue implemented as array-based binary heap.T7Build a priority queue with default ordering ('(<)' of N class)U$Build a priority queue with a given  less than operator.`$Build a priority queue with a given  less than operator.VCReturn a list of all the elements of a priority queue. (not sorted)W*Remove all elements from a priority queue.X"Create a copy of a priority queue.[:Get the internal representation of a given priority queue.\:Get the internal representation of a given priority queue.]!Pre-allocate internal buffer for n elements.^!Pre-allocate internal buffer for [0..n-1] values.QabcdRSTU`eVWXYZfg[\]^hijklmn QRSTUVWXYZ[\]^QRSTUVWX  YZ[\]^QabcdRSTU`eVWXYZfg[\]^hijklmnc(c) Masahiro Sakai 2012-2013 BSD-stylemasahiro.sakai@gmail.com provisionalnon-portable (ScopedTypeVariables, FlexibleInstances, MultiParamTypeClasses, FunctionalDependencies, TypeFamilies, BangPatterns, DeriveDataTypeable, CPP)None +2468=KM/aMonic monomialse Variable "x"g.Univariate polynomials over commutative ring rs(Square-free factorization of polynomialstfactor a polynomial p into p1 ^ n1 * p2 ^ n2 * .. and return a list [(p1,n1), (p2,n2), ..].u"Prime factorization of polynomialsvfactor a polynomial p into p1 ^ n1 * p2 ^ n2 * .. and return a list [(p1,n1), (p2,n2), ..].xContent of a polynomial yPrimitive part of a polynomialz"Polynomial over commutative ring r|"total degree of a given polynomial&construct a polynomial from a constant+construct a polynomial from a list of terms*construct a polynomial from a singlet term list of terms3leading term with respect to a given monomial order:leading coefficient with respect to a given monomial order7leading monomial with respect to a given monomial orderPLook up a coefficient for a given monomial. If no such term exists, it returns 0.PLook up a coefficient for a given monomial. If no such term exists, it returns Nothing.Ya polynomial is called primitive if the greatest common divisor of its coefficients is 1. Formal derivative of polynomialsFormal integral of polynomials EvaluationSubstitution or bind"Transform polynomial coefficients.XTransform a polynomial into a monic polynomial with respect to the given monomial order.Convert  K[x,x1,x2, &] into  K[x1,x2, &][x].Multivariate division algorithmdivModMP cmp f [g1,g2,..] returns a pair  ([q1,q2, &],r) such thatf = g1*q1 + g2*q2 + .. + r and g1, g2, .. do not divide r.Multivariate division algorithm )reduce cmp f gs = snd (divModMP cmp f gs)Natural ordering x^0 < x^1 < x^2 ..: is the unique monomial order for univariate polynomials."division of univariate polynomials"division of univariate polynomials"division of univariate polynomialsGCD of univariate polynomialsLCM of univariate polynomialsExtended GCD algorithmpseudo divisionpseudo quotientpseudo reminderGCD of univariate polynomials'Is the number a root of the polynomial?Is the polynomial square free?Lexicographic orderReverse lexicographic order.Note that revlex is NOT a monomial order.Graded lexicographic order"Graded reverse lexicographic order_`aobcdefghijklmnopqrstuvwxyzp{|}~qrstuvwxyz{|}~__`abcdefghijklmnopqrstuvwxyz{|}~{_`aobcdefghijklmnopqrstuvwxyzp{|}~qrstuvwxyz{|}~ (c) Masahiro Sakai 2013-2014 BSD-stylemasahiro.sakai@gmail.com provisional0non-portable (ScopedTypeVariables, BangPatterns)NoneMd(c) Masahiro Sakai 2013-2014 BSD-stylemasahiro.sakai@gmail.com provisionalportableNone (c) Masahiro Sakai 2013 BSD-stylemasahiro.sakai@gmail.com provisionalDnon-portable (BangPatterns, TypeSynonymInstances, FlexibleInstances)None24USquare-free decomposition of univariate polynomials over a field of characteristic 0.(c) Masahiro Sakai 2011-2014 BSD-stylemasahiro.sakai@gmail.com provisionalportableNone&SOS (special ordered sets) constraints/types of SOS (special ordered sets) constraintsType 2 SOS constraintType 1 SOS constraintrelational operators4type for representing lower/upper bound of variablesvariablelabel4type for representing lower/upper bound of variables constraintobjective functionterms expressionsProblemdefault boundsdefault lower bound (0)default upper bound (+") convert a string into a variable convert a variable into a string$looking up attributes for a variable looking up bounds for a variable looking up bounds for a variableEAA'(c) Masahiro Sakai 2012-2014 BSD-stylemasahiro.sakai@gmail.com provisionalportableNonewParse a string containing MPS file data. The source name is only | used in error messages and may be the empty string.&Parse a file containing MPS file data.MPS file parser;0 (c) Masahiro Sakai 2012 BSD-stylemasahiro.sakai@gmail.com provisionalportable Safe-Inferred&Lifted Bool type. It has three values , , .lifted true valuelifted false valueundefined truth value F lnot lTrue == lFalse lnot lFalse == lTrue lnot lUndef == lUndef  4 liftBool True == lTrue liftBool False == lFalse  a unliftBool lTrue == Just True unliftBool lFalse == Just False unliftBool lUndef == Nothing (c) Masahiro Sakai 2011 BSD-stylemasahiro.sakai@gmail.comnon-portable (BangPatterns) Safe-Inferred*Variable are repserented positive integer.XPositive (resp. negative) literal is represented as a positive (resp. negative) integer. )List of variables interpreted as products Coefficient and   Sum of    A pair of weight and constraint.  A pair of top cost and a list of soft constraints.Relational operatorsequalgreater than or equal!Lhs, relational operator and rhs.Pair of objective function and a list of constraints.4Parse a .opb file containing pseudo boolean problem.=Parse a .opb format string containing pseudo boolean problem.CParse a .wbo file containing weighted boolean optimization problem. LParse a .wbo format string containing weighted boolean optimization problem.?      !"      !"      !"3      !"(c) Masahiro Sakai 2013-2014 BSD-stylemasahiro.sakai@gmail.com experimentalportable Safe-Inferred#$     #$#$#$     (c) Masahiro Sakai 2013 BSD-stylemasahiro.sakai@gmail.com experimentalportable Safe-Inferred%%%%(c) Masahiro Sakai 2013 BSD-stylemasahiro.sakai@gmail.com experimentalportable Safe-Inferred&&&&(c) Masahiro Sakai 2013 BSD-stylemasahiro.sakai@gmail.com experimentalportable Safe-Inferred'''' Safe-Inferred24( XOR clause.'([l1,l2..ln], b)' means l1 " l2 " " " ln = b. Note that:&True can be represented as ([], False)&False can be represented as ([], True).Disjunction of 1.1kPositive (resp. negative) literals are represented as positive (resp. negative) integers. (DIMACS format).2AA model is represented as a mapping from variables to its values.7=Variable is represented as positive integers (DIMACS format).;7Construct a literal from a variable and its polarity.  (resp *) means positive (resp. negative) literal.<Negation of the 1.=Underlying variable of the 1>Polarity of the 1.  means positive literal and  means negative literal.@Normalizing clause! if the clause is trivially true.F normalizing PB term of the form c1 x1 + c2 x2 ... cn xn + c into d1 x1 + d2 x2 ... dm xm + d where d1,...,dm "e 1.G&normalizing PB constraint of the form c1 x1 + c2 cn ... cn xn >= b.H&normalizing PB constraint of the form c1 x1 + c2 cn ... cn xn = b.RNormalize XOR clause/()*+,-./0123456789:;variablepolarity<=>?@ABCDEFGHIJKLMNOPQRS,()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRS,765834210/9:;<=>?.@ABC-DE,+*)FGHIJKLMNOPQ(RS.()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRS(c) Masahiro Sakai 2013 BSD-stylemasahiro.sakai@gmail.com experimentalportable Safe-InferredTTTT(c) Masahiro Sakai 2012-2014 BSD-stylemasahiro.sakai@gmail.com provisionalportable Safe-InferredU!Maximal Satisfiable Subset (MSS).~A subset S " C is an MSS if S is satisfiable and "C_i " U\S, S"*{C_i} is unsatisfiable [CAMUS]. A MSS is the complement of an W.VSatisfiable Subset (SS).IA subset S " C is a SS if S is satisfiable. A SS is the complement of a X.W/Minimal Correction Subset of constraints (MCS).A subset M " C is an MCS if C\M is satisfiable and "C_i " M, C\(M\{C_i}) is unsatisfiable [CAMUS]. A MCS is the complement of an U and also known as a CoMSS.X&Correction Subset of constraints (CS).KA subset M " C is a CS if C\M is satisfiable. A CS is the complement of a V.Y2Minimal Unsatisfiable Subset of constraints (MUS).]A subset U " C is an MUS if U is unsatisfiable and "C_i " U, U\{C_i} is satisfiable [CAMUS]. Z)Unsatisfiable Subset of constraints (US)./A subset U " C is an US if U is unsatisfiable. UVWXYZUVWXYZZYXWVUUVWXYZ Safe-Inferred$[\]^_`abcdefghijklmnop ![\]^_`abcdefghijklmnop]^_`abcdefghijk\lmno[p[\]^_`abcdefghijklmnop ! Safe-Inferredqrstuvwxqrstuvwxqrstuvwxqrstuvwx(c) Masahiro Sakai 2012 BSD-stylemasahiro.sakai@gmail.com provisionalportable Safe-InferredyPrint a 2. in a way specified for SAT Competition. See  ,http://www.satcompetition.org/2011/rules.pdf for details.zPrint a 21 in a way specified for Max-SAT Evaluation. See  &http://maxsat.ia.udl.cat/requirements/ for details.{Print a 29 in a way specified for Pseudo-Boolean Competition. See  .http://www.cril.univ-artois.fr/PB12/format.pdf for details.yz{|"yz{|yz{|yz{|"(c) Masahiro Sakai 2012 BSD-stylemasahiro.sakai@gmail.com provisionalportable Safe-Inferred}~#$%& }~ ~} }~#$%&(c) Masahiro Sakai 2012 BSD-stylemasahiro.sakai@gmail.com provisionalportable Safe-InferredBWeigths must be greater than or equal to 1, and smaller than 2^63.'()*+,-.  '()*+,-.(c) Masahiro Sakai 2013 BSD-stylemasahiro.sakai@gmail.com experimentalportable Safe-Inferred(c) Masahiro Sakai 2013 BSD-stylemasahiro.sakai@gmail.com experimentalportable Safe-Inferred(c) Masahiro Sakai 2011-2012 BSD-stylemasahiro.sakai@gmail.com experimentalportable Safe-Inferred (c) Masahiro Sakai 2013 BSD-stylemasahiro.sakai@gmail.com experimentalportable Safe-Inferred//!(c) Masahiro Sakai 2014 BSD-stylemasahiro.sakai@gmail.com provisionalportable Safe-Inferred0101"(c) Masahiro Sakai 2014 BSD-stylemasahiro.sakai@gmail.com provisionalportable Safe-InferredM#(c) Masahiro Sakai 2014 BSD-stylemasahiro.sakai@gmail.com provisionalnon-portable (CPP) Safe-Inferred Filename of the executable (see 2 for details) any argumentsstandard inputAcallback function which is called when a line is read from stdoutAcallback function which is called when a line is read from stderr3434$(c) Masahiro Sakai 2014 BSD-stylemasahiro.sakai@gmail.com provisional!non-portable (DeriveDataTypeable) Safe-Inferred+56789:   56789:%(c) Masahiro Sakai 2014 BSD-stylemasahiro.sakai@gmail.com provisional!non-portable (DeriveDataTypeable) Safe-Inferred+;<=>?@A   ;<=>?@A&(c) Masahiro Sakai 2012-2014 BSD-stylemasahiro.sakai@gmail.com provisionalportable Safe-InferredMBCDEFGBCDEFG'(c) Masahiro Sakai 2012-2014 BSD-stylemasahiro.sakai@gmail.com provisionalVnon-portable (BangPatterns, ScopedTypeVariables, CPP, DeriveDataTypeable, RecursiveDo)None+;CM>HAinvoked with the watched literal when the literal is falsified. watch 0g  toConstraint+ 0T|0sQ0W0f heap allocation 0Lvzu0Y00n0 0Q00_00k0QC0n I 0n!0W0f0J0O0Jdeduce a clause C"(l from the constraint and return C. C and l should be false and true respectively under the current assignment.Solver instanceKAInverse of the variable activity decay factor. (default 1 / 0.95)L"Amount to bump next variable with.M<Inverse of the constraint activity decay factor. (1 / 0.999)N$Amount to bump next constraint with.O(The initial restart limit. (default 100)PTThe factor with which the restart limit is multiplied in each restart. (default 1.5)Q)The initial limit for learnt constraints.R[The limit for learnt constraints is multiplied with this factor periodically. (default 1.1)SHControls conflict constraint minimization (0=none, 1=local, 2=recursive)T.will be invoked when this literal is falsifiedU-will be invoked when the variable is assignedVFRegister the constraint to be notified when the literal becames false.WERegister the constraint to be notified when the variable is assigned.X:Returns list of constraints that are watching the literal.#number of variables of the problem.number of assigned variables.number of constraints.number of learnt constrints.Create a new Solver instance.Add a new variableAdd variables. /newVars solver n = replicateM n (newVar solver)Add variables. 1newVars_ solver n = newVars solver n >> return ()!Pre-allocate internal buffer for n variables.Add a clause to the solver.Add a cardinality constraints atleast({l1,l2,..},n).Add a cardinality constraints atmost({l1,l2,..},n).Add a cardinality constraints exactly({l1,l2,..},n).!Add a pseudo boolean constraints c1*l1 + c2*l2 + & "e n.!Add a pseudo boolean constraints c1*l1 + c2*l2 + & "d n.!Add a pseudo boolean constraints c1*l1 + c2*l2 + & = n.&Add a soft pseudo boolean constraints lit ! c1*l1 + c2*l2 + & "e n.&Add a soft pseudo boolean constraints lit ! c1*l1 + c2*l2 + & "d n.&Add a soft pseudo boolean constraints lit ! c1*l1 + c2*l2 + & = n.Add a parity constraint l1 " l2 " & " ln = rhsAdd a soft parity constraint lit ! l1 " l2 " & " ln = rhsSolve constraints. Returns ) if the problem is SATISFIABLE. Returns ! if the problem is UNSATISFIABLE.-Solve constraints under assuptions. Returns ) if the problem is SATISFIABLE. Returns ! if the problem is UNSATISFIABLE.After 3 returns True, it returns an satisfying assignment.After  returns False, it returns a set of assumptions that leads to contradiction. In particular, if it returns an empty set, the problem is unsatisiable without any assumptions.YNSimplify the constraint database according to the current top-level assigment.default value for RestartStrategy.TThe initial restart limit. (default 100) Negative value is used to disable restart.default value for  RestartFirst.TThe factor with which the restart limit is multiplied in each restart. (default 1.5)default value for  RestartInc.%The initial limit for learnt clauses.default value for LearntSizeFirst.WThe limit for learnt clauses is multiplied with this factor each restart. (default 1.1)default value for  LearntSizeInc.WThe limit for learnt clauses is multiplied with this factor each restart. (default 1.1)default value for CCMin.#The default polarity of a variable.QThe frequency with which the decision heuristic tries to choose a random variable:Set random generator used by the random variable selection:Get random generator used by the random variable selectionZ?Revert to the state at given level (keeping all assignment at level but not beyond).[?invoked with the watched literal when the literal is falsified.\deduce a clause C"(l from the constraint and return C. C and l should be false and true respectively under the current assignment.-set callback function for receiving messages.@]^_`abcdefghijklmnopqrstuvwxyz{|}~IHJKLMNOPQRSTUVWXThe  argument.set of literals  {l1,l2,..}" (duplicated elements are ignored)n.The  argumentset of literals  {l1,l2,..}" (duplicated elements are ignored)nThe  argumentset of literals  {l1,l2,..}" (duplicated elements are ignored)nThe  argument. set of terms [(c1,l1),(c2,l2), &]nThe  argument.list of [(c1,l1),(c2,l2), &]nThe  argument.list of terms [(c1,l1),(c2,l2), &]nThe  argument. indicator lit set of terms [(c1,l1),(c2,l2), &]nThe  argument. indicator lit set of terms [(c1,l1),(c2,l2), &]nThe  argument. indicator lit set of terms [(c1,l1),(c2,l2), &]nThe  argument. literals [l1, l2, &, ln]rhsThe  argument. indicator lit literals [l1, l2, &, ln]rhs AssumptionsYZ[\      !"#$%&'()*+,-./0123456789:;<S.127;<=>S71;<=>.2]^_`abcdefghijklmnopqrstuvwxyz{|}~IHJ-KLMNOPQRSTUVWXYZ[\      !"#$%&'()*+,-./0123456789:;<((c) Masahiro Sakai 2012 BSD-stylemasahiro.sakai@gmail.com provisional non-portableNone Options for   functiondefault  value dFind a minimal set of assumptions that causes a conflict. Initial set of assumptions is taken from . = UVWXYZ   =)(c) Masahiro Sakai 2012-2014 BSD-stylemasahiro.sakai@gmail.com provisionalportableNone  Options for , , `MCS candidates (see HYCAM paper for details). A MCS candidate must be a superset of a real MCS.default   value    >UVWXYZ             >*(c) Masahiro Sakai 2014 BSD-stylemasahiro.sakai@gmail.com provisionalportableNoneUVWXYZ         +(c) Masahiro Sakai 2014 BSD-stylemasahiro.sakai@gmail.com provisionalportableNone??,(c) Masahiro Sakai 2014 BSD-stylemasahiro.sakai@gmail.com provisionalportableNone @ABCDEFG@ABCDEFG-(c) Masahiro Sakai 2014 BSD-stylemasahiro.sakai@gmail.com provisionalportableNoneH"The smallest integer greater than n- that can be obtained by summing a subset of ws.IJKL !"MH ws nN !" !"IJKL !"MHN.(c) Masahiro Sakai 2013 BSD-stylemasahiro.sakai@gmail.com provisionalnon-portable (BangPatterns)None#O###O/(c) Masahiro Sakai 2013 BSD-stylemasahiro.sakai@gmail.com provisionalportableNone$P$$$P0(c) Masahiro Sakai 2012-2013 BSD-stylemasahiro.sakai@gmail.com provisionalportableNone*%QRSTUV&'()*+,-./0123456789:;<=>?@ABCWXYZ[%&'()*+,-./0123456789:;<=>?@ABC%01=>?@ABC&.-,+*)('/23456789:;<%QRSTUV&.-,+*)('/0123456789:;<=>?@ABCWXYZ[1(c) Masahiro Sakai 2012 BSD-stylemasahiro.sakai@gmail.com provisionalportable Safe-InferredD\]^_`abcdEFGHIJKeLfghij DEFGHIJKL DHEGFIJKLD\]^_`abcdEGFHIJKeLfghij2(c) Masahiro Sakai 2012-2014 BSD-stylemasahiro.sakai@gmail.com provisionalportable Safe-InferredM3types that can be combined with boolean operations.Ptypes that can be negated.MNOPQRSTUVWXklmnopqrs MNOPQRSTUVWX RSTUVWXPQMNO MNOPQRSTUVWXklmnopqrsNOUV3(c) Masahiro Sakai 2012 BSD-stylemasahiro.sakai@gmail.com provisionalKnon-portable (TypeSynonymInstances, FlexibleInstances, ScopedTypeVariables)None24M ^Element of model.t Shallow atomu Shallow termoTermr3Generalized literal type parameterized by atom typeuPredicate SymbolvFunction SymbolwVariablex.normalize a formula into a skolem normal form.TODO:Tseitin encodingy print entityLYZ[\]vwxyz^{|}~tu_`abcdefghijklmnopqrstuvwxyz{#YZ[\]^_`abcdefghijklmnopqrstuvwxyz{#wvurtsoqpmnlkj_ihgfedcba`xYZ[\]^zy{4YZ[\]vwxyz^{|}~tu_ ihgfedcba`jklmnoqprtsuvwxyz{4(c) Masahiro Sakai 2012-2013 BSD-stylemasahiro.sakai@gmail.com provisional"non-portable (ScopedTypeVariables)NoneM}$sugar strategy (not implemented yet)|}~ |}~ |~} |~}5(c) Masahiro Sakai 2012-2013 BSD-stylemasahiro.sakai@gmail.com provisionalYnon-portable (ScopedTypeVariables, BangPatterns, TypeSynonymInstances, FlexibleInstances)None24MHSquare-free decomposition of univariate polynomials over a finite field.1Berlekamp algorithm for polynomial factorization.8Input polynomial is assumed to be monic and square-free.6(c) Masahiro Sakai 2012-2013 BSD-stylemasahiro.sakai@gmail.com provisional0non-portable (BangPatterns, ScopedTypeVariables)NoneMf|^2e(c) Masahiro Sakai 2012-2013 BSD-stylemasahiro.sakai@gmail.com provisional6non-portable (TypeSynonymInstances, FlexibleInstances)None24fNone24 (c) Masahiro Sakai 2012-2013 BSD-stylemasahiro.sakai@gmail.com provisionalportableNone__`abcdefghijklmnopqrstuvwxyz{|}~az{{|}~uvstwxygefc`dabb_mnopqrjklhi7(c) Masahiro Sakai 2012 BSD-stylemasahiro.sakai@gmail.com provisionalnon-portable (Rank2Types)NoneHM    8(c) Masahiro Sakai 2012 BSD-stylemasahiro.sakai@gmail.com provisionalportableNone Sturm's chain (Sturm's sequence) Sturm's sequence of a polynomial%The number of distinct real roots of p in a given interval%The number of distinct real roots of p+ in a given interval. This function takes p's sturm chain instead of p itself.KClosed interval that contains all real roots of a given polynomial. h90nPuL =http://aozoragakuen.sakura.ne.jp/taiwa/taiwaNch02/node26.htmlYDisjoint intervals each of which contains exactly one real roots of the given polynoimal p,. The intervals can be further narrowed by  or .YDisjoint intervals each of which contains exactly one real roots of the given polynoimal p,. The intervals can be further narrowed by  or . This function takes p's sturm chain instead of p itself.  9Noneg(c) Masahiro Sakai 2012 BSD-stylemasahiro.sakai@gmail.com provisionalportableNone:(c) Masahiro Sakai 2011-2013 BSD-stylemasahiro.sakai@gmail.com provisionalportable Safe-InferredDisjunctive normal formlist of conjunction of literals;(c) Masahiro Sakai 2012-2013 BSD-stylemasahiro.sakai@gmail.com provisionalnon-portable (Rank2Types)NoneHMAlgebraic real numbers.0Real roots of the polynomial in ascending order.0Real roots of the polynomial in ascending order.-Returns approximate rational value such that %abs (a - approx a epsilon) <= epsilon.'Returns approximate interval such that +width (approxInterval a epsilon) <= epsilon.Same as .Same as .Same as .Same as .Same as .The n th root of a9Same algebraic real, but represented using finer grained .5The polynomial of which the algebraic number is root.@Isolating interval that separate the number from other roots of  of it.+Whether the algebraic number is a rational.kWhether the algebraic number is a root of a polynomial with integer coefficients with leading coefficient 1 (a monic polynomial).Height of the algebraic number.The height of an algebraic number is the greatest absolute value of the coefficients of the irreducible and primitive polynomial with integral rational coefficients.root index, satisfying  ( a) !! rootIndex a == a  Golden ratio Degree of the algebraic number.If the algebraic number's  has degree n2, then the algebraic number is said to be degree n.&aepsilonaepsilon%<(c) Masahiro Sakai 2011-2012 BSD-stylemasahiro.sakai@gmail.com provisionalportable Safe-InferredCombining two Maybe values using given function.is the number integral? , isInteger x = fromInteger (round x) == x fractional part ) fracPart x = x - fromInteger (floor x) =(c) Masahiro Sakai 2011-2013 BSD-stylemasahiro.sakai@gmail.com provisionalnon-portable (TypeFamilies)None=K Delta r k: represents r + k for symbolic infinitesimal parameter .#symbolic infinitesimal parameter .Conversion from a base r value to Delta r.Extracts the real part..Extracts the  part.. version of .  x/ returns the greatest integer not greater than x version of .  x) returns the least integer not less than xIs this a integer?    >(c) Masahiro Sakai 2011-2014 BSD-stylemasahiro.sakai@gmail.com provisionalportableNonevParse a string containing LP file data. The source name is only | used in error messages and may be the empty string.%Parse a file containing LP file data.LP file parserRender a problem into a string.8     8     ?(c) Masahiro Sakai 2011-2014 BSD-stylemasahiro.sakai@gmail.com provisionalportableNone.Parse .lp or .mps file based on file extension%Parse a file containing LP file data.&Parse a file containing MPS file data.G@(c) Masahiro Sakai 2012-2014 BSD-stylemasahiro.sakai@gmail.com experimentalportableNone( !"#$%&'()*+ !"#$%&'()*+A(c) Masahiro Sakai 2011-2014 BSD-stylemasahiro.sakai@gmail.com experimentalportableNone,-./0,-./0B(c) Masahiro Sakai 2011-2014 BSD-stylemasahiro.sakai@gmail.com experimentalportableNoneC(c) Masahiro Sakai 2011-2014 BSD-stylemasahiro.sakai@gmail.com experimentalportableNoneD(c) Masahiro Sakai 2012-2013 BSD-stylemasahiro.sakai@gmail.com provisionalnon-portable (BangPatterns)None 123456789 123456789E(c) Masahiro Sakai 2011-2013 BSD-stylemasahiro.sakai@gmail.com provisionalportable Safe-InferredA Model# is a map from variables to values.collecting free variablesMap from variablesSet of variables2Variables are represented as non-negative integers::F(c) Masahiro Sakai 2014 BSD-stylemasahiro.sakai@gmail.com provisionalportableNone+-Boolean expression over a given type of atoms;<=>?@ABCDEFGHIJKLM  ;<=>?@ABCDEFGHIJKLMG(c) Masahiro Sakai 2012 BSD-stylemasahiro.sakai@gmail.com provisionalportableNoneEncoder instance'Arbitrary formula not restricted to CNF Create a Encoder instance.Use pseudo boolean constraints or use only clauses.KAssert a given formula to underlying SAT solver by using Tseitin encoding.=Return an literal which is equivalent to a given conjunction.=Return an literal which is equivalent to a given disjunction.NOPQRS   NOPQRSHNoneTUTUI(c) Masahiro Sakai 2011-2013 BSD-stylemasahiro.sakai@gmail.com provisionalportable Safe-Inferredformulas of first order logic +convert a formula into negation normal form     VWXYMNOPQRSTUVWX                VWXYJ(c) Masahiro Sakai 2011 BSD-stylemasahiro.sakai@gmail.com provisionalOnon-portable (FlexibleInstances, MultiParamTypeClasses, FunctionalDependencies) Safe-Inferred2468 Atomic formula.type class for constructing relational formularelational operatorsflipping relational operatorrel (flipOp op) a b is equivalent to  rel op b anegating relational operatorrel (negOp op) a b is equivalent to notB (rel op a b)operator symbol0evaluate an operator into a comparision functionconstructing relational formulaconstructing relational formulaconstructing relational formula constructing relational formula!constructing relational formula"constructing relational formula !"#Z[\] !"## !" !"#Z[\] !"K(c) Masahiro Sakai 2011 BSD-stylemasahiro.sakai@gmail.com provisionalnon-portable (TypeFamilies)None=K%$Atomic Formula of Linear Arithmetics&nLinear combination of variables and constants. Non-negative keys are used for variables's coefficients. key + is used for constants.'(a mapping from variables to coefficients( Create a Expr/ from a mapping from variables to coefficients.)"terms contained in the expression.* Create a Expr from a list of terms.+6Special variable that should always be evaluated to 1.-variable.constant/map coefficients.0map coefficients.1(evaluate the expression under the model.2(evaluate the expression under the model.5applySubst1 x e e1 == e1[e/x]6'lookup a coefficient of the variable. $ coeff v e == fst (extract v e) 72lookup a coefficient of the variable. It returns Nothing$ if the expression does not contain v. 4 lookupCoeff v e == fmap fst (extractMaybe v e) 8 extract v e returns (c, e') such that e == c *^ v ^+^ e'9extractMaybe v e returns  Just (c, e') such that e == c *^ v ^+^ e' if e contains v, and returns Nothing otherwise.<%evaluate the formula under the model.>applySubst1 x e phi == phi[e/x]?1Solve linear (in)equation for the given variable. solveFor a v returns  Just (op, e) such that  Atom v op e is equivalent to a.@compute bounds for a Expr with respect to  BoundsEnv.'$%&^'()*+,_-./0`123456789:a;<=>?@bcdefg3 !"#$%&'()*+,-./0123456789:;<=>?@&'-.)*'(+,6789/012345:%;<=>?$@%$%&^'()*+,_-./0`123456789:a;<=>?@bcdefgL(c) Masahiro Sakai 2011 BSD-stylemasahiro.sakai@gmail.com provisional"non-portable (ScopedTypeVariables)NoneMBNon-basic variablesCBasic variablesHLookup a row by basic variable$hijklmnoABCDEFGHpqIJrKLMNOsPtQuRvSwTABCDEFGHIJKLMNOPQRSTDCBAEFGHIJKLNOPQRSMThkjilonmABCDEFGHpqIJrKLMNOsPtQuRvSwTM(c) Masahiro Sakai 2012 BSD-stylemasahiro.sakai@gmail.com provisional0non-portable (ScopedTypeVariables, BangPatterns)NoneMBUxyz{VWXYZ[\|}~]^_`abcdeUVWXYZ[\]^_`abcdeY\[ZVXWa]bcdeU^_`=Uxyz{VXWY\[Z|}~]^_`abcdeN(c) Masahiro Sakai 2013 BSD-stylemasahiro.sakai@gmail.com provisionalportableNonef&Complex numbers are an algebraic type.For a complex number z,  z# is a number with the magnitude of z8, but oriented in the positive real direction, whereas  z has the phase of z, but unit magnitude.h+Extracts the real part of a complex number.i0Extracts the imaginary part of a complex number.j"The conjugate of a complex number.k.The nonnegative magnitude of a complex number.l5The polynomial of which the algebraic number is root.Roots of the polynomialfghijklfghijklfghikljfghijklgO(c) Masahiro Sakai 2011-2013 BSD-stylemasahiro.sakai@gmail.com provisional7non-portable (FlexibleInstances, MultiParamTypeClasses) Safe-Inferred246m"results of satisfiability checkingqAtomic formularArithmetic expressionsxsingle variable expressiony evaluate an r with respect to a mnopqrstuvwxyz<MNOPQRSTUVWX      !"#mnopqrstuvwxyzrwvutsxyqzmpon mponqrwvutsxyzPNone{|}~{|}~{|}~{|}~Q(c) Masahiro Sakai 2011-2013 BSD-stylemasahiro.sakai@gmail.com provisionalportableNone Atomic constrainte = 0e > 0e "e 0'(t,c) represents t/c, and c must be >0.Simplify conjunction of s. It returns " when a inconsistency is detected. x  returns ![(_1, lift_1), &, (_m, lift_m)] such that:+"_LRA "y1, &, yn. ("x. ) ! (_1 "( & "( _m) where {y1, &, yn} = FV() \ {x}, andif  M "_LRA _i then lift_i M "_LRA . {x1, &,xm}  returns ![(_1, lift_1), &, (_n, lift_n)] such that:+"_LRA "y1, &, yp. ("x. ) ! (_1 "( & "( _n) where {y1, &, yp} = FV() \ {x1, &,xm}, andif  M "_LRA _i then lift_i M "_LRA . {x1, &,xn}  returns Just M that  M "_LRA  when such M exists, returns Nothing otherwise.FV() must be a subset of  {x1, &,xn}."R(c) Masahiro Sakai 2014-2015 BSD-stylemasahiro.sakai@gmail.com provisionalportableNoneoptimize dir obj  returns  (I, lift) whereI' is convex hull of feasible region, andlift is a function, that takes x " I8 and returns the feasible solution with objective value better than or equal to x.Note: i (resp.  iD) is the optimal value in case of minimization (resp. maximization).If I* is empty, then the problem is INFEASIBLE.SNone {x1, &,xm}  returns Sat M such that  M "_LRA  when such M exists,returns Unsat when such M does not exists, andreturns Unknown when  is beyond LRA.EEliminate quantifiers and returns equivalent quantifier-free formula.  returns  (, lift) such that:# is a quantifier-free formula and LRA " "y1, &, yn.  !  where {y1, &, yn} = FV() " FV(), andif  M "_LRA  then lift M "_LRA .% may or may not be a closed formula.h(c) Masahiro Sakai 2011-2013 BSD-stylemasahiro.sakai@gmail.com provisionalportableNone  T(c) Masahiro Sakai 2011-2014 BSD-stylemasahiro.sakai@gmail.com provisional7non-portable (MultiParamTypeClasses, FlexibleInstances)None2461Quantifier-free formula of Presburger arithmetic."Literals of Presburger arithmetic.Divisible True d e means e can be divided by d (i.e. d | e)Divisible False d e means e can not be divided by d (i.e. (d | e))IsPos e means e > 0'(t,c) represents t/c, and c must be >0.+Linear arithmetic expression over integers.d | e means e can be divided by d. M  returns whether  M "_LIA  or not. x  returns  (, lift) such that:"_LIA "y1, &, yn. ("x. ) !  where {y1, &, yn} = FV() \ {x}, andif  M "_LIA  then lift M "_LIA . {x1, &,xm}  returns  (, lift) such that:%"_LIA "y1, &, yn. ("x1, &, xm. ) !  where {y1, &, yn} = FV() \ {x1, &,xm}, andif  M "_LIA  then lift M "_LIA . x  returns ![(_1, lift_1), &, (_m, lift_m)] such that:+"_LIA "y1, &, yn. ("x. ) ! (_1 "( & "( _m) where {y1, &, yn} = FV() \ {x}, andif  M "_LIA _i then lift_i M "_LIA . {x1, &,xm}  returns ![(_1, lift_1), &, (_n, lift_n)] such that:+"_LIA "y1, &, yp. ("x. ) ! (_1 "( & "( _n) where {y1, &, yp} = FV() \ {x1, &,xm}, andif  M "_LIA _i then lift_i M "_LIA . {x1, &,xn}  returns Just M that  M "_LIA  when such M exists, returns Nothing otherwise.FV() must be a subset of  {x1, &,xn}. {x1, &,xn}  returns Just M that  M "_LIA  when such M exists, returns Nothing otherwise.FV() must be a subset of  {x1, &,xn}. {x1, &,xn}  I returns Just M that  M "_LIRA  when such M exists, returns Nothing otherwise.FV() must be a subset of  {x1, &,xn}.I7 is a set of integer variables and must be a subset of  {x1, &,xn}.)#U(c) Masahiro Sakai 2011-2013 BSD-stylemasahiro.sakai@gmail.com provisionalportableNoneEEliminate quantifiers and returns equivalent quantifier-free formula.  returns  (, lift) such that:# is a quantifier-free formula and LIA " "y1, &, yn.  !  where {y1, &, yn} = FV() " FV(), andif  M "_LIA  then lift M "_LIA .% may or may not be a closed formula.  {x1, &,xm} returns Sat M such that  M "_LIA  when such M exists,returns Unsat when such M does not exists, andreturns Unknown when  is beyond LIA.i(c) Masahiro Sakai 2011 BSD-stylemasahiro.sakai@gmail.com provisional non-portable (FlexibleInstances)NoneV(c) Masahiro Sakai 2012 BSD-stylemasahiro.sakai@gmail.com provisionalInon-portable (TypeSynonymInstances, FlexibleInstances, TypeFamilies, CPP)None24=Kresults of optimization0feasibility 0O0a0d0d non-basic variable xj 0nP$0Y'0M0O0Y00feasibility 0O0a0d0d non-basic variable xj 0nP$0\0U0O0Y0-set callback function for receiving messages.e     E !%E !%N      W(c) Masahiro Sakai 2012 BSD-stylemasahiro.sakai@gmail.com provisional.non-portable (ScopedTypeVariables, Rank2Types)NoneHM-set callback function for receiving messages. !"#$%&'   !"#$%&'X(c) Masahiro Sakai 2014 BSD-stylemasahiro.sakai@gmail.com provisionalportableNone Quantifier-free formula of LRA M  returns whether  M "_LRA  or not. x  returns  (, lift) such that:"_LRA "y1, &, yn. ("x. ) !  where {y1, &, yn} = FV() \ {x}, andif  M "_LRA  then  lift M " . {x1, &,xm}  returns  (, lift) such that:%"_LRA "y1, &, yn. ("x1, &, xm. ) !  where {y1, &, yn} = FV() \ {x1, &,xm}, andif  M "_LRA  then lift M "_LRA . x  returns ![(_1, lift_1), &, (_m, lift_m)] such that:+"_LRA "y1, &, yn. ("x. ) ! (_1 "( & "( _m) where {y1, &, yn} = FV() \ {x}, andif  M "_LRA _i then lift_i M "_LRA .( x  returns ![(_1, lift_1), &, (_m, lift_m)] such that:+"_LRA "y1, &, yn. ("x. ) ! (_1 "( & "( _m) where {y1, &, yn} = FV() \ {x}, andif  M "_LRA _i then lift_i M "_LRA . Note that ("x. (x)) ! "(_{t"S} (t) where  = {a_i x - b_i _i 0 | i " I, _i " {=, "`, "d, <}} the set of atomic subformulas in (x) S = { b_i / a_i, b_i / a_i + 1, b_i / a_i - 1 | i"I } "* {1/2 (b_i / a_i + b_j / a_j) | i,j"I, i"`j} {x1, &,xm}  returns ![(_1, lift_1), &, (_n, lift_n)] such that:+"_LRA "y1, &, yp. ("x. ) ! (_1 "( & "( _n) where {y1, &, yp} = FV() \ {x1, &,xm}, andif  M "_LRA _i then lift_i M "_LRA . {x1, &,xn}  returns Just M such that  M "_LRA  when such M exists, returns Nothing otherwise.FV() must be a subset of  {x1, &,xn}. {x1, &,xn}  returns Just M such that  M "_LRA  when such M exists, returns Nothing otherwise.FV() must be a subset of  {x1, &,xn}.()*+,-()*+,-Y(c) Masahiro Sakai 2011 BSD-stylemasahiro.sakai@gmail.com provisionalportableNone.'(t,c) represents t/c, and c must be >0.EoptCheckReal is used for checking whether real shadow is satisfiable.If it returns True0, the real shadow may or may not be satisfiable.If it returns False', the real shadow must be unsatisfiable opt {x1, &,xn}  returns Just M that  M "_LIA  when such M exists, returns Nothing otherwise.FV() must be a subset of  {x1, &,xn}. {x1, &,xn}  I returns Just M that  M "_LIRA  when such M exists, returns Nothing otherwise.FV() must be a subset of  {x1, &,xn}.I7 is a set of integer variables and must be a subset of  {x1, &,xn}.#/0.123456789:;<=>?@ABCDEFG  !/0.123456789:;<=>?@ABCDEFGZ(c) Masahiro Sakai 2011 BSD-stylemasahiro.sakai@gmail.com provisionalportableNone  [None=K HIJ HIJ\(c) Masahiro Sakai 2011 BSD-stylemasahiro.sakai@gmail.com provisional0non-portable (ScopedTypeVariables, BangPatterns)NoneM5tightening variable bounds by constraint propagation.KGtightening intervals by ceiling lower bounds and flooring upper bounds.Linitial bounds constraintsintegral variableslimit of iterationsMNK$@$@LMNK]NoneOO^(c) Masahiro Sakai 2012 BSD-stylemasahiro.sakai@gmail.com provisionalportableNone PQR   PQR_(c) Masahiro Sakai 2011 BSD-stylemasahiro.sakai@gmail.com provisional"non-portable (ScopedTypeVariables)NoneM results of optimizationAllocate a new  non-negative variable.eAdd a contraint and maintain feasibility condition by introducing artificial variable (if necessary).Disequality is not supported.Unlike F, an equality contstraint becomes one row with an artificial variable.FAdd a contraint, without maintaining feasibilty condition of tableaus.Disequality is not supported.Unlike *, an equality constraint becomes two rows.    STUVWXYZ[\            STUVWXYZ[\`(c) Masahiro Sakai 2011 BSD-stylemasahiro.sakai@gmail.com provisional"non-portable (ScopedTypeVariables)NoneMresults of optimization !"#$%&]^_`abcdefghijklmno !"#$%&"! $#&%"! #$%&]^_`abcdefghijklmnoa(c) Masahiro Sakai 2011 BSD-stylemasahiro.sakai@gmail.com provisional"non-portable (ScopedTypeVariables)NoneMpqrstuvwx'()yz{|}~  !"'()"! (')prqstuvwx'()yz{|}~jkljkmjknopqopropsoptuvwuvxuvyuvzuv{uv|uv}uv~uvuvb     cccccccccccccccccccccccccccccccccccccccccccccccccccccccccccccccccccccccccccccc c c c c ccccccccccccc      !"#$%&'()*+,-../01234566789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^^_`abcd)6eefghijklmnopqppprstuvwxyzZ{|}~pPQQPpp !!!"""#$$$$$$$$$$%%%%%%%%%%%%%&'''''''''''''''''''''''''''''''''''''''''' ' ' ' ' ''''''''''''''''''' '!'"'#'$'%'&'''(')'(((*(+(,((-)))*).)/)0)1)2))3)4)5)6*4*5*7+,---8-9-:--./0;0<0=0>0?0@0A0B0C0D0E0F0G0H0I0J0K0L0M0N0O000000000011P1Q1R1111S1T2U2V2W2X2Y2Z2[2\2]2^2_2`333a3b3c3d3e3f3g3h3i3j3k3l3m3n3o3e3x3Z3m3p33q3r3s3t3u3v3w33x3y3z3{4|4}4~44444444555566777777777778888888888889:::;;;;;;;;;;;;;;;<<<<<<<<=========>P>Q>R>??????@@@@@@@@@@@@@@@pApAqBpCpDEEEE}E~EFFhFiFjFkFlFmFFGGGeGGGGGGGHHeHIeIfIgIhIiIjIkIlImInIoIJJJJJ'JJ(JJ)J*JJJJJJJJJJJJKKmK<KKKKKKKKKKKKKKKKKKKKKKKKKKLLLLLLLLL L L L L LLLLLLLMMMMMMtMMsMMMMMMMMM N!N"NN#N$N%NO&O'O(O)OmO<O*O+O,OO-OOOP.P/P0P1Q-Q2Q3Q4Q5Q6Q7Q8Q9QQ:Q;Q<Q=Q>Q?QQQQQQ RGS@SASBTCTZTDT4T7T:TETFTTTTGTHTITTJUAU@VVKVVVLVMVNVOV(VPVQVRVSVTVUVVVVVWVVVXVYVVZV[V\V]VV^V_V`VVaVbVVVcVVGVVdVeVfVgVhViVjVkVlVVmVnWWWGWWWWoWpWWXCXFXXXGXHXIXYYYqYYrYsYYJYtZuZvZw[<[<[[x[y[z[\{]|]}^^ _M_O_(_P_~____h____y________`M`P`O`````GaaaGbbbbbbbbbbbb                   cccccccccccccccccccccccccccccccccccccccccccccccc         !"#$%&'()*+,-.V/01S23456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVNWPXYXZ[\]^_`abcdefghijklmnopmqorstup v!w!xyz{#|#}$~$$$$$%~%%%%%%&~&&&&&''''''''''''''''''''''''''''''''''''''''''''''''''''''''''''''''''''''''''''''''''''''''''''''''''''''''''''''''''''''''''''''''''''''''''' ' ' ' ' '''''''''''''''L''''' '!'"'#'$'%'&'''(')'*'+','-'.'/'0'1'2'3'4'5'6'7'8'9':';'<'='>'?'@'A'B'C'D'E'F'G'H'I'J'K'L'M'N'O'P'Q'R'S'T'U'V'W'X'Y'Z'['\']'^'_'`'a'b'c'd'e'f'g'h'i'j'k'l'm'n'o'p'q'r()+s,t,t,u,v,w,x,y,s-z-t-t-u-v-s-.s/s0;0{0|0}0~000000111111111111111222222222333333333333333333333333333333x3333333333344444444444555566666ef8888gggggggx:::;;;;;;;;;;;;;;;;;;;;;;;==>>>>>>6>>>>>>>>>>>>:>>>>">>>>>>>$>>>E>>> >>)>*>+> >,> >V> > >>>>>>>@@@@@@@@@@@@@@ @!@:@"@@#@$@%@&@@'@A(A)A*A+A,DD-D.D/D0D1D2D3D4EF5F5F6F7F8F9F:F;F<F=F>F?F@FAFBFCFDFEFFGGGGHGIGJGKHLHMINIOIPIQJRJSJTJUK<KVKKWKXKYKZK[K\K]L^L_L`LaLbLcLdLeLfLgLhLiLjLkLlLmMnMMoMpMqMrMsMtMuMvMwMxMyMzM{M|M}MM~MMMMMMMMMMMMMMMMMMMMMMMMMMMMMMNNwNxNNNNNNOO]OOOQQQQQQQVQQQQQRRST6TTTTTTT8TTTTTTTTTTTTTTTTTVVVWVVVVVVVVVVVVVVgVVVVVVVVVVVVVVVVLVVVV_V`VVVVVVVVVVWWWWWWWWWWWWWWWWWVW_W`WWXXXXXXY6YYY7YYYYYYYYYYYY YYYYY Y Y YY Y[[X[Y\ \\\]^^^__________```` `!`"`#`$`%`&`'`(`)`*`+`,`-`.`/a0a1a2aaa3aa4a5a6a7a8a9a:a;awa<a=ax>toysolver-0.2.0ToySolver.Data.MIP.Base%ToySolver.Internal.Data.PriorityQueueToySolver.VersionToySolver.Internal.Data.IOURefToySolver.Text.SDPFileToySolver.Text.GurobiSolToySolver.Internal.TextUtilToySolver.Internal.Data.Vec ToySolver.Internal.Data.SeqQueue,ToySolver.Internal.Data.IndexedPriorityQueueToySolver.Data.Polynomial7ToySolver.Data.Polynomial.Factorization.Hensel.Internal2ToySolver.Data.Polynomial.Factorization.SquareFreeToySolver.Text.MPSFileToySolver.Data.LBoolToySolver.Text.PBFileToySolver.Converter.PB2LSPToySolver.Converter.PB2WBOToySolver.Converter.PB2SMPToySolver.Converter.SAT2PBToySolver.SAT.TypesToySolver.Converter.WBO2PBToySolver.SAT.MUS.TypesToySolver.SAT.PBO.ContextToySolver.SAT.TheorySolverToySolver.SAT.PrinterToySolver.Text.GCNFToySolver.Text.MaxSATToySolver.Converter.MaxSAT2WBOToySolver.Converter.MaxSAT2NLPBToySolver.Converter.ObjTypeToySolver.Converter.PBSetObj#ToySolver.Combinatorial.Knapsack.DP#ToySolver.Combinatorial.Knapsack.BBToySolver.Internal.ProcessUtil&ToySolver.Combinatorial.HittingSet.SHD)ToySolver.Combinatorial.HittingSet.HTCBDD)ToySolver.Combinatorial.HittingSet.Simple ToySolver.SATToySolver.SAT.MUSToySolver.SAT.MUS.CAMUSToySolver.SAT.MUS.DAAToySolver.SAT.PBO.BCToySolver.SAT.PBO.BCDToySolver.SAT.PBO.BCD2ToySolver.SAT.PBO.UnsatBasedToySolver.SAT.PBO.MSU4ToySolver.SAT.PBOToySolver.CongruenceClosureToySolver.Data.BooleanToySolver.FOLModelFinder'ToySolver.Data.Polynomial.GroebnerBasis3ToySolver.Data.Polynomial.Factorization.FiniteField2ToySolver.Data.Polynomial.Factorization.Zassenhaus#ToySolver.Data.AlgebraicNumber.Root$ToySolver.Data.AlgebraicNumber.Sturm0ToySolver.Data.Polynomial.Interpolation.LagrangeToySolver.Data.DNF#ToySolver.Data.AlgebraicNumber.RealToySolver.Internal.UtilToySolver.Data.DeltaToySolver.Text.LPFileToySolver.Data.MIPToySolver.Converter.MIP2SMTToySolver.Converter.PB2IPToySolver.Converter.MaxSAT2IPToySolver.Converter.SAT2IP1ToySolver.Data.Polynomial.Factorization.KroneckerToySolver.Data.VarToySolver.Data.BoolExprToySolver.SAT.TseitinEncoderToySolver.WangToySolver.Data.FOL.FormulaToySolver.Data.ArithRelToySolver.Data.LAToySolver.Arith.SimplexToySolver.Arith.CAD&ToySolver.Data.AlgebraicNumber.ComplexToySolver.Data.FOL.ArithToySolver.Data.LA.FOL#ToySolver.Arith.FourierMotzkin.Base+ToySolver.Arith.FourierMotzkin.Optimization"ToySolver.Arith.FourierMotzkin.FOLToySolver.Arith.Cooper.BaseToySolver.Arith.Cooper.FOLToySolver.Arith.Simplex2ToySolver.Arith.MIPSolver2#ToySolver.Arith.VirtualSubstitutionToySolver.Arith.OmegaTest.BaseToySolver.Arith.OmegaTestToySolver.SAT.IntegerToySolver.Arith.BoundsInferenceToySolver.Arith.LPUtilToySolver.Arith.ContiTraversoToySolver.Arith.LPSolverToySolver.Arith.LPSolverHLToySolver.Arith.MIPSolverHLPaths_toysolverToySolver.Data.Polynomial.Base.ToySolver.Data.Polynomial.Factorization.Hensel/ToySolver.Data.Polynomial.Factorization.Integer0ToySolver.Data.Polynomial.Factorization.Rational&ToySolver.Data.AlgebraicNumber.GraeffeToySolver.Arith.FourierMotzkinToySolver.Arith.Cooper OptDir-0.0.3 Data.OptDirOptMinOptMaxOptDirextended-reals-0.2.1.0Data.ExtendedRealExtendedFiniteNegInfPosInf queue-0.1.2Data.Queue.ClassesnewFifoNewFifo enqueueBatchenqueueEnqueue dequeueBatchdequeueDequeue queueSize QueueSizeversionpackageVersionsIOURef newIOURef readIOURef writeIOURef modifyIOURef DenseBlock DenseMatrixBlockMatrixProblem blockStructcostsmatricesmDimnBlock blockElem denseBlock denseMatrix diagBlockparseDataString parseDataFileparseSparseDataStringparseSparseDataFilerender renderSparseModelreadIntreadUnsignedIntegerIndexUVecVec GenericVecnewgetSizereadwrite unsafeRead unsafeWriteresizegrowTopush unsafePopcleargetElemsclonegetArray getCapacityresizeCapacity PriorityQueuenewPriorityQueuenewPriorityQueueBy getHeapArray getHeapVecresizeHeapCapacitySeqQueueValuememberupdateresizeTableCapacity MonomialOrder UMonomialMonomial mindicesMapUTermTermX UPolynomial PrettyVar pPrintVar PrettyCoeff pPrintCoeffisNegativeCoeff PrintOptions pOptPrintVarpOptPrintCoeffpOptIsNegativeCoeffpOptMonomialOrderSQFreesqfreeFactorfactorContPPcontpp PolynomialcoeffMapDegreedegVarsvarsVarvarconstant fromTerms fromCoeffMapfromTermtermsltlclmcoeff lookupCoeff isPrimitivederivintegralevalsubstmapCoefftoMonictoUPolynomialOfdivModMPreducedefaultPrintOptions prettyPrintnatdivmoddivModdividesgcdlcmexgcdpdivModpdivpmodgcd'isRootOf isSquareFreetdegtscaletmulttdividestdivtderiv tintegralmone mfromIndicesmfromIndicesMapmindicesmmultmpowmdividesmdivmderiv mintegralmlcmmgcdmcoprimelexrevlexgrlexgrevlexhenselcabook_proposition_5_10cabook_proposition_5_11 sqfreeChar0 Variables SOSConstraintsosLabelsosTypesosBodySOSTypeS2S1RelOpEqlGeLe BoundExprLabelBoundsVarInfovarType varBoundsVarTypeSemiIntegerVariableSemiContinuousVariableIntegerVariableContinuousVariable Constraint constrLabelconstrIndicator constrBody constrIsLazyObjectiveFunctionExprdirobjectiveFunction constraintssosConstraintsuserCutsvarInfo defaultBounds defaultLB defaultUBtoVarfromVar getVarInfo getVarType getBoundsintersectBounds variablesintegerVariablessemiContinuousVariablessemiIntegerVariables parseString parseFileparserLBoollTruelFalselUndeflnotliftBool unliftBoolLit WeightedTermSumSoftConstraint SoftFormula wboTopCostwboConstraints wboNumVarswboNumConstraintsOpEqFormulapbObjectiveFunction pbConstraints pbNumVarspbNumConstraintsparseOPBString parseOPBFileparseWBOString parseWBOFile renderOPB renderWBOconvert convertWBO XORClause PBLinExactly PBLinAtLeastPBLinSum PBLinTermAtLeastClauseLitMapLitSetIModelevalVarVarMapVarSetvalidVarlitUndefvalidLitliterallitNotlitVar litPolarityevalLitnormalizeClause clauseSubsume evalClauseclauseToPBLinAtLeastnormalizeAtLeast evalAtLeastnormalizePBLinSumnormalizePBLinAtLeastnormalizePBLinExactly cutResolvecardinalityReductionnegatePBLinAtLeast evalPBLinSumevalPBLinAtLeastevalPBLinExactly pbLowerBound pbUpperBound pbSubsumenormalizeXORClause evalXORClauseMSSSSMCSCSMUSUS Normalized SimpleContextContextgetObjectiveFunctionisUnsatgetBestSolution getLowerBoundsetUnsat addSolution addLowerBound logMessage getBestValue getBestModel isOptimum isFinishedgetSearchUpperBound setFinishednewSimpleContextsetOnUpdateBestSolutionsetOnUpdateLowerBound setLogger normalize TheorySolver thAssertLitthCheck thExplainthPushBacktrackPointthPopBacktrackPoint emptyTheory satPrintModelmaxsatPrintModel pbPrintModel musPrintSolGClause GroupIndexGCNFnumVars numClauseslastGroupIndexclausesWeightWeightedClauseWCNFtopCostparseByteStringObjType ObjMaxZero ObjMaxOneObjNonesetObjsolverunProcessWithOutputCallbackFailureOptions optSHDCommand optSHDArgs optOnGetLineoptOnGetErrorLinedefaultOptionsminimalHittingSetsMethod MethodKnuth MethodTodaoptHTCBDDCommand optMethodRestartStrategy LubyRestarts ArminRestartsMiniSATRestarts PBHandlerTypePBHandlerTypePuebloPBHandlerTypeCounterLearningStrategyLearningHybridLearningClauseBudgetExceededSolver getVarFixed getLitFixedvarDecayActivityvarBumpActivitynVarsnAssigns nConstraintsnLearnt newSolvernewVarnewVarsnewVars_resizeVarCapacity addClause addAtLeast addAtMost addExactly addPBAtLeast addPBAtMost addPBExactlyaddPBAtLeastSoftaddPBAtMostSoftaddPBExactlySoft addXORClauseaddXORClauseSoft solveWithgetModelgetFailedAssumptionssetRestartStrategydefaultRestartStrategysetRestartFirstdefaultRestartFirst setRestartIncdefaultRestartIncsetLearningStrategydefaultLearningStrategysetLearntSizeFirstdefaultLearntSizeFirstsetLearntSizeIncdefaultLearntSizeIncsetCCMin defaultCCMinsetVarPolarity setCheckModel setRandomFreqdefaultRandomFreq setRandomGen getRandomGen setConfBudgetdefaultPBHandlerTypesetPBHandlerTypesetEnablePhaseSavinggetEnablePhaseSavingdefaultEnablePhaseSaving"setEnableForwardSubsumptionRemoval"getEnableForwardSubsumptionRemoval&defaultEnableForwardSubsumptionRemoval#setEnableBackwardSubsumptionRemoval#getEnableBackwardSubsumptionRemoval'defaultEnableBackwardSubsumptionRemoval optLogger optUpdateBest optLitPrinterfindMUSAssumptions optOnMCSFound optOnMUSFound optKnownMCSes optKnownMUSes optKnownCSesenumMCSAssumptionsallMCSAssumptionsallMUSAssumptionscamusdaaoptEnableHardeningoptEnableBiasedSearchoptSolvingNormalFirst OptimizerSearchStrategyBCD2BCDBCMSU4 UnsatBasedAdaptiveSearch BinarySearch LinearSearchdefaultSearchStrategy newOptimizeroptimizegetSearchStrategysetSearchStrategy!defaultEnableObjFunVarsHeuristicsgetEnableObjFunVarsHeuristicssetEnableObjFunVarsHeuristicsdefaultTrialLimitConfgetTrialLimitConfsetTrialLimitConfFlatTermFTAppFTConstmerge areCongruentBoolean.=>..<=>. ComplementnotBMonotoneBooleantruefalse.&&..||.andBorB mUniverse mRelations mFunctionsEntity GenFormulaExistsForallEquivImplyNotOrAndAtomFTPAppTmVarTmAppGenLitNegPosPSymFSym toSkolemNF showEntity showModel findModelStrategy SugarStrategyNormalStrategy optStrategy spolynomialbasisbasis' reduceGBasis berlekampbasisOfBerlekampSubalgebra zassenhaus normalizePolyrootAddrootMul rootShift rootScale rootRecip rootSimpPoly rootNthRootlift2findPoly SturmChain sturmChainnumRoots numRoots'separate separate'halvehalve'narrownarrow'approxapprox' interpolateDNFunDNFAReal realRoots realRootsExapproxIntervalnthRootrefineIsolatingIntervalminimalPolynomialisolatingInterval isRationalisAlgebraicIntegerheight rootIndex simpARealPoly goldenRatio combineMaybe isIntegerfracPart showRationalshowRationalAsFiniteDecimal revSequencerevMapMrevForMDeltadeltafromRealrealPart deltaPartfloor'ceiling' isInteger'readFile readLPFile readMPSFile writeFile writeLPFile writeMPSFile YicesVersionYices2Yices1LanguageYICESSMTLIB2 optLanguage optSetLogic optCheckSAToptProduceModel optOptimizeBoolExprfoldsimplifyEncoder encSolver evalFormula newEncodersetUsePB addFormula encodeConj encodeDisjgetDefinitionsSequentisValidpushNotArithRel IsArithRelarithRelNEqGtLtflipOpnegOpshowOpevalOp.<..<=..>..>=..==../=. fromArithRel BoundsEnvunitVarasConstmapCoeffWithVarevalExpr evalLinearlift1 applySubst applySubst1extract extractMaybeshowExprshowAtomevalAtomapplySubstAtomapplySubst1AtomsolveForcomputeIntervalRowColIndexRowIndexTableau emptyTableau objRowIndexpivot lookupRowaddRow setObjFun currentValuecurrentObjValueisValidTableau isFeasible isOptimalsimplex dualSimplexphaseIprimalDualSimplextoCSVCellIntervalPointRootOfproject' findSampleevalCell evalPointprojectprojectN projectN'solve'AComplex:+imagPart conjugate magnitude SatResultSatUnsatUnknown:/::*::+:Const fromFOLAtom toFOLFormula fromFOLExpr toFOLExprConstrIsZeroIsPosIsNonnegRatExprZtoRateqR fromLAAtomtoLAAtomconstraintsToDNF evalBoundsboundsToConstrs collectBounds solveFormulaeliminateQuantifierseliminateQuantifiers' QFFormula Divisible.|. evalQFFormula projectCases projectCasesNsolveQFFormulasolveQFLIRAConjRawModelobjLimit OptResultObjLimit UnboundedOptimum PivotStrategyPivotStrategyLargestCoefficientPivotStrategyBlandRule SolverValuetoValue showValue GenericSolver cloneSolversetPivotStrategy assertAtom assertAtomEx assertLower assertUppergetObj setOptDir getOptDirisBasicVariableisNonBasicVariablecheck getRawModel getObjValuegetLBgetUB getTableaugetValuegetRowgetColgetCoeff clearLoggerdumpsetShowRational setNThread optCheckRealcheckRealNoCheck checkRealByFMzmodcheckRealByCAD checkRealByVScheckRealBySimplex linearize addConstraintaddConstraintSoft inferBoundstoStandardFormtoStandardForm'LP emptySolver putTableaudefine#addConstraintWithArtificialVariabletableautwoPhaseSimplexcollectNonnegVarsOptUnsatmaximizeminimizecatchIObindirlibdirdatadir libexecdir sysconfdir getBinDir getLibDir getDataDir getLibexecDir getSysconfDirgetDataFileName pDataFilepSparseDataFilepComment pBlockStructpCostspDenseMatricespSparseMatricesnat_lineintrealsign renderImpl renderVecshowRatconcatSsepBySbase Text.Read integer-gmpGHC.Integer.TypeIntegerreadUnsignedInt cloneArraycopyToghc-prim GHC.ClassesOrdheapupdownleftrightparent$fQueueSizePriorityQueueIO$fDequeuePriorityQueueIOa$fEnqueuePriorityQueueIOa$fNewFifoPriorityQueueIO$fQueueSizeSeqQueueIO$fDequeueSeqQueueIOa$fEnqueueSeqQueueIOa$fNewFifoSeqQueueIOnewPriorityQueueBy#lt#table$fDequeuePriorityQueueIOInt$fEnqueuePriorityQueueIOInt asConstantscalezeroplusnegmultisZerocontIppIprettyPrintTermaddPrecmulPrecratPrecexpPrecappPrecmfromIndicesMap'$fHashableMonomial$fVarsMonomialv$fVarMonomialv$fDegreeMonomial$fNFDataMonomial$fIsStringMonomial$fShowMonomial $fHashableX $fNFDataX $fPrettyVarX$fPrettyVarInt$fPrettyCoeffPolynomial$fPrettyCoeffPrimeField$fPrettyCoeffRatio$fPrettyCoeffInteger$fPrettyPolynomial$fDefaultPrintOptions $fContPPRatio$fContPPInteger$fDegreePolynomial$fVarsPolynomialv$fVarPolynomialv$fHashablePolynomial$fNFDataPolynomial$fShowPolynomial$fVectorSpacePolynomial$fAdditiveGroupPolynomial$fIsStringPolynomial$fNumPolynomialf$fSQFreePolynomial$fSQFreePolynomial0defaultVarInfo$fVariablesSOSConstraint$fVariablesConstraint$fVariablesTerm$fVariablesProblem$fVariablesEither $fVariables[]$fDefaultVarInfo$fDefaultVarType$fDefaultConstraint$fDefaultProblemM BoundTypeSISCUILIBVPLMIFRFXUPLOColumnspace'spaces'spaces1' commentlinenewline'tokrowcolumnidentstringLnnumber nameSectionobjSenseSectionobjNameSection rowsSectionuserCutsSectionlazyConsSectionrowsBody colsSection rowAndVal rhsSection rangesSection boundsSection boundType sosSectionquadObjSectionqMatrixSectionqcMatrixSectionindicatorsSectionexecM writeString writeCharrender'writeSectionHeader writeFieldsnameRows quadMatrixcheckAtMostQuadratic $fShowLBoolformulahintsequence_of_commentscomment#sequence_of_comments_or_constraintscomment_or_constraint objective constraintsum weightedtermintegerunsigned_integerrelational_operator variablenameoneOrMoreSpacezeroOrMoreSpaceeolsemitermoneOrMoreLiterals softformula softheader'wbo_sequence_of_comments_or_constraintswbo_comment_or_constraintsoftconstraintshowOPBshowWBOshowSumshowWeightedTermshowLitshowConstraintshowSoftConstraintpbComputeNumVarswboComputeNumVars showConstrsum'showTerm GHC.TypesTrueFalse Data.MaybeNothing $fIModel(->) $fIModelArray$fIModelUArraynBasenObjectiveFunctionnOffsetscGetObjectiveFunction scUnsatRefscBestSolutionRefscLowerBoundRefscOnUpdateBestSolutionRefscOnUpdateLowerBoundRef scLoggerRef$fContextNormalized$fContextSimpleContextsplit isComment parseLine parseCNFLineseqList parseWCNFLineparseWCNFLineBSparseCNFLineBS parseClauseBS isCommentBSgenObjtest1test2process-1.2.0.0System.Processproc withForkWait ignoreSigPipe HittingSet HyperEdgeVertexexecSHD$fExceptionFailure$fDefaultOptions execHTCBDD$fDefaultMethodpropagateChoicemaintainNoSupersetsnubOrdbasicPropagateSomeConstraintHandler basicReasonOf svVarDecaysvVarInc svConstrDecay svConstrIncsvRestartFirst svRestartIncsvLearntSizeFirstsvLearntSizeIncsvCCMin ldWatches vdWatcheswatchLitwatchVarwatches backtrackTo propagatereasonOfXORClauseHandlerxorLits xorActivityxorHashPBHandlerPueblo puebloTerms puebloDegreepuebloMaxSlack puebloWatchespuebloWatchSumpuebloActivity puebloHashPBHandlerCounterpbTermspbDegree pbCoeffMap pbMaxSlackpbSlack pbActivitypbHashAtLeastHandler atLeastLits atLeastNumatLeastActivity atLeastHash ClauseHandlerclaLits claActivityclaHash CHXORClause CHPBPueblo CHPBCounter CHAtLeastCHClauseConstraintHandlertoConstraintHandlershowConstraintHandlerattachwatchedLiteralswatchedVariablesisPBRepresentabletoPBLinAtLeast isSatisfiedconstrIsProtected constrWeightconstrReadActivityconstrWriteActivity SearchResultSRBudgetExceeded SRRestart SRFinished VarActivitysvOk svVarQueuesvTrail svVarData svConstrDB svLearntDB svAssumptionssvLevel svBCPQueuesvModel svNDecisionsvNRandomDecision svNConflict svNRestart svNAssignssvNFixed svNLearntGCsvNRemovedConstrsvRestartStrategy svLearntLimsvLearntLimAdjCntsvLearntLimSeqsvEnablePhaseSaving!svEnableForwardSubsumptionRemovalsvLearningStrategysvPBHandlerType"svEnableBackwardSubsumptionRemovalsvLogger svStartWC svLastStatWC svCheckModel svRandomFreq svRandomGensvFailedAssumptions svConfBudgetLitData ldOccurListVarData vdAssignment vdPolarity vdPosLitData vdNegLitData vdActivity AssignmentaValueaIndexaLevelaReason aBacktrackCBsLevel levelRoot newVarData newLitDatavarDatalitDatavarValuelitValuevarLevellitLevel varReason varAssignNomarkBad bcpEnqueue bcpDequeue bcpCheckEmptyassignByassignassign_unassignaddBacktrackCBaddToDB addToLearntDBreduceDB varActivityvarRescaleAllActivitylearntConstraintsltVarsolve_searchcheckForwardSubsumptionremoveBackwardSubsumedBybackwardSubsumedByremoveConstraintHandlers pickBranchLitdecidededuceanalyzeConflict analyzeFinalanalyzeConflictHybridpbBacktrackLevelminimizeConflictClauseminimizeConflictClauseLocalminimizeConflictClauseRecursivepopTrailconstructModelconstrDecayActivityconstrBumpActivityconstrRescaleAllActivity resetStatprintStatHeader printStat showTimeDiffdetachisLocked findForWatch findForWatch2newClauseHandlerinstantiateClausebasicAttachClauseHandlernewAtLeastHandlerinstantiateAtLeastbasicAttachAtLeastHandler newPBHandlernewPBHandlerPromoted instantiatePB pbOverSAT pbToAtLeastnewPBHandlerCounter puebloAMaxnewPBHandlerPueblopuebloGetWatchSum puebloWatch puebloUnwatchpuebloPropagatepuebloUpdateWatchSumnewXORClauseHandlerinstantiateXORClausebasicAttachXORClauseHandler mkRestartSeqminiSatRestartSeqarminRestartSeqlubyRestartSeqlubyallManyMshiftdefaultHashWithSalt debugModecheckSatisfied sanityCheckdumpVarActivitydumpConstrActivityloglogIO#$fConstraintHandlerXORClauseHandler$fHashableXORClauseHandler$fEqXORClauseHandler"$fConstraintHandlerPBHandlerPueblo$fHashablePBHandlerPueblo$fEqPBHandlerPueblo#$fConstraintHandlerPBHandlerCounter$fHashablePBHandlerCounter$fEqPBHandlerCounter!$fConstraintHandlerAtLeastHandler$fHashableAtLeastHandler$fEqAtLeastHandler $fConstraintHandlerClauseHandler$fHashableClauseHandler$fEqClauseHandler($fConstraintHandlerSomeConstraintHandler$fHashableSomeConstraintHandler$fExceptionBudgetExceededsolveWBOCoreInfocoreLitscoreLBcoreUB coreMidValue coreUnionrefine optContext optSolveroptSearchStrategyRef optEnableObjFunVarsHeuristicsRefoptTrialLimitConfRef linSearch binSearchadaptiveSearch tweakParams$fDefaultSearchStrategy svVarCounter svPendingsvRepresentativeTable svClassList svUseList svLookupTable PendingEqnEqn1lookup setLookup addToPendinggetRepresentative $fBooleanBool$fMonotoneBooleanBool$fComplementBool $fBoolean(->)$fMonotoneBoolean(->)$fComplement(->) $fBoolean(,)$fMonotoneBoolean(,)$fComplement(,)SGenAtomSGenTermSubst GroundClause GroundLit GroundAtom GroundTermSClauseSLitSAtomSTermSEqSPAppSTmVarSTmApptoNNFtest_toSkolemNFflatten test_flattenshowEntityTuple enumSubstsimplifyGroundClause collectFSym collectPSymtest$fVarsSGenAtom$fVarsSGenTerm$fVarsGenFormula$fBooleanGenFormula$fComplementGenFormula$fMonotoneBooleanGenFormula $fVarsAtom $fVarsTerm $fVarsGenLit$fComplementGenLit$fVars[]ItemiFstiSndiCmpiLCMitempairs$fEqItem $fOrdItemsqfree' polyPthRoot$fFactorPolynomialnorm2sqliftdiv'combboundscountSignChanges countChanges boundIntervalNthRootgraeffesMethodf' $fBooleanDNF$fMonotoneBooleanDNF$fComplementDNFproperFraction'GHC.RealproperFraction truncate'truncateround'roundceilingfloor $fDegreeARealRealRoot realRoots'realRoot realRoot' scaleAReal shiftARealnthRoots$fPrettyCoeffAReal $fPrettyAReal$fRealFracAReal $fRealAReal$fFractionalAReal $fNumAReal $fOrdAReal $fEqAReal$fVectorSpaceDelta$fAdditiveGroupDeltaBounds2char'string'sepvariablelabelreservedproblemendconstraintSection subjectTorelOplazyConstraintsSectionbound boundExprinfgeneralSection binarySection semiSectionexprqexprqtermqfactorwriteVar renderExpr showCoeff showConstTerm renderLabelrenderOprenderConstraintrenderBoundExprrenderVariableListfillremoveEmptyExprEnvunlinesSlistand'or'not'intExprrealExprintNumrealNumreltoRealassert conditionsnonAdjacentPairsencodeisInttestFiletestdataconvExprconvVarrelaxGErelaxLEmtransfactor'factor2isUPolyZtoZxvalues interleavefactors primeFactorsSimplify runSimplifyisTrueisFalse$fBooleanSimplify$fMonotoneBooleanSimplify$fComplementSimplify$fVariablesBoolExpr$fBooleanBoolExpr$fMonotoneBooleanBoolExpr$fComplementBoolExpr$fHashableBoolExpr$fNFDataBoolExpr$fTraversableBoolExpr$fFoldableBoolExpr$fMonadBoolExpr$fApplicativeBoolExpr$fFunctorBoolExprencUsePB encConjTableencodeToClause encodeToLit addIsConjOfisValid'pick$fBooleanFormula$fMonotoneBooleanFormula$fComplementFormula$fVariablesFormula$fFunctorArithRel$fVariablesArithRel$fIsArithReleArithRel$fComplementArithRel normalizeExpr showExprWith$fVectorSpaceExpr$fAdditiveGroupExpr $fNFDataExpr $fReadExpr $fShowExpr$fVariablesExprPDResult PDUnbounded PDOptimalPDUnsat PivotResult PivotSuccess PivotFinishedPivotUnbounded normalizeRowsetRow copyObjRow isImproving primalPivot dualPivotremoveArtificialVariablespdPivot AssumptionCoeffSignConfshowCell showPoint emptySignConf showSignConfnormalizeSignConfKeylookupSignConfmr test_mr_1 test_mr_2runMassume buildSignConfcollectPolynomialsrefineSignConfemptyAssumption propagateEq propagateSignisOkay dropConstantsassumption2condcomputeSignSetshowDNFdumpProjection dumpSignConftest1atest1btest1ctest2atest2b test_projecttest_project_printtest_project_2test_project_3_print test_solvetest_collectPolynomialstest_collectPolynomials_printtest_buildSignConftest_buildSignConf_printtest_buildSignConf_2test_buildSignConf_2_printtest_buildSignConf_3test_buildSignConf_3_printGHC.Numabssignumrootstest3test4test5test6$fFractionalAComplex $fNumAComplex$fIsArithRelExprFormula $fFunctorExpr$fFractionalExpr $fNumExprfromRatevalRatleRltRgeRgtR subst1Constr evalConstrfindEq$fVariablesConstrdata-interval-1.2.0 Data.Interval lowerBound upperBound projectToObj' projectTo'negateDNFConstrLCMgetLCMWitnessWCase2WCase1leZltZgeZgtZeqZsubst1 simplifyLit evalWitness projectCases' checkedDiv testHagiya $fMonoidLCM$fIsArithRelExprBoolExpr$fComplementLit$fVariablesLit increaseNB decreaseNB svTableausvLBsvUBsvVCntsvOptDirsvDefDBsvPivotStrategysvNPivotobjVar simplifyAtomselectViolatingBasicVariableselectEnteringVariable canIncrease canDecrease canIncrease1 canDecrease1 dualRTestprunepivotAndUpdatefindMtestLBtestUBbasicVariables recordTime showDeltadumpSizecheckFeasibilitycheckNBFeasibilitycheckOptimality$fSolverValueDelta$fSolverValueRatioNodendLPndDepthndValueMIP mipRootLPmipIVsmipBest mipNThread mipLoggermipOnUpdateBestSolutionmipShowRationalbranchAndBoundviolatedderiveGomoryCutcanDeriveGomoryCutcollect IntervalZBoundsZapplySubst1Constr evalBoundsZcollectBoundsZisExactchooseVariable extractEq eliminateEqunivZ intersectZpickupZpickuptightenToIntegerCstrictmkModel costOrdering elimOrderingaddArtificialVariablegetArtificialVariablesclearArtificialVariablesgetDefs isSingleVarisSingleNegatedVar expandDefs expandDefs'introduceArtificialVariablesnormalizeConstraint example_3_2test_3_2 example_3_5test_3_5 example_4_1test_4_1 example_4_2test_4_2 example_4_3test_4_3 example_4_5test_4_5 example_4_6test_4_6 example_4_7test_4_7kuhn_7_3 test_kuhn_7_3testAllErrErrUnsat ErrUnboundedndSolver ndTableau ndLowerBoundtableau'conv mkInitialNodeisStrictlyBettertraverseexample1test1'example2