summaryrefslogtreecommitdiff
path: root/src/theory
AgeCommit message (Expand)Author
2018-06-01Min synth sol option.ajreynol
2018-05-31Do not guard for any constant disequalities.ajreynol
2018-05-31Moreajreynol
2018-05-31Move any constant to better spot.ajreynol
2018-05-31Update script, fix any constant printing.ajreynol
2018-05-31Extended rewrite builtin solutions.ajreynol
2018-05-31More simplifyajreynol
2018-05-31Simplify beta reduction.ajreynol
2018-05-31Fixajreynol
2018-05-31Deterministic vs non-deterministic PBE strategies.ajreynol
2018-05-31Merge branch 'master' of https://github.com/CVC4/CVC4 into sygusComp2018-2ajreynol
2018-05-30Fix bv-abstraction check for AND with non bit-vector atoms. (#2024)Mathias Preiner
2018-05-30Optionsajreynol
2018-05-30Repair condition to separate.ajreynol
2018-05-30Fix for issue #2002 (#2012)Andres Noetzli
2018-05-30Moreajreynol
2018-05-30Fixes for quantifiers + incremental (#2009)Andrew Reynolds
2018-05-30Normalize negated bit-vector terms over equalities. (#2017)Mathias Preiner
2018-05-30Improve trace.ajreynol
2018-05-30Docajreynol
2018-05-30Improve org.ajreynol
2018-05-30Minor, add option.ajreynol
2018-05-29Fixesajreynol
2018-05-29Merge branch 'sygusComp2018-2' into sym-break-anyconstHaniel Barbosa
2018-05-29Merge opt3.ajreynol
2018-05-29Merge branch 'sygusComp2018-2' into sym-break-anyconstHaniel Barbosa
2018-05-29deleting commentHaniel Barbosa
2018-05-29fixesHaniel Barbosa
2018-05-29revertHaniel Barbosa
2018-05-29draftHaniel Babosa
2018-05-29Initialize with extRewBv branch.ajreynol
2018-05-28Builtin evaluation functions for sygus (#1991)Andrew Reynolds
2018-05-27Fix cegqi assertions for quantified non-linear cases. (#1999)Andrew Reynolds
2018-05-25Reenable repair const (#1983)Andrew Reynolds
2018-05-25Fix various nl assertions. (#1980)Andrew Reynolds
2018-05-24Fix (#1979)Andrew Reynolds
2018-05-24Improve simple constant symmetry breaking for sygus (#1977)Andrew Reynolds
2018-05-24Fix compiler warnings (#1959)Andres Noetzli
2018-05-24Fix (#1975)Andrew Reynolds
2018-05-24Fixes for non-linear check model (#1974)Andrew Reynolds
2018-05-23Remove spurious assertion in nonlinear extension (#1972)Andrew Reynolds
2018-05-23Towards better symbolic enumeration in SyGuS (#1971)Haniel Barbosa
2018-05-23Add notions of evaluated kinds in TheoryModel (#1947)Andrew Reynolds
2018-05-23Generalize check-model in NonLinearExtension for quadratic equations (#1892)Andrew Reynolds
2018-05-22Repair constants using symbolic constructors (#1960)Andrew Reynolds
2018-05-22Make sygus infer find function definitions (#1951)Andrew Reynolds
2018-05-21Infrastructure for strings strategies (#1883)Andrew Reynolds
2018-05-21Infrastructure to mark unused sygus strategies (#1950)Andrew Reynolds
2018-05-21Refactor sygus eval unfold (#1946)Andrew Reynolds
2018-05-21Assign weight 1 for Boolean variables in SyGuS default grammars (#1948)Haniel Barbosa
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback