summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers
AgeCommit message (Expand)Author
2021-07-28Make extended rewriter methods const (#6948)Andrew Reynolds
2021-07-27Track instantiation reasons in proofs (#6935)Andrew Reynolds
2021-07-27Move enum value generator to own file (#6941)Andrew Reynolds
2021-07-27Minor fix for term database + central equality engine (#6928)Andrew Reynolds
2021-07-27Make all dependencies in the fast enumerator optional (#6918)Andrew Reynolds
2021-07-27Add sygus enumerator callback (#6923)Andrew Reynolds
2021-07-16Do not exhaustive instantiation when FMF is disabled (#6899)Andrew Reynolds
2021-07-15Fix context for proofs of instantiations (#6890)Andrew Reynolds
2021-07-15Distinguish quantifiers preprocess as its own proof rule (#6897)Andrew Reynolds
2021-07-15Move master equality engine notification to own file (#6877)Andrew Reynolds
2021-07-14Move synthesis verification check to own file (#6882)Andrew Reynolds
2021-07-07Standard output for trigger selection (#6841)Andrew Reynolds
2021-07-03Fix performance of string regression (#6832)Andres Noetzli
2021-07-03Add output tags -o, --output. (#6826)Mathias Preiner
2021-07-01Add recursive function definitions to subsolver in sygus (#6824)Andrew Reynolds
2021-07-01Add option to limit the number of instantiation rounds (#6818)Andrew Reynolds
2021-06-30Do not apply fmfBound to standard quantifiers when only stringsExp is enabled...Andrew Reynolds
2021-06-28Rename internal string kinds to match API (#6797)Andrew Reynolds
2021-06-22Fix type enumeration for non first-class sorts in FMF (#6719)Andrew Reynolds
2021-06-15Remove public option wrappers (#6716)Gereon Kremer
2021-06-08Fix for 2 dimensional dependent bounded quantifiers (#6710)Andrew Reynolds
2021-06-07Remove `Options::wasSetByUser()` (#6682)Gereon Kremer
2021-06-02Move public wrapper functions out of options class (#6600)Gereon Kremer
2021-05-27Fix CEGQI for datatypes with Boolean subfields (#6630)Andrew Reynolds
2021-05-27FP: Rename FLOATINGPOINT_PLUS to FLOATINGPOINT_ADD. (#6628)Aina Niemetz
2021-05-26 More precise includes of `Node` constants (#6617)Andres Noetzli
2021-05-24Move proof utilities to src/proof/ (#6611)Andrew Reynolds
2021-05-24Fix instance of no rewrite in extended rewriter (#6610)Andrew Reynolds
2021-05-21Fix and refactor relevant domain (#6528)Andrew Reynolds
2021-05-21Update to sygus standard output for check-synth responses (#6521)Andrew Reynolds
2021-05-21BV: Rename BITVECTOR_PLUS to BITVECTOR_ADD. (#6589)Aina Niemetz
2021-05-20Remove old unsat cores (#6581)Haniel Barbosa
2021-05-18Loop over terms to reconstruct instead of obligations. (#6504)Abdalrhman Mohamed
2021-05-13Add std::hash overloads for Node, TNode and TypeNode. (#6534)Mathias Preiner
2021-05-07Simplifications to expand definitions (#6487)Andrew Reynolds
2021-05-06Discard duplicate terms in patterns (#6501)Andrew Reynolds
2021-05-05Do not have quantifiers model inherit from theory model (#6493)Andrew Reynolds
2021-04-29Avoid exponential explosion of small constant in CEGQI (#6461)Gereon Kremer
2021-04-28Remove exception headers from options.h (#6456)Gereon Kremer
2021-04-27Fix refutational soundness bug in quantifier prenexing (#6448)Andrew Reynolds
2021-04-26First part of options refactoring (#6428)Gereon Kremer
2021-04-25Use fast enumeration by default for Boolean predicate synthesis (#6440)Andrew Reynolds
2021-04-23Enable strings exp by default for strings specific logics (#6424)Andrew Reynolds
2021-04-21Goodbye CVC4, hello cvc5! (#6371)Mathias Preiner
2021-04-20Quantifiers: Move implementation of type rules to cpp. (#6404)Aina Niemetz
2021-04-19Fully incorporate quantifiers macros into ppAssert / non-clausal simplificati...Andrew Reynolds
2021-04-15Rename occurrences of CVC4 to CVC5. (#6351)Aina Niemetz
2021-04-14Refactor / reimplement statistics (#6162)Gereon Kremer
2021-04-14Rename public and private headers in src/include. (#6352)Aina Niemetz
2021-04-14Add internal API methods for pool-based instantiation (#6350)Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback