summaryrefslogtreecommitdiff
path: root/src/theory/arith
AgeCommit message (Collapse)Author
2018-08-15format code blocksAndres Noetzli
2018-08-15Move node algorithmsAndres Noetzli
2018-08-07Require Swig 3 (#2283)Andres Noetzli
Removes some hacks due to Swig 2's incomplete C++11 support and adds checks for version 3 at configuration time as well as in swig.h
2018-07-26Changing the arithmetic static learner to use CDHashMap. This is 2/3 PRs for ↵Tim King
deprecating CDTrailHashMap. (#2207)
2018-07-25Changing ArithIteUtils to use CDInsertHashMap. (#2206)Tim King
This is 1/3 PRs for deprecating CDTrailHashMap.
2018-07-17 Purify applications of exp to transcendental arguments (#2097)Andrew Reynolds
2018-07-06Split ext theory to own file and document (#1809)Andrew Reynolds
2018-06-25Updated copyright headers.Aina Niemetz
2018-06-02Fix corner case of mixed int/real cegqi. (#2046)Andrew Reynolds
2018-05-25Fix various nl assertions. (#1980)Andrew Reynolds
2018-05-24Fix (#1975)Andrew Reynolds
2018-05-24Fixes for non-linear check model (#1974)Andrew Reynolds
2018-05-23Remove spurious assertion in nonlinear extension (#1972)Andrew Reynolds
2018-05-23Generalize check-model in NonLinearExtension for quadratic equations (#1892)Andrew Reynolds
2018-05-03Option to interleave tangent plane inferences (#1833)Andrew Reynolds
2018-05-01Improve tangent planes for transcendental functions (#1832)Andrew Reynolds
2018-04-29Make factoring inference more aggressive (#1825)Andrew Reynolds
2018-04-29Refactor nonlinear check (#1814)Andrew Reynolds
2018-04-29Improvements to simple transcendental function check model. (#1823)Andrew Reynolds
2018-04-27Simplify tangent plane direction (#1824)Andrew Reynolds
2018-04-25Remove nl solve subs option. (#1803)Andrew Reynolds
2018-04-19Refactor pbRewrites preprocessing pass (#1767)Andres Noetzli
This commit refactors the pbRewrites preprocessing pass into the new style. This commit is essentially just a code move and adds a regression test for the preprocessing pass. It also makes use of the AssertionPipeline::replace function to do proper dependency tracking.
2018-04-03Use choice when expanding definitions for inverse transcendental functions ↵Andrew Reynolds
(#1742)
2018-03-30Do not use factoring inference for transcendental functions (#1707)Andrew Reynolds
2018-03-20Internally remove redundant assertions and infer equalities in ↵Andrew Reynolds
NonLinearExtension (#1633)
2018-03-05Enable -Wsuggest-override by default. (#1643)Mathias Preiner
Adds missing override keywords.
2018-02-27Option to not use partial function semantics for arithmetic div by zero (#1620)Andrew Reynolds
2018-02-20Minor fixes and additions for transcendental functions (#1612)Andrew Reynolds
Also adds parsing support for PI in smt2 with syntax "real.pi".
2018-02-14Quantifiers subdirectories (#1608)Andrew Reynolds
2018-02-07Removing an unused variable. (#1576)Tim King
2018-02-07Add remaining transcendental functions (#1551)Andrew Reynolds
2018-02-06Resolving warnings from -Winconsistent-missing-override on clang. (#1563)Tim King
2018-02-02Restoring ostream format. Resolves a few CIDs 1362780. (#1543)Tim King
2018-01-26Removing structurally dead code. (#1540)Tim King
2018-01-23Commenting out throw specifiers for DeltaRationExceptions. These functions ↵Tim King
can be cleaned up later. (#1529)
2018-01-10Removing throw specifiers for TypeRules. (#1501)Tim King
2018-01-10Removing throw specifiers from type enumerators. (#1502)Tim King
2018-01-09Cleaning up throw specifiers on Exception and subclasses. (#1475)Tim King
2018-01-07Removes RationalFromDoubleException. Replaces this with an explicit M… (#1476)Tim King
* Removes RationalFromDoubleException. Replaces this with an explicit Maybe<Rational> datatype. Makes Maybe<T> CVC4_PUBLIC. Updates the users of Rational::fromDouble(). Miscellaneous cleanup of ApproxSimplex.
2018-01-03Global negate (#1466)Andrew Reynolds
2017-12-20Transcendental functions check model (#1443)Andrew Reynolds
2017-12-08Make collect model info return a Bool (#1421)Andrew Reynolds
2017-11-30Remove remaining references to QuantArith (#1408)Andrew Reynolds
2017-11-28Improve the rewriter for SINE. (#1221)Andrew Reynolds
2017-11-24Implement tangent and secant planes for transcendental functions (#1401)Andrew Reynolds
2017-11-22Transcendental tangent planes utilities (#1288)Andrew Reynolds
2017-11-17Add random number generator. (#1370)Aina Niemetz
This adds a deterministic (seeded) random number generator (RNG). It implements the xorshift* generator (see S. Vigna, An experimental exploration of Marsaglia's xorshift generators, scrambled. ACM Trans. Math. Softw. 42(4): 30:1-30:23, 2016).
2017-11-16(Refactor) Arithmetic monomial sum (#1381)Andrew Reynolds
* Add arithmetic monomial sum utility. * Clang format * Fix * Address review. * Fix missed comment. * Format * Fix
2017-11-07Combining d_conflictHasBeenRaised and d_conflictIndex into a CDMaybe. (#1332)Tim King
2017-11-07Moving the enum ArithType to partial_model. Adding a new type Unset in the ↵Tim King
enum. Always initializing VarInfo::d_type. (#1333)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback