summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers
AgeCommit message (Expand)Author
2018-03-05Enable -Wsuggest-override by default. (#1643)Mathias Preiner
2018-03-05Fix for sampler. (#1639)Andrew Reynolds
2018-03-02Optimization for sygus streaming mode (#1636)Andrew Reynolds
2018-03-02Simplify sygus wrt miniscoping (#1634)Andrew Reynolds
2018-03-02Print candidate rewrites in terms of original grammar (#1635)Andrew Reynolds
2018-03-01Create infrastructure for sygus modules (#1632)Andrew Reynolds
2018-02-27Minor fixes for rec-fun (#1616)Andrew Reynolds
2018-02-27Improvements to sygus sampling (#1621)Andrew Reynolds
2018-02-14Quantifiers subdirectories (#1608)Andrew Reynolds
2018-02-12Option to use extended rewriter as a preprocessing pass (#1600)Andrew Reynolds
2018-02-12Minor improvements to sygus sampler (#1598)Andrew Reynolds
2018-02-10More minor improvements to synth-rr (#1597)Andrew Reynolds
2018-02-09Move BitVector specific funs from bv::utils to util/bitvector.h. (#1589)Aina Niemetz
2018-02-09Class to reduce printing of redundant candidate rewrites (#1588)Andrew Reynolds
2018-02-08Adding virtual destructors on classes with virtual functions. (#1583)Tim King
2018-02-08Minor improvements to sygus sampling. (#1577)Andrew Reynolds
2018-02-07Fixing more inconsistent usages of override. (#1575)Tim King
2018-02-06Fixes two memory leaks coming from Transf. (#1564)Tim King
2018-02-06Updated copyright header for bv_inverter.(cpp|h).Aina Niemetz
2018-02-06Resolving warnings from -Winconsistent-missing-override on clang. (#1563)Tim King
2018-02-05Statically eliminate redundant sygus constructors (#1560)Andrew Reynolds
2018-02-04Sample based on sygus grammar by default (#1558)Andrew Reynolds
2018-02-02Option to use sampling for CEGIS (#1555)Andrew Reynolds
2018-02-02Fix remaining synthesis solution regressions (#1557)Andrew Reynolds
2018-02-01Add interface in sygus to get synthesis solution Nodes (#1552)Andrew Reynolds
2018-02-01Use sygus to synthesize/verify rewrite rules (#1547)Andrew Reynolds
2018-01-29Generalize explanations for PBE sygus strings based on negative contains when...Andrew Reynolds
2018-01-28Sort children of all commutative operators for sygus. (#1544)Andrew Reynolds
2018-01-23Fix MULT handling for CBQI BV. (#1531)Aina Niemetz
2018-01-22Add previous concat handling for CBQI BV as heuristic for EQ. (#1528)Aina Niemetz
2018-01-21Refactor and fix solveBvLit for CBQI BV. (#1526)Aina Niemetz
2018-01-13Remove BITVECTOR_SUB from isInvertible(). (#1513)Aina Niemetz
2018-01-12Improvements for CBQI BV (#1504)Andrew Reynolds
2018-01-10Removed division by constant handling for CBQI BV (unsound). (#1508)Aina Niemetz
2018-01-10Removing throw specifiers for TypeRules. (#1501)Tim King
2018-01-09Fix linearization for terms where the solve variable does not occur. (#1506)Mathias Preiner
2018-01-08Removing more miscellaneous throw specifiers. (#1488)Tim King
2018-01-08Added division by constant handling for CBQI BV. (#1498)Aina Niemetz
2018-01-08Improvements to quant+BV/Bool variable elimination (#1495)Andrew Reynolds
2018-01-07Re-ordering field initialization in QuantInfo to remove compiler warning. (#1...Tim King
2018-01-05Add special {SGE,SGT,NE}_UDIV1 side conditions for BV of size 1. (#1483)Mathias Preiner
2018-01-05Use simpler EQUAL SCs for LSHR0, LSHR1, ASHR0, AHSR1, SHL0, SHL1. (#1482)Mathias Preiner
2018-01-05Add UGT/SGT side conditions for AND/OR + other fixes. (#1481)Mathias Preiner
2018-01-04Fix side condition handling for PLUS, XOR, SIGN_EXTEND for CBQI BV. (#1480)Aina Niemetz
2018-01-04Add side conditions for inequalities of SHL. (#1472)Mathias Preiner
2018-01-04Improvements for CBQI (#1478)Andrew Reynolds
2018-01-03Add side conditions for UGT/SGT over BITVECTOR_UREM for CBQI BV. (#1470)Aina Niemetz
2018-01-03Add UGT/SGT side conditions for LSHR. (#1469)Mathias Preiner
2018-01-03 Add side conditions for inequalities over BITVECTOR_MULT for CBQI BV. (#1468)Aina Niemetz
2018-01-03Global negate (#1466)Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback