summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/sygus
AgeCommit message (Expand)Author
2021-07-03Add output tags -o, --output. (#6826)Mathias Preiner
2021-07-01Add recursive function definitions to subsolver in sygus (#6824)Andrew Reynolds
2021-06-28Rename internal string kinds to match API (#6797)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-27FP: Rename FLOATINGPOINT_PLUS to FLOATINGPOINT_ADD. (#6628)Aina Niemetz
2021-05-26 More precise includes of `Node` constants (#6617)Andres Noetzli
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-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-04-28Remove exception headers from options.h (#6456)Gereon Kremer
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-14Refactor / reimplement statistics (#6162)Gereon Kremer
2021-04-14Rename public and private headers in src/include. (#6352)Aina Niemetz
2021-04-14Merge equivalent sub-obligations instead of discarding them. (#6353)Abdalrhman Mohamed
2021-04-14Warn about infeasible SyGuS conjectures (#6345)Andrew Reynolds
2021-04-13Avoid using substitute's input cache after the method call. (#6328)Abdalrhman Mohamed
2021-04-12Fix computation of whether a type is finite (#6312)Andrew Reynolds
2021-04-12Refactor and update copyright headers. (#6316)Aina Niemetz
2021-04-09Rename CVC4_ macros to CVC5_. (#6327)Aina Niemetz
2021-04-09Rename CVC4__ header guards to CVC5__. (#6326)Aina Niemetz
2021-04-08Add identifiers for sources of incompleteness (#6311)Andrew Reynolds
2021-04-08Initial support for parametric datatypes in sygus (#6304)Andrew Reynolds
2021-04-07Fixes for abducts (#6279)Andrew Reynolds
2021-04-07Replace calls to NodeManager::mkSkolem with SkolemManager::mkDummySkolem (#6291)Andrew Reynolds
2021-04-01Rename namespace CVC5 to cvc5. (#6258)Aina Niemetz
2021-03-31Rename namespace CVC4 to CVC5. (#6249)Aina Niemetz
2021-03-31Eliminate dependencies on quantifiers engine in internal quantifiers code (#6...Andrew Reynolds
2021-03-30Miscellaneous elimination of dependencies on quantifiers engine (#6238)Andrew Reynolds
2021-03-29Eliminate the use of quantifiers engine in sygus solver (#6232)Andrew Reynolds
2021-03-29Move decision manager into theory inference manager (#6231)Andrew Reynolds
2021-03-26Pass term registry to quantifiers modules (#6216)Andrew Reynolds
2021-03-25Add missing includes. (#6207)Gereon Kremer
2021-03-24Use inference manager to access intantiate utility instead of quantifiers eng...Andrew Reynolds
2021-03-23Remove internal includes of Api header. (#6193)Aina Niemetz
2021-03-23Replace old sygus term reconstruction algorithm with a new one. (#5779)Abdalrhman Mohamed
2021-03-15Reorganizing initialization of term registry in quantifiers (#6127)Andrew Reynolds
2021-03-11Delete Expr layer. (#6117)Aina Niemetz
2021-03-09Some more cleanup of includes (#6083)Gereon Kremer
2021-03-09Update copyright headers to 2021. (#6081)Aina Niemetz
2021-03-05Remove partial UDIV/UREM operators. (#6069)Mathias Preiner
2021-03-03More cleanup of includes to reduce compilation times (#6037)Gereon Kremer
2021-03-03Remove uses of SExpr class. (#6035)Abdalrhman Mohamed
2021-03-02Introduce quantifiers term registry (#5983)Andrew Reynolds
2021-03-02Clean up includes to reduce compile times (#6031)Gereon Kremer
2021-02-22Eliminate raw use of output channel and valuation in quantifiers (#5933)Andrew Reynolds
2021-02-22Move quantifiers attributes to quantifiers registry (#5929)Andrew Reynolds
2021-02-17Eliminate non-static members in term util (#5919)Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback