summaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2020-03-21Simplify heuristic in `processNEqc` (#4129)Andres Noetzli
2020-03-20Don't run bv_nat parse test with competition build (#4126)Andres Noetzli
2020-03-20Generalize mkConcat for types (#4123)Andrew Reynolds
2020-03-20Fix variable shadowing issue in sygus-inference (#4121)Andrew Reynolds
2020-03-20Fix sort comparison within assertion in cegis (#4113)Andrew Reynolds
2020-03-20Guard cases of sort inference in quantifier free logics in uf cardinality (#4...Andrew Reynolds
2020-03-20Split string-specific operators from TheoryStringsRewriter (#3920)Andrew Reynolds
2020-03-20Do not assign higher-order representative if function does not exist (#4073)Andrew Reynolds
2020-03-20Handle failures for sygus QE preprocess (#4072)Andrew Reynolds
2020-03-20Parse error for SyGuS version 1.0 vs 2.0 (#4057)Andrew Reynolds
2020-03-20Make handling of illegal internal representatives in quantifiers engine more ...Andrew Reynolds
2020-03-20Refactor enumerator for strings (#4014)Andrew Reynolds
2020-03-19Fix regression output related to sygus+bv-div-zero (#4122)Andrew Reynolds
2020-03-19Bv2int fail on demandyoni206
2020-03-19Only apply testConstStringInRegExp to const regexp (#4120)Andres Noetzli
2020-03-19SyGuS must use total bitvector division (#4119)Andrew Reynolds
2020-03-18Only allow bv2nat/int2bv with BV and integer logic (#4118)Andres Noetzli
2020-03-19Remove spurious assertion (#4117)Andrew Reynolds
2020-03-18Explicitly handle isFinite for rounding modes (#4115)Andrew Reynolds
2020-03-18Always enable cbqi literal dependency (#4116)Andrew Reynolds
2020-03-18Fix issue with multiple infinities in CEGQI for LIRA (#4114)Andrew Reynolds
2020-03-18Move node visitor class from smt_util/ to expr/ (#4110)Alex Ozdemir
2020-03-16SmtEngine: Convert members owned by SmtEngine to unique pointers. (#4108)Aina Niemetz
2020-03-16Remove AlwaysAssert(false) for hole.Alex Ozdemir
2020-03-16clang-formatAlex Ozdemir
2020-03-16Fix simplicity check in propAlex Ozdemir
2020-03-16Fix antecedent loop. WhoopsAlex Ozdemir
2020-03-16Only save farkas+tightening proofs. Error on holesAlex Ozdemir
2020-03-16Expand the definition of a "simple" farkas proof.Alex Ozdemir
2020-03-16DecisionEngine: Use single unique pointer for ITE strategy . (#4078)Aina Niemetz
2020-03-16Issue 4077: Add unit test to reproduce issue. (#4107)Aina Niemetz
2020-03-16Create master equality engine at context level 0 (#4081)Andres Noetzli
2020-03-15Handle cases in --sygus-rr where evaluation is not constant (#4100)Andrew Reynolds
2020-03-13Removing a few deprecated options (#4052)Andrew Reynolds
2020-03-13Remove regress for real to int (#4071)Andrew Reynolds
2020-03-13Generalize type rules for strings to sequences (#3987)Andrew Reynolds
2020-03-13Fix case of non-constant value for sygus sampling (#4051)Andrew Reynolds
2020-03-12Add options for nec regression (#4056)Andrew Reynolds
2020-03-12Convert most instances of dataypes in parsers to the new API (#4054)Andrew Reynolds
2020-03-12Do not allow quantifiers over real variables in real to int pass. (#4049)Andrew Reynolds
2020-03-12Remove local theory extension option (#4048)Andrew Reynolds
2020-03-12Do not make models for quantified function variables (#4039)Andrew Reynolds
2020-03-12New C++ API: Remove support for (reset). (#4037)Aina Niemetz
2020-03-12Ensure legal candidate equalities when using relational triggers (#4035)Andrew Reynolds
2020-03-11Fix double notify in equality engine (#4036)Andrew Reynolds
2020-03-11Hide options for and related to the BV abstraction module. (#4041)Aina Niemetz
2020-03-11Simplifications to the Datatypes API (#4040)Andrew Reynolds
2020-03-11Add automatic Cython binding installation (#3933)makaimann
2020-03-11Do not enable some SMT-COMP specific options by default (#4038)Andrew Reynolds
2020-03-11Guard against null relevancy condition in SyGuS (#4033)Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback