summaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Expand)Author
2019-08-17Move quantifiers relevance module inside E-matching module (#3186)Andrew Reynolds
2019-08-17Mark symbols introduced by named attributes as defined. (#3190)Andrew Reynolds
2019-08-15 Fix for when to apply single invocation techniques (#3193)Andrew Reynolds
2019-08-14Remove option --continued-execution. (#3189)Mathias Preiner
2019-08-14 Update to standard implementation of getting free variables (#3175)Andrew Reynolds
2019-08-14Call separate SMT engine for single invocation sygus (#3151)Andrew Reynolds
2019-08-14cmake: Export CVC4 library interface. (#3179)Mathias Preiner
2019-08-14Minor cleaning of sygus term database (#3159)Andrew Reynolds
2019-08-14Fix issue related to higher-order purification in term database (#3157)Andrew Reynolds
2019-08-13SmtEngine: Reorganize class according to guidelines, some cleanup. (#3183)Aina Niemetz
2019-08-13New C++ API: Add checks and tests for Solver::simplify. (#3170)Aina Niemetz
2019-08-13New C++ API: Reorganize Solver code (move only). (#3170)Aina Niemetz
2019-08-13 Track sygus variable to term relationship via attribute (#3182)Andrew Reynolds
2019-08-13Update option to disable symbolic definitions in strings (#3180)Andrew Reynolds
2019-08-13Add string rewrite involving allchar stars (#3167)Andrew Reynolds
2019-08-13Properly implement logic info for separation logic (#3176)Andrew Reynolds
2019-08-13Implement check abduct feature (#3152)Andrew Reynolds
2019-08-13Introduce smt2 parsing utility ParseOp and refactor (#3165)Andrew Reynolds
2019-08-12Clean smt2 parsing of named attributes (#3172)Andrew Reynolds
2019-08-12 Give rewrite engine pointer to conflict-based instantiation module (#3174)Andrew Reynolds
2019-08-11New C++ API: Add documentation/guidelines for API guards. (#3178)Aina Niemetz
2019-08-11New C++ API: Add templated getIndices method for OpTerm (#3073)makaimann
2019-08-10Simplify how defined functions are tracked during parsing (#3177)Andrew Reynolds
2019-08-10Add option to only dump unsolved queries for --sygus-query-gen (#3173)Andrew Reynolds
2019-08-08Reorganize includes for quantifiers engine (#3169)Andrew Reynolds
2019-08-08Fix issues with Ninja build system and add configure option. (#3166)Mathias Preiner
2019-08-07New C++ API: Add checks and tests for push/pop. (#3121)Aina Niemetz
2019-08-07New C++ API: Introduce macros for try-catch blocks in Solver. (#3121)Aina Niemetz
2019-08-06New C++ API: Fix branch prediction in CHECK macros. (#3161)Aina Niemetz
2019-08-06Properly parse qualified identifiers (#3111)Andrew Reynolds
2019-08-05Remove forward declarations in quantifiers engine (#3156)Andrew Reynolds
2019-08-03Fix printing issue related to nested quotes (#3154)Andrew Reynolds
2019-08-03Collapse @ chains in SMT2 printer (#3140)Haniel Barbosa
2019-08-02Update CaDiCaL to version 1.0.3. (#3137)Mathias Preiner
2019-08-02Flip the polarity of the argument of get-abduct (#3153)Andrew Reynolds
2019-08-02 Move basic sygus enumerator to its own file (#3149)Andrew Reynolds
2019-08-02Remove simplification specialized for sygus si solution reconstruction (#3147)Andrew Reynolds
2019-08-02Support default sygus grammar for strings (#3148)Andrew Reynolds
2019-08-02Throw option exception when track inst lemmas is not used (#3145)Andrew Reynolds
2019-08-02Fix solution filtering for streaming abducts (#3143)Andrew Reynolds
2019-08-01Fix BVGauss unit tests. (#3142)Mathias Preiner
2019-08-01Enable sygus logic when produce-abducts is true (#3144)Andrew Reynolds
2019-08-01Fix memory leak in rewriter (debug mode). (#3141)Mathias Preiner
2019-08-01Move some generic utilities out of quantifiers (#3139)Andrew Reynolds
2019-08-01 Regular expression intersection modes (#3134)Andrew Reynolds
2019-07-31Parsing THF and adding several regressions (#3131)Haniel Barbosa
2019-07-31Add some missing cases in evaluator (#3133)Andrew Reynolds
2019-07-31Eager conflict detection in strings based on constant prefix/suffix (#3110)Andrew Reynolds
2019-07-30 Track solver execution mode (#3132)Andrew Reynolds
2019-07-30Code to activate hoelim preprocessing pass (#3129)Haniel Barbosa
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback