Age | Commit message (Collapse) | Author | |
---|---|---|---|
2012-05-18 | This commit adds TypeNode::leastCommonTypeNode(). The special case for ↵ | Tim King | |
arithmetic in TypeNode::operator==() has been removed. A number of faulty type checking checks were switched to use isSubtypeOf. The resolves bug #339 | |||
2012-05-18 | This commit removes the dead psuedoboolean code. | Tim King | |
2012-05-18 | Removing long unsigned operator+ from CDList's const_iterator. | Tim King | |
2012-05-17 | This fixes a fascinating segfault. This is the sequence of events: | Tim King | |
1) A restart occurs 2) A shared term is registered to arithmetic. 3) Arithmetic sets this up. 4) No new linear relations are added to arithmetic. 5) Eventually a restart occurs. 6) Arithmetic resets the tableau as it has not had a row added since the last restart. 7) A new variable is added. 8) This exceeds the size of the column vector of the saved tableau by exactly one. 9) segfault | |||
2012-05-17 | Fixing an issue with LogicInfo::isPure() that turned off simplification in ↵ | Morgan Deters | |
QF_UF and maybe others | |||
2012-05-17 | Fixed bug 338: | Liana Hadarean | |
- fixed buggy rewrite rules assuming certain nodes only had 2 children - added support for bv-rewrite dump - fixed smt2_printer for bv constants | |||
2012-05-17 | Queueing up asserted literals in the proxy instead of sending them off to ↵ | Dejan Jovanović | |
the theory engine immediately. The queue is discharged just before a check(). | |||
2012-05-16 | adding simple-minded handling of (dis-)equalities where constants are involved | Dejan Jovanović | |
2012-05-16 | Fixing C compatibility library (it still had a reference to CONST_INTEGER). | Morgan Deters | |
This hopefully fixes the Debian build. | |||
2012-05-16 | Changes to SAT solver: | Dejan Jovanović | |
* allowing propagation of false literals (handles conflict) * allowing lemmas during BCP (bug 337) * UF does direct propagation, without checking for literal value anymore | |||
2012-05-16 | equality status for bitvectors can now look into the sat solver to check for ↵ | Dejan Jovanović | |
IN_MODEL status | |||
2012-05-16 | removing duplicate literals in explanations of propagations | Dejan Jovanović | |
2012-05-16 | refactored TheoryBV bitblaster and equality engine into subtheories (similar ↵ | Liana Hadarean | |
to TheoryEngine | |||
2012-05-15 | fixed QF_BV performance problem due to using CDList instead of CDQueue | Liana Hadarean | |
2012-05-15 | Fix to shared terms visitor. | Tim King | |
2012-05-15 | Implement TypeNode::isComparableTo() and add a unit test for it. | Morgan Deters | |
2012-05-15 | Fixed several bugs in shared terms database | Clark Barrett | |
2012-05-15 | This commit removes the CONST_INTEGER kind from nodes. This code comes from ↵ | Tim King | |
the branch arithmetic/remove_const_int. | |||
2012-05-15 | renamed bv_sat.h, bv_sat.cpp to bitblaster.h, bitblaster.cpp respectively | Liana Hadarean | |
2012-05-15 | removing all extended commands (as inspired by the Z3 extended command set) ↵ | Morgan Deters | |
except for declare-datatypes | |||
2012-05-15 | Fix QF_AUFLIA (resolves bug #331). | Morgan Deters | |
2012-05-15 | fixing warnings, grr | Dejan Jovanović | |
2012-05-15 | several bug fixes: in TheoryBV::NotifyClass missing NOT in predicate notify ↵ | Liana Hadarean | |
and now term notify handles boolean constants; fixed bug 328 | |||
2012-05-14 | fixes for shared term registration. previously the type was not considered ↵ | Dejan Jovanović | |
when looking at theories of the term and for a term like read(a, f(x)) the term f(x) would not be registered to arithmetic in AUFLIA. this fixies the issue of bug 330 and moves it to some other assertion fail. | |||
2012-05-14 | Fixed assertion failures in array theory | Clark Barrett | |
This fixes bugs 335 and 333. | |||
2012-05-14 | in debug builds, -d can be used for trace tags that aren't also debug tags | Morgan Deters | |
2012-05-14 | fixing up preregistration again | Dejan Jovanović | |
2012-05-13 | fixing build warnings | Dejan Jovanović | |
2012-05-11 | fix regex in Debug_tags and Trace_tags generation for Mac OS | Morgan Deters | |
2012-05-11 | fix typo in sed line | Morgan Deters | |
2012-05-11 | output a warning message when a function type (or datatype, or array, etc.) ↵ | Morgan Deters | |
is created with a Boolean term inside it | |||
2012-05-11 | Disabled arith-rewrite-equalities by default unless in a pure arithmetic theory | Clark Barrett | |
2012-05-11 | Added some ITE rewrites, | Clark Barrett | |
Added ITE simplifier - on by default only for QF_LIA benchmarks Fixed one bug in arrays Added negate() to node.h - it returns kind == NOT ? kind[0] : kind.notNode() | |||
2012-05-11 | Partially fixes something-like-a-problem with TheoryArith::getDeltaValue(). | Tim King | |
2012-05-10 | Removing now unneeded (as of r3425) typenames from EqualityEngine. trunk now ↵ | Tim King | |
compiles on Debian. | |||
2012-05-09 | fix an issue which breaks language bindings (so this commit fixes debian ↵ | Morgan Deters | |
nightly builds) | |||
2012-05-09 | --disable-tracing at configure time now disables Trace() and Debug() ↵ | Morgan Deters | |
gestures both. | |||
2012-05-09 | * simplifying equality engine interface | Dejan Jovanović | |
* notifications are now through the interface subclass instead of a template * notifications include constants being merged * changed contextNotifyObj::notify to contextNotifyObj::contextNotifyPop so it's more descriptive and doesn't clutter methods when subclassed * sat solver now has explicit methods to make true and false constants * 0-level literals are removed from explanations of propagations | |||
2012-05-09 | rm something for a future merge that sneaked in | Kshitij Bansal | |
(gets rid of warning) | |||
2012-05-09 | Merge from decision branch (ITE support) | Kshitij Bansal | |
Major changes from last merge * ITEs supported * Don't share theory lemmas to DE, only assertions Should probably be noted that 'make regress' doesn't quite pass with --decision=justification. Throws off search in couple of arith benchmarks. No serious performance changes expected. Keep an eye. | |||
2012-05-09 | Fixing the debug tags generation and related methods in configuration.cpp ↵ | Dejan Jovanović | |
that disallowed me to debug my bugs by reporting that the debug tag doesn't exists, where in fact it was in the code. 1) The grep and sed for tags wasn't picking up on .isOn("tag") 2) The isDebugTag a) didn't take a parameter b) was using binary search using strcmp which is non-portable and didn't work for tags including special characters Morgan should vet this, since there is some crazy sed stuff going on | |||
2012-05-08 | Merging in bvprop branch, with proper bit-vector propagation. | Liana Hadarean | |
This should also fix bug 325. | |||
2012-05-07 | Fixing a bug with TheoryArith::ppAssert() and shared terms. | Tim King | |
2012-05-07 | Fixes a sign bug in the DioSolver. | Tim King | |
2012-05-04 | Guard for expensive Debug trace | Clark Barrett | |
2012-05-04 | options: fail if the debug or trace tag specified doesn't exist (-d -t) | François Bobot | |
2012-05-04 | fix: getNumTraceTags, getNumDebugTags | François Bobot | |
2012-05-04 | - This fixes a problem where simplex produced the same conflict in the ↵ | Tim King | |
single check call. - This increases the number of substitutions that ppAssert can solve on integer equations. | |||
2012-05-03 | Some cleanup starting off from trying to understand the sharing code. ↵ | Dejan Jovanović | |
Changes include * fixed term visitor from the bvprop branch * removed all the warnings from builds -- warnings are there to be noted *NOT* to be used as scribbles * moved the LogicInfo into the theory constructor | |||
2012-05-02 | Changing d_sharedTermsExist to logicInfo.isSharingEnabled() | Clark Barrett | |