projects / cvc5.git / history
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
Allow to pass ProofGenerator to arithmetic inference manager. (#5488)
[cvc5.git] / test /
2020-11-19 Andrew ReynoldsEnable new implementation of CEGQI based on nested... tree | commitdiff
2020-11-19 Andrew ReynoldsUse new let binding utility in smt2 printer (#5472) tree | commitdiff
2020-11-19 Andrew ReynoldsFix issues related to eliminating extended arithmetic... tree | commitdiff
2020-11-18 Andrew ReynoldsDisable slow nl regression (#5467) tree | commitdiff
2020-11-18 Andrew ReynoldsDo not expand definitions of extended arithmetic operat... tree | commitdiff
2020-11-18 Andrew ReynoldsUse symbol manager for get assignment (#5451) tree | commitdiff
2020-11-18 Andrew ReynoldsFix asan issues related to solver and symbol manager... tree | commitdiff
2020-11-14 Andrew ReynoldsFix double conflict in extended string solver (#5435) tree | commitdiff
2020-11-13 Andrew ReynoldsMake regular expression difference left associative... tree | commitdiff
2020-11-12 yoni206Models standard (#5415) tree | commitdiff
2020-11-11 Andrew ReynoldsMove symbol manager to src/expr/ (#5420) tree | commitdiff
2020-11-11 Andrew ReynoldsPass symbol manager to commands (#5410) tree | commitdiff
2020-11-11 Andrew ReynoldsFix preregistration in TheorySep before declare-heap... tree | commitdiff
2020-11-10 Andrew ReynoldsDo not mark extended functions as reduced based on... tree | commitdiff
2020-11-10 Andrew ReynoldsAdd proper support for the declare-heap command for... tree | commitdiff
2020-11-09 Andrew ReynoldsAdd symbol manager (#5380) tree | commitdiff
2020-11-09 Andrew ReynoldsSimplify handling of subtypes in smt2 printer (#5401) tree | commitdiff
2020-11-09 Andrew ReynoldsDo not regress explanations of datatype lemmas (#5376) tree | commitdiff
2020-11-06 mudathirmahgoubFix issue #5342 (#5349) tree | commitdiff
2020-11-06 Andrew ReynoldsSimplify printing with respect to expression types... tree | commitdiff
2020-11-05 mudathirmahgoubRemove mkSingleton from the API (#5366) tree | commitdiff
2020-11-04 Andres NoetzliAdd constants from equality engine evaluation to model... tree | commitdiff
2020-11-03 Andres NoetzliAdd support for printing `re.loop` and `re.^` (#5392) tree | commitdiff
2020-11-03 Andrew ReynoldsReset built model flag at presolve in nonlinear (#5386) tree | commitdiff
2020-11-03 makaimannRun python tests during make check (#5226) tree | commitdiff
2020-11-02 Andrew ReynoldsUpdate strings proxy variable map to be context indepen... tree | commitdiff
2020-10-30 Andrew ReynoldsUpdate api::Sort to use TypeNode instead of Type (... tree | commitdiff
2020-10-29 mudathirmahgoubAdd mkInteger to the API (#5274) tree | commitdiff
2020-10-28 yoni206run_regression.py to fail on invalid requirements ... tree | commitdiff
2020-10-28 Andrew ReynoldsFixes for unconstrained variables in nonlinear model... tree | commitdiff
2020-10-28 Andrew ReynoldsConvert symbol table from Expr-level to Term-level... tree | commitdiff
2020-10-27 Mathias Preinerrun_regression: Add --skip-timeout option, lower timeou... tree | commitdiff
2020-10-27 Abdalrhman MohamedRefactor DeclareSygusVarCommand and SynthFunCommand... tree | commitdiff
2020-10-27 Andrew ReynoldsAdd missing methods involving datatype sorts to the... tree | commitdiff
2020-10-27 Gereon KremerEnable --nl-cad by default (#5345) tree | commitdiff
2020-10-27 mudathirmahgoubAdd DUPICATE_REMOVAL operator to bags (#5336) tree | commitdiff
2020-10-24 mudathirmahgoubFix issue 5271 (#5335) tree | commitdiff
2020-10-23 Andrew ReynoldsFix related to preregistering boolean term variables... tree | commitdiff
2020-10-22 mudathirmahgoubFix issue 5309 (#5327) tree | commitdiff
2020-10-21 mudathirmahgoubImplement bags evaluator (#5322) tree | commitdiff
2020-10-21 mudathirmahgoubAdd operator MakeBagOp for constructing bags (#5209) tree | commitdiff
2020-10-20 yoni206Expand `seq.nth` lazily (#5287) tree | commitdiff
2020-10-16 Andrew ReynoldsCatch more cases of nested recursion in datatypes ... tree | commitdiff
2020-10-16 yoni206bv2int: caching introduced terms (#5283) tree | commitdiff
2020-10-14 yoni206bv2int: implementing the iand-sum mode (#5265) tree | commitdiff
2020-10-14 yoni206bv2int: rewritings and unsat cores (#5263) tree | commitdiff
2020-10-12 Andrew ReynoldsRemove uf-ss-totality option (#5251) tree | commitdiff
2020-10-12 Andrew ReynoldsEliminate uses of Expr in SmtEngine interface (#5240) tree | commitdiff
2020-10-12 Andrew ReynoldsEnsure uninterpreted sort owner is UF if uf-ho or finit... tree | commitdiff
2020-10-10 Abdalrhman MohamedProvide API version of some SMT Commands. (#5222) tree | commitdiff
2020-10-09 Andres Noetzlireset-assertions: Remove all non-global symbols in... tree | commitdiff
2020-10-08 makaimannGet correct NodeManagerScope for toStrings in API ... tree | commitdiff
2020-10-08 yoni206fix unit failures on debug without symfpu (#5212) tree | commitdiff
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
next