projects / cvc5.git / history
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
(proof-new) proofs in ee -> arith pipeline (#5215)
[cvc5.git] / test /
2020-10-07 Aina NiemetzNew C++ API: Rename Term::isConst() to Term::isValue... tree | commitdiff
2020-10-07 Gereon KremerMake sure conflicts are not rewritten (in arithmetic... tree | commitdiff
2020-10-06 yoni206bv-to-int: change order of passes (#5208) tree | commitdiff
2020-10-06 mudathirmahgoubAdd operators bag.from_set, bag.to_set to the theory... tree | commitdiff
2020-10-06 Abdalrhman MohamedRecover from some exceptions. (#5203) tree | commitdiff
2020-10-06 mudathirmahgoubRemove subtyping for sets (#5205) tree | commitdiff
2020-10-04 mudathirmahgoubRemove subtyping for sets theory (#5179) tree | commitdiff
2020-10-03 Andrew ReynoldsFix theory white unit test (#5194) tree | commitdiff
2020-10-03 Andrew ReynoldsStandardization of Theory (#5181) tree | commitdiff
2020-10-01 Aina NiemetzFloatingPoint: Add utility functions for largest and... tree | commitdiff
2020-10-01 Aina NiemetzBitVector: Extend interface of setBit to set it to... tree | commitdiff
2020-09-30 Aina NiemetzFloatingPoint: Add utility functions for largest and... tree | commitdiff
2020-09-29 Andrew ReynoldsReset assertions on resetAssertions (#5153) tree | commitdiff
2020-09-29 Andrew ReynoldsDisable regression that is timing out (#5142) tree | commitdiff
2020-09-28 mudathirmahgoubImplement bags rewriter (#5132) tree | commitdiff
2020-09-27 Andrew ReynoldsFix sygus quantifier elimination preprocess for multipl... tree | commitdiff
2020-09-26 Andrew ReynoldsUse original quantified formula for single invocation... tree | commitdiff
2020-09-26 Aina NiemetzRestrict bvxnor to only allow two operands (was n-ary... tree | commitdiff
2020-09-25 Haniel BarbosaCleaning and documenting cnf stream (#5134) tree | commitdiff
2020-09-24 Andrew ReynoldsModify lemma vs fact policy for datatype equalities... tree | commitdiff
2020-09-23 Andrew ReynoldsDisable cegqi-bv when using sygus (#5124) tree | commitdiff
2020-09-23 Aina NiemetzMissing format from #5112. tree | commitdiff
2020-09-23 yoni206bv2int: new options for bvand translation (#5096) tree | commitdiff
2020-09-23 Andrew ReynoldsAllow E-matching by default when strings are enabled... tree | commitdiff
2020-09-23 Aina NiemetzNew C++ API: Catch and throw recoverable exception... tree | commitdiff
2020-09-23 Abdalrhman MohamedRefactor Commands to use the Public API. (#5105) tree | commitdiff
2020-09-23 Andres Noetzli[Python API] Conversion to/from Unicode strings (#5120) tree | commitdiff
2020-09-22 Mathias PreinerAdd simple BV solver (#5065) tree | commitdiff
2020-09-22 mudathirmahgoubAdd skeleton for theory of bags (multisets) (#5100) tree | commitdiff
2020-09-22 makaimannAdd method to get Python object from constant value... tree | commitdiff
2020-09-22 Mathias PreinerUpdate copyright header script to support CMake and... tree | commitdiff
2020-09-22 yoni206Require dumping in a dumping test (#5108) tree | commitdiff
2020-09-18 yoni206bv2int: quantifiers support (#5080) tree | commitdiff
2020-09-18 Andres Noetzli[Strings] Fix extended equality rewriter (#5092) tree | commitdiff
2020-09-17 Andrew ReynoldsReduce recursion in term formula removal (#5052) tree | commitdiff
2020-09-17 yoni206Dumping internal define-funs with no arguments (#5077) tree | commitdiff
2020-09-16 Andres NoetzliOnly rewrite replace_re(_all) if regexp is const (... tree | commitdiff
2020-09-16 Abdalrhman MohamedDump commands in internal code using command printing... tree | commitdiff
2020-09-16 yoni206bv2int: support models in tests (#5068) tree | commitdiff
2020-09-15 Aina NiemetzRename system tests to api tests and remove obsolete... tree | commitdiff
2020-09-15 Andrew ReynoldsFix needsModel method for CEGQI (#5048) tree | commitdiff
2020-09-15 Ying ShengInterpolation: Add implementation for SyGuS interpolati... tree | commitdiff
2020-09-14 Andrew ReynoldsRefactoring the rewriter of sets (#4856) tree | commitdiff
2020-09-11 Andrew ReynoldsMove finite model minimization to UF last call effort... tree | commitdiff
2020-09-10 yoni206bv2int: improvement in lazy failures (#5020) tree | commitdiff
2020-09-09 Andrew ReynoldsFixes for regular expressions + sygus (#5044) tree | commitdiff
2020-09-09 mudathirmahgoubAdd is_singleton operator to the theory of sets (#5033) tree | commitdiff
2020-09-08 Andres NoetzliMake CVC/API BV div/mod semantics match SMT-LIB (#4997) tree | commitdiff
2020-09-04 Haniel Barbosa[Regressions] Fix regression issues related to BV proof... tree | commitdiff
2020-09-04 Mathias PreinerSplit lazy bit-vector solver from TheoryBV (#5009) tree | commitdiff
2020-09-03 Gereon KremerAdded a new rule to simplify (bvugt (bvurem T x) x... tree | commitdiff
2020-09-03 yoni206Changing the handled operators in bv2int preprocessing... tree | commitdiff
2020-09-02 Andres NoetzliFix CryptoMiniSat build, regression (#5006) tree | commitdiff
2020-09-02 Andres Noetzli[Python API] Add missing methods to Datatype/Term ... tree | commitdiff
2020-09-02 Andres Noetzli[API] Fix Python Examples (#4943) tree | commitdiff
2020-09-01 Haniel BarbosaRemoves old proof code (#4964) tree | commitdiff
2020-08-31 Gereon KremerFix --ackermann in the presence on syntactically differ... tree | commitdiff
2020-08-28 yoni206Incremental support for bv_to_int (#4967) tree | commitdiff
2020-08-26 Andrew ReynoldsReplace Expr-level datatype with Node-level DType ... tree | commitdiff
2020-08-24 Mathias PreinerIncrease regress level to 2 for production build. ... tree | commitdiff
2020-08-21 Andrew ReynoldsConnect the relevance manager to TheoryEngine and use... tree | commitdiff
2020-08-21 Andrew ReynoldsSimplify and fix care graph for ufHo (#4924) tree | commitdiff
2020-08-20 Andrew ReynoldsAdd strings-exp to regression (#4923) tree | commitdiff
2020-08-19 Andres NoetzliRequire `--strings-exp` when using `str.substr` (#4916) tree | commitdiff
2020-08-19 Gereon KremerChanges assertion (about maximum set cardinality) to... tree | commitdiff
2020-08-19 Andres Noetzli[Regressions] Do not test `--check-proofs` anymore... tree | commitdiff
2020-08-19 Gereon KremerFix SmtEngine::reset() (#4917) tree | commitdiff
2020-08-17 Alex OzdemirAdd identifier name for side condition. (#4902) tree | commitdiff
2020-08-13 Andrew ReynoldsSplit SmtSolver from SmtEngine (#4880) tree | commitdiff
2020-08-12 Andrew ReynoldsFixes for degenerate case of sygus decision tree learni... tree | commitdiff
2020-08-12 makaimannAdd option to only build library (#4801) tree | commitdiff
2020-08-12 Andrew ReynoldsFix unsupported option in regress1. (#4874) tree | commitdiff
2020-08-12 Andrew ReynoldsSplit SmtEngineState from SmtEngine (#4855) tree | commitdiff
2020-08-11 Andrew ReynoldsUpdate Expr-level unit tests that depend on datatypes... tree | commitdiff
2020-08-11 Aina NiemetzNew C++ API: Remove redundant API functions for mkReal... tree | commitdiff
2020-08-06 Andrew ReynoldsUpdates not related to creation for eliminating Expr... tree | commitdiff
2020-08-06 Andrew Reynolds(proof-new) Refactor regular expression operation ... tree | commitdiff
2020-08-05 Gereon KremerImprove error message for unsupported exponents (#4852) tree | commitdiff
2020-08-04 Andrew ReynoldsAdd API interface for specialized constructor term... tree | commitdiff
2020-08-03 makaimannDelete solver pointer in Cython __dealloc__ (#4799) tree | commitdiff
2020-08-02 Andres NoetzliEnsure strict length constraint for decompose rule... tree | commitdiff
2020-08-01 Andrew ReynoldsFix component contains for splicing due to substring... tree | commitdiff
2020-08-01 yoni206Add SyGuS Python API (#4812) tree | commitdiff
2020-07-30 Andres NoetzliPython API: Add support for sequences (#4757) tree | commitdiff
2020-07-28 Andrew ReynoldsFix regular expression delta for complement (#4765) tree | commitdiff
2020-07-28 yoni206Supporting seq.nth (#4723) tree | commitdiff
2020-07-28 Andrew ReynoldsUse lemma property enum for OutputChannel::lemma (... tree | commitdiff
2020-07-27 Alex OzdemirConsider negation's proof before triggering arith pfs... tree | commitdiff
2020-07-21 Andrew ReynoldsSupport uninterpreted constants in the evaluator (... tree | commitdiff
2020-07-20 Alex OzdemirFix a deadlock in the signature tests. (#4772) tree | commitdiff
2020-07-17 Andrew ReynoldsReplace options listener infrastructure (#4764) tree | commitdiff
2020-07-17 Andrew V. JonesSupport for using 'libedit' over 'readline' #4571 ... tree | commitdiff
2020-07-17 Gereon KremerIntegration of libpoly (#4679) tree | commitdiff
2020-07-15 Andres NoetzliUse Nodes for SmtEngine assertions (#4752) tree | commitdiff
2020-07-15 Andres NoetzliUse TypeNode in UninterpretedConstant (#4748) tree | commitdiff
2020-07-14 Andrew ReynoldsFix regression output. (#4741) tree | commitdiff
2020-07-14 Andres NoetzliUse TypeNode in EmptySet (#4740) tree | commitdiff
2020-07-14 Andrew ReynoldsDebug instantiations output (#4739) tree | commitdiff
2020-07-14 Andres NoetzliFix caching in TheoryEngine::getExplanation() (#4736) tree | commitdiff
2020-07-14 Andres NoetzliUse TypeNode/Node in ArrayStoreAll (#4728) tree | commitdiff
next